23174

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