{-# LANGUAGE CPP               #-}
{-# LANGUAGE ConstraintKinds   #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections     #-}
{-# LANGUAGE TypeApplications  #-}
{-# LANGUAGE ViewPatterns      #-}

{- | Functions for compiling GHC types into PlutusCore types, as well as compiling constructors,
matchers, and pattern match alternatives.
-}
module PlutusTx.Compiler.Type (
  compileTypeNorm,
  compileType,
  compileKind,
  getDataCons,
  getConstructors,
  getMatch,
  getMatchInstantiated,
) where

import PlutusTx.Compiler.Binders
import PlutusTx.Compiler.Error
import PlutusTx.Compiler.Kind
import PlutusTx.Compiler.Names
import PlutusTx.Compiler.Trace
import PlutusTx.Compiler.Types
import PlutusTx.Compiler.Utils
import PlutusTx.PIRTypes

import GHC.Builtin.Types.Prim qualified as GHC
import GHC.Core.FamInstEnv qualified as GHC
import GHC.Core.Multiplicity qualified as GHC
#if MIN_VERSION_ghc(9,4,0)
import GHC.Core.Reduction qualified as GHC
#endif
import GHC.Plugins qualified as GHC

import PlutusIR qualified as PIR
import PlutusIR.Compiler.Definitions qualified as PIR
import PlutusIR.MkPir qualified as PIR

import PlutusCore.Name.Unique qualified as PLC

import Control.Monad.Extra
import Control.Monad.Reader

import Data.List (sortBy)
import Data.Set qualified as Set
import Data.Traversable

-- Types

{- Note [Type families and normalizing types]
GHC provides a function to normalize type and data family applications in a type. This
is great for us, since it means that we can support them "for free" by just normalizing
them away.

However, that means we won't support cases that *don't* reduce, e.g. cases where the
family is applied to a type variable.

Technically, this normalization comes along with a coercion, since for data families
the instance type is only *representationally* equal to the family application. This is
okay for us, since we *always* treat data family applications as their instance type.

TODO: use topNormaliseType to be more efficient and handle newtypes as well. Problem
is dealing with recursive newtypes.
-}

{- | Compile a type, first of all normalizing it to remove type family redexes.

Generally, we need to call this whenever we are compiling a "new" type from the program.
If we are compiling a part of a type we are already processing then it has likely been
normalized and we can just use 'compileType'
-}
compileTypeNorm :: (CompilingDefault uni fun m ann) => GHC.Type -> m (PIRType uni)
compileTypeNorm :: forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Type -> m (PIRType uni)
compileTypeNorm Type
ty = do
  CompileContext{ccFamInstEnvs :: forall (uni :: * -> *) fun. CompileContext uni fun -> FamInstEnvs
ccFamInstEnvs = FamInstEnvs
envs} <- m (CompileContext DefaultUni DefaultFun)
forall r (m :: * -> *). MonadReader r m => m r
ask
  -- See Note [Type families and normalizing types]
#if MIN_VERSION_ghc(9,4,0)
  let (GHC.Reduction Coercion
_ Type
ty') = FamInstEnvs -> Role -> Type -> Reduction
GHC.normaliseType FamInstEnvs
envs Role
GHC.Representational Type
ty
#else
  let (_, ty') = GHC.normaliseType envs GHC.Representational ty
#endif
  Type -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Type -> m (PIRType uni)
compileType Type
ty'

-- | Compile a type.
compileType :: (CompilingDefault uni fun m ann) => GHC.Type -> m (PIRType uni)
compileType :: forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Type -> m (PIRType uni)
compileType Type
t = Int -> SDoc -> m (PIRType uni) -> m (PIRType uni)
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 type:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
GHC.<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr Type
t) (m (PIRType uni) -> m (PIRType uni))
-> m (PIRType uni) -> m (PIRType uni)
forall a b. (a -> b) -> a -> b
$ do
  -- See Note [Scopes]
  CompileContext{ccScope :: forall (uni :: * -> *) fun. CompileContext uni fun -> Scope uni
ccScope = Scope DefaultUni
scope} <- m (CompileContext DefaultUni DefaultFun)
forall r (m :: * -> *). MonadReader r m => m r
ask
  case Type
t of
    -- in scope type name
    (Type -> Maybe TyVar
GHC.getTyVar_maybe -> Just TyVar
v) -> case Scope DefaultUni -> Name -> Maybe PLCTyVar
forall (uni :: * -> *). Scope uni -> Name -> Maybe PLCTyVar
lookupTyName Scope DefaultUni
scope (TyVar -> Name
forall a. NamedThing a => a -> Name
GHC.getName TyVar
v) of
      Just (PIR.TyVarDecl Ann
_ TyName
name Kind Ann
_) -> PIRType uni -> m (PIRType uni)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PIRType uni -> m (PIRType uni)) -> PIRType uni -> m (PIRType uni)
forall a b. (a -> b) -> a -> b
$ Ann -> TyName -> PIRType uni
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
PIR.TyVar Ann
annMayInline TyName
name
      Maybe PLCTyVar
Nothing ->
        (Text -> Error DefaultUni DefaultFun ann)
-> SDoc -> m (PIRType uni)
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 DefaultUni DefaultFun ann
forall (uni :: * -> *) fun a. Text -> Error uni fun a
FreeVariableError (SDoc -> m (PIRType uni)) -> SDoc -> m (PIRType uni)
forall a b. (a -> b) -> a -> b
$ SDoc
"Type variable:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
GHC.<+> TyVar -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr TyVar
v
    (Type -> Maybe (FunTyFlag, Type, Type, Type)
GHC.splitFunTy_maybe -> Just (FunTyFlag, Type, Type, Type)
r) -> case (FunTyFlag, Type, Type, Type)
r of
#if MIN_VERSION_ghc(9,6,0)
      (FunTyFlag
_t, Type
_m, Type
i, Type
o) -> Ann -> PIRType uni -> PIRType uni -> PIRType uni
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
PIR.TyFun Ann
annMayInline (PIRType uni -> PIRType uni -> PIRType uni)
-> m (PIRType uni) -> m (PIRType uni -> PIRType uni)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Type -> m (PIRType uni)
compileType Type
i m (PIRType uni -> PIRType uni)
-> m (PIRType uni) -> m (PIRType uni)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Type -> m (PIRType uni)
compileType Type
o
#else
      (_m, i, o)     -> PIR.TyFun annMayInline <$> compileType i <*> compileType o
#endif
    ((() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
GHC.splitTyConApp_maybe -> Just (TyCon
tc, [Type]
ts)) ->
      PIRType uni -> [(Ann, PIRType uni)] -> PIRType uni
forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> [(ann, Type tyname uni ann)] -> Type tyname uni ann
PIR.mkIterTyApp
        (PIRType uni -> [(Ann, PIRType uni)] -> PIRType uni)
-> m (PIRType uni) -> m ([(Ann, PIRType uni)] -> PIRType uni)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
TyCon -> m (PIRType uni)
compileTyCon TyCon
tc
        -- Ignore 'RuntimeRep' type arguments to type constructors, see Note [Runtime reps]
        m ([(Ann, PIRType uni)] -> PIRType uni)
-> m [(Ann, PIRType uni)] -> m (PIRType uni)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((Type -> m (Ann, PIRType uni)) -> [Type] -> m [(Ann, PIRType uni)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((PIRType uni -> (Ann, PIRType uni))
-> m (PIRType uni) -> m (Ann, PIRType uni)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Ann
annMayInline,) (m (PIRType uni) -> m (Ann, PIRType uni))
-> (Type -> m (PIRType uni)) -> Type -> m (Ann, PIRType uni)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Type -> m (PIRType uni)
compileType) ([Type] -> [Type]
GHC.dropRuntimeRepArgs [Type]
ts))
    (Type -> Maybe (Type, Type)
GHC.splitAppTy_maybe -> Just (Type
t1, Type
t2)) ->
      Ann -> PIRType uni -> PIRType uni -> PIRType uni
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
PIR.TyApp Ann
annMayInline (PIRType uni -> PIRType uni -> PIRType uni)
-> m (PIRType uni) -> m (PIRType uni -> PIRType uni)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Type -> m (PIRType uni)
compileType Type
t1 m (PIRType uni -> PIRType uni)
-> m (PIRType uni) -> m (PIRType uni)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Type -> m (PIRType uni)
compileType Type
t2
    (Type -> Maybe (TyVar, Type)
GHC.splitForAllTyCoVar_maybe -> Just (TyVar
tv, Type
tpe)) ->
      -- Ignore type binders for runtime rep variables, see Note [Runtime reps]
      if (Type -> Bool
GHC.isRuntimeRepTy (Type -> Bool) -> (TyVar -> Type) -> TyVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
GHC.varType) TyVar
tv
      then Type -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Type -> m (PIRType uni)
compileType Type
tpe
      else TyVar -> m (PIRType uni) -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
TyVar -> m (PIRType uni) -> m (PIRType uni)
mkTyForallScoped TyVar
tv (Type -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Type -> m (PIRType uni)
compileType Type
tpe)
    -- I think it's safe to ignore the coercion here
    (Type -> Maybe (Type, Coercion)
GHC.splitCastTy_maybe -> Just (Type
tpe, Coercion
_)) -> Type -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Type -> m (PIRType uni)
compileType Type
tpe
    Type
_ -> (Text -> Error DefaultUni DefaultFun ann)
-> SDoc -> m (PIRType uni)
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 DefaultUni DefaultFun ann
forall (uni :: * -> *) fun a. Text -> Error uni fun a
UnsupportedError (SDoc -> m (PIRType uni)) -> SDoc -> m (PIRType uni)
forall a b. (a -> b) -> a -> b
$ SDoc
"Type" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
GHC.<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr Type
t

{- Note [Occurrences of recursive names]
When we compile recursive types/terms, we need to process their definitions before we can produce
the final definition that we will use going forward.

But the thing that makes them *recursive* is that they appear in their own definitions! So
what do we do when we see those occurrences?

For cases where we are introducing a new variable for the definition (terms and datatypes), we
simply add that variable as a "fake" definition before we process the definition of the main
entity. That will be enough to ensure that we can make references to it normally, without making
us loop. Then we fix it up at the end.

For newtypes, we can't do this because the final value we will use is precisely the definition. So
we just have to ban recursive newtypes, and we do this by blackholing the name while we process the
definition, and dying if we see it again.
-}

compileTyCon ::
  forall uni fun m ann.
  (CompilingDefault uni fun m ann) =>
  GHC.TyCon ->
  m (PIRType uni)
compileTyCon :: forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
TyCon -> m (PIRType uni)
compileTyCon TyCon
tc
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
GHC.intTyCon = Error DefaultUni DefaultFun ann -> m (PIRType uni)
forall c e (m :: * -> *) a.
MonadError (WithContext c e) m =>
e -> m a
throwPlain (Error DefaultUni DefaultFun ann -> m (PIRType uni))
-> Error DefaultUni DefaultFun ann -> m (PIRType uni)
forall a b. (a -> b) -> a -> b
$ Text -> Error DefaultUni DefaultFun ann
forall (uni :: * -> *) fun a. Text -> Error uni fun a
UnsupportedError Text
"Int: use Integer instead"
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
GHC.intPrimTyCon =
      Error DefaultUni DefaultFun ann -> m (PIRType uni)
forall c e (m :: * -> *) a.
MonadError (WithContext c e) m =>
e -> m a
throwPlain (Error DefaultUni DefaultFun ann -> m (PIRType uni))
-> Error DefaultUni DefaultFun ann -> m (PIRType uni)
forall a b. (a -> b) -> a -> b
$
        Text -> Error DefaultUni DefaultFun ann
forall (uni :: * -> *) fun a. Text -> Error uni fun a
UnsupportedError Text
"Int#: unboxed integers are not supported"
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
GHC.unboxedUnitTyCon = PIRType uni -> m (PIRType uni)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
PIR.mkTyBuiltin @_ @() Ann
annMayInline)
  | Bool
otherwise = do
      let tcName :: Name
tcName = TyCon -> Name
forall a. NamedThing a => a -> Name
GHC.getName TyCon
tc
          lexName :: LexName
lexName = Name -> LexName
LexName Name
tcName
      m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Name -> m Bool
forall (uni :: * -> *) fun (m :: * -> *).
MonadReader (CompileContext uni fun) m =>
Name -> m Bool
blackholed Name
tcName) (m () -> m ()) -> (SDoc -> m ()) -> SDoc -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Error DefaultUni DefaultFun ann) -> SDoc -> m ()
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 DefaultUni DefaultFun ann
forall (uni :: * -> *) fun a. Text -> Error uni fun a
UnsupportedError (SDoc -> m ()) -> SDoc -> m ()
forall a b. (a -> b) -> a -> b
$
        SDoc
"Recursive newtypes, use data:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
GHC.<+> Name -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr Name
tcName
      -- See Note [Dependency tracking]
      (Set LexName -> Set LexName) -> m ()
forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
(Set LexName -> Set LexName) -> m ()
modifyCurDeps (\Set LexName
d -> LexName -> Set LexName -> Set LexName
forall a. Ord a => a -> Set a -> Set a
Set.insert LexName
lexName Set LexName
d)
      Maybe (PIRType uni)
maybeDef <- Ann -> LexName -> m (Maybe (PIRType uni))
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
ann -> key -> m (Maybe (Type TyName uni ann))
PIR.lookupType Ann
annMayInline LexName
lexName
      case Maybe (PIRType uni)
maybeDef of
        Just PIRType uni
ty -> PIRType uni -> m (PIRType uni)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PIRType uni
ty
        -- See Note [Dependency tracking]
        Maybe (PIRType uni)
Nothing -> LexName -> m (PIRType uni) -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann a.
Compiling uni fun m ann =>
LexName -> m a -> m a
withCurDef LexName
lexName (m (PIRType uni) -> m (PIRType uni))
-> m (PIRType uni) -> m (PIRType uni)
forall a b. (a -> b) -> a -> b
$ do
          PLCTyVar
tvd <- TyCon -> m PLCTyVar
forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
TyCon -> m PLCTyVar
compileTcTyVarFresh TyCon
tc
          case TyCon -> Maybe ([TyVar], Type, CoAxiom Unbranched)
GHC.unwrapNewTyCon_maybe TyCon
tc of
            Just ([TyVar]
_, Type
underlying, CoAxiom Unbranched
_) -> do
              -- See Note [Coercions and newtypes]
              -- See Note [Occurrences of recursive names]
              -- We do this for dependency tracking, we won't use it due to the blackholing
              LexName -> TypeDef TyName DefaultUni Ann -> Set LexName -> m ()
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
key -> TypeDef TyName uni ann -> Set key -> m ()
PIR.defineType LexName
lexName (PLCTyVar
-> Type TyName DefaultUni Ann -> TypeDef TyName DefaultUni Ann
forall var val. var -> val -> Def var val
PIR.Def PLCTyVar
tvd (Ann -> PLCTyVar -> Type TyName DefaultUni Ann
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
PIR.mkTyVar Ann
annMayInline PLCTyVar
tvd)) Set LexName
forall a. Monoid a => a
mempty
              -- Type variables are in scope for the rhs of the alias
              PIRType uni
alias <-
                [TyVar] -> m (PIRType uni) -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
[TyVar] -> m (PIRType uni) -> m (PIRType uni)
mkIterTyLamScoped (TyCon -> [TyVar]
GHC.tyConTyVars TyCon
tc) (m (PIRType uni) -> m (PIRType uni))
-> m (PIRType uni) -> m (PIRType uni)
forall a b. (a -> b) -> a -> b
$
                  Name -> m (PIRType uni) -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) a.
MonadReader (CompileContext uni fun) m =>
Name -> m a -> m a
blackhole (TyCon -> Name
forall a. NamedThing a => a -> Name
GHC.getName TyCon
tc) (m (PIRType uni) -> m (PIRType uni))
-> m (PIRType uni) -> m (PIRType uni)
forall a b. (a -> b) -> a -> b
$
                    Type -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Type -> m (PIRType uni)
compileTypeNorm Type
underlying
              LexName
-> (TypeDef TyName uni Ann -> TypeDef TyName uni Ann) -> m ()
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
key -> (TypeDef TyName uni ann -> TypeDef TyName uni ann) -> m ()
PIR.modifyTypeDef LexName
lexName (TypeDef TyName uni Ann
-> TypeDef TyName uni Ann -> TypeDef TyName uni Ann
forall a b. a -> b -> a
const (TypeDef TyName uni Ann
 -> TypeDef TyName uni Ann -> TypeDef TyName uni Ann)
-> TypeDef TyName uni Ann
-> TypeDef TyName uni Ann
-> TypeDef TyName uni Ann
forall a b. (a -> b) -> a -> b
$ PLCTyVar -> PIRType uni -> TypeDef TyName uni Ann
forall var val. var -> val -> Def var val
PIR.Def PLCTyVar
tvd PIRType uni
alias)
              forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
key -> m ()
PIR.recordAlias @LexName @uni @fun LexName
lexName
              PIRType uni -> m (PIRType uni)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PIRType uni
alias
            Maybe ([TyVar], Type, CoAxiom Unbranched)
Nothing -> do
              [DataCon]
dcs <- TyCon -> m [DataCon]
forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
TyCon -> m [DataCon]
getDataCons TyCon
tc
              Name
matchName <-
                TyName -> Name
PLC.unTyName
                  (TyName -> Name) -> (TyName -> TyName) -> TyName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Text) -> TyName -> TyName
