{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
module Data.TypedEncoding.Combinators.Common where
import Data.TypedEncoding.Common.Types
import Data.TypedEncoding.Combinators.Unsafe
import Data.TypedEncoding.Common.Util.TypeLits (Append)
import GHC.TypeLits
import Data.Proxy
aboveF :: forall (ts :: [Symbol]) xs ys f c str . (Functor f) =>
(Enc xs c str -> f (Enc ys c str))
-> Enc (Append xs ts) c str -> f (Enc (Append ys ts) c str)
aboveF :: (Enc @[Symbol] xs c str -> f (Enc @[Symbol] ys c str))
-> Enc @[Symbol] (Append @Symbol xs ts) c str
-> f (Enc @[Symbol] (Append @Symbol ys ts) c str)
aboveF Enc @[Symbol] xs c str -> f (Enc @[Symbol] ys c str)
fn (UnsafeMkEnc Proxy @[Symbol] (Append @Symbol xs ts)
_ c
conf str
str) =
let f (Enc @[Symbol] ys c str)
re :: f (Enc ys c str) = Enc @[Symbol] xs c str -> f (Enc @[Symbol] ys c str)
fn (Enc @[Symbol] xs c str -> f (Enc @[Symbol] ys c str))
-> Enc @[Symbol] xs c str -> f (Enc @[Symbol] ys c str)
forall a b. (a -> b) -> a -> b
$ Proxy @[Symbol] xs -> c -> str -> Enc @[Symbol] xs c str
forall k (nms :: k) conf str.
Proxy @k nms -> conf -> str -> Enc @k nms conf str
UnsafeMkEnc Proxy @[Symbol] xs
forall k (t :: k). Proxy @k t
Proxy c
conf str
str
in Proxy @[Symbol] (Append @Symbol ys ts)
-> c -> str -> Enc @[Symbol] (Append @Symbol ys ts) c str
forall k (nms :: k) conf str.
Proxy @k nms -> conf -> str -> Enc @k nms conf str
UnsafeMkEnc Proxy @[Symbol] (Append @Symbol ys ts)
forall k (t :: k). Proxy @k t
Proxy c
conf (str -> Enc @[Symbol] (Append @Symbol ys ts) c str)
-> (Enc @[Symbol] ys c str -> str)
-> Enc @[Symbol] ys c str
-> Enc @[Symbol] (Append @Symbol ys ts) c str
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Enc @[Symbol] ys c str -> str
forall k (enc :: k) conf str. Enc @k enc conf str -> str
getPayload (Enc @[Symbol] ys c str
-> Enc @[Symbol] (Append @Symbol ys ts) c str)
-> f (Enc @[Symbol] ys c str)
-> f (Enc @[Symbol] (Append @Symbol ys ts) c str)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Enc @[Symbol] ys c str)
re
above :: forall (ts :: [Symbol]) xs ys c str .
(Enc xs c str -> Enc ys c str)
-> Enc (Append xs ts) c str -> Enc (Append ys ts) c str
above :: (Enc @[Symbol] xs c str -> Enc @[Symbol] ys c str)
-> Enc @[Symbol] (Append @Symbol xs ts) c str
-> Enc @[Symbol] (Append @Symbol ys ts) c str
above Enc @[Symbol] xs c str -> Enc @[Symbol] ys c str
fn (UnsafeMkEnc Proxy @[Symbol] (Append @Symbol xs ts)
_ c
conf str
str) =
let Enc @[Symbol] ys c str
re ::Enc ys c str = Enc @[Symbol] xs c str -> Enc @[Symbol] ys c str
fn (Enc @[Symbol] xs c str -> Enc @[Symbol] ys c str)
-> Enc @[Symbol] xs c str -> Enc @[Symbol] ys c str
forall a b. (a -> b) -> a -> b
$ Proxy @[Symbol] xs -> c -> str -> Enc @[Symbol] xs c str
forall k (nms :: k) conf str.
Proxy @k nms -> conf -> str -> Enc @k nms conf str
UnsafeMkEnc Proxy @[Symbol] xs
forall k (t :: k). Proxy @k t
Proxy c
conf str
str
in Proxy @[Symbol] (Append @Symbol ys ts)
-> c -> str -> Enc @[Symbol] (Append @Symbol ys ts) c str
forall k (nms :: k) conf str.
Proxy @k nms -> conf -> str -> Enc @k nms conf str
UnsafeMkEnc Proxy @[Symbol] (Append @Symbol ys ts)
forall k (t :: k). Proxy @k t
Proxy c
conf (str -> Enc @[Symbol] (Append @Symbol ys ts) c str)
-> (Enc @[Symbol] ys c str -> str)
-> Enc @[Symbol] ys c str
-> Enc @[Symbol] (Append @Symbol ys ts) c str
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Enc @[Symbol] ys c str -> str
forall k (enc :: k) conf str. Enc @k enc conf str -> str
getPayload (Enc @[Symbol] ys c str
-> Enc @[Symbol] (Append @Symbol ys ts) c str)
-> Enc @[Symbol] ys c str
-> Enc @[Symbol] (Append @Symbol ys ts) c str
forall a b. (a -> b) -> a -> b
$ Enc @[Symbol] ys c str
re
getTransformF :: forall e1 e2 f c s1 s2 . Functor f => (Enc e1 c s1 -> f (Enc e2 c s2)) -> c -> s1 -> f s2
getTransformF :: (Enc @k e1 c s1 -> f (Enc @k e2 c s2)) -> c -> s1 -> f s2
getTransformF Enc @k e1 c s1 -> f (Enc @k e2 c s2)
fn c
c s1
str = Enc @k e2 c s2 -> s2
forall k (enc :: k) conf str. Enc @k enc conf str -> str
getPayload (Enc @k e2 c s2 -> s2) -> f (Enc @k e2 c s2) -> f s2
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Enc @k e1 c s1 -> f (Enc @k e2 c s2)
fn (c -> s1 -> Enc @k e1 c s1
forall k conf str (enc :: k). conf -> str -> Enc @k enc conf str
unsafeSetPayload c
c s1
str)