author | haftmann |
Tue, 22 Apr 2008 22:00:31 +0200 | |
changeset 26740 | 6c8cd101f875 |
parent 26690 | e30b8d500c7d |
child 26939 | 1035c89b4c02 |
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 |
26740 | 11 |
-> (term -> term * (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm |
12 |
-> string list -> thm)) |
|
24283 | 13 |
-> cterm -> thm; |
26011 | 14 |
val evaluate_term: theory |
26740 | 15 |
-> (term -> term * (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm |
16 |
-> string list -> 'a)) |
|
24835
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 |
||
26740 | 106 |
fun evaluate eval_kind thy evaluator = |
24250 | 107 |
let |
26740 | 108 |
fun evaluator'' evaluator''' funcgr t = |
109 |
let |
|
110 |
val ((code, (vs_ty_t, deps)), _) = |
|
111 |
generate thy funcgr CodeThingol.ensure_value t; |
|
112 |
in evaluator''' code vs_ty_t deps end; |
|
113 |
fun evaluator' t = |
|
114 |
let |
|
115 |
val (t', evaluator''') = evaluator t; |
|
116 |
in (t', evaluator'' evaluator''') end; |
|
117 |
in eval_kind thy evaluator' end |
|
26011 | 118 |
|
26740 | 119 |
fun evaluate_conv thy = evaluate CodeFuncgr.eval_conv thy; |
120 |
fun evaluate_term thy = evaluate CodeFuncgr.eval_term thy; |
|
26011 | 121 |
|
26740 | 122 |
fun eval_ml reff args thy code ((vs, ty), t) deps = |
26011 | 123 |
CodeTarget.eval thy reff code (t, ty) args; |
24219 | 124 |
|
26011 | 125 |
fun eval evaluate term_of reff thy ct args = |
126 |
let |
|
127 |
val _ = if null (term_frees (term_of ct)) then () else error ("Term " |
|
128 |
^ quote (Sign.string_of_term thy (term_of ct)) |
|
26740 | 129 |
^ " to be evaluated contains free variables"); |
130 |
in evaluate thy (fn t => (t, eval_ml reff args thy)) ct end; |
|
26011 | 131 |
|
132 |
fun eval_conv reff = eval evaluate_conv Thm.term_of reff; |
|
133 |
fun eval_term reff = eval evaluate_term I reff; |
|
24219 | 134 |
|
24585 | 135 |
val satisfies_ref : (unit -> bool) option ref = ref NONE; |
24219 | 136 |
|
26011 | 137 |
val satisfies = eval_term ("CodePackage.satisfies_ref", satisfies_ref); |
24219 | 138 |
|
26113 | 139 |
(* code antiquotation *) |
140 |
||
141 |
fun code_antiq (ctxt, args) = |
|
142 |
let |
|
143 |
val thy = Context.theory_of ctxt; |
|
144 |
val (ts, (ctxt', args')) = Scan.repeat1 Args.term (ctxt, args); |
|
145 |
val cs = map (CodeUnit.check_const thy) ts; |
|
146 |
val (cs', code') = generate thy (CodeFuncgr.make thy cs) |
|
147 |
(fold_map ooo ensure_const) cs; |
|
148 |
val code'' = CodeTarget.sml_of thy cs' code' ^ " ()"; |
|
149 |
in (("codevals", code''), (ctxt', args')) end; |
|
150 |
||
151 |
||
152 |
(* const expressions *) |
|
153 |
||
26615
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
154 |
local |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
155 |
|
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
156 |
fun consts_of thy some_thyname = |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
157 |
let |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
158 |
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
|
159 |
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
|
160 |
((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
|
161 |
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
|
162 |
fun belongs_here thyname c = |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
163 |
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
|
164 |
in case some_thyname |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
165 |
of NONE => cs |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
166 |
| SOME thyname => filter (belongs_here thyname) cs |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
167 |
end; |
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_expr thy "*" = ([], consts_of thy NONE) |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
170 |
| 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
|
171 |
then ([], consts_of thy (SOME (unsuffix ".*" s))) |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
172 |
else ([CodeUnit.read_const thy s], []); |
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 |
in |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
175 |
|
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
176 |
fun read_const_exprs thy select exprs = |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
177 |
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
|
178 |
of (consts, []) => (false, consts) |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
179 |
| (consts, consts') => (true, consts @ select consts'); |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
180 |
|
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
181 |
end; (*local*) |
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
182 |
|
24219 | 183 |
fun filter_generatable thy consts = |
184 |
let |
|
24283 | 185 |
val (consts', funcgr) = CodeFuncgr.make_consts thy consts; |
24918 | 186 |
val (consts'', _) = generate thy funcgr (fold_map ooo perhaps_const) consts'; |
24219 | 187 |
val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE) |
188 |
(consts' ~~ consts''); |
|
189 |
in consts''' end; |
|
190 |
||
24436 | 191 |
fun generate_const_exprs thy raw_cs = |
192 |
let |
|
26615
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
193 |
val (perm1, cs) = read_const_exprs thy |
24436 | 194 |
(filter_generatable thy) raw_cs; |
195 |
val (perm2, cs') = case generate thy (CodeFuncgr.make thy cs) |
|
24918 | 196 |
(fold_map ooo ensure_const) cs |
197 |
of ([], _) => (true, NONE) |
|
198 |
| (cs, _) => (false, SOME cs); |
|
24436 | 199 |
in (perm1 orelse perm2, cs') end; |
200 |
||
201 |
||
202 |
(** code properties **) |
|
203 |
||
204 |
fun mk_codeprops thy all_cs sel_cs = |
|
205 |
let |
|
24976
821628d16552
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
wenzelm
parents:
24971
diff
changeset
|
206 |
fun select (thmref, thm) = case try (Thm.unvarify o Drule.zero_var_indexes) thm |
24436 | 207 |
of NONE => NONE |
208 |
| SOME thm => let |
|
209 |
val t = (ObjectLogic.drop_judgment thy o Thm.prop_of) thm; |
|
210 |
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
|
211 |
cons (AxClass.unoverload_const thy (c, ty)) | _ => I) t []; |
24436 | 212 |
in if exists (member (op =) sel_cs) cs |
213 |
andalso forall (member (op =) all_cs) cs |
|
214 |
then SOME (thmref, thm) else NONE end; |
|
215 |
fun mk_codeprop (thmref, thm) = |
|
216 |
let |
|
217 |
val t = ObjectLogic.drop_judgment thy (Thm.prop_of thm); |
|
218 |
val ty_judg = fastype_of t; |
|
219 |
val tfrees1 = fold_aterms (fn Const (c, ty) => |
|
220 |
Term.add_tfreesT ty | _ => I) t []; |
|
221 |
val vars = Term.add_frees t []; |
|
222 |
val tfrees2 = fold (Term.add_tfreesT o snd) vars []; |
|
223 |
val tfrees' = subtract (op =) tfrees2 tfrees1 |> map TFree; |
|
224 |
val ty = map Term.itselfT tfrees' @ map snd vars ---> ty_judg; |
|
225 |
val tfree_vars = map Logic.mk_type tfrees'; |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26285
diff
changeset
|
226 |
val c = Facts.string_of_ref thmref |
24436 | 227 |
|> NameSpace.explode |
228 |
|> (fn [x] => [x] | (x::xs) => xs) |
|
229 |
|> space_implode "_" |
|
230 |
val propdef = (((c, ty), tfree_vars @ map Free vars), t); |
|
231 |
in if c = "" then NONE else SOME (thmref, propdef) end; |
|
232 |
in |
|
26690 | 233 |
Facts.dest_static (PureThy.facts_of thy) |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26285
diff
changeset
|
234 |
|> maps Facts.selections |
24436 | 235 |
|> map_filter select |
236 |
|> map_filter mk_codeprop |
|
237 |
end; |
|
238 |
||
239 |
fun add_codeprops all_cs sel_cs thy = |
|
240 |
let |
|
241 |
val codeprops = mk_codeprops thy all_cs sel_cs; |
|
242 |
fun lift_name_yield f x = (Name.context, x) |> f ||> snd; |
|
243 |
fun add (thmref, (((raw_c, ty), ts), t)) (names, thy) = |
|
244 |
let |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
26285
diff
changeset
|
245 |
val _ = warning ("Adding theorem " ^ quote (Facts.string_of_ref thmref) |
24436 | 246 |
^ " as code property " ^ quote raw_c); |
247 |
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
|
248 |
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
|
249 |
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
|
250 |
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
|
251 |
in ((c, def), (names', thy'')) end; |
24436 | 252 |
in |
253 |
thy |
|
254 |
|> Sign.sticky_prefix "codeprop" |
|
255 |
|> lift_name_yield (fold_map add codeprops) |
|
256 |
||> Sign.restore_naming thy |
|
24621 | 257 |
|-> (fn c_thms => fold (Code.add_func o snd) c_thms #> pair c_thms) |
24436 | 258 |
end; |
259 |
||
260 |
||
24918 | 261 |
(** interfaces and Isar setup **) |
24219 | 262 |
|
263 |
local |
|
264 |
||
265 |
structure P = OuterParse |
|
266 |
and K = OuterKeyword |
|
267 |
||
24436 | 268 |
fun code_cmd raw_cs seris thy = |
24219 | 269 |
let |
24436 | 270 |
val (permissive, cs) = generate_const_exprs thy raw_cs; |
271 |
val _ = code thy permissive cs seris; |
|
272 |
in () end; |
|
24219 | 273 |
|
274 |
fun code_thms_cmd thy = |
|
26615
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
275 |
code_thms thy o snd o read_const_exprs thy (fst o CodeFuncgr.make_consts thy); |
24219 | 276 |
|
277 |
fun code_deps_cmd thy = |
|
26615
8a9d3eebd534
added read_const_exprs (from Pure/Isar/code_unit.ML);
wenzelm
parents:
26604
diff
changeset
|
278 |
code_deps thy o snd o read_const_exprs thy (fst o CodeFuncgr.make_consts thy); |
24219 | 279 |
|
24436 | 280 |
fun code_props_cmd raw_cs seris thy = |
281 |
let |
|
282 |
val (_, all_cs) = generate_const_exprs thy ["*"]; |
|
283 |
val (permissive, cs) = generate_const_exprs thy raw_cs; |
|
284 |
val (c_thms, thy') = add_codeprops (map (the o CodeName.const_rev thy) (these all_cs)) |
|
285 |
(map (the o CodeName.const_rev thy) (these cs)) thy; |
|
286 |
val prop_cs = (filter_generatable thy' o map fst) c_thms; |
|
24918 | 287 |
val _ = if null seris then () else (generate thy' (CodeFuncgr.make thy' prop_cs) |
288 |
(fold_map ooo ensure_const) prop_cs; ()); |
|
24436 | 289 |
val _ = if null seris then () else code thy' permissive |
290 |
(SOME (map (CodeName.const thy') prop_cs)) seris; |
|
291 |
in thy' end; |
|
292 |
||
24250 | 293 |
val (inK, module_nameK, fileK) = ("in", "module_name", "file"); |
24219 | 294 |
|
24436 | 295 |
fun code_exprP cmd = |
24219 | 296 |
(Scan.repeat P.term |
297 |
-- Scan.repeat (P.$$$ inK |-- P.name |
|
24250 | 298 |
-- Scan.option (P.$$$ module_nameK |-- P.name) |
24219 | 299 |
-- Scan.option (P.$$$ fileK |-- P.name) |
300 |
-- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") [] |
|
24436 | 301 |
) >> (fn (raw_cs, seris) => cmd raw_cs seris)); |
24219 | 302 |
|
24867 | 303 |
val _ = OuterSyntax.keywords [inK, module_nameK, fileK]; |
24219 | 304 |
|
24436 | 305 |
val (codeK, code_thmsK, code_depsK, code_propsK) = |
306 |
("export_code", "code_thms", "code_deps", "code_props"); |
|
24219 | 307 |
|
308 |
in |
|
309 |
||
24867 | 310 |
val _ = |
25110 | 311 |
OuterSyntax.command codeK "generate executable code for constants" |
24436 | 312 |
K.diag (P.!!! (code_exprP code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of))); |
24219 | 313 |
|
26604 | 314 |
fun codegen_shell_command thyname cmd = Toplevel.program (fn _ => |
25611 | 315 |
(use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd) |
316 |
of SOME f => (writeln "Now generating code..."; f (theory thyname)) |
|
317 |
| NONE => error ("Bad directive " ^ quote cmd))) |
|
318 |
handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure; |
|
24219 | 319 |
|
24867 | 320 |
val _ = |
24219 | 321 |
OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag |
322 |
(Scan.repeat P.term |
|
323 |
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory |
|
324 |
o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of))); |
|
325 |
||
24867 | 326 |
val _ = |
24219 | 327 |
OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations for code" OuterKeyword.diag |
328 |
(Scan.repeat P.term |
|
329 |
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory |
|
330 |
o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of))); |
|
331 |
||
24867 | 332 |
val _ = |
24436 | 333 |
OuterSyntax.command code_propsK "generate characteristic properties for executable constants" |
334 |
K.thy_decl (P.!!! (code_exprP code_props_cmd) >> Toplevel.theory); |
|
24219 | 335 |
|
26113 | 336 |
val _ = ML_Context.value_antiq "code" code_antiq; |
337 |
||
24436 | 338 |
end; (*local*) |
339 |
||
340 |
end; (*struct*) |