author | wenzelm |
Wed, 26 Nov 2014 20:05:34 +0100 | |
changeset 59058 | a78612c67ec0 |
parent 58011 | bc6bced136e5 |
child 59159 | 9312710451f5 |
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 |
|
9 |
||
10 |
type info = |
|
11 |
{is_partial : bool, |
|
12 |
defname : string, |
|
13 |
(* contains no logical entities: invariant under morphisms: *) |
|
14 |
add_simps : (binding -> binding) -> string -> (binding -> binding) -> |
|
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57959
diff
changeset
|
15 |
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
|
16 |
fnames : string list, |
34230 | 17 |
case_names : string list, |
18 |
fs : term list, |
|
19 |
R : term, |
|
52384 | 20 |
dom: term, |
34230 | 21 |
psimps: thm list, |
22 |
pinducts: thm list, |
|
34231 | 23 |
simps : thm list option, |
24 |
inducts : thm list option, |
|
52383 | 25 |
termination : thm, |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
26 |
cases : thm list, |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
27 |
pelims: thm list list, |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
28 |
elims: thm list list option} |
34230 | 29 |
|
30 |
end |
|
31 |
||
32 |
structure Function_Data : FUNCTION_DATA = |
|
33 |
struct |
|
34 |
||
35 |
type info = |
|
36 |
{is_partial : bool, |
|
37 |
defname : string, |
|
38 |
(* contains no logical entities: invariant under morphisms: *) |
|
39 |
add_simps : (binding -> binding) -> string -> (binding -> binding) -> |
|
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57959
diff
changeset
|
40 |
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
|
41 |
fnames : string list, |
34230 | 42 |
case_names : string list, |
43 |
fs : term list, |
|
44 |
R : term, |
|
52384 | 45 |
dom: term, |
34230 | 46 |
psimps: thm list, |
47 |
pinducts: thm list, |
|
34231 | 48 |
simps : thm list option, |
49 |
inducts : thm list option, |
|
52383 | 50 |
termination : thm, |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
51 |
cases : thm list, |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
52 |
pelims : thm list list, |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
53 |
elims : thm list list option} |
34230 | 54 |
|
55 |
end |
|
56 |
||
49965 | 57 |
signature FUNCTION_COMMON = |
58 |
sig |
|
59 |
include FUNCTION_DATA |
|
60 |
val profile : bool Unsynchronized.ref |
|
61 |
val PROFILE : string -> ('a -> 'b) -> 'a -> 'b |
|
62 |
val mk_acc : typ -> term -> term |
|
63 |
val function_name : string -> string |
|
64 |
val graph_name : string -> string |
|
65 |
val rel_name : string -> string |
|
66 |
val dom_name : string -> string |
|
67 |
val apply_termination_rule : Proof.context -> int -> tactic |
|
68 |
datatype function_result = FunctionResult of |
|
69 |
{fs: term list, |
|
70 |
G: term, |
|
71 |
R: term, |
|
52384 | 72 |
dom: term, |
49965 | 73 |
psimps : thm list, |
74 |
simple_pinducts : thm list, |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
75 |
cases : thm list, |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
76 |
pelims : thm list list, |
49965 | 77 |
termination : thm, |
78 |
domintros : thm list option} |
|
79 |
val transform_function_data : info -> morphism -> info |
|
80 |
val get_function : Proof.context -> (term * info) Item_Net.T |
|
81 |
val import_function_data : term -> Proof.context -> info option |
|
82 |
val import_last_function : Proof.context -> info option |
|
83 |
val add_function_data : info -> Context.generic -> Context.generic |
|
84 |
val set_termination_prover : (Proof.context -> tactic) -> Context.generic -> Context.generic |
|
85 |
val get_termination_prover : Proof.context -> tactic |
|
49979
4de92b4aa74a
added function store_termination_rule to the signature, as it is used in Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
49966
diff
changeset
|
86 |
val store_termination_rule : thm -> Context.generic -> Context.generic |
49965 | 87 |
datatype function_config = FunctionConfig of |
88 |
{sequential: bool, |
|
89 |
default: string option, |
|
90 |
domintros: bool, |
|
91 |
partials: bool} |
|
92 |
val default_config : function_config |
|
93 |
val split_def : Proof.context -> (string -> 'a) -> term -> |
|
94 |
string * (string * typ) list * term list * term list * term |
|
95 |
val check_defs : Proof.context -> ((string * typ) * 'a) list -> term list -> unit |
|
96 |
type fixes = ((string * typ) * mixfix) list |
|
97 |
type 'a spec = (Attrib.binding * 'a list) list |
|
98 |
type preproc = function_config -> Proof.context -> fixes -> term spec -> |
|
99 |
(term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) |
|
100 |
val fname_of : term -> string |
|
101 |
val mk_case_names : int -> string -> int -> string list |
|
102 |
val empty_preproc : (Proof.context -> ((string * typ) * mixfix) list -> term list -> 'c) -> preproc |
|
103 |
val get_preproc: Proof.context -> preproc |
|
104 |
val set_preproc: preproc -> Context.generic -> Context.generic |
|
105 |
val function_parser : function_config -> |
|
106 |
((function_config * (binding * string option * mixfix) list) * (Attrib.binding * string) list) parser |
|
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 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
116 |
(* Profiling *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
117 |
val profile = Unsynchronized.ref false; |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
118 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
119 |
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
|
120 |
|
54295 | 121 |
val acc_const_name = @{const_name Wellfounded.accp} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
122 |
fun mk_acc domT R = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
123 |
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
|
124 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
125 |
val function_name = suffix "C" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
126 |
val graph_name = suffix "_graph" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
127 |
val rel_name = suffix "_rel" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
128 |
val dom_name = suffix "_dom" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
129 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
130 |
(* Termination rules *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
131 |
|
46042 | 132 |
(* FIXME just one data slot (record) per program unit *) |
33519 | 133 |
structure TerminationRule = Generic_Data |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
134 |
( |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
135 |
type T = thm list |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
136 |
val empty = [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
137 |
val extend = I |
33519 | 138 |
val merge = Thm.merge_thms |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
139 |
); |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
140 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
141 |
val get_termination_rules = TerminationRule.get |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
142 |
val store_termination_rule = TerminationRule.map o cons |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
143 |
val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
144 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
145 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
146 |
(* Function definition result data *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
147 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
148 |
datatype function_result = FunctionResult of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
149 |
{fs: term list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
150 |
G: term, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
151 |
R: term, |
52384 | 152 |
dom: term, |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
153 |
psimps : thm list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
154 |
simple_pinducts : thm list, |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
155 |
cases : thm list, |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
156 |
pelims : thm list list, |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
157 |
termination : thm, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
158 |
domintros : thm list option} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
159 |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
160 |
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
|
161 |
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
|
162 |
let |
45290 | 163 |
val term = Morphism.term phi |
164 |
val thm = Morphism.thm phi |
|
165 |
val fact = Morphism.fact phi |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
166 |
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
|
167 |
in |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
168 |
{ add_simps = add_simps, case_names = case_names, fnames = fnames, |
52384 | 169 |
fs = map term fs, R = term R, dom = term dom, psimps = fact psimps, |
34231 | 170 |
pinducts = fact pinducts, simps = Option.map fact simps, |
171 |
inducts = Option.map fact inducts, termination = thm termination, |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
172 |
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
|
173 |
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
|
174 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
175 |
|
46042 | 176 |
(* FIXME just one data slot (record) per program unit *) |
33519 | 177 |
structure FunctionData = Generic_Data |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
178 |
( |
34230 | 179 |
type T = (term * info) Item_Net.T; |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58011
diff
changeset
|
180 |
val empty : T = Item_Net.init (op aconv o apply2 fst) (single o fst); |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
181 |
val extend = I; |
33519 | 182 |
fun merge tabs : T = Item_Net.merge tabs; |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
183 |
) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
184 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
185 |
val get_function = FunctionData.get o Context.Proof; |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
186 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
187 |
fun lift_morphism thy f = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
188 |
let |
46496
b8920f3fd259
discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);
wenzelm
parents:
46042
diff
changeset
|
189 |
fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t)) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
190 |
in |
54740 | 191 |
Morphism.morphism "lift_morphism" |
192 |
{binding = [], |
|
193 |
typ = [Logic.type_map term], |
|
194 |
term = [term], |
|
195 |
fact = [map f]} |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
196 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
197 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
198 |
fun import_function_data t ctxt = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
199 |
let |
42361 | 200 |
val thy = Proof_Context.theory_of ctxt |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
201 |
val ct = cterm_of thy t |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
202 |
val inst_morph = lift_morphism thy o Thm.instantiate |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
203 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
204 |
fun match (trm, data) = |
45290 | 205 |
SOME (transform_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct)))) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
206 |
handle Pattern.MATCH => NONE |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
207 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
208 |
get_first match (Item_Net.retrieve (get_function ctxt) t) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
209 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
210 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
211 |
fun import_last_function ctxt = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
212 |
case Item_Net.content (get_function ctxt) of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
213 |
[] => NONE |
49966 | 214 |
| (t, _) :: _ => |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
215 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
216 |
val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
217 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
218 |
import_function_data t' ctxt' |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
219 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
220 |
|
34230 | 221 |
fun add_function_data (data : info as {fs, termination, ...}) = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
222 |
FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
223 |
#> store_termination_rule termination |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
224 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
225 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
226 |
(* Default Termination Prover *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
227 |
|
46042 | 228 |
(* FIXME just one data slot (record) per program unit *) |
33519 | 229 |
structure TerminationProver = Generic_Data |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
230 |
( |
36521 | 231 |
type T = Proof.context -> tactic |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
232 |
val empty = (fn _ => error "Termination prover not configured") |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
233 |
val extend = I |
38761 | 234 |
fun merge (a, _) = a |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
235 |
) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
236 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
237 |
val set_termination_prover = TerminationProver.put |
49965 | 238 |
fun get_termination_prover ctxt = TerminationProver.get (Context.Proof ctxt) ctxt |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
239 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
240 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
241 |
(* Configuration management *) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
242 |
datatype function_opt |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
243 |
= Sequential |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
244 |
| Default of string |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
245 |
| DomIntros |
33101 | 246 |
| No_Partials |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
247 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
248 |
datatype function_config = FunctionConfig of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
249 |
{sequential: bool, |
41417 | 250 |
default: string option, |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
251 |
domintros: bool, |
41846
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
252 |
partials: bool} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
253 |
|
41846
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
254 |
fun apply_opt Sequential (FunctionConfig {sequential, default, domintros, partials}) = |
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
255 |
FunctionConfig {sequential=true, default=default, domintros=domintros, partials=partials} |
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
256 |
| apply_opt (Default d) (FunctionConfig {sequential, default, domintros, partials}) = |
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
257 |
FunctionConfig {sequential=sequential, default=SOME d, domintros=domintros, partials=partials} |
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
258 |
| apply_opt DomIntros (FunctionConfig {sequential, default, domintros, partials}) = |
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
259 |
FunctionConfig {sequential=sequential, default=default, domintros=true, partials=partials} |
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
260 |
| apply_opt No_Partials (FunctionConfig {sequential, default, domintros, partials}) = |
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
261 |
FunctionConfig {sequential=sequential, default=default, domintros=domintros, partials=false} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
262 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
263 |
val default_config = |
41417 | 264 |
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
|
265 |
domintros=false, partials=true} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
266 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
267 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
268 |
(* Analyzing function equations *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
269 |
|
39276
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
39134
diff
changeset
|
270 |
fun split_def ctxt check_head geq = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
271 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
272 |
fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq] |
56245 | 273 |
val qs = Term.strip_qnt_vars @{const_name Pure.all} geq |
274 |
val imp = Term.strip_qnt_body @{const_name Pure.all} geq |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
275 |
val (gs, eq) = Logic.strip_horn imp |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
276 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
277 |
val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
278 |
handle TERM _ => error (input_error "Not an equation") |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
279 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
280 |
val (head, args) = strip_comb f_args |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
281 |
|
39276
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
39134
diff
changeset
|
282 |
val fname = fst (dest_Free head) handle TERM _ => "" |
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
39134
diff
changeset
|
283 |
val _ = check_head fname |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
284 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
285 |
(fname, qs, gs, args, rhs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
286 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
287 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
288 |
(* Check for all sorts of errors in the input *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
289 |
fun check_defs ctxt fixes eqs = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
290 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
291 |
val fnames = map (fst o fst) fixes |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
292 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
293 |
fun check geq = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
294 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
295 |
fun input_error msg = error (cat_lines [msg, Syntax.string_of_term ctxt geq]) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
296 |
|
39276
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
39134
diff
changeset
|
297 |
fun check_head fname = |
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
39134
diff
changeset
|
298 |
member (op =) fnames fname orelse |
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
39134
diff
changeset
|
299 |
input_error ("Illegal equation head. Expected " ^ commas_quote fnames) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
300 |
|
39276
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
39134
diff
changeset
|
301 |
val (fname, qs, gs, args, rhs) = split_def ctxt check_head geq |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
302 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
303 |
val _ = length args > 0 orelse input_error "Function has no arguments:" |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
304 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
305 |
fun add_bvs t is = add_loose_bnos (t, 0, is) |
42081 | 306 |
val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs [])) |
307 |
|> map (fst o nth (rev qs)) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
308 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
309 |
val _ = null rvs orelse input_error |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
310 |
("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^ |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
311 |
" occur" ^ plural "s" "" rvs ^ " on right hand side only:") |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
312 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
313 |
val _ = forall (not o Term.exists_subterm |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36521
diff
changeset
|
314 |
(fn Free (n, _) => member (op =) fnames n | _ => false)) (gs @ args) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
315 |
orelse input_error "Defined function may not occur in premises or arguments" |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
316 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
317 |
val freeargs = map (fn t => subst_bounds (rev (map Free qs), t)) args |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
318 |
val funvars = filter (fn q => exists (exists_subterm (fn (Free q') $ _ => q = q' | _ => false)) freeargs) qs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
319 |
val _ = null funvars orelse (warning (cat_lines |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
320 |
["Bound variable" ^ plural " " "s " funvars ^ |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
321 |
commas_quote (map fst funvars) ^ " occur" ^ plural "s" "" funvars ^ |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
322 |
" in function position.", "Misspelled constructor???"]); true) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
323 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
324 |
(fname, length args) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
325 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
326 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
327 |
val grouped_args = AList.group (op =) (map check eqs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
328 |
val _ = grouped_args |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
329 |
|> map (fn (fname, ars) => |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
330 |
length (distinct (op =) ars) = 1 |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
331 |
orelse error ("Function " ^ quote fname ^ |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
332 |
" has different numbers of arguments in different equations")) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
333 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
334 |
val not_defined = subtract (op =) (map fst grouped_args) fnames |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
335 |
val _ = null not_defined |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
336 |
orelse error ("No defining equations for function" ^ |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
337 |
plural " " "s " not_defined ^ commas_quote not_defined) |
33751
7ead0ccf6cbd
check if equations are present for all functions to avoid low-level exception later
krauss
parents:
33519
diff
changeset
|
338 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
339 |
fun check_sorts ((fname, fT), _) = |
56254 | 340 |
Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, @{sort type}) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
341 |
orelse error (cat_lines |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
342 |
["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":", |
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
38764
diff
changeset
|
343 |
Syntax.string_of_typ (Config.put show_sorts true ctxt) fT]) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
344 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
345 |
val _ = map check_sorts fixes |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
346 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
347 |
() |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
348 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
349 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
350 |
(* Preprocessors *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
351 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
352 |
type fixes = ((string * typ) * mixfix) list |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
353 |
type 'a spec = (Attrib.binding * 'a list) list |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
354 |
type preproc = function_config -> Proof.context -> fixes -> term spec -> |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
355 |
(term list * (thm list -> thm spec) * (thm list -> thm list list) * string list) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
356 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
357 |
val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
358 |
HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
359 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
360 |
fun mk_case_names i "" k = mk_case_names i (string_of_int (i + 1)) k |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
361 |
| mk_case_names _ n 0 = [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
362 |
| mk_case_names _ n 1 = [n] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
363 |
| mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
364 |
|
49965 | 365 |
fun empty_preproc check (_: function_config) (ctxt: Proof.context) (fixes: fixes) spec = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
366 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
367 |
val (bnds, tss) = split_list spec |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
368 |
val ts = flat tss |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
369 |
val _ = check ctxt fixes ts |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
370 |
val fnames = map (fst o fst) fixes |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
371 |
val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
372 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
373 |
fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
374 |
(indices ~~ xs) |> map (map snd) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
375 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
376 |
(* using theorem names for case name currently disabled *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
377 |
val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
378 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
379 |
(ts, curry op ~~ bnds o Library.unflat tss, sort, cnames) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
380 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
381 |
|
46042 | 382 |
(* FIXME just one data slot (record) per program unit *) |
33519 | 383 |
structure Preprocessor = Generic_Data |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
384 |
( |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
385 |
type T = preproc |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
386 |
val empty : T = empty_preproc check_defs |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
387 |
val extend = I |
33519 | 388 |
fun merge (a, _) = a |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
389 |
) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
390 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
391 |
val get_preproc = Preprocessor.get o Context.Proof |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
392 |
val set_preproc = Preprocessor.map o K |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
393 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
394 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
395 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
396 |
local |
44357 | 397 |
val option_parser = Parse.group (fn () => "option") |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
398 |
((Parse.reserved "sequential" >> K Sequential) |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
399 |
|| ((Parse.reserved "default" |-- Parse.term) >> Default) |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
400 |
|| (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
|
401 |
|| (Parse.reserved "no_partials" >> K No_Partials)) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
402 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
403 |
fun config_parser default = |
46949 | 404 |
(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
|
405 |
>> (fn opts => fold apply_opt opts default) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
406 |
in |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
407 |
fun function_parser default_cfg = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
408 |
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
|
409 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
410 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
411 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
412 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
413 |
end |