61d39da · Idris-dev · git.iko.soy

CHANGELOG+2

compare with master

unifiedsplit

@@ -11,6 +11,8 @@ New in 0.9.9:

11* Added Data.HVect module

12* Fix fromInteger to take an Integer, rather than an Int

13* Integer literals for Fin

14+* Renamed O to Z, and fO to fZ

15+* Swapped Vect arguments, now Vect : Nat -> Type -> Type

14

16

15Internal changes

17Internal changes

16

18

effects/Effect/Memory.idr+6−6

@@ -21,9 +21,9 @@ data RawMemory : Effect where

21 Peek : (offset : Nat) ->

22 (size : Nat) ->

23 so (offset + size <= i) ->

24− RawMemory (MemoryChunk n i) (MemoryChunk n i) (Vect Bits8 size)

24+ RawMemory (MemoryChunk n i) (MemoryChunk n i) (Vect size Bits8)

25 Poke : (offset : Nat) ->

26− (Vect Bits8 size) ->

26+ (Vect size Bits8) ->

27 so (offset <= i && offset + size <= n) ->

28 RawMemory (MemoryChunk n i) (MemoryChunk n (max i (offset + size))) ()

29 Move : (src : MemoryChunk src_size src_init) ->

@@ -62,7 +62,7 @@ do_memmove dest src dest_offset src_offset size

62 dest src (fromInteger $ cast dest_offset) (fromInteger $ cast src_offset) (fromInteger $ cast size)

63

64private

65−do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect Bits8 size)

65+do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect size Bits8)

66do_peek _ _ Z = return (Prelude.Vect.Nil)

67do_peek ptr offset (S n)

68 = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FByte) ptr (fromInteger $ cast offset)

@@ -70,7 +70,7 @@ do_peek ptr offset (S n)

70 Prelude.Monad.return (Prelude.Vect.(::) b bs)

71

72private

73−do_poke : Ptr -> Nat -> Vect Bits8 size -> IO ()

73+do_poke : Ptr -> Nat -> Vect size Bits8 -> IO ()

74do_poke _ _ [] = return ()

75do_poke ptr offset (b::bs)

76 = do mkForeign (FFun "idris_poke" [FPtr, FInt, FByte] FUnit) ptr (fromInteger $ cast offset) b

@@ -117,13 +117,13 @@ peek : {i : Nat} ->

117 (offset : Nat) ->

118 (size : Nat) ->

119 so (offset + size <= i) ->

120− Eff m [RAW_MEMORY (MemoryChunk n i)] (Vect Bits8 size)

120+ Eff m [RAW_MEMORY (MemoryChunk n i)] (Vect size Bits8)

121peek offset size prf = Peek offset size prf

122

123poke : {n : Nat} ->

124 {i : Nat} ->

125 (offset : Nat) ->

126− Vect Bits8 size ->

126+ Vect size Bits8 ->

127 so (offset <= i && offset + size <= n) ->

128 EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY (MemoryChunk n (max i (offset + size)))] ()

129poke offset content prf = Poke offset content prf

javascript/JavaScript/JSON.idr+3−3

@@ -3,7 +3,7 @@ module JSON

3import Data.SortedMap

4

5data JSONType : Type where

6− JSONArray : (n : Nat) -> Vect JSONType n -> JSONType

6+ JSONArray : (n : Nat) -> Vect n JSONType -> JSONType

7 JSONString : JSONType

8 JSONNumber : JSONType

9 JSONBool : JSONType

@@ -11,9 +11,9 @@ data JSONType : Type where

11 JSONNull : JSONType

12

13mutual

14− using (ts : Vect JSONType n, fs : SortedMap String JSONType)

14+ using (ts : Vect n JSONType, fs : SortedMap String JSONType)

15 namespace JArray

16− data JArray : (n : Nat) -> Vect JSONType n -> Type where

16+ data JArray : (n : Nat) -> Vect n JSONType -> Type where

17 Nil : JArray 0 []

18 (::) : JSON t -> JArray n ts -> JArray (S n) (t :: ts)

19

lib/Data/HVect.idr+6−6

@@ -5,8 +5,8 @@ import Data.Vect

5%access public

6%default total

7

8−using (k : Nat, ts : Vect Type k)

8+using (k : Nat, ts : Vect k Type)

9− data HVect : Vect Type k -> Type where

9+ data HVect : Vect k Type -> Type where

10 Nil : HVect []

11 (::) : t -> HVect ts -> HVect (t::ts)

12

@@ -14,7 +14,7 @@ using (k : Nat, ts : Vect Type k)

14 index fZ (x::xs) = x

15 index (fS j) (x::xs) = index j xs

16

17− deleteAt : {us : Vect Type (S l)} -> (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)

17+ deleteAt : {us : Vect (S l) Type} -> (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)

18 deleteAt fZ (x::xs) = xs

19 deleteAt {l = S m} (fS j) (x::xs) = x :: deleteAt j xs

20 deleteAt _ [] impossible

@@ -27,7 +27,7 @@ using (k : Nat, ts : Vect Type k)

27 updateAt fZ f (x::xs) = f x :: xs

28 updateAt (fS j) f (x::xs) = x :: updateAt j f xs

29

30− (++) : {us : Vect Type l} -> HVect ts -> HVect us -> HVect (ts ++ us)

30+ (++) : {us : Vect l Type} -> HVect ts -> HVect us -> HVect (ts ++ us)

31 (++) [] ys = ys

32 (++) (x::xs) ys = x :: (xs ++ ys)

33

@@ -37,8 +37,8 @@ using (k : Nat, ts : Vect Type k)

37 instance (Eq t, Eq (HVect ts)) => Eq (HVect (t::ts)) where

38 (x::xs) == (y::ys) = x == y && xs == ys

39

40− class Shows (k : Nat) (ts : Vect Type k) where

40+ class Shows (k : Nat) (ts : Vect k Type) where

41− shows : HVect ts -> Vect String k

41+ shows : HVect ts -> Vect k String

42

43 instance Shows Z [] where

44 shows [] = []

lib/Data/Vect.idr+7−6

@@ -9,24 +9,25 @@ import Language.Reflection

9-- Elem

10--------------------------------------------------------------------------------

11

12+using (xs : Vect k a)

12−data Elem : a -> Vect a k -> Type where

13+ data Elem : a -> Vect k a -> Type where

13− Here : {xs : Vect a k} -> Elem x (x::xs)

14+ Here : Elem x (x::xs)

14− There : {xs : Vect a k} -> Elem x xs -> Elem x (y::xs)

15+ There : Elem x xs -> Elem x (y::xs)

15

16

16findElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic

17findElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic

17findElem Z ctxt goal = Refine "Here" `Seq` Solve

18findElem Z ctxt goal = Refine "Here" `Seq` Solve

18findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))

19findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))

19

20

20−replaceElem : (xs : Vect t k) -> Elem x xs -> (y : t) -> (ys : Vect t k ** Elem y ys)

21+replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> (ys : Vect k t ** Elem y ys)

21replaceElem (x::xs) Here y = (y :: xs ** Here)

22replaceElem (x::xs) Here y = (y :: xs ** Here)

22replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)

23replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)

23 | (ys ** yinys) = (x :: ys ** There yinys)

24 | (ys ** yinys) = (x :: ys ** There yinys)

24

25

25−replaceByElem : (xs : Vect t k) -> Elem x xs -> t -> Vect t k

26+replaceByElem : (xs : Vect k t) -> Elem x xs -> t -> Vect k t

26replaceByElem (x::xs) Here y = y :: xs

