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
|
open Util
open Names
open Term
open Pp
open Indfun_common
open Libnames
open Rawterm
open Declarations
type annot =
Struct of identifier
| Wf of Topconstr.constr_expr * identifier option
| Mes of Topconstr.constr_expr * identifier option
type newfixpoint_expr =
identifier * annot * Topconstr.local_binder list * Topconstr.constr_expr * Topconstr.constr_expr
let rec abstract_rawconstr c = function
| [] -> c
| Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_rawconstr c bl)
| Topconstr.LocalRawAssum (idl,t)::bl ->
List.fold_right (fun x b -> Topconstr.mkLambdaC([x],t,b)) idl
(abstract_rawconstr c bl)
let interp_casted_constr_with_implicits sigma env impls c =
(* Constrintern.interp_rawconstr_with_implicits sigma env [] impls c *)
Constrintern.intern_gen false sigma env ~impls:([],impls)
~allow_soapp:false ~ltacvars:([],[]) c
(*
Construct a fixpoint as a Rawterm
and not as a constr
*)
let build_newrecursive
(lnameargsardef) =
let env0 = Global.env()
and sigma = Evd.empty
in
let (rec_sign,rec_impls) =
List.fold_left
(fun (env,impls) (recname,_,bl,arityc,_) ->
let arityc = Command.generalize_constr_expr arityc bl in
let arity = Constrintern.interp_type sigma env0 arityc in
let impl =
if Impargs.is_implicit_args()
then Impargs.compute_implicits env0 arity
else [] in
let impls' =(recname,([],impl,Notation.compute_arguments_scope arity))::impls in
(Environ.push_named (recname,None,arity) env, impls'))
(env0,[]) lnameargsardef in
let recdef =
(* Declare local notations *)
let fs = States.freeze() in
let def =
try
List.map
(fun (_,_,bl,_,def) ->
let def = abstract_rawconstr def bl in
interp_casted_constr_with_implicits
sigma rec_sign rec_impls def
)
lnameargsardef
with e ->
States.unfreeze fs; raise e in
States.unfreeze fs; def
in
recdef
let compute_annot (name,annot,args,types,body) =
let names = List.map snd (Topconstr.names_of_local_assums args) in
match annot with
| None ->
if List.length names > 1 then
user_err_loc
(dummy_loc,"Function",
Pp.str "the recursive argument needs to be specified");
let new_annot = (id_of_name (List.hd names)) in
(name,Struct new_annot,args,types,body)
| Some r -> (name,r,args,types,body)
(* Checks whether or not the mutual bloc is recursive *)
let rec is_rec names =
let names = List.fold_right Idset.add names Idset.empty in
let check_id id names = Idset.mem id names in
let rec lookup names = function
| RVar(_,id) -> check_id id names
| RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false
| RCast(_,b,_,_) -> lookup names b
| RRec _ -> error "RRec not handled"
| RIf(_,b,_,lhs,rhs) ->
(lookup names b) || (lookup names lhs) || (lookup names rhs)
| RLetIn(_,na,t,b) | RLambda(_,na,t,b) | RProd(_,na,t,b) ->
lookup names t || lookup (Nameops.name_fold Idset.remove na names) b
| RLetTuple(_,nal,_,t,b) -> lookup names t ||
lookup
(List.fold_left
(fun acc na -> Nameops.name_fold Idset.remove na acc)
names
nal
)
b
| RApp(_,f,args) -> List.exists (lookup names) (f::args)
| RCases(_,_,el,brl) ->
List.exists (fun (e,_) -> lookup names e) el ||
List.exists (lookup_br names) brl
and lookup_br names (_,idl,_,rt) =
let new_names = List.fold_right Idset.remove idl names in
lookup new_names rt
in
lookup names
let prepare_body (name,annot,args,types,body) rt =
let n = (Topconstr.local_binders_length args) in
(* Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_rawconstr rt); *)
let fun_args,rt' = chop_rlambda_n n rt in
(fun_args,rt')
let generate_principle
do_built fix_rec_l recdefs interactive_proof parametrize
(continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) =
let names = List.map (function (name,_,_,_,_) -> name) fix_rec_l in
let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
let funs_args = List.map fst fun_bodies in
let funs_types = List.map (function (_,_,_,types,_) -> types) fix_rec_l in
try
(* We then register the Inductive graphs of the functions *)
Rawterm_to_relation.build_inductive parametrize names funs_args funs_types recdefs;
if do_built
then
begin
let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in
let ind_kn =
fst (locate_with_msg
(pr_reference f_R_mut++str ": Not an inductive type!")
locate_ind
f_R_mut)
in
let fname_kn (fname,_,_,_,_) =
let f_ref = Ident (dummy_loc,fname) in
locate_with_msg
(pr_reference f_ref++str ": Not an inductive type!")
locate_constant
f_ref
in
let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in
let _ =
Util.list_map_i
(fun i x ->
let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in
let princ_type =
(Global.lookup_constant princ).Declarations.const_type
in
Functional_principles_types.generate_functional_principle
interactive_proof
princ_type
None
None
funs_kn
i
(continue_proof 0 [|funs_kn.(i)|])
)
0
fix_rec_l
in
()
end
with e ->
Pp.msg_warning (Cerrors.explain_exn e)
let register_struct is_rec fixpoint_exprl =
match fixpoint_exprl with
| [(fname,_,bl,ret_type,body),_] when not is_rec ->
Command.declare_definition
fname
(Decl_kinds.Global,Options.boxed_definitions (),Decl_kinds.Definition)
bl
None
body
(Some ret_type)
(fun _ _ -> ())
| _ ->
Command.build_recursive fixpoint_exprl (Options.boxed_definitions())
let generate_correction_proof_wf f_ref tcc_lemma_ref
is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
(_: int) (_:Names.constant array) (_:Term.constr array) (_:int) : Tacmach.tactic =
Functional_principles_proofs.prove_principle_for_gen
(f_ref,functional_ref,eq_ref)
tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation
let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
pre_hook
=
let type_of_f = Command.generalize_constr_expr ret_type args in
let rec_arg_num =
let names =
List.map
snd
(Topconstr.names_of_local_assums args)
in
match wf_arg with
| None ->
if List.length names = 1 then 1
else error "Recursive argument must be specified"
| Some wf_arg ->
Util.list_index (Name wf_arg) names
in
let unbounded_eq =
let f_app_args =
Topconstr.CApp
(dummy_loc,
(None,Topconstr.mkIdentC fname) ,
(List.map
(function
| _,Anonymous -> assert false
| _,Name e -> (Topconstr.mkIdentC e,None)
)
(Topconstr.names_of_local_assums args)
)
)
in
Topconstr.CApp (dummy_loc,(None,Topconstr.mkIdentC (id_of_string "eq")),
[(f_app_args,None);(body,None)])
in
let eq = Command.generalize_constr_expr unbounded_eq args in
let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation =
try
pre_hook
(generate_correction_proof_wf f_ref tcc_lemma_ref is_mes
functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
);
Command.save_named true
with e ->
(* No proof done *)
()
in
Recdef.recursive_definition
is_mes fname
type_of_f
wf_rel_expr
rec_arg_num
eq
hook
let register_mes fname wf_mes_expr wf_arg args ret_type body =
let wf_arg_type,wf_arg =
match wf_arg with
| None ->
begin
match args with
| [Topconstr.LocalRawAssum ([(_,Name x)],t)] -> t,x
| _ -> error "Recursive argument must be specified"
end
| Some wf_args ->
try
match
List.find
(function
| Topconstr.LocalRawAssum(l,t) ->
List.exists
(function (_,Name id) -> id = wf_args | _ -> false)
l
| _ -> false
)
args
with
| Topconstr.LocalRawAssum(_,t) -> t,wf_args
| _ -> assert false
with Not_found -> assert false
in
let ltof =
let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in
Libnames.Qualid (dummy_loc,Libnames.qualid_of_sp
(Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof")))
in
let fun_from_mes =
let applied_mes =
Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg]) in
Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],wf_arg_type,applied_mes)
in
let wf_rel_from_mes =
Topconstr.mkAppC(Topconstr.mkRefC ltof,[wf_arg_type;fun_from_mes])
in
register_wf ~is_mes:true fname wf_rel_from_mes (Some wf_arg) args ret_type body
let do_generate_principle register_built interactive_proof fixpoint_exprl =
let recdefs = build_newrecursive fixpoint_exprl in
let _is_struct =
match fixpoint_exprl with
| [((name,Some (Wf (wf_rel,wf_x)),args,types,body))] ->
let pre_hook =
generate_principle
register_built
fixpoint_exprl
recdefs
true
false
in
if register_built then register_wf name wf_rel wf_x args types body pre_hook;
false
| [((name,Some (Mes (wf_mes,wf_x)),args,types,body))] ->
let pre_hook =
generate_principle
register_built
fixpoint_exprl
recdefs
true
false
in
if register_built then register_mes name wf_mes wf_x args types body pre_hook;
false
| _ ->
let fix_names =
List.map (function (name,_,_,_,_) -> name) fixpoint_exprl
in
let is_one_rec = is_rec fix_names in
let old_fixpoint_exprl =
List.map
(function
| (name,Some (Struct id),args,types,body),_ ->
let names =
List.map
snd
(Topconstr.names_of_local_assums args)
in
let annot =
try Some (Util.list_index (Name id) names - 1), Topconstr.CStructRec
with Not_found -> raise (UserError("",str "Cannot find argument " ++ Ppconstr.pr_id id))
in
(name,annot,args,types,body),(None:Vernacexpr.decl_notation)
| (name,None,args,types,body),recdef ->
let names = (Topconstr.names_of_local_assums args) in
if is_one_rec recdef && List.length names > 1 then
Util.user_err_loc
(Util.dummy_loc,"Function",
Pp.str "the recursive argument needs to be specified in Function")
else
(name,(Some 0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation)
| (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_->
error
("Cannot use mutual definition with well-founded recursion")
)
(List.combine fixpoint_exprl recdefs)
in
(* ok all the expressions are structural *)
let fix_names =
List.map (function (name,_,_,_,_) -> name) fixpoint_exprl
in
let is_rec = List.exists (is_rec fix_names) recdefs in
if register_built then register_struct is_rec old_fixpoint_exprl;
generate_principle
register_built
fixpoint_exprl
recdefs
interactive_proof
true
(Functional_principles_proofs.prove_princ_for_struct interactive_proof);
true
in
()
open Topconstr
let rec add_args id new_args b =
match b with
| CRef r ->
begin match r with
| Libnames.Ident(loc,fname) when fname = id ->
CAppExpl(dummy_loc,(None,r),new_args)
| _ -> b
end
| CFix _ | CCoFix _ -> anomaly "add_args : todo"
| CArrow(loc,b1,b2) ->
CArrow(loc,add_args id new_args b1, add_args id new_args b2)
| CProdN(loc,nal,b1) ->
CProdN(loc,List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal, add_args id new_args b1)
| CLambdaN(loc,nal,b1) ->
CLambdaN(loc,List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal, add_args id new_args b1)
| CLetIn(loc,na,b1,b2) ->
CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2)
| CAppExpl(loc,(pf,r),exprl) ->
begin
match r with
| Libnames.Ident(loc,fname) when fname = id ->
CAppExpl(loc,(pf,r),new_args@(List.map (add_args id new_args) exprl))
| _ -> CAppExpl(loc,(pf,r),List.map (add_args id new_args) exprl)
end
| CApp(loc,(pf,b),bl) ->
CApp(loc,(pf,add_args id new_args b), List.map (fun (e,o) -> add_args id new_args e,o) bl)
| CCases(loc,b_option,cel,cal) ->
CCases(loc,Util.option_map (add_args id new_args) b_option,
List.map (fun (b,(na,b_option)) -> add_args id new_args b,(na,Util.option_map (add_args id new_args) b_option)) cel,
List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
)
| CLetTuple(loc,nal,(na,b_option),b1,b2) ->
CLetTuple(loc,nal,(na,Util.option_map (add_args id new_args) b_option),
add_args id new_args b1,
add_args id new_args b2
)
| CIf(loc,b1,(na,b_option),b2,b3) ->
CIf(loc,add_args id new_args b1,
(na,Util.option_map (add_args id new_args) b_option),
add_args id new_args b2,
add_args id new_args b3
)
| CHole _ -> b
| CPatVar _ -> b
| CEvar _ -> b
| CSort _ -> b
| CCast(loc,b1,ck,b2) ->
CCast(loc,add_args id new_args b1,ck,add_args id new_args b2)
| CNotation _ -> anomaly "add_args : CNotation"
| CPrim _ -> b
| CDelimiters _ -> anomaly "add_args : CDelimiters"
| CDynamic _ -> anomaly "add_args : CDynamic"
let make_graph (id:identifier) =
let c_body =
try
let c = const_of_id id in
Global.lookup_constant c
with Not_found ->
raise (UserError ("",str "Cannot find " ++ Ppconstr.pr_id id) )
in
match c_body.const_body with
| None -> error "Cannot build a graph over an axiom !"
| Some b ->
let env = Global.env () in
let body = (force b) in
let extern_body,extern_type =
let old_implicit_args = Impargs.is_implicit_args ()
and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
let old_rawprint = !Options.raw_print in
Options.raw_print := true;
Impargs.make_implicit_args false;
Impargs.make_strict_implicit_args false;
Impargs.make_contextual_implicit_args false;
try
let res = Constrextern.extern_constr false env body in
let res' = Constrextern.extern_type false env c_body.const_type in
Impargs.make_implicit_args old_implicit_args;
Impargs.make_strict_implicit_args old_strict_implicit_args;
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
Options.raw_print := old_rawprint;
res,res'
with
| UserError(s,msg) as e ->
Impargs.make_implicit_args old_implicit_args;
Impargs.make_strict_implicit_args old_strict_implicit_args;
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
Options.raw_print := old_rawprint;
raise e
| e ->
Impargs.make_implicit_args old_implicit_args;
Impargs.make_strict_implicit_args old_strict_implicit_args;
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
Options.raw_print := old_rawprint;
raise e
in
let rec get_args b t : Topconstr.local_binder list *
Topconstr.constr_expr * Topconstr.constr_expr =
(* Pp.msgnl (str "body: " ++Ppconstr.pr_lconstr_expr b); *)
(* Pp.msgnl (str "type: " ++ Ppconstr.pr_lconstr_expr t); *)
(* Pp.msgnl (fnl ()); *)
match b with
| Topconstr.CLambdaN (loc, (nal_ta), b') ->
begin
let n =
(List.fold_left (fun n (nal,_) ->
n+List.length nal) 0 nal_ta )
in
let rec chop_n_arrow n t =
if n > 0
then
match t with
| Topconstr.CArrow(_,_,t) -> chop_n_arrow (n-1) t
| Topconstr.CProdN(_,nal_ta',t') ->
let n' =
List.fold_left
(fun n (nal,t'') ->
n+List.length nal) n nal_ta'
in
assert (n'<= n);
chop_n_arrow (n - n') t'
| _ -> anomaly "Not enough products"
else t
in
let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in
(List.map (fun (nal,ta) -> (Topconstr.LocalRawAssum (nal,ta))) nal_ta)@nal_tas, b'',t''
end
| _ -> [],b,t
in
let (nal_tas,b,t) = get_args extern_body extern_type in
let expr_list =
match b with
| Topconstr.CFix(loc,l_id,fixexprl) ->
let l =
List.map
(fun (id,(n,recexp),bl,t,b) ->
(* let nal = *)
(* List.flatten *)
(* (List.map *)
(* (function *)
(* | Topconstr.LocalRawDef (na,_)-> [] *)
(* | Topconstr.LocalRawAssum (nal,_) -> nal *)
(* ) *)
(* (nal_tas@bl) *)
(* ) *)
(* in *)
let bl' =
List.flatten
(List.map
(function
| Topconstr.LocalRawDef (na,_)-> []
| Topconstr.LocalRawAssum (nal,_) -> nal
)
bl
)
in
let rec_id =
match List.nth bl' (out_some n) with |(_,Name id) -> id | _ -> anomaly ""
in
let new_args =
List.flatten
(List.map
(function
| Topconstr.LocalRawDef (na,_)-> []
| Topconstr.LocalRawAssum (nal,_) -> List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n))) nal
)
nal_tas
)
in
let b' = add_args id new_args b in
(id, Some (Struct rec_id),nal_tas@bl,t,b')
)
fixexprl
in
l
| _ ->
[(id,None,nal_tas,t,b)]
in
(* List.iter (fun (id,rec_arg,bl,t,b) -> *)
(* Pp.msgnl *)
(* (Ppconstr.pr_id id ++ *)
(* Ppconstr.pr_binders bl ++ *)
(* begin match rec_arg with *)
(* | Some (Struct id) -> str " { struct " ++ Ppconstr.pr_id id ++ str " }" *)
(* | _ -> (mt ()) *)
(* end ++ *)
(* str " : " ++ Ppconstr.pr_lconstr_expr t ++ *)
(* str " := " ++ *)
(* Ppconstr.pr_lconstr_expr b *)
(* ) *)
(* ) *)
(* expr_list; *)
do_generate_principle false false expr_list
(* let make_graph _ = assert false *)
let do_generate_principle = do_generate_principle true
|