author | wenzelm |
Thu, 10 Apr 2008 14:53:31 +0200 | |
changeset 26615 | 8a9d3eebd534 |
parent 26604 | 3f757f8acf44 |
child 26662 | 39483503705f |
permissions | -rw-r--r-- |
24219 | 1 |
(* Title: Tools/code/code_package.ML |
2 |
ID: $Id$ |
|
3 |
Author: Florian Haftmann, TU Muenchen |
|
4 |
||
24918 | 5 |
Code generator interfaces and Isar setup. |
24219 | 6 |
*) |
7 |
||
8 |
signature CODE_PACKAGE = |
|
9 |
sig |
|
26011 | 10 |
val evaluate_conv: theory |
24381 | 11 |
-> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm |
12 |
-> string list -> cterm -> thm) |
|
24283 | 13 |
-> cterm -> thm; |
26011 | 14 |
val evaluate_term: theory |
24381 | 15 |
-> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24811
diff
changeset
|
16 |
-> string list -> term -> 'a) |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24811
diff
changeset
|
17 |
-> term -> 'a; |
26011 | 18 |
val eval_conv: string * (unit -> thm) option ref |
19 |
-> theory -> cterm -> string list -> thm; |
|
20 |
val eval_term: string * (unit -> 'a) option ref |
|
21 |
-> theory -> term -> string list -> 'a; |
|
22 |
val satisfies: theory -> term -> string list -> bool; |
|
24585 | 23 |
val satisfies_ref: (unit -> bool) option ref; |
25611 | 24 |
val codegen_shell_command: string (*theory name*) -> string (*cg expr*) -> unit; |
24219 | 25 |
end; |
26 |
||
27 |
structure CodePackage : CODE_PACKAGE = |
|
28 |
struct |
|
29 |
||
24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24835
diff
changeset
|
30 |
(** code theorems **) |
24219 | 31 |
|
24283 | 32 |
fun code_depgr thy [] = CodeFuncgr.make thy [] |
24219 | 33 |
| code_depgr thy consts = |
34 |
let |
|
24283 | 35 |
val gr = CodeFuncgr.make thy consts; |
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24381
diff
changeset
|
36 |
val select = Graph.all_succs gr consts; |
24219 | 37 |
in |
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24381
diff
changeset
|
38 |
gr |
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24381
diff
changeset
|
39 |
|> Graph.subgraph (member (op =) select) |
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25485
diff
changeset
|
40 |
|> Graph.map_nodes ((apsnd o map) (AxClass.overload thy)) |
24219 | 41 |
end; |
42 |
||
43 |
fun code_thms thy = |
|
44 |
Pretty.writeln o CodeFuncgr.pretty thy o code_depgr thy; |
|
45 |
||
46 |
fun code_deps thy consts = |
|
47 |
let |
|
48 |
val gr = code_depgr thy consts; |
|
49 |
fun mk_entry (const, (_, (_, parents))) = |
|
50 |
let |
|
51 |
val name = CodeUnit.string_of_const thy const; |
|
52 |
val nameparents = map (CodeUnit.string_of_const thy) parents; |
|
53 |
in { name = name, ID = name, dir = "", unfold = true, |
|
54 |
path = "", parents = nameparents } |
|
55 |
end; |
|
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24381
diff
changeset
|
56 |
val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr []; |
24219 | 57 |
in Present.display_graph prgr end; |
58 |
||
24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24835
diff
changeset
|
59 |
|
24918 | 60 |
(** code generation interfaces **) |
61 |
||
62 |
(* code data *) |
|
24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24835
diff
changeset
|
63 |
|
24219 | 64 |
structure Program = CodeDataFun |
65 |
( |
|
66 |
type T = CodeThingol.code; |
|
67 |
val empty = CodeThingol.empty_code; |
|
68 |
fun merge _ = CodeThingol.merge_code; |
|
69 |
fun purge _ NONE _ = CodeThingol.empty_code |
|
70 |
| purge NONE _ _ = CodeThingol.empty_code |
|
71 |
| purge (SOME thy) (SOME cs) code = |
|
72 |
let |
|
73 |
val cs_exisiting = |
|
74 |
map_filter (CodeName.const_rev thy) (Graph.keys code); |
|
75 |
val dels = (Graph.all_preds code |
|
76 |
o map (CodeName.const thy) |
|
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24381
diff
changeset
|
77 |
o filter (member (op =) cs_exisiting) |
24219 | 78 |
) cs; |
79 |
in Graph.del_nodes dels code end; |
|
80 |
); |
|
81 |
||
24918 | 82 |
(* generic generation combinators *) |
24811 | 83 |
|
24918 | 84 |
val ensure_const = CodeThingol.ensure_const; |
24219 | 85 |
|
24918 | 86 |
fun perhaps_const thy algbr funcgr c trns = |
87 |
case try (CodeThingol.ensure_const thy algbr funcgr c) trns |
|
24219 | 88 |
of SOME (c, trns) => (SOME c, trns) |
89 |
| NONE => (NONE, trns); |
|
90 |
||
25969 | 91 |
fun generate thy funcgr f x = |
92 |
Program.change_yield thy (CodeThingol.transact thy funcgr |
|
93 |
(fn thy => fn funcgr => fn algbr => f thy funcgr algbr x)); |
|
24219 | 94 |
|
26113 | 95 |
(* export_code functionality *) |
96 |
||
24436 | 97 |
fun code thy permissive cs seris = |
98 |
let |
|
99 |
val code = Program.get thy; |
|
100 |
val seris' = map (fn (((target, module), file), args) => |
|
24918 | 101 |
CodeTarget.get_serializer thy target permissive module file args cs) seris; |
24436 | 102 |
in (map (fn f => f code) seris' : unit list; ()) end; |
103 |
||
26113 | 104 |
(* evaluation machinery *) |
105 |
||
26011 | 106 |
fun evaluate eval_kind term_of thy eval = eval_kind thy (fn funcgr => fn ct => |
24250 | 107 |
let |
26011 | 108 |
val ((code, (vs_ty_t, deps)), _) = generate thy funcgr |
109 |
CodeThingol.ensure_value (term_of ct) |
|
110 |
in eval code vs_ty_t deps ct end); |
|
111 |
||
112 |
fun evaluate_conv thy = evaluate CodeFuncgr.eval_conv Thm.term_of thy; |
|
113 |
fun evaluate_term thy = evaluate CodeFuncgr.eval_term I thy; |
|
114 |
||
115 |
fun eval_ml reff args thy code ((vs, ty), t) deps _ = |
|
116 |
CodeTarget.eval thy reff code (t, ty) args; |
|
24219 | 117 |
|
26011 | 118 |
fun eval evaluate term_of reff thy ct args = |
119 |
let |
|
120 |
val _ = if null (term_frees (term_of ct)) then () else error ("Term " |
|
121 |
^ quote (Sign.string_of_term thy (term_of ct)) |
|
122 |
^ " to be evaluated containts free variables"); |
|
123 |
in evaluate thy (eval_ml reff args thy) ct end; |
|
124 |
||
125 |
fun eval_conv reff = eval evaluate_conv Thm.term_of reff; |
|
126 |
fun eval_term reff = eval evaluate_term I reff; |
|
24219 | 127 |
|
24585 | 128 |
val satisfies_ref : (unit -> bool) option ref = ref NONE; |
24219 | 129 |
|
26011 | 130 |
val satisfies = eval_term ("CodePackage.satisfies_ref", satisfies_ref); |
24219 | 131 |
|
26113 | 132 |
(* code antiquotation *) |
133 |
||
134 |
fun code_antiq (ctxt, args) = |
|
135 |
let |
|
136 |
val thy = Context.theory_of ctxt; |
|
137 |
val (ts, (ctxt', args')) = Scan.repeat1 Args.term (ctxt, args); |
|
138 |
val cs = map (CodeUnit.check_const thy) ts; |
|
139 |
val (cs', code') = generate thy (CodeFuncgr.make thy cs) |
|
140 |
(fold_map ooo ensure_const) cs; |
|
141 |
val code'' = CodeTarget.sml_of thy cs' code' ^ " ()"; |
|
142 |
in (("codevals", code''), (ctxt', args')) end; |
|
143 |
||
144 |
||
145 |
(* const expressions *) |
|
146 |
||
26615
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
147 |
local |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
148 |
|
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
149 |
fun consts_of thy some_thyname = |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
150 |
let |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
151 |
val this_thy = Option.map ThyInfo.get_theory some_thyname |> the_default thy; |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
152 |
val raw_cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I) |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
153 |
((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) []; |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
154 |
val cs = map (CodeUnit.subst_alias thy) raw_cs; |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
155 |
fun belongs_here thyname c = |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
156 |
not (exists (fn thy' => Sign.declared_const thy' c) (Theory.parents_of this_thy)) |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
157 |
in case some_thyname |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
158 |
of NONE => cs |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
159 |
| SOME thyname => filter (belongs_here thyname) cs |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
160 |
end; |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
161 |
|
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
162 |
fun read_const_expr thy "*" = ([], consts_of thy NONE) |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
163 |
| read_const_expr thy s = if String.isSuffix ".*" s |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
164 |
then ([], consts_of thy (SOME (unsuffix ".*" s))) |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
165 |
else ([CodeUnit.read_const thy s], []); |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
166 |
|
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
167 |
in |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
168 |
|
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
169 |
fun read_const_exprs thy select exprs = |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
170 |
case (pairself flat o split_list o map (read_const_expr thy)) exprs |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
171 |
of (consts, []) => (false, consts) |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
172 |
| (consts, consts') => (true, consts @ select consts'); |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
173 |
|
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
174 |
end; (*local*) |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
175 |
|
24219 | 176 |
fun filter_generatable thy consts = |
177 |
let |
|
24283 | 178 |
val (consts', funcgr) = CodeFuncgr.make_consts thy consts; |
24918 | 179 |
val (consts'', _) = generate thy funcgr (fold_map ooo perhaps_const) consts'; |
24219 | 180 |
val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE) |
181 |
(consts' ~~ consts''); |
|
182 |
in consts''' end; |
|
183 |
||
24436 | 184 |
fun generate_const_exprs thy raw_cs = |
185 |
let |
|
26615
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
186 |
val (perm1, cs) = read_const_exprs thy |
24436 | 187 |
(filter_generatable thy) raw_cs; |
188 |
val (perm2, cs') = case generate thy (CodeFuncgr.make thy cs) |
|
24918 | 189 |
(fold_map ooo ensure_const) cs |
190 |
of ([], _) => (true, NONE) |
|
191 |
| (cs, _) => (false, SOME cs); |
|
24436 | 192 |
in (perm1 orelse perm2, cs') end; |
193 |
||
194 |
||
195 |
(** code properties **) |
|
196 |
||
197 |
fun mk_codeprops thy all_cs sel_cs = |
|
198 |
let |
|
24976
821628d16552
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
wenzelm
parents:
24971
diff
changeset
|
199 |
fun select (thmref, thm) = case try (Thm.unvarify o Drule.zero_var_indexes) thm |
24436 | 200 |
of NONE => NONE |
201 |
| SOME thm => let |
|
202 |
val t = (ObjectLogic.drop_judgment thy o Thm.prop_of) thm; |
|
203 |
val cs = fold_aterms (fn Const (c, ty) => |
|
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25485
diff
changeset
|
204 |
cons (AxClass.unoverload_const thy (c, ty)) | _ => I) t []; |
24436 | 205 |
in if exists (member (op =) sel_cs) cs |
206 |
andalso forall (member (op =) all_cs) cs |
|
207 |
then SOME (thmref, thm) else NONE end; |
|
208 |
fun mk_codeprop (thmref, thm) = |
|
209 |
let |
|
210 |
val t = ObjectLogic.drop_judgment thy (Thm.prop_of thm); |
|
211 |
val ty_judg = fastype_of t; |
|
212 |
val tfrees1 = fold_aterms (fn Const (c, ty) => |
|
213 |
Term.add_tfreesT ty | _ => I) t []; |
|
214 |
val vars = Term.add_frees t []; |
|
215 |
val tfrees2 = fold (Term.add_tfreesT o snd) vars []; |
|
216 |
val tfrees' = subtract (op =) tfrees2 tfrees1 |> map TFree; |
|
217 |
val ty = map Term.itselfT tfrees' @ map snd vars ---> ty_judg; |
|
218 |
val tfree_vars = map Logic.mk_type tfrees'; |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26285
diff
changeset
|
219 |
val c = Facts.string_of_ref thmref |
24436 | 220 |
|> NameSpace.explode |
221 |
|> (fn [x] => [x] | (x::xs) => xs) |
|
222 |
|> space_implode "_" |
|
223 |
val propdef = (((c, ty), tfree_vars @ map Free vars), t); |
|
224 |
in if c = "" then NONE else SOME (thmref, propdef) end; |
|
225 |
in |
|
26285 | 226 |
Facts.dest (PureThy.all_facts_of thy) |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26285
diff
changeset
|
227 |
|> maps Facts.selections |
24436 | 228 |
|> map_filter select |
229 |
|> map_filter mk_codeprop |
|
230 |
end; |
|
231 |
||
232 |
fun add_codeprops all_cs sel_cs thy = |
|
233 |
let |
|
234 |
val codeprops = mk_codeprops thy all_cs sel_cs; |
|
235 |
fun lift_name_yield f x = (Name.context, x) |> f ||> snd; |
|
236 |
fun add (thmref, (((raw_c, ty), ts), t)) (names, thy) = |
|
237 |
let |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26285
diff
changeset
|
238 |
val _ = warning ("Adding theorem " ^ quote (Facts.string_of_ref thmref) |
24436 | 239 |
^ " as code property " ^ quote raw_c); |
240 |
val ([raw_c'], names') = Name.variants [raw_c] names; |
|
24971
4d006b03aa4a
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24918
diff
changeset
|
241 |
val (const as Const (c, _), thy') = thy |> Sign.declare_const [] (raw_c', ty, NoSyn); |
4d006b03aa4a
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24918
diff
changeset
|
242 |
val eq = Logic.mk_equals (list_comb (const, ts), t); |
4d006b03aa4a
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24918
diff
changeset
|
243 |
val ([def], thy'') = thy' |> PureThy.add_defs_i false [((Thm.def_name raw_c', eq), [])]; |
4d006b03aa4a
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24918
diff
changeset
|
244 |
in ((c, def), (names', thy'')) end; |
24436 | 245 |
in |
246 |
thy |
|
247 |
|> Sign.sticky_prefix "codeprop" |
|
248 |
|> lift_name_yield (fold_map add codeprops) |
|
249 |
||> Sign.restore_naming thy |
|
24621 | 250 |
|-> (fn c_thms => fold (Code.add_func o snd) c_thms #> pair c_thms) |
24436 | 251 |
end; |
252 |
||
253 |
||
24918 | 254 |
(** interfaces and Isar setup **) |
24219 | 255 |
|
256 |
local |
|
257 |
||
258 |
structure P = OuterParse |
|
259 |
and K = OuterKeyword |
|
260 |
||
24436 | 261 |
fun code_cmd raw_cs seris thy = |
24219 | 262 |
let |
24436 | 263 |
val (permissive, cs) = generate_const_exprs thy raw_cs; |
264 |
val _ = code thy permissive cs seris; |
|
265 |
in () end; |
|
24219 | 266 |
|
267 |
fun code_thms_cmd thy = |
|
26615
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
268 |
code_thms thy o snd o read_const_exprs thy (fst o CodeFuncgr.make_consts thy); |
24219 | 269 |
|
270 |
fun code_deps_cmd thy = |
|
26615
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
271 |
code_deps thy o snd o read_const_exprs thy (fst o CodeFuncgr.make_consts thy); |
24219 | 272 |
|
24436 | 273 |
fun code_props_cmd raw_cs seris thy = |
274 |
let |
|
275 |
val (_, all_cs) = generate_const_exprs thy ["*"]; |
|
276 |
val (permissive, cs) = generate_const_exprs thy raw_cs; |
|
277 |
val (c_thms, thy') = add_codeprops (map (the o CodeName.const_rev thy) (these all_cs)) |
|
278 |
(map (the o CodeName.const_rev thy) (these cs)) thy; |
|
279 |
val prop_cs = (filter_generatable thy' o map fst) c_thms; |
|
24918 | 280 |
val _ = if null seris then () else (generate thy' (CodeFuncgr.make thy' prop_cs) |
281 |
(fold_map ooo ensure_const) prop_cs; ()); |
|
24436 | 282 |
val _ = if null seris then () else code thy' permissive |
283 |
(SOME (map (CodeName.const thy') prop_cs)) seris; |
|
284 |
in thy' end; |
|
285 |
||
24250 | 286 |
val (inK, module_nameK, fileK) = ("in", "module_name", "file"); |
24219 | 287 |
|
24436 | 288 |
fun code_exprP cmd = |
24219 | 289 |
(Scan.repeat P.term |
290 |
-- Scan.repeat (P.$$$ inK |-- P.name |
|
24250 | 291 |
-- Scan.option (P.$$$ module_nameK |-- P.name) |
24219 | 292 |
-- Scan.option (P.$$$ fileK |-- P.name) |
293 |
-- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") [] |
|
24436 | 294 |
) >> (fn (raw_cs, seris) => cmd raw_cs seris)); |
24219 | 295 |
|
24867 | 296 |
val _ = OuterSyntax.keywords [inK, module_nameK, fileK]; |
24219 | 297 |
|
24436 | 298 |
val (codeK, code_thmsK, code_depsK, code_propsK) = |
299 |
("export_code", "code_thms", "code_deps", "code_props"); |
|
24219 | 300 |
|
301 |
in |
|
302 |
||
24867 | 303 |
val _ = |
25110 | 304 |
OuterSyntax.command codeK "generate executable code for constants" |
24436 | 305 |
K.diag (P.!!! (code_exprP code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of))); |
24219 | 306 |
|
26604 | 307 |
fun codegen_shell_command thyname cmd = Toplevel.program (fn _ => |
25611 | 308 |
(use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd) |
309 |
of SOME f => (writeln "Now generating code..."; f (theory thyname)) |
|
310 |
| NONE => error ("Bad directive " ^ quote cmd))) |
|
311 |
handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure; |
|
24219 | 312 |
|
24867 | 313 |
val _ = |
24219 | 314 |
OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag |
315 |
(Scan.repeat P.term |
|
316 |
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory |
|
317 |
o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of))); |
|
318 |
||
24867 | 319 |
val _ = |
24219 | 320 |
OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations for code" OuterKeyword.diag |
321 |
(Scan.repeat P.term |
|
322 |
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory |
|
323 |
o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of))); |
|
324 |
||
24867 | 325 |
val _ = |
24436 | 326 |
OuterSyntax.command code_propsK "generate characteristic properties for executable constants" |
327 |
K.thy_decl (P.!!! (code_exprP code_props_cmd) >> Toplevel.theory); |
|
24219 | 328 |
|
26113 | 329 |
val _ = ML_Context.value_antiq "code" code_antiq; |
330 |
||
24436 | 331 |
end; (*local*) |
332 |
||
333 |
end; (*struct*) |