grisette 0.9.0.0 → 0.10.0.0

raw patch · 64 files changed

+3069/−1010 lines, 64 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +25/−1
• README.md +164/−140
• grisette.cabal +15/−5
• src/Grisette/Core.hs +26/−0
• src/Grisette/Internal/Core/Data/Class/SymFiniteBits.hs +9/−6
• src/Grisette/Internal/SymPrim/SomeBV.hs +232/−68
• src/Grisette/Internal/SymPrim/SymPrim.hs +87/−0
• src/Grisette/Internal/TH/Ctor/Common.hs +61/−0
• src/Grisette/Internal/TH/Ctor/SmartConstructor.hs +180/−0
• src/Grisette/Internal/TH/Ctor/UnifiedConstructor.hs +187/−0
• src/Grisette/Internal/TH/GADT/Common.hs +99/−0
• src/Grisette/Internal/TH/GADT/DeriveEvalSym.hs +77/−0
• src/Grisette/Internal/TH/GADT/DeriveExtractSym.hs +75/−0
• src/Grisette/Internal/TH/GADT/DeriveGADT.hs +136/−0
• src/Grisette/Internal/TH/GADT/DeriveMergeable.hs +614/−0
• src/Grisette/Internal/TH/GADT/UnaryOpCommon.hs +212/−0
• src/Grisette/Internal/TH/MergeConstructor.hs +0/−147
• src/Grisette/Internal/TH/UnifiedConstructor.hs +0/−156
• src/Grisette/Lib/Control/Monad.hs +3/−3
• src/Grisette/Lib/Data/Bool.hs +3/−4
• src/Grisette/Lib/Data/Either.hs +3/−4
• src/Grisette/Lib/Data/Foldable.hs +5/−5
• src/Grisette/Lib/Data/Functor/Sum.hs +3/−4
• src/Grisette/Lib/Data/Maybe.hs +3/−4
• src/Grisette/Lib/Data/Tuple.hs +10/−11
• src/Grisette/SymPrim.hs +10/−0
• src/Grisette/TH.hs +24/−12
• src/Grisette/Unified.hs +8/−0
• src/Grisette/Unified/Internal/BVBVConversion.hs +3/−3
• src/Grisette/Unified/Internal/BVFPConversion.hs +3/−3
• src/Grisette/Unified/Internal/BaseConstraint.hs +1/−32
• src/Grisette/Unified/Internal/BaseMonad.hs +4/−4
• src/Grisette/Unified/Internal/Class/UnifiedFiniteBits.hs +21/−21
• src/Grisette/Unified/Internal/Class/UnifiedFromIntegral.hs +31/−31
• src/Grisette/Unified/Internal/Class/UnifiedITEOp.hs +3/−3
• src/Grisette/Unified/Internal/Class/UnifiedRep.hs +108/−0
• src/Grisette/Unified/Internal/Class/UnifiedSafeBitCast.hs +7/−7
• src/Grisette/Unified/Internal/Class/UnifiedSafeDiv.hs +16/−16
• src/Grisette/Unified/Internal/Class/UnifiedSafeFdiv.hs +4/−4
• src/Grisette/Unified/Internal/Class/UnifiedSafeFromFP.hs +13/−13
• src/Grisette/Unified/Internal/Class/UnifiedSafeLinearArith.hs +16/−16
• src/Grisette/Unified/Internal/Class/UnifiedSafeSymRotate.hs +13/−13
• src/Grisette/Unified/Internal/Class/UnifiedSafeSymShift.hs +13/−13
• src/Grisette/Unified/Internal/Class/UnifiedSolvable.hs +136/−0
• src/Grisette/Unified/Internal/Class/UnifiedSymEq.hs +3/−3
• src/Grisette/Unified/Internal/Class/UnifiedSymOrd.hs +3/−3
• src/Grisette/Unified/Internal/EvalMode.hs +13/−13
• src/Grisette/Unified/Internal/EvalModeTag.hs +5/−5
• src/Grisette/Unified/Internal/FPFPConversion.hs +3/−3
• src/Grisette/Unified/Internal/UnifiedAlgReal.hs +26/−22
• src/Grisette/Unified/Internal/UnifiedBV.hs +30/−34
• src/Grisette/Unified/Internal/UnifiedBool.hs +19/−10
• src/Grisette/Unified/Internal/UnifiedConstraint.hs +0/−27
• src/Grisette/Unified/Internal/UnifiedData.hs +11/−11
• src/Grisette/Unified/Internal/UnifiedFP.hs +17/−18
• src/Grisette/Unified/Internal/UnifiedFun.hs +11/−11
• src/Grisette/Unified/Internal/UnifiedInteger.hs +22/−20
• src/Grisette/Unified/Internal/UnifiedPrim.hs +59/−0
• src/Grisette/Unified/Internal/Util.hs +4/−4
• test/Grisette/Core/Data/Class/SymFiniteBitsTests.hs +25/−25
• test/Grisette/Core/TH/DerivationTest.hs +62/−7
• test/Grisette/SymPrim/SomeBVTests.hs +48/−0
• test/Grisette/Unified/EvalModeTest.hs +39/−39
• test/Grisette/Unified/UnifiedConstructorTest.hs +6/−6

@@ -6,6 +6,29 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [0.10.0.0] - 2024-12-11++### Added++- `SomeBV` now allows being used under conditionals even if no bit-width is+  specified. ([#261](https://github.com/lsrcz/grisette/pull/261))+- Added interface to smart constructor generation with decapitalized names.+  ([#263](https://github.com/lsrcz/grisette/pull/263))+- Added `SymPrim` constraints for symbolic primitive types.+  ([#264](https://github.com/lsrcz/grisette/pull/264))+- Added initial support for type class derivation for GADTs.+  ([#265](https://github.com/lsrcz/grisette/pull/265))++### Changed+- [Breaking] Improved the `SymFiniteBits` interface.+  ([#262](https://github.com/lsrcz/grisette/pull/262))+- [Breaking] Changed the smart constructor generation Template Haskell procedure+  name to `makeSmartCtorWith`, `makePrefixedSmartCtorWith`,+  `makeNamedSmartCtor`, and `makeSmartCtor`.+  ([#263](https://github.com/lsrcz/grisette/pull/263))+- [Breaking] Renamed the evaluation mode tags `Con` and `Sym` to `C` and `S`.+  ([#264](https://github.com/lsrcz/grisette/pull/264))+ ## [0.9.0.0] - 2024-11-07  ### Added@@ -497,7 +520,8 @@  - Initial release for Grisette. -[Unreleased]: https://github.com/lsrcz/grisette/compare/v0.9.0.0...HEAD+[Unreleased]: https://github.com/lsrcz/grisette/compare/v0.10.0.0...HEAD+[0.10.0.0]: https://github.com/lsrcz/grisette/compare/v0.9.0.0...v0.10.0.0 [0.9.0.0]: https://github.com/lsrcz/grisette/compare/v0.8.0.0...v0.9.0.0 [0.8.0.0]: https://github.com/lsrcz/grisette/compare/v0.7.0.0...v0.8.0.0 [0.7.0.0]: https://github.com/lsrcz/grisette/compare/v0.6.0.0...v0.7.0.0

