Data.TypedEncoding.Instances.Restriction.Bool

Boolean algebra on encodings

(Experimental, early alpha development stage) This module was not converted to v0.3 style yet.

Grammar

Simple grammar requires boolean terms to be included in parentheses

bool[BinaryOp]:(leftTerm)(rightTerm)
bool[UnaryOp]:(term)

Expected behavior is described next to the corresponding combinator.

Since: 0.2.2.0

Documentation

>>> :set -XOverloadedStrings -XMultiParamTypeClasses -XDataKinds -XTypeApplications
>>> import qualified Data.Text as T
>>> import           Data.TypedEncoding.Instances.Restriction.Misc()

encBoolOrLeft :: forall f s t xs c str. (BoolOpIs s "or" ~ True, Functor f, LeftTerm s ~ t) => (Enc xs c str -> f (Enc (t ': xs) c str)) -> Enc xs c str -> f (Enc (s ': xs) c str)

See examples in encBoolOrRight'

encBoolOrLeft' :: forall f s t xs c str. (BoolOpIs s "or" ~ True, Functor f, LeftTerm s ~ t, Encode f t t c str) => Enc xs c str -> f (Enc (s ': xs) c str)

See examples in encBoolOrRight'

encBoolOrLeft'' :: forall alg f s t xs c str. (BoolOpIs s "or" ~ True, Functor f, LeftTerm s ~ t, Encode f t alg c str) => Enc xs c str -> f (Enc (s ': xs) c str)

encBoolOrRight :: forall f s t xs c str. (BoolOpIs s "or" ~ True, Functor f, RightTerm s ~ t) => (Enc xs c str -> f (Enc (t ': xs) c str)) -> Enc xs c str -> f (Enc (s ': xs) c str)

encBoolOrRight' :: forall f s t xs c str. (BoolOpIs s "or" ~ True, Functor f, RightTerm s ~ t, Encode f t t c str) => Enc xs c str -> f (Enc (s ': xs) c str)

>>> :{
let tst1, tst2, tst3 :: Either EncodeEx (Enc '["boolOr:(r-Word8-decimal)(r-Int-decimal)"] () T.Text)
    tst1 = encBoolOrLeft' . toEncoding () $ "212" 
    tst2 = encBoolOrRight' . toEncoding () $ "1000000" 
    tst3 = encBoolOrLeft' . toEncoding () $ "1000000"
:}

>>> tst1
Right (UnsafeMkEnc Proxy () "212")

>>> tst2
Right (UnsafeMkEnc Proxy () "1000000")

>>> tst3
Left (EncodeEx "r-Word8-decimal" ("Payload does not satisfy format Word8-decimal: 1000000"))

encBoolOrRight'' :: forall alg f s t xs c str. (BoolOpIs s "or" ~ True, Functor f, RightTerm s ~ t, Encode f t alg c str) => Enc xs c str -> f (Enc (s ': xs) c str)

encBoolAnd :: forall f s t1 t2 xs c str. (BoolOpIs s "and" ~ True, KnownSymbol s, f ~ Either EncodeEx, Eq str, LeftTerm s ~ t1, RightTerm s ~ t2) => (Enc xs c str -> f (Enc (t1 ': xs) c str)) -> (Enc xs c str -> f (Enc (t2 ': xs) c str)) -> Enc xs c str -> f (Enc (s ': xs) c str)

encBoolAnd' :: forall s t1 t2 xs c str. (BoolOpIs s "and" ~ True, KnownSymbol s, Eq str, LeftTerm s ~ t1, RightTerm s ~ t2, Encode (Either EncodeEx) t1 t1 c str, Encode (Either EncodeEx) t2 t2 c str) => Enc xs c str -> Either EncodeEx (Enc (s ': xs) c str)

"boolOr:(enc1)(enc2)" contains strings that encode the same way under both encodings. for example "boolOr:(r-UPPER)(r-lower)" valid elements would include "123-34" but not "abc"

>>> :{
let tst1, tst2 :: Either EncodeEx (Enc '["boolAnd:(r-Word8-decimal)(r-Int-decimal)"] () T.Text)
    tst1 = encBoolAnd' . toEncoding () $ "234"
    tst2 = encBoolAnd' . toEncoding () $ "100000"
:}

>>> tst1
Right (UnsafeMkEnc Proxy () "234")
>>> tst2
Left (EncodeEx "r-Word8-decimal" ("Payload does not satisfy format Word8-decimal: 100000"))

encBoolAnd'' :: forall al1 al2 s t1 t2 xs c str. (BoolOpIs s "and" ~ True, KnownSymbol s, Eq str, LeftTerm s ~ t1, RightTerm s ~ t2, Encode (Either EncodeEx) t1 al1 c str, Encode (Either EncodeEx) t2 al2 c str) => Enc xs c str -> Either EncodeEx (Enc (s ': xs) c str)

encBoolNot :: forall s t xs c str. (BoolOpIs s "not" ~ True, KnownSymbol s, FirstTerm s ~ t, Restriction t) => (Enc xs c str -> Either EncodeEx (Enc (t ': xs) c str)) -> Enc xs c str -> Either EncodeEx (Enc (s ': xs) c str)

encBoolNot' :: forall s t xs c str. (BoolOpIs s "not" ~ True, KnownSymbol s, FirstTerm s ~ t, KnownSymbol t, Restriction t, Encode (Either EncodeEx) t t c str) => Enc xs c str -> Either EncodeEx (Enc (s ': xs) c str)

>>> :{
let tst1, tst2 :: Either EncodeEx (Enc '["boolNot:(r-Word8-decimal)"] () T.Text)
    tst1 = encBoolNot' . toEncoding () $ "334"
    tst2 = encBoolNot' . toEncoding () $ "127"
:}

>>> tst1
Right (UnsafeMkEnc Proxy () "334")
>>> tst2
Left (EncodeEx "boolNot:(r-Word8-decimal)" ("Encoding r-Word8-decimal succeeded"))

encBoolNot'' :: forall alg s t xs c str. (BoolOpIs s "not" ~ True, KnownSymbol s, FirstTerm s ~ t, Restriction t, Encode (Either EncodeEx) t alg c str) => Enc xs c str -> Either EncodeEx (Enc (s ': xs) c str)

decBoolR :: forall f xs t s c str. (NestedR s ~ True, Applicative f) => Enc (s ': xs) c str -> f (Enc xs c str)

Decodes boolean expression if all leaves are "r-"

recWithEncBoolR :: forall (s :: Symbol) xs c str. NestedR s ~ True => (Enc xs c str -> Either EncodeEx (Enc (s ': xs) c str)) -> Enc xs c str -> Either RecreateEx (Enc (s ': xs) c str)

unsafeRecWithEncR :: forall (s :: Symbol) xs c str. (Enc xs c str -> Either EncodeEx (Enc (s ': xs) c str)) -> Enc xs c str -> Either RecreateEx (Enc (s ': xs) c str)

Type family based parser

type family BoolOpIs (s :: Symbol) (op :: Symbol) :: Bool where ...

>>> :kind! BoolOpIs "boolAnd:(someenc)(otherenc)" "and"
...
= 'True

Equations

BoolOpIs s op = AcceptEq (Text "Invalid bool encoding " :<>: ShowType s) (CmpSymbol (BoolOp s) op)

type family BoolOp (s :: Symbol) :: Symbol where ...

This works fast with !kind but is much slower in declaration :kind! BoolOp "boolOr:()()"

Equations

BoolOp s = Fst (BoolOpHelper (Dupl s))

type family BoolOpHelper (x :: (Symbol, Symbol)) :: (Symbol, Bool) where ...

Equations

BoolOpHelper ((,) s1 s2) = (,) (ToLower (TakeUntil (Drop 4 s1) ":")) (AcceptEq (Text "Invalid bool encoding " :<>: ShowType s2) (CmpSymbol "bool" (Take 4 s2)))

type family IsBool (s :: Symbol) :: Bool where ...

Equations

IsBool s = AcceptEq (Text "Not boolean encoding " :<>: ShowType s) (CmpSymbol "bool" (Take 4 s))

type family NestedR (s :: Symbol) :: Bool where ...

>>> :kind! NestedR "boolOr:(r-abc)(r-cd)"
...
= 'True

>>> :kind! NestedR "boolOr:(boolAnd:(r-ab)(r-ac))(boolNot:(r-cd))"
...
= 'True

>>> :kind! NestedR "boolOr:(boolAnd:(r-ab)(ac))(boolNot:(r-cd))"
...
... (TypeError ...)
...

Equations

NestedR "" = True

NestedR s = Or (IsROrEmpty s) (And (IsBool s) (And (NestedR (LeftTerm s)) (NestedR (RightTerm s))))

type family FirstTerm (s :: Symbol) :: Symbol where ...

Equations

FirstTerm s = LeftTerm s

type family SecondTerm (s :: Symbol) :: Symbol where ...

returns "" for unary operator

Equations

SecondTerm s = RightTerm s

type family LeftTerm (s :: Symbol) :: Symbol where ...

>>> :kind! LeftTerm "boolSomeOp:(agag)(222)"
...
= "agag"

>>> :kind! LeftTerm "r-Int-decimal"
...
= ""

Equations

LeftTerm s = Concat (LDropLast (LTakeFstParen (LParenCnt (ToList s))))

type family RightTerm (s :: Symbol) :: Symbol where ...

>>> :kind! RightTerm "boolSomeOp:(agag)(222)"
...
= "222"

>>> :kind! RightTerm "r-Int-decimal"
...
= ""

Equations

RightTerm s = Concat (LDropLast (LTakeSndParen 0 (LParenCnt (ToList s))))

type family LDropLast (s :: [Symbol]) :: [Symbol] where ...

Equations

LDropLast '[] = '[]

LDropLast '[x] = '[]

LDropLast (x ': xs) = x ': LDropLast xs

type family LParenCnt (s :: [Symbol]) :: [(Symbol, Nat)] where ...

Equations

LParenCnt '[] = '[]

LParenCnt ("(" ': xs) = LParenCntHelper ((,) "(" Decr) (LParenCnt xs)

LParenCnt (")" ': xs) = LParenCntHelper ((,) ")" Incr) (LParenCnt xs)

LParenCnt (x ': xs) = LParenCntHelper ((,) x NoChng) (LParenCnt xs)

data Adjust

Constructors

Incr

Decr

NoChng

type family AdjHelper (a :: Adjust) (n :: Nat) :: Nat where ...

Equations

AdjHelper Incr n = n + 1

AdjHelper Decr 0 = 0

AdjHelper Decr n = n - 1

AdjHelper NoChng n = n

type family LParenCntHelper (s :: (Symbol, Adjust)) (sx :: [(Symbol, Nat)]) :: [(Symbol, Nat)] where ...

Equations

LParenCntHelper ((,) x k) '[] = (,) x (AdjHelper k 0) ': '[]

LParenCntHelper ((,) x k) ((,) c i ': xs) = (,) x (AdjHelper k i) ': ((,) c i ': xs)

type family LTakeFstParen (si :: [(Symbol, Nat)]) :: [Symbol] where ...

Equations

LTakeFstParen '[] = '[]

LTakeFstParen ((,) _ 0 ': xs) = LTakeFstParen xs

LTakeFstParen ((,) ")" 1 ': _) = '[")"]

LTakeFstParen ((,) a p ': xs) = a ': LTakeFstParen xs

type family LTakeSndParen (n :: Nat) (si :: [(Symbol, Nat)]) :: [Symbol] where ...

Equations

LTakeSndParen _ '[] = '[]

LTakeSndParen 0 ((,) ")" 1 ': xs) = LTakeSndParen 1 xs

LTakeSndParen 1 ((,) _ 0 ': xs) = LTakeSndParen 1 xs

LTakeSndParen 0 ((,) _ _ ': xs) = LTakeSndParen 0 xs

LTakeSndParen 1 ((,) a _ ': xs) = a ': LTakeSndParen 1 xs

LTakeSndParen n _ = '[]