git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
aa69931Edwin Brady
libs/base/Data/Fun.idr+4
compare with master
unifiedsplit
@@ -6,3 +6,7 @@ module Data.Fun
6Fun : Vect n Type -> Type -> Type
6Fun : Vect n Type -> Type -> Type
7Fun [] r = r
7Fun [] r = r
8Fun (t::ts) r = t -> Fun ts r
8Fun (t::ts) r = t -> Fun ts r
9+
10+target : {ts : Vect n Type} -> Fun ts r -> Type
11+target {r} _ = r
12+
libs/base/Data/SortedMap.idr+6−4
@@ -183,11 +183,13 @@ treeDelete {n=(S (S _))} k (Branch3 t1 k1 t2 k2 t3) =
183 Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
183 Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
184 Right t3' => Left (merge3 t1 k1 t2 k2 t3')
184 Right t3' => Left (merge3 t1 k1 t2 k2 t3')
185
185
186−-- FIXME: this is very inefficient
187treeToList : Ord k => Tree n k v -> List (k, v)
186treeToList : Ord k => Tree n k v -> List (k, v)
188−treeToList (Leaf k v) = [(k, v)]
187+treeToList = treeToList' (:: [])
188+ where
189+ treeToList' : Ord k => ((k, v) -> List (k, v)) -> Tree n k v -> List (k, v)
190+ treeToList' cont (Leaf k v) = cont (k, v)
189−treeToList (Branch2 t1 _ t2) = treeToList t1 ++ treeToList t2
191+ treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1
190−treeToList (Branch3 t1 _ t2 _ t3) = treeToList t1 ++ treeToList t2 ++ treeToList t3
192+ treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1
191
193
192data SortedMap : Type -> Type -> Type where
194data SortedMap : Type -> Type -> Type where
193 Empty : SortedMap k v
195 Empty : SortedMap k v
libs/prelude/Prelude/Bits.idr+13−21
@@ -8,26 +8,18 @@ import Prelude.Bool
8%default total
8%default total
9
9
10
10
11−private
12−toHexDigit : Fin 16 -> Char
13−toHexDigit n = index n hexVect where
14− hexVect : Vect 16 Char
15− hexVect = ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9',
16− 'A', 'B', 'C', 'D', 'E', 'F']
17−
18b8ToString : Bits8 -> String
11b8ToString : Bits8 -> String
19−b8ToString c = pack (with List [c1, c2]) where
12+b8ToString c = pack (with List [c1, c2])
20− %assert_total -- We will only supply numbers that can fit in 4 bits
13+ where getDigit : Bits8 -> Char
21− toFin16 : Bits8 -> Fin 16
14+ getDigit b = let n = prim__zextB8_Int b in
22− toFin16 n = if n == 0
15+ if n >= 0 && n <= 9
23− then fZ
16+ then '0' `prim__addChar` cast n
24− else believe_me (fS (toFin16 (n-1)))
17+ else if n >= 10 && n <= 15
25− c1 = toHexDigit upper where
18+ then 'A' `prim__addChar` cast (n - 10)
26− upper : Fin 16
19+ else '?' -- this is for totality - it should not happen
27− upper = toFin16 (prim__lshrB8 c 4)
20+ c1 = getDigit (prim__andB8 (prim__lshrB8 c 4) 15)
28− c2 = toHexDigit lower where
29− lower : Fin 16
30− lower = toFin16 (prim__andB8 c 0xf)
21+ c2 = getDigit (prim__andB8 c 15)
22+
31
23
32b16ToString : Bits16 -> String
24b16ToString : Bits16 -> String
33b16ToString c = c1 ++ c2 where
25b16ToString c = c1 ++ c2 where
@@ -42,7 +34,7 @@ b32ToString : Bits32 -> String
42b32ToString c = c1 ++ c2 where
34b32ToString c = c1 ++ c2 where
43 c1 = b16ToString upper where
35 c1 = b16ToString upper where
44 upper : Bits16
36 upper : Bits16
45− upper = prim__truncB32_B16 (prim__lshrB32 c 16)
37+ upper = prim__truncB32_B16 (prim__andB32 (prim__lshrB32 c 16) 0x0000ffff)
46 c2 = b16ToString lower where
38 c2 = b16ToString lower where
47 lower : Bits16
39 lower : Bits16
48 lower = prim__truncB32_B16 c
40 lower = prim__truncB32_B16 c
@@ -51,7 +43,7 @@ b64ToString : Bits64 -> String
51b64ToString c = c1 ++ c2 where
43b64ToString c = c1 ++ c2 where
52 c1 = b32ToString upper where
44 c1 = b32ToString upper where
53 upper : Bits32
45 upper : Bits32
54− upper = prim__truncB64_B32 (prim__lshrB64 c 32)
46+ upper = prim__truncB64_B32 (prim__andB64 (prim__lshrB64 c 32) 0x00000000ffffffff)
55 c2 = b32ToString lower where
47 c2 = b32ToString lower where
56 lower : Bits32
48 lower : Bits32
57 lower = prim__truncB64_B32 c
49 lower = prim__truncB64_B32 c
libs/prelude/Prelude/List.idr+17
@@ -269,6 +269,23 @@ intersperse sep (x::xs) = x :: intersperse' sep xs
269intercalate : List a -> List (List a) -> List a
269intercalate : List a -> List (List a) -> List a
270intercalate sep l = concat $ intersperse sep l
270intercalate sep l = concat $ intersperse sep l
271
271
272+-- | Transposes rows and columns of a list of lists.
273+--
274+-- > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]
275+--
276+-- This also works for non square scenarios, thus
277+-- involution does not always hold:
278+--
279+-- > transpose [[], [1, 2]] = [[1], [2]]
280+-- > transpose (transpose [[], [1, 2]]) = [[1, 2]]
281+--
282+-- TODO: Solution which satisfies the totality checker?
283+%assert_total
284+transpose : List (List a) -> List (List a)
285+transpose [] = []
286+transpose ([] :: xss) = transpose xss
287+transpose ((x::xs) :: xss) = (x :: (mapMaybe head' xss)) :: (transpose (xs :: (map (drop 1) xss)))
288+
272--------------------------------------------------------------------------------
289--------------------------------------------------------------------------------
273-- Membership tests
290-- Membership tests
274--------------------------------------------------------------------------------
291--------------------------------------------------------------------------------