[qed] introduction of e_open and e_close

src/plugins/qed/logic.ml

@@ -306,11 +306,12 @@ sig
   (** Bind the given variable if it appears free in the term,
       or return the term unchanged. *)
 
-  val e_open : var -> term -> term
-  (** Open the top-most binder with the given variable, or
-      return the term unchanged.
-      @raise Invalid_argument if the variable is not free and
-      has not the right type. *)
+  val e_open : ?pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool ->
+    term -> (binder * var) list * term
+  (** Open all the specified binders *)
+
+  val e_close : (binder * var) list -> term -> term
+  (** Closes all specified binders *)
 
   (** {3 Local Caches} *)
 

src/plugins/qed/term.ml

@@ -2285,15 +2285,6 @@ struct
           | _ -> is_eq e
         in ignore(exists_case a); !res
 
-  let e_open x (e : term) =
-    assert (lc_closed e) ;
-    match e.repr with
-    | Bind(_,t,a) ->
-        if not (Tau.equal t (tau_of_var x) || Vars.mem x e.vars)
-        then lc_open x a
-        else raise (Invalid_argument "Qed.e_open")
-    | _ -> e
-
   let e_bind q x (e : term) =
     assert (lc_closed e) ;
     let do_bind =
@@ -2311,6 +2302,26 @@ struct
   let e_exists = bind_xs Exists
   let e_lambda = bind_xs Lambda
 
+  let e_open ?pool ?(forall=true) ?(exists=true) ?(lambda=true) a =
+    match a.repr with
+    | Bind _ ->
+        let pool = match pool with Some p -> p | None ->
+          let p = POOL.create () in
+          Vars.iter (POOL.add p) a.vars ; p in
+        let filter = function
+          | Forall -> forall
+          | Exists -> exists
+          | Lambda -> lambda in
+        let rec walk qs a = match a.repr with
+          | Bind(q,t,b) when filter q ->
+              let x = fresh pool t in
+              walk ((q,x)::qs) (lc_open x b)
+          | _ -> qs , a
+        in walk [] a
+    | _ -> [],a
+
+  let e_close qs a = List.fold_left (fun b (q,x) -> e_bind q x b) a qs
+
   (* -------------------------------------------------------------------------- *)
   (* --- Iterators                                                          --- *)
   (* -------------------------------------------------------------------------- *)

src/plugins/wp/Lang.mli

@@ -293,6 +293,14 @@ sig
   val e_fun : Fun.t -> term list -> term
   val e_bind : binder -> var -> term -> term
 
+  val e_open : pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool ->
+    term -> (binder * var) list * term
+  (** Open all the specified binders
+      The pool must contain all free variables of the term. *)
+
+  val e_close : (binder * var) list -> term -> term
+  (** Closes all specified binders *)
+
   (** {3 Predicates} *)
 
   type pred
@@ -398,7 +406,7 @@ sig
   (** {3 Binders} *)
 
   val lc_closed : term -> bool
-  val lc_iter : (term -> unit) -> term -> unit
+  val lc_iter : (term -> unit) -> term -> unit (* TODO: to remove *)
 
   (** {3 Utilities} *)