{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}

module Transform.Simplify.Spec where

import Data.Text (Text)
import Data.Vector qualified as V
import PlutusCore qualified as PLC
import PlutusCore.MkPlc (mkConstant, mkIterApp, mkIterAppNoAnn)
import PlutusCore.Quote (Quote, freshName, runQuote)
import Test.Tasty (TestTree, testGroup)
import Transform.Simplify.Lib (goldenVsCse, goldenVsSimplified)
import UntypedPlutusCore
  ( CseWhichSubterms (..)
  , DefaultFun
  , DefaultUni
  , Name
  , Term (..)
  , UVarDecl (..)
  )
import UntypedPlutusCore.MkUPlc (mkIterLamAbs)

basic :: Term Name PLC.DefaultUni PLC.DefaultFun ()
basic :: Term Name DefaultUni DefaultFun ()
basic = ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1

nested :: Term Name PLC.DefaultUni PLC.DefaultFun ()
nested :: Term Name DefaultUni DefaultFun ()
nested = ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1

extraDelays :: Term Name PLC.DefaultUni PLC.DefaultFun ()
extraDelays :: Term Name DefaultUni DefaultFun ()
extraDelays = ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1

interveningLambda :: Term Name PLC.DefaultUni PLC.DefaultFun ()
interveningLambda :: Term Name DefaultUni DefaultFun ()
interveningLambda = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
n <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"a"
  let lam :: Term Name uni fun ()
lam = () -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
n (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$ () -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name uni fun ()
-> Term Name uni fun ()
-> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (() -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
n) (() -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
n)
      arg :: Term Name DefaultUni DefaultFun ()
arg = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term Name DefaultUni DefaultFun ()
 -> Quote (Term Name DefaultUni DefaultFun ()))
-> Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () Term Name DefaultUni DefaultFun ()
forall {uni :: * -> *} {fun}. Term Name uni fun ()
lam Term Name DefaultUni DefaultFun ()
arg

caseOfCase1 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
caseOfCase1 :: Term Name DefaultUni DefaultFun ()
caseOfCase1 = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
b <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"b"
  let ite :: Term name uni DefaultFun ()
ite = () -> Term name uni DefaultFun () -> Term name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (() -> DefaultFun -> Term name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
PLC.IfThenElse)
      true :: Term name uni fun ()
true = () -> Word64 -> [Term name uni fun ()] -> Term name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann
Constr () Word64
0 []
      false :: Term name uni fun ()
false = () -> Word64 -> [Term name uni fun ()] -> Term name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann
Constr () Word64
1 []
      alts :: Vector (Term Name DefaultUni DefaultFun ())
alts = [Term Name DefaultUni DefaultFun ()]
-> Vector (Term Name DefaultUni DefaultFun ())
forall a. [a] -> Vector a
V.fromList [forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1, forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2]
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term Name DefaultUni DefaultFun ()
 -> Quote (Term Name DefaultUni DefaultFun ()))
-> Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Vector (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case () (Term Name DefaultUni DefaultFun ()
-> [((), Term Name DefaultUni DefaultFun ())]
-> Term Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}. Term name uni DefaultFun ()
ite [((), () -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
b), ((), Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *} {fun}. Term name uni fun ()
true), ((), Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *} {fun}. Term name uni fun ()
false)]) Vector (Term Name DefaultUni DefaultFun ())
alts

{-| This should not simplify, because one of the branches of `ifThenElse` is not a `Constr`.
Unless both branches are known constructors, the case-of-case transformation
may increase the program size. -}
caseOfCase2 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
caseOfCase2 :: Term Name DefaultUni DefaultFun ()
caseOfCase2 = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
b <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"b"
  Name
t <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"t"
  let ite :: Term name uni DefaultFun ()
ite = () -> Term name uni DefaultFun () -> Term name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (() -> DefaultFun -> Term name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
PLC.IfThenElse)
      true :: Term Name uni fun ()
true = () -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
t
      false :: Term name uni fun ()
false = () -> Word64 -> [Term name uni fun ()] -> Term name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann
Constr () Word64
1 []
      alts :: Vector (Term Name DefaultUni DefaultFun ())
alts = [Term Name DefaultUni DefaultFun ()]
-> Vector (Term Name DefaultUni DefaultFun ())
forall a. [a] -> Vector a
V.fromList [forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1, forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2]
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term Name DefaultUni DefaultFun ()
 -> Quote (Term Name DefaultUni DefaultFun ()))
-> Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Vector (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case () (Term Name DefaultUni DefaultFun ()
-> [((), Term Name DefaultUni DefaultFun ())]
-> Term Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}. Term name uni DefaultFun ()
ite [((), () -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
b), ((), Term Name DefaultUni DefaultFun ()
forall {uni :: * -> *} {fun}. Term Name uni fun ()
true), ((), Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *} {fun}. Term name uni fun ()
false)]) Vector (Term Name DefaultUni DefaultFun ())
alts

{-| Similar to `caseOfCase1`, but the type of the @true@ and @false@ branches is
@[Integer]@ rather than Bool (note that @Constr 0@ has two parameters, @x@ and @xs@). -}
caseOfCase3 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
caseOfCase3 :: Term Name DefaultUni DefaultFun ()
caseOfCase3 = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
b <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"b"
  Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
  Name
xs <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"xs"
  Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
  let ite :: Term name uni DefaultFun ()
ite = () -> Term name uni DefaultFun () -> Term name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (() -> DefaultFun -> Term name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
PLC.IfThenElse)
      true :: Term Name uni fun ()
true = () -> Word64 -> [Term Name uni fun ()] -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann
Constr () Word64
0 [() -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
x, () -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
xs]
      false :: Term name uni fun ()
false = () -> Word64 -> [Term name uni fun ()] -> Term name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann
Constr () Word64
1 []
      altTrue :: Term Name uni fun ()
altTrue = () -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
f
      altFalse :: Term Name DefaultUni DefaultFun ()
altFalse = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2
      alts :: Vector (Term Name DefaultUni DefaultFun ())
alts = [Term Name DefaultUni DefaultFun ()]
-> Vector (Term Name DefaultUni DefaultFun ())
forall a. [a] -> Vector a
V.fromList [Term Name DefaultUni DefaultFun ()
forall {uni :: * -> *} {fun}. Term Name uni fun ()
altTrue, Term Name DefaultUni DefaultFun ()
altFalse]
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term Name DefaultUni DefaultFun ()
 -> Quote (Term Name DefaultUni DefaultFun ()))
-> Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Vector (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case () (Term Name DefaultUni DefaultFun ()
-> [((), Term Name DefaultUni DefaultFun ())]
-> Term Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}. Term name uni DefaultFun ()
ite [((), () -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
b), ((), Term Name DefaultUni DefaultFun ()
forall {uni :: * -> *} {fun}. Term Name uni fun ()
true), ((), Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *} {fun}. Term name uni fun ()
false)]) Vector (Term Name DefaultUni DefaultFun ())
alts

