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