{-# 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 = _mkDecoding
{-# DEPRECATED mkDecoding "Use _mkDecoding" #-}
_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 nm f xs conf str . Decoding f nm nm conf str -> Enc (nm ': xs) conf str -> f (Enc xs conf str)
runDecoding (UnsafeMkDecoding _ fn) = fn
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 nms f c str . (Monad f) => Decodings f nms nms c str -> Enc nms c str -> f (Enc ('[]::[Symbol]) c str)
runDecodings = runDecodings' @nms @nms
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)