Add Chapter 10 TypeDD tests

A lot to change here! To be honest, this chapter probably needs a
complete revision...

TypeDD.md

@@ -123,12 +123,97 @@ In `Hangman.idr`:
     game : {guesses : _} -> {letters : _} ->
            WordState (S guesses) (S letters) -> IO Finished
   
-
-
 Chapter 10
 ----------
 
-TODO
+Lots of changes necessary here, at least when constructing views, due to Idris
+2 having a better (that is, more precise and correct!) implementation of
+unification, and the rules for recursive `with` application being tightened up.
+
+In `MergeSort.idr`, add `import Data.List`
+
+In `MergeSortView.idr`, add `import Data.List`, and make the arguments to the
+views explicit:
+
+    mergeSort : Ord a => List a -> List a
+    mergeSort input with (splitRec input)
+      mergeSort [] | SplitRecNil = []
+      mergeSort [x] | SplitRecOne x = [x]
+      mergeSort (lefts ++ rights) | (SplitRecPair lefts rights lrec rrec)
+           = merge (mergeSort lefts | lrec)
+                   (mergeSort rights | rrec)
+
+In `SnocList.idr`, in `my_reverse`, the link between `Snoc rec` and `xs ++ [x]`
+needs to be made explicit. Idris 1 would happily decide that `xs` and `x` were
+the relevant implicit arguments to `Snoc` but this was little more than a guess
+based on what would make it type checker, whereas Idris 2 is more precise in
+what it allows to unify. So, `x` and `xs` need to be explicit arguments to
+`Snoc`:
+
+    data SnocList : List a -> Type where
+         Empty : SnocList []
+         Snoc : (x, xs : _) -> (rec : SnocList xs) -> SnocList (xs ++ [x])
+  
+Correspondingly, they need to be explicit when matching. For example:
+
+      my_reverse : List a -> List a
+      my_reverse input with (snocList input)
+        my_reverse [] | Empty = []
+        my_reverse (xs ++ [x]) | (Snoc x xs rec) = x :: my_reverse xs | rec
+
+Similar changes are necessary in `snocListHelp` and `my_reverse_help`. See
+tests/typedd-book/chapter10/SnocList.idr for the full details.
+
+Also, in `snocListHelp`, `input` is used at run time so needs to be bound
+in the type:
+
+    snocListHelp : {input : _} ->
+                   (snoc : SnocList input) -> (rest : List a) -> SnocList (input +
+
+It's no longer necessary to give `{input}` explicitly in the patterns for
+`snocListHelp`, although it's harmless to do so.
+
+In `IsSuffix.idr`, the matching has to be written slightly differently. The
+recursive with application in Idris 1 probably shouldn't have allowed this!
+
+    isSuffix : Eq a => List a -> List a -> Bool
+    isSuffix input1 input2 with (snocList input1, snocList input2)
+      isSuffix [] input2 | (Empty, s) = True
+      isSuffix input1 [] | (s, Empty) = False
+      isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec, Snoc ysrec)
+         = if x == y 
+              then isSuffix xs ys | (xsrec, ysrec)
+              else False
+
+This doesn't yet get past the totality checker, however, because it doesn't
+know about looking inside pairs.
+
+In `DataStore.idr`: Well this is embarrassing - I've no idea how Idris 1 lets
+this through! I think perhaps it's too "helpful" when solving unification
+problems. To fix it, add an extra parameter `scheme` to `StoreView`, and change
+the type of `SNil` to be explicit that the `empty` is the function defined in
+`DataStore`. Also add `entry` and `store` as explicit arguments to `SAdd`:
+
+    data StoreView : (schema : _) -> DataStore schema -> Type where
+         SNil : StoreView schema DataStore.empty
+         SAdd : (entry, store : _) -> (rec : StoreView schema store) ->
+                StoreView schema (addToStore entry store)
+
+Since `size` is as explicit argument in the `DataStore` record, it also needs
+to be relevant in the type of `storeViewHelp`:
+
+    storeViewHelp : {size : _} ->
+                    (items : Vect size (SchemaType schema)) ->
+                    StoreView schema (MkData size items)
+
+In `TestStore.idr`:
+
++ In `listItems`, `empty` needs to be `DataStore.empty` to be explicit that you
+  mean the function
++ In `filterKeys`, there is an error in the `SNil` case, which wasn't caught
+  because of the type of `SNil` above. It should be:
+
+    filterKeys test DataStore.empty | SNil = []
 
 Chapter 11
 ----------

