added subtract;
authorwenzelm
Wed Jul 13 16:07:29 2005 +0200 (2005-07-13)
changeset 16808644fc45c7292
parent 16807 730cace0ae48
child 16809 8ca51a846576
added subtract;
improved interface;
tuned;
src/Pure/net.ML
     1.1 --- a/src/Pure/net.ML	Wed Jul 13 16:07:28 2005 +0200
     1.2 +++ b/src/Pure/net.ML	Wed Jul 13 16:07:29 2005 +0200
     1.3 @@ -15,24 +15,26 @@
     1.4  *)
     1.5  
     1.6  signature NET =
     1.7 -  sig
     1.8 +sig
     1.9    type key
    1.10 +  val key_of_term: term -> key list
    1.11    type 'a net
    1.12 -  exception DELETE and INSERT
    1.13 -  val delete: (key list * 'a) * 'b net * ('a * 'b -> bool) -> 'b net
    1.14 -  val delete_term: (term * 'a) * 'b net * ('a * 'b -> bool) -> 'b net
    1.15    val empty: 'a net
    1.16 -  val insert: (key list * 'a) * 'a net * ('a*'a -> bool) -> 'a net
    1.17 -  val insert_term:   (term * 'a) * 'a net * ('a*'a -> bool) -> 'a net
    1.18 -  val lookup: 'a net * key list -> 'a list
    1.19 +  exception INSERT
    1.20 +  val insert: ('a * 'a -> bool) -> key list * 'a -> 'a net -> 'a net
    1.21 +  val insert_term: ('a * 'a -> bool) -> term * 'a -> 'a net -> 'a net
    1.22 +  exception DELETE
    1.23 +  val delete: ('b * 'a -> bool) -> key list * 'b -> 'a net -> 'a net
    1.24 +  val delete_term: ('b * 'a -> bool) -> term * 'b -> 'a net -> 'a net
    1.25 +  val lookup: 'a net -> key list -> 'a list
    1.26    val match_term: 'a net -> term -> 'a list
    1.27 -  val key_of_term: term -> key list
    1.28    val unify_term: 'a net -> term -> 'a list
    1.29 -  val dest: 'a net -> (key list * 'a) list
    1.30 -  val merge: 'a net * 'a net * ('a*'a -> bool) -> 'a net
    1.31 -  end;
    1.32 +  val entries: 'a net -> 'a list
    1.33 +  val subtract: ('b * 'a -> bool) -> 'a net -> 'b net -> 'b list
    1.34 +  val merge: ('a * 'a -> bool) -> 'a net * 'a net -> 'a net
    1.35 +end;
    1.36  
    1.37 -structure Net : NET =
    1.38 +structure Net: NET =
    1.39  struct
    1.40  
    1.41  datatype key = CombK | VarK | AtomK of string;
    1.42 @@ -85,7 +87,7 @@
    1.43    eq is the equality test for items.
    1.44    The empty list of keys generates a Leaf node, others a Net node.
    1.45  *)
    1.46 -fun insert ((keys,x), net, eq) =
    1.47 +fun insert eq (keys,x) net =
    1.48    let fun ins1 ([], Leaf xs) =
    1.49              if member eq xs x then  raise INSERT  else Leaf(x::xs)
    1.50          | ins1 (keys, Leaf[]) = ins1 (keys, emptynet)   (*expand empty...*)
    1.51 @@ -100,7 +102,9 @@
    1.52              in  Net{comb=comb, var=var, atoms=atoms'}  end
    1.53    in  ins1 (keys,net)  end;
    1.54  
    1.55 -fun insert_term ((t,x), net, eq) = insert((key_of_term t, x), net, eq);
    1.56 +fun insert_safe eq entry net = insert eq entry net handle INSERT => net;
    1.57 +fun insert_term eq (t, x) = insert eq (key_of_term t, x);
    1.58 +
    1.59  
    1.60  (*** Deletion from a discrimination net ***)
    1.61  
    1.62 @@ -114,7 +118,7 @@
    1.63  (*Deletes item x from the list at the node addressed by the keys.
    1.64    Raises DELETE if absent.  Collapses the net if possible.
    1.65    eq is the equality test for items. *)
    1.66 -fun delete ((keys, x), net, eq) =
    1.67 +fun delete eq (keys, x) net =
    1.68    let fun del1 ([], Leaf xs) =
    1.69              if member eq xs x then Leaf (remove eq x xs)
    1.70              else raise DELETE
    1.71 @@ -134,7 +138,7 @@
    1.72              in  newnet{comb=comb, var=var, atoms=atoms'}  end
    1.73    in  del1 (keys,net)  end;
    1.74  
    1.75 -fun delete_term ((t,x), net, eq) = delete((key_of_term t, x), net, eq);
    1.76 +fun delete_term eq (t, x) = delete eq (key_of_term t, x);
    1.77  
    1.78  
    1.79  (*** Retrieval functions for discrimination nets ***)
    1.80 @@ -147,12 +151,12 @@
    1.81    | SOME net => net);
    1.82  
    1.83  (*Return the list of items at the given node, [] if no such node*)
    1.84 -fun lookup (Leaf(xs), []) = xs
    1.85 -  | lookup (Leaf _, _::_) = []  (*non-empty keys and empty net*)
    1.86 -  | lookup (Net{comb,var,atoms}, CombK :: keys) = lookup(comb,keys)
    1.87 -  | lookup (Net{comb,var,atoms}, VarK :: keys) = lookup(var,keys)
    1.88 -  | lookup (Net{comb,var,atoms}, AtomK a :: keys) =
    1.89 -      lookup (the_atom atoms a, keys) handle ABSENT => [];
    1.90 +fun lookup (Leaf xs) [] = xs
    1.91 +  | lookup (Leaf _) (_ :: _) = []  (*non-empty keys and empty net*)
    1.92 +  | lookup (Net {comb, var, atoms}) (CombK :: keys) = lookup comb keys
    1.93 +  | lookup (Net {comb, var, atoms}) (VarK :: keys) = lookup var keys
    1.94 +  | lookup (Net {comb, var, atoms}) (AtomK a :: keys) =
    1.95 +      lookup (the_atom atoms a) keys handle ABSENT => [];
    1.96  
    1.97  
    1.98  (*Skipping a term in a net.  Recursively skip 2 levels if a combination*)
    1.99 @@ -160,7 +164,8 @@
   1.100    | net_skip (Net{comb,var,atoms}, nets) =
   1.101        foldr net_skip (Symtab.fold (cons o #2) atoms (var::nets)) (net_skip (comb,[]));
   1.102  
   1.103 -(** Matching and Unification**)
   1.104 +
   1.105 +(** Matching and Unification **)
   1.106  
   1.107  (*conses the linked net, if present, to nets*)
   1.108  fun look1 (atoms, a) nets =
   1.109 @@ -206,7 +211,27 @@
   1.110      extract_leaves (matching true t (net,[]));
   1.111  
   1.112  
   1.113 -(** dest **)
   1.114 +(** operations on nets **)
   1.115 +
   1.116 +(*subtraction: collect entries of second net that are NOT present in first net*)
   1.117 +fun subtract eq net1 net2 =
   1.118 +  let
   1.119 +    fun subtr (Net _) (Leaf ys) = append ys
   1.120 +      | subtr (Leaf xs) (Leaf ys) =
   1.121 +          fold_rev (fn y => if member eq xs y then I else cons y) ys
   1.122 +      | subtr (Leaf _) (net as Net _) = subtr emptynet net
   1.123 +      | subtr (Net {comb = comb1, var = var1, atoms = atoms1})
   1.124 +            (Net {comb = comb2, var = var2, atoms = atoms2}) =
   1.125 +          Symtab.fold (fn (a, net) =>
   1.126 +            subtr (if_none (Symtab.lookup (atoms1, a)) emptynet) net) atoms2 o
   1.127 +          subtr var1 var2 o
   1.128 +          subtr comb1 comb2;
   1.129 +  in subtr net1 net2 [] end;
   1.130 +
   1.131 +fun entries net = subtract (K false) empty net;
   1.132 +
   1.133 +
   1.134 +(* merge *)
   1.135  
   1.136  fun cons_fst x (xs, y) = (x :: xs, y);
   1.137  
   1.138 @@ -214,14 +239,8 @@
   1.139    | dest (Net {comb, var, atoms}) =
   1.140        map (cons_fst CombK) (dest comb) @
   1.141        map (cons_fst VarK) (dest var) @
   1.142 -      List.concat (map (fn (a, net) => map (cons_fst (AtomK a)) (dest net))
   1.143 -        (Symtab.dest atoms));
   1.144 -
   1.145 +      List.concat (map (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms));
   1.146  
   1.147 -(** merge **)
   1.148 -
   1.149 -fun add eq keys_x net = insert (keys_x, net, eq) handle INSERT => net;
   1.150 -fun merge (net1, net2, eq) = fold (add eq) (dest net2) net1;
   1.151 -
   1.152 +fun merge eq (net1, net2) = fold (insert_safe eq) (dest net2) net1;
   1.153  
   1.154  end;