-- editorconfig-checker-disable-file
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections     #-}
{-# LANGUAGE TypeApplications  #-}
-- | Functions for compiling let-bound PIR datatypes into PLC.
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)

{- Note [Normalization of data-constructors' types]

Currently the typechecking and compilation of dataconstructors/destructor
assume that the data-constructors' types (of the parsed PIR input) are in normalized form.
If these types are not normalized, the compilation will generate failing plc code.

There are no checks in place to enforce this normalization, and while
plutus-tx plugin is unlikely to generate PIR code with unnormalized types inside
these dataconstructor locations, it may still need to be taken into account in
the unlikely case that a user has manually modified the PIR input.

Future solutions:

1) disallow unnormalized types in dataconstructors, by adding a "isNormalized" check  prior to compilation.
2) allow unnormalized types in dataconstructors and normalize them prior to compilation.
-}

-- Utilities

-- | Given the type of a constructor, get the type of the "case" type with the given result type.
-- @constructorCaseType R (A->Maybe A) = (A -> R)@
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

-- | Given the type of a constructor, get its argument types.
-- @constructorArgTypes (A->Maybe A) = [A]
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

-- | "Unveil" a datatype definition in a type, by replacing uses of the name as a type variable with the concrete definition.
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)

-- Datatypes

{- Note [Encoding of datatypes]
PIR datatypes must be encoded into PLC. We support two schemes for doing this:
- Scott encoding (see Note [Scott encoding of datatypes] for details)
- Sums-of-products (SOPs) (See Note [SOP encoding of datatypes] for details)

Scott encoding is what we used originally, before we had SOPs. We still support both
modes, because users targeting older versions of the language can't use the SOP
encoding. Otherwise, the SOP encoding is superior (faster, simpler).
-}

