diff options
Diffstat (limited to 'pretyping/pattern.mli')
| -rw-r--r-- | pretyping/pattern.mli | 48 |
1 files changed, 44 insertions, 4 deletions
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index d805730e97..3b61c1e437 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -6,6 +6,9 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) +(** This module defines the type of pattern used for pattern-matching + terms in tatics *) + open Pp open Names open Sign @@ -16,12 +19,46 @@ open Nametab open Rawterm open Mod_subst -(** Pattern variables *) +(** {5 Maps of pattern variables} *) + +(** Type [constr_under_binders] is for representing the term resulting + of a matching. Matching can return terms defined in a some context + of named binders; in the context, variable names are ordered by + (<) and referred to by index in the term Thanks to the canonical + ordering, a matching problem like + + [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]] + + will be accepted. Thanks to the reference by index, a matching + problem like + + [match ... with [(fun x => ?p)] => [forall x => p]] + + will work even if [x] is also the name of an existing goal + variable. + + Note: we do not keep types in the signature. Besides simplicity, + the main reason is that it would force to close the signature over + binders that occur only in the types of effective binders but not + in the term itself (e.g. for a term [f x] with [f:A -> True] and + [x:A]). + + On the opposite side, by not keeping the types, we loose + opportunity to propagate type informations which otherwise would + not be inferable, as e.g. when matching [forall x, x = 0] with + pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in + expression [forall x, h = x] where nothing tells how the type of x + could be inferred. We also loose the ability of typing ltac + variables before calling the right-hand-side of ltac matching clauses. *) + +type constr_under_binders = identifier list * constr + +(** Types of substitutions with or w/o bound variables *) type patvar_map = (patvar * constr) list -val pr_patvar : patvar -> std_ppcmds +type extended_patvar_map = (patvar * constr_under_binders) list -(** Patterns *) +(** {5 Patterns} *) type constr_pattern = | PRef of global_reference @@ -41,6 +78,8 @@ type constr_pattern = | PFix of fixpoint | PCoFix of cofixpoint +(** {5 Functions on patterns} *) + val occur_meta_pattern : constr_pattern -> bool val subst_pattern : substitution -> constr_pattern -> constr_pattern @@ -72,6 +111,7 @@ val pattern_of_rawconstr : rawconstr -> patvar list * constr_pattern val instantiate_pattern : - (identifier * constr_pattern Lazy.t) list -> constr_pattern -> constr_pattern + (identifier * (identifier list * constr)) list -> + constr_pattern -> constr_pattern val lift_pattern : int -> constr_pattern -> constr_pattern |