-- | The `Delay` should be floated into the lambda.
floatDelay1 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
floatDelay1 :: Term Name DefaultUni DefaultFun ()
floatDelay1 = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
a <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"a"
  let body :: Term Name uni DefaultFun ()
body =
        ()
-> Term Name uni DefaultFun ()
-> Term Name uni DefaultFun ()
-> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply
          ()
          (()
-> Term Name uni DefaultFun ()
-> Term Name uni DefaultFun ()
-> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (() -> DefaultFun -> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
PLC.AddInteger) (() -> Term Name uni DefaultFun () -> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (() -> Name -> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
a)))
          (() -> Term Name uni DefaultFun () -> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (() -> Name -> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
a))
      lam :: Term Name uni DefaultFun ()
lam = ()
-> Name
-> Term Name uni DefaultFun ()
-> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
a Term Name uni DefaultFun ()
forall {uni :: * -> *}. Term Name uni DefaultFun ()
body
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term Name DefaultUni DefaultFun ()
 -> Quote (Term Name DefaultUni DefaultFun ()))
-> Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () Term Name DefaultUni DefaultFun ()
forall {uni :: * -> *}. Term Name uni DefaultFun ()
lam (()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1))

{-| The `Delay` should not be floated into the lambda, because the argument (1 + 2)
is not work-free. -}
floatDelay2 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
floatDelay2 :: Term Name DefaultUni DefaultFun ()
floatDelay2 = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
a <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"a"
  let body :: Term Name uni DefaultFun ()
body =
        ()
-> Term Name uni DefaultFun ()
-> Term Name uni DefaultFun ()
-> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply
          ()
          (()
-> Term Name uni DefaultFun ()
-> Term Name uni DefaultFun ()
-> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (() -> DefaultFun -> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
PLC.AddInteger) (() -> Term Name uni DefaultFun () -> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (() -> Name -> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
a)))
          (() -> Term Name uni DefaultFun () -> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (() -> Name -> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
a))
      lam :: Term Name uni DefaultFun ()
lam = ()
-> Name
-> Term Name uni DefaultFun ()
-> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
a Term Name uni DefaultFun ()
forall {uni :: * -> *}. Term Name uni DefaultFun ()
body
      arg :: Term name DefaultUni DefaultFun ()
arg =
        ()
-> Term name DefaultUni DefaultFun ()
-> Term name DefaultUni DefaultFun ()
-> Term name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply
          ()
          (()
-> Term name DefaultUni DefaultFun ()
-> Term name DefaultUni DefaultFun ()
-> Term name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (() -> DefaultFun -> Term name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
PLC.AddInteger) (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1))
          (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2)
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term Name DefaultUni DefaultFun ()
 -> Quote (Term Name DefaultUni DefaultFun ()))
-> Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () Term Name DefaultUni DefaultFun ()
forall {uni :: * -> *}. Term Name uni DefaultFun ()
lam (()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term Name DefaultUni DefaultFun ()
forall {name}. Term name DefaultUni DefaultFun ()
arg)

{-| The `Delay` should not be floated into the lambda in the first simplifier iteration,
because one of the occurrences of `a` is not under `Force`. It should be floated into
the lambda in the second simplifier iteration, after `b` is inlined. -}
floatDelay3 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
floatDelay3 :: Term Name DefaultUni DefaultFun ()
floatDelay3 = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
a <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"a"
  Name
b <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"b"
  let secondArg :: Term Name uni fun ()
secondArg = () -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (()
-> Term Name uni fun ()
-> Term Name uni fun ()
-> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (() -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
b (() -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
b)) (() -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
a))
      body :: Term Name uni DefaultFun ()
body = ()
-> Term Name uni DefaultFun ()
-> Term Name uni DefaultFun ()
-> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (()
-> Term Name uni DefaultFun ()
-> Term Name uni DefaultFun ()
-> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (() -> DefaultFun -> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
PLC.AddInteger) (() -> Term Name uni DefaultFun () -> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (() -> Name -> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
a))) Term Name uni DefaultFun ()
forall {uni :: * -> *} {fun}. Term Name uni fun ()
secondArg
      lam :: Term Name uni DefaultFun ()
lam = ()
-> Name
-> Term Name uni DefaultFun ()
-> Term Name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
a Term Name uni DefaultFun ()
forall {uni :: * -> *}. Term Name uni DefaultFun ()
body
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term Name DefaultUni DefaultFun ()
 -> Quote (Term Name DefaultUni DefaultFun ()))
-> Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () Term Name DefaultUni DefaultFun ()
forall {uni :: * -> *}. Term Name uni DefaultFun ()
lam (()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1))

basicInline :: Term Name PLC.DefaultUni PLC.DefaultFun ()
basicInline :: Term Name DefaultUni DefaultFun ()
basicInline = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
n <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"a"
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term Name DefaultUni DefaultFun ()
 -> Quote (Term Name DefaultUni DefaultFun ()))
-> Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
n (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
n)) (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1)

{-| A helper function to create a term which tests whether the inliner
behaves as expected for a given pure or impure term. It receives
a 'Quote' that produces a term together with a list of free variables.
The free variables are bound at the top level of the final term in order
to ensure that the produced final term is well-scoped. -}
mkInlinePurityTest
  :: Quote ([Name], Term Name PLC.DefaultUni PLC.DefaultFun ())
  -> Term Name PLC.DefaultUni PLC.DefaultFun ()
mkInlinePurityTest :: Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
mkInlinePurityTest Quote ([Name], Term Name DefaultUni DefaultFun ())
termToInline = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
a <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"a"
  Name
b <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"b"
  -- In `[(\a . \b . a) termToInline]`, `termToInline` will be inlined
  -- if and only if it is pure.
  ([Name]
freeVars, Term Name DefaultUni DefaultFun ()
term) <- Quote ([Name], Term Name DefaultUni DefaultFun ())
termToInline
  let withTopLevelBindings :: Term Name uni fun () -> Term Name uni fun ()
withTopLevelBindings =
        [UVarDecl Name ()] -> Term Name uni fun () -> Term Name uni fun ()
forall name ann (uni :: * -> *) fun.
[UVarDecl name ann]
-> Term name uni fun ann -> Term name uni fun ann
mkIterLamAbs
          (() -> Name -> UVarDecl Name ()
forall name ann. ann -> name -> UVarDecl name ann
UVarDecl () (Name -> UVarDecl Name ()) -> [Name] -> [UVarDecl Name ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
freeVars)
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term Name DefaultUni DefaultFun ()
 -> Quote (Term Name DefaultUni DefaultFun ()))
-> Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$
    Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {uni :: * -> *} {fun}.
