🪜 Raw_level_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Definition t : Set := int32.
Definition raw_level : Set := t.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
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 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) : int32 :=
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit (i_value ≥i 0) in
l_value +i32 (Int32.of_int i_value).
Definition sub (l_value : int32) (i_value : int) : option int32 :=
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit (i_value ≥i 0) in
let res := l_value -i32 (Int32.of_int i_value) in
if res ≥i32 0 then
Some res
else
None.
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 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 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) : int32 :=
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit (i_value ≥i 0) in
l_value +i32 (Int32.of_int i_value).
Definition sub (l_value : int32) (i_value : int) : option int32 :=
let '_ :=
(* ❌ Assert instruction is not handled. *)
assert unit (i_value ≥i 0) in
let res := l_value -i32 (Int32.of_int i_value) in
if res ≥i32 0 then
Some res
else
None.
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.
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 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 : int := 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) : option int32 :=
match function_parameter with
| cons s_value [] ⇒ Int32.of_string_opt s_value
| _ ⇒ 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 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 : int := 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) : option int32 :=
match function_parameter with
| cons s_value [] ⇒ Int32.of_string_opt s_value
| _ ⇒ 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.