🕰️ Period_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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.
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.
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_value ⇒ return? 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_value ⇒ t_value
| None ⇒ Pervasives.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
| None ⇒ Error_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 res ⇒ return? res
end
end.
Definition add (p1 : int64) (p2 : int64) : M? int64 :=
match Internal.(INTERNAL.add_) p1 p2 with
| None ⇒ Error_monad.error_value (Build_extensible "Period_overflow" unit tt)
| Some res ⇒ return? 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.
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_value ⇒ return? 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_value ⇒ t_value
| None ⇒ Pervasives.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
| None ⇒ Error_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 res ⇒ return? res
end
end.
Definition add (p1 : int64) (p2 : int64) : M? int64 :=
match Internal.(INTERNAL.add_) p1 p2 with
| None ⇒ Error_monad.error_value (Build_extensible "Period_overflow" unit tt)
| Some res ⇒ return? 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.