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

git.iko.soy/Idris-dev

Swapped Vect arguments

So now nicer to write type class instances for Functor, Applicative, etc

commit61d39dabbf63237671a9661064e6b0478add62e4 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 27 Jul 2013, 14:32 (13 years ago) parent844837c

37 files changed+197−193

compare with master

unifiedsplit

CHANGELOG+2 effects/Effect/Memory.idr+6−6 javascript/JavaScript/JSON.idr+3−3 lib/Data/HVect.idr+6−6 lib/Data/Vect.idr+7−6 lib/Data/Vect/Quantifiers.idr+11−11 lib/Prelude.idr+2−2 lib/Prelude/Vect.idr+62−62 test/reg002/reg002.idr+1−1 test/reg005/reg005.idr+5−5 test/reg009/reg009.lidr+3−3 test/reg011/reg011.idr+1−1 test/reg014/reg014.idr+1−1 test/reg018/reg018c.idr+1−1 test/reg018/reg018d.idr+1−1 test/reg020/reg020.idr+1−1 test/test001/test001.idr+4−4 test/test010/test010.idr+1−1 test/test011/test011.idr+2−2 test/test014/Resimp.idr+7−7 test/test017/test017.idr+1−1 test/test017/test017a.idr+1−1 test/test020/expected+2−2 test/test020/test020.idr+2−2 test/test020/test020a.idr+3−3 test/test025/test025.idr+3−3 tutorial/classes.tex+2−2 tutorial/examples/interp.idr+4−4 tutorial/examples/usefultypes.idr+2−2 tutorial/examples/vbroken.idr+1−1 tutorial/idris-tutorial.tex+1−1 tutorial/interp.tex+6−6 tutorial/intro.tex+2−2 tutorial/miscellany.tex+3−3 tutorial/modules.tex+2−2 tutorial/typesfuns.tex+33−32 tutorial/views.tex+2−2

CHANGELOG+2

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

1111* Added Data.HVect module

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

1313* Integer literals for Fin

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

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

1416

1517Internal changes

1618

effects/Effect/Memory.idr+6−6

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

2121 Peek : (offset : Nat) ->

2222 (size : Nat) ->

2323 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)

2525 Poke : (offset : Nat) ->

26− (Vect Bits8 size) ->

26+ (Vect size Bits8) ->

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

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

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

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

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

6363

6464private

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

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

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

6767do_peek ptr offset (S n)

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

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

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

7171

7272private

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

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

7474do_poke _ _ [] = return ()

7575do_poke ptr offset (b::bs)

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

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

117117 (offset : Nat) ->

118118 (size : Nat) ->

119119 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)

121121peek offset size prf = Peek offset size prf

122122

123123poke : {n : Nat} ->

124124 {i : Nat} ->

125125 (offset : Nat) ->

126− Vect Bits8 size ->

126+ Vect size Bits8 ->

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

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

129129poke offset content prf = Poke offset content prf

javascript/JavaScript/JSON.idr+3−3

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

33import Data.SortedMap

55data JSONType : Type where

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

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

77 JSONString : JSONType

88 JSONNumber : JSONType

99 JSONBool : JSONType

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

1111 JSONNull : JSONType

1212

1313mutual

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

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

1515 namespace JArray

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

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

1717 Nil : JArray 0 []

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

1919

lib/Data/HVect.idr+6−6

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

55%access public

66%default total

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

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

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

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

1010 Nil : HVect []

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

1212

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

1414 index fZ (x::xs) = x

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

1616

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)

1818 deleteAt fZ (x::xs) = xs

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

2020 deleteAt _ [] impossible

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

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

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

2929

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

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

3131 (++) [] ys = ys

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

3333

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

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

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

3939

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

41− shows : HVect ts -> Vect String k

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

41+ shows : HVect ts -> Vect k String

4242

4343 instance Shows Z [] where

4444 shows [] = []

lib/Data/Vect.idr+7−6

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

99-- Elem

1010--------------------------------------------------------------------------------

1111

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

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

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

12+using (xs : Vect k a)

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

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

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

1516

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

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

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

1920

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)

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

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

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

2425

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

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

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

2829

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)

3031mapElem Here = Here

3132mapElem (There e) = There (mapElem e)

3233

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

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

11module Data.Vect.Quantifiers

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

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

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

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

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

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

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

88anyNilAbsurd Here impossible

99anyNilAbsurd There impossible

1010

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

1212anyElim _ f (Here p) = f p

1313anyElim f _ (There p) = f p

