src/Pure/net.ML
author wenzelm
Wed Jun 02 11:09:26 2010 +0200 (2010-06-02 ago)
changeset 37251 72c7e636067b
parent 33371 d74dc1b54930
child 37523 40c352510065
permissions -rw-r--r--
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
     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   val insert_safe: ('a * 'a -> bool) -> key list * 'a -> 'a net -> 'a net
    26   val insert_term_safe: ('a * 'a -> bool) -> term * 'a -> 'a net -> 'a net
    27   exception DELETE
    28   val delete: ('b * 'a -> bool) -> key list * 'b -> 'a net -> 'a net
    29   val delete_term: ('b * 'a -> bool) -> term * 'b -> 'a net -> 'a net
    30   val delete_safe: ('b * 'a -> bool) -> key list * 'b -> 'a net -> 'a net
    31   val delete_term_safe: ('b * 'a -> bool) -> term * 'b -> 'a net -> 'a net
    32   val lookup: 'a net -> key list -> 'a list
    33   val match_term: 'a net -> term -> 'a list
    34   val unify_term: 'a net -> term -> 'a list
    35   val entries: 'a net -> 'a list
    36   val subtract: ('b * 'a -> bool) -> 'a net -> 'b net -> 'b list
    37   val merge: ('a * 'a -> bool) -> 'a net * 'a net -> 'a net
    38   val content: 'a net -> 'a list
    39 end;
    40 
    41 structure Net: NET =
    42 struct
    43 
    44 datatype key = CombK | VarK | AtomK of string;
    45 
    46 (*Keys are preorder lists of symbols -- Combinations, Vars, Atoms.
    47   Any term whose head is a Var is regarded entirely as a Var.
    48   Abstractions are also regarded as Vars;  this covers eta-conversion
    49     and "near" eta-conversions such as %x.?P(?f(x)).
    50 *)
    51 fun add_key_of_terms (t, cs) =
    52   let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs))
    53         | rands (Const(c,_), cs) = AtomK c :: cs
    54         | rands (Free(c,_),  cs) = AtomK c :: cs
    55         | rands (Bound i,  cs)   = AtomK (Name.bound i) :: cs
    56   in case (head_of t) of
    57       Var _ => VarK :: cs
    58     | Abs _ => VarK :: cs
    59     | _     => rands(t,cs)
    60   end;
    61 
    62 (*convert a term to a list of keys*)
    63 fun key_of_term t = add_key_of_terms (t, []);
    64 
    65 
    66 (*Trees indexed by key lists: each arc is labelled by a key.
    67   Each node contains a list of items, and arcs to children.
    68   The empty key addresses the entire net.
    69   Lookup functions preserve order in items stored at same level.
    70 *)
    71 datatype 'a net = Leaf of 'a list
    72                 | Net of {comb: 'a net,
    73                           var: 'a net,
    74                           atoms: 'a net Symtab.table};
    75 
    76 val empty = Leaf[];
    77 fun is_empty (Leaf []) = true | is_empty _ = false;
    78 val emptynet = Net{comb=empty, var=empty, atoms=Symtab.empty};
    79 
    80 
    81 (*** Insertion into a discrimination net ***)
    82 
    83 exception INSERT;       (*duplicate item in the net*)
    84 
    85 
    86 (*Adds item x to the list at the node addressed by the keys.
    87   Creates node if not already present.
    88   eq is the equality test for items.
    89   The empty list of keys generates a Leaf node, others a Net node.
    90 *)
    91 fun insert eq (keys,x) net =
    92   let fun ins1 ([], Leaf xs) =
    93             if member eq xs x then  raise INSERT  else Leaf(x::xs)
    94         | ins1 (keys, Leaf[]) = ins1 (keys, emptynet)   (*expand empty...*)
    95         | ins1 (CombK :: keys, Net{comb,var,atoms}) =
    96             Net{comb=ins1(keys,comb), var=var, atoms=atoms}
    97         | ins1 (VarK :: keys, Net{comb,var,atoms}) =
    98             Net{comb=comb, var=ins1(keys,var), atoms=atoms}
    99         | ins1 (AtomK a :: keys, Net{comb,var,atoms}) =
   100             let
   101               val net' = the_default empty (Symtab.lookup atoms a);
   102               val atoms' = Symtab.update (a, ins1 (keys, net')) atoms;
   103             in  Net{comb=comb, var=var, atoms=atoms'}  end
   104   in  ins1 (keys,net)  end;
   105 
   106 fun insert_term eq (t, x) = insert eq (key_of_term t, x);
   107 
   108 fun insert_safe eq entry net = insert eq entry net handle INSERT => net;
   109 fun insert_term_safe eq entry net = insert_term eq entry net handle INSERT => net;
   110 
   111 
   112 (*** Deletion from a discrimination net ***)
   113 
   114 exception DELETE;       (*missing item in the net*)
   115 
   116 (*Create a new Net node if it would be nonempty*)
   117 fun newnet (args as {comb,var,atoms}) =
   118   if is_empty comb andalso is_empty var andalso Symtab.is_empty atoms
   119   then empty else Net args;
   120 
   121 (*Deletes item x from the list at the node addressed by the keys.
   122   Raises DELETE if absent.  Collapses the net if possible.
   123   eq is the equality test for items. *)
   124 fun delete eq (keys, x) net =
   125   let fun del1 ([], Leaf xs) =
   126             if member eq xs x then Leaf (remove eq x xs)
   127             else raise DELETE
   128         | del1 (keys, Leaf[]) = raise DELETE
   129         | del1 (CombK :: keys, Net{comb,var,atoms}) =
   130             newnet{comb=del1(keys,comb), var=var, atoms=atoms}
   131         | del1 (VarK :: keys, Net{comb,var,atoms}) =
   132             newnet{comb=comb, var=del1(keys,var), atoms=atoms}
   133         | del1 (AtomK a :: keys, Net{comb,var,atoms}) =
   134             let val atoms' =
   135               (case Symtab.lookup atoms a of
   136                 NONE => raise DELETE
   137               | SOME net' =>
   138                   (case del1 (keys, net') of
   139                     Leaf [] => Symtab.delete a atoms
   140                   | net'' => Symtab.update (a, net'') atoms))
   141             in  newnet{comb=comb, var=var, atoms=atoms'}  end
   142   in  del1 (keys,net)  end;
   143 
   144 fun delete_term eq (t, x) = delete eq (key_of_term t, x);
   145 
   146 fun delete_safe eq entry net = delete eq entry net handle DELETE => net;
   147 fun delete_term_safe eq entry net = delete_term eq entry net handle DELETE => net;
   148 
   149 
   150 (*** Retrieval functions for discrimination nets ***)
   151 
   152 exception ABSENT;
   153 
   154 fun the_atom atoms a =
   155   (case Symtab.lookup atoms a of
   156     NONE => raise ABSENT
   157   | SOME net => net);
   158 
   159 (*Return the list of items at the given node, [] if no such node*)
   160 fun lookup (Leaf xs) [] = xs
   161   | lookup (Leaf _) (_ :: _) = []  (*non-empty keys and empty net*)
   162   | lookup (Net {comb, var, atoms}) (CombK :: keys) = lookup comb keys
   163   | lookup (Net {comb, var, atoms}) (VarK :: keys) = lookup var keys
   164   | lookup (Net {comb, var, atoms}) (AtomK a :: keys) =
   165       lookup (the_atom atoms a) keys handle ABSENT => [];
   166 
   167 
   168 (*Skipping a term in a net.  Recursively skip 2 levels if a combination*)
   169 fun net_skip (Leaf _) nets = nets
   170   | net_skip (Net{comb,var,atoms}) nets =
   171       fold_rev net_skip (net_skip comb []) (Symtab.fold (cons o #2) atoms (var::nets));
   172 
   173 
   174 (** Matching and Unification **)
   175 
   176 (*conses the linked net, if present, to nets*)
   177 fun look1 (atoms, a) nets =
   178   the_atom atoms a :: nets handle ABSENT => nets;
   179 
   180 (*Return the nodes accessible from the term (cons them before nets)
   181   "unif" signifies retrieval for unification rather than matching.
   182   Var in net matches any term.
   183   Abs or Var in object: if "unif", regarded as wildcard,
   184                                    else matches only a variable in net.
   185 *)
   186 fun matching unif t net nets =
   187   let fun rands _ (Leaf _, nets) = nets
   188         | rands t (Net{comb,atoms,...}, nets) =
   189             case t of
   190                 f$t => fold_rev (matching unif t) (rands f (comb,[])) nets
   191               | Const(c,_) => look1 (atoms, c) nets
   192               | Free(c,_)  => look1 (atoms, c) nets
   193               | Bound i    => look1 (atoms, Name.bound i) nets
   194               | _          => nets
   195   in
   196      case net of
   197          Leaf _ => nets
   198        | Net{var,...} =>
   199              case head_of t of
   200                  Var _ => if unif then net_skip net nets
   201                           else var::nets           (*only matches Var in net*)
   202   (*If "unif" then a var instantiation in the abstraction could allow
   203     an eta-reduction, so regard the abstraction as a wildcard.*)
   204                | Abs _ => if unif then net_skip net nets
   205                           else var::nets           (*only a Var can match*)
   206                | _ => rands t (net, var::nets)  (*var could match also*)
   207   end;
   208 
   209 fun extract_leaves l = maps (fn Leaf xs => xs) l;
   210 
   211 (*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
   212 fun match_term net t =
   213     extract_leaves (matching false t net []);
   214 
   215 (*return items whose key could unify with t*)
   216 fun unify_term net t =
   217     extract_leaves (matching true t net []);
   218 
   219 
   220 (** operations on nets **)
   221 
   222 (*subtraction: collect entries of second net that are NOT present in first net*)
   223 fun subtract eq net1 net2 =
   224   let
   225     fun subtr (Net _) (Leaf ys) = append ys
   226       | subtr (Leaf xs) (Leaf ys) =
   227           fold_rev (fn y => if member eq xs y then I else cons y) ys
   228       | subtr (Leaf _) (net as Net _) = subtr emptynet net
   229       | subtr (Net {comb = comb1, var = var1, atoms = atoms1})
   230             (Net {comb = comb2, var = var2, atoms = atoms2}) =
   231           subtr comb1 comb2
   232           #> subtr var1 var2
   233           #> Symtab.fold (fn (a, net) =>
   234             subtr (the_default emptynet (Symtab.lookup atoms1 a)) net) atoms2
   235   in subtr net1 net2 [] end;
   236 
   237 fun entries net = subtract (K false) empty net;
   238 
   239 
   240 (* merge *)
   241 
   242 fun cons_fst x (xs, y) = (x :: xs, y);
   243 
   244 fun dest (Leaf xs) = map (pair []) xs
   245   | dest (Net {comb, var, atoms}) =
   246       map (cons_fst CombK) (dest comb) @
   247       map (cons_fst VarK) (dest var) @
   248       maps (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms);
   249 
   250 fun merge eq (net1, net2) = fold (insert_safe eq) (dest net2) net1;
   251 
   252 fun content net = map #2 (dest net);
   253 
   254 end;