Revert #1714

kore/CHANGELOG.md

@@ -22,7 +22,6 @@ All notable changes to this project will be documented in this file.
 
 ### Changed
 
-- Execution does not branch when evaluating the hooked `KEQUAL.eq` function.
 - Clarified the message accompanying the "substitution coverage" error.
 
 ### Fixed

kore/src/Kore/Builtin/Bool.hs

@@ -14,8 +14,6 @@ module Kore.Builtin.Bool
     , extractBoolDomainValue
     , parse
     , termAndEquals
-    , termNotBool
-    , matchBool
       -- * Keys
     , orKey
     , andKey
@@ -210,26 +208,7 @@ termAndEquals unifyChildren a b =
         unification2 <- unifyChildren' termLike1 operand2
         let conditions = unification1 <> unification2
         pure (Pattern.withCondition termLike1 conditions)
-    worker _ _ = empty
 
-termNotBool
-    :: forall variable unifier
-    .  InternalVariable variable
-    => MonadUnify unifier
-    => TermSimplifier variable unifier
-    -> TermLike variable
-    -> TermLike variable
-    -> MaybeT unifier (Pattern variable)
-termNotBool unifyChildren a b =
-    worker a b <|> worker b a
-  where
-    worker termLike1 boolTerm
-      | Just BoolNot { operand } <- matchBoolNot termLike1
-      , isFunctionPattern termLike1
-      , Just value <- matchBool boolTerm
-      = lift $ do
-        let notValue = asInternal (termLikeSort boolTerm) (not value)
-        unifyChildren notValue operand
     worker _ _ = empty
 
 {- | Match a @BOOL.Bool@ builtin value.
@@ -255,20 +234,3 @@ matchBoolAnd (App_ symbol [operand1, operand2]) = do
     Monad.guard (hook2 == andKey)
     return BoolAnd { symbol, operand1, operand2 }
 matchBoolAnd _ = Nothing
-
-{- | The @BOOL.not@ hooked symbol applied to a @term@-type argument.
- -}
-data BoolNot term =
-    BoolNot
-        { symbol  :: !Symbol
-        , operand :: !term
-        }
-
-{- | Match the @BOOL.not@ hooked symbol.
- -}
-matchBoolNot :: TermLike variable -> Maybe (BoolNot (TermLike variable))
-matchBoolNot (App_ symbol [operand]) = do
-    hook2 <- (getHook . symbolHook) symbol
-    Monad.guard (hook2 == notKey)
-    return BoolNot { symbol, operand }
-matchBoolNot _ = Nothing

kore/src/Kore/Builtin/KEqual.hs

@@ -17,8 +17,6 @@ builtin modules.
 module Kore.Builtin.KEqual
     ( verifiers
     , builtinFunctions
-    , KEqual (..)
-    , termKEquals
       -- * keys
     , eqKey
     , neqKey
@@ -27,11 +25,6 @@ module Kore.Builtin.KEqual
 
 import Prelude.Kore
 
-import Control.Error
-    ( MaybeT
-    , hoistMaybe
-    )
-import qualified Control.Monad as Monad
 import qualified Data.Functor.Foldable as Recursive
 import qualified Data.HashMap.Strict as HashMap
 import Data.Map.Strict
@@ -45,9 +38,6 @@ import Data.Text
     ( Text
     )
 
-import Kore.Attribute.Hook
-    ( Hook (..)
-    )
 import qualified Kore.Attribute.Pattern as Attribute
 import qualified Kore.Builtin.Bool as Bool
 import Kore.Builtin.Builtin
@@ -56,22 +46,20 @@ import Kore.Builtin.Builtin
 import qualified Kore.Builtin.Builtin as Builtin
 import qualified Kore.Error
 import qualified Kore.Internal.OrPattern as OrPattern
-import Kore.Internal.Pattern
-    ( Pattern
-    )
 import qualified Kore.Internal.Pattern as Pattern
 import qualified Kore.Internal.SideCondition as SideCondition
-import Kore.Internal.Symbol
+    ( topTODO
+    )
 import Kore.Internal.TermLike
-import Kore.Step.Simplification.NotSimplifier
+import qualified Kore.Step.Simplification.And as And
+import qualified Kore.Step.Simplification.Ceil as Ceil
+import qualified Kore.Step.Simplification.Equals as Equals
+import qualified Kore.Step.Simplification.Not as Not
+import qualified Kore.Step.Simplification.Or as Or
 import Kore.Step.Simplification.Simplify
 import Kore.Syntax.Definition
     ( SentenceSymbol (..)
     )
-import Kore.Unification.Unify as Unify
-import Kore.Unification.Unify
-    ( MonadUnify
-    )
 
 verifiers :: Builtin.Verifiers
 verifiers =
@@ -137,8 +125,7 @@ builtinFunctions =
     ]
 
 evalKEq
-    :: forall variable simplifier
-    .  (InternalVariable variable, MonadSimplify simplifier)
+    :: (InternalVariable variable, MonadSimplify simplifier)
     => Bool
     -> CofreeF
         (Application Symbol)
@@ -147,24 +134,41 @@ evalKEq
     -> simplifier (AttemptedAxiom variable)
 evalKEq true (valid :< app) =
     case applicationChildren of
-        [t1, t2] -> Builtin.getAttemptedAxiom (evalEq t1 t2)
+        [t1, t2] -> evalEq t1 t2
         _ -> Builtin.wrongArity (if true then eqKey else neqKey)
   where
+    sideCondition = SideCondition.topTODO
+    false = not true
     sort = Attribute.patternSort valid
     Application { applicationChildren } = app
-    comparison x y
-        | true = x == y
-        | otherwise = x /= y
-    evalEq
-        :: TermLike variable
-        -> TermLike variable
-        -> MaybeT simplifier (AttemptedAxiom variable)
     evalEq termLike1 termLike2 = do
-        asConcrete1 <- hoistMaybe $ Builtin.toKey termLike1
-        asConcrete2 <- hoistMaybe $ Builtin.toKey termLike2
-        Builtin.appliedFunction
-            $ Bool.asPattern sort
-            $ comparison asConcrete1 asConcrete2
+        let pattern1 = Pattern.fromTermLike termLike1
+            pattern2 = Pattern.fromTermLike termLike2
+
+        defined1 <- Ceil.makeEvaluate sideCondition pattern1
+        defined2 <- Ceil.makeEvaluate sideCondition pattern2
+        defined <-
+            And.simplifyEvaluated Not.notSimplifier sideCondition defined1 defined2
+
+        equalTerms <-
+            Equals.makeEvaluateTermsToPredicate
+                termLike1
+                termLike2
+                sideCondition
+        let trueTerm = Bool.asInternal sort true
+            truePatterns = Pattern.withCondition trueTerm <$> equalTerms
+
+        notEqualTerms <- Not.simplifyEvaluatedPredicate equalTerms
+        let falseTerm = Bool.asInternal sort false
+            falsePatterns = Pattern.withCondition falseTerm <$> notEqualTerms
+
+        let undefinedResults = Or.simplifyEvaluated truePatterns falsePatterns
+        results <-
+            And.simplifyEvaluated Not.notSimplifier sideCondition defined undefinedResults
+        pure $ Applied AttemptedAxiomResults
+            { results
+            , remainders = OrPattern.bottom
+            }
 
 evalKIte
     :: forall variable simplifier
@@ -204,51 +208,3 @@ neqKey = "KEQUAL.neq"
 
 iteKey :: IsString s => s
 iteKey = "KEQUAL.ite"
-
-{- | The @KEQUAL.eq@ hooked symbol applied to @term@-type arguments.
- -}
-data KEqual term =
-    KEqual
-        { symbol :: !Symbol
-        , operand1, operand2 :: !term
-        }
-
-{- | Match the @KEQUAL.eq@ hooked symbol.
- -}
-matchKEqual :: TermLike variable -> Maybe (KEqual (TermLike variable))
-matchKEqual (App_ symbol [operand1, operand2]) = do
-    hook2 <- (getHook . symbolHook) symbol
-    Monad.guard (hook2 == eqKey)
-    return KEqual { symbol, operand1, operand2 }
-matchKEqual _ = Nothing
-
-termKEquals
-    :: forall variable unifier
-    .  InternalVariable variable
-    => MonadUnify unifier
-    => TermSimplifier variable unifier
-    -> NotSimplifier unifier
-    -> TermLike variable
-    -> TermLike variable
-    -> MaybeT unifier (Pattern variable)
-termKEquals unifyChildren (NotSimplifier notSimplifier) a b =
-    worker a b <|> worker b a
-  where
-    eraseTerm =
-        Pattern.fromCondition . Pattern.withoutTerm
-    worker termLike1 termLike2
-      | Just KEqual { operand1, operand2 } <- matchKEqual termLike1
-      , isFunctionPattern termLike1
-      , Just value2 <- Bool.matchBool termLike2
-      = lift $ do
-        solution <-
-            fmap OrPattern.fromPatterns
-            <$> Unify.gather
-            $ unifyChildren operand1 operand2
-        let solution' = fmap eraseTerm solution
-        finalSolution <-
-            if value2
-                then return solution'
-                else notSimplifier SideCondition.top solution'
-        Unify.scatter finalSolution
-    worker _ _ = empty

kore/src/Kore/Step/Simplification/AndTerms.hs

@@ -35,7 +35,6 @@ import qualified Data.Text.Prettyprint.Doc as Pretty
 
 import qualified Kore.Builtin.Bool as Builtin.Bool
 import qualified Kore.Builtin.Endianness as Builtin.Endianness
-import qualified Kore.Builtin.KEqual as Builtin.KEqual
 import qualified Kore.Builtin.List as Builtin.List
 import qualified Kore.Builtin.Map as Builtin.Map
 import qualified Kore.Builtin.Set as Builtin.Set
@@ -231,8 +230,6 @@ andEqualsFunctions notSimplifier = fmap mapEqualsFunctions
     , (BothT,   \_ _ _ -> constructorAndEqualsAssumesDifferentHeads, "constructorAndEqualsAssumesDifferentHeads")
     , (BothT,   \_ _ s -> overloadedConstructorSortInjectionAndEquals s, "overloadedConstructorSortInjectionAndEquals")
     , (BothT,   \_ _ s -> Builtin.Bool.termAndEquals s, "Builtin.Bool.termAndEquals")
-    , (BothT,   \_ _ s -> Builtin.Bool.termNotBool s, "Builtin.Bool.termNotBool")
-    , (EqualsT, \_ _ s -> Builtin.KEqual.termKEquals s notSimplifier, "Builtin.KEqual.termKEquals")
     , (BothT,   \_ _ _ -> Builtin.Endianness.unifyEquals, "Builtin.Endianness.unifyEquals")
     , (BothT,   \_ _ _ -> Builtin.Signedness.unifyEquals, "Builtin.Signedness.unifyEquals")
     , (BothT,   \_ _ s -> Builtin.Map.unifyEquals s, "Builtin.Map.unifyEquals")