23663
|
1 |
(* Title: Pure/Tools/am_interpreter.ML
|
23174
|
2 |
ID: $Id$
|
|
3 |
Author: Steven Obua
|
|
4 |
*)
|
|
5 |
|
|
6 |
structure AM_Interpreter : ABSTRACT_MACHINE = struct
|
|
7 |
|
23663
|
8 |
open AbstractMachine;
|
23174
|
9 |
|
23663
|
10 |
datatype closure = CDummy | CVar of int | CConst of int
|
23174
|
11 |
| CApp of closure * closure | CAbs of closure
|
|
12 |
| Closure of (closure list) * closure
|
|
13 |
|
|
14 |
structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
|
|
15 |
|
|
16 |
datatype program = Program of ((pattern * closure) list) prog_struct.table
|
|
17 |
|
|
18 |
datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
|
|
19 |
|
|
20 |
fun clos_of_term (Var x) = CVar x
|
|
21 |
| clos_of_term (Const c) = CConst c
|
|
22 |
| clos_of_term (App (u, v)) = CApp (clos_of_term u, clos_of_term v)
|
|
23 |
| clos_of_term (Abs u) = CAbs (clos_of_term u)
|
|
24 |
|
|
25 |
fun term_of_clos (CVar x) = Var x
|
|
26 |
| term_of_clos (CConst c) = Const c
|
|
27 |
| term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
|
|
28 |
| term_of_clos (CAbs u) = Abs (term_of_clos u)
|
|
29 |
| term_of_clos (Closure (e, u)) = raise (Run "internal error: closure in normalized term found")
|
23663
|
30 |
| term_of_clos CDummy = raise (Run "internal error: dummy in normalized term found")
|
23174
|
31 |
|
|
32 |
fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
|
|
33 |
| strip_closure args x = (x, args)
|
|
34 |
|
|
35 |
fun len_head_of_closure n (CApp (a,b)) = len_head_of_closure (n+1) a
|
|
36 |
| len_head_of_closure n x = (n, x)
|
|
37 |
|
|
38 |
|
|
39 |
(* earlier occurrence of PVar corresponds to higher de Bruijn index *)
|
|
40 |
fun pattern_match args PVar clos = SOME (clos::args)
|
|
41 |
| pattern_match args (PConst (c, patterns)) clos =
|
|
42 |
let
|
|
43 |
val (f, closargs) = strip_closure [] clos
|
|
44 |
in
|
|
45 |
case f of
|
|
46 |
CConst d =>
|
|
47 |
if c = d then
|
|
48 |
pattern_match_list args patterns closargs
|
|
49 |
else
|
|
50 |
NONE
|
|
51 |
| _ => NONE
|
|
52 |
end
|
|
53 |
and pattern_match_list args [] [] = SOME args
|
|
54 |
| pattern_match_list args (p::ps) (c::cs) =
|
|
55 |
(case pattern_match args p c of
|
|
56 |
NONE => NONE
|
|
57 |
| SOME args => pattern_match_list args ps cs)
|
|
58 |
| pattern_match_list _ _ _ = NONE
|
|
59 |
|
|
60 |
fun count_patternvars PVar = 1
|
|
61 |
| count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
|
|
62 |
|
|
63 |
fun pattern_key (PConst (c, ps)) = (c, length ps)
|
|
64 |
| pattern_key _ = raise (Compile "pattern reduces to variable")
|
|
65 |
|
23663
|
66 |
(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
|
|
67 |
check_freevars 0 t iff t is closed*)
|
|
68 |
fun check_freevars free (Var x) = x < free
|
|
69 |
| check_freevars free (Const c) = true
|
|
70 |
| check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
|
|
71 |
| check_freevars free (Abs m) = check_freevars (free+1) m
|
|
72 |
|
23174
|
73 |
fun compile eqs =
|
|
74 |
let
|
23663
|
75 |
val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
|
|
76 |
val eqs = map (fn (a,b,c) => (b,c)) eqs
|
|
77 |
fun check (p, r) = if check_freevars (count_patternvars p) r then () else raise Compile ("unbound variables in rule")
|
|
78 |
val eqs = map (fn (p, r) => (check (p,r); (pattern_key p, (p, clos_of_term r)))) eqs
|
|
79 |
fun merge (k, a) table = prog_struct.update (k, case prog_struct.lookup table k of NONE => [a] | SOME l => a::l) table
|
|
80 |
val p = fold merge eqs prog_struct.empty
|
23174
|
81 |
in
|
23663
|
82 |
Program p
|
23174
|
83 |
end
|
|
84 |
|
|
85 |
fun match_rules n [] clos = NONE
|
|
86 |
| match_rules n ((p,eq)::rs) clos =
|
|
87 |
case pattern_match [] p clos of
|
|
88 |
NONE => match_rules (n+1) rs clos
|
|
89 |
| SOME args => SOME (Closure (args, eq))
|
|
90 |
|
|
91 |
fun match_closure (Program prog) clos =
|
|
92 |
case len_head_of_closure 0 clos of
|
|
93 |
(len, CConst c) =>
|
|
94 |
(case prog_struct.lookup prog (c, len) of
|
|
95 |
NONE => NONE
|
|
96 |
| SOME rules => match_rules 0 rules clos)
|
|
97 |
| _ => NONE
|
|
98 |
|
23663
|
99 |
|
|
100 |
type state = bool * program * stack * closure
|
|
101 |
|
|
102 |
datatype loopstate = Continue of state | Stop of stack * closure
|
|
103 |
|
|
104 |
fun proj_C (Continue s) = s
|
|
105 |
| proj_C _ = raise Match
|
|
106 |
|
|
107 |
fun proj_S (Stop s) = s
|
|
108 |
| proj_S _ = raise Match
|
|
109 |
|
|
110 |
fun cont (Continue _) = true
|
|
111 |
| cont _ = false
|
23174
|
112 |
|
23663
|
113 |
fun do_reduction reduce p =
|
|
114 |
let
|
|
115 |
val s = ref (Continue p)
|
|
116 |
val _ = while cont (!s) do (s := reduce (proj_C (!s)))
|
|
117 |
in
|
|
118 |
proj_S (!s)
|
|
119 |
end
|
23174
|
120 |
|
23663
|
121 |
fun weak_reduce (false, prog, stack, Closure (e, CApp (a, b))) = Continue (false, prog, SAppL (Closure (e, b), stack), Closure (e, a))
|
|
122 |
| weak_reduce (false, prog, SAppL (b, stack), Closure (e, CAbs m)) = Continue (false, prog, stack, Closure (b::e, m))
|
|
123 |
| weak_reduce (false, prog, stack, Closure (e, CVar n)) = Continue (false, prog, stack, case List.nth (e, n) of CDummy => CVar n | r => r)
|
|
124 |
| weak_reduce (false, prog, stack, Closure (e, c as CConst _)) = Continue (false, prog, stack, c)
|
|
125 |
| weak_reduce (false, prog, stack, clos) =
|
|
126 |
(case match_closure prog clos of
|
|
127 |
NONE => Continue (true, prog, stack, clos)
|
|
128 |
| SOME r => Continue (false, prog, stack, r))
|
|
129 |
| weak_reduce (true, prog, SAppR (a, stack), b) = Continue (false, prog, stack, CApp (a,b))
|
|
130 |
| weak_reduce (true, prog, s as (SAppL (b, stack)), a) = Continue (false, prog, SAppR (a, stack), b)
|
|
131 |
| weak_reduce (true, prog, stack, c) = Stop (stack, c)
|
|
132 |
|
|
133 |
fun strong_reduce (false, prog, stack, Closure (e, CAbs m)) =
|
23174
|
134 |
let
|
23663
|
135 |
val (stack', wnf) = do_reduction weak_reduce (false, prog, SEmpty, Closure (CDummy::e, m))
|
23174
|
136 |
in
|
|
137 |
case stack' of
|
23663
|
138 |
SEmpty => Continue (false, prog, SAbs stack, wnf)
|
23174
|
139 |
| _ => raise (Run "internal error in strong: weak failed")
|
|
140 |
end
|
23663
|
141 |
| strong_reduce (false, prog, stack, clos as (CApp (u, v))) = Continue (false, prog, SAppL (v, stack), u)
|
|
142 |
| strong_reduce (false, prog, stack, clos) = Continue (true, prog, stack, clos)
|
|
143 |
| strong_reduce (true, prog, SAbs stack, m) = Continue (false, prog, stack, CAbs m)
|
|
144 |
| strong_reduce (true, prog, SAppL (b, stack), a) = Continue (false, prog, SAppR (a, stack), b)
|
|
145 |
| strong_reduce (true, prog, SAppR (a, stack), b) = Continue (true, prog, stack, CApp (a, b))
|
|
146 |
| strong_reduce (true, prog, stack, clos) = Stop (stack, clos)
|
23174
|
147 |
|
|
148 |
fun run prog t =
|
|
149 |
let
|
23663
|
150 |
val (stack, wnf) = do_reduction weak_reduce (false, prog, SEmpty, Closure ([], clos_of_term t))
|
23174
|
151 |
in
|
|
152 |
case stack of
|
23663
|
153 |
SEmpty => (case do_reduction strong_reduce (false, prog, SEmpty, wnf) of
|
23174
|
154 |
(SEmpty, snf) => term_of_clos snf
|
|
155 |
| _ => raise (Run "internal error in run: strong failed"))
|
|
156 |
| _ => raise (Run "internal error in run: weak failed")
|
|
157 |
end
|
|
158 |
|
23663
|
159 |
fun discard p = ()
|
23174
|
160 |
|
23663
|
161 |
end
|