{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE OverloadedStrings #-}
-- | Functions for compiling PIR let terms.
module PlutusIR.Compiler.Let (compileLets, LetKind(..)) where

import PlutusIR
import PlutusIR.Compiler.Datatype
import PlutusIR.Compiler.Definitions
import PlutusIR.Compiler.Provenance
import PlutusIR.Compiler.Recursion
import PlutusIR.Compiler.Types
import PlutusIR.Error
import PlutusIR.MkPir qualified as PIR

import Control.Monad
import Control.Monad.Error.Lens
import Control.Monad.Trans

import Control.Lens hiding (Strict)

import Data.List.NonEmpty hiding (partition, reverse)
import Data.List.NonEmpty qualified as NE

{- Note [Extra definitions while compiling let-bindings]
The let-compiling passes can generate some additional definitions, so we use the
support from 'Definitions' to ease this.

Specifically, only the recursive term pass should do this (it helps to share fixpoint combinators).
So putting in the definitions should mostly be a no-op, and we'll get errors if it's not.
It would be more elegant to somehow indicate that only one of the let-compiling passes needs
this, but this does the job.
Also we should pull out more stuff (e.g. see 'NonStrict' which uses unit).
-}

{- Note [Right-associative compilation of let-bindings for linear scoping]

The 'foldM' function for lists is left-associative, but we need right-associative for our case, i.e.
every right let must be wrapped/scoped by its left let

An pseudocode PIR example:
let b1 = rhs1;
    b2 = rhs2  (b1 is visible in rhs2);
in ...

must be treated the same as let b1 = rhs in (let b2 = rhs2 in ... )

Since there is no 'foldrM' in the stdlib, so we first reverse the bindings list,
and then apply the left-associative 'foldM' on them,
which yields the same results as doing a right-associative fold.
-}

data LetKind = RecTerms | NonRecTerms | Types | DataTypes

-- | Compile the let terms out of a 'Term'. Note: the result does *not* have globally unique names.
compileLets :: Compiling m e uni fun a => LetKind -> PIRTerm uni fun a -> m (PIRTerm uni fun a)
compileLets :: LetKind -> PIRTerm uni fun a -> m (PIRTerm uni fun a)
compileLets LetKind
kind PIRTerm uni fun a
t = m (Provenance a)
forall (uni :: * -> *) fun a (m :: * -> *).
MonadReader (CompilationCtx uni fun a) m =>
m (Provenance a)
getEnclosing m (Provenance a)
-> (Provenance a -> m (PIRTerm uni fun a)) -> m (PIRTerm uni fun a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Provenance a
p ->
    -- See Note [Extra definitions while compiling let-bindings]
    Provenance a
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
-> m (PIRTerm uni fun a)
forall (m :: * -> *) key ann (uni :: * -> *) fun.
(Monad m, Ord key) =>
ann
-> DefT key uni fun ann m (Term TyName Name uni fun ann)
-> m (Term TyName Name uni fun ann)
runDefT Provenance a
p (DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
 -> m (PIRTerm uni fun a))
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
-> m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$ LensLike
  (WrappedMonad (DefT SharedName uni fun (Provenance a) m))
  (PIRTerm uni fun a)
  (PIRTerm uni fun a)
  (PIRTerm uni fun a)
  (PIRTerm uni fun a)
-> (PIRTerm uni fun a
    -> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a))
-> PIRTerm uni fun a
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall (m :: * -> *) a b.
Monad m =>
LensLike (WrappedMonad m) a b a b -> (b -> m b) -> a -> m b
transformMOf LensLike
  (WrappedMonad (DefT SharedName uni fun (Provenance a) m))
  (PIRTerm uni fun a)
  (PIRTerm uni fun a)
  (PIRTerm uni fun a)
  (PIRTerm uni fun a)
forall tyname name (uni :: * -> *) fun a.
Traversal'
  (Term tyname name uni fun a) (Term tyname name uni fun a)
termSubterms (LetKind
-> PIRTerm uni fun a
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
LetKind
-> PIRTerm uni fun a
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
compileLet LetKind
kind) PIRTerm uni fun a
t

compileLet :: Compiling m e uni fun a => LetKind -> PIRTerm uni fun a -> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
compileLet :: LetKind
-> PIRTerm uni fun a
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
compileLet LetKind
kind = \case
    Let Provenance a
p Recursivity
r NonEmpty (Binding TyName Name uni fun (Provenance a))
bs PIRTerm uni fun a
body -> (Provenance a -> Provenance a)
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall (uni :: * -> *) fun a (m :: * -> *) b.
MonadReader (CompilationCtx uni fun a) m =>
(Provenance a -> Provenance a) -> m b -> m b
withEnclosing (Provenance a -> Provenance a -> Provenance a
forall a b. a -> b -> a
const (Provenance a -> Provenance a -> Provenance a)
-> Provenance a -> Provenance a -> Provenance a
forall a b. (a -> b) -> a -> b
$ Recursivity -> Provenance a -> Provenance a
forall a. Recursivity -> Provenance a -> Provenance a
LetBinding Recursivity
r Provenance a
p) (DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
 -> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a))
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$ case Recursivity
r of
            -- See Note [Right-associative compilation of let-bindings for linear scoping]
            Recursivity