tests/Main.idr

@@ -48,7 +48,7 @@ idrisTests
 typeddTests : List String
 typeddTests
    = ["chapter01", "chapter02", "chapter03", "chapter04", "chapter05",
-      "chapter06", "chapter07", "chapter08", "chapter09"]
+      "chapter06", "chapter07", "chapter08", "chapter09", "chapter10"]
 
 chezTests : List String
 chezTests

tests/typedd-book/chapter10/DLFail.idr

@@ -0,0 +1,3 @@
+describe_list_end : List Int -> String
+describe_list_end [] = "Empty"
+describe_list_end (xs ++ [x]) = "Non-empty, initial portion = " ++ show xs

tests/typedd-book/chapter10/DataStore.idr

@@ -0,0 +1,48 @@
+module DataStore
+
+import Data.Vect
+
+infixr 5 .+.
+
+public export
+data Schema = SString | SInt | (.+.) Schema Schema
+
+public export
+SchemaType : Schema -> Type
+SchemaType SString = String
+SchemaType SInt = Int
+SchemaType (x .+. y) = (SchemaType x, SchemaType y)
+
+export
+record DataStore (schema : Schema) where
+  constructor MkData
+  size : Nat
+  items : Vect size (SchemaType schema)
+
+export
+empty : DataStore schema
+empty = MkData 0 []
+
+export
+addToStore : (entry : SchemaType schema) ->
+             (store : DataStore schema) ->
+             DataStore schema 
+addToStore entry (MkData _ items)
+     = MkData _ (entry :: items)
+
+public export
+data StoreView : (schema : _) -> DataStore schema -> Type where
+     SNil : StoreView schema DataStore.empty
+     SAdd : (entry, store : _) -> (rec : StoreView schema store) -> 
+            StoreView schema (addToStore entry store)
+
+storeViewHelp : {size : _} ->
+                (items : Vect size (SchemaType schema)) -> 
+                StoreView schema (MkData size items)
+storeViewHelp [] = SNil
+storeViewHelp (entry :: xs) = SAdd _ _ (storeViewHelp xs)
+
+export
+storeView : (store : DataStore schema) -> StoreView schema store
+storeView (MkData size items) 
+    = storeViewHelp items

tests/typedd-book/chapter10/DescribeList.idr

@@ -0,0 +1,17 @@
+data ListLast : List a -> Type where
+     Empty : ListLast []
+     NonEmpty : (xs : List a) -> (x : a) -> ListLast (xs ++ [x])
+
+listLast : (xs : List a) -> ListLast xs
+listLast [] = Empty
+listLast (x :: xs) = case listLast xs of
+                          Empty => NonEmpty [] x
+                          NonEmpty xs y => NonEmpty (x :: xs) y
+
+describeHelper : (input : List Int) -> ListLast input -> String
+describeHelper [] Empty = "Empty"
+describeHelper (xs ++ [x]) (NonEmpty xs x)
+        = "Non-empty, initial portion = " ++ show xs
+
+describeListEnd : List Int -> String
+describeListEnd xs = describeHelper xs (listLast xs)

tests/typedd-book/chapter10/DescribeList2.idr

@@ -0,0 +1,15 @@
+data ListLast : List a -> Type where
+     Empty : ListLast []
+     NonEmpty : (xs : List a) -> (x : a) -> ListLast (xs ++ [x])
+
+listLast : (xs : List a) -> ListLast xs
+listLast [] = Empty
+listLast (x :: xs) = case listLast xs of
+                          Empty => NonEmpty [] x
+                          NonEmpty xs y => NonEmpty (x :: xs) y
+
+describe_list_end : List Int -> String
+
+describe_list_end input with (listLast input)
+  describe_list_end [] | Empty = ?describe_list_end_rhs_1
+  describe_list_end (xs ++ [x]) | (NonEmpty xs x) = ?describe_list_end_rhs_2

tests/typedd-book/chapter10/IsSuffix.idr

