{-# 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 ()
@@ [ Index -> Term DeBruijn DefaultUni DefaultFun ()
forall {uni :: * -> *} {fun}. Index -> Term DeBruijn uni fun ()
v Index
2 -- x
                  -- 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 ()
@@ [ ()
-> 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 ()) -- x
                -- 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