{-# LANGUAGE TypeApplications #-}
-- | The point of these tests is that binders with wrong indices will be undebruijnified
-- successfully, whereas variables with wrong indices (e.g. out of scope) will fail.
module DeBruijn.UnDeBruijnify (test_undebruijnify) where

import PlutusCore qualified as PLC
import PlutusCore.Default
import PlutusCore.Error
import PlutusCore.MkPlc
import PlutusCore.Pretty
import PlutusCore.Quote
import PlutusCore.StdLib.Data.Bool
import UntypedPlutusCore as UPLC
import UntypedPlutusCore.Test.DeBruijn.Bad
import UntypedPlutusCore.Test.DeBruijn.Good

import Control.Monad.Except
import Control.Monad.State
import Test.Tasty.Extras

type T = Term DeBruijn DefaultUni DefaultFun ()

-- | (lam0 [2 1 4 (lam1 [1 4 3 5])])
graceElaborate :: T
graceElaborate :: T
graceElaborate = T -> T
forall t (uni :: * -> *) fun.
(t ~ Term DeBruijn uni fun ()) =>
t -> t
lamAbs0 (T -> T) -> T -> T
forall a b. (a -> b) -> a -> b
$
    Index -> T
forall {uni :: * -> *} {fun}. Index -> Term DeBruijn uni fun ()
v Index
2 T -> [T] -> T
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ [ Index -> T
forall {uni :: * -> *} {fun}. Index -> Term DeBruijn uni fun ()
v Index
1
           , Index -> T
forall {uni :: * -> *} {fun}. Index -> Term DeBruijn uni fun ()
v Index
4
           , T -> T
forall t (uni :: * -> *) fun.
(t ~ Term DeBruijn uni fun ()) =>
t -> t
lamAbs1 (T -> T) -> T -> T
forall a b. (a -> b) -> a -> b
$ Index -> T
forall {uni :: * -> *} {fun}. Index -> Term DeBruijn uni fun ()
v Index
1 T -> [T] -> T
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ [ Index -> T
forall {uni :: * -> *} {fun}. Index -> Term DeBruijn uni fun ()
v Index
4
                              , Index -> T
forall {uni :: * -> *} {fun}. Index -> Term DeBruijn uni fun ()
v Index
3
                              , Index -> T
forall {uni :: * -> *} {fun}. Index -> Term DeBruijn uni fun ()
v Index
5
                              ]
           ]
 where
   v :: Index -> Term DeBruijn uni fun ()
v = () -> DeBruijn -> Term DeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () (DeBruijn -> Term DeBruijn uni fun ())
-> (Index -> DeBruijn) -> Index -> Term DeBruijn uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index -> DeBruijn
DeBruijn

testsDefault :: [(String, T)]
testsDefault :: [(String, T)]
testsDefault =
    [(String
"okId0", T
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
idFun0)
    ,(String
"okId99", T
fun1var1)
    ,(String
"okConst", T
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
const0 T -> [T] -> T
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ [T
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni Bool) =>
term ()
true, T
fun1var1])
    ,(String
"okDeep0", Natural -> T
deepFun0 Natural
10)
    ,(String
"okDeep99", Natural -> T
deepFun1 Natural
10)
    ,(String
"okMix1", Natural -> T
deepMix0_1 Natural
10)
    ,(String
"okMix2", Natural -> T
deepMix1_0 Natural
10)
    ,(String
"failTop", () -> T -> T
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () T
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
var0)
    ,(String
"failDeep", Natural -> T
deepOut0 Natural
10)
    ,(String
"failBody0", T
fun0var0)
    ,(String
"failBody99", T
fun1var0)
    ,(String
"failConst", T
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
const0 T -> [T] -> T
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ [T
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni Bool) =>
term ()
true, T
fun0var0])
    ,(String
"failITE", T
ite10)
    ,(String
"failMix", Natural -> T
deepOutMix1_0 Natural
10)
    ,(String
"failTop0", T
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
var0)
    ,(String
"failTop1", () -> DeBruijn -> T
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () (DeBruijn -> T) -> DeBruijn -> T
forall a b. (a -> b) -> a -> b
$ Index -> DeBruijn
DeBruijn Index
1)
    ,(String
"failApply01", T
manyFree01)
    ]

