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