Display location of rejected function equations (#2408)

* adding source location info for ignoreDefinition assertion

* switch branches

* Add error message for non-function-like definitions

Co-authored-by: Thomas Tuegel <thomas.tuegel@runtimeverification.com>

Author: emarzion

kore/src/Kore/Equation/Registry.hs

@@ -51,6 +51,7 @@ import Kore.Syntax.Sentence
     ( SentenceAxiom (..)
     )
 import qualified Kore.Verified as Verified
+import qualified Pretty
 
 {- | Create a mapping from symbol identifiers to their defining axioms.
 
@@ -154,8 +155,13 @@ ignoreEquation Equation { attributes }
 {- | Should we ignore the 'EqualityRule' for evaluating function definitions?
  -}
 ignoreDefinition :: Equation VariableName -> Bool
-ignoreDefinition Equation { left } =
-    assert isLeftFunctionLike False
+ignoreDefinition Equation { attributes, left }
+    | isLeftFunctionLike = False
+    | otherwise = (error . show . Pretty.vsep)
+        [ "left-hand side of equation was not function-like at:"
+        , Pretty.indent 4 $ Pretty.pretty sourceLocation
+        ]
   where
+    Attribute.Axiom { sourceLocation } = attributes
     isLeftFunctionLike =
         (Pattern.isFunction . Pattern.function) (extractAttributes left)