Revert "Issue 2100 follow up (#2574)"

This reverts commit 9733608.

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,38 +65,14 @@ data MatchEquationError variable
     deriving anyclass (Debug)
 
 instance InternalVariable variable => Pretty (MatchEquationError variable) where
-    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."
+    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"
 
 matchEquation ::
     forall variable.

kore/src/Kore/Equation/Validate.hs

@@ -113,14 +113,14 @@ validateAxiom attrs verified =
                 pack $
                     show $
                         Pretty.vsep
-                            [ "Expected function symbol, but found constructor symbol:"
+                            [ "Head of LHS of Not Simplification axiom is not a non-constructor function symbol. This is the LHS symbol:"
                             , unparse sym
                             ]
 
         checkVarFunctionArguments =
             failOnJust
                 eq
-                "Expected variable, but found:"
+                "LHS of NotSimplification axiom contains non-variable:"
                 $ 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 in argument of function equation:"
+            ( failOnJust eq "Found invalid subterm of Axiom equation argument:"
                 . checkArgIn
             )
             $ Predicate.getMultiAndPredicate arg
@@ -144,7 +144,20 @@ validateAxiom attrs verified =
             _
                 | TermLike.isConstructorLike term -> descend
             TermLike.App_ sym _
-                | isGoodSymbol sym -> descend
+                | 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
                 | otherwise -> Just term
             TermLike.InternalBytes_ _ _ -> Nothing
             TermLike.InternalBool_ _ -> Nothing
@@ -157,20 +170,6 @@ 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 ()