PLC.mapTyNameString (Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_match")
                  (TyName -> Name) -> m TyName -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> m TyName
forall (m :: * -> *). MonadQuote m => Name -> m TyName
compileTyNameFresh (TyCon -> Name
forall a. NamedThing a => a -> Name
GHC.getName TyCon
tc)

              -- See Note [Occurrences of recursive names]
              let fakeDatatype :: Datatype TyName Name uni Ann
fakeDatatype = Ann
-> PLCTyVar
-> [PLCTyVar]
-> Name
-> [VarDecl TyName Name uni Ann]
-> Datatype TyName Name uni Ann
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
PIR.Datatype Ann
annMayInline PLCTyVar
tvd [] Name
matchName []
              forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
key -> DatatypeDef TyName Name uni ann -> Set key -> m ()
PIR.defineDatatype @_ @uni LexName
lexName (PLCTyVar
-> Datatype TyName Name uni Ann -> DatatypeDef TyName Name uni Ann
forall var val. var -> val -> Def var val
PIR.Def PLCTyVar
tvd Datatype TyName Name uni Ann
fakeDatatype) Set LexName
forall a. Set a
Set.empty

              -- Type variables are in scope for the rest of the definition
              -- We remove 'RuntimeRep' type variables with 'dropRuntimeRepVars'
              -- to compile unboxed tuples type constructor, see Note [Runtime reps]
              [TyVar] -> ([PLCTyVar] -> m ()) -> m ()
forall (uni :: * -> *) fun (m :: * -> *) ann a.
Compiling uni fun m ann =>
[TyVar] -> ([PLCTyVar] -> m a) -> m a
withTyVarsScoped ([TyVar] -> [TyVar]
dropRuntimeRepVars ([TyVar] -> [TyVar]) -> [TyVar] -> [TyVar]
forall a b. (a -> b) -> a -> b
$ TyCon -> [TyVar]
GHC.tyConTyVars TyCon
tc) (([PLCTyVar] -> m ()) -> m ()) -> ([PLCTyVar] -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \[PLCTyVar]
tvs -> do
                [VarDecl TyName Name uni Ann]
constructors <- [DataCon]
-> (DataCon -> m (VarDecl TyName Name uni Ann))
-> m [VarDecl TyName Name uni Ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [DataCon]
dcs ((DataCon -> m (VarDecl TyName Name uni Ann))
 -> m [VarDecl TyName Name uni Ann])
-> (DataCon -> m (VarDecl TyName Name uni Ann))
-> m [VarDecl TyName Name uni Ann]
forall a b. (a -> b) -> a -> b
$ \DataCon
dc -> do
                  Name
name <- Name -> m Name
forall (m :: * -> *). MonadQuote m => Name -> m Name
compileNameFresh (DataCon -> Name
forall a. NamedThing a => a -> Name
GHC.getName DataCon
dc)
                  PIRType uni
ty <- DataCon -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
DataCon -> m (PIRType uni)
mkConstructorType DataCon
dc
                  VarDecl TyName Name uni Ann -> m (VarDecl TyName Name uni Ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni Ann -> m (VarDecl TyName Name uni Ann))
-> VarDecl TyName Name uni Ann -> m (VarDecl TyName Name uni Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Name -> PIRType uni -> VarDecl TyName Name uni Ann
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
PIR.VarDecl Ann
annMayInline Name
name PIRType uni
ty

                let datatype :: Datatype TyName Name uni Ann
datatype = Ann
-> PLCTyVar
-> [PLCTyVar]
-> Name
-> [VarDecl TyName Name uni Ann]
-> Datatype TyName Name uni Ann
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
PIR.Datatype Ann
annMayInline PLCTyVar
tvd [PLCTyVar]
tvs Name
matchName [VarDecl TyName Name uni Ann]
constructors

                forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
key
-> (DatatypeDef TyName Name uni ann
    -> DatatypeDef TyName Name uni ann)
-> m ()
PIR.modifyDatatypeDef @_ @uni LexName
lexName (DatatypeDef TyName Name uni Ann
-> DatatypeDef TyName Name uni Ann
-> DatatypeDef TyName Name uni Ann
forall a b. a -> b -> a
const (DatatypeDef TyName Name uni Ann
 -> DatatypeDef TyName Name uni Ann
 -> DatatypeDef TyName Name uni Ann)
-> DatatypeDef TyName Name uni Ann
-> DatatypeDef TyName Name uni Ann
-> DatatypeDef TyName Name uni Ann
forall a b. (a -> b) -> a -> b
$ PLCTyVar
-> Datatype TyName Name uni Ann -> DatatypeDef TyName Name uni Ann
forall var val. var -> val -> Def var val
PIR.Def PLCTyVar
tvd Datatype TyName Name uni Ann
datatype)
              PIRType uni -> m (PIRType uni)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PIRType uni -> m (PIRType uni)) -> PIRType uni -> m (PIRType uni)
forall a b. (a -> b) -> a -> b
$ Ann -> PLCTyVar -> PIRType uni
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
PIR.mkTyVar Ann
annMayInline PLCTyVar
tvd

{- Note [Case expressions and laziness]
PLC is strict, but users *do* expect that, e.g. they can write an if expression and have it be
lazy. This only *matters* because we have 'error', so it's important that 'if false error else ...'
does not evaluate to 'error'!

More generally, we can compile case expressions (of which an if expression is one) lazily,
i.e. we add a unit argument and apply it at the end.

However, we apply an important optimization: we only need to do this if it is not the case that
all the case expressions are values. In the common case they *will* be, so this gives us
significantly better codegen a lot of the time.

The check we do is:
- Alternatives with arguments will be turned into lambdas by us, so will be values.
- Otherwise, we compile the expression (we can do this easily since it doesn't need any variables
  in scope), and check whether it is a value.

This is somewhat wasteful, since we may compile the expression twice, but it's difficult to avoid,
and it's hard to tell if a GHC core expression will be a PLC value or not. Easiest to just try it.

One further optimization: we don't do compile a case lazily if it has one alternative. In this case
we're going to evaluate that alternative unconditionally, *and* we're going to evaluate the
scrutinee first, so the effects will also be in the right order.
-}

{- Note [Ordering of constructors]
It is very important that we compile types and constructors consistently, especially between
lifting at runtime and compilation via the plugin. The main place we can get bitten is ordering.

GHC is under no obligation to give us any particular ordering of constructors, so we impose
an alphabetical one (with a few exceptions, see [Ensuring compatibility with spec and stdlib
types]).

The other place where ordering matters is arguments to constructors, but here there is a
clear natural ordering which we will assume GHC respects.
-}

{- Note [Ensuring compatibility with spec and stdlib types]
Haskell's Bool has its constructors ordered with False before True, which results in the
normal case expression having the oppposite sense to the one in the spec, where
the true branch comes first (which is more logical).

Our options are:
- Reverse the branches in the spec.
    - This is ugly, the plugin details shouldn't influence the spec.
- Rewrite the primitive functions that produce booleans to produce spec booleans.
    - This is pretty bad codegen.
- Special case Bool to swap the order of the cases.

We take the least bad option, option 3.

The same problem arises for List. It's not in the spec, but the stdlib order (and the natural one)
is nil first and then cons, but ":" is less than "[]", so we end up with the wrong order. Again,
we just special case this.
-}

-- See Note [Ordering of constructors]
sortConstructors :: GHC.TyCon -> [GHC.DataCon] -> [GHC.DataCon]
sortConstructors :: TyCon -> [DataCon] -> [DataCon]
sortConstructors TyCon
tc [DataCon]
cs =
  -- note we compare on the OccName *not* the Name, as the latter compares on uniques,
  -- not the string name
  let sorted :: [DataCon]
sorted = (DataCon -> DataCon -> Ordering) -> [DataCon] -> [DataCon]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\DataCon
dc1 DataCon
dc2 -> OccName -> OccName -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (DataCon -> OccName
forall a. NamedThing a => a -> OccName
GHC.getOccName DataCon
dc1) (DataCon -> OccName
forall a. NamedThing a => a -> OccName
GHC.getOccName DataCon
dc2)) [DataCon]
cs
   in if TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
GHC.boolTyCon Bool -> Bool -> Bool
|| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
GHC.listTyCon then [DataCon] -> [DataCon]
forall a. [a] -> [a]
reverse [DataCon]
sorted else [DataCon]
sorted

getDataCons :: (Compiling uni fun m ann) => GHC.TyCon -> m [GHC.DataCon]
getDataCons :: forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
TyCon -> m [DataCon]
getDataCons TyCon
tc' = TyCon -> [DataCon] -> [DataCon]
sortConstructors TyCon
tc' ([DataCon] -> [DataCon]) -> m [DataCon] -> m [DataCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> m [DataCon]
forall {m :: * -> *} {uni :: * -> *} {fun} {ann}.
(MonadReader (CompileContext uni fun) m,
 MonadError (CompileError uni fun ann) m) =>
TyCon -> m [DataCon]
extractDcs TyCon
tc'
  where
    extractDcs :: TyCon -> m [DataCon]
extractDcs TyCon
tc
      | TyCon -> Bool
GHC.isAlgTyCon TyCon
tc Bool -> Bool -> Bool
|| TyCon -> Bool
GHC.isTupleTyCon TyCon
tc = case TyCon -> AlgTyConRhs
GHC.algTyConRhs TyCon
tc of
          AlgTyConRhs
GHC.AbstractTyCon ->
            (Text -> Error uni fun ann) -> SDoc -> m [DataCon]
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 [DataCon]) -> SDoc -> m [DataCon]
forall a b. (a -> b) -> a -> b
$
              SDoc
"Abstract type:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
GHC.<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr TyCon
tc
          GHC.DataTyCon{data_cons :: AlgTyConRhs -> [DataCon]
GHC.data_cons = [DataCon]
dcs} -> [DataCon] -> m [DataCon]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [DataCon]
dcs
          GHC.TupleTyCon{data_con :: AlgTyConRhs -> DataCon
GHC.data_con = DataCon
dc} -> [DataCon] -> m [DataCon]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [DataCon
dc]
          GHC.SumTyCon{data_cons :: AlgTyConRhs -> [DataCon]
GHC.data_cons = [DataCon]
dcs} -> [DataCon] -> m [DataCon]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [DataCon]
dcs
          GHC.NewTyCon{data_con :: AlgTyConRhs -> DataCon
GHC.data_con = DataCon
dc} -> [DataCon] -> m [DataCon]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [DataCon
dc]
      | TyCon -> Bool
GHC.isFamilyTyCon TyCon
tc =
          (Text -> Error uni fun ann) -> SDoc -> m [DataCon]
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 [DataCon]) -> SDoc -> m [DataCon]
forall a b. (a -> b) -> a -> b
$
            SDoc