-- | This is testing the (non-default) behavior of undebruijnification where
-- free debruijn indices are gracefully (without throwing an error) converted to fresh uniques.
-- See `freeIndexAsConsistentLevel`
testsGrace :: [(String, T)]
testsGrace :: [(String, T)]
testsGrace =
    [(String
"graceTop", () -> T -> T
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () T
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
var0)
    ,(String
"graceDeep", Natural -> T
deepOut0 Natural
5)
    ,(String
"graceConst", T
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
const0 T -> [T] -> T
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ [T
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni Bool) =>
term ()
true, T
fun0var0])
    ,(String
"graceElaborate", T
graceElaborate)
    ]

test_undebruijnify :: TestNested
test_undebruijnify :: TestNested
test_undebruijnify = String -> [TestNested] -> TestNested
testNested String
"Golden"
                    [String -> [TestNested] -> TestNested
testNested String
"Default" ([TestNested] -> TestNested) -> [TestNested] -> TestNested
forall a b. (a -> b) -> a -> b
$
                        ((String, T) -> TestNested) -> [(String, T)] -> [TestNested]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Program NamedDeBruijn DefaultUni DefaultFun ()
 -> QuoteT
      (ExceptT (Error DefaultUni DefaultFun ()) Identity)
      (Program Name DefaultUni DefaultFun ()))
-> (String, T) -> TestNested
forall {uni :: * -> *} {fun}.
(Program NamedDeBruijn uni fun ()
 -> QuoteT
      (ExceptT (Error DefaultUni DefaultFun ()) Identity)
      (Program Name DefaultUni DefaultFun ()))
-> (String, Term DeBruijn uni fun ()) -> TestNested
nestedGoldenVsPretty Program NamedDeBruijn DefaultUni DefaultFun ()
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Program Name DefaultUni DefaultFun ())
forall {uni2 :: * -> *} {fun2} {ann}.
Program NamedDeBruijn uni2 fun2 ann
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Program Name uni2 fun2 ann)
actDefault) [(String, T)]
testsDefault
                    ,String -> [TestNested] -> TestNested
testNested String
"Graceful" ([TestNested] -> TestNested) -> [TestNested] -> TestNested
forall a b. (a -> b) -> a -> b
$
                        ((String, T) -> TestNested) -> [(String, T)] -> [TestNested]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Program NamedDeBruijn DefaultUni DefaultFun ()
 -> QuoteT
      (ExceptT (Error DefaultUni DefaultFun ()) Identity)
      (Program Name DefaultUni DefaultFun ()))
-> (String, T) -> TestNested
forall {uni :: * -> *} {fun}.
(Program NamedDeBruijn uni fun ()
 -> QuoteT
      (ExceptT (Error DefaultUni DefaultFun ()) Identity)
      (Program Name DefaultUni DefaultFun ()))
-> (String, Term DeBruijn uni fun ()) -> TestNested
nestedGoldenVsPretty Program NamedDeBruijn DefaultUni DefaultFun ()
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Program Name DefaultUni DefaultFun ())
forall {uni2 :: * -> *} {fun2} {ann}.
Program NamedDeBruijn uni2 fun2 ann
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Program Name uni2 fun2 ann)
actGrace) [(String, T)]
testsGrace
                    ]
  where
    nestedGoldenVsPretty :: (Program NamedDeBruijn uni fun ()
 -> QuoteT
      (ExceptT (Error DefaultUni DefaultFun ()) Identity)
      (Program Name DefaultUni DefaultFun ()))
-> (String, Term DeBruijn uni fun ()) -> TestNested
nestedGoldenVsPretty Program NamedDeBruijn uni fun ()
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Program Name DefaultUni DefaultFun ())
act (String
n,Term DeBruijn uni fun ()
t) =
        String -> String -> Doc Any -> TestNested
forall ann. String -> String -> Doc ann -> TestNested
nestedGoldenVsDoc String
n String
".uplc" (Doc Any -> TestNested) -> Doc Any -> TestNested
forall a b. (a -> b) -> a -> b
$ QuoteT
  (ExceptT (Error DefaultUni DefaultFun ()) Identity)
  (Program Name DefaultUni DefaultFun ())
