module Homoiconic.Constrained
(
FAlgebra (..)
, AST
, runAST
, Tag
, AppTag
, AppTags
, ConsTag
, Free (..)
, FreeConstraints
, MkFree (..)
, View (..)
, Var
, var1
, var2
, var3
, mkFAlgebra
, mkTag
, mkTagFromCnst
, unsafeExtractSigTag0
, unsafeExtractSigTag
, unsafeCoerceSigTag
, runSig1Snoc
, runSig0Snoc
, embedSigTag
, Snoc
, Proxy (..)
, Typeable
, Constraint
)
where
import Homoiconic.Common.Tags
import Homoiconic.Constrained.TH
import Prelude
import Control.Monad
import Data.Foldable
import Data.List
import Data.Maybe
import Data.Typeable
import Data.Proxy
import Data.Kind
import GHC.Exts hiding (IsList(..))
import Unsafe.Coerce
class Typeable alg => FAlgebra (alg::Type->Constraint) where
data Sig alg (t::[Tag]) a
runSig1 :: alg a => proxy a -> Sig alg (s ': t) (AppTags t a) -> AppTags (s ': t) a
runSig0 :: alg a => proxy a -> Sig alg t (AppTags t a) -> AppTags t a
mapRun :: (FreeConstraints t' a)
=> (forall s. Free (Sig alg') s a -> AppTags s a)
-> Sig alg t (Free (Sig alg') t' a)
-> Sig alg t (AppTags t' a)
type AST (alg::Type->Constraint) t a = Free (Sig alg) t a
runAST :: forall alg t a.
( FAlgebra alg
, alg a
) => Free (Sig alg) t a -> AppTags t a
runAST (Pure a) = a
runAST (Free0 s) = runSig0 (Proxy::Proxy a) $ mapRun runAST s
runAST (Free1 s) = runSig1 (Proxy::Proxy a) $ mapRun runAST s
class (FAlgebra alg1, FAlgebra alg2) => View alg1 t1 alg2 t2 where
embedSig :: Sig alg1 t1 a -> Sig alg2 t2 a
unsafeExtractSig :: Sig alg2 t2 a -> Sig alg1 t1 a
embedSigTag :: View alg1 (t ': t1) alg2 (t ': t2) => Sig alg1 (t ': t1) a -> Sig alg2 (t ': t2) a
embedSigTag = embedSig
unsafeExtractSigTag ::
( View alg1 '[s] alg2 (s:t)
) => Sig alg2 (s ': t) (Free (Sig alg2) t a) -> Sig alg1 '[s] (Free (Sig alg2) t a)
unsafeExtractSigTag = unsafeExtractSig
unsafeExtractSigTag0 ::
( View alg1 '[] alg2 t
) => Sig alg2 t (Free (Sig alg2) t a) -> Sig alg1 '[] (Free (Sig alg2) t a)
unsafeExtractSigTag0 = unsafeExtractSig
instance FAlgebra alg => View alg t alg t where
embedSig = id
unsafeExtractSig = id
type family ConsTag (t::Tag) (ts::[Tag]) :: [Tag]
class MkFree s (t::[Tag]) a where
mkFree :: proxy s -> f (ConsTag s t) (Free f t a) -> Free f (ConsTag s t) a
data Free (f::[Tag]->Type->Type) (t::[Tag]) (a::Type) where
Free1 :: FreeConstraints t a => f (s ': t) (Free f t a) -> Free f (s ': t) a
Free0 :: FreeConstraints t a => f t (Free f t a) -> Free f t a
Pure :: AppTags t a -> Free f t a
type family FreeConstraints (t::[Tag]) (a::Type) :: Constraint
instance
( Show (AppTags t a)
, Show (f t (Free f t a))
, ShowUntag (f t (Free f t a))
) => Show (Free f t a)
where
show (Free1 f) = "("++show f++")"
show (Free0 f) = "("++show f++")"
show (Pure a) = show a
type family ShowUntag (f::Type) :: Constraint where
ShowUntag (f (s ': t) (Free f (s ': t) a)) = Show (f (s ': t) (Free f t a))
ShowUntag a = ()
newtype Var = Var String
deriving (Eq)
instance Show Var where
show (Var v) = v
var1 :: AppTags t Var~Var => AST alg t Var
var1 = Pure $ Var "var1"
var2 :: AppTags t Var~Var => AST alg t Var
var2 = Pure $ Var "var2"
var3 :: AppTags t Var~Var => AST alg t Var
var3 = Pure $ Var "var3"
runSig0Snoc :: forall proxy alg a t u.
( FAlgebra alg
, alg (AppTag u a)
) => Proxy u
-> Proxy a
-> Sig alg t (AppTags (t `Snoc` u) a)
-> AppTags (t `Snoc` u) a
runSig0Snoc ps pa u
= coerce_AppTags_Snoc pt ps pa $ runSig0 (Proxy::Proxy (AppTag u a)) $ coerce_AppTags_Snoc_f pt ps pa u
where
pt = Proxy :: Proxy t
type family Init (xs::[a]) where
Init (x ': '[]) = '[]
Init (x ': xs ) = x ': Init xs
runSig1Snoc :: forall proxy alg a s ttt t u.
( FAlgebra alg
, alg (AppTag u a)
) => Proxy (u::Tag)
-> Proxy (s::Tag)
-> Proxy (t::[Tag])
-> Proxy a
-> Sig alg ttt (AppTags t a)
-> AppTag s (AppTags t a)
runSig1Snoc pu ps pt pa s
= unsafeCoerce $ runSig1
(Proxy::Proxy (AppTag u a))
(unsafeCoerce s :: Sig alg (s ': Init t) (AppTags (Init t) (AppTag u a)))
unsafeCoerceSigTag :: proxy t' -> Sig alg t a -> Sig alg t' a
unsafeCoerceSigTag _ = unsafeCoerce
data HaskTag a b where
HaskTag ::
( forall (s::[Tag]). ()
=> Proxy s
-> Proxy a
-> Proxy b
-> AppTags s a
-> AppTags s b
) -> HaskTag a b
apHaskTag :: forall t a b . Proxy (t::[Tag]) -> HaskTag a b -> AppTags t a -> AppTags t b
apHaskTag pt (HaskTag f) = f pt (Proxy::Proxy a) (Proxy::Proxy b)
class FunctorTag (f::[Tag]->Type->Type) where
fmapTag :: HaskTag a b -> f t a -> f t b