{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Type.List (module Type.List, module X) where
import Prelude
import GHC.TypeLits
import Type.Bool
import Type.Container as X
import qualified Type.Set as Set
import Type.Monoid as X
data Lst (l :: [k])
type family FromLst a where FromLst (Lst l) = l
type family Removed (el :: e) (cont :: c) :: l
type family RemovedIdx (idx :: Nat) (cont :: c) :: l
type family ElAt (idx :: Nat) (cont :: c) :: l
type instance Removed (el :: e) ((l ': ls) :: [e]) = If (el == l) ls (l ': Removed el ls)
type instance RemovedIdx idx (l ': ls) = If (idx == 0) ls (l ': RemovedIdx (idx - 1) ls)
type instance ElAt idx (l ': ls) = If (idx == 0) l (ElAt (idx - 1) ls)
type instance In a (l ': ls) = If (a == l) 'True (In a ls)
type instance In a '[] = 'False
type family SuccMaybe (m :: Maybe Nat) where SuccMaybe ('Just n) = 'Just (n + 1)
SuccMaybe 'Nothing = 'Nothing
type instance Index a (l ': ls) = If (a == l) ('Just 0) (SuccMaybe (Index a ls))
type instance Index a '[] = ('Nothing :: Maybe Nat)
type instance IndexF a (l ': ls) = If (a == l) 0 (IndexF a ls + 1)
data Recursive a
type instance Index a (Recursive (l ': ls)) = If (a == l) ('Just 0) (SuccMaybe (Index a (Recursive ls)))
type instance Index a (Recursive '[] ) = ('Nothing :: Maybe Nat)
type instance Index2 n (a ': as) = If (n == 0) a (Index2 (n - 1) as)
type instance Empty '[] = 'True
type instance Empty (a ': as) = 'False
type instance Append a '[] = '[a]
type instance Append a (l ': ls) = l ': Append a ls
type instance Concat ('[] :: [k]) (lst :: [k]) = lst
type instance Concat ( (l ': ls) :: [k]) (lst :: [k]) = l ': Concat ls lst
type instance Remove a '[] = '[]
type instance Remove a (l ': ls) = If (a == l) ls (l ': Remove a ls)
type instance Diff l '[] = l
type instance Diff l (e ': es) = Diff (Remove e l) es
type instance Size '[] = 0
type instance Size (a ': as) = 1 + Size as
type family Head lst where
Head '[] = 'Nothing
Head (a ': as) = 'Just a
type family Head' lst where Head' (a ': as) = a
type family UniqueFix lst where UniqueFix '[] = '[]
UniqueFix lst = Unique lst
type instance Unique (lst :: [k]) = Set.ToList (Set.AsSet lst)
type instance Reverse (lst :: [k]) = Reverse' lst '[]
type family Reverse' lst lst' where
Reverse' '[] lst = lst
Reverse' (l ': ls) lst = Reverse' ls (l ': lst)
type family Take (n :: Nat) lst where
Take 0 lst = '[]
Take n (l ': ls) = l ': Take (n - 1) ls
type family Drop (n :: Nat) lst where
Drop 0 lst = lst
Drop n (l ': ls) = Drop (n - 1) ls
type family Join (lst :: [[k]]) :: [k] where
Join '[] = '[]
Join (lst ': lsts) = Concat lst (Join lsts)
type family Last (lst :: [k]) :: k where
Last '[x] = x
Last (x ': xs) = Last xs
type family Init (lst :: [k]) :: [k] where
Init '[] = '[]
Init '[x] = '[]
Init (x ': xs) = x ': Init xs
type family DropInit (lst :: [k]) :: [k] where
DropInit '[] = '[]
DropInit '[x] = '[x]
DropInit (x ': xs) = DropInit xs
type family Replicate (n :: Nat) a where
Replicate 0 a = '[]
Replicate n a = a ': Replicate (n - 1) a
type Zip a b = Zip2 a b
type family Zip2 (l1 :: [*]) (l2 :: [*]) :: [*] where
Zip2 (x1 ': xs1) (x2 ': xs2) = (x1,x2) ': Zip2 xs1 xs2
Zip2 l1 l2 = '[]
type family Zip3 (l1 :: [*]) (l2 :: [*]) (l3 :: [*]) :: [*] where
Zip3 (x1 ': xs1) (x2 ': xs2) (x3 ': xs3) = (x1,x2,x3) ': Zip3 xs1 xs2 xs3
Zip3 l1 l2 l3 = '[]
type family Zip4 (l1 :: [*]) (l2 :: [*]) (l3 :: [*]) (l4 :: [*]) :: [*] where
Zip4 (x1 ': xs1) (x2 ': xs2) (x3 ': xs3) (x4 ': xs4) = (x1,x2,x3,x4) ': Zip4 xs1 xs2 xs3 xs4
Zip4 l1 l2 l3 l4 = '[]
type family Zip5 (l1 :: [*]) (l2 :: [*]) (l3 :: [*]) (l4 :: [*]) (l5 :: [*]) :: [*] where
Zip5 (x1 ': xs1) (x2 ': xs2) (x3 ': xs3) (x4 ': xs4) (x5 ': xs5) = (x1,x2,x3,x4,x5) ': Zip5 xs1 xs2 xs3 xs4 xs5
Zip5 l1 l2 l3 l4 l5 = '[]
type family Unzip2 (lst :: [*]) :: ([*], [*]) where
Unzip2 '[] = '( '[], '[] )
Unzip2 ((x1,x2) ': lst) = PrependAll (x1,x2) (Unzip2 lst)
type family PrependAll (els :: *) (lsts :: k) :: k
type instance PrependAll (t1,t2) '(l1,l2) = '(t1 ': l1, t2 ': l2)
type instance PrependAll (t1,t2,t3) '(l1,l2,l3) = '(t1 ': l1, t2 ': l2, t3 ': l3)
type instance PrependAll (t1,t2,t3,t4) '(l1,l2,l3,l4) = '(t1 ': l1, t2 ': l2, t3 ': l3, t4 ': l4)
type instance PrependAll (t1,t2,t3,t4,t5) '(l1,l2,l3,l4,l5) = '(t1 ': l1, t2 ': l2, t3 ': l3, t4 ': l4, t5 ': l5)
type family Select (n :: Nat) (a :: *) :: *
type instance Select 1 (t1,t2) = t1
type instance Select 2 (t1,t2) = t2
type instance Select 1 (t1,t2,t3) = t1
type instance Select 2 (t1,t2,t3) = t2
type instance Select 3 (t1,t2,t3) = t3
type instance Select 1 (t1,t2,t3,t4) = t1
type instance Select 2 (t1,t2,t3,t4) = t2
type instance Select 3 (t1,t2,t3,t4) = t3
type instance Select 4 (t1,t2,t3,t4) = t4
type instance Select 1 (t1,t2,t3,t4,t5) = t1
type instance Select 2 (t1,t2,t3,t4,t5) = t2
type instance Select 3 (t1,t2,t3,t4,t5) = t3
type instance Select 4 (t1,t2,t3,t4,t5) = t4
type instance Select 5 (t1,t2,t3,t4,t5) = t5
type family Update (n :: Nat) (a :: k) (lst :: [k]) :: [k] where
Update 0 a (l ': ls) = a ': ls
Update n a (l ': ls) = l ': Update (n - 1) a ls
type family TakeUntil (a :: k) (ls :: [k]) :: [k] where
TakeUntil a '[] = '[]
TakeUntil a (a ': ls) = '[a]
TakeUntil a (l ': ls) = l ': TakeUntil a ls