:refactor: change Evaluate.hs to EvaluateSym.hs

lsrcz · Oct 25, 2023 · 22621aa · 22621aa
1 parent e22884f
commit 22621aa
Show file tree

Hide file tree

Showing 14 changed files with 18 additions and 18 deletions.
diff --git a/grisette.cabal b/grisette.cabal
@@ -61,7 +61,7 @@ library
       Grisette.Core.Data.Class.BitVector
       Grisette.Core.Data.Class.CEGISSolver
       Grisette.Core.Data.Class.Error
-      Grisette.Core.Data.Class.Evaluate
+      Grisette.Core.Data.Class.EvaluateSym
       Grisette.Core.Data.Class.ExtractSymbolics
       Grisette.Core.Data.Class.Function
       Grisette.Core.Data.Class.GenSym

diff --git a/src/Grisette/Backend/SBV/Data/SMT/Solving.hs b/src/Grisette/Backend/SBV/Data/SMT/Solving.hs
@@ -60,7 +60,7 @@ import Grisette.Core.Data.Class.CEGISSolver
   ( CEGISCondition (CEGISCondition),
     CEGISSolver (cegisMultiInputs),
   )
-import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))
+import Grisette.Core.Data.Class.EvaluateSym (EvaluateSym (evaluateSym))
 import Grisette.Core.Data.Class.ExtractSymbolics
   ( ExtractSymbolics (extractSymbolics),
   )

diff --git a/src/Grisette/Core.hs b/src/Grisette/Core.hs
@@ -1057,7 +1057,6 @@ import Grisette.Core.Data.Class.BitVector
     bvExtract,
     sizedBVExtract,
   )
-import Grisette.Core.Data.Class.SEq (SEq (..))
 import Grisette.Core.Data.Class.CEGISSolver
   ( CEGISCondition (..),
     CEGISSolver (..),
@@ -1077,7 +1076,7 @@ import Grisette.Core.Data.Class.Error
     symAssertWith,
     symThrowTransformableError,
   )
-import Grisette.Core.Data.Class.Evaluate
+import Grisette.Core.Data.Class.EvaluateSym
   ( EvaluateSym (..),
     evaluateSymToCon,
   )
@@ -1141,6 +1140,7 @@ import Grisette.Core.Data.Class.ModelOps
     SymbolSetOps (..),
     SymbolSetRep (..),
   )
+import Grisette.Core.Data.Class.SEq (SEq (..))
 import Grisette.Core.Data.Class.SOrd (SOrd (..))
 import Grisette.Core.Data.Class.SafeArith
   ( SafeDivision (..),

diff --git a/src/Grisette/Core/Control/Exception.hs b/src/Grisette/Core/Control/Exception.hs
@@ -35,7 +35,7 @@ import Grisette.Core.Data.Class.Error
   ( TransformError (transformError),
     symAssertTransformableError,
   )
-import Grisette.Core.Data.Class.Evaluate (EvaluateSym)
+import Grisette.Core.Data.Class.EvaluateSym (EvaluateSym)
 import Grisette.Core.Data.Class.ExtractSymbolics
   ( ExtractSymbolics,
   )

diff --git a/src/Grisette/Core/Control/Monad/CBMCExcept.hs b/src/Grisette/Core/Control/Monad/CBMCExcept.hs
@@ -64,8 +64,7 @@ import Data.Functor.Classes
 import Data.Functor.Contravariant (Contravariant (contramap))
 import Data.Hashable (Hashable)
 import GHC.Generics (Generic, Generic1)
-import Grisette.Core.Data.Class.SEq (SEq ((==~)))
-import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))
+import Grisette.Core.Data.Class.EvaluateSym (EvaluateSym (evaluateSym))
 import Grisette.Core.Data.Class.ExtractSymbolics
   ( ExtractSymbolics (extractSymbolics),
   )
@@ -82,6 +81,7 @@ import Grisette.Core.Data.Class.Mergeable
     rootStrategy1,
     wrapStrategy,
   )
+import Grisette.Core.Data.Class.SEq (SEq ((==~)))
 import Grisette.Core.Data.Class.SOrd (SOrd (symCompare, (<=~), (<~), (>=~), (>~)))
 import Grisette.Core.Data.Class.SimpleMergeable
   ( SimpleMergeable (mrgIte),

diff --git a/src/Grisette/Core/Control/Monad/UnionM.hs b/src/Grisette/Core/Control/Monad/UnionM.hs
@@ -58,8 +58,7 @@ import Grisette.Core.Control.Monad.Class.MonadParallelUnion
   )
 import Grisette.Core.Control.Monad.Union (MonadUnion)
 import Grisette.Core.Data.BV (IntN, WordN)
-import Grisette.Core.Data.Class.SEq (SEq ((==~)))
-import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))
+import Grisette.Core.Data.Class.EvaluateSym (EvaluateSym (evaluateSym))
 import Grisette.Core.Data.Class.ExtractSymbolics
   ( ExtractSymbolics (extractSymbolics),
   )
@@ -81,6 +80,7 @@ import Grisette.Core.Data.Class.Mergeable
     Mergeable1 (liftRootStrategy),
     MergingStrategy (SimpleStrategy),
   )
+import Grisette.Core.Data.Class.SEq (SEq ((==~)))
 import Grisette.Core.Data.Class.SOrd
   ( SOrd (symCompare, (<=~), (<~), (>=~), (>~)),
   )