"Irreducible type family application:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
GHC.<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr TyCon
tc
      | Bool
otherwise = (Text -> Error uni fun ann) -> SDoc -> m [DataCon]
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 [DataCon]) -> SDoc -> m [DataCon]
forall a b. (a -> b) -> a -> b
$ SDoc
"Type constructor:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
GHC.<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr TyCon
tc

{- Note [On data constructor workers and wrappers]
By default GHC has 'unbox-small-strict-fields' flag enabled.
This option causes all constructor fields which are marked strict and
which representation is smaller or equal to the size of a pointer to be unpacked.

Because of that we have to use 'dataConRepArgTys' for the constructor type
to get the argument types of the worker, not the wrapper.

That fixes the type mismatch problem when the GHC unpacks the field but we infer
the type of the original code without that information.
-}

{- | Makes the type of the constructor corresponding to the given 'DataCon', with the
type variables free.
-}
mkConstructorType :: (CompilingDefault uni fun m ann) => GHC.DataCon -> m (PIRType uni)
mkConstructorType :: forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
DataCon -> m (PIRType uni)
mkConstructorType DataCon
dc =
  -- see Note [On data constructor workers and wrappers]
  let argTys :: [Type]
argTys = Scaled Type -> Type
forall a. Scaled a -> a
GHC.scaledThing (Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCon -> [Scaled Type]
GHC.dataConRepArgTys DataCon
dc
   in -- See Note [Scott encoding of datatypes]
      Int -> SDoc -> m (PIRType uni) -> m (PIRType uni)
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
3 (SDoc
"Compiling data constructor type:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
GHC.<+> DataCon -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr DataCon
dc) (m (PIRType uni) -> m (PIRType uni))
-> m (PIRType uni) -> m (PIRType uni)
forall a b. (a -> b) -> a -> b
$ do
        [PIRType uni]
args <- (Type -> m (PIRType uni)) -> [Type] -> m [PIRType uni]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Type -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Type -> m (PIRType uni)
compileTypeNorm [Type]
argTys
        PIRType uni
resultType <- Type -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Type -> m (PIRType uni)
compileTypeNorm (DataCon -> Type
GHC.dataConOrigResTy DataCon
dc)
        -- t_c_i_1 -> ... -> t_c_i_j -> resultType
        PIRType uni -> m (PIRType uni)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PIRType uni -> m (PIRType uni)) -> PIRType uni -> m (PIRType uni)
