Source file comFixpoint.ml
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
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
module CVars = Vars
open Pp
open Util
open Names
open Context
open EConstr
open Constrexpr
open Constrintern
open Vernacexpr
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
let rec partial_order cmp = function
| [] -> []
| (x,xge)::rest ->
let rec browse res xge' = function
| [] ->
let res = List.map (function
| (z, Inr zge) when List.mem_f cmp x zge ->
(z, Inr (List.union cmp zge xge'))
| r -> r) res in
(x,Inr xge')::res
| y::xge ->
let rec link y =
try match List.assoc_f cmp y res with
| Inl z -> link z
| Inr yge ->
if List.mem_f cmp x yge then
let res = List.remove_assoc_f cmp y res in
let res = List.map (function
| (z, Inl t) ->
if cmp t y then (z, Inl x) else (z, Inl t)
| (z, Inr zge) ->
if List.mem_f cmp y zge then
(z, Inr (List.add_set cmp x (List.remove cmp y zge)))
else
(z, Inr zge)) res in
browse ((y,Inl x)::res) xge' (List.union cmp xge yge)
else
browse res (List.add_set cmp y (List.union cmp xge' yge)) xge
with Not_found -> browse res (List.add_set cmp y xge') xge
in link y
in browse (partial_order cmp rest) [] xge
let string_of_kind = function
| Decls.IsDefinition Fixpoint -> "fixpoint"
| IsDefinition CoFixpoint -> "cofixpoint"
| _ -> "declaration"
let non_full_mutual_message x xge y yge kind rest =
let reason =
if Id.List.mem x yge then
Id.print y ++ str " depends on " ++ Id.print x ++ strbrk " but not conversely"
else if Id.List.mem y xge then
Id.print x ++ str " depends on " ++ Id.print y ++ strbrk " but not conversely"
else
Id.print y ++ str " and " ++ Id.print x ++ strbrk " are not mutually dependent" in
let e = if List.is_empty rest then reason else strbrk "e.g., " ++ reason in
let w =
if kind <> Decls.IsDefinition CoFixpoint
then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl()
else mt () in
strbrk "Not a fully mutually defined " ++ str (string_of_kind kind) ++ fnl () ++
str "(" ++ e ++ str ")." ++ fnl () ++ w
let warn_non_full_mutual =
CWarnings.create ~name:"non-full-mutual" ~category:CWarnings.CoreCategories.fixpoints
(fun (x,xge,y,yge,kind,rest) ->
non_full_mutual_message x xge y yge kind rest)
let warn_non_recursive =
CWarnings.create ~name:"non-recursive" ~category:CWarnings.CoreCategories.fixpoints
(fun (x,kind) ->
strbrk "Not a truly recursive " ++ str (string_of_kind kind) ++ str ".")
let check_true_recursivity env evd ~kind fixl =
let names = List.map fst fixl in
let preorder =
List.map (fun (id,def) ->
(id, List.filter (fun id' -> Termops.occur_var env evd id' def) names))
fixl in
let po = partial_order Id.equal preorder in
match List.filter (function (_,Inr _) -> true | _ -> false) po with
| (x,Inr xge)::(y,Inr yge)::rest ->
warn_non_full_mutual (x,xge,y,yge,kind,rest)
| _ ->
match po with
| [x,Inr []] -> warn_non_recursive (x,kind)
| _ -> ()
open Rocqlib
let init_constant sigma rf = Evd.fresh_global sigma rf
let fix_sub_ref () = lib_ref "program.wf.fix_sub"
let measure_on_R_ref () = lib_ref "program.wf.mr"
let well_founded sigma = init_constant (Global.env ()) sigma (lib_ref "core.wf.well_founded")
let mkSubset sigma name typ prop =
let open EConstr in
let sigma, app_h = Evd.fresh_global (Global.env ()) sigma (delayed_force build_sigma).typ in
sigma, mkApp (app_h, [| typ; mkLambda (make_annot name ERelevance.relevant, typ, prop) |])
let ensure_program () =
try fix_sub_ref (), measure_on_R_ref ()
with NotFoundRef r ->
CErrors.user_err
Pp.(str r ++ spc() ++ str "not registered," ++ spc() ++
str "you should try requiring library Corelib.Program.Wf.")
let recproofid = Id.of_string "recproof"
let argname = Id.of_string "recarg"
let encapsulate_Fix_sub env sigma recname ctx body ccl (, rel, relargty, measure_body) =
let len = Context.Rel.length ctx in
let fix_sub_ref, measure_on_R_ref = ensure_program () in
let open Combinators in
let sigma, letbinders, {telescope_type = tuple_type; telescope_value = tuple_value} =
telescope env sigma ctx in
let tupled_ctx = letbinders @ [LocalAssum (make_annot (Name argname) ERelevance.relevant, tuple_type)] in
let measure = it_mkLambda_or_LetIn measure_body tupled_ctx in
let sigma, comb = Evd.fresh_global (Global.env ()) sigma measure_on_R_ref in
let rel_measure = mkApp (comb, [| tuple_type; relargty; rel; measure |]) in
let sigma, wf_term = well_founded sigma in
let wf_type = mkApp (wf_term, [| tuple_type ; rel_measure |]) in
let tupled_measure_body = it_mkLambda_or_LetIn measure_body letbinders in
let make_applied_rel x y =
mkApp (rel, [| Vars.subst1 x tupled_measure_body; Vars.subst1 y tupled_measure_body |]) in
let tupled_ccl = it_mkLambda_or_LetIn ccl letbinders in
let sigma, fix_sub =
let sigma, fix_sub_term = Evd.fresh_global (Global.env ()) sigma fix_sub_ref in
let sigma, wf_proof = Evarutil.new_evar env sigma
~src:(Loc.tag @@ Evar_kinds.QuestionMark {
Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Evar_kinds.Define false;
}) wf_type in
let sigma = Evd.set_obligation_evar sigma (fst (destEvar sigma wf_proof)) in
let ccl_pred = mkLambda (make_annot (Name argname) ERelevance.relevant, tuple_type, tupled_ccl) in
let def = mkApp (fix_sub_term, [| tuple_type ; rel_measure ; wf_proof ; ccl_pred |]) in
Typing.solve_evars env sigma def in
let arg = RelDecl.LocalAssum (make_annot (Name argname) ERelevance.relevant, tuple_type) in
let argid' = Id.of_string (Id.to_string argname ^ "'") in
let sigma, wfa =
let sigma, ss_term = mkSubset sigma (Name argid') tuple_type (make_applied_rel (mkRel 1) (mkRel 2)) in
sigma, RelDecl.LocalAssum (make_annot (Name argid') ERelevance.relevant, ss_term) in
let sigma, fix_sub_F_sub_ctx =
let sigma, proj = Evd.fresh_global (Global.env ()) sigma (delayed_force build_sigma).Rocqlib.proj1 in
let wfargpred = mkLambda (make_annot (Name argid') ERelevance.relevant, tuple_type, make_applied_rel (mkRel 1) (mkRel 3)) in
let projection =
mkApp (proj, [| tuple_type ; wfargpred ; mkRel 1 |])
in
let ccl_on_smaller_arg = Vars.substl [projection] (it_mkLambda_or_LetIn ccl letbinders) in
let ccl_on_smaller_arg = it_mkProd_or_LetIn ccl_on_smaller_arg [wfa] in
let recname' = Nameops.add_suffix recname "'" in
let smaller_arg = RelDecl.LocalAssum (make_annot (Name recname') ERelevance.relevant,
ccl_on_smaller_arg) in
sigma, Vars.lift_rel_context 1 letbinders @ smaller_arg :: [arg] in
let sigma, curryfier_body, curryfier_ty =
let sigma, intro = Evd.fresh_global (Global.env ()) sigma (delayed_force build_sigma).Rocqlib.intro in
let app =
let wfpred = mkLambda (make_annot (Name argid') ERelevance.relevant, tuple_type, make_applied_rel (mkRel 1) (mkRel (2 * len + 4))) in
let arg = mkApp (intro, [| tuple_type; wfpred; Vars.lift 1 tuple_value; mkRel 1 |]) in
mkApp (mkRel (2 * len + 2 ), [| arg |]) in
let extended_ctx = extradecl :: ctx in
let body = it_mkLambda_or_LetIn app extended_ctx in
let ty = it_mkProd_or_LetIn (Vars.lift 1 ccl) extended_ctx in
sigma, body, ty in
let body_ctx = RelDecl.LocalDef (make_annot (Name recname) ERelevance.relevant, curryfier_body, curryfier_ty) :: fix_sub_F_sub_ctx in
let intern_body_lam = it_mkLambda_or_LetIn body body_ctx in
let sigma, fix_sub = Typing.solve_evars env sigma fix_sub in
sigma, tupled_ctx, tuple_value, mkApp (fix_sub, [|intern_body_lam|])
let build_wellfounded env sigma poly udecl recname ctx body ccl impls rel_measure =
let len = Context.Rel.length ctx in
let _, body = decompose_lambda_n_decls sigma (len + 1) body in
let ccl = Vars.subst1 (mkRel 1) (snd (decompose_prod_n_decls sigma (len + 1) ccl)) in
let sigma, tupled_ctx, tuple_value, def = encapsulate_Fix_sub env sigma recname ctx body ccl rel_measure in
let ctx = Evarutil.nf_rel_context_evar sigma ctx in
let tupled_ctx = Evarutil.nf_rel_context_evar sigma tupled_ctx in
let ccl = Evarutil.nf_evar sigma ccl in
let tuple_value = Evarutil.nf_evar sigma tuple_value in
let recname_func, typ =
if len > 1 then
Nameops.add_suffix recname "_func", it_mkProd_or_LetIn ccl tupled_ctx
else
recname, it_mkProd_or_LetIn ccl ctx in
let body, typ, _uctx, evmap, obls =
Declare.Obls.prepare_obligations ~name:recname_func ~body:def ~types:typ env sigma in
let hook, impls =
if len > 1 then
let hook { Declare.Hook.S.dref; uctx; obls; _ } =
let update c = CVars.replace_vars obls (evmap mkVar (Evarutil.nf_evar (Evd.from_ctx uctx) c)) in
let tuple_value = update tuple_value in
let ccl = update ccl in
let ctx = Context.Rel.map_het (ERelevance.kind sigma) update ctx in
let univs = UState.check_univ_decl ~poly uctx udecl in
let h_body =
let inst = UState.(match fst univs with
| Polymorphic_entry uctx -> UVars.UContext.instance uctx
| Monomorphic_entry _ -> UVars.Instance.empty) in
Constr.mkRef (dref, inst) in
let body = Term.it_mkLambda_or_LetIn (Constr.mkApp (h_body, [|tuple_value|])) ctx in
let ty = Term.it_mkProd_or_LetIn ccl ctx in
let ce = Declare.definition_entry ~types:ty ~univs body in
let c = Declare.declare_constant ~name:recname ~kind:Decls.(IsDefinition Definition) (DefinitionEntry ce) in
let gr = GlobRef.ConstRef c in
if Impargs.is_implicit_args () || not (List.is_empty impls) then
Impargs.declare_manual_implicits false gr impls
in
Some (Declare.Hook.make hook), []
else
None, impls
in
sigma, recname_func, body, typ, impls, obls, hook
let make_qref s = Libnames.qualid_of_string s
let lt_ref = make_qref "Init.Peano.lt"
let position_of_argument ctx binders na =
let exception Found of int in
let name = Name na.CAst.v in
try
Context.Rel.fold_outside (fun decl n ->
match Context.Rel.Declaration.(get_value decl, Name.equal (get_name decl) name) with
| None, true -> raise (Found n)
| Some _, true ->
let loc = List.find_map (fun id -> if Name.equal name id.CAst.v then Some id.CAst.loc else None) (Constrexpr_ops.names_of_local_binders binders) in
let loc = Option.default na.CAst.loc loc in
CErrors.user_err ?loc
(Name.print name ++ str" must be a proper parameter and not a local definition.")
| None, false -> n + 1
| Some _, false -> n )
~init:0 ctx |> ignore;
CErrors.user_err ?loc:na.loc
(str "No parameter named " ++ Id.print na.v ++ str".");
with
Found k -> k
let find_rec_annot ~program_mode ~function_mode env sigma Vernacexpr.{fname={CAst.loc}; binders} ctx typ = function
| None ->
let ctx', _ = Reductionops.whd_decompose_prod_decls (push_rel_context ctx env) sigma typ in
let n = Context.Rel.nhyps ctx + Context.Rel.nhyps ctx' in
if Int.equal n 0 then CErrors.user_err ?loc Pp.(str "A fixpoint needs at least one parameter.");
None, List.interval 0 (n - 1)
| Some CAst.{v=rec_order;loc} ->
let default_order r = Option.default (CAst.make @@ CRef (lt_ref,None)) r in
match rec_order with
| CStructRec na -> None, [position_of_argument ctx binders na]
| CWfRec (na,r) ->
if function_mode then None, []
else Some (r, Constrexpr_ops.mkIdentC na.CAst.v), []
| CMeasureRec (na, mes, rfel) ->
if function_mode then
let _ = match binders, na with
| [CLocalDef({ CAst.v = Name id },_,_,_) | CLocalAssum([{ CAst.v = Name id }],_,_,_)], None -> ()
| _, None -> CErrors.user_err ?loc Pp.(str "Decreasing argument must be specified in measure clause.")
| _, Some na -> ignore (position_of_argument ctx binders na) in
None, []
else
let r = match na, rfel with
| Some id, None ->
let loc = id.CAst.loc in
CAst.make ?loc @@ CRef (Libnames.qualid_of_ident ?loc id.CAst.v,None)
| Some _, Some _ -> CErrors.user_err ?loc Pp.(str"Measure takes three arguments only in Function.")
| None, rfel -> default_order rfel in
Some (r, mes), []
let interp_rec_annot ~program_mode ~function_mode env sigma fixl ctxl ccll rec_order =
let open Pretyping in
let nowf () = List.map (fun _ -> None) fixl in
match rec_order with
| CFixRecOrder fix_orders ->
let fixwf, possible_guard = List.split (List.map4 (find_rec_annot ~program_mode ~function_mode env sigma) fixl ctxl ccll fix_orders) in
fixwf, {possibly_cofix = false; possible_fix_indices = possible_guard}
| CCoFixRecOrder -> nowf (), {possibly_cofix = true; possible_fix_indices = List.map (fun _ -> []) fixl}
| CUnknownRecOrder -> nowf (), RecLemmas.find_mutually_recursive_statements sigma ctxl ccll
let interp_fix_context ~program_mode env sigma {Vernacexpr.binders} =
let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma binders in
sigma, (env', ctx, impl_env, imps)
let interp_fix_ccl ~program_mode sigma impls env fix =
let flags = Pretyping.{ all_no_fail_flags with program_mode } in
let sigma, (c, impl) = interp_type_evars_impls ~flags ~impls env sigma fix.Vernacexpr.rtype in
let r = Retyping.relevance_of_type env sigma c in
sigma, (c, r, impl)
let interp_fix_body ~program_mode env_rec ctx sigma impls fix ccl =
Option.cata (fun body ->
let env_rec_ctx = push_rel_context ctx env_rec in
let sigma, body = interp_casted_constr_evars ~program_mode env_rec_ctx sigma ~impls body ccl in
sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.Vernacexpr.body_def
let build_fix_type sigma ctx ccl (_, ) =
let ccl = it_mkProd_or_LetIn (Vars.lift (Context.Rel.length extradecl) ccl) extradecl in
Evarutil.nf_evar sigma (it_mkProd_or_LetIn ccl ctx)
let build_dummy_fix_type sigma ctx ccl (_, ) =
let ccl = it_mkProd_or_LetIn (Vars.lift (Context.Rel.length extradecl) ccl) (List.map (RelDecl.map_type (fun _ -> mkProp)) extradecl) in
Evarutil.nf_evar sigma (it_mkProd_or_LetIn ccl ctx)
let encapsulate env sigma r t =
let fix_proto sigma =
Evd.fresh_global (Global.env ()) sigma (Rocqlib.lib_ref "program.tactic.fix_proto") in
let fix_proto_relevance = EConstr.ERelevance.relevant in
let sigma, sort = Typing.type_of ~refresh:true env sigma t in
try
let sigma, h_term = fix_proto sigma in
let app = EConstr.mkApp (h_term, [|sort; t|]) in
let sigma, app = Typing.solve_evars env sigma app in
sigma, fix_proto_relevance, app
with e when CErrors.noncritical e -> sigma, r, t
type ('constr, 'relevance) fix_data = {
fixnames : Names.Id.t list;
fixrs : 'relevance list;
fixdefs : 'constr option list;
fixtypes : 'constr list;
fixctxs : EConstr.rel_context list;
fiximps : (Names.Name.t * bool) option CAst.t list list;
fixntns : Metasyntax.notation_interpretation_decl list;
fixwfs : (rel_declaration * EConstr.t * EConstr.t * EConstr.t) option list;
}
let interp_wf ~program_mode env sigma recname ctx ccl = function
| None -> sigma, ((false, []), None, [])
| Some (r, measure) ->
let impl = CAst.make (Some (Name recproofid, true)) in
let env_ctx = push_rel_context ctx env in
let sigma, (rel, _) = interp_constr_evars_impls ~program_mode env sigma r in
let relargty = Hipattern.is_homogeneous_relation ?loc:(Constrexpr_ops.constr_loc r) env_ctx sigma rel in
let sigma, measure = interp_casted_constr_evars ~program_mode env_ctx sigma measure relargty in
let sigma, after, =
if program_mode then
let len = Context.Rel.length ctx in
let applied_rel_measure = mkApp (rel, [| measure; Vars.lift len measure |]) in
let = RelDecl.LocalAssum (make_annot (Name recproofid) ERelevance.relevant, applied_rel_measure) in
sigma, true, extradecl
else
let sigma, wf_term = well_founded sigma in
let applied_wf = mkApp (wf_term, [| relargty; rel; measure |]) in
let = RelDecl.LocalAssum (make_annot (Name recproofid) ERelevance.relevant, applied_wf) in
sigma, false, extradecl
in
sigma, ((after, [extradecl]), Some (extradecl, rel, relargty, measure), [impl])
let interp_mutual_definition env ~program_mode ~function_mode rec_order fixl =
let open Context.Named.Declaration in
let open EConstr in
let fixnames = List.map (fun fix -> fix.Vernacexpr.fname.CAst.v) fixl in
let sigma, decl = interp_mutual_univ_decl_opt env (List.map (fun Vernacexpr.{univs} -> univs) fixl) in
let sigma, (fixenv, fixctxs, fixctximpenvs, fixctximps) =
on_snd List.split4 @@
List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma) sigma fixl in
let sigma, (fixccls,fixrs,fixcclimps) =
on_snd List.split3 @@
List.fold_left3_map (interp_fix_ccl ~program_mode) sigma fixctximpenvs fixenv fixl in
let fixwfs, possible_guard = interp_rec_annot ~program_mode ~function_mode env sigma fixl fixctxs fixccls rec_order in
let sigma, (, fixwfs, fixwfimps) =
on_snd List.split3 @@ (List.fold_left4_map (interp_wf ~program_mode env) sigma fixnames fixctxs fixccls fixwfs) in
let fixtypes = List.map3 (build_fix_type sigma) fixctxs fixccls fixextras in
let sigma, rec_sign =
List.fold_left4
(fun (sigma, rec_sign) id r t (_,) ->
let sigma, r, t = if program_mode && List.is_empty extradecl then encapsulate env sigma r t else sigma, r, t in
sigma, LocalAssum (Context.make_annot id r, t) :: rec_sign)
(sigma, []) fixnames fixrs fixtypes fixextras
in
let fixrecimps = List.map3 (fun ctximps wfimps cclimps -> ctximps @ wfimps @ cclimps) fixctximps fixwfimps fixcclimps in
let fiximps = List.map2 (fun ctximps cclimps -> ctximps @ cclimps) fixctximps fixcclimps in
let fixntns = List.map_append (fun { Vernacexpr.notations } -> List.map Metasyntax.prepare_where_notation notations ) fixl in
let sigma, fixdefs =
let force = List.map (fun (_,) -> Id.Set.of_list (List.map_filter (fun d -> Nameops.Name.to_option (RelDecl.get_name d)) extra)) fixextras in
let dummy_fixtypes = List.map3 (build_dummy_fix_type sigma) fixctxs fixccls fixextras in
let impls = compute_internalization_env env sigma ~force Recursive fixnames dummy_fixtypes fixrecimps in
Metasyntax.with_syntax_protection (fun () ->
List.iter (Metasyntax.set_notation_for_interpretation env impls) fixntns;
List.fold_left5_map
(fun sigma fixctximpenv (after,) ctx body ccl ->
let impls = Id.Map.fold Id.Map.add fixctximpenv impls in
let env', ctx =
if after then env, List.map NamedDecl.to_rel_decl rec_sign @ ctx
else push_named_context rec_sign env, extradecl@ctx in
interp_fix_body ~program_mode env' ctx sigma impls body (Vars.lift (Context.Rel.length extradecl) ccl))
sigma fixctximpenvs fixextras fixctxs fixl fixccls)
() in
let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
let sigma = Evd.minimize_universes sigma in
let fix = {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs} in
(env, rec_sign, sigma), (fix, possible_guard, decl)
let check_recursive ~kind env evd {fixnames;fixdefs;fixwfs} =
if List.for_all Option.has_some fixdefs && List.for_all Option.is_empty fixwfs then begin
let fixdefs = List.map Option.get fixdefs in
check_true_recursivity env evd ~kind (List.combine fixnames fixdefs)
end
let ground_fixpoint env evd {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs} =
Pretyping.check_evars_are_solved ~program_mode:false env evd;
let fixrs = List.map (fun r -> EConstr.ERelevance.kind evd r) fixrs in
let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in
let fixtypes = List.map EConstr.(to_constr evd) fixtypes in
{fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs}
(** For Funind *)
let interp_fixpoint_short rec_order fixpoint_exprl =
let env = Global.env () in
let (_, _, sigma),(fix, _, _) = interp_mutual_definition ~program_mode:false ~function_mode:true env (CFixRecOrder rec_order) fixpoint_exprl in
let sigma = Pretyping.(solve_remaining_evars all_no_fail_flags env sigma) in
let typel = (ground_fixpoint env sigma fix).fixtypes in
typel, sigma
let build_recthms {fixnames;fixtypes;fixctxs;fiximps} =
List.map4 (fun name typ ctx impargs ->
let args = List.map Context.Rel.Declaration.get_name ctx in
Declare.CInfo.make ~name ~typ ~args ~impargs ()
) fixnames fixtypes fixctxs fiximps
let collect_evars_of_term evd c ty =
Evar.Set.union (Evd.evars_of_term evd c) (Evd.evars_of_term evd ty)
let collect_evars env sigma rec_sign recname def typ =
let deps = collect_evars_of_term sigma def typ in
let evars, _, def, typ =
RetrieveObl.retrieve_obligations env recname sigma
(List.length rec_sign) ~deps def typ in
(Some def, typ, evars)
let out_def = function
| Some def -> def
| None -> CErrors.user_err Pp.(str "Program Fixpoint needs defined bodies.")
let build_program_fixpoint env sigma rec_sign possible_guard fixnames fixrs fixdefs fixtypes fixwfs =
assert (List.for_all Option.is_empty fixwfs);
let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env sigma in
let sigma = Evarutil.nf_evar_map_undefined sigma in
let fixdefs = List.map out_def fixdefs in
let () =
let fixdecls =
Array.of_list (List.map2 (fun x r -> Context.make_annot (Name x) r) fixnames fixrs),
Array.of_list fixtypes,
Array.of_list fixdefs
in
ignore (Pretyping.esearch_guard env sigma possible_guard fixdecls) in
List.split3 (List.map3 (collect_evars env sigma rec_sign) fixnames fixdefs fixtypes)
let finish_obligations env sigma rec_sign possible_guard poly udecl = function
| {fixnames=[recname];fixrs;fixdefs=[body];fixtypes=[ccl];fixctxs=[ctx];fiximps=[imps];fixntns;fixwfs=[Some wf]} ->
let sigma = Evarutil.nf_evar_map sigma in
let sigma, recname, body, ccl, impls, obls, hook = build_wellfounded env sigma poly udecl recname ctx (Option.get body) ccl imps wf in
let fixrs = List.map (EConstr.ERelevance.kind sigma) fixrs in
sigma, {fixnames=[recname];fixrs;fixdefs=[Some body];fixtypes=[ccl];fixctxs=[ctx];fiximps=[impls];fixntns;fixwfs=[Some wf]}, [obls], hook
| {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs} ->
let fixdefs, fixtypes, obls = build_program_fixpoint env sigma rec_sign possible_guard fixnames fixrs fixdefs fixtypes fixwfs in
let fixrs = List.map (EConstr.ERelevance.kind sigma) fixrs in
sigma, {fixnames;fixrs;fixdefs;fixtypes;fixctxs;fiximps;fixntns;fixwfs}, obls, None
let finish_regular env sigma use_inference_hook fix =
let inference_hook = if use_inference_hook then Some Declare.Obls.program_inference_hook else None in
let sigma = Pretyping.(solve_remaining_evars ?hook:inference_hook all_no_fail_flags env sigma) in
sigma, ground_fixpoint env sigma fix, [], None
let do_mutually_recursive ?pm ~program_mode ?(use_inference_hook=false) ?scope ?clearbody ~kind ~poly ?typing_flags ?user_warns ?using (rec_order, fixl)
: Declare.OblState.t option * Declare.Proof.t option =
let env = Global.env () in
let env = Environ.update_typing_flags ?typing_flags env in
let (env,rec_sign,sigma),(fix,possible_guard,udecl) = interp_mutual_definition env ~program_mode ~function_mode:false rec_order fixl in
check_recursive ~kind env sigma fix;
let sigma, ({fixdefs=bodies;fixrs;fixtypes;fixwfs} as fix), obls, hook =
match pm with
| Some pm -> finish_obligations env sigma rec_sign possible_guard poly udecl fix
| None -> finish_regular env sigma use_inference_hook fix in
let info = Declare.Info.make ?scope ?clearbody ~kind ~poly ~udecl ?hook ?typing_flags ?user_warns ~ntns:fix.fixntns () in
let cinfo = build_recthms fix in
match pm with
| Some pm ->
let bodies = List.map Option.get bodies in
Evd.check_univ_decl_early ~poly ~with_obls:true sigma udecl (bodies @ fixtypes);
let sigma = if poly then sigma else Evd.fix_undefined_variables sigma in
let uctx = Evd.ustate sigma in
(match fixwfs, bodies, cinfo, obls with
| [Some _], [body], [cinfo], [obls] ->
let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~opaque:false ~body ~uctx ?using obls in
Some pm, None
| _ ->
let possible_guard = (possible_guard, fixrs) in
Some (Declare.Obls.add_mutual_definitions ~pm ~cinfo ~info ~opaque:false ~uctx ~bodies ~possible_guard ?using obls), None)
| None ->
try
let bodies = List.map Option.get bodies in
let uctx = Evd.ustate sigma in
let possible_guard = (possible_guard, fixrs) in
let _ : GlobRef.t list =
Declare.declare_mutual_definitions ~cinfo ~info ~opaque:false ~uctx ~possible_guard ~bodies ?using ()
in
None, None
with Option.IsNone ->
Evd.check_univ_decl_early ~poly ~with_obls:false sigma udecl (Option.List.flatten bodies @ fixtypes);
let possible_guard = (possible_guard, fixrs) in
let lemma = Declare.Proof.start_mutual_definitions ~info ~cinfo ~bodies ~possible_guard ?using sigma in
None, Some lemma