Skip to main content

🍃 Int32.v

Environment

Gitlab

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

Require TezosOfOCaml.Environment.Structs.V0.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_int32 (-a).

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

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

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

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

Definition rem (a : t) (b : t) : t := Pervasives.normalize_int32 (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_int32 (Z.abs a).

Definition max_int := 2147483647.

Definition min_int := -2147483648.

Parameter logand : int32 int32 int32.

Parameter logor : int32 int32 int32.

Parameter logxor : int32 int32 int32.

Parameter lognot : int32 int32.

Parameter shift_left : int32 int int32.

Parameter shift_right : int32 int int32.

Parameter shift_right_logical : int32 int int32.

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

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

Parameter of_string_opt : string option t.

Parameter to_string : t 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 "+i32" := add (at level 50, left associativity).
  Infix "-i32" := sub (at level 50, left associativity).
  Infix "*i32" := mul (at level 40, left associativity).
  Infix "/i32" := 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
  compare
  equal
  : tezos_z.