[WP] No more add_builtin during config in Cfloat

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                                                 --- *)