grisette 0.2.0.0 → 0.3.0.0

raw patch · 43 files changed

+1979/−583 lines, 43 filesdep −oncedep ~basedep ~doctestdep ~mtlPVP ok

version bump matches the API change (PVP)

Dependencies removed: once

Dependency ranges changed: base, doctest, mtl, parallel, sbv, template-haskell, transformers

API changes (from Hackage documentation)

Files

• CHANGELOG.md +42/−12
• LICENSE +1/−1
• README.md +33/−7
• grisette.cabal +29/−24
• src/Grisette/Backend/SBV/Data/SMT/Lowering.hs +52/−16
• src/Grisette/Backend/SBV/Data/SMT/Solving.hs +1/−0
• src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs +3/−3
• src/Grisette/Core.hs +2/−7
• src/Grisette/Core/Control/Monad/CBMCExcept.hs +5/−5
• src/Grisette/Core/Control/Monad/UnionM.hs +1/−3
• src/Grisette/Core/Data/BV.hs +90/−83
• src/Grisette/Core/Data/Class/BitVector.hs +46/−146
• src/Grisette/Core/Data/Class/Bool.hs +2/−2
• src/Grisette/Core/Data/Class/Evaluate.hs +6/−6
• src/Grisette/Core/Data/Class/GenSym.hs +85/−28
• src/Grisette/Core/Data/Class/Mergeable.hs +31/−12
• src/Grisette/Core/Data/Class/ModelOps.hs +3/−3
• src/Grisette/Core/Data/Class/SOrd.hs +1/−1
• src/Grisette/Core/Data/Class/SimpleMergeable.hs +4/−11
• src/Grisette/Core/Data/Class/SimpleMergeable.hs-boot +1/−1
• src/Grisette/Core/Data/Class/Solvable.hs +2/−2
• src/Grisette/Core/Data/Class/Substitute.hs +6/−6
• src/Grisette/Core/Data/Class/ToCon.hs +9/−9
• src/Grisette/Core/Data/Class/ToSym.hs +3/−3
• src/Grisette/Core/Data/Union.hs +1/−1
• src/Grisette/Experimental.hs +25/−0
• src/Grisette/Experimental/GenSymConstrained.hs +907/−0
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Caches.hs +11/−2
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs +51/−16
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs-boot +47/−16
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs +111/−39
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot +76/−23
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs +2/−0
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs +12/−0
• src/Grisette/IR/SymPrim/Data/Prim/Model.hs +4/−0
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/BV.hs +112/−29
• src/Grisette/IR/SymPrim/Data/Prim/Utils.hs +1/−1
• src/Grisette/IR/SymPrim/Data/SymPrim.hs +117/−43
• src/Grisette/Lib/Control/Monad/Trans/Cont.hs +2/−1
• src/Grisette/Utils/Parameterized.hs +8/−8
• test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs +8/−2
• test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs +20/−5
• test/Grisette/Core/Data/BVTests.hs +6/−6

@@ -1,27 +1,57 @@-# Changes+# Changelog -## Version 0.2.0.0+All notable changes to this project will be documented in this file. -### Feature-- Redesigned symbolic value interface.-  - `Sym Bool`/`Sym Integer`, etc., are no longer available and are replaced with `SymBool` and `SymInteger`. ([#41](https://github.com/lsrcz/grisette/pull/41))-  - New symbolic bit vector interface. Added unsized bit vector. ([#41](https://github.com/lsrcz/grisette/pull/41))+The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),+and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).++## [0.3.0.0] -- 2023-07-07++### Added+- Added the conversion between signed and unsigned bit vectors. ([#69](https://github.com/lsrcz/grisette/pull/69))+- Added the generation of `SomeSymIntN` and `SomeSymWordN` from a single `Int` for bit width. ([#73](https://github.com/lsrcz/grisette/pull/73))+- Added the `FiniteBits` instance for `SomeSymIntN` and `SomeSymWordN`. ([#83](https://github.com/lsrcz/grisette/pull/83))+- Added more flexible instances for symbolic generation for `Either`, `Maybe` and list types. ([#84](https://github.com/lsrcz/grisette/pull/84))+- Added an experimental `GenSymConstrained` type class. ([#89](https://github.com/lsrcz/grisette/pull/89))++### Changed+- Changed the operations for `SomeIntN` and `SomeWordN` to accepting dynamic runtime integers rather than compile-time integers. ([#71](https://github.com/lsrcz/grisette/pull/71))+- Comparing the equality of `SomeIntN`/`SomeWordN`/`SomeSymIntN`/`SomeSymWordN` with different bit widths returns false rather than crash now. ([#74](https://github.com/lsrcz/grisette/pull/74))++### Fixed+- Fixed the compatibility issue with sbv 10+. ([#66](https://github.com/lsrcz/grisette/pull/66))+- Fixed build error with newer GHC. ([#70](https://github.com/lsrcz/grisette/pull/70))+- Fixed the merging for `SomeSymIntN` and `SomeSymWordN`. ([#72](https://github.com/lsrcz/grisette/pull/72))++## [0.2.0.0] - 2023-04-13++### Added - Add term size count API. ([#48](https://github.com/lsrcz/grisette/pull/48), [#53](https://github.com/lsrcz/grisette/pull/53)) - Add timeout to solver interface. ([#49](https://github.com/lsrcz/grisette/pull/49), [#50](https://github.com/lsrcz/grisette/pull/50)) - Add parallel do-notation for parallel symbolic compilation. ([#51](https://github.com/lsrcz/grisette/pull/51))-- New safe operator interfaces. ([#56](https://github.com/lsrcz/grisette/pull/56))+- Added some missing instances for symbolic values and bit vectors. ([#46](https://github.com/lsrcz/grisette/pull/46), [#61](https://github.com/lsrcz/grisette/pull/61))+- Add missing instances for `MonadFresh` and `FreshT`. ([#59](https://github.com/lsrcz/grisette/pull/59)) +### Changed+- New safe operator interfaces. ([#56](https://github.com/lsrcz/grisette/pull/56))+- Redesigned symbolic value interface.+  - `Sym Bool`/`Sym Integer`, etc., are no longer available and are replaced with `SymBool` and `SymInteger`. ([#41](https://github.com/lsrcz/grisette/pull/41))+  - New symbolic bit vector interface. Added unsized bit vector. ([#41](https://github.com/lsrcz/grisette/pull/41)) -### Bugfix+### Removed - Dropped merging cache for `UnionM`. This fixed some segmentation fault errors. ([#43](https://github.com/lsrcz/grisette/pull/43))-- Added some missing instances for symbolic values and bit vectors. ([#46](https://github.com/lsrcz/grisette/pull/46), [#61](https://github.com/lsrcz/grisette/pull/61))++### Fixed - Fix CEGIS when no symbolic input is present. ([#52](https://github.com/lsrcz/grisette/pull/52)) - Fix overlapping `ToSym` and `ToCon` instances. ([#54](https://github.com/lsrcz/grisette/pull/54)) - Fix uninterpreted function lowering. ([#57](https://github.com/lsrcz/grisette/pull/57), [#58](https://github.com/lsrcz/grisette/pull/58))-- Add missing instances for `MonadFresh` and `FreshT`. ([#59](https://github.com/lsrcz/grisette/pull/59)) - Fix CEGIS crash when subsequent solver calls introduces new symbolic constant. ([#60](https://github.com/lsrcz/grisette/pull/60)) +## [0.1.0.0] - 2023-01-20 +### Added+- Initial release for Grisette. -## Version 0.1.0.0-Initial release.+[0.3.0.0]: https://github.com/lsrcz/grisette/compare/v0.2.0.0...v0.3.0.0+[0.2.0.0]: https://github.com/lsrcz/grisette/compare/v0.1.0.0...v0.2.0.0+[0.1.0.0]: https://github.com/lsrcz/grisette/tree/v0.1.0.0

@@ -1,4 +1,4 @@-Copyright (c) 2021-2022, Sirui Lu (siruilu@cs.washington.edu)+Copyright (c) 2021-2023, Sirui Lu (siruilu@cs.washington.edu)  All rights reserved. 

@@ -35,21 +35,47 @@ ### Install Grisette  Grisette is available via-[Hackage](https://hackage.haskell.org/package/grisette). You can install it with-`cabal`:+[Hackage](https://hackage.haskell.org/package/grisette). You can add it to your+project with `cabal`, and we also provided a stack template for quickly starting a+new project with Grisette. -```bash-$ cabal install grisette-```+#### Manually writing cabal file -However, Grisette is a library and is usually used as a dependency of other+Grisette is a library and is usually used as a dependency of other packages. You can add it to your project's `.cabal` file:  ```cabal library   ...-  build-depends: grisette >= 0.1 < 0.2+  build-depends: grisette >= 0.2 < 0.3 ```++#### Quick start template with `stack new`++You can quickly start an stack-based Grisette project with `stack new`:++```bash+$ stack new <projectname> github:lsrcz/grisette+```++You can specify the resolver version with the parameters:++```bash+$ stack new a-new-project github:lsrcz/grisette -p "resolver:lts-19.33"+```++For more details, please see the+[template file](https://github.com/lsrcz/stack-templates/blob/main/grisette.hsfiles) and the+[documentation for stack templates](https://docs.haskellstack.org/en/stable/templates_command/).++You can test your installation by running the following command:++```bash+$ stack run app+```++The command assumes a working [Z3](https://github.com/Z3Prover/z3) available+through `PATH`. You can install it with the instructions below.  ### Install SMT Solvers 

@@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.35.1.+-- This file has been generated from package.yaml by hpack version 0.35.2. -- -- see: https://github.com/sol/hpack  name:           grisette-version:        0.2.0.0+version:        0.3.0.0 synopsis:       Symbolic evaluation as a library description:    Grisette is a reusable symbolic evaluation library for Haskell. By                 translating programs into constraints, Grisette can help the development of@@ -24,6 +24,12 @@ license:        BSD3 license-file:   LICENSE build-type:     Simple+tested-with:+    GHC == 8.10.7+  , GHC == 9.0.2+  , GHC == 9.2.8+  , GHC == 9.4.5+  , GHC == 9.6.2 extra-source-files:     CHANGELOG.md     README.md@@ -75,6 +81,8 @@       Grisette.Core.Data.Union       Grisette.Core.TH       Grisette.Core.THCompat+      Grisette.Experimental+      Grisette.Experimental.GenSymConstrained       Grisette.Internal.Backend.SBV       Grisette.Internal.Core       Grisette.Internal.IR.SymPrim@@ -119,7 +127,7 @@       src   build-depends:       array >=0.5.4 && <0.6-    , base >4.14 && <5+    , base >=4.14 && <5     , bytestring >=0.10.12 && <0.12     , call-stack >=0.1 && <0.5     , deepseq >=1.4.4 && <1.5@@ -128,13 +136,12 @@     , hashtables >=1.2.3.4 && <1.4     , intern >=0.9.2 && <0.10     , loch-th >=0.2.2 && <0.3-    , mtl >=2.2.2 && <2.3-    , once >=0.2 && <0.5-    , parallel-    , sbv >=8.11 && <9.1-    , template-haskell >=2.16 && <2.20+    , mtl >=2.2.2 && <2.4+    , parallel >=3.2.2.0 && <3.3+    , sbv >=8.11 && <10.3+    , template-haskell >=2.16 && <2.21     , th-compat >=0.1.2 && <0.2-    , transformers >=0.5.6 && <0.6+    , transformers >=0.5.6 && <0.7     , unordered-containers >=0.2.11 && <0.3     , vector >=0.12.1 && <0.14   default-language: Haskell2010@@ -153,24 +160,23 @@   build-depends:       Glob     , array >=0.5.4 && <0.6-    , base >4.14 && <5+    , base >=4.14 && <5     , bytestring >=0.10.12 && <0.12     , call-stack >=0.1 && <0.5     , deepseq >=1.4.4 && <1.5-    , doctest >=0.18.2 && <0.21+    , doctest >=0.18.2 && <0.22     , generic-deriving >=1.14.1 && <1.15     , grisette     , hashable >=1.2.3 && <1.5     , hashtables >=1.2.3.4 && <1.4     , intern >=0.9.2 && <0.10     , loch-th >=0.2.2 && <0.3-    , mtl >=2.2.2 && <2.3-    , once >=0.2 && <0.5-    , parallel-    , sbv >=8.11 && <9.1-    , template-haskell >=2.16 && <2.20+    , mtl >=2.2.2 && <2.4+    , parallel >=3.2.2.0 && <3.3+    , sbv >=8.11 && <10.3+    , template-haskell >=2.16 && <2.21     , th-compat >=0.1.2 && <0.2-    , transformers >=0.5.6 && <0.6+    , transformers >=0.5.6 && <0.7     , unordered-containers >=0.2.11 && <0.3     , vector >=0.12.1 && <0.14   default-language: Haskell2010@@ -203,7 +209,7 @@       test   build-depends:       array >=0.5.4 && <0.6-    , base >4.14 && <5+    , base >=4.14 && <5     , bytestring >=0.10.12 && <0.12     , call-stack >=0.1 && <0.5     , deepseq >=1.4.4 && <1.5@@ -213,17 +219,16 @@     , hashtables >=1.2.3.4 && <1.4     , intern >=0.9.2 && <0.10     , loch-th >=0.2.2 && <0.3-    , mtl >=2.2.2 && <2.3-    , once >=0.2 && <0.5-    , parallel-    , sbv >=8.11 && <9.1+    , mtl >=2.2.2 && <2.4+    , parallel >=3.2.2.0 && <3.3+    , sbv >=8.11 && <10.3     , tasty >=1.1.0.3 && <1.5     , tasty-hunit ==0.10.*     , tasty-quickcheck >=0.10.1 && <0.11     , tasty-test-reporter >=0.1.1.2 && <0.2-    , template-haskell >=2.16 && <2.20+    , template-haskell >=2.16 && <2.21     , th-compat >=0.1.2 && <0.2-    , transformers >=0.5.6 && <0.6+    , transformers >=0.5.6 && <0.7     , unordered-containers >=0.2.11 && <0.3     , vector >=0.12.1 && <0.14   default-language: Haskell2010

@@ -1,4 +1,5 @@ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE CPP #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-}@@ -79,12 +80,12 @@   State SymBiMap () addResult tm sbvtm = modify $ addBiMapIntermediate (SomeTerm tm) (toDyn sbvtm) -translateTypeError :: HasCallStack => R.TypeRep a -> b+translateTypeError :: (HasCallStack) => R.TypeRep a -> b translateTypeError ta =   error $     "Don't know how to translate the type " ++ show ta ++ " to SMT" -translateUnaryError :: HasCallStack => String -> R.TypeRep a -> R.TypeRep b -> c+translateUnaryError :: (HasCallStack) => String -> R.TypeRep a -> R.TypeRep b -> c translateUnaryError op ta tb =   error $     "Don't know how to translate the op "@@ -95,7 +96,7 @@       ++ show tb       ++ " to SMT" -translateBinaryError :: HasCallStack => String -> R.TypeRep a -> R.TypeRep b -> R.TypeRep c -> d+translateBinaryError :: (HasCallStack) => String -> R.TypeRep a -> R.TypeRep b -> R.TypeRep c -> d translateBinaryError op ta tb tc =   error $     "Don't know how to translate the op "@@ -108,7 +109,7 @@       ++ show tc       ++ " to SMT" -translateTernaryError :: HasCallStack => String -> R.TypeRep a -> R.TypeRep b -> R.TypeRep c -> R.TypeRep d -> e+translateTernaryError :: (HasCallStack) => String -> R.TypeRep a -> R.TypeRep b -> R.TypeRep c -> R.TypeRep d -> e translateTernaryError op ta tb tc td =   error $     "Don't know how to translate the op "@@ -545,8 +546,8 @@     _ -> Nothing lowerSinglePrimUFun _ _ _ = error "Should not call this function" -class Monad m => SBVFreshMonad m where-  sbvFresh :: SBV.SymVal a => String -> m (SBV.SBV a)+class (Monad m) => SBVFreshMonad m where+  sbvFresh :: (SBV.SymVal a) => String -> m (SBV.SBV a)  instance SBVFreshMonad SBV.Symbolic where   sbvFresh = SBV.free@@ -710,6 +711,22 @@   case (config, R.typeRep @a) of     ResolvedBitsType -> lowerUnaryTerm config t arg (`rotate` n) m     _ -> translateBinaryError "rotate" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)+lowerSinglePrimImpl config t@(BVToSignedTerm _ (bv :: Term x)) m =+  case (R.typeRep @a, R.typeRep @x) of+    (SignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx)) ->+      case R.eqTypeRep (R.typeRep @na) (R.typeRep @nx) of+        Just R.HRefl ->+          lowerUnaryTerm config t bv SBV.sFromIntegral m+        _ -> translateUnaryError "bvu2s" (R.typeRep @x) (R.typeRep @a)+    _ -> translateUnaryError "bvu2s" (R.typeRep @x) (R.typeRep @a)+lowerSinglePrimImpl config t@(BVToUnsignedTerm _ (bv :: Term x)) m =+  case (R.typeRep @a, R.typeRep @x) of+    (UnsignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy nx)) ->+      case R.eqTypeRep (R.typeRep @na) (R.typeRep @nx) of+        Just R.HRefl ->+          lowerUnaryTerm config t bv SBV.sFromIntegral m+        _ -> translateUnaryError "bvs2u" (R.typeRep @x) (R.typeRep @a)+    _ -> translateUnaryError "bvs2u" (R.typeRep @x) (R.typeRep @a) lowerSinglePrimImpl config t@(BVConcatTerm _ (bv1 :: Term x) (bv2 :: Term y)) m =   case (R.typeRep @a, R.typeRep @x, R.typeRep @y) of     (UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx), UnsignedBVType (_ :: Proxy ny)) ->@@ -827,8 +844,27 @@ bvIsNonZeroFromGEq1 r1 = case unsafeAxiom :: w :~: 1 of   Refl -> r1 +#if 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)))]+preprocessUIFuncs =+  traverse+    (\case+      (a, (b, Right c)) -> Just (a, (b, c))+      _ -> Nothing)+#else+preprocessUIFuncs ::+  [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))] ->+  Maybe [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))]+preprocessUIFuncs = Just+#endif+ parseModel :: forall integerBitWidth. GrisetteSMTConfig integerBitWidth -> SBVI.SMTModel -> SymBiMap -> PM.Model-parseModel _ (SBVI.SMTModel _ _ assoc uifuncs) mp = foldr gouifuncs (foldr goassoc emptyModel assoc) uifuncs+parseModel _ (SBVI.SMTModel _ _ assoc orguifuncs) mp =+  case preprocessUIFuncs orguifuncs of+    Just uifuncs -> foldr gouifuncs (foldr goassoc emptyModel assoc) uifuncs+    _ -> error "SBV Failed to parse model"   where     goassoc :: (String, SBVI.CV) -> PM.Model -> PM.Model     goassoc (name, cv) m = case findStringToSymbol name mp of@@ -939,7 +975,7 @@     resolveFirst :: R.TypeRep a -> [([SBVI.CV], SBVI.CV)] -> [(a, [([SBVI.CV], SBVI.CV)])]     resolveFirst tf = fmap (\case (x : xs, v) -> (resolveSingle tf x, [(xs, v)]); _ -> error "impossible") -    partitionWithOrd :: forall a. Ord a => [(a, [([SBVI.CV], SBVI.CV)])] -> [(a, [([SBVI.CV], SBVI.CV)])]+    partitionWithOrd :: forall a. (Ord a) => [(a, [([SBVI.CV], SBVI.CV)])] -> [(a, [([SBVI.CV], SBVI.CV)])]     partitionWithOrd v = go sorted       where         sorted = sortWith fst v@@ -1485,7 +1521,7 @@   forall integerBitWidth.   () =>   forall s.-  ConfigConstraint integerBitWidth s =>+  (ConfigConstraint integerBitWidth s) =>   SBV.SMTConfig ->   GrisetteSMTConfig integerBitWidth pattern ResolvedConfig c <- (resolveConfigView -> DictConfig c)@@ -1522,7 +1558,7 @@ pattern ResolvedMergeableType ::   forall integerBitWidth s.   (SupportedPrim s) =>-  MergeableTypeConstraint integerBitWidth s =>+  (MergeableTypeConstraint integerBitWidth s) =>   (GrisetteSMTConfig integerBitWidth, R.TypeRep s) pattern ResolvedMergeableType <- (resolveMergeableTypeView -> Just DictMergeableType) @@ -1561,7 +1597,7 @@   forall integerBitWidth s.   (SupportedPrim s) =>   forall s'.-  SimpleTypeConstraint integerBitWidth s s' =>+  (SimpleTypeConstraint integerBitWidth s s') =>   (GrisetteSMTConfig integerBitWidth, R.TypeRep s) pattern ResolvedSimpleType <- (resolveSimpleTypeView -> Just DictSimpleType) @@ -1594,7 +1630,7 @@   forall integerBitWidth s.   (SupportedPrim s) =>   forall s'.-  DeepTypeConstraint integerBitWidth s s' =>+  (DeepTypeConstraint integerBitWidth s s') =>   (GrisetteSMTConfig integerBitWidth, R.TypeRep s) pattern ResolvedDeepType <- (resolveDeepTypeView -> Just DictDeepType) @@ -1623,7 +1659,7 @@   forall integerBitWidth s.   (SupportedPrim s) =>   forall s'.-  NumTypeConstraint integerBitWidth s s' =>+  (NumTypeConstraint integerBitWidth s s') =>   (GrisetteSMTConfig integerBitWidth, R.TypeRep s) pattern ResolvedNumType <- (resolveNumTypeView -> Just DictNumType) @@ -1651,7 +1687,7 @@   forall integerBitWidth s.   (SupportedPrim s) =>   forall s'.-  SDivisibleTypeConstraint integerBitWidth s s' =>+  (SDivisibleTypeConstraint integerBitWidth s s') =>   (GrisetteSMTConfig integerBitWidth, R.TypeRep s) pattern ResolvedSDivisibleType <- (resolveSDivisibleTypeView -> Just DictSDivisibleType) @@ -1680,7 +1716,7 @@   forall integerBitWidth s.   (SupportedPrim s) =>   forall s'.-  NumOrdTypeConstraint integerBitWidth s s' =>+  (NumOrdTypeConstraint integerBitWidth s s') =>   (GrisetteSMTConfig integerBitWidth, R.TypeRep s) pattern ResolvedNumOrdType <- (resolveNumOrdTypeView -> Just DictNumOrdType) @@ -1708,6 +1744,6 @@   forall integerBitWidth s.   (SupportedPrim s) =>   forall s'.-  BitsTypeConstraint integerBitWidth s s' =>+  (BitsTypeConstraint integerBitWidth s s') =>   (GrisetteSMTConfig integerBitWidth, R.TypeRep s) pattern ResolvedBitsType <- (resolveBitsTypeView -> Just DictBitsType)