NonRec -> m (PIRTerm uni fun a)
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (PIRTerm uni fun a)
 -> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a))
-> m (PIRTerm uni fun a)
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$ (PIRTerm uni fun a
 -> Binding TyName Name uni fun (Provenance a)
 -> m (PIRTerm uni fun a))
-> PIRTerm uni fun a
-> NonEmpty (Binding TyName Name uni fun (Provenance a))
-> m (PIRTerm uni fun a)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (LetKind
-> PIRTerm uni fun a
-> Binding TyName Name uni fun (Provenance a)
-> m (PIRTerm uni fun a)
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
LetKind
-> PIRTerm uni fun a
-> Binding TyName Name uni fun (Provenance a)
-> m (PIRTerm uni fun a)
compileNonRecBinding LetKind
kind) PIRTerm uni fun a
body (NonEmpty (Binding TyName Name uni fun (Provenance a))
-> NonEmpty (Binding TyName Name uni fun (Provenance a))
forall a. NonEmpty a -> NonEmpty a
NE.reverse NonEmpty (Binding TyName Name uni fun (Provenance a))
bs)
            Recursivity
Rec    -> LetKind
-> PIRTerm uni fun a
-> NonEmpty (Binding TyName Name uni fun (Provenance a))
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
LetKind
-> PIRTerm uni fun a
-> NonEmpty (Binding TyName Name uni fun (Provenance a))
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
compileRecBindings LetKind
kind PIRTerm uni fun a
body NonEmpty (Binding TyName Name uni fun (Provenance a))
bs
    PIRTerm uni fun a
x -> PIRTerm uni fun a
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure PIRTerm uni fun a
x

compileRecBindings
    :: Compiling m e uni fun a
    => LetKind
    -> PIRTerm uni fun a
    -> NE.NonEmpty (Binding TyName Name uni fun (Provenance a))
    -> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
compileRecBindings :: LetKind
-> PIRTerm uni fun a
-> NonEmpty (Binding TyName Name uni fun (Provenance a))
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
compileRecBindings LetKind
kind PIRTerm uni fun a
body NonEmpty (Binding TyName Name uni fun (Provenance a))
bs =
  case NonEmpty (NonEmpty (Binding TyName Name uni fun (Provenance a)))
grouped of
    NonEmpty (Binding TyName Name uni fun (Provenance a))
singleGroup :| [] ->
      case NonEmpty (Binding TyName Name uni fun (Provenance a))
-> Binding TyName Name uni fun (Provenance a)
forall a. NonEmpty a -> a
NE.head NonEmpty (Binding TyName Name uni fun (Provenance a))
singleGroup of
         TermBind {} -> LetKind
-> PIRTerm uni fun a
-> NonEmpty (Binding TyName Name uni fun (Provenance a))
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
LetKind
-> PIRTerm uni fun a
-> NonEmpty (Binding TyName Name uni fun (Provenance a))
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
compileRecTermBindings LetKind
kind PIRTerm uni fun a
body NonEmpty (Binding TyName Name uni fun (Provenance a))
singleGroup
         DatatypeBind {} ->  m (PIRTerm uni fun a)
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (PIRTerm uni fun a)
 -> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a))