1414

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)

1616any _ Nil = No anyNilAbsurd

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

1818 | Yes prf = Yes (Here prf)

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

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

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

2323

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

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

2525 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)

2727

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

2929negAnyAll {xs=Nil} _ = Nil

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

3131

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) -> _|_

3333notAllHere _ Nil impossible

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

3535

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) -> _|_

3737notAllThere _ Nil impossible

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

3939

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)

4141all _ Nil = Yes Nil

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

4343 | No prf = No (notAllHere prf)

lib/Prelude.idr+2−2

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

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

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

169169

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

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

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

172− show' : Vect a n -> String

172+ show' : Vect n a -> String

173173 show' [] = ""

174174 show' [x] = show x

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

lib/Prelude/Vect.idr+62−62

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

1010infixr 7 ::

1111

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

13− Nil : Vect a Z

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

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

13+ Nil : Vect Z a

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

1515

1616--------------------------------------------------------------------------------

1717-- Indexing into vectors

1818--------------------------------------------------------------------------------

1919

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

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

2121tail (x::xs) = xs

2222

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

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

2424head (x::xs) = x

2525

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

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

2727last (x::[]) = x

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

2929

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

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

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

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

3333

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

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

3535index fZ (x::xs) = x

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

3737index fZ [] impossible

3838

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

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

4040deleteAt fZ (x::xs) = xs

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

4242deleteAt _ [] impossible

4343

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

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

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

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

4747

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

4949-- Subvectors

5050--------------------------------------------------------------------------------

5151

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

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

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

5454take (fS k) [] impossible

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

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

5757

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

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

5959drop fZ xs = (_ ** xs)

6060drop (fS k) [] impossible

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

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

6464-- Conversions to and from list

6565--------------------------------------------------------------------------------

6666

67−toList : Vect a n -> List a

67+toList : Vect n a -> List a

6868toList [] = []

6969toList (x::xs) = x :: toList xs

7070

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

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

7272fromList [] = []

7373fromList (x::xs) = x :: fromList xs

7474

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

7676-- Building (bigger) vectors

7777--------------------------------------------------------------------------------

7878

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

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

8080(++) [] ys = ys

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

8282

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

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

8484replicate Z x = []

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

8686

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

8888-- Zips and unzips

8989--------------------------------------------------------------------------------

9090

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

9292zipWith f [] [] = []

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

9494

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

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

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

9797

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

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

9999unzip [] = ([], [])

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

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

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

104104-- Maps

105105--------------------------------------------------------------------------------

106106

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

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

108108map f [] = []

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

110110

111111-- 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)

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

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

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

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

122122-- Folds

123123--------------------------------------------------------------------------------

124124

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

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

126126foldl f e [] = e

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

128128

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

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

130130foldr f e [] = e

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

132132

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

134134-- Special folds

135135--------------------------------------------------------------------------------

136136

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

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

138138concat [] = []

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

140140

141−total and : Vect Bool m -> Bool

141+total and : Vect m Bool -> Bool

142142and = foldr (&&) True

143143

144−total or : Vect Bool m -> Bool

144+total or : Vect m Bool -> Bool

145145or = foldr (||) False

146146

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

148−any p = Vect.or . map p

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

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

149149

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

151−all p = Vect.and . map p

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

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

152152

153153--------------------------------------------------------------------------------

154154-- Transformations

155155--------------------------------------------------------------------------------

156156

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

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

158158reverse = reverse' []

159159 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

161161 reverse' acc [] ?= acc

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

163163

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

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

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

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

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

168168

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

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

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

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

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

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

175175-- Membership tests

176176--------------------------------------------------------------------------------

177177

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

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

179179elemBy p e [] = False

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

181181 | True = True

182182 | False = elemBy p e xs

183183

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

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

185185elem = elemBy (==)

186186

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

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

188188lookupBy p e [] = Nothing

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

190190 | True = Just r

191191 | False = lookupBy p e xs

192192

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

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

194194lookup = lookupBy (==)

195195

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

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

197197hasAnyBy p elems [] = False

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

199199 | True = True

200200 | False = hasAnyBy p elems xs

201201

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

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

203203hasAny = hasAnyBy (==)

204204

205205--------------------------------------------------------------------------------

206206-- Searching with a predicate

207207--------------------------------------------------------------------------------

208208

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

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

210210find p [] = Nothing

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

212212 | True = Just x

213213 | False = find p xs

214214

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

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

216216findIndex = findIndex' 0

217217 where

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

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

