-- 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
forall a. AnnInline a => a
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
forall a. AnnInline a => a
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
forall a. AnnInline a => a
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
forall a. AnnInline a => a
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
forall a. AnnInline a => a
annMayInline TyName
a (Ann -> Kind Ann
forall ann. ann -> Kind ann
PIR.Type Ann
forall a. AnnInline a => a
annMayInline) (Ann -> TyName -> Type TyName uni Ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
PIR.TyVar Ann
forall a. AnnInline a => a
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
forall a. AnnInline a => a
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