1 (* Title: HOL/Tools/function_package/fundef_common.ML |
|
2 Author: Alexander Krauss, TU Muenchen |
|
3 |
|
4 A package for general recursive function definitions. |
|
5 Common definitions and other infrastructure. |
|
6 *) |
|
7 |
|
8 structure FundefCommon = |
|
9 struct |
|
10 |
|
11 local open FundefLib in |
|
12 |
|
13 (* Profiling *) |
|
14 val profile = ref false; |
|
15 |
|
16 fun PROFILE msg = if !profile then timeap_msg msg else I |
|
17 |
|
18 |
|
19 val acc_const_name = @{const_name "accp"} |
|
20 fun mk_acc domT R = |
|
21 Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R |
|
22 |
|
23 val function_name = suffix "C" |
|
24 val graph_name = suffix "_graph" |
|
25 val rel_name = suffix "_rel" |
|
26 val dom_name = suffix "_dom" |
|
27 |
|
28 (* Termination rules *) |
|
29 |
|
30 structure TerminationRule = GenericDataFun |
|
31 ( |
|
32 type T = thm list |
|
33 val empty = [] |
|
34 val extend = I |
|
35 fun merge _ = Thm.merge_thms |
|
36 ); |
|
37 |
|
38 val get_termination_rules = TerminationRule.get |
|
39 val store_termination_rule = TerminationRule.map o cons |
|
40 val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof |
|
41 |
|
42 |
|
43 (* Function definition result data *) |
|
44 |
|
45 datatype fundef_result = |
|
46 FundefResult of |
|
47 { |
|
48 fs: term list, |
|
49 G: term, |
|
50 R: term, |
|
51 |
|
52 psimps : thm list, |
|
53 trsimps : thm list option, |
|
54 |
|
55 simple_pinducts : thm list, |
|
56 cases : thm, |
|
57 termination : thm, |
|
58 domintros : thm list option |
|
59 } |
|
60 |
|
61 |
|
62 datatype fundef_context_data = |
|
63 FundefCtxData of |
|
64 { |
|
65 defname : string, |
|
66 |
|
67 (* contains no logical entities: invariant under morphisms *) |
|
68 add_simps : (binding -> binding) -> string -> Attrib.src list -> thm list |
|
69 -> local_theory -> thm list * local_theory, |
|
70 case_names : string list, |
|
71 |
|
72 fs : term list, |
|
73 R : term, |
|
74 |
|
75 psimps: thm list, |
|
76 pinducts: thm list, |
|
77 termination: thm |
|
78 } |
|
79 |
|
80 fun morph_fundef_data (FundefCtxData {add_simps, case_names, fs, R, |
|
81 psimps, pinducts, termination, defname}) phi = |
|
82 let |
|
83 val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi |
|
84 val name = Binding.name_of o Morphism.binding phi o Binding.name |
|
85 in |
|
86 FundefCtxData { add_simps = add_simps, case_names = case_names, |
|
87 fs = map term fs, R = term R, psimps = fact psimps, |
|
88 pinducts = fact pinducts, termination = thm termination, |
|
89 defname = name defname } |
|
90 end |
|
91 |
|
92 structure FundefData = GenericDataFun |
|
93 ( |
|
94 type T = (term * fundef_context_data) Item_Net.T; |
|
95 val empty = Item_Net.init |
|
96 (op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool) |
|
97 fst; |
|
98 val copy = I; |
|
99 val extend = I; |
|
100 fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2) |
|
101 ); |
|
102 |
|
103 val get_fundef = FundefData.get o Context.Proof; |
|
104 |
|
105 |
|
106 (* Generally useful?? *) |
|
107 fun lift_morphism thy f = |
|
108 let |
|
109 val term = Drule.term_rule thy f |
|
110 in |
|
111 Morphism.thm_morphism f $> Morphism.term_morphism term |
|
112 $> Morphism.typ_morphism (Logic.type_map term) |
|
113 end |
|
114 |
|
115 fun import_fundef_data t ctxt = |
|
116 let |
|
117 val thy = ProofContext.theory_of ctxt |
|
118 val ct = cterm_of thy t |
|
119 val inst_morph = lift_morphism thy o Thm.instantiate |
|
120 |
|
121 fun match (trm, data) = |
|
122 SOME (morph_fundef_data data (inst_morph (Thm.match (cterm_of thy trm, ct)))) |
|
123 handle Pattern.MATCH => NONE |
|
124 in |
|
125 get_first match (Item_Net.retrieve (get_fundef ctxt) t) |
|
126 end |
|
127 |
|
128 fun import_last_fundef ctxt = |
|
129 case Item_Net.content (get_fundef ctxt) of |
|
130 [] => NONE |
|
131 | (t, data) :: _ => |
|
132 let |
|
133 val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
|
134 in |
|
135 import_fundef_data t' ctxt' |
|
136 end |
|
137 |
|
138 val all_fundef_data = Item_Net.content o get_fundef |
|
139 |
|
140 fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) = |
|
141 FundefData.map (fold (fn f => Item_Net.insert (f, data)) fs) |
|
142 #> store_termination_rule termination |
|
143 |
|
144 |
|
145 (* Simp rules for termination proofs *) |
|
146 |
|
147 structure TerminationSimps = NamedThmsFun |
|
148 ( |
|
149 val name = "termination_simp" |
|
150 val description = "Simplification rule for termination proofs" |
|
151 ); |
|
152 |
|
153 |
|
154 (* Default Termination Prover *) |
|
155 |
|
156 structure TerminationProver = GenericDataFun |
|
157 ( |
|
158 type T = Proof.context -> Proof.method |
|
159 val empty = (fn _ => error "Termination prover not configured") |
|
160 val extend = I |
|
161 fun merge _ (a,b) = b (* FIXME *) |
|
162 ); |
|
163 |
|
164 val set_termination_prover = TerminationProver.put |
|
165 val get_termination_prover = TerminationProver.get o Context.Proof |
|
166 |
|
167 |
|
168 (* Configuration management *) |
|
169 datatype fundef_opt |
|
170 = Sequential |
|
171 | Default of string |
|
172 | DomIntros |
|
173 | Tailrec |
|
174 |
|
175 datatype fundef_config |
|
176 = FundefConfig of |
|
177 { |
|
178 sequential: bool, |
|
179 default: string, |
|
180 domintros: bool, |
|
181 tailrec: bool |
|
182 } |
|
183 |
|
184 fun apply_opt Sequential (FundefConfig {sequential, default, domintros,tailrec}) = |
|
185 FundefConfig {sequential=true, default=default, domintros=domintros, tailrec=tailrec} |
|
186 | apply_opt (Default d) (FundefConfig {sequential, default, domintros,tailrec}) = |
|
187 FundefConfig {sequential=sequential, default=d, domintros=domintros, tailrec=tailrec} |
|
188 | apply_opt DomIntros (FundefConfig {sequential, default, domintros,tailrec}) = |
|
189 FundefConfig {sequential=sequential, default=default, domintros=true,tailrec=tailrec} |
|
190 | apply_opt Tailrec (FundefConfig {sequential, default, domintros,tailrec}) = |
|
191 FundefConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true} |
|
192 |
|
193 val default_config = |
|
194 FundefConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), |
|
195 domintros=false, tailrec=false } |
|
196 |
|
197 |
|
198 (* Analyzing function equations *) |
|
199 |
|
200 fun split_def ctxt geq = |
|
201 let |
|
202 fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq] |
|
203 val qs = Term.strip_qnt_vars "all" geq |
|
204 val imp = Term.strip_qnt_body "all" geq |
|
205 val (gs, eq) = Logic.strip_horn imp |
|
206 |
|
207 val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) |
|
208 handle TERM _ => error (input_error "Not an equation") |
|
209 |
|
210 val (head, args) = strip_comb f_args |
|
211 |
|
212 val fname = fst (dest_Free head) |
|
213 handle TERM _ => error (input_error "Head symbol must not be a bound variable") |
|
214 in |
|
215 (fname, qs, gs, args, rhs) |
|
216 end |
|
217 |
|
218 (* Check for all sorts of errors in the input *) |
|
219 fun check_defs ctxt fixes eqs = |
|
220 let |
|
221 val fnames = map (fst o fst) fixes |
|
222 |
|
223 fun check geq = |
|
224 let |
|
225 fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) |
|
226 |
|
227 val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq |
|
228 |
|
229 val _ = fname mem fnames |
|
230 orelse input_error |
|
231 ("Head symbol of left hand side must be " |
|
232 ^ plural "" "one out of " fnames ^ commas_quote fnames) |
|
233 |
|
234 val _ = length args > 0 orelse input_error "Function has no arguments:" |
|
235 |
|
236 fun add_bvs t is = add_loose_bnos (t, 0, is) |
|
237 val rvs = (add_bvs rhs [] \\ fold add_bvs args []) |
|
238 |> map (fst o nth (rev qs)) |
|
239 |
|
240 val _ = null rvs orelse input_error |
|
241 ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs |
|
242 ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:") |
|
243 |
|
244 val _ = forall (not o Term.exists_subterm |
|
245 (fn Free (n, _) => n mem fnames | _ => false)) (gs @ args) |
|
246 orelse input_error "Defined function may not occur in premises or arguments" |
|
247 |
|
248 val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args |
|
249 val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs |
|
250 val _ = null funvars |
|
251 orelse (warning (cat_lines |
|
252 ["Bound variable" ^ plural " " "s " funvars |
|
253 ^ commas_quote (map fst funvars) ^ |
|
254 " occur" ^ plural "s" "" funvars ^ " in function position.", |
|
255 "Misspelled constructor???"]); true) |
|
256 in |
|
257 (fname, length args) |
|
258 end |
|
259 |
|
260 val _ = AList.group (op =) (map check eqs) |
|
261 |> map (fn (fname, ars) => |
|
262 length (distinct (op =) ars) = 1 |
|
263 orelse error ("Function " ^ quote fname ^ |
|
264 " has different numbers of arguments in different equations")) |
|
265 |
|
266 fun check_sorts ((fname, fT), _) = |
|
267 Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS) |
|
268 orelse error (cat_lines |
|
269 ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":", |
|
270 setmp show_sorts true (Syntax.string_of_typ ctxt) fT]) |
|
271 |
|
272 val _ = map check_sorts fixes |
|
273 in |
|
274 () |
|
275 end |
|
276 |
|
277 (* Preprocessors *) |
|
278 |
|
279 type fixes = ((string * typ) * mixfix) list |
|
280 type 'a spec = (Attrib.binding * 'a list) list |
|
281 type preproc = fundef_config -> Proof.context -> fixes -> term spec |
|
282 -> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) |
|
283 |
|
284 val fname_of = fst o dest_Free o fst o strip_comb o fst |
|
285 o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all |
|
286 |
|
287 fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k |
|
288 | mk_case_names _ n 0 = [] |
|
289 | mk_case_names _ n 1 = [n] |
|
290 | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k) |
|
291 |
|
292 fun empty_preproc check _ ctxt fixes spec = |
|
293 let |
|
294 val (bnds, tss) = split_list spec |
|
295 val ts = flat tss |
|
296 val _ = check ctxt fixes ts |
|
297 val fnames = map (fst o fst) fixes |
|
298 val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts |
|
299 |
|
300 fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) |
|
301 (indices ~~ xs) |
|
302 |> map (map snd) |
|
303 |
|
304 (* using theorem names for case name currently disabled *) |
|
305 val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat |
|
306 in |
|
307 (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames) |
|
308 end |
|
309 |
|
310 structure Preprocessor = GenericDataFun |
|
311 ( |
|
312 type T = preproc |
|
313 val empty : T = empty_preproc check_defs |
|
314 val extend = I |
|
315 fun merge _ (a, _) = a |
|
316 ); |
|
317 |
|
318 val get_preproc = Preprocessor.get o Context.Proof |
|
319 val set_preproc = Preprocessor.map o K |
|
320 |
|
321 |
|
322 |
|
323 local |
|
324 structure P = OuterParse and K = OuterKeyword |
|
325 |
|
326 val option_parser = |
|
327 P.group "option" ((P.reserved "sequential" >> K Sequential) |
|
328 || ((P.reserved "default" |-- P.term) >> Default) |
|
329 || (P.reserved "domintros" >> K DomIntros) |
|
330 || (P.reserved "tailrec" >> K Tailrec)) |
|
331 |
|
332 fun config_parser default = |
|
333 (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") []) |
|
334 >> (fn opts => fold apply_opt opts default) |
|
335 in |
|
336 fun fundef_parser default_cfg = |
|
337 config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs |
|
338 end |
|
339 |
|
340 |
|
341 end |
|
342 end |
|
343 |
|