Commit 0bef17d9 authored by François Bobot's avatar François Bobot
Browse files

Replace Pervasives by Stdlib in extraction

parent 2ee10bbb
......@@ -25,9 +25,9 @@ Extract Inlined Constant sumbool_of_bool => "Farith_Big.identity".
Require Import Arith Even Div2 EqNat Euclid.
Require Import ExtrOcamlBasic.
Extract Inlined Constant Datatypes.negb => "Pervasives.not".
Extract Inlined Constant Datatypes.fst => "Pervasives.fst".
Extract Inlined Constant Datatypes.snd => "Pervasives.snd".
Extract Inlined Constant Datatypes.negb => "Stdlib.not".
Extract Inlined Constant Datatypes.fst => "Stdlib.fst".
Extract Inlined Constant Datatypes.snd => "Stdlib.snd".
(** NB: The extracted code should be linked with [nums.cm(x)a]
......
......@@ -53,10 +53,10 @@ let is_nan _ _ = function
Farith_Big.big_int -> Farith_Big.big_int -> binary_float -> binary_float **)
let coq_Bopp _ _ x = match x with
| 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 -> x
| 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 -> binary_float -> binary_float **)
......@@ -94,7 +94,7 @@ let coq_Bleb prec emax f1 f2 =
let choice_mode m sx mx lx =
match m with
| Farith_Big.NE -> cond_incr (round_N (Pervasives.not (Z.even mx)) lx) mx
| Farith_Big.NE -> cond_incr (round_N (Stdlib.not (Z.even 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
......@@ -106,7 +106,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 :
......@@ -207,8 +207,8 @@ let binary_normalize prec emax mode0 m e szero =
Farith_Big.big_int **)
let coq_Fplus_naive sx mx ex sy my ey ez =
Farith_Big.add (cond_Zopp sx (Pervasives.fst (shl_align mx ex ez)))
(cond_Zopp sy (Pervasives.fst (shl_align my ey ez)))
Farith_Big.add (cond_Zopp sx (Stdlib.fst (shl_align mx ex ez)))
(cond_Zopp sy (Stdlib.fst (shl_align my ey ez)))
(** val coq_Bplus :
Farith_Big.big_int -> Farith_Big.big_int -> Farith_Big.mode ->
......@@ -253,29 +253,29 @@ let coq_Bminus prec emax m x y =
| B754_zero sx ->
(match y with
| B754_zero sy ->
if eqb sx (Pervasives.not sy)
if eqb sx (Stdlib.not sy)
then x
else (match m with
| Farith_Big.DN -> B754_zero true
| _ -> B754_zero false)
| B754_infinity sy -> B754_infinity (Pervasives.not sy)
| B754_infinity sy -> B754_infinity (Stdlib.not sy)
| B754_nan -> B754_nan
| B754_finite (sy, my, ey) -> B754_finite ((Pervasives.not sy), my, ey))
| B754_finite (sy, my, ey) -> B754_finite ((Stdlib.not sy), my, ey))
| B754_infinity sx ->
(match y with
| B754_infinity sy -> if eqb sx (Pervasives.not sy) then x else B754_nan
| B754_infinity sy -> if eqb sx (Stdlib.not sy) then x else B754_nan
| B754_nan -> B754_nan
| _ -> x)
| B754_nan -> B754_nan
| B754_finite (sx, mx, ex) ->
(match y with
| B754_zero _ -> x
| B754_infinity sy -> B754_infinity (Pervasives.not sy)
| B754_infinity sy -> B754_infinity (Stdlib.not sy)
| B754_nan -> B754_nan
| B754_finite (sy, my, ey) ->
let ez = Farith_Big.min ex ey in
binary_normalize prec emax m
(coq_Fplus_naive sx mx ex (Pervasives.not sy) my ey ez) ez
(coq_Fplus_naive sx mx ex (Stdlib.not sy) my ey ez) ez
(match m with
| Farith_Big.DN -> true
| _ -> false))
......
......@@ -32,8 +32,7 @@ let is_singleton prec emax = function
| Intv (a, b, n) ->
if (&&)
((&&) (coq_Beqb prec emax a b)
(Pervasives.not (coq_Beqb prec emax a (B754_zero false))))
(Pervasives.not n)
(Stdlib.not (coq_Beqb prec emax a (B754_zero false)))) (Stdlib.not n)
then Some a
else None
......
......@@ -42,10 +42,10 @@ let coq_Fsucc prec emax x = match x with
Farith_Big.big_int -> Farith_Big.big_int -> float -> float **)
let coq_Fneg _ _ = function
| B754_zero s -> B754_zero (Pervasives.not s)
| B754_infinity s -> B754_infinity (Pervasives.not s)
| B754_zero s -> B754_zero (Stdlib.not s)
| B754_infinity s -> B754_infinity (Stdlib.not s)
| B754_nan -> B754_nan
| B754_finite (s, m, e) -> B754_finite ((Pervasives.not s), m, e)
| B754_finite (s, m, e) -> B754_finite ((Stdlib.not s), m, e)
(** val coq_Fpred :
Farith_Big.big_int -> Farith_Big.big_int -> float -> float **)
......
......@@ -16,7 +16,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 **)
......
# This file is generated by dune, edit dune-project instead
opam-version: "2.0"
synopsis: "formaly verified floating-points valuations based on Flocq"
maintainer: ["François Bobot"]
authors: ["François Bobot" "Loïc Correnson" "Arthur Correnson"]
depends: [
"dune" {>= "3.0"}
"zarith"
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment