Skip to main content

🚪 Entrypoint_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
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).

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 resres
  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
  | NoneToo_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
  | NoneOk default
  | Some strof_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 namePervasives.Ok name
  end.

Definition of_string_strict' (str : string) : Pervasives.result t string :=
  match of_string str with
  | Too_longPervasives.Error "Entrypoint name too long"
  | Got_defaultPervasives.Error "Unexpected annotation: default"
  | Ok namePervasives.Ok name
  end.

Definition of_string_strict_exn (str : string) : t :=
  match of_string_strict' str with
  | Pervasives.Ok v_valuev_value
  | Pervasives.Error errPervasives.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 namePervasives.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_longNone
  | Got_defaultSome default
  | Ok nameSome name
  end.

Definition of_string_lax_opt (str : string) : option t :=
  match of_string str with
  | Too_longNone
  | Got_defaultSome default
  | Ok nameSome 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 namePervasives.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_defaultPervasives.Ok default
  | Ok namePervasives.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 namePervasives.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 namename
  | Pervasives.Error errPervasives.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.