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