-- editorconfig-checker-disable-file
-- | This module assigns types to built-ins.
-- See the @plutus/plutus-core/docs/Constant application.md@
-- article for how this emerged.

{-# 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`

{- Note [MakeKnown in TypeSchemeArrow]
There's a @MakeKnown val arg@ constrained packed in the 'TypeSchemeArrow' constructor. It's not
supposed to be there, but unfortunately, in the @Generators@ tests we use 'TypeScheme' for
generation of arbitrary arguments of builtins and that requires 'makeKnown', which makes us have
the 'MakeKnown' in 'TypeSchemeArrow'.

The solution is to fix the @Generators@ tests. Explicitly constraining @args@ outside of
'TypeScheme' sounds like a promising strategy. Maybe we could just delete those tests altogether.

However it's also worth considering untangling 'RuntimeScheme' from 'TypeScheme' and generating the
two in parallel, so that we only need to optimize the former. Then we will be able to afford having
any kind of nonsense in 'TypeScheme'. Another reason for that would be the fact that Core output
has 'typeSchemeToRuntimeScheme' all over the place as it can't be inlined due to being a recursive
function, which we can't turn into an inlinable class method, because the indices of 'TypeScheme'
don't reflect its structure due to the 'TypeSchemeAll' constructor not being reflected at the type
level in any way. It's unlikely that having those 'typeSchemeToRuntimeScheme' has any impact on
performance, because they're only evaluated once during initialization, but it certainly has impact
on readability of the Core output.
-}

-- We have these 'Typeable' constraints here just for the generators tests. It's fine since
-- 'TypeScheme' is not used for evaluation and so we can shove into 'TypeScheme' whatever we want.
-- | The type of type schemes of built-in functions.
-- @args@ is a list of types of arguments, @res@ is the resulting type.
-- E.g. @Text -> Bool -> Integer@ is encoded as @TypeScheme val [Text, Bool] Integer@.
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

-- | Convert a 'TypeScheme' to the corresponding 'Type'.
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

-- The precedence of @->@ is @-1@, which is why this number appears in the implementation of the
-- instance.
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
$ -- @0@ is to account for associativity, see https://stackoverflow.com/a/43639618
              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