🍃 Pervasives.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Definition two_pow_31 : Z := 2147483648.
Definition two_pow_32 : Z := 4294967296.
Definition two_pow_62 : Z := 4611686018427387904.
Definition two_pow_63 : Z := 9223372036854775808.
Definition two_pow_64 : Z := 18446744073709551616.
Definition normalize_int (n : Z) : int :=
Z.modulo (n + two_pow_62) two_pow_63 - two_pow_62.
Definition normalize_int32 (n : Z) : int32 :=
Z.modulo (n + two_pow_31) two_pow_32 - two_pow_31.
Definition normalize_int64 (n : Z) : int64 :=
Z.modulo (n + two_pow_63) two_pow_64 - two_pow_63.
Parameter raise : ∀ {a : Set}, extensible_type → a.
Parameter raise_notrace : ∀ {a : Set}, extensible_type → a.
Parameter invalid_arg : ∀ {a : Set}, string → a.
Parameter failwith : ∀ {a : Set}, string → a.
Definition not : bool → bool := negb.
Definition op_andand : bool → bool → bool := andb.
Definition op_pipepipe : bool → bool → bool := orb.
Parameter __LOC__ : string.
Parameter __FILE__ : string.
Parameter __LINE__ : int.
Parameter __MODULE__ : string.
Parameter __POS__ : string × int × int × int.
Parameter __LOC_OF__ : ∀ {a : Set}, a → string × a.
Parameter __LINE_OF__ : ∀ {a : Set}, a → int × a.
Parameter __POS_OF__ : ∀ {a : Set}, a → (string × int × int × int) × a.
Definition op_pipegt : ∀ {a b : Set}, a → (a → b) → b :=
fun _ _ x f ⇒
f x.
Definition op_atat : ∀ {a b : Set}, (a → b) → a → b :=
fun _ _ f x ⇒
f x.
Definition op_tildeminus : int → int := fun z ⇒ normalize_int (Z.sub 0 z).
Definition op_tildeplus : int → int := fun z ⇒ z.
Definition succ : int → int := fun z ⇒ normalize_int (Z.add z 1).
Definition pred : int → int := fun z ⇒ normalize_int (Z.sub z 1).
Definition op_plus : int → int → int :=
fun a b ⇒ normalize_int (Z.add a b).
Definition op_minus : int → int → int :=
fun a b ⇒ normalize_int (Z.sub a b).
Definition op_star : int → int → int :=
fun a b ⇒ normalize_int (Z.mul a b).
Definition op_div : int → int → int :=
fun a b ⇒ normalize_int (Z.quot a b).
Definition _mod : int → int → int :=
fun a b ⇒ normalize_int (Z.rem a b).
Definition abs : int → int :=
fun a ⇒ normalize_int (Z.abs a).
Definition max_int : int := 4611686018427387903.
Definition min_int : int := -4611686018427387904.
Definition land : int → int → int := Z.land.
Definition lor : int → int → int := Z.lor.
Definition lxor : int → int → int := Z.lxor.
Definition lnot : int → int := Z.lnot.
Definition lsl (n : int) (s : int) : int :=
normalize_int (land (Z.shiftl n s) (two_pow_63 - 1)).
Definition lsr (n : int) (s : int) : int :=
if n >=? 0 then
Z.shiftr n s
else
normalize_int (Z.shiftr (Z.modulo n two_pow_63) s).
Definition asr : int → int → int := Z.shiftr.
Definition op_caret : string → string → string := String.append.
Definition int_of_char : ascii → int :=
fun c ⇒
normalize_int (Z.of_N (Ascii.N_of_ascii c)).
Definition char_of_int : int → ascii :=
fun z ⇒
Ascii.ascii_of_N (Z.to_N z).
Definition ignore : ∀ {a : Set}, a → unit :=
fun _ _ ⇒
tt.
Parameter string_of_bool : bool → string.
Parameter bool_of_string_opt : string → option bool.
Parameter string_of_int : int → string.
Parameter int_of_string_opt : string → option int.
Definition fst : ∀ {a b : Set}, a × b → a :=
fun _ _ ⇒
fst.
Definition snd : ∀ {a b : Set}, a × b → b :=
fun _ _ ⇒
snd.
Definition op_at : ∀ {a : Set}, list a → list a → list a :=
fun _ ⇒
List.append.
Module ref.
Record record {a : Set} : Set := Build {
contents : a }.
Arguments record : clear implicits.
Definition with_contents {t_a} contents (r : record t_a) :=
Build t_a contents.
End ref.
Definition ref := ref.record.
Parameter ref_value : ∀ {a : Set}, a → ref a.
Parameter op_exclamation : ∀ {a : Set}, ref a → a.
Parameter op_coloneq : ∀ {a : Set}, ref a → a → unit.
Parameter incr : ref int → unit.
Parameter decr : ref int → unit.
Inductive result (a b : Set) : Set :=
| Ok : a → result a b
| Error : b → result a b.
Arguments Ok {_ _}.
Arguments Error {_ _}.
Definition format6 (a b c d e f : Set) : Set :=
CamlinternalFormatBasics.format6 a b c d e f.
Definition format4 (a b c d : Set) : Set := format6 a b c c c d.
Definition format (a b c : Set) : Set := format4 a b c c.
Parameter string_of_format : ∀ {a b c d e f : Set},
format6 a b c d e f → string.
Parameter format_of_string : ∀ {a b c d e f : Set},
format6 a b c d e f → format6 a b c d e f.
Parameter op_caretcaret : ∀ {a b c d e f g h : Set},
format6 a b c d e f → format6 f b c e g h → format6 a b c d g h.
Module Notations.
Infix "&&" := op_andand (at level 40, left associativity).
Infix "||" := op_pipepipe (at level 50, left associativity).
Infix "+i" := op_plus (at level 50, left associativity).
Infix "-i" := op_minus (at level 50, left associativity).
Infix "*i" := op_star (at level 40, left associativity).
Infix "/i" := op_div (at level 40, left associativity).
End Notations.
Global Hint Unfold
two_pow_31
two_pow_32
two_pow_62
two_pow_63
two_pow_64
op_tildeminus
op_tildeplus
succ
pred
op_plus
op_minus
op_star
op_div
_mod
abs
max_int
min_int
land
lor
lxor
lnot
lsl
lsr
asr
: tezos_z.
Require Import CoqOfOCaml.Settings.
Definition two_pow_31 : Z := 2147483648.
Definition two_pow_32 : Z := 4294967296.
Definition two_pow_62 : Z := 4611686018427387904.
Definition two_pow_63 : Z := 9223372036854775808.
Definition two_pow_64 : Z := 18446744073709551616.
Definition normalize_int (n : Z) : int :=
Z.modulo (n + two_pow_62) two_pow_63 - two_pow_62.
Definition normalize_int32 (n : Z) : int32 :=
Z.modulo (n + two_pow_31) two_pow_32 - two_pow_31.
Definition normalize_int64 (n : Z) : int64 :=
Z.modulo (n + two_pow_63) two_pow_64 - two_pow_63.
Parameter raise : ∀ {a : Set}, extensible_type → a.
Parameter raise_notrace : ∀ {a : Set}, extensible_type → a.
Parameter invalid_arg : ∀ {a : Set}, string → a.
Parameter failwith : ∀ {a : Set}, string → a.
Definition not : bool → bool := negb.
Definition op_andand : bool → bool → bool := andb.
Definition op_pipepipe : bool → bool → bool := orb.
Parameter __LOC__ : string.
Parameter __FILE__ : string.
Parameter __LINE__ : int.
Parameter __MODULE__ : string.
Parameter __POS__ : string × int × int × int.
Parameter __LOC_OF__ : ∀ {a : Set}, a → string × a.
Parameter __LINE_OF__ : ∀ {a : Set}, a → int × a.
Parameter __POS_OF__ : ∀ {a : Set}, a → (string × int × int × int) × a.
Definition op_pipegt : ∀ {a b : Set}, a → (a → b) → b :=
fun _ _ x f ⇒
f x.
Definition op_atat : ∀ {a b : Set}, (a → b) → a → b :=
fun _ _ f x ⇒
f x.
Definition op_tildeminus : int → int := fun z ⇒ normalize_int (Z.sub 0 z).
Definition op_tildeplus : int → int := fun z ⇒ z.
Definition succ : int → int := fun z ⇒ normalize_int (Z.add z 1).
Definition pred : int → int := fun z ⇒ normalize_int (Z.sub z 1).
Definition op_plus : int → int → int :=
fun a b ⇒ normalize_int (Z.add a b).
Definition op_minus : int → int → int :=
fun a b ⇒ normalize_int (Z.sub a b).
Definition op_star : int → int → int :=
fun a b ⇒ normalize_int (Z.mul a b).
Definition op_div : int → int → int :=
fun a b ⇒ normalize_int (Z.quot a b).
Definition _mod : int → int → int :=
fun a b ⇒ normalize_int (Z.rem a b).
Definition abs : int → int :=
fun a ⇒ normalize_int (Z.abs a).
Definition max_int : int := 4611686018427387903.
Definition min_int : int := -4611686018427387904.
Definition land : int → int → int := Z.land.
Definition lor : int → int → int := Z.lor.
Definition lxor : int → int → int := Z.lxor.
Definition lnot : int → int := Z.lnot.
Definition lsl (n : int) (s : int) : int :=
normalize_int (land (Z.shiftl n s) (two_pow_63 - 1)).
Definition lsr (n : int) (s : int) : int :=
if n >=? 0 then
Z.shiftr n s
else
normalize_int (Z.shiftr (Z.modulo n two_pow_63) s).
Definition asr : int → int → int := Z.shiftr.
Definition op_caret : string → string → string := String.append.
Definition int_of_char : ascii → int :=
fun c ⇒
normalize_int (Z.of_N (Ascii.N_of_ascii c)).
Definition char_of_int : int → ascii :=
fun z ⇒
Ascii.ascii_of_N (Z.to_N z).
Definition ignore : ∀ {a : Set}, a → unit :=
fun _ _ ⇒
tt.
Parameter string_of_bool : bool → string.
Parameter bool_of_string_opt : string → option bool.
Parameter string_of_int : int → string.
Parameter int_of_string_opt : string → option int.
Definition fst : ∀ {a b : Set}, a × b → a :=
fun _ _ ⇒
fst.
Definition snd : ∀ {a b : Set}, a × b → b :=
fun _ _ ⇒
snd.
Definition op_at : ∀ {a : Set}, list a → list a → list a :=
fun _ ⇒
List.append.
Module ref.
Record record {a : Set} : Set := Build {
contents : a }.
Arguments record : clear implicits.
Definition with_contents {t_a} contents (r : record t_a) :=
Build t_a contents.
End ref.
Definition ref := ref.record.
Parameter ref_value : ∀ {a : Set}, a → ref a.
Parameter op_exclamation : ∀ {a : Set}, ref a → a.
Parameter op_coloneq : ∀ {a : Set}, ref a → a → unit.
Parameter incr : ref int → unit.
Parameter decr : ref int → unit.
Inductive result (a b : Set) : Set :=
| Ok : a → result a b
| Error : b → result a b.
Arguments Ok {_ _}.
Arguments Error {_ _}.
Definition format6 (a b c d e f : Set) : Set :=
CamlinternalFormatBasics.format6 a b c d e f.
Definition format4 (a b c d : Set) : Set := format6 a b c c c d.
Definition format (a b c : Set) : Set := format4 a b c c.
Parameter string_of_format : ∀ {a b c d e f : Set},
format6 a b c d e f → string.
Parameter format_of_string : ∀ {a b c d e f : Set},
format6 a b c d e f → format6 a b c d e f.
Parameter op_caretcaret : ∀ {a b c d e f g h : Set},
format6 a b c d e f → format6 f b c e g h → format6 a b c d g h.
Module Notations.
Infix "&&" := op_andand (at level 40, left associativity).
Infix "||" := op_pipepipe (at level 50, left associativity).
Infix "+i" := op_plus (at level 50, left associativity).
Infix "-i" := op_minus (at level 50, left associativity).
Infix "*i" := op_star (at level 40, left associativity).
Infix "/i" := op_div (at level 40, left associativity).
End Notations.
Global Hint Unfold
two_pow_31
two_pow_32
two_pow_62
two_pow_63
two_pow_64
op_tildeminus
op_tildeplus
succ
pred
op_plus
op_minus
op_star
op_div
_mod
abs
max_int
min_int
land
lor
lxor
lnot
lsl
lsr
asr
: tezos_z.