author | nipkow |
Fri, 09 Jun 2006 12:17:58 +0200 | |
changeset 19830 | b81d803dfaa4 |
parent 19795 | 746274ca400b |
child 19962 | 016ba2d907a7 |
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" |
19795 | 5 |
Preconditions: no Vars |
19147 | 6 |
*) |
7 |
||
19177 | 8 |
signature NBE = |
19147 | 9 |
sig |
19177 | 10 |
val norm_by_eval_i: term -> theory -> term * theory; |
11 |
val lookup: string -> NBE_Eval.Univ; |
|
19795 | 12 |
val update: string * NBE_Eval.Univ -> unit |
13 |
val trace_nbe: bool ref |
|
19147 | 14 |
end; |
15 |
||
19177 | 16 |
structure NBE: NBE = |
19147 | 17 |
struct |
18 |
||
19 |
structure NBE_Data = TheoryDataFun |
|
20 |
(struct |
|
19177 | 21 |
val name = "Pure/NBE"; |
22 |
type T = NBE_Eval.Univ Symtab.table; |
|
23 |
val empty = Symtab.empty; |
|
19147 | 24 |
val copy = I; |
25 |
val extend = I; |
|
19177 | 26 |
fun merge _ = Symtab.merge (K true); |
19147 | 27 |
fun print _ _ = (); |
28 |
end); |
|
29 |
||
19795 | 30 |
val trace_nbe = ref false; |
31 |
||
32 |
fun nbe_trace fs = if !trace_nbe then tracing(fs()) else (); |
|
33 |
||
19147 | 34 |
val _ = Context.add_setup NBE_Data.init; |
35 |
||
19177 | 36 |
val tab : NBE_Eval.Univ Symtab.table ref = ref Symtab.empty; |
37 |
fun lookup s = (the o Symtab.lookup (!tab)) s; |
|
38 |
fun update sx = (tab := Symtab.update sx (!tab)); |
|
39 |
fun defined s = Symtab.defined (!tab) s; |
|
40 |
||
19795 | 41 |
fun use_show "" = () |
42 |
| use_show s = |
|
43 |
(if !trace_nbe then tracing ("\n---generated code:\n"^ s) else (); |
|
44 |
use_text(tracing o enclose "\n---compiler echo:\n" "\n---\n", |
|
45 |
tracing o enclose "\n--- compiler echo (with error!):\n" "\n---\n") |
|
46 |
(!trace_nbe) s); |
|
19147 | 47 |
|
19795 | 48 |
(* FIXME move to term.ML *) |
49 |
fun subst_Frees [] tm = tm |
|
50 |
| subst_Frees inst tm = |
|
51 |
let |
|
52 |
fun subst (t as Free(s, _)) = the_default t (AList.lookup (op =) inst s) |
|
53 |
| subst (Abs (a, T, t)) = Abs (a, T, subst t) |
|
54 |
| subst (t $ u) = subst t $ subst u |
|
55 |
| subst t = t; |
|
56 |
in subst tm end; |
|
57 |
||
58 |
fun var_tab t = (Term.add_frees t [], Term.add_vars t []); |
|
59 |
||
60 |
fun anno_vars (Ftab,Vtab) = |
|
61 |
subst_Vars (map (fn (ixn,T) => (ixn, Var(ixn,T))) Vtab) o |
|
62 |
subst_Frees (map (fn (s,T) => (s, Free(s,T))) Ftab) |
|
63 |
||
64 |
(* FIXME try to use isar_cmd/print_term to take care of context *) |
|
19177 | 65 |
fun norm_by_eval_i t thy = |
19150 | 66 |
let |
67 |
val nbe_tab = NBE_Data.get thy; |
|
19341
3414c04fbc39
added definitional code generator module: codegen_theorems.ML
haftmann
parents:
19181
diff
changeset
|
68 |
val modl_old = CodegenThingol.project_module (Symtab.keys nbe_tab) |
19150 | 69 |
(CodegenPackage.get_root_module thy); |
19177 | 70 |
val (t', thy') = CodegenPackage.codegen_term t thy; |
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
71 |
val modl_new = CodegenPackage.get_root_module thy'; |
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
72 |
val diff = CodegenThingol.diff_module (modl_new, modl_old); |
19795 | 73 |
val _ = nbe_trace (fn() => "new definitions: " ^ (commas o map fst) diff); |
19150 | 74 |
val _ = (tab := nbe_tab; |
19177 | 75 |
Library.seq (use_show o NBE_Codegen.generate defined) diff); |
76 |
val thy'' = NBE_Data.put (!tab) thy'; |
|
77 |
val nt' = NBE_Eval.nbe (!tab) t'; |
|
19795 | 78 |
val _ = nbe_trace (fn() => "Input:\n" ^ Display.raw_string_of_term t) |
79 |
val _ = nbe_trace (fn()=> "Normalized:\n" ^ NBE_Eval.string_of_nterm nt'); |
|
19177 | 80 |
val t' = NBE_Codegen.nterm_to_term thy'' nt'; |
19795 | 81 |
val _ = nbe_trace (fn()=>"Converted back:\n" ^ Display.raw_string_of_term t'); |
82 |
val t'' = anno_vars (var_tab t) t'; |
|
83 |
val _ = nbe_trace (fn()=>"Vars typed:\n" ^ Display.raw_string_of_term t''); |
|
84 |
val ty = type_of t; |
|
85 |
val (t''', _) = |
|
19181 | 86 |
Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy) (K NONE) (K NONE) |
19795 | 87 |
[] false ([t''], ty); |
88 |
val s = Pretty.string_of |
|
89 |
(Pretty.block [Pretty.quote (Sign.pretty_term thy'' t'''), Pretty.fbrk, |
|
90 |
Pretty.str "::", Pretty.brk 1, Pretty.quote (Sign.pretty_typ thy'' ty)]) |
|
91 |
val _ = writeln s |
|
92 |
in (t''', thy'') end; |
|
19147 | 93 |
|
19177 | 94 |
fun norm_by_eval raw_t thy = norm_by_eval_i (Sign.read_term thy raw_t) thy; |
95 |
||
19147 | 96 |
structure P = OuterParse and K = OuterKeyword; |
97 |
||
98 |
val nbeP = |
|
19830 | 99 |
OuterSyntax.command "normal_form" "normalization by evaluation" K.thy_decl |
19177 | 100 |
(P.term >> (fn t => Toplevel.theory (snd o norm_by_eval t))); |
19147 | 101 |
|
102 |
val _ = OuterSyntax.add_parsers [nbeP]; |
|
103 |
||
19177 | 104 |
end; |