module Data.HSet.TypeLevel
( Nat(..)
, Elem
, Index
, MayIndexGo
, MayIndex
, MayFstIndexSnd
, TEq
, Length
, Append
, AppendUniq
, Union
, UnionList'
, UnionList
, XReverse
, Reverse
, Delete
, Replace
, TagElem
, And
, HSubset
) where
import Data.Tagged
data Nat = Z | S Nat
type family Elem (typ :: k) (typs :: [k]) :: Bool where
Elem typ '[] = 'False
Elem typ (typ ': typs) = 'True
Elem typ1 (typ2 ': typs) = Elem typ1 typs
type family Index (typ :: k) (typs :: [k]) :: Nat where
Index t (t ': ts) = 'Z
Index t (tt ': ts) = 'S (Index t ts)
type family MayIndexGo (typ :: k) (typs :: [k]) (acc :: Nat) :: (Maybe Nat) where
MayIndexGo t (t ': ts) acc = 'Just acc
MayIndexGo t (tt ': ts) acc = MayIndexGo t ts ('S acc)
MayIndexGo t '[] acc = 'Nothing
type MayIndex typ typs = MayIndexGo typ typs 'Z
type family MayFstIndexSnd (ts1 :: [k]) (ts2 :: [k]) :: (Maybe Nat) where
MayFstIndexSnd (e ': els) x = MayIndex e x
MayFstIndexSnd '[] x = 'Nothing
type family TEq (t1 :: k) (t2 :: k) :: Bool where
TEq a a = 'True
TEq a b = 'False
type family Length (list :: [*]) :: Nat where
Length '[] = 'Z
Length (x ': xs) = 'S (Length xs)
type family Append (l1 :: [*]) (l2 :: [*]) :: [*] where
Append '[] x = x
Append x '[] = x
Append (x ': xs) ys = x ': (Append xs ys)
type family AppendUniq (typs :: [*]) (typ :: *) :: [*] where
AppendUniq (t ': ts) t = t ': ts
AppendUniq (t ': ts) t1 = t ': (AppendUniq ts t1)
AppendUniq '[] t1 = '[t1]
type family Union (l1 :: [*]) (l2 :: [*]) :: [*] where
Union l1 '[] = l1
Union l1 (l ': ls) = Union (AppendUniq l1 l) ls
type family UnionList' (acc :: [*]) (ls :: [[*]]) :: [*] where
UnionList' acc (e ': es) = UnionList' (Union acc e) es
UnionList' acc '[] = acc
type UnionList l = UnionList' '[] l
type family XReverse (acc :: [*]) (l :: [*]) :: [*] where
XReverse acc '[] = acc
XReverse acc (e ': els) = XReverse (e ': acc) els
type Reverse a = XReverse '[] a
type family Delete (typ :: *) (typs :: [*]) :: [*] where
Delete x '[] = '[]
Delete x (x ': ys) = Delete x ys
Delete x (y ': ys) = y ': (Delete x ys)
type family Replace (typ1 :: *) (typ2 :: *) (typs :: [*]) :: [*] where
Replace a b (a ': xs) = (b ': xs)
Replace a b (x ': xs) = x ': (Replace a b xs)
type TagElem (tag :: k) (typ :: *) (typs :: [*])
= Replace typ (Tagged tag typ) typs
type family And (a :: Bool) (b :: Bool) where
And 'False x = 'False
And x 'False = 'False
And x y = 'True
type family HSubset (h1 :: [k]) (h2 :: [k]) where
HSubset '[] x = 'True
HSubset x '[] = 'False
HSubset (h1 ': tl2) h2 = And (Elem h1 h2) (HSubset tl2 h2)