diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 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 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 diff --git a/grisette.cabal b/grisette.cabal --- a/grisette.cabal +++ b/grisette.cabal @@ -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 diff --git a/src/Grisette/Core.hs b/src/Grisette/Core.hs --- a/src/Grisette/Core.hs +++ b/src/Grisette/Core.hs @@ -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 (..), diff --git a/src/Grisette/Internal/Core/Data/Class/SymFiniteBits.hs b/src/Grisette/Internal/Core/Data/Class/SymFiniteBits.hs --- a/src/Grisette/Internal/Core/Data/Class/SymFiniteBits.hs +++ b/src/Grisette/Internal/Core/Data/Class/SymFiniteBits.hs @@ -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 ..] diff --git a/src/Grisette/Internal/SymPrim/SomeBV.hs b/src/Grisette/Internal/SymPrim/SomeBV.hs --- a/src/Grisette/Internal/SymPrim/SomeBV.hs +++ b/src/Grisette/Internal/SymPrim/SomeBV.hs @@ -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 -> diff --git a/src/Grisette/Internal/SymPrim/SymPrim.hs b/src/Grisette/Internal/SymPrim/SymPrim.hs new file mode 100644 --- /dev/null +++ b/src/Grisette/Internal/SymPrim/SymPrim.hs @@ -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 + ) diff --git a/src/Grisette/Internal/TH/Ctor/Common.hs b/src/Grisette/Internal/TH/Ctor/Common.hs new file mode 100644 --- /dev/null +++ b/src/Grisette/Internal/TH/Ctor/Common.hs @@ -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 [] = [] diff --git a/src/Grisette/Internal/TH/Ctor/SmartConstructor.hs b/src/Grisette/Internal/TH/Ctor/SmartConstructor.hs new file mode 100644 --- /dev/null +++ b/src/Grisette/Internal/TH/Ctor/SmartConstructor.hs @@ -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) []] + ] diff --git a/src/Grisette/Internal/TH/Ctor/UnifiedConstructor.hs b/src/Grisette/Internal/TH/Ctor/UnifiedConstructor.hs new file mode 100644 --- /dev/null +++ b/src/Grisette/Internal/TH/Ctor/UnifiedConstructor.hs @@ -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) []] + ] diff --git a/src/Grisette/Internal/TH/GADT/Common.hs b/src/Grisette/Internal/TH/GADT/Common.hs new file mode 100644 --- /dev/null +++ b/src/Grisette/Internal/TH/GADT/Common.hs @@ -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 {..} diff --git a/src/Grisette/Internal/TH/GADT/DeriveEvalSym.hs b/src/Grisette/Internal/TH/GADT/DeriveEvalSym.hs new file mode 100644 --- /dev/null +++ b/src/Grisette/Internal/TH/GADT/DeriveEvalSym.hs @@ -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 diff --git a/src/Grisette/Internal/TH/GADT/DeriveExtractSym.hs b/src/Grisette/Internal/TH/GADT/DeriveExtractSym.hs new file mode 100644 --- /dev/null +++ b/src/Grisette/Internal/TH/GADT/DeriveExtractSym.hs @@ -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 diff --git a/src/Grisette/Internal/TH/GADT/DeriveGADT.hs b/src/Grisette/Internal/TH/GADT/DeriveGADT.hs new file mode 100644 --- /dev/null +++ b/src/Grisette/Internal/TH/GADT/DeriveGADT.hs @@ -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 diff --git a/src/Grisette/Internal/TH/GADT/DeriveMergeable.hs b/src/Grisette/Internal/TH/GADT/DeriveMergeable.hs new file mode 100644 --- /dev/null +++ b/src/Grisette/Internal/TH/GADT/DeriveMergeable.hs @@ -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 diff --git a/src/Grisette/Internal/TH/GADT/UnaryOpCommon.hs b/src/Grisette/Internal/TH/GADT/UnaryOpCommon.hs new file mode 100644 --- /dev/null +++ b/src/Grisette/Internal/TH/GADT/UnaryOpCommon.hs @@ -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] + ] diff --git a/src/Grisette/Internal/TH/MergeConstructor.hs b/src/Grisette/Internal/TH/MergeConstructor.hs deleted file mode 100644 --- a/src/Grisette/Internal/TH/MergeConstructor.hs +++ /dev/null @@ -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) []] - ] diff --git a/src/Grisette/Internal/TH/UnifiedConstructor.hs b/src/Grisette/Internal/TH/UnifiedConstructor.hs deleted file mode 100644 --- a/src/Grisette/Internal/TH/UnifiedConstructor.hs +++ /dev/null @@ -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) []] - ] diff --git a/src/Grisette/Lib/Control/Monad.hs b/src/Grisette/Lib/Control/Monad.hs --- a/src/Grisette/Lib/Control/Monad.hs +++ b/src/Grisette/Lib/Control/Monad.hs @@ -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. diff --git a/src/Grisette/Lib/Data/Bool.hs b/src/Grisette/Lib/Data/Bool.hs --- a/src/Grisette/Lib/Data/Bool.hs +++ b/src/Grisette/Lib/Data/Bool.hs @@ -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 diff --git a/src/Grisette/Lib/Data/Either.hs b/src/Grisette/Lib/Data/Either.hs --- a/src/Grisette/Lib/Data/Either.hs +++ b/src/Grisette/Lib/Data/Either.hs @@ -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 diff --git a/src/Grisette/Lib/Data/Foldable.hs b/src/Grisette/Lib/Data/Foldable.hs --- a/src/Grisette/Lib/Data/Foldable.hs +++ b/src/Grisette/Lib/Data/Foldable.hs @@ -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 diff --git a/src/Grisette/Lib/Data/Functor/Sum.hs b/src/Grisette/Lib/Data/Functor/Sum.hs --- a/src/Grisette/Lib/Data/Functor/Sum.hs +++ b/src/Grisette/Lib/Data/Functor/Sum.hs @@ -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 diff --git a/src/Grisette/Lib/Data/Maybe.hs b/src/Grisette/Lib/Data/Maybe.hs --- a/src/Grisette/Lib/Data/Maybe.hs +++ b/src/Grisette/Lib/Data/Maybe.hs @@ -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 diff --git a/src/Grisette/Lib/Data/Tuple.hs b/src/Grisette/Lib/Data/Tuple.hs --- a/src/Grisette/Lib/Data/Tuple.hs +++ b/src/Grisette/Lib/Data/Tuple.hs @@ -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"] ''(,,,,,,,) diff --git a/src/Grisette/SymPrim.hs b/src/Grisette/SymPrim.hs --- a/src/Grisette/SymPrim.hs +++ b/src/Grisette/SymPrim.hs @@ -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 (=->) (..)) diff --git a/src/Grisette/TH.hs b/src/Grisette/TH.hs --- a/src/Grisette/TH.hs +++ b/src/Grisette/TH.hs @@ -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) diff --git a/src/Grisette/Unified.hs b/src/Grisette/Unified.hs --- a/src/Grisette/Unified.hs +++ b/src/Grisette/Unified.hs @@ -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, ) diff --git a/src/Grisette/Unified/Internal/BVBVConversion.hs b/src/Grisette/Unified/Internal/BVBVConversion.hs --- a/src/Grisette/Unified/Internal/BVBVConversion.hs +++ b/src/Grisette/Unified/Internal/BVBVConversion.hs @@ -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) diff --git a/src/Grisette/Unified/Internal/BVFPConversion.hs b/src/Grisette/Unified/Internal/BVFPConversion.hs --- a/src/Grisette/Unified/Internal/BVFPConversion.hs +++ b/src/Grisette/Unified/Internal/BVFPConversion.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/BaseConstraint.hs b/src/Grisette/Unified/Internal/BaseConstraint.hs --- a/src/Grisette/Unified/Internal/BaseConstraint.hs +++ b/src/Grisette/Unified/Internal/BaseConstraint.hs @@ -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. diff --git a/src/Grisette/Unified/Internal/BaseMonad.hs b/src/Grisette/Unified/Internal/BaseMonad.hs --- a/src/Grisette/Unified/Internal/BaseMonad.hs +++ b/src/Grisette/Unified/Internal/BaseMonad.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/Class/UnifiedFiniteBits.hs b/src/Grisette/Unified/Internal/Class/UnifiedFiniteBits.hs --- a/src/Grisette/Unified/Internal/Class/UnifiedFiniteBits.hs +++ b/src/Grisette/Unified/Internal/Class/UnifiedFiniteBits.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/Class/UnifiedFromIntegral.hs b/src/Grisette/Unified/Internal/Class/UnifiedFromIntegral.hs --- a/src/Grisette/Unified/Internal/Class/UnifiedFromIntegral.hs +++ b/src/Grisette/Unified/Internal/Class/UnifiedFromIntegral.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/Class/UnifiedITEOp.hs b/src/Grisette/Unified/Internal/Class/UnifiedITEOp.hs --- a/src/Grisette/Unified/Internal/Class/UnifiedITEOp.hs +++ b/src/Grisette/Unified/Internal/Class/UnifiedITEOp.hs @@ -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 #-} diff --git a/src/Grisette/Unified/Internal/Class/UnifiedRep.hs b/src/Grisette/Unified/Internal/Class/UnifiedRep.hs new file mode 100644 --- /dev/null +++ b/src/Grisette/Unified/Internal/Class/UnifiedRep.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/Class/UnifiedSafeBitCast.hs b/src/Grisette/Unified/Internal/Class/UnifiedSafeBitCast.hs --- a/src/Grisette/Unified/Internal/Class/UnifiedSafeBitCast.hs +++ b/src/Grisette/Unified/Internal/Class/UnifiedSafeBitCast.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/Class/UnifiedSafeDiv.hs b/src/Grisette/Unified/Internal/Class/UnifiedSafeDiv.hs --- a/src/Grisette/Unified/Internal/Class/UnifiedSafeDiv.hs +++ b/src/Grisette/Unified/Internal/Class/UnifiedSafeDiv.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/Class/UnifiedSafeFdiv.hs b/src/Grisette/Unified/Internal/Class/UnifiedSafeFdiv.hs --- a/src/Grisette/Unified/Internal/Class/UnifiedSafeFdiv.hs +++ b/src/Grisette/Unified/Internal/Class/UnifiedSafeFdiv.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/Class/UnifiedSafeFromFP.hs b/src/Grisette/Unified/Internal/Class/UnifiedSafeFromFP.hs --- a/src/Grisette/Unified/Internal/Class/UnifiedSafeFromFP.hs +++ b/src/Grisette/Unified/Internal/Class/UnifiedSafeFromFP.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/Class/UnifiedSafeLinearArith.hs b/src/Grisette/Unified/Internal/Class/UnifiedSafeLinearArith.hs --- a/src/Grisette/Unified/Internal/Class/UnifiedSafeLinearArith.hs +++ b/src/Grisette/Unified/Internal/Class/UnifiedSafeLinearArith.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/Class/UnifiedSafeSymRotate.hs b/src/Grisette/Unified/Internal/Class/UnifiedSafeSymRotate.hs --- a/src/Grisette/Unified/Internal/Class/UnifiedSafeSymRotate.hs +++ b/src/Grisette/Unified/Internal/Class/UnifiedSafeSymRotate.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/Class/UnifiedSafeSymShift.hs b/src/Grisette/Unified/Internal/Class/UnifiedSafeSymShift.hs --- a/src/Grisette/Unified/Internal/Class/UnifiedSafeSymShift.hs +++ b/src/Grisette/Unified/Internal/Class/UnifiedSafeSymShift.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/Class/UnifiedSolvable.hs b/src/Grisette/Unified/Internal/Class/UnifiedSolvable.hs new file mode 100644 --- /dev/null +++ b/src/Grisette/Unified/Internal/Class/UnifiedSolvable.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/Class/UnifiedSymEq.hs b/src/Grisette/Unified/Internal/Class/UnifiedSymEq.hs --- a/src/Grisette/Unified/Internal/Class/UnifiedSymEq.hs +++ b/src/Grisette/Unified/Internal/Class/UnifiedSymEq.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/Class/UnifiedSymOrd.hs b/src/Grisette/Unified/Internal/Class/UnifiedSymOrd.hs --- a/src/Grisette/Unified/Internal/Class/UnifiedSymOrd.hs +++ b/src/Grisette/Unified/Internal/Class/UnifiedSymOrd.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/EvalMode.hs b/src/Grisette/Unified/Internal/EvalMode.hs --- a/src/Grisette/Unified/Internal/EvalMode.hs +++ b/src/Grisette/Unified/Internal/EvalMode.hs @@ -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 <- diff --git a/src/Grisette/Unified/Internal/EvalModeTag.hs b/src/Grisette/Unified/Internal/EvalModeTag.hs --- a/src/Grisette/Unified/Internal/EvalModeTag.hs +++ b/src/Grisette/Unified/Internal/EvalModeTag.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/FPFPConversion.hs b/src/Grisette/Unified/Internal/FPFPConversion.hs --- a/src/Grisette/Unified/Internal/FPFPConversion.hs +++ b/src/Grisette/Unified/Internal/FPFPConversion.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/UnifiedAlgReal.hs b/src/Grisette/Unified/Internal/UnifiedAlgReal.hs --- a/src/Grisette/Unified/Internal/UnifiedAlgReal.hs +++ b/src/Grisette/Unified/Internal/UnifiedAlgReal.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/UnifiedBV.hs b/src/Grisette/Unified/Internal/UnifiedBV.hs --- a/src/Grisette/Unified/Internal/UnifiedBV.hs +++ b/src/Grisette/Unified/Internal/UnifiedBV.hs @@ -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) diff --git a/src/Grisette/Unified/Internal/UnifiedBool.hs b/src/Grisette/Unified/Internal/UnifiedBool.hs --- a/src/Grisette/Unified/Internal/UnifiedBool.hs +++ b/src/Grisette/Unified/Internal/UnifiedBool.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/UnifiedConstraint.hs b/src/Grisette/Unified/Internal/UnifiedConstraint.hs deleted file mode 100644 --- a/src/Grisette/Unified/Internal/UnifiedConstraint.hs +++ /dev/null @@ -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 - ) diff --git a/src/Grisette/Unified/Internal/UnifiedData.hs b/src/Grisette/Unified/Internal/UnifiedData.hs --- a/src/Grisette/Unified/Internal/UnifiedData.hs +++ b/src/Grisette/Unified/Internal/UnifiedData.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/UnifiedFP.hs b/src/Grisette/Unified/Internal/UnifiedFP.hs --- a/src/Grisette/Unified/Internal/UnifiedFP.hs +++ b/src/Grisette/Unified/Internal/UnifiedFP.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/UnifiedFun.hs b/src/Grisette/Unified/Internal/UnifiedFun.hs --- a/src/Grisette/Unified/Internal/UnifiedFun.hs +++ b/src/Grisette/Unified/Internal/UnifiedFun.hs @@ -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] diff --git a/src/Grisette/Unified/Internal/UnifiedInteger.hs b/src/Grisette/Unified/Internal/UnifiedInteger.hs --- a/src/Grisette/Unified/Internal/UnifiedInteger.hs +++ b/src/Grisette/Unified/Internal/UnifiedInteger.hs @@ -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 diff --git a/src/Grisette/Unified/Internal/UnifiedPrim.hs b/src/Grisette/Unified/Internal/UnifiedPrim.hs new file mode 100644 --- /dev/null +++ b/src/Grisette/Unified/Internal/UnifiedPrim.hs @@ -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 + ) diff --git a/src/Grisette/Unified/Internal/Util.hs b/src/Grisette/Unified/Internal/Util.hs --- a/src/Grisette/Unified/Internal/Util.hs +++ b/src/Grisette/Unified/Internal/Util.hs @@ -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" diff --git a/test/Grisette/Core/Data/Class/SymFiniteBitsTests.hs b/test/Grisette/Core/Data/Class/SymFiniteBitsTests.hs --- a/test/Grisette/Core/Data/Class/SymFiniteBitsTests.hs +++ b/test/Grisette/Core/Data/Class/SymFiniteBitsTests.hs @@ -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 diff --git a/test/Grisette/Core/TH/DerivationTest.hs b/test/Grisette/Core/TH/DerivationTest.hs --- a/test/Grisette/Core/TH/DerivationTest.hs +++ b/test/Grisette/Core/TH/DerivationTest.hs @@ -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 + ] diff --git a/test/Grisette/SymPrim/SomeBVTests.hs b/test/Grisette/SymPrim/SomeBVTests.hs --- a/test/Grisette/SymPrim/SomeBVTests.hs +++ b/test/Grisette/SymPrim/SomeBVTests.hs @@ -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) diff --git a/test/Grisette/Unified/EvalModeTest.hs b/test/Grisette/Unified/EvalModeTest.hs --- a/test/Grisette/Unified/EvalModeTest.hs +++ b/test/Grisette/Unified/EvalModeTest.hs @@ -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 ] ] diff --git a/test/Grisette/Unified/UnifiedConstructorTest.hs b/test/Grisette/Unified/UnifiedConstructorTest.hs --- a/test/Grisette/Unified/UnifiedConstructorTest.hs +++ b/test/Grisette/Unified/UnifiedConstructorTest.hs @@ -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