{-# 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.Validation where
import Data.Proxy
import GHC.TypeLits
import Data.TypedEncoding.Common.Types.Enc
import Data.TypedEncoding.Common.Types.Common
data Validation f (nm :: Symbol) (alg :: Symbol) conf str where
UnsafeMkValidation :: Proxy nm -> (forall (xs :: [Symbol]) . Enc (nm ': xs) conf str -> f (Enc xs conf str)) -> Validation f nm alg conf str
mkValidation :: forall f (nm :: Symbol) conf str . (forall (xs :: [Symbol]) . Enc (nm ': xs) conf str -> f (Enc xs conf str)) -> Validation f nm (AlgNm nm) conf str
mkValidation = UnsafeMkValidation Proxy
{-# DEPRECATED mkValidation "Use _mkValidation" #-}
_mkValidation :: forall f (nm :: Symbol) conf str . (forall (xs :: [Symbol]) . Enc (nm ': xs) conf str -> f (Enc xs conf str)) -> Validation f nm (AlgNm nm) conf str
_mkValidation = UnsafeMkValidation Proxy
runValidation :: forall nm f xs conf str . Validation f nm nm conf str -> Enc (nm ': xs) conf str -> f (Enc xs conf str)
runValidation (UnsafeMkValidation _ fn) = fn
runValidation' :: forall alg nm f xs conf str . Validation f nm alg conf str -> Enc (nm ': xs) conf str -> f (Enc xs conf str)
runValidation' (UnsafeMkValidation _ fn) = fn
_runValidation :: forall nm f xs conf str alg . (AlgNm nm ~ alg) => Validation f nm alg conf str -> Enc (nm ': xs) conf str -> f (Enc xs conf str)
_runValidation = runValidation' @(AlgNm nm)
data Validations f (nms :: [Symbol]) (algs :: [Symbol]) conf str where
ZeroV :: Validations f '[] '[] conf str
ConsV :: Validation f nm alg conf str -> Validations f nms algs conf str -> Validations f (nm ': nms) (alg ': algs) conf str
runValidationChecks' :: forall algs nms f c str . (Monad f) => Validations f nms algs c str -> Enc nms c str -> f (Enc ('[]::[Symbol]) c str)
runValidationChecks' ZeroV enc0 = pure enc0
runValidationChecks' (ConsV fn xs) enc =
let re :: f (Enc _ c str) = runValidation' fn enc
in re >>= runValidationChecks' xs