@@ -0,0 +1,11 @@
+import Data.List.Views
+
+-- total
+isSuffix : Eq a => List a -> List a -> Bool
+isSuffix input1 input2 with (MkPair (snocList input1) (snocList input2))
+  isSuffix [] input2 | (Empty, s) = True
+  isSuffix input1 [] | (s, Empty) = False
+  isSuffix (xs ++ [x]) (ys ++ [y]) | (MkPair (Snoc x xs xsrec) (Snoc y ys ysrec))
+     = if x == y 
+          then isSuffix xs ys | (MkPair xsrec ysrec)
+          else False

tests/typedd-book/chapter10/MergeSort.idr

@@ -0,0 +1,28 @@
+import Data.List
+
+data SplitList : List a -> Type where
+     SplitNil : SplitList []
+     SplitOne : SplitList [x]
+     SplitPair : (lefts : List a) -> (rights : List a) ->
+                 SplitList (lefts ++ rights)
+
+total
+splitList : (xs : List a) ->  SplitList xs
+splitList xs = splitListHelp xs xs
+  where
+    splitListHelp : (counter : List a) -> (xs : List a) -> SplitList xs
+    splitListHelp _ [] = SplitNil
+    splitListHelp _ [x] = SplitOne
+    splitListHelp (_ :: _ :: ys) (x :: xs)
+       = case splitListHelp ys xs of
+              SplitNil => SplitOne
+              SplitOne {x=y} => SplitPair [x] [y]
+              SplitPair lefts rights => SplitPair (x :: lefts) rights
+    splitListHelp _ xs = SplitPair [] xs
+
+mergeSort : Ord a => List a -> List a
+mergeSort input with (splitList input)
+  mergeSort [] | SplitNil = []
+  mergeSort [x] | SplitOne = [x]
+  mergeSort (lefts ++ rights) | (SplitPair lefts rights)
+         = merge (mergeSort lefts) (mergeSort rights)

tests/typedd-book/chapter10/MergeSortView.idr

@@ -0,0 +1,10 @@
+import Data.List
+import Data.List.Views
+
+mergeSort : Ord a => List a -> List a
+mergeSort input with (splitRec input)
+  mergeSort [] | SplitRecNil = []
+  mergeSort [x] | SplitRecOne x = [x]
+  mergeSort (lefts ++ rights) | (SplitRecPair lefts rights lrec rrec)
+       = merge (mergeSort lefts | lrec)
+               (mergeSort rights | rrec)

tests/typedd-book/chapter10/Reverse.idr

@@ -0,0 +1,14 @@
+data ListLast : List a -> Type where
+     Empty : ListLast []
+     NonEmpty : (xs : List a) -> (x : a) -> ListLast (xs ++ [x])
+
+listLast : (xs : List a) -> ListLast xs
+listLast [] = Empty
+listLast (x :: xs) = case listLast xs of
+                          Empty => NonEmpty [] x
+                          NonEmpty xs y => NonEmpty (x :: xs) y
+
+myReverse : List a -> List a
+myReverse input with (listLast input)
+  myReverse [] | Empty = []
+  myReverse (xs ++ [x]) | (NonEmpty xs x) = x :: myReverse xs

tests/typedd-book/chapter10/ReverseSnoc.idr

@@ -0,0 +1,5 @@
+data SnocList ty = Empty | Snoc (SnocList ty) ty
+
+reverseSnoc : SnocList ty -> List ty
+reverseSnoc Empty = []
+reverseSnoc (Snoc xs x) = x :: reverseSnoc xs

tests/typedd-book/chapter10/Shape.idr

@@ -0,0 +1,18 @@
+module Shape
+
+public export
+data Shape = Triangle Double Double
+           | Rectangle Double Double
+           | Circle Double
+
+private
+rectangle_area : Double -> Double -> Double
+rectangle_area width height = width * height
+
+export
+area : Shape -> Double
+area (Triangle base height) = 0.5 * rectangle_area base height
+area (Rectangle length height) = rectangle_area length height
+area (Circle radius) = pi * radius * radius
+
+

tests/typedd-book/chapter10/Shape_abs.idr

@@ -0,0 +1,30 @@
+module Shape_abs
+
+export
+data Shape = Triangle Double Double
+           | Rectangle Double Double
+           | Circle Double
+
+export
+triangle : Double -> Double -> Shape
+triangle = Triangle
+
+export
+rectangle : Double -> Double -> Shape
+rectangle = Rectangle
+
+export
+circle : Double -> Shape
+circle = Circle
+
+private
+rectangle_area : Double -> Double -> Double
+rectangle_area width height = width * height
+
+export
+area : Shape -> Double
+area (Triangle base height) = 0.5 * rectangle_area base height
+area (Rectangle length height) = rectangle_area length height
+area (Circle radius) = pi * radius * radius
+
+

