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