author | obua |
Tue, 12 Jul 2005 21:49:38 +0200 | |
changeset 16782 | b214f21ae396 |
parent 16781 | 663235466562 |
child 16842 | 5979c46853d1 |
permissions | -rw-r--r-- |
16781 | 1 |
(* Title: Pure/Tools/am_compiler.ML |
2 |
ID: $Id$ |
|
3 |
Author: Steven Obua |
|
4 |
*) |
|
5 |
||
6 |
signature COMPILING_AM = |
|
7 |
sig |
|
8 |
include ABSTRACT_MACHINE |
|
9 |
||
10 |
datatype closure = CVar of int | CConst of int |
|
11 |
| CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure |
|
12 |
||
13 |
val set_compiled_rewriter : (term -> closure) -> unit |
|
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
16781
diff
changeset
|
14 |
val list_nth : 'a list * int -> 'a |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
16781
diff
changeset
|
15 |
val list_map : ('a -> 'b) -> 'a list -> 'b list |
16781 | 16 |
end |
17 |
||
18 |
structure AM_Compiler :> COMPILING_AM = struct |
|
19 |
||
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
16781
diff
changeset
|
20 |
val list_nth = List.nth; |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
16781
diff
changeset
|
21 |
val list_map = map; |
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
16781
diff
changeset
|
22 |
|
16781 | 23 |
datatype term = Var of int | Const of int | App of term * term | Abs of term |
24 |
||
25 |
datatype pattern = PVar | PConst of int * (pattern list) |
|
26 |
||
27 |
datatype closure = CVar of int | CConst of int |
|
28 |
| CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure |
|
29 |
||
30 |
val compiled_rewriter = ref (NONE:(term -> closure)Option.option) |
|
31 |
||
32 |
fun set_compiled_rewriter r = (compiled_rewriter := SOME r) |
|
33 |
||
34 |
type program = (term -> term) |
|
35 |
||
36 |
datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack |
|
37 |
||
38 |
exception Compile of string; |
|
39 |
exception Run of string; |
|
40 |
||
41 |
fun clos_of_term (Var x) = CVar x |
|
42 |
| clos_of_term (Const c) = CConst c |
|
43 |
| clos_of_term (App (u, v)) = CApp (clos_of_term u, clos_of_term v) |
|
44 |
| clos_of_term (Abs u) = CAbs (clos_of_term u) |
|
45 |
||
46 |
fun term_of_clos (CVar x) = Var x |
|
47 |
| term_of_clos (CConst c) = Const c |
|
48 |
| term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v) |
|
49 |
| term_of_clos (CAbs u) = Abs (term_of_clos u) |
|
50 |
| term_of_clos (Closure (e, u)) = raise (Run "internal error: closure in normalized term found") |
|
51 |
||
52 |
fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a |
|
53 |
| strip_closure args x = (x, args) |
|
54 |
||
55 |
(* Returns true iff at most 0 .. (free-1) occur unbound. therefore check_freevars 0 t iff t is closed *) |
|
56 |
fun check_freevars free (Var x) = x < free |
|
57 |
| check_freevars free (Const c) = true |
|
58 |
| check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v |
|
59 |
| check_freevars free (Abs m) = check_freevars (free+1) m |
|
60 |
||
61 |
fun count_patternvars PVar = 1 |
|
62 |
| count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps |
|
63 |
||
64 |
fun print_rule (p, t) = |
|
65 |
let |
|
66 |
fun str x = Int.toString x |
|
67 |
fun print_pattern n PVar = (n+1, "x"^(str n)) |
|
68 |
| print_pattern n (PConst (c, [])) = (n, "c"^(str c)) |
|
69 |
| print_pattern n (PConst (c, args)) = |
|
70 |
let |
|
71 |
val h = print_pattern n (PConst (c,[])) |
|
72 |
in |
|
73 |
print_pattern_list h args |
|
74 |
end |
|
75 |
and print_pattern_list r [] = r |
|
76 |
| print_pattern_list (n, p) (t::ts) = |
|
77 |
let |
|
78 |
val (n, t) = print_pattern n t |
|
79 |
in |
|
80 |
print_pattern_list (n, "App ("^p^", "^t^")") ts |
|
81 |
end |
|
82 |
||
83 |
val (n, pattern) = print_pattern 0 p |
|
84 |
val pattern = if List.exists Char.isSpace (String.explode pattern) then "("^pattern^")" else pattern |
|
85 |
||
86 |
fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*) "Var "^(str x) |
|
87 |
| print_term d (Const c) = "c"^(str c) |
|
88 |
| print_term d (App (a,b)) = "App ("^(print_term d a)^", "^(print_term d b)^")" |
|
89 |
| print_term d (Abs c) = "Abs ("^(print_term (d+1) c)^")" |
|
90 |
||
91 |
fun listvars n = if n = 0 then "x0" else "x"^(str n)^", "^(listvars (n-1)) |
|
92 |
||
93 |
val term = print_term 0 t |
|
94 |
val term = if n > 0 then "Closure (["^(listvars (n-1))^"], "^term^")" else "Closure ([], "^term^")" |
|
95 |
||
96 |
in |
|
97 |
"lookup stack "^pattern^" = weak stack ("^term^")" |
|
98 |
end |
|
99 |
||
100 |
fun remove_dups (c::cs) = |
|
101 |
let val cs = remove_dups cs in |
|
102 |
if (List.exists (fn x => x=c) cs) then cs else c::cs |
|
103 |
end |
|
104 |
| remove_dups [] = [] |
|
105 |
||
106 |
fun constants_of PVar = [] |
|
107 |
| constants_of (PConst (c, ps)) = c::(List.concat (map constants_of ps)) |
|
108 |
||
109 |
fun constants_of_term (Var _) = [] |
|
110 |
| constants_of_term (Abs m) = constants_of_term m |
|
111 |
| constants_of_term (App (a,b)) = (constants_of_term a)@(constants_of_term b) |
|
112 |
| constants_of_term (Const c) = [c] |
|
113 |
||
114 |
fun load_rules sname name prog = |
|
115 |
let |
|
116 |
val buffer = ref "" |
|
117 |
fun write s = (buffer := (!buffer)^s) |
|
118 |
fun writeln s = (write s; write "\n") |
|
119 |
fun writelist [] = () |
|
120 |
| writelist (s::ss) = (writeln s; writelist ss) |
|
121 |
fun str i = Int.toString i |
|
122 |
val _ = writelist [ |
|
123 |
"structure "^name^" = struct", |
|
124 |
"", |
|
125 |
"datatype term = App of term * term | Abs of term | Var of int | Const of int | Closure of term list * term"] |
|
126 |
val constants = remove_dups (List.concat (map (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog)) |
|
127 |
val _ = map (fn x => write (" | c"^(str x))) constants |
|
128 |
val _ = writelist [ |
|
129 |
"", |
|
130 |
"datatype stack = SEmpty | SAppL of term * stack | SAppR of term * stack | SAbs of stack", |
|
131 |
""] |
|
132 |
val _ = (case prog of |
|
133 |
r::rs => (writeln ("fun "^(print_rule r)); |
|
134 |
map (fn r => writeln(" | "^(print_rule r))) rs; |
|
135 |
writeln (" | lookup stack clos = weak_last stack clos"); ()) |
|
136 |
| [] => (writeln "fun lookup stack clos = weak_last stack clos")) |
|
137 |
val _ = writelist [ |
|
138 |
"and weak stack (Closure (e, App (a, b))) = weak (SAppL (Closure (e, b), stack)) (Closure (e, a))", |
|
139 |
" | weak (SAppL (b, stack)) (Closure (e, Abs m)) = weak stack (Closure (b::e, m))", |
|
140 |
" | weak stack (clos as Closure (_, Abs _)) = weak_last stack clos", |
|
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
16781
diff
changeset
|
141 |
" | weak stack (Closure (e, Var n)) = weak stack ("^sname^".list_nth (e, n) handle _ => (Var (n-(length e))))", |
16781 | 142 |
" | weak stack (Closure (e, c)) = weak stack c", |
143 |
" | weak stack clos = lookup stack clos", |
|
144 |
"and weak_last (SAppR (a, stack)) b = weak stack (App(a, b))", |
|
145 |
" | weak_last (SAppL (b, stack)) a = weak (SAppR (a, stack)) b", |
|
146 |
" | weak_last stack c = (stack, c)", |
|
147 |
"", |
|
148 |
"fun lift n (v as Var m) = if m < n then v else Var (m+1)", |
|
149 |
" | lift n (Abs t) = Abs (lift (n+1) t)", |
|
150 |
" | lift n (App (a,b)) = App (lift n a, lift n b)", |
|
151 |
" | lift n (Closure (e, a)) = Closure (lift_env n e, lift (n+(length e)) a)", |
|
152 |
" | lift n c = c", |
|
153 |
"and lift_env n e = map (lift n) e", |
|
154 |
"", |
|
155 |
"fun strong stack (Closure (e, Abs m)) = ", |
|
156 |
" let", |
|
157 |
" val (stack', wnf) = weak SEmpty (Closure ((Var 0)::(lift_env 0 e), m))", |
|
158 |
" in", |
|
159 |
" case stack' of", |
|
160 |
" SEmpty => strong (SAbs stack) wnf", |
|
161 |
" | _ => raise ("^sname^".Run \"internal error in strong: weak failed\")", |
|
162 |
" end", |
|
163 |
" | strong stack (clos as (App (u, v))) = strong (SAppL (v, stack)) u", |
|
164 |
" | strong stack clos = strong_last stack clos", |
|
165 |
"and strong_last (SAbs stack) m = strong stack (Abs m)", |
|
166 |
" | strong_last (SAppL (b, stack)) a = strong (SAppR (a, stack)) b", |
|
167 |
" | strong_last (SAppR (a, stack)) b = strong_last stack (App (a, b))", |
|
168 |
" | strong_last stack clos = (stack, clos)", |
|
169 |
""] |
|
170 |
||
171 |
val ic = "(case c of "^(String.concat (map (fn c => (str c)^" => c"^(str c)^" | ") constants))^" _ => Const c)" |
|
172 |
val _ = writelist [ |
|
173 |
"fun importTerm ("^sname^".Var x) = Var x", |
|
174 |
" | importTerm ("^sname^".Const c) = "^ic, |
|
175 |
" | importTerm ("^sname^".App (a, b)) = App (importTerm a, importTerm b)", |
|
176 |
" | importTerm ("^sname^".Abs m) = Abs (importTerm m)", |
|
177 |
""] |
|
178 |
||
179 |
fun ec c = " | exportTerm c"^(str c)^" = "^sname^".CConst "^(str c) |
|
180 |
val _ = writelist [ |
|
181 |
"fun exportTerm (Var x) = "^sname^".CVar x", |
|
182 |
" | exportTerm (Const c) = "^sname^".CConst c", |
|
183 |
" | exportTerm (App (a,b)) = "^sname^".CApp (exportTerm a, exportTerm b)", |
|
184 |
" | exportTerm (Abs m) = "^sname^".CAbs (exportTerm m)", |
|
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
16781
diff
changeset
|
185 |
" | exportTerm (Closure (closlist, clos)) = "^sname^".Closure ("^sname^".list_map exportTerm closlist, exportTerm clos)"] |
16781 | 186 |
val _ = writelist (map ec constants) |
187 |
||
188 |
val _ = writelist [ |
|
189 |
"", |
|
190 |
"fun rewrite t = ", |
|
191 |
" let", |
|
192 |
" val (stack, wnf) = weak SEmpty (Closure ([], importTerm t))", |
|
193 |
" in", |
|
194 |
" case stack of ", |
|
195 |
" SEmpty => (case strong SEmpty wnf of", |
|
196 |
" (SEmpty, snf) => exportTerm snf", |
|
197 |
" | _ => raise ("^sname^".Run \"internal error in rewrite: strong failed\"))", |
|
198 |
" | _ => (raise ("^sname^".Run \"internal error in rewrite: weak failed\"))", |
|
199 |
" end", |
|
200 |
"", |
|
201 |
"val _ = "^sname^".set_compiled_rewriter rewrite", |
|
202 |
"", |
|
203 |
"end;"] |
|
204 |
||
205 |
val _ = |
|
206 |
let |
|
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
16781
diff
changeset
|
207 |
(*val fout = TextIO.openOut "gen_code.ML" |
16781 | 208 |
val _ = TextIO.output (fout, !buffer) |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
16781
diff
changeset
|
209 |
val _ = TextIO.closeOut fout*) |
16781 | 210 |
in |
211 |
() |
|
212 |
end |
|
213 |
||
214 |
val dummy = (fn s => ()) |
|
215 |
in |
|
216 |
compiled_rewriter := NONE; |
|
217 |
use_text (dummy, dummy) false (!buffer); |
|
218 |
case !compiled_rewriter of |
|
219 |
NONE => raise (Compile "cannot communicate with compiled function") |
|
220 |
| SOME r => (compiled_rewriter := NONE; fn t => term_of_clos (r t)) |
|
221 |
end |
|
222 |
||
223 |
fun compile eqs = |
|
224 |
let |
|
225 |
val _ = map (fn (p, r) => |
|
226 |
(check_freevars (count_patternvars p) r; |
|
227 |
case p of PVar => raise (Compile "pattern reduces to a variable") | _ => ())) eqs |
|
228 |
in |
|
229 |
load_rules "AM_Compiler" "AM_compiled_code" eqs |
|
230 |
end |
|
231 |
||
232 |
fun run prog t = (prog t) |
|
233 |
||
234 |
end |
|
235 |
||
236 |
structure AbstractMachine = AM_Compiler |