[wp+qed] Allow to force builtin in Qed

src/plugins/qed/logic.ml

@@ -418,7 +418,7 @@ sig
 
   (** {3 Support for Builtins} *)
 
-  val set_builtin : Fun.t -> (term list -> term) -> unit
+  val set_builtin : ?force: bool -> Fun.t -> (term list -> term) -> unit
   (** Register a simplifier for function [f]. The computation code
         may raise [Not_found], in which case the symbol is not interpreted.
 
@@ -428,33 +428,58 @@ sig
 
         Highest priority is [0].
         Recursive calls must be performed on strictly smaller terms.
+
+        The [force] parameters defaults to [false], when it is [true], if there
+        exist another builtin, it is replaced with the new one. Use with care.
+
+        @modify Frama-C+dev add optional [force] parameter
   *)
 
-  val set_builtin' : Fun.t -> (term list -> tau option -> term) -> unit
+  val set_builtin' :
+    ?force: bool -> Fun.t -> (term list -> tau option -> term) -> unit
 
-  val set_builtin_map : Fun.t -> (term list -> term list) -> unit
+  val set_builtin_map :
+    ?force: bool ->  Fun.t -> (term list -> term list) -> unit
   (** Register a builtin for rewriting [f a1..an] into [f b1..bm].
 
       This is short cut for [set_builtin], where the head application of [f] avoids
       to run into an infinite loop.
+
+      The [force] parameters defaults to [false], when it is [true], if there
+      exist another builtin, it is replaced with the new one. Use with care.
+
+      @modify Frama-C+dev add optional [force] parameter
   *)
 
-  val set_builtin_get : Fun.t -> (term list -> tau option -> term -> term) -> unit
+  val set_builtin_get :
+    ?force: bool -> Fun.t -> (term list -> tau option -> term -> term) -> unit
   (** [set_builtin_get f rewrite] register a builtin
       for rewriting [(f a1..an)[k]] into [rewrite (a1..an) k].
       The type given is the type of (f a1..an).
+
+      The [force] parameters defaults to [false], when it is [true], if there
+      exist another builtin, it is replaced with the new one. Use with care.
+
+      @modify Frama-C+dev add optional [force] parameter
   *)
 
-  val set_builtin_eq : Fun.t -> (term -> term -> term) -> unit
+  val set_builtin_eq :
+    ?force: bool -> Fun.t -> (term -> term -> term) -> unit
   (** Register a builtin equality for comparing any term with head-symbol.
         {b Must} only use recursive comparison for strictly smaller terms.
         The recognized term with head function symbol is passed first.
 
         Highest priority is [0].
         Recursive calls must be performed on strictly smaller terms.
+
+        The [force] parameters defaults to [false], when it is [true], if there
+        exist another builtin, it is replaced with the new one. Use with care.
+
+        @modify Frama-C+dev add optional [force] parameter
   *)
 
-  val set_builtin_leq : Fun.t -> (term -> term -> term) -> unit
+  val set_builtin_leq :
+    ?force: bool -> Fun.t -> (term -> term -> term) -> unit
   (** Register a builtin for comparing any term with head-symbol.
         {b Must} only use recursive comparison for strictly smaller terms.
         The recognized term with head function symbol can be on both sides.
@@ -462,6 +487,11 @@ sig
 
         Highest priority is [0].
         Recursive calls must be performed on strictly smaller terms.
+
+        The [force] parameters defaults to [false], when it is [true], if there
+        exist another builtin, it is replaced with the new one. Use with care.
+
+        @modify Frama-C+dev add optional [force] parameter
   *)
 
   (** {3 Specific Patterns} *)

src/plugins/qed/term.ml

@@ -1009,40 +1009,41 @@ struct
   let c_builtin_lt  a b = distribute_if_over_operation true (fun a b -> operation (CMP(LT ,a,b))) a b !extern_lt  a b
   let c_builtin_leq a b = distribute_if_over_operation true (fun a b -> operation (CMP(LEQ,a,b))) a b !extern_leq a b
 
-  let prepare_builtin f m =
+  let prepare_builtin ~force f m =
     release () ;
-    if BUILTIN.mem f m then
+    if BUILTIN.mem f m && not force then
       let msg = Printf.sprintf
           "Builtin already registered for '%s'" (Fun.debug f) in
       raise (Failure msg)
 
-  let set_builtin' f p =
+  let set_builtin' ?(force=false) f p =
     begin
-      prepare_builtin f !state.builtins_fun ;
+      prepare_builtin ~force f !state.builtins_fun ;
       !state.builtins_fun <- BUILTIN.add f p !state.builtins_fun ;
     end
 
-  let set_builtin f p = set_builtin' f (fun es _ -> p es)
+  let set_builtin ?force f p = set_builtin' ?force f (fun es _ -> p es)
 
-  let set_builtin_get f p =
+  let set_builtin_get ?(force=false) f p =
     begin
-      prepare_builtin f !state.builtins_get ;
+      prepare_builtin ~force f !state.builtins_get ;
       !state.builtins_get <- BUILTIN.add f p !state.builtins_get ;
     end
 
-  let set_builtin_eq f p =
+  let set_builtin_eq ?(force=false) f p =
     begin
-      prepare_builtin f !state.builtins_eq ;
+      prepare_builtin ~force f !state.builtins_eq ;
       !state.builtins_eq <- BUILTIN.add f p !state.builtins_eq ;
     end
 
-  let set_builtin_leq f p =
+  let set_builtin_leq ?(force=false) f p =
     begin
-      prepare_builtin f !state.builtins_leq ;
+      prepare_builtin ~force f !state.builtins_leq ;
       !state.builtins_leq <- BUILTIN.add f p !state.builtins_leq ;
     end
 
-  let set_builtin_map f phi = set_builtin' f (fun es tau -> c_fun f (phi es) tau)
+  let set_builtin_map ?force f phi =
+    set_builtin' ?force f (fun es tau -> c_fun f (phi es) tau)
 
   (* -------------------------------------------------------------------------- *)
   (* --- Negation                                                           --- *)

src/plugins/wp/Lang.ml

@@ -726,6 +726,14 @@ struct
   end
   include QED
 
+  (* Hide force parameter. *)
+  let set_builtin f = QZERO.set_builtin f
+  let set_builtin' f = QZERO.set_builtin' f
+  let set_builtin_eq f = QZERO.set_builtin_eq f
+  let set_builtin_leq f = QZERO.set_builtin_leq f
+  let set_builtin_get f = QZERO.set_builtin_get f
+
+
   (* -------------------------------------------------------------------------- *)
   (* --- Term Extensions                                                    --- *)
   (* -------------------------------------------------------------------------- *)
@@ -1042,14 +1050,14 @@ module For_export = struct
   let rebuild ?cache t = QZERO.rebuild_in_state (get_state ()) ?cache t
 
   let set_builtin f c =
-    add_init (fun () -> QZERO.set_builtin f c)
+    add_init (fun () -> QZERO.set_builtin ~force:true f c)
 
   let set_builtin' f c =
-    add_init (fun () -> QZERO.set_builtin' f c)
+    add_init (fun () -> QZERO.set_builtin' ~force:true f c)
   let set_builtin_eq f c =
-    add_init (fun () -> QZERO.set_builtin_eq f c)
+    add_init (fun () -> QZERO.set_builtin_eq ~force:true f c)
   let set_builtin_leq f c =
-    add_init (fun () -> QZERO.set_builtin_leq f c)
+    add_init (fun () -> QZERO.set_builtin_leq ~force:true f c)
 
   let in_state f v = QZERO.in_state (get_state ()) f v