-- editorconfig-checker-disable-file
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies      #-}

-- | Simulating laziness.
module PlutusTx.Compiler.Laziness where

import PlutusTx.Compiler.Types
import PlutusTx.PIRTypes

import PlutusIR qualified as PIR

import PlutusCore.Quote

{- Note [Object- vs meta-language combinators]
Many of the things we define as *meta*-langugage combinators (i.e. operations on terms) could be defined
as combinators in the object language (i.e. terms). For example, we can define 'delay' as taking a term
and returning a lambda that takes unit and returns the term, or we could define a 'delay' term

\t : a . \u : unit . t

We generally prefer the metalanguage approach despite the fact that we could share combinators
with the standard library because it makes the generated terms simpler without the need for
a simplifier pass. Also, PLC isn't lazy, so combinators work less well.
-}

delay :: Compiling uni fun m ann => PIRTerm uni fun -> m (PIRTerm uni fun)
delay :: forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
PIRTerm uni fun -> m (PIRTerm uni fun)
delay PIRTerm uni fun
body = Ann -> TyName -> Kind Ann -> PIRTerm uni fun -> PIRTerm uni fun
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
PIR.TyAbs Ann
annMayInline (TyName -> Kind Ann -> PIRTerm uni fun -> PIRTerm uni fun)
-> m TyName -> m (Kind Ann -> PIRTerm uni fun -> PIRTerm uni fun)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Quote TyName -> m TyName
forall a. Quote a -> m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Text -> Quote TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"dead") m (Kind Ann -> PIRTerm uni fun -> PIRTerm uni fun)
-> m (Kind Ann) -> m (PIRTerm uni fun -> PIRTerm uni fun)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Kind Ann -> m (Kind Ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ann -> Kind Ann
forall ann. ann -> Kind ann
PIR.Type Ann
annMayInline) m (PIRTerm uni fun -> PIRTerm uni fun)
-> m (PIRTerm uni fun) -> m (PIRTerm uni fun)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PIRTerm uni fun -> m (PIRTerm uni fun)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PIRTerm uni fun
body

delayType :: Compiling uni fun m ann => PIRType uni -> m (PIRType uni)
delayType :: forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
PIRType uni -> m (PIRType uni)
delayType PIRType uni
orig = Ann -> TyName -> Kind Ann -> PIRType uni -> PIRType uni
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
PIR.TyForall Ann
annMayInline (TyName -> Kind Ann -> PIRType uni -> PIRType uni)
-> m TyName -> m (Kind Ann -> PIRType uni -> PIRType uni)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Quote TyName -> m TyName
forall a. Quote a -> m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Text -> Quote TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"dead") m (Kind Ann -> PIRType uni -> PIRType uni)
-> m (Kind Ann) -> m (PIRType uni -> PIRType uni)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Kind Ann -> m (Kind Ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ann -> Kind Ann
forall ann. ann -> Kind ann
PIR.Type Ann
annMayInline) m (PIRType uni -> PIRType uni)
-> m (PIRType uni) -> m (PIRType uni)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PIRType uni -> m (PIRType uni)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PIRType uni
orig

delayVar :: Compiling uni fun m ann => PIRVar uni -> m (PIRVar uni)
delayVar :: forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
PIRVar uni -> m (PIRVar uni)
delayVar (PIR.VarDecl Ann
ann Name
n Type TyName uni Ann
ty) = do
    Type TyName uni Ann
ty' <- Type TyName uni Ann -> m (Type TyName uni Ann)
forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
PIRType uni -> m (PIRType uni)
delayType Type TyName uni Ann
ty
    VarDecl TyName Name uni Ann -> m (VarDecl TyName Name uni Ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni Ann -> m (VarDecl TyName Name uni Ann))
-> VarDecl TyName Name uni Ann -> m (VarDecl TyName Name uni Ann)
forall a b. (a -> b) -> a -> b
$ Ann -> Name -> Type TyName uni Ann -> VarDecl TyName Name uni Ann
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
PIR.VarDecl Ann
ann Name
n Type TyName uni Ann
ty'

force
    :: CompilingDefault uni fun m ann
    => PIRTerm uni fun -> m (PIRTerm uni fun)
force :: forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
PIRTerm uni fun -> m (PIRTerm uni fun)
force PIRTerm uni fun
thunk = do
    TyName
a <- Quote TyName -> m TyName
forall a. Quote a -> m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Text -> Quote TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"dead")
    let fakeTy :: Type TyName uni Ann
fakeTy = 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
PIR.TyForall Ann
annMayInline TyName
a (Ann -> Kind Ann
forall ann. ann -> Kind ann
PIR.Type Ann
annMayInline) (Ann -> TyName -> Type TyName uni Ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
PIR.TyVar Ann
annMayInline TyName
a)
    PIRTerm uni fun -> m (PIRTerm uni fun)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PIRTerm uni fun -> m (PIRTerm uni fun))
-> PIRTerm uni fun -> m (PIRTerm uni fun)
forall a b. (a -> b) -> a -> b
$ Ann -> PIRTerm uni fun -> Type TyName uni Ann -> PIRTerm uni fun
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
PIR.TyInst Ann
annMayInline PIRTerm uni fun
thunk Type TyName uni Ann
fakeTy

maybeDelay :: Compiling uni fun m ann => Bool -> PIRTerm uni fun -> m (PIRTerm uni fun)
maybeDelay :: forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
Bool -> PIRTerm uni fun -> m (PIRTerm uni fun)
maybeDelay Bool
yes PIRTerm uni fun
t = if Bool
yes then PIRTerm uni fun -> m (PIRTerm uni fun)
forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
PIRTerm uni fun -> m (PIRTerm uni fun)
delay PIRTerm uni fun
t else PIRTerm uni fun -> m (PIRTerm uni fun)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PIRTerm uni fun
t

maybeDelayVar :: Compiling uni fun m ann => Bool -> PIRVar uni -> m (PIRVar uni)
maybeDelayVar :: forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
Bool -> PIRVar uni -> m (PIRVar uni)
maybeDelayVar Bool
yes PIRVar uni
v = if Bool
yes then PIRVar uni -> m (PIRVar uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
PIRVar uni -> m (PIRVar uni)
delayVar PIRVar uni
v else PIRVar uni -> m (PIRVar uni)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PIRVar uni
v

maybeDelayType :: Compiling uni fun m ann => Bool -> PIRType uni -> m (PIRType uni)
maybeDelayType :: forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
Bool -> PIRType uni -> m (PIRType uni)
maybeDelayType Bool
yes PIRType uni
t = if Bool
yes then PIRType uni -> m (PIRType uni)
forall (uni :: * -> *) fun (m :: * -> *) ann.
Compiling uni fun m ann =>
PIRType uni -> m (PIRType uni)
delayType PIRType uni
t else PIRType uni -> m (PIRType uni)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PIRType uni
t

maybeForce
    :: CompilingDefault uni fun m ann
    => Bool -> PIRTerm uni fun -> m (PIRTerm uni fun)
maybeForce :: forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
Bool -> PIRTerm uni fun -> m (PIRTerm uni fun)
maybeForce Bool
yes PIRTerm uni fun
t = if Bool
yes then PIRTerm uni fun -> m (PIRTerm uni fun)
forall (uni :: * -> *) fun (m :: * -> *) ann.
CompilingDefault uni fun m ann =>
PIRTerm uni fun -> m (PIRTerm uni fun)
force PIRTerm uni fun
t else PIRTerm uni fun -> m (PIRTerm uni fun)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PIRTerm uni fun
t