diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | lib/util.ml | 4 | ||||
| -rw-r--r-- | lib/util.mli | 1 | ||||
| -rw-r--r-- | pretyping/matching.ml | 271 | ||||
| -rw-r--r-- | pretyping/matching.mli | 40 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 234 |
6 files changed, 300 insertions, 253 deletions
@@ -203,6 +203,9 @@ Tactic Language "let ... in ..." into a lazy one. - Patterns for hypotheses types in "match goal" are now interpreted in type_scope. +- A bound variable whose name is not used elsewhere now serves as + metavariable in "match" and it gets instantiated by an identifier + (allow e.g. to extract the name of a statement like "exists x, P x"). Tactics diff --git a/lib/util.ml b/lib/util.ml index ebade654ef..2a60ad7b02 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -626,6 +626,10 @@ let rec list_remove_first a = function | b::l -> b::list_remove_first a l | [] -> raise Not_found +let rec list_remove_assoc_in_triple x = function + | [] -> [] + | (y,_,_ as z)::l -> if x = y then l else z::list_remove_assoc_in_triple x l + let list_add_set x l = if List.mem x l then l else x::l let list_eq_set l1 l2 = diff --git a/lib/util.mli b/lib/util.mli index 7e351e2705..a341fa5a29 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -137,6 +137,7 @@ val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool val list_except : 'a -> 'a list -> 'a list val list_remove : 'a -> 'a list -> 'a list val list_remove_first : 'a -> 'a list -> 'a list +val list_remove_assoc_in_triple : 'a -> ('a * 'b * 'c) list -> ('a * 'b * 'c) list val list_for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool val list_sep_last : 'a list -> 'a * 'a list val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 5162113506..6b3b4e1751 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -44,15 +44,37 @@ open Pattern *) +type bound_ident_map = (identifier * identifier) list + exception PatternMatchingFailure -let constrain (n,m) sigma = - if List.mem_assoc n sigma then - if eq_constr m (List.assoc n sigma) then sigma +let constrain (n,m) (names,terms as subst) = + try + if eq_constr m (List.assoc n terms) then subst else raise PatternMatchingFailure - else - (n,m)::sigma - + with + Not_found -> + if List.mem_assoc n names then + Flags.if_verbose Pp.warning + ("Collision between bound variable "^string_of_id n^ + " and a metavariable of same name."); + (names,(n,m)::terms) + +let add_binders na1 na2 (names,terms as subst) = + match na1, na2 with + | Name id1, Name id2 -> + if List.mem_assoc id1 names then + (Flags.if_verbose Pp.warning + ("Collision between bound variables of name"^string_of_id id1); + (names,terms)) + else + (if List.mem_assoc id1 terms then + Flags.if_verbose Pp.warning + ("Collision between bound variable "^string_of_id id1^ + " and another bound variable of same name."); + ((id1,id2)::names,terms)); + | _ -> subst + let build_lambda toabstract stk (m : constr) = let rec buildrec m p_0 p_1 = match p_0,p_1 with | (_, []) -> m @@ -77,7 +99,10 @@ let same_case_structure (_,cs1,ind,_) ci2 br1 br2 = | None -> cs1 = ci2.ci_cstr_nargs let matches_core convert allow_partial_app pat c = - let rec sorec stk sigma p t = + let conv = match convert with + | None -> eq_constr + | Some (env,sigma) -> is_conv env sigma in + let rec sorec stk subst p t = let cT = strip_outer_cast t in match p,kind_of_term cT with | PSoApp (n,args),m -> @@ -89,7 +114,7 @@ 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) sigma + constrain (n,build_lambda relargs stk cT) subst else raise PatternMatchingFailure @@ -97,66 +122,63 @@ let matches_core convert allow_partial_app pat c = let depth = List.length stk in if depth = 0 then (* Optimisation *) - constrain (n,cT) sigma + 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) sigma + constrain (n,lift (-depth) cT) subst else raise PatternMatchingFailure - | PMeta None, m -> sigma + | PMeta None, m -> subst - | PRef (VarRef v1), Var v2 when v1 = v2 -> sigma + | PRef (VarRef v1), Var v2 when v1 = v2 -> subst - | PVar v1, Var v2 when v1 = v2 -> sigma + | PVar v1, Var v2 when v1 = v2 -> subst - | PRef ref, _ when constr_of_global ref = cT -> sigma + | PRef ref, _ when conv (constr_of_global ref) cT -> subst - | PRel n1, Rel n2 when n1 = n2 -> sigma + | PRel n1, Rel n2 when n1 = n2 -> subst - | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> sigma + | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> subst - | PSort (RType _), Sort (Type _) -> sigma + | PSort (RType _), Sort (Type _) -> subst - | PApp (p, [||]), _ -> sorec stk sigma p t + | PApp (p, [||]), _ -> sorec stk subst p t | PApp (PApp (h, a1), a2), _ -> - sorec stk sigma (PApp(h,Array.append a1 a2)) t + sorec stk subst (PApp(h,Array.append a1 a2)) t | PApp (PMeta (Some n),args1), App (c2,args2) when allow_partial_app -> let p = Array.length args2 - Array.length args1 in if p>=0 then let args21, args22 = array_chop p args2 in - let sigma = + 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) sigma + constrain (n,lift (-depth) c) subst else raise PatternMatchingFailure in - array_fold_left2 (sorec stk) sigma args1 args22 + array_fold_left2 (sorec stk) subst args1 args22 else raise PatternMatchingFailure | PApp (c1,arg1), App (c2,arg2) -> - (try array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2 + (try array_fold_left2 (sorec stk) (sorec stk subst c1 c2) arg1 arg2 with Invalid_argument _ -> raise PatternMatchingFailure) | PProd (na1,c1,d1), Prod(na2,c2,d2) -> - sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2 + sorec ((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 stk sigma c1 c2) d1 d2 + sorec ((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 stk sigma c1 c2) d1 d2 - - | PRef (ConstRef _ as ref), _ when convert <> None -> - let (env,evars) = Option.get convert in - let c = constr_of_global ref in - if is_conv env evars c cT then sigma - else raise PatternMatchingFailure + sorec ((na2,t2)::stk) + (add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2 | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> let ctx,b2 = decompose_lam_n_assum ci.ci_cstr_nargs.(0) b2 in @@ -167,140 +189,129 @@ let matches_core convert allow_partial_app pat c = 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 b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in - sorec s' (sorec s (sorec stk sigma a1 a2) b1 b2) b1' b2' + sorec s' (sorec s (sorec stk subst a1 a2) b1 b2) b1' b2' else raise PatternMatchingFailure | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) -> if same_case_structure ci1 ci2 br1 br2 then array_fold_left2 (sorec stk) - (sorec stk (sorec stk sigma a1 a2) p1 p2) br1 br2 + (sorec stk (sorec stk subst a1 a2) p1 p2) br1 br2 else raise PatternMatchingFailure - | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> sigma - | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> sigma + | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst + | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst | _ -> raise PatternMatchingFailure - in - Sort.list (fun (a,_) (b,_) -> a<b) (sorec [] [] pat c) + in + let names,terms = sorec [] ([],[]) pat c in + (names,Sort.list (fun (a,_) (b,_) -> a<b) terms) -let matches = matches_core None false +let extended_matches = matches_core None false -let pmatches = matches_core None true +let matches c p = snd (matches_core None false c p) -(* To skip to the next occurrence *) -exception NextOccurrence of int +let pmatches c p = snd (matches_core None true c p) + +let special_meta = (-1) (* Tells if it is an authorized occurrence and if the instance is closed *) -let authorized_occ nocc mres = - if not (List.for_all (fun (_,c) -> closed0 c) (fst mres)) then +let authorized_occ sigma mk_ctx next = + if not (List.for_all (fun (_,c) -> closed0 c) (snd sigma)) then raise PatternMatchingFailure; - if nocc = 0 then mres - else raise (NextOccurrence nocc) - -let special_meta = (-1) + sigma, mk_ctx (mkMeta special_meta), next (* Tries to match a subterm of [c] with [pat] *) -let rec sub_match ?(partial_app=false) nocc pat c = +let rec sub_match ?(partial_app=false) pat c = + let rec aux c mk_ctx next = match kind_of_term c with | Cast (c1,k,c2) -> - (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with + (try authorized_occ (extended_matches pat c) mk_ctx next with | PatternMatchingFailure -> - let (lm,lc) = try_sub_match nocc pat [c1] in - (lm,mkCast (List.hd lc, k,c2)) - | NextOccurrence nocc -> - let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in - (lm,mkCast (List.hd lc, k,c2))) - | Lambda (x,c1,c2) -> - (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with + let mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in + try_aux [c1] mk_ctx next) + | Lambda (x,c1,c2) -> + (try authorized_occ (extended_matches pat c) mk_ctx next with | PatternMatchingFailure -> - let (lm,lc) = try_sub_match nocc pat [c1;c2] in - (lm,mkLambda (x,List.hd lc,List.nth lc 1)) - | NextOccurrence nocc -> - let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in - (lm,mkLambda (x,List.hd lc,List.nth lc 1))) + let mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in + try_aux [c1;c2] mk_ctx next) | Prod (x,c1,c2) -> - (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with + (try authorized_occ (extended_matches pat c) mk_ctx next with | PatternMatchingFailure -> - let (lm,lc) = try_sub_match nocc pat [c1;c2] in - (lm,mkProd (x,List.hd lc,List.nth lc 1)) - | NextOccurrence nocc -> - let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in - (lm,mkProd (x,List.hd lc,List.nth lc 1))) - | LetIn (x,c1,t2,c2) -> - (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with + let mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in + try_aux [c1;c2] mk_ctx next) + | LetIn (x,c1,t1,c2) -> + (try authorized_occ (extended_matches pat c) mk_ctx next with | PatternMatchingFailure -> - let (lm,lc) = try_sub_match nocc pat [c1;t2;c2] in - (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2)) - | NextOccurrence nocc -> - let (lm,lc) = try_sub_match (nocc - 1) pat [c1;t2;c2] in - (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2))) + let mk_ctx = function [c1;c2] -> mkLetIn (x,c1,t1,c2) | _ -> assert false + in try_aux [c1;c2] mk_ctx next) | App (c1,lc) -> - let rec aux nocc app args = - match args with - | [] -> - let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in - (lm,mkApp (List.hd le, Array.of_list (List.tl le))) - | arg :: args -> - let app = mkApp (app, [|arg|]) in - try let (lm,ce) = sub_match nocc pat app in - (lm,mkApp (ce, Array.of_list args)) - with NextOccurrence nocc -> - aux nocc app args - in - (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with - | PatternMatchingFailure -> - if partial_app then - aux nocc c1 (Array.to_list lc) - else - let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in - (lm,mkApp (List.hd le, Array.of_list (List.tl le))) - | NextOccurrence nocc -> - if partial_app then - aux nocc c1 (Array.to_list lc) - else - let (lm,le) = try_sub_match (nocc - 1) pat (c1::(Array.to_list lc)) in - (lm,mkApp (List.hd le, Array.of_list (List.tl le)))) + (try authorized_occ (extended_matches pat c) mk_ctx next with + | PatternMatchingFailure -> + let topdown = true in + if partial_app then + if topdown then + let lc1 = Array.sub lc 0 (Array.length lc - 1) in + let app = mkApp (c1,lc1) in + let mk_ctx = function + | [app';c] -> mk_ctx (mkApp (app',[|c|])) + | _ -> assert false in + try_aux [app;array_last lc] mk_ctx next + else + let rec aux2 app args next = + match args with + | [] -> + let mk_ctx le = + mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in + try_aux (c1::Array.to_list lc) mk_ctx next + | arg :: args -> + let app = mkApp (app,[|arg|]) in + let next () = aux2 app args next in + let mk_ctx ce = mk_ctx (mkApp (ce, Array.of_list args)) in + aux app mk_ctx next in + aux2 c1 (Array.to_list lc) next + else + let mk_ctx le = + mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in + try_aux (c1::Array.to_list lc) mk_ctx next) | Case (ci,hd,c1,lc) -> - (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with + (try authorized_occ (extended_matches pat c) mk_ctx next with | PatternMatchingFailure -> - let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in - (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))) - | NextOccurrence nocc -> - let (lm,le) = try_sub_match (nocc - 1) pat (c1::Array.to_list lc) in - (lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le)))) + let mk_ctx le = + mk_ctx (mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))) in + try_aux (c1::Array.to_list lc) mk_ctx next) | Construct _ | Fix _ | Ind _|CoFix _ |Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> - (try authorized_occ nocc ((matches pat c),mkMeta special_meta) with - | PatternMatchingFailure -> raise (NextOccurrence nocc) - | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1))) - -(* Tries [sub_match] for all terms in the list *) -and try_sub_match nocc pat lc = - let rec try_sub_match_rec nocc pat lacc = function - | [] -> raise (NextOccurrence nocc) - | c::tl -> - (try - let (lm,ce) = sub_match nocc pat c in - (lm,lacc@(ce::tl)) - with - | NextOccurrence nocc -> try_sub_match_rec nocc pat (lacc@[c]) tl) in - try_sub_match_rec nocc pat [] lc - -let match_subterm nocc pat c = - try sub_match nocc pat c - with NextOccurrence _ -> raise PatternMatchingFailure - -let match_appsubterm nocc pat c = - try sub_match ~partial_app:true nocc pat c - with NextOccurrence _ -> raise PatternMatchingFailure + (try authorized_occ (extended_matches pat c) mk_ctx next with + | PatternMatchingFailure -> next ()) + + (* Tries [sub_match] for all terms in the list *) + and try_aux lc mk_ctx next = + let rec try_sub_match_rec lacc = function + | [] -> next () + | c::tl -> + let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in + let next () = try_sub_match_rec (c::lacc) tl in + aux c mk_ctx next in + try_sub_match_rec [] lc in + aux c (fun x -> x) (fun () -> raise PatternMatchingFailure) + +type subterm_matching_result = + (bound_ident_map * patvar_map) * constr * (unit -> subterm_matching_result) + +let match_subterm pat c = sub_match pat c + +let match_appsubterm pat c = sub_match ~partial_app:true pat c + +let match_subterm_gen app pat c = sub_match ~partial_app:app pat c let is_matching pat n = try let _ = matches pat n in true with PatternMatchingFailure -> false -let matches_conv env sigma = matches_core (Some (env,sigma)) false +let matches_conv env sigma c p = + snd (matches_core (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 42f9eab122..574a4bbd23 100644 --- a/pretyping/matching.mli +++ b/pretyping/matching.mli @@ -22,36 +22,54 @@ exception PatternMatchingFailure val special_meta : metavariable +type bound_ident_map = (identifier * identifier) list + (* [matches pat c] matches [c] against [pat] and returns the resulting assignment of metavariables; it raises [PatternMatchingFailure] if not matchable; bindings are given in increasing order based on the numbers given in the pattern *) val matches : constr_pattern -> constr -> patvar_map -(* [is_matching pat c] just tells if [c] matches against [pat] *) +(* [extended_matches pat c] also returns the names of bound variables + in [c] that matches the bound variables in [pat]; if several bound + 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 +(* [is_matching pat c] just tells if [c] matches against [pat] *) val is_matching : constr_pattern -> constr -> bool (* [matches_conv env sigma] matches up to conversion in environment [(env,sigma)] when constants in pattern are concerned; it raises [PatternMatchingFailure] if not matchable; bindings are given in increasing order based on the numbers given in the pattern *) - val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map +(* The type of subterm matching results: a substitution + a context + (whose hole is denoted with [special_meta]) + a continuation that + either returns the next matching subterm or raise PatternMatchingFailure *) +type subterm_matching_result = + (bound_ident_map * patvar_map) * constr * (unit -> subterm_matching_result) + (* [match_subterm n pat c] returns the substitution and the context - corresponding to the [n+1]th **closed** subterm of [c] matching [pat]; - It raises PatternMatchingFailure if no such matching exists *) -val match_subterm : int -> constr_pattern -> constr -> patvar_map * constr + corresponding to the first **closed** subterm of [c] matching [pat], and + a continuation that looks for the next matching subterm. + It raises PatternMatchingFailure if no subterm matches the pattern *) +val match_subterm : constr_pattern -> constr -> subterm_matching_result + +(* [match_appsubterm pat c] returns the substitution and the context + corresponding to the first **closed** subterm of [c] matching [pat], + considering application contexts as well. It also returns a + continuation that looks for the next matching subterm. + It raises PatternMatchingFailure if no subterm matches the pattern *) +val match_appsubterm : constr_pattern -> constr -> subterm_matching_result -(* [match_appsubterm n pat c] returns the substitution and the context - corresponding to the [n+1]th **closed** subterm of [c] matching [pat], - considering application contexts as well; - It raises PatternMatchingFailure if no such matching exists *) -val match_appsubterm : int -> constr_pattern -> constr -> patvar_map * constr +(* [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *) +val match_subterm_gen : bool (* true = with app context *) -> + constr_pattern -> constr -> subterm_matching_result (* [is_matching_conv env sigma pat c] tells if [c] matches against [pat] up to conversion for constants in patterns *) - val is_matching_conv : env -> Evd.evar_map -> constr_pattern -> constr -> bool diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 897c8fd982..fc3673e6f4 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -649,6 +649,15 @@ let extern_request ch req gl la = List.iter (pf_apply (extern_tacarg ch) gl) la; output_string ch "</REQUEST>\n" +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 + (* For compatibility, bound variables are visible only if no other + binding of the same name exists *) + lmatch@lfun@lnames + (* Reads the hypotheses of a Match Context rule *) let rec intern_match_context_hyps sigma env lfun = function | (Hyp ((_,na) as locna,mp))::tl -> @@ -1042,77 +1051,79 @@ let is_match_catchable = function | e -> Logic.catchable_exception e (* Verifies if the matched list is coherent with respect to lcm *) -let rec verify_metas_coherence gl lcm = function +(* While non-linear matching is modulo eq_constr in matches, merge of *) +(* 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)::(verify_metas_coherence gl lcm tl) + (num,csr)::aux tl else raise Not_coherent_metas - | [] -> [] - -type match_result = - | Matches of (Names.identifier * value) list * (Rawterm.patvar * Term.constr) list * - (int * bool) - | Fail of int * bool + | [] -> lcm in + (ln@ln1,aux lm) (* Tries to match one hypothesis pattern with a list of hypotheses *) -let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) (lhyps,nocc) = +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)] | Anonymous -> [] in - let match_pat lmatch nocc id hyp pat = + let match_pat lmatch hyp pat = match pat with | Term t -> + let lmeta = extended_matches t hyp in (try - let lmeta = verify_metas_coherence gl lmatch (matches t hyp) in - Matches ([],lmeta,(0, true)) + let lmeta = verify_metas_coherence gl lmatch lmeta in + ([],lmeta,(fun () -> raise PatternMatchingFailure)) with - | PatternMatchingFailure | Not_coherent_metas -> - Fail (0, true)) + | Not_coherent_metas -> raise PatternMatchingFailure); | Subterm (b,ic,t) -> - (try - let (lm,ctxt) = - if b then match_appsubterm nocc t hyp else match_subterm nocc t hyp - in - let lmeta = verify_metas_coherence gl lmatch lm in - Matches - (give_context ctxt ic,lmeta,(nocc + 1,false)) + 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 + (give_context ctxt ic,lmeta,match_next_pattern find_next') with - | PatternMatchingFailure -> - Fail (0, true) - | Not_coherent_metas -> - Fail (nocc + 1, false)) - in - let rec apply_one_mhyp_context_rec nocc = function - | (id,b,hyp as hd)::tl as hyps -> + | Not_coherent_metas -> match_next_pattern find_next' () 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 - | None -> - (match match_pat lmatch nocc id hyp pat with - | Matches (ids, lmeta, (nocc, cont)) -> - (get_id_couple id hypname@ids, - lmeta,hd,((if cont then tl else hyps),nocc)) - | Fail (nocc, cont) -> - apply_one_mhyp_context_rec nocc (if cont then tl else hyps)) + | None -> + let rec match_next_pattern find_next () = + try + let (ids, lmeta, find_next') = find_next () in + (get_id_couple id hypname@ids, lmeta, hd, + match_next_pattern find_next') + with + | PatternMatchingFailure -> apply_one_mhyp_context_rec tl in + match_next_pattern (fun () -> match_pat lmatch hyp pat) () | Some patv -> - (match b with + match b with | Some body -> - (match match_pat lmatch nocc id body patv with - | Matches (ids, lmeta, (noccv, cont)) -> - (match match_pat (lmatch@lmeta) nocc id hyp pat with - | Matches (ids', lmeta', (nocc', cont')) -> - (get_id_couple id hypname@ids@ids', - lmeta@lmeta',hd,((if cont || cont' then tl else hyps),nocc')) - | Fail (nocc, cont) -> - apply_one_mhyp_context_rec nocc (if cont then tl else hyps)) - | Fail (nocc, cont) -> - apply_one_mhyp_context_rec nocc (if cont then tl else hyps)) - | None -> - apply_one_mhyp_context_rec nocc tl)) + let rec match_next_pattern_in_body next_in_body () = + try + let (ids,lmeta,next_in_body') = next_in_body() in + let rec match_next_pattern_in_typ next_in_typ () = + try + let (ids',lmeta',next_in_typ') = next_in_typ() in + (get_id_couple id hypname@ids@ids', lmeta', hd, + match_next_pattern_in_typ next_in_typ') + with + | PatternMatchingFailure -> + match_next_pattern_in_body next_in_body' () in + match_next_pattern_in_typ + (fun () -> match_pat lmeta hyp pat) () + with PatternMatchingFailure -> apply_one_mhyp_context_rec tl + in + match_next_pattern_in_body + (fun () -> match_pat lmatch body patv) () + | None -> apply_one_mhyp_context_rec tl) | [] -> db_hyp_pattern_failure ist.debug env (hypname,pat); raise PatternMatchingFailure in - apply_one_mhyp_context_rec nocc lhyps + apply_one_mhyp_context_rec lhyps let constr_to_id loc = function | VConstr c when isVar c -> destVar c @@ -1861,14 +1872,18 @@ and interp_letin ist gl llc u = val_interp ist gl u (* Interprets the Match Context expressions *) -and interp_match_context ist g lz lr lmr = - let rec apply_goal_sub app ist env goal nocc (id,c) csr mt mhyps hyps = - let (lgoal,ctxt) = if app then match_appsubterm nocc c csr - else match_subterm nocc c csr in - let lctxt = give_context ctxt id in +and interp_match_context ist goal lz lr lmr = + let hyps = pf_hyps goal in + let hyps = if lr then List.rev hyps else hyps in + let concl = pf_concl goal in + let env = pf_env goal in + let rec apply_goal_sub app ist (id,c) csr mt mhyps hyps = + 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 - with e when is_match_catchable e -> - apply_goal_sub app ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in + 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_context ist env goal nrs lex lpt = begin if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex); @@ -1881,27 +1896,24 @@ and interp_match_context ist g lz lr lmr = apply_match_context ist env goal (nrs+1) (List.tl lex) tl end | (Pat (mhyps,mgoal,mt))::tl -> - let hyps = pf_hyps goal in - let hyps = if lr then List.rev hyps else hyps in - let mhyps = List.rev mhyps (* Sens naturel *) in - let concl = pf_concl goal in - (match mgoal with - | Term mg -> - (try - let lgoal = matches mg concl in - db_matched_concl ist.debug (pf_env goal) concl; - apply_hyps_context ist env lz goal mt [] lgoal mhyps hyps - with e when is_match_catchable e -> - (match e with - | PatternMatchingFailure -> db_matching_failure ist.debug - | Eval_fail s -> db_eval_failure ist.debug s - | _ -> db_logic_failure ist.debug e); - apply_match_context ist env goal (nrs+1) (List.tl lex) tl) - | Subterm (b,id,mg) -> - (try apply_goal_sub b ist env goal 0 (id,mg) concl mt mhyps hyps - with - | PatternMatchingFailure -> - apply_match_context ist env goal (nrs+1) (List.tl lex) tl)) + let mhyps = List.rev mhyps (* Sens naturel *) in + (match mgoal with + | Term mg -> + (try + let lmatch = extended_matches mg concl in + db_matched_concl ist.debug env concl; + apply_hyps_context ist env lz goal mt [] lmatch mhyps hyps + with e when is_match_catchable e -> + (match e with + | PatternMatchingFailure -> db_matching_failure ist.debug + | Eval_fail s -> db_eval_failure ist.debug s + | _ -> db_logic_failure ist.debug e); + apply_match_context ist env goal (nrs+1) (List.tl lex) tl) + | Subterm (b,id,mg) -> + (try apply_goal_sub b ist (id,mg) concl mt mhyps hyps + with + | PatternMatchingFailure -> + apply_match_context ist env goal (nrs+1) (List.tl lex) tl)) | _ -> errorlabstrm "Tacinterp.apply_match_context" (v 0 (str "No matching clauses for match goal" ++ @@ -1909,36 +1921,36 @@ and interp_match_context ist g lz lr lmr = fnl() ++ str "(use \"Set Ltac Debug\" for more info)" else mt()))) end in - let env = pf_env g in - apply_match_context ist env g 0 lmr + apply_match_context ist env goal 0 lmr (read_match_rule (fst (constr_list ist env)) lmr) (* Tries to match the hypotheses in a Match Context *) and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps = - let rec apply_hyps_context_rec lfun lmatch lhyps_rest current = function - | hyp::tl as mhyps -> - let (hypname, mbod, mhyp) = - match hyp with - | Hyp ((_,hypname),mhyp) -> hypname, None, mhyp + let rec apply_hyps_context_rec lfun lmatch lhyps_rest = function + | hyp_pat::tl -> + let (hypname, _, _ as hyp_pat) = + match hyp_pat with + | Hyp ((_,hypname),mhyp) -> hypname, None, mhyp | Def ((_,hypname),mbod,mhyp) -> hypname, Some mbod, mhyp in - let (lids,lm,hyp_match,next) = - apply_one_mhyp_context ist env goal lmatch (hypname,mbod,mhyp) current in - db_matched_hyp ist.debug (pf_env goal) hyp_match hypname; - begin + let rec match_next_pattern find_next = + let (lids,lm,hyp_match,find_next') = find_next () in + db_matched_hyp ist.debug (pf_env goal) hyp_match hypname; try - let nextlhyps = list_except hyp_match lhyps_rest in - apply_hyps_context_rec (lfun@lids) (lmatch@lm) nextlhyps - (nextlhyps,0) tl + let id_match = pi1 hyp_match in + let nextlhyps = list_remove_assoc_in_triple id_match lhyps_rest in + apply_hyps_context_rec (lfun@lids) lm nextlhyps tl with e when is_match_catchable e -> - apply_hyps_context_rec lfun lmatch lhyps_rest next mhyps - end + match_next_pattern find_next' in + let init_match_pattern () = + apply_one_mhyp_context ist env goal lmatch hyp_pat lhyps_rest in + match_next_pattern init_match_pattern | [] -> - let lmatch = List.map (fun (id,c) -> (id,VConstr c)) lmatch in + let lfun = extend_values_with_bindings lmatch (lfun@ist.lfun) in db_mc_pattern_success ist.debug; - eval_with_fail {ist with lfun=lmatch@lfun@ist.lfun} lz goal mt + eval_with_fail {ist with lfun=lfun} lz goal mt in - apply_hyps_context_rec lctxt lgmatch hyps (hyps,0) mhyps + apply_hyps_context_rec lctxt lgmatch hyps mhyps and interp_external loc ist gl com req la = let f ch = extern_request ch req gl la in @@ -2030,33 +2042,31 @@ and interp_genarg_var_list1 ist gl x = (* Interprets the Match expressions *) and interp_match ist g lz constr lmr = - let rec apply_match_subterm app ist nocc (id,c) csr mt = - let (lm,ctxt) = - if app then match_appsubterm nocc c csr - else match_subterm nocc c csr - in - let lctxt = give_context ctxt id in - let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in - try eval_with_fail {ist with lfun=lm@lctxt@ist.lfun} lz g mt - with e when is_match_catchable e -> - apply_match_subterm app ist (nocc + 1) (id,c) csr mt - in + let rec apply_match_subterm app ist (id,c) csr mt = + 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 + try eval_with_fail {ist with lfun=lfun} lz g mt + 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 ist csr = function | (All t)::_ -> (try eval_with_fail ist lz g t with e when is_match_catchable e -> apply_match ist csr []) | (Pat ([],Term c,mt))::tl -> (try - let lm = - try matches c csr + let lmatch = + try extended_matches c csr with e -> debugging_exception_step ist false e (fun () -> str "matching with pattern" ++ fnl () ++ pr_constr_pattern_env (pf_env g) c); raise e in try - let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in - eval_with_fail { ist with lfun=lm@ist.lfun } lz g mt + let lfun = extend_values_with_bindings lmatch ist.lfun in + eval_with_fail { ist with lfun=lfun } lz g mt with e -> debugging_exception_step ist false e (fun () -> str "rule body for pattern" ++ @@ -2067,7 +2077,7 @@ and interp_match ist g lz constr lmr = apply_match ist csr tl) | (Pat ([],Subterm (b,id,c),mt))::tl -> - (try apply_match_subterm b ist 0 (id,c) csr mt + (try apply_match_subterm b ist (id,c) csr mt with PatternMatchingFailure -> apply_match ist csr tl) | _ -> errorlabstrm "Tacinterp.apply_match" (str |