{-# LANGUAGE TypeApplications #-}

module Scoping.Spec where

import Generators.Lib (genProgram, genTerm)

import UntypedPlutusCore (_soInlineHints, _soPreserveLogging, defaultSimplifyOpts)
import UntypedPlutusCore.Mark
import UntypedPlutusCore.Rename.Internal
import UntypedPlutusCore.Transform.CaseOfCase (caseOfCase)
import UntypedPlutusCore.Transform.CaseReduce (caseReduce)
import UntypedPlutusCore.Transform.Cse (cse)
import UntypedPlutusCore.Transform.FloatDelay (floatDelay)
import UntypedPlutusCore.Transform.ForceDelay (forceDelay)
import UntypedPlutusCore.Transform.Inline (inline)
import UntypedPlutusCore.Transform.Simplifier (evalSimplifierT)

import PlutusCore.Default.Builtins (DefaultFun)
import PlutusCore.Rename
import PlutusCore.Test qualified as T

import Test.Tasty

-- See Note [Scoping tests API].
test_names :: TestTree
test_names :: TestTree
test_names = TestName -> [TestTree] -> TestTree
testGroup TestName
"names"
    [ TestName
-> AstGen (Program Name DefaultUni DefaultFun ())
-> BindingRemoval
-> Prerename
-> (Program Name DefaultUni DefaultFun NameAnn
    -> Quote (Program Name DefaultUni DefaultFun NameAnn))
-> TestTree
forall (t :: * -> *) ann.
(PrettyPlc (t NameAnn), Rename (t NameAnn), Scoping t) =>
TestName
-> AstGen (t ann)
-> BindingRemoval
-> Prerename
-> (t NameAnn -> Quote (t NameAnn))
-> TestTree
T.test_scopingGood TestName
"renaming" (forall fun.
(Bounded fun, Enum fun) =>
AstGen (Program Name DefaultUni fun ())
genProgram @DefaultFun) BindingRemoval
T.BindingRemovalNotOk Prerename
T.PrerenameNo
        Program Name DefaultUni DefaultFun NameAnn
-> Quote (Program Name DefaultUni DefaultFun NameAnn)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
forall (m :: * -> *).
MonadQuote m =>
Program Name DefaultUni DefaultFun NameAnn
-> m (Program Name DefaultUni DefaultFun NameAnn)
rename
    , AstGen (Program Name DefaultUni DefaultFun ())
-> (Program Name DefaultUni DefaultFun NameAnn -> Quote ())
-> (forall (m :: * -> *).
    (MonadQuote m, MonadReader (Renaming TermUnique) m) =>
    Program Name DefaultUni DefaultFun NameAnn
    -> m (Program Name DefaultUni DefaultFun NameAnn))
-> TestTree
forall (t :: * -> *) ren ann.
(PrettyPlc (t NameAnn), Rename (t NameAnn), Scoping t,
 Monoid ren) =>
AstGen (t ann)
-> (t NameAnn -> Quote ())
-> (forall (m :: * -> *).
    (MonadQuote m, MonadReader ren m) =>
    t NameAnn -> m (t NameAnn))
-> TestTree
T.test_scopingSpoilRenamer (forall fun.
(Bounded fun, Enum fun) =>
AstGen (Program Name DefaultUni fun ())
genProgram @DefaultFun) Program Name DefaultUni DefaultFun NameAnn -> Quote ()
forall name (m :: * -> *) (uni :: * -> *) fun ann.
(HasUnique name TermUnique, MonadQuote m) =>
Program name uni fun ann -> m ()
markNonFreshProgram
        Program Name DefaultUni DefaultFun NameAnn
-> m (Program Name DefaultUni DefaultFun NameAnn)
forall (m :: * -> *).
(MonadQuote m, MonadReader (Renaming TermUnique) m) =>
Program Name DefaultUni DefaultFun NameAnn
-> m (Program Name DefaultUni DefaultFun NameAnn)
forall (m :: * -> *) name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Program name uni fun ann)) =>
Program name uni fun ann -> m (Program name uni fun ann)
renameProgramM
    , TestName
