author  wenzelm 
Fri, 02 Oct 2009 22:15:08 +0200  
changeset 32861  105f40051387 
parent 32740  9dd0a2f83429 
child 32960  69916a850301 
permissions  rwrr 
24584  1 
(* Title: Tools/Compute_Oracle/am_interpreter.ML 
23174  2 
Author: Steven Obua 
3 
*) 

4 

24654  5 
signature AM_BARRAS = 
6 
sig 

7 
include ABSTRACT_MACHINE 

32740  8 
val max_reductions : int option Unsynchronized.ref 
24654  9 
end 
10 

11 
structure AM_Interpreter : AM_BARRAS = struct 

23174  12 

23663  13 
open AbstractMachine; 
23174  14 

23663  15 
datatype closure = CDummy  CVar of int  CConst of int 
23174  16 
 CApp of closure * closure  CAbs of closure 
17 
 Closure of (closure list) * closure 

18 

31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
30161
diff
changeset

19 
structure prog_struct = Table(type key = int*int val ord = prod_ord int_ord int_ord); 
23174  20 

25520  21 
datatype program = Program of ((pattern * closure * (closure*closure) list) list) prog_struct.table 
23174  22 

23 
datatype stack = SEmpty  SAppL of closure * stack  SAppR of closure * stack  SAbs of stack 

24 

25 
fun clos_of_term (Var x) = CVar x 

26 
 clos_of_term (Const c) = CConst c 

27 
 clos_of_term (App (u, v)) = CApp (clos_of_term u, clos_of_term v) 

28 
 clos_of_term (Abs u) = CAbs (clos_of_term u) 

25217  29 
 clos_of_term (Computed t) = clos_of_term t 
23174  30 

31 
fun term_of_clos (CVar x) = Var x 

32 
 term_of_clos (CConst c) = Const c 

33 
 term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v) 

34 
 term_of_clos (CAbs u) = Abs (term_of_clos u) 

35 
 term_of_clos (Closure (e, u)) = raise (Run "internal error: closure in normalized term found") 

23663  36 
 term_of_clos CDummy = raise (Run "internal error: dummy in normalized term found") 
23174  37 

24654  38 
fun resolve_closure closures (CVar x) = (case List.nth (closures, x) of CDummy => CVar x  r => r) 
39 
 resolve_closure closures (CConst c) = CConst c 

40 
 resolve_closure closures (CApp (u, v)) = CApp (resolve_closure closures u, resolve_closure closures v) 

41 
 resolve_closure closures (CAbs u) = CAbs (resolve_closure (CDummy::closures) u) 

42 
 resolve_closure closures (CDummy) = raise (Run "internal error: resolve_closure applied to CDummy") 

43 
 resolve_closure closures (Closure (e, u)) = resolve_closure e u 

44 

45 
fun resolve_closure' c = resolve_closure [] c 

46 

47 
fun resolve_stack tm SEmpty = tm 

