🍃 Z.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Coq.ZArith.Zeuclid.
Require TezosOfOCaml.Environment.Structs.V0.Format.
Require TezosOfOCaml.Environment.Structs.V0.Int32.
Require TezosOfOCaml.Environment.Structs.V0.Int64.
Definition t : Set := Z.
Definition zero : t := 0.
Definition one : t := 1.
Definition minus_one : t := -1.
Definition of_int (a : int) : t := a.
Definition of_int32 (a : int32) : t := a.
Definition of_int64 (a : int64) : t := a.
Parameter of_string : string → t.
Parameter of_substring : string → int → int → t.
Parameter of_string_base : int → string → t.
Parameter of_substring_base : int → string → int → int → t.
Definition succ : t → t := fun z ⇒ Z.add z 1.
Definition pred : t → t := fun z ⇒ Z.sub z 1.
Definition abs : t → t := Z.abs.
Definition neg (a : t) : t := -a.
Definition add : t → t → t := Z.add.
Definition sub : t → t → t := Z.sub.
Definition mul : t → t → t := Z.mul.
Definition div : t → t → t := Z.quot.
Definition rem : t → t → t := Z.rem.
Definition div_rem (a b : t) : t × t :=
(Z.quot a b, Z.rem a b).
Parameter cdiv : t → t → t.
Parameter fdiv : t → t → t.
Definition ediv_rem (a b : t) : t × t :=
if b =? 0 then
Pervasives.raise (Build_extensible "Division_by_zero" unit tt)
else
(Zeuclid.ZEuclid.div a b, Zeuclid.ZEuclid.modulo a b).
Definition ediv (a b : t) : t :=
fst (ediv_rem a b).
Definition erem (a b : t) : t :=
snd (ediv_rem a b).
Parameter divexact : t → t → t.
Parameter divisible : t → t → bool.
Parameter congruent : t → t → t → bool.
Definition logand : t → t → t :=
Z.land.
Definition logor : t → t → t :=
Z.lor.
Definition logxor : t → t → t :=
Z.lxor.
Definition lognot : t → t :=
Z.lnot.
Definition shift_left : t → int → t :=
Z.shiftl.
Definition shift_right : t → int → t := Z.shiftr.
Parameter shift_right_trunc : t → int → t.
Parameter numbits : t → int.
Parameter trailing_zeros : t → int.
Definition testbit : t → int → bool :=
Z.testbit.
Parameter popcount : t → int.
Parameter hamdist : t → t → int.
Definition to_int (z : t) : int :=
if andb (Pervasives.min_int <=? z) (z <=? Pervasives.max_int) then
z
else
Pervasives.raise (Build_extensible "Overflow" unit tt).
Definition to_int32 (z : t) : int32 :=
if andb (Int32.min_int <=? z) (z <=? Int32.max_int) then
z
else
Pervasives.raise (Build_extensible "Overflow" unit tt).
Definition to_int64 (z : t) : int64 :=
if andb (Int64.min_int <=? z) (z <=? Int64.max_int) then
z
else
Pervasives.raise (Build_extensible "Overflow" unit tt).
Parameter to_string : t → string.
Parameter format : string → t → string.
Definition fits_int (z : t) : bool :=
(Pervasives.min_int <=? z) && (z <=? Pervasives.max_int).
Definition fits_int32 (z : t) : bool :=
(Int32.min_int <=? z) && (z <=? Int32.max_int).
Definition fits_int64 (z : t) : bool :=
(Int64.min_int <=? z) && (z <=? Int64.max_int).
Parameter pp_print : Format.formatter → t → unit.
Definition compare (a b : t) : int :=
if a <? b then
-1
else if a =? b then
0
else
1.
Definition equal : t → t → bool := Z.eqb.
Definition leq : t → t → bool := Z.leb.
Definition geq : t → t → bool := Z.geb.
Definition lt : t → t → bool := Z.ltb.
Definition gt : t → t → bool := Z.gtb.
Parameter sign : t → int.
Definition min : t → t → t := Z.min.
Definition max : t → t → t := Z.max.
Definition is_even : t → bool := Z.even.
Definition is_odd : t → bool := Z.odd.
Parameter pow : t → int → t.
Parameter sqrt : t → t.
Parameter sqrt_rem : t → t × t.
Parameter root_value : t → int → t.
Parameter rootrem : t → int → t × t.
Parameter perfect_power : t → bool.
Parameter perfect_square : t → bool.
Parameter log2 : t → int.
Parameter log2up : t → int.
Parameter size_value : t → int.
Parameter extract : t → int → int → t.
Parameter signed_extract : t → int → int → t.
Parameter to_bits : t → string.
Parameter of_bits : string → t.
Module Notations.
Infix "+Z" := add (at level 50, left associativity).
Infix "-Z" := sub (at level 50, left associativity).
Infix "*Z" := mul (at level 40, left associativity).
Infix "/Z" := div (at level 40, left associativity).
End Notations.
Global Hint Unfold
zero
one
minus_one
of_int
of_int32
of_int64
succ
pred
abs
neg
add
sub
mul
div
rem
div_rem
compare
equal
leq
geq
lt
gt
min
max
: tezos_z.
Require Import CoqOfOCaml.Settings.
Require Coq.ZArith.Zeuclid.
Require TezosOfOCaml.Environment.Structs.V0.Format.
Require TezosOfOCaml.Environment.Structs.V0.Int32.
Require TezosOfOCaml.Environment.Structs.V0.Int64.
Definition t : Set := Z.
Definition zero : t := 0.
Definition one : t := 1.
Definition minus_one : t := -1.
Definition of_int (a : int) : t := a.
Definition of_int32 (a : int32) : t := a.
Definition of_int64 (a : int64) : t := a.
Parameter of_string : string → t.
Parameter of_substring : string → int → int → t.
Parameter of_string_base : int → string → t.
Parameter of_substring_base : int → string → int → int → t.
Definition succ : t → t := fun z ⇒ Z.add z 1.
Definition pred : t → t := fun z ⇒ Z.sub z 1.
Definition abs : t → t := Z.abs.
Definition neg (a : t) : t := -a.
Definition add : t → t → t := Z.add.
Definition sub : t → t → t := Z.sub.
Definition mul : t → t → t := Z.mul.
Definition div : t → t → t := Z.quot.
Definition rem : t → t → t := Z.rem.
Definition div_rem (a b : t) : t × t :=
(Z.quot a b, Z.rem a b).
Parameter cdiv : t → t → t.
Parameter fdiv : t → t → t.
Definition ediv_rem (a b : t) : t × t :=
if b =? 0 then
Pervasives.raise (Build_extensible "Division_by_zero" unit tt)
else
(Zeuclid.ZEuclid.div a b, Zeuclid.ZEuclid.modulo a b).
Definition ediv (a b : t) : t :=
fst (ediv_rem a b).
Definition erem (a b : t) : t :=
snd (ediv_rem a b).
Parameter divexact : t → t → t.
Parameter divisible : t → t → bool.
Parameter congruent : t → t → t → bool.
Definition logand : t → t → t :=
Z.land.
Definition logor : t → t → t :=
Z.lor.
Definition logxor : t → t → t :=
Z.lxor.
Definition lognot : t → t :=
Z.lnot.
Definition shift_left : t → int → t :=
Z.shiftl.
Definition shift_right : t → int → t := Z.shiftr.
Parameter shift_right_trunc : t → int → t.
Parameter numbits : t → int.
Parameter trailing_zeros : t → int.
Definition testbit : t → int → bool :=
Z.testbit.
Parameter popcount : t → int.
Parameter hamdist : t → t → int.
Definition to_int (z : t) : int :=
if andb (Pervasives.min_int <=? z) (z <=? Pervasives.max_int) then
z
else
Pervasives.raise (Build_extensible "Overflow" unit tt).
Definition to_int32 (z : t) : int32 :=
if andb (Int32.min_int <=? z) (z <=? Int32.max_int) then
z
else
Pervasives.raise (Build_extensible "Overflow" unit tt).
Definition to_int64 (z : t) : int64 :=
if andb (Int64.min_int <=? z) (z <=? Int64.max_int) then
z
else
Pervasives.raise (Build_extensible "Overflow" unit tt).
Parameter to_string : t → string.
Parameter format : string → t → string.
Definition fits_int (z : t) : bool :=
(Pervasives.min_int <=? z) && (z <=? Pervasives.max_int).
Definition fits_int32 (z : t) : bool :=
(Int32.min_int <=? z) && (z <=? Int32.max_int).
Definition fits_int64 (z : t) : bool :=
(Int64.min_int <=? z) && (z <=? Int64.max_int).
Parameter pp_print : Format.formatter → t → unit.
Definition compare (a b : t) : int :=
if a <? b then
-1
else if a =? b then
0
else
1.
Definition equal : t → t → bool := Z.eqb.
Definition leq : t → t → bool := Z.leb.
Definition geq : t → t → bool := Z.geb.
Definition lt : t → t → bool := Z.ltb.
Definition gt : t → t → bool := Z.gtb.
Parameter sign : t → int.
Definition min : t → t → t := Z.min.
Definition max : t → t → t := Z.max.
Definition is_even : t → bool := Z.even.
Definition is_odd : t → bool := Z.odd.
Parameter pow : t → int → t.
Parameter sqrt : t → t.
Parameter sqrt_rem : t → t × t.
Parameter root_value : t → int → t.
Parameter rootrem : t → int → t × t.
Parameter perfect_power : t → bool.
Parameter perfect_square : t → bool.
Parameter log2 : t → int.
Parameter log2up : t → int.
Parameter size_value : t → int.
Parameter extract : t → int → int → t.
Parameter signed_extract : t → int → int → t.
Parameter to_bits : t → string.
Parameter of_bits : string → t.
Module Notations.
Infix "+Z" := add (at level 50, left associativity).
Infix "-Z" := sub (at level 50, left associativity).
Infix "*Z" := mul (at level 40, left associativity).
Infix "/Z" := div (at level 40, left associativity).
End Notations.
Global Hint Unfold
zero
one
minus_one
of_int
of_int32
of_int64
succ
pred
abs
neg
add
sub
mul
div
rem
div_rem
compare
equal
leq
geq
lt
gt
min
max
: tezos_z.