@@ -2,32 +2,32 @@  [![Haskell Tests](https://github.com/lsrcz/grisette/actions/workflows/test.yml/badge.svg)](https://github.com/lsrcz/grisette/actions/workflows/test.yml) [![Hackage Version](https://img.shields.io/hackage/v/grisette)](https://hackage.haskell.org/package/grisette)-[![Hackage Dependencies](https://img.shields.io/hackage-deps/v/grisette)](https://packdeps.haskellers.com/feed?needle=grisette) -Grisette is a symbolic evaluation library for Haskell. By translating-programs into constraints, Grisette can help the development of program-reasoning tools, including verification and synthesis.+Grisette is a symbolic evaluation library for Haskell.+By translating programs into SMT constraints, Grisette can help the development+of program reasoning tools, including verification and synthesis.  For a detailed description of the system, please refer to our POPL'23 paper [Grisette: Symbolic Compilation as a Functional Programming Library](https://lsrcz.github.io/files/POPL23.pdf). -## Features--- **Multi-path** symbolic evaluation with efficient (customizable) state merging.-- Symbolic evaluation is **purely functional**. The propagated symbolic value includes the assertion / error state of the execution, yet it is just a data structure. As a result, Grisette is a library that does not modify the Haskell compiler.-- The separation of symbolic and concrete values is enforced with **static types**. These types help discover opportunities for partial evaluation as well as safe use of Haskell libraries.- ## Design and Benefits -- Modular purely functional design, with a focus on composability.+- **Separate the concern** of problem modeling and symbolic compilation. Users+  only need to focus on modeling the problem and write interpreters, and the+  symbolic compilation algorithms are provided by Grisette.+- **Supports rich theories** including booleans, uninterpreted functions,+  bitvectors, integers, real numbers, and floating points.+- **Multi-path symbolic evaluation** with efficient state merging, suitable for+  whole program verification, program synthesis, and other symbolic reasoning+  tasks.+- **Modular purely functional design**, with a focus on composability.+  - Use our familiar Haskell facilities like `Either` to maintain exceptions+    (e.g., assertions and assumptions).   - Allows for symbolic evaluation of user-defined data structures / data     structures from third-party libraries.-  - Allows for symbolic evaluation of error-handling code with user-defined-    error types.-  - Allows for memoization (tested and benchmarked) / parallelization (not-    tested and benchmarked yet) of symbolic evaluation.-- Core multi-path symbolic evaluation semantics modeled as a monad, allowing for-  easy integration with other monadic effects, for example:+  - Allows for memoization / parallelization of symbolic evaluation.+- **Core multi-path symbolic evaluation semantics modeled as a monad**, allowing+  for easy integration with other monadic effects, for example:   - error handling via `ExceptT`,   - stateful computation via `StateT`,   - unstructured control flow via `ContT`, etc.@@ -36,34 +36,45 @@  ### Install Grisette -Grisette is available via-[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.+Grisette is available on [Hackage](https://hackage.haskell.org/package/grisette)+and Stackage. You can add it to your project with `cabal`, and we also provided+a stack template for quickly starting a new project with Grisette.  #### Manually writing cabal file -Grisette is a library and is usually used as a dependency of other-packages. You can add it to your project's `.cabal` file:+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.9 < 0.10+  build-depends: grisette >= 0.10 < 0.11 ``` -#### Quick start template with `stack new`+#### Using stack -You can quickly start an stack-based Grisette project with `stack new`:+Note: Grisette on Stackage is currently outdated. Please make sure to use+`extra-deps` to get the latest version of Grisette from stackage. In your+`stack.yaml` file, add: -```bash-$ stack new <projectname> github:lsrcz/grisette+```yaml+extra-deps:+  - grisette-0.10.0.0 ``` -You can specify the resolver version with the parameters:+and in your `package.yaml` file: +```yaml+dependencies:+  - grisette >= 0.10 < 0.11+```++#### Quick start template with `stack new`++You can quickly start an stack-based Grisette project with `stack new`:+ ```bash-$ stack new a-new-project github:lsrcz/grisette -p "resolver:lts-22.27"+$ stack new <projectname> github:lsrcz/grisette ```  For more details, please see the@@ -116,148 +127,161 @@  ## Example -The following example uses Grisette to build a synthesizer of arithmetic-programs. Given the input-output pair (2,5), the synthesizer can tell us that-the program `\x -> x+3` has the desired behavior. The example is adapted from-[this blog-post](https://www.cs.utexas.edu/~bornholt/post/building-synthesizer.html) by-James Bornholt.--The example has three parts:+The following example uses Grisette to build a symbolic domain-specific language+for boolean and integer expressions. -- We define the arithmetic language. The language is _symbolic_:-  - its syntax tree represents a set of concrete syntax trees (i.e.,-    representing a program space), and-  - its interpreter accepts such symbolic syntax trees (program spaces), and-    interpret all represented concrete syntax trees to symbolic formulas.-- We define the candidate program space of the synthesizer by creating a-  particular symbolic syntax tree. The synthesizer will search the space of-  concrete trees for a solution.-- We interpret the symbolic syntax tree and pass the resulting constraints to-  the solver. If a solution exists, the solver returns a concrete tree that-  agrees with the input-output example.+We will+- define the *syntax* and *semantics* of an arithmetic language, and+- build a *verifier* to check if a given arithmetic expression is equivalent to+  another, and+- build a *synthesizer* to find an arithmetic expression that is equivalent to+  a given expression. -### Defining the Arithmetic Language+### Defining the Syntax -We will synthesize a single-input program `\x -> E` in this example. Here the-`E` is an expression type, and is defined by the following grammar.+Our language is a simple boolean and integer expression language, following the+grammar: +```haskell+Expr -> IntExpr | BoolExpr+IntExpr -> IntVal int+         | Add IntExpr IntExpr+         | Mul IntExpr IntExpr+BoolExpr -> BoolVal bool+          | BAnd BoolExpr BoolExpr+          | BOr BoolExpr BoolExpr+          | Eq Expr Expr ```-E -> c      -- constant-   | x      -- value for input variable-   | E + E  -- addition-   | E * E  -- multiplication++A symbolic expression can be represented in Grisette as a GADT as follows. In+the GADT,++- `SymInteger` and `SymBool` are symbolic (primitive) types, and they represent+  SMT terms of integer and boolean theories, respectively.+- `Union` represents choices of symbolic expressions, and we introduce it to+  represent program spaces and allow the synthesizer to choose operands from+  different symbolic expressions.+- `BasicSymPrim` is a constraint that contains all the symbolic primitive types+  that Grisette supports, including `SymInteger` and `SymBool`.++```haskell+data Expr a where+  IntVal :: SymInteger -> IntExpr+  BoolVal :: SymBool -> BoolExpr+  Add :: UIntExpr -> UIntExpr -> IntExpr+  Mul :: UIntExpr -> UIntExpr -> IntExpr+  BAnd :: UBoolExpr -> UBoolExpr -> BoolExpr+  BOr :: UBoolExpr -> UBoolExpr -> BoolExpr+  Eq :: (BasicSymPrim a) => UExpr a -> UExpr a -> BoolExpr++type IntExpr = Expr SymInteger+type BoolExpr = Expr SymBool+type UExpr a = Union (Expr a)+type UIntExpr = UExpr SymInteger+type UBoolExpr = UExpr SymBool ``` -The syntax defines how a concrete expression is represented. To synthesize a-program, we need to define ***symbolic*** program spaces. We do this with the-`Union` container provided by Grisette to represent choices within multiple ASTs-compactly in a single value.+To make this GADT works well with Grisette, we need to derive some instances and+get some smart constructors: +- `deriveGADTAll` derives all the instances related to Grisette, and+- `makeSmartCtor` generates smart constructors for the GADT.+ ```haskell-data SymExpr-  -- `SymConst` represents a constant in the syntax tree.-  ---  -- `SymConst 1` is the constant 1, while `SymConst "c1"` is a symbolic-  -- constant, representing a hole in the expression. The solver can be used to-  -- find out what the concrete value for a symbolic constant should be.-  = SymConst SymInteger-  -- `SymInput` is exactly the same as `SymConst`, but is for inputs. We-  -- separate them just for clarity.-  | SymInput SymInteger-  -- `SymAdd` and `SymMul` represent the addition and multiplication operators.-  ---  -- The children are **choices** from some symbolic expressions, which is-  -- represented by the `Union` monadic container.-  ---  -- The solver will try to pick one choice from them.-  | SymAdd (Union SymExpr) (Union SymExpr)-  | SymMul (Union SymExpr) (Union SymExpr)-  -- `Generic` helps us derive other type class instances for `SymExpr`.-  deriving stock (Generic, Show)-  -- Some type classes provided by Grisette for building symbolic evaluation-  -- tools. See the documentation for more details.-  deriving (Mergeable, EvalSym) via (Default SymExpr)+deriving instance Show (Expr a)+deriveGADTAll ''Expr+makeSmartCtor ''Expr --- The following template haskell procedures can also derive the instances we--- need.--- derive ''SymExpr [''Generic, ''Show, ''Mergeable, ''EvalSym]--- deriveAllExcept ''SymExpr [''Ord]+> intVal 1 :: UIntExpr -- smart constructor for IntVal in Unions+{IntVal 1}+-- Add takes two UIntExprs, use the smart constructors+> Add (intVal "a") (intVal 1)+Add {IntVal a} {IntVal 1} ``` -Some smart constructors help us build program spaces.+The introduction of `Union` allows us to represent choices of expressions, and+the following code chooses between `a + 2` or `a * 2`. A synthesizer can then pick+true or false for the `choice` variable to decide which expression to pick. If+the synthesizer picks true, the result is `a + 2`; otherwise, it is `a * 2`.  ```haskell--- A template haskell procedure generates smart constructors for--- `Union SymExpr`.------ >>> SymConst 1 :: SymExpr--- SymConst 1--- >>> mrgSymConst 1 :: Union SymExpr--- {SymConst 1}-mkMergeConstructor "mrg" ''SymExpr+add2 = add (intVal "a") (intVal 2)+mul2 = mul (intVal "a") (intVal 2)+> mrgIf "choice" add2 mul2 :: UIntExpr+{If choice {Add {IntVal a} {IntVal 2}} {Mul {IntVal a} {IntVal 2}}} ``` -Then, the following code defines a program space `\x -> x + {x, c}`. Some-example programs in this space are `\x -> x + x`, `\x -> x + 1`, and `\x -> x +-2`. The solver will be used to choose the right hand side of the addition. It-may choose to use the input variable `x`, or synthesize a constant `c`.+### Defining the Semantics+The semantics of the expressions can be defined by the following interpreter.+Grisette provides various combinators for working with symbolic values. In the+interpreter, the `.#` operator is very important. It conceptually +- extracts all the choices from the `Union` container,+- apply the `eval` function to each choice, and+- merge the results into a single value.+ ```haskell-progSpace :: SymInteger -> SymExpr-progSpace x =-  SymAdd-    (mrgSymInput x)-    (mrgIf "choice" (mrgSymInput x) (mrgSymConst "c"))+eval :: Expr a -> a+eval (IntVal a) = a+eval (BoolVal a) = a+eval (Add a b) = eval .# a + eval .# b+eval (Mul a b) = eval .# a * eval .# b+eval (BAnd a b) = eval .# a .&& eval .# b+eval (BOr a b) = eval .# a .|| eval .# b+eval (Eq a b) = eval .# a .== eval .# b ``` -We can then convert this program space to its logical encoding and reason about-it. This is done simply writing an interpreter to interpret all the expressions-represented by an `SymExpr` all at once.+There are other operators like `.==`, `.&&`, `.||`, etc. These operators are+provided by Grisette and have symbolic semantics. They construct constraints+instead of evaluating to a concrete value. -The interpreter is similar to a concrete interpreter, except that the `onUnion`-combinator is used to lift the interpreter to work on `Union` values (a space of-expressions).+We may also write `eval` with do-notations as `Union` is a monad. Please refer+to the [tutorials](tutorials) for more details. +### Get a verifier+With the syntax and semantics defined, we can build a verifier to check if two+expressions are equivalent. This can be done by checking if there exists a+counter-example that falsifies the equivalence of the two expressions.++In the following code, we verify that $a+b$ and $b+a$ are equivalent, as there+does not exist a counter-example that makes the two expressions evaluate to+different values.+ ```haskell-interpret :: SymExpr -> SymInteger-interpret (SymConst x) = x-interpret (SymInput x) = x-interpret (SymAdd x y) = interpretSpace x + interpretSpace y-interpret (SymMul x y) = interpretSpace x * interpretSpace y+lhs = Add (intVal "a") (intVal "b")+rhs = Add (intVal "b") (intVal "a")+rhs2 = Add (intVal "a") (intVal "a") --- interpret a program space-interpretSpace :: Union SymExpr -> SymInteger-interpretSpace = onUnion interpret+> solve z3 $ eval lhs ./= eval rhs+Left Unsat ``` -We can then compose the interpreter with the program space to make it-executable.+In the following code, we verify that $a+b$ and $a+a$ are not equivalent, as+there exists a counter-example that makes the two expressions evaluate to+different values. The counter-example is $a=0$, $b=1$, such that $a+b=1$ and+$a+a=0$. -```haskell-executableSpace :: Integer -> SymInteger-executableSpace = interpret . space . toSym+``` haskell+> solve z3 $ eval lhs ./= eval rhs2+Right (Model {a -> 0 :: Integer, b -> 1 :: Integer}) ``` -Then we can do synthesis. We call the program space on the input 2, and-construct the constraint that the result is equal to 5. We then call the solver-with the `solve` function. The solver finds a solution such that the condition-evaluates to true. It returns the solution as a *model*, which contains an-assignment to the symbolic constants (holes).+### Get a synthesizer+We can also build a synthesizer using the built-in CEGIS algorithm in Grisette.+Given a target expression, we can synthesize an expression using a sketch with+"symbolic holes" that is equivalent to the target expression. -We can then get the synthesized program by evaluating the program space with the-model.+In the following code, we synthesize an expression that is equivalent to $a+a$+using a sketch with a "symbolic hole" $c$. The `cegisForAll` function treats all+the variables in the sketch but not in the target expression as holes to fill+in.  ```haskell-example :: IO ()-example = do-  Right model <- solve z3 $ executableSpace 2 .== 5-  -- result: SymPlus {SymInput x} {SymConst 3}-  print $ evalSym False model (progSpace "x")-  let synthesizedProgram :: Integer -> Integer =-        evalSymToCon model . executableSpace-  -- result: 13-  print $ synthesizedProgram 10+target = Add (intVal "a") (intVal "a")+sketch = Mul (intVal "a") (intVal "c")++> cegisForAll z3 target $ cegisPostCond $ eval target .== eval sketch+([],CEGISSuccess (Model {c -> 2 :: Integer})) ```  The complete code is at [examples/basic/Main.hs](examples/basic/Main.hs). More

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           grisette-version:        0.9.0.0+version:        0.10.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@@ -38,7 +38,7 @@   , GHC == 9.2.8   , GHC == 9.4.8   , GHC == 9.6.6-  , GHC == 9.8.2+  , GHC == 9.8.3   , GHC == 9.10.1 extra-source-files:     CHANGELOG.md@@ -151,16 +151,24 @@       Grisette.Internal.SymPrim.SymFP       Grisette.Internal.SymPrim.SymGeneralFun       Grisette.Internal.SymPrim.SymInteger+      Grisette.Internal.SymPrim.SymPrim       Grisette.Internal.SymPrim.SymTabularFun       Grisette.Internal.SymPrim.TabularFun+      Grisette.Internal.TH.Ctor.Common+      Grisette.Internal.TH.Ctor.SmartConstructor+      Grisette.Internal.TH.Ctor.UnifiedConstructor       Grisette.Internal.TH.DeriveBuiltin       Grisette.Internal.TH.DeriveInstanceProvider       Grisette.Internal.TH.DerivePredefined       Grisette.Internal.TH.DeriveTypeParamHandler       Grisette.Internal.TH.DeriveUnifiedInterface       Grisette.Internal.TH.DeriveWithHandlers-      Grisette.Internal.TH.MergeConstructor-      Grisette.Internal.TH.UnifiedConstructor+      Grisette.Internal.TH.GADT.Common+      Grisette.Internal.TH.GADT.DeriveEvalSym+      Grisette.Internal.TH.GADT.DeriveExtractSym+      Grisette.Internal.TH.GADT.DeriveGADT+      Grisette.Internal.TH.GADT.DeriveMergeable+      Grisette.Internal.TH.GADT.UnaryOpCommon       Grisette.Internal.TH.Util       Grisette.Internal.Utils.Derive       Grisette.Internal.Utils.Parameterized@@ -195,6 +203,7 @@       Grisette.Unified.Internal.Class.UnifiedFiniteBits       Grisette.Unified.Internal.Class.UnifiedFromIntegral       Grisette.Unified.Internal.Class.UnifiedITEOp+      Grisette.Unified.Internal.Class.UnifiedRep       Grisette.Unified.Internal.Class.UnifiedSafeBitCast       Grisette.Unified.Internal.Class.UnifiedSafeDiv       Grisette.Unified.Internal.Class.UnifiedSafeFdiv@@ -203,6 +212,7 @@       Grisette.Unified.Internal.Class.UnifiedSafeSymRotate       Grisette.Unified.Internal.Class.UnifiedSafeSymShift       Grisette.Unified.Internal.Class.UnifiedSimpleMergeable+      Grisette.Unified.Internal.Class.UnifiedSolvable       Grisette.Unified.Internal.Class.UnifiedSymEq       Grisette.Unified.Internal.Class.UnifiedSymOrd       Grisette.Unified.Internal.EvalMode@@ -212,11 +222,11 @@       Grisette.Unified.Internal.UnifiedAlgReal       Grisette.Unified.Internal.UnifiedBool       Grisette.Unified.Internal.UnifiedBV-      Grisette.Unified.Internal.UnifiedConstraint       Grisette.Unified.Internal.UnifiedData       Grisette.Unified.Internal.UnifiedFP       Grisette.Unified.Internal.UnifiedFun       Grisette.Unified.Internal.UnifiedInteger+      Grisette.Unified.Internal.UnifiedPrim       Grisette.Unified.Internal.Util       Grisette.Unified.Lib.Control.Applicative       Grisette.Unified.Lib.Control.Monad

@@ -358,6 +358,18 @@     SymRotate (..),     SafeSymRotate (..),     SignConversion (..),+    lsb,+    msb,+    setBitTo,+    bitBlast,+    FromBits (..),+    SymFiniteBits (..),+    symBitBlast,+    symLsb,+    symMsb,+    symPopCount,+    symCountLeadingZeros,+    symCountTrailingZeros,      -- ** Safe operation for Numbers     DivOr (..),@@ -1724,6 +1736,20 @@     genericSymEq,     symEq1,     symEq2,+  )+import Grisette.Internal.Core.Data.Class.SymFiniteBits+  ( FromBits (..),+    SymFiniteBits (..),+    bitBlast,+    lsb,+    msb,+    setBitTo,+    symBitBlast,+    symCountLeadingZeros,+    symCountTrailingZeros,+    symLsb,+    symMsb,+    symPopCount,   ) import Grisette.Internal.Core.Data.Class.SymFromIntegral   ( SymFromIntegral (..),

@@ -182,12 +182,14 @@ symMsb x = symTestBit x (finiteBitSize x - 1)  -- | Count the number of set bits in a symbolic value.-symPopCount :: (Num b, ITEOp b, SymFiniteBits a) => a -> b-symPopCount v = sum $ (\b -> symIte b 1 0) <$> symBitBlast v+symPopCount :: (Num a, ITEOp a, SymFiniteBits a) => a -> a+-- Node: v - v + is a trick to assign the correct bit-width to the result.+symPopCount v = v - v + sum ((\b -> symIte b 1 0) <$> symBitBlast v)  -- | Count the number of leading zeros in a symbolic value.-symCountLeadingZeros :: (Num b, ITEOp b, SymFiniteBits a) => a -> b-symCountLeadingZeros v = go bits rs+symCountLeadingZeros :: (Num a, ITEOp a, SymFiniteBits a) => a -> a+-- Node: v - v + is a trick to assign the correct bit-width to the result.+symCountLeadingZeros v = v - v + go bits rs   where     bits = reverse $ symBitBlast v     rs = fromIntegral <$> [0 ..]@@ -196,8 +198,9 @@     go _ [] = error "Should not happen"  -- | Count the number of trailing zeros in a symbolic value.-symCountTrailingZeros :: (Num b, ITEOp b, SymFiniteBits a) => a -> b-symCountTrailingZeros v = go bits rs+symCountTrailingZeros :: (Num a, ITEOp a, SymFiniteBits a) => a -> a+-- Node: v - v + is a trick to assign the correct bit-width to the result.+symCountTrailingZeros v = v - v + go bits rs   where     bits = symBitBlast v     rs = fromIntegral <$> [0 ..]

@@ -1,12 +1,14 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveLift #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternSynonyms #-}@@ -142,12 +144,13 @@ import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte)) import Grisette.Internal.Core.Data.Class.Mergeable   ( Mergeable (rootStrategy),-    MergingStrategy (SortedStrategy),+    MergingStrategy (SimpleStrategy, SortedStrategy),     wrapStrategy,   ) import Grisette.Internal.Core.Data.Class.PPrint   ( PPrint (pformat),   )+import Grisette.Internal.Core.Data.Class.PlainUnion (simpleMerge) import Grisette.Internal.Core.Data.Class.SafeDiv   ( DivOr (divModOr, divOr, modOr, quotOr, quotRemOr, remOr),     SafeDiv (safeDiv, safeDivMod, safeMod, safeQuot, safeQuotRem, safeRem),@@ -169,6 +172,7 @@ import Grisette.Internal.Core.Data.Class.SignConversion   ( SignConversion (toSigned, toUnsigned),   )+import Grisette.Internal.Core.Data.Class.SimpleMergeable (mrgIf) import Grisette.Internal.Core.Data.Class.Solvable   ( Solvable (con, conView, isym, ssym, sym),   )@@ -189,7 +193,7 @@   ) import Grisette.Internal.Core.Data.Class.ToCon (ToCon (toCon)) import Grisette.Internal.Core.Data.Class.ToSym (ToSym (toSym))-import Grisette.Internal.Core.Data.Class.TryMerge (TryMerge, tryMerge)+import Grisette.Internal.Core.Data.Class.TryMerge (TryMerge, mrgSingle, tryMerge) import Grisette.Internal.Core.Data.Symbol (Identifier, Symbol) import Grisette.Internal.SymPrim.AllSyms (AllSyms (allSyms, allSymsS)) import Grisette.Internal.SymPrim.BV@@ -239,9 +243,36 @@   displayException (UndeterminedBitwidth msg) =     "Cannot determine bit-width for literals: " <> T.unpack msg +class MaySomeBV bv where+  assignLitBitWidth :: (KnownNat n, 1 <= n) => SomeBVLit -> bv n++instance MaySomeBV IntN where+  assignLitBitWidth = \case+    SomeBVIntLit i -> fromInteger i+    SomeBVCondLit _ -> error "Should not happen"++instance MaySomeBV WordN where+  assignLitBitWidth = \case+    SomeBVIntLit i -> fromInteger i+    SomeBVCondLit _ -> error "Should not happen"++instance MaySomeBV SymIntN where+  assignLitBitWidth = \case+    SomeBVIntLit i -> fromInteger i+    SomeBVCondLit u -> simpleMerge $ do+      i <- u+      mrgSingle $ fromInteger i++instance MaySomeBV SymWordN where+  assignLitBitWidth = \case+    SomeBVIntLit i -> fromInteger i+    SomeBVCondLit u -> simpleMerge $ do+      i <- u+      mrgSingle $ fromInteger i+ assignBitWidthList ::   forall bv.-  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>+  (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) =>   T.Text ->   [SomeBV bv] ->   Either SomeBVException [SomeBV bv]@@ -263,13 +294,13 @@     assignSingleBitWidth ::       forall i. (KnownNat i, 1 <= i) => bv i -> SomeBV bv -> SomeBV bv     assignSingleBitWidth _ s@(SomeBV _) = s-    assignSingleBitWidth _ (SomeBVLit i) = SomeBV (fromIntegral i :: bv i)+    assignSingleBitWidth _ (SomeBVLit i) = SomeBV (assignLitBitWidth i :: bv i)  class AssignBitWidth a where   assignBitWidth :: T.Text -> a -> Either SomeBVException a  instance-  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>+  (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) =>   AssignBitWidth (SomeBV bv, SomeBV bv)   where   assignBitWidth msg (a, b) = do@@ -279,7 +310,7 @@       _ -> error "Should not happen"  instance-  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>+  (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) =>   AssignBitWidth (SomeBV bv, SomeBV bv, SomeBV bv)   where   assignBitWidth msg (a, b, c) = do@@ -289,7 +320,7 @@       _ -> error "Should not happen"  instance-  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>+  (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) =>   AssignBitWidth (SomeBV bv, SomeBV bv, SomeBV bv, SomeBV bv)   where   assignBitWidth msg (a, b, c, d) = do@@ -351,8 +382,110 @@ -- bvlit(6) data SomeBV bv where   SomeBV :: (KnownNat n, 1 <= n) => bv n -> SomeBV bv-  SomeBVLit :: Integer -> SomeBV bv+  SomeBVLit :: SomeBVLit -> SomeBV bv +data SomeBVLit where+  SomeBVIntLit :: Integer -> SomeBVLit+  SomeBVCondLit :: Union Integer -> SomeBVLit+  deriving (Eq, Generic, Lift)+  deriving anyclass (Hashable, NFData)+  deriving (Mergeable, ExtractSym, AllSyms) via (Default SomeBVLit)++instance PPrint SomeBVLit where+  pformat (SomeBVIntLit i) = pformat i+  pformat (SomeBVCondLit u) = pformat u++toUnionInteger :: SomeBVLit -> Union Integer+toUnionInteger (SomeBVIntLit i) = mrgSingle i+toUnionInteger (SomeBVCondLit u) = u++instance Num SomeBVLit where+  SomeBVIntLit a + SomeBVIntLit b = SomeBVIntLit $ a + b+  l + r = SomeBVCondLit $ toUnionInteger l + toUnionInteger r+  SomeBVIntLit a - SomeBVIntLit b = SomeBVIntLit $ a - b+  l - r = SomeBVCondLit $ toUnionInteger l - toUnionInteger r+  SomeBVIntLit a * SomeBVIntLit b = SomeBVIntLit $ a * b+  l * r = SomeBVCondLit $ toUnionInteger l * toUnionInteger r+  negate (SomeBVIntLit a) = SomeBVIntLit $ negate a+  negate l = SomeBVCondLit $ negate $ toUnionInteger l+  abs (SomeBVIntLit a) = SomeBVIntLit $ abs a+  abs l = SomeBVCondLit $ abs $ toUnionInteger l+  signum (SomeBVIntLit a) = SomeBVIntLit $ signum a+  signum l = SomeBVCondLit $ signum $ toUnionInteger l+  fromInteger = SomeBVIntLit++instance Bits SomeBVLit where+  SomeBVIntLit l .&. SomeBVIntLit r = SomeBVIntLit $ l .&. r+  l .&. r = SomeBVCondLit $ do+    l <- toUnionInteger l+    r <- toUnionInteger r+    mrgSingle $ l .&. r+  SomeBVIntLit l .|. SomeBVIntLit r = SomeBVIntLit $ l .|. r+  l .|. r = SomeBVCondLit $ do+    l <- toUnionInteger l+    r <- toUnionInteger r+    mrgSingle $ l .|. r+  SomeBVIntLit l `xor` SomeBVIntLit r = SomeBVIntLit $ l `xor` r+  l `xor` r = SomeBVCondLit $ do+    l <- toUnionInteger l+    r <- toUnionInteger r+    mrgSingle $ l `xor` r+  complement (SomeBVIntLit l) = SomeBVIntLit $ complement l+  complement l = SomeBVCondLit $ do+    l <- toUnionInteger l+    mrgSingle $ complement l+  setBit (SomeBVIntLit l) i = SomeBVIntLit $ setBit l i+  setBit l i = SomeBVCondLit $ do+    l <- toUnionInteger l+    mrgSingle $ setBit l i+  clearBit (SomeBVIntLit l) i = SomeBVIntLit $ clearBit l i+  clearBit l i = SomeBVCondLit $ do+    l <- toUnionInteger l+    mrgSingle $ clearBit l i+  complementBit (SomeBVIntLit l) i = SomeBVIntLit $ complementBit l i+  complementBit l i = SomeBVCondLit $ do+    l <- toUnionInteger l+    mrgSingle $ complementBit l i+  shiftL (SomeBVIntLit a) i = SomeBVIntLit $ shiftL a i+  shiftL l i = SomeBVCondLit $ do+    l <- toUnionInteger l+    mrgSingle $ shiftL l i+  unsafeShiftL (SomeBVIntLit a) i = SomeBVIntLit $ unsafeShiftL a i+  unsafeShiftL l i = SomeBVCondLit $ do+    l <- toUnionInteger l+    mrgSingle $ unsafeShiftL l i+  shift = throw $ UndeterminedBitwidth "shift"+  rotate = throw $ UndeterminedBitwidth "rotate"+  bitSize = throw $ UndeterminedBitwidth "bitSize"+  bitSizeMaybe = throw $ UndeterminedBitwidth "bitSizeMaybe"+  isSigned = error "isSigned is not defined for SomeBVLit"+  testBit = throw $ UndeterminedBitwidth "testBit"+  bit = throw $ UndeterminedBitwidth "bit"+  popCount = throw $ UndeterminedBitwidth "popCount"++instance Show SomeBVLit where+  show (SomeBVIntLit i) = show i+  show (SomeBVCondLit u) = show u++instance Serial SomeBVLit where+  serialize (SomeBVIntLit i) = putWord8 0 >> serialize i+  serialize (SomeBVCondLit u) =+    putWord8 1 >> serialize u+  deserialize = do+    tag <- getWord8+    case tag of+      0 -> SomeBVIntLit <$> deserialize+      1 -> SomeBVCondLit <$> deserialize+      _ -> fail "Invalid tag"++instance Cereal.Serialize SomeBVLit where+  put = serialize+  get = deserialize++instance Binary.Binary SomeBVLit where+  put = serialize+  get = deserialize+ instance   (forall n. (KnownNat n, 1 <= n) => Serial (bv n)) =>   Serial (SomeBV bv)@@ -389,7 +522,8 @@  instance   ( forall n. (KnownNat n, 1 <= n) => Hashable (bv n),-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   Hashable (SomeBV bv)   where@@ -414,6 +548,8 @@   show (SomeBVLit i) = "bvlit(" <> show i <> ")"   {-# INLINE show #-} +-- , MaySomeBV bv+ instance   (forall n. (KnownNat n, 1 <= n) => NFData (bv n)) =>   NFData (SomeBV bv)@@ -424,7 +560,8 @@  instance   ( forall n. (KnownNat n, 1 <= n) => Eq (bv n),-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   Eq (SomeBV bv)   where@@ -432,22 +569,23 @@     case sameNat (Proxy @l) (Proxy @r) of       Just Refl -> l == r       Nothing -> False-  SomeBV (l :: bv l) == SomeBVLit r = l == fromIntegral r-  SomeBVLit l == SomeBV r = fromIntegral l == r-  SomeBVLit _ == SomeBVLit _ = throw $ UndeterminedBitwidth "=="+  SomeBV (l :: bv l) == SomeBVLit r = l == assignLitBitWidth r+  l == r@SomeBV {} = r == l+  _ == _ = throw $ UndeterminedBitwidth "=="   {-# INLINE (==) #-}   SomeBV (l :: bv l) /= SomeBV (r :: bv r) =     case sameNat (Proxy @l) (Proxy @r) of       Just Refl -> l /= r       Nothing -> True-  SomeBV (l :: bv l) /= SomeBVLit r = l /= fromIntegral r-  SomeBVLit l /= SomeBV r = fromIntegral l /= r-  SomeBVLit _ /= SomeBVLit _ = throw $ UndeterminedBitwidth "/="+  SomeBV (l :: bv l) /= SomeBVLit r = l /= assignLitBitWidth r+  l /= r@SomeBV {} = r /= l+  _ /= _ = throw $ UndeterminedBitwidth "/="   {-# INLINE (/=) #-}  instance   ( forall n. (KnownNat n, 1 <= n) => Ord (bv n),-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   Ord (SomeBV bv)   where@@ -467,7 +605,7 @@     binSomeBV compare (const $ const $ throw $ UndeterminedBitwidth "compare")   {-# INLINE compare #-} -instance (forall n. (KnownNat n, 1 <= n) => Num (bv n)) => Num (SomeBV bv) where+instance (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => Num (SomeBV bv) where   (+) = binSomeBVR1 (+) (+)   {-# INLINE (+) #-}   (-) = binSomeBVR1 (-) (-)@@ -480,12 +618,13 @@   {-# INLINE abs #-}   signum = unarySomeBVR1 signum (const $ throw $ UndeterminedBitwidth "signum")   {-# INLINE signum #-}-  fromInteger = SomeBVLit+  fromInteger = SomeBVLit . SomeBVIntLit   {-# INLINE fromInteger #-}  instance   ( forall n. (KnownNat n, 1 <= n) => Bits (bv n),-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   Bits (SomeBV bv)   where@@ -519,7 +658,7 @@       . unarySomeBV         bitSizeMaybe         (const $ throw $ UndeterminedBitwidth "bitSize")-  isSigned _ = False+  isSigned _ = isSigned (undefined :: bv 1)   shiftL s i = unarySomeBVR1 (`shiftL` i) (`shiftL` i) s   unsafeShiftL s i = unarySomeBVR1 (`unsafeShiftL` i) (`unsafeShiftL` i) s   shiftR s i =@@ -544,7 +683,8 @@  instance   ( forall n. (KnownNat n, 1 <= n) => FiniteBits (bv n),-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   FiniteBits (SomeBV bv)   where@@ -578,7 +718,7 @@   {-# INLINE fromEnum #-}  instance-  (forall n. (KnownNat n, 1 <= n) => Real (bv n)) =>+  (forall n. (KnownNat n, 1 <= n) => Real (bv n), MaySomeBV bv) =>   Real (SomeBV bv)   where   toRational =@@ -586,7 +726,7 @@   {-# INLINE toRational #-}  instance-  (forall n. (KnownNat n, 1 <= n) => Integral (bv n)) =>+  (forall n. (KnownNat n, 1 <= n) => Integral (bv n), MaySomeBV bv) =>   Integral (SomeBV bv)   where   toInteger =@@ -728,14 +868,23 @@   Mergeable (SomeBV bv)   where   rootStrategy =-    SortedStrategy @CompileTimeNat-      (\(SomeBV (_ :: bv n)) -> CompileTimeNat (Proxy @n))-      ( \(CompileTimeNat (_ :: proxy n)) ->-          wrapStrategy-            (rootStrategy @(bv n))-            SomeBV-            (\(SomeBV x) -> unsafeCoerce x)+    SortedStrategy @(Maybe CompileTimeNat)+      ( \case+          (SomeBVLit _) -> Nothing+          (SomeBV (_ :: bv n)) -> Just (CompileTimeNat (Proxy @n))       )+      ( \case+          Nothing -> SimpleStrategy $+            \c (SomeBVLit l) (SomeBVLit r) ->+              SomeBVLit $+                SomeBVCondLit $+                  mrgIf c (toUnionInteger l) (toUnionInteger r)+          Just (CompileTimeNat (_ :: proxy n)) ->+            wrapStrategy+              (rootStrategy @(bv n))+              SomeBV+              (\(SomeBV x) -> unsafeCoerce x)+      )  -- | The 'symDistinct' instance for t'SomeBV' will have the following behavior: --@@ -749,7 +898,8 @@ --   formula using @distinct@. instance   ( forall n. (KnownNat n, 1 <= n) => SymEq (bv n),-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   SymEq (SomeBV bv)   where@@ -757,16 +907,16 @@     case sameNat (Proxy @l) (Proxy @r) of       Just Refl -> l .== r       Nothing -> con False-  SomeBV (l :: bv l) .== SomeBVLit r = l .== fromIntegral r-  SomeBVLit l .== SomeBV (r :: bv r) = fromIntegral l .== r+  SomeBV (l :: bv l) .== SomeBVLit r = l .== assignLitBitWidth r+  SomeBVLit l .== SomeBV (r :: bv r) = assignLitBitWidth l .== r   SomeBVLit _ .== SomeBVLit _ = throw $ UndeterminedBitwidth ".=="   {-# INLINE (.==) #-}   SomeBV (l :: bv l) ./= SomeBV (r :: bv r) =     case sameNat (Proxy @l) (Proxy @r) of       Just Refl -> l ./= r       Nothing -> con True-  SomeBV (l :: bv l) ./= SomeBVLit r = l ./= fromIntegral r-  SomeBVLit l ./= SomeBV (r :: bv r) = fromIntegral l ./= r+  SomeBV (l :: bv l) ./= SomeBVLit r = l ./= assignLitBitWidth r+  SomeBVLit l ./= SomeBV (r :: bv r) = assignLitBitWidth l ./= r   SomeBVLit _ ./= SomeBVLit _ = throw $ UndeterminedBitwidth "./="   symDistinct l = case l of     [] -> con True@@ -787,7 +937,8 @@  instance   ( forall n. (KnownNat n, 1 <= n) => SymOrd (bv n),-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   SymOrd (SomeBV bv)   where@@ -936,7 +1087,7 @@ {-# INLINE divRemOrBase0 #-}  divRemOrBase ::-  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>+  (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) =>   ( forall n.     (KnownNat n, 1 <= n) =>     (bv n, bv n) ->@@ -955,7 +1106,8 @@  instance   ( forall n. (KnownNat n, 1 <= n) => DivOr (bv n),-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   DivOr (SomeBV bv)   where@@ -979,7 +1131,8 @@     MonadError (Either SomeBVException e) m,     TryMerge m,     Mergeable e,-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   SafeDiv (Either SomeBVException e) (SomeBV bv) m   where@@ -1021,7 +1174,8 @@     MonadError (Either SomeBVException e) m,     TryMerge m,     Mergeable e,-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   SafeLinearArith (Either SomeBVException e) (SomeBV bv) m   where@@ -1046,7 +1200,8 @@  instance   ( forall n. (KnownNat n, 1 <= n) => SymShift (bv n),-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   SymShift (SomeBV bv)   where@@ -1063,7 +1218,8 @@  instance   ( forall n. (KnownNat n, 1 <= n) => SymRotate (bv n),-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   SymRotate (SomeBV bv)   where@@ -1085,7 +1241,8 @@     MonadError (Either SomeBVException e) m,     TryMerge m,     Mergeable e,-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   SafeSymShift (Either SomeBVException e) (SomeBV bv) m   where@@ -1117,7 +1274,8 @@     MonadError (Either SomeBVException e) m,     TryMerge m,     Mergeable e,-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   SafeSymRotate (Either SomeBVException e) (SomeBV bv) m   where@@ -1134,17 +1292,20 @@  instance   ( forall n. (KnownNat n, 1 <= n) => ITEOp (bv n),-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   ITEOp (SomeBV bv)   where   symIte cond =     binSomeBVR1       (symIte cond)-      (const $ const $ throw $ UndeterminedBitwidth "symIte")+      (\l r -> SomeBVCondLit $ mrgIf cond (toUnionInteger l) (toUnionInteger r))  instance-  (forall n. (KnownNat n, 1 <= n) => AllSyms (bv n)) =>+  ( forall n. (KnownNat n, 1 <= n) => AllSyms (bv n),+    MaySomeBV bv+  ) =>   AllSyms (SomeBV bv)   where   allSyms = unarySomeBV allSyms allSyms@@ -1315,7 +1476,7 @@ unarySomeBV ::   forall bv r.   (forall n. (KnownNat n, 1 <= n) => bv n -> r) ->-  (Integer -> r) ->+  (SomeBVLit -> r) ->   SomeBV bv ->   r unarySomeBV f _ (SomeBV bv) = f bv@@ -1326,7 +1487,7 @@ -- t'SomeBV'. The result will also be wrapped with t'SomeBV'. unarySomeBVR1 ::   (forall n. (KnownNat n, 1 <= n) => bv n -> bv n) ->-  (Integer -> Integer) ->+  (SomeBVLit -> SomeBVLit) ->   SomeBV bv ->   SomeBV bv unarySomeBVR1 f g = unarySomeBV (SomeBV . f) (SomeBVLit . g)@@ -1335,9 +1496,9 @@ -- | Lift a binary operation on sized bitvectors that returns anything to -- t'SomeBV'. Crash if the bitwidths do not match. binSomeBV ::-  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>+  (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) =>   (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> r) ->-  (Integer -> Integer -> r) ->+  (SomeBVLit -> SomeBVLit -> r) ->   SomeBV bv ->   SomeBV bv ->   r@@ -1345,15 +1506,15 @@   case sameNat (Proxy @l) (Proxy @r) of     Just Refl -> f l r     Nothing -> throw BitwidthMismatch-binSomeBV f _ (SomeBV (l :: bv l)) (SomeBVLit r) = f l $ fromIntegral r-binSomeBV f _ (SomeBVLit l) (SomeBV (r :: bv r)) = f (fromIntegral l) r+binSomeBV f _ (SomeBV (l :: bv l)) (SomeBVLit r) = f l $ assignLitBitWidth r+binSomeBV f _ (SomeBVLit l) (SomeBV (r :: bv r)) = f (assignLitBitWidth l) r binSomeBV _ g (SomeBVLit l) (SomeBVLit r) = g l r {-# INLINE binSomeBV #-}  -- | Lift a ternary operation on sized bitvectors that returns anything to -- t'SomeBV'. Crash if the bitwidths do not match. ternSomeBV ::-  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>+  (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) =>   (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n -> r) ->   SomeBV bv ->   SomeBV bv ->@@ -1373,9 +1534,9 @@ -- t'SomeBV'. The result will also be wrapped with t'SomeBV'. Crash if the -- bitwidths do not match. binSomeBVR1 ::-  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>+  (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) =>   (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n) ->-  (Integer -> Integer -> Integer) ->+  (SomeBVLit -> SomeBVLit -> SomeBVLit) ->   SomeBV bv ->   SomeBV bv ->   SomeBV bv@@ -1386,9 +1547,9 @@ -- t'SomeBV'. The results will also be wrapped with t'SomeBV'. Crash if the -- bitwidths do not match. binSomeBVR2 ::-  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>+  (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) =>   (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) ->-  (Integer -> Integer -> (Integer, Integer)) ->+  (SomeBVLit -> SomeBVLit -> (SomeBVLit, SomeBVLit)) ->   SomeBV bv ->   SomeBV bv ->   (SomeBV bv, SomeBV bv)@@ -1402,7 +1563,7 @@ -- t'SomeBV'. The result will also be wrapped with t'SomeBV'. Crash if the -- bitwidths do not match. ternSomeBVR1 ::-  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>+  (forall n. (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) =>   (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n -> bv n) ->   SomeBV bv ->   SomeBV bv ->@@ -1419,10 +1580,11 @@     TryMerge m,     Mergeable e,     Mergeable r,-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m r) ->-  (Integer -> Integer -> ExceptT (Either SomeBVException e) m r) ->+  (SomeBVLit -> SomeBVLit -> ExceptT (Either SomeBVException e) m r) ->   SomeBV bv ->   SomeBV bv ->   m r@@ -1450,10 +1612,11 @@     TryMerge m,     Mergeable e,     forall n. (KnownNat n, 1 <= n) => Mergeable (bv n),-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n)) ->-  (Integer -> Integer -> ExceptT (Either SomeBVException e) m Integer) ->+  (SomeBVLit -> SomeBVLit -> ExceptT (Either SomeBVException e) m SomeBVLit) ->   SomeBV bv ->   SomeBV bv ->   m (SomeBV bv)@@ -1474,7 +1637,8 @@     TryMerge m,     Mergeable e,     forall n. (KnownNat n, 1 <= n) => Mergeable (bv n),-    forall n. (KnownNat n, 1 <= n) => Num (bv n)+    forall n. (KnownNat n, 1 <= n) => Num (bv n),+    MaySomeBV bv   ) =>   ( forall n.     (KnownNat n, 1 <= n) =>@@ -1482,9 +1646,9 @@     bv n ->     ExceptT e m (bv n, bv n)   ) ->-  ( Integer ->-    Integer ->-    ExceptT (Either SomeBVException e) m (Integer, Integer)+  ( SomeBVLit ->+    SomeBVLit ->+    ExceptT (Either SomeBVException e) m (SomeBVLit, SomeBVLit)   ) ->   SomeBV bv ->   SomeBV bv ->

@@ -0,0 +1,87 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}++-- |+-- Module      :   Grisette.Internal.SymPrim.SymPrim+-- Copyright   :   (c) Sirui Lu 2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Internal.SymPrim.SymPrim (Prim, SymPrim, BasicSymPrim) where++import Control.DeepSeq (NFData)+import Data.Binary (Binary)+import Data.Bytes.Serial (Serial)+import Data.Hashable (Hashable)+import Data.Serialize (Serialize)+import Grisette.Internal.Core.Data.Class.EvalSym (EvalSym)+import Grisette.Internal.Core.Data.Class.ExtractSym (ExtractSym)+import Grisette.Internal.Core.Data.Class.Function (Apply)+import Grisette.Internal.Core.Data.Class.GenSym (GenSymSimple)+import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp)+import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)+import Grisette.Internal.Core.Data.Class.PPrint (PPrint)+import Grisette.Internal.Core.Data.Class.SimpleMergeable (SimpleMergeable)+import Grisette.Internal.Core.Data.Class.Solvable (Solvable)+import Grisette.Internal.Core.Data.Class.SubstSym (SubstSym)+import Grisette.Internal.Core.Data.Class.SymEq (SymEq)+import Grisette.Internal.Core.Data.Class.SymOrd (SymOrd)+import Grisette.Internal.Core.Data.Class.ToCon (ToCon)+import Grisette.Internal.Core.Data.Class.ToSym (ToSym)+import Grisette.Internal.SymPrim.AllSyms (AllSyms)+import Grisette.Internal.SymPrim.Prim.Internal.Term+  ( ConRep (ConType),+    LinkedRep,+  )+import Language.Haskell.TH.Syntax (Lift)+import Type.Reflection (Typeable)++-- | A type that is used as a constraint for all the primitive types (including+-- concrete primitives) in Grisette.+type Prim a =+  ( Show a,+    Binary a,+    Serial a,+    Serialize a,+    NFData a,+    Eq a,+    EvalSym a,+    ExtractSym a,+    Mergeable a,+    PPrint a,+    SubstSym a,+    SymEq a,+    SymOrd a,+    AllSyms a,+    Hashable a,+    Lift a,+    Typeable a+  )++-- | A type that is used as a constraint for all the symbolic primitive types+-- in Grisette.+type SymPrim a =+  ( Prim a,+    ITEOp a,+    GenSymSimple a a+  )++-- | A type that is used as a constraint for all the basic symbolic primitive+-- types in Grisette.+--+-- 'Grisette.SymPrim.SomeSymWordN' is not considered as a basic symbolic+-- primitive type.+type BasicSymPrim a =+  ( SymPrim a,+    SimpleMergeable a,+    GenSymSimple () a,+    Apply a,+    Solvable (ConType a) a,+    ConRep a,+    LinkedRep (ConType a) a,+    ToCon a (ConType a),+    ToSym (ConType a) a+  )

