24584

1 
(* Title: Tools/Compute_Oracle/am_interpreter.ML

23174

2 
ID: $Id$


3 
Author: Steven Obua


4 
*)


5 

24654

6 
signature AM_BARRAS =


7 
sig


8 
include ABSTRACT_MACHINE


9 
val max_reductions : int option ref


10 
end


11 


12 
structure AM_Interpreter : AM_BARRAS = struct

23174

13 

23663

14 
open AbstractMachine;

23174

15 

23663

16 
datatype closure = CDummy  CVar of int  CConst of int

23174

17 
 CApp of closure * closure  CAbs of closure


18 
 Closure of (closure list) * closure


19 


20 
structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);


21 

25520

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

23174

23 


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


25 


26 
fun clos_of_term (Var x) = CVar x


27 
 clos_of_term (Const c) = CConst c


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


29 
 clos_of_term (Abs u) = CAbs (clos_of_term u)

25217

30 
 clos_of_term (Computed t) = clos_of_term t

23174

31 


32 
fun term_of_clos (CVar x) = Var x


33 
 term_of_clos (CConst c) = Const c


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


35 
 term_of_clos (CAbs u) = Abs (term_of_clos u)


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

23663

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

23174

38 

24654

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


40 
 resolve_closure closures (CConst c) = CConst c


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


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


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


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


45 


46 
fun resolve_closure' c = resolve_closure [] c


47 


48 
fun resolve_stack tm SEmpty = tm


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


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


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


52 


53 
fun resolve (stack, closure) =


54 
let


55 
val _ = writeln "start resolving"


56 
val t = resolve_stack (resolve_closure' closure) stack


57 
val _ = writeln "finished resolving"


58 
in


59 
t


60 
end


61 

23174

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


63 
 strip_closure args x = (x, args)


64 


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


66 
 len_head_of_closure n x = (n, x)


67 


68 


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


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


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


72 
let


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


74 
in


75 
case f of


76 
CConst d =>


77 
if c = d then


78 
pattern_match_list args patterns closargs


79 
else


80 
NONE


81 
 _ => NONE


82 
end


83 
and pattern_match_list args [] [] = SOME args


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


85 
(case pattern_match args p c of


86 
NONE => NONE


87 
 SOME args => pattern_match_list args ps cs)


88 
 pattern_match_list _ _ _ = NONE


89 


90 
fun count_patternvars PVar = 1


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


92 


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


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


95 

23663

96 
(*Returns true iff at most 0 .. (free1) occur unbound. therefore


97 
check_freevars 0 t iff t is closed*)


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


99 
 check_freevars free (Const c) = true


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


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

25217

102 
 check_freevars free (Computed t) = check_freevars free t

23663

103 

25520

104 
fun compile cache_patterns const_arity eqs =

23174

105 
let

25520

106 
fun check p r = if check_freevars p r then () else raise Compile ("unbound variables in rule")


107 
fun check_guard p (Guard (a,b)) = (check p a; check p b)


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


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


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

23663

111 
fun merge (k, a) table = prog_struct.update (k, case prog_struct.lookup table k of NONE => [a]  SOME l => a::l) table


112 
val p = fold merge eqs prog_struct.empty

23174

113 
in

23663

114 
Program p

23174

115 
end


116 

23663

117 


118 
type state = bool * program * stack * closure


119 


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


121 


122 
fun proj_C (Continue s) = s


123 
 proj_C _ = raise Match


124 

24654

125 
exception InterruptedExecution of stack * closure


126 

23663

127 
fun proj_S (Stop s) = s

24654

128 
 proj_S (Continue (_,_,s,c)) = (s,c)

23663

129 


130 
fun cont (Continue _) = true


131 
 cont _ = false

23174

132 

24654

133 
val max_reductions = ref (NONE : int option)


134 

23663

135 
fun do_reduction reduce p =


136 
let


137 
val s = ref (Continue p)

24654

138 
val counter = ref 0


139 
val _ = case !max_reductions of


140 
NONE => while cont (!s) do (s := reduce (proj_C (!s)))


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

23663

142 
in

24654

143 
case !max_reductions of


144 
SOME m => if !counter >= m then raise InterruptedExecution (proj_S (!s)) else proj_S (!s)


145 
 NONE => proj_S (!s)

23663

146 
end

23174

147 

25520

148 
fun match_rules prog n [] clos = NONE


149 
 match_rules prog n ((p,eq,guards)::rs) clos =


150 
case pattern_match [] p clos of


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


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


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


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


155 
case len_head_of_closure 0 clos of


156 
(len, CConst c) =>


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


158 
NONE => NONE


159 
 SOME rules => match_rules p 0 rules clos)


160 
 _ => NONE


161 


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

23663

163 
 weak_reduce (false, prog, SAppL (b, stack), Closure (e, CAbs m)) = Continue (false, prog, stack, Closure (b::e, m))


164 
 weak_reduce (false, prog, stack, Closure (e, CVar n)) = Continue (false, prog, stack, case List.nth (e, n) of CDummy => CVar n  r => r)


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


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


167 
(case match_closure prog clos of


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


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


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


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


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


173 

25520

174 
and strong_reduce (false, prog, stack, Closure (e, CAbs m)) =

24654

175 
(let


176 
val (stack', wnf) = do_reduction weak_reduce (false, prog, SEmpty, Closure (CDummy::e, m))


177 
in


178 
case stack' of


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


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


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

23663

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


183 
 strong_reduce (false, prog, stack, clos) = Continue (true, prog, stack, clos)


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


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


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


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

23174

188 

25520

189 
and simp prog t =


190 
(let


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


192 
in


193 
case stack of


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


195 
(SEmpty, snf) => snf


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


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


198 
end handle InterruptedExecution state => resolve state)


199 


200 

23174

201 
fun run prog t =

24654

202 
(let


203 
val (stack, wnf) = do_reduction weak_reduce (false, prog, SEmpty, Closure ([], clos_of_term t))


204 
in


205 
case stack of


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


207 
(SEmpty, snf) => term_of_clos snf


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


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


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

23174

211 

23663

212 
fun discard p = ()

23174

213 

23663

214 
end
