hasmtlib 2.1.0 → 2.2.0

raw patch · 7 files changed

+187/−79 lines, 7 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +8/−0
• hasmtlib.cabal +1/−1
• src/Language/Hasmtlib/Codec.hs +82/−53
• src/Language/Hasmtlib/Equatable.hs +22/−0
• src/Language/Hasmtlib/Iteable.hs +8/−0
• src/Language/Hasmtlib/Orderable.hs +23/−0
• src/Language/Hasmtlib/Variable.hs +43/−25

@@ -6,6 +6,14 @@ 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.2.0 _(2024-08-09)_++### Added+- Added multiple basic instances for `Equatable`, `Orderable`, `Iteable`, `Variable` & `Codec`++### Changed+- *(breaking change)* `Variable` & `Codec` now ship with a `Generic` default implementation instead of relying on `Applicative`. This will break your instances if the type does not have an instance for `Generic`.+ ## v2.1.0 _(2024-07-26)_  ### Added

@@ -1,7 +1,7 @@ cabal-version:         3.0  name:                  hasmtlib-version:               2.1.0+version:               2.2.0 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.

@@ -1,7 +1,6 @@ {-# LANGUAGE DefaultSignatures #-}--- required for DefaultEncoded a-{-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE UndecidableInstances #-}  module Language.Hasmtlib.Codec where @@ -20,28 +19,43 @@ import Data.IntMap as IM hiding (foldl) import Data.Dependent.Map as DMap import Data.Tree (Tree)+import Data.Monoid (Sum, Product, First, Last, Dual)+import Data.Functor.Identity (Identity) import qualified Data.Vector.Sized as V import Control.Monad+import GHC.Generics --- | Compute the default 'Decoded' 'Type' for every functor-wrapper.---   Useful for instances using default signatures.+-- | Computes a default 'Decoded' 'Type' by distributing 'Decoded' to it's type arguments. type family DefaultDecoded a :: Type where-  DefaultDecoded (f a) = f (Decoded a)+  DefaultDecoded (t a b c d e f g h) = t (Decoded a) (Decoded b) (Decoded c) (Decoded d) (Decoded e) (Decoded f) (Decoded g) (Decoded h)+  DefaultDecoded (t a b c d e f g) = t (Decoded a) (Decoded b) (Decoded c) (Decoded d) (Decoded e) (Decoded f) (Decoded g)+  DefaultDecoded (t a b c d e f) = t (Decoded a) (Decoded b) (Decoded c) (Decoded d) (Decoded e) (Decoded f)+  DefaultDecoded (t a b c d e) = t (Decoded a) (Decoded b) (Decoded c) (Decoded d) (Decoded e)+  DefaultDecoded (t a b c d) = t (Decoded a) (Decoded b) (Decoded c) (Decoded d)+  DefaultDecoded (t a b c) = t (Decoded a) (Decoded b) (Decoded c)+  DefaultDecoded (t a b) = t (Decoded a) (Decoded b)+  DefaultDecoded (t a) = t (Decoded a)+  DefaultDecoded () = ()  -- | Lift values to SMT-Values or decode them.+--+--   You can derive an instance of this class if your type is 'Generic'. class Codec a where+  -- | Resulting of decoding @a@   type Decoded a :: Type   type Decoded a = DefaultDecoded a    -- | Decode a value using given solution.   decode :: Solution -> a -> Maybe (Decoded a)-  default decode :: (Traversable f, Codec b, a ~ f b, Decoded a ~ f (Decoded b)) => Solution -> a -> Maybe (Decoded a)-  decode sol = traverse (decode sol)+  default decode :: (Generic a, Generic (Decoded a), GCodec (Rep a), GDecoded (Rep a) x ~ Rep (Decoded a) x) => Solution -> a -> Maybe (Decoded a)+  decode sol x = do+    gdecodedx <- gdecode sol $ from x+    Just $ to gdecodedx    -- | Encode a value as constant.   encode :: Decoded a -> a-  default encode :: (Functor f, Codec b, a ~ f b, Decoded a ~ f (Decoded b)) => Decoded a -> a-  encode = fmap encode+  default encode :: (Generic a, Generic (Decoded a), GCodec (Rep a), GDecoded (Rep a) x ~ Rep (Decoded a) x) => Decoded a -> a+  encode = to . gencode . from  -- | Decode and evaluate expressions instance KnownSMTSort t => Codec (Expr t) where@@ -117,56 +131,71 @@    encode = Constant . wrapValue -instance Codec () where-  type Decoded () = ()-  decode _ _ = Just ()-  encode _   = ()+instance Codec ()+instance (Codec a, Codec b) => Codec (a,b)+instance (Codec a, Codec b, Codec c) => Codec (a,b,c)+instance (Codec a, Codec b, Codec c, Codec d) => Codec (a,b,c,d)+instance (Codec a, Codec b, Codec c, Codec d, Codec e) => Codec (a,b,c,d,e)+instance (Codec a, Codec b, Codec c, Codec d, Codec e, Codec f) => Codec (a,b,c,d,e,f)+instance (Codec a, Codec b, Codec c, Codec d, Codec e, Codec f, Codec g) => Codec (a,b,c,d,e,f,g)+instance (Codec a, Codec b, Codec c, Codec d, Codec e, Codec f, Codec g, Codec h) => Codec (a,b,c,d,e,f,g,h)+instance Codec a => Codec [a]+instance Codec a => Codec (Maybe a)+instance Codec a => Codec (Tree a)+instance (Codec a, Codec b) => Codec (Either a b)+instance Codec a => Codec (Sum a)+instance Codec a => Codec (Product a)+instance Codec a => Codec (First a)+instance Codec a => Codec (Last a)+instance Codec a => Codec (Dual a)+instance Codec a => Codec (Identity a) -instance (Codec a, Codec b) => Codec (a,b) where-  type Decoded (a,b) = (Decoded a, Decoded b)-  decode s (a,b) = (,) <$> decode s a <*> decode s b-  encode   (a,b) = (encode a, encode b)+instance Codec a => Codec (IntMap a) where+  decode sol = traverse (decode sol)+  encode = fmap encode -instance (Codec a, Codec b, Codec c) => Codec (a,b,c) where-  type Decoded (a,b,c) = (Decoded a, Decoded b, Decoded c)-  decode s (a,b,c) = (,,) <$> decode s a <*> decode s b <*> decode s c-  encode   (a,b,c) = (encode a, encode b, encode c)+instance Codec a => Codec (Seq a) where+  decode sol = traverse (decode sol)+  encode = fmap encode -instance (Codec a, Codec b, Codec c, Codec d) => Codec (a,b,c,d) where-  type Decoded (a,b,c,d) = (Decoded a, Decoded b, Decoded c, Decoded d)-  decode s (a,b,c,d) = (,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d-  encode   (a,b,c,d) = (encode a, encode b, encode c, encode d)+instance Codec a => Codec (Map k a) where+  type Decoded (Map k a) = Map k (Decoded a)+  decode sol = traverse (decode sol)+  encode = fmap encode -instance (Codec a, Codec b, Codec c, Codec d, Codec e) => Codec (a,b,c,d,e) where-  type Decoded (a,b,c,d,e) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e)-  decode s (a,b,c,d,e) = (,,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e-  encode   (a,b,c,d,e) = (encode a, encode b, encode c, encode d, encode e)+class GCodec f where+  type GDecoded f :: Type -> Type+  gdecode :: Solution -> f a -> Maybe (GDecoded f a)+  gencode :: GDecoded f a -> f a -instance (Codec a, Codec b, Codec c, Codec d, Codec e, Codec f) => Codec (a,b,c,d,e,f) where-  type Decoded (a,b,c,d,e,f) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f)-  decode s (a,b,c,d,e,f) = (,,,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f-  encode   (a,b,c,d,e,f) = (encode a, encode b, encode c, encode d, encode e, encode f)+instance GCodec U1 where+  type GDecoded U1 = U1+  gdecode _ U1     = Just U1+  gencode          = id -instance (Codec a, Codec b, Codec c, Codec d, Codec e, Codec f, Codec g) => Codec (a,b,c,d,e,f,g) where-  type Decoded (a,b,c,d,e,f,g) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f, Decoded g)-  decode s (a,b,c,d,e,f,g) = (,,,,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f <*> decode s g-  encode   (a,b,c,d,e,f,g) = (encode a, encode b, encode c, encode d, encode e, encode f, encode g)+instance GCodec V1 where+  type GDecoded V1 = V1+  gdecode _        = Just+  gencode          = id -instance (Codec a, Codec b, Codec c, Codec d, Codec e, Codec f, Codec g, Codec h) => Codec (a,b,c,d,e,f,g,h) where-  type Decoded (a,b,c,d,e,f,g,h) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f, Decoded g, Decoded h)-  decode s (a,b,c,d,e,f,g,h) = (,,,,,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f <*> decode s g <*> decode s h-  encode   (a,b,c,d,e,f,g,h) = (encode a, encode b, encode c, encode d, encode e, encode f, encode g, encode h)+instance (GCodec f, GCodec g) => GCodec (f :*: g) where+  type GDecoded (f :*: g) = (GDecoded f :*: GDecoded g)+  gdecode sol (a :*: b)   = liftM2 (:*:) (gdecode sol a) (gdecode sol b)+  gencode (a :*: b)       = gencode a :*: gencode b -instance Codec a => Codec [a]-instance Codec a => Codec (IntMap a)-instance Codec a => Codec (Map k a)-instance Codec a => Codec (Maybe a)-instance Codec a => Codec (Seq a)-instance Codec a => Codec (Tree a)+instance (GCodec f, GCodec g) => GCodec (f :+: g) where+  type GDecoded (f :+: g) = (GDecoded f :+: GDecoded g)+  gdecode sol (L1 a)      = L1 <$> gdecode sol a+  gdecode sol (R1 a)      = R1 <$> gdecode sol a+  gencode (L1 a)          = L1 $ gencode a+  gencode (R1 a)          = R1 $ gencode a -instance (Codec a, Codec b) => Codec (Either a b) where-  type Decoded (Either a b) = Either (Decoded a) (Decoded b)-  decode s (Left  a) = Left  <$> decode s a-  decode s (Right b) = Right <$> decode s b-  encode   (Left  a) = Left  (encode a)-  encode   (Right b) = Right (encode b)+instance GCodec f => GCodec (M1 i c f) where+  type GDecoded (M1 i c f) = (M1 i c (GDecoded f))+  gdecode sol (M1 x)       = M1 <$> gdecode sol x+  gencode (M1 x)           = M1 $ gencode x++instance Codec a => GCodec (K1 i a) where+  type GDecoded (K1 i a) = K1 i (Decoded a)+  gdecode sol (K1 a)     = K1 <$> decode sol a+  gencode (K1 a)         = K1 $ encode a

@@ -11,12 +11,17 @@ import Data.Int import Data.Word import Data.Void+import Data.Tree (Tree)+import Data.Monoid (Sum, Product, First, Last, Dual)+import Data.Functor.Identity (Identity) import qualified Data.Vector.Sized as V import Numeric.Natural import GHC.Generics  -- | Test two as on equality as SMT-Expression. --+--   You can derive an instance of this class if your type is 'Generic'.+-- -- @ --     x <- var @RealType --     y <- var@@ -83,3 +88,20 @@ instance Equatable Double   where x === y = bool (x == y) instance Equatable Ordering where x === y = bool (x == y) instance Equatable Bool     where x === y = bool (x == y)+instance (Equatable a, Equatable b) => Equatable (a,b)+instance (Equatable a, Equatable b, Equatable c) => Equatable (a,b,c)+instance (Equatable a, Equatable b, Equatable c, Equatable d) => Equatable (a,b,c,d)+instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e) => Equatable (a,b,c,d,e)+instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f) => Equatable (a,b,c,d,e,f)+instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f, Equatable g) => Equatable (a,b,c,d,e,f,g)+instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f, Equatable g, Equatable h) => Equatable (a,b,c,d,e,f,g,h)+instance Equatable a => Equatable [a]+instance Equatable a => Equatable (Tree a)+instance Equatable a => Equatable (Maybe a)+instance (Equatable a, Equatable b) => Equatable (Either a b)+instance Equatable a => Equatable (Sum a)+instance Equatable a => Equatable (Product a)+instance Equatable a => Equatable (First a)+instance Equatable a => Equatable (Last a)+instance Equatable a => Equatable (Dual a)+instance Equatable a => Equatable (Identity a)