{- Note [Scott encoding of datatypes]
We can translate our datatypes using the Scott encoding. The fundamental idea is that there is one thing
you can do with a datatype value: pattern match on it. A datatype value is therefore represented by
precisely the thing you need to do a pattern match. Namely, a function that takes functions implementing
each arm of the match, and then gives you a result.

We also need to think about the types. In general, we need:
- The encoded type corresponding to the datatype itself
- The encoded type of each constructor
- The encoded term for each constructor
- The encoded type of the destructor
- The encoded term for the destructor

-- Basic example

For example, consider 'data Maybe a = Nothing | Just a'. Then:
- The type corresponding to the datatype is:
  Maybe = \(t :: *) . forall (out_Maybe :: *) . out_Maybe -> (t -> out_Maybe) -> out_Maybe
- The type of the constructors are:
  Just : forall (t :: *) . t -> Maybe t
  Nothing : forall (t :: *) . Maybe t
- The terms for the constructors are:
  Just = /\ (t :: *) \(x : t) /\ (out_Maybe :: *) \(case_Nothing : out_Maybe) (case_Just : t -> out_Maybe) . case_Just x
  Nothing = /\ (t :: *) /\ (out_Maybe :: *) \(case_Nothing : out_Maybe) (case_Just : t -> out_Maybe) . case_Nothing
- The type of the destructor is:
  match_Maybe : forall (t :: *) . Maybe t -> forall (out_Maybe :: *) . out_Maybe -> (t -> out_Maybe) -> out_Maybe
- The term for the destructor is:
  match_Maybe = /\(t :: *) \(x : Maybe t) . x

-- General case

Consider a datatype as defined in Plutus IR:
(datatype
  (tyvardecl T (type))
  (tyvardecl t_0 k_0)
  ..
  (tyvardecl t_n k_n)
  match_T
  (vardecl c_0 (fun t_c_0_0 .. (fun t_c_0_(c_0_k)) [T t0 .. tn]))
  ..
  (vardecl c_j (fun t_c_j_0 .. (fun t_c_j_(c_j_k)) [T t0 .. tn]))
)

That is, it has:
- Name T
- Type parameters t_0 to t_n of kind k_0 to k_n
- Kind * -> ... n times ... -> *
- Destructor match_t
_ Constructors c_0 to c_j with the arguments of c_i having types t_c_i_1 to t_c_i_(c_i_k)

The type corresponding to the datatype is:
\(t_0 :: k_0) .. (t_n :: k_n) .
  forall out_T :: * .
    (t_c_0_0 -> .. -> t_c_0_(c_0_k) -> out_T) -> .. -> (t_c_j_0 -> .. -> t_c_j_(c_j_k) -> out_T) ->
      out_T

The type of the constructor c_i (0 <= i <= j) is:
forall (t_0 :: k_0) .. (t_n :: k_n) .
  t_c_i_0 -> .. -> t_c_i_(c_i_k) ->
    (T t_0 .. t_n)
This is actually declared for us in the datatype declaration, but without the type
variables being abstracted out. We use this to get the argument types of the constructor.

The term for the constructor c_i (0 <= i <= j) is (slightly fudged types, see Note [Abstract data types]):
/\(t_0 :: k_0) .. (t_n :: k_n) .
  \(x_0 : t_c_i_0) .. (x_(c_i_k) : t_c_i_(c_i_k)) .
    /\(out_T :: *) .
      \(case_c_0 : (t_c_0_0 -> .. -> t_c_0_(c_0_k) -> out_T)) .. (case_c_j : (t_c_j_0 -> .. -> t_c_j_(c_j_k) -> out_T)) .
        case_c_i x_0 .. x_(c_i_k)

The type of the destructor is:
forall (t_0 :: k_0) .. (t_n :: k_n) .
  (T t_0 .. t_n) ->
    forall out_T :: * .
      (t_c_0_0 -> .. -> t_c_0_(c_0_k) -> out_T) -> .. -> (t_c_j_0 -> .. -> t_c_j_(c_j_k) -> out_T) ->
        out_T

The term for the destructor is (slightly fudged types, see Note [Abstract data types]):
/\(t_0 :: k_0) .. (t_n :: k_n) .
  \(x :: (T t_0 .. t_n)) .
    x
-}

