🎰 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.
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.
(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.
(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.