diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index a451922eb1f2411ea7fb1f72e7a2e906f9f8a4c0..91338a35f39b1ae9c23f051afebb2150d72373f5 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -368,14 +368,23 @@ sig
val e_subst_var : var -> term -> term -> term
- (** {3 Locally Nameless Representation} *)
+ (** {3 Locally Nameless Representation}
- val lc_closed : term -> bool (** All bound variables are under their binder *)
+ These functions can be {i unsafe} because they might expose terms
+ that contains non-bound b-vars. Never use such terms to build
+ substitutions (sigma).
+ *)
val lc_vars : term -> Bvars.t
+ val lc_closed : term -> bool
+ (** All bound variables are under their binder *)
- val lc_term : term -> lc_term
val lc_repr : lc_term -> term
+ (** Calling this function is {i unsafe} unless the term is lc_closed *)
+
+ val lc_iter : (term -> unit) -> term -> unit
+ (** Similar to [f_iter] but exposes non-closed sub-terms of `Bind`
+ as regular [term] values instead of [lc_term] ones. *)
(** {3 Iteration Scheme} *)
@@ -392,8 +401,6 @@ sig
Raises Invalid_argument in case of a bind-term without pool.
The optional pool must contain all free variables of the term. *)
- val lc_iter : (term -> unit) -> term -> unit
-
(** {3 Partial Typing} *)
(** Try to extract a type of term.
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 1c3ca9819c35e78e420af817cd891e54c527bb2c..ff663736385c38996242a8f7a39857d35bc6ba1e 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -1970,7 +1970,6 @@ struct
let lc_closed_at n e = Bvars.closed_at n e.bind
let lc_vars e = e.bind
let lc_repr e = e
- let lc_term e = e
(*
Warning: must only be used for alpha-conversion
@@ -2080,6 +2079,13 @@ struct
filter = [] ;
}
+ let validate fn e =
+ if false && not (lc_closed e) then
+ begin
+ Format.eprintf "Invalid %s: %a@." fn pretty e ;
+ raise (Invalid_argument (fn ^ ": non lc-closed binding"))
+ end
+
let cache sigma =
ref begin
match sigma.shared with MAP( m , _ ) -> m | _ -> Tmap.empty
@@ -2087,11 +2093,15 @@ struct
let fresh sigma t = fresh sigma.pool t
+ let call f e =
+ let v = f e in
+ validate "Qed.Subst.add_fun" v ; v
+
let rec compute e = function
| EMPTY -> raise Not_found
- | FUN(f,EMPTY) -> f e
+ | FUN(f,EMPTY) -> call f e
| MAP(m,EMPTY) -> Tmap.find e m
- | FUN(f,s) -> (try f e with Not_found -> compute e s)
+ | FUN(f,s) -> (try call f e with Not_found -> compute e s)
| MAP(m,s) -> (try Tmap.find e m with Not_found -> compute e s)
let get sigma a = compute a sigma.shared
@@ -2100,13 +2110,22 @@ struct
List.for_all (fun f -> f a) sigma.filter
let add sigma a b =
+ validate "Qed.Subst.add (domain)" a ;
+ validate "Qed.Subst.add (codomain)" b ;
sigma.shared <- match sigma.shared with
| MAP(m,s) -> MAP (Tmap.add a b m,s)
| (FUN _ | EMPTY) as s -> MAP (Tmap.add a b Tmap.empty,s)
let add_map sigma m =
if not (Tmap.is_empty m) then
- sigma.shared <- MAP(m,sigma.shared)
+ begin
+ Tmap.iter
+ (fun a b ->
+ validate "Qed.Subst.add_map (domain)" a ;
+ validate "Qed.Subst.add_map (codomain)" b ;
+ ) m ;
+ sigma.shared <- MAP(m,sigma.shared)
+ end
let add_fun sigma f =
sigma.shared <- FUN(f,sigma.shared)
@@ -2184,9 +2203,12 @@ struct
c_apply f' vs
let e_subst sigma e =
+ Subst.validate "Qed.e_subst (target)" e ;
subst sigma Intmap.empty e
let e_subst_var x v e =
+ Subst.validate "Qed.e_subst_var (value)" v ;
+ Subst.validate "Qed.e_subst_var (target)" e ;
let filter e = Vars.mem x e.vars in
if not (filter e) then e else
if Bvars.is_empty v.bind && Bvars.is_empty e.bind then
@@ -2302,8 +2324,8 @@ struct
match q with Forall | Exists -> Vars.mem x e.vars | Lambda -> true in
if do_bind then
match let_intro_case q x e with
- | None -> c_bind q (tau_of_var x) (lc_close x e)
| Some v -> e_subst_var x v e (* case [let x = v ; e] *)
+ | _ -> c_bind q (tau_of_var x) (lc_close x e)
else e
let e_close qs a = List.fold_left (fun b (q,x) -> e_bind q x b) a qs
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 4996cc10890733f2cf17ff7c8c47057dade44838..1f2ecea227a8d5771411009634b05f861e16ddf6 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -757,7 +757,7 @@ struct
let p_forall = e_forall
let p_exists = e_exists
let p_subst = e_subst
- let p_apply = e_subst_var
+ let p_subst_var = e_subst_var
let p_and p q = e_and [p;q]
let p_or p q = e_or [p;q]
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index d02b68cdb98e5ad7a59352b3c7e30d1680f45490..ee4a6dade82b253a7bfbfb82cf5bd26927b89d52 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -365,7 +365,7 @@ sig
val e_subst : sigma -> term -> term
val p_subst : sigma -> pred -> pred
- val p_apply : var -> term -> pred -> pred
+ val p_subst_var : var -> term -> pred -> pred
val e_vars : term -> var list (** Sorted *)
val p_vars : pred -> var list (** Sorted *)
diff --git a/src/plugins/wp/TacInstance.ml b/src/plugins/wp/TacInstance.ml
index 9e5f2c1311c7d68202a9699cdc34bfad81bdb717..1b95285882dde1a81db416d4eb23ac4b1537fa58 100644
--- a/src/plugins/wp/TacInstance.ml
+++ b/src/plugins/wp/TacInstance.ml
@@ -79,12 +79,13 @@ let rec bind_exists bindings property =
Lang.F.p_bind L.Exists x property
else
let value = Tactical.selected v in
- Lang.F.p_apply x value property
+ Lang.F.p_subst_var x value property
in bind_exists bindings closed
let rec range x a b w =
if a <= b then
- ( Printf.sprintf "%s-%d" (fst w) a , F.p_apply x (F.e_int a) (snd w) )
+ ( Printf.sprintf "%s-%d" (fst w) a ,
+ Lang.F.p_subst_var x (F.e_int a) (snd w) )
:: range x (succ a) b w
else []
@@ -104,7 +105,7 @@ let rec bind_forall ranges bindings property =
bind_forall ranges bindings (Lang.F.p_bind L.Forall x property)
| _ ->
let value = Tactical.selected v in
- bind_forall ranges bindings (Lang.F.p_apply x value property)
+ bind_forall ranges bindings (Lang.F.p_subst_var x value property)
end
| [] ->
bind_ranges [ "Instance" , property ] ranges