{-# LANGUAGE TypeApplications #-}
-- | The point of these tests is that *both* binders with wrong indices and
-- variables with wrong indices (e.g. out of scope) will fail the scope-check pass.
module DeBruijn.Scope (test_scope) where

import PlutusCore.Default
import PlutusCore.MkPlc
import PlutusCore.StdLib.Data.Unit
import PlutusPrelude
import UntypedPlutusCore
import UntypedPlutusCore.Test.DeBruijn.Bad
import UntypedPlutusCore.Test.DeBruijn.Good

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

type T = Term DeBruijn DefaultUni DefaultFun ()

testsOk :: [(String, T)]
testsOk :: [(TestName, T)]
testsOk =
    [(TestName
"idFun0", T
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
idFun0)
    ,(TestName
"deepFun0", Natural -> T
deepFun0 Natural
10)
    ,(TestName
"deeperFun0", Natural -> T
deeperFun0 Natural
10)
    ]

testsFail :: [(String, T)]
testsFail :: [(TestName, T)]
testsFail =
    [(TestName
"delay0", () -> 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)
    ,(TestName
"top0", T
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
var0)
    ,(TestName
"top1", () -> 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)
    ,(TestName
"fun1var1", T
fun1var1)
    ,(TestName
"fun0var0", T
fun0var0)
    ,(TestName
"fun1var0", T
fun1var0)
    ,(TestName
"const0var0", 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 ()) =>
term ()
unitval, T
fun0var0])
    ,(TestName
"const0var1", 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 ()) =>
term ()
unitval, T
fun1var1])
    ,(TestName
"ite10", T
ite10)
    ,(TestName
"deepOut0", Natural -> T
deepOut0 Natural
10)
    ,(TestName
"deepFun1", Natural -> T
deepFun1 Natural
10)
    ,(TestName
"deepMix0_1", Natural -> T
deepMix0_1 Natural
10)
    ,(TestName
"deepOutMix1_0", Natural -> T
deepOutMix1_0 Natural
10)
    ,(TestName
"manyFree01", T
manyFree01)
    ]

test_scope :: TestNested
test_scope :: TestNested
test_scope = TestName -> [TestNested] -> TestNested
testNested TestName
"Scope" ([TestNested] -> TestNested) -> [TestNested] -> TestNested
forall a b. (a -> b) -> a -> b
$ TestTree -> TestNested
forall a (m :: * -> *). MonadFree ((,) a) m => a -> m ()
embed (TestTree -> TestNested)
-> ((TestName, Assertion) -> TestTree)
-> (TestName, Assertion)
-> TestNested
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TestName -> Assertion -> TestTree)
-> (TestName, Assertion) -> TestTree
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TestName -> Assertion -> TestTree
testCase ((TestName, Assertion) -> TestNested)
-> [(TestName, Assertion)] -> [TestNested]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                 ((T -> Assertion) -> (TestName, T) -> (TestName, Assertion)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second T -> Assertion
forall {uni :: * -> *} {fun} {a}.
Term DeBruijn uni fun a -> Assertion
testPasses ((TestName, T) -> (TestName, Assertion))
-> [(TestName, T)] -> [(TestName, Assertion)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TestName, T)]
testsOk)
               [(TestName, Assertion)]
-> [(TestName, Assertion)] -> [(TestName, Assertion)]
forall a. Semigroup a => a -> a -> a
<> ((T -> Assertion) -> (TestName, T) -> (TestName, Assertion)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second T -> Assertion
forall {uni :: * -> *} {fun} {a}.
Term DeBruijn uni fun a -> Assertion
testThrows ((TestName, T) -> (TestName, Assertion))
-> [(TestName, T)] -> [(TestName, Assertion)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TestName, T)]
testsFail)
    where
      testPasses :: Term DeBruijn uni fun a -> Assertion
testPasses Term DeBruijn uni fun a
t = Either FreeVariableError () -> Bool
forall a b. Either a b -> Bool
isRight (Term DeBruijn uni fun a -> Either FreeVariableError ()
forall {uni :: * -> *} {fun} {a}.
Term DeBruijn uni fun a -> Either FreeVariableError ()
runScope Term DeBruijn uni fun a
t) Bool -> TestName -> Assertion
forall t.
(AssertionPredicable t, HasCallStack) =>
t -> TestName -> Assertion
@? TestName
"scope checking failed unexpectedly"

      testThrows :: Term DeBruijn uni fun a -> Assertion
testThrows Term DeBruijn uni fun a
t = Either FreeVariableError () -> Bool
forall a b. Either a b -> Bool
isLeft (Term DeBruijn uni fun a -> Either FreeVariableError ()
forall {uni :: * -> *} {fun} {a}.
Term DeBruijn uni fun a -> Either FreeVariableError ()
runScope Term DeBruijn uni fun a
t)  Bool -> TestName -> Assertion
forall t.
(AssertionPredicable t, HasCallStack) =>
t -> TestName -> Assertion
@? TestName
"scope checking passed unexpectedly"

      runScope :: Term DeBruijn uni fun a -> Either FreeVariableError ()
runScope = forall e a. Except e a -> Either e a
runExcept @FreeVariableError (Except FreeVariableError () -> Either FreeVariableError ())
-> (Term DeBruijn uni fun a -> Except FreeVariableError ())
-> Term DeBruijn uni fun a
-> Either FreeVariableError ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term DeBruijn uni fun a -> Except FreeVariableError ()
forall e (m :: * -> *) name (uni :: * -> *) fun a.
(HasIndex name, MonadError e m, AsFreeVariableError e) =>
Term name uni fun a -> m ()
checkScope