-> AstGen (Term Name DefaultUni DefaultFun ())
-> BindingRemoval
-> Prerename
-> (Term Name DefaultUni DefaultFun NameAnn
    -> Quote (Term Name DefaultUni DefaultFun NameAnn))
-> TestTree
forall (t :: * -> *) ann.
(PrettyPlc (t NameAnn), Rename (t NameAnn), Scoping t) =>
TestName
-> AstGen (t ann)
-> BindingRemoval
-> Prerename
-> (t NameAnn -> Quote (t NameAnn))
-> TestTree
T.test_scopingGood TestName
"case-of-case" (forall fun.
(Bounded fun, Enum fun) =>
AstGen (Term Name DefaultUni fun ())
genTerm @DefaultFun) BindingRemoval
T.BindingRemovalOk Prerename
T.PrerenameYes ((Term Name DefaultUni DefaultFun NameAnn
  -> Quote (Term Name DefaultUni DefaultFun NameAnn))
 -> TestTree)
-> (Term Name DefaultUni DefaultFun NameAnn
    -> Quote (Term Name DefaultUni DefaultFun NameAnn))
-> TestTree
forall a b. (a -> b) -> a -> b
$
        SimplifierT
  Name
  DefaultUni
  DefaultFun
  NameAnn
  (QuoteT Identity)
  (Term Name DefaultUni DefaultFun NameAnn)
-> Quote (Term Name DefaultUni DefaultFun NameAnn)
forall (m :: * -> *) name (uni :: * -> *) fun ann a.
Monad m =>
SimplifierT name uni fun ann m a -> m a
evalSimplifierT (SimplifierT
   Name
   DefaultUni
   DefaultFun
   NameAnn
   (QuoteT Identity)
   (Term Name DefaultUni DefaultFun NameAnn)
 -> Quote (Term Name DefaultUni DefaultFun NameAnn))
-> (Term Name DefaultUni DefaultFun NameAnn
    -> SimplifierT
         Name
         DefaultUni
         DefaultFun
         NameAnn
         (QuoteT Identity)
         (Term Name DefaultUni DefaultFun NameAnn))
