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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
(* $Id$ *)
(*i*)
open Util
open Names
open Term
open Sign
open Evd
open Pattern
open Proof_trees
(*i*)
(* The pattern table for tactics. *)
(* The idea is that we want to write tactic files which are only
"activated" when certain modules are loaded and imported. Already,
the question of how to store the tactics is hard, and we will not
address that here. However, the question arises of how to store
the patterns that we will want to use for term-destructuring, and
the solution proposed is that we will store patterns with a
"module-marker", telling us which modules have to be open in order
to use the pattern. So we will write:
\begin{verbatim}
let mark = make_module_marker ["<module-name>";<module-name>;...];;
let p1 = put_pat mark "<parseable pattern goes here>";;
\end{verbatim}
And now, we can use [(get p1)]
to get the term which corresponds to this pattern, already parsed
and with the global names adjusted.
In other words, we will have the term which we would have had if we
had done an:
\begin{verbatim}
constr_of_com mt_ctxt (initial_sign()) "<text here>"
\end{verbatim}
except that it will be computed at module-opening time, rather than
at tactic-application time. The ONLY difference will be that
no implicit syntax resolution will happen. *)
(* A pattern is intented to be pattern-matched (using functions
[somatch] and co), while a squeleton is a term with holes intented to
be substituted by [soinstance] *)
(*s First part : introduction of term patterns and term squeletons *)
(* [make_module_marker modl] makes a key from the list of
vernacular modules [modl] where names in a pattern or squeleton has
to be searched *)
type module_mark = Stock.module_mark
val make_module_marker : string list -> module_mark
(* [put_pat mmk s] declares a pattern [s] to be parsed using the
definitions in the modules associated to the key [mmk] *)
type marked_pattern
val put_pat : module_mark -> string -> marked_pattern
val get_pat : marked_pattern -> constr_pattern
(* [put_squel mmk s] declares an open term [s] to be parsed using the
definitions in the modules associated to the key [mmk] *)
type marked_term
val put_squel : module_mark -> string -> marked_term
(*i val get_squel : marked_term -> constr i*)
(*i Remplacé par Astterm.interp_constrpattern
val raw_sopattern_of_compattern : Environ.env -> Coqast.t -> constr
i*)
(* [get_reference mods id] interprets [id] as a global identifier
assuming defined in the modules listed in [mods] *)
val get_reference : string list -> string -> constr
(*s Second part : Given a term with second-order variables in it,
represented by Meta's, and possibly applied using \verb!XTRA[$SOAPP]! to
terms, this function will perform second-order, binding-preserving,
matching, in the case where the pattern is a pattern in the sense
of Dale Miller.
ALGORITHM:
Given a pattern, we decompose it, flattening casts and apply's,
recursing on all operators, and pushing the name of the binder each
time we descend a binder.
When we reach a first-order variable, we ask that the corresponding
term's free-rels all be higher than the depth of the current stack.
When we reach a second-order application, we ask that the
intersection of the free-rels of the term and the current stack be
contained in the arguments of the application, and in that case, we
construct a [DLAM] with the names on the stack. *)
(* [dest_somatch c pat] matches [c] against [pat] and returns the resulting
assignment of metavariables; it raises [PatternMatchingFailure] if
not matchable *)
(*i
val dest_somatch : constr -> marked_pattern -> constr list
(* [somatches c pat] just tells if [c] matches against [pat] *)
val somatches : constr -> marked_pattern -> bool
(* [dest_somatch_conv env sigma] matches up to conversion in
environment [(env,sgima)] when constants in pattern are concerned;
it raises [PatternMatchingFailure] if not matchable *)
val dest_somatch_conv :
Environ.env -> 'a evar_map -> constr -> marked_pattern -> (int * constr) list
(* [somatches_conv env sigma c pat] tells if [c] matches against [pat]
up to conversion for constants in patterns *)
val somatches_conv :
Environ.env -> 'a evar_map -> constr -> marked_pattern -> bool
i*)
val soinstance : marked_term -> constr list -> constr
(* This works only for squeleton without metavariables *)
val get_squel : marked_term -> constr
val is_imp_term : constr -> bool
(*s I implemented the following functions which test whether a term [t]
is an inductive but non-recursive type, a general conjuction, a
general disjunction, or a type with no constructors.
They are more general than matching with [or_term], [and_term], etc,
since they do not depend on the name of the type. Hence, they
also work on ad-hoc disjunctions introduced by the user.
(Eduardo, 6/8/97). *)
type 'a matching_function = constr -> 'a option
type testing_function = constr -> bool
val match_with_non_recursive_type : (constr * constr list) matching_function
val is_non_recursive_type : testing_function
val match_with_disjunction : (constr * constr list) matching_function
val is_disjunction : testing_function
val match_with_conjunction : (constr * constr list) matching_function
val is_conjunction : testing_function
val match_with_empty_type : constr matching_function
val is_empty_type : testing_function
val match_with_unit_type : constr matching_function
val is_unit_type : testing_function
val match_with_equation : (constr * constr list) matching_function
val is_equation : testing_function
val match_with_nottype : (constr * constr) matching_function
val is_nottype : testing_function
|
