⬆️ Compatiblity with sbv-10.3

lsrcz · Jan 9, 2024 · cf2e6cb · cf2e6cb
1 parent 3861a79
commit cf2e6cb
Show file tree

Hide file tree

Showing 5 changed files with 28 additions and 11 deletions.
diff --git a/grisette.cabal b/grisette.cabal
@@ -154,9 +154,9 @@ library
     , mtl >=2.2.2 && <2.4
     , parallel >=3.2.2.0 && <3.3
     , prettyprinter >=1.5.0 && <1.8
-    , sbv >=8.11 && <10.3
+    , sbv >=8.11 && <10.4
     , stm ==2.5.*
-    , template-haskell >=2.16 && <2.21
+    , template-haskell >=2.16 && <2.22
     , text >=1.2.4.1 && <2.2
     , th-compat >=0.1.2 && <0.2
     , transformers >=0.5.6 && <0.7
@@ -193,9 +193,9 @@ test-suite doctest
     , mtl >=2.2.2 && <2.4
     , parallel >=3.2.2.0 && <3.3
     , prettyprinter >=1.5.0 && <1.8
-    , sbv >=8.11 && <10.3
+    , sbv >=8.11 && <10.4
     , stm ==2.5.*
-    , template-haskell >=2.16 && <2.21
+    , template-haskell >=2.16 && <2.22
     , text >=1.2.4.1 && <2.2
     , th-compat >=0.1.2 && <0.2
     , transformers >=0.5.6 && <0.7
@@ -276,9 +276,9 @@ test-suite spec
     , mtl >=2.2.2 && <2.4
     , parallel >=3.2.2.0 && <3.3
     , prettyprinter >=1.5.0 && <1.8
-    , sbv >=8.11 && <10.3
+    , sbv >=8.11 && <10.4
     , stm ==2.5.*
-    , template-haskell >=2.16 && <2.21
+    , template-haskell >=2.16 && <2.22
     , test-framework >=0.8.2 && <0.9
     , test-framework-hunit >=0.3.0.2 && <0.4
     , test-framework-quickcheck2 >=0.3.0.5 && <0.4

diff --git a/package.yaml b/package.yaml
@@ -36,13 +36,13 @@ dependencies:
   - generic-deriving >= 1.14.1 && < 1.15
   - bytestring >= 0.10.12 && < 0.13
   - unordered-containers >= 0.2.11 && < 0.3
-  - template-haskell >= 2.16 && < 2.21
+  - template-haskell >= 2.16 && < 2.22
   - deepseq >= 1.4.4 && < 1.6
   - hashtables >= 1.2.3.4 && < 1.4
   - loch-th >= 0.2.2 && < 0.3
   - th-compat >= 0.1.2 && < 0.2
   - array >= 0.5.4 && < 0.6
-  - sbv >= 8.11 && < 10.3
+  - sbv >= 8.11 && < 10.4
   - parallel >= 3.2.2.0 && < 3.3
   - text >= 1.2.4.1 && < 2.2
   - QuickCheck >= 2.14 && < 2.15

diff --git a/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs b/src/Grisette/Backend/SBV/Data/SMT/Lowering.hs
@@ -966,7 +966,16 @@ bvIsNonZeroFromGEq1 :: forall w r. (1 <= w) => ((SBV.BVIsNonZero w) => r) -> r
 bvIsNonZeroFromGEq1 r1 = case unsafeAxiom :: w :~: 1 of
   Refl -> r1
 
-#if MIN_VERSION_sbv(10,0,0)
+#if MIN_VERSION_sbv(10,3,0)
+preprocessUIFuncs ::
+  [(String, (Bool, SBVI.SBVType, Either String ([([SBVI.CV], SBVI.CV)], SBVI.CV)))] ->
+  Maybe [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))]
+preprocessUIFuncs =
+  traverse
+    (\case
+      (a, (_, b, Right c)) -> Just (a, (b, c))
+      _ -> Nothing)
+#elif MIN_VERSION_sbv(10,0,0)
 preprocessUIFuncs ::
   [(String, (SBVI.SBVType, Either String ([([SBVI.CV], SBVI.CV)], SBVI.CV)))] ->
   Maybe [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))]

diff --git a/stack-nightly.yaml b/stack-nightly.yaml
@@ -39,7 +39,8 @@ packages:
 # - git: https://github.com/commercialhaskell/stack.git
 #   commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
 #
-
+extra-deps:
+  - sbv-10.3
 # Override default flag values for local packages and extra-deps
 # flags: {}
 

diff --git a/stack-nightly.yaml.lock b/stack-nightly.yaml.lock
@@ -3,7 +3,14 @@
 # For more information, please see the documentation at:
 #   https://docs.haskellstack.org/en/stable/lock_files
 
-packages: []
+packages:
+- completed:
+    hackage: sbv-10.3@sha256:d869a49fd8e6303a81f7f704bb8669deff20d000e4644f93ddc64749d4bc0f9a,23712
+    pantry-tree:
+      sha256: 94cac2af8f8ac8f1a6cf8bbd37c679cdeff94d6034c074c670c20adf2e8c86dc
+      size: 72362
+  original:
+    hackage: sbv-10.3
 snapshots:
 - completed:
     sha256: b69a06c70e1092e2aa60ce69a4877c6181fbe53dfb7ea041cb98d97617d6007f