-> Doc Any
forall {ann}.
QuoteT
  (ExceptT (Error DefaultUni DefaultFun ()) Identity)
  (Program Name DefaultUni DefaultFun ())
-> Doc ann
toPretty (QuoteT
   (ExceptT (Error DefaultUni DefaultFun ()) Identity)
   (Program Name DefaultUni DefaultFun ())
 -> Doc Any)
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Program Name DefaultUni DefaultFun ())
-> Doc Any
forall a b. (a -> b) -> a -> b
$ Program NamedDeBruijn uni fun ()
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Program Name DefaultUni DefaultFun ())
act (Program NamedDeBruijn uni fun ()
 -> QuoteT
      (ExceptT (Error DefaultUni DefaultFun ()) Identity)
      (Program Name DefaultUni DefaultFun ()))
-> Program NamedDeBruijn uni fun ()
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Program Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Term DeBruijn uni fun () -> Program NamedDeBruijn uni fun ()
forall {uni :: * -> *} {fun}.
Term DeBruijn uni fun () -> Program NamedDeBruijn uni fun ()
mkProg Term DeBruijn uni fun ()
t

    actDefault :: Program NamedDeBruijn uni2 fun2 ann
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Program Name uni2 fun2 ann)
actDefault = (Term NamedDeBruijn uni2 fun2 ann
 -> QuoteT
      (ExceptT (Error DefaultUni DefaultFun ()) Identity)
      (Term Name uni2 fun2 ann))
-> Program NamedDeBruijn uni2 fun2 ann
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Program Name uni2 fun2 ann)
forall name1 (uni1 :: * -> *) fun1 ann name2 (uni2 :: * -> *) fun2
       (f :: * -> *).
Functor f =>
(Term name1 uni1 fun1 ann -> f (Term name2 uni2 fun2 ann))
-> Program name1 uni1 fun1 ann -> f (Program name2 uni2 fun2 ann)
progTerm Term NamedDeBruijn uni2 fun2 ann
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Term Name uni2 fun2 ann)
forall (m :: * -> *) e (uni :: * -> *) fun ann.
(MonadQuote m, AsFreeVariableError e, MonadError e m) =>
Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
unDeBruijnTerm

    actGrace :: Program NamedDeBruijn uni2 fun2 ann
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Program Name uni2 fun2 ann)
actGrace = (StateT
   (Map Level Unique)
   (QuoteT (ExceptT (Error DefaultUni DefaultFun ()) Identity))
   (Program Name uni2 fun2 ann)
 -> Map Level Unique
 -> QuoteT
      (ExceptT (Error DefaultUni DefaultFun ()) Identity)
      (Program Name uni2 fun2 ann))
-> Map Level Unique
-> StateT
     (Map Level Unique)
     (QuoteT (ExceptT (Error DefaultUni DefaultFun ()) Identity))
     (Program Name uni2 fun2 ann)
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Program Name uni2 fun2 ann)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT
  (Map Level Unique)
  (QuoteT (ExceptT (Error DefaultUni DefaultFun ()) Identity))
  (Program Name uni2 fun2 ann)
-> Map Level Unique
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Program Name uni2 fun2 ann)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Map Level Unique
forall a. Monoid a => a
mempty
               (StateT
   (Map Level Unique)
   (QuoteT (ExceptT (Error DefaultUni DefaultFun ()) Identity))
   (Program Name uni2 fun2 ann)
 -> QuoteT
      (ExceptT (Error DefaultUni DefaultFun ()) Identity)
      (Program Name uni2 fun2 ann))
-> (Program NamedDeBruijn uni2 fun2 ann
    -> StateT
         (Map Level Unique)
         (QuoteT (ExceptT (Error DefaultUni DefaultFun ()) Identity))
         (Program Name uni2 fun2 ann))
-> Program NamedDeBruijn uni2 fun2 ann
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Program Name uni2 fun2 ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term NamedDeBruijn uni2 fun2 ann
 -> StateT
      (Map Level Unique)
      (QuoteT (ExceptT (Error DefaultUni DefaultFun ()) Identity))
      (Term Name uni2 fun2 ann))
-> Program NamedDeBruijn uni2 fun2 ann
-> StateT
     (Map Level Unique)
     (QuoteT (ExceptT (Error DefaultUni DefaultFun ()) Identity))
     (Program Name uni2 fun2 ann)
