Skip to main content

🕰️ Period_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.

Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent "malformed_period"
      "Malformed period" "Period is negative."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (period : int64) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "The given period '"
                  (CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
                    CamlinternalFormatBasics.No_padding
                    CamlinternalFormatBasics.No_precision
                    (CamlinternalFormatBasics.String_literal "' is negative "
                      CamlinternalFormatBasics.End_of_format)))
                "The given period '%Ld' is negative ") period))
      (Data_encoding.obj1
        (Data_encoding.req None None "malformed_period"
          Data_encoding.int64_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Malformed_period" then
            let n_value := cast int64 payload in
            Some n_value
          else None
        end)
      (fun (n_value : int64) ⇒
        Build_extensible "Malformed_period" int64 n_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent "invalid_arg"
      "Invalid arg" "Negative multiple of periods are not allowed."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Invalid arg"
                  CamlinternalFormatBasics.End_of_format) "Invalid arg")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_arg" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Invalid_arg" unit tt) in
  let title := "Period overflow" in
  Error_monad.register_error_kind Error_monad.Permanent "period_overflow" title
    "Last operation generated an integer overflow."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String
                CamlinternalFormatBasics.No_padding
                CamlinternalFormatBasics.End_of_format) "%s") title))
    Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Period_overflow" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Period_overflow" unit tt).

Module INTERNAL.
  Record signature : Set := {
    t := int64;
    create : int64 option t;
    zero : t;
    one : t;
    mult_ : t t option t;
    add_ : t t option t;
    encoding : Data_encoding.t t;
    rpc_arg : RPC_arg.arg t;
    pp : Format.formatter t unit;
    op_eq : t t bool;
    op_ltgt : t t bool;
    op_lt : t t bool;
    op_lteq : t t bool;
    op_gteq : t t bool;
    op_gt : t t bool;
    compare : t t int;
    equal : t t bool;
    max : t t t;
    min : t t t;
  }.
End INTERNAL.
Definition INTERNAL := INTERNAL.signature.

Module Internal.
  Definition t : Set := Int64.t.

  Definition encoding : Data_encoding.encoding int64 :=
    Data_encoding.with_decoding_guard
      (fun (t_value : int64) ⇒
        if t_value i64 0 then
          Pervasives.Ok tt
        else
          Pervasives.Error "Positive int64 required") Data_encoding.int64_value.

  Definition rpc_arg : RPC_arg.arg int64 := RPC_arg.uint63.

  Definition pp (ppf : Format.formatter) (v_value : int64) : unit :=
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
          CamlinternalFormatBasics.No_padding
          CamlinternalFormatBasics.No_precision
          CamlinternalFormatBasics.End_of_format) "%Ld") v_value.

Inclusion of the module [Compare.Int64]
  Definition op_eq := Compare.Int64.(Compare.S.op_eq).

  Definition op_ltgt := Compare.Int64.(Compare.S.op_ltgt).

  Definition op_lt := Compare.Int64.(Compare.S.op_lt).

  Definition op_lteq := Compare.Int64.(Compare.S.op_lteq).

  Definition op_gteq := Compare.Int64.(Compare.S.op_gteq).

  Definition op_gt := Compare.Int64.(Compare.S.op_gt).

  Definition compare := Compare.Int64.(Compare.S.compare).

  Definition equal := Compare.Int64.(Compare.S.equal).

  Definition max := Compare.Int64.(Compare.S.max).

  Definition min := Compare.Int64.(Compare.S.min).

  Definition zero : int64 := 0.

  Definition one : int64 := 1.

  Definition create (t_value : t) : option t :=
    if op_gteq t_value zero then
      Some t_value
    else
      None.

  Definition mult_ (a_value : t) (b_value : t) : option int64 :=
    if op_ltgt a_value zero then
      let res := a_value ×i64 b_value in
      if op_ltgt (res /i64 a_value) b_value then
        None
      else
        Some res
    else
      Some zero.

  Definition add_ (a_value : t) (b_value : t) : option int64 :=
    let res := a_value +i64 b_value in
    if (op_lt res a_value) || (op_lt res b_value) then
      None
    else
      Some res.

  (* Internal *)
  Definition module :=
    {|
      INTERNAL.create := create;
      INTERNAL.zero := zero;
      INTERNAL.one := one;
      INTERNAL.mult_ := mult_;
      INTERNAL.add_ := add_;
      INTERNAL.encoding := encoding;
      INTERNAL.rpc_arg := rpc_arg;
      INTERNAL.pp := pp;
      INTERNAL.op_eq := op_eq;
      INTERNAL.op_ltgt := op_ltgt;
      INTERNAL.op_lt := op_lt;
      INTERNAL.op_lteq := op_lteq;
      INTERNAL.op_gteq := op_gteq;
      INTERNAL.op_gt := op_gt;
      INTERNAL.compare := compare;
      INTERNAL.equal := equal;
      INTERNAL.max := max;
      INTERNAL.min := min
    |}.
