Skip to main content

🪜 Raw_level_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.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.

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_valuel_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_valuePervasives.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.