1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/Tools/am_interpreter.ML Tue Jul 12 19:29:52 2005 +0200
1.3 @@ -0,0 +1,227 @@
1.4 +(* Title: Pure/Tools/am_interpreter.ML
1.5 + ID: $Id$
1.6 + Author: Steven Obua
1.7 +*)
1.8 +
1.9 +signature ABSTRACT_MACHINE = sig
1.10 +datatype term = Var of int | Const of int | App of term * term | Abs of term
1.11 +
1.12 +datatype pattern = PVar | PConst of int * (pattern list)
1.13 +
1.14 +type program
1.15 +
1.16 +exception Compile of string;
1.17 +val compile : (pattern * term) list -> program
1.18 +
1.19 +exception Run of string;
1.20 +val run : program -> term -> term
1.21 +
1.22 +end
1.23 +
1.24 +signature BIN_TREE_KEY =
1.25 +sig
1.26 + type key
1.27 + val less : key * key -> bool
1.28 + val eq : key * key -> bool
1.29 +end
1.30 +
1.31 +signature BIN_TREE =
1.32 +sig
1.33 + type key
1.34 + type 'a t
1.35 + val tree_of_list : (key * 'a list -> 'b) -> (key * 'a) list -> 'b t
1.36 + val lookup : 'a t -> key -> 'a Option.option
1.37 + val empty : 'a t
1.38 +end
1.39 +
1.40 +functor BinTreeFun(Key: BIN_TREE_KEY) : BIN_TREE =
1.41 +struct
1.42 +
1.43 +type key = Key.key
1.44 +
1.45 +datatype 'a t = Empty | Node of key * 'a * 'a t * 'a t
1.46 +
1.47 +val empty = Empty
1.48 +
1.49 +fun insert (k, a) [] = [(k, a)]
1.50 + | insert (k, a) ((l,b)::x') =
1.51 + if Key.less (k, l) then (k, a)::(l,b)::x'
1.52 + else if Key.eq (k, l) then (k, a@b)::x'
1.53 + else (l,b)::(insert (k, a) x')
1.54 +
1.55 +fun sort ((k, a)::x) = insert (k, a) (sort x)
1.56 + | sort [] = []
1.57 +
1.58 +fun tree_of_sorted_list [] = Empty
1.59 + | tree_of_sorted_list l =
1.60 + let
1.61 + val len = length l
1.62 + val leftlen = (len - 1) div 2
1.63 + val left = tree_of_sorted_list (List.take (l, leftlen))
1.64 + val rightl = List.drop (l, leftlen)
1.65 + val (k, x) = hd rightl
1.66 + in
1.67 + Node (k, x, left, tree_of_sorted_list (tl rightl))
1.68 + end
1.69 +
1.70 +fun tree_of_list f l = tree_of_sorted_list (map (fn (k, a) => (k, f (k,a))) (sort (map (fn (k, a) => (k, [a])) l)))
1.71 +
1.72 +fun lookup Empty key = NONE
1.73 + | lookup (Node (k, x, left, right)) key =
1.74 + if Key.less (key, k) then
1.75 + lookup left key
1.76 + else if Key.less (k, key) then
1.77 + lookup right key
1.78 + else
1.79 + SOME x
1.80 +end;
1.81 +
1.82 +structure IntBinTree = BinTreeFun (type key = int val less = (op <) val eq = (op = : int * int -> bool));
1.83 +
1.84 +structure AM_Interpreter :> ABSTRACT_MACHINE = struct
1.85 +
1.86 +datatype term = Var of int | Const of int | App of term * term | Abs of term
1.87 +
1.88 +datatype pattern = PVar | PConst of int * (pattern list)
1.89 +
1.90 +datatype closure = CVar of int | CConst of int
1.91 + | CApp of closure * closure | CAbs of closure
1.92 + | Closure of (closure list) * closure
1.93 +
1.94 +structure IntPairKey =
1.95 +struct
1.96 +type key = int * int
1.97 +fun less ((x1, y1), (x2, y2)) = x1 < x2 orelse (x1 = x2 andalso y1 < y2)
1.98 +fun eq (k1, k2) = (k1 = k2)
1.99 +end
1.100 +
1.101 +structure prog_struct = BinTreeFun (IntPairKey)
1.102 +
1.103 +type program = ((pattern * closure) list) prog_struct.t
1.104 +
1.105 +datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
1.106 +
1.107 +exception Compile of string;
1.108 +exception Run of string;
1.109 +
1.110 +fun clos_of_term (Var x) = CVar x
1.111 + | clos_of_term (Const c) = CConst c
1.112 + | clos_of_term (App (u, v)) = CApp (clos_of_term u, clos_of_term v)
1.113 + | clos_of_term (Abs u) = CAbs (clos_of_term u)
1.114 +
1.115 +fun term_of_clos (CVar x) = Var x
1.116 + | term_of_clos (CConst c) = Const c
1.117 + | term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
1.118 + | term_of_clos (CAbs u) = Abs (term_of_clos u)
1.119 + | term_of_clos (Closure (e, u)) = raise (Run "internal error: closure in normalized term found")
1.120 +
1.121 +fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
1.122 + | strip_closure args x = (x, args)
1.123 +
1.124 +fun len_head_of_closure n (CApp (a,b)) = len_head_of_closure (n+1) a
1.125 + | len_head_of_closure n x = (n, x)
1.126 +
1.127 +
1.128 +(* earlier occurrence of PVar corresponds to higher de Bruijn index *)
1.129 +fun pattern_match args PVar clos = SOME (clos::args)
1.130 + | pattern_match args (PConst (c, patterns)) clos =
1.131 + let
1.132 + val (f, closargs) = strip_closure [] clos
1.133 + in
1.134 + case f of
1.135 + CConst d =>
1.136 + if c = d then
1.137 + pattern_match_list args patterns closargs
1.138 + else
1.139 + NONE
1.140 + | _ => NONE
1.141 + end
1.142 +and pattern_match_list args [] [] = SOME args
1.143 + | pattern_match_list args (p::ps) (c::cs) =
1.144 + (case pattern_match args p c of
1.145 + NONE => NONE
1.146 + | SOME args => pattern_match_list args ps cs)
1.147 + | pattern_match_list _ _ _ = NONE
1.148 +
1.149 +(* Returns true iff at most 0 .. (free-1) occur unbound. therefore check_freevars 0 t iff t is closed *)
1.150 +fun check_freevars free (Var x) = x < free
1.151 + | check_freevars free (Const c) = true
1.152 + | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
1.153 + | check_freevars free (Abs m) = check_freevars (free+1) m
1.154 +
1.155 +fun count_patternvars PVar = 1
1.156 + | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
1.157 +
1.158 +fun pattern_key (PConst (c, ps)) = (c, length ps)
1.159 + | pattern_key _ = raise (Compile "pattern reduces to variable")
1.160 +
1.161 +fun compile eqs =
1.162 + let
1.163 + val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r;
1.164 + (pattern_key p, (p, clos_of_term r)))) eqs
1.165 + in
1.166 + prog_struct.tree_of_list (fn (key, rules) => rules) eqs
1.167 + end
1.168 +
1.169 +fun match_rules n [] clos = NONE
1.170 + | match_rules n ((p,eq)::rs) clos =
1.171 + case pattern_match [] p clos of
1.172 + NONE => match_rules (n+1) rs clos
1.173 + | SOME args => SOME (Closure (args, eq))
1.174 +
1.175 +fun match_closure prog clos =
1.176 + case len_head_of_closure 0 clos of
1.177 + (len, CConst c) =>
1.178 + (case prog_struct.lookup prog (c, len) of
1.179 + NONE => NONE
1.180 + | SOME rules => match_rules 0 rules clos)
1.181 + | _ => NONE
1.182 +
1.183 +fun lift n (c as (CConst _)) = c
1.184 + | lift n (v as CVar m) = if m < n then v else CVar (m+1)
1.185 + | lift n (CAbs t) = CAbs (lift (n+1) t)
1.186 + | lift n (CApp (a,b)) = CApp (lift n a, lift n b)
1.187 + | lift n (Closure (e, a)) = Closure (lift_env n e, lift (n+(length e)) a)
1.188 +and lift_env n e = map (lift n) e
1.189 +
1.190 +fun weak prog stack (Closure (e, CApp (a, b))) = weak prog (SAppL (Closure (e, b), stack)) (Closure (e, a))
1.191 + | weak prog (SAppL (b, stack)) (Closure (e, CAbs m)) = weak prog stack (Closure (b::e, m))
1.192 + | weak prog stack (Closure (e, CVar n)) = weak prog stack (List.nth (e, n) handle Subscript => (CVar (n-(length e))))
1.193 + | weak prog stack (Closure (e, c as CConst _)) = weak prog stack c
1.194 + | weak prog stack clos =
1.195 + case match_closure prog clos of
1.196 + NONE => weak_last prog stack clos
1.197 + | SOME r => weak prog stack r
1.198 +and weak_last prog (SAppR (a, stack)) b = weak prog stack (CApp (a,b))
1.199 + | weak_last prog (s as (SAppL (b, stack))) a = weak prog (SAppR (a, stack)) b
1.200 + | weak_last prog stack c = (stack, c)
1.201 +
1.202 +fun strong prog stack (Closure (e, CAbs m)) =
1.203 + let
1.204 + val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
1.205 + in
1.206 + case stack' of
1.207 + SEmpty => strong prog (SAbs stack) wnf
1.208 + | _ => raise (Run "internal error in strong: weak failed")
1.209 + end
1.210 + | strong prog stack (clos as (CApp (u, v))) = strong prog (SAppL (v, stack)) u
1.211 + | strong prog stack clos = strong_last prog stack clos
1.212 +and strong_last prog (SAbs stack) m = strong prog stack (CAbs m)
1.213 + | strong_last prog (SAppL (b, stack)) a = strong prog (SAppR (a, stack)) b
1.214 + | strong_last prog (SAppR (a, stack)) b = strong_last prog stack (CApp (a, b))
1.215 + | strong_last prog stack clos = (stack, clos)
1.216 +
1.217 +fun run prog t =
1.218 + let
1.219 + val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
1.220 + in
1.221 + case stack of
1.222 + SEmpty => (case strong prog SEmpty wnf of
1.223 + (SEmpty, snf) => term_of_clos snf
1.224 + | _ => raise (Run "internal error in run: strong failed"))
1.225 + | _ => raise (Run "internal error in run: weak failed")
1.226 + end
1.227 +
1.228 +end
1.229 +
1.230 +structure AbstractMachine = AM_Interpreter