{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies        #-}
module PlutusIR.Compiler (
    compileTerm,
    compileToReadable,
    compileReadableToPlc,
    Compiling,
    Error (..),
    AsError (..),
    AsTypeError (..),
    AsTypeErrorExt (..),
    Provenance (..),
    DatatypeComponent (..),
    noProvenance,
    CompilationOpts,
    coOptimize,
    coPedantic,
    coVerbose,
    coDebug,
    coMaxSimplifierIterations,
    coDoSimplifierUnwrapCancel,
    coDoSimplifierBeta,
    coDoSimplifierInline,
    coInlineHints,
    coProfile,
    defaultCompilationOpts,
    CompilationCtx,
    ccOpts,
    ccEnclosing,
    ccTypeCheckConfig,
    PirTCConfig(..),
    AllowEscape(..),
    toDefaultCompilationCtx) where

import PlutusIR

import PlutusIR.Compiler.Let qualified as Let
import PlutusIR.Compiler.Lower
import PlutusIR.Compiler.Provenance
import PlutusIR.Compiler.Types
import PlutusIR.Error
import PlutusIR.Transform.Beta qualified as Beta
import PlutusIR.Transform.DeadCode qualified as DeadCode
import PlutusIR.Transform.Inline qualified as Inline
import PlutusIR.Transform.LetFloat qualified as LetFloat
import PlutusIR.Transform.LetMerge qualified as LetMerge
import PlutusIR.Transform.NonStrict qualified as NonStrict
import PlutusIR.Transform.RecSplit qualified as RecSplit
import PlutusIR.Transform.Rename ()
import PlutusIR.Transform.ThunkRecursions qualified as ThunkRec
import PlutusIR.Transform.Unwrap qualified as Unwrap
import PlutusIR.TypeCheck.Internal

import PlutusCore qualified as PLC

import Control.Lens
import Control.Monad
import Control.Monad.Extra (orM, whenM)
import Control.Monad.Reader
import Debug.Trace (traceM)
import PlutusPrelude

-- Simplifier passes
data Pass uni fun =
  Pass { Pass uni fun -> String
_name      :: String
       , Pass uni fun
-> forall (m :: * -> *) e a. Compiling m e uni fun a => m Bool
_shouldRun :: forall m e a.   Compiling m e uni fun a => m Bool
       , Pass uni fun
-> forall (m :: * -> *) e a.
   Compiling m e uni fun a =>
   Term TyName Name uni fun (Provenance a)
   -> m (Term TyName Name uni fun (Provenance a))
_pass      :: forall m e a. Compiling m e uni fun a => Term TyName Name uni fun (Provenance a) -> m (Term TyName Name uni fun (Provenance a))
       }

onOption :: Compiling m e uni fun a => Lens' (CompilationOpts a) Bool -> m Bool
onOption :: Lens' (CompilationOpts a) Bool -> m Bool
onOption Lens' (CompilationOpts a) Bool
coOpt = Getting Bool (CompilationCtx uni fun a) Bool -> m Bool
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((CompilationOpts a -> Const Bool (CompilationOpts a))
-> CompilationCtx uni fun a
-> Const Bool (CompilationCtx uni fun a)
forall (uni :: * -> *) fun a.
Lens' (CompilationCtx uni fun a) (CompilationOpts a)
ccOpts ((CompilationOpts a -> Const Bool (CompilationOpts a))
 -> CompilationCtx uni fun a
 -> Const Bool (CompilationCtx uni fun a))
-> ((Bool -> Const Bool Bool)
    -> CompilationOpts a -> Const Bool (CompilationOpts a))
-> Getting Bool (CompilationCtx uni fun a) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Const Bool Bool)
-> CompilationOpts a -> Const Bool (CompilationOpts a)
Lens' (CompilationOpts a) Bool
coOpt)

