Merge pull request #79 from bruderj15/develop

Publish v2.4.0

CHANGELOG.md

@@ -6,6 +6,15 @@ 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.4.0 _(2024-08-21)_
+
+### Added
+- Added _**observable** sharing_ with `Language.Hasmtlib.Internal.Sharing`. Thank you fabeulous@github for the great help!
+- Added `Language.Hasmtlib.Internal.Uniplate1` for plating GADTs
+
+### Changed
+- Deleted and moved `Language.Hasmtlib.Equatable`, `Language.Hasmtlib.Orderable`, `Language.Hasmtlib.Iteable` & `Language.Hasmtlib.Internal.Expr` into `Language.Hasmtlib.Type.Expr`
+
 ## v2.3.2 _(2024-08-17)_
 
 ### Changed

README.md

@@ -6,18 +6,18 @@ 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.
 It is highly inspired by [ekmett/ersatz](https://github.com/ekmett/ersatz) which does the same for QSAT. Communication with external solvers is handled by [tweag/smtlib-backends](https://github.com/tweag/smtlib-backends).
 
-Building expressions with type-level representations of the SMTLib2-Types guarantees type-safety when communicating with external solvers.
+Building expressions with **type-level representations** of the **SMTLib2-Sorts** guarantees type-safety when communicating with external solvers.
 
-Although Hasmtlib does not yet make use of _observable_ sharing [(StableNames)](https://downloads.haskell.org/ghc/9.6.1/docs/libraries/base-4.18.0.0/System-Mem-StableName.html#:~:text=Stable%20Names,-data%20StableName%20a&text=An%20abstract%20name%20for%20an,makeStableName%20on%20the%20same%20object.) like Ersatz does, sharing in the API still allows for pure formula construction.
+While **formula construction** is entirely **pure**, Hasmtlib - just like `ersatz` - makes use of _**observable sharing**_ for expressions.
 
-Therefore, this allows you to use the much richer subset of Haskell than a purely monadic meta-language would, which the strong [hgoes/smtlib2](https://github.com/hgoes/smtlib2) is one of. This ultimately results in extremely compact code.
+This allows you to use the much richer subset of Haskell than a purely monadic meta-language would, which ultimately results in extremely compact code.
 
 For instance, to define the addition of two `V3` containing Real-SMT-Expressions:
 ```haskell
 v3Add :: V3 (Expr RealSort) -> V3 (Expr RealSort) -> V3 (Expr RealSort)
 v3Add = liftA2 (+)
 ```
-Even better, the [Expr-GADT](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Internal/Expr.hs) allows for a polymorph definition:
+Even better, the [Expr-GADT](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Internal/Expr.hs) allows a polymorph definition:
 ```haskell
 v3Add :: Num (Expr t) => V3 (Expr t) -> V3 (Expr t) -> V3 (Expr t)
 v3Add = liftA2 (+)

hasmtlib.cabal

@@ -1,7 +1,7 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               2.3.2
+version:               2.4.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.
@@ -28,18 +28,17 @@ library
   default-extensions:  DataKinds, GADTs, TypeFamilies, OverloadedStrings
 
   exposed-modules:     Language.Hasmtlib
-                     , Language.Hasmtlib.Lens
                      , Language.Hasmtlib.Codec
-                     , Language.Hasmtlib.Iteable
                      , Language.Hasmtlib.Boolean
                      , Language.Hasmtlib.Variable
                      , Language.Hasmtlib.Counting
-                     , Language.Hasmtlib.Equatable
-                     , Language.Hasmtlib.Orderable
                      , Language.Hasmtlib.Integraled
                      , Language.Hasmtlib.Internal.Parser
                      , Language.Hasmtlib.Internal.Bitvec
                      , Language.Hasmtlib.Internal.Render
+                     , Language.Hasmtlib.Internal.Sharing
+                     , Language.Hasmtlib.Internal.Uniplate1
+                     , Language.Hasmtlib.Internal.Constraint
                      , Language.Hasmtlib.Solver.Common
                      , Language.Hasmtlib.Solver.Bitwuzla
                      , Language.Hasmtlib.Solver.CVC5
@@ -58,13 +57,11 @@ library
                      , Language.Hasmtlib.Type.Option
                      , Language.Hasmtlib.Type.ArrayMap
 
-  other-modules:       Language.Hasmtlib.Internal.Expr
-                     , Language.Hasmtlib.Internal.Expr.Num
-
   build-depends:       attoparsec                   >= 0.14.4 && < 1
                      , base                         >= 4.17.2 && < 5
                      , bytestring                   >= 0.11.5 && < 1
                      , containers                   >= 0.6.7  && < 1
+                     , unordered-containers         >= 0.2.20 && < 0.3
                      , dependent-map                >= 0.4    && < 1
                      , mtl                          >= 2.2.2  && < 3
                      , text                         >= 2.0.2  && < 3

src/Language/Hasmtlib.hs

@@ -10,12 +10,8 @@ module Language.Hasmtlib
   , module Language.Hasmtlib.Type.SMTSort
   , module Language.Hasmtlib.Type.Solution
   , module Language.Hasmtlib.Type.ArrayMap
-  , module Language.Hasmtlib.Lens
   , module Language.Hasmtlib.Integraled
-  , module Language.Hasmtlib.Iteable
   , module Language.Hasmtlib.Boolean
-  , module Language.Hasmtlib.Equatable
-  , module Language.Hasmtlib.Orderable
   , module Language.Hasmtlib.Codec
   , module Language.Hasmtlib.Counting
   , module Language.Hasmtlib.Variable
@@ -39,12 +35,8 @@ import Language.Hasmtlib.Type.Option
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
-import Language.Hasmtlib.Lens
 import Language.Hasmtlib.Integraled
-import Language.Hasmtlib.Iteable
 import Language.Hasmtlib.Boolean
-import Language.Hasmtlib.Equatable
-import Language.Hasmtlib.Orderable
 import Language.Hasmtlib.Codec
 import Language.Hasmtlib.Counting
 import Language.Hasmtlib.Variable

src/Language/Hasmtlib/Boolean.hs

@@ -89,20 +89,22 @@ any :: (Foldable t, Boolean b) => (a -> b) -> t a -> b
 any p = foldl (\acc b -> acc || p b) false
 
 instance Boolean Bool where
-  bool  = id
-  true  = True
-  false = False
-  (&&)  = (P.&&)
-  (||)  = (P.||)
-  not   = P.not
-  xor   = (/=)
+  bool   = id
+  true   = True
+  false  = False
+  (&&)   = (P.&&)
+  (||)   = (P.||)
+  not    = P.not
+  xor    = (/=)
+  (<==>) = (==)
 
 instance Boolean Bit where
-  bool = Bit
-  (&&) = (.&.)
-  (||) = (.|.)
-  not  = complement
-  xor  = Bits.xor
+  bool     = Bit
+  (&&)     = (.&.)
+  (||)     = (.|.)
+  not      = complement
+  xor      = Bits.xor
+  x <==> y = bool (x == y)
 
 -- | Defined bitwise
 instance KnownNat n => Boolean (V.Vector n Bit) where
@@ -111,3 +113,4 @@ instance KnownNat n => Boolean (V.Vector n Bit) where
   (||) = V.zipWith (||)
   not  = V.map not
   xor  = V.zipWith Bits.xor
+  x <==> y = bool (x == y)

src/Language/Hasmtlib/Codec.hs

@@ -7,7 +7,7 @@ module Language.Hasmtlib.Codec where
 
 import Prelude hiding (not, (&&), (||), all, and)
 import Language.Hasmtlib.Internal.Bitvec
-import Language.Hasmtlib.Internal.Expr
+import Language.Hasmtlib.Type.Expr (Expr(..), SMTVar(..), unwrapValue, wrapValue)
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Type.SMTSort

src/Language/Hasmtlib/Counting.hs

@@ -1,12 +1,8 @@
 module Language.Hasmtlib.Counting where
 
 import Prelude hiding (not, (&&), (||), or)
-import Language.Hasmtlib.Internal.Expr.Num ()
-import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Type.SMTSort
-import Language.Hasmtlib.Equatable
-import Language.Hasmtlib.Orderable
-import Language.Hasmtlib.Iteable
+import Language.Hasmtlib.Type.Expr
 import Data.Proxy
 
 -- | Wrapper for 'count' which takes a 'Proxy'.

src/Language/Hasmtlib/Internal/Constraint.hs

@@ -0,0 +1,14 @@
+module Language.Hasmtlib.Internal.Constraint where
+
+import Data.Kind
+
+-- | AllC ensures that a list of constraints is applied to a poly-kinded 'Type' k
+--
+-- @
+-- AllC '[]       k = ()
+-- AllC (c ': cs) k = (c k, AllC cs k)
+-- @
+type AllC :: [k -> Constraint] -> k -> Constraint
+type family AllC cs k :: Constraint where
+  AllC '[]       k = ()
+  AllC (c ': cs) k = (c k, AllC cs k)