@@ -6,6 +6,8 @@ import Language.Hasmtlib.Type.SMTSort import Data.Sequence (Seq) import Data.Tree+import Data.Monoid (Sum, Product, First, Last, Dual)+import Data.Functor.Identity (Identity)  -- | If condition (p :: b) then (t :: a) else (f :: a) --@@ -30,6 +32,12 @@ instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Maybe a) instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Seq a) instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Tree a)+instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Sum a)+instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Product a)+instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (First a)+instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Last a)+instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Dual a)+instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Identity a)  instance Iteable (Expr BoolSort) () where   ite _ _ _ = ()

@@ -13,12 +13,17 @@ import Data.Int import Data.Word import Data.Void+import Data.Tree (Tree)+import Data.Monoid (Sum, Product, First, Last, Dual)+import Data.Functor.Identity (Identity) import Numeric.Natural import GHC.Generics import GHC.TypeNats  -- | Compare two as as SMT-Expression. --+--   You can derive an instance of this class if your type is 'Generic'.+-- -- @ -- x <- var @RealSort -- y <- var@@ -155,3 +160,21 @@                                   x <=? y = bool (x <= y) instance Orderable Bool     where x <?  y = bool (x <  y)                                   x <=? y = bool (x <= y)++instance (Orderable a, Orderable b) => Orderable (a,b)+instance (Orderable a, Orderable b, Orderable c) => Orderable (a,b,c)+instance (Orderable a, Orderable b, Orderable c, Orderable d) => Orderable (a,b,c,d)+instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e) => Orderable (a,b,c,d,e)+instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f) => Orderable (a,b,c,d,e,f)+instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f, Orderable g) => Orderable (a,b,c,d,e,f,g)+instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f, Orderable g, Orderable h) => Orderable (a,b,c,d,e,f,g,h)+instance Orderable a => Orderable [a]+instance Orderable a => Orderable (Tree a)+instance Orderable a => Orderable (Maybe a)+instance (Orderable a, Orderable b) => Orderable (Either a b)+instance Orderable a => Orderable (Sum a)+instance Orderable a => Orderable (Product a)+instance Orderable a => Orderable (First a)+instance Orderable a => Orderable (Last a)+instance Orderable a => Orderable (Dual a)+instance Orderable a => Orderable (Identity a)

