From d08532d5344d96d10604760fa44109c9d56e73ce Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 8 Jan 2015 18:18:02 +0100 Subject: Avoiding introducing yet another convention in naming files. --- Makefile.common | 6 +- dev/printers.mllib | 2 +- plugins/Derive/Derive.v | 1 - plugins/Derive/derive.ml | 104 -------- plugins/Derive/derive.mli | 13 - plugins/Derive/derive_plugin.mllib | 2 - plugins/Derive/g_derive.ml4 | 16 -- plugins/Derive/vo.itarget | 1 - plugins/derive/Derive.v | 1 + plugins/derive/derive.ml | 104 ++++++++ plugins/derive/derive.mli | 13 + plugins/derive/derive_plugin.mllib | 2 + plugins/derive/g_derive.ml4 | 16 ++ plugins/derive/vo.itarget | 1 + plugins/quote/quote.ml | 2 +- pretyping/constrMatching.ml | 494 ------------------------------------- pretyping/constrMatching.mli | 85 ------- pretyping/constr_matching.ml | 494 +++++++++++++++++++++++++++++++++++++ pretyping/constr_matching.mli | 85 +++++++ pretyping/pretyping.mllib | 2 +- pretyping/tacred.ml | 10 +- proofs/tacmach.ml | 6 +- tactics/auto.ml | 4 +- tactics/eqdecide.ml | 2 +- tactics/equality.ml | 16 +- tactics/tacinterp.ml | 10 +- tactics/tacticMatching.ml | 373 ---------------------------- tactics/tacticMatching.mli | 49 ---- tactics/tactic_matching.ml | 373 ++++++++++++++++++++++++++++ tactics/tactic_matching.mli | 49 ++++ tactics/tactics.ml | 2 +- tactics/tactics.mllib | 2 +- toplevel/search.ml | 10 +- 33 files changed, 1175 insertions(+), 1175 deletions(-) delete mode 100644 plugins/Derive/Derive.v delete mode 100644 plugins/Derive/derive.ml delete mode 100644 plugins/Derive/derive.mli delete mode 100644 plugins/Derive/derive_plugin.mllib delete mode 100644 plugins/Derive/g_derive.ml4 delete mode 100644 plugins/Derive/vo.itarget create mode 100644 plugins/derive/Derive.v create mode 100644 plugins/derive/derive.ml create mode 100644 plugins/derive/derive.mli create mode 100644 plugins/derive/derive_plugin.mllib create mode 100644 plugins/derive/g_derive.ml4 create mode 100644 plugins/derive/vo.itarget delete mode 100644 pretyping/constrMatching.ml delete mode 100644 pretyping/constrMatching.mli create mode 100644 pretyping/constr_matching.ml create mode 100644 pretyping/constr_matching.mli delete mode 100644 tactics/tacticMatching.ml delete mode 100644 tactics/tacticMatching.mli create mode 100644 tactics/tactic_matching.ml create mode 100644 tactics/tactic_matching.mli diff --git a/Makefile.common b/Makefile.common index 7c98b64def..d752a5be91 100644 --- a/Makefile.common +++ b/Makefile.common @@ -68,7 +68,7 @@ CORESRCDIRS:=\ PLUGINS:=\ omega romega micromega quote \ setoid_ring extraction fourier \ - cc funind firstorder Derive \ + cc funind firstorder derive \ rtauto nsatz syntax decl_mode btauto SRCDIRS:=\ @@ -190,7 +190,7 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \ ascii_syntax_plugin.cma \ string_syntax_plugin.cma ) DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma -DERIVECMA:=plugins/Derive/derive_plugin.cma +DERIVECMA:=plugins/derive/derive_plugin.cma PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ $(QUOTECMA) $(RINGCMA) \ @@ -314,7 +314,7 @@ BTAUTOVO:=$(call cat_vo_itarget, plugins/btauto) RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto) EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction) CCVO:= -DERIVEVO:=$(call cat_vo_itarget, plugins/Derive) +DERIVEVO:=$(call cat_vo_itarget, plugins/derive) PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) \ $(FOURIERVO) $(CCVO) $(FUNINDVO) \ diff --git a/dev/printers.mllib b/dev/printers.mllib index 2e61cb6973..2f78c2e915 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -132,7 +132,7 @@ Recordops Evarconv Typing Patternops -ConstrMatching +Constr_matching Find_subterm Tacred Classops diff --git a/plugins/Derive/Derive.v b/plugins/Derive/Derive.v deleted file mode 100644 index 0d5a93b034..0000000000 --- a/plugins/Derive/Derive.v +++ /dev/null @@ -1 +0,0 @@ -Declare ML Module "derive_plugin". \ No newline at end of file diff --git a/plugins/Derive/derive.ml b/plugins/Derive/derive.ml deleted file mode 100644 index 156c9771aa..0000000000 --- a/plugins/Derive/derive.ml +++ /dev/null @@ -1,104 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Term.constr) (x:Entries.const_entry_body) - : Entries.const_entry_body = - Future.chain ~pure:true x begin fun ((b,ctx),fx) -> - (f b , ctx) , fx - end - -(** [start_deriving f suchthat lemma] starts a proof of [suchthat] - (which can contain references to [f]) in the context extended by - [f:=?x]. When the proof ends, [f] is defined as the value of [?x] - and [lemma] as the proof. *) -let start_deriving f suchthat lemma = - - let env = Global.env () in - let sigma = Evd.from_env env in - let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in - - (** create a sort variable for the type of [f] *) - (* spiwack: I don't know what the rigidity flag does, picked the one - that looked the most general. *) - let (sigma,f_type_sort) = Evd.new_sort_variable Evd.univ_flexible_alg sigma in - let f_type_type = Term.mkSort f_type_sort in - (** create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *) - let goals = - let open Proofview in - TCons ( env , sigma , f_type_type , (fun sigma f_type -> - TCons ( env , sigma , f_type , (fun sigma ef -> - let env' = Environ.push_named (f , (Some ef) , f_type) env in - let evdref = ref sigma in - let suchthat = Constrintern.interp_type_evars env' evdref suchthat in - TCons ( env' , !evdref , suchthat , (fun sigma _ -> - TNil sigma)))))) - in - - (** The terminator handles the registering of constants when the proof is closed. *) - let terminator com = - let open Proof_global in - (** Extracts the relevant information from the proof. [Admitted] - and [Save] result in user errors. [opaque] is [true] if the - proof was concluded by [Qed], and [false] if [Defined]. [f_def] - and [lemma_def] correspond to the proof of [f] and of - [suchthat], respectively. *) - let (opaque,f_def,lemma_def) = - match com with - | Admitted -> Errors.error"Admitted isn't supported in Derive." - | Proved (_,Some _,_) -> - Errors.error"Cannot save a proof of Derive with an explicit name." - | Proved (opaque, None, obj) -> - match Proof_global.(obj.entries) with - | [_;f_def;lemma_def] -> - opaque , f_def , lemma_def - | _ -> assert false - in - (** The opacity of [f_def] is adjusted to be [false], as it - must. Then [f] is declared in the global environment. *) - let f_def = { f_def with Entries.const_entry_opaque = false } in - let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in - let f_kn = Declare.declare_constant f f_def in - let f_kn_term = Term.mkConst f_kn in - (** In the type and body of the proof of [suchthat] there can be - references to the variable [f]. It needs to be replaced by - references to the constant [f] declared above. This substitution - performs this precise action. *) - let substf c = Vars.replace_vars [f,f_kn_term] c in - (** Extracts the type of the proof of [suchthat]. *) - let lemma_pretype = - match Entries.(lemma_def.const_entry_type) with - | Some t -> t - | None -> assert false (* Proof_global always sets type here. *) - in - (** The references of [f] are subsituted appropriately. *) - let lemma_type = substf lemma_pretype in - (** The same is done in the body of the proof. *) - let lemma_body = - map_const_entry_body substf Entries.(lemma_def.const_entry_body) - in - let lemma_def = let open Entries in { lemma_def with - const_entry_body = lemma_body ; - const_entry_type = Some lemma_type ; - const_entry_opaque = opaque ; } - in - let lemma_def = - Entries.DefinitionEntry lemma_def , - Decl_kinds.(IsProof Proposition) - in - ignore (Declare.declare_constant lemma lemma_def) - in - - let () = Proof_global.start_dependent_proof lemma kind goals terminator in - let _ = Proof_global.with_current_proof begin fun _ p -> - Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p - end in - () - - - - diff --git a/plugins/Derive/derive.mli b/plugins/Derive/derive.mli deleted file mode 100644 index 5157c4a272..0000000000 --- a/plugins/Derive/derive.mli +++ /dev/null @@ -1,13 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Constrexpr.constr_expr -> Names.Id.t -> unit diff --git a/plugins/Derive/derive_plugin.mllib b/plugins/Derive/derive_plugin.mllib deleted file mode 100644 index 5ee0fc6da6..0000000000 --- a/plugins/Derive/derive_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Derive -G_derive diff --git a/plugins/Derive/g_derive.ml4 b/plugins/Derive/g_derive.ml4 deleted file mode 100644 index 0721c675fa..0000000000 --- a/plugins/Derive/g_derive.ml4 +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - [ Derive.start_deriving f suchthat lemma ] -END diff --git a/plugins/Derive/vo.itarget b/plugins/Derive/vo.itarget deleted file mode 100644 index b480982193..0000000000 --- a/plugins/Derive/vo.itarget +++ /dev/null @@ -1 +0,0 @@ -Derive.vo \ No newline at end of file diff --git a/plugins/derive/Derive.v b/plugins/derive/Derive.v new file mode 100644 index 0000000000..0d5a93b034 --- /dev/null +++ b/plugins/derive/Derive.v @@ -0,0 +1 @@ +Declare ML Module "derive_plugin". \ No newline at end of file diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml new file mode 100644 index 0000000000..156c9771aa --- /dev/null +++ b/plugins/derive/derive.ml @@ -0,0 +1,104 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Term.constr) (x:Entries.const_entry_body) + : Entries.const_entry_body = + Future.chain ~pure:true x begin fun ((b,ctx),fx) -> + (f b , ctx) , fx + end + +(** [start_deriving f suchthat lemma] starts a proof of [suchthat] + (which can contain references to [f]) in the context extended by + [f:=?x]. When the proof ends, [f] is defined as the value of [?x] + and [lemma] as the proof. *) +let start_deriving f suchthat lemma = + + let env = Global.env () in + let sigma = Evd.from_env env in + let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in + + (** create a sort variable for the type of [f] *) + (* spiwack: I don't know what the rigidity flag does, picked the one + that looked the most general. *) + let (sigma,f_type_sort) = Evd.new_sort_variable Evd.univ_flexible_alg sigma in + let f_type_type = Term.mkSort f_type_sort in + (** create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *) + let goals = + let open Proofview in + TCons ( env , sigma , f_type_type , (fun sigma f_type -> + TCons ( env , sigma , f_type , (fun sigma ef -> + let env' = Environ.push_named (f , (Some ef) , f_type) env in + let evdref = ref sigma in + let suchthat = Constrintern.interp_type_evars env' evdref suchthat in + TCons ( env' , !evdref , suchthat , (fun sigma _ -> + TNil sigma)))))) + in + + (** The terminator handles the registering of constants when the proof is closed. *) + let terminator com = + let open Proof_global in + (** Extracts the relevant information from the proof. [Admitted] + and [Save] result in user errors. [opaque] is [true] if the + proof was concluded by [Qed], and [false] if [Defined]. [f_def] + and [lemma_def] correspond to the proof of [f] and of + [suchthat], respectively. *) + let (opaque,f_def,lemma_def) = + match com with + | Admitted -> Errors.error"Admitted isn't supported in Derive." + | Proved (_,Some _,_) -> + Errors.error"Cannot save a proof of Derive with an explicit name." + | Proved (opaque, None, obj) -> + match Proof_global.(obj.entries) with + | [_;f_def;lemma_def] -> + opaque , f_def , lemma_def + | _ -> assert false + in + (** The opacity of [f_def] is adjusted to be [false], as it + must. Then [f] is declared in the global environment. *) + let f_def = { f_def with Entries.const_entry_opaque = false } in + let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in + let f_kn = Declare.declare_constant f f_def in + let f_kn_term = Term.mkConst f_kn in + (** In the type and body of the proof of [suchthat] there can be + references to the variable [f]. It needs to be replaced by + references to the constant [f] declared above. This substitution + performs this precise action. *) + let substf c = Vars.replace_vars [f,f_kn_term] c in + (** Extracts the type of the proof of [suchthat]. *) + let lemma_pretype = + match Entries.(lemma_def.const_entry_type) with + | Some t -> t + | None -> assert false (* Proof_global always sets type here. *) + in + (** The references of [f] are subsituted appropriately. *) + let lemma_type = substf lemma_pretype in + (** The same is done in the body of the proof. *) + let lemma_body = + map_const_entry_body substf Entries.(lemma_def.const_entry_body) + in + let lemma_def = let open Entries in { lemma_def with + const_entry_body = lemma_body ; + const_entry_type = Some lemma_type ; + const_entry_opaque = opaque ; } + in + let lemma_def = + Entries.DefinitionEntry lemma_def , + Decl_kinds.(IsProof Proposition) + in + ignore (Declare.declare_constant lemma lemma_def) + in + + let () = Proof_global.start_dependent_proof lemma kind goals terminator in + let _ = Proof_global.with_current_proof begin fun _ p -> + Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p + end in + () + + + + diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli new file mode 100644 index 0000000000..5157c4a272 --- /dev/null +++ b/plugins/derive/derive.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Constrexpr.constr_expr -> Names.Id.t -> unit diff --git a/plugins/derive/derive_plugin.mllib b/plugins/derive/derive_plugin.mllib new file mode 100644 index 0000000000..5ee0fc6da6 --- /dev/null +++ b/plugins/derive/derive_plugin.mllib @@ -0,0 +1,2 @@ +Derive +G_derive diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 new file mode 100644 index 0000000000..0721c675fa --- /dev/null +++ b/plugins/derive/g_derive.ml4 @@ -0,0 +1,16 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + [ Derive.start_deriving f suchthat lemma ] +END diff --git a/plugins/derive/vo.itarget b/plugins/derive/vo.itarget new file mode 100644 index 0000000000..b480982193 --- /dev/null +++ b/plugins/derive/vo.itarget @@ -0,0 +1 @@ +Derive.vo \ No newline at end of file diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 64166a0de6..1299c99ef5 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -107,7 +107,7 @@ open Names open Term open Pattern open Patternops -open ConstrMatching +open Constr_matching open Tacmach (*i*) diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml deleted file mode 100644 index ad4c678cbd..0000000000 --- a/pretyping/constrMatching.ml +++ /dev/null @@ -1,494 +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 rec build_lambda vars stk m = match vars with -| [] -> - let len = List.length stk in - lift (-1 * len) m -| n :: vars -> - (* change [ x1 ... xn y z1 ... zm |- t ] into - [ x1 ... xn z1 ... zm |- lam y. t ] *) - let len = List.length stk in - let init i = - if i < pred n then mkRel (i + 2) - else if Int.equal i (pred n) then mkRel 1 - else mkRel (i + 1) - in - let m = substl (List.init len init) m in - let pre, suf = List.chop (pred n) stk in - match suf with - | [] -> assert false - | (_, na, t) :: suf -> - let map i = if i > n then pred i else i in - let vars = List.map map vars in - (** Check that the abstraction is legal *) - let frels = free_rels t in - let brels = List.fold_right Int.Set.add vars Int.Set.empty in - let () = if not (Int.Set.subset frels brels) then raise PatternMatchingFailure in - (** Create the abstraction *) - let m = mkLambda (na, t, m) in - build_lambda vars (pre @ suf) m - -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 env sigma convert allow_partial_app allow_bound_rels pat c = - let convref ref c = - match ref, kind_of_term c with - | VarRef id, Var id' -> Names.id_eq id id' - | ConstRef c, Const (c',_) -> Names.eq_constant c c' - | IndRef i, Ind (i', _) -> Names.eq_ind i i' - | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c' - | _, _ -> - (if convert then - let sigma,c' = Evd.fresh_global env sigma ref in - is_conv env sigma c' c - else false) - in - let rec sorec stk env subst p t = - let cT = strip_outer_cast t in - match p,kind_of_term cT with - | PSoApp (n,args),m -> - let fold (ans, seen) = function - | PRel n -> - let () = if Int.Set.mem n seen then error "Non linear second-order pattern" in - (n :: ans, Int.Set.add n seen) - | _ -> error "Only bound indices allowed in second order pattern matching." - in - let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in - let frels = free_rels cT in - if Int.Set.subset frels relset 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 convref 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 env subst p t - - | PApp (PApp (h, a1), a2), _ -> - sorec stk env subst (PApp(h,Array.append a1 a2)) t - - | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app -> - (let diff = Array.length args2 - Array.length args1 in - if diff >= 0 then - let args21, args22 = Array.chop diff 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 env) subst args1 args22 - else (* Might be a projection on the right *) - match kind_of_term c2 with - | Proj (pr, c) when not (Projection.unfolded pr) -> - (try let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in - sorec stk env subst p term - with Retyping.RetypeError _ -> raise PatternMatchingFailure) - | _ -> raise PatternMatchingFailure) - - | PApp (c1,arg1), App (c2,arg2) -> - (match c1, kind_of_term c2 with - | PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr)) - || Projection.unfolded pr -> - raise PatternMatchingFailure - | PProj (pr1,c1), Proj (pr,c) -> - if Projection.equal pr1 pr then - try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c) arg1 arg2 - with Invalid_argument _ -> raise PatternMatchingFailure - else raise PatternMatchingFailure - | _, Proj (pr,c) when not (Projection.unfolded pr) -> - (try let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in - sorec stk env subst p term - with Retyping.RetypeError _ -> raise PatternMatchingFailure) - | _, _ -> - try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2 - with Invalid_argument _ -> raise PatternMatchingFailure) - - | PApp (PRef (ConstRef c1), _), Proj (pr, c2) - when Projection.unfolded pr || not (eq_constant c1 (Projection.constant pr)) -> - raise PatternMatchingFailure - - | PApp (c, args), Proj (pr, c2) -> - (try let term = Retyping.expand_projection env sigma pr c2 [] in - sorec stk env subst p term - with Retyping.RetypeError _ -> raise PatternMatchingFailure) - - | PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 -> - sorec stk env subst c1 c2 - - | PProd (na1,c1,d1), Prod(na2,c2,d2) -> - sorec ((na1,na2,c2)::stk) (Environ.push_rel (na2,None,c2) env) - (add_binders na1 na2 (sorec stk env subst c1 c2)) d1 d2 - - | PLambda (na1,c1,d1), Lambda(na2,c2,d2) -> - sorec ((na1,na2,c2)::stk) (Environ.push_rel (na2,None,c2) env) - (add_binders na1 na2 (sorec stk env subst c1 c2)) d1 d2 - - | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) -> - sorec ((na1,na2,t2)::stk) (Environ.push_rel (na2,Some c2,t2) env) - (add_binders na1 na2 (sorec stk env 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' (Environ.push_rel_context ctx' env) - (sorec s (Environ.push_rel_context ctx env) (sorec stk env 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 env subst c br2.(j) - in - let chk_head = sorec stk env (sorec stk env 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 [] env (Id.Map.empty, Id.Map.empty) pat c - -let matches_core_closed env sigma convert allow_partial_app pat c = - let names, subst = matches_core env sigma convert allow_partial_app false pat c in - (names, Id.Map.map snd subst) - -let extended_matches env sigma = matches_core env sigma false true true - -let matches env sigma pat c = snd (matches_core_closed env sigma false 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 env sigma 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 env sigma pat head - -(* Tells if it is an authorized occurrence and if the instance is closed *) -let authorized_occ env sigma partial_app closed pat c mk_ctx next = - try - let subst = matches_core_closed env sigma false partial_app pat c in - if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd subst) - then next () - else mkresult subst (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) env sigma pat c = - let rec aux env 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 [env] [c1] next_mk_ctx next in - authorized_occ env sigma 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 () = - let env' = Environ.push_rel (x,None,c1) env in - try_aux [env;env'] [c1; c2] next_mk_ctx next in - authorized_occ env sigma 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 () = - let env' = Environ.push_rel (x,None,c1) env in - try_aux [env;env'] [c1;c2] next_mk_ctx next in - authorized_occ env sigma 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 () = - let env' = Environ.push_rel (x,Some c1,t) env in - try_aux [env;env'] [c1;c2] next_mk_ctx next in - authorized_occ env sigma 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 [env] [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 [env] (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 env 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 [env] (c1::Array.to_list lc) mk_ctx next - in - authorized_occ env sigma 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 [env] (c1 :: Array.to_list lc) next_mk_ctx next in - authorized_occ env sigma 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 - [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in - authorized_occ env sigma 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 [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next - | Proj (p,c') -> - let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in - let next () = - if partial_app then - try - let term = Retyping.expand_projection env sigma p c' [] in - aux env term mk_ctx next - with Retyping.RetypeError _ -> raise PatternMatchingFailure - else - try_aux [env] [c'] next_mk_ctx next in - authorized_occ env sigma partial_app closed pat c mk_ctx next - | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> - authorized_occ env sigma partial_app closed pat c mk_ctx next - - (* Tries [sub_match] for all terms in the list *) - and try_aux lenv lc mk_ctx next = - let rec try_sub_match_rec lacc lenv lc = - match lenv, lc with - | _, [] -> next () - | env :: tlenv, c::tl -> - let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in - let next () = - let env' = match tlenv with [] -> lenv | _ -> tlenv in - try_sub_match_rec (c::lacc) env' tl - in - aux env c mk_ctx next - | _ -> assert false in - try_sub_match_rec [] lenv lc in - let lempty () = IStream.Nil in - let result () = aux env c (fun x -> x) lempty in - IStream.thunk result - -let match_subterm env sigma pat c = sub_match env sigma pat c - -let match_appsubterm env sigma pat c = - sub_match ~partial_app:true env sigma pat c - -let match_subterm_gen env sigma app pat c = - sub_match ~partial_app:app env sigma pat c - -let is_matching env sigma pat c = - try let _ = matches env sigma pat c in true - with PatternMatchingFailure -> false - -let is_matching_head env sigma pat c = - try let _ = matches_head env sigma pat c in true - with PatternMatchingFailure -> false - -let is_matching_appsubterm ?(closed=true) env sigma pat c = - let results = sub_match ~partial_app:true ~closed env sigma pat c in - not (IStream.is_empty results) - -let matches_conv env sigma c p = - snd (matches_core_closed env sigma true 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 deleted file mode 100644 index a4e797dae0..0000000000 --- a/pretyping/constrMatching.mli +++ /dev/null @@ -1,85 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Evd.evar_map -> constr_pattern -> 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 : env -> Evd.evar_map -> 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 : - env -> Evd.evar_map -> constr_pattern -> constr -> bound_ident_map * extended_patvar_map - -(** [is_matching pat c] just tells if [c] matches against [pat] *) -val is_matching : env -> Evd.evar_map -> 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 : env -> Evd.evar_map -> 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 : env -> Evd.evar_map -> 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 : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t - -(** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *) -val match_subterm_gen : env -> Evd.evar_map -> 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 -> env -> Evd.evar_map -> 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/constr_matching.ml b/pretyping/constr_matching.ml new file mode 100644 index 0000000000..ad4c678cbd --- /dev/null +++ b/pretyping/constr_matching.ml @@ -0,0 +1,494 @@ +(************************************************************************) +(* 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 rec build_lambda vars stk m = match vars with +| [] -> + let len = List.length stk in + lift (-1 * len) m +| n :: vars -> + (* change [ x1 ... xn y z1 ... zm |- t ] into + [ x1 ... xn z1 ... zm |- lam y. t ] *) + let len = List.length stk in + let init i = + if i < pred n then mkRel (i + 2) + else if Int.equal i (pred n) then mkRel 1 + else mkRel (i + 1) + in + let m = substl (List.init len init) m in + let pre, suf = List.chop (pred n) stk in + match suf with + | [] -> assert false + | (_, na, t) :: suf -> + let map i = if i > n then pred i else i in + let vars = List.map map vars in + (** Check that the abstraction is legal *) + let frels = free_rels t in + let brels = List.fold_right Int.Set.add vars Int.Set.empty in + let () = if not (Int.Set.subset frels brels) then raise PatternMatchingFailure in + (** Create the abstraction *) + let m = mkLambda (na, t, m) in + build_lambda vars (pre @ suf) m + +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 env sigma convert allow_partial_app allow_bound_rels pat c = + let convref ref c = + match ref, kind_of_term c with + | VarRef id, Var id' -> Names.id_eq id id' + | ConstRef c, Const (c',_) -> Names.eq_constant c c' + | IndRef i, Ind (i', _) -> Names.eq_ind i i' + | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c' + | _, _ -> + (if convert then + let sigma,c' = Evd.fresh_global env sigma ref in + is_conv env sigma c' c + else false) + in + let rec sorec stk env subst p t = + let cT = strip_outer_cast t in + match p,kind_of_term cT with + | PSoApp (n,args),m -> + let fold (ans, seen) = function + | PRel n -> + let () = if Int.Set.mem n seen then error "Non linear second-order pattern" in + (n :: ans, Int.Set.add n seen) + | _ -> error "Only bound indices allowed in second order pattern matching." + in + let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in + let frels = free_rels cT in + if Int.Set.subset frels relset 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 convref 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 env subst p t + + | PApp (PApp (h, a1), a2), _ -> + sorec stk env subst (PApp(h,Array.append a1 a2)) t + + | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app -> + (let diff = Array.length args2 - Array.length args1 in + if diff >= 0 then + let args21, args22 = Array.chop diff 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 env) subst args1 args22 + else (* Might be a projection on the right *) + match kind_of_term c2 with + | Proj (pr, c) when not (Projection.unfolded pr) -> + (try let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in + sorec stk env subst p term + with Retyping.RetypeError _ -> raise PatternMatchingFailure) + | _ -> raise PatternMatchingFailure) + + | PApp (c1,arg1), App (c2,arg2) -> + (match c1, kind_of_term c2 with + | PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr)) + || Projection.unfolded pr -> + raise PatternMatchingFailure + | PProj (pr1,c1), Proj (pr,c) -> + if Projection.equal pr1 pr then + try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c) arg1 arg2 + with Invalid_argument _ -> raise PatternMatchingFailure + else raise PatternMatchingFailure + | _, Proj (pr,c) when not (Projection.unfolded pr) -> + (try let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in + sorec stk env subst p term + with Retyping.RetypeError _ -> raise PatternMatchingFailure) + | _, _ -> + try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2 + with Invalid_argument _ -> raise PatternMatchingFailure) + + | PApp (PRef (ConstRef c1), _), Proj (pr, c2) + when Projection.unfolded pr || not (eq_constant c1 (Projection.constant pr)) -> + raise PatternMatchingFailure + + | PApp (c, args), Proj (pr, c2) -> + (try let term = Retyping.expand_projection env sigma pr c2 [] in + sorec stk env subst p term + with Retyping.RetypeError _ -> raise PatternMatchingFailure) + + | PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 -> + sorec stk env subst c1 c2 + + | PProd (na1,c1,d1), Prod(na2,c2,d2) -> + sorec ((na1,na2,c2)::stk) (Environ.push_rel (na2,None,c2) env) + (add_binders na1 na2 (sorec stk env subst c1 c2)) d1 d2 + + | PLambda (na1,c1,d1), Lambda(na2,c2,d2) -> + sorec ((na1,na2,c2)::stk) (Environ.push_rel (na2,None,c2) env) + (add_binders na1 na2 (sorec stk env subst c1 c2)) d1 d2 + + | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) -> + sorec ((na1,na2,t2)::stk) (Environ.push_rel (na2,Some c2,t2) env) + (add_binders na1 na2 (sorec stk env 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' (Environ.push_rel_context ctx' env) + (sorec s (Environ.push_rel_context ctx env) (sorec stk env 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 env subst c br2.(j) + in + let chk_head = sorec stk env (sorec stk env 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 [] env (Id.Map.empty, Id.Map.empty) pat c + +let matches_core_closed env sigma convert allow_partial_app pat c = + let names, subst = matches_core env sigma convert allow_partial_app false pat c in + (names, Id.Map.map snd subst) + +let extended_matches env sigma = matches_core env sigma false true true + +let matches env sigma pat c = snd (matches_core_closed env sigma false 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 env sigma 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 env sigma pat head + +(* Tells if it is an authorized occurrence and if the instance is closed *) +let authorized_occ env sigma partial_app closed pat c mk_ctx next = + try + let subst = matches_core_closed env sigma false partial_app pat c in + if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd subst) + then next () + else mkresult subst (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) env sigma pat c = + let rec aux env 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 [env] [c1] next_mk_ctx next in + authorized_occ env sigma 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 () = + let env' = Environ.push_rel (x,None,c1) env in + try_aux [env;env'] [c1; c2] next_mk_ctx next in + authorized_occ env sigma 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 () = + let env' = Environ.push_rel (x,None,c1) env in + try_aux [env;env'] [c1;c2] next_mk_ctx next in + authorized_occ env sigma 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 () = + let env' = Environ.push_rel (x,Some c1,t) env in + try_aux [env;env'] [c1;c2] next_mk_ctx next in + authorized_occ env sigma 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 [env] [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 [env] (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 env 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 [env] (c1::Array.to_list lc) mk_ctx next + in + authorized_occ env sigma 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 [env] (c1 :: Array.to_list lc) next_mk_ctx next in + authorized_occ env sigma 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 + [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in + authorized_occ env sigma 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 [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in + authorized_occ env sigma partial_app closed pat c mk_ctx next + | Proj (p,c') -> + let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in + let next () = + if partial_app then + try + let term = Retyping.expand_projection env sigma p c' [] in + aux env term mk_ctx next + with Retyping.RetypeError _ -> raise PatternMatchingFailure + else + try_aux [env] [c'] next_mk_ctx next in + authorized_occ env sigma partial_app closed pat c mk_ctx next + | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> + authorized_occ env sigma partial_app closed pat c mk_ctx next + + (* Tries [sub_match] for all terms in the list *) + and try_aux lenv lc mk_ctx next = + let rec try_sub_match_rec lacc lenv lc = + match lenv, lc with + | _, [] -> next () + | env :: tlenv, c::tl -> + let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in + let next () = + let env' = match tlenv with [] -> lenv | _ -> tlenv in + try_sub_match_rec (c::lacc) env' tl + in + aux env c mk_ctx next + | _ -> assert false in + try_sub_match_rec [] lenv lc in + let lempty () = IStream.Nil in + let result () = aux env c (fun x -> x) lempty in + IStream.thunk result + +let match_subterm env sigma pat c = sub_match env sigma pat c + +let match_appsubterm env sigma pat c = + sub_match ~partial_app:true env sigma pat c + +let match_subterm_gen env sigma app pat c = + sub_match ~partial_app:app env sigma pat c + +let is_matching env sigma pat c = + try let _ = matches env sigma pat c in true + with PatternMatchingFailure -> false + +let is_matching_head env sigma pat c = + try let _ = matches_head env sigma pat c in true + with PatternMatchingFailure -> false + +let is_matching_appsubterm ?(closed=true) env sigma pat c = + let results = sub_match ~partial_app:true ~closed env sigma pat c in + not (IStream.is_empty results) + +let matches_conv env sigma c p = + snd (matches_core_closed env sigma true 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/constr_matching.mli b/pretyping/constr_matching.mli new file mode 100644 index 0000000000..a4e797dae0 --- /dev/null +++ b/pretyping/constr_matching.mli @@ -0,0 +1,85 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Evd.evar_map -> constr_pattern -> 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 : env -> Evd.evar_map -> 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 : + env -> Evd.evar_map -> constr_pattern -> constr -> bound_ident_map * extended_patvar_map + +(** [is_matching pat c] just tells if [c] matches against [pat] *) +val is_matching : env -> Evd.evar_map -> 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 : env -> Evd.evar_map -> 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 : env -> Evd.evar_map -> 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 : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t + +(** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *) +val match_subterm_gen : env -> Evd.evar_map -> 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 -> env -> Evd.evar_map -> 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 b189360c07..25d17c7c9f 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -20,7 +20,7 @@ Miscops Glob_ops Redops Patternops -ConstrMatching +Constr_matching Tacred Typeclasses_errors Typeclasses diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 2064fb6e17..9a778e0181 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -943,9 +943,9 @@ let simpl env sigma c = strong whd_simpl env sigma c let matches_head env sigma c t = match kind_of_term t with - | App (f,_) -> ConstrMatching.matches env sigma c f - | Proj (p, _) -> ConstrMatching.matches env sigma c (mkConst (Projection.constant p)) - | _ -> raise ConstrMatching.PatternMatchingFailure + | App (f,_) -> Constr_matching.matches env sigma c f + | Proj (p, _) -> Constr_matching.matches env sigma c (mkConst (Projection.constant p)) + | _ -> raise Constr_matching.PatternMatchingFailure let is_pattern_meta = function Pattern.PMeta _ -> true | _ -> false @@ -980,7 +980,7 @@ let e_contextually byhead (occs,c) f env sigma t = try let subst = if byhead then matches_head env sigma c t - else ConstrMatching.matches env sigma c t in + else Constr_matching.matches env sigma c t in let ok = if nowhere_except_in then Int.List.mem !pos locs else not (Int.List.mem !pos locs) in @@ -996,7 +996,7 @@ let e_contextually byhead (occs,c) f env sigma t = end else traverse_below nested envc t - with ConstrMatching.PatternMatchingFailure -> + with Constr_matching.PatternMatchingFailure -> traverse_below nested envc t and traverse_below nested envc t = (* when byhead, find other occurrences without matching again partial diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index fe648e7655..4088373ca1 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -96,8 +96,8 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) -let pf_is_matching = pf_apply ConstrMatching.is_matching_conv -let pf_matches = pf_apply ConstrMatching.matches_conv +let pf_is_matching = pf_apply Constr_matching.is_matching_conv +let pf_matches = pf_apply Constr_matching.matches_conv (********************************************) (* Definition of the most primitive tactics *) @@ -226,7 +226,7 @@ module New = struct let pf_hnf_type_of gl t = pf_whd_betadeltaiota gl (pf_get_type_of gl t) - let pf_matches gl pat t = pf_apply ConstrMatching.matches_conv gl pat t + let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t let pf_compute gl t = pf_apply compute gl t diff --git a/tactics/auto.ml b/tactics/auto.ml index ef6c38bf6c..fc4a459dec 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -129,8 +129,8 @@ let conclPattern concl pat tac = | None -> Proofview.tclUNIT Id.Map.empty | Some pat -> try - Proofview.tclUNIT (ConstrMatching.matches env sigma pat concl) - with ConstrMatching.PatternMatchingFailure -> + Proofview.tclUNIT (Constr_matching.matches env sigma pat concl) + with Constr_matching.PatternMatchingFailure -> Proofview.tclZERO (UserError ("conclPattern",str"conclPattern")) in Proofview.Goal.enter (fun gl -> diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index df8a018bb8..70490722e6 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -23,7 +23,7 @@ open Declarations open Tactics open Tacticals.New open Auto -open ConstrMatching +open Constr_matching open Hipattern open Tacmach.New open Coqlib diff --git a/tactics/equality.ml b/tactics/equality.ml index 9740f6c1f8..02d163acae 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1437,7 +1437,7 @@ let decomp_tuple_term env c t = and cdr_code = applist (mkConstU (destConstRef p2,i),[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 ConstrMatching.PatternMatchingFailure -> + with Constr_matching.PatternMatchingFailure -> [] in [((ex,exty),inner_code)]::iterated_decomp in decomprec (mkRel 1) c t @@ -1508,7 +1508,7 @@ let cutSubstInHyp l2r eqn id = let try_rewrite tac = Proofview.tclORELSE tac begin function (e, info) -> match e with - | ConstrMatching.PatternMatchingFailure -> + | Constr_matching.PatternMatchingFailure -> tclZEROMSG (str "Not a primitive equality here.") | e when catchable_exception e -> tclZEROMSG @@ -1581,7 +1581,7 @@ let unfold_body x = let restrict_to_eq_and_identity eq = (* compatibility *) if not (is_global glob_eq eq) && not (is_global glob_identity eq) - then raise ConstrMatching.PatternMatchingFailure + then raise Constr_matching.PatternMatchingFailure exception FoundHyp of (Id.t * constr * bool) @@ -1592,7 +1592,7 @@ let is_eq_x gl x (id,_,c) = let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in if (Term.eq_constr x lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true)); if (Term.eq_constr x rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false)) - with ConstrMatching.PatternMatchingFailure -> + with Constr_matching.PatternMatchingFailure -> () (* Rewrite "hyp:x=rhs" or "hyp:rhs=x" (if dir=false) everywhere and @@ -1684,7 +1684,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = if Term.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 ConstrMatching.PatternMatchingFailure -> failwith "caught" + with Constr_matching.PatternMatchingFailure -> failwith "caught" in let test p = try Some (test p) with Failure _ -> None in let hyps = pf_hyps_types gl in @@ -1700,13 +1700,13 @@ let cond_eq_term_left c t gl = try let (_,x,_) = pi3 (find_eq_data_decompose gl t) in if pf_conv_x gl c x then true else failwith "not convertible" - with ConstrMatching.PatternMatchingFailure -> failwith "not an equality" + with Constr_matching.PatternMatchingFailure -> failwith "not an equality" let cond_eq_term_right c t gl = try let (_,_,x) = pi3 (find_eq_data_decompose gl t) in if pf_conv_x gl c x then false else failwith "not convertible" - with ConstrMatching.PatternMatchingFailure -> failwith "not an equality" + with Constr_matching.PatternMatchingFailure -> failwith "not an equality" let cond_eq_term c t gl = try @@ -1714,7 +1714,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 ConstrMatching.PatternMatchingFailure -> failwith "not an equality" + with Constr_matching.PatternMatchingFailure -> failwith "not an equality" let rewrite_assumption_cond cond_eq_term cl = let rec arec hyps gl = match hyps with diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 89f6fbc747..a3862de582 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -729,7 +729,7 @@ let interp_may_eval f ist env sigma = function let (sigma,ic) = f ist env sigma c in let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in let evdref = ref sigma in - let c = subst_meta [ConstrMatching.special_meta,ic] ctxt in + let c = subst_meta [Constr_matching.special_meta,ic] ctxt in let c = Typing.solve_evars env evdref c in !evdref , c with @@ -1528,8 +1528,8 @@ and interp_letin ist llc u = fold ist.lfun llc (** [interp_match_success lz ist succ] interprets a single matching success - (of type {!TacticMatching.t}). *) -and interp_match_success ist { TacticMatching.subst ; context ; terms ; lhs } = + (of type {!Tactic_matching.t}). *) +and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } = let (>>=) = Ftactic.bind in let lctxt = Id.Map.map interp_context context in let hyp_subst = Id.Map.map Value.of_constr terms in @@ -1590,7 +1590,7 @@ and interp_match ist lz constr lmr = let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in - interp_match_successes lz ist (TacticMatching.match_term env sigma constr ilr) + interp_match_successes lz ist (Tactic_matching.match_term env sigma constr ilr) end (* Interprets the Match Context expressions *) @@ -1602,7 +1602,7 @@ and interp_match_goal ist lz lr lmr = let hyps = if lr then List.rev hyps else hyps in let concl = Proofview.Goal.concl gl in let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in - interp_match_successes lz ist (TacticMatching.match_goal env sigma hyps concl ilr) + interp_match_successes lz ist (Tactic_matching.match_goal env sigma hyps concl ilr) end (* Interprets extended tactic generic arguments *) diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml deleted file mode 100644 index 52fa2e4a2d..0000000000 --- a/tactics/tacticMatching.ml +++ /dev/null @@ -1,373 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - 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] *) -let id_map_try_add id x m = - match id with - | Some id -> Id.Map.add id x m - | None -> m - -(** Adds a binding to a {!Id.Map.t} if the name is [Name id] *) -let id_map_try_add_name id x m = - match id with - | Name id -> Id.Map.add id x m - | Anonymous -> m - -(** Takes the union of two {!Id.Map.t}. If there is conflict, - the binding of the right-hand argument shadows that of the left-hand - argument. *) -let id_map_right_biased_union m1 m2 = - if Id.Map.is_empty m1 then m2 (** Don't reconstruct the whole map *) - else Id.Map.fold Id.Map.add m2 m1 - -(** Tests whether the substitution [s] is empty. *) -let is_empty_subst (ln,lm) = - Id.Map.(is_empty ln && is_empty lm) - -(** {6 Non-linear patterns} *) - - -(** The patterns of Ltac are not necessarily linear. Non-linear - pattern are partially handled by the {!Matching} module, however - goal patterns are not primitive to {!Matching}, hence we must deal - with non-linearity between hypotheses and conclusion. Subterms are - considered equal up to the equality implemented in - [equal_instances]. *) -(* spiwack: it doesn't seem to be quite the same rule for non-linear - term patterns and non-linearity between hypotheses and/or - conclusion. Indeed, in [Matching], matching is made modulo - syntactic equality, and here we merge modulo conversion. It may be - a good idea to have an entry point of [Matching] with a partial - substitution as argument instead of merging substitution here. That - would ensure consistency. *) -let equal_instances env sigma (ctx',c') (ctx,c) = - (* How to compare instances? Do we want the terms to be convertible? - unifiable? Do we want the universe levels to be relevant? - (historically, conv_x is used) *) - CList.equal Id.equal ctx ctx' && Reductionops.is_conv env sigma c' c - - -(** Merges two substitutions. Raises [Not_coherent_metas] when - encountering two instances of the same metavariable which are not - equal according to {!equal_instances}. *) -exception Not_coherent_metas -let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) = - let merge id oc1 oc2 = match oc1, oc2 with - | None, None -> None - | None, Some c | Some c, None -> Some c - | Some c1, Some c2 -> - if equal_instances env sigma c1 c2 then Some c1 - else raise Not_coherent_metas - in - let (+++) lfun1 lfun2 = Id.Map.fold Id.Map.add lfun1 lfun2 in - (** ppedrot: Is that even correct? *) - let merged = ln +++ ln1 in - (merged, Id.Map.merge merge lcm lm) - -let matching_error = - Errors.UserError ("tactic matching" , Pp.str "No matching clauses for match.") - -let imatching_error = (matching_error, Exninfo.null) - -(** A functor is introduced to share the environment and the - evar_map. They do not change and it would be a pity to introduce - closures everywhere just for the occasional calls to - {!equal_instances}. *) -module type StaticEnvironment = sig - val env : Environ.env - val sigma : Evd.evar_map -end -module PatternMatching (E:StaticEnvironment) = struct - - - (** {6 The pattern-matching monad } *) - - - (** To focus on the algorithmic portion of pattern-matching, the - bookkeeping is relegated to a monad: the composition of the - bactracking monad of {!IStream.t} with a "writer" effect. *) - (* spiwack: as we don't benefit from the various stream optimisations - of Haskell, it may be costly to give the monad in direct style such as - here. We may want to use some continuation passing style. *) - type 'a tac = 'a Proofview.tactic - type 'a m = { stream : 'r. ('a -> unit t -> 'r tac) -> unit t -> 'r tac } - - (** The empty substitution. *) - let empty_subst = Id.Map.empty , Id.Map.empty - - (** Composes two substitutions using {!verify_metas_coherence}. It - must be a monoid with neutral element {!empty_subst}. Raises - [Not_coherent_metas] when composition cannot be achieved. *) - let subst_prod s1 s2 = - if is_empty_subst s1 then s2 - else if is_empty_subst s2 then s1 - else verify_metas_coherence E.env E.sigma s1 s2 - - (** The empty context substitution. *) - let empty_context_subst = Id.Map.empty - - (** Compose two context substitutions, in case of conflict the - right hand substitution shadows the left hand one. *) - let context_subst_prod = id_map_right_biased_union - - (** The empty term substitution. *) - let empty_term_subst = Id.Map.empty - - (** Compose two terms substitutions, in case of conflict the - right hand substitution shadows the left hand one. *) - let term_subst_prod = id_map_right_biased_union - - (** Merge two writers (and ignore the first value component). *) - let merge m1 m2 = - try Some { - subst = subst_prod m1.subst m2.subst; - context = context_subst_prod m1.context m2.context; - terms = term_subst_prod m1.terms m2.terms; - lhs = m2.lhs; - } - with Not_coherent_metas -> None - - (** Monadic [return]: returns a single success with empty substitutions. *) - let return (type a) (lhs:a) : a m = - { stream = fun k ctx -> k lhs ctx } - - (** Monadic bind: each success of [x] is replaced by the successes - of [f x]. The substitutions of [x] and [f x] are composed, - dropping the apparent successes when the substitutions are not - coherent. *) - let (>>=) (type a) (type b) (m:a m) (f:a -> b m) : b m = - { stream = fun k ctx -> m.stream (fun x ctx -> (f x).stream k ctx) ctx } - - (** A variant of [(>>=)] when the first argument returns [unit]. *) - let (<*>) (type a) (m:unit m) (y:a m) : a m = - { stream = fun k ctx -> m.stream (fun () ctx -> y.stream k ctx) ctx } - - (** Failure of the pattern-matching monad: no success. *) - let fail (type a) : a m = { stream = fun _ _ -> Proofview.tclZERO matching_error } - - let run (m : 'a m) = - let ctx = { - subst = empty_subst ; - context = empty_context_subst ; - terms = empty_term_subst ; - lhs = (); - } in - let eval lhs ctx = Proofview.tclUNIT { ctx with lhs } in - m.stream eval ctx - - (** Chooses in a list, in the same order as the list *) - let rec pick (l:'a list) (e, info) : 'a m = match l with - | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e } - | x :: l -> - { stream = fun k ctx -> Proofview.tclOR (k x ctx) (fun e -> (pick l e).stream k ctx) } - - let pick l = pick l imatching_error - - (** Declares a subsitution, a context substitution and a term substitution. *) - let put subst context terms : unit m = - let s = { subst ; context ; terms ; lhs = () } in - { stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s } - - (** Declares a substitution. *) - let put_subst subst : unit m = put subst empty_context_subst empty_term_subst - - (** Declares a term substitution. *) - let put_terms terms : unit m = put empty_subst empty_context_subst terms - - - - (** {6 Pattern-matching} *) - - - (** [wildcard_match_term lhs] matches a term against a wildcard - pattern ([_ => lhs]). It has a single success with an empty - substitution. *) - let wildcard_match_term = return - - (** [pattern_match_term refresh pat term lhs] returns the possible - matchings of [term] with the pattern [pat => lhs]. If refresh is - true, refreshes the universes of [term]. *) - let pattern_match_term refresh pat term lhs = -(* let term = if refresh then Termops.refresh_universes_strict term else term in *) - match pat with - | Term p -> - begin - try - put_subst (ConstrMatching.extended_matches E.env E.sigma p term) <*> - return lhs - with ConstrMatching.PatternMatchingFailure -> fail - end - | Subterm (with_app_context,id_ctxt,p) -> - - let rec map s (e, info) = - { stream = fun k ctx -> match IStream.peek s with - | IStream.Nil -> Proofview.tclZERO ~info e - | IStream.Cons ({ ConstrMatching.m_sub ; m_ctx }, s) -> - 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 - let nctx = { subst ; context ; terms ; lhs = () } in - match merge ctx nctx with - | None -> (map s (e, info)).stream k ctx - | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx) - } - in - map (ConstrMatching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error - - - (** [rule_match_term term rule] matches the term [term] with the - matching rule [rule]. *) - let rule_match_term term = function - | All lhs -> wildcard_match_term lhs - | Pat ([],pat,lhs) -> pattern_match_term false pat term lhs - | Pat _ -> - (** Rules with hypotheses, only work in match goal. *) - fail - - (** [match_term term rules] matches the term [term] with the set of - matching rules [rules].*) - let rec match_term (e, info) term rules = match rules with - | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e } - | r :: rules -> - { stream = fun k ctx -> - let head = rule_match_term term r in - let tail e = match_term e term rules in - Proofview.tclOR (head.stream k ctx) (fun e -> (tail e).stream k ctx) - } - - - (** [hyp_match_type hypname pat hyps] matches a single - hypothesis pattern [hypname:pat] against the hypotheses in - [hyps]. Tries the hypotheses in order. For each success returns - the name of the matched hypothesis. *) - let hyp_match_type hypname pat hyps = - pick hyps >>= fun (id,b,hyp) -> - let refresh = not (Option.is_empty b) in - pattern_match_term refresh pat hyp () <*> - put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*> - return id - - (** [hyp_match_type hypname bodypat typepat hyps] matches a single - hypothesis pattern [hypname := bodypat : typepat] against the - hypotheses in [hyps].Tries the hypotheses in order. For each - success returns the name of the matched hypothesis. *) - let hyp_match_body_and_type hypname bodypat typepat hyps = - pick hyps >>= function - | (id,Some body,hyp) -> - pattern_match_term false bodypat body () <*> - pattern_match_term true typepat hyp () <*> - put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*> - return id - | (id,None,hyp) -> fail - - (** [hyp_match pat hyps] dispatches to - {!hyp_match_type} or {!hyp_match_body_and_type} depending on whether - [pat] is [Hyp _] or [Def _]. *) - let hyp_match pat hyps = - match pat with - | Hyp ((_,hypname),typepat) -> - hyp_match_type hypname typepat hyps - | Def ((_,hypname),bodypat,typepat) -> - hyp_match_body_and_type hypname bodypat typepat hyps - - (** [hyp_pattern_list_match pats hyps lhs], matches the list of - patterns [pats] against the hypotheses in [hyps], and eventually - returns [lhs]. *) - let rec hyp_pattern_list_match pats hyps lhs = - match pats with - | pat::pats -> - hyp_match pat hyps >>= fun matched_hyp -> - (* spiwack: alternatively it is possible to return the list - with the matched hypothesis removed directly in - [hyp_match]. *) - let select_matched_hyp (id,_,_) = Id.equal id matched_hyp in - let hyps = CList.remove_first select_matched_hyp hyps in - hyp_pattern_list_match pats hyps lhs - | [] -> return lhs - - (** [rule_match_goal hyps concl rule] matches the rule [rule] - against the goal [hyps|-concl]. *) - let rule_match_goal hyps concl = function - | All lhs -> wildcard_match_term lhs - | Pat (hyppats,conclpat,lhs) -> - (* the rules are applied from the topmost one (in the concrete - syntax) to the bottommost. *) - let hyppats = List.rev hyppats in - pattern_match_term false conclpat concl () <*> - hyp_pattern_list_match hyppats hyps lhs - - (** [match_goal hyps concl rules] matches the goal [hyps|-concl] - with the set of matching rules [rules]. *) - let rec match_goal (e, info) hyps concl rules = match rules with - | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e } - | r :: rules -> - { stream = fun k ctx -> - let head = rule_match_goal hyps concl r in - let tail e = match_goal e hyps concl rules in - Proofview.tclOR (head.stream k ctx) (fun e -> (tail e).stream k ctx) - } - -end - -(** [match_term env sigma term rules] matches the term [term] with the - set of matching rules [rules]. The environment [env] and the - evar_map [sigma] are not currently used, but avoid code - duplication. *) -let match_term env sigma term rules = - let module E = struct - let env = env - let sigma = sigma - end in - let module M = PatternMatching(E) in - M.run (M.match_term imatching_error term rules) - - -(** [match_goal env sigma hyps concl rules] matches the goal - [hyps|-concl] with the set of matching rules [rules]. The - environment [env] and the evar_map [sigma] are used to check - convertibility for pattern variables shared between hypothesis - patterns or the conclusion pattern. *) -let match_goal env sigma hyps concl rules = - let module E = struct - let env = env - let sigma = sigma - end in - let module M = PatternMatching(E) in - M.run (M.match_goal imatching_error hyps concl rules) diff --git a/tactics/tacticMatching.mli b/tactics/tacticMatching.mli deleted file mode 100644 index 989f07d671..0000000000 --- a/tactics/tacticMatching.mli +++ /dev/null @@ -1,49 +0,0 @@ - (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - Evd.evar_map -> - Term.constr -> - (Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> - Tacexpr.glob_tactic_expr t Proofview.tactic - -(** [match_goal env sigma hyps concl rules] matches the goal - [hyps|-concl] with the set of matching rules [rules]. The - environment [env] and the evar_map [sigma] are used to check - convertibility for pattern variables shared between hypothesis - patterns or the conclusion pattern. *) -val match_goal: - Environ.env -> - Evd.evar_map -> - Context.named_context -> - Term.constr -> - (Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> - Tacexpr.glob_tactic_expr t Proofview.tactic diff --git a/tactics/tactic_matching.ml b/tactics/tactic_matching.ml new file mode 100644 index 0000000000..f4b13bba85 --- /dev/null +++ b/tactics/tactic_matching.ml @@ -0,0 +1,373 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + Constr_matching.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] *) +let id_map_try_add id x m = + match id with + | Some id -> Id.Map.add id x m + | None -> m + +(** Adds a binding to a {!Id.Map.t} if the name is [Name id] *) +let id_map_try_add_name id x m = + match id with + | Name id -> Id.Map.add id x m + | Anonymous -> m + +(** Takes the union of two {!Id.Map.t}. If there is conflict, + the binding of the right-hand argument shadows that of the left-hand + argument. *) +let id_map_right_biased_union m1 m2 = + if Id.Map.is_empty m1 then m2 (** Don't reconstruct the whole map *) + else Id.Map.fold Id.Map.add m2 m1 + +(** Tests whether the substitution [s] is empty. *) +let is_empty_subst (ln,lm) = + Id.Map.(is_empty ln && is_empty lm) + +(** {6 Non-linear patterns} *) + + +(** The patterns of Ltac are not necessarily linear. Non-linear + pattern are partially handled by the {!Matching} module, however + goal patterns are not primitive to {!Matching}, hence we must deal + with non-linearity between hypotheses and conclusion. Subterms are + considered equal up to the equality implemented in + [equal_instances]. *) +(* spiwack: it doesn't seem to be quite the same rule for non-linear + term patterns and non-linearity between hypotheses and/or + conclusion. Indeed, in [Matching], matching is made modulo + syntactic equality, and here we merge modulo conversion. It may be + a good idea to have an entry point of [Matching] with a partial + substitution as argument instead of merging substitution here. That + would ensure consistency. *) +let equal_instances env sigma (ctx',c') (ctx,c) = + (* How to compare instances? Do we want the terms to be convertible? + unifiable? Do we want the universe levels to be relevant? + (historically, conv_x is used) *) + CList.equal Id.equal ctx ctx' && Reductionops.is_conv env sigma c' c + + +(** Merges two substitutions. Raises [Not_coherent_metas] when + encountering two instances of the same metavariable which are not + equal according to {!equal_instances}. *) +exception Not_coherent_metas +let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) = + let merge id oc1 oc2 = match oc1, oc2 with + | None, None -> None + | None, Some c | Some c, None -> Some c + | Some c1, Some c2 -> + if equal_instances env sigma c1 c2 then Some c1 + else raise Not_coherent_metas + in + let (+++) lfun1 lfun2 = Id.Map.fold Id.Map.add lfun1 lfun2 in + (** ppedrot: Is that even correct? *) + let merged = ln +++ ln1 in + (merged, Id.Map.merge merge lcm lm) + +let matching_error = + Errors.UserError ("tactic matching" , Pp.str "No matching clauses for match.") + +let imatching_error = (matching_error, Exninfo.null) + +(** A functor is introduced to share the environment and the + evar_map. They do not change and it would be a pity to introduce + closures everywhere just for the occasional calls to + {!equal_instances}. *) +module type StaticEnvironment = sig + val env : Environ.env + val sigma : Evd.evar_map +end +module PatternMatching (E:StaticEnvironment) = struct + + + (** {6 The pattern-matching monad } *) + + + (** To focus on the algorithmic portion of pattern-matching, the + bookkeeping is relegated to a monad: the composition of the + bactracking monad of {!IStream.t} with a "writer" effect. *) + (* spiwack: as we don't benefit from the various stream optimisations + of Haskell, it may be costly to give the monad in direct style such as + here. We may want to use some continuation passing style. *) + type 'a tac = 'a Proofview.tactic + type 'a m = { stream : 'r. ('a -> unit t -> 'r tac) -> unit t -> 'r tac } + + (** The empty substitution. *) + let empty_subst = Id.Map.empty , Id.Map.empty + + (** Composes two substitutions using {!verify_metas_coherence}. It + must be a monoid with neutral element {!empty_subst}. Raises + [Not_coherent_metas] when composition cannot be achieved. *) + let subst_prod s1 s2 = + if is_empty_subst s1 then s2 + else if is_empty_subst s2 then s1 + else verify_metas_coherence E.env E.sigma s1 s2 + + (** The empty context substitution. *) + let empty_context_subst = Id.Map.empty + + (** Compose two context substitutions, in case of conflict the + right hand substitution shadows the left hand one. *) + let context_subst_prod = id_map_right_biased_union + + (** The empty term substitution. *) + let empty_term_subst = Id.Map.empty + + (** Compose two terms substitutions, in case of conflict the + right hand substitution shadows the left hand one. *) + let term_subst_prod = id_map_right_biased_union + + (** Merge two writers (and ignore the first value component). *) + let merge m1 m2 = + try Some { + subst = subst_prod m1.subst m2.subst; + context = context_subst_prod m1.context m2.context; + terms = term_subst_prod m1.terms m2.terms; + lhs = m2.lhs; + } + with Not_coherent_metas -> None + + (** Monadic [return]: returns a single success with empty substitutions. *) + let return (type a) (lhs:a) : a m = + { stream = fun k ctx -> k lhs ctx } + + (** Monadic bind: each success of [x] is replaced by the successes + of [f x]. The substitutions of [x] and [f x] are composed, + dropping the apparent successes when the substitutions are not + coherent. *) + let (>>=) (type a) (type b) (m:a m) (f:a -> b m) : b m = + { stream = fun k ctx -> m.stream (fun x ctx -> (f x).stream k ctx) ctx } + + (** A variant of [(>>=)] when the first argument returns [unit]. *) + let (<*>) (type a) (m:unit m) (y:a m) : a m = + { stream = fun k ctx -> m.stream (fun () ctx -> y.stream k ctx) ctx } + + (** Failure of the pattern-matching monad: no success. *) + let fail (type a) : a m = { stream = fun _ _ -> Proofview.tclZERO matching_error } + + let run (m : 'a m) = + let ctx = { + subst = empty_subst ; + context = empty_context_subst ; + terms = empty_term_subst ; + lhs = (); + } in + let eval lhs ctx = Proofview.tclUNIT { ctx with lhs } in + m.stream eval ctx + + (** Chooses in a list, in the same order as the list *) + let rec pick (l:'a list) (e, info) : 'a m = match l with + | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e } + | x :: l -> + { stream = fun k ctx -> Proofview.tclOR (k x ctx) (fun e -> (pick l e).stream k ctx) } + + let pick l = pick l imatching_error + + (** Declares a subsitution, a context substitution and a term substitution. *) + let put subst context terms : unit m = + let s = { subst ; context ; terms ; lhs = () } in + { stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s } + + (** Declares a substitution. *) + let put_subst subst : unit m = put subst empty_context_subst empty_term_subst + + (** Declares a term substitution. *) + let put_terms terms : unit m = put empty_subst empty_context_subst terms + + + + (** {6 Pattern-matching} *) + + + (** [wildcard_match_term lhs] matches a term against a wildcard + pattern ([_ => lhs]). It has a single success with an empty + substitution. *) + let wildcard_match_term = return + + (** [pattern_match_term refresh pat term lhs] returns the possible + matchings of [term] with the pattern [pat => lhs]. If refresh is + true, refreshes the universes of [term]. *) + let pattern_match_term refresh pat term lhs = +(* let term = if refresh then Termops.refresh_universes_strict term else term in *) + match pat with + | Term p -> + begin + try + put_subst (Constr_matching.extended_matches E.env E.sigma p term) <*> + return lhs + with Constr_matching.PatternMatchingFailure -> fail + end + | Subterm (with_app_context,id_ctxt,p) -> + + let rec map s (e, info) = + { stream = fun k ctx -> match IStream.peek s with + | IStream.Nil -> Proofview.tclZERO ~info e + | IStream.Cons ({ Constr_matching.m_sub ; m_ctx }, s) -> + 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 + let nctx = { subst ; context ; terms ; lhs = () } in + match merge ctx nctx with + | None -> (map s (e, info)).stream k ctx + | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx) + } + in + map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error + + + (** [rule_match_term term rule] matches the term [term] with the + matching rule [rule]. *) + let rule_match_term term = function + | All lhs -> wildcard_match_term lhs + | Pat ([],pat,lhs) -> pattern_match_term false pat term lhs + | Pat _ -> + (** Rules with hypotheses, only work in match goal. *) + fail + + (** [match_term term rules] matches the term [term] with the set of + matching rules [rules].*) + let rec match_term (e, info) term rules = match rules with + | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e } + | r :: rules -> + { stream = fun k ctx -> + let head = rule_match_term term r in + let tail e = match_term e term rules in + Proofview.tclOR (head.stream k ctx) (fun e -> (tail e).stream k ctx) + } + + + (** [hyp_match_type hypname pat hyps] matches a single + hypothesis pattern [hypname:pat] against the hypotheses in + [hyps]. Tries the hypotheses in order. For each success returns + the name of the matched hypothesis. *) + let hyp_match_type hypname pat hyps = + pick hyps >>= fun (id,b,hyp) -> + let refresh = not (Option.is_empty b) in + pattern_match_term refresh pat hyp () <*> + put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*> + return id + + (** [hyp_match_type hypname bodypat typepat hyps] matches a single + hypothesis pattern [hypname := bodypat : typepat] against the + hypotheses in [hyps].Tries the hypotheses in order. For each + success returns the name of the matched hypothesis. *) + let hyp_match_body_and_type hypname bodypat typepat hyps = + pick hyps >>= function + | (id,Some body,hyp) -> + pattern_match_term false bodypat body () <*> + pattern_match_term true typepat hyp () <*> + put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*> + return id + | (id,None,hyp) -> fail + + (** [hyp_match pat hyps] dispatches to + {!hyp_match_type} or {!hyp_match_body_and_type} depending on whether + [pat] is [Hyp _] or [Def _]. *) + let hyp_match pat hyps = + match pat with + | Hyp ((_,hypname),typepat) -> + hyp_match_type hypname typepat hyps + | Def ((_,hypname),bodypat,typepat) -> + hyp_match_body_and_type hypname bodypat typepat hyps + + (** [hyp_pattern_list_match pats hyps lhs], matches the list of + patterns [pats] against the hypotheses in [hyps], and eventually + returns [lhs]. *) + let rec hyp_pattern_list_match pats hyps lhs = + match pats with + | pat::pats -> + hyp_match pat hyps >>= fun matched_hyp -> + (* spiwack: alternatively it is possible to return the list + with the matched hypothesis removed directly in + [hyp_match]. *) + let select_matched_hyp (id,_,_) = Id.equal id matched_hyp in + let hyps = CList.remove_first select_matched_hyp hyps in + hyp_pattern_list_match pats hyps lhs + | [] -> return lhs + + (** [rule_match_goal hyps concl rule] matches the rule [rule] + against the goal [hyps|-concl]. *) + let rule_match_goal hyps concl = function + | All lhs -> wildcard_match_term lhs + | Pat (hyppats,conclpat,lhs) -> + (* the rules are applied from the topmost one (in the concrete + syntax) to the bottommost. *) + let hyppats = List.rev hyppats in + pattern_match_term false conclpat concl () <*> + hyp_pattern_list_match hyppats hyps lhs + + (** [match_goal hyps concl rules] matches the goal [hyps|-concl] + with the set of matching rules [rules]. *) + let rec match_goal (e, info) hyps concl rules = match rules with + | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e } + | r :: rules -> + { stream = fun k ctx -> + let head = rule_match_goal hyps concl r in + let tail e = match_goal e hyps concl rules in + Proofview.tclOR (head.stream k ctx) (fun e -> (tail e).stream k ctx) + } + +end + +(** [match_term env sigma term rules] matches the term [term] with the + set of matching rules [rules]. The environment [env] and the + evar_map [sigma] are not currently used, but avoid code + duplication. *) +let match_term env sigma term rules = + let module E = struct + let env = env + let sigma = sigma + end in + let module M = PatternMatching(E) in + M.run (M.match_term imatching_error term rules) + + +(** [match_goal env sigma hyps concl rules] matches the goal + [hyps|-concl] with the set of matching rules [rules]. The + environment [env] and the evar_map [sigma] are used to check + convertibility for pattern variables shared between hypothesis + patterns or the conclusion pattern. *) +let match_goal env sigma hyps concl rules = + let module E = struct + let env = env + let sigma = sigma + end in + let module M = PatternMatching(E) in + M.run (M.match_goal imatching_error hyps concl rules) diff --git a/tactics/tactic_matching.mli b/tactics/tactic_matching.mli new file mode 100644 index 0000000000..abeb47c3b9 --- /dev/null +++ b/tactics/tactic_matching.mli @@ -0,0 +1,49 @@ + (************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + Evd.evar_map -> + Term.constr -> + (Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> + Tacexpr.glob_tactic_expr t Proofview.tactic + +(** [match_goal env sigma hyps concl rules] matches the goal + [hyps|-concl] with the set of matching rules [rules]. The + environment [env] and the evar_map [sigma] are used to check + convertibility for pattern variables shared between hypothesis + patterns or the conclusion pattern. *) +val match_goal: + Environ.env -> + Evd.evar_map -> + Context.named_context -> + Term.constr -> + (Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list -> + Tacexpr.glob_tactic_expr t Proofview.tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 26fd773232..d52d2786d6 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1979,7 +1979,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 ConstrMatching.PatternMatchingFailure + -> raise Constr_matching.PatternMatchingFailure let intro_decomp_eq loc l thin tac id = Proofview.Goal.nf_enter begin fun gl -> diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 46f2abd7f5..2c5edc20ed 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -20,7 +20,7 @@ Tacenv Hints Auto Tacintern -TacticMatching +Tactic_matching Tacinterp Evar_tactics Term_dnet diff --git a/toplevel/search.ml b/toplevel/search.ml index 26e6416a9a..6b0692679b 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -112,7 +112,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 ConstrMatching.is_matching env Evd.empty pat typ then true + if Constr_matching.is_matching env Evd.empty pat typ then true else match kind_of_term typ with | Prod (_, _, typ) | LetIn (_, _, _, typ) -> pattern_filter pat ref env typ @@ -120,7 +120,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 ConstrMatching.is_matching_head env Evd.empty pat typ then true + if Constr_matching.is_matching_head env Evd.empty pat typ then true else match kind_of_term typ with | Prod (_, _, typ) | LetIn (_, _, _, typ) -> head_filter pat ref env typ @@ -149,7 +149,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 -> - ConstrMatching.is_matching_appsubterm ~closed:false env Evd.empty pat typ + Constr_matching.is_matching_appsubterm ~closed:false env Evd.empty pat typ | GlobSearchString s -> String.string_contains ~where:(name_of_reference gr) ~what:s @@ -288,11 +288,11 @@ let interface_search flags = toggle (Str.string_match regexp id 0) flag in let match_type (pat, flag) = - toggle (ConstrMatching.is_matching env Evd.empty pat constr) flag + toggle (Constr_matching.is_matching env Evd.empty pat constr) flag in let match_subtype (pat, flag) = toggle - (ConstrMatching.is_matching_appsubterm ~closed:false + (Constr_matching.is_matching_appsubterm ~closed:false env Evd.empty pat constr) flag in let match_module (mdl, flag) = -- cgit v1.2.3