src/Pure/net.ML
author wenzelm
Mon Jul 04 17:07:11 2005 +0200 (2005-07-04)
changeset 16677 6c038c13fd0f
parent 15574 b1d1b5bfc464
child 16686 cc735c10b44d
permissions -rw-r--r--
use fast_string_ord;
     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   type 'a net
    21   exception DELETE and INSERT
    22   val delete: (key list * 'a) * 'b net * ('a * 'b -> bool) -> 'b net
    23   val delete_term: (term * 'a) * 'b net * ('a * 'b -> bool) -> 'b net
    24   val empty: 'a net
    25   val insert: (key list * 'a) * 'a net * ('a*'a -> bool) -> 'a net
    26   val insert_term:   (term * 'a) * 'a net * ('a*'a -> bool) -> 'a net
    27   val lookup: 'a net * key list -> 'a list
    28   val match_term: 'a net -> term -> 'a list
    29   val key_of_term: term -> key list
    30   val unify_term: 'a net -> term -> 'a list
    31   val dest: 'a net -> (key list * 'a) list
    32   val merge: 'a net * 'a net * ('a*'a -> bool) -> 'a net
    33   end;
    34 
    35 structure Net : NET =
    36 struct
    37 
    38 datatype key = CombK | VarK | AtomK of string;
    39 
    40 (*Bound variables*)
    41 fun string_of_bound i = "*B*" ^ chr (i div 256) ^ chr (i mod 256);
    42 
    43 (*Keys are preorder lists of symbols -- Combinations, Vars, Atoms.
    44   Any term whose head is a Var is regarded entirely as a Var.
    45   Abstractions are also regarded as Vars;  this covers eta-conversion
    46     and "near" eta-conversions such as %x.?P(?f(x)).
    47 *)
    48 fun add_key_of_terms (t, cs) =
    49   let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs))
    50         | rands (Const(c,_), cs) = AtomK c :: cs
    51         | rands (Free(c,_),  cs) = AtomK c :: cs
    52         | rands (Bound i,  cs)   = AtomK (string_of_bound i) :: cs
    53   in case (head_of t) of
    54       Var _ => VarK :: cs
    55     | Abs _ => VarK :: cs
    56     | _     => rands(t,cs)
    57   end;
    58 
    59 (*convert a term to a list of keys*)
    60 fun key_of_term t = add_key_of_terms (t, []);
    61 
    62 
    63 (*Trees indexed by key lists: each arc is labelled by a key.
    64   Each node contains a list of items, and arcs to children.
    65   Keys in the association list (alist) are stored in ascending order.
    66   The empty key addresses the entire net.
    67   Lookup functions preserve order in items stored at same level.
    68 *)
    69 datatype 'a net = Leaf of 'a list
    70                 | Net of {comb: 'a net,
    71                           var: 'a net,
    72                           alist: (string * 'a net) list};
    73 
    74 val empty = Leaf[];
    75 val emptynet = Net{comb=empty, var=empty, alist=[]};
    76 
    77 
    78 (*** Insertion into a discrimination net ***)
    79 
    80 exception INSERT;       (*duplicate item in the net*)
    81 
    82 
    83 (*Adds item x to the list at the node addressed by the keys.
    84   Creates node if not already present.
    85   eq is the equality test for items.
    86   The empty list of keys generates a Leaf node, others a Net node.
    87 *)
    88 fun insert ((keys,x), net, eq) =
    89   let fun ins1 ([], Leaf xs) =
    90             if gen_mem eq (x,xs) then  raise INSERT  else Leaf(x::xs)
    91         | ins1 (keys, Leaf[]) = ins1 (keys, emptynet)   (*expand empty...*)
    92         | ins1 (CombK :: keys, Net{comb,var,alist}) =
    93             Net{comb=ins1(keys,comb), var=var, alist=alist}
    94         | ins1 (VarK :: keys, Net{comb,var,alist}) =
    95             Net{comb=comb, var=ins1(keys,var), alist=alist}
    96         | ins1 (AtomK a :: keys, Net{comb,var,alist}) =
    97             let fun newpair net = (a, ins1(keys,net))
    98                 fun inslist [] = [newpair empty]
    99                   | inslist ((b, netb) :: alist) =
   100                       (case fast_string_ord (a, b) of
   101                         EQUAL => newpair netb :: alist
   102                       | LESS => (*absent, insert in alist*)
   103                           newpair empty :: (b,netb) :: alist
   104                       | GREATER => (b,netb) :: inslist alist)
   105             in  Net{comb=comb, var=var, alist= inslist alist}  end
   106   in  ins1 (keys,net)  end;
   107 
   108 fun insert_term ((t,x), net, eq) = insert((key_of_term t, x), net, eq);
   109 
   110 (*** Deletion from a discrimination net ***)
   111 
   112 exception DELETE;       (*missing item in the net*)
   113 
   114 (*Create a new Net node if it would be nonempty*)
   115 fun newnet {comb=Leaf[], var=Leaf[], alist=[]} = empty
   116   | newnet {comb,var,alist} = Net{comb=comb, var=var, alist=alist};
   117 
   118 (*add new (b,net) pair to the alist provided net is nonempty*)
   119 fun conspair((b, Leaf[]), alist) = alist
   120   | conspair((b, net), alist)    = (b, net) :: alist;
   121 
   122 (*Deletes item x from the list at the node addressed by the keys.
   123   Raises DELETE if absent.  Collapses the net if possible.
   124   eq is the equality test for items. *)
   125 fun delete ((keys, x), net, eq) =
   126   let fun del1 ([], Leaf xs) =
   127             if gen_mem eq (x,xs) then Leaf (gen_rem (eq o swap) (xs,x))
   128             else raise DELETE
   129         | del1 (keys, Leaf[]) = raise DELETE
   130         | del1 (CombK :: keys, Net{comb,var,alist}) =
   131             newnet{comb=del1(keys,comb), var=var, alist=alist}
   132         | del1 (VarK :: keys, Net{comb,var,alist}) =
   133             newnet{comb=comb, var=del1(keys,var), alist=alist}
   134         | del1 (AtomK a :: keys, Net{comb,var,alist}) =
   135             let fun newpair net = (a, del1(keys,net))
   136                 fun dellist [] = raise DELETE
   137                   | dellist((b, netb) :: alist) =
   138                       (case fast_string_ord (a, b) of
   139                         EQUAL => conspair(newpair netb, alist)
   140                       | LESS => (*absent*) raise DELETE
   141                       | GREATER => (b,netb) :: dellist alist)
   142             in  newnet{comb=comb, var=var, alist= dellist alist}  end
   143   in  del1 (keys,net)  end;
   144 
   145 fun delete_term ((t,x), net, eq) = delete((key_of_term t, x), net, eq);
   146 
   147 
   148 (*** Retrieval functions for discrimination nets ***)
   149 
   150 exception OASSOC;
   151 
   152 (*Ordered association list lookup*)
   153 fun oassoc ([], a) = raise OASSOC
   154   | oassoc ((b,x)::pairs, a) =
   155       (case fast_string_ord (a, b) of
   156         EQUAL => x
   157       | LESS => raise OASSOC
   158       | GREATER => oassoc(pairs,a));
   159 
   160 (*Return the list of items at the given node, [] if no such node*)
   161 fun lookup (Leaf(xs), []) = xs
   162   | lookup (Leaf _, _::_) = []  (*non-empty keys and empty net*)
   163   | lookup (Net{comb,var,alist}, CombK :: keys) = lookup(comb,keys)
   164   | lookup (Net{comb,var,alist}, VarK :: keys) = lookup(var,keys)
   165   | lookup (Net{comb,var,alist}, AtomK a :: keys) =
   166       lookup(oassoc(alist,a),keys)  handle  OASSOC => [];
   167 
   168 
   169 (*Skipping a term in a net.  Recursively skip 2 levels if a combination*)
   170 fun net_skip (Leaf _, nets) = nets
   171   | net_skip (Net{comb,var,alist}, nets) =
   172     foldr net_skip
   173           (foldr (fn ((_,net), nets) => net::nets) (var::nets) alist)
   174           (net_skip (comb,[]))
   175 
   176 (** Matching and Unification**)
   177 
   178 (*conses the linked net, if present, to nets*)
   179 fun look1 (alist, a) nets =
   180        oassoc(alist,a) :: nets  handle  OASSOC => 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 *)
   188 fun matching unif t (net,nets) =
   189   let fun rands _ (Leaf _, nets) = nets
   190         | rands t (Net{comb,alist,...}, nets) =
   191             case t of
   192                 f$t => foldr (matching unif t) nets (rands f (comb,[]))
   193               | Const(c,_) => look1 (alist, c) nets
   194               | Free(c,_)  => look1 (alist, c) nets
   195               | Bound i    => look1 (alist, string_of_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 
   211 fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l);
   212 
   213 (*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
   214 fun match_term net t =
   215     extract_leaves (matching false t (net,[]));
   216 
   217 (*return items whose key could unify with t*)
   218 fun unify_term net t =
   219     extract_leaves (matching true t (net,[]));
   220 
   221 
   222 (** dest **)
   223 
   224 fun cons_fst x (xs, y) = (x :: xs, y);
   225 
   226 fun dest (Leaf xs) = map (pair []) xs
   227   | dest (Net {comb, var, alist}) =
   228       map (cons_fst CombK) (dest comb) @
   229       map (cons_fst VarK) (dest var) @
   230       List.concat (map (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) alist);
   231 
   232 
   233 (** merge **)
   234 
   235 fun add eq (net, keys_x) =
   236   insert (keys_x, net, eq) handle INSERT => net;
   237 
   238 fun merge (net1, net2, eq) =
   239   Library.foldl (add eq) (net1, dest net2);
   240 
   241 
   242 end;