19116
|
1 |
(* ID: $Id$
|
|
2 |
Author: Klaus Aehlig, Tobias Nipkow
|
|
3 |
*)
|
|
4 |
|
|
5 |
(* Global asssumptions:
|
|
6 |
For each function: there is at least one defining eqns and
|
|
7 |
all defining equations have same number of arguments.
|
|
8 |
|
|
9 |
FIXME
|
|
10 |
fun MLname s = "nbe_" ^ s;
|
|
11 |
val quote = quote;
|
|
12 |
|
|
13 |
FIXME xtab in theory
|
|
14 |
|
|
15 |
FIXME CodegenThingol names! which "error"?
|
|
16 |
*)
|
|
17 |
|
19118
|
18 |
signature NBE_CODEGEN =
|
|
19 |
sig
|
|
20 |
val export: Theory.theory -> string * CodegenThingol.def -> string
|
|
21 |
end
|
|
22 |
|
|
23 |
|
|
24 |
structure NBE_Codegen: NBE_CODEGEN =
|
|
25 |
struct
|
|
26 |
|
19116
|
27 |
val is_constr = NBE_Eval.is_constr;
|
|
28 |
val Eval = "NBE_Eval";
|
|
29 |
val Eval_register= Eval ^ ".register";
|
|
30 |
val Eval_lookup = Eval ^ ".lookup";
|
|
31 |
val Eval_apply = Eval ^ ".apply";
|
|
32 |
val Eval_Constr = Eval ^ ".Constr";
|
|
33 |
val Eval_C = Eval ^ ".C";
|
|
34 |
val Eval_AbsN = Eval ^ ".AbsN";
|
|
35 |
val Eval_Fun = Eval ^ ".Fun";
|
|
36 |
val Eval_BVar = Eval ^ ".BVar";
|
|
37 |
val Eval_new_name = Eval ^ ".new_name";
|
|
38 |
val Eval_to_term = Eval ^ ".to_term";
|
|
39 |
|
|
40 |
fun MLname s = "nbe_" ^ s;
|
|
41 |
fun MLvname s = "v_" ^ MLname s;
|
|
42 |
fun MLparam n = "p_" ^ string_of_int n;
|
|
43 |
fun MLintern s = "i_" ^ MLname s;
|
|
44 |
|
|
45 |
fun MLparams n = map MLparam (1 upto n);
|
|
46 |
|
|
47 |
structure S =
|
|
48 |
struct
|
|
49 |
|
|
50 |
val quote = quote; (* FIXME *)
|
|
51 |
|
|
52 |
fun app e1 e2 = "(" ^ e1 ^ " " ^ e2 ^ ")";
|
|
53 |
fun abs v e = "(fn" ^ v ^ " => " ^ e ^ ")";
|
|
54 |
fun tup es = "(" ^ commas es ^ ")";
|
|
55 |
fun list es = "[" ^ commas es ^ "]";
|
|
56 |
|
|
57 |
fun apps s ss = Library.foldl (uncurry app) (s, ss);
|
|
58 |
fun nbe_apps s ss =
|
|
59 |
Library.foldr (fn (s,e) => app (app Eval_apply e) s) (ss,s);
|
|
60 |
|
|
61 |
fun eqns name ees =
|
|
62 |
let fun eqn (es,e) = name ^ " " ^ space_implode " " es ^ " = " ^ e
|
|
63 |
in "fun " ^ space_implode "\n | " (map eqn ees) ^ ";\n" end;
|
|
64 |
|
|
65 |
|
|
66 |
fun Val v s = "val " ^ v ^ " = " ^ s;
|
|
67 |
fun Let ds e = "let\n" ^ (space_implode "\n" ds) ^ " in " ^ e ^ " end"
|
|
68 |
|
|
69 |
end
|
|
70 |
|
|
71 |
fun mk_nbeFUN(nm,e) =
|
|
72 |
S.app Eval_Fun (S.tup [S.abs(S.list [MLvname nm])e,S.list [],"1",
|
|
73 |
S.abs(S.tup [])(S.Let
|
|
74 |
[S.Val (MLintern "var") (S.app Eval_new_name (S.tup [])),
|
|
75 |
S.Val (MLvname nm) (S.app Eval_BVar (S.tup [(MLintern "var"), S.list []]))]
|
|
76 |
(S.app Eval_AbsN(S.tup[MLintern "var",(S.app Eval_to_term e)])))]);
|
|
77 |
|
|
78 |
fun take_last n xs = rev (Library.take(n, rev xs));
|
|
79 |
fun drop_last n xs = rev (Library.drop(n, rev xs));
|
|
80 |
|
|
81 |
fun selfcall nm ar args =
|
|
82 |
if (ar <= length args) then
|
|
83 |
S.nbe_apps (S.app (MLname nm) (S.list (take_last ar args)))
|
|
84 |
(drop_last ar args)
|
|
85 |
else S.app Eval_Fun (S.tup [MLname nm,S.list args,
|
|
86 |
string_of_int(ar - (length args)),
|
|
87 |
S.abs (S.tup []) (S.app Eval_C
|
|
88 |
(S.quote nm))]);
|
|
89 |
|
|
90 |
|
|
91 |
fun mk_rexpr nm ar =
|
|
92 |
let fun mk args t = case t of
|
|
93 |
CodegenThingol.IConst((s,_),_) =>
|
|
94 |
if s=nm then selfcall nm ar args
|
|
95 |
else if is_constr s then S.app Eval_Constr
|
|
96 |
(S.tup [S.quote s,S.list args ])
|
|
97 |
else S.nbe_apps (MLname s) args
|
|
98 |
| CodegenThingol.IVarE(s,_) => S.nbe_apps (MLvname s) args
|
|
99 |
| CodegenThingol.IApp(e1,e2) => mk (args @ [mk [] e2]) e1
|
|
100 |
| CodegenThingol.IAbs(CodegenThingol.IVarE(nm,_), e) =>
|
|
101 |
S.nbe_apps (mk_nbeFUN(nm, mk [] e)) args
|
|
102 |
| _ => sys_error "NBE mkexpr"
|
|
103 |
in mk [] end;
|
|
104 |
|
|
105 |
val mk_lexpr =
|
|
106 |
let fun mk args t = case t of
|
|
107 |
CodegenThingol.IConst((s,_),_) =>
|
|
108 |
S.app Eval_Constr (S.tup [S.quote s, S.list args])
|
|
109 |
| CodegenThingol.IVarE(s,_) => if args = [] then MLvname s else
|
|
110 |
sys_error "NBE mk_lexpr illegal higher order pattern"
|
|
111 |
| CodegenThingol.IApp(e1,e2) => mk (args @ [mk [] e2]) e1
|
|
112 |
| _ => sys_error "NBE mk_lexpr illegal pattern"
|
|
113 |
in mk [] end;
|
|
114 |
|
|
115 |
fun mk_eqn nm ar (lhs,e) = ([S.list(map mk_lexpr (rev lhs))], mk_rexpr nm ar e);
|
|
116 |
|
|
117 |
fun funs_of_expr(CodegenThingol.IConst((s,_),_),fs) = s::fs
|
|
118 |
| funs_of_expr(CodegenThingol.IApp(e1,e2),fs) =
|
|
119 |
funs_of_expr(e1, funs_of_expr(e2, fs))
|
|
120 |
| funs_of_expr(CodegenThingol.IAbs(_, e),fs) = funs_of_expr(e,fs)
|
|
121 |
| funs_of_expr(_,fs) = fs;
|
|
122 |
|
|
123 |
fun lookup nm =
|
|
124 |
S.Val (MLname nm) (S.app Eval_lookup (S.quote nm));
|
|
125 |
|
|
126 |
fun export thy (nm,CodegenThingol.Fun(eqns,_)) =
|
|
127 |
let
|
|
128 |
val ar = length(fst(hd eqns));
|
|
129 |
val params = S.list (rev (MLparams ar));
|
|
130 |
val funs = Library.flat(map (fn (_,e) => funs_of_expr(e,[])) eqns) \ nm;
|
|
131 |
val globals = map lookup (filter_out is_constr funs);
|
|
132 |
val default_eqn = ([params], S.app Eval_Constr (S.tup[S.quote nm,params]));
|
|
133 |
val code = S.eqns (MLname nm) (map (mk_eqn nm ar) eqns @ [default_eqn])
|
|
134 |
val register = S.app Eval_register
|
|
135 |
(S.tup[S.quote nm, MLname nm, string_of_int ar])
|
|
136 |
in
|
|
137 |
S.Let (globals @ [code]) register
|
|
138 |
end
|
|
139 |
| export _ _ = "\"NBE no op\"";
|
|
140 |
|
19118
|
141 |
end;
|
|
142 |
|
|
143 |
(*
|
|
144 |
|
19116
|
145 |
val use_show = fn s => (writeln ("\n---generated code:\n"^ s);
|
|
146 |
use_text(writeln o enclose "\n---compiler echo:\n" "\n---\n",
|
|
147 |
writeln o enclose "\n--- compiler echo (with error!):\n"
|
|
148 |
"\n---\n")
|
|
149 |
true s);
|
|
150 |
|
|
151 |
val dummyIT = CodegenThingol.IType("DUMMY",[]);
|
|
152 |
|
|
153 |
use_show(export "" ("append",CodegenThingol.Fun(
|
|
154 |
[([CodegenThingol.IConst(("Nil",dummyIT),[]),
|
|
155 |
CodegenThingol.IVarE("ys",dummyIT)],
|
|
156 |
CodegenThingol.IVarE("ys",dummyIT)),
|
|
157 |
([CodegenThingol.IApp(
|
|
158 |
CodegenThingol.IApp(
|
|
159 |
CodegenThingol.IConst(("Cons",dummyIT),[]),
|
|
160 |
CodegenThingol.IVarE("x",dummyIT)),
|
|
161 |
CodegenThingol.IVarE("xs",dummyIT)),
|
|
162 |
CodegenThingol.IVarE("ys",dummyIT)],
|
|
163 |
CodegenThingol.IApp(
|
|
164 |
CodegenThingol.IApp(
|
|
165 |
CodegenThingol.IConst(("Cons",dummyIT),[]),
|
|
166 |
CodegenThingol.IVarE("x",dummyIT)),
|
|
167 |
CodegenThingol.IApp(
|
|
168 |
CodegenThingol.IApp(
|
|
169 |
CodegenThingol.IConst(("append",dummyIT),[]),
|
|
170 |
CodegenThingol.IVarE("xs",dummyIT)),
|
|
171 |
CodegenThingol.IVarE("ys",dummyIT))))]
|
|
172 |
,([],dummyIT))));
|
|
173 |
|
|
174 |
|
|
175 |
let
|
|
176 |
fun test a b = if a=b then () else error "oops!";
|
|
177 |
|
|
178 |
val CNil = Const("Nil",dummyT);
|
|
179 |
val CCons = Const("Cons",dummyT);
|
|
180 |
val Cappend = Const("append",dummyT);
|
|
181 |
val Fx = Free("x",dummyT);
|
|
182 |
val Fy = Free("y",dummyT);
|
|
183 |
val Fxs = Free("xs",dummyT);
|
|
184 |
val Fys = Free("ys",dummyT);
|
|
185 |
open NBE_Eval
|
|
186 |
in
|
|
187 |
test (nbe(CNil)) (C "Nil");
|
|
188 |
test (nbe(CCons)) (C "Cons");
|
|
189 |
test (nbe(Cappend)) (C "append");
|
|
190 |
test (nbe(Cappend $ CNil $ CNil)) (C "Nil");
|
|
191 |
test (nbe(Cappend $ Fxs)) (A (C "append", V "xs"));
|
|
192 |
test (nbe(Cappend $ Fxs $ Fys)) (A (A (C "append", V "xs"), V "ys"));
|
|
193 |
test (nbe(Cappend $ CNil $ Fxs)) (V "xs");
|
|
194 |
test (nbe(Cappend $ (CCons $ Fx $ Fxs) $ Fys))
|
|
195 |
(A (A (C "Cons", V "x"), A (A (C "append", V "xs"), V "ys")));
|
|
196 |
test (nbe(Cappend $ (CCons $ Fx $ Fxs) $ (CCons $ Fy $ Fys)))
|
|
197 |
(A (A (C "Cons", V "x"), A (A (C "append", V "xs"), A (A (C "Cons", V "y"), V "ys"))));
|
|
198 |
test (nbe(Cappend $ (CCons $ Fx $ (CCons $ Fy $ Fxs)) $ (CCons$Fy$Fys)))
|
|
199 |
(A
|
|
200 |
(A (C "Cons", V "x"),
|
|
201 |
A
|
|
202 |
(A (C "Cons", V "y"),
|
|
203 |
A (A (C "append", V "xs"), A (A (C "Cons", V "y"), V "ys")))))
|
|
204 |
|
|
205 |
end;
|
|
206 |
|
|
207 |
|
|
208 |
use_show(export "" ("app",CodegenThingol.Fun(
|
|
209 |
[
|
|
210 |
([CodegenThingol.IConst(("Nil",dummyIT),[])],
|
|
211 |
CodegenThingol.IAbs(CodegenThingol.IVarE("ys",dummyIT),
|
|
212 |
CodegenThingol.IVarE("ys",dummyIT))),
|
|
213 |
|
|
214 |
([CodegenThingol.IApp(
|
|
215 |
CodegenThingol.IApp(
|
|
216 |
CodegenThingol.IConst(("Cons",dummyIT),[]),
|
|
217 |
CodegenThingol.IVarE("x",dummyIT)),
|
|
218 |
CodegenThingol.IVarE("xs",dummyIT))],
|
|
219 |
CodegenThingol.IAbs(CodegenThingol.IVarE("ys",dummyIT),
|
|
220 |
CodegenThingol.IApp(
|
|
221 |
CodegenThingol.IApp(
|
|
222 |
CodegenThingol.IConst(("Cons",dummyIT),[]),
|
|
223 |
CodegenThingol.IVarE("x",dummyIT)),
|
|
224 |
CodegenThingol.IApp(
|
|
225 |
CodegenThingol.IApp(
|
|
226 |
CodegenThingol.IConst(("app",dummyIT),[]),
|
|
227 |
CodegenThingol.IVarE("xs",dummyIT)),
|
|
228 |
CodegenThingol.IVarE("ys",dummyIT)))))]
|
|
229 |
,([],dummyIT))));
|
|
230 |
|
|
231 |
|
|
232 |
let
|
|
233 |
fun test a b = if a=b then () else error "oops!";
|
|
234 |
|
|
235 |
val CNil = Const("Nil",dummyT);
|
|
236 |
val CCons = Const("Cons",dummyT);
|
|
237 |
val Cappend = Const("app",dummyT);
|
|
238 |
val Fx = Free("x",dummyT);
|
|
239 |
val Fy = Free("y",dummyT);
|
|
240 |
val Fxs = Free("xs",dummyT);
|
|
241 |
val Fys = Free("ys",dummyT);
|
|
242 |
open NBE_Eval
|
|
243 |
in
|
|
244 |
test (nbe(CNil)) (C "Nil");
|
|
245 |
test (nbe(CCons)) (C "Cons");
|
|
246 |
test (nbe(Cappend)) (C "app");
|
|
247 |
test (nbe(Cappend $ CNil)) (AbsN (1, B 1));
|
|
248 |
test (nbe(Cappend $ CNil $ CNil)) (C "Nil");
|
|
249 |
test (nbe(Cappend $ Fxs)) (A (C "app", V "xs"));
|
|
250 |
test (nbe(Cappend $ Fxs $ Fys)) (A (A (C "app", V "xs"), V "ys"));
|
|
251 |
test (nbe(Cappend $ CNil $ Fxs)) (V "xs");
|
|
252 |
test (nbe(Cappend $ (CCons $ Fx $ Fxs) $ Fys))
|
|
253 |
(A (A (C "Cons", V "x"), A (A (C "app", V "xs"), V "ys")));
|
|
254 |
test (nbe(Cappend $ (CCons $ Fx $ Fxs)))
|
|
255 |
(AbsN (1, A (A (C "Cons", V "x"), A (A (C "app", V "xs"), B 1))));
|
|
256 |
test (nbe(Cappend $ (CCons $ Fx $ Fxs) $ (CCons $ Fy $ Fys)))
|
|
257 |
(A (A (C "Cons", V "x"), A (A (C "app", V "xs"), A (A (C "Cons", V "y"), V "ys"))));
|
|
258 |
test (nbe(Cappend $ (CCons $ Fx $ (CCons $ Fy $ Fxs)) $ (CCons$Fy$Fys)))
|
|
259 |
(A
|
|
260 |
(A (C "Cons", V "x"),
|
|
261 |
A
|
|
262 |
(A (C "Cons", V "y"),
|
|
263 |
A (A (C "app", V "xs"), A (A (C "Cons", V "y"), V "ys")))));
|
|
264 |
()
|
|
265 |
end;
|
|
266 |
|
|
267 |
|
|
268 |
use_show(export "" ("add",CodegenThingol.Fun(
|
|
269 |
[
|
|
270 |
([CodegenThingol.IConst(("0",dummyIT),[])],
|
|
271 |
CodegenThingol.IAbs(CodegenThingol.IVarE("n",dummyIT),
|
|
272 |
CodegenThingol.IVarE("n",dummyIT))),
|
|
273 |
([CodegenThingol.IApp(
|
|
274 |
CodegenThingol.IConst(("S",dummyIT),[]),
|
|
275 |
CodegenThingol.IVarE("n",dummyIT))],
|
|
276 |
CodegenThingol.IAbs(CodegenThingol.IVarE("m",dummyIT),
|
|
277 |
CodegenThingol.IApp(
|
|
278 |
CodegenThingol.IConst(("S",dummyIT),[]),
|
|
279 |
CodegenThingol.IApp(
|
|
280 |
CodegenThingol.IApp(
|
|
281 |
CodegenThingol.IConst(("add",dummyIT),[]),
|
|
282 |
CodegenThingol.IVarE("n",dummyIT)),
|
|
283 |
CodegenThingol.IVarE("m",dummyIT)))))]
|
|
284 |
,([],dummyIT))));
|
|
285 |
|
|
286 |
|
|
287 |
let
|
|
288 |
fun test a b = if a=b then () else error "oops!";
|
|
289 |
|
|
290 |
val C0 = Const("0",dummyT);
|
|
291 |
val CS = Const("S",dummyT);
|
|
292 |
val Cadd = Const("add",dummyT);
|
|
293 |
val Fx = Free("x",dummyT);
|
|
294 |
val Fy = Free("y",dummyT);
|
|
295 |
open NBE_Eval
|
|
296 |
in
|
|
297 |
test (nbe(Cadd $ C0)) (AbsN (1, B 1));
|
|
298 |
test (nbe(Cadd $ C0 $ C0)) (C "0");
|
|
299 |
test (nbe(Cadd $ (CS $ (CS $ (CS $ Fx))) $ (CS $ (CS $ (CS $ Fy)))))
|
|
300 |
(A (C "S", A (C "S", A (C "S", A (A (C "add", V "x"), A (C "S", A (C "S", A (C "S", V "y")))))))
|
|
301 |
)
|
|
302 |
end;
|
|
303 |
|
|
304 |
|
|
305 |
|
|
306 |
use_show(export "" ("mul",CodegenThingol.Fun(
|
|
307 |
[
|
|
308 |
([CodegenThingol.IConst(("0",dummyIT),[])],
|
|
309 |
CodegenThingol.IAbs(CodegenThingol.IVarE("n",dummyIT),
|
|
310 |
CodegenThingol.IConst(("0",dummyIT),[]))),
|
|
311 |
([CodegenThingol.IApp(
|
|
312 |
CodegenThingol.IConst(("S",dummyIT),[]),
|
|
313 |
CodegenThingol.IVarE("n",dummyIT))],
|
|
314 |
CodegenThingol.IAbs(CodegenThingol.IVarE("m",dummyIT),
|
|
315 |
CodegenThingol.IApp(
|
|
316 |
CodegenThingol.IApp(
|
|
317 |
CodegenThingol.IConst(("add",dummyIT),[]),
|
|
318 |
CodegenThingol.IVarE("m",dummyIT)),
|
|
319 |
CodegenThingol.IApp(
|
|
320 |
CodegenThingol.IApp(
|
|
321 |
CodegenThingol.IConst(("mul",dummyIT),[]),
|
|
322 |
CodegenThingol.IVarE("n",dummyIT)),
|
|
323 |
CodegenThingol.IVarE("m",dummyIT)))))]
|
|
324 |
,([],dummyIT))));
|
|
325 |
|
|
326 |
|
|
327 |
let
|
|
328 |
fun test a b = if a=b then () else error "oops!";
|
|
329 |
|
|
330 |
val C0 = Const("0",dummyT);
|
|
331 |
val CS = Const("S",dummyT);
|
|
332 |
val Cmul = Const("mul",dummyT);
|
|
333 |
val Fx = Free("x",dummyT);
|
|
334 |
val Fy = Free("y",dummyT);
|
|
335 |
open NBE_Eval
|
|
336 |
in
|
|
337 |
test (nbe(Cmul $ C0)) (AbsN (1, C "0"));
|
|
338 |
test (nbe(Cmul $ C0 $ Fx)) (C "0");
|
|
339 |
test (nbe(Cmul $ (CS $ (CS $ (CS $ C0)))))
|
|
340 |
(AbsN (1, A (A (C "add", B 1), A (A (C "add", B 1), A (A (C "add", B 1), C "0")))));
|
|
341 |
test (nbe(Cmul $ (CS $ (CS $ (CS $ Fx)))))
|
|
342 |
(AbsN (1, A (A (C "add", B 1), A (A (C "add", B 1),
|
|
343 |
A (A (C "add", B 1), A (A (C "mul", V "x"), B 1))))));
|
|
344 |
test (nbe(Cmul $ (CS $ (CS $ Fx)) $ (CS $ (CS $ (CS $ Fy)))))
|
|
345 |
(A (C "S", A(C "S",A(C "S",A(A (C "add", V "y"),A(C "S",A(C "S",A(C "S",A
|
|
346 |
(A (C "add", V "y"),A(A (C "mul", V "x"),A(C "S",A(C "S",A(C "S", V"y")))))))))))));
|
|
347 |
()
|
|
348 |
end;
|
19118
|
349 |
*)
|
19116
|
350 |
|
|
351 |
|
|
352 |
(*
|
|
353 |
fun top_eval st thy =
|
|
354 |
let val t = Sign.read_term thy st
|
|
355 |
val tabs = CodegenPackage.mk_tabs thy;
|
|
356 |
val thy') =
|
|
357 |
CodegenPackage.expand_module NONE (CodegenPackage.codegen_term
|
|
358 |
thy tabs [t]) thy
|
|
359 |
val s = map export diff
|
|
360 |
in use s; (* FIXME val thy'' = thy' |> *)
|
|
361 |
Pretty.writeln (Sign.pretty_term thy t');
|
|
362 |
thy'
|
|
363 |
end
|
|
364 |
|
|
365 |
structure P = OuterParse;
|
|
366 |
|
|
367 |
val nbeP =
|
|
368 |
OuterSyntax.command "norm_by_eval" "norm by eval" K.thy_decl
|
|
369 |
(P.term >> (Toplevel.theory o top_eval));
|
|
370 |
|
|
371 |
val _ = OuterSyntax.add_parsers [nbeP];
|
|
372 |
|
|
373 |
ProofGeneral.write_keywords "nbe";
|
|
374 |
(* isar-keywords-nbe.el -> isabelle/etc/
|
|
375 |
Isabelle -k nbe *)
|
19118
|
376 |
|
19116
|
377 |
*)
|