Skip to main content

🍃 Int64.v

Environment

See proofs, Gitlab , OCaml

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

Require TezosOfOCaml.Proto_alpha.Environment.Pervasives.

Definition t : Set := Z.

Definition zero : t := 0.

Definition one : t := 1.

Definition minus_one : t := -1.

Definition neg (a : t) : t := Pervasives.normalize_int64 (-a).

Definition add (a : t) (b : t) : t := Pervasives.normalize_int64 (Z.add a b).

Definition sub (a : t) (b : t) : t := Pervasives.normalize_int64 (Z.sub a b).

Definition mul (a : t) (b : t) : t := Pervasives.normalize_int64 (Z.mul a b).

Definition div (a : t) (b : t) : t := Pervasives.normalize_int64 (Z.div a b).

Definition rem (a : t) (b : t) : t := Pervasives.normalize_int64 (Z.rem a b).

Definition succ (a : t) : t := add a 1.

Definition pred (a : t) : t := sub a 1.

Definition abs (a : t) : t := Pervasives.normalize_int64 (Z.abs a).

Definition max_int : t := 9223372036854775807.

Definition min_int : t := -9223372036854775808.

Parameter logand : int64 int64 int64.

Parameter logor : int64 int64 int64.

Parameter logxor : int64 int64 int64.

Parameter lognot : int64 int64.

Parameter shift_left : int64 int int64.

Parameter shift_right : int64 int int64.

Parameter shift_right_logical : int64 int int64.

Definition of_int (a : int) : t := a.

Definition to_int (a : t) : int := Pervasives.normalize_int a.

Definition of_int32 (a : int32) : t := a.

Definition to_int32 (a : t) : int32 := Pervasives.normalize_int32 a.

Parameter of_string_opt : string option int64.

Parameter to_string : int64 string.

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.

Module Notations.
  Infix "+i64" := add (at level 50, left associativity).
  Infix "-i64" := sub (at level 50, left associativity).
  Infix "*i64" := mul (at level 40, left associativity).
  Infix "/i64" := div (at level 40, left associativity).
End Notations.

Global Hint Unfold
  zero
  one
  minus_one
  neg
  add
  sub
  mul
  div
  rem
  succ
  pred
  abs
  max_int
  min_int
  of_int
  to_int
  of_int32
  to_int32
  compare
  equal
  : tezos_z.