@@ -40,6 +40,7 @@ import Control.DeepSeq import Control.Exception import Control.Monad.Except+import Control.Monad.IO.Class import qualified Data.HashSet as S import Data.Hashable import Data.Kind

@@ -37,14 +37,14 @@ sizeBiMap :: SymBiMap -> Int sizeBiMap = M.size . biMapToSBV -addBiMap :: HasCallStack => SomeTerm -> Dynamic -> String -> SomeTypedSymbol -> SymBiMap -> SymBiMap+addBiMap :: (HasCallStack) => SomeTerm -> Dynamic -> String -> SomeTypedSymbol -> SymBiMap -> SymBiMap addBiMap s d n sb (SymBiMap t f) = SymBiMap (M.insert s d t) (M.insert n sb f) -addBiMapIntermediate :: HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap+addBiMapIntermediate :: (HasCallStack) => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap addBiMapIntermediate s d (SymBiMap t f) = SymBiMap (M.insert s d t) f  findStringToSymbol :: String -> SymBiMap -> Maybe SomeTypedSymbol findStringToSymbol s (SymBiMap _ f) = M.lookup s f -lookupTerm :: HasCallStack => SomeTerm -> SymBiMap -> Maybe Dynamic+lookupTerm :: (HasCallStack) => SomeTerm -> SymBiMap -> Maybe Dynamic lookupTerm t m = M.lookup t (biMapToSBV m)

@@ -181,13 +181,8 @@     SEq (..),     SymBoolOp,     SOrd (..),-    SomeBV (..),-    someBVZext',-    someBVSext',-    someBVExt',-    someBVSelect',-    someBVExtract,-    someBVExtract',+    BV (..),+    bvExtract,     SizedBV (..),     sizedBVExtract,     SafeDivision (..),

