Remove explainBottom (#2674)

* Add new log entry

* Format with fourmolu

* Generalize TestLog

* Materialize Nix expressions

* Rebuild

* Don't discard result in TestLog

* Use Text in WarnUnifyBottom, move TestLog, update tests (now failing)

* Use the log entry, fix the tests

* Format with fourmolu

* Remove extra newline

* Use mempty LogAction

* Turn WarnUnifyBottom into DebugUnifyBottom

* Temporarily turn on DebugUnifyBottom

* Update Entry.helpDoc

* Remove UnifierWithExplanation and the ReplOutput for unification failure

* Cleanup

* Use MonadUnify instead of MonadLog and Alternative

Co-authored-by: github-actions <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

Author: 3 people

kore/kore.cabal

@@ -360,6 +360,7 @@ library
     Kore.Log.WarnStuckClaimState
     Kore.Log.WarnSymbolSMTRepresentation
     Kore.Log.WarnTrivialClaim
+    Kore.Log.DebugUnifyBottom
     Kore.ModelChecker.Bounded
     Kore.ModelChecker.Simplification
     Kore.ModelChecker.Step

kore/src/Kore/Builtin/AssociativeCommutative.hs

@@ -55,6 +55,7 @@ import Data.Reflection (
     Given,
  )
 import qualified Data.Reflection as Reflection
+import Data.Text (Text)
 import qualified GHC.Generics as GHC
 import qualified Generics.SOP as SOP
 import qualified Kore.Attribute.Pattern.Simplified as Attribute (
@@ -103,6 +104,9 @@ import Kore.Internal.TermLike (
     pattern InternalSet_,
  )
 import qualified Kore.Internal.TermLike as TermLike
+import Kore.Log.DebugUnifyBottom (
+    debugUnifyBottomAndReturnBottom,
+ )
 import Kore.Rewriting.RewritingVariable (
     RewritingVariableName,
  )
@@ -114,17 +118,13 @@ import Kore.Syntax.Variable
 import Kore.Unification.Unify (
     MonadUnify,
  )
-import qualified Kore.Unification.Unify as Monad.Unify
 import Kore.Unparser (
     unparse,
     unparseToString,
  )
 import qualified Kore.Unparser as Unparser
 import Logic
 import Prelude.Kore
-import Pretty (
-    Doc,
- )
 import qualified Pretty
 
 -- | Any @TermWrapper@ may be inside of an 'InternalAc'.
@@ -762,7 +762,7 @@ unifyEqualsNormalized
             case toNormalized patt of
                 Bottom ->
                     lift $
-                        Monad.Unify.explainAndReturnBottom
+                        debugUnifyBottomAndReturnBottom
                             "Duplicated elements in normalization."
                             first
                             second
@@ -863,9 +863,9 @@ unifyEqualsNormalizedAc
                 (\key count result -> replicate count key ++ result)
                 []
 
-        bottomWithExplanation :: Doc () -> unifier a
+        bottomWithExplanation :: Text -> unifier a
         bottomWithExplanation explanation =
-            Monad.Unify.explainAndReturnBottom explanation first second
+            debugUnifyBottomAndReturnBottom explanation first second
 
         unifyEqualsElementLists' =
             unifyEqualsElementLists
@@ -1040,7 +1040,7 @@ buildResultFromUnifiers ::
     , InternalVariable variable
     , TermWrapper normalized
     ) =>
-    (forall result. Doc () -> unifier result) ->
+    (forall result. Text -> unifier result) ->
     [(Key, Value normalized (TermLike variable))] ->
     [(TermLike variable, Value normalized (TermLike variable))] ->
     [TermLike variable] ->
@@ -1131,7 +1131,7 @@ buildResultFromUnifiers
 
 addAllDisjoint ::
     (Monad unifier, Ord a, Hashable a) =>
-    (forall result. Doc () -> unifier result) ->
+    (forall result. Text -> unifier result) ->
     HashMap a b ->
     [(a, b)] ->
     unifier (HashMap a b)
@@ -1241,7 +1241,7 @@ unifyEqualsElementLists
             --
             -- Since the two lists have different counts, their structures can
             -- never unify.
-            Monad.Unify.explainAndReturnBottom
+            debugUnifyBottomAndReturnBottom
                 "Cannot unify ac structures with different sizes."
                 first
                 second
@@ -1294,7 +1294,7 @@ unifyEqualsElementLists
             -- The second structure does not include an opaque term, so all the
             -- elements in the first structure must be matched by elements in the second
             -- one. Since we don't have enough, we return bottom.
-            Monad.Unify.explainAndReturnBottom
+            debugUnifyBottomAndReturnBottom
                 "Cannot unify ac structures with different sizes."
                 first
                 second
@@ -1312,7 +1312,7 @@ unifyEqualsElementLists
 
             case elementListAsInternal tools (termLikeSort first) remainder2Terms of
                 Nothing ->
-                    Monad.Unify.explainAndReturnBottom
+                    debugUnifyBottomAndReturnBottom
                         "Duplicated element in unification results"
                         first
                         second
@@ -1348,7 +1348,7 @@ unifyOpaqueVariable ::
     , InternalVariable variable
     ) =>
     SmtMetadataTools Attribute.Symbol ->
