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
|
19962
|
10 |
val norm_term: theory -> term -> term
|
|
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 |
|
19968
|
19 |
|
|
20 |
(* theory data setup *)
|
|
21 |
|
19147
|
22 |
structure NBE_Data = TheoryDataFun
|
|
23 |
(struct
|
19962
|
24 |
val name = "Pure/NBE"
|
|
25 |
type T = NBE_Eval.Univ Symtab.table
|
|
26 |
val empty = Symtab.empty
|
|
27 |
val copy = I
|
|
28 |
val extend = I
|
|
29 |
fun merge _ = Symtab.merge (K true)
|
|
30 |
fun print _ _ = ()
|
19147
|
31 |
end);
|
|
32 |
|
19968
|
33 |
val _ = Context.add_setup NBE_Data.init;
|
19795
|
34 |
|
|
35 |
|
19968
|
36 |
(* sandbox communication *)
|
19147
|
37 |
|
19177
|
38 |
val tab : NBE_Eval.Univ Symtab.table ref = ref Symtab.empty;
|
|
39 |
fun lookup s = (the o Symtab.lookup (!tab)) s;
|
|
40 |
fun update sx = (tab := Symtab.update sx (!tab));
|
|
41 |
fun defined s = Symtab.defined (!tab) s;
|
|
42 |
|
19147
|
43 |
|
19968
|
44 |
(* FIXME replace by Term.map_aterms *)
|
19795
|
45 |
fun subst_Frees [] tm = tm
|
|
46 |
| subst_Frees inst tm =
|
|
47 |
let
|
|
48 |
fun subst (t as Free(s, _)) = the_default t (AList.lookup (op =) inst s)
|
|
49 |
| subst (Abs (a, T, t)) = Abs (a, T, subst t)
|
|
50 |
| subst (t $ u) = subst t $ subst u
|
|
51 |
| subst t = t;
|
|
52 |
in subst tm end;
|
|
53 |
|
|
54 |
fun var_tab t = (Term.add_frees t [], Term.add_vars t []);
|
|
55 |
|
19968
|
56 |
fun anno_vars (Ftab, Vtab) =
|
|
57 |
subst_Vars (map (fn (ixn, T) => (ixn, Var(ixn,T))) Vtab) o
|
|
58 |
subst_Frees (map (fn (s, T) => (s, Free(s,T))) Ftab)
|
|
59 |
|
|
60 |
|
|
61 |
(* debugging *)
|
|
62 |
|
|
63 |
val trace_nbe = ref false;
|
|
64 |
|
|
65 |
fun trace f = if !trace_nbe then tracing (f ()) else ();
|
|
66 |
|
|
67 |
(* FIXME better turn this into a function
|
|
68 |
NBE_Eval.Univ Symtab.table -> NBE_Eval.Univ Symtab.table
|
|
69 |
with implicit side effect *)
|
|
70 |
fun use_code "" = ()
|
|
71 |
| use_code s =
|
|
72 |
(if !trace_nbe then tracing ("\n---generated code:\n"^ s) else ();
|
|
73 |
use_text(tracing o enclose "\n---compiler echo:\n" "\n---\n",
|
|
74 |
tracing o enclose "\n--- compiler echo (with error!):\n" "\n---\n")
|
|
75 |
(!trace_nbe) s);
|
|
76 |
|
|
77 |
|
|
78 |
(* norm by eval *)
|
19795
|
79 |
|
|
80 |
(* FIXME try to use isar_cmd/print_term to take care of context *)
|
19968
|
81 |
fun norm_print t thy =
|
19150
|
82 |
let
|
19968
|
83 |
val _ = trace (fn () => "Input:\n" ^ Display.raw_string_of_term t);
|
|
84 |
fun compile_term t thy =
|
|
85 |
let
|
|
86 |
val (modl_this, thy') = CodegenPackage.get_root_module thy;
|
|
87 |
val nbe_tab = NBE_Data.get thy';
|
|
88 |
val modl_old = CodegenThingol.project_module (Symtab.keys nbe_tab) modl_this;
|
|
89 |
val (t', thy'') = CodegenPackage.codegen_term t thy';
|
|
90 |
val (modl_new, thy''') = CodegenPackage.get_root_module thy'';
|
|
91 |
val diff = CodegenThingol.diff_module (modl_new, modl_old);
|
|
92 |
val _ = trace (fn () => "new definitions: " ^ (commas o map fst) diff);
|
|
93 |
val _ = (tab := nbe_tab;
|
|
94 |
Library.seq (use_code o NBE_Codegen.generate defined) diff);
|
|
95 |
val thy'''' = NBE_Data.put (!tab) thy''';
|
|
96 |
val nt' = NBE_Eval.nbe (!tab) t';
|
|
97 |
in (nt', thy'''') end;
|
|
98 |
fun eval_term t nt thy =
|
|
99 |
let
|
|
100 |
val vtab = var_tab t;
|
|
101 |
val ty = type_of t;
|
|
102 |
fun restrain ty t = Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy)
|
|
103 |
(K NONE) (K NONE)
|
|
104 |
[] false ([t], ty) |> fst;
|
|
105 |
val _ = trace (fn () => "Normalized:\n" ^ NBE_Eval.string_of_nterm nt);
|
|
106 |
val t' = NBE_Codegen.nterm_to_term thy nt;
|
|
107 |
val _ = trace (fn () =>"Converted back:\n" ^ Display.raw_string_of_term t');
|
|
108 |
val t'' = anno_vars vtab t';
|
|
109 |
val _ = trace (fn () =>"Vars typed:\n" ^ Display.raw_string_of_term t'');
|
|
110 |
val t''' = restrain ty t''
|
|
111 |
val s = Pretty.string_of
|
|
112 |
(Pretty.block [Pretty.quote (Sign.pretty_term thy t'''), Pretty.fbrk,
|
|
113 |
Pretty.str "::", Pretty.brk 1, Pretty.quote (Sign.pretty_typ thy ty)])
|
|
114 |
val _ = writeln s
|
|
115 |
in (t''', thy) end;
|
|
116 |
in
|
|
117 |
thy
|
|
118 |
|> compile_term t
|
|
119 |
|-> (fn nt => eval_term t nt)
|
|
120 |
end;
|
19147
|
121 |
|
19968
|
122 |
fun norm_print' s thy = norm_print (Sign.read_term thy s) thy;
|
|
123 |
|
|
124 |
fun norm_term thy t = fst (norm_print t (Theory.copy thy));
|
19962
|
125 |
|
19177
|
126 |
|
19968
|
127 |
(* Isar setup *)
|
|
128 |
|
|
129 |
local structure P = OuterParse and K = OuterKeyword in
|
19147
|
130 |
|
|
131 |
val nbeP =
|
19830
|
132 |
OuterSyntax.command "normal_form" "normalization by evaluation" K.thy_decl
|
19968
|
133 |
(P.term >> (fn s => Toplevel.theory (snd o norm_print' s)));
|
|
134 |
|
|
135 |
end;
|
19147
|
136 |
|
|
137 |
val _ = OuterSyntax.add_parsers [nbeP];
|
|
138 |
|
19177
|
139 |
end;
|