isVerbose :: Compiling m e uni fun a => m Bool
isVerbose :: m Bool
isVerbose = Getting Bool (CompilationCtx uni fun a) Bool -> m Bool
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Getting Bool (CompilationCtx uni fun a) Bool -> m Bool)
-> Getting Bool (CompilationCtx uni fun a) Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ (CompilationOpts a -> Const Bool (CompilationOpts a))
-> CompilationCtx uni fun a
-> Const Bool (CompilationCtx uni fun a)
forall (uni :: * -> *) fun a.
Lens' (CompilationCtx uni fun a) (CompilationOpts a)
ccOpts ((CompilationOpts a -> Const Bool (CompilationOpts a))
 -> CompilationCtx uni fun a
 -> Const Bool (CompilationCtx uni fun a))
-> ((Bool -> Const Bool Bool)
    -> CompilationOpts a -> Const Bool (CompilationOpts a))
-> Getting Bool (CompilationCtx uni fun a) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Const Bool Bool)
-> CompilationOpts a -> Const Bool (CompilationOpts a)
forall a. Lens' (CompilationOpts a) Bool
coVerbose

isDebug :: Compiling m e uni fun a => m Bool
isDebug :: m Bool
isDebug = Getting Bool (CompilationCtx uni fun a) Bool -> m Bool
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Getting Bool (CompilationCtx uni fun a) Bool -> m Bool)
-> Getting Bool (CompilationCtx uni fun a) Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ (CompilationOpts a -> Const Bool (CompilationOpts a))
-> CompilationCtx uni fun a
-> Const Bool (CompilationCtx uni fun a)
forall (uni :: * -> *) fun a.
Lens' (CompilationCtx uni fun a) (CompilationOpts a)
ccOpts ((CompilationOpts a -> Const Bool (CompilationOpts a))
 -> CompilationCtx uni fun a
 -> Const Bool (CompilationCtx uni fun a))
-> ((Bool -> Const Bool Bool)
    -> CompilationOpts a -> Const Bool (CompilationOpts a))
-> Getting Bool (CompilationCtx uni fun a) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Const Bool Bool)
-> CompilationOpts a -> Const Bool (CompilationOpts a)
forall a. Lens' (CompilationOpts a) Bool
coDebug

logVerbose :: Compiling m e uni fun a => String -> m ()
logVerbose :: String -> m ()
logVerbose = m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ([m Bool] -> m Bool
forall (m :: * -> *). Monad m => [m Bool] -> m Bool
orM [m Bool
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
m Bool
isVerbose, m Bool
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
m Bool
isDebug]) (m () -> m ()) -> (String -> m ()) -> String -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM

logDebug :: Compiling m e uni fun a => String -> m ()
logDebug :: String -> m ()
logDebug = m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM m Bool
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
m Bool
isDebug (m () -> m ()) -> (String -> m ()) -> String -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> m ()
forall (f :: * -> *). Applicative f => String -> f ()
traceM