forall a b. (a -> b) -> a -> b
$ Ann -> [PIRType uni] -> PIRType uni -> PIRType uni
forall ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
PIR.mkIterTyFun Ann
annMayInline [PIRType uni]
args PIRType uni
resultType

ghcStrictnessNote :: GHC.SDoc
ghcStrictnessNote :: SDoc
ghcStrictnessNote =
  SDoc
"Note: GHC can generate these unexpectedly, you may need"
    SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
GHC.<+> SDoc
"'-fno-strictness', '-fno-specialise', '-fno-spec-constr',"
    SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
GHC.<+> SDoc
"'-fno-unbox-strict-fields', or '-fno-unbox-small-strict-fields'."

-- | Get the constructors of the given 'TyCon' as PLC terms.
getConstructors :: (CompilingDefault uni fun m ann) => GHC.TyCon -> m [PIRTerm uni fun]
getConstructors :: forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
TyCon -> m [PIRTerm uni fun]
getConstructors TyCon
tc = do
  -- make sure the constructors have been created
  Type TyName DefaultUni Ann
_ <- TyCon -> m (Type TyName DefaultUni Ann)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
TyCon -> m (PIRType uni)
compileTyCon TyCon
tc
  Maybe [PIRTerm uni fun]
maybeConstrs <- Ann -> LexName -> m (Maybe [PIRTerm uni fun])
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
ann -> key -> m (Maybe [Term TyName Name uni fun ann])
PIR.lookupConstructors Ann
annMayInline (Name -> LexName
LexName (Name -> LexName) -> Name -> LexName
forall a b. (a -> b) -> a -> b
$ TyCon -> Name
forall a. NamedThing a => a -> Name
GHC.getName TyCon
tc)
  case Maybe [PIRTerm uni fun]
