Merge pull request #1408 from ahmadsalim/bug/sortedmap
Fixed bug regarding insertion in SortedMap.
commita0ba488ee99af9e7ac0b2e578b1469814901f8cd
authorDavid Christiansen <david@davidchristiansen.dk>
dateSat 19 Jul 2014, 23:14 (12 years ago)
parent8b66f2a927cca7
libs/base/Data/SortedMap.idr+1−1
@@ -114,7 +114,7 @@ treeInsert' k v (Branch3 t1 k1 t2 k2 t3) =
114114 else
115115 case treeInsert' k v t3 of
116116 Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
117− Right (a, b, c) => Right (Branch2 t1 k2 t2, k2, Branch2 a b c)
117+ Right (a, b, c) => Right (Branch2 t1 k1 t2, k2, Branch2 a b c)
118118
119119treeInsert : Ord k => k -> v -> Tree n k v -> Either (Tree n k v) (Tree (S n) k v)
120120treeInsert k v t =
test/reg048/expectednew file
No changes to the content.
test/reg048/reg048.idrnew file+24
@@ -0,0 +1,24 @@
1+module Main
2+import Data.SortedMap
3+
4+test : List Int -> IO ()
5+test xs = do let lst = Data.SortedMap.toList mp
6+ if length lst /= n
7+ then putStrLn $ "wrong length for " ++ show xs
8+ else do let res = map (\x => lookup x mp) xs
9+ let found = mapMaybe id res
10+ if length found /= n
11+ then putStrLn $ "some lost in " ++ show xs ++ ": res=" ++ show res
12+ ++ " toList=" ++ show lst
13+ else return ()
14+
15+ where
16+ mp : SortedMap Int ()
17+ mp = foldr (\x => \m => insert x () m) empty xs
18+ n : Nat
19+ n = length xs
20+
21+main : IO ()
22+main = do test [1,2,3]
23+ test [4,3,2,1]
24+ test [1,2,3,4]
test/reg048/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+idris $@ reg048.idr -o reg048
3+./reg048
4+rm -f reg048 *.ibc