Merge branch 'master' into no-simplify-lhs

Author: emarzion

deps/k_release

@@ -1 +1 @@
-v5.0.0-7888200
+v5.0.0-6e054d6

docker/run.sh

@@ -1,3 +1,4 @@
 #!/usr/bin/env bash
 # Run command in Docker
-docker run --rm --mount src=$(pwd),target=/home/user/kore,type=bind --workdir=/home/user/kore kore "$@"
+# Usage: ./docker/run.sh make test
+docker run --rm --mount src=$(pwd),target=/home/user/kore,type=bind --workdir=/home/user/kore kore "$@"

kore/kore.cabal

@@ -4,7 +4,7 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: c7335f234ff802f2b2d42c8970fd41a6fa133676b9afa09d411e6222e1120d42
+-- hash: 999e1c394d84530678f479451e3ecface6622df87771c72c3aa313a406716b15
 
 name:           kore
 version:        0.39.0.0
@@ -376,7 +376,6 @@ library
       Kore.Unification.Procedure
       Kore.Unification.SubstitutionNormalization
       Kore.Unification.SubstitutionSimplifier
-      Kore.Unification.UnificationProcedure
       Kore.Unification.UnifierT
       Kore.Unification.Unify
       Kore.Unparser

kore/src/Kore/Equation/Registry.hs

@@ -51,6 +51,7 @@ import Kore.Syntax.Sentence
     ( SentenceAxiom (..)
     )
 import qualified Kore.Verified as Verified
+import qualified Pretty
 
 {- | Create a mapping from symbol identifiers to their defining axioms.
 
@@ -154,8 +155,13 @@ ignoreEquation Equation { attributes }
 {- | Should we ignore the 'EqualityRule' for evaluating function definitions?
  -}
 ignoreDefinition :: Equation VariableName -> Bool
-ignoreDefinition Equation { left } =
-    assert isLeftFunctionLike False
+ignoreDefinition Equation { attributes, left }
+    | isLeftFunctionLike = False
+    | otherwise = (error . show . Pretty.vsep)
+        [ "left-hand side of equation was not function-like at:"
+        , Pretty.indent 4 $ Pretty.pretty sourceLocation
+        ]
   where
+    Attribute.Axiom { sourceLocation } = attributes
     isLeftFunctionLike =
         (Pattern.isFunction . Pattern.function) (extractAttributes left)

kore/src/Kore/ModelChecker/Step.hs

@@ -63,7 +63,6 @@ import Kore.Syntax.Variable
     ( VariableName
     )
 import Kore.TopBottom
-import qualified Kore.Unification.Procedure as Unification
 import qualified Pretty
 
 data Prim patt rewrite =
@@ -212,8 +211,6 @@ transitionRule
     transitionComputeWeakNext _ (GoalRemLHS _)
       = return (GoalLHS Pattern.bottom)
 
-    unificationProcedure = Unification.unificationProcedure
-
     transitionComputeWeakNextHelper
         :: [RewriteRule VariableName]
         -> Pattern VariableName
@@ -223,7 +220,6 @@ transitionRule
     transitionComputeWeakNextHelper rules config = do
         results <-
             Step.applyRewriteRulesParallel
-                unificationProcedure
                 (mkRewritingRule <$> rules)
                 (mkRewritingPattern config)
             & lift . lift

kore/src/Kore/Reachability/Claim.hs

@@ -148,7 +148,6 @@ import Kore.Syntax.Variable
 import Kore.TopBottom
     ( TopBottom (..)
     )
-import qualified Kore.Unification.Procedure as Unification
 import Kore.Unparser
     ( Unparse (..)
     )
@@ -280,7 +279,6 @@ deriveSeqClaim lensClaimPattern mkClaim claims claim =
             results <-
                 Step.applyClaimsSequence
                     mkClaim
-                    Unification.unificationProcedure
                     config
                     (Lens.view lensClaimPattern <$> claims)
                     & lift
@@ -650,8 +648,7 @@ derivePar'
     -> claim
     -> Strategy.TransitionT (AppliedRule claim) m (ApplyResult claim)
 derivePar' lensRulePattern mkRule =
-    deriveWith lensRulePattern mkRule
-    $ Step.applyRewriteRulesParallel Unification.unificationProcedure
+    deriveWith lensRulePattern mkRule Step.applyRewriteRulesParallel
 
 type Deriver monad =
         [RewriteRule RewritingVariableName]
@@ -694,8 +691,7 @@ deriveSeq'
     -> claim
     -> Strategy.TransitionT (AppliedRule claim) m (ApplyResult claim)
 deriveSeq' lensRulePattern mkRule =
-    deriveWith lensRulePattern mkRule . flip
-    $ Step.applyRewriteRulesSequence Unification.unificationProcedure
+    deriveWith lensRulePattern mkRule $ flip Step.applyRewriteRulesSequence
 
 deriveResults
     :: Step.UnifyingRuleVariable representation ~ RewritingVariableName

kore/src/Kore/Repl.hs

@@ -88,7 +88,7 @@ import Prof
     )
 
 import Kore.Unification.Procedure