27replaceByElem (x::xs) Here y = y :: xs

27replaceByElem (x::xs) (There xinxs) y = x :: replaceByElem xs xinxs y

28replaceByElem (x::xs) (There xinxs) y = x :: replaceByElem xs xinxs y

28

29

29−mapElem : {xs : Vect t k} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs)

30+mapElem : {xs : Vect k t} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs)

30mapElem Here = Here

31mapElem Here = Here

31mapElem (There e) = There (mapElem e)

32mapElem (There e) = There (mapElem e)

32

33

lib/Data/Vect/Quantifiers.idr+11−11

@@ -1,18 +1,18 @@

1module Data.Vect.Quantifiers

2

3−data Any : (P : a -> Type) -> Vect a n -> Type where

3+data Any : (P : a -> Type) -> Vect n a -> Type where

4− Here : {P : a -> Type} -> {xs : Vect a n} -> P x -> Any P (x :: xs)

4+ Here : {P : a -> Type} -> {xs : Vect n a} -> P x -> Any P (x :: xs)

5− There : {P : a -> Type} -> {xs : Vect a n} -> Any P xs -> Any P (x :: xs)

5+ There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)

6

7anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_

8anyNilAbsurd Here impossible

9anyNilAbsurd There impossible

10

11−anyElim : {xs : Vect a n} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b

11+anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b

12anyElim _ f (Here p) = f p

13anyElim f _ (There p) = f p

14

15−any : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect a n) -> Dec (Any P xs)

15+any : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (Any P xs)

16any _ Nil = No anyNilAbsurd

17any p (x::xs) with (p x)

18 | Yes prf = Yes (Here prf)

@@ -21,23 +21,23 @@ any p (x::xs) with (p x)

21 Yes prf' => Yes (There prf')

22 No prf' => No (anyElim prf' prf)

23

24−data All : (P : a -> Type) -> Vect a n -> Type where

24+data All : (P : a -> Type) -> Vect n a -> Type where

25 Nil : {P : a -> Type} -> All P Nil

26− (::) : {P : a -> Type} -> {xs : Vect a n} -> P x -> All P xs -> All P (x :: xs)

26+ (::) : {P : a -> Type} -> {xs : Vect n a} -> P x -> All P xs -> All P (x :: xs)

27

28−negAnyAll : {P : a -> Type} -> {xs : Vect a n} -> Not (Any P xs) -> All (\x => Not (P x)) xs

28+negAnyAll : {P : a -> Type} -> {xs : Vect n a} -> Not (Any P xs) -> All (\x => Not (P x)) xs

29negAnyAll {xs=Nil} _ = Nil

30negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))

31

32−notAllHere : {P : a -> Type} -> {xs : Vect a n} -> Not (P x) -> All P (x :: xs) -> _|_

32+notAllHere : {P : a -> Type} -> {xs : Vect n a} -> Not (P x) -> All P (x :: xs) -> _|_

33notAllHere _ Nil impossible

34notAllHere np (p :: _) = np p

35

36−notAllThere : {P : a -> Type} -> {xs : Vect a n} -> Not (All P xs) -> All P (x :: xs) -> _|_

36+notAllThere : {P : a -> Type} -> {xs : Vect n a} -> Not (All P xs) -> All P (x :: xs) -> _|_

37notAllThere _ Nil impossible

38notAllThere np (_ :: ps) = np ps

39

40−all : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect a n) -> Dec (All P xs)

40+all : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs)

41all _ Nil = Yes Nil

42all d (x::xs) with (d x)

43 | No prf = No (notAllHere prf)

lib/Prelude.idr+2−2

@@ -167,9 +167,9 @@ instance Show a => Show (List a) where

167 show' acc [x] = acc ++ show x

168 show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs

169

170−instance Show a => Show (Vect a n) where

170+instance Show a => Show (Vect n a) where

171 show xs = "[" ++ show' xs ++ "]" where

172− show' : Vect a n -> String

172+ show' : Vect n a -> String

173 show' [] = ""

174 show' [x] = show x

175 show' (x :: xs) = show x ++ ", " ++ show' xs

lib/Prelude/Vect.idr+62−62

@@ -9,39 +9,39 @@ import Prelude.Nat

9

10infixr 7 ::

11

12−data Vect : Type -> Nat -> Type where

12+data Vect : Nat -> Type -> Type where

13− Nil : Vect a Z

13+ Nil : Vect Z a

14− (::) : a -> Vect a n -> Vect a (S n)

14+ (::) : a -> Vect n a -> Vect (S n) a

15

16--------------------------------------------------------------------------------

17-- Indexing into vectors

18--------------------------------------------------------------------------------

19

20−tail : Vect a (S n) -> Vect a n

20+tail : Vect (S n) a -> Vect n a

21tail (x::xs) = xs

22

23−head : Vect a (S n) -> a

23+head : Vect (S n) a -> a

24head (x::xs) = x

25

26−last : Vect a (S n) -> a

26+last : Vect (S n) a -> a

27last (x::[]) = x

28last (x::y::ys) = last $ y::ys

29

30−init : Vect a (S n) -> Vect a n

30+init : Vect (S n) a -> Vect n a

31init (x::[]) = []

32init (x::y::ys) = x :: init (y::ys)

33

34−index : Fin n -> Vect a n -> a

34+index : Fin n -> Vect n a -> a

35index fZ (x::xs) = x

36index (fS k) (x::xs) = index k xs

37index fZ [] impossible

38

39−deleteAt : Fin (S n) -> Vect a (S n) -> Vect a n

39+deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a

40deleteAt fZ (x::xs) = xs

41deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs

42deleteAt _ [] impossible

43

44−replaceAt : Fin n -> t -> Vect t n -> Vect t n

44+replaceAt : Fin n -> t -> Vect n t -> Vect n t

45replaceAt fZ y (x::xs) = y::xs

46replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs

47

@@ -49,13 +49,13 @@ replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs

49-- Subvectors

50--------------------------------------------------------------------------------

51

52−take : Fin n -> Vect a n -> (p ** Vect a p)

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

53take fZ xs = (_ ** [])

54take (fS k) [] impossible

55take (fS k) (x::xs) with (take k xs)

56 | (_ ** tail) = (_ ** x::tail)

57

58−drop : Fin n -> Vect a n -> (p ** Vect a p)

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

59drop fZ xs = (_ ** xs)

60drop (fS k) [] impossible

61drop (fS k) (x::xs) = drop k xs

@@ -64,11 +64,11 @@ drop (fS k) (x::xs) = drop k xs

64-- Conversions to and from list

65--------------------------------------------------------------------------------

66

67−toList : Vect a n -> List a

67+toList : Vect n a -> List a

68toList [] = []

69toList (x::xs) = x :: toList xs

70

71−fromList : (l : List a) -> Vect a (length l)

71+fromList : (l : List a) -> Vect (length l) a

72fromList [] = []

73fromList (x::xs) = x :: fromList xs

74

@@ -76,11 +76,11 @@ fromList (x::xs) = x :: fromList xs

76-- Building (bigger) vectors

77--------------------------------------------------------------------------------

78

79−(++) : Vect a m -> Vect a n -> Vect a (m + n)

79+(++) : Vect m a -> Vect n a -> Vect (m + n) a

80(++) [] ys = ys

81(++) (x::xs) ys = x :: xs ++ ys

82

83−replicate : (n : Nat) -> a -> Vect a n

83+replicate : (n : Nat) -> a -> Vect n a

84replicate Z x = []

85replicate (S k) x = x :: replicate k x

86

