Skip to main content

🍃 Z.v

Environment

See proofs, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Proto_alpha.Environment.Format.
Require Proto_alpha.Environment.Int32.
Require Proto_alpha.Environment.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 zZ.add z 1.

Definition pred : t t := fun zZ.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.div.

Definition rem : t t t := Z.rem.

Definition div_rem (a b : t) : t × t :=
  (div a b, rem a b).

Parameter cdiv : t t t.

Parameter fdiv : t t t.

Parameter ediv_rem : t t t × t.

Parameter ediv : t t t.

Parameter erem : t t t.

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.

Parameter shift_right : t int t.

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.

(* Many of these conversion functions can raise exceptions in case of
   overflow. TODO: find a solution. *)

Definition to_int : t int := Pervasives.normalize_int.

Definition to_int32 : t int32 := Pervasives.normalize_int32.

Definition to_int64 : t int64 := Pervasives.normalize_int64.

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
  to_int
  to_int32
  to_int64
  : tezos_z.