🎰 Slot_repr.v
Translated OCaml
See proofs, See simulations, Gitlab , OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
Error_monad.register_error_kind Error_monad.Permanent "slot.invalid_slot"
"invalid slot" "Invalid slot"
(Some
(fun (ppf : Format.formatter) ⇒
fun (x_value : int) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "invalid slot: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format)) "invalid slot: %d")
x_value))
(Data_encoding.obj1
(Data_encoding.req None None "bad_slot" Data_encoding.int31))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_slot" then
let x_value := cast int payload in
Some x_value
else None
end) (fun (x_value : int) ⇒ Build_extensible "Invalid_slot" int x_value).
Include Compare.Int.
Definition slot : Set := t.
Definition encoding : Data_encoding.encoding int := Data_encoding.uint16.
Definition pp : Format.formatter → int → unit := Format.pp_print_int.
Definition zero : int := 0.
Definition to_int {A : Set} (x_value : A) : A := x_value.
Definition max_value : int := (Pervasives.lsl 1 16) -i 1.
Definition of_int_do_not_use_except_for_parameters {A : Set} (i_value : A)
: A := i_value.
Definition of_int (i_value : int) : M? int :=
if (i_value <i 0) || (i_value >i max_value) then
Error_monad.error_value (Build_extensible "Invalid_slot" int i_value)
else
return? i_value.
Definition succ (slot : int) : M? int := of_int (slot +i 1).
Definition Map :=
Map.Make
{|
Compare.COMPARABLE.compare := Compare.Int.compare
|}.
Definition _Set :=
_Set.Make
{|
Compare.COMPARABLE.compare := Compare.Int.compare
|}.
Module Range.
Error_monad.register_error_kind Error_monad.Permanent "slot.invalid_slot"
"invalid slot" "Invalid slot"
(Some
(fun (ppf : Format.formatter) ⇒
fun (x_value : int) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "invalid slot: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format)) "invalid slot: %d")
x_value))
(Data_encoding.obj1
(Data_encoding.req None None "bad_slot" Data_encoding.int31))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_slot" then
let x_value := cast int payload in
Some x_value
else None
end) (fun (x_value : int) ⇒ Build_extensible "Invalid_slot" int x_value).
Include Compare.Int.
Definition slot : Set := t.
Definition encoding : Data_encoding.encoding int := Data_encoding.uint16.
Definition pp : Format.formatter → int → unit := Format.pp_print_int.
Definition zero : int := 0.
Definition to_int {A : Set} (x_value : A) : A := x_value.
Definition max_value : int := (Pervasives.lsl 1 16) -i 1.
Definition of_int_do_not_use_except_for_parameters {A : Set} (i_value : A)
: A := i_value.
Definition of_int (i_value : int) : M? int :=
if (i_value <i 0) || (i_value >i max_value) then
Error_monad.error_value (Build_extensible "Invalid_slot" int i_value)
else
return? i_value.
Definition succ (slot : int) : M? int := of_int (slot +i 1).
Definition Map :=
Map.Make
{|
Compare.COMPARABLE.compare := Compare.Int.compare
|}.
Definition _Set :=
_Set.Make
{|
Compare.COMPARABLE.compare := Compare.Int.compare
|}.
Module Range.
Records for the constructor parameters
Module ConstructorRecords_t.
Module t.
Module Interval.
Record record {lo hi : Set} : Set := Build {
lo : lo;
hi : hi;
}.
Arguments record : clear implicits.
Definition with_lo {t_lo t_hi} lo (r : record t_lo t_hi) :=
Build t_lo t_hi lo r.(hi).
Definition with_hi {t_lo t_hi} hi (r : record t_lo t_hi) :=
Build t_lo t_hi r.(lo) hi.
End Interval.
Definition Interval_skeleton := Interval.record.
End t.
End ConstructorRecords_t.
Import ConstructorRecords_t.
Reserved Notation "'t.Interval".
Inductive t : Set :=
| Interval : 't.Interval → t
where "'t.Interval" := (t.Interval_skeleton int int).
Module t.
Include ConstructorRecords_t.t.
Definition Interval := 't.Interval.
End t.
Definition create (min : int) (count : int) : M? t :=
let? '_ :=
Error_monad.error_when (op_lt min 0)
(Build_extensible "Invalid_slot" int min) in
let? '_ :=
Error_monad.error_when (op_gt min max_value)
(Build_extensible "Invalid_slot" int min) in
let? '_ :=
Error_monad.error_when (op_lt count 1)
(Build_extensible "Invalid_slot" int count) in
let? '_ :=
Error_monad.error_when (op_gt count max_value)
(Build_extensible "Invalid_slot" int count) in
let max := (min +i count) -i 1 in
let? '_ :=
Error_monad.error_when (op_gt max max_value)
(Build_extensible "Invalid_slot" int max) in
return? (Interval {| t.Interval.lo := min; t.Interval.hi := max; |}).
#[bypass_check(guard)]
Definition fold {A : Set}
(f_value : A → int → A) (init_value : A) (function_parameter : t) : A :=
let 'Interval {| t.Interval.lo := lo; t.Interval.hi := hi |} :=
function_parameter in
let fix loop (acc_value : A) (next : int) {struct next} : A :=
if next >i hi then
acc_value
else
loop (f_value acc_value next) (next +i 1) in
loop (f_value init_value lo) (lo +i 1).
#[bypass_check(guard)]
Definition fold_es {A B : Set}
(f_value : A → int → Pervasives.result A B) (init_value : A)
(function_parameter : t) : Pervasives.result A B :=
let 'Interval {| t.Interval.lo := lo; t.Interval.hi := hi |} :=
function_parameter in
let fix loop (acc_value : A) (next : int) {struct next}
: Pervasives.result A B :=
if next >i hi then
return? acc_value
else
let? acc_value := f_value acc_value next in
loop acc_value (next +i 1) in
let? acc_value := f_value init_value lo in
loop acc_value (lo +i 1).
#[bypass_check(guard)]
Definition rev_fold_es {A B : Set}
(f_value : A → int → Pervasives.result A B) (init_value : A)
(function_parameter : t) : Pervasives.result A B :=
let 'Interval {| t.Interval.lo := lo; t.Interval.hi := hi |} :=
function_parameter in
let fix loop (acc_value : A) (next : int) {struct next}
: Pervasives.result A B :=
if next <i lo then
return? acc_value
else
let? acc_value := f_value acc_value next in
loop acc_value (next -i 1) in
let? acc_value := f_value init_value hi in
loop acc_value (hi -i 1).
End Range.
Module t.
Module Interval.
Record record {lo hi : Set} : Set := Build {
lo : lo;
hi : hi;
}.
Arguments record : clear implicits.
Definition with_lo {t_lo t_hi} lo (r : record t_lo t_hi) :=
Build t_lo t_hi lo r.(hi).
Definition with_hi {t_lo t_hi} hi (r : record t_lo t_hi) :=
Build t_lo t_hi r.(lo) hi.
End Interval.
Definition Interval_skeleton := Interval.record.
End t.
End ConstructorRecords_t.
Import ConstructorRecords_t.
Reserved Notation "'t.Interval".
Inductive t : Set :=
| Interval : 't.Interval → t
where "'t.Interval" := (t.Interval_skeleton int int).
Module t.
Include ConstructorRecords_t.t.
Definition Interval := 't.Interval.
End t.
Definition create (min : int) (count : int) : M? t :=
let? '_ :=
Error_monad.error_when (op_lt min 0)
(Build_extensible "Invalid_slot" int min) in
let? '_ :=
Error_monad.error_when (op_gt min max_value)
(Build_extensible "Invalid_slot" int min) in
let? '_ :=
Error_monad.error_when (op_lt count 1)
(Build_extensible "Invalid_slot" int count) in
let? '_ :=
Error_monad.error_when (op_gt count max_value)
(Build_extensible "Invalid_slot" int count) in
let max := (min +i count) -i 1 in
let? '_ :=
Error_monad.error_when (op_gt max max_value)
(Build_extensible "Invalid_slot" int max) in
return? (Interval {| t.Interval.lo := min; t.Interval.hi := max; |}).
#[bypass_check(guard)]
Definition fold {A : Set}
(f_value : A → int → A) (init_value : A) (function_parameter : t) : A :=
let 'Interval {| t.Interval.lo := lo; t.Interval.hi := hi |} :=
function_parameter in
let fix loop (acc_value : A) (next : int) {struct next} : A :=
if next >i hi then
acc_value
else
loop (f_value acc_value next) (next +i 1) in
loop (f_value init_value lo) (lo +i 1).
#[bypass_check(guard)]
Definition fold_es {A B : Set}
(f_value : A → int → Pervasives.result A B) (init_value : A)
(function_parameter : t) : Pervasives.result A B :=
let 'Interval {| t.Interval.lo := lo; t.Interval.hi := hi |} :=
function_parameter in
let fix loop (acc_value : A) (next : int) {struct next}
: Pervasives.result A B :=
if next >i hi then
return? acc_value
else
let? acc_value := f_value acc_value next in
loop acc_value (next +i 1) in
let? acc_value := f_value init_value lo in
loop acc_value (lo +i 1).
#[bypass_check(guard)]
Definition rev_fold_es {A B : Set}
(f_value : A → int → Pervasives.result A B) (init_value : A)
(function_parameter : t) : Pervasives.result A B :=
let 'Interval {| t.Interval.lo := lo; t.Interval.hi := hi |} :=
function_parameter in
let fix loop (acc_value : A) (next : int) {struct next}
: Pervasives.result A B :=
if next <i lo then
return? acc_value
else
let? acc_value := f_value acc_value next in
loop acc_value (next -i 1) in
let? acc_value := f_value init_value hi in
loop acc_value (hi -i 1).
End Range.