From 66570f60b0cdc6309e000f8bd351b8815ff4107f Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 28 Sep 2020 13:52:40 +0200
Subject: [PATCH] [wp+qed] Allow to force builtin in Qed
---
src/plugins/qed/logic.ml | 42 ++++++++++++++++++++++++++++++++++------
src/plugins/qed/term.ml | 25 ++++++++++++------------
src/plugins/wp/Lang.ml | 16 +++++++++++----
3 files changed, 61 insertions(+), 22 deletions(-)
diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index e7ce8e49087..eb4ff31c0b0 100644
--- a/src/plugins/qed/logic.ml
+++ b/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} *)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index c533be908fb..bc8331ad3c9 100644
--- a/src/plugins/qed/term.ml
+++ b/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 --- *)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 43f7709a6ac..2c3dbf50588 100644
--- a/src/plugins/wp/Lang.ml
+++ b/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
--
GitLab