grisette 0.10.0.0 → 0.11.0.0

raw patch · 207 files changed

+23323/−18507 lines, 207 filesdep ~doctestdep ~hashabledep ~template-haskellPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: doctest, hashable, template-haskell

API changes (from Hackage documentation)

Files

• CHANGELOG.md +30/−1
• README.md +22/−19
• grisette.cabal +117/−48
• src/Grisette/Core.hs +10/−7
• src/Grisette/Internal/Core/Control/Monad/Union.hs +3/−667
• src/Grisette/Internal/Core/Data/Class/CEGISSolver.hs +7/−1
• src/Grisette/Internal/Core/Data/Class/EvalSym.hs +3/−627
• src/Grisette/Internal/Core/Data/Class/ExtractSym.hs +3/−655
• src/Grisette/Internal/Core/Data/Class/GenSym.hs +1/−1
• src/Grisette/Internal/Core/Data/Class/ITEOp.hs +10/−1
• src/Grisette/Internal/Core/Data/Class/Mergeable.hs +43/−1187
• src/Grisette/Internal/Core/Data/Class/PPrint.hs +2/−889
• src/Grisette/Internal/Core/Data/Class/PlainUnion.hs +26/−4
• src/Grisette/Internal/Core/Data/Class/SafeDiv.hs +3/−453
• src/Grisette/Internal/Core/Data/Class/SimpleMergeable.hs +3/−808
• src/Grisette/Internal/Core/Data/Class/Solver.hs +3/−390
• src/Grisette/Internal/Core/Data/Class/SubstSym.hs +3/−630
• src/Grisette/Internal/Core/Data/Class/SymEq.hs +3/−573
• src/Grisette/Internal/Core/Data/Class/SymOrd.hs +3/−788
• src/Grisette/Internal/Core/Data/Class/ToCon.hs +4/−664
• src/Grisette/Internal/Core/Data/Class/ToSym.hs +3/−745
• src/Grisette/Internal/Core/Data/Class/TryMerge.hs +5/−193
• src/Grisette/Internal/Core/Data/UnionBase.hs +6/−377
• src/Grisette/Internal/Internal/Decl/Core/Control/Monad/Union.hs +271/−0
• src/Grisette/Internal/Internal/Decl/Core/Data/Class/EvalSym.hs +269/−0
• src/Grisette/Internal/Internal/Decl/Core/Data/Class/ExtractSym.hs +250/−0
• src/Grisette/Internal/Internal/Decl/Core/Data/Class/Mergeable.hs +530/−0
• src/Grisette/Internal/Internal/Decl/Core/Data/Class/PPrint.hs +481/−0
• src/Grisette/Internal/Internal/Decl/Core/Data/Class/SafeDiv.hs +161/−0
• src/Grisette/Internal/Internal/Decl/Core/Data/Class/SimpleMergeable.hs +305/−0
• src/Grisette/Internal/Internal/Decl/Core/Data/Class/Solver.hs +414/−0
• src/Grisette/Internal/Internal/Decl/Core/Data/Class/SubstSym.hs +245/−0
• src/Grisette/Internal/Internal/Decl/Core/Data/Class/SymEq.hs +253/−0
• src/Grisette/Internal/Internal/Decl/Core/Data/Class/SymOrd.hs +327/−0
• src/Grisette/Internal/Internal/Decl/Core/Data/Class/ToCon.hs +208/−0
• src/Grisette/Internal/Internal/Decl/Core/Data/Class/ToSym.hs +208/−0
• src/Grisette/Internal/Internal/Decl/Core/Data/Class/TryMerge.hs +106/−0
• src/Grisette/Internal/Internal/Decl/Core/Data/UnionBase.hs +271/−0
• src/Grisette/Internal/Internal/Decl/SymPrim/AllSyms.hs +256/−0
• src/Grisette/Internal/Internal/Decl/Unified/BVFPConversion.hs +145/−0
• src/Grisette/Internal/Internal/Decl/Unified/Class/UnifiedITEOp.hs +35/−0
• src/Grisette/Internal/Internal/Decl/Unified/Class/UnifiedSimpleMergeable.hs +78/−0
• src/Grisette/Internal/Internal/Decl/Unified/Class/UnifiedSymEq.hs +64/−0
• src/Grisette/Internal/Internal/Decl/Unified/Class/UnifiedSymOrd.hs +59/−0
• src/Grisette/Internal/Internal/Decl/Unified/EvalMode.hs +294/−0
• src/Grisette/Internal/Internal/Decl/Unified/FPFPConversion.hs +78/−0
• src/Grisette/Internal/Internal/Decl/Unified/UnifiedBV.hs +257/−0
• src/Grisette/Internal/Internal/Decl/Unified/UnifiedBool.hs +45/−0
• src/Grisette/Internal/Internal/Decl/Unified/UnifiedFP.hs +137/−0
• src/Grisette/Internal/Internal/Impl/Core/Control/Monad/Union.hs +495/−0
• src/Grisette/Internal/Internal/Impl/Core/Data/Class/EvalSym.hs +338/−0
• src/Grisette/Internal/Internal/Impl/Core/Data/Class/ExtractSym.hs +394/−0
• src/Grisette/Internal/Internal/Impl/Core/Data/Class/Mergeable.hs +540/−0
• src/Grisette/Internal/Internal/Impl/Core/Data/Class/PPrint.hs +405/−0
• src/Grisette/Internal/Internal/Impl/Core/Data/Class/SafeDiv.hs +347/−0
• src/Grisette/Internal/Internal/Impl/Core/Data/Class/SimpleMergeable.hs +564/−0
• src/Grisette/Internal/Internal/Impl/Core/Data/Class/Solver.hs +63/−0
• src/Grisette/Internal/Internal/Impl/Core/Data/Class/SubstSym.hs +359/−0
• src/Grisette/Internal/Internal/Impl/Core/Data/Class/SymEq.hs +323/−0
• src/Grisette/Internal/Internal/Impl/Core/Data/Class/SymOrd.hs +477/−0
• src/Grisette/Internal/Internal/Impl/Core/Data/Class/ToCon.hs +438/−0
• src/Grisette/Internal/Internal/Impl/Core/Data/Class/ToSym.hs +500/−0
• src/Grisette/Internal/Internal/Impl/Core/Data/Class/TryMerge.hs +151/−0
• src/Grisette/Internal/Internal/Impl/Core/Data/UnionBase.hs +153/−0
• src/Grisette/Internal/Internal/Impl/SymPrim/AllSyms.hs +179/−0
• src/Grisette/Internal/Internal/Impl/Unified/BVFPConversion.hs +143/−0
• src/Grisette/Internal/Internal/Impl/Unified/Class/UnifiedITEOp.hs +100/−0
• src/Grisette/Internal/Internal/Impl/Unified/Class/UnifiedSimpleMergeable.hs +756/−0
• src/Grisette/Internal/Internal/Impl/Unified/Class/UnifiedSymEq.hs +358/−0
• src/Grisette/Internal/Internal/Impl/Unified/Class/UnifiedSymOrd.hs +499/−0
• src/Grisette/Internal/Internal/Impl/Unified/EvalMode.hs +39/−0
• src/Grisette/Internal/Internal/Impl/Unified/FPFPConversion.hs +84/−0
• src/Grisette/Internal/Internal/Impl/Unified/UnifiedBV.hs +149/−0
• src/Grisette/Internal/Internal/Impl/Unified/UnifiedBool.hs +26/−0
• src/Grisette/Internal/Internal/Impl/Unified/UnifiedFP.hs +99/−0
• src/Grisette/Internal/SymPrim/AllSyms.hs +3/−445
• src/Grisette/Internal/SymPrim/BV.hs +12/−2
• src/Grisette/Internal/SymPrim/GeneralFun.hs +7/−1
• src/Grisette/Internal/SymPrim/Prim/Internal/Instances/PEvalOrdTerm.hs +1/−2
• src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs +19/−4
• src/Grisette/Internal/SymPrim/Prim/Internal/Utils.hs +4/−0
• src/Grisette/Internal/SymPrim/SymAlgReal.hs +4/−1
• src/Grisette/Internal/SymPrim/SymBV.hs +4/−1
• src/Grisette/Internal/SymPrim/SymBool.hs +4/−1
• src/Grisette/Internal/SymPrim/SymFP.hs +4/−1
• src/Grisette/Internal/SymPrim/SymGeneralFun.hs +4/−1
• src/Grisette/Internal/SymPrim/SymInteger.hs +7/−2
• src/Grisette/Internal/SymPrim/SymPrim.hs +3/−3
• src/Grisette/Internal/SymPrim/SymTabularFun.hs +4/−1
• src/Grisette/Internal/TH/Ctor/Common.hs +2/−3
• src/Grisette/Internal/TH/Ctor/UnifiedConstructor.hs +71/−23
• src/Grisette/Internal/TH/DeriveBuiltin.hs +0/−91
• src/Grisette/Internal/TH/DeriveInstanceProvider.hs +0/−70
• src/Grisette/Internal/TH/DerivePredefined.hs +0/−372
• src/Grisette/Internal/TH/DeriveTypeParamHandler.hs +0/−197
• src/Grisette/Internal/TH/DeriveUnifiedInterface.hs +0/−336
• src/Grisette/Internal/TH/DeriveWithHandlers.hs +0/−127
• src/Grisette/Internal/TH/GADT/BinaryOpCommon.hs +377/−0
• src/Grisette/Internal/TH/GADT/Common.hs +396/−43
• src/Grisette/Internal/TH/GADT/ConvertOpCommon.hs +469/−0
• src/Grisette/Internal/TH/GADT/DeriveAllSyms.hs +88/−0
• src/Grisette/Internal/TH/GADT/DeriveEq.hs +79/−0
• src/Grisette/Internal/TH/GADT/DeriveEvalSym.hs +44/−27
• src/Grisette/Internal/TH/GADT/DeriveExtractSym.hs +54/−30
• src/Grisette/Internal/TH/GADT/DeriveGADT.hs +654/−55
• src/Grisette/Internal/TH/GADT/DeriveHashable.hs +90/−0
• src/Grisette/Internal/TH/GADT/DeriveMergeable.hs +479/−301
• src/Grisette/Internal/TH/GADT/DeriveNFData.hs +82/−0
• src/Grisette/Internal/TH/GADT/DeriveOrd.hs +78/−0
• src/Grisette/Internal/TH/GADT/DerivePPrint.hs +195/−0
• src/Grisette/Internal/TH/GADT/DeriveSerial.hs +203/−0
• src/Grisette/Internal/TH/GADT/DeriveShow.hs +195/−0
• src/Grisette/Internal/TH/GADT/DeriveSimpleMergeable.hs +87/−0
• src/Grisette/Internal/TH/GADT/DeriveSubstSym.hs +87/−0
• src/Grisette/Internal/TH/GADT/DeriveSymEq.hs +85/−0
• src/Grisette/Internal/TH/GADT/DeriveSymOrd.hs +99/−0
• src/Grisette/Internal/TH/GADT/DeriveToCon.hs +67/−0
• src/Grisette/Internal/TH/GADT/DeriveToSym.hs +67/−0
• src/Grisette/Internal/TH/GADT/DeriveUnifiedSimpleMergeable.hs +112/−0
• src/Grisette/Internal/TH/GADT/DeriveUnifiedSymEq.hs +102/−0
• src/Grisette/Internal/TH/GADT/DeriveUnifiedSymOrd.hs +102/−0
• src/Grisette/Internal/TH/GADT/ShowPPrintCommon.hs +57/−0
• src/Grisette/Internal/TH/GADT/UnaryOpCommon.hs +282/−123
• src/Grisette/Internal/TH/GADT/UnifiedOpCommon.hs +107/−0
• src/Grisette/Internal/TH/Util.hs +105/−10
• src/Grisette/Internal/Unified/BVBVConversion.hs +161/−0
• src/Grisette/Internal/Unified/BVFPConversion.hs +19/−0
• src/Grisette/Internal/Unified/BaseConstraint.hs +26/−0
• src/Grisette/Internal/Unified/BaseMonad.hs +31/−0
• src/Grisette/Internal/Unified/Class/UnifiedFiniteBits.hs +202/−0
• src/Grisette/Internal/Unified/Class/UnifiedFromIntegral.hs +225/−0
• src/Grisette/Internal/Unified/Class/UnifiedITEOp.hs +19/−0
• src/Grisette/Internal/Unified/Class/UnifiedRep.hs +108/−0
• src/Grisette/Internal/Unified/Class/UnifiedSafeBitCast.hs +125/−0
• src/Grisette/Internal/Unified/Class/UnifiedSafeDiv.hs +265/−0
• src/Grisette/Internal/Unified/Class/UnifiedSafeFdiv.hs +82/−0
• src/Grisette/Internal/Unified/Class/UnifiedSafeFromFP.hs +213/−0
• src/Grisette/Internal/Unified/Class/UnifiedSafeLinearArith.hs +216/−0
• src/Grisette/Internal/Unified/Class/UnifiedSafeSymRotate.hs +180/−0
• src/Grisette/Internal/Unified/Class/UnifiedSafeSymShift.hs +224/−0
• src/Grisette/Internal/Unified/Class/UnifiedSimpleMergeable.hs +28/−0
• src/Grisette/Internal/Unified/Class/UnifiedSolvable.hs +135/−0
• src/Grisette/Internal/Unified/Class/UnifiedSymEq.hs +26/−0
• src/Grisette/Internal/Unified/Class/UnifiedSymOrd.hs +32/−0
• src/Grisette/Internal/Unified/EvalMode.hs +24/−0
• src/Grisette/Internal/Unified/EvalModeTag.hs +29/−0
• src/Grisette/Internal/Unified/FPFPConversion.hs +18/−0
• src/Grisette/Internal/Unified/Theories.hs +28/−0
• src/Grisette/Internal/Unified/UnifiedAlgReal.hs +80/−0
• src/Grisette/Internal/Unified/UnifiedBV.hs +24/−0
• src/Grisette/Internal/Unified/UnifiedBool.hs +14/−0
• src/Grisette/Internal/Unified/UnifiedData.hs +140/−0
• src/Grisette/Internal/Unified/UnifiedFP.hs +20/−0
• src/Grisette/Internal/Unified/UnifiedFun.hs +371/−0
• src/Grisette/Internal/Unified/UnifiedInteger.hs +79/−0
• src/Grisette/Internal/Unified/UnifiedPrim.hs +59/−0
• src/Grisette/Internal/Unified/Util.hs +96/−0
• src/Grisette/Lib/Control/Monad.hs +1/−1
• src/Grisette/TH.hs +31/−62
• src/Grisette/Unified.hs +44/−28
• src/Grisette/Unified/Internal/BVBVConversion.hs +0/−161
• src/Grisette/Unified/Internal/BVFPConversion.hs +0/−231
• src/Grisette/Unified/Internal/BaseConstraint.hs +0/−26
• src/Grisette/Unified/Internal/BaseMonad.hs +0/−31
• src/Grisette/Unified/Internal/Class/UnifiedFiniteBits.hs +0/−203
• src/Grisette/Unified/Internal/Class/UnifiedFromIntegral.hs +0/−226
• src/Grisette/Unified/Internal/Class/UnifiedITEOp.hs +0/−106
• src/Grisette/Unified/Internal/Class/UnifiedRep.hs +0/−108
• src/Grisette/Unified/Internal/Class/UnifiedSafeBitCast.hs +0/−128
• src/Grisette/Unified/Internal/Class/UnifiedSafeDiv.hs +0/−265
• src/Grisette/Unified/Internal/Class/UnifiedSafeFdiv.hs +0/−83
• src/Grisette/Unified/Internal/Class/UnifiedSafeFromFP.hs +0/−213
• src/Grisette/Unified/Internal/Class/UnifiedSafeLinearArith.hs +0/−217
• src/Grisette/Unified/Internal/Class/UnifiedSafeSymRotate.hs +0/−180
• src/Grisette/Unified/Internal/Class/UnifiedSafeSymShift.hs +0/−224
• src/Grisette/Unified/Internal/Class/UnifiedSimpleMergeable.hs +0/−809
• src/Grisette/Unified/Internal/Class/UnifiedSolvable.hs +0/−136
• src/Grisette/Unified/Internal/Class/UnifiedSymEq.hs +0/−416
• src/Grisette/Unified/Internal/Class/UnifiedSymOrd.hs +0/−545
• src/Grisette/Unified/Internal/EvalMode.hs +0/−304
• src/Grisette/Unified/Internal/EvalModeTag.hs +0/−29
• src/Grisette/Unified/Internal/FPFPConversion.hs +0/−127
• src/Grisette/Unified/Internal/Theories.hs +0/−28
• src/Grisette/Unified/Internal/UnifiedAlgReal.hs +0/−80
• src/Grisette/Unified/Internal/UnifiedBV.hs +0/−341
• src/Grisette/Unified/Internal/UnifiedBool.hs +0/−48
• src/Grisette/Unified/Internal/UnifiedData.hs +0/−137
• src/Grisette/Unified/Internal/UnifiedFP.hs +0/−190
• src/Grisette/Unified/Internal/UnifiedFun.hs +0/−359
• src/Grisette/Unified/Internal/UnifiedInteger.hs +0/−79
• src/Grisette/Unified/Internal/UnifiedPrim.hs +0/−59
• src/Grisette/Unified/Internal/Util.hs +0/−33
• src/Grisette/Unified/Lib/Control/Monad.hs +1/−1
• src/Grisette/Unified/Lib/Data/Foldable.hs +17/−12
• test/Grisette/Core/Control/Monad/UnionTests.hs +17/−7
• test/Grisette/Core/Data/Class/PPrintTests.hs +33/−26
• test/Grisette/Core/Data/Class/SymEqTests.hs +93/−92
• test/Grisette/Core/Data/Class/SymOrdTests.hs +8/−8
• test/Grisette/Core/Data/Class/ToSymTests.hs +1/−3
• test/Grisette/Core/TH/DerivationData.hs +428/−0
• test/Grisette/Core/TH/DerivationTest.hs +146/−96
• test/Grisette/Core/TH/PartialEvalMode.hs +18/−0
• test/Grisette/SymPrim/FPTests.hs +0/−1
• test/Grisette/Unified/EvalModeTest.hs +6/−4
• test/Grisette/Unified/UnifiedClassesTest.hs +81/−19
• test/Grisette/Unified/UnifiedConstructorTest.hs +62/−23
• test/Main.hs +3/−1