tests/typedd-book/chapter10/SnocList.idr

@@ -0,0 +1,27 @@
+import Data.List
+
+data SnocList : List a -> Type where
+     Empty : SnocList []
+     Snoc : (x, xs : _) -> (rec : SnocList xs) -> SnocList (xs ++ [x])
+
+snocListHelp : {input : _} ->
+               (snoc : SnocList input) -> (rest : List a) -> SnocList (input ++ rest)
+snocListHelp snoc [] = rewrite appendNilRightNeutral input in snoc
+snocListHelp snoc (x :: xs)
+    = rewrite appendAssociative input [x] xs in 
+              snocListHelp (Snoc x input snoc) xs
+
+snocList : (xs : List a) -> SnocList xs
+snocList xs = snocListHelp Empty xs
+
+my_reverse_help : (input : List a) -> SnocList input -> List a
+my_reverse_help [] Empty = []
+my_reverse_help (xs ++ [x]) (Snoc x xs rec) = x :: my_reverse_help xs rec
+
+my_reverse1 : List a -> List a
+my_reverse1 input = my_reverse_help input (snocList input)
+
+my_reverse : List a -> List a
+my_reverse input with (snocList input)
+  my_reverse [] | Empty = []
+  my_reverse (xs ++ [x]) | (Snoc x xs rec) = x :: my_reverse xs | rec

tests/typedd-book/chapter10/TestStore.idr

@@ -0,0 +1,24 @@
+import DataStore
+
+testStore : DataStore (SString .+. SString .+. SInt)
+testStore = addToStore ("Mercury", "Mariner 10", 1974) $
+            addToStore ("Venus", "Venera", 1961) $
+            addToStore ("Uranus", "Voyager 2", 1986) $
+            addToStore ("Pluto", "New Horizons", 2015) $
+            empty
+
+listItems : DataStore schema -> List (SchemaType schema)
+listItems input with (storeView input)
+  listItems DataStore.empty | SNil = []
+  listItems (addToStore entry store) | (SAdd entry store rec) 
+         = entry :: listItems store | rec
+
+filterKeys : (test : SchemaType val_schema -> Bool) ->
+             DataStore (SString .+. val_schema) -> List String
+filterKeys test input with (storeView input)
+  filterKeys test DataStore.empty | SNil = []
+  filterKeys test (addToStore (key, value) store) | (SAdd (key, value) store rec) 
+       = if test value 
+            then key :: filterKeys test store | rec
+            else filterKeys test store | rec
+

tests/typedd-book/chapter10/expected

@@ -0,0 +1,16 @@
+1/1: Building DataStore (DataStore.idr)
+1/1: Building DescribeList (DescribeList.idr)
+1/1: Building DescribeList2 (DescribeList2.idr)
+1/1: Building DLFail (DLFail.idr)
+DLFail.idr:3:20--3:29:While processing left hand side of Main.describe_list_end at DLFail.idr:3:1--4:1:
+Can't match on ?xs ++ [?x] (Not a constructor application or primitive)
+It elaborates to: ?xs ++ [?x]
+1/1: Building IsSuffix (IsSuffix.idr)
+1/1: Building MergeSort (MergeSort.idr)
+1/1: Building MergeSortView (MergeSortView.idr)
+1/1: Building Reverse (Reverse.idr)
+1/1: Building ReverseSnoc (ReverseSnoc.idr)
+1/1: Building Shape (Shape.idr)
+1/1: Building Shape_abs (Shape_abs.idr)
+1/1: Building SnocList (SnocList.idr)
+2/2: Building TestStore (TestStore.idr)

tests/typedd-book/chapter10/run

@@ -0,0 +1,15 @@
+$1 DataStore.idr --check
+$1 DescribeList.idr --check
+$1 DescribeList2.idr --check
+$1 DLFail.idr --check
+$1 IsSuffix.idr --check
+$1 MergeSort.idr --check
+$1 MergeSortView.idr --check
+$1 Reverse.idr --check
+$1 ReverseSnoc.idr --check
+$1 Shape.idr --check
+$1 Shape_abs.idr --check
+$1 SnocList.idr --check
+$1 TestStore.idr --check
+
+rm -rf build