Merge pull request #77 from bruderj15/74-fixes

74 fixes

.github/workflows/haskell-ci.yml

@@ -1,16 +1,16 @@
 # This GitHub workflow config has been generated by a script via
 #
-#   haskell-ci 'github' '.\hasmtlib.cabal'
+#   haskell-ci 'github' 'hasmtlib.cabal'
 #
 # To regenerate the script (for example after adjusting tested-with) run
 #
 #   haskell-ci regenerate
 #
 # For more information, see https://github.com/haskell-CI/haskell-ci
 #
-# version: 0.19.20240514
+# version: 0.19.20240708
 #
-# REGENDATA ("0.19.20240514",["github",".\\hasmtlib.cabal"])
+# REGENDATA ("0.19.20240708",["github","hasmtlib.cabal"])
 #
 name: Haskell-CI
 on:
@@ -28,9 +28,19 @@ jobs:
     strategy:
       matrix:
         include:
-          - compiler: ghc-9.6.5
+          - compiler: ghc-9.8.2
             compilerKind: ghc
-            compilerVersion: 9.6.5
+            compilerVersion: 9.8.2
+            setup-method: ghcup
+            allow-failure: false
+          - compiler: ghc-9.6.4
+            compilerKind: ghc
+            compilerVersion: 9.6.4
+            setup-method: ghcup
+            allow-failure: false
+          - compiler: ghc-9.4.8
+            compilerKind: ghc
+            compilerVersion: 9.4.8
             setup-method: ghcup
             allow-failure: false
       fail-fast: false
@@ -40,10 +50,10 @@ jobs:
           apt-get update
           apt-get install -y --no-install-recommends gnupg ca-certificates dirmngr curl git software-properties-common libtinfo5
           mkdir -p "$HOME/.ghcup/bin"
