Refactor Unification Loop (#2602)

* Prelude.Kore: Export Data.Functor.(<&>)

* Prelude.Kore: Export Data.Functor.void

* initial work on substituting out old functions

* Format with fourmolu

* Committing current progress.

* pushing test failure

* Changing type signatures and splitting up unifyInj

* Fixed sortInjectionAndEquals

* Format with fourmolu

* Refactoring constructorAndEqualsAssumesDifferentHeads

* Format with fourmolu

* near fix for overloadedConstructorSortInjectionAndEquals

* Format with fourmolu

* More progress and reverting overloadedConstructor...

* Format with fourmolu

* trigger build

* Using named field puns

* Format with fourmolu

* Cleaning up code based on review suggestions

* Format with fourmolu

* Misc. cleanup.

* Adding inj args to InjUnify

* Format with fourmolu

* adding missing strict field annotations

* documentation for matches + minor code fixes

* Format with fourmolu

* reverting the removal of assertions

* Fixing documentation + removal of unncess. type annotation

* Format with fourmolu

* changing matchBytesDifferent to matchBytes

* Format with fourmolu

* Apply worker-wrapper transformation

Apply a worker-wrapper transformation to functions maybeTermAnd and
maybeTermEquals to preserve their encapsulation and avoid passing redundant
arguments.

* sortInjectionAndEquals: Remove extra argument

* Remove AndEquals terminology around sort injections

* Format with fourmolu

* unifyInjs: Simplify signature

* Clean up injection simplifier

* Format with fourmolu

* Test.Kore.Builtin.KEqual: Clean up

* Test.Kore.Builtin.Int: Clean up

* Test.Kore.Builtin.Bool: Clean up

* Kore.Step.Simplification.ExpandAlias: Clean up

* Extract Bytes unifier to Kore.Builtin.InternalBytes

* Clean up UnifyStringLiteral

* Clean up variableFunctionAnd

* Separate matchVariables and matchVariableFunction

* Format with fourmolu

Co-authored-by: Thomas Tuegel <ttuegel@mailbox.org>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Thomas Tuegel <thomas.tuegel@runtimeverification.com>

Author: 3 people

kore/src/Kore/Builtin/Bool.hs

@@ -16,6 +16,10 @@ module Kore.Builtin.Bool (
     unifyBoolOr,
     unifyBoolNot,
     matchBool,
+    matchBools,
+    matchUnifyBoolAnd,
+    matchUnifyBoolOr,
+    matchUnifyBoolNot,
 
     -- * Keys
     orKey,
@@ -29,9 +33,6 @@ module Kore.Builtin.Bool (
     orElseKey,
 ) where
 
-import Control.Error (
-    MaybeT,
- )
 import qualified Control.Monad as Monad
 import Data.Functor.Const
 import qualified Data.HashMap.Strict as HashMap
@@ -55,6 +56,7 @@ import Kore.Internal.Pattern (
 import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.Symbol
 import Kore.Internal.TermLike
+import Kore.Rewriting.RewritingVariable
 import Kore.Step.Simplification.Simplify (
     BuiltinAndAxiomSimplifier,
     TermSimplifier,
@@ -163,48 +165,88 @@ builtinFunctions =
     xor a b = (a && not b) || (not a && b)
     implies a b = not a || b
 
--- | Unification of @BOOL.Bool@ values.
+data UnifyBool = UnifyBool
+    { bool1, bool2 :: !InternalBool
+    }
+
+{- | Matches
+
+@
+\\equals{_, _}(\\dv{Bool}(_), \\dv{Bool}(_))
+@
+
+and
+
+@
+\\and{_}(\\dv{Bool}(_), \\dv{Bool}(_))
+@
+-}
+matchBools ::
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName ->
+    Maybe UnifyBool
+matchBools first second
+    | InternalBool_ bool1 <- first
+      , InternalBool_ bool2 <- second =
+        Just UnifyBool{bool1, bool2}
+    | otherwise = Nothing
+{-# INLINE matchBools #-}
+
+-- | When bool values are equal, returns first term; otherwise returns bottom.
 unifyBool ::
-    forall variable unifier.
-    InternalVariable variable =>
+    forall unifier.
     MonadUnify unifier =>
-    TermLike variable ->
-    TermLike variable ->
-    MaybeT unifier (Pattern variable)
-unifyBool a b =
-    worker a b <|> worker b a
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName ->
+    UnifyBool ->
+    unifier (Pattern RewritingVariableName)
+unifyBool termLike1 termLike2 unifyData
+    | bool1 == bool2 =
+        return (Pattern.fromTermLike termLike1)
+    | otherwise =
+        Unify.explainAndReturnBottom
+            "different Bool domain values"
+            termLike1
+            termLike2
   where
-    worker termLike1 termLike2
-        | Just value1 <- matchBool termLike1
-          , Just value2 <- matchBool termLike2 =
-            lift $
-                if value1 == value2
-                    then return (Pattern.fromTermLike termLike1)
-                    else
-                        Unify.explainAndReturnBottom
-                            "different Bool domain values"
-                            termLike1
-                            termLike2
-    worker _ _ = empty
+    UnifyBool{bool1, bool2} = unifyData
+
+{- | Matches
+
+@
+\\equals{_, _}(\\dv{Bool}("true"), andBool(_,_))
+@
+
+and
+
+@
+\\and{_}(\\dv{Bool}("true"), andBool(_,_))
+@
+-}
+matchUnifyBoolAnd ::
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName ->
+    Maybe BoolAnd
+matchUnifyBoolAnd first second
+    | Just True <- matchBool first
+      , Just boolAnd <- matchBoolAnd second
+      , isFunctionPattern second =
+        Just boolAnd
+    | otherwise =
+        Nothing
+{-# INLINE matchUnifyBoolAnd #-}
 
 unifyBoolAnd ::
-    forall variable unifier.
-    InternalVariable variable =>
+    forall unifier.
     MonadUnify unifier =>
-    TermSimplifier variable unifier ->
-    TermLike variable ->
-    TermLike variable ->
-    MaybeT unifier (Pattern variable)
-unifyBoolAnd unifyChildren a b =
-    worker a b <|> worker b a
+    TermSimplifier RewritingVariableName unifier ->
+    TermLike RewritingVariableName ->
+    BoolAnd ->
+    unifier (Pattern RewritingVariableName)
+unifyBoolAnd unifyChildren term boolAnd =
+    unifyBothWith unifyChildren term operand1 operand2
   where
-    worker termLike1 termLike2
-        | Just value1 <- matchBool termLike1
-          , value1
-          , Just BoolAnd{operand1, operand2} <- matchBoolAnd termLike2
-          , isFunctionPattern termLike2 =
-            unifyBothWith unifyChildren termLike1 operand1 operand2
-    worker _ _ = empty
+    BoolAnd{operand1, operand2} = boolAnd
 
 {- |Takes a (function-like) pattern and unifies it against two other patterns.
    Returns the original pattern and the conditions resulting from unification.
@@ -221,8 +263,8 @@ unifyBothWith ::
     TermLike variable ->
     -- | first term to be unified with the base term
     TermLike variable ->
-    MaybeT unifier (Pattern variable)
-unifyBothWith unify termLike1 operand1 operand2 = lift $ do
+    unifier (Pattern variable)
+unifyBothWith unify termLike1 operand1 operand2 = do
     unification1 <- unify' termLike1 operand1
     unification2 <- unify' termLike1 operand2
     let conditions = unification1 <> unification2
@@ -231,44 +273,83 @@ unifyBothWith unify termLike1 operand1 operand2 = lift $ do
     unify' term1 term2 =
         Pattern.withoutTerm <$> unify term1 term2
 
+{- | Matches
+
+@
+\\equals{_, _}(\\dv{Bool}("false"), boolOr(_,_))
+@
+
+and
+
+@
+\\and{_}(\\dv{Bool}("false"), boolOr(_,_))
+@
+-}
+matchUnifyBoolOr ::
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName ->
+    Maybe BoolOr
+matchUnifyBoolOr first second
+    | Just False <- matchBool first
+      , Just boolOr <- matchBoolOr second
+      , isFunctionPattern second =
+        Just boolOr
+    | otherwise = Nothing
+{-# INLINE matchUnifyBoolOr #-}
+
 unifyBoolOr ::
-    forall variable unifier.
-    InternalVariable variable =>
+    forall unifier.
     MonadUnify unifier =>
-    TermSimplifier variable unifier ->
-    TermLike variable ->
-    TermLike variable ->
-    MaybeT unifier (Pattern variable)
-unifyBoolOr unifyChildren a b =
-    worker a b <|> worker b a
+    TermSimplifier RewritingVariableName unifier ->
+    TermLike RewritingVariableName ->
+    BoolOr ->
+    unifier (Pattern RewritingVariableName)
+unifyBoolOr unifyChildren termLike boolOr =
+    unifyBothWith unifyChildren termLike operand1 operand2
   where
-    worker termLike1 termLike2
-        | Just value1 <- matchBool termLike1
-          , not value1
-          , Just BoolOr{operand1, operand2} <- matchBoolOr termLike2
-          , isFunctionPattern termLike2 =
-            unifyBothWith unifyChildren termLike1 operand1 operand2
-    worker _ _ = empty
+    BoolOr{operand1, operand2} = boolOr
+
+data UnifyBoolNot = UnifyBoolNot
+    { boolNot :: BoolNot
+    , value :: Bool
+    }
+
+{- | Matches
+
+@
+\\equals{_, _}(notBool(_), \\dv{Bool}(_))
+@
+
+and
+
+@
+\\and{_}(notBool(_), \\dv{Bool}(_))
+@
+-}
+matchUnifyBoolNot ::
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName ->
+    Maybe UnifyBoolNot
+matchUnifyBoolNot first second
+    | Just boolNot <- matchBoolNot first
+      , isFunctionPattern first
+      , Just value <- matchBool second =
+        Just $ UnifyBoolNot boolNot value
+    | otherwise = Nothing
+{-# INLINE matchUnifyBoolNot #-}
 
 unifyBoolNot ::
-    forall variable unifier.
-    InternalVariable variable =>
-    MonadUnify unifier =>
-    TermSimplifier variable unifier ->
-    TermLike variable ->
-    TermLike variable ->
-    MaybeT unifier (Pattern variable)
-unifyBoolNot unifyChildren a b =
-    worker a b <|> worker b a
+    forall unifier.
+    TermSimplifier RewritingVariableName unifier ->
+    TermLike RewritingVariableName ->
+    UnifyBoolNot ->
+    unifier (Pattern RewritingVariableName)
+unifyBoolNot unifyChildren term unifyData =
+    let notValue = asInternal (termLikeSort term) (not value)
+     in unifyChildren notValue operand
   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
+    UnifyBoolNot{boolNot, value} = unifyData
+    BoolNot{operand} = boolNot
 
 -- | Match a @BOOL.Bool@ builtin value.
 matchBool :: TermLike variable -> Maybe Bool
@@ -277,41 +358,41 @@ matchBool (InternalBool_ InternalBool{internalBoolValue}) =
 matchBool _ = Nothing
 
 -- | The @BOOL.and@ hooked symbol applied to @term@-type arguments.
-data BoolAnd term = BoolAnd
+data BoolAnd = BoolAnd
     { symbol :: !Symbol
-    , operand1, operand2 :: !term
+    , operand1, operand2 :: !(TermLike RewritingVariableName)
     }
 
 -- | Match the @BOOL.and@ hooked symbol.
-matchBoolAnd :: TermLike variable -> Maybe (BoolAnd (TermLike variable))
+matchBoolAnd :: TermLike RewritingVariableName -> Maybe BoolAnd
 matchBoolAnd (App_ symbol [operand1, operand2]) = do
     hook2 <- (getHook . symbolHook) symbol
     Monad.guard (hook2 == andKey)
     return BoolAnd{symbol, operand1, operand2}
 matchBoolAnd _ = Nothing
 
 -- | The @BOOL.or@ hooked symbol applied to @term@-type arguments.
-data BoolOr term = BoolOr
+data BoolOr = BoolOr
     { symbol :: !Symbol
-    , operand1, operand2 :: !term
+    , operand1, operand2 :: !(TermLike RewritingVariableName)
     }
 
 -- | Match the @BOOL.or@ hooked symbol.
-matchBoolOr :: TermLike variable -> Maybe (BoolOr (TermLike variable))
+matchBoolOr :: TermLike RewritingVariableName -> Maybe BoolOr
 matchBoolOr (App_ symbol [operand1, operand2]) = do
     hook2 <- (getHook . symbolHook) symbol
     Monad.guard (hook2 == orKey)
     return BoolOr{symbol, operand1, operand2}
 matchBoolOr _ = Nothing
 
 -- | The @BOOL.not@ hooked symbol applied to a @term@-type argument.
-data BoolNot term = BoolNot
+data BoolNot = BoolNot
     { symbol :: !Symbol
-    , operand :: !term
+    , operand :: !(TermLike RewritingVariableName)
     }
 
 -- | Match the @BOOL.not@ hooked symbol.
-matchBoolNot :: TermLike variable -> Maybe (BoolNot (TermLike variable))
+matchBoolNot :: TermLike RewritingVariableName -> Maybe BoolNot
 matchBoolNot (App_ symbol [operand]) = do
     hook2 <- (getHook . symbolHook) symbol
     Monad.guard (hook2 == notKey)