From d8bd15dd2f08881eb3e8ee9f836bb2bda3b50036 Mon Sep 17 00:00:00 2001 From: Sage Hane Date: Tue, 3 Dec 2024 15:51:37 +0900 Subject: [PATCH 1/2] TDDwI: Minor changes to chapter10 --- docs/source/typedd/typedd.rst | 23 +++++++++-------------- tests/typedd-book/chapter10/IsSuffix.idr | 13 +++++++------ 2 files changed, 16 insertions(+), 20 deletions(-) diff --git a/docs/source/typedd/typedd.rst b/docs/source/typedd/typedd.rst index 287cc1a50d..e3f3687ff9 100644 --- a/docs/source/typedd/typedd.rst +++ b/docs/source/typedd/typedd.rst @@ -281,28 +281,23 @@ in the type: .. code-block:: idris snocListHelp : {input : _} -> - (snoc : SnocList input) -> (rest : List a) -> SnocList (input + + (snoc : SnocList input) -> (rest : List a) -> SnocList (input ++ rest) 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! -Note that the ``Snoc`` - ``Snoc`` case has to be written first otherwise Idris -generates a case tree splitting on ``input1`` and ``input2`` instead of the -``SnocList`` objects and this leads to a lot of cases being detected as missing. +``IsSuffix.idr`` also has to be adjusted to match the new ``Snoc`` arguments. .. code-block:: idris + total isSuffix : Eq a => List a -> List a -> Bool - isSuffix input1 input2 with (snocList input1, snocList input2) - isSuffix _ _ | (Snoc x xs xsrec, Snoc y ys ysrec) - = (x == y) && (isSuffix _ _ | (xsrec, ysrec)) - isSuffix _ _ | (Empty, s) = True - isSuffix _ _ | (s, Empty) = False - -This doesn't yet get past the totality checker, however, because it doesn't -know about looking inside pairs. + isSuffix input1 input2 with (snocList input1) + isSuffix [] input2 | Empty = True + isSuffix (xs ++ [x]) input2 | (Snoc x xs xsrec) with (snocList input2) + isSuffix (xs ++ [x]) [] | (Snoc x xs xsrec) | Empty = False + isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc x xs xsrec) | (Snoc y ys ysrec) + = if x == y then isSuffix xs ys | xsrec else False For the ``VList`` view in the exercise 4 after Chapter 10-2 ``import Data.List.Views.Extra`` from ``contrib`` library. diff --git a/tests/typedd-book/chapter10/IsSuffix.idr b/tests/typedd-book/chapter10/IsSuffix.idr index 4c50e8d6e6..77c6ddf98b 100644 --- a/tests/typedd-book/chapter10/IsSuffix.idr +++ b/tests/typedd-book/chapter10/IsSuffix.idr @@ -1,9 +1,10 @@ import Data.List.Views --- total +total isSuffix : Eq a => List a -> List a -> Bool -isSuffix input1 input2 with (snocList input1, snocList input2) - isSuffix _ _ | (Snoc x xs xsrec, Snoc y ys ysrec) - = (x == y) && (isSuffix _ _ | (xsrec, ysrec)) - isSuffix _ _ | (Empty, s) = True - isSuffix _ _ | (s, Empty) = False +isSuffix input1 input2 with (snocList input1) + isSuffix [] input2 | Empty = True + isSuffix (xs ++ [x]) input2 | (Snoc x xs xsrec) with (snocList input2) + isSuffix (xs ++ [x]) [] | (Snoc x xs xsrec) | Empty = False + isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc x xs xsrec) | (Snoc y ys ysrec) + = if x == y then isSuffix xs ys | xsrec else False From 4a8638aaffbe3484c6325f68931c96503bd0a13b Mon Sep 17 00:00:00 2001 From: Sage Hane Date: Thu, 5 Dec 2024 22:30:47 +0900 Subject: [PATCH 2/2] Add notes for exercise 2 of chapter 10-2 --- docs/source/typedd/typedd.rst | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/docs/source/typedd/typedd.rst b/docs/source/typedd/typedd.rst index e3f3687ff9..89a40ef99c 100644 --- a/docs/source/typedd/typedd.rst +++ b/docs/source/typedd/typedd.rst @@ -299,6 +299,18 @@ It's no longer necessary to give ``{input}`` explicitly in the patterns for isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc x xs xsrec) | (Snoc y ys ysrec) = if x == y then isSuffix xs ys | xsrec else False +For the ``SplitRec`` view in the exercise 2 after Chapter 10-2 ``import Data.Vect.Views.Extra`` +from ``contrib`` library. The ``n`` argument needs to be made explicit, and so +does the ``xs`` and ``ys`` for the ``SplitRecPair`` constructor. + +.. code-block:: idris + + mergeSort : {n : _} -> Ord a => Vect n a -> Vect n a + mergeSort xs with (splitRec xs) + mergeSort [] | SplitRecNil = ?mergeSort_rhs_rhss_0 + mergeSort [x] | SplitRecOne = ?mergeSort_rhs_rhss_1 + mergeSort (xs ++ ys) | (SplitRecPair {xs} {ys} lrec rrec) = ?mergeSort_rhs_rhss_2 + For the ``VList`` view in the exercise 4 after Chapter 10-2 ``import Data.List.Views.Extra`` from ``contrib`` library. In ``DataStore.idr``: Well this is embarrassing - I've no idea how Idris 1 lets