add mapSizeU & adapt type of delU to work on maps with unique values

src/libraries/OS-Independent/Data/Map.dcl

@@ -160,6 +160,13 @@ singleton   :: !k !v -> Map k v
  */
 mapSize     :: !(Map k v) -> Int
 
+/**
+ * The number of elements in a possibly unique Map.
+ * @property corresponds to mapSize: A.m :: Map k v:
+ *     fst (mapSizeU m) =.= mapSize m
+ */
+mapSizeU :: !u:(Map k v:v) -> (!Int, !u:Map k v:v), [u <= v]
+
 /**
  * Adds or replaces the value for a given key.
  *
@@ -222,8 +229,8 @@ del :: !k !(Map k a) -> Map k a | < k
 /**
  * Removes the value at a given key position. The mapping can be unique.
  */
-delU :: !a !.(Map a b) -> u:(!v:(Maybe b), !Map a b) | == a & < a, [u <= v] // !k !w:(Map k u:v) -> x:(Maybe u:v, !y:(Map k u:v)) | == k & < k, [ w y <= u, x <= y, w <= y]
-	special a=Int; a=String
+delU :: !k !w:(Map k u:v) -> x:(Maybe u:v, !y:(Map k u:v)) | == k & < k, [ w y <= u, x <= y, w <= y]
+	special k=Int; k=String
 
 foldrWithKey :: !(k v u:a -> u:a) !u:a !(Map k v) -> u:a
 foldlWithKey :: !(.a -> .(k -> .(v -> .a))) !.a !(Map k v) -> .a

src/libraries/OS-Independent/Data/Map.icl

@@ -26,6 +26,10 @@ mapSize :: !(Map k a) -> Int
 mapSize Tip              = 0
 mapSize (Bin sz _ _ _ _) = sz
 
+mapSizeU :: !u:(Map k v:v) -> (!Int, !u:Map k v:v), [u <= v]
+mapSizeU m=:Tip              = (0, m)
+mapSizeU m=:(Bin sz _ _ _ _) = (sz, m)
+
 lexOrd x y :== if (x < y) LT (if (x > y) GT EQ)
 
 member :: !k !(Map k a) -> Bool | < k
@@ -1694,7 +1698,7 @@ ratio :== 2
 //
 // It is only written in such a way that every node is pattern-matched only once.
 
-balance :: !k !a !(Map k a) !(Map k a) -> Map k a
+balance :: !k !u:v !v:(Map k u:v) !v:(Map k u:v) -> v:Map k u:v, [v <= u]
 balance k x l r = case l of
   Tip -> case r of
            Tip -> Bin 1 k x Tip Tip
@@ -1703,26 +1707,34 @@ balance k x l r = case l of
            (Bin _ rk rx (Bin _ rlk rlx _ _) Tip) -> Bin 3 rlk rlx (Bin 1 k x Tip Tip) (Bin 1 rk rx Tip Tip)
            (Bin rs rk rx rl=:(Bin rls rlk rlx rll rlr) rr=:(Bin rrs _ _ _ _))
              | rls < ratio*rrs -> Bin (1+rs) rk rx (Bin (1+rls) k x Tip rl) rr
-             | otherwise -> Bin (1+rs) rlk rlx (Bin (1+mapSize rll) k x Tip rll) (Bin (1+rrs+mapSize rlr) rk rx rlr rr)
+             # (rlls, rll) = mapSizeU rll
+             # (rlrs, rlr) = mapSizeU rlr
+             | otherwise -> Bin (1+rs) rlk rlx (Bin (1+rlls) k x Tip rll) (Bin (1+rrs+rlrs) rk rx rlr rr)
 
   (Bin ls lk lx ll lr) -> case r of
            Tip -> case (ll, lr) of
-                    (Tip, Tip) -> Bin 2 k x l Tip
+                    (ll=:Tip, lr=:Tip) -> Bin 2 k x (Bin ls lk lx ll lr) Tip
                     (Tip, (Bin _ lrk lrx _ _)) -> Bin 3 lrk lrx (Bin 1 lk lx Tip Tip) (Bin 1 k x Tip Tip)
-                    ((Bin _ _ _ _ _), Tip) -> Bin 3 lk lx ll (Bin 1 k x Tip Tip)
-                    ((Bin lls _ _ _ _), (Bin lrs lrk lrx lrl lrr))
+                    (ll=:(Bin _ _ _ _ _), Tip) -> Bin 3 lk lx ll (Bin 1 k x Tip Tip)
+                    (ll=:(Bin lls _ _ _ _), lr=:(Bin lrs lrk lrx lrl lrr))
                       | lrs < ratio*lls -> Bin (1+ls) lk lx ll (Bin (1+lrs) k x lr Tip)
-                      | otherwise -> Bin (1+ls) lrk lrx (Bin (1+lls+mapSize lrl) lk lx ll lrl) (Bin (1+mapSize lrr) k x lrr Tip)
+                      # (lrls, lrl) = mapSizeU lrl
+                      # (lrrs, lrr) = mapSizeU lrr
+                      | otherwise -> Bin (1+ls) lrk lrx (Bin (1+lls+lrls) lk lx ll lrl) (Bin (1+lrrs) k x lrr Tip)
            (Bin rs rk rx rl rr)
               | rs > delta*ls  -> case (rl, rr) of
-                   (Bin rls rlk rlx rll rlr, Bin rrs _ _ _ _)
+                   (rl=:Bin rls rlk rlx rll rlr, rr=:Bin rrs _ _ _ _)
                      | rls < ratio*rrs -> Bin (1+ls+rs) rk rx (Bin (1+ls+rls) k x l rl) rr