-> m (PIRTerm uni fun a)
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$ LetKind
-> PIRTerm uni fun a
-> NonEmpty (Binding TyName Name uni fun (Provenance a))
-> m (PIRTerm uni fun a)
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
LetKind
-> PIRTerm uni fun a
-> NonEmpty (Binding TyName Name uni fun (Provenance a))
-> m (PIRTerm uni fun a)
compileRecDataBindings LetKind
kind PIRTerm uni fun a
body NonEmpty (Binding TyName Name uni fun (Provenance a))
singleGroup
         TypeBind {} -> m (PIRTerm uni fun a)
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (PIRTerm uni fun a)
 -> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a))
-> m (PIRTerm uni fun a)
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$ m (Provenance a)
forall (uni :: * -> *) fun a (m :: * -> *).
MonadReader (CompilationCtx uni fun a) m =>
m (Provenance a)
getEnclosing m (Provenance a)
-> (Provenance a -> m (PIRTerm uni fun a)) -> m (PIRTerm uni fun a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Provenance a
p -> 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)
_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
CompilationError Provenance a
p Text
"Type bindings cannot appear in recursive let, use datatypebind instead"
    -- only one single group should appear, we do not allow mixing of bind styles
    NonEmpty (NonEmpty (Binding TyName Name uni fun (Provenance a)))
_ -> m (PIRTerm uni fun a)
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (PIRTerm uni fun a)
 -> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a))
-> m (PIRTerm uni fun a)
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$ m (Provenance a)
forall (uni :: * -> *) fun a (m :: * -> *).
MonadReader (CompilationCtx uni fun a) m =>
m (Provenance a)
getEnclosing m (Provenance a)
-> (Provenance a -> m (PIRTerm uni fun a)) -> m (PIRTerm uni fun a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Provenance a
p -> 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)
_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
CompilationError Provenance a
p Text
"Mixed term/type/data bindings in recursive let"
  where
        -- We group the bindings by their binding style, i.e.: term , data or type bindingstyle
        -- All bindings of a let should be of the same style; for that, we make use of the `groupWith1`
        -- and we expect to see exactly 1 group returned by it.
        -- The `NE.groupWith1` returns N>=1 of "adjacent" grouppings, compared to the similar `NE.groupAllWith1`
        -- which returns  at most 3 groups (1 => termbind, 2 -> typebind, 3 -> databind).
        -- `NE.groupAllWith1` is an overkill here, since we don't care about the minimal number of groups, just that there is exactly 1 group.
        grouped :: NonEmpty (NonEmpty (Binding TyName Name uni fun (Provenance a)))
grouped  = (Binding TyName Name uni fun (Provenance a) -> Int)
-> NonEmpty (Binding TyName Name uni fun (Provenance a))
-> NonEmpty (NonEmpty (Binding TyName Name uni fun (Provenance a)))
forall b a. Eq b => (a -> b) -> NonEmpty a -> NonEmpty (NonEmpty a)
NE.groupWith1 (\case { TermBind {} -> Int
1 ::Int ; TypeBind {} -> Int
2; Binding TyName Name uni fun (Provenance a)
_ -> Int
3 }) NonEmpty (Binding TyName Name uni fun (Provenance a))
bs

compileRecTermBindings
    :: Compiling m e uni fun a
    => LetKind
    -> PIRTerm uni fun a
    -> NE.NonEmpty (Binding TyName Name uni fun (Provenance a))
    -> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
