{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}
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
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
#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'
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
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
(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
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)) ->
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)
(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
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
(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
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
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
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)
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
[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
sortConstructors :: GHC.TyCon -> [GHC.DataCon] -> [GHC.DataCon]
sortConstructors :: TyCon -> [DataCon] -> [DataCon]
sortConstructors TyCon
tc [DataCon]
cs =
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
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 =
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
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)
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'."
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
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
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
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
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
[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'
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
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)