{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module Data.TypedEncoding.Common.Types.Decoding where
import Data.Proxy
import GHC.TypeLits
import Data.TypedEncoding.Common.Types.Enc
import Data.TypedEncoding.Common.Types.Common
data Decoding f (nm :: Symbol) (alg :: Symbol) conf str where
UnsafeMkDecoding :: Proxy nm -> (forall (xs :: [Symbol]) . Enc (nm ': xs) conf str -> f (Enc xs conf str)) -> Decoding f nm alg conf str
mkDecoding :: forall f (nm :: Symbol) conf str . (forall (xs :: [Symbol]) . Enc (nm ': xs) conf str -> f (Enc xs conf str)) -> Decoding f nm (AlgNm nm) conf str
mkDecoding = UnsafeMkDecoding Proxy
runDecoding :: forall alg nm f xs conf str . Decoding f nm alg conf str -> Enc (nm ': xs) conf str -> f (Enc xs conf str)
runDecoding (UnsafeMkDecoding _ fn) = fn
{-# DEPRECATED runDecoding "Use runDecoding'" #-}
runDecoding' :: forall alg nm f xs conf str . Decoding f nm alg conf str -> Enc (nm ': xs) conf str -> f (Enc xs conf str)
runDecoding' (UnsafeMkDecoding _ fn) = fn
_runDecoding :: forall nm f xs conf str alg . (AlgNm nm ~ alg) => Decoding f nm alg conf str -> Enc (nm ': xs) conf str -> f (Enc xs conf str)
_runDecoding = runDecoding @(AlgNm nm)
data Decodings f (nms :: [Symbol]) (algs :: [Symbol]) conf str where
ZeroD :: Decodings f '[] '[] conf str
ConsD :: Decoding f nm alg conf str -> Decodings f nms algs conf str -> Decodings f (nm ': nms) (alg ': algs) conf str
runDecodings :: forall algs nms f c str . (Monad f) => Decodings f nms algs c str -> Enc nms c str -> f (Enc ('[]::[Symbol]) c str)
runDecodings = runDecodings' @algs @nms
{-# DEPRECATED runDecodings "Use runDecodings'" #-}
runDecodings' :: forall algs nms f c str . (Monad f) => Decodings f nms algs c str -> Enc nms c str -> f (Enc ('[]::[Symbol]) c str)
runDecodings' ZeroD enc0 = pure enc0
runDecodings' (ConsD fn xs) enc =
let re :: f (Enc _ c str) = runDecoding fn enc
in re >>= runDecodings xs
_runDecodings :: forall nms f c str algs . (Monad f, algs ~ AlgNmMap nms) => Decodings f nms algs c str -> Enc nms c str -> f (Enc ('[]::[Symbol]) c str)
_runDecodings = runDecodings @(AlgNmMap nms)