@@ -0,0 +1,61 @@+-- |+-- Module      :   Grisette.Internal.TH.Ctor.Common+-- Copyright   :   (c) Sirui Lu 2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Internal.TH.Ctor.Common+  ( withNameTransformer,+    prefixTransformer,+    decapitalizeTransformer,+  )+where++import Control.Monad (unless)+import Data.Char (isAlphaNum, toLower)+import Data.Foldable (traverse_)+import Grisette.Internal.TH.Util (occName)+import Language.Haskell.TH (Dec, Name, Q)+import Language.Haskell.TH.Datatype+  ( ConstructorInfo (constructorName),+    DatatypeInfo (datatypeCons),+    reifyDatatype,+  )++checkName :: String -> Q ()+checkName name =+  unless (all (\x -> isAlphaNum x || x == '\'' || x == '_') name) $+    fail+      ( "Constructor name contain invalid characters, consider providing a "+          ++ "custom name: "+          ++ show name+      )++-- | Generate smart constructor given a type name, using a name transformer+-- to transform constructor names.+withNameTransformer ::+  -- | A function that generates decs given a list of constructor names and a+  -- type name+  ([String] -> Name -> Q [Dec]) ->+  -- | A function that transforms constructor names+  (String -> String) ->+  -- | The type to generate the wrappers for+  Name ->+  Q [Dec]+withNameTransformer namedGen nameTransformer typName = do+  d <- reifyDatatype typName+  let constructorNames = occName . constructorName <$> datatypeCons d+  let transformedNames = nameTransformer <$> constructorNames+  traverse_ checkName transformedNames+  namedGen transformedNames typName++-- | A name transformer that prefixes a string to the constructor name+prefixTransformer :: String -> String -> String+prefixTransformer = (++)++-- | A name transformer that converts the first character to lowercase+decapitalizeTransformer :: String -> String+decapitalizeTransformer (x : xs) = toLower x : xs+decapitalizeTransformer [] = []

@@ -0,0 +1,180 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE TemplateHaskellQuotes #-}+{-# LANGUAGE Trustworthy #-}++-- |+-- Module      :   Grisette.Internal.TH.Ctor.SmartConstructor+-- Copyright   :   (c) Sirui Lu 2021-2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Internal.TH.Ctor.SmartConstructor+  ( makeSmartCtorWith,+    makePrefixedSmartCtor,+    makeNamedSmartCtor,+    makeSmartCtor,+  )+where++import Control.Monad (join, replicateM, when, zipWithM)+import Data.Bifunctor (Bifunctor (second))+import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)+import Grisette.Internal.Core.Data.Class.TryMerge (TryMerge, mrgSingle)+import Grisette.Internal.TH.Ctor.Common+  ( decapitalizeTransformer,+    prefixTransformer,+    withNameTransformer,+  )+import Grisette.Internal.TH.Util (constructorInfoToType, putHaddock)+import Language.Haskell.TH+  ( Body (NormalB),+    Clause (Clause),+    Dec (FunD, SigD),+    Exp (AppE, ConE, LamE, VarE),+    Name,+    Pat (VarP),+    Pred,+    Q,+    Type (AppT, ArrowT, ForallT, VarT),+    mkName,+    newName,+  )+import Language.Haskell.TH.Datatype+  ( ConstructorInfo+      ( constructorFields,+        constructorName+      ),+    DatatypeInfo (datatypeCons),+    reifyDatatype,+  )+import Language.Haskell.TH.Datatype.TyVarBndr+  ( Specificity (SpecifiedSpec),+    TyVarBndrSpec,+    plainTVFlag,+  )++-- | Generate constructor wrappers that wraps the result in a container with+-- `TryMerge` with provided name transformer.+--+-- > makeSmartCtorWith (\name -> "mrg" ++ name) ''Maybe+--+-- generates+--+-- > mrgNothing :: (Mergeable (Maybe a), Applicative m, TryMerge m) => m (Maybe a)+-- > mrgNothing = mrgSingle Nothing+makeSmartCtorWith :: (String -> String) -> Name -> Q [Dec]+makeSmartCtorWith = withNameTransformer makeNamedSmartCtor++-- | Generate constructor wrappers that wraps the result in a container with+-- `TryMerge`.+--+-- > makePrefixedSmartCtor "mrg" ''Maybe+--+-- generates+--+-- > mrgNothing :: (Mergeable (Maybe a), Applicative m, TryMerge m) => m (Maybe a)+-- > mrgNothing = mrgSingle Nothing+-- > mrgJust :: (Mergeable (Maybe a), Applicative m, TryMerge m) => a -> m (Maybe a)+-- > mrgJust = \x -> mrgSingle (Just x)+makePrefixedSmartCtor ::+  -- | Prefix for generated wrappers+  String ->+  -- | The type to generate the wrappers for+  Name ->+  Q [Dec]+makePrefixedSmartCtor = makeSmartCtorWith . prefixTransformer++-- | Generate constructor wrappers that wraps the result in a container with+-- `TryMerge`.+--+-- > makeSmartCtor ''Maybe+--+-- generates+--+-- > nothing :: (Mergeable (Maybe a), Applicative m, TryMerge m) => m (Maybe a)+-- > nothing = mrgSingle Nothing+-- > just :: (Mergeable (Maybe a), Applicative m, TryMerge m) => a -> m (Maybe a)+-- > just = \x -> mrgSingle (Just x)+makeSmartCtor ::+  -- | The type to generate the wrappers for+  Name ->+  Q [Dec]+makeSmartCtor = makeSmartCtorWith decapitalizeTransformer++-- | Generate constructor wrappers that wraps the result in a container with+-- `TryMerge` with provided names.+--+-- > makeNamedSmartCtor ["mrgTuple2"] ''(,)+--+-- generates+--+-- > mrgTuple2 :: (Mergeable (a, b), Applicative m, TryMerge m) => a -> b -> u (a, b)+-- > mrgTuple2 = \v1 v2 -> mrgSingle (v1, v2)+makeNamedSmartCtor ::+  -- | Names for generated wrappers+  [String] ->+  -- | The type to generate the wrappers for+  Name ->+  Q [Dec]+makeNamedSmartCtor names typName = do+  d <- reifyDatatype typName+  let constructors = datatypeCons d+  when (length names /= length constructors) $+    fail "Number of names does not match the number of constructors"+  ds <- zipWithM (mkSingleWrapper d) names constructors+  return $ join ds++augmentNormalCExpr :: Int -> Exp -> Q Exp+augmentNormalCExpr n f = do+  xs <- replicateM n (newName "x")+  let args = map VarP xs+  mrgSingleFun <- [|mrgSingle|]+  return $+    LamE+      args+      ( AppE mrgSingleFun $+          foldl AppE f (map VarE xs)+      )++augmentFinalType :: Type -> Q (([TyVarBndrSpec], [Pred]), Type)+augmentFinalType (AppT a@(AppT ArrowT _) t) = do+  tl <- augmentFinalType t+  return $ second (AppT a) tl+augmentFinalType t = do+  mName <- newName "m"+  let mTy = VarT mName+  mergeable <- [t|Mergeable|]+  applicative <- [t|Applicative|]+  tryMerge <- [t|TryMerge|]+  return+    ( ( [plainTVFlag mName SpecifiedSpec],+        [AppT mergeable t, AppT applicative mTy, AppT tryMerge mTy]+      ),+      AppT mTy t+    )++augmentConstructorType :: Type -> Q Type+augmentConstructorType (ForallT tybinders ctx ty1) = do+  ((bndrs, preds), augmentedTyp) <- augmentFinalType ty1+  return $ ForallT (tybinders ++ bndrs) (preds ++ ctx) augmentedTyp+augmentConstructorType t = do+  ((bndrs, preds), augmentedTyp) <- augmentFinalType t+  return $ ForallT bndrs preds augmentedTyp++mkSingleWrapper :: DatatypeInfo -> String -> ConstructorInfo -> Q [Dec]+mkSingleWrapper dataType name info = do+  constructorTyp <- constructorInfoToType dataType info+  augmentedTyp <- augmentConstructorType constructorTyp+  let oriName = constructorName info+  let retName = mkName name+  expr <- augmentNormalCExpr (length $ constructorFields info) (ConE oriName)+  putHaddock retName $+    "Smart constructor for v'"+      <> show oriName+      <> "' to construct values wrapped and possibly merged in a container."+  return+    [ SigD retName augmentedTyp,+      FunD retName [Clause [] (NormalB expr) []]+    ]