applyPass :: (Compiling m e uni fun a, b ~ Provenance a) => Pass uni fun -> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
applyPass :: Pass uni fun
-> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
applyPass Pass uni fun
pass = m Bool
-> (Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (uni :: * -> *) fun a (m :: * -> *) b.
MonadReader (CompilationCtx uni fun a) m =>
m Bool -> (b -> m b) -> b -> m b
runIf (Pass uni fun
-> forall (m :: * -> *) e a. Compiling m e uni fun a => m Bool
forall (uni :: * -> *) fun.
Pass uni fun
-> forall (m :: * -> *) e a. Compiling m e uni fun a => m Bool
_shouldRun Pass uni fun
pass) ((Term TyName Name uni fun (Provenance a)
  -> m (Term TyName Name uni fun (Provenance a)))
 -> Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall a b. (a -> b) -> a -> b
$ (Term TyName Name uni fun (Provenance a) -> m ())
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through Term TyName Name uni fun (Provenance a) -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun b.
Compiling m e uni fun b =>
Term TyName Name uni fun (Provenance b) -> m ()
check (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< \Term TyName Name uni fun (Provenance a)
term -> do
  let passName :: String
passName = Pass uni fun -> String
forall (uni :: * -> *) fun. Pass uni fun -> String
_name Pass uni fun
pass
  String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"      !!! " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
passName
  String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logDebug   (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"        !!! Before " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
passName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (Term TyName Name uni fun (Provenance a) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Term TyName Name uni fun (Provenance a)
term)
  Term TyName Name uni fun (Provenance a)
term' <- Pass uni fun
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (uni :: * -> *) fun.
Pass uni fun
-> forall (m :: * -> *) e a.
   Compiling m e uni fun a =>
   Term TyName Name uni fun (Provenance a)
   -> m (Term TyName Name uni fun (Provenance a))
_pass Pass uni fun
pass Term TyName Name uni fun (Provenance a)
term
  String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logDebug   (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"        !!! After " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
passName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (Term TyName Name uni fun (Provenance a) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Term TyName Name uni fun (Provenance a)
term')
  Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term TyName Name uni fun (Provenance a)
term'

availablePasses :: [Pass uni fun]
availablePasses :: [Pass uni fun]
availablePasses =
    [ String
-> (forall (m :: * -> *) e a. Compiling m e uni fun a => m Bool)
-> (forall (m :: * -> *) e a.
    Compiling m e uni fun a =>
    Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Pass uni fun
forall (uni :: * -> *) fun.
String
-> (forall (m :: * -> *) e a. Compiling m e uni fun a => m Bool)
-> (forall (m :: * -> *) e a.
    Compiling m e uni fun a =>
    Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Pass uni fun
Pass String
"unwrap cancel"        (Lens' (CompilationOpts a) Bool -> m Bool
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
Lens' (CompilationOpts a) Bool -> m Bool
onOption forall a. Lens' (CompilationOpts a) Bool
Lens' (CompilationOpts a) Bool
coDoSimplifierUnwrapCancel)       (Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> Term TyName Name uni fun (Provenance a))
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name uni fun (Provenance a)
-> Term TyName Name uni fun (Provenance a)
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> Term tyname name uni fun a
Unwrap.unwrapCancel)
    , String
-> (forall (m :: * -> *) e a. Compiling m e uni fun a => m Bool)
-> (forall (m :: * -> *) e a.
    Compiling m e uni fun a =>
    Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Pass uni fun
forall (uni :: * -> *) fun.
String
-> (forall (m :: * -> *) e a. Compiling m e uni fun a => m Bool)
-> (forall (m :: * -> *) e a.
    Compiling m e uni fun a =>
    Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Pass uni fun
Pass String
"beta"                 (Lens' (CompilationOpts a) Bool -> m Bool
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
Lens' (CompilationOpts a) Bool -> m Bool
onOption forall a. Lens' (CompilationOpts a) Bool
Lens' (CompilationOpts a) Bool
coDoSimplifierBeta)               (Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> Term TyName Name uni fun (Provenance a))
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name uni fun (Provenance a)
-> Term TyName Name uni fun (Provenance a)
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> Term tyname name uni fun a
Beta.beta)
    , String
-> (forall (m :: * -> *) e a. Compiling m e uni fun a => m Bool)
-> (forall (m :: * -> *) e a.
    Compiling m e uni fun a =>
    Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Pass uni fun
forall (uni :: * -> *) fun.
String
-> (forall (m :: * -> *) e a. Compiling m e uni fun a => m Bool)
-> (forall (m :: * -> *) e a.
    Compiling m e uni fun a =>
    Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Pass uni fun
Pass String
"inline"               (Lens' (CompilationOpts a) Bool -> m Bool
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
Lens' (CompilationOpts a) Bool -> m Bool
onOption forall a. Lens' (CompilationOpts a) Bool
Lens' (CompilationOpts a) Bool
coDoSimplifierInline)             (\Term TyName Name uni fun (Provenance a)
t -> do { InlineHints Name (Provenance a)
hints <- (CompilationCtx uni fun a -> InlineHints Name (Provenance a))
-> m (InlineHints Name (Provenance a))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Getting
  (InlineHints Name (Provenance a))
  (CompilationCtx uni fun a)
  (InlineHints Name (Provenance a))
-> CompilationCtx uni fun a -> InlineHints Name (Provenance a)
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((CompilationOpts a
 -> Const (InlineHints Name (Provenance a)) (CompilationOpts a))
-> CompilationCtx uni fun a
-> Const
     (InlineHints Name (Provenance a)) (CompilationCtx uni fun a)
forall (uni :: * -> *) fun a.
Lens' (CompilationCtx uni fun a) (CompilationOpts a)
ccOpts ((CompilationOpts a
  -> Const (InlineHints Name (Provenance a)) (CompilationOpts a))
 -> CompilationCtx uni fun a
 -> Const
      (InlineHints Name (Provenance a)) (CompilationCtx uni fun a))
-> ((InlineHints Name (Provenance a)
     -> Const
          (InlineHints Name (Provenance a))
          (InlineHints Name (Provenance a)))
    -> CompilationOpts a
    -> Const (InlineHints Name (Provenance a)) (CompilationOpts a))
-> Getting
     (InlineHints Name (Provenance a))
     (CompilationCtx uni fun a)
     (InlineHints Name (Provenance a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InlineHints Name (Provenance a)
 -> Const
      (InlineHints Name (Provenance a))
      (InlineHints Name (Provenance a)))
-> CompilationOpts a
-> Const (InlineHints Name (Provenance a)) (CompilationOpts a)
forall a a2.
Lens
  (CompilationOpts a)
  (CompilationOpts a2)
  (InlineHints Name (Provenance a))
  (InlineHints Name (Provenance a2))
coInlineHints)); InlineHints Name (Provenance a)
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall tyname name (uni :: * -> *) fun a (m :: * -> *).
ExternalConstraints tyname name uni fun m =>
InlineHints name a
-> Term tyname name uni fun a -> m (Term tyname name uni fun a)
Inline.inline InlineHints Name (Provenance a)
hints Term TyName Name uni fun (Provenance a)
t })
    ]

-- | Actual simplifier
simplify
    :: forall m e uni fun a b. (Compiling m e uni fun a, b ~ Provenance a)
    => Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplify :: Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplify = ((Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
 -> (Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
 -> Term TyName Name uni fun b
 -> m (Term TyName Name uni fun b))
-> (Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
-> [Term TyName Name uni fun b -> m (Term TyName Name uni fun b)]
-> Term TyName Name uni fun b
-> m (Term TyName Name uni fun b)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
-> (Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
-> Term TyName Name uni fun b
-> m (Term TyName Name uni fun b)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
(>=>) Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Pass uni fun
 -> Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
-> [Pass uni fun]
-> [Term TyName Name uni fun b -> m (Term TyName Name uni fun b)]
forall a b. (a -> b) -> [a] -> [b]
map Pass uni fun
-> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
forall (m :: * -> *) e (uni :: * -> *) fun a b.
(Compiling m e uni fun a, b ~ Provenance a) =>
Pass uni fun
-> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
applyPass [Pass uni fun]
forall (uni :: * -> *) fun. [Pass uni fun]
availablePasses)

-- | Perform some simplification of a 'Term'.
simplifyTerm
  :: forall m e uni fun a b. (Compiling m e uni fun a, b ~ Provenance a)
  => Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplifyTerm :: Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplifyTerm = (Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
-> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
forall (uni :: * -> *) fun a (m :: * -> *) b.
MonadReader (CompilationCtx uni fun a) m =>
(b -> m b) -> b -> m b
runIfOpts Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplify'
    -- NOTE: we need at least one pass of dead code elimination
    where
        simplify' :: Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
        simplify' :: Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplify' Term TyName Name uni fun b
t = do
            Int
maxIterations <- Getting Int (CompilationCtx uni fun a) Int -> m Int
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((CompilationOpts a -> Const Int (CompilationOpts a))
-> CompilationCtx uni fun a -> Const Int (CompilationCtx uni fun a)
forall (uni :: * -> *) fun a.
Lens' (CompilationCtx uni fun a) (CompilationOpts a)
ccOpts ((CompilationOpts a -> Const Int (CompilationOpts a))
 -> CompilationCtx uni fun a
 -> Const Int (CompilationCtx uni fun a))
-> ((Int -> Const Int Int)
    -> CompilationOpts a -> Const Int (CompilationOpts a))
-> Getting Int (CompilationCtx uni fun a) Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Const Int Int)
-> CompilationOpts a -> Const Int (CompilationOpts a)
forall a. Lens' (CompilationOpts a) Int
coMaxSimplifierIterations)
            Int -> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplifyNTimes Int
maxIterations Term TyName Name uni fun b
t
        -- Run the simplifier @n@ times
        simplifyNTimes :: Int -> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
        simplifyNTimes :: Int -> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplifyNTimes Int
n = ((Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
 -> (Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
 -> Term TyName Name uni fun b
 -> m (Term TyName Name uni fun b))
-> (Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
-> [Term TyName Name uni fun b -> m (Term TyName Name uni fun b)]
-> Term TyName Name uni fun b
-> m (Term TyName Name uni fun b)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
-> (Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
-> Term TyName Name uni fun b
-> m (Term TyName Name uni fun b)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
(>=>) Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Int
 -> Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
-> [Int]
-> [Term TyName Name uni fun b -> m (Term TyName Name uni fun b)]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplifyStep [Int
1 .. Int
n])
        -- generate simplification step
        simplifyStep :: Int -> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
        simplifyStep :: Int -> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplifyStep Int
i Term TyName Name uni fun b
term = do
          String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"    !!! simplifier pass " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
          Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
forall (m :: * -> *) e (uni :: * -> *) fun a b.
(Compiling m e uni fun a, b ~ Provenance a) =>
Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplify Term TyName Name uni fun b
term


-- | Perform floating/merging of lets in a 'Term' to their nearest lambda/Lambda/letStrictNonValue.
-- Note: It assumes globally unique names
floatTerm :: (Compiling m e uni fun a, Semigroup b) => Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
floatTerm :: Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
floatTerm = (Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
-> Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
forall (uni :: * -> *) fun a (m :: * -> *) b.
MonadReader (CompilationCtx uni fun a) m =>
(b -> m b) -> b -> m b
runIfOpts ((Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
 -> Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
-> (Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
-> Term TyName Name uni fun b
-> m (Term TyName Name uni fun b)
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun b -> m (Term TyName Name uni fun b))
-> (Term TyName Name uni fun b -> Term TyName Name uni fun b)
-> Term TyName Name uni fun b
-> m (Term TyName Name uni fun b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name uni fun b -> Term TyName Name uni fun b
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> Term tyname name uni fun a
LetMerge.letMerge (Term TyName Name uni fun b -> Term TyName Name uni fun b)
-> (Term TyName Name uni fun b -> Term TyName Name uni fun b)
-> Term TyName Name uni fun b
-> Term TyName Name uni fun b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name uni fun b -> Term TyName Name uni fun b
forall (uni :: * -> *) fun a name tyname.
(Ord name, Ord tyname, HasUnique tyname TypeUnique,
 HasUnique name TermUnique) =>
Term tyname name uni fun a -> Term tyname name uni fun a
RecSplit.recSplit (Term TyName Name uni fun b -> Term TyName Name uni fun b)
-> (Term TyName Name uni fun b -> Term TyName Name uni fun b)
-> Term TyName Name uni fun b
-> Term TyName Name uni fun b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name uni fun b -> Term TyName Name uni fun b
forall (uni :: * -> *) fun tyname name a.
(ToBuiltinMeaning uni fun, HasUnique tyname TypeUnique,
 HasUnique name TermUnique, Ord tyname, Ord name, Semigroup a) =>
Term tyname name uni fun a -> Term tyname name uni fun a
LetFloat.floatTerm

-- | Typecheck a PIR Term iff the context demands it.
-- Note: assumes globally unique names
typeCheckTerm :: (Compiling m e uni fun a, b ~ Provenance a) => Term TyName Name uni fun b -> m ()
typeCheckTerm :: Term TyName Name uni fun b -> m ()
typeCheckTerm Term TyName Name uni fun b
t = do
    Maybe (PirTCConfig uni fun)
mtcconfig <- (CompilationCtx uni fun a -> Maybe (PirTCConfig uni fun))
-> m (Maybe (PirTCConfig uni fun))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CompilationCtx uni fun a -> Maybe (PirTCConfig uni fun)
forall (uni :: * -> *) fun a.
CompilationCtx uni fun a -> Maybe (PirTCConfig uni fun)
_ccTypeCheckConfig
    case Maybe (PirTCConfig uni fun)
mtcconfig of
        Just PirTCConfig uni fun
tcconfig -> m (Normalized (Type TyName uni ())) -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m (Normalized (Type TyName uni ())) -> m ())
-> (PirTCEnv uni fun e (Normalized (Type TyName uni ()))
    -> m (Normalized (Type TyName uni ())))
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PirTCConfig uni fun
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
-> m (Normalized (Type TyName uni ()))
forall e (m :: * -> *) (uni :: * -> *) fun a.
(MonadError e m, MonadQuote m) =>
PirTCConfig uni fun -> PirTCEnv uni fun e a -> m a
runTypeCheckM PirTCConfig uni fun
tcconfig (PirTCEnv uni fun e (Normalized (Type TyName uni ())) -> m ())
-> PirTCEnv uni fun e (Normalized (Type TyName uni ())) -> m ()
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun b
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
forall (uni :: * -> *) fun ann e.
(GEq uni, Ix fun,
 AsTypeError e (Term TyName Name uni fun ()) uni fun ann,
 ToKind uni, HasUniApply uni, AsTypeErrorExt e uni ann) =>
Term TyName Name uni fun ann
-> PirTCEnv uni fun e (Normalized (Type TyName uni ()))
inferTypeM Term TyName Name uni fun b
t
        Maybe (PirTCConfig uni fun)
Nothing       -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

check :: Compiling m e uni fun b => Term TyName Name uni fun (Provenance b) -> m ()
check :: Term TyName Name uni fun (Provenance b) -> m ()
check Term TyName Name uni fun (Provenance b)
arg = do
    Bool
shouldCheck <- Getting Bool (CompilationCtx uni fun b) Bool -> m Bool
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((CompilationOpts b -> Const Bool (CompilationOpts b))
-> CompilationCtx uni fun b
-> Const Bool (CompilationCtx uni fun b)
forall (uni :: * -> *) fun a.
Lens' (CompilationCtx uni fun a) (CompilationOpts a)
ccOpts ((CompilationOpts b -> Const Bool (CompilationOpts b))
 -> CompilationCtx uni fun b
 -> Const Bool (CompilationCtx uni fun b))
-> ((Bool -> Const Bool Bool)
    -> CompilationOpts b -> Const Bool (CompilationOpts b))
-> Getting Bool (CompilationCtx uni fun b) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Const Bool Bool)
-> CompilationOpts b -> Const Bool (CompilationOpts b)
forall a. Lens' (CompilationOpts a) Bool
coPedantic)
    -- the typechecker requires global uniqueness, so rename here
    if Bool
shouldCheck then Term TyName Name uni fun (Provenance b) -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a b.
(Compiling m e uni fun a, b ~ Provenance a) =>
Term TyName Name uni fun b -> m ()
typeCheckTerm (Term TyName Name uni fun (Provenance b) -> m ())
-> m (Term TyName Name uni fun (Provenance b)) -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term TyName Name uni fun (Provenance b)
-> m (Term TyName Name uni fun (Provenance b))
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
PLC.rename Term TyName Name uni fun (Provenance b)
arg else () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | The 1st half of the PIR compiler pipeline up to floating/merging the lets.
-- We stop momentarily here to give a chance to the tx-plugin
-- to dump a "readable" version of pir (i.e. floated).
compileToReadable
  :: (Compiling m e uni fun a, b ~ Provenance a)
  => Term TyName Name uni fun a
  -> m (Term TyName Name uni fun b)
compileToReadable :: Term TyName Name uni fun a -> m (Term TyName Name uni fun b)
compileToReadable =
    (Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun a
    -> Term TyName Name uni fun (Provenance a))
-> Term TyName Name uni fun a
-> m (Term TyName Name uni fun (Provenance a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name uni fun a
-> Term TyName Name uni fun (Provenance a)
forall (f :: * -> *) a. Functor f => f a -> f (Provenance a)
original)
    -- We need globally unique names for typechecking, floating, and compiling non-strict bindings
    (Term TyName Name uni fun a
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Term TyName Name uni fun a
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a)
-> m () -> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose String
"  !!! rename")
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
PLC.rename
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a) -> m ())
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through Term TyName Name uni fun (Provenance a) -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a b.
(Compiling m e uni fun a, b ~ Provenance a) =>
Term TyName Name uni fun b -> m ()
typeCheckTerm
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a)
-> m () -> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose String
"  !!! removeDeadBindings")
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall name (uni :: * -> *) fun (m :: * -> *) a.
(HasUnique name TermUnique, ToBuiltinMeaning uni fun,
 MonadQuote m) =>
Term TyName name uni fun a -> m (Term TyName name uni fun a)
DeadCode.removeDeadBindings
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a)
-> m () -> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose String
"  !!! simplifyTerm")
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) e (uni :: * -> *) fun a b.
(Compiling m e uni fun a, b ~ Provenance a) =>
Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplifyTerm
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a)
-> m () -> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose String
"  !!! floatTerm")
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) e (uni :: * -> *) fun a b.
(Compiling m e uni fun a, Semigroup b) =>
Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
floatTerm
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (Term TyName Name uni fun (Provenance a)))
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a) -> m ())
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through Term TyName Name uni fun (Provenance a) -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun b.
Compiling m e uni fun b =>
Term TyName Name uni fun (Provenance b) -> m ()
check

-- | The 2nd half of the PIR compiler pipeline.
-- Compiles a 'Term' into a PLC Term, by removing/translating step-by-step the PIR's language constructs to PLC.
-- Note: the result *does* have globally unique names.
compileReadableToPlc :: (Compiling m e uni fun a, b ~ Provenance a) => Term TyName Name uni fun b -> m (PLCTerm uni fun a)
compileReadableToPlc :: Term TyName Name uni fun b -> m (PLCTerm uni fun a)
compileReadableToPlc =
    (Term TyName Name uni fun (Provenance a)
-> m () -> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose String
"  !!! compileNonStrictBindings")
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Bool
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) (uni :: * -> *) fun a.
MonadQuote m =>
Bool
-> Term TyName Name uni fun a -> m (Term TyName Name uni fun a)
NonStrict.compileNonStrictBindings Bool
False
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a) -> m ())
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through Term TyName Name uni fun (Provenance a) -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun b.
Compiling m e uni fun b =>
Term TyName Name uni fun (Provenance b) -> m ()
check
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a)
-> m () -> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose String
"  !!! thunkRecursions")
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> Term TyName Name uni fun (Provenance a))
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name uni fun (Provenance a)
-> Term TyName Name uni fun (Provenance a)
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a -> Term tyname name uni fun a
ThunkRec.thunkRecursions)
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a) -> m ())
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through Term TyName Name uni fun (Provenance a) -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun b.
Compiling m e uni fun b =>
Term TyName Name uni fun (Provenance b) -> m ()
check
    -- Process only the non-strict bindings created by 'thunkRecursions' with unit delay/forces
    -- See Note [Using unit versus force/delay]
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a)
-> m () -> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose String
"  !!! compileNonStrictBindings")
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Bool
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) (uni :: * -> *) fun a.
MonadQuote m =>
Bool
-> Term TyName Name uni fun a -> m (Term TyName Name uni fun a)
NonStrict.compileNonStrictBindings Bool
True
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a) -> m ())
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through Term TyName Name uni fun (Provenance a) -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun b.
Compiling m e uni fun b =>
Term TyName Name uni fun (Provenance b) -> m ()
check
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a)
-> m () -> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose String
"  !!! compileLets DataTypes")
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> LetKind
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
LetKind -> PIRTerm uni fun a -> m (PIRTerm uni fun a)
Let.compileLets LetKind
Let.DataTypes
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a) -> m ())
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through Term TyName Name uni fun (Provenance a) -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun b.
Compiling m e uni fun b =>
Term TyName Name uni fun (Provenance b) -> m ()
check
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a)
-> m () -> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose String
"  !!! compileLets RecTerms")
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> LetKind
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
LetKind -> PIRTerm uni fun a -> m (PIRTerm uni fun a)
Let.compileLets LetKind
Let.RecTerms
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a) -> m ())
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through Term TyName Name uni fun (Provenance a) -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun b.
Compiling m e uni fun b =>
Term TyName Name uni fun (Provenance b) -> m ()
check
    -- We introduce some non-recursive let bindings while eliminating recursive let-bindings, so we
    -- can eliminate any of them which are unused here.
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a)
-> m () -> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose String
"  !!! removeDeadBindings")
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall name (uni :: * -> *) fun (m :: * -> *) a.
(HasUnique name TermUnique, ToBuiltinMeaning uni fun,
 MonadQuote m) =>
