diff -r 663235466562 -r b214f21ae396 src/Pure/Tools/am_interpreter.ML --- a/src/Pure/Tools/am_interpreter.ML Tue Jul 12 19:29:52 2005 +0200 +++ b/src/Pure/Tools/am_interpreter.ML Tue Jul 12 21:49:38 2005 +0200 @@ -18,66 +18,6 @@ end -signature BIN_TREE_KEY = -sig - type key - val less : key * key -> bool - val eq : key * key -> bool -end - -signature BIN_TREE = -sig - type key - type 'a t - val tree_of_list : (key * 'a list -> 'b) -> (key * 'a) list -> 'b t - val lookup : 'a t -> key -> 'a Option.option - val empty : 'a t -end - -functor BinTreeFun(Key: BIN_TREE_KEY) : BIN_TREE = -struct - -type key = Key.key - -datatype 'a t = Empty | Node of key * 'a * 'a t * 'a t - -val empty = Empty - -fun insert (k, a) [] = [(k, a)] - | insert (k, a) ((l,b)::x') = - if Key.less (k, l) then (k, a)::(l,b)::x' - else if Key.eq (k, l) then (k, a@b)::x' - else (l,b)::(insert (k, a) x') - -fun sort ((k, a)::x) = insert (k, a) (sort x) - | sort [] = [] - -fun tree_of_sorted_list [] = Empty - | tree_of_sorted_list l = - let - val len = length l - val leftlen = (len - 1) div 2 - val left = tree_of_sorted_list (List.take (l, leftlen)) - val rightl = List.drop (l, leftlen) - val (k, x) = hd rightl - in - Node (k, x, left, tree_of_sorted_list (tl rightl)) - end - -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))) - -fun lookup Empty key = NONE - | lookup (Node (k, x, left, right)) key = - if Key.less (key, k) then - lookup left key - else if Key.less (k, key) then - lookup right key - else - SOME x -end; - -structure IntBinTree = BinTreeFun (type key = int val less = (op <) val eq = (op = : int * int -> bool)); - structure AM_Interpreter :> ABSTRACT_MACHINE = struct datatype term = Var of int | Const of int | App of term * term | Abs of term @@ -88,16 +28,9 @@ | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure -structure IntPairKey = -struct -type key = int * int -fun less ((x1, y1), (x2, y2)) = x1 < x2 orelse (x1 = x2 andalso y1 < y2) -fun eq (k1, k2) = (k1 = k2) -end +structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord); -structure prog_struct = BinTreeFun (IntPairKey) - -type program = ((pattern * closure) list) prog_struct.t +type program = ((pattern * closure) list) prog_struct.table datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack @@ -160,7 +93,7 @@ val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r; (pattern_key p, (p, clos_of_term r)))) eqs in - prog_struct.tree_of_list (fn (key, rules) => rules) eqs + prog_struct.make (map (fn (k, a) => (k, [a])) eqs) end fun match_rules n [] clos = NONE @@ -172,7 +105,7 @@ fun match_closure prog clos = case len_head_of_closure 0 clos of (len, CConst c) => - (case prog_struct.lookup prog (c, len) of + (case prog_struct.lookup (prog, (c, len)) of NONE => NONE | SOME rules => match_rules 0 rules clos) | _ => NONE