module Blanks.Interface
( Blank
, BlankLeft
, BlankRight
, BlankInfo
, BlankFunctor
, BlankRawFold
, BlankFold
, BlankPair
, blankFree
, blankEmbed
, blankAbstract
, blankAbstract1
, blankUnAbstract
, blankUnAbstract1
, blankInstantiate
, blankInstantiate1
, blankApply
, blankApply1
, blankApplyThrow
, blankApply1Throw
, blankBind
, blankBindOpt
, blankLift
, blankRawFold
, blankFold
, blankLiftAnno
, blankHoistAnno
, blankMapAnno
) where
import Blanks.NatNewtype (NatNewtype)
import Blanks.ScopeW
import Blanks.Sub (SubError, ThrowSub, rethrowSub)
import Blanks.UnderScope (UnderScopeFold)
import Data.Functor.Adjunction (Adjunction)
import Data.Kind (Type)
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
type family BlankLeft (g :: Type -> Type) :: Type -> Type
type family BlankRight (g :: Type -> Type) :: Type -> Type
type family BlankInfo (g :: Type -> Type) :: Type
type family BlankFunctor (g :: Type -> Type) :: Type -> Type
type BlankRawFold (g :: Type -> Type) (a :: Type) (r :: Type) = UnderScopeFold (BlankInfo g) (BlankFunctor g) (g a) a r
type BlankFold (g :: Type -> Type) (a :: Type) (r :: Type) = BlankRawFold g a (BlankRight g r)
class
( Adjunction (BlankLeft g) (BlankRight g)
, Applicative (BlankRight g)
, Functor (BlankFunctor g)
, NatNewtype (ScopeW (BlankLeft g) (BlankInfo g) (BlankFunctor g) g) g
) => Blank (g :: Type -> Type)
type BlankPair g h = (Blank g, Blank h, BlankInfo g ~ BlankInfo h, BlankFunctor g ~ BlankFunctor h)
blankFree ::
Blank g
=> a
-> BlankRight g (g a)
blankFree = scopeWFree
{-# INLINE blankFree #-}
blankEmbed ::
Blank g
=> BlankFunctor g (g a)
-> BlankRight g (g a)
blankEmbed = scopeWEmbed
{-# INLINE blankEmbed #-}
blankAbstract ::
(Blank g, Eq a)
=> BlankInfo g
-> Seq a
-> g a
-> BlankRight g (g a)
blankAbstract = scopeWAbstract
{-# INLINE blankAbstract #-}
blankAbstract1 :: (Blank g, Eq a) => BlankInfo g -> a -> g a -> BlankRight g (g a)
blankAbstract1 n k = scopeWAbstract n (Seq.singleton k)
{-# INLINE blankAbstract1 #-}
blankUnAbstract ::
Blank g
=> Seq a
-> g a
-> g a
blankUnAbstract = scopeWUnAbstract
{-# INLINE blankUnAbstract #-}
blankUnAbstract1 :: Blank g => a -> g a -> g a
blankUnAbstract1 = scopeWUnAbstract . Seq.singleton
{-# INLINE blankUnAbstract1 #-}
blankInstantiate ::
Blank g
=> Seq (BlankRight g (g a))
-> g a
-> g a
blankInstantiate = scopeWInstantiate
{-# INLINE blankInstantiate #-}
blankInstantiate1 :: Blank g => BlankRight g (g a) -> g a -> g a
blankInstantiate1 = scopeWInstantiate . Seq.singleton
{-# INLINE blankInstantiate1 #-}
blankApply ::
Blank g
=> Seq (BlankRight g (g a))
-> g a
-> Either SubError (g a)
blankApply = scopeWApply
{-# INLINE blankApply #-}
blankApply1 :: Blank g => BlankRight g (g a) -> g a -> Either SubError (g a)
blankApply1 = scopeWApply . Seq.singleton
{-# INLINE blankApply1 #-}
blankApplyThrow :: (Blank g, ThrowSub m, Applicative m) => Seq (BlankRight g (g a)) -> g a -> m (g a)
blankApplyThrow ks = rethrowSub . scopeWApply ks
{-# INLINE blankApplyThrow #-}
blankApply1Throw :: (Blank g, ThrowSub m, Applicative m) => BlankRight g (g a) -> g a -> m (g a)
blankApply1Throw k = rethrowSub . scopeWApply (Seq.singleton k)
{-# INLINE blankApply1Throw #-}
blankBind :: Blank g => (a -> BlankRight g (g b)) -> g a -> g b
blankBind = scopeWBind
{-# INLINE blankBind #-}
blankBindOpt :: Blank g => (a -> Maybe (BlankRight g (g a))) -> g a -> g a
blankBindOpt = scopeWBindOpt
{-# INLINE blankBindOpt #-}
blankLift :: (Blank g, Monad (BlankRight g), Traversable (BlankFunctor g)) => BlankFunctor g a -> BlankRight g (g a)
blankLift = scopeWLift
{-# INLINE blankLift #-}
blankRawFold :: Blank g => BlankRawFold g a r -> g a -> BlankLeft g r
blankRawFold = scopeWRawFold
{-# INLINE blankRawFold #-}
blankFold :: Blank g => BlankFold g a r -> g a -> r
blankFold = scopeWFold
{-# INLINE blankFold #-}
blankLiftAnno :: Blank g => BlankLeft g a -> g a
blankLiftAnno = scopeWLiftAnno
{-# INLINE blankLiftAnno #-}
blankHoistAnno :: BlankPair g h => (forall x. BlankLeft g x -> BlankLeft h x) -> g a -> h a
blankHoistAnno = scopeWHoistAnno
{-# INLINE blankHoistAnno #-}
blankMapAnno :: Blank g => (BlankLeft g a -> BlankLeft g b) -> g a -> g b
blankMapAnno = scopeWMapAnno
{-# INLINE blankMapAnno #-}