src/Pure/net.ML
changeset 1458 fd510875fb71
parent 228 4f43430f226e
child 1460 5a6f2aabd538
     1.1 --- a/src/Pure/net.ML	Mon Jan 29 13:50:10 1996 +0100
     1.2 +++ b/src/Pure/net.ML	Mon Jan 29 13:56:41 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	net
     1.5 +(*  Title:      net
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1993  University of Cambridge
    1.10  
    1.11  Discrimination nets: a data structure for indexing items
    1.12 @@ -46,9 +46,9 @@
    1.13  *)
    1.14  fun add_key_of_terms (t, cs) = 
    1.15    let fun rands (f$t, cs) = CombK :: rands (f, add_key_of_terms(t, cs))
    1.16 -	| rands (Const(c,_), cs) = AtomK c :: cs
    1.17 -	| rands (Free(c,_),  cs) = AtomK c :: cs
    1.18 -	| rands (Bound i,  cs)   = AtomK (string_of_bound i) :: cs
    1.19 +        | rands (Const(c,_), cs) = AtomK c :: cs
    1.20 +        | rands (Free(c,_),  cs) = AtomK c :: cs
    1.21 +        | rands (Bound i,  cs)   = AtomK (string_of_bound i) :: cs
    1.22    in case (head_of t) of
    1.23        Var _ => VarK :: cs
    1.24      | Abs _ => VarK :: cs
    1.25 @@ -66,9 +66,9 @@
    1.26    Lookup functions preserve order in items stored at same level.
    1.27  *)
    1.28  datatype 'a net = Leaf of 'a list
    1.29 -		| Net of {comb: 'a net, 
    1.30 -			  var: 'a net,
    1.31 -			  alist: (string * 'a net) list};
    1.32 +                | Net of {comb: 'a net, 
    1.33 +                          var: 'a net,
    1.34 +                          alist: (string * 'a net) list};
    1.35  
    1.36  val empty = Leaf[];
    1.37  val emptynet = Net{comb=empty, var=empty, alist=[]};
    1.38 @@ -76,7 +76,7 @@
    1.39  
    1.40  (*** Insertion into a discrimination net ***)
    1.41  
    1.42 -exception INSERT;	(*duplicate item in the net*)
    1.43 +exception INSERT;       (*duplicate item in the net*)
    1.44  
    1.45  
    1.46  (*Adds item x to the list at the node addressed by the keys.
    1.47 @@ -89,25 +89,25 @@
    1.48              if gen_mem eq (x,xs) then  raise INSERT  else Leaf(x::xs)
    1.49          | ins1 (keys, Leaf[]) = ins1 (keys, emptynet)   (*expand empty...*)
    1.50          | ins1 (CombK :: keys, Net{comb,var,alist}) =
    1.51 -	    Net{comb=ins1(keys,comb), var=var, alist=alist}
    1.52 -	| ins1 (VarK :: keys, Net{comb,var,alist}) =
    1.53 -	    Net{comb=comb, var=ins1(keys,var), alist=alist}
    1.54 -	| ins1 (AtomK a :: keys, Net{comb,var,alist}) =
    1.55 -	    let fun newpair net = (a, ins1(keys,net)) 
    1.56 -		fun inslist [] = [newpair empty]
    1.57 -		  | inslist((b: string, netb) :: alist) =
    1.58 -		      if a=b then newpair netb :: alist
    1.59 -		      else if a<b then (*absent, ins1ert in alist*)
    1.60 -			  newpair empty :: (b,netb) :: alist
    1.61 -		      else (*a>b*) (b,netb) :: inslist alist
    1.62 -	    in  Net{comb=comb, var=var, alist= inslist alist}  end
    1.63 +            Net{comb=ins1(keys,comb), var=var, alist=alist}
    1.64 +        | ins1 (VarK :: keys, Net{comb,var,alist}) =
    1.65 +            Net{comb=comb, var=ins1(keys,var), alist=alist}
    1.66 +        | ins1 (AtomK a :: keys, Net{comb,var,alist}) =
    1.67 +            let fun newpair net = (a, ins1(keys,net)) 
    1.68 +                fun inslist [] = [newpair empty]
    1.69 +                  | inslist((b: string, netb) :: alist) =
    1.70 +                      if a=b then newpair netb :: alist
    1.71 +                      else if a<b then (*absent, ins1ert in alist*)
    1.72 +                          newpair empty :: (b,netb) :: alist
    1.73 +                      else (*a>b*) (b,netb) :: inslist alist
    1.74 +            in  Net{comb=comb, var=var, alist= inslist alist}  end
    1.75    in  ins1 (keys,net)  end;
    1.76  
    1.77  fun insert_term ((t,x), net, eq) = insert((key_of_term t, x), net, eq);
    1.78  
    1.79  (*** Deletion from a discrimination net ***)
    1.80  
    1.81 -exception DELETE;	(*missing item in the net*)
    1.82 +exception DELETE;       (*missing item in the net*)
    1.83  
    1.84  (*Create a new Net node if it would be nonempty*)
    1.85  fun newnet {comb=Leaf[], var=Leaf[], alist=[]} = empty
    1.86 @@ -124,19 +124,19 @@
    1.87    let fun del1 ([], Leaf xs) =
    1.88              if gen_mem eq (x,xs) then Leaf (gen_rem eq (xs,x))
    1.89              else raise DELETE
    1.90 -	| del1 (keys, Leaf[]) = raise DELETE
    1.91 -	| del1 (CombK :: keys, Net{comb,var,alist}) =
    1.92 -	    newnet{comb=del1(keys,comb), var=var, alist=alist}
    1.93 -	| del1 (VarK :: keys, Net{comb,var,alist}) =
    1.94 -	    newnet{comb=comb, var=del1(keys,var), alist=alist}
    1.95 -	| del1 (AtomK a :: keys, Net{comb,var,alist}) =
    1.96 -	    let fun newpair net = (a, del1(keys,net)) 
    1.97 -		fun dellist [] = raise DELETE
    1.98 -		  | dellist((b: string, netb) :: alist) =
    1.99 -		      if a=b then conspair(newpair netb, alist)
   1.100 -		      else if a<b then (*absent*) raise DELETE
   1.101 -		      else (*a>b*)  (b,netb) :: dellist alist
   1.102 -	    in  newnet{comb=comb, var=var, alist= dellist alist}  end
   1.103 +        | del1 (keys, Leaf[]) = raise DELETE
   1.104 +        | del1 (CombK :: keys, Net{comb,var,alist}) =
   1.105 +            newnet{comb=del1(keys,comb), var=var, alist=alist}
   1.106 +        | del1 (VarK :: keys, Net{comb,var,alist}) =
   1.107 +            newnet{comb=comb, var=del1(keys,var), alist=alist}
   1.108 +        | del1 (AtomK a :: keys, Net{comb,var,alist}) =
   1.109 +            let fun newpair net = (a, del1(keys,net)) 
   1.110 +                fun dellist [] = raise DELETE
   1.111 +                  | dellist((b: string, netb) :: alist) =
   1.112 +                      if a=b then conspair(newpair netb, alist)
   1.113 +                      else if a<b then (*absent*) raise DELETE
   1.114 +                      else (*a>b*)  (b,netb) :: dellist alist
   1.115 +            in  newnet{comb=comb, var=var, alist= dellist alist}  end
   1.116    in  del1 (keys,net)  end;
   1.117  
   1.118  fun delete_term ((t,x), net, eq) = delete((key_of_term t, x), net, eq);
   1.119 @@ -154,7 +154,7 @@
   1.120  
   1.121  (*Return the list of items at the given node, [] if no such node*)
   1.122  fun lookup (Leaf(xs), []) = xs
   1.123 -  | lookup (Leaf _, _::_) = []	(*non-empty keys and empty net*)
   1.124 +  | lookup (Leaf _, _::_) = []  (*non-empty keys and empty net*)
   1.125    | lookup (Net{comb,var,alist}, CombK :: keys) = lookup(comb,keys)
   1.126    | lookup (Net{comb,var,alist}, VarK :: keys) = lookup(var,keys)
   1.127    | lookup (Net{comb,var,alist}, AtomK a :: keys) = 
   1.128 @@ -166,7 +166,7 @@
   1.129    | net_skip (Net{comb,var,alist}, nets) = 
   1.130      foldr net_skip 
   1.131            (net_skip (comb,[]), 
   1.132 -	   foldr (fn ((_,net), nets) => net::nets) (alist, var::nets));
   1.133 +           foldr (fn ((_,net), nets) => net::nets) (alist, var::nets));
   1.134  
   1.135  (** Matching and Unification**)
   1.136  
   1.137 @@ -182,25 +182,25 @@
   1.138  *)
   1.139  fun matching unif t (net,nets) =
   1.140    let fun rands _ (Leaf _, nets) = nets
   1.141 -	| rands t (Net{comb,alist,...}, nets) =
   1.142 -	    case t of 
   1.143 -		f$t => foldr (matching unif t) (rands f (comb,[]), nets)
   1.144 -	      | Const(c,_) => look1 (alist, c) nets
   1.145 -	      | Free(c,_)  => look1 (alist, c) nets
   1.146 -	      | Bound i    => look1 (alist, string_of_bound i) nets
   1.147 -	      | _      	   => nets
   1.148 +        | rands t (Net{comb,alist,...}, nets) =
   1.149 +            case t of 
   1.150 +                f$t => foldr (matching unif t) (rands f (comb,[]), nets)
   1.151 +              | Const(c,_) => look1 (alist, c) nets
   1.152 +              | Free(c,_)  => look1 (alist, c) nets
   1.153 +              | Bound i    => look1 (alist, string_of_bound i) nets
   1.154 +              | _          => nets
   1.155    in 
   1.156       case net of
   1.157 -	 Leaf _ => nets
   1.158 +         Leaf _ => nets
   1.159         | Net{var,...} =>
   1.160 -	   case (head_of t) of
   1.161 -	       Var _ => if unif then net_skip (net,nets)
   1.162 -			else var::nets	   	(*only matches Var in net*)
   1.163 +           case (head_of t) of
   1.164 +               Var _ => if unif then net_skip (net,nets)
   1.165 +                        else var::nets          (*only matches Var in net*)
   1.166  (*If "unif" then a var instantiation in the abstraction could allow
   1.167    an eta-reduction, so regard the abstraction as a wildcard.*)
   1.168 -	     | Abs _ => if unif then net_skip (net,nets)
   1.169 -			else var::nets		(*only a Var can match*)
   1.170 -	     | _ => rands t (net, var::nets)	(*var could match also*)
   1.171 +             | Abs _ => if unif then net_skip (net,nets)
   1.172 +                        else var::nets          (*only a Var can match*)
   1.173 +             | _ => rands t (net, var::nets)    (*var could match also*)
   1.174    end;
   1.175  
   1.176  val extract_leaves = flat o map (fn Leaf(xs) => xs);