48 
 resolve_stack tm (SAppL (c, s)) = resolve_stack (CApp (tm, resolve_closure' c)) s 

49 
 resolve_stack tm (SAppR (c, s)) = resolve_stack (CApp (resolve_closure' c, tm)) s 

50 
 resolve_stack tm (SAbs s) = resolve_stack (CAbs tm) s 

51 

52 
fun resolve (stack, closure) = 

53 
let 

54 
val _ = writeln "start resolving" 

55 
val t = resolve_stack (resolve_closure' closure) stack 

56 
val _ = writeln "finished resolving" 

57 
in 

58 
t 

59 
end 

60 

23174  61 
fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a 
62 
 strip_closure args x = (x, args) 

63 

64 
fun len_head_of_closure n (CApp (a,b)) = len_head_of_closure (n+1) a 

65 
 len_head_of_closure n x = (n, x) 

66 

67 

68 
(* earlier occurrence of PVar corresponds to higher de Bruijn index *) 

69 
fun pattern_match args PVar clos = SOME (clos::args) 

70 
 pattern_match args (PConst (c, patterns)) clos = 

71 
let 

72 
val (f, closargs) = strip_closure [] clos 

73 
in 

74 
case f of 

75 
CConst d => 

76 
if c = d then 

77 
pattern_match_list args patterns closargs 

78 
else 

79 
NONE 

80 
 _ => NONE 

81 
end 

82 
and pattern_match_list args [] [] = SOME args 

83 
 pattern_match_list args (p::ps) (c::cs) = 

84 
(case pattern_match args p c of 

85 
NONE => NONE 

86 
 SOME args => pattern_match_list args ps cs) 

87 
 pattern_match_list _ _ _ = NONE 

88 

89 
fun count_patternvars PVar = 1 

90 
 count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps 

91 

92 
fun pattern_key (PConst (c, ps)) = (c, length ps) 

93 
 pattern_key _ = raise (Compile "pattern reduces to variable") 

94 

23663  95 
(*Returns true iff at most 0 .. (free1) occur unbound. therefore 
96 
check_freevars 0 t iff t is closed*) 

97 
fun check_freevars free (Var x) = x < free 

98 
 check_freevars free (Const c) = true 

99 
 check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v 

100 
 check_freevars free (Abs m) = check_freevars (free+1) m 

25217  101 
 check_freevars free (Computed t) = check_freevars free t 
23663  102 

25520  103 
fun compile cache_patterns const_arity eqs = 
23174  104 
let 
25520  105 
fun check p r = if check_freevars p r then () else raise Compile ("unbound variables in rule") 
106 
fun check_guard p (Guard (a,b)) = (check p a; check p b) 

107 
fun clos_of_guard (Guard (a,b)) = (clos_of_term a, clos_of_term b) 

108 
val eqs = map (fn (guards, p, r) => let val pcount = count_patternvars p val _ = map (check_guard pcount) (guards) val _ = check pcount r in 

109 
(pattern_key p, (p, clos_of_term r, map clos_of_guard guards)) end) eqs 

23663  110 
fun merge (k, a) table = prog_struct.update (k, case prog_struct.lookup table k of NONE => [a]  SOME l => a::l) table 
111 
val p = fold merge eqs prog_struct.empty 

23174  112 
in 
23663  113 
Program p 
23174  114 
end 
115 

23663  116 

117 
type state = bool * program * stack * closure 

118 

119 
datatype loopstate = Continue of state  Stop of stack * closure 

120 

121 
fun proj_C (Continue s) = s 

122 
 proj_C _ = raise Match 

123 

24654  124 
exception InterruptedExecution of stack * closure 
125 

23663  126 
fun proj_S (Stop s) = s 
24654  127 
 proj_S (Continue (_,_,s,c)) = (s,c) 
23663  128 

129 
fun cont (Continue _) = true 

130 
 cont _ = false 

23174  131 

32740  132 
val max_reductions = Unsynchronized.ref (NONE : int option) 
24654  133 

23663  134 
fun do_reduction reduce p = 
135 
let 

32740  136 
val s = Unsynchronized.ref (Continue p) 
137 
val counter = Unsynchronized.ref 0 

24654  138 
val _ = case !max_reductions of 
139 
NONE => while cont (!s) do (s := reduce (proj_C (!s))) 

140 
 SOME m => while cont (!s) andalso (!counter < m) do (s := reduce (proj_C (!s)); counter := (!counter) + 1) 

23663  141 
in 
24654  142 
case !max_reductions of 
143 
SOME m => if !counter >= m then raise InterruptedExecution (proj_S (!s)) else proj_S (!s) 

144 
 NONE => proj_S (!s) 

23663  145 
end 
23174  146 

25520  147 
fun match_rules prog n [] clos = NONE 
148 
 match_rules prog n ((p,eq,guards)::rs) clos = 

149 
case pattern_match [] p clos of 

150 
NONE => match_rules prog (n+1) rs clos 

151 
 SOME args => if forall (guard_checks prog args) guards then SOME (Closure (args, eq)) else match_rules prog (n+1) rs clos 

152 
and guard_checks prog args (a,b) = (simp prog (Closure (args, a)) = simp prog (Closure (args, b))) 

153 
and match_closure (p as (Program prog)) clos = 

154 
case len_head_of_closure 0 clos of 

155 
(len, CConst c) => 

156 
(case prog_struct.lookup prog (c, len) of 

157 
NONE => NONE 

158 
 SOME rules => match_rules p 0 rules clos) 

159 
 _ => NONE 

160 

161 
and weak_reduce (false, prog, stack, Closure (e, CApp (a, b))) = Continue (false, prog, SAppL (Closure (e, b), stack), Closure (e, a)) 

23663  162 
 weak_reduce (false, prog, SAppL (b, stack), Closure (e, CAbs m)) = Continue (false, prog, stack, Closure (b::e, m)) 
163 
 weak_reduce (false, prog, stack, Closure (e, CVar n)) = Continue (false, prog, stack, case List.nth (e, n) of CDummy => CVar n  r => r) 

164 
 weak_reduce (false, prog, stack, Closure (e, c as CConst _)) = Continue (false, prog, stack, c) 

165 
 weak_reduce (false, prog, stack, clos) = 

166 
(case match_closure prog clos of 

167 
NONE => Continue (true, prog, stack, clos) 

168 
 SOME r => Continue (false, prog, stack, r)) 

169 
 weak_reduce (true, prog, SAppR (a, stack), b) = Continue (false, prog, stack, CApp (a,b)) 

170 
 weak_reduce (true, prog, s as (SAppL (b, stack)), a) = Continue (false, prog, SAppR (a, stack), b) 

171 
 weak_reduce (true, prog, stack, c) = Stop (stack, c) 

172 

25520  173 
and strong_reduce (false, prog, stack, Closure (e, CAbs m)) = 
24654  174 
(let 
175 
val (stack', wnf) = do_reduction weak_reduce (false, prog, SEmpty, Closure (CDummy::e, m)) 

176 
in 

177 
case stack' of 

178 
SEmpty => Continue (false, prog, SAbs stack, wnf) 

179 
 _ => raise (Run "internal error in strong: weak failed") 

180 
end handle InterruptedExecution state => raise InterruptedExecution (stack, resolve state)) 

23663  181 
 strong_reduce (false, prog, stack, clos as (CApp (u, v))) = Continue (false, prog, SAppL (v, stack), u) 
182 
 strong_reduce (false, prog, stack, clos) = Continue (true, prog, stack, clos) 

183 
 strong_reduce (true, prog, SAbs stack, m) = Continue (false, prog, stack, CAbs m) 

184 
 strong_reduce (true, prog, SAppL (b, stack), a) = Continue (false, prog, SAppR (a, stack), b) 

185 
 strong_reduce (true, prog, SAppR (a, stack), b) = Continue (true, prog, stack, CApp (a, b)) 

186 
 strong_reduce (true, prog, stack, clos) = Stop (stack, clos) 

23174  187 

25520  188 
and simp prog t = 
189 
(let 

190 
val (stack, wnf) = do_reduction weak_reduce (false, prog, SEmpty, t) 

191 
in 

192 
case stack of 

193 
SEmpty => (case do_reduction strong_reduce (false, prog, SEmpty, wnf) of 

194 
(SEmpty, snf) => snf 

195 
 _ => raise (Run "internal error in run: strong failed")) 

196 
 _ => raise (Run "internal error in run: weak failed") 

197 
end handle InterruptedExecution state => resolve state) 

198 

199 

23174  200 
fun run prog t = 
24654  201 
(let 
202 
val (stack, wnf) = do_reduction weak_reduce (false, prog, SEmpty, Closure ([], clos_of_term t)) 

203 
in 

204 
case stack of 

205 
SEmpty => (case do_reduction strong_reduce (false, prog, SEmpty, wnf) of 

206 
(SEmpty, snf) => term_of_clos snf 

207 
 _ => raise (Run "internal error in run: strong failed")) 

208 
 _ => raise (Run "internal error in run: weak failed") 

209 
end handle InterruptedExecution state => term_of_clos (resolve state)) 

23174  210 

23663  211 
fun discard p = () 
23174  212 

23663  213 
end 