🪙 Tez_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V7.
Definition id : string := "tez".
Definition name : string := "mutez".
Definition repr : Set := int64.
Inductive t : Set :=
| Tez_tag : repr → t.
Definition zero : t := Tez_tag 0.
Definition one_mutez : t := Tez_tag 1.
Definition max_mutez : t := Tez_tag Int64.max_int.
Definition mul_int (function_parameter : t) : int64 → t :=
let 'Tez_tag tez := function_parameter in
fun (i_value : int64) ⇒ Tez_tag (tez ×i64 i_value).
Definition one_cent : t := mul_int one_mutez 10000.
Definition fifty_cents : t := mul_int one_cent 50.
Definition one : t := mul_int one_cent 100.
Definition of_string (s_value : string) : option t :=
let triplets (function_parameter : list string) : bool :=
match function_parameter with
| cons hd tl ⇒
let len := String.length hd in
(len ≤i 3) &&
((len >i 0) &&
(List.for_all (fun (s_value : string) ⇒ (String.length s_value) =i 3) tl))
| [] ⇒ false
end in
let integers (s_value : string) : bool :=
triplets (String.split_on_char "," % char s_value) in
let decimals (s_value : string) : bool :=
let l_value := String.split_on_char "," % char s_value in
if Compare.List_length_with.op_gt l_value 2 then
false
else
triplets (List.rev l_value) in
let parse (_left : string) (_right : string) : option t :=
let remove_commas (s_value : string) : string :=
String.concat "" (String.split_on_char "," % char s_value) in
let pad_to_six (s_value : string) : string :=
let len := String.length s_value in
String.init_value 6
(fun (i_value : int) ⇒
if i_value <i len then
String.get s_value i_value
else
"0" % char) in
let prepared :=
Pervasives.op_caret (remove_commas _left)
(pad_to_six (remove_commas _right)) in
Option.map (fun (i_value : repr) ⇒ Tez_tag i_value)
(Int64.of_string_opt prepared) in
match String.split_on_char "." % char s_value with
| cons _left (cons _right []) ⇒
if String.contains s_value "," % char then
if (integers _left) && (decimals _right) then
parse _left _right
else
None
else
if ((String.length _right) >i 0) && ((String.length _right) ≤i 6) then
parse _left _right
else
None
| cons _left [] ⇒
if
(Pervasives.not (String.contains s_value "," % char)) || (integers _left)
then
parse _left ""
else
None
| _ ⇒ None
end.
#[bypass_check(guard)]
Definition pp (ppf : Format.formatter) (function_parameter : t) : unit :=
let 'Tez_tag amount := function_parameter in
let mult_int := 1000000 in
let fix _left (ppf : Format.formatter) (amount : int64) {struct amount}
: unit :=
let '(d_value, r_value) := ((amount /i64 1000), (Int64.rem amount 1000)) in
if d_value >i64 0 then
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
(CamlinternalFormatBasics.Lit_padding
CamlinternalFormatBasics.Zeros 3)
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format)) "%a%03Ld") _left d_value
r_value
else
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format) "%Ld") r_value in
let _right (ppf : Format.formatter) (amount : int) : unit :=
let triplet (ppf : Format.formatter) (v_value : int) : unit :=
if (Pervasives._mod v_value 10) >i 0 then
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
(CamlinternalFormatBasics.Lit_padding
CamlinternalFormatBasics.Zeros 3)
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format) "%03d") v_value
else
if (Pervasives._mod v_value 100) >i 0 then
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
(CamlinternalFormatBasics.Lit_padding
CamlinternalFormatBasics.Zeros 2)
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format) "%02d") (v_value /i 10)
else
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format) "%d") (v_value /i 100)
in
let '(hi, lo) := ((amount /i 1000), (Pervasives._mod amount 1000)) in
if lo =i 0 then
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format)
"%a") triplet hi
else
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
(CamlinternalFormatBasics.Lit_padding CamlinternalFormatBasics.Zeros
3) CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)) "%03d%a") hi triplet lo
in
let '(ints, decs) :=
((amount /i64 mult_int), (Int64.to_int (Int64.rem amount mult_int))) in
let '_ := _left ppf ints in
if decs >i 0 then
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Char_literal "." % char
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format))
".%a") _right decs
else
tt.
Definition to_string (t_value : t) : string :=
Format.asprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format)
"%a") pp t_value.
Definition op_minusquestion (tez1 : t) (tez2 : t) : M? t :=
let 'Tez_tag t1 := tez1 in
let 'Tez_tag t2 := tez2 in
if t2 ≤i64 t1 then
return? (Tez_tag (t1 -i64 t2))
else
Error_monad.error_value
(Build_extensible "Subtraction_underflow" (t × t) (tez1, tez2)).
Definition sub_opt (function_parameter : t) : t → option t :=
let 'Tez_tag t1 := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag t2 := function_parameter in
if t2 ≤i64 t1 then
Some (Tez_tag (t1 -i64 t2))
else
None.
Definition op_plusquestion (tez1 : t) (tez2 : t) : M? t :=
let 'Tez_tag t1 := tez1 in
let 'Tez_tag t2 := tez2 in
let t_value := t1 +i64 t2 in
if t_value <i64 t1 then
Error_monad.error_value
(Build_extensible "Addition_overflow" (t × t) (tez1, tez2))
else
return? (Tez_tag t_value).
Definition op_starquestion (tez : t) (m_value : int64) : M? t :=
let 'Tez_tag t_value := tez in
if m_value <i64 0 then
Error_monad.error_value
(Build_extensible "Negative_multiplicator" (t × int64) (tez, m_value))
else
if m_value =i64 0 then
return? (Tez_tag 0)
else
if t_value >i64 (Int64.max_int /i64 m_value) then
Error_monad.error_value
(Build_extensible "Multiplication_overflow" (t × int64) (tez, m_value))
else
return? (Tez_tag (t_value ×i64 m_value)).
Definition op_divquestion (tez : t) (d_value : int64) : M? t :=
let 'Tez_tag t_value := tez in
if d_value ≤i64 0 then
Error_monad.error_value
(Build_extensible "Invalid_divisor" (t × int64) (tez, d_value))
else
return? (Tez_tag (t_value /i64 d_value)).
Definition mul_exn (t_value : t) (m_value : int) : t :=
match op_starquestion t_value (Int64.of_int m_value) with
| Pervasives.Ok v_value ⇒ v_value
| Pervasives.Error _ ⇒ Pervasives.invalid_arg "mul_exn"
end.
Definition div_exn (t_value : t) (d_value : int) : t :=
match op_divquestion t_value (Int64.of_int d_value) with
| Pervasives.Ok v_value ⇒ v_value
| Pervasives.Error _ ⇒ Pervasives.invalid_arg "div_exn"
end.
Definition of_mutez (t_value : int64) : option t :=
if t_value <i64 0 then
None
else
Some (Tez_tag t_value).
Definition of_mutez_exn (x_value : int64) : t :=
match of_mutez x_value with
| None ⇒ Pervasives.invalid_arg "Tez.of_mutez"
| Some v_value ⇒ v_value
end.
Definition to_mutez (function_parameter : t) : repr :=
let 'Tez_tag t_value := function_parameter in
t_value.
Definition encoding : Data_encoding.encoding t :=
let decode (function_parameter : t) : Z.t :=
let 'Tez_tag t_value := function_parameter in
Z.of_int64 t_value in
let encode :=
Data_encoding.Json.wrap_error
(fun (i_value : Z.t) ⇒ Tez_tag (Z.to_int64 i_value)) in
Data_encoding.def name None None
(Data_encoding.check_size 10
(Data_encoding.conv decode encode None Data_encoding.n_value)).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V7.
Definition id : string := "tez".
Definition name : string := "mutez".
Definition repr : Set := int64.
Inductive t : Set :=
| Tez_tag : repr → t.
Definition zero : t := Tez_tag 0.
Definition one_mutez : t := Tez_tag 1.
Definition max_mutez : t := Tez_tag Int64.max_int.
Definition mul_int (function_parameter : t) : int64 → t :=
let 'Tez_tag tez := function_parameter in
fun (i_value : int64) ⇒ Tez_tag (tez ×i64 i_value).
Definition one_cent : t := mul_int one_mutez 10000.
Definition fifty_cents : t := mul_int one_cent 50.
Definition one : t := mul_int one_cent 100.
Definition of_string (s_value : string) : option t :=
let triplets (function_parameter : list string) : bool :=
match function_parameter with
| cons hd tl ⇒
let len := String.length hd in
(len ≤i 3) &&
((len >i 0) &&
(List.for_all (fun (s_value : string) ⇒ (String.length s_value) =i 3) tl))
| [] ⇒ false
end in
let integers (s_value : string) : bool :=
triplets (String.split_on_char "," % char s_value) in
let decimals (s_value : string) : bool :=
let l_value := String.split_on_char "," % char s_value in
if Compare.List_length_with.op_gt l_value 2 then
false
else
triplets (List.rev l_value) in
let parse (_left : string) (_right : string) : option t :=
let remove_commas (s_value : string) : string :=
String.concat "" (String.split_on_char "," % char s_value) in
let pad_to_six (s_value : string) : string :=
let len := String.length s_value in
String.init_value 6
(fun (i_value : int) ⇒
if i_value <i len then
String.get s_value i_value
else
"0" % char) in
let prepared :=
Pervasives.op_caret (remove_commas _left)
(pad_to_six (remove_commas _right)) in
Option.map (fun (i_value : repr) ⇒ Tez_tag i_value)
(Int64.of_string_opt prepared) in
match String.split_on_char "." % char s_value with
| cons _left (cons _right []) ⇒
if String.contains s_value "," % char then
if (integers _left) && (decimals _right) then
parse _left _right
else
None
else
if ((String.length _right) >i 0) && ((String.length _right) ≤i 6) then
parse _left _right
else
None
| cons _left [] ⇒
if
(Pervasives.not (String.contains s_value "," % char)) || (integers _left)
then
parse _left ""
else
None
| _ ⇒ None
end.
#[bypass_check(guard)]
Definition pp (ppf : Format.formatter) (function_parameter : t) : unit :=
let 'Tez_tag amount := function_parameter in
let mult_int := 1000000 in
let fix _left (ppf : Format.formatter) (amount : int64) {struct amount}
: unit :=
let '(d_value, r_value) := ((amount /i64 1000), (Int64.rem amount 1000)) in
if d_value >i64 0 then
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
(CamlinternalFormatBasics.Lit_padding
CamlinternalFormatBasics.Zeros 3)
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format)) "%a%03Ld") _left d_value
r_value
else
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format) "%Ld") r_value in
let _right (ppf : Format.formatter) (amount : int) : unit :=
let triplet (ppf : Format.formatter) (v_value : int) : unit :=
if (Pervasives._mod v_value 10) >i 0 then
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
(CamlinternalFormatBasics.Lit_padding
CamlinternalFormatBasics.Zeros 3)
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format) "%03d") v_value
else
if (Pervasives._mod v_value 100) >i 0 then
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
(CamlinternalFormatBasics.Lit_padding
CamlinternalFormatBasics.Zeros 2)
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format) "%02d") (v_value /i 10)
else
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format) "%d") (v_value /i 100)
in
let '(hi, lo) := ((amount /i 1000), (Pervasives._mod amount 1000)) in
if lo =i 0 then
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format)
"%a") triplet hi
else
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
(CamlinternalFormatBasics.Lit_padding CamlinternalFormatBasics.Zeros
3) CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Alpha
CamlinternalFormatBasics.End_of_format)) "%03d%a") hi triplet lo
in
let '(ints, decs) :=
((amount /i64 mult_int), (Int64.to_int (Int64.rem amount mult_int))) in
let '_ := _left ppf ints in
if decs >i 0 then
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Char_literal "." % char
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format))
".%a") _right decs
else
tt.
Definition to_string (t_value : t) : string :=
Format.asprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format)
"%a") pp t_value.
Definition op_minusquestion (tez1 : t) (tez2 : t) : M? t :=
let 'Tez_tag t1 := tez1 in
let 'Tez_tag t2 := tez2 in
if t2 ≤i64 t1 then
return? (Tez_tag (t1 -i64 t2))
else
Error_monad.error_value
(Build_extensible "Subtraction_underflow" (t × t) (tez1, tez2)).
Definition sub_opt (function_parameter : t) : t → option t :=
let 'Tez_tag t1 := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag t2 := function_parameter in
if t2 ≤i64 t1 then
Some (Tez_tag (t1 -i64 t2))
else
None.
Definition op_plusquestion (tez1 : t) (tez2 : t) : M? t :=
let 'Tez_tag t1 := tez1 in
let 'Tez_tag t2 := tez2 in
let t_value := t1 +i64 t2 in
if t_value <i64 t1 then
Error_monad.error_value
(Build_extensible "Addition_overflow" (t × t) (tez1, tez2))
else
return? (Tez_tag t_value).
Definition op_starquestion (tez : t) (m_value : int64) : M? t :=
let 'Tez_tag t_value := tez in
if m_value <i64 0 then
Error_monad.error_value
(Build_extensible "Negative_multiplicator" (t × int64) (tez, m_value))
else
if m_value =i64 0 then
return? (Tez_tag 0)
else
if t_value >i64 (Int64.max_int /i64 m_value) then
Error_monad.error_value
(Build_extensible "Multiplication_overflow" (t × int64) (tez, m_value))
else
return? (Tez_tag (t_value ×i64 m_value)).
Definition op_divquestion (tez : t) (d_value : int64) : M? t :=
let 'Tez_tag t_value := tez in
if d_value ≤i64 0 then
Error_monad.error_value
(Build_extensible "Invalid_divisor" (t × int64) (tez, d_value))
else
return? (Tez_tag (t_value /i64 d_value)).
Definition mul_exn (t_value : t) (m_value : int) : t :=
match op_starquestion t_value (Int64.of_int m_value) with
| Pervasives.Ok v_value ⇒ v_value
| Pervasives.Error _ ⇒ Pervasives.invalid_arg "mul_exn"
end.
Definition div_exn (t_value : t) (d_value : int) : t :=
match op_divquestion t_value (Int64.of_int d_value) with
| Pervasives.Ok v_value ⇒ v_value
| Pervasives.Error _ ⇒ Pervasives.invalid_arg "div_exn"
end.
Definition of_mutez (t_value : int64) : option t :=
if t_value <i64 0 then
None
else
Some (Tez_tag t_value).
Definition of_mutez_exn (x_value : int64) : t :=
match of_mutez x_value with
| None ⇒ Pervasives.invalid_arg "Tez.of_mutez"
| Some v_value ⇒ v_value
end.
Definition to_mutez (function_parameter : t) : repr :=
let 'Tez_tag t_value := function_parameter in
t_value.
Definition encoding : Data_encoding.encoding t :=
let decode (function_parameter : t) : Z.t :=
let 'Tez_tag t_value := function_parameter in
Z.of_int64 t_value in
let encode :=
Data_encoding.Json.wrap_error
(fun (i_value : Z.t) ⇒ Tez_tag (Z.to_int64 i_value)) in
Data_encoding.def name None None
(Data_encoding.check_size 10
(Data_encoding.conv decode encode None Data_encoding.n_value)).
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
(Pervasives.op_caret id ".addition_overflow")
(Pervasives.op_caret "Overflowing " (Pervasives.op_caret id " addition"))
(Pervasives.op_caret "An addition of two "
(Pervasives.op_caret id " amounts overflowed"))
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : t × t) ⇒
let '(opa, opb) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Overflowing addition of "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal " " % char
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " and "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal " " % char
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))))))))
"Overflowing addition of %a %s and %a %s") pp opa id pp opb id))
(Data_encoding.obj1
(Data_encoding.req None None "amounts"
(Data_encoding.tup2 encoding encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Addition_overflow" then
let '(a_value, b_value) := cast (t × t) payload in
Some (a_value, b_value)
else None
end)
(fun (function_parameter : t × t) ⇒
let '(a_value, b_value) := function_parameter in
Build_extensible "Addition_overflow" (t × t) (a_value, b_value)) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
(Pervasives.op_caret id ".subtraction_underflow")
(Pervasives.op_caret "Underflowing "
(Pervasives.op_caret id " subtraction"))
(Pervasives.op_caret "A subtraction of two "
(Pervasives.op_caret id " amounts underflowed"))
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : t × t) ⇒
let '(opa, opb) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Underflowing subtraction of "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal " " % char
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " and "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal " " % char
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))))))))
"Underflowing subtraction of %a %s and %a %s") pp opa id pp opb
id))
(Data_encoding.obj1
(Data_encoding.req None None "amounts"
(Data_encoding.tup2 encoding encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Subtraction_underflow" then
let '(a_value, b_value) := cast (t × t) payload in
Some (a_value, b_value)
else None
end)
(fun (function_parameter : t × t) ⇒
let '(a_value, b_value) := function_parameter in
Build_extensible "Subtraction_underflow" (t × t) (a_value, b_value)) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
(Pervasives.op_caret id ".multiplication_overflow")
(Pervasives.op_caret "Overflowing "
(Pervasives.op_caret id " multiplication"))
(Pervasives.op_caret "A multiplication of a "
(Pervasives.op_caret id " amount by an integer overflowed"))
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : t × int64) ⇒
let '(opa, opb) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Overflowing multiplication of "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal " " % char
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " and "
(CamlinternalFormatBasics.Int64
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format))))))
"Overflowing multiplication of %a %s and %Ld") pp opa id opb))
(Data_encoding.obj2 (Data_encoding.req None None "amount" encoding)
(Data_encoding.req None None "multiplicator" Data_encoding.int64_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Multiplication_overflow" then
let '(a_value, b_value) := cast (t × int64) payload in
Some (a_value, b_value)
else None
end)
(fun (function_parameter : t × int64) ⇒
let '(a_value, b_value) := function_parameter in
Build_extensible "Multiplication_overflow" (t × int64)
(a_value, b_value)) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
(Pervasives.op_caret id ".negative_multiplicator")
(Pervasives.op_caret "Negative " (Pervasives.op_caret id " multiplicator"))
(Pervasives.op_caret "Multiplication of a "
(Pervasives.op_caret id " amount by a negative integer"))
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : t × int64) ⇒
let '(opa, opb) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Multiplication of "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal " " % char
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
" by negative integer "
(CamlinternalFormatBasics.Int64
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format))))))
"Multiplication of %a %s by negative integer %Ld") pp opa id opb))
(Data_encoding.obj2 (Data_encoding.req None None "amount" encoding)
(Data_encoding.req None None "multiplicator" Data_encoding.int64_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Negative_multiplicator" then
let '(a_value, b_value) := cast (t × int64) payload in
Some (a_value, b_value)
else None
end)
(fun (function_parameter : t × int64) ⇒
let '(a_value, b_value) := function_parameter in
Build_extensible "Negative_multiplicator" (t × int64) (a_value, b_value))
in
Error_monad.register_error_kind Error_monad.Temporary
(Pervasives.op_caret id ".invalid_divisor")
(Pervasives.op_caret "Invalid " (Pervasives.op_caret id " divisor"))
(Pervasives.op_caret "Multiplication of a "
(Pervasives.op_caret id " amount by a non positive integer"))
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : t × int64) ⇒
let '(opa, opb) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Division of "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal " " % char
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
" by non positive integer "
(CamlinternalFormatBasics.Int64
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format))))))
"Division of %a %s by non positive integer %Ld") pp opa id opb))
(Data_encoding.obj2 (Data_encoding.req None None "amount" encoding)
(Data_encoding.req None None "divisor" Data_encoding.int64_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_divisor" then
let '(a_value, b_value) := cast (t × int64) payload in
Some (a_value, b_value)
else None
end)
(fun (function_parameter : t × int64) ⇒
let '(a_value, b_value) := function_parameter in
Build_extensible "Invalid_divisor" (t × int64) (a_value, b_value)).
Definition tez : Set := t.
Definition compare (function_parameter : t) : t → int :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
Compare.Int64.(Compare.S.compare) x_value y_value.
Definition op_eq (function_parameter : t) : t → bool :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
x_value =i64 y_value.
Definition op_ltgt (function_parameter : t) : t → bool :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
x_value ≠i64 y_value.
Definition op_lt (function_parameter : t) : t → bool :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
x_value <i64 y_value.
Definition op_gt (function_parameter : t) : t → bool :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
x_value >i64 y_value.
Definition op_lteq (function_parameter : t) : t → bool :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
x_value ≤i64 y_value.
Definition op_gteq (function_parameter : t) : t → bool :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
x_value ≥i64 y_value.
Definition equal (function_parameter : t) : t → bool :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
Compare.Int64.(Compare.S.equal) x_value y_value.
Definition max (function_parameter : t) : t → t :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
Tez_tag (Compare.Int64.(Compare.S.max) x_value y_value).
Definition min (function_parameter : t) : t → t :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
Tez_tag (Compare.Int64.(Compare.S.min) x_value y_value).
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
(Pervasives.op_caret id ".addition_overflow")
(Pervasives.op_caret "Overflowing " (Pervasives.op_caret id " addition"))
(Pervasives.op_caret "An addition of two "
(Pervasives.op_caret id " amounts overflowed"))
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : t × t) ⇒
let '(opa, opb) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Overflowing addition of "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal " " % char
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " and "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal " " % char
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))))))))
"Overflowing addition of %a %s and %a %s") pp opa id pp opb id))
(Data_encoding.obj1
(Data_encoding.req None None "amounts"
(Data_encoding.tup2 encoding encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Addition_overflow" then
let '(a_value, b_value) := cast (t × t) payload in
Some (a_value, b_value)
else None
end)
(fun (function_parameter : t × t) ⇒
let '(a_value, b_value) := function_parameter in
Build_extensible "Addition_overflow" (t × t) (a_value, b_value)) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
(Pervasives.op_caret id ".subtraction_underflow")
(Pervasives.op_caret "Underflowing "
(Pervasives.op_caret id " subtraction"))
(Pervasives.op_caret "A subtraction of two "
(Pervasives.op_caret id " amounts underflowed"))
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : t × t) ⇒
let '(opa, opb) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Underflowing subtraction of "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal " " % char
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " and "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal " " % char
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format))))))))
"Underflowing subtraction of %a %s and %a %s") pp opa id pp opb
id))
(Data_encoding.obj1
(Data_encoding.req None None "amounts"
(Data_encoding.tup2 encoding encoding)))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Subtraction_underflow" then
let '(a_value, b_value) := cast (t × t) payload in
Some (a_value, b_value)
else None
end)
(fun (function_parameter : t × t) ⇒
let '(a_value, b_value) := function_parameter in
Build_extensible "Subtraction_underflow" (t × t) (a_value, b_value)) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
(Pervasives.op_caret id ".multiplication_overflow")
(Pervasives.op_caret "Overflowing "
(Pervasives.op_caret id " multiplication"))
(Pervasives.op_caret "A multiplication of a "
(Pervasives.op_caret id " amount by an integer overflowed"))
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : t × int64) ⇒
let '(opa, opb) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Overflowing multiplication of "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal " " % char
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal " and "
(CamlinternalFormatBasics.Int64
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format))))))
"Overflowing multiplication of %a %s and %Ld") pp opa id opb))
(Data_encoding.obj2 (Data_encoding.req None None "amount" encoding)
(Data_encoding.req None None "multiplicator" Data_encoding.int64_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Multiplication_overflow" then
let '(a_value, b_value) := cast (t × int64) payload in
Some (a_value, b_value)
else None
end)
(fun (function_parameter : t × int64) ⇒
let '(a_value, b_value) := function_parameter in
Build_extensible "Multiplication_overflow" (t × int64)
(a_value, b_value)) in
let '_ :=
Error_monad.register_error_kind Error_monad.Temporary
(Pervasives.op_caret id ".negative_multiplicator")
(Pervasives.op_caret "Negative " (Pervasives.op_caret id " multiplicator"))
(Pervasives.op_caret "Multiplication of a "
(Pervasives.op_caret id " amount by a negative integer"))
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : t × int64) ⇒
let '(opa, opb) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Multiplication of "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal " " % char
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
" by negative integer "
(CamlinternalFormatBasics.Int64
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format))))))
"Multiplication of %a %s by negative integer %Ld") pp opa id opb))
(Data_encoding.obj2 (Data_encoding.req None None "amount" encoding)
(Data_encoding.req None None "multiplicator" Data_encoding.int64_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Negative_multiplicator" then
let '(a_value, b_value) := cast (t × int64) payload in
Some (a_value, b_value)
else None
end)
(fun (function_parameter : t × int64) ⇒
let '(a_value, b_value) := function_parameter in
Build_extensible "Negative_multiplicator" (t × int64) (a_value, b_value))
in
Error_monad.register_error_kind Error_monad.Temporary
(Pervasives.op_caret id ".invalid_divisor")
(Pervasives.op_caret "Invalid " (Pervasives.op_caret id " divisor"))
(Pervasives.op_caret "Multiplication of a "
(Pervasives.op_caret id " amount by a non positive integer"))
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : t × int64) ⇒
let '(opa, opb) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Division of "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.Char_literal " " % char
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
" by non positive integer "
(CamlinternalFormatBasics.Int64
CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format))))))
"Division of %a %s by non positive integer %Ld") pp opa id opb))
(Data_encoding.obj2 (Data_encoding.req None None "amount" encoding)
(Data_encoding.req None None "divisor" Data_encoding.int64_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_divisor" then
let '(a_value, b_value) := cast (t × int64) payload in
Some (a_value, b_value)
else None
end)
(fun (function_parameter : t × int64) ⇒
let '(a_value, b_value) := function_parameter in
Build_extensible "Invalid_divisor" (t × int64) (a_value, b_value)).
Definition tez : Set := t.
Definition compare (function_parameter : t) : t → int :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
Compare.Int64.(Compare.S.compare) x_value y_value.
Definition op_eq (function_parameter : t) : t → bool :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
x_value =i64 y_value.
Definition op_ltgt (function_parameter : t) : t → bool :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
x_value ≠i64 y_value.
Definition op_lt (function_parameter : t) : t → bool :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
x_value <i64 y_value.
Definition op_gt (function_parameter : t) : t → bool :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
x_value >i64 y_value.
Definition op_lteq (function_parameter : t) : t → bool :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
x_value ≤i64 y_value.
Definition op_gteq (function_parameter : t) : t → bool :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
x_value ≥i64 y_value.
Definition equal (function_parameter : t) : t → bool :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
Compare.Int64.(Compare.S.equal) x_value y_value.
Definition max (function_parameter : t) : t → t :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
Tez_tag (Compare.Int64.(Compare.S.max) x_value y_value).
Definition min (function_parameter : t) : t → t :=
let 'Tez_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Tez_tag y_value := function_parameter in
Tez_tag (Compare.Int64.(Compare.S.min) x_value y_value).