Huge refactoring to make module structures clearer

CHANGELOG.md

@@ -17,7 +17,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Removed
 
-- Removed the `Grisette.Lib.Mtl` module. ([#132](https://github.com/lsrcz/grisette/pull/132))
+- [Breaking] Removed the `Grisette.Lib.Mtl` module. ([#132](https://github.com/lsrcz/grisette/pull/132))
+- [Breaking] Removed `SymBoolOp` and `SymIntegerOp`. ([#146](https://github.com/lsrcz/grisette/pull/146))
+- [Breaking] Removed `ExtractSymbolics` instance for `SymbolSet`. ([#146](https://github.com/lsrcz/grisette/pull/146))
 
 ### Fixed
 
@@ -34,7 +36,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - [Breaking] Changed the name of `Union` constructors and patterns. ([#133](https://github.com/lsrcz/grisette/pull/133))
 - The `Union` patterns, when used as constructors, now merges the result. ([#133](https://github.com/lsrcz/grisette/pull/133))
 - Changed the symbolic identifier type from `String` to `Data.Text.Text`. ([#141](https://github.com/lsrcz/grisette/pull/141))
-- `Grisette.Data.Class.BitVector.BVSignConversion` is now `Grisette.Data.Class.SignConversion.SignConversion`. ([#142](https://github.com/lsrcz/grisette/pull/142))
+- [Breaking] `Grisette.Data.Class.BitVector.BVSignConversion` is now `Grisette.Data.Class.SignConversion.SignConversion`. ([#142](https://github.com/lsrcz/grisette/pull/142))
+- [Breaking] Moved the `ITEOp`, `LogicalOp`, and `SEq` type classes to dedicated modules. ([#146](https://github.com/lsrcz/grisette/pull/146))
+- [Breaking] Moved `Grisette.Data.Class.Evaluate` to `Grisette.Data.Class.EvaluateSym`. ([#146](https://github.com/lsrcz/grisette/pull/146))
+- [Breaking] Moved `Grisette.Data.Class.Substitute` to `Grisette.Data.Class.SubstituteSym`. ([#146](https://github.com/lsrcz/grisette/pull/146))
+- [Breaking] Split the `Grisette.Data.Class.SafeArith` module to `Grisette.Data.Class.SafeDivision` and `Grisette.Data.Class.SafeLinearArith`. ([#146](https://github.com/lsrcz/grisette/pull/146))
 
 ## [0.3.1.1] -- 2023-09-29
 

grisette.cabal

@@ -59,23 +59,26 @@ library
       Grisette.Core.Control.Monad.UnionM
       Grisette.Core.Data.BV
       Grisette.Core.Data.Class.BitVector
-      Grisette.Core.Data.Class.Bool
       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
       Grisette.Core.Data.Class.GPretty
+      Grisette.Core.Data.Class.ITEOp
+      Grisette.Core.Data.Class.LogicalOp
       Grisette.Core.Data.Class.Mergeable
       Grisette.Core.Data.Class.ModelOps
-      Grisette.Core.Data.Class.SafeArith
+      Grisette.Core.Data.Class.SafeDivision
+      Grisette.Core.Data.Class.SafeLinearArith
+      Grisette.Core.Data.Class.SEq
       Grisette.Core.Data.Class.SignConversion
       Grisette.Core.Data.Class.SimpleMergeable
       Grisette.Core.Data.Class.Solvable
       Grisette.Core.Data.Class.Solver
       Grisette.Core.Data.Class.SOrd
-      Grisette.Core.Data.Class.Substitute
+      Grisette.Core.Data.Class.SubstituteSym
       Grisette.Core.Data.Class.ToCon
       Grisette.Core.Data.Class.ToSym
       Grisette.Core.Data.FileLocation

src/Grisette/Backend/SBV/Data/SMT/Solving.hs

@@ -56,15 +56,15 @@ import Grisette.Backend.SBV.Data.SMT.Lowering
     parseModel,
   )
 import Grisette.Core.Data.BV (IntN, WordN)
-import Grisette.Core.Data.Class.Bool (LogicalOp (nots, (&&~)))
 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),
   )
+import Grisette.Core.Data.Class.LogicalOp (LogicalOp (nots, (&&~)))
 import Grisette.Core.Data.Class.ModelOps
   ( ModelOps (exact, exceptFor),
     SymbolSetOps (isEmptySet),

src/Grisette/Core.hs

@@ -181,7 +181,6 @@ module Grisette.Core
     LogicalOp (..),
     ITEOp (..),
     SEq (..),
-    SymBoolOp,
     SOrd (..),
     BV (..),
     bvExtract,
@@ -190,7 +189,6 @@ module Grisette.Core
     SignConversion (..),
     SafeDivision (..),
     SafeLinearArith (..),
-    SymIntegerOp,
     Function (..),
 
     -- ** Unsolvable types
@@ -1032,8 +1030,6 @@ import Grisette.Core.BuiltinUnionWrappers
 import Grisette.Core.Control.Exception
   ( AssertionError (..),
     VerificationConditions (..),
-    symAssert,
-    symAssume,
   )
 import Grisette.Core.Control.Monad.CBMCExcept
   ( CBMCEither (..),
@@ -1059,12 +1055,6 @@ import Grisette.Core.Data.Class.BitVector
     bvExtract,
     sizedBVExtract,
   )
-import Grisette.Core.Data.Class.Bool
-  ( ITEOp (..),
-    LogicalOp (..),
-    SEq (..),
-    SymBoolOp,
-  )
 import Grisette.Core.Data.Class.CEGISSolver
   ( CEGISCondition (..),
     CEGISSolver (..),
@@ -1080,11 +1070,13 @@ import Grisette.Core.Data.Class.CEGISSolver
   )
 import Grisette.Core.Data.Class.Error
   ( TransformError (..),
+    symAssert,
     symAssertTransformableError,
     symAssertWith,
+    symAssume,
     symThrowTransformableError,
   )
-import Grisette.Core.Data.Class.Evaluate
+import Grisette.Core.Data.Class.EvaluateSym
   ( EvaluateSym (..),
     evaluateSymToCon,
   )
@@ -1122,6 +1114,8 @@ import Grisette.Core.Data.Class.GenSym
     runFresh,
     runFreshT,
   )
+import Grisette.Core.Data.Class.ITEOp (ITEOp (..))
+import Grisette.Core.Data.Class.LogicalOp (LogicalOp (..))
 import Grisette.Core.Data.Class.Mergeable
   ( DynamicSortedIdx (..),
     Mergeable (..),
@@ -1146,12 +1140,10 @@ 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 (..),
-    SafeLinearArith (..),
-    SymIntegerOp,
-  )
+import Grisette.Core.Data.Class.SafeDivision (SafeDivision (..))
+import Grisette.Core.Data.Class.SafeLinearArith (SafeLinearArith (..))
 import Grisette.Core.Data.Class.SignConversion (SignConversion (..))
 import Grisette.Core.Data.Class.SimpleMergeable
   ( SimpleMergeable (..),
@@ -1179,7 +1171,7 @@ import Grisette.Core.Data.Class.Solver
     solveExcept,
     solveMultiExcept,
   )
-import Grisette.Core.Data.Class.Substitute
+import Grisette.Core.Data.Class.SubstituteSym
   ( SubstituteSym (..),
     SubstituteSym' (..),
   )

src/Grisette/Core/Control/Exception.hs

@@ -4,7 +4,6 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE Trustworthy #-}
 
 -- |
@@ -19,38 +18,16 @@ module Grisette.Core.Control.Exception
   ( -- * Predefined exceptions
     AssertionError (..),
     VerificationConditions (..),
-    symAssert,
-    symAssume,
   )
 where
 
 import Control.DeepSeq (NFData)
-import Control.Exception (ArithException, ArrayException)
-import Control.Monad.Except (MonadError)
 import GHC.Generics (Generic)
-import Generics.Deriving (Default (Default))
-import Grisette.Core.Control.Monad.Union (MonadUnion)
-import Grisette.Core.Data.Class.Bool (SEq)
-import Grisette.Core.Data.Class.Error
-  ( TransformError (transformError),
-    symAssertTransformableError,
-  )
-import Grisette.Core.Data.Class.Evaluate (EvaluateSym)
-import Grisette.Core.Data.Class.ExtractSymbolics
-  ( ExtractSymbolics,
-  )
-import Grisette.Core.Data.Class.Mergeable (Mergeable)
-import Grisette.Core.Data.Class.SOrd
-  ( SOrd (symCompare, (<=~), (<~), (>=~), (>~)),
-  )
-import Grisette.Core.Data.Class.SimpleMergeable
-  ( SimpleMergeable,
-    mrgSingle,
-  )
-import Grisette.Core.Data.Class.Solvable (Solvable (con))
-import Grisette.Core.Data.Class.ToCon (ToCon)
-import Grisette.Core.Data.Class.ToSym (ToSym)
-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool)
+
+-- import Grisette.Core.Data.Class.Mergeable (Mergeable)
+-- import Grisette.Core.Data.Class.SimpleMergeable
+--   ( SimpleMergeable,
+--   )
 
 -- $setup
 -- >>> import Grisette.Core
@@ -61,122 +38,10 @@ import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool)
 -- | Assertion error.
 data AssertionError = AssertionError
   deriving (Show, Eq, Ord, Generic, NFData)
-  deriving (ToCon AssertionError, ToSym AssertionError) via (Default AssertionError)
-
-deriving via (Default AssertionError) instance Mergeable AssertionError
-
-deriving via (Default AssertionError) instance SimpleMergeable AssertionError
-
-deriving via (Default AssertionError) instance SEq AssertionError
-
-instance SOrd AssertionError where
-  _ <=~ _ = con True
-  _ <~ _ = con False
-  _ >=~ _ = con True
-  _ >~ _ = con False
-  _ `symCompare` _ = mrgSingle EQ
-
-deriving via (Default AssertionError) instance EvaluateSym AssertionError
-
-deriving via (Default AssertionError) instance ExtractSymbolics AssertionError
 
 -- | Verification conditions.
 -- A crashed program path can terminate with either assertion violation errors or assumption violation errors.
 data VerificationConditions
   = AssertionViolation
   | AssumptionViolation
   deriving (Show, Eq, Ord, Generic, NFData)
-  deriving (ToCon VerificationConditions, ToSym VerificationConditions) via (Default VerificationConditions)
-
-deriving via (Default VerificationConditions) instance Mergeable VerificationConditions
-
-deriving via (Default VerificationConditions) instance SEq VerificationConditions
-
-instance SOrd VerificationConditions where
-  l >=~ r = con $ l >= r
-  l >~ r = con $ l > r
-  l <=~ r = con $ l <= r
-  l <~ r = con $ l < r
-  l `symCompare` r = mrgSingle $ l `compare` r
-
-deriving via (Default VerificationConditions) instance EvaluateSym VerificationConditions
-
-deriving via (Default VerificationConditions) instance ExtractSymbolics VerificationConditions
-
-instance TransformError VerificationConditions VerificationConditions where
-  transformError = id
-
-instance TransformError AssertionError VerificationConditions where
-  transformError _ = AssertionViolation
-
-instance TransformError ArithException AssertionError where
-  transformError _ = AssertionError
-
-instance TransformError ArrayException AssertionError where
-  transformError _ = AssertionError
-
-instance TransformError AssertionError AssertionError where
-  transformError = id
-
--- | Used within a monadic multi path computation to begin exception processing.
---
--- Checks the condition passed to the function.
--- The current execution path will be terminated with assertion error if the condition is false.
---
--- If the condition is symbolic, Grisette will split the execution into two paths based on the condition.
--- The symbolic execution will continue on the then-branch, where the condition is true.
--- For the else branch, where the condition is false, the execution will be terminated.
---
--- The resulting monadic environment should be compatible with the 'AssertionError'
--- error type. See 'TransformError' type class for details.
---
--- __/Examples/__:
---
--- Terminates the execution if the condition is false.
--- Note that we may lose the 'Mergeable' knowledge here if no possible execution
--- path is viable. This may affect the efficiency in theory, but in practice this
--- should not be a problem as all paths are terminated and no further evaluation
--- would be performed.
---
--- >>> symAssert (con False) :: ExceptT AssertionError UnionM ()
--- ExceptT {Left AssertionError}
--- >>> do; symAssert (con False); mrgReturn 1 :: ExceptT AssertionError UnionM Integer
--- ExceptT <Left AssertionError>
---
--- No effect if the condition is true:
---
--- >>> symAssert (con True) :: ExceptT AssertionError UnionM ()
--- ExceptT {Right ()}
--- >>> do; symAssert (con True); mrgReturn 1 :: ExceptT AssertionError UnionM Integer
--- ExceptT {Right 1}
---
--- Splitting the path and terminate one of them when the condition is symbolic.
---
--- >>> symAssert (ssym "a") :: ExceptT AssertionError UnionM ()
--- ExceptT {If (! a) (Left AssertionError) (Right ())}
--- >>> do; symAssert (ssym "a"); mrgReturn 1 :: ExceptT AssertionError UnionM Integer
--- ExceptT {If (! a) (Left AssertionError) (Right 1)}
---
--- 'AssertionError' is compatible with 'VerificationConditions':
---
--- >>> symAssert (ssym "a") :: ExceptT VerificationConditions UnionM ()
--- ExceptT {If (! a) (Left AssertionViolation) (Right ())}
-symAssert ::
-  (TransformError AssertionError to, Mergeable to, MonadError to erm, MonadUnion erm) =>
-  SymBool ->
-  erm ()
-symAssert = symAssertTransformableError AssertionError
-
--- | Used within a monadic multi path computation to begin exception processing.
---
--- Similar to 'symAssert', but terminates the execution path with 'AssumptionViolation' error.
---
--- /Examples/:
---
--- >>> symAssume (ssym "a") :: ExceptT VerificationConditions UnionM ()
--- ExceptT {If (! a) (Left AssumptionViolation) (Right ())}
-symAssume ::
-  (TransformError VerificationConditions to, Mergeable to, MonadError to erm, MonadUnion erm) =>
-  SymBool ->
-  erm ()
-symAssume = symAssertTransformableError AssumptionViolation

src/Grisette/Core/Control/Monad/CBMCExcept.hs

@@ -64,8 +64,8 @@ import Data.Functor.Classes
 import Data.Functor.Contravariant (Contravariant (contramap))
 import Data.Hashable (Hashable)
 import GHC.Generics (Generic, Generic1)
-import Grisette.Core.Data.Class.Bool (SEq ((==~)))
-import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))
+import Grisette.Core.Control.Monad.UnionM (UnionM)
+import Grisette.Core.Data.Class.EvaluateSym (EvaluateSym (evaluateSym))
 import Grisette.Core.Data.Class.ExtractSymbolics
   ( ExtractSymbolics (extractSymbolics),
   )
@@ -82,6 +82,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),
@@ -469,3 +470,6 @@ instance
   UnionWithExcept (CBMCExceptT e u v) u e v
   where
   extractUnionExcept = merge . fmap runCBMCEither . runCBMCExceptT
+
+instance UnionWithExcept (UnionM (CBMCEither e v)) UnionM e v where
+  extractUnionExcept = fmap runCBMCEither