-- editorconfig-checker-disable-file
{-# LANGUAGE CPP               #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns      #-}

-- | Functions for compiling GHC kinds into PlutusCore kinds.
module PlutusTx.Compiler.Kind (compileKind) where

import PlutusTx.Compiler.Error
import PlutusTx.Compiler.Trace
import PlutusTx.Compiler.Types
import PlutusTx.Compiler.Utils

import GHC.Plugins qualified as GHC

import PlutusCore qualified as PLC

compileKind :: Compiling uni fun m ann => GHC.Kind -> m (PLC.Kind ())
compileKind :: forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
Kind -> m (Kind ())
compileKind Kind
k = Int -> SDoc -> m (Kind ()) -> m (Kind ())
forall (uni :: * -> *) fun (m :: * -> *) e a.
(MonadReader (CompileContext uni fun) m, MonadState CompileState m,
 MonadError (WithContext Text e) m) =>
Int -> SDoc -> m a -> m a
traceCompilation Int
2 (SDoc
"Compiling kind:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
GHC.<+> Kind -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr Kind
k) (m (Kind ()) -> m (Kind ())) -> m (Kind ()) -> m (Kind ())
forall a b. (a -> b) -> a -> b
$ case Kind
k of
    -- this is a bit weird because GHC uses 'Type' to represent kinds, so '* -> *' is a 'TyFun'
    (Kind -> Bool
GHC.isLiftedTypeKind -> Bool
True)         -> Kind () -> m (Kind ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> m (Kind ())) -> Kind () -> m (Kind ())
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
PLC.Type ()
    (Kind -> Maybe (FunTyFlag, Kind, Kind, Kind)
GHC.splitFunTy_maybe -> Just (FunTyFlag, Kind, Kind, Kind)
r) -> case (FunTyFlag, Kind, Kind, Kind)
r of
#if MIN_VERSION_ghc(9,6,0)
        (FunTyFlag
_t, Kind
_m, Kind
i, Kind
o) -> () -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
PLC.KindArrow () (Kind () -> Kind () -> Kind ())
-> m (Kind ()) -> m (Kind () -> Kind ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind -> m (Kind ())
forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
Kind -> m (Kind ())
compileKind Kind
i m (Kind () -> Kind ()) -> m (Kind ()) -> m (Kind ())
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Kind -> m (Kind ())
forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
Kind -> m (Kind ())
compileKind Kind
o
#else
        (_m, i, o)     -> PLC.KindArrow () <$> compileKind i <*> compileKind o
#endif
    -- Ignore type binders for runtime rep variables, see Note [Runtime reps]
    (Kind -> Maybe (TyCoVar, Kind)
GHC.splitForAllTyCoVar_maybe -> Just (TyCoVar
tvar, Kind
ty)) | (Kind -> Bool
GHC.isRuntimeRepTy (Kind -> Bool) -> (TyCoVar -> Kind) -> TyCoVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCoVar -> Kind
GHC.varType) TyCoVar
tvar -> Kind -> m (Kind ())
forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
Kind -> m (Kind ())
compileKind Kind
ty
    -- Interpret 'TYPE rep' as 'TYPE LiftedRep', for any rep, see Note [Runtime reps]
#if MIN_VERSION_ghc(9,6,0)
    (Kind -> Bool
GHC.isTypeLikeKind -> Bool
True) -> Kind () -> m (Kind ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> m (Kind ())) -> Kind () -> m (Kind ())
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
PLC.Type ()
#else
    (GHC.classifiesTypeWithValues -> True) -> pure $ PLC.Type ()
#endif
    Kind
_                                      -> (Text -> Error uni fun ann) -> SDoc -> m (Kind ())
forall (uni :: * -> *) fun ann (m :: * -> *) a.
(MonadError (CompileError uni fun ann) m,
 MonadReader (CompileContext uni fun) m) =>
(Text -> Error uni fun ann) -> SDoc -> m a
throwSd Text -> Error uni fun ann
forall (uni :: * -> *) fun a. Text -> Error uni fun a
UnsupportedError (SDoc -> m (Kind ())) -> SDoc -> m (Kind ())
forall a b. (a -> b) -> a -> b
$ SDoc
"Kind:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
GHC.<+> (Kind -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr Kind
k)