Skip to main content

🍬 Script_timestamp.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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Time_repr.

Definition repr : Set := Z.t.

Inductive t : Set :=
| Timestamp_tag : repr t.

Definition compare (function_parameter : t) : t int :=
  let 'Timestamp_tag x_value := function_parameter in
  fun (function_parameter : t) ⇒
    let 'Timestamp_tag y_value := function_parameter in
    Z.compare x_value y_value.

Definition of_int64 (i_value : int64) : t := Timestamp_tag (Z.of_int64 i_value).

Definition of_string (x_value : string) : option t :=
  match Time_repr.of_notation x_value with
  | None
    Option.catch None
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Timestamp_tag (Z.of_string x_value))
  | Some timeSome (of_int64 (Time_repr.to_seconds time))
  end.

Definition to_notation (function_parameter : t) : option string :=
  let 'Timestamp_tag x_value := function_parameter in
  Option.catch None
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Time_repr.to_notation (Time.of_seconds (Z.to_int64 x_value))).

Definition to_num_str (function_parameter : t) : string :=
  let 'Timestamp_tag x_value := function_parameter in
  Z.to_string x_value.

Definition to_string (x_value : t) : string :=
  match to_notation x_value with
  | Noneto_num_str x_value
  | Some s_values_value
  end.

Definition diff_value (function_parameter : t) : t Script_int.num :=
  let 'Timestamp_tag x_value := function_parameter in
  fun (function_parameter : t) ⇒
    let 'Timestamp_tag y_value := function_parameter in
    Script_int.of_zint (x_value -Z y_value).

Definition sub_delta (function_parameter : t) : Script_int.num t :=
  let 'Timestamp_tag t_value := function_parameter in
  fun (delta : Script_int.num) ⇒
    Timestamp_tag (t_value -Z (Script_int.to_zint delta)).

Definition add_delta (function_parameter : t) : Script_int.num t :=
  let 'Timestamp_tag t_value := function_parameter in
  fun (delta : Script_int.num) ⇒
    Timestamp_tag (t_value +Z (Script_int.to_zint delta)).

Definition to_zint (function_parameter : t) : repr :=
  let 'Timestamp_tag x_value := function_parameter in
  x_value.

Definition of_zint (x_value : repr) : t := Timestamp_tag x_value.

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.conv to_zint of_zint None Data_encoding.z_value.

Definition now (ctxt : Alpha_context.context) : t :=
  let first_delay :=
    Alpha_context.Period.to_seconds
      (Alpha_context.Constants.minimal_block_delay ctxt) in
  let current_timestamp := Alpha_context.Timestamp.predecessor ctxt in
  of_int64
    (Alpha_context.Timestamp.to_seconds (Time.add current_timestamp first_delay)).