src/Pure/net.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 225 76f60e6400e8
permissions -rw-r--r--
Initial revision
     1 (*  Title: 	net
     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 
    14 signature NET = 
    15   sig
    16   type key
    17   type 'a net
    18   exception DELETE and INSERT
    19   val delete: (key list * 'a) * 'a net * ('a*'a -> bool) -> 'a net
    20   val delete_term:   (term * 'a) * 'a net * ('a*'a -> bool) -> 'a net
    21   val empty: 'a net
    22   val insert: (key list * 'a) * 'a net * ('a*'a -> bool) -> 'a net
    23   val insert_term:   (term * 'a) * 'a net * ('a*'a -> bool) -> 'a net
    24   val lookup: 'a net * key list -> 'a list
    25   val match_term: 'a net -> term -> 'a list
    26   val key_of_term: term -> key list
    27   val unify_term: 'a net -> term -> 'a list
    28   end;
    29 
    30 
    31 functor NetFun () : NET = 
    32 struct
    33 
    34 datatype key = CombK | VarK | AtomK of string;
    35 
    36 (*Only 'loose' bound variables could arise, since Abs nodes are skipped*)
    37 fun string_of_bound i = "*B*" ^ chr i;
    38 
    39 (*Keys are preorder lists of symbols -- constants, Vars, bound vars, ...
    40   Any term whose head is a Var is regarded entirely as a Var;
    41   abstractions are also regarded as Vars (to cover eta-conversion)
    42 *)
    43 fun add_key_of_terms (t, cs) = 
    44   let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs))
    45 	| rands (Const(c,_), cs) = AtomK c :: cs
    46 	| rands (Free(c,_),  cs) = AtomK c :: cs
    47 	| rands (Bound i,  cs) = AtomK (string_of_bound i) :: cs
    48   in case (head_of t) of
    49       Var _       => VarK :: cs
    50     | Abs (_,_,t) => VarK :: cs
    51     | _ => rands(t,cs)
    52   end;
    53 
    54 (*convert a term to a key -- a list of keys*)
    55 fun key_of_term t = add_key_of_terms (t, []);
    56 
    57 
    58 (*Trees indexed by key lists: each arc is labelled by a key.
    59   Each node contains a list of items, and arcs to children.
    60   Keys in the association list (alist) are stored in ascending order.
    61   The empty key addresses the entire net.
    62   Lookup functions preserve order in items stored at same level.
    63 *)
    64 datatype 'a net = Leaf of 'a list
    65 		| Net of {comb: 'a net, 
    66 			  var: 'a net,
    67 			  alist: (string * 'a net) list};
    68 
    69 val empty = Leaf[];
    70 val emptynet = Net{comb=empty, var=empty, alist=[]};
    71 
    72 
    73 (*** Insertion into a discrimination net ***)
    74 
    75 exception INSERT;	(*duplicate item in the net*)
    76 
    77 
    78 (*Adds item x to the list at the node addressed by the keys.
    79   Creates node if not already present.
    80   eq is the equality test for items. 
    81   The empty list of keys generates a Leaf node, others a Net node.
    82 *)
    83 fun insert ((keys,x), net, eq) =
    84   let fun ins1 ([], Leaf xs) = 
    85             if gen_mem eq (x,xs) then  raise INSERT  else Leaf(x::xs)
    86         | ins1 (keys, Leaf[]) = ins1 (keys, emptynet)   (*expand empty...*)
    87         | ins1 (CombK :: keys, Net{comb,var,alist}) =
    88 	    Net{comb=ins1(keys,comb), var=var, alist=alist}
    89 	| ins1 (VarK :: keys, Net{comb,var,alist}) =
    90 	    Net{comb=comb, var=ins1(keys,var), alist=alist}
    91 	| ins1 (AtomK a :: keys, Net{comb,var,alist}) =
    92 	    let fun newpair net = (a, ins1(keys,net)) 
    93 		fun inslist [] = [newpair empty]
    94 		  | inslist((b: string, netb) :: alist) =
    95 		      if a=b then newpair netb :: alist
    96 		      else if a<b then (*absent, ins1ert in alist*)
    97 			  newpair empty :: (b,netb) :: alist
    98 		      else (*a>b*) (b,netb) :: inslist alist
    99 	    in  Net{comb=comb, var=var, alist= inslist alist}  end
   100   in  ins1 (keys,net)  end;
   101 
   102 fun insert_term ((t,x), net, eq) = insert((key_of_term t, x), net, eq);
   103 
   104 (*** Deletion from a discrimination net ***)
   105 
   106 exception DELETE;	(*missing item in the net*)
   107 
   108 (*Create a new Net node if it would be nonempty*)
   109 fun newnet {comb=Leaf[], var=Leaf[], alist=[]} = empty
   110   | newnet {comb,var,alist} = Net{comb=comb, var=var, alist=alist};
   111 
   112 (*add new (b,net) pair to the alist provided net is nonempty*)
   113 fun conspair((b, Leaf[]), alist) = alist
   114   | conspair((b, net), alist)    = (b, net) :: alist;
   115 
   116 (*Deletes item x from the list at the node addressed by the keys.
   117   Raises DELETE if absent.  Collapses the net if possible.
   118   eq is the equality test for items. *)
   119 fun delete ((keys, x), net, eq) = 
   120   let fun del1 ([], Leaf xs) =
   121             if gen_mem eq (x,xs) then Leaf (gen_rem eq (xs,x))
   122             else raise DELETE
   123 	| del1 (keys, Leaf[]) = raise DELETE
   124 	| del1 (CombK :: keys, Net{comb,var,alist}) =
   125 	    newnet{comb=del1(keys,comb), var=var, alist=alist}
   126 	| del1 (VarK :: keys, Net{comb,var,alist}) =
   127 	    newnet{comb=comb, var=del1(keys,var), alist=alist}
   128 	| del1 (AtomK a :: keys, Net{comb,var,alist}) =
   129 	    let fun newpair net = (a, del1(keys,net)) 
   130 		fun dellist [] = raise DELETE
   131 		  | dellist((b: string, netb) :: alist) =
   132 		      if a=b then conspair(newpair netb, alist)
   133 		      else if a<b then (*absent*) raise DELETE
   134 		      else (*a>b*)  (b,netb) :: dellist alist
   135 	    in  newnet{comb=comb, var=var, alist= dellist alist}  end
   136   in  del1 (keys,net)  end;
   137 
   138 fun delete_term ((t,x), net, eq) = delete((key_of_term t, x), net, eq);
   139 
   140 (*** Retrieval functions for discrimination nets ***)
   141 
   142 exception OASSOC;
   143 
   144 (*Ordered association list lookup*)
   145 fun oassoc ([], a: string) = raise OASSOC
   146   | oassoc ((b,x)::pairs, a) =
   147       if b<a then oassoc(pairs,a)
   148       else if a=b then x
   149       else raise OASSOC;
   150 
   151 (*Return the list of items at the given node, [] if no such node*)
   152 fun lookup (Leaf(xs), []) = xs
   153   | lookup (Leaf _, _::_) = []	(*non-empty keys and empty net*)
   154   | lookup (Net{comb,var,alist}, CombK :: keys) = lookup(comb,keys)
   155   | lookup (Net{comb,var,alist}, VarK :: keys) = lookup(var,keys)
   156   | lookup (Net{comb,var,alist}, AtomK a :: keys) = 
   157       lookup(oassoc(alist,a),keys)  handle  OASSOC => [];
   158 
   159 
   160 (*Skipping a term in a net.  Recursively skip 2 levels if a combination*)
   161 fun net_skip (Leaf _, nets) = nets
   162   | net_skip (Net{comb,var,alist}, nets) = 
   163     foldr net_skip 
   164           (net_skip (comb,[]), 
   165 	   foldr (fn ((_,net), nets) => net::nets) (alist, var::nets));
   166 
   167 (** Matching and Unification**)
   168 
   169 (*conses the linked net, if present, to nets*)
   170 fun look1 (alist, a) nets =
   171        oassoc(alist,a) :: nets  handle  OASSOC => nets;
   172 
   173 (*Return the nodes accessible from the term (cons them before nets) 
   174   "unif" signifies retrieval for unification rather than matching.
   175   Var in net matches any term.
   176   Abs in object (and Var if "unif") regarded as wildcard.
   177   If not "unif", Var in object only matches a variable in net.*)
   178 fun matching unif t (net,nets) =
   179   let fun rands _ (Leaf _, nets) = nets
   180 	| rands t (Net{comb,alist,...}, nets) =
   181 	    case t of 
   182 		(f$t) => foldr (matching unif t) (rands f (comb,[]), nets)
   183 	      | (Const(c,_)) => look1 (alist, c) nets
   184 	      | (Free(c,_))  => look1 (alist, c) nets
   185 	      | (Bound i)    => look1 (alist, string_of_bound i) 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 	     | Abs(_,_,u) => net_skip (net,nets)   (*could match anything*)
   194 	     | _ => rands t (net, var::nets)	   (*var could match also*)
   195   end;
   196 
   197 val extract_leaves = flat o map (fn Leaf(xs) => xs);
   198 
   199 (*return items whose key could match t*)
   200 fun match_term net t = 
   201     extract_leaves (matching false t (net,[]));
   202 
   203 (*return items whose key could unify with t*)
   204 fun unify_term net t = 
   205     extract_leaves (matching true t (net,[]));
   206 
   207 end;