diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index 81842f01a2eb694506b55e6640baba76d03a7870..a62ca61f74f49ede1bd466217377af4d37ba2a55 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -45,9 +45,8 @@ let ftau = function
| Float32 -> t32
| Float64 -> t64
-let pp_suffix fmt = function
- | Float32 -> Format.pp_print_string fmt "f32"
- | Float64 -> Format.pp_print_string fmt "f64"
+let ft_suffix = function Float32 -> "f32" | Float64 -> "f64"
+let pp_suffix fmt ft = Format.pp_print_string fmt (ft_suffix ft)
let link phi = Lang.infoprover (Qed.Engine.F_call phi)
@@ -135,15 +134,16 @@ let fmake ulp value = match ulp with
| Float64 -> F.e_fun fq64 [F.e_float value]
let qmake ulp q = fmake ulp (Transitioning.Q.to_float q)
-let mantissa = "\\([-+]?[0-9]*\\)"
-let comma = "\\(.\\(\\(0*[1-9]\\)*\\)0*\\)?"
-let exponent = "\\([eE]\\([-+]?[0-9]*\\)\\)?"
-let suffix = "\\([flFL]\\)?"
-let real = Str.regexp (mantissa ^ comma ^ exponent ^ suffix ^ "$")
+let re_mantissa = "\\([-+]?[0-9]*\\)"
+let re_comma = "\\(.\\(\\(0*[1-9]\\)*\\)0*\\)?"
+let re_exponent = "\\([eE]\\([-+]?[0-9]*\\)\\)?"
+let re_suffix = "\\([flFL]\\)?"
+let re_real =
+ Str.regexp (re_mantissa ^ re_comma ^ re_exponent ^ re_suffix ^ "$")
let parse_literal ~model v r =
try
- if Str.string_match real r 0 then
+ if Str.string_match re_real r 0 then
let has_suffix =
try ignore (Str.matched_group 7 r) ; true
with Not_found -> false in
@@ -217,19 +217,52 @@ let make_pred_float name op ft =
Lang.F.set_builtin phi (compute op ft) ;
REGISTRY.define phi (op,ft) ; phi
-let register = Ctypes.f_memo
+let f_memo = Ctypes.f_memo
-let real_of_flt = register (make_fun_float ~result:Logic.Real "of" REAL)
-let flt_of_real = register (make_fun_float "to" ROUND)
-let flt_add = register (make_fun_float "add" ADD)
-let flt_mul = register (make_fun_float "mul" MUL)
-let flt_div = register (make_fun_float "div" DIV)
-let flt_neg = register (make_fun_float "neg" NEG)
+let real_of_flt = f_memo (make_fun_float ~result:Logic.Real "of" REAL)
+let flt_of_real = f_memo (make_fun_float "to" ROUND)
+let flt_add = f_memo (make_fun_float "add" ADD)
+let flt_mul = f_memo (make_fun_float "mul" MUL)
+let flt_div = f_memo (make_fun_float "div" DIV)
+let flt_neg = f_memo (make_fun_float "neg" NEG)
-let flt_lt = register (make_pred_float "lt" LT)
-let flt_eq = register (make_pred_float "eq" EQ)
-let flt_le = register (make_pred_float "le" LE)
-let flt_neq = register (make_pred_float "ne" NE)
+let flt_lt = f_memo (make_pred_float "lt" LT)
+let flt_eq = f_memo (make_pred_float "eq" EQ)
+let flt_le = f_memo (make_pred_float "le" LE)
+let flt_neq = f_memo (make_pred_float "ne" NE)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Builtins --- *)
+(* -------------------------------------------------------------------------- *)
+
+let register_builtin_comparison suffix ft =
+ begin
+ let open Qed.Logic in
+ let params = [Sdata;Sdata] in
+ let sort = Sprop in
+ let gt = generated_f ~params ~sort "\\gt_%s" suffix in
+ let ge = generated_f ~params ~sort "\\ge_%s" suffix in
+ let open LogicBuiltins in
+ let signature = [F ft;F ft] in
+ add_builtin ("\\eq_" ^ suffix) signature (flt_eq ft) ;
+ add_builtin ("\\ne_" ^ suffix) signature (flt_neq ft) ;
+ add_builtin ("\\lt_" ^ suffix) signature (flt_lt ft) ;
+ add_builtin ("\\le_" ^ suffix) signature (flt_le ft) ;
+ add_builtin ("\\gt_" ^ suffix) signature gt ;
+ add_builtin ("\\ge_" ^ suffix) signature ge ;
+ Context.register
+ begin fun () ->
+ let compute phi x y = e_fun phi [y;x] in
+ Lang.F.set_builtin_2 gt (compute (flt_lt ft)) ;
+ Lang.F.set_builtin_2 ge (compute (flt_le ft)) ;
+ end
+ end
+
+let () =
+ begin
+ register_builtin_comparison "float" Float32 ;
+ register_builtin_comparison "double" Float64 ;
+ end
(* -------------------------------------------------------------------------- *)
(* --- Models --- *)
@@ -238,13 +271,13 @@ let flt_neq = register (make_pred_float "ne" NE)
let () =
begin
let open LogicBuiltins in
- let register ft =
+ let register_builtin ft =
add_builtin "\\model" [F ft] (f_model ft) ;
add_builtin "\\delta" [F ft] (f_delta ft) ;
add_builtin "\\epsilon" [F ft] (f_epsilon ft) ;
in
- register Float32 ;
- register Float64 ;
+ register_builtin Float32 ;
+ register_builtin Float64 ;
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Cmath.ml b/src/plugins/wp/Cmath.ml
index cf021942c218bebc364ae593e962dfa20d0b2d4e..73f81d6118262bce0d8ca3dd8dc02befcbab9597 100644
--- a/src/plugins/wp/Cmath.ml
+++ b/src/plugins/wp/Cmath.ml
@@ -82,41 +82,6 @@ let builtin_truncate f e =
end
| Fun( f , [e] ) when f == f_real_of_int -> e
| _ -> raise Not_found
-(* -------------------------------------------------------------------------- *)
-(* --- Float comparisons --- *)
-(* -------------------------------------------------------------------------- *)
-
-let f_lt_float = f_builtin ~library:"cfloat" ~result:Prop "\\lt_float"
-let f_gt_float =
- generated_f ~params:[Sdata; Sdata] ~sort:Sprop "\\gt_float"
-let () =
- LogicBuiltins.(
- add_builtin "\\gt_float" [F Ctypes.Float32; F Ctypes.Float32] f_gt_float)
-let builtin_gt_float x y = e_fun f_lt_float [y; x]
-
-let f_le_float = f_builtin ~library:"cfloat" ~result:Prop "\\le_float"
-let f_ge_float =
- generated_f ~params:[Sdata; Sdata] ~sort:Sprop "\\ge_float"
-let () =
- LogicBuiltins.(
- add_builtin "\\ge_float" [F Ctypes.Float32; F Ctypes.Float32] f_ge_float)
-let builtin_ge_float x y = e_fun f_le_float [y; x]
-
-let f_lt_double = f_builtin ~library:"cfloat" ~result:Prop "\\lt_double"
-let f_gt_double =
- generated_f ~params:[Sdata; Sdata] ~sort:Sprop "\\gt_double"
-let () =
- LogicBuiltins.(
- add_builtin "\\gt_double" [F Ctypes.Float64; F Ctypes.Float64] f_gt_double)
-let builtin_gt_double x y = e_fun f_lt_double [y; x]
-
-let f_le_double = f_builtin ~library:"cfloat" ~result:Prop "\\le_double"
-let f_ge_double =
- generated_f ~params:[Sdata; Sdata] ~sort:Sprop "\\ge_double"
-let () =
- LogicBuiltins.(
- add_builtin "\\ge_double" [F Ctypes.Float64; F Ctypes.Float64] f_ge_double)
-let builtin_ge_double x y = e_fun f_le_double [y; x]
(* -------------------------------------------------------------------------- *)
(* --- Conversions --- *)
@@ -382,11 +347,6 @@ let () =
let () = Context.register
begin fun () ->
- F.set_builtin_2 f_gt_float builtin_gt_float;
- F.set_builtin_2 f_ge_float builtin_ge_float;
- F.set_builtin_2 f_gt_double builtin_gt_double;
- F.set_builtin_2 f_ge_double builtin_ge_double;
-
F.set_builtin_1 f_real_of_int builtin_real_of_int ;
F.set_builtin_1 f_truncate (builtin_truncate f_truncate) ;
F.set_builtin_1 f_ceil (builtin_truncate f_ceil) ;
diff --git a/src/plugins/wp/Cmath.mli b/src/plugins/wp/Cmath.mli
index e27a286e076c264de3d18f930b477a3019700f5c..7c1510ffdc31ba5d0463ffb389a324544528f07e 100644
--- a/src/plugins/wp/Cmath.mli
+++ b/src/plugins/wp/Cmath.mli
@@ -34,3 +34,5 @@ val f_real_of_int : lfun
val f_iabs : lfun
val f_rabs : lfun
val f_sqrt : lfun
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index b46c539ca5100a4cb67bce7395195998f3582f92..7dd358acc6900842611fed12bc90a0c096eaa60c 100644
--- a/src/plugins/wp/share/wp.driver
+++ b/src/plugins/wp/share/wp.driver
@@ -105,14 +105,6 @@ predicate "\\is_plus_infinity"(float32) = "is_positive_infinite_f32";
predicate "\\is_plus_infinity"(float64) = "is_positive_infinite_f64";
predicate "\\is_minus_infinity"(float32) = "is_negative_infinite_f32";
predicate "\\is_minus_infinity"(float64) = "is_negative_infinite_f64";
-predicate "\\le_float"(float32,float32) = "le_f32";
-predicate "\\lt_float"(float32,float32) = "lt_f32";
-predicate "\\eq_float"(float32,float32) = "eq_f32";
-predicate "\\ne_float"(float32,float32) = "ne_f64";
-predicate "\\le_double"(float64,float64) = "le_f64";
-predicate "\\lt_double"(float64,float64) = "lt_f64";
-predicate "\\eq_double"(float64,float64) = "eq_f64";
-predicate "\\ne_double"(float64,float64) = "ne_f64";
logic bool "\\round_float"(rounding_mode,real) = "round_float";
logic bool "\\round_double"(rounding_mode,real) = "round_double";