src/Pure/net.ML
author berghofe
Wed Oct 31 19:37:04 2001 +0100 (2001-10-31)
changeset 11998 b14e7686ce84
parent 7943 e31a3c0c2c1e
child 12319 cb3ea5750c3b
permissions -rw-r--r--
- enter_thmx -> enter_thms
- improved naming of theorems: enter_thms now takes functions pre_name and post_name
as arguments
     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   type 'a net
    21   exception DELETE and INSERT
    22   val delete: (key list * 'a) * 'a net * ('a*'a -> bool) -> 'a net
    23   val delete_term:   (term * 'a) * 'a net * ('a*'a -> bool) -> 'a net
    24   val empty: 'a net
    25   val insert: (key list * 'a) * 'a net * ('a*'a -> bool) -> 'a net
    26   val insert_term:   (term * 'a) * 'a net * ('a*'a -> bool) -> 'a net
    27   val lookup: 'a net * key list -> 'a list
    28   val match_term: 'a net -> term -> 'a list
    29   val key_of_term: term -> key list
    30   val unify_term: 'a net -> term -> 'a list
    31   val dest: 'a net -> (key list * 'a) list
    32   val merge: 'a net * 'a net * ('a*'a -> bool) -> 'a net
    33   end;
    34 
    35 
    36 structure Net : NET = 
    37 struct
    38 
    39 datatype key = CombK | VarK | AtomK of string;
    40 
    41 (*Bound variables*)
    42 fun string_of_bound i = "*B*" ^ chr (i div 256) ^ chr (i mod 256);
    43 
    44 (*Keys are preorder lists of symbols -- Combinations, Vars, Atoms.
    45   Any term whose head is a Var is regarded entirely as a Var.
    46   Abstractions are also regarded as Vars;  this covers eta-conversion
    47     and "near" eta-conversions such as %x.?P(?f(x)).
    48 *)
    49 fun add_key_of_terms (t, cs) = 
    50   let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs))
    51 	| rands (Const(c,_), cs) = AtomK c :: cs
    52 	| rands (Free(c,_),  cs) = AtomK c :: cs
    53 	| rands (Bound i,  cs)   = AtomK (string_of_bound i) :: cs
    54   in case (head_of t) of
    55       Var _ => VarK :: cs
    56     | Abs _ => VarK :: cs
    57     | _     => rands(t,cs)
    58   end;
    59 
    60 (*convert a term to a list of keys*)
    61 fun key_of_term t = add_key_of_terms (t, []);
    62 
    63 
    64 (*Trees indexed by key lists: each arc is labelled by a key.
    65   Each node contains a list of items, and arcs to children.
    66   Keys in the association list (alist) are stored in ascending order.
    67   The empty key addresses the entire net.
    68   Lookup functions preserve order in items stored at same level.
    69 *)
    70 datatype 'a net = Leaf of 'a list
    71 		| Net of {comb: 'a net, 
    72 			  var: 'a net,
    73 			  alist: (string * 'a net) list};
    74 
    75 val empty = Leaf[];
    76 val emptynet = Net{comb=empty, var=empty, alist=[]};
    77 
    78 
    79 (*** Insertion into a discrimination net ***)
    80 
    81 exception INSERT;	(*duplicate item in the net*)
    82 
    83 
    84 (*Adds item x to the list at the node addressed by the keys.
    85   Creates node if not already present.
    86   eq is the equality test for items. 
    87   The empty list of keys generates a Leaf node, others a Net node.
    88 *)
    89 fun insert ((keys,x), net, eq) =
    90   let fun ins1 ([], Leaf xs) = 
    91             if gen_mem eq (x,xs) then  raise INSERT  else Leaf(x::xs)
    92         | ins1 (keys, Leaf[]) = ins1 (keys, emptynet)   (*expand empty...*)
    93         | ins1 (CombK :: keys, Net{comb,var,alist}) =
    94 	    Net{comb=ins1(keys,comb), var=var, alist=alist}
    95 	| ins1 (VarK :: keys, Net{comb,var,alist}) =
    96 	    Net{comb=comb, var=ins1(keys,var), alist=alist}
    97 	| ins1 (AtomK a :: keys, Net{comb,var,alist}) =
    98 	    let fun newpair net = (a, ins1(keys,net)) 
    99 		fun inslist [] = [newpair empty]
   100 		  | inslist((b: string, netb) :: alist) =
   101 		      if a=b then newpair netb :: alist
   102 		      else if a<b then (*absent, ins1ert in alist*)
   103 			  newpair empty :: (b,netb) :: alist
   104 		      else (*a>b*) (b,netb) :: inslist alist
   105 	    in  Net{comb=comb, var=var, alist= inslist alist}  end
   106   in  ins1 (keys,net)  end;
   107 
   108 fun insert_term ((t,x), net, eq) = insert((key_of_term t, x), net, eq);
   109 
   110 (*** Deletion from a discrimination net ***)
   111 
   112 exception DELETE;	(*missing item in the net*)
   113 
   114 (*Create a new Net node if it would be nonempty*)
   115 fun newnet {comb=Leaf[], var=Leaf[], alist=[]} = empty
   116   | newnet {comb,var,alist} = Net{comb=comb, var=var, alist=alist};
   117 
   118 (*add new (b,net) pair to the alist provided net is nonempty*)
   119 fun conspair((b, Leaf[]), alist) = alist
   120   | conspair((b, net), alist)    = (b, net) :: alist;
   121 
   122 (*Deletes item x from the list at the node addressed by the keys.
   123   Raises DELETE if absent.  Collapses the net if possible.
   124   eq is the equality test for items. *)
   125 fun delete ((keys, x), net, eq) = 
   126   let fun del1 ([], Leaf xs) =
   127             if gen_mem eq (x,xs) then Leaf (gen_rem eq (xs,x))
   128             else raise DELETE
   129 	| del1 (keys, Leaf[]) = raise DELETE
   130 	| del1 (CombK :: keys, Net{comb,var,alist}) =
   131 	    newnet{comb=del1(keys,comb), var=var, alist=alist}
   132 	| del1 (VarK :: keys, Net{comb,var,alist}) =
   133 	    newnet{comb=comb, var=del1(keys,var), alist=alist}
   134 	| del1 (AtomK a :: keys, Net{comb,var,alist}) =
   135 	    let fun newpair net = (a, del1(keys,net)) 
   136 		fun dellist [] = raise DELETE
   137 		  | dellist((b: string, netb) :: alist) =
   138 		      if a=b then conspair(newpair netb, alist)
   139 		      else if a<b then (*absent*) raise DELETE
   140 		      else (*a>b*)  (b,netb) :: dellist alist
   141 	    in  newnet{comb=comb, var=var, alist= dellist alist}  end
   142   in  del1 (keys,net)  end;
   143 
   144 fun delete_term ((t,x), net, eq) = delete((key_of_term t, x), net, eq);
   145 
   146 (*** Retrieval functions for discrimination nets ***)
   147 
   148 exception OASSOC;
   149 
   150 (*Ordered association list lookup*)
   151 fun oassoc ([], a: string) = raise OASSOC
   152   | oassoc ((b,x)::pairs, a) =
   153       if b<a then oassoc(pairs,a)
   154       else if a=b then x
   155       else raise OASSOC;
   156 
   157 (*Return the list of items at the given node, [] if no such node*)
   158 fun lookup (Leaf(xs), []) = xs
   159   | lookup (Leaf _, _::_) = []	(*non-empty keys and empty net*)
   160   | lookup (Net{comb,var,alist}, CombK :: keys) = lookup(comb,keys)
   161   | lookup (Net{comb,var,alist}, VarK :: keys) = lookup(var,keys)
   162   | lookup (Net{comb,var,alist}, AtomK a :: keys) = 
   163       lookup(oassoc(alist,a),keys)  handle  OASSOC => [];
   164 
   165 
   166 (*Skipping a term in a net.  Recursively skip 2 levels if a combination*)
   167 fun net_skip (Leaf _, nets) = nets
   168   | net_skip (Net{comb,var,alist}, nets) = 
   169     foldr net_skip 
   170           (net_skip (comb,[]), 
   171 	   foldr (fn ((_,net), nets) => net::nets) (alist, var::nets));
   172 
   173 (** Matching and Unification**)
   174 
   175 (*conses the linked net, if present, to nets*)
   176 fun look1 (alist, a) nets =
   177        oassoc(alist,a) :: nets  handle  OASSOC => nets;
   178 
   179 (*Return the nodes accessible from the term (cons them before nets) 
   180   "unif" signifies retrieval for unification rather than matching.
   181   Var in net matches any term.
   182   Abs or Var in object: if "unif", regarded as wildcard, 
   183                                    else matches only a variable in net.
   184 *)
   185 fun matching unif t (net,nets) =
   186   let fun rands _ (Leaf _, nets) = nets
   187 	| rands t (Net{comb,alist,...}, nets) =
   188 	    case t of 
   189 		f$t => foldr (matching unif t) (rands f (comb,[]), nets)
   190 	      | Const(c,_) => look1 (alist, c) nets
   191 	      | Free(c,_)  => look1 (alist, c) nets
   192 	      | Bound i    => look1 (alist, string_of_bound i) nets
   193 	      | _      	   => nets
   194   in 
   195      case net of
   196 	 Leaf _ => nets
   197        | Net{var,...} =>
   198 	     case head_of t of
   199 		 Var _ => if unif then net_skip (net,nets)
   200 			  else var::nets	   (*only matches Var in net*)
   201   (*If "unif" then a var instantiation in the abstraction could allow
   202     an eta-reduction, so regard the abstraction as a wildcard.*)
   203 	       | Abs _ => if unif then net_skip (net,nets)
   204 			  else var::nets	   (*only a Var can match*)
   205 	       | _ => rands t (net, var::nets)  (*var could match also*)
   206   end;
   207 
   208 fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l);
   209 
   210 (*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
   211 fun match_term net t = 
   212     extract_leaves (matching false t (net,[]));
   213 
   214 (*return items whose key could unify with t*)
   215 fun unify_term net t = 
   216     extract_leaves (matching true t (net,[]));
   217 
   218 
   219 (** dest **)
   220 
   221 fun cons_fst x (xs, y) = (x :: xs, y);
   222 
   223 fun dest (Leaf xs) = map (pair []) xs
   224   | dest (Net {comb, var, alist}) =
   225       map (cons_fst CombK) (dest comb) @
   226       map (cons_fst VarK) (dest var) @
   227       flat (map (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) alist);
   228 
   229 
   230 (** merge **)
   231 
   232 fun add eq (net, keys_x) =
   233   insert (keys_x, net, eq) handle INSERT => net;
   234 
   235 fun merge (net1, net2, eq) =
   236   foldl (add eq) (net1, dest net2);
   237 
   238 
   239 end;