@@ -88,14 +88,14 @@ replicate (S k) x = x :: replicate k x

88-- Zips and unzips

89--------------------------------------------------------------------------------

90

91−zipWith : (a -> b -> c) -> Vect a n -> Vect b n -> Vect c n

91+zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c

92zipWith f [] [] = []

93zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys

94

95−zip : Vect a n -> Vect b n -> Vect (a, b) n

95+zip : Vect n a -> Vect n b -> Vect n (a, b)

96zip = zipWith (\x => \y => (x,y))

97

98−unzip : Vect (a, b) n -> (Vect a n, Vect b n)

98+unzip : Vect n (a, b) -> (Vect n a, Vect n b)

99unzip [] = ([], [])

100unzip ((l, r)::xs) with (unzip xs)

101 | (lefts, rights) = (l::lefts, r::rights)

@@ -104,12 +104,12 @@ unzip ((l, r)::xs) with (unzip xs)

104-- Maps

105--------------------------------------------------------------------------------

106

107−map : (a -> b) -> Vect a n -> Vect b n

107+map : (a -> b) -> Vect n a -> Vect n b

108map f [] = []

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

110

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

112−--mapMaybe : (a -> Maybe b) -> Vect a n -> (p ** Vect b p)

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

113--mapMaybe f [] = (_ ** [])

114--mapMaybe f (x::xs) = mapMaybe' (f x)

115-- XXX: working around the type restrictions on case statements

@@ -122,11 +122,11 @@ map f (x::xs) = f x :: map f xs

122-- Folds

123--------------------------------------------------------------------------------

124

125−total foldl : (a -> b -> a) -> a -> Vect b m -> a

125+total foldl : (a -> b -> a) -> a -> Vect m b -> a

126foldl f e [] = e

127foldl f e (x::xs) = foldl f (f e x) xs

128

129−total foldr : (a -> b -> b) -> b -> Vect a m -> b

129+total foldr : (a -> b -> b) -> b -> Vect m a -> b

130foldr f e [] = e

131foldr f e (x::xs) = f x (foldr f e xs)

132

@@ -134,39 +134,39 @@ foldr f e (x::xs) = f x (foldr f e xs)

134-- Special folds

135--------------------------------------------------------------------------------

136

137−concat : Vect (Vect a n) m -> Vect a (m * n)

137+concat : Vect m (Vect n a) -> Vect (m * n) a

138concat [] = []

139concat (v::vs) = v ++ concat vs

140

141−total and : Vect Bool m -> Bool

141+total and : Vect m Bool -> Bool

142and = foldr (&&) True

143

144−total or : Vect Bool m -> Bool

144+total or : Vect m Bool -> Bool

145or = foldr (||) False

146

147−total any : (a -> Bool) -> Vect a m -> Bool

147+total any : (a -> Bool) -> Vect m a -> Bool

148−any p = Vect.or . map p

148+any p = Vect.or . Vect.map p

149

150−total all : (a -> Bool) -> Vect a m -> Bool

150+total all : (a -> Bool) -> Vect m a -> Bool

151−all p = Vect.and . map p

151+all p = Vect.and . Vect.map p

152

153--------------------------------------------------------------------------------

154-- Transformations

155--------------------------------------------------------------------------------

156

157−total reverse : Vect a n -> Vect a n

157+total reverse : Vect n a -> Vect n a

158reverse = reverse' []

159 where

160− total reverse' : Vect a m -> Vect a n -> Vect a (m + n)

160+ total reverse' : Vect m a -> Vect n a -> Vect (m + n) a

161 reverse' acc [] ?= acc

162 reverse' acc (x::xs) ?= reverse' (x::acc) xs

163

164−total intersperse' : a -> Vect a m -> (p ** Vect a p)

164+total intersperse' : a -> Vect m a -> (p ** Vect p a)

165intersperse' sep [] = (_ ** [])

166intersperse' sep (y::ys) with (intersperse' sep ys)

167 | (_ ** tail) = (_ ** sep::y::tail)

168

169−total intersperse : a -> Vect a m -> (p ** Vect a p)

169+total intersperse : a -> Vect m a -> (p ** Vect p a)

170intersperse sep [] = (_ ** [])

171intersperse sep (x::xs) with (intersperse' sep xs)

172 | (_ ** tail) = (_ ** x::tail)

@@ -175,56 +175,56 @@ intersperse sep (x::xs) with (intersperse' sep xs)

175-- Membership tests

176--------------------------------------------------------------------------------

177

178−elemBy : (a -> a -> Bool) -> a -> Vect a n -> Bool

178+elemBy : (a -> a -> Bool) -> a -> Vect n a -> Bool

179elemBy p e [] = False

180elemBy p e (x::xs) with (p e x)

181 | True = True

182 | False = elemBy p e xs

183

184−elem : Eq a => a -> Vect a n -> Bool

184+elem : Eq a => a -> Vect n a -> Bool

185elem = elemBy (==)

186

187−lookupBy : (a -> a -> Bool) -> a -> Vect (a, b) n -> Maybe b

187+lookupBy : (a -> a -> Bool) -> a -> Vect n (a, b) -> Maybe b

188lookupBy p e [] = Nothing

189lookupBy p e ((l, r)::xs) with (p e l)

190 | True = Just r

191 | False = lookupBy p e xs

192

193−lookup : Eq a => a -> Vect (a, b) n -> Maybe b

193+lookup : Eq a => a -> Vect n (a, b) -> Maybe b

194lookup = lookupBy (==)

195

196−hasAnyBy : (a -> a -> Bool) -> Vect a m -> Vect a n -> Bool

196+hasAnyBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool

197hasAnyBy p elems [] = False

198hasAnyBy p elems (x::xs) with (elemBy p x elems)

199 | True = True

200 | False = hasAnyBy p elems xs

201

202−hasAny : Eq a => Vect a m -> Vect a n -> Bool

202+hasAny : Eq a => Vect m a -> Vect n a -> Bool

203hasAny = hasAnyBy (==)

204

205--------------------------------------------------------------------------------

206-- Searching with a predicate

207--------------------------------------------------------------------------------

208

209−find : (a -> Bool) -> Vect a n -> Maybe a

209+find : (a -> Bool) -> Vect n a -> Maybe a

210find p [] = Nothing

211find p (x::xs) with (p x)

212 | True = Just x

213 | False = find p xs

214

215−findIndex : (a -> Bool) -> Vect a n -> Maybe Nat

215+findIndex : (a -> Bool) -> Vect n a -> Maybe Nat

216findIndex = findIndex' 0

217 where

218− findIndex' : Nat -> (a -> Bool) -> Vect a n -> Maybe Nat

218+ findIndex' : Nat -> (a -> Bool) -> Vect n a -> Maybe Nat

219 findIndex' cnt p [] = Nothing

220 findIndex' cnt p (x::xs) with (p x)

221 | True = Just cnt

222 | False = findIndex' (S cnt) p xs

223

224−total findIndices : (a -> Bool) -> Vect a m -> (p ** Vect Nat p)

224+total findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)

225findIndices = findIndices' 0

226 where

227− total findIndices' : Nat -> (a -> Bool) -> Vect a m -> (p ** Vect Nat p)

227+ total findIndices' : Nat -> (a -> Bool) -> Vect m a -> (p ** Vect p Nat)

228 findIndices' cnt p [] = (_ ** [])

229 findIndices' cnt p (x::xs) with (findIndices' (S cnt) p xs)

230 | (_ ** tail) =

@@ -233,23 +233,23 @@ findIndices = findIndices' 0

233 else