219219 findIndex' cnt p [] = Nothing

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

221221 | True = Just cnt

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

223223

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

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

225225findIndices = findIndices' 0

226226 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)

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

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

230230 | (_ ** tail) =

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

233233 else

234234 (_ ** tail)

235235

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

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

237237elemIndexBy p e = findIndex $ p e

238238

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

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

240240elemIndex = elemIndexBy (==)

241241

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)

243243elemIndicesBy p e = findIndices $ p e

244244

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)

246246elemIndices = elemIndicesBy (==)

247247

248248--------------------------------------------------------------------------------

249249-- Filters

250250--------------------------------------------------------------------------------

251251

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

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

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

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

255255 | (_ ** tail) =

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

258258 else

259259 (_ ** tail)

260260

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

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

262262nubBy = nubBy' []

263263 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)

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

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

267267 | True = nubBy' acc p xs

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

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

270270

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

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

272272nub = nubBy (==)

273273

274274--------------------------------------------------------------------------------

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

279279-- Predicates

280280--------------------------------------------------------------------------------

281281

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

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

283283isPrefixOfBy p [] right = True

284284isPrefixOfBy p left [] = False

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

286286 | True = isPrefixOfBy p xs ys

287287 | False = False

288288

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

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

290290isPrefixOf = isPrefixOfBy (==)

291291

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

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

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

294294

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

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

296296isSuffixOf = isSuffixOfBy (==)

297297

298298--------------------------------------------------------------------------------

299299-- Conversions

300300--------------------------------------------------------------------------------

301301

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

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

303303maybeToVect Nothing = (_ ** [])

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

305305

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

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

307307vectToMaybe [] = Nothing

308308vectToMaybe (x::xs) = Just x

309309

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

311311-- Misc

312312--------------------------------------------------------------------------------

313313

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

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

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

316316catMaybes (Nothing::xs) = catMaybes xs

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

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

319319

320−range : Vect (Fin n) n

320+range : Vect n (Fin n)

321321range =

322322 reverse range_

323323 where

324− range_ : Vect (Fin n) n

324+ range_ : Vect n (Fin n)

325325 range_ {n=Z} = Nil

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

327327

test/reg002/reg002.idr+1−1

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

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

2323S_inj Infinity Infinity refl = refl

2424

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

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

2626swap Nil = Nil

2727swap (x :: Nil) = x :: Nil

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

test/reg005/reg005.idr+5−5

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

11module Main

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

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

44rep Z x = []

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

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

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

88 REnd : RLE []

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

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

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

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

1212

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

1515

1616------------

1717

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

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

1919rle [] = REnd

2020rle (x :: xs) with (rle xs)

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

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

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

2626 = RChar Z x (RChar n y rs)

2727

28−compress : Vect Char n -> String

28+compress : Vect n Char -> String

2929compress xs with (rle xs)

3030 compress Nil | REnd = ""

3131 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

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

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

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

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

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

88> 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)))

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

1111> | True = (_

1212> **

test/reg011/reg011.idr+1−1

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

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

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

3− -> Vect a m -> P m

3+ -> Vect m a -> P m

44-- vfoldl P cons nil []

55-- = nil

66vfoldl P cons nil (x :: xs)

test/reg014/reg014.idr+1−1

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

11module reg014

33Matrix : Type -> Nat -> Nat -> Type

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

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

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

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

test/reg018/reg018c.idr+1−1

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

88-- natFromStream : Nat -> InfStream Nat

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

1010

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

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

1212take Z _ = []

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

1414

test/reg018/reg018d.idr+1−1

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

11module Main

33total

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)

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

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

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

test/reg020/reg020.idr+1−1

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

1515linebreakOnly : String

1616linebreakOnly = "\n"

1717

18−all : Vect String 5

18+all : Vect 5 String

1919all =

2020 [ emptyString

2121 , helloWorld

test/test001/test001.idr+4−4

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

77interpTy TyBool = Bool

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

10−using (G : Vect Ty n)

10+using (G : Vect n Ty)

1111

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

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

1313 Nil : Env Nil

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

1515

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

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

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

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

1919

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

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

2323 lookup stop [] impossible

2424

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

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

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

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

2828 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

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

66 | MkBad' Int

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

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

99vapp [] ys = ys

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

1111

test/test011/test011.idr+2−2

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

33record Foo : Nat -> Type where

44 MkFoo : (name : String) ->

5− (things : Vect a n) ->

6− (more_things : Vect b m) ->

5+ (things : Vect n a) ->

6+ (more_things : Vect m b) ->

77 Foo n

99record Person : Type where

test/test014/Resimp.idr+7−7

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

3232

3333infixr 5 :->

3434

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)

