module Test.Kore.Rewrite.Implication (
    test_freeVariables,
    test_refreshRule,
    test_substitute,
) where

import Data.Default
import Data.Foldable qualified as Foldable
import Data.Map.Strict qualified as Map
import Data.Set qualified as Set
import Kore.Attribute.Pattern.FreeVariables as FreeVariables
import Kore.Internal.Conditional (
    fromPredicate,
 )
import Kore.Internal.OrPattern qualified as OrPattern
import Kore.Internal.Pattern qualified as Pattern
import Kore.Internal.Predicate qualified as Predicate
import Kore.Internal.TermLike
import Kore.Rewrite.Implication
import Kore.Rewrite.RewritingVariable
import Kore.Rewrite.UnifyingRule
import Prelude.Kore
import Test.Kore.Rewrite.MockSymbols qualified as Mock
import Test.Tasty
import Test.Tasty.HUnit.Ext

test_freeVariables :: TestTree
test_freeVariables =
    testCase "Extract free variables" $ do
        let expect =
                foldMap
                    (freeVariable . mkSomeVariable)
                    [x, z, t]
            actual = freeVariables testRulePattern
        assertEqual "Expected free variables" expect actual

test_refreshRule :: [TestTree]
test_refreshRule =
    [ testCase "Rename target variables" $ do
        let avoiding :: FreeVariables RewritingVariableName
            avoiding = freeVariables testRulePattern
            (renaming, rulePattern') =
                refreshRule avoiding testRulePattern
            renamed = Set.fromList (Foldable.toList renaming)
            free' :: FreeVariables RewritingVariableName
            free' = freeVariables rulePattern'
            notAvoided (variableName -> var) =
                not (FreeVariables.isFreeVariable var avoiding)
        assertEqual
            "Expected to rename all free variables of original RulePattern"
            (FreeVariables.toNames avoiding)
            (Map.keysSet renaming)
        assertBool
            "Expected to renamed variables distinct from original variables"
            (all notAvoided renamed)
        assertBool
            "Expected no free variables in common with original RulePattern"
            (all notAvoided (FreeVariables.toList free'))
    , testCase "no stale variables" $ do
        let (renaming, _) = refreshRule mempty testRulePattern
        assertBool "expected not to rename variables" (null renaming)
    , testGroup "stale existentials" $
        let assertions (renaming, claim@Implication{existentials}) = do
                assertBool
                    "expected to refresh existentials"
                    (notElem y existentials)
                assertBool
                    "expected to substitute fresh variables"
                    (notElem (inject y) $ FreeVariables.toList (freeVariablesRight claim))
                assertBool
                    "expected not to rename free variables"
                    (null renaming)
         in [ testCase "from outside" $ do
                let stale = freeVariable (inject y)
                assertions $ refreshRule stale testRulePattern
            , testCase "from left-hand side" $ do
                let input =
                        testRulePattern
                            { left =
                                Pattern.fromTermAndPredicate
                                    (mkElemVar y)
                                    ( Predicate.makeCeilPredicate
                                        (mkElemVar z)
                                    )
                            }
                assertions $ refreshRule mempty input
            ]
    ]

test_substitute :: [TestTree]
test_substitute =
    [ testCase "does not capture free variables from the substitution" $ do
        let dummy =
                Pattern.fromCondition
                    Mock.testSort
                    (fromPredicate Predicate.makeTruePredicate)
            right = OrPattern.fromTermLike (mkElemVar y)
            imp = mkImplication () dummy right [x]
            newImp =
                substitute
                    (Map.singleton (inject $ variableName y) (mkElemVar x))
                    imp
        assertBool "Expected the expected variable to not be captured" $
            not $ nullFreeVariables $ freeVariablesRight newImp
    ]

testRulePattern :: Implication ()
testRulePattern =
    Implication
        { left =
            -- Include an implicitly-quantified variable.
            Pattern.fromTermAndPredicate
                (mkElemVar x)
                (Predicate.makeCeilPredicate (mkElemVar z))
        , modality = ()
        , existentials = [y]
        , right =
            Pattern.fromTermAndPredicate
                (mkElemVar y)
                (Predicate.makeCeilPredicate (mkElemVar t))
                & OrPattern.fromPattern
        , attributes = def
        }

x, y, z, t :: ElementVariable RewritingVariableName
x = mapElementVariable (pure mkRuleVariable) Mock.x
y = mapElementVariable (pure mkRuleVariable) Mock.y
z = mapElementVariable (pure mkRuleVariable) Mock.z
t = mapElementVariable (pure mkRuleVariable) Mock.t

 Include an implicitly-quantified variable.
module Test.Kore.Rewrite.Implication (
    test_freeVariables,
    test_refreshRule,
    test_substitute,
) where

import Data.Default
import Data.Foldable qualified as Foldable
import Data.Map.Strict qualified as Map
import Data.Set qualified as Set
import Kore.Attribute.Pattern.FreeVariables as FreeVariables
import Kore.Internal.Conditional (
    fromPredicate,
 )
import Kore.Internal.OrPattern qualified as OrPattern
import Kore.Internal.Pattern qualified as Pattern
import Kore.Internal.Predicate qualified as Predicate
import Kore.Internal.TermLike
import Kore.Rewrite.Implication
import Kore.Rewrite.RewritingVariable
import Kore.Rewrite.UnifyingRule
import Prelude.Kore
import Test.Kore.Rewrite.MockSymbols qualified as Mock
import Test.Tasty
import Test.Tasty.HUnit.Ext

test_freeVariables :: TestTree
test_freeVariables =
    testCase "Extract free variables" $ do
        let expect =
                foldMap
                    (freeVariable . mkSomeVariable)
                    [x, z, t]
            actual = freeVariables testRulePattern
        assertEqual "Expected free variables" expect actual

test_refreshRule :: [TestTree]
test_refreshRule =
    [ testCase "Rename target variables" $ do
        let avoiding :: FreeVariables RewritingVariableName
            avoiding = freeVariables testRulePattern
            (renaming, rulePattern') =
                refreshRule avoiding testRulePattern
            renamed = Set.fromList (Foldable.toList renaming)
            free' :: FreeVariables RewritingVariableName
            free' = freeVariables rulePattern'
            notAvoided (variableName -> var) =
                not (FreeVariables.isFreeVariable var avoiding)
        assertEqual
            "Expected to rename all free variables of original RulePattern"
            (FreeVariables.toNames avoiding)
            (Map.keysSet renaming)
        assertBool
            "Expected to renamed variables distinct from original variables"
            (all notAvoided renamed)
        assertBool
            "Expected no free variables in common with original RulePattern"
            (all notAvoided (FreeVariables.toList free'))
    , testCase "no stale variables" $ do
        let (renaming, _) = refreshRule mempty testRulePattern
        assertBool "expected not to rename variables" (null renaming)
    , testGroup "stale existentials" $
        let assertions (renaming, claim@Implication{existentials}) = do
                assertBool
                    "expected to refresh existentials"
                    (notElem y existentials)
                assertBool
                    "expected to substitute fresh variables"
                    (notElem (inject y) $ FreeVariables.toList (freeVariablesRight claim))
                assertBool
                    "expected not to rename free variables"
                    (null renaming)
         in [ testCase "from outside" $ do
                let stale = freeVariable (inject y)
                assertions $ refreshRule stale testRulePattern
            , testCase "from left-hand side" $ do
                let input =
                        testRulePattern
                            { left =
                                Pattern.fromTermAndPredicate
                                    (mkElemVar y)
                                    ( Predicate.makeCeilPredicate
                                        (mkElemVar z)
                                    )
                            }
                assertions $ refreshRule mempty input
            ]
    ]

test_substitute :: [TestTree]
test_substitute =
    [ testCase "does not capture free variables from the substitution" $ do
        let dummy =
                Pattern.fromCondition
                    Mock.testSort
                    (fromPredicate Predicate.makeTruePredicate)
            right = OrPattern.fromTermLike (mkElemVar y)
            imp = mkImplication () dummy right [x]
            newImp =
                substitute
                    (Map.singleton (inject $ variableName y) (mkElemVar x))
                    imp
        assertBool "Expected the expected variable to not be captured" $
            not $ nullFreeVariables $ freeVariablesRight newImp
    ]

testRulePattern :: Implication ()
testRulePattern =
    Implication
        { left =
            Pattern.fromTermAndPredicate
                (mkElemVar x)
                (Predicate.makeCeilPredicate (mkElemVar z))
        , modality = ()
        , existentials = [y]
        , right =
            Pattern.fromTermAndPredicate
                (mkElemVar y)
                (Predicate.makeCeilPredicate (mkElemVar t))
                & OrPattern.fromPattern
        , attributes = def
        }

x, y, z, t :: ElementVariable RewritingVariableName
x = mapElementVariable (pure mkRuleVariable) Mock.x
y = mapElementVariable (pure mkRuleVariable) Mock.y
z = mapElementVariable (pure mkRuleVariable) Mock.z
t = mapElementVariable (pure mkRuleVariable) Mock.t