Term Name uni fun () -> Term Name uni fun ()
withTopLevelBindings (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
      ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
a (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
b (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
a) Term Name DefaultUni DefaultFun ()
term

-- | A single @Var@ is pure.
inlinePure1 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
inlinePure1 :: Term Name DefaultUni DefaultFun ()
inlinePure1 = Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
mkInlinePurityTest (Quote ([Name], Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
a <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"a"
  ([Name], Term Name DefaultUni DefaultFun ())
-> Quote ([Name], Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Name
a], () -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
a)

{-| @force (delay a)@ is pure.

Note that this relies on @forceDelayCancel@ to cancel the @force@ and the @delay@,
otherwise the inliner would treat the term as impure. -}
inlinePure2 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
inlinePure2 :: Term Name DefaultUni DefaultFun ()
inlinePure2 = Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
mkInlinePurityTest (Quote ([Name], Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
a <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"a"
  ([Name], Term Name DefaultUni DefaultFun ())
-> Quote ([Name], Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Name
a], ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
a)

{-| @[(\x -> \y -> [x x]) (con integer 1)]@ is pure.

Note that the @(con integer 1)@ won't get inlined: it isn't pre-inlined because
@x@ occurs twice, and it isn't post-inlined because @costIsAcceptable Constant{} = False@.
However, the entire term will be inlined since it is pure. -}
inlinePure3 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
inlinePure3 :: Term Name DefaultUni DefaultFun ()
inlinePure3 = Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
mkInlinePurityTest (Quote ([Name], Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
  Name
y <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"y"
  let t :: Term Name DefaultUni fun ()
t =
        ()
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply
          ()
          (()
-> Name
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
x (Term Name DefaultUni fun () -> Term Name DefaultUni fun ())
-> Term Name DefaultUni fun () -> Term Name DefaultUni fun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Name
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
y (Term Name DefaultUni fun () -> Term Name DefaultUni fun ())
-> Term Name DefaultUni fun () -> Term Name DefaultUni fun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (() -> Name -> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
x) (() -> Name -> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
x))
          (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1)
      vars :: [a]
vars = []
  ([Name], Term Name DefaultUni DefaultFun ())
-> Quote ([Name], Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Name]
forall a. [a]
vars, Term Name DefaultUni DefaultFun ()
forall {fun}. Term Name DefaultUni fun ()
t)

{-| @force ([(\x -> delay (\y -> [x x])) (delay ([error (con integer 1)]))])@ is pure,
but it is very tricky to see so. It requires us to match up a force and a
delay through several steps of intervening computation. -}
inlinePure4 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
inlinePure4 :: Term Name DefaultUni DefaultFun ()
inlinePure4 = Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
mkInlinePurityTest (Quote ([Name], Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
  Name
y <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"y"
  let term :: Term Name DefaultUni fun ()
term =
        () -> Term Name DefaultUni fun () -> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni fun () -> Term Name DefaultUni fun ())
-> Term Name DefaultUni fun () -> Term Name DefaultUni fun ()
forall a b. (a -> b) -> a -> b
$
          ()
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply
            ()
            (()
-> Name
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
x (Term Name DefaultUni fun () -> Term Name DefaultUni fun ())
-> Term Name DefaultUni fun () -> Term Name DefaultUni fun ()
forall a b. (a -> b) -> a -> b
$ () -> Term Name DefaultUni fun () -> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni fun () -> Term Name DefaultUni fun ())
-> Term Name DefaultUni fun () -> Term Name DefaultUni fun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Name
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
y (Term Name DefaultUni fun () -> Term Name DefaultUni fun ())
-> Term Name DefaultUni fun () -> Term Name DefaultUni fun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (() -> Name -> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
x) (() -> Name -> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
x))
            (() -> Term Name DefaultUni fun () -> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni fun () -> Term Name DefaultUni fun ())
-> Term Name DefaultUni fun () -> Term Name DefaultUni fun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (() -> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
Error ()) (Term Name DefaultUni fun () -> Term Name DefaultUni fun ())
-> Term Name DefaultUni fun () -> Term Name DefaultUni fun ()
forall a b. (a -> b) -> a -> b
$ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1)
  ([Name], Term Name DefaultUni DefaultFun ())
-> Quote ([Name], Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], Term Name DefaultUni DefaultFun ()
forall {fun}. Term Name DefaultUni fun ()
term)

-- | @error@ is impure.
inlineImpure1 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
inlineImpure1 :: Term Name DefaultUni DefaultFun ()
inlineImpure1 = Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
mkInlinePurityTest (Quote ([Name], Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ([Name], Term Name DefaultUni DefaultFun ())
-> Quote ([Name], Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], () -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
Error ())

-- | @force (delay error)@ is impure.
inlineImpure2 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
inlineImpure2 :: Term Name DefaultUni DefaultFun ()
inlineImpure2 = Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
mkInlinePurityTest (Quote ([Name], Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ([Name], Term Name DefaultUni DefaultFun ())
-> Quote ([Name], Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> (Term Name DefaultUni DefaultFun ()
    -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ () -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
Error ())

{-| @force (force (force (delay (delay (delay (error))))))@ is impure, since it
is the same as @error@. -}
inlineImpure3 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
inlineImpure3 :: Term Name DefaultUni DefaultFun ()
inlineImpure3 =
  Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
mkInlinePurityTest (Quote ([Name], Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
    ([Name], Term Name DefaultUni DefaultFun ())
-> Quote ([Name], Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      ( []
      , ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force ()
          (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> (Term Name DefaultUni DefaultFun ()
    -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force ()
          (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> (Term Name DefaultUni DefaultFun ()
    -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force ()
          (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> (Term Name DefaultUni DefaultFun ()
    -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay ()
          (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> (Term Name DefaultUni DefaultFun ()
    -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay ()
          (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> (Term Name DefaultUni DefaultFun ()
    -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay ()
          (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ () -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
Error ()
      )

{-| @force (force (force (delay (delay a))))@ is impure, since @a@ may expand
to an impure term such as @error@. -}
inlineImpure4 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
inlineImpure4 :: Term Name DefaultUni DefaultFun ()
inlineImpure4 = Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
mkInlinePurityTest (Quote ([Name], Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote ([Name], Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
a <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"a"
  let term :: Term Name uni fun ()
term =
        () -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force ()
          (Term Name uni fun () -> Term Name uni fun ())
-> (Name -> Term Name uni fun ()) -> Name -> Term Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force ()
          (Term Name uni fun () -> Term Name uni fun ())
-> (Name -> Term Name uni fun ()) -> Name -> Term Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force ()
          (Term Name uni fun () -> Term Name uni fun ())
-> (Name -> Term Name uni fun ()) -> Name -> Term Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay ()
          (Term Name uni fun () -> Term Name uni fun ())
-> (Name -> Term Name uni fun ()) -> Name -> Term Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay ()
          (Term Name uni fun () -> Term Name uni fun ())
-> (Name -> Term Name uni fun ()) -> Name -> Term Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var ()
          (Name -> Term Name uni fun ()) -> Name -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$ Name
a
  ([Name], Term Name DefaultUni DefaultFun ())
-> Quote ([Name], Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Name
a], Term Name DefaultUni DefaultFun ()
forall {uni :: * -> *} {fun}. Term Name uni fun ()
term)

{-| @(\a -> f (a 0 1) (a 2)) (\x y -> g x y)@

The first occurrence of `a` should be inlined because doing so does not increase
the size or the cost.

The second occurrence of `a` should be unconditionally inlined in the second simplifier
iteration, but in this test we are only running one iteration. -}
callsiteInline :: Term Name PLC.DefaultUni PLC.DefaultFun ()
callsiteInline :: Term Name DefaultUni DefaultFun ()
callsiteInline = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
a <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"a"
  Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
  Name
g <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"g"
  Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
  Name
y <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"y"
  let fun :: Term Name DefaultUni fun ()
fun =
        ()
-> Name
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
a (Term Name DefaultUni fun () -> Term Name DefaultUni fun ())
-> Term Name DefaultUni fun () -> Term Name DefaultUni fun ()
forall a b. (a -> b) -> a -> b
$
          Term Name DefaultUni fun ()
-> [Term Name DefaultUni fun ()] -> Term Name DefaultUni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
            (() -> Name -> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
f)
            [ Term Name DefaultUni fun ()
-> [Term Name DefaultUni fun ()] -> Term Name DefaultUni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> Name -> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
a) [forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0, forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1]
            , Term Name DefaultUni fun ()
-> [Term Name DefaultUni fun ()] -> Term Name DefaultUni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> Name -> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
a) [forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2]
            ]
      arg :: Term Name uni fun ()
arg = () -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
x (Term Name uni fun () -> Term Name uni fun ())
-> (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun ()
-> Term Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
y (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$ Term Name uni fun ()
-> [Term Name uni fun ()] -> Term Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
g) [() -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
y, () -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
x]
      termWithBoundTopLevel :: Term Name DefaultUni fun ()
termWithBoundTopLevel = ()
-> Name
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
f (Term Name DefaultUni fun () -> Term Name DefaultUni fun ())
-> Term Name DefaultUni fun () -> Term Name DefaultUni fun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Name
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
g (Term Name DefaultUni fun () -> Term Name DefaultUni fun ())
-> Term Name DefaultUni fun () -> Term Name DefaultUni fun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
-> Term Name DefaultUni fun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () Term Name DefaultUni fun ()
forall {fun}. Term Name DefaultUni fun ()
fun Term Name DefaultUni fun ()
forall {uni :: * -> *} {fun}. Term Name uni fun ()
arg
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term Name DefaultUni DefaultFun ()
forall {fun}. Term Name DefaultUni fun ()
termWithBoundTopLevel

multiApp :: Term Name PLC.DefaultUni PLC.DefaultFun ()
multiApp :: Term Name DefaultUni DefaultFun ()
multiApp = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
a <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"a"
  Name
b <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"b"
  Name
c <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"c"
  let lam :: Term Name uni fun ()
lam = () -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
a (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
b (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
c (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$ Term Name uni fun ()
-> [Term Name uni fun ()] -> Term Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
c) [() -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
a, () -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
b]
      app :: Term Name DefaultUni fun ()
app =
        Term Name DefaultUni fun ()
-> [Term Name DefaultUni fun ()] -> Term Name DefaultUni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          Term Name DefaultUni fun ()
forall {uni :: * -> *} {fun}. Term Name uni fun ()
lam
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
3
          ]
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term Name DefaultUni DefaultFun ()
forall {fun}. Term Name DefaultUni fun ()
app

forceDelayNoApps :: Term Name PLC.DefaultUni PLC.DefaultFun ()
forceDelayNoApps :: Term Name DefaultUni DefaultFun ()
forceDelayNoApps = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  let one :: Term Name DefaultUni DefaultFun ()
one = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1
      term :: Term Name DefaultUni DefaultFun ()
term = ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term Name DefaultUni DefaultFun ()
one
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term Name DefaultUni DefaultFun ()
term

forceDelayNoAppsLayered :: Term Name PLC.DefaultUni PLC.DefaultFun ()
forceDelayNoAppsLayered :: Term Name DefaultUni DefaultFun ()
forceDelayNoAppsLayered = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  let one :: Term Name DefaultUni DefaultFun ()
one = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1
      term :: Term Name DefaultUni DefaultFun ()
term = ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term Name DefaultUni DefaultFun ()
one
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term Name DefaultUni DefaultFun ()
term

{-| The UPLC term in this test should come from the following TPLC term after erasing its types:

> (/\(p :: *) -> \(x : p) -> /\(q :: *) -> \(y : q) -> /\(r :: *) -> \(z : r) -> z)
>   Int 1 Int 2 Int 3

This case is simple in the sense that each type abstraction
is followed by a single term abstraction. -}
forceDelaySimple :: Term Name PLC.DefaultUni PLC.DefaultFun ()
forceDelaySimple :: Term Name DefaultUni DefaultFun ()
forceDelaySimple = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
  Name
y <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"y"
  Name
z <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"z"
  let one :: Term Name DefaultUni DefaultFun ()
one = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1
      two :: Term Name DefaultUni DefaultFun ()
two = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2
      three :: Term Name DefaultUni DefaultFun ()
three = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
3
      t :: Term Name uni fun ()
t = () -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (() -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
x (() -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (() -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
y (() -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (() -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
z (() -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
z))))))
      app :: Term Name DefaultUni DefaultFun ()
app = ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () Term Name DefaultUni DefaultFun ()
forall {uni :: * -> *} {fun}. Term Name uni fun ()
t) Term Name DefaultUni DefaultFun ()
one)) Term Name DefaultUni DefaultFun ()
two)) Term Name DefaultUni DefaultFun ()
three
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term Name DefaultUni DefaultFun ()
app

{-| A test for the case when there are multiple applications between the 'Force' at the top
and the 'Delay' at the top of the term inside the abstractions/applications. -}
forceDelayMultiApply :: Term Name PLC.DefaultUni PLC.DefaultFun ()
forceDelayMultiApply :: Term Name DefaultUni DefaultFun ()
forceDelayMultiApply = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
x1 <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x1"
  Name
x2 <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x2"
  Name
x3 <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x3"
  Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
  Name
funcVar <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"funcVar"
  let one :: Term Name DefaultUni DefaultFun ()
one = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1
      two :: Term Name DefaultUni DefaultFun ()
two = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2
      three :: Term Name DefaultUni DefaultFun ()
three = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
3
      term :: Term Name DefaultUni DefaultFun ()
term =
        ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
funcVar (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
          ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
            Term Name DefaultUni DefaultFun ()
-> [Term Name DefaultUni DefaultFun ()]
-> Term Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              ( ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
x1 (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
                  ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
x2 (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
                    ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
x3 (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
                      ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
f (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
                        ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
                          Term Name DefaultUni DefaultFun ()
-> [Term Name DefaultUni DefaultFun ()]
-> Term Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
f) [() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
x1, () -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
x2, () -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
x3]
              )
              [Term Name DefaultUni DefaultFun ()
one, Term Name DefaultUni DefaultFun ()
two, Term Name DefaultUni DefaultFun ()
three, () -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
funcVar]
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term Name DefaultUni DefaultFun ()
term

{-| A test for the case when there are multiple type abstractions over a single term
abstraction/application. -}
forceDelayMultiForce :: Term Name PLC.DefaultUni PLC.DefaultFun ()
forceDelayMultiForce :: Term Name DefaultUni DefaultFun ()
forceDelayMultiForce = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
  let one :: Term Name DefaultUni DefaultFun ()
one = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1
      term :: Term Name DefaultUni DefaultFun ()
term =
        ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
          ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
            ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
              ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply
                ()
                ( ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
x (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
                    ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
                      ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
                        ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
                          () -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
x
                )
                Term Name DefaultUni DefaultFun ()
one
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term Name DefaultUni DefaultFun ()
term

{-| The UPLC term in this test should come from the following TPLC term after erasing its types:

> (/\(p1 :: *) (p2 :: *) -> \(x : p2) ->
>   /\(q1 :: *) (q2 :: *) (q3 :: *) -> \(y1 : q1) (y2 : q2) (y3 : String) ->
>     /\(r :: *) -> \(z1 : r) -> \(z2 : r) ->
>       /\(t :: *) -> \(f : p1 -> q1 -> q2 -> String -> r -> r -> String) ->
>         f x y1 y2 y3 z1 z2
> ) Int Int 1 Int String Int 2 "foo" "bar" Int 3 3 ByteString
> (funcVar : Int -> Int -> String -> String -> Int -> String)

Note this term has multiple interleaved type and term instantiations/applications. -}
forceDelayComplex :: Term Name PLC.DefaultUni PLC.DefaultFun ()
forceDelayComplex :: Term Name DefaultUni DefaultFun ()
forceDelayComplex = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
  Name
y1 <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"y1"
  Name
y2 <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"y2"
  Name
y3 <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"y3"
  Name
z1 <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"z1"
  Name
z2 <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"z2"
  Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
  Name
funcVar <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"funcVar"
  let one :: Term Name DefaultUni DefaultFun ()
one = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1
      two :: Term Name DefaultUni DefaultFun ()
two = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2
      three :: Term Name DefaultUni DefaultFun ()
three = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
3
      foo :: Term Name DefaultUni DefaultFun ()
foo = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Text () Text
"foo"
      bar :: Term Name DefaultUni DefaultFun ()
bar = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Text () Text
"bar"
      term :: Term Name uni fun ()
term =
        () -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$
          () -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$
            () -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
x (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$
              () -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$
                () -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$
                  () -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$
                    () -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
y1 (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$
                      () -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
y2 (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$
                        () -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
y3 (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$
                          () -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$
                            () -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
z1 (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$
                              () -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
z2 (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$
                                () -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$
                                  () -> Name -> Term Name uni fun () -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
f (Term Name uni fun () -> Term Name uni fun ())
-> Term Name uni fun () -> Term Name uni fun ()
forall a b. (a -> b) -> a -> b
$
                                    Term Name uni fun ()
-> [Term Name uni fun ()] -> Term Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
                                      (() -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
f)
                                      [ () -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
x
                                      , () -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
y1
                                      , () -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
y2
                                      , () -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
y3
                                      , () -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
z1
                                      , () -> Name -> Term Name uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
z2
                                      ]
      app :: Term Name DefaultUni DefaultFun ()
app =
        ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
funcVar (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
          ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply
            ()
            ( ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
                Term Name DefaultUni DefaultFun ()
-> [Term Name DefaultUni DefaultFun ()]
-> Term Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
                  ( ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
                      Term Name DefaultUni DefaultFun ()
-> [Term Name DefaultUni DefaultFun ()]
-> Term Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
                        ( ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
                            ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
                              ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
                                ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply
                                  ()
                                  (()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () Term Name DefaultUni DefaultFun ()
forall {uni :: * -> *} {fun}. Term Name uni fun ()
term)
                                  Term Name DefaultUni DefaultFun ()
one
                        )
                        [Term Name DefaultUni DefaultFun ()
two, Term Name DefaultUni DefaultFun ()
foo, Term Name DefaultUni DefaultFun ()
bar]
                  )
                  [Term Name DefaultUni DefaultFun ()
three, Term Name DefaultUni DefaultFun ()
three]
            )
            (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
funcVar)
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term Name DefaultUni DefaultFun ()
app

forceCaseDelayNoApps1 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
forceCaseDelayNoApps1 :: Term Name DefaultUni DefaultFun ()
forceCaseDelayNoApps1 = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
scrut <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"scrut"
  let one :: Term Name DefaultUni DefaultFun ()
one = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1
      term :: Term Name DefaultUni DefaultFun ()
term =
        ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
scrut (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
          ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
            ()
-> Term Name DefaultUni DefaultFun ()
-> Vector (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case () (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
scrut) ([Term Name DefaultUni DefaultFun ()]
-> Vector (Term Name DefaultUni DefaultFun ())
forall a. [a] -> Vector a
V.fromList [()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term Name DefaultUni DefaultFun ()
one])
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term Name DefaultUni DefaultFun ()
term

forceCaseDelayWithApps1 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
forceCaseDelayWithApps1 :: Term Name DefaultUni DefaultFun ()
forceCaseDelayWithApps1 = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
scrut <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"scrut"
  Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
  let one :: Term Name DefaultUni DefaultFun ()
one = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1
      term :: Term Name DefaultUni DefaultFun ()
term =
        ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
scrut (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
          ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
            ()
-> Term Name DefaultUni DefaultFun ()
-> Vector (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case
              ()
              (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
scrut)
              ([Term Name DefaultUni DefaultFun ()]
-> Vector (Term Name DefaultUni DefaultFun ())
forall a. [a] -> Vector a
V.fromList [()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
x (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term Name DefaultUni DefaultFun ()
one])
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term Name DefaultUni DefaultFun ()
term

forceCaseDelayNoApps2 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
forceCaseDelayNoApps2 :: Term Name DefaultUni DefaultFun ()
forceCaseDelayNoApps2 = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
scrut <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"scrut"
  let one :: Term Name DefaultUni DefaultFun ()
one = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1
      two :: Term Name DefaultUni DefaultFun ()
two = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2
      term :: Term Name DefaultUni DefaultFun ()
term =
        ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
scrut (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
          ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
            ()
-> Term Name DefaultUni DefaultFun ()
-> Vector (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case
              ()
              (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
scrut)
              ([Term Name DefaultUni DefaultFun ()]
-> Vector (Term Name DefaultUni DefaultFun ())
forall a. [a] -> Vector a
V.fromList [()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term Name DefaultUni DefaultFun ()
one, ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term Name DefaultUni DefaultFun ()
two])
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term Name DefaultUni DefaultFun ()
term

forceCaseDelayWithApps2 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
forceCaseDelayWithApps2 :: Term Name DefaultUni DefaultFun ()
forceCaseDelayWithApps2 = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
scrut <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"scrut"
  Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
  let one :: Term Name DefaultUni DefaultFun ()
one = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1
      two :: Term Name DefaultUni DefaultFun ()
two = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2
      term :: Term Name DefaultUni DefaultFun ()
term =
        ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
scrut (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
          ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
            ()
-> Term Name DefaultUni DefaultFun ()
-> Vector (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case
              ()
              (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
scrut)
              ([Term Name DefaultUni DefaultFun ()]
-> Vector (Term Name DefaultUni DefaultFun ())
forall a. [a] -> Vector a
V.fromList [()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
x (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term Name DefaultUni DefaultFun ()
one, ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term Name DefaultUni DefaultFun ()
two])
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term Name DefaultUni DefaultFun ()
term

forceCaseDelayNoApps2Fail :: Term Name PLC.DefaultUni PLC.DefaultFun ()
forceCaseDelayNoApps2Fail :: Term Name DefaultUni DefaultFun ()
forceCaseDelayNoApps2Fail = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
scrut <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"scrut"
  let one :: Term Name DefaultUni DefaultFun ()
one = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1
      two :: Term Name DefaultUni DefaultFun ()
two = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2
      term :: Term Name DefaultUni DefaultFun ()
term =
        ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
scrut (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
          ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
            ()
-> Term Name DefaultUni DefaultFun ()
-> Vector (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case
              ()
              (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
scrut)
              ([Term Name DefaultUni DefaultFun ()]
-> Vector (Term Name DefaultUni DefaultFun ())
forall a. [a] -> Vector a
V.fromList [()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term Name DefaultUni DefaultFun ()
one, Term Name DefaultUni DefaultFun ()
two])
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term Name DefaultUni DefaultFun ()
term

forceCaseDelayWithApps2Fail :: Term Name PLC.DefaultUni PLC.DefaultFun ()
forceCaseDelayWithApps2Fail :: Term Name DefaultUni DefaultFun ()
forceCaseDelayWithApps2Fail = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
scrut <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"scrut"
  Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
  Name
y <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"y"
  let one :: Term Name DefaultUni DefaultFun ()
one = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1
      two :: Term Name DefaultUni DefaultFun ()
two = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2
      term :: Term Name DefaultUni DefaultFun ()
term =
        ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
scrut (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
          ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
            ()
-> Term Name DefaultUni DefaultFun ()
-> Vector (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case
              ()
              (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
scrut)
              ( [Term Name DefaultUni DefaultFun ()]
-> Vector (Term Name DefaultUni DefaultFun ())
forall a. [a] -> Vector a
V.fromList
                  [ ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
x (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
y (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term Name DefaultUni DefaultFun ()
one
                  , ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
x Term Name DefaultUni DefaultFun ()
two
                  ]
              )
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term Name DefaultUni DefaultFun ()
term

-- | This is the first example in Note [CSE].
cse1 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
cse1 :: Term Name DefaultUni DefaultFun ()
cse1 = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
  Name
y <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"y"
  let plus :: Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus Term name uni DefaultFun ()
a Term name uni DefaultFun ()
b = Term name uni DefaultFun ()
-> [((), Term name uni DefaultFun ())]
-> Term name uni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp (() -> DefaultFun -> Term name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
PLC.AddInteger) [((), Term name uni DefaultFun ()
a), ((), Term name uni DefaultFun ()
b)]
      body :: Term Name DefaultUni DefaultFun ()
body = Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus Term Name DefaultUni DefaultFun ()
onePlusTwoPlusX Term Name DefaultUni DefaultFun ()
caseExpr
      con :: Integer -> Term Name DefaultUni DefaultFun ()
con = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer ()
      twoPlusX :: Term Name DefaultUni DefaultFun ()
twoPlusX = Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
2) (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
x)
      onePlusTwoPlusX :: Term Name DefaultUni DefaultFun ()
onePlusTwoPlusX = Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
1) Term Name DefaultUni DefaultFun ()
twoPlusX
      threePlusX :: Term Name DefaultUni DefaultFun ()
threePlusX = Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
3) (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
x)
      fourPlusX :: Term Name DefaultUni DefaultFun ()
fourPlusX = Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
4) (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
x)
      branch1 :: Term Name DefaultUni DefaultFun ()
branch1 = Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus Term Name DefaultUni DefaultFun ()
onePlusTwoPlusX Term Name DefaultUni DefaultFun ()
threePlusX
      branch2 :: Term Name DefaultUni DefaultFun ()
branch2 = Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus Term Name DefaultUni DefaultFun ()
twoPlusX Term Name DefaultUni DefaultFun ()
threePlusX
      branch3 :: Term Name DefaultUni DefaultFun ()
branch3 = Term Name DefaultUni DefaultFun ()
fourPlusX
      caseExpr :: Term Name DefaultUni DefaultFun ()
caseExpr = ()
-> Term Name DefaultUni DefaultFun ()
-> Vector (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case () (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
y) ([Term Name DefaultUni DefaultFun ()]
-> Vector (Term Name DefaultUni DefaultFun ())
forall a. [a] -> Vector a
V.fromList [Term Name DefaultUni DefaultFun ()
branch1, Term Name DefaultUni DefaultFun ()
branch2, Term Name DefaultUni DefaultFun ()
branch3])
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term Name DefaultUni DefaultFun ()
 -> Quote (Term Name DefaultUni DefaultFun ()))
-> Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
x (()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
y Term Name DefaultUni DefaultFun ()
body)

-- | This is the second example in Note [CSE].
cse2 :: Term Name DefaultUni DefaultFun ()
cse2 :: Term Name DefaultUni DefaultFun ()
cse2 = ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () (()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () Term Name DefaultUni DefaultFun ()
body)
  where
    plus :: Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus Term name uni DefaultFun ()
a Term name uni DefaultFun ()
b = Term name uni DefaultFun ()
-> [((), Term name uni DefaultFun ())]
-> Term name uni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp (() -> DefaultFun -> Term name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
PLC.AddInteger) [((), Term name uni DefaultFun ()
a), ((), Term name uni DefaultFun ()
b)]
    con :: Integer -> Term Name DefaultUni DefaultFun ()
con = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer ()
    body :: Term Name DefaultUni DefaultFun ()
body = Term Name DefaultUni DefaultFun ()
-> [((), Term Name DefaultUni DefaultFun ())]
-> Term Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp (() -> DefaultFun -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
PLC.IfThenElse) [((), Term Name DefaultUni DefaultFun ()
cond), ((), Term Name DefaultUni DefaultFun ()
true), ((), Term Name DefaultUni DefaultFun ()
false)]
    cond :: Term Name DefaultUni DefaultFun ()
cond = ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () (() -> DefaultFun -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
PLC.LessThanInteger) (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
0)) (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
0)
    true :: Term Name DefaultUni DefaultFun ()
true = ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
1) (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
2)) (Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
1) (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
2)))
    false :: Term Name DefaultUni DefaultFun ()
false = ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () (Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
1) (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
2))

-- | This is the third example in Note [CSE].
cse3 :: Term Name PLC.DefaultUni PLC.DefaultFun ()
cse3 :: Term Name DefaultUni DefaultFun ()
cse3 = Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term Name DefaultUni DefaultFun ())
 -> Term Name DefaultUni DefaultFun ())
-> Quote (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
  Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
  Name
y <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"y"
  Name
z <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"z"
  Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
  let plus :: Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus Term name uni DefaultFun ()
a Term name uni DefaultFun ()
b = Term name uni DefaultFun ()
-> [((), Term name uni DefaultFun ())]
-> Term name uni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp (() -> DefaultFun -> Term name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
PLC.AddInteger) [((), Term name uni DefaultFun ()
a), ((), Term name uni DefaultFun ()
b)]
      con :: Integer -> Term Name DefaultUni DefaultFun ()
con = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer ()
      arg1 :: Term Name DefaultUni DefaultFun ()
arg1 =
        Term Name DefaultUni DefaultFun ()
-> [((), Term Name DefaultUni DefaultFun ())]
-> Term Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp
          (()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
y (Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
1) (Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
y) (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
y))))
          [((), Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
0) (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
x))]
      arg2 :: Term Name DefaultUni DefaultFun ()
arg2 =
        Term Name DefaultUni DefaultFun ()
-> [((), Term Name DefaultUni DefaultFun ())]
-> Term Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp
          (()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
z (Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
2) (Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
z) (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
z))))
          [((), Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
0) (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
x))]
  Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term Name DefaultUni DefaultFun ()
 -> Quote (Term Name DefaultUni DefaultFun ()))
-> Term Name DefaultUni DefaultFun ()
-> Quote (Term Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
f (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () Name
x (Term Name DefaultUni DefaultFun ()
-> [((), Term Name DefaultUni DefaultFun ())]
-> Term Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp (() -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () Name
f) [((), Term Name DefaultUni DefaultFun ()
arg1), ((), Term Name DefaultUni DefaultFun ()
arg2)])

--  ((1+2) + (3+4) + ...)
--  +
--  ((1+2) + (3+4) + ...)
cseExpensive :: Term Name DefaultUni DefaultFun ()
cseExpensive :: Term Name DefaultUni DefaultFun ()
cseExpensive = Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus Term Name DefaultUni DefaultFun ()
arg Term Name DefaultUni DefaultFun ()
arg'
  where
    plus :: Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus Term name uni DefaultFun ()
a Term name uni DefaultFun ()
b = Term name uni DefaultFun ()
-> [((), Term name uni DefaultFun ())]
-> Term name uni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp (() -> DefaultFun -> Term name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
PLC.AddInteger) [((), Term name uni DefaultFun ()
a), ((), Term name uni DefaultFun ()
b)]
    con :: Integer -> Term Name DefaultUni DefaultFun ()
con = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer ()
    mkArg :: [Integer] -> Term Name DefaultUni DefaultFun ()
mkArg = (Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> [Term Name DefaultUni DefaultFun ()]
-> Term Name DefaultUni DefaultFun ()
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus ([Term Name DefaultUni DefaultFun ()]
 -> Term Name DefaultUni DefaultFun ())
-> ([Integer] -> [Term Name DefaultUni DefaultFun ()])
-> [Integer]
-> Term Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Term Name DefaultUni DefaultFun ())
-> [Integer] -> [Term Name DefaultUni DefaultFun ()]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Integer
i -> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (Integer -> Term Name DefaultUni DefaultFun ()
con (Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
i)) (Integer -> Term Name DefaultUni DefaultFun ()
con (Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)))
    arg :: Term Name DefaultUni DefaultFun ()
arg = [Integer] -> Term Name DefaultUni DefaultFun ()
mkArg [Integer
0 .. Integer
200]
    arg' :: Term Name DefaultUni DefaultFun ()
arg' = [Integer] -> Term Name DefaultUni DefaultFun ()
mkArg [Integer
0 .. Integer
200]

-- tree where nodes are + and leaves are constants
csePlusTree :: Term Name DefaultUni DefaultFun ()
csePlusTree :: Term Name DefaultUni DefaultFun ()
csePlusTree = Int -> Term Name DefaultUni DefaultFun ()
go Int
5
  where
    go :: Int -> Term Name DefaultUni DefaultFun ()
    go :: Int -> Term Name DefaultUni DefaultFun ()
go Int
0 = Integer -> Term Name DefaultUni DefaultFun ()
con Integer
1
    go Int
n = Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (Int -> Term Name DefaultUni DefaultFun ()
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)) (Int -> Term Name DefaultUni DefaultFun ()
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))

    plus :: Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus Term name uni DefaultFun ()
a Term name uni DefaultFun ()
b = Term name uni DefaultFun ()
-> [((), Term name uni DefaultFun ())]
-> Term name uni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp (() -> DefaultFun -> Term name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
PLC.AddInteger) [((), Term name uni DefaultFun ()
a), ((), Term name uni DefaultFun ()
b)]
    con :: Integer -> Term Name DefaultUni DefaultFun ()
con = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer ()

-- (1 + (1 + ... + 0))
-- optimised to
-- let f = (1 +) in f (f (... 0))
cseRepeatPlus :: Term Name DefaultUni DefaultFun ()
cseRepeatPlus :: Term Name DefaultUni DefaultFun ()
cseRepeatPlus = Int -> Term Name DefaultUni DefaultFun ()
go Int
5
  where
    go :: Int -> Term Name DefaultUni DefaultFun ()
    go :: Int -> Term Name DefaultUni DefaultFun ()
go Int
0 = Integer -> Term Name DefaultUni DefaultFun ()
con Integer
0
    go Int
n = Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall {name} {uni :: * -> *}.
Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus (Integer -> Term Name DefaultUni DefaultFun ()
con Integer
1) (Int -> Term Name DefaultUni DefaultFun ()
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))

    plus :: Term name uni DefaultFun ()
-> Term name uni DefaultFun () -> Term name uni DefaultFun ()
plus Term name uni DefaultFun ()
a Term name uni DefaultFun ()
b = Term name uni DefaultFun ()
-> [((), Term name uni DefaultFun ())]
-> Term name uni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp (() -> DefaultFun -> Term name uni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin () DefaultFun
PLC.AddInteger) [((), Term name uni DefaultFun ()
a), ((), Term name uni DefaultFun ()
b)]
    con :: Integer -> Term Name DefaultUni DefaultFun ()
con = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer ()

testSimplifyInputs :: [(String, Term Name PLC.DefaultUni PLC.DefaultFun ())]
testSimplifyInputs :: [(String, Term Name DefaultUni DefaultFun ())]
testSimplifyInputs =
  [ (String
"basic", Term Name DefaultUni DefaultFun ()
basic)
  , (String
"nested", Term Name DefaultUni DefaultFun ()
nested)
  , (String
"extraDelays", Term Name DefaultUni DefaultFun ()
extraDelays)
  , (String
"floatDelay1", Term Name DefaultUni DefaultFun ()
floatDelay1)
  , (String
"floatDelay2", Term Name DefaultUni DefaultFun ()
floatDelay2)
  , (String
"floatDelay3", Term Name DefaultUni DefaultFun ()
floatDelay3)
  , (String
"interveningLambda", Term Name DefaultUni DefaultFun ()
interveningLambda)
  , (String
"basicInline", Term Name DefaultUni DefaultFun ()
basicInline)
  , (String
"callsiteInline", Term Name DefaultUni DefaultFun ()
callsiteInline)
  , (String
"inlinePure1", Term Name DefaultUni DefaultFun ()
inlinePure1)
  , (String
"inlinePure2", Term Name DefaultUni DefaultFun ()
inlinePure2)
  , (String
"inlinePure3", Term Name DefaultUni DefaultFun ()
inlinePure3)
  , (String
"inlinePure4", Term Name DefaultUni DefaultFun ()
inlinePure4)
  , (String
"inlineImpure1", Term Name DefaultUni DefaultFun ()
inlineImpure1)
  , (String
"inlineImpure2", Term Name DefaultUni DefaultFun ()
inlineImpure2)
  , (String
"inlineImpure3", Term Name DefaultUni DefaultFun ()
inlineImpure3)
  , (String
"inlineImpure4", Term Name DefaultUni DefaultFun ()
inlineImpure4)
  , (String
"multiApp", Term Name DefaultUni DefaultFun ()
multiApp)
  , (String
"forceDelayNoApps", Term Name DefaultUni DefaultFun ()
forceDelayNoApps)
  , (String
"forceDelayNoAppsLayered", Term Name DefaultUni DefaultFun ()
forceDelayNoAppsLayered)
  , (String
"forceDelaySimple", Term Name DefaultUni DefaultFun ()
forceDelaySimple)
  , (String
"forceDelayMultiApply", Term Name DefaultUni DefaultFun ()
forceDelayMultiApply)
  , (String
"forceDelayMultiForce", Term Name DefaultUni DefaultFun ()
forceDelayMultiForce)
  , (String
"forceDelayComplex", Term Name DefaultUni DefaultFun ()
forceDelayComplex)
  , (String
"forceCaseDelayNoApps1", Term Name DefaultUni DefaultFun ()
forceCaseDelayNoApps1)
  , (String
"forceCaseDelayWithApps1", Term Name DefaultUni DefaultFun ()
forceCaseDelayWithApps1)
  , (String
"forceCaseDelayNoApps2", Term Name DefaultUni DefaultFun ()
forceCaseDelayNoApps2)
  , (String
"forceCaseDelayWithApps2", Term Name DefaultUni DefaultFun ()
forceCaseDelayWithApps2)
  , (String
"forceCaseDelayNoApps2Fail", Term Name DefaultUni DefaultFun ()
forceCaseDelayNoApps2Fail)
  , (String
"forceCaseDelayWithApps2Fail", Term Name DefaultUni DefaultFun ()
forceCaseDelayWithApps2Fail)
  ]

testCseInputs :: [(String, Term Name PLC.DefaultUni PLC.DefaultFun ())]
testCseInputs :: [(String, Term Name DefaultUni DefaultFun ())]
testCseInputs =
  [ (String
"cse1", Term Name DefaultUni DefaultFun ()
cse1)
  , (String
"cse2", Term Name DefaultUni DefaultFun ()
cse2)
  , (String
"cse3", Term Name DefaultUni DefaultFun ()
cse3)
  , (String
"cseExpensive", Term Name DefaultUni DefaultFun ()
cseExpensive)
  ]

testCseInputsWorkFree :: [(String, Term Name PLC.DefaultUni PLC.DefaultFun ())]
testCseInputsWorkFree :: [(String, Term Name DefaultUni DefaultFun ())]
testCseInputsWorkFree =
  [ (String
"cse1WorkFree", Term Name DefaultUni DefaultFun ()
cse1)
  , (String
"csePlusTree", Term Name DefaultUni DefaultFun ()
csePlusTree)
  , (String
"cseRepeatPlus", Term Name DefaultUni DefaultFun ()
cseRepeatPlus)
  ]

test_simplify :: TestTree
test_simplify :: TestTree
test_simplify =
  String -> [TestTree] -> TestTree
testGroup
    String
"simplify"
    ([TestTree] -> TestTree) -> [TestTree] -> TestTree
forall a b. (a -> b) -> a -> b
$ ((String, Term Name DefaultUni DefaultFun ()) -> TestTree)
-> [(String, Term Name DefaultUni DefaultFun ())] -> [TestTree]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((String -> Term Name DefaultUni DefaultFun () -> TestTree)
-> (String, Term Name DefaultUni DefaultFun ()) -> TestTree
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> Term Name DefaultUni DefaultFun () -> TestTree
goldenVsSimplified) [(String, Term Name DefaultUni DefaultFun ())]
testSimplifyInputs
      [TestTree] -> [TestTree] -> [TestTree]
forall a. Semigroup a => a -> a -> a
<> ((String, Term Name DefaultUni DefaultFun ()) -> TestTree)
-> [(String, Term Name DefaultUni DefaultFun ())] -> [TestTree]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((String -> Term Name DefaultUni DefaultFun () -> TestTree)
-> (String, Term Name DefaultUni DefaultFun ()) -> TestTree
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (CseWhichSubterms
-> String -> Term Name DefaultUni DefaultFun () -> TestTree
goldenVsCse CseWhichSubterms
ExcludeWorkFree)) [(String, Term Name DefaultUni DefaultFun ())]
testCseInputs
      [TestTree] -> [TestTree] -> [TestTree]
forall a. Semigroup a => a -> a -> a
<> ((String, Term Name DefaultUni DefaultFun ()) -> TestTree)
-> [(String, Term Name DefaultUni DefaultFun ())] -> [TestTree]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((String -> Term Name DefaultUni DefaultFun () -> TestTree)
-> (String, Term Name DefaultUni DefaultFun ()) -> TestTree
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (CseWhichSubterms
-> String -> Term Name DefaultUni DefaultFun () -> TestTree
goldenVsCse CseWhichSubterms
AllSubterms)) [(String, Term Name DefaultUni DefaultFun ())]
testCseInputsWorkFree