grisette 0.3.1.0 → 0.3.1.1
raw patch · 110 files changed
+3413/−954 lines, 110 filesdep +HUnitdep +test-frameworkdep +test-framework-hunitdep −call-stackdep −tastydep −tasty-hunitdep ~bytestringdep ~deepseqdep ~doctestPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependencies added: HUnit, test-framework, test-framework-hunit, test-framework-quickcheck2
Dependencies removed: call-stack, tasty, tasty-hunit, tasty-quickcheck, tasty-test-reporter, vector
Dependency ranges changed: bytestring, deepseq, doctest, text
API changes (from Hackage documentation)
- Grisette.Core.Data.Class.SafeArith: Denormal :: ArithException
- Grisette.Core.Data.Class.SafeArith: LossOfPrecision :: ArithException
- Grisette.Core.Data.Class.SafeArith: RatioZeroDenominator :: ArithException
- Grisette.IR.SymPrim.Data.TabularFun: instance (Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term.SupportedPrim a, Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term.SupportedPrim b) => Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term.SupportedPrim (a Grisette.IR.SymPrim.Data.TabularFun.=-> b)
+ Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term: instance (Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term.SupportedPrim a, Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term.SupportedPrim b) => Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term.SupportedPrim (a Grisette.IR.SymPrim.Data.TabularFun.=-> b)
- Grisette.Core: [StrategyList] :: forall bool a container. container [DynamicSortedIdx] -> container (MergingStrategy a) -> StrategyList container
+ Grisette.Core: [StrategyList] :: forall a container. container [DynamicSortedIdx] -> container (MergingStrategy a) -> StrategyList container
- Grisette.Core: buildStrategyList :: forall bool a container. Functor container => MergingStrategy a -> container a -> StrategyList container
+ Grisette.Core: buildStrategyList :: forall a container. Functor container => MergingStrategy a -> container a -> StrategyList container
- Grisette.Core: choose :: forall bool a u. Mergeable a => [a] -> FreshIdent -> UnionM a
+ Grisette.Core: choose :: forall a. Mergeable a => [a] -> FreshIdent -> UnionM a
- Grisette.Core: chooseFresh :: forall bool a m u. (Mergeable a, MonadFresh m) => [a] -> m (UnionM a)
+ Grisette.Core: chooseFresh :: forall a m. (Mergeable a, MonadFresh m) => [a] -> m (UnionM a)
- Grisette.Core: chooseUnion :: forall a u. Mergeable a => [UnionM a] -> FreshIdent -> UnionM a
+ Grisette.Core: chooseUnion :: forall a. Mergeable a => [UnionM a] -> FreshIdent -> UnionM a
- Grisette.Core: chooseUnionFresh :: forall bool a m u. (Mergeable a, MonadFresh m) => [UnionM a] -> m (UnionM a)
+ Grisette.Core: chooseUnionFresh :: forall a m. (Mergeable a, MonadFresh m) => [UnionM a] -> m (UnionM a)
- Grisette.Core: class (SymbolSetOps symbolSet typedSymbol) => SymbolSetRep rep symbolSet (typedSymbol :: * -> *)
+ Grisette.Core: class (SymbolSetOps symbolSet typedSymbol) => SymbolSetRep rep symbolSet (typedSymbol :: Type -> Type)
- Grisette.Core: derivedNoSpecFresh :: forall bool a m u. (Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) => () -> m (UnionM a)
+ Grisette.Core: derivedNoSpecFresh :: forall a m. (Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) => () -> m (UnionM a)
- Grisette.Core: infix 4 >=~
+ Grisette.Core: infix 4 >~
- Grisette.Core: mrgInL :: forall {k_a9Ng :: Type} (f_a9Nh :: k_a9Ng -> Type) (g_a9Ni :: k_a9Ng -> Type) (a_a9Nj :: k_a9Ng). Mergeable (Sum f_a9Nh g_a9Ni a_a9Nj) => f_a9Nh a_a9Nj -> UnionM (Sum f_a9Nh g_a9Ni a_a9Nj)
+ Grisette.Core: mrgInL :: forall {k_a9N9 :: Type} (f_a9Na :: k_a9N9 -> Type) (g_a9Nb :: k_a9N9 -> Type) (a_a9Nc :: k_a9N9). Mergeable (Sum f_a9Na g_a9Nb a_a9Nc) => f_a9Na a_a9Nc -> UnionM (Sum f_a9Na g_a9Nb a_a9Nc)
- Grisette.Core: mrgInR :: forall {k_a9Ng :: Type} (f_a9Nh :: k_a9Ng -> Type) (g_a9Ni :: k_a9Ng -> Type) (a_a9Nj :: k_a9Ng). Mergeable (Sum f_a9Nh g_a9Ni a_a9Nj) => g_a9Ni a_a9Nj -> UnionM (Sum f_a9Nh g_a9Ni a_a9Nj)
+ Grisette.Core: mrgInR :: forall {k_a9N9 :: Type} (f_a9Na :: k_a9N9 -> Type) (g_a9Nb :: k_a9N9 -> Type) (a_a9Nc :: k_a9N9). Mergeable (Sum f_a9Na g_a9Nb a_a9Nc) => g_a9Nb a_a9Nc -> UnionM (Sum f_a9Na g_a9Nb a_a9Nc)
- Grisette.Core: mrgLeft :: forall (a_a9xk :: Type) (b_a9xl :: Type). Mergeable (Either a_a9xk b_a9xl) => a_a9xk -> UnionM (Either a_a9xk b_a9xl)
+ Grisette.Core: mrgLeft :: forall (a_a9xd :: Type) (b_a9xe :: Type). Mergeable (Either a_a9xd b_a9xe) => a_a9xd -> UnionM (Either a_a9xd b_a9xe)
- Grisette.Core: mrgRight :: forall (a_a9xk :: Type) (b_a9xl :: Type). Mergeable (Either a_a9xk b_a9xl) => b_a9xl -> UnionM (Either a_a9xk b_a9xl)
+ Grisette.Core: mrgRight :: forall (a_a9xd :: Type) (b_a9xe :: Type). Mergeable (Either a_a9xd b_a9xe) => b_a9xe -> UnionM (Either a_a9xd b_a9xe)
- Grisette.Core: onUnion :: forall bool u a r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> r) -> u a -> r
+ Grisette.Core: onUnion :: forall u a r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> r) -> u a -> r
- Grisette.Core: onUnion2 :: forall bool u a b r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> r) -> u a -> u b -> r
+ Grisette.Core: onUnion2 :: forall u a b r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> r) -> u a -> u b -> r
- Grisette.Core: onUnion3 :: forall bool u a b c r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> r) -> u a -> u b -> u c -> r
+ Grisette.Core: onUnion3 :: forall u a b c r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> r) -> u a -> u b -> u c -> r
- Grisette.Core: onUnion4 :: forall bool u a b c d r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> d -> r) -> u a -> u b -> u c -> u d -> r
+ Grisette.Core: onUnion4 :: forall u a b c d r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> d -> r) -> u a -> u b -> u c -> u d -> r
- Grisette.Core: simpleMerge :: forall bool u a. (SimpleMergeable a, UnionLike u, UnionPrjOp u) => u a -> a
+ Grisette.Core: simpleMerge :: forall u a. (SimpleMergeable a, UnionLike u, UnionPrjOp u) => u a -> a
- Grisette.Core.BuiltinUnionWrappers: mrgInL :: forall {k_a9Ng :: Type} (f_a9Nh :: k_a9Ng -> Type) (g_a9Ni :: k_a9Ng -> Type) (a_a9Nj :: k_a9Ng). Mergeable (Sum f_a9Nh g_a9Ni a_a9Nj) => f_a9Nh a_a9Nj -> UnionM (Sum f_a9Nh g_a9Ni a_a9Nj)
+ Grisette.Core.BuiltinUnionWrappers: mrgInL :: forall {k_a9N9 :: Type} (f_a9Na :: k_a9N9 -> Type) (g_a9Nb :: k_a9N9 -> Type) (a_a9Nc :: k_a9N9). Mergeable (Sum f_a9Na g_a9Nb a_a9Nc) => f_a9Na a_a9Nc -> UnionM (Sum f_a9Na g_a9Nb a_a9Nc)
- Grisette.Core.BuiltinUnionWrappers: mrgInR :: forall {k_a9Ng :: Type} (f_a9Nh :: k_a9Ng -> Type) (g_a9Ni :: k_a9Ng -> Type) (a_a9Nj :: k_a9Ng). Mergeable (Sum f_a9Nh g_a9Ni a_a9Nj) => g_a9Ni a_a9Nj -> UnionM (Sum f_a9Nh g_a9Ni a_a9Nj)
+ Grisette.Core.BuiltinUnionWrappers: mrgInR :: forall {k_a9N9 :: Type} (f_a9Na :: k_a9N9 -> Type) (g_a9Nb :: k_a9N9 -> Type) (a_a9Nc :: k_a9N9). Mergeable (Sum f_a9Na g_a9Nb a_a9Nc) => g_a9Nb a_a9Nc -> UnionM (Sum f_a9Na g_a9Nb a_a9Nc)
- Grisette.Core.BuiltinUnionWrappers: mrgLeft :: forall (a_a9xk :: Type) (b_a9xl :: Type). Mergeable (Either a_a9xk b_a9xl) => a_a9xk -> UnionM (Either a_a9xk b_a9xl)
+ Grisette.Core.BuiltinUnionWrappers: mrgLeft :: forall (a_a9xd :: Type) (b_a9xe :: Type). Mergeable (Either a_a9xd b_a9xe) => a_a9xd -> UnionM (Either a_a9xd b_a9xe)
- Grisette.Core.BuiltinUnionWrappers: mrgRight :: forall (a_a9xk :: Type) (b_a9xl :: Type). Mergeable (Either a_a9xk b_a9xl) => b_a9xl -> UnionM (Either a_a9xk b_a9xl)
+ Grisette.Core.BuiltinUnionWrappers: mrgRight :: forall (a_a9xd :: Type) (b_a9xe :: Type). Mergeable (Either a_a9xd b_a9xe) => b_a9xe -> UnionM (Either a_a9xd b_a9xe)
- Grisette.Core.Data.BV: binSomeWordN :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> r) -> SomeWordN -> SomeWordN -> r
+ Grisette.Core.Data.BV: binSomeWordN :: (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> r) -> SomeWordN -> SomeWordN -> r
- Grisette.Core.Data.BV: binSomeWordNR1 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> WordN n) -> SomeWordN -> SomeWordN -> SomeWordN
+ Grisette.Core.Data.BV: binSomeWordNR1 :: (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> WordN n) -> SomeWordN -> SomeWordN -> SomeWordN
- Grisette.Core.Data.BV: binSomeWordNR2 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> (WordN n, WordN n)) -> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
+ Grisette.Core.Data.BV: binSomeWordNR2 :: (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> (WordN n, WordN n)) -> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
- Grisette.Core.Data.BV: unarySomeWordN :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> r) -> SomeWordN -> r
+ Grisette.Core.Data.BV: unarySomeWordN :: (forall n. (KnownNat n, 1 <= n) => WordN n -> r) -> SomeWordN -> r
- Grisette.Core.Data.BV: unarySomeWordNR1 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n) -> SomeWordN -> SomeWordN
+ Grisette.Core.Data.BV: unarySomeWordNR1 :: (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n) -> SomeWordN -> SomeWordN
- Grisette.Core.Data.Class.GenSym: choose :: forall bool a u. Mergeable a => [a] -> FreshIdent -> UnionM a
+ Grisette.Core.Data.Class.GenSym: choose :: forall a. Mergeable a => [a] -> FreshIdent -> UnionM a
- Grisette.Core.Data.Class.GenSym: chooseFresh :: forall bool a m u. (Mergeable a, MonadFresh m) => [a] -> m (UnionM a)
+ Grisette.Core.Data.Class.GenSym: chooseFresh :: forall a m. (Mergeable a, MonadFresh m) => [a] -> m (UnionM a)
- Grisette.Core.Data.Class.GenSym: chooseUnion :: forall a u. Mergeable a => [UnionM a] -> FreshIdent -> UnionM a
+ Grisette.Core.Data.Class.GenSym: chooseUnion :: forall a. Mergeable a => [UnionM a] -> FreshIdent -> UnionM a
- Grisette.Core.Data.Class.GenSym: chooseUnionFresh :: forall bool a m u. (Mergeable a, MonadFresh m) => [UnionM a] -> m (UnionM a)
+ Grisette.Core.Data.Class.GenSym: chooseUnionFresh :: forall a m. (Mergeable a, MonadFresh m) => [UnionM a] -> m (UnionM a)
- Grisette.Core.Data.Class.GenSym: derivedNoSpecFresh :: forall bool a m u. (Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) => () -> m (UnionM a)
+ Grisette.Core.Data.Class.GenSym: derivedNoSpecFresh :: forall a m. (Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) => () -> m (UnionM a)
- Grisette.Core.Data.Class.Mergeable: [StrategyList] :: forall bool a container. container [DynamicSortedIdx] -> container (MergingStrategy a) -> StrategyList container
+ Grisette.Core.Data.Class.Mergeable: [StrategyList] :: forall a container. container [DynamicSortedIdx] -> container (MergingStrategy a) -> StrategyList container
- Grisette.Core.Data.Class.Mergeable: buildStrategyList :: forall bool a container. Functor container => MergingStrategy a -> container a -> StrategyList container
+ Grisette.Core.Data.Class.Mergeable: buildStrategyList :: forall a container. Functor container => MergingStrategy a -> container a -> StrategyList container
- Grisette.Core.Data.Class.ModelOps: class (SymbolSetOps symbolSet typedSymbol) => SymbolSetRep rep symbolSet (typedSymbol :: * -> *)
+ Grisette.Core.Data.Class.ModelOps: class (SymbolSetOps symbolSet typedSymbol) => SymbolSetRep rep symbolSet (typedSymbol :: Type -> Type)
- Grisette.Core.Data.Class.SimpleMergeable: onUnion :: forall bool u a r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> r) -> u a -> r
+ Grisette.Core.Data.Class.SimpleMergeable: onUnion :: forall u a r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> r) -> u a -> r
- Grisette.Core.Data.Class.SimpleMergeable: onUnion2 :: forall bool u a b r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> r) -> u a -> u b -> r
+ Grisette.Core.Data.Class.SimpleMergeable: onUnion2 :: forall u a b r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> r) -> u a -> u b -> r
- Grisette.Core.Data.Class.SimpleMergeable: onUnion3 :: forall bool u a b c r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> r) -> u a -> u b -> u c -> r
+ Grisette.Core.Data.Class.SimpleMergeable: onUnion3 :: forall u a b c r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> r) -> u a -> u b -> u c -> r
- Grisette.Core.Data.Class.SimpleMergeable: onUnion4 :: forall bool u a b c d r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> d -> r) -> u a -> u b -> u c -> u d -> r
+ Grisette.Core.Data.Class.SimpleMergeable: onUnion4 :: forall u a b c d r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> d -> r) -> u a -> u b -> u c -> u d -> r
- Grisette.Core.Data.Class.SimpleMergeable: simpleMerge :: forall bool u a. (SimpleMergeable a, UnionLike u, UnionPrjOp u) => u a -> a
+ Grisette.Core.Data.Class.SimpleMergeable: simpleMerge :: forall u a. (SimpleMergeable a, UnionLike u, UnionPrjOp u) => u a -> a
- Grisette.Experimental: derivedFreshConstrainedNoSpec :: forall bool a m u e. (Generic a, GenSymConstrainedNoSpec (Rep a), Mergeable a, MonadFresh m, MonadError e m, UnionLike m) => e -> () -> m (UnionM a)
+ Grisette.Experimental: derivedFreshConstrainedNoSpec :: forall a m e. (Generic a, GenSymConstrainedNoSpec (Rep a), Mergeable a, MonadFresh m, MonadError e m, UnionLike m) => e -> () -> m (UnionM a)
- Grisette.Experimental.GenSymConstrained: derivedFreshConstrainedNoSpec :: forall bool a m u e. (Generic a, GenSymConstrainedNoSpec (Rep a), Mergeable a, MonadFresh m, MonadError e m, UnionLike m) => e -> () -> m (UnionM a)
+ Grisette.Experimental.GenSymConstrained: derivedFreshConstrainedNoSpec :: forall a m e. (Generic a, GenSymConstrainedNoSpec (Rep a), Mergeable a, MonadFresh m, MonadError e m, UnionLike m) => e -> () -> m (UnionM a)
- Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term: type PrimConstraint t = ();
+ Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term: type PrimConstraint _ = ();
- Grisette.Internal.IR.SymPrim: type PrimConstraint t = ();
+ Grisette.Internal.IR.SymPrim: type PrimConstraint _ = ();
- Grisette.Utils: knownAdd :: forall m n r. KnownProof m -> KnownProof n -> KnownProof (m + n)
+ Grisette.Utils: knownAdd :: forall m n. KnownProof m -> KnownProof n -> KnownProof (m + n)
- Grisette.Utils.Parameterized: knownAdd :: forall m n r. KnownProof m -> KnownProof n -> KnownProof (m + n)
+ Grisette.Utils.Parameterized: knownAdd :: forall m n. KnownProof m -> KnownProof n -> KnownProof (m + n)
Files
- CHANGELOG.md +7/−2
- README.md +1/−1
- doctest/Main.hs +1/−1
- grisette.cabal +20/−23
- src/Grisette.hs +4/−1
- src/Grisette/Backend/SBV.hs +14/−0
- src/Grisette/Backend/SBV/Data/SMT/Lowering.hs +103/−32
- src/Grisette/Backend/SBV/Data/SMT/Solving.hs +44/−20
- src/Grisette/Backend/SBV/Data/SMT/Solving.hs-boot +9/−7
- src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs +6/−2
- src/Grisette/Core.hs +165/−8
- src/Grisette/Core/BuiltinUnionWrappers.hs +4/−4
- src/Grisette/Core/Control/Exception.hs +23/−13
- src/Grisette/Core/Control/Monad/CBMCExcept.hs +56/−15
- src/Grisette/Core/Control/Monad/Class/MonadParallelUnion.hs +9/−8
- src/Grisette/Core/Control/Monad/Union.hs +1/−1
- src/Grisette/Core/Control/Monad/UnionM.hs +72/−26
- src/Grisette/Core/Control/Monad/UnionM.hs-boot +3/−5
- src/Grisette/Core/Data/BV.hs +84/−20
- src/Grisette/Core/Data/Class/BitVector.hs +10/−2
- src/Grisette/Core/Data/Class/Bool.hs +40/−8
- src/Grisette/Core/Data/Class/Bool.hs-boot +2/−2
- src/Grisette/Core/Data/Class/CEGISSolver.hs +16/−9
- src/Grisette/Core/Data/Class/Error.hs +6/−6
- src/Grisette/Core/Data/Class/Evaluate.hs +21/−11
- src/Grisette/Core/Data/Class/ExtractSymbolics.hs +20/−7
- src/Grisette/Core/Data/Class/GPretty.hs +58/−17
- src/Grisette/Core/Data/Class/GenSym.hs +92/−37
- src/Grisette/Core/Data/Class/Mergeable.hs +81/−27
- src/Grisette/Core/Data/Class/Mergeable.hs-boot +8/−3
- src/Grisette/Core/Data/Class/ModelOps.hs +2/−4
- src/Grisette/Core/Data/Class/SOrd.hs +29/−10
- src/Grisette/Core/Data/Class/SafeArith.hs +32/−16
- src/Grisette/Core/Data/Class/SimpleMergeable.hs +41/−14
- src/Grisette/Core/Data/Class/SimpleMergeable.hs-boot +3/−1
- src/Grisette/Core/Data/Class/Solvable.hs +5/−5
- src/Grisette/Core/Data/Class/Solver.hs +12/−13
- src/Grisette/Core/Data/Class/Substitute.hs +21/−10
- src/Grisette/Core/Data/Class/ToCon.hs +18/−8
- src/Grisette/Core/Data/Class/ToSym.hs +19/−8
- src/Grisette/Core/Data/FileLocation.hs +10/−6
- src/Grisette/Core/Data/MemoUtils.hs +3/−3
- src/Grisette/Core/Data/Union.hs +33/−7
- src/Grisette/Core/TH.hs +18/−3
- src/Grisette/Core/THCompat.hs +26/−9
- src/Grisette/Experimental.hs +14/−0
- src/Grisette/Experimental/GenSymConstrained.hs +35/−15
- src/Grisette/IR/SymPrim.hs +36/−3
- src/Grisette/IR/SymPrim/Data/IntBitwidth.hs +2/−2
- src/Grisette/IR/SymPrim/Data/Prim/Helpers.hs +6/−2
- src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Caches.hs +12/−5
- src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs +66/−8
- src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs-boot +19/−6
- src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/SomeTerm.hs +7/−2
- src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs +102/−14
- src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot +17/−10
- src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs +105/−3
- src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs-boot +15/−2
- src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs +65/−4
- src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs-boot +7/−3
- src/Grisette/IR/SymPrim/Data/Prim/Model.hs +138/−6
- src/Grisette/IR/SymPrim/Data/Prim/Model.hs-boot +6/−1
- src/Grisette/IR/SymPrim/Data/Prim/ModelValue.hs +8/−1
- src/Grisette/IR/SymPrim/Data/Prim/PartialEval/BV.hs +20/−2
- src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bits.hs +26/−1
- src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bool.hs +26/−5
- src/Grisette/IR/SymPrim/Data/Prim/PartialEval/GeneralFun.hs +14/−2
- src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Integral.hs +13/−3
- src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Num.hs +25/−3
- src/Grisette/IR/SymPrim/Data/Prim/PartialEval/PartialEval.hs +2/−2
- src/Grisette/IR/SymPrim/Data/Prim/PartialEval/TabularFun.hs +14/−1
- src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Unfold.hs +14/−2
- src/Grisette/IR/SymPrim/Data/Prim/Utils.hs +7/−0
- src/Grisette/IR/SymPrim/Data/SymPrim.hs +198/−36
- src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot +16/−10
- src/Grisette/IR/SymPrim/Data/TabularFun.hs +5/−14
- src/Grisette/IR/SymPrim/Data/TabularFun.hs-boot +14/−0
- src/Grisette/Internal/Backend/SBV.hs +4/−1
- src/Grisette/Internal/Core.hs +11/−0
- src/Grisette/Internal/IR/SymPrim.hs +91/−2
- src/Grisette/Lib/Base.hs +31/−0
- src/Grisette/Lib/Control/Monad.hs +9/−4
- src/Grisette/Lib/Control/Monad.hs-boot +17/−4
- src/Grisette/Lib/Control/Monad/Except.hs +4/−5
- src/Grisette/Lib/Control/Monad/Trans.hs +4/−4
- src/Grisette/Lib/Control/Monad/Trans/Cont.hs +7/−5
- src/Grisette/Lib/Data/Foldable.hs +8/−5
- src/Grisette/Lib/Data/List.hs +10/−11
- src/Grisette/Lib/Data/Traversable.hs +8/−1
- src/Grisette/Lib/Mtl.hs +8/−1
- src/Grisette/Qualified/ParallelUnionDo.hs +6/−3
- src/Grisette/Utils.hs +32/−0
- src/Grisette/Utils/Parameterized.hs +14/−4
- test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs +40/−20
- test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs +116/−66
- test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs +112/−7
- test/Grisette/Backend/SBV/Data/SMT/TermRewritingTests.hs +53/−10
- test/Grisette/Core/Control/Monad/UnionMTests.hs +11/−7
- test/Grisette/Core/Data/BVTests.hs +62/−23
- test/Grisette/Core/Data/Class/GPrettyTests.hs +38/−23
- test/Grisette/IR/SymPrim/Data/Prim/BVTests.hs +18/−7
- test/Grisette/IR/SymPrim/Data/Prim/BitsTests.hs +23/−6
- test/Grisette/IR/SymPrim/Data/Prim/BoolTests.hs +25/−6
- test/Grisette/IR/SymPrim/Data/Prim/IntegralTests.hs +45/−25
- test/Grisette/IR/SymPrim/Data/Prim/ModelTests.hs +39/−9
- test/Grisette/IR/SymPrim/Data/Prim/NumTests.hs +30/−6
- test/Grisette/IR/SymPrim/Data/Prim/TabularFunTests.hs +17/−5
- test/Grisette/IR/SymPrim/Data/SymPrimTests.hs +184/−53
- test/Grisette/IR/SymPrim/Data/TabularFunTests.hs +8/−5
- test/Main.hs +22/−23
CHANGELOG.md view
@@ -5,6 +5,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [Unreleased]++## [0.3.1.1] -- 2023-09-29++No user-facing changes.+ ## [0.3.1.0] -- 2023-07-19 ### Added@@ -64,9 +70,8 @@ - Initial release for Grisette. [Unreleased]: https://github.com/lsrcz/grisette/compare/v0.3.1.0...HEAD+[0.3.1.1]: https://github.com/lsrcz/grisette/compare/v0.3.1.0...v0.3.1.1 [0.3.1.0]: https://github.com/lsrcz/grisette/compare/v0.3.0.0...v0.3.1.0-[0.3.0.0]: https://github.com/lsrcz/grisette/compare/v0.2.0.0...v0.3.0.0-[Unreleased]: https://github.com/lsrcz/grisette/compare/v0.3.0.0...HEAD [0.3.0.0]: https://github.com/lsrcz/grisette/compare/v0.2.0.0...v0.3.0.0 [0.2.0.0]: https://github.com/lsrcz/grisette/compare/v0.1.0.0...v0.2.0.0 [0.1.0.0]: https://github.com/lsrcz/grisette/tree/v0.1.0.0
README.md view
@@ -47,7 +47,7 @@ ```cabal library ...- build-depends: grisette >= 0.2 < 0.3+ build-depends: grisette >= 0.3 < 0.4 ``` #### Quick start template with `stack new`
doctest/Main.hs view
@@ -1,4 +1,4 @@-module Main where+module Main (main) where import System.FilePath.Glob (glob) import Test.DocTest (doctest)
grisette.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: grisette-version: 0.3.1.0+version: 0.3.1.1 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@@ -28,7 +28,7 @@ GHC == 8.10.7 , GHC == 9.0.2 , GHC == 9.2.8- , GHC == 9.4.5+ , GHC == 9.4.6 , GHC == 9.6.2 extra-source-files: CHANGELOG.md@@ -126,13 +126,13 @@ Paths_grisette 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 build-depends: QuickCheck >=2.13.2 && <2.15 , array >=0.5.4 && <0.6 , base >=4.14 && <5- , bytestring >=0.10.12 && <0.12- , call-stack >=0.1 && <0.5- , deepseq >=1.4.4 && <1.5+ , bytestring >=0.10.12 && <0.13+ , deepseq >=1.4.4 && <1.6 , generic-deriving >=1.14.1 && <1.15 , hashable >=1.2.3 && <1.5 , hashtables >=1.2.3.4 && <1.4@@ -143,11 +143,10 @@ , prettyprinter >=1.5.0 && <1.8 , sbv >=8.11 && <10.3 , template-haskell >=2.16 && <2.21- , text >=1.2.4.1 && <2.1+ , text >=1.2.4.1 && <2.2 , th-compat >=0.1.2 && <0.2 , transformers >=0.5.6 && <0.7 , unordered-containers >=0.2.11 && <0.3- , vector >=0.12.1 && <0.14 default-language: Haskell2010 if flag(fast) ghc-options: -O2@@ -161,15 +160,15 @@ Paths_grisette hs-source-dirs: doctest+ ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N build-depends: Glob , QuickCheck >=2.13.2 && <2.15 , array >=0.5.4 && <0.6 , base >=4.14 && <5- , bytestring >=0.10.12 && <0.12- , call-stack >=0.1 && <0.5- , deepseq >=1.4.4 && <1.5- , doctest >=0.18.2 && <0.22+ , bytestring >=0.10.12 && <0.13+ , deepseq >=1.4.4 && <1.6+ , doctest >=0.18.2 && <0.23 , generic-deriving >=1.14.1 && <1.15 , grisette , hashable >=1.2.3 && <1.5@@ -181,11 +180,10 @@ , prettyprinter >=1.5.0 && <1.8 , sbv >=8.11 && <10.3 , template-haskell >=2.16 && <2.21- , text >=1.2.4.1 && <2.1+ , text >=1.2.4.1 && <2.2 , th-compat >=0.1.2 && <0.2 , transformers >=0.5.6 && <0.7 , unordered-containers >=0.2.11 && <0.3- , vector >=0.12.1 && <0.14 default-language: Haskell2010 if flag(fast) ghc-options: -O2@@ -215,13 +213,14 @@ Paths_grisette hs-source-dirs: test+ ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N build-depends:- QuickCheck >=2.13.2 && <2.15+ HUnit ==1.6.*+ , QuickCheck >=2.13.2 && <2.15 , array >=0.5.4 && <0.6 , base >=4.14 && <5- , bytestring >=0.10.12 && <0.12- , call-stack >=0.1 && <0.5- , deepseq >=1.4.4 && <1.5+ , bytestring >=0.10.12 && <0.13+ , deepseq >=1.4.4 && <1.6 , generic-deriving >=1.14.1 && <1.15 , grisette , hashable >=1.2.3 && <1.5@@ -232,16 +231,14 @@ , parallel >=3.2.2.0 && <3.3 , prettyprinter >=1.5.0 && <1.8 , sbv >=8.11 && <10.3- , tasty >=1.1.0.3 && <1.5- , tasty-hunit ==0.10.*- , tasty-quickcheck >=0.10.1 && <0.11- , tasty-test-reporter >=0.1.1.2 && <0.2 , template-haskell >=2.16 && <2.21- , text >=1.2.4.1 && <2.1+ , 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+ , text >=1.2.4.1 && <2.2 , th-compat >=0.1.2 && <0.2 , transformers >=0.5.6 && <0.7 , unordered-containers >=0.2.11 && <0.3- , vector >=0.12.1 && <0.14 default-language: Haskell2010 if flag(fast) ghc-options: -O2
src/Grisette.hs view
@@ -1,5 +1,8 @@+-- Disable this warning because we are re-exporting things.+{-# OPTIONS_GHC -Wno-missing-import-lists #-}+ -- |--- Module : Grisette.Core+-- Module : Grisette -- Copyright : (c) Sirui Lu 2021-2023 -- License : BSD-3-Clause (see the LICENSE file) --
src/Grisette/Backend/SBV.hs view
@@ -1,3 +1,6 @@+-- Disable this warning because we are re-exporting things.+{-# OPTIONS_GHC -Wno-missing-import-lists #-}+ -- | -- Module : Grisette.Backend.SBV -- Copyright : (c) Sirui Lu 2021-2023@@ -34,3 +37,14 @@ import qualified Data.SBV as SBV import Grisette.Backend.SBV.Data.SMT.Solving+ ( ApproximationConfig (..),+ ExtraConfig (..),+ GrisetteSMTConfig (..),+ SolvingFailure (..),+ approx,+ clearApprox,+ clearTimeout,+ precise,+ withApprox,+ withTimeout,+ )
src/Grisette/Backend/SBV/Data/SMT/Lowering.hs view
@@ -32,54 +32,125 @@ ) where -import Control.Monad.State.Strict-import Data.Bifunctor+import Data.Bifunctor (Bifunctor (bimap, first, second)) import Data.Bits-import Data.Dynamic-import Data.Foldable-import Data.Kind-import Data.Maybe+ ( Bits (complement, rotate, shift, xor, (.&.), (.|.)),+ )+import Data.Dynamic (Typeable, fromDyn, toDyn)+import Data.Foldable (Foldable (foldl'), asum)+import Data.Kind (Type)+import Data.Maybe (fromMaybe) import qualified Data.SBV as SBV import qualified Data.SBV.Control as SBVC import qualified Data.SBV.Internals as SBVI import Data.Type.Equality (type (~~))-import Data.Typeable+import Data.Typeable (Proxy (Proxy), type (:~:) (Refl)) import GHC.Exts (sortWith)-import GHC.Natural-import GHC.Stack+import GHC.Stack (HasCallStack) import GHC.TypeNats+ ( KnownNat,+ Nat,+ natVal,+ type (+),+ type (-),+ type (<=),+ ) import {-# SOURCE #-} Grisette.Backend.SBV.Data.SMT.Solving+ ( ApproximationConfig (Approx, NoApprox),+ ExtraConfig (integerApprox),+ GrisetteSMTConfig (GrisetteSMTConfig),+ TermTy,+ ) import Grisette.Backend.SBV.Data.SMT.SymBiMap-import Grisette.Core.Data.BV+ ( SymBiMap,+ addBiMap,+ addBiMapIntermediate,+ emptySymBiMap,+ findStringToSymbol,+ lookupTerm,+ sizeBiMap,+ )+import Grisette.Core.Data.BV (IntN (IntN, unIntN), WordN (WordN)) import Grisette.Core.Data.Class.ModelOps+ ( ModelOps (emptyModel, insertValue),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( conTerm,+ symTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm+ ( SomeTerm (SomeTerm),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( SomeTypedSymbol (SomeTypedSymbol),+ SupportedPrim (withPrim),+ Term+ ( AbsNumTerm,+ AddNumTerm,+ AndBitsTerm,+ AndTerm,+ BVConcatTerm,+ BVExtendTerm,+ BVSelectTerm,+ BVToSignedTerm,+ BVToUnsignedTerm,+ BinaryTerm,+ ComplementBitsTerm,+ ConTerm,+ DivBoundedIntegralTerm,+ DivIntegralTerm,+ EqvTerm,+ GeneralFunApplyTerm,+ ITETerm,+ LENumTerm,+ LTNumTerm,+ ModBoundedIntegralTerm,+ ModIntegralTerm,+ NotTerm,+ OrBitsTerm,+ OrTerm,+ QuotBoundedIntegralTerm,+ QuotIntegralTerm,+ RemBoundedIntegralTerm,+ RemIntegralTerm,+ RotateBitsTerm,+ ShiftBitsTerm,+ SignumNumTerm,+ SymTerm,+ TabularFunApplyTerm,+ TernaryTerm,+ TimesNumTerm,+ UMinusNumTerm,+ UnaryTerm,+ XorBitsTerm+ ),+ TypedSymbol (IndexedSymbol),+ buildGeneralFun,+ someTypedSymbol,+ withSymbolSupported,+ type (-->),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils-import Grisette.IR.SymPrim.Data.Prim.Model as PM+ ( introSupportedPrimConstraint,+ )+import Grisette.IR.SymPrim.Data.Prim.Model as PM (Model) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool+ ( pevalEqvTerm,+ pevalITETerm,+ ) import Grisette.IR.SymPrim.Data.TabularFun+ ( type (=->) (TabularFun),+ ) import Grisette.Utils.Parameterized+ ( KnownProof (KnownProof),+ LeqProof (LeqProof),+ unsafeAxiom,+ unsafeKnownProof,+ unsafeLeqProof,+ withKnownProof,+ ) import qualified Type.Reflection as R-import Unsafe.Coerce -cachedResult ::- forall integerBitWidth a.- (SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>- Term a ->- State SymBiMap (Maybe (TermTy integerBitWidth a))-cachedResult t = gets $ \m -> do- d <- lookupTerm (SomeTerm t) m- Just $ fromDyn d undefined--addResult ::- forall integerBitWidth a.- (SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>- Term a ->- TermTy integerBitWidth a ->- State SymBiMap ()-addResult tm sbvtm = modify $ addBiMapIntermediate (SomeTerm tm) (toDyn sbvtm)- translateTypeError :: (HasCallStack) => R.TypeRep a -> b translateTypeError ta = error $@@ -144,7 +215,7 @@ lowerTFunCon config v _ -> translateTypeError (R.typeRep @a) _ -> translateTypeError (R.typeRep @a)-lowerValue config v = translateTypeError (R.typeRep @a)+lowerValue _ _ = translateTypeError (R.typeRep @a) lowerTFunCon :: forall integerBitWidth a b.@@ -154,9 +225,9 @@ (TermTy integerBitWidth a -> TermTy integerBitWidth b) lowerTFunCon config@ResolvedConfig {} (TabularFun l d) = go l d where- go [] d v = lowerValue config d+ go [] d _ = lowerValue config d go ((x, r) : xs) d v = SBV.ite (lowerValue config x SBV..== v) (lowerValue config r) (go xs d v)-lowerTFunCon _ (TabularFun l d) = translateTypeError (R.typeRep @a)+lowerTFunCon _ TabularFun {} = translateTypeError (R.typeRep @a) buildUTFun11 :: forall integerBitWidth s1 s2 a.
src/Grisette/Backend/SBV/Data/SMT/Solving.hs view
@@ -37,35 +37,59 @@ ) where -import Control.DeepSeq-import Control.Exception-import Control.Monad.Except-import Control.Monad.IO.Class+import Control.DeepSeq (NFData)+import Control.Exception (handle)+import Control.Monad.IO.Class (liftIO) import qualified Data.HashSet as S-import Data.Hashable-import Data.Kind+import Data.Hashable (Hashable)+import Data.Kind (Type) import Data.List (partition)-import Data.Maybe+import Data.Maybe (fromJust) import qualified Data.SBV as SBV import Data.SBV.Control (Query) import qualified Data.SBV.Control as SBVC-import GHC.TypeNats+import GHC.TypeNats (KnownNat, Nat) import Grisette.Backend.SBV.Data.SMT.Lowering-import Grisette.Core.Data.BV-import Grisette.Core.Data.Class.Bool+ ( SymBiMap,+ lowerSinglePrim,+ lowerSinglePrimCached,+ parseModel,+ )+import Grisette.Core.Data.BV (IntN, WordN)+import Grisette.Core.Data.Class.Bool (LogicalOp (nots, (&&~))) import Grisette.Core.Data.Class.CEGISSolver-import Grisette.Core.Data.Class.Evaluate+ ( CEGISCondition (CEGISCondition),+ CEGISSolver (cegisMultiInputs),+ )+import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym)) import Grisette.Core.Data.Class.ExtractSymbolics-import Grisette.Core.Data.Class.GenSym+ ( ExtractSymbolics (extractSymbolics),+ ) import Grisette.Core.Data.Class.ModelOps-import Grisette.Core.Data.Class.Solvable-import Grisette.Core.Data.Class.Solver+ ( ModelOps (exact, exceptFor),+ SymbolSetOps (isEmptySet),+ )+import Grisette.Core.Data.Class.Solvable (Solvable (con))+import Grisette.Core.Data.Class.Solver (Solver (solve, solveAll, solveMulti)) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( conTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( SomeTypedSymbol (SomeTypedSymbol),+ Term,+ type (-->),+ ) import Grisette.IR.SymPrim.Data.Prim.Model as PM+ ( Model,+ SymbolSet (unSymbolSet),+ equation,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool-import Grisette.IR.SymPrim.Data.SymPrim-import Grisette.IR.SymPrim.Data.TabularFun+ ( pevalNotTerm,+ pevalOrTerm,+ )+import Grisette.IR.SymPrim.Data.SymPrim (SymBool (SymBool))+import Grisette.IR.SymPrim.Data.TabularFun (type (=->)) import Language.Haskell.TH.Syntax (Lift) -- $setup@@ -76,7 +100,7 @@ type Aux :: Bool -> Nat -> Type type family Aux o n where- Aux 'True n = SBV.SInteger+ Aux 'True _ = SBV.SInteger Aux 'False n = SBV.SInt n type IsZero :: Nat -> Bool@@ -88,8 +112,8 @@ type family TermTy bitWidth b where TermTy _ Bool = SBV.SBool TermTy n Integer = Aux (IsZero n) n- TermTy n (IntN x) = SBV.SBV (SBV.IntN x)- TermTy n (WordN x) = SBV.SBV (SBV.WordN x)+ TermTy _ (IntN x) = SBV.SBV (SBV.IntN x)+ TermTy _ (WordN x) = SBV.SBV (SBV.WordN x) TermTy n (a =-> b) = TermTy n a -> TermTy n b TermTy n (a --> b) = TermTy n a -> TermTy n b TermTy _ v = v@@ -325,7 +349,7 @@ instance CEGISSolver (GrisetteSMTConfig n) SolvingFailure where cegisMultiInputs ::- forall inputs spec.+ forall inputs. (ExtractSymbolics inputs, EvaluateSym inputs) => GrisetteSMTConfig n -> [inputs] ->
src/Grisette/Backend/SBV/Data/SMT/Solving.hs-boot view
@@ -13,16 +13,18 @@ ) where -import Data.Kind+import Data.Kind (Type) import qualified Data.SBV as SBV-import GHC.TypeNats-import Grisette.Core.Data.BV+import GHC.TypeNats (KnownNat, Nat)+import Grisette.Core.Data.BV (IntN, WordN) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term-import Grisette.IR.SymPrim.Data.TabularFun+ ( type (-->),+ )+import Grisette.IR.SymPrim.Data.TabularFun (type (=->)) type Aux :: Bool -> Nat -> Type type family Aux o n where- Aux 'True n = SBV.SInteger+ Aux 'True _ = SBV.SInteger Aux 'False n = SBV.SInt n type IsZero :: Nat -> Bool@@ -34,8 +36,8 @@ type family TermTy bitWidth b where TermTy _ Bool = SBV.SBool TermTy n Integer = Aux (IsZero n) n- TermTy n (IntN x) = SBV.SBV (SBV.IntN x)- TermTy n (WordN x) = SBV.SBV (SBV.WordN x)+ TermTy _ (IntN x) = SBV.SBV (SBV.IntN x)+ TermTy _ (WordN x) = SBV.SBV (SBV.WordN x) TermTy n (a =-> b) = TermTy n a -> TermTy n b TermTy n (a --> b) = TermTy n a -> TermTy n b TermTy _ v = v
src/Grisette/Backend/SBV/Data/SMT/SymBiMap.hs view
@@ -19,11 +19,15 @@ ) where -import Data.Dynamic+import Data.Dynamic (Dynamic) import qualified Data.HashMap.Strict as M-import GHC.Stack+import GHC.Stack (HasCallStack) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm+ ( SomeTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( SomeTypedSymbol,+ ) data SymBiMap = SymBiMap { biMapToSBV :: M.HashMap SomeTerm Dynamic,
src/Grisette/Core.hs view
@@ -1,5 +1,7 @@ {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE Trustworthy #-}+-- Disable this warning because we are re-exporting things.+{-# OPTIONS_GHC -Wno-missing-import-lists #-} -- | -- Module : Grisette.Core@@ -1011,33 +1013,188 @@ import Generics.Deriving (Default (..), Default1 (..)) import Grisette.Core.BuiltinUnionWrappers+ ( mrgAssertionViolation,+ mrgAssumptionViolation,+ mrgFalse,+ mrgInL,+ mrgInR,+ mrgJust,+ mrgLeft,+ mrgNothing,+ mrgRight,+ mrgTrue,+ mrgTuple2,+ mrgTuple3,+ mrgUnit,+ ) import Grisette.Core.Control.Exception+ ( AssertionError (..),+ VerificationConditions (..),+ symAssert,+ symAssume,+ ) import Grisette.Core.Control.Monad.CBMCExcept+ ( CBMCEither (..),+ CBMCExceptT (..),+ cbmcExcept,+ mapCBMCExceptT,+ withCBMCExceptT,+ ) import Grisette.Core.Control.Monad.Class.MonadParallelUnion-import Grisette.Core.Control.Monad.Union+ ( MonadParallelUnion (..),+ )+import Grisette.Core.Control.Monad.Union (MonadUnion) import Grisette.Core.Control.Monad.UnionM+ ( IsConcrete,+ UnionM,+ liftToMonadUnion,+ unionSize,+ (#~),+ ) import Grisette.Core.Data.Class.BitVector+ ( BV (..),+ SizedBV (..),+ bvExtract,+ sizedBVExtract,+ ) import Grisette.Core.Data.Class.Bool+ ( ITEOp (..),+ LogicalOp (..),+ SEq (..),+ SymBoolOp,+ ) import Grisette.Core.Data.Class.CEGISSolver+ ( CEGISCondition (..),+ CEGISSolver (..),+ cegis,+ cegisExcept,+ cegisExceptMultiInputs,+ cegisExceptStdVC,+ cegisExceptStdVCMultiInputs,+ cegisExceptVC,+ cegisExceptVCMultiInputs,+ cegisPostCond,+ cegisPrePost,+ ) import Grisette.Core.Data.Class.Error+ ( TransformError (..),+ symAssertTransformableError,+ symAssertWith,+ symThrowTransformableError,+ ) import Grisette.Core.Data.Class.Evaluate+ ( EvaluateSym (..),+ evaluateSymToCon,+ ) import Grisette.Core.Data.Class.ExtractSymbolics-import Grisette.Core.Data.Class.Function-import Grisette.Core.Data.Class.GPretty+ ( ExtractSymbolics (..),+ )+import Grisette.Core.Data.Class.Function (Function (..))+import Grisette.Core.Data.Class.GPretty (GPretty (..)) import Grisette.Core.Data.Class.GenSym+ ( EnumGenBound (..),+ EnumGenUpperBound (..),+ Fresh,+ FreshIdent (..),+ FreshIndex (..),+ FreshT,+ GenSym (..),+ GenSymSimple (..),+ ListSpec (..),+ MonadFresh (..),+ SimpleListSpec (..),+ choose,+ chooseFresh,+ chooseSimple,+ chooseSimpleFresh,+ chooseUnion,+ chooseUnionFresh,+ derivedNoSpecFresh,+ derivedNoSpecSimpleFresh,+ derivedSameShapeSimpleFresh,+ genSym,+ genSymSimple,+ name,+ nameWithInfo,+ runFresh,+ runFreshT,+ ) import Grisette.Core.Data.Class.Mergeable+ ( DynamicSortedIdx (..),+ Mergeable (..),+ Mergeable1 (..),+ Mergeable2 (..),+ Mergeable3 (..),+ MergingStrategy (..),+ StrategyList (..),+ buildStrategyList,+ derivedRootStrategy,+ product2Strategy,+ resolveStrategy,+ resolveStrategy',+ rootStrategy1,+ rootStrategy2,+ rootStrategy3,+ wrapStrategy,+ ) import Grisette.Core.Data.Class.ModelOps-import Grisette.Core.Data.Class.SOrd+ ( ModelOps (..),+ ModelRep (..),+ SymbolSetOps (..),+ SymbolSetRep (..),+ )+import Grisette.Core.Data.Class.SOrd (SOrd (..)) import Grisette.Core.Data.Class.SafeArith+ ( SafeDivision (..),+ SafeLinearArith (..),+ SymIntegerOp,+ ) import Grisette.Core.Data.Class.SimpleMergeable-import Grisette.Core.Data.Class.Solvable+ ( SimpleMergeable (..),+ SimpleMergeable1 (..),+ SimpleMergeable2 (..),+ UnionLike (..),+ UnionPrjOp (..),+ merge,+ mrgIf,+ mrgIte1,+ mrgIte2,+ mrgSingle,+ onUnion,+ onUnion2,+ onUnion3,+ onUnion4,+ simpleMerge,+ pattern IfU,+ pattern SingleU,+ )+import Grisette.Core.Data.Class.Solvable (Solvable (..), pattern Con) import Grisette.Core.Data.Class.Solver+ ( Solver (..),+ UnionWithExcept (..),+ solveExcept,+ solveMultiExcept,+ ) import Grisette.Core.Data.Class.Substitute-import Grisette.Core.Data.Class.ToCon-import Grisette.Core.Data.Class.ToSym+ ( SubstituteSym (..),+ SubstituteSym' (..),+ )+import Grisette.Core.Data.Class.ToCon (ToCon (..))+import Grisette.Core.Data.Class.ToSym (ToSym (..)) import Grisette.Core.Data.FileLocation+ ( FileLocation (..),+ ilocsym,+ nameWithLoc,+ slocsym,+ ) import Grisette.Core.Data.MemoUtils-import Grisette.Core.TH+ ( htmemo,+ htmemo2,+ htmemo3,+ htmemoFix,+ htmup,+ )+import Grisette.Core.TH (makeUnionWrapper, makeUnionWrapper') -- $setup -- >>> import Grisette.Core
src/Grisette/Core/BuiltinUnionWrappers.hs view
@@ -30,10 +30,10 @@ ) where -import Data.Functor.Sum-import Grisette.Core.Control.Exception-import Grisette.Core.Data.Class.SimpleMergeable-import Grisette.Core.TH+import Data.Functor.Sum (Sum)+import Grisette.Core.Control.Exception (VerificationConditions)+import Grisette.Core.Data.Class.SimpleMergeable (mrgSingle)+import Grisette.Core.TH (makeUnionWrapper, makeUnionWrapper') $(makeUnionWrapper "mrg" ''Bool) $(makeUnionWrapper' ["mrgUnit"] ''())
src/Grisette/Core/Control/Exception.hs view
@@ -24,23 +24,33 @@ ) where -import Control.DeepSeq-import Control.Exception-import Control.Monad.Except-import GHC.Generics-import Generics.Deriving-import Grisette.Core.Control.Monad.Union-import Grisette.Core.Data.Class.Bool+import Control.DeepSeq (NFData)+import Control.Exception (ArithException, ArrayException)+import Control.Monad.Except (MonadError)+import GHC.Generics (Generic)+import Generics.Deriving (Default (Default))+import Grisette.Core.Control.Monad.Union (MonadUnion)+import Grisette.Core.Data.Class.Bool (SEq) import Grisette.Core.Data.Class.Error-import Grisette.Core.Data.Class.Evaluate+ ( TransformError (transformError),+ symAssertTransformableError,+ )+import Grisette.Core.Data.Class.Evaluate (EvaluateSym) import Grisette.Core.Data.Class.ExtractSymbolics-import Grisette.Core.Data.Class.Mergeable+ ( ExtractSymbolics,+ )+import Grisette.Core.Data.Class.Mergeable (Mergeable) import Grisette.Core.Data.Class.SOrd+ ( SOrd (symCompare, (<=~), (<~), (>=~), (>~)),+ ) import Grisette.Core.Data.Class.SimpleMergeable-import Grisette.Core.Data.Class.Solvable-import Grisette.Core.Data.Class.ToCon-import Grisette.Core.Data.Class.ToSym-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim+ ( SimpleMergeable,+ mrgSingle,+ )+import Grisette.Core.Data.Class.Solvable (Solvable (con))+import Grisette.Core.Data.Class.ToCon (ToCon)+import Grisette.Core.Data.Class.ToSym (ToSym)+import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool) -- $setup -- >>> import Grisette.Core
src/Grisette/Core/Control/Monad/CBMCExcept.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveLift #-} {-# LANGUAGE DerivingStrategies #-}@@ -30,30 +31,70 @@ ) where +#if MIN_VERSION_base(4,18,0) import Control.Applicative-import Control.DeepSeq-import Control.Monad+ ( Alternative (empty, (<|>)),+ )+#else+import Control.Applicative+ ( Alternative (empty, (<|>)),+ Applicative (liftA2),+ )+#endif+import Control.DeepSeq (NFData)+import Control.Monad (MonadPlus (mplus, mzero)) import qualified Control.Monad.Except as OrigExcept import qualified Control.Monad.Fail as Fail-import Control.Monad.Fix-import Control.Monad.Trans-import Control.Monad.Zip+import Control.Monad.Fix (MonadFix (mfix))+import Control.Monad.Trans (MonadIO (liftIO), MonadTrans (lift))+import Control.Monad.Zip (MonadZip (mzipWith)) import Data.Functor.Classes-import Data.Functor.Contravariant-import Data.Hashable-import GHC.Generics-import Grisette.Core.Data.Class.Bool-import Grisette.Core.Data.Class.Evaluate+ ( Eq1 (liftEq),+ Ord1 (liftCompare),+ Read1 (liftReadList, liftReadsPrec),+ Show1 (liftShowList, liftShowsPrec),+ compare1,+ eq1,+ readsData,+ readsPrec1,+ readsUnaryWith,+ showsPrec1,+ showsUnaryWith,+ )+import Data.Functor.Contravariant (Contravariant (contramap))+import Data.Hashable (Hashable)+import GHC.Generics (Generic, Generic1)+import Grisette.Core.Data.Class.Bool (SEq ((==~)))+import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym)) import Grisette.Core.Data.Class.ExtractSymbolics+ ( ExtractSymbolics (extractSymbolics),+ ) import Grisette.Core.Data.Class.GenSym+ ( GenSym (fresh),+ GenSymSimple (simpleFresh),+ derivedNoSpecFresh,+ derivedSameShapeSimpleFresh,+ ) import Grisette.Core.Data.Class.Mergeable-import Grisette.Core.Data.Class.SOrd+ ( Mergeable (rootStrategy),+ Mergeable1 (liftRootStrategy),+ MergingStrategy (NoStrategy, SimpleStrategy, SortedStrategy),+ rootStrategy1,+ wrapStrategy,+ )+import Grisette.Core.Data.Class.SOrd (SOrd (symCompare, (<=~), (<~), (>=~), (>~))) import Grisette.Core.Data.Class.SimpleMergeable-import Grisette.Core.Data.Class.Solver-import Grisette.Core.Data.Class.ToCon-import Grisette.Core.Data.Class.ToSym+ ( SimpleMergeable (mrgIte),+ SimpleMergeable1 (liftMrgIte),+ UnionLike (mergeWithStrategy, mrgIfWithStrategy, single, unionIf),+ merge,+ mrgIf,+ )+import Grisette.Core.Data.Class.Solver (UnionWithExcept (extractUnionExcept))+import Grisette.Core.Data.Class.ToCon (ToCon (toCon))+import Grisette.Core.Data.Class.ToSym (ToSym (toSym)) import Language.Haskell.TH.Syntax (Lift)-import Unsafe.Coerce+import Unsafe.Coerce (unsafeCoerce) -- | A wrapper type for 'Either'. Uses different merging strategies. newtype CBMCEither a b = CBMCEither {runCBMCEither :: Either a b}
src/Grisette/Core/Control/Monad/Class/MonadParallelUnion.hs view
@@ -13,21 +13,22 @@ ) where -import Control.DeepSeq-import Control.Monad.Cont-import Control.Monad.Except-import Control.Monad.Identity+import Control.DeepSeq (NFData)+import Control.Monad.Except (ExceptT (ExceptT), runExceptT)+import Control.Monad.Identity (IdentityT (IdentityT, runIdentityT)) import qualified Control.Monad.RWS.Lazy as RWSLazy import qualified Control.Monad.RWS.Strict as RWSStrict-import Control.Monad.Reader+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+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 Grisette.Core.Data.Class.Mergeable+import Grisette.Core.Data.Class.Mergeable (Mergeable) import Grisette.Core.Data.Class.SimpleMergeable-import Grisette.Lib.Control.Monad+ ( UnionLike,+ merge,+ ) -- | Parallel union monad. --
src/Grisette/Core/Control/Monad/Union.hs view
@@ -19,7 +19,7 @@ ) where -import Grisette.Core.Data.Class.SimpleMergeable+import Grisette.Core.Data.Class.SimpleMergeable (UnionLike) -- $setup -- >>> import Grisette.Core
src/Grisette/Core/Control/Monad/UnionM.hs view
@@ -8,6 +8,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskellQuotes #-} {-# LANGUAGE Trustworthy #-}@@ -38,47 +39,92 @@ ) where -import Control.DeepSeq-import Control.Monad.Identity (Identity (..))-import Control.Parallel.Strategies+import Control.DeepSeq (NFData (rnf), NFData1 (liftRnf), force, rnf1)+import Control.Parallel.Strategies (rpar, rseq, runEval) import Data.Functor.Classes+ ( Eq1 (liftEq),+ Show1 (liftShowsPrec),+ showsPrec1,+ ) import qualified Data.HashMap.Lazy as HML-import Data.Hashable-import Data.IORef-import Data.String-import GHC.IO hiding (evaluate)-import GHC.TypeNats+import Data.Hashable (Hashable (hashWithSalt))+import Data.String (IsString (fromString))+import GHC.TypeNats (KnownNat, type (<=)) import Grisette.Core.Control.Monad.CBMCExcept+ ( CBMCEither (runCBMCEither),+ ) import Grisette.Core.Control.Monad.Class.MonadParallelUnion-import Grisette.Core.Control.Monad.Union-import Grisette.Core.Data.BV+ ( MonadParallelUnion (parBindUnion),+ )+import Grisette.Core.Control.Monad.Union (MonadUnion)+import Grisette.Core.Data.BV (IntN, WordN) import Grisette.Core.Data.Class.Bool-import Grisette.Core.Data.Class.Evaluate+ ( ITEOp (ites),+ LogicalOp (implies, nots, xors, (&&~), (||~)),+ SEq ((==~)),+ )+import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym)) import Grisette.Core.Data.Class.ExtractSymbolics-import Grisette.Core.Data.Class.Function+ ( ExtractSymbolics (extractSymbolics),+ )+import Grisette.Core.Data.Class.Function (Function (Arg, Ret, (#))) import Grisette.Core.Data.Class.GPretty+ ( GPretty (gpretty),+ groupedEnclose,+ ) import Grisette.Core.Data.Class.GenSym+ ( GenSym (fresh),+ GenSymSimple (simpleFresh),+ ) import Grisette.Core.Data.Class.Mergeable+ ( Mergeable (rootStrategy),+ Mergeable1 (liftRootStrategy),+ MergingStrategy (SimpleStrategy),+ ) import Grisette.Core.Data.Class.SOrd+ ( SOrd (symCompare, (<=~), (<~), (>=~), (>~)),+ ) import Grisette.Core.Data.Class.SimpleMergeable+ ( SimpleMergeable (mrgIte),+ SimpleMergeable1 (liftMrgIte),+ UnionLike (mergeWithStrategy, mrgIfWithStrategy, single, unionIf),+ UnionPrjOp (ifView, leftMost, singleView),+ merge,+ mrgIf,+ mrgSingle,+ simpleMerge,+ (#~),+ ) import Grisette.Core.Data.Class.Solvable-import Grisette.Core.Data.Class.Solver-import Grisette.Core.Data.Class.Substitute-import Grisette.Core.Data.Class.ToCon-import Grisette.Core.Data.Class.ToSym+ ( Solvable (con, conView, iinfosym, isym, sinfosym, ssym),+ pattern Con,+ )+import Grisette.Core.Data.Class.Solver (UnionWithExcept (extractUnionExcept))+import Grisette.Core.Data.Class.ToCon (ToCon (toCon))+import Grisette.Core.Data.Class.ToSym (ToSym (toSym)) import Grisette.Core.Data.Union+ ( Union (If, Single),+ fullReconstruct,+ ifWithStrategy,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( LinkedRep,+ SupportedPrim,+ type (-->),+ ) import Grisette.IR.SymPrim.Data.SymPrim-import Grisette.IR.SymPrim.Data.TabularFun-import Language.Haskell.TH.Syntax+ ( AllSyms (allSymsS),+ SymBool,+ SymIntN,+ SymInteger,+ SymWordN,+ type (-~>),+ type (=~>),+ )+import Grisette.IR.SymPrim.Data.TabularFun (type (=->))+import Language.Haskell.TH.Syntax (Lift (lift, liftTyped)) import Language.Haskell.TH.Syntax.Compat (unTypeSplice) -#if MIN_VERSION_prettyprinter(1,7,0)-import Prettyprinter-#else-import Data.Text.Prettyprint.Doc-#endif- -- $setup -- >>> import Grisette.Core -- >>> import Grisette.IR.SymPrim@@ -238,11 +284,11 @@ wrapBracket l r p = showChar l . p . showChar r instance Show1 UnionM where- liftShowsPrec sp sl i (UAny a) =+ liftShowsPrec sp sl _ (UAny a) = wrapBracket '<' '>' . liftShowsPrecUnion sp sl 0 $ a- liftShowsPrec sp sl i (UMrg _ a) =+ liftShowsPrec sp sl _ (UMrg _ a) = wrapBracket '{' '}' . liftShowsPrecUnion sp sl 0 $ a
src/Grisette/Core/Control/Monad/UnionM.hs-boot view
@@ -4,11 +4,9 @@ module Grisette.Core.Control.Monad.UnionM (UnionM (..)) where -import Data.IORef-import Grisette.Core.Data.Class.Bool-import Grisette.Core.Data.Class.Mergeable-import Grisette.Core.Data.Class.SimpleMergeable-import Grisette.Core.Data.Union+import Grisette.Core.Data.Class.Mergeable (MergingStrategy)+import Grisette.Core.Data.Class.SimpleMergeable (UnionLike)+import Grisette.Core.Data.Union (Union) data UnionM a where -- | 'UnionM' with no 'Mergeable' knowledge.
src/Grisette/Core/Data/BV.hs view
@@ -44,28 +44,92 @@ ) where -import Control.Applicative-import Control.DeepSeq+import Control.Applicative (Alternative ((<|>)))+import Control.DeepSeq (NFData (rnf)) import Control.Exception+ ( ArithException (Overflow),+ Exception (displayException),+ throw,+ ) import Data.Bits-import Data.CallStack-import Data.Hashable-import Data.Maybe-import Data.Proxy-import Data.Typeable+ ( Bits+ ( bit,+ bitSize,+ bitSizeMaybe,+ clearBit,+ complement,+ complementBit,+ isSigned,+ popCount,+ rotate,+ rotateL,+ rotateR,+ setBit,+ shift,+ shiftL,+ shiftR,+ testBit,+ unsafeShiftL,+ unsafeShiftR,+ xor,+ zeroBits,+ (.&.),+ (.|.)+ ),+ FiniteBits (countLeadingZeros, countTrailingZeros, finiteBitSize),+ )+import Data.Hashable (Hashable (hashWithSalt))+import Data.Maybe (fromMaybe, isJust)+import Data.Proxy (Proxy (Proxy))+import Data.Typeable (type (:~:) (Refl)) import GHC.Enum-import GHC.Generics+ ( boundedEnumFrom,+ boundedEnumFromThen,+ predError,+ succError,+ toEnumError,+ )+import GHC.Generics (Generic) import GHC.Read-import GHC.Real+ ( Read (readListPrec, readPrec),+ parens,+ readListDefault,+ readListPrecDefault,+ readNumber,+ )+import GHC.Real ((%)) import GHC.TypeNats+ ( KnownNat,+ Nat,+ natVal,+ sameNat,+ type (+),+ type (<=),+ ) import Grisette.Core.Data.Class.BitVector+ ( BV (bvConcat, bvExt, bvSelect, bvSext, bvZext),+ BVSignConversion (toSigned, toUnsigned),+ SizedBV (sizedBVConcat, sizedBVExt, sizedBVSelect, sizedBVSext, sizedBVZext),+ ) import Grisette.Utils.Parameterized-import Language.Haskell.TH.Syntax-import Numeric+ ( KnownProof (KnownProof),+ LeqProof (LeqProof),+ knownAdd,+ leqAddPos,+ unsafeKnownProof,+ unsafeLeqProof,+ )+import Language.Haskell.TH.Syntax (Lift (liftTyped))+import Numeric (showHex, showIntAtBase) import qualified Test.QuickCheck as QC-import Text.ParserCombinators.ReadP (skipSpaces, string)+import Text.ParserCombinators.ReadP (string) import Text.ParserCombinators.ReadPrec-import Text.Read+ ( ReadPrec,+ get,+ look,+ pfail,+ )+import Text.Read (lift) import qualified Text.Read.Lex as L data BitwidthMismatch = BitwidthMismatch@@ -84,29 +148,29 @@ data SomeWordN where SomeWordN :: (KnownNat n, 1 <= n) => WordN n -> SomeWordN -unarySomeWordN :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> r) -> SomeWordN -> r+unarySomeWordN :: (forall n. (KnownNat n, 1 <= n) => WordN n -> r) -> SomeWordN -> r unarySomeWordN op (SomeWordN (w :: WordN w)) = op w {-# INLINE unarySomeWordN #-} -unarySomeWordNR1 :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n) -> SomeWordN -> SomeWordN+unarySomeWordNR1 :: (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n) -> SomeWordN -> SomeWordN unarySomeWordNR1 op (SomeWordN (w :: WordN w)) = SomeWordN $ op w {-# INLINE unarySomeWordNR1 #-} -binSomeWordN :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> r) -> SomeWordN -> SomeWordN -> r+binSomeWordN :: (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> r) -> SomeWordN -> SomeWordN -> r binSomeWordN op (SomeWordN (l :: WordN l)) (SomeWordN (r :: WordN r)) = case sameNat (Proxy @l) (Proxy @r) of Just Refl -> op l r Nothing -> throw BitwidthMismatch {-# INLINE binSomeWordN #-} -binSomeWordNR1 :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> WordN n) -> SomeWordN -> SomeWordN -> SomeWordN+binSomeWordNR1 :: (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> WordN n) -> SomeWordN -> SomeWordN -> SomeWordN binSomeWordNR1 op (SomeWordN (l :: WordN l)) (SomeWordN (r :: WordN r)) = case sameNat (Proxy @l) (Proxy @r) of Just Refl -> SomeWordN $ op l r Nothing -> throw BitwidthMismatch {-# INLINE binSomeWordNR1 #-} -binSomeWordNR2 :: (HasCallStack) => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> (WordN n, WordN n)) -> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)+binSomeWordNR2 :: (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> (WordN n, WordN n)) -> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN) binSomeWordNR2 op (SomeWordN (l :: WordN l)) (SomeWordN (r :: WordN r)) = case sameNat (Proxy @l) (Proxy @r) of Just Refl ->@@ -699,7 +763,7 @@ where n = fromIntegral $ natVal (Proxy @n) res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeWordN- res p1 p2 =+ res _ _ = case ( unsafeKnownProof @ix (fromIntegral ix), unsafeKnownProof @w (fromIntegral w), unsafeLeqProof @1 @w,@@ -709,7 +773,7 @@ SomeWordN $ sizedBVSelect (Proxy @ix) (Proxy @w) a instance BV SomeIntN where- bvConcat l r = toSigned $ bvConcat (toUnsigned l) (toUnsigned l)+ bvConcat l r = toSigned $ bvConcat (toUnsigned l) (toUnsigned r) {-# INLINE bvConcat #-} bvZext l = toSigned . bvZext l . toUnsigned {-# INLINE bvZext #-}
src/Grisette/Core/Data/Class/BitVector.hs view
@@ -28,9 +28,17 @@ ) where -import Data.Proxy-import GHC.TypeNats+import Data.Proxy (Proxy (Proxy))+import GHC.TypeNats (KnownNat, type (+), type (-), type (<=)) import Grisette.Utils.Parameterized+ ( KnownProof (KnownProof),+ LeqProof (LeqProof),+ addNat,+ hasRepr,+ natRepr,+ subNat,+ unsafeLeqProof,+ ) -- $setup -- >>> import Grisette.Core
src/Grisette/Core/Data/Class/Bool.hs view
@@ -30,27 +30,59 @@ ) where -import Control.Monad.Except+import Control.Monad.Except (ExceptT (ExceptT)) import Control.Monad.Identity ( Identity (Identity), IdentityT (IdentityT), )-import Control.Monad.Trans.Maybe+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.Sum-import Data.Int+import Data.Functor.Sum (Sum)+import Data.Int (Int16, Int32, Int64, Int8) import qualified Data.Text as T-import Data.Word-import GHC.TypeNats+import Data.Word (Word16, Word32, Word64, Word8)+import GHC.TypeNats (KnownNat, type (<=)) import Generics.Deriving-import Grisette.Core.Data.BV+ ( Default (Default),+ Generic (Rep, from),+ K1 (K1),+ M1 (M1),+ U1,+ V1,+ type (:*:) ((:*:)),+ type (:+:) (L1, R1),+ )+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN) import {-# SOURCE #-} Grisette.Core.Data.Class.SimpleMergeable-import Grisette.Core.Data.Class.Solvable+ ( SimpleMergeable,+ )+import Grisette.Core.Data.Class.Solvable (Solvable (con)) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( LinkedRep,+ SupportedPrim,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool+ ( pevalAndTerm,+ pevalITETerm,+ pevalImplyTerm,+ pevalNotTerm,+ pevalOrTerm,+ pevalXorTerm,+ ) import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim+ ( SomeSymIntN,+ SomeSymWordN,+ SymBool (SymBool),+ SymIntN (SymIntN),+ SymInteger (SymInteger),+ SymWordN (SymWordN),+ binSomeSymIntNR1,+ binSomeSymWordNR1,+ type (-~>) (SymGeneralFun),+ type (=~>) (SymTabularFun),+ ) -- $setup -- >>> import Grisette.Core
src/Grisette/Core/Data/Class/Bool.hs-boot view
@@ -1,6 +1,6 @@-module Grisette.Core.Data.Class.Bool (LogicalOp (..)) where+module Grisette.Core.Data.Class.Bool (LogicalOp (..), ITEOp (..)) where -import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim+import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool) class LogicalOp b where -- | Symbolic disjunction
src/Grisette/Core/Data/Class/CEGISSolver.hs view
@@ -39,18 +39,25 @@ ) where -import GHC.Generics-import Generics.Deriving+import GHC.Generics (Generic)+import Generics.Deriving (Default (Default)) import Grisette.Core.Control.Exception-import Grisette.Core.Data.Class.Bool-import Grisette.Core.Data.Class.Evaluate+ ( VerificationConditions (AssertionViolation, AssumptionViolation),+ )+import Grisette.Core.Data.Class.Evaluate (EvaluateSym) import Grisette.Core.Data.Class.ExtractSymbolics-import Grisette.Core.Data.Class.Mergeable+ ( ExtractSymbolics,+ )+import Grisette.Core.Data.Class.Mergeable (Mergeable) import Grisette.Core.Data.Class.SimpleMergeable-import Grisette.Core.Data.Class.Solvable-import Grisette.Core.Data.Class.Solver-import Grisette.IR.SymPrim.Data.Prim.Model-import Grisette.IR.SymPrim.Data.SymPrim+ ( SimpleMergeable,+ UnionPrjOp,+ simpleMerge,+ )+import Grisette.Core.Data.Class.Solvable (Solvable (con))+import Grisette.Core.Data.Class.Solver (UnionWithExcept (extractUnionExcept))+import Grisette.IR.SymPrim.Data.Prim.Model (Model)+import Grisette.IR.SymPrim.Data.SymPrim (SymBool) -- $setup -- >>> import Grisette.Core
src/Grisette/Core/Data/Class/Error.hs view
@@ -21,17 +21,17 @@ ) where -import Control.Monad.Except-import Grisette.Core.Control.Monad.Union-import Grisette.Core.Data.Class.Bool-import Grisette.Core.Data.Class.Mergeable-import Grisette.Core.Data.Class.SimpleMergeable-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim+import Control.Monad.Except (MonadError (throwError))+import Grisette.Core.Control.Monad.Union (MonadUnion)+import Grisette.Core.Data.Class.Mergeable (Mergeable)+import Grisette.Core.Data.Class.SimpleMergeable (merge, mrgIf)+import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool) -- $setup -- >>> import Control.Exception -- >>> import Grisette.Core -- >>> import Grisette.IR.SymPrim+-- >>> import Control.Monad.Except -- >>> :set -XOverloadedStrings -- >>> :set -XFlexibleContexts
src/Grisette/Core/Data/Class/Evaluate.hs view
@@ -25,24 +25,34 @@ ) where -import Control.Monad.Except+import Control.Monad.Except (ExceptT (ExceptT)) import Control.Monad.Identity-import Control.Monad.Trans.Maybe+ ( 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.Sum-import Data.Int-import Data.Maybe+import Data.Functor.Sum (Sum)+import Data.Int (Int16, Int32, Int64, Int8)+import Data.Maybe (fromJust) import qualified Data.Text as T-import Data.Word-import GHC.TypeNats+import Data.Word (Word16, Word32, Word64, Word8)+import GHC.TypeNats (KnownNat, type (<=)) import Generics.Deriving+ ( Default (Default, unDefault),+ Generic (Rep, from, to),+ K1 (K1),+ M1 (M1),+ U1,+ type (:*:) ((:*:)),+ type (:+:) (L1, R1),+ ) import Generics.Deriving.Instances ()-import Grisette.Core.Data.BV-import Grisette.Core.Data.Class.ModelOps-import Grisette.Core.Data.Class.ToCon-import Grisette.IR.SymPrim.Data.Prim.Model+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)+import Grisette.Core.Data.Class.ToCon (ToCon (toCon))+import Grisette.IR.SymPrim.Data.Prim.Model (Model) -- $setup -- >>> import Grisette.Core
src/Grisette/Core/Data/Class/ExtractSymbolics.hs view
@@ -24,20 +24,33 @@ ) where -import Control.Monad.Except+import Control.Monad.Except (ExceptT (ExceptT)) import Control.Monad.Identity-import Control.Monad.Trans.Maybe+ ( 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.Sum-import Data.Int+import Data.Functor.Sum (Sum)+import Data.Int (Int16, Int32, Int64, Int8) import qualified Data.Text as T-import Data.Word-import GHC.TypeNats+import Data.Word (Word16, Word32, Word64, Word8)+import GHC.TypeNats (KnownNat, type (<=)) import Generics.Deriving-import Grisette.Core.Data.BV+ ( Default (Default, unDefault),+ Generic (Rep, from),+ K1 (unK1),+ M1 (unM1),+ U1,+ type (:*:) ((:*:)),+ type (:+:) (L1, R1),+ )+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN) import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.Model+ ( SymbolSet,+ ) -- $setup -- >>> import Grisette.Core
src/Grisette/Core/Data/Class/GPretty.hs view
@@ -18,27 +18,68 @@ ) where -import Control.Monad.Except+import Control.Monad.Except (ExceptT (ExceptT)) import Control.Monad.Identity-import Control.Monad.Trans.Maybe+ ( 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.Sum-import Data.Int-import Data.Proxy-import Data.String+import Data.Functor.Sum (Sum)+import Data.Int (Int16, Int32, Int64, Int8)+import Data.String (IsString (fromString)) import qualified Data.Text as T-import Data.Word+import Data.Word (Word16, Word32, Word64, Word8) import GHC.Generics-import GHC.TypeLits-import Generics.Deriving hiding (isNullary)-import Grisette.Core.Data.BV+ ( C,+ C1,+ Constructor (conFixity, conIsRecord, conName),+ D,+ Fixity (Infix, Prefix),+ Generic (Rep, from),+ K1 (K1),+ M1 (M1),+ S,+ Selector (selName),+ U1 (U1),+ V1,+ type (:*:) ((:*:)),+ type (:+:) (L1, R1),+ )+import GHC.TypeLits (KnownNat, type (<=))+import Generics.Deriving (Default (Default, unDefault))+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN) #if MIN_VERSION_prettyprinter(1,7,0) import Prettyprinter+ ( (<+>),+ align,+ encloseSep,+ flatAlt,+ group,+ nest,+ vcat,+ viaShow,+ vsep,+ Doc,+ Pretty(pretty),+ ) #else import Data.Text.Prettyprint.Doc+ ( (<+>),+ align,+ encloseSep,+ flatAlt,+ group,+ nest,+ vcat,+ viaShow,+ vsep,+ Doc,+ Pretty(pretty),+ ) #endif glist :: [Doc ann] -> Doc ann@@ -153,7 +194,7 @@ [ gprettyPrec' t n a, pretty s <+> gprettyPrec' t n b ]- gprettyPrec' t@Tup n (a :*: b) =+ gprettyPrec' t@Tup _ (a :*: b) = vcat [ gprettyPrec' t 0 a, "," <> flatAlt " " "" <> gprettyPrec' t 0 b@@ -309,7 +350,7 @@ (GPretty (m (Maybe a))) => GPretty (MaybeT m a) where- gprettyPrec i (MaybeT a) =+ gprettyPrec _ (MaybeT a) = group $ nest 2 $ vsep@@ -322,7 +363,7 @@ (GPretty (m (Either e a))) => GPretty (ExceptT e m a) where- gprettyPrec i (ExceptT a) =+ gprettyPrec _ (ExceptT a) = group $ nest 2 $ vsep@@ -335,7 +376,7 @@ (GPretty (m (a, w))) => GPretty (WriterLazy.WriterT w m a) where- gprettyPrec i (WriterLazy.WriterT a) =+ gprettyPrec _ (WriterLazy.WriterT a) = group $ nest 2 $ vsep@@ -347,7 +388,7 @@ (GPretty (m (a, w))) => GPretty (WriterStrict.WriterT w m a) where- gprettyPrec i (WriterStrict.WriterT a) =+ gprettyPrec _ (WriterStrict.WriterT a) = group $ nest 2 $ vsep@@ -357,7 +398,7 @@ -- Identity instance (GPretty a) => GPretty (Identity a) where- gprettyPrec i (Identity a) =+ gprettyPrec _ (Identity a) = group $ nest 2 $ vsep@@ -367,7 +408,7 @@ -- IdentityT instance (GPretty (m a)) => GPretty (IdentityT m a) where- gprettyPrec i (IdentityT a) =+ gprettyPrec _ (IdentityT a) = group $ nest 2 $ vsep
src/Grisette/Core/Data/Class/GenSym.hs view
@@ -66,43 +66,97 @@ ) where -import Control.DeepSeq-import Control.Monad.Cont+import Control.DeepSeq (NFData (rnf)) import Control.Monad.Except-import Control.Monad.Identity+ ( ExceptT (ExceptT),+ MonadError (catchError, throwError),+ )+import Control.Monad.Identity (Identity (runIdentity)) import Control.Monad.RWS.Class+ ( MonadRWS,+ MonadReader (ask, local),+ MonadState (get, put),+ MonadWriter (listen, pass, writer),+ asks,+ gets,+ ) import qualified Control.Monad.RWS.Lazy as RWSLazy import qualified Control.Monad.RWS.Strict as RWSStrict-import Control.Monad.Reader-import Control.Monad.Signatures-import Control.Monad.State+import Control.Monad.Reader (ReaderT (ReaderT))+import Control.Monad.Signatures (Catch) import qualified Control.Monad.State.Lazy as StateLazy import qualified Control.Monad.State.Strict as StateStrict-import Control.Monad.Trans.Maybe-import Control.Monad.Writer+import Control.Monad.Trans.Class+ ( MonadTrans (lift),+ )+import Control.Monad.Trans.Maybe (MaybeT (MaybeT)) import qualified Control.Monad.Writer.Lazy as WriterLazy import qualified Control.Monad.Writer.Strict as WriterStrict-import Data.Bifunctor+import Data.Bifunctor (Bifunctor (first)) import qualified Data.ByteString as B-import Data.Hashable-import Data.Int-import Data.String+import Data.Hashable (Hashable (hashWithSalt))+import Data.Int (Int16, Int32, Int64, Int8)+import Data.String (IsString (fromString)) import qualified Data.Text as T import Data.Typeable-import Data.Word-import GHC.TypeNats-import Generics.Deriving hiding (index)-import Grisette.Core.Control.Monad.Union-import {-# SOURCE #-} Grisette.Core.Control.Monad.UnionM-import Grisette.Core.Data.BV-import Grisette.Core.Data.Class.Bool+ ( Proxy (Proxy),+ Typeable,+ eqT,+ typeRep,+ type (:~:) (Refl),+ )+import Data.Word (Word16, Word32, Word64, Word8)+import GHC.TypeNats (KnownNat, Nat, type (<=))+import Generics.Deriving+ ( Generic (Rep, from, to),+ K1 (K1),+ M1 (M1),+ U1 (U1),+ type (:*:) ((:*:)),+ type (:+:) (L1, R1),+ )+import {-# SOURCE #-} Grisette.Core.Control.Monad.UnionM (UnionM)+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN) import Grisette.Core.Data.Class.Mergeable+ ( Mergeable (rootStrategy),+ Mergeable1 (liftRootStrategy),+ Mergeable2 (liftRootStrategy2),+ MergingStrategy (SimpleStrategy),+ rootStrategy1,+ wrapStrategy,+ ) import Grisette.Core.Data.Class.SimpleMergeable+ ( SimpleMergeable (mrgIte),+ SimpleMergeable1 (liftMrgIte),+ UnionLike (mergeWithStrategy, mrgIfWithStrategy, single, unionIf),+ merge,+ mrgIf,+ mrgSingle,+ ) import Grisette.Core.Data.Class.Solvable+ ( Solvable (iinfosym, isym),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( LinkedRep,+ SupportedPrim,+ ) import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim-import Grisette.Utils-import Language.Haskell.TH.Syntax hiding (lift)+ ( SomeSymIntN (SomeSymIntN),+ SomeSymWordN (SomeSymWordN),+ SymBool,+ SymIntN,+ SymInteger,+ SymWordN,+ type (-~>),+ type (=~>),+ )+import Grisette.Utils.Parameterized+ ( KnownProof (KnownProof),+ LeqProof (LeqProof),+ unsafeKnownProof,+ unsafeLeqProof,+ )+import Language.Haskell.TH.Syntax (Lift (liftTyped)) -- $setup -- >>> import Grisette.Core@@ -305,17 +359,17 @@ catchError = liftFreshTCache catchError instance (MonadWriter w m) => MonadWriter w (FreshT m) where- writer p = FreshT $ \ident index -> (,index) <$> writer p+ writer p = FreshT $ \_ index -> (,index) <$> writer p listen (FreshT r) = FreshT $ \ident index -> (\((a, b), c) -> ((a, c), b)) <$> listen (r ident index) pass (FreshT r) = FreshT $ \ident index -> pass $ (\((a, b), c) -> ((a, c), b)) <$> r ident index instance (MonadState s m) => MonadState s (FreshT m) where- get = FreshT $ \ident index -> gets (,index)- put s = FreshT $ \ident index -> (,index) <$> put s+ get = FreshT $ \_ index -> gets (,index)+ put s = FreshT $ \_ index -> (,index) <$> put s instance (MonadReader r m) => MonadReader r (FreshT m) where local t (FreshT r) = FreshT $ \ident index -> local t (r ident index)- ask = FreshT $ \ident index -> asks (,index)+ ask = FreshT $ \_ index -> asks (,index) instance (MonadRWS r w s m) => MonadRWS r w s (FreshT m) @@ -344,12 +398,12 @@ getFreshIdent = ReaderT $ const getFreshIdent instance (MonadFresh m, Monoid w) => MonadFresh (RWSLazy.RWST r w s m) where- nextFreshIndex = RWSLazy.RWST $ \r s -> (,s,mempty) <$> nextFreshIndex- getFreshIdent = RWSLazy.RWST $ \r s -> (,s,mempty) <$> getFreshIdent+ nextFreshIndex = RWSLazy.RWST $ \_ s -> (,s,mempty) <$> nextFreshIndex+ getFreshIdent = RWSLazy.RWST $ \_ s -> (,s,mempty) <$> getFreshIdent instance (MonadFresh m, Monoid w) => MonadFresh (RWSStrict.RWST r w s m) where- nextFreshIndex = RWSStrict.RWST $ \r s -> (,s,mempty) <$> nextFreshIndex- getFreshIdent = RWSStrict.RWST $ \r s -> (,s,mempty) <$> getFreshIdent+ nextFreshIndex = RWSStrict.RWST $ \_ s -> (,s,mempty) <$> nextFreshIndex+ getFreshIdent = RWSStrict.RWST $ \_ s -> (,s,mempty) <$> getFreshIdent -- | 'FreshT' specialized with Identity. type Fresh = FreshT Identity@@ -482,7 +536,7 @@ GenSymNoSpec (a :+: b) where freshNoSpec ::- forall m u c.+ forall m c. ( MonadFresh m ) => m (UnionM ((a :+: b) c))@@ -497,7 +551,7 @@ GenSymNoSpec (a :*: b) where freshNoSpec ::- forall m u c.+ forall m c. ( MonadFresh m ) => m (UnionM ((a :*: b) c))@@ -518,7 +572,7 @@ -- -- __Note:__ __Never__ use on recursive types. derivedNoSpecFresh ::- forall bool a m u.+ forall a m. ( Generic a, GenSymNoSpec (Rep a), Mergeable a,@@ -633,7 +687,7 @@ -- >>> runFresh (chooseFresh [1,2,3]) "a" :: UnionM Integer -- {If a@0 1 (If a@1 2 3)} chooseFresh ::- forall bool a m u.+ forall a m. ( Mergeable a, MonadFresh m ) =>@@ -650,7 +704,7 @@ -- A globally unique identifier should be supplied to ensure the uniqueness of -- symbolic constants in the generated symbolic values. choose ::- forall bool a u.+ forall a. ( Mergeable a ) => [a] ->@@ -707,7 +761,7 @@ -- >>> runFresh (chooseUnionFresh [a, b]) "c" :: UnionM Integer -- {If (&& c@0 a@0) 1 (If (|| c@0 b@0) 2 3)} chooseUnionFresh ::- forall bool a m u.+ forall a m. ( Mergeable a, MonadFresh m ) =>@@ -724,7 +778,7 @@ -- A globally unique identifier should be supplied to ensure the uniqueness of -- symbolic constants in the generated symbolic values. chooseUnion ::- forall a u.+ forall a. ( Mergeable a ) => [UnionM a] ->@@ -829,6 +883,7 @@ GenSymSimple (Either aspec bspec) (Either a b) where simpleFresh (Left a) = Left <$> simpleFresh a+ simpleFresh (Right b) = Right <$> simpleFresh b instance (GenSym () a, Mergeable a, GenSym () b, Mergeable b) =>@@ -1631,7 +1686,7 @@ error "Can only generate bit vectors with positive bit size" \ where \ f :: forall p (n :: Nat) m. (MonadFresh m) => p n -> m symtype; \- f p = case (unsafeKnownProof @n (fromIntegral i), unsafeLeqProof @1 @n) of \+ f _ = case (unsafeKnownProof @n (fromIntegral i), unsafeLeqProof @1 @n) of \ (KnownProof, LeqProof) -> do \ v :: origtype n <- simpleFresh (); \ return $ symtype v; \
src/Grisette/Core/Data/Class/Mergeable.hs view
@@ -51,36 +51,90 @@ where import Control.Exception-import Control.Monad.Cont-import Control.Monad.Except+ ( 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, runIdentity),+ IdentityT (IdentityT, runIdentityT),+ ) import qualified Control.Monad.RWS.Lazy as RWSLazy import qualified Control.Monad.RWS.Strict as RWSStrict-import Control.Monad.Reader+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+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-import Data.Functor.Sum-import Data.Int-import Data.Kind+ ( Eq1,+ Ord1,+ Show1,+ compare1,+ eq1,+ showsPrec1,+ )+import Data.Functor.Sum (Sum (InL, InR))+import Data.Int (Int16, Int32, Int64, Int8)+import Data.Kind (Type) import qualified Data.Monoid as Monoid import qualified Data.Text as T import Data.Typeable-import Data.Word-import GHC.Natural-import qualified GHC.TypeLits-import GHC.TypeNats+ ( Proxy (Proxy),+ Typeable,+ eqT,+ type (:~:) (Refl),+ )+import Data.Word (Word16, Word32, Word64, Word8)+import GHC.Natural (Natural)+import GHC.TypeNats (KnownNat, natVal, 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,+ type (:*:) ((:*:)),+ type (:+:) (L1, R1),+ ) import Grisette.Core.Data.BV-import Grisette.Core.Data.Class.Bool+ ( BitwidthMismatch,+ IntN (IntN),+ SomeIntN (SomeIntN),+ SomeWordN (SomeWordN),+ WordN (WordN),+ )+import Grisette.Core.Data.Class.Bool (ITEOp (ites)) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( LinkedRep,+ SupportedPrim,+ ) import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim-import Grisette.Utils-import Unsafe.Coerce+ ( SomeSymIntN (SomeSymIntN),+ SomeSymWordN (SomeSymWordN),+ SymBool,+ SymIntN,+ SymInteger,+ SymWordN,+ type (-~>),+ type (=~>),+ )+import Grisette.Utils.Parameterized (unsafeAxiom)+import Unsafe.Coerce (unsafeCoerce) -- | Helper type for combining arbitrary number of indices into one. -- Useful when trying to write efficient merge strategy for lists/vectors.@@ -467,20 +521,20 @@ instance Mergeable SomeIntN where rootStrategy = SortedStrategy @Natural- (\(SomeIntN (v :: IntN n)) -> natVal (Proxy @n))- ( \n ->+ (\(SomeIntN (_ :: IntN n)) -> natVal (Proxy @n))+ ( \_ -> SortedStrategy @Integer- (\(SomeIntN (IntN i)) -> toInteger i)+ (\(SomeIntN (IntN i)) -> i) (const $ SimpleStrategy $ \_ l _ -> l) ) instance Mergeable SomeWordN where rootStrategy = SortedStrategy @Natural- (\(SomeWordN (v :: WordN n)) -> natVal (Proxy @n))- ( \n ->+ (\(SomeWordN (_ :: WordN n)) -> natVal (Proxy @n))+ ( \_ -> SortedStrategy @Integer- (\(SomeWordN (WordN i)) -> toInteger i)+ (\(SomeWordN (WordN i)) -> i) (const $ SimpleStrategy $ \_ l _ -> l) ) @@ -513,14 +567,14 @@ -- | Helper type for building efficient merge strategy for list-like containers. data StrategyList container where StrategyList ::- forall bool a container.+ forall a container. container [DynamicSortedIdx] -> container (MergingStrategy a) -> StrategyList container -- | Helper function for building efficient merge strategy for list-like containers. buildStrategyList ::- forall bool a container.+ forall a container. (Functor container) => MergingStrategy a -> container a ->@@ -994,8 +1048,8 @@ instance Mergeable SomeSymIntN where rootStrategy = SortedStrategy @Natural- (\(SomeSymIntN (v :: SymIntN n)) -> natVal (Proxy @n))- ( \n ->+ (\(SomeSymIntN (_ :: SymIntN n)) -> natVal (Proxy @n))+ ( \_ -> SimpleStrategy ( \c (SomeSymIntN (l :: SymIntN l)) (SomeSymIntN (r :: SymIntN r)) -> case unsafeAxiom @l @r of@@ -1006,8 +1060,8 @@ instance Mergeable SomeSymWordN where rootStrategy = SortedStrategy @Natural- (\(SomeSymWordN (v :: SymWordN n)) -> natVal (Proxy @n))- ( \n ->+ (\(SomeSymWordN (_ :: SymWordN n)) -> natVal (Proxy @n))+ ( \_ -> SimpleStrategy ( \c (SomeSymWordN (l :: SymWordN l)) (SomeSymWordN (r :: SymWordN r)) -> case unsafeAxiom @l @r of@@ -1027,6 +1081,6 @@ Denormal -> 4 :: Int RatioZeroDenominator -> 5 :: Int )- (const $ SimpleStrategy $ \_ l r -> l)+ (const $ SimpleStrategy $ \_ l _ -> l) deriving via (Default BitwidthMismatch) instance (Mergeable BitwidthMismatch)
src/Grisette/Core/Data/Class/Mergeable.hs-boot view
@@ -2,10 +2,15 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE Trustworthy #-} -module Grisette.Core.Data.Class.Mergeable where+module Grisette.Core.Data.Class.Mergeable+ ( MergingStrategy (..),+ Mergeable' (..),+ Mergeable (..),+ )+where -import Data.Typeable-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim+import Data.Typeable (Typeable)+import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool) data MergingStrategy a where SimpleStrategy :: (SymBool -> a -> a -> a) -> MergingStrategy a
src/Grisette/Core/Data/Class/ModelOps.hs view
@@ -21,9 +21,7 @@ ) where -import Data.Hashable-import Data.Kind-import Data.Typeable+import Data.Kind (Type) -- $setup -- >>> import Grisette.Core@@ -88,7 +86,7 @@ -- SymbolSet {a :: Bool, b :: Bool} class (SymbolSetOps symbolSet typedSymbol) =>- SymbolSetRep rep symbolSet (typedSymbol :: * -> *)+ SymbolSetRep rep symbolSet (typedSymbol :: Type -> Type) where -- | Build a symbolic constant set buildSymbolSet :: rep -> symbolSet
src/Grisette/Core/Data/Class/SOrd.hs view
@@ -26,24 +26,43 @@ ) where -import Control.Monad.Except+import Control.Monad.Except (ExceptT (ExceptT)) import Control.Monad.Identity-import Control.Monad.Trans.Maybe+ ( 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.Sum-import Data.Int+import Data.Functor.Sum (Sum)+import Data.Int (Int16, Int32, Int64, Int8) import qualified Data.Text as T-import Data.Word-import GHC.TypeLits+import Data.Word (Word16, Word32, Word64, Word8)+import GHC.TypeLits (KnownNat, type (<=)) import Generics.Deriving-import {-# SOURCE #-} Grisette.Core.Control.Monad.UnionM-import Grisette.Core.Data.BV+ ( Default (Default),+ Generic (Rep, from),+ K1 (K1),+ M1 (M1),+ U1,+ V1,+ type (:*:) ((:*:)),+ type (:+:) (L1, R1),+ )+import {-# SOURCE #-} Grisette.Core.Control.Monad.UnionM (UnionM)+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN) import Grisette.Core.Data.Class.Bool+ ( LogicalOp ((&&~), (||~)),+ SEq ((/=~), (==~)),+ SEq' ((==~~)),+ ) import Grisette.Core.Data.Class.SimpleMergeable-import Grisette.Core.Data.Class.Solvable-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim+ ( mrgIf,+ mrgSingle,+ )+import Grisette.Core.Data.Class.Solvable (Solvable (con))+import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool) -- $setup -- >>> import Grisette.Core
src/Grisette/Core/Data/Class/SafeArith.hs view
@@ -30,24 +30,39 @@ ) where -import Control.Exception-import Control.Monad.Except-import Data.Int-import Data.Typeable-import Data.Word-import GHC.TypeNats-import Grisette.Core.Control.Monad.Union+import Control.Exception (ArithException (DivideByZero, Overflow, Underflow))+import Control.Monad.Except (MonadError (throwError))+import Data.Int (Int16, Int32, Int64, Int8)+import Data.Typeable (Proxy (Proxy), type (:~:) (Refl))+import Data.Word (Word16, Word32, Word64, Word8)+import GHC.TypeNats (KnownNat, sameNat, type (<=))+import Grisette.Core.Control.Monad.Union (MonadUnion) import Grisette.Core.Data.BV+ ( BitwidthMismatch (BitwidthMismatch),+ IntN,+ SomeIntN (SomeIntN),+ SomeWordN (SomeWordN),+ WordN,+ ) import Grisette.Core.Data.Class.Bool-import Grisette.Core.Data.Class.Error-import Grisette.Core.Data.Class.Mergeable+ ( LogicalOp ((&&~), (||~)),+ SEq ((==~)),+ )+import Grisette.Core.Data.Class.Mergeable (Mergeable) import Grisette.Core.Data.Class.SOrd+ ( SOrd ((<=~), (<~), (>=~), (>~)),+ ) import Grisette.Core.Data.Class.SimpleMergeable-import Grisette.Core.Data.Class.Solvable+ ( merge,+ mrgIf,+ mrgSingle,+ )+import Grisette.Core.Data.Class.Solvable (Solvable (con)) -- $setup -- >>> import Grisette.Core -- >>> import Grisette.IR.SymPrim+-- >>> import Control.Monad.Except -- | Safe division with monadic error handling in multi-path -- execution. These procedures throw an exception when the@@ -94,7 +109,7 @@ -- | Safe signed 'rem' with monadic error handling in multi-path execution. safeRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a safeRem l r = do- (d, m) <- safeDivMod l r+ (_, m) <- safeDivMod l r mrgIf ((l >=~ 0 &&~ r >~ 0) ||~ (l <=~ 0 &&~ r <~ 0) ||~ m ==~ 0) (mrgSingle m)@@ -154,7 +169,7 @@ -- The error is transformed. safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a safeRem' t l r = do- (d, m) <- safeDivMod' t l r+ (_, m) <- safeDivMod' t l r mrgIf ((l >=~ 0 &&~ r >~ 0) ||~ (l <=~ 0 &&~ r <~ 0) ||~ m ==~ 0) (mrgSingle m)@@ -177,12 +192,13 @@ #define QRIGHT(a) QID(a)' #define QRIGHTT(a) QID(a)' t'+#define QRIGHTU(a) QID(a)' _' #define SAFE_DIVISION_FUNC(name, op) \ name _ r | r == 0 = merge $ throwError DivideByZero; \ name l r = mrgSingle $ l `op` r; \-QRIGHTT(name) _ r | r == 0 = let t1 = t' in merge $ throwError (t' DivideByZero); \-QRIGHTT(name) l r = mrgSingle $ l `op` r+QRIGHTT(name) _ r | r == 0 = let _ = t' in merge $ throwError (t' DivideByZero); \+QRIGHTU(name) l r = mrgSingle $ l `op` r #define SAFE_DIVISION_CONCRETE(type) \ instance SafeDivision ArithException type where \@@ -395,7 +411,7 @@ safeAdd' t (type (l :: ctype l)) (type (r :: ctype r)) = merge (\ case sameNat (Proxy @l) (Proxy @r) of \ Just Refl -> type <$> safeAdd' (t . Right) l r; \- _ -> let t' = t; t''' = t in throwError $ t' $ Left BitwidthMismatch); \+ _ -> let t' = t; _ = t' in throwError $ t' $ Left BitwidthMismatch); \ safeMinus (type (l :: ctype l)) (type (r :: ctype r)) = merge (\ case sameNat (Proxy @l) (Proxy @r) of \ Just Refl -> type <$> safeMinus' Right l r; \@@ -403,7 +419,7 @@ safeMinus' t (type (l :: ctype l)) (type (r :: ctype r)) = merge (\ case sameNat (Proxy @l) (Proxy @r) of \ Just Refl -> type <$> safeMinus' (t . Right) l r; \- _ -> let t' = t; t''' = t in throwError $ t' $ Left BitwidthMismatch); \+ _ -> let t' = t; _ = t' in throwError $ t' $ Left BitwidthMismatch); \ safeNeg (type l) = merge $ type <$> safeNeg' Right l; \ safeNeg' t (type l) = merge $ type <$> safeNeg' (t . Right) l
src/Grisette/Core/Data/Class/SimpleMergeable.hs view
@@ -46,26 +46,53 @@ ) where -import Control.Monad.Except+import Control.Monad.Except (ExceptT (ExceptT)) import Control.Monad.Identity+ ( Identity (Identity),+ IdentityT (IdentityT),+ ) import qualified Control.Monad.RWS.Lazy as RWSLazy import qualified Control.Monad.RWS.Strict as RWSStrict-import Control.Monad.Reader+import Control.Monad.Reader (ReaderT (ReaderT)) import qualified Control.Monad.State.Lazy as StateLazy import qualified Control.Monad.State.Strict as StateStrict-import Control.Monad.Trans.Cont-import Control.Monad.Trans.Maybe+import Control.Monad.Trans.Cont (ContT (ContT))+import Control.Monad.Trans.Maybe (MaybeT (MaybeT)) import qualified Control.Monad.Writer.Lazy as WriterLazy import qualified Control.Monad.Writer.Strict as WriterStrict-import Data.Kind+import Data.Kind (Type) import GHC.Generics-import GHC.TypeNats-import Generics.Deriving-import Grisette.Core.Data.Class.Bool-import Grisette.Core.Data.Class.Function+ ( Generic (Rep, from, to),+ K1 (K1),+ M1 (M1),+ U1,+ V1,+ type (:*:) ((:*:)),+ )+import GHC.TypeNats (KnownNat, type (<=))+import Generics.Deriving (Default (Default))+import Grisette.Core.Data.Class.Bool (ITEOp (ites))+import Grisette.Core.Data.Class.Function (Function (Arg, Ret, (#))) import Grisette.Core.Data.Class.Mergeable+ ( Mergeable (rootStrategy),+ Mergeable',+ Mergeable1 (liftRootStrategy),+ Mergeable2 (liftRootStrategy2),+ Mergeable3 (liftRootStrategy3),+ MergingStrategy (SimpleStrategy),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( LinkedRep,+ SupportedPrim,+ ) import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim+ ( SymBool,+ SymIntN,+ SymInteger,+ SymWordN,+ type (-~>),+ type (=~>),+ ) -- $setup -- >>> import Grisette.Core@@ -718,7 +745,7 @@ -- <If a b c> -- >>> simpleMerge $ (unionIf (ssym "a") (return $ ssym "b") (return $ ssym "c") :: UnionM SymBool) -- (ite a b c)-simpleMerge :: forall bool u a. (SimpleMergeable a, UnionLike u, UnionPrjOp u) => u a -> a+simpleMerge :: forall u a. (SimpleMergeable a, UnionLike u, UnionPrjOp u) => u a -> a simpleMerge u = case merge u of SingleU x -> x _ -> error "Should not happen"@@ -730,7 +757,7 @@ -- >>> sumU (unionIf "cond" (return ["a"]) (return ["b","c"]) :: UnionM [SymInteger]) -- (ite cond a (+ b c)) onUnion ::- forall bool u a r.+ forall u a r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> r) -> (u a -> r)@@ -738,7 +765,7 @@ -- | Lift a function to work on union values. onUnion2 ::- forall bool u a b r.+ forall u a b r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> r) -> (u a -> u b -> r)@@ -746,7 +773,7 @@ -- | Lift a function to work on union values. onUnion3 ::- forall bool u a b c r.+ forall u a b c r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> r) -> (u a -> u b -> u c -> r)@@ -754,7 +781,7 @@ -- | Lift a function to work on union values. onUnion4 ::- forall bool u a b c d r.+ forall u a b c d r. (SimpleMergeable r, UnionLike u, UnionPrjOp u, Monad u) => (a -> b -> c -> d -> r) -> (u a -> u b -> u c -> u d -> r)
src/Grisette/Core/Data/Class/SimpleMergeable.hs-boot view
@@ -4,7 +4,9 @@ module Grisette.Core.Data.Class.SimpleMergeable (SimpleMergeable (..)) where import {-# SOURCE #-} Grisette.Core.Data.Class.Mergeable-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim+ ( Mergeable,+ )+import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool) class (Mergeable a) => SimpleMergeable a where mrgIte :: SymBool -> a -> a -> a
src/Grisette/Core/Data/Class/Solvable.hs view
@@ -18,11 +18,11 @@ ) where -import Control.DeepSeq-import Data.Hashable-import Data.String-import Data.Typeable-import Language.Haskell.TH.Syntax+import Control.DeepSeq (NFData)+import Data.Hashable (Hashable)+import Data.String (IsString)+import Data.Typeable (Typeable)+import Language.Haskell.TH.Syntax (Lift) -- $setup -- >>> import Grisette.Core
src/Grisette/Core/Data/Class/Solver.hs view
@@ -39,21 +39,20 @@ ) where -import Control.DeepSeq-import Control.Monad.Except-import Data.Hashable-import Generics.Deriving-import Grisette.Core.Control.Exception-import Grisette.Core.Data.Class.Bool-import Grisette.Core.Data.Class.Evaluate-import Grisette.Core.Data.Class.ExtractSymbolics+import Control.DeepSeq (NFData)+import Control.Monad.Except (ExceptT, runExceptT)+import Data.Hashable (Hashable)+import GHC.Generics (Generic) import Grisette.Core.Data.Class.SimpleMergeable-import Grisette.Core.Data.Class.Solvable-import Grisette.IR.SymPrim.Data.Prim.Model-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim-import Language.Haskell.TH.Syntax+ ( UnionPrjOp,+ simpleMerge,+ )+import Grisette.IR.SymPrim.Data.Prim.Model (Model)+import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool)+import Language.Haskell.TH.Syntax (Lift) -data SolveInternal = SolveInternal deriving (Eq, Show, Ord, Generic, Hashable, Lift, NFData)+data SolveInternal = SolveInternal+ deriving (Eq, Show, Ord, Generic, Hashable, Lift, NFData) -- $setup -- >>> import Grisette.Core
src/Grisette/Core/Data/Class/Substitute.hs view
@@ -25,24 +25,35 @@ ) where -import Control.Monad.Except+import Control.Monad.Except (ExceptT (ExceptT)) import Control.Monad.Identity-import Control.Monad.Trans.Maybe+ ( 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.Sum-import Data.Int+import Data.Functor.Sum (Sum)+import Data.Int (Int16, Int32, Int64, Int8) import qualified Data.Text as T-import Data.Word-import GHC.TypeNats+import Data.Word (Word16, Word32, Word64, Word8)+import GHC.TypeNats (KnownNat, type (<=)) import Generics.Deriving+ ( Default (Default, unDefault),+ Generic (Rep, from, to),+ K1 (K1),+ M1 (M1),+ U1,+ type (:*:) ((:*:)),+ type (:+:) (L1, R1),+ ) import Generics.Deriving.Instances ()-import Grisette.Core.Data.BV+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim+ ( LinkedRep,+ TypedSymbol,+ ) -- $setup -- >>> import Grisette.Core
src/Grisette/Core/Data/Class/ToCon.hs view
@@ -24,21 +24,31 @@ ) where -import Control.Monad.Except+import Control.Monad.Except (ExceptT (ExceptT)) import Control.Monad.Identity-import Control.Monad.Trans.Maybe+ ( Identity (Identity, runIdentity),+ 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.Sum-import Data.Int+import Data.Functor.Sum (Sum)+import Data.Int (Int16, Int32, Int64, Int8) import qualified Data.Text as T-import Data.Word+import Data.Word (Word16, Word32, Word64, Word8) import GHC.Generics-import GHC.TypeNats-import Generics.Deriving+ ( Generic (Rep, from, to),+ K1 (K1),+ M1 (M1),+ U1,+ type (:*:) ((:*:)),+ type (:+:) (L1, R1),+ )+import GHC.TypeNats (KnownNat, type (<=))+import Generics.Deriving (Default (Default)) import Generics.Deriving.Instances ()-import Grisette.Core.Data.BV+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN) -- $setup -- >>> import Grisette.Core
src/Grisette/Core/Data/Class/ToSym.hs view
@@ -25,21 +25,32 @@ where import Control.Monad.Identity-import Control.Monad.Reader+ ( Identity (Identity),+ IdentityT (IdentityT),+ )+import Control.Monad.Reader (ReaderT (ReaderT)) import qualified Control.Monad.State.Lazy as StateLazy import qualified Control.Monad.State.Strict as StateStrict-import Control.Monad.Trans.Except-import Control.Monad.Trans.Maybe+import Control.Monad.Trans.Except (ExceptT (ExceptT))+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.Sum-import Data.Int+import Data.Functor.Sum (Sum)+import Data.Int (Int16, Int32, Int64, Int8) import qualified Data.Text as T-import Data.Word-import GHC.TypeNats+import Data.Word (Word16, Word32, Word64, Word8)+import GHC.TypeNats (KnownNat, type (<=)) import Generics.Deriving-import Grisette.Core.Data.BV+ ( Default (Default),+ Generic (Rep, from, to),+ K1 (K1),+ M1 (M1),+ U1,+ type (:*:) ((:*:)),+ type (:+:) (L1, R1),+ )+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN) -- $setup -- >>> import Grisette.IR.SymPrim
src/Grisette/Core/Data/FileLocation.hs view
@@ -4,6 +4,8 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE Trustworthy #-} +{- HLINT ignore "Unused LANGUAGE pragma" -}+ -- | -- Module : Grisette.Core.Data.FileLocation -- Copyright : (c) Sirui Lu 2021-2023@@ -21,14 +23,16 @@ ) where -import Control.DeepSeq-import Data.Hashable+import Control.DeepSeq (NFData)+import Data.Hashable (Hashable) import Debug.Trace.LocationTH (__LOCATION__)-import GHC.Generics-import Grisette.Core.Data.Class.GenSym+import GHC.Generics (Generic)+import Grisette.Core.Data.Class.GenSym (FreshIdent, nameWithInfo) import Grisette.Core.Data.Class.Solvable-import Language.Haskell.TH.Syntax-import Language.Haskell.TH.Syntax.Compat+ ( Solvable (iinfosym, sinfosym),+ )+import Language.Haskell.TH.Syntax (Lift, unsafeTExpCoerce)+import Language.Haskell.TH.Syntax.Compat (SpliceQ, liftSplice) -- $setup -- >>> import Grisette.Core
src/Grisette/Core/Data/MemoUtils.hs view
@@ -22,9 +22,9 @@ where import Data.Function (fix)-import Data.HashTable.IO as H-import Data.Hashable-import System.IO.Unsafe+import qualified Data.HashTable.IO as H+import Data.Hashable (Hashable)+import System.IO.Unsafe (unsafePerformIO) type HashTable k v = H.BasicHashTable k v
src/Grisette/Core/Data/Union.hs view
@@ -4,6 +4,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeFamilies #-} @@ -26,22 +27,47 @@ ) where -import Control.DeepSeq+import Control.DeepSeq (NFData (rnf), NFData1 (liftRnf), rnf1) import Data.Functor.Classes-import Data.Hashable-import GHC.Generics+ ( Eq1 (liftEq),+ Show1 (liftShowsPrec),+ showsPrec1,+ showsUnaryWith,+ )+import Data.Hashable (Hashable (hashWithSalt))+import GHC.Generics (Generic, Generic1) import Grisette.Core.Data.Class.Bool+ ( ITEOp (ites),+ LogicalOp (nots, (&&~), (||~)),+ ) import Grisette.Core.Data.Class.GPretty+ ( GPretty (gprettyPrec),+ condEnclose,+ ) import Grisette.Core.Data.Class.Mergeable+ ( Mergeable (rootStrategy),+ Mergeable1 (liftRootStrategy),+ MergingStrategy (NoStrategy, SimpleStrategy, SortedStrategy),+ ) import Grisette.Core.Data.Class.SimpleMergeable-import Grisette.Core.Data.Class.Solvable+ ( SimpleMergeable (mrgIte),+ SimpleMergeable1 (liftMrgIte),+ UnionLike (mergeWithStrategy, mrgIfWithStrategy, mrgSingleWithStrategy, single, unionIf),+ UnionPrjOp (ifView, leftMost, singleView),+ mrgIf,+ )+import Grisette.Core.Data.Class.Solvable (pattern Con) import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim-import Language.Haskell.TH.Syntax+ ( AllSyms (allSymsS),+ SomeSym (SomeSym),+ SymBool,+ )+import Language.Haskell.TH.Syntax (Lift) #if MIN_VERSION_prettyprinter(1,7,0)-import Prettyprinter+import Prettyprinter (align, group, nest, vsep) #else-import Data.Text.Prettyprint.Doc+import Data.Text.Prettyprint.Doc (align, group, nest, vsep) #endif -- | The default union implementation.
src/Grisette/Core/TH.hs view
@@ -17,10 +17,25 @@ ) where -import Control.Monad-import Grisette.Core.THCompat+import Control.Monad (join, replicateM, when, zipWithM)+import Grisette.Core.THCompat (augmentFinalType) import Language.Haskell.TH-import Language.Haskell.TH.Syntax+ ( Body (NormalB),+ Clause (Clause),+ Con (ForallC, GadtC, InfixC, NormalC, RecC, RecGadtC),+ Dec (DataD, FunD, NewtypeD, SigD),+ Exp (AppE, ConE, LamE, VarE),+ Info (DataConI, TyConI),+ Name,+ Pat (VarP),+ Q,+ Type (ForallT),+ mkName,+ newName,+ pprint,+ reify,+ )+import Language.Haskell.TH.Syntax (Name (Name), OccName (OccName)) -- | Generate constructor wrappers that wraps the result in a union-like monad with provided names. --
src/Grisette/Core/THCompat.hs view
@@ -1,7 +1,6 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE TemplateHaskellQuotes #-} {-# LANGUAGE Trustworthy #-}-{- ORMOLU_DISABLE -} -- | -- Module : Grisette.Core.THCompat@@ -11,20 +10,38 @@ -- Maintainer : siruilu@cs.washington.edu -- Stability : Experimental -- Portability : GHC only- module Grisette.Core.THCompat (augmentFinalType) where -import Data.Bifunctor+import Data.Bifunctor (Bifunctor (second))+import Grisette.Core.Control.Monad.UnionM (UnionM)+import Grisette.Core.Data.Class.Mergeable (Mergeable)+#if MIN_VERSION_template_haskell(2,17,0) import Language.Haskell.TH.Syntax-import Grisette.Core.Control.Monad.Union-import Grisette.Core.Data.Class.Bool-import Grisette.Core.Data.Class.Mergeable-import Grisette.Core.Control.Monad.UnionM-import Grisette.IR.SymPrim.Data.SymPrim+ ( Pred,+ Q,+ Specificity,+ TyVarBndr,+ Type+ ( AppT,+ ArrowT,+ MulArrowT+ ),+ )+#else+import Language.Haskell.TH.Syntax+ ( Pred,+ Q,+ TyVarBndr,+ Type+ ( AppT,+ ArrowT+ ),+ )+#endif #if MIN_VERSION_template_haskell(2,17,0) augmentFinalType :: Type -> Q (([TyVarBndr Specificity], [Pred]), Type)-#elif MIN_VERSION_template_haskell(2,16,0)+#else augmentFinalType :: Type -> Q (([TyVarBndr], [Pred]), Type) #endif augmentFinalType (AppT a@(AppT ArrowT _) t) = do
src/Grisette/Experimental.hs view
@@ -1,3 +1,6 @@+-- Disable this warning because we are re-exporting things.+{-# OPTIONS_GHC -Wno-missing-import-lists #-}+ module Grisette.Experimental ( -- * Experimental features @@ -23,3 +26,14 @@ where import Grisette.Experimental.GenSymConstrained+ ( GenSymConstrained (..),+ GenSymSimpleConstrained (..),+ SOrdBound (..),+ SOrdLowerBound (..),+ SOrdUpperBound (..),+ derivedFreshConstrainedNoSpec,+ derivedSimpleFreshConstrainedNoSpec,+ derivedSimpleFreshConstrainedSameShape,+ genSymConstrained,+ genSymSimpleConstrained,+ )
src/Grisette/Experimental/GenSymConstrained.hs view
@@ -28,20 +28,40 @@ ) where -import Control.Monad.Except-import Control.Monad.Trans.Maybe-import Data.Int-import Data.Word-import Debug.Trace+import Control.Monad.Except (ExceptT (ExceptT), MonadError (throwError))+import Control.Monad.Trans.Maybe (MaybeT (MaybeT)) import GHC.Generics-import GHC.TypeLits+ ( Generic (Rep, from, to),+ K1 (K1),+ M1 (M1),+ U1 (U1),+ type (:*:) ((:*:)),+ type (:+:) (L1, R1),+ ) import Grisette.Core.Control.Monad.UnionM-import Grisette.Core.Data.BV-import Grisette.Core.Data.Class.Bool+ ( UnionM,+ liftToMonadUnion,+ )+import Grisette.Core.Data.Class.Bool (LogicalOp ((||~))) import Grisette.Core.Data.Class.GenSym-import Grisette.Core.Data.Class.Mergeable-import Grisette.Core.Data.Class.SOrd+ ( FreshIdent,+ GenSym (fresh),+ GenSymSimple (simpleFresh),+ ListSpec (ListSpec),+ MonadFresh,+ SimpleListSpec (SimpleListSpec),+ chooseFresh,+ chooseUnionFresh,+ runFreshT,+ )+import Grisette.Core.Data.Class.Mergeable (Mergeable, Mergeable1)+import Grisette.Core.Data.Class.SOrd (SOrd ((<~), (>=~))) import Grisette.Core.Data.Class.SimpleMergeable+ ( UnionLike,+ merge,+ mrgIf,+ mrgSingle,+ ) -- $setup -- >>> import Grisette.Core@@ -160,7 +180,7 @@ mrgSingle s instance GenSymConstrained (SOrdBound Integer ()) Integer where- freshConstrained e (SOrdBound l r _) = chooseFresh [l .. r - 1]+ freshConstrained _ (SOrdBound l r _) = chooseFresh [l .. r - 1] -- Either instance@@ -676,7 +696,7 @@ ) => GenSymConstrained spec (ExceptT a m b) where- freshConstrained e v = trace "x" $ do+ freshConstrained e v = do x <- freshConstrained e v mrgSingle $ merge . fmap ExceptT $ x @@ -740,7 +760,7 @@ GenSymConstrainedNoSpec (a :+: b) where freshConstrainedNoSpec ::- forall m u c e.+ forall m c e. ( MonadFresh m, MonadError e m, UnionLike m@@ -758,7 +778,7 @@ GenSymConstrainedNoSpec (a :*: b) where freshConstrainedNoSpec ::- forall m u c e.+ forall m c e. ( MonadFresh m, MonadError e m, UnionLike m@@ -782,7 +802,7 @@ -- -- __Note:__ __Never__ use on recursive types. derivedFreshConstrainedNoSpec ::- forall bool a m u e.+ forall a m e. ( Generic a, GenSymConstrainedNoSpec (Rep a), Mergeable a,
src/Grisette/IR/SymPrim.hs view
@@ -1,4 +1,6 @@ {-# LANGUAGE ExplicitNamespaces #-}+-- Disable this warning because we are re-exporting things.+{-# OPTIONS_GHC -Wno-missing-import-lists #-} -- | -- Module : Grisette.IR.SymPrim@@ -22,8 +24,8 @@ -- ** Symbolic types SupportedPrim,- SymRep (..),- ConRep (..),+ SymRep (SymType),+ ConRep (ConType), LinkedRep, SymBool (..), SymInteger (..),@@ -48,7 +50,38 @@ where import Grisette.Core.Data.BV+ ( IntN,+ SomeIntN (..),+ SomeWordN (..),+ WordN,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( ConRep (..),+ LinkedRep,+ SupportedPrim,+ SymRep (..),+ TypedSymbol (..),+ type (-->),+ ) import Grisette.IR.SymPrim.Data.Prim.Model+ ( Model (..),+ ModelValuePair (..),+ SymbolSet (..),+ ) import Grisette.IR.SymPrim.Data.SymPrim-import Grisette.IR.SymPrim.Data.TabularFun+ ( AllSyms (..),+ ModelSymPair (..),+ SomeSymIntN (..),+ SomeSymWordN (..),+ SymBool (..),+ SymIntN (..),+ SymInteger (..),+ SymWordN (..),+ allSymsSize,+ symSize,+ symsSize,+ (-->),+ type (-~>) (..),+ type (=~>) (..),+ )+import Grisette.IR.SymPrim.Data.TabularFun (type (=->) (..))
src/Grisette/IR/SymPrim/Data/IntBitwidth.hs view
@@ -6,10 +6,10 @@ -- Maintainer : siruilu@cs.washington.edu -- Stability : Experimental -- Portability : GHC only-module Grisette.IR.SymPrim.Data.IntBitwidth where+module Grisette.IR.SymPrim.Data.IntBitwidth (intBitwidthQ) where import Data.Bits (FiniteBits (finiteBitSize))-import Language.Haskell.TH+import Language.Haskell.TH (TyLit (NumTyLit), Type (LitT), TypeQ) intBitwidthQ :: TypeQ intBitwidthQ = return $ LitT (NumTyLit $ toInteger $ finiteBitSize (undefined :: Int))
src/Grisette/IR/SymPrim/Data/Prim/Helpers.hs view
@@ -24,10 +24,14 @@ ) where -import Data.Typeable+import Data.Typeable (Typeable, cast) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( Term (BinaryTerm, TernaryTerm, UnaryTerm),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils-import Unsafe.Coerce+ ( castTerm,+ )+import Unsafe.Coerce (unsafeCoerce) unsafeUnaryTermView :: forall a b tag. (Typeable tag) => Term a -> Maybe (tag, Term b) unsafeUnaryTermView (UnaryTerm _ (tag :: tagt) t1) =
src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Caches.hs view
@@ -16,13 +16,20 @@ module Grisette.IR.SymPrim.Data.Prim.InternedTerm.Caches (typeMemoizedCache) where import Control.Concurrent-import Data.Data+ ( forkIO,+ newEmptyMVar,+ putMVar,+ readMVar,+ takeMVar,+ tryPutMVar,+ )+import Data.Data (Proxy (Proxy), TypeRep, Typeable, typeRep) import qualified Data.HashMap.Strict as M-import Data.IORef-import Data.Interned+import Data.IORef (IORef, atomicModifyIORef', newIORef)+import Data.Interned (Cache, Interned, mkCache) import GHC.Base (Any)-import GHC.IO-import Unsafe.Coerce+import GHC.IO (unsafeDupablePerformIO, unsafePerformIO)+import Unsafe.Coerce (unsafeCoerce) mkOnceIO :: IO a -> IO (IO a) mkOnceIO io = do
src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs view
@@ -65,21 +65,79 @@ ) where -import Control.DeepSeq-import Data.Array-import Data.Bits+import Control.DeepSeq (NFData)+import Data.Array ((!))+import Data.Bits (Bits) import qualified Data.HashMap.Strict as M-import Data.Hashable+import Data.Hashable (Hashable (hash)) import Data.IORef (atomicModifyIORef') import Data.Interned+ ( Interned (Uninterned, cache, cacheWidth, describe, identify),+ ) import Data.Interned.Internal+ ( Cache (getCache),+ CacheState (CacheState),+ ) import GHC.IO (unsafeDupablePerformIO)-import GHC.TypeNats+import GHC.TypeNats (KnownNat, type (+), type (<=)) import Grisette.Core.Data.Class.BitVector+ ( BVSignConversion,+ SizedBV,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.TabularFun-import Language.Haskell.TH.Syntax-import Type.Reflection+ ( BinaryOp,+ SupportedPrim,+ Term,+ TernaryOp,+ TypedSymbol (IndexedSymbol, SimpleSymbol, WithInfo),+ UTerm+ ( UAbsNumTerm,+ UAddNumTerm,+ UAndBitsTerm,+ UAndTerm,+ UBVConcatTerm,+ UBVExtendTerm,+ UBVSelectTerm,+ UBVToSignedTerm,+ UBVToUnsignedTerm,+ UBinaryTerm,+ UComplementBitsTerm,+ UConTerm,+ UDivBoundedIntegralTerm,+ UDivIntegralTerm,+ UEqvTerm,+ UGeneralFunApplyTerm,+ UITETerm,+ ULENumTerm,+ ULTNumTerm,+ UModBoundedIntegralTerm,+ UModIntegralTerm,+ UNotTerm,+ UOrBitsTerm,+ UOrTerm,+ UQuotBoundedIntegralTerm,+ UQuotIntegralTerm,+ URemBoundedIntegralTerm,+ URemIntegralTerm,+ URotateBitsTerm,+ UShiftBitsTerm,+ USignumNumTerm,+ USymTerm,+ UTabularFunApplyTerm,+ UTernaryTerm,+ UTimesNumTerm,+ UUMinusNumTerm,+ UUnaryTerm,+ UXorBitsTerm+ ),+ UnaryOp,+ type (-->),+ )+import Grisette.IR.SymPrim.Data.TabularFun+ ( type (=->),+ )+import Language.Haskell.TH.Syntax (Lift)+import Type.Reflection (Typeable, typeRep) internTerm :: forall t. (SupportedPrim t) => Uninterned (Term t) -> Term t internTerm !bt = unsafeDupablePerformIO $ atomicModifyIORef' slot go
src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs-boot view
@@ -54,15 +54,28 @@ ) where -import Control.DeepSeq-import Data.Bits-import Data.Hashable-import Data.Typeable-import GHC.TypeNats+import Control.DeepSeq (NFData)+import Data.Bits (Bits)+import Data.Hashable (Hashable)+import Data.Typeable (Typeable)+import GHC.TypeNats (KnownNat, type (+), type (<=)) import Grisette.Core.Data.Class.BitVector+ ( BVSignConversion,+ SizedBV,+ ) import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( BinaryOp,+ SupportedPrim,+ Term,+ TernaryOp,+ TypedSymbol,+ UnaryOp,+ type (-->),+ ) import {-# SOURCE #-} Grisette.IR.SymPrim.Data.TabularFun-import Language.Haskell.TH.Syntax+ ( type (=->),+ )+import Language.Haskell.TH.Syntax (Lift) constructUnary :: forall tag arg t.
src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/SomeTerm.hs view
@@ -13,10 +13,15 @@ -- Portability : GHC only module Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm (SomeTerm (..)) where -import Data.Hashable-import Data.Typeable+import Data.Hashable (Hashable (hashWithSalt))+import Data.Typeable (Proxy (Proxy), typeRep) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( SupportedPrim,+ Term,+ ) import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils+ ( identityWithTypeRep,+ ) data SomeTerm where SomeTerm :: forall a. (SupportedPrim a) => Term a -> SomeTerm
src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs view
@@ -51,34 +51,115 @@ ) where -import Control.DeepSeq-import Data.Bits+import Control.DeepSeq (NFData (rnf))+import Data.Bits (Bits) import Data.Function (on)-import Data.Hashable+import Data.Hashable (Hashable (hashWithSalt)) import Data.Interned-import Data.Kind-import Data.String-import Data.Typeable (Proxy (..), cast)-import GHC.Generics-import GHC.TypeNats-import Grisette.Core.Data.BV+ ( Cache,+ Id,+ Interned (Description, Uninterned, cache, describe, identify),+ )+import Data.Kind (Constraint)+import Data.String (IsString (fromString))+import Data.Typeable (Proxy (Proxy), cast)+import GHC.Generics (Generic)+import GHC.TypeNats (KnownNat, Nat, type (+), type (<=))+import Grisette.Core.Data.BV (IntN, WordN) import Grisette.Core.Data.Class.BitVector-import Grisette.Core.Data.Class.Function+ ( BVSignConversion,+ SizedBV,+ )+import Grisette.Core.Data.Class.Function (Function (Arg, Ret, (#))) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Caches+ ( typeMemoizedCache,+ ) import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( absNumTerm,+ addNumTerm,+ andBitsTerm,+ andTerm,+ bvToSignedTerm,+ bvToUnsignedTerm,+ bvconcatTerm,+ bvextendTerm,+ bvselectTerm,+ complementBitsTerm,+ conTerm,+ constructBinary,+ constructTernary,+ constructUnary,+ divBoundedIntegralTerm,+ divIntegralTerm,+ eqvTerm,+ generalFunApplyTerm,+ iteTerm,+ leNumTerm,+ ltNumTerm,+ modBoundedIntegralTerm,+ modIntegralTerm,+ notTerm,+ orBitsTerm,+ orTerm,+ quotBoundedIntegralTerm,+ quotIntegralTerm,+ remBoundedIntegralTerm,+ remIntegralTerm,+ rotateBitsTerm,+ shiftBitsTerm,+ signumNumTerm,+ symTerm,+ tabularFunApplyTerm,+ timesNumTerm,+ uminusNumTerm,+ xorBitsTerm,+ ) import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution+ ( substTerm,+ ) import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils+ ( identity,+ introSupportedPrimConstraint,+ pformat,+ ) import Grisette.IR.SymPrim.Data.Prim.ModelValue+ ( ModelValue,+ toModelValue,+ ) import Grisette.IR.SymPrim.Data.Prim.Utils-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.TabularFun-import Language.Haskell.TH.Syntax-import Language.Haskell.TH.Syntax.Compat+ ( eqHeteroRep,+ eqTypeRepBool,+ )+import Grisette.IR.SymPrim.Data.TabularFun+ ( type (=->) (TabularFun),+ )+import Language.Haskell.TH.Syntax (Lift (lift, liftTyped))+import Language.Haskell.TH.Syntax.Compat (unTypeSplice) import Type.Reflection+ ( SomeTypeRep (SomeTypeRep),+ TypeRep,+ Typeable,+ eqTypeRep,+ typeRep,+ type (:~~:) (HRefl),+ ) #if MIN_VERSION_prettyprinter(1,7,0) import Prettyprinter+ ( column,+ pageWidth,+ Doc,+ PageWidth(Unbounded, AvailablePerLine),+ Pretty(pretty),+ ) #else import Data.Text.Prettyprint.Doc+ ( column,+ pageWidth,+ Doc,+ PageWidth(Unbounded, AvailablePerLine),+ Pretty(pretty),+ ) #endif -- $setup@@ -89,7 +170,7 @@ -- term. class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t where type PrimConstraint t :: Constraint- type PrimConstraint t = ()+ type PrimConstraint _ = () default withPrim :: (PrimConstraint t) => proxy t -> ((PrimConstraint t) => a) -> a withPrim :: proxy t -> ((PrimConstraint t) => a) -> a withPrim _ i = i@@ -1099,3 +1180,10 @@ instance (SupportedPrim a, SupportedPrim b) => SupportedPrim (a --> b) where type PrimConstraint (a --> b) = (SupportedPrim a, SupportedPrim b) defaultValue = buildGeneralFun (SimpleSymbol "a") (conTerm defaultValue)++instance+ (SupportedPrim a, SupportedPrim b) =>+ SupportedPrim (a =-> b)+ where+ type PrimConstraint (a =-> b) = (SupportedPrim a, SupportedPrim b)+ defaultValue = TabularFun [] (defaultValue @b)
src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot view
@@ -28,22 +28,29 @@ ) where -import Control.DeepSeq-import Data.Bits-import Data.Hashable-import Data.Interned-import Data.Kind-import GHC.TypeNats+import Control.DeepSeq (NFData)+import Data.Bits (Bits)+import Data.Hashable (Hashable)+import Data.Interned (Cache, Id)+import Data.Kind (Constraint)+import GHC.TypeNats (KnownNat, type (+), type (<=)) import Grisette.Core.Data.Class.BitVector-import Grisette.Core.Data.Class.Function+ ( BVSignConversion,+ SizedBV,+ ) import Grisette.IR.SymPrim.Data.Prim.ModelValue+ ( ModelValue,+ toModelValue,+ ) import {-# SOURCE #-} Grisette.IR.SymPrim.Data.TabularFun-import Language.Haskell.TH.Syntax-import Type.Reflection+ ( type (=->),+ )+import Language.Haskell.TH.Syntax (Lift)+import Type.Reflection (TypeRep, Typeable) class (Lift t, Typeable t, Hashable t, Eq t, Show t, NFData t) => SupportedPrim t where type PrimConstraint t :: Constraint- type PrimConstraint t = ()+ type PrimConstraint _ = () default withPrim :: (PrimConstraint t) => proxy t -> ((PrimConstraint t) => a) -> a withPrim :: proxy t -> ((PrimConstraint t) => a) -> a withPrim _ i = i
src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE GADTs #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}@@ -12,21 +13,122 @@ -- Maintainer : siruilu@cs.washington.edu -- Stability : Experimental -- Portability : GHC only-module Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution (substTerm) where+module Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution+ ( substTerm,+ )+where -import Grisette.Core.Data.MemoUtils+import Grisette.Core.Data.MemoUtils (htmemo) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( conTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm+ ( SomeTerm (SomeTerm),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( BinaryOp (partialEvalBinary),+ SupportedPrim,+ Term+ ( AbsNumTerm,+ AddNumTerm,+ AndBitsTerm,+ AndTerm,+ BVConcatTerm,+ BVExtendTerm,+ BVSelectTerm,+ BVToSignedTerm,+ BVToUnsignedTerm,+ BinaryTerm,+ ComplementBitsTerm,+ ConTerm,+ DivBoundedIntegralTerm,+ DivIntegralTerm,+ EqvTerm,+ GeneralFunApplyTerm,+ ITETerm,+ LENumTerm,+ LTNumTerm,+ ModBoundedIntegralTerm,+ ModIntegralTerm,+ NotTerm,+ OrBitsTerm,+ OrTerm,+ QuotBoundedIntegralTerm,+ QuotIntegralTerm,+ RemBoundedIntegralTerm,+ RemIntegralTerm,+ RotateBitsTerm,+ ShiftBitsTerm,+ SignumNumTerm,+ SymTerm,+ TabularFunApplyTerm,+ TernaryTerm,+ TimesNumTerm,+ UMinusNumTerm,+ UnaryTerm,+ XorBitsTerm+ ),+ TernaryOp (partialEvalTernary),+ TypedSymbol,+ UnaryOp (partialEvalUnary),+ someTypedSymbol,+ type (-->) (GeneralFun),+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV+ ( pevalBVConcatTerm,+ pevalBVExtendTerm,+ pevalBVSelectTerm,+ pevalBVToSignedTerm,+ pevalBVToUnsignedTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits+ ( pevalAndBitsTerm,+ pevalComplementBitsTerm,+ pevalOrBitsTerm,+ pevalRotateBitsTerm,+ pevalShiftBitsTerm,+ pevalXorBitsTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool+ ( pevalAndTerm,+ pevalEqvTerm,+ pevalITETerm,+ pevalNotTerm,+ pevalOrTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun+ ( pevalGeneralFunApplyTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral+ ( pevalDivBoundedIntegralTerm,+ pevalDivIntegralTerm,+ pevalModBoundedIntegralTerm,+ pevalModIntegralTerm,+ pevalQuotBoundedIntegralTerm,+ pevalQuotIntegralTerm,+ pevalRemBoundedIntegralTerm,+ pevalRemIntegralTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num+ ( pevalAbsNumTerm,+ pevalAddNumTerm,+ pevalLeNumTerm,+ pevalLtNumTerm,+ pevalSignumNumTerm,+ pevalTimesNumTerm,+ pevalUMinusNumTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun+ ( pevalTabularFunApplyTerm,+ ) import Type.Reflection-import Unsafe.Coerce+ ( TypeRep,+ eqTypeRep,+ typeRep,+ pattern App,+ type (:~~:) (HRefl),+ )+import Unsafe.Coerce (unsafeCoerce) substTerm :: forall a b. (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term a -> Term b -> Term b substTerm sym term = gov
src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs-boot view
@@ -1,7 +1,20 @@ {-# LANGUAGE RankNTypes #-} -module Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution (substTerm) where+module Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution+ ( substTerm,+ )+where import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( SupportedPrim,+ Term,+ TypedSymbol,+ ) -substTerm :: forall a b. (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term a -> Term b -> Term b+substTerm ::+ forall a b.+ (SupportedPrim a, SupportedPrim b) =>+ TypedSymbol a ->+ Term a ->+ Term b ->+ Term b
src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs view
@@ -27,13 +27,74 @@ where import Control.Monad.State-import Data.HashMap.Strict as M-import Data.HashSet as S-import Data.Interned+ ( MonadState (get, put),+ State,+ evalState,+ execState,+ gets,+ modify',+ )+import qualified Data.HashMap.Strict as M+import qualified Data.HashSet as S+import Data.Interned (Id) import Data.Typeable+ ( Proxy (Proxy),+ TypeRep,+ Typeable,+ cast,+ typeRep,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm+ ( SomeTerm (SomeTerm),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term-import Grisette.IR.SymPrim.Data.TabularFun ()+ ( BinaryOp (pformatBinary),+ SomeTypedSymbol (SomeTypedSymbol),+ SupportedPrim (pformatCon, pformatSym),+ Term+ ( AbsNumTerm,+ AddNumTerm,+ AndBitsTerm,+ AndTerm,+ BVConcatTerm,+ BVExtendTerm,+ BVSelectTerm,+ BVToSignedTerm,+ BVToUnsignedTerm,+ BinaryTerm,+ ComplementBitsTerm,+ ConTerm,+ DivBoundedIntegralTerm,+ DivIntegralTerm,+ EqvTerm,+ GeneralFunApplyTerm,+ ITETerm,+ LENumTerm,+ LTNumTerm,+ ModBoundedIntegralTerm,+ ModIntegralTerm,+ NotTerm,+ OrBitsTerm,+ OrTerm,+ QuotBoundedIntegralTerm,+ QuotIntegralTerm,+ RemBoundedIntegralTerm,+ RemIntegralTerm,+ RotateBitsTerm,+ ShiftBitsTerm,+ SignumNumTerm,+ SymTerm,+ TabularFunApplyTerm,+ TernaryTerm,+ TimesNumTerm,+ UMinusNumTerm,+ UnaryTerm,+ XorBitsTerm+ ),+ TernaryOp (pformatTernary),+ TypedSymbol,+ UnaryOp (pformatUnary),+ ) import qualified Type.Reflection as R identity :: Term t -> Id
src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs-boot view
@@ -12,10 +12,14 @@ ) where -import Data.HashSet as S-import Data.Interned-import Data.Typeable+import qualified Data.HashSet as S+import Data.Interned (Id)+import Data.Typeable (TypeRep, Typeable) import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( SomeTypedSymbol,+ SupportedPrim,+ Term,+ ) identity :: Term t -> Id identityWithTypeRep :: forall t. Term t -> (TypeRep, Id)
src/Grisette/IR/SymPrim/Data/Prim/Model.hs view
@@ -5,6 +5,7 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}@@ -29,26 +30,157 @@ import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S-import Data.Hashable-import Data.List-import Data.Proxy-import GHC.Generics+import Data.Hashable (Hashable)+import Data.List (sort, sortOn)+import Data.Proxy (Proxy (Proxy))+import GHC.Generics (Generic) import Grisette.Core.Data.Class.ExtractSymbolics+ ( ExtractSymbolics (extractSymbolics),+ ) import Grisette.Core.Data.Class.ModelOps-import Grisette.Core.Data.MemoUtils+ ( ModelOps+ ( emptyModel,+ exceptFor,+ exceptFor',+ extendTo,+ insertValue,+ isEmptyModel,+ modelContains,+ restrictTo,+ valueOf+ ),+ ModelRep (buildModel),+ SymbolSetOps+ ( containsSymbol,+ differenceSet,+ emptySet,+ insertSymbol,+ intersectionSet,+ isEmptySet,+ unionSet+ ),+ SymbolSetRep (buildSymbolSet),+ )+import Grisette.Core.Data.MemoUtils (htmemo) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( conTerm,+ symTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm+ ( SomeTerm (SomeTerm),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( BinaryOp (partialEvalBinary),+ SomeTypedSymbol (SomeTypedSymbol),+ SupportedPrim (defaultValue, defaultValueDynamic),+ Term+ ( AbsNumTerm,+ AddNumTerm,+ AndBitsTerm,+ AndTerm,+ BVConcatTerm,+ BVExtendTerm,+ BVSelectTerm,+ BVToSignedTerm,+ BVToUnsignedTerm,+ BinaryTerm,+ ComplementBitsTerm,+ ConTerm,+ DivBoundedIntegralTerm,+ DivIntegralTerm,+ EqvTerm,+ GeneralFunApplyTerm,+ ITETerm,+ LENumTerm,+ LTNumTerm,+ ModBoundedIntegralTerm,+ ModIntegralTerm,+ NotTerm,+ OrBitsTerm,+ OrTerm,+ QuotBoundedIntegralTerm,+ QuotIntegralTerm,+ RemBoundedIntegralTerm,+ RemIntegralTerm,+ RotateBitsTerm,+ ShiftBitsTerm,+ SignumNumTerm,+ SymTerm,+ TabularFunApplyTerm,+ TernaryTerm,+ TimesNumTerm,+ UMinusNumTerm,+ UnaryTerm,+ XorBitsTerm+ ),+ TernaryOp (partialEvalTernary),+ TypedSymbol,+ UnaryOp (partialEvalUnary),+ showUntyped,+ someTypedSymbol,+ withSymbolSupported,+ type (-->) (GeneralFun),+ ) import Grisette.IR.SymPrim.Data.Prim.ModelValue+ ( ModelValue,+ toModelValue,+ unsafeFromModelValue,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV+ ( pevalBVConcatTerm,+ pevalBVExtendTerm,+ pevalBVSelectTerm,+ pevalBVToSignedTerm,+ pevalBVToUnsignedTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits+ ( pevalAndBitsTerm,+ pevalComplementBitsTerm,+ pevalOrBitsTerm,+ pevalRotateBitsTerm,+ pevalShiftBitsTerm,+ pevalXorBitsTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool+ ( pevalAndTerm,+ pevalEqvTerm,+ pevalITETerm,+ pevalNotTerm,+ pevalOrTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun+ ( pevalGeneralFunApplyTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral+ ( pevalDivBoundedIntegralTerm,+ pevalDivIntegralTerm,+ pevalModBoundedIntegralTerm,+ pevalModIntegralTerm,+ pevalQuotBoundedIntegralTerm,+ pevalQuotIntegralTerm,+ pevalRemBoundedIntegralTerm,+ pevalRemIntegralTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num+ ( pevalAbsNumTerm,+ pevalAddNumTerm,+ pevalLeNumTerm,+ pevalLtNumTerm,+ pevalSignumNumTerm,+ pevalTimesNumTerm,+ pevalUMinusNumTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun+ ( pevalTabularFunApplyTerm,+ ) import Type.Reflection-import Unsafe.Coerce+ ( TypeRep,+ eqTypeRep,+ typeRep,+ pattern App,+ type (:~~:) (HRefl),+ )+import Unsafe.Coerce (unsafeCoerce) -- $setup -- >>> import Grisette.Core
src/Grisette/IR/SymPrim/Data/Prim/Model.hs-boot view
@@ -1,7 +1,12 @@-module Grisette.IR.SymPrim.Data.Prim.Model where+module Grisette.IR.SymPrim.Data.Prim.Model+ ( SymbolSet (..),+ )+where import qualified Data.HashSet as S import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( SomeTypedSymbol,+ ) newtype SymbolSet = SymbolSet {unSymbolSet :: S.HashSet SomeTypedSymbol}
src/Grisette/IR/SymPrim/Data/Prim/ModelValue.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE ExplicitNamespaces #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -18,8 +19,14 @@ ) where -import Data.Hashable+import Data.Hashable (Hashable (hashWithSalt)) import Type.Reflection+ ( TypeRep,+ Typeable,+ eqTypeRep,+ typeRep,+ type (:~~:) (HRefl),+ ) data ModelValue where ModelValue :: forall v. (Show v, Eq v, Hashable v) => TypeRep v -> v -> ModelValue
src/Grisette/IR/SymPrim/Data/Prim/PartialEval/BV.hs view
@@ -29,13 +29,31 @@ ) where -import Data.Typeable-import GHC.TypeNats+import Data.Typeable (Typeable)+import GHC.TypeNats (KnownNat, type (+), type (<=)) import Grisette.Core.Data.Class.BitVector+ ( BVSignConversion (toSigned, toUnsigned),+ SizedBV (sizedBVConcat, sizedBVSelect, sizedBVSext, sizedBVZext),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( bvToSignedTerm,+ bvToUnsignedTerm,+ bvconcatTerm,+ bvextendTerm,+ bvselectTerm,+ conTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( SupportedPrim,+ Term (BVToSignedTerm, BVToUnsignedTerm, ConTerm),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils+ ( castTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold+ ( binaryUnfoldOnce,+ unaryUnfoldOnce,+ ) -- ToSigned pevalBVToSignedTerm ::
src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bits.hs view
@@ -26,10 +26,35 @@ where import Data.Bits-import Data.Typeable+ ( Bits+ ( bitSizeMaybe,+ complement,+ rotate,+ shift,+ xor,+ zeroBits,+ (.&.),+ (.|.)+ ),+ )+import Data.Typeable (Typeable, cast) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( andBitsTerm,+ complementBitsTerm,+ conTerm,+ orBitsTerm,+ rotateBitsTerm,+ shiftBitsTerm,+ xorBitsTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( SupportedPrim,+ Term (ComplementBitsTerm, ConTerm, RotateBitsTerm, ShiftBitsTerm),+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold+ ( binaryUnfoldOnce,+ unaryUnfoldOnce,+ ) bitsConTermView :: (Bits b, Typeable b) => Term a -> Maybe b bitsConTermView (ConTerm _ b) = cast b
src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bool.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ExplicitNamespaces #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-}@@ -35,14 +36,34 @@ ) where -import Control.Monad-import Data.Maybe-import Data.Typeable+import Control.Monad (msum)+import Data.Maybe (fromMaybe)+import Data.Typeable (cast, eqT, type (:~:) (Refl)) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( andTerm,+ conTerm,+ eqvTerm,+ iteTerm,+ notTerm,+ orTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( SupportedPrim,+ Term+ ( AddNumTerm,+ AndTerm,+ ConTerm,+ EqvTerm,+ ITETerm,+ NotTerm,+ OrTerm+ ),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils-import Grisette.IR.SymPrim.Data.Prim.Utils-import Unsafe.Coerce+ ( castTerm,+ )+import Grisette.IR.SymPrim.Data.Prim.Utils (pattern Dyn)+import Unsafe.Coerce (unsafeCoerce) trueTerm :: Term Bool trueTerm = conTerm True
src/Grisette/IR/SymPrim/Data/Prim/PartialEval/GeneralFun.hs view
@@ -11,14 +11,26 @@ -- Maintainer : siruilu@cs.washington.edu -- Stability : Experimental -- Portability : GHC only-module Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun (pevalGeneralFunApplyTerm) where+module Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun+ ( pevalGeneralFunApplyTerm,+ )+where -import Grisette.Core.Data.Class.Function import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( generalFunApplyTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( SupportedPrim,+ Term (ConTerm, ITETerm),+ type (-->) (GeneralFun),+ ) import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution+ ( substTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool (pevalITETerm) import Grisette.IR.SymPrim.Data.Prim.PartialEval.PartialEval+ ( totalize2,+ ) pevalGeneralFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a --> b) -> Term a -> Term b pevalGeneralFunApplyTerm = totalize2 doPevalGeneralFunApplyTerm generalFunApplyTerm
src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Integral.hs view
@@ -20,12 +20,22 @@ ) where -import Grisette.Core.Data.BV import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( conTerm,+ divBoundedIntegralTerm,+ divIntegralTerm,+ modIntegralTerm,+ quotBoundedIntegralTerm,+ quotIntegralTerm,+ remIntegralTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils+ ( SupportedPrim,+ Term (ConTerm),+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold-import Grisette.IR.SymPrim.Data.Prim.Utils+ ( binaryUnfoldOnce,+ ) -- div pevalDivIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Num.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE ExplicitNamespaces #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-}@@ -31,12 +32,33 @@ ) where -import Data.Typeable+import Data.Typeable (Typeable, cast, eqT, type (:~:) (Refl)) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( absNumTerm,+ addNumTerm,+ conTerm,+ leNumTerm,+ ltNumTerm,+ signumNumTerm,+ timesNumTerm,+ uminusNumTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( SupportedPrim,+ Term+ ( AbsNumTerm,+ AddNumTerm,+ ConTerm,+ TimesNumTerm,+ UMinusNumTerm+ ),+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold-import Grisette.IR.SymPrim.Data.Prim.Utils-import Unsafe.Coerce+ ( binaryUnfoldOnce,+ unaryUnfoldOnce,+ )+import Grisette.IR.SymPrim.Data.Prim.Utils (pattern Dyn)+import Unsafe.Coerce (unsafeCoerce) numConTermView :: (Num b, Typeable b) => Term a -> Maybe b numConTermView (ConTerm _ b) = cast b
src/Grisette/IR/SymPrim/Data/Prim/PartialEval/PartialEval.hs view
@@ -31,8 +31,8 @@ ) where -import Control.Monad.Except-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+import Control.Monad.Except (MonadError (catchError))+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term (Term) type PartialFun a b = a -> Maybe b
src/Grisette/IR/SymPrim/Data/Prim/PartialEval/TabularFun.hs view
@@ -16,12 +16,25 @@ ) where -import Grisette.Core.Data.Class.Function+import Grisette.Core.Data.Class.Function (Function ((#))) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( conTerm,+ tabularFunApplyTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( SupportedPrim,+ Term (ConTerm),+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool+ ( pevalEqvTerm,+ pevalITETerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.PartialEval+ ( totalize2,+ ) import Grisette.IR.SymPrim.Data.TabularFun+ ( type (=->) (TabularFun),+ ) pevalTabularFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a =-> b) -> Term a -> Term b pevalTabularFunApplyTerm = totalize2 doPevalTabularFunApplyTerm tabularFunApplyTerm
src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Unfold.hs view
@@ -16,11 +16,23 @@ ) where -import Control.Monad.Except-import Data.Typeable+import Control.Monad.Except (MonadError (catchError))+import Data.Typeable (Typeable) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( SupportedPrim,+ Term (ITETerm),+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool+ ( pevalITETerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.PartialEval+ ( PartialRuleBinary,+ PartialRuleUnary,+ TotalRuleBinary,+ TotalRuleUnary,+ totalize,+ totalize2,+ ) unaryPartialUnfoldOnce :: forall a b.
src/Grisette/IR/SymPrim/Data/Prim/Utils.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE ExplicitNamespaces #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-}@@ -26,6 +27,12 @@ import Data.Typeable (cast) import Type.Reflection+ ( TypeRep,+ Typeable,+ eqTypeRep,+ typeRep,+ type (:~~:) (HRefl),+ ) pattern Dyn :: (Typeable a, Typeable b) => a -> b pattern Dyn x <- (cast -> Just x)
src/Grisette/IR/SymPrim/Data/SymPrim.hs view
@@ -10,6 +10,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-}@@ -56,62 +57,227 @@ ) where -import Control.DeepSeq-import Control.Monad.Except+import Control.DeepSeq (NFData (rnf))+import Control.Monad.Except (ExceptT (ExceptT), MonadError (throwError)) import Control.Monad.Identity-import Control.Monad.Trans.Maybe+ ( 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 Data.Bits+ ( Bits+ ( bit,+ bitSize,+ bitSizeMaybe,+ clearBit,+ complement,+ complementBit,+ isSigned,+ popCount,+ rotate,+ rotateL,+ rotateR,+ setBit,+ shift,+ shiftL,+ shiftR,+ testBit,+ unsafeShiftL,+ unsafeShiftR,+ xor,+ zeroBits,+ (.&.),+ (.|.)+ ),+ FiniteBits (finiteBitSize),+ ) import qualified Data.ByteString as B-import Data.Functor.Sum-import Data.Hashable-import Data.Int-import Data.Proxy-import Data.String+import Data.Functor.Sum (Sum)+import Data.Hashable (Hashable (hashWithSalt))+import Data.Int (Int16, Int32, Int64, Int8)+import Data.Proxy (Proxy (Proxy))+import Data.String (IsString (fromString)) import qualified Data.Text as T-import Data.Typeable-import Data.Word+import Data.Typeable (typeRep, type (:~:) (Refl))+import Data.Word (Word16, Word32, Word64, Word8) import GHC.Generics+ ( Generic (Rep, from),+ K1 (K1),+ M1 (M1),+ U1,+ type (:*:) ((:*:)),+ type (:+:) (L1, R1),+ ) import GHC.TypeNats-import Generics.Deriving+ ( KnownNat,+ Nat,+ natVal,+ sameNat,+ type (+),+ type (<=),+ )+import Generics.Deriving (Default (Default, unDefault)) import Grisette.Core.Control.Exception+ ( AssertionError,+ VerificationConditions,+ ) import Grisette.Core.Data.BV+ ( IntN (IntN),+ SomeIntN (SomeIntN),+ SomeWordN (SomeWordN),+ WordN (WordN),+ ) import Grisette.Core.Data.Class.BitVector+ ( BV (bvConcat, bvExt, bvSelect, bvSext, bvZext),+ BVSignConversion (toSigned, toUnsigned),+ SizedBV (sizedBVConcat, sizedBVExt, sizedBVSelect, sizedBVSext, sizedBVZext),+ ) import Grisette.Core.Data.Class.Bool-import Grisette.Core.Data.Class.Error-import Grisette.Core.Data.Class.Evaluate+ ( LogicalOp (nots, (&&~), (||~)),+ SEq ((/=~), (==~)),+ )+import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym)) import Grisette.Core.Data.Class.ExtractSymbolics-import Grisette.Core.Data.Class.Function-import Grisette.Core.Data.Class.GPretty-import Grisette.Core.Data.Class.GenSym-import Grisette.Core.Data.Class.Mergeable+ ( ExtractSymbolics (extractSymbolics),+ )+import Grisette.Core.Data.Class.Function (Function (Arg, Ret, (#)))+import Grisette.Core.Data.Class.GPretty (GPretty (gpretty)) import Grisette.Core.Data.Class.ModelOps-import Grisette.Core.Data.Class.SOrd+ ( ModelOps (emptyModel, insertValue),+ ModelRep (buildModel),+ )+import Grisette.Core.Data.Class.SOrd (SOrd (symCompare, (<=~), (<~), (>=~), (>~))) import Grisette.Core.Data.Class.SafeArith-import Grisette.Core.Data.Class.SimpleMergeable+ ( ArithException (DivideByZero, Overflow, Underflow),+ SafeDivision+ ( safeDiv,+ safeDiv',+ safeDivMod,+ safeDivMod',+ safeMod,+ safeMod',+ safeQuot,+ safeQuot',+ safeQuotRem,+ safeQuotRem',+ safeRem,+ safeRem'+ ),+ SafeLinearArith+ ( safeAdd,+ safeAdd',+ safeMinus,+ safeMinus',+ safeNeg,+ safeNeg'+ ),+ SymIntegerOp,+ )+import Grisette.Core.Data.Class.SimpleMergeable (mrgIf) import Grisette.Core.Data.Class.Solvable-import Grisette.Core.Data.Class.Substitute-import Grisette.Core.Data.Class.ToCon-import Grisette.Core.Data.Class.ToSym-import Grisette.IR.SymPrim.Data.IntBitwidth+ ( Solvable (con, conView, iinfosym, isym, sinfosym, ssym),+ pattern Con,+ )+import Grisette.Core.Data.Class.Substitute (SubstituteSym (substituteSym))+import Grisette.Core.Data.Class.ToCon (ToCon (toCon))+import Grisette.Core.Data.Class.ToSym (ToSym (toSym))+import Grisette.IR.SymPrim.Data.IntBitwidth (intBitwidthQ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( conTerm,+ iinfosymTerm,+ isymTerm,+ sinfosymTerm,+ ssymTerm,+ symTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm+ ( SomeTerm (SomeTerm),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( ConRep (ConType),+ LinkedRep (underlyingTerm, wrapTerm),+ SupportedPrim,+ SymRep (SymType),+ Term (ConTerm, SymTerm),+ TypedSymbol (WithInfo),+ prettyPrintTerm,+ type (-->) (GeneralFun),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution+ ( substTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils+ ( extractSymbolicsTerm,+ pformat,+ someTermsSize,+ termSize,+ termsSize,+ ) import Grisette.IR.SymPrim.Data.Prim.Model+ ( Model,+ SymbolSet (SymbolSet),+ evaluateTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV+ ( pevalBVConcatTerm,+ pevalBVExtendTerm,+ pevalBVSelectTerm,+ pevalBVToSignedTerm,+ pevalBVToUnsignedTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits+ ( pevalAndBitsTerm,+ pevalComplementBitsTerm,+ pevalOrBitsTerm,+ pevalRotateBitsTerm,+ pevalShiftBitsTerm,+ pevalXorBitsTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool+ ( pevalEqvTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun+ ( pevalGeneralFunApplyTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral+ ( pevalDivBoundedIntegralTerm,+ pevalDivIntegralTerm,+ pevalModBoundedIntegralTerm,+ pevalModIntegralTerm,+ pevalQuotBoundedIntegralTerm,+ pevalQuotIntegralTerm,+ pevalRemBoundedIntegralTerm,+ pevalRemIntegralTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num+ ( pevalAbsNumTerm,+ pevalAddNumTerm,+ pevalGeNumTerm,+ pevalGtNumTerm,+ pevalLeNumTerm,+ pevalLtNumTerm,+ pevalMinusNumTerm,+ pevalSignumNumTerm,+ pevalTimesNumTerm,+ pevalUMinusNumTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun-import Grisette.IR.SymPrim.Data.TabularFun-import Grisette.Lib.Control.Monad+ ( pevalTabularFunApplyTerm,+ )+import Grisette.IR.SymPrim.Data.TabularFun (type (=->))+import Grisette.Lib.Control.Monad (mrgReturn) import Grisette.Utils.Parameterized-import Language.Haskell.TH.Syntax+ ( KnownProof (KnownProof),+ LeqProof (LeqProof),+ knownAdd,+ leqAddPos,+ leqTrans,+ unsafeKnownProof,+ unsafeLeqProof,+ )+import Language.Haskell.TH.Syntax (Lift) -- $setup -- >>> import Grisette.Core@@ -186,7 +352,7 @@ safeNeg v = mrgReturn $ -v safeNeg' _ v = mrgReturn $ -v safeMinus ls rs = mrgReturn $ ls - rs- safeMinus' e ls rs = mrgReturn $ ls - rs+ safeMinus' _ ls rs = mrgReturn $ ls - rs instance SymIntegerOp SymInteger @@ -320,11 +486,11 @@ SomeSymIntN :: (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN unarySomeSymIntN :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> r) -> String -> SomeSymIntN -> r-unarySomeSymIntN op str (SomeSymIntN (w :: SymIntN w)) = op w+unarySomeSymIntN op _ (SomeSymIntN (w :: SymIntN w)) = op w {-# INLINE unarySomeSymIntN #-} unarySomeSymIntNR1 :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n) -> String -> SomeSymIntN -> SomeSymIntN-unarySomeSymIntNR1 op str (SomeSymIntN (w :: SymIntN w)) = SomeSymIntN $ op w+unarySomeSymIntNR1 op _ (SomeSymIntN (w :: SymIntN w)) = SomeSymIntN $ op w {-# INLINE unarySomeSymIntNR1 #-} binSomeSymIntN :: (forall n. (KnownNat n, 1 <= n) => SymIntN n -> SymIntN n -> r) -> String -> SomeSymIntN -> SomeSymIntN -> r@@ -432,11 +598,11 @@ SomeSymWordN :: (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN unarySomeSymWordN :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> r) -> String -> SomeSymWordN -> r-unarySomeSymWordN op str (SomeSymWordN (w :: SymWordN w)) = op w+unarySomeSymWordN op _ (SomeSymWordN (w :: SymWordN w)) = op w {-# INLINE unarySomeSymWordN #-} unarySomeSymWordNR1 :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n) -> String -> SomeSymWordN -> SomeSymWordN-unarySomeSymWordNR1 op str (SomeSymWordN (w :: SymWordN w)) = SomeSymWordN $ op w+unarySomeSymWordNR1 op _ (SomeSymWordN (w :: SymWordN w)) = SomeSymWordN $ op w {-# INLINE unarySomeSymWordNR1 #-} binSomeSymWordN :: (forall n. (KnownNat n, 1 <= n) => SymWordN n -> SymWordN n -> r) -> String -> SomeSymWordN -> SomeSymWordN -> r@@ -1356,7 +1522,7 @@ where \ n = fromIntegral $ natVal (Proxy @n); \ res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> somety; \- res p1 p2 = \+ res _ _ = \ case ( unsafeKnownProof @ix (fromIntegral ix), \ unsafeKnownProof @w (fromIntegral w), \ unsafeLeqProof @1 @w, \@@ -1447,10 +1613,6 @@ someUnderlyingTerm :: SomeSym -> SomeTerm someUnderlyingTerm (SomeSym s) = SomeTerm $ underlyingTerm s--someSymSize :: [SomeSym] -> Int-someSymSize = someTermsSize . fmap someUnderlyingTerm-{-# INLINE someSymSize #-} someSymsSize :: [SomeSym] -> Int someSymsSize = someTermsSize . fmap someUnderlyingTerm
src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot view
@@ -31,18 +31,24 @@ ) where -import Control.DeepSeq-import Data.Hashable-import GHC.Generics-import GHC.TypeNats-import Grisette.Core.Data.BV-import Grisette.Core.Data.Class.Evaluate+import Control.DeepSeq (NFData)+import Data.Hashable (Hashable)+import GHC.TypeNats (KnownNat, Nat, type (<=))+import Grisette.Core.Data.BV (IntN, WordN)+import Grisette.Core.Data.Class.Evaluate (EvaluateSym) import Grisette.Core.Data.Class.ExtractSymbolics-import Grisette.Core.Data.Class.GPretty-import Grisette.Core.Data.Class.Solvable+ ( ExtractSymbolics,+ )+import Grisette.Core.Data.Class.GPretty (GPretty)+import Grisette.Core.Data.Class.Solvable (Solvable) import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term-import Grisette.IR.SymPrim.Data.TabularFun-import Language.Haskell.TH.Syntax+ ( LinkedRep,+ SupportedPrim,+ Term,+ type (-->),+ )+import Grisette.IR.SymPrim.Data.TabularFun (type (=->))+import Language.Haskell.TH.Syntax (Lift) newtype SymBool = SymBool {underlyingBoolTerm :: Term Bool}
src/Grisette/IR/SymPrim/Data/TabularFun.hs view
@@ -2,7 +2,6 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveLift #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} @@ -19,12 +18,11 @@ ) where -import Control.DeepSeq-import Data.Hashable-import GHC.Generics-import Grisette.Core.Data.Class.Function-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term-import Language.Haskell.TH.Syntax+import Control.DeepSeq (NFData, NFData1)+import Data.Hashable (Hashable)+import GHC.Generics (Generic, Generic1)+import Grisette.Core.Data.Class.Function (Function (Arg, Ret, (#)))+import Language.Haskell.TH.Syntax (Lift) -- $setup -- >>> import Grisette.Core@@ -45,13 +43,6 @@ deriving (Show, Eq, Generic, Generic1, Lift, NFData, NFData1) infixr 0 =->--instance- (SupportedPrim a, SupportedPrim b) =>- SupportedPrim (a =-> b)- where- type PrimConstraint (a =-> b) = (SupportedPrim a, SupportedPrim b)- defaultValue = TabularFun [] (defaultValue @b) instance (Eq a) => Function (a =-> b) where type Arg (a =-> b) = a
src/Grisette/IR/SymPrim/Data/TabularFun.hs-boot view
@@ -5,4 +5,18 @@ ) where +import Control.DeepSeq (NFData)+import Data.Hashable (Hashable)+import Language.Haskell.TH.Syntax (Lift)+ data (=->) a b = TabularFun {funcTable :: [(a, b)], defaultFuncValue :: b}++instance (Eq a, Eq b) => Eq (a =-> b)++instance (Show a, Show b) => Show (a =-> b)++instance (Hashable a, Hashable b) => Hashable (a =-> b)++instance (Lift a, Lift b) => Lift (a =-> b)++instance (NFData a, NFData b) => NFData (a =-> b)
src/Grisette/Internal/Backend/SBV.hs view
@@ -14,4 +14,7 @@ where import Grisette.Backend.SBV.Data.SMT.Lowering-import Grisette.Backend.SBV.Data.SMT.Solving+ ( lowerSinglePrim,+ parseModel,+ )+import Grisette.Backend.SBV.Data.SMT.Solving (TermTy)
src/Grisette/Internal/Core.hs view
@@ -1,4 +1,6 @@ {-# LANGUAGE Trustworthy #-}+-- Disable this warning because we are re-exporting things.+{-# OPTIONS_GHC -Wno-missing-import-lists #-} -- | -- Module : Grisette.Internal.Core@@ -23,4 +25,13 @@ where import Grisette.Core.Control.Monad.UnionM+ ( UnionM (..),+ isMerged,+ underlyingUnion,+ ) import Grisette.Core.Data.Union+ ( Union (..),+ fullReconstruct,+ ifWithLeftMost,+ ifWithStrategy,+ )
src/Grisette/Internal/IR/SymPrim.hs view
@@ -1,4 +1,6 @@ {-# LANGUAGE PatternSynonyms #-}+-- Disable this warning because we are re-exporting things.+{-# OPTIONS_GHC -Wno-missing-import-lists #-} -- | -- Module : Grisette.Internal.IR.SymPrim@@ -91,16 +93,103 @@ where import Grisette.IR.SymPrim.Data.Prim.Helpers+ ( pattern BinaryTermPatt,+ pattern TernaryTermPatt,+ pattern UnaryTermPatt,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( conTerm,+ constructBinary,+ constructTernary,+ constructUnary,+ iinfosymTerm,+ isymTerm,+ sinfosymTerm,+ ssymTerm,+ symTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm+ ( SomeTerm (..),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( BinaryOp (..),+ SomeTypedSymbol (..),+ SupportedPrim (..),+ Term (..),+ TernaryOp (..),+ UnaryOp (..),+ showUntyped,+ someTypedSymbol,+ withSymbolSupported,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils-import Grisette.IR.SymPrim.Data.Prim.Model+ ( castTerm,+ extractSymbolicsTerm,+ identity,+ identityWithTypeRep,+ introSupportedPrimConstraint,+ pformat,+ termSize,+ termsSize,+ )+import Grisette.IR.SymPrim.Data.Prim.Model (evaluateTerm) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool+ ( falseTerm,+ pevalAndTerm,+ pevalEqvTerm,+ pevalITETerm,+ pevalImplyTerm,+ pevalNotEqvTerm,+ pevalNotTerm,+ pevalOrTerm,+ pevalXorTerm,+ trueTerm,+ pattern BoolConTerm,+ pattern BoolTerm,+ pattern FalseTerm,+ pattern TrueTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun+ ( pevalGeneralFunApplyTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral+ ( pevalDivIntegralTerm,+ pevalModIntegralTerm,+ pevalQuotIntegralTerm,+ pevalRemIntegralTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num+ ( pevalAbsNumTerm,+ pevalAddNumTerm,+ pevalGeNumTerm,+ pevalGtNumTerm,+ pevalLeNumTerm,+ pevalLtNumTerm,+ pevalMinusNumTerm,+ pevalSignumNumTerm,+ pevalTimesNumTerm,+ pevalUMinusNumTerm,+ pattern NumConTerm,+ pattern NumOrdConTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.PartialEval+ ( BinaryCommPartialStrategy (..),+ BinaryPartialStrategy (..),+ PartialFun,+ PartialRuleBinary,+ PartialRuleUnary,+ TotalRuleBinary,+ TotalRuleUnary,+ UnaryPartialStrategy (..),+ binaryPartial,+ totalize,+ totalize2,+ unaryPartial,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun+ ( pevalTabularFunApplyTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold-import Grisette.IR.SymPrim.Data.SymPrim+ ( binaryUnfoldOnce,+ unaryUnfoldOnce,+ )
src/Grisette/Lib/Base.hs view
@@ -49,6 +49,37 @@ where import Grisette.Lib.Control.Monad+ ( mrgBindWithStrategy,+ mrgFmap,+ mrgFoldM,+ mrgMplus,+ mrgMzero,+ mrgReturn,+ mrgReturnWithStrategy,+ (>>=~),+ (>>~),+ ) import Grisette.Lib.Data.Foldable+ ( mrgFoldlM,+ mrgFoldrM,+ mrgForM_,+ mrgFor_,+ mrgMapM_,+ mrgMsum,+ mrgSequence_,+ mrgTraverse_,+ ) import Grisette.Lib.Data.List+ ( symDrop,+ symFilter,+ symTake,+ (!!~),+ ) import Grisette.Lib.Data.Traversable+ ( mrgFor,+ mrgForM,+ mrgMapM,+ mrgSequence,+ mrgSequenceA,+ mrgTraverse,+ )
src/Grisette/Lib/Control/Monad.hs view
@@ -25,12 +25,17 @@ ) where -import Control.Monad-import Grisette.Core.Control.Monad.Union-import Grisette.Core.Data.Class.Bool+import Control.Monad (MonadPlus (mplus, mzero))+import Grisette.Core.Control.Monad.Union (MonadUnion) import Grisette.Core.Data.Class.Mergeable+ ( Mergeable,+ MergingStrategy,+ ) import Grisette.Core.Data.Class.SimpleMergeable-import Grisette.Lib.Data.Foldable+ ( UnionLike (mergeWithStrategy),+ merge,+ )+import Grisette.Lib.Data.Foldable (mrgFoldlM) -- | 'return' with 'MergingStrategy' knowledge propagation. mrgReturnWithStrategy :: (MonadUnion u) => MergingStrategy a -> a -> u a
src/Grisette/Lib/Control/Monad.hs-boot view
@@ -1,12 +1,25 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE Trustworthy #-} -module Grisette.Lib.Control.Monad where+module Grisette.Lib.Control.Monad+ ( mrgReturnWithStrategy,+ mrgBindWithStrategy,+ mrgReturn,+ (>>=~),+ mrgFoldM,+ (>>~),+ mrgMzero,+ mrgMplus,+ mrgFmap,+ )+where -import Control.Monad-import Grisette.Core.Control.Monad.Union-import Grisette.Core.Data.Class.Bool+import Control.Monad (MonadPlus)+import Grisette.Core.Control.Monad.Union (MonadUnion) import Grisette.Core.Data.Class.Mergeable+ ( Mergeable,+ MergingStrategy,+ ) mrgReturnWithStrategy :: (MonadUnion u) => MergingStrategy a -> a -> u a mrgBindWithStrategy :: (MonadUnion u) => MergingStrategy b -> u a -> (a -> u b) -> u b
src/Grisette/Lib/Control/Monad/Except.hs view
@@ -15,11 +15,10 @@ ) where -import Control.Monad.Except-import Grisette.Core.Control.Monad.Union-import Grisette.Core.Data.Class.Bool-import Grisette.Core.Data.Class.Mergeable-import Grisette.Core.Data.Class.SimpleMergeable+import Control.Monad.Except (MonadError (catchError, throwError))+import Grisette.Core.Control.Monad.Union (MonadUnion)+import Grisette.Core.Data.Class.Mergeable (Mergeable)+import Grisette.Core.Data.Class.SimpleMergeable (merge) -- | 'throwError' with 'MergingStrategy' knowledge propagation. mrgThrowError :: (MonadError e m, MonadUnion m, Mergeable a) => e -> m a
src/Grisette/Lib/Control/Monad/Trans.hs view
@@ -16,10 +16,10 @@ ) where -import Control.Monad.Trans-import Grisette.Core.Control.Monad.Union-import Grisette.Core.Data.Class.Mergeable-import Grisette.Core.Data.Class.SimpleMergeable+import Control.Monad.Trans (MonadTrans (lift))+import Grisette.Core.Control.Monad.Union (MonadUnion)+import Grisette.Core.Data.Class.Mergeable (Mergeable)+import Grisette.Core.Data.Class.SimpleMergeable (merge) -- | 'lift' with 'MergingStrategy' knowledge propagation. mrgLift ::
src/Grisette/Lib/Control/Monad/Trans/Cont.hs view
@@ -16,12 +16,14 @@ ) where -import Control.Monad.Cont-import Control.Monad.Trans.Class-import Grisette.Core.Data.Class.Bool-import Grisette.Core.Data.Class.Mergeable+import Control.Monad.Cont (ContT (runContT))+import Control.Monad.Trans.Class (lift)+import Grisette.Core.Data.Class.Mergeable (Mergeable) import Grisette.Core.Data.Class.SimpleMergeable-import Grisette.Lib.Control.Monad+ ( UnionLike,+ merge,+ )+import Grisette.Lib.Control.Monad (mrgReturn) -- | 'Control.Monad.Cont.runContT' with 'MergingStrategy' knowledge propagation mrgRunContT :: (UnionLike m, Mergeable r) => ContT r m a -> (a -> m r) -> m r
src/Grisette/Lib/Data/Foldable.hs view
@@ -22,12 +22,15 @@ ) where -import Control.Monad-import Grisette.Core.Control.Monad.Union-import Grisette.Core.Data.Class.Bool-import Grisette.Core.Data.Class.Mergeable-import Grisette.Core.Data.Class.SimpleMergeable+import Control.Monad (MonadPlus)+import Grisette.Core.Control.Monad.Union (MonadUnion)+import Grisette.Core.Data.Class.Mergeable (Mergeable)+import Grisette.Core.Data.Class.SimpleMergeable (merge) import {-# SOURCE #-} Grisette.Lib.Control.Monad+ ( mrgMplus,+ mrgMzero,+ mrgReturn,+ ) -- | 'Data.Foldable.foldlM' with 'MergingStrategy' knowledge propagation. mrgFoldlM :: (MonadUnion m, Mergeable b, Foldable t) => (b -> a -> m b) -> b -> t a -> m b
src/Grisette/Lib/Data/List.hs view
@@ -17,17 +17,16 @@ ) where -import Control.Exception-import Control.Monad.Except-import Grisette.Core.Control.Monad.Union-import Grisette.Core.Data.Class.Bool-import Grisette.Core.Data.Class.Error-import Grisette.Core.Data.Class.Mergeable-import Grisette.Core.Data.Class.SOrd-import Grisette.Core.Data.Class.SafeArith-import Grisette.Core.Data.Class.SimpleMergeable-import Grisette.IR.SymPrim.Data.SymPrim-import Grisette.Lib.Control.Monad+import Control.Exception (ArrayException (IndexOutOfBounds))+import Control.Monad.Except (MonadError (throwError))+import Grisette.Core.Control.Monad.Union (MonadUnion)+import Grisette.Core.Data.Class.Bool (SEq ((==~)))+import Grisette.Core.Data.Class.Error (TransformError (transformError))+import Grisette.Core.Data.Class.Mergeable (Mergeable)+import Grisette.Core.Data.Class.SOrd (SOrd ((<=~)))+import Grisette.Core.Data.Class.SimpleMergeable (mrgIf)+import Grisette.IR.SymPrim.Data.SymPrim (SymBool, SymInteger)+import Grisette.Lib.Control.Monad (mrgFmap, mrgReturn) -- | Symbolic version of 'Data.List.!!', the result would be merged and -- propagate the mergeable knowledge.
src/Grisette/Lib/Data/Traversable.hs view
@@ -21,9 +21,16 @@ ) where -import Grisette.Core.Control.Monad.Union+import Grisette.Core.Control.Monad.Union (MonadUnion) import Grisette.Core.Data.Class.Mergeable+ ( Mergeable,+ Mergeable1,+ rootStrategy1,+ ) import Grisette.Core.Data.Class.SimpleMergeable+ ( UnionLike (mergeWithStrategy),+ merge,+ ) -- | 'Data.Traversable.traverse' with 'MergingStrategy' knowledge propagation. mrgTraverse ::
src/Grisette/Lib/Mtl.hs view
@@ -26,5 +26,12 @@ where import Grisette.Lib.Control.Monad.Except-import Grisette.Lib.Control.Monad.Trans+ ( mrgCatchError,+ mrgThrowError,+ )+import Grisette.Lib.Control.Monad.Trans (mrgLift) import Grisette.Lib.Control.Monad.Trans.Cont+ ( mrgEvalContT,+ mrgResetT,+ mrgRunContT,+ )
src/Grisette/Qualified/ParallelUnionDo.hs view
@@ -6,11 +6,14 @@ -- Maintainer : siruilu@cs.washington.edu -- Stability : Experimental -- Portability : GHC only-module Grisette.Qualified.ParallelUnionDo where+module Grisette.Qualified.ParallelUnionDo ((>>=), (>>)) where -import Control.Parallel.Strategies+import Control.Parallel.Strategies (NFData) import Grisette.Core.Control.Monad.Class.MonadParallelUnion-import Grisette.Core.Data.Class.Mergeable+ ( MonadParallelUnion (parBindUnion),+ )+import Grisette.Core.Data.Class.Mergeable (Mergeable)+import Prelude (const, ($)) (>>=) :: (MonadParallelUnion m, Mergeable b, NFData b) => m a -> (a -> m b) -> m b (>>=) = parBindUnion
src/Grisette/Utils.hs view
@@ -1,3 +1,6 @@+-- Disable this warning because we are re-exporting things.+{-# OPTIONS_GHC -Wno-missing-import-lists #-}+ -- | -- Module : Grisette.Utils -- Copyright : (c) Sirui Lu 2021-2023@@ -48,3 +51,32 @@ where import Grisette.Utils.Parameterized+ ( KnownProof (..),+ LeqProof (..),+ NatRepr,+ addNat,+ decNat,+ divNat,+ halfNat,+ hasRepr,+ incNat,+ knownAdd,+ leqAdd,+ leqAdd2,+ leqAddPos,+ leqRefl,+ leqSucc,+ leqTrans,+ leqZero,+ natRepr,+ natValue,+ predNat,+ subNat,+ testLeq,+ unsafeAxiom,+ unsafeKnownProof,+ unsafeLeqProof,+ unsafeMkNatRepr,+ withKnownProof,+ withLeqProof,+ )
src/Grisette/Utils/Parameterized.hs view
@@ -88,10 +88,20 @@ ) where -import Data.Typeable-import GHC.Natural+import Data.Typeable (Proxy (Proxy), type (:~:) (Refl))+import GHC.Natural (Natural) import GHC.TypeNats-import Unsafe.Coerce+ ( Div,+ KnownNat,+ Nat,+ SomeNat (SomeNat),+ natVal,+ someNatVal,+ type (+),+ type (-),+ type (<=),+ )+import Unsafe.Coerce (unsafeCoerce) -- | Assert a proof of equality between two types. -- This is unsafe if used improperly, so use this with caution!@@ -176,7 +186,7 @@ -- | Adding two type-level natural numbers with known runtime values gives a -- type-level natural number with a known runtime value.-knownAdd :: forall m n r. KnownProof m -> KnownProof n -> KnownProof (m + n)+knownAdd :: forall m n. KnownProof m -> KnownProof n -> KnownProof (m + n) knownAdd KnownProof KnownProof = hasRepr @(m + n) (NatRepr (natVal (Proxy @m) + natVal (Proxy @n))) -- | @'LeqProof m n'@ is a type whose values are only inhabited when @m <= n@.
test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs view
@@ -5,33 +5,53 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} -module Grisette.Backend.SBV.Data.SMT.CEGISTests where+module Grisette.Backend.SBV.Data.SMT.CEGISTests (cegisTests) where -import Control.Monad.Except-import qualified Data.HashSet as S-import Data.Proxy+import Control.Monad.Except (ExceptT, runExceptT)+import Data.Proxy (Proxy (Proxy)) import qualified Data.SBV as SBV-import Data.String-import Grisette.Backend.SBV-import Grisette.Backend.SBV.Data.SMT.Solving+import Data.String (IsString (fromString))+import GHC.Stack (HasCallStack)+import Grisette.Backend.SBV (GrisetteSMTConfig, precise, z3) import Grisette.Core.Control.Exception-import Grisette.Core.Control.Monad.UnionM+ ( VerificationConditions,+ symAssert,+ symAssume,+ )+import Grisette.Core.Control.Monad.UnionM (UnionM) import Grisette.Core.Data.Class.BitVector+ ( SizedBV (sizedBVConcat, sizedBVSelect, sizedBVSext, sizedBVZext),+ ) import Grisette.Core.Data.Class.Bool+ ( ITEOp (ites),+ LogicalOp (nots, xors, (&&~), (||~)),+ SEq ((==~)),+ ) import Grisette.Core.Data.Class.CEGISSolver-import Grisette.Core.Data.Class.Error-import Grisette.Core.Data.Class.Evaluate+ ( CEGISSolver (cegisMultiInputs),+ cegis,+ cegisExceptVC,+ cegisPostCond,+ )+import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym)) import Grisette.Core.Data.Class.ExtractSymbolics-import Grisette.Core.Data.Class.Function-import Grisette.Core.Data.Class.SOrd-import Grisette.Core.Data.Class.SimpleMergeable-import Grisette.Core.Data.Class.Solvable-import Grisette.Core.Data.Class.Solver-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term-import Grisette.IR.SymPrim.Data.Prim.Model+ ( ExtractSymbolics,+ )+import Grisette.Core.Data.Class.Function (Function ((#)))+import Grisette.Core.Data.Class.SOrd (SOrd ((<~), (>=~)))+import Grisette.Core.Data.Class.SimpleMergeable (mrgIf)+import Grisette.Core.Data.Class.Solvable (Solvable (con, ssym))+import Grisette.Core.Data.Class.Solver (Solver (solve)) import Grisette.IR.SymPrim.Data.SymPrim-import Test.Tasty-import Test.Tasty.HUnit+ ( SymBool,+ SymIntN,+ SymInteger,+ type (-~>),+ type (=~>),+ )+import Test.Framework (Test, testGroup)+import Test.Framework.Providers.HUnit (testCase)+import Test.HUnit (Assertion, assertFailure, (@=?)) testCegis :: (HasCallStack, ExtractSymbolics a, EvaluateSym a, Show a) => GrisetteSMTConfig i -> Bool -> a -> [SymBool] -> Assertion testCegis config shouldSuccess a bs = do@@ -63,7 +83,7 @@ (symAssert x) (go xs (i + 1)) -cegisTests :: TestTree+cegisTests :: Test cegisTests = let unboundedConfig = precise SBV.z3 -- {SBV.verbose=True} in testGroup
test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs view
@@ -7,24 +7,74 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} -module Grisette.Backend.SBV.Data.SMT.LoweringTests where+module Grisette.Backend.SBV.Data.SMT.LoweringTests (loweringTests) where -import Control.Monad.Trans+import Control.Monad.Trans (MonadTrans (lift)) import Data.Bits-import Data.Dynamic+ ( Bits (complement, rotate, shift, xor, (.&.), (.|.)),+ )+import Data.Dynamic (Typeable, fromDynamic) import qualified Data.HashMap.Strict as M-import Data.Proxy+import Data.Proxy (Proxy (Proxy)) import qualified Data.SBV as SBV import qualified Data.SBV.Control as SBV-import Grisette.Backend.SBV.Data.SMT.Lowering+import GHC.Stack (HasCallStack)+import Grisette.Backend.SBV.Data.SMT.Lowering (lowerSinglePrim) import Grisette.Backend.SBV.Data.SMT.Solving+ ( GrisetteSMTConfig (sbvConfig),+ TermTy,+ approx,+ precise,+ ) import Grisette.Backend.SBV.Data.SMT.SymBiMap-import Grisette.Core.Data.BV+ ( SymBiMap (biMapToSBV),+ )+import Grisette.Core.Data.BV (IntN, WordN) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( absNumTerm,+ addNumTerm,+ andBitsTerm,+ andTerm,+ bvToSignedTerm,+ bvToUnsignedTerm,+ bvconcatTerm,+ bvselectTerm,+ bvsignExtendTerm,+ bvzeroExtendTerm,+ complementBitsTerm,+ divBoundedIntegralTerm,+ divIntegralTerm,+ eqvTerm,+ iteTerm,+ leNumTerm,+ ltNumTerm,+ modBoundedIntegralTerm,+ modIntegralTerm,+ notTerm,+ orBitsTerm,+ orTerm,+ quotBoundedIntegralTerm,+ quotIntegralTerm,+ remBoundedIntegralTerm,+ remIntegralTerm,+ rotateBitsTerm,+ shiftBitsTerm,+ signumNumTerm,+ ssymTerm,+ timesNumTerm,+ uminusNumTerm,+ xorBitsTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm+ ( SomeTerm (SomeTerm),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term-import Test.Tasty-import Test.Tasty.HUnit+ ( SupportedPrim,+ Term,+ )+import Test.Framework (Test, testGroup)+import Test.Framework.Providers.HUnit (testCase)+import Test.HUnit (Assertion, assertFailure) testUnaryOpLowering :: forall a b as n.@@ -70,21 +120,21 @@ SBV.Unsat -> return () _ -> lift $ assertFailure $ "Lowering for " ++ name ++ " generated unknown formula" -testUnaryOpLowering' ::- forall a b as n tag.- ( HasCallStack,- UnaryOp tag a b,- SBV.EqSymbolic (TermTy n b),- Typeable (TermTy n a),- SBV.SymVal as,- TermTy n a ~ SBV.SBV as,- Show as- ) =>- GrisetteSMTConfig n ->- tag ->- (TermTy n a -> TermTy n b) ->- Assertion-testUnaryOpLowering' config t = testUnaryOpLowering @a @b @as config (constructUnary t) (show t)+-- testUnaryOpLowering' ::+-- forall a b as n tag.+-- ( HasCallStack,+-- UnaryOp tag a b,+-- SBV.EqSymbolic (TermTy n b),+-- Typeable (TermTy n a),+-- SBV.SymVal as,+-- TermTy n a ~ SBV.SBV as,+-- Show as+-- ) =>+-- GrisetteSMTConfig n ->+-- tag ->+-- (TermTy n a -> TermTy n b) ->+-- Assertion+-- testUnaryOpLowering' config t = testUnaryOpLowering @a @b @as config (constructUnary t) (show t) testBinaryOpLowering :: forall a b c as bs n.@@ -139,25 +189,25 @@ _ -> lift $ assertFailure $ "Lowering for " ++ name ++ " generated unknown formula" _ -> lift $ assertFailure "Failed to extract the term" -testBinaryOpLowering' ::- forall a b c as bs n tag.- ( HasCallStack,- BinaryOp tag a b c,- SBV.EqSymbolic (TermTy n c),- Typeable (TermTy n a),- Typeable (TermTy n b),- SBV.SymVal as,- SBV.SymVal bs,- Show as,- Show bs,- TermTy n a ~ SBV.SBV as,- TermTy n b ~ SBV.SBV bs- ) =>- GrisetteSMTConfig n ->- tag ->- (TermTy n a -> TermTy n b -> TermTy n c) ->- Assertion-testBinaryOpLowering' config t = testBinaryOpLowering @a @b @c @as @bs config (constructBinary t) (show t)+-- testBinaryOpLowering' ::+-- forall a b c as bs n tag.+-- ( HasCallStack,+-- BinaryOp tag a b c,+-- SBV.EqSymbolic (TermTy n c),+-- Typeable (TermTy n a),+-- Typeable (TermTy n b),+-- SBV.SymVal as,+-- SBV.SymVal bs,+-- Show as,+-- Show bs,+-- TermTy n a ~ SBV.SBV as,+-- TermTy n b ~ SBV.SBV bs+-- ) =>+-- GrisetteSMTConfig n ->+-- tag ->+-- (TermTy n a -> TermTy n b -> TermTy n c) ->+-- Assertion+-- testBinaryOpLowering' config t = testBinaryOpLowering @a @b @c @as @bs config (constructBinary t) (show t) testTernaryOpLowering :: forall a b c d as bs cs n.@@ -224,31 +274,31 @@ _ -> lift $ assertFailure $ "Lowering for " ++ name ++ " generated unknown formula" _ -> lift $ assertFailure "Failed to extract the term" -testTernaryOpLowering' ::- forall a b c d as bs cs n tag.- ( HasCallStack,- TernaryOp tag a b c d,- SBV.EqSymbolic (TermTy n d),- Typeable (TermTy n a),- Typeable (TermTy n b),- Typeable (TermTy n c),- SBV.SymVal as,- SBV.SymVal bs,- SBV.SymVal cs,- Show as,- Show bs,- Show cs,- TermTy n a ~ SBV.SBV as,- TermTy n b ~ SBV.SBV bs,- TermTy n c ~ SBV.SBV cs- ) =>- GrisetteSMTConfig n ->- tag ->- (TermTy n a -> TermTy n b -> TermTy n c -> TermTy n d) ->- Assertion-testTernaryOpLowering' config t = testTernaryOpLowering @a @b @c @d @as @bs @cs config (constructTernary t) (show t)+-- testTernaryOpLowering' ::+-- forall a b c d as bs cs n tag.+-- ( HasCallStack,+-- TernaryOp tag a b c d,+-- SBV.EqSymbolic (TermTy n d),+-- Typeable (TermTy n a),+-- Typeable (TermTy n b),+-- Typeable (TermTy n c),+-- SBV.SymVal as,+-- SBV.SymVal bs,+-- SBV.SymVal cs,+-- Show as,+-- Show bs,+-- Show cs,+-- TermTy n a ~ SBV.SBV as,+-- TermTy n b ~ SBV.SBV bs,+-- TermTy n c ~ SBV.SBV cs+-- ) =>+-- GrisetteSMTConfig n ->+-- tag ->+-- (TermTy n a -> TermTy n b -> TermTy n c -> TermTy n d) ->+-- Assertion+-- testTernaryOpLowering' config t = testTernaryOpLowering @a @b @c @d @as @bs @cs config (constructTernary t) (show t) -loweringTests :: TestTree+loweringTests :: Test loweringTests = let unboundedConfig = precise SBV.z3 boundedConfig = approx (Proxy @5) SBV.z3
test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs view
@@ -12,22 +12,127 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -module Grisette.Backend.SBV.Data.SMT.TermRewritingGen where+module Grisette.Backend.SBV.Data.SMT.TermRewritingGen+ ( TermRewritingSpec (..),+ GeneralSpec (..),+ DifferentSizeBVSpec (..),+ FixedSizedBVWithBoolSpec (..),+ BoolWithLIASpec (..),+ LIAWithBoolSpec (..),+ BoolOnlySpec (..),+ constructUnarySpec',+ constructBinarySpec',+ constructTernarySpec',+ divIntegralSpec,+ modIntegralSpec,+ quotIntegralSpec,+ remIntegralSpec,+ divBoundedIntegralSpec,+ modBoundedIntegralSpec,+ quotBoundedIntegralSpec,+ remBoundedIntegralSpec,+ uminusNumSpec,+ timesNumSpec,+ addNumSpec,+ iteSpec,+ eqvSpec,+ notSpec,+ andSpec,+ orSpec,+ )+where -import Data.Bits-import Data.Data-import Data.Kind-import GHC.TypeLits-import Grisette.Core.Data.Class.BitVector+import Data.Bits (Bits)+import Data.Data (Proxy (Proxy), Typeable)+import Data.Kind (Type)+import GHC.TypeLits (KnownNat, Nat, type (+), type (<=))+import Grisette.Core.Data.Class.BitVector (SizedBV) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( absNumTerm,+ addNumTerm,+ andBitsTerm,+ andTerm,+ bvconcatTerm,+ bvextendTerm,+ bvselectTerm,+ complementBitsTerm,+ conTerm,+ constructBinary,+ constructTernary,+ constructUnary,+ divBoundedIntegralTerm,+ divIntegralTerm,+ eqvTerm,+ iteTerm,+ leNumTerm,+ ltNumTerm,+ modBoundedIntegralTerm,+ modIntegralTerm,+ notTerm,+ orBitsTerm,+ orTerm,+ quotBoundedIntegralTerm,+ quotIntegralTerm,+ remBoundedIntegralTerm,+ remIntegralTerm,+ rotateBitsTerm,+ shiftBitsTerm,+ signumNumTerm,+ ssymTerm,+ timesNumTerm,+ uminusNumTerm,+ xorBitsTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( BinaryOp (partialEvalBinary),+ SupportedPrim,+ Term,+ TernaryOp (partialEvalTernary),+ UnaryOp (partialEvalUnary),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils+ ( pformat,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV+ ( pevalBVConcatTerm,+ pevalBVExtendTerm,+ pevalBVSelectTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits+ ( pevalAndBitsTerm,+ pevalComplementBitsTerm,+ pevalOrBitsTerm,+ pevalRotateBitsTerm,+ pevalShiftBitsTerm,+ pevalXorBitsTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool+ ( pevalAndTerm,+ pevalEqvTerm,+ pevalITETerm,+ pevalNotTerm,+ pevalOrTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral+ ( pevalDivBoundedIntegralTerm,+ pevalDivIntegralTerm,+ pevalModBoundedIntegralTerm,+ pevalModIntegralTerm,+ pevalQuotBoundedIntegralTerm,+ pevalQuotIntegralTerm,+ pevalRemBoundedIntegralTerm,+ pevalRemIntegralTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num-import Test.Tasty.QuickCheck+ ( pevalAbsNumTerm,+ pevalAddNumTerm,+ pevalLeNumTerm,+ pevalLtNumTerm,+ pevalSignumNumTerm,+ pevalTimesNumTerm,+ pevalUMinusNumTerm,+ )+import Test.QuickCheck (Arbitrary (arbitrary), Gen, frequency, oneof, sized) class (SupportedPrim b) => TermRewritingSpec a b | a -> b where norewriteVer :: a -> Term b
test/Grisette/Backend/SBV/Data/SMT/TermRewritingTests.hs view
@@ -4,20 +4,63 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE UndecidableInstances #-} -module Grisette.Backend.SBV.Data.SMT.TermRewritingTests where+module Grisette.Backend.SBV.Data.SMT.TermRewritingTests+ ( termRewritingTests,+ )+where -import Data.Foldable+import Data.Foldable (traverse_) import qualified Data.SBV as SBV import Grisette.Backend.SBV.Data.SMT.Solving+ ( GrisetteSMTConfig,+ precise,+ ) import Grisette.Backend.SBV.Data.SMT.TermRewritingGen-import Grisette.Core.Data.BV-import Grisette.Core.Data.Class.Solver+ ( BoolOnlySpec,+ BoolWithLIASpec,+ DifferentSizeBVSpec,+ FixedSizedBVWithBoolSpec,+ GeneralSpec,+ LIAWithBoolSpec,+ TermRewritingSpec+ ( conSpec,+ counterExample,+ norewriteVer,+ rewriteVer,+ same,+ symSpec+ ),+ addNumSpec,+ andSpec,+ divBoundedIntegralSpec,+ divIntegralSpec,+ eqvSpec,+ iteSpec,+ modBoundedIntegralSpec,+ modIntegralSpec,+ notSpec,+ orSpec,+ quotBoundedIntegralSpec,+ quotIntegralSpec,+ remBoundedIntegralSpec,+ remIntegralSpec,+ timesNumSpec,+ uminusNumSpec,+ )+import Grisette.Core.Data.BV (IntN, WordN)+import Grisette.Core.Data.Class.Solver (Solver (solve)) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( SupportedPrim,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils-import Grisette.IR.SymPrim.Data.SymPrim-import Test.Tasty-import Test.Tasty.HUnit-import Test.Tasty.QuickCheck+ ( pformat,+ )+import Grisette.IR.SymPrim.Data.SymPrim (SymBool (SymBool))+import Test.Framework (Test, TestName, testGroup)+import Test.Framework.Providers.HUnit (testCase)+import Test.Framework.Providers.QuickCheck2 (testProperty)+import Test.HUnit (Assertion, assertFailure)+import Test.QuickCheck (ioProperty, mapSize) validateSpec :: (TermRewritingSpec a av, Show a, SupportedPrim av) => GrisetteSMTConfig n -> a -> Assertion validateSpec config a = do@@ -38,7 +81,7 @@ (TermRewritingSpec a b, Show a, Enum b, Num b, SupportedPrim b) => TestName -> (a -> a -> a) ->- TestTree+ Test divisionTest name f = testGroup name@@ -57,7 +100,7 @@ [-3 .. 3] ] -termRewritingTests :: TestTree+termRewritingTests :: Test termRewritingTests = testGroup "TermRewritingTests"
test/Grisette/Core/Control/Monad/UnionMTests.hs view
@@ -1,15 +1,19 @@ {-# LANGUAGE OverloadedStrings #-} -module Grisette.Core.Control.Monad.UnionMTests where+module Grisette.Core.Control.Monad.UnionMTests (unionMTests) where -import Grisette.Core.Control.Monad.UnionM-import Grisette.Core.Data.Class.GenSym+import Grisette.Core.Control.Monad.UnionM (UnionM, unionSize)+import Grisette.Core.Data.Class.GenSym (choose) import Grisette.Core.Data.Class.SimpleMergeable-import Grisette.Core.Data.Class.Solvable-import Test.Tasty-import Test.Tasty.HUnit+ ( UnionLike (single),+ mrgIf,+ )+import Grisette.Core.Data.Class.Solvable (Solvable (ssym))+import Test.Framework (Test, testGroup)+import Test.Framework.Providers.HUnit (testCase)+import Test.HUnit ((@=?)) -unionMTests :: TestTree+unionMTests :: Test unionMTests = testGroup "UnionMTests"
test/Grisette/Core/Data/BVTests.hs view
@@ -4,22 +4,61 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} -module Grisette.Core.Data.BVTests where+module Grisette.Core.Data.BVTests (bvTests) where -import Control.DeepSeq+import Control.DeepSeq (NFData (rnf), deepseq, force) import Control.Exception-import Control.Monad-import Data.Bifunctor+ ( ArithException,+ SomeException,+ catch,+ evaluate,+ )+import Control.Monad (when)+import Data.Bifunctor (Bifunctor (bimap)) import Data.Bits-import Data.Int-import Data.Proxy-import Data.Typeable-import Data.Word-import Grisette.Core.Data.BV+ ( Bits+ ( bit,+ bitSizeMaybe,+ clearBit,+ complement,+ complementBit,+ isSigned,+ popCount,+ rotate,+ rotateL,+ rotateR,+ setBit,+ shift,+ shiftL,+ shiftR,+ testBit,+ xor,+ zeroBits,+ (.&.),+ (.|.)+ ),+ FiniteBits (countLeadingZeros, countTrailingZeros, finiteBitSize),+ )+import Data.Int (Int8)+import Data.Proxy (Proxy (Proxy))+import Data.Typeable (Typeable, typeRep)+import Data.Word (Word8)+import GHC.Stack (HasCallStack)+import Grisette.Core.Data.BV (IntN (IntN), WordN (unWordN)) import Grisette.Core.Data.Class.BitVector-import Test.Tasty-import Test.Tasty.HUnit-import Test.Tasty.QuickCheck hiding ((.&.))+ ( SizedBV+ ( sizedBVConcat,+ sizedBVExt,+ sizedBVSelect,+ sizedBVSext,+ sizedBVZext+ ),+ )+import Test.Framework (Test, TestName, testGroup)+import Test.Framework.Providers.HUnit (testCase)+import Test.Framework.Providers.QuickCheck2 (testProperty)+import Test.HUnit (Assertion, assertFailure, (@=?))+import Test.QuickCheck (Arbitrary, Property, ioProperty) unaryConform :: forall a b c d. (Show c, Eq c, HasCallStack) => (a -> b) -> (d -> c) -> (a -> c) -> (b -> d) -> a -> Property unaryConform a2b d2c f g x = ioProperty $ f x @=? d2c (g (a2b x))@@ -80,7 +119,7 @@ Proxy ref -> Proxy typ -> Int ->- TestTree+ Test finiteBitsConformTest pref ptyp numBits = testGroup (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for FiniteBits instances")@@ -94,7 +133,7 @@ (Typeable ref, Typeable typ, Bounded typ, Bounded ref, Integral ref, Num typ, Eq typ, Show typ) => Proxy ref -> Proxy typ ->- TestTree+ Test boundedConformTest pref ptyp = testGroup (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for Bounded instances")@@ -117,7 +156,7 @@ (b -> b) -> a -> b ->- TestTree+ Test succPredLikeTest name boundName a2b fa fb bounda boundb = testGroup name@@ -144,7 +183,7 @@ ) => Proxy ref -> Proxy typ ->- TestTree+ Test enumConformTest pref ptyp = testGroup (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for Enum instances")@@ -203,10 +242,10 @@ (a -> b) -> (a -> a -> a) -> (b -> b -> b) ->- TestTree+ Test divLikeTest name a2b fa fb = testGroup- "name"+ name [ testCase "divided by zero" $ do sameDiv 1 0 a2b fa fb sameDiv 0 0 a2b fa fb@@ -225,10 +264,10 @@ (a -> b) -> (a -> a -> (a, a)) -> (b -> b -> (b, b)) ->- TestTree+ Test divModLikeTest name a2b fa fb = testGroup- "name"+ name [ testCase "divided by zero" $ do sameDivMod 1 0 a2b fa fb sameDivMod 0 0 a2b fa fb@@ -245,7 +284,7 @@ (Typeable ref, Typeable typ, Integral ref, Num typ, Arbitrary ref, Real typ, Show ref) => proxy ref -> proxy typ ->- TestTree+ Test realConformTest pref ptyp = testGroup (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for Real instances")@@ -274,7 +313,7 @@ ) => Proxy ref -> Proxy typ ->- TestTree+ Test integralConformTest pref ptyp = testGroup (show (typeRep ptyp) ++ " conform to " ++ show (typeRep pref) ++ " for Integral instances")@@ -287,7 +326,7 @@ testProperty "toInteger" $ unaryConform @ref @typ fromIntegral id toInteger toInteger ] -bvTests :: TestTree+bvTests :: Test bvTests = testGroup "BVTests"
test/Grisette/Core/Data/Class/GPrettyTests.hs view
@@ -5,31 +5,46 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} -module Grisette.Core.Data.Class.GPrettyTests where+module Grisette.Core.Data.Class.GPrettyTests (gprettyTests) where -import Data.Int-import Data.Text as T-import Data.Word-import GHC.Generics-import GHC.Stack-import Generics.Deriving+import Data.Int (Int16, Int32, Int64, Int8)+import Data.Text as T (Text, pack, unpack)+import Data.Word (Word16, Word32, Word64, Word8)+import GHC.Generics (Generic)+import GHC.Stack (HasCallStack)+import Generics.Deriving (Default (Default)) import Grisette.Core.Data.BV-import Grisette.Core.Data.Class.Bool-import Grisette.Core.Data.Class.GPretty-import Grisette.IR.SymPrim.Data.SymPrim-import Test.Tasty-import Test.Tasty.HUnit-import Test.Tasty.QuickCheck hiding ((.&.))+ ( IntN,+ SomeIntN (SomeIntN),+ SomeWordN (SomeWordN),+ WordN,+ )+import Grisette.Core.Data.Class.Bool (LogicalOp ((&&~)))+import Grisette.Core.Data.Class.GPretty (GPretty (gpretty))+import Grisette.IR.SymPrim.Data.SymPrim (SymBool)+import Test.Framework (Test, testGroup)+import Test.Framework.Providers.HUnit (testCase)+import Test.Framework.Providers.QuickCheck2 (testProperty)+import Test.HUnit ((@=?))+import Test.QuickCheck (Arbitrary (arbitrary), Gen, forAll, oneof) #if MIN_VERSION_prettyprinter(1,7,0) import Prettyprinter-import Prettyprinter.Render.Text+ ( PageWidth(AvailablePerLine, Unbounded),+ layoutPretty,+ LayoutOptions(LayoutOptions),+ )+import Prettyprinter.Render.Text (renderStrict) #else import Data.Text.Prettyprint.Doc-import Data.Text.Prettyprint.Doc.Render.Text+ ( PageWidth(AvailablePerLine, Unbounded),+ layoutPretty,+ LayoutOptions(LayoutOptions),+ )+import Data.Text.Prettyprint.Doc.Render.Text (renderStrict) #endif -testGPretty :: (HasCallStack, GPretty a) => String -> Int -> a -> T.Text -> TestTree+testGPretty :: (HasCallStack, GPretty a) => String -> Int -> a -> T.Text -> Test testGPretty n i a s = testCase n $ renderStrict@@ -40,21 +55,21 @@ @=? s propertyGPrettyShow ::- forall proxy a.+ forall a. (HasCallStack, GPretty a, Show a) => String -> Gen a ->- TestTree+ Test propertyGPrettyShow n g = testProperty n $ forAll g $ \(a :: a) -> do renderStrict (layoutPretty (LayoutOptions Unbounded) (gpretty a)) == T.pack (show a) propertyGPrettyRead ::- forall proxy a.+ forall a. (HasCallStack, GPretty a, Read a, Show a, Eq a) => String -> Gen a ->- TestTree+ Test propertyGPrettyRead n g = testProperty n $ \i -> forAll g $ \(a :: a) -> do read@@ -69,11 +84,11 @@ == a propertyGPretty ::- forall proxy a.+ forall a. (HasCallStack, GPretty a, Read a, Show a, Eq a) => String -> Gen a ->- TestTree+ Test propertyGPretty n g = testGroup n@@ -123,7 +138,7 @@ a <- arbitrary Record a <$> arbitrary -gprettyTests :: TestTree+gprettyTests :: Test gprettyTests = testGroup "GPrettyTests"
test/Grisette/IR/SymPrim/Data/Prim/BVTests.hs view
@@ -3,17 +3,28 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} -module Grisette.IR.SymPrim.Data.Prim.BVTests where+module Grisette.IR.SymPrim.Data.Prim.BVTests (bvTests) where -import Data.Proxy-import Grisette.Core.Data.BV+import Data.Proxy (Proxy (Proxy))+import Grisette.Core.Data.BV (IntN, WordN) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( bvconcatTerm,+ bvextendTerm,+ bvselectTerm,+ conTerm,+ ssymTerm,+ )+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term (Term) import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV-import Test.Tasty-import Test.Tasty.HUnit+ ( pevalBVConcatTerm,+ pevalBVExtendTerm,+ pevalBVSelectTerm,+ )+import Test.Framework (Test, testGroup)+import Test.Framework.Providers.HUnit (testCase)+import Test.HUnit ((@=?)) -bvTests :: TestTree+bvTests :: Test bvTests = testGroup "BVTests"
test/Grisette/IR/SymPrim/Data/Prim/BitsTests.hs view
@@ -1,16 +1,33 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE ScopedTypeVariables #-} -module Grisette.IR.SymPrim.Data.Prim.BitsTests where+module Grisette.IR.SymPrim.Data.Prim.BitsTests (bitsTests) where -import Grisette.Core.Data.BV+import Grisette.Core.Data.BV (IntN, WordN) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( andBitsTerm,+ complementBitsTerm,+ conTerm,+ orBitsTerm,+ rotateBitsTerm,+ shiftBitsTerm,+ ssymTerm,+ xorBitsTerm,+ )+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term (Term) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits-import Test.Tasty-import Test.Tasty.HUnit+ ( pevalAndBitsTerm,+ pevalComplementBitsTerm,+ pevalOrBitsTerm,+ pevalRotateBitsTerm,+ pevalShiftBitsTerm,+ pevalXorBitsTerm,+ )+import Test.Framework (Test, testGroup)+import Test.Framework.Providers.HUnit (testCase)+import Test.HUnit ((@=?)) -bitsTests :: TestTree+bitsTests :: Test bitsTests = testGroup "BitsTests"
test/Grisette/IR/SymPrim/Data/Prim/BoolTests.hs view
@@ -2,17 +2,36 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} -module Grisette.IR.SymPrim.Data.Prim.BoolTests where+module Grisette.IR.SymPrim.Data.Prim.BoolTests (boolTests) where -import Grisette.Core.Data.BV+import Grisette.Core.Data.BV (IntN, WordN) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( andTerm,+ conTerm,+ eqvTerm,+ notTerm,+ orTerm,+ ssymTerm,+ )+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term (Term) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool+ ( pevalAndTerm,+ pevalEqvTerm,+ pevalITETerm,+ pevalImplyTerm,+ pevalNotEqvTerm,+ pevalNotTerm,+ pevalOrTerm,+ pevalXorTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num-import Test.Tasty-import Test.Tasty.HUnit+ ( pevalAddNumTerm,+ )+import Test.Framework (Test, testGroup)+import Test.Framework.Providers.HUnit (testCase)+import Test.HUnit ((@=?)) -boolTests :: TestTree+boolTests :: Test boolTests = testGroup "BoolTests"
test/Grisette/IR/SymPrim/Data/Prim/IntegralTests.hs view
@@ -3,18 +3,39 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} -module Grisette.IR.SymPrim.Data.Prim.IntegralTests where+module Grisette.IR.SymPrim.Data.Prim.IntegralTests (integralTests) where -import Control.DeepSeq-import Control.Exception-import Data.Proxy-import Grisette.Core.Data.BV+import Control.DeepSeq (NFData (rnf), force)+import Control.Exception (ArithException, catch, evaluate)+import Data.Proxy (Proxy (Proxy))+import Grisette.Core.Data.BV (IntN (IntN), WordN (WordN)) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( conTerm,+ divBoundedIntegralTerm,+ divIntegralTerm,+ modIntegralTerm,+ quotBoundedIntegralTerm,+ quotIntegralTerm,+ remIntegralTerm,+ ssymTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( SupportedPrim,+ Term,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral-import Test.Tasty-import Test.Tasty.HUnit-import Test.Tasty.QuickCheck+ ( pevalDivBoundedIntegralTerm,+ pevalDivIntegralTerm,+ pevalModIntegralTerm,+ pevalQuotBoundedIntegralTerm,+ pevalQuotIntegralTerm,+ pevalRemIntegralTerm,+ )+import Test.Framework (Test, TestName, testGroup)+import Test.Framework.Providers.HUnit (testCase)+import Test.Framework.Providers.QuickCheck2 (testProperty)+import Test.HUnit ((@=?))+import Test.QuickCheck (Arbitrary, ioProperty) newtype AEWrapper = AEWrapper ArithException deriving (Eq) @@ -34,22 +55,21 @@ (Term t -> Term t -> Term t) -> IO () sameDivPeval i j pf cf consf = do- cx <- evaluate (force $ Right $ cf i j) `catch` \(e :: ArithException) -> return $ Left AEWrapper+ cx <- evaluate (force $ Right $ cf i j) `catch` \(_ :: ArithException) -> return $ Left AEWrapper case cx of- Left f -> pf (conTerm i) (conTerm j) @=? consf (conTerm i) (conTerm j)+ Left _ -> pf (conTerm i) (conTerm j) @=? consf (conTerm i) (conTerm j) Right t -> pf (conTerm i) (conTerm j) @=? conTerm t divisionPevalBoundedTests ::- forall p t0 t.- (Num t, Eq t, Arbitrary t0, Show t0, Bounded t, SupportedPrim t, Integral t) =>+ forall p t.+ (Num t, Eq t, Bounded t, SupportedPrim t, Integral t) => p t -> TestName ->- (t0 -> t) -> (Term t -> Term t -> Term t) -> (t -> t -> t) -> (Term t -> Term t -> Term t) ->- TestTree-divisionPevalBoundedTests _ name transform pf cf consf =+ Test+divisionPevalBoundedTests _ name pf cf consf = testGroup name [ testCase "On concrete min divide by -1" $@@ -65,8 +85,8 @@ (Term t -> Term t -> Term t) -> (t -> t -> t) -> (Term t -> Term t -> Term t) ->- TestTree-divisionPevalTests p name transform pf cf consf =+ Test+divisionPevalTests _ name transform pf cf consf = testGroup name [ testProperty "On concrete prop" $@@ -90,12 +110,12 @@ (forall t. (SupportedPrim t, Bounded t, Integral t) => Term t -> Term t -> Term t) -> (forall t. (Bounded t, Integral t) => t -> t -> t) -> (forall t. (SupportedPrim t, Bounded t, Integral t) => Term t -> Term t -> Term t) ->- TestTree+ Test divisionPevalBoundedTestGroup name pf cf consf = testGroup name [ divisionPevalTests (Proxy @(IntN 4)) "IntN" IntN pf cf consf,- divisionPevalBoundedTests (Proxy @(IntN 4)) "IntN Bounded" IntN pf cf consf+ divisionPevalBoundedTests (Proxy @(IntN 4)) "IntN Bounded" pf cf consf ] divisionPevalUnboundedTestGroup ::@@ -103,13 +123,13 @@ (forall t. (SupportedPrim t, Integral t) => Term t -> Term t -> Term t) -> (forall t. (Integral t) => t -> t -> t) -> (forall t. (SupportedPrim t, Integral t) => Term t -> Term t -> Term t) ->- TestTree+ Test divisionPevalUnboundedTestGroup name pf cf consf = testGroup name [ divisionPevalTests (Proxy @Integer) "Integer" id pf cf consf, divisionPevalTests (Proxy @(WordN 4)) "WordN" WordN pf cf consf,- divisionPevalBoundedTests (Proxy @(WordN 4)) "WordN Bounded" WordN pf cf consf+ divisionPevalBoundedTests (Proxy @(WordN 4)) "WordN Bounded" pf cf consf ] moduloPevalTests ::@@ -121,8 +141,8 @@ (Term t -> Term t -> Term t) -> (t -> t -> t) -> (Term t -> Term t -> Term t) ->- TestTree-moduloPevalTests p name transform pf cf consf =+ Test+moduloPevalTests _ name transform pf cf consf = testGroup name [ testProperty "On concrete" $@@ -148,7 +168,7 @@ (forall t. (SupportedPrim t, Integral t) => Term t -> Term t -> Term t) -> (forall t. (Integral t) => t -> t -> t) -> (forall t. (SupportedPrim t, Integral t) => Term t -> Term t -> Term t) ->- TestTree+ Test moduloPevalTestGroup name pf cf consf = testGroup name@@ -157,7 +177,7 @@ moduloPevalTests (Proxy @(WordN 4)) "WordN" WordN pf cf consf ] -integralTests :: TestTree+integralTests :: Test integralTests = testGroup "IntegralTests"
test/Grisette/IR/SymPrim/Data/Prim/ModelTests.hs view
@@ -1,23 +1,53 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE ScopedTypeVariables #-} -module Grisette.IR.SymPrim.Data.Prim.ModelTests where+module Grisette.IR.SymPrim.Data.Prim.ModelTests (modelTests) where -import Data.HashMap.Strict as M+import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S-import Grisette.Core.Data.BV+import Grisette.Core.Data.BV (IntN, WordN) import Grisette.Core.Data.Class.ModelOps+ ( ModelOps+ ( emptyModel,+ exact,+ exceptFor,+ extendTo,+ insertValue,+ restrictTo,+ valueOf+ ),+ ModelRep (buildModel),+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( conTerm,+ ssymTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term-import Grisette.IR.SymPrim.Data.Prim.Model as Model-import Grisette.IR.SymPrim.Data.Prim.ModelValue+ ( Term,+ TypedSymbol (SimpleSymbol),+ someTypedSymbol,+ )+import Grisette.IR.SymPrim.Data.Prim.Model+ ( Model (Model),+ ModelValuePair ((::=)),+ SymbolSet (SymbolSet),+ equation,+ evaluateTerm,+ )+import Grisette.IR.SymPrim.Data.Prim.ModelValue (toModelValue) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool+ ( pevalEqvTerm,+ pevalITETerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num-import Test.Tasty-import Test.Tasty.HUnit-import Type.Reflection+ ( pevalAddNumTerm,+ pevalUMinusNumTerm,+ )+import Test.Framework (Test, testGroup)+import Test.Framework.Providers.HUnit (testCase)+import Test.HUnit ((@=?)) -modelTests :: TestTree+modelTests :: Test modelTests = let asymbol :: TypedSymbol Integer = SimpleSymbol "a" bsymbol :: TypedSymbol Bool = SimpleSymbol "b"
test/Grisette/IR/SymPrim/Data/Prim/NumTests.hs view
@@ -1,17 +1,41 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE ScopedTypeVariables #-} -module Grisette.IR.SymPrim.Data.Prim.NumTests where+module Grisette.IR.SymPrim.Data.Prim.NumTests (numTests) where -import Grisette.Core.Data.BV+import Grisette.Core.Data.BV (IntN, WordN) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( absNumTerm,+ addNumTerm,+ conTerm,+ leNumTerm,+ ltNumTerm,+ signumNumTerm,+ ssymTerm,+ timesNumTerm,+ uminusNumTerm,+ )+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term (Term) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool+ ( pevalITETerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num-import Test.Tasty-import Test.Tasty.HUnit+ ( pevalAbsNumTerm,+ pevalAddNumTerm,+ pevalGeNumTerm,+ pevalGtNumTerm,+ pevalLeNumTerm,+ pevalLtNumTerm,+ pevalMinusNumTerm,+ pevalSignumNumTerm,+ pevalTimesNumTerm,+ pevalUMinusNumTerm,+ )+import Test.Framework (Test, testGroup)+import Test.Framework.Providers.HUnit (testCase)+import Test.HUnit ((@=?)) -numTests :: TestTree+numTests :: Test numTests = testGroup "NumTests"
test/Grisette/IR/SymPrim/Data/Prim/TabularFunTests.hs view
@@ -1,17 +1,29 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} -module Grisette.IR.SymPrim.Data.Prim.TabularFunTests where+module Grisette.IR.SymPrim.Data.Prim.TabularFunTests (tabularFunTests) where import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( conTerm,+ ssymTerm,+ tabularFunApplyTerm,+ )+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term (Term) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool+ ( pevalEqvTerm,+ pevalITETerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun+ ( pevalTabularFunApplyTerm,+ ) import Grisette.IR.SymPrim.Data.TabularFun-import Test.Tasty-import Test.Tasty.HUnit+ ( type (=->) (TabularFun),+ )+import Test.Framework (Test, testGroup)+import Test.Framework.Providers.HUnit (testCase)+import Test.HUnit ((@=?)) -tabularFunTests :: TestTree+tabularFunTests :: Test tabularFunTests = testGroup "TabularFunTests"
test/Grisette/IR/SymPrim/Data/SymPrimTests.hs view
@@ -2,54 +2,198 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE NegativeLiterals #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} -module Grisette.IR.SymPrim.Data.SymPrimTests where+module Grisette.IR.SymPrim.Data.SymPrimTests (symPrimTests) where -import Control.DeepSeq+import Control.DeepSeq (NFData (rnf), force) import Control.Exception-import Control.Monad.Except+ ( ArithException (DivideByZero, Overflow, Underflow),+ catch,+ evaluate,+ )+import Control.Monad.Except (ExceptT, MonadError (throwError)) import Data.Bits+ ( Bits+ ( bit,+ bitSizeMaybe,+ complement,+ isSigned,+ popCount,+ rotate,+ shift,+ testBit,+ xor,+ (.&.),+ (.|.)+ ),+ ) import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S-import Data.Int-import Data.Proxy-import Data.Word-import Grisette.Core.Control.Monad.UnionM-import Grisette.Core.Data.BV+import Data.Int (Int8)+import Data.Proxy (Proxy (Proxy))+import Data.Word (Word8)+import Grisette.Core.Control.Monad.UnionM (UnionM)+import Grisette.Core.Data.BV (IntN (IntN), WordN (WordN)) import Grisette.Core.Data.Class.BitVector+ ( SizedBV+ ( sizedBVConcat,+ sizedBVExt,+ sizedBVSelect,+ sizedBVSext,+ sizedBVZext+ ),+ ) import Grisette.Core.Data.Class.Bool+ ( ITEOp (ites),+ LogicalOp (implies, nots, xors, (&&~), (||~)),+ SEq ((/=~), (==~)),+ ) import Grisette.Core.Data.Class.Evaluate+ ( EvaluateSym (evaluateSym),+ ) import Grisette.Core.Data.Class.ExtractSymbolics-import Grisette.Core.Data.Class.Function+ ( ExtractSymbolics (extractSymbolics),+ )+import Grisette.Core.Data.Class.Function (Function ((#))) import Grisette.Core.Data.Class.GenSym+ ( genSym,+ genSymSimple,+ nameWithInfo,+ ) import Grisette.Core.Data.Class.Mergeable+ ( Mergeable (rootStrategy),+ MergingStrategy (SimpleStrategy),+ ) import Grisette.Core.Data.Class.ModelOps+ ( ModelOps (emptyModel, insertValue),+ ModelRep (buildModel),+ ) import Grisette.Core.Data.Class.SOrd+ ( SOrd (symCompare, (<=~), (<~), (>=~), (>~)),+ ) import Grisette.Core.Data.Class.SafeArith+ ( SafeDivision+ ( safeDiv,+ safeDiv',+ safeDivMod,+ safeDivMod',+ safeMod,+ safeMod',+ safeQuot,+ safeQuot',+ safeQuotRem,+ safeQuotRem',+ safeRem,+ safeRem'+ ),+ SafeLinearArith+ ( safeAdd,+ safeAdd',+ safeMinus,+ safeMinus',+ safeNeg,+ safeNeg'+ ),+ ) import Grisette.Core.Data.Class.SimpleMergeable+ ( SimpleMergeable (mrgIte),+ merge,+ mrgIf,+ mrgSingle,+ ) import Grisette.Core.Data.Class.Solvable-import Grisette.Core.Data.Class.ToCon-import Grisette.Core.Data.Class.ToSym+ ( Solvable (con, conView, iinfosym, isym, ssym),+ pattern Con,+ )+import Grisette.Core.Data.Class.ToCon (ToCon (toCon))+import Grisette.Core.Data.Class.ToSym (ToSym (toSym)) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors+ ( conTerm,+ isymTerm,+ ssymTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+ ( LinkedRep (wrapTerm),+ Term,+ TypedSymbol (SimpleSymbol),+ someTypedSymbol,+ type (-->),+ ) import Grisette.IR.SymPrim.Data.Prim.Model-import Grisette.IR.SymPrim.Data.Prim.ModelValue+ ( Model (Model),+ SymbolSet (SymbolSet),+ )+import Grisette.IR.SymPrim.Data.Prim.ModelValue (toModelValue) import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV+ ( pevalBVConcatTerm,+ pevalBVExtendTerm,+ pevalBVSelectTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits+ ( pevalAndBitsTerm,+ pevalComplementBitsTerm,+ pevalOrBitsTerm,+ pevalRotateBitsTerm,+ pevalShiftBitsTerm,+ pevalXorBitsTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool+ ( pevalAndTerm,+ pevalEqvTerm,+ pevalITETerm,+ pevalImplyTerm,+ pevalNotTerm,+ pevalOrTerm,+ pevalXorTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral+ ( pevalDivBoundedIntegralTerm,+ pevalDivIntegralTerm,+ pevalModBoundedIntegralTerm,+ pevalModIntegralTerm,+ pevalQuotBoundedIntegralTerm,+ pevalQuotIntegralTerm,+ pevalRemBoundedIntegralTerm,+ pevalRemIntegralTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num+ ( pevalAbsNumTerm,+ pevalAddNumTerm,+ pevalGeNumTerm,+ pevalGtNumTerm,+ pevalLeNumTerm,+ pevalLtNumTerm,+ pevalMinusNumTerm,+ pevalSignumNumTerm,+ pevalTimesNumTerm,+ pevalUMinusNumTerm,+ ) import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun+ ( pevalTabularFunApplyTerm,+ ) import Grisette.IR.SymPrim.Data.SymPrim-import Grisette.IR.SymPrim.Data.TabularFun-import Test.Tasty-import Test.Tasty.HUnit-import Test.Tasty.QuickCheck hiding ((.&.))-import Type.Reflection hiding (Con)+ ( ModelSymPair ((:=)),+ SymBool (SymBool),+ SymIntN (SymIntN),+ SymInteger (SymInteger),+ SymWordN (SymWordN),+ symSize,+ symsSize,+ (-->),+ type (-~>),+ type (=~>),+ )+import Grisette.IR.SymPrim.Data.TabularFun (type (=->))+import Test.Framework (Test, TestName, testGroup)+import Test.Framework.Providers.HUnit (testCase)+import Test.Framework.Providers.QuickCheck2 (testProperty)+import Test.HUnit (Assertion, assertFailure, (@=?))+import Test.QuickCheck (Arbitrary, ioProperty) newtype AEWrapper = AEWrapper ArithException deriving (Eq) @@ -96,7 +240,7 @@ (c -> c -> c) -> Assertion sameSafeDiv' i j f cf = do- xc <- evaluate (force $ Right $ cf i j) `catch` \(e :: ArithException) -> return $ Left ()+ xc <- evaluate (force $ Right $ cf i j) `catch` \(_ :: ArithException) -> return $ Left () case xc of Left () -> f (const ()) (con i :: s) (con j) @=? merge (throwError ()) Right c -> f (const ()) (con i :: s) (con j) @=? mrgSingle (con c)@@ -138,7 +282,7 @@ (c -> c -> (c, c)) -> Assertion sameSafeDivMod' i j f cf = do- xc <- evaluate (force $ Right $ cf i j) `catch` \(e :: ArithException) -> return $ Left ()+ xc <- evaluate (force $ Right $ cf i j) `catch` \(_ :: ArithException) -> return $ Left () case xc of Left () -> f (const ()) (con i :: s) (con j) @=? merge (throwError ()) Right (c1, c2) -> f (const ()) (con i :: s) (con j) @=? mrgSingle (con c1, con c2)@@ -150,7 +294,7 @@ ((ArithException -> ()) -> s -> s -> ExceptT () UnionM s) -> (c -> c -> c) -> (Term c -> Term c -> Term c) ->- [TestTree]+ [Test] safeDivisionBoundedOnlyTests f f' cf pf = [ testCase "on concrete min divided by minus one" $ do sameSafeDiv minBound (-1) f cf@@ -185,10 +329,9 @@ (LinkedRep c s, Solvable c s, Eq s, Num c, Show s, Mergeable s, SEq s) => (s -> s -> ExceptT ArithException UnionM s) -> ((ArithException -> ()) -> s -> s -> ExceptT () UnionM s) ->- (c -> c -> c) -> (Term c -> Term c -> Term c) ->- [TestTree]-safeDivisionUnboundedOnlyTests f f' cf pf =+ [Test]+safeDivisionUnboundedOnlyTests f f' pf = [ testCase "on symbolic" $ do f (ssym "a" :: s) (ssym "b") @=? ( mrgIf@@ -213,9 +356,8 @@ (s -> s -> ExceptT ArithException UnionM s) -> ((ArithException -> ()) -> s -> s -> ExceptT () UnionM s) -> (c -> c -> c) ->- (Term c -> Term c -> Term c) ->- [TestTree]-safeDivisionGeneralTests transform f f' cf pf =+ [Test]+safeDivisionGeneralTests transform f f' cf = [ testProperty "on concrete prop" $ \(i0 :: c0, j0 :: c0) -> ioProperty $ do let i = transform i0@@ -243,10 +385,10 @@ ((ArithException -> ()) -> s -> s -> ExceptT () UnionM s) -> (c -> c -> c) -> (Term c -> Term c -> Term c) ->- TestTree+ Test safeDivisionBoundedTests name transform f f' cf pf = testGroup name $- safeDivisionGeneralTests transform f f' cf pf+ safeDivisionGeneralTests transform f f' cf ++ safeDivisionBoundedOnlyTests f f' cf pf safeDivisionUnboundedTests ::@@ -258,11 +400,11 @@ ((ArithException -> ()) -> s -> s -> ExceptT () UnionM s) -> (c -> c -> c) -> (Term c -> Term c -> Term c) ->- TestTree+ Test safeDivisionUnboundedTests name transform f f' cf pf = testGroup name $- safeDivisionGeneralTests transform f f' cf pf- ++ safeDivisionUnboundedOnlyTests f f' cf pf+ safeDivisionGeneralTests transform f f' cf+ ++ safeDivisionUnboundedOnlyTests f f' pf safeDivModBoundedOnlyTests :: forall c s.@@ -279,7 +421,7 @@ (c -> c -> (c, c)) -> (Term c -> Term c -> Term c) -> (Term c -> Term c -> Term c) ->- [TestTree]+ [Test] safeDivModBoundedOnlyTests f f' cf pf1 pf2 = [ testCase "on concrete min divided by minus one" $ do sameSafeDivMod minBound (-1) f cf@@ -329,11 +471,10 @@ s -> ExceptT () UnionM (s, s) ) ->- (c -> c -> (c, c)) -> (Term c -> Term c -> Term c) -> (Term c -> Term c -> Term c) ->- [TestTree]-safeDivModUnboundedOnlyTests f f' cf pf1 pf2 =+ [Test]+safeDivModUnboundedOnlyTests f f' pf1 pf2 = [ testCase "on symbolic" $ do f (ssym "a" :: s) (ssym "b") @=? ( mrgIf@@ -373,10 +514,8 @@ ExceptT () UnionM (s, s) ) -> (c -> c -> (c, c)) ->- (Term c -> Term c -> Term c) ->- (Term c -> Term c -> Term c) ->- [TestTree]-safeDivModGeneralTests transform f f' cf pf1 pf2 =+ [Test]+safeDivModGeneralTests transform f f' cf = [ testProperty "on concrete" $ \(i0 :: c0, j0 :: c0) -> ioProperty $ do let i = transform i0@@ -412,10 +551,10 @@ (c -> c -> (c, c)) -> (Term c -> Term c -> Term c) -> (Term c -> Term c -> Term c) ->- TestTree+ Test safeDivModBoundedTests name transform f f' cf pf1 pf2 = testGroup name $- safeDivModGeneralTests transform f f' cf pf1 pf2+ safeDivModGeneralTests transform f f' cf ++ safeDivModBoundedOnlyTests f f' cf pf1 pf2 safeDivModUnboundedTests ::@@ -435,13 +574,13 @@ (c -> c -> (c, c)) -> (Term c -> Term c -> Term c) -> (Term c -> Term c -> Term c) ->- TestTree+ Test safeDivModUnboundedTests name transform f f' cf pf1 pf2 = testGroup name $- safeDivModGeneralTests transform f f' cf pf1 pf2- ++ safeDivModUnboundedOnlyTests f f' cf pf1 pf2+ safeDivModGeneralTests transform f f' cf+ ++ safeDivModUnboundedOnlyTests f f' pf1 pf2 -symPrimTests :: TestTree+symPrimTests :: Test symPrimTests = testGroup "SymPrimTests"@@ -919,14 +1058,6 @@ fsymbol :: TypedSymbol (IntN 4) = "f" gsymbol :: TypedSymbol (WordN 16) = "g" hsymbol :: TypedSymbol (IntN 16) = "h"- a :: SymInteger = ssym "a"- b :: SymBool = "b"- c :: SymInteger = "c"- d :: SymBool = "d"- e :: SymWordN 4 = "e"- f :: SymIntN 4 = "f"- g :: SymWordN 16 = "g"- h :: SymIntN 16 = "h" va :: Integer = 1 vc :: Integer = 2 ve :: WordN 4 = 3
test/Grisette/IR/SymPrim/Data/TabularFunTests.hs view
@@ -1,14 +1,17 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} -module Grisette.IR.SymPrim.Data.TabularFunTests where+module Grisette.IR.SymPrim.Data.TabularFunTests (tabularFunTests) where -import Grisette.Core.Data.Class.Function+import Grisette.Core.Data.Class.Function (Function ((#))) import Grisette.IR.SymPrim.Data.TabularFun-import Test.Tasty-import Test.Tasty.HUnit+ ( type (=->) (TabularFun),+ )+import Test.Framework (Test, testGroup)+import Test.Framework.Providers.HUnit (testCase)+import Test.HUnit ((@=?)) -tabularFunTests :: TestTree+tabularFunTests :: Test tabularFunTests = testGroup "TabularFunTests"
test/Main.hs view
@@ -1,4 +1,4 @@-module Main where+module Main (main) where {- import Grisette.Core.Control.ExceptionTests@@ -22,39 +22,38 @@ import Grisette.Lib.Data.TraversableTests -} -import Grisette.Backend.SBV.Data.SMT.CEGISTests+import Grisette.Backend.SBV.Data.SMT.CEGISTests (cegisTests) import Grisette.Backend.SBV.Data.SMT.LoweringTests+ ( loweringTests,+ ) import Grisette.Backend.SBV.Data.SMT.TermRewritingTests-import Grisette.Core.Control.Monad.UnionMTests+ ( termRewritingTests,+ )+import Grisette.Core.Control.Monad.UnionMTests (unionMTests) import qualified Grisette.Core.Data.BVTests-import Grisette.Core.Data.Class.GPrettyTests+import Grisette.Core.Data.Class.GPrettyTests (gprettyTests) import qualified Grisette.IR.SymPrim.Data.Prim.BVTests-import Grisette.IR.SymPrim.Data.Prim.BitsTests-import Grisette.IR.SymPrim.Data.Prim.BoolTests+import Grisette.IR.SymPrim.Data.Prim.BitsTests (bitsTests)+import Grisette.IR.SymPrim.Data.Prim.BoolTests (boolTests) import Grisette.IR.SymPrim.Data.Prim.IntegralTests-import Grisette.IR.SymPrim.Data.Prim.ModelTests-import Grisette.IR.SymPrim.Data.Prim.NumTests+ ( integralTests,+ )+import Grisette.IR.SymPrim.Data.Prim.ModelTests (modelTests)+import Grisette.IR.SymPrim.Data.Prim.NumTests (numTests) import qualified Grisette.IR.SymPrim.Data.Prim.TabularFunTests-import Grisette.IR.SymPrim.Data.SymPrimTests+import Grisette.IR.SymPrim.Data.SymPrimTests (symPrimTests) import qualified Grisette.IR.SymPrim.Data.TabularFunTests-import Test.Tasty-import Test.Tasty.Ingredients-import qualified Test.Tasty.Ingredients.ConsoleReporter as ConsoleReporter-import qualified Test.Tasty.Runners.Reporter as Reporter+import Test.Framework (Test, defaultMain, testGroup) main :: IO ()-main = defaultMainWithIngredients [composeReporters Reporter.ingredient ConsoleReporter.consoleTestReporter] tests--tests :: TestTree-tests =- testGroup- "grisette"+main =+ defaultMain [ coreTests, irTests, sbvTests ] -coreTests :: TestTree+coreTests :: Test coreTests = testGroup "core"@@ -71,7 +70,7 @@ ] {--coreTests :: TestTree+coreTests :: Test coreTests = testGroup "grisette-core"@@ -127,7 +126,7 @@ ] -} -irTests :: TestTree+irTests :: Test irTests = testGroup "grisette-symir"@@ -148,7 +147,7 @@ ] ] -sbvTests :: TestTree+sbvTests :: Test sbvTests = testGroup "Grisette.Backend.SBV.Data.SMT"