Skip to main content

➰ Cycle_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.Misc.
Require TezosOfOCaml.Proto_alpha.Storage_description.

Definition t : Set := int32.

Definition cycle : Set := t.

Definition encoding : Data_encoding.encoding int32 := Data_encoding.int32_value.

Definition rpc_arg : RPC_arg.arg int32 :=
  RPC_arg.like RPC_arg.uint31 (Some "A cycle integer") "block_cycle".

Definition pp (ppf : Format.formatter) (cycle : int32) : unit :=
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
        CamlinternalFormatBasics.No_padding
        CamlinternalFormatBasics.No_precision
        CamlinternalFormatBasics.End_of_format) "%ld") cycle.

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 Map :=
  Map.Make
    {|
      Compare.COMPARABLE.compare := Compare.Int32.(Compare.S.compare)
    |}.

Definition root_value : int32 := 0.

Definition succ : int32 int32 := Int32.succ.

Definition pred (function_parameter : int32) : option int32 :=
  match function_parameter with
  | 0 ⇒ None
  | i_valueSome (Int32.pred i_value)
  end.

Definition add (c_value : int32) (i_value : int) : int32 :=
  let '_ :=
    (* ❌ Assert instruction is not handled. *)
    assert unit (i_value i 0) in
  c_value +i32 (Int32.of_int i_value).

Definition sub (c_value : int32) (i_value : int) : option int32 :=
  let '_ :=
    (* ❌ Assert instruction is not handled. *)
    assert unit (i_value i 0) in
  let r_value := c_value -i32 (Int32.of_int i_value) in
  if r_value <i32 0 then
    None
  else
    Some r_value.

Definition diff_value : int32 int32 int32 := Int32.sub.

Definition to_int32 {A : Set} (i_value : A) : A := i_value.

Definition of_int32_exn (l_value : int32) : int32 :=
  if l_value i32 0 then
    l_value
  else
    Pervasives.invalid_arg "Cycle_repr.of_int32_exn".

Definition of_string_exn (s_value : string) : int32 :=
  let int32_opt := Int32.of_string_opt s_value in
  match int32_opt with
  | NonePervasives.invalid_arg "Cycle_repr.of_string_exn"
  | Some int32_valueof_int32_exn int32_value
  end.

Definition op_minusminusminusgt : Int32.t Int32.t list Int32.t :=
  Misc.op_minusminusminusgt.

Module Index.
  Definition t : Set := cycle.

  Definition path_length : int := 1.

  Definition to_path (c_value : int32) (l_value : list string) : list string :=
    cons (Int32.to_string (to_int32 c_value)) 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.