Merge pull request #119 from bruderj15/develop

Publish v2.7.2

CHANGELOG.md

@@ -6,6 +6,17 @@ file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [PVP versioning](https://pvp.haskell.org/).
 
+## v2.7.2 _(2024-11-27)_
+
+### Added
+- Added dependency `constrained-some`
+
+### Changed
+- Replaced internal usages of custom existential `SomeSMTSort` with `Some1` from `constrained-some`
+
+### Removed
+- Removed module `Language.Hasmtlib.Internal.Constraint`
+
 ## v2.7.1 _(2024-10-05)_
 
 ### Changed

hasmtlib.cabal

@@ -1,7 +1,7 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               2.7.1
+version:               2.7.2
 synopsis:              A monad for interfacing with external SMT solvers
 description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.
   It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.
@@ -36,7 +36,6 @@ library
                      , Language.Hasmtlib.Internal.Render
                      , Language.Hasmtlib.Internal.Sharing
                      , Language.Hasmtlib.Internal.Uniplate1
-                     , Language.Hasmtlib.Internal.Constraint
                      , Language.Hasmtlib.Solver.Bitwuzla
                      , Language.Hasmtlib.Solver.CVC5
                      , Language.Hasmtlib.Solver.MathSAT
@@ -78,6 +77,7 @@ library
                      , bitvec                       >= 1.1.5  && < 2
                      , finite-typelits              >= 0.1.0  && < 1
                      , vector-sized                 >= 1      && < 2
+                     , constrained-some             >= 0.1    && < 0.2
 
   ghc-options:       -O2
                      -Wall

src/Language/Hasmtlib/Internal/Parser.hs

@@ -13,6 +13,7 @@ import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Type.Expr
+import Data.Some.Constraint
 import Data.Bit
 import Data.Coerce
 import Data.Proxy
@@ -66,23 +67,23 @@ parseSomeSol = do
   _     <- string "var_"
   vId   <- decimal @Int
   _     <- skipSpace >> string "()" >> skipSpace
-  (SomeSMTSort someSort) <- parseSomeSort
+  (Some1 someSort) <- parseSomeSort
   _     <- skipSpace
   expr  <- parseExpr' someSort
   _     <- skipSpace >> char ')'
   case decode mempty expr of
     Nothing    -> fail $ "Solver reponded with solution for var_" ++ show vId ++ " but it contains "
                       ++ "another var. This cannot be parsed and evaluated currently."
-    Just value -> return $ SomeSMTSort $ SMTVarSol (coerce vId) (wrapValue value)
+    Just value -> return $ Some1 $ SMTVarSol (coerce vId) (wrapValue value)
 {-# INLINEABLE parseSomeSol #-}
 
 parseSomeSort :: Parser (SomeKnownOrdSMTSort SSMTSort)
-parseSomeSort = (string "Bool" *> pure (SomeSMTSort SBoolSort))
-        <|> (string "Int"  *> pure (SomeSMTSort SIntSort))
-        <|> (string "Real" *> pure (SomeSMTSort SRealSort))
+parseSomeSort = (string "Bool" *> pure (Some1 SBoolSort))
+        <|> (string "Int"  *> pure (Some1 SIntSort))
+        <|> (string "Real" *> pure (Some1 SRealSort))
         <|> parseSomeBitVecSort
         <|> parseSomeArraySort
-        <|> (string "String" *> pure (SomeSMTSort SStringSort))
+        <|> (string "String" *> pure (Some1 SStringSort))
 {-# INLINEABLE parseSomeSort #-}
 
 parseSomeBitVecSort :: Parser (SomeKnownOrdSMTSort SSMTSort)
@@ -95,18 +96,18 @@ parseSomeBitVecSort = do
     -- SMTLib does not differentiate between signed and unsigned BitVec on the type-level
     -- We do. So we always just put Unsigned here and in Codec (Expr t)
     -- if (t ~ BvSort Signed _) we retrieve unsigned solution and flip type-level encoding
-    SomeNat pn -> return $ SomeSMTSort $ SBvSort (Proxy @Unsigned) pn
+    SomeNat pn -> return $ Some1 $ SBvSort (Proxy @Unsigned) pn
 {-# INLINEABLE parseSomeBitVecSort #-}
 
 parseSomeArraySort :: Parser (SomeKnownOrdSMTSort SSMTSort)
 parseSomeArraySort = do
   _ <- char '(' >> skipSpace
   _ <- string "Array" >> skipSpace
-  (SomeSMTSort keySort)   <- parseSomeSort
+  (Some1 keySort)   <- parseSomeSort
   _ <- skipSpace
-  (SomeSMTSort valueSort) <- parseSomeSort
+  (Some1 valueSort) <- parseSomeSort
   _ <- skipSpace >> char ')'
-  return $ SomeSMTSort $ SArraySort (goProxy keySort) (goProxy valueSort)
+  return $ Some1 $ SArraySort (goProxy keySort) (goProxy valueSort)
     where
       goProxy :: forall t. SSMTSort t -> Proxy t
       goProxy _ = Proxy @t

src/Language/Hasmtlib/Internal/Render.hs

@@ -11,6 +11,7 @@ import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Bitvec
 import Language.Hasmtlib.Type.ArrayMap
 import Data.Coerce
+import Data.Some.Constraint
 import Data.Sequence
 import Data.Foldable (foldl')
 import Data.Map (size, minViewWithKey)
@@ -292,7 +293,7 @@ class RenderProblem s where
 instance RenderProblem SMT where
   renderOptions = fromList . fmap render . view options
   renderLogic = maybe mempty (renderSetLogic . stringUtf8) . view mlogic
-  renderDeclareVars = fmap (\(SomeSMTSort v) -> renderDeclareVar v) . view vars
+  renderDeclareVars = fmap (\(Some1 v) -> renderDeclareVar v) . view vars
   renderAssertions = fmap renderAssert . view formulas
   renderSoftAssertions _ = mempty
   renderMinimizations _ = mempty
@@ -304,5 +305,5 @@ instance RenderProblem OMT where
   renderDeclareVars = renderDeclareVars . view smt
   renderAssertions = renderAssertions . view smt
   renderSoftAssertions = fmap render . view softFormulas
-  renderMinimizations = fmap (\case SomeSMTSort minExpr -> render minExpr) . view targetMinimize
-  renderMaximizations = fmap (\case SomeSMTSort maxExpr -> render maxExpr) . view targetMaximize
+  renderMinimizations = fmap (\case Some1 minExpr -> render minExpr) . view targetMinimize
+  renderMaximizations = fmap (\case Some1 maxExpr -> render maxExpr) . view targetMaximize

src/Language/Hasmtlib/Internal/Sharing.hs

@@ -12,6 +12,7 @@ import Language.Hasmtlib.Type.MonadSMT
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Expr
 import Data.GADT.Compare
+import Data.Some.Constraint
 import Data.HashMap.Lazy
 import Data.Default
 import Data.Kind
@@ -72,7 +73,7 @@ share expr@(Exists _ _) _ = return expr
 share origExpr expr = do
   let sn = unsafePerformIO (makeStableName' origExpr)
    in use (stableMap.at sn) >>= \mexpr' -> case mexpr' of
-        Just (SomeSMTSort expr') -> case geq (sortSing' origExpr) (sortSing' expr') of
+        Just (Some1 expr') -> case geq (sortSing' origExpr) (sortSing' expr') of
           Nothing -> expr >>= makeNode sn
           Just Refl -> return expr'
         Nothing -> expr >>= makeNode sn
@@ -81,7 +82,7 @@ makeNode :: (Equatable (Expr t), KnownSMTSort t, MonadSMT s m, Sharing s, Sharin
 makeNode sn nodeExpr = do
   nodeVar <- var
   assertSharedNode sn $ nodeVar === nodeExpr
-  stableMap.at sn ?= SomeSMTSort nodeVar
+  stableMap.at sn ?= Some1 nodeVar
   return nodeVar
 
 makeStableName' :: a -> IO (StableName ())

src/Language/Hasmtlib/Internal/Uniplate1.hs

@@ -2,8 +2,8 @@
 
 module Language.Hasmtlib.Internal.Uniplate1 where
 
-import Language.Hasmtlib.Internal.Constraint
 import Data.Functor.Identity
+import Data.Some.Constraint
 import Data.Kind
 
 type Uniplate1 :: (k -> Type) -> [k -> Constraint] -> Constraint

src/Language/Hasmtlib/Type/Debugger.hs

@@ -27,6 +27,7 @@ import Language.Hasmtlib.Type.SMT
 import Language.Hasmtlib.Type.OMT
 import Language.Hasmtlib.Type.Expr
 import Language.Hasmtlib.Type.SMTSort
+import Data.Some.Constraint
 import Data.Sequence as Seq hiding ((|>))
 import Data.ByteString.Lazy (ByteString, split)
 import Data.ByteString.Lazy.UTF8 (toString)
@@ -160,23 +161,23 @@ class StateDebugger s where
 instance StateDebugger SMT where
   statistically = silently
     { debugState = \s -> do
-      putStrLn $ "Bool Vars:  " ++ show (Seq.length $ Seq.filter (\(SomeSMTSort v) -> case sortSing' v of SBoolSort -> True ; _ -> False) $ s^.vars)
-      putStrLn $ "Arith Vars: " ++ show (Seq.length $ Seq.filter (\(SomeSMTSort v) -> case sortSing' v of SBoolSort -> False ; _ -> True) $ s^.vars)
+      putStrLn $ "Bool Vars:  " ++ show (Seq.length $ Seq.filter (\(Some1 v) -> case sortSing' v of SBoolSort -> True ; _ -> False) $ s^.vars)
+      putStrLn $ "Arith Vars: " ++ show (Seq.length $ Seq.filter (\(Some1 v) -> case sortSing' v of SBoolSort -> False ; _ -> True) $ s^.vars)
       putStrLn $ "Assertions: " ++ show (Seq.length (s^.formulas))
       putStrLn $ "Size:       " ++ show (sum $ fmap exprSize $ s^.formulas)
     }
 
 instance StateDebugger OMT where
   statistically = silently
     { debugState = \omt -> do
-      putStrLn $ "Bool Vars:       " ++ show (Seq.length $ Seq.filter (\(SomeSMTSort v) -> case sortSing' v of SBoolSort -> True ; _ -> False) $ omt^.smt.vars)
-      putStrLn $ "Arith Vars:      " ++ show (Seq.length $ Seq.filter (\(SomeSMTSort v) -> case sortSing' v of SBoolSort -> False ; _ -> True) $ omt^.smt.vars)
+      putStrLn $ "Bool Vars:       " ++ show (Seq.length $ Seq.filter (\(Some1 v) -> case sortSing' v of SBoolSort -> True ; _ -> False) $ omt^.smt.vars)
+      putStrLn $ "Arith Vars:      " ++ show (Seq.length $ Seq.filter (\(Some1 v) -> case sortSing' v of SBoolSort -> False ; _ -> True) $ omt^.smt.vars)
       putStrLn $ "Hard assertions: " ++ show (Seq.length (omt^.smt.formulas))
       putStrLn $ "Soft assertions: " ++ show (Seq.length (omt^.softFormulas))
       putStrLn $ "Optimizations:   " ++ show (Seq.length (omt^.targetMinimize) + Seq.length (omt^.targetMaximize))
       let omtSize = sum (fmap exprSize $ omt^.smt.formulas)
                   + sum (fmap (exprSize . view formula) $ omt^.softFormulas)
-                  + sum (fmap (\(SomeSMTSort (Minimize expr)) -> exprSize expr) $ omt^.targetMinimize)
-                  + sum (fmap (\(SomeSMTSort (Maximize expr)) -> exprSize expr) $ omt^.targetMaximize)
+                  + sum (fmap (\(Some1 (Minimize expr)) -> exprSize expr) $ omt^.targetMinimize)
+                  + sum (fmap (\(Some1 (Maximize expr)) -> exprSize expr) $ omt^.targetMaximize)
       putStrLn $ "Size:            " ++ show omtSize
     }

src/Language/Hasmtlib/Type/OMT.hs

@@ -31,6 +31,7 @@ import Language.Hasmtlib.Type.MonadSMT
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Expr
 import Language.Hasmtlib.Type.SMT
+import Data.Some.Constraint
 import Data.List (isPrefixOf)
 import Data.Default
 import Data.Coerce
@@ -76,7 +77,7 @@ instance MonadState OMT m => MonadSMT OMT m where
 
   var' p = do
     newVar <- smtvar' p
-    smt.vars %= (|> SomeSMTSort newVar)
+    smt.vars %= (|> Some1 newVar)
     return $ Var newVar
   {-# INLINE var' #-}
 
@@ -97,11 +98,11 @@ instance MonadSMT OMT m => MonadOMT OMT m where
   minimize expr = do
     sm <- use (smt.sharingMode)
     sExpr <- runSharing sm expr
-    modifying targetMinimize (|> SomeSMTSort (Minimize sExpr))
+    modifying targetMinimize (|> Some1 (Minimize sExpr))
   maximize expr = do
     sm <- use (smt.sharingMode)
     sExpr <- runSharing sm expr
-    modifying targetMaximize (|> SomeSMTSort (Maximize sExpr))
+    modifying targetMaximize (|> Some1 (Maximize sExpr))
   assertSoft expr w gid = do
     sm <- use (smt.sharingMode)
     sExpr <- runSharing sm expr

src/Language/Hasmtlib/Type/SMT.hs

@@ -21,6 +21,7 @@ import Language.Hasmtlib.Type.MonadSMT
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Option
 import Language.Hasmtlib.Type.Expr
+import Data.Some.Constraint
 import Data.List (isPrefixOf)
 import Data.Default
 import Data.Coerce
@@ -57,7 +58,7 @@ instance MonadState SMT m => MonadSMT SMT m where
 
   var' p = do
     newVar <- smtvar' p
-    vars %= (|> SomeSMTSort newVar)
+    vars %= (|> Some1 newVar)
     return $ Var newVar
   {-# INLINEABLE var' #-}
 

src/Language/Hasmtlib/Type/SMTSort.hs

@@ -18,17 +18,16 @@ module Language.Hasmtlib.Type.SMTSort
 , KnownSMTSort(..), sortSing'
 
   -- * Existential
-, SomeSMTSort(..)
 , SomeKnownSMTSort
 )
 where
 
-import Language.Hasmtlib.Internal.Constraint
 import Language.Hasmtlib.Type.Bitvec
 import Language.Hasmtlib.Type.ArrayMap
 import Data.GADT.Compare
 import Data.Kind
 import Data.Proxy
+import Data.Some.Constraint
 import qualified Data.Text as Text
 import Control.Lens
 import GHC.TypeLits
@@ -125,11 +124,5 @@ instance KnownSMTSort StringSort                 where sortSing = SStringSort
 sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t
 sortSing' _ = sortSing @t
 
--- | An existential wrapper that hides some 'SMTSort' and a list of 'Constraint's holding for it.
-data SomeSMTSort cs f where
-  SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f
-
-deriving instance (forall t. Show (f t)) => Show (SomeSMTSort cs f)
-
 -- | An existential wrapper that hides some known 'SMTSort'.
-type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f
+type SomeKnownSMTSort f = Some1 ((~) f) KnownSMTSort

src/Language/Hasmtlib/Type/Solution.hs

@@ -38,6 +38,7 @@ import Language.Hasmtlib.Type.SMTSort
 import Data.IntMap as IMap hiding (foldl)
 import Data.Dependent.Map as DMap
 import Data.Dependent.Map.Lens
+import Data.Some.Constraint
 import Control.Lens
 
 -- | Results of check-sat commands.
@@ -64,12 +65,12 @@ class Ord (HaskellType t) => OrdHaskellType t
 instance Ord (HaskellType t) => OrdHaskellType t
 
 -- | An existential wrapper that hides some known 'SMTSort' with an 'Ord' 'HaskellType'
-type SomeKnownOrdSMTSort f = SomeSMTSort '[KnownSMTSort, OrdHaskellType] f
+type SomeKnownOrdSMTSort f = Somes1 '[(~) f] '[KnownSMTSort, OrdHaskellType]
 
 -- | Create a 'Solution' from some 'SMTVarSol's.
 fromSomeVarSols :: [SomeKnownOrdSMTSort SMTVarSol] -> Solution
 fromSomeVarSols = foldl
-  (\dsol (SomeSMTSort s) -> let sSort = sortSing' s in
+  (\dsol (Some1 s) -> let sSort = sortSing' s in
     dsol & dmat sSort %~
       (\case
         Nothing -> Just $ IntValueMap $ IMap.singleton (s^.solVar.varId) (s^.solVal)