# HG changeset patch # User wenzelm # Date 1120639302 -7200 # Node ID 479f7ac538b581d349b9971079ebecec24da9309 # Parent c28599f981f2fb7f35f5866fdc88d033fd1e0a23 use Symtab.table instead of ordered lists; diff -r c28599f981f2 -r 479f7ac538b5 src/Pure/net.ML --- a/src/Pure/net.ML Wed Jul 06 10:41:41 2005 +0200 +++ b/src/Pure/net.ML Wed Jul 06 10:41:42 2005 +0200 @@ -14,6 +14,8 @@ only wildcards in patterns. Requires operands to be beta-eta-normal. *) +val time_string_of_bound = time_init (); + signature NET = sig type key @@ -39,6 +41,7 @@ (*Bound variables*) fun string_of_bound i = "*B*" ^ chr (i div 256) ^ chr (i mod 256); +val string_of_bound = time time_string_of_bound string_of_bound; (*Keys are preorder lists of symbols -- Combinations, Vars, Atoms. Any term whose head is a Var is regarded entirely as a Var. @@ -62,17 +65,17 @@ (*Trees indexed by key lists: each arc is labelled by a key. Each node contains a list of items, and arcs to children. - Keys in the association list (alist) are stored in ascending order. The empty key addresses the entire net. Lookup functions preserve order in items stored at same level. *) datatype 'a net = Leaf of 'a list | Net of {comb: 'a net, var: 'a net, - alist: (string * 'a net) list}; + atoms: 'a net Symtab.table}; val empty = Leaf[]; -val emptynet = Net{comb=empty, var=empty, alist=[]}; +fun is_empty (Leaf []) = true | is_empty _ = false; +val emptynet = Net{comb=empty, var=empty, atoms=Symtab.empty}; (*** Insertion into a discrimination net ***) @@ -89,20 +92,15 @@ let fun ins1 ([], Leaf xs) = if member eq xs x then raise INSERT else Leaf(x::xs) | ins1 (keys, Leaf[]) = ins1 (keys, emptynet) (*expand empty...*) - | ins1 (CombK :: keys, Net{comb,var,alist}) = - Net{comb=ins1(keys,comb), var=var, alist=alist} - | ins1 (VarK :: keys, Net{comb,var,alist}) = - Net{comb=comb, var=ins1(keys,var), alist=alist} - | ins1 (AtomK a :: keys, Net{comb,var,alist}) = - let fun newpair net = (a, ins1(keys,net)) - fun inslist [] = [newpair empty] - | inslist ((b, netb) :: alist) = - (case fast_string_ord (a, b) of - EQUAL => newpair netb :: alist - | LESS => (*absent, insert in alist*) - newpair empty :: (b,netb) :: alist - | GREATER => (b,netb) :: inslist alist) - in Net{comb=comb, var=var, alist= inslist alist} end + | ins1 (CombK :: keys, Net{comb,var,atoms}) = + Net{comb=ins1(keys,comb), var=var, atoms=atoms} + | ins1 (VarK :: keys, Net{comb,var,atoms}) = + Net{comb=comb, var=ins1(keys,var), atoms=atoms} + | ins1 (AtomK a :: keys, Net{comb,var,atoms}) = + let + val net' = if_none (Symtab.lookup (atoms, a)) empty; + val atoms' = Symtab.update ((a, ins1(keys,net')), atoms); + in Net{comb=comb, var=var, atoms=atoms'} end in ins1 (keys,net) end; fun insert_term ((t,x), net, eq) = insert((key_of_term t, x), net, eq); @@ -112,12 +110,9 @@ exception DELETE; (*missing item in the net*) (*Create a new Net node if it would be nonempty*) -fun newnet {comb=Leaf[], var=Leaf[], alist=[]} = empty - | newnet {comb,var,alist} = Net{comb=comb, var=var, alist=alist}; - -(*add new (b,net) pair to the alist provided net is nonempty*) -fun conspair((b, Leaf[]), alist) = alist - | conspair((b, net), alist) = (b, net) :: alist; +fun newnet (args as {comb,var,atoms}) = + if is_empty comb andalso is_empty var andalso Symtab.is_empty atoms + then empty else Net args; (*Deletes item x from the list at the node addressed by the keys. Raises DELETE if absent. Collapses the net if possible. @@ -127,19 +122,19 @@ if member eq xs x then Leaf (remove eq x xs) else raise DELETE | del1 (keys, Leaf[]) = raise DELETE - | del1 (CombK :: keys, Net{comb,var,alist}) = - newnet{comb=del1(keys,comb), var=var, alist=alist} - | del1 (VarK :: keys, Net{comb,var,alist}) = - newnet{comb=comb, var=del1(keys,var), alist=alist} - | del1 (AtomK a :: keys, Net{comb,var,alist}) = - let fun newpair net = (a, del1(keys,net)) - fun dellist [] = raise DELETE - | dellist((b, netb) :: alist) = - (case fast_string_ord (a, b) of - EQUAL => conspair(newpair netb, alist) - | LESS => (*absent*) raise DELETE - | GREATER => (b,netb) :: dellist alist) - in newnet{comb=comb, var=var, alist= dellist alist} end + | del1 (CombK :: keys, Net{comb,var,atoms}) = + newnet{comb=del1(keys,comb), var=var, atoms=atoms} + | del1 (VarK :: keys, Net{comb,var,atoms}) = + newnet{comb=comb, var=del1(keys,var), atoms=atoms} + | del1 (AtomK a :: keys, Net{comb,var,atoms}) = + let val atoms' = + (case Symtab.lookup (atoms, a) of + NONE => raise DELETE + | SOME net' => + (case del1 (keys, net') of + Leaf [] => Symtab.delete a atoms + | net'' => Symtab.update ((a, net''), atoms))) + in newnet{comb=comb, var=var, atoms=atoms'} end in del1 (keys,net) end; fun delete_term ((t,x), net, eq) = delete((key_of_term t, x), net, eq); @@ -147,37 +142,32 @@ (*** Retrieval functions for discrimination nets ***) -exception OASSOC; +exception ABSENT; -(*Ordered association list lookup*) -fun oassoc ([], a) = raise OASSOC - | oassoc ((b,x)::pairs, a) = - (case fast_string_ord (a, b) of - EQUAL => x - | LESS => raise OASSOC - | GREATER => oassoc(pairs,a)); +fun the_atom atoms a = + (case Symtab.lookup (atoms, a) of + NONE => raise ABSENT + | SOME net => net); (*Return the list of items at the given node, [] if no such node*) fun lookup (Leaf(xs), []) = xs | lookup (Leaf _, _::_) = [] (*non-empty keys and empty net*) - | lookup (Net{comb,var,alist}, CombK :: keys) = lookup(comb,keys) - | lookup (Net{comb,var,alist}, VarK :: keys) = lookup(var,keys) - | lookup (Net{comb,var,alist}, AtomK a :: keys) = - lookup(oassoc(alist,a),keys) handle OASSOC => []; + | lookup (Net{comb,var,atoms}, CombK :: keys) = lookup(comb,keys) + | lookup (Net{comb,var,atoms}, VarK :: keys) = lookup(var,keys) + | lookup (Net{comb,var,atoms}, AtomK a :: keys) = + lookup (the_atom atoms a, keys) handle ABSENT => []; (*Skipping a term in a net. Recursively skip 2 levels if a combination*) fun net_skip (Leaf _, nets) = nets - | net_skip (Net{comb,var,alist}, nets) = - foldr net_skip - (foldr (fn ((_,net), nets) => net::nets) (var::nets) alist) - (net_skip (comb,[])) + | net_skip (Net{comb,var,atoms}, nets) = + foldr net_skip (Symtab.fold (cons o #2) atoms (var::nets)) (net_skip (comb,[])); (** Matching and Unification**) (*conses the linked net, if present, to nets*) -fun look1 (alist, a) nets = - oassoc(alist,a) :: nets handle OASSOC => nets; +fun look1 (atoms, a) nets = + the_atom atoms a :: nets handle ABSENT => nets; (*Return the nodes accessible from the term (cons them before nets) "unif" signifies retrieval for unification rather than matching. @@ -187,12 +177,12 @@ *) fun matching unif t (net,nets) = let fun rands _ (Leaf _, nets) = nets - | rands t (Net{comb,alist,...}, nets) = + | rands t (Net{comb,atoms,...}, nets) = case t of f$t => foldr (matching unif t) nets (rands f (comb,[])) - | Const(c,_) => look1 (alist, c) nets - | Free(c,_) => look1 (alist, c) nets - | Bound i => look1 (alist, string_of_bound i) nets + | Const(c,_) => look1 (atoms, c) nets + | Free(c,_) => look1 (atoms, c) nets + | Bound i => look1 (atoms, string_of_bound i) nets | _ => nets in case net of @@ -224,10 +214,11 @@ fun cons_fst x (xs, y) = (x :: xs, y); fun dest (Leaf xs) = map (pair []) xs - | dest (Net {comb, var, alist}) = + | dest (Net {comb, var, atoms}) = map (cons_fst CombK) (dest comb) @ map (cons_fst VarK) (dest var) @ - List.concat (map (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) alist); + List.concat (map (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) + (Symtab.dest atoms)); (** merge **)