src/Pure/Tools/am_interpreter.ML
changeset 16781 663235466562
child 16782 b214f21ae396
     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