234 (_ ** tail)

235

236−elemIndexBy : (a -> a -> Bool) -> a -> Vect a m -> Maybe Nat

236+elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe Nat

237elemIndexBy p e = findIndex $ p e

238

239−elemIndex : Eq a => a -> Vect a m -> Maybe Nat

239+elemIndex : Eq a => a -> Vect m a -> Maybe Nat

240elemIndex = elemIndexBy (==)

241

242−total elemIndicesBy : (a -> a -> Bool) -> a -> Vect a m -> (p ** Vect Nat p)

242+total elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> (p ** Vect p Nat)

243elemIndicesBy p e = findIndices $ p e

244

245−total elemIndices : Eq a => a -> Vect a m -> (p ** Vect Nat p)

245+total elemIndices : Eq a => a -> Vect m a -> (p ** Vect p Nat)

246elemIndices = elemIndicesBy (==)

247

248--------------------------------------------------------------------------------

249-- Filters

250--------------------------------------------------------------------------------

251

252−total filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)

252+total filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)

253filter p [] = ( _ ** [] )

254filter p (x::xs) with (filter p xs)

255 | (_ ** tail) =

@@ -258,17 +258,17 @@ filter p (x::xs) with (filter p xs)

258 else

259 (_ ** tail)

260

261−nubBy : (a -> a -> Bool) -> Vect a n -> (p ** Vect a p)

261+nubBy : (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)

262nubBy = nubBy' []

263 where

264− nubBy' : Vect a m -> (a -> a -> Bool) -> Vect a n -> (p ** Vect a p)

264+ nubBy' : Vect m a -> (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)

265 nubBy' acc p [] = (_ ** [])

266 nubBy' acc p (x::xs) with (elemBy p x acc)

267 | True = nubBy' acc p xs

268 | False with (nubBy' (x::acc) p xs)

269 | (_ ** tail) = (_ ** x::tail)

270

271−nub : Eq a => Vect a n -> (p ** Vect a p)

271+nub : Eq a => Vect n a -> (p ** Vect p a)

272nub = nubBy (==)

273

274--------------------------------------------------------------------------------

@@ -279,31 +279,31 @@ nub = nubBy (==)

279-- Predicates

280--------------------------------------------------------------------------------

281

282−isPrefixOfBy : (a -> a -> Bool) -> Vect a m -> Vect a n -> Bool

282+isPrefixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool

283isPrefixOfBy p [] right = True

284isPrefixOfBy p left [] = False

285isPrefixOfBy p (x::xs) (y::ys) with (p x y)

286 | True = isPrefixOfBy p xs ys

287 | False = False

288

289−isPrefixOf : Eq a => Vect a m -> Vect a n -> Bool

289+isPrefixOf : Eq a => Vect m a -> Vect n a -> Bool

290isPrefixOf = isPrefixOfBy (==)

291

292−isSuffixOfBy : (a -> a -> Bool) -> Vect a m -> Vect a n -> Bool

292+isSuffixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool

293isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)

294

295−isSuffixOf : Eq a => Vect a m -> Vect a n -> Bool

295+isSuffixOf : Eq a => Vect m a -> Vect n a -> Bool

296isSuffixOf = isSuffixOfBy (==)

297

298--------------------------------------------------------------------------------

299-- Conversions

300--------------------------------------------------------------------------------

301

302−total maybeToVect : Maybe a -> (p ** Vect a p)

302+total maybeToVect : Maybe a -> (p ** Vect p a)

303maybeToVect Nothing = (_ ** [])

304maybeToVect (Just j) = (_ ** [j])

305

306−total vectToMaybe : Vect a n -> Maybe a

306+total vectToMaybe : Vect n a -> Maybe a

307vectToMaybe [] = Nothing

308vectToMaybe (x::xs) = Just x

309

@@ -311,17 +311,17 @@ vectToMaybe (x::xs) = Just x

311-- Misc

312--------------------------------------------------------------------------------

313

314−catMaybes : Vect (Maybe a) n -> (p ** Vect a p)

314+catMaybes : Vect n (Maybe a) -> (p ** Vect p a)

315catMaybes [] = (_ ** [])

316catMaybes (Nothing::xs) = catMaybes xs

317catMaybes ((Just j)::xs) with (catMaybes xs)

318 | (_ ** tail) = (_ ** j::tail)

319

320−range : Vect (Fin n) n

320+range : Vect n (Fin n)

321range =

322 reverse range_

323 where

324− range_ : Vect (Fin n) n

324+ range_ : Vect n (Fin n)

325 range_ {n=Z} = Nil

326 range_ {n=(S _)} = last :: map weaken range_

327

test/reg002/reg002.idr+1−1

@@ -22,7 +22,7 @@ S_inj (Co n) Infinity p = FalseElim (S_Co_not_Inf p)

22S_inj Infinity (Co m) p = FalseElim (S_Co_not_Inf (sym p))

23S_inj Infinity Infinity refl = refl

24

25−swap : {n : Nat} -> Vect a n -> Vect a n

25+swap : {n : Nat} -> Vect n a -> Vect n a

26swap Nil = Nil

27swap (x :: Nil) = x :: Nil

28swap (x :: y :: xs) = (y :: x :: (swap xs))

test/reg005/reg005.idr+5−5

@@ -1,12 +1,12 @@

1module Main

2

3−rep : (n : Nat) -> Char -> Vect Char n

3+rep : (n : Nat) -> Char -> Vect n Char

4rep Z x = []

5rep (S k) x = x :: rep k x

6

7−data RLE : Vect Char n -> Type where

7+data RLE : Vect n Char -> Type where

8 REnd : RLE []

9− RChar : {xs : Vect Char k} ->

9+ RChar : {xs : Vect k Char} ->

10 (n : Nat) -> (x : Char) -> RLE xs ->

11 RLE (rep (S n) x ++ xs)

12

@@ -15,7 +15,7 @@ eq x y = if x == y then Just ?eqCharOK else Nothing

15

16------------

17

18−rle : (xs : Vect Char n) -> RLE xs

18+rle : (xs : Vect n Char) -> RLE xs

19rle [] = REnd

20rle (x :: xs) with (rle xs)

21 rle (x :: Vect.Nil) | REnd = RChar Z x REnd

@@ -25,7 +25,7 @@ rle (x :: xs) with (rle xs)

25 rle (x :: rep (S n) y ++ ys) | RChar n y rs | Nothing

26 = RChar Z x (RChar n y rs)

27

28−compress : Vect Char n -> String

28+compress : Vect n Char -> String

29compress xs with (rle xs)

30 compress Nil | REnd = ""

31 compress (rep (S n) x ++ xs) | RChar _ _ rs

test/reg009/reg009.lidr+3−3

@@ -1,12 +1,12 @@

1−> isAnyBy : (alpha -> Bool) -> (n : Nat ** Vect alpha n) -> Bool

1+> isAnyBy : (alpha -> Bool) -> (n : Nat ** Vect n alpha) -> Bool

2> isAnyBy _ (_ ** Nil) = False

3> isAnyBy p (_ ** (a :: as)) = p a || isAnyBy p (_ ** as)

4

5

6> filterTagP : (p : alpha -> Bool) ->

7−> (as : Vect alpha n) ->

7+> (as : Vect n alpha) ->

8> so (isAnyBy p (n ** as)) ->

9−> (m : Nat ** (Vect (a : alpha ** so (p a)) m, so (m > Z)))

9+> (m : Nat ** (Vect m (a : alpha ** so (p a)), so (m > Z)))

10> filterTagP {n = S m} p (a :: as) q with (p a)

