diff --git a/src/libraries/OS-Independent/Data/Map.dcl b/src/libraries/OS-Independent/Data/Map.dcl index e2df242e030cb3f955b4d01c041691df6bfcaaf4..87921c584b9b8118bf9413534b06bb5faea336bf 100644 --- a/src/libraries/OS-Independent/Data/Map.dcl +++ b/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 /** diff --git a/src/libraries/OS-Independent/Data/Map.icl b/src/libraries/OS-Independent/Data/Map.icl index 3eb06e901a4cef1907c56d4943b3095f90d7d3e6..0940555c335dd7cf7ab421d0a566717c42f941e6 100644 --- a/src/libraries/OS-Independent/Data/Map.icl +++ b/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