author | nipkow |
Fri, 09 Jun 2006 12:17:58 +0200 | |
changeset 19830 | b81d803dfaa4 |
parent 19795 | 746274ca400b |
child 20706 | f77bd47a70df |
permissions | -rwxr-xr-x |
19116 | 1 |
(* ID: $Id$ |
19177 | 2 |
Author: Klaus Aehlig, LMU Muenchen; Tobias Nipkow, TU Muenchen |
3 |
||
4 |
Code generator for "normalization by evaluation". |
|
19116 | 5 |
*) |
6 |
||
7 |
(* Global asssumptions: |
|
8 |
For each function: there is at least one defining eqns and |
|
9 |
all defining equations have same number of arguments. |
|
10 |
||
11 |
FIXME |
|
19147 | 12 |
fun MLname |
19116 | 13 |
val quote = quote; |
14 |
||
15 |
*) |
|
16 |
||
19118 | 17 |
signature NBE_CODEGEN = |
18 |
sig |
|
19177 | 19 |
val generate: (string -> bool) -> string * CodegenThingol.def -> string; |
20 |
val nterm_to_term: theory -> NBE_Eval.nterm -> term; |
|
19118 | 21 |
end |
22 |
||
23 |
||
24 |
structure NBE_Codegen: NBE_CODEGEN = |
|
25 |
struct |
|
26 |
||
19116 | 27 |
val Eval = "NBE_Eval"; |
19147 | 28 |
val Eval_mk_Fun = Eval ^ ".mk_Fun"; |
19116 | 29 |
val Eval_apply = Eval ^ ".apply"; |
30 |
val Eval_Constr = Eval ^ ".Constr"; |
|
31 |
val Eval_C = Eval ^ ".C"; |
|
32 |
val Eval_AbsN = Eval ^ ".AbsN"; |
|
33 |
val Eval_Fun = Eval ^ ".Fun"; |
|
34 |
val Eval_BVar = Eval ^ ".BVar"; |
|
35 |
val Eval_new_name = Eval ^ ".new_name"; |
|
36 |
val Eval_to_term = Eval ^ ".to_term"; |
|
37 |
||
19147 | 38 |
fun MLname s = "nbe_" ^ translate_string (fn "." => "_" | c => c) s; |
19116 | 39 |
fun MLvname s = "v_" ^ MLname s; |
40 |
fun MLparam n = "p_" ^ string_of_int n; |
|
41 |
fun MLintern s = "i_" ^ MLname s; |
|
42 |
||
43 |
fun MLparams n = map MLparam (1 upto n); |
|
44 |
||
45 |
structure S = |
|
46 |
struct |
|
47 |
||
48 |
val quote = quote; (* FIXME *) |
|
49 |
||
50 |
fun app e1 e2 = "(" ^ e1 ^ " " ^ e2 ^ ")"; |
|
51 |
fun abs v e = "(fn" ^ v ^ " => " ^ e ^ ")"; |
|
52 |
fun tup es = "(" ^ commas es ^ ")"; |
|
53 |
fun list es = "[" ^ commas es ^ "]"; |
|
54 |
||
55 |
fun apps s ss = Library.foldl (uncurry app) (s, ss); |
|
56 |
fun nbe_apps s ss = |
|
57 |
Library.foldr (fn (s,e) => app (app Eval_apply e) s) (ss,s); |
|
58 |
||
59 |
fun eqns name ees = |
|
60 |
let fun eqn (es,e) = name ^ " " ^ space_implode " " es ^ " = " ^ e |
|
61 |
in "fun " ^ space_implode "\n | " (map eqn ees) ^ ";\n" end; |
|
62 |
||
63 |
||
64 |
fun Val v s = "val " ^ v ^ " = " ^ s; |
|
65 |
fun Let ds e = "let\n" ^ (space_implode "\n" ds) ^ " in " ^ e ^ " end" |
|
66 |
||
67 |
end |
|
68 |
||
19177 | 69 |
val tab_lookup = S.app "NBE.lookup"; |
70 |
val tab_update = S.app "NBE.update"; |
|
19147 | 71 |
|
19116 | 72 |
fun mk_nbeFUN(nm,e) = |
73 |
S.app Eval_Fun (S.tup [S.abs(S.list [MLvname nm])e,S.list [],"1", |
|
74 |
S.abs(S.tup [])(S.Let |
|
75 |
[S.Val (MLintern "var") (S.app Eval_new_name (S.tup [])), |
|
76 |
S.Val (MLvname nm) (S.app Eval_BVar (S.tup [(MLintern "var"), S.list []]))] |
|
77 |
(S.app Eval_AbsN(S.tup[MLintern "var",(S.app Eval_to_term e)])))]); |
|
78 |
||
79 |
fun take_last n xs = rev (Library.take(n, rev xs)); |
|
80 |
fun drop_last n xs = rev (Library.drop(n, rev xs)); |
|
81 |
||
82 |
fun selfcall nm ar args = |
|
83 |
if (ar <= length args) then |
|
84 |
S.nbe_apps (S.app (MLname nm) (S.list (take_last ar args))) |
|
85 |
(drop_last ar args) |
|
86 |
else S.app Eval_Fun (S.tup [MLname nm,S.list args, |
|
87 |
string_of_int(ar - (length args)), |
|
88 |
S.abs (S.tup []) (S.app Eval_C |
|
89 |
(S.quote nm))]); |
|
90 |
||
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19147
diff
changeset
|
91 |
open BasicCodegenThingol; |
19116 | 92 |
|
19147 | 93 |
fun mk_rexpr defined nm ar = |
19202 | 94 |
let |
95 |
fun mk args = CodegenThingol.map_pure (mk' args) |
|
96 |
and mk' args (IConst (c, _)) = |
|
97 |
if c = nm then selfcall nm ar args |
|
98 |
else if defined c then S.nbe_apps (MLname c) args |
|
99 |
else S.app Eval_Constr (S.tup [S.quote c, S.list args]) |
|
100 |
| mk' args (IVar s) = S.nbe_apps (MLvname s) args |
|
101 |
| mk' args (e1 `$ e2) = mk (args @ [mk [] e2]) e1 |
|
102 |
| mk' args ((nm, _) `|-> e) = S.nbe_apps (mk_nbeFUN (nm, mk [] e)) args; |
|
19116 | 103 |
in mk [] end; |
104 |
||
105 |
val mk_lexpr = |
|
19202 | 106 |
let |
107 |
fun mk args = CodegenThingol.map_pure (mk' args) |
|
108 |
and mk' args (IConst (c, _)) = |
|
109 |
S.app Eval_Constr (S.tup [S.quote c, S.list args]) |
|
110 |
| mk' args (IVar s) = if args = [] then MLvname s else |
|
111 |
sys_error "NBE mk_lexpr illegal higher order pattern" |
|
112 |
| mk' args (e1 `$ e2) = mk (args @ [mk [] e2]) e1 |
|
113 |
| mk' args (_ `|-> _) = |
|
114 |
sys_error "NBE mk_lexpr illegal pattern"; |
|
19116 | 115 |
in mk [] end; |
116 |
||
19147 | 117 |
fun mk_eqn defined nm ar (lhs,e) = |
19202 | 118 |
if has_duplicates (op =) (fold CodegenThingol.add_varnames lhs []) then [] else |
19178 | 119 |
[([S.list(map mk_lexpr (rev lhs))], mk_rexpr defined nm ar e)]; |
19116 | 120 |
|
19147 | 121 |
fun lookup nm = S.Val (MLname nm) (tab_lookup (S.quote nm)); |
19116 | 122 |
|
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19147
diff
changeset
|
123 |
fun generate defined (nm, CodegenThingol.Fun (eqns, _)) = |
19177 | 124 |
let |
19202 | 125 |
val ar = (length o fst o hd) eqns; |
126 |
val params = (S.list o rev o MLparams) ar; |
|
127 |
val funs = |
|
128 |
[] |
|
129 |
|> fold (fn (_, e) => CodegenThingol.add_constnames e) eqns |
|
130 |
|> remove (op =) nm; |
|
19177 | 131 |
val globals = map lookup (filter defined funs); |
132 |
val default_eqn = ([params], S.app Eval_Constr (S.tup[S.quote nm,params])); |
|
133 |
val code = S.eqns (MLname nm) |
|
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19341
diff
changeset
|
134 |
(maps (mk_eqn defined nm ar) eqns @ [default_eqn]) |
19177 | 135 |
val register = tab_update |
136 |
(S.app Eval_mk_Fun (S.tup[S.quote nm, MLname nm, string_of_int ar])) |
|
137 |
in |
|
138 |
S.Let (globals @ [code]) register |
|
139 |
end |
|
140 |
| generate _ _ = ""; |
|
141 |
||
142 |
open NBE_Eval; |
|
143 |
||
19795 | 144 |
val tcount = ref 0; |
145 |
||
19830 | 146 |
(* FIXME get rid of TFree case!!! *) |
19795 | 147 |
fun varifyT ty = |
148 |
let val ty' = map_type_tvar (fn ((s,i),S) => TypeInfer.param (!tcount + i) (s,S)) ty; |
|
149 |
val _ = (tcount := !tcount + maxidx_of_typ ty + 1); |
|
150 |
val ty'' = map_type_tfree (TypeInfer.param (!tcount)) ty' |
|
151 |
in tcount := !tcount+1; ty'' end; |
|
152 |
||
19177 | 153 |
fun nterm_to_term thy t = |
19116 | 154 |
let |
19177 | 155 |
fun consts_of (C s) = insert (op =) s |
156 |
| consts_of (V _) = I |
|
157 |
| consts_of (B _) = I |
|
158 |
| consts_of (A (t1, t2)) = consts_of t1 #> consts_of t2 |
|
159 |
| consts_of (AbsN (_, t)) = consts_of t; |
|
160 |
val consts = consts_of t []; |
|
19795 | 161 |
val ctab = consts ~~ CodegenPackage.consts_of_idfs thy consts; |
162 |
val the_const = apsnd varifyT o the o AList.lookup (op =) ctab; |
|
19177 | 163 |
fun to_term bounds (C s) = Const (the_const s) |
164 |
| to_term bounds (V s) = Free (s, dummyT) |
|
165 |
| to_term bounds (B i) = Bound (find_index (fn j => i = j) bounds) |
|
166 |
| to_term bounds (A (t1, t2)) = to_term bounds t1 $ to_term bounds t2 |
|
167 |
| to_term bounds (AbsN (i, t)) = |
|
168 |
Abs("u", dummyT, to_term (i::bounds) t); |
|
19795 | 169 |
in tcount := 0; to_term [] t end; |
19116 | 170 |
|
19118 | 171 |
end; |