diff options
Diffstat (limited to 'pretyping/pattern.mli')
| -rw-r--r-- | pretyping/pattern.mli | 71 |
1 files changed, 56 insertions, 15 deletions
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index 195fecfe..cde6d4dc 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -1,14 +1,14 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pattern.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) +(** This module defines the type of pattern used for pattern-matching + terms in tatics *) -(*i*) open Pp open Names open Sign @@ -16,17 +16,55 @@ open Term open Environ open Libnames open Nametab -open Rawterm +open Glob_term open Mod_subst -(*i*) -(* Types of substitutions with or w/o bound 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 type extended_patvar_map = (patvar * constr_under_binders) list -(* Patterns *) +(** {5 Patterns} *) + +type case_info_pattern = + { cip_style : case_style; + cip_ind : inductive option; + cip_ind_args : (int * int) option; (** number of params and args *) + cip_extensible : bool (** does this match end with _ => _ ? *) } type constr_pattern = | PRef of global_reference @@ -38,14 +76,17 @@ type constr_pattern = | PLambda of name * constr_pattern * constr_pattern | PProd of name * constr_pattern * constr_pattern | PLetIn of name * constr_pattern * constr_pattern - | PSort of rawsort + | PSort of glob_sort | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern - | PCase of (case_style * int array * inductive option * (int * int) option) - * constr_pattern * constr_pattern * constr_pattern array + | PCase of case_info_pattern * constr_pattern * constr_pattern * + (int * int * constr_pattern) list (** index of constructor, nb of args *) | PFix of fixpoint | PCoFix of cofixpoint +(** Nota : in a [PCase], the array of branches might be shorter than + expected, denoting the use of a final "_ => _" branch *) + (** {5 Functions on patterns} *) val occur_meta_pattern : constr_pattern -> bool @@ -54,28 +95,28 @@ val subst_pattern : substitution -> constr_pattern -> constr_pattern exception BoundPattern -(* [head_pattern_bound t] extracts the head variable/constant of the +(** [head_pattern_bound t] extracts the head variable/constant of the type [t] or raises [BoundPattern] (even if a sort); it raises an anomaly if [t] is an abstraction *) val head_pattern_bound : constr_pattern -> global_reference -(* [head_of_constr_reference c] assumes [r] denotes a reference and +(** [head_of_constr_reference c] assumes [r] denotes a reference and returns its label; raises an anomaly otherwise *) val head_of_constr_reference : Term.constr -> global_reference -(* [pattern_of_constr c] translates a term [c] with metavariables into +(** [pattern_of_constr c] translates a term [c] with metavariables into a pattern; currently, no destructor (Cases, Fix, Cofix) and no existential variable are allowed in [c] *) val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern -(* [pattern_of_rawconstr l c] translates a term [c] with metavariables into +(** [pattern_of_glob_constr l c] translates a term [c] with metavariables into a pattern; variables bound in [l] are replaced by the pattern to which they are bound *) -val pattern_of_rawconstr : rawconstr -> +val pattern_of_glob_constr : glob_constr -> patvar list * constr_pattern val instantiate_pattern : |