{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StrictData #-}
module PlutusCore.Builtin.TypeScheme
( Typeable
, TypeScheme (..)
, argProxy
, typeSchemeToType
) where
import PlutusCore.Builtin.KnownKind
import PlutusCore.Builtin.KnownType
import PlutusCore.Builtin.KnownTypeAst
import PlutusCore.Core
import PlutusCore.Name.Unique
import Data.Kind qualified as GHC (Type)
import Data.Proxy
import Data.Text qualified as Text
import Data.Typeable
import GHC.TypeLits
infixr 9 `TypeSchemeArrow`
data TypeScheme val (args :: [GHC.Type]) res where
TypeSchemeResult
:: (Typeable res, KnownTypeAst TyName (UniOf val) res, MakeKnown val res)
=> TypeScheme val '[] res
TypeSchemeArrow
:: (Typeable arg, KnownTypeAst TyName (UniOf val) arg, MakeKnown val arg, ReadKnown val arg)
=> TypeScheme val args res -> TypeScheme val (arg ': args) res
TypeSchemeAll
:: (KnownSymbol text, KnownNat uniq, KnownKind kind)
=> Proxy '(text, uniq, kind)
-> TypeScheme val args res
-> TypeScheme val args res
argProxy :: TypeScheme val (arg ': args) res -> Proxy arg
argProxy :: forall val arg (args :: [*]) res.
TypeScheme val (arg : args) res -> Proxy arg
argProxy TypeScheme val (arg : args) res
_ = Proxy arg
forall {k} (t :: k). Proxy t
Proxy
typeSchemeToType :: TypeScheme val args res -> Type TyName (UniOf val) ()
typeSchemeToType :: forall val (args :: [*]) res.
TypeScheme val args res -> Type TyName (UniOf val) ()
typeSchemeToType sch :: TypeScheme val args res
sch@TypeScheme val args res
TypeSchemeResult = TypeScheme val args res -> Type TyName (UniOf val) ()
forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst tyname uni x =>
proxy x -> Type tyname uni ()
toTypeAst TypeScheme val args res
sch
typeSchemeToType sch :: TypeScheme val args res
sch@(TypeSchemeArrow TypeScheme val args res
schB) =
()
-> Type TyName (UniOf val) ()
-> Type TyName (UniOf val) ()
-> Type TyName (UniOf val) ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (Proxy arg -> Type TyName (UniOf val) ()
forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst tyname uni x =>
proxy x -> Type tyname uni ()
toTypeAst (Proxy arg -> Type TyName (UniOf val) ())
-> Proxy arg -> Type TyName (UniOf val) ()
forall a b. (a -> b) -> a -> b
$ TypeScheme val (arg : args) res -> Proxy arg
forall val arg (args :: [*]) res.
TypeScheme val (arg : args) res -> Proxy arg
argProxy TypeScheme val args res
TypeScheme val (arg : args) res
sch) (Type TyName (UniOf val) () -> Type TyName (UniOf val) ())
-> Type TyName (UniOf val) () -> Type TyName (UniOf val) ()
forall a b. (a -> b) -> a -> b
$ TypeScheme val args res -> Type TyName (UniOf val) ()
forall val (args :: [*]) res.
TypeScheme val args res -> Type TyName (UniOf val) ()
typeSchemeToType TypeScheme val args res
schB
typeSchemeToType (TypeSchemeAll (Proxy '(text, uniq, kind)
_ :: Proxy '(text, uniq, kind)) TypeScheme val args res
schB) =
let text :: Text
text = String -> Text
Text.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal @text Proxy text
forall {k} (t :: k). Proxy t
Proxy
uniq :: Int
uniq = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @uniq Proxy uniq
forall {k} (t :: k). Proxy t
Proxy
a :: TyName
a = Name -> TyName
TyName (Name -> TyName) -> Name -> TyName
forall a b. (a -> b) -> a -> b
$ Text -> Unique -> Name
Name Text
text (Unique -> Name) -> Unique -> Name
forall a b. (a -> b) -> a -> b
$ Int -> Unique
Unique Int
uniq
in ()
-> TyName
-> Kind ()
-> Type TyName (UniOf val) ()
-> Type TyName (UniOf val) ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
a (SingKind kind -> Kind ()
forall k. SingKind k -> Kind ()
demoteKind (SingKind kind -> Kind ()) -> SingKind kind -> Kind ()
forall a b. (a -> b) -> a -> b
$ forall k. KnownKind k => SingKind k
knownKind @kind) (Type TyName (UniOf val) () -> Type TyName (UniOf val) ())
-> Type TyName (UniOf val) () -> Type TyName (UniOf val) ()
forall a b. (a -> b) -> a -> b
$ TypeScheme val args res -> Type TyName (UniOf val) ()
forall val (args :: [*]) res.
TypeScheme val args res -> Type TyName (UniOf val) ()
typeSchemeToType TypeScheme val args res
schB
instance Show (TypeScheme val args res) where
showsPrec :: Int -> TypeScheme val args res -> ShowS
showsPrec Int
p sch :: TypeScheme val args res
sch@TypeScheme val args res
TypeSchemeResult =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0)
(ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> TypeRep -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (-Int
1) (TypeScheme val args res -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep TypeScheme val args res
sch)
showsPrec Int
p sch :: TypeScheme val args res
sch@(TypeSchemeArrow TypeScheme val args res
schB) =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0)
(ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
Int -> TypeRep -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 (Proxy arg -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy arg -> TypeRep) -> Proxy arg -> TypeRep
forall a b. (a -> b) -> a -> b
$ TypeScheme val (arg : args) res -> Proxy arg
forall val arg (args :: [*]) res.
TypeScheme val (arg : args) res -> Proxy arg
argProxy TypeScheme val args res
TypeScheme val (arg : args) res
sch)
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" -> "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> TypeScheme val args res -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (-Int
1) TypeScheme val args res
schB
showsPrec Int
p (TypeSchemeAll (Proxy '(text, uniq, kind)
_ :: Proxy '(text, uniq, kind)) TypeScheme val args res
schB) =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0)
(ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"forall "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString (forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal @text Proxy text
forall {k} (t :: k). Proxy t
Proxy)
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
". "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> TypeScheme val args res -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 TypeScheme val args res
schB