Term TyName name uni fun a -> m (Term TyName name uni fun a)
DeadCode.removeDeadBindings
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a) -> m ())
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through Term TyName Name uni fun (Provenance a) -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun b.
Compiling m e uni fun b =>
Term TyName Name uni fun (Provenance b) -> m ()
check
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a)
-> m () -> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose String
"  !!! simplifyTerm")
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) e (uni :: * -> *) fun a b.
(Compiling m e uni fun a, b ~ Provenance a) =>
Term TyName Name uni fun b -> m (Term TyName Name uni fun b)
simplifyTerm
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a) -> m ())
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through Term TyName Name uni fun (Provenance a) -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun b.
Compiling m e uni fun b =>
Term TyName Name uni fun (Provenance b) -> m ()
check
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a)
-> m () -> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose String
"  !!! compileLets Types")
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> LetKind
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
LetKind -> PIRTerm uni fun a -> m (PIRTerm uni fun a)
Let.compileLets LetKind
Let.Types
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a) -> m ())
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through Term TyName Name uni fun (Provenance a) -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun b.
Compiling m e uni fun b =>
Term TyName Name uni fun (Provenance b) -> m ()
check
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a)
-> m () -> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose String
"  !!! compileLets NonRecTerms")
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> LetKind
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
LetKind -> PIRTerm uni fun a -> m (PIRTerm uni fun a)
Let.compileLets LetKind
Let.NonRecTerms
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a) -> m ())
-> Term TyName Name uni fun (Provenance a)
-> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through Term TyName Name uni fun (Provenance a) -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun b.
Compiling m e uni fun b =>
Term TyName Name uni fun (Provenance b) -> m ()
check
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a)
-> m () -> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose String
"  !!! lowerTerm")
    (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Term TyName Name uni fun (Provenance a) -> m (PLCTerm uni fun a)
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
PIRTerm uni fun a -> m (PLCTerm uni fun a)
lowerTerm

--- | Compile a 'Term' into a PLC Term. Note: the result *does* have globally unique names.
compileTerm :: Compiling m e uni fun a
            => Term TyName Name uni fun a -> m (PLCTerm uni fun a)
compileTerm :: Term TyName Name uni fun a -> m (PLCTerm uni fun a)
compileTerm =
  (Term TyName Name uni fun a
-> m () -> m (Term TyName Name uni fun a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose String
"!!! compileToReadable")
  (Term TyName Name uni fun a -> m (Term TyName Name uni fun a))
-> (Term TyName Name uni fun a -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun a
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Term TyName Name uni fun a
-> m (Term TyName Name uni fun (Provenance a))
forall (m :: * -> *) e (uni :: * -> *) fun a b.
(Compiling m e uni fun a, b ~ Provenance a) =>
Term TyName Name uni fun a -> m (Term TyName Name uni fun b)
compileToReadable
  (Term TyName Name uni fun a
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun a
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Term TyName Name uni fun (Provenance a)
-> m () -> m (Term TyName Name uni fun (Provenance a))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
String -> m ()
logVerbose String
"!!! compileReadableToPlc")
  (Term TyName Name uni fun (Provenance a)
 -> m (Term TyName Name uni fun (Provenance a)))
-> (Term TyName Name uni fun (Provenance a)
    -> m (PLCTerm uni fun a))
-> Term TyName Name uni fun (Provenance a)
-> m (PLCTerm uni fun a)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Term TyName Name uni fun (Provenance a) -> m (PLCTerm uni fun a)
forall (m :: * -> *) e (uni :: * -> *) fun a b.
(Compiling m e uni fun a, b ~ Provenance a) =>
Term TyName Name uni fun b -> m (PLCTerm uni fun a)
compileReadableToPlc