src/Pure/net.ML
author blanchet
Mon May 19 23:43:53 2014 +0200 (2014-05-19)
changeset 57008 10f68b83b474
parent 56137 af71fb1cb31f
child 63614 676ba20db063
permissions -rw-r--r--
use E 1.8's auto scheduler option
     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   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
    41 end;
    42 
    43 structure Net: NET =
    44 struct
    45 
    46 datatype 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 *)
    53 fun 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*)
    65 fun key_of_term t = add_key_of_terms (t, []);
    66 
    67 (*encode_type -- for indexing purposes*)
    68 fun 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 *)
    78 datatype 'a net = Leaf of 'a list
    79                 | Net of {comb: 'a net,
    80                           var: 'a net,
    81                           atoms: 'a net Symtab.table};
    82 
    83 val empty = Leaf[];
    84 fun is_empty (Leaf []) = true | is_empty _ = false;
    85 val emptynet = Net{comb=empty, var=empty, atoms=Symtab.empty};
    86 
    87 
    88 (*** Insertion into a discrimination net ***)
    89 
    90 exception 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 *)
    98 fun 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 
   111 fun insert_term eq (t, x) = insert eq (key_of_term t, x);
   112 
   113 fun insert_safe eq entry net = insert eq entry net handle INSERT => net;
   114 fun insert_term_safe eq entry net = insert_term eq entry net handle INSERT => net;
   115 
   116 
   117 (*** Deletion from a discrimination net ***)
   118 
   119 exception DELETE;       (*missing item in the net*)
   120 
   121 (*Create a new Net node if it would be nonempty*)
   122 fun 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. *)
   129 fun 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 
   149 fun delete_term eq (t, x) = delete eq (key_of_term t, x);
   150 
   151 fun delete_safe eq entry net = delete eq entry net handle DELETE => net;
   152 fun delete_term_safe eq entry net = delete_term eq entry net handle DELETE => net;
   153 
   154 
   155 (*** Retrieval functions for discrimination nets ***)
   156 
   157 exception ABSENT;
   158 
   159 fun the_atom atoms a =
   160   (case Symtab.lookup atoms a of
   161     NONE => raise ABSENT
   162   | SOME net => net);
   163 
   164 (*Return the list of items at the given node, [] if no such node*)
   165 fun lookup (Leaf xs) [] = xs
   166   | lookup (Leaf _) (_ :: _) = []  (*non-empty keys and empty net*)
   167   | lookup (Net {comb, var, atoms}) (CombK :: keys) = lookup comb keys
   168   | lookup (Net {comb, var, atoms}) (VarK :: keys) = lookup var keys
   169   | lookup (Net {comb, var, atoms}) (AtomK a :: keys) =
   170       lookup (the_atom atoms a) keys handle ABSENT => [];
   171 
   172 
   173 (*Skipping a term in a net.  Recursively skip 2 levels if a combination*)
   174 fun net_skip (Leaf _) nets = nets
   175   | net_skip (Net{comb,var,atoms}) nets =
   176       fold_rev net_skip (net_skip comb []) (Symtab.fold (cons o #2) atoms (var::nets));
   177 
   178 
   179 (** Matching and Unification **)
   180 
   181 (*conses the linked net, if present, to nets*)
   182 fun look1 (atoms, a) nets =
   183   the_atom atoms a :: nets handle ABSENT => nets;
   184 
   185 (*Return the nodes accessible from the term (cons them before nets)
   186   "unif" signifies retrieval for unification rather than matching.
   187   Var in net matches any term.
   188   Abs or Var in object: if "unif", regarded as wildcard,
   189                                    else matches only a variable in net.
   190 *)
   191 fun matching unif t net nets =
   192   let fun rands _ (Leaf _, nets) = nets
   193         | rands t (Net{comb,atoms,...}, nets) =
   194             case t of
   195                 f$t => fold_rev (matching unif t) (rands f (comb,[])) nets
   196               | Const(c,_) => look1 (atoms, c) nets
   197               | Free(c,_)  => look1 (atoms, c) nets
   198               | Bound i    => look1 (atoms, Name.bound i) nets
   199               | _          => nets
   200   in
   201      case net of
   202          Leaf _ => nets
   203        | Net{var,...} =>
   204              case head_of t of
   205                  Var _ => if unif then net_skip net nets
   206                           else var::nets           (*only matches Var in net*)
   207   (*If "unif" then a var instantiation in the abstraction could allow
   208     an eta-reduction, so regard the abstraction as a wildcard.*)
   209                | Abs _ => if unif then net_skip net nets
   210                           else var::nets           (*only a Var can match*)
   211                | _ => rands t (net, var::nets)  (*var could match also*)
   212   end;
   213 
   214 fun extract_leaves l = maps (fn Leaf xs => xs) l;
   215 
   216 (*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
   217 fun match_term net t =
   218     extract_leaves (matching false t net []);
   219 
   220 (*return items whose key could unify with t*)
   221 fun unify_term net t =
   222     extract_leaves (matching true t net []);
   223 
   224 
   225 (** operations on nets **)
   226 
   227 (*subtraction: collect entries of second net that are NOT present in first net*)
   228 fun subtract eq net1 net2 =
   229   let
   230     fun subtr (Net _) (Leaf ys) = append ys
   231       | subtr (Leaf xs) (Leaf ys) =
   232           fold_rev (fn y => if member eq xs y then I else cons y) ys
   233       | subtr (Leaf _) (net as Net _) = subtr emptynet net
   234       | subtr (Net {comb = comb1, var = var1, atoms = atoms1})
   235             (Net {comb = comb2, var = var2, atoms = atoms2}) =
   236           subtr comb1 comb2
   237           #> subtr var1 var2
   238           #> Symtab.fold (fn (a, net) =>
   239             subtr (the_default emptynet (Symtab.lookup atoms1 a)) net) atoms2
   240   in subtr net1 net2 [] end;
   241 
   242 fun entries net = subtract (K false) empty net;
   243 
   244 
   245 (* merge *)
   246 
   247 fun cons_fst x (xs, y) = (x :: xs, y);
   248 
   249 fun dest (Leaf xs) = map (pair []) xs
   250   | dest (Net {comb, var, atoms}) =
   251       map (cons_fst CombK) (dest comb) @
   252       map (cons_fst VarK) (dest var) @
   253       maps (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms);
   254 
   255 fun merge eq (net1, net2) =
   256   fold (insert_safe eq) (dest net2) net1;  (* FIXME non-canonical merge order!?! *)
   257 
   258 fun content net = map #2 (dest net);
   259 
   260 end;