src/Pure/net.ML
author wenzelm
Thu May 31 23:47:36 2007 +0200 (2007-05-31 ago)
changeset 23178 07ba6b58b3d2
parent 20080 1398063aa271
child 29606 fedb8be05f24
permissions -rw-r--r--
simplified/unified list fold;
     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   val content: 'a net -> 'a list
    36 end;
    37 
    38 structure Net: NET =
    39 struct
    40 
    41 datatype key = CombK | VarK | AtomK of string;
    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 (Name.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   The empty key addresses the entire net.
    66   Lookup functions preserve order in items stored at same level.
    67 *)
    68 datatype 'a net = Leaf of 'a list
    69                 | Net of {comb: 'a net,
    70                           var: 'a net,
    71                           atoms: 'a net Symtab.table};
    72 
    73 val empty = Leaf[];
    74 fun is_empty (Leaf []) = true | is_empty _ = false;
    75 val emptynet = Net{comb=empty, var=empty, atoms=Symtab.empty};
    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 eq (keys,x) net =
    89   let fun ins1 ([], Leaf xs) =
    90             if member eq xs x then  raise INSERT  else Leaf(x::xs)
    91         | ins1 (keys, Leaf[]) = ins1 (keys, emptynet)   (*expand empty...*)
    92         | ins1 (CombK :: keys, Net{comb,var,atoms}) =
    93             Net{comb=ins1(keys,comb), var=var, atoms=atoms}
    94         | ins1 (VarK :: keys, Net{comb,var,atoms}) =
    95             Net{comb=comb, var=ins1(keys,var), atoms=atoms}
    96         | ins1 (AtomK a :: keys, Net{comb,var,atoms}) =
    97             let
    98               val net' = the_default empty (Symtab.lookup atoms a);
    99               val atoms' = Symtab.update (a, ins1 (keys, net')) atoms;
   100             in  Net{comb=comb, var=var, atoms=atoms'}  end
   101   in  ins1 (keys,net)  end;
   102 
   103 fun insert_safe eq entry net = insert eq entry net handle INSERT => net;
   104 fun insert_term eq (t, x) = insert eq (key_of_term t, x);
   105 
   106 
   107 (*** Deletion from a discrimination net ***)
   108 
   109 exception DELETE;       (*missing item in the net*)
   110 
   111 (*Create a new Net node if it would be nonempty*)
   112 fun newnet (args as {comb,var,atoms}) =
   113   if is_empty comb andalso is_empty var andalso Symtab.is_empty atoms
   114   then empty else Net args;
   115 
   116 (*Deletes item x from the list at the node addressed by the keys.
   117   Raises DELETE if absent.  Collapses the net if possible.
   118   eq is the equality test for items. *)
   119 fun delete eq (keys, x) net =
   120   let fun del1 ([], Leaf xs) =
   121             if member eq xs x then Leaf (remove eq x xs)
   122             else raise DELETE
   123         | del1 (keys, Leaf[]) = raise DELETE
   124         | del1 (CombK :: keys, Net{comb,var,atoms}) =
   125             newnet{comb=del1(keys,comb), var=var, atoms=atoms}
   126         | del1 (VarK :: keys, Net{comb,var,atoms}) =
   127             newnet{comb=comb, var=del1(keys,var), atoms=atoms}
   128         | del1 (AtomK a :: keys, Net{comb,var,atoms}) =
   129             let val atoms' =
   130               (case Symtab.lookup atoms a of
   131                 NONE => raise DELETE
   132               | SOME net' =>
   133                   (case del1 (keys, net') of
   134                     Leaf [] => Symtab.delete a atoms
   135                   | net'' => Symtab.update (a, net'') atoms))
   136             in  newnet{comb=comb, var=var, atoms=atoms'}  end
   137   in  del1 (keys,net)  end;
   138 
   139 fun delete_term eq (t, x) = delete eq (key_of_term t, x);
   140 
   141 
   142 (*** Retrieval functions for discrimination nets ***)
   143 
   144 exception ABSENT;
   145 
   146 fun the_atom atoms a =
   147   (case Symtab.lookup atoms a of
   148     NONE => raise ABSENT
   149   | SOME net => net);
   150 
   151 (*Return the list of items at the given node, [] if no such node*)
   152 fun lookup (Leaf xs) [] = xs
   153   | lookup (Leaf _) (_ :: _) = []  (*non-empty keys and empty net*)
   154   | lookup (Net {comb, var, atoms}) (CombK :: keys) = lookup comb keys
   155   | lookup (Net {comb, var, atoms}) (VarK :: keys) = lookup var keys
   156   | lookup (Net {comb, var, atoms}) (AtomK a :: keys) =
   157       lookup (the_atom atoms a) keys handle ABSENT => [];
   158 
   159 
   160 (*Skipping a term in a net.  Recursively skip 2 levels if a combination*)
   161 fun net_skip (Leaf _) nets = nets
   162   | net_skip (Net{comb,var,atoms}) nets =
   163       fold_rev net_skip (net_skip comb []) (Symtab.fold (cons o #2) atoms (var::nets));
   164 
   165 
   166 (** Matching and Unification **)
   167 
   168 (*conses the linked net, if present, to nets*)
   169 fun look1 (atoms, a) nets =
   170   the_atom atoms a :: nets handle ABSENT => nets;
   171 
   172 (*Return the nodes accessible from the term (cons them before nets)
   173   "unif" signifies retrieval for unification rather than matching.
   174   Var in net matches any term.
   175   Abs or Var in object: if "unif", regarded as wildcard,
   176                                    else matches only a variable in net.
   177 *)
   178 fun matching unif t net nets =
   179   let fun rands _ (Leaf _, nets) = nets
   180         | rands t (Net{comb,atoms,...}, nets) =
   181             case t of
   182                 f$t => fold_rev (matching unif t) (rands f (comb,[])) nets
   183               | Const(c,_) => look1 (atoms, c) nets
   184               | Free(c,_)  => look1 (atoms, c) nets
   185               | Bound i    => look1 (atoms, Name.bound i) nets
   186               | _          => nets
   187   in
   188      case net of
   189          Leaf _ => nets
   190        | Net{var,...} =>
   191              case head_of t of
   192                  Var _ => if unif then net_skip net nets
   193                           else var::nets           (*only matches Var in net*)
   194   (*If "unif" then a var instantiation in the abstraction could allow
   195     an eta-reduction, so regard the abstraction as a wildcard.*)
   196                | Abs _ => if unif then net_skip net nets
   197                           else var::nets           (*only a Var can match*)
   198                | _ => rands t (net, var::nets)  (*var could match also*)
   199   end;
   200 
   201 fun extract_leaves l = maps (fn Leaf xs => xs) l;
   202 
   203 (*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
   204 fun match_term net t =
   205     extract_leaves (matching false t net []);
   206 
   207 (*return items whose key could unify with t*)
   208 fun unify_term net t =
   209     extract_leaves (matching true t net []);
   210 
   211 
   212 (** operations on nets **)
   213 
   214 (*subtraction: collect entries of second net that are NOT present in first net*)
   215 fun subtract eq net1 net2 =
   216   let
   217     fun subtr (Net _) (Leaf ys) = append ys
   218       | subtr (Leaf xs) (Leaf ys) =
   219           fold_rev (fn y => if member eq xs y then I else cons y) ys
   220       | subtr (Leaf _) (net as Net _) = subtr emptynet net
   221       | subtr (Net {comb = comb1, var = var1, atoms = atoms1})
   222             (Net {comb = comb2, var = var2, atoms = atoms2}) =
   223           subtr comb1 comb2
   224           #> subtr var1 var2
   225           #> Symtab.fold (fn (a, net) =>
   226             subtr (the_default emptynet (Symtab.lookup atoms1 a)) net) atoms2
   227   in subtr net1 net2 [] end;
   228 
   229 fun entries net = subtract (K false) empty net;
   230 
   231 
   232 (* merge *)
   233 
   234 fun cons_fst x (xs, y) = (x :: xs, y);
   235 
   236 fun dest (Leaf xs) = map (pair []) xs
   237   | dest (Net {comb, var, atoms}) =
   238       map (cons_fst CombK) (dest comb) @
   239       map (cons_fst VarK) (dest var) @
   240       maps (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms);
   241 
   242 fun merge eq (net1, net2) = fold (insert_safe eq) (dest net2) net1;
   243 
   244 fun content net = map #2 (dest net);
   245 
   246 end;