1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
(************************************************************************)
(* 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
(** {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 * 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
|