diff --git a/src/Grisette/Core/Data/Class/CEGISSolver.hs b/src/Grisette/Core/Data/Class/CEGISSolver.hs
@@ -44,7 +44,7 @@ import Generics.Deriving (Default (Default))
 import Grisette.Core.Control.Exception
   ( VerificationConditions (AssertionViolation, AssumptionViolation),
   )
-import Grisette.Core.Data.Class.Evaluate (EvaluateSym)
+import Grisette.Core.Data.Class.EvaluateSym (EvaluateSym)
 import Grisette.Core.Data.Class.ExtractSymbolics
   ( ExtractSymbolics,
   )

diff --git a/src/Grisette/Core/Data/Class/Evaluate.hs → src/Grisette/Core/Data/Class/EvaluateSym.hs b/src/Grisette/Core/Data/Class/Evaluate.hs → src/Grisette/Core/Data/Class/EvaluateSym.hs
@@ -11,14 +11,14 @@
 {-# LANGUAGE UndecidableInstances #-}
 
 -- |
--- Module      :   Grisette.Core.Data.Class.Evaluate
+-- Module      :   Grisette.Core.Data.Class.EvaluateSym
 -- Copyright   :   (c) Sirui Lu 2021-2023
 -- License     :   BSD-3-Clause (see the LICENSE file)
 --
 -- Maintainer  :   siruilu@cs.washington.edu
 -- Stability   :   Experimental
 -- Portability :   GHC only
-module Grisette.Core.Data.Class.Evaluate
+module Grisette.Core.Data.Class.EvaluateSym
   ( -- * Evaluating symbolic values with model
     EvaluateSym (..),
     evaluateSymToCon,

diff --git a/test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs b/test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs
@@ -28,7 +28,7 @@ import Grisette.Core.Data.Class.CEGISSolver
     cegisExceptVC,
     cegisPostCond,
   )
-import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))
+import Grisette.Core.Data.Class.EvaluateSym (EvaluateSym (evaluateSym))
 import Grisette.Core.Data.Class.ExtractSymbolics
   ( ExtractSymbolics,
   )

diff --git a/test/Grisette/Core/Control/ExceptionTests.hs b/test/Grisette/Core/Control/ExceptionTests.hs
@@ -16,7 +16,7 @@ import Grisette.Core.Control.Monad.UnionM (UnionM)
 import Grisette.Core.Data.Class.Error
   ( TransformError (transformError),
   )
-import Grisette.Core.Data.Class.Evaluate
+import Grisette.Core.Data.Class.EvaluateSym
   ( EvaluateSym (evaluateSym),
   )
 import Grisette.Core.Data.Class.ExtractSymbolics

diff --git a/test/Grisette/Core/Control/Monad/UnionMTests.hs b/test/Grisette/Core/Control/Monad/UnionMTests.hs
@@ -13,7 +13,7 @@ import Grisette.Core.Control.Monad.UnionM
     underlyingUnion,
     unionSize,
   )
-import Grisette.Core.Data.Class.Evaluate
+import Grisette.Core.Data.Class.EvaluateSym
   ( EvaluateSym (evaluateSym),
   )
 import Grisette.Core.Data.Class.ExtractSymbolics

diff --git a/test/Grisette/Core/Data/Class/EvaluateSymTests.hs b/test/Grisette/Core/Data/Class/EvaluateSymTests.hs
@@ -19,7 +19,7 @@ import Data.Int (Int16, Int32, Int64, Int8)
 import Data.Word (Word16, Word32, Word64, Word8)
 import GHC.Stack (HasCallStack)
 import Grisette (TypedSymbol (IndexedSymbol))
-import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))
+import Grisette.Core.Data.Class.EvaluateSym (EvaluateSym (evaluateSym))
 import Grisette.Core.Data.Class.ITEOp (ITEOp (ites))
 import Grisette.Core.Data.Class.LogicalOp (LogicalOp (nots, (&&~), (||~)))
 import Grisette.Core.Data.Class.ModelOps

diff --git a/test/Grisette/IR/SymPrim/Data/SymPrimTests.hs b/test/Grisette/IR/SymPrim/Data/SymPrimTests.hs
@@ -48,7 +48,7 @@ import Grisette.Core.Data.Class.BitVector
         sizedBVZext
       ),
   )
-import Grisette.Core.Data.Class.Evaluate
+import Grisette.Core.Data.Class.EvaluateSym
   ( EvaluateSym (evaluateSym),
   )
 import Grisette.Core.Data.Class.ExtractSymbolics

diff --git a/test/Grisette/TestUtil/SymbolicAssertion.hs b/test/Grisette/TestUtil/SymbolicAssertion.hs
@@ -3,7 +3,7 @@ module Grisette.TestUtil.SymbolicAssertion ((@?=~)) where
 import GHC.Stack (HasCallStack)
 import Grisette.Backend.SBV (z3)
 import Grisette.Backend.SBV.Data.SMT.Solving (SolvingFailure (Unsat), precise)
-import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))
+import Grisette.Core.Data.Class.EvaluateSym (EvaluateSym (evaluateSym))
 import Grisette.Core.Data.Class.LogicalOp (LogicalOp (nots))
 import Grisette.Core.Data.Class.SEq (SEq ((==~)))
 import Grisette.Core.Data.Class.Solver (Solver (solve))