@@ -6,6 +6,35 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [0.11.0.0] - 2024-12-29++### Added+- Added `deriveGADT` for deriving all relevant instances for GADTs.+  ([#267](https://github.com/lsrcz/grisette/pull/267))+- Added `EvalModeConvertible` for a unified constraint for the evaluation modes+  that can be converted to each other with `ToCon` and `ToSym`.+  ([#267](https://github.com/lsrcz/grisette/pull/267))++### Changed+- [Breaking] We no longer support direct `toCon` from a union to a single value+  or `toSym` from a single value to a union. These should now be done through+  `mrgToSym`, `toUnionSym`, and `unionToCon`.+  ([#267](https://github.com/lsrcz/grisette/pull/267))+- [Breaking] Changed the `EvalMode` tag for `Con` to `C` and `Sym` to `S`.+  ([#267](https://github.com/lsrcz/grisette/pull/267))++### Fixed+- Fixed some missing constraints for unified interfaces.+  ([#267](https://github.com/lsrcz/grisette/pull/267))+- Fixed badly staged types in the lifting of terms.+  ([#267](https://github.com/lsrcz/grisette/pull/267))+- Fixed the `Read` instance for bit-vectors on GHC 9.12.+  ([#267](https://github.com/lsrcz/grisette/pull/267))++### Removed+- Removed old template-haskell-based derivation mechanism.+  ([#267](https://github.com/lsrcz/grisette/pull/267))+ ## [0.10.0.0] - 2024-12-11  ### Added@@ -520,7 +549,7 @@  - Initial release for Grisette. -[Unreleased]: https://github.com/lsrcz/grisette/compare/v0.10.0.0...HEAD+[0.11.0.0]: 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

@@ -48,7 +48,7 @@ ```cabal library   ...-  build-depends: grisette >= 0.10 < 0.11+  build-depends: grisette >= 0.11 < 0.12 ```  #### Using stack@@ -59,14 +59,14 @@  ```yaml extra-deps:-  - grisette-0.10.0.0+  - grisette-0.11.0.0 ```  and in your `package.yaml` file:  ```yaml dependencies:-  - grisette >= 0.10 < 0.11+  - grisette >= 0.11 < 0.12 ```  #### Quick start template with `stack new`@@ -168,33 +168,36 @@ 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+  Add :: IntUExpr -> IntUExpr -> IntExpr+  Mul :: IntUExpr -> IntUExpr -> IntExpr+  BAnd :: BoolUExpr -> BoolUExpr -> BoolExpr+  BOr :: BoolUExpr -> BoolUExpr -> 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+type IntUExpr = UExpr SymInteger+type BoolUExpr = UExpr SymBool ```  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+- `deriveGADT` provides instances for data types that are frequently used with+  or provided by Grisette. See the+  [documentation](https://hackage.haskell.org/package/grisette/docs/Grisette-TH.html)+  for the details on what instances are provided. - `makeSmartCtor` generates smart constructors for the GADT.  ```haskell deriving instance Show (Expr a)-deriveGADTAll ''Expr+deriveGADT [''Expr] basicClasses0 makeSmartCtor ''Expr -> intVal 1 :: UIntExpr -- smart constructor for IntVal in Unions+> intVal 1 :: IntUExpr -- smart constructor for IntVal in Unions {IntVal 1}--- Add takes two UIntExprs, use the smart constructors+-- Add takes two IntUExprs, use the smart constructors > Add (intVal "a") (intVal 1) Add {IntVal a} {IntVal 1} ```@@ -207,7 +210,7 @@ ```haskell add2 = add (intVal "a") (intVal 2) mul2 = mul (intVal "a") (intVal 2)-> mrgIf "choice" add2 mul2 :: UIntExpr+> mrgIf "choice" add2 mul2 :: IntUExpr {If choice {Add {IntVal a} {IntVal 2}} {Mul {IntVal a} {IntVal 2}}} ``` @@ -248,11 +251,11 @@ different values.  ```haskell-lhs = Add (intVal "a") (intVal "b")-rhs = Add (intVal "b") (intVal "a")-rhs2 = Add (intVal "a") (intVal "a")+aPlusB = Add (intVal "a") (intVal "b")+bPlusA = Add (intVal "b") (intVal "a")+aPlusA = Add (intVal "a") (intVal "a") -> solve z3 $ eval lhs ./= eval rhs+> solve z3 $ eval aPlusB ./= eval bPlusA Left Unsat ``` @@ -262,7 +265,7 @@ $a+a=0$.  ``` haskell-> solve z3 $ eval lhs ./= eval rhs2+> solve z3 $ eval aPlusB ./= eval aPlusA Right (Model {a -> 0 :: Integer, b -> 1 :: Integer}) ``` 

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           grisette-version:        0.10.0.0+version:        0.11.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,8 +38,9 @@   , GHC == 9.2.8   , GHC == 9.4.8   , GHC == 9.6.6-  , GHC == 9.8.3+  , GHC == 9.8.4   , GHC == 9.10.1+  , GHC == 9.12.1 extra-source-files:     CHANGELOG.md     README.md@@ -157,19 +158,66 @@       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.GADT.BinaryOpCommon       Grisette.Internal.TH.GADT.Common+      Grisette.Internal.TH.GADT.ConvertOpCommon+      Grisette.Internal.TH.GADT.DeriveAllSyms+      Grisette.Internal.TH.GADT.DeriveEq       Grisette.Internal.TH.GADT.DeriveEvalSym       Grisette.Internal.TH.GADT.DeriveExtractSym       Grisette.Internal.TH.GADT.DeriveGADT+      Grisette.Internal.TH.GADT.DeriveHashable       Grisette.Internal.TH.GADT.DeriveMergeable+      Grisette.Internal.TH.GADT.DeriveNFData+      Grisette.Internal.TH.GADT.DeriveOrd+      Grisette.Internal.TH.GADT.DerivePPrint+      Grisette.Internal.TH.GADT.DeriveSerial+      Grisette.Internal.TH.GADT.DeriveShow+      Grisette.Internal.TH.GADT.DeriveSimpleMergeable+      Grisette.Internal.TH.GADT.DeriveSubstSym+      Grisette.Internal.TH.GADT.DeriveSymEq+      Grisette.Internal.TH.GADT.DeriveSymOrd+      Grisette.Internal.TH.GADT.DeriveToCon+      Grisette.Internal.TH.GADT.DeriveToSym+      Grisette.Internal.TH.GADT.DeriveUnifiedSimpleMergeable+      Grisette.Internal.TH.GADT.DeriveUnifiedSymEq+      Grisette.Internal.TH.GADT.DeriveUnifiedSymOrd+      Grisette.Internal.TH.GADT.ShowPPrintCommon       Grisette.Internal.TH.GADT.UnaryOpCommon+      Grisette.Internal.TH.GADT.UnifiedOpCommon       Grisette.Internal.TH.Util+      Grisette.Internal.Unified.BaseConstraint+      Grisette.Internal.Unified.BaseMonad+      Grisette.Internal.Unified.BVBVConversion+      Grisette.Internal.Unified.BVFPConversion+      Grisette.Internal.Unified.Class.UnifiedFiniteBits+      Grisette.Internal.Unified.Class.UnifiedFromIntegral+      Grisette.Internal.Unified.Class.UnifiedITEOp+      Grisette.Internal.Unified.Class.UnifiedRep+      Grisette.Internal.Unified.Class.UnifiedSafeBitCast+      Grisette.Internal.Unified.Class.UnifiedSafeDiv+      Grisette.Internal.Unified.Class.UnifiedSafeFdiv+      Grisette.Internal.Unified.Class.UnifiedSafeFromFP+      Grisette.Internal.Unified.Class.UnifiedSafeLinearArith+      Grisette.Internal.Unified.Class.UnifiedSafeSymRotate+      Grisette.Internal.Unified.Class.UnifiedSafeSymShift+      Grisette.Internal.Unified.Class.UnifiedSimpleMergeable+      Grisette.Internal.Unified.Class.UnifiedSolvable+      Grisette.Internal.Unified.Class.UnifiedSymEq+      Grisette.Internal.Unified.Class.UnifiedSymOrd+      Grisette.Internal.Unified.EvalMode+      Grisette.Internal.Unified.EvalModeTag+      Grisette.Internal.Unified.FPFPConversion+      Grisette.Internal.Unified.Theories+      Grisette.Internal.Unified.UnifiedAlgReal+      Grisette.Internal.Unified.UnifiedBool+      Grisette.Internal.Unified.UnifiedBV+      Grisette.Internal.Unified.UnifiedData+      Grisette.Internal.Unified.UnifiedFP+      Grisette.Internal.Unified.UnifiedFun+      Grisette.Internal.Unified.UnifiedInteger+      Grisette.Internal.Unified.UnifiedPrim+      Grisette.Internal.Unified.Util       Grisette.Internal.Utils.Derive       Grisette.Internal.Utils.Parameterized       Grisette.Lib.Base@@ -196,45 +244,64 @@       Grisette.SymPrim       Grisette.TH       Grisette.Unified-      Grisette.Unified.Internal.BaseConstraint-      Grisette.Unified.Internal.BaseMonad-      Grisette.Unified.Internal.BVBVConversion-      Grisette.Unified.Internal.BVFPConversion-      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-      Grisette.Unified.Internal.Class.UnifiedSafeFromFP-      Grisette.Unified.Internal.Class.UnifiedSafeLinearArith-      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-      Grisette.Unified.Internal.EvalModeTag-      Grisette.Unified.Internal.FPFPConversion-      Grisette.Unified.Internal.Theories-      Grisette.Unified.Internal.UnifiedAlgReal-      Grisette.Unified.Internal.UnifiedBool-      Grisette.Unified.Internal.UnifiedBV-      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       Grisette.Unified.Lib.Data.Foldable       Grisette.Unified.Lib.Data.Functor       Grisette.Utils   other-modules:-      Paths_grisette+      Grisette.Internal.Internal.Decl.Core.Data.Class.ExtractSym+      Grisette.Internal.Internal.Decl.Core.Data.Class.PPrint+      Grisette.Internal.Internal.Decl.Core.Data.Class.ToCon+      Grisette.Internal.Internal.Decl.Core.Data.Class.SafeDiv+      Grisette.Internal.Internal.Decl.Core.Data.Class.SubstSym+      Grisette.Internal.Internal.Decl.Core.Data.Class.ToSym+      Grisette.Internal.Internal.Decl.Core.Data.Class.SymEq+      Grisette.Internal.Internal.Decl.Core.Data.Class.TryMerge+      Grisette.Internal.Internal.Decl.Core.Data.Class.SymOrd+      Grisette.Internal.Internal.Decl.Core.Data.Class.Solver+      Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable+      Grisette.Internal.Internal.Decl.Core.Data.Class.Mergeable+      Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym+      Grisette.Internal.Internal.Decl.Core.Data.UnionBase+      Grisette.Internal.Internal.Decl.Core.Control.Monad.Union+      Grisette.Internal.Internal.Decl.SymPrim.AllSyms+      Grisette.Internal.Internal.Decl.Unified.UnifiedBV+      Grisette.Internal.Internal.Decl.Unified.UnifiedBool+      Grisette.Internal.Internal.Decl.Unified.BVFPConversion+      Grisette.Internal.Internal.Decl.Unified.Class.UnifiedSymEq+      Grisette.Internal.Internal.Decl.Unified.Class.UnifiedSymOrd+      Grisette.Internal.Internal.Decl.Unified.Class.UnifiedSimpleMergeable+      Grisette.Internal.Internal.Decl.Unified.Class.UnifiedITEOp+      Grisette.Internal.Internal.Decl.Unified.UnifiedFP+      Grisette.Internal.Internal.Decl.Unified.EvalMode+      Grisette.Internal.Internal.Decl.Unified.FPFPConversion+      Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym+      Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint+      Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon+      Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv+      Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym+      Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym+      Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq+      Grisette.Internal.Internal.Impl.Core.Data.Class.TryMerge+      Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd+      Grisette.Internal.Internal.Impl.Core.Data.Class.Solver+      Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable+      Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable+      Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym+      Grisette.Internal.Internal.Impl.Core.Data.UnionBase+      Grisette.Internal.Internal.Impl.Core.Control.Monad.Union+      Grisette.Internal.Internal.Impl.SymPrim.AllSyms+      Grisette.Internal.Internal.Impl.Unified.UnifiedBV+      Grisette.Internal.Internal.Impl.Unified.UnifiedBool+      Grisette.Internal.Internal.Impl.Unified.BVFPConversion+      Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymEq+      Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymOrd+      Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSimpleMergeable+      Grisette.Internal.Internal.Impl.Unified.Class.UnifiedITEOp+      Grisette.Internal.Internal.Impl.Unified.UnifiedFP+      Grisette.Internal.Internal.Impl.Unified.EvalMode+      Grisette.Internal.Internal.Impl.Unified.FPFPConversion   hs-source-dirs:       src   ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -Wno-x-partial -Wno-unrecognised-warning-flags@@ -253,7 +320,7 @@     , containers >=0.4 && <0.8     , deepseq >=1.4.4 && <1.6     , generic-deriving >=1.14.1 && <1.15-    , hashable >=1.2.3 && <1.6+    , hashable >=1.2.5 && <1.6     , libBF >=0.6.3 && <0.7     , loch-th >=0.2.2 && <0.3     , mtl >=2.2.2 && <2.4@@ -261,7 +328,7 @@     , prettyprinter >=1.5.0 && <1.8     , sbv >=8.17 && <12     , stm ==2.5.*-    , template-haskell >=2.16 && <2.23+    , template-haskell >=2.16 && <2.24     , text >=1.2.4.1 && <2.2     , th-abstraction >=0.4 && <0.8     , th-compat >=0.1.2 && <0.2@@ -297,10 +364,10 @@     , cereal-text >=0.1.0.2 && <0.2     , containers >=0.4 && <0.8     , deepseq >=1.4.4 && <1.6-    , doctest >=0.18.2 && <0.23+    , doctest >=0.18.2 && <0.24     , generic-deriving >=1.14.1 && <1.15     , grisette-    , hashable >=1.2.3 && <1.6+    , hashable >=1.2.5 && <1.6     , libBF >=0.6.3 && <0.7     , loch-th >=0.2.2 && <0.3     , mtl >=2.2.2 && <2.4@@ -308,7 +375,7 @@     , prettyprinter >=1.5.0 && <1.8     , sbv >=8.17 && <12     , stm ==2.5.*-    , template-haskell >=2.16 && <2.23+    , template-haskell >=2.16 && <2.24     , text >=1.2.4.1 && <2.2     , th-abstraction >=0.4 && <0.8     , th-compat >=0.1.2 && <0.2@@ -356,7 +423,9 @@       Grisette.Core.Data.Class.ToSymTests       Grisette.Core.Data.Class.TryMergeTests       Grisette.Core.Data.UnionBaseTests+      Grisette.Core.TH.DerivationData       Grisette.Core.TH.DerivationTest+      Grisette.Core.TH.PartialEvalMode       Grisette.Lib.Control.ApplicativeTest       Grisette.Lib.Control.Monad.ExceptTests       Grisette.Lib.Control.Monad.State.ClassTests@@ -415,7 +484,7 @@     , deepseq >=1.4.4 && <1.6     , generic-deriving >=1.14.1 && <1.15     , grisette-    , hashable >=1.2.3 && <1.6+    , hashable >=1.2.5 && <1.6     , libBF >=0.6.3 && <0.7     , loch-th >=0.2.2 && <0.3     , mtl >=2.2.2 && <2.4@@ -423,7 +492,7 @@     , prettyprinter >=1.5.0 && <1.8     , sbv >=8.17 && <12     , stm ==2.5.*-    , template-haskell >=2.16 && <2.23+    , template-haskell >=2.16 && <2.24     , test-framework >=0.8.2 && <0.9     , test-framework-hunit >=0.3.0.2 && <0.4     , test-framework-quickcheck2 >=0.3.0.5 && <0.4