{- Note [SOP encoding of datatypes]
We can translate our datatypes using SOPs. This is much more direct than Scott encoding, since
we have terms in the language for construction and destruction themselves.

We still need to think about the types. In general, we need:
- The encoded type corresponding to the datatype itself
- The encoded type of each constructor
- The encoded term for each constructor
- The encoded type of the destructor
- The encoded term for the destructor

-- Basic example

For example, consider 'data Maybe a = Nothing | Just a'. Then:
- The type corresponding to the datatype is:
  Maybe = \(a :: *) . sop [] [a]
- The type of the constructors are:
  Nothing : forall (a :: *) . Maybe a
  Just    : forall (a :: *) . a -> Maybe a
- The terms for the constructors are:
  Nothing =           /\(a :: *) . constr 0 (Maybe a)
  Just    = /\(a :: *) \(x :: a) . constr 1 (Maybe a) x
- The type of the destructor is:
  match_Maybe :: forall (a :: *) . Maybe a -> forall (out_Maybe :: *) . out_Maybe -> (a -> out_Maybe) -> out_Maybe
- The term for the destructor is:
  match_Maybe = /\(a :: *) \(x : Maybe a) /\(out_Maybe :: *) \(case_Nothing :: out_Maybe) (case_Just :: a -> out_Maybe) .
    case out_Maybe x case_Nothing case_Just

-- General case

Consider a datatype as defined in Plutus IR:
(datatype
  (tyvardecl T (type))
  (tyvardecl t_0 k_0)
  ..
  (tyvardecl t_n k_n)
  match_T
  (vardecl c_0 (fun t_c_0_0 .. (fun t_c_0_(c_0_k)) [T t0 .. tn]))
  ..
  (vardecl c_j (fun t_c_j_0 .. (fun t_c_j_(c_j_k)) [T t0 .. tn]))
)

That is, it has:
- Name T
- Type parameters t_0 to t_n of kind k_0 to k_n
- Kind * -> ... n times .. -> *
- Destructor match_T
_ Constructors c_0 to c_j with the arguments of c_i having types t_c_i_0 to t_c_i_(c_i_k)

The type corresponding to the datatype is:
\(t_0 :: k_0) .. (t_n :: k_n) . sop [t_c_0_0 .. t_c_0_(c_0_k)] .. [t_c_j_0 .. t_c_j_(c_j_k)]

The type of the constructor c_i (0 <= i <= j) is:
forall (t_0 :: t_0) .. (t_n :: k_n) .
  t_c_i_0 -> .. -> t_c_i_(c_i_k) ->
    (T t_0 .. t_n)
This is actually declared for us in the datatype declaration, but without the type
variables being abstracted out. We use this to get the argument types of the constructor.

The term for the constructor c_i (0 <= i <= j) is (slightly fudged types, see Note [Abstract data types]):
/\(t_0 :: t_0) .. (t_n :: k_n) .
  \(x_0 : t_c_i_0) .. (x_(c_i_k) : t_c_i_(c_i_k)) .
    constr (T t_0 .. t_n) i (T t_0 .. t_n) x_0 .. x_(c_i_k)

The type of the destructor is:
forall (t_0 :: k_0) .. (t_n :: k_n) .
  (T t_0 .. t_n) ->
    forall out_T :: * .
      (t_c_0_1 -> .. -> t_c_0_(c_0_k) -> out_T) -> .. -> (t_c_j_0 -> .. -> t_c_j_(c_j_k) -> out_T) ->
        out_T

The term for the destructor is (slightly fudged types, see Note [Abstract data types]):
/\(t_0 :: k_0) .. (t_n :: k_n) .
  \(x :: (T t_0 .. t_n)) .
    /\(out_T :: *) .
      \(case_c_0 : (t_c_0_0 -> .. -> t_c_0_(c_0_k) -> out_T)) .. (case_c_j : (t_c_j_0 -> .. -> t_c_j_(c_j_k) -> out_T)) .
        case out_T x case_c_0 .. case_c_j
-}

{- Note [Compiling uses of datatypes]

We turn constructor invocations into calls to the constructor functions.

Pattern matching is slightly more complex as we need to turn it into an invocation of the destructor:
- We take each alternative, turn it into a function of its bound variables.
- We apply the destructor to the scrutinee, and then instantiate that (which will be polymorphic
  in the result type) at the type of the overall match expression.
    - This does indicate one wrinkle: we need to know the overall type, we can't infer it.
- We apply the instantiated value to the functions for each alternative.
-}

{- Note [Abstract data types]
While the Scott encoding makes it easy to simply convert all types inline, it
is convenient for a number of reasons to instead abstract out data types. Namely:
- The resulting code is much more readable, since we have named types instead
of (potentially big) inlined types.
- We generate less code because we're not repeating the definition at every use site.

The basic idea is to "let-bind" types using type abstractions, and values using
lambda abstractions. There are a few considerations that make this tricky, however:

1. When types are inlined, the Scott encoding allows us to construct values by
  constructing the matching function inline. When they are abstract, we need to provide
  (suitably polymorphic) constructors abstractly.
2. When types are inlined, the Scott encoding allows us to match against a type by
  simply using it as a function. When they are abstract, we need to provide a
  (suitably polymorphic) matching function abstractly.
3. The definition of a type must be abstract in the binding types of the constructors and destructors
  (so they can be used alongside the abstract type), but it must *not* be abstract in the
  *definition* of the constructors or destructors, because they depend on knowing the real structure
  of the type.
    1. In fact we can do slightly better than this: in the constructors of a recursive datatype we can use the type
       as a name inside the 'wrap'.

Consequently, for a single type we end up with something like the following:

(/\ ty :: * .
  -- ty abstract in these types
  \(c_1 : <constructor type i>) .. (c_j : <constructor type j>) .
    -- ty abstract in this type
    \match : <destructor type> .
      <user term>
)
<defn of ty>
-- ty concrete in these terms, except maybe inside a 'wrap'
<defn of c_1>
..
<defn of c_j>
-- ty concrete in this term
<defn of match>

(see Note [Encoding of datatypes] for how the actual definitions are constructed)
-}