@@ -0,0 +1,187 @@+{-# LANGUAGE TemplateHaskell #-}++-- |+-- Module      :   Grisette.Internal.TH.Ctor.UnifiedConstructor+-- Copyright   :   (c) Sirui Lu 2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Internal.TH.Ctor.UnifiedConstructor+  ( makeUnifiedCtorWith,+    makePrefixedUnifiedCtor,+    makeNamedUnifiedCtor,+    makeUnifiedCtor,+  )+where++import Control.Monad (join, replicateM, when, zipWithM)+import Grisette.Internal.TH.Ctor.Common+  ( decapitalizeTransformer,+    prefixTransformer,+    withNameTransformer,+  )+import Grisette.Internal.TH.Util (constructorInfoToType, putHaddock)+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag)+import Grisette.Unified.Internal.UnifiedData+  ( GetData,+    UnifiedData,+    wrapData,+  )+import Language.Haskell.TH (pprint)+import Language.Haskell.TH.Datatype+  ( ConstructorInfo (constructorFields, constructorName),+    DatatypeInfo (datatypeCons, datatypeVars),+    reifyDatatype,+    tvKind,+    tvName,+  )+import Language.Haskell.TH.Datatype.TyVarBndr (TyVarBndrSpec, kindedTVSpecified)+import Language.Haskell.TH.Lib (appE, appTypeE, lamE, varE, varP)+import Language.Haskell.TH.Syntax+  ( Body (NormalB),+    Clause (Clause),+    Dec (FunD, SigD),+    Exp (ConE),+    Name,+    Pred,+    Q,+    Type (AppT, ArrowT, ConT, ForallT, VarT),+    mkName,+    newName,+  )++-- | Generate smart constructors to create unified values with provided name+-- transformer.+--+-- For a type @T mode a b c@ with constructors @T1@, @T2@, etc., this function+-- will generate smart constructors with the name transformed, e.g., given the+-- name transformer @(\name -> "mk" ++ name)@, it will generate @mkT1@, @mkT2@,+-- @mkT2@, etc.+--+-- The generated smart constructors will contruct values of type+-- @GetData mode (T mode a b c)@.+makeUnifiedCtorWith :: (String -> String) -> Name -> Q [Dec]+makeUnifiedCtorWith = withNameTransformer makeNamedUnifiedCtor++-- | Generate smart constructors to create unified values.+--+-- For a type @T mode a b c@ with constructors @T1@, @T2@, etc., this function+-- will generate smart constructors with the given prefix, e.g., @mkT1@, @mkT2@,+-- etc.+--+-- The generated smart constructors will contruct values of type+-- @GetData mode (T mode a b c)@.+makePrefixedUnifiedCtor ::+  -- | Prefix for generated wrappers+  String ->+  -- | The type to generate the wrappers for+  Name ->+  Q [Dec]+makePrefixedUnifiedCtor = makeUnifiedCtorWith . prefixTransformer++-- | Generate smart constructors to create unified values.+--+-- For a type @T mode a b c@ with constructors @T1@, @T2@, etc., this function+-- will generate smart constructors with the names decapitalized, e.g.,+-- @t1@, @t2@, etc.+--+-- The generated smart constructors will contruct values of type+-- @GetData mode (T mode a b c)@.+makeUnifiedCtor ::+  -- | The type to generate the wrappers for+  Name ->+  Q [Dec]+makeUnifiedCtor = makeUnifiedCtorWith decapitalizeTransformer++-- | Generate smart constructors to create unified values.+--+-- For a type @T mode a b c@ with constructors @T1@, @T2@, etc., this function+-- will generate smart constructors with the given names.+--+-- The generated smart constructors will contruct values of type+-- @GetData mode (T mode a b c)@.+makeNamedUnifiedCtor ::+  -- | Names for generated wrappers+  [String] ->+  -- | The type to generate the wrappers for+  Name ->+  Q [Dec]+makeNamedUnifiedCtor names typName = do+  d <- reifyDatatype typName+  let constructors = datatypeCons d+  when (length names /= length constructors) $+    fail "Number of names does not match the number of constructors"+  let modeVars = filter ((== ConT ''EvalModeTag) . tvKind) (datatypeVars d)+  -- when (length modeVars /= 1) $+  --  fail "Expected exactly one EvalModeTag variable in the datatype."+  case modeVars of+    [mode] -> do+      ds <-+        zipWithM+          (mkSingleWrapper d Nothing $ VarT $ tvName mode)+          names+          constructors+      return $ join ds+    [] -> do+      n <- newName "mode"+      let newBndr = kindedTVSpecified n (ConT ''EvalModeTag)+      ds <-+        zipWithM+          (mkSingleWrapper d (Just newBndr) (VarT n))+          names+          constructors+      return $ join ds+    _ -> fail "Expected one or zero EvalModeTag variable in the datatype."++augmentFinalType :: Type -> Type -> Q ([Pred], Type)+augmentFinalType mode (AppT a@(AppT ArrowT _) t) = do+  (pred, ret) <- augmentFinalType mode t+  return (pred, AppT a ret)+augmentFinalType mode t = do+  r <- [t|GetData $(return mode) $(return t)|]+  predu <- [t|UnifiedData $(return mode) $(return t)|]+  return ([predu], r)++augmentConstructorType :: Maybe TyVarBndrSpec -> Type -> Type -> Q Type+augmentConstructorType modeBndr mode (ForallT tybinders ctx ty1) = do+  (preds, augmentedTyp) <- augmentFinalType mode ty1+  case modeBndr of+    Just bndr -> return $ ForallT (bndr : tybinders) (preds ++ ctx) augmentedTyp+    Nothing -> return $ ForallT tybinders (preds ++ ctx) augmentedTyp+augmentConstructorType modeBndr mode ty = do+  (preds, augmentedTyp) <- augmentFinalType mode ty+  case modeBndr of+    Just bndr -> return $ ForallT [bndr] preds augmentedTyp+    Nothing ->+      fail $+        "augmentConstructorType: unsupported constructor type: " ++ pprint ty++augmentExpr :: Type -> Int -> Exp -> Q Exp+augmentExpr mode n f = do+  xs <- replicateM n (newName "x")+  let args = map varP xs+  lamE+    args+    ( ( appE+          (appTypeE [|wrapData|] (return mode))+          (foldl appE (return f) (map varE xs))+      )+    )++mkSingleWrapper :: DatatypeInfo -> Maybe TyVarBndrSpec -> Type -> String -> ConstructorInfo -> Q [Dec]+mkSingleWrapper dataType modeBndr mode name info = do+  constructorTyp <- constructorInfoToType dataType info+  augmentedTyp <- augmentConstructorType modeBndr mode constructorTyp+  let oriName = constructorName info+  let retName = mkName name+  expr <- augmentExpr mode (length $ constructorFields info) (ConE oriName)+  putHaddock retName $+    "Smart constructor for v'"+      <> show oriName+      <> "' to construct unified value."+  return+    [ SigD retName augmentedTyp,+      FunD retName [Clause [] (NormalB expr) []]+    ]

@@ -0,0 +1,99 @@+{-# LANGUAGE RecordWildCards #-}++-- |+-- Module      :   Grisette.Internal.TH.GADT.Common+-- Copyright   :   (c) Sirui Lu 2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Internal.TH.GADT.Common+  ( CheckArgsResult (..),+    checkArgs,+  )+where++import Control.Monad (when)+import qualified Data.Map as M+import qualified Data.Set as S+import Grisette.Internal.TH.Util (occName)+import Language.Haskell.TH+  ( Name,+    Q,+    Type (VarT),+    newName,+  )+import Language.Haskell.TH.Datatype+  ( ConstructorInfo (constructorFields),+    DatatypeInfo (datatypeCons, datatypeVars),+    TypeSubstitution (applySubstitution, freeVariables),+    reifyDatatype,+    tvName,+  )+import Language.Haskell.TH.Datatype.TyVarBndr (TyVarBndr_, mapTVName)++-- | Result of 'checkArgs' for a GADT.+data CheckArgsResult = CheckArgsResult+  { constructors :: [ConstructorInfo],+    keptNewNames :: [Name],+    keptNewVars :: [TyVarBndr_ ()],+    argNewNames :: [Name],+    argNewVars :: [TyVarBndr_ ()],+    isVarUsedInFields :: Name -> Bool+  }++-- | Check if the number of type parameters is valid for a GADT, and return+-- new names for the type variables, split into kept and arg parts.+checkArgs ::+  String ->+  Int ->+  Name ->+  Int ->+  Q CheckArgsResult+checkArgs clsName maxArgNum typName n = do+  when (n < 0) $+    fail $+      unlines+        [ "Cannot derive "+            ++ clsName+            ++ " instance with negative type parameters",+          "Requested: " ++ show n,+          "Hint: Use a non-negative number of type parameters"+        ]+  when (n > maxArgNum) $+    fail $+      "Requesting "+        <> clsName+        <> " instance with more than "+        <> show maxArgNum+        <> " type parameters"+  d <- reifyDatatype typName+  let dvars = datatypeVars d+  when (length dvars < n) $+    fail $+      "Requesting Mergeable"+        <> show n+        <> " instance, while the type "+        <> show typName+        <> " has only "+        <> show (length dvars)+        <> " type variables."+  let keptVars = take (length dvars - n) dvars+  keptNewNames <- traverse (newName . occName . tvName) keptVars+  let keptNewVars =+        zipWith (mapTVName . const) keptNewNames keptVars+  let argVars = drop (length dvars - n) dvars+  argNewNames <- traverse (newName . occName . tvName) argVars+  let argNewVars =+        zipWith (mapTVName . const) argNewNames argVars+  let substMap =+        M.fromList $+          zip+            (tvName <$> dvars)+            (VarT <$> keptNewNames ++ argNewNames)+  let constructors = applySubstitution substMap $ datatypeCons d+  let allFields = concatMap constructorFields constructors+  let allFieldsFreeVars = S.fromList $ freeVariables allFields+  let isVarUsedInFields var = S.member var allFieldsFreeVars+  return $ CheckArgsResult {..}

@@ -0,0 +1,77 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TupleSections #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}++{-# HLINT ignore "Unused LANGUAGE pragma" #-}++-- |+-- Module      :   Grisette.Internal.TH.GADT.DeriveEvalSym+-- Copyright   :   (c) Sirui Lu 2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Internal.TH.GADT.DeriveEvalSym+  ( deriveGADTEvalSym,+    deriveGADTEvalSym1,+    deriveGADTEvalSym2,+  )+where++import Grisette.Internal.Core.Data.Class.EvalSym+  ( EvalSym (evalSym),+    EvalSym1 (liftEvalSym),+    EvalSym2 (liftEvalSym2),+  )+import Grisette.Internal.TH.GADT.UnaryOpCommon+  ( UnaryOpClassConfig+      ( UnaryOpClassConfig,+        unaryOpFieldConfig,+        unaryOpFunNames,+        unaryOpInstanceNames+      ),+    UnaryOpFieldConfig+      ( UnaryOpFieldConfig,+        extraPatNames,+        fieldCombineFun+      ),+    genUnaryOpClass,+  )+import Language.Haskell.TH+  ( Dec,+    Exp (AppE),+    Name,+    Q,+  )++genEvalSym' :: Int -> Name -> Q [Dec]+genEvalSym' n typName = do+  genUnaryOpClass+    UnaryOpClassConfig+      { unaryOpFieldConfig =+          UnaryOpFieldConfig+            { extraPatNames = ["fillDefault", "model"],+              fieldCombineFun = \con exp -> return $ foldl AppE con exp+            },+        unaryOpInstanceNames =+          [''EvalSym, ''EvalSym1, ''EvalSym2],+        unaryOpFunNames =+          ['evalSym, 'liftEvalSym, 'liftEvalSym2]+      }+    n+    typName++-- | Derive 'EvalSym' instance for a GADT.+deriveGADTEvalSym :: Name -> Q [Dec]+deriveGADTEvalSym = genEvalSym' 0++-- | Derive 'EvalSym1' instance for a GADT.+deriveGADTEvalSym1 = genEvalSym' 1++-- | Derive 'EvalSym2' instance for a GADT.+deriveGADTEvalSym2 :: Name -> Q [Dec]+deriveGADTEvalSym2 = genEvalSym' 2

@@ -0,0 +1,75 @@+{-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}++{-# HLINT ignore "Unused LANGUAGE pragma" #-}++-- |+-- Module      :   Grisette.Internal.TH.GADT.DeriveExtractSym+-- Copyright   :   (c) Sirui Lu 2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Internal.TH.GADT.DeriveExtractSym+  ( deriveGADTExtractSym,+    deriveGADTExtractSym1,+    deriveGADTExtractSym2,+  )+where++import Grisette.Internal.Core.Data.Class.ExtractSym+  ( ExtractSym (extractSymMaybe),+    ExtractSym1 (liftExtractSymMaybe),+    ExtractSym2 (liftExtractSymMaybe2),+  )+import Grisette.Internal.TH.GADT.UnaryOpCommon+  ( UnaryOpClassConfig+      ( UnaryOpClassConfig,+        unaryOpFieldConfig,+        unaryOpFunNames,+        unaryOpInstanceNames+      ),+    UnaryOpFieldConfig+      ( UnaryOpFieldConfig,+        extraPatNames,+        fieldCombineFun+      ),+    genUnaryOpClass,+  )+import Language.Haskell.TH+  ( Dec,+    Exp (AppE, ListE, VarE),+    Name,+    Q,+  )++genExtractSym' :: Int -> Name -> Q [Dec]+genExtractSym' n typName = do+  genUnaryOpClass+    UnaryOpClassConfig+      { unaryOpFieldConfig =+          UnaryOpFieldConfig+            { extraPatNames = [],+              fieldCombineFun = \_ exp ->+                return $ AppE (VarE 'mconcat) $ ListE exp+            },+        unaryOpInstanceNames =+          [''ExtractSym, ''ExtractSym1, ''ExtractSym2],+        unaryOpFunNames =+          ['extractSymMaybe, 'liftExtractSymMaybe, 'liftExtractSymMaybe2]+      }+    n+    typName++-- | Derive 'ExtractSym' instance for a GADT.+deriveGADTExtractSym :: Name -> Q [Dec]+deriveGADTExtractSym = genExtractSym' 0++-- | Derive 'ExtractSym1' instance for a GADT.+deriveGADTExtractSym1 :: Name -> Q [Dec]+deriveGADTExtractSym1 = genExtractSym' 1++-- | Derive 'ExtractSym2' instance for a GADT.+deriveGADTExtractSym2 :: Name -> Q [Dec]+deriveGADTExtractSym2 = genExtractSym' 2

@@ -0,0 +1,136 @@+{-# HLINT ignore "Unused LANGUAGE pragma" #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}++-- |+-- Module      :   Grisette.Internal.TH.GADT.DeriveGADT+-- Copyright   :   (c) Sirui Lu 2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Internal.TH.GADT.DeriveGADT+  ( deriveGADT,+    deriveGADTAll,+    deriveGADTAllExcept,+  )+where++import qualified Data.Map as M+import qualified Data.Set as S+import Grisette.Internal.Core.Data.Class.EvalSym+  ( EvalSym,+    EvalSym1,+    EvalSym2,+  )+import Grisette.Internal.Core.Data.Class.ExtractSym+  ( ExtractSym,+    ExtractSym1,+    ExtractSym2,+  )+import Grisette.Internal.Core.Data.Class.Mergeable+  ( Mergeable,+    Mergeable1,+    Mergeable2,+    Mergeable3,+  )+import Grisette.Internal.TH.GADT.DeriveEvalSym+  ( deriveGADTEvalSym,+    deriveGADTEvalSym1,+    deriveGADTEvalSym2,+  )+import Grisette.Internal.TH.GADT.DeriveExtractSym+  ( deriveGADTExtractSym,+    deriveGADTExtractSym1,+    deriveGADTExtractSym2,+  )+import Grisette.Internal.TH.GADT.DeriveMergeable (genMergeable, genMergeable', genMergeableAndGetMergingInfoResult)+import Language.Haskell.TH (Dec, Name, Q)++deriveProcedureMap :: M.Map Name (Name -> Q [Dec])+deriveProcedureMap =+  M.fromList+    [ -- (''Mergeable, deriveGADTMergeable),+      -- (''Mergeable1, deriveGADTMergeable1),+      -- (''Mergeable2, deriveGADTMergeable2),+      -- (''Mergeable3, deriveGADTMergeable3),+      (''EvalSym, deriveGADTEvalSym),+      (''EvalSym1, deriveGADTEvalSym1),+      (''EvalSym2, deriveGADTEvalSym2),+      (''ExtractSym, deriveGADTExtractSym),+      (''ExtractSym1, deriveGADTExtractSym1),+      (''ExtractSym2, deriveGADTExtractSym2)+    ]++deriveSingleGADT :: Name -> Name -> Q [Dec]+deriveSingleGADT typName className = do+  case M.lookup className deriveProcedureMap of+    Just procedure -> procedure typName+    Nothing ->+      fail $ "No derivation available for class " ++ show className++-- | Derive the specified classes for a GADT with the given name.+--+-- Support the following classes.+--+-- * 'Mergeable'+-- * 'Mergeable1'+-- * 'Mergeable2'+-- * 'Mergeable3'+-- * 'EvalSym'+-- * 'EvalSym1'+-- * 'EvalSym2'+-- * 'ExtractSym'+-- * 'ExtractSym1'+-- * 'ExtractSym2'+deriveGADT :: Name -> [Name] -> Q [Dec]+deriveGADT typName classNames = do+  let allClassNames = S.toList $ S.fromList classNames+  let (ns, ms) = splitMergeable allClassNames+  decs <- mapM (deriveSingleGADT typName) ns+  decMergeables <- deriveMergeables ms+  return $ concat decs ++ decMergeables+  where+    deriveMergeables :: [Int] -> Q [Dec]+    deriveMergeables [] = return []+    deriveMergeables [n] = genMergeable typName n+    deriveMergeables (n : ns) = do+      (info, dn) <- genMergeableAndGetMergingInfoResult typName n+      dns <- traverse (genMergeable' info typName) ns+      return $ dn ++ concatMap snd dns+    splitMergeable :: [Name] -> ([Name], [Int])+    splitMergeable [] = ([], [])+    splitMergeable (x : xs) =+      let (ns, is) = splitMergeable xs+       in if+            | x == ''Mergeable -> (ns, 0 : is)+            | x == ''Mergeable1 -> (ns, 1 : is)+            | x == ''Mergeable2 -> (ns, 2 : is)+            | x == ''Mergeable3 -> (ns, 3 : is)+            | otherwise -> (x : ns, is)++-- | Derive all (non-functor) classes related to Grisette for a GADT with the+-- given name.+--+-- Classes that are derived by this procedure are:+--+-- * 'Mergeable'+-- * 'EvalSym'+-- * 'ExtractSym'+--+-- Note that it is okay to derive for non-GADT types using this procedure, and+-- it will be slightly more efficient.+deriveGADTAll :: Name -> Q [Dec]+deriveGADTAll typName =+  deriveGADT typName [''Mergeable, ''EvalSym, ''ExtractSym]++-- | Derive all (non-functor) classes related to Grisette for a GADT with the+-- given name except the specified classes.+deriveGADTAllExcept :: Name -> [Name] -> Q [Dec]+deriveGADTAllExcept typName classNames = do+  deriveGADT typName $+    S.toList $+      S.fromList [''Mergeable, ''EvalSym, ''ExtractSym]+        S.\\ S.fromList classNames

@@ -0,0 +1,614 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeApplications #-}++-- |+-- Module      :   Grisette.Internal.TH.GADT.DeriveMergeable+-- Copyright   :   (c) Sirui Lu 2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Internal.TH.GADT.DeriveMergeable+  ( deriveGADTMergeable,+    deriveGADTMergeable1,+    deriveGADTMergeable2,+    deriveGADTMergeable3,+    genMergeableAndGetMergingInfoResult,+    genMergeable,+    genMergeable',+  )+where++import Control.Monad (foldM, replicateM, zipWithM)+import qualified Data.Map as M+import Data.Maybe (catMaybes, isJust, mapMaybe)+import Data.Proxy (Proxy (Proxy))+import qualified Data.Set as S+import Grisette.Internal.Core.Data.Class.Mergeable+  ( Mergeable (rootStrategy),+    Mergeable1 (liftRootStrategy),+    Mergeable2 (liftRootStrategy2),+    Mergeable3 (liftRootStrategy3),+    MergingStrategy (SimpleStrategy, SortedStrategy),+    product2Strategy,+    wrapStrategy,+  )+import Grisette.Internal.TH.GADT.Common+  ( CheckArgsResult+      ( CheckArgsResult,+        argNewNames,+        argNewVars,+        constructors,+        isVarUsedInFields,+        keptNewNames,+        keptNewVars+      ),+    checkArgs,+  )+import Grisette.Internal.TH.Util (occName)+import Language.Haskell.TH+  ( Bang (Bang),+    Body (NormalB),+    Clause (Clause),+    Con (ForallC, GadtC),+    Dec (DataD, FunD, InstanceD, SigD),+    Exp (AppE, ConE, VarE),+    Name,+    Pat (SigP, VarP, WildP),+    Pred,+    Q,+    SourceStrictness (NoSourceStrictness),+    SourceUnpackedness (NoSourceUnpackedness),+    Type (AppT, ArrowT, ConT, ForallT, StarT, VarT),+    appE,+    conE,+    conT,+    lamE,+    lookupTypeName,+    mkName,+    newName,+    normalB,+    tupP,+    varE,+    varP,+    varT,+    wildP,+  )+import Language.Haskell.TH.Datatype+  ( ConstructorInfo+      ( constructorContext,+        constructorFields,+        constructorName,+        constructorVars+      ),+    DatatypeInfo (datatypeCons, datatypeName, datatypeVars),+    TypeSubstitution (applySubstitution, freeVariables),+    reifyDatatype,+    tvName,+  )+import Language.Haskell.TH.Datatype.TyVarBndr+  ( TyVarBndrUnit,+    TyVarBndr_,+    mapTVFlag,+    plainTVFlag,+    specifiedSpec,+    tvKind,+  )+import Language.Haskell.TH.Lib (clause, conP, litE, stringL)+import Type.Reflection (SomeTypeRep (SomeTypeRep), TypeRep, typeRep)+import Unsafe.Coerce (unsafeCoerce)++genMergingInfoCon ::+  [TyVarBndrUnit] ->+  Name ->+  Bool ->+  ConstructorInfo ->+  Q (Con, Name, S.Set Int, [Clause], [Clause], [Clause])+genMergingInfoCon dataTypeVars tyName isLast con = do+  let conName = occName $ constructorName con+  let newConName = mkName $ conName <> "MergingInfo"+  if null (constructorFields con) && null dataTypeVars+    then do+      eqClause <-+        clause+          [conP newConName [], conP newConName []]+          (normalB $ conE 'True)+          []+      cmpClause0 <-+        clause+          [conP newConName [], conP newConName []]+          (normalB $ conE 'EQ)+          []+      cmpClause1 <-+        clause+          [conP newConName [], wildP]+          (normalB $ conE 'LT)+          []+      cmpClause2 <-+        clause+          [wildP, conP newConName []]+          (normalB $ conE 'GT)+          []+      let cmpClauses =+            if isLast+              then [cmpClause0]+              else [cmpClause0, cmpClause1, cmpClause2]+      let nameLit = litE $ stringL conName+      let showExp = [|$nameLit <> " " <> show (Proxy @($(conT tyName)))|]+      showClause <-+        clause+          [conP newConName []]+          (normalB showExp)+          []+      return+        ( GadtC [newConName] [] (ConT tyName),+          newConName,+          S.fromList [],+          [eqClause],+          cmpClauses,+          [showClause]+        )+    else do+      let oriVars = dataTypeVars ++ constructorVars con+      newNames <- traverse (newName . occName . tvName) oriVars+      let newVars = fmap VarT newNames+      let substMap = M.fromList $ zip (tvName <$> oriVars) newVars+      let fields =+            zip [0 ..] $+              applySubstitution substMap $+                constructorFields con+      let tyFields =+            AppT (ConT ''TypeRep)+              <$> applySubstitution+                substMap+                ((VarT . tvName) <$> constructorVars con)+      let strategyFields = fmap (AppT (ConT ''MergingStrategy) . snd) fields+      tyFieldNamesL <- traverse (const $ newName "p") tyFields+      tyFieldNamesR <- traverse (const $ newName "p") tyFields+      let tyFieldPatsL = fmap varP tyFieldNamesL+      let tyFieldPatsR = fmap varP tyFieldNamesR+      let tyFieldVarsL = fmap varE tyFieldNamesL+      let tyFieldVarsR = fmap varE tyFieldNamesR+      let strategyFieldPats = replicate (length strategyFields) wildP+      let patsL = tyFieldPatsL ++ strategyFieldPats+      let patsR = tyFieldPatsR ++ strategyFieldPats+      let allWildcards = fmap (const wildP) $ tyFieldPatsL ++ strategyFieldPats+      let eqCont l r cont =+            [|+              SomeTypeRep $l == SomeTypeRep $r+                && $cont+              |]+      let eqExp =+            foldl (\cont (l, r) -> eqCont l r cont) (conE 'True) $+              zip tyFieldVarsL tyFieldVarsR+      eqClause <-+        clause+          [conP newConName patsL, conP newConName patsR]+          (normalB eqExp)+          []+      let cmpCont l r cont =+            [|+              case SomeTypeRep $l `compare` SomeTypeRep $r of+                EQ -> $cont+                x -> x+              |]+      let cmpExp =+            foldl (\cont (l, r) -> cmpCont l r cont) (conE 'EQ) $+              zip tyFieldVarsL tyFieldVarsR+      cmpClause0 <-+        clause+          [conP newConName patsL, conP newConName patsR]+          (normalB cmpExp)+          []+      cmpClause1 <-+        clause+          [conP newConName allWildcards, wildP]+          (normalB $ conE 'LT)+          []+      cmpClause2 <-+        clause+          [wildP, conP newConName allWildcards]+          (normalB $ conE 'GT)+          []+      let cmpClauses =+            if isLast+              then [cmpClause0]+              else [cmpClause0, cmpClause1, cmpClause2]+      let showCont t cont =+            [|$cont <> " " <> show $t|]+      let showExp = foldl (flip showCont) (litE $ stringL conName) tyFieldVarsL+      showClause <-+        clause+          [conP newConName patsL]+          (normalB showExp)+          []+      let ctx = applySubstitution substMap $ constructorContext con+      let ctxAndGadtUsedVars =+            S.fromList (freeVariables ctx)+              <> S.fromList (freeVariables tyFields)+              <> S.fromList (freeVariables strategyFields)+      let isCtxAndGadtUsedVar nm = S.member nm ctxAndGadtUsedVars+      return+        ( ForallC+            ( (`plainTVFlag` specifiedSpec)+                <$> filter isCtxAndGadtUsedVar newNames+            )+            ctx+            $ GadtC+              [newConName]+              ( (Bang NoSourceUnpackedness NoSourceStrictness,)+                  <$> tyFields ++ strategyFields+              )+              (ConT tyName),+          newConName,+          S.fromList [0 .. length tyFields - 1],+          -- S.fromList $ fst <$> dedupedFields,+          [eqClause],+          cmpClauses,+          [showClause]+        )++data MergingInfoResult = MergingInfoResult+  { _infoName :: Name,+    _conInfoNames :: [Name],+    _pos :: [S.Set Int]+  }++genMergingInfo :: Name -> Q (MergingInfoResult, [Dec])+genMergingInfo typName = do+  d <- reifyDatatype typName+  let originalName = occName $ datatypeName d+  let newName = originalName <> "MergingInfo"+  found <- lookupTypeName newName+  let constructors = datatypeCons d+  let name = mkName newName+  r <-+    if null constructors+      then return []+      else do+        cons0 <-+          traverse (genMergingInfoCon (datatypeVars d) name False) $+            init constructors+        consLast <-+          genMergingInfoCon (datatypeVars d) name True $+            last constructors+        return $ cons0 ++ [consLast]+  let cons = fmap (\(a, _, _, _, _, _) -> a) r+  let eqClauses =+        concatMap (\(_, _, _, a, _, _) -> a) r+          ++ [ Clause [WildP, WildP] (NormalB $ ConE 'False) []+               | length constructors > 1+             ]+  let cmpClauses = concatMap (\(_, _, _, _, a, _) -> a) r+  let showClauses = concatMap (\(_, _, _, _, _, a) -> a) r+  return+    ( MergingInfoResult+        name+        (fmap (\(_, a, _, _, _, _) -> a) r)+        (fmap (\(_, _, a, _, _, _) -> a) r),+      if isJust found+        then []+        else+          [ DataD [] name [] Nothing cons [],+            InstanceD+              Nothing+              []+              (ConT ''Eq `AppT` ConT name)+              [FunD '(==) eqClauses],+            InstanceD+              Nothing+              []+              (ConT ''Ord `AppT` ConT name)+              [FunD 'compare cmpClauses],+            InstanceD+              Nothing+              []+              (ConT ''Show `AppT` ConT name)+              [FunD 'show showClauses]+          ]+    )++-- | Generate 'Mergeable' instance and merging information for a GADT.+genMergeableAndGetMergingInfoResult ::+  Name -> Int -> Q (MergingInfoResult, [Dec])+genMergeableAndGetMergingInfoResult typName n = do+  (infoResult, infoDec) <- genMergingInfo typName+  (_, decs) <- genMergeable' infoResult typName n+  return (infoResult, infoDec ++ decs)++-- | Generate 'Mergeable' instance for a GADT.+genMergeable :: Name -> Int -> Q [Dec]+genMergeable typName n = do+  (infoResult, infoDec) <- genMergingInfo typName+  (_, decs) <- genMergeable' infoResult typName n+  return $ infoDec ++ decs++genMergeFunClause' :: Name -> ConstructorInfo -> Q Clause+genMergeFunClause' conInfoName con = do+  let numExistential = length $ constructorVars con+  let numFields = length $ constructorFields con+  let argWildCards = replicate numExistential wildP+  case numFields of+    0 -> do+      let pat = conP conInfoName []+      clause+        (argWildCards ++ [pat])+        (normalB [|SimpleStrategy $ \_ t _ -> t|])+        []+    1 -> do+      pname <- newName "s"+      upname <- newName "a"+      let unwrapPat = conP (constructorName con) [varP upname]+      let unwrapFun = lamE [unwrapPat] $ appE (varE 'unsafeCoerce) (varE upname)+      clause+        [conP conInfoName $ argWildCards ++ [varP pname]]+        ( normalB+            [|+              wrapStrategy+                $(varE pname)+                (unsafeCoerce . $(conE $ constructorName con))+                $unwrapFun+              |]+        )+        []+    _ -> do+      -- fail $ show (argWildCards, conInfoName)+      pnames <- replicateM numFields $ newName "s"+      upnames <- replicateM numFields $ newName "a"+      let wrapPat1 [] = error "Should not happen"+          wrapPat1 [x] = varP x+          wrapPat1 (x : xs) = tupP [varP x, wrapPat1 xs]+      let wrapped = foldl AppE (ConE $ constructorName con) $ fmap VarE upnames+      let wrapFun =+            lamE+              [varP $ head upnames, wrapPat1 $ tail upnames]+              [|unsafeCoerce ($(return wrapped))|]+      let unwrapPat = conP (constructorName con) $ fmap varP upnames+      let unwrapExp1 [] = error "Should not happen"+          unwrapExp1 [_] = error "Should not happen"+          unwrapExp1 [x, y] =+            [|(unsafeCoerce $(varE x), unsafeCoerce $(varE y))|]+          unwrapExp1 (x : xs) = [|(unsafeCoerce $(varE x), $(unwrapExp1 xs))|]+      let unwrapFun = lamE [unwrapPat] (unwrapExp1 upnames)+      let strategy1 [] = error "Should not happen"+          strategy1 [x] = varE x+          strategy1 (x : xs) =+            [|+              product2Strategy+                ((,))+                (\(x, y) -> (x, y))+                $(varE x)+                $(strategy1 xs)+              |]+      clause+        ([conP conInfoName $ argWildCards ++ fmap varP pnames])+        ( normalB+            [|+              product2Strategy+                $wrapFun+                $unwrapFun+                $(varE $ head pnames)+                $(strategy1 $ tail pnames)+              |]+        )+        []++genMergingInfoFunClause' ::+  [Name] -> Name -> S.Set Int -> ConstructorInfo -> Q Clause+genMergingInfoFunClause' argTypes conInfoName pos oldCon = do+  let conName = constructorName oldCon+  let oldConVars = constructorVars oldCon+  newNames <- traverse (newName . occName . tvName) oldConVars+  let substMap = M.fromList $ zip (tvName <$> oldConVars) (VarT <$> newNames)+  let con = applySubstitution substMap oldCon+  let conVars = constructorVars con+  let fields = constructorFields con+  let capture n =+        if S.member n pos+          then do+            return (SigP WildP $ fields !! n)+          else return (WildP)+  capturedVarTyReps <-+    traverse (\bndr -> [|typeRep @($(varT $ tvName bndr))|]) conVars+  varPat <- conP conName $ capture <$> [0 .. length (constructorFields con) - 1]+  let infoExpWithTypeReps = foldl AppE (ConE conInfoName) capturedVarTyReps++  let fields = constructorFields con+  let usedArgs = S.fromList $ freeVariables fields++  strategyNames <-+    traverse+      ( \nm ->+          if S.member nm usedArgs+            then do+              pname <- newName "p"+              return (nm, Just pname)+            else return (nm, Nothing)+      )+      argTypes+  let argToStrategyPat =+        mapMaybe (\(nm, mpat) -> fmap (nm,) mpat) strategyNames+  let strategyPats = fmap (maybe WildP VarP . snd) strategyNames++  let argTypeSet = S.fromList argTypes+  let containsArg :: Type -> Bool+      containsArg ty =+        S.intersection argTypeSet (S.fromList (freeVariables [ty])) /= S.empty+  let typeHasNoArg = not . containsArg++  let fieldStrategyExp ty =+        if not (containsArg ty)+          then [|rootStrategy :: MergingStrategy $(return ty)|]+          else case ty of+            _+              | typeHasNoArg ty ->+                  [|rootStrategy :: MergingStrategy $(return ty)|]+            AppT a b+              | typeHasNoArg a ->+                  [|+                    liftRootStrategy+                      $(fieldStrategyExp b) ::+                      MergingStrategy $(return ty)+                    |]+            AppT (AppT a b) c+              | typeHasNoArg a ->+                  [|+                    liftRootStrategy2+                      $(fieldStrategyExp b)+                      $(fieldStrategyExp c) ::+                      MergingStrategy $(return ty)+                    |]+            AppT (AppT (AppT a b) c) d+              | typeHasNoArg a ->+                  [|+                    liftRootStrategy3+                      $(fieldStrategyExp b)+                      $(fieldStrategyExp c)+                      $(fieldStrategyExp d) ::+                      MergingStrategy $(return ty)+                    |]+            VarT nm -> do+              case lookup nm argToStrategyPat of+                Just pname -> varE pname+                _ -> fail "BUG: fieldStrategyExp"+            _ -> fail $ "fieldStrategyExp: unsupported type: " <> show ty+  fieldStrategyExps <- traverse fieldStrategyExp fields+  let infoExp = foldl AppE infoExpWithTypeReps fieldStrategyExps+  -- fail $ show infoExp+  return $ Clause (strategyPats ++ [varPat]) (NormalB infoExp) []++-- | Generate 'Mergeable' instance for a GADT, using a given merging info+-- result.+genMergeable' :: MergingInfoResult -> Name -> Int -> Q (Name, [Dec])+genMergeable' (MergingInfoResult infoName conInfoNames pos) typName n = do+  CheckArgsResult {..} <- checkArgs "Mergeable" 3 typName n++  d <- reifyDatatype typName+  let ctxForVar :: TyVarBndr_ flag -> Q (Maybe Pred)+      ctxForVar var = case tvKind var of+        StarT -> Just <$> [t|Mergeable $(varT $ tvName var)|]+        AppT (AppT ArrowT StarT) StarT ->+          Just <$> [t|Mergeable1 $(varT $ tvName var)|]+        AppT (AppT (AppT ArrowT StarT) StarT) StarT ->+          Just <$> [t|Mergeable2 $(varT $ tvName var)|]+        AppT (AppT (AppT (AppT ArrowT StarT) StarT) StarT) StarT ->+          Just <$> [t|Mergeable3 $(varT $ tvName var)|]+        AppT (AppT (AppT (AppT ArrowT StarT) StarT) StarT) _ ->+          fail $ "Unsupported kind: " <> show (tvKind var)+        _ -> return Nothing+  mergeableContexts <-+    traverse ctxForVar $ filter (isVarUsedInFields . tvName) keptNewVars++  let targetType =+        foldl+          (\ty nm -> AppT ty (VarT nm))+          (ConT typName)+          (keptNewNames ++ argNewNames)+  let infoType = ConT infoName+  let mergingInfoFunFinalType = AppT (AppT ArrowT targetType) infoType++  let mergingInfoFunTypeWithoutCtx =+        foldr+          ((AppT . AppT ArrowT) . AppT (ConT ''MergingStrategy) . VarT)+          mergingInfoFunFinalType+          argNewNames++  let mergingInfoFunType =+        ForallT+          (mapTVFlag (const specifiedSpec) <$> keptNewVars ++ argNewVars)+          (catMaybes mergeableContexts)+          mergingInfoFunTypeWithoutCtx+  let mergingInfoFunName =+        mkName $+          "mergingInfo"+            <> (if n /= 0 then show n else "")+            <> occName (datatypeName d)+  let mergingInfoFunSigD = SigD mergingInfoFunName mergingInfoFunType+  clauses <-+    traverse+      ( \(conInfoName, pos, con) ->+          genMergingInfoFunClause' (tvName <$> argNewVars) conInfoName pos con+      )+      $ zip3 conInfoNames pos constructors+  let mergingInfoFunDec = FunD mergingInfoFunName clauses++  let mergeFunType =+        AppT (AppT ArrowT infoType) (AppT (ConT ''MergingStrategy) targetType)+  let mergeFunName =+        mkName $+          "merge"+            <> (if n /= 0 then show n else "")+            <> occName (datatypeName d)+  let mergeFunSigD = SigD mergeFunName mergeFunType+  mergeFunClauses <- zipWithM genMergeFunClause' conInfoNames constructors+  let mergeFunDec = FunD mergeFunName mergeFunClauses++  let instanceHead = case n of+        0 -> ConT ''Mergeable+        1 -> ConT ''Mergeable1+        2 -> ConT ''Mergeable2+        3 -> ConT ''Mergeable3+        _ -> error "Unsupported n"++  let instanceType =+        AppT+          instanceHead+          (foldl AppT (ConT typName) $ fmap VarT keptNewNames)++  let mergeInstanceFunName = case n of+        0 -> 'rootStrategy+        1 -> 'liftRootStrategy+        2 -> 'liftRootStrategy2+        3 -> 'liftRootStrategy3+        _ -> error "Unsupported n"+  mergeInstanceFunPatNames <- replicateM n $ newName "rootStrategy"+  let mergeInstanceFunPats = VarP <$> mergeInstanceFunPatNames++  mergeInstanceFunBody <-+    [|+      SortedStrategy+        $( foldM+             (\exp name -> appE (return exp) $ varE name)+             (VarE mergingInfoFunName)+             mergeInstanceFunPatNames+         )+        $(varE mergeFunName)+      |]++  let mergeInstanceFunClause =+        Clause mergeInstanceFunPats (NormalB mergeInstanceFunBody) []++  return+    ( mergingInfoFunName,+      [ mergingInfoFunSigD,+        mergingInfoFunDec,+        mergeFunSigD,+        mergeFunDec,+        InstanceD+          Nothing+          (catMaybes mergeableContexts)+          instanceType+          [FunD mergeInstanceFunName [mergeInstanceFunClause]]+      ]+    )++-- | Derive 'Mergeable' instance for GADT.+deriveGADTMergeable :: Name -> Q [Dec]+deriveGADTMergeable nm = genMergeable nm 0++-- | Derive 'Mergeable1' instance for GADT.+deriveGADTMergeable1 :: Name -> Q [Dec]+deriveGADTMergeable1 nm = genMergeable nm 1++-- | Derive 'Mergeable2' instance for GADT.+deriveGADTMergeable2 :: Name -> Q [Dec]+deriveGADTMergeable2 nm = genMergeable nm 2++-- | Derive 'Mergeable3' instance for GADT.+deriveGADTMergeable3 :: Name -> Q [Dec]+deriveGADTMergeable3 nm = genMergeable nm 3

@@ -0,0 +1,212 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TupleSections #-}++-- |+-- Module      :   Grisette.Internal.TH.GADT.UnaryOpCommon+-- Copyright   :   (c) Sirui Lu 2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Internal.TH.GADT.UnaryOpCommon+  ( UnaryOpClassConfig (..),+    UnaryOpFieldConfig (..),+    genUnaryOpClause,+    genUnaryOpClass,+  )+where++import Control.Monad (replicateM, zipWithM)+import qualified Data.Map as M+import Data.Maybe (catMaybes, mapMaybe)+import qualified Data.Set as S+import Grisette.Internal.TH.GADT.Common+  ( CheckArgsResult+      ( CheckArgsResult,+        argNewNames,+        constructors,+        isVarUsedInFields,+        keptNewNames,+        keptNewVars+      ),+    checkArgs,+  )+import Grisette.Internal.TH.Util (occName)+import Language.Haskell.TH+  ( Body (NormalB),+    Clause (Clause),+    Dec (FunD, InstanceD),+    Exp (ConE),+    Name,+    Pat (VarP, WildP),+    Pred,+    Q,+    Type (AppT, ArrowT, ConT, StarT, VarT),+    appE,+    conP,+    conT,+    newName,+    varE,+    varP,+    varT,+  )+import Language.Haskell.TH.Datatype+  ( ConstructorInfo (constructorFields, constructorName),+    TypeSubstitution (freeVariables),+    tvName,+  )+import Language.Haskell.TH.Datatype.TyVarBndr (TyVarBndr_, tvKind)++fieldExp :: [Name] -> M.Map Name Name -> Type -> Q Exp+fieldExp unaryOpFunNames argToFunPat ty = do+  let notContains =+        M.null $+          M.restrictKeys argToFunPat (S.fromList $ freeVariables [ty])+  let allArgNames = M.keysSet argToFunPat+  let typeHasNoArg ty =+        S.fromList (freeVariables [ty]) `S.intersection` allArgNames == S.empty+  if notContains+    then varE $ head unaryOpFunNames+    else case ty of+      _ | typeHasNoArg ty -> [|$(varE $ head unaryOpFunNames)|]+      AppT a b | typeHasNoArg a -> do+        [|+          $(varE $ unaryOpFunNames !! 1)+            $(fieldExp unaryOpFunNames argToFunPat b)+          |]+      AppT (AppT a b) c+        | typeHasNoArg a ->+            [|+              $(varE $ unaryOpFunNames !! 2)+                $(fieldExp unaryOpFunNames argToFunPat b)+                $(fieldExp unaryOpFunNames argToFunPat c)+              |]+      AppT (AppT (AppT a b) c) d+        | typeHasNoArg a ->+            [|+              $(varE $ unaryOpFunNames !! 3)+                $(fieldExp unaryOpFunNames argToFunPat b)+                $(fieldExp unaryOpFunNames argToFunPat c)+                $(fieldExp unaryOpFunNames argToFunPat d)+              |]+      VarT nm -> do+        case M.lookup nm argToFunPat of+          Just pname -> varE pname+          _ -> fail $ "fieldExp: unsupported type: " <> show ty+      _ -> fail $ "fieldExp: unsupported type: " <> show ty++patAndExps ::+  (M.Map Name Name -> Type -> Q Exp) -> [Name] -> [Type] -> Q ([Pat], [Exp])+patAndExps fieldFunExpGen argTypes fields = do+  let usedArgs = S.fromList $ freeVariables fields+  args <-+    traverse+      ( \nm ->+          if S.member nm usedArgs+            then do+              pname <- newName "p"+              return (nm, Just pname)+            else return (nm, Nothing)+      )+      argTypes+  let argToFunPat = M.fromList $ mapMaybe (\(nm, mpat) -> fmap (nm,) mpat) args+  let funPats = fmap (maybe WildP VarP . snd) args+  fieldEvalSymFunExps <- traverse (fieldFunExpGen argToFunPat) fields+  return (funPats, fieldEvalSymFunExps)++-- | Configuration for a unary function field expression generation on a GADT.+data UnaryOpFieldConfig = UnaryOpFieldConfig+  { extraPatNames :: [String],+    fieldCombineFun :: Exp -> [Exp] -> Q Exp+  }++-- | Generate a clause for a unary function on a GADT.+genUnaryOpClause ::+  [Name] ->+  UnaryOpFieldConfig ->+  [Name] ->+  ConstructorInfo ->+  Q Clause+genUnaryOpClause+  unaryOpFunNames+  (UnaryOpFieldConfig {..})+  argTypes+  conInfo = do+    let fields = constructorFields conInfo+    (funPats, fieldFunExps) <-+      patAndExps (fieldExp unaryOpFunNames) argTypes fields+    extraPatNames <- traverse newName extraPatNames+    fieldsPatNames <- replicateM (length fields) $ newName "field"+    let extraPats = fmap VarP extraPatNames+    fieldPats <- conP (constructorName conInfo) (fmap varP fieldsPatNames)++    fieldExps <-+      zipWithM+        ( \nm fun ->+            appE+              ( foldl+                  (\exp name -> appE exp (varE name))+                  (return fun)+                  extraPatNames+              )+              (varE nm)+        )+        fieldsPatNames+        fieldFunExps++    resExp <- fieldCombineFun (ConE (constructorName conInfo)) fieldExps+    return $ Clause (funPats ++ extraPats ++ [fieldPats]) (NormalB resExp) []++-- | Configuration for a unary operation type class generation on a GADT.+data UnaryOpClassConfig = UnaryOpClassConfig+  { unaryOpFieldConfig :: UnaryOpFieldConfig,+    unaryOpInstanceNames :: [Name],+    unaryOpFunNames :: [Name]+  }++-- | Generate a unary operation type class instance for a GADT.+genUnaryOpClass ::+  UnaryOpClassConfig ->+  Int ->+  Name ->+  Q [Dec]+genUnaryOpClass (UnaryOpClassConfig {..}) n typName = do+  CheckArgsResult {..} <-+    checkArgs+      (occName $ head unaryOpInstanceNames)+      (length unaryOpInstanceNames - 1)+      typName+      n+  let ctxForVar :: TyVarBndr_ flag -> Q (Maybe Pred)+      ctxForVar var = case tvKind var of+        StarT -> Just <$> [t|$(conT $ head unaryOpInstanceNames) $(varT $ tvName var)|]+        AppT (AppT ArrowT StarT) StarT ->+          Just <$> [t|$(conT $ unaryOpInstanceNames !! 1) $(varT $ tvName var)|]+        AppT (AppT (AppT ArrowT StarT) StarT) StarT ->+          Just <$> [t|$(conT $ unaryOpInstanceNames !! 2) $(varT $ tvName var)|]+        AppT (AppT (AppT (AppT ArrowT StarT) StarT) StarT) StarT ->+          Just <$> [t|$(conT $ unaryOpInstanceNames !! 3) $(varT $ tvName var)|]+        AppT (AppT (AppT (AppT ArrowT StarT) StarT) StarT) _ ->+          fail $ "Unsupported kind: " <> show (tvKind var)+        _ -> return Nothing+  ctxs <- traverse ctxForVar $ filter (isVarUsedInFields . tvName) keptNewVars+  clauses <-+    traverse+      (genUnaryOpClause unaryOpFunNames unaryOpFieldConfig argNewNames)+      constructors+  let instanceType =+        AppT (ConT $ unaryOpInstanceNames !! n) $+          foldl AppT (ConT typName) $+            fmap VarT keptNewNames+  let instanceFunName = unaryOpFunNames !! n+  let instanceFun = FunD instanceFunName clauses+  return+    [ InstanceD+        Nothing+        (catMaybes ctxs)+        instanceType+        [instanceFun]+    ]

@@ -1,147 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE TemplateHaskellQuotes #-}-{-# LANGUAGE Trustworthy #-}---- |--- Module      :   Grisette.Internal.TH.MergedConstructor--- Copyright   :   (c) Sirui Lu 2021-2024--- License     :   BSD-3-Clause (see the LICENSE file)------ Maintainer  :   siruilu@cs.washington.edu--- Stability   :   Experimental--- Portability :   GHC only-module Grisette.Internal.TH.MergeConstructor-  ( mkMergeConstructor,-    mkMergeConstructor',-  )-where--import Control.Monad (join, replicateM, when, zipWithM)-import Data.Bifunctor (Bifunctor (second))-import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)-import Grisette.Internal.Core.Data.Class.TryMerge (TryMerge)-import Grisette.Internal.TH.Util (constructorInfoToType, occName, putHaddock)-import Language.Haskell.TH-  ( Body (NormalB),-    Clause (Clause),-    Dec (FunD, SigD),-    Exp (AppE, ConE, LamE, VarE),-    Name,-    Pat (VarP),-    Pred,-    Q,-    Type (AppT, ArrowT, ForallT, VarT),-    mkName,-    newName,-  )-import Language.Haskell.TH.Datatype-  ( ConstructorInfo-      ( constructorFields,-        constructorName-      ),-    DatatypeInfo (datatypeCons),-    reifyDatatype,-  )-import Language.Haskell.TH.Datatype.TyVarBndr-  ( Specificity (SpecifiedSpec),-    TyVarBndrSpec,-    plainTVFlag,-  )---- | Generate constructor wrappers that wraps the result in a container with--- `TryMerge` with provided names.------ > mkMergeConstructor' ["mrgTuple2"] ''(,)------ generates------ > mrgTuple2 :: (Mergeable (a, b), Applicative m, TryMerge m) => a -> b -> u (a, b)--- > mrgTuple2 = \v1 v2 -> mrgSingle (v1, v2)-mkMergeConstructor' ::-  -- | Names for generated wrappers-  [String] ->-  -- | The type to generate the wrappers for-  Name ->-  Q [Dec]-mkMergeConstructor' names typName = do-  d <- reifyDatatype typName-  let constructors = datatypeCons d-  when (length names /= length constructors) $-    fail "Number of names does not match the number of constructors"-  ds <- zipWithM (mkSingleWrapper d) names constructors-  return $ join ds---- | Generate constructor wrappers that wraps the result in a container with--- `TryMerge`.------ > mkMergeConstructor "mrg" ''Maybe------ generates------ > mrgJust :: (Mergeable (Maybe a), Applicative m, TryMerge m) => m (Maybe a)--- > mrgNothing = mrgSingle Nothing--- > mrgJust :: (Mergeable (Maybe a), Applicative m, TryMerge m) => a -> m (Maybe a)--- > mrgJust = \x -> mrgSingle (Just x)-mkMergeConstructor ::-  -- | Prefix for generated wrappers-  String ->-  -- | The type to generate the wrappers for-  Name ->-  Q [Dec]-mkMergeConstructor prefix typName = do-  d <- reifyDatatype typName-  let constructorNames = occName . constructorName <$> datatypeCons d-  mkMergeConstructor' ((prefix ++) <$> constructorNames) typName--augmentNormalCExpr :: Int -> Exp -> Q Exp-augmentNormalCExpr n f = do-  xs <- replicateM n (newName "x")-  let args = map VarP xs-  mrgSingleFun <- [|mrgSingle|]-  return $-    LamE-      args-      ( AppE mrgSingleFun $-          foldl AppE f (map VarE xs)-      )--augmentFinalType :: Type -> Q (([TyVarBndrSpec], [Pred]), Type)-augmentFinalType (AppT a@(AppT ArrowT _) t) = do-  tl <- augmentFinalType t-  return $ second (AppT a) tl-augmentFinalType t = do-  mName <- newName "m"-  let mTy = VarT mName-  mergeable <- [t|Mergeable|]-  applicative <- [t|Applicative|]-  tryMerge <- [t|TryMerge|]-  return-    ( ( [plainTVFlag mName SpecifiedSpec],-        [AppT mergeable t, AppT applicative mTy, AppT tryMerge mTy]-      ),-      AppT mTy t-    )--augmentConstructorType :: Type -> Q Type-augmentConstructorType (ForallT tybinders ctx ty1) = do-  ((bndrs, preds), augmentedTyp) <- augmentFinalType ty1-  return $ ForallT (tybinders ++ bndrs) (preds ++ ctx) augmentedTyp-augmentConstructorType t = do-  ((bndrs, preds), augmentedTyp) <- augmentFinalType t-  return $ ForallT bndrs preds augmentedTyp--mkSingleWrapper :: DatatypeInfo -> String -> ConstructorInfo -> Q [Dec]-mkSingleWrapper dataType name info = do-  constructorTyp <- constructorInfoToType dataType info-  augmentedTyp <- augmentConstructorType constructorTyp-  let oriName = constructorName info-  let retName = mkName name-  expr <- augmentNormalCExpr (length $ constructorFields info) (ConE oriName)-  putHaddock retName $-    "Smart constructor for v'"-      <> show oriName-      <> "' to construct values wrapped and possibly merged in a container."-  return-    [ SigD retName augmentedTyp,-      FunD retName [Clause [] (NormalB expr) []]-    ]

@@ -1,156 +0,0 @@-{-# LANGUAGE TemplateHaskell #-}---- |--- Module      :   Grisette.Internal.TH.UnifiedConstructor--- Copyright   :   (c) Sirui Lu 2024--- License     :   BSD-3-Clause (see the LICENSE file)------ Maintainer  :   siruilu@cs.washington.edu--- Stability   :   Experimental--- Portability :   GHC only-module Grisette.Internal.TH.UnifiedConstructor-  ( mkUnifiedConstructor,-    mkUnifiedConstructor',-  )-where--import Control.Monad (join, replicateM, when, zipWithM)-import Grisette.Internal.TH.Util (constructorInfoToType, occName, putHaddock)-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag)-import Grisette.Unified.Internal.UnifiedData-  ( GetData,-    UnifiedData,-    wrapData,-  )-import Language.Haskell.TH (pprint)-import Language.Haskell.TH.Datatype-  ( ConstructorInfo (constructorFields, constructorName),-    DatatypeInfo (datatypeCons, datatypeVars),-    reifyDatatype,-    tvKind,-    tvName,-  )-import Language.Haskell.TH.Datatype.TyVarBndr (TyVarBndrSpec, kindedTVSpecified)-import Language.Haskell.TH.Lib (appE, appTypeE, lamE, varE, varP)-import Language.Haskell.TH.Syntax-  ( Body (NormalB),-    Clause (Clause),-    Dec (FunD, SigD),-    Exp (ConE),-    Name,-    Pred,-    Q,-    Type (AppT, ArrowT, ConT, ForallT, VarT),-    mkName,-    newName,-  )---- | Generate smart constructors to create unified values.------ For a type @T mode a b c@ with constructors @T1@, @T2@, etc., this function--- will generate smart constructors with the given prefix, e.g., @mkT1@, @mkT2@,--- etc.------ The generated smart constructors will contruct values of type--- @GetData mode (T mode a b c)@.-mkUnifiedConstructor ::-  -- | Prefix for generated wrappers-  String ->-  -- | The type to generate the wrappers for-  Name ->-  Q [Dec]-mkUnifiedConstructor prefix typName = do-  d <- reifyDatatype typName-  let constructorNames = occName . constructorName <$> datatypeCons d-  mkUnifiedConstructor' ((prefix ++) <$> constructorNames) typName---- | Generate smart constructors to create unified values.------ For a type @T mode a b c@ with constructors @T1@, @T2@, etc., this function--- will generate smart constructors with the given names.------ The generated smart constructors will contruct values of type--- @GetData mode (T mode a b c)@.-mkUnifiedConstructor' ::-  -- | Names for generated wrappers-  [String] ->-  -- | The type to generate the wrappers for-  Name ->-  Q [Dec]-mkUnifiedConstructor' names typName = do-  d <- reifyDatatype typName-  let constructors = datatypeCons d-  when (length names /= length constructors) $-    fail "Number of names does not match the number of constructors"-  let modeVars = filter ((== ConT ''EvalModeTag) . tvKind) (datatypeVars d)-  -- when (length modeVars /= 1) $-  --  fail "Expected exactly one EvalModeTag variable in the datatype."-  case modeVars of-    [mode] -> do-      ds <--        zipWithM-          (mkSingleWrapper d Nothing $ VarT $ tvName mode)-          names-          constructors-      return $ join ds-    [] -> do-      n <- newName "mode"-      let newBndr = kindedTVSpecified n (ConT ''EvalModeTag)-      ds <--        zipWithM-          (mkSingleWrapper d (Just newBndr) (VarT n))-          names-          constructors-      return $ join ds-    _ -> fail "Expected one or zero EvalModeTag variable in the datatype."--augmentFinalType :: Type -> Type -> Q ([Pred], Type)-augmentFinalType mode (AppT a@(AppT ArrowT _) t) = do-  (pred, ret) <- augmentFinalType mode t-  return (pred, AppT a ret)-augmentFinalType mode t = do-  r <- [t|GetData $(return mode) $(return t)|]-  predu <- [t|UnifiedData $(return mode) $(return t)|]-  return ([predu], r)--augmentConstructorType :: Maybe TyVarBndrSpec -> Type -> Type -> Q Type-augmentConstructorType modeBndr mode (ForallT tybinders ctx ty1) = do-  (preds, augmentedTyp) <- augmentFinalType mode ty1-  case modeBndr of-    Just bndr -> return $ ForallT (bndr : tybinders) (preds ++ ctx) augmentedTyp-    Nothing -> return $ ForallT tybinders (preds ++ ctx) augmentedTyp-augmentConstructorType modeBndr mode ty = do-  (preds, augmentedTyp) <- augmentFinalType mode ty-  case modeBndr of-    Just bndr -> return $ ForallT [bndr] preds augmentedTyp-    Nothing ->-      fail $-        "augmentConstructorType: unsupported constructor type: " ++ pprint ty--augmentExpr :: Type -> Int -> Exp -> Q Exp-augmentExpr mode n f = do-  xs <- replicateM n (newName "x")-  let args = map varP xs-  lamE-    args-    ( ( appE-          (appTypeE [|wrapData|] (return mode))-          (foldl appE (return f) (map varE xs))-      )-    )--mkSingleWrapper :: DatatypeInfo -> Maybe TyVarBndrSpec -> Type -> String -> ConstructorInfo -> Q [Dec]-mkSingleWrapper dataType modeBndr mode name info = do-  constructorTyp <- constructorInfoToType dataType info-  augmentedTyp <- augmentConstructorType modeBndr mode constructorTyp-  let oriName = constructorName info-  let retName = mkName name-  expr <- augmentExpr mode (length $ constructorFields info) (ConE oriName)-  putHaddock retName $-    "Smart constructor for v'"-      <> show oriName-      <> "' to construct unified value."-  return-    [ SigD retName augmentedTyp,-      FunD retName [Clause [] (NormalB expr) []]-    ]

@@ -106,7 +106,7 @@     mrgMapM,     mrgSequence,   )-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Sym))+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (S)) import qualified Grisette.Unified.Lib.Control.Monad as Unified  -- | 'return' with 'MergingStrategy' knowledge propagation.@@ -318,7 +318,7 @@   int ->   m a ->   m [a]-symReplicateM = Unified.symReplicateM @'Sym+symReplicateM = Unified.symReplicateM @'S {-# INLINE symReplicateM #-}  -- | 'Control.Monad.replicateM_' with 'MergingStrategy' knowledge propagation.@@ -338,7 +338,7 @@   int ->   m a ->   m ()-symReplicateM_ = Unified.symReplicateM_ @'Sym+symReplicateM_ = Unified.symReplicateM_ @'S {-# INLINE symReplicateM_ #-}  -- | 'Control.Monad.guard' with 'MergingStrategy' knowledge propagation.

@@ -13,9 +13,8 @@ -- Portability :   GHC only module Grisette.Lib.Data.Bool (mrgTrue, mrgFalse) where -import Grisette.Internal.Core.Data.Class.TryMerge (mrgSingle)-import Grisette.Internal.TH.MergeConstructor-  ( mkMergeConstructor,+import Grisette.Internal.TH.Ctor.SmartConstructor+  ( makePrefixedSmartCtor,   ) -mkMergeConstructor "mrg" ''Bool+makePrefixedSmartCtor "mrg" ''Bool

@@ -13,9 +13,8 @@ -- Portability :   GHC only module Grisette.Lib.Data.Either (mrgLeft, mrgRight) where -import Grisette.Internal.Core.Data.Class.TryMerge (mrgSingle)-import Grisette.Internal.TH.MergeConstructor-  ( mkMergeConstructor,+import Grisette.Internal.TH.Ctor.SmartConstructor+  ( makePrefixedSmartCtor,   ) -mkMergeConstructor "mrg" ''Either+makePrefixedSmartCtor "mrg" ''Either

@@ -66,7 +66,7 @@   ) import Grisette.Internal.SymPrim.SymBool (SymBool) import Grisette.Lib.Control.Applicative (mrgAsum)-import Grisette.Unified (EvalModeTag (Sym))+import Grisette.Unified (EvalModeTag (S)) import qualified Grisette.Unified.Lib.Data.Foldable as Unified  -- | 'Data.Foldable.elem' with symbolic equality.@@ -81,7 +81,7 @@   (Foldable t, MonadUnion m, Mergeable a, SymOrd a) =>   t a ->   m a-mrgMaximum = Unified.mrgMaximum @'Sym+mrgMaximum = Unified.mrgMaximum @'S {-# INLINE mrgMaximum #-}  -- | 'Data.Foldable.maximum' with result merged with 'ITEOp'.@@ -90,7 +90,7 @@   (Foldable t, Mergeable a, SymOrd a, ITEOp a) =>   t a ->   a-symMaximum = Unified.symMaximum @'Sym+symMaximum = Unified.symMaximum @'S {-# INLINE symMaximum #-}  -- | 'Data.Foldable.minimum' with 'Grisette.Core.MergingStrategy' knowledge@@ -100,7 +100,7 @@   (Foldable t, MonadUnion m, Mergeable a, SymOrd a) =>   t a ->   m a-mrgMinimum = Unified.mrgMinimum @'Sym+mrgMinimum = Unified.mrgMinimum @'S {-# INLINE mrgMinimum #-}  -- | 'Data.Foldable.minimum' with result merged with 'ITEOp'.@@ -109,7 +109,7 @@   (Foldable t, Mergeable a, SymOrd a, ITEOp a) =>   t a ->   a-symMinimum = Unified.symMinimum @'Sym+symMinimum = Unified.symMinimum @'S {-# INLINE symMinimum #-}  -- | 'Data.Foldable.foldrM' with 'Grisette.Core.MergingStrategy' knowledge

@@ -14,9 +14,8 @@ module Grisette.Lib.Data.Functor.Sum (mrgInR, mrgInL) where  import Data.Functor.Sum (Sum)-import Grisette.Internal.Core.Data.Class.TryMerge (mrgSingle)-import Grisette.Internal.TH.MergeConstructor-  ( mkMergeConstructor,+import Grisette.Internal.TH.Ctor.SmartConstructor+  ( makePrefixedSmartCtor,   ) -mkMergeConstructor "mrg" ''Sum+makePrefixedSmartCtor "mrg" ''Sum

@@ -13,9 +13,8 @@ -- Portability :   GHC only module Grisette.Lib.Data.Maybe (mrgNothing, mrgJust) where -import Grisette.Internal.Core.Data.Class.TryMerge (mrgSingle)-import Grisette.Internal.TH.MergeConstructor-  ( mkMergeConstructor,+import Grisette.Internal.TH.Ctor.SmartConstructor+  ( makePrefixedSmartCtor,   ) -mkMergeConstructor "mrg" ''Maybe+makePrefixedSmartCtor "mrg" ''Maybe

@@ -24,16 +24,15 @@   ) where -import Grisette.Internal.Core.Data.Class.TryMerge (mrgSingle)-import Grisette.Internal.TH.MergeConstructor-  ( mkMergeConstructor',+import Grisette.Internal.TH.Ctor.SmartConstructor+  ( makeNamedSmartCtor,   ) -mkMergeConstructor' ["mrgUnit"] ''()-mkMergeConstructor' ["mrgTuple2"] ''(,)-mkMergeConstructor' ["mrgTuple3"] ''(,,)-mkMergeConstructor' ["mrgTuple4"] ''(,,,)-mkMergeConstructor' ["mrgTuple5"] ''(,,,,)-mkMergeConstructor' ["mrgTuple6"] ''(,,,,,)-mkMergeConstructor' ["mrgTuple7"] ''(,,,,,,)-mkMergeConstructor' ["mrgTuple8"] ''(,,,,,,,)+makeNamedSmartCtor ["mrgUnit"] ''()+makeNamedSmartCtor ["mrgTuple2"] ''(,)+makeNamedSmartCtor ["mrgTuple3"] ''(,,)+makeNamedSmartCtor ["mrgTuple4"] ''(,,,)+makeNamedSmartCtor ["mrgTuple5"] ''(,,,,)+makeNamedSmartCtor ["mrgTuple6"] ''(,,,,,)+makeNamedSmartCtor ["mrgTuple7"] ''(,,,,,,)+makeNamedSmartCtor ["mrgTuple8"] ''(,,,,,,,)

@@ -155,6 +155,11 @@     type (=~>) (..),     type (-~>) (..), +    -- ** Shared constraints+    Prim,+    SymPrim,+    BasicSymPrim,+     -- ** Quantifiers     forallSet,     forallSym,@@ -336,6 +341,11 @@ import Grisette.Internal.SymPrim.SymGeneralFun ((-->), type (-~>) (..)) import Grisette.Internal.SymPrim.SymInteger   ( SymInteger (..),+  )+import Grisette.Internal.SymPrim.SymPrim+  ( BasicSymPrim,+    Prim,+    SymPrim,   ) import Grisette.Internal.SymPrim.SymTabularFun (type (=~>) (..)) import Grisette.Internal.SymPrim.TabularFun (type (=->) (..))

@@ -13,14 +13,21 @@     derive,     deriveAll,     deriveAllExcept,+    deriveGADT,+    deriveGADTAll,+    deriveGADTAllExcept,      -- * Smart constructors that merges in a monad-    mkMergeConstructor,-    mkMergeConstructor',+    makePrefixedSmartCtor,+    makeNamedSmartCtor,+    makeSmartCtor,+    makeSmartCtorWith,      -- * Smart constructors that are polymorphic in evaluation modes-    mkUnifiedConstructor,-    mkUnifiedConstructor',+    makePrefixedUnifiedCtor,+    makeNamedUnifiedCtor,+    makeUnifiedCtor,+    makeUnifiedCtorWith,      -- * Tools for building more derivation procedures @@ -51,6 +58,18 @@   ) where +import Grisette.Internal.TH.Ctor.SmartConstructor+  ( makeNamedSmartCtor,+    makePrefixedSmartCtor,+    makeSmartCtor,+    makeSmartCtorWith,+  )+import Grisette.Internal.TH.Ctor.UnifiedConstructor+  ( makeNamedUnifiedCtor,+    makePrefixedUnifiedCtor,+    makeUnifiedCtor,+    makeUnifiedCtorWith,+  ) import Grisette.Internal.TH.DeriveBuiltin   ( deriveBuiltinExtra,   )@@ -81,11 +100,4 @@     deriveUnifiedInterfaceExtra,   ) import Grisette.Internal.TH.DeriveWithHandlers (deriveWithHandlers)-import Grisette.Internal.TH.MergeConstructor-  ( mkMergeConstructor,-    mkMergeConstructor',-  )-import Grisette.Internal.TH.UnifiedConstructor-  ( mkUnifiedConstructor,-    mkUnifiedConstructor',-  )+import Grisette.Internal.TH.GADT.DeriveGADT (deriveGADT, deriveGADTAll, deriveGADTAllExcept)

@@ -115,6 +115,10 @@     UnifiedSafeFdiv (..),     safeFdiv, +    -- ** Shared constraints+    UnifiedPrim,+    UnifiedBasicPrim,+     -- * Unified types      -- ** Boolean@@ -340,4 +344,8 @@ import Grisette.Unified.Internal.UnifiedInteger   ( GetInteger,     UnifiedInteger,+  )+import Grisette.Unified.Internal.UnifiedPrim+  ( UnifiedBasicPrim,+    UnifiedPrim,   )

@@ -28,7 +28,7 @@ import Grisette.Internal.SymPrim.BV (IntN, WordN) import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN) import Grisette.Unified.Internal.Class.UnifiedFromIntegral (UnifiedFromIntegral)-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Con, Sym))+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S)) import Grisette.Unified.Internal.UnifiedBV (UnifiedBVImpl (GetIntN, GetWordN))  class@@ -54,12 +54,12 @@ #define CONINSTANCE(ty0, ty1) \ instance \   (KnownNat n0, 1 <= n0, KnownNat n1, 1 <= n1) => \-  UnifiedBVBVConversionImpl QUOTE()Con ty0 ty1 n0 n1 (ty0 n0) (ty1 n1)+  UnifiedBVBVConversionImpl QUOTE()C ty0 ty1 n0 n1 (ty0 n0) (ty1 n1)  #define SYMINSTANCE(ty0, ty1) \ instance \   (KnownNat n0, 1 <= n0, KnownNat n1, 1 <= n1) => \-  UnifiedBVBVConversionImpl QUOTE()Sym ty0 ty1 n0 n1 (ty0 n0) (ty1 n1)+  UnifiedBVBVConversionImpl QUOTE()S ty0 ty1 n0 n1 (ty0 n0) (ty1 n1)  #if 1 CONINSTANCE(WordN, WordN)

