🪜 Raw_level_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Definition t : Set := int32.
Definition raw_level : Set := t.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Definition t : Set := int32.
Definition raw_level : Set := t.
Inclusion of the module [Compare.Int32]
Definition op_eq := Compare.Int32.(Compare.S.op_eq).
Definition op_ltgt := Compare.Int32.(Compare.S.op_ltgt).
Definition op_lt := Compare.Int32.(Compare.S.op_lt).
Definition op_lteq := Compare.Int32.(Compare.S.op_lteq).
Definition op_gteq := Compare.Int32.(Compare.S.op_gteq).
Definition op_gt := Compare.Int32.(Compare.S.op_gt).
Definition compare := Compare.Int32.(Compare.S.compare).
Definition equal := Compare.Int32.(Compare.S.equal).
Definition max := Compare.Int32.(Compare.S.max).
Definition min := Compare.Int32.(Compare.S.min).
Definition _Set :=
_Set.Make
{|
Compare.COMPARABLE.compare := Compare.Int32.(Compare.S.compare)
|}.
Definition Map :=
Map.Make
{|
Compare.COMPARABLE.compare := Compare.Int32.(Compare.S.compare)
|}.
Definition pp (ppf : Format.formatter) (level : int32) : unit :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format) "%ld") level.
Definition rpc_arg : RPC_arg.arg int32 :=
let construct (raw_level : int32) : string :=
Int32.to_string raw_level in
let destruct (str : string) : Pervasives.result int32 string :=
Option.to_result "Cannot parse level" (Int32.of_string_opt str) in
RPC_arg.make (Some "A level integer") "block_level" destruct construct tt.
Definition root_value : int32 := 0.
Definition succ : int32 → int32 := Int32.succ.
Definition add (l_value : int32) (i_value : int) : M? int32 :=
if i_value ≥i 0 then
return? (l_value +i32 (Int32.of_int i_value))
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Definition sub (l_value : int32) (i_value : int) : M? (option int32) :=
if i_value ≥i 0 then
let res := l_value -i32 (Int32.of_int i_value) in
if res ≥i32 0 then
Error_monad.Result_syntax.return_some res
else
Error_monad.Result_syntax.return_none
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Definition pred (l_value : t) : option int32 :=
if op_eq l_value 0 then
None
else
Some (Int32.pred l_value).
Definition diff_value : int32 → int32 → int32 := Int32.sub.
Definition to_int32 {A : Set} (l_value : A) : A := l_value.
Definition to_int32_non_negative (l_value : int32)
: M? Bounded.Non_negative_int32.(Bounded.S.t) :=
match Bounded.Non_negative_int32.(Bounded.S.of_value) l_value with
| Some x_value ⇒ return? x_value
| _ ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
end.
Definition op_ltgt := Compare.Int32.(Compare.S.op_ltgt).
Definition op_lt := Compare.Int32.(Compare.S.op_lt).
Definition op_lteq := Compare.Int32.(Compare.S.op_lteq).
Definition op_gteq := Compare.Int32.(Compare.S.op_gteq).
Definition op_gt := Compare.Int32.(Compare.S.op_gt).
Definition compare := Compare.Int32.(Compare.S.compare).
Definition equal := Compare.Int32.(Compare.S.equal).
Definition max := Compare.Int32.(Compare.S.max).
Definition min := Compare.Int32.(Compare.S.min).
Definition _Set :=
_Set.Make
{|
Compare.COMPARABLE.compare := Compare.Int32.(Compare.S.compare)
|}.
Definition Map :=
Map.Make
{|
Compare.COMPARABLE.compare := Compare.Int32.(Compare.S.compare)
|}.
Definition pp (ppf : Format.formatter) (level : int32) : unit :=
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format) "%ld") level.
Definition rpc_arg : RPC_arg.arg int32 :=
let construct (raw_level : int32) : string :=
Int32.to_string raw_level in
let destruct (str : string) : Pervasives.result int32 string :=
Option.to_result "Cannot parse level" (Int32.of_string_opt str) in
RPC_arg.make (Some "A level integer") "block_level" destruct construct tt.
Definition root_value : int32 := 0.
Definition succ : int32 → int32 := Int32.succ.
Definition add (l_value : int32) (i_value : int) : M? int32 :=
if i_value ≥i 0 then
return? (l_value +i32 (Int32.of_int i_value))
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Definition sub (l_value : int32) (i_value : int) : M? (option int32) :=
if i_value ≥i 0 then
let res := l_value -i32 (Int32.of_int i_value) in
if res ≥i32 0 then
Error_monad.Result_syntax.return_some res
else
Error_monad.Result_syntax.return_none
else
Error_monad.error_value (Build_extensible "Asserted" unit tt).
Definition pred (l_value : t) : option int32 :=
if op_eq l_value 0 then
None
else
Some (Int32.pred l_value).
Definition diff_value : int32 → int32 → int32 := Int32.sub.
Definition to_int32 {A : Set} (l_value : A) : A := l_value.
Definition to_int32_non_negative (l_value : int32)
: M? Bounded.Non_negative_int32.(Bounded.S.t) :=
match Bounded.Non_negative_int32.(Bounded.S.of_value) l_value with
| Some x_value ⇒ return? x_value
| _ ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
end.
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
Error_monad.register_error_kind Error_monad.Permanent "unexpected_level"
"Unexpected level" "Level must be non-negative."
(Some
(fun (ppf : Format.formatter) ⇒
fun (l_value : Int32.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "The level is "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
" but should be non-negative."
CamlinternalFormatBasics.End_of_format)))
"The level is %s but should be non-negative.")
(Int32.to_string l_value)))
(Data_encoding.obj1
(Data_encoding.req None None "level" Data_encoding.int32_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpected_level" then
let l_value := cast Int32.t payload in
Some l_value
else None
end)
(fun (l_value : Int32.t) ⇒
Build_extensible "Unexpected_level" Int32.t l_value).
Definition of_int32 (l_value : int32) : M? int32 :=
if l_value ≥i32 0 then
return? l_value
else
Error_monad.error_value (Build_extensible "Unexpected_level" int32 l_value).
Definition of_int32_exn (l_value : int32) : int32 :=
match of_int32 l_value with
| Pervasives.Ok l_value ⇒ l_value
| Pervasives.Error _ ⇒ Pervasives.invalid_arg "Level_repr.of_int32"
end.
Definition of_int32_non_negative
(l_value : Bounded.Non_negative_int32.(Bounded.S.t)) : M? int32 :=
match of_int32 (Bounded.Non_negative_int32.(Bounded.S.to_value) l_value) with
| Pervasives.Ok l_value ⇒ return? l_value
| Pervasives.Error _ ⇒
Error_monad.error_value (Build_extensible "Asserted" unit tt)
end.
Definition encoding : Data_encoding.encoding int32 :=
Data_encoding.conv_with_guard to_int32
(fun (l_value : int32) ⇒
match of_int32 l_value with
| Pervasives.Ok l_value ⇒ Pervasives.Ok l_value
| Pervasives.Error _ ⇒ Pervasives.Error "Level_repr.of_int32"
end) None Data_encoding.int32_value.
Module Index.
Definition t : Set := raw_level.
Definition path_length : M? int := return? 1.
Definition to_path (level : int32) (l_value : list string) : list string :=
cons (Int32.to_string level) l_value.
Definition of_path (function_parameter : list string) : M? (option int32) :=
match function_parameter with
| cons s_value [] ⇒ return? (Int32.of_string_opt s_value)
| _ ⇒ return? None
end.
Definition rpc_arg : RPC_arg.arg int32 := rpc_arg.
Definition encoding : Data_encoding.encoding int32 := encoding.
Definition compare : t → t → int := compare.
(* Index *)
Definition module :=
{|
Storage_description.INDEX.path_length := path_length;
Storage_description.INDEX.to_path := to_path;
Storage_description.INDEX.of_path := of_path;
Storage_description.INDEX.rpc_arg := rpc_arg;
Storage_description.INDEX.encoding := encoding;
Storage_description.INDEX.compare := compare
|}.
End Index.
Definition Index := Index.module.
Error_monad.register_error_kind Error_monad.Permanent "unexpected_level"
"Unexpected level" "Level must be non-negative."
(Some
(fun (ppf : Format.formatter) ⇒
fun (l_value : Int32.t) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "The level is "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
" but should be non-negative."
CamlinternalFormatBasics.End_of_format)))
"The level is %s but should be non-negative.")
(Int32.to_string l_value)))
(Data_encoding.obj1
(Data_encoding.req None None "level" Data_encoding.int32_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpected_level" then
let l_value := cast Int32.t payload in
Some l_value
else None
end)
(fun (l_value : Int32.t) ⇒
Build_extensible "Unexpected_level" Int32.t l_value).
Definition of_int32 (l_value : int32) : M? int32 :=
if l_value ≥i32 0 then
return? l_value
else
Error_monad.error_value (Build_extensible "Unexpected_level" int32 l_value).
Definition of_int32_exn (l_value : int32) : int32 :=
match of_int32 l_value with
| Pervasives.Ok l_value ⇒ l_value
| Pervasives.Error _ ⇒ Pervasives.invalid_arg "Level_repr.of_int32"
end.
Definition of_int32_non_negative
(l_value : Bounded.Non_negative_int32.(Bounded.S.t)) : M? int32 :=
match of_int32 (Bounded.Non_negative_int32.(Bounded.S.to_value) l_value) with
| Pervasives.Ok l_value ⇒ return? l_value
| Pervasives.Error _ ⇒
Error_monad.error_value (Build_extensible "Asserted" unit tt)
end.
Definition encoding : Data_encoding.encoding int32 :=
Data_encoding.conv_with_guard to_int32
(fun (l_value : int32) ⇒
match of_int32 l_value with
| Pervasives.Ok l_value ⇒ Pervasives.Ok l_value
| Pervasives.Error _ ⇒ Pervasives.Error "Level_repr.of_int32"
end) None Data_encoding.int32_value.
Module Index.
Definition t : Set := raw_level.
Definition path_length : M? int := return? 1.
Definition to_path (level : int32) (l_value : list string) : list string :=
cons (Int32.to_string level) l_value.
Definition of_path (function_parameter : list string) : M? (option int32) :=
match function_parameter with
| cons s_value [] ⇒ return? (Int32.of_string_opt s_value)
| _ ⇒ return? None
end.
Definition rpc_arg : RPC_arg.arg int32 := rpc_arg.
Definition encoding : Data_encoding.encoding int32 := encoding.
Definition compare : t → t → int := compare.
(* Index *)
Definition module :=
{|
Storage_description.INDEX.path_length := path_length;
Storage_description.INDEX.to_path := to_path;
Storage_description.INDEX.of_path := of_path;
Storage_description.INDEX.rpc_arg := rpc_arg;
Storage_description.INDEX.encoding := encoding;
Storage_description.INDEX.compare := compare
|}.
End Index.
Definition Index := Index.module.