🚪 Entrypoint_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.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Non_empty_string.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Module Pre_entrypoint.
Definition t : Set := Non_empty_string.t.
Definition of_non_empty_string (str : Non_empty_string.t)
: option Non_empty_string.t :=
if (String.length str) >i 31 then
None
else
Some str.
End Pre_entrypoint.
Definition t : Set := Pre_entrypoint.t.
Definition compare (x_value : t) (y_value : t) : int :=
Non_empty_string.compare x_value y_value.
Definition op_eq (x_value : t) (y_value : t) : bool :=
Non_empty_string.op_eq x_value y_value.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Non_empty_string.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Module Pre_entrypoint.
Definition t : Set := Non_empty_string.t.
Definition of_non_empty_string (str : Non_empty_string.t)
: option Non_empty_string.t :=
if (String.length str) >i 31 then
None
else
Some str.
End Pre_entrypoint.
Definition t : Set := Pre_entrypoint.t.
Definition compare (x_value : t) (y_value : t) : int :=
Non_empty_string.compare x_value y_value.
Definition op_eq (x_value : t) (y_value : t) : bool :=
Non_empty_string.op_eq x_value y_value.
Init function; without side-effects in Coq
Definition init_module1 : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"michelson_v1.entrypoint_name_too_long"
"Entrypoint name too long (type error)"
"An entrypoint name exceeds the maximum length of 31 characters." None
(Data_encoding.obj1
(Data_encoding.req None None "name" Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Name_too_long" then
let entrypoint := cast string payload in
Some entrypoint
else None
end)
(fun (entrypoint : string) ⇒
Build_extensible "Name_too_long" string entrypoint).
Error_monad.register_error_kind Error_monad.Permanent
"michelson_v1.entrypoint_name_too_long"
"Entrypoint name too long (type error)"
"An entrypoint name exceeds the maximum length of 31 characters." None
(Data_encoding.obj1
(Data_encoding.req None None "name" Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Name_too_long" then
let entrypoint := cast string payload in
Some entrypoint
else None
end)
(fun (entrypoint : string) ⇒
Build_extensible "Name_too_long" string entrypoint).
Init function; without side-effects in Coq
Definition init_module2 : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"michelson_v1.unexpected_default_entrypoint"
"The annotation 'default' was encountered where an entrypoint is expected"
"A node in the syntax tree was improperly annotated. An annotation used to designate an entrypoint cannot be exactly 'default'."
None
(Data_encoding.obj1
(Data_encoding.req None None "location" Script_repr.location_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpected_default" then
let loc_value := cast Script_repr.location payload in
Some loc_value
else None
end)
(fun (loc_value : Script_repr.location) ⇒
Build_extensible "Unexpected_default" Script_repr.location loc_value).
Definition default : Pre_entrypoint.t :=
match
Pre_entrypoint.of_non_empty_string
(Non_empty_string.of_string_exn "default") with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert Pre_entrypoint.t false
| Some res ⇒ res
end.
Definition is_default (name : t) : bool := op_eq name default.
Inductive of_string_result : Set :=
| Ok : t → of_string_result
| Too_long : of_string_result
| Got_default : of_string_result.
Definition of_non_empty_string (str : Non_empty_string.t) : of_string_result :=
match Pre_entrypoint.of_non_empty_string str with
| None ⇒ Too_long
| Some str ⇒
if is_default str then
Got_default
else
Ok str
end.
Definition of_string (str : string) : of_string_result :=
match Non_empty_string.of_string str with
| None ⇒ Ok default
| Some str ⇒ of_non_empty_string str
end.
Definition of_string_strict (loc_value : Script_repr.location) (str : string)
: M? t :=
match of_string str with
| Too_long ⇒
Error_monad.error_value (Build_extensible "Name_too_long" string str)
| Got_default ⇒
Error_monad.error_value
(Build_extensible "Unexpected_default" Script_repr.location loc_value)
| Ok name ⇒ Pervasives.Ok name
end.
Definition of_string_strict' (str : string) : Pervasives.result t string :=
match of_string str with
| Too_long ⇒ Pervasives.Error "Entrypoint name too long"
| Got_default ⇒ Pervasives.Error "Unexpected annotation: default"
| Ok name ⇒ Pervasives.Ok name
end.
Definition of_string_strict_exn (str : string) : t :=
match of_string_strict' str with
| Pervasives.Ok v_value ⇒ v_value
| Pervasives.Error err ⇒ Pervasives.invalid_arg err
end.
Definition of_annot_strict
(loc_value : Script_repr.location) (a_value : Non_empty_string.t) : M? t :=
match of_non_empty_string a_value with
| Too_long ⇒
Error_monad.error_value (Build_extensible "Name_too_long" string a_value)
| Got_default ⇒
Error_monad.error_value
(Build_extensible "Unexpected_default" Script_repr.location loc_value)
| Ok name ⇒ Pervasives.Ok name
end.
Definition of_annot_lax_opt (a_value : Non_empty_string.t) : option t :=
match of_non_empty_string a_value with
| Too_long ⇒ None
| Got_default ⇒ Some default
| Ok name ⇒ Some name
end.
Definition of_string_lax_opt (str : string) : option t :=
match of_string str with
| Too_long ⇒ None
| Got_default ⇒ Some default
| Ok name ⇒ Some name
end.
Definition of_string_lax (str : string) : M? t :=
match of_string_lax_opt str with
| None ⇒
Error_monad.error_value (Build_extensible "Name_too_long" string str)
| Some name ⇒ Pervasives.Ok name
end.
Definition of_annot_lax (a_value : Non_empty_string.t) : M? t :=
match of_non_empty_string a_value with
| Too_long ⇒
Error_monad.error_value (Build_extensible "Name_too_long" string a_value)
| Got_default ⇒ Pervasives.Ok default
| Ok name ⇒ Pervasives.Ok name
end.
Definition of_string_lax' (str : string) : Pervasives.result t string :=
match of_string_lax_opt str with
| None ⇒
Pervasives.Error
(Pervasives.op_caret "Entrypoint name too long """
(Pervasives.op_caret str """"))
| Some name ⇒ Pervasives.Ok name
end.
Definition root_value : t := of_string_strict_exn "root".
Definition do_ : t := of_string_strict_exn "do".
Definition set_delegate : t := of_string_strict_exn "set_delegate".
Definition remove_delegate : t := of_string_strict_exn "remove_delegate".
Definition deposit : t := of_string_strict_exn "deposit".
Definition is_deposit : t → bool := op_eq deposit.
Definition is_root : t → bool := op_eq root_value.
Definition to_non_empty_string (name : t) : Non_empty_string.t := name.
Definition to_string (name : t) : string := name.
Definition to_address_suffix (name : t) : string :=
if is_default name then
""
else
Pervasives.op_caret "%" name.
Definition unparse_as_field_annot (name : t) : string :=
Pervasives.op_caret "%" name.
Definition of_string_lax_exn (str : string) : t :=
match of_string_lax' str with
| Pervasives.Ok name ⇒ name
| Pervasives.Error err ⇒ Pervasives.invalid_arg err
end.
Definition pp (fmt : Format.formatter) (name : t) : unit :=
Format.pp_print_string fmt name.
Definition simple_encoding : Data_encoding.encoding t :=
Data_encoding.conv_with_guard (fun (name : t) ⇒ name) of_string_lax' None
Data_encoding.string_value.
Definition value_encoding : Data_encoding.encoding t :=
Data_encoding.conv_with_guard
(fun (name : t) ⇒
if is_default name then
""
else
name) of_string_strict' None Data_encoding._Variable.string_value.
Definition smart_encoding : Data_encoding.encoding t :=
Data_encoding.def "entrypoint" (Some "entrypoint")
(Some "Named entrypoint to a Michelson smart contract")
(let builtin_case (tag : int) (name : Pre_entrypoint.t)
: Data_encoding.case t :=
Data_encoding.case_value name None (Data_encoding.Tag tag)
(Data_encoding.constant name)
(fun (n_value : t) ⇒
if op_eq n_value name then
Some tt
else
None)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
name) in
Data_encoding.union None
[
builtin_case 0 default;
builtin_case 1 root_value;
builtin_case 2 do_;
builtin_case 3 set_delegate;
builtin_case 4 remove_delegate;
builtin_case 5 deposit;
Data_encoding.case_value "named" None (Data_encoding.Tag 255)
(Data_encoding.Bounded.string_value 31)
(fun (name : t) ⇒ Some name) of_string_lax_exn
]).
Definition rpc_arg : RPC_arg.arg t :=
RPC_arg.make (Some "A Michelson entrypoint (string of length < 32)")
"entrypoint" of_string_lax' (fun (name : t) ⇒ name) tt.
Definition in_memory_size (name : t) : Saturation_repr.t :=
Cache_memory_helpers.string_size_gen (String.length name).
Module T.
Definition t : Set := t.
Definition compare : t → t → int := compare.
(* T *)
Definition module :=
{|
Compare.COMPARABLE.compare := compare
|}.
End T.
Definition T := T.module.
Definition _Set := _Set.Make T.
Definition Map := Map.Make T.
Error_monad.register_error_kind Error_monad.Permanent
"michelson_v1.unexpected_default_entrypoint"
"The annotation 'default' was encountered where an entrypoint is expected"
"A node in the syntax tree was improperly annotated. An annotation used to designate an entrypoint cannot be exactly 'default'."
None
(Data_encoding.obj1
(Data_encoding.req None None "location" Script_repr.location_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unexpected_default" then
let loc_value := cast Script_repr.location payload in
Some loc_value
else None
end)
(fun (loc_value : Script_repr.location) ⇒
Build_extensible "Unexpected_default" Script_repr.location loc_value).
Definition default : Pre_entrypoint.t :=
match
Pre_entrypoint.of_non_empty_string
(Non_empty_string.of_string_exn "default") with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert Pre_entrypoint.t false
| Some res ⇒ res
end.
Definition is_default (name : t) : bool := op_eq name default.
Inductive of_string_result : Set :=
| Ok : t → of_string_result
| Too_long : of_string_result
| Got_default : of_string_result.
Definition of_non_empty_string (str : Non_empty_string.t) : of_string_result :=
match Pre_entrypoint.of_non_empty_string str with
| None ⇒ Too_long
| Some str ⇒
if is_default str then
Got_default
else
Ok str
end.
Definition of_string (str : string) : of_string_result :=
match Non_empty_string.of_string str with
| None ⇒ Ok default
| Some str ⇒ of_non_empty_string str
end.
Definition of_string_strict (loc_value : Script_repr.location) (str : string)
: M? t :=
match of_string str with
| Too_long ⇒
Error_monad.error_value (Build_extensible "Name_too_long" string str)
| Got_default ⇒
Error_monad.error_value
(Build_extensible "Unexpected_default" Script_repr.location loc_value)
| Ok name ⇒ Pervasives.Ok name
end.
Definition of_string_strict' (str : string) : Pervasives.result t string :=
match of_string str with
| Too_long ⇒ Pervasives.Error "Entrypoint name too long"
| Got_default ⇒ Pervasives.Error "Unexpected annotation: default"
| Ok name ⇒ Pervasives.Ok name
end.
Definition of_string_strict_exn (str : string) : t :=
match of_string_strict' str with
| Pervasives.Ok v_value ⇒ v_value
| Pervasives.Error err ⇒ Pervasives.invalid_arg err
end.
Definition of_annot_strict
(loc_value : Script_repr.location) (a_value : Non_empty_string.t) : M? t :=
match of_non_empty_string a_value with
| Too_long ⇒
Error_monad.error_value (Build_extensible "Name_too_long" string a_value)
| Got_default ⇒
Error_monad.error_value
(Build_extensible "Unexpected_default" Script_repr.location loc_value)
| Ok name ⇒ Pervasives.Ok name
end.
Definition of_annot_lax_opt (a_value : Non_empty_string.t) : option t :=
match of_non_empty_string a_value with
| Too_long ⇒ None
| Got_default ⇒ Some default
| Ok name ⇒ Some name
end.
Definition of_string_lax_opt (str : string) : option t :=
match of_string str with
| Too_long ⇒ None
| Got_default ⇒ Some default
| Ok name ⇒ Some name
end.
Definition of_string_lax (str : string) : M? t :=
match of_string_lax_opt str with
| None ⇒
Error_monad.error_value (Build_extensible "Name_too_long" string str)
| Some name ⇒ Pervasives.Ok name
end.
Definition of_annot_lax (a_value : Non_empty_string.t) : M? t :=
match of_non_empty_string a_value with
| Too_long ⇒
Error_monad.error_value (Build_extensible "Name_too_long" string a_value)
| Got_default ⇒ Pervasives.Ok default
| Ok name ⇒ Pervasives.Ok name
end.
Definition of_string_lax' (str : string) : Pervasives.result t string :=
match of_string_lax_opt str with
| None ⇒
Pervasives.Error
(Pervasives.op_caret "Entrypoint name too long """
(Pervasives.op_caret str """"))
| Some name ⇒ Pervasives.Ok name
end.
Definition root_value : t := of_string_strict_exn "root".
Definition do_ : t := of_string_strict_exn "do".
Definition set_delegate : t := of_string_strict_exn "set_delegate".
Definition remove_delegate : t := of_string_strict_exn "remove_delegate".
Definition deposit : t := of_string_strict_exn "deposit".
Definition is_deposit : t → bool := op_eq deposit.
Definition is_root : t → bool := op_eq root_value.
Definition to_non_empty_string (name : t) : Non_empty_string.t := name.
Definition to_string (name : t) : string := name.
Definition to_address_suffix (name : t) : string :=
if is_default name then
""
else
Pervasives.op_caret "%" name.
Definition unparse_as_field_annot (name : t) : string :=
Pervasives.op_caret "%" name.
Definition of_string_lax_exn (str : string) : t :=
match of_string_lax' str with
| Pervasives.Ok name ⇒ name
| Pervasives.Error err ⇒ Pervasives.invalid_arg err
end.
Definition pp (fmt : Format.formatter) (name : t) : unit :=
Format.pp_print_string fmt name.
Definition simple_encoding : Data_encoding.encoding t :=
Data_encoding.conv_with_guard (fun (name : t) ⇒ name) of_string_lax' None
Data_encoding.string_value.
Definition value_encoding : Data_encoding.encoding t :=
Data_encoding.conv_with_guard
(fun (name : t) ⇒
if is_default name then
""
else
name) of_string_strict' None Data_encoding._Variable.string_value.
Definition smart_encoding : Data_encoding.encoding t :=
Data_encoding.def "entrypoint" (Some "entrypoint")
(Some "Named entrypoint to a Michelson smart contract")
(let builtin_case (tag : int) (name : Pre_entrypoint.t)
: Data_encoding.case t :=
Data_encoding.case_value name None (Data_encoding.Tag tag)
(Data_encoding.constant name)
(fun (n_value : t) ⇒
if op_eq n_value name then
Some tt
else
None)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
name) in
Data_encoding.union None
[
builtin_case 0 default;
builtin_case 1 root_value;
builtin_case 2 do_;
builtin_case 3 set_delegate;
builtin_case 4 remove_delegate;
builtin_case 5 deposit;
Data_encoding.case_value "named" None (Data_encoding.Tag 255)
(Data_encoding.Bounded.string_value 31)
(fun (name : t) ⇒ Some name) of_string_lax_exn
]).
Definition rpc_arg : RPC_arg.arg t :=
RPC_arg.make (Some "A Michelson entrypoint (string of length < 32)")
"entrypoint" of_string_lax' (fun (name : t) ⇒ name) tt.
Definition in_memory_size (name : t) : Saturation_repr.t :=
Cache_memory_helpers.string_size_gen (String.length name).
Module T.
Definition t : Set := t.
Definition compare : t → t → int := compare.
(* T *)
Definition module :=
{|
Compare.COMPARABLE.compare := compare
|}.
End T.
Definition T := T.module.
Definition _Set := _Set.Make T.
Definition Map := Map.Make T.