Skip to main content

🍃 Pervasives.v

Environment

See proofs, Gitlab , OCaml

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 znormalize_int (Z.sub 0 z).

Definition op_tildeplus : int int := fun zz.

Definition succ : int int := fun znormalize_int (Z.add z 1).

Definition pred : int int := fun znormalize_int (Z.sub z 1).

Definition op_plus : int int int :=
  fun a bnormalize_int (Z.add a b).

Definition op_minus : int int int :=
  fun a bnormalize_int (Z.sub a b).

Definition op_star : int int int :=
  fun a bnormalize_int (Z.mul a b).

Definition op_div : int int int :=
  fun a bnormalize_int (Z.div a b).

Definition _mod : int int int :=
  fun a bnormalize_int (Z.rem a b).

Definition abs : int int :=
  fun anormalize_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.