-    ( unificationProcedureWorker
+    ( unificationProcedure
     )
 import Kore.Unparser
     ( unparseToString
@@ -208,7 +208,7 @@ runRepl
     config =
         Config
             { stepper    = stepper0
-            , unifier    = unificationProcedureWorker
+            , unifier    = unificationProcedure
             , logger
             , outputFile
             , mainModuleName

kore/src/Kore/Step.hs

@@ -70,7 +70,6 @@ import Kore.Step.Strategy hiding
     ( transitionRule
     )
 import qualified Kore.Step.Strategy as Strategy
-import qualified Kore.Unification.Procedure as Unification
 
 {- | The program's state during symbolic execution.
 -}
@@ -192,7 +191,6 @@ transitionRule rewriteGroups = transitionRuleWorker
         transitionRewrite' applied rewrites
           | Just config' <- retractRemaining applied =
             Step.applyRewriteRulesParallel
-                Unification.unificationProcedure
                 rewrites
                 config'
                 & lift
@@ -207,7 +205,6 @@ transitionRule rewriteGroups = transitionRuleWorker
         let rules = concat rewriteGroups
         results <-
             Step.applyRewriteRulesSequence
-                Unification.unificationProcedure
                 config
                 rules
         deriveResults results

kore/src/Kore/Step/RewriteStep.hs

@@ -68,7 +68,6 @@ import Kore.Step.Simplification.Simplify
 import Kore.Step.Step
     ( Result
     , Results
-    , UnificationProcedure (..)
     , UnifiedRule
     , applyInitialConditions
     , applyRemainder
@@ -284,14 +283,13 @@ applyWithFinalizer
     => Rule.UnifyingRuleVariable rule ~ RewritingVariableName
     => From rule SourceLocation
     => Finalizer rule simplifier
-    -> UnificationProcedure simplifier
     -> [rule]
     -- ^ Rewrite rules
     -> Pattern RewritingVariableName
     -- ^ Configuration being rewritten
     -> simplifier (Results rule)
-applyWithFinalizer finalize unificationProcedure rules initial = do
-    results <- unifyRules unificationProcedure initial rules
+applyWithFinalizer finalize rules initial = do
+    results <- unifyRules initial rules
     debugAppliedRewriteRules initial (locations <$> results)
     let initialVariables = freeVariables initial
     finalize initialVariables initial results
@@ -307,8 +305,7 @@ See also: 'applyRewriteRule'
 applyRulesParallel
     :: forall simplifier
     .  MonadSimplify simplifier
-    => UnificationProcedure simplifier
-    -> [RulePattern RewritingVariableName]
+    => [RulePattern RewritingVariableName]
     -- ^ Rewrite rules
     -> Pattern RewritingVariableName
     -- ^ Configuration being rewritten
@@ -323,18 +320,16 @@ See also: 'applyRewriteRule'
 applyRewriteRulesParallel
     :: forall simplifier
     .  MonadSimplify simplifier
-    => UnificationProcedure simplifier
-    -> [RewriteRule RewritingVariableName]
+    => [RewriteRule RewritingVariableName]
     -- ^ Rewrite rules
     -> Pattern RewritingVariableName
     -- ^ Configuration being rewritten
     -> simplifier (Results (RulePattern RewritingVariableName))
 applyRewriteRulesParallel
-    unificationProcedure
     (map getRewriteRule -> rules)
     initial
   = do
-    results <- applyRulesParallel unificationProcedure rules initial
+    results <- applyRulesParallel rules initial
     assertFunctionLikeResults (term initial) results
     return results
 
@@ -347,8 +342,7 @@ See also: 'applyRewriteRule'
 applyRulesSequence
     :: forall simplifier
     .  MonadSimplify simplifier
-    => UnificationProcedure simplifier
-    -> [RulePattern RewritingVariableName]
+    => [RulePattern RewritingVariableName]
     -- ^ Rewrite rules
     -> Pattern RewritingVariableName
     -- ^ Configuration being rewritten
@@ -363,18 +357,16 @@ See also: 'applyRewriteRulesParallel'
 applyRewriteRulesSequence
     :: forall simplifier
     .  MonadSimplify simplifier
-    => UnificationProcedure simplifier
-    -> Pattern RewritingVariableName
+    => Pattern RewritingVariableName
     -- ^ Configuration being rewritten
     -> [RewriteRule RewritingVariableName]
     -- ^ Rewrite rules
     -> simplifier (Results (RulePattern RewritingVariableName))
 applyRewriteRulesSequence
-    unificationProcedure
     initialConfig
     (map getRewriteRule -> rules)
   = do
-    results <- applyRulesSequence unificationProcedure rules initialConfig
+    results <- applyRulesSequence rules initialConfig
     assertFunctionLikeResults (term initialConfig) results
     return results
 
@@ -383,17 +375,15 @@ applyClaimsSequence
     .  MonadSimplify simplifier
     => UnifyingRuleWithRepresentation ClaimPattern goal
     => (ClaimPattern -> goal)
-    -> UnificationProcedure simplifier
     -> Pattern RewritingVariableName
     -- ^ Configuration being rewritten
     -> [ClaimPattern]
     -- ^ Rewrite rules
     -> simplifier (Results ClaimPattern)
-applyClaimsSequence mkClaim unificationProcedure initialConfig claims = do
+applyClaimsSequence mkClaim initialConfig claims = do
     results <-
         applyWithFinalizer
             (finalizeSequence mkClaim finalizeAppliedClaim)
-            unificationProcedure
             claims
             initialConfig
     assertFunctionLikeResults (term initialConfig) results

kore/src/Kore/Step/Search.hs

@@ -55,7 +55,7 @@ import Kore.Step.Substitution
     )
 import Kore.TopBottom
 import Kore.Unification.Procedure
-    ( unificationProcedureWorker
+    ( unificationProcedure
     )
 import qualified Kore.Unification.UnifierT as Unifier
 import Logic
@@ -133,7 +133,7 @@ matchWith
 matchWith sideCondition e1 e2 = do
     unifiers <-
         lift $ Unifier.runUnifierT Not.notSimplifier
-        $ unificationProcedureWorker sideCondition t1 t2
+        $ unificationProcedure sideCondition t1 t2
     let
         mergeAndEvaluate
             :: Condition variable