maybeConstrs of
    Just [PIRTerm uni fun]
constrs -> [PIRTerm uni fun] -> m [PIRTerm uni fun]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [PIRTerm uni fun]
constrs
    Maybe [PIRTerm uni fun]
Nothing ->
      (Text -> Error DefaultUni DefaultFun ann)
-> SDoc -> m [PIRTerm uni fun]
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 DefaultUni DefaultFun ann
forall (uni :: * -> *) fun a. Text -> Error uni fun a
UnsupportedError (SDoc -> m [PIRTerm uni fun]) -> SDoc -> m [PIRTerm uni fun]
forall a b. (a -> b) -> a -> b
$
        SDoc
"Cannot construct a value of type:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
GHC.<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr TyCon
tc SDoc -> SDoc -> SDoc
GHC.$+$ SDoc
ghcStrictnessNote

-- | Get the matcher of the given 'TyCon' as a PLC term
getMatch :: (CompilingDefault uni fun m ann) => GHC.TyCon -> m (PIRTerm uni fun)
getMatch :: forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
TyCon -> m (PIRTerm uni fun)
getMatch TyCon
tc = do
  -- ensure the tycon has been compiled, which will create the matcher
  Type TyName DefaultUni Ann
_ <- TyCon -> m (Type TyName DefaultUni Ann)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
TyCon -> m (PIRType uni)
compileTyCon TyCon
tc
  Maybe (PIRTerm uni fun)