11> | True = (_

12> **

test/reg011/reg011.idr+1−1

@@ -1,6 +1,6 @@

1vfoldl : (P : Nat -> Type) ->

2 ((x : Nat) -> P x -> a -> P (S x)) -> P Z

3− -> Vect a m -> P m

3+ -> Vect m a -> P m

4-- vfoldl P cons nil []

5-- = nil

6vfoldl P cons nil (x :: xs)

test/reg014/reg014.idr+1−1

@@ -1,7 +1,7 @@

1module reg014

2

3Matrix : Type -> Nat -> Nat -> Type

4−Matrix a n m = Vect (Vect a m) n

4+Matrix a n m = Vect n (Vect m a)

5

6transpose : Matrix a (S n) (S m) -> Matrix a (S m) (S n)

7transpose ((x:: []) :: []) = [[x]]

test/reg018/reg018c.idr+1−1

@@ -8,7 +8,7 @@ codata InfStream a = (::) a (InfStream a)

8-- natFromStream : Nat -> InfStream Nat

9-- natFromStream n = (::) n (natFromStream (S n))

10

11−take : (n: Nat) -> InfStream a -> Vect a n

11+take : (n: Nat) -> InfStream a -> Vect n a

12take Z _ = []

13take (S n) (x :: xs) = x :: take n xs

14

test/reg018/reg018d.idr+1−1

@@ -1,7 +1,7 @@

1module Main

2

3total

4−pull : Fin (S n) -> Vect a (S n) -> (a, Vect a n)

4+pull : Fin (S n) -> Vect (S n) a -> (a, Vect n a)

5pull {n=Z} _ (x :: xs) = (x, xs)

6-- pull {n=S q} fZ (Vect.(::) {n=S _} x xs) = (x, xs)

7pull {n=S _} (fS n) (x :: xs) =

test/reg020/reg020.idr+1−1

@@ -15,7 +15,7 @@ tabOnly = "\t"

15linebreakOnly : String

16linebreakOnly = "\n"

17

18−all : Vect String 5

18+all : Vect 5 String

19all =

20 [ emptyString

21 , helloWorld

test/test001/test001.idr+4−4

@@ -7,13 +7,13 @@ interpTy TyInt = Int

7interpTy TyBool = Bool

8interpTy (TyFun s t) = interpTy s -> interpTy t

9

10−using (G : Vect Ty n)

10+using (G : Vect n Ty)

11

12− data Env : Vect Ty n -> Type where

12+ data Env : Vect n Ty -> Type where

13 Nil : Env Nil

14 (::) : interpTy a -> Env G -> Env (a :: G)

15

16− data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where

16+ data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where

17 stop : HasType fZ (t :: G) t

18 pop : HasType k G t -> HasType (fS k) (u :: G) t

19

@@ -22,7 +22,7 @@ using (G : Vect Ty n)

22 lookup (pop k) (x :: xs) = lookup k xs

23 lookup stop [] impossible

24

25− data Expr : Vect Ty n -> Ty -> Type where

25+ data Expr : Vect n Ty -> Ty -> Type where

26 Var : HasType i G t -> Expr G t

27 Val : (x : Int) -> Expr G TyInt

28 Lam : Expr (a :: G) t -> Expr G (TyFun a t)

test/test010/test010.idr+1−1

@@ -5,7 +5,7 @@ data MyNat = MyO | MyS MyNat

5data Bad = MkBad (Bad -> Int) Int

6 | MkBad' Int

7

8−vapp : Vect a n -> Vect a m -> Vect a (n + m)

8+vapp : Vect n a -> Vect m a -> Vect (n + m) a

9vapp [] ys = ys

10vapp (x :: xs) ys = x :: vapp xs ys

11

test/test011/test011.idr+2−2

@@ -2,8 +2,8 @@ module Main

2

3record Foo : Nat -> Type where

4 MkFoo : (name : String) ->

5− (things : Vect a n) ->

5+ (things : Vect n a) ->

6− (more_things : Vect b m) ->

6+ (more_things : Vect m b) ->

7 Foo n

8

9record Person : Type where

test/test014/Resimp.idr+7−7

@@ -32,7 +32,7 @@ ioc = MkCreator

32

33infixr 5 :->

34

35−using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)

35+using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)

36

37 data Ty = R Type

38 | Val Type

@@ -45,11 +45,11 @@ using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)

45 interpTy (Choice x y) = Either x y

46 interpTy (a :-> b) = a -> interpTy b

47

48− data HasType : Vect Ty n -> Fin n -> Ty -> Type where

48+ data HasType : Vect n Ty -> Fin n -> Ty -> Type where

49 stop : HasType (a :: gam) fZ a

50 pop : HasType gam i b -> HasType (a :: gam) (fS i) b

51

52− data Env : Vect Ty n -> Type where

52+ data Env : Vect n Ty -> Type where

53 Nil : Env Nil

54 (::) : interpTy a -> Env gam -> Env (a :: gam)

55

@@ -57,7 +57,7 @@ using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)

57 envLookup stop (x :: xs) = x

58 envLookup (pop k) (x :: xs) = envLookup k xs

59

60− update : (gam : Vect Ty n) -> HasType gam i b -> Ty -> Vect Ty n

60+ update : (gam : Vect n Ty) -> HasType gam i b -> Ty -> Vect n Ty

61 update (x :: xs) stop y = y :: xs

62 update (x :: xs) (pop k) y = x :: update xs k y

63 update Nil stop _ impossible

@@ -79,7 +79,7 @@ using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)

79 envTail : Env (a :: gam) -> Env gam

80 envTail (x :: xs) = xs

81

82− data Args : Vect Ty n -> List Type -> Type where

82+ data Args : Vect n Ty -> List Type -> Type where

83 ANil : Args gam []

84 ACons : HasType gam i a ->

85 Args gam as -> Args gam (interpTy a :: as)

@@ -88,7 +88,7 @@ using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)

88 funTy list.Nil t = t

89 funTy (a :: as) t = a :-> funTy as t

90

91− data Res : Vect Ty n -> Vect Ty n -> Ty -> Type where

91+ data Res : Vect n Ty -> Vect n Ty -> Ty -> Type where

92

