git.iko.soy/Idris-dev
on master help sign in
Fixed bug regarding insertion in SortedMap.
927cca7Ahmad Salim Al-Sibahi
libs/base/Data/SortedMap.idr+1−1
compare with master
unifiedsplit
@@ -114,7 +114,7 @@ treeInsert' k v (Branch3 t1 k1 t2 k2 t3) =
114 else
114 else
115 case treeInsert' k v t3 of
115 case treeInsert' k v t3 of
116 Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
116 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)
118
118
119treeInsert : Ord k => k -> v -> Tree n k v -> Either (Tree n k v) (Tree (S n) k v)
119treeInsert : Ord k => k -> v -> Tree n k v -> Either (Tree n k v) (Tree (S n) k v)
120treeInsert k v t =
120treeInsert 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