compileRecTermBindings :: LetKind
-> PIRTerm uni fun a
-> NonEmpty (Binding TyName Name uni fun (Provenance a))
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
compileRecTermBindings LetKind
RecTerms PIRTerm uni fun a
body NonEmpty (Binding TyName Name uni fun (Provenance a))
bs = do
    NonEmpty
  (Def
     (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
binds <- NonEmpty (Binding TyName Name uni fun (Provenance a))
-> (Binding TyName Name uni fun (Provenance a)
    -> DefT
         SharedName
         uni
         fun
         (Provenance a)
         m
         (Def
            (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)))
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (NonEmpty
        (Def
           (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM NonEmpty (Binding TyName Name uni fun (Provenance a))
bs ((Binding TyName Name uni fun (Provenance a)
  -> DefT
       SharedName
       uni
       fun
       (Provenance a)
       m
       (Def
          (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)))
 -> DefT
      SharedName
      uni
      fun
      (Provenance a)
      m
      (NonEmpty
         (Def
            (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))))
-> (Binding TyName Name uni fun (Provenance a)
    -> DefT
         SharedName
         uni
         fun
         (Provenance a)
         m
         (Def
            (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)))
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (NonEmpty
        (Def
           (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)))
forall a b. (a -> b) -> a -> b
$ \case
        TermBind Provenance a
_ Strictness
Strict VarDecl TyName Name uni fun (Provenance a)
vd PIRTerm uni fun a
rhs -> Def
  (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Def
   (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
 -> DefT
      SharedName
      uni
      fun
      (Provenance a)
      m
      (Def
         (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)))
-> Def
     (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
forall a b. (a -> b) -> a -> b
$ VarDecl TyName Name uni fun (Provenance a)
-> PIRTerm uni fun a
-> Def
     (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)
forall var val. var -> val -> Def var val
PIR.Def VarDecl TyName Name uni fun (Provenance a)
vd PIRTerm uni fun a
rhs
        Binding TyName Name uni fun (Provenance a)
_ -> m (Def
     (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Def
      (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
 -> DefT
      SharedName
      uni
      fun
      (Provenance a)
      m
      (Def
         (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)))
-> m (Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
forall a b. (a -> b) -> a -> b
$ m (Provenance a)
forall (uni :: * -> *) fun a (m :: * -> *).
MonadReader (CompilationCtx uni fun a) m =>
m (Provenance a)
getEnclosing m (Provenance a)
-> (Provenance a
    -> m (Def
            (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)))
-> m (Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Provenance a
p -> AReview e (Error uni fun (Provenance a))
-> Error uni fun (Provenance a)
-> m (Def
        (VarDecl TyName Name uni fun (Provenance a)) (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)
_Error (Error uni fun (Provenance a)
 -> m (Def
         (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a)))
-> Error uni fun (Provenance a)
-> m (Def
        (VarDecl TyName Name uni fun (Provenance a)) (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
CompilationError Provenance a
p Text
"Internal error: type binding in term binding group"
    PIRTerm uni fun a
-> NonEmpty
     (Def
        (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
PIRTerm uni fun a
-> NonEmpty (TermDef TyName Name uni fun (Provenance a))
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
compileRecTerms PIRTerm uni fun a
body NonEmpty
  (Def
     (VarDecl TyName Name uni fun (Provenance a)) (PIRTerm uni fun a))
binds
compileRecTermBindings LetKind
_ PIRTerm uni fun a
body NonEmpty (Binding TyName Name uni fun (Provenance a))
bs = m (PIRTerm uni fun a)
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (PIRTerm uni fun a)
 -> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a))
-> m (PIRTerm uni fun a)
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$ m (Provenance a)
forall (uni :: * -> *) fun a (m :: * -> *).
MonadReader (CompilationCtx uni fun a) m =>
m (Provenance a)
getEnclosing m (Provenance a)
-> (Provenance a -> m (PIRTerm uni fun a)) -> m (PIRTerm uni fun a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Provenance a
p -> PIRTerm uni fun a -> m (PIRTerm uni fun 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
-> Recursivity
-> NonEmpty (Binding TyName Name uni fun (Provenance a))
-> PIRTerm uni fun a
-> PIRTerm uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let Provenance a
p Recursivity
Rec NonEmpty (Binding TyName Name uni fun (Provenance a))
bs PIRTerm uni fun a
body

compileRecDataBindings :: Compiling m e uni fun a => LetKind -> PIRTerm uni fun a -> NE.NonEmpty (Binding TyName Name uni fun (Provenance a)) -> m (PIRTerm uni fun a)
compileRecDataBindings :: LetKind
-> PIRTerm uni fun a
-> NonEmpty (Binding TyName Name uni fun (Provenance a))
-> m (PIRTerm uni fun a)
compileRecDataBindings LetKind
DataTypes PIRTerm uni fun a
body NonEmpty (Binding TyName Name uni fun (Provenance a))
bs = do
    NonEmpty (Datatype TyName Name uni fun (Provenance a))
binds <- NonEmpty (Binding TyName Name uni fun (Provenance a))
-> (Binding TyName Name uni fun (Provenance a)
    -> m (Datatype TyName Name uni fun (Provenance a)))
-> m (NonEmpty (Datatype TyName Name uni fun (Provenance a)))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM NonEmpty (Binding TyName Name uni fun (Provenance a))
bs ((Binding TyName Name uni fun (Provenance a)
  -> m (Datatype TyName Name uni fun (Provenance a)))
 -> m (NonEmpty (Datatype TyName Name uni fun (Provenance a))))
-> (Binding TyName Name uni fun (Provenance a)
    -> m (Datatype TyName Name uni fun (Provenance a)))
-> m (NonEmpty (Datatype TyName Name uni fun (Provenance a)))
forall a b. (a -> b) -> a -> b
$ \case
        DatatypeBind Provenance a
_ Datatype TyName Name uni fun (Provenance a)
d -> Datatype TyName Name uni fun (Provenance a)
-> m (Datatype TyName Name uni fun (Provenance a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Datatype TyName Name uni fun (Provenance a)
d
        Binding TyName Name uni fun (Provenance a)
_ -> m (Provenance a)
forall (uni :: * -> *) fun a (m :: * -> *).
MonadReader (CompilationCtx uni fun a) m =>
m (Provenance a)
getEnclosing m (Provenance a)
-> (Provenance a
    -> m (Datatype TyName Name uni fun (Provenance a)))
-> m (Datatype TyName Name uni fun (Provenance a))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Provenance a
p -> AReview e (Error uni fun (Provenance a))
-> Error uni fun (Provenance a)
-> m (Datatype TyName Name uni fun (Provenance 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)
_Error (Error uni fun (Provenance a)
 -> m (Datatype TyName Name uni fun (Provenance a)))
-> Error uni fun (Provenance a)
-> m (Datatype TyName Name uni fun (Provenance 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
CompilationError Provenance a
p Text
"Internal error: term or type binding in datatype binding group"
    PIRTerm uni fun a
-> NonEmpty (Datatype TyName Name uni fun (Provenance a))
-> m (PIRTerm uni fun a)
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
PIRTerm uni fun a
-> NonEmpty (Datatype TyName Name uni fun (Provenance a))
-> m (PIRTerm uni fun a)
compileRecDatatypes PIRTerm uni fun a
body NonEmpty (Datatype TyName Name uni fun (Provenance a))
binds
compileRecDataBindings LetKind
_ PIRTerm uni fun a
body NonEmpty (Binding TyName Name uni fun (Provenance a))
bs = m (Provenance a)
forall (uni :: * -> *) fun a (m :: * -> *).
MonadReader (CompilationCtx uni fun a) m =>
m (Provenance a)
getEnclosing m (Provenance a)
-> (Provenance a -> m (PIRTerm uni fun a)) -> m (PIRTerm uni fun a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Provenance a
p -> PIRTerm uni fun a -> m (PIRTerm uni fun 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
-> Recursivity
-> NonEmpty (Binding TyName Name uni fun (Provenance a))
-> PIRTerm uni fun a
-> PIRTerm uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let Provenance a
p Recursivity
Rec NonEmpty (Binding TyName Name uni fun (Provenance a))
bs PIRTerm uni fun a
body

compileNonRecBinding :: Compiling m e uni fun a => LetKind -> PIRTerm uni fun a -> Binding TyName Name uni fun (Provenance a) -> m (PIRTerm uni fun a)
compileNonRecBinding :: LetKind
-> PIRTerm uni fun a
-> Binding TyName Name uni fun (Provenance a)
-> m (PIRTerm uni fun a)
compileNonRecBinding LetKind
NonRecTerms PIRTerm uni fun a
body (TermBind Provenance a
x Strictness
Strict VarDecl TyName Name uni fun (Provenance a)
d PIRTerm uni fun a
rhs) = (Provenance a -> Provenance a)
-> m (PIRTerm uni fun a) -> m (PIRTerm uni fun a)
forall (uni :: * -> *) fun a (m :: * -> *) b.
MonadReader (CompilationCtx uni fun a) m =>
(Provenance a -> Provenance a) -> m b -> m b
withEnclosing (Provenance a -> Provenance a -> Provenance a
forall a b. a -> b -> a
const (Provenance a -> Provenance a -> Provenance a)
-> Provenance a -> Provenance a -> Provenance a
forall a b. (a -> b) -> a -> b
$ String -> Provenance a -> Provenance a
forall a. String -> Provenance a -> Provenance a
TermBinding (VarDecl TyName Name uni fun (Provenance a) -> String
forall tyname (uni :: * -> *) fun a.
VarDecl tyname Name uni fun a -> String
varDeclNameString VarDecl TyName Name uni fun (Provenance a)
d) Provenance a
x) (m (PIRTerm uni fun a) -> m (PIRTerm uni fun a))
-> m (PIRTerm uni fun a) -> m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$
   Provenance a
-> TermDef
     (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
-> PIRTerm uni fun a
-> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> TermDef term tyname name uni fun ann -> term ann -> term ann
PIR.mkImmediateLamAbs (Provenance a
 -> TermDef
      (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
 -> PIRTerm uni fun a
 -> PIRTerm uni fun a)
-> m (Provenance a)
-> m (TermDef
        (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
      -> PIRTerm uni fun a -> PIRTerm uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Provenance a)
forall (uni :: * -> *) fun a (m :: * -> *).
MonadReader (CompilationCtx uni fun a) m =>
m (Provenance a)
getEnclosing m (TermDef
     (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
   -> PIRTerm uni fun a -> PIRTerm uni fun a)
-> m (TermDef
        (Term TyName Name uni fun) TyName Name uni fun (Provenance a))
-> m (PIRTerm uni fun a -> PIRTerm uni fun a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TermDef
  (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
-> m (TermDef
        (Term TyName Name uni fun) TyName Name uni fun (Provenance a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni fun (Provenance a)
-> PIRTerm uni fun a
-> TermDef
     (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
forall var val. var -> val -> Def var val
PIR.Def VarDecl TyName Name uni fun (Provenance a)
d PIRTerm uni fun a
rhs) m (PIRTerm uni fun a -> PIRTerm uni fun a)
-> m (PIRTerm uni fun a) -> m (PIRTerm uni fun a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure PIRTerm uni fun a
body
compileNonRecBinding LetKind
Types PIRTerm uni fun a
body (TypeBind Provenance a
x TyVarDecl TyName (Provenance a)
d Type TyName uni (Provenance a)
rhs) = (Provenance a -> Provenance a)
-> m (PIRTerm uni fun a) -> m (PIRTerm uni fun a)
forall (uni :: * -> *) fun a (m :: * -> *) b.
MonadReader (CompilationCtx uni fun a) m =>
(Provenance a -> Provenance a) -> m b -> m b
withEnclosing (Provenance a -> Provenance a -> Provenance a
forall a b. a -> b -> a
const (Provenance a -> Provenance a -> Provenance a)
-> Provenance a -> Provenance a -> Provenance a
forall a b. (a -> b) -> a -> b
$ String -> Provenance a -> Provenance a
forall a. String -> Provenance a -> Provenance a
TypeBinding (TyVarDecl TyName (Provenance a) -> String
forall a. TyVarDecl TyName a -> String
tyVarDeclNameString TyVarDecl TyName (Provenance a)
d) Provenance a
x) (m (PIRTerm uni fun a) -> m (PIRTerm uni fun a))
-> m (PIRTerm uni fun a) -> m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$
   Provenance a
-> TypeDef TyName uni (Provenance a)
-> PIRTerm uni fun a
-> PIRTerm uni fun a
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> TypeDef tyname uni ann -> term ann -> term ann
PIR.mkImmediateTyAbs (Provenance a
 -> TypeDef TyName uni (Provenance a)
 -> PIRTerm uni fun a
 -> PIRTerm uni fun a)
-> m (Provenance a)
-> m (TypeDef TyName uni (Provenance a)
      -> PIRTerm uni fun a -> PIRTerm uni fun a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Provenance a)
forall (uni :: * -> *) fun a (m :: * -> *).
MonadReader (CompilationCtx uni fun a) m =>
m (Provenance a)
getEnclosing m (TypeDef TyName uni (Provenance a)
   -> PIRTerm uni fun a -> PIRTerm uni fun a)
-> m (TypeDef TyName uni (Provenance a))
-> m (PIRTerm uni fun a -> PIRTerm uni fun a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TypeDef TyName uni (Provenance a)
-> m (TypeDef TyName uni (Provenance a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVarDecl TyName (Provenance a)
-> Type TyName uni (Provenance a)
-> TypeDef TyName uni (Provenance a)
forall var val. var -> val -> Def var val
PIR.Def TyVarDecl TyName (Provenance a)
d Type TyName uni (Provenance a)
rhs) m (PIRTerm uni fun a -> PIRTerm uni fun a)
-> m (PIRTerm uni fun a) -> m (PIRTerm uni fun a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PIRTerm uni fun a -> m (PIRTerm uni fun a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure PIRTerm uni fun a
body
compileNonRecBinding LetKind
DataTypes PIRTerm uni fun a
body (DatatypeBind Provenance a
x Datatype TyName Name uni fun (Provenance a)
d) = (Provenance a -> Provenance a)
-> m (PIRTerm uni fun a) -> m (PIRTerm uni fun a)
forall (uni :: * -> *) fun a (m :: * -> *) b.
MonadReader (CompilationCtx uni fun a) m =>
(Provenance a -> Provenance a) -> m b -> m b
withEnclosing (Provenance a -> Provenance a -> Provenance a
forall a b. a -> b -> a
const (Provenance a -> Provenance a -> Provenance a)
-> Provenance a -> Provenance a -> Provenance a
forall a b. (a -> b) -> a -> b
$ String -> Provenance a -> Provenance a
forall a. String -> Provenance a -> Provenance a
TypeBinding (Datatype TyName Name uni fun (Provenance a) -> String
forall (uni :: * -> *) fun a.
Datatype TyName Name uni fun a -> String
datatypeNameString Datatype TyName Name uni fun (Provenance a)
d) Provenance a
x) (m (PIRTerm uni fun a) -> m (PIRTerm uni fun a))
-> m (PIRTerm uni fun a) -> m (PIRTerm uni fun a)
forall a b. (a -> b) -> a -> b
$
   Recursivity
-> PIRTerm uni fun a
-> Datatype TyName Name uni fun (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 fun (Provenance a)
-> m (PIRTerm uni fun a)
compileDatatype Recursivity
NonRec PIRTerm uni fun a
body Datatype TyName Name uni fun (Provenance a)
d
compileNonRecBinding LetKind
_ PIRTerm uni fun a
body Binding TyName Name uni fun (Provenance a)
b = m (Provenance a)
forall (uni :: * -> *) fun a (m :: * -> *).
MonadReader (CompilationCtx uni fun a) m =>
m (Provenance a)
getEnclosing m (Provenance a)
-> (Provenance a -> m (PIRTerm uni fun a)) -> m (PIRTerm uni fun a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Provenance a
p -> PIRTerm uni fun a -> m (PIRTerm uni fun 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
-> Recursivity
-> NonEmpty (Binding TyName Name uni fun (Provenance a))
-> PIRTerm uni fun a
-> PIRTerm uni fun a
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let Provenance a
p Recursivity
NonRec (Binding TyName Name uni fun (Provenance a)
-> NonEmpty (Binding TyName Name uni fun (Provenance a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Binding TyName Name uni fun (Provenance a)
b) PIRTerm uni fun a
body