{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
module PlutusIR.Compiler.Datatype
( compileDatatype
, compileDatatypeDefs
, compileRecDatatypes
, mkDatatypeValueType
, mkDestructorTy
, mkScottTy
, resultTypeName
) where
import PlutusPrelude (showText)
import PlutusIR
import PlutusIR.Compiler.Names
import PlutusIR.Compiler.Provenance
import PlutusIR.Compiler.Types
import PlutusIR.Error
import PlutusIR.MkPir qualified as PIR
import PlutusIR.Transform.Substitute
import PlutusCore.Core qualified as PLC
import PlutusCore.MkPlc qualified as PLC
import PlutusCore.Quote
import PlutusCore.StdLib.Type qualified as Types
import Control.Monad.Error.Lens
import Data.Text qualified as T
import Data.Traversable
import Control.Lens hiding (index)
import Data.List.NonEmpty qualified as NE
import Data.Word (Word64)
constructorCaseType :: a -> Type tyname uni a -> VarDecl tyname name uni a -> Type tyname uni a
constructorCaseType :: forall a tyname (uni :: * -> *) name.
a
-> Type tyname uni a
-> VarDecl tyname name uni a
-> Type tyname uni a
constructorCaseType a
ann Type tyname uni a
resultType VarDecl tyname name uni a
vd = a -> [Type tyname uni a] -> Type tyname uni a -> Type tyname uni a
forall ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
PLC.mkIterTyFun a
ann (Type tyname uni a -> [Type tyname uni a]
forall tyname (uni :: * -> *) a.
Type tyname uni a -> [Type tyname uni a]
PLC.funTyArgs (VarDecl tyname name uni a -> Type tyname uni a
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> Type tyname uni ann
_varDeclType VarDecl tyname name uni a
vd)) Type tyname uni a
resultType
constructorArgTypes :: VarDecl tyname name uni a -> [Type tyname uni a]
constructorArgTypes :: forall tyname name (uni :: * -> *) a.
VarDecl tyname name uni a -> [Type tyname uni a]
constructorArgTypes = Type tyname uni a -> [Type tyname uni a]
forall tyname (uni :: * -> *) a.
Type tyname uni a -> [Type tyname uni a]
PLC.funTyArgs (Type tyname uni a -> [Type tyname uni a])
-> (VarDecl tyname name uni a -> Type tyname uni a)
-> VarDecl tyname name uni a
-> [Type tyname uni a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarDecl tyname name uni a -> Type tyname uni a
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> Type tyname uni ann
_varDeclType
unveilDatatype :: Eq tyname => Type tyname uni a -> Datatype tyname name uni a -> Type tyname uni a -> Type tyname uni a
unveilDatatype :: forall tyname (uni :: * -> *) a name.
Eq tyname =>
Type tyname uni a
-> Datatype tyname name uni a
-> Type tyname uni a
-> Type tyname uni a
unveilDatatype Type tyname uni a
dty (Datatype a
_ TyVarDecl tyname a
tn [TyVarDecl tyname a]
_ name
_ [VarDecl tyname name uni a]
_) = (tyname -> Maybe (Type tyname uni a))
-> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) ann.
(tyname -> Maybe (Type tyname uni ann))
-> Type tyname uni ann -> Type tyname uni ann
typeSubstTyNames (\tyname
n -> if tyname
n tyname -> tyname -> Bool
forall a. Eq a => a -> a -> Bool
== TyVarDecl tyname a -> tyname
forall tyname ann. TyVarDecl tyname ann -> tyname
_tyVarDeclName TyVarDecl tyname a
tn then Type tyname uni a -> Maybe (Type tyname uni a)
forall a. a -> Maybe a
Just Type tyname uni a
dty else Maybe (Type tyname uni a)
forall a. Maybe a
Nothing)
resultTypeName :: MonadQuote m => Datatype TyName Name uni a -> m TyName
resultTypeName :: forall (m :: * -> *) (uni :: * -> *) a.
MonadQuote m =>
Datatype TyName Name uni a -> m TyName
resultTypeName (Datatype a
_ TyVarDecl TyName a
tn [TyVarDecl TyName a]
_ Name
_ [VarDecl TyName Name uni a]
_) = Quote TyName -> m TyName
forall a. Quote a -> m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote TyName -> m TyName) -> Quote TyName -> m TyName
forall a b. (a -> b) -> a -> b
$ Text -> Quote TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName (Text -> Quote TyName) -> Text -> Quote TyName
forall a b. (a -> b) -> a -> b
$ Text
"out_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (Name -> Text
_nameText (Name -> Text) -> Name -> Text
forall a b. (a -> b) -> a -> b
$ TyName -> Name
unTyName (TyName -> Name) -> TyName -> Name
forall a b. (a -> b) -> a -> b
$ TyVarDecl TyName a -> TyName
forall tyname ann. TyVarDecl tyname ann -> tyname
_tyVarDeclName TyVarDecl TyName a
tn)
mkScottTy :: MonadQuote m => ann -> Datatype TyName Name uni ann -> m (Type TyName uni ann)
mkScottTy :: forall (m :: * -> *) ann (uni :: * -> *).
MonadQuote m =>
ann -> Datatype TyName Name uni ann -> m (Type TyName uni ann)
mkScottTy ann
ann d :: Datatype TyName Name uni ann
d@(Datatype ann
_ TyVarDecl TyName ann
_ [TyVarDecl TyName ann]
_ Name
_ [VarDecl TyName Name uni ann]
constrs) = do
TyName
res <- Datatype TyName Name uni ann -> m TyName
forall (m :: * -> *) (uni :: * -> *) a.
MonadQuote m =>
Datatype TyName Name uni a -> m TyName
resultTypeName Datatype TyName Name uni ann
d
let caseTys :: [Type TyName uni ann]
caseTys = (VarDecl TyName Name uni ann -> Type TyName uni ann)
-> [VarDecl TyName Name uni ann] -> [Type TyName uni ann]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ann
-> Type TyName uni ann
-> VarDecl TyName Name uni ann
-> Type TyName uni ann
forall a tyname (uni :: * -> *) name.
a
-> Type tyname uni a
-> VarDecl tyname name uni a
-> Type tyname uni a
constructorCaseType ann
ann (ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann TyName
res)) [VarDecl TyName Name uni ann]
constrs
Type TyName uni ann -> m (Type TyName uni ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni ann -> m (Type TyName uni ann))
-> Type TyName uni ann -> m (Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$
ann
-> TyName -> Kind ann -> Type TyName uni ann -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall ann
ann TyName
res (ann -> Kind ann
forall ann. ann -> Kind ann
Type ann
ann) (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann -> Type TyName uni ann
forall a b. (a -> b) -> a -> b
$
ann
-> [Type TyName uni ann]
-> Type TyName uni ann
-> Type TyName uni ann
forall ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
PIR.mkIterTyFun ann
ann [Type TyName uni ann]
caseTys (ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann TyName
res)
mkDatatypeSOPTy :: ann -> Datatype TyName Name uni ann -> Type TyName uni ann
mkDatatypeSOPTy :: forall ann (uni :: * -> *).
ann -> Datatype TyName Name uni ann -> Type TyName uni ann
mkDatatypeSOPTy ann
ann (Datatype ann
_ TyVarDecl TyName ann
_ [TyVarDecl TyName ann]
_ Name
_ [VarDecl TyName Name uni ann]
constrs) = ann -> [[Type TyName uni ann]] -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP ann
ann ((VarDecl TyName Name uni ann -> [Type TyName uni ann])
-> [VarDecl TyName Name uni ann] -> [[Type TyName uni ann]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VarDecl TyName Name uni ann -> [Type TyName uni ann]
forall tyname name (uni :: * -> *) a.
VarDecl tyname name uni a -> [Type tyname uni a]
constructorArgTypes [VarDecl TyName Name uni ann]
constrs)
mkPatternFunctorBody :: MonadQuote m => DatatypeCompilationOpts -> ann -> Datatype TyName Name uni ann -> m (Type TyName uni ann)
mkPatternFunctorBody :: forall (m :: * -> *) ann (uni :: * -> *).
MonadQuote m =>
DatatypeCompilationOpts
-> ann -> Datatype TyName Name uni ann -> m (Type TyName uni ann)
mkPatternFunctorBody DatatypeCompilationOpts
opts ann
ann Datatype TyName Name uni ann
d = case DatatypeCompilationOpts -> DatatypeStyle
_dcoStyle DatatypeCompilationOpts
opts of
DatatypeStyle
ScottEncoding -> ann -> Datatype TyName Name uni ann -> m (Type TyName uni ann)
forall (m :: * -> *) ann (uni :: * -> *).
MonadQuote m =>
ann -> Datatype TyName Name uni ann -> m (Type TyName uni ann)
mkScottTy ann
ann Datatype TyName Name uni ann
d
DatatypeStyle
SumsOfProducts -> Type TyName uni ann -> m (Type TyName uni ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni ann -> m (Type TyName uni ann))
-> Type TyName uni ann -> m (Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$ ann -> Datatype TyName Name uni ann -> Type TyName uni ann
forall ann (uni :: * -> *).
ann -> Datatype TyName Name uni ann -> Type TyName uni ann
mkDatatypeSOPTy ann
ann Datatype TyName Name uni ann
d
mkDatatypeType :: forall m uni fun a. MonadQuote m => DatatypeCompilationOpts -> Recursivity -> Datatype TyName Name uni (Provenance a) -> m (PLCRecType uni fun a)
mkDatatypeType :: forall (m :: * -> *) (uni :: * -> *) fun a.
MonadQuote m =>
DatatypeCompilationOpts
-> Recursivity
-> Datatype TyName Name uni (Provenance a)
-> m (PLCRecType uni fun a)
mkDatatypeType DatatypeCompilationOpts
opts Recursivity
r d :: Datatype TyName Name uni (Provenance a)
d@(Datatype Provenance a
ann TyVarDecl TyName (Provenance a)
tn [TyVarDecl TyName (Provenance a)]
tvs Name
_ [VarDecl TyName Name uni (Provenance a)]
_) = do
Type TyName uni (Provenance a)
pf <- DatatypeCompilationOpts
-> Provenance a
-> Datatype TyName Name uni (Provenance a)
-> m (Type TyName uni (Provenance a))
forall (m :: * -> *) ann (uni :: * -> *).
MonadQuote m =>
DatatypeCompilationOpts
-> ann -> Datatype TyName Name uni ann -> m (Type TyName uni ann)
mkPatternFunctorBody DatatypeCompilationOpts
opts Provenance a
ann Datatype TyName Name uni (Provenance a)
d
case Recursivity
r of
Recursivity
NonRec -> PLCRecType uni fun a -> m (PLCRecType uni fun a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PLCRecType uni fun a -> m (PLCRecType uni fun a))
-> PLCRecType uni fun a -> m (PLCRecType uni fun a)
forall a b. (a -> b) -> a -> b
$ Type TyName uni (Provenance a) -> PLCRecType uni fun a
forall (uni :: * -> *) fun a. PLCType uni a -> PLCRecType uni fun a
PlainType (Type TyName uni (Provenance a) -> PLCRecType uni fun a)
-> Type TyName uni (Provenance a) -> PLCRecType uni fun a
forall a b. (a -> b) -> a -> b
$ [TyVarDecl TyName (Provenance a)]
-> Type TyName uni (Provenance a) -> Type TyName uni (Provenance a)
forall tyname ann (uni :: * -> *).
[TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
PLC.mkIterTyLam [TyVarDecl TyName (Provenance a)]
tvs Type TyName uni (Provenance a)
pf
Recursivity
Rec -> do
RecursiveType uni fun (Provenance a) -> PLCRecType uni fun a
forall (uni :: * -> *) fun a.
RecursiveType uni fun (Provenance a) -> PLCRecType uni fun a
RecursiveType (RecursiveType uni fun (Provenance a) -> PLCRecType uni fun a)
-> m (RecursiveType uni fun (Provenance a))
-> m (PLCRecType uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Quote (RecursiveType uni fun (Provenance a))
-> m (RecursiveType uni fun (Provenance a))
forall a. Quote a -> m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote (RecursiveType uni fun (Provenance a))
-> m (RecursiveType uni fun (Provenance a)))
-> Quote (RecursiveType uni fun (Provenance a))
-> m (RecursiveType uni fun (Provenance a))
forall a b. (a -> b) -> a -> b
$ forall (uni :: * -> *) ann fun.
FromDataPieces uni ann (RecursiveType uni fun ann)
Types.makeRecursiveType @uni @(Provenance a) Provenance a
ann (TyVarDecl TyName (Provenance a) -> TyName
forall tyname ann. TyVarDecl tyname ann -> tyname
_tyVarDeclName TyVarDecl TyName (Provenance a)
tn) [TyVarDecl TyName (Provenance a)]
tvs Type TyName uni (Provenance a)
pf)
mkDatatypeValueType :: a -> Datatype TyName Name uni a -> Type TyName uni a
mkDatatypeValueType :: forall ann (uni :: * -> *).
ann -> Datatype TyName Name uni ann -> Type TyName uni ann
mkDatatypeValueType a
ann (Datatype a
_ TyVarDecl TyName a
tn [TyVarDecl TyName a]
tvs Name
_ [VarDecl TyName Name uni a]
_) = Type TyName uni a -> [(a, Type TyName uni a)] -> Type TyName uni a
forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> [(ann, Type tyname uni ann)] -> Type tyname uni ann
PIR.mkIterTyApp (a -> TyVarDecl TyName a -> Type TyName uni a
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
PIR.mkTyVar a
ann TyVarDecl TyName a
tn) ([(a, Type TyName uni a)] -> Type TyName uni a)
-> [(a, Type TyName uni a)] -> Type TyName uni a
forall a b. (a -> b) -> a -> b
$ (a
ann,) (Type TyName uni a -> (a, Type TyName uni a))
-> (TyVarDecl TyName a -> Type TyName uni a)
-> TyVarDecl TyName a
-> (a, Type TyName uni a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> TyVarDecl TyName a -> Type TyName uni a
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
PIR.mkTyVar a
ann (TyVarDecl TyName a -> (a, Type TyName uni a))
-> [TyVarDecl TyName a] -> [(a, Type TyName uni a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyVarDecl TyName a]
tvs
mkConstructorType :: Datatype TyName Name uni (Provenance a) -> VarDecl TyName Name uni (Provenance a) -> PIRType uni a
mkConstructorType :: forall (uni :: * -> *) a.
Datatype TyName Name uni (Provenance a)
-> VarDecl TyName Name uni (Provenance a) -> PIRType uni a
mkConstructorType (Datatype Provenance a
_ TyVarDecl TyName (Provenance a)
_ [TyVarDecl TyName (Provenance a)]
tvs Name
_ [VarDecl TyName Name uni (Provenance a)]
_) VarDecl TyName Name uni (Provenance a)
constr = [TyVarDecl TyName (Provenance a)]
-> Type TyName uni (Provenance a) -> Type TyName uni (Provenance a)
forall tyname ann (uni :: * -> *).
[TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
PIR.mkIterTyForall [TyVarDecl TyName (Provenance a)]
tvs (Type TyName uni (Provenance a) -> Type TyName uni (Provenance a))
-> Type TyName uni (Provenance a) -> Type TyName uni (Provenance a)
forall a b. (a -> b) -> a -> b
$ VarDecl TyName Name uni (Provenance a)
-> Type TyName uni (Provenance a)
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> Type tyname uni ann
_varDeclType VarDecl TyName Name uni (Provenance a)
constr
mkConstructor :: MonadQuote m => DatatypeCompilationOpts -> PLCRecType uni fun a -> Datatype TyName Name uni (Provenance a) -> Word64 -> m (PIRTerm uni fun a)
mkConstructor :: forall (m :: * -> *) (uni :: * -> *) fun a.
MonadQuote m =>
DatatypeCompilationOpts
-> PLCRecType uni fun a
-> Datatype TyName Name uni (Provenance a)
-> Word64
-> m (PIRTerm uni fun a)
mkConstructor DatatypeCompilationOpts
opts PLCRecType uni fun a
dty d :: Datatype TyName Name uni (Provenance a)
d@(Datatype Provenance a
ann TyVarDecl TyName (Provenance a)
_ [TyVarDecl TyName (Provenance a)]
tvs Name
_ [VarDecl TyName Name uni (Provenance a)]
constrs) Word64
index = do
let thisConstr :: VarDecl TyName Name uni (Provenance a)
thisConstr = [VarDecl TyName Name uni (Provenance a)]
constrs [VarDecl TyName Name uni (Provenance a)]
-> Int -> VarDecl TyName Name uni (Provenance a)
forall a. HasCallStack => [a] -> Int -> a
!! Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
index
[VarDecl TyName Name uni (Provenance a)]
argsAndTypes <- do
let argTypes :: [Type TyName uni (Provenance a)]
argTypes = Type TyName uni (Provenance a)
-> Datatype TyName Name uni (Provenance a)
-> Type TyName uni (Provenance a)
-> Type TyName uni (Provenance a)
forall tyname (uni :: * -> *) a name.
Eq tyname =>
Type tyname uni a
-> Datatype tyname name uni a
-> Type tyname uni a
-> Type tyname uni a
unveilDatatype (PLCRecType uni fun a -> Type TyName uni (Provenance a)
forall (uni :: * -> *) fun a. PLCRecType uni fun a -> PLCType uni a
getType PLCRecType uni fun a
dty) Datatype TyName Name uni (Provenance a)
d (Type TyName uni (Provenance a) -> Type TyName uni (Provenance a))
-> [Type TyName uni (Provenance a)]
-> [Type TyName uni (Provenance a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarDecl TyName Name uni (Provenance a)
-> [Type TyName uni (Provenance a)]
forall tyname name (uni :: * -> *) a.
VarDecl tyname name uni a -> [Type tyname uni a]
constructorArgTypes VarDecl TyName Name uni (Provenance a)
thisConstr
[Name]
argNames <- [Int] -> (Int -> m Name) -> m [Name]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Int
0..([Type TyName uni (Provenance a)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type TyName uni (Provenance a)]
argTypes Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] (\Int
i -> Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
safeFreshName (Text -> m Name) -> Text -> m Name
forall a b. (a -> b) -> a -> b
$ Text
"arg_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
showText Int
i)
[VarDecl TyName Name uni (Provenance a)]
-> m [VarDecl TyName Name uni (Provenance a)]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([VarDecl TyName Name uni (Provenance a)]
-> m [VarDecl TyName Name uni (Provenance a)])
-> [VarDecl TyName Name uni (Provenance a)]
-> m [VarDecl TyName Name uni (Provenance a)]
forall a b. (a -> b) -> a -> b
$ (Name
-> Type TyName uni (Provenance a)
-> VarDecl TyName Name uni (Provenance a))
-> [Name]
-> [Type TyName uni (Provenance a)]
-> [VarDecl TyName Name uni (Provenance a)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Provenance a
-> Name
-> Type TyName uni (Provenance a)
-> VarDecl TyName Name uni (Provenance a)
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl Provenance a
ann) [Name]
argNames [Type TyName uni (Provenance a)]
argTypes
PIRTerm uni fun a
constrBody <- case DatatypeCompilationOpts -> DatatypeStyle
_dcoStyle DatatypeCompilationOpts
opts of
DatatypeStyle
SumsOfProducts -> do
Type TyName uni (Provenance a)
pf <- DatatypeCompilationOpts
-> Provenance a
-> Datatype TyName Name uni (Provenance a)
-> m (Type TyName uni (Provenance a))
forall (m :: * -> *) ann (uni :: * -> *).
MonadQuote m =>
DatatypeCompilationOpts
-> ann -> Datatype TyName Name uni ann -> m (Type TyName uni ann)
mkPatternFunctorBody DatatypeCompilationOpts
opts Provenance a
ann Datatype TyName Name uni (Provenance a)
d
let unrolled :: Type TyName uni (Provenance a)
unrolled = Type TyName uni (Provenance a)
-> Datatype TyName Name uni (Provenance a)
-> Type TyName uni (Provenance a)
-> Type TyName uni (Provenance a)
forall tyname (uni :: * -> *) a name.
Eq tyname =>
Type tyname uni a
-> Datatype tyname name uni a
-> Type tyname uni a
-> Type tyname uni a
unveilDatatype (PLCRecType uni fun a -> Type TyName uni (Provenance a)
forall (uni :: * -> *) fun a. PLCRecType uni fun a -> PLCType uni a
getType PLCRecType uni fun a
dty) Datatype TyName Name uni (Provenance a)
d Type TyName uni (Provenance a)
pf
PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PIRTerm uni fun a -> m (PIRTerm uni fun a))
-> PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$ Provenance a
-> Type TyName uni (Provenance a)
-> Word64
-> [PIRTerm uni fun a]
-> PIRTerm uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Word64
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
Constr Provenance a
ann Type TyName uni (Provenance a)
unrolled Word64
index ((VarDecl TyName Name uni (Provenance a) -> PIRTerm uni fun a)
-> [VarDecl TyName Name uni (Provenance a)] -> [PIRTerm uni fun a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Provenance a
-> VarDecl TyName Name uni (Provenance a) -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni ann -> term ann
PIR.mkVar Provenance a
ann) [VarDecl TyName Name uni (Provenance a)]
argsAndTypes)
DatatypeStyle
ScottEncoding -> do
TyName
resultType <- Datatype TyName Name uni (Provenance a) -> m TyName
forall (m :: * -> *) (uni :: * -> *) a.
MonadQuote m =>
Datatype TyName Name uni a -> m TyName
resultTypeName Datatype TyName Name uni (Provenance a)
d
[VarDecl TyName Name uni (Provenance a)]
casesAndTypes <- do
let caseTypes :: [Type TyName uni (Provenance a)]
caseTypes = Type TyName uni (Provenance a)
-> Datatype TyName Name uni (Provenance a)
-> Type TyName uni (Provenance a)
-> Type TyName uni (Provenance a)
forall tyname (uni :: * -> *) a name.
Eq tyname =>
Type tyname uni a
-> Datatype tyname name uni a
-> Type tyname uni a
-> Type tyname uni a
unveilDatatype (PLCRecType uni fun a -> Type TyName uni (Provenance a)
forall (uni :: * -> *) fun a. PLCRecType uni fun a -> PLCType uni a
getType PLCRecType uni fun a
dty) Datatype TyName Name uni (Provenance a)
d (Type TyName uni (Provenance a) -> Type TyName uni (Provenance a))
-> [Type TyName uni (Provenance a)]
-> [Type TyName uni (Provenance a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VarDecl TyName Name uni (Provenance a)
-> Type TyName uni (Provenance a))
-> [VarDecl TyName Name uni (Provenance a)]
-> [Type TyName uni (Provenance a)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Provenance a
-> Type TyName uni (Provenance a)
-> VarDecl TyName Name uni (Provenance a)
-> Type TyName uni (Provenance a)
forall a tyname (uni :: * -> *) name.
a
-> Type tyname uni a
-> VarDecl tyname name uni a
-> Type tyname uni a
constructorCaseType Provenance a
ann (Provenance a -> TyName -> Type TyName uni (Provenance a)
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar Provenance a
ann TyName
resultType)) [VarDecl TyName Name uni (Provenance a)]
constrs
[Name]
caseArgNames <- [VarDecl TyName Name uni (Provenance a)]
-> (VarDecl TyName Name uni (Provenance a) -> m Name) -> m [Name]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [VarDecl TyName Name uni (Provenance a)]
constrs (\VarDecl TyName Name uni (Provenance a)
c -> Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
safeFreshName (Text -> m Name) -> Text -> m Name
forall a b. (a -> b) -> a -> b
$ Text
"case_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (VarDecl TyName Name uni (Provenance a) -> String
forall tyname (uni :: * -> *) a.
VarDecl tyname Name uni a -> String
varDeclNameString VarDecl TyName Name uni (Provenance a)
c))
[VarDecl TyName Name uni (Provenance a)]
-> m [VarDecl TyName Name uni (Provenance a)]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([VarDecl TyName Name uni (Provenance a)]
-> m [VarDecl TyName Name uni (Provenance a)])
-> [VarDecl TyName Name uni (Provenance a)]
-> m [VarDecl TyName Name uni (Provenance a)]
forall a b. (a -> b) -> a -> b
$ (Name
-> Type TyName uni (Provenance a)
-> VarDecl TyName Name uni (Provenance a))
-> [Name]
-> [Type TyName uni (Provenance a)]
-> [VarDecl TyName Name uni (Provenance a)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Provenance a
-> Name
-> Type TyName uni (Provenance a)
-> VarDecl TyName Name uni (Provenance a)
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl Provenance a
ann) [Name]
caseArgNames [Type TyName uni (Provenance a)]
caseTypes
let thisCase :: PIRTerm uni fun a
thisCase = Provenance a
-> VarDecl TyName Name uni (Provenance a) -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni ann -> term ann
PIR.mkVar Provenance a
ann (VarDecl TyName Name uni (Provenance a) -> PIRTerm uni fun a)
-> VarDecl TyName Name uni (Provenance a) -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$ [VarDecl TyName Name uni (Provenance a)]
casesAndTypes [VarDecl TyName Name uni (Provenance a)]
-> Int -> VarDecl TyName Name uni (Provenance a)
forall a. HasCallStack => [a] -> Int -> a
!! Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
index
PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PIRTerm uni fun a -> m (PIRTerm uni fun a))
-> PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$
Provenance a
-> TyName
-> Kind (Provenance a)
-> PIRTerm uni fun a
-> PIRTerm uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs Provenance a
ann TyName
resultType (Provenance a -> Kind (Provenance a)
forall ann. ann -> Kind ann
Type Provenance a
ann) (PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$
[VarDecl TyName Name uni (Provenance a)]
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni ann] -> term ann -> term ann
PIR.mkIterLamAbs [VarDecl TyName Name uni (Provenance a)]
casesAndTypes (PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$
PIRTerm uni fun a
-> [(Provenance a, PIRTerm uni fun a)] -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
PIR.mkIterApp PIRTerm uni fun a
thisCase ((VarDecl TyName Name uni (Provenance a)
-> (Provenance a, PIRTerm uni fun a))
-> [VarDecl TyName Name uni (Provenance a)]
-> [(Provenance a, PIRTerm uni fun a)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Provenance a
ann,) (PIRTerm uni fun a -> (Provenance a, PIRTerm uni fun a))
-> (VarDecl TyName Name uni (Provenance a) -> PIRTerm uni fun a)
-> VarDecl TyName Name uni (Provenance a)
-> (Provenance a, PIRTerm uni fun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Provenance a
-> VarDecl TyName Name uni (Provenance a) -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni ann -> term ann
PIR.mkVar Provenance a
ann) [VarDecl TyName Name uni (Provenance a)]
argsAndTypes)
let constr :: PIRTerm uni fun a
constr =
[TyVarDecl TyName (Provenance a)]
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[TyVarDecl tyname ann] -> term ann -> term ann
PIR.mkIterTyAbs [TyVarDecl TyName (Provenance a)]
tvs (PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$
[VarDecl TyName Name uni (Provenance a)]
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni ann] -> term ann -> term ann
PIR.mkIterLamAbs [VarDecl TyName Name uni (Provenance a)]
argsAndTypes (PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$
Provenance a
-> PLCRecType uni fun a
-> [Type TyName uni (Provenance a)]
-> PIRTerm uni fun a
-> PIRTerm uni fun a
forall a (uni :: * -> *) fun.
Provenance a
-> PLCRecType uni fun a
-> [PLCType uni a]
-> PIRTerm uni fun a
-> PIRTerm uni fun a
wrap Provenance a
ann PLCRecType uni fun a
dty ((TyVarDecl TyName (Provenance a) -> Type TyName uni (Provenance a))
-> [TyVarDecl TyName (Provenance a)]
-> [Type TyName uni (Provenance a)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Provenance a
-> TyVarDecl TyName (Provenance a)
-> Type TyName uni (Provenance a)
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
PIR.mkTyVar Provenance a
ann) [TyVarDecl TyName (Provenance a)]
tvs) PIRTerm uni fun a
constrBody
PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PIRTerm uni fun a -> m (PIRTerm uni fun a))
-> PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$ (Provenance a -> Provenance a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b.
(a -> b)
-> Term TyName Name uni fun a -> Term TyName Name uni fun b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Provenance a
a -> DatatypeComponent -> Provenance a -> Provenance a
forall a. DatatypeComponent -> Provenance a -> Provenance a
DatatypeComponent DatatypeComponent
Constructor Provenance a
a) PIRTerm uni fun a
constr
mkDestructor :: MonadQuote m => DatatypeCompilationOpts -> PLCRecType uni fun a -> Datatype TyName Name uni (Provenance a) -> m (PIRTerm uni fun a)
mkDestructor :: forall (m :: * -> *) (uni :: * -> *) fun a.
MonadQuote m =>
DatatypeCompilationOpts
-> PLCRecType uni fun a
-> Datatype TyName Name uni (Provenance a)
-> m (PIRTerm uni fun a)
mkDestructor DatatypeCompilationOpts
opts PLCRecType uni fun a
dty d :: Datatype TyName Name uni (Provenance a)
d@(Datatype Provenance a
ann TyVarDecl TyName (Provenance a)
_ [TyVarDecl TyName (Provenance a)]
tvs Name
_ [VarDecl TyName Name uni (Provenance a)]
constrs) = do
let appliedReal :: Type TyName uni (Provenance a)
appliedReal = Type TyName uni (Provenance a)
-> [(Provenance a, Type TyName uni (Provenance a))]
-> Type TyName uni (Provenance a)
forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> [(ann, Type tyname uni ann)] -> Type tyname uni ann
PIR.mkIterTyApp (PLCRecType uni fun a -> Type TyName uni (Provenance a)
forall (uni :: * -> *) fun a. PLCRecType uni fun a -> PLCType uni a
getType PLCRecType uni fun a
dty) ((TyVarDecl TyName (Provenance a)
-> (Provenance a, Type TyName uni (Provenance a)))
-> [TyVarDecl TyName (Provenance a)]
-> [(Provenance a, Type TyName uni (Provenance a))]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Provenance a
ann,) (Type TyName uni (Provenance a)
-> (Provenance a, Type TyName uni (Provenance a)))
-> (TyVarDecl TyName (Provenance a)
-> Type TyName uni (Provenance a))
-> TyVarDecl TyName (Provenance a)
-> (Provenance a, Type TyName uni (Provenance a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Provenance a
-> TyVarDecl TyName (Provenance a)
-> Type TyName uni (Provenance a)
forall ann tyname (uni :: * -> *).
ann -> TyVarDecl tyname ann -> Type tyname uni ann
PIR.mkTyVar Provenance a
ann) [TyVarDecl TyName (Provenance a)]
tvs)
Name
xn <- Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
safeFreshName Text
"x"
PIRTerm uni fun a
destrBody <- case DatatypeCompilationOpts -> DatatypeStyle
_dcoStyle DatatypeCompilationOpts
opts of
DatatypeStyle
SumsOfProducts -> do
TyName
resultType <- Datatype TyName Name uni (Provenance a) -> m TyName
forall (m :: * -> *) (uni :: * -> *) a.
MonadQuote m =>
Datatype TyName Name uni a -> m TyName
resultTypeName Datatype TyName Name uni (Provenance a)
d
[VarDecl TyName Name uni (Provenance a)]
caseVars <- [VarDecl TyName Name uni (Provenance a)]
-> (VarDecl TyName Name uni (Provenance a)
-> m (VarDecl TyName Name uni (Provenance a)))
-> m [VarDecl TyName Name uni (Provenance a)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [VarDecl TyName Name uni (Provenance a)]
constrs ((VarDecl TyName Name uni (Provenance a)
-> m (VarDecl TyName Name uni (Provenance a)))
-> m [VarDecl TyName Name uni (Provenance a)])
-> (VarDecl TyName Name uni (Provenance a)
-> m (VarDecl TyName Name uni (Provenance a)))
-> m [VarDecl TyName Name uni (Provenance a)]
forall a b. (a -> b) -> a -> b
$ \VarDecl TyName Name uni (Provenance a)
c -> do
let caseType :: Type TyName uni (Provenance a)
caseType = Provenance a
-> Type TyName uni (Provenance a)
-> VarDecl TyName Name uni (Provenance a)
-> Type TyName uni (Provenance a)
forall a tyname (uni :: * -> *) name.
a
-> Type tyname uni a
-> VarDecl tyname name uni a
-> Type tyname uni a
constructorCaseType Provenance a
ann (Provenance a -> TyName -> Type TyName uni (Provenance a)
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar Provenance a
ann TyName
resultType) VarDecl TyName Name uni (Provenance a)
c
unveiledCaseType :: Type TyName uni (Provenance a)
unveiledCaseType = Type TyName uni (Provenance a)
-> Datatype TyName Name uni (Provenance a)
-> Type TyName uni (Provenance a)
-> Type TyName uni (Provenance a)
forall tyname (uni :: * -> *) a name.
Eq tyname =>
Type tyname uni a
-> Datatype tyname name uni a
-> Type tyname uni a
-> Type tyname uni a
unveilDatatype (PLCRecType uni fun a -> Type TyName uni (Provenance a)
forall (uni :: * -> *) fun a. PLCRecType uni fun a -> PLCType uni a
getType PLCRecType uni fun a
dty) Datatype TyName Name uni (Provenance a)
d Type TyName uni (Provenance a)
caseType
Name
caseArgName <- Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
safeFreshName (Text -> m Name) -> Text -> m Name
forall a b. (a -> b) -> a -> b
$ Text
"case_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (VarDecl TyName Name uni (Provenance a) -> String
forall tyname (uni :: * -> *) a.
VarDecl tyname Name uni a -> String
varDeclNameString VarDecl TyName Name uni (Provenance a)
c)
VarDecl TyName Name uni (Provenance a)
-> m (VarDecl TyName Name uni (Provenance a))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni (Provenance a)
-> m (VarDecl TyName Name uni (Provenance a)))
-> VarDecl TyName Name uni (Provenance a)
-> m (VarDecl TyName Name uni (Provenance a))
forall a b. (a -> b) -> a -> b
$ Provenance a
-> Name
-> Type TyName uni (Provenance a)
-> VarDecl TyName Name uni (Provenance a)
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl Provenance a
ann Name
caseArgName Type TyName uni (Provenance a)
unveiledCaseType
PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PIRTerm uni fun a -> m (PIRTerm uni fun a))
-> PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$
Provenance a
-> TyName
-> Kind (Provenance a)
-> PIRTerm uni fun a
-> PIRTerm uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs Provenance a
ann TyName
resultType (Provenance a -> Kind (Provenance a)
forall ann. ann -> Kind ann
Type Provenance a
ann) (PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$
[VarDecl TyName Name uni (Provenance a)]
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni ann] -> term ann -> term ann
PIR.mkIterLamAbs [VarDecl TyName Name uni (Provenance a)]
caseVars (PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$
Provenance a
-> Type TyName uni (Provenance a)
-> PIRTerm uni fun a
-> [PIRTerm uni fun a]
-> PIRTerm uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Term tyname name uni fun a
-> [Term tyname name uni fun a]
-> Term tyname name uni fun a
Case Provenance a
ann (Provenance a -> TyName -> Type TyName uni (Provenance a)
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar Provenance a
ann TyName
resultType) (Provenance a
-> PLCRecType uni fun a -> PIRTerm uni fun a -> PIRTerm uni fun a
forall a (uni :: * -> *) fun.
Provenance a
-> PLCRecType uni fun a -> PIRTerm uni fun a -> PIRTerm uni fun a
unwrap Provenance a
ann PLCRecType uni fun a
dty (PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$ Provenance a -> Name -> PIRTerm uni fun a
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var Provenance a
ann Name
xn) ((VarDecl TyName Name uni (Provenance a) -> PIRTerm uni fun a)
-> [VarDecl TyName Name uni (Provenance a)] -> [PIRTerm uni fun a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Provenance a
-> VarDecl TyName Name uni (Provenance a) -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni ann -> term ann
PIR.mkVar Provenance a
ann) [VarDecl TyName Name uni (Provenance a)]
caseVars)
DatatypeStyle
ScottEncoding ->
PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PIRTerm uni fun a -> m (PIRTerm uni fun a))
-> PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$
Provenance a
-> PLCRecType uni fun a -> PIRTerm uni fun a -> PIRTerm uni fun a
forall a (uni :: * -> *) fun.
Provenance a
-> PLCRecType uni fun a -> PIRTerm uni fun a -> PIRTerm uni fun a
unwrap Provenance a
ann PLCRecType uni fun a
dty (PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$
Provenance a -> Name -> PIRTerm uni fun a
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var Provenance a
ann Name
xn
let destr :: PIRTerm uni fun a
destr =
[TyVarDecl TyName (Provenance a)]
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[TyVarDecl tyname ann] -> term ann -> term ann
PIR.mkIterTyAbs [TyVarDecl TyName (Provenance a)]
tvs (PIRTerm uni fun a -> PIRTerm uni fun a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall a b. (a -> b) -> a -> b
$
Provenance a
-> Name
-> Type TyName uni (Provenance a)
-> PIRTerm uni fun a
-> PIRTerm uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs Provenance a
ann Name
xn Type TyName uni (Provenance a)
appliedReal PIRTerm uni fun a
destrBody
PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PIRTerm uni fun a -> m (PIRTerm uni fun a))
-> PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$ DatatypeComponent -> Provenance a -> Provenance a
forall a. DatatypeComponent -> Provenance a -> Provenance a
DatatypeComponent DatatypeComponent
Destructor (Provenance a -> Provenance a)
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PIRTerm uni fun a
destr
mkDestructorTy :: MonadQuote m => Datatype TyName Name uni a -> m (Type TyName uni a)
mkDestructorTy :: forall (m :: * -> *) (uni :: * -> *) a.
MonadQuote m =>
Datatype TyName Name uni a -> m (Type TyName uni a)
mkDestructorTy dt :: Datatype TyName Name uni a
dt@(Datatype a
ann TyVarDecl TyName a
_ [TyVarDecl TyName a]
tvs Name
_ [VarDecl TyName Name uni a]
_) = do
Type TyName uni a
st <- a -> Datatype TyName Name uni a -> m (Type TyName uni a)
forall (m :: * -> *) ann (uni :: * -> *).
MonadQuote m =>
ann -> Datatype TyName Name uni ann -> m (Type TyName uni ann)
mkScottTy a
ann Datatype TyName Name uni a
dt
let valueType :: Type TyName uni a
valueType = a -> Datatype TyName Name uni a -> Type TyName uni a
forall ann (uni :: * -> *).
ann -> Datatype TyName Name uni ann -> Type TyName uni ann
mkDatatypeValueType a
ann Datatype TyName Name uni a
dt
Type TyName uni a -> m (Type TyName uni a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni a -> m (Type TyName uni a))
-> Type TyName uni a -> m (Type TyName uni a)
forall a b. (a -> b) -> a -> b
$ [TyVarDecl TyName a] -> Type TyName uni a -> Type TyName uni a
forall tyname ann (uni :: * -> *).
[TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
PIR.mkIterTyForall [TyVarDecl TyName a]
tvs (Type TyName uni a -> Type TyName uni a)
-> Type TyName uni a -> Type TyName uni a
forall a b. (a -> b) -> a -> b
$ a -> Type TyName uni a -> Type TyName uni a -> Type TyName uni a
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun a
ann Type TyName uni a
valueType Type TyName uni a
st
compileDatatype
:: Compiling m e uni fun a
=> Recursivity
-> PIRTerm uni fun a
-> Datatype TyName Name uni (Provenance a)
-> m (PIRTerm uni fun a)
compileDatatype :: forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
Recursivity
-> PIRTerm uni fun a
-> Datatype TyName Name uni (Provenance a)
-> m (PIRTerm uni fun a)
compileDatatype Recursivity
r PIRTerm uni fun a
body Datatype TyName Name uni (Provenance a)
d = do
DatatypeCompilationOpts
opts <- Getting
DatatypeCompilationOpts
(CompilationCtx uni fun a)
DatatypeCompilationOpts
-> m DatatypeCompilationOpts
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((CompilationOpts a
-> Const DatatypeCompilationOpts (CompilationOpts a))
-> CompilationCtx uni fun a
-> Const DatatypeCompilationOpts (CompilationCtx uni fun a)
forall (uni :: * -> *) fun a (f :: * -> *).
Functor f =>
(CompilationOpts a -> f (CompilationOpts a))
-> CompilationCtx uni fun a -> f (CompilationCtx uni fun a)
ccOpts ((CompilationOpts a
-> Const DatatypeCompilationOpts (CompilationOpts a))
-> CompilationCtx uni fun a
-> Const DatatypeCompilationOpts (CompilationCtx uni fun a))
-> ((DatatypeCompilationOpts
-> Const DatatypeCompilationOpts DatatypeCompilationOpts)
-> CompilationOpts a
-> Const DatatypeCompilationOpts (CompilationOpts a))
-> Getting
DatatypeCompilationOpts
(CompilationCtx uni fun a)
DatatypeCompilationOpts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DatatypeCompilationOpts
-> Const DatatypeCompilationOpts DatatypeCompilationOpts)
-> CompilationOpts a
-> Const DatatypeCompilationOpts (CompilationOpts a)
forall a (f :: * -> *).
Functor f =>
(DatatypeCompilationOpts -> f DatatypeCompilationOpts)
-> CompilationOpts a -> f (CompilationOpts a)
coDatatypes)
Provenance a
p <- m (Provenance a)
forall (uni :: * -> *) fun a (m :: * -> *).
MonadReader (CompilationCtx uni fun a) m =>
m (Provenance a)
getEnclosing
(Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
concreteTyDef, [Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)]
constrDefs, Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
destrDef) <- DatatypeCompilationOpts
-> Recursivity
-> Datatype TyName Name uni (Provenance a)
-> m (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a),
[Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)],
Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a))
forall (m :: * -> *) (uni :: * -> *) a fun.
MonadQuote m =>
DatatypeCompilationOpts
-> Recursivity
-> Datatype TyName Name uni (Provenance a)
-> m (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a),
[Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)],
Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a))
compileDatatypeDefs DatatypeCompilationOpts
opts Recursivity
r Datatype TyName Name uni (Provenance a)
d
let
tyVars :: [TyVarDecl TyName (Provenance a)]
tyVars = [Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
-> TyVarDecl TyName (Provenance a)
forall var val. Def var val -> var
PIR.defVar Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
concreteTyDef]
tys :: [PLCType uni a]
tys = [PLCRecType uni fun a -> PLCType uni a
forall (uni :: * -> *) fun a. PLCRecType uni fun a -> PLCType uni a
getType (PLCRecType uni fun a -> PLCType uni a)
-> PLCRecType uni fun a -> PLCType uni a
forall a b. (a -> b) -> a -> b
$ Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
-> PLCRecType uni fun a
forall var val. Def var val -> val
PIR.defVal Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
concreteTyDef]
vars :: [VarDecl TyName Name uni (Provenance a)]
vars = (Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
-> VarDecl TyName Name uni (Provenance a))
-> [Def
(VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)]
-> [VarDecl TyName Name uni (Provenance a)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
-> VarDecl TyName Name uni (Provenance a)
forall var val. Def var val -> var
PIR.defVar [Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)]
constrDefs [VarDecl TyName Name uni (Provenance a)]
-> [VarDecl TyName Name uni (Provenance a)]
-> [VarDecl TyName Name uni (Provenance a)]
forall a. [a] -> [a] -> [a]
++ [ Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
-> VarDecl TyName Name uni (Provenance a)
forall var val. Def var val -> var
PIR.defVar Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
destrDef ]
vals :: [PIRTerm uni fun a]
vals = (Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
-> PIRTerm uni fun a)
-> [Def
(VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)]
-> [PIRTerm uni fun a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
-> PIRTerm uni fun a
forall var val. Def var val -> val
PIR.defVal [Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)]
constrDefs [PIRTerm uni fun a] -> [PIRTerm uni fun a] -> [PIRTerm uni fun a]
forall a. [a] -> [a] -> [a]
++ [ Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
-> PIRTerm uni fun a
forall var val. Def var val -> val
PIR.defVal Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
destrDef ]
PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PIRTerm uni fun a -> m (PIRTerm uni fun a))
-> PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$
PIRTerm uni fun a
-> [(Provenance a, PIRTerm uni fun a)] -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
PIR.mkIterApp
(PIRTerm uni fun a
-> [(Provenance a, PLCType uni a)] -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, Type tyname uni ann)] -> term ann
PIR.mkIterInst ([TyVarDecl TyName (Provenance a)]
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[TyVarDecl tyname ann] -> term ann -> term ann
PIR.mkIterTyAbs [TyVarDecl TyName (Provenance a)]
tyVars ([VarDecl TyName Name uni (Provenance a)]
-> PIRTerm uni fun a -> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni ann] -> term ann -> term ann
PIR.mkIterLamAbs [VarDecl TyName Name uni (Provenance a)]
vars PIRTerm uni fun a
body)) ((Provenance a
p,) (PLCType uni a -> (Provenance a, PLCType uni a))
-> [PLCType uni a] -> [(Provenance a, PLCType uni a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PLCType uni a]
tys))
((Provenance a
p,) (PIRTerm uni fun a -> (Provenance a, PIRTerm uni fun a))
-> [PIRTerm uni fun a] -> [(Provenance a, PIRTerm uni fun a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PIRTerm uni fun a]
vals)
compileDatatypeDefs
:: MonadQuote m
=> DatatypeCompilationOpts
-> Recursivity
-> Datatype TyName Name uni (Provenance a)
-> m (PLC.Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a),
[PLC.Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)],
PLC.Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a))
compileDatatypeDefs :: forall (m :: * -> *) (uni :: * -> *) a fun.
MonadQuote m =>
DatatypeCompilationOpts
-> Recursivity
-> Datatype TyName Name uni (Provenance a)
-> m (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a),
[Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)],
Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a))
compileDatatypeDefs DatatypeCompilationOpts
opts Recursivity
r d :: Datatype TyName Name uni (Provenance a)
d@(Datatype Provenance a
ann TyVarDecl TyName (Provenance a)
tn [TyVarDecl TyName (Provenance a)]
_ Name
destr [VarDecl TyName Name uni (Provenance a)]
constrs) = do
Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
concreteTyDef <- TyVarDecl TyName (Provenance a)
-> PLCRecType uni fun a
-> Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
forall var val. var -> val -> Def var val
PIR.Def TyVarDecl TyName (Provenance a)
tn (PLCRecType uni fun a
-> Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a))
-> m (PLCRecType uni fun a)
-> m (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DatatypeCompilationOpts
-> Recursivity
-> Datatype TyName Name uni (Provenance a)
-> m (PLCRecType uni fun a)
forall (m :: * -> *) (uni :: * -> *) fun a.
MonadQuote m =>
DatatypeCompilationOpts
-> Recursivity
-> Datatype TyName Name uni (Provenance a)
-> m (PLCRecType uni fun a)
mkDatatypeType DatatypeCompilationOpts
opts Recursivity
r Datatype TyName Name uni (Provenance a)
d
[Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)]
constrDefs <- [(VarDecl TyName Name uni (Provenance a), Word64)]
-> ((VarDecl TyName Name uni (Provenance a), Word64)
-> m (Def
(VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)))
-> m [Def
(VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for ([VarDecl TyName Name uni (Provenance a)]
-> [Word64] -> [(VarDecl TyName Name uni (Provenance a), Word64)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VarDecl TyName Name uni (Provenance a)]
constrs [Word64
0..]) (((VarDecl TyName Name uni (Provenance a), Word64)
-> m (Def
(VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)))
-> m [Def
(VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)])
-> ((VarDecl TyName Name uni (Provenance a), Word64)
-> m (Def
(VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)))
-> m [Def
(VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)]
forall a b. (a -> b) -> a -> b
$ \(VarDecl TyName Name uni (Provenance a)
constr, Word64
i) -> do
let constrTy :: Type TyName uni (Provenance a)
constrTy = DatatypeComponent -> Provenance a -> Provenance a
forall a. DatatypeComponent -> Provenance a -> Provenance a
DatatypeComponent DatatypeComponent
ConstructorType (Provenance a -> Provenance a)
-> Type TyName uni (Provenance a) -> Type TyName uni (Provenance a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Datatype TyName Name uni (Provenance a)
-> VarDecl TyName Name uni (Provenance a)
-> Type TyName uni (Provenance a)
forall (uni :: * -> *) a.
Datatype TyName Name uni (Provenance a)
-> VarDecl TyName Name uni (Provenance a) -> PIRType uni a
mkConstructorType Datatype TyName Name uni (Provenance a)
d VarDecl TyName Name uni (Provenance a)
constr
PIRTerm uni fun a
c <- DatatypeCompilationOpts
-> PLCRecType uni fun a
-> Datatype TyName Name uni (Provenance a)
-> Word64
-> m (PIRTerm uni fun a)
forall (m :: * -> *) (uni :: * -> *) fun a.
MonadQuote m =>
DatatypeCompilationOpts
-> PLCRecType uni fun a
-> Datatype TyName Name uni (Provenance a)
-> Word64
-> m (PIRTerm uni fun a)
mkConstructor DatatypeCompilationOpts
opts (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
-> PLCRecType uni fun a
forall var val. Def var val -> val
PIR.defVal Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
concreteTyDef) Datatype TyName Name uni (Provenance a)
d Word64
i
Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
-> m (Def
(VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
-> m (Def
(VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)))
-> Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
-> m (Def
(VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a))
forall a b. (a -> b) -> a -> b
$ VarDecl TyName Name uni (Provenance a)
-> PIRTerm uni fun a
-> Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
forall var val. var -> val -> Def var val
PIR.Def (Provenance a
-> Name
-> Type TyName uni (Provenance a)
-> VarDecl TyName Name uni (Provenance a)
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl (DatatypeComponent -> Provenance a -> Provenance a
forall a. DatatypeComponent -> Provenance a -> Provenance a
DatatypeComponent DatatypeComponent
Constructor Provenance a
ann) (VarDecl TyName Name uni (Provenance a) -> Name
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> name
_varDeclName VarDecl TyName Name uni (Provenance a)
constr) Type TyName uni (Provenance a)
constrTy) PIRTerm uni fun a
c
Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
destrDef <- do
Type TyName uni (Provenance a)
destTy <- (Provenance a -> Provenance a)
-> Type TyName uni (Provenance a) -> Type TyName uni (Provenance a)
forall a b. (a -> b) -> Type TyName uni a -> Type TyName uni b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DatatypeComponent -> Provenance a -> Provenance a
forall a. DatatypeComponent -> Provenance a -> Provenance a
DatatypeComponent DatatypeComponent
DestructorType) (Type TyName uni (Provenance a) -> Type TyName uni (Provenance a))
-> m (Type TyName uni (Provenance a))
-> m (Type TyName uni (Provenance a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Datatype TyName Name uni (Provenance a)
-> m (Type TyName uni (Provenance a))
forall (m :: * -> *) (uni :: * -> *) a.
MonadQuote m =>
Datatype TyName Name uni a -> m (Type TyName uni a)
mkDestructorTy Datatype TyName Name uni (Provenance a)
d
PIRTerm uni fun a
t <- DatatypeCompilationOpts
-> PLCRecType uni fun a
-> Datatype TyName Name uni (Provenance a)
-> m (PIRTerm uni fun a)
forall (m :: * -> *) (uni :: * -> *) fun a.
MonadQuote m =>
DatatypeCompilationOpts
-> PLCRecType uni fun a
-> Datatype TyName Name uni (Provenance a)
-> m (PIRTerm uni fun a)
mkDestructor DatatypeCompilationOpts
opts (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
-> PLCRecType uni fun a
forall var val. Def var val -> val
PIR.defVal Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
concreteTyDef) Datatype TyName Name uni (Provenance a)
d
Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
-> m (Def
(VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
-> m (Def
(VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)))
-> Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
-> m (Def
(VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a))
forall a b. (a -> b) -> a -> b
$ VarDecl TyName Name uni (Provenance a)
-> PIRTerm uni fun a
-> Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
forall var val. var -> val -> Def var val
PIR.Def (Provenance a
-> Name
-> Type TyName uni (Provenance a)
-> VarDecl TyName Name uni (Provenance a)
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl (DatatypeComponent -> Provenance a -> Provenance a
forall a. DatatypeComponent -> Provenance a -> Provenance a
DatatypeComponent DatatypeComponent
Destructor Provenance a
ann) Name
destr Type TyName uni (Provenance a)
destTy) PIRTerm uni fun a
t
(Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a),
[Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)],
Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a))
-> m (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a),
[Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)],
Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Def (TyVarDecl TyName (Provenance a)) (PLCRecType uni fun a)
concreteTyDef, [Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)]
constrDefs, Def (VarDecl TyName Name uni (Provenance a)) (PIRTerm uni fun a)
destrDef)
compileRecDatatypes
:: Compiling m e uni fun a
=> PIRTerm uni fun a
-> NE.NonEmpty (Datatype TyName Name uni (Provenance a))
-> m (PIRTerm uni fun a)
compileRecDatatypes :: forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
PIRTerm uni fun a
-> NonEmpty (Datatype TyName Name uni (Provenance a))
-> m (PIRTerm uni fun a)
compileRecDatatypes PIRTerm uni fun a
body NonEmpty (Datatype TyName Name uni (Provenance a))
ds = case NonEmpty (Datatype TyName Name uni (Provenance a))
ds of
Datatype TyName Name uni (Provenance a)
d NE.:| [] -> Recursivity
-> PIRTerm uni fun a
-> Datatype TyName Name uni (Provenance a)
-> m (PIRTerm uni fun a)
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
Recursivity
-> PIRTerm uni fun a
-> Datatype TyName Name uni (Provenance a)
-> m (PIRTerm uni fun a)
compileDatatype Recursivity
Rec PIRTerm uni fun a
body Datatype TyName Name uni (Provenance a)
d
NonEmpty (Datatype TyName Name uni (Provenance a))
_ -> do
Provenance a
p <- m (Provenance a)
forall (uni :: * -> *) fun a (m :: * -> *).
MonadReader (CompilationCtx uni fun a) m =>
m (Provenance a)
getEnclosing
AReview e (Error uni fun (Provenance a))
-> Error uni fun (Provenance a) -> m (PIRTerm uni fun a)
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview e (Error uni fun (Provenance a))
forall r (uni :: * -> *) fun a.
AsError r uni fun a =>
Prism' r (Error uni fun a)
Prism' e (Error uni fun (Provenance a))
_Error (Error uni fun (Provenance a) -> m (PIRTerm uni fun a))
-> Error uni fun (Provenance a) -> m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$ Provenance a -> Text -> Error uni fun (Provenance a)
forall (uni :: * -> *) fun a. a -> Text -> Error uni fun a
UnsupportedError Provenance a
p Text
"Mutually recursive datatypes"