From a6a64c6ddf754dec24909bfbc5c03af122821ad7 Mon Sep 17 00:00:00 2001
From: madman-bob <robert.wright@ed.ac.uk>
Date: Sat, 30 Oct 2021 00:12:44 +0100
Subject: [PATCH] [ contrib ] Alternating lists of known parity (#2043)

---
 libs/contrib/Data/List/Alternating.idr        | 230 ++++++++++++++++++
 libs/contrib/Data/String/Parser.idr           |  15 ++
 libs/contrib/contrib.ipkg                     |   1 +
 tests/chez/chez027/StringParser.idr           |   3 +
 tests/chez/chez027/expected                   |   1 +
 .../list_alternating/AlternatingList.idr      |  63 +++++
 tests/contrib/list_alternating/expected       |  33 +++
 tests/contrib/list_alternating/input          |   2 +
 tests/contrib/list_alternating/run            |   3 +
 9 files changed, 351 insertions(+)
 create mode 100644 libs/contrib/Data/List/Alternating.idr
 create mode 100644 tests/contrib/list_alternating/AlternatingList.idr
 create mode 100644 tests/contrib/list_alternating/expected
 create mode 100644 tests/contrib/list_alternating/input
 create mode 100644 tests/contrib/list_alternating/run

diff --git a/libs/contrib/Data/List/Alternating.idr b/libs/contrib/Data/List/Alternating.idr
new file mode 100644
index 000000000..83628cef6
--- /dev/null
+++ b/libs/contrib/Data/List/Alternating.idr
@@ -0,0 +1,230 @@
+module Data.List.Alternating
+
+import Data.Bifoldable
+import Data.List
+
+infixl 5 +>
+infixr 5 <+
+
+mutual
+    namespace Odd
+        ||| Non-empty list, starting and ending with an a, where adjacent elements alternate
+        ||| between types a and b.
+        ||| We can think of this type as:
+        ||| - A fence, with the `a`s as fence-posts, and the `b`s as panels.
+        ||| - A non-empty list of `a`s, separated by `b`s
+        ||| - A list of `b`s, separated by, and surrounded by, `a`s
+        ||| - The free extension of a monoid `a`, with variables in `b`
+        public export
+        data Odd a b = (::) a (Even b a)
+
+    namespace Even
+        ||| A list, starting with an a, and ending with a b; where adjacent elements
+        ||| alternate between types a and b.
+        ||| Equivalent to List (a, b)
+        public export
+        data Even a b = Nil | (::) a (Odd b a)
+
+%name Odd xs, ys, zs
+%name Even xs, ys, zs
+
+mutual
+    public export
+    Eq a => Eq b => Eq (Odd a b) where
+        x :: xs == y :: ys = x == y && xs == ys
+
+    public export
+    Eq a => Eq b => Eq (Even a b) where
+        [] == [] = True
+        x :: xs == y :: ys = x == y && xs == ys
+        _ == _ = False
+
+mutual
+    public export
+    Ord a => Ord b => Ord (Odd a b) where
+        compare (x :: xs) (y ::ys)
+           = case compare x y of
+                  EQ => compare xs ys
+                  c => c
+
+    public export
+    Ord a => Ord b => Ord (Even a b) where
+        compare [] [] = EQ
+        compare [] (x :: xs) = LT
+        compare (x :: xs) [] = GT
+        compare (x :: xs) (y ::ys)
+           = case compare x y of
+                  EQ => compare xs ys
+                  c => c
+
+mutual
+    public export
+    Bifunctor Odd where
+        bimap f g (x :: xs) = (f x) :: (bimap g f xs)
+
+    public export
+    Bifunctor Even where
+        bimap f g [] = []
+        bimap f g (x :: xs) = (f x) :: (bimap g f xs)
+
+mutual
+    public export
+    Bifoldable Odd where
+        bifoldr f g acc (x :: xs) = f x (bifoldr g f acc xs)
+
+        bifoldl f g acc (x :: xs) = bifoldl g f (f acc x) xs
+
+    public export
+    Bifoldable Even where
+        bifoldr f g acc [] = acc
+        bifoldr f g acc (x :: xs) = f x (bifoldr g f acc xs)
+
+        bifoldl f g acc [] = acc
+        bifoldl f g acc (x :: xs) = bifoldl g f (f acc x) xs
+
+mutual
+    public export
+    Bitraversable Odd where
+        bitraverse f g (x :: xs) = [| f x :: bitraverse g f xs |]
+
+    public export
+    Bitraversable Even where
+        bitraverse f g [] = [| [] |]
+        bitraverse f g (x :: xs) = [| f x :: bitraverse g f xs |]
+
+namespace Snd
+    public export
+    Functor (Odd a) where
+        map = mapSnd
+
+namespace Fst
+    public export
+    [FstFunctor] Functor (\a => Odd a b) where
+        map = mapFst
+
+mutual
+    namespace Odd
+        public export
+        (++) : Odd a b -> Odd b a -> Even a b
+        (x :: xs) ++ ys = x :: xs ++ ys
+
+    namespace EvenOdd
+        public export
+        (++) : Even a b -> Odd a b -> Odd a b
+        [] ++ ys = ys
+        (x :: xs) ++ ys = x :: xs ++ ys
+
+mutual
+    namespace Even
+        public export
+        (++) : Even a b -> Even a b -> Even a b
+        [] ++ ys = ys
+        (x :: xs) ++ ys = x :: xs ++ ys
+
+    namespace OddEven
+        public export
+        (++) : Odd a b -> Even b a -> Odd a b
+        (x :: xs) ++ ys = x :: xs ++ ys
+
+||| The semigroup structure induced by treating Odd as the free extension of a
+||| monoid `a`, with variables in `b`
+public export
+Semigroup a => Semigroup (Odd a b) where
+    [x] <+> (y :: ys) = (x <+> y) :: ys
+    (x :: y :: xs) <+> ys = x :: y :: xs <+> ys
+
+namespace Odd
+    public export
+    (+>) : Semigroup a => Odd a b -> a -> Odd a b
+    [x] +> z = [x <+> z]
+    x :: y :: xs +> z = x :: y :: (xs +> z)
+
+    public export
+    (<+) : Semigroup a => a -> Odd a b -> Odd a b
+    x <+ y :: ys = (x <+> y) :: ys
+
+public export
+Semigroup (Even a b) where
+    (<+>) = (++)
+
+public export
+Monoid a => Monoid (Odd a b) where
+    neutral = [neutral]
+
+public export
+Monoid (Even a b) where
+    neutral = []
+
+public export
+Foldable (Odd a) where
+    foldr = bifoldr (flip const)
+    foldl = bifoldl const
+
+public export
+singleton : a -> Odd a b
+singleton x = [x]
+
+namespace Snd
+    public export
+    Monoid a => Applicative (Odd a) where
+        pure x = [neutral, x, neutral]
+        fs <*> xs = biconcatMap singleton (flip map xs) fs
+
+public export
+flatten : Odd (Odd a b) b -> Odd a b
+flatten [x] = x
+flatten (x :: y :: xs) = x ++ (y :: flatten xs)
+
+namespace Fst
+    public export
+    [FstApplicative] Applicative (\a => Odd a b) using FstFunctor where
+        pure x = [x]
+        fs <*> xs = flatten $ bimap (flip mapFst xs) id fs
+
+public export
+Monoid a => Alternative (Odd a) where
+    empty = [neutral]
+    xs <|> ys = xs <+> ys
+
+namespace Snd
+    public export
+    [SndMonad] Monoid a => Monad (Odd a) where
+        x >>= f = biconcatMap singleton f x
+
+    public export
+    (>>=) : Monoid a => Odd a b -> (b -> Odd a c) -> Odd a c
+    (>>=) = (>>=) @{SndMonad}
+
+namespace Fst
+    public export
+    [FstMonad] Monad (\a => Odd a b) using FstApplicative where
+        x >>= f = flatten $ mapFst f x
+        join = flatten
+
+    public export
+    (>>=) : Odd a c -> (a -> Odd b c) -> Odd b c
+    (>>=) = (>>=) @{FstMonad}
+
+public export
+Traversable (Odd a) where
+    traverse = bitraverse pure
+
+mutual
+    namespace Odd
+        public export
+        forget : Odd a a -> List a
+        forget (x :: xs) = x :: forget xs
+
+    namespace Even
+        public export
+        forget : Even a a -> List a
+        forget [] = []
+        forget (x :: xs) = x :: forget xs
+
+export
+Show a => Show b => Show (Odd a b) where
+    show xs = "[\{concat $ intersperse ", " $ forget $ bimap show show xs}]"
+
+export
+Show a => Show b => Show (Even a b) where
+    show xs = "[\{concat $ intersperse ", " $ forget $ bimap show show xs}]"
diff --git a/libs/contrib/Data/String/Parser.idr b/libs/contrib/Data/String/Parser.idr
index 4af903c03..b46e74e78 100644
--- a/libs/contrib/Data/String/Parser.idr
+++ b/libs/contrib/Data/String/Parser.idr
@@ -6,6 +6,7 @@ import Control.Monad.Trans
 import Data.String
 import Data.Fin
 import Data.List
+import Data.List.Alternating
 import Data.List1
 import Data.Vect
 
@@ -353,6 +354,20 @@ covering
 commaSep : Monad m => ParseT m a -> ParseT m (List a)
 commaSep p = p `sepBy` (char ',')
 
+||| Parses alternating occurrences of `a`s and `b`s.
+||| Can be thought of as parsing:
+||| - a list of `b`s, separated, and surrounded, by `a`s
+||| - a non-empty list of `a`s, separated by `b`s
+||| where we care about the separators
+export
+covering
+alternating : Monad m
+           => ParseT m a
+           -> ParseT m b
+           -> ParseT m (Odd a b)
+alternating x y = do vx <- x
+                     (vx ::) <$> [| y :: alternating x y |] <|> pure [vx]
+
 ||| Run the specified parser precisely `n` times, returning a vector
 ||| of successes.
 export
diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg
index e58d1ec97..c32b95021 100644
--- a/libs/contrib/contrib.ipkg
+++ b/libs/contrib/contrib.ipkg
@@ -54,6 +54,7 @@ modules = Control.ANSI,
           Data.List.Palindrome,
           Data.List.HasLength,
           Data.List.AtIndex,
+          Data.List.Alternating,
 
           Data.List.Elem.Extra,
 
diff --git a/tests/chez/chez027/StringParser.idr b/tests/chez/chez027/StringParser.idr
index a22e99d55..0e41ed4d7 100644
--- a/tests/chez/chez027/StringParser.idr
+++ b/tests/chez/chez027/StringParser.idr
@@ -3,6 +3,7 @@ module Main
 import Control.Monad.Identity
 import Control.Monad.Trans
 
+import Data.List.Alternating
 import Data.Maybe
 import Data.Vect
 import Data.String.Parser
@@ -65,6 +66,8 @@ main = do
     showRes res
     res <- parseT (commaSep alphaNum) "a,1,b,2"
     showRes res
+    res <- parseT (alternating letter natural) "a12b3c"
+    showRes res
     res <- parseT (ntimes 4 letter) "abcd"
     showRes res
     res <- parseT (requireFailure letter) "1"
diff --git a/tests/chez/chez027/expected b/tests/chez/chez027/expected
index ce9786b32..ce140b9f8 100644
--- a/tests/chez/chez027/expected
+++ b/tests/chez/chez027/expected
@@ -11,6 +11,7 @@ Parse failed at position 0: Not good
 True
 False
 ['a', '1', 'b', '2']
+['a', 12, 'b', 3, 'c']
 ['a', 'b', 'c', 'd']
 ()
 Parse failed at position 0: Purposefully changed OK to Fail
diff --git a/tests/contrib/list_alternating/AlternatingList.idr b/tests/contrib/list_alternating/AlternatingList.idr
new file mode 100644
index 000000000..f36048cd7
--- /dev/null
+++ b/tests/contrib/list_alternating/AlternatingList.idr
@@ -0,0 +1,63 @@
+import Data.List.Alternating
+
+main : IO ()
+main = do
+    let xs = the (Odd Double String) [1, "Hello", 2, "world", 3]
+    let ys = the (Odd Double String) [1, "Hello", 0, "world", 3]
+
+    printLn xs
+
+    printLn $ xs == xs
+    printLn $ xs == ys
+
+    printLn $ compare xs xs == EQ
+    printLn $ compare xs ys == GT
+
+    printLn $ bimap (+ 1) (++ "!") xs
+
+    printLn $ bifoldr (mapFst . avg) (mapSnd . join) (0, "") xs
+    printLn $ bifoldl (flip $ mapFst . avg) (flip $ mapSnd . (flip join)) (0, "") xs
+
+    ignore $ bitraverse printLn printLn xs
+
+    printLn $ map (++ "!") xs
+
+    printLn $ the (Odd Double String) $ [1, "Hello"] ++ [2, "world", 3]
+    printLn $ the (Odd Double String) $ [1, "Hello", 2] ++ ["world", 3]
+
+    let us = the (Odd String Double) ["Hello", 0, "world", 1, "!"]
+    let vs = the (Odd String Double) ["Lorem", 1, "ipsum"]
+
+    printLn $ us <+> vs
+    printLn $ us +> "!"
+    printLn $ "Oh, " <+ us
+    printLn $ the (Odd String Double) neutral
+
+    printLn $ foldr avg 0 us
+    printLn $ foldl avg 0 us
+
+    printLn $ the (Odd String Double) $ pure 1
+    printLn $ the (Odd String Double) $ ["Hello", (+1), "world", (+10), "!"] <*> ["Lorem", 1, "ipsum", 2, "."]
+
+    printLn $ the (Odd String Double) empty
+    printLn $ us <|> vs
+
+    printLn $ Snd.do
+        x <- the (Odd String Double) ["Hello", 1, "world", 2, "!"]
+        [",", x + 1, " "]
+
+    printLn $ Fst.do
+        x <- the (Odd String Double) ["Hello", 1, "world", 2, "!"]
+        ["Um,", 3, x]
+
+    ignore $ traverse printLn us
+
+    printLn $ the (List String) $ forget $ mapFst show xs
+  where
+    avg : Double -> Double -> Double
+    avg x y = (x + y) / 2
+
+    join : String -> String -> String
+    join "" t = t
+    join s "" = s
+    join s t = s ++ " " ++ t
diff --git a/tests/contrib/list_alternating/expected b/tests/contrib/list_alternating/expected
new file mode 100644
index 000000000..07b486edb
--- /dev/null
+++ b/tests/contrib/list_alternating/expected
@@ -0,0 +1,33 @@
+1/1: Building AlternatingList (AlternatingList.idr)
+Main> [1.0, "Hello", 2.0, "world", 3.0]
+True
+False
+True
+True
+[2.0, "Hello!", 3.0, "world!", 4.0]
+(1.375, "Hello world")
+(2.125, "Hello world")
+1.0
+"Hello"
+2.0
+"world"
+3.0
+[1.0, "Hello!", 2.0, "world!", 3.0]
+[1.0, "Hello", 2.0, "world", 3.0]
+[1.0, "Hello", 2.0, "world", 3.0]
+["Hello", 0.0, "world", 1.0, "!Lorem", 1.0, "ipsum"]
+["Hello", 0.0, "world", 1.0, "!!"]
+["Oh, Hello", 0.0, "world", 1.0, "!"]
+[""]
+0.25
+0.5
+["", 1.0, ""]
+["HelloLorem", 2.0, "ipsum", 3.0, ".worldLorem", 11.0, "ipsum", 12.0, ".!"]
+[""]
+["Hello", 0.0, "world", 1.0, "!Lorem", 1.0, "ipsum"]
+["Hello,", 2.0, " world,", 3.0, " !"]
+["Um,", 3.0, "Hello", 1.0, "Um,", 3.0, "world", 2.0, "Um,", 3.0, "!"]
+0.0
+1.0
+["1.0", "Hello", "2.0", "world", "3.0"]
+Main> Bye for now!
diff --git a/tests/contrib/list_alternating/input b/tests/contrib/list_alternating/input
new file mode 100644
index 000000000..fc5992c29
--- /dev/null
+++ b/tests/contrib/list_alternating/input
@@ -0,0 +1,2 @@
+:exec main
+:q
diff --git a/tests/contrib/list_alternating/run b/tests/contrib/list_alternating/run
new file mode 100644
index 000000000..7e88e7af1
--- /dev/null
+++ b/tests/contrib/list_alternating/run
@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-banner --no-color --console-width 0 -p contrib AlternatingList.idr < input