From 0d8a11017e45ff9b0b18af1d6cd69c66184b55ae Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 2 Mar 2014 14:17:09 +0100 Subject: Matching --> ConstrMatching (was clashing with OCaml's compiler-libs) There are currently two other clashs : Lexer and Errors, but for the moment these ones haven't impacted my experiments with extraction and compiler-libs, while this Matching issue had. And anyway the new name is more descriptive, in the spirit of the recent TacticMatching. --- dev/printers.mllib | 2 +- plugins/quote/quote.ml | 2 +- pretyping/constrMatching.ml | 409 ++++++++++++++++++++++++++++++++++++++++++ pretyping/constrMatching.mli | 86 +++++++++ pretyping/matching.ml | 410 ------------------------------------------- pretyping/matching.mli | 86 --------- pretyping/pretyping.mllib | 2 +- pretyping/tacred.ml | 10 +- proofs/tacmach.ml | 4 +- tactics/auto.ml | 11 +- tactics/eqdecide.ml4 | 2 +- tactics/equality.ml | 19 +- tactics/hipattern.ml4 | 2 +- tactics/tacinterp.ml | 3 +- tactics/tacticMatching.ml | 16 +- tactics/tacticMatching.mli | 2 +- tactics/tactics.ml | 2 +- toplevel/search.ml | 11 +- 18 files changed, 539 insertions(+), 540 deletions(-) create mode 100644 pretyping/constrMatching.ml create mode 100644 pretyping/constrMatching.mli delete mode 100644 pretyping/matching.ml delete mode 100644 pretyping/matching.mli diff --git a/dev/printers.mllib b/dev/printers.mllib index 82ef43a7d5..30ac772d0a 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -118,7 +118,7 @@ Evarconv Arguments_renaming Typing Patternops -Matching +ConstrMatching Tacred Classops Typeclasses_errors diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 21b221318e..affe31d790 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -107,7 +107,7 @@ open Names open Term open Pattern open Patternops -open Matching +open ConstrMatching open Tacmach open Proofview.Notations (*i*) diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml new file mode 100644 index 0000000000..45b097c003 --- /dev/null +++ b/pretyping/constrMatching.ml @@ -0,0 +1,409 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + let () = if Id.Map.mem n names then warn_bound_meta n in + (names, Id.Map.add n x terms) + +let add_binders na1 na2 (names, terms as subst) = match na1, na2 with +| Name id1, Name id2 -> + if Id.Map.mem id1 names then + let () = warn_bound_bound id1 in + (names, terms) + else + let names = Id.Map.add id1 id2 names in + let () = if Id.Map.mem id1 terms then warn_bound_again id1 in + (names, terms) +| _ -> subst + +let build_lambda toabstract stk (m : constr) = + let rec buildrec m k stk = match stk with + | [] -> m + | (_, na, t) :: tl -> + if Int.Set.mem k toabstract then + buildrec (mkLambda (na, t, m)) (k + 1) tl + else + buildrec (lift (-1) m) (k + 1) tl + in + buildrec m 1 stk + +let rec extract_bound_aux k accu frels stk = match stk with +| [] -> accu +| (na1, na2, _) :: stk -> + if Int.Set.mem k frels then + begin match na1 with + | Name id -> + let () = assert (match na2 with Anonymous -> false | Name _ -> true) in + let () = if Id.Set.mem id accu then raise PatternMatchingFailure in + extract_bound_aux (k + 1) (Id.Set.add id accu) frels stk + | Anonymous -> raise PatternMatchingFailure + end + else extract_bound_aux (k + 1) accu frels stk + +let extract_bound_vars frels stk = + extract_bound_aux 1 Id.Set.empty frels stk + +let dummy_constr = mkProp + +let make_renaming ids = function +| (Name id, Name _, _) -> + begin + try mkRel (List.index Id.equal id ids) + with Not_found -> dummy_constr + end +| _ -> dummy_constr + +let merge_binding allow_bound_rels stk n cT subst = + let c = match stk with + | [] -> (* Optimization *) + ([], cT) + | _ -> + let frels = free_rels cT in + if allow_bound_rels then + let vars = extract_bound_vars frels stk in + let ordered_vars = Id.Set.elements vars in + let rename binding = make_renaming ordered_vars binding in + let renaming = List.map rename stk in + (ordered_vars, substl renaming cT) + else + let depth = List.length stk in + let min_elt = try Int.Set.min_elt frels with Not_found -> succ depth in + if depth < min_elt 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 + 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 -> + let fold accu = function + | PRel n -> Int.Set.add n accu + | _ -> error "Only bound indices allowed in second order pattern matching." + in + let relargs = List.fold_left fold Int.Set.empty args in + let frels = free_rels cT in + if Int.Set.subset frels relargs then + constrain n ([], build_lambda relargs stk cT) subst + else + raise PatternMatchingFailure + + | PMeta (Some n), m -> merge_binding allow_bound_rels stk n cT subst + + | PMeta None, m -> subst + + | PRef (VarRef v1), Var v2 when Id.equal v1 v2 -> subst + + | PVar v1, Var v2 when Id.equal v1 v2 -> subst + + | PRef ref, _ when conv (constr_of_global ref) cT -> subst + + | PRel n1, Rel n2 when Int.equal n1 n2 -> subst + + | PSort GProp, Sort (Prop Null) -> subst + + | PSort GSet, Sort (Prop Pos) -> subst + + | PSort (GType _), Sort (Type _) -> subst + + | PApp (p, [||]), _ -> sorec stk subst p t + + | PApp (PApp (h, a1), a2), _ -> + sorec stk subst (PApp(h,Array.append a1 a2)) t + + | PApp (PMeta meta,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 c = mkApp(c2,args21) in + let subst = + match meta with + | None -> subst + | Some n -> merge_binding allow_bound_rels stk n c subst in + 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 subst c1 c2) arg1 arg2 + with Invalid_argument _ -> raise PatternMatchingFailure) + + | PProd (na1,c1,d1), Prod(na2,c2,d2) -> + 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 ((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 ((na1,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_ndecls.(0) b2 in + let ctx',b2' = decompose_lam_n_assum ci.ci_cstr_ndecls.(1) b2' in + 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) -> (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 + raise PatternMatchingFailure + + | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) -> + let n2 = Array.length br2 in + let () = match ci1.cip_ind with + | None -> () + | Some ind1 -> + (** ppedrot: Something spooky going here. The comparison used to be + the generic one, so I may have broken something. *) + if not (eq_ind ind1 ci2.ci_ind) then raise PatternMatchingFailure + in + let () = + if not ci1.cip_extensible && not (Int.equal (List.length br1) n2) + then raise PatternMatchingFailure + in + let chk_branch subst (j,n,c) = + (* (ind,j+1) is normally known to be a correct constructor + and br2 a correct match over the same inductive *) + assert (j < n2); + sorec stk subst c br2.(j) + in + let chk_head = sorec stk (sorec stk subst a1 a2) p1 p2 in + List.fold_left chk_branch chk_head br1 + + | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst + | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst + | _ -> raise PatternMatchingFailure + + in + sorec [] (Id.Map.empty, Id.Map.empty) pat c + +let matches_core_closed convert allow_partial_app pat c = + let names, subst = matches_core convert allow_partial_app false pat c in + (names, Id.Map.map snd subst) + +let extended_matches = matches_core None true true + +let matches pat c = snd (matches_core_closed None true pat c) + +let special_meta = (-1) + +type matching_result = + { m_sub : bound_ident_map * patvar_map; + m_ctx : constr; } + +let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) ) + +let isPMeta = function PMeta _ -> true | _ -> false + +let matches_head pat c = + let head = + match pat, kind_of_term c with + | PApp (c1,arg1), App (c2,arg2) -> + if isPMeta c1 then c else + let n1 = Array.length arg1 in + if n1 < Array.length arg2 then mkApp (c2,Array.sub arg2 0 n1) else c + | c1, App (c2,arg2) when not (isPMeta c1) -> c2 + | _ -> c in + matches pat head + +(* 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_closed None partial_app pat c in + if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd sigma) + then next () + else mkresult sigma (mk_ctx (mkMeta special_meta)) next + with PatternMatchingFailure -> next () + +(* Tries to match a subterm of [c] with [pat] *) +let sub_match ?(partial_app=false) ?(closed=true) pat c = + let rec aux c mk_ctx next = + match kind_of_term c with + | Cast (c1,k,c2) -> + let next_mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in + let next () = try_aux [c1] next_mk_ctx next in + authorized_occ partial_app closed pat c mk_ctx next + | Lambda (x,c1,c2) -> + let next_mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in + let next () = try_aux [c1;c2] next_mk_ctx next in + authorized_occ partial_app closed pat c mk_ctx next + | Prod (x,c1,c2) -> + let next_mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in + let next () = try_aux [c1;c2] next_mk_ctx next in + authorized_occ partial_app closed pat c mk_ctx next + | LetIn (x,c1,t,c2) -> + let next_mk_ctx = function + | [c1;c2] -> mkLetIn (x,c1,t,c2) + | _ -> assert false + in + let next () = try_aux [c1;c2] next_mk_ctx next in + authorized_occ partial_app closed pat c mk_ctx next + | App (c1,lc) -> + let next () = + 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 + in + authorized_occ partial_app closed pat c mk_ctx next + | Case (ci,hd,c1,lc) -> + let next_mk_ctx = function + | [] -> assert false + | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) + in + let next () = try_aux (c1 :: Array.to_list lc) next_mk_ctx next in + authorized_occ partial_app closed pat c mk_ctx next + | Fix (indx,(names,types,bodies)) -> + let nb_fix = Array.length types in + let next_mk_ctx le = + let (ntypes,nbodies) = CList.chop nb_fix le in + mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in + let next () = + try_aux + ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in + authorized_occ partial_app closed pat c mk_ctx next + | CoFix (i,(names,types,bodies)) -> + let nb_fix = Array.length types in + let next_mk_ctx le = + let (ntypes,nbodies) = CList.chop nb_fix le in + mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in + let next () = + try_aux ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in + authorized_occ partial_app closed pat c mk_ctx next + | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> + authorized_occ partial_app closed pat c mk_ctx 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 + let lempty () = IStream.Nil in + let result () = aux c (fun x -> x) lempty in + IStream.thunk 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 c = + try let _ = matches pat c in true + with PatternMatchingFailure -> false + +let is_matching_head pat c = + try let _ = matches_head pat c in true + with PatternMatchingFailure -> false + +let is_matching_appsubterm ?(closed=true) pat c = + let results = sub_match ~partial_app:true ~closed pat c in + not (IStream.is_empty results) + +let matches_conv env sigma 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 + with PatternMatchingFailure -> false diff --git a/pretyping/constrMatching.mli b/pretyping/constrMatching.mli new file mode 100644 index 0000000000..b82f115251 --- /dev/null +++ b/pretyping/constrMatching.mli @@ -0,0 +1,86 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* constr -> patvar_map + +(** [matches_head pat c] does the same as [matches pat c] but accepts + [pat] to match an applicative prefix of [c] *) +val matches_head : constr_pattern -> constr -> patvar_map + +(** [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 * extended_patvar_map + +(** [is_matching pat c] just tells if [c] matches against [pat] *) +val is_matching : constr_pattern -> constr -> bool + +(** [is_matching_head pat c] just tells if [c] or an applicative + prefix of it matches against [pat] *) +val is_matching_head : 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 here with [special_meta]) *) +type matching_result = + { m_sub : bound_ident_map * patvar_map; + m_ctx : constr } + +(** [match_subterm n pat c] returns the substitution and the context + corresponding to each **closed** subterm of [c] matching [pat]. *) +val match_subterm : constr_pattern -> constr -> matching_result IStream.t + +(** [match_appsubterm pat c] returns the substitution and the context + corresponding to each **closed** subterm of [c] matching [pat], + considering application contexts as well. *) +val match_appsubterm : constr_pattern -> constr -> matching_result IStream.t + +(** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *) +val match_subterm_gen : bool (** true = with app context *) -> + constr_pattern -> constr -> matching_result IStream.t + +(** [is_matching_appsubterm pat c] tells if a subterm of [c] matches + against [pat] taking partial subterms into consideration *) +val is_matching_appsubterm : ?closed:bool -> constr_pattern -> constr -> bool + +(** [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/pretyping/matching.ml b/pretyping/matching.ml deleted file mode 100644 index 0d3f249281..0000000000 --- a/pretyping/matching.ml +++ /dev/null @@ -1,410 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let () = if Id.Map.mem n names then warn_bound_meta n in - (names, Id.Map.add n x terms) - -let add_binders na1 na2 (names, terms as subst) = match na1, na2 with -| Name id1, Name id2 -> - if Id.Map.mem id1 names then - let () = warn_bound_bound id1 in - (names, terms) - else - let names = Id.Map.add id1 id2 names in - let () = if Id.Map.mem id1 terms then warn_bound_again id1 in - (names, terms) -| _ -> subst - -let build_lambda toabstract stk (m : constr) = - let rec buildrec m k stk = match stk with - | [] -> m - | (_, na, t) :: tl -> - if Int.Set.mem k toabstract then - buildrec (mkLambda (na, t, m)) (k + 1) tl - else - buildrec (lift (-1) m) (k + 1) tl - in - buildrec m 1 stk - -let rec extract_bound_aux k accu frels stk = match stk with -| [] -> accu -| (na1, na2, _) :: stk -> - if Int.Set.mem k frels then - begin match na1 with - | Name id -> - let () = assert (match na2 with Anonymous -> false | Name _ -> true) in - let () = if Id.Set.mem id accu then raise PatternMatchingFailure in - extract_bound_aux (k + 1) (Id.Set.add id accu) frels stk - | Anonymous -> raise PatternMatchingFailure - end - else extract_bound_aux (k + 1) accu frels stk - -let extract_bound_vars frels stk = - extract_bound_aux 1 Id.Set.empty frels stk - -let dummy_constr = mkProp - -let make_renaming ids = function -| (Name id, Name _, _) -> - begin - try mkRel (List.index Id.equal id ids) - with Not_found -> dummy_constr - end -| _ -> dummy_constr - -let merge_binding allow_bound_rels stk n cT subst = - let c = match stk with - | [] -> (* Optimization *) - ([], cT) - | _ -> - let frels = free_rels cT in - if allow_bound_rels then - let vars = extract_bound_vars frels stk in - let ordered_vars = Id.Set.elements vars in - let rename binding = make_renaming ordered_vars binding in - let renaming = List.map rename stk in - (ordered_vars, substl renaming cT) - else - let depth = List.length stk in - let min_elt = try Int.Set.min_elt frels with Not_found -> succ depth in - if depth < min_elt 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 - 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 -> - let fold accu = function - | PRel n -> Int.Set.add n accu - | _ -> error "Only bound indices allowed in second order pattern matching." - in - let relargs = List.fold_left fold Int.Set.empty args in - let frels = free_rels cT in - if Int.Set.subset frels relargs then - constrain n ([], build_lambda relargs stk cT) subst - else - raise PatternMatchingFailure - - | PMeta (Some n), m -> merge_binding allow_bound_rels stk n cT subst - - | PMeta None, m -> subst - - | PRef (VarRef v1), Var v2 when Id.equal v1 v2 -> subst - - | PVar v1, Var v2 when Id.equal v1 v2 -> subst - - | PRef ref, _ when conv (constr_of_global ref) cT -> subst - - | PRel n1, Rel n2 when Int.equal n1 n2 -> subst - - | PSort GProp, Sort (Prop Null) -> subst - - | PSort GSet, Sort (Prop Pos) -> subst - - | PSort (GType _), Sort (Type _) -> subst - - | PApp (p, [||]), _ -> sorec stk subst p t - - | PApp (PApp (h, a1), a2), _ -> - sorec stk subst (PApp(h,Array.append a1 a2)) t - - | PApp (PMeta meta,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 c = mkApp(c2,args21) in - let subst = - match meta with - | None -> subst - | Some n -> merge_binding allow_bound_rels stk n c subst in - 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 subst c1 c2) arg1 arg2 - with Invalid_argument _ -> raise PatternMatchingFailure) - - | PProd (na1,c1,d1), Prod(na2,c2,d2) -> - 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 ((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 ((na1,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_ndecls.(0) b2 in - let ctx',b2' = decompose_lam_n_assum ci.ci_cstr_ndecls.(1) b2' in - 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) -> (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 - raise PatternMatchingFailure - - | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) -> - let n2 = Array.length br2 in - let () = match ci1.cip_ind with - | None -> () - | Some ind1 -> - (** ppedrot: Something spooky going here. The comparison used to be - the generic one, so I may have broken something. *) - if not (eq_ind ind1 ci2.ci_ind) then raise PatternMatchingFailure - in - let () = - if not ci1.cip_extensible && not (Int.equal (List.length br1) n2) - then raise PatternMatchingFailure - in - let chk_branch subst (j,n,c) = - (* (ind,j+1) is normally known to be a correct constructor - and br2 a correct match over the same inductive *) - assert (j < n2); - sorec stk subst c br2.(j) - in - let chk_head = sorec stk (sorec stk subst a1 a2) p1 p2 in - List.fold_left chk_branch chk_head br1 - - | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst - | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst - | _ -> raise PatternMatchingFailure - - in - sorec [] (Id.Map.empty, Id.Map.empty) pat c - -let matches_core_closed convert allow_partial_app pat c = - let names, subst = matches_core convert allow_partial_app false pat c in - (names, Id.Map.map snd subst) - -let extended_matches = matches_core None true true - -let matches pat c = snd (matches_core_closed None true pat c) - -let special_meta = (-1) - -type matching_result = - { m_sub : bound_ident_map * patvar_map; - m_ctx : constr; } - -let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) ) - -let isPMeta = function PMeta _ -> true | _ -> false - -let matches_head pat c = - let head = - match pat, kind_of_term c with - | PApp (c1,arg1), App (c2,arg2) -> - if isPMeta c1 then c else - let n1 = Array.length arg1 in - if n1 < Array.length arg2 then mkApp (c2,Array.sub arg2 0 n1) else c - | c1, App (c2,arg2) when not (isPMeta c1) -> c2 - | _ -> c in - matches pat head - -(* 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_closed None partial_app pat c in - if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd sigma) - then next () - else mkresult sigma (mk_ctx (mkMeta special_meta)) next - with PatternMatchingFailure -> next () - -(* Tries to match a subterm of [c] with [pat] *) -let sub_match ?(partial_app=false) ?(closed=true) pat c = - let rec aux c mk_ctx next = - match kind_of_term c with - | Cast (c1,k,c2) -> - let next_mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in - let next () = try_aux [c1] next_mk_ctx next in - authorized_occ partial_app closed pat c mk_ctx next - | Lambda (x,c1,c2) -> - let next_mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in - let next () = try_aux [c1;c2] next_mk_ctx next in - authorized_occ partial_app closed pat c mk_ctx next - | Prod (x,c1,c2) -> - let next_mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in - let next () = try_aux [c1;c2] next_mk_ctx next in - authorized_occ partial_app closed pat c mk_ctx next - | LetIn (x,c1,t,c2) -> - let next_mk_ctx = function - | [c1;c2] -> mkLetIn (x,c1,t,c2) - | _ -> assert false - in - let next () = try_aux [c1;c2] next_mk_ctx next in - authorized_occ partial_app closed pat c mk_ctx next - | App (c1,lc) -> - let next () = - 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 - in - authorized_occ partial_app closed pat c mk_ctx next - | Case (ci,hd,c1,lc) -> - let next_mk_ctx = function - | [] -> assert false - | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) - in - let next () = try_aux (c1 :: Array.to_list lc) next_mk_ctx next in - authorized_occ partial_app closed pat c mk_ctx next - | Fix (indx,(names,types,bodies)) -> - let nb_fix = Array.length types in - let next_mk_ctx le = - let (ntypes,nbodies) = CList.chop nb_fix le in - mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in - let next () = - try_aux - ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in - authorized_occ partial_app closed pat c mk_ctx next - | CoFix (i,(names,types,bodies)) -> - let nb_fix = Array.length types in - let next_mk_ctx le = - let (ntypes,nbodies) = CList.chop nb_fix le in - mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in - let next () = - try_aux ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in - authorized_occ partial_app closed pat c mk_ctx next - | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> - authorized_occ partial_app closed pat c mk_ctx 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 - let lempty () = IStream.Nil in - let result () = aux c (fun x -> x) lempty in - IStream.thunk 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 c = - try let _ = matches pat c in true - with PatternMatchingFailure -> false - -let is_matching_head pat c = - try let _ = matches_head pat c in true - with PatternMatchingFailure -> false - -let is_matching_appsubterm ?(closed=true) pat c = - let results = sub_match ~partial_app:true ~closed pat c in - not (IStream.is_empty results) - -let matches_conv env sigma 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 - with PatternMatchingFailure -> false - diff --git a/pretyping/matching.mli b/pretyping/matching.mli deleted file mode 100644 index b82f115251..0000000000 --- a/pretyping/matching.mli +++ /dev/null @@ -1,86 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* constr -> patvar_map - -(** [matches_head pat c] does the same as [matches pat c] but accepts - [pat] to match an applicative prefix of [c] *) -val matches_head : constr_pattern -> constr -> patvar_map - -(** [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 * extended_patvar_map - -(** [is_matching pat c] just tells if [c] matches against [pat] *) -val is_matching : constr_pattern -> constr -> bool - -(** [is_matching_head pat c] just tells if [c] or an applicative - prefix of it matches against [pat] *) -val is_matching_head : 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 here with [special_meta]) *) -type matching_result = - { m_sub : bound_ident_map * patvar_map; - m_ctx : constr } - -(** [match_subterm n pat c] returns the substitution and the context - corresponding to each **closed** subterm of [c] matching [pat]. *) -val match_subterm : constr_pattern -> constr -> matching_result IStream.t - -(** [match_appsubterm pat c] returns the substitution and the context - corresponding to each **closed** subterm of [c] matching [pat], - considering application contexts as well. *) -val match_appsubterm : constr_pattern -> constr -> matching_result IStream.t - -(** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *) -val match_subterm_gen : bool (** true = with app context *) -> - constr_pattern -> constr -> matching_result IStream.t - -(** [is_matching_appsubterm pat c] tells if a subterm of [c] matches - against [pat] taking partial subterms into consideration *) -val is_matching_appsubterm : ?closed:bool -> constr_pattern -> constr -> bool - -(** [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/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index d4892f2f8a..469be6d9ea 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -20,7 +20,7 @@ Miscops Glob_ops Redops Patternops -Matching +ConstrMatching Tacred Typeclasses_errors Typeclasses diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 46037e5eee..4b03c935f5 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -22,7 +22,6 @@ open Closure open Reductionops open Cbv open Patternops -open Matching open Locus (* Errors *) @@ -804,8 +803,8 @@ let simpl env sigma c = strong whd_simpl env sigma c let matches_head c t = match kind_of_term t with - | App (f,_) -> matches c f - | _ -> raise PatternMatchingFailure + | App (f,_) -> ConstrMatching.matches c f + | _ -> raise ConstrMatching.PatternMatchingFailure let contextually byhead (occs,c) f env sigma t = let (nowhere_except_in,locs) = Locusops.convert_occs occs in @@ -815,7 +814,8 @@ let contextually byhead (occs,c) f env sigma t = if nowhere_except_in && (!pos > maxocc) then t else try - let subst = if byhead then matches_head c t else matches c t in + let subst = + if byhead then matches_head c t else ConstrMatching.matches c t in let ok = if nowhere_except_in then Int.List.mem !pos locs else not (Int.List.mem !pos locs) in @@ -829,7 +829,7 @@ let contextually byhead (occs,c) f env sigma t = mkApp (f, Array.map_left (traverse envc) l) else t - with PatternMatchingFailure -> + with ConstrMatching.PatternMatchingFailure -> map_constr_with_binders_left_to_right (fun d (env,c) -> (push_rel d env,lift_pattern 1 c)) traverse envc t diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index c0875d756f..de73f7720d 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -102,8 +102,8 @@ let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) let pf_check_type gls c1 c2 = ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2))) -let pf_is_matching = pf_apply Matching.is_matching_conv -let pf_matches = pf_apply Matching.matches_conv +let pf_is_matching = pf_apply ConstrMatching.is_matching_conv +let pf_matches = pf_apply ConstrMatching.matches_conv (************************************) (* Tactics handling a list of goals *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 61e7dde181..3b99cc5b9e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -21,7 +21,6 @@ open Evd open Typing open Pattern open Patternops -open Matching open Tacmach open Pfedit open Genredexpr @@ -1115,10 +1114,12 @@ let conclPattern concl pat tac = match pat with | None -> Proofview.tclUNIT Id.Map.empty | Some pat -> - try Proofview.tclUNIT (matches pat concl) - with PatternMatchingFailure -> Proofview.tclZERO (UserError ("conclPattern",str"conclPattern")) in - constr_bindings >>= fun constr_bindings -> - Hook.get forward_interp_tactic constr_bindings tac + try Proofview.tclUNIT (ConstrMatching.matches pat concl) + with ConstrMatching.PatternMatchingFailure -> + Proofview.tclZERO (UserError ("conclPattern",str"conclPattern")) + in + constr_bindings >>= fun constr_bindings -> + Hook.get forward_interp_tactic constr_bindings tac (***********************************************************) (** A debugging / verbosity framework for trivial and auto *) diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 4b1cd87150..7b47605119 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -23,7 +23,7 @@ open Declarations open Tactics open Tacticals open Auto -open Matching +open ConstrMatching open Hipattern open Tacmach open Coqlib diff --git a/tactics/equality.ml b/tactics/equality.ml index 1006fd2de7..2854d10194 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -25,7 +25,6 @@ open Typing open Retyping open Tacmach open Logic -open Matching open Hipattern open Tacexpr open Tacticals @@ -1383,7 +1382,7 @@ let decomp_tuple_term env c t = and cdr_code = applist (p2,[a;p;inner_code]) in let cdrtyp = beta_applist (p,[car]) in List.map (fun l -> ((car,a),car_code)::l) (decomprec cdr_code cdr cdrtyp) - with PatternMatchingFailure -> + with ConstrMatching.PatternMatchingFailure -> [] in [((ex,exty),inner_code)]::iterated_decomp @@ -1458,7 +1457,7 @@ let try_rewrite tac gls = try tac gls with - | PatternMatchingFailure -> + | ConstrMatching.PatternMatchingFailure -> errorlabstrm "try_rewrite" (str "Not a primitive equality here.") | e when catchable_exception e -> errorlabstrm "try_rewrite" @@ -1523,8 +1522,8 @@ let unfold_body x gl = let restrict_to_eq_and_identity eq = (* compatibility *) if not (eq_constr eq (constr_of_global glob_eq)) && - not (eq_constr eq (constr_of_global glob_identity)) then - raise PatternMatchingFailure + not (eq_constr eq (constr_of_global glob_identity)) + then raise ConstrMatching.PatternMatchingFailure exception FoundHyp of (Id.t * constr * bool) @@ -1534,7 +1533,7 @@ let is_eq_x gl x (id,_,c) = let (_,lhs,rhs) = snd (find_eq_data_decompose gl c) in if (eq_constr x lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true)); if (eq_constr x rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false)) - with PatternMatchingFailure -> + with ConstrMatching.PatternMatchingFailure -> () (* Rewrite "hyp:x=rhs" or "hyp:rhs=x" (if dir=false) everywhere and @@ -1635,7 +1634,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = if eq_constr x y then failwith "caught"; match kind_of_term x with Var x -> x | _ -> match kind_of_term y with Var y -> y | _ -> failwith "caught" - with PatternMatchingFailure -> failwith "caught" + with ConstrMatching.PatternMatchingFailure -> failwith "caught" in let test p = try Some (test p) with Failure _ -> None in let hyps = Tacmach.New.pf_hyps_types gl in @@ -1651,13 +1650,13 @@ let cond_eq_term_left c t gl = try let (_,x,_) = snd (find_eq_data_decompose gl t) in if pf_conv_x gl c x then true else failwith "not convertible" - with PatternMatchingFailure -> failwith "not an equality" + with ConstrMatching.PatternMatchingFailure -> failwith "not an equality" let cond_eq_term_right c t gl = try let (_,_,x) = snd (find_eq_data_decompose gl t) in if pf_conv_x gl c x then false else failwith "not convertible" - with PatternMatchingFailure -> failwith "not an equality" + with ConstrMatching.PatternMatchingFailure -> failwith "not an equality" let cond_eq_term c t gl = try @@ -1665,7 +1664,7 @@ let cond_eq_term c t gl = if pf_conv_x gl c x then true else if pf_conv_x gl c y then false else failwith "not convertible" - with PatternMatchingFailure -> failwith "not an equality" + with ConstrMatching.PatternMatchingFailure -> failwith "not an equality" let cond_eq_term_left c t = Tacmach.New.of_old (cond_eq_term_left c t) let cond_eq_term_right c t = Tacmach.New.of_old (cond_eq_term_right c t) diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 534b90491a..80720cfaf6 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -15,7 +15,7 @@ open Names open Term open Termops open Inductiveops -open Matching +open ConstrMatching open Coqlib open Declarations diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index cd265843d3..0e802f8a9c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -9,7 +9,6 @@ open Constrintern open Pattern open Patternops -open Matching open Pp open Genredexpr open Glob_term @@ -643,7 +642,7 @@ let interp_may_eval f ist env sigma = function (try let (sigma,ic) = f ist env sigma c and ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in - sigma , subst_meta [special_meta,ic] ctxt + sigma , subst_meta [ConstrMatching.special_meta,ic] ctxt with | Not_found -> user_err_loc (loc, "interp_may_eval", diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml index e52a9011cf..85108f8ed2 100644 --- a/tactics/tacticMatching.ml +++ b/tactics/tacticMatching.ml @@ -19,7 +19,7 @@ open Tacexpr those of {!Matching.matching_result}), and a {!Term.constr} substitution mapping corresponding to matched hypotheses. *) type 'a t = { - subst : Matching.bound_ident_map * Pattern.extended_patvar_map ; + subst : ConstrMatching.bound_ident_map * Pattern.extended_patvar_map ; context : Term.constr Id.Map.t; terms : Term.constr Id.Map.t; lhs : 'a; @@ -33,9 +33,9 @@ type 'a t = { (** Some of the functions of {!Matching} return the substitution with a [patvar_map] instead of an [extended_patvar_map]. [adjust] coerces substitution of the former type to the latter. *) -let adjust : Matching.bound_ident_map * Pattern.patvar_map -> - Matching.bound_ident_map * Pattern.extended_patvar_map = fun (l, lc) -> - (l, Id.Map.map (fun c -> [], c) lc) +let adjust : ConstrMatching.bound_ident_map * Pattern.patvar_map -> + ConstrMatching.bound_ident_map * Pattern.extended_patvar_map = + fun (l, lc) -> (l, Id.Map.map (fun c -> [], c) lc) (** Adds a binding to a {!Id.Map.t} if the identifier is [Some id] *) @@ -240,19 +240,19 @@ module PatternMatching (E:StaticEnvironment) = struct | Term p -> begin try - put_subst (Matching.extended_matches p term) <*> + put_subst (ConstrMatching.extended_matches p term) <*> return lhs - with Matching.PatternMatchingFailure -> fail + with ConstrMatching.PatternMatchingFailure -> fail end | Subterm (with_app_context,id_ctxt,p) -> (* spiwack: this branch is easier in direct style, would need to be changed if the implementation of the monad changes. *) - IStream.map begin fun { Matching.m_sub ; m_ctx } -> + IStream.map begin fun { ConstrMatching.m_sub ; m_ctx } -> let subst = adjust m_sub in let context = id_map_try_add id_ctxt m_ctx Id.Map.empty in let terms = empty_term_subst in { subst ; context ; terms ; lhs } - end (Matching.match_subterm_gen with_app_context p term) + end (ConstrMatching.match_subterm_gen with_app_context p term) (** [rule_match_term term rule] matches the term [term] with the diff --git a/tactics/tacticMatching.mli b/tactics/tacticMatching.mli index 1b440e195b..6889ea0e9b 100644 --- a/tactics/tacticMatching.mli +++ b/tactics/tacticMatching.mli @@ -17,7 +17,7 @@ those of {!Matching.matching_result}), and a {!Term.constr} substitution mapping corresponding to matched hypotheses. *) type 'a t = { - subst : Matching.bound_ident_map * Pattern.extended_patvar_map ; + subst : ConstrMatching.bound_ident_map * Pattern.extended_patvar_map ; context : Term.constr Names.Id.Map.t; terms : Term.constr Names.Id.Map.t; lhs : 'a; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d1b096048d..a5f88c9291 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1416,7 +1416,7 @@ let my_find_eq_data_decompose gl t = with e when is_anomaly e (* Hack in case equality is not yet defined... one day, maybe, known equalities will be dynamically registered *) - -> raise Matching.PatternMatchingFailure + -> raise ConstrMatching.PatternMatchingFailure let intro_decomp_eq loc b l l' thin tac id gl = let c = mkVar id in diff --git a/toplevel/search.ml b/toplevel/search.ml index 91762c0003..78fa3a325d 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -114,7 +114,7 @@ let format_display l = prlist_with_sep fnl (fun x -> x) (List.rev l) (** FIXME: this is quite dummy, we may find a more efficient algorithm. *) let rec pattern_filter pat ref env typ = let typ = strip_outer_cast typ in - if Matching.is_matching pat typ then true + if ConstrMatching.is_matching pat typ then true else match kind_of_term typ with | Prod (_, _, typ) | LetIn (_, _, _, typ) -> pattern_filter pat ref env typ @@ -122,7 +122,7 @@ let rec pattern_filter pat ref env typ = let rec head_filter pat ref env typ = let typ = strip_outer_cast typ in - if Matching.is_matching_head pat typ then true + if ConstrMatching.is_matching_head pat typ then true else match kind_of_term typ with | Prod (_, _, typ) | LetIn (_, _, _, typ) -> head_filter pat ref env typ @@ -151,7 +151,7 @@ let name_of_reference ref = Id.to_string (basename_of_global ref) let search_about_filter query gr env typ = match query with | GlobSearchSubPattern pat -> - Matching.is_matching_appsubterm ~closed:false pat typ + ConstrMatching.is_matching_appsubterm ~closed:false pat typ | GlobSearchString s -> String.string_contains ~where:(name_of_reference gr) ~what:s @@ -277,10 +277,11 @@ let interface_search flags = toggle (Str.string_match regexp id 0) flag in let match_type (pat, flag) = - toggle (Matching.is_matching pat constr) flag + toggle (ConstrMatching.is_matching pat constr) flag in let match_subtype (pat, flag) = - toggle (Matching.is_matching_appsubterm ~closed:false pat constr) flag + toggle + (ConstrMatching.is_matching_appsubterm ~closed:false pat constr) flag in let match_module (mdl, flag) = toggle (Libnames.is_dirpath_prefix_of mdl path) flag -- cgit v1.2.3