From 01f0402d75d9360db519a9259e899b64c763fb6f Mon Sep 17 00:00:00 2001 From: Evan Marzion Date: Mon, 8 Mar 2021 09:42:27 -0600 Subject: [PATCH] adding match for And (#2435) * adding match for And * Format with stylish-haskell * trigger build * adding unit tests * fix merge * moving matchAnd after matchEqualHeads Co-authored-by: emarzion Co-authored-by: Octavian Mircea Sebe --- kore/src/Kore/Step/Axiom/Matcher.hs | 10 +++++++++ kore/test/Test/Kore/Step/Axiom/Matcher.hs | 27 +++++++++++++++++++++++ 2 files changed, 37 insertions(+) diff --git a/kore/src/Kore/Step/Axiom/Matcher.hs b/kore/src/Kore/Step/Axiom/Matcher.hs index 813fac2300..ab52b6b1e6 100644 --- a/kore/src/Kore/Step/Axiom/Matcher.hs +++ b/kore/src/Kore/Step/Axiom/Matcher.hs @@ -176,6 +176,7 @@ matchOne matchOne pair = ( matchVariable pair <|> matchEqualHeads pair + <|> matchAnd pair <|> matchExists pair <|> matchForall pair <|> matchApplication pair @@ -443,6 +444,15 @@ matchDefined (Pair term1 term2) | Defined_ def2 <- term2 = push (Pair term1 def2) | otherwise = empty +matchAnd + :: (MatchingVariable variable, MonadSimplify simplifier) + => Pair (TermLike variable) + -> MaybeT (MatcherT variable simplifier) () +matchAnd (Pair term1 term2) + | And_ _ conj1 conj2 <- term1 = + push (Pair conj1 term2) >> push (Pair conj2 term2) + | otherwise = empty + -- * Implementation type MatchingVariable variable = InternalVariable variable diff --git a/kore/test/Test/Kore/Step/Axiom/Matcher.hs b/kore/test/Test/Kore/Step/Axiom/Matcher.hs index 816011bcc3..3b8e8936f0 100644 --- a/kore/test/Test/Kore/Step/Axiom/Matcher.hs +++ b/kore/test/Test/Kore/Step/Axiom/Matcher.hs @@ -15,6 +15,7 @@ module Test.Kore.Step.Axiom.Matcher , test_matching_Exists , test_matching_Forall , test_matching_Equals + , test_matching_And , test_matcherOverloading , match , MatchResult @@ -778,6 +779,32 @@ test_matching_Pair = [(inject xInt, mkElemVar zInt), (inject yInt, mkElemVar zInt)] ] +test_matching_And :: [TestTree] +test_matching_And = + [ matches "and(x, x) matches x" + (mkAnd (mkElemVar xInt) (mkElemVar xInt)) + (mkElemVar xInt) + [] + , matches "and(x, y) matches y" + (mkAnd (mkElemVar xInt) (mkElemVar yInt)) + (mkElemVar yInt) + [(inject xInt, mkElemVar yInt)] + , matches "and(y, x) matches y" + (mkAnd (mkElemVar yInt) (mkElemVar xInt)) + (mkElemVar yInt) + [(inject xInt, mkElemVar yInt)] + , matches "and(x, y) matches z" + (mkAnd (mkElemVar xInt) (mkElemVar yInt)) + (mkElemVar zInt) + [(inject xInt, mkElemVar zInt), (inject yInt, mkElemVar zInt)] + , doesn'tMatch "and(x, 1) does not match 2" + (mkAnd (mkElemVar xInt) (mkInt 1)) + (mkInt 2) + , doesn'tMatch "and(1, x) does not match 2" + (mkAnd (mkInt 1) (mkElemVar xInt)) + (mkInt 2) + ] + mkPair :: TermLike RewritingVariableName -> TermLike RewritingVariableName