adapt type of singleton/put to work on maps with unique values

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

@@ -151,7 +151,7 @@ newMap      :: w:(Map k u:v), [ w <= u]
  * Create a Map with one element.
  * @complexity O(1)
  */
-singleton   :: !k !v -> Map k v
+singleton :: !k !v:v -> u:Map k v:v, [u <= v]
 
 /**
  * The number of elements in a Map.
@@ -182,7 +182,7 @@ mapSizeU :: !u:(Map k v:v) -> (!Int, !u:Map k v:v), [u <= v]
  *         m` = put k v m
  * @complexity O(log n)
  */
-put :: !k !a !(Map k a) -> Map k a | < k
+put :: !k !v:v !u:(Map k v:v) -> u:Map k v:v | < k
 	special k=Int; k=String
 
 /**

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

@@ -159,11 +159,11 @@ getGE k m = goNothing k m
 newMap :: w:(Map k u:v), [ w <= u]
 newMap = Tip
 
-singleton :: !k !a -> Map k a
+singleton :: !k !v:v -> u:Map k v:v, [u <= v]
 singleton k x = Bin 1 k x Tip Tip
 
 // See Note: Type of local 'go' function
-put :: !k !a !(Map k a) -> Map k a | < k
+put :: !k !v:v !u:(Map k v:v) -> u:Map k v:v | < k
 put kx x Tip               = singleton kx x
 put kx x (Bin sz ky y l r) =
   if (kx < ky)
@@ -1744,7 +1744,7 @@ balance k x l r = case l of
 
 // balanceL is called when left subtree might have been puted to or when
 // right subtree might have been deleted from.
-balanceL :: !k !a !(Map k a) !(Map k a) -> Map k a
+balanceL :: !k !v:v !u:(Map k v:v) !u:(Map k v:v) -> u:Map k v:v, [u <= v]
 balanceL k x l r = case r of
   Tip -> case l of
            Tip -> Bin 1 k x Tip Tip
@@ -1753,22 +1753,26 @@ balanceL k x l r = case r of
            (Bin _ lk lx ll=:(Bin _ _ _ _ _) Tip) -> Bin 3 lk lx ll (Bin 1 k x Tip Tip)
            (Bin ls lk lx 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 _ _ _ _) -> case l of
            Tip -> Bin (1+rs) k x Tip r
 
            (Bin ls lk lx ll lr)
               | 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.balanceL"
               | otherwise -> Bin (1+ls+rs) k x l r
 
 // balanceR is called when right subtree might have been puted to or when
 // left subtree might have been deleted from.
-balanceR :: !k !a !(Map k a) !(Map k a) -> Map k a
+balanceR :: !k !v:v !u:(Map k v:v) !u:(Map k v:v) -> u:Map k v:v, [u <= v]
 balanceR k x l r = case l of
   Tip -> case r of
            Tip -> Bin 1 k x Tip Tip
@@ -1777,16 +1781,20 @@ balanceR 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 _ _ _ _) -> case r of
            Tip -> Bin (1+ls) k x l 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.balanceR"
               | otherwise -> Bin (1+ls+rs) k x l r