diff --git a/hie.yaml b/hie.yaml index 1db43fe193d..a7c123cbd9e 100644 --- a/hie.yaml +++ b/hie.yaml @@ -255,6 +255,9 @@ cradle: - path: "libs/constrained-generators/bench/Main.hs" component: "constrained-generators:bench:bench" + - path: "libs/constrained-generators/bench/Constrained/Bench.hs" + component: "constrained-generators:bench:bench" + - path: "libs/ledger-state/src" component: "lib:ledger-state" diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs index b82cbae363a..3ce1e227d08 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs @@ -19,7 +19,7 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Core ( import Cardano.Ledger.BaseTypes (Inject, ShelleyBase) import Cardano.Ledger.Core (EraRule) import qualified Constrained as CV2 -import Constrained.Base (Spec (..)) +import Constrained.Base (Specification (..)) import Control.State.Transition.Extended (STS (..)) import Data.Bifunctor (Bifunctor (..)) import Data.Bitraversable (bimapM) @@ -73,21 +73,21 @@ class type ExecContext fn rule era = () environmentSpec :: - CV2.Spec fn (Environment (EraRule rule era)) + CV2.Specification fn (Environment (EraRule rule era)) stateSpec :: Environment (EraRule rule era) -> - CV2.Spec fn (State (EraRule rule era)) + CV2.Specification fn (State (EraRule rule era)) signalSpec :: Environment (EraRule rule era) -> State (EraRule rule era) -> - CV2.Spec fn (Signal (EraRule rule era)) + CV2.Specification fn (Signal (EraRule rule era)) - execContextSpec :: CV2.Spec fn (ExecContext fn rule era) + execContextSpec :: CV2.Specification fn (ExecContext fn rule era) default execContextSpec :: ExecContext fn rule era ~ () => - CV2.Spec fn (ExecContext fn rule era) + CV2.Specification fn (ExecContext fn rule era) execContextSpec = TrueSpec runAgdaRule :: diff --git a/libs/cardano-ledger-test/bench/Bench/Constrained/STS.hs b/libs/cardano-ledger-test/bench/Bench/Constrained/STS.hs index a19b7b31af7..4f9d180fd9f 100644 --- a/libs/cardano-ledger-test/bench/Bench/Constrained/STS.hs +++ b/libs/cardano-ledger-test/bench/Bench/Constrained/STS.hs @@ -12,14 +12,14 @@ import Cardano.Ledger.Conway import Cardano.Ledger.Conway.Rules import Cardano.Ledger.Crypto import Constrained -import Constrained.Bench +import Control.DeepSeq import Criterion import Test.Cardano.Ledger.Constrained.Conway govEnv :: GovEnv (ConwayEra StandardCrypto) govEnv = genFromSpecWithSeed 10 30 (govEnvSpec @ConwayFn) -singleProposalTreeSpec :: Spec ConwayFn ProposalTree +singleProposalTreeSpec :: Specification ConwayFn ProposalTree singleProposalTreeSpec = constrained $ \ppupTree -> [ wellFormedChildren (lit SNothing) ppupTree , allGASInTree ppupTree $ \gas -> @@ -38,3 +38,8 @@ stsBenchmarks = ] where govPropSpec = govProposalsSpec @ConwayFn govEnv + +benchSpec :: (HasSpec fn a, NFData a) => Int -> Int -> String -> Specification fn a -> Benchmark +benchSpec seed size nm spec = + bench (unlines [nm, show (genFromSpecWithSeed seed size spec)]) $ + nf (genFromSpecWithSeed seed size) spec diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs index 355808835e4..96832fcbd1c 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs @@ -22,7 +22,7 @@ import Test.Cardano.Ledger.Constrained.Conway.Pool certEnvSpec :: IsConwayUniv fn => - Spec fn (CertEnv (ConwayEra StandardCrypto)) + Specification fn (CertEnv (ConwayEra StandardCrypto)) certEnvSpec = constrained $ \ce -> match ce $ \_ pp _ -> @@ -30,7 +30,7 @@ certEnvSpec = certStateSpec :: IsConwayUniv fn => - Spec fn (CertState (ConwayEra StandardCrypto)) + Specification fn (CertState (ConwayEra StandardCrypto)) certStateSpec = constrained $ \cs -> match cs $ \vState pState dState -> @@ -43,7 +43,7 @@ txCertSpec :: IsConwayUniv fn => CertEnv (ConwayEra StandardCrypto) -> CertState (ConwayEra StandardCrypto) -> - Spec fn (ConwayTxCert (ConwayEra StandardCrypto)) + Specification fn (ConwayTxCert (ConwayEra StandardCrypto)) txCertSpec (CertEnv slot pp ce) CertState {..} = constrained $ \txCert -> caseOn diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs index 4d50906e5a5..27de6721519 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs @@ -21,7 +21,7 @@ import Test.Cardano.Ledger.Constrained.Conway.Instances dStateSpec :: IsConwayUniv fn => - Spec fn (DState (ConwayEra StandardCrypto)) + Specification fn (DState (ConwayEra StandardCrypto)) dStateSpec = constrained $ \ds -> match ds $ \rewardMap _futureGenDelegs _genDelegs _rewards -> match rewardMap $ \rdMap ptrMap sPoolMap _dRepMap -> @@ -33,7 +33,7 @@ delegCertSpec :: IsConwayUniv fn => PParams (ConwayEra StandardCrypto) -> DState (ConwayEra StandardCrypto) -> - Spec fn (ConwayDelegCert StandardCrypto) + Specification fn (ConwayDelegCert StandardCrypto) delegCertSpec pp ds = let rewardMap = unUnify $ rewards ds delegMap = unUnify $ delegations ds diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs index 9a8d3defc64..9181e2fd34d 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs @@ -31,7 +31,7 @@ import Test.Cardano.Ledger.Constrained.Conway.PParams govEnvSpec :: IsConwayUniv fn => - Spec fn (GovEnv (ConwayEra StandardCrypto)) + Specification fn (GovEnv (ConwayEra StandardCrypto)) govEnvSpec = constrained $ \ge -> match ge $ \_ _ pp _ _ _ -> satisfies pp pparamsSpec @@ -42,7 +42,7 @@ govEnvSpec = constrained $ \ge -> govProposalsSpec :: IsConwayUniv fn => GovEnv (ConwayEra StandardCrypto) -> - Spec fn (Proposals (ConwayEra StandardCrypto)) + Specification fn (Proposals (ConwayEra StandardCrypto)) govProposalsSpec GovEnv {geEpoch, gePPolicy, gePrevGovActionIds} = constrained $ \props -> match props $ \ppupTree hardForkTree committeeTree constitutionTree unorderedProposals -> @@ -154,7 +154,7 @@ allGASAndChildInTree t k = forAll (snd_ t) $ \t' -> forAll' t' $ \gas cs -> forAll cs $ \t'' -> - k gas (roseRoot_ t'') + k gas (rootLabel_ t'') wellFormedChildren :: IsConwayUniv fn => @@ -166,11 +166,11 @@ wellFormedChildren root rootAndTrees = [ assert $ root ==. root' -- The root matches the root given in the environment , forAll trees $ \t -> [ -- Every node just below the root has the root as its parent - withPrevActId (roseRoot_ t) (assert . (==. root)) + withPrevActId (rootLabel_ t) (assert . (==. root)) , -- Every node's children have the id of the node as its parent forAll' t $ \gas children -> [ forAll children $ \t' -> - [ withPrevActId (roseRoot_ t') (assert . (==. cSJust_ (gasId_ gas))) + [ withPrevActId (rootLabel_ t') (assert . (==. cSJust_ (gasId_ gas))) -- TODO: figure out why this causes a crash! -- , t' `dependsOn` gas ] @@ -245,7 +245,7 @@ govProceduresSpec :: IsConwayUniv fn => GovEnv (ConwayEra StandardCrypto) -> Proposals (ConwayEra StandardCrypto) -> - Spec fn (GovProcedures (ConwayEra StandardCrypto)) + Specification fn (GovProcedures (ConwayEra StandardCrypto)) govProceduresSpec ge@GovEnv {..} ps = let actions f = [ gid diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs index 95195e8bd6e..e30e72c0ab1 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/GovCert.hs @@ -19,14 +19,14 @@ import Cardano.Ledger.Crypto (StandardCrypto) import Test.Cardano.Ledger.Constrained.Conway.Instances import Test.Cardano.Ledger.Constrained.Conway.PParams -vStateSpec :: Spec fn (VState (ConwayEra StandardCrypto)) +vStateSpec :: Specification fn (VState (ConwayEra StandardCrypto)) vStateSpec = TrueSpec govCertSpec :: IsConwayUniv fn => ConwayGovCertEnv (ConwayEra StandardCrypto) -> VState (ConwayEra StandardCrypto) -> - Spec fn (ConwayGovCert StandardCrypto) + Specification fn (ConwayGovCert StandardCrypto) govCertSpec ConwayGovCertEnv {..} vs = let reps = lit $ Map.keysSet $ vsDReps vs deposits = lit [(k, drepDeposit dep) | (k, dep) <- Map.toList $ vsDReps vs] @@ -54,7 +54,7 @@ govCertSpec ConwayGovCertEnv {..} vs = govCertEnvSpec :: IsConwayUniv fn => - Spec fn (ConwayGovCertEnv (ConwayEra StandardCrypto)) + Specification fn (ConwayGovCertEnv (ConwayEra StandardCrypto)) govCertEnvSpec = constrained $ \gce -> match gce $ \pp _ -> diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs index bc157f2ddc7..9a0cf79bf28 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs @@ -62,6 +62,7 @@ import Cardano.Ledger.Allegra.Scripts import Cardano.Ledger.Alonzo.PParams import Cardano.Ledger.Alonzo.Scripts (AlonzoScript (..)) import Cardano.Ledger.Alonzo.Tx +import Cardano.Ledger.Alonzo.TxAuxData (AlonzoTxAuxData (..), AuxiliaryDataHash) import Cardano.Ledger.Alonzo.TxOut import Cardano.Ledger.Alonzo.TxWits import Cardano.Ledger.Babbage.TxBody (BabbageTxOut (..)) @@ -70,6 +71,7 @@ import Cardano.Ledger.Binary (Sized (..)) import Cardano.Ledger.CertState import Cardano.Ledger.Coin import Cardano.Ledger.Compactible +import Cardano.Ledger.Conway (ConwayEra) import Cardano.Ledger.Conway.Core import Cardano.Ledger.Conway.Governance import Cardano.Ledger.Conway.PParams @@ -78,6 +80,7 @@ import Cardano.Ledger.Conway.Scripts () import Cardano.Ledger.Conway.TxBody import Cardano.Ledger.Conway.TxCert import Cardano.Ledger.Credential +import Cardano.Ledger.Crypto (Crypto, StandardCrypto) import Cardano.Ledger.EpochBoundary import Cardano.Ledger.HKD import Cardano.Ledger.Keys ( @@ -100,10 +103,13 @@ import Cardano.Ledger.SafeHash import Cardano.Ledger.Shelley.LedgerState hiding (ptrMap) import Cardano.Ledger.Shelley.PoolRank import Cardano.Ledger.Shelley.Rules +import Cardano.Ledger.Shelley.TxAuxData (Metadatum) import Cardano.Ledger.TxIn (TxId (..), TxIn (..)) import Cardano.Ledger.UMap import Cardano.Ledger.UTxO import Cardano.Ledger.Val (Val) +import Constrained hiding (Value) +import Constrained qualified as C import Control.Monad.Trans.Fail.String import Crypto.Hash (Blake2b_224) import Data.ByteString qualified as BS @@ -137,14 +143,7 @@ import Test.Cardano.Ledger.Alonzo.Arbitrary () import Test.Cardano.Ledger.Core.Utils import Test.QuickCheck hiding (Args, Fun, forAll) -import Cardano.Ledger.Alonzo.TxAuxData (AlonzoTxAuxData (..), AuxiliaryDataHash) -import Cardano.Ledger.Conway (ConwayEra) -import Cardano.Ledger.Crypto (Crypto, StandardCrypto) -import Cardano.Ledger.Shelley.TxAuxData (Metadatum) -import Constrained hiding (Value) -import Constrained qualified as C - -type ConwayUnivFns = StringFn : RoseTreeFn : BaseFns +type ConwayUnivFns = StringFn : TreeFn : BaseFns type ConwayFn = Fix (OneofL ConwayUnivFns) type IsConwayUniv fn = @@ -152,7 +151,7 @@ type IsConwayUniv fn = , Member (StringFn fn) fn , Member (MapFn fn) fn , Member (FunFn fn) fn - , Member (RoseTreeFn fn) fn + , Member (TreeFn fn) fn ) -- TxBody HasSpec instance ------------------------------------------------ @@ -399,7 +398,7 @@ However, when you do that some questions arise: Sum and Prod things (with some global index of sizes: `TypeRep -> Int`). Potentially you could solve this by having size constraints in the language. There the question is how you design those constraints - their semantics could be `const True` while still -changing the `Spec` - thus giving you the ability to provide a generation time hint! +changing the `Specification` - thus giving you the ability to provide a generation time hint! Solving (1) is more tricky however. The best guess I have is that you would need to push any constraint you have into functions `MyConstraint :: MyUniv fn '[Timelock era] Bool` @@ -599,7 +598,7 @@ instance IsConwayUniv fn => HasSpec fn Text where conformsTo _ _ = True toPreds _ _ = toPred True -data StringSpec fn = StringSpec {strSpecLen :: Spec fn Int} +data StringSpec fn = StringSpec {strSpecLen :: Specification fn Int} deriving instance IsConwayUniv fn => Show (StringSpec fn) @@ -682,8 +681,8 @@ instance IsConwayUniv fn => Functions (StringFn fn) fn where (_ :: StringFn fn '[s] Int) -> getLengthSpec @s ss class StringLike s where - lengthSpec :: IsConwayUniv fn => Spec fn Int -> TypeSpec fn s - getLengthSpec :: TypeSpec fn s -> Spec fn Int + lengthSpec :: IsConwayUniv fn => Specification fn Int -> TypeSpec fn s + getLengthSpec :: TypeSpec fn s -> Specification fn Int getLength :: s -> Int instance HasSimpleRep (Delegatee c) @@ -1020,7 +1019,7 @@ gasProposalProcedure_ :: gasProposalProcedure_ = sel @4 type GAS = GovActionState (ConwayEra StandardCrypto) -type ProposalTree = (StrictMaybe (GovActionId StandardCrypto), [RoseTree GAS]) +type ProposalTree = (StrictMaybe (GovActionId StandardCrypto), [Tree GAS]) type ProposalsType = '[ ProposalTree -- PParamUpdate , ProposalTree -- HardFork @@ -1059,8 +1058,8 @@ instance HasSimpleRep (Proposals (ConwayEra StandardCrypto)) where buildProposalTree :: TreeMaybe (GovActionId StandardCrypto) -> ProposalTree buildProposalTree (TreeMaybe (Node mId cs)) = (mId, map buildTree cs) - buildTree :: Tree (StrictMaybe (GovActionId StandardCrypto)) -> RoseTree GAS - buildTree (Node (SJust gid) cs) | Just gas <- Map.lookup gid idMap = RoseNode gas (map buildTree cs) + buildTree :: Tree (StrictMaybe (GovActionId StandardCrypto)) -> Tree GAS + buildTree (Node (SJust gid) cs) | Just gas <- Map.lookup gid idMap = Node gas (map buildTree cs) buildTree _ = error "toSimpleRep @Proposals: toGovRelationTree returned trees with Nothing nodes below the root" @@ -1077,7 +1076,7 @@ instance HasSimpleRep (Proposals (ConwayEra StandardCrypto)) where oMap = foldMap (foldMap mkOMap) [ppupTree, hfTree, comTree, conTree] <> OMap.fromFoldable others in unsafeMkProposals root oMap where - mkOMap (RoseNode a ts) = a OMap.<| foldMap mkOMap ts + mkOMap (Node a ts) = a OMap.<| foldMap mkOMap ts instance IsConwayUniv fn => HasSpec fn (Proposals (ConwayEra StandardCrypto)) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Ledger.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Ledger.hs index 097ebeda9f7..42f71c76044 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Ledger.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Ledger.hs @@ -19,7 +19,7 @@ ledgerTxSpec :: IsConwayUniv fn => LedgerEnv (ConwayEra StandardCrypto) -> LedgerState (ConwayEra StandardCrypto) -> - Spec fn (Tx (ConwayEra StandardCrypto)) + Specification fn (Tx (ConwayEra StandardCrypto)) ledgerTxSpec env st = constrained $ \tx -> [ satisfies tx (utxoTxSpec utxoEnv (lsUTxOState st)) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/PParams.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/PParams.hs index e55520fdacb..c8c9511807f 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/PParams.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/PParams.hs @@ -13,7 +13,7 @@ import Cardano.Ledger.Conway.Core import Cardano.Ledger.Crypto (StandardCrypto) import Test.Cardano.Ledger.Constrained.Conway.Instances (IsConwayUniv) -pparamsSpec :: IsConwayUniv fn => Spec fn (PParams (ConwayEra StandardCrypto)) +pparamsSpec :: IsConwayUniv fn => Specification fn (PParams (ConwayEra StandardCrypto)) pparamsSpec = constrained $ \pp -> match pp $ \cpp -> diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Pool.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Pool.hs index 02f8ca37b10..706feaf2911 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Pool.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Pool.hs @@ -31,7 +31,7 @@ currentEpoch = runIdentity . EI.epochInfoEpoch (epochInfoPure testGlobals) poolEnvSpec :: IsConwayUniv fn => - Spec fn (PoolEnv (ConwayEra StandardCrypto)) + Specification fn (PoolEnv (ConwayEra StandardCrypto)) poolEnvSpec = constrained $ \pe -> match pe $ \_ pp -> @@ -39,7 +39,7 @@ poolEnvSpec = pStateSpec :: IsConwayUniv fn => - Spec fn (PState (ConwayEra StandardCrypto)) + Specification fn (PState (ConwayEra StandardCrypto)) pStateSpec = constrained $ \ps -> match ps $ \stakePoolParams futureStakePoolParams retiring deposits -> [ assertExplain ["dom of retiring is a subset of dom of stakePoolParams"] $ @@ -57,7 +57,7 @@ poolCertSpec :: IsConwayUniv fn => PoolEnv (ConwayEra StandardCrypto) -> PState (ConwayEra StandardCrypto) -> - Spec fn (PoolCert StandardCrypto) + Specification fn (PoolCert StandardCrypto) poolCertSpec (PoolEnv s pp) ps = constrained $ \pc -> (caseOn pc) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Utxo.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Utxo.hs index 9c9739f14b3..a01ccafe717 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Utxo.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Utxo.hs @@ -29,7 +29,7 @@ import Cardano.Ledger.Crypto (StandardCrypto) import Test.Cardano.Ledger.Constrained.Conway.Instances import Test.Cardano.Ledger.Constrained.Conway.PParams -utxoEnvSpec :: IsConwayUniv fn => Spec fn (UtxoEnv (ConwayEra StandardCrypto)) +utxoEnvSpec :: IsConwayUniv fn => Specification fn (UtxoEnv (ConwayEra StandardCrypto)) utxoEnvSpec = constrained $ \utxoEnv -> match utxoEnv $ @@ -79,7 +79,7 @@ utxoEnvSpec = utxoStateSpec :: IsConwayUniv fn => UtxoEnv (ConwayEra StandardCrypto) -> - Spec fn (UTxOState (ConwayEra StandardCrypto)) + Specification fn (UTxOState (ConwayEra StandardCrypto)) utxoStateSpec _env = constrained $ \utxoState -> match utxoState $ @@ -98,7 +98,7 @@ utxoTxSpec :: IsConwayUniv fn => UtxoEnv (ConwayEra StandardCrypto) -> UTxOState (ConwayEra StandardCrypto) -> - Spec fn (Tx (ConwayEra StandardCrypto)) + Specification fn (Tx (ConwayEra StandardCrypto)) utxoTxSpec env st = constrained $ \tx -> match tx $ \bdy _wits isValid _auxData -> diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs index ead9a6131f9..bfeaa4bbd8a 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs @@ -44,7 +44,7 @@ import Test.Tasty.QuickCheck type GenShrink a = (Gen a, a -> [a]) -genShrinkFromSpec :: forall fn a. HasSpec fn a => Spec fn a -> GenShrink a +genShrinkFromSpec :: forall fn a. HasSpec fn a => Specification fn a -> GenShrink a genShrinkFromSpec spec = (genFromSpec_ @fn spec, shrinkWithSpec @fn spec) stsPropertyV2 :: @@ -65,9 +65,9 @@ stsPropertyV2 :: , HasSpec fn st , HasSpec fn sig ) => - Spec fn env -> - (env -> Spec fn st) -> - (env -> st -> Spec fn sig) -> + Specification fn env -> + (env -> Specification fn st) -> + (env -> st -> Specification fn sig) -> (env -> st -> sig -> st -> p) -> Property stsPropertyV2 specEnv specState specSig prop = diff --git a/libs/constrained-generators/bench/Constrained/Bench.hs b/libs/constrained-generators/bench/Constrained/Bench.hs new file mode 100644 index 00000000000..5f609163e6d --- /dev/null +++ b/libs/constrained-generators/bench/Constrained/Bench.hs @@ -0,0 +1,57 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Constrained.Bench where + +import Constrained +import Control.DeepSeq +import Criterion +import Data.Map (Map) +import Data.Set (Set) +import Data.Tree + +type RoseFn = Fix (OneofL (TreeFn : BaseFns)) + +benchmarks :: Benchmark +benchmarks = + bgroup + "constrained" + [ benchSpec 10 30 "TrueSpec@Map" (TrueSpec :: Specification BaseFn (Map Int Int)) + , benchSpec 10 30 "TrueSpec@[]" (TrueSpec :: Specification BaseFn [Int]) + , benchSpec 10 30 "TrueSpec@Set" (TrueSpec :: Specification BaseFn (Set Int)) + , benchSpec + 10 + 30 + "TrueSpec@Tree" + (giveHint (Nothing, 30) <> TrueSpec :: Specification RoseFn (Tree Int)) + , benchSpec 10 30 "roseTreeMaybe" roseTreeMaybe + , benchSpec 10 30 "listSumPair" listSumPair + ] + +roseTreeMaybe :: Specification RoseFn (Tree (Maybe (Int, Int))) +roseTreeMaybe = constrained $ \t -> + [ forAll' t $ \mp ts -> + forAll ts $ \t' -> + onJust mp $ \p -> + onJust (rootLabel_ t') $ \p' -> + fst_ p' ==. snd_ p + , forAll' t $ \mp _ -> isJust mp + , genHint (Nothing, 10) t + ] + +listSumPair :: Specification BaseFn [(Int, Int)] +listSumPair = constrained $ \xs -> + [ assert $ foldMap_ (composeFn fstFn toGenericFn) xs ==. 100 + , forAll' xs $ \x y -> [20 <. x, x <. 30, y <. 100] + ] + +benchSpec :: (HasSpec fn a, NFData a) => Int -> Int -> String -> Specification fn a -> Benchmark +benchSpec seed size nm spec = + bench (unlines [nm, show (genFromSpecWithSeed seed size spec)]) $ + nf (genFromSpecWithSeed seed size) spec diff --git a/libs/constrained-generators/constrained-generators.cabal b/libs/constrained-generators/constrained-generators.cabal index 81bb18307d8..36ec415422b 100644 --- a/libs/constrained-generators/constrained-generators.cabal +++ b/libs/constrained-generators/constrained-generators.cabal @@ -32,9 +32,15 @@ library Constrained.Spec.Pairs Constrained.Spec.Maps Constrained.Spec.Tree - Constrained.Test Constrained.Internals - Constrained.Bench + Constrained.Examples + Constrained.Examples.Basic + Constrained.Examples.Map + Constrained.Examples.Set + Constrained.Examples.List + Constrained.Examples.Tree + Constrained.Examples.Either + Constrained.Properties hs-source-dirs: src default-language: Haskell2010 @@ -48,40 +54,41 @@ library containers, mtl, prettyprinter, - QuickCheck, - random, - tasty, - tasty-quickcheck, - ghc-prim, - deepseq, - criterion + QuickCheck ^>=2.14, + random test-suite constrained type: exitcode-stdio-1.0 main-is: Tests.hs hs-source-dirs: test + other-modules: Constrained.Test default-language: Haskell2010 ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints - -Wunused-packages -rtsopts -threaded + -Wunused-packages build-depends: base, constrained-generators, - tasty + hspec, + containers, + QuickCheck benchmark bench type: exitcode-stdio-1.0 main-is: Main.hs hs-source-dirs: bench + other-modules: Constrained.Bench default-language: Haskell2010 ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints - -Wunused-packages -threaded -rtsopts -O2 + -Wunused-packages build-depends: base, + containers, + constrained-generators, criterion, - constrained-generators + deepseq diff --git a/libs/constrained-generators/src/Constrained.hs b/libs/constrained-generators/src/Constrained.hs index 4c810e1ae63..cfe9afc3a8b 100644 --- a/libs/constrained-generators/src/Constrained.hs +++ b/libs/constrained-generators/src/Constrained.hs @@ -5,7 +5,7 @@ -- It is supposed to contain everything you need to write constraints -- and implement `HasSpec` and `HasSimpleRep` instances. module Constrained ( - Spec (..), -- TODO: it would be nice not to expose this whole thing + Specification (..), -- TODO: it would be nice not to expose this whole thing Pred (..), -- TODO: it would be nice not to expose this whole thing Term, Binder (..), -- TODO: it would be nice not to expose this whole thing @@ -93,6 +93,8 @@ module Constrained ( right_, toGeneric_, fromGeneric_, + sizeOf_, + length_, injectFn, app, lit, diff --git a/libs/constrained-generators/src/Constrained/Base.hs b/libs/constrained-generators/src/Constrained/Base.hs index 5d42fc80afa..aab9b6ee90d 100644 --- a/libs/constrained-generators/src/Constrained/Base.hs +++ b/libs/constrained-generators/src/Constrained/Base.hs @@ -39,7 +39,7 @@ -- be a nice thing to do but it's not very easy. The problem -- is that a lot of the things in here depend on each other -- via a cycle like `Pred` depends on `Term` which depend on --- `HasSpec` which depends on `Spec` and `Generic` and `Spec` +-- `HasSpec` which depends on `Specification` and `Generic` and `Specification` -- depends in turn on `Pred` and so on. module Constrained.Base where @@ -89,13 +89,13 @@ import Constrained.Univ The strategy for generating things from `Pred`s is relatively straightforward and relies on one key fact: any constraint that has only one free variable `x` -and where `x` occurs only once can be turned into a `Spec` for `x`. +and where `x` occurs only once can be turned into a `Specification` for `x`. We say that such constraints _define_ `x` and given a set of constraints `ps` and a variable `x` we can split `ps` into the constraints that define `x` and any constraints that don't. We can then generate a value from `x` by computing a spec for each defining constraint in `ps` and using the `Semigroup` structure -of `Spec`s to combine them and give them to `genFromSpec`. Once we obtain a +of `Specification`s to combine them and give them to `genFromSpec`. Once we obtain a value for `x` we can substitute this value in all other constraints and pick another variable to solve. @@ -106,7 +106,7 @@ For example, given the following constraints on integers `x` and `y` y < x we see that `x < 10` and `3 <= x` are defining constraints for `x` and there -are no definining constraints for `y`. We compute a `Spec` for `x` for each +are no definining constraints for `y`. We compute a `Specification` for `x` for each constraint, in this case `x < 10` turns into something like `(-∞,10)` and `3 <= x` turns into `[3, ∞)`. We combine the specs to form `[3, 10)` from which we can generate a value, e.g. 4 (chosen by fair dice roll). We then substitute @@ -500,17 +500,17 @@ runCaseOn s ((x :-> ps) :> bs@(_ :> _)) f = case s of -- for instances of Ord at runtime! type OrdSet a = [a] --- | A `Spec fn a` denotes a set of `a`s -data Spec fn a where +-- | A `Specification fn a` denotes a set of `a`s +data Specification fn a where -- | Elements of a known set MemberSpec :: -- | It must be an element of this set OrdSet a -> - Spec fn a + Specification fn a -- | The empty set ErrorSpec :: [String] -> - Spec fn a + Specification fn a -- | The set described by some predicates -- over the bound variable. -- @@ -522,18 +522,18 @@ data Spec fn a where Var a -> -- | And the variable is subject to these constraints Pred fn -> - Spec fn a + Specification fn a -- | A type-specific spec TypeSpec :: HasSpec fn a => TypeSpec fn a -> -- | It can't be any of the elements of this set OrdSet a -> - Spec fn a + Specification fn a -- | Anything - TrueSpec :: Spec fn a + TrueSpec :: Specification fn a -instance HasSpec fn a => Semigroup (Spec fn a) where +instance HasSpec fn a => Semigroup (Specification fn a) where TrueSpec <> s = s s <> TrueSpec = s ErrorSpec e <> ErrorSpec e' = ErrorSpec (e ++ "" : (replicate 20 '-') : "" : e') @@ -560,19 +560,19 @@ instance HasSpec fn a => Semigroup (Spec fn a) where TypeSpec s'' cant'' -> TypeSpec s'' (cant <> cant' <> cant'') s'' -> s'' <> notMemberSpec (cant <> cant') -instance HasSpec fn a => Monoid (Spec fn a) where +instance HasSpec fn a => Monoid (Specification fn a) where mempty = TrueSpec -equalSpec :: a -> Spec fn a +equalSpec :: a -> Specification fn a equalSpec = MemberSpec . pure -notEqualSpec :: forall fn a. HasSpec fn a => a -> Spec fn a +notEqualSpec :: forall fn a. HasSpec fn a => a -> Specification fn a notEqualSpec = TypeSpec (emptySpec @fn @a) . pure -notMemberSpec :: forall fn a f. (HasSpec fn a, Foldable f) => f a -> Spec fn a +notMemberSpec :: forall fn a f. (HasSpec fn a, Foldable f) => f a -> Specification fn a notMemberSpec = typeSpecOpt (emptySpec @fn @a) . toList -typeSpec :: HasSpec fn a => TypeSpec fn a -> Spec fn a +typeSpec :: HasSpec fn a => TypeSpec fn a -> Specification fn a typeSpec ts = TypeSpec ts mempty -- The HasSpec Class ------------------------------------------------------ @@ -598,7 +598,7 @@ class ) => HasSpec fn a where - -- | The `TypeSpec fn a` is the type-specific `Spec fn a`. + -- | The `TypeSpec fn a` is the type-specific `Specification fn a`. type TypeSpec (fn :: [Type] -> Type -> Type) a type TypeSpec fn a = TypeSpec fn (SimpleRep a) @@ -606,12 +606,12 @@ class -- `TypeSpec` behaves sort-of like a monoid with a neutral -- enement `emptySpec` and a `combineSpec` for combining -- two `TypeSpec fn a`. However, in order to provide flexibilty - -- `combineSpec` takes two `TypeSpec` and provide a `Spec`. This + -- `combineSpec` takes two `TypeSpec` and provide a `Specification`. This -- avoids e.g. having to have a separate implementation of `ErrorSpec` -- and `MemberSpec` in `TypeSpec`. emptySpec :: TypeSpec fn a - combineSpec :: TypeSpec fn a -> TypeSpec fn a -> Spec fn a + combineSpec :: TypeSpec fn a -> TypeSpec fn a -> Specification fn a -- | Generate a value that satisfies the `TypeSpec`. -- The key property for this generator is soundness: @@ -630,23 +630,23 @@ class toPreds :: Term fn a -> TypeSpec fn a -> Pred fn -- | Compute an upper and lower bound on the number of solutions genFromTypeSpec might return - cardinalTypeSpec :: TypeSpec fn a -> Spec fn Integer + cardinalTypeSpec :: TypeSpec fn a -> Specification fn Integer cardinalTypeSpec _ = TrueSpec -- | A bound on the number of solutions `genFromTypeSpec TrueSpec` can produce. -- For a type with finite elements, we can get a much more accurate -- answer than TrueSpec - cardinalTrueSpec :: Spec fn Integer + cardinalTrueSpec :: Specification fn Integer cardinalTrueSpec = TrueSpec -- | For some types (especially finite ones) there may be much better ways to construct - -- a Spec than the default method of just adding a large 'bad' list to TypSpec. This + -- a Specification than the default method of just adding a large 'bad' list to TypSpec. This -- function allows each HasSpec instance to decide. - typeSpecOpt :: TypeSpec fn a -> [a] -> Spec fn a + typeSpecOpt :: TypeSpec fn a -> [a] -> Specification fn a typeSpecOpt tySpec bad = TypeSpec tySpec bad -- | Prerequisites for the instance that are sometimes necessary - -- when working with e.g. `Spec`s or functions in the universe. + -- when working with e.g. `Specification`s or functions in the universe. type Prerequisites fn a :: Constraint type Prerequisites fn a = () @@ -669,7 +669,7 @@ class below simply convert the relevant things between `SimpleRep a` and `a`. For example, in the implementation of `combineSpec s s'` we treat `s` and `s'` (which have type `TypeSpec fn a`) as `TypeSpec fn (SimpleRep a)`, - combine them, and go from the resulting `Spec fn (SimpleRep a)` to `Spec + combine them, and go from the resulting `Specification fn (SimpleRep a)` to `Specification fn a` using `fromSimpleRepSpec`. -} @@ -684,7 +684,7 @@ class ) => TypeSpec fn a -> TypeSpec fn a -> - Spec fn a + Specification fn a combineSpec s s' = fromSimpleRepSpec $ combineSpec @fn @(SimpleRep a) s s' default genFromTypeSpec :: @@ -734,7 +734,8 @@ data WithHasSpec fn f a where -- The Forallable class --------------------------------------------------- class Forallable t e | t -> e where - forAllSpec :: (HasSpec fn t, HasSpec fn e, BaseUniverse fn) => Spec fn e -> Spec fn t + forAllSpec :: + (HasSpec fn t, HasSpec fn e, BaseUniverse fn) => Specification fn e -> Specification fn t default forAllSpec :: ( HasSpec fn t , HasSpec fn e @@ -743,8 +744,8 @@ class Forallable t e | t -> e where , Forallable (SimpleRep t) e , HasSpec fn (SimpleRep t) ) => - Spec fn e -> - Spec fn t + Specification fn e -> + Specification fn t forAllSpec es = fromSimpleRepSpec $ forAllSpec @(SimpleRep t) @e es forAllToList :: t -> [e] @@ -762,25 +763,25 @@ class Forallable t e | t -> e where -- control distribution of generated values. class (HasSpec fn a, Show (Hint a)) => HasGenHint fn a where type Hint a - giveHint :: Hint a -> Spec fn a + giveHint :: Hint a -> Specification fn a -- Semantics of specs ----------------------------------------------------- conformsToSpecM :: - forall fn a m. (HasSpec fn a, MonadGenError m, Alternative m) => a -> Spec fn a -> m () + forall fn a m. (HasSpec fn a, MonadGenError m, Alternative m) => a -> Specification fn a -> m () conformsToSpecM _ TrueSpec = pure () conformsToSpecM a (MemberSpec as) = explain [show a ++ " not an element of " ++ show as] $ guard $ elem a as conformsToSpecM a (TypeSpec s cant) = guard $ notElem a cant && conformsTo @fn a s conformsToSpecM a (SuspendedSpec v ps) = guard =<< checkPred (singletonEnv v a) ps conformsToSpecM _ (ErrorSpec es) = explain es $ guard False -conformsToSpecProp :: forall fn a. HasSpec fn a => a -> Spec fn a -> Property +conformsToSpecProp :: forall fn a. HasSpec fn a => a -> Specification fn a -> Property conformsToSpecProp a s = fromGEProp $ conformsToSpecM a s -conformsToSpec :: forall fn a. HasSpec fn a => a -> Spec fn a -> Bool +conformsToSpec :: forall fn a. HasSpec fn a => a -> Specification fn a -> Bool conformsToSpec a s = isOk $ conformsToSpecM a s -satisfies :: forall fn a. HasSpec fn a => Term fn a -> Spec fn a -> Pred fn +satisfies :: forall fn a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn satisfies _ TrueSpec = TruePred satisfies e (MemberSpec as) = Assert [show e ++ " `elem` " ++ show as] $ elem_ e (Lit as) satisfies t (SuspendedSpec x p) = Subst x t p @@ -799,7 +800,8 @@ satisfies _ (ErrorSpec e) = FalsePred e -- | Generate a value that satisfies the spec. This function can fail if the -- spec is inconsistent, there is a dependency error, or if the underlying -- generators are not flexible enough. -genFromSpec :: forall fn a m. (HasCallStack, HasSpec fn a, MonadGenError m) => Spec fn a -> GenT m a +genFromSpec :: + forall fn a m. (HasCallStack, HasSpec fn a, MonadGenError m) => Specification fn a -> GenT m a genFromSpec TrueSpec = genFromSpec @fn (typeSpec $ emptySpec @fn @a) genFromSpec spec@(MemberSpec as) | null as = genError ["MemberSpec {}"] @@ -823,7 +825,7 @@ genFromSpec ts@(TypeSpec s cant) = genFromTypeSpec @fn s `suchThatT` (`notElem` cant) genFromSpec (ErrorSpec e) = genError e -shrinkWithSpec :: forall fn a. HasSpec fn a => Spec fn a -> a -> [a] +shrinkWithSpec :: forall fn a. HasSpec fn a => Specification fn a -> a -> [a] -- TODO: possibly allow for ignoring the `conformsToSpec` check in the `TypeSpec` -- case when you know what you're doing shrinkWithSpec spec a = filter (`conformsToSpec` spec) $ case spec of @@ -839,13 +841,14 @@ shrinkWithSpec spec a = filter (`conformsToSpec` spec) $ case spec of shr = shrinkWithTypeSpec @fn (emptySpec @fn @a) -- | A version of `genFromSpec` that simply errors if the generator fails -genFromSpec_ :: forall fn a. (HasCallStack, HasSpec fn a) => Spec fn a -> Gen a +genFromSpec_ :: forall fn a. (HasCallStack, HasSpec fn a) => Specification fn a -> Gen a genFromSpec_ spec = do res <- strictGen $ genFromSpec spec errorGE $ fmap pure res -- | A version of `genFromSpec` that takes a seed and a size and gives you a result -genFromSpecWithSeed :: forall fn a. (HasCallStack, HasSpec fn a) => Int -> Int -> Spec fn a -> a +genFromSpecWithSeed :: + forall fn a. (HasCallStack, HasSpec fn a) => Int -> Int -> Specification fn a -> a genFromSpecWithSeed seed size spec = unGen (genFromSpec_ spec) (mkQCGen seed) size genInverse :: @@ -855,7 +858,7 @@ genInverse :: , Functions fn fn ) => fn '[a] b -> - Spec fn a -> + Specification fn a -> b -> GenT m a genInverse f argS x = @@ -1004,7 +1007,8 @@ linearize preds graph = do ------------------------------------------------------------------------ -- | Precondition: the `Pred fn` defines the `Var a` -computeSpecSimplified :: forall fn a. (HasSpec fn a, HasCallStack) => Var a -> Pred fn -> Spec fn a +computeSpecSimplified :: + forall fn a. (HasSpec fn a, HasCallStack) => Var a -> Pred fn -> Specification fn a computeSpecSimplified x p = fromGE ErrorSpec $ case p of GenHint h t -> propagateSpec (giveHint h) <$> toCtx x t -- NOTE: this implies you do need to actually propagate hints, e.g. propagate depth control in a `tail` or `cdr` like function Subst x' t p' -> pure $ computeSpec x (substitutePred x' t p') -- NOTE: this is impossible as it should have gone away already @@ -1029,20 +1033,20 @@ computeSpecSimplified x p = fromGE ErrorSpec $ case p of Reify {} -> fatalError ["The impossible happened in computeSpec: Reify", show x, show p] -- | Precondition: the `Pred fn` defines the `Var a` -computeSpec :: forall fn a. (HasSpec fn a, HasCallStack) => Var a -> Pred fn -> Spec fn a +computeSpec :: forall fn a. (HasSpec fn a, HasCallStack) => Var a -> Pred fn -> Specification fn a computeSpec x p = computeSpecSimplified x (simplifyPred p) -computeSpecBinder :: Binder fn a -> Spec fn a +computeSpecBinder :: Binder fn a -> Specification fn a computeSpecBinder (x :-> p) = computeSpec x p -computeSpecBinderSimplified :: Binder fn a -> Spec fn a +computeSpecBinderSimplified :: Binder fn a -> Specification fn a computeSpecBinderSimplified (x :-> p) = computeSpecSimplified x p caseSpec :: forall fn as. HasSpec fn (SumOver as) => - List (Spec fn) as -> - Spec fn (SumOver as) + List (Specification fn) as -> + Specification fn (SumOver as) caseSpec Nil = error "The impossible happened in caseSpec" caseSpec (s :> Nil) = s caseSpec (s :> ss@(_ :> _)) @@ -1051,9 +1055,9 @@ caseSpec (s :> ss@(_ :> _)) propagateSpec :: forall fn v a. HasSpec fn v => - Spec fn a -> + Specification fn a -> Ctx fn v a -> - Spec fn v + Specification fn v propagateSpec spec = \case CtxHOLE -> spec CtxApp f (ListCtx pre c suf) @@ -1079,8 +1083,8 @@ class ) => f as b -> ListCtx Value as (HOLE a) -> - Spec fn b -> - Spec fn a + Specification fn b -> + Specification fn a rewriteRules :: ( TypeList as @@ -1099,7 +1103,7 @@ class ) => f '[a] b -> TypeSpec fn a -> - Spec fn b + Specification fn b mapSpec :: forall fn a b. @@ -1107,8 +1111,8 @@ mapSpec :: , HasSpec fn b ) => fn '[a] b -> - Spec fn a -> - Spec fn b + Specification fn a -> + Specification fn b mapSpec f TrueSpec = mapTypeSpec f (emptySpec @fn @a) mapSpec _ (ErrorSpec err) = ErrorSpec err mapSpec f (MemberSpec as) = MemberSpec $ map (sem f) as @@ -1117,8 +1121,9 @@ mapSpec f (SuspendedSpec x p) = Exists (\_ -> fatalError ["mapSpec"]) (x :-> fold [assert $ x' ==. app f (V x), p]) mapSpec f (TypeSpec ts cant) = mapTypeSpec f ts <> notMemberSpec (map (sem f) cant) --- | If the `Spec fn Bool` doesn't constrain the boolean you will get a `TrueSpec` out. -caseBoolSpec :: HasSpec fn a => Spec fn Bool -> (Bool -> Spec fn a) -> Spec fn a +-- | If the `Specification fn Bool` doesn't constrain the boolean you will get a `TrueSpec` out. +caseBoolSpec :: + HasSpec fn a => Specification fn Bool -> (Bool -> Specification fn a) -> Specification fn a caseBoolSpec spec cont = case possibleValues spec of [] -> ErrorSpec ["No possible values in caseBoolSpec"] [b] -> cont b @@ -1126,7 +1131,7 @@ caseBoolSpec spec cont = case possibleValues spec of where possibleValues s = filter (flip conformsToSpec s) [True, False] -isErrorLike :: Spec fn a -> Bool +isErrorLike :: Specification fn a -> Bool isErrorLike ErrorSpec {} = True isErrorLike (MemberSpec []) = True isErrorLike _ = False @@ -1848,8 +1853,8 @@ deriving instance Eq (GenericsFn fn args res) fromSimpleRepSpec :: forall a fn. (HasSpec fn a, HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) => - Spec fn (SimpleRep a) -> - Spec fn a + Specification fn (SimpleRep a) -> + Specification fn a fromSimpleRepSpec = \case TrueSpec -> TrueSpec ErrorSpec e -> ErrorSpec e @@ -1862,8 +1867,8 @@ fromSimpleRepSpec = \case toSimpleRepSpec :: forall a fn. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) => - Spec fn a -> - Spec fn (SimpleRep a) + Specification fn a -> + Specification fn (SimpleRep a) toSimpleRepSpec = \case TrueSpec -> TrueSpec ErrorSpec e -> ErrorSpec e @@ -1894,7 +1899,7 @@ toSimpleRepSpec = \case in constraints: ``` - fooSpec :: Spec fn Foo + fooSpec :: Specification fn Foo fooSpec = constrained $ \ foo -> match foo $ \ actualFoo -> ... ``` @@ -2075,7 +2080,8 @@ instance SimpleConstructor f => SimpleGeneric (C1 ('MetaCons c a b) f) where ------------------------------------------------------------------------ class HasSpec fn a => Foldy fn a where - genList :: (BaseUniverse fn, MonadGenError m) => Spec fn a -> Spec fn a -> GenT m [a] + genList :: + (BaseUniverse fn, MonadGenError m) => Specification fn a -> Specification fn a -> GenT m [a] theAddFn :: fn '[a, a] a theZero :: a @@ -2093,7 +2099,7 @@ data FoldSpec (fn :: [Type] -> Type -> Type) a where , BaseUniverse fn ) => fn '[a] b -> - Spec fn b -> + Specification fn b -> FoldSpec fn a combineFoldSpec :: MonadGenError m => FoldSpec fn a -> FoldSpec fn a -> m (FoldSpec fn a) @@ -2129,7 +2135,7 @@ enumerateInterval (NumSpecInterval lo hi) = interleave (x : xs) ys = x : interleave ys xs isEmptyNumSpec :: - (TypeSpec fn a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) => Spec fn a -> Bool + (TypeSpec fn a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) => Specification fn a -> Bool isEmptyNumSpec = \case ErrorSpec {} -> True TrueSpec -> False @@ -2138,7 +2144,7 @@ isEmptyNumSpec = \case TypeSpec i cant -> null $ enumerateInterval i \\ cant knownUpperBound :: - (TypeSpec fn a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) => Spec fn a -> Maybe a + (TypeSpec fn a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) => Specification fn a -> Maybe a knownUpperBound TrueSpec = upperBound knownUpperBound (MemberSpec []) = Nothing knownUpperBound (MemberSpec as) = Just $ maximum as @@ -2153,7 +2159,7 @@ knownUpperBound (TypeSpec (NumSpecInterval lo hi) cant) = upper (lo <|> lowerBou | otherwise = listToMaybe $ [b, b - 1 .. a] \\ cant knownLowerBound :: - (TypeSpec fn a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) => Spec fn a -> Maybe a + (TypeSpec fn a ~ NumSpec a, Ord a, Enum a, Num a, MaybeBounded a) => Specification fn a -> Maybe a knownLowerBound TrueSpec = lowerBound knownLowerBound (MemberSpec []) = Nothing knownLowerBound (MemberSpec as) = Just $ minimum as @@ -2183,8 +2189,8 @@ narrowByFuelAndSize :: a -> -- | Integer Int -> - (Spec fn a, Spec fn a) -> - (Spec fn a, Spec fn a) + (Specification fn a, Specification fn a) -> + (Specification fn a, Specification fn a) narrowByFuelAndSize fuel size specs = loop (1000 :: Int) (narrowFoldSpecs specs) where @@ -2300,8 +2306,8 @@ narrowFoldSpecs :: , Random a , MaybeBounded a ) => - (Spec fn a, Spec fn a) -> - (Spec fn a, Spec fn a) + (Specification fn a, Specification fn a) -> + (Specification fn a, Specification fn a) narrowFoldSpecs specs = maybe specs narrowFoldSpecs (go specs) where -- Note: make sure there is some progress when returning Just or this will loop forever @@ -2369,8 +2375,8 @@ genNumList :: , MaybeBounded a , Foldy fn a ) => - Spec fn a -> - Spec fn a -> + Specification fn a -> + Specification fn a -> GenT m [a] genNumList elemSIn foldSIn = do let extraElemConstraints @@ -2385,11 +2391,9 @@ genNumList elemSIn foldSIn = do let narrowedSpecs = narrowFoldSpecs (normElemS, normFoldS) explain [ "Can't generate list of ints with fold constraint" - , show $ " elemSpec =" <+> pretty elemSIn - , show $ " elemSpec <> extra =" <+> pretty elemSIn' - , show $ " normElemSpec =" <+> pretty normElemS - , show $ " foldSpec =" <+> pretty foldSIn - , show $ " narrowedSpecs =" <+> pretty narrowedSpecs + , " elemSpec = " ++ show elemSIn + , " normElemSpec = " ++ show normElemS + , " foldSpec = " ++ show foldSIn ] $ gen narrowedSpecs 50 [] >>= pureGen . shuffle where @@ -2416,13 +2420,14 @@ genNumList elemSIn foldSIn = do (maybe es (flip Set.insert es) me) (spec <> maybe mempty notEqualSpec me) - gen :: forall m'. MonadGenError m' => (Spec fn a, Spec fn a) -> Int -> [a] -> GenT m' [a] + gen :: + forall m'. MonadGenError m' => (Specification fn a, Specification fn a) -> Int -> [a] -> GenT m' [a] gen (elemS, foldS) fuel lst | fuel <= 0 , not $ 0 `conformsToSpec` foldS = genError [ "Ran out of fuel in genNumList" - , " " ++ show ("elemSpec =" <+> pretty elemSIn) + , " elemSpec =" ++ show elemSIn , " foldSpec = " ++ show foldSIn , " lst = " ++ show (reverse lst) ] @@ -2515,10 +2520,10 @@ genFromFold :: , HasSpec fn a ) => [a] -> - Spec fn Integer -> - Spec fn a -> + Specification fn Integer -> + Specification fn a -> fn '[a] b -> - Spec fn b -> + Specification fn b -> GenT m [a] genFromFold must size elemS fn foldS = do let elemS' = mapSpec fn elemS @@ -2560,12 +2565,12 @@ instance (BaseUniverse fn, HasSpec fn ()) => HasSpec fn Bool where -- Sum -------------------------------------------------------------------- -guardSumSpec :: (HasSpec fn a, HasSpec fn b) => SumSpec fn a b -> Spec fn (Sum a b) +guardSumSpec :: (HasSpec fn a, HasSpec fn b) => SumSpec fn a b -> Specification fn (Sum a b) guardSumSpec s@(SumSpec sa sb) | isErrorLike sa, isErrorLike sb = ErrorSpec ["empty SumSpec"] | otherwise = typeSpec s -data SumSpec fn a b = SumSpec (Spec fn a) (Spec fn b) +data SumSpec fn a b = SumSpec (Specification fn a) (Specification fn b) instance (HasSpec fn a, HasSpec fn b) => Semigroup (SumSpec fn a b) where SumSpec sa sb <> SumSpec sa' sb' = SumSpec (sa <> sa') (sb <> sb') @@ -2615,7 +2620,7 @@ deriving instance (HasSpec fn a, HasSpec fn b) => Show (SumSpec fn a b) -- Sets ------------------------------------------------------------------- -data SetSpec fn a = SetSpec (Set a) (Spec fn a) (Spec fn Integer) +data SetSpec fn a = SetSpec (Set a) (Specification fn a) (Specification fn Integer) instance (Ord a, HasSpec fn a) => Semigroup (SetSpec fn a) where SetSpec must es size <> SetSpec must' es' size' = @@ -2664,7 +2669,7 @@ instance (Ord a, HasSpec fn a) => HasSpec fn (Set a) where <> satisfies (size_ s) size instance Ord a => Forallable (Set a) a where - forAllSpec (e :: Spec fn a) + forAllSpec (e :: Specification fn a) | Evidence <- prerequisites @fn @(Set a) = typeSpec $ SetSpec mempty e TrueSpec forAllToList = Set.toList @@ -2792,7 +2797,8 @@ instance BaseUniverse fn => Functions (SetFn fn) fn where -- List ------------------------------------------------------------------- -data ListSpec fn a = ListSpec (Maybe Integer) [a] (Spec fn Integer) (Spec fn a) (FoldSpec fn a) +data ListSpec fn a + = ListSpec (Maybe Integer) [a] (Specification fn Integer) (Specification fn a) (FoldSpec fn a) deriving instance Show (FoldSpec fn a) deriving instance HasSpec fn a => Show (ListSpec fn a) @@ -2930,7 +2936,7 @@ emptyNumSpec :: Ord a => NumSpec a emptyNumSpec = mempty combineNumSpec :: - (HasSpec fn n, Ord n, TypeSpec fn n ~ NumSpec n) => NumSpec n -> NumSpec n -> Spec fn n + (HasSpec fn n, Ord n, TypeSpec fn n ~ NumSpec n) => NumSpec n -> NumSpec n -> Specification fn n combineNumSpec s s' = case s <> s' of s''@(NumSpecInterval (Just a) (Just b)) | a > b -> ErrorSpec [show s''] s'' -> typeSpec s'' @@ -3242,44 +3248,44 @@ data OrdFn (fn :: [Type] -> Type -> Type) as b where Less :: (Ord a, OrdLike fn a) => OrdFn fn '[a, a] Bool class HasSpec fn a => OrdLike fn a where - leqSpec :: a -> Spec fn a + leqSpec :: a -> Specification fn a default leqSpec :: ( TypeSpec fn a ~ TypeSpec fn (SimpleRep a) , HasSimpleRep a , OrdLike fn (SimpleRep a) ) => a -> - Spec fn a + Specification fn a leqSpec = fromSimpleRepSpec . leqSpec @fn . toSimpleRep - ltSpec :: a -> Spec fn a + ltSpec :: a -> Specification fn a default ltSpec :: ( TypeSpec fn a ~ TypeSpec fn (SimpleRep a) , HasSimpleRep a , OrdLike fn (SimpleRep a) ) => a -> - Spec fn a + Specification fn a ltSpec = fromSimpleRepSpec . ltSpec @fn . toSimpleRep - geqSpec :: a -> Spec fn a + geqSpec :: a -> Specification fn a default geqSpec :: ( TypeSpec fn a ~ TypeSpec fn (SimpleRep a) , HasSimpleRep a , OrdLike fn (SimpleRep a) ) => a -> - Spec fn a + Specification fn a geqSpec = fromSimpleRepSpec . geqSpec @fn . toSimpleRep - gtSpec :: a -> Spec fn a + gtSpec :: a -> Specification fn a default gtSpec :: ( TypeSpec fn a ~ TypeSpec fn (SimpleRep a) , HasSimpleRep a , OrdLike fn (SimpleRep a) ) => a -> - Spec fn a + Specification fn a gtSpec = fromSimpleRepSpec . gtSpec @fn . toSimpleRep instance {-# OVERLAPPABLE #-} (HasSpec fn a, MaybeBounded a, Num a, TypeSpec fn a ~ NumSpec a) => OrdLike fn a where @@ -3402,7 +3408,7 @@ instance FunctionLike (IntFn fn) where sem Negate = negate class (Num a, HasSpec fn a) => NumLike fn a where - subtractSpec :: a -> TypeSpec fn a -> Spec fn a + subtractSpec :: a -> TypeSpec fn a -> Specification fn a default subtractSpec :: ( TypeSpec fn a ~ TypeSpec fn (SimpleRep a) , HasSimpleRep a @@ -3410,17 +3416,17 @@ class (Num a, HasSpec fn a) => NumLike fn a where ) => a -> TypeSpec fn a -> - Spec fn a + Specification fn a subtractSpec a ts = fromSimpleRepSpec $ subtractSpec @fn (toSimpleRep a) ts - negateSpec :: TypeSpec fn a -> Spec fn a + negateSpec :: TypeSpec fn a -> Specification fn a default negateSpec :: ( TypeSpec fn a ~ TypeSpec fn (SimpleRep a) , HasSimpleRep a , NumLike fn (SimpleRep a) ) => TypeSpec fn a -> - Spec fn a + Specification fn a negateSpec = fromSimpleRepSpec . negateSpec @fn @(SimpleRep a) safeSubtract :: a -> a -> Maybe a @@ -3682,7 +3688,7 @@ constrained :: forall a fn p. (IsPred p fn, HasSpec fn a) => (Term fn a -> p) -> - Spec fn a + Specification fn a constrained body = let x :-> p = bind body in computeSpecSimplified x (optimisePred p) @@ -3909,7 +3915,7 @@ instance HasSpec fn a => Show (Term fn a) where instance Show (Pred fn) where show = show . pretty -instance HasSpec fn a => Pretty (WithPrec (Spec fn a)) where +instance HasSpec fn a => Pretty (WithPrec (Specification fn a)) where pretty (WithPrec d s) = case s of ErrorSpec es -> "ErrorSpec" /> vsep' (map fromString es) TrueSpec -> "TrueSpec" @@ -3922,10 +3928,10 @@ instance HasSpec fn a => Pretty (WithPrec (Spec fn a)) where <+> fromString (showsPrec 11 ts "") <+> viaShow cant -instance HasSpec fn a => Pretty (Spec fn a) where +instance HasSpec fn a => Pretty (Specification fn a) where pretty = pretty . WithPrec 0 -instance HasSpec fn a => Show (Spec fn a) where +instance HasSpec fn a => Show (Specification fn a) where showsPrec d = shows . pretty . WithPrec d -- ====================================================================== @@ -3936,7 +3942,7 @@ instance HasSpec fn a => Show (Spec fn a) where -- | Because Sizes should always be >= 0, We provide this alternate generator -- that can be used to replace (genFromSpec @Integer), to ensure this important property -genFromSizeSpec :: (BaseUniverse fn, MonadGenError m) => Spec fn Integer -> GenT m Integer +genFromSizeSpec :: (BaseUniverse fn, MonadGenError m) => Specification fn Integer -> GenT m Integer genFromSizeSpec integerSpec = genFromSpec (integerSpec <> geqSpec 0) data SizeFn (fn :: [Type] -> Type -> Type) as b where @@ -3965,7 +3971,7 @@ instance (BaseUniverse fn, HasSpec fn Integer) => Functions (SizeFn fn) fn where mapTypeSpec f ts = mapTypeSpecSize f ts -mapTypeSpecSize :: forall fn a b f. f ~ SizeFn fn => f '[a] b -> TypeSpec fn a -> Spec fn b +mapTypeSpecSize :: forall fn a b f. f ~ SizeFn fn => f '[a] b -> TypeSpec fn a -> Specification fn b mapTypeSpecSize f ts = case f of SizeOf -> constrained $ \x -> @@ -3995,11 +4001,11 @@ atMostSize a | a < 0 = error ("Negative Int in call to atMostSize: " ++ show a) | otherwise = NumSpecInterval Nothing (Just a) -exactSizeSpec :: BaseUniverse fn => Integer -> Spec fn Integer +exactSizeSpec :: BaseUniverse fn => Integer -> Specification fn Integer exactSizeSpec a = MemberSpec [a] -- | The widest interval whose largest element is admitted by the original spec -maxSpec :: BaseUniverse fn => Spec fn Integer -> Spec fn Integer +maxSpec :: BaseUniverse fn => Specification fn Integer -> Specification fn Integer maxSpec TrueSpec = TrueSpec maxSpec s@(SuspendedSpec _ _) = constrained $ \x -> unsafeExists $ \y -> [y `satisfies` s, Assert ["maxSpec on SuspendedSpec"] (x <=. y)] @@ -4014,9 +4020,9 @@ maxSpec (TypeSpec (NumSpecInterval _ hi) bad) = TypeSpec (NumSpecInterval Nothin class Sized t where sizeOf :: t -> Integer - liftSizeSpec :: HasSpec fn t => SizeSpec -> Spec fn t - liftMemberSpec :: HasSpec fn t => OrdSet Integer -> Spec fn t - sizeOfTypeSpec :: HasSpec fn t => TypeSpec fn t -> Spec fn Integer + liftSizeSpec :: HasSpec fn t => SizeSpec -> Specification fn t + liftMemberSpec :: HasSpec fn t => OrdSet Integer -> Specification fn t + sizeOfTypeSpec :: HasSpec fn t => TypeSpec fn t -> Specification fn Integer instance Ord a => Sized (Set.Set a) where sizeOf = toInteger . Set.size @@ -4032,7 +4038,7 @@ instance Sized [a] where sizeOfTypeSpec (ListSpec _ must sizespec _ _) = sizespec <> (TypeSpec (atLeastSize (sizeOf must)) []) -- How to constrain the size of any type, with a Sized instance -hasSize :: (HasSpec fn t, Sized t) => SizeSpec -> Spec fn t +hasSize :: (HasSpec fn t, Sized t) => SizeSpec -> Specification fn t hasSize sz = liftSizeSpec sz -- ================================================================================== @@ -4064,27 +4070,30 @@ instance Num (NumSpec Integer) where signum = error "No signum in the Num (NumSpec Integer) instance" -- ======================================================================== --- To implement the (HasSpec fn t) method: cardinalTypeSpec :: HasSpec fn a => TypeSpec fn a -> Spec fn Integer --- We are going to need some arithmetic-like operations on (Spec fn Integer) +-- To implement the (HasSpec fn t) method: cardinalTypeSpec :: HasSpec fn a => TypeSpec fn a -> Specification fn Integer +-- We are going to need some arithmetic-like operations on (Specification fn Integer) -- We will instance equations like these in some HasSpec instances -- -- cardinalTypeSpec (Cartesian x y) = 'multSpecInt' (cardinality x) (cardinality y) -- -- cardinalTypeSpec (SumSpec leftspec rightspec) = 'addSpecInt' (cardinality leftspec) (cardinality rightspec) -- --- To get those functions, we are going to have to lift opertions on (TypeSpec fn Integer) to (Spec fn Integer) +-- To get those functions, we are going to have to lift opertions on (TypeSpec fn Integer) to (Specification fn Integer) -addSpecInt :: BaseUniverse fn => Spec fn Integer -> Spec fn Integer -> Spec fn Integer +addSpecInt :: + BaseUniverse fn => Specification fn Integer -> Specification fn Integer -> Specification fn Integer addSpecInt x y = operateSpec (+) (+) x y -subSpecInt :: BaseUniverse fn => Spec fn Integer -> Spec fn Integer -> Spec fn Integer +subSpecInt :: + BaseUniverse fn => Specification fn Integer -> Specification fn Integer -> Specification fn Integer subSpecInt x y = operateSpec (-) (-) x y -multSpecInt :: BaseUniverse fn => Spec fn Integer -> Spec fn Integer -> Spec fn Integer +multSpecInt :: + BaseUniverse fn => Specification fn Integer -> Specification fn Integer -> Specification fn Integer multSpecInt x y = operateSpec (*) (*) x y -- | let 'n' be some numeric type, and 'f' and 'ft' be operations on 'n' and (TypeSpec fn n) --- Then lift these operations from (TypeSpec fn n) to (Spec fn n) +-- Then lift these operations from (TypeSpec fn n) to (Specification fn n) -- Normally 'f' will be a (Num n) instance method (+,-,*) on n, -- and 'ft' will be a a (Num (TypeSpec fn n)) instance method (+,-,*) on (TypeSpec fn n) -- But this will work for any operations 'f' and 'ft' with the right types @@ -4092,9 +4101,9 @@ operateSpec :: (TypeSpec fn n ~ NumSpec n, Enum n, Ord n) => (n -> n -> n) -> (TypeSpec fn n -> TypeSpec fn n -> TypeSpec fn n) -> - Spec fn n -> - Spec fn n -> - Spec fn n + Specification fn n -> + Specification fn n -> + Specification fn n operateSpec f ft x y = case (x, y) of (ErrorSpec xs, ErrorSpec ys) -> ErrorSpec (xs ++ ys) (ErrorSpec xs, _) -> ErrorSpec xs @@ -4125,8 +4134,9 @@ operateSpec f ft x y = case (x, y) of -- | Put some (admittedly loose bounds) on the number of solutions that -- 'genFromTypeSpec' might return. For lots of types, there is no way to be very accurate. -- Here we lift the HasSpec methods 'cardinalTrueSpec' and 'cardinalTypeSpec' --- from (TypeSpec fn Integer) to (Spec fn Integer) -cardinality :: forall fn a. (Eq a, BaseUniverse fn, HasSpec fn a) => Spec fn a -> Spec fn Integer +-- from (TypeSpec fn Integer) to (Specification fn Integer) +cardinality :: + forall fn a. (Eq a, BaseUniverse fn, HasSpec fn a) => Specification fn a -> Specification fn Integer cardinality TrueSpec = cardinalTrueSpec @fn @a cardinality (MemberSpec es) = exactSizeSpec (sizeOf (nub es)) cardinality ErrorSpec {} = equalSpec 0 @@ -4137,9 +4147,10 @@ cardinality (TypeSpec s cant) = cardinality SuspendedSpec {} = cardinalTrueSpec @fn @a -- | A generic function to use as an instance for the HasSpec method --- cardinalTypeSpec :: HasSpec fn a => TypeSpec fn a -> Spec fn Integer +-- cardinalTypeSpec :: HasSpec fn a => TypeSpec fn a -> Specification fn Integer -- for types 'n' such that (TypeSpec n ~ NumSpec n) -cardinalSizeSpec :: forall n fn. (Integral n, Num n, MaybeBounded n) => NumSpec n -> Spec fn Integer +cardinalSizeSpec :: + forall n fn. (Integral n, Num n, MaybeBounded n) => NumSpec n -> Specification fn Integer cardinalSizeSpec (NumSpecInterval (Just lo) (Just hi)) = if hi >= lo then MemberSpec [toInteger (hi - lo)] else MemberSpec [0] cardinalSizeSpec (NumSpecInterval Nothing (Just hi)) = @@ -4171,9 +4182,9 @@ countSpec (NumSpecInterval lo hi) = if lo > hi then 0 else toInteger high - toIn finiteSize :: forall n. (Integral n, Bounded n) => Integer finiteSize = toInteger (maxBound @n) - toInteger (minBound @n) + 1 --- | This is an optimizing version of TypeSpec :: TypeSpec fn n -> [n] -> Spec fn n +-- | This is an optimizing version of TypeSpec :: TypeSpec fn n -> [n] -> Specification fn n -- for Bounded NumSpecs. --- notInNumSpec :: Bounded n => TypeSpec fn n -> [n] -> Spec fn n +-- notInNumSpec :: Bounded n => TypeSpec fn n -> [n] -> Specification fn n -- We use this function to specialize the (HasSpec fn t) method 'typeSpecOpt' for Bounded n. -- So given (TypeSpec interval badlist) we might want to transform it to (MemberSpec goodlist) -- There are 2 opportunities where this can payoff big time. @@ -4198,7 +4209,7 @@ notInNumSpec :: ) => NumSpec n -> [n] -> - Spec fn n + Specification fn n notInNumSpec ns@(NumSpecInterval a b) bad | toInteger (length bad) > (finiteSize @n `div` 2) || countSpec ns < toInteger (length bad) = MemberSpec [x | x <- [lowBound a .. highBound b], notElem x bad] @@ -4256,8 +4267,8 @@ multT PosInf PosInf = PosInf multT PosInf NegInf = NegInf multT PosInf (Ok _) = PosInf --- | Add information to a Spec, if it is an ErrorSpec, otherwise just return the Spec -explainSpec :: String -> Spec fn t -> Spec fn t +-- | Add information to a Specification, if it is an ErrorSpec, otherwise just return the Specification +explainSpec :: String -> Specification fn t -> Specification fn t explainSpec msg (ErrorSpec xs) = ErrorSpec (msg : xs) explainSpec _ spec = spec @@ -4265,11 +4276,12 @@ explainSpec _ spec = spec -- Generally useful functions -- | sizeOfSpec generalizes the method 'sizeOfTypeSpec' --- From (sizeOfTypeSpec :: TypeSpec fn t -> Spec fn Integer) --- To (sizeOfSpec :: Spec fn t -> Spec fn Integer) +-- From (sizeOfTypeSpec :: TypeSpec fn t -> Specification fn Integer) +-- To (sizeOfSpec :: Specification fn t -> Specification fn Integer) -- It is not unusual for instances (HasSpec fn t) to define sizeOfTypeSpec with calls to sizeOfSpec, --- Because many (TypeSpec fn t)'s contain (Spec fn s), for types 's' different from 't' -sizeOfSpec :: forall fn t. (BaseUniverse fn, Sized t) => Spec fn t -> Spec fn Integer +-- Because many (TypeSpec fn t)'s contain (Specification fn s), for types 's' different from 't' +sizeOfSpec :: + forall fn t. (BaseUniverse fn, Sized t) => Specification fn t -> Specification fn Integer sizeOfSpec TrueSpec = TrueSpec sizeOfSpec (MemberSpec xs) = MemberSpec (map sizeOf xs) sizeOfSpec (ErrorSpec xs) = ErrorSpec xs @@ -4281,7 +4293,7 @@ sizeOfSpec (SuspendedSpec x p) = sizeOfSpec (TypeSpec x _) = sizeOfTypeSpec @t @fn x -- | Turn a Size spec into an ErrorSpec if it has negative numbers. -checkForNegativeSize :: Spec fn Integer -> Spec fn Integer +checkForNegativeSize :: Specification fn Integer -> Specification fn Integer checkForNegativeSize spec@(TypeSpec (NumSpecInterval x y) _) = case (x, y) of (Just lo, _) | lo < 0 -> ErrorSpec ["Negative low bound in conversion to SizeSpec: " ++ show spec] diff --git a/libs/constrained-generators/src/Constrained/Bench.hs b/libs/constrained-generators/src/Constrained/Bench.hs deleted file mode 100644 index 44579a1a8c8..00000000000 --- a/libs/constrained-generators/src/Constrained/Bench.hs +++ /dev/null @@ -1,38 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} - -module Constrained.Bench where - -import Constrained -import Constrained.Test -import Control.DeepSeq -import Criterion -import Data.Map (Map) -import Data.Set (Set) - -benchmarks :: Benchmark -benchmarks = - bgroup - "constrained" - [ benchSpec 10 30 "TrueSpec@Map" (TrueSpec :: Spec BaseFn (Map Int Int)) - , benchSpec 10 30 "TrueSpec@[]" (TrueSpec :: Spec BaseFn [Int]) - , benchSpec 10 30 "TrueSpec@Set" (TrueSpec :: Spec BaseFn (Set Int)) - , benchSpec - 10 - 30 - "TrueSpec@RoseTree" - (giveHint (Nothing, 30) <> TrueSpec :: Spec RoseFn (RoseTree Int)) - , benchSpec 10 30 "roseTreeMaybe" roseTreeMaybe - , benchSpec 10 30 "listSumPair" (listSumPair @Int) - ] - -benchSpec :: (HasSpec fn a, NFData a) => Int -> Int -> String -> Spec fn a -> Benchmark -benchSpec seed size nm spec = - bench (unlines [nm, show (genFromSpecWithSeed seed size spec)]) $ - nf (genFromSpecWithSeed seed size) spec diff --git a/libs/constrained-generators/src/Constrained/Examples.hs b/libs/constrained-generators/src/Constrained/Examples.hs new file mode 100644 index 00000000000..3fd77375cd2 --- /dev/null +++ b/libs/constrained-generators/src/Constrained/Examples.hs @@ -0,0 +1,8 @@ +module Constrained.Examples (module X) where + +import Constrained.Examples.Basic as X +import Constrained.Examples.Either as X +import Constrained.Examples.List as X +import Constrained.Examples.Map as X +import Constrained.Examples.Set as X +import Constrained.Examples.Tree as X diff --git a/libs/constrained-generators/src/Constrained/Examples/Basic.hs b/libs/constrained-generators/src/Constrained/Examples/Basic.hs new file mode 100644 index 00000000000..17db49b7cb7 --- /dev/null +++ b/libs/constrained-generators/src/Constrained/Examples/Basic.hs @@ -0,0 +1,137 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE UndecidableInstances #-} + +module Constrained.Examples.Basic where + +import GHC.Generics + +import Constrained + +leqPair :: Specification BaseFn (Int, Int) +leqPair = constrained $ \p -> + match p $ \x y -> + x <=. y + +simplePairSpec :: Specification BaseFn (Int, Int) +simplePairSpec = constrained $ \p -> + match p $ \x y -> + [ x /=. 0 + , y /=. 0 + ] + +sizeAddOrSub1 :: Specification BaseFn Integer +sizeAddOrSub1 = constrained $ \s -> + 4 ==. s + 2 + +sizeAddOrSub2 :: Specification BaseFn Integer +sizeAddOrSub2 = constrained $ \s -> + 4 ==. 2 + s + +sizeAddOrSub3 :: Specification BaseFn Integer +sizeAddOrSub3 = constrained $ \s -> + 4 ==. s - 2 + +-- | We expect a negative Integer, so ltSpec tests for that. +sizeAddOrSub4 :: Specification BaseFn Integer +sizeAddOrSub4 = ltSpec 0 <> (constrained $ \s -> 4 ==. 2 - s) + +sizeAddOrSub5 :: Specification BaseFn Integer +sizeAddOrSub5 = constrained $ \s -> + 2 ==. 12 - s + +listSubSize :: Specification BaseFn [Int] +listSubSize = constrained $ \s -> + 2 ==. 12 - (sizeOf_ s) + +orPair :: Specification BaseFn (Int, Int) +orPair = constrained' $ \x y -> + x <=. 5 ||. y <=. 5 + +trickyCompositional :: Specification BaseFn (Int, Int) +trickyCompositional = constrained $ \p -> + satisfies p simplePairSpec <> assert (fst_ p ==. 1000) + +data Foo = Foo Int | Bar Int Int + deriving (Show, Eq, Ord, Generic) + +instance HasSimpleRep Foo +instance BaseUniverse fn => HasSpec fn Foo + +fooSpec :: Specification BaseFn Foo +fooSpec = constrained $ \foo -> + (caseOn foo) + (branch $ \i -> 0 <=. i) + (branch $ \i j -> i <=. j) + +intSpec :: Specification BaseFn (Int, Int) +intSpec = constrained' $ \a b -> + reify a (`mod` 10) $ \a' -> b ==. a' + +mapElemKeySpec :: Specification BaseFn Int +mapElemKeySpec = constrained $ \n -> + letBind (pair_ n $ lit (False, 4)) $ \(p :: Term BaseFn (Int, (Bool, Int))) -> + letBind (snd_ (snd_ p)) $ \x -> + [x <. 10, 0 <. x, not_ $ elem_ n $ lit []] + +intRangeSpec :: Int -> Specification BaseFn Int +intRangeSpec a = constrained $ \n -> n <. lit a + +testRewriteSpec :: Specification BaseFn ((Int, Int), (Int, Int)) +testRewriteSpec = constrained' $ \x y -> + x ==. fromGeneric_ (toGeneric_ y) + +pairSingletonSpec :: Specification BaseFn (Int, Int) +pairSingletonSpec = constrained $ \q -> + forAll (singleton_ q) $ \p -> + letBind (fst_ p) $ \x -> + letBind (snd_ p) $ \y -> + x <=. y + +parallelLet :: Specification BaseFn (Int, Int) +parallelLet = constrained $ \p -> + [ letBind (fst_ p) $ \x -> 0 <. x + , letBind (snd_ p) $ \x -> x <. 0 + ] + +letExists :: Specification BaseFn (Int, Int) +letExists = constrained $ \p -> + [ letBind (fst_ p) $ \x -> 0 <. x + , exists (\eval -> pure $ snd (eval p)) $ + \x -> + [ x <. 0 + , snd_ p ==. x + ] + ] + +letExistsLet :: Specification BaseFn (Int, Int) +letExistsLet = constrained $ \p -> + [ letBind (fst_ p) $ \x -> 0 <. x + , exists (\eval -> pure $ snd (eval p)) $ + \x -> + [ assert $ x <. 0 + , letBind (snd_ p) $ \y -> + [ x ==. y + , y <. -1 + ] + ] + ] + +dependencyWeirdness :: Specification BaseFn (Int, Int, Int) +dependencyWeirdness = constrained' $ \x y z -> + reify (x + y) id $ \zv -> z ==. zv + +parallelLetPair :: Specification BaseFn (Int, Int) +parallelLetPair = constrained $ \p -> + [ match p $ \x y -> + [ assert $ x <=. y + , y `dependsOn` x + ] + , match p $ \x y -> y <=. x + ] + +existsUnfree :: Specification BaseFn Int +existsUnfree = constrained $ \_ -> exists (\_ -> pure 1) $ \y -> y `elem_` lit [1, 2 :: Int] diff --git a/libs/constrained-generators/src/Constrained/Examples/Either.hs b/libs/constrained-generators/src/Constrained/Examples/Either.hs new file mode 100644 index 00000000000..acf5a0fd90f --- /dev/null +++ b/libs/constrained-generators/src/Constrained/Examples/Either.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE ImportQualifiedPost #-} + +module Constrained.Examples.Either where + +import Data.Set qualified as Set + +import Constrained + +eitherSpec :: Specification BaseFn (Either Int Int) +eitherSpec = constrained $ \e -> + (caseOn e) + (branch $ \i -> i <=. 0) + (branch $ \i -> 0 <=. i) + +foldTrueCases :: Specification BaseFn (Either Int Int) +foldTrueCases = constrained $ \x -> + [ assert $ not_ $ member_ x (lit (Set.fromList [Left 10])) + , letBind (pair_ x (lit (0 :: Int))) $ \p -> + caseOn + (fst_ p) + (branch $ \_ -> True) + (branch $ \_ -> True) + ] diff --git a/libs/constrained-generators/src/Constrained/Examples/List.hs b/libs/constrained-generators/src/Constrained/Examples/List.hs new file mode 100644 index 00000000000..52448b0cc4a --- /dev/null +++ b/libs/constrained-generators/src/Constrained/Examples/List.hs @@ -0,0 +1,104 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MonoLocalBinds #-} + +module Constrained.Examples.List where + +import Data.Word + +import Constrained +import Constrained.Examples.Basic + +type Numbery a = + ( Foldy BaseFn a + , OrdLike BaseFn a + , NumLike BaseFn a + , Ord a + , Enum a + ) + +listSum :: Numbery a => Specification BaseFn [a] +listSum = constrained $ \as -> + 10 <=. sum_ as + +listSumForall :: Numbery a => Specification BaseFn [a] +listSumForall = constrained $ \xs -> + [ forAll xs $ \x -> 1 <. x + , assert $ sum_ xs ==. 20 + ] + +listSumRange :: Numbery a => Specification BaseFn [a] +listSumRange = constrained $ \xs -> + let n = sum_ xs + in [ forAll xs $ \x -> 1 <. x + , assert $ n <. 20 + , assert $ 10 <. n + ] + +listSumRangeUpper :: Numbery a => Specification BaseFn [a] +listSumRangeUpper = constrained $ \xs -> + let n = sum_ xs + in -- All it takes is one big negative number, + -- then we can't get enough small ones to exceed 10 + -- in the number of tries allowed. + -- So we make x relatively large ( <. 12), If its is + -- relatively small ( <. 5), we can get unlucky. + [ forAll xs $ \x -> [x <. 12] + , assert $ n <. 20 + , assert $ 10 <. n + ] + +listSumRangeRange :: Numbery a => Specification BaseFn [a] +listSumRangeRange = constrained $ \xs -> + let n = sum_ xs + in [ forAll xs $ \x -> [1 <. x, x <. 5] + , assert $ n <. 20 + , assert $ 10 <. n + ] + +listSumElemRange :: Numbery a => Specification BaseFn [a] +listSumElemRange = constrained $ \xs -> + let n = sum_ xs + in [ forAll xs $ \x -> [1 <. x, x <. 5] + , assert $ n `elem_` lit [10, 12 .. 20] + ] + +listSumPair :: Numbery a => Specification BaseFn [(a, Int)] +listSumPair = constrained $ \xs -> + [ assert $ foldMap_ (composeFn fstFn toGenericFn) xs ==. 100 + , forAll' xs $ \x y -> [20 <. x, x <. 30, y <. 100] + ] + +listEmpty :: Specification BaseFn [Int] +listEmpty = constrained $ \xs -> + [ forAll xs $ \_ -> False + , assert $ length_ xs <=. 10 + ] + +pairListError :: Specification BaseFn [(Int, Int)] +pairListError = constrained $ \ps -> + [ assert $ length_ ps <=. 10 + , forAll' ps $ \a b -> + [ a `elem_` lit [1 .. 8] + , a ==. 9 + , b ==. a + ] + ] + +listMustSizeIssue :: Specification BaseFn [Int] +listMustSizeIssue = constrained $ \xs -> + [ 1 `elem_` xs + , length_ xs ==. 1 + ] + +sumListBad :: Specification BaseFn [Word64] +sumListBad = constrained $ \xs -> + [ forAll xs $ \x -> unsafeExists $ \y -> y ==. x + , assert $ sum_ xs ==. lit 10 + ] + +listExistsUnfree :: Specification BaseFn [Int] +listExistsUnfree = constrained $ \xs -> + [ forAll xs $ \x -> x `satisfies` existsUnfree + , assert $ sizeOf_ xs ==. 3 + ] diff --git a/libs/constrained-generators/src/Constrained/Examples/Map.hs b/libs/constrained-generators/src/Constrained/Examples/Map.hs new file mode 100644 index 00000000000..18ae6b41db6 --- /dev/null +++ b/libs/constrained-generators/src/Constrained/Examples/Map.hs @@ -0,0 +1,53 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE UndecidableInstances #-} + +module Constrained.Examples.Map where + +import Data.Map (Map) +import Data.Set (Set) +import Data.Set qualified as Set +import Data.Word +import GHC.Generics + +import Constrained + +mapElemSpec :: Specification BaseFn (Map Int (Bool, Int)) +mapElemSpec = constrained $ \m -> + [ assert $ m /=. lit mempty + , forAll' (rng_ m) $ \_ b -> + [0 <. b, b <. 10] + ] + +mapPairSpec :: Specification BaseFn (Map Int Int, Set Int) +mapPairSpec = constrained' $ \m s -> + subset_ (dom_ m) s + +mapEmptyDomainSpec :: Specification BaseFn (Map Int Int) +mapEmptyDomainSpec = constrained $ \m -> + subset_ (dom_ m) mempty -- mempty in the Monoid instance (Term fn (Set a)) + +mapSubSize :: Specification BaseFn (Map Int Int) +mapSubSize = constrained $ \s -> + 2 ==. 12 - (sizeOf_ s) + +knownDomainMap :: Specification BaseFn (Map Int Int) +knownDomainMap = constrained $ \m -> + [ dom_ m ==. lit (Set.fromList [1, 2]) + , not_ $ 0 `elem_` rng_ m + ] + +data Three = One | Two | Three + deriving (Ord, Eq, Show, Generic) + +instance HasSimpleRep Three +instance BaseUniverse fn => HasSpec fn Three + +mapSizeConstrained :: Specification BaseFn (Map Three Int) +mapSizeConstrained = constrained $ \m -> size_ (dom_ m) <=. 3 + +sumRange :: Specification BaseFn (Map Word64 Word64) +sumRange = constrained $ \m -> sum_ (rng_ m) ==. lit 10 diff --git a/libs/constrained-generators/src/Constrained/Examples/Set.hs b/libs/constrained-generators/src/Constrained/Examples/Set.hs new file mode 100644 index 00000000000..c06c94c0bd6 --- /dev/null +++ b/libs/constrained-generators/src/Constrained/Examples/Set.hs @@ -0,0 +1,164 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +module Constrained.Examples.Set where + +import GHC.Generics + +import Data.Set (Set) +import Data.Set qualified as Set + +import Constrained +import Constrained.Examples.Basic + +setPairSpec :: Specification BaseFn (Set Int, Set Int) +setPairSpec = constrained' $ \s s' -> + forAll s $ \x -> + forAll s' $ \y -> + x <=. y + +fixedSetSpec :: Specification BaseFn (Set Int) +fixedSetSpec = constrained $ \s -> + forAll s $ \x -> + [x <=. lit (i :: Int) | i <- [1 .. 3]] + +setOfPairLetSpec :: Specification BaseFn (Set (Int, Int)) +setOfPairLetSpec = constrained $ \ps -> + forAll' ps $ \x y -> + x <=. y + +setSingletonSpec :: Specification BaseFn (Set (Int, Int)) +setSingletonSpec = constrained $ \ps -> + forAll ps $ \p -> + forAll (singleton_ (fst_ p)) $ \x -> + x <=. 10 + +eitherSimpleSetSpec :: Specification BaseFn (Set (Either Int Int)) +eitherSimpleSetSpec = constrained $ \ss -> + forAll ss $ \s -> + (caseOn s) + (branch $ \a -> a <=. 0) + (branch $ \b -> 0 <=. b) + +forAllAnySpec :: Specification BaseFn (Set Int) +forAllAnySpec = constrained $ \as -> + forAll as $ \_ -> True + +maybeJustSetSpec :: Specification BaseFn (Set (Maybe Int)) +maybeJustSetSpec = constrained $ \ms -> + forAll ms $ \m -> + (caseOn m) + (branch $ \_ -> False) + (branch $ \y -> 0 <=. y) + +notSubsetSpec :: Specification BaseFn (Set Int, Set Int) +notSubsetSpec = constrained' $ \s s' -> not_ $ subset_ s s' + +emptyEitherMemberSpec :: Specification BaseFn (Set (Either Int Int)) +emptyEitherMemberSpec = constrained $ \s -> + forAll s $ \x -> + (caseOn x) + (branch $ \l -> member_ l mempty) + (branch $ \r -> member_ r mempty) + +emptyEitherSpec :: Specification BaseFn (Set (Either Int Int)) +emptyEitherSpec = constrained $ \s -> + forAll s $ \x -> + (caseOn x) + (branch $ \_ -> False) + (branch $ \_ -> False) + +notSubset :: Specification BaseFn (Set Int) +notSubset = constrained $ \s -> + not_ $ s `subset_` lit (Set.fromList [1, 2, 3]) + +unionSized :: Specification BaseFn (Set Int) +unionSized = constrained $ \s -> + 10 ==. size_ (s <> lit (Set.fromList [1 .. 8])) + +maybeSpec :: Specification BaseFn (Set (Maybe Int)) +maybeSpec = constrained $ \ms -> + forAll ms $ \m -> + (caseOn m) + (branch $ \_ -> False) + (branch $ \y -> 0 <=. y) + +eitherSetSpec :: + Specification BaseFn (Set (Either Int Int), Set (Either Int Int), Set (Either Int Int)) +eitherSetSpec = constrained' $ \es as bs -> + [ assert $ es ==. (as <> bs) + , forAll as $ \a -> + (caseOn a) + (branch $ \a' -> a' <=. 0) + (branch $ \b' -> 1 <=. b') + , forAll bs $ \b -> + (caseOn b) + (branch $ \_ -> False) + (branch $ \b' -> 1 <=. b') + ] + +weirdSetPairSpec :: Specification BaseFn ([Int], Set (Either Int Int)) +weirdSetPairSpec = constrained' $ \as as' -> + [ as' `dependsOn` as + , forAll as $ \a -> + member_ (left_ a) as' + , forAll as' $ \a' -> + (caseOn a') + (branch $ \x -> elem_ x as) + (branch $ \_ -> False) + ] + +setPair :: Specification BaseFn (Set (Int, Int)) +setPair = constrained $ \s -> + [ forAll s $ \p -> + p `satisfies` leqPair + , assert $ lit (0, 1) `member_` s + ] + +setSpec :: Specification BaseFn (Set Int) +setSpec = constrained $ \ss -> + forAll ss $ \s -> + s <=. 10 + +compositionalSpec :: Specification BaseFn (Set Int) +compositionalSpec = constrained $ \x -> + [ satisfies x setSpec + , assert $ 0 `member_` x + ] + +emptySetSpec :: Specification BaseFn (Set Int) +emptySetSpec = constrained $ \s -> + forAll s $ \x -> member_ x mempty + +setSubSize :: Specification BaseFn (Set Int) +setSubSize = constrained $ \s -> + 2 ==. 12 - (sizeOf_ s) + +newtype NotASet a = NotASet (Set a) + deriving (Generic, Show, Eq) +instance Ord a => HasSimpleRep (NotASet a) where + type SimpleRep (NotASet a) = [a] + fromSimpleRep = NotASet . Set.fromList + toSimpleRep (NotASet s) = Set.toList s +instance (Ord a, HasSpec fn a) => HasSpec fn (NotASet a) +instance Ord a => Forallable (NotASet a) a + +emptyListSpec :: Specification BaseFn ([Int], NotASet (Either Int Int, Int)) +emptyListSpec = constrained' $ \is ls -> + [ forAll is $ \i -> i <=. 0 + , forAll' ls $ \l _ -> + caseOn l (branch $ \_ -> False) (branch $ \_ -> False) + ] + +foldSingleCase :: Specification BaseFn Int +foldSingleCase = constrained $ \x -> + [ assert $ not_ $ member_ x (lit (Set.fromList [10])) + , letBind (pair_ x $ lit [(10, 20) :: (Int, Int)]) $ \p -> + match p $ \_ p1 -> forAll p1 $ \p2 -> + assert (0 <=. snd_ p2) + ] diff --git a/libs/constrained-generators/src/Constrained/Examples/Tree.hs b/libs/constrained-generators/src/Constrained/Examples/Tree.hs new file mode 100644 index 00000000000..e682e15083a --- /dev/null +++ b/libs/constrained-generators/src/Constrained/Examples/Tree.hs @@ -0,0 +1,116 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +module Constrained.Examples.Tree where + +import Data.Tree + +import Constrained + +allZeroTree :: Specification BaseFn (BinTree Int) +allZeroTree = constrained $ \t -> + [ forAll' t $ \_ a _ -> a ==. 0 + , genHint 10 t + ] + +isBST :: Specification BaseFn (BinTree Int) +isBST = constrained $ \t -> + [ forAll' t $ \left a right -> + -- TODO: if there was a `binTreeRoot` function on trees + -- this wouldn't need to be quadratic as we would + -- only check agains the head of the left and right + -- subtrees, not _every element_ + [ forAll' left $ \_ l _ -> l <. a + , forAll' right $ \_ h _ -> a <. h + ] + , genHint 10 t + ] + +noChildrenSameTree :: Specification BaseFn (BinTree Int) +noChildrenSameTree = constrained $ \t -> + [ forAll' t $ \left a right -> + [ forAll' left $ \_ l _ -> l /=. a + , forAll' right $ \_ r _ -> r /=. a + ] + , genHint 8 t + ] + +type RoseFn = Fix (OneofL (TreeFn : BaseFns)) + +isAllZeroTree :: Specification RoseFn (Tree Int) +isAllZeroTree = constrained $ \t -> + [ forAll' t $ \a cs -> + [ a ==. 0 + , length_ cs <=. 4 + ] + , genHint (Just 2, 30) t + ] + +noSameChildrenTree :: Specification RoseFn (Tree Int) +noSameChildrenTree = constrained $ \t -> + [ forAll' t $ \a cs -> + [ assert $ a `elem_` lit [1 .. 8] + , forAll cs $ \t' -> + forAll' t' $ \b _ -> + b /=. a + ] + , genHint (Just 2, 30) t + ] + +successiveChildren :: Specification RoseFn (Tree Int) +successiveChildren = constrained $ \t -> + [ forAll' t $ \a cs -> + [ forAll cs $ \t' -> + rootLabel_ t' ==. a + 1 + ] + , genHint (Just 2, 10) t + ] + +successiveChildren8 :: Specification RoseFn (Tree Int) +successiveChildren8 = constrained $ \t -> + [ t `satisfies` successiveChildren + , forAll' t $ \a _ -> a `elem_` lit [1 .. 5] + ] + +roseTreeList :: Specification RoseFn [Tree Int] +roseTreeList = constrained $ \ts -> + [ assert $ length_ ts <=. 10 + , forAll ts $ \t -> + [ forAll t $ \_ -> False + ] + ] + +roseTreePairs :: Specification RoseFn (Tree ([Int], [Int])) +roseTreePairs = constrained $ \t -> + [ assert $ rootLabel_ t ==. lit ([1 .. 10], [1 .. 10]) + , forAll' t $ \p ts -> + forAll ts $ \t' -> + fst_ (rootLabel_ t') ==. snd_ p + , genHint (Nothing, 10) t + ] + +roseTreeMaybe :: Specification RoseFn (Tree (Maybe (Int, Int))) +roseTreeMaybe = constrained $ \t -> + [ forAll' t $ \mp ts -> + forAll ts $ \t' -> + onJust mp $ \p -> + onJust (rootLabel_ t') $ \p' -> + fst_ p' ==. snd_ p + , forAll' t $ \mp _ -> isJust mp + , genHint (Nothing, 10) t + ] + +badTreeInteraction :: Specification RoseFn (Tree (Either Int Int)) +badTreeInteraction = constrained $ \t -> + [ forAll' t $ \n ts' -> + [ isCon @"Right" n + , forAll ts' $ \_ -> True + ] + , forAll' t $ \n ts' -> + forAll ts' $ \t' -> + [ genHint (Just 4, 10) t' + , assert $ rootLabel_ t' ==. n + ] + , genHint (Just 4, 10) t + ] diff --git a/libs/constrained-generators/src/Constrained/Instances.hs b/libs/constrained-generators/src/Constrained/Instances.hs index b0e4ab488c4..8ca942a8917 100644 --- a/libs/constrained-generators/src/Constrained/Instances.hs +++ b/libs/constrained-generators/src/Constrained/Instances.hs @@ -85,8 +85,8 @@ instance BaseUniverse fn => Functions (BoolFn fn) fn where mapTypeSpec Not (SumSpec a b) = typeSpec $ SumSpec b a --- | We have something like ('constant' ||. HOLE) must evaluate to 'need'. Return a (Spec fn Bool) for HOLE, that makes that True. -okOr :: Bool -> Bool -> Spec fn Bool +-- | We have something like ('constant' ||. HOLE) must evaluate to 'need'. Return a (Specification fn Bool) for HOLE, that makes that True. +okOr :: Bool -> Bool -> Specification fn Bool okOr constant need = case (constant, need) of (True, True) -> TrueSpec (True, False) -> ErrorSpec ["(" ++ show constant ++ "||. HOLE) must equal False. That cannot be the case."] diff --git a/libs/constrained-generators/src/Constrained/Properties.hs b/libs/constrained-generators/src/Constrained/Properties.hs new file mode 100644 index 00000000000..99cbafd0c3e --- /dev/null +++ b/libs/constrained-generators/src/Constrained/Properties.hs @@ -0,0 +1,89 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} + +-- | Useful properties for debugging custom @HasSpec@ instances. +module Constrained.Properties where + +import Constrained.Internals +import Test.QuickCheck qualified as QC + +prop_sound :: + HasSpec fn a => + Specification fn a -> + QC.Property +prop_sound spec = + QC.forAllBlind (strictGen $ genFromSpec spec) $ \ma -> + case ma of + Result _ a -> QC.cover 80 True "successful" $ QC.counterexample (show a) $ conformsToSpecProp a spec + _ -> QC.cover 80 False "successful" True + +-- | `prop_complete ps` assumes that `ps` is satisfiable +prop_complete :: HasSpec fn a => Specification fn a -> QC.Property +prop_complete s = + QC.forAllBlind (strictGen $ genFromSpec s) $ \ma -> fromGEProp $ do + a <- ma + -- Force the value to make sure we don't crash with `error` somewhere + -- or fall into an inifinite loop + pure $ length (show a) > 0 + +prop_shrink_sound :: HasSpec fn a => Specification fn a -> QC.Property +prop_shrink_sound s = + QC.forAll (strictGen $ genFromSpec s) $ \ma -> fromGEDiscard $ do + a <- ma + let shrinks = shrinkWithSpec s a + pure $ + QC.cover 40 (not $ null shrinks) "non-null shrinks" $ + if null shrinks + then QC.property True + else QC.forAll (QC.elements shrinks) $ \a' -> + conformsToSpecProp a' s + +prop_conformEmpty :: + forall fn a. + HasSpec fn a => + a -> + QC.Property +prop_conformEmpty a = QC.property $ conformsTo @fn a (emptySpec @fn @a) + +prop_propagateSpec :: + (HasSpec fn a, HasSpec fn b) => + Var b -> + Term fn a -> + Specification fn a -> + QC.Property +prop_propagateSpec var tm spec = + let spec' = errorGE $ do + ctx <- toCtx var tm + pure $ propagateSpec spec ctx + in QC.forAll (strictGen $ genFromSpec spec') $ \geval -> fromGE (\err -> QC.counterexample (unlines err) False) $ do + val <- geval + res <- runTerm (singletonEnv var val) tm + pure $ QC.property $ conformsToSpec res spec + +prop_mapSpec :: + ( HasSpec fn a + , HasSpec fn b + ) => + fn '[a] b -> + Specification fn a -> + QC.Property +prop_mapSpec fn spec = + QC.forAll (strictGen $ genFromSpec spec) $ \ma -> fromGEDiscard $ do + a <- ma + pure $ conformsToSpec (sem fn a) (mapSpec fn spec) + +prop_propagateSpecSound :: + ( HasSpec fn a + , HasSpec fn b + ) => + fn '[a] b -> + b -> + QC.Property +prop_propagateSpecSound fn b = + QC.forAll (strictGen $ genInverse fn TrueSpec b) $ \ma -> fromGEDiscard $ do + a <- ma + pure $ sem fn a == b diff --git a/libs/constrained-generators/src/Constrained/Spec/Generics.hs b/libs/constrained-generators/src/Constrained/Spec/Generics.hs index 5bd52fe26a8..6dd718f38d0 100644 --- a/libs/constrained-generators/src/Constrained/Spec/Generics.hs +++ b/libs/constrained-generators/src/Constrained/Spec/Generics.hs @@ -47,8 +47,8 @@ module Constrained.Spec.Generics ( ) where import Data.Typeable +import GHC.TypeLits (Symbol) import GHC.TypeNats -import GHC.Types (Symbol) import Constrained.Base import Constrained.Core @@ -383,7 +383,7 @@ constrained' :: , IsPred p fn ) => FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> - Spec fn a + Specification fn a constrained' f = constrained $ \x -> match @fn @p x f -- | Like `reify` but pattern matches on the bound `Term fn b` diff --git a/libs/constrained-generators/src/Constrained/Spec/Maps.hs b/libs/constrained-generators/src/Constrained/Spec/Maps.hs index 7803ce48313..f059775ad9b 100644 --- a/libs/constrained-generators/src/Constrained/Spec/Maps.hs +++ b/libs/constrained-generators/src/Constrained/Spec/Maps.hs @@ -45,8 +45,8 @@ instance Ord a => Sized (Map.Map a b) where data MapSpec fn k v = MapSpec { mapSpecMustKeys :: Set k , mapSpecMustValues :: [v] - , mapSpecSize :: Spec fn Integer - , mapSpecElem :: Spec fn (k, v) + , mapSpecSize :: Specification fn Integer + , mapSpecElem :: Specification fn (k, v) , mapSpecFold :: FoldSpec fn v } diff --git a/libs/constrained-generators/src/Constrained/Spec/Pairs.hs b/libs/constrained-generators/src/Constrained/Spec/Pairs.hs index 28799c72384..c7225b90340 100644 --- a/libs/constrained-generators/src/Constrained/Spec/Pairs.hs +++ b/libs/constrained-generators/src/Constrained/Spec/Pairs.hs @@ -27,14 +27,18 @@ import Constrained.Univ -- HasSpec ---------------------------------------------------------------- -cartesian :: (HasSpec fn a, HasSpec fn b) => Spec fn a -> Spec fn b -> Spec fn (Prod a b) +cartesian :: + (HasSpec fn a, HasSpec fn b) => + Specification fn a -> + Specification fn b -> + Specification fn (Prod a b) cartesian (MemberSpec []) _ = MemberSpec [] cartesian _ (MemberSpec []) = MemberSpec [] cartesian (ErrorSpec es) _ = ErrorSpec es cartesian _ (ErrorSpec es) = ErrorSpec es cartesian s s' = typeSpec $ Cartesian s s' -data PairSpec fn a b = Cartesian (Spec fn a) (Spec fn b) +data PairSpec fn a b = Cartesian (Specification fn a) (Specification fn b) instance (HasSpec fn a, HasSpec fn b) => HasSpec fn (Prod a b) where type TypeSpec fn (Prod a b) = PairSpec fn a b diff --git a/libs/constrained-generators/src/Constrained/Spec/Tree.hs b/libs/constrained-generators/src/Constrained/Spec/Tree.hs index 5a7c854cf97..999d4f0ed6a 100644 --- a/libs/constrained-generators/src/Constrained/Spec/Tree.hs +++ b/libs/constrained-generators/src/Constrained/Spec/Tree.hs @@ -11,11 +11,12 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} -module Constrained.Spec.Tree (BinTree (..), RoseTree (..), RoseTreeFn, roseRoot_, RoseTreeSpec (..)) where +module Constrained.Spec.Tree (BinTree (..), TreeFn, rootLabel_, TreeSpec (..)) where -import Control.DeepSeq import Data.Kind +import Data.Tree import GHC.Generics import Test.QuickCheck (shrinkList) @@ -34,18 +35,13 @@ import Constrained.Univ data BinTree a = BinTip | BinNode (BinTree a) a (BinTree a) - deriving (Ord, Eq, Show) - -data RoseTree a = RoseNode a [RoseTree a] deriving (Ord, Eq, Show, Generic) -instance NFData a => NFData (RoseTree a) - ------------------------------------------------------------------------ -- HasSpec for BinTree ------------------------------------------------------------------------ -data BinTreeSpec fn a = BinTreeSpec Integer (Spec fn (BinTree a, a, BinTree a)) +data BinTreeSpec fn a = BinTreeSpec Integer (Specification fn (BinTree a, a, BinTree a)) deriving (Show) instance Forallable (BinTree a) (BinTree a, a, BinTree a) where @@ -106,40 +102,40 @@ instance HasSpec fn a => HasGenHint fn (BinTree a) where giveHint h = typeSpec $ BinTreeSpec h TrueSpec ------------------------------------------------------------------------ --- HasSpec for RoseTree +-- HasSpec for Tree ------------------------------------------------------------------------ -data RoseTreeSpec fn a = RoseTreeSpec +data TreeSpec fn a = TreeSpec { roseTreeAvgLength :: Maybe Integer , roseTreeMaxSize :: Integer - , roseTreeRootSpec :: Spec fn a - , roseTreeCtxSpec :: Spec fn (a, [RoseTree a]) + , roseTreeRootSpec :: Specification fn a + , roseTreeCtxSpec :: Specification fn (a, [Tree a]) } -deriving instance (HasSpec fn a, Member (RoseTreeFn fn) fn) => Show (RoseTreeSpec fn a) +deriving instance (HasSpec fn a, Member (TreeFn fn) fn) => Show (TreeSpec fn a) -instance Forallable (RoseTree a) (a, [RoseTree a]) where - forAllSpec = guardRoseSpec . RoseTreeSpec Nothing 8000 TrueSpec - forAllToList (RoseNode a children) = (a, children) : concatMap forAllToList children +instance Forallable (Tree a) (a, [Tree a]) where + forAllSpec = guardRoseSpec . TreeSpec Nothing 8000 TrueSpec + forAllToList (Node a children) = (a, children) : concatMap forAllToList children -- TODO: get rid of this when we implement `cardinality` -- in `HasSpec` -guardRoseSpec :: HasSpec fn (RoseTree a) => RoseTreeSpec fn a -> Spec fn (RoseTree a) -guardRoseSpec spec@(RoseTreeSpec _ _ rs s) +guardRoseSpec :: HasSpec fn (Tree a) => TreeSpec fn a -> Specification fn (Tree a) +guardRoseSpec spec@(TreeSpec _ _ rs s) | isErrorLike rs = ErrorSpec ["guardRoseSpec: rootSpec is error"] | isErrorLike s = ErrorSpec ["guardRoseSpec: ctxSpec is error"] | otherwise = TypeSpec spec [] -instance (HasSpec fn a, Member (RoseTreeFn fn) fn) => HasSpec fn (RoseTree a) where - type TypeSpec fn (RoseTree a) = RoseTreeSpec fn a +instance (HasSpec fn a, Member (TreeFn fn) fn) => HasSpec fn (Tree a) where + type TypeSpec fn (Tree a) = TreeSpec fn a - emptySpec = RoseTreeSpec Nothing 8000 TrueSpec TrueSpec + emptySpec = TreeSpec Nothing 8000 TrueSpec TrueSpec - combineSpec (RoseTreeSpec mal sz rs s) (RoseTreeSpec mal' sz' rs' s') + combineSpec (TreeSpec mal sz rs s) (TreeSpec mal' sz' rs' s') | isErrorLike (typeSpec (Cartesian rs'' TrueSpec) <> s'') = ErrorSpec [] | otherwise = guardRoseSpec $ - RoseTreeSpec + TreeSpec (unionWithMaybe max mal mal') (min sz sz') rs'' @@ -148,14 +144,14 @@ instance (HasSpec fn a, Member (RoseTreeFn fn) fn) => HasSpec fn (RoseTree a) wh rs'' = rs <> rs' s'' = s <> s' - conformsTo (RoseNode a children) (RoseTreeSpec _ _ rs s) = + conformsTo (Node a children) (TreeSpec _ _ rs s) = and [ (a, children) `conformsToSpec` s - , all (\(RoseNode a' children') -> (a', children') `conformsToSpec` s) children + , all (\(Node a' children') -> (a', children') `conformsToSpec` s) children , a `conformsToSpec` rs ] - genFromTypeSpec (RoseTreeSpec mal sz rs s) = do + genFromTypeSpec (TreeSpec mal sz rs s) = do let sz' = maybe (sz `div` 4) (sz `div`) mal childrenSpec = typeSpec $ @@ -163,40 +159,40 @@ instance (HasSpec fn a, Member (RoseTreeFn fn) fn) => HasSpec fn (RoseTree a) wh (Just sz') [] TrueSpec - (typeSpec $ RoseTreeSpec mal sz' TrueSpec s) + (typeSpec $ TreeSpec mal sz' TrueSpec s) NoFold innerSpec = s <> typeSpec (Cartesian rs childrenSpec) - fmap (uncurry RoseNode) $ - genFromSpec @fn @(a, [RoseTree a]) innerSpec + fmap (uncurry Node) $ + genFromSpec @fn @(a, [Tree a]) innerSpec - shrinkWithTypeSpec (RoseTreeSpec _ _ rs ctxSpec) (RoseNode a ts) = - [RoseNode a [] | not $ null ts] + shrinkWithTypeSpec (TreeSpec _ _ rs ctxSpec) (Node a ts) = + [Node a [] | not $ null ts] ++ ts - ++ [RoseNode a' ts | a' <- shrinkWithSpec rs a] - ++ [RoseNode a [t] | t <- ts] - ++ [ RoseNode a ts' - | ts' <- shrinkList (shrinkWithTypeSpec (RoseTreeSpec Nothing 8000 TrueSpec ctxSpec)) ts + ++ [Node a' ts | a' <- shrinkWithSpec rs a] + ++ [Node a [t] | t <- ts] + ++ [ Node a ts' + | ts' <- shrinkList (shrinkWithTypeSpec (TreeSpec Nothing 8000 TrueSpec ctxSpec)) ts ] - toPreds t (RoseTreeSpec mal sz rs s) = + toPreds t (TreeSpec mal sz rs s) = (forAll t $ \n -> n `satisfies` s) - <> roseRoot_ t `satisfies` rs + <> rootLabel_ t `satisfies` rs <> genHint (mal, sz) t -instance (Member (RoseTreeFn fn) fn, HasSpec fn a) => HasGenHint fn (RoseTree a) where - type Hint (RoseTree a) = (Maybe Integer, Integer) - giveHint (avgLen, sz) = typeSpec $ RoseTreeSpec avgLen sz TrueSpec TrueSpec +instance (Member (TreeFn fn) fn, HasSpec fn a) => HasGenHint fn (Tree a) where + type Hint (Tree a) = (Maybe Integer, Integer) + giveHint (avgLen, sz) = typeSpec $ TreeSpec avgLen sz TrueSpec TrueSpec -data RoseTreeFn (fn :: [Type] -> Type -> Type) args res where - RoseRoot :: RoseTreeFn fn '[RoseTree a] a +data TreeFn (fn :: [Type] -> Type -> Type) args res where + RootLabel :: TreeFn fn '[Tree a] a -deriving instance Eq (RoseTreeFn fn args res) -deriving instance Show (RoseTreeFn fn args res) +deriving instance Eq (TreeFn fn args res) +deriving instance Show (TreeFn fn args res) -instance FunctionLike (RoseTreeFn fn) where - sem RoseRoot = \(RoseNode a _) -> a +instance FunctionLike (TreeFn fn) where + sem RootLabel = \(Node a _) -> a -instance (Member (RoseTreeFn fn) fn, BaseUniverse fn) => Functions (RoseTreeFn fn) fn where +instance (Member (TreeFn fn) fn, BaseUniverse fn) => Functions (TreeFn fn) fn where propagateSpecFun _ _ TrueSpec = TrueSpec propagateSpecFun _ _ (ErrorSpec err) = ErrorSpec err propagateSpecFun _ _ (MemberSpec []) = MemberSpec [] @@ -207,23 +203,23 @@ instance (Member (RoseTreeFn fn) fn, BaseUniverse fn) => Functions (RoseTreeFn f constrained $ \v' -> let args = appendList (mapList (\(Value a) -> Lit a) pre) (v' :> mapList (\(Value a) -> Lit a) suf) in Let (App (injectFn fn) args) (v :-> ps) - RoseRoot -> + RootLabel -> -- No TypeAbstractions in ghc-8.10 case fn of - (_ :: RoseTreeFn fn '[RoseTree a] a) - | NilCtx HOLE <- ctx -> typeSpec $ RoseTreeSpec Nothing 8000 spec TrueSpec + (_ :: TreeFn fn '[Tree a] a) + | NilCtx HOLE <- ctx -> typeSpec $ TreeSpec Nothing 8000 spec TrueSpec -- NOTE: this function over-approximates and returns a liberal spec. mapTypeSpec f ts = case f of - RoseRoot -> + RootLabel -> -- No TypeAbstractions in ghc-8.10 case f of - (_ :: RoseTreeFn fn '[RoseTree a] a) - | RoseTreeSpec _ _ rs _ <- ts -> rs + (_ :: TreeFn fn '[Tree a] a) + | TreeSpec _ _ rs _ <- ts -> rs -roseRoot_ :: +rootLabel_ :: forall fn a. - (Member (RoseTreeFn fn) fn, HasSpec fn a) => - Term fn (RoseTree a) -> + (Member (TreeFn fn) fn, HasSpec fn a) => + Term fn (Tree a) -> Term fn a -roseRoot_ = app (injectFn $ RoseRoot @fn) +rootLabel_ = app (injectFn $ RootLabel @fn) diff --git a/libs/constrained-generators/src/Constrained/Test.hs b/libs/constrained-generators/src/Constrained/Test.hs deleted file mode 100644 index bc8840227a7..00000000000 --- a/libs/constrained-generators/src/Constrained/Test.hs +++ /dev/null @@ -1,896 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE FunctionalDependencies #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE ImportQualifiedPost #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE NumericUnderscores #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} -{-# OPTIONS_GHC -Wno-orphans #-} - -module Constrained.Test where - -import Data.Int -import Data.Map (Map) -import Data.Set (Set) -import Data.Set qualified as Set -import Data.Typeable -import Data.Word -import GHC.Generics -import GHC.Natural -import Test.QuickCheck hiding (Args, Fun, forAll) -import Test.QuickCheck qualified as QC -import Test.Tasty -import Test.Tasty.QuickCheck (testProperty) - -import Constrained.Internals - --- Properties ------------------------------------------------------------- - -prop_conformEmpty :: - forall fn a. - HasSpec fn a => - a -> - Property -prop_conformEmpty a = property $ conformsTo @fn a (emptySpec @fn @a) - -prop_propagateSpec :: - (HasSpec fn a, HasSpec fn b) => - Var b -> - Term fn a -> - Spec fn a -> - Property -prop_propagateSpec var tm spec = - let spec' = errorGE $ do - ctx <- toCtx var tm - pure $ propagateSpec spec ctx - in QC.forAll (strictGen $ genFromSpec spec') $ \geval -> fromGE (\err -> counterexample (unlines err) False) $ do - val <- geval - res <- runTerm (singletonEnv var val) tm - pure $ property $ conformsToSpec res spec - -prop_mapSpec :: - ( HasSpec fn a - , HasSpec fn b - ) => - fn '[a] b -> - Spec fn a -> - Property -prop_mapSpec fn spec = - QC.forAll (strictGen $ genFromSpec spec) $ \ma -> fromGEDiscard $ do - a <- ma - pure $ conformsToSpec (sem fn a) (mapSpec fn spec) - -prop_genInverse :: - ( HasSpec fn a - , HasSpec fn b - ) => - fn '[a] b -> - Spec fn a -> - b -> - Property -prop_genInverse fn spec b = - QC.forAll (strictGen $ genInverse fn spec b) $ \ma -> fromGEDiscard $ do - a <- ma - pure $ conformsToSpec a spec && sem fn a == b - -prop_sound :: - HasSpec fn a => - Spec fn a -> - Property -prop_sound spec = - QC.forAllBlind (strictGen $ genFromSpec spec) $ \ma -> - case ma of - Result _ a -> cover 80 True "successful" $ counterexample (show a) $ conformsToSpecProp a spec - _ -> cover 80 False "successful" True - --- | `prop_complete ps` assumes that `ps` is satisfiable -prop_complete :: HasSpec fn a => Spec fn a -> Property -prop_complete s = - QC.forAllBlind (strictGen $ genFromSpec s) $ \ma -> fromGEProp $ do - a <- ma - -- Force the value to make sure we don't crash with `error` somewhere - -- or fall into an inifinite loop - pure $ length (show a) > 0 - -prop_shrink_sound :: HasSpec fn a => Spec fn a -> Property -prop_shrink_sound s = - QC.forAll (strictGen $ genFromSpec s) $ \ma -> fromGEDiscard $ do - a <- ma - let shrinks = shrinkWithSpec s a - pure $ - cover 40 (not $ null shrinks) "non-null shrinks" $ - if null shrinks - then property True - else QC.forAll (QC.elements shrinks) $ \a' -> - conformsToSpecProp a' s - --- Test suite ------------------------------------------------------------- - -genTest :: HasSpec BaseFn a => Spec BaseFn a -> IO a -genTest = fmap errorGE . generate . strictGen . genFromSpec - -testAll :: IO () -testAll = defaultMain tests - -tests :: TestTree -tests = - testGroup "constrained" $ - [ testSpec "setSpec" setSpec - , testSpec "leqPair" leqPair - , testSpec "setPair" setPair - , testSpecNoShrink "listEmpty" listEmpty - , testSpec "compositionalSpec" compositionalSpec - , testSpec "simplePairSpec" simplePairSpec - , testSpec "trickyCompositional" trickyCompositional - , testSpec "emptyListSpec" emptyListSpec - , testSpec "eitherSpec" eitherSpec - , testSpec "maybeSpec" maybeSpec - , testSpec "eitherSetSpec" eitherSetSpec - , testSpec "fooSpec" fooSpec - , -- TODO: this spec needs double shrinking to shrink properly - -- so we need to figure something out about double-shrinking - testSpecNoShrink "intSpec" intSpec - , testSpec "mapElemSpec" mapElemSpec - , testSpec "mapElemKeySpec" mapElemKeySpec - , testSpec "mapPairSpec" mapPairSpec - , testSpecNoShrink "mapEmptyDomainSpec" mapEmptyDomainSpec - , -- TODO: this _can_ be shrunk, but it's incredibly expensive to do - -- so and it's not obvious if there is a faster way without implementing - -- more detailed shrinking of `SuspendedSpec`s - testSpecNoShrink "setPairSpec" setPairSpec - , testSpec "fixedSetSpec" fixedSetSpec - , testSpec "setOfPairLetSpec" setOfPairLetSpec - , testSpecNoShrink "emptyEitherSpec" emptyEitherSpec - , testSpecNoShrink "emptyEitherMemberSpec" emptyEitherMemberSpec - , testSpec "setSingletonSpec" setSingletonSpec - , testSpec "pairSingletonSpec" pairSingletonSpec - , testSpec "eitherSimpleSetSpec" eitherSimpleSetSpec - , testSpecNoShrink "emptySetSpec" emptySetSpec - , testSpec "forAllAnySpec" forAllAnySpec - , testSpec "notSubsetSpec" notSubsetSpec - , testSpec "maybeJustSetSpec" maybeJustSetSpec - , testSpec "weirdSetPairSpec" weirdSetPairSpec - , testSpec "knownDomainMap" knownDomainMap - , -- TODO: figure out double-shrinking - testSpecNoShrink "testRewriteSpec" testRewriteSpec - , testSpec "parallelLet" parallelLet - , testSpec "letExists" letExists - , testSpec "letExistsLet" letExistsLet - , testSpec "notSubset" notSubset - , testSpec "unionSized" unionSized - , -- TODO: figure out double-shrinking - testSpecNoShrink "dependencyWeirdness" dependencyWeirdness - , testSpec "foldTrueCases" foldTrueCases - , testSpec "foldSingleCase" foldSingleCase - , testSpec "listSumPair" (listSumPair @Int) - , -- TODO: figure out double-shrinking - testSpecNoShrink "parallelLetPair" parallelLetPair - , testSpec "mapSizeConstrained" mapSizeConstrained - , testSpec "allZeroTree" allZeroTree - , testSpec "noChildrenSameTree" noChildrenSameTree - , testSpec "isBST" isBST - , testSpecNoShrink "pairListError" pairListError - , testSpecNoShrink "listMustSizeIssue" listMustSizeIssue - , testSpec "successiveChildren" successiveChildren - , testSpec "successiveChildren8" successiveChildren8 - , testSpecNoShrink "roseTreeList" roseTreeList - , testSpec "orPair" orPair - , testSpec "roseTreePairs" roseTreePairs - , testSpec "roseTreeMaybe" roseTreeMaybe - , testSpec "badTreeInteraction" badTreeInteraction - , testSpec "sumRange" sumRange - , testSpec "sumListBad" sumListBad - , testSpec "listExistsUnfree" listExistsUnfree - , testSpec "existsUnfree" existsUnfree - , numberyTests - , sizeTests - , numNumSpecTree - ] - ++ [ testSpec ("intRangeSpec " ++ show i) (intRangeSpec i) - | i <- [-1000, -100, -10, 0, 10, 100, 1000] - ] - ++ [ testGroup - "prop_conformEmpty" - [ testProperty "Int" $ prop_conformEmpty @BaseFn @Int - , testProperty "Set Int" $ prop_conformEmpty @BaseFn @(Set Int) - , testProperty "Map Int Int" $ prop_conformEmpty @BaseFn @(Map Int Int) - , testProperty "[Int]" $ prop_conformEmpty @BaseFn @[Int] - , testProperty "[(Int, Int)]" $ prop_conformEmpty @BaseFn @[(Int, Int)] - ] - ] - -numberyTests :: TestTree -numberyTests = - testGroup - "numbery tests" - [ testNumberyListSpec "listSum" listSum - , testNumberyListSpecNoShrink "listSumForall" listSumForall - , testNumberyListSpec "listSumRange" listSumRange - , testNumberyListSpec "listSumRangeUpper" listSumRangeUpper - , testNumberyListSpec "listSumRangeRange" listSumRangeRange - , testNumberyListSpec "listSumElemRange" listSumElemRange - ] - -sizeTests :: TestTree -sizeTests = - testGroup "SizeTests" $ - [ testSpecNoShrink "sizeAddOrSub1" sizeAddOrSub1 - , testSpecNoShrink "sizeAddOrSub2" sizeAddOrSub2 - , testSpecNoShrink "sizeAddOrSub3" sizeAddOrSub3 - , testSpecNoShrink "sizeAddOrSub4 returns Negative Size" sizeAddOrSub4 - , testSpecNoShrink "sizeAddOrSub5" sizeAddOrSub5 - , testSpecNoShrink "sizeAddOrSub5" sizeAddOrSub5 - , testSpec "listSubSize" listSubSize - , testSpec "listSubSize" setSubSize - , testSpec "listSubSize" mapSubSize - , testSpec "hasSizeList" hasSizeList - , testSpec "hasSizeSet" hasSizeSet - , testSpec "hasSizeMap" hasSizeMap - ] - -type Numbery a = - ( Foldy BaseFn a - , OrdLike BaseFn a - , NumLike BaseFn a - , Ord a - , Enum a - ) - -data NumberyType where - N :: (Typeable a, Numbery a) => Proxy a -> NumberyType - -testNumberyListSpec :: String -> (forall a. Numbery a => Spec BaseFn [a]) -> TestTree -testNumberyListSpec = testNumberyListSpec' True - -testNumberyListSpecNoShrink :: String -> (forall a. Numbery a => Spec BaseFn [a]) -> TestTree -testNumberyListSpecNoShrink = testNumberyListSpec' False - -testNumberyListSpec' :: Bool -> String -> (forall a. Numbery a => Spec BaseFn [a]) -> TestTree -testNumberyListSpec' withShrink n p = - testGroup - n - [ testSpec' withShrink (show $ typeRep proxy) (p @a) - | N (proxy :: Proxy a) <- numberyTypes - ] - where - numberyTypes = - [ N @Int Proxy - , N @Integer Proxy - , N @Natural Proxy - , N @Word64 Proxy - , N @Word32 Proxy - , N @Word16 Proxy - , N @Word8 Proxy - , N @Int64 Proxy - , N @Int32 Proxy - , N @Int16 Proxy - , N @Int8 Proxy - ] - -testSpec :: HasSpec fn a => String -> Spec fn a -> TestTree -testSpec = testSpec' True - -testSpecNoShrink :: HasSpec fn a => String -> Spec fn a -> TestTree -testSpecNoShrink = testSpec' False - -testSpec' :: HasSpec fn a => Bool -> String -> Spec fn a -> TestTree -testSpec' withShrink n s = do - sequentialTestGroup - n - AllSucceed - $ [testProperty "prop_sound" $ within 10_000_000 $ checkCoverage $ prop_sound s] - ++ [ testProperty "prop_shrink_sound" $ within 10_000_000 $ checkCoverage $ prop_shrink_sound s - | withShrink - ] - --- Examples --------------------------------------------------------------- - -leqPair :: Spec BaseFn (Int, Int) -leqPair = constrained $ \p -> - match p $ \x y -> - x <=. y - -setPair :: Spec BaseFn (Set (Int, Int)) -setPair = constrained $ \s -> - [ forAll s $ \p -> - p `satisfies` leqPair - , assert $ lit (0, 1) `member_` s - ] - -setSpec :: Spec BaseFn (Set Int) -setSpec = constrained $ \ss -> - forAll ss $ \s -> - s <=. 10 - -compositionalSpec :: Spec BaseFn (Set Int) -compositionalSpec = constrained $ \x -> - [ satisfies x setSpec - , assert $ 0 `member_` x - ] - -simplePairSpec :: Spec BaseFn (Int, Int) -simplePairSpec = constrained $ \p -> - match p $ \x y -> - [ x /=. 0 - , y /=. 0 - ] - -trickyCompositional :: Spec BaseFn (Int, Int) -trickyCompositional = constrained $ \p -> - satisfies p simplePairSpec <> assert (fst_ p ==. 1000) - -newtype NotASet a = NotASet (Set a) - deriving (Generic, Show, Eq) -instance Ord a => HasSimpleRep (NotASet a) where - type SimpleRep (NotASet a) = [a] - fromSimpleRep = NotASet . Set.fromList - toSimpleRep (NotASet s) = Set.toList s -instance (Ord a, HasSpec fn a) => HasSpec fn (NotASet a) -instance Ord a => Forallable (NotASet a) a - -emptyListSpec :: Spec BaseFn ([Int], NotASet (Either Int Int, Int)) -emptyListSpec = constrained' $ \is ls -> - [ forAll is $ \i -> i <=. 0 - , forAll' ls $ \l _ -> - caseOn l (branch $ \_ -> False) (branch $ \_ -> False) - ] - -eitherSpec :: Spec BaseFn (Either Int Int) -eitherSpec = constrained $ \e -> - (caseOn e) - (branch $ \i -> i <=. 0) - (branch $ \i -> 0 <=. i) - -maybeSpec :: Spec BaseFn (Set (Maybe Int)) -maybeSpec = constrained $ \ms -> - forAll ms $ \m -> - (caseOn m) - (branch $ \_ -> False) - (branch $ \y -> 0 <=. y) - -eitherSetSpec :: Spec BaseFn (Set (Either Int Int), Set (Either Int Int), Set (Either Int Int)) -eitherSetSpec = constrained' $ \es as bs -> - [ assert $ es ==. (as <> bs) - , forAll as $ \a -> - (caseOn a) - (branch $ \a' -> a' <=. 0) - (branch $ \b' -> 1 <=. b') - , forAll bs $ \b -> - (caseOn b) - (branch $ \_ -> False) - (branch $ \b' -> 1 <=. b') - ] - -data Foo = Foo Int | Bar Int Int - deriving (Show, Eq, Ord, Generic) - -instance HasSimpleRep Foo -instance BaseUniverse fn => HasSpec fn Foo - -fooSpec :: Spec BaseFn Foo -fooSpec = constrained $ \foo -> - (caseOn foo) - (branch $ \i -> 0 <=. i) - (branch $ \i j -> i <=. j) - -intSpec :: Spec BaseFn (Int, Int) -intSpec = constrained' $ \a b -> - reify a (`mod` 10) $ \a' -> b ==. a' - -mapElemSpec :: Spec BaseFn (Map Int (Bool, Int)) -mapElemSpec = constrained $ \m -> - [ assert $ m /=. lit mempty - , forAll' (rng_ m) $ \_ b -> - [0 <. b, b <. 10] - ] - -mapElemKeySpec :: Spec BaseFn Int -mapElemKeySpec = constrained $ \n -> - letBind (pair_ n $ lit (False, 4)) $ \(p :: Term BaseFn (Int, (Bool, Int))) -> - letBind (snd_ (snd_ p)) $ \x -> - [x <. 10, 0 <. x, not_ $ elem_ n $ lit []] - -intRangeSpec :: Int -> Spec BaseFn Int -intRangeSpec a = constrained $ \n -> n <. lit a - -testRewriteSpec :: Spec BaseFn ((Int, Int), (Int, Int)) -testRewriteSpec = constrained' $ \x y -> - x ==. fromGeneric_ (toGeneric_ y) - -mapPairSpec :: Spec BaseFn (Map Int Int, Set Int) -mapPairSpec = constrained' $ \m s -> - subset_ (dom_ m) s - -mapEmptyDomainSpec :: Spec BaseFn (Map Int Int) -mapEmptyDomainSpec = constrained $ \m -> - subset_ (dom_ m) mempty -- mempty in the Monoid instance (Term fn (Set a)) - -setPairSpec :: Spec BaseFn (Set Int, Set Int) -setPairSpec = constrained' $ \s s' -> - forAll s $ \x -> - forAll s' $ \y -> - x <=. y - -fixedSetSpec :: Spec BaseFn (Set Int) -fixedSetSpec = constrained $ \s -> - forAll s $ \x -> - [x <=. lit (i :: Int) | i <- [1 .. 3]] - -setOfPairLetSpec :: Spec BaseFn (Set (Int, Int)) -setOfPairLetSpec = constrained $ \ps -> - forAll' ps $ \x y -> - x <=. y - -setSingletonSpec :: Spec BaseFn (Set (Int, Int)) -setSingletonSpec = constrained $ \ps -> - forAll ps $ \p -> - forAll (singleton_ (fst_ p)) $ \x -> - x <=. 10 - -pairSingletonSpec :: Spec BaseFn (Int, Int) -pairSingletonSpec = constrained $ \q -> - forAll (singleton_ q) $ \p -> - letBind (fst_ p) $ \x -> - letBind (snd_ p) $ \y -> - x <=. y - -eitherSimpleSetSpec :: Spec BaseFn (Set (Either Int Int)) -eitherSimpleSetSpec = constrained $ \ss -> - forAll ss $ \s -> - (caseOn s) - (branch $ \a -> a <=. 0) - (branch $ \b -> 0 <=. b) - -forAllAnySpec :: Spec BaseFn (Set Int) -forAllAnySpec = constrained $ \as -> - forAll as $ \_ -> True - -weirdSetPairSpec :: Spec BaseFn ([Int], Set (Either Int Int)) -weirdSetPairSpec = constrained' $ \as as' -> - [ as' `dependsOn` as - , forAll as $ \a -> - member_ (left_ a) as' - , forAll as' $ \a' -> - (caseOn a') - (branch $ \x -> elem_ x as) - (branch $ \_ -> False) - ] - -maybeJustSetSpec :: Spec BaseFn (Set (Maybe Int)) -maybeJustSetSpec = constrained $ \ms -> - forAll ms $ \m -> - (caseOn m) - (branch $ \_ -> False) - (branch $ \y -> 0 <=. y) - -notSubsetSpec :: Spec BaseFn (Set Int, Set Int) -notSubsetSpec = constrained' $ \s s' -> not_ $ subset_ s s' - -emptySetSpec :: Spec BaseFn (Set Int) -emptySetSpec = constrained $ \s -> - forAll s $ \x -> member_ x mempty - -emptyEitherMemberSpec :: Spec BaseFn (Set (Either Int Int)) -emptyEitherMemberSpec = constrained $ \s -> - forAll s $ \x -> - (caseOn x) - (branch $ \l -> member_ l mempty) - (branch $ \r -> member_ r mempty) - -emptyEitherSpec :: Spec BaseFn (Set (Either Int Int)) -emptyEitherSpec = constrained $ \s -> - forAll s $ \x -> - (caseOn x) - (branch $ \_ -> False) - (branch $ \_ -> False) - -knownDomainMap :: Spec BaseFn (Map Int Int) -knownDomainMap = constrained $ \m -> - [ dom_ m ==. lit (Set.fromList [1, 2]) - , not_ $ 0 `elem_` rng_ m - ] - -parallelLet :: Spec BaseFn (Int, Int) -parallelLet = constrained $ \p -> - [ letBind (fst_ p) $ \x -> 0 <. x - , letBind (snd_ p) $ \x -> x <. 0 - ] - -letExists :: Spec BaseFn (Int, Int) -letExists = constrained $ \p -> - [ letBind (fst_ p) $ \x -> 0 <. x - , exists (\eval -> pure $ snd (eval p)) $ - \x -> - [ x <. 0 - , snd_ p ==. x - ] - ] - -letExistsLet :: Spec BaseFn (Int, Int) -letExistsLet = constrained $ \p -> - [ letBind (fst_ p) $ \x -> 0 <. x - , exists (\eval -> pure $ snd (eval p)) $ - \x -> - [ assert $ x <. 0 - , letBind (snd_ p) $ \y -> - [ x ==. y - , y <. -1 - ] - ] - ] - -notSubset :: Spec BaseFn (Set Int) -notSubset = constrained $ \s -> - not_ $ s `subset_` lit (Set.fromList [1, 2, 3]) - -unionSized :: Spec BaseFn (Set Int) -unionSized = constrained $ \s -> - 10 ==. size_ (s <> lit (Set.fromList [1 .. 8])) - -listSum :: Numbery a => Spec BaseFn [a] -listSum = constrained $ \as -> - 10 <=. sum_ as - -listSumForall :: Numbery a => Spec BaseFn [a] -listSumForall = constrained $ \xs -> - [ forAll xs $ \x -> 1 <. x - , assert $ sum_ xs ==. 20 - ] - -listSumRange :: Numbery a => Spec BaseFn [a] -listSumRange = constrained $ \xs -> - let n = sum_ xs - in [ forAll xs $ \x -> 1 <. x - , assert $ n <. 20 - , assert $ 10 <. n - ] - -listSumRangeUpper :: Numbery a => Spec BaseFn [a] -listSumRangeUpper = constrained $ \xs -> - let n = sum_ xs - in -- All it takes is one big negative number, - -- then we can't get enough small ones to exceed 10 - -- in the number of tries allowed. - -- So we make x relatively large ( <. 12), If its is - -- relatively small ( <. 5), we can get unlucky. - [ forAll xs $ \x -> [x <. 12] - , assert $ n <. 20 - , assert $ 10 <. n - ] - -listSumRangeRange :: Numbery a => Spec BaseFn [a] -listSumRangeRange = constrained $ \xs -> - let n = sum_ xs - in [ forAll xs $ \x -> [1 <. x, x <. 5] - , assert $ n <. 20 - , assert $ 10 <. n - ] - -listSumElemRange :: Numbery a => Spec BaseFn [a] -listSumElemRange = constrained $ \xs -> - let n = sum_ xs - in [ forAll xs $ \x -> [1 <. x, x <. 5] - , assert $ n `elem_` lit [10, 12 .. 20] - ] - -listSumPair :: Numbery a => Spec BaseFn [(a, Int)] -listSumPair = constrained $ \xs -> - [ assert $ foldMap_ (composeFn fstFn toGenericFn) xs ==. 100 - , forAll' xs $ \x y -> [20 <. x, x <. 30, y <. 100] - ] - -listEmpty :: Spec BaseFn [Int] -listEmpty = constrained $ \xs -> - [ forAll xs $ \_ -> False - , assert $ length_ xs <=. 10 - ] - -dependencyWeirdness :: Spec BaseFn (Int, Int, Int) -dependencyWeirdness = constrained' $ \x y z -> - reify (x + y) id $ \zv -> z ==. zv - -foldTrueCases :: Spec BaseFn (Either Int Int) -foldTrueCases = constrained $ \x -> - [ assert $ not_ $ member_ x (lit (Set.fromList [Left 10])) - , letBind (pair_ x (lit (0 :: Int))) $ \p -> - caseOn - (fst_ p) - (branch $ \_ -> True) - (branch $ \_ -> True) - ] - -foldSingleCase :: Spec BaseFn Int -foldSingleCase = constrained $ \x -> - [ assert $ not_ $ member_ x (lit (Set.fromList [10])) - , letBind (pair_ x $ lit [(10, 20) :: (Int, Int)]) $ \p -> - match p $ \_ p1 -> forAll p1 $ \p2 -> - assert (0 <=. snd_ p2) - ] - -parallelLetPair :: Spec BaseFn (Int, Int) -parallelLetPair = constrained $ \p -> - [ match p $ \x y -> - [ assert $ x <=. y - , y `dependsOn` x - ] - , match p $ \x y -> y <=. x - ] - -data Three = One | Two | Three - deriving (Ord, Eq, Show, Generic) - -instance HasSimpleRep Three -instance BaseUniverse fn => HasSpec fn Three - -mapSizeConstrained :: Spec BaseFn (Map Three Int) -mapSizeConstrained = constrained $ \m -> size_ (dom_ m) <=. 3 - -orPair :: Spec BaseFn [(Int, Int)] -orPair = constrained $ \ps -> - forAll' ps $ \x y -> - x <=. 5 ||. y <=. 5 - -allZeroTree :: Spec BaseFn (BinTree Int) -allZeroTree = constrained $ \t -> - [ forAll' t $ \_ a _ -> a ==. 0 - , genHint 10 t - ] - -isBST :: Spec BaseFn (BinTree Int) -isBST = constrained $ \t -> - [ forAll' t $ \left a right -> - -- TODO: if there was a `binTreeRoot` function on trees - -- this wouldn't need to be quadratic as we would - -- only check agains the head of the left and right - -- subtrees, not _every element_ - [ forAll' left $ \_ l _ -> l <. a - , forAll' right $ \_ h _ -> a <. h - ] - , genHint 10 t - ] - -noChildrenSameTree :: Spec BaseFn (BinTree Int) -noChildrenSameTree = constrained $ \t -> - [ forAll' t $ \left a right -> - [ forAll' left $ \_ l _ -> l /=. a - , forAll' right $ \_ r _ -> r /=. a - ] - , genHint 8 t - ] - -type RoseFn = Fix (OneofL (RoseTreeFn : BaseFns)) - -allZeroRoseTree :: Spec RoseFn (RoseTree Int) -allZeroRoseTree = constrained $ \t -> - [ forAll' t $ \a cs -> - [ a ==. 0 - , length_ cs <=. 4 - ] - , genHint (Just 2, 30) t - ] - -noSameChildrenRoseTree :: Spec RoseFn (RoseTree Int) -noSameChildrenRoseTree = constrained $ \t -> - [ forAll' t $ \a cs -> - [ assert $ a `elem_` lit [1 .. 8] - , forAll cs $ \t' -> - forAll' t' $ \b _ -> - b /=. a - ] - , genHint (Just 2, 30) t - ] - -successiveChildren :: Spec RoseFn (RoseTree Int) -successiveChildren = constrained $ \t -> - [ forAll' t $ \a cs -> - [ forAll cs $ \t' -> - roseRoot_ t' ==. a + 1 - ] - , genHint (Just 2, 10) t - ] - -successiveChildren8 :: Spec RoseFn (RoseTree Int) -successiveChildren8 = constrained $ \t -> - [ t `satisfies` successiveChildren - , forAll' t $ \a _ -> a `elem_` lit [1 .. 5] - ] - -roseTreeList :: Spec RoseFn [RoseTree Int] -roseTreeList = constrained $ \ts -> - [ assert $ length_ ts <=. 10 - , forAll ts $ \t -> - [ forAll t $ \_ -> False - ] - ] - -pairListError :: Spec BaseFn [(Int, Int)] -pairListError = constrained $ \ps -> - [ assert $ length_ ps <=. 10 - , forAll' ps $ \a b -> - [ a `elem_` lit [1 .. 8] - , a ==. 9 - , b ==. a - ] - ] - -listMustSizeIssue :: Spec BaseFn [Int] -listMustSizeIssue = constrained $ \xs -> - [ 1 `elem_` xs - , length_ xs ==. 1 - ] - -roseTreePairs :: Spec RoseFn (RoseTree ([Int], [Int])) -roseTreePairs = constrained $ \t -> - [ assert $ roseRoot_ t ==. lit ([1 .. 10], [1 .. 10]) - , forAll' t $ \p ts -> - forAll ts $ \t' -> - fst_ (roseRoot_ t') ==. snd_ p - , genHint (Nothing, 10) t - ] - -roseTreeMaybe :: Spec RoseFn (RoseTree (Maybe (Int, Int))) -roseTreeMaybe = constrained $ \t -> - [ forAll' t $ \mp ts -> - forAll ts $ \t' -> - onJust mp $ \p -> - onJust (roseRoot_ t') $ \p' -> - fst_ p' ==. snd_ p - , forAll' t $ \mp _ -> isJust mp - , genHint (Nothing, 10) t - ] - -sumRange :: Spec BaseFn (Map Word64 Word64) -sumRange = constrained $ \m -> sum_ (rng_ m) ==. lit 10 - -sumListBad :: Spec BaseFn [Word64] -sumListBad = constrained $ \xs -> - [ forAll xs $ \x -> unsafeExists $ \y -> y ==. x - , assert $ sum_ xs ==. lit 10 - ] - -listExistsUnfree :: Spec BaseFn [Int] -listExistsUnfree = constrained $ \xs -> - [ forAll xs $ \x -> x `satisfies` existsUnfree - , assert $ sizeOf_ xs ==. 3 - ] - -existsUnfree :: Spec BaseFn Int -existsUnfree = constrained $ \_ -> exists (\_ -> pure 1) $ \y -> y `elem_` lit [1, 2 :: Int] - -badTreeInteraction :: Spec RoseFn (RoseTree (Either Int Int)) -badTreeInteraction = constrained $ \t -> - [ forAll' t $ \n ts' -> - [ isCon @"Right" n - , forAll ts' $ \_ -> True - ] - , forAll' t $ \n ts' -> - forAll ts' $ \t' -> - [ genHint (Just 4, 10) t' - , assert $ roseRoot_ t' ==. n - ] - , genHint (Just 4, 10) t - ] - -sizeAddOrSub1 :: Spec BaseFn Integer -sizeAddOrSub1 = constrained $ \s -> - 4 ==. s + 2 - -sizeAddOrSub2 :: Spec BaseFn Integer -sizeAddOrSub2 = constrained $ \s -> - 4 ==. 2 + s - -sizeAddOrSub3 :: Spec BaseFn Integer -sizeAddOrSub3 = constrained $ \s -> - 4 ==. s - 2 - --- | We expect a negative Integer, so ltSpec tests for that. -sizeAddOrSub4 :: Spec BaseFn Integer -sizeAddOrSub4 = ltSpec 0 <> (constrained $ \s -> 4 ==. 2 - s) - -sizeAddOrSub5 :: Spec BaseFn Integer -sizeAddOrSub5 = constrained $ \s -> - 2 ==. 12 - s - -listSubSize :: Spec BaseFn [Int] -listSubSize = constrained $ \s -> - 2 ==. 12 - (sizeOf_ s) - -setSubSize :: Spec BaseFn (Set Int) -setSubSize = constrained $ \s -> - 2 ==. 12 - (sizeOf_ s) - -mapSubSize :: Spec BaseFn (Map Int Int) -mapSubSize = constrained $ \s -> - 2 ==. 12 - (sizeOf_ s) - -hasSizeList :: Spec BaseFn [Int] -hasSizeList = hasSize (rangeSize 0 4) - -hasSizeSet :: Spec BaseFn (Set Int) -hasSizeSet = hasSize (rangeSize 1 3) - -hasSizeMap :: Spec BaseFn (Map Int Int) -hasSizeMap = hasSize (rangeSize 1 3) - --- ======================================================== --- Test properties of the instance Num(NumSpec Integer) - -instance Arbitrary (NumSpec Integer) where - arbitrary = do - lo <- arbitrary - hi <- next lo - pure $ NumSpecInterval lo hi - where - next Nothing = arbitrary - next (Just n) = frequency [(1, pure Nothing), (3, Just <$> suchThat arbitrary (> n))] - --- | When we multiply intervals, we get a bounding box, around the possible values. --- When the intervals have infinities, the bounding box can be very loose. In fact the --- order in which we multiply intervals with infinities can affect how loose the bounding box is. --- So ((NegInf, n) * (a, b)) * (c,d) AND (NegInf, n) * ((a, b) * (c,d)) may have different bounding boxes --- To test the associative laws we must have no infinities, and then the associative law will hold. -noInfinity :: Gen (NumSpec Integer) -noInfinity = do - lo <- arbitrary - hi <- suchThat arbitrary (> lo) - pure $ NumSpecInterval (Just lo) (Just hi) - -plusNegate :: NumSpec Integer -> NumSpec Integer -> Property -plusNegate x y = x - y === x + negate y - -commutesNumSpec :: NumSpec Integer -> NumSpec Integer -> Property -commutesNumSpec x y = x + y === y + x - -assocNumSpec :: NumSpec Integer -> NumSpec Integer -> NumSpec Integer -> Property -assocNumSpec x y z = x + (y + z) === (x + y) + z - -commuteTimes :: (NumSpec Integer) -> (NumSpec Integer) -> Property -commuteTimes x y = x * y === y * x - -assocNumSpecTimes :: Gen Property -assocNumSpecTimes = do - x <- noInfinity - y <- noInfinity - z <- noInfinity - pure (x * (y * z) === (x * y) * z) - -negNegate :: NumSpec Integer -> Property -negNegate x = x === negate (negate x) - -scaleNumSpec :: NumSpec Integer -> Property -scaleNumSpec y = y + y === 2 * y - -scaleOne :: NumSpec Integer -> Property -scaleOne y = y === 1 * y - -numNumSpecTree :: TestTree -numNumSpecTree = - testGroup - "Num (NumSpec Integer) properties" - [ testProperty "plusNegate(x - y == x + negate y)" plusNegate - , testProperty "scaleNumSpec(y + y = 2 * y)" scaleNumSpec - , testProperty "scaleOne(y = 1 * y)" scaleOne - , testProperty "negNagate(x = x == negate (negate x))" negNegate - , testProperty "commutesNumSpec(x+y = y+x)" commutesNumSpec - , testProperty "assocNumSpec(x+(y+z) == (x+y)+z)" assocNumSpec - , testProperty "assocNumSpecTimes(x*(y*z) == (x*y)*z)" assocNumSpecTimes - , testProperty "commuteTimes" commuteTimes - ] - --- ========================================================== - -runTestSpec :: HasSpec BaseFn t => Spec BaseFn t -> IO () -runTestSpec spec = defaultMain (testSpec "interactive test with runTestSpec" spec) - -generateSpec :: forall fn a. HasSpec fn a => Spec fn a -> IO a -generateSpec spec = generate (genFromSpec_ @fn spec) diff --git a/libs/constrained-generators/test/Constrained/Test.hs b/libs/constrained-generators/test/Constrained/Test.hs new file mode 100644 index 00000000000..b378cb86f2f --- /dev/null +++ b/libs/constrained-generators/test/Constrained/Test.hs @@ -0,0 +1,276 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Constrained.Test where + +import Control.Monad +import Data.Int +import Data.Map (Map) +import Data.Set (Set) +import Data.Typeable +import Data.Word +import GHC.Natural +import Test.Hspec +import Test.Hspec.QuickCheck +import Test.QuickCheck hiding (Args, Fun, forAll) + +import Constrained.Examples +import Constrained.Internals +import Constrained.Properties + +------------------------------------------------------------------------ +-- Test suite +------------------------------------------------------------------------ + +testAll :: IO () +testAll = hspec tests + +tests :: Spec +tests = + describe "constrained" $ do + testSpec "setSpec" setSpec + testSpec "leqPair" leqPair + testSpec "setPair" setPair + testSpecNoShrink "listEmpty" listEmpty + testSpec "compositionalSpec" compositionalSpec + testSpec "simplePairSpec" simplePairSpec + testSpec "trickyCompositional" trickyCompositional + testSpec "emptyListSpec" emptyListSpec + testSpec "eitherSpec" eitherSpec + testSpec "maybeSpec" maybeSpec + testSpec "eitherSetSpec" eitherSetSpec + testSpec "fooSpec" fooSpec + -- TODO: this spec needs double shrinking to shrink properly + -- so we need to figure something out about double-shrinking + testSpecNoShrink "intSpec" intSpec + testSpec "mapElemSpec" mapElemSpec + testSpec "mapElemKeySpec" mapElemKeySpec + testSpec "mapPairSpec" mapPairSpec + testSpecNoShrink "mapEmptyDomainSpec" mapEmptyDomainSpec + -- TODO: this _can_ be shrunk, but it's incredibly expensive to do + -- so and it's not obvious if there is a faster way without implementing + -- more detailed shrinking of `SuspendedSpec`s + testSpecNoShrink "setPairSpec" setPairSpec + testSpec "fixedSetSpec" fixedSetSpec + testSpec "setOfPairLetSpec" setOfPairLetSpec + testSpecNoShrink "emptyEitherSpec" emptyEitherSpec + testSpecNoShrink "emptyEitherMemberSpec" emptyEitherMemberSpec + testSpec "setSingletonSpec" setSingletonSpec + testSpec "pairSingletonSpec" pairSingletonSpec + testSpec "eitherSimpleSetSpec" eitherSimpleSetSpec + testSpecNoShrink "emptySetSpec" emptySetSpec + testSpec "forAllAnySpec" forAllAnySpec + testSpec "notSubsetSpec" notSubsetSpec + testSpec "maybeJustSetSpec" maybeJustSetSpec + testSpec "weirdSetPairSpec" weirdSetPairSpec + testSpec "knownDomainMap" knownDomainMap + -- TODO: figure out double-shrinking + testSpecNoShrink "testRewriteSpec" testRewriteSpec + testSpec "parallelLet" parallelLet + testSpec "letExists" letExists + testSpec "letExistsLet" letExistsLet + testSpec "notSubset" notSubset + testSpec "unionSized" unionSized + -- TODO: figure out double-shrinking + testSpecNoShrink "dependencyWeirdness" dependencyWeirdness + testSpec "foldTrueCases" foldTrueCases + testSpec "foldSingleCase" foldSingleCase + testSpec "listSumPair" (listSumPair @Int) + -- TODO: figure out double-shrinking + testSpecNoShrink "parallelLetPair" parallelLetPair + testSpec "mapSizeConstrained" mapSizeConstrained + testSpec "isAllZeroTree" isAllZeroTree + testSpec "noChildrenSameTree" noChildrenSameTree + testSpec "isBST" isBST + testSpecNoShrink "pairListError" pairListError + testSpecNoShrink "listMustSizeIssue" listMustSizeIssue + testSpec "successiveChildren" successiveChildren + testSpec "successiveChildren8" successiveChildren8 + testSpecNoShrink "roseTreeList" roseTreeList + testSpec "orPair" orPair + testSpec "roseTreePairs" roseTreePairs + testSpec "roseTreeMaybe" roseTreeMaybe + testSpec "badTreeInteraction" badTreeInteraction + testSpec "sumRange" sumRange + testSpec "sumListBad" sumListBad + testSpec "listExistsUnfree" listExistsUnfree + testSpec "existsUnfree" existsUnfree + numberyTests + sizeTests + numNumSpecTree + sequence_ + [ testSpec ("intRangeSpec " ++ show i) (intRangeSpec i) + | i <- [-1000, -100, -10, 0, 10, 100, 1000] + ] + describe "prop_conformEmpty" $ do + prop "Int" $ prop_conformEmpty @BaseFn @Int + prop "Set Int" $ prop_conformEmpty @BaseFn @(Set Int) + prop "Map Int Int" $ prop_conformEmpty @BaseFn @(Map Int Int) + prop "[Int]" $ prop_conformEmpty @BaseFn @[Int] + prop "[(Int, Int)]" $ prop_conformEmpty @BaseFn @[(Int, Int)] + +numberyTests :: Spec +numberyTests = + describe "numbery tests" $ do + testNumberyListSpec "listSum" listSum + testNumberyListSpecNoShrink "listSumForall" listSumForall + testNumberyListSpec "listSumRange" listSumRange + testNumberyListSpec "listSumRangeUpper" listSumRangeUpper + testNumberyListSpec "listSumRangeRange" listSumRangeRange + testNumberyListSpec "listSumElemRange" listSumElemRange + +sizeTests :: Spec +sizeTests = + describe "SizeTests" $ do + testSpecNoShrink "sizeAddOrSub1" sizeAddOrSub1 + testSpecNoShrink "sizeAddOrSub2" sizeAddOrSub2 + testSpecNoShrink "sizeAddOrSub3" sizeAddOrSub3 + testSpecNoShrink "sizeAddOrSub4 returns Negative Size" sizeAddOrSub4 + testSpecNoShrink "sizeAddOrSub5" sizeAddOrSub5 + testSpecNoShrink "sizeAddOrSub5" sizeAddOrSub5 + testSpec "listSubSize" listSubSize + testSpec "listSubSize" setSubSize + testSpec "listSubSize" mapSubSize + testSpec "hasSizeList" hasSizeList + testSpec "hasSizeSet" hasSizeSet + testSpec "hasSizeMap" hasSizeMap + +data NumberyType where + N :: (Typeable a, Numbery a) => Proxy a -> NumberyType + +testNumberyListSpec :: String -> (forall a. Numbery a => Specification BaseFn [a]) -> Spec +testNumberyListSpec = testNumberyListSpec' True + +testNumberyListSpecNoShrink :: String -> (forall a. Numbery a => Specification BaseFn [a]) -> Spec +testNumberyListSpecNoShrink = testNumberyListSpec' False + +testNumberyListSpec' :: Bool -> String -> (forall a. Numbery a => Specification BaseFn [a]) -> Spec +testNumberyListSpec' withShrink n p = + describe n $ + sequence_ + [ testSpec' withShrink (show $ typeRep proxy) (p @a) + | N (proxy :: Proxy a) <- numberyTypes + ] + where + numberyTypes = + [ N @Int Proxy + , N @Integer Proxy + , N @Natural Proxy + , N @Word64 Proxy + , N @Word32 Proxy + , N @Word16 Proxy + , N @Word8 Proxy + , N @Int64 Proxy + , N @Int32 Proxy + , N @Int16 Proxy + , N @Int8 Proxy + ] + +testSpec :: HasSpec fn a => String -> Specification fn a -> Spec +testSpec = testSpec' True + +testSpecNoShrink :: HasSpec fn a => String -> Specification fn a -> Spec +testSpecNoShrink = testSpec' False + +testSpec' :: HasSpec fn a => Bool -> String -> Specification fn a -> Spec +testSpec' withShrink n s = + describe n $ do + prop "prop_sound" $ within 10_000_000 $ checkCoverage $ prop_sound s + when withShrink $ + prop "prop_shrink_sound" $ + within 10_000_000 $ + checkCoverage $ + prop_shrink_sound s + +------------------------------------------------------------------------ +-- Test properties of the instance Num (NumSpec Integer) +------------------------------------------------------------------------ + +instance Arbitrary (NumSpec Integer) where + arbitrary = do + lo <- arbitrary + hi <- next lo + pure $ NumSpecInterval lo hi + where + next Nothing = arbitrary + next (Just n) = frequency [(1, pure Nothing), (3, Just <$> suchThat arbitrary (> n))] + +-- | When we multiply intervals, we get a bounding box, around the possible values. +-- When the intervals have infinities, the bounding box can be very loose. In fact the +-- order in which we multiply intervals with infinities can affect how loose the bounding box is. +-- So ((NegInf, n) * (a, b)) * (c,d) AND (NegInf, n) * ((a, b) * (c,d)) may have different bounding boxes +-- To test the associative laws we must have no infinities, and then the associative law will hold. +noInfinity :: Gen (NumSpec Integer) +noInfinity = do + lo <- arbitrary + hi <- suchThat arbitrary (> lo) + pure $ NumSpecInterval (Just lo) (Just hi) + +plusNegate :: NumSpec Integer -> NumSpec Integer -> Property +plusNegate x y = x - y === x + negate y + +commutesNumSpec :: NumSpec Integer -> NumSpec Integer -> Property +commutesNumSpec x y = x + y === y + x + +assocNumSpec :: NumSpec Integer -> NumSpec Integer -> NumSpec Integer -> Property +assocNumSpec x y z = x + (y + z) === (x + y) + z + +commuteTimes :: NumSpec Integer -> NumSpec Integer -> Property +commuteTimes x y = x * y === y * x + +assocNumSpecTimes :: Gen Property +assocNumSpecTimes = do + x <- noInfinity + y <- noInfinity + z <- noInfinity + pure (x * (y * z) === (x * y) * z) + +negNegate :: NumSpec Integer -> Property +negNegate x = x === negate (negate x) + +scaleNumSpec :: NumSpec Integer -> Property +scaleNumSpec y = y + y === 2 * y + +scaleOne :: NumSpec Integer -> Property +scaleOne y = y === 1 * y + +numNumSpecTree :: Spec +numNumSpecTree = + describe "Num (NumSpec Integer) properties" $ do + prop "plusNegate(x - y == x + negate y)" plusNegate + prop "scaleNumSpec(y + y = 2 * y)" scaleNumSpec + prop "scaleOne(y = 1 * y)" scaleOne + prop "negNagate(x = x == negate (negate x))" negNegate + prop "commutesNumSpec(x+y = y+x)" commutesNumSpec + prop "assocNumSpec(x+(y+z) == (x+y)+z)" assocNumSpec + prop "assocNumSpecTimes(x*(y*z) == (x*y)*z)" assocNumSpecTimes + prop "commuteTimes" commuteTimes + +------------------------------------------------------------------------ +-- Tests for `hasSize` +------------------------------------------------------------------------ + +hasSizeList :: Specification BaseFn [Int] +hasSizeList = hasSize (rangeSize 0 4) + +hasSizeSet :: Specification BaseFn (Set Int) +hasSizeSet = hasSize (rangeSize 1 3) + +hasSizeMap :: Specification BaseFn (Map Int Int) +hasSizeMap = hasSize (rangeSize 1 3) diff --git a/libs/constrained-generators/test/Tests.hs b/libs/constrained-generators/test/Tests.hs index 0f687446362..acc97d6a388 100644 --- a/libs/constrained-generators/test/Tests.hs +++ b/libs/constrained-generators/test/Tests.hs @@ -2,7 +2,7 @@ module Main where import Constrained.Test -import Test.Tasty +import Test.Hspec main :: IO () -main = defaultMain tests +main = hspec tests