author | haftmann |
Wed, 28 Nov 2007 09:01:42 +0100 | |
changeset 25485 | 33840a854e63 |
parent 25110 | 7253d331e9fc |
child 25597 | 34860182b250 |
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 |
|
10 |
val eval_conv: theory |
|
24381 | 11 |
-> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm |
12 |
-> string list -> cterm -> thm) |
|
24283 | 13 |
-> cterm -> thm; |
14 |
val eval_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; |
24585 | 18 |
val satisfies_ref: (unit -> bool) option ref; |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24811
diff
changeset
|
19 |
val satisfies: theory -> term -> string list -> bool; |
24219 | 20 |
val codegen_command: theory -> string -> unit; |
21 |
end; |
|
22 |
||
23 |
structure CodePackage : CODE_PACKAGE = |
|
24 |
struct |
|
25 |
||
24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24835
diff
changeset
|
26 |
(** code theorems **) |
24219 | 27 |
|
24283 | 28 |
fun code_depgr thy [] = CodeFuncgr.make thy [] |
24219 | 29 |
| code_depgr thy consts = |
30 |
let |
|
24283 | 31 |
val gr = CodeFuncgr.make thy consts; |
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24381
diff
changeset
|
32 |
val select = Graph.all_succs gr consts; |
24219 | 33 |
in |
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24381
diff
changeset
|
34 |
gr |
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24381
diff
changeset
|
35 |
|> Graph.subgraph (member (op =) select) |
25485 | 36 |
|> Graph.map_nodes ((apsnd o map) (Class.overload thy)) |
24219 | 37 |
end; |
38 |
||
39 |
fun code_thms thy = |
|
40 |
Pretty.writeln o CodeFuncgr.pretty thy o code_depgr thy; |
|
41 |
||
42 |
fun code_deps thy consts = |
|
43 |
let |
|
44 |
val gr = code_depgr thy consts; |
|
45 |
fun mk_entry (const, (_, (_, parents))) = |
|
46 |
let |
|
47 |
val name = CodeUnit.string_of_const thy const; |
|
48 |
val nameparents = map (CodeUnit.string_of_const thy) parents; |
|
49 |
in { name = name, ID = name, dir = "", unfold = true, |
|
50 |
path = "", parents = nameparents } |
|
51 |
end; |
|
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24381
diff
changeset
|
52 |
val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr []; |
24219 | 53 |
in Present.display_graph prgr end; |
54 |
||
24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24835
diff
changeset
|
55 |
|
24918 | 56 |
(** code generation interfaces **) |
57 |
||
58 |
(* code data *) |
|
24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24835
diff
changeset
|
59 |
|
24219 | 60 |
structure Program = CodeDataFun |
61 |
( |
|
62 |
type T = CodeThingol.code; |
|
63 |
val empty = CodeThingol.empty_code; |
|
64 |
fun merge _ = CodeThingol.merge_code; |
|
65 |
fun purge _ NONE _ = CodeThingol.empty_code |
|
66 |
| purge NONE _ _ = CodeThingol.empty_code |
|
67 |
| purge (SOME thy) (SOME cs) code = |
|
68 |
let |
|
69 |
val cs_exisiting = |
|
70 |
map_filter (CodeName.const_rev thy) (Graph.keys code); |
|
71 |
val dels = (Graph.all_preds code |
|
72 |
o map (CodeName.const thy) |
|
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24381
diff
changeset
|
73 |
o filter (member (op =) cs_exisiting) |
24219 | 74 |
) cs; |
75 |
in Graph.del_nodes dels code end; |
|
76 |
); |
|
77 |
||
24918 | 78 |
(* generic generation combinators *) |
24811 | 79 |
|
24918 | 80 |
val ensure_const = CodeThingol.ensure_const; |
24219 | 81 |
|
24918 | 82 |
fun perhaps_const thy algbr funcgr c trns = |
83 |
case try (CodeThingol.ensure_const thy algbr funcgr c) trns |
|
24219 | 84 |
of SOME (c, trns) => (SOME c, trns) |
85 |
| NONE => (NONE, trns); |
|
86 |
||
87 |
fun generate thy funcgr gen it = |
|
88 |
let |
|
89 |
val naming = NameSpace.qualified_names NameSpace.default_naming; |
|
90 |
val consttab = Consts.empty |
|
24770
695a8e087b9f
Sign.add_consts_authentic: tags (Markup.property list);
wenzelm
parents:
24662
diff
changeset
|
91 |
|> fold (fn c => Consts.declare true naming [] (c, CodeFuncgr.typ funcgr c)) |
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24381
diff
changeset
|
92 |
(CodeFuncgr.all funcgr); |
24219 | 93 |
val algbr = (Code.operational_algebra thy, consttab); |
94 |
in |
|
95 |
Program.change_yield thy |
|
24918 | 96 |
(CodeThingol.transact (gen thy algbr funcgr it)) |
24219 | 97 |
end; |
98 |
||
24436 | 99 |
fun code thy permissive cs seris = |
100 |
let |
|
101 |
val code = Program.get thy; |
|
102 |
val seris' = map (fn (((target, module), file), args) => |
|
24918 | 103 |
CodeTarget.get_serializer thy target permissive module file args cs) seris; |
24436 | 104 |
in (map (fn f => f code) seris' : unit list; ()) end; |
105 |
||
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24811
diff
changeset
|
106 |
fun raw_eval evaluate term_of thy g = |
24250 | 107 |
let |
24918 | 108 |
fun result (_, code) = |
24250 | 109 |
let |
24918 | 110 |
val CodeThingol.Fun ((vs, ty), [(([], t), _)]) = |
111 |
Graph.get_node code CodeName.value_name; |
|
112 |
val deps = Graph.imm_succs code CodeName.value_name; |
|
113 |
val code' = Graph.del_nodes [CodeName.value_name] code; |
|
114 |
val code'' = CodeThingol.project_code false [] (SOME deps) code'; |
|
115 |
in ((code'', ((vs, ty), t), deps), code') end; |
|
24283 | 116 |
fun h funcgr ct = |
24219 | 117 |
let |
24918 | 118 |
val ((code, vs_ty_t, deps), _) = term_of ct |
119 |
|> generate thy funcgr CodeThingol.ensure_value |
|
120 |
|> result |
|
121 |
||> `(fn code' => Program.change thy (K code')); |
|
24381 | 122 |
in g code vs_ty_t deps ct end; |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24811
diff
changeset
|
123 |
in evaluate thy h end; |
24219 | 124 |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24811
diff
changeset
|
125 |
fun eval_conv thy = raw_eval CodeFuncgr.eval_conv Thm.term_of thy; |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24811
diff
changeset
|
126 |
fun eval_term thy = raw_eval CodeFuncgr.eval_term I thy; |
24219 | 127 |
|
24585 | 128 |
val satisfies_ref : (unit -> bool) option ref = ref NONE; |
24219 | 129 |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24811
diff
changeset
|
130 |
fun satisfies thy t witnesses = |
24283 | 131 |
let |
24381 | 132 |
fun evl code ((vs, ty), t) deps ct = |
24918 | 133 |
CodeTarget.eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref) |
24662
f79f6061525c
more precise treatment of free dictionary parameters for evaluation
haftmann
parents:
24621
diff
changeset
|
134 |
code (t, ty) witnesses; |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24811
diff
changeset
|
135 |
in eval_term thy evl t end; |
24219 | 136 |
|
137 |
fun filter_generatable thy consts = |
|
138 |
let |
|
24283 | 139 |
val (consts', funcgr) = CodeFuncgr.make_consts thy consts; |
24918 | 140 |
val (consts'', _) = generate thy funcgr (fold_map ooo perhaps_const) consts'; |
24219 | 141 |
val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE) |
142 |
(consts' ~~ consts''); |
|
143 |
in consts''' end; |
|
144 |
||
24436 | 145 |
fun generate_const_exprs thy raw_cs = |
146 |
let |
|
147 |
val (perm1, cs) = CodeUnit.read_const_exprs thy |
|
148 |
(filter_generatable thy) raw_cs; |
|
149 |
val (perm2, cs') = case generate thy (CodeFuncgr.make thy cs) |
|
24918 | 150 |
(fold_map ooo ensure_const) cs |
151 |
of ([], _) => (true, NONE) |
|
152 |
| (cs, _) => (false, SOME cs); |
|
24436 | 153 |
in (perm1 orelse perm2, cs') end; |
154 |
||
155 |
||
156 |
(** code properties **) |
|
157 |
||
158 |
fun mk_codeprops thy all_cs sel_cs = |
|
159 |
let |
|
24976
821628d16552
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
wenzelm
parents:
24971
diff
changeset
|
160 |
fun select (thmref, thm) = case try (Thm.unvarify o Drule.zero_var_indexes) thm |
24436 | 161 |
of NONE => NONE |
162 |
| SOME thm => let |
|
163 |
val t = (ObjectLogic.drop_judgment thy o Thm.prop_of) thm; |
|
164 |
val cs = fold_aterms (fn Const (c, ty) => |
|
165 |
cons (Class.unoverload_const thy (c, ty)) | _ => I) t []; |
|
166 |
in if exists (member (op =) sel_cs) cs |
|
167 |
andalso forall (member (op =) all_cs) cs |
|
168 |
then SOME (thmref, thm) else NONE end; |
|
169 |
fun mk_codeprop (thmref, thm) = |
|
170 |
let |
|
171 |
val t = ObjectLogic.drop_judgment thy (Thm.prop_of thm); |
|
172 |
val ty_judg = fastype_of t; |
|
173 |
val tfrees1 = fold_aterms (fn Const (c, ty) => |
|
174 |
Term.add_tfreesT ty | _ => I) t []; |
|
175 |
val vars = Term.add_frees t []; |
|
176 |
val tfrees2 = fold (Term.add_tfreesT o snd) vars []; |
|
177 |
val tfrees' = subtract (op =) tfrees2 tfrees1 |> map TFree; |
|
178 |
val ty = map Term.itselfT tfrees' @ map snd vars ---> ty_judg; |
|
179 |
val tfree_vars = map Logic.mk_type tfrees'; |
|
180 |
val c = PureThy.string_of_thmref thmref |
|
181 |
|> NameSpace.explode |
|
182 |
|> (fn [x] => [x] | (x::xs) => xs) |
|
183 |
|> space_implode "_" |
|
184 |
val propdef = (((c, ty), tfree_vars @ map Free vars), t); |
|
185 |
in if c = "" then NONE else SOME (thmref, propdef) end; |
|
186 |
in |
|
187 |
PureThy.thms_containing thy ([], []) |
|
188 |
|> maps PureThy.selections |
|
189 |
|> map_filter select |
|
190 |
|> map_filter mk_codeprop |
|
191 |
end; |
|
192 |
||
193 |
fun add_codeprops all_cs sel_cs thy = |
|
194 |
let |
|
195 |
val codeprops = mk_codeprops thy all_cs sel_cs; |
|
196 |
fun lift_name_yield f x = (Name.context, x) |> f ||> snd; |
|
197 |
fun add (thmref, (((raw_c, ty), ts), t)) (names, thy) = |
|
198 |
let |
|
199 |
val _ = warning ("Adding theorem " ^ quote (PureThy.string_of_thmref thmref) |
|
200 |
^ " as code property " ^ quote raw_c); |
|
201 |
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
|
202 |
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
|
203 |
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
|
204 |
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
|
205 |
in ((c, def), (names', thy'')) end; |
24436 | 206 |
in |
207 |
thy |
|
208 |
|> Sign.sticky_prefix "codeprop" |
|
209 |
|> lift_name_yield (fold_map add codeprops) |
|
210 |
||> Sign.restore_naming thy |
|
24621 | 211 |
|-> (fn c_thms => fold (Code.add_func o snd) c_thms #> pair c_thms) |
24436 | 212 |
end; |
213 |
||
214 |
||
24918 | 215 |
(** interfaces and Isar setup **) |
24219 | 216 |
|
217 |
local |
|
218 |
||
219 |
structure P = OuterParse |
|
220 |
and K = OuterKeyword |
|
221 |
||
24436 | 222 |
fun code_cmd raw_cs seris thy = |
24219 | 223 |
let |
24436 | 224 |
val (permissive, cs) = generate_const_exprs thy raw_cs; |
225 |
val _ = code thy permissive cs seris; |
|
226 |
in () end; |
|
24219 | 227 |
|
228 |
fun code_thms_cmd thy = |
|
24283 | 229 |
code_thms thy o snd o CodeUnit.read_const_exprs thy (fst o CodeFuncgr.make_consts thy); |
24219 | 230 |
|
231 |
fun code_deps_cmd thy = |
|
24283 | 232 |
code_deps thy o snd o CodeUnit.read_const_exprs thy (fst o CodeFuncgr.make_consts thy); |
24219 | 233 |
|
24436 | 234 |
fun code_props_cmd raw_cs seris thy = |
235 |
let |
|
236 |
val (_, all_cs) = generate_const_exprs thy ["*"]; |
|
237 |
val (permissive, cs) = generate_const_exprs thy raw_cs; |
|
238 |
val (c_thms, thy') = add_codeprops (map (the o CodeName.const_rev thy) (these all_cs)) |
|
239 |
(map (the o CodeName.const_rev thy) (these cs)) thy; |
|
240 |
val prop_cs = (filter_generatable thy' o map fst) c_thms; |
|
24918 | 241 |
val _ = if null seris then () else (generate thy' (CodeFuncgr.make thy' prop_cs) |
242 |
(fold_map ooo ensure_const) prop_cs; ()); |
|
24436 | 243 |
val _ = if null seris then () else code thy' permissive |
244 |
(SOME (map (CodeName.const thy') prop_cs)) seris; |
|
245 |
in thy' end; |
|
246 |
||
24250 | 247 |
val (inK, module_nameK, fileK) = ("in", "module_name", "file"); |
24219 | 248 |
|
24436 | 249 |
fun code_exprP cmd = |
24219 | 250 |
(Scan.repeat P.term |
251 |
-- Scan.repeat (P.$$$ inK |-- P.name |
|
24250 | 252 |
-- Scan.option (P.$$$ module_nameK |-- P.name) |
24219 | 253 |
-- Scan.option (P.$$$ fileK |-- P.name) |
254 |
-- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") [] |
|
24436 | 255 |
) >> (fn (raw_cs, seris) => cmd raw_cs seris)); |
24219 | 256 |
|
24867 | 257 |
val _ = OuterSyntax.keywords [inK, module_nameK, fileK]; |
24219 | 258 |
|
24436 | 259 |
val (codeK, code_thmsK, code_depsK, code_propsK) = |
260 |
("export_code", "code_thms", "code_deps", "code_props"); |
|
24219 | 261 |
|
262 |
in |
|
263 |
||
24867 | 264 |
val _ = |
25110 | 265 |
OuterSyntax.command codeK "generate executable code for constants" |
24436 | 266 |
K.diag (P.!!! (code_exprP code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of))); |
24219 | 267 |
|
268 |
fun codegen_command thy cmd = |
|
24436 | 269 |
case Scan.read OuterLex.stopper (P.!!! (code_exprP code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd) |
24219 | 270 |
of SOME f => (writeln "Now generating code..."; f thy) |
271 |
| NONE => error ("Bad directive " ^ quote cmd); |
|
272 |
||
24867 | 273 |
val _ = |
24219 | 274 |
OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag |
275 |
(Scan.repeat P.term |
|
276 |
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory |
|
277 |
o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of))); |
|
278 |
||
24867 | 279 |
val _ = |
24219 | 280 |
OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations for code" OuterKeyword.diag |
281 |
(Scan.repeat P.term |
|
282 |
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory |
|
283 |
o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of))); |
|
284 |
||
24867 | 285 |
val _ = |
24436 | 286 |
OuterSyntax.command code_propsK "generate characteristic properties for executable constants" |
287 |
K.thy_decl (P.!!! (code_exprP code_props_cmd) >> Toplevel.theory); |
|
24219 | 288 |
|
24436 | 289 |
end; (*local*) |
290 |
||
291 |
end; (*struct*) |