@@ -47,7 +47,7 @@ import Grisette.Unified.Internal.Class.UnifiedSafeBitCast (UnifiedSafeBitCast) import Grisette.Unified.Internal.Class.UnifiedSafeFromFP (UnifiedSafeFromFP) import Grisette.Unified.Internal.Class.UnifiedSimpleMergeable (UnifiedBranching)-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Con, Sym))+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S)) import Grisette.Unified.Internal.UnifiedBV (UnifiedBVImpl (GetIntN, GetWordN)) import Grisette.Unified.Internal.UnifiedFP   ( UnifiedFPImpl (GetFP, GetFPRoundingMode),@@ -83,7 +83,7 @@ instance   (ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) =>   UnifiedBVFPConversionImpl-    'Con+    'C     WordN     IntN     FP@@ -98,7 +98,7 @@ instance   (ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) =>   UnifiedBVFPConversionImpl-    'Sym+    'S     SymWordN     SymIntN     SymFP

@@ -9,43 +9,12 @@ -- Stability   :   Experimental -- Portability :   GHC only module Grisette.Unified.Internal.BaseConstraint-  ( BasicGrisetteType,-    ConSymConversion,+  ( ConSymConversion,   ) where -import Control.DeepSeq (NFData)-import Data.Bytes.Serial (Serial)-import Data.Hashable (Hashable)-import Grisette.Internal.Core.Data.Class.EvalSym (EvalSym)-import Grisette.Internal.Core.Data.Class.ExtractSym (ExtractSym)-import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)-import Grisette.Internal.Core.Data.Class.PPrint (PPrint)-import Grisette.Internal.Core.Data.Class.SubstSym (SubstSym)-import Grisette.Internal.Core.Data.Class.SymEq (SymEq)-import Grisette.Internal.Core.Data.Class.SymOrd (SymOrd) import Grisette.Internal.Core.Data.Class.ToCon (ToCon) import Grisette.Internal.Core.Data.Class.ToSym (ToSym)-import Grisette.Internal.SymPrim.AllSyms (AllSyms)-import Language.Haskell.TH.Syntax (Lift)---- | A type that is used as a constraint for all the types in Grisette.-type BasicGrisetteType t =-  ( AllSyms t,-    Eq t,-    EvalSym t,-    ExtractSym t,-    PPrint t,-    Hashable t,-    Lift t,-    Mergeable t,-    NFData t,-    SymEq t,-    Show t,-    SymOrd t,-    Serial t,-    SubstSym t-  )  -- | A type that is used as a constraint for all the types in Grisette that can -- be converted between concrete and symbolic types.

@@ -18,14 +18,14 @@ import Control.Monad.Identity (Identity) import Data.Kind (Type) import Grisette.Internal.Core.Control.Monad.Union (Union)-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Con, Sym))+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S))  -- | A type family that specifies the base monad for the evaluation mode. ----- Resolves to 'Identity' for `Con` mode, and 'Union' for `Sym` mode.+-- Resolves to 'Identity' for `C` mode, and 'Union' for `S` mode. type family   BaseMonad (mode :: EvalModeTag) =     (r :: Type -> Type) | r -> mode   where-  BaseMonad 'Con = Identity-  BaseMonad 'Sym = Union+  BaseMonad 'C = Identity+  BaseMonad 'S = Union

@@ -55,7 +55,7 @@ import Grisette.Unified.Internal.Class.UnifiedITEOp   ( UnifiedITEOp (withBaseITEOp),   )-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Con, Sym), IsConMode)+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S), IsConMode) import Grisette.Unified.Internal.UnifiedBool (UnifiedBool (GetBool)) import Grisette.Unified.Internal.Util (withMode) @@ -130,43 +130,43 @@  -- | Unified `Grisette.Internal.Core.Data.Class.SymFiniteBits.symPopCount`. symPopCount ::-  forall mode a b.-  (Typeable mode, UnifiedFiniteBits mode a, Num b, UnifiedITEOp mode b) =>+  forall mode a.+  (Typeable mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) =>   a ->-  b+  a symPopCount a =   withMode @mode     (withBaseFiniteBits @mode @a (fromIntegral $ popCount a))     ( withBaseFiniteBits @mode @a $-        withBaseITEOp @mode @b (SymFiniteBits.symPopCount a)+        withBaseITEOp @mode @a (SymFiniteBits.symPopCount a)     )  -- | Unified -- `Grisette.Internal.Core.Data.Class.SymFiniteBits.symCountLeadingZeros`. symCountLeadingZeros ::-  forall mode a b.-  (Typeable mode, UnifiedFiniteBits mode a, Num b, UnifiedITEOp mode b) =>+  forall mode a.+  (Typeable mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) =>   a ->-  b+  a symCountLeadingZeros a =   withMode @mode     (withBaseFiniteBits @mode @a (fromIntegral $ countLeadingZeros a))     ( withBaseFiniteBits @mode @a $-        withBaseITEOp @mode @b (SymFiniteBits.symCountLeadingZeros a)+        withBaseITEOp @mode @a (SymFiniteBits.symCountLeadingZeros a)     )  -- | Unified -- `Grisette.Internal.Core.Data.Class.SymFiniteBits.symCountTrailingZeros`. symCountTrailingZeros ::-  forall mode a b.-  (Typeable mode, UnifiedFiniteBits mode a, Num b, UnifiedITEOp mode b) =>+  forall mode a.+  (Typeable mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) =>   a ->-  b+  a symCountTrailingZeros a =   withMode @mode     (withBaseFiniteBits @mode @a (fromIntegral $ countTrailingZeros a))     ( withBaseFiniteBits @mode @a $-        withBaseITEOp @mode @b (SymFiniteBits.symCountTrailingZeros a)+        withBaseITEOp @mode @a (SymFiniteBits.symCountTrailingZeros a)     )  -- | A class that provides unified equality comparison.@@ -178,26 +178,26 @@     ((If (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a)) => r) ->     r -instance (KnownNat n, 1 <= n) => UnifiedFiniteBits 'Con (WordN n) where+instance (KnownNat n, 1 <= n) => UnifiedFiniteBits 'C (WordN n) where   withBaseFiniteBits r = r -instance (KnownNat n, 1 <= n) => UnifiedFiniteBits 'Con (IntN n) where+instance (KnownNat n, 1 <= n) => UnifiedFiniteBits 'C (IntN n) where   withBaseFiniteBits r = r -instance UnifiedFiniteBits 'Con SomeWordN where+instance UnifiedFiniteBits 'C SomeWordN where   withBaseFiniteBits r = r -instance UnifiedFiniteBits 'Con SomeIntN where+instance UnifiedFiniteBits 'C SomeIntN where   withBaseFiniteBits r = r -instance (KnownNat n, 1 <= n) => UnifiedFiniteBits 'Sym (SymWordN n) where+instance (KnownNat n, 1 <= n) => UnifiedFiniteBits 'S (SymWordN n) where   withBaseFiniteBits r = r -instance (KnownNat n, 1 <= n) => UnifiedFiniteBits 'Sym (SymIntN n) where+instance (KnownNat n, 1 <= n) => UnifiedFiniteBits 'S (SymIntN n) where   withBaseFiniteBits r = r -instance UnifiedFiniteBits 'Sym SomeSymWordN where+instance UnifiedFiniteBits 'S SomeSymWordN where   withBaseFiniteBits r = r -instance UnifiedFiniteBits 'Sym SomeSymIntN where+instance UnifiedFiniteBits 'S SomeSymIntN where   withBaseFiniteBits r = r

