author | wenzelm |
Fri, 06 Mar 2015 15:58:56 +0100 | |
changeset 59621 | 291934bac95e |
parent 59618 | e6939796717e |
child 60682 | 5a6cd2560549 |
permissions | -rw-r--r-- |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
1 |
(* Title: HOL/Tools/Function/function_common.ML |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
2 |
Author: Alexander Krauss, TU Muenchen |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
3 |
|
41114 | 4 |
Common definitions and other infrastructure for the function package. |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
5 |
*) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
6 |
|
34230 | 7 |
signature FUNCTION_DATA = |
8 |
sig |
|
59159 | 9 |
type info = |
10 |
{is_partial : bool, |
|
11 |
defname : string, |
|
12 |
(*contains no logical entities: invariant under morphisms:*) |
|
13 |
add_simps : (binding -> binding) -> string -> (binding -> binding) -> |
|
14 |
Token.src list -> thm list -> local_theory -> thm list * local_theory, |
|
15 |
fnames : string list, |
|
16 |
case_names : string list, |
|
17 |
fs : term list, |
|
18 |
R : term, |
|
19 |
dom: term, |
|
20 |
psimps: thm list, |
|
21 |
pinducts: thm list, |
|
22 |
simps : thm list option, |
|
23 |
inducts : thm list option, |
|
24 |
termination : thm, |
|
25 |
cases : thm list, |
|
26 |
pelims: thm list list, |
|
27 |
elims: thm list list option} |
|
34230 | 28 |
end |
29 |
||
30 |
structure Function_Data : FUNCTION_DATA = |
|
31 |
struct |
|
32 |
||
33 |
type info = |
|
34 |
{is_partial : bool, |
|
35 |
defname : string, |
|
59159 | 36 |
(*contains no logical entities: invariant under morphisms:*) |
34230 | 37 |
add_simps : (binding -> binding) -> string -> (binding -> binding) -> |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57959
diff
changeset
|
38 |
Token.src list -> thm list -> local_theory -> thm list * local_theory, |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
39 |
fnames : string list, |
34230 | 40 |
case_names : string list, |
41 |
fs : term list, |
|
42 |
R : term, |
|
52384 | 43 |
dom: term, |
34230 | 44 |
psimps: thm list, |
45 |
pinducts: thm list, |
|
34231 | 46 |
simps : thm list option, |
47 |
inducts : thm list option, |
|
52383 | 48 |
termination : thm, |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
49 |
cases : thm list, |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
50 |
pelims : thm list list, |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
51 |
elims : thm list list option} |
34230 | 52 |
|
53 |
end |
|
54 |
||
49965 | 55 |
signature FUNCTION_COMMON = |
56 |
sig |
|
57 |
include FUNCTION_DATA |
|
58 |
val profile : bool Unsynchronized.ref |
|
59 |
val PROFILE : string -> ('a -> 'b) -> 'a -> 'b |
|
60 |
val mk_acc : typ -> term -> term |
|
61 |
val function_name : string -> string |
|
62 |
val graph_name : string -> string |
|
63 |
val rel_name : string -> string |
|
64 |
val dom_name : string -> string |
|
59159 | 65 |
val split_def : Proof.context -> (string -> 'a) -> term -> |
66 |
string * (string * typ) list * term list * term list * term |
|
67 |
val check_defs : Proof.context -> ((string * typ) * 'a) list -> term list -> unit |
|
68 |
type fixes = ((string * typ) * mixfix) list |
|
69 |
type 'a spec = (Attrib.binding * 'a list) list |
|
70 |
datatype function_config = FunctionConfig of |
|
71 |
{sequential: bool, |
|
72 |
default: string option, |
|
73 |
domintros: bool, |
|
74 |
partials: bool} |
|
75 |
type preproc = function_config -> Proof.context -> fixes -> term spec -> |
|
76 |
(term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) |
|
77 |
val fname_of : term -> string |
|
78 |
val mk_case_names : int -> string -> int -> string list |
|
79 |
val empty_preproc : (Proof.context -> ((string * typ) * mixfix) list -> term list -> 'c) -> |
|
80 |
preproc |
|
81 |
val termination_rule_tac : Proof.context -> int -> tactic |
|
82 |
val store_termination_rule : thm -> Context.generic -> Context.generic |
|
83 |
val get_functions : Proof.context -> (term * info) Item_Net.T |
|
84 |
val add_function_data : info -> Context.generic -> Context.generic |
|
85 |
val termination_prover_tac : Proof.context -> tactic |
|
86 |
val set_termination_prover : (Proof.context -> tactic) -> Context.generic -> Context.generic |
|
87 |
val get_preproc: Proof.context -> preproc |
|
88 |
val set_preproc: preproc -> Context.generic -> Context.generic |
|
49965 | 89 |
datatype function_result = FunctionResult of |
90 |
{fs: term list, |
|
91 |
G: term, |
|
92 |
R: term, |
|
52384 | 93 |
dom: term, |
49965 | 94 |
psimps : thm list, |
95 |
simple_pinducts : thm list, |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
96 |
cases : thm list, |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
97 |
pelims : thm list list, |
49965 | 98 |
termination : thm, |
99 |
domintros : thm list option} |
|
100 |
val transform_function_data : info -> morphism -> info |
|
101 |
val import_function_data : term -> Proof.context -> info option |
|
102 |
val import_last_function : Proof.context -> info option |
|
103 |
val default_config : function_config |
|
104 |
val function_parser : function_config -> |
|
59159 | 105 |
((function_config * (binding * string option * mixfix) list) * |
106 |
(Attrib.binding * string) list) parser |
|
49965 | 107 |
end |
108 |
||
109 |
structure Function_Common : FUNCTION_COMMON = |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
110 |
struct |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
111 |
|
34230 | 112 |
open Function_Data |
113 |
||
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
114 |
local open Function_Lib in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
115 |
|
59159 | 116 |
|
117 |
(* profiling *) |
|
118 |
||
119 |
val profile = Unsynchronized.ref false |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
120 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
121 |
fun PROFILE msg = if !profile then timeap_msg msg else I |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
122 |
|
54295 | 123 |
val acc_const_name = @{const_name Wellfounded.accp} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
124 |
fun mk_acc domT R = |
59159 | 125 |
Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
126 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
127 |
val function_name = suffix "C" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
128 |
val graph_name = suffix "_graph" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
129 |
val rel_name = suffix "_rel" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
130 |
val dom_name = suffix "_dom" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
131 |
|
59159 | 132 |
|
133 |
(* analyzing function equations *) |
|
134 |
||
135 |
fun split_def ctxt check_head geq = |
|
136 |
let |
|
137 |
fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq] |
|
138 |
val qs = Term.strip_qnt_vars @{const_name Pure.all} geq |
|
139 |
val imp = Term.strip_qnt_body @{const_name Pure.all} geq |
|
140 |
val (gs, eq) = Logic.strip_horn imp |
|
141 |
||
142 |
val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) |
|
143 |
handle TERM _ => error (input_error "Not an equation") |
|
144 |
||
145 |
val (head, args) = strip_comb f_args |
|
146 |
||
147 |
val fname = fst (dest_Free head) handle TERM _ => "" |
|
148 |
val _ = check_head fname |
|
149 |
in |
|
150 |
(fname, qs, gs, args, rhs) |
|
151 |
end |
|
152 |
||
153 |
(*check for all sorts of errors in the input*) |
|
154 |
fun check_defs ctxt fixes eqs = |
|
155 |
let |
|
156 |
val fnames = map (fst o fst) fixes |
|
157 |
||
158 |
fun check geq = |
|
159 |
let |
|
160 |
fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) |
|
161 |
||
162 |
fun check_head fname = |
|
163 |
member (op =) fnames fname orelse |
|
164 |
input_error ("Illegal equation head. Expected " ^ commas_quote fnames) |
|
165 |
||
166 |
val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq |
|
167 |
||
168 |
val _ = length args > 0 orelse input_error "Function has no arguments:" |
|
169 |
||
170 |
fun add_bvs t is = add_loose_bnos (t, 0, is) |
|
171 |
val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs [])) |
|
172 |
|> map (fst o nth (rev qs)) |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
173 |
|
59159 | 174 |
val _ = null rvs orelse input_error |
175 |
("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^ |
|
176 |
" occur" ^ plural "s" "" rvs ^ " on right hand side only:") |
|
177 |
||
178 |
val _ = forall (not o Term.exists_subterm |
|
179 |
(fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args) |
|
180 |
orelse input_error "Defined function may not occur in premises or arguments" |
|
181 |
||
182 |
val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args |
|
183 |
val funvars = |
|
184 |
filter |
|
185 |
(fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs |
|
186 |
val _ = null funvars orelse (warning (cat_lines |
|
187 |
["Bound variable" ^ plural " " "s " funvars ^ |
|
188 |
commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^ |
|
189 |
" in function position.", "Misspelled constructor???"]); true) |
|
190 |
in |
|
191 |
(fname, length args) |
|
192 |
end |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
193 |
|
59159 | 194 |
val grouped_args = AList.group (op =) (map check eqs) |
195 |
val _ = grouped_args |
|
196 |
|> map (fn (fname, ars) => |
|
197 |
length (distinct (op =) ars) = 1 orelse |
|
198 |
error ("Function " ^ quote fname ^ |
|
199 |
" has different numbers of arguments in different equations")) |
|
200 |
||
201 |
val not_defined = subtract (op =) (map fst grouped_args) fnames |
|
202 |
val _ = null not_defined |
|
203 |
orelse error ("No defining equations for function" ^ |
|
204 |
plural " " "s " not_defined ^ commas_quote not_defined) |
|
205 |
||
206 |
fun check_sorts ((fname, fT), _) = |
|
207 |
Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, @{sort type}) |
|
208 |
orelse error (cat_lines |
|
209 |
["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":", |
|
210 |
Syntax.string_of_typ (Config.put show_sorts true ctxt) fT]) |
|
211 |
||
212 |
val _ = map check_sorts fixes |
|
213 |
in |
|
214 |
() |
|
215 |
end |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
216 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
217 |
|
59159 | 218 |
(* preprocessors *) |
219 |
||
220 |
type fixes = ((string * typ) * mixfix) list |
|
221 |
type 'a spec = (Attrib.binding * 'a list) list |
|
222 |
||
223 |
datatype function_config = FunctionConfig of |
|
224 |
{sequential: bool, |
|
225 |
default: string option, |
|
226 |
domintros: bool, |
|
227 |
partials: bool} |
|
228 |
||
229 |
type preproc = function_config -> Proof.context -> fixes -> term spec -> |
|
230 |
(term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) |
|
231 |
||
232 |
val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o |
|
233 |
HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all |
|
234 |
||
235 |
fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k |
|
236 |
| mk_case_names _ _ 0 = [] |
|
237 |
| mk_case_names _ n 1 = [n] |
|
238 |
| mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k) |
|
239 |
||
240 |
fun empty_preproc check (_: function_config) (ctxt: Proof.context) (fixes: fixes) spec = |
|
241 |
let |
|
242 |
val (bnds, tss) = split_list spec |
|
243 |
val ts = flat tss |
|
244 |
val _ = check ctxt fixes ts |
|
245 |
val fnames = map (fst o fst) fixes |
|
246 |
val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts |
|
247 |
||
248 |
fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) |
|
249 |
(indices ~~ xs) |> map (map snd) |
|
250 |
||
251 |
(* using theorem names for case name currently disabled *) |
|
252 |
val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat |
|
253 |
in |
|
254 |
(ts, curry op ~~ bnds o Library.unflat tss, sort, cnames) |
|
255 |
end |
|
256 |
||
257 |
||
258 |
(* context data *) |
|
259 |
||
260 |
structure Data = Generic_Data |
|
261 |
( |
|
262 |
type T = |
|
263 |
thm list * |
|
264 |
(term * info) Item_Net.T * |
|
265 |
(Proof.context -> tactic) * |
|
266 |
preproc |
|
267 |
val empty: T = |
|
268 |
([], |
|
269 |
Item_Net.init (op aconv o apply2 fst) (single o fst), |
|
270 |
fn _ => error "Termination prover not configured", |
|
271 |
empty_preproc check_defs) |
|
272 |
val extend = I |
|
273 |
fun merge |
|
274 |
((termination_rules1, functions1, termination_prover1, preproc1), |
|
275 |
(termination_rules2, functions2, _, _)) : T = |
|
276 |
(Thm.merge_thms (termination_rules1, termination_rules2), |
|
277 |
Item_Net.merge (functions1, functions2), |
|
278 |
termination_prover1, |
|
279 |
preproc1) |
|
280 |
) |
|
281 |
||
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59159
diff
changeset
|
282 |
fun termination_rule_tac ctxt = resolve_tac ctxt (#1 (Data.get (Context.Proof ctxt))) |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59159
diff
changeset
|
283 |
|
59159 | 284 |
val store_termination_rule = Data.map o @{apply 4(1)} o cons |
285 |
||
286 |
val get_functions = #2 o Data.get o Context.Proof |
|
287 |
fun add_function_data (info : info as {fs, termination, ...}) = |
|
288 |
(Data.map o @{apply 4(2)}) (fold (fn f => Item_Net.update (f, info)) fs) |
|
289 |
#> store_termination_rule termination |
|
290 |
||
291 |
fun termination_prover_tac ctxt = #3 (Data.get (Context.Proof ctxt)) ctxt |
|
292 |
val set_termination_prover = Data.map o @{apply 4(3)} o K |
|
293 |
||
294 |
val get_preproc = #4 o Data.get o Context.Proof |
|
295 |
val set_preproc = Data.map o @{apply 4(4)} o K |
|
296 |
||
297 |
||
298 |
(* function definition result data *) |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
299 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
300 |
datatype function_result = FunctionResult of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
301 |
{fs: term list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
302 |
G: term, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
303 |
R: term, |
52384 | 304 |
dom: term, |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
305 |
psimps : thm list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
306 |
simple_pinducts : thm list, |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
307 |
cases : thm list, |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
308 |
pelims : thm list list, |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
309 |
termination : thm, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
310 |
domintros : thm list option} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
311 |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
312 |
fun transform_function_data ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts, |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
313 |
simps, inducts, termination, defname, is_partial, cases, pelims, elims} : info) phi = |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
314 |
let |
45290 | 315 |
val term = Morphism.term phi |
316 |
val thm = Morphism.thm phi |
|
317 |
val fact = Morphism.fact phi |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
318 |
val name = Binding.name_of o Morphism.binding phi o Binding.name |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
319 |
in |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
320 |
{ add_simps = add_simps, case_names = case_names, fnames = fnames, |
52384 | 321 |
fs = map term fs, R = term R, dom = term dom, psimps = fact psimps, |
34231 | 322 |
pinducts = fact pinducts, simps = Option.map fact simps, |
323 |
inducts = Option.map fact inducts, termination = thm termination, |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
324 |
defname = name defname, is_partial=is_partial, cases = fact cases, |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
325 |
elims = Option.map (map fact) elims, pelims = map fact pelims } |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
326 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
327 |
|
59618 | 328 |
fun lift_morphism ctxt f = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
329 |
let |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
330 |
fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of ctxt t)) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
331 |
in |
54740 | 332 |
Morphism.morphism "lift_morphism" |
333 |
{binding = [], |
|
334 |
typ = [Logic.type_map term], |
|
335 |
term = [term], |
|
336 |
fact = [map f]} |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
337 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
338 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
339 |
fun import_function_data t ctxt = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
340 |
let |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
341 |
val ct = Thm.cterm_of ctxt t |
59618 | 342 |
val inst_morph = lift_morphism ctxt o Thm.instantiate |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
343 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
344 |
fun match (trm, data) = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
345 |
SOME (transform_function_data data (inst_morph (Thm.match (Thm.cterm_of ctxt trm, ct)))) |
59618 | 346 |
handle Pattern.MATCH => NONE |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
347 |
in |
59159 | 348 |
get_first match (Item_Net.retrieve (get_functions ctxt) t) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
349 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
350 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
351 |
fun import_last_function ctxt = |
59159 | 352 |
(case Item_Net.content (get_functions ctxt) of |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
353 |
[] => NONE |
49966 | 354 |
| (t, _) :: _ => |
59159 | 355 |
let val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
356 |
in import_function_data t' ctxt' end) |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
357 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
358 |
|
59159 | 359 |
(* configuration management *) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
360 |
|
59159 | 361 |
datatype function_opt = |
362 |
Sequential |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
363 |
| Default of string |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
364 |
| DomIntros |
33101 | 365 |
| No_Partials |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
366 |
|
59159 | 367 |
fun apply_opt Sequential (FunctionConfig {sequential = _, default, domintros, partials}) = |
368 |
FunctionConfig |
|
369 |
{sequential = true, default = default, domintros = domintros, partials = partials} |
|
370 |
| apply_opt (Default d) (FunctionConfig {sequential, default = _, domintros, partials}) = |
|
371 |
FunctionConfig |
|
372 |
{sequential = sequential, default = SOME d, domintros = domintros, partials = partials} |
|
373 |
| apply_opt DomIntros (FunctionConfig {sequential, default, domintros = _, partials}) = |
|
374 |
FunctionConfig |
|
375 |
{sequential = sequential, default = default, domintros = true, partials = partials} |
|
376 |
| apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials = _}) = |
|
377 |
FunctionConfig |
|
378 |
{sequential = sequential, default = default, domintros = domintros, partials = false} |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
379 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
380 |
val default_config = |
41417 | 381 |
FunctionConfig { sequential=false, default=NONE, |
41846
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
382 |
domintros=false, partials=true} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
383 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
384 |
local |
44357 | 385 |
val option_parser = Parse.group (fn () => "option") |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
386 |
((Parse.reserved "sequential" >> K Sequential) |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
387 |
|| ((Parse.reserved "default" |-- Parse.term) >> Default) |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
388 |
|| (Parse.reserved "domintros" >> K DomIntros) |
41846
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
389 |
|| (Parse.reserved "no_partials" >> K No_Partials)) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
390 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
391 |
fun config_parser default = |
46949 | 392 |
(Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) []) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
393 |
>> (fn opts => fold apply_opt opts default) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
394 |
in |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
395 |
fun function_parser default_cfg = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
396 |
config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
397 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
398 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
399 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
400 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
401 |
end |