diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:08:53 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:08:53 +0000 |
commit | 8a71afd27620a5d6c507b115d6fd408d879544c5 (patch) | |
tree | 7365991d6afdfeae8529b5d47e3830b63a037a56 /pretyping | |
parent | 392300a73bc4e57d2be865d9a8d77c608ef02f59 (diff) |
Pattern as a mli-only file, operations in Patternops
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15376 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/matching.ml | 1 | ||||
-rw-r--r-- | pretyping/pattern.mli | 127 | ||||
-rw-r--r-- | pretyping/patternops.ml (renamed from pretyping/pattern.ml) | 41 | ||||
-rw-r--r-- | pretyping/patternops.mli | 57 | ||||
-rw-r--r-- | pretyping/pretyping.mllib | 2 | ||||
-rw-r--r-- | pretyping/tacred.ml | 1 |
6 files changed, 64 insertions, 165 deletions
diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 6be95cd82..554face37 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -20,6 +20,7 @@ open Glob_term open Sign open Environ open Pattern +open Patternops open Misctypes (*i*) diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli deleted file mode 100644 index f9c2358b7..000000000 --- a/pretyping/pattern.mli +++ /dev/null @@ -1,127 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <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 *) -(************************************************************************) - -(** This module defines the type of pattern used for pattern-matching - terms in tatics *) - -open Pp -open Names -open Sign -open Term -open Environ -open Libnames -open Nametab -open Glob_term -open Mod_subst -open Misctypes - -(** {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 - -(** {5 Patterns} *) - -type case_info_pattern = - { cip_style : case_style; - cip_ind : inductive option; - cip_ind_args : int option; (** number of params and args *) - cip_extensible : bool (** does this match end with _ => _ ? *) } - -type constr_pattern = - | PRef of global_reference - | PVar of identifier - | PEvar of existential_key * constr_pattern array - | PRel of int - | PApp of constr_pattern * constr_pattern array - | PSoApp of patvar * constr_pattern list - | PLambda of name * constr_pattern * constr_pattern - | PProd of name * constr_pattern * constr_pattern - | PLetIn of name * constr_pattern * constr_pattern - | PSort of glob_sort - | PMeta of patvar option - | PIf of constr_pattern * constr_pattern * constr_pattern - | 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 - -val subst_pattern : substitution -> constr_pattern -> constr_pattern - -exception BoundPattern - -(** [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 - 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 - 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_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_glob_constr : glob_constr -> - patvar list * constr_pattern - -val instantiate_pattern : - Evd.evar_map -> (identifier * (identifier list * constr)) list -> - constr_pattern -> constr_pattern - -val lift_pattern : int -> constr_pattern -> constr_pattern diff --git a/pretyping/pattern.ml b/pretyping/patternops.ml index 08e5ac75c..244d03021 100644 --- a/pretyping/pattern.ml +++ b/pretyping/patternops.ml @@ -20,39 +20,8 @@ open Pp open Mod_subst open Misctypes open Decl_kinds - -(* Metavariables *) - -type constr_under_binders = identifier list * constr - -type patvar_map = (patvar * constr) list -type extended_patvar_map = (patvar * constr_under_binders) list - -(* Patterns *) - -type case_info_pattern = - { cip_style : case_style; - cip_ind : inductive option; - cip_ind_args : int option; (** number of args *) - cip_extensible : bool (** does this match end with _ => _ ? *) } - -type constr_pattern = - | PRef of global_reference - | PVar of identifier - | PEvar of existential_key * constr_pattern array - | PRel of int - | PApp of constr_pattern * constr_pattern array - | PSoApp of patvar * constr_pattern list - | PLambda of name * constr_pattern * constr_pattern - | PProd of name * constr_pattern * constr_pattern - | PLetIn of name * constr_pattern * constr_pattern - | PSort of glob_sort - | PMeta of patvar option - | PIf of constr_pattern * constr_pattern * constr_pattern - | PCase of case_info_pattern * constr_pattern * constr_pattern * - (int * int * constr_pattern) list (** constructor index, nb of args *) - | PFix of fixpoint - | PCoFix of cofixpoint +open Pattern +open Evd let rec occur_meta_pattern = function | PApp (f,args) -> @@ -94,8 +63,6 @@ let head_of_constr_reference c = match kind_of_term c with | Var id -> VarRef id | _ -> anomaly "Not a rigid reference" -open Evd - let pattern_of_constr sigma t = let ctx = ref [] in let rec pattern_of_constr t = @@ -111,7 +78,7 @@ let pattern_of_constr sigma t = | Prod (na,c,b) -> PProd (na,pattern_of_constr c,pattern_of_constr b) | Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b) | App (f,a) -> - (match + (match match kind_of_term f with Evar (evk,args as ev) -> (match snd (Evd.evar_source evk sigma) with @@ -377,5 +344,5 @@ and pats_of_glob_branches loc metas vars ind brs = let pattern_of_glob_constr c = let metas = ref [] in - let p = pat_of_raw metas [] c in + let p = pat_of_raw metas [] c in (!metas,p) diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli new file mode 100644 index 000000000..74e5a81ae --- /dev/null +++ b/pretyping/patternops.mli @@ -0,0 +1,57 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 *) +(************************************************************************) + +open Pp +open Names +open Sign +open Term +open Environ +open Libnames +open Nametab +open Glob_term +open Mod_subst +open Misctypes +open Pattern + +(** {5 Functions on patterns} *) + +val occur_meta_pattern : constr_pattern -> bool + +val subst_pattern : substitution -> constr_pattern -> constr_pattern + +exception BoundPattern + +(** [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 + 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 + 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_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_glob_constr : glob_constr -> + patvar list * constr_pattern + +val instantiate_pattern : + Evd.evar_map -> (identifier * (identifier list * constr)) list -> + constr_pattern -> constr_pattern + +val lift_pattern : int -> constr_pattern -> constr_pattern diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index fca2d714f..2d25b1413 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -17,7 +17,7 @@ Typing Miscops Glob_ops Redops -Pattern +Patternops Matching Tacred Typeclasses_errors diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 6ff469012..05136d25d 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -24,6 +24,7 @@ open Reductionops open Cbv open Glob_term open Pattern +open Patternops open Matching open Locus |