@@ -36,7 +36,7 @@ import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN) import Grisette.Internal.SymPrim.SymFP (SymFP) import Grisette.Internal.SymPrim.SymInteger (SymInteger)-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Con, Sym), IsConMode)+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S), IsConMode) import Grisette.Unified.Internal.Util (withMode)  -- | Unified `Grisette.Internal.Core.Data.Class.SymFromIntegral.symFromIntegral`@@ -69,158 +69,158 @@   where   withBaseFromIntegral r = r -instance UnifiedFromIntegral 'Con Integer AlgReal where+instance UnifiedFromIntegral 'C Integer AlgReal where   withBaseFromIntegral r = r -instance UnifiedFromIntegral 'Con Integer Integer where+instance UnifiedFromIntegral 'C Integer Integer where   withBaseFromIntegral r = r -instance (KnownNat n, 1 <= n) => UnifiedFromIntegral 'Con Integer (IntN n) where+instance (KnownNat n, 1 <= n) => UnifiedFromIntegral 'C Integer (IntN n) where   withBaseFromIntegral r = r  instance   (KnownNat n, 1 <= n) =>-  UnifiedFromIntegral 'Con Integer (WordN n)+  UnifiedFromIntegral 'C Integer (WordN n)   where   withBaseFromIntegral r = r -instance (ValidFP eb sb) => UnifiedFromIntegral 'Con Integer (FP eb sb) where+instance (ValidFP eb sb) => UnifiedFromIntegral 'C Integer (FP eb sb) where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n') =>-  UnifiedFromIntegral 'Con (IntN n') AlgReal+  UnifiedFromIntegral 'C (IntN n') AlgReal   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n') =>-  UnifiedFromIntegral 'Con (IntN n') Integer+  UnifiedFromIntegral 'C (IntN n') Integer   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>-  UnifiedFromIntegral 'Con (IntN n') (IntN n)+  UnifiedFromIntegral 'C (IntN n') (IntN n)   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>-  UnifiedFromIntegral 'Con (IntN n') (WordN n)+  UnifiedFromIntegral 'C (IntN n') (WordN n)   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n', ValidFP eb sb) =>-  UnifiedFromIntegral 'Con (IntN n') (FP eb sb)+  UnifiedFromIntegral 'C (IntN n') (FP eb sb)   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n') =>-  UnifiedFromIntegral 'Con (WordN n') AlgReal+  UnifiedFromIntegral 'C (WordN n') AlgReal   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n') =>-  UnifiedFromIntegral 'Con (WordN n') Integer+  UnifiedFromIntegral 'C (WordN n') Integer   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>-  UnifiedFromIntegral 'Con (WordN n') (IntN n)+  UnifiedFromIntegral 'C (WordN n') (IntN n)   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>-  UnifiedFromIntegral 'Con (WordN n') (WordN n)+  UnifiedFromIntegral 'C (WordN n') (WordN n)   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n', ValidFP eb sb) =>-  UnifiedFromIntegral 'Con (WordN n') (FP eb sb)+  UnifiedFromIntegral 'C (WordN n') (FP eb sb)   where   withBaseFromIntegral r = r -instance UnifiedFromIntegral 'Sym SymInteger SymAlgReal where+instance UnifiedFromIntegral 'S SymInteger SymAlgReal where   withBaseFromIntegral r = r -instance UnifiedFromIntegral 'Sym SymInteger SymInteger where+instance UnifiedFromIntegral 'S SymInteger SymInteger where   withBaseFromIntegral r = r -instance (KnownNat n, 1 <= n) => UnifiedFromIntegral 'Sym SymInteger (SymIntN n) where+instance (KnownNat n, 1 <= n) => UnifiedFromIntegral 'S SymInteger (SymIntN n) where   withBaseFromIntegral r = r  instance   (KnownNat n, 1 <= n) =>-  UnifiedFromIntegral 'Sym SymInteger (SymWordN n)+  UnifiedFromIntegral 'S SymInteger (SymWordN n)   where   withBaseFromIntegral r = r -instance (ValidFP eb sb) => UnifiedFromIntegral 'Sym SymInteger (SymFP eb sb) where+instance (ValidFP eb sb) => UnifiedFromIntegral 'S SymInteger (SymFP eb sb) where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n') =>-  UnifiedFromIntegral 'Sym (SymIntN n') SymAlgReal+  UnifiedFromIntegral 'S (SymIntN n') SymAlgReal   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n') =>-  UnifiedFromIntegral 'Sym (SymIntN n') SymInteger+  UnifiedFromIntegral 'S (SymIntN n') SymInteger   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>-  UnifiedFromIntegral 'Sym (SymIntN n') (SymIntN n)+  UnifiedFromIntegral 'S (SymIntN n') (SymIntN n)   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>-  UnifiedFromIntegral 'Sym (SymIntN n') (SymWordN n)+  UnifiedFromIntegral 'S (SymIntN n') (SymWordN n)   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n', ValidFP eb sb) =>-  UnifiedFromIntegral 'Sym (SymIntN n') (SymFP eb sb)+  UnifiedFromIntegral 'S (SymIntN n') (SymFP eb sb)   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n') =>-  UnifiedFromIntegral 'Sym (SymWordN n') SymAlgReal+  UnifiedFromIntegral 'S (SymWordN n') SymAlgReal   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n') =>-  UnifiedFromIntegral 'Sym (SymWordN n') SymInteger+  UnifiedFromIntegral 'S (SymWordN n') SymInteger   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>-  UnifiedFromIntegral 'Sym (SymWordN n') (SymIntN n)+  UnifiedFromIntegral 'S (SymWordN n') (SymIntN n)   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n', KnownNat n, 1 <= n) =>-  UnifiedFromIntegral 'Sym (SymWordN n') (SymWordN n)+  UnifiedFromIntegral 'S (SymWordN n') (SymWordN n)   where   withBaseFromIntegral r = r  instance   (KnownNat n', 1 <= n', ValidFP eb sb) =>-  UnifiedFromIntegral 'Sym (SymWordN n') (SymFP eb sb)+  UnifiedFromIntegral 'S (SymWordN n') (SymFP eb sb)   where   withBaseFromIntegral r = r

@@ -38,7 +38,7 @@ import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable) import qualified Grisette.Internal.Core.Data.Class.PlainUnion import Grisette.Unified.Internal.BaseMonad (BaseMonad)-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Sym), IsConMode)+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (S), IsConMode) import Grisette.Unified.Internal.UnifiedBool (UnifiedBool (GetBool)) import Grisette.Unified.Internal.Util (withMode) @@ -101,6 +101,6 @@   withBaseITEOp r = withMode @mode r r   {-# INLINE withBaseITEOp #-} -instance (Mergeable v, UnifiedITEOp 'Sym v) => UnifiedITEOp 'Sym (Union v) where-  withBaseITEOp r = withBaseITEOp @'Sym @v r+instance (Mergeable v, UnifiedITEOp 'S v) => UnifiedITEOp 'S (Union v) where+  withBaseITEOp r = withBaseITEOp @'S @v r   {-# INLINE withBaseITEOp #-}

@@ -0,0 +1,108 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++-- |+-- Module      :   Grisette.Unified.Internal.Class.UnifiedRep+-- Copyright   :   (c) Sirui Lu 2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Unified.Internal.Class.UnifiedRep+  ( UnifiedConRep (..),+    UnifiedSymRep (..),+  )+where++import GHC.TypeLits (KnownNat, type (<=))+import Grisette.Internal.SymPrim.AlgReal (AlgReal)+import Grisette.Internal.SymPrim.BV (IntN, WordN)+import Grisette.Internal.SymPrim.FP (FP, ValidFP)+import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal)+import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)+import Grisette.Internal.SymPrim.SymBool (SymBool)+import Grisette.Internal.SymPrim.SymFP (SymFP)+import Grisette.Internal.SymPrim.SymInteger (SymInteger)++-- | A class that gives the concrete type of a unified primitive type.+class UnifiedConRep a where+  type ConType a++-- | A class that gives the symbolic type of a unified primitive type.+class UnifiedSymRep a where+  type SymType a++instance UnifiedConRep Bool where+  type ConType Bool = Bool++instance UnifiedSymRep Bool where+  type SymType Bool = SymBool++instance UnifiedConRep SymBool where+  type ConType SymBool = Bool++instance UnifiedSymRep SymBool where+  type SymType SymBool = SymBool++instance UnifiedConRep Integer where+  type ConType Integer = Integer++instance UnifiedSymRep Integer where+  type SymType Integer = SymInteger++instance UnifiedConRep SymInteger where+  type ConType SymInteger = Integer++instance UnifiedSymRep SymInteger where+  type SymType SymInteger = SymInteger++instance UnifiedConRep AlgReal where+  type ConType AlgReal = AlgReal++instance UnifiedSymRep AlgReal where+  type SymType AlgReal = SymAlgReal++instance UnifiedConRep SymAlgReal where+  type ConType SymAlgReal = AlgReal++instance UnifiedSymRep SymAlgReal where+  type SymType SymAlgReal = SymAlgReal++instance (KnownNat n, 1 <= n) => UnifiedConRep (IntN n) where+  type ConType (IntN n) = IntN n++instance (KnownNat n, 1 <= n) => UnifiedSymRep (IntN n) where+  type SymType (IntN n) = SymIntN n++instance (KnownNat n, 1 <= n) => UnifiedConRep (SymIntN n) where+  type ConType (SymIntN n) = IntN n++instance (KnownNat n, 1 <= n) => UnifiedSymRep (SymIntN n) where+  type SymType (SymIntN n) = SymIntN n++instance (KnownNat n, 1 <= n) => UnifiedConRep (WordN n) where+  type ConType (WordN n) = WordN n++instance (KnownNat n, 1 <= n) => UnifiedSymRep (WordN n) where+  type SymType (WordN n) = SymWordN n++instance (KnownNat n, 1 <= n) => UnifiedConRep (SymWordN n) where+  type ConType (SymWordN n) = WordN n++instance (KnownNat n, 1 <= n) => UnifiedSymRep (SymWordN n) where+  type SymType (SymWordN n) = SymWordN n++instance (ValidFP eb sb) => UnifiedConRep (FP eb sb) where+  type ConType (FP eb sb) = FP eb sb++instance (ValidFP eb sb) => UnifiedSymRep (FP eb sb) where+  type SymType (FP eb sb) = SymFP eb sb++instance (ValidFP eb sb) => UnifiedConRep (SymFP eb sb) where+  type ConType (SymFP eb sb) = FP eb sb++instance (ValidFP eb sb) => UnifiedSymRep (SymFP eb sb) where+  type SymType (SymFP eb sb) = SymFP eb sb

@@ -40,7 +40,7 @@ import Grisette.Unified.Internal.Class.UnifiedSimpleMergeable   ( UnifiedBranching (withBaseBranching),   )-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Sym))+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (S)) import Grisette.Unified.Internal.Util (withMode)  -- | Unified `Grisette.Internal.Core.Data.Class.SafeLinearArith.safeSub`@@ -105,24 +105,24 @@  instance   ( MonadError NotRepresentableFPError m,-    UnifiedBranching 'Sym m,+    UnifiedBranching 'S m,     ValidFP eb sb,     KnownNat n,     1 <= n,     n ~ (eb + sb)   ) =>-  UnifiedSafeBitCast 'Sym NotRepresentableFPError (SymFP eb sb) (SymWordN n) m+  UnifiedSafeBitCast 'S NotRepresentableFPError (SymFP eb sb) (SymWordN n) m   where-  withBaseSafeBitCast r = withBaseBranching @'Sym @m r+  withBaseSafeBitCast r = withBaseBranching @'S @m r  instance   ( MonadError NotRepresentableFPError m,-    UnifiedBranching 'Sym m,+    UnifiedBranching 'S m,     ValidFP eb sb,     KnownNat n,     1 <= n,     n ~ (eb + sb)   ) =>-  UnifiedSafeBitCast 'Sym NotRepresentableFPError (SymFP eb sb) (SymIntN n) m+  UnifiedSafeBitCast 'S NotRepresentableFPError (SymFP eb sb) (SymIntN n) m   where-  withBaseSafeBitCast r = withBaseBranching @'Sym @m r+  withBaseSafeBitCast r = withBaseBranching @'S @m r

@@ -53,7 +53,7 @@   ( UnifiedBranching (withBaseBranching),   ) import Grisette.Unified.Internal.EvalModeTag-  ( EvalModeTag (Sym),+  ( EvalModeTag (S),   ) import Grisette.Unified.Internal.Util (withMode) @@ -183,10 +183,10 @@     withMode @mode (withBaseBranching @mode @m r) (withBaseBranching @mode @m r)  instance-  (MonadError ArithException m, UnifiedBranching 'Sym m) =>-  UnifiedSafeDiv 'Sym ArithException SymInteger m+  (MonadError ArithException m, UnifiedBranching 'S m) =>+  UnifiedSafeDiv 'S ArithException SymInteger m   where-  withBaseSafeDiv r = withBaseBranching @'Sym @m r+  withBaseSafeDiv r = withBaseBranching @'S @m r  instance   (MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) =>@@ -196,10 +196,10 @@     withMode @mode (withBaseBranching @mode @m r) (withBaseBranching @mode @m r)  instance-  (MonadError ArithException m, UnifiedBranching 'Sym m, KnownNat n, 1 <= n) =>-  UnifiedSafeDiv 'Sym ArithException (SymIntN n) m+  (MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) =>+  UnifiedSafeDiv 'S ArithException (SymIntN n) m   where-  withBaseSafeDiv r = withBaseBranching @'Sym @m r+  withBaseSafeDiv r = withBaseBranching @'S @m r  instance   (MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) =>@@ -209,10 +209,10 @@     withMode @mode (withBaseBranching @mode @m r) (withBaseBranching @mode @m r)  instance-  (MonadError ArithException m, UnifiedBranching 'Sym m, KnownNat n, 1 <= n) =>-  UnifiedSafeDiv 'Sym ArithException (SymWordN n) m+  (MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) =>+  UnifiedSafeDiv 'S ArithException (SymWordN n) m   where-  withBaseSafeDiv r = withBaseBranching @'Sym @m r+  withBaseSafeDiv r = withBaseBranching @'S @m r  instance   ( MonadError (Either SomeBVException ArithException) m,@@ -229,15 +229,15 @@  instance   ( MonadError (Either SomeBVException ArithException) m,-    UnifiedBranching 'Sym m+    UnifiedBranching 'S m   ) =>   UnifiedSafeDiv-    'Sym+    'S     (Either SomeBVException ArithException)     SomeSymIntN     m   where-  withBaseSafeDiv r = withBaseBranching @'Sym @m r+  withBaseSafeDiv r = withBaseBranching @'S @m r  instance   ( MonadError (Either SomeBVException ArithException) m,@@ -254,12 +254,12 @@  instance   ( MonadError (Either SomeBVException ArithException) m,-    UnifiedBranching 'Sym m+    UnifiedBranching 'S m   ) =>   UnifiedSafeDiv-    'Sym+    'S     (Either SomeBVException ArithException)     SomeSymWordN     m   where-  withBaseSafeDiv r = withBaseBranching @'Sym @m r+  withBaseSafeDiv r = withBaseBranching @'S @m r

@@ -36,7 +36,7 @@ import Grisette.Unified.Internal.Class.UnifiedSimpleMergeable   ( UnifiedBranching (withBaseBranching),   )-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Sym))+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (S)) import Grisette.Unified.Internal.Util (withMode)  -- | Unified `Grisette.Internal.Core.Data.Class.SafeFdiv.safeFdiv` operation.@@ -77,7 +77,7 @@     withMode @mode (withBaseBranching @mode @m r) (withBaseBranching @mode @m r)  instance-  (MonadError ArithException m, UnifiedBranching 'Sym m) =>-  UnifiedSafeFdiv 'Sym ArithException SymAlgReal m+  (MonadError ArithException m, UnifiedBranching 'S m) =>+  UnifiedSafeFdiv 'S ArithException SymAlgReal m   where-  withBaseUnifiedSafeFdiv r = withBaseBranching @'Sym @m r+  withBaseUnifiedSafeFdiv r = withBaseBranching @'S @m r

@@ -47,7 +47,7 @@ import Grisette.Unified.Internal.Class.UnifiedSimpleMergeable   ( UnifiedBranching (withBaseBranching),   )-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Sym))+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (S)) import Grisette.Unified.Internal.Util (withMode)  -- | Unified `Grisette.Internal.Core.Data.Class.SafeFromFP.safeFromFP`@@ -150,64 +150,64 @@  instance   ( MonadError NotRepresentableFPError m,-    UnifiedBranching 'Sym m,+    UnifiedBranching 'S m,     ValidFP eb sb   ) =>   UnifiedSafeFromFP-    'Sym+    'S     NotRepresentableFPError     SymInteger     (SymFP eb sb)     SymFPRoundingMode     m   where-  withBaseSafeFromFP r = withBaseBranching @'Sym @m r+  withBaseSafeFromFP r = withBaseBranching @'S @m r  instance   ( MonadError NotRepresentableFPError m,-    UnifiedBranching 'Sym m,+    UnifiedBranching 'S m,     ValidFP eb sb   ) =>   UnifiedSafeFromFP-    'Sym+    'S     NotRepresentableFPError     SymAlgReal     (SymFP eb sb)     SymFPRoundingMode     m   where-  withBaseSafeFromFP r = withBaseBranching @'Sym @m r+  withBaseSafeFromFP r = withBaseBranching @'S @m r  instance   ( MonadError NotRepresentableFPError m,-    UnifiedBranching 'Sym m,+    UnifiedBranching 'S m,     ValidFP eb sb,     KnownNat n,     1 <= n   ) =>   UnifiedSafeFromFP-    'Sym+    'S     NotRepresentableFPError     (SymIntN n)     (SymFP eb sb)     SymFPRoundingMode     m   where-  withBaseSafeFromFP r = withBaseBranching @'Sym @m r+  withBaseSafeFromFP r = withBaseBranching @'S @m r  instance   ( MonadError NotRepresentableFPError m,-    UnifiedBranching 'Sym m,+    UnifiedBranching 'S m,     ValidFP eb sb,     KnownNat n,     1 <= n   ) =>   UnifiedSafeFromFP-    'Sym+    'S     NotRepresentableFPError     (SymWordN n)     (SymFP eb sb)     SymFPRoundingMode     m   where-  withBaseSafeFromFP r = withBaseBranching @'Sym @m r+  withBaseSafeFromFP r = withBaseBranching @'S @m r

@@ -51,7 +51,7 @@   ( UnifiedBranching (withBaseBranching),   ) import Grisette.Unified.Internal.EvalModeTag-  ( EvalModeTag (Sym),+  ( EvalModeTag (S),   ) import Grisette.Unified.Internal.Util (withMode) @@ -135,10 +135,10 @@     withMode @mode (withBaseBranching @mode @m r) (withBaseBranching @mode @m r)  instance-  (MonadError ArithException m, UnifiedBranching 'Sym m) =>-  UnifiedSafeLinearArith 'Sym ArithException SymInteger m+  (MonadError ArithException m, UnifiedBranching 'S m) =>+  UnifiedSafeLinearArith 'S ArithException SymInteger m   where-  withBaseSafeLinearArith r = withBaseBranching @'Sym @m r+  withBaseSafeLinearArith r = withBaseBranching @'S @m r  instance   (MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) =>@@ -148,10 +148,10 @@     withMode @mode (withBaseBranching @mode @m r) (withBaseBranching @mode @m r)  instance-  (MonadError ArithException m, UnifiedBranching 'Sym m, KnownNat n, 1 <= n) =>-  UnifiedSafeLinearArith 'Sym ArithException (SymIntN n) m+  (MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) =>+  UnifiedSafeLinearArith 'S ArithException (SymIntN n) m   where-  withBaseSafeLinearArith r = withBaseBranching @'Sym @m r+  withBaseSafeLinearArith r = withBaseBranching @'S @m r  instance   (MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) =>@@ -161,10 +161,10 @@     withMode @mode (withBaseBranching @mode @m r) (withBaseBranching @mode @m r)  instance-  (MonadError ArithException m, UnifiedBranching 'Sym m, KnownNat n, 1 <= n) =>-  UnifiedSafeLinearArith 'Sym ArithException (SymWordN n) m+  (MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) =>+  UnifiedSafeLinearArith 'S ArithException (SymWordN n) m   where-  withBaseSafeLinearArith r = withBaseBranching @'Sym @m r+  withBaseSafeLinearArith r = withBaseBranching @'S @m r  instance   ( MonadError (Either SomeBVException ArithException) m,@@ -181,15 +181,15 @@  instance   ( MonadError (Either SomeBVException ArithException) m,-    UnifiedBranching 'Sym m+    UnifiedBranching 'S m   ) =>   UnifiedSafeLinearArith-    'Sym+    'S     (Either SomeBVException ArithException)     SomeSymIntN     m   where-  withBaseSafeLinearArith r = withBaseBranching @'Sym @m r+  withBaseSafeLinearArith r = withBaseBranching @'S @m r  instance   ( MonadError (Either SomeBVException ArithException) m,@@ -206,12 +206,12 @@  instance   ( MonadError (Either SomeBVException ArithException) m,-    UnifiedBranching 'Sym m+    UnifiedBranching 'S m   ) =>   UnifiedSafeLinearArith-    'Sym+    'S     (Either SomeBVException ArithException)     SomeSymWordN     m   where-  withBaseSafeLinearArith r = withBaseBranching @'Sym @m r+  withBaseSafeLinearArith r = withBaseBranching @'S @m r

@@ -46,7 +46,7 @@   ( UnifiedBranching (withBaseBranching),   ) import Grisette.Unified.Internal.EvalModeTag-  ( EvalModeTag (Sym),+  ( EvalModeTag (S),   ) import Grisette.Unified.Internal.Util (withMode) @@ -111,10 +111,10 @@     withMode @mode (withBaseBranching @mode @m r) (withBaseBranching @mode @m r)  instance-  (MonadError ArithException m, UnifiedBranching 'Sym m, KnownNat n, 1 <= n) =>-  UnifiedSafeSymRotate 'Sym ArithException (SymIntN n) m+  (MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) =>+  UnifiedSafeSymRotate 'S ArithException (SymIntN n) m   where-  withBaseSafeSymRotate r = withBaseBranching @'Sym @m r+  withBaseSafeSymRotate r = withBaseBranching @'S @m r  instance   (MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) =>@@ -124,10 +124,10 @@     withMode @mode (withBaseBranching @mode @m r) (withBaseBranching @mode @m r)  instance-  (MonadError ArithException m, UnifiedBranching 'Sym m, KnownNat n, 1 <= n) =>-  UnifiedSafeSymRotate 'Sym ArithException (SymWordN n) m+  (MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) =>+  UnifiedSafeSymRotate 'S ArithException (SymWordN n) m   where-  withBaseSafeSymRotate r = withBaseBranching @'Sym @m r+  withBaseSafeSymRotate r = withBaseBranching @'S @m r  instance   ( MonadError (Either SomeBVException ArithException) m,@@ -144,15 +144,15 @@  instance   ( MonadError (Either SomeBVException ArithException) m,-    UnifiedBranching 'Sym m+    UnifiedBranching 'S m   ) =>   UnifiedSafeSymRotate-    'Sym+    'S     (Either SomeBVException ArithException)     SomeSymIntN     m   where-  withBaseSafeSymRotate r = withBaseBranching @'Sym @m r+  withBaseSafeSymRotate r = withBaseBranching @'S @m r  instance   ( MonadError (Either SomeBVException ArithException) m,@@ -169,12 +169,12 @@  instance   ( MonadError (Either SomeBVException ArithException) m,-    UnifiedBranching 'Sym m+    UnifiedBranching 'S m   ) =>   UnifiedSafeSymRotate-    'Sym+    'S     (Either SomeBVException ArithException)     SomeSymWordN     m   where-  withBaseSafeSymRotate r = withBaseBranching @'Sym @m r+  withBaseSafeSymRotate r = withBaseBranching @'S @m r

@@ -48,7 +48,7 @@   ( UnifiedBranching (withBaseBranching),   ) import Grisette.Unified.Internal.EvalModeTag-  ( EvalModeTag (Sym),+  ( EvalModeTag (S),   ) import Grisette.Unified.Internal.Util (withMode) @@ -155,10 +155,10 @@     withMode @mode (withBaseBranching @mode @m r) (withBaseBranching @mode @m r)  instance-  (MonadError ArithException m, UnifiedBranching 'Sym m, KnownNat n, 1 <= n) =>-  UnifiedSafeSymShift 'Sym ArithException (SymIntN n) m+  (MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) =>+  UnifiedSafeSymShift 'S ArithException (SymIntN n) m   where-  withBaseSafeSymShift r = withBaseBranching @'Sym @m r+  withBaseSafeSymShift r = withBaseBranching @'S @m r  instance   (MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) =>@@ -168,10 +168,10 @@     withMode @mode (withBaseBranching @mode @m r) (withBaseBranching @mode @m r)  instance-  (MonadError ArithException m, UnifiedBranching 'Sym m, KnownNat n, 1 <= n) =>-  UnifiedSafeSymShift 'Sym ArithException (SymWordN n) m+  (MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) =>+  UnifiedSafeSymShift 'S ArithException (SymWordN n) m   where-  withBaseSafeSymShift r = withBaseBranching @'Sym @m r+  withBaseSafeSymShift r = withBaseBranching @'S @m r  instance   ( MonadError (Either SomeBVException ArithException) m,@@ -188,15 +188,15 @@  instance   ( MonadError (Either SomeBVException ArithException) m,-    UnifiedBranching 'Sym m+    UnifiedBranching 'S m   ) =>   UnifiedSafeSymShift-    'Sym+    'S     (Either SomeBVException ArithException)     SomeSymIntN     m   where-  withBaseSafeSymShift r = withBaseBranching @'Sym @m r+  withBaseSafeSymShift r = withBaseBranching @'S @m r  instance   ( MonadError (Either SomeBVException ArithException) m,@@ -213,12 +213,12 @@  instance   ( MonadError (Either SomeBVException ArithException) m,-    UnifiedBranching 'Sym m+    UnifiedBranching 'S m   ) =>   UnifiedSafeSymShift-    'Sym+    'S     (Either SomeBVException ArithException)     SomeSymWordN     m   where-  withBaseSafeSymShift r = withBaseBranching @'Sym @m r+  withBaseSafeSymShift r = withBaseBranching @'S @m r

@@ -0,0 +1,136 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}++-- |+-- Module      :   Grisette.Unified.Internal.Class.UnifiedSolvable+-- Copyright   :   (c) Sirui Lu 2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Unified.Internal.Class.UnifiedSolvable+  ( UnifiedSolvable (withBaseSolvable),+    con,+    pattern Con,+    conView,+  )+where++import Data.Type.Bool (If)+import Data.Typeable (Typeable)+import GHC.TypeLits (KnownNat, type (<=))+import Grisette.Internal.Core.Data.Class.Solvable (Solvable)+import qualified Grisette.Internal.Core.Data.Class.Solvable as Grisette+import Grisette.Internal.SymPrim.AlgReal (AlgReal)+import Grisette.Internal.SymPrim.BV (IntN, WordN)+import Grisette.Internal.SymPrim.FP (FP, ValidFP)+import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal)+import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)+import Grisette.Internal.SymPrim.SymBool (SymBool)+import Grisette.Internal.SymPrim.SymFP (SymFP)+import Grisette.Internal.SymPrim.SymInteger (SymInteger)+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S), IsConMode)+import Grisette.Unified.Internal.Util (withMode)++-- $setup+-- >>> import Grisette.Core (ssym)++-- | Wrap a concrete value in a symbolic value.+--+-- >>> con True :: Bool+-- True+--+-- >>> con True :: SymBool+-- true+con ::+  forall mode a con. (Typeable mode, UnifiedSolvable mode a con) => con -> a+con v =+  withMode @mode+    (withBaseSolvable @mode @a @con v)+    (withBaseSolvable @mode @a @con $ Grisette.con v)++-- | Extract the concrete value from a symbolic value.+--+-- >>> conView (con True :: SymBool)+-- Just True+--+-- >>> conView (ssym "a" :: SymBool)+-- Nothing+--+-- >>> conView True+-- Just True+conView ::+  forall mode a con.+  (Typeable mode, UnifiedSolvable mode a con) =>+  a ->+  Maybe con+conView v =+  withMode @mode+    (withBaseSolvable @mode @a @con $ Just v)+    (withBaseSolvable @mode @a @con $ Grisette.conView v)++-- | A pattern synonym for extracting the concrete value from a symbolic value.+--+-- >>> case con True :: SymBool of Con v -> v+-- True+--+-- >>> case ssym "a" :: SymBool of Con v -> Just v; _ -> Nothing+-- Nothing+pattern Con :: (Typeable mode, UnifiedSolvable mode a con) => con -> a+pattern Con v <-+  (conView -> Just v)+  where+    Con v = con v++-- | A class that provides the ability to extract/wrap the concrete value+-- from/into a symbolic value.+class UnifiedSolvable mode a con | a -> mode con, con mode -> a where+  withBaseSolvable ::+    ((If (IsConMode mode) (a ~ con) (Solvable con a)) => r) -> r++instance UnifiedSolvable 'C Bool Bool where+  withBaseSolvable r = r++instance UnifiedSolvable 'S SymBool Bool where+  withBaseSolvable r = r++instance UnifiedSolvable 'C Integer Integer where+  withBaseSolvable r = r++instance UnifiedSolvable 'S SymInteger Integer where+  withBaseSolvable r = r++instance UnifiedSolvable 'C AlgReal AlgReal where+  withBaseSolvable r = r++instance UnifiedSolvable 'S SymAlgReal AlgReal where+  withBaseSolvable r = r++instance (KnownNat n, 1 <= n) => UnifiedSolvable 'C (WordN n) (WordN n) where+  withBaseSolvable r = r++instance (KnownNat n, 1 <= n) => UnifiedSolvable 'S (SymWordN n) (WordN n) where+  withBaseSolvable r = r++instance (KnownNat n, 1 <= n) => UnifiedSolvable 'C (IntN n) (IntN n) where+  withBaseSolvable r = r++instance (KnownNat n, 1 <= n) => UnifiedSolvable 'S (SymIntN n) (IntN n) where+  withBaseSolvable r = r++instance (ValidFP eb sb) => UnifiedSolvable 'C (FP eb sb) (FP eb sb) where+  withBaseSolvable r = r++instance (ValidFP eb sb) => UnifiedSolvable 'S (SymFP eb sb) (FP eb sb) where+  withBaseSolvable r = r

@@ -65,7 +65,7 @@   ( deriveFunctorArgUnifiedInterfaces,     deriveUnifiedInterface1s,   )-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Sym), IsConMode)+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (S), IsConMode) import Grisette.Unified.Internal.UnifiedBool (UnifiedBool (GetBool)) import Grisette.Unified.Internal.Util (withMode) @@ -246,8 +246,8 @@   withBaseSymEq2 r = r   {-# INLINE withBaseSymEq2 #-} -instance (UnifiedSymEq 'Sym v) => UnifiedSymEq 'Sym (Union v) where-  withBaseSymEq r = withBaseSymEq @'Sym @v r+instance (UnifiedSymEq 'S v) => UnifiedSymEq 'S (Union v) where+  withBaseSymEq r = withBaseSymEq @'S @v r   {-# INLINE withBaseSymEq #-}  instance

@@ -86,7 +86,7 @@   ( UnifiedBranching (withBaseBranching),   ) import Grisette.Unified.Internal.EvalModeTag-  ( EvalModeTag (Sym),+  ( EvalModeTag (S),     IsConMode,   ) import Grisette.Unified.Internal.UnifiedBool (UnifiedBool (GetBool))@@ -375,8 +375,8 @@   withBaseSymOrd2 r = r   {-# INLINE withBaseSymOrd2 #-} -instance (UnifiedSymOrd 'Sym v) => UnifiedSymOrd 'Sym (Union v) where-  withBaseSymOrd r = withBaseSymOrd @'Sym @v r+instance (UnifiedSymOrd 'S v) => UnifiedSymOrd 'S (Union v) where+  withBaseSymOrd r = withBaseSymOrd @'S @v r   {-# INLINE withBaseSymOrd #-}  instance

@@ -39,7 +39,7 @@ import Grisette.Unified.Internal.BVFPConversion (AllUnifiedBVFPConversion) import Grisette.Unified.Internal.BaseMonad (BaseMonad) import Grisette.Unified.Internal.Class.UnifiedSimpleMergeable (UnifiedBranching)-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Con, Sym))+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S)) import Grisette.Unified.Internal.FPFPConversion (AllUnifiedFPFPConversion) import Grisette.Unified.Internal.Theories   ( TheoryToUnify (UAlgReal, UFP, UFun, UIntN, UInteger, UWordN),@@ -48,7 +48,6 @@ import Grisette.Unified.Internal.UnifiedAlgReal (UnifiedAlgReal) import Grisette.Unified.Internal.UnifiedBV (AllUnifiedBV) import Grisette.Unified.Internal.UnifiedBool (UnifiedBool (GetBool))-import Grisette.Unified.Internal.UnifiedConstraint (UnifiedPrimitive) import Grisette.Unified.Internal.UnifiedData (AllUnifiedData) import Grisette.Unified.Internal.UnifiedFP (AllUnifiedFP) import Grisette.Unified.Internal.UnifiedFun@@ -56,6 +55,7 @@     unifiedFunInstanceName,   ) import Grisette.Unified.Internal.UnifiedInteger (UnifiedInteger)+import Grisette.Unified.Internal.UnifiedPrim (UnifiedBasicPrim) import Language.Haskell.TH   ( DecsQ,     Type (AppT, ArrowT, ConT, StarT, VarT),@@ -78,7 +78,7 @@ class   ( Typeable mode,     UnifiedBool mode,-    UnifiedPrimitive mode (GetBool mode),+    UnifiedBasicPrim mode (GetBool mode),     Monad (BaseMonad mode),     TryMerge (BaseMonad mode),     UnifiedBranching mode (BaseMonad mode),@@ -86,9 +86,9 @@   ) =>   EvalModeBase mode -instance EvalModeBase 'Con+instance EvalModeBase 'C -instance EvalModeBase 'Sym+instance EvalModeBase 'S  -- | Provide the support for 'Grisette.Unified.GetIntN', -- 'Grisette.Unified.GetWordN', 'Grisette.Unified.GetSomeIntN', and@@ -97,9 +97,9 @@ -- For compilers prior to GHC 9.2.1, see the notes for 'EvalModeAll'. class (AllUnifiedBV mode, AllUnifiedBVBVConversion mode) => EvalModeBV mode -instance EvalModeBV 'Con+instance EvalModeBV 'C -instance EvalModeBV 'Sym+instance EvalModeBV 'S  -- | Provide the support for 'Grisette.Unified.GetInteger'. --@@ -117,9 +117,9 @@   ) =>   EvalModeFP mode -instance EvalModeFP 'Con+instance EvalModeFP 'C -instance EvalModeFP 'Sym+instance EvalModeFP 'S  -- | Provide the support for 'Grisette.Unified.GetAlgReal'. --@@ -172,9 +172,9 @@   ) =>   EvalModeAll mode -instance EvalModeAll 'Con+instance EvalModeAll 'C -instance EvalModeAll 'Sym+instance EvalModeAll 'S  -- | A constraint that specifies that the mode is valid, and provide all the -- corresponding constraints for the operations for the types.@@ -262,8 +262,8 @@       [kindedTV modeName (ConT ''EvalModeTag)]       []       []-  rc <- instanceD (return []) (appT (conT $ mkName nm) (promotedT 'Con)) []-  rs <- instanceD (return []) (appT (conT $ mkName nm) (promotedT 'Sym)) []+  rc <- instanceD (return []) (appT (conT $ mkName nm) (promotedT 'C)) []+  rs <- instanceD (return []) (appT (conT $ mkName nm) (promotedT 'S)) []   m <- newName "m"   let mType = varT m   monad <-

@@ -19,11 +19,11 @@  import Language.Haskell.TH.Syntax (Lift) --- | Evaluation mode for unified types. 'Con' means concrete evaluation, 'Sym'+-- | Evaluation mode for unified types. 'C' means concrete evaluation, 'S' -- means symbolic evaluation.-data EvalModeTag = Con | Sym deriving (Lift)+data EvalModeTag = C | S deriving (Lift) --- | Type family to check if a mode is 'Con'.+-- | Type family to check if a mode is 'C'. type family IsConMode (mode :: EvalModeTag) = (r :: Bool) | r -> mode where-  IsConMode 'Con = 'True-  IsConMode 'Sym = 'False+  IsConMode 'C = 'True+  IsConMode 'S = 'False

@@ -25,7 +25,7 @@ import Grisette.Internal.Core.Data.Class.IEEEFP (IEEEFPConvertible) import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP) import Grisette.Internal.SymPrim.SymFP (SymFP, SymFPRoundingMode)-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Con, Sym))+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S)) import Grisette.Unified.Internal.UnifiedFP (UnifiedFPImpl (GetFP, GetFPRoundingMode))  class@@ -47,7 +47,7 @@ instance   (ValidFP eb0 sb0, ValidFP eb1 sb1) =>   UnifiedFPFPConversionImpl-    'Con+    'C     FP     eb0     sb0@@ -60,7 +60,7 @@ instance   (ValidFP eb0 sb0, ValidFP eb1 sb1) =>   UnifiedFPFPConversionImpl-    'Sym+    'S     SymFP     eb0     sb0

