author | haftmann |
Thu, 06 Apr 2006 16:08:25 +0200 | |
changeset 19341 | 3414c04fbc39 |
parent 19181 | 5c9f58562602 |
child 19795 | 746274ca400b |
permissions | -rw-r--r-- |
19147 | 1 |
(* ID: $Id$ |
2 |
Author: Tobias Nipkow, Florian Haftmann, TU Muenchen |
|
3 |
||
19177 | 4 |
Toplevel theory interface for "normalization by evaluation" |
19147 | 5 |
*) |
6 |
||
19177 | 7 |
signature NBE = |
19147 | 8 |
sig |
19177 | 9 |
val norm_by_eval_i: term -> theory -> term * theory; |
10 |
val lookup: string -> NBE_Eval.Univ; |
|
11 |
val update: string * NBE_Eval.Univ -> unit; |
|
19147 | 12 |
end; |
13 |
||
19177 | 14 |
structure NBE: NBE = |
19147 | 15 |
struct |
16 |
||
17 |
structure NBE_Data = TheoryDataFun |
|
18 |
(struct |
|
19177 | 19 |
val name = "Pure/NBE"; |
20 |
type T = NBE_Eval.Univ Symtab.table; |
|
21 |
val empty = Symtab.empty; |
|
19147 | 22 |
val copy = I; |
23 |
val extend = I; |
|
19177 | 24 |
fun merge _ = Symtab.merge (K true); |
19147 | 25 |
fun print _ _ = (); |
26 |
end); |
|
27 |
||
28 |
val _ = Context.add_setup NBE_Data.init; |
|
29 |
||
19177 | 30 |
val tab : NBE_Eval.Univ Symtab.table ref = ref Symtab.empty; |
31 |
fun lookup s = (the o Symtab.lookup (!tab)) s; |
|
32 |
fun update sx = (tab := Symtab.update sx (!tab)); |
|
33 |
fun defined s = Symtab.defined (!tab) s; |
|
34 |
||
19147 | 35 |
fun use_show s = (writeln ("\n---generated code:\n"^ s); |
36 |
use_text(writeln o enclose "\n---compiler echo:\n" "\n---\n", |
|
37 |
writeln o enclose "\n--- compiler echo (with error!):\n" |
|
38 |
"\n---\n") |
|
39 |
true s); |
|
40 |
||
19177 | 41 |
fun norm_by_eval_i t thy = |
19150 | 42 |
let |
43 |
val nbe_tab = NBE_Data.get thy; |
|
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19181
diff
changeset
|
44 |
val modl_old = CodegenThingol.project_module (Symtab.keys nbe_tab) |
19150 | 45 |
(CodegenPackage.get_root_module thy); |
19177 | 46 |
val (t', thy') = CodegenPackage.codegen_term t thy; |
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
47 |
val modl_new = CodegenPackage.get_root_module thy'; |
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
48 |
val diff = CodegenThingol.diff_module (modl_new, modl_old); |
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
49 |
val _ = writeln ("new definitions: " ^ (commas o map fst) diff); |
19150 | 50 |
val _ = (tab := nbe_tab; |
19177 | 51 |
Library.seq (use_show o NBE_Codegen.generate defined) diff); |
52 |
val thy'' = NBE_Data.put (!tab) thy'; |
|
53 |
val nt' = NBE_Eval.nbe (!tab) t'; |
|
19181 | 54 |
val _ = print nt'; |
19177 | 55 |
val t' = NBE_Codegen.nterm_to_term thy'' nt'; |
19181 | 56 |
(* |
57 |
val _ = print t'; |
|
58 |
val (t'', _) = |
|
59 |
Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy) (K NONE) (K NONE) |
|
60 |
[] true ([t'], type_of t); |
|
61 |
*) |
|
19177 | 62 |
val _ = (Pretty.writeln o Sign.pretty_term thy'') t'; |
19150 | 63 |
in |
19177 | 64 |
(t', thy'') |
19150 | 65 |
end; |
19147 | 66 |
|
19177 | 67 |
fun norm_by_eval raw_t thy = norm_by_eval_i (Sign.read_term thy raw_t) thy; |
68 |
||
19147 | 69 |
structure P = OuterParse and K = OuterKeyword; |
70 |
||
71 |
val nbeP = |
|
19177 | 72 |
OuterSyntax.command "norm_by_eval" "normalization by evaluation" K.thy_decl |
73 |
(P.term >> (fn t => Toplevel.theory (snd o norm_by_eval t))); |
|
19147 | 74 |
|
75 |
val _ = OuterSyntax.add_parsers [nbeP]; |
|
76 |
||
19177 | 77 |
end; |