-                     | otherwise -> Bin (1+ls+rs) rlk rlx (Bin (1+ls+mapSize rll) k x l rll) (Bin (1+rrs+mapSize rlr) rk rx rlr rr)
+                     # (rlls, rll) = mapSizeU rll
+                     # (rlrs, rlr) = mapSizeU rlr
+                     | otherwise -> Bin (1+ls+rs) rlk rlx (Bin (1+ls+rlls) k x l rll) (Bin (1+rrs+rlrs) rk rx rlr rr)
                    (_, _) -> abort "Failure in Data.Map.balance"
               | ls > delta*rs  -> case (ll, lr) of
-                   (Bin lls _ _ _ _, Bin lrs lrk lrx lrl lrr)
+                   (ll=:Bin lls _ _ _ _, lr=:Bin lrs lrk lrx lrl lrr)
                      | lrs < ratio*lls -> Bin (1+ls+rs) lk lx ll (Bin (1+rs+lrs) k x lr r)
-                     | otherwise -> Bin (1+ls+rs) lrk lrx (Bin (1+lls+mapSize lrl) lk lx ll lrl) (Bin (1+rs+mapSize lrr) k x lrr r)
+                     # (lrls, lrl) = mapSizeU lrl
+                     # (lrrs, lrr) = mapSizeU lrr
+                     | otherwise -> Bin (1+ls+rs) lrk lrx (Bin (1+lls+lrls) lk lx ll lrl) (Bin (1+rs+lrrs) k x lrr r)
                    (_, _) -> abort "Failure in Data.Map.balance"
               | otherwise -> Bin (1+ls+rs) k x l r
 
@@ -1997,18 +2009,18 @@ getU k (Bin h nk nv left right)
     #! (mbv, right) = getU k right
     = (mbv, Bin h nk nv left right)
 
-delU :: !a !.(Map a b) -> u:(!v:(Maybe b), !Map a b) | == a & < a, [u <= v]
+delU :: !k !w:(Map k u:v) -> x:(Maybe u:v, !y:(Map k u:v)) | == k & < k, [ w y <= u, x <= y, w <= y]
 delU k Tip = (Nothing, Tip)              //Do nothing
 delU k (Bin h nk nv Tip Tip)            //A node with just leaves as children can be safely removed
-  | k == nk = (Just nv, Tip)
-             = (Nothing, Bin h nk nv Tip Tip)
+	| k == nk   = (Just nv, Tip)
+	| otherwise = (Nothing, Bin h nk nv Tip Tip)
 delU k (Bin h nk nv Tip right)            //A node without smaller items
-  | k == nk = (Just nv, right)            //When found, just remove
-  | k < nk   = (Nothing, Bin h nk nv Tip right)  //Do nothing, k is not in the mapping
-  | otherwise
-    #! (mbv, right)    = delU k right
-    #! (hright, right) = height right
-    = (mbv, balance nk nv Tip right)
+	| k == nk = (Just nv, right)            //When found, just remove
+	| k < nk  = (Nothing, Bin h nk nv Tip right)  //Do nothing, k is not in the mapping
+	| otherwise
+		#! (mbv, right)    = delU k right
+		#! (hright, right) = height right
+		= (mbv, balance nk nv Tip right)
 delU k (Bin h nk nv left Tip)						//A node without larger items
 	| k == nk	= (Just nv, left)						//When found just remove
 	| k < nk	
@@ -2033,17 +2045,17 @@ delU k (Bin h nk nv left right)						//A node with both larger and smaller items
 		= (mbv, balance nk nv left right)
 where // TODO
 	//Takes the k and v values from the maximum node in the tree and removes that node
-    takeMax :: !(Map a b) -> (!Map a b, !a, !b)
+	takeMax :: !u:(Map k v:v) -> (!u:Map k v:v, !k, !v:v), [u <= v]
 	takeMax Tip = abort "takeMax of leaf evaluated" 
 	takeMax (Bin _ nk nv left Tip)	= (left, nk, nv)
 	takeMax (Bin _ nk nv left right)
-      #! (right,k,v)    = takeMax right
-      #! (hleft,left)   = height left
-      #! (hright,right) = height right
-      = (balance nk nv left right, k, v)
+		#! (right,k,v)    = takeMax right
+		#! (hleft,left)   = height left
+		#! (hright,right) = height right
+		= (balance nk nv left right, k, v)
 
 	//Determines the height of the parent node of two sub trees
-    parentHeight :: !(Map a b) !(Map c d) -> (!Int, !Map a b, !Map c d)
+	parentHeight :: !u:(Map a v:b) !u:(Map c v:d) -> (!Int, !u:Map a v:b, !u:Map c v:d)
 	parentHeight left right
 		#! (hleft,left)   = height left
 		#! (hright,right) = height right
@@ -2051,8 +2063,8 @@ where // TODO
 		= (h, left, right)
 
 height :: !u:(Map k w:v) -> x:(!Int, !y:(Map k w:v)), [u y <= w, x <= y, u <= y]
-height Tip                    = (0, Tip)
-height (Bin h k v left right) = (h, Bin h k v left right)
+height m=:Tip             = (0, m)
+height m=:(Bin h _ _ _ _) = (h, m)
 
 gEq{|Map|} fk fv mx my = mapSize mx == mapSize my && and [fk kx ky && fv vx vy \\ (kx,vx) <- toList mx & (ky,vy) <- toList my]