{- Note [Recursive datatypes]
Recursive data types make the scheme described in [Encoding of datatypes] a bit more
complex. At the moment we only support self-recursive datatypes.

For a (self-)recursive datatype we have to change three things:
- The type of the datatype itself must have an enclosing fix over the type variable for
  the type itself.
- Constructors must include a wrap.
- Destructors must include an unwrap.
-}

-- See Note [Encoding of datatypes]
-- | Make the "Scott-encoded" type for a 'Datatype', with type variables free.
-- This is exactly the type of an eliminator function for the datatype.
--
-- @mkScottTy Maybe = forall out_Maybe. out_Maybe -> (a -> out_Maybe) -> out_Maybe@
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
   -- FIXME: normalize datacons' types also here
   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
$
      -- forall res.
      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
$
      -- c_1 -> .. -> c_n -> res
      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)

{- | Make the body of the "pattern functor" of a 'Datatype'. This is just the non-abstract datatype type,
but with the type variable for the type itself free and its type variables free.

Scott: @mkPatternFunctorBody List = forall (out_List :: *) . out_List -> (a -> List a -> out_List) -> out_List@
SOPs: @mkPatternFunctorBody List = sop [] [a, List a]@
-}
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

{- | Make the real PLC type corresponding to a 'Datatype' with the given pattern functor body.

Scott:
@
    mkDatatypeType List <pattern functor body of List>
        = fix (\(List :: * -> *) (a :: *) -> <pattern functor body of List>)
        = fix (\(List :: * -> *) (a :: *) -> forall (r :: *) . r -> (a -> List a -> r) -> r)
@

SOPs:
@
    mkDatatypeType List <pattern functor of List>
        = fix (\(List :: * -> *) (a :: *) -> <pattern functor body of List>)
        = fix (\(List :: * -> *) (a :: *) -> \(a :: *) -> sop [] [a, List a])
@
-}
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
    -- See Note [Recursive datatypes]
    -- We are reusing the same type name for the fixpoint variable. This is fine
    -- so long as we do renaming later, since we only reuse the name inside an inner binder
    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)

-- | The type of a datatype-value is of the form `[TyCon tyarg1 tyarg2 ... tyargn]`
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

-- Constructors

{- | Make the type of a constructor of a 'Datatype'. This is not quite the same as the declared type because the declared type has the
type variables free.
@
    mkConstructorType List Cons = forall (a :: *) . a -> List a -> List a
@
-}
mkConstructorType :: Datatype TyName Name uni (Provenance a) -> VarDecl TyName Name uni (Provenance a) -> PIRType uni a
-- this type appears *inside* the scope of the abstraction for the datatype so we can just reference the name and
-- we don't need to do anything to the declared type
-- see Note [Abstract data types]
-- FIXME: normalize constructors also here
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

-- See Note [Encoding of datatypes]
{- | Make a constructor of a 'Datatype' with the given pattern functor. The constructor argument mostly serves to identify the constructor
that we are interested in in the list of constructors.

Scott:
@
    mkConstructor <definition of List> List Cons
        = /\(a :: *) . \(x : a) (xs : <definition of List> a) .
            wrap <pattern functor of List> /\(out_List :: *) .
                \(case_Nil : out_List) (case_Cons : a -> List a -> out_List) . case_Cons arg1 arg2
@

SOPs:
@
    mkConstructor <definition of List> List Cons
        = /\(a :: *) . \(x : a) (xs : <definition of List> a) .
            wrap <pattern functor of List>
                constr ((\(List :: * -> *) . <pattern functor of List>) <definition of List>) arg1 arg2
@
-}
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
    -- This is inelegant, but it should never fail
    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

    -- constructor args and their types
    [VarDecl TyName Name uni (Provenance a)]