@@ -6,21 +6,27 @@ import Language.Hasmtlib.Type.MonadSMT import Language.Hasmtlib.Type.SMTSort import Data.Proxy+import Data.Monoid (Sum, Product, First, Last, Alt, Dual)+import Data.Functor.Const (Const)+import Data.Functor.Identity (Identity)+import Data.Functor.Compose (Compose)+import GHC.Generics  -- | Construct a variable datum of a data-type by creating variables for all its fields. --+--   You can derive an instance of this class if your type is 'Generic' and has exactly one constructor.+-- -- @---    data V3 a = V3 a a a+--    data V3 a = V3 a a a deriving Generic --    instance Variable a => V3 a -- @ -----    >>> varV3 <- variable @(V3 (Expr RealType)) ; varV3---        V3 (Var RealType) (Var RealType) (Var RealType)+--    >>> varV3 :: V3 (Expr RealType) <- variable ; varV3+--        V3 (Expr RealType) (Expr RealType) (Expr RealType) class Variable a where   variable :: MonadSMT s m => m a-  default variable :: (MonadSMT s m, Applicative f, Traversable f, Variable b, a ~ f b) => m a-  variable = sequenceA $ pure variable-  {-# INLINEABLE variable #-}+  default variable :: (MonadSMT s m, Generic a, GVariable (Rep a)) => m a+  variable = to <$> gvariable  -- | Wrapper for 'variable' which takes a 'Proxy' variable' :: forall s m a. (MonadSMT s m, Variable a) => Proxy a -> m a@@ -31,29 +37,41 @@   variable = var   {-# INLINE variable #-} -instance Variable () where-  variable = return ()--instance (Variable a, Variable b) => Variable (a,b) where-  variable = (,) <$> variable <*> variable+instance Variable ()+instance (Variable a, Variable b) => Variable (a,b)+instance (Variable a, Variable b, Variable c) => Variable (a,b,c)+instance (Variable a, Variable b, Variable c, Variable d) => Variable (a,b,c,d)+instance (Variable a, Variable b, Variable c, Variable d, Variable e) => Variable (a,b,c,d,e)+instance (Variable a, Variable b, Variable c, Variable d, Variable e, Variable f) => Variable (a,b,c,d,e,f)+instance (Variable a, Variable b, Variable c, Variable d, Variable e, Variable f, Variable g) => Variable (a,b,c,d,e,f,g)+instance (Variable a, Variable b, Variable c, Variable d, Variable e, Variable f, Variable g, Variable h) => Variable (a,b,c,d,e,f,g,h)+instance Variable a => Variable (Sum a)+instance Variable a => Variable (Product a)+instance Variable a => Variable (First a)+instance Variable a => Variable (Last a)+instance Variable a => Variable (Dual a)+instance Variable a => Variable (Identity a)+instance Variable m => Variable (Const m a)+instance Variable (f a) => Variable (Alt f a)+instance Variable (f (g a)) => Variable (Compose f g a) -instance (Variable a, Variable b, Variable c) => Variable (a,b,c) where-  variable = (,,) <$> variable <*> variable  <*> variable+instance Variable a => Variable (Maybe a) where+  variable = Just <$> variable -instance (Variable a, Variable b, Variable c, Variable d) => Variable (a,b,c,d) where-  variable = (,,,) <$> variable <*> variable <*> variable <*> variable+instance Variable b => Variable (Either a b) where+  variable = Right <$> variable -instance (Variable a, Variable b, Variable c, Variable d, Variable e) => Variable (a,b,c,d,e) where-  variable = (,,,,) <$> variable <*> variable <*> variable <*> variable <*> variable+class GVariable f where+  gvariable :: MonadSMT s m => m (f a) -instance (Variable a, Variable b, Variable c, Variable d, Variable e, Variable f) => Variable (a,b,c,d,e,f) where-  variable = (,,,,,) <$> variable <*> variable <*> variable <*> variable <*> variable <*> variable+instance GVariable U1 where+  gvariable = return U1 -instance (Variable a, Variable b, Variable c, Variable d, Variable e, Variable f, Variable g) => Variable (a,b,c,d,e,f,g) where-  variable = (,,,,,,) <$> variable <*> variable <*> variable <*> variable <*> variable <*> variable <*> variable+instance (GVariable f, GVariable g) => GVariable (f :*: g) where+  gvariable = liftA2 (:*:) gvariable gvariable -instance (Variable a, Variable b, Variable c, Variable d, Variable e, Variable f, Variable g, Variable h) => Variable (a,b,c,d,e,f,g,h) where-  variable = (,,,,,,,) <$> variable <*> variable <*> variable <*> variable <*> variable <*> variable <*> variable <*> variable+instance GVariable f => GVariable (M1 i c f) where+  gvariable = M1 <$> gvariable -instance Variable a => Variable (Maybe a)-instance Variable b => Variable (Either a b)+instance Variable a => GVariable (K1 i a) where+  gvariable = K1 <$> variable