🕰️ Time_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.Period_repr.

Include Time.

Definition time : Set := Time.t.

Init function; without side-effects in Coq

Definition init_module_repr : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent "timestamp_add"
      "Timestamp add" "Overflow when adding timestamps."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Overflow when adding timestamps."
                  CamlinternalFormatBasics.End_of_format)
                "Overflow when adding timestamps."))) Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Timestamp_add" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Timestamp_add" unit tt) in
  Error_monad.register_error_kind Error_monad.Permanent "timestamp_sub"
    "Timestamp sub" "Subtracting timestamps resulted in negative period."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Subtracting timestamps resulted in negative period."
                CamlinternalFormatBasics.End_of_format)
              "Subtracting timestamps resulted in negative period.")))
    Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Timestamp_sub" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Timestamp_sub" unit tt).

Definition of_seconds_string (s_value : string) : option Time.t :=
  Option.map Time.of_seconds (Int64.of_string_opt s_value).

Definition to_seconds_string (s_value : t) : string :=
  Int64.to_string (to_seconds s_value).

Definition pp : Format.formatter → t → unit := pp_hum.

Definition op_plusquestion (x_value : Time.t) (y_value : Period_repr.period)
  : M? Time.t :=
  let span := Period_repr.to_seconds y_value in
  let t64 := Time.add x_value span in
  if op_lt x_value (Time.of_seconds 0) then
    return? t64
  else
    if op_lt t64 (Time.of_seconds 0) then
      Error_monad.error_value (Build_extensible "Timestamp_add" unit tt)
    else
      return? t64.

Definition op_minusquestion (x_value : Time.t) (y_value : Time.t)
  : M? Period_repr.period :=
  Error_monad.record_trace (Build_extensible "Timestamp_sub" unit tt)
    (Period_repr.of_seconds (Time.diff_value x_value y_value)).

Definition op_minus (x_value : Time.t) (y_value : Period_repr.period)
  : Time.t :=
  Time.of_seconds
    ((Time.to_seconds x_value) -i64 (Period_repr.to_seconds y_value)).