@@ -161,7 +161,7 @@ mapCBMCExceptT f m = CBMCExceptT $ (unsafeCoerce . f . unsafeCoerce) (runCBMCExceptT m)  -- | Map the error in a 'CBMCExceptT'-withCBMCExceptT :: Functor m => (e -> e') -> CBMCExceptT e m a -> CBMCExceptT e' m a+withCBMCExceptT :: (Functor m) => (e -> e') -> CBMCExceptT e m a -> CBMCExceptT e' m a withCBMCExceptT f = mapCBMCExceptT $ fmap $ either (Left . f) Right  -- | Similar to 'ExceptT', but with different error handling mechanism.@@ -282,7 +282,7 @@   mzipWith f (CBMCExceptT a) (CBMCExceptT b) = CBMCExceptT $ mzipWith (liftA2 f) a b   {-# INLINE mzipWith #-} -instance Contravariant m => Contravariant (CBMCExceptT e m) where+instance (Contravariant m) => Contravariant (CBMCExceptT e m) where   contramap f = CBMCExceptT . contramap (fmap f) . runCBMCExceptT   {-# INLINE contramap #-} @@ -302,7 +302,7 @@     CBMCEither (Right r) -> return (CBMCEither . Right $ r) {-# INLINE catchE #-} -instance Monad m => OrigExcept.MonadError e (CBMCExceptT e m) where+instance (Monad m) => OrigExcept.MonadError e (CBMCExceptT e m) where   throwError = throwE   {-# INLINE throwError #-}   catchError = catchE@@ -406,13 +406,13 @@   symCompare (CBMCExceptT l) (CBMCExceptT r) = symCompare l r  instance-  ToCon (m1 (CBMCEither e1 a)) (m2 (CBMCEither e2 b)) =>+  (ToCon (m1 (CBMCEither e1 a)) (m2 (CBMCEither e2 b))) =>   ToCon (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b)   where   toCon (CBMCExceptT v) = CBMCExceptT <$> toCon v  instance-  ToCon (m1 (CBMCEither e1 a)) (Either e2 b) =>+  (ToCon (m1 (CBMCEither e1 a)) (Either e2 b)) =>   ToCon (CBMCExceptT e1 m1 a) (Either e2 b)   where   toCon (CBMCExceptT v) = toCon v

@@ -397,8 +397,6 @@ TO_SYM_FROM_UNION_CON_BV(WordN, SymWordN) TO_SYM_FROM_UNION_CON_FUN((=->), (=~>)) TO_SYM_FROM_UNION_CON_FUN((-->), (-~>))-TO_SYM_FROM_UNION_CON_BV_SOME(SomeIntN, SomeSymIntN)-TO_SYM_FROM_UNION_CON_BV_SOME(SomeWordN, SomeSymWordN) #endif  instance {-# INCOHERENT #-} (ToCon a b) => ToCon (UnionM a) b where@@ -543,7 +541,7 @@       go (If _ _ _ t f) = mrgIf <$> simpleFresh () <*> go t <*> go f  -- AllSyms-instance AllSyms a => AllSyms (UnionM a) where+instance (AllSyms a) => AllSyms (UnionM a) where   allSymsS = allSymsS . underlyingUnion  -- Concrete Key HashMaps

@@ -79,29 +79,29 @@ data SomeWordN where   SomeWordN :: (KnownNat n, 1 <= n) => WordN n -> SomeWordN -unarySomeWordN :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> r) -> SomeWordN -> r+unarySomeWordN :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> r) -> SomeWordN -> r unarySomeWordN op (SomeWordN (w :: WordN w)) = op w {-# INLINE unarySomeWordN #-} -unarySomeWordNR1 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n) -> SomeWordN -> SomeWordN+unarySomeWordNR1 :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n) -> SomeWordN -> SomeWordN unarySomeWordNR1 op (SomeWordN (w :: WordN w)) = SomeWordN $ op w {-# INLINE unarySomeWordNR1 #-} -binSomeWordN :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> r) -> SomeWordN -> SomeWordN -> r+binSomeWordN :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> r) -> SomeWordN -> SomeWordN -> r binSomeWordN op (SomeWordN (l :: WordN l)) (SomeWordN (r :: WordN r)) =   case sameNat (Proxy @l) (Proxy @r) of     Just Refl -> op l r     Nothing -> throw BitwidthMismatch {-# INLINE binSomeWordN #-} -binSomeWordNR1 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> WordN n) -> SomeWordN -> SomeWordN -> SomeWordN+binSomeWordNR1 :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> WordN n) -> SomeWordN -> SomeWordN -> SomeWordN binSomeWordNR1 op (SomeWordN (l :: WordN l)) (SomeWordN (r :: WordN r)) =   case sameNat (Proxy @l) (Proxy @r) of     Just Refl -> SomeWordN $ op l r     Nothing -> throw BitwidthMismatch {-# INLINE binSomeWordNR1 #-} -binSomeWordNR2 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> (WordN n, WordN n)) -> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)+binSomeWordNR2 :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> (WordN n, WordN n)) -> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN) binSomeWordNR2 op (SomeWordN (l :: WordN l)) (SomeWordN (r :: WordN r)) =   case sameNat (Proxy @l) (Proxy @r) of     Just Refl ->@@ -111,9 +111,15 @@ {-# INLINE binSomeWordNR2 #-}  instance Eq SomeWordN where-  (==) = binSomeWordN (==)+  SomeWordN (l :: WordN l) == SomeWordN (r :: WordN r) =+    case sameNat (Proxy @l) (Proxy @r) of+      Just Refl -> l == r+      Nothing -> False   {-# INLINE (==) #-}-  (/=) = binSomeWordN (/=)+  SomeWordN (l :: WordN l) /= SomeWordN (r :: WordN r) =+    case sameNat (Proxy @l) (Proxy @r) of+      Just Refl -> l /= r+      Nothing -> True   {-# INLINE (/=) #-}  instance Ord SomeWordN where@@ -150,7 +156,7 @@       binRepPre = "0b" ++ replicate (fromIntegral bitwidth - length binRep) '0'       binRep = showIntAtBase 2 (\x -> if x == 0 then '0' else '1') w "" -convertInt :: Num a => L.Lexeme -> ReadPrec a+convertInt :: (Num a) => L.Lexeme -> ReadPrec a convertInt (L.Number n)   | Just i <- L.numberToInteger n = return (fromInteger i) convertInt _ = pfail@@ -205,9 +211,15 @@ {-# INLINE binSomeIntNR2 #-}  instance Eq SomeIntN where-  (==) = binSomeIntN (==)+  SomeIntN (l :: IntN l) == SomeIntN (r :: IntN r) =+    case sameNat (Proxy @l) (Proxy @r) of+      Just Refl -> l == r+      Nothing -> False   {-# INLINE (==) #-}-  (/=) = binSomeIntN (/=)+  SomeIntN (l :: IntN l) /= SomeIntN (r :: IntN r) =+    case sameNat (Proxy @l) (Proxy @r) of+      Just Refl -> l /= r+      Nothing -> True   {-# INLINE (/=) #-}  instance Ord SomeIntN where@@ -270,8 +282,8 @@    -- complementBit use default implementation   testBit (WordN a) = testBit a-  bitSizeMaybe _ = Just $ fromIntegral (natVal (Proxy :: Proxy n))-  bitSize _ = fromIntegral (natVal (Proxy :: Proxy n))+  bitSizeMaybe = Just . finiteBitSize+  bitSize = finiteBitSize   isSigned _ = False   shiftL (WordN a) i = WordN (a `shiftL` i) .&. maxBound @@ -312,8 +324,8 @@   clearBit s i = unarySomeWordNR1 (`clearBit` i) s   complementBit s i = unarySomeWordNR1 (`complementBit` i) s   testBit s i = unarySomeWordN (`testBit` i) s-  bitSizeMaybe (SomeWordN (n :: WordN n)) = Just $ fromIntegral $ natVal n-  bitSize (SomeWordN (n :: WordN n)) = fromIntegral $ natVal n+  bitSizeMaybe = Just . finiteBitSize+  bitSize = finiteBitSize   isSigned _ = False   shiftL s i = unarySomeWordNR1 (`shiftL` i) s   unsafeShiftL s i = unarySomeWordNR1 (`unsafeShiftL` i) s@@ -405,7 +417,7 @@   signum = unarySomeWordNR1 signum   fromInteger = error "fromInteger is not defined for SomeWordN as no bitwidth is known" -minusOneIntN :: forall proxy n. KnownNat n => proxy n -> IntN n+minusOneIntN :: forall proxy n. (KnownNat n) => proxy n -> IntN n minusOneIntN _ = IntN (1 `shiftL` fromIntegral (natVal (Proxy :: Proxy n)) - 1)  instance (KnownNat n, 1 <= n) => Bits (IntN n) where@@ -424,8 +436,8 @@    -- complementBit use default implementation   testBit (IntN a) = testBit a-  bitSizeMaybe _ = Just $ fromIntegral (natVal (Proxy :: Proxy n))-  bitSize _ = fromIntegral (natVal (Proxy :: Proxy n))+  bitSizeMaybe = Just . finiteBitSize+  bitSize = finiteBitSize   isSigned _ = True    shiftL (IntN a) i = IntN (unWordN $ (WordN a :: WordN n) `shiftL` i)@@ -459,8 +471,8 @@   clearBit s i = unarySomeIntNR1 (`clearBit` i) s   complementBit s i = unarySomeIntNR1 (`complementBit` i) s   testBit s i = unarySomeIntN (`testBit` i) s-  bitSizeMaybe (SomeIntN (n :: IntN n)) = Just $ fromIntegral $ natVal n-  bitSize (SomeIntN (n :: IntN n)) = fromIntegral $ natVal n+  bitSizeMaybe = Just . finiteBitSize+  bitSize = finiteBitSize   isSigned _ = False   shiftL s i = unarySomeIntNR1 (`shiftL` i) s   unsafeShiftL s i = unarySomeIntNR1 (`unsafeShiftL` i) s@@ -596,10 +608,10 @@       noi = (1 :: Integer) `shiftL` l   sizedBVExt = sizedBVZext   sizedBVSelect ::-    forall n ix w proxy.+    forall n ix w p q.     (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) =>-    proxy ix ->-    proxy w ->+    p ix ->+    q w ->     WordN n ->     WordN w   sizedBVSelect pix pw (WordN v) = WordN ((v `shiftR` ix) .&. mask)@@ -616,76 +628,71 @@   sizedBVSext pr (IntN v) = IntN $ unWordN $ sizedBVSext pr (WordN v :: WordN l)   sizedBVExt = sizedBVSext   sizedBVSelect ::-    forall n ix w proxy.+    forall n ix w p q.     (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) =>-    proxy ix ->-    proxy w ->+    p ix ->+    q w ->     IntN n ->     IntN w   sizedBVSelect pix pw (IntN v) = IntN $ unWordN $ sizedBVSelect pix pw (WordN v :: WordN n) -instance SomeBV SomeWordN where-  someBVConcat (SomeWordN (a :: WordN l)) (SomeWordN (b :: WordN r)) =+instance BV SomeWordN where+  bvConcat (SomeWordN (a :: WordN l)) (SomeWordN (b :: WordN r)) =     case (leqAddPos (Proxy @l) (Proxy @r), knownAdd @l @r KnownProof KnownProof) of       (LeqProof, KnownProof) ->         SomeWordN $ sizedBVConcat a b-  someBVZext (p :: p l) (SomeWordN (a :: WordN n))-    | l < n = error "someBVZext: trying to zero extend a value to a smaller size"-    | otherwise =-        case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of-          (LeqProof, LeqProof) -> SomeWordN $ sizedBVZext p a+  {-# INLINE bvConcat #-}+  bvZext l (SomeWordN (a :: WordN n))+    | l < n = error "bvZext: trying to zero extend a value to a smaller size"+    | otherwise = res (Proxy @n)     where-      l = natVal p-      n = natVal (Proxy @n)-  someBVSext (p :: p l) (SomeWordN (a :: WordN n))-    | l < n = error "someBVSext: trying to zero extend a value to a smaller size"-    | otherwise =-        case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of-          (LeqProof, LeqProof) -> SomeWordN $ sizedBVSext p a+      n = fromIntegral $ natVal (Proxy @n)+      res :: forall (l :: Nat). Proxy l -> SomeWordN+      res p =+        case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of+          (KnownProof, LeqProof, LeqProof) -> SomeWordN $ sizedBVZext p a+  bvSext l (SomeWordN (a :: WordN n))+    | l < n = error "bvSext: trying to zero extend a value to a smaller size"+    | otherwise = res (Proxy @n)     where-      l = natVal p-      n = natVal (Proxy @n)-  someBVExt = someBVZext-  someBVSelect (p :: p ix) (q :: q w) (SomeWordN (a :: WordN n))-    | ix + w > n = error "someBVSelect: trying to select a bitvector outside the bounds of the input"-    | w == 0 = error "someBVSelect: trying to select a bitvector of size 0"-    | otherwise =-        case (unsafeLeqProof @1 @w, unsafeLeqProof @(ix + w) @n) of-          (LeqProof, LeqProof) -> SomeWordN $ sizedBVSelect (Proxy @ix) (Proxy @w) a+      n = fromIntegral $ natVal (Proxy @n)+      res :: forall (l :: Nat). Proxy l -> SomeWordN+      res p =+        case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of+          (KnownProof, LeqProof, LeqProof) -> SomeWordN $ sizedBVSext p a+  bvExt = bvZext+  bvSelect ix w (SomeWordN (a :: WordN n))+    | ix + w > n = error "bvSelect: trying to select a bitvector outside the bounds of the input"+    | w == 0 = error "bvSelect: trying to select a bitvector of size 0"+    | otherwise = res (Proxy @n) (Proxy @n)     where-      ix = natVal p-      w = natVal q-      n = natVal (Proxy @n)+      n = fromIntegral $ natVal (Proxy @n)+      res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeWordN+      res p1 p2 =+        case ( unsafeKnownProof @ix (fromIntegral ix),+               unsafeKnownProof @w (fromIntegral w),+               unsafeLeqProof @1 @w,+               unsafeLeqProof @(ix + w) @n+             ) of+          (KnownProof, KnownProof, LeqProof, LeqProof) ->+            SomeWordN $ sizedBVSelect (Proxy @ix) (Proxy @w) a -instance SomeBV SomeIntN where-  someBVConcat (SomeIntN (a :: IntN l)) (SomeIntN (b :: IntN r)) =-    case (leqAddPos (Proxy @l) (Proxy @r), knownAdd (KnownProof @l) (KnownProof @r)) of-      (LeqProof, KnownProof) ->-        SomeIntN $ sizedBVConcat a b-  someBVZext (p :: p l) (SomeIntN (a :: IntN n))-    | l < n = error "someBVZext: trying to zero extend a value to a smaller size"-    | otherwise =-        case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of-          (LeqProof, LeqProof) -> SomeIntN $ sizedBVZext p a-    where-      l = natVal p-      n = natVal (Proxy @n)-  someBVSext (p :: p l) (SomeIntN (a :: IntN n))-    | l < n = error "someBVSext: trying to zero extend a value to a smaller size"-    | otherwise =-        case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of-          (LeqProof, LeqProof) -> SomeIntN $ sizedBVSext p a-    where-      l = natVal p-      n = natVal (Proxy @n)-  someBVExt = someBVZext-  someBVSelect (p :: p ix) (q :: q w) (SomeIntN (a :: IntN n))-    | ix + w > n = error "someBVSelect: trying to select a bitvector outside the bounds of the input"-    | w == 0 = error "someBVSelect: trying to select a bitvector of size 0"-    | otherwise =-        case (unsafeLeqProof @1 @w, unsafeLeqProof @(ix + w) @n) of-          (LeqProof, LeqProof) -> SomeIntN $ sizedBVSelect (Proxy @ix) (Proxy @w) a-    where-      ix = natVal p-      w = natVal q-      n = natVal (Proxy @n)+instance BV SomeIntN where+  bvConcat l r = toSigned $ bvConcat (toUnsigned l) (toUnsigned l)+  {-# INLINE bvConcat #-}+  bvZext l = toSigned . bvZext l . toUnsigned+  {-# INLINE bvZext #-}+  bvSext l = toSigned . bvSext l . toUnsigned+  {-# INLINE bvSext #-}+  bvExt l = toSigned . bvExt l . toUnsigned+  {-# INLINE bvExt #-}+  bvSelect ix w = toSigned . bvSelect ix w . toUnsigned+  {-# INLINE bvSelect #-}++instance (KnownNat n, 1 <= n) => BVSignConversion (WordN n) (IntN n) where+  toSigned (WordN i) = IntN i+  toUnsigned (IntN i) = WordN i++instance BVSignConversion SomeWordN SomeIntN where+  toSigned (SomeWordN i) = SomeIntN $ toSigned i+  toUnsigned (SomeIntN i) = SomeWordN $ toUnsigned i

@@ -1,6 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-}@@ -19,15 +20,11 @@ -- Portability :   GHC only module Grisette.Core.Data.Class.BitVector   ( -- * Bit vector operations-    SomeBV (..),-    someBVZext',-    someBVSext',-    someBVExt',-    someBVSelect',-    someBVExtract,-    someBVExtract',+    BV (..),+    bvExtract,     SizedBV (..),     sizedBVExtract,+    BVSignConversion (..),   ) where @@ -45,38 +42,34 @@ -- >>> :set -XFlexibleInstances -- >>> :set -XFunctionalDependencies --- | Bit vector operations. Including concatenation ('someBVConcat'),--- extension ('someBVZext', 'someBVSext', 'someBVExt'), and selection--- ('someBVSelect').-class SomeBV bv where+-- | Bit vector operations. Including concatenation ('bvConcat'),+-- extension ('bvZext', 'bvSext', 'bvExt'), and selection+-- ('bvSelect').+class BV bv where   -- | Concatenation of two bit vectors.   ---  -- >>> someBVConcat (SomeSymWordN (0b101 :: SymWordN 3)) (SomeSymWordN (0b010 :: SymWordN 3))+  -- >>> bvConcat (SomeSymWordN (0b101 :: SymWordN 3)) (SomeSymWordN (0b010 :: SymWordN 3))   -- 0b101010-  someBVConcat :: bv -> bv -> bv+  bvConcat :: bv -> bv -> bv    -- | Zero extension of a bit vector.   ---  -- >>> someBVZext (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))+  -- >>> bvZext 6 (SomeSymWordN (0b101 :: SymWordN 3))   -- 0b000101-  someBVZext ::-    forall p l.-    KnownNat l =>+  bvZext ::     -- | Desired output length-    p l ->+    Int ->     -- | Bit vector to extend     bv ->     bv    -- | Sign extension of a bit vector.   ---  -- >>> someBVSext (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))+  -- >>> bvSext 6 (SomeSymWordN (0b101 :: SymWordN 3))   -- 0b111101-  someBVSext ::-    forall p l.-    KnownNat l =>+  bvSext ::     -- | Desired output length-    p l ->+    Int ->     -- | Bit vector to extend     bv ->     bv@@ -84,19 +77,17 @@   -- | Extension of a bit vector.   -- Signedness is determined by the input bit vector type.   ---  -- >>> someBVExt (Proxy @6) (SomeSymIntN (0b101 :: SymIntN 3))+  -- >>> bvExt 6 (SomeSymIntN (0b101 :: SymIntN 3))   -- 0b111101-  -- >>> someBVExt (Proxy @6) (SomeSymIntN (0b001 :: SymIntN 3))+  -- >>> bvExt 6 (SomeSymIntN (0b001 :: SymIntN 3))   -- 0b000001-  -- >>> someBVExt (Proxy @6) (SomeSymWordN (0b101 :: SymWordN 3))+  -- >>> bvExt 6 (SomeSymWordN (0b101 :: SymWordN 3))   -- 0b000101-  -- >>> someBVExt (Proxy @6) (SomeSymWordN (0b001 :: SymWordN 3))+  -- >>> bvExt 6 (SomeSymWordN (0b001 :: SymWordN 3))   -- 0b000001-  someBVExt ::-    forall p l.-    KnownNat l =>+  bvExt ::     -- | Desired output length-    p l ->+    Int ->     -- | Bit vector to extend     bv ->     bv@@ -106,136 +97,37 @@   --   -- The least significant bit is indexed as 0.   ---  -- >>> someBVSelect (Proxy @1) (Proxy @3) (SomeSymIntN (0b001010 :: SymIntN 6))+  -- >>> bvSelect 1 3 (SomeSymIntN (0b001010 :: SymIntN 6))   -- 0b101-  someBVSelect ::-    forall p ix q w.-    (KnownNat ix, KnownNat w) =>+  bvSelect ::     -- | Index of the least significant bit of the slice-    p ix ->+    Int ->     -- | Desired output width, @ix + w <= n@ must hold where @n@ is     -- the size of the input bit vector-    q w ->+    Int ->     -- | Bit vector to select from     bv ->     bv --- | Zero extension of a bit vector.------ >>> someBVZext' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))--- 0b000101-someBVZext' ::-  forall l bv.-  SomeBV bv =>-  -- | Desired output length-  NatRepr l ->-  -- | Bit vector to extend-  bv ->-  bv-someBVZext' p@(_ :: NatRepr l) = withKnownProof (hasRepr p) $ someBVZext (Proxy @l)-{-# INLINE someBVZext' #-}---- | Sign extension of a bit vector.------ >>> someBVSext' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))--- 0b111101-someBVSext' ::-  forall l bv.-  SomeBV bv =>-  NatRepr l ->-  -- | Desired output length-  bv ->-  -- | Bit vector to extend-  bv-someBVSext' p@(_ :: NatRepr l) = withKnownProof (hasRepr p) $ someBVSext (Proxy @l)-{-# INLINE someBVSext' #-}---- | Extension of a bit vector.--- Signedness is determined by the input bit vector type.------ >>> someBVExt' (natRepr @6) (SomeSymIntN (0b101 :: SymIntN 3))--- 0b111101--- >>> someBVExt' (natRepr @6) (SomeSymIntN (0b001 :: SymIntN 3))--- 0b000001--- >>> someBVExt' (natRepr @6) (SomeSymWordN (0b101 :: SymWordN 3))--- 0b000101--- >>> someBVExt' (natRepr @6) (SomeSymWordN (0b001 :: SymWordN 3))--- 0b000001-someBVExt' ::-  forall l bv.-  SomeBV bv =>-  -- | Desired output length-  NatRepr l ->-  -- | Bit vector to extend-  bv ->-  bv-someBVExt' p@(_ :: NatRepr l) = withKnownProof (hasRepr p) $ someBVExt (Proxy @l)-{-# INLINE someBVExt' #-}---- | Slicing out a smaller bit vector from a larger one,--- selecting a slice with width @w@ starting from index @ix@.------ The least significant bit is indexed as 0.------ >>> someBVSelect' (natRepr @1) (natRepr @3) (SomeSymIntN (0b001010 :: SymIntN 6))--- 0b101-someBVSelect' ::-  forall ix w bv.-  SomeBV bv =>-  -- | Index of the least significant bit of the slice-  NatRepr ix ->-  -- | Desired output width, @ix + w <= n@ must hold where @n@ is-  -- the size of the input bit vector-  NatRepr w ->-  -- | Bit vector to select from-  bv ->-  bv-someBVSelect' p@(_ :: NatRepr l) q@(_ :: NatRepr r) = withKnownProof (hasRepr p) $ withKnownProof (hasRepr q) $ someBVSelect p q-{-# INLINE someBVSelect' #-}- -- | Slicing out a smaller bit vector from a larger one, extract a slice from -- bit @i@ down to @j@. -- -- The least significant bit is indexed as 0. ----- >>> someBVExtract (Proxy @4) (Proxy @2) (SomeSymIntN (0b010100 :: SymIntN 6))--- 0b101-someBVExtract ::-  forall p (i :: Nat) q (j :: Nat) bv.-  (SomeBV bv, KnownNat i, KnownNat j) =>-  -- | The start position to extract from, @i < n@ must hold where @n@ is-  -- the size of the output bit vector-  p i ->-  -- | The end position to extract from, @j <= i@ must hold-  q j ->-  -- | Bit vector to extract from-  bv ->-  bv-someBVExtract _ _ =-  withKnownProof (unsafeKnownProof @(i - j + 1) (fromIntegral (natVal (Proxy @i)) - fromIntegral (natVal (Proxy @j)) + 1)) $-    someBVSelect (Proxy @j) (Proxy @(i - j + 1))-{-# INLINE someBVExtract #-}---- | Slicing out a smaller bit vector from a larger one, extract a slice from--- bit @i@ down to @j@.------ The least significant bit is indexed as 0.------ >>> someBVExtract' (natRepr @4) (natRepr @2) (SomeSymIntN (0b010100 :: SymIntN 6))+-- >>> bvExtract 4 2 (SomeSymIntN (0b010100 :: SymIntN 6)) -- 0b101-someBVExtract' ::-  forall (i :: Nat) (j :: Nat) bv.-  SomeBV bv =>+bvExtract ::+  (BV bv) =>   -- | The start position to extract from, @i < n@ must hold where @n@ is   -- the size of the output bit vector-  NatRepr i ->+  Int ->   -- | The end position to extract from, @j <= i@ must hold-  NatRepr j ->+  Int ->   -- | Bit vector to extract from   bv ->   bv-someBVExtract' p@(_ :: NatRepr l) q@(_ :: NatRepr r) = withKnownProof (hasRepr p) $ withKnownProof (hasRepr q) $ someBVExtract p q-{-# INLINE someBVExtract' #-}+bvExtract i j = bvSelect j (i - j + 1)+{-# INLINE bvExtract #-}  -- | Sized bit vector operations. Including concatenation ('sizedBVConcat'), -- extension ('sizedBVZext', 'sizedBVSext', 'sizedBVExt'), and selection@@ -300,10 +192,10 @@   sizedBVSelect ::     (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) =>     -- | Index of the least significant bit of the slice-    proxy ix ->+    p ix ->     -- | Desired output width, @ix + w <= n@ must hold where @n@ is     -- the size of the input bit vector-    proxy w ->+    q w ->     -- | Bit vector to select from     bv n ->     bv w@@ -316,13 +208,13 @@ -- >>> sizedBVExtract (Proxy @4) (Proxy @2) (con 0b010100 :: SymIntN 6) -- 0b101 sizedBVExtract ::-  forall proxy i j n bv.+  forall p i q j n bv.   (SizedBV bv, KnownNat n, KnownNat i, KnownNat j, 1 <= n, i + 1 <= n, j <= i) =>   -- | The start position to extract from, @i < n@ must hold where @n@ is   -- the size of the output bit vector-  proxy i ->+  p i ->   -- | The end position to extract from, @j <= i@ must hold-  proxy j ->+  q j ->   -- | Bit vector to extract from   bv n ->   bv (i - j + 1)@@ -334,3 +226,11 @@     (KnownProof, LeqProof, LeqProof) ->       sizedBVSelect (Proxy @j) (Proxy @(i - j + 1)) {-# INLINE sizedBVExtract #-}++-- | Convert bitvectors from and to signed+class BVSignConversion ubv sbv | ubv -> sbv, sbv -> ubv where+  -- | Convert unsigned bitvector to signed+  toSigned :: ubv -> sbv++  -- | Convert signed bitvector to unsigned+  toUnsigned :: sbv -> ubv

@@ -75,11 +75,11 @@   _ ==~~ _ = con True   {-# INLINE (==~~) #-} -instance SEq c => SEq' (K1 i c) where+instance (SEq c) => SEq' (K1 i c) where   (K1 a) ==~~ (K1 b) = a ==~ b   {-# INLINE (==~~) #-} -instance SEq' a => SEq' (M1 i c a) where+instance (SEq' a) => SEq' (M1 i c a) where   (M1 a) ==~~ (M1 b) = a ==~~ b   {-# INLINE (==~~) #-} 

@@ -78,10 +78,10 @@ instance EvaluateSym' U1 where   evaluateSym' _ _ = id -instance EvaluateSym c => EvaluateSym' (K1 i c) where+instance (EvaluateSym c) => EvaluateSym' (K1 i c) where   evaluateSym' fillDefault model (K1 v) = K1 $ evaluateSym fillDefault model v -instance EvaluateSym' a => EvaluateSym' (M1 i c a) where+instance (EvaluateSym' a) => EvaluateSym' (M1 i c a) where   evaluateSym' fillDefault model (M1 v) = M1 $ evaluateSym' fillDefault model v  instance (EvaluateSym' a, EvaluateSym' b) => EvaluateSym' (a :+: b) where@@ -214,16 +214,16 @@     (EvaluateSym (f a), EvaluateSym (g a)) => EvaluateSym (Sum f g a)  -- WriterT-instance EvaluateSym (m (a, s)) => EvaluateSym (WriterLazy.WriterT s m a) where+instance (EvaluateSym (m (a, s))) => EvaluateSym (WriterLazy.WriterT s m a) where   evaluateSym fillDefault model (WriterLazy.WriterT v) = WriterLazy.WriterT $ evaluateSym fillDefault model v -instance EvaluateSym (m (a, s)) => EvaluateSym (WriterStrict.WriterT s m a) where+instance (EvaluateSym (m (a, s))) => EvaluateSym (WriterStrict.WriterT s m a) where   evaluateSym fillDefault model (WriterStrict.WriterT v) = WriterStrict.WriterT $ evaluateSym fillDefault model v  -- Identity-instance EvaluateSym a => EvaluateSym (Identity a) where+instance (EvaluateSym a) => EvaluateSym (Identity a) where   evaluateSym fillDefault model (Identity a) = Identity $ evaluateSym fillDefault model a  -- IdentityT-instance EvaluateSym (m a) => EvaluateSym (IdentityT m a) where+instance (EvaluateSym (m a)) => EvaluateSym (IdentityT m a) where   evaluateSym fillDefault model (IdentityT a) = IdentityT $ evaluateSym fillDefault model a

@@ -6,6 +6,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE QuantifiedConstraints #-}@@ -99,6 +100,7 @@ import Grisette.Core.Data.Class.Solvable import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim+import Grisette.Utils import Language.Haskell.TH.Syntax hiding (lift)  -- $setup@@ -219,7 +221,7 @@ -- -- The monad should be a reader monad for the 'FreshIdent' and a state monad for -- the 'FreshIndex'.-class Monad m => MonadFresh m where+class (Monad m) => MonadFresh m where   -- | Increase the index by one and return the new index.   nextFreshIndex :: m FreshIndex @@ -355,7 +357,7 @@ runFresh :: Fresh a -> FreshIdent -> a runFresh m ident = runIdentity $ runFreshT m ident -instance Monad m => MonadFresh (FreshT m) where+instance (Monad m) => MonadFresh (FreshT m) where   nextFreshIndex = FreshT $ \_ idx -> return (idx, idx + 1)   getFreshIdent = FreshT $ curry return @@ -388,7 +390,7 @@   -- is ensured. No specification is needed.   --   -- >>> runFresh (fresh ()) "a" :: UnionM (Maybe Bool)-  -- {If a@0 Nothing (If a@1 (Just False) (Just True))}+  -- {If a@1 Nothing (If a@0 (Just False) (Just True))}   --   -- The following example generates lists of symbolic booleans with length 1 to 2.   --@@ -807,20 +809,23 @@  -- Either instance-  ( GenSymSimple a a,+  ( GenSym aspec a,     Mergeable a,-    GenSymSimple b b,+    GenSym bspec b,     Mergeable b   ) =>-  GenSym (Either a b) (Either a b)+  GenSym (Either aspec bspec) (Either a b)+  where+  fresh (Left aspec) = (merge . fmap Left) <$> fresh aspec+  fresh (Right bspec) = (merge . fmap Right) <$> fresh bspec  instance-  ( GenSymSimple a a,-    GenSymSimple b b+  ( GenSymSimple aspec a,+    GenSymSimple bspec b   ) =>-  GenSymSimple (Either a b) (Either a b)+  GenSymSimple (Either aspec bspec) (Either a b)   where-  simpleFresh = derivedSameShapeSimpleFresh+  simpleFresh (Left a) = Left <$> simpleFresh a  instance   (GenSym () a, Mergeable a, GenSym () b, Mergeable b) =>@@ -828,35 +833,54 @@   where   fresh = derivedNoSpecFresh +instance+  ( GenSym aspec a,+    Mergeable a,+    GenSym bspec b,+    Mergeable b+  ) =>+  GenSym (aspec, bspec) (Either a b)+  where+  fresh (aspec, bspec) = do+    l :: UnionM a <- fresh aspec+    r :: UnionM b <- fresh bspec+    chooseUnionFresh [Left <$> l, Right <$> r]+ -- Maybe instance-  (GenSymSimple a a, Mergeable a) =>-  GenSym (Maybe a) (Maybe a)+  (GenSym aspec a, Mergeable a) =>+  GenSym (Maybe aspec) (Maybe a)+  where+  fresh Nothing = return $ mrgSingle Nothing+  fresh (Just aspec) = (merge . fmap Just) <$> fresh aspec  instance-  (GenSymSimple a a) =>-  GenSymSimple (Maybe a) (Maybe a)+  (GenSymSimple aspec a) =>+  GenSymSimple (Maybe aspec) (Maybe a)   where-  simpleFresh = derivedSameShapeSimpleFresh+  simpleFresh Nothing = return Nothing+  simpleFresh (Just aspec) = Just <$> simpleFresh aspec -instance (GenSym () a, Mergeable a) => GenSym () (Maybe a) where-  fresh = derivedNoSpecFresh+instance (GenSym aspec a, Mergeable a) => GenSym aspec (Maybe a) where+  fresh aspec = do+    a :: UnionM a <- fresh aspec+    chooseUnionFresh [return Nothing, Just <$> a]  -- List instance-  (GenSymSimple () a, Mergeable a) =>+  (GenSym () a, Mergeable a) =>   GenSym Integer [a]   where   fresh v = do     l <- gl v     let xs = reverse $ scanr (:) [] l-    chooseFresh xs+    chooseUnionFresh $ merge . sequence <$> xs     where-      gl :: (MonadFresh m) => Integer -> m [a]+      gl :: (MonadFresh m) => Integer -> m [UnionM a]       gl v1         | v1 <= 0 = return []         | otherwise = do-            l <- simpleFresh ()+            l <- fresh ()             r <- gl (v1 - 1)             return $ l : r @@ -878,7 +902,7 @@   deriving (Show)  instance-  (GenSymSimple spec a, Mergeable a) =>+  (GenSym spec a, Mergeable a) =>   GenSym (ListSpec spec) [a]   where   fresh (ListSpec minLen maxLen subSpec) =@@ -887,19 +911,23 @@       else do         l <- gl maxLen         let xs = drop minLen $ reverse $ scanr (:) [] l-        chooseFresh xs+        chooseUnionFresh $ merge . sequence <$> xs     where-      gl :: (MonadFresh m) => Int -> m [a]+      gl :: (MonadFresh m) => Int -> m [UnionM a]       gl currLen         | currLen <= 0 = return []         | otherwise = do-            l <- simpleFresh subSpec+            l <- fresh subSpec             r <- gl (currLen - 1)             return $ l : r  instance-  (GenSymSimple a a, Mergeable a) =>+  (GenSym a a, Mergeable a) =>   GenSym [a] [a]+  where+  fresh l = do+    r :: [UnionM a] <- traverse fresh l+    return $ merge $ sequence r  instance   (GenSymSimple a a) =>@@ -920,10 +948,22 @@   deriving (Show)  instance-  (GenSymSimple spec a, Mergeable a) =>+  (GenSym spec a, Mergeable a) =>   GenSym (SimpleListSpec spec) [a]   where-  fresh = fmap mrgSingle . simpleFresh+  fresh (SimpleListSpec len subSpec) =+    if len < 0+      then error $ "Bad lengths: " ++ show len+      else do+        merge . sequence <$> gl len+    where+      gl :: (MonadFresh m) => Int -> m [UnionM a]+      gl currLen+        | currLen <= 0 = return []+        | otherwise = do+            l <- fresh subSpec+            r <- gl (currLen - 1)+            return $ l : r  instance   (GenSymSimple spec a) =>@@ -1579,6 +1619,19 @@   simpleFresh _ = do; \     i :: origtype n <- simpleFresh (); \     return $ symtype i+#define GENSYM_N_INT_BV_SOME(symtype) \+instance GenSym Int symtype where \+  fresh p = mrgSingle <$> simpleFresh p+#define GENSYM_N_INT_SIMPLE_BV_SOME(symtype, origtype) \+instance GenSymSimple Int symtype where \+  simpleFresh i = if i > 0 then f (Proxy @0) else \+    error "Can only generate bit vectors with positive bit size" \+    where \+      f :: forall p (n :: Nat) m. (MonadFresh m) => p n -> m symtype; \+      f p = case (unsafeKnownProof @n (fromIntegral i), unsafeLeqProof @1 @n) of \+        (KnownProof, LeqProof) -> do \+        v :: origtype n <- simpleFresh (); \+        return $ symtype v; \  #define GENSYM_FUN(op) \ instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => GenSym (sa op sb) (sa op sb)@@ -1620,10 +1673,14 @@ GENSYM_SIMPLE_BV_SOME(SomeSymIntN) GENSYM_N_BV_SOME(SomeSymIntN) GENSYM_N_SIMPLE_BV_SOME(SomeSymIntN, SymIntN)+GENSYM_N_INT_BV_SOME(SomeSymIntN)+GENSYM_N_INT_SIMPLE_BV_SOME(SomeSymIntN, SymIntN) GENSYM_BV_SOME(SomeSymWordN) GENSYM_SIMPLE_BV_SOME(SomeSymWordN) GENSYM_N_BV_SOME(SomeSymWordN) GENSYM_N_SIMPLE_BV_SOME(SomeSymWordN, SymWordN)+GENSYM_N_INT_BV_SOME(SomeSymWordN)+GENSYM_N_INT_SIMPLE_BV_SOME(SomeSymWordN, SymWordN)  GENSYM_FUN(=~>) GENSYM_SIMPLE_FUN(=~>)

@@ -78,6 +78,7 @@ import Grisette.Core.Data.Class.Bool import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim+import Grisette.Utils import Unsafe.Coerce  -- | Helper type for combining arbitrary number of indices into one.@@ -322,15 +323,15 @@   liftRootStrategy' m = wrapStrategy m Par1 unPar1   {-# INLINE liftRootStrategy' #-} -instance Mergeable1 f => Mergeable1' (Rec1 f) where+instance (Mergeable1 f) => Mergeable1' (Rec1 f) where   liftRootStrategy' m = wrapStrategy (liftRootStrategy m) Rec1 unRec1   {-# INLINE liftRootStrategy' #-} -instance Mergeable c => Mergeable1' (K1 i c) where+instance (Mergeable c) => Mergeable1' (K1 i c) where   liftRootStrategy' _ = wrapStrategy rootStrategy K1 unK1   {-# INLINE liftRootStrategy' #-} -instance Mergeable1' a => Mergeable1' (M1 i c a) where+instance (Mergeable1' a) => Mergeable1' (M1 i c a) where   liftRootStrategy' m = wrapStrategy (liftRootStrategy' m) M1 unM1   {-# INLINE liftRootStrategy' #-} @@ -529,15 +530,15 @@     strategies = snd <$> r {-# INLINE buildStrategyList #-} -instance Eq1 container => Eq (StrategyList container) where+instance (Eq1 container) => Eq (StrategyList container) where   (StrategyList idxs1 _) == (StrategyList idxs2 _) = eq1 idxs1 idxs2   {-# INLINE (==) #-} -instance Ord1 container => Ord (StrategyList container) where+instance (Ord1 container) => Ord (StrategyList container) where   compare (StrategyList idxs1 _) (StrategyList idxs2 _) = compare1 idxs1 idxs2   {-# INLINE compare #-} -instance Show1 container => Show (StrategyList container) where+instance (Show1 container) => Show (StrategyList container) where   showsPrec i (StrategyList idxs1 _) = showsPrec1 i idxs1  -- List@@ -975,10 +976,6 @@ instance (KnownNat n, 1 <= n) => Mergeable (symtype n) where \   rootStrategy = SimpleStrategy ites -#define MERGEABLE_BV_SOME(symtype) \-instance Mergeable symtype where \-  rootStrategy = SimpleStrategy ites- #define MERGEABLE_FUN(op) \ instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Mergeable (sa op sb) where \   rootStrategy = SimpleStrategy ites@@ -988,11 +985,33 @@ MERGEABLE_SIMPLE(SymInteger) MERGEABLE_BV(SymIntN) MERGEABLE_BV(SymWordN)-MERGEABLE_BV_SOME(SomeSymIntN)-MERGEABLE_BV_SOME(SomeSymWordN) MERGEABLE_FUN(=~>) MERGEABLE_FUN(-~>) #endif++instance Mergeable SomeSymIntN where+  rootStrategy =+    SortedStrategy @Natural+      (\(SomeSymIntN (v :: SymIntN n)) -> natVal (Proxy @n))+      ( \n ->+          SimpleStrategy+            ( \c (SomeSymIntN (l :: SymIntN l)) (SomeSymIntN (r :: SymIntN r)) ->+                case unsafeAxiom @l @r of+                  Refl -> SomeSymIntN $ ites c l r+            )+      )++instance Mergeable SomeSymWordN where+  rootStrategy =+    SortedStrategy @Natural+      (\(SomeSymWordN (v :: SymWordN n)) -> natVal (Proxy @n))+      ( \n ->+          SimpleStrategy+            ( \c (SomeSymWordN (l :: SymWordN l)) (SomeSymWordN (r :: SymWordN r)) ->+                case unsafeAxiom @l @r of+                  Refl -> SomeSymWordN $ ites c l r+            )+      )  -- Exceptions instance Mergeable ArithException where

@@ -56,7 +56,7 @@ -- >>> differenceSet abSet acSet -- SymbolSet {b :: Bool} class-  Monoid symbolSet =>+  (Monoid symbolSet) =>   SymbolSetOps symbolSet (typedSymbol :: Type -> Type)     | symbolSet -> typedSymbol   where@@ -87,7 +87,7 @@ -- >>> buildSymbolSet ("a" :: TypedSymbol Bool, "b" :: TypedSymbol Bool) :: SymbolSet -- SymbolSet {a :: Bool, b :: Bool} class-  SymbolSetOps symbolSet typedSymbol =>+  (SymbolSetOps symbolSet typedSymbol) =>   SymbolSetRep rep symbolSet (typedSymbol :: * -> *)   where   -- | Build a symbolic constant set@@ -120,7 +120,7 @@ -- >>> exact acSet abModel -- Model {a -> True :: Bool, c -> False :: Bool} class-  SymbolSetOps symbolSet typedSymbol =>+  (SymbolSetOps symbolSet typedSymbol) =>   ModelOps model symbolSet typedSymbol     | model -> symbolSet typedSymbol   where

@@ -279,7 +279,7 @@   (>~) = symCompareSingleList False True   symCompare = symCompareList -deriving via (Default (Maybe a)) instance SOrd a => SOrd (Maybe a)+deriving via (Default (Maybe a)) instance (SOrd a) => SOrd (Maybe a)  deriving via (Default (Either a b)) instance (SOrd a, SOrd b) => SOrd (Either a b) 

@@ -104,7 +104,7 @@ -- > data X = ... -- >   deriving Generic -- >   deriving (Mergeable, SimpleMergeable) via (Default X)-class Mergeable a => SimpleMergeable a where+class (Mergeable a) => SimpleMergeable a where   -- | Performs if-then-else with the simple root merge strategy.   --   -- >>> mrgIte "a" "b" "c" :: SymInteger@@ -359,7 +359,7 @@     )   {-# INLINE mrgIte #-} -instance SimpleMergeable b => SimpleMergeable (a -> b) where+instance (SimpleMergeable b) => SimpleMergeable (a -> b) where   mrgIte = mrgIte1   {-# INLINE mrgIte #-} @@ -694,7 +694,7 @@ -- -- >>> case (single 1 :: UnionM Integer) of SingleU v -> v -- 1-pattern SingleU :: UnionPrjOp u => a -> u a+pattern SingleU :: (UnionPrjOp u) => a -> u a pattern SingleU x <-   (singleView -> Just x)   where@@ -703,7 +703,7 @@ -- | Pattern match to extract guard values with 'ifView' -- >>> case (unionIf "a" (single 1) (single 2) :: UnionM Integer) of IfU c t f -> (c,t,f) -- (a,<1>,<2>)-pattern IfU :: UnionPrjOp u => SymBool -> u a -> u a -> u a+pattern IfU :: (UnionPrjOp u) => SymBool -> u a -> u a -> u a pattern IfU c t f <-   (ifView -> Just (c, t, f))   where@@ -785,11 +785,6 @@   mrgIte = ites; \   {-# INLINE mrgIte #-} -#define SIMPLE_MERGEABLE_SOME_BV(symtype, bf) \-instance SimpleMergeable symtype where \-  mrgIte c = bf (ites c) "mrgIte"; \-  {-# INLINE mrgIte #-}- #define SIMPLE_MERGEABLE_FUN(op) \ instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => SimpleMergeable (sa op sb) where \   mrgIte = ites; \@@ -800,8 +795,6 @@ SIMPLE_MERGEABLE_SIMPLE(SymInteger) SIMPLE_MERGEABLE_BV(SymIntN) SIMPLE_MERGEABLE_BV(SymWordN)-SIMPLE_MERGEABLE_SOME_BV(SomeSymIntN, binSomeSymIntNR1)-SIMPLE_MERGEABLE_SOME_BV(SomeSymWordN, binSomeSymWordNR1) SIMPLE_MERGEABLE_FUN(=~>) SIMPLE_MERGEABLE_FUN(-~>) #endif

@@ -6,5 +6,5 @@ import {-# SOURCE #-} Grisette.Core.Data.Class.Mergeable import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim -class Mergeable a => SimpleMergeable a where+class (Mergeable a) => SimpleMergeable a where   mrgIte :: SymBool -> a -> a -> a

@@ -30,7 +30,7 @@  -- | The class defines the creation and pattern matching of solvable type -- values.-class IsString t => Solvable c t | t -> c where+class (IsString t) => Solvable c t | t -> c where   -- | Wrap a concrete value in a symbolic value.   --   -- >>> con True :: SymBool@@ -95,7 +95,7 @@ -- -- >>> case con True :: SymBool of Con v -> v -- True-pattern Con :: Solvable c t => c -> t+pattern Con :: (Solvable c t) => c -> t pattern Con c <-   (conView -> Just c)   where

@@ -63,12 +63,12 @@   --   -- >>> substituteSym "a" ("c" &&~ "d" :: Sym Bool) ["a" &&~ "b" :: Sym Bool, "a"]   -- [(&& (&& c d) b),(&& c d)]-  substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> a -> a+  substituteSym :: (LinkedRep cb sb) => TypedSymbol cb -> sb -> a -> a  -- | Auxiliary class for 'SubstituteSym' instance derivation class SubstituteSym' a where   -- | Auxiliary function for 'substituteSym' derivation-  substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> a c -> a c+  substituteSym' :: (LinkedRep cb sb) => TypedSymbol cb -> sb -> a c -> a c  instance   ( Generic a,@@ -81,10 +81,10 @@ instance SubstituteSym' U1 where   substituteSym' _ _ = id -instance SubstituteSym c => SubstituteSym' (K1 i c) where+instance (SubstituteSym c) => SubstituteSym' (K1 i c) where   substituteSym' sym val (K1 v) = K1 $ substituteSym sym val v -instance SubstituteSym' a => SubstituteSym' (M1 i c a) where+instance (SubstituteSym' a) => SubstituteSym' (M1 i c a) where   substituteSym' sym val (M1 v) = M1 $ substituteSym' sym val v  instance (SubstituteSym' a, SubstituteSym' b) => SubstituteSym' (a :+: b) where@@ -258,11 +258,11 @@   substituteSym sym val (WriterStrict.WriterT v) = WriterStrict.WriterT $ substituteSym sym val v  -- Identity-instance SubstituteSym a => SubstituteSym (Identity a) where+instance (SubstituteSym a) => SubstituteSym (Identity a) where   substituteSym sym val (Identity a) = Identity $ substituteSym sym val a  -- IdentityT-instance SubstituteSym (m a) => SubstituteSym (IdentityT m a) where+instance (SubstituteSym (m a)) => SubstituteSym (IdentityT m a) where   substituteSym sym val (IdentityT a) = IdentityT $ substituteSym sym val a  {-

@@ -72,10 +72,10 @@ instance ToCon' U1 U1 where   toCon' = Just -instance ToCon a b => ToCon' (K1 i a) (K1 i b) where+instance (ToCon a b) => ToCon' (K1 i a) (K1 i b) where   toCon' (K1 a) = K1 <$> toCon a -instance ToCon' a b => ToCon' (M1 i c1 a) (M1 i c2 b) where+instance (ToCon' a b) => ToCon' (M1 i c1 a) (M1 i c2 b) where   toCon' (M1 a) = M1 <$> toCon' a  instance (ToCon' a1 a2, ToCon' b1 b2) => ToCon' (a1 :+: b1) (a2 :+: b2) where@@ -172,20 +172,20 @@  -- MaybeT instance-  ToCon (m1 (Maybe a)) (m2 (Maybe b)) =>+  (ToCon (m1 (Maybe a)) (m2 (Maybe b))) =>   ToCon (MaybeT m1 a) (MaybeT m2 b)   where   toCon (MaybeT v) = MaybeT <$> toCon v  -- ExceptT instance-  ToCon (m1 (Either e1 a)) (m2 (Either e2 b)) =>+  (ToCon (m1 (Either e1 a)) (m2 (Either e2 b))) =>   ToCon (ExceptT e1 m1 a) (ExceptT e2 m2 b)   where   toCon (ExceptT v) = ExceptT <$> toCon v  instance-  ToCon (m1 (Either e1 a)) (Either e2 b) =>+  (ToCon (m1 (Either e1 a)) (Either e2 b)) =>   ToCon (ExceptT e1 m1 a) (Either e2 b)   where   toCon (ExceptT v) = toCon v@@ -198,19 +198,19 @@  -- WriterT instance-  ToCon (m1 (a, s1)) (m2 (b, s2)) =>+  (ToCon (m1 (a, s1)) (m2 (b, s2))) =>   ToCon (WriterLazy.WriterT s1 m1 a) (WriterLazy.WriterT s2 m2 b)   where   toCon (WriterLazy.WriterT v) = WriterLazy.WriterT <$> toCon v  instance-  ToCon (m1 (a, s1)) (m2 (b, s2)) =>+  (ToCon (m1 (a, s1)) (m2 (b, s2))) =>   ToCon (WriterStrict.WriterT s1 m1 a) (WriterStrict.WriterT s2 m2 b)   where   toCon (WriterStrict.WriterT v) = WriterStrict.WriterT <$> toCon v  -- Identity-instance ToCon a b => ToCon (Identity a) (Identity b) where+instance (ToCon a b) => ToCon (Identity a) (Identity b) where   toCon (Identity a) = Identity <$> toCon a  instance ToCon (Identity v) v where@@ -220,5 +220,5 @@   toCon = Just . Identity  -- IdentityT-instance ToCon (m a) (m1 b) => ToCon (IdentityT m a) (IdentityT m1 b) where+instance (ToCon (m a) (m1 b)) => ToCon (IdentityT m a) (IdentityT m1 b) where   toCon (IdentityT a) = IdentityT <$> toCon a

@@ -113,7 +113,7 @@ deriving via (Default (Either e2 a2)) instance (ToSym e1 e2, ToSym a1 a2) => ToSym (Either e1 a1) (Either e2 a2)  -- Maybe-deriving via (Default (Maybe b)) instance ToSym a b => ToSym (Maybe a) (Maybe b)+deriving via (Default (Maybe b)) instance (ToSym a b) => ToSym (Maybe a) (Maybe b)  -- List deriving via (Default [b]) instance (ToSym a b) => ToSym [a] [b]@@ -201,9 +201,9 @@     (ToSym (f a) (f1 a1), ToSym (g a) (g1 a1)) => ToSym (Sum f g a) (Sum f1 g1 a1)  -- Identity-instance ToSym a b => ToSym (Identity a) (Identity b) where+instance (ToSym a b) => ToSym (Identity a) (Identity b) where   toSym (Identity a) = Identity $ toSym a  -- IdentityT-instance ToSym (m a) (m1 b) => ToSym (IdentityT m a) (IdentityT m1 b) where+instance (ToSym (m a) (m1 b)) => ToSym (IdentityT m a) (IdentityT m1 b) where   toSym (IdentityT v) = IdentityT $ toSym v

@@ -128,7 +128,7 @@   s `hashWithSalt` (Single a) = s `hashWithSalt` (0 :: Int) `hashWithSalt` a   s `hashWithSalt` (If _ _ c l r) = s `hashWithSalt` (1 :: Int) `hashWithSalt` c `hashWithSalt` l `hashWithSalt` r -instance AllSyms a => AllSyms (Union a) where+instance (AllSyms a) => AllSyms (Union a) where   allSymsS (Single v) = allSymsS v   allSymsS (If _ _ c t f) = \l -> SomeSym c : (allSymsS t . allSymsS f $ l) 

@@ -0,0 +1,25 @@+module Grisette.Experimental+  ( -- * Experimental features++    -- | The experimental features are likely to be changed in the future,+    -- and they do not comply with the semantics versioning policy.+    --+    -- Use the APIs with caution.++    -- ** Symbolic Generation with Errors Class+    GenSymConstrained (..),+    GenSymSimpleConstrained (..),+    genSymConstrained,+    genSymSimpleConstrained,+    derivedSimpleFreshConstrainedNoSpec,+    derivedSimpleFreshConstrainedSameShape,+    derivedFreshConstrainedNoSpec,++    -- ** Some common GenSymConstrained specifications+    SOrdUpperBound (..),+    SOrdLowerBound (..),+    SOrdBound (..),+  )+where++import Grisette.Experimental.GenSymConstrained

@@ -0,0 +1,907 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++module Grisette.Experimental.GenSymConstrained+  ( -- * Symbolic value generation with errors+    GenSymConstrained (..),+    GenSymSimpleConstrained (..),+    genSymConstrained,+    genSymSimpleConstrained,+    derivedFreshConstrainedNoSpec,+    derivedSimpleFreshConstrainedNoSpec,+    derivedSimpleFreshConstrainedSameShape,++    -- * Some common GenSymConstrained specifications+    SOrdUpperBound (..),+    SOrdLowerBound (..),+    SOrdBound (..),+  )+where++import Control.Monad.Except+import Control.Monad.Trans.Maybe+import qualified Data.ByteString as B+import Data.Int+import Data.Word+import Debug.Trace+import GHC.Generics+import GHC.TypeLits+import Grisette.Core.Control.Monad.UnionM+import Grisette.Core.Data.BV+import Grisette.Core.Data.Class.Bool+import Grisette.Core.Data.Class.GenSym+import Grisette.Core.Data.Class.Mergeable+import Grisette.Core.Data.Class.SOrd+import Grisette.Core.Data.Class.SimpleMergeable++-- $setup+-- >>> import Grisette.Core+-- >>> import Grisette.Experimental+-- >>> import Grisette.IR.SymPrim+-- >>> :set -XOverloadedStrings+-- >>> :set -XTypeApplications++-- | Class of types in which symbolic values can be generated with some+-- specification.+--+-- See 'GenSym' for more details. The difference of this class is that it allows+-- constraints to be generated along with the generation of symbolic values.+class (Mergeable a) => GenSymConstrained spec a where+  -- | Generates a symbolic value with the given specification.+  --+  -- Constraint violations will throw an error in the monadic environment.+  --+  -- >>> runFreshT (freshConstrained () (SOrdUpperBound (1 :: SymInteger) ())) "a" :: ExceptT () UnionM (UnionM SymInteger)+  -- ExceptT <If (<= 1 a@0) (Left ()) (Right {a@0})>+  freshConstrained ::+    (MonadFresh m, MonadError e m, UnionLike m) =>+    e ->+    spec ->+    m (UnionM a)+  default freshConstrained ::+    (GenSymSimpleConstrained spec a) =>+    ( MonadFresh m,+      MonadError e m,+      UnionLike m+    ) =>+    e ->+    spec ->+    m (UnionM a)+  freshConstrained e spec = mrgSingle <$> simpleFreshConstrained e spec++genSymConstrained :: forall spec a e. (GenSymConstrained spec a, Mergeable e) => e -> spec -> FreshIdent -> ExceptT e UnionM (UnionM a)+genSymConstrained e spec = merge . runFreshT (freshConstrained e spec)++-- | Class of types in which symbolic values can be generated with some+-- specification.+--+-- See 'GenSymSimple' for more details. The difference of this class is that it allows+-- constraints to be generated along with the generation of symbolic values.+class (Mergeable a) => GenSymSimpleConstrained spec a where+  -- | Generates a symbolic value with the given specification.+  --+  -- Constraint violations will throw an error in the monadic environment.+  --+  -- >>> runFreshT (simpleFreshConstrained () (SOrdUpperBound (1 :: SymInteger) ())) "a" :: ExceptT () UnionM SymInteger+  -- ExceptT <If (<= 1 a@0) (Left ()) (Right a@0)>+  simpleFreshConstrained ::+    (MonadFresh m, MonadError e m, UnionLike m) =>+    e ->+    spec ->+    m a++genSymSimpleConstrained :: forall spec a e. (GenSymSimpleConstrained spec a, Mergeable e) => e -> spec -> FreshIdent -> ExceptT e UnionM a+genSymSimpleConstrained e spec = merge . runFreshT (simpleFreshConstrained e spec)++instance {-# OVERLAPPABLE #-} (Mergeable a, GenSym spec a) => GenSymConstrained spec a where+  freshConstrained _ = fresh++instance {-# OVERLAPPABLE #-} (Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained spec a where+  simpleFreshConstrained _ = simpleFresh++-- | Exclusive bound, generates the values with the specification, then filters+-- out the ones that are greater than or equal to the bound+data SOrdUpperBound a spec = SOrdUpperBound a spec++instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdUpperBound a spec) a where+  freshConstrained e (SOrdUpperBound u spec) = do+    s <- fresh spec+    v <- liftToMonadUnion s+    mrgIf (v >=~ u) (throwError e) (return ())+    mrgSingle $ mrgSingle v++instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdUpperBound a spec) a where+  simpleFreshConstrained e (SOrdUpperBound u spec) = do+    s <- simpleFresh spec+    mrgIf (s >=~ u) (throwError e) (return ())+    mrgSingle s++-- | Inclusive bound, generates the values with the specification, then filters+-- out the ones that are less than the bound+data SOrdLowerBound a spec = SOrdLowerBound a spec++instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdLowerBound a spec) a where+  freshConstrained e (SOrdLowerBound l spec) = do+    s <- fresh spec+    v <- liftToMonadUnion s+    mrgIf (v <~ l) (throwError e) (return ())+    mrgSingle $ mrgSingle v++instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdLowerBound a spec) a where+  simpleFreshConstrained e (SOrdLowerBound l spec) = do+    s <- simpleFresh spec+    mrgIf (s <~ l) (throwError e) (return ())+    mrgSingle s++-- | Left-inclusive, right-exclusive bound, generates the values with the+-- specification, then filters out the ones that are out-of-bound+data SOrdBound a spec = SOrdBound a a spec++instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdBound a spec) a where+  freshConstrained e (SOrdBound l u spec) = do+    s <- fresh spec+    v <- liftToMonadUnion s+    mrgIf (v <~ l ||~ v >=~ u) (throwError e) (return ())+    mrgSingle $ mrgSingle v++instance {-# OVERLAPPABLE #-} (SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdBound a spec) a where+  simpleFreshConstrained e (SOrdBound l u spec) = do+    s <- simpleFresh spec+    mrgIf (s <~ l ||~ s >=~ u) (throwError e) (return ())+    mrgSingle s++instance GenSymConstrained (SOrdBound Integer ()) Integer where+  freshConstrained e (SOrdBound l r _) = chooseFresh [l .. r - 1]++-- Either+instance+  ( GenSymConstrained aspec a,+    Mergeable a,+    GenSymConstrained bspec b,+    Mergeable b+  ) =>+  GenSymConstrained (Either aspec bspec) (Either a b)+  where+  freshConstrained e (Left aspec) = merge $ (merge . fmap Left) <$> freshConstrained e aspec+  freshConstrained e (Right bspec) = merge $ (merge . fmap Right) <$> freshConstrained e bspec++instance+  ( GenSymSimpleConstrained a a,+    GenSymSimpleConstrained b b+  ) =>+  GenSymSimpleConstrained (Either a b) (Either a b)+  where+  simpleFreshConstrained = derivedSimpleFreshConstrainedSameShape++instance+  (GenSymConstrained () a, Mergeable a, GenSymConstrained () b, Mergeable b) =>+  GenSymConstrained () (Either a b)+  where+  freshConstrained = derivedFreshConstrainedNoSpec++-- Maybe+instance+  (GenSymConstrained aspec a, Mergeable a) =>+  GenSymConstrained (Maybe aspec) (Maybe a)+  where+  freshConstrained _ Nothing = mrgSingle $ mrgSingle Nothing+  freshConstrained e (Just aspec) = merge $ (merge . fmap Just) <$> freshConstrained e aspec++instance+  (GenSymSimpleConstrained aspec a) =>+  GenSymSimpleConstrained (Maybe aspec) (Maybe a)+  where+  simpleFreshConstrained _ Nothing = mrgSingle Nothing+  simpleFreshConstrained e (Just aspec) = merge $ Just <$> simpleFreshConstrained e aspec++instance (GenSymConstrained aspec a, Mergeable a) => GenSymConstrained aspec (Maybe a) where+  freshConstrained e aspec = do+    a :: UnionM a <- freshConstrained e aspec+    merge $ chooseUnionFresh [return Nothing, Just <$> a]++-- List+instance+  (GenSymConstrained () a, Mergeable a) =>+  GenSymConstrained Integer [a]+  where+  freshConstrained e v = do+    l <- gl e v+    let xs = reverse $ scanr (:) [] l+    merge $ chooseUnionFresh $ merge . sequence <$> xs+    where+      gl :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Integer -> m [UnionM a]+      gl e1 v1+        | v1 <= 0 = mrgSingle []+        | otherwise = do+            l <- freshConstrained e1 ()+            r <- gl e1 (v1 - 1)+            mrgSingle $ l : r++instance+  (GenSymConstrained spec a, Mergeable a) =>+  GenSymConstrained (ListSpec spec) [a]+  where+  freshConstrained e (ListSpec minLen maxLen subSpec) =+    if minLen < 0 || maxLen < 0 || minLen >= maxLen+      then error $ "Bad lengths: " ++ show (minLen, maxLen)+      else do+        l <- gl e maxLen+        let xs = drop minLen $ reverse $ scanr (:) [] l+        merge $ chooseUnionFresh $ merge . sequence <$> xs+    where+      gl :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Int -> m [UnionM a]+      gl e1 currLen+        | currLen <= 0 = return []+        | otherwise = do+            l <- freshConstrained e1 subSpec+            r <- gl e1 (currLen - 1)+            return $ l : r++instance+  (GenSymConstrained a a, Mergeable a) =>+  GenSymConstrained [a] [a]+  where+  freshConstrained e l = do+    r :: [UnionM a] <- traverse (freshConstrained e) l+    mrgSingle $ merge $ sequence r++instance+  (GenSymSimpleConstrained a a) =>+  GenSymSimpleConstrained [a] [a]+  where+  simpleFreshConstrained = derivedSimpleFreshConstrainedSameShape++instance+  (GenSymConstrained spec a, Mergeable a) =>+  GenSymConstrained (SimpleListSpec spec) [a]+  where+  freshConstrained e (SimpleListSpec len subSpec) =+    if len < 0+      then error $ "Bad lengths: " ++ show len+      else do+        merge $ merge . sequence <$> gl e len+    where+      gl :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Int -> m [UnionM a]+      gl e1 currLen+        | currLen <= 0 = mrgSingle []+        | otherwise = do+            l <- freshConstrained e1 subSpec+            r <- gl e1 (currLen - 1)+            mrgSingle $ l : r++instance+  (GenSymSimpleConstrained spec a) =>+  GenSymSimpleConstrained (SimpleListSpec spec) [a]+  where+  simpleFreshConstrained e (SimpleListSpec len subSpec) =+    if len < 0+      then error $ "Bad lengths: " ++ show len+      else do+        gl e len+    where+      gl :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Int -> m [a]+      gl e1 currLen+        | currLen <= 0 = mrgSingle []+        | otherwise = do+            l <- simpleFreshConstrained e1 subSpec+            r <- gl e1 (currLen - 1)+            mrgSingle $ l : r++-- (,)+instance+  ( GenSymConstrained aspec a,+    Mergeable a,+    GenSymConstrained bspec b,+    Mergeable b+  ) =>+  GenSymConstrained (aspec, bspec) (a, b)+  where+  freshConstrained err (aspec, bspec) = do+    a1 <- freshConstrained err aspec+    b1 <- freshConstrained err bspec+    mrgSingle $ do+      ax <- a1+      bx <- b1+      mrgSingle (ax, bx)++instance+  ( GenSymSimpleConstrained aspec a,+    GenSymSimpleConstrained bspec b+  ) =>+  GenSymSimpleConstrained (aspec, bspec) (a, b)+  where+  simpleFreshConstrained e (aspec, bspec) = do+    merge $+      (,)+        <$> simpleFreshConstrained e aspec+        <*> simpleFreshConstrained e bspec++-- (,,)+instance+  ( GenSymConstrained aspec a,+    Mergeable a,+    GenSymConstrained bspec b,+    Mergeable b,+    GenSymConstrained cspec c,+    Mergeable c+  ) =>+  GenSymConstrained (aspec, bspec, cspec) (a, b, c)+  where+  freshConstrained err (aspec, bspec, cspec) = do+    a1 <- freshConstrained err aspec+    b1 <- freshConstrained err bspec+    c1 <- freshConstrained err cspec+    mrgSingle $ do+      ax <- a1+      bx <- b1+      cx <- c1+      mrgSingle (ax, bx, cx)++instance+  ( GenSymSimpleConstrained aspec a,+    GenSymSimpleConstrained bspec b,+    GenSymSimpleConstrained cspec c+  ) =>+  GenSymSimpleConstrained (aspec, bspec, cspec) (a, b, c)+  where+  simpleFreshConstrained e (aspec, bspec, cspec) = do+    merge $+      (,,)+        <$> simpleFreshConstrained e aspec+        <*> simpleFreshConstrained e bspec+        <*> simpleFreshConstrained e cspec++-- (,,,)+instance+  ( GenSymConstrained aspec a,+    Mergeable a,+    GenSymConstrained bspec b,+    Mergeable b,+    GenSymConstrained cspec c,+    Mergeable c,+    GenSymConstrained dspec d,+    Mergeable d+  ) =>+  GenSymConstrained (aspec, bspec, cspec, dspec) (a, b, c, d)+  where+  freshConstrained err (aspec, bspec, cspec, dspec) = do+    a1 <- freshConstrained err aspec+    b1 <- freshConstrained err bspec+    c1 <- freshConstrained err cspec+    d1 <- freshConstrained err dspec+    mrgSingle $ do+      ax <- a1+      bx <- b1+      cx <- c1+      dx <- d1+      mrgSingle (ax, bx, cx, dx)++instance+  ( GenSymSimpleConstrained aspec a,+    GenSymSimpleConstrained bspec b,+    GenSymSimpleConstrained cspec c,+    GenSymSimpleConstrained dspec d+  ) =>+  GenSymSimpleConstrained (aspec, bspec, cspec, dspec) (a, b, c, d)+  where+  simpleFreshConstrained e (aspec, bspec, cspec, dspec) = do+    merge $+      (,,,)+        <$> simpleFreshConstrained e aspec+        <*> simpleFreshConstrained e bspec+        <*> simpleFreshConstrained e cspec+        <*> simpleFreshConstrained e dspec++-- (,,,,)+instance+  ( GenSymConstrained aspec a,+    Mergeable a,+    GenSymConstrained bspec b,+    Mergeable b,+    GenSymConstrained cspec c,+    Mergeable c,+    GenSymConstrained dspec d,+    Mergeable d,+    GenSymConstrained espec e,+    Mergeable e+  ) =>+  GenSymConstrained (aspec, bspec, cspec, dspec, espec) (a, b, c, d, e)+  where+  freshConstrained err (aspec, bspec, cspec, dspec, espec) = do+    a1 <- freshConstrained err aspec+    b1 <- freshConstrained err bspec+    c1 <- freshConstrained err cspec+    d1 <- freshConstrained err dspec+    e1 <- freshConstrained err espec+    mrgSingle $ do+      ax <- a1+      bx <- b1+      cx <- c1+      dx <- d1+      ex <- e1+      mrgSingle (ax, bx, cx, dx, ex)++instance+  ( GenSymSimpleConstrained aspec a,+    GenSymSimpleConstrained bspec b,+    GenSymSimpleConstrained cspec c,+    GenSymSimpleConstrained dspec d,+    GenSymSimpleConstrained espec e+  ) =>+  GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec) (a, b, c, d, e)+  where+  simpleFreshConstrained e (aspec, bspec, cspec, dspec, espec) = do+    merge $+      (,,,,)+        <$> simpleFreshConstrained e aspec+        <*> simpleFreshConstrained e bspec+        <*> simpleFreshConstrained e cspec+        <*> simpleFreshConstrained e dspec+        <*> simpleFreshConstrained e espec++-- (,,,,,)+instance+  ( GenSymConstrained aspec a,+    Mergeable a,+    GenSymConstrained bspec b,+    Mergeable b,+    GenSymConstrained cspec c,+    Mergeable c,+    GenSymConstrained dspec d,+    Mergeable d,+    GenSymConstrained espec e,+    Mergeable e,+    GenSymConstrained fspec f,+    Mergeable f+  ) =>+  GenSymConstrained (aspec, bspec, cspec, dspec, espec, fspec) (a, b, c, d, e, f)+  where+  freshConstrained err (aspec, bspec, cspec, dspec, espec, fspec) = do+    a1 <- freshConstrained err aspec+    b1 <- freshConstrained err bspec+    c1 <- freshConstrained err cspec+    d1 <- freshConstrained err dspec+    e1 <- freshConstrained err espec+    f1 <- freshConstrained err fspec+    mrgSingle $ do+      ax <- a1+      bx <- b1+      cx <- c1+      dx <- d1+      ex <- e1+      fx <- f1+      mrgSingle (ax, bx, cx, dx, ex, fx)++instance+  ( GenSymSimpleConstrained aspec a,+    GenSymSimpleConstrained bspec b,+    GenSymSimpleConstrained cspec c,+    GenSymSimpleConstrained dspec d,+    GenSymSimpleConstrained espec e,+    GenSymSimpleConstrained fspec f+  ) =>+  GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec, fspec) (a, b, c, d, e, f)+  where+  simpleFreshConstrained e (aspec, bspec, cspec, dspec, espec, fspec) = do+    merge $+      (,,,,,)+        <$> simpleFreshConstrained e aspec+        <*> simpleFreshConstrained e bspec+        <*> simpleFreshConstrained e cspec+        <*> simpleFreshConstrained e dspec+        <*> simpleFreshConstrained e espec+        <*> simpleFreshConstrained e fspec++-- (,,,,,,)+instance+  ( GenSymConstrained aspec a,+    Mergeable a,+    GenSymConstrained bspec b,+    Mergeable b,+    GenSymConstrained cspec c,+    Mergeable c,+    GenSymConstrained dspec d,+    Mergeable d,+    GenSymConstrained espec e,+    Mergeable e,+    GenSymConstrained fspec f,+    Mergeable f,+    GenSymConstrained gspec g,+    Mergeable g+  ) =>+  GenSymConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec) (a, b, c, d, e, f, g)+  where+  freshConstrained err (aspec, bspec, cspec, dspec, espec, fspec, gspec) = do+    a1 <- freshConstrained err aspec+    b1 <- freshConstrained err bspec+    c1 <- freshConstrained err cspec+    d1 <- freshConstrained err dspec+    e1 <- freshConstrained err espec+    f1 <- freshConstrained err fspec+    g1 <- freshConstrained err gspec+    mrgSingle $ do+      ax <- a1+      bx <- b1+      cx <- c1+      dx <- d1+      ex <- e1+      fx <- f1+      gx <- g1+      mrgSingle (ax, bx, cx, dx, ex, fx, gx)++instance+  ( GenSymSimpleConstrained aspec a,+    GenSymSimpleConstrained bspec b,+    GenSymSimpleConstrained cspec c,+    GenSymSimpleConstrained dspec d,+    GenSymSimpleConstrained espec e,+    GenSymSimpleConstrained fspec f,+    GenSymSimpleConstrained gspec g+  ) =>+  GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec) (a, b, c, d, e, f, g)+  where+  simpleFreshConstrained e (aspec, bspec, cspec, dspec, espec, fspec, gspec) = do+    merge $+      (,,,,,,)+        <$> simpleFreshConstrained e aspec+        <*> simpleFreshConstrained e bspec+        <*> simpleFreshConstrained e cspec+        <*> simpleFreshConstrained e dspec+        <*> simpleFreshConstrained e espec+        <*> simpleFreshConstrained e fspec+        <*> simpleFreshConstrained e gspec++-- (,,,,,,,)+instance+  ( GenSymConstrained aspec a,+    Mergeable a,+    GenSymConstrained bspec b,+    Mergeable b,+    GenSymConstrained cspec c,+    Mergeable c,+    GenSymConstrained dspec d,+    Mergeable d,+    GenSymConstrained espec e,+    Mergeable e,+    GenSymConstrained fspec f,+    Mergeable f,+    GenSymConstrained gspec g,+    Mergeable g,+    GenSymConstrained hspec h,+    Mergeable h+  ) =>+  GenSymConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) (a, b, c, d, e, f, g, h)+  where+  freshConstrained err (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) = do+    a1 <- freshConstrained err aspec+    b1 <- freshConstrained err bspec+    c1 <- freshConstrained err cspec+    d1 <- freshConstrained err dspec+    e1 <- freshConstrained err espec+    f1 <- freshConstrained err fspec+    g1 <- freshConstrained err gspec+    h1 <- freshConstrained err hspec+    mrgSingle $ do+      ax <- a1+      bx <- b1+      cx <- c1+      dx <- d1+      ex <- e1+      fx <- f1+      gx <- g1+      hx <- h1+      mrgSingle (ax, bx, cx, dx, ex, fx, gx, hx)++instance+  ( GenSymSimpleConstrained aspec a,+    GenSymSimpleConstrained bspec b,+    GenSymSimpleConstrained cspec c,+    GenSymSimpleConstrained dspec d,+    GenSymSimpleConstrained espec e,+    GenSymSimpleConstrained fspec f,+    GenSymSimpleConstrained gspec g,+    GenSymSimpleConstrained hspec h+  ) =>+  GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) (a, b, c, d, e, f, g, h)+  where+  simpleFreshConstrained e (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) = do+    merge $+      (,,,,,,,)+        <$> simpleFreshConstrained e aspec+        <*> simpleFreshConstrained e bspec+        <*> simpleFreshConstrained e cspec+        <*> simpleFreshConstrained e dspec+        <*> simpleFreshConstrained e espec+        <*> simpleFreshConstrained e fspec+        <*> simpleFreshConstrained e gspec+        <*> simpleFreshConstrained e hspec++-- MaybeT+instance+  {-# OVERLAPPABLE #-}+  ( GenSymConstrained spec (m (Maybe a)),+    Mergeable1 m,+    Mergeable a+  ) =>+  GenSymConstrained spec (MaybeT m a)+  where+  freshConstrained e v = do+    x <- freshConstrained e v+    mrgSingle $ merge . fmap MaybeT $ x++instance+  {-# OVERLAPPABLE #-}+  ( GenSymSimpleConstrained spec (m (Maybe a)),+    Mergeable1 m,+    Mergeable a+  ) =>+  GenSymSimpleConstrained spec (MaybeT m a)+  where+  simpleFreshConstrained e v = merge $ MaybeT <$> simpleFreshConstrained e v++instance+  {-# OVERLAPPING #-}+  ( GenSymSimpleConstrained (m (Maybe a)) (m (Maybe a)),+    Mergeable1 m,+    Mergeable a+  ) =>+  GenSymSimpleConstrained (MaybeT m a) (MaybeT m a)+  where+  simpleFreshConstrained e (MaybeT v) = merge $ MaybeT <$> simpleFreshConstrained e v++instance+  {-# OVERLAPPING #-}+  ( GenSymSimpleConstrained (m (Maybe a)) (m (Maybe a)),+    Mergeable1 m,+    Mergeable a+  ) =>+  GenSymConstrained (MaybeT m a) (MaybeT m a)++-- ExceptT+instance+  {-# OVERLAPPABLE #-}+  ( GenSymConstrained spec (m (Either a b)),+    Mergeable1 m,+    Mergeable a,+    Mergeable b+  ) =>+  GenSymConstrained spec (ExceptT a m b)+  where+  freshConstrained e v = trace "x" $ do+    x <- freshConstrained e v+    mrgSingle $ merge . fmap ExceptT $ x++instance+  {-# OVERLAPPABLE #-}+  ( GenSymSimpleConstrained spec (m (Either a b)),+    Mergeable1 m,+    Mergeable a,+    Mergeable b+  ) =>+  GenSymSimpleConstrained spec (ExceptT a m b)+  where+  simpleFreshConstrained e v = merge $ ExceptT <$> simpleFreshConstrained e v++instance+  {-# OVERLAPPING #-}+  ( GenSymSimpleConstrained (m (Either e a)) (m (Either e a)),+    Mergeable1 m,+    Mergeable e,+    Mergeable a+  ) =>+  GenSymSimpleConstrained (ExceptT e m a) (ExceptT e m a)+  where+  simpleFreshConstrained e (ExceptT v) = merge $ ExceptT <$> simpleFreshConstrained e v++instance+  {-# OVERLAPPING #-}+  ( GenSymSimpleConstrained (m (Either e a)) (m (Either e a)),+    Mergeable1 m,+    Mergeable e,+    Mergeable a+  ) =>+  GenSymConstrained (ExceptT e m a) (ExceptT e m a)++-- Deriving++class GenSymConstrainedNoSpec a where+  freshConstrainedNoSpec ::+    ( MonadFresh m,+      MonadError e m,+      UnionLike m+    ) =>+    e ->+    m (UnionM (a c))++instance GenSymConstrainedNoSpec U1 where+  freshConstrainedNoSpec _ = return $ mrgSingle U1++instance (GenSymConstrained () c) => GenSymConstrainedNoSpec (K1 i c) where+  freshConstrainedNoSpec e = fmap K1 <$> freshConstrained e ()++instance (GenSymConstrainedNoSpec a) => GenSymConstrainedNoSpec (M1 i c a) where+  freshConstrainedNoSpec e = fmap M1 <$> freshConstrainedNoSpec e++instance+  ( GenSymConstrainedNoSpec a,+    GenSymConstrainedNoSpec b,+    forall x. Mergeable (a x),+    forall x. Mergeable (b x)+  ) =>+  GenSymConstrainedNoSpec (a :+: b)+  where+  freshConstrainedNoSpec ::+    forall m u c e.+    ( MonadFresh m,+      MonadError e m,+      UnionLike m+    ) =>+    e ->+    m (UnionM ((a :+: b) c))+  freshConstrainedNoSpec e = do+    cond :: bool <- simpleFresh ()+    l :: UnionM (a c) <- freshConstrainedNoSpec e+    r :: UnionM (b c) <- freshConstrainedNoSpec e+    return $ mrgIf cond (fmap L1 l) (fmap R1 r)++instance+  (GenSymConstrainedNoSpec a, GenSymConstrainedNoSpec b) =>+  GenSymConstrainedNoSpec (a :*: b)+  where+  freshConstrainedNoSpec ::+    forall m u c e.+    ( MonadFresh m,+      MonadError e m,+      UnionLike m+    ) =>+    e ->+    m (UnionM ((a :*: b) c))+  freshConstrainedNoSpec e = do+    l :: UnionM (a c) <- freshConstrainedNoSpec e+    r :: UnionM (b c) <- freshConstrainedNoSpec e+    return $ do+      l1 <- l+      r1 <- r+      return $ l1 :*: r1++-- | We cannot provide DerivingVia style derivation for 'GenSymConstrained', while you can+-- use this 'freshConstrained' implementation to implement 'GenSymConstrained' for your own types.+--+-- This 'freshConstrained' implementation is for the types that does not need any specification.+-- It will generate product types by generating each fields with @()@ as specification,+-- and generate all possible values for a sum type.+--+-- __Note:__ __Never__ use on recursive types.+derivedFreshConstrainedNoSpec ::+  forall bool a m u e.+  ( Generic a,+    GenSymConstrainedNoSpec (Rep a),+    Mergeable a,+    MonadFresh m,+    MonadError e m,+    UnionLike m+  ) =>+  e ->+  () ->+  m (UnionM a)+derivedFreshConstrainedNoSpec e _ = merge $ (merge . fmap to) <$> freshConstrainedNoSpec e++class GenSymSimpleConstrainedNoSpec a where+  simpleFreshConstrainedNoSpec ::+    ( MonadFresh m,+      MonadError e m,+      UnionLike m+    ) =>+    e ->+    m (a c)++instance GenSymSimpleConstrainedNoSpec U1 where+  simpleFreshConstrainedNoSpec _ = return U1++instance (GenSymSimpleConstrained () c) => GenSymSimpleConstrainedNoSpec (K1 i c) where+  simpleFreshConstrainedNoSpec e = K1 <$> simpleFreshConstrained e ()++instance (GenSymSimpleConstrainedNoSpec a) => GenSymSimpleConstrainedNoSpec (M1 i c a) where+  simpleFreshConstrainedNoSpec e = M1 <$> simpleFreshConstrainedNoSpec e++instance+  (GenSymSimpleConstrainedNoSpec a, GenSymSimpleConstrainedNoSpec b) =>+  GenSymSimpleConstrainedNoSpec (a :*: b)+  where+  simpleFreshConstrainedNoSpec e = do+    l :: a c <- simpleFreshConstrainedNoSpec e+    r :: b c <- simpleFreshConstrainedNoSpec e+    return $ l :*: r++-- | We cannot provide DerivingVia style derivation for 'GenSymSimpleConstrained', while+-- you can use this 'simpleFreshConstrained' implementation to implement 'GenSymSimpleConstrained' fo+-- your own types.+--+-- This 'simpleFreshConstrained' implementation is for the types that does not need any specification.+-- It will generate product types by generating each fields with '()' as specification.+-- It will not work on sum types.+--+-- __Note:__ __Never__ use on recursive types.+derivedSimpleFreshConstrainedNoSpec ::+  forall a m e.+  ( Generic a,+    GenSymSimpleConstrainedNoSpec (Rep a),+    MonadFresh m,+    MonadError e m,+    UnionLike m,+    Mergeable a+  ) =>+  e ->+  () ->+  m a+derivedSimpleFreshConstrainedNoSpec e _ = merge $ (merge . fmap to) $ simpleFreshConstrainedNoSpec e++class GenSymConstrainedSameShape a where+  simpleFreshConstrainedSameShape ::+    ( MonadFresh m,+      MonadError e m,+      UnionLike m+    ) =>+    e ->+    a c ->+    m (a c)++instance GenSymConstrainedSameShape U1 where+  simpleFreshConstrainedSameShape _ _ = return U1++instance (GenSymSimpleConstrained c c) => GenSymConstrainedSameShape (K1 i c) where+  simpleFreshConstrainedSameShape e (K1 c) = K1 <$> simpleFreshConstrained e c++instance (GenSymConstrainedSameShape a) => GenSymConstrainedSameShape (M1 i c a) where+  simpleFreshConstrainedSameShape e (M1 a) = M1 <$> simpleFreshConstrainedSameShape e a++instance+  (GenSymConstrainedSameShape a, GenSymConstrainedSameShape b) =>+  GenSymConstrainedSameShape (a :+: b)+  where+  simpleFreshConstrainedSameShape e (L1 a) = L1 <$> simpleFreshConstrainedSameShape e a+  simpleFreshConstrainedSameShape e (R1 a) = R1 <$> simpleFreshConstrainedSameShape e a++instance+  (GenSymConstrainedSameShape a, GenSymConstrainedSameShape b) =>+  GenSymConstrainedSameShape (a :*: b)+  where+  simpleFreshConstrainedSameShape e (a :*: b) = do+    l :: a c <- simpleFreshConstrainedSameShape e a+    r :: b c <- simpleFreshConstrainedSameShape e b+    return $ l :*: r++-- | We cannot provide DerivingVia style derivation for 'GenSymSimpleConstrained', while+-- you can use this 'simpleFreshConstrained' implementation to implement 'GenSymSimpleConstrained' fo+-- your own types.+--+-- This 'simpleFreshConstrained' implementation is for the types that can be generated with+-- a reference value of the same type.+--+-- For sum types, it will generate the result with the same data constructor.+-- For product types, it will generate the result by generating each field with+-- the corresponding reference value.+--+-- __Note:__ __Can__ be used on recursive types.+derivedSimpleFreshConstrainedSameShape ::+  ( Generic a,+    GenSymConstrainedSameShape (Rep a),+    Mergeable a,+    MonadFresh m,+    MonadError e m,+    UnionLike m+  ) =>+  e ->+  a ->+  m a+derivedSimpleFreshConstrainedSameShape e a = merge $ (merge . fmap to) $ simpleFreshConstrainedSameShape e (from a)

@@ -3,6 +3,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}+{-# OPTIONS_GHC -fno-cse #-}  -- | -- Module      :   Grisette.IR.SymPrim.Data.Prim.InternedTerm.Caches@@ -14,7 +15,7 @@ -- Portability :   GHC only module Grisette.IR.SymPrim.Data.Prim.InternedTerm.Caches (typeMemoizedCache) where -import Control.Once+import Control.Concurrent import Data.Data import qualified Data.HashMap.Strict as M import Data.IORef@@ -23,8 +24,16 @@ import GHC.IO import Unsafe.Coerce +mkOnceIO :: IO a -> IO (IO a)+mkOnceIO io = do+  mv <- newEmptyMVar+  demand <- newEmptyMVar+  forkIO (takeMVar demand >> io >>= putMVar mv)+  return (tryPutMVar demand () >> readMVar mv)+ termCacheCell :: IO (IORef (M.HashMap TypeRep Any))-termCacheCell = unsafeDupablePerformIO $ once $ newIORef M.empty+termCacheCell = unsafePerformIO $ mkOnceIO $ newIORef M.empty+{-# NOINLINE termCacheCell #-}  typeMemoizedCache :: forall a. (Interned a, Typeable a) => Cache a typeMemoizedCache = unsafeDupablePerformIO $ do

@@ -1,10 +1,13 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}  -- | -- Module      :   Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors@@ -42,6 +45,8 @@     complementBitsTerm,     shiftBitsTerm,     rotateBitsTerm,+    bvToSignedTerm,+    bvToUnsignedTerm,     bvconcatTerm,     bvselectTerm,     bvextendTerm,@@ -163,11 +168,11 @@ andTerm l r = internTerm $ UAndTerm l r {-# INLINE andTerm #-} -eqvTerm :: SupportedPrim a => Term a -> Term a -> Term Bool+eqvTerm :: (SupportedPrim a) => Term a -> Term a -> Term Bool eqvTerm l r = internTerm $ UEqvTerm l r {-# INLINE eqvTerm #-} -iteTerm :: SupportedPrim a => Term Bool -> Term a -> Term a -> Term a+iteTerm :: (SupportedPrim a) => Term Bool -> Term a -> Term a -> Term a iteTerm c l r = internTerm $ UITETerm c l r {-# INLINE iteTerm #-} @@ -223,14 +228,41 @@ rotateBitsTerm t n = internTerm $ URotateBitsTerm t n {-# INLINE rotateBitsTerm #-} +bvToSignedTerm ::+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+    Typeable ubv,+    Typeable sbv,+    KnownNat n,+    1 <= n,+    BVSignConversion (ubv n) (sbv n)+  ) =>+  Term (ubv n) ->+  Term (sbv n)+bvToSignedTerm = internTerm . UBVToSignedTerm++bvToUnsignedTerm ::+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+    Typeable ubv,+    Typeable sbv,+    KnownNat n,+    1 <= n,+    BVSignConversion (ubv n) (sbv n)+  ) =>+  Term (sbv n) ->+  Term (ubv n)+bvToUnsignedTerm = internTerm . UBVToUnsignedTerm+ bvconcatTerm ::-  ( SupportedPrim (bv a),-    SupportedPrim (bv b),-    SupportedPrim (bv (a + b)),+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat a,     KnownNat b,+    KnownNat (a + b),     1 <= a,     1 <= b,+    1 <= a + b,     SizedBV bv   ) =>   Term (bv a) ->@@ -240,9 +272,9 @@ {-# INLINE bvconcatTerm #-}  bvselectTerm ::-  forall bv n ix w proxy.-  ( SupportedPrim (bv n),-    SupportedPrim (bv w),+  forall bv n ix w p q.+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat n,     KnownNat ix,     KnownNat w,@@ -251,8 +283,8 @@     ix + w <= n,     SizedBV bv   ) =>-  proxy ix ->-  proxy w ->+  p ix ->+  q w ->   Term (bv n) ->   Term (bv w) bvselectTerm _ _ v = internTerm $ UBVSelectTerm (typeRep @ix) (typeRep @w) v@@ -260,11 +292,12 @@  bvextendTerm ::   forall bv l r proxy.-  ( SupportedPrim (bv l),-    SupportedPrim (bv r),+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat l,     KnownNat r,     1 <= l,+    1 <= r,     l <= r,     SizedBV bv   ) =>@@ -277,11 +310,12 @@  bvsignExtendTerm ::   forall bv l r proxy.-  ( SupportedPrim (bv l),-    SupportedPrim (bv r),+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat l,     KnownNat r,     1 <= l,+    1 <= r,     l <= r,     SizedBV bv   ) =>@@ -293,11 +327,12 @@  bvzeroExtendTerm ::   forall bv l r proxy.-  ( SupportedPrim (bv l),-    SupportedPrim (bv r),+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat l,     KnownNat r,     1 <= l,+    1 <= r,     l <= r,     SizedBV bv   ) =>

@@ -1,7 +1,10 @@ {-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}  module Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors   ( constructUnary,@@ -31,6 +34,8 @@     complementBitsTerm,     shiftBitsTerm,     rotateBitsTerm,+    bvToSignedTerm,+    bvToUnsignedTerm,     bvconcatTerm,     bvselectTerm,     bvextendTerm,@@ -98,8 +103,8 @@ notTerm :: Term Bool -> Term Bool orTerm :: Term Bool -> Term Bool -> Term Bool andTerm :: Term Bool -> Term Bool -> Term Bool-eqvTerm :: SupportedPrim a => Term a -> Term a -> Term Bool-iteTerm :: SupportedPrim a => Term Bool -> Term a -> Term a -> Term a+eqvTerm :: (SupportedPrim a) => Term a -> Term a -> Term Bool+iteTerm :: (SupportedPrim a) => Term Bool -> Term a -> Term a -> Term a addNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a -> Term a uminusNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a timesNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a -> Term a@@ -113,23 +118,46 @@ complementBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Term a shiftBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Int -> Term a rotateBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Int -> Term a+bvToSignedTerm ::+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+    Typeable ubv,+    Typeable sbv,+    KnownNat n,+    1 <= n,+    BVSignConversion (ubv n) (sbv n)+  ) =>+  Term (ubv n) ->+  Term (sbv n)+bvToUnsignedTerm ::+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+    Typeable ubv,+    Typeable sbv,+    KnownNat n,+    1 <= n,+    BVSignConversion (ubv n) (sbv n)+  ) =>+  Term (sbv n) ->+  Term (ubv n) bvconcatTerm ::-  ( SupportedPrim (bv a),-    SupportedPrim (bv b),-    SupportedPrim (bv (a + b)),+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat a,     KnownNat b,+    KnownNat (a + b),     1 <= a,     1 <= b,+    1 <= a + b,     SizedBV bv   ) =>   Term (bv a) ->   Term (bv b) ->   Term (bv (a + b)) bvselectTerm ::-  forall bv n ix w proxy.-  ( SupportedPrim (bv n),-    SupportedPrim (bv w),+  forall bv n ix w p q.+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat n,     KnownNat ix,     KnownNat w,@@ -138,17 +166,18 @@     ix + w <= n,     SizedBV bv   ) =>-  proxy ix ->-  proxy w ->+  p ix ->+  q w ->   Term (bv n) ->   Term (bv w) bvextendTerm ::   forall bv l r proxy.-  ( SupportedPrim (bv l),-    SupportedPrim (bv r),+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat l,     KnownNat r,     1 <= l,+    1 <= r,     l <= r,     SizedBV bv   ) =>@@ -158,11 +187,12 @@   Term (bv r) bvsignExtendTerm ::   forall bv l r proxy.-  ( SupportedPrim (bv l),-    SupportedPrim (bv r),+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat l,     KnownNat r,     1 <= l,+    1 <= r,     l <= r,     SizedBV bv   ) =>@@ -171,11 +201,12 @@   Term (bv r) bvzeroExtendTerm ::   forall bv l r proxy.-  ( SupportedPrim (bv l),-    SupportedPrim (bv r),+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat l,     KnownNat r,     1 <= l,+    1 <= r,     l <= r,     SizedBV bv   ) =>

@@ -5,10 +5,12 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveLift #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskellQuotes #-}@@ -78,8 +80,8 @@ class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t where   type PrimConstraint t :: Constraint   type PrimConstraint t = ()-  default withPrim :: PrimConstraint t => proxy t -> (PrimConstraint t => a) -> a-  withPrim :: proxy t -> (PrimConstraint t => a) -> a+  default withPrim :: (PrimConstraint t) => proxy t -> ((PrimConstraint t) => a) -> a+  withPrim :: proxy t -> ((PrimConstraint t) => a) -> a   withPrim _ i = i   termCache :: Cache (Term t)   termCache = typeMemoizedCache@@ -97,7 +99,7 @@   type ConType sym  -- | Type family to resolve the symbolic type associated with a concrete type.-class SupportedPrim con => SymRep con where+class (SupportedPrim con) => SymRep con where   type SymType con  -- | One-to-one mapping between symbolic types and concrete types.@@ -163,8 +165,8 @@ -- >>> "a" :: TypedSymbol Bool -- a :: Bool data TypedSymbol t where-  SimpleSymbol :: SupportedPrim t => String -> TypedSymbol t-  IndexedSymbol :: SupportedPrim t => String -> Int -> TypedSymbol t+  SimpleSymbol :: (SupportedPrim t) => String -> TypedSymbol t+  IndexedSymbol :: (SupportedPrim t) => String -> Int -> TypedSymbol t   WithInfo ::     forall t a.     ( SupportedPrim t,@@ -222,10 +224,10 @@   rnf (IndexedSymbol str i) = rnf str `seq` rnf i   rnf (WithInfo s info) = rnf s `seq` rnf info -instance SupportedPrim t => IsString (TypedSymbol t) where+instance (SupportedPrim t) => IsString (TypedSymbol t) where   fromString = SimpleSymbol -withSymbolSupported :: TypedSymbol t -> (SupportedPrim t => a) -> a+withSymbolSupported :: TypedSymbol t -> ((SupportedPrim t) => a) -> a withSymbolSupported (SimpleSymbol _) a = a withSymbolSupported (IndexedSymbol _ _) a = a withSymbolSupported (WithInfo _ _) a = a@@ -313,8 +315,8 @@   NotTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> Term Bool   OrTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool   AndTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool-  EqvTerm :: SupportedPrim t => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool-  ITETerm :: SupportedPrim t => {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t+  EqvTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool+  ITETerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t   AddNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t   UMinusNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t   TimesNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t@@ -328,14 +330,39 @@   ComplementBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t   ShiftBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> {-# UNPACK #-} !Int -> Term t   RotateBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> {-# UNPACK #-} !Int -> Term t+  BVToSignedTerm ::+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+      Typeable ubv,+      Typeable sbv,+      KnownNat n,+      1 <= n,+      BVSignConversion (ubv n) (sbv n)+    ) =>+    {-# UNPACK #-} !Id ->+    !(Term (ubv n)) ->+    Term (sbv n)+  BVToUnsignedTerm ::+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+      Typeable ubv,+      Typeable sbv,+      KnownNat n,+      1 <= n,+      BVSignConversion (ubv n) (sbv n)+    ) =>+    {-# UNPACK #-} !Id ->+    !(Term (sbv n)) ->+    Term (ubv n)   BVConcatTerm ::-    ( SupportedPrim (bv a),-      SupportedPrim (bv b),-      SupportedPrim (bv (a + b)),+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+      Typeable bv,       KnownNat a,       KnownNat b,+      KnownNat (a + b),       1 <= a,       1 <= b,+      1 <= a + b,       SizedBV bv     ) =>     {-# UNPACK #-} !Id ->@@ -343,8 +370,8 @@     !(Term (bv b)) ->     Term (bv (a + b))   BVSelectTerm ::-    ( SupportedPrim (bv n),-      SupportedPrim (bv w),+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+      Typeable bv,       KnownNat n,       KnownNat ix,       KnownNat w,@@ -359,11 +386,12 @@     !(Term (bv n)) ->     Term (bv w)   BVExtendTerm ::-    ( SupportedPrim (bv l),-      SupportedPrim (bv r),+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+      Typeable bv,       KnownNat l,       KnownNat r,       1 <= l,+      1 <= r,       l <= r,       SizedBV bv     ) =>@@ -425,6 +453,8 @@   liftTyped (ComplementBitsTerm _ arg) = [||complementBitsTerm arg||]   liftTyped (ShiftBitsTerm _ arg n) = [||shiftBitsTerm arg n||]   liftTyped (RotateBitsTerm _ arg n) = [||rotateBitsTerm arg n||]+  liftTyped (BVToSignedTerm _ v) = [||bvToSignedTerm v||]+  liftTyped (BVToUnsignedTerm _ v) = [||bvToUnsignedTerm v||]   liftTyped (BVConcatTerm _ arg1 arg2) = [||bvconcatTerm arg1 arg2||]   liftTyped (BVSelectTerm _ (_ :: TypeRep ix) (_ :: TypeRep w) arg) = [||bvselectTerm (Proxy @ix) (Proxy @w) arg||]   liftTyped (BVExtendTerm _ signed (_ :: TypeRep n) arg) = [||bvextendTerm signed (Proxy @n) arg||]@@ -499,6 +529,8 @@   show (ComplementBitsTerm i arg) = "ComplementBits{id=" ++ show i ++ ", arg=" ++ show arg ++ "}"   show (ShiftBitsTerm i arg n) = "ShiftBits{id=" ++ show i ++ ", arg=" ++ show arg ++ ", n=" ++ show n ++ "}"   show (RotateBitsTerm i arg n) = "RotateBits{id=" ++ show i ++ ", arg=" ++ show arg ++ ", n=" ++ show n ++ "}"+  show (BVToSignedTerm i arg) = "BVToSigned{id=" ++ show i ++ ", arg=" ++ show arg ++ "}"+  show (BVToUnsignedTerm i arg) = "BVToUnsigned{id=" ++ show i ++ ", arg=" ++ show arg ++ "}"   show (BVConcatTerm i arg1 arg2) = "BVConcat{id=" ++ show i ++ ", arg1=" ++ show arg1 ++ ", arg2=" ++ show arg2 ++ "}"   show (BVSelectTerm i ix w arg) =     "BVSelect{id=" ++ show i ++ ", ix=" ++ show ix ++ ", w=" ++ show w ++ ", arg=" ++ show arg ++ "}"@@ -551,8 +583,8 @@   UNotTerm :: !(Term Bool) -> UTerm Bool   UOrTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool   UAndTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool-  UEqvTerm :: SupportedPrim t => !(Term t) -> !(Term t) -> UTerm Bool-  UITETerm :: SupportedPrim t => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t+  UEqvTerm :: (SupportedPrim t) => !(Term t) -> !(Term t) -> UTerm Bool+  UITETerm :: (SupportedPrim t) => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t   UAddNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t   UUMinusNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t   UTimesNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t@@ -566,22 +598,45 @@   UComplementBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> UTerm t   UShiftBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> {-# UNPACK #-} !Int -> UTerm t   URotateBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> {-# UNPACK #-} !Int -> UTerm t+  UBVToSignedTerm ::+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+      Typeable ubv,+      Typeable sbv,+      KnownNat n,+      1 <= n,+      BVSignConversion (ubv n) (sbv n)+    ) =>+    !(Term (ubv n)) ->+    UTerm (sbv n)+  UBVToUnsignedTerm ::+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+      Typeable ubv,+      Typeable sbv,+      KnownNat n,+      1 <= n,+      BVSignConversion (ubv n) (sbv n)+    ) =>+    !(Term (sbv n)) ->+    UTerm (ubv n)   UBVConcatTerm ::-    ( SupportedPrim (bv a),-      SupportedPrim (bv b),-      SupportedPrim (bv (a + b)),+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+      Typeable bv,       KnownNat a,       KnownNat b,+      KnownNat (a + b),       1 <= a,       1 <= b,+      1 <= a + b,       SizedBV bv     ) =>     !(Term (bv a)) ->     !(Term (bv b)) ->     UTerm (bv (a + b))   UBVSelectTerm ::-    ( SupportedPrim (bv n),-      SupportedPrim (bv w),+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+      Typeable bv,       KnownNat n,       KnownNat ix,       KnownNat w,@@ -595,11 +650,12 @@     !(Term (bv n)) ->     UTerm (bv w)   UBVExtendTerm ::-    ( SupportedPrim (bv l),-      SupportedPrim (bv r),+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+      Typeable bv,       KnownNat l,       KnownNat r,       1 <= l,+      1 <= r,       l <= r,       SizedBV bv     ) =>@@ -634,7 +690,7 @@ eqTypedId (a, i1) (b, i2) = i1 == i2 && eqTypeRepBool a b {-# INLINE eqTypedId #-} -eqHeteroTag :: Eq a => (TypeRep a, a) -> (TypeRep b, b) -> Bool+eqHeteroTag :: (Eq a) => (TypeRep a, a) -> (TypeRep b, b) -> Bool eqHeteroTag (tpa, taga) (tpb, tagb) = eqHeteroRep tpa tpb taga tagb {-# INLINE eqHeteroTag #-} @@ -680,6 +736,14 @@     DShiftBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Int -> Description (Term t)     DRotateBitsTerm :: {-# UNPACK #-} !Id -> {-# UNPACK #-} !Int -> Description (Term t)     DBVConcatTerm :: TypeRep bv1 -> TypeRep bv2 -> {-# UNPACK #-} !Id -> {-# UNPACK #-} !Id -> Description (Term t)+    DBVToSignedTerm ::+      forall ubv sbv (n :: Nat).+      !(TypeRep (ubv n), Id) ->+      Description (Term (sbv n))+    DBVToUnsignedTerm ::+      forall sbv ubv (n :: Nat).+      !(TypeRep (sbv n), Id) ->+      Description (Term (ubv n))     DBVSelectTerm ::       forall bv (n :: Nat) (w :: Nat) (ix :: Nat).       !(TypeRep ix) ->@@ -738,6 +802,8 @@   describe (UComplementBitsTerm arg) = DComplementBitsTerm (identity arg)   describe (UShiftBitsTerm arg n) = DShiftBitsTerm (identity arg) n   describe (URotateBitsTerm arg n) = DRotateBitsTerm (identity arg) n+  describe (UBVToSignedTerm (arg :: Term bv)) = DBVToSignedTerm (typeRep :: TypeRep bv, identity arg)+  describe (UBVToUnsignedTerm (arg :: Term bv)) = DBVToSignedTerm (typeRep :: TypeRep bv, identity arg)   describe (UBVConcatTerm (arg1 :: bv1) (arg2 :: bv2)) =     DBVConcatTerm (typeRep :: TypeRep bv1) (typeRep :: TypeRep bv2) (identity arg1) (identity arg2)   describe (UBVSelectTerm (ix :: TypeRep ix) _ (arg :: Term arg)) =@@ -782,6 +848,8 @@       go (UComplementBitsTerm arg) = ComplementBitsTerm i arg       go (UShiftBitsTerm arg n) = ShiftBitsTerm i arg n       go (URotateBitsTerm arg n) = RotateBitsTerm i arg n+      go (UBVToSignedTerm arg) = BVToSignedTerm i arg+      go (UBVToUnsignedTerm arg) = BVToUnsignedTerm i arg       go (UBVConcatTerm arg1 arg2) = BVConcatTerm i arg1 arg2       go (UBVSelectTerm ix w arg) = BVSelectTerm i ix w arg       go (UBVExtendTerm signed n arg) = BVExtendTerm i signed n arg@@ -823,6 +891,8 @@   DComplementBitsTerm li == DComplementBitsTerm ri = li == ri   DShiftBitsTerm li ln == DShiftBitsTerm ri rn = li == ri && ln == rn   DRotateBitsTerm li ln == DRotateBitsTerm ri rn = li == ri && ln == rn+  DBVToSignedTerm li == DBVToSignedTerm ri = eqTypedId li ri+  DBVToUnsignedTerm li == DBVToUnsignedTerm ri = eqTypedId li ri   DBVConcatTerm lrep1 lrep2 li1 li2 == DBVConcatTerm rrep1 rrep2 ri1 ri2 =     eqTypeRepBool lrep1 rrep1 && eqTypeRepBool lrep2 rrep2 && li1 == ri1 && li2 == ri2   DBVSelectTerm lix li == DBVSelectTerm rix ri =@@ -881,25 +951,27 @@   hashWithSalt s (DComplementBitsTerm id1) = s `hashWithSalt` (20 :: Int) `hashWithSalt` id1   hashWithSalt s (DShiftBitsTerm id1 n) = s `hashWithSalt` (21 :: Int) `hashWithSalt` id1 `hashWithSalt` n   hashWithSalt s (DRotateBitsTerm id1 n) = s `hashWithSalt` (22 :: Int) `hashWithSalt` id1 `hashWithSalt` n+  hashWithSalt s (DBVToSignedTerm id) = s `hashWithSalt` (23 :: Int) `hashWithSalt` id+  hashWithSalt s (DBVToUnsignedTerm id) = s `hashWithSalt` (24 :: Int) `hashWithSalt` id   hashWithSalt s (DBVConcatTerm rep1 rep2 id1 id2) =-    s `hashWithSalt` (23 :: Int) `hashWithSalt` rep1 `hashWithSalt` rep2 `hashWithSalt` id1 `hashWithSalt` id2-  hashWithSalt s (DBVSelectTerm ix id1) = s `hashWithSalt` (24 :: Int) `hashWithSalt` ix `hashWithSalt` id1+    s `hashWithSalt` (25 :: Int) `hashWithSalt` rep1 `hashWithSalt` rep2 `hashWithSalt` id1 `hashWithSalt` id2+  hashWithSalt s (DBVSelectTerm ix id1) = s `hashWithSalt` (26 :: Int) `hashWithSalt` ix `hashWithSalt` id1   hashWithSalt s (DBVExtendTerm signed n id1) =     s-      `hashWithSalt` (25 :: Int)+      `hashWithSalt` (27 :: Int)       `hashWithSalt` signed       `hashWithSalt` n       `hashWithSalt` id1-  hashWithSalt s (DTabularFunApplyTerm id1 id2) = s `hashWithSalt` (26 :: Int) `hashWithSalt` id1 `hashWithSalt` id2-  hashWithSalt s (DGeneralFunApplyTerm id1 id2) = s `hashWithSalt` (27 :: Int) `hashWithSalt` id1 `hashWithSalt` id2-  hashWithSalt s (DDivIntegralTerm id1 id2) = s `hashWithSalt` (28 :: Int) `hashWithSalt` id1 `hashWithSalt` id2-  hashWithSalt s (DModIntegralTerm id1 id2) = s `hashWithSalt` (29 :: Int) `hashWithSalt` id1 `hashWithSalt` id2-  hashWithSalt s (DQuotIntegralTerm id1 id2) = s `hashWithSalt` (30 :: Int) `hashWithSalt` id1 `hashWithSalt` id2-  hashWithSalt s (DRemIntegralTerm id1 id2) = s `hashWithSalt` (31 :: Int) `hashWithSalt` id1 `hashWithSalt` id2-  hashWithSalt s (DDivBoundedIntegralTerm id1 id2) = s `hashWithSalt` (32 :: Int) `hashWithSalt` id1 `hashWithSalt` id2-  hashWithSalt s (DModBoundedIntegralTerm id1 id2) = s `hashWithSalt` (33 :: Int) `hashWithSalt` id1 `hashWithSalt` id2-  hashWithSalt s (DQuotBoundedIntegralTerm id1 id2) = s `hashWithSalt` (34 :: Int) `hashWithSalt` id1 `hashWithSalt` id2-  hashWithSalt s (DRemBoundedIntegralTerm id1 id2) = s `hashWithSalt` (35 :: Int) `hashWithSalt` id1 `hashWithSalt` id2+  hashWithSalt s (DTabularFunApplyTerm id1 id2) = s `hashWithSalt` (28 :: Int) `hashWithSalt` id1 `hashWithSalt` id2+  hashWithSalt s (DGeneralFunApplyTerm id1 id2) = s `hashWithSalt` (29 :: Int) `hashWithSalt` id1 `hashWithSalt` id2+  hashWithSalt s (DDivIntegralTerm id1 id2) = s `hashWithSalt` (30 :: Int) `hashWithSalt` id1 `hashWithSalt` id2+  hashWithSalt s (DModIntegralTerm id1 id2) = s `hashWithSalt` (31 :: Int) `hashWithSalt` id1 `hashWithSalt` id2+  hashWithSalt s (DQuotIntegralTerm id1 id2) = s `hashWithSalt` (32 :: Int) `hashWithSalt` id1 `hashWithSalt` id2+  hashWithSalt s (DRemIntegralTerm id1 id2) = s `hashWithSalt` (33 :: Int) `hashWithSalt` id1 `hashWithSalt` id2+  hashWithSalt s (DDivBoundedIntegralTerm id1 id2) = s `hashWithSalt` (34 :: Int) `hashWithSalt` id1 `hashWithSalt` id2+  hashWithSalt s (DModBoundedIntegralTerm id1 id2) = s `hashWithSalt` (35 :: Int) `hashWithSalt` id1 `hashWithSalt` id2+  hashWithSalt s (DQuotBoundedIntegralTerm id1 id2) = s `hashWithSalt` (36 :: Int) `hashWithSalt` id1 `hashWithSalt` id2+  hashWithSalt s (DRemBoundedIntegralTerm id1 id2) = s `hashWithSalt` (37 :: Int) `hashWithSalt` id1 `hashWithSalt` id2  -- Basic Bool defaultValueForBool :: Bool

@@ -1,12 +1,15 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}  module Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term   ( SupportedPrim (..),@@ -41,8 +44,8 @@ class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t where   type PrimConstraint t :: Constraint   type PrimConstraint t = ()-  default withPrim :: PrimConstraint t => proxy t -> (PrimConstraint t => a) -> a-  withPrim :: proxy t -> (PrimConstraint t => a) -> a+  default withPrim :: (PrimConstraint t) => proxy t -> ((PrimConstraint t) => a) -> a+  withPrim :: proxy t -> ((PrimConstraint t) => a) -> a   withPrim _ i = i   termCache :: Cache (Term t)   termCache = typeMemoizedCache@@ -58,7 +61,7 @@ class ConRep sym where   type ConType sym -class SupportedPrim con => SymRep con where+class (SupportedPrim con) => SymRep con where   type SymType con  class@@ -114,8 +117,8 @@   pformatTernary :: tag -> Term arg1 -> Term arg2 -> Term arg3 -> String  data TypedSymbol t where-  SimpleSymbol :: SupportedPrim t => String -> TypedSymbol t-  IndexedSymbol :: SupportedPrim t => String -> Int -> TypedSymbol t+  SimpleSymbol :: (SupportedPrim t) => String -> TypedSymbol t+  IndexedSymbol :: (SupportedPrim t) => String -> Int -> TypedSymbol t   WithInfo ::     forall t a.     ( SupportedPrim t,@@ -160,8 +163,8 @@   NotTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> Term Bool   OrTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool   AndTerm :: {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term Bool) -> Term Bool-  EqvTerm :: SupportedPrim t => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool-  ITETerm :: SupportedPrim t => {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t+  EqvTerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term Bool+  ITETerm :: (SupportedPrim t) => {-# UNPACK #-} !Id -> !(Term Bool) -> !(Term t) -> !(Term t) -> Term t   AddNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t   UMinusNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t   TimesNumTerm :: (SupportedPrim t, Num t) => {-# UNPACK #-} !Id -> !(Term t) -> !(Term t) -> Term t@@ -175,14 +178,39 @@   ComplementBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> Term t   ShiftBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> {-# UNPACK #-} !Int -> Term t   RotateBitsTerm :: (SupportedPrim t, Bits t) => {-# UNPACK #-} !Id -> !(Term t) -> {-# UNPACK #-} !Int -> Term t+  BVToSignedTerm ::+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+      Typeable ubv,+      Typeable sbv,+      KnownNat n,+      1 <= n,+      BVSignConversion (ubv n) (sbv n)+    ) =>+    {-# UNPACK #-} !Id ->+    !(Term (ubv n)) ->+    Term (sbv n)+  BVToUnsignedTerm ::+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+      Typeable ubv,+      Typeable sbv,+      KnownNat n,+      1 <= n,+      BVSignConversion (ubv n) (sbv n)+    ) =>+    {-# UNPACK #-} !Id ->+    !(Term (sbv n)) ->+    Term (ubv n)   BVConcatTerm ::-    ( SupportedPrim (bv a),-      SupportedPrim (bv b),-      SupportedPrim (bv (a + b)),+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+      Typeable bv,       KnownNat a,       KnownNat b,+      KnownNat (a + b),       1 <= a,       1 <= b,+      1 <= (a + b),       SizedBV bv     ) =>     {-# UNPACK #-} !Id ->@@ -190,8 +218,8 @@     !(Term (bv b)) ->     Term (bv (a + b))   BVSelectTerm ::-    ( SupportedPrim (bv n),-      SupportedPrim (bv w),+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+      Typeable bv,       KnownNat n,       KnownNat ix,       KnownNat w,@@ -206,11 +234,12 @@     !(Term (bv n)) ->     Term (bv w)   BVExtendTerm ::-    ( SupportedPrim (bv l),-      SupportedPrim (bv r),+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+      Typeable bv,       KnownNat l,       KnownNat r,       1 <= l,+      1 <= r,       l <= r,       SizedBV bv     ) =>@@ -264,8 +293,8 @@   UNotTerm :: !(Term Bool) -> UTerm Bool   UOrTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool   UAndTerm :: !(Term Bool) -> !(Term Bool) -> UTerm Bool-  UEqvTerm :: SupportedPrim t => !(Term t) -> !(Term t) -> UTerm Bool-  UITETerm :: SupportedPrim t => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t+  UEqvTerm :: (SupportedPrim t) => !(Term t) -> !(Term t) -> UTerm Bool+  UITETerm :: (SupportedPrim t) => !(Term Bool) -> !(Term t) -> !(Term t) -> UTerm t   UAddNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t   UUMinusNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> UTerm t   UTimesNumTerm :: (SupportedPrim t, Num t) => !(Term t) -> !(Term t) -> UTerm t@@ -279,22 +308,45 @@   UComplementBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> UTerm t   UShiftBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> {-# UNPACK #-} !Int -> UTerm t   URotateBitsTerm :: (SupportedPrim t, Bits t) => !(Term t) -> {-# UNPACK #-} !Int -> UTerm t+  UBVToSignedTerm ::+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+      Typeable ubv,+      Typeable sbv,+      KnownNat n,+      1 <= n,+      BVSignConversion (ubv n) (sbv n)+    ) =>+    !(Term (ubv n)) ->+    UTerm (sbv n)+  UBVToUnsignedTerm ::+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+      forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+      Typeable ubv,+      Typeable sbv,+      KnownNat n,+      1 <= n,+      BVSignConversion (ubv n) (sbv n)+    ) =>+    !(Term (sbv n)) ->+    UTerm (ubv n)   UBVConcatTerm ::-    ( SupportedPrim (bv a),-      SupportedPrim (bv b),-      SupportedPrim (bv (a + b)),+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+      Typeable bv,       KnownNat a,       KnownNat b,+      KnownNat (a + b),       1 <= a,       1 <= b,+      1 <= a + b,       SizedBV bv     ) =>     !(Term (bv a)) ->     !(Term (bv b)) ->     UTerm (bv (a + b))   UBVSelectTerm ::-    ( SupportedPrim (bv n),-      SupportedPrim (bv w),+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+      Typeable bv,       KnownNat n,       KnownNat ix,       KnownNat w,@@ -308,11 +360,12 @@     !(Term (bv n)) ->     UTerm (bv w)   UBVExtendTerm ::-    ( SupportedPrim (bv l),-      SupportedPrim (bv r),+    ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+      Typeable bv,       KnownNat l,       KnownNat r,       1 <= l,+      1 <= r,       l <= r,       SizedBV bv     ) =>

@@ -69,6 +69,8 @@         ComplementBitsTerm _ op -> SomeTerm $ pevalComplementBitsTerm (gov op)         ShiftBitsTerm _ op n -> SomeTerm $ pevalShiftBitsTerm (gov op) n         RotateBitsTerm _ op n -> SomeTerm $ pevalRotateBitsTerm (gov op) n+        BVToSignedTerm _ op -> SomeTerm $ pevalBVToSignedTerm op+        BVToUnsignedTerm _ op -> SomeTerm $ pevalBVToUnsignedTerm op         BVConcatTerm _ op1 op2 -> SomeTerm $ pevalBVConcatTerm (gov op1) (gov op2)         BVSelectTerm _ ix w op -> SomeTerm $ pevalBVSelectTerm ix w (gov op)         BVExtendTerm _ n signed op -> SomeTerm $ pevalBVExtendTerm n signed (gov op)

@@ -64,6 +64,8 @@ identityWithTypeRep (ComplementBitsTerm i _) = (typeRep (Proxy @t), i) identityWithTypeRep (ShiftBitsTerm i _ _) = (typeRep (Proxy @t), i) identityWithTypeRep (RotateBitsTerm i _ _) = (typeRep (Proxy @t), i)+identityWithTypeRep (BVToSignedTerm i _) = (typeRep (Proxy @t), i)+identityWithTypeRep (BVToUnsignedTerm i _) = (typeRep (Proxy @t), i) identityWithTypeRep (BVConcatTerm i _ _) = (typeRep (Proxy @t), i) identityWithTypeRep (BVSelectTerm i _ _ _) = (typeRep (Proxy @t), i) identityWithTypeRep (BVExtendTerm i _ _ _) = (typeRep (Proxy @t), i)@@ -103,6 +105,8 @@ introSupportedPrimConstraint ComplementBitsTerm {} x = x introSupportedPrimConstraint ShiftBitsTerm {} x = x introSupportedPrimConstraint RotateBitsTerm {} x = x+introSupportedPrimConstraint BVToSignedTerm {} x = x+introSupportedPrimConstraint BVToUnsignedTerm {} x = x introSupportedPrimConstraint BVConcatTerm {} x = x introSupportedPrimConstraint BVSelectTerm {} x = x introSupportedPrimConstraint BVExtendTerm {} x = x@@ -155,6 +159,8 @@     go (SomeTerm (ComplementBitsTerm _ arg)) = goUnary arg     go (SomeTerm (ShiftBitsTerm _ arg _)) = goUnary arg     go (SomeTerm (RotateBitsTerm _ arg _)) = goUnary arg+    go (SomeTerm (BVToSignedTerm _ arg)) = goUnary arg+    go (SomeTerm (BVToUnsignedTerm _ arg)) = goUnary arg     go (SomeTerm (BVConcatTerm _ arg1 arg2)) = goBinary arg1 arg2     go (SomeTerm (BVSelectTerm _ _ _ arg)) = goUnary arg     go (SomeTerm (BVExtendTerm _ _ _ arg)) = goUnary arg@@ -208,6 +214,8 @@ castTerm t@ComplementBitsTerm {} = cast t castTerm t@ShiftBitsTerm {} = cast t castTerm t@RotateBitsTerm {} = cast t+castTerm t@BVToSignedTerm {} = cast t+castTerm t@BVToUnsignedTerm {} = cast t castTerm t@BVConcatTerm {} = cast t castTerm t@BVSelectTerm {} = cast t castTerm t@BVExtendTerm {} = cast t@@ -247,6 +255,8 @@ pformat (ComplementBitsTerm _ arg) = "(~ " ++ pformat arg ++ ")" pformat (ShiftBitsTerm _ arg n) = "(shift " ++ pformat arg ++ " " ++ show n ++ ")" pformat (RotateBitsTerm _ arg n) = "(rotate " ++ pformat arg ++ " " ++ show n ++ ")"+pformat (BVToSignedTerm _ arg) = "(bvu2s " ++ pformat arg ++ " " ++ ")"+pformat (BVToUnsignedTerm _ arg) = "(bvs2u " ++ pformat arg ++ " " ++ ")" pformat (BVConcatTerm _ arg1 arg2) = "(bvconcat " ++ pformat arg1 ++ " " ++ pformat arg2 ++ ")" pformat (BVSelectTerm _ ix w arg) = "(bvselect " ++ show ix ++ " " ++ show w ++ " " ++ pformat arg ++ ")" pformat (BVExtendTerm _ signed n arg) =@@ -294,6 +304,8 @@     go t@(ComplementBitsTerm _ arg) = goUnary t arg     go t@(ShiftBitsTerm _ arg _) = goUnary t arg     go t@(RotateBitsTerm _ arg _) = goUnary t arg+    go t@(BVToSignedTerm _ arg) = goUnary t arg+    go t@(BVToUnsignedTerm _ arg) = goUnary t arg     go t@(BVConcatTerm _ arg1 arg2) = goBinary t arg1 arg2     go t@(BVSelectTerm _ _ _ arg) = goUnary t arg     go t@(BVExtendTerm _ _ _ arg) = goUnary t arg

@@ -332,6 +332,10 @@       goUnary (`pevalShiftBitsTerm` n) arg     go (SomeTerm (RotateBitsTerm _ arg n)) =       goUnary (`pevalRotateBitsTerm` n) arg+    go (SomeTerm (BVToSignedTerm _ arg)) =+      goUnary pevalBVToSignedTerm arg+    go (SomeTerm (BVToUnsignedTerm _ arg)) =+      goUnary pevalBVToUnsignedTerm arg     go (SomeTerm (BVConcatTerm _ arg1 arg2)) =       goBinary pevalBVConcatTerm arg1 arg2     go (SomeTerm (BVSelectTerm _ ix w arg)) =

@@ -4,6 +4,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-}@@ -18,7 +19,9 @@ -- Stability   :   Experimental -- Portability :   GHC only module Grisette.IR.SymPrim.Data.Prim.PartialEval.BV-  ( pevalBVConcatTerm,+  ( pevalBVToSignedTerm,+    pevalBVToUnsignedTerm,+    pevalBVConcatTerm,     pevalBVSelectTerm,     pevalBVExtendTerm,     pevalBVZeroExtendTerm,@@ -26,17 +29,91 @@   ) where +import Data.Typeable import GHC.TypeNats import Grisette.Core.Data.Class.BitVector import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold +-- ToSigned+pevalBVToSignedTerm ::+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+    Typeable ubv,+    Typeable sbv,+    KnownNat n,+    1 <= n,+    BVSignConversion (ubv n) (sbv n)+  ) =>+  Term (ubv n) ->+  Term (sbv n)+pevalBVToSignedTerm = unaryUnfoldOnce doPevalBVToSignedTerm bvToSignedTerm++doPevalBVToSignedTerm ::+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+    Typeable ubv,+    Typeable sbv,+    KnownNat n,+    1 <= n,+    BVSignConversion (ubv n) (sbv n)+  ) =>+  Term (ubv n) ->+  Maybe (Term (sbv n))+doPevalBVToSignedTerm (ConTerm _ b) = Just $ conTerm $ toSigned b+doPevalBVToSignedTerm (BVToUnsignedTerm _ b) = Just b >>= castTerm+doPevalBVToSignedTerm _ = Nothing++-- ToUnsigned+{-+bvToUnsignedTerm ::+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+    Typeable sbv,+    Typeable ubv,+    KnownNat n,+    1 <= n,+    BVToUnsigned (sbv n) (ubv n)+  ) =>+  Term (sbv n) ->+  Term (ubv n)+bvToUnsignedTerm = internTerm . UBVToUnsignedTerm+-}+pevalBVToUnsignedTerm ::+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+    Typeable ubv,+    Typeable sbv,+    KnownNat n,+    1 <= n,+    BVSignConversion (ubv n) (sbv n)+  ) =>+  Term (sbv n) ->+  Term (ubv n)+pevalBVToUnsignedTerm = unaryUnfoldOnce doPevalBVToUnsignedTerm bvToUnsignedTerm++doPevalBVToUnsignedTerm ::+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (ubv n),+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (sbv n),+    Typeable ubv,+    Typeable sbv,+    KnownNat n,+    1 <= n,+    BVSignConversion (ubv n) (sbv n)+  ) =>+  Term (sbv n) ->+  Maybe (Term (ubv n))+doPevalBVToUnsignedTerm (ConTerm _ b) = Just $ conTerm $ toUnsigned b+doPevalBVToUnsignedTerm (BVToSignedTerm _ b) = Just b >>= castTerm+doPevalBVToUnsignedTerm _ = Nothing+ -- select pevalBVSelectTerm ::-  forall bv n ix w proxy.-  ( SupportedPrim (bv n),-    SupportedPrim (bv w),+  forall bv n ix w p q.+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat n,     KnownNat ix,     KnownNat w,@@ -45,16 +122,16 @@     ix + w <= n,     SizedBV bv   ) =>-  proxy ix ->-  proxy w ->+  p ix ->+  q w ->   Term (bv n) ->   Term (bv w) pevalBVSelectTerm ix w = unaryUnfoldOnce (doPevalBVSelectTerm ix w) (bvselectTerm ix w)  doPevalBVSelectTerm ::-  forall bv n ix w proxy.-  ( SupportedPrim (bv n),-    SupportedPrim (bv w),+  forall bv n ix w p q.+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat n,     KnownNat ix,     KnownNat w,@@ -63,8 +140,8 @@     ix + w <= n,     SizedBV bv   ) =>-  proxy ix ->-  proxy w ->+  p ix ->+  q w ->   Term (bv n) ->   Maybe (Term (bv w)) doPevalBVSelectTerm ix w (ConTerm _ b) = Just $ conTerm $ sizedBVSelect ix w b@@ -73,12 +150,13 @@ -- ext pevalBVZeroExtendTerm ::   forall proxy l r bv.-  ( KnownNat l,+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,+    KnownNat l,     KnownNat r,     1 <= l,+    1 <= r,     l <= r,-    SupportedPrim (bv l),-    SupportedPrim (bv r),     SizedBV bv   ) =>   proxy r ->@@ -88,12 +166,13 @@  pevalBVSignExtendTerm ::   forall proxy l r bv.-  ( KnownNat l,+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,+    KnownNat l,     KnownNat r,     1 <= l,+    1 <= r,     l <= r,-    SupportedPrim (bv l),-    SupportedPrim (bv r),     SizedBV bv   ) =>   proxy r ->@@ -103,12 +182,13 @@  pevalBVExtendTerm ::   forall proxy l r bv.-  ( KnownNat l,+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,+    KnownNat l,     KnownNat r,     1 <= l,+    1 <= r,     l <= r,-    SupportedPrim (bv l),-    SupportedPrim (bv r),     SizedBV bv   ) =>   Bool ->@@ -119,12 +199,13 @@  doPevalBVExtendTerm ::   forall proxy l r bv.-  ( KnownNat l,+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,+    KnownNat l,     KnownNat r,     1 <= l,+    1 <= r,     l <= r,-    SupportedPrim (bv l),-    SupportedPrim (bv r),     SizedBV bv   ) =>   Bool ->@@ -135,13 +216,14 @@ doPevalBVExtendTerm _ _ _ = Nothing  pevalBVConcatTerm ::-  ( SupportedPrim (bv a),-    SupportedPrim (bv b),-    SupportedPrim (bv (a + b)),+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat a,     KnownNat b,+    KnownNat (a + b),     1 <= a,     1 <= b,+    1 <= a + b,     SizedBV bv   ) =>   Term (bv a) ->@@ -150,13 +232,14 @@ pevalBVConcatTerm = binaryUnfoldOnce doPevalBVConcatTerm bvconcatTerm  doPevalBVConcatTerm ::-  ( SupportedPrim (bv a),-    SupportedPrim (bv b),-    SupportedPrim (bv (a + b)),+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat a,     KnownNat b,+    KnownNat (a + b),     1 <= a,     1 <= b,+    1 <= (a + b),     SizedBV bv   ) =>   Term (bv a) ->

