Merge priority rules (#1898)

* Tests for merging priority rules

* Merge priority rules

* Fix lint errors

* AntiLeft test

* Fix review comment

* Fix review comments.

Co-authored-by: Virgil Serbanuta <virgil.serbanuta>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>

Author: virgil-serbanuta

docs/2020-06-30-Combining-Priority-Axioms.md

@@ -53,8 +53,8 @@ priority rewrite rule.
     ...
     ∧ ¬ (∃ Xn . φn(Xn) ∧ Pn(Xn))
   ⌉
-// If β(X₁) is functional then β(X₁)∧ φ(X) = β(X₁) ∧ ⌈β(X₁)∧ φ(X)⌉
-= ⌈ β(X₁) ∧ ⌈β(X₁)∧ φ(X)⌉ ∧ P(X)
+// If β(X₁) is functional then β(X₁) ∧ φ(X) = β(X₁) ∧ ⌈β(X₁) ∧ φ(X)⌉
+= ⌈ β(X₁) ∧ ⌈β(X₁) ∧ φ(X)⌉ ∧ P(X)
     ∧ ¬ (∃ X₁ . φ₁(X₁) ∧ P₁(X₁))
     ...
     ∧ ¬ (∃ Xn . φn(Xn) ∧ Pn(Xn))

kore/src/Kore/ASTVerifier/SentenceVerifier.hs

@@ -83,6 +83,9 @@ import Kore.Internal.TermLike.TermLike
     ( freeVariables
     )
 import Kore.Sort
+import qualified Kore.Step.AntiLeft as AntiLeft
+    ( toTermLike
+    )
 import Kore.Step.Rule
     ( QualifiedAxiomPattern (..)
     , fromSentenceAxiom
@@ -426,7 +429,8 @@ verifyClaimSentence sentence =
           where
             rightVars, leftVars :: Set (SomeVariable VariableName)
             rightVars = freeVariables rhs & FreeVariables.toSet
-            lhs = catMaybes [antiLeft] <> [left, unwrapPredicate requires]
+            lhs = Foldable.toList (AntiLeft.toTermLike <$> antiLeft)
+                <> [left, unwrapPredicate requires]
             leftVars = foldMap freeVariables lhs & FreeVariables.toSet
 
 verifySorts :: [ParsedSentence] -> SentenceVerifier ()