Replay "Issue 2100 follow up (#2574)"

This reverts commit 97494af.

Author: ttuegel

kore/src/Kore/ASTVerifier/SentenceVerifier.hs

@@ -48,7 +48,7 @@ import Kore.ASTVerifier.PatternVerifier as PatternVerifier
 import Kore.ASTVerifier.SortVerifier
 import Kore.ASTVerifier.Verifier
 import qualified Kore.Attribute.Axiom as Attribute (
-    Axiom (..),
+    Axiom,
     parseAxiomAttributes,
  )
 import qualified Kore.Attribute.Hook as Attribute

kore/src/Kore/Equation/Sentence.hs

@@ -65,14 +65,38 @@ data MatchEquationError variable
     deriving anyclass (Debug)
 
 instance InternalVariable variable => Pretty (MatchEquationError variable) where
-    pretty (NotEquation term) = "The given term is not an equation:\n" <> unparse term
-    pretty (RequiresError notPred) = "The equation's requires clause is not a predicate:\n" <> pretty notPred
-    pretty (ArgumentError notPred) = "The equation's argument clause is not a predicate:\n" <> pretty notPred
-    pretty (AntiLeftError notPred) = "The equation's anti-left clause is not a predicate:\n" <> pretty notPred
-    pretty (EnsuresError notPred) = "The equation's ensures clause is not a predicate:\n" <> pretty notPred
-    pretty FunctionalAxiom = "The term is a functional axiom"
-    pretty ConstructorAxiom = "The term is a constructor axiom"
-    pretty SubsortAxiom = "The term is a subsort axiom"
+    pretty (NotEquation term) =
+        Pretty.vsep
+            [ "The given term is not an equation:"
+            , unparse term
+            ]
+    pretty (RequiresError notPred) =
+        Pretty.vsep
+            [ "The equation's requires clause is not a predicate:"
+            , pretty notPred
+            , "This is a frontend bug. Please report this error at https://github.com/kframework/k/issues."
+            ]
+    pretty (ArgumentError notPred) =
+        Pretty.vsep
+            [ "The equation's argument clause is not a predicate:"
+            , pretty notPred
+            , "This is a frontend bug. Please report this error at https://github.com/kframework/k/issues."
+            ]
+    pretty (AntiLeftError notPred) =
+        Pretty.vsep
+            [ "The equation's anti-left clause is not a predicate:"
+            , pretty notPred
+            , "This is a frontend bug. Please report this error at https://github.com/kframework/k/issues."
+            ]
+    pretty (EnsuresError notPred) =
+        Pretty.vsep
+            [ "The equation's ensures clause is not a predicate:"
+            , pretty notPred
+            , "This is a frontend bug. Please report this error at https://github.com/kframework/k/issues."
+            ]
+    pretty FunctionalAxiom = "The term is a functional axiom."
+    pretty ConstructorAxiom = "The term is a constructor axiom."
+    pretty SubsortAxiom = "The term is a subsort axiom."
 
 matchEquation ::
     forall variable.

kore/src/Kore/Equation/Validate.hs

@@ -113,14 +113,14 @@ validateAxiom attrs verified =
                 pack $
                     show $
                         Pretty.vsep
-                            [ "Head of LHS of Not Simplification axiom is not a non-constructor function symbol. This is the LHS symbol:"
+                            [ "Expected function symbol, but found constructor symbol:"
                             , unparse sym
                             ]
 
         checkVarFunctionArguments =
             failOnJust
                 eq
-                "LHS of NotSimplification axiom contains non-variable:"
+                "Expected variable, but found:"
                 $ asum $ getNotVar <$> termLikeF
 
         getNotVar (TermLike.Var_ _) = Nothing
@@ -129,7 +129,7 @@ validateAxiom attrs verified =
     checkArg _ Nothing = return ()
     checkArg eq (Just arg) =
         traverse_
-            ( failOnJust eq "Found invalid subterm of Axiom equation argument:"
+            ( failOnJust eq "Found invalid subterm in argument of function equation:"
                 . checkArgIn
             )
             $ Predicate.getMultiAndPredicate arg
@@ -144,20 +144,7 @@ validateAxiom attrs verified =
             _
                 | TermLike.isConstructorLike term -> descend
             TermLike.App_ sym _
-                | or
-                    [ Symbol.isConstructorLike sym
-                    , Symbol.isAnywhere sym && Symbol.isInjective sym
-                    , Map.isSymbolConcat sym
-                    , Map.isSymbolElement sym
-                    , Map.isSymbolUnit sym
-                    , Set.isSymbolConcat sym
-                    , Set.isSymbolElement sym
-                    , Set.isSymbolUnit sym
-                    , List.isSymbolConcat sym
-                    , List.isSymbolElement sym
-                    , List.isSymbolUnit sym
-                    ] ->
-                    descend
+                | isGoodSymbol sym -> descend
                 | otherwise -> Just term
             TermLike.InternalBytes_ _ _ -> Nothing
             TermLike.InternalBool_ _ -> Nothing
@@ -170,6 +157,20 @@ validateAxiom attrs verified =
             _ -> Just term
           where
             _ :< termF = Recursive.project term
+            isGoodSymbol sym =
+                or
+                    [ Symbol.isConstructorLike sym
+                    , Symbol.isAnywhere sym && Symbol.isInjective sym
+                    , Map.isSymbolConcat sym
+                    , Map.isSymbolElement sym
+                    , Map.isSymbolUnit sym
+                    , Set.isSymbolConcat sym
+                    , Set.isSymbolElement sym
+                    , Set.isSymbolUnit sym
+                    , List.isSymbolConcat sym
+                    , List.isSymbolElement sym
+                    , List.isSymbolUnit sym
+                    ]
             descend = asum $ findBadArgSubterm <$> termF
 
     failOnJust _ _ Nothing = return ()