93{-- Resource creation and usage. 'Let' creates a resource - the type

94 at the end means that the resource must have been consumed by the time

@@ -164,5 +164,5 @@ dsl res

164 index_first = stop

165 index_next = pop

166

167−syntax RES [x] = {gam:Vect Ty n} -> Res gam gam (R x)

167+syntax RES [x] = {gam:Vect n Ty} -> Res gam gam (R x)

168

test/test017/test017.idr+1−1

@@ -41,7 +41,7 @@ mnubBy = nubBy' []

41 x :: nubBy' (x::acc) p xs

42

43partial

44−vtrans : Vect a n -> Vect a n -> List a

44+vtrans : Vect n a -> Vect n a -> List a

45vtrans [] _ = []

46vtrans (x :: xs) ys = x :: vtrans ys ys

47

test/test017/test017a.idr+1−1

@@ -1,7 +1,7 @@

1module scg

2

3total

4−vtrans : Vect a n -> Vect a n -> List a

4+vtrans : Vect n a -> Vect n a -> List a

5vtrans [] _ = []

6vtrans (x :: xs) ys = x :: vtrans ys ys

7

test/test020/expected+2−2

@@ -1,6 +1,6 @@

1−test020a.idr:16:Can't unify Vect a n with List a

1+test020a.idr:16:Can't unify Vect n a with List a

2

3Specifically:

4− Can't unify Vect a n with List a

4+ Can't unify Vect n a with List a

5[3, 2, 1]

6Number 42

test/test020/test020.idr+2−2

@@ -5,11 +5,11 @@ natInt : Nat -> Integer

5natInt x = cast x

6

7implicit

8−forget : Vect a n -> List a

8+forget : Vect n a -> List a

9forget [] = []

10forget (x :: xs) = x :: forget xs

11

12−foo : Vect a n -> List a

12+foo : Vect n a -> List a

13foo xs = reverse xs

14

15implicit intString : Integer -> String

test/test020/test020a.idr+3−3

@@ -1,16 +1,16 @@

1module Main

2

3implicit

4−forget : Vect a n -> List a

4+forget : Vect n a -> List a

5forget [] = []

6forget (x :: xs) = x :: forget xs

7

8implicit

9−forget' : Vect a n -> List a

9+forget' : Vect n a -> List a

10forget' [] = []

11forget' (x :: xs) = forget xs

12

13−foo : Vect a n -> List a

13+foo : Vect n a -> List a

14foo xs = reverse xs

15

16main : IO ()

test/test025/test025.idr+3−3

@@ -8,13 +8,13 @@ MemoryIO : Type -> Type -> Type -> Type

8MemoryIO td ts r = Eff (IOExcept String) [ Dst ::: RAW_MEMORY td

9 , Src ::: RAW_MEMORY ts ] r

10

11−inpVect : Vect Bits8 5

11+inpVect : Vect 5 Bits8

12inpVect = map prim__truncInt_B8 [0, 1, 2, 3, 5]

13

14−sub1 : Vect Bits8 n -> Vect Bits8 n

14+sub1 : Vect n Bits8 -> Vect n Bits8

15sub1 xs = map (prim__truncInt_B8 . (\ x => x - 1) . prim__zextB8_Int) xs

16

17−testMemory : MemoryIO () () (Vect Int 4)

17+testMemory : MemoryIO () () (Vect 4 Int)

18testMemory = do Src :- allocate 5

19 Src :- poke 0 inpVect oh

20 Dst :- allocate 5

tutorial/classes.tex+2−2

@@ -61,9 +61,9 @@ to a \texttt{String}:

61

62\begin{SaveVerbatim}{showvec}

63

64−instance Show a => Show (Vect a n) where

64+instance Show a => Show (Vect n a) where

65 show xs = "[" ++ show' xs ++ "]" where

66− show' : Vect a n -> String

66+ show' : Vect n a -> String

67 show' Nil = ""

68 show' (x :: Nil) = show x

69 show' (x :: xs) = show x ++ ", " ++ show' xs

tutorial/examples/interp.idr+4−4

@@ -7,13 +7,13 @@ interpTy TyInt = Int

7interpTy TyBool = Bool

8interpTy (TyFun s t) = interpTy s -> interpTy t

9

10−using (G : Vect Ty n)

10+using (G : Vect n Ty)

11

12− data Env : Vect Ty n -> Type where

12+ data Env : Vect n Ty -> Type where

13 Nil : Env Nil

14 (::) : interpTy a -> Env G -> Env (a :: G)

15

16− data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where

16+ data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where

17 stop : HasType fZ (t :: G) t

18 pop : HasType k G t -> HasType (fS k) (u :: G) t

19

@@ -21,7 +21,7 @@ using (G : Vect Ty n)

21 lookup stop (x :: xs) = x

22 lookup (pop k) (x :: xs) = lookup k xs

23

24− data Expr : Vect Ty n -> Ty -> Type where

24+ data Expr : Vect n Ty -> Ty -> Type where

25 Var : HasType i G t -> Expr G t

26 Val : (x : Int) -> Expr G TyInt

27 Lam : Expr (a :: G) t -> Expr G (TyFun a t)

tutorial/examples/usefultypes.idr+2−2

@@ -1,11 +1,11 @@

1

2−intVec : Vect Int 5

2+intVec : Vect 5 Int

3intVec = [1, 2, 3, 4, 5]

4

5double : Int -> Int

6double x = x * 2

7

8−vec : (n ** Vect Int n)

8+vec : (n ** Vect n Int)

9vec = (_ ** [3, 4])

10

11list_lookup : Nat -> List a -> Maybe a

tutorial/examples/vbroken.idr+1−1

@@ -1,4 +1,4 @@

1−vapp : Vect a n -> Vect a m -> Vect a (n + m)

1+vapp : Vect n a -> Vect m a -> Vect (n + m) a

2vapp Nil ys = ys

3vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN

4

tutorial/idris-tutorial.tex+1−1

@@ -11,7 +11,7 @@

11\input{library.ltx}

12

13\newcommand{\Idris}{\textsc{Idris}}

14−\newcommand{\version}{0.9.8}

14+\newcommand{\version}{0.9.9}

15

16\title{Programming in \Idris{}: a tutorial}

17\author{Edwin Brady \\ \url{eb@cs.st-andrews.ac.uk}}

tutorial/interp.tex+6−6

@@ -40,7 +40,7 @@ in a \texttt{using} block:

40

41\begin{SaveVerbatim}{usingg}

42

43−using (G:Vect Ty n)

43+using (G:Vect n Ty)

44

45\end{SaveVerbatim}

46\useverb{usingg}

@@ -51,7 +51,7 @@ indexed by the types of the local variables, and the type of the expression itse

51

52\begin{SaveVerbatim}{exprdecl}

53

54−data Expr : Vect Ty n -> Ty -> Type

54+data Expr : Vect n Ty -> Ty -> Type

55

56\end{SaveVerbatim}

57\useverb{exprdecl}

@@ -63,11 +63,11 @@ constructor in turn.

63

64\begin{SaveVerbatim}{exprty}

65

66−data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where

66+data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where

67 stop : HasType fZ (t :: G) t

68 pop : HasType k G t -> HasType (fS k) (u :: G) t

69

70−data Expr : Vect Ty n -> Ty -> Type where

70+data Expr : Vect n Ty -> Ty -> Type where

71 Var : HasType i G t -> Expr G t

72 Val : (x : Int) -> Expr G TyInt

73 Lam : Expr (a :: G) t -> Expr G (TyFun a t)

@@ -87,7 +87,7 @@ Variables are represented by a proof of their membership in the context,

87

88\begin{SaveVerbatim}{hastype}

89

90−data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Type where

90+data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where

91 stop : HasType fZ (t :: G) t

92 pop : HasType k G t -> HasType (fS k) (u :: G) t

93

@@ -181,7 +181,7 @@ is defined in the context, we can then produce a value from the environment:

181

182\begin{SaveVerbatim}{envtype}

183

184−data Env : Vect Ty n -> Type where

184+data Env : Vect n Ty -> Type where

185 Nil : Env Nil

186 (::) : interpTy a -> Env G -> Env (a :: G)

187

tutorial/intro.tex+2−2

@@ -24,7 +24,7 @@ types are a \emph{first class} language construct and can be manipulated like

24any other value. The standard

25example is the type of lists of a given length\footnote{Typically, and perhaps

26confusingly, referred to in the dependently typed programming literature as

27−``vectors''}, \texttt{Vect a n}, where \texttt{a} is the element type and

27+``vectors''}, \texttt{Vect n a}, where \texttt{a} is the element type and

28\texttt{n} is the length of the list and can be an arbitrary

29term.

30

@@ -37,7 +37,7 @@ to the \texttt{app} function, which concatenates vectors:

37

38\begin{SaveVerbatim}{appendv}

39

40−app : Vect a n -> Vect a m -> Vect a (n + m)