maybeMatch <- Ann -> LexName -> m (Maybe (PIRTerm uni fun))
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
ann -> key -> m (Maybe (Term TyName Name uni fun ann))
PIR.lookupDestructor Ann
annMayInline (Name -> LexName
LexName (Name -> LexName) -> Name -> LexName
forall a b. (a -> b) -> a -> b
$ TyCon -> Name
forall a. NamedThing a => a -> Name
GHC.getName TyCon
tc)
  case Maybe (PIRTerm uni fun)
maybeMatch of
    Just PIRTerm uni fun
match -> PIRTerm uni fun -> m (PIRTerm uni fun)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PIRTerm uni fun
match
    Maybe (PIRTerm uni fun)
Nothing ->
      (Text -> Error DefaultUni DefaultFun ann)
-> SDoc -> m (PIRTerm uni fun)
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 DefaultUni DefaultFun ann
forall (uni :: * -> *) fun a. Text -> Error uni fun a
UnsupportedError (SDoc -> m (PIRTerm uni fun)) -> SDoc -> m (PIRTerm uni fun)
forall a b. (a -> b) -> a -> b
$
        SDoc
"Cannot case on a value on type:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
GHC.<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr TyCon
tc SDoc -> SDoc -> SDoc
GHC.$+$ SDoc
ghcStrictnessNote

