src/Pure/Tools/am_interpreter.ML
changeset 16782 b214f21ae396
parent 16781 663235466562
child 16842 5979c46853d1
     1.1 --- a/src/Pure/Tools/am_interpreter.ML	Tue Jul 12 19:29:52 2005 +0200
     1.2 +++ b/src/Pure/Tools/am_interpreter.ML	Tue Jul 12 21:49:38 2005 +0200
     1.3 @@ -18,66 +18,6 @@
     1.4  
     1.5  end
     1.6  
     1.7 -signature BIN_TREE_KEY =
     1.8 -sig
     1.9 -  type key
    1.10 -  val less : key * key -> bool
    1.11 -  val eq : key * key -> bool
    1.12 -end
    1.13 -
    1.14 -signature BIN_TREE = 
    1.15 -sig
    1.16 -    type key    
    1.17 -    type 'a t
    1.18 -    val tree_of_list : (key * 'a list -> 'b) -> (key * 'a) list -> 'b t
    1.19 -    val lookup : 'a t -> key -> 'a Option.option
    1.20 -    val empty : 'a t
    1.21 -end
    1.22 -
    1.23 -functor BinTreeFun(Key: BIN_TREE_KEY) : BIN_TREE  =
    1.24 -struct
    1.25 -
    1.26 -type key = Key.key
    1.27 -
    1.28 -datatype 'a t = Empty | Node of key * 'a * 'a t * 'a t 
    1.29 -
    1.30 -val empty = Empty
    1.31 -
    1.32 -fun insert (k, a) [] = [(k, a)]
    1.33 -  | insert (k, a) ((l,b)::x') = 
    1.34 -    if Key.less (k, l) then (k, a)::(l,b)::x'
    1.35 -    else if Key.eq (k, l) then (k, a@b)::x'
    1.36 -    else (l,b)::(insert (k, a) x')
    1.37 -
    1.38 -fun sort ((k, a)::x) = insert (k, a) (sort x)
    1.39 -  | sort [] = []
    1.40 -
    1.41 -fun tree_of_sorted_list [] = Empty
    1.42 -  | tree_of_sorted_list l = 
    1.43 -    let
    1.44 -	val len = length l
    1.45 -	val leftlen = (len - 1) div 2
    1.46 -	val left = tree_of_sorted_list (List.take (l, leftlen))
    1.47 -	val rightl = List.drop (l, leftlen)
    1.48 -	val (k, x) = hd rightl
    1.49 -    in
    1.50 -	Node (k, x, left, tree_of_sorted_list (tl rightl))
    1.51 -    end
    1.52 -	
    1.53 -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.54 -		 
    1.55 -fun lookup Empty key = NONE
    1.56 -  | lookup (Node (k, x, left, right)) key =
    1.57 -    if Key.less (key, k) then
    1.58 -	lookup left key
    1.59 -    else if Key.less (k, key) then
    1.60 -	lookup right key
    1.61 -    else
    1.62 -	SOME x
    1.63 -end;
    1.64 -
    1.65 -structure IntBinTree = BinTreeFun (type key = int val less = (op <) val eq = (op = : int * int -> bool));
    1.66 -
    1.67  structure AM_Interpreter :> ABSTRACT_MACHINE = struct
    1.68  
    1.69  datatype term = Var of int | Const of int | App of term * term | Abs of term
    1.70 @@ -88,16 +28,9 @@
    1.71  		 | CApp of closure * closure | CAbs of closure 
    1.72  		 | Closure of (closure list) * closure 
    1.73  
    1.74 -structure IntPairKey = 
    1.75 -struct
    1.76 -type key = int * int
    1.77 -fun less ((x1, y1), (x2, y2)) = x1 < x2 orelse (x1 = x2 andalso y1 < y2)
    1.78 -fun eq (k1, k2) = (k1 = k2)
    1.79 -end
    1.80 +structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
    1.81  
    1.82 -structure prog_struct = BinTreeFun (IntPairKey)
    1.83 -
    1.84 -type program = ((pattern * closure) list) prog_struct.t
    1.85 +type program = ((pattern * closure) list) prog_struct.table
    1.86  
    1.87  datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
    1.88  
    1.89 @@ -160,7 +93,7 @@
    1.90  	val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r; 
    1.91  				     (pattern_key p, (p, clos_of_term r)))) eqs
    1.92      in
    1.93 -	prog_struct.tree_of_list (fn (key, rules) => rules) eqs
    1.94 +	prog_struct.make (map (fn (k, a) => (k, [a])) eqs)
    1.95      end	
    1.96  
    1.97  fun match_rules n [] clos = NONE
    1.98 @@ -172,7 +105,7 @@
    1.99  fun match_closure prog clos = 
   1.100      case len_head_of_closure 0 clos of
   1.101  	(len, CConst c) =>
   1.102 -	(case prog_struct.lookup prog (c, len) of
   1.103 +	(case prog_struct.lookup (prog, (c, len)) of
   1.104  	    NONE => NONE
   1.105  	  | SOME rules => match_rules 0 rules clos)
   1.106        | _ => NONE