Add liftSimplifier and perform a little restructuring of the codebase (#3171)

* Add liftSimplifier & put MonadSimplify and Simplifier together

* Fix the definitions in the test suite and hide runSimplifier

* Moved certain functions outside MonadSimplify, killed TestSimplifierT

* Rename 'Data' to 'API', 'runSimplifier' to 'testRunSimplifier'

* Materialize Nix expressions

Co-authored-by: github-actions <github-actions@github.com>

Author: breakerzirconia

kore/kore.cabal

@@ -457,12 +457,12 @@ library
     Kore.Simplify.And
     Kore.Simplify.AndPredicates
     Kore.Simplify.AndTerms
+    Kore.Simplify.API
     Kore.Simplify.Application
     Kore.Simplify.Bottom
     Kore.Simplify.Ceil
     Kore.Simplify.CeilSimplifier
     Kore.Simplify.Condition
-    Kore.Simplify.Data
     Kore.Simplify.DomainValue
     Kore.Simplify.Equals
     Kore.Simplify.Exists

kore/src/Kore/Exec.hs

@@ -174,12 +174,12 @@ import Kore.Rewrite.Transition (
     runTransitionT,
     scatter,
  )
-import Kore.Simplify.Data (
+import Kore.Simplify.API (
     Simplifier,
     evalSimplifier,
     evalSimplifierProofs,
  )
-import Kore.Simplify.Data qualified as Simplifier
+import Kore.Simplify.API qualified as Simplifier
 import Kore.Simplify.Pattern qualified as Pattern
 import Kore.Simplify.Simplify (
     SimplifierXSwitch,

kore/src/Kore/JsonRpc.hs

@@ -39,7 +39,7 @@ import Kore.Rewrite (ExecutionMode (All), Natural)
 -- import Kore.Rewrite.RewritingVariable as RewritingVariable
 import Kore.Simplify.Simplify (SimplifierXSwitch)
 
--- import Kore.Simplify.Data (
+-- import Kore.Simplify.API (
 --     evalSimplifier,
 --  )
 import Kore.Syntax.Json (KoreJson)

kore/src/Kore/Reachability/Claim.hs

@@ -137,7 +137,7 @@ import Kore.Rewrite.Strategy (
  )
 import Kore.Rewrite.Strategy qualified as Strategy
 import Kore.Rewrite.Transition qualified as Transition
-import Kore.Simplify.Data (
+import Kore.Simplify.API (
     MonadSimplify,
  )
 import Kore.Simplify.Exists qualified as Exists

kore/src/Kore/Repl.hs

@@ -65,7 +65,7 @@ import Kore.Repl.Interpreter
 import Kore.Repl.Parser
 import Kore.Repl.State
 import Kore.Rewrite.Strategy qualified as Strategy
-import Kore.Simplify.Data (
+import Kore.Simplify.API (
     Simplifier,
  )
 import Kore.Syntax.Module (

kore/src/Kore/Repl/Data.hs

@@ -94,7 +94,7 @@ import Kore.Rewrite.RewritingVariable (
     RewritingVariableName,
  )
 import Kore.Rewrite.Strategy qualified as Strategy
-import Kore.Simplify.Data (
+import Kore.Simplify.API (
     Simplifier,
  )
 import Kore.Simplify.Not qualified as Not

kore/src/Kore/Repl/Interpreter.hs

@@ -181,7 +181,7 @@ import Kore.Rewrite.RewritingVariable (
  )
 import Kore.Rewrite.RulePattern qualified as RulePattern
 import Kore.Rewrite.Strategy qualified as Strategy
-import Kore.Simplify.Data (
+import Kore.Simplify.API (
     Simplifier,
  )
 import Kore.Syntax.Application

kore/src/Kore/Repl/State.hs

@@ -145,7 +145,7 @@ import Kore.Rewrite.RewritingVariable (
     RewritingVariableName,
  )
 import Kore.Rewrite.Strategy qualified as Strategy
-import Kore.Simplify.Data (
+import Kore.Simplify.API (
     Simplifier,
  )
 import Kore.Syntax.Definition (

kore/src/Kore/Simplify/Data.hs kore/src/Kore/Simplify/API.hskore/src/Kore/Simplify/Data.hs renamed to kore/src/Kore/Simplify/API.hs

@@ -1,36 +1,39 @@
 {-# LANGUAGE UndecidableInstances #-}
 
 {- |
-Module      : Kore.Simplify.Data
+Module      : Kore.Simplify.API
 Description : Data structures used for term simplification.
 Copyright   : (c) Runtime Verification, 2018-2021
 License     : BSD-3-Clause
 Maintainer  : virgil.serbanuta@runtimeverification.com
 Stability   : experimental
 Portability : portable
 -}
-module Kore.Simplify.Data (
-    Simplifier,
-    TermSimplifier,
-    Env (..),
-    runSimplifier,
-    runSimplifierBranch,
+module Kore.Simplify.API (
     evalSimplifier,
     evalSimplifierProofs,
 
     -- * Re-exports
+    Env (..),
+    Simplifier,
+    runSimplifier,
+    runSimplifierBranch,
+    TermSimplifier,
     MonadSimplify (..),
+    askMetadataTools,
+    simplifyPattern,
+    simplifyTerm,
+    askSimplifierAxioms,
+    askInjSimplifier,
+    askOverloadSimplifier,
+    getCache,
+    putCache,
+    askSimplifierXSwitch,
     InternalVariable,
     MonadProf,
 ) where
 
-import Control.Monad.Catch (
-    MonadCatch,
-    MonadMask,
-    MonadThrow,
- )
 import Control.Monad.Reader
-import Control.Monad.State.Strict
 import Data.Map.Strict (
     Map,
  )
@@ -82,40 +85,13 @@ import Kore.Simplify.TermLike qualified as TermLike
 import Kore.Syntax.Variable (
     VariableName,
  )
-import Logic
 import Prelude.Kore
 import Pretty qualified
 import Prof
 import SMT (
     SMT,
  )
 
--- * Simplifier
-
-data Env = Env
-    { metadataTools :: !(SmtMetadataTools Attribute.Symbol)
-    , simplifierCondition :: !(ConditionSimplifier Simplifier)
-    , simplifierAxioms :: !BuiltinAndAxiomSimplifierMap
-    , memo :: !(Memo.Self Simplifier)
-    , injSimplifier :: !InjSimplifier
-    , overloadSimplifier :: !OverloadSimplifier
-    , simplifierXSwitch :: !SimplifierXSwitch
-    }
-
-{- | @Simplifier@ represents a simplification action.
-
-A @Simplifier@ can send constraints to the SMT solver through 'MonadSMT'.
-
-A @Simplifier@ can write to the log through 'HasLog'.
--}
-newtype Simplifier a
-    = Simplifier (StateT SimplifierCache (ReaderT Env SMT) a)
-    deriving newtype (Functor, Applicative, Monad)
-    deriving newtype (MonadSMT, MonadLog, MonadProf)
-    deriving newtype (MonadIO, MonadCatch, MonadThrow, MonadMask)
-    deriving newtype (MonadReader Env)
-    deriving newtype (MonadState SimplifierCache)
-
 traceProfSimplify ::
     MonadProf prof =>
     Pattern RewritingVariableName ->
@@ -131,66 +107,6 @@ traceProfSimplify (Pattern.toTermLike -> termLike) =
             . Pretty.pretty
             <$> matchAxiomIdentifier termLike
 
-instance MonadSimplify Simplifier where
-    askMetadataTools = asks metadataTools
-    {-# INLINE askMetadataTools #-}
-
-    simplifyPattern sideCondition patt =
-        traceProfSimplify patt (Pattern.makeEvaluate sideCondition patt)
-    {-# INLINE simplifyPattern #-}
-
-    simplifyTerm = TermLike.simplify
-    {-# INLINE simplifyTerm #-}
-
-    simplifyCondition topCondition conditional = do
-        ConditionSimplifier simplify <- asks simplifierCondition
-        simplify topCondition conditional
-    {-# INLINE simplifyCondition #-}
-
-    askSimplifierAxioms = asks simplifierAxioms
-    {-# INLINE askSimplifierAxioms #-}
-
-    localSimplifierAxioms locally =
-        local $ \env@Env{simplifierAxioms} ->
-            env{simplifierAxioms = locally simplifierAxioms}
-    {-# INLINE localSimplifierAxioms #-}
-
-    askMemo = asks memo
-    {-# INLINE askMemo #-}
-
-    askInjSimplifier = asks injSimplifier
-    {-# INLINE askInjSimplifier #-}
-
-    askOverloadSimplifier = asks overloadSimplifier
-    {-# INLINE askOverloadSimplifier #-}
-
-    getCache = get
-    {-# INLINE getCache #-}
-
-    putCache = put
-    {-# INLINE putCache #-}
-
-    askSimplifierXSwitch = asks simplifierXSwitch
-    {-# INLINE askSimplifierXSwitch #-}
-
--- | Run a simplification, returning the results along all branches.
-runSimplifierBranch ::
-    Env ->
-    -- | simplifier computation
-    LogicT Simplifier a ->
-    SMT [a]
-runSimplifierBranch env = runSimplifier env . observeAllT
-
-{- | Run a simplification, returning the result of only one branch.
-
-__Warning__: @runSimplifier@ calls 'error' if the 'Simplifier' does not contain
-exactly one branch. Use 'evalSimplifierBranch' to evaluation simplifications
-that may branch.
--}
-runSimplifier :: Env -> Simplifier a -> SMT a
-runSimplifier env (Simplifier simplifier) =
-    runReaderT (evalStateT simplifier initCache) env
-
 mkSimplifierEnv ::
     SimplifierXSwitch ->
     VerifiedModuleSyntax Attribute.Symbol ->
@@ -207,6 +123,8 @@ mkSimplifierEnv simplifierXSwitch verifiedModule sortGraph overloadGraph metadat
         Env
             { metadataTools = metadataTools
             , simplifierCondition
+            , simplifierPattern
+            , simplifierTerm
             , simplifierAxioms = earlySimplifierAxioms
             , memo = Memo.forgetful
             , injSimplifier
@@ -222,6 +140,12 @@ mkSimplifierEnv simplifierXSwitch verifiedModule sortGraph overloadGraph metadat
     simplifierCondition =
         {-# SCC "evalSimplifier/simplifierCondition" #-}
         Condition.create substitutionSimplifier
+    simplifierPattern sideCondition patt =
+        {-# SCC "evalSimplifier/simplifierPattern" #-}
+        traceProfSimplify patt (Pattern.makeEvaluate sideCondition patt)
+    simplifierTerm =
+        {-# SCC "evalSimplifier/simplifierTerm" #-}
+        TermLike.simplify
     -- Initialize without any builtin or axiom simplifiers.
     earlySimplifierAxioms = Map.empty
 
@@ -259,6 +183,8 @@ mkSimplifierEnv simplifierXSwitch verifiedModule sortGraph overloadGraph metadat
             Env
                 { metadataTools
                 , simplifierCondition
+                , simplifierPattern
+                , simplifierTerm
                 , simplifierAxioms
                 , memo
                 , injSimplifier

kore/src/Kore/Simplify/Overloading.hs

@@ -49,6 +49,7 @@ import Kore.Rewrite.RewritingVariable (
 import Kore.Simplify.OverloadSimplifier
 import Kore.Simplify.Simplify as Simplifier (
     MonadSimplify (..),
+    askOverloadSimplifier,
  )
 import Pair
 import Prelude.Kore hiding (