🎰 Slot_repr.v

Simulations

See code, See proofs, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Slot_repr.

Module Range.
  Import TezosOfOCaml.Proto_alpha.Slot_repr.Range.

Simulation for [Slot_repr.Range.fold_es].

  Definition fold_es {A B : Set}
    (f_value : A → int → Pervasives.result A B) (init_value : A)
    (hi lo fuel : nat) : Pervasives.result A B :=
    let fix loop (acc_value : A) (next : nat) {struct next}
      : Pervasives.result A B :=
      match next with
      | Datatypes.O ⇒ return? acc_value
      | Datatypes.S next ⇒
          let? acc_value := f_value acc_value (Z.of_nat (hi - next)) in
          loop acc_value next
      end
    in
    let? acc_value := f_value init_value (Z.of_nat lo) in
    loop acc_value fuel.

Simulation for [Slot_repr.Range.rev_fold_es].

  Definition rev_fold_es {A B : Set}
    (f_value : A → int → Pervasives.result A B) (init_value : A)
    (hi lo fuel : nat) : Pervasives.result A B :=
    let fix loop (acc_value : A) (next : nat) {struct next}
      : Pervasives.result A B :=
      match next with
      | Datatypes.O ⇒ return? acc_value
      | Datatypes.S next ⇒
          let? acc_value := f_value acc_value (Z.of_nat (lo + next)) in
          loop acc_value next
      end
    in
    let? acc_value := f_value init_value (Z.of_nat hi) in
    loop acc_value fuel.
End Range.