@@ -26,51 +26,55 @@ import Grisette.Internal.Core.Data.Class.SafeFdiv (FdivOr) import Grisette.Internal.SymPrim.AlgReal (AlgReal) import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal)-import Grisette.Unified.Internal.BaseConstraint-  ( BasicGrisetteType,-    ConSymConversion,-  )+import Grisette.Internal.SymPrim.SymPrim (Prim) import Grisette.Unified.Internal.Class.UnifiedFromIntegral (UnifiedFromIntegral)+import Grisette.Unified.Internal.Class.UnifiedRep+  ( UnifiedConRep (ConType),+    UnifiedSymRep (SymType),+  ) import Grisette.Unified.Internal.Class.UnifiedSafeFdiv (UnifiedSafeFdiv) import Grisette.Unified.Internal.Class.UnifiedSimpleMergeable (UnifiedBranching)-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Con, Sym))-import Grisette.Unified.Internal.UnifiedConstraint (UnifiedPrimitive)+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S)) import Grisette.Unified.Internal.UnifiedInteger (GetInteger)+import Grisette.Unified.Internal.UnifiedPrim (UnifiedBasicPrim)  class-  ( BasicGrisetteType (GetAlgReal mode),-    ConSymConversion AlgReal SymAlgReal (GetAlgReal mode),-    Num (GetAlgReal mode),-    Fractional (GetAlgReal mode),-    UnifiedPrimitive mode (GetAlgReal mode),-    FdivOr (GetAlgReal mode),+  ( r ~ GetAlgReal mode,+    UnifiedConRep r,+    UnifiedSymRep r,+    ConType r ~ AlgReal,+    SymType r ~ SymAlgReal,+    UnifiedBasicPrim mode r,+    Prim r,+    Num r,+    Fractional r,+    FdivOr r,     forall m.     (UnifiedBranching mode m, MonadError ArithException m) =>     UnifiedSafeFdiv mode ArithException r m,-    UnifiedFromIntegral mode (GetInteger mode) r,-    r ~ GetAlgReal mode+    UnifiedFromIntegral mode (GetInteger mode) r   ) =>   UnifiedAlgRealImpl (mode :: EvalModeTag) r     | mode -> r   where-  -- | Get a unified algebraic real type. Resolves to 'AlgReal' in 'Con' mode,-  -- and 'SymAlgReal' in 'Sym' mode.+  -- | Get a unified algebraic real type. Resolves to 'AlgReal' in 'C' mode,+  -- and 'SymAlgReal' in 'S' mode.   --   -- 'Floating', 'Grisette.LogBaseOr' and 'Grisette.SafeLogBase' for   -- 'SymAlgReal' are not provided as they are not available for 'AlgReal'.   type GetAlgReal mode = real | real -> mode -instance UnifiedAlgRealImpl 'Con AlgReal where-  type GetAlgReal 'Con = AlgReal+instance UnifiedAlgRealImpl 'C AlgReal where+  type GetAlgReal 'C = AlgReal -instance UnifiedAlgRealImpl 'Sym SymAlgReal where-  type GetAlgReal 'Sym = SymAlgReal+instance UnifiedAlgRealImpl 'S SymAlgReal where+  type GetAlgReal 'S = SymAlgReal  -- | Evaluation mode with unified 'AlgReal' type. class   (UnifiedAlgRealImpl mode (GetAlgReal mode)) =>   UnifiedAlgReal (mode :: EvalModeTag) -instance UnifiedAlgReal 'Con+instance UnifiedAlgReal 'C -instance UnifiedAlgReal 'Sym+instance UnifiedAlgReal 'S

@@ -56,15 +56,15 @@     SomeWordN,   ) import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)-import Grisette.Unified.Internal.BaseConstraint-  ( BasicGrisetteType,-    ConSymConversion,-  )+import Grisette.Unified.Internal.BaseConstraint (ConSymConversion) import Grisette.Unified.Internal.Class.UnifiedFiniteBits   ( UnifiedFiniteBits,   ) import Grisette.Unified.Internal.Class.UnifiedFromIntegral (UnifiedFromIntegral)-import Grisette.Unified.Internal.Class.UnifiedITEOp (UnifiedITEOp)+import Grisette.Unified.Internal.Class.UnifiedRep+  ( UnifiedConRep (ConType),+    UnifiedSymRep (SymType),+  ) import Grisette.Unified.Internal.Class.UnifiedSafeDiv (UnifiedSafeDiv) import Grisette.Unified.Internal.Class.UnifiedSafeLinearArith   ( UnifiedSafeLinearArith,@@ -75,18 +75,14 @@ import Grisette.Unified.Internal.Class.UnifiedSafeSymShift (UnifiedSafeSymShift) import Grisette.Unified.Internal.Class.UnifiedSimpleMergeable   ( UnifiedBranching,-    UnifiedSimpleMergeable,   )-import Grisette.Unified.Internal.Class.UnifiedSymEq (UnifiedSymEq)-import Grisette.Unified.Internal.Class.UnifiedSymOrd (UnifiedSymOrd)-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Con, Sym))+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S)) import Grisette.Unified.Internal.UnifiedAlgReal (GetAlgReal) import Grisette.Unified.Internal.UnifiedInteger (GetInteger)+import Grisette.Unified.Internal.UnifiedPrim (UnifiedBasicPrim, UnifiedPrim)  type BVConstraint mode word int =-  ( BasicGrisetteType word,-    BasicGrisetteType int,-    Num word,+  ( Num word,     Num int,     Bits word,     Bits int,@@ -96,12 +92,6 @@     SymShift int,     SymRotate word,     SymRotate int,-    UnifiedSymEq mode word,-    UnifiedSymEq mode int,-    UnifiedSymOrd mode word,-    UnifiedSymOrd mode int,-    UnifiedITEOp mode word,-    UnifiedITEOp mode int,     SignConversion word int,     UnifiedFiniteBits mode word,     UnifiedFiniteBits mode int@@ -109,7 +99,9 @@     Constraint  type SomeBVPair mode word int =-  ( BVConstraint mode word int,+  ( UnifiedPrim mode word,+    UnifiedPrim mode int,+    BVConstraint mode word int,     BV word,     BV int,     DivOr word,@@ -121,11 +113,15 @@  -- | Implementation for 'UnifiedBV'. class-  ( BVConstraint mode (GetWordN mode n) (GetIntN mode n),-    ConSymConversion (WordN n) (SymWordN n) (GetWordN mode n),-    UnifiedSimpleMergeable mode (GetWordN mode n),-    ConSymConversion (IntN n) (SymIntN n) (GetIntN mode n),-    UnifiedSimpleMergeable mode (GetIntN mode n),+  ( UnifiedConRep word,+    UnifiedSymRep int,+    ConType word ~ WordN n,+    SymType word ~ SymWordN n,+    ConType int ~ IntN n,+    SymType int ~ SymIntN n,+    UnifiedBasicPrim mode word,+    UnifiedBasicPrim mode int,+    BVConstraint mode word int,     wordn ~ GetWordN mode,     intn ~ GetIntN mode,     word ~ wordn n,@@ -150,34 +146,34 @@       int -> intn n   where   -- | Get a unified unsigned size-tagged bit vector type. Resolves to 'WordN'-  -- in 'Con' mode, and 'SymWordN' in 'Sym' mode.+  -- in 'C' mode, and 'SymWordN' in 'S' mode.   type GetWordN mode = (w :: Nat -> Type) | w -> mode    -- | Get a unified signed size-tagged bit vector type. Resolves to 'IntN'-  -- in 'Con' mode, and 'SymIntN' in 'Sym' mode.+  -- in 'C' mode, and 'SymIntN' in 'S' mode.   type GetIntN mode = (i :: Nat -> Type) | i -> mode  instance   (KnownNat n, 1 <= n) =>-  UnifiedBVImpl 'Con WordN IntN n (WordN n) (IntN n)+  UnifiedBVImpl 'C WordN IntN n (WordN n) (IntN n)   where-  type GetWordN 'Con = WordN-  type GetIntN 'Con = IntN+  type GetWordN 'C = WordN+  type GetIntN 'C = IntN  instance   (KnownNat n, 1 <= n) =>-  UnifiedBVImpl 'Sym SymWordN SymIntN n (SymWordN n) (SymIntN n)+  UnifiedBVImpl 'S SymWordN SymIntN n (SymWordN n) (SymIntN n)   where-  type GetWordN 'Sym = SymWordN-  type GetIntN 'Sym = SymIntN+  type GetWordN 'S = SymWordN+  type GetIntN 'S = SymIntN  -- | Get a unified unsigned dynamic bit width bit vector type. Resolves to--- 'SomeWordN' in 'Con' mode, and 'SomeSymWordN' in 'Sym' mode.+-- 'SomeWordN' in 'C' mode, and 'SomeSymWordN' in 'S' mode. type family GetSomeWordN mode = sw | sw -> mode where   GetSomeWordN mode = SomeBV (GetWordN mode)  -- | Get a unified signed dynamic bit width bit vector type. Resolves to--- 'SomeIntN' in 'Con' mode, and 'SomeSymIntN' in 'Sym' mode.+-- 'SomeIntN' in 'C' mode, and 'SomeSymIntN' in 'S' mode. type family GetSomeIntN mode = sw | sw -> mode where   GetSomeIntN mode = SomeBV (GetIntN mode) 

@@ -1,6 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeFamilyDependencies #-}+{-# LANGUAGE TypeOperators #-}  -- | -- Module      :   Grisette.Unified.Internal.UnifiedBool@@ -14,26 +15,34 @@  import Grisette.Internal.Core.Data.Class.LogicalOp (LogicalOp) import Grisette.Internal.SymPrim.SymBool (SymBool)+import Grisette.Internal.SymPrim.SymPrim (Prim) import Grisette.Unified.Internal.BaseConstraint-  ( BasicGrisetteType,-    ConSymConversion,+  ( ConSymConversion,   )-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Con, Sym))+import Grisette.Unified.Internal.Class.UnifiedRep+  ( UnifiedConRep (ConType),+    UnifiedSymRep (SymType),+  )+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S))  -- | Evaluation mode with unified 'Bool' type. class-  ( BasicGrisetteType (GetBool mode),+  ( Prim (GetBool mode),+    UnifiedConRep (GetBool mode),+    UnifiedSymRep (GetBool mode),+    ConType (GetBool mode) ~ Bool,+    SymType (GetBool mode) ~ SymBool,     ConSymConversion Bool SymBool (GetBool mode),     LogicalOp (GetBool mode)   ) =>   UnifiedBool (mode :: EvalModeTag)   where-  -- | Get a unified Boolean type. Resolves to 'Bool' in 'Con' mode, and-  -- 'SymBool' in 'Sym' mode.+  -- | Get a unified Boolean type. Resolves to 'Bool' in 'C' mode, and+  -- 'SymBool' in 'S' mode.   type GetBool mode = bool | bool -> mode -instance UnifiedBool 'Con where-  type GetBool 'Con = Bool+instance UnifiedBool 'C where+  type GetBool 'C = Bool -instance UnifiedBool 'Sym where-  type GetBool 'Sym = SymBool+instance UnifiedBool 'S where+  type GetBool 'S = SymBool

@@ -1,27 +0,0 @@-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE MonoLocalBinds #-}---- |--- Module      :   Grisette.Unified.Internal.UnifiedConstraint--- Copyright   :   (c) Sirui Lu 2024--- License     :   BSD-3-Clause (see the LICENSE file)------ Maintainer  :   siruilu@cs.washington.edu--- Stability   :   Experimental--- Portability :   GHC only-module Grisette.Unified.Internal.UnifiedConstraint (UnifiedPrimitive) where--import Grisette.Unified.Internal.Class.UnifiedITEOp (UnifiedITEOp)-import Grisette.Unified.Internal.Class.UnifiedSimpleMergeable-  ( UnifiedSimpleMergeable,-  )-import Grisette.Unified.Internal.Class.UnifiedSymEq (UnifiedSymEq)-import Grisette.Unified.Internal.Class.UnifiedSymOrd (UnifiedSymOrd)---- | Basic constraints for a unified primitive type.-type UnifiedPrimitive mode t =-  ( UnifiedITEOp mode t,-    UnifiedSymEq mode t,-    UnifiedSymOrd mode t,-    UnifiedSimpleMergeable mode t-  )

@@ -54,7 +54,7 @@   ) import Grisette.Unified.Internal.Class.UnifiedSymEq (UnifiedSymEq) import Grisette.Unified.Internal.Class.UnifiedSymOrd (UnifiedSymOrd)-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Con, Sym))+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S)) import Instances.TH.Lift () import Language.Haskell.TH.Syntax (Lift) @@ -87,8 +87,8 @@   UnifiedDataImpl (mode :: EvalModeTag) v u     | u -> mode v   where-  -- | Get a unified data type. Resolves to @v@ in 'Con' mode, and @'Union' v@-  -- in 'Sym' mode.+  -- | Get a unified data type. Resolves to @v@ in 'C' mode, and @'Union' v@+  -- in 'S' mode.   type GetData mode v = r | r -> mode v    -- | Wraps a value into the unified data type.@@ -97,18 +97,18 @@   -- | Extracts a value from the unified data type.   extractData :: (Monad m, UnifiedBranching mode m) => u -> m v -instance (Mergeable v) => UnifiedDataImpl 'Con v (Identity v) where-  type GetData 'Con v = Identity v+instance (Mergeable v) => UnifiedDataImpl 'C v (Identity v) where+  type GetData 'C v = Identity v   wrapData = Identity   extractData ::-    forall m. (Mergeable v, Monad m, UnifiedBranching Con m) => Identity v -> m v-  extractData = withBaseBranching @'Con @m $ mrgSingle . runIdentity+    forall m. (Mergeable v, Monad m, UnifiedBranching C m) => Identity v -> m v+  extractData = withBaseBranching @'C @m $ mrgSingle . runIdentity -instance (Mergeable v) => UnifiedDataImpl 'Sym v (Union v) where-  type GetData 'Sym v = Union v+instance (Mergeable v) => UnifiedDataImpl 'S v (Union v) where+  type GetData 'S v = Union v   wrapData = mrgSingle   extractData ::-    forall m. (Mergeable v, Monad m, UnifiedBranching Sym m) => Union v -> m v+    forall m. (Mergeable v, Monad m, UnifiedBranching S m) => Union v -> m v   extractData = liftBaseMonad  -- | This class is needed as constraint in user code prior to GHC 9.2.1.@@ -118,7 +118,7 @@ instance (UnifiedDataImpl bool v (GetData bool v)) => UnifiedData bool v  class-  (UnifiedSimpleMergeable 'Sym (GetData 'Sym v)) =>+  (UnifiedSimpleMergeable 'S (GetData 'S v)) =>   UnifiedDataSimpleMergeable v  instance (Mergeable v) => UnifiedDataSimpleMergeable v