@@ -44,7 +44,7 @@ eqHetero = cmpHetero (==) {-# INLINE eqHetero #-} -eqHeteroRep :: forall a b. Eq a => TypeRep a -> TypeRep b -> a -> b -> Bool+eqHeteroRep :: forall a b. (Eq a) => TypeRep a -> TypeRep b -> a -> b -> Bool eqHeteroRep ta tb = cmpHeteroRep ta tb (==) {-# INLINE eqHeteroRep #-} 

@@ -309,7 +309,7 @@ -- >>> :set -XOverloadedStrings -XDataKinds -XBinaryLiterals -- >>> (SomeSymIntN ("a" :: SymIntN 5)) + (SomeSymIntN (5 :: SymIntN 5)) -- (+ 0b00101 a)--- >>> someBVConcat (SomeSymIntN (con 0b101 :: SymIntN 3)) (SomeSymIntN (con 0b110 :: SymIntN 3))+-- >>> bvConcat (SomeSymIntN (con 0b101 :: SymIntN 3)) (SomeSymIntN (con 0b110 :: SymIntN 3)) -- 0b101110 -- -- More symbolic operations are available. Please refer to the documentation@@ -421,7 +421,7 @@ -- >>> :set -XOverloadedStrings -XDataKinds -XBinaryLiterals -- >>> (SomeSymWordN ("a" :: SymWordN 5)) + (SomeSymWordN (5 :: SymWordN 5)) -- (+ 0b00101 a)--- >>> someBVConcat (SomeSymWordN (con 0b101 :: SymWordN 3)) (SomeSymWordN (con 0b110 :: SymWordN 3))+-- >>> bvConcat (SomeSymWordN (con 0b101 :: SymWordN 3)) (SomeSymWordN (con 0b110 :: SymWordN 3)) -- 0b101110 -- -- More symbolic operations are available. Please refer to the documentation@@ -656,19 +656,31 @@ #define BITS_BV(symtype, signed) \ instance (KnownNat n, 1 <= n) => Bits (symtype n) where \   symtype l .&. symtype r = symtype $ pevalAndBitsTerm l r; \+  {-# INLINE (.&.) #-}; \   symtype l .|. symtype r = symtype $ pevalOrBitsTerm l r; \+  {-# INLINE (.|.) #-}; \   symtype l `xor` symtype r = symtype $ pevalXorBitsTerm l r; \+  {-# INLINE xor #-}; \   complement (symtype n) = symtype $ pevalComplementBitsTerm n; \+  {-# INLINE complement #-}; \   shift (symtype n) i = symtype $ pevalShiftBitsTerm n i; \+  {-# INLINE shift #-}; \   rotate (symtype n) i = symtype $ pevalRotateBitsTerm n i; \-  bitSize _ = fromIntegral $ natVal (Proxy @n); \-  bitSizeMaybe _ = Just $ fromIntegral $ natVal (Proxy @n); \+  {-# INLINE rotate #-}; \+  bitSize = finiteBitSize; \+  {-# INLINE bitSize #-}; \+  bitSizeMaybe = Just . finiteBitSize; \+  {-# INLINE bitSizeMaybe #-}; \   isSigned _ = signed; \+  {-# INLINE isSigned #-}; \   testBit (Con n) =  testBit n; \   testBit _ = error "You cannot call testBit on symbolic variables"; \+  {-# INLINE testBit #-}; \   bit = con . bit; \+  {-# INLINE bit #-}; \   popCount (Con n) = popCount n; \-  popCount _ = error "You cannot call popCount on symbolic variables"+  popCount _ = error "You cannot call popCount on symbolic variables"; \+  {-# INLINE popCount #-}  #define BITS_BV_SOME(somety, origty, br1, uf, ur1) \ instance Bits somety where \@@ -696,9 +708,9 @@   {-# INLINE complementBit #-}; \   testBit s i = uf (`testBit` i) "testBit" s; \   {-# INLINE testBit #-}; \-  bitSizeMaybe (somety (n :: origty n)) = Just $ fromIntegral $ natVal n; \+  bitSizeMaybe = Just . finiteBitSize; \   {-# INLINE bitSizeMaybe #-}; \-  bitSize (somety (n :: origty n)) = fromIntegral $ natVal n; \+  bitSize = finiteBitSize; \   {-# INLINE bitSize #-}; \   isSigned _ = False; \   {-# INLINE isSigned #-}; \@@ -724,6 +736,25 @@ BITS_BV_SOME(SomeSymWordN, SymWordN, binSomeSymWordNR1, unarySomeSymWordN, unarySomeSymWordNR1) #endif +-- FiniteBits++#define FINITE_BITS_BV(symtype) \+instance (KnownNat n, 1 <= n) => FiniteBits (symtype n) where \+  finiteBitSize _ = fromIntegral $ natVal (Proxy @n); \+  {-# INLINE finiteBitSize #-}; \++#define FINITE_BITS_BV_SOME(somety, origty) \+instance FiniteBits somety where \+  finiteBitSize (somety (n :: origty n)) = fromIntegral $ natVal n; \+  {-# INLINE finiteBitSize #-}++#if 1+FINITE_BITS_BV(SymIntN)+FINITE_BITS_BV(SymWordN)+FINITE_BITS_BV_SOME(SomeSymIntN, SymIntN)+FINITE_BITS_BV_SOME(SomeSymWordN, SymWordN)+#endif+ -- Show  #define SHOW_SIMPLE(symtype) \@@ -1105,11 +1136,17 @@ instance (KnownNat n, 1 <= n) => SEq (symtype n) where \   (symtype l) ==~ (symtype r) = SymBool $ pevalEqvTerm l r -#define SEQ_BV_SOME(somety, bf) \+#define SEQ_BV_SOME(somety, origty) \ instance SEq somety where \-  (==~) = bf (==~) "==~"; \+  somety (l :: origty l) ==~ somety (r :: origty r) = \+    (case sameNat (Proxy @l) (Proxy @r) of \+      Just Refl -> l ==~ r; \+      Nothing -> con False); \   {-# INLINE (==~) #-}; \-  (/=~) = bf (/=~) "/=~"; \+  somety (l :: origty l) /=~ somety (r :: origty r) = \+    (case sameNat (Proxy @l) (Proxy @r) of \+      Just Refl -> l /=~ r; \+      Nothing -> con True); \   {-# INLINE (/=~) #-}  #if 1@@ -1117,8 +1154,8 @@ SEQ_SIMPLE(SymInteger) SEQ_BV(SymIntN) SEQ_BV(SymWordN)-SEQ_BV_SOME(SomeSymIntN, binSomeSymIntN)-SEQ_BV_SOME(SomeSymWordN, binSomeSymWordN)+SEQ_BV_SOME(SomeSymIntN, SymIntN)+SEQ_BV_SOME(SomeSymWordN, SymWordN) #endif  -- SOrd@@ -1231,8 +1268,8 @@     LeqProof -> symtype $ pevalBVExtendTerm True (Proxy @r) v  #define BVSELECT_SIZED(symtype) \-sizedBVSelect :: forall n ix w proxy. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) => \-  proxy ix -> proxy w -> symtype n -> symtype w; \+sizedBVSelect :: forall n ix w p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) => \+  p ix -> q w -> symtype n -> symtype w; \ sizedBVSelect pix pw (symtype v) = symtype $ pevalBVSelectTerm pix pw v  #if 1@@ -1254,49 +1291,86 @@ -- BV  #define BVCONCAT(somety, origty) \-someBVConcat (somety (a :: origty l)) (somety (b :: origty r)) = \+bvConcat (somety (a :: origty l)) (somety (b :: origty r)) = \   case (leqAddPos (Proxy @l) (Proxy @r), knownAdd @l @r KnownProof KnownProof) of \     (LeqProof, KnownProof) -> \       somety $ sizedBVConcat a b  #define BVZEXT(somety, origty) \-someBVZext (p :: p l) (somety (a :: origty n)) \-  | natVal p < natVal (Proxy @n) = error "zextBV: trying to zero extend a value to a smaller size" \-  | otherwise = \-    case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \-      (LeqProof, LeqProof) -> somety $ sizedBVZext p a+bvZext l (somety (a :: origty n)) \+  | l < n = error "bvZext: trying to zero extend a value to a smaller size" \+  | otherwise = res (Proxy @n) \+  where \+    n = fromIntegral $ natVal (Proxy @n); \+    res :: forall (l :: Nat). Proxy l -> somety; \+    res p = \+      case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \+        (KnownProof, LeqProof, LeqProof) -> somety $ sizedBVZext p a  #define BVSEXT(somety, origty) \-someBVSext (p :: p l) (somety (a :: origty n)) \-  | natVal p < natVal (Proxy @n) = error "zextBV: trying to zero extend a value to a smaller size" \-  | otherwise = \-    case (unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \-      (LeqProof, LeqProof) -> somety $ sizedBVSext p a+bvSext l (somety (a :: origty n)) \+  | l < n = error "bvZext: trying to zero extend a value to a smaller size" \+  | otherwise = res (Proxy @n) \+  where \+    n = fromIntegral $ natVal (Proxy @n); \+    res :: forall (l :: Nat). Proxy l -> somety; \+    res p = \+      case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \+        (KnownProof, LeqProof, LeqProof) -> somety $ sizedBVSext p a  #define BVSELECT(somety, origty) \-someBVSelect (p :: p ix) (q :: q w) (somety (a :: origty n)) \-  | natVal p + natVal q > natVal (Proxy @n) = error "selectBV: trying to select a bitvector outside the bounds of the input" \-  | natVal q == 0 = error "selectBV: trying to select a bitvector of size 0" \-  | otherwise = \-    case (unsafeLeqProof @1 @w, unsafeLeqProof @(ix + w) @n) of \-      (LeqProof, LeqProof) -> somety $ sizedBVSelect (Proxy @ix) (Proxy @w) a+bvSelect ix w (somety (a :: origty n)) \+    | ix + w > n = error "bvSelect: trying to select a bitvector outside the bounds of the input" \+    | w == 0 = error "bvSelect: trying to select a bitvector of size 0" \+    | otherwise = res (Proxy @n) (Proxy @n) \+    where \+      n = fromIntegral $ natVal (Proxy @n); \+      res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> somety; \+      res p1 p2 = \+        case ( unsafeKnownProof @ix (fromIntegral ix), \+               unsafeKnownProof @w (fromIntegral w), \+               unsafeLeqProof @1 @w, \+               unsafeLeqProof @(ix + w) @n \+             ) of \+          (KnownProof, KnownProof, LeqProof, LeqProof) -> \+            somety $ sizedBVSelect (Proxy @ix) (Proxy @w) a  #if 1-instance SomeBV SomeSymIntN where+instance BV SomeSymIntN where   BVCONCAT(SomeSymIntN, SymIntN)+  {-# INLINE bvConcat #-}   BVZEXT(SomeSymIntN, SymIntN)+  {-# INLINE bvZext #-}   BVSEXT(SomeSymIntN, SymIntN)-  someBVExt = someBVSext+  {-# INLINE bvSext #-}+  bvExt = bvSext+  {-# INLINE bvExt #-}   BVSELECT(SomeSymIntN, SymIntN)+  {-# INLINE bvSelect #-} -instance SomeBV SomeSymWordN where+instance BV SomeSymWordN where   BVCONCAT(SomeSymWordN, SymWordN)+  {-# INLINE bvConcat #-}   BVZEXT(SomeSymWordN, SymWordN)+  {-# INLINE bvZext #-}   BVSEXT(SomeSymWordN, SymWordN)-  someBVExt = someBVZext+  {-# INLINE bvSext #-}+  bvExt = bvZext+  {-# INLINE bvExt #-}   BVSELECT(SomeSymWordN, SymWordN)+  {-# INLINE bvSelect #-} #endif +-- BVSignConversion++instance (KnownNat n, 1 <= n) => BVSignConversion (SymWordN n) (SymIntN n) where+  toSigned (SymWordN n) = SymIntN $ pevalBVToSignedTerm n+  toUnsigned (SymIntN n) = SymWordN $ pevalBVToUnsignedTerm n++instance BVSignConversion SomeSymWordN SomeSymIntN where+  toSigned (SomeSymWordN n) = SomeSymIntN $ toSigned n+  toUnsigned (SomeSymIntN n) = SomeSymWordN $ toUnsigned n+ -- ModelRep  -- | A pair of a symbolic constant and its value.@@ -1305,7 +1379,7 @@ -- >>> buildModel ("a" := (1 :: Integer), "b" := True) :: Model -- Model {a -> 1 :: Integer, b -> True :: Bool} data ModelSymPair ct st where-  (:=) :: LinkedRep ct st => st -> ct -> ModelSymPair ct st+  (:=) :: (LinkedRep ct st) => st -> ct -> ModelSymPair ct st  instance ModelRep (ModelSymPair ct st) Model where   buildModel (sym := val) =@@ -1318,7 +1392,7 @@ -- -- >>> symsSize [1, "a" :: SymInteger, "a" + 1 :: SymInteger] -- 3-symsSize :: forall con sym. LinkedRep con sym => [sym] -> Int+symsSize :: forall con sym. (LinkedRep con sym) => [sym] -> Int symsSize = termsSize . fmap (underlyingTerm @con) {-# INLINE symsSize #-} @@ -1333,7 +1407,7 @@ -- 3 -- >>> symSize (("a" + 1) * ("a" + 1) :: SymInteger) -- 4-symSize :: forall con sym. LinkedRep con sym => sym -> Int+symSize :: forall con sym. (LinkedRep con sym) => sym -> Int symSize = termSize . underlyingTerm @con {-# INLINE symSize #-} @@ -1375,7 +1449,7 @@ -- -- >>> allSymsSize ("a" :: SymInteger, "a" + "b" :: SymInteger, ("a" + "b") * "c" :: SymInteger) -- 5-allSymsSize :: AllSyms a => a -> Int+allSymsSize :: (AllSyms a) => a -> Int allSymsSize = someSymsSize . allSyms  class AllSyms' a where@@ -1387,10 +1461,10 @@ instance AllSyms' U1 where   allSymsS' _ = id -instance AllSyms c => AllSyms' (K1 i c) where+instance (AllSyms c) => AllSyms' (K1 i c) where   allSymsS' (K1 v) = allSymsS v -instance AllSyms' a => AllSyms' (M1 i c a) where+instance (AllSyms' a) => AllSyms' (M1 i c a) where   allSymsS' (M1 v) = allSymsS' v  instance (AllSyms' a, AllSyms' b) => AllSyms' (a :+: b) where@@ -1580,11 +1654,11 @@   allSymsS (WriterStrict.WriterT v) = allSymsS v  -- Identity-instance AllSyms a => AllSyms (Identity a) where+instance (AllSyms a) => AllSyms (Identity a) where   allSymsS (Identity a) = allSymsS a  -- IdentityT-instance AllSyms (m a) => AllSyms (IdentityT m a) where+instance (AllSyms (m a)) => AllSyms (IdentityT m a) where   allSymsS (IdentityT a) = allSymsS a  -- VerificationConditions

@@ -17,6 +17,7 @@ where  import Control.Monad.Cont+import Control.Monad.Trans.Class import Grisette.Core.Data.Class.Bool import Grisette.Core.Data.Class.Mergeable import Grisette.Core.Data.Class.SimpleMergeable@@ -33,6 +34,6 @@ {-# INLINE mrgEvalContT #-}  -- | 'Control.Monad.Cont.resetT' with 'MergingStrategy' knowledge propagation-mrgResetT :: (UnionLike m, Mergeable r, Monad m) => Monad m => ContT r m r -> ContT r' m r+mrgResetT :: (UnionLike m, Mergeable r, Monad m) => (Monad m) => ContT r m r -> ContT r' m r mrgResetT = lift . mrgEvalContT {-# INLINE mrgResetT #-}

@@ -117,11 +117,11 @@  -- | Construct a runtime representation of a type-level natural number when its -- runtime value is known.-natRepr :: forall n. KnownNat n => NatRepr n+natRepr :: forall n. (KnownNat n) => NatRepr n natRepr = NatRepr (natVal (Proxy @n))  -- | Decrement a 'NatRepr' by 1.-decNat :: 1 <= n => NatRepr n -> NatRepr (n - 1)+decNat :: (1 <= n) => NatRepr n -> NatRepr (n - 1) decNat (NatRepr n) = NatRepr (n - 1)  -- | Predecessor of a 'NatRepr'@@ -137,11 +137,11 @@ addNat (NatRepr m) (NatRepr n) = NatRepr (m + n)  -- | Subtraction of two 'NatRepr's.-subNat :: n <= m => NatRepr m -> NatRepr n -> NatRepr (m - n)+subNat :: (n <= m) => NatRepr m -> NatRepr n -> NatRepr (m - n) subNat (NatRepr m) (NatRepr n) = NatRepr (m - n)  -- | Division of two 'NatRepr's.-divNat :: 1 <= n => NatRepr m -> NatRepr n -> NatRepr (Div m n)+divNat :: (1 <= n) => NatRepr m -> NatRepr n -> NatRepr (Div m n) divNat (NatRepr m) (NatRepr n) = NatRepr (m `div` n)  -- | Half of a 'NatRepr'.@@ -151,10 +151,10 @@ -- | @'KnownProof n'@ is a type whose values are only inhabited when @n@ has -- a known runtime value. data KnownProof (n :: Nat) where-  KnownProof :: KnownNat n => KnownProof n+  KnownProof :: (KnownNat n) => KnownProof n  -- | Introduces the 'KnownNat' constraint when it's proven.-withKnownProof :: KnownProof n -> (KnownNat n => r) -> r+withKnownProof :: KnownProof n -> ((KnownNat n) => r) -> r withKnownProof p r = case p of KnownProof -> r  -- | Construct a 'KnownProof' given the runtime value.@@ -181,10 +181,10 @@  -- | @'LeqProof m n'@ is a type whose values are only inhabited when @m <= n@. data LeqProof (m :: Nat) (n :: Nat) where-  LeqProof :: m <= n => LeqProof m n+  LeqProof :: (m <= n) => LeqProof m n  -- | Introduces the @m <= n@ constraint when it's proven.-withLeqProof :: LeqProof m n -> (m <= n => r) -> r+withLeqProof :: LeqProof m n -> ((m <= n) => r) -> r withLeqProof p r = case p of LeqProof -> r  -- | Construct a 'LeqProof'.

@@ -572,7 +572,10 @@                 testBinaryOpLowering @(IntN 5) @(IntN 5) @(IntN 5) boundedConfig quotBoundedIntegralTerm "quot" SBV.sQuot,               testCase "Rem - bounded" $ do                 testBinaryOpLowering @(IntN 5) @(IntN 5) @(IntN 5) unboundedConfig remBoundedIntegralTerm "rem" SBV.sRem-                testBinaryOpLowering @(IntN 5) @(IntN 5) @(IntN 5) boundedConfig remBoundedIntegralTerm "rem" SBV.sRem+                testBinaryOpLowering @(IntN 5) @(IntN 5) @(IntN 5) boundedConfig remBoundedIntegralTerm "rem" SBV.sRem,+              testCase "ToUnsigned" $ do+                testUnaryOpLowering @(IntN 5) @(WordN 5) unboundedConfig bvToUnsignedTerm "toUnsigned" SBV.sFromIntegral+                testUnaryOpLowering @(IntN 5) @(WordN 5) boundedConfig bvToUnsignedTerm "toUnsigned" SBV.sFromIntegral             ],           testGroup             "WordN"@@ -773,6 +776,9 @@                 testBinaryOpLowering @(WordN 5) @(WordN 5) @(WordN 5) boundedConfig quotIntegralTerm "quot" SBV.sQuot,               testCase "Rem" $ do                 testBinaryOpLowering @(WordN 5) @(WordN 5) @(WordN 5) unboundedConfig remIntegralTerm "rem" SBV.sRem-                testBinaryOpLowering @(WordN 5) @(WordN 5) @(WordN 5) boundedConfig remIntegralTerm "rem" SBV.sRem+                testBinaryOpLowering @(WordN 5) @(WordN 5) @(WordN 5) boundedConfig remIntegralTerm "rem" SBV.sRem,+              testCase "ToSigned" $ do+                testUnaryOpLowering @(WordN 5) @(IntN 5) unboundedConfig bvToSignedTerm "toSigned" SBV.sFromIntegral+                testUnaryOpLowering @(WordN 5) @(IntN 5) boundedConfig bvToSignedTerm "toSigned" SBV.sFromIntegral             ]         ]

