{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
module Haskus.Utils.Types.List
(
Snoc
, Concat
, Replicate
, Zip
, RemoveAt
, RemoveAt1
, RemoveAtN
, Remove
, Nub
, NubHead
, Head
, Tail
, Init
, Take
, Drop
, InsertAt
, ReplaceAt
, Replace
, ReplaceN
, ReplaceNS
, CheckMember
, CheckMembers
, Union
, Complement
, Product
, Member
, Members
, CheckNub
, IndexOf
, IndexesOf
, MaybeIndexOf
, Index
, Reverse
, Generate
, Map
, Max
, Length
, Indexes
, MapTest
)
where
import Haskus.Utils.Types
import GHC.Exts (Constraint)
type family Map (f :: a -> k) (xs :: [a]) :: [k] where
Map f '[] = '[]
Map f (x ': xs) = f x ': Map f xs
type family Max (xs :: [Nat]) where
Max (x ': xs) = Max' x xs
type family Max' (x :: Nat) (xs :: [Nat]) where
Max' x '[] = x
Max' x (a ': xs) = Max' (If (x <=? a) a x) xs
type family Tail (xs :: [k]) :: [k] where
Tail (x ': xs) = xs
type family Drop (n :: Nat) (xs :: [k]) :: [k] where
Drop 0 xs = xs
Drop n (x ': xs) = Drop (n-1) xs
type family Take (n :: Nat) (xs :: [k]) :: [k] where
Take 0 xs = '[]
Take n (x ': xs) = x ': (Take (n-1) xs)
type family Init (xs :: [k]) :: [k] where
Init '[x] = '[]
Init (x ': xs) = x ': (Init xs)
type family Snoc (xs :: [k]) (x :: k) :: [k] where
Snoc '[] x = '[x]
Snoc (y ': ys) x = y ': (Snoc ys x)
type family Head (xs :: [k]) :: k where
Head (x ': xs) = x
type family Concat (xs :: [k]) (ys :: [k]) :: [k] where
Concat '[] '[] = '[]
Concat '[] ys = ys
Concat (x ': xs) ys = x ': Concat xs ys
type family Length (xs :: [k]) :: Nat where
Length xs = Length' 0 xs
type family Length' n (xs :: [k]) :: Nat where
Length' n '[] = n
Length' n (x ': xs) = Length' (n+1) xs
type family Replicate (n :: Nat) (s :: k) :: [k] where
Replicate n s = Replicate' s n '[]
type family Replicate' (x :: k) (n :: Nat) (xs :: [k]) :: [k] where
Replicate' x 0 xs = xs
Replicate' x n xs = Replicate' x (n-1) (x ': xs)
type family InsertAt (n :: Nat) (l :: [k]) (l2 :: [k]) :: [k] where
InsertAt 0 xs ys = Concat ys xs
InsertAt n (x ': xs) ys = x ': InsertAt (n-1) xs ys
type family ReplaceAt (n :: Nat) (l :: [k]) (l2 :: [k]) :: [k] where
ReplaceAt 0 (x ': xs) ys = Concat ys xs
ReplaceAt n (x ': xs) ys = x ': ReplaceAt (n-1) xs ys
type family Replace (t1 :: k) (t2 :: k) (l :: [k]) :: [k] where
Replace t1 t2 '[] = '[]
Replace t1 t2 (t1 ': xs) = t2 ': (Replace t1 t2 xs)
Replace t1 t2 (x ': xs) = x ': (Replace t1 t2 xs)
type family ReplaceN (n :: Nat) (t :: k) (l :: [k]) :: [k] where
ReplaceN 0 t (x ': xs) = (t ': xs)
ReplaceN n t (x ': xs) = x ': ReplaceN (n-1) t xs
type family ReplaceNS (ns :: [Nat]) (t :: k) (l :: [k]) :: [k] where
ReplaceNS '[] t l = l
ReplaceNS (i ': is) t l = ReplaceNS is t (ReplaceN i t l)
type family Reverse (l :: [k]) :: [k] where
Reverse l = Reverse' l '[]
type family Reverse' (l :: [k]) (l2 :: [k]) :: [k] where
Reverse' '[] l = l
Reverse' (x ': xs) l = Reverse' xs (x ': l)
type family RemoveAt (n :: Nat) (l :: [k]) :: [k] where
RemoveAt 0 (x ': xs) = xs
RemoveAt n (x ': xs) = x ': RemoveAt (n-1) xs
type family RemoveAt1 (n :: Nat) (l :: [k]) :: [k] where
RemoveAt1 0 xs = xs
RemoveAt1 1 (x ': xs) = xs
RemoveAt1 n (x ': xs) = x ': RemoveAt1 (n-1) xs
type family RemoveAtN (ns :: [Nat]) (l :: [k]) :: [k] where
RemoveAtN '[] xs = xs
RemoveAtN (i ': is) xs = RemoveAtN is (RemoveAt i xs)
type family Generate (n :: Nat) (m :: Nat) :: [Nat] where
Generate n n = '[]
Generate n m = n ': Generate (n+1) m
type family CheckMember (a :: k) (l :: [k]) :: Constraint where
CheckMember a l = CheckMember' l a l
type family CheckMember' (i :: [k]) (a :: k) (l :: [k]) :: Constraint where
CheckMember' i a (a ': l) = ()
CheckMember' i a (b ': l) = CheckMember' i a l
CheckMember' i a '[] = TypeError ( 'Text "`"
':<>: 'ShowType a
':<>: 'Text "'"
':<>: 'Text " is not a member of "
':<>: 'ShowType i)
type family CheckMembers (l1 :: [k]) (l2 :: [k]) :: Constraint where
CheckMembers l1 l1 = ()
CheckMembers l1 l2 = CheckMembers' l2 '[] l1 l2
type family CheckMembers' (i :: [k]) (e :: [k]) (l1 :: [k]) (l2 :: [k]) :: Constraint where
CheckMembers' i e '[] '[] = TypeError ( 'ShowType e
':$$: 'Text "is not a subset of"
':$$: 'ShowType i)
CheckMembers' i e '[] l2 = ()
CheckMembers' i e (l ': ls) '[] = CheckMembers' i (l ': e) ls i
CheckMembers' i e (x ': xs) (x ': ys) = CheckMembers' i e xs i
CheckMembers' i e (x ': xs) (y ': ys) = CheckMembers' i e (x ': xs) ys
type family Indexes (l :: [k]) :: [Nat] where
Indexes xs = IndexesFrom 0 xs
type family IndexesFrom (n :: Nat) (xs :: [k]) :: [Nat] where
IndexesFrom n '[] = '[]
IndexesFrom n (x ': xs) = n ': IndexesFrom (n+1) xs
type family MapTest (a :: k) (l :: [k]) :: [Nat] where
MapTest a '[] = '[]
MapTest a (a ': xs) = 1 ': MapTest a xs
MapTest a (x ': xs) = 0 ': MapTest a xs
type family Zip (l :: [*]) (l2 :: [*]) where
Zip '[] xs = '[]
Zip xs '[] = '[]
Zip (x ': xs) (y ': ys) = (x,y) ': Zip xs ys
type family Remove (a :: k) (l :: [k]) :: [k] where
Remove a '[] = '[]
Remove a (a ': as) = Remove a as
Remove a (b ': as) = b ': Remove a as
type family Nub (l :: [k]) :: [k] where
Nub xs = Reverse (Nub' xs '[])
type family Nub' (as :: [k]) (xs :: [k]) :: [k] where
Nub' '[] xs = xs
Nub' (x ': as) xs = Nub' (Remove x as) (x ': xs)
type family NubHead (l :: [k]) :: [k] where
NubHead '[] = '[]
NubHead (x ': xs) = x ': Remove x xs
type family IndexOf (a :: k) (l :: [k]) :: Nat where
IndexOf x xs = IndexOf' x xs xs
type family IndexOf' (a :: k) (l :: [k]) (l2 :: [k]) :: Nat where
IndexOf' x (x ': xs) l2 = 0
IndexOf' y (x ': xs) l2 = 1 + IndexOf' y xs l2
type family IndexesOf (a :: k) (l :: [k]) :: [Nat] where
IndexesOf x xs = IndexesOf' 0 x xs
type family IndexesOf' n (a :: k) (l :: [k]) :: [Nat] where
IndexesOf' n x '[] = '[]
IndexesOf' n x (x ': xs) = n ': IndexesOf' (n+1) x xs
IndexesOf' n x (y ': xs) = IndexesOf' (n+1) x xs
type family MaybeIndexOf (a :: k) (l :: [k]) where
MaybeIndexOf x xs = MaybeIndexOf' 0 x xs
type family MaybeIndexOf' (n :: Nat) (a :: k) (l :: [k]) where
MaybeIndexOf' n x '[] = 0
MaybeIndexOf' n x (x ': xs) = 1 + n
MaybeIndexOf' n x (y ': xs) = MaybeIndexOf' (n+1) x xs
type family Index (n :: Nat) (l :: [k]) :: k where
Index 0 (x ': xs) = x
Index n (x ': xs) = Index (n-1) xs
type family Union (xs :: [k]) (ys :: [k]) :: [k] where
Union xs ys = Nub (Concat xs ys)
type family Complement (xs :: [k]) (ys :: [k]) :: [k] where
Complement xs '[] = xs
Complement xs (y:ys) = Complement (Remove y xs) ys
type family Product (xs :: [*]) (ys :: [*]) :: [*] where
Product '[] ys = '[]
Product xy '[] = '[]
Product (x:xs) ys = Concat (Product' x ys) (Product xs ys)
type family Product' (x :: *) (ys :: [*]) :: [*] where
Product' x '[] = '[]
Product' x (y ': ys) = (x,y) ': Product' x ys
type Member x xs =
( x ~ Index (IndexOf x xs) xs
, KnownNat (IndexOf x xs)
)
type family Members xs ys :: Constraint where
Members '[] ys = ()
Members (x ': xs) ys = (Member x ys, Members xs ys)
type CheckNub (l :: [k]) =
( CheckNubEx l (Nub l) ~ 'True
)
type family CheckNubEx (l1 :: [k]) (l2 :: [k]) where
CheckNubEx l l = 'True
CheckNubEx l1 l2 = TypeError
( 'Text "Type-list contains unallowed redundant types."
':$$: 'Text "Got: " ':<>: 'ShowType l1
':$$: 'Text "Expected: " ':<>: 'ShowType l2
)