Make a start on Data.Vect

TypeDD.md

@@ -19,17 +19,23 @@ the base libraries instead. So:
 
 In `Average.idr`, add:
 
-import Data.Strings -- for `words`
-import Data.List -- for `length` on lists
+    import Data.Strings -- for `words`
+    import Data.List -- for `length` on lists
 
 In `AveMain.idr` and `Reverse.idr` add:
 
-import System.REPL -- for 'repl'
+    import System.REPL -- for 'repl'
 
 Chaoter 3
 ---------
 
-TODO
+Unbound implicits have multiplicity 0, so we can't match on them at run-time.
+Therefore, in `Matrix.idr`, we need to change the type of `createEmpties`
+and `transposeMat` so that the length of the inner vector is available to
+match on:
+
+    createEmpties : {n : _} -> Vect n (Vect 0 elem)
+    transposeMat : {n : _} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
 
 Chaoter 4
 ---------

libs/base/Data/Vect.idr

@@ -0,0 +1,88 @@
+module Data.Vect
+
+public export
+data Vect : (len : Nat) -> (elem : Type) -> Type where
+  ||| Empty vector
+  Nil  : Vect Z elem
+  ||| A non-empty vector of length `S len`, consisting of a head element and
+  ||| the rest of the list, of length `len`.
+  (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
+
+-- Hints for interactive editing
+%name Vect xs,ys,zs,ws
+
+export
+length : (xs : Vect len elem) -> Nat
+length [] = 0
+length (x::xs) = 1 + length xs
+
+||| Show that the length function on vectors in fact calculates the length
+private 
+lengthCorrect : (len : Nat) -> (xs : Vect len elem) -> length xs = len
+lengthCorrect Z     []        = Refl
+lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl
+
+--------------------------------------------------------------------------------
+-- Indexing into vectors
+--------------------------------------------------------------------------------
+
+||| All but the first element of the vector
+|||
+||| ```idris example
+||| tail [1,2,3,4]
+||| ```
+public export
+tail : Vect (S len) elem -> Vect len elem
+tail (x::xs) = xs
+
+||| Only the first element of the vector
+|||
+||| ```idris example
+||| head [1,2,3,4]
+||| ```
+public export
+head : Vect (S len) elem -> elem
+head (x::xs) = x
+
+||| The last element of the vector
+|||
+||| ```idris example
+||| last [1,2,3,4]
+||| ```
+public export
+last : Vect (S len) elem -> elem
+last (x::[])    = x
+last (x::y::ys) = last $ y::ys
+
+||| All but the last element of the vector
+|||
+||| ```idris example
+||| init [1,2,3,4]
+||| ```
+public export
+init : Vect (S len) elem -> Vect len elem
+init (x::[])    = []
+init (x::y::ys) = x :: init (y::ys)
+
+||| Append two vectors
+|||
+||| ```idris example
+||| [1,2,3,4] ++ [5,6]
+||| ```
+public export
+(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
+(++) []      ys = ys
+(++) (x::xs) ys = x :: xs ++ ys
+
+||| Repeate some value some number of times.
+|||
+||| @ len the number of times to repeat it
+||| @ x the value to repeat
+|||
+||| ```idris example
+||| replicate 4 1
+||| ```
+replicate : (len : Nat) -> (x : elem) -> Vect len elem
+replicate Z     x = []
+replicate (S k) x = x :: replicate k x
+

libs/base/base.ipkg

@@ -7,6 +7,7 @@ modules = Control.WellFounded,
           Data.IORef,
           Data.List,
           Data.Strings,
+          Data.Vect,
 
           System,
           System.Concurrency.Raw,

tests/Main.idr

@@ -47,7 +47,7 @@ idrisTests
 
 typeddTests : List String
 typeddTests
-   = ["chapter001", "chapter002"]
+   = ["chapter01", "chapter02", "chapter03"]
 
 chezTests : List String
 chezTests
@@ -103,7 +103,7 @@ main
               | _ => do putStrLn "Usage: runtests [ttimp path]"
          ttimps <- traverse (runTest "ttimp" idris2) ttimpTests
          idrs <- traverse (runTest "idris2" idris2) idrisTests
-         typedds <- traverse (runTest "typedd" idris2) typeddTests
+         typedds <- traverse (runTest "typedd-book" idris2) typeddTests
          chexec <- findChez
          chezs <- maybe (do putStrLn "Chez Scheme not found"
                             pure [])

tests/typedd-book/chapter03/IsEven.idr

@@ -0,0 +1,12 @@
+isEven' : Nat -> Bool
+isEven' Z = True
+isEven' (S k) = not (isEven' k)
+
+mutual
+  isEven : Nat -> Bool
+  isEven Z = True
+  isEven (S k) = isOdd k
+
+  isOdd : Nat -> Bool
+  isOdd Z = False
+  isOdd (S k) = isEven k

tests/typedd-book/chapter03/Matrix.idr

@@ -0,0 +1,14 @@
+import Data.Vect
+
+createEmpties : {n : _} -> Vect n (Vect 0 elem)
+createEmpties {n = Z} = []
+createEmpties {n = (S k)} = [] :: createEmpties
+
+transposeHelper : (x : Vect n elem) -> (xs_trans : Vect n (Vect k elem)) -> Vect n (Vect (S k) elem)
+transposeHelper [] [] = []
+transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys
+
+transposeMat : {n : _} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
+transposeMat [] = createEmpties
+transposeMat (x :: xs) = let xsTrans = transposeMat xs in
+                             transposeHelper x xsTrans

tests/typedd-book/chapter03/VecSort.idr

@@ -0,0 +1,12 @@
+import Data.Vect
+
+insert : Ord elem => (x : elem) -> (xsSorted : Vect k elem) -> Vect (S k) elem
+insert x [] = [x]
+insert x (y :: xs) = case x < y of
+                          False => y :: insert x xs
+                          True => x :: y :: xs
+
+insSort : Ord elem => Vect n elem -> Vect n elem
+insSort [] = []
+insSort (x :: xs) = let xsSorted = insSort xs in
+                        insert x xsSorted

tests/typedd-book/chapter03/Vectors.idr

@@ -0,0 +1,10 @@
+import Data.Vect
+
+fourInts : Vect 4 Int
+fourInts = [0, 1, 2, 3]
+
+sixInts : Vect 6 Int
+sixInts = [4, 5, 6, 7, 8, 9]
+
+tenInts : Vect 10 Int
+tenInts = fourInts ++ sixInts

tests/typedd-book/chapter03/WordLength.idr

@@ -0,0 +1,3 @@
+allLengths : List String -> List Nat
+allLengths [] = []
+allLengths (word :: words) = length word :: allLengths words

tests/typedd-book/chapter03/WordLength_vec.idr

@@ -0,0 +1,6 @@
+import Data.Vect
+
+total
+allLengths : Vect len String -> Vect len Nat
+allLengths [] = []
+allLengths (word :: words) = length word :: allLengths words

tests/typedd-book/chapter03/XOR.idr

@@ -0,0 +1,3 @@
+xor : Bool -> Bool -> Bool
+xor False y = y
+xor True y = not y

tests/typedd-book/chapter03/expected

@@ -0,0 +1,7 @@
+1/1: Building IsEven (IsEven.idr)
+1/1: Building Matrix (Matrix.idr)
+1/1: Building VecSort (VecSort.idr)
+1/1: Building Vectors (Vectors.idr)
+1/1: Building WordLength (WordLength.idr)
+1/1: Building WordLength_vec (WordLength_vec.idr)
+1/1: Building XOR (XOR.idr)

tests/typedd-book/chapter03/run

@@ -0,0 +1,9 @@
+$1 IsEven.idr --check
+$1 Matrix.idr --check
+$1 VecSort.idr --check
+$1 Vectors.idr --check
+$1 WordLength.idr --check
+$1 WordLength_vec.idr --check
+$1 XOR.idr --check
+
+rm -rf build