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