1(* Title: Pure/net.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1993 University of Cambridge 4 5Discrimination nets: a data structure for indexing items 6 7From the book 8 E. Charniak, C. K. Riesbeck, D. V. McDermott. 9 Artificial Intelligence Programming. 10 (Lawrence Erlbaum Associates, 1980). [Chapter 14] 11 12match_term no longer treats abstractions as wildcards; instead they match 13only wildcards in patterns. Requires operands to be beta-eta-normal. 14*) 15 16signature NET = 17sig 18 type key 19 val key_of_term: term -> key list 20 val encode_type: typ -> term 21 type 'a net 22 val empty: 'a net 23 val is_empty: 'a net -> bool 24 exception INSERT 25 val insert: ('a * 'a -> bool) -> key list * 'a -> 'a net -> 'a net 26 val insert_term: ('a * 'a -> bool) -> term * 'a -> 'a net -> 'a net 27 val insert_safe: ('a * 'a -> bool) -> key list * 'a -> 'a net -> 'a net 28 val insert_term_safe: ('a * 'a -> bool) -> term * 'a -> 'a net -> 'a net 29 exception DELETE 30 val delete: ('b * 'a -> bool) -> key list * 'b -> 'a net -> 'a net 31 val delete_term: ('b * 'a -> bool) -> term * 'b -> 'a net -> 'a net 32 val delete_safe: ('b * 'a -> bool) -> key list * 'b -> 'a net -> 'a net 33 val delete_term_safe: ('b * 'a -> bool) -> term * 'b -> 'a net -> 'a net 34 val lookup: 'a net -> key list -> 'a list 35 val match_term: 'a net -> term -> 'a list 36 val unify_term: 'a net -> term -> 'a list 37 val entries: 'a net -> 'a list 38 val subtract: ('b * 'a -> bool) -> 'a net -> 'b net -> 'b list 39 val merge: ('a * 'a -> bool) -> 'a net * 'a net -> 'a net 40 val content: 'a net -> 'a list 41end; 42 43structure Net: NET = 44struct 45 46datatype key = CombK | VarK | AtomK of string; 47 48(*Keys are preorder lists of symbols -- Combinations, Vars, Atoms. 49 Any term whose head is a Var is regarded entirely as a Var. 50 Abstractions are also regarded as Vars; this covers eta-conversion 51 and "near" eta-conversions such as %x.?P(?f(x)). 52*) 53fun add_key_of_terms (t, cs) = 54 let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs)) 55 | rands (Const(c,_), cs) = AtomK c :: cs 56 | rands (Free(c,_), cs) = AtomK c :: cs 57 | rands (Bound i, cs) = AtomK (Name.bound i) :: cs 58 in case head_of t of 59 Var _ => VarK :: cs 60 | Abs _ => VarK :: cs 61 | _ => rands(t,cs) 62 end; 63 64(*convert a term to a list of keys*) 65fun key_of_term t = add_key_of_terms (t, []); 66 67(*encode_type -- for indexing purposes*) 68fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts) 69 | encode_type (TFree (a, _)) = Free (a, dummyT) 70 | encode_type (TVar (a, _)) = Var (a, dummyT); 71 72 73(*Trees indexed by key lists: each arc is labelled by a key. 74 Each node contains a list of items, and arcs to children. 75 The empty key addresses the entire net. 76 Lookup functions preserve order in items stored at same level. 77*) 78datatype 'a net = Leaf of 'a list 79 | Net of {comb: 'a net, 80 var: 'a net, 81 atoms: 'a net Symtab.table}; 82 83val empty = Leaf[]; 84fun is_empty (Leaf []) = true | is_empty _ = false; 85val emptynet = Net{comb=empty, var=empty, atoms=Symtab.empty}; 86 87 88(*** Insertion into a discrimination net ***) 89 90exception INSERT; (*duplicate item in the net*) 91 92 93(*Adds item x to the list at the node addressed by the keys. 94 Creates node if not already present. 95 eq is the equality test for items. 96 The empty list of keys generates a Leaf node, others a Net node. 97*) 98fun insert eq (keys,x) net = 99 let fun ins1 ([], Leaf xs) = 100 if member eq xs x then raise INSERT else Leaf(x::xs) 101 | ins1 (keys, Leaf[]) = ins1 (keys, emptynet) (*expand empty...*) 102 | ins1 (CombK :: keys, Net{comb,var,atoms}) = 103 Net{comb=ins1(keys,comb), var=var, atoms=atoms} 104 | ins1 (VarK :: keys, Net{comb,var,atoms}) = 105 Net{comb=comb, var=ins1(keys,var), atoms=atoms} 106 | ins1 (AtomK a :: keys, Net{comb,var,atoms}) = 107 let val atoms' = Symtab.map_default (a, empty) (fn net' => ins1 (keys, net')) atoms; 108 in Net{comb=comb, var=var, atoms=atoms'} end 109 in ins1 (keys,net) end; 110 111fun insert_term eq (t, x) = insert eq (key_of_term t, x); 112 113fun insert_safe eq entry net = insert eq entry net handle INSERT => net; 114fun insert_term_safe eq entry net = insert_term eq entry net handle INSERT => net; 115 116 117(*** Deletion from a discrimination net ***) 118 119exception DELETE; (*missing item in the net*) 120 121(*Create a new Net node if it would be nonempty*) 122fun newnet (args as {comb,var,atoms}) = 123 if is_empty comb andalso is_empty var andalso Symtab.is_empty atoms 124 then empty else Net args; 125 126(*Deletes item x from the list at the node addressed by the keys. 127 Raises DELETE if absent. Collapses the net if possible. 128 eq is the equality test for items. *) 129fun delete eq (keys, x) net = 130 let fun del1 ([], Leaf xs) = 131 if member eq xs x then Leaf (remove eq x xs) 132 else raise DELETE 133 | del1 (keys, Leaf[]) = raise DELETE 134 | del1 (CombK :: keys, Net{comb,var,atoms}) = 135 newnet{comb=del1(keys,comb), var=var, atoms=atoms} 136 | del1 (VarK :: keys, Net{comb,var,atoms}) = 137 newnet{comb=comb, var=del1(keys,var), atoms=atoms} 138 | del1 (AtomK a :: keys, Net{comb,var,atoms}) = 139 let val atoms' = 140 (case Symtab.lookup atoms a of 141 NONE => raise DELETE 142 | SOME net' => 143 (case del1 (keys, net') of 144 Leaf [] => Symtab.delete a atoms 145 | net'' => Symtab.update (a, net'') atoms)) 146 in newnet{comb=comb, var=var, atoms=atoms'} end 147 in del1 (keys,net) end; 148 149fun delete_term eq (t, x) = delete eq (key_of_term t, x); 150 151fun delete_safe eq entry net = delete eq entry net handle DELETE => net; 152fun delete_term_safe eq entry net = delete_term eq entry net handle DELETE => net; 153 154 155(*** Retrieval functions for discrimination nets ***) 156 157(*Return the list of items at the given node, [] if no such node*) 158fun lookup (Leaf xs) [] = xs 159 | lookup (Leaf _) (_ :: _) = [] (*non-empty keys and empty net*) 160 | lookup (Net {comb, ...}) (CombK :: keys) = lookup comb keys 161 | lookup (Net {var, ...}) (VarK :: keys) = lookup var keys 162 | lookup (Net {atoms, ...}) (AtomK a :: keys) = 163 (case Symtab.lookup atoms a of 164 SOME net => lookup net keys 165 | NONE => []); 166 167 168(*Skipping a term in a net. Recursively skip 2 levels if a combination*) 169fun net_skip (Leaf _) nets = nets 170 | net_skip (Net{comb,var,atoms}) nets = 171 fold_rev net_skip (net_skip comb []) (Symtab.fold (cons o #2) atoms (var::nets)); 172 173 174(** Matching and Unification **) 175 176(*conses the linked net, if present, to nets*) 177fun look1 (atoms, a) nets = 178 (case Symtab.lookup atoms a of 179 NONE => nets 180 | SOME net => net :: nets); 181 182(*Return the nodes accessible from the term (cons them before nets) 183 "unif" signifies retrieval for unification rather than matching. 184 Var in net matches any term. 185 Abs or Var in object: if "unif", regarded as wildcard, 186 else matches only a variable in net. 187*) 188fun matching unif t net nets = 189 let fun rands _ (Leaf _, nets) = nets 190 | rands t (Net{comb,atoms,...}, nets) = 191 case t of 192 f$t => fold_rev (matching unif t) (rands f (comb,[])) nets 193 | Const(c,_) => look1 (atoms, c) nets 194 | Free(c,_) => look1 (atoms, c) nets 195 | Bound i => look1 (atoms, Name.bound i) nets 196 | _ => nets 197 in 198 case net of 199 Leaf _ => nets 200 | Net{var,...} => 201 case head_of t of 202 Var _ => if unif then net_skip net nets 203 else var::nets (*only matches Var in net*) 204 (*If "unif" then a var instantiation in the abstraction could allow 205 an eta-reduction, so regard the abstraction as a wildcard.*) 206 | Abs _ => if unif then net_skip net nets 207 else var::nets (*only a Var can match*) 208 | _ => rands t (net, var::nets) (*var could match also*) 209 end; 210 211fun extract_leaves l = maps (fn Leaf xs => xs) l; 212 213(*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*) 214fun match_term net t = 215 extract_leaves (matching false t net []); 216 217(*return items whose key could unify with t*) 218fun unify_term net t = 219 extract_leaves (matching true t net []); 220 221 222(** operations on nets **) 223 224(*subtraction: collect entries of second net that are NOT present in first net*) 225fun subtract eq net1 net2 = 226 let 227 fun subtr (Net _) (Leaf ys) = append ys 228 | subtr (Leaf xs) (Leaf ys) = 229 fold_rev (fn y => if member eq xs y then I else cons y) ys 230 | subtr (Leaf _) (net as Net _) = subtr emptynet net 231 | subtr (Net {comb = comb1, var = var1, atoms = atoms1}) 232 (Net {comb = comb2, var = var2, atoms = atoms2}) = 233 subtr comb1 comb2 234 #> subtr var1 var2 235 #> Symtab.fold (fn (a, net) => 236 subtr (the_default emptynet (Symtab.lookup atoms1 a)) net) atoms2 237 in subtr net1 net2 [] end; 238 239fun entries net = subtract (K false) empty net; 240 241 242(* merge *) 243 244fun cons_fst x (xs, y) = (x :: xs, y); 245 246fun dest (Leaf xs) = map (pair []) xs 247 | dest (Net {comb, var, atoms}) = 248 map (cons_fst CombK) (dest comb) @ 249 map (cons_fst VarK) (dest var) @ 250 maps (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms); 251 252fun merge eq (net1, net2) = 253 fold (insert_safe eq) (dest net2) net1; (* FIXME non-canonical merge order!?! *) 254 255fun content net = map #2 (dest net); 256 257end; 258