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