git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
commitaa69931d369b8557e2c16e2a3fbfaa0274e8948a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 27 Feb 2014, 11:10 (13 years ago) parentc15d4cb3bc4846
4 files changed+40−25
compare with master
unifiedsplit
libs/base/Data/Fun.idr+4 libs/base/Data/SortedMap.idr+6−4 libs/prelude/Prelude/Bits.idr+13−21 libs/prelude/Prelude/List.idr+17
libs/base/Data/Fun.idr+4
@@ -6,3 +6,7 @@ module Data.Fun
66Fun : Vect n Type -> Type -> Type
77Fun [] r = r
88Fun (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) =
183183 Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
184184 Right t3' => Left (merge3 t1 k1 t2 k2 t3')
185185
186−-- FIXME: this is very inefficient
187186treeToList : Ord k => Tree n k v -> List (k, v)
188−treeToList (Leaf k v) = [(k, v)]
189−treeToList (Branch2 t1 _ t2) = treeToList t1 ++ treeToList t2
190−treeToList (Branch3 t1 _ t2 _ t3) = treeToList t1 ++ treeToList t2 ++ treeToList t3
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)
191+ treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1
192+ treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1
191193
192194data SortedMap : Type -> Type -> Type where
193195 Empty : SortedMap k v
libs/prelude/Prelude/Bits.idr+13−21
@@ -8,26 +8,18 @@ import Prelude.Bool
88%default total
99
1010
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−
1811b8ToString : Bits8 -> String
19−b8ToString c = pack (with List [c1, c2]) where
20− %assert_total -- We will only supply numbers that can fit in 4 bits
21− toFin16 : Bits8 -> Fin 16
22− toFin16 n = if n == 0
23− then fZ
24− else believe_me (fS (toFin16 (n-1)))
25− c1 = toHexDigit upper where
26− upper : Fin 16
27− upper = toFin16 (prim__lshrB8 c 4)
28− c2 = toHexDigit lower where
29− lower : Fin 16
30− lower = toFin16 (prim__andB8 c 0xf)
12+b8ToString c = pack (with List [c1, c2])
13+ where getDigit : Bits8 -> Char
14+ getDigit b = let n = prim__zextB8_Int b in
15+ if n >= 0 && n <= 9
16+ then '0' `prim__addChar` cast n
17+ else if n >= 10 && n <= 15
18+ then 'A' `prim__addChar` cast (n - 10)
19+ else '?' -- this is for totality - it should not happen
20+ c1 = getDigit (prim__andB8 (prim__lshrB8 c 4) 15)
21+ c2 = getDigit (prim__andB8 c 15)
22+
3123
3224b16ToString : Bits16 -> String
3325b16ToString c = c1 ++ c2 where
@@ -42,7 +34,7 @@ b32ToString : Bits32 -> String
4234b32ToString c = c1 ++ c2 where
4335 c1 = b16ToString upper where
4436 upper : Bits16
45− upper = prim__truncB32_B16 (prim__lshrB32 c 16)
37+ upper = prim__truncB32_B16 (prim__andB32 (prim__lshrB32 c 16) 0x0000ffff)
4638 c2 = b16ToString lower where
4739 lower : Bits16
4840 lower = prim__truncB32_B16 c
@@ -51,7 +43,7 @@ b64ToString : Bits64 -> String
5143b64ToString c = c1 ++ c2 where
5244 c1 = b32ToString upper where
5345 upper : Bits32
54− upper = prim__truncB64_B32 (prim__lshrB64 c 32)
46+ upper = prim__truncB64_B32 (prim__andB64 (prim__lshrB64 c 32) 0x00000000ffffffff)
5547 c2 = b32ToString lower where
5648 lower : Bits32
5749 lower = prim__truncB64_B32 c
libs/prelude/Prelude/List.idr+17
@@ -269,6 +269,23 @@ intersperse sep (x::xs) = x :: intersperse' sep xs
269269intercalate : List a -> List (List a) -> List a
270270intercalate sep l = concat $ intersperse sep l
271271
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+
272289--------------------------------------------------------------------------------
273290-- Membership tests
274291--------------------------------------------------------------------------------