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
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: topconstr.mli 9976 2007-07-12 11:58:30Z msozeau $ i*)
(*i*)
open Pp
open Util
open Names
open Libnames
open Rawterm
open Term
open Mod_subst
(*i*)
(*s This is the subtype of rawconstr allowed in syntactic extensions *)
(* No location since intended to be substituted at any place of a text *)
(* Complex expressions such as fixpoints and cofixpoints are excluded, *)
(* non global expressions such as existential variables also *)
type aconstr =
(* Part common to [rawconstr] and [cases_pattern] *)
| ARef of global_reference
| AVar of identifier
| AApp of aconstr * aconstr list
| AList of identifier * identifier * aconstr * aconstr * bool
(* Part only in [rawconstr] *)
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
| ACases of aconstr option *
(aconstr * (name * (inductive * int * name list) option)) list *
(cases_pattern list * aconstr) list
| ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
| AIf of aconstr * (name * aconstr option) * aconstr * aconstr
| ASort of rawsort
| AHole of Evd.hole_kind
| APatVar of patvar
| ACast of aconstr * aconstr cast_type
(**********************************************************************)
(* Translate a rawconstr into a notation given the list of variables *)
(* bound by the notation; also interpret recursive patterns *)
val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
(* Name of the special identifier used to encode recursive notations *)
val ldots_var : identifier
(* Equality of rawconstr (warning: only partially implemented) *)
val eq_rawconstr : rawconstr -> rawconstr -> bool
(**********************************************************************)
(* Re-interpret a notation as a rawconstr, taking care of binders *)
val rawconstr_of_aconstr_with_binders : loc ->
('a -> identifier -> 'a * identifier) ->
('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr
val rawconstr_of_aconstr : loc -> aconstr -> rawconstr
(**********************************************************************)
(* Substitution of kernel names, avoiding a list of bound identifiers *)
val subst_aconstr : substitution -> identifier list -> aconstr -> aconstr
(**********************************************************************)
(* [match_aconstr metas] matches a rawconstr against an aconstr with *)
(* metavariables in [metas]; raise [No_match] if the matching fails *)
exception No_match
type scope_name = string
type tmp_scope_name = scope_name
type interpretation =
(identifier * (tmp_scope_name option * scope_name list)) list * aconstr
val match_aconstr : rawconstr -> interpretation ->
(rawconstr * (tmp_scope_name option * scope_name list)) list
(**********************************************************************)
(*s Concrete syntax for terms *)
type notation = string
type explicitation = ExplByPos of int | ExplByName of identifier
type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
type prim_token = Numeral of Bigint.bigint | String of string
type cases_pattern_expr =
| CPatAlias of loc * cases_pattern_expr * identifier
| CPatCstr of loc * reference * cases_pattern_expr list
| CPatAtom of loc * reference option
| CPatOr of loc * cases_pattern_expr list
| CPatNotation of loc * notation * cases_pattern_expr list
| CPatPrim of loc * prim_token
| CPatDelimiters of loc * string * cases_pattern_expr
type constr_expr =
| CRef of reference
| CFix of loc * identifier located * fixpoint_expr list
| CCoFix of loc * identifier located * cofixpoint_expr list
| CArrow of loc * constr_expr * constr_expr
| CProdN of loc * (name located list * constr_expr) list * constr_expr
| CLambdaN of loc * (name located list * constr_expr) list * constr_expr
| CLetIn of loc * name located * constr_expr * constr_expr
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
| CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
| CCases of loc * constr_expr option *
(constr_expr * (name option * constr_expr option)) list *
(loc * cases_pattern_expr list list * constr_expr) list
| CLetTuple of loc * name list * (name option * constr_expr option) *
constr_expr * constr_expr
| CIf of loc * constr_expr * (name option * constr_expr option)
* constr_expr * constr_expr
| CHole of loc
| CPatVar of loc * (bool * patvar)
| CEvar of loc * existential_key
| CSort of loc * rawsort
| CCast of loc * constr_expr * constr_expr cast_type
| CNotation of loc * notation * constr_expr list
| CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
and fixpoint_expr =
identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
and cofixpoint_expr =
identifier * local_binder list * constr_expr * constr_expr
and recursion_order_expr =
| CStructRec
| CWfRec of constr_expr
| CMeasureRec of constr_expr
and local_binder =
| LocalRawDef of name located * constr_expr
| LocalRawAssum of name located list * constr_expr
(**********************************************************************)
(* Utilities on constr_expr *)
val constr_loc : constr_expr -> loc
val cases_pattern_expr_loc : cases_pattern_expr -> loc
val replace_vars_constr_expr :
(identifier * identifier) list -> constr_expr -> constr_expr
val free_vars_of_constr_expr : constr_expr -> Idset.t
val occur_var_constr_expr : identifier -> constr_expr -> bool
(* Specific function for interning "in indtype" syntax of "match" *)
val ids_of_cases_indtype : constr_expr -> identifier list
val mkIdentC : identifier -> constr_expr
val mkRefC : reference -> constr_expr
val mkAppC : constr_expr * constr_expr list -> constr_expr
val mkCastC : constr_expr * constr_expr cast_type -> constr_expr
val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr
val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
val mkProdC : name located list * constr_expr * constr_expr -> constr_expr
val coerce_to_id : constr_expr -> identifier located
val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
(* For binders parsing *)
(* Includes let binders *)
val local_binders_length : local_binder list -> int
(* Excludes let binders *)
val local_assums_length : local_binder list -> int
(* Does not take let binders into account *)
val names_of_local_assums : local_binder list -> name located list
(* With let binders *)
val names_of_local_binders : local_binder list -> name located list
(* Used in correctness and interface; absence of var capture not guaranteed *)
(* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
val map_constr_expr_with_binders :
(identifier -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) ->
'a -> constr_expr -> constr_expr
(**********************************************************************)
(* Concrete syntax for modules and module types *)
type with_declaration_ast =
| CWith_Module of identifier list located * qualid located
| CWith_Definition of identifier list located * constr_expr
type module_type_ast =
| CMTEident of qualid located
| CMTEwith of module_type_ast * with_declaration_ast
type module_ast =
| CMEident of qualid located
| CMEapply of module_ast * module_ast
|