-    (forall a. Doc () -> unifier a) ->
+    (forall a. Text -> unifier a) ->
     -- | unifier function
     (TermLike variable -> TermLike variable -> unifier (Pattern variable)) ->
     TermLike.ElementVariable variable ->

kore/src/Kore/Builtin/Bool.hs

@@ -56,6 +56,9 @@ import Kore.Internal.Pattern (
 import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.Symbol
 import Kore.Internal.TermLike
+import Kore.Log.DebugUnifyBottom (
+    debugUnifyBottomAndReturnBottom,
+ )
 import Kore.Rewriting.RewritingVariable
 import Kore.Step.Simplification.Simplify (
     BuiltinAndAxiomSimplifier,
@@ -64,7 +67,6 @@ import Kore.Step.Simplification.Simplify (
 import Kore.Unification.Unify (
     MonadUnify,
  )
-import qualified Kore.Unification.Unify as Unify
 import Prelude.Kore
 import qualified Text.Megaparsec as Parsec
 import qualified Text.Megaparsec.Char as Parsec
@@ -204,7 +206,7 @@ unifyBool termLike1 termLike2 unifyData
     | bool1 == bool2 =
         return (Pattern.fromTermLike termLike1)
     | otherwise =
-        Unify.explainAndReturnBottom
+        debugUnifyBottomAndReturnBottom
             "different Bool domain values"
             termLike1
             termLike2

kore/src/Kore/Builtin/Endianness.hs

@@ -28,9 +28,11 @@ import Kore.Internal.Pattern (
 import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.Symbol
 import Kore.Internal.TermLike
+import Kore.Log.DebugUnifyBottom (
+    debugUnifyBottomAndReturnBottom,
+ )
 import Kore.Unification.Unify (
     MonadUnify,
-    explainAndReturnBottom,
  )
 import qualified Kore.Verified as Verified
 import Prelude.Kore
@@ -85,7 +87,7 @@ unifyEquals termLike1@(Endianness_ end1) termLike2@(Endianness_ end2)
     | end1 == end2 = return (Pattern.fromTermLike termLike1)
     | otherwise =
         lift $
-            explainAndReturnBottom
+            debugUnifyBottomAndReturnBottom
                 "Cannot unify distinct constructors."
                 termLike1
                 termLike2

kore/src/Kore/Builtin/Int.hs

@@ -125,6 +125,7 @@ import Kore.Internal.Symbol (
     symbolHook,
  )
 import Kore.Internal.TermLike as TermLike
+import Kore.Log.DebugUnifyBottom (debugUnifyBottomAndReturnBottom)
 import Kore.Rewriting.RewritingVariable (
     RewritingVariableName,
  )
@@ -471,7 +472,8 @@ unifyInt term1 term2 unifyData =
     worker
         | on (==) internalIntValue int1 int2 =
             return $ Pattern.fromTermLike term1
-        | otherwise = explainAndReturnBottom "distinct integers" term1 term2
+        | otherwise =
+            debugUnifyBottomAndReturnBottom "distinct integers" term1 term2
 
 data UnifyIntEq = UnifyIntEq
     { eqTerm :: !(EqTerm (TermLike RewritingVariableName))

kore/src/Kore/Builtin/List.hs

@@ -100,6 +100,9 @@ import qualified Kore.Internal.TermLike as TermLike (
     isFunctionPattern,
     markSimplified,
  )
+import Kore.Log.DebugUnifyBottom (
+    debugUnifyBottom,
+ )
 import Kore.Rewriting.RewritingVariable (
     RewritingVariableName,
  )
@@ -110,7 +113,6 @@ import Kore.Syntax.Sentence (
 import Kore.Unification.Unify (
     MonadUnify,
  )
-import qualified Kore.Unification.Unify as Monad.Unify
 import Prelude.Kore
 
 {- | Verify that the sort is hooked to the builtin @List@ sort.
@@ -549,7 +551,7 @@ unifyEquals
                   where
                     prefixLength = Seq.length list1 - Seq.length suffix2
         bottomWithExplanation = do
-            Monad.Unify.explainBottom
+            debugUnifyBottom
                 "Cannot unify lists of different length."
                 first
                 second

kore/src/Kore/Builtin/Map.hs

@@ -95,6 +95,9 @@ import Kore.Internal.TermLike (
     pattern InternalMap_,
  )
 import qualified Kore.Internal.TermLike as TermLike
+import Kore.Log.DebugUnifyBottom (
+    debugUnifyBottomAndReturnBottom,
+ )
 import Kore.Rewriting.RewritingVariable (
     RewritingVariableName,
  )
@@ -573,7 +576,7 @@ unifyEquals unifyEqualsChildren first second = do
                     return (Ac.asInternal tools sort1 normalized)
                 Ac.Bottom ->
                     lift $
-                        Monad.Unify.explainAndReturnBottom
+                        debugUnifyBottomAndReturnBottom
                             "Duplicated elements in normalization."
                             first
                             second

kore/src/Kore/Builtin/Set.hs

@@ -95,6 +95,9 @@ import Kore.Internal.TermLike (
     pattern InternalSet_,
  )
 import qualified Kore.Internal.TermLike as TermLike
+import Kore.Log.DebugUnifyBottom (
+    debugUnifyBottomAndReturnBottom,
+ )
 import Kore.Rewriting.RewritingVariable (
     RewritingVariableName,
  )
@@ -585,7 +588,7 @@ unifyEquals
                         return (Ac.asInternal tools sort1 normalized)
                     Ac.Bottom ->
                         lift $
-                            Monad.Unify.explainAndReturnBottom
+                            debugUnifyBottomAndReturnBottom
                                 "Duplicated elements in normalization."
                                 first
                                 second

kore/src/Kore/Builtin/Signedness.hs

@@ -28,9 +28,11 @@ import Kore.Internal.Pattern (
 import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.Symbol
 import Kore.Internal.TermLike
+import Kore.Log.DebugUnifyBottom (
+    debugUnifyBottomAndReturnBottom,
+ )
 import Kore.Unification.Unify (
     MonadUnify,
-    explainAndReturnBottom,
  )
 import qualified Kore.Verified as Verified
 import Prelude.Kore
@@ -85,7 +87,7 @@ unifyEquals termLike1@(Signedness_ sign1) termLike2@(Signedness_ sign2)
     | sign1 == sign2 = return (Pattern.fromTermLike termLike1)
     | otherwise =
         lift $
-            explainAndReturnBottom
+            debugUnifyBottomAndReturnBottom
                 "Cannot unify distinct constructors."
                 termLike1
                 termLike2

kore/src/Kore/Builtin/String.hs

@@ -86,6 +86,9 @@ import Kore.Internal.Symbol (
     symbolHook,
  )
 import Kore.Internal.TermLike as TermLike
+import Kore.Log.DebugUnifyBottom (
+    debugUnifyBottomAndReturnBottom,
+ )
 import Kore.Log.WarnNotImplemented
 import Kore.Rewriting.RewritingVariable (
     RewritingVariableName,
@@ -514,7 +517,8 @@ unifyString term1 term2 unifyData =
     worker
         | on (==) internalStringValue string1 string2 =
             return $ Pattern.fromTermLike term1
-        | otherwise = explainAndReturnBottom "distinct strings" term1 term2
+        | otherwise =
+            debugUnifyBottomAndReturnBottom "distinct strings" term1 term2
     UnifyString{string1, string2} = unifyData
 
 {- | Unification of the @STRING.eq@ symbol