-> Term Name DefaultUni DefaultFun NameAnn
-> Quote (Term Name DefaultUni DefaultFun NameAnn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term Name DefaultUni DefaultFun NameAnn
-> SimplifierT
     Name
     DefaultUni
     DefaultFun
     NameAnn
     (QuoteT Identity)
     (Term Name DefaultUni DefaultFun NameAnn)
forall fun (m :: * -> *) name (uni :: * -> *) a.
(fun ~ DefaultFun, Monad m) =>
Term name uni fun a
-> SimplifierT name uni fun a m (Term name uni fun a)
caseOfCase
    , -- COKC removes entire branches, some of which are going to contain binders, but we still use
      -- 'BindingRemovalNotOk', because the 'EstablishScoping' instance does not attempt to
      -- reference bindings from one branch in another one. We could do that, but then we'd be
      -- removing not just TODO.
      TestName
-> AstGen (Term Name DefaultUni DefaultFun ())
-> BindingRemoval
-> Prerename
-> (Term Name DefaultUni DefaultFun NameAnn
    -> Quote (Term Name DefaultUni DefaultFun NameAnn))
-> TestTree
forall (t :: * -> *) ann.
(PrettyPlc (t NameAnn), Rename (t NameAnn), Scoping t) =>
TestName
-> AstGen (t ann)
-> BindingRemoval
-> Prerename
-> (t NameAnn -> Quote (t NameAnn))
-> TestTree
T.test_scopingGood TestName
"case-of-known-constructor"
        (forall fun.
(Bounded fun, Enum fun) =>
AstGen (Term Name DefaultUni fun ())
genTerm @DefaultFun)
        BindingRemoval
T.BindingRemovalOk  -- COKC removes branches, which may (and likely do) contain bindings.
        Prerename
T.PrerenameYes
        (SimplifierT
  Name
  DefaultUni
  DefaultFun
  NameAnn
  (QuoteT Identity)
  (Term Name DefaultUni DefaultFun NameAnn)
-> Quote (Term Name DefaultUni DefaultFun NameAnn)
forall (m :: * -> *) name (uni :: * -> *) fun ann a.
Monad m =>
SimplifierT name uni fun ann m a -> m a
evalSimplifierT (SimplifierT
   Name
   DefaultUni
   DefaultFun
   NameAnn
   (QuoteT Identity)
   (Term Name DefaultUni DefaultFun NameAnn)
 -> Quote (Term Name DefaultUni DefaultFun NameAnn))
-> (Term Name DefaultUni DefaultFun NameAnn
    -> SimplifierT
         Name
         DefaultUni
         DefaultFun
         NameAnn
         (QuoteT Identity)
         (Term Name DefaultUni DefaultFun NameAnn))
-> Term Name DefaultUni DefaultFun NameAnn
-> Quote (Term Name DefaultUni DefaultFun NameAnn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term Name DefaultUni DefaultFun NameAnn
-> SimplifierT
     Name
     DefaultUni
     DefaultFun
     NameAnn
     (QuoteT Identity)
     (Term Name DefaultUni DefaultFun NameAnn)
forall (m :: * -> *) name (uni :: * -> *) fun a.
Monad m =>
Term name uni fun a
-> SimplifierT name uni fun a m (Term name uni fun a)
caseReduce)
    , -- CSE creates entirely new names, which isn't supported by the scoping check machinery.
      TestName
-> AstGen (Term Name DefaultUni DefaultFun ())
-> BindingRemoval
-> Prerename
-> (Term Name DefaultUni DefaultFun NameAnn
    -> Quote (Term Name DefaultUni DefaultFun NameAnn))
-> TestTree
forall (t :: * -> *) ann.
(PrettyPlc (t NameAnn), Rename (t NameAnn), Scoping t) =>
TestName
-> AstGen (t ann)
-> BindingRemoval
-> Prerename
-> (t NameAnn -> Quote (t NameAnn))
-> TestTree
T.test_scopingBad TestName
"cse"
        (forall fun.
(Bounded fun, Enum fun) =>
AstGen (Term Name DefaultUni fun ())
genTerm @DefaultFun)
        BindingRemoval
T.BindingRemovalOk
        Prerename
T.PrerenameYes
        (SimplifierT
  Name
  DefaultUni
  DefaultFun
  NameAnn
  (QuoteT Identity)
  (Term Name DefaultUni DefaultFun NameAnn)
-> Quote (Term Name DefaultUni DefaultFun NameAnn)
forall (m :: * -> *) name (uni :: * -> *) fun ann a.
Monad m =>
SimplifierT name uni fun ann m a -> m a
evalSimplifierT (SimplifierT
   Name
   DefaultUni
   DefaultFun
   NameAnn
   (QuoteT Identity)
   (Term Name DefaultUni DefaultFun NameAnn)
 -> Quote (Term Name DefaultUni DefaultFun NameAnn))
-> (Term Name DefaultUni DefaultFun NameAnn
    -> SimplifierT
         Name
         DefaultUni
         DefaultFun
         NameAnn
         (QuoteT Identity)
         (Term Name DefaultUni DefaultFun NameAnn))
-> Term Name DefaultUni DefaultFun NameAnn
-> Quote (Term Name DefaultUni DefaultFun NameAnn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinSemanticsVariant DefaultFun
-> Term Name DefaultUni DefaultFun NameAnn
-> SimplifierT
     Name
     DefaultUni
     DefaultFun
     NameAnn
     (QuoteT Identity)
     (Term Name DefaultUni DefaultFun NameAnn)
forall (m :: * -> *) (uni :: * -> *) fun ann.
(MonadQuote m, Hashable (Term Name uni fun ()),
 Rename (Term Name uni fun ann), ToBuiltinMeaning uni fun) =>
BuiltinSemanticsVariant fun
-> Term Name uni fun ann
-> SimplifierT Name uni fun ann m (Term Name uni fun ann)
cse BuiltinSemanticsVariant DefaultFun
forall a. Bounded a => a
maxBound)
    , TestName
-> AstGen (Term Name DefaultUni DefaultFun ())
-> BindingRemoval
-> Prerename
-> (Term Name DefaultUni DefaultFun NameAnn
    -> Quote (Term Name DefaultUni DefaultFun NameAnn))
-> TestTree
forall (t :: * -> *) ann.
(PrettyPlc (t NameAnn), Rename (t NameAnn), Scoping t) =>
TestName
-> AstGen (t ann)
-> BindingRemoval
-> Prerename
-> (t NameAnn -> Quote (t NameAnn))
-> TestTree
T.test_scopingGood TestName
"float-delay"
        (forall fun.
(Bounded fun, Enum fun) =>
AstGen (Term Name DefaultUni fun ())
genTerm @DefaultFun)
        BindingRemoval
T.BindingRemovalNotOk
        Prerename
T.PrerenameNo
        (SimplifierT
  Name
  DefaultUni
  DefaultFun
  NameAnn
  (QuoteT Identity)
  (Term Name DefaultUni DefaultFun NameAnn)
-> Quote (Term Name DefaultUni DefaultFun NameAnn)
forall (m :: * -> *) name (uni :: * -> *) fun ann a.
Monad m =>
SimplifierT name uni fun ann m a -> m a
evalSimplifierT (SimplifierT
   Name
   DefaultUni
   DefaultFun
   NameAnn
   (QuoteT Identity)
   (Term Name DefaultUni DefaultFun NameAnn)
 -> Quote (Term Name DefaultUni DefaultFun NameAnn))
-> (Term Name DefaultUni DefaultFun NameAnn
    -> SimplifierT
         Name
         DefaultUni
         DefaultFun
         NameAnn
         (QuoteT Identity)
         (Term Name DefaultUni DefaultFun NameAnn))
-> Term Name DefaultUni DefaultFun NameAnn
-> Quote (Term Name DefaultUni DefaultFun NameAnn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term Name DefaultUni DefaultFun NameAnn
-> SimplifierT
     Name
     DefaultUni
     DefaultFun
     NameAnn
     (QuoteT Identity)
     (Term Name DefaultUni DefaultFun NameAnn)
forall (m :: * -> *) name (uni :: * -> *) fun a.
(MonadQuote m, Rename (Term name uni fun a),
 HasUnique name TermUnique) =>
Term name uni fun a
-> SimplifierT name uni fun a m (Term name uni fun a)
floatDelay)
    , TestName
-> AstGen (Term Name DefaultUni DefaultFun ())
-> BindingRemoval
-> Prerename
-> (Term Name DefaultUni DefaultFun NameAnn
    -> Quote (Term Name DefaultUni DefaultFun NameAnn))
-> TestTree
forall (t :: * -> *) ann.
(PrettyPlc (t NameAnn), Rename (t NameAnn), Scoping t) =>
TestName
-> AstGen (t ann)
-> BindingRemoval
-> Prerename
-> (t NameAnn -> Quote (t NameAnn))
-> TestTree
T.test_scopingGood TestName
"force-delay"
        (forall fun.
(Bounded fun, Enum fun) =>
AstGen (Term Name DefaultUni fun ())
genTerm @DefaultFun)
        BindingRemoval
T.BindingRemovalNotOk
        Prerename
T.PrerenameYes
        (SimplifierT
  Name
  DefaultUni
  DefaultFun
  NameAnn
  (QuoteT Identity)
  (Term Name DefaultUni DefaultFun NameAnn)
-> Quote (Term Name DefaultUni DefaultFun NameAnn)
forall (m :: * -> *) name (uni :: * -> *) fun ann a.
Monad m =>
SimplifierT name uni fun ann m a -> m a
evalSimplifierT (SimplifierT
   Name
   DefaultUni
   DefaultFun
   NameAnn
   (QuoteT Identity)
   (Term Name DefaultUni DefaultFun NameAnn)
 -> Quote (Term Name DefaultUni DefaultFun NameAnn))
-> (Term Name DefaultUni DefaultFun NameAnn
    -> SimplifierT
         Name
         DefaultUni
         DefaultFun
         NameAnn
         (QuoteT Identity)
         (Term Name DefaultUni DefaultFun NameAnn))
-> Term Name DefaultUni DefaultFun NameAnn
-> Quote (Term Name DefaultUni DefaultFun NameAnn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinSemanticsVariant DefaultFun
-> Term Name DefaultUni DefaultFun NameAnn
-> SimplifierT
     Name
     DefaultUni
     DefaultFun
     NameAnn
     (QuoteT Identity)
     (Term Name DefaultUni DefaultFun NameAnn)
forall (uni :: * -> *) fun (m :: * -> *) name a.
(uni ~ DefaultUni, fun ~ DefaultFun, Monad m) =>
BuiltinSemanticsVariant fun
-> Term name uni fun a
-> SimplifierT name uni fun a m (Term name uni fun a)
forceDelay BuiltinSemanticsVariant DefaultFun
forall a. Bounded a => a
maxBound)
    , TestName
-> AstGen (Term Name DefaultUni DefaultFun ())
-> BindingRemoval
-> Prerename
-> (Term Name DefaultUni DefaultFun NameAnn
    -> Quote (Term Name DefaultUni DefaultFun NameAnn))
-> TestTree
forall (t :: * -> *) ann.
(PrettyPlc (t NameAnn), Rename (t NameAnn), Scoping t) =>
TestName
-> AstGen (t ann)
-> BindingRemoval
-> Prerename
-> (t NameAnn -> Quote (t NameAnn))
-> TestTree
T.test_scopingGood TestName
"inline"
        (forall fun.
(Bounded fun, Enum fun) =>
AstGen (Term Name DefaultUni fun ())
genTerm @DefaultFun)
        BindingRemoval
T.BindingRemovalOk
        Prerename
T.PrerenameYes
        (SimplifierT
  Name
  DefaultUni
  DefaultFun
  NameAnn
  (QuoteT Identity)
  (Term Name DefaultUni DefaultFun NameAnn)
-> Quote (Term Name DefaultUni DefaultFun NameAnn)
forall (m :: * -> *) name (uni :: * -> *) fun ann a.
Monad m =>
SimplifierT name uni fun ann m a -> m a
evalSimplifierT (SimplifierT
   Name
   DefaultUni
   DefaultFun
   NameAnn
   (QuoteT Identity)
   (Term Name DefaultUni DefaultFun NameAnn)
 -> Quote (Term Name DefaultUni DefaultFun NameAnn))
-> (Term Name DefaultUni DefaultFun NameAnn
    -> SimplifierT
         Name
         DefaultUni
         DefaultFun
         NameAnn
         (QuoteT Identity)
         (Term Name DefaultUni DefaultFun NameAnn))
-> Term Name DefaultUni DefaultFun NameAnn
-> Quote (Term Name DefaultUni DefaultFun NameAnn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          Size
-> Bool
-> Bool
-> InlineHints Name NameAnn
-> BuiltinSemanticsVariant DefaultFun
-> Term Name DefaultUni DefaultFun NameAnn
-> SimplifierT
     Name
     DefaultUni
     DefaultFun
     NameAnn
     (QuoteT Identity)
     (Term Name DefaultUni DefaultFun NameAnn)
forall name (uni :: * -> *) fun (m :: * -> *) a.
ExternalConstraints name uni fun m =>
Size
-> Bool
-> Bool
-> InlineHints name a
-> BuiltinSemanticsVariant fun
-> Term name uni fun a
-> SimplifierT name uni fun a m (Term name uni fun a)
inline Size
0
            Bool
True
            (SimplifyOpts Any Any -> Bool
forall name a. SimplifyOpts name a -> Bool
_soPreserveLogging SimplifyOpts Any Any
forall name a. SimplifyOpts name a
defaultSimplifyOpts)
            (SimplifyOpts Name NameAnn -> InlineHints Name NameAnn
forall name a. SimplifyOpts name a -> InlineHints name a
_soInlineHints SimplifyOpts Name NameAnn
forall name a. SimplifyOpts name a
defaultSimplifyOpts)
            BuiltinSemanticsVariant DefaultFun
forall a. Bounded a => a
maxBound )
    ]