Move Queriable class to Data.SBV

makes imports simpler
LeventErkok · Nov 6, 2024 · 5097f8b · 5097f8b
1 parent c5f47d7
commit 5097f8b
Show file tree

Hide file tree

Showing 15 changed files with 50 additions and 75 deletions.
diff --git a/Data/SBV.hs b/Data/SBV.hs
@@ -145,13 +145,15 @@
 -- get in touch if there is a solver you'd like to see included.
 -----------------------------------------------------------------------------
 
-{-# LANGUAGE DataKinds            #-}
-{-# LANGUAGE FlexibleContexts     #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE ScopedTypeVariables  #-}
-{-# LANGUAGE TypeApplications     #-}
-{-# LANGUAGE TypeFamilies         #-}
-{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE DefaultSignatures     #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
 
 {-# OPTIONS_GHC -Wall -Werror #-}
 
@@ -421,6 +423,9 @@ module Data.SBV (
   , isConcrete, isSymbolic, isConcretely, mkSymVal
   , MonadSymbolic(..), Symbolic, SymbolicT, label, output, runSMT, runSMTWith
 
+  -- * Queriable values
+  , Queriable(..), freshVar, freshVar_, getValue
+
   -- * Module exports
   -- $moduleExportIntro
 
@@ -430,7 +435,8 @@ module Data.SBV (
   , module Data.Ratio
   ) where
 
-import Control.Monad (when)
+import Control.Monad       (when)
+import Control.Monad.Trans (MonadIO)
 
 import Data.SBV.Core.AlgReals
 import Data.SBV.Core.Data       hiding (free, free_, mkFreeVars,
@@ -488,11 +494,14 @@ import Data.Ratio
 import Data.Word
 
 import Data.SBV.SMT.Utils (SBVException(..))
+
 import Data.SBV.Control.Types (SMTReasonUnknown(..), Logic(..))
+import Data.SBV.Control.Utils (getValue, freshVar, freshVar_)
 
 import qualified Data.SBV.Utils.CrackNum as CN
 
 import Data.Proxy (Proxy(..))
+import Data.Kind  (Type)
 import GHC.TypeLits (KnownNat, type (<=), type (+), type (-))
 
 import Prelude hiding((+), (-)) -- to avoid the haddock ambiguity
@@ -1752,4 +1761,34 @@ optIndependentWith config p = do
      _                   -> error $ "An independent optimization call resulted in a bad result:"
                                   ++ "\n" ++ show res
 
+-- | An queriable value: Mapping between concrete/symbolic values. If your type is traversable and simply embeds
+-- symbolic equivalents for one type, then you can simply define 'create'. (Which is the most common case.)
+class Queriable m a where
+  type QueryResult a :: Type
+
+  -- | ^ Create a new symbolic value of type @a@
+  create  :: QueryT m a
+
+  -- | ^ Extract the current value in a SAT context
+  project :: a -> QueryT m (QueryResult a)
+
+  -- | ^ Create a literal value. Morally, 'embed' and 'project' are inverses of each other
+  -- via the 'QueryT' monad transformer.
+  embed   :: QueryResult a -> QueryT m a
+
+  default project :: (a ~ t (SBV e), QueryResult a ~ t e, Traversable t, MonadIO m, SymVal e) => a -> QueryT m (QueryResult a)
+  project = mapM getValue
+
+  default embed :: (a ~ t (SBV e), QueryResult a ~ t e, Traversable t, MonadIO m, SymVal e) => QueryResult a -> QueryT m a
+  embed = pure . fmap literal
+  {-# MINIMAL create #-}
+
+-- | Generic 'Queriable' instance for 'SymVal' values
+instance {-# OVERLAPPABLE #-} (MonadIO m, SymVal a) => Queriable m (SBV a) where
+  type QueryResult (SBV a) = a
+
+  create  = freshVar_
+  project = getValue
+  embed   = return . literal
+
 {- HLint ignore module "Use import/export shortcut" -}
diff --git a/Data/SBV/Control.hs b/Data/SBV/Control.hs
@@ -9,20 +9,13 @@
 -- Control sublanguage for interacting with SMT solvers.
 -----------------------------------------------------------------------------
 
-{-# LANGUAGE ConstraintKinds       #-}
-{-# LANGUAGE DefaultSignatures     #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE TypeFamilies          #-}
-{-# LANGUAGE TypeOperators         #-}
-
 {-# OPTIONS_GHC -Wall -Werror #-}
 
 module Data.SBV.Control (
      -- $queryIntro
 
      -- * User queries
-       ExtractIO(..), MonadQuery(..), Queriable(..), Query, query
+       ExtractIO(..), MonadQuery(..), Query, query
 
      -- * Create a fresh variable
      , freshVar_, freshVar
@@ -88,46 +81,10 @@ import Data.SBV.Control.Utils (registerUISMTFunction, registerSMTType)
 
 import qualified Data.SBV.Control.Utils as Trans
 
-import Data.SBV.Core.Data (SymVal, SBV, literal)
-
-import Control.Monad.Trans (MonadIO)
-import Data.Kind (Type)
-
-
 -- | Run a custom query
 query :: Query a -> Symbolic a
 query = Trans.executeQuery QueryExternal
 
--- | An queriable value: Mapping between concrete/symbolic values. If your type is traversable and simply embeds
--- symbolic equivalents for one type, then you can simply define 'create'. (Which is the most common case.)
-class Queriable m a where
-  type QueryResult a :: Type
-
-  -- | ^ Create a new symbolic value of type @a@
-  create  :: QueryT m a
-
-  -- | ^ Extract the current value in a SAT context
-  project :: a -> QueryT m (QueryResult a)
-
-  -- | ^ Create a literal value. Morally, 'embed' and 'project' are inverses of each other
-  -- via the 'QueryT' monad transformer.
-  embed   :: QueryResult a -> QueryT m a
-
-  default project :: (a ~ t (SBV e), QueryResult a ~ t e, Traversable t, MonadIO m, SymVal e) => a -> QueryT m (QueryResult a)
-  project = mapM getValue
-
-  default embed :: (a ~ t (SBV e), QueryResult a ~ t e, Traversable t, MonadIO m, SymVal e) => QueryResult a -> QueryT m a
-  embed = pure . fmap literal
-  {-# MINIMAL create #-}
-
--- | Generic 'Queriable' instance for 'SymVal' values
-instance {-# OVERLAPPABLE #-} (MonadIO m, SymVal a) => Queriable m (SBV a) where
-  type QueryResult (SBV a) = a
-
-  create  = freshVar_
-  project = getValue
-  embed   = return . literal
-
 {- $queryIntro
 In certain cases, the user might want to take over the communication with the solver, programmatically
 querying the engine and issuing commands accordingly. Queries can be extremely powerful as

diff --git a/Documentation/SBV/Examples/ProofTools/BMC.hs b/Documentation/SBV/Examples/ProofTools/BMC.hs
@@ -30,7 +30,6 @@ module Documentation.SBV.Examples.ProofTools.BMC where
 
 import Data.SBV
 import Data.SBV.Tools.BMC
-import Data.SBV.Control
 
 -- * System state
 

diff --git a/Documentation/SBV/Examples/ProofTools/Fibonacci.hs b/Documentation/SBV/Examples/ProofTools/Fibonacci.hs
@@ -34,7 +34,6 @@ module Documentation.SBV.Examples.ProofTools.Fibonacci where
 
 import Data.SBV
 import Data.SBV.Tools.Induction
-import Data.SBV.Control
 
 -- * System state
 

diff --git a/Documentation/SBV/Examples/ProofTools/Strengthen.hs b/Documentation/SBV/Examples/ProofTools/Strengthen.hs
@@ -41,7 +41,6 @@ module Documentation.SBV.Examples.ProofTools.Strengthen where
 
 import Data.SBV
 import Data.SBV.Tools.Induction
-import Data.SBV.Control
 
 -- * System state
 

diff --git a/Documentation/SBV/Examples/ProofTools/Sum.hs b/Documentation/SBV/Examples/ProofTools/Sum.hs
@@ -33,7 +33,6 @@ module Documentation.SBV.Examples.ProofTools.Sum where
 
 import Data.SBV
 import Data.SBV.Tools.Induction
-import Data.SBV.Control
 
 -- * System state
 

diff --git a/Documentation/SBV/Examples/Puzzles/DieHard.hs b/Documentation/SBV/Examples/Puzzles/DieHard.hs
@@ -26,7 +26,6 @@
 module Documentation.SBV.Examples.Puzzles.DieHard where
 
 import Data.SBV
-import Data.SBV.Control
 import Data.SBV.Tools.BMC
 
 -- | Possible actions

diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Append.hs b/Documentation/SBV/Examples/WeakestPreconditions/Append.hs
@@ -25,16 +25,14 @@
 module Documentation.SBV.Examples.WeakestPreconditions.Append where
 
 import Data.SBV
-import Data.SBV.Control
+import Data.SBV.Tools.WeakestPreconditions
 
 import Prelude hiding ((++))
 import qualified Prelude as P
 
 import           Data.SBV.List ((++))
 import qualified Data.SBV.List as L
 
-import Data.SBV.Tools.WeakestPreconditions
-
 import GHC.Generics (Generic)
 
 -- * Program state

diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs b/Documentation/SBV/Examples/WeakestPreconditions/Basics.hs
@@ -25,8 +25,6 @@
 module Documentation.SBV.Examples.WeakestPreconditions.Basics where
 
 import Data.SBV
-import Data.SBV.Control
-
 import Data.SBV.Tools.WeakestPreconditions
 
 import GHC.Generics (Generic)

diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs b/Documentation/SBV/Examples/WeakestPreconditions/Fib.hs
@@ -26,8 +26,6 @@
 module Documentation.SBV.Examples.WeakestPreconditions.Fib where
 
 import Data.SBV
-import Data.SBV.Control
-
 import Data.SBV.Tools.WeakestPreconditions
 
 import GHC.Generics (Generic)

diff --git a/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs b/Documentation/SBV/Examples/WeakestPreconditions/GCD.hs
@@ -28,8 +28,6 @@
 module Documentation.SBV.Examples.WeakestPreconditions.GCD where
 
 import Data.SBV
-import Data.SBV.Control
-
 import Data.SBV.Tools.WeakestPreconditions
 
 import GHC.Generics (Generic)

diff --git a/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs b/Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs
@@ -24,8 +24,6 @@
 module Documentation.SBV.Examples.WeakestPreconditions.IntDiv where
 
 import Data.SBV
-import Data.SBV.Control
-
 import Data.SBV.Tools.WeakestPreconditions
 
 import GHC.Generics (Generic)

diff --git a/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs b/Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs
@@ -26,8 +26,6 @@
 module Documentation.SBV.Examples.WeakestPreconditions.IntSqrt where
 
 import Data.SBV
-import Data.SBV.Control
-
 import Data.SBV.Tools.WeakestPreconditions
 
 import GHC.Generics (Generic)

diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Length.hs b/Documentation/SBV/Examples/WeakestPreconditions/Length.hs
@@ -23,12 +23,10 @@
 module Documentation.SBV.Examples.WeakestPreconditions.Length where
 
 import Data.SBV
-import Data.SBV.Control
+import Data.SBV.Tools.WeakestPreconditions
 
 import qualified Data.SBV.List as L
 
-import Data.SBV.Tools.WeakestPreconditions
-
 import GHC.Generics (Generic)
 
 -- * Program state

diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs
@@ -25,8 +25,6 @@
 module Documentation.SBV.Examples.WeakestPreconditions.Sum where
 
 import Data.SBV
-import Data.SBV.Control
-
 import Data.SBV.Tools.WeakestPreconditions
 
 import GHC.Generics (Generic)