@@ -39,23 +39,22 @@ import Grisette.Internal.Core.Data.Class.SymIEEEFP (SymIEEEFPTraits) import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, NotRepresentableFPError, ValidFP) import Grisette.Internal.SymPrim.SymFP (SymFP, SymFPRoundingMode)-import Grisette.Unified.Internal.BaseConstraint-  ( BasicGrisetteType,-    ConSymConversion,-  ) import Grisette.Unified.Internal.Class.UnifiedFromIntegral (UnifiedFromIntegral)+import Grisette.Unified.Internal.Class.UnifiedRep (UnifiedConRep (ConType), UnifiedSymRep (SymType)) import Grisette.Unified.Internal.Class.UnifiedSafeFromFP (UnifiedSafeFromFP) import Grisette.Unified.Internal.Class.UnifiedSimpleMergeable (UnifiedBranching)-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Con, Sym))+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S)) import Grisette.Unified.Internal.UnifiedAlgReal (GetAlgReal)-import Grisette.Unified.Internal.UnifiedConstraint (UnifiedPrimitive) import Grisette.Unified.Internal.UnifiedInteger (GetInteger)+import Grisette.Unified.Internal.UnifiedPrim (UnifiedBasicPrim)  -- | Implementation for 'UnifiedFP'. class-  ( BasicGrisetteType fp,-    ConSymConversion (FP eb sb) (SymFP eb sb) fp,-    UnifiedPrimitive mode fp,+  ( UnifiedConRep fp,+    UnifiedSymRep fp,+    ConType fp ~ FP eb sb,+    SymType fp ~ SymFP eb sb,+    UnifiedBasicPrim mode fp,     Floating fp,     SymIEEEFPTraits fp,     IEEEFPConstants fp,@@ -74,27 +73,27 @@       rd -> fpn,       rd eb sb -> fp   where-  -- | Get a unified floating point type. Resolves to 'FP' in 'Con' mode, and-  -- 'SymFP' in 'Sym' mode.+  -- | Get a unified floating point type. Resolves to 'FP' in 'C' mode, and+  -- 'SymFP' in 'S' mode.   type GetFP mode = (f :: Nat -> Nat -> Type) | f -> mode    -- | Get a unified floating point rounding mode type. Resolves to-  -- 'FPRoundingMode' in 'Con' mode, and 'SymFPRoundingMode' in 'Sym' mode.+  -- 'FPRoundingMode' in 'C' mode, and 'SymFPRoundingMode' in 'S' mode.   type GetFPRoundingMode mode = r | r -> mode  instance   (ValidFP eb sb) =>-  UnifiedFPImpl 'Con FP eb sb (FP eb sb) FPRoundingMode+  UnifiedFPImpl 'C FP eb sb (FP eb sb) FPRoundingMode   where-  type GetFP 'Con = FP-  type GetFPRoundingMode 'Con = FPRoundingMode+  type GetFP 'C = FP+  type GetFPRoundingMode 'C = FPRoundingMode  instance   (ValidFP eb sb) =>-  UnifiedFPImpl 'Sym SymFP eb sb (SymFP eb sb) SymFPRoundingMode+  UnifiedFPImpl 'S SymFP eb sb (SymFP eb sb) SymFPRoundingMode   where-  type GetFP 'Sym = SymFP-  type GetFPRoundingMode 'Sym = SymFPRoundingMode+  type GetFP 'S = SymFP+  type GetFPRoundingMode 'S = SymFPRoundingMode  -- | Evaluation mode with unified 'FP' type. class

@@ -60,7 +60,7 @@ import Grisette.Internal.SymPrim.SymInteger (SymInteger) import Grisette.Internal.SymPrim.SymTabularFun (type (=~>)) import Grisette.Internal.SymPrim.TabularFun (type (=->))-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Con, Sym))+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S)) import Grisette.Unified.Internal.Theories   ( TheoryToUnify (UAlgReal, UBool, UFP, UFun, UIntN, UInteger, UWordN),   )@@ -103,17 +103,17 @@  -- | Provide unified function types. class UnifiedFun (mode :: EvalModeTag) where-  -- | Get a unified function type. Resolves to t'Grisette.SymPrim.=->' in 'Con'-  -- mode, and t'Grisette.SymPrim.=~>' in 'Sym' mode.+  -- | Get a unified function type. Resolves to t'Grisette.SymPrim.=->' in 'C'+  -- mode, and t'Grisette.SymPrim.=~>' in 'S' mode.   type     GetFun mode =       (fun :: Data.Kind.Type -> Data.Kind.Type -> Data.Kind.Type) | fun -> mode -instance UnifiedFun 'Con where-  type GetFun 'Con = (=->)+instance UnifiedFun 'C where+  type GetFun 'C = (=->) -instance UnifiedFun 'Sym where-  type GetFun 'Sym = (=~>)+instance UnifiedFun 'S where+  type GetFun 'S = (=~>)  -- | The unified function type with 2 arguments. type GetFun2 mode a b = GetFun mode a b@@ -194,12 +194,12 @@   dc <-     instanceD       (return preds)-      (applyTypeList (promotedT 'Con : additionalTypes))+      (applyTypeList (promotedT 'C : additionalTypes))       []   ds <-     instanceD       (return preds)-      (applyTypeList (promotedT 'Sym : additionalTypes))+      (applyTypeList (promotedT 'S : additionalTypes))       []   return [x, dc, ds]   where@@ -254,12 +254,12 @@   dc <-     instanceD       (return [])-      (appT (conT $ mkName nm) (promotedT 'Con))+      (appT (conT $ mkName nm) (promotedT 'C))       []   ds <-     instanceD       (return [])-      (appT (conT $ mkName nm) (promotedT 'Sym))+      (appT (conT $ mkName nm) (promotedT 'S))       []   return [x, dc, ds] 

@@ -27,51 +27,53 @@ import Control.Exception (ArithException) import Control.Monad.Except (MonadError) import Grisette.Internal.SymPrim.SymInteger (SymInteger)-import Grisette.Unified.Internal.BaseConstraint-  ( BasicGrisetteType,-    ConSymConversion,-  ) import Grisette.Unified.Internal.Class.UnifiedFromIntegral (UnifiedFromIntegral)+import Grisette.Unified.Internal.Class.UnifiedRep+  ( UnifiedConRep (ConType),+    UnifiedSymRep (SymType),+  ) import Grisette.Unified.Internal.Class.UnifiedSafeDiv (UnifiedSafeDiv) import Grisette.Unified.Internal.Class.UnifiedSafeLinearArith   ( UnifiedSafeLinearArith,   ) import Grisette.Unified.Internal.Class.UnifiedSimpleMergeable (UnifiedBranching)-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Con, Sym))-import Grisette.Unified.Internal.UnifiedConstraint (UnifiedPrimitive)+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S))+import Grisette.Unified.Internal.UnifiedPrim (UnifiedBasicPrim)  class-  ( BasicGrisetteType (GetInteger mode),-    ConSymConversion Integer SymInteger (GetInteger mode),-    Num (GetInteger mode),-    UnifiedPrimitive mode (GetInteger mode),+  ( i ~ GetInteger mode,+    UnifiedConRep i,+    UnifiedSymRep i,+    ConType i ~ Integer,+    SymType i ~ SymInteger,+    UnifiedBasicPrim mode i,+    Num i,     forall m.     (UnifiedBranching mode m, MonadError ArithException m) =>     UnifiedSafeDiv mode ArithException i m,     forall m.     (UnifiedBranching mode m, MonadError ArithException m) =>     UnifiedSafeLinearArith mode ArithException i m,-    UnifiedFromIntegral mode i i,-    i ~ GetInteger mode+    UnifiedFromIntegral mode i i   ) =>   UnifiedIntegerImpl (mode :: EvalModeTag) i     | mode -> i   where-  -- | Get a unified Integer type. Resolves to 'Integer' in 'Con' mode, and-  -- 'SymInteger' in 'Sym' mode.+  -- | Get a unified Integer type. Resolves to 'Integer' in 'C' mode, and+  -- 'SymInteger' in 'S' mode.   type GetInteger mode = int | int -> mode -instance UnifiedIntegerImpl 'Con Integer where-  type GetInteger 'Con = Integer+instance UnifiedIntegerImpl 'C Integer where+  type GetInteger 'C = Integer -instance UnifiedIntegerImpl 'Sym SymInteger where-  type GetInteger 'Sym = SymInteger+instance UnifiedIntegerImpl 'S SymInteger where+  type GetInteger 'S = SymInteger  -- | Evaluation mode with unified 'Integer' type. class   (UnifiedIntegerImpl mode (GetInteger mode)) =>   UnifiedInteger (mode :: EvalModeTag) -instance UnifiedInteger 'Con+instance UnifiedInteger 'C -instance UnifiedInteger 'Sym+instance UnifiedInteger 'S

@@ -0,0 +1,59 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MonoLocalBinds #-}++-- |+-- Module      :   Grisette.Unified.Internal.UnifiedPrim+-- Copyright   :   (c) Sirui Lu 2024+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Unified.Internal.UnifiedPrim+  ( UnifiedPrim,+    UnifiedBasicPrim,+  )+where++import Grisette.Internal.SymPrim.SymPrim (Prim)+import Grisette.Unified.Internal.BaseConstraint (ConSymConversion)+import Grisette.Unified.Internal.Class.UnifiedITEOp+  ( UnifiedITEOp,+  )+import Grisette.Unified.Internal.Class.UnifiedRep+  ( UnifiedConRep (ConType),+    UnifiedSymRep (SymType),+  )+import Grisette.Unified.Internal.Class.UnifiedSimpleMergeable+  ( UnifiedSimpleMergeable,+  )+import Grisette.Unified.Internal.Class.UnifiedSolvable (UnifiedSolvable)+import Grisette.Unified.Internal.Class.UnifiedSymEq (UnifiedSymEq)+import Grisette.Unified.Internal.Class.UnifiedSymOrd (UnifiedSymOrd)++-- | A type that is used as a constraint for all the (unified) primitive types+-- in Grisette.+type UnifiedPrim mode a =+  ( Prim a,+    UnifiedITEOp mode a,+    UnifiedSymEq mode a,+    UnifiedSymOrd mode a+  )++-- | A type that is used as a constraint for all the basic (unified) primitive+-- types in Grisette.+--+-- 'Grisette.Unified.GetSomeWordN' is not considered as a basic (unified)+-- primitive type.+type UnifiedBasicPrim mode a =+  ( UnifiedPrim mode a,+    UnifiedSimpleMergeable mode a,+    UnifiedConRep a,+    UnifiedSymRep a,+    UnifiedSolvable mode a (ConType a),+    ConSymConversion (ConType a) (SymType a) a+  )

@@ -17,16 +17,16 @@ module Grisette.Unified.Internal.Util (withMode) where  import Data.Typeable (Typeable, eqT, type (:~:) (Refl))-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Con, Sym))+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (C, S))  -- | Case analysis on the mode. withMode ::   forall mode r.   (Typeable mode) =>-  ((mode ~ 'Con) => r) ->-  ((mode ~ 'Sym) => r) ->+  ((mode ~ 'C) => r) ->+  ((mode ~ 'S) => r) ->   r-withMode con sym = case (eqT @mode @'Con, eqT @mode @'Sym) of+withMode con sym = case (eqT @mode @'C, eqT @mode @'S) of   (Just Refl, _) -> con   (_, Just Refl) -> sym   _ -> error "impossible"

@@ -16,7 +16,6 @@     SomeSymWordN,     SymEq,     SymIntN,-    SymInteger,     SymWordN,   ) import Grisette.Internal.Core.Data.Class.SymFiniteBits@@ -41,6 +40,7 @@     SymFiniteBits bv,     Show bv,     SymEq bv,+    Num bv,     EvalSym bv   ) =>   p bv ->@@ -75,20 +75,20 @@         symMsb (bv 4 0b0101 :: bv) @?= false         symMsb (bv 4 0b1101 :: bv) @?= true,       testCase "symPopCount" $ do-        symPopCount (bv 4 0 :: bv) @?= (0 :: SymInteger)-        symPopCount (bv 4 0b0101 :: bv) @?= (2 :: SymInteger)-        symPopCount (bv 4 0b1101 :: bv) @?= (3 :: SymInteger)-        symPopCount (bv 4 0b1111 :: bv) @?= (4 :: SymInteger),+        symPopCount (bv 4 0 :: bv) @?= 0+        symPopCount (bv 4 0b0101 :: bv) @?= 2+        symPopCount (bv 4 0b1101 :: bv) @?= 3+        symPopCount (bv 4 0b1111 :: bv) @?= 4,       testCase "symCountLeadingZeros" $ do-        symCountLeadingZeros (bv 4 0 :: bv) @?= (4 :: SymInteger)-        symCountLeadingZeros (bv 4 0b0101 :: bv) @?= (1 :: SymInteger)-        symCountLeadingZeros (bv 4 0b1101 :: bv) @?= (0 :: SymInteger)-        symCountLeadingZeros (bv 4 0b0011 :: bv) @?= (2 :: SymInteger),+        symCountLeadingZeros (bv 4 0 :: bv) @?= 4+        symCountLeadingZeros (bv 4 0b0101 :: bv) @?= 1+        symCountLeadingZeros (bv 4 0b1101 :: bv) @?= 0+        symCountLeadingZeros (bv 4 0b0011 :: bv) @?= 2,       testCase "symCountTrailingZeros" $ do-        symCountTrailingZeros (bv 4 0 :: bv) @?= (4 :: SymInteger)-        symCountTrailingZeros (bv 4 0b1010 :: bv) @?= (1 :: SymInteger)-        symCountTrailingZeros (bv 4 0b1011 :: bv) @?= (0 :: SymInteger)-        symCountTrailingZeros (bv 4 0b1100 :: bv) @?= (2 :: SymInteger)+        symCountTrailingZeros (bv 4 0 :: bv) @?= 4+        symCountTrailingZeros (bv 4 0b1010 :: bv) @?= 1+        symCountTrailingZeros (bv 4 0b1011 :: bv) @?= 0+        symCountTrailingZeros (bv 4 0b1100 :: bv) @?= 2     ]  bvSymFiniteBitsTest ::@@ -132,20 +132,20 @@         symMsb (0b0101 :: bv 4) @?= false         symMsb (0b1101 :: bv 4) @?= true,       testCase "symPopCount" $ do-        symPopCount (0 :: bv 4) @?= (0 :: SymInteger)-        symPopCount (0b0101 :: bv 4) @?= (2 :: SymInteger)-        symPopCount (0b1101 :: bv 4) @?= (3 :: SymInteger)-        symPopCount (0b1111 :: bv 4) @?= (4 :: SymInteger),+        symPopCount (0 :: bv 4) @?= 0+        symPopCount (0b0101 :: bv 4) @?= 2+        symPopCount (0b1101 :: bv 4) @?= 3+        symPopCount (0b1111 :: bv 4) @?= 4,       testCase "symCountLeadingZeros" $ do-        symCountLeadingZeros (0 :: bv 4) @?= (4 :: SymInteger)-        symCountLeadingZeros (0b0101 :: bv 4) @?= (1 :: SymInteger)-        symCountLeadingZeros (0b1101 :: bv 4) @?= (0 :: SymInteger)-        symCountLeadingZeros (0b0011 :: bv 4) @?= (2 :: SymInteger),+        symCountLeadingZeros (0 :: bv 4) @?= 4+        symCountLeadingZeros (0b0101 :: bv 4) @?= 1+        symCountLeadingZeros (0b1101 :: bv 4) @?= 0+        symCountLeadingZeros (0b0011 :: bv 4) @?= 2,       testCase "symCountTrailingZeros" $ do-        symCountTrailingZeros (0 :: bv 4) @?= (4 :: SymInteger)-        symCountTrailingZeros (0b1010 :: bv 4) @?= (1 :: SymInteger)-        symCountTrailingZeros (0b1011 :: bv 4) @?= (0 :: SymInteger)-        symCountTrailingZeros (0b1100 :: bv 4) @?= (2 :: SymInteger)+        symCountTrailingZeros (0 :: bv 4) @?= 4+        symCountTrailingZeros (0b1010 :: bv 4) @?= 1+        symCountTrailingZeros (0b1011 :: bv 4) @?= 0+        symCountTrailingZeros (0b1100 :: bv 4) @?= 2     ]  symFiniteBitsTests :: Test

@@ -7,6 +7,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-}@@ -19,14 +20,28 @@  import Control.Monad.Identity (Identity (Identity)) import Data.Maybe (fromJust)+import Data.Typeable (Typeable) import Grisette-  ( Default (Default),+  ( BasicSymPrim,+    Default (Default),+    EvalSym,+    EvalSym1,+    EvalSym2,+    ExtractSym,+    ExtractSym1,+    ExtractSym2,+    Mergeable,+    Mergeable1,+    Mergeable2,+    SymBool,     SymInteger,     ToCon (toCon),     ToSym (toSym),+    Union,+    deriveAll,+    deriveGADT,   )-import Grisette.TH (deriveAll)-import Grisette.Unified (EvalModeTag (Con, Sym), GetBool, GetData, GetWordN)+import Grisette.Unified (EvalModeTag (C, S), GetBool, GetData, GetWordN)  data T mode n a   = T (GetBool mode) [GetWordN mode n] [a] (GetData mode (T mode n a))@@ -34,12 +49,12 @@  deriveAll ''T -concreteT :: T 'Con 10 Integer+concreteT :: T 'C 10 Integer concreteT =-  toSym (T True [10] [10 :: Integer] (Identity TNil) :: T 'Con 10 Integer)+  toSym (T True [10] [10 :: Integer] (Identity TNil) :: T 'C 10 Integer) -symbolicT :: T 'Sym 10 SymInteger-symbolicT = fromJust $ toCon (toSym concreteT :: T 'Sym 10 SymInteger)+symbolicT :: T 'S 10 SymInteger+symbolicT = fromJust $ toCon (toSym concreteT :: T 'S 10 SymInteger)  newtype X mode = X [GetBool mode] @@ -53,3 +68,43 @@   }  deriveAll ''IdenticalFields++data Expr f a where+  I :: SymInteger -> Expr f SymInteger+  B :: SymBool -> Expr f SymBool+  Add :: Union (Expr f SymInteger) -> Union (Expr f SymInteger) -> Expr f SymInteger+  Mul :: Union (Expr f SymInteger) -> Union (Expr f SymInteger) -> Expr f SymInteger+  Eq :: (BasicSymPrim a, Typeable a) => Union (Expr f a) -> Union (Expr f a) -> Expr f SymBool+  Eq3 ::+    (BasicSymPrim a, Typeable b) =>+    Union (Expr f a) ->+    Union (Expr f a) ->+    Union (Expr f b) ->+    Union (Expr f b) ->+    Expr f b+  XExpr :: f a -> Expr f a++deriveGADT+  ''Expr+  [ ''Mergeable,+    ''Mergeable1,+    ''EvalSym,+    ''EvalSym1,+    ''ExtractSym,+    ''ExtractSym1+  ]++data P a b = P a | Q Int++deriveGADT+  ''P+  [ ''Mergeable,+    ''Mergeable1,+    ''Mergeable2,+    ''EvalSym,+    ''EvalSym1,+    ''EvalSym2,+    ''ExtractSym,+    ''ExtractSym1,+    ''ExtractSym2+  ]

@@ -114,6 +114,30 @@   let SomeBVLit expected = r   actual @?= expected +testSymFuncMatch ::+  String ->+  (SomeSymIntN -> SomeSymIntN -> SomeSymIntN) ->+  SomeSymIntN ->+  SomeSymIntN ->+  SomeSymIntN ->+  Test+testSymFuncMatch name f a b r = testCase name $ do+  let actual = f a b+  let expected = r+  actual @?= expected++testSymFuncMatchLit ::+  String ->+  (SomeSymIntN -> SomeSymIntN -> SomeSymIntN) ->+  SomeSymIntN ->+  SomeSymIntN ->+  SomeSymIntN ->+  Test+testSymFuncMatchLit name f a b r = testCase name $ do+  let SomeBVLit actual = f a b+  let SomeBVLit expected = r+  actual @?= expected+ testFuncMisMatch ::   (NFData r, Show r, Eq r) =>   (SomeIntN -> SomeIntN -> r) ->@@ -277,6 +301,30 @@                 5                 2                 7,+              testSymFuncMatch+                "SomeBV/SomeBV"+                (binSomeBV (\l r -> SomeBV $ l + r) undefined)+                (ssymBV 4 "a")+                (ssymBV 4 "b")+                ((ssymBV 4 "a") + (ssymBV 4 "b")),+              testSymFuncMatch+                "SomeBV/SomeBVCondLit"+                (binSomeBV (\l r -> SomeBV $ l + r) undefined)+                (ssymBV 4 "a")+                (symIte "b" 5 6)+                ((ssymBV 4 "a") + symIte "b" (bv 4 5) (bv 4 6)),+              testSymFuncMatchLit+                "SomeBVCondLit/SomeBVCondLit"+                (binSomeBV undefined (\l r -> SomeBVLit $ l + r))+                (symIte "a" 5 6)+                (symIte "b" 5 6)+                (symIte "a" (symIte "b" 10 11) (symIte "b" 11 12)),+              testSymFuncMatchLit+                "SomeBVLit/SomeBVCondLit"+                (binSomeBV undefined (\l r -> SomeBVLit $ l + r))+                5+                (symIte "b" 5 6)+                (symIte "b" 10 11),               testFuncMisMatch @SomeIntN                 (binSomeBV (\l r -> SomeIntN $ l + r) undefined)                 (bv 4 5)

@@ -74,7 +74,7 @@     EvalModeBase,     EvalModeFP,     EvalModeInteger,-    EvalModeTag (Con, Sym),+    EvalModeTag (C, S),     GetBool,     GetData,     GetFP,@@ -455,8 +455,8 @@     "EvalMode"     [ testGroup         "GetBool"-        [ testCase "Con" $ fbool True False @?= False,-          testCase "Sym" $ do+        [ testCase "C" $ fbool True False @?= False,+          testCase "S" $ do             let l = "l" :: SymBool             let r = "r" :: SymBool             fbool l r@@ -467,8 +467,8 @@         ],       testGroup         "GetInteger"-        [ testCase "Con" $ finteger (1 :: Integer) 2 @?= 1,-          testCase "Sym" $ do+        [ testCase "C" $ finteger (1 :: Integer) 2 @?= 1,+          testCase "S" $ do             let l = "l" :: SymInteger             let r = "r" :: SymInteger             finteger l r@@ -479,11 +479,11 @@         ],       testGroup         "GetIntN"-        [ testCase "Con" $ do+        [ testCase "C" $ do             fbv (1 :: IntN 8) 2 @?= Right 1             fbv' (1 :: IntN 8) 2 @?= ExceptT (Identity (Right 1))             fbvEvalMode (1 :: IntN 8) 2 @?= ExceptT (Identity (Right 1)),-          testCase "Sym" $ do+          testCase "S" $ do             let l = "l" :: SymIntN 8             let r = "r" :: SymIntN 8             let expected = do@@ -503,11 +503,11 @@         ],       testGroup         "GetSomeIntN"-        [ testCase "Con" $ do+        [ testCase "C" $ do             fsomebv (bv 8 1 :: SomeIntN) (bv 8 2) @?= Right (bv 8 1)             fsomebv' (bv 8 1 :: SomeIntN) (bv 8 2)               @?= ExceptT (Identity (Right (bv 8 1))),-          testCase "Sym" $ do+          testCase "S" $ do             let l = ssymBV 8 "l" :: SomeSymIntN             let r = ssymBV 8 "r" :: SomeSymIntN             let expected = do@@ -526,10 +526,10 @@         ],       testGroup         "GetData"-        [ testCase "Con" $ do-            fdata @'Con (Identity $ A 2) @?= Right 2-            fdata @'Con (Identity $ A 1) @?= Left DivideByZero,-          testCase "Sym" $ do+        [ testCase "C" $ do+            fdata @'C (Identity $ A 2) @?= Right 2+            fdata @'C (Identity $ A 1) @?= Left DivideByZero,+          testCase "S" $ do             let a = "a" :: SymIntN 8             fdata (mrgReturn $ A a)               @?= ( Grisette.safeDiv a (a - 1) ::@@ -540,47 +540,47 @@         "Conversion"         [ testGroup             "FP/BV"-            [ testCase "Con" $ do-                bvToFPBitCast @'Con 0x22 @?= 0.15625-                fpToBVBitCast @'Con 0.15625 @?= 0x22-                fpToBVBitCast @'Con fpNaN @?= 0x7c-                safeFPToBVBitCast @'Con 0.15625 @?= Right 0x22-                safeFPToBVBitCast @'Con fpNaN @?= Left NaNError,-              testCase "Sym" $ do-                bvToFPBitCast @'Sym 0x22 @?= 0.15625+            [ testCase "C" $ do+                bvToFPBitCast @'C 0x22 @?= 0.15625+                fpToBVBitCast @'C 0.15625 @?= 0x22+                fpToBVBitCast @'C fpNaN @?= 0x7c+                safeFPToBVBitCast @'C 0.15625 @?= Right 0x22+                safeFPToBVBitCast @'C fpNaN @?= Left NaNError,+              testCase "S" $ do+                bvToFPBitCast @'S 0x22 @?= 0.15625                 let a = "a" :: SymIntN 8-                bvToFPBitCast @'Sym a @?= bitCast a-                fpToBVBitCast @'Sym 0.15625 @?= 0x22-                fpToBVBitCast @'Sym fpNaN @?= 0x7c+                bvToFPBitCast @'S a @?= bitCast a+                fpToBVBitCast @'S 0.15625 @?= 0x22+                fpToBVBitCast @'S fpNaN @?= 0x7c                 let b = "b" :: SymFP 4 4-                fpToBVBitCast @'Sym b @?= bitCastOrCanonical b-                safeFPToBVBitCast @'Sym b+                fpToBVBitCast @'S b @?= bitCastOrCanonical b+                safeFPToBVBitCast @'S b                   @?= ( Grisette.safeBitCast b ::                           ExceptT NotRepresentableFPError Union (SymIntN 8)                       )             ],           testGroup             "FP/FP"-            [ testCase "Con" $ do-                fpToFPConvert @'Con rne 1 @?= 1,-              testCase "Sym" $ do-                fpToFPConvert @'Sym rne 1 @?= 1+            [ testCase "C" $ do+                fpToFPConvert @'C rne 1 @?= 1,+              testCase "S" $ do+                fpToFPConvert @'S rne 1 @?= 1             ],           testGroup             "BV/BV"-            [ testCase "Con" $ do-                bvToBVFromIntegral @'Con 0xa @?= 0xa,-              testCase "Sym" $ do-                bvToBVFromIntegral @'Sym 0xa @?= 0xa+            [ testCase "C" $ do+                bvToBVFromIntegral @'C 0xa @?= 0xa,+              testCase "S" $ do+                bvToBVFromIntegral @'S 0xa @?= 0xa             ]         ],       testGroup         "GetFun"-        [ testCase "Con" $ do-            ufuncTest @'Con 1 @?= 0-            ufuncTest @'Con 2 @?= 2,-          testCase "Sym" $ do+        [ testCase "C" $ do+            ufuncTest @'C 1 @?= 0+            ufuncTest @'C 2 @?= 2,+          testCase "S" $ do             let a = "a"-            ufuncTest @'Sym a @?= symIte (a Grisette..== 1) 0 2+            ufuncTest @'S a @?= symIte (a Grisette..== 1) 0 2         ]     ]

@@ -29,9 +29,9 @@ import Control.Monad.Identity (Identity (Identity)) import Generics.Deriving (Default (Default)) import Grisette (Solvable (con), SymInteger, ToSym (toSym), Union, mrgReturn)-import Grisette.TH (deriveAll, mkUnifiedConstructor, mkUnifiedConstructor')+import Grisette.TH (deriveAll, makeNamedUnifiedCtor, makePrefixedUnifiedCtor) import Grisette.Unified.Internal.EvalMode (EvalModeBase)-import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (Sym))+import Grisette.Unified.Internal.EvalModeTag (EvalModeTag (S)) import Grisette.Unified.Internal.UnifiedBool (UnifiedBool (GetBool)) import Test.Framework (Test, testGroup) import Test.Framework.Providers.HUnit (testCase)@@ -42,7 +42,7 @@   | T1  deriveAll ''T-mkUnifiedConstructor "mk" ''T+makePrefixedUnifiedCtor "mk" ''T  #if MIN_VERSION_base(4,16,0) type FConstraint mode = (EvalModeBase mode)@@ -57,12 +57,12 @@ data TNoMode a = TNoMode0 Bool a (TNoMode a) | TNoMode1  deriveAll ''TNoMode-mkUnifiedConstructor' ["tNoMode0", "tNoMode1"] ''TNoMode+makeNamedUnifiedCtor ["tNoMode0", "tNoMode1"] ''TNoMode  data TNoArg = TNoArg  deriveAll ''TNoArg-mkUnifiedConstructor "mk" ''TNoArg+makePrefixedUnifiedCtor "mk" ''TNoArg  unifiedConstructorTest :: Test unifiedConstructorTest =@@ -72,7 +72,7 @@         f @?= Identity (T True 10 (Identity T1))         f           @?= ( mrgReturn (T (con True) 10 (mrgReturn T1)) ::-                  Union (T 'Sym SymInteger)+                  Union (T 'S SymInteger)               ),       testCase "NoMode" $ do         tNoMode0 True (10 :: Int) TNoMode1