Remove a few unused definitions (#3159)

* Remove a few unused definitions

* liftConditionSimplifier is dead code
* simplifyRewriteRule is dead code
* TestSimplifier is dead code
* simplifyRulePattern is used in tests but not the app
* simplifyPatternId is a no-op wrapper around fromPattern

* Apply suggestions from code review

* Format with fourmolu

Co-authored-by: ana-pantilie <45069775+ana-pantilie@users.noreply.github.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>

Author: 4 people

kore/src/Kore/Rewrite/Rule/Simplify.hs

@@ -5,8 +5,6 @@ License     : BSD-3-Clause
 module Kore.Rewrite.Rule.Simplify (
     SimplifyRuleLHS (..),
     simplifyClaimPattern,
-    simplifyRewriteRule,
-    simplifyRulePattern,
 ) where
 
 import Kore.Internal.Condition qualified as Condition
@@ -26,7 +24,6 @@ import Kore.Internal.Predicate (
     makeAndPredicate,
     pattern PredicateTrue,
  )
-import Kore.Internal.Predicate qualified as Predicate
 import Kore.Internal.SideCondition qualified as SideCondition
 import Kore.Internal.Substitution qualified as Substitution
 import Kore.Internal.TermLike as TermLike
@@ -35,7 +32,6 @@ import Kore.Reachability (
     OnePathClaim (..),
     SomeClaim (..),
  )
-import Kore.Rewrite.AntiLeft qualified as AntiLeft
 import Kore.Rewrite.ClaimPattern (
     ClaimPattern (..),
  )
@@ -47,11 +43,9 @@ import Kore.Rewrite.RulePattern (
     RewriteRule (..),
     RulePattern (RulePattern),
  )
-import Kore.Rewrite.RulePattern qualified as OLD
 import Kore.Rewrite.RulePattern qualified as RulePattern (
     RulePattern (..),
     applySubstitution,
-    rhsForgetSimplified,
  )
 import Kore.Rewrite.SMT.Evaluator qualified as SMT.Evaluator
 import Kore.Simplify.Pattern qualified as Pattern
@@ -153,62 +147,6 @@ simplifyClaimRule claimPattern = fmap MultiAnd.make $
             Just False -> empty
             _ -> return conditional
 
-{- | Simplify a 'Rule' using only matching logic rules.
-
-See also: 'simplifyRulePattern'
--}
-simplifyRewriteRule ::
-    MonadSimplify simplifier =>
-    RewriteRule RewritingVariableName ->
-    simplifier (RewriteRule RewritingVariableName)
-simplifyRewriteRule (RewriteRule rule) =
-    RewriteRule <$> simplifyRulePattern rule
-
-{- | Simplify a 'RulePattern' using only matching logic rules.
-
-The original rule is returned unless the simplification result matches certain
-narrowly-defined criteria.
--}
-simplifyRulePattern ::
-    MonadSimplify simplifier =>
-    RulePattern RewritingVariableName ->
-    simplifier (RulePattern RewritingVariableName)
-simplifyRulePattern rule = do
-    let RulePattern{left} = rule
-    simplifiedLeft <- simplifyPattern' left
-    case OrPattern.toPatterns simplifiedLeft of
-        [Conditional{term, predicate, substitution}]
-            | PredicateTrue <- predicate -> do
-                -- TODO (virgil): Dropping the substitution for equations
-                -- and for rewrite rules where the substituted variables occur
-                -- in the RHS is wrong because those variables are not
-                -- existentially quantified.
-                let subst = Substitution.toMap substitution
-                    left' = substitute subst term
-                    antiLeft' = substitute subst <$> antiLeft
-                      where
-                        RulePattern{antiLeft} = rule
-                    requires' = substitute subst requires
-                      where
-                        RulePattern{requires} = rule
-                    rhs' = substitute subst rhs
-                      where
-                        RulePattern{rhs} = rule
-                    RulePattern{attributes} = rule
-                return
-                    RulePattern
-                        { left = TermLike.forgetSimplified left'
-                        , antiLeft = AntiLeft.forgetSimplified <$> antiLeft'
-                        , requires = Predicate.forgetSimplified requires'
-                        , rhs = RulePattern.rhsForgetSimplified rhs'
-                        , attributes = attributes
-                        }
-        _ ->
-            -- Unable to simplify the given rule pattern, so we return the
-            -- original pattern in the hope that we can do something with it
-            -- later.
-            return rule
-
 {- | Simplify a 'ClaimPattern' using only matching logic rules.
 
 The original rule is returned unless the simplification result matches certain

kore/src/Kore/Simplify/Simplify.hs

@@ -11,7 +11,6 @@ module Kore.Simplify.Simplify (
     -- * Condition simplifiers
     ConditionSimplifier (..),
     emptyConditionSimplifier,
-    liftConditionSimplifier,
 
     -- * Builtin and axiom simplifiers
     SimplifierCache (attemptedEquationsCache),
@@ -54,13 +53,9 @@ module Kore.Simplify.Simplify (
 
 import Control.Monad qualified as Monad
 import Control.Monad.Counter
-import Control.Monad.Morph (
-    MFunctor,
- )
+import Control.Monad.Morph (MFunctor)
 import Control.Monad.Morph qualified as Monad.Morph
-import Control.Monad.RWS.Strict (
-    RWST,
- )
+import Control.Monad.RWS.Strict (RWST)
 import Control.Monad.State.Strict qualified as Strict
 import Control.Monad.Trans.Accum
 import Control.Monad.Trans.Except
@@ -71,41 +66,25 @@ import Data.Functor.Foldable qualified as Recursive
 import Data.HashMap.Strict (HashMap)
 import Data.HashMap.Strict qualified as HashMap
 import Data.Map.Strict qualified as Map
-import Data.Text (
-    Text,
- )
+import Data.Text (Text)
 import GHC.Generics qualified as GHC
 import Generics.SOP qualified as SOP
 import Kore.Attribute.Symbol qualified as Attribute
 import Kore.Debug
 import Kore.Equation.DebugEquation (AttemptEquationError)
 import Kore.Equation.Equation (Equation)
-import Kore.IndexedModule.MetadataTools (
-    SmtMetadataTools,
- )
+import Kore.IndexedModule.MetadataTools (SmtMetadataTools)
 import Kore.Internal.Condition qualified as Condition
-import Kore.Internal.Conditional (
-    Conditional,
- )
+import Kore.Internal.Conditional (Conditional)
 import Kore.Internal.MultiOr qualified as MultiOr
-import Kore.Internal.OrCondition (
-    OrCondition,
- )
+import Kore.Internal.OrCondition (OrCondition)
 import Kore.Internal.OrCondition qualified as OrCondition
-import Kore.Internal.OrPattern (
-    OrPattern,
-    fromPattern,
- )
+import Kore.Internal.OrPattern (OrPattern, fromPattern)
 import Kore.Internal.OrPattern qualified as OrPattern
-import Kore.Internal.Pattern (
-    Pattern,
- )
+import Kore.Internal.Pattern (Pattern)
 import Kore.Internal.Pattern qualified as Pattern
 import Kore.Internal.Predicate qualified as Predicate
-import Kore.Internal.SideCondition (
-    SideCondition,
-    toRepresentation,
- )
+import Kore.Internal.SideCondition (SideCondition, toRepresentation)
 import Kore.Internal.SideCondition.SideCondition qualified as SideCondition (
     Representation,
  )
@@ -117,38 +96,22 @@ import Kore.Internal.TermLike (
     TermLikeF (..),
     pattern App_,
  )
-import Kore.Internal.Variable (
-    InternalVariable,
- )
-import Kore.Log.WarnFunctionWithoutEvaluators (
-    warnFunctionWithoutEvaluators,
- )
-import Kore.Rewrite.Axiom.Identifier (
-    AxiomIdentifier (..),
- )
+import Kore.Internal.Variable (InternalVariable)
+import Kore.Log.WarnFunctionWithoutEvaluators (warnFunctionWithoutEvaluators)
+import Kore.Rewrite.Axiom.Identifier (AxiomIdentifier (..))
 import Kore.Rewrite.Axiom.Identifier qualified as Axiom.Identifier
 import Kore.Rewrite.Function.Memo qualified as Memo
-import Kore.Rewrite.RewritingVariable (
-    RewritingVariableName,
- )
-import Kore.Simplify.InjSimplifier (
-    InjSimplifier,
- )
-import Kore.Simplify.OverloadSimplifier (
-    OverloadSimplifier (..),
- )
+import Kore.Rewrite.RewritingVariable (RewritingVariableName)
+import Kore.Simplify.InjSimplifier (InjSimplifier)
+import Kore.Simplify.OverloadSimplifier (OverloadSimplifier (..))
 import Kore.Syntax.Application
 import Kore.Unparser
 import Log
 import Logic
 import Prelude.Kore
-import Pretty (
-    (<+>),
- )
+import Pretty ((<+>))
 import Pretty qualified
-import SMT (
-    MonadSMT (..),
- )
+import SMT (MonadSMT (..))
 
 type TermSimplifier variable m =
     TermLike variable -> TermLike variable -> m (Pattern variable)
@@ -343,16 +306,6 @@ emptyConditionSimplifier :: ConditionSimplifier monad
 emptyConditionSimplifier =
     ConditionSimplifier (\_ predicate -> return predicate)
 
-liftConditionSimplifier ::
-    (Monad monad, MonadTrans trans, Monad (trans monad)) =>
-    ConditionSimplifier monad ->
-    ConditionSimplifier (trans monad)
-liftConditionSimplifier (ConditionSimplifier simplifier) =
-    ConditionSimplifier $ \sideCondition predicate -> do
-        results <-
-            lift . lift $
-                observeAllT $ simplifier sideCondition predicate
-        scatter results
 -- * Builtin and axiom simplifiers
 
 {- | Used for keeping track of already attempted equations which failed to