diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index e7d338eb65ac927c372450109ea548f80c755c25..447f155996c70d9e4f244ddeea2a43f7cba231f7 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -71,6 +71,10 @@ let tau_of_float f =
| Real -> Logic.Real
| Float -> ftau f
+let float_name = function
+ | Float32 -> "float"
+ | Float64 -> "double"
+
(* -------------------------------------------------------------------------- *)
(* --- Operators --- *)
(* -------------------------------------------------------------------------- *)
@@ -110,17 +114,22 @@ let op_name = function
module REGISTRY = WpContext.Static
(struct
type key = lfun
- type data = op * c_float
+ type data = op * c_float * (term list -> term) option
let name = "Wp.Cfloat.REGISTRY"
include Lang.Fun
end)
-let find = REGISTRY.find
+let get_impl x =
+ match REGISTRY.find x with
+ | _, _, Some impl -> impl
+ | _ -> raise Not_found
+
+let find k = let tf, phi, _ = REGISTRY.find k in tf, phi
let () = Context.register
begin fun () ->
- REGISTRY.define fq32 (EXACT,Float32) ;
- REGISTRY.define fq64 (EXACT,Float64) ;
+ REGISTRY.define fq32 (EXACT,Float32,None) ;
+ REGISTRY.define fq64 (EXACT,Float64,None) ;
end
(* -------------------------------------------------------------------------- *)
@@ -288,8 +297,8 @@ let compute_real op xs =
| NE , [ x ; y ] -> F.e_neq x y
| _ -> raise Not_found
-let compute op ulp xs =
- match Context.get model with
+let compute model op ulp xs =
+ match model with
| Real -> compute_real op xs
| Float -> compute_float op ulp xs
@@ -297,62 +306,142 @@ let compute op ulp xs =
(* --- Operations --- *)
(* -------------------------------------------------------------------------- *)
-let make_fun_float ?result name op ft =
+let make_fun_float ?result model name op ft =
let result = match result with None -> ftau ft | Some r -> r in
let phi = extern_f ~library ~result "%s_%a" name pp_suffix ft in
- Lang.F.set_builtin phi (compute op ft) ;
- REGISTRY.define phi (op,ft) ; phi
+ let impl = compute model op ft in
+ Lang.F.set_builtin phi impl ;
+ REGISTRY.define phi (op,ft, Some impl) ;
+ phi
-let make_pred_float name op ft =
+let make_pred_float model name op ft =
let prop = Pretty_utils.sfprintf "%s_%a" name pp_suffix ft in
let bool = Pretty_utils.sfprintf "%s_%ab" name pp_suffix ft in
let phi = extern_p ~library ~bool ~prop () in
- Lang.F.set_builtin phi (compute op ft) ;
- REGISTRY.define phi (op,ft) ; phi
+ let impl = compute model op ft in
+ Lang.F.set_builtin phi impl ;
+ REGISTRY.define phi (op,ft, Some impl) ;
+ phi
let f_memo = Ctypes.f_memo
-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)
+module Model (X: sig val kind: model end) =
+struct
+ let make_fun_float ?result = make_fun_float ?result X.kind
+ let make_pred_float = make_pred_float X.kind
+
+ 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 = 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)
+end
+
+module Real_model = Model(struct let kind = Real end)
+module Float_model = Model(struct let kind = Float end)
+
+let model_flt_add = function
+ | Real -> Real_model.flt_add
+ | Float -> Float_model.flt_add
+
+let model_flt_mul = function
+ | Real -> Real_model.flt_mul
+ | Float -> Float_model.flt_mul
+
+let model_flt_div = function
+ | Real -> Real_model.flt_div
+ | Float -> Float_model.flt_div
+
+let model_flt_neg = function
+ | Real -> Real_model.flt_neg
+ | Float -> Float_model.flt_neg
+
+let model_flt_lt = function
+ | Real -> Real_model.flt_lt
+ | Float -> Float_model.flt_lt
+
+let model_flt_eq = function
+ | Real -> Real_model.flt_eq
+ | Float -> Float_model.flt_eq
+
+let model_flt_le = function
+ | Real -> Real_model.flt_le
+ | Float -> Float_model.flt_le
+
+let model_flt_neq = function
+ | Real -> Real_model.flt_neq
+ | Float -> Float_model.flt_neq
+
+let model_real_of_flt = function
+ | Real -> Real_model.real_of_flt
+ | Float -> Float_model.real_of_flt
+
+let model_flt_of_real = function
+ | Real -> Real_model.flt_of_real
+ | Float -> Float_model.flt_of_real
+
+let flt_eq ft = model_flt_eq (Context.get model) ft
+let flt_neq = model_flt_neq (Context.get model)
+let flt_le = model_flt_le (Context.get model)
+let flt_lt = model_flt_lt (Context.get model)
+let flt_neg = model_flt_neg (Context.get model)
+let flt_add ft = model_flt_add (Context.get model) ft
+let flt_mul = model_flt_mul (Context.get model)
+let flt_div = model_flt_div (Context.get model)
+let flt_of_real = model_flt_of_real (Context.get model)
+let real_of_flt = model_real_of_flt (Context.get model)
-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 hack f ft xs =
+ let phi = f (Context.get model) ft in
+ try (get_impl phi) xs
+ with Not_found -> F.e_fun phi xs
+
+let make_converse_dispatch name dispatch ft =
+ let register model_name impl =
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 ;
- let converse phi x y = e_fun phi [y;x] in
- Lang.F.set_builtin_2 gt (converse (flt_lt ft)) ;
- Lang.F.set_builtin_2 ge (converse (flt_le ft)) ;
- end
+ let phi = generated_f ~params:[Sdata;Sdata] ~sort:Sprop "\\%s_%s_%s"
+ model_name name (float_name ft)
+ in
+ Lang.F.set_builtin phi impl
+ in
+ let op_r xs = (hack dispatch ft) (List.rev xs) in
+ let op_f xs = (hack dispatch ft) (List.rev xs) in
+ register "Real" op_r ;
+ register "Float" op_f ;
+ let hack params =
+ match Context.get model with
+ | Real -> op_r params
+ | Float -> op_f params
+ in
+ hack
+
+let make_all ft =
+ let suffix = float_name ft in
+ let gt_dispatch = make_converse_dispatch "gt" model_flt_lt ft in
+ let ge_dispatch = make_converse_dispatch "ge" model_flt_le ft in
+ LogicBuiltins.hack ("\\lt_" ^ suffix) (hack model_flt_lt ft) ;
+ LogicBuiltins.hack ("\\gt_" ^ suffix) gt_dispatch ;
+ LogicBuiltins.hack ("\\le_" ^ suffix) (hack model_flt_le ft) ;
+ LogicBuiltins.hack ("\\ge_" ^ suffix) ge_dispatch ;
+ LogicBuiltins.hack ("\\eq_" ^ suffix) (hack model_flt_eq ft) ;
+ LogicBuiltins.hack ("\\ne_" ^ suffix) (hack model_flt_neq ft) ;
+ ()
let () =
Context.register
begin fun () ->
- register_builtin_comparison "float" Float32 ;
- register_builtin_comparison "double" Float64 ;
+ make_all Float32 ;
+ make_all Float64
end
(* -------------------------------------------------------------------------- *)
@@ -360,17 +449,14 @@ let () =
(* -------------------------------------------------------------------------- *)
let () =
- Context.register
- begin fun () ->
- let open LogicBuiltins in
- 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_builtin Float32 ;
- register_builtin Float64 ;
- end
+ let open LogicBuiltins in
+ 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_builtin Float32 ;
+ register_builtin Float64
(* -------------------------------------------------------------------------- *)
(* --- Conversion Symbols --- *)