b265313 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Take and drop ported from list library to vectors. Function catMaybes causes Idris to diverge upon type checking in the REPL.

b265313Dominic Mulligan15 years ago

lib/prelude/vect.idr+25−2

compare with master

unifiedsplit

@@ -36,6 +36,21 @@ index (fS k) (x::xs) = index k xs

36index fO [] impossible

37index (fS _) [] impossible

39+--------------------------------------------------------------------------------

40+-- Subvectors

41+--------------------------------------------------------------------------------

42+

43+take : Fin n -> Vect a n -> (p ** Vect a p)

44+take fO xs = (_ ** [])

45+take (fS k) [] impossible

46+take (fS k) (x::xs) with (take k xs)

47+ | (_ ** tail) = (_ ** x::tail)

48+

49+drop : Fin n -> Vect a n -> (p ** Vect a p)

50+drop fO xs = (_ ** xs)

51+drop (fS k) [] impossible

52+drop (fS k) (x::xs) = drop k xs

53+

39--------------------------------------------------------------------------------

54--------------------------------------------------------------------------------

40-- Conversions to and from list

55-- Conversions to and from list

41--------------------------------------------------------------------------------

56--------------------------------------------------------------------------------

@@ -64,6 +79,16 @@ total map : (a -> b) -> Vect a n -> Vect b n

64map f [] = []

79map f [] = []

65map f (x::xs) = f x :: map f xs

80map f (x::xs) = f x :: map f xs

82+-- XXX: causes Idris to enter an infinite loop when type checking in the REPL

83+--mapMaybe : (a -> Maybe b) -> Vect a n -> (p ** Vect b p)

84+--mapMaybe f [] = (_ ** [])

85+--mapMaybe f (x::xs) = mapMaybe' (f x)

86+-- XXX: working around the type restrictions on case statements

87+-- where

88+-- mapMaybe' : (Maybe b) -> (n ** Vect b n) -> (p ** Vect b p)

89+-- mapMaybe' Nothing (n ** tail) = (n ** tail)

90+-- mapMaybe' (Just j) (n ** tail) = (S n ** j::tail)

91+

67--------------------------------------------------------------------------------

92--------------------------------------------------------------------------------

68-- Folds

93-- Folds

69--------------------------------------------------------------------------------

94--------------------------------------------------------------------------------

@@ -217,8 +242,6 @@ nub = nubBy (==)

217-- Splitting and breaking lists

242-- Splitting and breaking lists

218--------------------------------------------------------------------------------

243--------------------------------------------------------------------------------

219

244

220−-- XXX: todo

221−

222--------------------------------------------------------------------------------

245--------------------------------------------------------------------------------

223-- Predicates

246-- Predicates

224--------------------------------------------------------------------------------

247--------------------------------------------------------------------------------