40+app : Vect n a -> Vect m a -> Vect (n + m) a

41

42\end{SaveVerbatim}

43\useverb{appendv}

tutorial/miscellany.tex+3−3

@@ -342,7 +342,7 @@ have types. For example:

342*universe> :t Nat

343Nat : Type

344*universe> :t Vect

345−Vect : Type -> Nat -> Type

345+Vect : Nat -> Type -> Type

346

347\end{SaveVerbatim}

348\useverb{typetypes}

@@ -353,13 +353,13 @@ But what about the type of \texttt{Type}? If we ask \Idris{} it reports

353\begin{SaveVerbatim}{setset}

354

355*universe> :t Type

356−Type : Type

356+Type : Type 1

357

358\end{SaveVerbatim}

359\useverb{setset}

360

361\noindent

362−It \emph{appears} that \texttt{Type} is its own type. This would lead to an inconsitency

362+If \texttt{Type} were its own type, it would lead to an inconsitency

363due to Girard's paradox~\cite{girard-thesis}, so internally there is a \emph{hierarchy}

364of types (or \emph{universes}):

365

tutorial/modules.tex+2−2

@@ -207,11 +207,11 @@ constructors. They may also be dependent types with implicit arguments:

207

208\begin{SaveVerbatim}{paramdata}

209

210−parameters (xs : Vect a x, y : Nat)

210+parameters (xs : Vect x a, y : Nat)

211 data Vects : Type -> Type where

212 MkVects : Vect a y -> Vects a

213

214− append : Vects a -> Vect a (x + y)

214+ append : Vects a -> Vect (x + y) a

215 append (MkVects ys) = xs ++ ys

216

217\end{SaveVerbatim}

tutorial/typesfuns.tex+33−32

@@ -273,13 +273,14 @@ test = [c (S 1), c Z, d (S Z)]

273

274A standard example of a dependent type is the type of ``lists with length'',

275conventionally called vectors in the dependent type literature. In \Idris{},

276−we declare vectors as follows:

276+we declare vectors as follows\footnote{Note that prior to \Idris{} 0.9.9,

277+the order of the arguments to \texttt{Vect} was reversed.}:

277

278

278\begin{SaveVerbatim}{vect}

279\begin{SaveVerbatim}{vect}

279

280

280−data Vect : Type -> Nat -> Type where

281+data Vect : Nat -> Type -> Type where

281− Nil : Vect a Z

282+ Nil : Vect Z a

282− (::) : a -> Vect a k -> Vect a (S k)

283+ (::) : a -> Vect k a -> Vect (S k) a

283

284

284\end{SaveVerbatim}

285\end{SaveVerbatim}

285\useverb{vect}

286\useverb{vect}

@@ -292,13 +293,13 @@ Ambiguous constructor names can normally be resolved from context.

292

293

293This declares a family of types, and so the form of the declaration is rather

294This declares a family of types, and so the form of the declaration is rather

294different from the simple type declarations above. We explicitly state the type

295different from the simple type declarations above. We explicitly state the type

295−of the type constructor \tTC{Vect} --- it takes a type and a \tTC{Nat} as an

296+of the type constructor \tTC{Vect} --- it takes a \tTC{Nat} and a type as an

296argument, where \tTC{Type} stands for the type of types. We say that \tTC{Vect}

297argument, where \tTC{Type} stands for the type of types. We say that \tTC{Vect}

297−is \emph{parameterised} by a type, and \emph{indexed} over \tTC{Nat}. Each

298+is \emph{indexed} over \tTC{Nat} and \emph{parameterised} by \tTC{Type}. Each

298constructor targets a different part of the family of types. \tDC{Nil} can only

299constructor targets a different part of the family of types. \tDC{Nil} can only

299be used to construct vectors with zero length, and \tDC{::} to construct

300be used to construct vectors with zero length, and \tDC{::} to construct

300vectors with non-zero length. In the type of \tDC{::}, we state explicitly that an element

301vectors with non-zero length. In the type of \tDC{::}, we state explicitly that an element

301−of type \texttt{a} and a tail of type \texttt{Vect a k} (i.e., a vector of length \texttt{k})

302+of type \texttt{a} and a tail of type \texttt{Vect k a} (i.e., a vector of length \texttt{k})

302combine to make a vector of length \texttt{S k}.

303combine to make a vector of length \texttt{S k}.

303

304

304We can define functions on dependent types such as \tTC{Vect} in the same way

305We can define functions on dependent types such as \tTC{Vect} in the same way

@@ -309,7 +310,7 @@ library, appends two \tTC{Vect}s:

309

310

310\begin{SaveVerbatim}{vapp}

311\begin{SaveVerbatim}{vapp}

311

312

312−(++) : Vect A n -> Vect A m -> Vect A (n + m)

313+(++) : Vect n a -> Vect m a -> Vect (n + m) a

313(++) Nil ys = ys

314(++) Nil ys = ys

314(++) (x :: xs) ys = x :: xs ++ ys

315(++) (x :: xs) ys = x :: xs ++ ys

315

316

@@ -323,7 +324,7 @@ not hold, \Idris{} will not accept the definition. For example:

323

324

324\begin{SaveVerbatim}{vapperr}

325\begin{SaveVerbatim}{vapperr}

325

326

326−(++) : Vect a n -> Vect a m -> Vect a (n + m)

327+(++) : Vect n a -> Vect m a -> Vect (n + m) a

327(++) Nil ys = ys

328(++) Nil ys = ys

328(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN

329(++) (x :: xs) ys = x :: xs ++ xs -- BROKEN

329

330

@@ -333,10 +334,10 @@ not hold, \Idris{} will not accept the definition. For example:

333\begin{SaveVerbatim}{vapperrmsg}

334\begin{SaveVerbatim}{vapperrmsg}

334

335

335$ idris vbroken.idr --check

336$ idris vbroken.idr --check

336−vbroken.idr:3:Can't unify Vect a n with Vect a m

337+vbroken.idr:3:Can't unify Vect n a with Vect m a

337

338

338Specifically:

339Specifically:

339− Can't unify n with m

340+ Can't unify n with m

340

341

341\end{SaveVerbatim}

342\end{SaveVerbatim}

342\begin{SaveVerbatim}{bleh}

343\begin{SaveVerbatim}{bleh}

@@ -383,7 +384,7 @@ by a bounded index given as a \tTC{Fin n}, is defined in the prelude:

383

384

384\begin{SaveVerbatim}{vindex}

385\begin{SaveVerbatim}{vindex}

385

386

386−index : Fin n -> Vect a n -> a

387+index : Fin n -> Vect n a -> a

387index fZ (x :: xs) = x

388index fZ (x :: xs) = x

388index (fS k) (x :: xs) = index k xs

389index (fS k) (x :: xs) = index k xs

389

390

@@ -408,7 +409,7 @@ Let us take a closer look at the type of \texttt{index}:

408

409

409\begin{SaveVerbatim}{vindexty}

410\begin{SaveVerbatim}{vindexty}

410

411

411−index : Fin n -> Vect a n -> a

412+index : Fin n -> Vect n a -> a

412

413

413\end{SaveVerbatim}

414\end{SaveVerbatim}

414\useverb{vindexty}

415\useverb{vindexty}

@@ -421,7 +422,7 @@ arguments to \texttt{index}. We could also write the type of \texttt{index} as:

421

422

422\begin{SaveVerbatim}{vindeximpty}

423\begin{SaveVerbatim}{vindeximpty}

423

424

424−index : {a:Type} -> {n:Nat} -> Fin n -> Vect a n -> a

425+index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a

425

426

426\end{SaveVerbatim}

427\end{SaveVerbatim}

427\useverb{vindeximpty}

428\useverb{vindeximpty}

@@ -429,7 +430,7 @@ index : {a:Type} -> {n:Nat} -> Fin n -> Vect a n -> a

429\noindent

430\noindent

430Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are

431Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are

431not given in applications of \texttt{index}; their values can be inferred from

432not given in applications of \texttt{index}; their values can be inferred from

432−the types of the \texttt{Fin n} and \texttt{Vect a n} arguments. Any name

433+the types of the \texttt{Fin n} and \texttt{Vect n a} arguments. Any name

433with a \remph{lower case initial letter} which

434with a \remph{lower case initial letter} which

434appears as a parameter or index in a type declaration, but which is otherwise

435appears as a parameter or index in a type declaration, but which is otherwise

435free, will be automatically bound as an implicit argument. Implicit arguments

436free, will be automatically bound as an implicit argument. Implicit arguments

@@ -449,7 +450,7 @@ declared the type of \texttt{index} as:

449

450

450\begin{SaveVerbatim}{vindexn}

451\begin{SaveVerbatim}{vindexn}

451

452

452−index : (i:Fin n) -> (xs:Vect a n) -> a

453+index : (i:Fin n) -> (xs:Vect n a) -> a

453

454

454\end{SaveVerbatim}

455\end{SaveVerbatim}

455\useverb{vindexn}

456\useverb{vindexn}

@@ -469,9 +470,9 @@ definition, which defines a predicate on vectors:

469

470

470\begin{SaveVerbatim}{elem}

471\begin{SaveVerbatim}{elem}

471

472

472−data Elem : a -> Vect a n -> Type where

473+data Elem : a -> Vect n a -> Type where

473− here : {x:a} -> {xs:Vect a n} -> Elem x (x :: xs)

474+ here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)

