Continuation of Unification Loop Refactor

kore/src/Kore/Builtin/Bool.hs

@@ -169,6 +169,7 @@ builtinFunctions =
 
 data UnifyBool = UnifyBool
     { bool1, bool2 :: !InternalBool
+    , term1, term2 :: !(TermLike RewritingVariableName)
     }
 
 {- | Matches
@@ -187,31 +188,34 @@ matchBools ::
     TermLike RewritingVariableName ->
     TermLike RewritingVariableName ->
     Maybe UnifyBool
-matchBools first second
-    | InternalBool_ bool1 <- first
-      , InternalBool_ bool2 <- second =
-        Just UnifyBool{bool1, bool2}
+matchBools term1 term2
+    | InternalBool_ bool1 <- term2
+      , InternalBool_ bool2 <- term1 =
+        Just UnifyBool{bool1, bool2, term1, term2}
     | otherwise = Nothing
 {-# INLINE matchBools #-}
 
 -- | When bool values are equal, returns first term; otherwise returns bottom.
 unifyBool ::
     forall unifier.
     MonadUnify unifier =>
-    TermLike RewritingVariableName ->
-    TermLike RewritingVariableName ->
     UnifyBool ->
     unifier (Pattern RewritingVariableName)
-unifyBool termLike1 termLike2 unifyData
+unifyBool unifyData
     | bool1 == bool2 =
-        return (Pattern.fromTermLike termLike1)
+        return (Pattern.fromTermLike term1)
     | otherwise =
         debugUnifyBottomAndReturnBottom
             "different Bool domain values"
-            termLike1
-            termLike2
+            term1
+            term2
   where
-    UnifyBool{bool1, bool2} = unifyData
+    UnifyBool{bool1, bool2, term1, term2} = unifyData
+
+data UnifyBoolAnd = UnifyBoolAnd
+    { term :: !(TermLike RewritingVariableName)
+    , boolAnd :: !BoolAnd
+    }
 
 {- | Matches
 
@@ -222,18 +226,24 @@ unifyBool termLike1 termLike2 unifyData
 and
 
 @
-\\and{_}(\\dv{Bool}("true"), andBool(_,_))
+\\and{_}(\\dv{Bool}("true"), andBool(_,_)),
 @
+
+symmetric in the two arguments.
 -}
 matchUnifyBoolAnd ::
     TermLike RewritingVariableName ->
     TermLike RewritingVariableName ->
-    Maybe BoolAnd
+    Maybe UnifyBoolAnd
 matchUnifyBoolAnd first second
     | Just True <- matchBool first
       , Just boolAnd <- matchBoolAnd second
       , isFunctionPattern second =
-        Just boolAnd
+        Just $ UnifyBoolAnd{term = first, boolAnd}
+    | Just True <- matchBool second
+      , Just boolAnd <- matchBoolAnd first
+      , isFunctionPattern first =
+        Just $ UnifyBoolAnd{term = second, boolAnd}
     | otherwise =
         Nothing
 {-# INLINE matchUnifyBoolAnd #-}
@@ -242,12 +252,12 @@ unifyBoolAnd ::
     forall unifier.
     MonadUnify unifier =>
     TermSimplifier RewritingVariableName unifier ->
-    TermLike RewritingVariableName ->
-    BoolAnd ->
+    UnifyBoolAnd ->
     unifier (Pattern RewritingVariableName)
-unifyBoolAnd unifyChildren term boolAnd =
+unifyBoolAnd unifyChildren unifyData =
     unifyBothWith unifyChildren term operand1 operand2
   where
+    UnifyBoolAnd{term, boolAnd} = unifyData
     BoolAnd{operand1, operand2} = boolAnd
 
 {- |Takes a (function-like) pattern and unifies it against two other patterns.
@@ -275,6 +285,11 @@ unifyBothWith unify termLike1 operand1 operand2 = do
     unify' term1 term2 =
         Pattern.withoutTerm <$> unify term1 term2
 
+data UnifyBoolOr = UnifyBoolOr
+    { term :: !(TermLike RewritingVariableName)
+    , boolOr :: !BoolOr
+    }
+
 {- | Matches
 
 @
@@ -284,36 +299,42 @@ unifyBothWith unify termLike1 operand1 operand2 = do
 and
 
 @
-\\and{_}(\\dv{Bool}("false"), boolOr(_,_))
+\\and{_}(\\dv{Bool}("false"), boolOr(_,_)),
 @
+
+symmetric in the two arguments.
 -}
 matchUnifyBoolOr ::
     TermLike RewritingVariableName ->
     TermLike RewritingVariableName ->
-    Maybe BoolOr
+    Maybe UnifyBoolOr
 matchUnifyBoolOr first second
     | Just False <- matchBool first
       , Just boolOr <- matchBoolOr second
       , isFunctionPattern second =
-        Just boolOr
+        Just UnifyBoolOr{term = first, boolOr}
+    | Just False <- matchBool second
+      , Just boolOr <- matchBoolOr first
+      , isFunctionPattern first =
+        Just UnifyBoolOr{term = second, boolOr}
     | otherwise = Nothing
 {-# INLINE matchUnifyBoolOr #-}
 
 unifyBoolOr ::
     forall unifier.
     MonadUnify unifier =>
     TermSimplifier RewritingVariableName unifier ->
-    TermLike RewritingVariableName ->
-    BoolOr ->
+    UnifyBoolOr ->
     unifier (Pattern RewritingVariableName)
-unifyBoolOr unifyChildren termLike boolOr =
-    unifyBothWith unifyChildren termLike operand1 operand2
+unifyBoolOr unifyChildren unifyData =
+    unifyBothWith unifyChildren term operand1 operand2
   where
+    UnifyBoolOr{term, boolOr} = unifyData
     BoolOr{operand1, operand2} = boolOr
 
 data UnifyBoolNot = UnifyBoolNot
-    { boolNot :: BoolNot
-    , value :: Bool
+    { boolNot :: !BoolNot
+    , value :: !InternalBool
     }
 
 {- | Matches
@@ -325,8 +346,10 @@ data UnifyBoolNot = UnifyBoolNot
 and
 
 @
-\\and{_}(notBool(_), \\dv{Bool}(_))
+\\and{_}(notBool(_), \\dv{Bool}(_)),
 @
+
+symmetric in the two arguments.
 -}
 matchUnifyBoolNot ::
     TermLike RewritingVariableName ->
@@ -335,24 +358,33 @@ matchUnifyBoolNot ::
 matchUnifyBoolNot first second
     | Just boolNot <- matchBoolNot first
       , isFunctionPattern first
-      , Just value <- matchBool second =
-        Just $ UnifyBoolNot boolNot value
+      , Just value <- matchInternalBool second =
+        Just UnifyBoolNot{boolNot, value}
+    | Just boolNot <- matchBoolNot second
+      , isFunctionPattern second
+      , Just value <- matchInternalBool first =
+        Just UnifyBoolNot{boolNot, value}
     | otherwise = Nothing
 {-# INLINE matchUnifyBoolNot #-}
 
 unifyBoolNot ::
     forall unifier.
     TermSimplifier RewritingVariableName unifier ->
-    TermLike RewritingVariableName ->
     UnifyBoolNot ->
     unifier (Pattern RewritingVariableName)
-unifyBoolNot unifyChildren term unifyData =
-    let notValue = asInternal (termLikeSort term) (not value)
+unifyBoolNot unifyChildren unifyData =
+    let notValue = asInternal internalBoolSort (not internalBoolValue)
      in unifyChildren notValue operand
   where
     UnifyBoolNot{boolNot, value} = unifyData
+    InternalBool{internalBoolValue, internalBoolSort} = value
     BoolNot{operand} = boolNot
 
+matchInternalBool :: TermLike variable -> Maybe InternalBool
+matchInternalBool (InternalBool_ internalBool) =
+    Just internalBool
+matchInternalBool _ = Nothing
+
 -- | Match a @BOOL.Bool@ builtin value.
 matchBool :: TermLike variable -> Maybe Bool
 matchBool (InternalBool_ InternalBool{internalBoolValue}) =

kore/src/Kore/Builtin/Endianness.hs

@@ -7,12 +7,10 @@ module Kore.Builtin.Endianness (
     littleEndianKey,
     bigEndianKey,
     unifyEquals,
+    matchUnifyEqualsEndianness,
     module Kore.Builtin.Endianness.Endianness,
 ) where
 
-import Control.Error (
-    MaybeT,
- )
 import Data.Functor.Const
 import qualified Data.HashMap.Strict as HashMap
 import Data.String (
@@ -31,6 +29,7 @@ import Kore.Internal.TermLike
 import Kore.Log.DebugUnifyBottom (
     debugUnifyBottomAndReturnBottom,
  )
+import Kore.Rewrite.RewritingVariable
 import Kore.Unification.Unify (
     MonadUnify,
  )
@@ -77,18 +76,33 @@ littleEndianVerifier = endiannessVerifier LittleEndian
 bigEndianVerifier :: ApplicationVerifier Verified.Pattern
 bigEndianVerifier = endiannessVerifier BigEndian
 
+data UnifyEqualsEndianness = UnifyEqualsEndianness
+    { end1, end2 :: !Endianness
+    , term1, term2 :: !(TermLike RewritingVariableName)
+    }
+
+-- | Matches two terms having the Endianness constructor.
+matchUnifyEqualsEndianness ::
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName ->
+    Maybe UnifyEqualsEndianness
+matchUnifyEqualsEndianness term1 term2
+    | Endianness_ end1 <- term1
+      , Endianness_ end2 <- term2 =
+        Just UnifyEqualsEndianness{end1, end2, term1, term2}
+    | otherwise = Nothing
+{-# INLINE matchUnifyEqualsEndianness #-}
+
 unifyEquals ::
-    InternalVariable variable =>
     MonadUnify unifier =>
-    TermLike variable ->
-    TermLike variable ->
-    MaybeT unifier (Pattern variable)
-unifyEquals termLike1@(Endianness_ end1) termLike2@(Endianness_ end2)
-    | end1 == end2 = return (Pattern.fromTermLike termLike1)
+    UnifyEqualsEndianness ->
+    unifier (Pattern RewritingVariableName)
+unifyEquals unifyData
+    | end1 == end2 = return (Pattern.fromTermLike term1)
     | otherwise =
-        lift $
-            debugUnifyBottomAndReturnBottom
-                "Cannot unify distinct constructors."
-                termLike1
-                termLike2
-unifyEquals _ _ = empty
+        debugUnifyBottomAndReturnBottom
+            "Cannot unify distinct constructors."
+            term1
+            term2
+  where
+    UnifyEqualsEndianness{end1, end2, term1, term2} = unifyData

kore/src/Kore/Builtin/EqTerm.hs

@@ -8,11 +8,7 @@ module Kore.Builtin.EqTerm (
     unifyEqTerm,
 ) where
 
-import Control.Error (
-    MaybeT,
- )
 import qualified Control.Monad as Monad
-import qualified Kore.Builtin.Bool as Bool
 import qualified Kore.Internal.MultiOr as MultiOr
 import qualified Kore.Internal.OrPattern as OrPattern
 import Kore.Internal.Pattern (
@@ -61,16 +57,14 @@ unifyEqTerm ::
     TermSimplifier RewritingVariableName unifier ->
     NotSimplifier unifier ->
     EqTerm (TermLike RewritingVariableName) ->
-    TermLike RewritingVariableName ->
-    MaybeT unifier (Pattern RewritingVariableName)
-unifyEqTerm unifyChildren (NotSimplifier notSimplifier) eqTerm termLike2
-    | Just value2 <- Bool.matchBool termLike2 =
-        lift $ do
-            solution <- unifyChildren operand1 operand2 & OrPattern.gather
-            let solution' = MultiOr.map eraseTerm solution
-            (if value2 then pure else notSimplifier SideCondition.top) solution'
-                >>= Unify.scatter
-    | otherwise = empty
+    Bool ->
+    unifier (Pattern RewritingVariableName)
+unifyEqTerm unifyChildren (NotSimplifier notSimplifier) eqTerm value =
+    do
+        solution <- unifyChildren operand1 operand2 & OrPattern.gather
+        let solution' = MultiOr.map eraseTerm solution
+        (if value then pure else notSimplifier SideCondition.top) solution'
+            >>= Unify.scatter
   where
     EqTerm{operand1, operand2} = eqTerm
     eraseTerm = Pattern.fromCondition_ . Pattern.withoutTerm

kore/src/Kore/Builtin/Int.hs

@@ -435,6 +435,7 @@ matchIntEqual =
 
 data UnifyInt = UnifyInt
     { int1, int2 :: !InternalInt
+    , term1, term2 :: !(TermLike RewritingVariableName)
     }
 
 {- | Matches
@@ -453,25 +454,23 @@ matchInt ::
     TermLike RewritingVariableName ->
     TermLike RewritingVariableName ->
     Maybe UnifyInt
-matchInt first second
-    | InternalInt_ int1 <- first
-      , InternalInt_ int2 <- second =
-        Just UnifyInt{int1, int2}
+matchInt term1 term2
+    | InternalInt_ int1 <- term1
+      , InternalInt_ int2 <- term2 =
+        Just UnifyInt{int1, int2, term1, term2}
     | otherwise = Nothing
 {-# INLINE matchInt #-}
 
 -- | When int values are equal, returns first term; otherwise returns bottom.
 unifyInt ::
     forall unifier.
     MonadUnify unifier =>
-    TermLike RewritingVariableName ->
-    TermLike RewritingVariableName ->
     UnifyInt ->
     unifier (Pattern RewritingVariableName)
-unifyInt term1 term2 unifyData =
+unifyInt unifyData =
     assert (on (==) internalIntSort int1 int2) worker
   where
-    UnifyInt{int1, int2} = unifyData
+    UnifyInt{int1, int2, term1, term2} = unifyData
     worker :: unifier (Pattern RewritingVariableName)
     worker
         | on (==) internalIntValue int1 int2 =
@@ -486,8 +485,10 @@ data UnifyIntEq = UnifyIntEq
 
 {- | Matches
 @
-\\equals{_, _}(eqInt{_}(_, _), \\dv{Bool}(_))
+\\equals{_, _}(eqInt{_}(_, _), \\dv{Bool}(_)),
 @
+
+symmetric in the two arguments.
 -}
 matchUnifyIntEq ::
     TermLike RewritingVariableName ->
@@ -498,6 +499,10 @@ matchUnifyIntEq first second
       , isFunctionPattern first
       , InternalBool_ internalBool <- second =
         Just UnifyIntEq{eqTerm, internalBool}
+    | Just eqTerm <- matchIntEqual second
+      , isFunctionPattern second
+      , InternalBool_ internalBool <- first =
+        Just UnifyIntEq{eqTerm, internalBool}
     | otherwise = Nothing
 {-# INLINE matchUnifyIntEq #-}