-          curl -sL https://downloads.haskell.org/ghcup/0.1.20.0/x86_64-linux-ghcup-0.1.20.0 > "$HOME/.ghcup/bin/ghcup"
+          curl -sL https://downloads.haskell.org/ghcup/0.1.30.0/x86_64-linux-ghcup-0.1.30.0 > "$HOME/.ghcup/bin/ghcup"
           chmod a+x "$HOME/.ghcup/bin/ghcup"
           "$HOME/.ghcup/bin/ghcup" install ghc "$HCVER" || (cat "$HOME"/.ghcup/logs/*.* && false)
-          "$HOME/.ghcup/bin/ghcup" install cabal 3.10.2.0 || (cat "$HOME"/.ghcup/logs/*.* && false)
+          "$HOME/.ghcup/bin/ghcup" install cabal 3.12.1.0 || (cat "$HOME"/.ghcup/logs/*.* && false)
         env:
           HCKIND: ${{ matrix.compilerKind }}
           HCNAME: ${{ matrix.compiler }}
@@ -61,7 +71,7 @@ jobs:
           echo "HC=$HC" >> "$GITHUB_ENV"
           echo "HCPKG=$HCPKG" >> "$GITHUB_ENV"
           echo "HADDOCK=$HADDOCK" >> "$GITHUB_ENV"
-          echo "CABAL=$HOME/.ghcup/bin/cabal-3.10.2.0 -vnormal+nowrap" >> "$GITHUB_ENV"
+          echo "CABAL=$HOME/.ghcup/bin/cabal-3.12.1.0 -vnormal+nowrap" >> "$GITHUB_ENV"
           HCNUMVER=$(${HC} --numeric-version|perl -ne '/^(\d+)\.(\d+)\.(\d+)(\.(\d+))?$/; print(10000 * $1 + 100 * $2 + ($3 == 0 ? $5 != 1 : $3))')
           echo "HCNUMVER=$HCNUMVER" >> "$GITHUB_ENV"
           echo "ARG_TESTS=--enable-tests" >> "$GITHUB_ENV"

.github/workflows/publish.yml

@@ -14,8 +14,8 @@ jobs:
       - uses: actions/checkout@v3
       - uses: sol/haskell-autotag@v1
         id: autotag
-      - run: ghcup install ghc 9.6.5
-      - run: ghcup set ghc 9.6.5
+      - run: ghcup install ghc 9.6.4
+      - run: ghcup set ghc 9.6.4
       - run: cabal sdist
       - run: cabal update
       - run: cabal haddock --haddock-for-hackage --enable-documentation

.hlint.yaml

@@ -0,0 +1,13 @@
+- arguments: [-XCPP, --cpp-define=HLINT, --cpp-ansi]
+
+- ignore:
+    name: Use camelCase
+
+- ignore:
+    name: Use lambda-case
+
+- ignore:
+    name: Use || # We define a different `or`
+
+- ignore:
+    name: Use && # We define a different `and`

CHANGELOG.md

@@ -6,6 +6,12 @@ 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.3.2 _(2024-08-17)_
+
+### Changed
+- Internal replacement of `Prelude.liftA2` for backwards compatiblity
+- Fixed bug where `solveMaximizedDebug` would solve minimized instead of maximized
+
 ## v2.3.1 _(2024-08-16)_
 
 ### Changed

hasmtlib.cabal

@@ -1,7 +1,7 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               2.3.1
+version:               2.3.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.
@@ -18,7 +18,9 @@ category:              SMT, Logic
 build-type:            Simple
 extra-source-files:    README.md
 extra-doc-files:       CHANGELOG.md
-tested-with:           GHC == 9.6.5
+tested-with:           GHC == 9.4.8
+                     , GHC == 9.6.4
+                     , GHC == 9.8.2
 
 library
   hs-source-dirs:      src

src/Language/Hasmtlib/Codec.hs

@@ -73,15 +73,15 @@ instance KnownSMTSort t => Codec (Expr t) where
     val <- IM.lookup (coerce var) m
     return $ unwrapValue val
   decode _ (Constant v)         = Just $ unwrapValue v
-  decode sol (Plus x y)         = liftA2 (+)   (decode sol x) (decode sol y)
+  decode sol (Plus x y)         = (+)   <$> decode sol x <*> decode sol y
   decode sol (Neg x)            = fmap negate  (decode sol x)
-  decode sol (Mul x y)          = liftA2 (*)   (decode sol x) (decode sol y)
+  decode sol (Mul x y)          = (*)   <$> decode sol x <*> decode sol y
   decode sol (Abs x)            = fmap abs     (decode sol x)
-  decode sol (Mod x y)          = liftA2 mod   (decode sol x) (decode sol y)
-  decode sol (IDiv x y)         = liftA2 div   (decode sol x) (decode sol y)
-  decode sol (Div x y)          = liftA2 (/)   (decode sol x) (decode sol y)
-  decode sol (LTH x y)          = liftA2 (<)   (decode sol x) (decode sol y)
-  decode sol (LTHE x y)         = liftA2 (<=)  (decode sol x) (decode sol y)
+  decode sol (Mod x y)          = mod   <$> decode sol x <*> decode sol y
+  decode sol (IDiv x y)         = div   <$> decode sol x <*> decode sol y
+  decode sol (Div x y)          = (/)   <$> decode sol x <*> decode sol y
+  decode sol (LTH x y)          = (<)   <$> decode sol x <*> decode sol y
+  decode sol (LTHE x y)         = (<=)  <$> decode sol x <*> decode sol y
   decode sol (EQU xs)           = do
     xs' <- decode sol (V.toList xs)
     case xs' of
@@ -91,13 +91,13 @@ instance KnownSMTSort t => Codec (Expr t) where
     xs' <- decode sol (V.toList xs)
     let xss = List.filter ((==2) . length) $ List.permutations xs'
     return $ all (\case (a:b:_) -> a /= b ; _ -> true) xss
-  decode sol (GTHE x y)         = liftA2 (>=)  (decode sol x) (decode sol y)
-  decode sol (GTH x y)          = liftA2 (>)   (decode sol x) (decode sol y)
+  decode sol (GTHE x y)         = (>=)  <$> decode sol x <*> decode sol y
+  decode sol (GTH x y)          = (>)   <$> decode sol x <*> decode sol y
   decode sol (Not x)            = fmap   not  (decode sol x)
-  decode sol (And x y)          = liftA2 (&&) (decode sol x) (decode sol y)
-  decode sol (Or x y)           = liftA2 (||) (decode sol x) (decode sol y)
-  decode sol (Impl x y)         = liftA2 (==>) (decode sol x) (decode sol y)
-  decode sol (Xor x y)          = liftA2 xor   (decode sol x) (decode sol y)
+  decode sol (And x y)          = (&&) <$> decode sol x <*> decode sol y
+  decode sol (Or x y)           = (||) <$> decode sol x <*> decode sol y
+  decode sol (Impl x y)         = (==>) <$> decode sol x <*> decode sol y
+  decode sol (Xor x y)          = xor   <$> decode sol x <*> decode sol y
   decode _ Pi                   = Just pi
   decode sol (Sqrt x)           = fmap sqrt  (decode sol x)
   decode sol (Exp x)            = fmap exp   (decode sol x)
@@ -110,48 +110,48 @@ instance KnownSMTSort t => Codec (Expr t) where
   decode sol (ToReal x)         = fmap realToFrac (decode sol x)
   decode sol (ToInt x)          = fmap truncate   (decode sol x)
   decode sol (IsInt x)          = fmap ((0 ==) . snd . properFraction) (decode sol x)
-  decode sol (Ite p t f)        = liftM3 (\p' t' f' -> if p' then t' else f') (decode sol p) (decode sol t) (decode sol f)
+  decode sol (Ite p t f)        = (\p' t' f' -> if p' then t' else f') <$> decode sol p <*> decode sol t <*> decode sol f
   decode sol (BvNot x)          = fmap not (decode sol x)
-  decode sol (BvAnd x y)        = liftA2 (&&) (decode sol x) (decode sol y)
-  decode sol (BvOr x y)         = liftA2 (||) (decode sol x) (decode sol y)
-  decode sol (BvXor x y)        = liftA2 xor (decode sol x) (decode sol y)
+  decode sol (BvAnd x y)        = (&&) <$> decode sol x <*> decode sol y
+  decode sol (BvOr x y)         = (||) <$> decode sol x <*> decode sol y
+  decode sol (BvXor x y)        = xor <$> decode sol x <*> decode sol y
   decode sol (BvNand x y)       = nand <$> sequenceA [decode sol x, decode sol y]
   decode sol (BvNor x y)        = nor  <$> sequenceA [decode sol x, decode sol y]
   decode sol (BvNeg x)          = fmap negate (decode sol x)
-  decode sol (BvAdd x y)        = liftA2 (+) (decode sol x) (decode sol y)
-  decode sol (BvSub x y)        = liftA2 (-) (decode sol x) (decode sol y)
-  decode sol (BvMul x y)        = liftA2 (*) (decode sol x) (decode sol y)
-  decode sol (BvuDiv x y)       = liftA2 div (decode sol x) (decode sol y)
-  decode sol (BvuRem x y)       = liftA2 rem (decode sol x) (decode sol y)
-  decode sol (BvShL x y)        = join $ liftA2 bvShL (decode sol x) (decode sol y)
-  decode sol (BvLShR x y)       = join $ liftA2 bvLShR (decode sol x) (decode sol y)
-  decode sol (BvConcat x y)     = liftA2 bvConcat (decode sol x) (decode sol y)
+  decode sol (BvAdd x y)        = (+) <$> decode sol x <*> decode sol y
+  decode sol (BvSub x y)        = (-) <$> decode sol x <*> decode sol y
+  decode sol (BvMul x y)        = (*) <$> decode sol x <*> decode sol y
+  decode sol (BvuDiv x y)       = div <$> decode sol x <*> decode sol y
+  decode sol (BvuRem x y)       = rem <$> decode sol x <*> decode sol y
+  decode sol (BvShL x y)        = join $ bvShL <$> decode sol x <*> decode sol y
+  decode sol (BvLShR x y)       = join $ bvLShR <$> decode sol x <*> decode sol y
+  decode sol (BvConcat x y)     = bvConcat <$> decode sol x <*> decode sol y
   decode sol (BvRotL i x)       = bvRotL i <$> decode sol x
   decode sol (BvRotR i x)       = bvRotR i <$> decode sol x
-  decode sol (BvuLT x y)        = liftA2 (<) (decode sol x) (decode sol y)
-  decode sol (BvuLTHE x y)      = liftA2 (<=) (decode sol x) (decode sol y)
-  decode sol (BvuGTHE x y)      = liftA2 (>=) (decode sol x) (decode sol y)
-  decode sol (BvuGT x y)        = liftA2 (>) (decode sol x) (decode sol y)
-  decode sol (ArrSelect i arr)  = liftA2 arrSelect (decode sol i) (decode sol arr)
-  decode sol (ArrStore i x arr) = liftM3 arrStore (decode sol i) (decode sol x) (decode sol arr)
-  decode sol (StrConcat x y)         = liftM2 (<>) (decode sol x) (decode sol y)
+  decode sol (BvuLT x y)        = (<) <$> decode sol x <*> decode sol y
+  decode sol (BvuLTHE x y)      = (<=) <$> decode sol x <*> decode sol y
+  decode sol (BvuGTHE x y)      = (>=) <$> decode sol x <*> decode sol y
+  decode sol (BvuGT x y)        = (>) <$> decode sol x <*> decode sol y
+  decode sol (ArrSelect i arr)  = arrSelect <$> decode sol i <*> decode sol arr
+  decode sol (ArrStore i x arr) = arrStore <$> decode sol i <*> decode sol x <*> decode sol arr
+  decode sol (StrConcat x y)         = (<>) <$> decode sol x <*> decode sol y
   decode sol (StrLength x)           = toInteger . Text.length <$> decode sol x
-  decode sol (StrLT x y)             = liftM2 (<) (decode sol x) (decode sol y)
-  decode sol (StrLTHE x y)           = liftM2 (<=) (decode sol x) (decode sol y)
-  decode sol (StrAt x i)             = liftM2 (\x' i' -> Text.singleton $ Text.index x' (fromInteger i')) (decode sol x) (decode sol i)
-  decode sol (StrSubstring x i j)    = liftM3 (\x' (fromInteger -> i') (fromInteger -> j') -> Text.take (j' - i') $ Text.drop i' x') (decode sol x) (decode sol i) (decode sol j)
-  decode sol (StrPrefixOf x y)       = liftM2 Text.isPrefixOf (decode sol x) (decode sol y)
-  decode sol (StrSuffixOf x y)       = liftM2 Text.isSuffixOf (decode sol x) (decode sol y)
-  decode sol (StrContains x y)       = liftM2 (flip Text.isInfixOf) (decode sol x) (decode sol y)
-  decode sol (StrIndexOf x y i)      = join $ liftM3 (\x' y' (fromInteger -> i') -> Text.findIndex ((y' ==) . Text.singleton) (Text.drop i' x') >>= Just . toInteger) (decode sol x) (decode sol y) (decode sol i)
-  decode sol (StrReplace src target replacement) = liftM3 (\src' target' replacement' -> replaceOne target' replacement' src') (decode sol target) (decode sol src) (decode sol replacement)
+  decode sol (StrLT x y)             = (<) <$> decode sol x <*> decode sol y
+  decode sol (StrLTHE x y)           = (<=) <$> decode sol x <*> decode sol y
+  decode sol (StrAt x i)             = (\x' i' -> Text.singleton $ Text.index x' (fromInteger i')) <$> decode sol x <*> decode sol i
+  decode sol (StrSubstring x i j)    = (\x' (fromInteger -> i') (fromInteger -> j') -> Text.take (j' - i') $ Text.drop i' x') <$> decode sol x <*> decode sol i <*> decode sol j
+  decode sol (StrPrefixOf x y)       = Text.isPrefixOf <$> decode sol x <*> decode sol y
+  decode sol (StrSuffixOf x y)       = Text.isSuffixOf <$> decode sol x <*> decode sol y
+  decode sol (StrContains x y)       = flip Text.isInfixOf <$> decode sol x <*> decode sol y
+  decode sol (StrIndexOf x y i)      = join $ (\x' y' (fromInteger -> i') -> Text.findIndex ((y' ==) . Text.singleton) (Text.drop i' x') >>= Just . toInteger) <$> decode sol x <*> decode sol y <*> decode sol i
+  decode sol (StrReplace src target replacement) = (\src' target' replacement' -> replaceOne target' replacement' src') <$> decode sol target <*> decode sol src <*> decode sol replacement
     where
       replaceOne pattern substitution text
         | Text.null back = text
         | otherwise = Text.concat [front, substitution, Text.drop (Text.length pattern) back]
           where
             (front, back) = Text.breakOn pattern text
-  decode sol (StrReplaceAll src target replacement) = liftM3 (\src' target' replacement' -> Text.replace target' replacement' src') (decode sol target) (decode sol src) (decode sol replacement)
+  decode sol (StrReplaceAll src target replacement) = (\src' target' replacement' -> Text.replace target' replacement' src') <$> decode sol target <*> decode sol src <*> decode sol replacement
   decode _ (ForAll _ _)         = Nothing
   decode _ (Exists _ _)         = Nothing
   encode = Constant . wrapValue
@@ -205,7 +205,7 @@ instance GCodec V1 where
 
 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)
+  gdecode sol (a :*: b)   = (:*:) <$> gdecode sol a <*> gdecode sol b
   gencode (a :*: b)       = gencode a :*: gencode b
 
 instance (GCodec f, GCodec g) => GCodec (f :+: g) where

src/Language/Hasmtlib/Iteable.hs

@@ -18,7 +18,7 @@ import Data.Functor.Identity (Identity)
 class Iteable b a where
   ite :: b -> a -> a -> a
   default ite :: (Iteable b c, Applicative f, f c ~ a) => b -> a -> a -> a
-  ite p t f = liftA2 (ite p) t f
+  ite p t f = ite p <$> t <*> f
 
 instance Iteable (Expr BoolSort) (Expr t) where
   ite = Ite

src/Language/Hasmtlib/Type/Solver.hs

@@ -147,7 +147,7 @@ solveMaximizedDebug :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderabl
   => (Solution -> IO ())
   -> Expr t
   -> m (Result, Solution)
-solveMaximizedDebug debug = solveOptimized (Just debug) (<?)
+solveMaximizedDebug debug = solveOptimized (Just debug) (>?)
 
 solveOptimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t)
   => Maybe (Solution -> IO ())

src/Language/Hasmtlib/Variable.hs

@@ -68,7 +68,7 @@ instance GVariable U1 where
   gvariable = return U1
 
 instance (GVariable f, GVariable g) => GVariable (f :*: g) where
-  gvariable = liftA2 (:*:) gvariable gvariable
+  gvariable = (:*:) <$> gvariable <*> gvariable
 
 instance GVariable f => GVariable (M1 i c f) where
   gvariable = M1 <$> gvariable