474− there : {x,y:a} -> {xs:Vect a n} -> Elem x xs -> Elem x (y :: xs)

475+ there : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)

475

476

476\end{SaveVerbatim}

477\end{SaveVerbatim}

477\useverb{elem}

478\useverb{elem}

@@ -484,7 +485,7 @@ or \texttt{there}, in the tail of the vector. For example:

484

485

485\begin{SaveVerbatim}{testelem}

486\begin{SaveVerbatim}{testelem}

486

487

487−testVec : Vect Int 4

488+testVec : Vect 4 Int

488testVec = 3 :: 4 :: 5 :: 6 :: Nil

489testVec = 3 :: 4 :: 5 :: 6 :: Nil

489

490

490inVect : Elem 5 testVec

491inVect : Elem 5 testVec

@@ -500,8 +501,8 @@ ordering of any implicit arguments which can appear within the block:

500

501

501\begin{SaveVerbatim}{elemusing}

502\begin{SaveVerbatim}{elemusing}

502

503

503−using (x:a, y:a, xs:Vect a n)

504+using (x:a, y:a, xs:Vect n a)

504− data Elem : a -> Vect a n -> Type where

505+ data Elem : a -> Vect n a -> Type where

505 here : Elem x (x :: xs)

506 here : Elem x (x :: xs)

506 there : Elem x xs -> Elem x (y :: xs)

507 there : Elem x xs -> Elem x (y :: xs)

507

508

@@ -662,9 +663,9 @@ We have already seen the \texttt{List} and \texttt{Vect} data types:

662

663

663data List a = Nil | (::) a (List a)

664data List a = Nil | (::) a (List a)

664

665

665−data Vect : Type -> Nat -> Type where

666+data Vect : Nat -> Type -> Type where

666− Nil : Vect a Z

667+ Nil : Vect Z a

667− (::) : a -> Vect a k -> Vect a (S k)

668+ (::) : a -> Vect k a -> Vect (S k) a

668

669

669\end{SaveVerbatim}

670\end{SaveVerbatim}

670\useverb{listvec}

671\useverb{listvec}

@@ -692,7 +693,7 @@ map : (a -> b) -> List a -> List b

692map f [] = []

693map f [] = []

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

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

694

695

695−map : (a -> b) -> Vect a n -> Vect b n

696+map : (a -> b) -> Vect n a -> Vect n b

696map f [] = []

697map f [] = []

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

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

698

699

@@ -704,7 +705,7 @@ For example, to double every element in a vector of integers:

704

705

705\begin{SaveVerbatim}{dvect}

706\begin{SaveVerbatim}{dvect}

706

707

707−intVec : Vect Int 5

708+intVec : Vect 5 Int

708intVec = [1, 2, 3, 4, 5]

709intVec = [1, 2, 3, 4, 5]

709

710

710double : Int -> Int

711double : Int -> Int

@@ -860,7 +861,7 @@ constructs a value of this type. For example, we can pair a number with a

860

861

861\begin{SaveVerbatim}{dvec}

862\begin{SaveVerbatim}{dvec}

862

863

863−vec : (n : Nat ** Vect Int n)

864+vec : (n : Nat ** Vect n Int)

864vec = (2 ** [3, 4])

865vec = (2 ** [3, 4])

865

866

866\end{SaveVerbatim}

867\end{SaveVerbatim}

@@ -874,7 +875,7 @@ written as:

874

875

875\begin{SaveVerbatim}{dvec1}

876\begin{SaveVerbatim}{dvec1}

876

877

877−vec : (n : Nat ** Vect Int n)

878+vec : (n : Nat ** Vect n Int)

878vec = (_ ** [3, 4])

879vec = (_ ** [3, 4])

879

880

880\end{SaveVerbatim}

881\end{SaveVerbatim}

@@ -886,7 +887,7 @@ again, it can be inferred:

886

887

887\begin{SaveVerbatim}{dvec2}

888\begin{SaveVerbatim}{dvec2}

888

889

889−vec : (n ** Vect Int n)

890+vec : (n ** Vect n Int)

890vec = (_ ** [3, 4])

891vec = (_ ** [3, 4])

891

892

892\end{SaveVerbatim}

893\end{SaveVerbatim}

@@ -900,7 +901,7 @@ length of the resulting vector will be:

900

901

901\begin{SaveVerbatim}{vfilter}

902\begin{SaveVerbatim}{vfilter}

902

903

903−filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)

904+filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)

904

905

905\end{SaveVerbatim}

906\end{SaveVerbatim}

906\useverb{vfilter}

907\useverb{vfilter}

@@ -1154,7 +1155,7 @@ the record as a whole. For example:

1154\begin{SaveVerbatim}{deprec}

1155\begin{SaveVerbatim}{deprec}

1155

1156

1156record Class : Type where

1157record Class : Type where

1157− ClassInfo : (students : Vect Person n) ->

1158+ ClassInfo : (students : Vect n Person) ->

1158 (className : String) ->

1159 (className : String) ->

1159 Class

1160 Class

1160

1161

tutorial/views.tex+2−2

@@ -9,7 +9,7 @@ determined by whether the vector was empty or not:

9

10\begin{SaveVerbatim}{appdep}

11

12−(++) : Vect a n -> Vect a m -> Vect a (n + m)

12+(++) : Vect n a -> Vect m a -> Vect (n + m) a

13(++) {n=Z} [] ys = ys

14(++) {n=S k} (x :: xs) ys = x :: xs ++ ys

15

@@ -34,7 +34,7 @@ a vector filter function, defined as follows:

34

35\begin{SaveVerbatim}{vfilterdef}

36

37−filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)

37+filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)

38filter p [] = ( _ ** [] )

39filter p (x :: xs) with (filter p xs)

40 | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )