From 22621aae30b741f0994affdc9d1195560b2b28d0 Mon Sep 17 00:00:00 2001
From: Sirui Lu <siruilu@cs.washington.edu>
Date: Tue, 24 Oct 2023 20:08:47 -0700
Subject: [PATCH] :refactor: change Evaluate.hs to EvaluateSym.hs

---
 grisette.cabal                                               | 2 +-
 src/Grisette/Backend/SBV/Data/SMT/Solving.hs                 | 2 +-
 src/Grisette/Core.hs                                         | 4 ++--
 src/Grisette/Core/Control/Exception.hs                       | 2 +-
 src/Grisette/Core/Control/Monad/CBMCExcept.hs                | 4 ++--
 src/Grisette/Core/Control/Monad/UnionM.hs                    | 4 ++--
 src/Grisette/Core/Data/Class/CEGISSolver.hs                  | 2 +-
 src/Grisette/Core/Data/Class/{Evaluate.hs => EvaluateSym.hs} | 4 ++--
 test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs             | 2 +-
 test/Grisette/Core/Control/ExceptionTests.hs                 | 2 +-
 test/Grisette/Core/Control/Monad/UnionMTests.hs              | 2 +-
 test/Grisette/Core/Data/Class/EvaluateSymTests.hs            | 2 +-
 test/Grisette/IR/SymPrim/Data/SymPrimTests.hs                | 2 +-
 test/Grisette/TestUtil/SymbolicAssertion.hs                  | 2 +-
 14 files changed, 18 insertions(+), 18 deletions(-)
 rename src/Grisette/Core/Data/Class/{Evaluate.hs => EvaluateSym.hs} (98%)

diff --git a/grisette.cabal b/grisette.cabal
index 0ba65a4e..82c5b23c 100644
--- 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
index 522d58bb..dec1e3ae 100644
--- 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
index 9f346737..fd47f7eb 100644
--- 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
index 0438b634..d2cd881c 100644
--- 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
index d19e8c31..3342f2eb 100644
--- 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
index 27e7f405..2f19d3fa 100644
--- 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
index 7a281a81..e86a1566 100644
--- 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 b/src/Grisette/Core/Data/Class/EvaluateSym.hs
similarity index 98%
rename from src/Grisette/Core/Data/Class/Evaluate.hs
rename to src/Grisette/Core/Data/Class/EvaluateSym.hs
index 586adfc1..041922ea 100644
--- a/src/Grisette/Core/Data/Class/Evaluate.hs
+++ b/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
index b49d0e4d..4fe7816c 100644
--- 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
index a6aeb4d0..0f2f1daa 100644
--- 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
index 947808b9..0ed439df 100644
--- 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
index 05cbe782..c389b576 100644
--- 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
index 20e7aec3..5692e0fd 100644
--- 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
index 0a0c8088..065b3679 100644
--- 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))