{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Data.TypedEncoding.Common.Types.UncheckedEnc where
import Data.Proxy
import Data.TypedEncoding.Common.Class.Util
import Data.TypedEncoding.Common.Types.Common
data UncheckedEnc c str = MkUncheckedEnc [EncAnn] c str deriving (Show, Eq)
toUncheckedEnc :: [EncAnn] -> c -> str -> UncheckedEnc c str
toUncheckedEnc = MkUncheckedEnc
getUncheckedEncAnn :: UncheckedEnc c str -> [EncAnn]
getUncheckedEncAnn (MkUncheckedEnc ann _ _) = ann
verifyAnn :: forall xs c str . SymbolList xs => UncheckedEnc c str -> Either String (UncheckedEnc c str)
verifyAnn x@(MkUncheckedEnc xs _ _) =
let p = Proxy :: Proxy xs
in if symbolVals @ xs == xs
then Right x
else Left $ "UncheckedEnc has not matching annotation " ++ displ xs
instance (Show c, Displ str) => Displ (UncheckedEnc c str) where
displ (MkUncheckedEnc xs c s) =
"MkUncheckedEnc " ++ displ xs ++ " " ++ show c ++ " " ++ displ s