src/Pure/net.ML
author paulson
Tue Mar 25 10:41:44 1997 +0100 (1997-03-25)
changeset 2836 148829646a51
parent 2792 6c17c5ec3d8b
child 3548 108d09eb3454
permissions -rw-r--r--
Toby's better treatment of eta-contraction
     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 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   end;
    32 
    33 
    34 structure Net : NET = 
    35 struct
    36 
    37 datatype key = CombK | VarK | AtomK of string;
    38 
    39 (*Bound variables*)
    40 fun string_of_bound i = "*B*" ^ chr i;
    41 
    42 (*Keys are preorder lists of symbols -- Combinations, Vars, Atoms.
    43   Any term whose head is a Var is regarded entirely as a Var.
    44   Abstractions are also regarded as Vars;  this covers eta-conversion
    45     and "near" eta-conversions such as %x.?P(?f(x)).
    46 *)
    47 fun add_key_of_terms (t, cs) = 
    48   let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs))
    49 	| rands (Const(c,_), cs) = AtomK c :: cs
    50 	| rands (Free(c,_),  cs) = AtomK c :: cs
    51 	| rands (Bound i,  cs)   = AtomK (string_of_bound i) :: cs
    52   in case (head_of t) of
    53       Var _ => VarK :: cs
    54     | Abs _ => VarK :: cs
    55     | _     => rands(t,cs)
    56   end;
    57 
    58 (*convert a term to a list of keys*)
    59 fun key_of_term t = add_key_of_terms (t, []);
    60 
    61 
    62 (*Trees indexed by key lists: each arc is labelled by a key.
    63   Each node contains a list of items, and arcs to children.
    64   Keys in the association list (alist) are stored in ascending order.
    65   The empty key addresses the entire net.
    66   Lookup functions preserve order in items stored at same level.
    67 *)
    68 datatype 'a net = Leaf of 'a list
    69 		| Net of {comb: 'a net, 
    70 			  var: 'a net,
    71 			  alist: (string * 'a net) list};
    72 
    73 val empty = Leaf[];
    74 val emptynet = Net{comb=empty, var=empty, alist=[]};
    75 
    76 
    77 (*** Insertion into a discrimination net ***)
    78 
    79 exception INSERT;	(*duplicate item in the net*)
    80 
    81 
    82 (*Adds item x to the list at the node addressed by the keys.
    83   Creates node if not already present.
    84   eq is the equality test for items. 
    85   The empty list of keys generates a Leaf node, others a Net node.
    86 *)
    87 fun insert ((keys,x), net, eq) =
    88   let fun ins1 ([], Leaf xs) = 
    89             if gen_mem eq (x,xs) then  raise INSERT  else Leaf(x::xs)
    90         | ins1 (keys, Leaf[]) = ins1 (keys, emptynet)   (*expand empty...*)
    91         | ins1 (CombK :: keys, Net{comb,var,alist}) =
    92 	    Net{comb=ins1(keys,comb), var=var, alist=alist}
    93 	| ins1 (VarK :: keys, Net{comb,var,alist}) =
    94 	    Net{comb=comb, var=ins1(keys,var), alist=alist}
    95 	| ins1 (AtomK a :: keys, Net{comb,var,alist}) =
    96 	    let fun newpair net = (a, ins1(keys,net)) 
    97 		fun inslist [] = [newpair empty]
    98 		  | inslist((b: string, netb) :: alist) =
    99 		      if a=b then newpair netb :: alist
   100 		      else if a<b then (*absent, ins1ert in alist*)
   101 			  newpair empty :: (b,netb) :: alist
   102 		      else (*a>b*) (b,netb) :: inslist alist
   103 	    in  Net{comb=comb, var=var, alist= inslist alist}  end
   104   in  ins1 (keys,net)  end;
   105 
   106 fun insert_term ((t,x), net, eq) = insert((key_of_term t, x), net, eq);
   107 
   108 (*** Deletion from a discrimination net ***)
   109 
   110 exception DELETE;	(*missing item in the net*)
   111 
   112 (*Create a new Net node if it would be nonempty*)
   113 fun newnet {comb=Leaf[], var=Leaf[], alist=[]} = empty
   114   | newnet {comb,var,alist} = Net{comb=comb, var=var, alist=alist};
   115 
   116 (*add new (b,net) pair to the alist provided net is nonempty*)
   117 fun conspair((b, Leaf[]), alist) = alist
   118   | conspair((b, net), alist)    = (b, net) :: alist;
   119 
   120 (*Deletes item x from the list at the node addressed by the keys.
   121   Raises DELETE if absent.  Collapses the net if possible.
   122   eq is the equality test for items. *)
   123 fun delete ((keys, x), net, eq) = 
   124   let fun del1 ([], Leaf xs) =
   125             if gen_mem eq (x,xs) then Leaf (gen_rem eq (xs,x))
   126             else raise DELETE
   127 	| del1 (keys, Leaf[]) = raise DELETE
   128 	| del1 (CombK :: keys, Net{comb,var,alist}) =
   129 	    newnet{comb=del1(keys,comb), var=var, alist=alist}
   130 	| del1 (VarK :: keys, Net{comb,var,alist}) =
   131 	    newnet{comb=comb, var=del1(keys,var), alist=alist}
   132 	| del1 (AtomK a :: keys, Net{comb,var,alist}) =
   133 	    let fun newpair net = (a, del1(keys,net)) 
   134 		fun dellist [] = raise DELETE
   135 		  | dellist((b: string, netb) :: alist) =
   136 		      if a=b then conspair(newpair netb, alist)
   137 		      else if a<b then (*absent*) raise DELETE
   138 		      else (*a>b*)  (b,netb) :: dellist alist
   139 	    in  newnet{comb=comb, var=var, alist= dellist alist}  end
   140   in  del1 (keys,net)  end;
   141 
   142 fun delete_term ((t,x), net, eq) = delete((key_of_term t, x), net, eq);
   143 
   144 (*** Retrieval functions for discrimination nets ***)
   145 
   146 exception OASSOC;
   147 
   148 (*Ordered association list lookup*)
   149 fun oassoc ([], a: string) = raise OASSOC
   150   | oassoc ((b,x)::pairs, a) =
   151       if b<a then oassoc(pairs,a)
   152       else if a=b then x
   153       else raise OASSOC;
   154 
   155 (*Return the list of items at the given node, [] if no such node*)
   156 fun lookup (Leaf(xs), []) = xs
   157   | lookup (Leaf _, _::_) = []	(*non-empty keys and empty net*)
   158   | lookup (Net{comb,var,alist}, CombK :: keys) = lookup(comb,keys)
   159   | lookup (Net{comb,var,alist}, VarK :: keys) = lookup(var,keys)
   160   | lookup (Net{comb,var,alist}, AtomK a :: keys) = 
   161       lookup(oassoc(alist,a),keys)  handle  OASSOC => [];
   162 
   163 
   164 (*Skipping a term in a net.  Recursively skip 2 levels if a combination*)
   165 fun net_skip (Leaf _, nets) = nets
   166   | net_skip (Net{comb,var,alist}, nets) = 
   167     foldr net_skip 
   168           (net_skip (comb,[]), 
   169 	   foldr (fn ((_,net), nets) => net::nets) (alist, var::nets));
   170 
   171 (** Matching and Unification**)
   172 
   173 (*conses the linked net, if present, to nets*)
   174 fun look1 (alist, a) nets =
   175        oassoc(alist,a) :: nets  handle  OASSOC => nets;
   176 
   177 (*Return the nodes accessible from the term (cons them before nets) 
   178   "unif" signifies retrieval for unification rather than matching.
   179   Var in net matches any term.
   180   Abs or Var in object: if "unif", regarded as wildcard, 
   181                                    else matches only a variable in net.
   182 *)
   183 fun matching unif t (net,nets) =
   184   let fun rands _ (Leaf _, nets) = nets
   185 	| rands t (Net{comb,alist,...}, nets) =
   186 	    case t of 
   187 		f$t => foldr (matching unif t) (rands f (comb,[]), nets)
   188 	      | Const(c,_) => look1 (alist, c) nets
   189 	      | Free(c,_)  => look1 (alist, c) nets
   190 	      | Bound i    => look1 (alist, string_of_bound i) nets
   191 	      | _      	   => nets
   192   in 
   193      case net of
   194 	 Leaf _ => nets
   195        | Net{var,...} =>
   196 	     let val etat = Pattern.eta_contract_atom t
   197 	     in case (head_of etat) of
   198 		 Var _ => if unif then net_skip (net,nets)
   199 			  else var::nets	   (*only matches Var in net*)
   200   (*If "unif" then a var instantiation in the abstraction could allow
   201     an eta-reduction, so regard the abstraction as a wildcard.*)
   202 	       | Abs _ => if unif then net_skip (net,nets)
   203 			  else var::nets	   (*only a Var can match*)
   204 	       | _ => rands etat (net, var::nets)  (*var could match also*)
   205 	     end
   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 end;