1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
8
(*i camlp4deps: "parsing/grammar.cma" i*)
20
let pr_binding prc = function
21
| loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
22
| loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
24
let pr_bindings prc prlc = function
25
| Rawterm.ImplicitBindings l ->
26
brk (1,1) ++ str "with" ++ brk (1,1) ++
27
Util.prlist_with_sep spc prc l
28
| Rawterm.ExplicitBindings l ->
29
brk (1,1) ++ str "with" ++ brk (1,1) ++
30
Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
31
| Rawterm.NoBindings -> mt ()
33
let pr_with_bindings prc prlc (c,bl) =
34
prc c ++ hv 0 (pr_bindings prc prlc bl)
36
let pr_fun_ind_using prc prlc _ opt_c =
39
| Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc (p,b))
41
(* Duplication of printing functions because "'a with_bindings" is
42
(internally) not uniform in 'a: indeed constr_with_bindings at the
43
"typed" level has type "open_constr with_bindings" instead of
44
"constr with_bindings"; hence, its printer cannot be polymorphic in
47
let pr_with_bindings_typed prc prlc (c,bl) =
49
hv 0 (pr_bindings (fun c -> prc (snd c)) (fun c -> prlc (snd c)) bl)
51
let pr_fun_ind_using_typed prc prlc _ opt_c =
54
| Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc (p,b))
57
ARGUMENT EXTEND fun_ind_using
58
TYPED AS constr_with_bindings_opt
59
PRINTED BY pr_fun_ind_using_typed
60
RAW_TYPED AS constr_with_bindings_opt
61
RAW_PRINTED BY pr_fun_ind_using
62
GLOB_TYPED AS constr_with_bindings_opt
63
GLOB_PRINTED BY pr_fun_ind_using
64
| [ "using" constr_with_bindings(c) ] -> [ Some c ]
69
TACTIC EXTEND newfuninv
70
[ "functional" "inversion" quantified_hypothesis(hyp) reference_opt(fname) ] ->
72
Invfun.invfun hyp fname
77
let pr_intro_as_pat prc _ _ pat =
79
| Some pat -> spc () ++ str "as" ++ spc () ++ pr_intro_pattern pat
83
ARGUMENT EXTEND with_names TYPED AS intro_pattern_opt PRINTED BY pr_intro_as_pat
84
| [ "as" simple_intropattern(ipat) ] -> [ Some ipat ]
91
TACTIC EXTEND newfunind
92
["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
97
| c::cl -> applist(c,cl)
99
functional_induction true c princl pat ]
101
(***** debug only ***)
102
TACTIC EXTEND snewfunind
103
["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
105
let c = match cl with
108
| c::cl -> applist(c,cl)
110
functional_induction false c princl pat ]
114
let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_coma prc
116
ARGUMENT EXTEND constr_coma_sequence'
118
PRINTED BY pr_constr_coma_sequence
119
| [ constr(c) "," constr_coma_sequence'(l) ] -> [ c::l ]
120
| [ constr(c) ] -> [ [c] ]
123
let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
125
ARGUMENT EXTEND auto_using'
127
PRINTED BY pr_auto_using
128
| [ "using" constr_coma_sequence'(l) ] -> [ l ]
132
let pr_rec_annotation2_aux s r id l =
133
str ("{"^s^" ") ++ Ppconstr.pr_constr_expr r ++
134
Util.pr_opt Nameops.pr_id id ++
135
Pptactic.pr_auto_using Ppconstr.pr_constr_expr l ++ str "}"
137
let pr_rec_annotation2 = function
138
| Struct id -> str "{struct" ++ Nameops.pr_id id ++ str "}"
139
| Wf(r,id,l) -> pr_rec_annotation2_aux "wf" r id l
140
| Mes(r,id,l) -> pr_rec_annotation2_aux "measure" r id l
142
VERNAC ARGUMENT EXTEND rec_annotation2
143
PRINTED BY pr_rec_annotation2
144
[ "{" "struct" ident(id) "}"] -> [ Struct id ]
145
| [ "{" "wf" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Wf(r,id,l) ]
146
| [ "{" "measure" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Mes(r,id,l) ]
149
let pr_binder2 (idl,c) =
150
str "(" ++ Util.prlist_with_sep spc Nameops.pr_id idl ++ spc () ++
151
str ": " ++ Ppconstr.pr_lconstr_expr c ++ str ")"
153
VERNAC ARGUMENT EXTEND binder2
154
PRINTED BY pr_binder2
155
[ "(" ne_ident_list(idl) ":" lconstr(c) ")"] -> [ (idl,c) ]
158
let make_binder2 (idl,c) =
159
LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,Topconstr.default_binder_kind,c)
161
let pr_rec_definition2 (id,bl,annot,type_,def) =
162
Nameops.pr_id id ++ spc () ++ Util.prlist_with_sep spc pr_binder2 bl ++
163
Util.pr_opt pr_rec_annotation2 annot ++ spc () ++ str ":" ++ spc () ++
164
Ppconstr.pr_lconstr_expr type_ ++ str " :=" ++ spc () ++
165
Ppconstr.pr_lconstr_expr def
167
VERNAC ARGUMENT EXTEND rec_definition2
168
PRINTED BY pr_rec_definition2
169
[ ident(id) binder2_list(bl)
170
rec_annotation2_opt(annot) ":" lconstr(type_)
171
":=" lconstr(def)] ->
172
[ (id,bl,annot,type_,def) ]
175
let make_rec_definitions2 (id,bl,annot,type_,def) =
176
let bl = List.map make_binder2 bl in
177
let names = List.map snd (Topconstr.names_of_local_assums bl) in
178
let check_one_name () =
179
if List.length names > 1 then
181
(Util.dummy_loc,"Function",
182
Pp.str "the recursive argument needs to be specified");
184
let check_exists_args an =
186
let id = match an with
187
| Struct id -> id | Wf(_,Some id,_) -> id | Mes(_,Some id,_) -> id
188
| Wf(_,None,_) | Mes(_,None,_) -> failwith "check_exists_args"
190
(try ignore(Util.list_index0 (Name id) names); annot
191
with Not_found -> Util.user_err_loc
192
(Util.dummy_loc,"Function",
193
Pp.str "No argument named " ++ Nameops.pr_id id)
195
with Failure "check_exists_args" -> check_one_name ();annot
204
((Util.dummy_loc,id), ni, bl, type_, def)
207
VERNAC COMMAND EXTEND Function
208
["Function" ne_rec_definition2_list_sep(recsl,"with")] ->
210
do_generate_principle false (List.map make_rec_definitions2 recsl);
215
let pr_fun_scheme_arg (princ_name,fun_name,s) =
216
Nameops.pr_id princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
217
Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++
218
Ppconstr.pr_rawsort s
220
VERNAC ARGUMENT EXTEND fun_scheme_arg
221
PRINTED BY pr_fun_scheme_arg
222
| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ]
226
let warning_error names e =
228
| Building_graph e ->
230
(str "Cannot define graph(s) for " ++
231
h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++
232
if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
233
| Defining_principle e ->
235
(str "Cannot define principle(s) for "++
236
h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++
237
if do_observe () then Cerrors.explain_exn e else mt ())
241
VERNAC COMMAND EXTEND NewFunctionalScheme
242
["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] ->
246
Functional_principles_types.build_scheme fas
247
with Functional_principles_types.No_graph_found ->
250
| (_,fun_name,_)::_ ->
253
make_graph (Nametab.global fun_name)
256
try Functional_principles_types.build_scheme fas
257
with Functional_principles_types.No_graph_found ->
258
Util.error ("Cannot generate induction principle(s)")
260
let names = List.map (fun (_,na,_) -> na) fas in
261
warning_error names e
264
| _ -> assert false (* we can only have non empty list *)
267
let names = List.map (fun (_,na,_) -> na) fas in
268
warning_error names e
273
(***** debug only ***)
275
VERNAC COMMAND EXTEND NewFunctionalCase
276
["Functional" "Case" fun_scheme_arg(fas) ] ->
278
Functional_principles_types.build_case_scheme fas
282
(***** debug only ***)
283
VERNAC COMMAND EXTEND GenerateGraph
284
["Generate" "graph" "for" reference(c)] -> [ make_graph (Nametab.global c) ]
293
(* comment this line to see debug msgs *)
294
let msg x = () ;; let pr_lconstr c = str ""
295
(* uncomment this to see debugging *)
296
let prconstr c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n")
297
let prlistconstr lc = List.iter prconstr lc
298
let prstr s = msg(str s)
299
let prNamedConstr s c =
302
msg(str(s^"==>\n ") ++ Printer.pr_lconstr c ++ str "\n<==\n");
308
(** Information about an occurrence of a function call (application)
311
fname: constr; (** The function applied *)
312
largs: constr list; (** List of arguments *)
313
free: bool; (** [true] if all arguments are debruijn free *)
314
max_rel: int; (** max debruijn index in the funcall *)
315
onlyvars: bool (** [true] if all arguments are variables (and not debruijn) *)
319
(** [constr_head_match(a b c) a] returns true, false otherwise. *)
320
let constr_head_match u t=
323
let uhd,args= destApp u in
327
(** [hdMatchSub inu t] returns the list of occurrences of [t] in
328
[inu]. DeBruijn are not pushed, so some of them may be unbound in
330
let rec hdMatchSub inu (test: constr -> bool) : fapp_info list =
332
match kind_of_term inu with
333
| Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) ->
334
hdMatchSub tp test @ hdMatchSub (lift 1 cstr) test
335
| Fix (_,(lna,tl,bl)) -> (* not sure Fix is correct *)
337
(fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) test)
339
| _ -> (* Cofix will be wrong *)
342
l @ hdMatchSub cstr test) [] inu in
343
if not (test inu) then subres
345
let f,args = decompose_app inu in
346
let freeset = Termops.free_rels inu in
347
let max_rel = try Util.Intset.max_elt freeset with Not_found -> -1 in
348
{fname = f; largs = args; free = Util.Intset.is_empty freeset;
349
max_rel = max_rel; onlyvars = List.for_all isVar args }
353
mkApp (Coqlib.build_coq_eq(),[| typ; c1; c2|])
356
let poseq_unsafe idunsafe cstr gl =
357
let typ = Tacmach.pf_type_of gl cstr in
359
(Tactics.letin_tac None (Name idunsafe) cstr None allClauses)
361
(Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr))
366
let poseq id cstr gl =
367
let x = Tactics.fresh_id [] id gl in
368
poseq_unsafe x cstr gl
372
let list_constr_largs = ref []
374
let rec poseq_list_ids_rec lcstr gl =
378
match kind_of_term c with
380
(list_constr_largs:=c::!list_constr_largs ; poseq_list_ids_rec lcstr' gl)
382
let _ = prstr "c = " in
383
let _ = prconstr c in
384
let _ = prstr "\n" in
385
let typ = Tacmach.pf_type_of gl c in
386
let cname = Termops.id_of_name_using_hdchar (Global.env()) typ Anonymous in
387
let x = Tactics.fresh_id [] cname gl in
388
let _ = list_constr_largs:=mkVar x :: !list_constr_largs in
389
let _ = prstr " list_constr_largs = " in
390
let _ = prlistconstr !list_constr_largs in
391
let _ = prstr "\n" in
395
(poseq_list_ids_rec lcstr')
398
let poseq_list_ids lcstr gl =
399
let _ = list_constr_largs := [] in
400
poseq_list_ids_rec lcstr gl
402
(** [find_fapp test g] returns the list of [app_info] of all calls to
403
functions that satisfy [test] in the conclusion of goal g. Trivial
404
repetition (not modulo conversion) are deleted. *)
405
let find_fapp (test:constr -> bool) g : fapp_info list =
406
let pre_res = hdMatchSub (Tacmach.pf_concl g) test in
408
List.fold_right (fun x acc -> if List.mem x acc then acc else x::acc) pre_res [] in
409
(prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res);
414
(** [finduction id filter g] tries to apply functional induction on
415
an occurence of function [id] in the conclusion of goal [g]. If
416
[id]=[None] then calls to any function are selected. In any case
417
[heuristic] is used to select the most pertinent occurrence. *)
418
let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info list)
419
(nexttac:Proof_type.tactic) g =
420
let test = match oid with
422
let idconstr = mkConst (const_of_id id) in
423
(fun u -> constr_head_match u idconstr) (* select only id *)
424
| None -> (fun u -> isApp u) in (* select calls to any function *)
425
let info_list = find_fapp test g in
426
let ordered_info_list = heuristic info_list in
427
prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list);
428
if List.length ordered_info_list = 0 then Util.error "function not found in goal\n";
429
let taclist: Proof_type.tactic list =
433
(tclTHEN (poseq_list_ids info.largs)
436
(functional_induction
437
true (applist (info.fname, List.rev !list_constr_largs))
439
nexttac)) ordered_info_list in
440
(* we try each (f t u v) until one does not fail *)
441
(* TODO: try also to mix functional schemes *)
447
(** [chose_heuristic oi x] returns the heuristic for reordering
448
(and/or forgetting some elts of) a list of occurrences of
449
function calls infos to chose first with functional induction. *)
450
let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list =
452
| Some i -> (fun l -> [ List.nth l (i-1) ]) (* occurrence was given by the user *)
454
(* Default heuristic: put first occurrences where all arguments
455
are *bound* (meaning already introduced) variables *)
457
if x.free && x.onlyvars && y.free && y.onlyvars then 0 (* both pertinent *)
458
else if x.free && x.onlyvars then -1
459
else if y.free && y.onlyvars then 1
460
else 0 (* both not pertinent *)
466
TACTIC EXTEND finduction
467
["finduction" ident(id) natural_opt(oi)] ->
470
| Some(n) when n<=0 -> Util.error "numerical argument must be > 0"
472
let heuristic = chose_heuristic oi in
473
finduction (Some id) heuristic tclIDTAC
480
[ "fauto" tactic(tac)] ->
482
let heuristic = chose_heuristic None in
483
finduction None heuristic (snd tac)
488
let heuristic = chose_heuristic None in
489
finduction None heuristic tclIDTAC
496
[ "poseq" ident(x) constr(c) ] ->
500
VERNAC COMMAND EXTEND Showindinfo
501
[ "showindinfo" ident(x) ] -> [ Merge.showind x ]
504
VERNAC COMMAND EXTEND MergeFunind
505
[ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")"
506
"with" "(" ident(id2) ne_ident_list(cl2) ")" "using" ident(id) ] ->
508
let f1 = Constrintern.interp_constr Evd.empty (Global.env())
509
(CRef (Libnames.Ident (Util.dummy_loc,id1))) in
510
let f2 = Constrintern.interp_constr Evd.empty (Global.env())
511
(CRef (Libnames.Ident (Util.dummy_loc,id2))) in
512
let f1type = Typing.type_of (Global.env()) Evd.empty f1 in
513
let f2type = Typing.type_of (Global.env()) Evd.empty f2 in
514
let ar1 = List.length (fst (decompose_prod f1type)) in
515
let ar2 = List.length (fst (decompose_prod f2type)) in
517
if ar1 <> List.length cl1 then
518
Util.error ("not the right number of arguments for " ^ string_of_id id1) in
520
if ar2 <> List.length cl2 then
521
Util.error ("not the right number of arguments for " ^ string_of_id id2) in
522
Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2) id
added
removed
contrib/funind/g_indfun.ml4