End Internal.
Definition Internal : INTERNAL := Internal.module.

Inclusion of the module [Internal]
Definition t := Internal.(INTERNAL.t).

Definition create := Internal.(INTERNAL.create).

Definition zero := Internal.(INTERNAL.zero).

Definition one := Internal.(INTERNAL.one).

Definition mult_ := Internal.(INTERNAL.mult_).

Definition add_ := Internal.(INTERNAL.add_).

Definition encoding := Internal.(INTERNAL.encoding).

Definition rpc_arg := Internal.(INTERNAL.rpc_arg).

Definition pp := Internal.(INTERNAL.pp).

Definition op_eq := Internal.(INTERNAL.op_eq).

Definition op_ltgt := Internal.(INTERNAL.op_ltgt).

Definition op_lt := Internal.(INTERNAL.op_lt).

Definition op_lteq := Internal.(INTERNAL.op_lteq).

Definition op_gteq := Internal.(INTERNAL.op_gteq).

Definition op_gt := Internal.(INTERNAL.op_gt).

Definition compare := Internal.(INTERNAL.compare).

Definition equal := Internal.(INTERNAL.equal).

Definition max := Internal.(INTERNAL.max).

Definition min := Internal.(INTERNAL.min).

Definition period : Set := int64.

Definition to_seconds (t_value : int64) : int64 := t_value.

Definition of_seconds (secs : int64) : M? int64 :=
  match Internal.(INTERNAL.create) secs with
  | Some v_valuereturn? v_value
  | None
    Error_monad.error_value (Build_extensible "Malformed_period" int64 secs)
  end.

Definition of_seconds_exn (t_value : int64) : int64 :=
  match Internal.(INTERNAL.create) t_value with
  | Some t_valuet_value
  | NonePervasives.invalid_arg "Period.of_seconds_exn"
  end.

Definition mult (i_value : int32) (p_value : int64) : M? int64 :=
  match Internal.(INTERNAL.create) (Int64.of_int32 i_value) with
  | NoneError_monad.error_value (Build_extensible "Invalid_arg" unit tt)
  | Some iper
    match Internal.(INTERNAL.mult_) iper p_value with
    | None
      Error_monad.error_value (Build_extensible "Period_overflow" unit tt)
    | Some resreturn? res
    end
  end.

Definition add (p1 : int64) (p2 : int64) : M? int64 :=
  match Internal.(INTERNAL.add_) p1 p2 with
  | NoneError_monad.error_value (Build_extensible "Period_overflow" unit tt)
  | Some resreturn? res
  end.

Definition op_plusquestion : int64 int64 M? int64 := add.

Definition one_second : int64 := Internal.(INTERNAL.one).

Definition one_minute : int64 := of_seconds_exn 60.

Definition one_hour : int64 := of_seconds_exn 3600.