Replace by Pervasives by stdlib

F.ml

@@ -317,7 +317,7 @@ let of_float u =
 let to_float ?(mode=NE) u =
   if u == zero then 0.0 else
     let (a,n) = rounding NE b64 m64 u in
-    Pervasives.ldexp (Z.to_float a) n
+    Stdlib.ldexp (Z.to_float a) n
 
 (* -------------------------------------------------------------------------- *)
 (* --- String Conversion                                                  --- *)

extracted/farith_F_aux.ml

@@ -213,8 +213,8 @@ module Aux =
   (** val default_nan : 'a1 fconf -> binary_float **)
 
   let default_nan conf0 =
-    B754_nan ((Pervasives.fst (default_nan_pl conf0)),
-      (Pervasives.snd (default_nan_pl conf0)))
+    B754_nan ((Stdlib.fst (default_nan_pl conf0)),
+      (Stdlib.snd (default_nan_pl conf0)))
 
   (** val of_q : 'a1 fconf -> Farith_Big.mode -> Q.t -> binary_float **)
 
@@ -713,7 +713,7 @@ module D =
   let conv _ conf2 mode f =
     match Obj.magic f with
     | B754_nan (b, _) ->
-      Obj.magic (B754_nan (b, (Pervasives.snd (Aux.default_nan_pl conf2))))
+      Obj.magic (B754_nan (b, (Stdlib.snd (Aux.default_nan_pl conf2))))
     | B754_finite (sx, mx, ex) ->
       Obj.magic coq_FF2B (cprec conf2.mw) (cemax conf2.ew)
         (binary_round (cprec conf2.mw) (cemax conf2.ew) mode sx mx ex)

extracted/farith_Fappli_IEEE.ml

@@ -61,11 +61,11 @@ let coq_B2FF _ _ = function
     bool * nan_pl) -> binary_float -> binary_float **)
 
 let coq_Bopp _ _ opp_nan = function
-| B754_zero sx -> B754_zero (Pervasives.not sx)
-| B754_infinity sx -> B754_infinity (Pervasives.not sx)
+| B754_zero sx -> B754_zero (Stdlib.not sx)
+| B754_infinity sx -> B754_infinity (Stdlib.not sx)
 | B754_nan (sx, plx) ->
   let (sres, plres) = opp_nan sx plx in B754_nan (sres, plres)
