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
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
|
(* $Id$ *)
open Util
open Names
open Generic
open Term
open Sign
open Constant
open Inductive
open Reduction
open Libobject
open Lib
open Impargs
open Indrec
type strength =
| DischargeAt of section_path
| NeverDischarge
let make_strength = function
| [] -> NeverDischarge
| l -> DischargeAt (sp_of_wd l)
let make_strength_0 () = make_strength (Lib.cwd())
let make_strength_1 () =
let path = try List.tl (List.tl (Lib.cwd())) with Failure _ -> [] in
make_strength path
let make_strength_2 () =
let path = try List.tl (Lib.cwd()) with Failure _ -> [] in
make_strength path
(* Variables. *)
type variable_declaration = constr * strength * bool
let vartab = ref (Spmap.empty : (identifier * variable_declaration) Spmap.t)
let _ = Summary.declare_summary "VARIABLE"
{ Summary.freeze_function = (fun () -> !vartab);
Summary.unfreeze_function = (fun ft -> vartab := ft);
Summary.init_function = (fun () -> vartab := Spmap.empty) }
let cache_variable (sp,(id,(ty,_,_) as vd)) =
Global.push_var (id,ty);
Nametab.push id sp;
declare_var_implicits id;
vartab := Spmap.add sp vd !vartab
let load_variable _ =
anomaly "we shouldn't load a variable"
let open_variable _ =
anomaly "we shouldn't open a variable"
let specification_variable _ =
anomaly "we shouldn't extract the specification of a variable"
let (in_variable, out_variable) =
let od = {
cache_function = cache_variable;
load_function = load_variable;
open_function = open_variable;
specification_function = specification_variable } in
declare_object ("VARIABLE", od)
let declare_variable id ((ty,_,_) as obj) =
Global.push_var (id,ty);
let sp = add_leaf id CCI (in_variable (id,obj)) in
Nametab.push id sp;
declare_var_implicits id
(* Parameters. *)
let cache_parameter (sp,c) =
Global.add_parameter sp c;
Nametab.push (basename sp) sp;
declare_constant_implicits sp
let open_parameter (sp,_) =
Nametab.push (basename sp) sp;
declare_constant_implicits sp
let specification_parameter obj = obj
let (in_parameter, out_parameter) =
let od = {
cache_function = cache_parameter;
load_function = (fun _ -> ());
open_function = open_parameter;
specification_function = specification_parameter } in
declare_object ("PARAMETER", od)
let declare_parameter id c =
let sp = add_leaf id CCI (in_parameter c) in
Global.add_parameter sp c;
Nametab.push (basename sp) sp;
declare_constant_implicits sp
(* Constants. *)
type constant_declaration = constant_entry * strength * bool
let csttab = ref (Spmap.empty : constant_declaration Spmap.t)
let _ = Summary.declare_summary "CONSTANT"
{ Summary.freeze_function = (fun () -> !vartab);
Summary.unfreeze_function = (fun ft -> vartab := ft);
Summary.init_function = (fun () -> vartab := Spmap.empty) }
let cache_constant (sp,ce) =
Global.add_constant sp ce;
Nametab.push (basename sp) sp;
declare_constant_implicits sp
let open_constant (sp,_) =
Nametab.push (basename sp) sp;
declare_constant_implicits sp
let specification_constant obj = obj
let (in_constant, out_constant) =
let od = {
cache_function = cache_constant;
load_function = (fun _ -> ());
open_function = open_constant;
specification_function = specification_constant } in
declare_object ("CONSTANT", od)
let declare_constant id ((ce,_,_) as cd) =
let sp = add_leaf id CCI (in_constant ce) in
Global.add_constant sp ce;
Nametab.push (basename sp) sp;
declare_constant_implicits sp
(* Inductives. *)
let push_inductive_names sp mie =
List.iter
(fun (id,_,cnames,_) ->
Nametab.push id sp;
List.iter (fun x -> Nametab.push x sp) cnames)
mie.mind_entry_inds
let cache_inductive (sp,mie) =
Global.add_mind sp mie;
push_inductive_names sp mie;
declare_inductive_implicits sp
let open_inductive (sp,mie) =
push_inductive_names sp mie;
declare_inductive_implicits sp
let specification_inductive obj = obj
let (in_inductive, out_inductive) =
let od = {
cache_function = cache_inductive;
load_function = (fun _ -> ());
open_function = open_inductive;
specification_function = specification_inductive } in
declare_object ("INDUCTIVE", od)
let declare_mind mie =
let id = match mie.mind_entry_inds with
| (id,_,_,_)::_ -> id
| [] -> anomaly "cannot declare an empty list of inductives"
in
let sp = add_leaf id CCI (in_inductive mie) in
Global.add_mind sp mie;
push_inductive_names sp mie;
declare_inductive_implicits sp
(* Test and access functions. *)
let is_constant sp =
try let _ = Global.lookup_constant sp in true with Not_found -> false
let constant_strength sp = failwith "TODO"
let is_variable id =
let sp = Nametab.sp_of_id CCI id in Spmap.mem sp !vartab
let out_variable sp =
let (id,(_,str,sticky)) = Spmap.find sp !vartab in
let (_,ty) = Global.lookup_var id in
(id,ty,str,sticky)
let variable_strength id =
let sp = Nametab.sp_of_id CCI id in
let _,(_,str,_) = Spmap.find sp !vartab in
str
(* Global references. *)
let first f v =
let n = Array.length v in
let rec look_for i =
if i = n then raise Not_found;
try f i v.(i) with Not_found -> look_for (succ i)
in
look_for 0
let mind_oper_of_id sp id mib =
first
(fun tyi mip ->
if id = mip.mind_typename then
MutInd (sp,tyi)
else
first
(fun cj cid ->
if id = cid then
MutConstruct((sp,tyi),succ cj)
else raise Not_found)
mip.mind_consnames)
mib.mind_packets
let global_operator sp id =
try
let cb = Global.lookup_constant sp in Const sp, cb.const_hyps
with Not_found ->
let mib = Global.lookup_mind sp in
mind_oper_of_id sp id mib, mib.mind_hyps
let global_reference kind id =
let sp = Nametab.sp_of_id kind id in
let (oper,_) = global_operator sp id in
let hyps = Global.var_context () in
let ids = ids_of_sign hyps in
DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
let global_reference_imps kind id =
let c = global_reference kind id in
match c with
| DOPN (Const sp,_) ->
c, list_of_implicits (constant_implicits sp)
| DOPN (MutInd (sp,i),_) ->
c, list_of_implicits (inductive_implicits (sp,i))
| DOPN (MutConstruct ((sp,i),j),_) ->
c, list_of_implicits (constructor_implicits ((sp,i),j))
| _ -> assert false
let global env id = global_reference CCI id
let is_global id =
try
let osp = Nametab.sp_of_id CCI id in
list_prefix_of (dirpath osp) (Lib.cwd())
with Not_found ->
false
let mind_path = function
| DOPN(MutInd (sp,0),_) -> sp
| DOPN(MutInd (sp,tyi),_) ->
let mib = Global.lookup_mind sp in
let mip = mind_nth_type_packet mib tyi in
let (pa,_,k) = repr_path sp in
Names.make_path pa (mip.mind_typename) k
| DOPN(MutConstruct ((sp,tyi),ind),_) ->
let mib = Global.lookup_mind sp in
let mip = mind_nth_type_packet mib tyi in
let (pa,_,k) = repr_path sp in
Names.make_path pa (mip.mind_consnames.(ind-1)) k
| _ -> invalid_arg "mind_path"
(* Eliminations. *)
let declare_eliminations sp =
let env = Global.env () in
let sigma = Evd.empty in
let mindid = basename sp in
let mind = global_reference (kind_of_path sp) mindid in
let redmind = minductype_spec env sigma mind in
let mindstr = string_of_id mindid in
let declare na c =
declare_constant (id_of_string na)
({ const_entry_body = c; const_entry_type = None },
false, NeverDischarge)
in
let mispec = Global.lookup_mind_specif redmind in
let elim_scheme =
strip_all_casts (mis_make_indrec env sigma [] mispec).(0) in
let npars = mis_nparams mispec in
let make_elim s = instanciate_indrec_scheme s npars elim_scheme in
let kelim = mis_kelim mispec in
if List.mem prop kelim then
declare (mindstr^"_ind") (make_elim prop);
if List.mem spec kelim then
declare (mindstr^"_rec") (make_elim spec);
if List.mem types kelim then
declare (mindstr^"_rect") (make_elim (Type (Univ.new_univ sp)))
|