From 596242f1031f069e1c9ddf1434ac9ba0f9fe99ee Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 18 Feb 2019 10:57:29 +0100
Subject: [PATCH] [wp] move simplifier type to Lang
---
src/plugins/wp/Cint.mli | 4 ++--
src/plugins/wp/Conditions.ml | 17 -----------------
src/plugins/wp/Conditions.mli | 28 +---------------------------
src/plugins/wp/Lang.ml | 21 +++++++++++++++++++++
src/plugins/wp/Lang.mli | 29 +++++++++++++++++++++++++++++
5 files changed, 53 insertions(+), 46 deletions(-)
diff --git a/src/plugins/wp/Cint.mli b/src/plugins/wp/Cint.mli
index 263c43e16af..a78c5b91909 100644
--- a/src/plugins/wp/Cint.mli
+++ b/src/plugins/wp/Cint.mli
@@ -77,10 +77,10 @@ val f_bitwised : lfun list (** All except f_bit *)
(** Simplifiers *)
-val is_cint_simplifier: Conditions.simplifier
+val is_cint_simplifier: simplifier
(** Remove the [is_cint] in formulas that are
redundant with other conditions. *)
-val mask_simplifier: Conditions.simplifier
+val mask_simplifier: simplifier
val is_positive_or_null: term -> bool
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index aa3a1478d52..1fac69012b5 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -845,23 +845,6 @@ and letify_case sigma ~target ~export seq =
(* --- External Simplifier --- *)
(* -------------------------------------------------------------------------- *)
-exception Contradiction
-
-class type simplifier =
- object
- method name : string
- method copy : simplifier
- method assume : F.pred -> unit
- method target : F.pred -> unit
- method fixpoint : unit
- method infer : F.pred list
-
- method simplify_exp : F.term -> F.term
- method simplify_hyp : F.pred -> F.pred
- method simplify_branch : F.pred -> F.pred
- method simplify_goal : F.pred -> F.pred
- end
-
let simplify_exp solvers e =
List.fold_left (fun e s -> s#simplify_exp e) e solvers
let simplify_goal solvers p =
diff --git a/src/plugins/wp/Conditions.mli b/src/plugins/wp/Conditions.mli
index 46607fa5871..7a5c2b853e0 100644
--- a/src/plugins/wp/Conditions.mli
+++ b/src/plugins/wp/Conditions.mli
@@ -180,36 +180,10 @@ val bundle : bundle -> sequence
(** {2 Simplifier} *)
-exception Contradiction
-
-class type simplifier =
- object
- method name : string
- method copy : simplifier
- method assume : F.pred -> unit
- (** Assumes the hypothesis *)
- method target : F.pred -> unit
- (** Give the predicate that will be simplified later *)
- method fixpoint : unit
- (** Called after assuming hypothesis and knowing the goal *)
- method infer : F.pred list
- (** Add new hypotheses implied by the original hypothesis. *)
-
- method simplify_exp : F.term -> F.term
- (** Currently simplify an expression. *)
- method simplify_hyp : F.pred -> F.pred
- (** Currently simplify an hypothesis before assuming it. In any
- case must return a weaker formula. *)
- method simplify_branch : F.pred -> F.pred
- (** Currently simplify a branch condition. In any case must return an
- equivalent formula. *)
- method simplify_goal : F.pred -> F.pred
- (** Simplify the goal. In any case must return a stronger formula. *)
- end
-
val clean : sequent -> sequent
val filter : sequent -> sequent
val parasite : sequent -> sequent
val simplify : ?solvers:simplifier list -> ?intros:int -> sequent -> sequent
val pruning : ?solvers:simplifier list -> sequent -> sequent
+
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 8577ac6702a..3051ed18a41 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -1000,3 +1000,24 @@ struct
end
(* -------------------------------------------------------------------------- *)
+(* --- Simplifier --- *)
+(* -------------------------------------------------------------------------- *)
+
+exception Contradiction
+
+class type simplifier =
+ object
+ method name : string
+ method copy : simplifier
+ method assume : F.pred -> unit
+ method target : F.pred -> unit
+ method fixpoint : unit
+ method infer : F.pred list
+
+ method simplify_exp : F.term -> F.term
+ method simplify_hyp : F.pred -> F.pred
+ method simplify_branch : F.pred -> F.pred
+ method simplify_goal : F.pred -> F.pred
+ end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 4644a22391f..e594b3720e9 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -552,4 +552,33 @@ sig
end
+(** {2 Simplifiers} *)
+
+exception Contradiction
+
+class type simplifier =
+ object
+ method name : string
+ method copy : simplifier
+ method assume : F.pred -> unit
+ (** Assumes the hypothesis *)
+ method target : F.pred -> unit
+ (** Give the predicate that will be simplified later *)
+ method fixpoint : unit
+ (** Called after assuming hypothesis and knowing the goal *)
+ method infer : F.pred list
+ (** Add new hypotheses implied by the original hypothesis. *)
+
+ method simplify_exp : F.term -> F.term
+ (** Currently simplify an expression. *)
+ method simplify_hyp : F.pred -> F.pred
+ (** Currently simplify an hypothesis before assuming it. In any
+ case must return a weaker formula. *)
+ method simplify_branch : F.pred -> F.pred
+ (** Currently simplify a branch condition. In any case must return an
+ equivalent formula. *)
+ method simplify_goal : F.pred -> F.pred
+ (** Simplify the goal. In any case must return a stronger formula. *)
+ end
+
(* -------------------------------------------------------------------------- *)
--
GitLab