aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/ppconstr.ml1
-rw-r--r--parsing/ppconstr.mli1
-rw-r--r--parsing/printer.ml13
-rw-r--r--parsing/printer.mli6
-rw-r--r--plugins/field/field.ml46
-rw-r--r--plugins/setoid_ring/newring.ml42
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml16
-rw-r--r--pretyping/matching.ml110
-rw-r--r--pretyping/matching.mli13
-rw-r--r--pretyping/pattern.ml42
-rw-r--r--pretyping/pattern.mli48
-rw-r--r--pretyping/pretyping.ml33
-rw-r--r--pretyping/pretyping.mli21
-rw-r--r--proofs/evar_refiner.mli2
-rw-r--r--proofs/proof_type.ml2
-rw-r--r--proofs/proof_type.mli2
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/evar_tactics.ml2
-rw-r--r--tactics/tacinterp.ml152
-rw-r--r--tactics/tacinterp.mli6
-rw-r--r--tactics/tauto.ml410
-rw-r--r--test-suite/success/ltac.v13
-rw-r--r--toplevel/himsg.ml4
23 files changed, 339 insertions, 168 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 597505686d..cf5a58eea4 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -122,6 +122,7 @@ let pr_rawsort = function
let pr_id = pr_id
let pr_name = pr_name
let pr_qualid = pr_qualid
+let pr_patvar = pr_id
let pr_expl_args pr (a,expl) =
match expl with
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 2becdbcfd6..afa744a507 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -46,6 +46,7 @@ val pr_sep_com :
val pr_id : identifier -> std_ppcmds
val pr_name : name -> std_ppcmds
val pr_qualid : qualid -> std_ppcmds
+val pr_patvar : patvar -> std_ppcmds
val pr_with_occurrences :
('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds
diff --git a/parsing/printer.ml b/parsing/printer.ml
index d3c4ae63da..61f7e377a2 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -57,6 +57,19 @@ let pr_constr t = pr_constr_env (Global.env()) t
let pr_open_lconstr (_,c) = pr_lconstr c
let pr_open_constr (_,c) = pr_constr c
+let pr_constr_under_binders_env_gen pr env (ids,c) =
+ (* Warning: clashes can occur with variables of same name in env but *)
+ (* we also need to preserve the actual names of the patterns *)
+ (* So what to do? *)
+ let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in
+ pr (push_rels_assum assums env) c
+
+let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env
+let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env
+
+let pr_constr_under_binders c = pr_constr_under_binders_env (Global.env()) c
+let pr_lconstr_under_binders c = pr_lconstr_under_binders_env (Global.env()) c
+
let pr_type_core at_top env t =
pr_constr_expr (extern_type at_top env t)
let pr_ltype_core at_top env t =
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 52a0900759..241650b7d6 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -38,6 +38,12 @@ val pr_open_constr : open_constr -> std_ppcmds
val pr_open_lconstr_env : env -> open_constr -> std_ppcmds
val pr_open_lconstr : open_constr -> std_ppcmds
+val pr_constr_under_binders_env : env -> constr_under_binders -> std_ppcmds
+val pr_constr_under_binders : constr_under_binders -> std_ppcmds
+
+val pr_lconstr_under_binders_env : env -> constr_under_binders -> std_ppcmds
+val pr_lconstr_under_binders : constr_under_binders -> std_ppcmds
+
val pr_ltype_env_at_top : env -> types -> std_ppcmds
val pr_ltype_env : env -> types -> std_ppcmds
val pr_ltype : types -> std_ppcmds
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index f08ed7db61..4ea9c99b79 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.ml4
@@ -154,7 +154,7 @@ let field g =
| _ -> raise Exit
with Hipattern.NoEquationFound | Exit ->
error "The statement is not built from Leibniz' equality" in
- let th = VConstr (lookup (pf_env g) typ) in
+ let th = VConstr ([],lookup (pf_env g) typ) in
(interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ())
<:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g
@@ -174,8 +174,8 @@ let field_term l g =
Coqlib.check_required_library ["Coq";"field";"LegacyField"];
let env = (pf_env g)
and evc = (project g) in
- let th = valueIn (VConstr (guess_theory env evc l))
- and nl = List.map (fun x -> valueIn (VConstr x)) (Quote.sort_subterm g l) in
+ let th = valueIn (VConstr ([],guess_theory env evc l))
+ and nl = List.map (fun x -> valueIn (VConstr ([],x))) (Quote.sort_subterm g l) in
(List.fold_right
(fun c a ->
let tac = (Tacinterp.interp <:tactic<(Field_Term $th $c)>>) in
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 0f8c2f010b..4782e001a6 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -206,7 +206,7 @@ let exec_tactic env n f args =
!res
let constr_of = function
- | VConstr c -> c
+ | VConstr ([],c) -> c
| _ -> failwith "Ring.exec_tactic: anomaly"
let stdlib_modules =
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 87c67cc147..80527f01d5 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -105,14 +105,24 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
else id
- let pretype_id loc env (lvar,unbndltacvars) id =
+ let invert_ltac_bound_name env id0 id =
+ try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+ with Not_found ->
+ errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
+ str " depends on pattern variable name " ++ pr_id id ++
+ str " which is not bound in current context")
+
+ let pretype_id loc env sigma (lvar,unbndltacvars) id =
let id = strip_meta id in (* May happen in tactics defined by Grammar *)
try
let (n,_,typ) = lookup_rel_id id (rel_context env) in
{ uj_val = mkRel n; uj_type = lift n typ }
with Not_found ->
try
- List.assoc id lvar
+ let (ids,c) = List.assoc id lvar in
+ let subst = List.map (invert_ltac_bound_name env id) ids in
+ let c = substl subst c in
+ { uj_val = c; uj_type = Retyping.get_type_of env sigma c }
with Not_found ->
try
let (_,_,typ) = lookup_named id env in
@@ -170,7 +180,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
| RVar (loc, id) ->
inh_conv_coerce_to_tycon loc env evdref
- (pretype_id loc env lvar id)
+ (pretype_id loc env !evdref lvar id)
tycon
| REvar (loc, ev, instopt) ->
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 2c0285ed24..ddfe5dd076 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -46,9 +46,10 @@ type bound_ident_map = (identifier * identifier) list
exception PatternMatchingFailure
-let constrain (n,m) (names,terms as subst) =
+let constrain (n,(ids,m as x)) (names,terms as subst) =
try
- if eq_constr m (List.assoc n terms) then subst
+ let (ids',m') = List.assoc n terms in
+ if ids = ids' && eq_constr m m' then subst
else raise PatternMatchingFailure
with
Not_found ->
@@ -56,7 +57,7 @@ let constrain (n,m) (names,terms as subst) =
Flags.if_verbose Pp.warning
("Collision between bound variable "^string_of_id n^
" and a metavariable of same name.");
- (names,(n,m)::terms)
+ (names,(n,x)::terms)
let add_binders na1 na2 (names,terms as subst) =
match na1, na2 with
@@ -76,7 +77,7 @@ let add_binders na1 na2 (names,terms as subst) =
let build_lambda toabstract stk (m : constr) =
let rec buildrec m p_0 p_1 = match p_0,p_1 with
| (_, []) -> m
- | (n, (na,t)::tl) ->
+ | (n, (_,na,t)::tl) ->
if List.mem n toabstract then
buildrec (mkLambda (na,t,m)) (n+1) tl
else
@@ -96,7 +97,58 @@ let same_case_structure (_,cs1,ind,_) ci2 br1 br2 =
| Some ind -> ind = ci2.ci_ind
| None -> cs1 = ci2.ci_cstr_ndecls
-let matches_core convert allow_partial_app pat c =
+let rec list_insert f a = function
+ | [] -> [a]
+ | b::l when f a b -> a::b::l
+ | b::l when a = b -> raise PatternMatchingFailure
+ | b::l -> b :: list_insert f a l
+
+let extract_bound_vars =
+ let rec aux k = function
+ | ([],_) -> []
+ | (n::l,(na1,na2,_)::stk) when k = n ->
+ begin match na1,na2 with
+ | Name id1,Name _ -> list_insert (<) id1 (aux (k+1) (l,stk))
+ | Name _,Anonymous -> anomaly "Unnamed bound variable"
+ | Anonymous,_ -> raise PatternMatchingFailure
+ end
+ | (l,_::stk) -> aux (k+1) (l,stk)
+ | (_,[]) -> assert false
+ in aux 1
+
+let dummy_constr = mkProp
+
+let rec make_renaming ids = function
+ | (Name id,Name _,_)::stk ->
+ let renaming = make_renaming ids stk in
+ (try mkRel (list_index id ids) :: renaming
+ with Not_found -> dummy_constr :: renaming)
+ | (_,_,_)::stk ->
+ dummy_constr :: make_renaming ids stk
+ | [] ->
+ []
+
+let merge_binding allow_bound_rels stk n cT subst =
+ let depth = List.length stk in
+ let c =
+ if depth = 0 then
+ (* Optimization *)
+ ([],cT)
+ else
+ let frels = Intset.elements (free_rels cT) in
+ let frels = List.filter (fun i -> i <= depth) frels in
+ if allow_bound_rels then
+ let frels = Sort.list (<) frels in
+ let canonically_ordered_vars = extract_bound_vars (frels,stk) in
+ let renaming = make_renaming canonically_ordered_vars stk in
+ (canonically_ordered_vars, substl renaming cT)
+ else if frels = [] then
+ ([],lift (-depth) cT)
+ else
+ raise PatternMatchingFailure in
+ constrain (n,c) subst
+
+let matches_core convert allow_partial_app allow_bound_rels pat c =
let conv = match convert with
| None -> eq_constr
| Some (env,sigma) -> is_conv env sigma in
@@ -112,21 +164,11 @@ let matches_core convert allow_partial_app pat c =
args in
let frels = Intset.elements (free_rels cT) in
if list_subset frels relargs then
- constrain (n,build_lambda relargs stk cT) subst
+ constrain (n,([],build_lambda relargs stk cT)) subst
else
raise PatternMatchingFailure
- | PMeta (Some n), m ->
- let depth = List.length stk in
- if depth = 0 then
- (* Optimisation *)
- constrain (n,cT) subst
- else
- let frels = Intset.elements (free_rels cT) in
- if List.for_all (fun i -> i > depth) frels then
- constrain (n,lift (-depth) cT) subst
- else
- raise PatternMatchingFailure
+ | PMeta (Some n), m -> merge_binding allow_bound_rels stk n cT subst
| PMeta None, m -> subst
@@ -151,14 +193,8 @@ let matches_core convert allow_partial_app pat c =
let p = Array.length args2 - Array.length args1 in
if p>=0 then
let args21, args22 = array_chop p args2 in
- let subst =
- let depth = List.length stk in
- let c = mkApp(c2,args21) in
- let frels = Intset.elements (free_rels c) in
- if List.for_all (fun i -> i > depth) frels then
- constrain (n,lift (-depth) c) subst
- else
- raise PatternMatchingFailure in
+ let c = mkApp(c2,args21) in
+ let subst = merge_binding allow_bound_rels stk n c subst in
array_fold_left2 (sorec stk) subst args1 args22
else raise PatternMatchingFailure
@@ -167,15 +203,15 @@ let matches_core convert allow_partial_app pat c =
with Invalid_argument _ -> raise PatternMatchingFailure)
| PProd (na1,c1,d1), Prod(na2,c2,d2) ->
- sorec ((na2,c2)::stk)
+ sorec ((na1,na2,c2)::stk)
(add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
| PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
- sorec ((na2,c2)::stk)
+ sorec ((na1,na2,c2)::stk)
(add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
| PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) ->
- sorec ((na2,t2)::stk)
+ sorec ((na1,na2,t2)::stk)
(add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
| PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
@@ -184,8 +220,10 @@ let matches_core convert allow_partial_app pat c =
let n = rel_context_length ctx in
let n' = rel_context_length ctx' in
if noccur_between 1 n b2 & noccur_between 1 n' b2' then
- let s = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx in
- let s' = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx' in
+ let s =
+ List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx in
+ let s' =
+ List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx' in
let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
sorec s' (sorec s (sorec stk subst a1 a2) b1 b2) b1' b2'
else
@@ -206,16 +244,20 @@ let matches_core convert allow_partial_app pat c =
let names,terms = sorec [] ([],[]) pat c in
(names,Sort.list (fun (a,_) (b,_) -> a<b) terms)
-let extended_matches = matches_core None true
+let matches_core_closed convert allow_partial_app pat c =
+ let names,subst = matches_core convert allow_partial_app false pat c in
+ (names, List.map (fun (a,(_,b)) -> (a,b)) subst)
+
+let extended_matches = matches_core None true true
-let matches c p = snd (matches_core None true c p)
+let matches c p = snd (matches_core_closed None true c p)
let special_meta = (-1)
(* Tells if it is an authorized occurrence and if the instance is closed *)
let authorized_occ partial_app closed pat c mk_ctx next =
try
- let sigma = matches_core None partial_app pat c in
+ let sigma = matches_core_closed None partial_app pat c in
if closed && not (List.for_all (fun (_,c) -> closed0 c) (snd sigma))
then next ()
else sigma, mk_ctx (mkMeta special_meta), next
@@ -308,7 +350,7 @@ let is_matching_appsubterm ?(closed=true) pat c =
with PatternMatchingFailure -> false
let matches_conv env sigma c p =
- snd (matches_core (Some (env,sigma)) false c p)
+ snd (matches_core_closed (Some (env,sigma)) false c p)
let is_matching_conv env sigma pat n =
try let _ = matches_conv env sigma pat n in true
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 95314054e5..eb9c8fc8c6 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -6,18 +6,25 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
+(** This module implements pattern-matching on terms *)
+
open Names
open Term
open Environ
open Pattern
open Termops
-(** {6 This modules implements pattern-matching on terms } *)
-
+(** [PatternMatchingFailure] is the exception raised when pattern
+ matching fails *)
exception PatternMatchingFailure
+(** [special_meta] is the default name of the meta holding the
+ surrounding context in subterm matching *)
val special_meta : metavariable
+(** [bound_ident_map] represents the result of matching binding
+ identifiers of the pattern with the binding identifiers of the term
+ matched *)
type bound_ident_map = (identifier * identifier) list
(** [matches pat c] matches [c] against [pat] and returns the resulting
@@ -31,7 +38,7 @@ val matches : constr_pattern -> constr -> patvar_map
variables or metavariables have the same name, the metavariable,
or else the rightmost bound variable, takes precedence *)
val extended_matches :
- constr_pattern -> constr -> bound_ident_map * patvar_map
+ constr_pattern -> constr -> bound_ident_map * extended_patvar_map
(** [is_matching pat c] just tells if [c] matches against [pat] *)
val is_matching : constr_pattern -> constr -> bool
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 48218f47f2..59f3cde88a 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -19,8 +19,10 @@ open Mod_subst
(* Metavariables *)
+type constr_under_binders = identifier list * constr
+
type patvar_map = (patvar * constr) list
-let pr_patvar = pr_id
+type extended_patvar_map = (patvar * constr_under_binders) list
(* Patterns *)
@@ -143,9 +145,9 @@ let pattern_of_constr sigma t =
let map_pattern_with_binders g f l = function
| PApp (p,pl) -> PApp (f l p, Array.map (f l) pl)
| PSoApp (n,pl) -> PSoApp (n, List.map (f l) pl)
- | PLambda (n,a,b) -> PLambda (n,f l a,f (g l) b)
- | PProd (n,a,b) -> PProd (n,f l a,f (g l) b)
- | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g l) b)
+ | PLambda (n,a,b) -> PLambda (n,f l a,f (g n l) b)
+ | PProd (n,a,b) -> PProd (n,f l a,f (g n l) b)
+ | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g n l) b)
| PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2)
| PCase (ci,po,p,pl) -> PCase (ci,f l po,f l p,Array.map (f l) pl)
(* Non recursive *)
@@ -153,18 +155,40 @@ let map_pattern_with_binders g f l = function
(* Bound to terms *)
| PFix _ | PCoFix _ as x) -> x
-let map_pattern f = map_pattern_with_binders (fun () -> ()) (fun () -> f) ()
+let map_pattern f = map_pattern_with_binders (fun _ () -> ()) (fun () -> f) ()
+
+let error_instantiate_pattern id l =
+ let is = if List.length l = 1 then "is" else "are" in
+ errorlabstrm "" (str "Cannot substitute the term bound to " ++ pr_id id
+ ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l
+ ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
-let rec instantiate_pattern lvar = function
- | PVar id as x -> (try Lazy.force(List.assoc id lvar) with Not_found -> x)
+let instantiate_pattern lvar c =
+ let rec aux vars = function
+ | PVar id as x ->
+ (try
+ let ctx,c = List.assoc id lvar in
+ try
+ let inst =
+ List.map (fun id -> mkRel (list_index (Name id) vars)) ctx in
+ let c = substl inst c in
+ snd (pattern_of_constr Evd.empty c)
+ with Not_found (* list_index failed *) ->
+ let vars =
+ list_map_filter (function Name id -> Some id | _ -> None) vars in
+ error_instantiate_pattern id (list_subtract ctx vars)
+ with Not_found (* List.assoc failed *) ->
+ x)
| (PFix _ | PCoFix _) -> error ("Non instantiable pattern.")
- | c -> map_pattern (instantiate_pattern lvar) c
+ | c ->
+ map_pattern_with_binders (fun id vars -> id::vars) aux vars c in
+ aux [] c
let rec liftn_pattern k n = function
| PRel i as x -> if i >= n then PRel (i+k) else x
| PFix x -> PFix (destFix (liftn k n (mkFix x)))
| PCoFix x -> PCoFix (destCoFix (liftn k n (mkCoFix x)))
- | c -> map_pattern_with_binders succ (liftn_pattern k) n c
+ | c -> map_pattern_with_binders (fun _ -> succ) (liftn_pattern k) n c
let lift_pattern k = liftn_pattern k 1
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index d805730e97..3b61c1e437 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -6,6 +6,9 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
+(** This module defines the type of pattern used for pattern-matching
+ terms in tatics *)
+
open Pp
open Names
open Sign
@@ -16,12 +19,46 @@ open Nametab
open Rawterm
open Mod_subst
-(** Pattern variables *)
+(** {5 Maps of pattern variables} *)
+
+(** Type [constr_under_binders] is for representing the term resulting
+ of a matching. Matching can return terms defined in a some context
+ of named binders; in the context, variable names are ordered by
+ (<) and referred to by index in the term Thanks to the canonical
+ ordering, a matching problem like
+
+ [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]]
+
+ will be accepted. Thanks to the reference by index, a matching
+ problem like
+
+ [match ... with [(fun x => ?p)] => [forall x => p]]
+
+ will work even if [x] is also the name of an existing goal
+ variable.
+
+ Note: we do not keep types in the signature. Besides simplicity,
+ the main reason is that it would force to close the signature over
+ binders that occur only in the types of effective binders but not
+ in the term itself (e.g. for a term [f x] with [f:A -> True] and
+ [x:A]).
+
+ On the opposite side, by not keeping the types, we loose
+ opportunity to propagate type informations which otherwise would
+ not be inferable, as e.g. when matching [forall x, x = 0] with
+ pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in
+ expression [forall x, h = x] where nothing tells how the type of x
+ could be inferred. We also loose the ability of typing ltac
+ variables before calling the right-hand-side of ltac matching clauses. *)
+
+type constr_under_binders = identifier list * constr
+
+(** Types of substitutions with or w/o bound variables *)
type patvar_map = (patvar * constr) list
-val pr_patvar : patvar -> std_ppcmds
+type extended_patvar_map = (patvar * constr_under_binders) list
-(** Patterns *)
+(** {5 Patterns} *)
type constr_pattern =
| PRef of global_reference
@@ -41,6 +78,8 @@ type constr_pattern =
| PFix of fixpoint
| PCoFix of cofixpoint
+(** {5 Functions on patterns} *)
+
val occur_meta_pattern : constr_pattern -> bool
val subst_pattern : substitution -> constr_pattern -> constr_pattern
@@ -72,6 +111,7 @@ val pattern_of_rawconstr : rawconstr ->
patvar list * constr_pattern
val instantiate_pattern :
- (identifier * constr_pattern Lazy.t) list -> constr_pattern -> constr_pattern
+ (identifier * (identifier list * constr)) list ->
+ constr_pattern -> constr_pattern
val lift_pattern : int -> constr_pattern -> constr_pattern
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 71a21f6c88..e63b9a234f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -45,8 +45,10 @@ open Evarconv
open Pattern
type typing_constraint = OfType of types option | IsType
-type var_map = (identifier * unsafe_judgment) list
+type var_map = (identifier * constr_under_binders) list
type unbound_ltac_var_map = (identifier * identifier option) list
+type ltac_var_map = var_map * unbound_ltac_var_map
+type rawconstr_ltac_closure = ltac_var_map * rawconstr
(************************************************************************)
(* This concerns Cases *)
@@ -131,7 +133,7 @@ sig
*)
val understand_ltac :
- bool -> evar_map -> env -> var_map * unbound_ltac_var_map ->
+ bool -> evar_map -> env -> ltac_var_map ->
typing_constraint -> rawconstr -> evar_map * constr
(* Standard call to get a constr from a rawconstr, resolving implicit args *)
@@ -162,18 +164,15 @@ sig
*)
val pretype :
type_constraint -> env -> evar_map ref ->
- var_map * (identifier * identifier option) list ->
- rawconstr -> unsafe_judgment
+ ltac_var_map -> rawconstr -> unsafe_judgment
val pretype_type :
val_constraint -> env -> evar_map ref ->
- var_map * (identifier * identifier option) list ->
- rawconstr -> unsafe_type_judgment
+ ltac_var_map -> rawconstr -> unsafe_type_judgment
val pretype_gen :
bool -> bool -> bool -> evar_map ref -> env ->
- var_map * (identifier * identifier option) list ->
- typing_constraint -> rawconstr -> constr
+ ltac_var_map -> typing_constraint -> rawconstr -> constr
(*i*)
end
@@ -225,7 +224,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let check_branches_message loc env evdref c (explft,lft) =
for i = 0 to Array.length explft - 1 do
if not (e_cumul env evdref lft.(i) explft.(i)) then
- let sigma = !evdref in
+ let sigma = !evdref in
error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
done
@@ -243,7 +242,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct
| Anonymous -> name'
| _ -> name
- let pretype_id loc env (lvar,unbndltacvars) id =
+ let invert_ltac_bound_name env id0 id =
+ try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+ with Not_found ->
+ errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
+ str " depends on pattern variable name " ++ pr_id id ++
+ str " which is not bound in current context.")
+
+ let pretype_id loc env sigma (lvar,unbndltacvars) id =
(* Look for the binder of [id] *)
try
let (n,_,typ) = lookup_rel_id id (rel_context env) in
@@ -251,7 +257,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
with Not_found ->
(* Check if [id] is an ltac variable *)
try
- List.assoc id lvar
+ let (ids,c) = List.assoc id lvar in
+ let subst = List.map (invert_ltac_bound_name env id) ids in
+ let c = substl subst c in
+ { uj_val = c; uj_type = Retyping.get_type_of env sigma c }
with Not_found ->
(* Check if [id] is a section or goal variable *)
try
@@ -295,7 +304,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
| RVar (loc, id) ->
inh_conv_coerce_to_tycon loc env evdref
- (pretype_id loc env lvar id)
+ (pretype_id loc env !evdref lvar id)
tycon
| REvar (loc, evk, instopt) ->
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 18a6b03a71..00eb613abc 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -6,6 +6,12 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
+(** This file implements type inference. It maps [rawconstr]
+ (i.e. untyped terms whose names are located) to [constr]. In
+ particular, it drives complex pattern-matching problems ("match")
+ into elementary ones, insertion of coercions and resolution of
+ implicit arguments. *)
+
open Names
open Sign
open Term
@@ -21,8 +27,10 @@ val search_guard :
type typing_constraint = OfType of types option | IsType
-type var_map = (identifier * unsafe_judgment) list
+type var_map = (identifier * Pattern.constr_under_binders) list
type unbound_ltac_var_map = (identifier * identifier option) list
+type ltac_var_map = var_map * unbound_ltac_var_map
+type rawconstr_ltac_closure = ltac_var_map * rawconstr
module type S =
sig
@@ -56,7 +64,7 @@ sig
*)
val understand_ltac :
- bool -> evar_map -> env -> var_map * unbound_ltac_var_map ->
+ bool -> evar_map -> env -> ltac_var_map ->
typing_constraint -> rawconstr -> evar_map * constr
(** Standard call to get a constr from a rawconstr, resolving implicit args *)
@@ -84,18 +92,15 @@ sig
(** Internal of Pretyping... *)
val pretype :
type_constraint -> env -> evar_map ref ->
- var_map * (identifier * identifier option) list ->
- rawconstr -> unsafe_judgment
+ ltac_var_map -> rawconstr -> unsafe_judgment
val pretype_type :
val_constraint -> env -> evar_map ref ->
- var_map * (identifier * identifier option) list ->
- rawconstr -> unsafe_type_judgment
+ ltac_var_map -> rawconstr -> unsafe_type_judgment
val pretype_gen :
bool -> bool -> bool -> evar_map ref -> env ->
- var_map * (identifier * identifier option) list ->
- typing_constraint -> rawconstr -> constr
+ ltac_var_map -> typing_constraint -> rawconstr -> constr
(**/**)
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index ca3bd1e802..a8debc6fd6 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -17,7 +17,7 @@ open Rawterm
(** Refinement of existential variables. *)
val w_refine : evar * evar_info ->
- (var_map * unbound_ltac_var_map) * rawconstr -> evar_map -> evar_map
+ rawconstr_ltac_closure -> evar_map -> evar_map
val instantiate_pf_com :
Evd.evar -> Topconstr.constr_expr -> Evd.evar_map -> Evd.evar_map
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 55a73c608b..27b186a82a 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -96,7 +96,7 @@ type ltac_call_kind =
| LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
| LtacVarCall of identifier * glob_tactic_expr
| LtacConstrInterp of rawconstr *
- ((identifier * constr) list * (identifier * identifier option) list)
+ (extended_patvar_map * (identifier * identifier option) list)
type ltac_trace = (int * loc * ltac_call_kind) list
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index b07389ceee..73be0c2b7a 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -126,7 +126,7 @@ type ltac_call_kind =
| LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
| LtacVarCall of identifier * glob_tactic_expr
| LtacConstrInterp of rawconstr *
- ((identifier * constr) list * (identifier * identifier option) list)
+ (extended_patvar_map * (identifier * identifier option) list)
type ltac_trace = (int * loc * ltac_call_kind) list
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 32a199e607..0448b0b224 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -543,7 +543,7 @@ let add_extern pri pat tacast local dbname =
(match (list_subtract tacmetas patmetas) with
| i::_ ->
errorlabstrm "add_extern"
- (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound.")
+ (str "The meta-variable ?" ++ Ppconstr.pr_patvar i ++ str" is not bound.")
| [] ->
Lib.add_anonymous_leaf
(inAutoHint(local,dbname, AddTactic [make_extern pri (Some pat) tacast])))
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index c8e6c9769c..b8552a5aae 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -51,7 +51,7 @@ let instantiate n (ist,rawc) ido gl =
if n <= 0 then error "Incorrect existential variable index.";
let evk,_ = destEvar (List.nth evl (n-1)) in
let evi = Evd.find sigma evk in
- let ltac_vars = Tacinterp.extract_ltac_vars ist sigma (Evd.evar_env evi) in
+ let ltac_vars = Tacinterp.extract_ltac_constr_values ist (Evd.evar_env evi) in
let sigma' = w_refine (evk,evi) (ltac_vars,rawc) sigma in
tclTHEN
(tclEVARS sigma')
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3d5f2ba1bb..72064f4e52 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -81,7 +81,8 @@ type value =
| VIntroPattern of intro_pattern_expr (* includes idents which are not *)
(* bound as in "Intro H" but which may be bound *)
(* later, as in "tac" in "Intro H; tac" *)
- | VConstr of constr (* includes idents known to be bound and references *)
+ | VConstr of constr_under_binders
+ (* includes idents known to be bound and references *)
| VConstr_context of constr
| VList of value list
| VRec of (identifier*value) list ref * glob_tactic_expr
@@ -125,7 +126,10 @@ let rec pr_value env = function
| VVoid -> str "()"
| VInteger n -> int n
| VIntroPattern ipat -> pr_intro_pattern (dloc,ipat)
- | VConstr c | VConstr_context c ->
+ | VConstr c ->
+ (match env with Some env ->
+ pr_lconstr_under_binders_env env c | _ -> str "a term")
+ | VConstr_context c ->
(match env with Some env -> pr_lconstr_env env c | _ -> str "a term")
| (VRTactic _ | VFun _ | VRec _) -> str "a tactic"
| VList [] -> str "an empty list"
@@ -638,10 +642,10 @@ let declare_xml_printer f = print_xml_term := f
let internalise_tacarg ch = G_xml.parse_tactic_arg ch
let extern_tacarg ch env sigma = function
- | VConstr c -> !print_xml_term ch env sigma c
+ | VConstr ([],c) -> !print_xml_term ch env sigma c
| VRTactic _ | VFun _ | VVoid | VInteger _ | VConstr_context _
- | VIntroPattern _ | VRec _ | VList _ ->
- error "Only externing of terms is implemented."
+ | VIntroPattern _ | VRec _ | VList _ | VConstr _ ->
+ error "Only externing of closed terms is implemented."
let extern_request ch req gl la =
output_string ch "<REQUEST req=\""; output_string ch req;
@@ -653,7 +657,7 @@ let value_of_ident id = VIntroPattern (IntroIdentifier id)
let extend_values_with_bindings (ln,lm) lfun =
let lnames = List.map (fun (id,id') ->(id,value_of_ident id')) ln in
- let lmatch = List.map (fun (id,c) -> (id,VConstr c)) lm in
+ let lmatch = List.map (fun (id,(ids,c)) -> (id,VConstr (ids,c))) lm in
(* For compatibility, bound variables are visible only if no other
binding of the same name exists *)
lmatch@lfun@lnames
@@ -988,7 +992,7 @@ and intern_genarg ist x =
(* Evaluation/interpretation *)
let constr_to_id loc = function
- | VConstr c when isVar c -> destVar c
+ | VConstr ([],c) when isVar c -> destVar c
| _ -> invalid_arg_loc (loc, "Not an identifier")
let constr_to_qid loc c =
@@ -1039,7 +1043,7 @@ let interp_ltac_var coerce ist env locid =
(* Interprets an identifier which must be fresh *)
let coerce_to_ident fresh env = function
| VIntroPattern (IntroIdentifier id) -> id
- | VConstr c when isVar c & not (fresh & is_variable env (destVar c)) ->
+ | VConstr ([],c) when isVar c & not (fresh & is_variable env (destVar c)) ->
(* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *)
destVar c
| v -> raise (CannotCoerceTo "a fresh identifier")
@@ -1060,7 +1064,7 @@ let interp_fresh_name ist env = function
let coerce_to_intro_pattern env = function
| VIntroPattern ipat -> ipat
- | VConstr c when isVar c ->
+ | VConstr ([],c) when isVar c ->
(* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
(* but also in "destruct H as (H,H')" *)
IntroIdentifier (destVar c)
@@ -1107,11 +1111,16 @@ let interp_int_or_var_list ist l =
let constr_of_value env = function
| VConstr csr -> csr
- | VIntroPattern (IntroIdentifier id) -> constr_of_id env id
+ | VIntroPattern (IntroIdentifier id) -> ([],constr_of_id env id)
| _ -> raise Not_found
+let closed_constr_of_value env v =
+ let ids,c = constr_of_value env v in
+ if ids <> [] then raise Not_found;
+ c
+
let coerce_to_hyp env = function
- | VConstr c when isVar c -> destVar c
+ | VConstr ([],c) when isVar c -> destVar c
| VIntroPattern (IntroIdentifier id) when is_variable env id -> id
| _ -> raise (CannotCoerceTo "a variable")
@@ -1154,7 +1163,7 @@ let interp_move_location ist gl = function
(* Interprets a qualified name *)
let coerce_to_reference env v =
try match v with
- | VConstr c -> global_of_constr c (* may raise Not_found *)
+ | VConstr ([],c) -> global_of_constr c (* may raise Not_found *)
| _ -> raise Not_found
with Not_found -> raise (CannotCoerceTo "a reference")
@@ -1166,7 +1175,7 @@ let interp_reference ist env = function
let pf_interp_reference ist gl = interp_reference ist (pf_env gl)
let coerce_to_inductive = function
- | VConstr c when isInd c -> destInd c
+ | VConstr ([],c) when isInd c -> destInd c
| _ -> raise (CannotCoerceTo "an inductive type")
let interp_inductive ist = function
@@ -1175,8 +1184,8 @@ let interp_inductive ist = function
let coerce_to_evaluable_ref env v =
let ev = match v with
- | VConstr c when isConst c -> EvalConstRef (destConst c)
- | VConstr c when isVar c -> EvalVarRef (destVar c)
+ | VConstr ([],c) when isConst c -> EvalConstRef (destConst c)
+ | VConstr ([],c) when isVar c -> EvalVarRef (destVar c)
| VIntroPattern (IntroIdentifier id) when List.mem id (ids_of_context env)
-> EvalVarRef id
| _ -> raise (CannotCoerceTo "an evaluable reference")
@@ -1214,18 +1223,18 @@ let interp_clause ist gl { onhyps=ol; concl_occs=occs } =
(* Interpretation of constructions *)
(* Extract the constr list from lfun *)
-let rec constr_list_aux env = function
+let extract_ltac_constr_values ist env =
+ let rec aux = function
| (id,v)::tl ->
- let (l1,l2) = constr_list_aux env tl in
+ let (l1,l2) = aux tl in
(try ((id,constr_of_value env v)::l1,l2)
with Not_found ->
let ido = match v with
| VIntroPattern (IntroIdentifier id0) -> Some id0
| _ -> None in
(l1,(id,ido)::l2))
- | [] -> ([],[])
-
-let constr_list ist env = constr_list_aux env ist.lfun
+ | [] -> ([],[]) in
+ aux ist.lfun
(* Extract the identifier list from lfun: join all branches (what to do else?)*)
let rec intropattern_ids (loc,pat) = match pat with
@@ -1259,20 +1268,6 @@ let interp_fresh_id ist env l =
let pf_interp_fresh_id ist gl = interp_fresh_id ist (pf_env gl)
-(* To retype a list of key*constr with undefined key *)
-let retype_list sigma env lst =
- List.fold_right (fun (x,csr) a ->
- try (x,Retyping.get_judgment_of env sigma csr)::a with
- | Anomaly _ -> a) lst []
-
-let extract_ltac_vars_data ist sigma env =
- let (ltacvars,_ as vars) = constr_list ist env in
- vars, retype_list sigma env ltacvars
-
-let extract_ltac_vars ist sigma env =
- let (_,unbndltacvars),typs = extract_ltac_vars_data ist sigma env in
- typs,unbndltacvars
-
let implicit_tactic = ref None
let declare_implicit_tactic tac = implicit_tactic := Some tac
@@ -1326,8 +1321,7 @@ let solve_remaining_evars fail_evar use_classes env initial_sigma evd c =
!evdref,c
let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma (c,ce) =
- let (ltacvars,unbndltacvars as vars),typs =
- extract_ltac_vars_data ist sigma env in
+ let (ltacvars,unbndltacvars as vars) = extract_ltac_constr_values ist env in
let c = match ce with
| None -> c
(* If at toplevel (ce<>None), the error can be due to an incorrect
@@ -1339,8 +1333,7 @@ let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma
in
let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in
let evd,c =
- catch_error trace
- (understand_ltac expand_evar sigma env (typs,unbndltacvars) kind) c in
+ catch_error trace (understand_ltac expand_evar sigma env vars kind) c in
let evd,c =
if expand_evar then
solve_remaining_evars fail_evar use_classes env sigma evd c
@@ -1378,7 +1371,7 @@ let pf_interp_constr ist gl =
interp_constr ist (pf_env gl) (project gl)
let constr_list_of_VList env = function
- | VList l -> List.map (constr_of_value env) l
+ | VList l -> List.map (closed_constr_of_value env) l
| _ -> raise Not_found
let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
@@ -1484,31 +1477,32 @@ let interp_constr_may_eval ist gl c =
csr
end
-let rec message_of_value = function
+let rec message_of_value gl = function
| VVoid -> str "()"
| VInteger n -> int n
| VIntroPattern ipat -> pr_intro_pattern (dloc,ipat)
- | VConstr_context c | VConstr c -> pr_constr c
+ | VConstr_context c -> pr_constr_env (pf_env gl) c
+ | VConstr c -> pr_constr_under_binders_env (pf_env gl) c
| VRec _ | VRTactic _ | VFun _ -> str "<tactic>"
- | VList l -> prlist_with_sep spc message_of_value l
+ | VList l -> prlist_with_sep spc (message_of_value gl) l
-let rec interp_message_token ist = function
+let rec interp_message_token ist gl = function
| MsgString s -> str s
| MsgInt n -> int n
| MsgIdent (loc,id) ->
let v =
try List.assoc id ist.lfun
with Not_found -> user_err_loc (loc,"",pr_id id ++ str" not found.") in
- message_of_value v
+ message_of_value gl v
-let rec interp_message_nl ist = function
+let rec interp_message_nl ist gl = function
| [] -> mt()
- | l -> prlist_with_sep spc (interp_message_token ist) l ++ fnl()
+ | l -> prlist_with_sep spc (interp_message_token ist gl) l ++ fnl()
-let interp_message ist l =
+let interp_message ist gl l =
(* Force evaluation of interp_message_token so that potential errors
are raised now and not at printing time *)
- prlist (fun x -> spc () ++ x) (List.map (interp_message_token ist) l)
+ prlist (fun x -> spc () ++ x) (List.map (interp_message_token ist gl) l)
let intro_pattern_list_of_Vlist loc env = function
| VList l -> List.map (fun a -> loc,coerce_to_intro_pattern env a) l
@@ -1625,7 +1619,7 @@ let interp_induction_arg ist gl sigma arg =
match List.assoc id ist.lfun with
| VInteger n -> ElimOnAnonHyp n
| VIntroPattern (IntroIdentifier id) -> ElimOnIdent (loc,id)
- | VConstr c -> ElimOnConstr (c,NoBindings)
+ | VConstr ([],c) -> ElimOnConstr (c,NoBindings)
| _ -> user_err_loc (loc,"",
strbrk "Cannot coerce " ++ pr_id id ++
strbrk " neither to a quantified hypothesis nor to a term.")
@@ -1663,8 +1657,7 @@ let eval_pattern lfun ist env sigma (_,pat as c) =
if use_types then
snd (interp_typed_pattern ist env sigma c)
else
- let lvar = List.map (fun (id,c) -> (id,lazy(snd (pattern_of_constr Evd.empty c)))) lfun in
- instantiate_pattern lvar pat
+ instantiate_pattern lfun pat
let read_pattern lfun ist env sigma = function
| Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c)
@@ -1710,18 +1703,22 @@ let is_match_catchable = function
(* different instances of the same metavars is here modulo conversion... *)
let verify_metas_coherence gl (ln1,lcm) (ln,lm) =
let rec aux = function
- | (num,csr)::tl ->
- if (List.for_all (fun (a,b) -> a<>num or pf_conv_x gl b csr) lcm) then
- (num,csr)::aux tl
- else
- raise Not_coherent_metas
+ | (id,(ctx,c) as x)::tl ->
+ if List.for_all
+ (fun (id',(ctx',c')) -> id'<>id or ctx = ctx' & pf_conv_x gl c' c) lcm
+ then
+ x :: aux tl
+ else
+ raise Not_coherent_metas
| [] -> lcm in
(ln@ln1,aux lm)
+let adjust (l,lc) = (l,List.map (fun (id,c) -> (id,([],c))) lc)
+
(* Tries to match one hypothesis pattern with a list of hypotheses *)
let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
let get_id_couple id = function
- | Name idpat -> [idpat,VConstr (mkVar id)]
+ | Name idpat -> [idpat,VConstr ([],mkVar id)]
| Anonymous -> [] in
let match_pat lmatch hyp pat =
match pat with
@@ -1736,11 +1733,11 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
let rec match_next_pattern find_next () =
let (lmeta,ctxt,find_next') = find_next () in
try
- let lmeta = verify_metas_coherence gl lmatch lmeta in
+ let lmeta = verify_metas_coherence gl lmatch (adjust lmeta) in
(give_context ctxt ic,lmeta,match_next_pattern find_next')
with
| Not_coherent_metas -> match_next_pattern find_next' () in
- match_next_pattern(fun () -> match_subterm_gen b t hyp) () in
+ match_next_pattern (fun () -> match_subterm_gen b t hyp) () in
let rec apply_one_mhyp_context_rec = function
| (id,b,hyp as hd)::tl ->
(match patv with
@@ -1782,8 +1779,8 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
(* misc *)
-let mk_constr_value ist gl c = VConstr (pf_interp_constr ist gl c)
-let mk_hyp_value ist gl c = VConstr (mkVar (interp_hyp ist gl c))
+let mk_constr_value ist gl c = VConstr ([],pf_interp_constr ist gl c)
+let mk_hyp_value ist gl c = VConstr ([],mkVar (interp_hyp ist gl c))
let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c)
let pack_sigma (sigma,c) = {it=c;sigma=sigma}
@@ -1826,8 +1823,8 @@ and eval_tactic ist = function
catch_error (push_trace(loc,call)ist.trace) tac gl
| TacFun _ | TacLetIn _ -> assert false
| TacMatchGoal _ | TacMatch _ -> assert false
- | TacId s -> tclIDTAC_MESSAGE (interp_message_nl ist s)
- | TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) (interp_message ist s)
+ | TacId s -> fun gl -> tclIDTAC_MESSAGE (interp_message_nl ist gl s) gl
+ | TacFail (n,s) -> fun gl -> tclFAIL (interp_int_or_var ist n) (interp_message ist gl s) gl
| TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
| TacAbstract (tac,ido) ->
fun gl -> Tactics.tclABSTRACT
@@ -1877,7 +1874,7 @@ and interp_tacarg ist gl = function
| Reference r -> interp_ltac_reference dloc false ist gl r
| Integer n -> VInteger n
| IntroPattern ipat -> VIntroPattern (snd (interp_intro_pattern ist gl ipat))
- | ConstrMayEval c -> VConstr (interp_constr_may_eval ist gl c)
+ | ConstrMayEval c -> VConstr ([],interp_constr_may_eval ist gl c)
| MetaIdArg (loc,_,id) -> assert false
| TacCall (loc,r,[]) -> interp_ltac_reference loc true ist gl r
| TacCall (loc,f,l) ->
@@ -1898,7 +1895,7 @@ and interp_tacarg ist gl = function
else if tg = "value" then
value_out t
else if tg = "constr" then
- VConstr (constr_out t)
+ VConstr ([],constr_out t)
else
anomaly_loc (dloc, "Tacinterp.val_interp",
(str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">"))
@@ -1992,7 +1989,7 @@ and interp_match_goal ist goal lz lr lmr =
let rec match_next_pattern find_next () =
let (lgoal,ctxt,find_next') = find_next () in
let lctxt = give_context ctxt id in
- try apply_hyps_context ist env lz goal mt lctxt lgoal mhyps hyps
+ try apply_hyps_context ist env lz goal mt lctxt (adjust lgoal) mhyps hyps
with e when is_match_catchable e -> match_next_pattern find_next' () in
match_next_pattern (fun () -> match_subterm_gen app c csr) () in
let rec apply_match_goal ist env goal nrs lex lpt =
@@ -2033,7 +2030,8 @@ and interp_match_goal ist goal lz lr lmr =
else mt()) ++ str"."))
end in
apply_match_goal ist env goal 0 lmr
- (read_match_rule (fst (constr_list ist env)) ist env (project goal) lmr)
+ (read_match_rule (fst (extract_ltac_constr_values ist env))
+ ist env (project goal) lmr)
(* Tries to match the hypotheses in a Match Context *)
and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
@@ -2161,7 +2159,7 @@ and interp_match ist g lz constr lmr =
let rec match_next_pattern find_next () =
let (lmatch,ctxt,find_next') = find_next () in
let lctxt = give_context ctxt id in
- let lfun = extend_values_with_bindings lmatch (lctxt@ist.lfun) in
+ let lfun = extend_values_with_bindings (adjust lmatch) (lctxt@ist.lfun) in
try eval_with_fail {ist with lfun=lfun} lz g mt
with e when is_match_catchable e ->
match_next_pattern find_next' () in
@@ -2202,7 +2200,7 @@ and interp_match ist g lz constr lmr =
debugging_exception_step ist true e
(fun () -> str "evaluation of the matched expression");
raise e in
- let ilr = read_match_rule (fst (constr_list ist (pf_env g))) ist (pf_env g) (project g) lmr in
+ let ilr = read_match_rule (fst (extract_ltac_constr_values ist (pf_env g))) ist (pf_env g) (project g) lmr in
let res =
try apply_match ist csr ilr with e ->
debugging_exception_step ist true e (fun () -> str "match expression");
@@ -2223,11 +2221,13 @@ and interp_ltac_constr ist gl e =
let cresult = constr_of_value (pf_env gl) result in
debugging_step ist (fun () ->
Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++
- str " has value " ++ fnl() ++ print_constr_env (pf_env gl) cresult);
- cresult
+ str " has value " ++ fnl() ++
+ pr_constr_under_binders_env (pf_env gl) cresult);
+ if fst cresult <> [] then raise Not_found;
+ snd cresult
with Not_found ->
errorlabstrm ""
- (str "Must evaluate to a term" ++ fnl() ++
+ (str "Must evaluate to a closed term" ++ fnl() ++
str "offending expression: " ++ fnl() ++
Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++ str "this is a " ++
(match result with
@@ -2454,15 +2454,15 @@ and interp_atomic ist gl tac =
| VarArgType ->
mk_hyp_value ist gl (out_gen globwit_var x)
| RefArgType ->
- VConstr (constr_of_global
+ VConstr ([],constr_of_global
(pf_interp_reference ist gl (out_gen globwit_ref x)))
| SortArgType ->
- VConstr (mkSort (interp_sort (out_gen globwit_sort x)))
+ VConstr ([],mkSort (interp_sort (out_gen globwit_sort x)))
| ConstrArgType ->
mk_constr_value ist gl (out_gen globwit_constr x)
| ConstrMayEvalArgType ->
VConstr
- (interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x))
+ ([],interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x))
| ExtraArgType s when tactic_genarg_level s <> None ->
(* Special treatment of tactic arguments *)
val_interp ist gl
@@ -3020,7 +3020,7 @@ let tacticOut = function
let _ = Auto.set_extern_interp
(fun l ->
- let l = List.map (fun (id,c) -> (id,VConstr c)) l in
+ let l = List.map (fun (id,c) -> (id,VConstr ([],c))) l in
interp_tactic {lfun=l;avoid_ids=[];debug=get_debug(); trace=[]})
let _ = Auto.set_extern_intern_tac
(fun l ->
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 7c731e2b9c..5fa9c220d4 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -27,7 +27,7 @@ type value =
| VVoid
| VInteger of int
| VIntroPattern of intro_pattern_expr
- | VConstr of constr
+ | VConstr of Pattern.constr_under_binders
| VConstr_context of constr
| VList of value list
| VRec of (identifier*value) list ref * glob_tactic_expr
@@ -39,8 +39,8 @@ and interp_sign =
debug : debug_info;
trace : ltac_trace }
-val extract_ltac_vars : interp_sign -> Evd.evar_map -> Environ.env ->
- Pretyping.var_map * Pretyping.unbound_ltac_var_map
+val extract_ltac_constr_values : interp_sign -> Environ.env ->
+ Pretyping.ltac_var_map
(** Transforms an id into a constr if possible *)
val constr_of_id : Environ.env -> identifier -> constr
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 2bb225c667..ef0d62285f 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -22,7 +22,7 @@ open Genarg
let assoc_var s ist =
match List.assoc (Names.id_of_string s) ist.lfun with
- | VConstr c -> c
+ | VConstr ([],c) -> c
| _ -> failwith "tauto: anomaly"
(** Parametrization of tauto *)
@@ -114,8 +114,8 @@ let flatten_contravariant_conj ist =
| Some (_,args) ->
let i = List.length args in
if not binary_mode || i = 2 then
- let newtyp = valueIn (VConstr (List.fold_right mkArrow args c)) in
- let hyp = valueIn (VConstr hyp) in
+ let newtyp = valueIn (VConstr ([],List.fold_right mkArrow args c)) in
+ let hyp = valueIn (VConstr ([],hyp)) in
let intros =
iter_tac (List.map (fun _ -> <:tactic< intro >>) args)
<:tactic< idtac >> in
@@ -149,9 +149,9 @@ let flatten_contravariant_disj ist =
| Some (_,args) ->
let i = List.length args in
if not binary_mode || i = 2 then
- let hyp = valueIn (VConstr hyp) in
+ let hyp = valueIn (VConstr ([],hyp)) in
iter_tac (list_map_i (fun i arg ->
- let typ = valueIn (VConstr (mkArrow arg c)) in
+ let typ = valueIn (VConstr ([],mkArrow arg c)) in
<:tactic<
let typ := $typ in
let hyp := $hyp in
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 09d21628b9..dfa41c820a 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -230,3 +230,16 @@ Section LtacLoopTest.
Timeout 1 try f()().
Abort.
End LtacLoopTest.
+
+(* Test binding of open terms *)
+
+Ltac test_open_match z :=
+ match z with
+ (forall y x, ?h = 0) => assert (forall x y, h = x + y)
+ end.
+
+Goal True.
+test_open_match (forall z y, y + z = 0).
+reflexivity.
+apply I.
+Qed.
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 8fcf156084..39c5455899 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -822,14 +822,14 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
| _ -> mt ())
| Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
let filter =
- function (id,None) -> None | (id,Some id') -> Some(id,mkVar id') in
+ function (id,None) -> None | (id,Some id') -> Some(id,([],mkVar id')) in
let unboundvars = list_map_filter filter unboundvars in
quote (pr_rawconstr_env (Global.env()) c) ++
(if unboundvars <> [] or vars <> [] then
strbrk " (with " ++
prlist_with_sep pr_coma
(fun (id,c) ->
- pr_id id ++ str ":=" ++ Printer.pr_lconstr c)
+ pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
(List.rev vars @ unboundvars) ++ str ")"
else mt())) ++
(if n=2 then str " (repeated twice)"
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:49:41 +0000