{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Control.Static.Static where
import Data.Constraint (Dict (..))
import Data.Kind (Type)
import Data.Singletons.Prelude
import Data.Singletons.TH (genDefunSymbols)
import Data.Text (pack, unpack)
import Control.Static.Common
import Control.Static.Serialise
type SKey (k :: Symbol) = Sing k
data SKeyed k v = SKeyed !(SKey k) !v
deriving Functor
withSKeyedExt :: SKeyedExt g -> (forall (a :: Symbol) . SKeyed a g -> r) -> r
withSKeyedExt (SKeyedExt s a) f = withSomeSing (pack s) $ \k -> f (SKeyed k a)
toSKeyedExt :: RepVal g v k => SKeyed k v -> SKeyedExt g
toSKeyedExt (SKeyed k v) = SKeyedExt (unpack (fromSing k)) (toRep k v)
toSKeyedEither
:: Sing (k :: Symbol) -> Maybe (Either String v) -> Either SKeyedError v
toSKeyedEither k Nothing = Left $ SKeyedNotFound $ unpack $ fromSing k
toSKeyedEither _ (Just (Left e)) = Left $ SKeyedExtDecodeFailure e
toSKeyedEither _ (Just (Right v)) = Right v
skeyedCons
:: (c @@ k @@ v) => SKeyed k v -> TCTab c kk vv -> TCTab c (k ': kk) (v ': vv)
skeyedCons (SKeyed k v) = TCCons k v
type RepExtSym3 c g ext
= AndC2 c (FlipSym1 (TyCon2 (RepVal g) .@#@$$$ ApplySym1 ext))
type family TyContIX r ext (v :: Type) where
TyContIX r ext v = v -> ext @@ v -> r
genDefunSymbols [''TyContIX]
gwithStatic
:: forall c0 c1 f g ext (k :: Symbol) (kk :: [Symbol]) vv r
. TCTab (RepExtSym3 c0 g ext) kk vv
-> SKeyed k g
-> TCTab c1 kk (Fmap f vv)
-> ( forall k' v
. 'Just '(k', v) ~ LookupKV k kk vv
=> 'Just '(k', f @@ v) ~ Fmap (FmapSym1 f) (LookupKV k kk vv)
=> (c0 @@ k' @@ v)
=> (c1 @@ k' @@ (f @@ v))
=> Sing k'
-> (f @@ v)
-> v
-> (ext @@ v)
-> r
)
-> Either SKeyedError r
gwithStatic tab val@(SKeyed k ga) post go =
toSKeyedEither k $ case lookupTC2 @_ @_ @_ @f k tab post of
(TCNothing , TCNothing ) -> Nothing
(TCJust Dict k' v, TCJust Dict _ p) -> Just $ go k' p v <$> fromRep k' ga
withStaticCts
:: forall c0 c1 g ext (k :: Symbol) (kk :: [Symbol]) vv r
. TCTab (RepExtSym3 c0 g ext) kk vv
-> SKeyed k g
-> TCTab c1 kk (Fmap (TyContIXSym2 r ext) vv)
-> Either SKeyedError r
withStaticCts tab val post =
gwithStatic @_ @_ @(TyContIXSym2 r ext) tab val post (flip const)
withSomeStaticCts
:: forall c0 c1 g ext (kk :: [Symbol]) vv r
. TCTab (RepExtSym3 c0 g ext) kk vv
-> SKeyedExt g
-> TCTab c1 kk (Fmap (TyContIXSym2 r ext) vv)
-> Either SKeyedError r
withSomeStaticCts tab ext post =
withSKeyedExt ext $ \(val :: SKeyed k g) -> withStaticCts tab val post
withStaticCxt
:: forall c f g ext (k :: Symbol) (kk :: [Symbol]) vv r
. TCTab (RepExtSym3 c g ext) kk vv
-> SKeyed k g
-> ( forall k' v
. 'Just '(k', v) ~ LookupKV k kk vv
=> ProofLookupKV f k kk vv
=> (c @@ k' @@ v) => Sing k' -> v -> (ext @@ v) -> r
)
-> Either SKeyedError r
withStaticCxt tab val@(SKeyed k ga) go =
toSKeyedEither k $ case lookupTC @_ @_ @f k tab of
(TCNothing , _ ) -> Nothing
(TCJust Dict k' v, Dict) -> Just $ go k' v <$> fromRep k' ga
withSomeStaticCxt
:: forall c f g ext (kk :: [Symbol]) vv r
. TCTab (RepExtSym3 c g ext) kk vv
-> SKeyedExt g
-> ( forall k k' v
. 'Just '(k', v) ~ LookupKV k kk vv
=> ProofLookupKV f k kk vv
=> (c @@ k' @@ v) => Sing k' -> v -> (ext @@ v) -> r
)
-> Either SKeyedError r
withSomeStaticCxt tab ext go =
withSKeyedExt ext $ \(val :: SKeyed k g) -> withStaticCxt @_ @f tab val (go @k)