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
open Util
open Names
open Constr
open Term
open Declarations
open UVars
open Cooking
module NamedDecl = Context.Named.Declaration
module RelDecl = Context.Rel.Declaration
let lift_univs info univ_hyps = function
| Monomorphic ->
assert (UVars.Instance.is_empty univ_hyps);
info, univ_hyps, Monomorphic
| Polymorphic auctx ->
let info, (qn, un), auctx = lift_poly_univs info auctx in
let univ_hyps =
let open UVars.Instance in
let qs, us = to_array univ_hyps in
let qs = Array.sub qs 0 (Array.length qs - qn) in
let us = Array.sub us 0 (Array.length us - un) in
of_array (qs,us)
in
info, univ_hyps, Polymorphic auctx
let lift_private_univs info = function
| Opaqueproof.PrivateMonomorphic () as priv ->
let () = lift_private_mono_univs info () in
priv
| Opaqueproof.PrivatePolymorphic ctx ->
let ctx = lift_private_poly_univs info ctx in
Opaqueproof.PrivatePolymorphic ctx
let cook_opaque_proofterm info c =
let fold info (c, priv) =
let priv = lift_private_univs info priv in
let c = abstract_as_body (create_cache info) c in
(c, priv)
in
List.fold_right fold info c
let cook_constant _env info cb =
let info, univ_hyps, univs = lift_univs info cb.const_univ_hyps cb.const_universes in
let cache = create_cache info in
let map c = abstract_as_body cache c in
let body = match cb.const_body with
| Undef _ as x -> x
| Def cs -> Def (map cs)
| OpaqueDef o ->
OpaqueDef (Opaqueproof.discharge_opaque info o)
| Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
| Symbol _ -> CErrors.anomaly (Pp.str "Symbols cannot be cooked")
in
let typ = abstract_as_type cache cb.const_type in
let names = names_info info in
let hyps = List.filter (fun d -> not (Id.Set.mem (NamedDecl.get_id d) names)) cb.const_hyps in
{
const_hyps = hyps;
const_univ_hyps = univ_hyps;
const_body = body;
const_type = typ;
const_body_code = ();
const_universes = univs;
const_relevance = cb.const_relevance;
const_inline_code = cb.const_inline_code;
const_typing_flags = cb.const_typing_flags;
}
let cook_rel_context cache ctx =
let t = it_mkProd_or_LetIn mkProp ctx in
let t = abstract_as_type cache t in
let ctx, t = decompose_prod_decls t in
assert (Constr.equal t mkProp);
ctx
let cook_lc cache ~ntypes t =
let diff = Context.Rel.length (rel_context_of_cooking_cache cache) in
let subs = List.init ntypes (fun k -> mkApp (mkRel (k+diff+1), instance_of_cooking_cache cache)) in
let t = Vars.substl subs t in
abstract_as_type cache t
let cook_projection cache ~params t =
let t = mkArrowR mkProp t in
let t = it_mkProd_or_LetIn t params in
let t = abstract_as_type cache t in
let nrels = Context.Rel.nhyps (rel_context_of_cooking_cache cache) in
let _, t = decompose_prod_n_decls (Context.Rel.length params + 1 + nrels) t in
t
let cook_one_ind cache ~ntypes mip =
let mind_arity = match mip.mind_arity with
| RegularArity {mind_user_arity=arity;mind_sort=sort} ->
let arity = abstract_as_type cache arity in
let sort = abstract_as_sort cache sort in
RegularArity {mind_user_arity=arity; mind_sort=sort}
| TemplateArity {template_level} ->
TemplateArity {template_level}
in
let mind_arity_ctxt = cook_rel_context cache mip.mind_arity_ctxt in
let mind_user_lc = Array.map (cook_lc cache ~ntypes) mip.mind_user_lc in
let mind_nf_lc = Array.map (fun (ctx,t) ->
let lc = it_mkProd_or_LetIn t ctx in
let lc = cook_lc cache ~ntypes lc in
decompose_prod_decls lc)
mip.mind_nf_lc
in
{ mind_typename = mip.mind_typename;
mind_arity_ctxt;
mind_arity;
mind_consnames = mip.mind_consnames;
mind_user_lc;
mind_nrealargs = mip.mind_nrealargs;
mind_nrealdecls = mip.mind_nrealdecls;
mind_squashed = mip.mind_squashed;
mind_nf_lc;
mind_consnrealargs = mip.mind_consnrealargs;
mind_consnrealdecls = mip.mind_consnrealdecls;
mind_recargs = mip.mind_recargs;
mind_relevance = mip.mind_relevance;
mind_nb_constant = mip.mind_nb_constant;
mind_nb_args = mip.mind_nb_args;
mind_reloc_tbl = mip.mind_reloc_tbl;
}
let cook_inductive info mib =
let info, univ_hyps, mind_universes = lift_univs info mib.mind_univ_hyps mib.mind_universes in
let cache = create_cache info in
let nnewparams = Context.Rel.nhyps (rel_context_of_cooking_cache cache) in
let mind_params_ctxt = cook_rel_context cache mib.mind_params_ctxt in
let ntypes = mib.mind_ntypes in
let mind_packets = Array.map (cook_one_ind cache ~ntypes) mib.mind_packets in
let mind_record = match mib.mind_record with
| NotRecord -> NotRecord
| FakeRecord -> FakeRecord
| PrimRecord data ->
let data = Array.map (fun (id,projs,relevances,tys) ->
let tys = Array.map (cook_projection cache ~params:mib.mind_params_ctxt) tys in
(id,projs,relevances,tys))
data
in
PrimRecord data
in
let names = names_info info in
let mind_hyps =
List.filter (fun d -> not (Id.Set.mem (NamedDecl.get_id d) names))
mib.mind_hyps
in
let mind_variance, mind_sec_variance =
match mib.mind_variance, mib.mind_sec_variance with
| None, None -> None, None
| None, Some _ | Some _, None -> assert false
| Some variance, Some sec_variance ->
let ulen = snd (AbstractContext.size (universe_context_of_cooking_info info)) in
let sec_variance, newvariance =
Array.chop (Array.length sec_variance - ulen) sec_variance
in
Some (Array.append newvariance variance), Some sec_variance
in
let mind_template = match mib.mind_template with
| None -> None
| Some {template_param_levels=levels; template_context} ->
let sec_levels = CList.map_filter (fun d ->
if RelDecl.is_local_assum d then Some None
else None)
(rel_context_of_cooking_cache cache)
in
let levels = List.rev_append sec_levels levels in
Some {template_param_levels=levels; template_context}
in
{
mind_packets;
mind_record;
mind_finite = mib.mind_finite;
mind_ntypes = mib.mind_ntypes;
mind_hyps;
mind_univ_hyps = univ_hyps;
mind_nparams = mib.mind_nparams + nnewparams;
mind_nparams_rec = mib.mind_nparams_rec + nnewparams;
mind_params_ctxt;
mind_universes;
mind_template;
mind_variance;
mind_sec_variance;
mind_private = mib.mind_private;
mind_typing_flags = mib.mind_typing_flags;
}
let cook_rel_context info ctx =
cook_rel_context (create_cache info) ctx