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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i camlp4deps: "parsing/grammar.cma" i*)
open Term
open Names
open Pp
open Topconstr
open Indfun_common
open Indfun
open Genarg
TACTIC EXTEND newfuninv
[ "functional" "inversion" ident(hyp) ident(fname) ] ->
[
Invfun.invfun hyp fname
]
END
let pr_fun_ind_using prc _ _ opt_c =
match opt_c with
| None -> mt ()
| Some c -> spc () ++ hov 2 (str "using" ++ spc () ++ prc c)
ARGUMENT EXTEND fun_ind_using
TYPED AS constr_opt
PRINTED BY pr_fun_ind_using
| [ "using" constr(c) ] -> [ Some c ]
| [ ] -> [ None ]
END
let pr_intro_as_pat prc _ _ pat =
str "as" ++ spc () ++ pr_intro_pattern pat
ARGUMENT EXTEND with_names TYPED AS intro_pattern PRINTED BY pr_intro_as_pat
| [ "as" simple_intropattern(ipat) ] -> [ ipat ]
| [] ->[ IntroAnonymous ]
END
let is_rec scheme_info =
let test_branche min acc (_,_,br) =
acc ||
(let new_branche = Sign.it_mkProd_or_LetIn mkProp (fst (Sign.decompose_prod_assum br)) in
let free_rels_in_br = Termops.free_rels new_branche in
let max = min + scheme_info.Tactics.npredicates in
Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br)
in
Util.list_fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
let choose_dest_or_ind scheme_info =
if is_rec scheme_info
then Tactics.new_induct
else
Tactics.new_destruct
TACTIC EXTEND newfunind
["new" "functional" "induction" constr(c) fun_ind_using(princl) with_names(pat)] ->
[
let f,args = decompose_app c in
fun g ->
let princ =
match princl with
| None -> (* No principle is given let's find the good one *)
let fname =
match kind_of_term f with
| Const c' ->
id_of_label (con_label c')
| _ -> Util.error "Must be used with a function"
in
let princ_name =
(
Indrec.make_elimination_ident
fname
(Tacticals.elimination_sort_of_goal g)
)
in
mkConst(const_of_id princ_name )
| Some princ -> princ
in
let princ_type = Tacmach.pf_type_of g princ in
let princ_infos = Tactics.compute_elim_sig princ_type in
let args_as_induction_constr =
let c_list =
if princ_infos.Tactics.farg_in_concl
then [c] else []
in
List.map (fun c -> Tacexpr.ElimOnConstr c) (args@c_list)
in
let princ' = Some (princ,Rawterm.NoBindings) in
choose_dest_or_ind
princ_infos
args_as_induction_constr
princ'
pat g
]
END
VERNAC ARGUMENT EXTEND rec_annotation2
[ "{" "struct" ident(id) "}"] -> [ Struct id ]
| [ "{" "wf" constr(r) ident_opt(id) "}" ] -> [ Wf(r,id) ]
| [ "{" "mes" constr(r) ident_opt(id) "}" ] -> [ Mes(r,id) ]
END
VERNAC ARGUMENT EXTEND binder2
[ "(" ne_ident_list(idl) ":" lconstr(c) ")"] ->
[
LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,c) ]
END
VERNAC ARGUMENT EXTEND rec_definition2
[ ident(id) binder2_list( bl)
rec_annotation2_opt(annot) ":" lconstr( type_)
":=" lconstr(def)] ->
[let names = List.map snd (Topconstr.names_of_local_assums bl) in
let check_one_name () =
if List.length names > 1 then
Util.user_err_loc
(Util.dummy_loc,"GenFixpoint",
Pp.str "the recursive argument needs to be specified");
in
let check_exists_args an =
try
let id = match an with Struct id -> id | Wf(_,Some id) -> id | Mes(_,Some id) -> id | Wf(_,None) | Mes(_,None) -> failwith "check_exists_args" in
(try ignore(Util.list_index (Name id) names - 1); annot
with Not_found -> Util.user_err_loc
(Util.dummy_loc,"GenFixpoint",
Pp.str "No argument named " ++ Nameops.pr_id id)
)
with Failure "check_exists_args" -> check_one_name ();annot
in
let ni =
match annot with
| None ->
annot
| Some an ->
check_exists_args an
in
(id, ni, bl, type_, def) ]
END
VERNAC ARGUMENT EXTEND rec_definitions2
| [ rec_definition2(rd) ] -> [ [rd] ]
| [ rec_definition2(hd) "with" rec_definitions2(tl) ] -> [ hd::tl ]
END
VERNAC COMMAND EXTEND GenFixpoint
["GenFixpoint" rec_definitions2(recsl)] ->
[ do_generate_principle false recsl]
END
VERNAC COMMAND EXTEND IGenFixpoint
["IGenFixpoint" rec_definitions2(recsl)] ->
[ do_generate_principle true recsl]
END
VERNAC ARGUMENT EXTEND fun_scheme_arg
| [ ident(princ_name) ":=" "Induction" "for" ident(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ]
END
VERNAC ARGUMENT EXTEND fun_scheme_args
| [ fun_scheme_arg(fa) ] -> [ [fa] ]
| [ fun_scheme_arg(fa) "with" fun_scheme_args(fas) ] -> [fa::fas]
END
VERNAC COMMAND EXTEND NewFunctionalScheme
["New" "Functional" "Scheme" fun_scheme_args(fas) ] ->
[
New_arg_principle.make_scheme fas
]
END
VERNAC COMMAND EXTEND NewFunctionalCase
["New" "Functional" "Case" fun_scheme_arg(fas) ] ->
[
New_arg_principle.make_case_scheme fas
]
END
VERNAC COMMAND EXTEND GenerateGraph
["Generate" "graph" "for" ident(c)] -> [ make_graph c ]
END
|
