{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module PlutusCore.Builtin.KnownTypeAst
( TyNameRep (..)
, TyVarRep
, TyAppRep
, TyForallRep
, Hole
, RepHole
, TypeHole
, KnownBuiltinTypeAst
, KnownTypeAst (..)
, Merge
) where
import PlutusCore.Builtin.Emitter
import PlutusCore.Builtin.KnownKind
import PlutusCore.Builtin.Polymorphism
import PlutusCore.Core
import PlutusCore.Evaluation.Result
import PlutusCore.MkPlc hiding (error)
import PlutusCore.Name
import Data.Kind qualified as GHC (Constraint, Type)
import Data.Proxy
import Data.Some.GADT qualified as GADT
import Data.Text qualified as Text
import GHC.TypeLits
import Universe
data Hole
type RepHole :: forall a hole. a -> hole
data family RepHole x
type TypeHole :: forall hole. GHC.Type -> hole
data family TypeHole a
type BuiltinHead :: forall k. k -> k
data family BuiltinHead f
type ElaborateBuiltin :: forall k. k -> k
type family ElaborateBuiltin a where
ElaborateBuiltin (f x) = ElaborateBuiltin f `TyAppRep` x
ElaborateBuiltin f = BuiltinHead f
type KnownBuiltinTypeAst uni a = KnownTypeAst uni (ElaborateBuiltin a)
type KnownTypeAst :: forall a. (GHC.Type -> GHC.Type) -> a -> GHC.Constraint
class KnownTypeAst uni x where
type ToHoles x :: [Hole]
type ToHoles x = ToHoles (ElaborateBuiltin x)
type ToBinds x :: [GADT.Some TyNameRep]
type ToBinds x = ToBinds (ElaborateBuiltin x)
toTypeAst :: proxy x -> Type TyName uni ()
default toTypeAst :: KnownBuiltinTypeAst uni x => proxy x -> Type TyName uni ()
toTypeAst proxy x
_ = Proxy (ElaborateBuiltin x) -> Type TyName uni ()
forall a (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst uni x =>
proxy x -> Type TyName uni ()
toTypeAst (Proxy (ElaborateBuiltin x) -> Type TyName uni ())
-> Proxy (ElaborateBuiltin x) -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ Proxy (ElaborateBuiltin x)
forall k (t :: k). Proxy t
Proxy @(ElaborateBuiltin x)
{-# INLINE toTypeAst #-}
instance KnownTypeAst uni a => KnownTypeAst uni (EvaluationResult a) where
type ToHoles (EvaluationResult a) = '[TypeHole a]
type ToBinds (EvaluationResult a) = ToBinds a
toTypeAst :: proxy (EvaluationResult a) -> Type TyName uni ()
toTypeAst proxy (EvaluationResult a)
_ = Proxy a -> Type TyName uni ()
forall a (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst uni x =>
proxy x -> Type TyName uni ()
toTypeAst (Proxy a -> Type TyName uni ()) -> Proxy a -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ Proxy a
forall k (t :: k). Proxy t
Proxy @a
{-# INLINE toTypeAst #-}
instance KnownTypeAst uni a => KnownTypeAst uni (Emitter a) where
type ToHoles (Emitter a) = '[TypeHole a]
type ToBinds (Emitter a) = ToBinds a
toTypeAst :: proxy (Emitter a) -> Type TyName uni ()
toTypeAst proxy (Emitter a)
_ = Proxy a -> Type TyName uni ()
forall a (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst uni x =>
proxy x -> Type TyName uni ()
toTypeAst (Proxy a -> Type TyName uni ()) -> Proxy a -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ Proxy a
forall k (t :: k). Proxy t
Proxy @a
{-# INLINE toTypeAst #-}
instance KnownTypeAst uni rep => KnownTypeAst uni (SomeConstant uni rep) where
type ToHoles (SomeConstant _ rep) = '[RepHole rep]
type ToBinds (SomeConstant _ rep) = ToBinds rep
toTypeAst :: proxy (SomeConstant uni rep) -> Type TyName uni ()
toTypeAst proxy (SomeConstant uni rep)
_ = Proxy rep -> Type TyName uni ()
forall a (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst uni x =>
proxy x -> Type TyName uni ()
toTypeAst (Proxy rep -> Type TyName uni ())
-> Proxy rep -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ Proxy rep
forall k (t :: k). Proxy t
Proxy @rep
{-# INLINE toTypeAst #-}
instance KnownTypeAst uni rep => KnownTypeAst uni (Opaque val rep) where
type ToHoles (Opaque _ rep) = '[RepHole rep]
type ToBinds (Opaque _ rep) = ToBinds rep
toTypeAst :: proxy (Opaque val rep) -> Type TyName uni ()
toTypeAst proxy (Opaque val rep)
_ = Proxy rep -> Type TyName uni ()
forall a (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst uni x =>
proxy x -> Type TyName uni ()
toTypeAst (Proxy rep -> Type TyName uni ())
-> Proxy rep -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ Proxy rep
forall k (t :: k). Proxy t
Proxy @rep
{-# INLINE toTypeAst #-}
toTyNameAst
:: forall text uniq. (KnownSymbol text, KnownNat uniq)
=> Proxy ('TyNameRep text uniq) -> TyName
toTyNameAst :: Proxy ('TyNameRep text uniq) -> TyName
toTyNameAst Proxy ('TyNameRep text uniq)
_ =
Name -> TyName
TyName (Name -> TyName) -> Name -> TyName
forall a b. (a -> b) -> a -> b
$ Text -> Unique -> Name
Name
(String -> Text
Text.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Proxy text -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal @text Proxy text
forall k (t :: k). Proxy t
Proxy)
(Int -> Unique
Unique (Int -> Unique) -> (Integer -> Int) -> Integer -> Unique
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Unique) -> Integer -> Unique
forall a b. (a -> b) -> a -> b
$ Proxy uniq -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @uniq Proxy uniq
forall k (t :: k). Proxy t
Proxy)
{-# INLINE toTyNameAst #-}
instance uni `Contains` f => KnownTypeAst uni (BuiltinHead f) where
type ToHoles (BuiltinHead f) = '[]
type ToBinds (BuiltinHead f) = '[]
toTypeAst :: proxy (BuiltinHead f) -> Type TyName uni ()
toTypeAst proxy (BuiltinHead f)
_ = () -> Type TyName uni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
Contains uni a =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @f ()
{-# INLINE toTypeAst #-}
instance (KnownTypeAst uni a, KnownTypeAst uni b) => KnownTypeAst uni (a -> b) where
type ToHoles (a -> b) = '[TypeHole a, TypeHole b]
type ToBinds (a -> b) = Merge (ToBinds a) (ToBinds b)
toTypeAst :: proxy (a -> b) -> Type TyName uni ()
toTypeAst proxy (a -> b)
_ = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (Proxy a -> Type TyName uni ()
forall a (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst uni x =>
proxy x -> Type TyName uni ()
toTypeAst (Proxy a -> Type TyName uni ()) -> Proxy a -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ Proxy a
forall k (t :: k). Proxy t
Proxy @a) (Proxy b -> Type TyName uni ()
forall a (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst uni x =>
proxy x -> Type TyName uni ()
toTypeAst (Proxy b -> Type TyName uni ()) -> Proxy b -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ Proxy b
forall k (t :: k). Proxy t
Proxy @b)
{-# INLINE toTypeAst #-}
instance (name ~ 'TyNameRep text uniq, KnownSymbol text, KnownNat uniq) =>
KnownTypeAst uni (TyVarRep name) where
type ToHoles (TyVarRep name) = '[]
type ToBinds (TyVarRep name) = '[ 'GADT.Some name ]
toTypeAst :: proxy (TyVarRep name) -> Type TyName uni ()
toTypeAst proxy (TyVarRep name)
_ = () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () (TyName -> Type TyName uni ())
-> (Proxy ('TyNameRep text uniq) -> TyName)
-> Proxy ('TyNameRep text uniq)
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy ('TyNameRep text uniq) -> TyName
forall kind (text :: Symbol) (uniq :: Nat).
(KnownSymbol text, KnownNat uniq) =>
Proxy ('TyNameRep text uniq) -> TyName
toTyNameAst (Proxy ('TyNameRep text uniq) -> Type TyName uni ())
-> Proxy ('TyNameRep text uniq) -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ Proxy ('TyNameRep text uniq)
forall k (t :: k). Proxy t
Proxy @('TyNameRep text uniq)
{-# INLINE toTypeAst #-}
instance (KnownTypeAst uni fun, KnownTypeAst uni arg) => KnownTypeAst uni (TyAppRep fun arg) where
type ToHoles (TyAppRep fun arg) = '[RepHole fun, RepHole arg]
type ToBinds (TyAppRep fun arg) = Merge (ToBinds fun) (ToBinds arg)
toTypeAst :: proxy (TyAppRep fun arg) -> Type TyName uni ()
toTypeAst proxy (TyAppRep fun arg)
_ = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () (Proxy fun -> Type TyName uni ()
forall a (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst uni x =>
proxy x -> Type TyName uni ()
toTypeAst (Proxy fun -> Type TyName uni ())
-> Proxy fun -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ Proxy fun
forall k (t :: k). Proxy t
Proxy @fun) (Proxy arg -> Type TyName uni ()
forall a (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst uni x =>
proxy x -> Type TyName uni ()
toTypeAst (Proxy arg -> Type TyName uni ())
-> Proxy arg -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ Proxy arg
forall k (t :: k). Proxy t
Proxy @arg)
{-# INLINE toTypeAst #-}
instance
( name ~ 'TyNameRep @kind text uniq, KnownSymbol text, KnownNat uniq
, KnownKind kind, KnownTypeAst uni a
) => KnownTypeAst uni (TyForallRep name a) where
type ToHoles (TyForallRep name a) = '[RepHole a]
type ToBinds (TyForallRep name a) = Delete ('GADT.Some name) (ToBinds a)
toTypeAst :: proxy (TyForallRep name a) -> Type TyName uni ()
toTypeAst proxy (TyForallRep name a)
_ =
() -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall ()
(Proxy ('TyNameRep text uniq) -> TyName
forall kind (text :: Symbol) (uniq :: Nat).
(KnownSymbol text, KnownNat uniq) =>
Proxy ('TyNameRep text uniq) -> TyName
toTyNameAst (Proxy ('TyNameRep text uniq) -> TyName)
-> Proxy ('TyNameRep text uniq) -> TyName
forall a b. (a -> b) -> a -> b
$ Proxy ('TyNameRep text uniq)
forall k (t :: k). Proxy t
Proxy @('TyNameRep text uniq))
(SingKind kind -> Kind ()
forall k. SingKind k -> Kind ()
demoteKind (SingKind kind -> Kind ()) -> SingKind kind -> Kind ()
forall a b. (a -> b) -> a -> b
$ KnownKind kind => SingKind kind
forall k. KnownKind k => SingKind k
knownKind @kind)
(Proxy a -> Type TyName uni ()
forall a (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst uni x =>
proxy x -> Type TyName uni ()
toTypeAst (Proxy a -> Type TyName uni ()) -> Proxy a -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ Proxy a
forall k (t :: k). Proxy t
Proxy @a)
{-# INLINE toTypeAst #-}
type family Delete x xs :: [a] where
Delete _ '[] = '[]
Delete x (x ': xs) = Delete x xs
Delete x (y ': xs) = y ': Delete x xs
type family Merge xs ys :: [a] where
Merge '[] ys = ys
Merge (x ': xs) ys = x ': Delete x (Merge xs ys)