{- | Get the matcher of the given 'Type' (which must be equal to a type constructor application)
as a PLC term instantiated for the type constructor argument types.
-}
getMatchInstantiated :: (CompilingDefault uni fun m ann) => GHC.Type -> m (PIRTerm uni fun)
getMatchInstantiated :: forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Type -> m (PIRTerm uni fun)
getMatchInstantiated Type
t =
  Int -> SDoc -> m (PIRTerm uni fun) -> m (PIRTerm uni fun)
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
3 (SDoc
"Creating instantiated matcher for type:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
GHC.<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr Type
t) (m (PIRTerm uni fun) -> m (PIRTerm uni fun))
-> m (PIRTerm uni fun) -> m (PIRTerm uni fun)
forall a b. (a -> b) -> a -> b
$ case Type
t of
    ((() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
GHC.splitTyConApp_maybe -> Just (TyCon
tc, [Type]
args)) -> do
      PIRTerm uni fun
match <- TyCon -> m (PIRTerm uni fun)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
TyCon -> m (PIRTerm uni fun)
getMatch TyCon
tc
      -- We drop 'RuntimeRep' arguments, see Note [Runtime reps]
      [Type TyName DefaultUni Ann]
args' <- (Type -> m (Type TyName DefaultUni Ann))
-> [Type] -> m [Type TyName DefaultUni Ann]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Type -> m (Type TyName DefaultUni Ann)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Type -> m (PIRType uni)
compileTypeNorm ([Type] -> [Type]
GHC.dropRuntimeRepArgs [Type]
args)
      PIRTerm uni fun -> m (PIRTerm uni fun)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PIRTerm uni fun -> m (PIRTerm uni fun))
