24584

1 
(* Title: Tools/Compute_Oracle/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 .. (free1) 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
