Merge branch 'feature/wp/fix-circular-dependencies' into 'master'

[wp] move simplifier type to Lang

See merge request frama-c/frama-c!2155

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

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 =

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

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

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