3636

3737 data Ty = R Type

3838 | Val Type

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

4545 interpTy (Choice x y) = Either x y

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

4747

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

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

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

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

5151

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

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

5353 Nil : Env Nil

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

5555

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

5757 envLookup stop (x :: xs) = x

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

5959

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

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

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

6363 update Nil stop _ impossible

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

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

8080 envTail (x :: xs) = xs

8181

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

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

8383 ANil : Args gam []

8484 ACons : HasType gam i a ->

8585 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)

8888 funTy list.Nil t = t

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

9090

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

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

9292

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

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

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

164164 index_first = stop

165165 index_next = pop

166166

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)

168168

test/test017/test017.idr+1−1

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

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

4242

4343partial

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

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

4545vtrans [] _ = []

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

4747

test/test017/test017a.idr+1−1

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

11module scg

33total

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

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

55vtrans [] _ = []

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

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

33Specifically:

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

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

55[3, 2, 1]

66Number 42

test/test020/test020.idr+2−2

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

55natInt x = cast x

77implicit

8−forget : Vect a n -> List a

8+forget : Vect n a -> List a

99forget [] = []

1010forget (x :: xs) = x :: forget xs

1111

12−foo : Vect a n -> List a

12+foo : Vect n a -> List a

1313foo xs = reverse xs

1414

1515implicit intString : Integer -> String

test/test020/test020a.idr+3−3

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

11module Main

33implicit

4−forget : Vect a n -> List a

4+forget : Vect n a -> List a

55forget [] = []

66forget (x :: xs) = x :: forget xs

88implicit

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

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

1010forget' [] = []

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

1212

13−foo : Vect a n -> List a

13+foo : Vect n a -> List a

1414foo xs = reverse xs

1515

1616main : IO ()

test/test025/test025.idr+3−3

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

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

99 , Src ::: RAW_MEMORY ts ] r

1010

11−inpVect : Vect Bits8 5

11+inpVect : Vect 5 Bits8

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

1313

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

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

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

1616

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

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

1818testMemory = do Src :- allocate 5

1919 Src :- poke 0 inpVect oh

2020 Dst :- allocate 5

tutorial/classes.tex+2−2

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

6161

6262\begin{SaveVerbatim}{showvec}

6363

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

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

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

66− show' : Vect a n -> String

66+ show' : Vect n a -> String

6767 show' Nil = ""

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

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

tutorial/examples/interp.idr+4−4

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

77interpTy TyBool = Bool

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

10−using (G : Vect Ty n)

10+using (G : Vect n Ty)

1111

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

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

1313 Nil : Env Nil

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

1515

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

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

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

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

1919

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

2121 lookup stop (x :: xs) = x

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

2323

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

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

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

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

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

tutorial/examples/usefultypes.idr+2−2

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

2−intVec : Vect Int 5

2+intVec : Vect 5 Int

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

55double : Int -> Int

66double x = x * 2

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

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

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

1010

1111list_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

22vapp Nil ys = ys

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

tutorial/idris-tutorial.tex+1−1

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

1111\input{library.ltx}

1212

1313\newcommand{\Idris}{\textsc{Idris}}

14−\newcommand{\version}{0.9.8}

14+\newcommand{\version}{0.9.9}

1515

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

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

tutorial/interp.tex+6−6

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

4040

4141\begin{SaveVerbatim}{usingg}

4242

43−using (G:Vect Ty n)

43+using (G:Vect n Ty)

4444

4545\end{SaveVerbatim}

4646\useverb{usingg}

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

5151

5252\begin{SaveVerbatim}{exprdecl}

5353

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

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

5555

5656\end{SaveVerbatim}

5757\useverb{exprdecl}

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

6363

6464\begin{SaveVerbatim}{exprty}

6565

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

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

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

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

6969

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

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

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

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

7373 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,

8787

8888\begin{SaveVerbatim}{hastype}

8989

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

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

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

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

9393

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

181181

182182\begin{SaveVerbatim}{envtype}

183183

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

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

185185 Nil : Env Nil

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

187187

tutorial/intro.tex+2−2

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

2424any other value. The standard

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

2626confusingly, 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

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

2929term.

3030

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

3737

3838\begin{SaveVerbatim}{appendv}

3939

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

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

4141

4242\end{SaveVerbatim}

4343\useverb{appendv}