argsAndTypes <- do
        -- these types appear *outside* the scope of the abstraction for the datatype, so we need to use the concrete datatype here
        -- see Note [Abstract data types]
        -- FIXME: normalize datacons' types also here
        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
        -- we don't have any names for these things, we just had the type, so we call them "arg_i
        [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
            -- We have to be a bit careful annotating the type of the constr. It is inside the 'wrap' so it
            -- needs to be one level "unrolled".

            -- The pattern functor with a hole in it
            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
            -- ... and with the hole filled in with the datatype type
            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

            -- case arguments and their types
            [VarDecl TyName Name uni (Provenance a)]
casesAndTypes <- do
                  -- these types appear *outside* the scope of the abstraction for the datatype, so we need to use the concrete datatype here
                  -- see Note [Abstract data types]
                  -- FIXME: normalize datacons' types also here
                  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

            -- This is inelegant, but it should never fail
            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
$
                -- forall out
                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
$
                -- \case_1 .. case_j
                [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
$
                -- c_i arg_1 .. arg_m
                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 =
            -- /\t_1 .. t_n
            [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
$
            -- \arg_1 .. arg_m
            [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
$
            -- See Note [Recursive datatypes]
            -- wrap
            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

-- Destructors

-- See Note [Encoding of datatypes]
{- | Make the destructor for a 'Datatype'.

Scott:
@
    mkDestructor <definition of List> List
       = /\(a :: *) -> \(x : (<definition of List> a)) -> unwrap x
@

SOPs:
@
    mkDestructor <definition of List> List
       = /\(a :: *) -> \(x : (<definition of List> a)) ->
         /\(r :: *) ->
         \(case_Nil :: r) (case_Cons :: a -> (<definition of List> a) -> r) -> case r (unwrap x) case_Nil case_Cons
@
-}
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
    -- This term appears *outside* the scope of the abstraction for the datatype, so we need to put in the Scott-encoded type here
    -- see Note [Abstract data types]
    -- dty t_1 .. t_n
    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
            -- Variables for case arguments, and the bodies to be used as the actual cases
            [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
                -- these types appear *outside* the scope of the abstraction for the datatype, so we need to use the concrete datatype here
                -- see Note [Abstract data types]
                -- FIXME: normalize datacons' types also here
                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
$
                -- forall out
                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
$
                -- \case_1 .. case_j
                [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
$
                -- See Note [Recursive datatypes]
                -- case (unwrap x) case_1 .. case_j
                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
$
                -- See Note [Recursive datatypes]
                -- unwrap
                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 =
            -- /\t_1 .. t_n
            [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
$
            -- \x
            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

-- See Note [Encoding of datatypes]
-- | Make the type of a destructor for a 'Datatype'.
-- @
--     mkDestructorTy List
--         = forall (a :: *) . List a -> forall (out_List :: *) . (out_List -> (a -> List a -> out_List) -> out_List)
-- @
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
    -- The scott type is exactly the eliminator type, which is what we want here regardless of the compilation style
    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
    -- these types appear *inside* the scope of the abstraction for the datatype, so we can just directly use
    -- references to the name
    -- see Note [Abstract data types]
    -- t t_1 .. t_n
    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
    -- forall t_1 .. t_n
    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

-- The main function

-- | Compile a 'Datatype' bound with the given body.
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 ]
    -- See Note [Abstract data types]
    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)

-- | Compile a 'Datatype' to a triple of type-constructor, data-constructors, destructor definitions.
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"