Revert "Validate function definitions (#2168)"

This reverts commit 39a42a5.

Author: ttuegel

Dockerfile

@@ -20,7 +20,6 @@ RUN    curl -sSL https://github.com/github/hub/releases/download/v$HUB/hub-linux
     && rm -fr hub-linux-amd64-$HUB
 
 ENV LC_ALL=C.UTF-8
-ADD ./src/main/kore/prelude.kore /usr/include/kframework/kore/prelude.kore
 
 ARG USER_ID=1000
 ARG GROUP_ID=1000

kore/kore.cabal

@@ -289,7 +289,6 @@ library
     Kore.Equation.Registry
     Kore.Equation.Sentence
     Kore.Equation.Simplification
-    Kore.Equation.Validate
     Kore.Error
     Kore.Exec
     Kore.IndexedModule.Error

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
@@ -68,11 +68,10 @@ import qualified Kore.Attribute.Sort.HasDomainValues as Attribute.HasDomainValue
 import qualified Kore.Attribute.Symbol as Attribute
 import qualified Kore.Attribute.Symbol as Attribute.Symbol
 import qualified Kore.Builtin as Builtin
-import Kore.Equation.Validate
 import Kore.Error
 import Kore.IndexedModule.IndexedModule
 import Kore.IndexedModule.Resolvers as Resolvers
-import qualified Kore.Internal.Symbol as Symbol
+import qualified Kore.Internal.Symbol as Internal.Symbol
 import Kore.Internal.TermLike.TermLike (
     freeVariables,
  )
@@ -357,7 +356,6 @@ verifyAxiomSentence sentence =
                 verifiedModule'
                 (freeVariables sentence)
                 (sentenceAxiomAttributes sentence)
-        validateAxiom attrs verified
         State.modify $ addAxiom verified attrs
   where
     addAxiom verified attrs =
@@ -485,7 +483,7 @@ parseAndVerifyAxiomAttributes ::
     IndexedModule Verified.Pattern Attribute.Symbol attrs ->
     FreeVariables VariableName ->
     Attributes ->
-    error (Attribute.Axiom Symbol.Symbol VariableName)
+    error (Attribute.Axiom Internal.Symbol.Symbol VariableName)
 parseAndVerifyAxiomAttributes indexModule freeVars attrs =
     parseAxiomAttributes' attrs >>= verifyAxiomAttributes indexModule
   where

kore/src/Kore/Equation/Registry.hs

@@ -27,6 +27,7 @@ import Kore.Attribute.Axiom (
  )
 import qualified Kore.Attribute.Axiom as Attribute
 import Kore.Attribute.Overload
+import qualified Kore.Attribute.Pattern as Pattern
 import Kore.Attribute.Symbol (
     StepperAttributes,
  )
@@ -49,6 +50,7 @@ import Kore.Syntax.Sentence (
  )
 import qualified Kore.Verified as Verified
 import Prelude.Kore
+import qualified Pretty
 
 -- | Create a mapping from symbol identifiers to their defining axioms.
 extractEquations ::
@@ -110,10 +112,11 @@ partitionEquations equations =
     equations' =
         equations
             & filter (not . ignoreEquation)
-    (simplificationRules, functionRules) =
+    (simplificationRules, unProcessedFunctionRules) =
         partition Equation.isSimplificationRule
             . sortOn Equation.equationPriority
             $ equations'
+    functionRules = filter (not . ignoreDefinition) unProcessedFunctionRules
 
 {- | Should we ignore the 'EqualityRule' for evaluation or simplification?
 
@@ -137,3 +140,17 @@ ignoreEquation Equation{attributes}
     Unit{isUnit} = Attribute.unit attributes
     Idem{isIdem} = Attribute.idem attributes
     Overload{getOverload} = Attribute.overload attributes
+
+-- | Should we ignore the 'EqualityRule' for evaluating function definitions?
+ignoreDefinition :: Equation RewritingVariableName -> Bool
+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)

kore/src/Kore/Equation/Sentence.hs

@@ -38,12 +38,8 @@ import qualified Kore.Internal.TermLike as TermLike
 import Kore.Syntax.Sentence (
     SentenceAxiom (..),
  )
-import Kore.Unparser (
-    unparse,
- )
 import qualified Kore.Verified as Verified
 import Prelude.Kore
-import Pretty
 
 fromSentenceAxiom ::
     (Attribute.Axiom Symbol VariableName, Verified.SentenceAxiom) ->
@@ -64,16 +60,6 @@ data MatchEquationError variable
     deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
     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"
-
 matchEquation ::
     forall variable.
     InternalVariable variable =>

kore/src/Kore/Equation/Validate.hs

@@ -1105,6 +1105,12 @@ hasFreeVariable ::
     Bool
 hasFreeVariable variableName = isFreeVariable variableName . freeVariables
 
+{- | Traverse the predicate from the top down and apply substitutions.
+
+The 'freeVariables' annotation is used to avoid traversing subterms that
+contain none of the targeted variables.
+-}
+
 -- !!  TODO The following is just a temporary solution and  !!
 -- !!  the code using wrapPredicate should be refactored    !!
 
@@ -1118,11 +1124,6 @@ wrapPredicate =
         id
         . makePredicate
 
-{- | Traverse the predicate from the top down and apply substitutions.
-
-The 'freeVariables' annotation is used to avoid traversing subterms that
-contain none of the targeted variables.
--}
 substitute ::
     InternalVariable variable =>
     Map (SomeVariableName variable) (TermLike variable) ->

kore/src/Kore/Internal/Predicate.hs

@@ -14,7 +14,6 @@ module Kore.Internal.Symbol (
     isTotal,
     isInjective,
     isMemo,
-    isAnywhere,
     noEvaluators,
     symbolHook,
     constructor,
@@ -171,9 +170,6 @@ isTotal = Attribute.isTotal . symbolAttributes
 isMemo :: Symbol -> Bool
 isMemo = Attribute.isMemo . Attribute.memo . symbolAttributes
 
-isAnywhere :: Symbol -> Bool
-isAnywhere = Attribute.isAnywhere . Attribute.anywhere . symbolAttributes
-
 noEvaluators :: Symbol -> Bool
 noEvaluators =
     Attribute.hasNoEvaluators . Attribute.noEvaluators . symbolAttributes