author | haftmann |
Tue, 29 Jan 2008 10:20:00 +0100 | |
changeset 26011 | d55224947082 |
parent 25969 | d3f8ab2726ed |
child 26113 | ba5909699cc3 |
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 |
|
24436 | 95 |
fun code thy permissive cs seris = |
96 |
let |
|
97 |
val code = Program.get thy; |
|
98 |
val seris' = map (fn (((target, module), file), args) => |
|
24918 | 99 |
CodeTarget.get_serializer thy target permissive module file args cs) seris; |
24436 | 100 |
in (map (fn f => f code) seris' : unit list; ()) end; |
101 |
||
26011 | 102 |
fun evaluate eval_kind term_of thy eval = eval_kind thy (fn funcgr => fn ct => |
24250 | 103 |
let |
26011 | 104 |
val ((code, (vs_ty_t, deps)), _) = generate thy funcgr |
105 |
CodeThingol.ensure_value (term_of ct) |
|
106 |
in eval code vs_ty_t deps ct end); |
|
107 |
||
108 |
fun evaluate_conv thy = evaluate CodeFuncgr.eval_conv Thm.term_of thy; |
|
109 |
fun evaluate_term thy = evaluate CodeFuncgr.eval_term I thy; |
|
110 |
||
111 |
fun eval_ml reff args thy code ((vs, ty), t) deps _ = |
|
112 |
CodeTarget.eval thy reff code (t, ty) args; |
|
24219 | 113 |
|
26011 | 114 |
fun eval evaluate term_of reff thy ct args = |
115 |
let |
|
116 |
val _ = if null (term_frees (term_of ct)) then () else error ("Term " |
|
117 |
^ quote (Sign.string_of_term thy (term_of ct)) |
|
118 |
^ " to be evaluated containts free variables"); |
|
119 |
in evaluate thy (eval_ml reff args thy) ct end; |
|
120 |
||
121 |
fun eval_conv reff = eval evaluate_conv Thm.term_of reff; |
|
122 |
fun eval_term reff = eval evaluate_term I reff; |
|
24219 | 123 |
|
24585 | 124 |
val satisfies_ref : (unit -> bool) option ref = ref NONE; |
24219 | 125 |
|
26011 | 126 |
val satisfies = eval_term ("CodePackage.satisfies_ref", satisfies_ref); |
24219 | 127 |
|
128 |
fun filter_generatable thy consts = |
|
129 |
let |
|
24283 | 130 |
val (consts', funcgr) = CodeFuncgr.make_consts thy consts; |
24918 | 131 |
val (consts'', _) = generate thy funcgr (fold_map ooo perhaps_const) consts'; |
24219 | 132 |
val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE) |
133 |
(consts' ~~ consts''); |
|
134 |
in consts''' end; |
|
135 |
||
24436 | 136 |
fun generate_const_exprs thy raw_cs = |
137 |
let |
|
138 |
val (perm1, cs) = CodeUnit.read_const_exprs thy |
|
139 |
(filter_generatable thy) raw_cs; |
|
140 |
val (perm2, cs') = case generate thy (CodeFuncgr.make thy cs) |
|
24918 | 141 |
(fold_map ooo ensure_const) cs |
142 |
of ([], _) => (true, NONE) |
|
143 |
| (cs, _) => (false, SOME cs); |
|
24436 | 144 |
in (perm1 orelse perm2, cs') end; |
145 |
||
146 |
||
147 |
(** code properties **) |
|
148 |
||
149 |
fun mk_codeprops thy all_cs sel_cs = |
|
150 |
let |
|
24976
821628d16552
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
wenzelm
parents:
24971
diff
changeset
|
151 |
fun select (thmref, thm) = case try (Thm.unvarify o Drule.zero_var_indexes) thm |
24436 | 152 |
of NONE => NONE |
153 |
| SOME thm => let |
|
154 |
val t = (ObjectLogic.drop_judgment thy o Thm.prop_of) thm; |
|
155 |
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
|
156 |
cons (AxClass.unoverload_const thy (c, ty)) | _ => I) t []; |
24436 | 157 |
in if exists (member (op =) sel_cs) cs |
158 |
andalso forall (member (op =) all_cs) cs |
|
159 |
then SOME (thmref, thm) else NONE end; |
|
160 |
fun mk_codeprop (thmref, thm) = |
|
161 |
let |
|
162 |
val t = ObjectLogic.drop_judgment thy (Thm.prop_of thm); |
|
163 |
val ty_judg = fastype_of t; |
|
164 |
val tfrees1 = fold_aterms (fn Const (c, ty) => |
|
165 |
Term.add_tfreesT ty | _ => I) t []; |
|
166 |
val vars = Term.add_frees t []; |
|
167 |
val tfrees2 = fold (Term.add_tfreesT o snd) vars []; |
|
168 |
val tfrees' = subtract (op =) tfrees2 tfrees1 |> map TFree; |
|
169 |
val ty = map Term.itselfT tfrees' @ map snd vars ---> ty_judg; |
|
170 |
val tfree_vars = map Logic.mk_type tfrees'; |
|
171 |
val c = PureThy.string_of_thmref thmref |
|
172 |
|> NameSpace.explode |
|
173 |
|> (fn [x] => [x] | (x::xs) => xs) |
|
174 |
|> space_implode "_" |
|
175 |
val propdef = (((c, ty), tfree_vars @ map Free vars), t); |
|
176 |
in if c = "" then NONE else SOME (thmref, propdef) end; |
|
177 |
in |
|
178 |
PureThy.thms_containing thy ([], []) |
|
179 |
|> maps PureThy.selections |
|
180 |
|> map_filter select |
|
181 |
|> map_filter mk_codeprop |
|
182 |
end; |
|
183 |
||
184 |
fun add_codeprops all_cs sel_cs thy = |
|
185 |
let |
|
186 |
val codeprops = mk_codeprops thy all_cs sel_cs; |
|
187 |
fun lift_name_yield f x = (Name.context, x) |> f ||> snd; |
|
188 |
fun add (thmref, (((raw_c, ty), ts), t)) (names, thy) = |
|
189 |
let |
|
190 |
val _ = warning ("Adding theorem " ^ quote (PureThy.string_of_thmref thmref) |
|
191 |
^ " as code property " ^ quote raw_c); |
|
192 |
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
|
193 |
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
|
194 |
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
|
195 |
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
|
196 |
in ((c, def), (names', thy'')) end; |
24436 | 197 |
in |
198 |
thy |
|
199 |
|> Sign.sticky_prefix "codeprop" |
|
200 |
|> lift_name_yield (fold_map add codeprops) |
|
201 |
||> Sign.restore_naming thy |
|
24621 | 202 |
|-> (fn c_thms => fold (Code.add_func o snd) c_thms #> pair c_thms) |
24436 | 203 |
end; |
204 |
||
205 |
||
24918 | 206 |
(** interfaces and Isar setup **) |
24219 | 207 |
|
208 |
local |
|
209 |
||
210 |
structure P = OuterParse |
|
211 |
and K = OuterKeyword |
|
212 |
||
24436 | 213 |
fun code_cmd raw_cs seris thy = |
24219 | 214 |
let |
24436 | 215 |
val (permissive, cs) = generate_const_exprs thy raw_cs; |
216 |
val _ = code thy permissive cs seris; |
|
217 |
in () end; |
|
24219 | 218 |
|
219 |
fun code_thms_cmd thy = |
|
24283 | 220 |
code_thms thy o snd o CodeUnit.read_const_exprs thy (fst o CodeFuncgr.make_consts thy); |
24219 | 221 |
|
222 |
fun code_deps_cmd thy = |
|
24283 | 223 |
code_deps thy o snd o CodeUnit.read_const_exprs thy (fst o CodeFuncgr.make_consts thy); |
24219 | 224 |
|
24436 | 225 |
fun code_props_cmd raw_cs seris thy = |
226 |
let |
|
227 |
val (_, all_cs) = generate_const_exprs thy ["*"]; |
|
228 |
val (permissive, cs) = generate_const_exprs thy raw_cs; |
|
229 |
val (c_thms, thy') = add_codeprops (map (the o CodeName.const_rev thy) (these all_cs)) |
|
230 |
(map (the o CodeName.const_rev thy) (these cs)) thy; |
|
231 |
val prop_cs = (filter_generatable thy' o map fst) c_thms; |
|
24918 | 232 |
val _ = if null seris then () else (generate thy' (CodeFuncgr.make thy' prop_cs) |
233 |
(fold_map ooo ensure_const) prop_cs; ()); |
|
24436 | 234 |
val _ = if null seris then () else code thy' permissive |
235 |
(SOME (map (CodeName.const thy') prop_cs)) seris; |
|
236 |
in thy' end; |
|
237 |
||
24250 | 238 |
val (inK, module_nameK, fileK) = ("in", "module_name", "file"); |
24219 | 239 |
|
24436 | 240 |
fun code_exprP cmd = |
24219 | 241 |
(Scan.repeat P.term |
242 |
-- Scan.repeat (P.$$$ inK |-- P.name |
|
24250 | 243 |
-- Scan.option (P.$$$ module_nameK |-- P.name) |
24219 | 244 |
-- Scan.option (P.$$$ fileK |-- P.name) |
245 |
-- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") [] |
|
24436 | 246 |
) >> (fn (raw_cs, seris) => cmd raw_cs seris)); |
24219 | 247 |
|
24867 | 248 |
val _ = OuterSyntax.keywords [inK, module_nameK, fileK]; |
24219 | 249 |
|
24436 | 250 |
val (codeK, code_thmsK, code_depsK, code_propsK) = |
251 |
("export_code", "code_thms", "code_deps", "code_props"); |
|
24219 | 252 |
|
253 |
in |
|
254 |
||
24867 | 255 |
val _ = |
25110 | 256 |
OuterSyntax.command codeK "generate executable code for constants" |
24436 | 257 |
K.diag (P.!!! (code_exprP code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of))); |
24219 | 258 |
|
25611 | 259 |
fun codegen_shell_command thyname cmd = Isar.toplevel (fn _ => |
260 |
(use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd) |
|
261 |
of SOME f => (writeln "Now generating code..."; f (theory thyname)) |
|
262 |
| NONE => error ("Bad directive " ^ quote cmd))) |
|
263 |
handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure; |
|
24219 | 264 |
|
24867 | 265 |
val _ = |
24219 | 266 |
OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag |
267 |
(Scan.repeat P.term |
|
268 |
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory |
|
269 |
o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of))); |
|
270 |
||
24867 | 271 |
val _ = |
24219 | 272 |
OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations for code" OuterKeyword.diag |
273 |
(Scan.repeat P.term |
|
274 |
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory |
|
275 |
o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of))); |
|
276 |
||
24867 | 277 |
val _ = |
24436 | 278 |
OuterSyntax.command code_propsK "generate characteristic properties for executable constants" |
279 |
K.thy_decl (P.!!! (code_exprP code_props_cmd) >> Toplevel.theory); |
|
24219 | 280 |
|
24436 | 281 |
end; (*local*) |
282 |
||
283 |
end; (*struct*) |