diff options
Diffstat (limited to 'pretyping/matching.mli')
| -rw-r--r-- | pretyping/matching.mli | 42 |
1 files changed, 35 insertions, 7 deletions
diff --git a/pretyping/matching.mli b/pretyping/matching.mli index e6065c68..b54a17b7 100644 --- a/pretyping/matching.mli +++ b/pretyping/matching.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: matching.mli 6616 2005-01-21 17:18:23Z herbelin $ i*) +(*i $Id: matching.mli 11739 2009-01-02 19:33:19Z herbelin $ i*) (*i*) open Names @@ -22,30 +22,58 @@ exception PatternMatchingFailure val special_meta : metavariable +type bound_ident_map = (identifier * identifier) list + (* [matches pat c] matches [c] against [pat] and returns the resulting assignment of metavariables; it raises [PatternMatchingFailure] if not matchable; bindings are given in increasing order based on the numbers given in the pattern *) val matches : constr_pattern -> constr -> patvar_map -(* [is_matching pat c] just tells if [c] matches against [pat] *) +(* [extended_matches pat c] also returns the names of bound variables + in [c] that matches the bound variables in [pat]; if several bound + variables or metavariables have the same name, the metavariable, + or else the rightmost bound variable, takes precedence *) +val extended_matches : + constr_pattern -> constr -> bound_ident_map * patvar_map +(* [is_matching pat c] just tells if [c] matches against [pat] *) val is_matching : constr_pattern -> constr -> bool (* [matches_conv env sigma] matches up to conversion in environment [(env,sigma)] when constants in pattern are concerned; it raises [PatternMatchingFailure] if not matchable; bindings are given in increasing order based on the numbers given in the pattern *) - val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map +(* The type of subterm matching results: a substitution + a context + (whose hole is denoted with [special_meta]) + a continuation that + either returns the next matching subterm or raise PatternMatchingFailure *) +type subterm_matching_result = + (bound_ident_map * patvar_map) * constr * (unit -> subterm_matching_result) + (* [match_subterm n pat c] returns the substitution and the context - corresponding to the [n+1]th **closed** subterm of [c] matching [pat]; - It raises PatternMatchingFailure if no such matching exists *) -val match_subterm : int -> constr_pattern -> constr -> patvar_map * constr + corresponding to the first **closed** subterm of [c] matching [pat], and + a continuation that looks for the next matching subterm. + It raises PatternMatchingFailure if no subterm matches the pattern *) +val match_subterm : constr_pattern -> constr -> subterm_matching_result + +(* [match_appsubterm pat c] returns the substitution and the context + corresponding to the first **closed** subterm of [c] matching [pat], + considering application contexts as well. It also returns a + continuation that looks for the next matching subterm. + It raises PatternMatchingFailure if no subterm matches the pattern *) +val match_appsubterm : constr_pattern -> constr -> subterm_matching_result + +(* [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *) +val match_subterm_gen : bool (* true = with app context *) -> + constr_pattern -> constr -> subterm_matching_result + +(* [is_matching_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 |