➰ 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.Environment.V8.
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_value ⇒ Some (Int32.pred i_value)
  end.

Definition add (c_value : int32) (i_value : int) : M? int32 :=
  if i_value ≥i 0 then
    Pervasives.Ok (c_value +i32 (Int32.of_int i_value))
  else
    Error_monad.error_value (Build_extensible "Asserted" unit tt).

Definition sub (c_value : int32) (i_value : int) : M? (option int32) :=
  if i_value ≥i 0 then
    let r_value := c_value -i32 (Int32.of_int i_value) in
    if r_value <i32 0 then
      Pervasives.Ok None
    else
      Pervasives.Ok (Some r_value)
  else
    Error_monad.error_value (Build_extensible "Asserted" unit tt).

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
  | None ⇒ Pervasives.invalid_arg "Cycle_repr.of_string_exn"
  | Some int32_value ⇒ of_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 : M? int := return? 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) : M? (option int32) :=
    match function_parameter with
    | cons s_value [] ⇒ return? (Int32.of_string_opt s_value)
    | _ ⇒ return? 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.