-> PIRTerm uni fun -> m (PIRTerm uni fun)
forall a b. (a -> b) -> a -> b
$ PIRTerm uni fun
-> [(Ann, Type TyName DefaultUni Ann)] -> PIRTerm uni fun
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, Type tyname uni ann)] -> term ann
PIR.mkIterInst PIRTerm uni fun
match ([(Ann, Type TyName DefaultUni Ann)] -> PIRTerm uni fun)
-> [(Ann, Type TyName DefaultUni Ann)] -> PIRTerm uni fun
forall a b. (a -> b) -> a -> b
$ (Ann
annMayInline,) (Type TyName DefaultUni Ann -> (Ann, Type TyName DefaultUni Ann))
-> [Type TyName DefaultUni Ann]
-> [(Ann, Type TyName DefaultUni Ann)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type TyName DefaultUni Ann]
args'
    -- must be a TC app
    Type
_ ->
      (Text -> Error DefaultUni DefaultFun ann)
-> SDoc -> m (PIRTerm uni fun)
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 DefaultUni DefaultFun ann
forall (uni :: * -> *) fun a. Text -> Error uni fun a
CompilationError (SDoc -> m (PIRTerm uni fun)) -> SDoc -> m (PIRTerm uni fun)
forall a b. (a -> b) -> a -> b
$
        SDoc
"Cannot case on a value of a type which is not a datatype:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
GHC.<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
GHC.ppr Type
t

{- | Drops prefix of 'RuntimeRep' type variables (similar to 'dropRuntimeRepArgs').
Useful for e.g. dropping 'LiftedRep type variables arguments of unboxed tuple type applications:

  dropRuntimeRepVars [ k0, k1, a, b ] == [a, b]
-}
dropRuntimeRepVars :: [GHC.TyVar] -> [GHC.TyVar]
dropRuntimeRepVars :: [TyVar] -> [TyVar]
dropRuntimeRepVars = (TyVar -> Bool) -> [TyVar] -> [TyVar]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Type -> Bool
GHC.isRuntimeRepTy (Type -> Bool) -> (TyVar -> Type) -> TyVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
GHC.varType)