@@ -5,6 +5,7 @@ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-}+{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}@@ -186,10 +187,14 @@   ( TermRewritingSpec a (bv an),     TermRewritingSpec b (bv bn),     TermRewritingSpec c (bv (an + bn)),+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat an,     KnownNat bn,+    KnownNat (an + bn),     1 <= an,     1 <= bn,+    1 <= an + bn,     SizedBV bv   ) =>   a ->@@ -200,6 +205,8 @@ bvselectSpec ::   ( TermRewritingSpec a (bv an),     TermRewritingSpec b (bv bn),+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat an,     KnownNat ix,     KnownNat bn,@@ -218,9 +225,12 @@ bvextendSpec ::   ( TermRewritingSpec a (bv an),     TermRewritingSpec b (bv bn),+    forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    Typeable bv,     KnownNat an,     KnownNat bn,     1 <= an,+    1 <= bn,     an <= bn,     SizedBV bv   ) =>@@ -470,7 +480,8 @@  dsbv1 ::   forall proxy bv.-  ( SupportedBV bv 1,+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    SupportedBV bv 1,     SupportedBV bv 2,     SupportedBV bv 3,     SupportedBV bv 4,@@ -521,7 +532,8 @@  dsbv2 ::   forall proxy bv.-  ( SupportedBV bv 1,+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    SupportedBV bv 1,     SupportedBV bv 2,     SupportedBV bv 3,     SupportedBV bv 4,@@ -572,7 +584,8 @@  dsbv3 ::   forall proxy bv.-  ( SupportedBV bv 1,+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    SupportedBV bv 1,     SupportedBV bv 2,     SupportedBV bv 3,     SupportedBV bv 4,@@ -622,7 +635,8 @@  dsbv4 ::   forall proxy bv.-  ( SupportedBV bv 1,+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    SupportedBV bv 1,     SupportedBV bv 2,     SupportedBV bv 3,     SupportedBV bv 4,@@ -673,7 +687,8 @@ dsbv4 _ _ = error "Should never be called"  instance-  ( SupportedBV bv 1,+  ( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),+    SupportedBV bv 1,     SupportedBV bv 2,     SupportedBV bv 3,     SupportedBV bv 4,

@@ -37,19 +37,19 @@   Property binaryConform a2b c2d f2e f g x y = ioProperty $ f x y @=? f2e (g (a2b x) (c2d y)) -wordUnaryConform :: HasCallStack => (WordN 8 -> WordN 8) -> (Word8 -> Word8) -> Word8 -> Assertion+wordUnaryConform :: (HasCallStack) => (WordN 8 -> WordN 8) -> (Word8 -> Word8) -> Word8 -> Assertion wordUnaryConform f g x = unWordN (f (fromIntegral x)) @=? toInteger (g x) -wordUnaryNonNegIntConform :: HasCallStack => (Int -> WordN 8) -> (Int -> Word8) -> Int -> Assertion+wordUnaryNonNegIntConform :: (HasCallStack) => (Int -> WordN 8) -> (Int -> Word8) -> Int -> Assertion wordUnaryNonNegIntConform f g y = when (y >= 0) $ unWordN (f y) @=? toInteger (g y) -wordBinIntConform :: HasCallStack => (WordN 8 -> Int -> WordN 8) -> (Word8 -> Int -> Word8) -> Word8 -> Int -> Assertion+wordBinIntConform :: (HasCallStack) => (WordN 8 -> Int -> WordN 8) -> (Word8 -> Int -> Word8) -> Word8 -> Int -> Assertion wordBinIntConform f g x y = unWordN (f (fromIntegral x) y) @=? toInteger (g x y) -wordBinNonNegIntConform :: HasCallStack => (WordN 8 -> Int -> WordN 8) -> (Word8 -> Int -> Word8) -> Word8 -> Int -> Assertion+wordBinNonNegIntConform :: (HasCallStack) => (WordN 8 -> Int -> WordN 8) -> (Word8 -> Int -> Word8) -> Word8 -> Int -> Assertion wordBinNonNegIntConform f g x y = when (y >= 0) $ unWordN (f (fromIntegral x) y) @=? toInteger (g x y) -wordBinConform :: HasCallStack => (WordN 8 -> WordN 8 -> WordN 8) -> (Word8 -> Word8 -> Word8) -> Word8 -> Word8 -> Assertion+wordBinConform :: (HasCallStack) => (WordN 8 -> WordN 8 -> WordN 8) -> (Word8 -> Word8 -> Word8) -> Word8 -> Word8 -> Assertion wordBinConform f g x y = unWordN (f (fromIntegral x) (fromIntegral y)) @=? toInteger (g x y)  intN8eqint8 :: IntN 8 -> Int8 -> Assertion@@ -102,7 +102,7 @@       testCase "maxBound" $ (maxBound :: typ) @=? fromIntegral (maxBound :: ref)     ] -shouldThrow :: NFData a => String -> a -> IO ()+shouldThrow :: (NFData a) => String -> a -> IO () shouldThrow name x = do   errored <- catch (evaluate $ x `deepseq` True) (\(_ :: SomeException) -> return False)   when errored $ assertFailure $ name ++ " should throw an exception"