🍬 Script_timestamp.v
Translated 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 time ⇒ Some (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
| None ⇒ to_num_str x_value
| Some s_value ⇒ s_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)).
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 time ⇒ Some (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
| None ⇒ to_num_str x_value
| Some s_value ⇒ s_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)).