@@ -556,16 +556,13 @@     --     deriving (Mergeable) via (Default X)     -- :}     ---    -- Grisette also provide 'Grisette.deriveAll' template haskell procedure to+    -- Grisette also provide 'Grisette.deriveGADT' template haskell procedure to     -- derive all the instances for the classes that are relevant. This include-    -- 'GHC.Generics.Generic', 'Show', 'Mergeable', etc. If you only want to-    -- derive some of them, you can also use 'Grisette.deriveAllExcept' or-    -- 'Grisette.derive'.+    -- 'Show', 'Mergeable', 'Mergeable1', etc.     --     -- >>> :{     -- data X = X SymInteger Integer-    -- deriveAllExcept ''X [''Ord]-    -- -- Ord is excluded because it is a symbolic type+    -- deriveGADT [''X] [''Show, ''Mergeable]     -- :}     --     -- Having the 'Mergeable' instance allows you to use the 'Union' type to@@ -596,7 +593,7 @@     -- >>> import Control.Monad.Except     -- >>> :{     --   data Error = Fail-    --   deriveAll ''Error+    --   deriveGADT [''Error] allClasses0     -- :}     --     -- >>> mrgIf "a" (throwError Fail) (return "x") :: ExceptT Error Union SymInteger@@ -1381,12 +1378,15 @@     GToCon (..),     genericToCon,     genericLiftToCon,+    unionToCon,      -- *** 'ToSym'     ToSymArgs (..),     GToSym (..),     genericToSym,     genericLiftToSym,+    mrgToSym,+    toUnionSym,      -- *** 'EvalSym'     EvalSymArgs (..),@@ -1645,6 +1645,7 @@     onUnion3,     onUnion4,     simpleMerge,+    unionToCon,     (.#),     pattern If,     pattern Single,@@ -1801,6 +1802,8 @@     TryMerge (..),     mrgSingle,     mrgSingleWithStrategy,+    mrgToSym,+    toUnionSym,     tryMerge,   ) import Grisette.Internal.Core.Data.MemoUtils

@@ -1,21 +1,4 @@-{-# LANGUAGE BangPatterns #-}-{-# LANGUAGE CPP #-}-{-# HLINT ignore "Use <&>" #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskellQuotes #-}-{-# LANGUAGE Trustworthy #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}-{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}+{-# OPTIONS_GHC -Wno-missing-import-lists #-}  -- | -- Module      :   Grisette.Internal.Core.Control.Monad.Union@@ -40,652 +23,5 @@   ) where -import Control.Applicative (Alternative ((<|>)))-import Control.DeepSeq (NFData (rnf), NFData1 (liftRnf), rnf1)-import qualified Data.Binary as Binary-import Data.Bytes.Serial (Serial (deserialize, serialize))-import Data.Functor.Classes-  ( Eq1 (liftEq),-    Show1 (liftShowsPrec),-    showsPrec1,-  )-import qualified Data.HashMap.Lazy as HML-import Data.Hashable (Hashable (hashWithSalt))-import qualified Data.Serialize as Cereal-import Data.String (IsString (fromString))-import GHC.TypeNats (KnownNat, type (<=))-import Grisette.Internal.Core.Control.Monad.Class.Union (MonadUnion)-import Grisette.Internal.Core.Data.Class.EvalSym-  ( EvalSym (evalSym),-    EvalSym1 (liftEvalSym),-    evalSym1,-  )-import Grisette.Internal.Core.Data.Class.ExtractSym-  ( ExtractSym (extractSymMaybe),-    ExtractSym1 (liftExtractSymMaybe),-    extractSymMaybe1,-  )-import Grisette.Internal.Core.Data.Class.Function (Function ((#)))-import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))-import Grisette.Internal.Core.Data.Class.LogicalOp-  ( LogicalOp (false, symImplies, symNot, symXor, true, (.&&), (.||)),-  )-import Grisette.Internal.Core.Data.Class.Mergeable-  ( Mergeable (rootStrategy),-    Mergeable1 (liftRootStrategy),-    MergingStrategy (SimpleStrategy),-    rootStrategy1,-  )-import Grisette.Internal.Core.Data.Class.PPrint-  ( PPrint (pformatPrec),-    PPrint1 (liftPFormatPrec),-    groupedEnclose,-    pformatPrec1,-  )-import Grisette.Internal.Core.Data.Class.PlainUnion-  ( PlainUnion (ifView, singleView),-    simpleMerge,-  )-import Grisette.Internal.Core.Data.Class.SimpleMergeable-  ( SimpleMergeable (mrgIte),-    SimpleMergeable1 (liftMrgIte),-    SymBranching (mrgIfPropagatedStrategy, mrgIfWithStrategy),-    mrgIf,-  )-import Grisette.Internal.Core.Data.Class.Solvable-  ( Solvable (con, conView, sym),-    pattern Con,-  )-import Grisette.Internal.Core.Data.Class.Solver-  ( UnionWithExcept (extractUnionExcept),-  )-import Grisette.Internal.Core.Data.Class.SubstSym-  ( SubstSym (substSym),-    SubstSym1 (liftSubstSym),-    substSym1,-  )-import Grisette.Internal.Core.Data.Class.SymEq-  ( SymEq ((.==)),-    SymEq1 (liftSymEq),-    symEq1,-  )-import Grisette.Internal.Core.Data.Class.ToCon-  ( ToCon (toCon),-    ToCon1 (liftToCon),-    toCon1,-  )-import Grisette.Internal.Core.Data.Class.ToSym-  ( ToSym (toSym),-    ToSym1 (liftToSym),-    toSym1,-  )-import Grisette.Internal.Core.Data.Class.TryMerge-  ( TryMerge (tryMergeWithStrategy),-    mrgSingle,-    mrgSingleWithStrategy,-    tryMerge,-  )-import Grisette.Internal.Core.Data.UnionBase-  ( UnionBase (UnionIf, UnionSingle),-    ifWithLeftMost,-  )-import Grisette.Internal.SymPrim.AllSyms-  ( AllSyms (allSymsS),-    AllSyms1 (liftAllSymsS),-    allSymsS1,-  )-import Grisette.Internal.SymPrim.BV (IntN, WordN)-import Grisette.Internal.SymPrim.GeneralFun-  ( type (-->),-  )-import Grisette.Internal.SymPrim.Prim.Term-  ( LinkedRep,-    SupportedNonFuncPrim,-    SupportedPrim,-  )-import Grisette.Internal.SymPrim.SymBV-  ( SymIntN,-    SymWordN,-  )-import Grisette.Internal.SymPrim.SymBool (SymBool)-import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>))-import Grisette.Internal.SymPrim.SymInteger (SymInteger)-import Grisette.Internal.SymPrim.SymTabularFun (type (=~>))-import Grisette.Internal.SymPrim.TabularFun (type (=->))-import Language.Haskell.TH.Syntax (Lift (lift, liftTyped))-import Language.Haskell.TH.Syntax.Compat (unTypeSplice)---- $setup--- >>> import Grisette.Core--- >>> import Grisette.SymPrim---- | 'Union' is the 'UnionBase' container (hidden) enhanced with--- 'MergingStrategy'--- [knowledge propagation](https://okmij.org/ftp/Haskell/set-monad.html#PE).------ The 'UnionBase' models the underlying semantics evaluation semantics for--- unsolvable types with the nested if-then-else tree semantics, and can be--- viewed as the following structure:------ > data UnionBase a--- >   = UnionSingle a--- >   | UnionIf bool (Union a) (Union a)------ The 'UnionSingle' constructor is for a single value with the path condition--- @true@, and the 'UnionIf' constructor is the if operator in an if-then-else--- tree.--- For clarity, when printing a 'Union' value, we will omit the 'UnionSingle'--- constructor. The following two representations has the same semantics.------ > If      c1    (If c11 v11 (If c12 v12 v13))--- >   (If   c2    v2--- >               v3)------ \[---   \left\{\begin{aligned}&t_1&&\mathrm{if}&&c_1\\&v_2&&\mathrm{else if}&&c_2\\&v_3&&\mathrm{otherwise}&&\end{aligned}\right.\hspace{2em}\mathrm{where}\hspace{2em}t_1 = \left\{\begin{aligned}&v_{11}&&\mathrm{if}&&c_{11}\\&v_{12}&&\mathrm{else if}&&c_{12}\\&v_{13}&&\mathrm{otherwise}&&\end{aligned}\right.--- \]------ To reduce the size of the if-then-else tree to reduce the number of paths to--- execute, Grisette would merge the branches in a 'UnionBase' container and--- maintain a representation invariant for them. To perform this merging--- procedure, Grisette relies on a type class called 'Mergeable' and the--- merging strategy defined by it.------ 'UnionBase' is a monad, so we can easily write code with the do-notation and--- monadic combinators. However, the standard monadic operators cannot--- resolve any extra constraints, including the 'Mergeable' constraint (see--- [The constrained-monad--- problem](https://dl.acm.org/doi/10.1145/2500365.2500602)--- by Sculthorpe et al.).--- This prevents the standard do-notations to merge the results automatically,--- and would result in bad performance or very verbose code.------ To reduce this boilerplate, Grisette provide another monad, 'Union' that--- would try to cache the merging strategy.--- The 'Union' has two data constructors (hidden intentionally), 'UAny' and--- 'UMrg'. The 'UAny' data constructor (printed as @<@@...@@>@) wraps an--- arbitrary (probably unmerged) 'UnionBase'. It is constructed when no--- 'Mergeable' knowledge is available (for example, when constructed with--- Haskell\'s 'return'). The 'UMrg' data constructor (printed as @{...}@) wraps--- a merged 'UnionBase' along with the 'Mergeable' constraint. This constraint--- can be propagated to the contexts without 'Mergeable' knowledge, and helps--- the system to merge the resulting 'UnionBase'.------ __/Examples:/__------ 'return' cannot resolve the 'Mergeable' constraint.------ >>> return 1 :: Union Integer--- <1>------ 'Grisette.Lib.Control.Monad.mrgReturn' can resolve the 'Mergeable' constraint.------ >>> import Grisette.Lib.Base--- >>> mrgReturn 1 :: Union Integer--- {1}------ 'mrgIfPropagatedStrategy' does not try to 'Mergeable' constraint.------ >>> mrgIfPropagatedStrategy "a" (return 1) (mrgIfPropagatedStrategy "b" (return 1) (return 2)) :: Union Integer--- <If a 1 (If b 1 2)>------ But 'mrgIfPropagatedStrategy' is able to merge the result if some of the--- branches are merged and have a cached merging strategy:------ >>> mrgIfPropagatedStrategy "a" (return 1) (mrgIfPropagatedStrategy "b" (mrgReturn 1) (return 2)) :: Union Integer--- {If (|| a b) 1 2}------ The '>>=' operator uses 'mrgIfPropagatedStrategy' internally. When the final--- statement in a do-block merges the values, the system can then merge the--- final result.------ >>> :{---   do---     x <- mrgIfPropagatedStrategy (ssym "a") (return 1) (mrgIfPropagatedStrategy (ssym "b") (return 1) (return 2))---     mrgSingle $ x + 1 :: Union Integer--- :}--- {If (|| a b) 2 3}------ Calling a function that merges a result at the last line of a do-notation--- will also merge the whole block. If you stick to these @mrg*@ combinators and--- all the functions will merge the results, the whole program can be--- symbolically evaluated efficiently.------ >>> f x y = mrgIf "c" x y :: Union Integer--- >>> :{---   do---     x <- mrgIfPropagatedStrategy (ssym "a") (return 1) (mrgIfPropagatedStrategy (ssym "b") (return 1) (return 2))---     f x (x + 1)--- :}--- {If (&& c (|| a b)) 1 (If (|| a (|| b c)) 2 3)}------ In "Grisette.Lib.Base", "Grisette.Lib.Mtl", we also provided more @mrg*@--- variants of other combinators. You should stick to these combinators to--- ensure efficient merging by Grisette.-data Union a where-  -- | 'Union' with no 'Mergeable' knowledge.-  UAny ::-    -- | Original 'UnionBase'.-    UnionBase a ->-    Union a-  -- | 'Union' with 'Mergeable' knowledge.-  UMrg ::-    -- | Cached merging strategy.-    MergingStrategy a ->-    -- | Merged 'UnionBase'-    UnionBase a ->-    Union a--instance (Mergeable a, Serial a) => Serial (Union a) where-  serialize = serialize . unionBase-  deserialize = UMrg rootStrategy <$> deserialize--instance (Mergeable a, Serial a) => Cereal.Serialize (Union a) where-  put = serialize-  get = deserialize--instance (Mergeable a, Serial a) => Binary.Binary (Union a) where-  put = serialize-  get = deserialize---- | Get the (possibly empty) cached merging strategy.-unionMergingStrategy :: Union a -> Maybe (MergingStrategy a)-unionMergingStrategy (UMrg s _) = Just s-unionMergingStrategy _ = Nothing--instance (NFData a) => NFData (Union a) where-  rnf = rnf1--instance NFData1 Union where-  liftRnf _a (UAny m) = liftRnf _a m-  liftRnf _a (UMrg _ m) = liftRnf _a m--instance (Lift a) => Lift (Union a) where-  liftTyped (UAny v) = [||UAny v||]-  liftTyped (UMrg _ v) = [||UAny v||]-  lift = unTypeSplice . liftTyped--instance (Show a) => (Show (Union a)) where-  showsPrec = showsPrec1--liftShowsPrecUnion ::-  forall a.-  (Int -> a -> ShowS) ->-  ([a] -> ShowS) ->-  Int ->-  UnionBase a ->-  ShowS-liftShowsPrecUnion sp _ i (UnionSingle a) = sp i a-liftShowsPrecUnion sp sl i (UnionIf _ _ cond t f) =-  showParen (i > 10) $-    showString "If"-      . showChar ' '-      . showsPrec 11 cond-      . showChar ' '-      . sp1 11 t-      . showChar ' '-      . sp1 11 f-  where-    sp1 = liftShowsPrecUnion sp sl--wrapBracket :: Char -> Char -> ShowS -> ShowS-wrapBracket l r p = showChar l . p . showChar r--instance Show1 Union where-  liftShowsPrec sp sl _ (UAny a) =-    wrapBracket '<' '>'-      . liftShowsPrecUnion sp sl 0-      $ a-  liftShowsPrec sp sl _ (UMrg _ a) =-    wrapBracket '{' '}'-      . liftShowsPrecUnion sp sl 0-      $ a--instance (PPrint a) => PPrint (Union a) where-  pformatPrec = pformatPrec1--instance PPrint1 Union where-  liftPFormatPrec fa fl _ = \case-    (UAny a) -> groupedEnclose "<" ">" $ liftPFormatPrec fa fl 0 a-    (UMrg _ a) -> groupedEnclose "{" "}" $ liftPFormatPrec fa fl 0 a---- | Extract the underlying Union. May be unmerged.-unionBase :: Union a -> UnionBase a-unionBase (UAny a) = a-unionBase (UMrg _ a) = a-{-# INLINE unionBase #-}---- | Check if a 'Union' is already merged.-isMerged :: Union a -> Bool-isMerged UAny {} = False-isMerged UMrg {} = True-{-# INLINE isMerged #-}--instance PlainUnion Union where-  singleView = singleView . unionBase-  {-# INLINE singleView #-}-  ifView (UAny u) = case ifView u of-    Just (c, t, f) -> Just (c, UAny t, UAny f)-    Nothing -> Nothing-  ifView (UMrg m u) = case ifView u of-    Just (c, t, f) -> Just (c, UMrg m t, UMrg m f)-    Nothing -> Nothing-  {-# INLINE ifView #-}--instance Functor Union where-  fmap f fa = fa >>= return . f-  {-# INLINE fmap #-}--instance Applicative Union where-  pure = UAny . pure-  {-# INLINE pure #-}-  f <*> a = f >>= (\xf -> a >>= (return . xf))-  {-# INLINE (<*>) #-}--bindUnionBase :: UnionBase a -> (a -> Union b) -> Union b-bindUnionBase (UnionSingle a') f' = f' a'-bindUnionBase (UnionIf _ _ cond ifTrue ifFalse) f' =-  mrgIfPropagatedStrategy-    cond-    (bindUnionBase ifTrue f')-    (bindUnionBase ifFalse f')-{-# INLINE bindUnionBase #-}--instance Monad Union where-  a >>= f = bindUnionBase (unionBase a) f-  {-# INLINE (>>=) #-}---- | Lift a unary operation to 'Union'.-unionUnaryOp :: (a -> a) -> Union a -> Union a-unionUnaryOp f a = do-  a1 <- a-  maybe return mrgSingleWithStrategy (unionMergingStrategy a) $ f a1-{-# INLINE unionUnaryOp #-}---- | Lift a binary operation to 'Union'.-unionBinOp ::-  (a -> a -> a) ->-  Union a ->-  Union a ->-  Union a-unionBinOp f a b = do-  a1 <- a-  b1 <- b-  maybe-    return-    mrgSingleWithStrategy-    (unionMergingStrategy a <|> unionMergingStrategy b)-    $ f a1 b1-{-# INLINE unionBinOp #-}--instance (Mergeable a) => Mergeable (Union a) where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance (Mergeable a) => SimpleMergeable (Union a) where-  mrgIte = mrgIf-  {-# INLINE mrgIte #-}--instance Mergeable1 Union where-  liftRootStrategy m = SimpleStrategy $ mrgIfWithStrategy m-  {-# INLINE liftRootStrategy #-}--instance SimpleMergeable1 Union where-  liftMrgIte m = mrgIfWithStrategy (SimpleStrategy m)-  {-# INLINE liftMrgIte #-}--instance TryMerge Union where-  tryMergeWithStrategy _ m@(UMrg _ _) = m-  tryMergeWithStrategy s (UAny u) = UMrg s $ tryMergeWithStrategy s u-  {-# INLINE tryMergeWithStrategy #-}--instance SymBranching Union where-  mrgIfWithStrategy s (Con c) l r =-    if c then tryMergeWithStrategy s l else tryMergeWithStrategy s r-  mrgIfWithStrategy s cond l r =-    UMrg s $-      mrgIfWithStrategy-        s-        cond-        (unionBase l)-        (unionBase r)-  {-# INLINE mrgIfWithStrategy #-}-  mrgIfPropagatedStrategy cond (UAny t) (UAny f) =-    UAny $ ifWithLeftMost False cond t f-  mrgIfPropagatedStrategy cond t@(UMrg m _) f = mrgIfWithStrategy m cond t f-  mrgIfPropagatedStrategy cond t f@(UMrg m _) = mrgIfWithStrategy m cond t f-  {-# INLINE mrgIfPropagatedStrategy #-}--instance (SymEq a) => SymEq (Union a) where-  (.==) = symEq1-  {-# INLINE (.==) #-}--instance SymEq1 Union where-  liftSymEq f x y = simpleMerge $ f <$> x <*> y-  {-# INLINE liftSymEq #-}---- | Lift the 'Union' to any Applicative 'SymBranching'.-liftUnion ::-  forall u a. (Mergeable a, SymBranching u, Applicative u) => Union a -> u a-liftUnion u = go (unionBase u)-  where-    go :: UnionBase a -> u a-    go (UnionSingle v) = mrgSingle v-    go (UnionIf _ _ c t f) = mrgIf c (go t) (go f)---- | Alias for `liftUnion`, but for monads.-liftToMonadUnion :: (Mergeable a, MonadUnion u) => Union a -> u a-liftToMonadUnion = liftUnion--instance {-# INCOHERENT #-} (ToSym a b, Mergeable b) => ToSym a (Union b) where-  toSym = mrgSingle . toSym--instance (ToSym a b) => ToSym (Union a) (Union b) where-  toSym = toSym1--instance ToSym1 Union Union where-  liftToSym f = tryMerge . fmap f--instance ToSym (Union Bool) SymBool where-  toSym = simpleMerge . fmap con--instance ToSym (Union Integer) SymInteger where-  toSym = simpleMerge . fmap con--instance (KnownNat n, 1 <= n) => ToSym (Union (IntN n)) (SymIntN n) where-  toSym = simpleMerge . fmap con--instance (KnownNat n, 1 <= n) => ToSym (Union (WordN n)) (SymWordN n) where-  toSym = simpleMerge . fmap con--instance-  ( SupportedPrim ((=->) ca cb),-    SupportedNonFuncPrim ca,-    LinkedRep ca sa,-    LinkedRep cb sb-  ) =>-  ToSym (Union ((=->) ca cb)) ((=~>) sa sb)-  where-  toSym = simpleMerge . fmap con--instance-  ( SupportedPrim ((-->) ca cb),-    SupportedNonFuncPrim ca,-    LinkedRep ca sa,-    LinkedRep cb sb-  ) =>-  ToSym (Union ((-->) ca cb)) ((-~>) sa sb)-  where-  toSym = simpleMerge . fmap con--instance {-# INCOHERENT #-} (ToCon a b, Mergeable a) => ToCon (Union a) b where-  toCon v = go $ unionBase $ tryMerge v-    where-      go (UnionSingle x) = toCon x-      go _ = Nothing--instance (ToCon a b) => ToCon (Union a) (Union b) where-  toCon = toCon1--instance ToCon1 Union Union where-  liftToCon f v = go $ unionBase v-    where-      go (UnionSingle x) = case f x of-        Nothing -> Nothing-        Just v -> Just $ return v-      go (UnionIf _ _ c t f) = do-        t' <- go t-        f' <- go f-        return $ mrgIfPropagatedStrategy c t' f'--instance (EvalSym a) => EvalSym (Union a) where-  evalSym = evalSym1--instance EvalSym1 Union where-  liftEvalSym f fillDefault model x = go $ unionBase x-    where-      go (UnionSingle v) = single $ f fillDefault model v-      go (UnionIf _ _ cond t f) =-        unionIf (evalSym fillDefault model cond) (go t) (go f)-      strategy = unionMergingStrategy x-      single = maybe return mrgSingleWithStrategy strategy-      unionIf = maybe mrgIfPropagatedStrategy mrgIfWithStrategy strategy--instance (SubstSym a) => SubstSym (Union a) where-  substSym = substSym1--instance SubstSym1 Union where-  liftSubstSym f sym val x = go $ unionBase x-    where-      go (UnionSingle v) = single $ f sym val v-      go (UnionIf _ _ cond t f) =-        unionIf-          (substSym sym val cond)-          (go t)-          (go f)-      strategy = unionMergingStrategy x-      single = maybe return mrgSingleWithStrategy strategy-      unionIf = maybe mrgIfPropagatedStrategy mrgIfWithStrategy strategy--instance (ExtractSym a) => ExtractSym (Union a) where-  extractSymMaybe = extractSymMaybe1--instance ExtractSym1 Union where-  liftExtractSymMaybe e v = go $ unionBase v-    where-      go (UnionSingle x) = e x-      go (UnionIf _ _ cond t f) = extractSymMaybe cond <> go t <> go f--instance (Hashable a) => Hashable (Union a) where-  s `hashWithSalt` (UAny u) = s `hashWithSalt` (0 :: Int) `hashWithSalt` u-  s `hashWithSalt` (UMrg _ u) = s `hashWithSalt` (1 :: Int) `hashWithSalt` u--instance (Eq a) => Eq (Union a) where-  UAny l == UAny r = l == r-  UMrg _ l == UMrg _ r = l == r-  _ == _ = False--instance Eq1 Union where-  liftEq e l r = liftEq e (unionBase l) (unionBase r)--instance (Num a, Mergeable a) => Num (Union a) where-  fromInteger = mrgSingle . fromInteger-  negate = unionUnaryOp negate-  (+) = unionBinOp (+)-  (*) = unionBinOp (*)-  (-) = unionBinOp (-)-  abs = unionUnaryOp abs-  signum = unionUnaryOp signum--instance (ITEOp a, Mergeable a) => ITEOp (Union a) where-  symIte = mrgIf--instance (LogicalOp a, Mergeable a) => LogicalOp (Union a) where-  true = mrgSingle true-  false = mrgSingle false-  (.||) = unionBinOp (.||)-  (.&&) = unionBinOp (.&&)-  symNot = unionUnaryOp symNot-  symXor = unionBinOp symXor-  symImplies = unionBinOp symImplies--instance (Solvable c t, Mergeable t) => Solvable c (Union t) where-  con = mrgSingle . con-  {-# INLINE con #-}-  sym = mrgSingle . sym-  {-# INLINE sym #-}-  conView v = do-    c <- singleView $ tryMerge v-    conView c-  {-# INLINE conView #-}--instance-  (Function f arg ret, Mergeable f, Mergeable ret) =>-  Function (Union f) arg (Union ret)-  where-  f # a = do-    f1 <- f-    mrgSingle $ f1 # a--instance (IsString a, Mergeable a) => IsString (Union a) where-  fromString = mrgSingle . fromString---- AllSyms-instance (AllSyms a) => AllSyms (Union a) where-  allSymsS = allSymsS1--instance AllSyms1 Union where-  liftAllSymsS f = liftAllSymsS f . unionBase---- Concrete Key HashMaps---- | Tag for concrete types.--- Useful for specifying the merge strategy for some parametrized types where we should have different--- merge strategy for symbolic and concrete ones.-class (Eq t, Ord t, Hashable t) => IsConcrete t--instance IsConcrete Bool--instance IsConcrete Integer--instance (IsConcrete k, Mergeable t) => Mergeable (HML.HashMap k (Union (Maybe t))) where-  rootStrategy = SimpleStrategy mrgIte--instance (IsConcrete k, Mergeable t) => SimpleMergeable (HML.HashMap k (Union (Maybe t))) where-  mrgIte cond l r =-    HML.unionWith (mrgIf cond) ul ur-    where-      ul =-        foldr-          ( \k m -> case HML.lookup k m of-              Nothing -> HML.insert k (mrgSingle Nothing) m-              _ -> m-          )-          l-          (HML.keys r)-      ur =-        foldr-          ( \k m -> case HML.lookup k m of-              Nothing -> HML.insert k (mrgSingle Nothing) m-              _ -> m-          )-          r-          (HML.keys l)--instance UnionWithExcept (Union (Either e v)) Union e v where-  extractUnionExcept = id---- | The size of a union is defined as the number of branches.--- For example,------ >>> unionSize (return True)--- 1--- >>> unionSize (mrgIf "a" (return 1) (return 2) :: Union Integer)--- 2--- >>> unionSize (choose [1..7] "a" :: Union Integer)--- 7-unionSize :: Union a -> Int-unionSize = unionSize' . unionBase-  where-    unionSize' (UnionSingle _) = 1-    unionSize' (UnionIf _ _ _ l r) = unionSize' l + unionSize' r+import Grisette.Internal.Internal.Decl.Core.Control.Monad.Union+import Grisette.Internal.Internal.Impl.Core.Control.Monad.Union

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveLift #-}@@ -68,11 +69,16 @@   ) where +#if MIN_VERSION_base(4,20,0)+import Data.List (partition)+#else+import Data.List (foldl', partition)+#endif+ import Control.DeepSeq (NFData) import qualified Data.Binary as Binary import Data.Bytes.Serial (Serial (deserialize, serialize)) import Data.Hashable (Hashable)-import Data.List (foldl', partition) import qualified Data.Serialize as Cereal import GHC.Generics (Generic) import Generics.Deriving (Default (Default))

@@ -1,19 +1,4 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DerivingVia #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE QuantifiedConstraints #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE Trustworthy #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-missing-import-lists #-}  -- | -- Module      :   Grisette.Internal.Core.Data.Class.EvalSym@@ -42,614 +27,5 @@   ) where -import Control.Monad.Except (ExceptT (ExceptT), runExceptT)-import Control.Monad.Identity-  ( Identity (Identity),-    IdentityT (IdentityT),-  )-import Control.Monad.Trans.Maybe (MaybeT (MaybeT, runMaybeT))-import qualified Control.Monad.Writer.Lazy as WriterLazy-import qualified Control.Monad.Writer.Strict as WriterStrict-import qualified Data.ByteString as B-import Data.Functor.Compose (Compose (Compose))-import Data.Functor.Const (Const)-import Data.Functor.Product (Product)-import Data.Functor.Sum (Sum)-import qualified Data.HashSet as HS-import Data.Int (Int16, Int32, Int64, Int8)-import Data.Kind (Type)-import Data.Maybe (fromJust)-import Data.Monoid (Alt, Ap)-import Data.Ord (Down)-import Data.Ratio (Ratio, denominator, numerator, (%))-import qualified Data.Text as T-import Data.Word (Word16, Word32, Word64, Word8)-import GHC.TypeNats (KnownNat, type (<=))-import Generics.Deriving-  ( Default (Default, unDefault),-    Default1 (Default1, unDefault1),-    Generic (Rep, from, to),-    Generic1 (Rep1, from1, to1),-    K1 (K1),-    M1 (M1),-    Par1 (Par1),-    Rec1 (Rec1),-    U1,-    V1,-    (:.:) (Comp1),-    type (:*:) ((:*:)),-    type (:+:) (L1, R1),-  )-import Generics.Deriving.Instances ()-import qualified Generics.Deriving.Monoid as Monoid-import Grisette.Internal.Core.Control.Exception-  ( AssertionError,-    VerificationConditions,-  )-import Grisette.Internal.Core.Data.Class.ToCon-  ( ToCon (toCon),-    ToCon1,-    ToCon2,-    toCon1,-    toCon2,-  )-import Grisette.Internal.SymPrim.AlgReal (AlgReal)-import Grisette.Internal.SymPrim.BV (IntN, WordN)-import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, NotRepresentableFPError, ValidFP)-import Grisette.Internal.SymPrim.GeneralFun (type (-->) (GeneralFun))-import Grisette.Internal.SymPrim.Prim.Model (Model, evalTerm)-import Grisette.Internal.SymPrim.Prim.Term-  ( SymRep (SymType),-    someTypedSymbol,-  )-import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal))-import Grisette.Internal.SymPrim.SymBV-  ( SymIntN (SymIntN),-    SymWordN (SymWordN),-  )-import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))-import Grisette.Internal.SymPrim.SymFP-  ( SymFP (SymFP),-    SymFPRoundingMode (SymFPRoundingMode),-  )-import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>) (SymGeneralFun))-import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))-import Grisette.Internal.SymPrim.SymTabularFun (type (=~>) (SymTabularFun))-import Grisette.Internal.SymPrim.TabularFun (type (=->) (TabularFun))-import Grisette.Internal.TH.DeriveBuiltin (deriveBuiltins)-import Grisette.Internal.TH.DeriveInstanceProvider-  ( Strategy (ViaDefault, ViaDefault1),-  )-import Grisette.Internal.Utils.Derive (Arity0, Arity1)---- $setup--- >>> import Grisette.Core--- >>> import Grisette.SymPrim--- >>> import Data.Proxy---- | Evaluating symbolic values with some model. This would substitute the--- symbols (symbolic constants) with the values in the model.------ >>> let model = insertValue "a" (1 :: Integer) emptyModel :: Model--- >>> evalSym False model ([ssym "a", ssym "b"] :: [SymInteger])--- [1,b]------ If we set the first argument true, the missing symbols will be filled in--- with some default values:------ >>> evalSym True model ([ssym "a", ssym "b"] :: [SymInteger])--- [1,0]------ __Note 1:__ This type class can be derived for algebraic data types.--- You may need the @DerivingVia@ and @DerivingStrategies@ extensions.------ > data X = ... deriving Generic deriving EvalSym via (Default X)-class EvalSym a where-  -- | Evaluate a symbolic value with some model, possibly fill in values for-  -- the missing symbols.-  evalSym :: Bool -> Model -> a -> a---- | Evaluate a symbolic value with some model, fill in values for the missing--- symbols, and convert the result to a concrete value.------ >>> let model = insertValue "a" (1 :: Integer) emptyModel :: Model--- >>> evalSymToCon model ([ssym "a", ssym "b"] :: [SymInteger]) :: [Integer]--- [1,0]-evalSymToCon :: (ToCon a b, EvalSym a) => Model -> a -> b-evalSymToCon model a = fromJust $ toCon $ evalSym True model a---- | Lifting of 'EvalSym' to unary type constructors.-class (forall a. (EvalSym a) => EvalSym (f a)) => EvalSym1 f where-  -- | Lift the 'evalSym' function to unary type constructors.-  liftEvalSym :: (Bool -> Model -> a -> a) -> (Bool -> Model -> f a -> f a)---- | Lifting the standard 'evalSym' to unary type constructors.-evalSym1 :: (EvalSym1 f, EvalSym a) => Bool -> Model -> f a -> f a-evalSym1 = liftEvalSym evalSym-{-# INLINE evalSym1 #-}---- | Evaluate and convert to concrete values with lifted standard 'evalSym' for--- unary type constructors. See 'evalSymToCon'.-evalSymToCon1 ::-  (EvalSym1 f, EvalSym a, ToCon1 f g, ToCon a b) =>-  Model ->-  f a ->-  g b-evalSymToCon1 model a = fromJust $ toCon1 $ evalSym1 True model a-{-# INLINE evalSymToCon1 #-}---- | Lifting of 'EvalSym1' to binary type constructors.-class (forall a. (EvalSym a) => EvalSym1 (f a)) => EvalSym2 f where-  -- | Lift the 'evalSym' function to binary type constructors.-  liftEvalSym2 ::-    (Bool -> Model -> a -> a) ->-    (Bool -> Model -> b -> b) ->-    (Bool -> Model -> f a b -> f a b)---- | Lifting the standard 'evalSym' to binary type constructors.-evalSym2 ::-  (EvalSym2 f, EvalSym a, EvalSym b) =>-  Bool ->-  Model ->-  f a b ->-  f a b-evalSym2 = liftEvalSym2 evalSym evalSym-{-# INLINE evalSym2 #-}---- | Evaluate and convert to concrete values with lifted standard 'evalSym' for--- binary type constructors. See 'evalSymToCon'.-evalSymToCon2 ::-  ( EvalSym2 f,-    EvalSym a,-    EvalSym c,-    ToCon2 f g,-    ToCon a b,-    ToCon c d-  ) =>-  Model ->-  f a c ->-  g b d-evalSymToCon2 model a = fromJust $ toCon2 $ evalSym2 True model a-{-# INLINE evalSymToCon2 #-}---- Derivations---- | The arguments to the generic 'evalSym' function.-data family EvalSymArgs arity a :: Type--data instance EvalSymArgs Arity0 _ = EvalSymArgs0--newtype instance EvalSymArgs Arity1 a-  = EvalSymArgs1 (Bool -> Model -> a -> a)---- | The class of types that can be generically evaluated.-class GEvalSym arity f where-  gevalSym :: EvalSymArgs arity a -> Bool -> Model -> f a -> f a--instance GEvalSym arity V1 where-  gevalSym _ _ _ = id-  {-# INLINE gevalSym #-}--instance GEvalSym arity U1 where-  gevalSym _ _ _ = id-  {-# INLINE gevalSym #-}--instance-  (GEvalSym arity a, GEvalSym arity b) =>-  GEvalSym arity (a :*: b)-  where-  gevalSym args fillDefault model (a :*: b) =-    gevalSym args fillDefault model a-      :*: gevalSym args fillDefault model b-  {-# INLINE gevalSym #-}--instance-  (GEvalSym arity a, GEvalSym arity b) =>-  GEvalSym arity (a :+: b)-  where-  gevalSym args fillDefault model (L1 l) =-    L1 $ gevalSym args fillDefault model l-  gevalSym args fillDefault model (R1 r) =-    R1 $ gevalSym args fillDefault model r-  {-# INLINE gevalSym #-}--instance (GEvalSym arity a) => GEvalSym arity (M1 i c a) where-  gevalSym args fillDefault model (M1 x) =-    M1 $ gevalSym args fillDefault model x-  {-# INLINE gevalSym #-}--instance (EvalSym a) => GEvalSym arity (K1 i a) where-  gevalSym _ fillDefault model (K1 x) = K1 $ evalSym fillDefault model x-  {-# INLINE gevalSym #-}--instance GEvalSym Arity1 Par1 where-  gevalSym (EvalSymArgs1 f) fillDefault model (Par1 x) =-    Par1 $ f fillDefault model x-  {-# INLINE gevalSym #-}--instance (EvalSym1 a) => GEvalSym Arity1 (Rec1 a) where-  gevalSym (EvalSymArgs1 f) fillDefault model (Rec1 x) =-    Rec1 $ liftEvalSym f fillDefault model x-  {-# INLINE gevalSym #-}--instance-  (EvalSym1 f, GEvalSym Arity1 g) =>-  GEvalSym Arity1 (f :.: g)-  where-  gevalSym targs fillDefault model (Comp1 x) =-    Comp1 $ liftEvalSym (gevalSym targs) fillDefault model x-  {-# INLINE gevalSym #-}---- | Generic 'evalSym' function.-genericEvalSym ::-  (Generic a, GEvalSym Arity0 (Rep a)) => Bool -> Model -> a -> a-genericEvalSym fillDefault model =-  to . gevalSym EvalSymArgs0 fillDefault model . from-{-# INLINE genericEvalSym #-}---- | Generic 'liftEvalSym' function.-genericLiftEvalSym ::-  (Generic1 f, GEvalSym Arity1 (Rep1 f)) =>-  (Bool -> Model -> a -> a) ->-  Bool ->-  Model ->-  f a ->-  f a-genericLiftEvalSym f fillDefault model =-  to1 . gevalSym (EvalSymArgs1 f) fillDefault model . from1-{-# INLINE genericLiftEvalSym #-}--instance-  (Generic a, GEvalSym Arity0 (Rep a)) =>-  EvalSym (Default a)-  where-  evalSym fillDefault model =-    Default . genericEvalSym fillDefault model . unDefault-  {-# INLINE evalSym #-}--instance-  (Generic1 f, GEvalSym Arity1 (Rep1 f), EvalSym a) =>-  EvalSym (Default1 f a)-  where-  evalSym = evalSym1-  {-# INLINE evalSym #-}--instance-  (Generic1 f, GEvalSym Arity1 (Rep1 f)) =>-  EvalSym1 (Default1 f)-  where-  liftEvalSym f fillDefault model =-    Default1 . genericLiftEvalSym f fillDefault model . unDefault1-  {-# INLINE liftEvalSym #-}--#define CONCRETE_EVALUATESYM(type) \-instance EvalSym type where \-  evalSym _ _ = id--#define CONCRETE_EVALUATESYM_BV(type) \-instance (KnownNat n, 1 <= n) => EvalSym (type n) where \-  evalSym _ _ = id--#if 1-CONCRETE_EVALUATESYM(Bool)-CONCRETE_EVALUATESYM(Integer)-CONCRETE_EVALUATESYM(Char)-CONCRETE_EVALUATESYM(Int)-CONCRETE_EVALUATESYM(Int8)-CONCRETE_EVALUATESYM(Int16)-CONCRETE_EVALUATESYM(Int32)-CONCRETE_EVALUATESYM(Int64)-CONCRETE_EVALUATESYM(Word)-CONCRETE_EVALUATESYM(Word8)-CONCRETE_EVALUATESYM(Word16)-CONCRETE_EVALUATESYM(Word32)-CONCRETE_EVALUATESYM(Word64)-CONCRETE_EVALUATESYM(Float)-CONCRETE_EVALUATESYM(Double)-CONCRETE_EVALUATESYM(B.ByteString)-CONCRETE_EVALUATESYM(T.Text)-CONCRETE_EVALUATESYM(FPRoundingMode)-CONCRETE_EVALUATESYM(Monoid.All)-CONCRETE_EVALUATESYM(Monoid.Any)-CONCRETE_EVALUATESYM(Ordering)-CONCRETE_EVALUATESYM_BV(IntN)-CONCRETE_EVALUATESYM_BV(WordN)-CONCRETE_EVALUATESYM(AlgReal)-#endif--instance (Integral a, EvalSym a) => EvalSym (Ratio a) where-  evalSym fillDefault model r =-    evalSym fillDefault model (numerator r)-      % evalSym fillDefault model (denominator r)--instance (ValidFP eb fb) => EvalSym (FP eb fb) where-  evalSym _ _ = id---- Symbolic primitives-#define EVALUATE_SYM_SIMPLE(symtype) \-instance EvalSym symtype where \-  evalSym fillDefault model (symtype t) = \-    symtype $ evalTerm fillDefault model HS.empty t--#define EVALUATE_SYM_BV(symtype) \-instance (KnownNat n, 1 <= n) => EvalSym (symtype n) where \-  evalSym fillDefault model (symtype t) = \-    symtype $ evalTerm fillDefault model HS.empty t--#define EVALUATE_SYM_FUN(cop, op, cons) \-instance EvalSym (op sa sb) where \-  evalSym fillDefault model (cons t) = \-    cons $ evalTerm fillDefault model HS.empty t--#if 1-EVALUATE_SYM_SIMPLE(SymBool)-EVALUATE_SYM_SIMPLE(SymInteger)-EVALUATE_SYM_SIMPLE(SymFPRoundingMode)-EVALUATE_SYM_SIMPLE(SymAlgReal)-EVALUATE_SYM_BV(SymIntN)-EVALUATE_SYM_BV(SymWordN)-EVALUATE_SYM_FUN((=->), (=~>), SymTabularFun)-EVALUATE_SYM_FUN((-->), (-~>), SymGeneralFun)-#endif--instance (ValidFP eb sb) => EvalSym (SymFP eb sb) where-  evalSym fillDefault model (SymFP t) =-    SymFP $ evalTerm fillDefault model HS.empty t---- Instances-deriveBuiltins-  (ViaDefault ''EvalSym)-  [''EvalSym]-  [ ''[],-    ''Maybe,-    ''Either,-    ''(),-    ''(,),-    ''(,,),-    ''(,,,),-    ''(,,,,),-    ''(,,,,,),-    ''(,,,,,,),-    ''(,,,,,,,),-    ''(,,,,,,,,),-    ''(,,,,,,,,,),-    ''(,,,,,,,,,,),-    ''(,,,,,,,,,,,),-    ''(,,,,,,,,,,,,),-    ''(,,,,,,,,,,,,,),-    ''(,,,,,,,,,,,,,,),-    ''AssertionError,-    ''VerificationConditions,-    ''NotRepresentableFPError,-    ''Identity,-    ''Monoid.Dual,-    ''Monoid.Sum,-    ''Monoid.Product,-    ''Monoid.First,-    ''Monoid.Last,-    ''Down-  ]--deriveBuiltins-  (ViaDefault1 ''EvalSym1)-  [''EvalSym, ''EvalSym1]-  [ ''[],-    ''Maybe,-    ''Either,-    ''(,),-    ''(,,),-    ''(,,,),-    ''(,,,,),-    ''(,,,,,),-    ''(,,,,,,),-    ''(,,,,,,,),-    ''(,,,,,,,,),-    ''(,,,,,,,,,),-    ''(,,,,,,,,,,),-    ''(,,,,,,,,,,,),-    ''(,,,,,,,,,,,,),-    ''(,,,,,,,,,,,,,),-    ''(,,,,,,,,,,,,,,),-    ''Identity,-    ''Monoid.Dual,-    ''Monoid.Sum,-    ''Monoid.Product,-    ''Monoid.First,-    ''Monoid.Last,-    ''Down-  ]---- ExceptT-instance-  (EvalSym1 m, EvalSym e, EvalSym a) =>-  EvalSym (ExceptT e m a)-  where-  evalSym = evalSym1-  {-# INLINE evalSym #-}--instance (EvalSym1 m, EvalSym e) => EvalSym1 (ExceptT e m) where-  liftEvalSym f fillDefault model =-    ExceptT . liftEvalSym (liftEvalSym f) fillDefault model . runExceptT-  {-# INLINE liftEvalSym #-}---- MaybeT-instance (EvalSym1 m, EvalSym a) => EvalSym (MaybeT m a) where-  evalSym = evalSym1-  {-# INLINE evalSym #-}--instance (EvalSym1 m) => EvalSym1 (MaybeT m) where-  liftEvalSym f fillDefault model =-    MaybeT . liftEvalSym (liftEvalSym f) fillDefault model . runMaybeT-  {-# INLINE liftEvalSym #-}---- WriterT-instance-  (EvalSym1 m, EvalSym s, EvalSym a) =>-  EvalSym (WriterLazy.WriterT s m a)-  where-  evalSym = evalSym1-  {-# INLINE evalSym #-}--instance-  (EvalSym1 m, EvalSym s) =>-  EvalSym1 (WriterLazy.WriterT s m)-  where-  liftEvalSym f fillDefault model =-    WriterLazy.WriterT-      . liftEvalSym (liftEvalSym2 f evalSym) fillDefault model-      . WriterLazy.runWriterT-  {-# INLINE liftEvalSym #-}--instance-  (EvalSym1 m, EvalSym s, EvalSym a) =>-  EvalSym (WriterStrict.WriterT s m a)-  where-  evalSym = evalSym1-  {-# INLINE evalSym #-}--instance-  (EvalSym1 m, EvalSym s) =>-  EvalSym1 (WriterStrict.WriterT s m)-  where-  liftEvalSym f fillDefault model =-    WriterStrict.WriterT-      . liftEvalSym (liftEvalSym2 f evalSym) fillDefault model-      . WriterStrict.runWriterT-  {-# INLINE liftEvalSym #-}---- IdentityT-instance (EvalSym1 m, EvalSym a) => EvalSym (IdentityT m a) where-  evalSym = evalSym1-  {-# INLINE evalSym #-}--instance (EvalSym1 m) => EvalSym1 (IdentityT m) where-  liftEvalSym f fillDefault model (IdentityT a) =-    IdentityT $ liftEvalSym f fillDefault model a-  {-# INLINE liftEvalSym #-}---- Product-deriving via-  (Default (Product l r a))-  instance-    (EvalSym (l a), EvalSym (r a)) => EvalSym (Product l r a)--deriving via-  (Default1 (Product l r))-  instance-    (EvalSym1 l, EvalSym1 r) => EvalSym1 (Product l r)---- Sum-deriving via-  (Default (Sum l r a))-  instance-    (EvalSym (l a), EvalSym (r a)) => EvalSym (Sum l r a)--deriving via-  (Default1 (Sum l r))-  instance-    (EvalSym1 l, EvalSym1 r) => EvalSym1 (Sum l r)---- Compose-deriving via-  (Default (Compose f g a))-  instance-    (EvalSym (f (g a))) => EvalSym (Compose f g a)--instance (EvalSym1 f, EvalSym1 g) => EvalSym1 (Compose f g) where-  liftEvalSym f fillDefault m (Compose l) =-    Compose $ liftEvalSym (liftEvalSym f) fillDefault m l-  {-# INLINE liftEvalSym #-}---- Const-deriving via (Default (Const a b)) instance (EvalSym a) => EvalSym (Const a b)--deriving via (Default1 (Const a)) instance (EvalSym a) => EvalSym1 (Const a)---- Alt-deriving via (Default (Alt f a)) instance (EvalSym (f a)) => EvalSym (Alt f a)--deriving via (Default1 (Alt f)) instance (EvalSym1 f) => EvalSym1 (Alt f)---- Ap-deriving via (Default (Ap f a)) instance (EvalSym (f a)) => EvalSym (Ap f a)--deriving via (Default1 (Ap f)) instance (EvalSym1 f) => EvalSym1 (Ap f)---- Generic-deriving via (Default (U1 p)) instance EvalSym (U1 p)--deriving via (Default (V1 p)) instance EvalSym (V1 p)--deriving via-  (Default (K1 i c p))-  instance-    (EvalSym c) => EvalSym (K1 i c p)--deriving via-  (Default (M1 i c f p))-  instance-    (EvalSym (f p)) => EvalSym (M1 i c f p)--deriving via-  (Default ((f :+: g) p))-  instance-    (EvalSym (f p), EvalSym (g p)) => EvalSym ((f :+: g) p)--deriving via-  (Default ((f :*: g) p))-  instance-    (EvalSym (f p), EvalSym (g p)) => EvalSym ((f :*: g) p)--deriving via-  (Default (Par1 p))-  instance-    (EvalSym p) => EvalSym (Par1 p)--deriving via-  (Default (Rec1 f p))-  instance-    (EvalSym (f p)) => EvalSym (Rec1 f p)--deriving via-  (Default ((f :.: g) p))-  instance-    (EvalSym (f (g p))) => EvalSym ((f :.: g) p)--instance EvalSym2 Either where-  liftEvalSym2 f _ fillDefault model (Left a) = Left $ f fillDefault model a-  liftEvalSym2 _ g fillDefault model (Right a) =-    Right $ g fillDefault model a-  {-# INLINE liftEvalSym2 #-}--instance EvalSym2 (,) where-  liftEvalSym2 f g fillDefault model (a, b) =-    (f fillDefault model a, g fillDefault model b)-  {-# INLINE liftEvalSym2 #-}--instance (EvalSym a) => EvalSym2 ((,,) a) where-  liftEvalSym2 f g fillDefault model (a, b, c) =-    ( evalSym fillDefault model a,-      f fillDefault model b,-      g fillDefault model c-    )-  {-# INLINE liftEvalSym2 #-}--instance (EvalSym a, EvalSym b) => EvalSym2 ((,,,) a b) where-  liftEvalSym2 f g fillDefault model (a, b, c, d) =-    ( evalSym fillDefault model a,-      evalSym fillDefault model b,-      f fillDefault model c,-      g fillDefault model d-    )-  {-# INLINE liftEvalSym2 #-}--instance (EvalSym a, EvalSym b) => EvalSym (a =-> b) where-  evalSym fillDefault model (TabularFun s t) =-    TabularFun-      (evalSym fillDefault model s)-      (evalSym fillDefault model t)--instance (EvalSym (SymType b)) => EvalSym (a --> b) where-  evalSym fillDefault model (GeneralFun s t) =-    GeneralFun s $-      evalTerm fillDefault model (HS.singleton $ someTypedSymbol s) t+import Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym+import Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym ()

@@ -1,20 +1,4 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DerivingVia #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE QuantifiedConstraints #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE Trustworthy #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-missing-import-lists #-}  -- | -- Module      :   Grisette.Internal.Core.Data.Class.ExtractSym@@ -42,641 +26,5 @@   ) where -import Control.Monad.Except (ExceptT (ExceptT))-import Control.Monad.Identity-  ( Identity (Identity),-    IdentityT (IdentityT),-  )-import Control.Monad.Trans.Maybe (MaybeT (MaybeT))-import qualified Control.Monad.Writer.Lazy as WriterLazy-import qualified Control.Monad.Writer.Strict as WriterStrict-import qualified Data.ByteString as B-import Data.Functor.Compose (Compose (Compose))-import Data.Functor.Const (Const)-import Data.Functor.Product (Product)-import Data.Functor.Sum (Sum)-import qualified Data.HashSet as HS-import Data.Int (Int16, Int32, Int64, Int8)-import Data.Kind (Type)-import Data.Maybe (fromJust)-import Data.Monoid (Alt, Ap)-import qualified Data.Monoid as Monoid-import Data.Ord (Down)-import Data.Ratio (Ratio, denominator, numerator)-import qualified Data.Text as T-import Data.Typeable (type (:~~:) (HRefl))-import Data.Word (Word16, Word32, Word64, Word8)-import GHC.TypeNats (KnownNat, type (<=))-import Generics.Deriving-  ( Default (Default, unDefault),-    Default1 (Default1, unDefault1),-    Generic (Rep, from),-    Generic1 (Rep1, from1),-    K1 (K1),-    M1 (M1),-    Par1 (Par1),-    Rec1 (Rec1),-    U1,-    V1,-    type (:*:) ((:*:)),-    type (:+:) (L1, R1),-    type (:.:) (Comp1),-  )-import Grisette.Internal.Core.Control.Exception-  ( AssertionError,-    VerificationConditions,-  )-import Grisette.Internal.SymPrim.AlgReal (AlgReal)-import Grisette.Internal.SymPrim.BV (IntN, WordN)-import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, NotRepresentableFPError, ValidFP)-import Grisette.Internal.SymPrim.GeneralFun (type (-->) (GeneralFun))-import Grisette.Internal.SymPrim.Prim.Model-  ( AnySymbolSet,-    SymbolSet (SymbolSet),-  )-import Grisette.Internal.SymPrim.Prim.Term-  ( IsSymbolKind (decideSymbolKind),-    SymRep (SymType),-    SymbolKind,-    someTypedSymbol,-  )-import Grisette.Internal.SymPrim.Prim.TermUtils (extractTerm)-import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal))-import Grisette.Internal.SymPrim.SymBV-  ( SymIntN (SymIntN),-    SymWordN (SymWordN),-  )-import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))-import Grisette.Internal.SymPrim.SymFP-  ( SymFP (SymFP),-    SymFPRoundingMode (SymFPRoundingMode),-  )-import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>) (SymGeneralFun))-import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))-import Grisette.Internal.SymPrim.SymTabularFun (type (=~>) (SymTabularFun))-import Grisette.Internal.SymPrim.TabularFun (type (=->) (TabularFun))-import Grisette.Internal.TH.DeriveBuiltin (deriveBuiltins)-import Grisette.Internal.TH.DeriveInstanceProvider-  ( Strategy (ViaDefault, ViaDefault1),-  )-import Grisette.Internal.Utils.Derive (Arity0, Arity1)---- $setup--- >>> import Grisette.Core--- >>> import Grisette.SymPrim--- >>> import Grisette.Lib.Base--- >>> import Data.HashSet as HashSet--- >>> import Data.List (sort)---- | Extracts all the symbols (symbolic constants) that are transitively--- contained in the given value.------ >>> extractSym ("a" :: SymBool)--- SymbolSet {a :: Bool}------ >>> extractSym (mrgIf "a" (mrgReturn ["b"]) (mrgReturn ["c", "d"]) :: Union [SymBool])--- SymbolSet {a :: Bool, b :: Bool, c :: Bool, d :: Bool}------ __Note 1:__ This type class can be derived for algebraic data types.--- You may need the @DerivingVia@ and @DerivingStrategies@ extensions.------ > data X = ... deriving Generic deriving ExtractSym via (Default X)-class ExtractSym a where-  extractSym :: a -> AnySymbolSet-  extractSym = fromJust . extractSymMaybe-  {-# INLINE extractSym #-}-  extractSymMaybe :: (IsSymbolKind knd) => a -> Maybe (SymbolSet knd)---- | Lifting of 'ExtractSym' to unary type constructors.-class-  (forall a. (ExtractSym a) => ExtractSym (f a)) =>-  ExtractSym1 f-  where-  -- | Lifts the 'extractSymMaybe' function to unary type constructors.-  liftExtractSymMaybe ::-    (IsSymbolKind knd) =>-    (a -> Maybe (SymbolSet knd)) ->-    f a ->-    Maybe (SymbolSet knd)---- | Lift the standard 'extractSym' to unary type constructors.-extractSym1 ::-  (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) =>-  f a ->-  SymbolSet knd-extractSym1 = fromJust . liftExtractSymMaybe extractSymMaybe-{-# INLINE extractSym1 #-}---- | Lift the standard 'extractSymMaybe' to unary type constructors.-extractSymMaybe1 ::-  (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) =>-  f a ->-  Maybe (SymbolSet knd)-extractSymMaybe1 = liftExtractSymMaybe extractSymMaybe-{-# INLINE extractSymMaybe1 #-}---- | Lifting of 'ExtractSym' to binary type constructors.-class-  (forall a. (ExtractSym a) => ExtractSym1 (f a)) =>-  ExtractSym2 f-  where-  -- | Lifts the 'extractSymMaybe' function to binary type constructors.-  liftExtractSymMaybe2 ::-    (IsSymbolKind knd) =>-    (a -> Maybe (SymbolSet knd)) ->-    (b -> Maybe (SymbolSet knd)) ->-    f a b ->-    Maybe (SymbolSet knd)---- | Lift the standard 'extractSym' to binary type constructors.-extractSym2 ::-  (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) =>-  f a b ->-  SymbolSet knd-extractSym2 = fromJust . liftExtractSymMaybe2 extractSymMaybe extractSymMaybe---- | Lift the standard 'extractSymMaybe' to binary type constructors.-extractSymMaybe2 ::-  (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) =>-  f a b ->-  Maybe (SymbolSet knd)-extractSymMaybe2 = liftExtractSymMaybe2 extractSymMaybe extractSymMaybe-{-# INLINE extractSymMaybe2 #-}---- Derivations---- | The arguments to the generic 'extractSym' function.-data family ExtractSymArgs arity (knd :: SymbolKind) a :: Type--data instance ExtractSymArgs Arity0 _ _ = ExtractSymArgs0--newtype instance ExtractSymArgs Arity1 knd a-  = ExtractSymArgs1 (a -> Maybe (SymbolSet knd))---- | The class of types that can generically extract the symbols.-class GExtractSym arity f where-  gextractSymMaybe ::-    (IsSymbolKind knd) =>-    ExtractSymArgs arity knd a ->-    f a ->-    Maybe (SymbolSet knd)--instance GExtractSym arity V1 where-  gextractSymMaybe _ _ = Just mempty-  {-# INLINE gextractSymMaybe #-}--instance GExtractSym arity U1 where-  gextractSymMaybe _ _ = Just mempty-  {-# INLINE gextractSymMaybe #-}--instance (GExtractSym arity a) => GExtractSym arity (M1 i c a) where-  gextractSymMaybe args (M1 x) = gextractSymMaybe args x-  {-# INLINE gextractSymMaybe #-}--instance (ExtractSym a) => GExtractSym arity (K1 i a) where-  gextractSymMaybe _ (K1 x) = extractSymMaybe x-  {-# INLINE gextractSymMaybe #-}--instance-  (GExtractSym arity a, GExtractSym arity b) =>-  GExtractSym arity (a :+: b)-  where-  gextractSymMaybe args (L1 x) = gextractSymMaybe args x-  gextractSymMaybe args (R1 x) = gextractSymMaybe args x-  {-# INLINE gextractSymMaybe #-}--instance-  (GExtractSym arity a, GExtractSym arity b) =>-  GExtractSym arity (a :*: b)-  where-  gextractSymMaybe args (x :*: y) =-    gextractSymMaybe args x <> gextractSymMaybe args y-  {-# INLINE gextractSymMaybe #-}--instance GExtractSym Arity1 Par1 where-  gextractSymMaybe (ExtractSymArgs1 f) (Par1 x) = f x-  {-# INLINE gextractSymMaybe #-}--instance (ExtractSym1 a) => GExtractSym Arity1 (Rec1 a) where-  gextractSymMaybe (ExtractSymArgs1 f) (Rec1 x) =-    liftExtractSymMaybe f x-  {-# INLINE gextractSymMaybe #-}--instance-  (ExtractSym1 f, GExtractSym Arity1 g) =>-  GExtractSym Arity1 (f :.: g)-  where-  gextractSymMaybe targs (Comp1 x) =-    liftExtractSymMaybe (gextractSymMaybe targs) x-  {-# INLINE gextractSymMaybe #-}---- | Generic 'extractSym' function.-genericExtractSymMaybe ::-  (Generic a, GExtractSym Arity0 (Rep a), IsSymbolKind knd) =>-  a ->-  Maybe (SymbolSet knd)-genericExtractSymMaybe = gextractSymMaybe ExtractSymArgs0 . from---- | Generic 'liftExtractSymMaybe' function.-genericLiftExtractSymMaybe ::-  (Generic1 f, GExtractSym Arity1 (Rep1 f), IsSymbolKind knd) =>-  (a -> Maybe (SymbolSet knd)) ->-  f a ->-  Maybe (SymbolSet knd)-genericLiftExtractSymMaybe f =-  gextractSymMaybe (ExtractSymArgs1 f) . from1--instance-  (Generic a, GExtractSym Arity0 (Rep a)) =>-  ExtractSym (Default a)-  where-  extractSymMaybe = genericExtractSymMaybe . unDefault-  {-# INLINE extractSymMaybe #-}--instance-  (Generic1 f, GExtractSym Arity1 (Rep1 f), ExtractSym a) =>-  ExtractSym (Default1 f a)-  where-  extractSymMaybe = extractSymMaybe1-  {-# INLINE extractSymMaybe #-}--instance-  (Generic1 f, GExtractSym Arity1 (Rep1 f)) =>-  ExtractSym1 (Default1 f)-  where-  liftExtractSymMaybe f = genericLiftExtractSymMaybe f . unDefault1-  {-# INLINE liftExtractSymMaybe #-}--#define CONCRETE_EXTRACT_SYMBOLICS(type) \-instance ExtractSym type where \-  extractSymMaybe _ = return mempty--#define CONCRETE_EXTRACT_SYMBOLICS_BV(type) \-instance (KnownNat n, 1 <= n) => ExtractSym (type n) where \-  extractSymMaybe _ = return mempty--#if 1-CONCRETE_EXTRACT_SYMBOLICS(Bool)-CONCRETE_EXTRACT_SYMBOLICS(Integer)-CONCRETE_EXTRACT_SYMBOLICS(Char)-CONCRETE_EXTRACT_SYMBOLICS(Int)-CONCRETE_EXTRACT_SYMBOLICS(Int8)-CONCRETE_EXTRACT_SYMBOLICS(Int16)-CONCRETE_EXTRACT_SYMBOLICS(Int32)-CONCRETE_EXTRACT_SYMBOLICS(Int64)-CONCRETE_EXTRACT_SYMBOLICS(Word)-CONCRETE_EXTRACT_SYMBOLICS(Word8)-CONCRETE_EXTRACT_SYMBOLICS(Word16)-CONCRETE_EXTRACT_SYMBOLICS(Word32)-CONCRETE_EXTRACT_SYMBOLICS(Word64)-CONCRETE_EXTRACT_SYMBOLICS(Float)-CONCRETE_EXTRACT_SYMBOLICS(Double)-CONCRETE_EXTRACT_SYMBOLICS(B.ByteString)-CONCRETE_EXTRACT_SYMBOLICS(T.Text)-CONCRETE_EXTRACT_SYMBOLICS(FPRoundingMode)-CONCRETE_EXTRACT_SYMBOLICS(Monoid.All)-CONCRETE_EXTRACT_SYMBOLICS(Monoid.Any)-CONCRETE_EXTRACT_SYMBOLICS(Ordering)-CONCRETE_EXTRACT_SYMBOLICS_BV(WordN)-CONCRETE_EXTRACT_SYMBOLICS_BV(IntN)-CONCRETE_EXTRACT_SYMBOLICS(AlgReal)-#endif--instance (ExtractSym a) => ExtractSym (Ratio a) where-  extractSymMaybe a =-    extractSymMaybe (numerator a) <> extractSymMaybe (denominator a)-  {-# INLINE extractSymMaybe #-}--instance (ValidFP eb sb) => ExtractSym (FP eb sb) where-  extractSymMaybe _ = return mempty--#define EXTRACT_SYMBOLICS_SIMPLE(symtype) \-instance ExtractSym symtype where \-  extractSymMaybe :: \-    forall knd. (IsSymbolKind knd) => symtype -> Maybe (SymbolSet knd); \-  extractSymMaybe (symtype t) = \-    case decideSymbolKind @knd of\-      Left HRefl -> SymbolSet <$> extractTerm HS.empty t; \-      Right HRefl -> SymbolSet <$> extractTerm HS.empty t--#define EXTRACT_SYMBOLICS_BV(symtype) \-instance (KnownNat n, 1 <= n) => ExtractSym (symtype n) where \-  extractSymMaybe :: \-    forall knd. (IsSymbolKind knd) => symtype n -> Maybe (SymbolSet knd); \-  extractSymMaybe (symtype t) = \-    case decideSymbolKind @knd of\-      Left HRefl -> SymbolSet <$> extractTerm HS.empty t; \-      Right HRefl -> SymbolSet <$> extractTerm HS.empty t--#define EXTRACT_SYMBOLICS_FUN(op, cons) \-instance ExtractSym (op sa sb) where \-  extractSymMaybe :: \-    forall knd. (IsSymbolKind knd) => op sa sb -> Maybe (SymbolSet knd); \-  extractSymMaybe (cons t) = \-    case decideSymbolKind @knd of \-      Left HRefl -> Nothing; \-      Right HRefl -> SymbolSet <$> extractTerm HS.empty t--#if 1-EXTRACT_SYMBOLICS_SIMPLE(SymBool)-EXTRACT_SYMBOLICS_SIMPLE(SymInteger)-EXTRACT_SYMBOLICS_SIMPLE(SymFPRoundingMode)-EXTRACT_SYMBOLICS_SIMPLE(SymAlgReal)-EXTRACT_SYMBOLICS_BV(SymIntN)-EXTRACT_SYMBOLICS_BV(SymWordN)-EXTRACT_SYMBOLICS_FUN((=~>), SymTabularFun)-EXTRACT_SYMBOLICS_FUN((-~>), SymGeneralFun)-#endif--instance (ValidFP eb fb) => ExtractSym (SymFP eb fb) where-  extractSymMaybe ::-    forall knd. (IsSymbolKind knd) => SymFP eb fb -> Maybe (SymbolSet knd)-  extractSymMaybe (SymFP t) =-    case decideSymbolKind @knd of-      Left HRefl -> SymbolSet <$> extractTerm HS.empty t-      Right HRefl -> SymbolSet <$> extractTerm HS.empty t---- Instances-deriveBuiltins-  (ViaDefault ''ExtractSym)-  [''ExtractSym]-  [ ''[],-    ''Maybe,-    ''Either,-    ''(),-    ''(,),-    ''(,,),-    ''(,,,),-    ''(,,,,),-    ''(,,,,,),-    ''(,,,,,,),-    ''(,,,,,,,),-    ''(,,,,,,,,),-    ''(,,,,,,,,,),-    ''(,,,,,,,,,,),-    ''(,,,,,,,,,,,),-    ''(,,,,,,,,,,,,),-    ''(,,,,,,,,,,,,,),-    ''(,,,,,,,,,,,,,,),-    ''AssertionError,-    ''VerificationConditions,-    ''NotRepresentableFPError,-    ''Identity,-    ''Monoid.Dual,-    ''Monoid.Sum,-    ''Monoid.Product,-    ''Monoid.First,-    ''Monoid.Last,-    ''Down-  ]--deriveBuiltins-  (ViaDefault1 ''ExtractSym1)-  [''ExtractSym, ''ExtractSym1]-  [ ''[],-    ''Maybe,-    ''Either,-    ''(,),-    ''(,,),-    ''(,,,),-    ''(,,,,),-    ''(,,,,,),-    ''(,,,,,,),-    ''(,,,,,,,),-    ''(,,,,,,,,),-    ''(,,,,,,,,,),-    ''(,,,,,,,,,,),-    ''(,,,,,,,,,,,),-    ''(,,,,,,,,,,,,),-    ''(,,,,,,,,,,,,,),-    ''(,,,,,,,,,,,,,,),-    ''Identity,-    ''Monoid.Dual,-    ''Monoid.Sum,-    ''Monoid.Product,-    ''Monoid.First,-    ''Monoid.Last,-    ''Down-  ]---- ExceptT-instance-  (ExtractSym1 m, ExtractSym e, ExtractSym a) =>-  ExtractSym (ExceptT e m a)-  where-  extractSymMaybe = extractSymMaybe1-  {-# INLINE extractSymMaybe #-}--instance-  (ExtractSym1 m, ExtractSym e) =>-  ExtractSym1 (ExceptT e m)-  where-  liftExtractSymMaybe f (ExceptT v) =-    liftExtractSymMaybe (liftExtractSymMaybe f) v-  {-# INLINE liftExtractSymMaybe #-}---- MaybeT-instance-  (ExtractSym1 m, ExtractSym a) =>-  ExtractSym (MaybeT m a)-  where-  extractSymMaybe = extractSymMaybe1-  {-# INLINE extractSymMaybe #-}--instance-  (ExtractSym1 m) =>-  ExtractSym1 (MaybeT m)-  where-  liftExtractSymMaybe f (MaybeT v) =-    liftExtractSymMaybe (liftExtractSymMaybe f) v-  {-# INLINE liftExtractSymMaybe #-}---- WriterT-instance-  (ExtractSym1 m, ExtractSym w, ExtractSym a) =>-  ExtractSym (WriterLazy.WriterT w m a)-  where-  extractSymMaybe = extractSymMaybe1-  {-# INLINE extractSymMaybe #-}--instance-  (ExtractSym1 m, ExtractSym w) =>-  ExtractSym1 (WriterLazy.WriterT w m)-  where-  liftExtractSymMaybe f (WriterLazy.WriterT v) =-    liftExtractSymMaybe (liftExtractSymMaybe2 f extractSymMaybe) v-  {-# INLINE liftExtractSymMaybe #-}--instance-  (ExtractSym1 m, ExtractSym w, ExtractSym a) =>-  ExtractSym (WriterStrict.WriterT w m a)-  where-  extractSymMaybe = extractSymMaybe1-  {-# INLINE extractSymMaybe #-}--instance-  (ExtractSym1 m, ExtractSym w) =>-  ExtractSym1 (WriterStrict.WriterT w m)-  where-  liftExtractSymMaybe f (WriterStrict.WriterT v) =-    liftExtractSymMaybe (liftExtractSymMaybe2 f extractSymMaybe) v-  {-# INLINE liftExtractSymMaybe #-}---- IdentityT-instance-  (ExtractSym1 m, ExtractSym a) =>-  ExtractSym (IdentityT m a)-  where-  extractSymMaybe = extractSymMaybe1-  {-# INLINE extractSymMaybe #-}--instance (ExtractSym1 m) => ExtractSym1 (IdentityT m) where-  liftExtractSymMaybe f (IdentityT v) = liftExtractSymMaybe f v-  {-# INLINE liftExtractSymMaybe #-}---- Product-deriving via-  (Default (Product l r a))-  instance-    (ExtractSym (l a), ExtractSym (r a)) =>-    ExtractSym (Product l r a)--deriving via-  (Default1 (Product l r))-  instance-    (ExtractSym1 l, ExtractSym1 r) =>-    ExtractSym1 (Product l r)---- Sum-deriving via-  (Default (Sum l r a))-  instance-    (ExtractSym (l a), ExtractSym (r a)) =>-    ExtractSym (Sum l r a)--deriving via-  (Default1 (Sum l r))-  instance-    (ExtractSym1 l, ExtractSym1 r) => ExtractSym1 (Sum l r)---- Compose-deriving via-  (Default (Compose f g a))-  instance-    (ExtractSym (f (g a))) => ExtractSym (Compose f g a)--instance-  (ExtractSym1 f, ExtractSym1 g) =>-  ExtractSym1 (Compose f g)-  where-  liftExtractSymMaybe f (Compose l) =-    liftExtractSymMaybe (liftExtractSymMaybe f) l-  {-# INLINE liftExtractSymMaybe #-}---- Const-deriving via-  (Default (Const a b))-  instance-    (ExtractSym a) => ExtractSym (Const a b)--deriving via-  (Default1 (Const a))-  instance-    (ExtractSym a) => ExtractSym1 (Const a)---- Alt-deriving via-  (Default (Alt f a))-  instance-    (ExtractSym (f a)) => ExtractSym (Alt f a)--deriving via-  (Default1 (Alt f))-  instance-    (ExtractSym1 f) => ExtractSym1 (Alt f)---- Ap-deriving via-  (Default (Ap f a))-  instance-    (ExtractSym (f a)) => ExtractSym (Ap f a)--deriving via-  (Default1 (Ap f))-  instance-    (ExtractSym1 f) => ExtractSym1 (Ap f)---- Generic-deriving via (Default (U1 p)) instance ExtractSym (U1 p)--deriving via (Default (V1 p)) instance ExtractSym (V1 p)--deriving via-  (Default (K1 i c p))-  instance-    (ExtractSym c) => ExtractSym (K1 i c p)--deriving via-  (Default (M1 i c f p))-  instance-    (ExtractSym (f p)) => ExtractSym (M1 i c f p)--deriving via-  (Default ((f :+: g) p))-  instance-    (ExtractSym (f p), ExtractSym (g p)) =>-    ExtractSym ((f :+: g) p)--deriving via-  (Default ((f :*: g) p))-  instance-    (ExtractSym (f p), ExtractSym (g p)) =>-    ExtractSym ((f :*: g) p)--deriving via-  (Default (Par1 p))-  instance-    (ExtractSym p) => ExtractSym (Par1 p)--deriving via-  (Default (Rec1 f p))-  instance-    (ExtractSym (f p)) => ExtractSym (Rec1 f p)--deriving via-  (Default ((f :.: g) p))-  instance-    (ExtractSym (f (g p))) => ExtractSym ((f :.: g) p)---- ExtractSym2-instance ExtractSym2 Either where-  liftExtractSymMaybe2 f _ (Left x) = f x-  liftExtractSymMaybe2 _ g (Right y) = g y-  {-# INLINE liftExtractSymMaybe2 #-}--instance ExtractSym2 (,) where-  liftExtractSymMaybe2 f g (x, y) = f x <> g y-  {-# INLINE liftExtractSymMaybe2 #-}--instance (ExtractSym a) => ExtractSym2 ((,,) a) where-  liftExtractSymMaybe2 f g (x, y, z) = extractSymMaybe x <> f y <> g z-  {-# INLINE liftExtractSymMaybe2 #-}--instance-  (ExtractSym a, ExtractSym b) =>-  ExtractSym2 ((,,,) a b)-  where-  liftExtractSymMaybe2 f g (x, y, z, w) =-    extractSymMaybe x <> extractSymMaybe y <> f z <> g w-  {-# INLINE liftExtractSymMaybe2 #-}--instance (ExtractSym a, ExtractSym b) => ExtractSym (a =-> b) where-  extractSymMaybe (TabularFun s t) =-    extractSymMaybe s <> extractSymMaybe t--instance (ExtractSym (SymType b)) => ExtractSym (a --> b) where-  extractSymMaybe :: forall knd. (IsSymbolKind knd) => (a --> b) -> Maybe (SymbolSet knd)-  extractSymMaybe (GeneralFun t f) =-    case decideSymbolKind @knd of-      Left HRefl -> Nothing-      Right HRefl -> SymbolSet <$> extractTerm (HS.singleton $ someTypedSymbol t) f+import Grisette.Internal.Internal.Decl.Core.Data.Class.ExtractSym+import Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym ()

@@ -132,7 +132,7 @@     tryMerge,   ) import Grisette.Internal.Core.Data.Symbol (Identifier)-import Grisette.Internal.Core.Data.UnionBase+import Grisette.Internal.Internal.Decl.Core.Data.UnionBase   ( UnionBase (UnionIf, UnionSingle),   ) import Grisette.Internal.SymPrim.BV (IntN, WordN)

@@ -21,9 +21,14 @@  import Control.Monad.Identity (Identity (Identity)) import qualified Data.HashSet as HS+import Data.Proxy (Proxy) import GHC.TypeNats (KnownNat, type (<=)) import Grisette.Internal.SymPrim.FP (ValidFP)-import Grisette.Internal.SymPrim.GeneralFun (freshArgSymbol, substTerm, type (-->) (GeneralFun))+import Grisette.Internal.SymPrim.GeneralFun+  ( freshArgSymbol,+    substTerm,+    type (-->) (GeneralFun),+  ) import Grisette.Internal.SymPrim.Prim.SomeTerm (SomeTerm (SomeTerm)) import Grisette.Internal.SymPrim.Prim.Term   ( SupportedPrim (pevalITETerm),@@ -108,4 +113,8 @@  instance (ITEOp v) => ITEOp (Identity v) where   symIte c (Identity t) (Identity f) = Identity $ symIte c t f+  {-# INLINE symIte #-}++instance ITEOp (Proxy a) where+  symIte _ l _ = l   {-# INLINE symIte #-}

@@ -1,1187 +1,43 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DerivingVia #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE QuantifiedConstraints #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE Trustworthy #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}---- |--- Module      :   Grisette.Internal.Core.Data.Class.Mergeable--- Copyright   :   (c) Sirui Lu 2021-2023--- License     :   BSD-3-Clause (see the LICENSE file)------ Maintainer  :   siruilu@cs.washington.edu--- Stability   :   Experimental--- Portability :   GHC only-module Grisette.Internal.Core.Data.Class.Mergeable-  ( -- * Merging strategy-    MergingStrategy (..),--    -- * Mergeable-    Mergeable (..),-    Mergeable1 (..),-    rootStrategy1,-    Mergeable2 (..),-    rootStrategy2,-    Mergeable3 (..),-    rootStrategy3,--    -- * Generic 'Mergeable'-    MergeableArgs (..),-    GMergeable (..),-    genericRootStrategy,-    genericLiftRootStrategy,--    -- * Combinators for manually building merging strategies-    wrapStrategy,-    product2Strategy,-    DynamicSortedIdx (..),-    StrategyList (..),-    buildStrategyList,-    resolveStrategy,-    resolveStrategy',-    resolveMergeable1,-  )-where--import Control.Exception-  ( ArithException-      ( Denormal,-        DivideByZero,-        LossOfPrecision,-        Overflow,-        RatioZeroDenominator,-        Underflow-      ),-  )-import Control.Monad.Cont (ContT (ContT))-import Control.Monad.Except (ExceptT (ExceptT), runExceptT)-import Control.Monad.Identity-  ( Identity (Identity),-    IdentityT (IdentityT, runIdentityT),-  )-import qualified Control.Monad.RWS.Lazy as RWSLazy-import qualified Control.Monad.RWS.Strict as RWSStrict-import Control.Monad.Reader (ReaderT (ReaderT, runReaderT))-import qualified Control.Monad.State.Lazy as StateLazy-import qualified Control.Monad.State.Strict as StateStrict-import Control.Monad.Trans.Maybe (MaybeT (MaybeT, runMaybeT))-import qualified Control.Monad.Writer.Lazy as WriterLazy-import qualified Control.Monad.Writer.Strict as WriterStrict-import qualified Data.ByteString as B-import Data.Functor.Classes-  ( Eq1,-    Ord1,-    Show1,-    compare1,-    eq1,-    showsPrec1,-  )-import Data.Functor.Compose (Compose (Compose, getCompose))-import Data.Functor.Const (Const)-import Data.Functor.Product (Product)-import Data.Functor.Sum (Sum)-import Data.Int (Int16, Int32, Int64, Int8)-import Data.Kind (Type)-import Data.Monoid (Alt, Ap, Endo (Endo, appEndo))-import qualified Data.Monoid as Monoid-import Data.Ord (Down)-import Data.Ratio (Ratio)-import qualified Data.Text as T-import Data.Typeable-  ( Typeable,-    eqT,-    type (:~:) (Refl),-  )-import Data.Word (Word16, Word32, Word64, Word8)-import GHC.TypeNats (KnownNat, type (+), type (<=))-import Generics.Deriving-  ( Default (Default),-    Default1 (Default1),-    Generic (Rep, from, to),-    Generic1 (Rep1, from1, to1),-    K1 (K1, unK1),-    M1 (M1, unM1),-    Par1 (Par1, unPar1),-    Rec1 (Rec1, unRec1),-    U1,-    V1,-    (:.:) (Comp1, unComp1),-    type (:*:) ((:*:)),-    type (:+:) (L1, R1),-  )-import Grisette.Internal.Core.Control.Exception-  ( AssertionError,-    VerificationConditions,-  )-import Grisette.Internal.Core.Data.Class.BitCast (bitCastOrCanonical)-import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))-import Grisette.Internal.SymPrim.AlgReal (AlgReal, AlgRealPoly, RealPoint)-import Grisette.Internal.SymPrim.BV-  ( IntN,-    WordN,-  )-import Grisette.Internal.SymPrim.FP-  ( FP,-    FPRoundingMode,-    NotRepresentableFPError,-    ValidFP,-    withValidFPProofs,-  )-import Grisette.Internal.SymPrim.GeneralFun (type (-->))-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, SymFPRoundingMode)-import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>))-import Grisette.Internal.SymPrim.SymInteger (SymInteger)-import Grisette.Internal.SymPrim.SymTabularFun (type (=~>))-import Grisette.Internal.SymPrim.TabularFun (type (=->))-import Grisette.Internal.TH.DeriveBuiltin (deriveBuiltins)-import Grisette.Internal.TH.DeriveInstanceProvider-  ( Strategy (ViaDefault, ViaDefault1),-  )-import Grisette.Internal.Utils.Derive (Arity0, Arity1)-import Unsafe.Coerce (unsafeCoerce)---- | Merging strategies.------ __You probably do not need to know the details of this type if you are only__--- __going to use algebraic data types. You can get merging strategies for__--- __them with type derivation.__------ In Grisette, a merged union (if-then-else tree) follows the--- __/hierarchical sorted representation invariant/__ with regards to some--- merging strategy.------ A merging strategy encodes how to merge a __/subset/__ of the values of a--- given type. We have three types of merging strategies:------ * Simple strategy--- * Sorted strategy--- * No strategy------ The 'SimpleStrategy' merges values with a simple merge function.--- For example,------    * the symbolic boolean values can be directly merged with 'symIte'.------    * the set @{1}@, which is a subset of the values of the type @Integer@,---        can be simply merged as the set contains only a single value.------    * all the 'Just' values of the type @Maybe SymBool@ can be simply merged---        by merging the wrapped symbolic boolean with 'symIte'.------ The 'SortedStrategy' merges values by first grouping the values with an--- indexing function, and the values with the same index will be organized as--- a sub-tree in the if-then-else structure of--- 'Grisette.Core.Data.UnionBase.UnionBase'. Each group (sub-tree) will be--- further merged with a sub-strategy for the index.--- The index type should be a totally ordered type (with the 'Ord'--- type class). Grisette will use the indexing function to partition the values--- into sub-trees, and organize them in a sorted way. The sub-trees will further--- be merged with the sub-strategies. For example,------    * all the integers can be merged with 'SortedStrategy' by indexing with---      the identity function and use the 'SimpleStrategy' shown before as the---      sub-strategies.------    * all the @Maybe SymBool@ values can be merged with 'SortedStrategy' by---      indexing with 'Data.Maybe.isJust', the 'Nothing' and 'Just' values can---      then be merged with different simple strategies as sub-strategies.------ The 'NoStrategy' does not perform any merging.--- For example, we cannot merge values with function types that returns concrete--- lists.------ For ADTs, we can automatically derive the 'Mergeable' type class, which--- provides a merging strategy.------ If the derived version does not work for you, you should determine--- if your type can be directly merged with a merging function. If so, you can--- implement the merging strategy as a 'SimpleStrategy'.--- If the type cannot be directly merged with a merging function, but could be--- partitioned into subsets of values that can be simply merged with a function,--- you should implement the merging strategy as a 'SortedStrategy'.--- For easier building of the merging strategies, check out the combinators--- like `wrapStrategy`.------ For more details, please see the documents of the constructors, or refer to--- [Grisette's paper](https://lsrcz.github.io/files/POPL23.pdf).-data MergingStrategy a where-  -- | Simple mergeable strategy.-  ---  -- For symbolic booleans, we can implement its merge strategy as follows:-  ---  -- > SimpleStrategy symIte :: MergingStrategy SymBool-  SimpleStrategy ::-    -- | Merge function.-    (SymBool -> a -> a -> a) ->-    MergingStrategy a-  -- | Sorted mergeable strategy.-  ---  -- For Integers, we can implement its merge strategy as follows:-  ---  -- > SortedStrategy id (\_ -> SimpleStrategy $ \_ t _ -> t)-  ---  -- For @Maybe SymBool@, we can implement its merge strategy as follows:-  ---  -- > SortedStrategy-  -- >   (\case; Nothing -> False; Just _ -> True)-  -- >   (\idx ->-  -- >      if idx-  -- >        then SimpleStrategy $ \_ t _ -> t-  -- >        else SimpleStrategy $ \cond (Just l) (Just r) -> Just $ symIte cond l r)-  SortedStrategy ::-    (Ord idx, Typeable idx, Show idx) =>-    -- | Indexing function-    (a -> idx) ->-    -- | Sub-strategy function-    (idx -> MergingStrategy a) ->-    MergingStrategy a-  -- | For preventing the merging intentionally. This could be-  -- useful for keeping some value concrete and may help generate more efficient-  -- formulas.-  ---  -- See [Grisette's paper](https://lsrcz.github.io/files/POPL23.pdf) for-  -- details.-  NoStrategy :: MergingStrategy a---- | Each type is associated with a root merge strategy given by 'rootStrategy'.--- The root merge strategy should be able to merge every value of the type.--- Grisette will use the root merge strategy to merge the values of the type in--- a union.------ __Note 1:__ This type class can be derived for algebraic data types.--- You may need the @DerivingVia@ and @DerivingStrategies@ extensions.------ > data X = ... deriving Generic deriving Mergeable via (Default X)-class Mergeable a where-  -- | The root merging strategy for the type.-  rootStrategy :: MergingStrategy a---- | Lifting of the 'Mergeable' class to unary type constructors.-class-  (forall a. (Mergeable a) => Mergeable (u a)) =>-  Mergeable1 (u :: Type -> Type)-  where-  -- | Lift merge strategy through the type constructor.-  liftRootStrategy :: MergingStrategy a -> MergingStrategy (u a)---- | Lift the root merge strategy through the unary type constructor.-rootStrategy1 :: (Mergeable a, Mergeable1 u) => MergingStrategy (u a)-rootStrategy1 = liftRootStrategy rootStrategy-{-# INLINE rootStrategy1 #-}---- | Workaround as GHC prior to 9.6 doesn't support quantified constraints--- reliably.------ Similar to https://github.com/haskell/core-libraries-committee/issues/10,--- which is only available with 9.6 or higher.-resolveMergeable1 ::-  forall f a r. (Mergeable1 f, Mergeable a) => ((Mergeable (f a)) => r) -> r-resolveMergeable1 v = v---- | Lifting of the 'Mergeable' class to binary type constructors.-class-  (forall a. (Mergeable a) => Mergeable1 (u a)) =>-  Mergeable2 (u :: Type -> Type -> Type)-  where-  -- | Lift merge strategy through the type constructor.-  liftRootStrategy2 ::-    MergingStrategy a ->-    MergingStrategy b ->-    MergingStrategy (u a b)---- | Lift the root merge strategy through the binary type constructor.-rootStrategy2 ::-  (Mergeable a, Mergeable b, Mergeable2 u) =>-  MergingStrategy (u a b)-rootStrategy2 = liftRootStrategy2 rootStrategy rootStrategy-{-# INLINE rootStrategy2 #-}---- | Lifting of the 'Mergeable' class to ternary type constructors.-class-  (forall a. (Mergeable a) => Mergeable2 (u a)) =>-  Mergeable3 (u :: Type -> Type -> Type -> Type)-  where-  -- | Lift merge strategy through the type constructor.-  liftRootStrategy3 ::-    MergingStrategy a ->-    MergingStrategy b ->-    MergingStrategy c ->-    MergingStrategy (u a b c)---- | Lift the root merge strategy through the binary type constructor.-rootStrategy3 ::-  (Mergeable a, Mergeable b, Mergeable c, Mergeable3 u) =>-  MergingStrategy (u a b c)-rootStrategy3 = liftRootStrategy3 rootStrategy rootStrategy rootStrategy-{-# INLINE rootStrategy3 #-}---- | Useful utility function for building merge strategies manually.------ For example, to build the merge strategy for the just branch of @Maybe a@,--- one could write------ > wrapStrategy Just fromMaybe rootStrategy :: MergingStrategy (Maybe a)-wrapStrategy ::-  -- | The merge strategy to be wrapped-  MergingStrategy a ->-  -- | The wrap function-  (a -> b) ->-  -- | The unwrap function, which does not have to be defined for every value-  (b -> a) ->-  MergingStrategy b-wrapStrategy (SimpleStrategy m) wrap unwrap =-  SimpleStrategy-    ( \cond ifTrue ifFalse ->-        wrap $ m cond (unwrap ifTrue) (unwrap ifFalse)-    )-wrapStrategy (SortedStrategy idxFun substrategy) wrap unwrap =-  SortedStrategy-    (idxFun . unwrap)-    (\idx -> wrapStrategy (substrategy idx) wrap unwrap)-wrapStrategy NoStrategy _ _ = NoStrategy-{-# INLINE wrapStrategy #-}---- | Useful utility function for building merge strategies for product types--- manually.------ For example, to build the merge strategy for the following product type,--- one could write------ > data X = X { x1 :: Int, x2 :: Bool }--- > product2Strategy X (\(X a b) -> (a, b)) rootStrategy rootStrategy--- >   :: MergingStrategy X-product2Strategy ::-  -- | The wrap function-  (a -> b -> r) ->-  -- | The unwrap function, which does not have to be defined for every value-  (r -> (a, b)) ->-  -- | The first merge strategy to be wrapped-  MergingStrategy a ->-  -- | The second merge strategy to be wrapped-  MergingStrategy b ->-  MergingStrategy r-product2Strategy wrap unwrap strategy1 strategy2 =-  case (strategy1, strategy2) of-    (NoStrategy, _) -> NoStrategy-    (_, NoStrategy) -> NoStrategy-    (SimpleStrategy m1, SimpleStrategy m2) ->-      SimpleStrategy $ \cond t f -> case (unwrap t, unwrap f) of-        ((hdt, tlt), (hdf, tlf)) ->-          wrap (m1 cond hdt hdf) (m2 cond tlt tlf)-    (s1@(SimpleStrategy _), SortedStrategy idxf subf) ->-      SortedStrategy-        (idxf . snd . unwrap)-        (product2Strategy wrap unwrap s1 . subf)-    (SortedStrategy idxf subf, s2) ->-      SortedStrategy-        (idxf . fst . unwrap)-        (\idx -> product2Strategy wrap unwrap (subf idx) s2)-{-# INLINE product2Strategy #-}---- Derivations---- | The arguments to the generic merging strategy function.-data family MergeableArgs arity a :: Type--data instance MergeableArgs Arity0 _ = MergeableArgs0--newtype instance MergeableArgs Arity1 a = MergeableArgs1 (MergingStrategy a)---- | The class of types that can be generically merged.-class GMergeable arity f where-  grootStrategy :: MergeableArgs arity a -> MergingStrategy (f a)--instance GMergeable arity V1 where-  grootStrategy _ = SimpleStrategy (\_ t _ -> t)-  {-# INLINE grootStrategy #-}--instance GMergeable arity U1 where-  grootStrategy _ = SimpleStrategy (\_ t _ -> t)-  {-# INLINE grootStrategy #-}--instance-  (GMergeable arity a, GMergeable arity b) =>-  GMergeable arity (a :*: b)-  where-  grootStrategy args =-    product2Strategy-      (:*:)-      (\(a :*: b) -> (a, b))-      (grootStrategy args)-      (grootStrategy args)-  {-# INLINE grootStrategy #-}--instance-  (GMergeable arity a, GMergeable arity b) =>-  GMergeable arity (a :+: b)-  where-  grootStrategy args =-    SortedStrategy-      ( \case-          L1 _ -> False-          R1 _ -> True-      )-      ( \idx ->-          if not idx-            then-              wrapStrategy-                (grootStrategy args)-                L1-                (\case (L1 v) -> v; _ -> error "Should not happen")-            else-              wrapStrategy-                (grootStrategy args)-                R1-                (\case (R1 v) -> v; _ -> error "Should not happen")-      )-  {-# INLINE grootStrategy #-}--instance (GMergeable arity a) => GMergeable arity (M1 i c a) where-  grootStrategy arg = wrapStrategy (grootStrategy arg) M1 unM1-  {-# INLINE grootStrategy #-}--instance (Mergeable c) => GMergeable arity (K1 i c) where-  grootStrategy _ = wrapStrategy rootStrategy K1 unK1-  {-# INLINE grootStrategy #-}--instance GMergeable Arity1 Par1 where-  grootStrategy (MergeableArgs1 strategy) = wrapStrategy strategy Par1 unPar1-  {-# INLINE grootStrategy #-}--instance (Mergeable1 f) => GMergeable Arity1 (Rec1 f) where-  grootStrategy (MergeableArgs1 m) =-    wrapStrategy (liftRootStrategy m) Rec1 unRec1-  {-# INLINE grootStrategy #-}--instance-  (Mergeable1 f, GMergeable Arity1 g) =>-  GMergeable Arity1 (f :.: g)-  where-  grootStrategy targs =-    wrapStrategy (liftRootStrategy (grootStrategy targs)) Comp1 unComp1-  {-# INLINE grootStrategy #-}--instance (Generic a, GMergeable Arity0 (Rep a)) => Mergeable (Default a) where-  rootStrategy = unsafeCoerce (genericRootStrategy :: MergingStrategy a)-  {-# INLINE rootStrategy #-}---- | Generic 'rootStrategy'.-genericRootStrategy ::-  (Generic a, GMergeable Arity0 (Rep a)) => MergingStrategy a-genericRootStrategy = wrapStrategy (grootStrategy MergeableArgs0) to from-{-# INLINE genericRootStrategy #-}--instance-  (Generic1 f, GMergeable Arity1 (Rep1 f), Mergeable a) =>-  Mergeable (Default1 f a)-  where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance (Generic1 f, GMergeable Arity1 (Rep1 f)) => Mergeable1 (Default1 f) where-  liftRootStrategy (m :: MergingStrategy a) =-    unsafeCoerce (genericLiftRootStrategy m :: MergingStrategy (f a))-  {-# INLINE liftRootStrategy #-}---- | Generic 'liftRootStrategy'.-genericLiftRootStrategy ::-  (Generic1 f, GMergeable Arity1 (Rep1 f)) =>-  MergingStrategy a ->-  MergingStrategy (f a)-genericLiftRootStrategy m =-  wrapStrategy (grootStrategy $ MergeableArgs1 m) to1 from1-{-# INLINE genericLiftRootStrategy #-}---- | Helper type for combining arbitrary number of indices into one.--- Useful when trying to write efficient merge strategy for lists/vectors.-data DynamicSortedIdx where-  DynamicSortedIdx :: forall idx. (Show idx, Ord idx, Typeable idx) => idx -> DynamicSortedIdx--instance Eq DynamicSortedIdx where-  (DynamicSortedIdx (a :: a)) == (DynamicSortedIdx (b :: b)) = case eqT @a @b of-    Just Refl -> a == b-    _ -> False-  {-# INLINE (==) #-}--instance Ord DynamicSortedIdx where-  compare (DynamicSortedIdx (a :: a)) (DynamicSortedIdx (b :: b)) = case eqT @a @b of-    Just Refl -> compare a b-    _ -> error "This Ord is incomplete"-  {-# INLINE compare #-}--instance Show DynamicSortedIdx where-  show (DynamicSortedIdx a) = show a---- | Resolves the indices and the terminal merge strategy for a value of some--- 'Mergeable' type.-resolveStrategy ::-  forall x.-  MergingStrategy x ->-  x ->-  ([DynamicSortedIdx], MergingStrategy x)-resolveStrategy s x = resolveStrategy' x s-{-# INLINE resolveStrategy #-}---- | Resolves the indices and the terminal merge strategy for a value given a--- merge strategy for its type.-resolveStrategy' ::-  forall x. x -> MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x)-resolveStrategy' x = go-  where-    go :: MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x)-    go (SortedStrategy idxFun subStrategy) = case go ss of-      (idxs, r) -> (DynamicSortedIdx idx : idxs, r)-      where-        idx = idxFun x-        ss = subStrategy idx-    go s = ([], s)-{-# INLINE resolveStrategy' #-}--#define CONCRETE_ORD_MERGEABLE(type) \-instance Mergeable type where \-  rootStrategy = \-    let sub = SimpleStrategy $ \_ t _ -> t \-     in SortedStrategy id $ const sub--#define CONCRETE_ORD_MERGEABLE_BV(type) \-instance (KnownNat n, 1 <= n) => Mergeable (type n) where \-  rootStrategy = \-    let sub = SimpleStrategy $ \_ t _ -> t \-     in SortedStrategy id $ const sub--#if 1-CONCRETE_ORD_MERGEABLE(Bool)-CONCRETE_ORD_MERGEABLE(Integer)-CONCRETE_ORD_MERGEABLE(Char)-CONCRETE_ORD_MERGEABLE(Int)-CONCRETE_ORD_MERGEABLE(Int8)-CONCRETE_ORD_MERGEABLE(Int16)-CONCRETE_ORD_MERGEABLE(Int32)-CONCRETE_ORD_MERGEABLE(Int64)-CONCRETE_ORD_MERGEABLE(Word)-CONCRETE_ORD_MERGEABLE(Word8)-CONCRETE_ORD_MERGEABLE(Word16)-CONCRETE_ORD_MERGEABLE(Word32)-CONCRETE_ORD_MERGEABLE(Word64)-CONCRETE_ORD_MERGEABLE(Float)-CONCRETE_ORD_MERGEABLE(Double)-CONCRETE_ORD_MERGEABLE(B.ByteString)-CONCRETE_ORD_MERGEABLE(T.Text)-CONCRETE_ORD_MERGEABLE(FPRoundingMode)-CONCRETE_ORD_MERGEABLE(Monoid.All)-CONCRETE_ORD_MERGEABLE(Monoid.Any)-CONCRETE_ORD_MERGEABLE(Ordering)-CONCRETE_ORD_MERGEABLE_BV(WordN)-CONCRETE_ORD_MERGEABLE_BV(IntN)-#endif--instance (Integral a, Typeable a, Show a) => Mergeable (Ratio a) where-  rootStrategy =-    let sub = SimpleStrategy $ \_ t _ -> t-     in SortedStrategy id $ const sub--instance (ValidFP eb sb) => Mergeable (FP eb sb) where-  rootStrategy =-    let sub = SimpleStrategy $ \_ t _ -> t-     in withValidFPProofs @eb @sb-          $ SortedStrategy-            (\fp -> (bitCastOrCanonical fp :: WordN (eb + sb)))-          $ const sub--instance Mergeable (a =-> b) where-  rootStrategy = NoStrategy--instance Mergeable (a --> b) where-  rootStrategy = SimpleStrategy symIte--#define MERGEABLE_SIMPLE(symtype) \-instance Mergeable symtype where \-  rootStrategy = SimpleStrategy symIte--#define MERGEABLE_BV(symtype) \-instance (KnownNat n, 1 <= n) => Mergeable (symtype n) where \-  rootStrategy = SimpleStrategy symIte--#define MERGEABLE_FUN(cop, op, consop) \-instance Mergeable (op sa sb) where \-  rootStrategy = SimpleStrategy symIte--#if 1-MERGEABLE_SIMPLE(SymBool)-MERGEABLE_SIMPLE(SymInteger)-MERGEABLE_SIMPLE(SymFPRoundingMode)-MERGEABLE_SIMPLE(SymAlgReal)-MERGEABLE_BV(SymIntN)-MERGEABLE_BV(SymWordN)-MERGEABLE_FUN((=->), (=~>), SymTabularFun)-MERGEABLE_FUN((-->), (-~>), SymGeneralFun)-#endif--instance (ValidFP eb sb) => Mergeable (SymFP eb sb) where-  rootStrategy = SimpleStrategy symIte---- function-instance (Mergeable b) => Mergeable (a -> b) where-  rootStrategy = case rootStrategy @b of-    SimpleStrategy m -> SimpleStrategy $ \cond t f v -> m cond (t v) (f v)-    _ -> NoStrategy-  {-# INLINE rootStrategy #-}--instance Mergeable1 ((->) a) where-  liftRootStrategy ms = case ms of-    SimpleStrategy m -> SimpleStrategy $ \cond t f v -> m cond (t v) (f v)-    _ -> NoStrategy-  {-# INLINE liftRootStrategy #-}--instance Mergeable2 ((->)) where-  liftRootStrategy2 _ ms = case ms of-    SimpleStrategy m -> SimpleStrategy $ \cond t f v -> m cond (t v) (f v)-    _ -> NoStrategy-  {-# INLINE liftRootStrategy2 #-}---- List---- | Helper type for building efficient merge strategy for list-like containers.-data StrategyList container where-  StrategyList ::-    forall a container.-    container [DynamicSortedIdx] ->-    container (MergingStrategy a) ->-    StrategyList container---- | Helper function for building efficient merge strategy for list-like--- containers.-buildStrategyList ::-  forall a container.-  (Functor container) =>-  MergingStrategy a ->-  container a ->-  StrategyList container-buildStrategyList s l = StrategyList idxs strategies-  where-    r = resolveStrategy s <$> l-    idxs = fst <$> r-    strategies = snd <$> r-{-# INLINE buildStrategyList #-}--instance (Eq1 container) => Eq (StrategyList container) where-  (StrategyList idxs1 _) == (StrategyList idxs2 _) = eq1 idxs1 idxs2-  {-# INLINE (==) #-}--instance (Ord1 container) => Ord (StrategyList container) where-  compare (StrategyList idxs1 _) (StrategyList idxs2 _) = compare1 idxs1 idxs2-  {-# INLINE compare #-}--instance (Show1 container) => Show (StrategyList container) where-  showsPrec i (StrategyList idxs1 _) = showsPrec1 i idxs1-  {-# INLINE showsPrec #-}--instance (Mergeable a) => Mergeable [a] where-  rootStrategy = case rootStrategy :: MergingStrategy a of-    SimpleStrategy m ->-      SortedStrategy length $ \_ ->-        SimpleStrategy $ \cond -> zipWith (m cond)-    NoStrategy ->-      SortedStrategy length $ const NoStrategy-    _ -> SortedStrategy length $ \_ ->-      SortedStrategy (buildStrategyList rootStrategy) $-        \(StrategyList _ strategies) ->-          let s :: [MergingStrategy a] = unsafeCoerce strategies-              allSimple = all (\case SimpleStrategy _ -> True; _ -> False) s-           in if allSimple-                then SimpleStrategy $ \cond l r ->-                  ( \case-                      (SimpleStrategy f, l1, r1) -> f cond l1 r1-                      _ -> error "impossible"-                  )-                    <$> zip3 s l r-                else NoStrategy-  {-# INLINE rootStrategy #-}--instance Mergeable1 [] where-  liftRootStrategy (ms :: MergingStrategy a) = case ms of-    SimpleStrategy m ->-      SortedStrategy length $ \_ ->-        SimpleStrategy $ \cond -> zipWith (m cond)-    NoStrategy ->-      SortedStrategy length $ const NoStrategy-    _ -> SortedStrategy length $ \_ ->-      SortedStrategy (buildStrategyList ms) $ \(StrategyList _ strategies) ->-        let s :: [MergingStrategy a] = unsafeCoerce strategies-            allSimple = all (\case SimpleStrategy _ -> True; _ -> False) s-         in if allSimple-              then SimpleStrategy $ \cond l r ->-                ( \case-                    (SimpleStrategy f, l1, r1) -> f cond l1 r1-                    _ -> error "impossible"-                )-                  <$> zip3 s l r-              else NoStrategy-  {-# INLINE liftRootStrategy #-}---- (,)-instance (Mergeable a, Mergeable b) => Mergeable (a, b) where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance (Mergeable a) => Mergeable1 ((,) a) where-  liftRootStrategy = liftRootStrategy2 rootStrategy-  {-# INLINE liftRootStrategy #-}--instance Mergeable2 (,) where-  liftRootStrategy2 = product2Strategy (,) id-  {-# INLINE liftRootStrategy2 #-}---- (,,)-instance (Mergeable a, Mergeable b, Mergeable c) => Mergeable ((,,) a b c) where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance (Mergeable a, Mergeable b) => Mergeable1 ((,,) a b) where-  liftRootStrategy = liftRootStrategy2 rootStrategy-  {-# INLINE liftRootStrategy #-}--instance (Mergeable a) => Mergeable2 ((,,) a) where-  liftRootStrategy2 = liftRootStrategy3 rootStrategy-  {-# INLINE liftRootStrategy2 #-}--instance Mergeable3 (,,) where-  liftRootStrategy3 m1 m2 m3 =-    product2Strategy-      (\a (b, c) -> (a, b, c))-      (\(a, b, c) -> (a, (b, c)))-      m1-      (liftRootStrategy2 m2 m3)-  {-# INLINE liftRootStrategy3 #-}---- (,,,)-instance-  (Mergeable a, Mergeable b, Mergeable c, Mergeable d) =>-  Mergeable ((,,,) a b c d)-  where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance-  (Mergeable a, Mergeable b, Mergeable c) =>-  Mergeable1 ((,,,) a b c)-  where-  liftRootStrategy = liftRootStrategy2 rootStrategy-  {-# INLINE liftRootStrategy #-}--instance (Mergeable a, Mergeable b) => Mergeable2 ((,,,) a b) where-  liftRootStrategy2 = liftRootStrategy3 rootStrategy-  {-# INLINE liftRootStrategy2 #-}--instance (Mergeable a) => Mergeable3 ((,,,) a) where-  liftRootStrategy3 m1 m2 m3 =-    product2Strategy-      (\(a, b) (c, d) -> (a, b, c, d))-      (\(a, b, c, d) -> ((a, b), (c, d)))-      (liftRootStrategy m1)-      (liftRootStrategy2 m2 m3)-  {-# INLINE liftRootStrategy3 #-}---- Instances-deriveBuiltins-  (ViaDefault ''Mergeable)-  [''Mergeable]-  [ ''Maybe,-    ''Either,-    ''AlgRealPoly,-    ''RealPoint,-    ''AlgReal,-    ''(),-    -- The following three are implemented by hand because they need to be-    -- consistent with Mergeable2 instances.-    -- ''(,),-    -- ''(,,),-    -- ''(,,,),-    ''(,,,,),-    ''(,,,,,),-    ''(,,,,,,),-    ''(,,,,,,,),-    ''(,,,,,,,,),-    ''(,,,,,,,,,),-    ''(,,,,,,,,,,),-    ''(,,,,,,,,,,,),-    ''(,,,,,,,,,,,,),-    ''(,,,,,,,,,,,,,),-    ''(,,,,,,,,,,,,,,),-    ''AssertionError,-    ''VerificationConditions,-    ''NotRepresentableFPError,-    ''Identity,-    ''Monoid.Dual,-    ''Monoid.Sum,-    ''Monoid.Product,-    ''Monoid.First,-    ''Monoid.Last,-    ''Down-  ]--deriveBuiltins-  (ViaDefault1 ''Mergeable1)-  [''Mergeable, ''Mergeable1]-  [ ''Maybe,-    ''Either,-    -- The following three are implemented by hand because they need to be-    -- consistent with Mergeable2 instances.-    -- ''(,),-    -- ''(,,),-    -- ''(,,,),-    ''(,,,,),-    ''(,,,,,),-    ''(,,,,,,),-    ''(,,,,,,,),-    ''(,,,,,,,,),-    ''(,,,,,,,,,),-    ''(,,,,,,,,,,),-    ''(,,,,,,,,,,,),-    ''(,,,,,,,,,,,,),-    ''(,,,,,,,,,,,,,),-    ''(,,,,,,,,,,,,,,),-    ''Identity,-    ''Monoid.Dual,-    ''Monoid.Sum,-    ''Monoid.Product,-    ''Monoid.First,-    ''Monoid.Last,-    ''Down-  ]---- MaybeT-instance (Mergeable1 m, Mergeable a) => Mergeable (MaybeT m a) where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance (Mergeable1 m) => Mergeable1 (MaybeT m) where-  liftRootStrategy m =-    wrapStrategy (liftRootStrategy (liftRootStrategy m)) MaybeT runMaybeT-  {-# INLINE liftRootStrategy #-}---- ExceptT-instance-  (Mergeable1 m, Mergeable e, Mergeable a) =>-  Mergeable (ExceptT e m a)-  where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance (Mergeable1 m, Mergeable e) => Mergeable1 (ExceptT e m) where-  liftRootStrategy m =-    wrapStrategy (liftRootStrategy (liftRootStrategy m)) ExceptT runExceptT-  {-# INLINE liftRootStrategy #-}---- state-instance-  (Mergeable s, Mergeable a, Mergeable1 m) =>-  Mergeable (StateLazy.StateT s m a)-  where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance (Mergeable s, Mergeable1 m) => Mergeable1 (StateLazy.StateT s m) where-  liftRootStrategy m =-    wrapStrategy-      (liftRootStrategy (liftRootStrategy (liftRootStrategy2 m rootStrategy)))-      StateLazy.StateT-      StateLazy.runStateT-  {-# INLINE liftRootStrategy #-}--instance-  (Mergeable s, Mergeable a, Mergeable1 m) =>-  Mergeable (StateStrict.StateT s m a)-  where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance-  (Mergeable s, Mergeable1 m) =>-  Mergeable1 (StateStrict.StateT s m)-  where-  liftRootStrategy m =-    wrapStrategy-      (liftRootStrategy (liftRootStrategy (liftRootStrategy2 m rootStrategy)))-      StateStrict.StateT-      StateStrict.runStateT-  {-# INLINE liftRootStrategy #-}---- writer-instance-  (Mergeable s, Mergeable a, Mergeable1 m) =>-  Mergeable (WriterLazy.WriterT s m a)-  where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance-  (Mergeable s, Mergeable1 m) =>-  Mergeable1 (WriterLazy.WriterT s m)-  where-  liftRootStrategy m =-    wrapStrategy-      (liftRootStrategy (liftRootStrategy2 m rootStrategy))-      WriterLazy.WriterT-      WriterLazy.runWriterT-  {-# INLINE liftRootStrategy #-}--instance-  (Mergeable s, Mergeable a, Mergeable1 m) =>-  Mergeable (WriterStrict.WriterT s m a)-  where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance-  (Mergeable s, Mergeable1 m) =>-  Mergeable1 (WriterStrict.WriterT s m)-  where-  liftRootStrategy m =-    wrapStrategy-      (liftRootStrategy (liftRootStrategy2 m rootStrategy))-      WriterStrict.WriterT-      WriterStrict.runWriterT-  {-# INLINE liftRootStrategy #-}---- reader-instance-  (Mergeable a, Mergeable1 m) =>-  Mergeable (ReaderT s m a)-  where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance (Mergeable1 m) => Mergeable1 (ReaderT s m) where-  liftRootStrategy m =-    wrapStrategy-      (liftRootStrategy (liftRootStrategy m))-      ReaderT-      runReaderT-  {-# INLINE liftRootStrategy #-}---- IdentityT-instance (Mergeable1 m, Mergeable a) => Mergeable (IdentityT m a) where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance (Mergeable1 m) => Mergeable1 (IdentityT m) where-  liftRootStrategy m = wrapStrategy (liftRootStrategy m) IdentityT runIdentityT-  {-# INLINE liftRootStrategy #-}---- ContT-instance (Mergeable1 m, Mergeable r) => Mergeable (ContT r m a) where-  rootStrategy =-    wrapStrategy-      (liftRootStrategy rootStrategy1)-      ContT-      (\(ContT v) -> v)-  {-# INLINE rootStrategy #-}--instance (Mergeable1 m, Mergeable r) => Mergeable1 (ContT r m) where-  liftRootStrategy _ =-    wrapStrategy-      (liftRootStrategy rootStrategy1)-      ContT-      (\(ContT v) -> v)-  {-# INLINE liftRootStrategy #-}---- RWS-instance-  (Mergeable s, Mergeable w, Mergeable a, Mergeable1 m) =>-  Mergeable (RWSLazy.RWST r w s m a)-  where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance-  (Mergeable s, Mergeable w, Mergeable1 m) =>-  Mergeable1 (RWSLazy.RWST r w s m)-  where-  liftRootStrategy m =-    wrapStrategy-      ( liftRootStrategy . liftRootStrategy . liftRootStrategy $-          liftRootStrategy3 m rootStrategy rootStrategy-      )-      RWSLazy.RWST-      (\(RWSLazy.RWST rws) -> rws)-  {-# INLINE liftRootStrategy #-}--instance-  (Mergeable s, Mergeable w, Mergeable a, Mergeable1 m) =>-  Mergeable (RWSStrict.RWST r w s m a)-  where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance-  (Mergeable s, Mergeable w, Mergeable1 m) =>-  Mergeable1 (RWSStrict.RWST r w s m)-  where-  liftRootStrategy m =-    wrapStrategy-      ( liftRootStrategy . liftRootStrategy . liftRootStrategy $-          liftRootStrategy3 m rootStrategy rootStrategy-      )-      RWSStrict.RWST-      (\(RWSStrict.RWST rws) -> rws)-  {-# INLINE liftRootStrategy #-}---- Product-deriving via-  (Default (Product l r a))-  instance-    (Mergeable (l a), Mergeable (r a)) => Mergeable (Product l r a)--deriving via-  (Default1 (Product l r))-  instance-    (Mergeable1 l, Mergeable1 r) => Mergeable1 (Product l r)---- Sum-deriving via-  (Default (Sum l r a))-  instance-    (Mergeable (l a), Mergeable (r a)) => Mergeable (Sum l r a)--deriving via-  (Default1 (Sum l r))-  instance-    (Mergeable1 l, Mergeable1 r) => Mergeable1 (Sum l r)---- Compose-deriving via-  (Default (Compose f g a))-  instance-    (Mergeable (f (g a))) => Mergeable (Compose f g a)--instance (Mergeable1 f, Mergeable1 g) => Mergeable1 (Compose f g) where-  liftRootStrategy s =-    wrapStrategy (liftRootStrategy (liftRootStrategy s)) Compose getCompose-  {-# INLINE liftRootStrategy #-}---- Const-deriving via-  (Default (Const a b))-  instance-    (Mergeable a) => Mergeable (Const a b)--deriving via-  (Default1 (Const a))-  instance-    (Mergeable a) => Mergeable1 (Const a)---- Alt-deriving via-  (Default (Alt f a))-  instance-    (Mergeable (f a)) => Mergeable (Alt f a)--deriving via-  (Default1 (Alt f))-  instance-    (Mergeable1 f) => Mergeable1 (Alt f)---- Ap-deriving via-  (Default (Ap f a))-  instance-    (Mergeable (f a)) => Mergeable (Ap f a)--deriving via-  (Default1 (Ap f))-  instance-    (Mergeable1 f) => Mergeable1 (Ap f)---- Endo-instance (Mergeable a) => Mergeable (Endo a) where-  rootStrategy = rootStrategy1-  {-# INLINE rootStrategy #-}--instance Mergeable1 Endo where-  liftRootStrategy strategy =-    wrapStrategy (liftRootStrategy strategy) Endo appEndo---- Generic-deriving via (Default (U1 p)) instance Mergeable (U1 p)--deriving via (Default (V1 p)) instance Mergeable (V1 p)--deriving via-  (Default (K1 i c p))-  instance-    (Mergeable c) => Mergeable (K1 i c p)--deriving via-  (Default (M1 i c f p))-  instance-    (Mergeable (f p)) => Mergeable (M1 i c f p)--deriving via-  (Default ((f :+: g) p))-  instance-    (Mergeable (f p), Mergeable (g p)) => Mergeable ((f :+: g) p)--deriving via-  (Default ((f :*: g) p))-  instance-    (Mergeable (f p), Mergeable (g p)) => Mergeable ((f :*: g) p)--deriving via-  (Default (Par1 p))-  instance-    (Mergeable p) => Mergeable (Par1 p)--deriving via-  (Default (Rec1 f p))-  instance-    (Mergeable (f p)) => Mergeable (Rec1 f p)--deriving via-  (Default ((f :.: g) p))-  instance-    (Mergeable (f (g p))) => Mergeable ((f :.: g) p)---- Exceptions-instance Mergeable ArithException where-  rootStrategy =-    SortedStrategy-      ( \case-          Overflow -> 0 :: Int-          Underflow -> 1 :: Int-          LossOfPrecision -> 2 :: Int-          DivideByZero -> 3 :: Int-          Denormal -> 4 :: Int-          RatioZeroDenominator -> 5 :: Int-      )-      (const $ SimpleStrategy $ \_ l _ -> l)--instance Mergeable2 Either where-  liftRootStrategy2 m1 m2 =-    SortedStrategy-      ( \case-          Left _ -> False-          Right _ -> True-      )-      ( \case-          False -> wrapStrategy m1 Left (\case (Left v) -> v; _ -> undefined)-          True -> wrapStrategy m2 Right (\case (Right v) -> v; _ -> undefined)-      )-  {-# INLINE liftRootStrategy2 #-}+{-# OPTIONS_GHC -Wno-missing-import-lists #-}++-- |+-- Module      :   Grisette.Internal.Core.Data.Class.Mergeable+-- Copyright   :   (c) Sirui Lu 2021-2023+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Internal.Core.Data.Class.Mergeable+  ( -- * Merging strategy+    MergingStrategy (..),++    -- * Mergeable+    Mergeable (..),+    Mergeable1 (..),+    rootStrategy1,+    Mergeable2 (..),+    rootStrategy2,+    Mergeable3 (..),+    rootStrategy3,++    -- * Generic 'Mergeable'+    MergeableArgs (..),+    GMergeable (..),+    genericRootStrategy,+    genericLiftRootStrategy,++    -- * Combinators for manually building merging strategies+    wrapStrategy,+    product2Strategy,+    DynamicSortedIdx (..),+    StrategyList (..),+    buildStrategyList,+    resolveStrategy,+    resolveStrategy',+    resolveMergeable1,+  )+where++import Grisette.Internal.Internal.Decl.Core.Data.Class.Mergeable+import Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable ()