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