forall name1 (uni1 :: * -> *) fun1 ann name2 (uni2 :: * -> *) fun2
       (f :: * -> *).
Functor f =>
(Term name1 uni1 fun1 ann -> f (Term name2 uni2 fun2 ann))
-> Program name1 uni1 fun1 ann -> f (Program name2 uni2 fun2 ann)
progTerm ((Index
 -> ReaderT
      LevelInfo
      (StateT
         (Map Level Unique)
         (QuoteT (ExceptT (Error DefaultUni DefaultFun ()) Identity)))
      Unique)
-> Term NamedDeBruijn uni2 fun2 ann
-> StateT
     (Map Level Unique)
     (QuoteT (ExceptT (Error DefaultUni DefaultFun ()) Identity))
     (Term Name uni2 fun2 ann)
forall (m :: * -> *) (uni :: * -> *) fun ann.
MonadQuote m =>
(Index -> ReaderT LevelInfo m Unique)
-> Term NamedDeBruijn uni fun ann -> m (Term Name uni fun ann)
unDeBruijnTermWith Index
-> ReaderT
     LevelInfo
     (StateT
        (Map Level Unique)
        (QuoteT (ExceptT (Error DefaultUni DefaultFun ()) Identity)))
     Unique
forall (m :: * -> *).
(MonadReader LevelInfo m, MonadState (Map Level Unique) m,
 MonadQuote m) =>
Index -> m Unique
freeIndexAsConsistentLevel)

    mkProg :: Term DeBruijn uni fun () -> Program NamedDeBruijn uni fun ()
mkProg = ()
-> Version
-> Term NamedDeBruijn uni fun ()
-> Program NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Version -> Term name uni fun ann -> Program name uni fun ann
Program () Version
PLC.latestVersion (Term NamedDeBruijn uni fun () -> Program NamedDeBruijn uni fun ())
-> (Term DeBruijn uni fun () -> Term NamedDeBruijn uni fun ())
-> Term DeBruijn uni fun ()
-> Program NamedDeBruijn uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DeBruijn -> NamedDeBruijn)
-> Term DeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall name name' (uni :: * -> *) fun ann.
(name -> name') -> Term name uni fun ann -> Term name' uni fun ann
termMapNames DeBruijn -> NamedDeBruijn
fakeNameDeBruijn

    toPretty :: QuoteT
  (ExceptT (Error DefaultUni DefaultFun ()) Identity)
  (Program Name DefaultUni DefaultFun ())
-> Doc ann
toPretty = Either
  (Error DefaultUni DefaultFun ())
  (Program Name DefaultUni DefaultFun ())
-> Doc ann
forall a ann. PrettyPlc a => a -> Doc ann
prettyPlcClassicSimple (Either
   (Error DefaultUni DefaultFun ())
   (Program Name DefaultUni DefaultFun ())
 -> Doc ann)
-> (QuoteT
      (ExceptT (Error DefaultUni DefaultFun ()) Identity)
      (Program Name DefaultUni DefaultFun ())
    -> Either
         (Error DefaultUni DefaultFun ())
         (Program Name DefaultUni DefaultFun ()))
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Program Name DefaultUni DefaultFun ())
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e a. Except e a -> Either e a
runExcept @(Error DefaultUni DefaultFun ()) (Except
   (Error DefaultUni DefaultFun ())
   (Program Name DefaultUni DefaultFun ())
 -> Either
      (Error DefaultUni DefaultFun ())
      (Program Name DefaultUni DefaultFun ()))
-> (QuoteT
      (ExceptT (Error DefaultUni DefaultFun ()) Identity)
      (Program Name DefaultUni DefaultFun ())
    -> Except
         (Error DefaultUni DefaultFun ())
         (Program Name DefaultUni DefaultFun ()))
-> QuoteT
     (ExceptT (Error DefaultUni DefaultFun ()) Identity)
     (Program Name DefaultUni DefaultFun ())
-> Either
     (Error DefaultUni DefaultFun ())
     (Program Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QuoteT
  (ExceptT (Error DefaultUni DefaultFun ()) Identity)
  (Program Name DefaultUni DefaultFun ())
-> Except
     (Error DefaultUni DefaultFun ())
     (Program Name DefaultUni DefaultFun ())
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT