typed-encoding-0.4.2.0: Type safe string transformations

Safe HaskellSafe
LanguageHaskell2010

Data.TypedEncoding.Common.Util.TypeLits

Description

TypeLits related utilities.

Lots of this could be avoided by adding singletons as dependency.

Uses symbols library for its ToList type family.

Currently this is spread out in different modules

(TODO) these will need to get consolidated.

Synopsis

Documentation

>>> :set -XScopedTypeVariables -XTypeFamilies -XKindSignatures -XDataKinds

type family AcceptEq (msg :: ErrorMessage) (c :: Ordering) :: Bool where ... Source #

Equations

AcceptEq _ EQ = True 
AcceptEq msg _ = TypeError msg 

type family OrdBool (c :: Ordering) :: Bool where ... Source #

Equations

OrdBool EQ = True 
OrdBool _ = False 

type family And (b1 :: Bool) (b2 :: Bool) :: Bool where ... Source #

Equations

And True True = True 
And _ _ = False 

type family Or (b1 :: Bool) (b2 :: Bool) :: Bool where ... Source #

Equations

Or False False = False 
Or _ _ = True 

type family If (b1 :: Bool) (a :: k) (b :: k) :: k where ... Source #

Equations

If True a _ = a 
If False _ b = b 

type family Repeat (n :: Nat) (s :: Symbol) :: Symbol where ... Source #

Equations

Repeat 0 s = "" 
Repeat n s = AppendSymbol s (Repeat (n - 1) s) 

type family Fst (s :: (k, h)) :: k where ... Source #

Equations

Fst ((,) a _) = a 

type family Dupl (s :: k) :: (k, k) where ... Source #

Equations

Dupl a = (,) a a 

type family Concat (s :: [Symbol]) :: Symbol where ... Source #

>>> :kind! Concat (LDrop 6 (ToList "bool: \"r-ban:ff-ff\" | \"r-ban:ffff\""))
...
= "\"r-ban:ff-ff\" | \"r-ban:ffff\""

Since: 0.2.1.0

Equations

Concat '[] = "" 
Concat (x ': xs) = AppendSymbol x (Concat xs) 

type family Drop (n :: Nat) (s :: Symbol) :: Symbol where ... Source #

Equations

Drop n s = Concat (LDrop n (ToList s)) 

type family LDrop (n :: Nat) (s :: [k]) :: [k] where ... Source #

Since: 0.2.1.0

Equations

LDrop 0 s = s 
LDrop n '[] = '[] 
LDrop n (x ': xs) = LDrop (n - 1) xs 

type family Take (n :: Nat) (s :: Symbol) :: Symbol where ... Source #

>>> :kind! Take 3 "123456"
...
= "123"

Since: 0.2.1.0

Equations

Take n s = Concat (LTake n (ToList s)) 

type family LTake (n :: Nat) (s :: [k]) :: [k] where ... Source #

Since: 0.2.1.0

Equations

LTake 0 s = '[] 
LTake n '[] = '[] 
LTake n (x ': xs) = x ': LTake (n - 1) xs 

type family TakeUntil (s :: Symbol) (stop :: Symbol) :: Symbol where ... Source #

Equations

TakeUntil s stop = Concat (LTakeUntil (ToList s) stop) 

type family LTakeUntil (s :: [Symbol]) (stop :: Symbol) :: [Symbol] where ... Source #

Since: 0.2.1.0

Equations

LTakeUntil '[] _ = '[] 
LTakeUntil (x ': xs) stop = LTakeUntilHelper (x ': LTakeUntil xs stop) (CmpSymbol x stop) 

type family LTakeUntilHelper (s :: [Symbol]) (o :: Ordering) :: [Symbol] where ... Source #

Equations

LTakeUntilHelper '[] _ = '[] 
LTakeUntilHelper (x ': xs) EQ = '[] 
LTakeUntilHelper (x ': xs) _ = x ': xs 

type family Length (s :: Symbol) :: Nat where ... Source #

Since: 0.2.1.0

Equations

Length x = LLengh (ToList x) 

type family LLengh (s :: [k]) :: Nat where ... Source #

Since: 0.2.1.0

Equations

LLengh '[] = 0 
LLengh (x ': xs) = 1 + LLengh xs 

type family LLast (s :: [Symbol]) :: Symbol where ... Source #

>>> :kind! LLast '["1","2","3"]
...
= "3"

Since: 0.2.2.0

Equations

LLast '[] = TypeError (Text "Empty Symbol list not allowed") 
LLast '[x] = x 
LLast (_ ': xs) = LLast xs 

type family Snoc (s :: [k]) (t :: k) :: [k] where ... Source #

>>> :kind! Concat (Snoc '["1","2","3"] "4")
...
= "1234"

Since: 0.2.2.0

Equations

Snoc '[] x = '[x] 
Snoc (x ': xs) y = x ': Snoc xs y 

type family UnSnoc (s :: [k]) :: ([k], k) where ... Source #

:kind! UnSnoc '["1","2","3"] ... = '( (':) Symbol "1" ((':) Symbol "2" ('[] Symbol)), "3")

Since: 0.2.2.0

Equations

UnSnoc '[] = TypeError (Text "Empty list, no last element") 
UnSnoc '[x] = (,) '[] x 
UnSnoc (x ': xs) = UnSnocHelper x (UnSnoc xs) 

type family UnSnocHelper (s :: k) (t :: ([k], k)) :: ([k], k) where ... Source #

Equations

UnSnocHelper y ((,) xs x) = (,) (y ': xs) x