author | boehmes |
Wed, 07 Apr 2010 20:38:11 +0200 | |
changeset 36082 | 8f10b0e77d94 |
parent 32960 | 69916a850301 |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: Tools/Compute_Oracle/am_compiler.ML |
23174 | 2 |
Author: Steven Obua |
3 |
*) |
|
4 |
||
5 |
signature COMPILING_AM = |
|
6 |
sig |
|
7 |
include ABSTRACT_MACHINE |
|
8 |
||
23663 | 9 |
val set_compiled_rewriter : (term -> term) -> unit |
23174 | 10 |
val list_nth : 'a list * int -> 'a |
11 |
val list_map : ('a -> 'b) -> 'a list -> 'b list |
|
12 |
end |
|
13 |
||
14 |
structure AM_Compiler : COMPILING_AM = struct |
|
15 |
||
16 |
val list_nth = List.nth; |
|
17 |
val list_map = map; |
|
18 |
||
23663 | 19 |
open AbstractMachine; |
23174 | 20 |
|
32740 | 21 |
val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option) |
23174 | 22 |
|
23 |
fun set_compiled_rewriter r = (compiled_rewriter := SOME r) |
|
24 |
||
25 |
type program = (term -> term) |
|
26 |
||
27 |
fun count_patternvars PVar = 1 |
|
28 |
| count_patternvars (PConst (_, ps)) = |
|
29 |
List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps |
|
30 |
||
31 |
fun print_rule (p, t) = |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
32 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
33 |
fun str x = Int.toString x |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
34 |
fun print_pattern n PVar = (n+1, "x"^(str n)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
35 |
| print_pattern n (PConst (c, [])) = (n, "c"^(str c)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
36 |
| print_pattern n (PConst (c, args)) = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
37 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
38 |
val h = print_pattern n (PConst (c,[])) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
39 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
40 |
print_pattern_list h args |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
41 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
42 |
and print_pattern_list r [] = r |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
43 |
| print_pattern_list (n, p) (t::ts) = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
44 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
45 |
val (n, t) = print_pattern n t |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
46 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
47 |
print_pattern_list (n, "App ("^p^", "^t^")") ts |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
48 |
end |
23174 | 49 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
50 |
val (n, pattern) = print_pattern 0 p |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
51 |
val pattern = |
23174 | 52 |
if exists_string Symbol.is_ascii_blank pattern then "(" ^ pattern ^")" |
53 |
else pattern |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
54 |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
55 |
fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*) |
23174 | 56 |
"Var " ^ str x |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
57 |
| print_term d (Const c) = "c" ^ str c |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
58 |
| print_term d (App (a,b)) = "App (" ^ print_term d a ^ ", " ^ print_term d b ^ ")" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
59 |
| print_term d (Abs c) = "Abs (" ^ print_term (d + 1) c ^ ")" |
25217 | 60 |
| print_term d (Computed c) = print_term d c |
23174 | 61 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
62 |
fun listvars n = if n = 0 then "x0" else "x"^(str n)^", "^(listvars (n-1)) |
23174 | 63 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
64 |
val term = print_term 0 t |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
65 |
val term = |
23174 | 66 |
if n > 0 then "Closure (["^(listvars (n-1))^"], "^term^")" |
67 |
else "Closure ([], "^term^")" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
68 |
|
23174 | 69 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
70 |
" | weak_reduce (false, stack, "^pattern^") = Continue (false, stack, "^term^")" |
23174 | 71 |
end |
72 |
||
73 |
fun constants_of PVar = [] |
|
74 |
| constants_of (PConst (c, ps)) = c :: maps constants_of ps |
|
75 |
||
76 |
fun constants_of_term (Var _) = [] |
|
77 |
| constants_of_term (Abs m) = constants_of_term m |
|
78 |
| constants_of_term (App (a,b)) = (constants_of_term a)@(constants_of_term b) |
|
79 |
| constants_of_term (Const c) = [c] |
|
25217 | 80 |
| constants_of_term (Computed c) = constants_of_term c |
23174 | 81 |
|
82 |
fun load_rules sname name prog = |
|
83 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
84 |
val buffer = Unsynchronized.ref "" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
85 |
fun write s = (buffer := (!buffer)^s) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
86 |
fun writeln s = (write s; write "\n") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
87 |
fun writelist [] = () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
88 |
| writelist (s::ss) = (writeln s; writelist ss) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
89 |
fun str i = Int.toString i |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
90 |
val _ = writelist [ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
91 |
"structure "^name^" = struct", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
92 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
93 |
"datatype term = Dummy | App of term * term | Abs of term | Var of int | Const of int | Closure of term list * term"] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
94 |
val constants = distinct (op =) (maps (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
95 |
val _ = map (fn x => write (" | c"^(str x))) constants |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
96 |
val _ = writelist [ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
97 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
98 |
"datatype stack = SEmpty | SAppL of term * stack | SAppR of term * stack | SAbs of stack", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
99 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
100 |
"type state = bool * stack * term", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
101 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
102 |
"datatype loopstate = Continue of state | Stop of stack * term", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
103 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
104 |
"fun proj_C (Continue s) = s", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
105 |
" | proj_C _ = raise Match", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
106 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
107 |
"fun proj_S (Stop s) = s", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
108 |
" | proj_S _ = raise Match", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
109 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
110 |
"fun cont (Continue _) = true", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
111 |
" | cont _ = false", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
112 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
113 |
"fun do_reduction reduce p =", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
114 |
" let", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
115 |
" val s = Unsynchronized.ref (Continue p)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
116 |
" val _ = while cont (!s) do (s := reduce (proj_C (!s)))", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
117 |
" in", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
118 |
" proj_S (!s)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
119 |
" end", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
120 |
""] |
23663 | 121 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
122 |
val _ = writelist [ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
123 |
"fun weak_reduce (false, stack, Closure (e, App (a, b))) = Continue (false, SAppL (Closure (e, b), stack), Closure (e, a))", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
124 |
" | weak_reduce (false, SAppL (b, stack), Closure (e, Abs m)) = Continue (false, stack, Closure (b::e, m))", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
125 |
" | weak_reduce (false, stack, c as Closure (e, Abs m)) = Continue (true, stack, c)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
126 |
" | weak_reduce (false, stack, Closure (e, Var n)) = Continue (false, stack, case "^sname^".list_nth (e, n) of Dummy => Var n | r => r)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
127 |
" | weak_reduce (false, stack, Closure (e, c)) = Continue (false, stack, c)"] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
128 |
val _ = writelist (map print_rule prog) |
23663 | 129 |
val _ = writelist [ |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
130 |
" | weak_reduce (false, stack, clos) = Continue (true, stack, clos)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
131 |
" | weak_reduce (true, SAppR (a, stack), b) = Continue (false, stack, App (a,b))", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
132 |
" | weak_reduce (true, s as (SAppL (b, stack)), a) = Continue (false, SAppR (a, stack), b)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
133 |
" | weak_reduce (true, stack, c) = Stop (stack, c)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
134 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
135 |
"fun strong_reduce (false, stack, Closure (e, Abs m)) =", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
136 |
" let", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
137 |
" val (stack', wnf) = do_reduction weak_reduce (false, SEmpty, Closure (Dummy::e, m))", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
138 |
" in", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
139 |
" case stack' of", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
140 |
" SEmpty => Continue (false, SAbs stack, wnf)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
141 |
" | _ => raise ("^sname^".Run \"internal error in strong: weak failed\")", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
142 |
" end", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
143 |
" | strong_reduce (false, stack, clos as (App (u, v))) = Continue (false, SAppL (v, stack), u)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
144 |
" | strong_reduce (false, stack, clos) = Continue (true, stack, clos)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
145 |
" | strong_reduce (true, SAbs stack, m) = Continue (false, stack, Abs m)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
146 |
" | strong_reduce (true, SAppL (b, stack), a) = Continue (false, SAppR (a, stack), b)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
147 |
" | strong_reduce (true, SAppR (a, stack), b) = Continue (true, stack, App (a, b))", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
148 |
" | strong_reduce (true, stack, clos) = Stop (stack, clos)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
149 |
""] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
150 |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
151 |
val ic = "(case c of "^(implode (map (fn c => (str c)^" => c"^(str c)^" | ") constants))^" _ => Const c)" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
152 |
val _ = writelist [ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
153 |
"fun importTerm ("^sname^".Var x) = Var x", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
154 |
" | importTerm ("^sname^".Const c) = "^ic, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
155 |
" | importTerm ("^sname^".App (a, b)) = App (importTerm a, importTerm b)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
156 |
" | importTerm ("^sname^".Abs m) = Abs (importTerm m)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
157 |
""] |
23174 | 158 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
159 |
fun ec c = " | exportTerm c"^(str c)^" = "^sname^".Const "^(str c) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
160 |
val _ = writelist [ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
161 |
"fun exportTerm (Var x) = "^sname^".Var x", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
162 |
" | exportTerm (Const c) = "^sname^".Const c", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
163 |
" | exportTerm (App (a,b)) = "^sname^".App (exportTerm a, exportTerm b)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
164 |
" | exportTerm (Abs m) = "^sname^".Abs (exportTerm m)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
165 |
" | exportTerm (Closure (closlist, clos)) = raise ("^sname^".Run \"internal error, cannot export Closure\")", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
166 |
" | exportTerm Dummy = raise ("^sname^".Run \"internal error, cannot export Dummy\")"] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
167 |
val _ = writelist (map ec constants) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
168 |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
169 |
val _ = writelist [ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
170 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
171 |
"fun rewrite t = ", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
172 |
" let", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
173 |
" val (stack, wnf) = do_reduction weak_reduce (false, SEmpty, Closure ([], importTerm t))", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
174 |
" in", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
175 |
" case stack of ", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
176 |
" SEmpty => (case do_reduction strong_reduce (false, SEmpty, wnf) of", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
177 |
" (SEmpty, snf) => exportTerm snf", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
178 |
" | _ => raise ("^sname^".Run \"internal error in rewrite: strong failed\"))", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
179 |
" | _ => (raise ("^sname^".Run \"internal error in rewrite: weak failed\"))", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
180 |
" end", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
181 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
182 |
"val _ = "^sname^".set_compiled_rewriter rewrite", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
183 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
184 |
"end;"] |
23174 | 185 |
|
186 |
in |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
187 |
compiled_rewriter := NONE; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
188 |
use_text ML_Env.local_context (1, "") false (!buffer); |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
189 |
case !compiled_rewriter of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
190 |
NONE => raise (Compile "cannot communicate with compiled function") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
191 |
| SOME r => (compiled_rewriter := NONE; r) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
192 |
end |
23174 | 193 |
|
25520 | 194 |
fun compile cache_patterns const_arity eqs = |
23174 | 195 |
let |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
196 |
val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
197 |
val eqs = map (fn (a,b,c) => (b,c)) eqs |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
198 |
fun check (p, r) = if check_freevars (count_patternvars p) r then () else raise Compile ("unbound variables in rule") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
199 |
val _ = map (fn (p, r) => |
23663 | 200 |
(check (p, r); |
201 |
case p of PVar => raise (Compile "pattern is just a variable") | _ => ())) eqs |
|
23174 | 202 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
203 |
load_rules "AM_Compiler" "AM_compiled_code" eqs |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
204 |
end |
23174 | 205 |
|
206 |
fun run prog t = (prog t) |
|
23663 | 207 |
|
208 |
fun discard p = () |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
209 |
|
23174 | 210 |
end |
211 |