tutorial/miscellany.tex+3−3

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

342342*universe> :t Nat

343343Nat : Type

344344*universe> :t Vect

345−Vect : Type -> Nat -> Type

345+Vect : Nat -> Type -> Type

346346

347347\end{SaveVerbatim}

348348\useverb{typetypes}

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

353353\begin{SaveVerbatim}{setset}

354354

355355*universe> :t Type

356−Type : Type

356+Type : Type 1

357357

358358\end{SaveVerbatim}

359359\useverb{setset}

360360

361361\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

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

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

365365

tutorial/modules.tex+2−2

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

207207

208208\begin{SaveVerbatim}{paramdata}

209209

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

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

211211 data Vects : Type -> Type where

212212 MkVects : Vect a y -> Vects a

213213

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

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

215215 append (MkVects ys) = xs ++ ys

216216

217217\end{SaveVerbatim}

tutorial/typesfuns.tex+33−32

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

273273

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

275275conventionally 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.}:

277278

278279\begin{SaveVerbatim}{vect}

279280

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

281− Nil : Vect a Z

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

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

282+ Nil : Vect Z a

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

283284

284285\end{SaveVerbatim}

285286\useverb{vect}

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

292293

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

294295different 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

296297argument, 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

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

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

300301vectors 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})

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

303304

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

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

309310

310311\begin{SaveVerbatim}{vapp}

311312

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

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

313314(++) Nil ys = ys

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

315316

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

323324

324325\begin{SaveVerbatim}{vapperr}

325326

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

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

327328(++) Nil ys = ys

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

329330

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

333334\begin{SaveVerbatim}{vapperrmsg}

334335

335336$ 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

337338

338339Specifically:

339− Can't unify n with m

340+ Can't unify n with m

340341

341342\end{SaveVerbatim}

342343\begin{SaveVerbatim}{bleh}

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

383384

384385\begin{SaveVerbatim}{vindex}

385386

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

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

387388index fZ (x :: xs) = x

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

389390

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

408409

409410\begin{SaveVerbatim}{vindexty}

410411

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

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

412413

413414\end{SaveVerbatim}

414415\useverb{vindexty}

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

421422

422423\begin{SaveVerbatim}{vindeximpty}

423424

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

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

425426

426427\end{SaveVerbatim}

427428\useverb{vindeximpty}

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

429430\noindent

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

431432not 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

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

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

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

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

449450

450451\begin{SaveVerbatim}{vindexn}

451452

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

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

453454

454455\end{SaveVerbatim}

455456\useverb{vindexn}

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

469470

470471\begin{SaveVerbatim}{elem}

471472

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

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

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

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

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

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

475476

476477\end{SaveVerbatim}

477478\useverb{elem}

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

484485

485486\begin{SaveVerbatim}{testelem}

486487

487−testVec : Vect Int 4

488+testVec : Vect 4 Int

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

489490

490491inVect : Elem 5 testVec

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

500501

501502\begin{SaveVerbatim}{elemusing}

502503

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

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

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

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

505506 here : Elem x (x :: xs)

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

507508

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

662663

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

664665

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

666− Nil : Vect a Z

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

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

667+ Nil : Vect Z a

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

668669

669670\end{SaveVerbatim}

670671\useverb{listvec}

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

692693map f [] = []

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

694695

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

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

696697map f [] = []

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

698699

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

704705

705706\begin{SaveVerbatim}{dvect}

706707

707−intVec : Vect Int 5

708+intVec : Vect 5 Int

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

709710

710711double : Int -> Int

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

860861

861862\begin{SaveVerbatim}{dvec}

862863

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

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

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

865866

866867\end{SaveVerbatim}

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

874875

875876\begin{SaveVerbatim}{dvec1}

876877

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

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

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

879880

880881\end{SaveVerbatim}

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

886887

887888\begin{SaveVerbatim}{dvec2}

888889

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

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

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

891892

892893\end{SaveVerbatim}

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

900901

901902\begin{SaveVerbatim}{vfilter}

902903

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

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

904905

905906\end{SaveVerbatim}

906907\useverb{vfilter}

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

11541155\begin{SaveVerbatim}{deprec}

11551156

11561157record Class : Type where

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

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

11581159 (className : String) ->

11591160 Class

11601161

tutorial/views.tex+2−2

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

1010\begin{SaveVerbatim}{appdep}

1111

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

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

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

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

1515

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

3434

3535\begin{SaveVerbatim}{vfilterdef}

3636

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

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

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

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

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