mirror of
https://github.com/Lysxia/first-class-families.git
synced 2024-10-27 03:49:57 +03:00
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.
This commit is contained in:
parent
7caa2aa745
commit
6bf03f71c5
@ -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 '[])
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user