Do not return \bottom for unsolved List unification cases (#2693)

ttuegel · web-flow · commit 295d9b958a73 · 2021-06-25T16:39:32.000-05:00
* Kore.Builtin.Builtin: Remove function unifyEqualsUnsolved

This function tries to re-simplify unsolved unification problems, but it makes
no sense to do that: we are already in the simplifier for the type of
unification problem, and attempting to re-simplify the unsolved problem cannot
make any more progress!

* Kore.Builtin.List.unifyEquals: Do not return \bottom for unsolved cases
diff --git a/kore/src/Kore/Builtin/Builtin.hs b/kore/src/Kore/Builtin/Builtin.hs
@@ -39,7 +39,6 @@ module Kore.Builtin.Builtin (
     makeDomainValuePattern,
 
     -- * Implementing builtin unification
-    unifyEqualsUnsolved,
     module Kore.Builtin.Verifiers,
 ) where
 
@@ -78,51 +77,28 @@ import qualified Kore.IndexedModule.Resolvers as IndexedModule
 import Kore.Internal.ApplicationSorts
 import qualified Kore.Internal.OrPattern as OrPattern
 import Kore.Internal.Pattern (
-    Conditional (..),
     Pattern,
  )
 import Kore.Internal.Pattern as Pattern (
     fromTermLike,
-    top,
-    withCondition,
  )
-import Kore.Internal.Predicate (
-    makeEqualsPredicate,
- )
-import qualified Kore.Internal.Predicate as Predicate
 import Kore.Internal.SideCondition (
     SideCondition,
  )
-import qualified Kore.Internal.SideCondition as SideCondition (
-    topTODO,
- )
 import Kore.Internal.TermLike as TermLike
-import Kore.Rewriting.RewritingVariable (
-    RewritingVariableName,
- )
 import Kore.Sort (
     predicateSort,
  )
-import Kore.Step.Simplification.SimplificationType as SimplificationType (
-    SimplificationType (..),
- )
 import Kore.Step.Simplification.Simplify (
     AttemptedAxiom (..),
     AttemptedAxiomResults (AttemptedAxiomResults),
     BuiltinAndAxiomSimplifier (BuiltinAndAxiomSimplifier),
     MonadSimplify,
     applicationAxiomSimplifier,
-    makeEvaluateTermCeil,
  )
 import qualified Kore.Step.Simplification.Simplify as AttemptedAxiomResults (
     AttemptedAxiomResults (..),
  )
-import Kore.Unification.Unify (
-    MonadUnify,
- )
-import qualified Kore.Unification.Unify as Monad.Unify (
-    scatter,
- )
 import Kore.Unparser
 import Prelude.Kore
 
@@ -494,27 +470,6 @@ getAttemptedAxiom ::
 getAttemptedAxiom attempt =
     fromMaybe NotApplicable <$> runMaybeT attempt
 
--- | Return an unsolved unification problem.
-unifyEqualsUnsolved ::
-    MonadUnify unifier =>
-    SimplificationType ->
-    TermLike RewritingVariableName ->
-    TermLike RewritingVariableName ->
-    unifier (Pattern RewritingVariableName)
-unifyEqualsUnsolved SimplificationType.And a b = do
-    let unified = TermLike.markSimplified $ mkAnd a b
-    orCondition <-
-        makeEvaluateTermCeil
-            SideCondition.topTODO
-            unified
-    predicate <- Monad.Unify.scatter orCondition
-    return (unified `Pattern.withCondition` predicate)
-unifyEqualsUnsolved SimplificationType.Equals a b =
-    return
-        Pattern.top
-            { predicate = Predicate.markSimplified $ makeEqualsPredicate a b
-            }
-
 makeDomainValueTerm ::
     InternalVariable variable =>
     Sort ->
diff --git a/kore/src/Kore/Builtin/List.hs b/kore/src/Kore/Builtin/List.hs
@@ -103,9 +103,6 @@ import qualified Kore.Internal.TermLike as TermLike (
 import Kore.Rewriting.RewritingVariable (
     RewritingVariableName,
  )
-import Kore.Step.Simplification.SimplificationType (
-    SimplificationType,
- )
 import Kore.Step.Simplification.Simplify as Simplifier
 import Kore.Syntax.Sentence (
     SentenceSort (..),
@@ -384,7 +381,6 @@ builtinFunctions =
 unifyEquals ::
     forall unifier.
     MonadUnify unifier =>
-    SimplificationType ->
     ( TermLike RewritingVariableName ->
       TermLike RewritingVariableName ->
       unifier (Pattern RewritingVariableName)
@@ -393,7 +389,6 @@ unifyEquals ::
     TermLike RewritingVariableName ->
     MaybeT unifier (Pattern RewritingVariableName)
 unifyEquals
-    simplificationType
     simplifyChild
     first
     second =
@@ -426,8 +421,8 @@ unifyEquals
             | otherwise = empty
         unifyEquals0 (App_ symbol1 args1) (App_ symbol2 args2)
             | isSymbolConcat symbol1
-              , isSymbolConcat symbol1 =
-                lift $ case (args1, args2) of
+              , isSymbolConcat symbol2 =
+                case (args1, args2) of
                     ( [InternalList_ builtin1, x1@(Var_ _)]
                         , [InternalList_ builtin2, x2@(Var_ _)]
                         ) ->
@@ -437,6 +432,7 @@ unifyEquals
                                 x1
                                 builtin2
                                 x2
+                                & lift
                     ( [x1@(Var_ _), InternalList_ builtin1]
                         , [x2@(Var_ _), InternalList_ builtin2]
                         ) ->
@@ -446,23 +442,20 @@ unifyEquals
                                 builtin1
                                 x2
                                 builtin2
+                                & lift
                     _ -> empty
-        unifyEquals0 dv1@(InternalList_ builtin1) pat2 =
+        unifyEquals0 (InternalList_ builtin1) pat2 =
             case pat2 of
                 InternalList_ builtin2 ->
                     lift $ unifyEqualsConcrete builtin1 builtin2
-                app@(App_ symbol2 args2)
+                (App_ symbol2 args2)
                     | isSymbolConcat symbol2 ->
-                        lift $ case args2 of
+                        case args2 of
                             [InternalList_ builtin2, x@(Var_ _)] ->
-                                unifyEqualsFramedRight builtin1 builtin2 x
+                                unifyEqualsFramedRight builtin1 builtin2 x & lift
                             [x@(Var_ _), InternalList_ builtin2] ->
-                                unifyEqualsFramedLeft builtin1 x builtin2
-                            [_, _] ->
-                                Builtin.unifyEqualsUnsolved
-                                    simplificationType
-                                    dv1
-                                    app
+                                unifyEqualsFramedLeft builtin1 x builtin2 & lift
+                            [_, _] -> empty
                             _ -> Builtin.wrongArity concatKey
                     | otherwise -> empty
                 _ -> empty
diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs
@@ -73,9 +73,6 @@ import Kore.Step.Simplification.NoConfusion
 import Kore.Step.Simplification.NotSimplifier
 import Kore.Step.Simplification.OverloadSimplifier as OverloadSimplifier
 import Kore.Step.Simplification.Overloading as Overloading
-import qualified Kore.Step.Simplification.SimplificationType as SimplificationType (
-    SimplificationType (..),
- )
 import Kore.Step.Simplification.Simplify as Simplifier
 import Kore.Unification.Unify as Unify
 import Kore.Unparser
@@ -212,11 +209,7 @@ maybeTermEquals notSimplifier childTransformers first second = do
                 , Builtin.Map.unifyEquals childTransformers first second
                 , Builtin.Map.unifyNotInKeys childTransformers notSimplifier first second
                 , Builtin.Set.unifyEquals childTransformers first second
-                , Builtin.List.unifyEquals
-                    SimplificationType.Equals
-                    childTransformers
-                    first
-                    second
+                , Builtin.List.unifyEquals childTransformers first second
                 , domainValueAndConstructorErrors first second
                 ]
 
@@ -300,11 +293,7 @@ maybeTermAnd notSimplifier childTransformers first second = do
                 , Builtin.Signedness.unifyEquals first second
                 , Builtin.Map.unifyEquals childTransformers first second
                 , Builtin.Set.unifyEquals childTransformers first second
-                , Builtin.List.unifyEquals
-                    SimplificationType.And
-                    childTransformers
-                    first
-                    second
+                , Builtin.List.unifyEquals childTransformers first second
                 , domainValueAndConstructorErrors first second
                 , Error.hoistMaybe (functionAnd first second)
                 ]
diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs
@@ -20,7 +20,7 @@ import Data.Text (
  )
 import qualified Kore.Builtin.AssociativeCommutative as Ac
 import Kore.Internal.Condition as Condition
-import qualified Kore.Internal.Conditional as Conditional
+import Kore.Internal.From
 import Kore.Internal.InternalSet
 import Kore.Internal.MultiAnd (
     MultiAnd,
@@ -937,10 +937,9 @@ test_andTermsSimplification =
             actual <- unify term7 term8
             assertEqual "" expect actual
         , testCase "fallback for external List symbols" $ do
-            let expectTerm = mkAnd rhs lhs
-                expect =
-                    Pattern.fromTermLike expectTerm
-                        `Conditional.andPredicate` makeCeilPredicate expectTerm
+            let expect =
+                    (Pattern.withCondition rhs)
+                        (fromEquals_ rhs lhs & Condition.fromPredicate)
                 x = mkElemVar $ configElementVariableFromId "x" Mock.testSort
                 l = mkElemVar $ configElementVariableFromId "y" Mock.listSort
                 -- List unification does not fully succeed because the
