From 6bf03f71c5aecd49aad5e9e724845fe1e9a01022 Mon Sep 17 00:00:00 2001
From: gspia <iahogsp@gmail.com>
Date: Tue, 7 Jan 2020 20:14:53 +0200
Subject: [PATCH] Add Take, Drop and Reverse functions

This commit adds the functions listed in the title.
The implementations follow the algorithms given in Data.List for
the corresponding term-level functions.
---
 src/Fcf/Data/List.hs | 78 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 78 insertions(+)

diff --git a/src/Fcf/Data/List.hs b/src/Fcf/Data/List.hs
index 660e8f9..9011931 100644
--- a/src/Fcf/Data/List.hs
+++ b/src/Fcf/Data/List.hs
@@ -32,6 +32,9 @@ module Fcf.Data.List
   , Zip
   , Unzip
   , Cons2
+  , Take
+  , Drop
+  , Reverse
   ) where
 
 import qualified GHC.TypeLits as TL
@@ -205,3 +208,78 @@ type instance Eval (Unzip as) = Eval (Foldr Cons2 '( '[], '[]) (Eval as))
 data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])
 type instance Eval (Cons2 '(a, b) '(as, bs)) = '(a ': as, b ': bs)
 
+
+-- Helper for the Take. This corresponds to the unsafeTake in the data list lib.
+data UtakeStop :: Nat -> [a] -> Exp [a]
+type instance Eval (UtakeStop 0 _)         = '[]
+type instance Eval (UtakeStop 1 (a ': as)) = '[a]
+
+-- Helper for the Take. This corresponds to the unsafeTake in the data list lib.
+data Utake :: Nat -> [a] -> Exp [a]
+-- As the following refuses to compile, we use UtakeStop-helper.
+-- type instance Eval (Utake 0 (a ': as)) = '[]
+-- type instance Eval (Utake 1 (a ': as)) = '[a]
+-- type instance Eval (Utake m (a ': as)) = Eval ('(:) a <$> (Utake (m TL.- 1) as))
+type instance Eval (Utake n (a ': as)) = Eval
+  (If (Eval (n < 2))
+    (UtakeStop n (a ': as))
+    ('(:) a <$> (Utake (n TL.- 1) as))
+  )
+
+-- | Type-level list take.
+--
+-- === Example
+--
+-- @
+-- :kind! Eval (Take 2 '[1,2,3,4,5])
+-- @
+data Take :: Nat -> [a] -> Exp [a]
+type instance Eval (Take n as) = Eval
+  (If (Eval (n > 0))
+    (Utake n as)
+    (Pure '[])
+  )
+
+-- Helper for the Drop. This corresponds to the unsafeDrop in the data list lib.
+data UdropStop :: Nat -> [a] -> Exp [a]
+type instance Eval (UdropStop 0 _ )        = '[]
+type instance Eval (UdropStop 1 (a ': as)) = as
+-- Helper for the Drop. This corresponds to the unsafeDrop in the data list lib.
+data Udrop :: Nat -> [a] -> Exp [a]
+type instance Eval (Udrop n (a ': as)) = Eval
+  (If (Eval (n < 2))
+    (UdropStop n (a ': as))
+    (Udrop (n TL.- 1) as)
+  )
+
+-- | Type-level list drop.
+--
+-- === Example
+--
+-- @
+-- :kind! Eval (Drop 2 '[1,2,3,4,5])
+-- @
+data Drop :: Nat -> [a] -> Exp [a]
+type instance Eval (Drop n as) = Eval
+  (If (Eval (n > 0))
+    (Udrop n as)
+    (Pure as)
+  )
+
+
+-- Helper for Reverse. This corresponds to rev in the data list lib.
+data Rev :: [a] -> [a] -> Exp [a]
+type instance Eval (Rev '[]       a) = a
+type instance Eval (Rev (x ': xs) a) = Eval (Rev xs (x ': a))
+
+
+-- | Type-level list reverse.
+--
+-- === Example
+--
+-- @
+-- :kind! Eval (Reverse '[1,2,3,4,5])
+-- @
+data Reverse :: [a] -> Exp [a]
+type instance Eval (Reverse l) = Eval (Rev l '[])
+