{-# LANGUAGE OverloadedLists  #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies     #-}
module Evaluation.FreeVars (test_freevars) where

import PlutusCore.Default
import PlutusCore.Evaluation.Machine.ExBudgetingDefaults qualified as PLC
import PlutusCore.MkPlc
import PlutusCore.StdLib.Data.Unit
import PlutusPrelude
import UntypedPlutusCore as UPLC
import UntypedPlutusCore.Evaluation.Machine.Cek
import UntypedPlutusCore.Evaluation.Machine.Cek.Internal
import UntypedPlutusCore.Test.DeBruijn.Bad
import UntypedPlutusCore.Test.DeBruijn.Good

import Test.Tasty
import Test.Tasty.HUnit

-- | Test the behaviour of Cek evaluator module *directly*
-- by using the Internal module, thus bypassing any prior term conformance checks, e.g.
-- that the term is closed (no free variables).
testCekInternalFree :: TestTree
testCekInternalFree :: TestTree
testCekInternalFree = TestName -> [TestTree] -> TestTree
testGroup TestName
"cekInternal" ([TestTree] -> TestTree) -> [TestTree] -> TestTree
forall a b. (a -> b) -> a -> b
$ ((TestName, Assertion) -> TestTree)
-> [(TestName, Assertion)] -> [TestTree]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TestName -> Assertion -> TestTree)
-> (TestName, Assertion) -> TestTree
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TestName -> Assertion -> TestTree
testCase)
    [(TestName
"delay0", Term DeBruijn DefaultUni DefaultFun () -> Bool
eval (()
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term DeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
var0) Bool -> Bool -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Bool
True)
    ,(TestName
"fun0var0", Term DeBruijn DefaultUni DefaultFun () -> Bool
eval Term DeBruijn DefaultUni DefaultFun ()
fun0var0 Bool -> Bool -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Bool
True)
    -- Interesting example because it is a `const x y` where x is a value and y is out-of-scope.
    -- The evaluation result (success or failure) depends on how the machine
    -- ignores  the irrelevant to the computation) part of the environment.
    ,(TestName
"const0var0", Term DeBruijn DefaultUni DefaultFun () -> Bool
eval (Term DeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
const0 Term DeBruijn DefaultUni DefaultFun ()
-> [Term DeBruijn DefaultUni DefaultFun ()]
-> Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ [Item [Term DeBruijn DefaultUni DefaultFun ()]
Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni ()) =>
term ()
unitval, Item [Term DeBruijn DefaultUni DefaultFun ()]
Term DeBruijn DefaultUni DefaultFun ()
fun0var0]) Bool -> Bool -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Bool
True)
    -- same as above, plus match on discharged value to show that freevar is completely ignored
    ,(TestName
"const0var0Discharge", Term DeBruijn DefaultUni DefaultFun ()
-> Either
     (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
     (Term NamedDeBruijn DefaultUni DefaultFun ())
evalV (Term DeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
const0 Term DeBruijn DefaultUni DefaultFun ()
-> [Term DeBruijn DefaultUni DefaultFun ()]
-> Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ [Item [Term DeBruijn DefaultUni DefaultFun ()]
Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni ()) =>
term ()
unitval, Item [Term DeBruijn DefaultUni DefaultFun ()]
Term DeBruijn DefaultUni DefaultFun ()
fun0var0]) Either
  (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
  (Term NamedDeBruijn DefaultUni DefaultFun ())
-> Either
     (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
     (Term NamedDeBruijn DefaultUni DefaultFun ())
-> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Term NamedDeBruijn DefaultUni DefaultFun ()
-> Either
     (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
     (Term NamedDeBruijn DefaultUni DefaultFun ())
forall a b. b -> Either a b
Right Term NamedDeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni ()) =>
term ()
unitval)
    ,(TestName
"iteLazy0", Term DeBruijn DefaultUni DefaultFun () -> Bool
eval Term DeBruijn DefaultUni DefaultFun ()
iteLazy0 Bool -> Bool -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Bool
True)
    ,(TestName
"iteStrict0", Term DeBruijn DefaultUni DefaultFun () -> Bool
eval Term DeBruijn DefaultUni DefaultFun ()
iteStrict0 Bool -> Bool -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Bool
False)
    ,(TestName
"illITELazy", Term DeBruijn DefaultUni DefaultFun () -> Bool
eval Term DeBruijn DefaultUni DefaultFun ()
illITELazy Bool -> Bool -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Bool
True)
    ,(TestName
"illITEStrict", Term DeBruijn DefaultUni DefaultFun () -> Bool
eval Term DeBruijn DefaultUni DefaultFun ()
illITEStrict Bool -> Bool -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Bool
True)
    ,(TestName
"illAdd", Term DeBruijn DefaultUni DefaultFun () -> Bool
eval Term DeBruijn DefaultUni DefaultFun ()
illAdd Bool -> Bool -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Bool
False)
    ,(TestName
"illOverAppBuiltin", Term DeBruijn DefaultUni DefaultFun () -> Bool
eval Term DeBruijn DefaultUni DefaultFun ()
illOverAppBuiltin Bool -> Bool -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Bool
False)
    ,(TestName
"illOverAppFun", Term DeBruijn DefaultUni DefaultFun () -> Bool
eval Term DeBruijn DefaultUni DefaultFun ()
illOverAppFun Bool -> Bool -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Bool
False)
    ]
  where
      evalV :: Term DeBruijn DefaultUni DefaultFun ()
-> Either
     (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
     (Term NamedDeBruijn DefaultUni DefaultFun ())
evalV = Term DeBruijn DefaultUni DefaultFun ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun ann.
Term DeBruijn uni fun ann -> Term NamedDeBruijn uni fun ann
toFakeTerm
             (Term DeBruijn DefaultUni DefaultFun ()
 -> Term NamedDeBruijn DefaultUni DefaultFun ())
-> (Term NamedDeBruijn DefaultUni DefaultFun ()
    -> Either
         (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
         (Term NamedDeBruijn DefaultUni DefaultFun ()))
-> Term DeBruijn DefaultUni DefaultFun ()
-> Either
     (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
     (Term NamedDeBruijn DefaultUni DefaultFun ())
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ())
-> ExBudgetMode CountingSt DefaultUni DefaultFun
-> EmitterMode DefaultUni DefaultFun
-> Term NamedDeBruijn DefaultUni DefaultFun ()
-> CekReport CountingSt NamedDeBruijn DefaultUni DefaultFun
forall (uni :: * -> *) fun ann cost.
ThrowableBuiltins uni fun =>
MachineParameters CekMachineCosts fun (CekValue uni fun ann)
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> NTerm uni fun ann
-> CekReport cost NamedDeBruijn uni fun
runCekDeBruijn MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ())
forall ann.
Typeable ann =>
MachineParameters
  CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
PLC.defaultCekParametersForTesting ExBudgetMode CountingSt DefaultUni DefaultFun
forall (uni :: * -> *) fun. ExBudgetMode CountingSt uni fun
counting EmitterMode DefaultUni DefaultFun
forall (uni :: * -> *) fun. EmitterMode uni fun
noEmitter
             (Term NamedDeBruijn DefaultUni DefaultFun ()
 -> CekReport CountingSt NamedDeBruijn DefaultUni DefaultFun)
-> (CekReport CountingSt NamedDeBruijn DefaultUni DefaultFun
    -> Either
         (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
         (Term NamedDeBruijn DefaultUni DefaultFun ()))
-> Term NamedDeBruijn DefaultUni DefaultFun ()
-> Either
     (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
     (Term NamedDeBruijn DefaultUni DefaultFun ())
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> CekReport CountingSt NamedDeBruijn DefaultUni DefaultFun
-> CekResult NamedDeBruijn DefaultUni DefaultFun
forall cost name (uni :: * -> *) fun.
CekReport cost name uni fun -> CekResult name uni fun
_cekReportResult
             (CekReport CountingSt NamedDeBruijn DefaultUni DefaultFun
 -> CekResult NamedDeBruijn DefaultUni DefaultFun)
-> (CekResult NamedDeBruijn DefaultUni DefaultFun
    -> Either
         (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
         (Term NamedDeBruijn DefaultUni DefaultFun ()))
-> CekReport CountingSt NamedDeBruijn DefaultUni DefaultFun
-> Either
     (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
     (Term NamedDeBruijn DefaultUni DefaultFun ())
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> CekResult NamedDeBruijn DefaultUni DefaultFun
-> Either
     (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
     (Term NamedDeBruijn DefaultUni DefaultFun ())
forall name (uni :: * -> *) fun.
CekResult name uni fun
-> Either
     (CekEvaluationException name uni fun) (Term name uni fun ())
cekResultToEither

      eval :: Term DeBruijn DefaultUni DefaultFun () -> Bool
eval = Term DeBruijn DefaultUni DefaultFun ()
-> Either
     (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
     (Term NamedDeBruijn DefaultUni DefaultFun ())
evalV
             (Term DeBruijn DefaultUni DefaultFun ()
 -> Either
      (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
      (Term NamedDeBruijn DefaultUni DefaultFun ()))
-> (Either
      (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
      (Term NamedDeBruijn DefaultUni DefaultFun ())
    -> Bool)
-> Term DeBruijn DefaultUni DefaultFun ()
-> Bool
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Either
  (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
  (Term NamedDeBruijn DefaultUni DefaultFun ())
-> Bool
forall a b. Either a b -> Bool
isRight


-- | Test the behaviour of discharge function against open terms (containing free variables)
-- by manually constructing CekValue's and Cek Environment's. The free variables should
-- be left untouched.
testDischargeFree :: TestTree
testDischargeFree :: TestTree
testDischargeFree = TestName -> [TestTree] -> TestTree
testGroup TestName
"discharge" ([TestTree] -> TestTree) -> [TestTree] -> TestTree
forall a b. (a -> b) -> a -> b
$ ((TestName, Assertion) -> TestTree)
-> [(TestName, Assertion)] -> [TestTree]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TestName -> Assertion -> TestTree)
-> (TestName, Assertion) -> TestTree
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TestName -> Assertion -> TestTree
testCase)
    [(TestName
"freeRemains1", Assertion
freeRemains1)
    ,(TestName
"freeRemains2", Assertion
freeRemains2)
    ]
  where
    freeRemains1 :: Assertion
freeRemains1 =
        -- dis( empty |- (delay (\x ->var0)) ) === (delay (\x -> var0))
        CekValue DefaultUni DefaultFun ()
-> DischargeResult DefaultUni DefaultFun
forall {ann}.
CekValue DefaultUni DefaultFun ann
-> DischargeResult DefaultUni DefaultFun
dis (Term NamedDeBruijn DefaultUni DefaultFun ()
-> CekValEnv DefaultUni DefaultFun ()
-> CekValue DefaultUni DefaultFun ()
forall (uni :: * -> *) fun ann.
NTerm uni fun ann -> CekValEnv uni fun ann -> CekValue uni fun ann
VDelay (Term DeBruijn DefaultUni DefaultFun ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun ann.
Term DeBruijn uni fun ann -> Term NamedDeBruijn uni fun ann
toFakeTerm Term DeBruijn DefaultUni DefaultFun ()
fun0var0)
            []) -- empty env
        DischargeResult DefaultUni DefaultFun
-> DischargeResult DefaultUni DefaultFun -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?=
        Term NamedDeBruijn DefaultUni DefaultFun ()
-> DischargeResult DefaultUni DefaultFun
forall (uni :: * -> *) fun.
NTerm uni fun () -> DischargeResult uni fun
DischargeNonConstant (Term DeBruijn DefaultUni DefaultFun ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun ann.
Term DeBruijn uni fun ann -> Term NamedDeBruijn uni fun ann
toFakeTerm (Term DeBruijn DefaultUni DefaultFun ()
 -> Term NamedDeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term DeBruijn DefaultUni DefaultFun ()
fun0var0)

    freeRemains2 :: Assertion
freeRemains2 =
        -- dis( y:unit |- \x-> x y var0) ) === (\x -> x unit var0)
        -- x is bound so it is left alone
        -- y is discharged from the env
        -- var0 is free so it is left alone
        CekValue DefaultUni DefaultFun ()
-> DischargeResult DefaultUni DefaultFun
forall {ann}.
CekValue DefaultUni DefaultFun ann
-> DischargeResult DefaultUni DefaultFun
dis (NamedDeBruijn
-> Term NamedDeBruijn DefaultUni DefaultFun ()
-> CekValEnv DefaultUni DefaultFun ()
-> CekValue DefaultUni DefaultFun ()
forall (uni :: * -> *) fun ann.
NamedDeBruijn
-> NTerm uni fun ann
-> CekValEnv uni fun ann
-> CekValue uni fun ann
VLamAbs (DeBruijn -> NamedDeBruijn
fakeNameDeBruijn (DeBruijn -> NamedDeBruijn) -> DeBruijn -> NamedDeBruijn
forall a b. (a -> b) -> a -> b
$ Index -> DeBruijn
DeBruijn Index
deBruijnInitIndex)
                (Term DeBruijn DefaultUni DefaultFun ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun ann.
Term DeBruijn uni fun ann -> Term NamedDeBruijn uni fun ann
toFakeTerm (Term DeBruijn DefaultUni DefaultFun ()
 -> Term NamedDeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
                 Index -> Term DeBruijn DefaultUni DefaultFun ()
forall {uni :: * -> *} {fun}. Index -> Term DeBruijn uni fun ()
v Index
1 Term DeBruijn DefaultUni DefaultFun ()
-> [Term DeBruijn DefaultUni DefaultFun ()]
-> Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ -- x
                 [Index -> Term DeBruijn DefaultUni DefaultFun ()
forall {uni :: * -> *} {fun}. Index -> Term DeBruijn uni fun ()
v Index
2 -- y
                 ,Item [Term DeBruijn DefaultUni DefaultFun ()]
Term DeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
var0 -- free
                 ]
                )
             [Some (ValueOf DefaultUni) -> CekValue DefaultUni DefaultFun ()
forall (uni :: * -> *) fun ann.
Some (ValueOf uni) -> CekValue uni fun ann
VCon (Some (ValueOf DefaultUni) -> CekValue DefaultUni DefaultFun ())
-> Some (ValueOf DefaultUni) -> CekValue DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ () -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). Contains uni a => a -> Some (ValueOf uni)
someValue ()] -- env has y
            )
         DischargeResult DefaultUni DefaultFun
-> DischargeResult DefaultUni DefaultFun -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?=
         Term NamedDeBruijn DefaultUni DefaultFun ()
-> DischargeResult DefaultUni DefaultFun
forall (uni :: * -> *) fun.
NTerm uni fun () -> DischargeResult uni fun
DischargeNonConstant (Term DeBruijn DefaultUni DefaultFun ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun ann.
Term DeBruijn uni fun ann -> Term NamedDeBruijn uni fun ann
toFakeTerm (Term DeBruijn DefaultUni DefaultFun ()
 -> Term NamedDeBruijn DefaultUni DefaultFun ())
-> (Term DeBruijn DefaultUni DefaultFun ()
    -> Term DeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term DeBruijn DefaultUni DefaultFun ()
-> Term DeBruijn DefaultUni DefaultFun ()
forall t (uni :: * -> *) fun.
(t ~ Term DeBruijn uni fun ()) =>
t -> t
lamAbs0 (Term DeBruijn DefaultUni DefaultFun ()
 -> Term NamedDeBruijn DefaultUni DefaultFun ())
-> Term DeBruijn DefaultUni DefaultFun ()
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$
             Index -> Term DeBruijn DefaultUni DefaultFun ()
forall {uni :: * -> *} {fun}. Index -> Term DeBruijn uni fun ()
v Index
1 Term DeBruijn DefaultUni DefaultFun ()
-> [Term DeBruijn DefaultUni DefaultFun ()]
-> Term DeBruijn DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
@@ -- x
             [ ()
-> Some (ValueOf DefaultUni)
-> Term DeBruijn DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term name uni fun ann
Constant () (() -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). Contains uni a => a -> Some (ValueOf uni)
someValue ()) -- substituted y
             , Item [Term DeBruijn DefaultUni DefaultFun ()]
Term DeBruijn DefaultUni DefaultFun ()
forall (uni :: * -> *) fun. Term DeBruijn uni fun ()
var0 -- free
             ]
         )

    dis :: CekValue DefaultUni DefaultFun ann
-> DischargeResult DefaultUni DefaultFun
dis = forall (uni :: * -> *) fun ann.
CekValue uni fun ann -> DischargeResult uni fun
dischargeCekValue @DefaultUni @DefaultFun
    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

test_freevars :: TestTree
test_freevars :: TestTree
test_freevars = TestName -> [TestTree] -> TestTree
testGroup TestName
"FreeVars"
    [ Item [TestTree]
TestTree
testCekInternalFree
    , Item [TestTree]
TestTree
testDischargeFree
    ]

-- shortcuts
toFakeTerm :: Term DeBruijn uni fun ann -> Term NamedDeBruijn uni fun ann
toFakeTerm :: forall (uni :: * -> *) fun ann.
Term DeBruijn uni fun ann -> Term NamedDeBruijn uni fun ann
toFakeTerm = (DeBruijn -> NamedDeBruijn)
-> Term DeBruijn uni fun ann -> Term NamedDeBruijn uni fun ann
forall name name' (uni :: * -> *) fun ann.
(name -> name') -> Term name uni fun ann -> Term name' uni fun ann
termMapNames DeBruijn -> NamedDeBruijn
fakeNameDeBruijn