-| B754_finite (sx, mx, ex) -> B754_finite ((Pervasives.not sx), mx, ex)
+| B754_finite (sx, mx, ex) -> B754_finite ((Stdlib.not sx), mx, ex)
 
 (** val coq_Babs :
     Farith_Big.big_int -> Farith_Big.big_int -> (bool -> nan_pl ->
@@ -225,7 +225,7 @@ let shr_fexp prec emax =
 let choice_mode m sx mx lx =
   match m with
   | Farith_Big.NE ->
-    cond_incr (round_N (Pervasives.not (coq_Zeven mx)) lx) mx
+    cond_incr (round_N (Stdlib.not (coq_Zeven mx)) lx) mx
   | Farith_Big.ZR -> mx
   | Farith_Big.DN -> cond_incr (round_sign_DN sx lx) mx
   | Farith_Big.UP -> cond_incr (round_sign_UP sx lx) mx
@@ -237,7 +237,7 @@ let overflow_to_inf m s =
   match m with
   | Farith_Big.ZR -> false
   | Farith_Big.DN -> s
-  | Farith_Big.UP -> Pervasives.not s
+  | Farith_Big.UP -> Stdlib.not s
   | _ -> true
 
 (** val binary_overflow :
@@ -289,22 +289,22 @@ let binary_round_aux prec emax mode sx mx ex lx =
 let coq_Bmult prec emax mult_nan m x y =
   match x with
   | B754_zero sx ->
-    let f = fun pl -> B754_nan ((Pervasives.fst pl), (Pervasives.snd pl)) in
+    let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in
     (match y with
      | B754_zero sy -> B754_zero (xorb sx sy)
      | B754_finite (sy, _, _) -> B754_zero (xorb sx sy)
      | _ -> f (mult_nan x y))
   | B754_infinity sx ->
-    let f = fun pl -> B754_nan ((Pervasives.fst pl), (Pervasives.snd pl)) in
+    let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in
     (match y with
      | B754_infinity sy -> B754_infinity (xorb sx sy)
      | B754_finite (sy, _, _) -> B754_infinity (xorb sx sy)
      | _ -> f (mult_nan x y))
   | B754_nan (_, _) ->
     let pl = mult_nan x y in
-    B754_nan ((Pervasives.fst pl), (Pervasives.snd pl))
+    B754_nan ((Stdlib.fst pl), (Stdlib.snd pl))
   | B754_finite (sx, mx, ex) ->
-    let f = fun pl -> B754_nan ((Pervasives.fst pl), (Pervasives.snd pl)) in
+    let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in
     (match y with
      | B754_zero sy -> B754_zero (xorb sx sy)
      | B754_infinity sy -> B754_infinity (xorb sx sy)
@@ -370,7 +370,7 @@ let binary_normalize prec emax mode m e szero =
 let coq_Bplus prec emax plus_nan m x y =
   match x with
   | B754_zero sx ->
-    let f = fun pl -> B754_nan ((Pervasives.fst pl), (Pervasives.snd pl)) in
+    let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in
     (match y with
      | B754_zero sy ->
        if eqb sx sy
@@ -381,16 +381,16 @@ let coq_Bplus prec emax plus_nan m x y =
      | B754_nan (_, _) -> f (plus_nan x y)
      | _ -> y)
   | B754_infinity sx ->
-    let f = fun pl -> B754_nan ((Pervasives.fst pl), (Pervasives.snd pl)) in
+    let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in
     (match y with
      | B754_infinity sy -> if eqb sx sy then x else f (plus_nan x y)
      | B754_nan (_, _) -> f (plus_nan x y)
      | _ -> x)
   | B754_nan (_, _) ->
     let pl = plus_nan x y in
-    B754_nan ((Pervasives.fst pl), (Pervasives.snd pl))
+    B754_nan ((Stdlib.fst pl), (Stdlib.snd pl))
   | B754_finite (sx, mx, ex) ->
-    let f = fun pl -> B754_nan ((Pervasives.fst pl), (Pervasives.snd pl)) in
+    let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in
     (match y with
      | B754_zero _ -> x
      | B754_infinity _ -> y
@@ -398,8 +398,8 @@ let coq_Bplus prec emax plus_nan m x y =
      | B754_finite (sy, my, ey) ->
        let ez = Farith_Big.min ex ey in
        binary_normalize prec emax m
-         (Farith_Big.add (cond_Zopp sx (Pervasives.fst (shl_align mx ex ez)))
-           (cond_Zopp sy (Pervasives.fst (shl_align my ey ez)))) ez
+         (Farith_Big.add (cond_Zopp sx (Stdlib.fst (shl_align mx ex ez)))
+           (cond_Zopp sy (Stdlib.fst (shl_align my ey ez)))) ez
          (match m with
           | Farith_Big.DN -> true
           | _ -> false))
@@ -444,22 +444,22 @@ let coq_Fdiv_core_binary prec m1 e1 m2 e2 =
 let coq_Bdiv prec emax div_nan m x y =
   match x with
   | B754_zero sx ->
-    let f = fun pl -> B754_nan ((Pervasives.fst pl), (Pervasives.snd pl)) in
+    let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in
     (match y with
      | B754_infinity sy -> B754_zero (xorb sx sy)
      | B754_finite (sy, _, _) -> B754_zero (xorb sx sy)
      | _ -> f (div_nan x y))
   | B754_infinity sx ->
-    let f = fun pl -> B754_nan ((Pervasives.fst pl), (Pervasives.snd pl)) in
+    let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in
     (match y with
      | B754_zero sy -> B754_infinity (xorb sx sy)
      | B754_finite (sy, _, _) -> B754_infinity (xorb sx sy)
      | _ -> f (div_nan x y))
   | B754_nan (_, _) ->
     let pl = div_nan x y in
-    B754_nan ((Pervasives.fst pl), (Pervasives.snd pl))
+    B754_nan ((Stdlib.fst pl), (Stdlib.snd pl))
   | B754_finite (sx, mx, ex) ->
-    let f = fun pl -> B754_nan ((Pervasives.fst pl), (Pervasives.snd pl)) in
+    let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in
     (match y with
      | B754_zero sy -> B754_infinity (xorb sx sy)
      | B754_infinity sy -> B754_zero (xorb sx sy)
@@ -533,7 +533,7 @@ let coq_Fsqrt_core_binary prec m e =
     bool * nan_pl) -> Farith_Big.mode -> binary_float -> binary_float **)
 
 let coq_Bsqrt prec emax sqrt_nan m x =
-  let f = fun pl -> B754_nan ((Pervasives.fst pl), (Pervasives.snd pl)) in
+  let f = fun pl -> B754_nan ((Stdlib.fst pl), (Stdlib.snd pl)) in
   (match x with
    | B754_zero _ -> x
    | B754_infinity b -> if b then f (sqrt_nan x) else x

extracted/farith_Fcalc_round.ml

@@ -35,7 +35,7 @@ let round_sign_DN s = function
 
 let round_sign_UP s = function
 | Coq_loc_Exact -> false
-| Coq_loc_Inexact _ -> Pervasives.not s
+| Coq_loc_Inexact _ -> Stdlib.not s
 
 (** val round_N : bool -> location -> bool **)
 

farith_Big.ml

@@ -185,13 +185,13 @@ let div_floor = Z.fdiv
 let div2_floor n = Z.shift_right n 1
 let mod_floor a b =
   let r = Z.rem a b in
-  if (Pervasives.(lxor) (Z.sign a) (Z.sign b) >= 0) || Z.equal r Z.zero
+  if (Stdlib.(lxor) (Z.sign a) (Z.sign b) >= 0) || Z.equal r Z.zero
   then r
   else Z.add b r
 
 let div_mod_floor a b =
   let p,r as pr = Z.div_rem a b in
-  if ((Pervasives.(lxor) (Z.sign a) (Z.sign b)) >= 0) || Z.equal r Z.zero
+  if ((Stdlib.(lxor) (Z.sign a) (Z.sign b)) >= 0) || Z.equal r Z.zero
   then pr
   else Z.pred p, Z.add b r
 

tests/subnormal.ml

 
-let eps n = Pervasives.ldexp 1.0 n
+let eps n = Stdlib.ldexp 1.0 n
 
 let pp_class fmt u =
   Format.pp_print_string fmt
@@ -26,8 +26,8 @@ let test_to_float n =
     let f = F.power2 n in
     let v = F.to_float f in
     Format.printf "to-float %a = %f (%a)@." F.pp f v pp_class v ;
-    let fu,eu = Pervasives.frexp u in
-    let fv,ev = Pervasives.frexp v in
+    let fu,eu = Stdlib.frexp u in
+    let fv,ev = Stdlib.frexp v in
     Format.printf "   expected = %fp%d@\n" fu eu ;
     Format.printf "   obtained = %fp%d@." fv ev ;
   end