diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,41 @@ +# Releases + +All notable changes to this project will be documented in this file. + +The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), +and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). + +## [0.4.0] - 2025-08-30 + +- Compatibility with GHC 9.2 - 9.12 +- Add `Shaped` and `Produce` instances for `NonEmpty` +- Fix output for non-Unicode locales + +## [0.3.0] - 2019-11-01 + +- Add `Show` instance for `Demand` + +## [0.2.0] - 2018-10-08 + +### Added + +- Expose instrumentation of data structures as a safe interface in the `IO` monad. +- Add monadic folds and unfolds `translateA`, `foldM`, `unfoldM`, and `unzipWithM` to `Test.StrictCheck.Shaped`. + +### Removed + +- Remove the referentially opaque observation primitives in `Test.StrictCheck.Unsafe`. + +### Changed + +- Improve type inference by making `Shape` an injective type family. + +## [0.1.1] - 2018-10-01 + +### Fixed + +- Fix critical semantic [bug #2](https://github.com/kwf/StrictCheck/issues/2) which caused violation of referential transparency when compiling with optimizations on GHC 8.6. + +## [0.1.0] - 2018-06-22 + +First release of StrictCheck. This version matches the reviewed artifact submitted to ICFP, archived on the ACM DL, with the exception of some small documentation tweaks. diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,21 +1,21 @@ -MIT License - -Copyright (c) 2018 Kenneth Foner, Hengchu Zhang, and Leonidas Lampropoulos - -Permission is hereby granted, free of charge, to any person obtaining a copy -of this software and associated documentation files (the "Software"), to deal -in the Software without restriction, including without limitation the rights -to use, copy, modify, merge, publish, distribute, sublicense, and/or sell -copies of the Software, and to permit persons to whom the Software is -furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all -copies or substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR -IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, -FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE -AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER -LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, -OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE -SOFTWARE. +MIT License + +Copyright (c) 2018 Kenneth Foner, Hengchu Zhang, and Leonidas Lampropoulos + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,10 +1,12 @@ - # StrictCheck: Keep Your Laziness In Check - - StrictCheck is a property-based random testing framework for - observing, specifying, and testing the strictness behaviors of Haskell - functions. Strictness behavior is traditionally considered a non-functional - property; StrictCheck allows it to be tested as if it were one, by reifying - demands on data structures so they can be manipulated and examined within - Haskell. - - For details, see the library on Hackage: . +# StrictCheck: Keep Your Laziness In Check + +[![Hackage](https://img.shields.io/hackage/v/StrictCheck.svg)](https://hackage.haskell.org/package/StrictCheck) + +StrictCheck is a property-based random testing framework for +observing, specifying, and testing the strictness behaviors of Haskell +functions. Strictness behavior is traditionally considered a non-functional +property; StrictCheck allows it to be tested as if it were one, by reifying +demands on data structures so they can be manipulated and examined within +Haskell. + +For details, see the library on Hackage: . diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -1,2 +1,2 @@ -import Distribution.Simple -main = defaultMain +import Distribution.Simple +main = defaultMain diff --git a/StrictCheck.cabal b/StrictCheck.cabal --- a/StrictCheck.cabal +++ b/StrictCheck.cabal @@ -1,86 +1,84 @@ -name: StrictCheck -version: 0.3.0 -synopsis: StrictCheck: Keep Your Laziness In Check -description: StrictCheck is a property-based random testing framework for - observing, specifying, and testing the strictness behaviors of Haskell - functions. Strictness behavior is traditionally considered a non-functional - property; StrictCheck allows it to be tested as if it were one, by reifying - demands on data structures so they can be manipulated and examined within - Haskell. -homepage: https://github.com/kwf/StrictCheck#readme -license: MIT -license-file: LICENSE -author: Kenneth Foner, Hengchu Zhang, and Leo Lampropoulos -maintainer: kwf@very.science -copyright: (c) 2018 Kenneth Foner, Hengchu Zhang, and Leo Lampropoulos -category: Testing -build-type: Simple -cabal-version: >=1.10 -extra-source-files: README.md - -source-repository this - type: git - branch: master - tag: master - location: https://github.com/kwf/StrictCheck - -library - hs-source-dirs: src - default-language: Haskell2010 - build-depends: base >= 4.7 && < 5, - QuickCheck >= 2.10 && < 2.12, - containers >= 0.5 && < 0.7, - generics-sop >= 0.3.2 && < 0.4, - bifunctors >= 5.5 && < 5.6, - template-haskell >= 2.12 && < 2.15 - exposed-modules: Test.StrictCheck - Test.StrictCheck.Curry, - Test.StrictCheck.Consume, - Test.StrictCheck.Produce, - Test.StrictCheck.Demand, - Test.StrictCheck.Observe, - Test.StrictCheck.Observe.Unsafe, - Test.StrictCheck.Shaped, - Test.StrictCheck.Shaped.Flattened, - Test.StrictCheck.Internal.Inputs, - Test.StrictCheck.Internal.Unevaluated, - Test.StrictCheck.Internal.Shrink, - Test.StrictCheck.Internal.Omega, - Test.StrictCheck.TH, - Test.StrictCheck.Examples.Lists, - Test.StrictCheck.Examples.Map - default-extensions: DataKinds, GADTs, BangPatterns, TypeFamilies, RankNTypes, - AllowAmbiguousTypes, DefaultSignatures, TypeApplications, - ScopedTypeVariables, FlexibleContexts, - UndecidableInstances, ConstraintKinds, DeriveFunctor, - FlexibleInstances, StandaloneDeriving, DeriveGeneric, - DeriveAnyClass, TypeOperators, PolyKinds, - GeneralizedNewtypeDeriving, - ViewPatterns, LambdaCase, TupleSections, ImplicitParams, - NamedFieldPuns, PatternSynonyms - ghc-options: -Wall -Wno-unticked-promoted-constructors - -Wredundant-constraints - -test-suite test-strictcheck - type: exitcode-stdio-1.0 - hs-source-dirs: tests - main-is: Tests.hs - other-modules: Specs, RefTrans - default-language: Haskell2010 - default-extensions: DataKinds, GADTs, BangPatterns, TypeFamilies, RankNTypes, - AllowAmbiguousTypes, UndecidableInstances, - DefaultSignatures, TypeApplications, ScopedTypeVariables, - FlexibleContexts, ConstraintKinds, DeriveFunctor, - FlexibleInstances, StandaloneDeriving, DeriveGeneric, - DeriveAnyClass, TypeOperators, PolyKinds, LambdaCase, - TupleSections, TypeFamilyDependencies, - MultiParamTypeClasses, - GeneralizedNewtypeDeriving, ViewPatterns, - PatternSynonyms - ghc-options: -Wall -fno-warn-unused-imports -O2 - build-depends: base, - HUnit, - generics-sop, - deepseq, - StrictCheck, - QuickCheck +name: StrictCheck +version: 0.4.0 +synopsis: StrictCheck: Keep Your Laziness In Check +description: StrictCheck is a property-based random testing framework for + observing, specifying, and testing the strictness behaviors of Haskell + functions. Strictness behavior is traditionally considered a non-functional + property; StrictCheck allows it to be tested as if it were one, by reifying + demands on data structures so they can be manipulated and examined within + Haskell. +homepage: https://github.com/kwf/StrictCheck#readme +license: MIT +license-file: LICENSE +author: Kenneth Foner, Hengchu Zhang, and Leo Lampropoulos +maintainer: lysxia@gmail.com +copyright: (c) 2018 Kenneth Foner, Hengchu Zhang, and Leo Lampropoulos +category: Testing +build-type: Simple +cabal-version: 2.0 +extra-doc-files: README.md, CHANGELOG.md +tested-with: GHC == 9.12.2, GHC == 9.6.7, GHC == 9.2.8 + +source-repository this + type: git + branch: master + tag: master + location: https://github.com/kwf/StrictCheck + +library + hs-source-dirs: src + default-language: Haskell2010 + build-depends: base >= 4.7 && < 5, + template-haskell >= 2.18 && < 2.24, + QuickCheck >= 2.10 && < 2.17, + containers >= 0.5 && < 0.9, + generics-sop >= 0.3.2 && < 0.6, + bifunctors >= 5.5 && < 5.7 + exposed-modules: Test.StrictCheck + Test.StrictCheck.Curry, + Test.StrictCheck.Consume, + Test.StrictCheck.Produce, + Test.StrictCheck.Demand, + Test.StrictCheck.Observe, + Test.StrictCheck.Observe.Unsafe, + Test.StrictCheck.Shaped, + Test.StrictCheck.Shaped.Flattened, + Test.StrictCheck.Internal.Inputs, + Test.StrictCheck.Internal.Unevaluated, + Test.StrictCheck.Internal.Shrink, + Test.StrictCheck.Internal.Omega, + Test.StrictCheck.TH, + Test.StrictCheck.Examples.Lists, + Test.StrictCheck.Examples.Map + default-extensions: DataKinds, GADTs, BangPatterns, TypeFamilies, RankNTypes, + AllowAmbiguousTypes, DefaultSignatures, TypeApplications, + ScopedTypeVariables, FlexibleContexts, + UndecidableInstances, ConstraintKinds, DeriveFunctor, + FlexibleInstances, StandaloneDeriving, DeriveGeneric, + DeriveAnyClass, TypeOperators, PolyKinds, + GeneralizedNewtypeDeriving, + ViewPatterns, LambdaCase, TupleSections, ImplicitParams, + NamedFieldPuns, PatternSynonyms + ghc-options: -Wall -Wno-unticked-promoted-constructors + -Wredundant-constraints + +test-suite test-strictcheck + type: exitcode-stdio-1.0 + hs-source-dirs: tests + main-is: Tests.hs + other-modules: Specs, RefTrans + default-language: Haskell2010 + default-extensions: DataKinds, GADTs, BangPatterns, TypeFamilies, RankNTypes, + AllowAmbiguousTypes, UndecidableInstances, + DefaultSignatures, TypeApplications, ScopedTypeVariables, + FlexibleContexts, ConstraintKinds, DeriveFunctor, + FlexibleInstances, StandaloneDeriving, DeriveGeneric, + DeriveAnyClass, TypeOperators, PolyKinds, LambdaCase, + TupleSections, TypeFamilyDependencies, + MultiParamTypeClasses, + GeneralizedNewtypeDeriving, ViewPatterns, + PatternSynonyms + ghc-options: -Wall -fno-warn-unused-imports + build-depends: base, + StrictCheck, + QuickCheck diff --git a/src/Test/StrictCheck.hs b/src/Test/StrictCheck.hs --- a/src/Test/StrictCheck.hs +++ b/src/Test/StrictCheck.hs @@ -1,514 +1,572 @@ -{-| The top-level interface to the StrictCheck library for random strictness - testing. - - __Quick Start:__ - - Want to explore the strictness of functions before you write specifications? - Go to "Test.StrictCheck.Observe" and look at the functions 'observe1' and - 'observe'. - - Want to check the strictness of a function against a specification of its - strictness? - - 1. Write a 'Spec' describing your expectation of the function's behavior. - See "Test.StrictCheck.Demand" for more on working with demands, and - "Test.StrictCheck.Examples.Lists" for examples of some specifications of - functions on lists. - 2. Check your function using 'strictCheckSpecExact', like so: - - > strictCheckSpecExact spec function - - If your function passes testing, you'll get a success message just like in - "Test.QuickCheck"; if a counterexample to your specification is found, you - will see a pretty Unicode box diagram describing the mismatch. - - __Hint:__ StrictCheck, just like QuickCheck, doesn't work with polymorphic - functions. If you get baffling type errors, first make sure that all your - types are totally concrete. --} - -{-# language DerivingStrategies #-} - -module Test.StrictCheck - ( -- * Specifying demand behavior - Spec(..) - , getSpec - -- * Checking specifications - , StrictCheck - , strictCheckSpecExact - , strictCheckWithResults - -- * Providing arguments for 'strictCheckWithResults' - , genViaProduce - , Shrink(..) - , shrinkViaArbitrary - , Strictness - , strictnessViaSized - -- * Representing individual evaluations of functions - , Evaluation(..) - , evaluationForall - , shrinkEvalWith - -- * Comparing demands - , DemandComparison(..) - , compareToSpecWith - , equalToSpec - -- * Re-exported n-ary products from "Generics.SOP" - , NP(..), I(..), All - -- * Re-exports of the rest of the library - , module Test.StrictCheck.Demand - , module Test.StrictCheck.Observe - , module Test.StrictCheck.Produce - , module Test.StrictCheck.Consume - , module Test.StrictCheck.Shaped - ) - where - -import Test.StrictCheck.Curry as Curry -import Test.StrictCheck.Produce -import Test.StrictCheck.Consume -import Test.StrictCheck.Observe -import Test.StrictCheck.Demand -import Test.StrictCheck.Shaped - -import Test.StrictCheck.Internal.Omega -import Test.StrictCheck.Internal.Shrink - ( Shrink(..), axialShrinks, fairInterleave ) - -import Generics.SOP hiding (Shape) - -import Test.QuickCheck as Exported hiding (Args, Result, function) -import qualified Test.QuickCheck as QC - -import Data.List -import Data.Maybe -import Data.IORef -import Type.Reflection - --- | The default comparison of demands: exact equality -compareEquality :: All Shaped xs => NP DemandComparison xs -compareEquality = hcpure (Proxy @Shaped) (DemandComparison (==)) - --- | The default way to generate inputs: via 'Produce' -genViaProduce :: All Produce xs => NP Gen xs -genViaProduce = hcpure (Proxy @Produce) (freely produce) - --- | The default way to shrink inputs: via 'shrink' (from "Test.QuickCheck"'s --- 'Arbitrary' typeclass) -shrinkViaArbitrary :: All Arbitrary xs => NP Shrink xs -shrinkViaArbitrary = hcpure (Proxy @Arbitrary) (Shrink shrink) - --- | The default way to generate random strictnesses: uniformly choose between --- 1 and the test configuration's @size@ parameter -strictnessViaSized :: Gen Strictness -strictnessViaSized = - Strictness <$> (choose . (1,) =<< getSize) - --- | A newtype for wrapping a comparison on demands --- --- This is useful when constructing an 'NP' n-ary product of such comparisons. -newtype DemandComparison a = - DemandComparison (Demand a -> Demand a -> Bool) - --- | A demand specification for some function @f@ is itself a function which --- manipulates demand values for some function's arguments and results --- --- A @Spec@ for @f@ wraps a function which takes, in order: --- --- * a continuation @predict@ which accepts all of @f@'s argument types in order, --- * an implicit representation of a demand on @f@'s result (embedded in @f@'s --- actual result type using special bottom values, see the documentation for --- "Test.StrictCheck.Demand" for details), and --- * all of @f@'s original arguments in order --- --- The intention is that the @Spec@ will call @predict@ on some set of demands --- representing the demands it predicts that @f@ will exert on its inputs, --- given the provided demand on @f@'s outputs. --- --- For example, here is a correct @Spec@ for 'take': --- --- > take_spec :: Spec '[Int, [a]] [a] --- > take_spec = --- > Spec $ \predict d n xs -> --- > predict n (if n > length xs then d else d ++ thunk) --- --- See the documentation for "Test.StrictCheck.Demand" for information about how --- to manipulate these implicit demand representations when writing @Spec@s, and --- see the documentation for "Test.StrictCheck.Examples.Lists" for more examples --- of writing specifications. -newtype Spec (args :: [*]) (result :: *) - = Spec (forall r. (args ⋯-> r) -> result -> args ⋯-> r) - --- | Unwrap a @Spec@ constructor, returning the contained CPS-ed specification --- --- Conceptually, this is the inverse to the @Spec@ constructor, but because --- @Spec@ is variadic, @getSpec . Spec@ and @Spec . getSpec@ don't typecheck --- without additional type annotation. -getSpec - :: forall r args result. - Spec args result - -> (args ⋯-> r) - -> result - -> args ⋯-> r -getSpec (Spec s) k d = s @r k d - --- | Given a list of ways to compare demands, a demand specification, and an --- evaluation of a particular function, determine if the function met the --- specification, as decided by the comparisons. If so, return the prediction --- of the specification. -compareToSpecWith - :: forall args result. - (All Shaped args, Curry args, Shaped result) - => NP DemandComparison args - -> Spec args result - -> Evaluation args result - -> Maybe (NP Demand args) -compareToSpecWith comparisons spec (Evaluation inputs inputsD resultD) = - let prediction = - Curry.uncurry - (getSpec @(NP Demand args) - spec - collectDemands - (fromDemand $ E resultD)) - inputs - correct = - all id . hcollapse $ - hcliftA3 (Proxy @Shaped) - (\(DemandComparison c) iD iD' -> K $ iD `c` iD') - comparisons - inputsD - prediction - in if correct then Nothing else Just prediction - where - collectDemands :: args ⋯-> NP Demand args - collectDemands = - curryCollect @args (hcmap (Proxy @Shaped) (toDemand . unI)) - -curryCollect - :: forall (xs :: [*]) r. Curry xs => (NP I xs -> r) -> xs ⋯-> r -curryCollect k = Curry.curry @xs k - --- | Checks if a given 'Evaluation' exactly matches the prediction of a given --- 'Spec', returning the prediction of that @Spec@ if not --- --- __Note:__ In the case of __success__ this returns @Nothing@; in the case of --- __failure__ this returns @Just@ the incorrect prediction. -equalToSpec - :: forall args result. - (All Shaped args, Shaped result, Curry args) - => Spec args result - -> Evaluation args result - -> Maybe (NP Demand args) -equalToSpec spec e = - compareToSpecWith compareEquality spec e - --- | A @Strictness@ represents (roughly) how strict a randomly generated --- function or evaluation context should be --- --- An evaluation context generated with some strictness @s@ (i.e. through --- 'evaluationForall') will consume at most @s@ constructors of its input, --- although it might consume fewer. -newtype Strictness - = Strictness Int - deriving stock (Eq, Ord) - deriving newtype (Show, Num) - --- | A function can be checked against a specification if it meets the --- @StrictCheck@ constraint -type StrictCheck function = - ( Shaped (Result function) - , Consume (Result function) - , Curry (Args function) - , All Typeable (Args function) - , All Shaped (Args function) ) - --- | The most general function for random strictness testing: all of the more --- convenient such functions can be derived from this one --- --- Given some function @f@, this takes as arguments: --- --- * A 'QC.Args' record describing arguments to pass to the underlying --- QuickCheck engine --- * An 'NP' n-ary product of 'Shrink' shrinkers, one for each argument of @f@ --- * An 'NP' n-ary product of 'Gen' generators, one for each argument of @f@ --- * A 'Gen' generator for strictnesses to be tested --- * A predicate on 'Evaluation's: if the 'Evaluation' passes the predicate, --- it should return @Nothing@; otherwise, it should return @Just@ some --- @evidence@ representing the failure (when checking 'Spec's, this evidence --- comes in the form of a @Spec@'s (incorrect) prediction) --- * the function @f@ to be tested --- --- If all tests succeed, @(Nothing, result)@ is returned, where @result@ is the --- underlying 'QC.Result' type from "Test.QuickCheck". If there is a test --- failure, it also returns @Just@ the failed 'Evaluation' as well as whatever --- @evidence@ was produced by the predicate. -strictCheckWithResults :: - forall function evidence. - StrictCheck function - => QC.Args - -> NP Shrink (Args function) -- TODO: allow dependent shrinking - -> NP Gen (Args function) -- TODO: allow dependent generation - -> Gen Strictness - -> (Evaluation (Args function) (Result function) -> Maybe evidence) - -> function - -> IO ( Maybe ( Evaluation (Args function) (Result function) - , evidence ) - , QC.Result ) -strictCheckWithResults - qcArgs shrinks gens strictness predicate function = do - ref <- newIORef Nothing - result <- - quickCheckWithResult qcArgs{chatty = False{-, maxSuccess = 10000-}} $ - forAllShrink - (evaluationForall @function gens strictness function) - (shrinkEvalWith @function shrinks function) $ - \example -> - case predicate example of - Nothing -> - property True - Just evidence -> - whenFail (writeIORef ref $ Just (example, evidence)) False - readIORef ref >>= \case - Nothing -> pure (Nothing, result) - Just example -> pure (Just example, result) - --- | Check a function to see whether it exactly meets a strictness specification --- --- If the function fails to meet the specification, a counterexample is --- pretty-printed in a box-drawn diagram illustrating how the specification --- failed to match the real observed behavior of the function. -strictCheckSpecExact - :: forall function. - ( StrictCheck function - , All Arbitrary (Args function) - , All Produce (Args function) - ) => Spec (Args function) (Result function) - -> function - -> IO () -strictCheckSpecExact spec function = - do (maybeExample, result) <- - strictCheckWithResults - stdArgs - shrinkViaArbitrary - genViaProduce - strictnessViaSized - (equalToSpec spec) - function - (putStrLn . head . lines) (output result) - case maybeExample of - Nothing -> return () - Just example -> - putStrLn (Prelude.uncurry displayCounterSpec example) - ------------------------------------------------------------- --- An Evaluation is what we generate when StrictCheck-ing -- ------------------------------------------------------------- - --- | A snapshot of the observed strictness behavior of a function --- --- An @Evaluation@ contains the 'inputs' at which a function was called, the --- 'inputDemands' which were induced upon those inputs, and the 'resultDemand' --- which induced that demand on the inputs. -data Evaluation args result = - Evaluation - { inputs :: NP I args -- ^ Inputs to a function - , inputDemands :: NP Demand args -- ^ Demands on the input - , resultDemand :: PosDemand result -- ^ Demand on the result - } - -instance (All Typeable args, Typeable result) - => Show (Evaluation args result) where - show _ = - " :: Evaluation" - ++ " '[" ++ intercalate ", " argTypes ++ "]" - ++ " " ++ show (typeRep :: TypeRep result) - where - argTypes :: [String] - argTypes = - hcollapse - $ hliftA (K . show) - $ (hcpure (Proxy @Typeable) typeRep :: NP TypeRep args) - - ------------------------------------ --- Generating random evaluations -- ------------------------------------ - --- | Given a list of generators for a function's arguments and a generator for --- random strictnesses (measured in number of constructors evaluated), create --- a generator for random 'Evaluation's of that function in random contexts -evaluationForall - :: forall f. - ( Curry (Args f) - , Consume (Result f) - , Shaped (Result f) - , All Shaped (Args f) - ) => NP Gen (Args f) - -> Gen Strictness - -> f - -> Gen (Evaluation (Args f) (Result f)) -evaluationForall gens strictnessGen function = do - inputs <- hsequence gens - strictness <- strictnessGen - toOmega <- freely produce - return (go strictness toOmega inputs) - where - -- If context is fully lazy, increase strictness until it forces something - go :: Strictness - -> (Result f -> Omega) - -> NP I (Args f) - -> Evaluation (Args f) (Result f) - go (Strictness s) tO is = - let (resultD, inputsD) = - observeNP (forceOmega s . tO) (uncurryAll @f function) is - in case resultD of - T -> go (Strictness s + 1) tO is - E posResultD -> - Evaluation is inputsD posResultD - - ---------------------------- --- Shrinking evaluations -- ---------------------------- - --- | Given a shrinker for each of the arguments of a function, the function --- itself, and some 'Evaluation' of that function, produce a list of smaller --- @Evaluation@s of that function -shrinkEvalWith - :: forall f. - ( Curry (Args f) - , Shaped (Result f) - , All Shaped (Args f) - ) => NP Shrink (Args f) - -> f - -> Evaluation (Args f) (Result f) - -> [Evaluation (Args f) (Result f)] -shrinkEvalWith - shrinks (uncurryAll -> function) (Evaluation inputs _ resultD) = - let shrunkDemands = shrinkDemand @(Result f) resultD - shrunkInputs = fairInterleave (axialShrinks shrinks inputs) - shrinkingDemand = mapMaybe (reObserve inputs) shrunkDemands - shrinkingInputs = mapMaybe (flip reObserve resultD) shrunkInputs - in fairInterleave [ shrinkingDemand, shrinkingInputs ] - where - reObserve - :: NP I (Args f) - -> PosDemand (Result f) - -> Maybe (Evaluation (Args f) (Result f)) - reObserve is rD = - let (rD', isD) = observeNP (evaluateDemand rD) function is - in fmap (Evaluation is isD) $ - case rD' of - T -> Nothing - E pos -> Just pos - - --- | Render a counter-example to a specification (that is, an 'Evaluation' --- paired with some expected input demands it doesn't match) as a Unicode --- box-drawing sketch -displayCounterSpec - :: forall args result. - (Shaped result, All Shaped args) - => Evaluation args result - -> NP Demand args - -> String -displayCounterSpec (Evaluation inputs inputsD resultD) predictedInputsD = - beside inputBox (" " : "───" : repeat " ") resultBox - ++ (flip replicate ' ' $ - (2 `max` (subtract 2 $ (lineMax [inputString] `div` 2)))) - ++ "🡓 🡓 🡓\n" - ++ beside - actualBox - (" " : " " : " ═╱═ " : repeat " ") - predictedBox - where - inputBox = - box "┌" '─' "┐" - "│" inputHeader "├" - "├" '─' "┤" - "│" inputString "│" - "└" '─' "┘" - - resultBox = - box "┌" '─' "┐" - "┤" resultHeader "│" - "├" '─' "┤" - "│" resultString "│" - "└" '─' "┘" - - actualBox = - box "┌" '─' "┐" - "│" actualHeader "│" - "├" '─' "┤" - "│" actualDemandString "│" - "└" '─' "┘" - - predictedBox = - box "┌" '─' "┐" - "│" predictedHeader "│" - "├" '─' "┤" - "│" predictedDemandString "│" - "└" '─' "┘" - - inputHeader = " Input" ++ plural - resultHeader = " Demand on result" - actualHeader = " Actual input demand" ++ plural - predictedHeader = " Spec's input demand" ++ plural - - inputString = - showBulletedNPWith @Shaped (prettyDemand . interleave Eval . unI) inputs - resultString = " " ++ prettyDemand @result (E resultD) - actualDemandString = - showBulletedNPWith @Shaped prettyDemand inputsD - predictedDemandString = - showBulletedNPWith @Shaped prettyDemand predictedInputsD - - rule w l c r = frame w l (replicate w c) r ++ "\n" - - frame w before str after = - before ++ str - ++ (replicate (w - length str) ' ') - ++ after - - frames w before para after = - unlines $ map (\str -> frame w before str after) (lines para) - - beside l cs r = - unlines . take (length ls `max` length rs) $ - zipWith3 - (\x c y -> x ++ c ++ y) - (ls ++ repeat (replicate (lineMax [l]) ' ')) - cs - (rs ++ repeat "") - where - ls = lines l - rs = lines r - - box top_l top top_r - header_l header header_r - div_l div_c div_r - body_l body body_r - bottom_l bottom bottom_r = - let w = lineMax [header, body] - in rule w top_l top top_r - ++ frames w header_l header header_r - ++ rule w div_l div_c div_r - ++ frames w body_l body body_r - ++ rule w bottom_l bottom bottom_r - - lineMax strs = - (maximum . map - (\(lines -> ls) -> maximum (map length ls) + 1) $ strs) - - plural = case inputs of - (_ :* Nil) -> "" - _ -> "s" - - showBulletedNPWith - :: forall c g xs. All c xs - => (forall x. c x => g x -> String) -> NP g xs -> String - -- showBulletedNPWith display (x :* Nil) = " " ++ display x ++ "\n" - showBulletedNPWith display list = showNPWith' list - where - showNPWith' :: forall ys. All c ys => NP g ys -> String - showNPWith' Nil = "" - showNPWith' (y :* ys) = - " • " ++ display y ++ "\n" ++ showNPWith' ys +{-| The top-level interface to the StrictCheck library for random strictness + testing. + + __Quick Start:__ + + Want to explore the strictness of functions before you write specifications? + Go to "Test.StrictCheck.Observe" and look at the functions 'observe1' and + 'observe'. + + Want to check the strictness of a function against a specification of its + strictness? + + 1. Write a 'Spec' describing your expectation of the function's behavior. + See "Test.StrictCheck.Demand" for more on working with demands, and + "Test.StrictCheck.Examples.Lists" for examples of some specifications of + functions on lists. + 2. Check your function using 'strictCheckSpecExact', like so: + + > strictCheckSpecExact spec function + + If your function passes testing, you'll get a success message just like in + "Test.QuickCheck"; if a counterexample to your specification is found, you + will see a pretty Unicode box diagram describing the mismatch. + + __Hint:__ StrictCheck, just like QuickCheck, doesn't work with polymorphic + functions. If you get baffling type errors, first make sure that all your + types are totally concrete. +-} + +{-# language DerivingStrategies #-} + +module Test.StrictCheck + ( -- * Specifying demand behavior + Spec(..) + , getSpec + -- * Checking specifications + , StrictCheck + , strictCheckSpecExact + , strictCheckWithResults + -- * Providing arguments for 'strictCheckWithResults' + , genViaProduce + , Shrink(..) + , shrinkViaArbitrary + , Strictness + , strictnessViaSized + -- * Representing individual evaluations of functions + , Evaluation(..) + , evaluationForall + , shrinkEvalWith + -- * Comparing demands + , DemandComparison(..) + , compareToSpecWith + , equalToSpec + -- * Re-exported n-ary products from "Generics.SOP" + , NP(..), I(..), All + -- * Re-exports of the rest of the library + , module Test.StrictCheck.Demand + , module Test.StrictCheck.Observe + , module Test.StrictCheck.Produce + , module Test.StrictCheck.Consume + , module Test.StrictCheck.Shaped + ) + where + +import Test.StrictCheck.Curry as Curry +import Test.StrictCheck.Produce +import Test.StrictCheck.Consume +import Test.StrictCheck.Observe +import Test.StrictCheck.Demand +import Test.StrictCheck.Shaped + +import Test.StrictCheck.Internal.Omega +import Test.StrictCheck.Internal.Shrink + ( Shrink(..), axialShrinks, fairInterleave ) + +import Generics.SOP hiding (Shape) + +import Test.QuickCheck as Exported hiding (Args, Result, function) +import qualified Test.QuickCheck as QC + +import Data.Char (ord) +import Data.Function (on) +import Data.Kind (Type) +import Data.List +import Data.Maybe +import Data.IORef +import GHC.IO.Encoding (textEncodingName) +import qualified System.IO as IO +import Type.Reflection + +-- | The default comparison of demands: exact equality +compareEquality :: All Shaped xs => NP DemandComparison xs +compareEquality = hcpure (Proxy @Shaped) (DemandComparison (==)) + +-- | The default way to generate inputs: via 'Produce' +genViaProduce :: All Produce xs => NP Gen xs +genViaProduce = hcpure (Proxy @Produce) (freely produce) + +-- | The default way to shrink inputs: via 'shrink' (from "Test.QuickCheck"'s +-- 'Arbitrary' typeclass) +shrinkViaArbitrary :: All Arbitrary xs => NP Shrink xs +shrinkViaArbitrary = hcpure (Proxy @Arbitrary) (Shrink shrink) + +-- | The default way to generate random strictnesses: uniformly choose between +-- 1 and the test configuration's @size@ parameter +strictnessViaSized :: Gen Strictness +strictnessViaSized = + Strictness <$> (choose . (1,) =<< getSize) + +-- | A newtype for wrapping a comparison on demands +-- +-- This is useful when constructing an 'NP' n-ary product of such comparisons. +newtype DemandComparison a = + DemandComparison (Demand a -> Demand a -> Bool) + +-- | A demand specification for some function @f@ is itself a function which +-- manipulates demand values for some function's arguments and results +-- +-- A @Spec@ for @f@ wraps a function which takes, in order: +-- +-- * a continuation @predict@ which accepts all of @f@'s argument types in order, +-- * an implicit representation of a demand on @f@'s result (embedded in @f@'s +-- actual result type using special bottom values, see the documentation for +-- "Test.StrictCheck.Demand" for details), and +-- * all of @f@'s original arguments in order +-- +-- The intention is that the @Spec@ will call @predict@ on some set of demands +-- representing the demands it predicts that @f@ will exert on its inputs, +-- given the provided demand on @f@'s outputs. +-- +-- For example, here is a correct @Spec@ for 'take': +-- +-- > take_spec :: Spec '[Int, [a]] [a] +-- > take_spec = +-- > Spec $ \predict d n xs -> +-- > predict n (if n > length xs then d else d ++ thunk) +-- +-- See the documentation for "Test.StrictCheck.Demand" for information about how +-- to manipulate these implicit demand representations when writing @Spec@s, and +-- see the documentation for "Test.StrictCheck.Examples.Lists" for more examples +-- of writing specifications. +newtype Spec (args :: [Type]) (result :: Type) + = Spec (forall r. (args ⋯-> r) -> result -> args ⋯-> r) + +-- | Unwrap a @Spec@ constructor, returning the contained CPS-ed specification +-- +-- Conceptually, this is the inverse to the @Spec@ constructor, but because +-- @Spec@ is variadic, @getSpec . Spec@ and @Spec . getSpec@ don't typecheck +-- without additional type annotation. +getSpec + :: forall r args result. + Spec args result + -> (args ⋯-> r) + -> result + -> args ⋯-> r +getSpec (Spec s) k d = s @r k d + +-- | Given a list of ways to compare demands, a demand specification, and an +-- evaluation of a particular function, determine if the function met the +-- specification, as decided by the comparisons. If so, return the prediction +-- of the specification. +compareToSpecWith + :: forall args result. + (All Shaped args, Curry args, Shaped result) + => NP DemandComparison args + -> Spec args result + -> Evaluation args result + -> Maybe (NP Demand args) +compareToSpecWith comparisons spec (Evaluation inputs inputsD resultD) = + let prediction = + Curry.uncurry + (getSpec @(NP Demand args) + spec + collectDemands + (fromDemand $ E resultD)) + inputs + correct = + all id . hcollapse $ + hcliftA3 (Proxy @Shaped) + (\(DemandComparison c) iD iD' -> K $ iD `c` iD') + comparisons + inputsD + prediction + in if correct then Nothing else Just prediction + where + collectDemands :: args ⋯-> NP Demand args + collectDemands = + curryCollect @args (hcmap (Proxy @Shaped) (toDemand . unI)) + +curryCollect + :: forall (xs :: [Type]) r. Curry xs => (NP I xs -> r) -> xs ⋯-> r +curryCollect k = Curry.curry @xs k + +-- | Checks if a given 'Evaluation' exactly matches the prediction of a given +-- 'Spec', returning the prediction of that @Spec@ if not +-- +-- __Note:__ In the case of __success__ this returns @Nothing@; in the case of +-- __failure__ this returns @Just@ the incorrect prediction. +equalToSpec + :: forall args result. + (All Shaped args, Shaped result, Curry args) + => Spec args result + -> Evaluation args result + -> Maybe (NP Demand args) +equalToSpec spec e = + compareToSpecWith compareEquality spec e + +-- | A @Strictness@ represents (roughly) how strict a randomly generated +-- function or evaluation context should be +-- +-- An evaluation context generated with some strictness @s@ (i.e. through +-- 'evaluationForall') will consume at most @s@ constructors of its input, +-- although it might consume fewer. +newtype Strictness + = Strictness Int + deriving stock (Eq, Ord) + deriving newtype (Show, Num) + +-- | A function can be checked against a specification if it meets the +-- @StrictCheck@ constraint +type StrictCheck function = + ( Shaped (Result function) + , Consume (Result function) + , Curry (Args function) + , All Typeable (Args function) + , All Shaped (Args function) ) + +-- | The most general function for random strictness testing: all of the more +-- convenient such functions can be derived from this one +-- +-- Given some function @f@, this takes as arguments: +-- +-- * A 'QC.Args' record describing arguments to pass to the underlying +-- QuickCheck engine +-- * An 'NP' n-ary product of 'Shrink' shrinkers, one for each argument of @f@ +-- * An 'NP' n-ary product of 'Gen' generators, one for each argument of @f@ +-- * A 'Gen' generator for strictnesses to be tested +-- * A predicate on 'Evaluation's: if the 'Evaluation' passes the predicate, +-- it should return @Nothing@; otherwise, it should return @Just@ some +-- @evidence@ representing the failure (when checking 'Spec's, this evidence +-- comes in the form of a @Spec@'s (incorrect) prediction) +-- * the function @f@ to be tested +-- +-- If all tests succeed, @(Nothing, result)@ is returned, where @result@ is the +-- underlying 'QC.Result' type from "Test.QuickCheck". If there is a test +-- failure, it also returns @Just@ the failed 'Evaluation' as well as whatever +-- @evidence@ was produced by the predicate. +strictCheckWithResults :: + forall function evidence. + StrictCheck function + => QC.Args + -> NP Shrink (Args function) -- TODO: allow dependent shrinking + -> NP Gen (Args function) -- TODO: allow dependent generation + -> Gen Strictness + -> (Evaluation (Args function) (Result function) -> Maybe evidence) + -> function + -> IO ( Maybe ( Evaluation (Args function) (Result function) + , evidence ) + , QC.Result ) +strictCheckWithResults + qcArgs shrinks gens strictness predicate function = do + ref <- newIORef Nothing + result <- + quickCheckWithResult qcArgs{chatty = False{-, maxSuccess = 10000-}} $ + forAllShrink + (evaluationForall @function gens strictness function) + (shrinkEvalWith @function shrinks function) $ + \example -> + case predicate example of + Nothing -> + property True + Just evidence -> + whenFail (writeIORef ref $ Just (example, evidence)) False + readIORef ref >>= \case + Nothing -> pure (Nothing, result) + Just example -> pure (Just example, result) + +-- | Check a function to see whether it exactly meets a strictness specification +-- +-- If the function fails to meet the specification, a counterexample is +-- pretty-printed in a box-drawn diagram illustrating how the specification +-- failed to match the real observed behavior of the function. +strictCheckSpecExact + :: forall function. + ( StrictCheck function + , All Arbitrary (Args function) + , All Produce (Args function) + ) => Spec (Args function) (Result function) + -> function + -> IO () +strictCheckSpecExact spec function = + do (maybeExample, result) <- + strictCheckWithResults + stdArgs + shrinkViaArbitrary + genViaProduce + strictnessViaSized + (equalToSpec spec) + function + case lines (output result) of + line0 : _ -> putStrLn line0 + [] -> pure () + case maybeExample of + Nothing -> return () + Just example -> do + unicode <- doesStdoutAcceptUnicode + putStrLn (Prelude.uncurry (displayCounterSpec unicode) example) + +doesStdoutAcceptUnicode :: IO Bool +doesStdoutAcceptUnicode = do + encoding <- IO.hGetEncoding IO.stdout + case encoding of + Nothing -> pure False + Just enc -> pure (any (((==) `on` textEncodingName) enc) [IO.utf8, IO.utf8_bom, IO.utf16, IO.utf16le, IO.utf16be, IO.utf32, IO.utf32le, IO.utf32be]) + +------------------------------------------------------------ +-- An Evaluation is what we generate when StrictCheck-ing -- +------------------------------------------------------------ + +-- | A snapshot of the observed strictness behavior of a function +-- +-- An @Evaluation@ contains the 'inputs' at which a function was called, the +-- 'inputDemands' which were induced upon those inputs, and the 'resultDemand' +-- which induced that demand on the inputs. +data Evaluation args result = + Evaluation + { inputs :: NP I args -- ^ Inputs to a function + , inputDemands :: NP Demand args -- ^ Demands on the input + , resultDemand :: PosDemand result -- ^ Demand on the result + } + +instance (All Typeable args, Typeable result) + => Show (Evaluation args result) where + show _ = + " :: Evaluation" + ++ " '[" ++ intercalate ", " argTypes ++ "]" + ++ " " ++ show (typeRep :: TypeRep result) + where + argTypes :: [String] + argTypes = + hcollapse + $ hliftA (K . show) + $ (hcpure (Proxy @Typeable) typeRep :: NP TypeRep args) + + +----------------------------------- +-- Generating random evaluations -- +----------------------------------- + +-- | Given a list of generators for a function's arguments and a generator for +-- random strictnesses (measured in number of constructors evaluated), create +-- a generator for random 'Evaluation's of that function in random contexts +evaluationForall + :: forall f. + ( Curry (Args f) + , Consume (Result f) + , Shaped (Result f) + , All Shaped (Args f) + ) => NP Gen (Args f) + -> Gen Strictness + -> f + -> Gen (Evaluation (Args f) (Result f)) +evaluationForall gens strictnessGen function = do + inputs <- hsequence gens + strictness <- strictnessGen + toOmega <- freely produce + return (go strictness toOmega inputs) + where + -- If context is fully lazy, increase strictness until it forces something + go :: Strictness + -> (Result f -> Omega) + -> NP I (Args f) + -> Evaluation (Args f) (Result f) + go (Strictness s) tO is = + let (resultD, inputsD) = + observeNP (forceOmega s . tO) (uncurryAll @f function) is + in case resultD of + T -> go (Strictness s + 1) tO is + E posResultD -> + Evaluation is inputsD posResultD + + +--------------------------- +-- Shrinking evaluations -- +--------------------------- + +-- | Given a shrinker for each of the arguments of a function, the function +-- itself, and some 'Evaluation' of that function, produce a list of smaller +-- @Evaluation@s of that function +shrinkEvalWith + :: forall f. + ( Curry (Args f) + , Shaped (Result f) + , All Shaped (Args f) + ) => NP Shrink (Args f) + -> f + -> Evaluation (Args f) (Result f) + -> [Evaluation (Args f) (Result f)] +shrinkEvalWith + shrinks (uncurryAll -> function) (Evaluation inputs _ resultD) = + let shrunkDemands = shrinkDemand @(Result f) resultD + shrunkInputs = fairInterleave (axialShrinks shrinks inputs) + shrinkingDemand = mapMaybe (reObserve inputs) shrunkDemands + shrinkingInputs = mapMaybe (flip reObserve resultD) shrunkInputs + in fairInterleave [ shrinkingDemand, shrinkingInputs ] + where + reObserve + :: NP I (Args f) + -> PosDemand (Result f) + -> Maybe (Evaluation (Args f) (Result f)) + reObserve is rD = + let (rD', isD) = observeNP (evaluateDemand rD) function is + in fmap (Evaluation is isD) $ + case rD' of + T -> Nothing + E pos -> Just pos + +-- | If 'False' (unicode output is disabled), replace all non-ASCII characters with '?'. +sanitize :: Bool -> String -> String +sanitize True = id +sanitize False = fmap (\c -> if ord c < 128 then c else '?') + +-- | Render a counter-example to a specification (that is, an 'Evaluation' +-- paired with some expected input demands it doesn't match) as a +-- box-drawing sketch (in Unicode or ASCII depending on whether the +-- first argument is 'True' or 'False') +displayCounterSpec + :: forall args result. + (Shaped result, All Shaped args) + => Bool -- ^ 'True' to enable prettier Unicode output + -> Evaluation args result + -> NP Demand args + -> String +displayCounterSpec unicode (Evaluation inputs inputsD resultD) predictedInputsD = + sanitize unicode $ + beside inputBox (" " : threeDashes : repeat " ") resultBox + ++ (flip replicate ' ' $ + (2 `max` (subtract 2 $ (lineMax [inputString] `div` 2)))) + ++ threeArrows + ++ beside + actualBox + (" " : " " : notEqual : repeat " ") + predictedBox + where + threeDashes | unicode = "───" + | otherwise = "---" + threeArrows | unicode = "🡓 🡓 🡓\n" + | otherwise = "v v v\n" + notEqual | unicode = " ═╱═ " + | otherwise = " =/= " + inputBox + | unicode = + box "┌" '─' "┐" + "│" inputHeader "├" + "├" '─' "┤" + "│" inputString "│" + "└" '─' "┘" + | otherwise = + box "+" '-' "+" + "|" inputHeader "+" + "+" '-' "+" + "|" inputString "|" + "+" '-' "+" + + resultBox + | unicode = + box "┌" '─' "┐" + "┤" resultHeader "│" + "├" '─' "┤" + "│" resultString "│" + "└" '─' "┘" + | otherwise = + box "+" '-' "+" + "+" resultHeader "|" + "+" '-' "+" + "|" resultString "|" + "+" '-' "+" + + actualBox + | unicode = + box "┌" '─' "┐" + "│" actualHeader "│" + "├" '─' "┤" + "│" actualDemandString "│" + "└" '─' "┘" + | otherwise = + box "+" '-' "+" + "|" actualHeader "|" + "+" '-' "+" + "|" actualDemandString "|" + "+" '-' "+" + + predictedBox + | unicode = + box "┌" '─' "┐" + "│" predictedHeader "│" + "├" '─' "┤" + "│" predictedDemandString "│" + "└" '─' "┘" + | otherwise = + box "+" '-' "+" + "|" predictedHeader "|" + "+" '-' "+" + "|" predictedDemandString "|" + "+" '-' "+" + + inputHeader = " Input" ++ plural + resultHeader = " Demand on result" + actualHeader = " Actual input demand" ++ plural + predictedHeader = " Spec's input demand" ++ plural + + inputString = + showBulletedNPWith @Shaped (prettyDemand . interleave Eval . unI) inputs + resultString = " " ++ prettyDemand @result (E resultD) + actualDemandString = + showBulletedNPWith @Shaped prettyDemand inputsD + predictedDemandString = + showBulletedNPWith @Shaped prettyDemand predictedInputsD + + rule w l c r = frame w l (replicate w c) r ++ "\n" + + frame w before str after = + before ++ str + ++ (replicate (w - length str) ' ') + ++ after + + frames w before para after = + unlines $ map (\str -> frame w before str after) (lines para) + + beside l cs r = + unlines . take (length ls `max` length rs) $ + zipWith3 + (\x c y -> x ++ c ++ y) + (ls ++ repeat (replicate (lineMax [l]) ' ')) + cs + (rs ++ repeat "") + where + ls = lines l + rs = lines r + + box top_l top top_r + header_l header header_r + div_l div_c div_r + body_l body body_r + bottom_l bottom bottom_r = + let w = lineMax [header, body] + in rule w top_l top top_r + ++ frames w header_l header header_r + ++ rule w div_l div_c div_r + ++ frames w body_l body body_r + ++ rule w bottom_l bottom bottom_r + + lineMax strs = + (maximum . map + (\(lines -> ls) -> maximum (map length ls) + 1) $ strs) + + plural = case inputs of + (_ :* Nil) -> "" + _ -> "s" + + showBulletedNPWith + :: forall c g xs. All c xs + => (forall x. c x => g x -> String) -> NP g xs -> String + -- showBulletedNPWith display (x :* Nil) = " " ++ display x ++ "\n" + showBulletedNPWith display list = showNPWith' list + where + showNPWith' :: forall ys. All c ys => NP g ys -> String + showNPWith' Nil = "" + showNPWith' (y :* ys) = + bullet ++ display y ++ "\n" ++ showNPWith' ys + bullet | unicode = " • " + | otherwise = " * " diff --git a/src/Test/StrictCheck/Consume.hs b/src/Test/StrictCheck/Consume.hs --- a/src/Test/StrictCheck/Consume.hs +++ b/src/Test/StrictCheck/Consume.hs @@ -1,275 +1,275 @@ -{-| This module defines the 'Consume' typeclass, used for incrementally - destructing inputs to random non-strict functions. - - Calling 'consume' on some value lazily returns an abstract type of 'Input', - which contains all the entropy present in the original value. Paired with - 'Test.StrictCheck.Produce', these @Input@ values can be used to generate - random non-strict functions, whose strictness behavior is dependent on the - values given to them. --} -module Test.StrictCheck.Consume - ( -- * Incrementally consuming input - Input - , Inputs - , Consume(..) - -- * Manually writing 'Consume' instances - , constructor - , normalize - , consumeTrivial - , consumePrimitive - -- * Generically deriving 'Consume' instances - , GConsume - , gConsume - ) where - -import Test.QuickCheck -import Generics.SOP -import Generics.SOP.NS - -import Test.StrictCheck.Internal.Inputs - -import Data.Complex - -import Data.Foldable as Fold -import Data.List.NonEmpty (NonEmpty(..)) -import Data.Tree as Tree -import Data.Set as Set -import Data.Map as Map -import Data.Sequence as Seq -import Data.IntMap as IntMap -import Data.IntSet as IntSet - - --- | Lazily monomorphize some input value, by converting it into an @Input@. --- This is an incremental version of QuickCheck's @CoArbitrary@ typeclass. --- It can also be seen as a generalization of the @NFData@ class. --- --- Instances of @Consume@ can be derived automatically for any type implementing --- the @Generic@ class from "GHC.Generics". Using the @DeriveAnyClass@ --- extension, we can say: --- --- > import GHC.Generics as GHC --- > import Generics.SOP as SOP --- > --- > data D x y --- > = A --- > | B (x, y) --- > deriving (GHC.Generic, SOP.Generic, Consume) --- --- This automatic derivation follows these rules, which you can follow too if --- you're manually writing an instance for some type which is not @Generic@: --- --- For each distinct constructor, make a single call to 'constructor' with --- a distinct @Int@, and a list of @Input@s, each created by recursively calling --- 'consume' on every field in that constructor. For abstract types (e.g. sets), --- the same procedure can be used upon an extracted list representation of the --- contents. -class Consume a where - -- | Convert an @a@ into an @Input@ by recursively destructing it using calls - -- to @consume@ - consume :: a -> Input - default consume :: GConsume a => a -> Input - consume = gConsume - --- | Reassemble pieces of input into a larger Input: this is to be called on the --- result of @consume@-ing subparts of input -constructor :: Int -> [Input] -> Input -constructor n !is = - Input (Variant (variant n)) is - --- | Use the CoArbitrary instance for a type to consume it --- --- This should only be used for "flat" types, i.e. those which contain no --- interesting consumable substructure, as it's fully strict (non-incremental) -consumePrimitive :: CoArbitrary a => a -> Input -consumePrimitive !a = - Input (Variant (coarbitrary a)) [] - --- | Consume a type which has no observable structure whatsoever --- --- This should only be used for types for which there is only one inhabitant, or --- for which inhabitants cannot be distinguished at all. -consumeTrivial :: a -> Input -consumeTrivial !_ = - Input mempty [] - --- | Fully normalize something which can be consumed -normalize :: Consume a => a -> () -normalize (consume -> input) = go input - where - go (Input _ is) = Fold.foldr seq () (fmap go is) - --------------------------------------------- --- Deriving Consume instances generically -- --------------------------------------------- - --- | The constraints necessary to generically @consume@ something -type GConsume a = (Generic a, All2 Consume (Code a)) - --- | Generic 'consume' -gConsume :: GConsume a => a -> Input -gConsume !(from -> sop) = - constructor (index_SOP sop) - . hcollapse - . hcliftA (Proxy @Consume) (K . consume . unI) - $ sop - - ---------------- --- Instances -- ---------------- - -instance Consume (a -> b) where consume = consumeTrivial -instance Consume (Proxy p) where consume = consumeTrivial - -instance Consume Char where consume = consumePrimitive -instance Consume Word where consume = consumePrimitive -instance Consume Int where consume = consumePrimitive -instance Consume Double where consume = consumePrimitive -instance Consume Float where consume = consumePrimitive -instance Consume Rational where consume = consumePrimitive -instance Consume Integer where consume = consumePrimitive -instance (CoArbitrary a, RealFloat a) => Consume (Complex a) where - consume = consumePrimitive - -instance Consume () -instance Consume Bool -instance Consume Ordering -instance Consume a => Consume (Maybe a) -instance (Consume a, Consume b) => Consume (Either a b) -instance Consume a => Consume [a] - - -instance Consume a => Consume (NonEmpty a) where - consume (a :| as) = constructor 0 [consume a, consume as] - -instance Consume a => Consume (Tree a) where - consume (Node a as) = constructor 0 [consume a, consume as] - -instance Consume v => Consume (Map k v) where - consume = constructor 0 . fmap (consume . snd) . Map.toList - -consumeContainer :: (Consume a, Foldable t) => t a -> Input -consumeContainer = constructor 0 . fmap consume . Fold.toList - -instance Consume v => Consume (Seq v) where consume = consumeContainer -instance Consume v => Consume (Set v) where consume = consumeContainer -instance Consume v => Consume (IntMap v) where consume = consumeContainer -instance Consume IntSet where - consume = consumeContainer . IntSet.toList - --- TODO: instances for the rest of Containers - -instance (Consume a, Consume b) => Consume (a, b) -instance (Consume a, Consume b, Consume c) => Consume (a, b, c) -instance (Consume a, Consume b, Consume c, Consume d) => Consume (a, b, c, d) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e - ) => Consume - (a, b, c, d, e) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - ) => Consume - (a, b, c, d, e, f) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g - ) => Consume - (a, b, c, d, e, f, g) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h - ) => Consume - (a, b, c, d, e, f, g, h) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i - ) => Consume - (a, b, c, d, e, f, g, h, i) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j - ) => Consume - (a, b, c, d, e, f, g, h, i, j) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j, Consume k - ) => Consume - (a, b, c, d, e, f, g, h, i, j, k) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l - ) => Consume - (a, b, c, d, e, f, g, h, i, j, k, l) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l - , Consume m - ) => Consume - (a, b, c, d, e, f, g, h, i, j, k, l, m) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l - , Consume m, Consume n - ) => Consume - (a, b, c, d, e, f, g, h, i, j, k, l, m, n) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l - , Consume m, Consume n, Consume o - ) => Consume - (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l - , Consume m, Consume n, Consume o, Consume p - ) => Consume - (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l - , Consume m, Consume n, Consume o, Consume p, Consume q - ) => Consume - (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l - , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r - ) => Consume - (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l - , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r - , Consume s - ) => Consume - (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l - , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r - , Consume s, Consume t - ) => Consume - (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l - , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r - , Consume s, Consume t, Consume u - ) => Consume - (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l - , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r - , Consume s, Consume t, Consume u, Consume v - ) => Consume - (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l - , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r - , Consume s, Consume t, Consume u, Consume v, Consume w - ) => Consume - (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l - , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r - , Consume s, Consume t, Consume u, Consume v, Consume w, Consume x - ) => Consume - (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l - , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r - , Consume s, Consume t, Consume u, Consume v, Consume w, Consume x - , Consume y - ) => Consume - (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) -instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f - , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l - , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r - , Consume s, Consume t, Consume u, Consume v, Consume w, Consume x - , Consume y, Consume z - ) => Consume - (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z) +{-| This module defines the 'Consume' typeclass, used for incrementally + destructing inputs to random non-strict functions. + + Calling 'consume' on some value lazily returns an abstract type of 'Input', + which contains all the entropy present in the original value. Paired with + 'Test.StrictCheck.Produce', these @Input@ values can be used to generate + random non-strict functions, whose strictness behavior is dependent on the + values given to them. +-} +module Test.StrictCheck.Consume + ( -- * Incrementally consuming input + Input + , Inputs + , Consume(..) + -- * Manually writing 'Consume' instances + , constructor + , normalize + , consumeTrivial + , consumePrimitive + -- * Generically deriving 'Consume' instances + , GConsume + , gConsume + ) where + +import Test.QuickCheck +import Generics.SOP +import Generics.SOP.NS + +import Test.StrictCheck.Internal.Inputs + +import Data.Complex + +import Data.Foldable as Fold +import Data.List.NonEmpty (NonEmpty(..)) +import Data.Tree as Tree +import Data.Set as Set +import Data.Map as Map +import Data.Sequence as Seq +import Data.IntMap as IntMap +import Data.IntSet as IntSet + + +-- | Lazily monomorphize some input value, by converting it into an @Input@. +-- This is an incremental version of QuickCheck's @CoArbitrary@ typeclass. +-- It can also be seen as a generalization of the @NFData@ class. +-- +-- Instances of @Consume@ can be derived automatically for any type implementing +-- the @Generic@ class from "GHC.Generics". Using the @DeriveAnyClass@ +-- extension, we can say: +-- +-- > import GHC.Generics as GHC +-- > import Generics.SOP as SOP +-- > +-- > data D x y +-- > = A +-- > | B (x, y) +-- > deriving (GHC.Generic, SOP.Generic, Consume) +-- +-- This automatic derivation follows these rules, which you can follow too if +-- you're manually writing an instance for some type which is not @Generic@: +-- +-- For each distinct constructor, make a single call to 'constructor' with +-- a distinct @Int@, and a list of @Input@s, each created by recursively calling +-- 'consume' on every field in that constructor. For abstract types (e.g. sets), +-- the same procedure can be used upon an extracted list representation of the +-- contents. +class Consume a where + -- | Convert an @a@ into an @Input@ by recursively destructing it using calls + -- to @consume@ + consume :: a -> Input + default consume :: GConsume a => a -> Input + consume = gConsume + +-- | Reassemble pieces of input into a larger Input: this is to be called on the +-- result of @consume@-ing subparts of input +constructor :: Int -> [Input] -> Input +constructor n !is = + Input (Variant (variant n)) is + +-- | Use the CoArbitrary instance for a type to consume it +-- +-- This should only be used for "flat" types, i.e. those which contain no +-- interesting consumable substructure, as it's fully strict (non-incremental) +consumePrimitive :: CoArbitrary a => a -> Input +consumePrimitive !a = + Input (Variant (coarbitrary a)) [] + +-- | Consume a type which has no observable structure whatsoever +-- +-- This should only be used for types for which there is only one inhabitant, or +-- for which inhabitants cannot be distinguished at all. +consumeTrivial :: a -> Input +consumeTrivial !_ = + Input mempty [] + +-- | Fully normalize something which can be consumed +normalize :: Consume a => a -> () +normalize (consume -> input) = go input + where + go (Input _ is) = Fold.foldr seq () (fmap go is) + +-------------------------------------------- +-- Deriving Consume instances generically -- +-------------------------------------------- + +-- | The constraints necessary to generically @consume@ something +type GConsume a = (Generic a, All2 Consume (Code a)) + +-- | Generic 'consume' +gConsume :: GConsume a => a -> Input +gConsume !(from -> sop) = + constructor (index_SOP sop) + . hcollapse + . hcliftA (Proxy @Consume) (K . consume . unI) + $ sop + + +--------------- +-- Instances -- +--------------- + +instance Consume (a -> b) where consume = consumeTrivial +instance Consume (Proxy p) where consume = consumeTrivial + +instance Consume Char where consume = consumePrimitive +instance Consume Word where consume = consumePrimitive +instance Consume Int where consume = consumePrimitive +instance Consume Double where consume = consumePrimitive +instance Consume Float where consume = consumePrimitive +instance Consume Rational where consume = consumePrimitive +instance Consume Integer where consume = consumePrimitive +instance CoArbitrary a => Consume (Complex a) where + consume = consumePrimitive + +instance Consume () +instance Consume Bool +instance Consume Ordering +instance Consume a => Consume (Maybe a) +instance (Consume a, Consume b) => Consume (Either a b) +instance Consume a => Consume [a] + + +instance Consume a => Consume (NonEmpty a) where + consume (a :| as) = constructor 0 [consume a, consume as] + +instance Consume a => Consume (Tree a) where + consume (Node a as) = constructor 0 [consume a, consume as] + +instance Consume v => Consume (Map k v) where + consume = constructor 0 . fmap (consume . snd) . Map.toList + +consumeContainer :: (Consume a, Foldable t) => t a -> Input +consumeContainer = constructor 0 . fmap consume . Fold.toList + +instance Consume v => Consume (Seq v) where consume = consumeContainer +instance Consume v => Consume (Set v) where consume = consumeContainer +instance Consume v => Consume (IntMap v) where consume = consumeContainer +instance Consume IntSet where + consume = consumeContainer . IntSet.toList + +-- TODO: instances for the rest of Containers + +instance (Consume a, Consume b) => Consume (a, b) +instance (Consume a, Consume b, Consume c) => Consume (a, b, c) +instance (Consume a, Consume b, Consume c, Consume d) => Consume (a, b, c, d) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e + ) => Consume + (a, b, c, d, e) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + ) => Consume + (a, b, c, d, e, f) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g + ) => Consume + (a, b, c, d, e, f, g) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h + ) => Consume + (a, b, c, d, e, f, g, h) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i + ) => Consume + (a, b, c, d, e, f, g, h, i) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j + ) => Consume + (a, b, c, d, e, f, g, h, i, j) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j, Consume k + ) => Consume + (a, b, c, d, e, f, g, h, i, j, k) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l + ) => Consume + (a, b, c, d, e, f, g, h, i, j, k, l) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l + , Consume m + ) => Consume + (a, b, c, d, e, f, g, h, i, j, k, l, m) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l + , Consume m, Consume n + ) => Consume + (a, b, c, d, e, f, g, h, i, j, k, l, m, n) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l + , Consume m, Consume n, Consume o + ) => Consume + (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l + , Consume m, Consume n, Consume o, Consume p + ) => Consume + (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l + , Consume m, Consume n, Consume o, Consume p, Consume q + ) => Consume + (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l + , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r + ) => Consume + (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l + , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r + , Consume s + ) => Consume + (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l + , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r + , Consume s, Consume t + ) => Consume + (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l + , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r + , Consume s, Consume t, Consume u + ) => Consume + (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l + , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r + , Consume s, Consume t, Consume u, Consume v + ) => Consume + (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l + , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r + , Consume s, Consume t, Consume u, Consume v, Consume w + ) => Consume + (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l + , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r + , Consume s, Consume t, Consume u, Consume v, Consume w, Consume x + ) => Consume + (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l + , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r + , Consume s, Consume t, Consume u, Consume v, Consume w, Consume x + , Consume y + ) => Consume + (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) +instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f + , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l + , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r + , Consume s, Consume t, Consume u, Consume v, Consume w, Consume x + , Consume y, Consume z + ) => Consume + (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z) diff --git a/src/Test/StrictCheck/Curry.hs b/src/Test/StrictCheck/Curry.hs --- a/src/Test/StrictCheck/Curry.hs +++ b/src/Test/StrictCheck/Curry.hs @@ -1,147 +1,148 @@ -{-| This module defines a flexible and efficient way to curry and uncurry - functions of any arity. This is useful in the context of StrictCheck to - provide a lightweight interface to test developers which does not require - them to directly work with heterogeneous lists. --} -module Test.StrictCheck.Curry - ( -- * Computing the types of curried functions - type (⋯->) - , type (-..->) - , Args - , Result - -- * Currying functions at all arities - , Curry(..) - , curryAll - , uncurryAll - , withCurryIdentity - -- * Generalized to any heterogeneous list - , List(..) - ) where - - -import Prelude hiding (curry, uncurry) - -import Data.Type.Equality -import qualified Unsafe.Coerce as UNSAFE - -import qualified Generics.SOP as SOP - - -------------------------------------------------- --- Manipulating the types of curried functions -- -------------------------------------------------- - --- | Given a function type, return a list of all its argument types --- --- For example: --- --- > Args (Int -> Bool -> Char) ~ [Int, Bool] -type family Args (f :: *) :: [*] where - Args (a -> rest) = a : Args rest - Args x = '[] - --- | Given a list of argument types and the "rest" of a function type, return a --- curried function type which takes the specified argument types in order, --- before returning the given rest --- --- For example: --- --- > [Int, Bool] ⋯-> Char ~ Int -> Bool -> Char --- --- This infix unicode symbol is meant to evoke a function arrow with an --- ellipsis. -type family (args :: [*]) ⋯-> (rest :: *) :: * where - '[] ⋯-> rest = rest - (a : args) ⋯-> rest = a -> args ⋯-> rest - --- | For those who don't want to type in unicode, we provide this ASCII synonym --- for the ellipsis function arrow @(⋯->)@ -type args -..-> rest = args ⋯-> rest - --- | Strip all arguments from a function type, yielding its (non-function-type) --- result --- --- For example: --- --- > Result (Int -> Bool -> Char) ~ Char -type family Result (f :: *) :: * where - Result (a -> rest) = Result rest - Result r = r - -curryIdentity :: forall function. - function :~: (Args function ⋯-> Result function) -curryIdentity = UNSAFE.unsafeCoerce (Refl :: () :~: ()) - --- | For any function type @function@, it is always true that --- --- > function ~ (Args function ⋯-> Result function) --- --- GHC doesn't know this, however, so @withCurryIdentity@ provides this proof to --- the enclosed computation, by discharging this wanted equality constraint. -withCurryIdentity :: forall function r. - (function ~ (Args function ⋯-> Result function) => r) -> r -withCurryIdentity r = - case curryIdentity @function of Refl -> r - - ------------------------- --- Partial uncurrying -- ------------------------- - --- | This currying mechanism is agnostic to the concrete heterogeneous list type --- used to carry arguments. The @List@ class abstracts over the nil and cons --- operations of a heterogeneous list: to use your own, just define an instance. -class List (list :: [*] -> *) where - nil :: list '[] - cons :: x -> list xs -> list (x : xs) - uncons :: list (x : xs) -> (x, list xs) - --- | The Curry class witnesses that for any list of arguments, it is always --- possible to curry/uncurry at that arity -class Curry (args :: [*]) where - uncurry - :: forall result list. - List list => (args ⋯-> result) -> list args -> result - curry - :: forall result list. - List list => (list args -> result) -> args ⋯-> result - -instance Curry '[] where - uncurry x = \(!_) -> x - curry f = f nil - -instance Curry xs => Curry (x : xs) where - uncurry f = \(uncons -> (x, xs)) -> uncurry (f x) xs - curry f = \x -> curry (\xs -> f (cons x xs)) - - --------------------------------------------------------- --- Variadic uncurrying/currying, aka (un)curryAll-ing -- --------------------------------------------------------- - --- | Uncurry all arguments to a function type --- --- This is a special case of 'uncurry', and may ease type inference. -uncurryAll - :: forall function list. (List list, Curry (Args function)) - => function -> (list (Args function) -> Result function) -uncurryAll = withCurryIdentity @function uncurry - --- | Curry all arguments to a function from a heterogeneous list to a result --- --- This is a special case of 'curry', and may ease type inference. -curryAll - :: forall args result list. (List list, Curry args) - => (list args -> result) - -> (args ⋯-> result) -curryAll = curry - - --------------------------- --- Instances for HLists -- --------------------------- - -instance List (SOP.NP SOP.I) where - nil = SOP.Nil - cons x xs = SOP.I x SOP.:* xs - uncons (SOP.I x SOP.:* xs) = (x, xs) +{-| This module defines a flexible and efficient way to curry and uncurry + functions of any arity. This is useful in the context of StrictCheck to + provide a lightweight interface to test developers which does not require + them to directly work with heterogeneous lists. +-} +module Test.StrictCheck.Curry + ( -- * Computing the types of curried functions + type (⋯->) + , type (-..->) + , Args + , Result + -- * Currying functions at all arities + , Curry(..) + , curryAll + , uncurryAll + , withCurryIdentity + -- * Generalized to any heterogeneous list + , List(..) + ) where + + +import Prelude hiding (curry, uncurry) + +import Data.Kind (Type) +import Data.Type.Equality +import qualified Unsafe.Coerce as UNSAFE + +import qualified Generics.SOP as SOP + + +------------------------------------------------- +-- Manipulating the types of curried functions -- +------------------------------------------------- + +-- | Given a function type, return a list of all its argument types +-- +-- For example: +-- +-- > Args (Int -> Bool -> Char) ~ [Int, Bool] +type family Args (f :: Type) :: [Type] where + Args (a -> rest) = a : Args rest + Args x = '[] + +-- | Given a list of argument types and the "rest" of a function type, return a +-- curried function type which takes the specified argument types in order, +-- before returning the given rest +-- +-- For example: +-- +-- > [Int, Bool] ⋯-> Char ~ Int -> Bool -> Char +-- +-- This infix unicode symbol is meant to evoke a function arrow with an +-- ellipsis. +type family (args :: [Type]) ⋯-> (rest :: Type) :: Type where + '[] ⋯-> rest = rest + (a : args) ⋯-> rest = a -> args ⋯-> rest + +-- | For those who don't want to type in unicode, we provide this ASCII synonym +-- for the ellipsis function arrow @(⋯->)@ +type args -..-> rest = args ⋯-> rest + +-- | Strip all arguments from a function type, yielding its (non-function-type) +-- result +-- +-- For example: +-- +-- > Result (Int -> Bool -> Char) ~ Char +type family Result (f :: Type) :: Type where + Result (a -> rest) = Result rest + Result r = r + +curryIdentity :: forall function. + function :~: (Args function ⋯-> Result function) +curryIdentity = UNSAFE.unsafeCoerce (Refl :: () :~: ()) + +-- | For any function type @function@, it is always true that +-- +-- > function ~ (Args function ⋯-> Result function) +-- +-- GHC doesn't know this, however, so @withCurryIdentity@ provides this proof to +-- the enclosed computation, by discharging this wanted equality constraint. +withCurryIdentity :: forall function r. + (function ~ (Args function ⋯-> Result function) => r) -> r +withCurryIdentity r = + case curryIdentity @function of Refl -> r + + +------------------------ +-- Partial uncurrying -- +------------------------ + +-- | This currying mechanism is agnostic to the concrete heterogeneous list type +-- used to carry arguments. The @List@ class abstracts over the nil and cons +-- operations of a heterogeneous list: to use your own, just define an instance. +class List (list :: [Type] -> Type) where + nil :: list '[] + cons :: x -> list xs -> list (x : xs) + uncons :: list (x : xs) -> (x, list xs) + +-- | The Curry class witnesses that for any list of arguments, it is always +-- possible to curry/uncurry at that arity +class Curry (args :: [Type]) where + uncurry + :: forall result list. + List list => (args ⋯-> result) -> list args -> result + curry + :: forall result list. + List list => (list args -> result) -> args ⋯-> result + +instance Curry '[] where + uncurry x = \(!_) -> x + curry f = f nil + +instance Curry xs => Curry (x : xs) where + uncurry f = \(uncons -> (x, xs)) -> uncurry (f x) xs + curry f = \x -> curry (\xs -> f (cons x xs)) + + +-------------------------------------------------------- +-- Variadic uncurrying/currying, aka (un)curryAll-ing -- +-------------------------------------------------------- + +-- | Uncurry all arguments to a function type +-- +-- This is a special case of 'uncurry', and may ease type inference. +uncurryAll + :: forall function list. (List list, Curry (Args function)) + => function -> (list (Args function) -> Result function) +uncurryAll = withCurryIdentity @function uncurry + +-- | Curry all arguments to a function from a heterogeneous list to a result +-- +-- This is a special case of 'curry', and may ease type inference. +curryAll + :: forall args result list. (List list, Curry args) + => (list args -> result) + -> (args ⋯-> result) +curryAll = curry + + +-------------------------- +-- Instances for HLists -- +-------------------------- + +instance List (SOP.NP SOP.I) where + nil = SOP.Nil + cons x xs = SOP.I x SOP.:* xs + uncons (SOP.I x SOP.:* xs) = (x, xs) diff --git a/src/Test/StrictCheck/Demand.hs b/src/Test/StrictCheck/Demand.hs --- a/src/Test/StrictCheck/Demand.hs +++ b/src/Test/StrictCheck/Demand.hs @@ -1,310 +1,310 @@ -{-| A 'Demand' on some value of type @T@ is shaped like a @T@, but possibly - truncated, to represent partial evaluation. This module defines the type of - demands, and functions to manipulate them for the purpose of constructing - demand specifications. - - A demand for some type @T@ can be represented one of two interconvertible - ways: - - * explicitly, as a recursively interleaved @Shape@ of @T@ - * implicitly, as a value of @T@ with specially-tagged bottom values - which represent un-evaluated portions of that value - - The explicit representation is useful for writing traversals and other such - manipulations of demand values, while the implicit representation can prove - convenient for writing demand specifications. The implicit representation is - the default when writing specifications, but through the use of 'toDemand' - and 'fromDemand', either representation can be used wherever it is most - appropriate. --} -module Test.StrictCheck.Demand - ( -- * The explicit @Demand@ interface - Thunk(..) - , Demand, PosDemand - , pattern E, pattern T - -- ** Manipulating explicit @Demand@s - , evaluateDemand - , shrinkDemand - , prettyDemand, printDemand - , eqDemand - , showPrettyFieldThunkS - -- * The implicit @Demand@ interface - , thunk, isThunk - -- * Converting between explicit and implicit representations - , toDemand, fromDemand - ) where - -import qualified Control.Exception as Exception -import qualified GHC.Generics as GHC -import Control.Applicative -import Data.Bifunctor -import System.IO.Unsafe -import Data.Monoid ( Endo(..) ) -import Generics.SOP hiding (Shape) - -import Test.StrictCheck.Shaped -import Test.StrictCheck.Internal.Unevaluated - --------------------------------------------------------- --- The basic types which make up a demand description -- --------------------------------------------------------- - --- | A @Thunk a@ is either an @a@ or a @Thunk@ --- --- When we interleave this type into the @Shape@ of some type, we get the type --- of demands on that type. --- --- @Thunk a@ is isomorphic to a (strict) @Maybe a@. -data Thunk a - = Eval !a - | Thunk - deriving (Eq, Ord, Show, Functor, GHC.Generic) - -instance Applicative Thunk where - pure = Eval - Thunk <*> _ = Thunk - _ <*> Thunk = Thunk - Eval f <*> Eval a = Eval (f a) - -instance Num a => Num (Thunk a) where - (+) = liftA2 (+) - (-) = liftA2 (-) - (*) = liftA2 (*) - abs = fmap abs - signum = fmap signum - fromInteger = Eval . fromInteger - --- | A @Demand@ on some type @a@ is the same shape as that original @a@, but with --- possible @Thunk@s interleaved into it -type Demand - = (%) Thunk - --- | A @PosDemand@ is a "strictly positive" demand, i.e. one where the topmost --- level of the demanded value has definitely been forced --- --- This is the one-level unwrapping of @Demand@, and is useful to express some --- invariants in specifications -type PosDemand a - = Shape a Demand - -{-# COMPLETE E, T #-} - --- | Pattern synonym to abbreviate demand manipulation: @E a = Wrap (Eval a)@ -pattern E :: Shape a Demand -> Demand a -pattern E a = Wrap (Eval a) - --- | Pattern synonym to abbreviate demand manipulation: @T = Wrap Thunk@ -pattern T :: Demand a -pattern T = Wrap Thunk - - ------------------------- --- Implicit interface -- ------------------------- - - --- | A bottom value (inhabiting all types) which StrictCheck interprets as --- an unevaluated subpart of a data structure --- --- > toDemand thunk == T --- > fromDemand T == thunk -thunk :: forall a. a -thunk = Exception.throw Unevaluated - --- | Tests if a particular value is an implicit 'thunk' --- --- In order to work, this function evaluates its input to weak-head normal form; --- keep this in mind if you care about laziness. -isThunk :: Shaped a => a -> Bool -isThunk a = - case toDemand a of - T -> True - _ -> False - --- | Given an @a@ whose substructures may contain 'thunk's (i.e. an implicit --- demand representation), convert it to an explicit 'Demand' --- --- Inverse to 'fromDemand'. -toDemand :: Shaped a => a -> Demand a -toDemand = interleave toThunk - where - {-# NOINLINE toThunk #-} - toThunk :: a -> Thunk a - toThunk a = unsafePerformIO $ - Exception.catch - (let !_ = a in return (Eval a)) - (\(_ :: Unevaluated) -> return Thunk) - --- | Given an explicit @Demand@ for some type @a@, convert it to a value of type --- @a@, substituting a 'thunk' for each 'T' found in the explicit demand --- --- Inverse to 'toDemand'. -fromDemand :: Shaped a => Demand a -> a -fromDemand = fuse fromThunk - where - {-# NOINLINE fromThunk #-} - fromThunk :: Thunk a -> a - fromThunk (Eval a) = a - fromThunk Thunk = - Exception.throw Unevaluated - ------------------------ --- Shrinking demands -- ------------------------ - --- | Shrink a non-zero demand (analogous to QuickCheck's @shrink@) --- --- While QuickCheck's typical @shrink@ instances reduce the size of a value by --- slicing off the top-most structure, @shrinkDemand@ reduces the size of a --- demand by pruning it's deepest /leaves/. This ensures that all resultant --- shrunken demands are strict sub-demands of the original. -shrinkDemand :: forall a. Shaped a => PosDemand a -> [PosDemand a] -shrinkDemand d = - match @a d d $ \(Flattened un flat) _ -> - un <$> shrinkOne flat - where - shrinkOne :: All Shaped xs => NP Demand xs -> [NP Demand xs] - shrinkOne Nil = [] - shrinkOne (T :* xs) = - (T :*) <$> shrinkOne xs - shrinkOne ((E f :: Demand x) :* xs) = - fmap ((:* xs) . E) (shrinkDemand @x f) - ++ fmap (E f :* ) (shrinkOne xs) - - ------------------------------------- --- Evaluating demands as contexts -- ------------------------------------- - --- | Evaluate some value of type @a@ to the degree specified by the given demand --- --- If the demand and the value diverge (they pick a different side of a sum), --- evaluation will stop at this point. Usually, @evaluateDemand@ is only called --- on demands which are known to be structurally-compatible with the --- accompanying value, although nothing really goes wrong if this is not true. -evaluateDemand :: forall a. Shaped a => PosDemand a -> a -> () -evaluateDemand demand value = - go @a (E demand) (I % value) - where - go :: forall x. Shaped x => Thunk % x -> I % x -> () - go T _ = () - go (E d) (Wrap (I v)) = - match @x d v $ - \(Flattened _ fieldsD) -> maybe () $ - \(Flattened _ fieldsV) -> - foldr seq () . hcollapse $ - hcliftA2 (Proxy @Shaped) ((K .) . go) fieldsD fieldsV - - ------------------------------ --- Pretty-printing demands -- ------------------------------ - --- | A very general 'showsPrec' style function for printing demands --- --- @showPrettyFieldThunkS q t p r@ returns a function @(String -> String)@ which --- appends its input to a pretty-printed representation of a demand. --- --- Specifically: --- * @q@ is a boolean flag determining if names should be printed --- as qualified --- * @t@ is a string which is to be printed when a thunk is encountered --- * @p@ is the precedence context of this function call --- * @r@ is the 'Rendered Thunk' representing some demand --- --- This is very general, but we expose it in its complexity just in case some --- person wants to build a different pretty-printer. --- --- The precedence-aware pretty-printing algorithm used here is adapted from a --- solution given by Brian Huffman on StackOverflow: --- . -showPrettyFieldThunkS - :: Bool -> String -> Int -> Rendered Thunk -> String -> String -showPrettyFieldThunkS _ t _ (RWrap Thunk) = (t ++) -showPrettyFieldThunkS qualifyNames t prec (RWrap (Eval pd)) = - case pd of - ConstructorD name fields -> - showParen (prec > 10 && length fields > 0) $ - showString (qualify name) - . flip foldMapCompose fields - (((' ' :) .) . showPrettyFieldThunkS qualifyNames t 11) - RecordD name recfields -> - showParen (prec > 10) $ - showString (qualify name) - . flip foldMapCompose recfields - (\(fName, x) -> - ((((" " ++ qualify fName ++ " = ") ++) .) $ - showPrettyFieldThunkS qualifyNames t 11 x)) - InfixD name assoc fixity l r -> - showParen (prec > fixity) $ - let (lprec, rprec) = - case assoc of - LeftAssociative -> (fixity, fixity + 1) - RightAssociative -> (fixity + 1, fixity) - NotAssociative -> (fixity + 1, fixity + 1) - in showPrettyFieldThunkS qualifyNames t lprec l - . showString (" " ++ qualify name ++ " ") - . showPrettyFieldThunkS qualifyNames t rprec r - CustomD fixity list -> - showParen (prec > fixity) $ - foldr (.) id $ flip fmap list $ - extractEither - . bimap (showString . qualifyEither) - (\(f, pf) -> showPrettyFieldThunkS qualifyNames t f pf) - where - qualify (m, _, n) = - if qualifyNames then (m ++ "." ++ n) else n - - qualifyEither (Left s) = s - qualifyEither (Right (m, n)) = - if qualifyNames then (m ++ "." ++ n) else n - - extractEither (Left x) = x - extractEither (Right x) = x - - foldMapCompose :: (a -> (b -> b)) -> [a] -> (b -> b) - foldMapCompose f = appEndo . foldMap (Endo . f) - --- | Pretty-print a demand for display, given the precendence context -prettyDemandPrec :: Shaped a => Int -> Demand a -> ShowS -prettyDemandPrec prec d = - showPrettyFieldThunkS False "_" prec (renderfold d) - --- | Pretty-print a demand for display -prettyDemand :: Shaped a => Demand a -> String -prettyDemand d = prettyDemandPrec 0 d "" - --- | Print a demand to standard output --- --- > printDemand = putStrLn . prettyDemand -printDemand :: Shaped a => Demand a -> IO () -printDemand = putStrLn . prettyDemand - -instance Shaped a => Show (Demand a) where - showsPrec = prettyDemandPrec - --- TODO: Comparisons module? - --- | Determine if two demands are exactly equal --- --- This relies on the @match@ method from the @Shaped@ instance for the two --- demands, and does not require the underlying types to have @Eq@ instances. --- However, this means that types whose @match@ methods are more coarse than --- their equality will be compared differently by @eqDemand@. In particular, --- the demand representations of functions will all be compared to be equal. -eqDemand :: forall a. Shaped a => Demand a -> Demand a -> Bool -eqDemand T T = True -eqDemand T (E _) = False -eqDemand (E _) T = False -eqDemand (E d1) (E d2) = - match @a d1 d2 $ - \(Flattened _ flatD1) -> maybe False $ - \(Flattened _ flatD2) -> - all id . hcollapse $ - hcliftA2 (Proxy @Shaped) - ((K .) . eqDemand) flatD1 flatD2 - --- | 'Demand's are compared for equality using 'eqDemand'; see its documentation --- for details -instance Shaped a => Eq (Demand a) where - (==) = eqDemand +{-| A 'Demand' on some value of type @T@ is shaped like a @T@, but possibly + truncated, to represent partial evaluation. This module defines the type of + demands, and functions to manipulate them for the purpose of constructing + demand specifications. + + A demand for some type @T@ can be represented one of two interconvertible + ways: + + * explicitly, as a recursively interleaved @Shape@ of @T@ + * implicitly, as a value of @T@ with specially-tagged bottom values + which represent un-evaluated portions of that value + + The explicit representation is useful for writing traversals and other such + manipulations of demand values, while the implicit representation can prove + convenient for writing demand specifications. The implicit representation is + the default when writing specifications, but through the use of 'toDemand' + and 'fromDemand', either representation can be used wherever it is most + appropriate. +-} +module Test.StrictCheck.Demand + ( -- * The explicit @Demand@ interface + Thunk(..) + , Demand, PosDemand + , pattern E, pattern T + -- ** Manipulating explicit @Demand@s + , evaluateDemand + , shrinkDemand + , prettyDemand, printDemand + , eqDemand + , showPrettyFieldThunkS + -- * The implicit @Demand@ interface + , thunk, isThunk + -- * Converting between explicit and implicit representations + , toDemand, fromDemand + ) where + +import qualified Control.Exception as Exception +import qualified GHC.Generics as GHC +import Control.Applicative (liftA2) -- for GHC 9.2 +import Data.Bifunctor +import System.IO.Unsafe +import Data.Monoid ( Endo(..) ) +import Generics.SOP hiding (Shape) + +import Test.StrictCheck.Shaped +import Test.StrictCheck.Internal.Unevaluated + +-------------------------------------------------------- +-- The basic types which make up a demand description -- +-------------------------------------------------------- + +-- | A @Thunk a@ is either an @a@ or a @Thunk@ +-- +-- When we interleave this type into the @Shape@ of some type, we get the type +-- of demands on that type. +-- +-- @Thunk a@ is isomorphic to a (strict) @Maybe a@. +data Thunk a + = Eval !a + | Thunk + deriving (Eq, Ord, Show, Functor, GHC.Generic) + +instance Applicative Thunk where + pure = Eval + Thunk <*> _ = Thunk + _ <*> Thunk = Thunk + Eval f <*> Eval a = Eval (f a) + +instance Num a => Num (Thunk a) where + (+) = liftA2 (+) + (-) = liftA2 (-) + (*) = liftA2 (*) + abs = fmap abs + signum = fmap signum + fromInteger = Eval . fromInteger + +-- | A @Demand@ on some type @a@ is the same shape as that original @a@, but with +-- possible @Thunk@s interleaved into it +type Demand + = (%) Thunk + +-- | A @PosDemand@ is a "strictly positive" demand, i.e. one where the topmost +-- level of the demanded value has definitely been forced +-- +-- This is the one-level unwrapping of @Demand@, and is useful to express some +-- invariants in specifications +type PosDemand a + = Shape a Demand + +{-# COMPLETE E, T #-} + +-- | Pattern synonym to abbreviate demand manipulation: @E a = Wrap (Eval a)@ +pattern E :: Shape a Demand -> Demand a +pattern E a = Wrap (Eval a) + +-- | Pattern synonym to abbreviate demand manipulation: @T = Wrap Thunk@ +pattern T :: Demand a +pattern T = Wrap Thunk + + +------------------------ +-- Implicit interface -- +------------------------ + + +-- | A bottom value (inhabiting all types) which StrictCheck interprets as +-- an unevaluated subpart of a data structure +-- +-- > toDemand thunk == T +-- > fromDemand T == thunk +thunk :: forall a. a +thunk = Exception.throw Unevaluated + +-- | Tests if a particular value is an implicit 'thunk' +-- +-- In order to work, this function evaluates its input to weak-head normal form; +-- keep this in mind if you care about laziness. +isThunk :: Shaped a => a -> Bool +isThunk a = + case toDemand a of + T -> True + _ -> False + +-- | Given an @a@ whose substructures may contain 'thunk's (i.e. an implicit +-- demand representation), convert it to an explicit 'Demand' +-- +-- Inverse to 'fromDemand'. +toDemand :: Shaped a => a -> Demand a +toDemand = interleave toThunk + where + {-# NOINLINE toThunk #-} + toThunk :: a -> Thunk a + toThunk a = unsafePerformIO $ + Exception.catch + (let !_ = a in return (Eval a)) + (\(_ :: Unevaluated) -> return Thunk) + +-- | Given an explicit @Demand@ for some type @a@, convert it to a value of type +-- @a@, substituting a 'thunk' for each 'T' found in the explicit demand +-- +-- Inverse to 'toDemand'. +fromDemand :: Shaped a => Demand a -> a +fromDemand = fuse fromThunk + where + {-# NOINLINE fromThunk #-} + fromThunk :: Thunk a -> a + fromThunk (Eval a) = a + fromThunk Thunk = + Exception.throw Unevaluated + +----------------------- +-- Shrinking demands -- +----------------------- + +-- | Shrink a non-zero demand (analogous to QuickCheck's @shrink@) +-- +-- While QuickCheck's typical @shrink@ instances reduce the size of a value by +-- slicing off the top-most structure, @shrinkDemand@ reduces the size of a +-- demand by pruning it's deepest /leaves/. This ensures that all resultant +-- shrunken demands are strict sub-demands of the original. +shrinkDemand :: forall a. Shaped a => PosDemand a -> [PosDemand a] +shrinkDemand d = + match @a d d $ \(Flattened un flat) _ -> + un <$> shrinkOne flat + where + shrinkOne :: All Shaped xs => NP Demand xs -> [NP Demand xs] + shrinkOne Nil = [] + shrinkOne (T :* xs) = + (T :*) <$> shrinkOne xs + shrinkOne ((E f :: Demand x) :* xs) = + fmap ((:* xs) . E) (shrinkDemand @x f) + ++ fmap (E f :* ) (shrinkOne xs) + + +------------------------------------ +-- Evaluating demands as contexts -- +------------------------------------ + +-- | Evaluate some value of type @a@ to the degree specified by the given demand +-- +-- If the demand and the value diverge (they pick a different side of a sum), +-- evaluation will stop at this point. Usually, @evaluateDemand@ is only called +-- on demands which are known to be structurally-compatible with the +-- accompanying value, although nothing really goes wrong if this is not true. +evaluateDemand :: forall a. Shaped a => PosDemand a -> a -> () +evaluateDemand demand value = + go @a (E demand) (I % value) + where + go :: forall x. Shaped x => Thunk % x -> I % x -> () + go T _ = () + go (E d) (Wrap (I v)) = + match @x d v $ + \(Flattened _ fieldsD) -> maybe () $ + \(Flattened _ fieldsV) -> + foldr seq () . hcollapse $ + hcliftA2 (Proxy @Shaped) ((K .) . go) fieldsD fieldsV + + +----------------------------- +-- Pretty-printing demands -- +----------------------------- + +-- | A very general 'showsPrec' style function for printing demands +-- +-- @showPrettyFieldThunkS q t p r@ returns a function @(String -> String)@ which +-- appends its input to a pretty-printed representation of a demand. +-- +-- Specifically: +-- * @q@ is a boolean flag determining if names should be printed +-- as qualified +-- * @t@ is a string which is to be printed when a thunk is encountered +-- * @p@ is the precedence context of this function call +-- * @r@ is the 'Rendered Thunk' representing some demand +-- +-- This is very general, but we expose it in its complexity just in case some +-- person wants to build a different pretty-printer. +-- +-- The precedence-aware pretty-printing algorithm used here is adapted from a +-- solution given by Brian Huffman on StackOverflow: +-- . +showPrettyFieldThunkS + :: Bool -> String -> Int -> Rendered Thunk -> String -> String +showPrettyFieldThunkS _ t _ (RWrap Thunk) = (t ++) +showPrettyFieldThunkS qualifyNames t prec (RWrap (Eval pd)) = + case pd of + ConstructorD name fields -> + showParen (prec > 10 && length fields > 0) $ + showString (qualify name) + . flip foldMapCompose fields + (((' ' :) .) . showPrettyFieldThunkS qualifyNames t 11) + RecordD name recfields -> + showParen (prec > 10) $ + showString (qualify name) + . flip foldMapCompose recfields + (\(fName, x) -> + ((((" " ++ qualify fName ++ " = ") ++) .) $ + showPrettyFieldThunkS qualifyNames t 11 x)) + InfixD name assoc fixity l r -> + showParen (prec > fixity) $ + let (lprec, rprec) = + case assoc of + LeftAssociative -> (fixity, fixity + 1) + RightAssociative -> (fixity + 1, fixity) + NotAssociative -> (fixity + 1, fixity + 1) + in showPrettyFieldThunkS qualifyNames t lprec l + . showString (" " ++ qualify name ++ " ") + . showPrettyFieldThunkS qualifyNames t rprec r + CustomD fixity list -> + showParen (prec > fixity) $ + foldr (.) id $ flip fmap list $ + extractEither + . bimap (showString . qualifyEither) + (\(f, pf) -> showPrettyFieldThunkS qualifyNames t f pf) + where + qualify (m, _, n) = + if qualifyNames then (m ++ "." ++ n) else n + + qualifyEither (Left s) = s + qualifyEither (Right (m, n)) = + if qualifyNames then (m ++ "." ++ n) else n + + extractEither (Left x) = x + extractEither (Right x) = x + + foldMapCompose :: (a -> (b -> b)) -> [a] -> (b -> b) + foldMapCompose f = appEndo . foldMap (Endo . f) + +-- | Pretty-print a demand for display, given the precendence context +prettyDemandPrec :: Shaped a => Int -> Demand a -> ShowS +prettyDemandPrec prec d = + showPrettyFieldThunkS False "_" prec (renderfold d) + +-- | Pretty-print a demand for display +prettyDemand :: Shaped a => Demand a -> String +prettyDemand d = prettyDemandPrec 0 d "" + +-- | Print a demand to standard output +-- +-- > printDemand = putStrLn . prettyDemand +printDemand :: Shaped a => Demand a -> IO () +printDemand = putStrLn . prettyDemand + +instance Shaped a => Show (Demand a) where + showsPrec = prettyDemandPrec + +-- TODO: Comparisons module? + +-- | Determine if two demands are exactly equal +-- +-- This relies on the @match@ method from the @Shaped@ instance for the two +-- demands, and does not require the underlying types to have @Eq@ instances. +-- However, this means that types whose @match@ methods are more coarse than +-- their equality will be compared differently by @eqDemand@. In particular, +-- the demand representations of functions will all be compared to be equal. +eqDemand :: forall a. Shaped a => Demand a -> Demand a -> Bool +eqDemand T T = True +eqDemand T (E _) = False +eqDemand (E _) T = False +eqDemand (E d1) (E d2) = + match @a d1 d2 $ + \(Flattened _ flatD1) -> maybe False $ + \(Flattened _ flatD2) -> + all id . hcollapse $ + hcliftA2 (Proxy @Shaped) + ((K .) . eqDemand) flatD1 flatD2 + +-- | 'Demand's are compared for equality using 'eqDemand'; see its documentation +-- for details +instance Shaped a => Eq (Demand a) where + (==) = eqDemand diff --git a/src/Test/StrictCheck/Examples/Lists.hs b/src/Test/StrictCheck/Examples/Lists.hs --- a/src/Test/StrictCheck/Examples/Lists.hs +++ b/src/Test/StrictCheck/Examples/Lists.hs @@ -1,266 +1,272 @@ -{-| This module defines a variety of specifications for functions on lists, - demonstrating the specification interface of StrictCheck. See the - documentation of "Test.StrictCheck" (specifically 'strictCheckSpecExact') - for details on how to test these specifications. - - This module's primary utility is to teach how specifications work. Because - Haddock omits the definitions of values, you'll learn the most by viewing - the source of this module. --} -module Test.StrictCheck.Examples.Lists where - -import Test.StrictCheck -import Data.Functor - --- * Specifying some simple functions on lists - --- | A correct specification for 'length' -length_spec :: Spec '[[a]] Int -length_spec = - Spec $ \predict _ xs -> - predict (xs $> thunk) - --- | A naive specification for 'take', which is wrong -take_spec_too_easy :: Spec '[Int, [a]] [a] -take_spec_too_easy = - Spec $ \predict _d n xs -> - predict n xs - --- | A correct specification for 'take' -take_spec :: Spec '[Int, [a]] [a] -take_spec = - Spec $ \predict d n xs -> - predict n (if n > length xs then d else d ++ thunk) - --- | A functionally correct implementation of 'take' which has subtly different --- strictness properties --- --- This will fail when tested against 'take_spec'. -take' :: Int -> [a] -> [a] -take' _ [] = [] -take' n (x : xs) - | n > 0 = x : take' (n-1) xs - | otherwise = [] - --- | A correct specification of '(++)' -append_spec :: Shaped a => Spec '[[a], [a]] [a] -append_spec = - Spec $ \predict d ls rs -> - let spineLen = length . cap $ d ++ [undefined] -- number of spine thunks forced - overLs = spineLen > length ls -- forced all of ls? - overRs = spineLen > length ls + length rs -- forced all of bs? - (ls', rs') = splitAt (length ls) (cap d) - in predict - (ls' ++ if overLs then [] else thunk) - (rs' ++ if overRs then [] else thunk) - --- | A correct specification of 'reverse' -reverse_spec :: Shaped a => Spec '[[a]] [a] -reverse_spec = - Spec $ \predict d xs -> - let padLen = length xs - length (cap d) - spinePad = replicate padLen thunk - in predict $ spinePad ++ (reverse (cap d)) - --- | A correct specification for 'zip' -zip_spec :: (Shaped a, Shaped b) => Spec '[[a], [b]] [(a, b)] -zip_spec = - Spec $ \predict d as bs -> - let (d_as, d_bs) = unzip d - in predict - (if length (cap d_bs) > length as - && not (length (cap d_as) > length bs) - then d_as - else d_as ++ thunk) - (if length (cap d_as) > length bs - && not (length (cap d_bs) > length as) - then d_bs - else d_bs ++ thunk) - --- | A functionally correct implementation of 'zip' which has subtly different --- strictness properties --- --- This will fail when tested against 'zip_spec'. -zip' :: [a] -> [b] -> [(a, b)] -zip' [ ] [ ] = [] -zip' (_ : as) [ ] = zip' as [] -zip' [ ] (_ : bs) = zip' [] bs -zip' (a : as) (b : bs) = (a, b) : zip' as bs - --- | A correct specification for 'map', demonstrating specifications for --- higher-order functions -map_spec - :: forall a b. (Shaped a, Shaped b) - => Spec '[a -> b, [a]] [b] -map_spec = - Spec $ \predict d f xs -> - predict - (if all isThunk (cap d) then thunk else f) - (zipWith (specify1 f) d xs) - --- * Specifying the productive rotate function from Okasaki's purely functional --- queue implementation (see paper for more details) - --- | Given three lists @xs@, @ys@, and @zs@, compute @xs ++ reverse ys ++ zs@, --- but with more uniform strictness --- --- Specifically, if @ys@ is shorter than @xs@, the work necessary to reverse it --- will have already occurred by the time @xs@ is traversed. -rotate :: [a] -> [a] -> [a] -> [a] -rotate [ ] [ ] as = as -rotate [ ] (b : bs) as = rotate [] bs (b : as) -rotate (f : fs) [ ] as = f : rotate fs [] as -rotate (f : fs) (b : bs) as = f : rotate fs bs (b : as) - --- | Specialization of 'rotate': @rot xs ys = rotate xs ys []@ -rot :: [a] -> [a] -> [a] -rot fs bs = rotate fs bs [] - --- | The naive version of 'rot': @rot' xs ys = xs ++ reverse ys@ --- --- This is functionally equivalent to 'rot' but not equivalent in strictness --- behavior. -rot' :: [a] -> [a] -> [a] -rot' fs bs = fs ++ reverse bs - --- | A previous iteration of `rot_spec'`, this one is also correct, but may be --- less readable. -rot_spec :: Shaped a => Spec '[[a], [a]] [a] -rot_spec = - Spec $ \predict d fs bs -> - let (fs', bs') = splitAt (length fs) (cap d) - spineLen = length (cap (d ++ [undefined])) -- # of spine thunks forced - overflow = spineLen > length fs -- begun taking from bs? - overrot = length (cap d) > length bs -- forced all of bs? - padLength = - length bs `min` - if overflow - then length bs - length bs' - else length (cap d) - spinePad = replicate padLength thunk - in predict - ( fs' ++ if overflow then [] else thunk) - (spinePad ++ reverse bs' ++ if overflow || overrot then [] else thunk) - --- | A correct specification of `rot`, this is also the version we presented in --- the paper. -rot_spec' :: Shaped a => Spec '[[a], [a]] [a] -rot_spec' = - Spec $ \predict d fs bs -> - let demandOnFs - | length (cap d) > length fs = - take (length fs) (cap d) - | otherwise = d - demandOnBs - | length (cap $ d ++ [undefined]) > length fs = - reverse $ take (length bs) - $ drop (length fs) (cap d) ++ repeat thunk - | length (cap d) > length bs = - reverse $ drop (length fs) (cap d) ++ replicate (length bs) thunk - | otherwise = - (reverse $ drop (length fs) (cap d) ++ replicate (length (cap d)) thunk) ++ thunk - in predict demandOnFs demandOnBs --- where predictedFsDemand --- | outputDemandLength < length fs = --- outputDemand ++ thunk --- | otherwise = --- fsPartOfOutDemand --- predictedBsDemand --- | outputDemandLength < length bs = --- --- | otherwise = --- --- let (fs', bs') = splitAt (length fs) (cap d) --- spineLen = length (cap (d ++ [undefined])) -- # of spine thunks forced --- overflow = spineLen > length fs -- begun taking from bs? --- overrot = length (cap d) > length bs -- forced all of bs? --- padLength = --- length bs `min` --- if overflow --- then length bs - length bs' --- else length (cap d) --- spinePad = replicate padLength thunk --- in predict --- ( fs' ++ if overflow then [] else thunk) --- (spinePad ++ reverse bs' ++ if overflow || overrot then [] else thunk) - ---rot_spec' :: Shaped a => Spec '[[a], [a]] [a] ---rot_spec' = rot_spec - --- | An incorrect specification for `rot` that miscalculates the number of cells --- forced. -rot_simple_spec :: Shaped a => Spec '[[a], [a]] [a] -rot_simple_spec = - Spec $ \predict d fs bs -> - let demandOnFs - | length (cap d) > length fs = - take (length fs) d - | otherwise = d - demandOnBs - | length (cap d) > length fs || - (null bs && length fs == length (cap d) && length fs /= length (cap $ d ++ [thunk])) = - reverse $ take (length bs) $ (drop (length fs) (cap d)) ++ repeat thunk - | otherwise = - thunk - in predict demandOnFs demandOnBs - -test_rot :: [Int] -> [Int] -> [Int] -> IO () -test_rot d xs ys = - (\(x :* y :* Nil) -> printDemand x >> printDemand y) - . snd $ observe (toContext d) (rot @Int) xs ys - --- * Utilities for working with demands over lists - --- | If the tail of the second list is 'thunk', replace it with the first list -replaceThunk :: Shaped a => [a] -> [a] -> [a] -replaceThunk r xs | isThunk xs = r -replaceThunk _ [ ] = [] -replaceThunk r (x : xs) = x : replaceThunk r xs - --- | If the tail of the list is 'thunk', replace it with @[]@ --- --- This is a special case of 'replaceThunk'. -cap :: Shaped a => [a] -> [a] -cap = replaceThunk [] - --- | Lift an ordinary function to apply to explicit 'Demand's --- --- It is true that @Demand@s are a functor, but they can't be a Haskell --- 'Functor' because they're a type family -(%$) :: (Shaped a, Shaped b) => (a -> b) -> Demand a -> Demand b -(%$) f = toDemand . f . fromDemand - --- | Apply a 'Demand' on a function to a 'Demand' on a value --- --- It is true that @Demand@s are an applicative functor, but they can't be a --- Haskell 'Functor' because they're a type family -(%*) :: (Shaped a, Shaped b) => Demand (a -> b) -> Demand a -> Demand b -f %* a = toDemand $ fromDemand f (fromDemand a) - --- TODO: make n-ary version of this (CPS-ed) --- | Given a unary function, an implicit demand on its result, and its input, --- compute its actual demand on its input in that context --- --- This demand is calculated using 'observe1', so it is guaranteed to be --- correct. -specify1 :: forall a b. (Shaped a, Shaped b) - => (a -> b) -> b -> a -> a -specify1 f b a = - fromDemand . snd $ observe1 (toContext b) f a - --- | Given an implicit demand, convert it to an evaluation context --- --- That is, @toContext d a@ evaluates @a@ to the degree that @d@ is a defined --- value. This uses the function 'evaluateDemand'; refer to its documentation --- for details about how demands are used to evaluate values. -toContext :: Shaped b => b -> b -> () -toContext b = - case toDemand b of - T -> const () - E b' -> evaluateDemand b' - --- | Assert at runtime that a value is /not/ a 'thunk', failing with an error --- if it is -expectTotal :: Shaped a => a -> a -expectTotal a = - if isThunk a then error "expectTotal: given thunk" else a +{-| This module defines a variety of specifications for functions on lists, + demonstrating the specification interface of StrictCheck. See the + documentation of "Test.StrictCheck" (specifically 'strictCheckSpecExact') + for details on how to test these specifications. + + This module's primary utility is to teach how specifications work. Because + Haddock omits the definitions of values, you'll learn the most by viewing + the source of this module. +-} +module Test.StrictCheck.Examples.Lists where + +import Test.StrictCheck +import Data.Functor (($>)) + +-- * Specifying some simple functions on lists + +-- | A correct specification for 'length' +length_spec :: Spec '[[a]] Int +length_spec = + Spec $ \predict _ xs -> + predict (xs $> thunk) + +-- | An incorrect specification for 'length' (to test the pretty printer) +bad_length_spec :: Spec '[[a]] Int +bad_length_spec = + Spec $ \predict _ xs -> + predict (take 1 xs $> thunk) + +-- | A naive specification for 'take', which is wrong +take_spec_too_easy :: Spec '[Int, [a]] [a] +take_spec_too_easy = + Spec $ \predict _d n xs -> + predict n xs + +-- | A correct specification for 'take' +take_spec :: Spec '[Int, [a]] [a] +take_spec = + Spec $ \predict d n xs -> + predict n (if n > length xs then d else d ++ thunk) + +-- | A functionally correct implementation of 'take' which has subtly different +-- strictness properties +-- +-- This will fail when tested against 'take_spec'. +take' :: Int -> [a] -> [a] +take' _ [] = [] +take' n (x : xs) + | n > 0 = x : take' (n-1) xs + | otherwise = [] + +-- | A correct specification of '(++)' +append_spec :: Shaped a => Spec '[[a], [a]] [a] +append_spec = + Spec $ \predict d ls rs -> + let spineLen = length . cap $ d ++ [undefined] -- number of spine thunks forced + overLs = spineLen > length ls -- forced all of ls? + overRs = spineLen > length ls + length rs -- forced all of bs? + (ls', rs') = splitAt (length ls) (cap d) + in predict + (ls' ++ if overLs then [] else thunk) + (rs' ++ if overRs then [] else thunk) + +-- | A correct specification of 'reverse' +reverse_spec :: Shaped a => Spec '[[a]] [a] +reverse_spec = + Spec $ \predict d xs -> + let padLen = length xs - length (cap d) + spinePad = replicate padLen thunk + in predict $ spinePad ++ (reverse (cap d)) + +-- | A correct specification for 'zip' +zip_spec :: (Shaped a, Shaped b) => Spec '[[a], [b]] [(a, b)] +zip_spec = + Spec $ \predict d as bs -> + let (d_as, d_bs) = unzip d + in predict + (if length (cap d_bs) > length as + && not (length (cap d_as) > length bs) + then d_as + else d_as ++ thunk) + (if length (cap d_as) > length bs + && not (length (cap d_bs) > length as) + then d_bs + else d_bs ++ thunk) + +-- | A functionally correct implementation of 'zip' which has subtly different +-- strictness properties +-- +-- This will fail when tested against 'zip_spec'. +zip' :: [a] -> [b] -> [(a, b)] +zip' [ ] [ ] = [] +zip' (_ : as) [ ] = zip' as [] +zip' [ ] (_ : bs) = zip' [] bs +zip' (a : as) (b : bs) = (a, b) : zip' as bs + +-- | A correct specification for 'map', demonstrating specifications for +-- higher-order functions +map_spec + :: forall a b. (Shaped a, Shaped b) + => Spec '[a -> b, [a]] [b] +map_spec = + Spec $ \predict d f xs -> + predict + (if all isThunk (cap d) then thunk else f) + (zipWith (specify1 f) d xs) + +-- * Specifying the productive rotate function from Okasaki's purely functional +-- queue implementation (see paper for more details) + +-- | Given three lists @xs@, @ys@, and @zs@, compute @xs ++ reverse ys ++ zs@, +-- but with more uniform strictness +-- +-- Specifically, if @ys@ is shorter than @xs@, the work necessary to reverse it +-- will have already occurred by the time @xs@ is traversed. +rotate :: [a] -> [a] -> [a] -> [a] +rotate [ ] [ ] as = as +rotate [ ] (b : bs) as = rotate [] bs (b : as) +rotate (f : fs) [ ] as = f : rotate fs [] as +rotate (f : fs) (b : bs) as = f : rotate fs bs (b : as) + +-- | Specialization of 'rotate': @rot xs ys = rotate xs ys []@ +rot :: [a] -> [a] -> [a] +rot fs bs = rotate fs bs [] + +-- | The naive version of 'rot': @rot' xs ys = xs ++ reverse ys@ +-- +-- This is functionally equivalent to 'rot' but not equivalent in strictness +-- behavior. +rot' :: [a] -> [a] -> [a] +rot' fs bs = fs ++ reverse bs + +-- | A previous iteration of `rot_spec'`, this one is also correct, but may be +-- less readable. +rot_spec :: Shaped a => Spec '[[a], [a]] [a] +rot_spec = + Spec $ \predict d fs bs -> + let (fs', bs') = splitAt (length fs) (cap d) + spineLen = length (cap (d ++ [undefined])) -- # of spine thunks forced + overflow = spineLen > length fs -- begun taking from bs? + overrot = length (cap d) > length bs -- forced all of bs? + padLength = + length bs `min` + if overflow + then length bs - length bs' + else length (cap d) + spinePad = replicate padLength thunk + in predict + ( fs' ++ if overflow then [] else thunk) + (spinePad ++ reverse bs' ++ if overflow || overrot then [] else thunk) + +-- | A correct specification of `rot`, this is also the version we presented in +-- the paper. +rot_spec' :: Shaped a => Spec '[[a], [a]] [a] +rot_spec' = + Spec $ \predict d fs bs -> + let demandOnFs + | length (cap d) > length fs = + take (length fs) (cap d) + | otherwise = d + demandOnBs + | length (cap $ d ++ [undefined]) > length fs = + reverse $ take (length bs) + $ drop (length fs) (cap d) ++ repeat thunk + | length (cap d) > length bs = + reverse $ drop (length fs) (cap d) ++ replicate (length bs) thunk + | otherwise = + (reverse $ drop (length fs) (cap d) ++ replicate (length (cap d)) thunk) ++ thunk + in predict demandOnFs demandOnBs +-- where predictedFsDemand +-- | outputDemandLength < length fs = +-- outputDemand ++ thunk +-- | otherwise = +-- fsPartOfOutDemand +-- predictedBsDemand +-- | outputDemandLength < length bs = +-- +-- | otherwise = +-- +-- let (fs', bs') = splitAt (length fs) (cap d) +-- spineLen = length (cap (d ++ [undefined])) -- # of spine thunks forced +-- overflow = spineLen > length fs -- begun taking from bs? +-- overrot = length (cap d) > length bs -- forced all of bs? +-- padLength = +-- length bs `min` +-- if overflow +-- then length bs - length bs' +-- else length (cap d) +-- spinePad = replicate padLength thunk +-- in predict +-- ( fs' ++ if overflow then [] else thunk) +-- (spinePad ++ reverse bs' ++ if overflow || overrot then [] else thunk) + +--rot_spec' :: Shaped a => Spec '[[a], [a]] [a] +--rot_spec' = rot_spec + +-- | An incorrect specification for `rot` that miscalculates the number of cells +-- forced. +rot_simple_spec :: Shaped a => Spec '[[a], [a]] [a] +rot_simple_spec = + Spec $ \predict d fs bs -> + let demandOnFs + | length (cap d) > length fs = + take (length fs) d + | otherwise = d + demandOnBs + | length (cap d) > length fs || + (null bs && length fs == length (cap d) && length fs /= length (cap $ d ++ [thunk])) = + reverse $ take (length bs) $ (drop (length fs) (cap d)) ++ repeat thunk + | otherwise = + thunk + in predict demandOnFs demandOnBs + +test_rot :: [Int] -> [Int] -> [Int] -> IO () +test_rot d xs ys = + (\(x :* y :* Nil) -> printDemand x >> printDemand y) + . snd $ observe (toContext d) (rot @Int) xs ys + +-- * Utilities for working with demands over lists + +-- | If the tail of the second list is 'thunk', replace it with the first list +replaceThunk :: Shaped a => [a] -> [a] -> [a] +replaceThunk r xs | isThunk xs = r +replaceThunk _ [ ] = [] +replaceThunk r (x : xs) = x : replaceThunk r xs + +-- | If the tail of the list is 'thunk', replace it with @[]@ +-- +-- This is a special case of 'replaceThunk'. +cap :: Shaped a => [a] -> [a] +cap = replaceThunk [] + +-- | Lift an ordinary function to apply to explicit 'Demand's +-- +-- It is true that @Demand@s are a functor, but they can't be a Haskell +-- 'Functor' because they're a type family +(%$) :: (Shaped a, Shaped b) => (a -> b) -> Demand a -> Demand b +(%$) f = toDemand . f . fromDemand + +-- | Apply a 'Demand' on a function to a 'Demand' on a value +-- +-- It is true that @Demand@s are an applicative functor, but they can't be a +-- Haskell 'Functor' because they're a type family +(%*) :: (Shaped a, Shaped b) => Demand (a -> b) -> Demand a -> Demand b +f %* a = toDemand $ fromDemand f (fromDemand a) + +-- TODO: make n-ary version of this (CPS-ed) +-- | Given a unary function, an implicit demand on its result, and its input, +-- compute its actual demand on its input in that context +-- +-- This demand is calculated using 'observe1', so it is guaranteed to be +-- correct. +specify1 :: forall a b. (Shaped a, Shaped b) + => (a -> b) -> b -> a -> a +specify1 f b a = + fromDemand . snd $ observe1 (toContext b) f a + +-- | Given an implicit demand, convert it to an evaluation context +-- +-- That is, @toContext d a@ evaluates @a@ to the degree that @d@ is a defined +-- value. This uses the function 'evaluateDemand'; refer to its documentation +-- for details about how demands are used to evaluate values. +toContext :: Shaped b => b -> b -> () +toContext b = + case toDemand b of + T -> const () + E b' -> evaluateDemand b' + +-- | Assert at runtime that a value is /not/ a 'thunk', failing with an error +-- if it is +expectTotal :: Shaped a => a -> a +expectTotal a = + if isThunk a then error "expectTotal: given thunk" else a diff --git a/src/Test/StrictCheck/Examples/Map.hs b/src/Test/StrictCheck/Examples/Map.hs --- a/src/Test/StrictCheck/Examples/Map.hs +++ b/src/Test/StrictCheck/Examples/Map.hs @@ -1,198 +1,198 @@ -{-# LANGUAGE TemplateHaskell, BangPatterns, DerivingStrategies #-} - -{- | This module showcases another type of specification different from those in - "Test.StrictCheck.Examples.Lists". Here, we demonstrate that StrictCheck is - able to distinguish value-lazy maps from value-strict maps. - - In this module, we first develop the solution of the Knapsack dynamic - programming problem by taking the fixpoint of a step function of the solution - table. We represent the solution table with a map, and write a specification - that is critical for the termination of this solution. --} -module Test.StrictCheck.Examples.Map where - -import Prelude hiding (lookup) -import Debug.Trace - -import qualified GHC.Generics as GHC -import Generics.SOP (Generic, HasDatatypeInfo, NS(..), hd, tl) - -import Test.StrictCheck -import Test.StrictCheck.TH - -import Data.Maybe -import Data.Function - -import Test.QuickCheck - --- | We roll our own map type to avoid dealing with abstract types. -data Map k v = Bin (Map k v) k v (Map k v) -- ^ A node that contains a key value pair - | Empty -- ^ An empty node - deriving stock (GHC.Generic, Show, Eq, Ord) - deriving anyclass (Generic, HasDatatypeInfo, Consume, Shaped) - --- | A specialized map useful for knapsack. The pair of ints represent the two --- parameters to each knapsack sub-problem solved along the way. These two --- parameters determine the subsequence of items each sub-problem is concerned --- with, and the weight limit. -type KMap = Map (Int, Int) Int - -$(derivePatternSynonyms ''Map) - --- | This replaces the thunk in a map partial value with the `r` parameter. This --- is very similar to the `cap` function in the lists example. -replaceThunk :: (Shaped k, Shaped v) => Map k v -> Map k v -> Map k v -replaceThunk r m | isThunk m = r -replaceThunk _ Empty = Empty -replaceThunk r (Bin ml k v mr) = Bin (replaceThunk r ml) k v (replaceThunk r mr) - --- | A helper for building a map from a list of values. -fromList :: [((Int, Int), Int)] -> KMap -fromList = foldr (\(k, v) acc -> insert k v acc) Empty - --- | A simplified insert that ignores rebalancing since rebalancing is not --- important for the spec we will write. -insert :: (Ord k) => k -> v -> Map k v -> Map k v -insert key value Empty = Bin Empty key value Empty -insert key value (Bin ml k v mr) | key < k = Bin (insert key value ml) k v mr - | key > k = Bin ml k v (insert key value mr) - | otherwise = Bin ml key value mr - --- | The lookup function specialized for knapsack. -lookup :: KMap -> (Int, Int) -> Maybe Int -lookup Empty _ = Nothing -lookup (Bin ml k' v mr) k | k == k' = Just v - | k < k' = lookup ml k - | otherwise = lookup mr k - --- | This function extracts all of the keys of a map. -keys :: Map k v -> [k] -keys Empty = [] -keys (Bin ml k _ mr) = keys ml ++ [k] ++ keys mr - --- | A lookup function that returns the default value `0` for keys that are not --- in the map. This saves us from doing repeated pattern matching when querying --- the solution table. -(!) :: KMap -> (Int, Int) -> Int -(!) m k = case lookup m k of - Nothing -> 0 - Just v -> v - --- | Weight parameters to the knapsack problem. -weights :: [Int] -weights = [10, 20, 30] - --- | Value parameters to the knapsack problem, note that this must be the same --- length as `weights`. -values :: [Int] -values = [60, 100, 120] - --- | The weight limit of the knapsack problem. -limit :: Int -limit = 50 - --- | One step of the knapsack computation. This is a direct translation from the --- recurrence relation of the knapsack problem. -solutionStep :: Map (Int, Int) Int -> Map (Int, Int) Int -solutionStep soln = - fromList [((j, k), knapsack j k) | j <- [0 .. length weights-1], k <- [0 .. limit]] - where - knapsack j k = if j - 1 < 0 || k - weights !! j < 0 - then if j >= 0 && weights !! j <= k then values !! j else 0 - else max (soln ! (j-1, k)) - (soln ! (j-1, k - weights !! j) + values !! j) - --- | The fixpoint of the recurrence relation, which is also the solution for the --- knapsack problem. -solution :: Map (Int, Int) Int -solution = fix solutionStep - --- | A pattern synonym for extracting demands of each component from the demand --- of a pair. -pattern Pair' :: Demand a -> Demand b -> Demand (a, b) -pattern Pair' x y = Wrap (Eval (GS (Z (x :* y :* Nil)))) - --- | This function computes the nth pre-fixpoint of the knapsack solution, and --- looks up the value at the specified cell from the pre-fixpoint. -iterSolution :: (Int, Int) -> Int -> Map (Int, Int) Int -> Maybe Int -iterSolution k n soln = lookup m k - where m | n <= 0 = soln - | otherwise = (iterate solutionStep soln) !! n - --- | This is the same as `iterSolution`, but uses a newtype wrapper for the --- index into the map since we want to write a customized `Arbitrary` instance --- for `Key`. -iterSolutionWithKey :: Key -> Int -> Map (Int, Int) Int -> Maybe Int -iterSolutionWithKey (Key k) = iterSolution k - --- | The newtype wrapper of index into the knapsack solution table. -newtype Key = Key { getKey :: (Int, Int) } - deriving stock (GHC.Generic, Show, Eq, Ord) - deriving anyclass (Generic, HasDatatypeInfo, Consume, Shaped) - --- | The customized generator for `Key` that only generates valid keys given the --- problem parameters. -instance Arbitrary Key where - -- Just to make sure keys are within the parameters of the problem - arbitrary = fmap Key $ - (,) <$> elements [0 .. length weights - 1] <*> elements [0 .. limit] - --- | The customized generator for solution tables that only generates valid --- pre-fixpoints. -instance Arbitrary KMap where - -- I need to generate only valid pre-fixpoints, which is either - -- Empty (iterated 0 times), or iterate once on Empty, or twice, and - -- so on - arbitrary = do - NonNegative n <- arbitrary - return $ (iterate solutionStep Empty) !! n - --- | A dummy produce instance for the solution table. -instance Produce KMap where - -- I don't need lazy functions on KMaps. Since the spec only checks - -- whether a particular entry in the KMap is evaluated or not. - produce = arbitrary - --- | A dummy produce instance for the index into the solution table. -instance Produce Key where - -- I don't need lazy functions on keys either. - produce = arbitrary - --- | This IO action ties the spec together with everything built so far, and --- runs the StrictCheck randomized testing framework. -runMapTest :: IO () -runMapTest = strictCheckWithResults - stdArgs{maxSize=100, maxSuccess=1000} - shrinkViaArbitrary - genViaProduce - strictnessViaSized - iterSolution_spec - iterSolutionWithKey >>= print - --- | This is the specification that establishes a property important for the --- termination of `solution`: given any pre-fixpoint of `pre-solution`, forcing --- the value at pre-solution[i][j] should not induce a demand at the (i, j) cell --- of the input that steps to pre-solution, since otherwise this would be an --- infinite loop in the fixpoint. --- The value-lazy `Map` defined in this module satisfies this property. However, --- if we make this `Map` value-strict using BangPatterns, StrictCheck will --- report a failure when `runMapTest` is executed. -iterSolution_spec :: Evaluation '[Key, Int, KMap] (Maybe Int) -> Maybe (Int, Int) -iterSolution_spec (Evaluation args demands dOut) = - let I (Key evalK) = hd args - I nIter = hd (tl args) - dInM = hd (tl (tl demands)) - inM = replaceThunk Empty (fromDemand @KMap dInM) - evalV = lookup inM evalK - in if (inM == Empty) || - isBaseCase evalK || - nIter <= 0 || - isThunk evalV || - isNothing evalV - then Nothing - else trace ("KeyD: " ++ show evalK) $ - trace ("InD: " ++ prettyDemand dInM) $ - trace ("OutD: " ++ prettyDemand @(Maybe Int) (E dOut)) $ - trace ("isT: " ++ (show . isThunk $ lookup inM evalK)) $ - Just evalK - where isBaseCase (j, k) = j - 1 < 0 || k - weights !! j < 0 +{-# LANGUAGE TemplateHaskell, BangPatterns, DerivingStrategies #-} + +{- | This module showcases another type of specification different from those in + "Test.StrictCheck.Examples.Lists". Here, we demonstrate that StrictCheck is + able to distinguish value-lazy maps from value-strict maps. + + In this module, we first develop the solution of the Knapsack dynamic + programming problem by taking the fixpoint of a step function of the solution + table. We represent the solution table with a map, and write a specification + that is critical for the termination of this solution. +-} +module Test.StrictCheck.Examples.Map where + +import Prelude hiding (lookup) +import Debug.Trace + +import qualified GHC.Generics as GHC +import Generics.SOP (Generic, HasDatatypeInfo, NS(..), hd, tl) + +import Test.StrictCheck +import Test.StrictCheck.TH + +import Data.Maybe +import Data.Function + +import Test.QuickCheck + +-- | We roll our own map type to avoid dealing with abstract types. +data Map k v = Bin (Map k v) k v (Map k v) -- ^ A node that contains a key value pair + | Empty -- ^ An empty node + deriving stock (GHC.Generic, Show, Eq, Ord) + deriving anyclass (Generic, HasDatatypeInfo, Consume, Shaped) + +-- | A specialized map useful for knapsack. The pair of ints represent the two +-- parameters to each knapsack sub-problem solved along the way. These two +-- parameters determine the subsequence of items each sub-problem is concerned +-- with, and the weight limit. +type KMap = Map (Int, Int) Int + +$(derivePatternSynonyms ''Map) + +-- | This replaces the thunk in a map partial value with the `r` parameter. This +-- is very similar to the `cap` function in the lists example. +replaceThunk :: (Shaped k, Shaped v) => Map k v -> Map k v -> Map k v +replaceThunk r m | isThunk m = r +replaceThunk _ Empty = Empty +replaceThunk r (Bin ml k v mr) = Bin (replaceThunk r ml) k v (replaceThunk r mr) + +-- | A helper for building a map from a list of values. +fromList :: [((Int, Int), Int)] -> KMap +fromList = foldr (\(k, v) acc -> insert k v acc) Empty + +-- | A simplified insert that ignores rebalancing since rebalancing is not +-- important for the spec we will write. +insert :: (Ord k) => k -> v -> Map k v -> Map k v +insert key value Empty = Bin Empty key value Empty +insert key value (Bin ml k v mr) | key < k = Bin (insert key value ml) k v mr + | key > k = Bin ml k v (insert key value mr) + | otherwise = Bin ml key value mr + +-- | The lookup function specialized for knapsack. +lookup :: KMap -> (Int, Int) -> Maybe Int +lookup Empty _ = Nothing +lookup (Bin ml k' v mr) k | k == k' = Just v + | k < k' = lookup ml k + | otherwise = lookup mr k + +-- | This function extracts all of the keys of a map. +keys :: Map k v -> [k] +keys Empty = [] +keys (Bin ml k _ mr) = keys ml ++ [k] ++ keys mr + +-- | A lookup function that returns the default value `0` for keys that are not +-- in the map. This saves us from doing repeated pattern matching when querying +-- the solution table. +(!) :: KMap -> (Int, Int) -> Int +(!) m k = case lookup m k of + Nothing -> 0 + Just v -> v + +-- | Weight parameters to the knapsack problem. +weights :: [Int] +weights = [10, 20, 30] + +-- | Value parameters to the knapsack problem, note that this must be the same +-- length as `weights`. +values :: [Int] +values = [60, 100, 120] + +-- | The weight limit of the knapsack problem. +limit :: Int +limit = 50 + +-- | One step of the knapsack computation. This is a direct translation from the +-- recurrence relation of the knapsack problem. +solutionStep :: Map (Int, Int) Int -> Map (Int, Int) Int +solutionStep soln = + fromList [((j, k), knapsack j k) | j <- [0 .. length weights-1], k <- [0 .. limit]] + where + knapsack j k = if j - 1 < 0 || k - weights !! j < 0 + then if j >= 0 && weights !! j <= k then values !! j else 0 + else max (soln ! (j-1, k)) + (soln ! (j-1, k - weights !! j) + values !! j) + +-- | The fixpoint of the recurrence relation, which is also the solution for the +-- knapsack problem. +solution :: Map (Int, Int) Int +solution = fix solutionStep + +-- | A pattern synonym for extracting demands of each component from the demand +-- of a pair. +pattern Pair' :: Demand a -> Demand b -> Demand (a, b) +pattern Pair' x y = Wrap (Eval (GS (Z (x :* y :* Nil)))) + +-- | This function computes the nth pre-fixpoint of the knapsack solution, and +-- looks up the value at the specified cell from the pre-fixpoint. +iterSolution :: (Int, Int) -> Int -> Map (Int, Int) Int -> Maybe Int +iterSolution k n soln = lookup m k + where m | n <= 0 = soln + | otherwise = (iterate solutionStep soln) !! n + +-- | This is the same as `iterSolution`, but uses a newtype wrapper for the +-- index into the map since we want to write a customized `Arbitrary` instance +-- for `Key`. +iterSolutionWithKey :: Key -> Int -> Map (Int, Int) Int -> Maybe Int +iterSolutionWithKey (Key k) = iterSolution k + +-- | The newtype wrapper of index into the knapsack solution table. +newtype Key = Key { getKey :: (Int, Int) } + deriving stock (GHC.Generic, Show, Eq, Ord) + deriving anyclass (Generic, HasDatatypeInfo, Consume, Shaped) + +-- | The customized generator for `Key` that only generates valid keys given the +-- problem parameters. +instance Arbitrary Key where + -- Just to make sure keys are within the parameters of the problem + arbitrary = fmap Key $ + (,) <$> elements [0 .. length weights - 1] <*> elements [0 .. limit] + +-- | The customized generator for solution tables that only generates valid +-- pre-fixpoints. +instance Arbitrary KMap where + -- I need to generate only valid pre-fixpoints, which is either + -- Empty (iterated 0 times), or iterate once on Empty, or twice, and + -- so on + arbitrary = do + NonNegative n <- arbitrary + return $ (iterate solutionStep Empty) !! n + +-- | A dummy produce instance for the solution table. +instance Produce KMap where + -- I don't need lazy functions on KMaps. Since the spec only checks + -- whether a particular entry in the KMap is evaluated or not. + produce = arbitrary + +-- | A dummy produce instance for the index into the solution table. +instance Produce Key where + -- I don't need lazy functions on keys either. + produce = arbitrary + +-- | This IO action ties the spec together with everything built so far, and +-- runs the StrictCheck randomized testing framework. +runMapTest :: IO () +runMapTest = strictCheckWithResults + stdArgs{maxSize=100, maxSuccess=1000} + shrinkViaArbitrary + genViaProduce + strictnessViaSized + iterSolution_spec + iterSolutionWithKey >>= print + +-- | This is the specification that establishes a property important for the +-- termination of `solution`: given any pre-fixpoint of `pre-solution`, forcing +-- the value at pre-solution[i][j] should not induce a demand at the (i, j) cell +-- of the input that steps to pre-solution, since otherwise this would be an +-- infinite loop in the fixpoint. +-- The value-lazy `Map` defined in this module satisfies this property. However, +-- if we make this `Map` value-strict using BangPatterns, StrictCheck will +-- report a failure when `runMapTest` is executed. +iterSolution_spec :: Evaluation '[Key, Int, KMap] (Maybe Int) -> Maybe (Int, Int) +iterSolution_spec (Evaluation args demands dOut) = + let I (Key evalK) = hd args + I nIter = hd (tl args) + dInM = hd (tl (tl demands)) + inM = replaceThunk Empty (fromDemand @KMap dInM) + evalV = lookup inM evalK + in if (inM == Empty) || + isBaseCase evalK || + nIter <= 0 || + isThunk evalV || + isNothing evalV + then Nothing + else trace ("KeyD: " ++ show evalK) $ + trace ("InD: " ++ prettyDemand dInM) $ + trace ("OutD: " ++ prettyDemand @(Maybe Int) (E dOut)) $ + trace ("isT: " ++ (show . isThunk $ lookup inM evalK)) $ + Just evalK + where isBaseCase (j, k) = j - 1 < 0 || k - weights !! j < 0 diff --git a/src/Test/StrictCheck/Internal/Inputs.hs b/src/Test/StrictCheck/Internal/Inputs.hs --- a/src/Test/StrictCheck/Internal/Inputs.hs +++ b/src/Test/StrictCheck/Internal/Inputs.hs @@ -1,58 +1,58 @@ -{-| __Internal module__: This module does not make any stability guarantees, and - may not adhere to the PVP. - - This module implements the rose-tree data structure used by StrictCheck to - monomorphize inputs to functions. We decouple the consumption of input from - the production of output by converting any input to an @Input@: a lazily - constructed rose tree with nodes each containing a @(Gen a -> Gen a)@ which - captures a random perturbation associated with the shape of the value - consumed. The tree-shape of an @Input@ matches that of the entire consumed - value, and evaluating any subpart of it forces the evaluation of the - corresponding part of the original value. --} -module Test.StrictCheck.Internal.Inputs - ( Variant(..) - , Input(..) - , Inputs(..) - , draw - , destruct - ) where - -import Test.QuickCheck (Gen) - - --------------------------------------------------- --- The core user-facing types: Input and Inputs -- --------------------------------------------------- - --- | A variant which can be applied to any generator--kept in a newtype to get --- around lack of impredicativity. -newtype Variant - = Variant { vary :: forall a. Gen a -> Gen a } - -instance Semigroup Variant where - v <> w = Variant (vary v . vary w) - -instance Monoid Variant where - mappend = (<>) - mempty = Variant id - --- | A tree representing all possible destruction sequences for a value --- Unfolding the contained lists forces a particular random control path --- for destructing the datatype. -data Input - = Input Variant [Input] -- ^ Not exposed in safe API - --- | A list of inputs given to a function, in abstract form. This lazy structure --- is evaluated piecewise during the course of producing a function, thus --- triggering the partial evaluation of the original input to the function. -newtype Inputs - = Inputs [Input] -- ^ Not exposed in safe API - --- | Extract the list of @Input@s from an @Inputs@ -destruct :: Inputs -> [Input] -destruct (Inputs is) = is - --- | Extract the entropy and subfield-@Input@s from a given @Input@ -draw :: Input -> (Variant, [Input]) -draw (Input v is) = (v, is) +{-| __Internal module__: This module does not make any stability guarantees, and + may not adhere to the PVP. + + This module implements the rose-tree data structure used by StrictCheck to + monomorphize inputs to functions. We decouple the consumption of input from + the production of output by converting any input to an @Input@: a lazily + constructed rose tree with nodes each containing a @(Gen a -> Gen a)@ which + captures a random perturbation associated with the shape of the value + consumed. The tree-shape of an @Input@ matches that of the entire consumed + value, and evaluating any subpart of it forces the evaluation of the + corresponding part of the original value. +-} +module Test.StrictCheck.Internal.Inputs + ( Variant(..) + , Input(..) + , Inputs(..) + , draw + , destruct + ) where + +import Test.QuickCheck (Gen) + + +-------------------------------------------------- +-- The core user-facing types: Input and Inputs -- +-------------------------------------------------- + +-- | A variant which can be applied to any generator--kept in a newtype to get +-- around lack of impredicativity. +newtype Variant + = Variant { vary :: forall a. Gen a -> Gen a } + +instance Semigroup Variant where + v <> w = Variant (vary v . vary w) + +instance Monoid Variant where + mappend = (<>) + mempty = Variant id + +-- | A tree representing all possible destruction sequences for a value +-- Unfolding the contained lists forces a particular random control path +-- for destructing the datatype. +data Input + = Input Variant [Input] -- ^ Not exposed in safe API + +-- | A list of inputs given to a function, in abstract form. This lazy structure +-- is evaluated piecewise during the course of producing a function, thus +-- triggering the partial evaluation of the original input to the function. +newtype Inputs + = Inputs [Input] -- ^ Not exposed in safe API + +-- | Extract the list of @Input@s from an @Inputs@ +destruct :: Inputs -> [Input] +destruct (Inputs is) = is + +-- | Extract the entropy and subfield-@Input@s from a given @Input@ +draw :: Input -> (Variant, [Input]) +draw (Input v is) = (v, is) diff --git a/src/Test/StrictCheck/Internal/Omega.hs b/src/Test/StrictCheck/Internal/Omega.hs --- a/src/Test/StrictCheck/Internal/Omega.hs +++ b/src/Test/StrictCheck/Internal/Omega.hs @@ -1,35 +1,35 @@ -{-| __Internal module__: This module does not make any stability guarantees, and - may not adhere to the PVP. - - This module defines the 'Omega' type, which has only one inhabitant: the - infinite chain of successors. Any function which consumes an @Omega@ is - functionally equivalent to any other; likewise for those which produce an - @Omega@. However, they may have radically differing strictness behaviors. It - is for this reason that we have use for this type in the course of random - example generation. --} -module Test.StrictCheck.Internal.Omega - ( Omega(..) - , forceOmega - ) where - -import Test.StrictCheck.Produce -import Test.StrictCheck.Shaped - -import qualified GHC.Generics as GHC -import Generics.SOP - --- | The type with one inhabitant: the infinite chain of successors -data Omega = Succ Omega - deriving (GHC.Generic, Generic, HasDatatypeInfo, Shaped) - -instance Produce Omega where - produce = Succ <$> recur - --- | Evaluate @n@ constructors of a given @Omega@ value, returning unit -forceOmega :: Int -> Omega -> () -forceOmega n o - | n <= 0 - = () - | Succ o' <- o - = forceOmega (n - 1) o' +{-| __Internal module__: This module does not make any stability guarantees, and + may not adhere to the PVP. + + This module defines the 'Omega' type, which has only one inhabitant: the + infinite chain of successors. Any function which consumes an @Omega@ is + functionally equivalent to any other; likewise for those which produce an + @Omega@. However, they may have radically differing strictness behaviors. It + is for this reason that we have use for this type in the course of random + example generation. +-} +module Test.StrictCheck.Internal.Omega + ( Omega(..) + , forceOmega + ) where + +import Test.StrictCheck.Produce +import Test.StrictCheck.Shaped + +import qualified GHC.Generics as GHC +import Generics.SOP + +-- | The type with one inhabitant: the infinite chain of successors +data Omega = Succ Omega + deriving (GHC.Generic, Generic, HasDatatypeInfo, Shaped) + +instance Produce Omega where + produce = Succ <$> recur + +-- | Evaluate @n@ constructors of a given @Omega@ value, returning unit +forceOmega :: Int -> Omega -> () +forceOmega n o + | n <= 0 + = () + | Succ o' <- o + = forceOmega (n - 1) o' diff --git a/src/Test/StrictCheck/Internal/Shrink.hs b/src/Test/StrictCheck/Internal/Shrink.hs --- a/src/Test/StrictCheck/Internal/Shrink.hs +++ b/src/Test/StrictCheck/Internal/Shrink.hs @@ -1,98 +1,98 @@ -{-| __Internal module__: This module does not make any stability guarantees, and - may not adhere to the PVP. - - This module defines several utilities useful for shrinking demands and - evaluations. - - Of these, only 'axialShrinks' and 'fairInterleave' are used by StrictCheck; - nevertheless, we expose the 'DZipper' type and its associated functions in - this internal module just in case. --} -module Test.StrictCheck.Internal.Shrink - ( Shrink(..) - , axialShrinks - , fairInterleave - -- * CPS-based zippers through heterogeneous products - , DZipper(..) - , next - , positions - , dzipper - , dzip - ) where - -import Generics.SOP -import Data.Functor.Product - --- Fair n-ary axial shrinking (a.k.a. *fair* generalization of shrink on tuples) - --- | Newtype allowing us to construct 'NP' n-ary products of shrinkers -newtype Shrink a - = Shrink (a -> [a]) - --- | A @DZipper@ is a suspended traversal through a non-empty 'NP' n-ary product --- --- The position of the traversal within that product is existentially --- quantified. -data DZipper f whole where - DZipper :: (NP f (c : rs) -> NP f whole) - -> f c - -> NP f rs - -> DZipper f whole - --- | Step one to the right in a @DZipper@, returning @Nothing@ if this is not --- possible -next :: DZipper f whole -> Maybe (DZipper f whole) -next (DZipper _ _ Nil) = Nothing -next (DZipper ls c (r :* rs')) = - Just $ DZipper (ls . (c :*)) r rs' - --- | Given an n-ary product of @xs@, get a list of @DZipper@s, each focused in --- sequence on the values of the input product --- --- This is similar to the @duplicate@ operation on comonads. -positions :: NP f xs -> [DZipper f xs] -positions (dzipper -> mstart) = - maybe [] go mstart - where - go start = start : maybe [] go (next start) - --- | Convert an n-ary product into a @DZipper@, returning @Nothing@ if the --- input product is empty -dzipper :: NP f xs -> Maybe (DZipper f xs) -dzipper Nil = Nothing -dzipper (c :* rs) = Just $ DZipper id c rs - --- | Collapse a @DZipper@ back into the n-ary product it represents -dzip :: DZipper f xs -> NP f xs -dzip (DZipper ls c rs) = ls (c :* rs) - --- | Given a list of shrinkers and a list of values-to-be-shrunk, generate --- a list of shrunken lists-of-values, each inner list being one potential --- "axis" for shrinking --- --- That is, the first element of the result is all the ways the original --- product could be shrunken by /only/ shrinking its first component, etc. -axialShrinks :: SListI xs => NP Shrink xs -> NP I xs -> [[NP I xs]] -axialShrinks shrinks xs = - fmap (hliftA (\(Pair _ v) -> v) . dzip) - . centerIter <$> positions withShrinks - where - iter (Pair (Shrink s) (I v)) = - Pair (Shrink s) . I <$> (s v) - - centerIter (DZipper ls c rs) = - map (\c' -> DZipper ls c' rs) (iter c) - - withShrinks = - hliftA2 Pair shrinks xs - --- | Fairly interleave a list of lists in a round-robin fashion -fairInterleave :: [[a]] -> [a] -fairInterleave = roundRobin id - where - roundRobin k ((x : xs) : xss) = x : roundRobin (k . (xs :)) xss - roundRobin k ([ ] : xss) = roundRobin k xss - roundRobin k [ ] = - case k [] of - [ ] -> [] - xss -> roundRobin id xss +{-| __Internal module__: This module does not make any stability guarantees, and + may not adhere to the PVP. + + This module defines several utilities useful for shrinking demands and + evaluations. + + Of these, only 'axialShrinks' and 'fairInterleave' are used by StrictCheck; + nevertheless, we expose the 'DZipper' type and its associated functions in + this internal module just in case. +-} +module Test.StrictCheck.Internal.Shrink + ( Shrink(..) + , axialShrinks + , fairInterleave + -- * CPS-based zippers through heterogeneous products + , DZipper(..) + , next + , positions + , dzipper + , dzip + ) where + +import Generics.SOP +import Data.Functor.Product + +-- Fair n-ary axial shrinking (a.k.a. *fair* generalization of shrink on tuples) + +-- | Newtype allowing us to construct 'NP' n-ary products of shrinkers +newtype Shrink a + = Shrink (a -> [a]) + +-- | A @DZipper@ is a suspended traversal through a non-empty 'NP' n-ary product +-- +-- The position of the traversal within that product is existentially +-- quantified. +data DZipper f whole where + DZipper :: (NP f (c : rs) -> NP f whole) + -> f c + -> NP f rs + -> DZipper f whole + +-- | Step one to the right in a @DZipper@, returning @Nothing@ if this is not +-- possible +next :: DZipper f whole -> Maybe (DZipper f whole) +next (DZipper _ _ Nil) = Nothing +next (DZipper ls c (r :* rs')) = + Just $ DZipper (ls . (c :*)) r rs' + +-- | Given an n-ary product of @xs@, get a list of @DZipper@s, each focused in +-- sequence on the values of the input product +-- +-- This is similar to the @duplicate@ operation on comonads. +positions :: NP f xs -> [DZipper f xs] +positions (dzipper -> mstart) = + maybe [] go mstart + where + go start = start : maybe [] go (next start) + +-- | Convert an n-ary product into a @DZipper@, returning @Nothing@ if the +-- input product is empty +dzipper :: NP f xs -> Maybe (DZipper f xs) +dzipper Nil = Nothing +dzipper (c :* rs) = Just $ DZipper id c rs + +-- | Collapse a @DZipper@ back into the n-ary product it represents +dzip :: DZipper f xs -> NP f xs +dzip (DZipper ls c rs) = ls (c :* rs) + +-- | Given a list of shrinkers and a list of values-to-be-shrunk, generate +-- a list of shrunken lists-of-values, each inner list being one potential +-- "axis" for shrinking +-- +-- That is, the first element of the result is all the ways the original +-- product could be shrunken by /only/ shrinking its first component, etc. +axialShrinks :: SListI xs => NP Shrink xs -> NP I xs -> [[NP I xs]] +axialShrinks shrinks xs = + fmap (hliftA (\(Pair _ v) -> v) . dzip) + . centerIter <$> positions withShrinks + where + iter (Pair (Shrink s) (I v)) = + Pair (Shrink s) . I <$> (s v) + + centerIter (DZipper ls c rs) = + map (\c' -> DZipper ls c' rs) (iter c) + + withShrinks = + hliftA2 Pair shrinks xs + +-- | Fairly interleave a list of lists in a round-robin fashion +fairInterleave :: [[a]] -> [a] +fairInterleave = roundRobin id + where + roundRobin k ((x : xs) : xss) = x : roundRobin (k . (xs :)) xss + roundRobin k ([ ] : xss) = roundRobin k xss + roundRobin k [ ] = + case k [] of + [ ] -> [] + xss -> roundRobin id xss diff --git a/src/Test/StrictCheck/Internal/Unevaluated.hs b/src/Test/StrictCheck/Internal/Unevaluated.hs --- a/src/Test/StrictCheck/Internal/Unevaluated.hs +++ b/src/Test/StrictCheck/Internal/Unevaluated.hs @@ -1,23 +1,23 @@ -{-| __Internal module__: This module does not make any stability guarantees, and - may not adhere to the PVP. - - This module defines the internal exception type used to implement the - to/from-Demand methods in "Test.StrictCheck.Demand". We don't export this - type from the library to discourage users from interacting with this - mechanism. --} - -module Test.StrictCheck.Internal.Unevaluated - ( Unevaluated(..) - ) where - -import Control.Exception - --- | In @fromDemand@, this exception is (purely, lazily) thrown whenever a --- @Thunk@ is encountered. In @toDemand@, it is caught and converted back to a --- @Thunk@. -data Unevaluated - = Unevaluated - deriving Show - -instance Exception Unevaluated +{-| __Internal module__: This module does not make any stability guarantees, and + may not adhere to the PVP. + + This module defines the internal exception type used to implement the + to/from-Demand methods in "Test.StrictCheck.Demand". We don't export this + type from the library to discourage users from interacting with this + mechanism. +-} + +module Test.StrictCheck.Internal.Unevaluated + ( Unevaluated(..) + ) where + +import Control.Exception + +-- | In @fromDemand@, this exception is (purely, lazily) thrown whenever a +-- @Thunk@ is encountered. In @toDemand@, it is caught and converted back to a +-- @Thunk@. +data Unevaluated + = Unevaluated + deriving Show + +instance Exception Unevaluated diff --git a/src/Test/StrictCheck/Observe.hs b/src/Test/StrictCheck/Observe.hs --- a/src/Test/StrictCheck/Observe.hs +++ b/src/Test/StrictCheck/Observe.hs @@ -1,148 +1,148 @@ -{-| This module implements the core "trick" of StrictCheck: observing the - demand behavior of a function in a purely functional way. - - All the functions in this module are safe and referentially transparent. - - Observing the evaluation of a function using these functions incurs at most - a small constant multiple of overhead compared to just executing the function - with no observation. --} -module Test.StrictCheck.Observe - ( observe1 - , observe - , observeNP - ) where - -import Data.Bifunctor -import Data.Functor.Product - -import Generics.SOP hiding (Shape) - -import Test.StrictCheck.Curry hiding (curry, uncurry) -import Test.StrictCheck.Shaped -import Test.StrictCheck.Observe.Unsafe -import Test.StrictCheck.Demand - ------------------------------------------------------- --- Observing demand behavior of arbitrary functions -- ------------------------------------------------------- - --- | Observe the demand behavior --- --- * in a given evaluation context, --- * of a given __unary function__, --- * called upon a given input, --- --- returning a pair of --- --- * the demand on its output exerted by the evaluation context, and --- * the demand on its input this induced --- --- Suppose we want to see how strict @reverse@ is when we evaluate its result --- to weak-head normal form: --- --- >>> (b, a) = observe1 (`seq` ()) (reverse @Int) [1, 2, 3] --- >>> printDemand b -- output demand --- _ : _ --- >>> printDemand a -- input demand --- _ : _ : _ : _ : [] --- --- This tells us that our context did indeed evaluate the result of @reverse@ --- to force only its first constructor, and that doing so required the entire --- spine of the list to be evaluated, but did not evaluate any of its elements. -{-# NOINLINE observe1 #-} -observe1 - :: (Shaped a, Shaped b) - => (b -> ()) -> (a -> b) -> a -> (Demand b, Demand a) -observe1 context function input = - let (input', inputD) = - instrument input -- (1) - (result', resultD) = - instrument (function input') -- (2) - in let !_ = context result' -- (3) - in (resultD, inputD) -- (4) - - -- NOTE: The observation function: - -- (1) instruments the input - -- (2) instruments the result of the function applied to the input - -- (3) evaluates the instrumented result of the function in the context, and - -- (4) returns the observed demands on the result and the input. - --- | Observe the demand behavior --- --- * in a given evaluation context --- * of a given __uncurried n-ary function__ (taking as input an n-ary --- product of inputs represented as an 'NP' 'I' from "Generics.SOP") --- * called upon all of its inputs (provided as curried ordinary inputs), --- --- returning a pair of --- --- * the demand on its output exerted by the evaluation context, and --- * the demands on its inputs this induced, represented as an 'NP' 'Demand' --- from "Generics.SOP" --- --- This is mostly useful for implementing the internals of StrictCheck; --- 'observe' is more ergonomic for exploration by end-users. -{-# NOINLINE observeNP #-} -observeNP - :: (All Shaped inputs, Shaped result) - => (result -> ()) - -> (NP I inputs -> result) - -> NP I inputs - -> ( Demand result - , NP Demand inputs ) -observeNP context function inputs = - let entangled = - hcliftA - (Proxy @Shaped) - (uncurry Pair . first I . instrument . unI) - inputs - (inputs', inputsD) = - (hliftA (\(Pair r _) -> r) entangled, - hliftA (\(Pair _ l) -> l) entangled) - (result', resultD) = instrument (function inputs') - in let !_ = context result' - in (resultD, inputsD) - --- | Observe the demand behavior --- --- * in a given evaluation context --- * of a given __curried n-ary function__ --- * called upon all of its inputs (provided as curried ordinary inputs), --- --- returning a pair of --- --- * the demand on its output exerted by the evaluation context, and --- * the demands on its inputs this induced, represented as an 'NP' 'Demand' --- from "Generics.SOP" --- --- This function is variadic and curried: it takes @n + 2@ arguments, where --- @n@ is the total number of arguments taken by the observed function. --- --- Suppose we want to see how strict @zipWith (*)@ is when we evaluate its --- result completely (to normal form): --- --- >>> productZip = zipWith ((*) @Int) --- >>> (zs, (xs :* ys :* Nil)) = observe normalize productZip [10, 20] [30, 40] --- >>> printDemand zs -- output demand --- 300 : 800 : [] --- >>> printDemand xs -- input demand #1 --- 10 : 20 : [] --- >>> printDemand ys -- input demand #2 --- 30 : 40 : _ --- --- If you haven't thought very carefully about the strictness behavior of @zip@, --- this may be a surprising result; this is part of the fun! -observe - :: ( All Shaped (Args function) - , Shaped (Result function) - , Curry (Args function) ) - => (Result function -> ()) - -> function - -> Args function - ⋯-> ( Demand (Result function) - , NP Demand (Args function) ) -observe context function = - curryAll (observeNP context (uncurryAll function)) - --- NOTE: We don't need a NOINLINE annotation here because this wraps observeNP. +{-| This module implements the core "trick" of StrictCheck: observing the + demand behavior of a function in a purely functional way. + + All the functions in this module are safe and referentially transparent. + + Observing the evaluation of a function using these functions incurs at most + a small constant multiple of overhead compared to just executing the function + with no observation. +-} +module Test.StrictCheck.Observe + ( observe1 + , observe + , observeNP + ) where + +import Data.Bifunctor +import Data.Functor.Product + +import Generics.SOP hiding (Shape) + +import Test.StrictCheck.Curry hiding (curry, uncurry) +import Test.StrictCheck.Shaped +import Test.StrictCheck.Observe.Unsafe +import Test.StrictCheck.Demand + +------------------------------------------------------ +-- Observing demand behavior of arbitrary functions -- +------------------------------------------------------ + +-- | Observe the demand behavior +-- +-- * in a given evaluation context, +-- * of a given __unary function__, +-- * called upon a given input, +-- +-- returning a pair of +-- +-- * the demand on its output exerted by the evaluation context, and +-- * the demand on its input this induced +-- +-- Suppose we want to see how strict @reverse@ is when we evaluate its result +-- to weak-head normal form: +-- +-- >>> (b, a) = observe1 (`seq` ()) (reverse @Int) [1, 2, 3] +-- >>> printDemand b -- output demand +-- _ : _ +-- >>> printDemand a -- input demand +-- _ : _ : _ : _ : [] +-- +-- This tells us that our context did indeed evaluate the result of @reverse@ +-- to force only its first constructor, and that doing so required the entire +-- spine of the list to be evaluated, but did not evaluate any of its elements. +{-# NOINLINE observe1 #-} +observe1 + :: (Shaped a, Shaped b) + => (b -> ()) -> (a -> b) -> a -> (Demand b, Demand a) +observe1 context function input = + let (input', inputD) = + instrument input -- (1) + (result', resultD) = + instrument (function input') -- (2) + in let !_ = context result' -- (3) + in (resultD, inputD) -- (4) + + -- NOTE: The observation function: + -- (1) instruments the input + -- (2) instruments the result of the function applied to the input + -- (3) evaluates the instrumented result of the function in the context, and + -- (4) returns the observed demands on the result and the input. + +-- | Observe the demand behavior +-- +-- * in a given evaluation context +-- * of a given __uncurried n-ary function__ (taking as input an n-ary +-- product of inputs represented as an 'NP' 'I' from "Generics.SOP") +-- * called upon all of its inputs (provided as curried ordinary inputs), +-- +-- returning a pair of +-- +-- * the demand on its output exerted by the evaluation context, and +-- * the demands on its inputs this induced, represented as an 'NP' 'Demand' +-- from "Generics.SOP" +-- +-- This is mostly useful for implementing the internals of StrictCheck; +-- 'observe' is more ergonomic for exploration by end-users. +{-# NOINLINE observeNP #-} +observeNP + :: (All Shaped inputs, Shaped result) + => (result -> ()) + -> (NP I inputs -> result) + -> NP I inputs + -> ( Demand result + , NP Demand inputs ) +observeNP context function inputs = + let entangled = + hcliftA + (Proxy @Shaped) + (uncurry Pair . first I . instrument . unI) + inputs + (inputs', inputsD) = + (hliftA (\(Pair r _) -> r) entangled, + hliftA (\(Pair _ l) -> l) entangled) + (result', resultD) = instrument (function inputs') + in let !_ = context result' + in (resultD, inputsD) + +-- | Observe the demand behavior +-- +-- * in a given evaluation context +-- * of a given __curried n-ary function__ +-- * called upon all of its inputs (provided as curried ordinary inputs), +-- +-- returning a pair of +-- +-- * the demand on its output exerted by the evaluation context, and +-- * the demands on its inputs this induced, represented as an 'NP' 'Demand' +-- from "Generics.SOP" +-- +-- This function is variadic and curried: it takes @n + 2@ arguments, where +-- @n@ is the total number of arguments taken by the observed function. +-- +-- Suppose we want to see how strict @zipWith (*)@ is when we evaluate its +-- result completely (to normal form): +-- +-- >>> productZip = zipWith ((*) @Int) +-- >>> (zs, (xs :* ys :* Nil)) = observe normalize productZip [10, 20] [30, 40] +-- >>> printDemand zs -- output demand +-- 300 : 800 : [] +-- >>> printDemand xs -- input demand #1 +-- 10 : 20 : [] +-- >>> printDemand ys -- input demand #2 +-- 30 : 40 : _ +-- +-- If you haven't thought very carefully about the strictness behavior of @zip@, +-- this may be a surprising result; this is part of the fun! +observe + :: ( All Shaped (Args function) + , Shaped (Result function) + , Curry (Args function) ) + => (Result function -> ()) + -> function + -> Args function + ⋯-> ( Demand (Result function) + , NP Demand (Args function) ) +observe context function = + curryAll (observeNP context (uncurryAll function)) + +-- NOTE: We don't need a NOINLINE annotation here because this wraps observeNP. diff --git a/src/Test/StrictCheck/Observe/Unsafe.hs b/src/Test/StrictCheck/Observe/Unsafe.hs --- a/src/Test/StrictCheck/Observe/Unsafe.hs +++ b/src/Test/StrictCheck/Observe/Unsafe.hs @@ -1,76 +1,76 @@ -{-| This module defines the underlying __unsafe__ primitives StrictCheck uses - to implement purely functional observation of evaluation. - - The "functions" in this module are __not referentially transparent__! --} -module Test.StrictCheck.Observe.Unsafe where - -import System.IO.Unsafe -import Data.IORef - -import Data.Bifunctor -import Generics.SOP (I(..), unI) - -import Test.StrictCheck.Shaped -import Test.StrictCheck.Demand - --- | From some value of any type, produce a pair: a copy of the original value, --- and a 'Thunk' of that same type, with their values determined by the --- /order/ in which their values themselves are evaluated --- --- If the copy of the value is evaluated to weak-head normal form before the --- returned @Thunk@, then any future inspection of the @Thunk@ will show that it --- is equal to the original value wrapped in an @Eval@. However, if the copy of --- the value is /not/ evaluated by the time the @Thunk@ is evaluated, any future --- inspection of the @Thunk@ will show that it is equal to @Thunk@. --- --- A picture may be worth 1000 words: --- --- >>> x = "hello," ++ " world" --- >>> (x', t) = entangle x --- >>> x' --- "hello, world" --- >>> t --- Eval "hello, world" --- --- >>> x = "hello," ++ " world" --- >>> (x', t) = entangle x --- >>> t --- Thunk --- >>> x' --- "hello, world" --- >>> t --- Thunk -{-# NOINLINE entangle #-} -entangle :: forall a. a -> (a, Thunk a) -entangle a = - unsafePerformIO $ do - ref <- newIORef Thunk - return ( unsafePerformIO $ do - writeIORef ref (Eval a) - return a - , unsafePerformIO $ readIORef ref ) - --- | Recursively 'entangle' an @a@, producing not merely a @Thunk@, but an --- entire @Demand@ which is piecewise entangled with that value. Whatever --- portion of the entangled value is evaluated before the corresponding portion --- of the returned @Demand@ will be represented in the shape of that @Demand@. --- However, any part of the returned @Demand@ which is evaluated before the --- corresponding portion of the entangled value will be forever equal to --- @Thunk@. --- --- The behavior of this function is even more tricky to predict than that of --- 'entangle', especially when evaluation of the entangled value and the --- corresponding @Demand@ happen at the same time. In StrictCheck, all --- evaluation of the entangled value occurs before any evaluation of the --- @Demand@; we never interleave their evaluation. -{-# NOINLINE instrument #-} -instrument :: Shaped a => a -> (a, Demand a) -instrument = - first (fuse unI) - . unzipWith entangle' - . interleave I - where - entangle' :: I x -> (I x, Thunk x) - entangle' = - first I . entangle . unI +{-| This module defines the underlying __unsafe__ primitives StrictCheck uses + to implement purely functional observation of evaluation. + + The "functions" in this module are __not referentially transparent__! +-} +module Test.StrictCheck.Observe.Unsafe where + +import System.IO.Unsafe +import Data.IORef + +import Data.Bifunctor +import Generics.SOP (I(..), unI) + +import Test.StrictCheck.Shaped +import Test.StrictCheck.Demand + +-- | From some value of any type, produce a pair: a copy of the original value, +-- and a 'Thunk' of that same type, with their values determined by the +-- /order/ in which their values themselves are evaluated +-- +-- If the copy of the value is evaluated to weak-head normal form before the +-- returned @Thunk@, then any future inspection of the @Thunk@ will show that it +-- is equal to the original value wrapped in an @Eval@. However, if the copy of +-- the value is /not/ evaluated by the time the @Thunk@ is evaluated, any future +-- inspection of the @Thunk@ will show that it is equal to @Thunk@. +-- +-- A picture may be worth 1000 words: +-- +-- >>> x = "hello," ++ " world" +-- >>> (x', t) = entangle x +-- >>> x' +-- "hello, world" +-- >>> t +-- Eval "hello, world" +-- +-- >>> x = "hello," ++ " world" +-- >>> (x', t) = entangle x +-- >>> t +-- Thunk +-- >>> x' +-- "hello, world" +-- >>> t +-- Thunk +{-# NOINLINE entangle #-} +entangle :: forall a. a -> (a, Thunk a) +entangle a = + unsafePerformIO $ do + ref <- newIORef Thunk + return ( unsafePerformIO $ do + writeIORef ref (Eval a) + return a + , unsafePerformIO $ readIORef ref ) + +-- | Recursively 'entangle' an @a@, producing not merely a @Thunk@, but an +-- entire @Demand@ which is piecewise entangled with that value. Whatever +-- portion of the entangled value is evaluated before the corresponding portion +-- of the returned @Demand@ will be represented in the shape of that @Demand@. +-- However, any part of the returned @Demand@ which is evaluated before the +-- corresponding portion of the entangled value will be forever equal to +-- @Thunk@. +-- +-- The behavior of this function is even more tricky to predict than that of +-- 'entangle', especially when evaluation of the entangled value and the +-- corresponding @Demand@ happen at the same time. In StrictCheck, all +-- evaluation of the entangled value occurs before any evaluation of the +-- @Demand@; we never interleave their evaluation. +{-# NOINLINE instrument #-} +instrument :: Shaped a => a -> (a, Demand a) +instrument = + first (fuse unI) + . unzipWith entangle' + . interleave I + where + entangle' :: I x -> (I x, Thunk x) + entangle' = + first I . entangle . unI diff --git a/src/Test/StrictCheck/Produce.hs b/src/Test/StrictCheck/Produce.hs --- a/src/Test/StrictCheck/Produce.hs +++ b/src/Test/StrictCheck/Produce.hs @@ -1,229 +1,231 @@ -{-| This module defines the 'Produce' typeclass, used for generating random - values for testing in StrictCheck. - - 'Produce' is a strict generalization of "Test.QuickCheck"'s 'Arbitrary' - typeclass. Paired with 'Consume' (a generalization of 'CoArbitrary') it can - be used to create random non-strict functions, whose strictness behavior is - dependent on the values given to them. --} - -module Test.StrictCheck.Produce - ( Produce(..) - -- * Tools for writing 'Produce' instances - , recur - , build - -- * Producing non-strict functions - , returning - , variadic - -- * Integration with "Test.QuickCheck"'s @Arbitrary@ - , Lazy(..) - , freely - -- * Abstract types representing input to a function - , Input - , Inputs - -- * The traversal distribution for processing @Input@s - , draws - ) where - -import Test.QuickCheck hiding (variant) -import Test.QuickCheck.Gen.Unsafe - -import Test.StrictCheck.Internal.Inputs -import Test.StrictCheck.Consume -import Test.StrictCheck.Curry - -import Generics.SOP -import Data.Complex -import Data.Monoid ((<>)) - - -------------------------------------------------------- --- The user interface for creating Produce instances -- -------------------------------------------------------- - --- TODO: parameterize over destruction pattern? - --- | Produce an arbitrary value of type @b@, such that destructing that value --- incrementally evaluates some input to a function. --- --- Writing instances of @Produce@ is very similar to writing instances of --- QuickCheck's 'Arbitrary'. The distinction: when making a recursive call to --- produce a subfield of a structure, __always__ use 'build' or 'recur', and --- __never__ a direct call to 'produce' itself. This ensures that the input can --- potentially be demanded at any step of evaluation of the produced value. --- --- If, in the course of generating a value of type @b@, you need to generate a --- random value of some other type, which is /not/ going to be a subpart of the --- resultant @b@ (e.g. a length or depth), use a direct call to @arbitrary@ or --- some other generator which does not consume input. --- --- An example instance of @Produce@: --- --- > data D a --- > = X a --- > | Y [Int] --- > --- > instance Produce a => Produce (D a) where --- > produce = --- > oneof [ fmap X recur --- > , fmap Y recur --- > ] -class Produce b where - produce :: (?inputs::Inputs) => Gen b - -theInputs :: (?inputs::Inputs) => [Input] -theInputs = destruct ?inputs - --- | Given an input-consuming producer, wrap it in an outer layer of input --- consumption, so that this consumption can be interleaved when the producer is --- called recursively to generate a subfield of a larger produced datatype. -build :: (?inputs::Inputs) => ((?inputs::Inputs) => Gen a) -> Gen a -build gen = do - (v, is') <- draws theInputs - vary v $ let ?inputs = Inputs is' in gen - --- | Destruct some inputs to generate an output. This function handles the --- interleaving of input destruction with output construction. When producing a --- data type, it should be called to produce each subfield -- *not* produce --- itself. -recur :: (Produce a, ?inputs::Inputs) => Gen a -recur = build produce - - ---------------------------------------- --- How to make random lazy functions -- ---------------------------------------- - --- NOTE: This instance must be defined in this module, as it has to break the --- abstraction of the Inputs type. No other instance needs to break this. --- Incidentally, it also must break Gen's abstraction barrier, because it needs --- to use promote to make a function. - -instance (Consume a, Produce b) => Produce (a -> b) where - produce = returning produce - --- | Create an input-consuming producer of input-consuming functions, given an --- input-consuming producer for results of that function. -returning - :: (Consume a, ?inputs::Inputs) - => ((?inputs::Inputs) => Gen b) - -> Gen (a -> b) -returning out = - promote $ \a -> - let ?inputs = Inputs (consume a : theInputs) - in build out - --- | Create an input-consuming producer of input-consuming functions, of any --- arity. This will usually be used in conjuntion with type application, to --- specify the type(s) of the argument(s) to the function. -variadic :: - forall args result. - (All Consume args, Curry args, ?inputs::Inputs) - => ((?inputs::Inputs) => Gen result) - -> Gen (args ⋯-> result) -variadic out = - fmap (curryAll @args @_ @(NP I)) . promote $ \args -> - let ?inputs = - Inputs . (++ theInputs) $ - hcollapse $ hcliftA (Proxy @Consume) (K . consume . unI) args - in build out - - -------------------------------------------------------------------------- --- Random destruction of the original input, as transformed into Input -- -------------------------------------------------------------------------- - --- | Destruct a random subpart of the given 'Input's, returning the 'Variant' --- corresponding to the combined information harvested during this process, and --- the remaining "leaves" of the inputs yet to be destructed --- --- To maximize the likelihood that different random consumption paths through --- the same value will diverge (desirable when generating functions with --- interesting strictness), @draws@ destructs the forest of @Input@s as a --- depth-first random traversal with a budget sampled from a geometric --- distribution with expectation 1. -draws :: [Input] -> Gen (Variant, [Input]) -draws inputs = go [inputs] - where - -- Mutually recursive: - go, inwardFrom :: [[Input]] -> Gen (Variant, [Input]) - - go levels = - oneof -- 50% choice between: - [ return (mempty, concat levels) -- stop consuming input, or - , inwardFrom levels ] -- keep consuming input - - inwardFrom levels = - case levels of - [ ] -> return mempty -- if no more input: stop - [ ] : outside -> inwardFrom outside -- if nothing here: backtrack - here : outside -> do -- if something here: go deeper - (Input v inside, here') <- pick here - vary v $ do - (entropy, levels') <- go (inside : here' : outside) -- back to 'go' - return (v <> entropy, levels') - - -- Pick a random list element and the remaining list - pick :: [a] -> Gen (a, [a]) - pick as = do - index <- choose (0, length as - 1) - let (before, picked : after) = splitAt index as - return (picked, before ++ after) - - - ---------------------------------------------- --- Integration with QuickCheck's Arbitrary -- ---------------------------------------------- - --- | We hook into QuickCheck's existing Arbitrary infrastructure by using --- a newtype to differentiate our special way of generating things. -newtype Lazy a - = Lazy { runLazy :: a } - -instance Produce a => Arbitrary (Lazy a) where - arbitrary = Lazy <$> freely produce - --- | Actually produce an output, given an input-consuming producer. If a --- function is to be produced, it will be almost-certainly non-strict. -freely :: ((?inputs::Inputs) => Gen a) -> Gen a -freely p = let ?inputs = Inputs [] in p - - ---------------- --- Instances -- ---------------- - -instance Produce () where produce = arbitrary -instance Produce Bool where produce = arbitrary -instance Produce Ordering where produce = arbitrary - -instance Produce Char where produce = arbitrary -instance Produce Word where produce = arbitrary -instance Produce Int where produce = arbitrary -instance Produce Double where produce = arbitrary -instance Produce Float where produce = arbitrary -instance Produce Rational where produce = arbitrary -instance Produce Integer where produce = arbitrary - -instance (Arbitrary a, RealFloat a) => Produce (Complex a) where - produce = arbitrary - -instance Produce a => Produce (Maybe a) where - produce = - oneof [ return Nothing - , Just <$> recur - ] - -instance (Produce a, Produce b) => Produce (Either a b) where - produce = - oneof [ Left <$> recur - , Right <$> recur - ] - -instance (Produce a) => Produce [a] where - produce = - frequency [ (1, return []) - , (1, (:) <$> recur - <*> recur) - ] +{-| This module defines the 'Produce' typeclass, used for generating random + values for testing in StrictCheck. + + 'Produce' is a strict generalization of "Test.QuickCheck"'s 'Arbitrary' + typeclass. Paired with 'Consume' (a generalization of 'CoArbitrary') it can + be used to create random non-strict functions, whose strictness behavior is + dependent on the values given to them. +-} + +module Test.StrictCheck.Produce + ( Produce(..) + -- * Tools for writing 'Produce' instances + , recur + , build + -- * Producing non-strict functions + , returning + , variadic + -- * Integration with "Test.QuickCheck"'s @Arbitrary@ + , Lazy(..) + , freely + -- * Abstract types representing input to a function + , Input + , Inputs + -- * The traversal distribution for processing @Input@s + , draws + ) where + +import Test.QuickCheck hiding (variant) +import Test.QuickCheck.Gen.Unsafe + +import Test.StrictCheck.Internal.Inputs +import Test.StrictCheck.Consume +import Test.StrictCheck.Curry + +import Generics.SOP +import Data.Complex +import Data.List.NonEmpty (NonEmpty(..)) + +------------------------------------------------------- +-- The user interface for creating Produce instances -- +------------------------------------------------------- + +-- TODO: parameterize over destruction pattern? + +-- | Produce an arbitrary value of type @b@, such that destructing that value +-- incrementally evaluates some input to a function. +-- +-- Writing instances of @Produce@ is very similar to writing instances of +-- QuickCheck's 'Arbitrary'. The distinction: when making a recursive call to +-- produce a subfield of a structure, __always__ use 'build' or 'recur', and +-- __never__ a direct call to 'produce' itself. This ensures that the input can +-- potentially be demanded at any step of evaluation of the produced value. +-- +-- If, in the course of generating a value of type @b@, you need to generate a +-- random value of some other type, which is /not/ going to be a subpart of the +-- resultant @b@ (e.g. a length or depth), use a direct call to @arbitrary@ or +-- some other generator which does not consume input. +-- +-- An example instance of @Produce@: +-- +-- > data D a +-- > = X a +-- > | Y [Int] +-- > +-- > instance Produce a => Produce (D a) where +-- > produce = +-- > oneof [ fmap X recur +-- > , fmap Y recur +-- > ] +class Produce b where + produce :: (?inputs::Inputs) => Gen b + +theInputs :: (?inputs::Inputs) => [Input] +theInputs = destruct ?inputs + +-- | Given an input-consuming producer, wrap it in an outer layer of input +-- consumption, so that this consumption can be interleaved when the producer is +-- called recursively to generate a subfield of a larger produced datatype. +build :: (?inputs::Inputs) => ((?inputs::Inputs) => Gen a) -> Gen a +build gen = do + (v, is') <- draws theInputs + vary v $ let ?inputs = Inputs is' in gen + +-- | Destruct some inputs to generate an output. This function handles the +-- interleaving of input destruction with output construction. When producing a +-- data type, it should be called to produce each subfield -- *not* produce +-- itself. +recur :: (Produce a, ?inputs::Inputs) => Gen a +recur = build produce + + +--------------------------------------- +-- How to make random lazy functions -- +--------------------------------------- + +-- NOTE: This instance must be defined in this module, as it has to break the +-- abstraction of the Inputs type. No other instance needs to break this. +-- Incidentally, it also must break Gen's abstraction barrier, because it needs +-- to use promote to make a function. + +instance (Consume a, Produce b) => Produce (a -> b) where + produce = returning produce + +-- | Create an input-consuming producer of input-consuming functions, given an +-- input-consuming producer for results of that function. +returning + :: (Consume a, ?inputs::Inputs) + => ((?inputs::Inputs) => Gen b) + -> Gen (a -> b) +returning out = + promote $ \a -> + let ?inputs = Inputs (consume a : theInputs) + in build out + +-- | Create an input-consuming producer of input-consuming functions, of any +-- arity. This will usually be used in conjuntion with type application, to +-- specify the type(s) of the argument(s) to the function. +variadic :: + forall args result. + (All Consume args, Curry args, ?inputs::Inputs) + => ((?inputs::Inputs) => Gen result) + -> Gen (args ⋯-> result) +variadic out = + fmap (curryAll @args @_ @(NP I)) . promote $ \args -> + let ?inputs = + Inputs . (++ theInputs) $ + hcollapse $ hcliftA (Proxy @Consume) (K . consume . unI) args + in build out + + +------------------------------------------------------------------------- +-- Random destruction of the original input, as transformed into Input -- +------------------------------------------------------------------------- + +-- | Destruct a random subpart of the given 'Input's, returning the 'Variant' +-- corresponding to the combined information harvested during this process, and +-- the remaining "leaves" of the inputs yet to be destructed +-- +-- To maximize the likelihood that different random consumption paths through +-- the same value will diverge (desirable when generating functions with +-- interesting strictness), @draws@ destructs the forest of @Input@s as a +-- depth-first random traversal with a budget sampled from a geometric +-- distribution with expectation 1. +draws :: [Input] -> Gen (Variant, [Input]) +draws inputs = go [inputs] + where + -- Mutually recursive: + go, inwardFrom :: [[Input]] -> Gen (Variant, [Input]) + + go levels = + oneof -- 50% choice between: + [ return (mempty, concat levels) -- stop consuming input, or + , inwardFrom levels ] -- keep consuming input + + inwardFrom levels = + case levels of + [ ] -> return mempty -- if no more input: stop + [ ] : outside -> inwardFrom outside -- if nothing here: backtrack + here : outside -> do -- if something here: go deeper + (Input v inside, here') <- pick here + vary v $ do + (entropy, levels') <- go (inside : here' : outside) -- back to 'go' + return (v <> entropy, levels') + + -- Pick a random list element and the remaining list + pick :: [a] -> Gen (a, [a]) + pick as = do + index <- choose (0, length as - 1) + case splitAt index as of + (before, picked : after) -> return (picked, before ++ after) + _ -> error "pick: empty list" + + +--------------------------------------------- +-- Integration with QuickCheck's Arbitrary -- +--------------------------------------------- + +-- | We hook into QuickCheck's existing Arbitrary infrastructure by using +-- a newtype to differentiate our special way of generating things. +newtype Lazy a + = Lazy { runLazy :: a } + +instance Produce a => Arbitrary (Lazy a) where + arbitrary = Lazy <$> freely produce + +-- | Actually produce an output, given an input-consuming producer. If a +-- function is to be produced, it will be almost-certainly non-strict. +freely :: ((?inputs::Inputs) => Gen a) -> Gen a +freely p = let ?inputs = Inputs [] in p + + +--------------- +-- Instances -- +--------------- + +instance Produce () where produce = arbitrary +instance Produce Bool where produce = arbitrary +instance Produce Ordering where produce = arbitrary + +instance Produce Char where produce = arbitrary +instance Produce Word where produce = arbitrary +instance Produce Int where produce = arbitrary +instance Produce Double where produce = arbitrary +instance Produce Float where produce = arbitrary +instance Produce Rational where produce = arbitrary +instance Produce Integer where produce = arbitrary + +instance Arbitrary a => Produce (Complex a) where + produce = arbitrary + +instance Produce a => Produce (Maybe a) where + produce = + oneof [ return Nothing + , Just <$> recur + ] + +instance (Produce a, Produce b) => Produce (Either a b) where + produce = + oneof [ Left <$> recur + , Right <$> recur + ] + +instance (Produce a) => Produce [a] where + produce = + frequency [ (1, return []) + , (1, (:) <$> recur + <*> recur) + ] + +instance Produce a => Produce (NonEmpty a) where + produce = (:|) <$> recur <*> recur diff --git a/src/Test/StrictCheck/Shaped.hs b/src/Test/StrictCheck/Shaped.hs --- a/src/Test/StrictCheck/Shaped.hs +++ b/src/Test/StrictCheck/Shaped.hs @@ -1,876 +1,875 @@ -{-# language InstanceSigs, DerivingStrategies #-} -{-# language PartialTypeSignatures #-} -{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-} -{-| This module defines the 'Shaped' typeclass, which is used to generically - manipulate values as fixed-points of higher-order functors in order to - analyze their structure, e.g. while observing evaluation. - - If you just care about testing the strictness of functions over datatypes - which are already instances of @Shaped@, you don't need to use this module. - - __Important note:__ To define new instances of 'Shaped' for types which - implement 'GHC.Generic', __an empty instance will suffice__, as all the - methods of 'Shaped' can be filled in by generic implementations. For - example: - - > import GHC.Generics as GHC - > import Generics.SOP as SOP - > - > data D = C deriving (GHC.Generic) - > - > instance SOP.Generic D - > instance SOP.HasDatatypeInfo D - > - > instance Shaped D - - Using the @DeriveAnyClass@ extension, this can be shortened to one line: - - > data D = C deriving (GHC.Generic, SOP.Generic, SOP.HasDatatypeInfo, Shaped) - - Manual instances of 'Shaped' are necessary for types which do not or cannot - implement GHC's @Generic@ typeclass, such as existential types, abstract - types, and GADTs. - - This module is heavily based upon the approach in "Data.Functor.Foldable", - which in turn is modeled after the paper "Functional Programming with - Bananas, Lenses, Envelopes and Barbed Wire" (1991) by Erik Meijer, Maarten - Fokkinga and Ross Paterson. If you don't yet understand recursion schemes - and want to understand this module, it's probably a good idea to familiarize - yourself with "Data.Functor.Foldable" before diving into this higher-order - generalization. --} -module Test.StrictCheck.Shaped - ( Shaped(..) - , module Test.StrictCheck.Shaped.Flattened - -- * Fixed-points of 'Shape's - , type (%)(..) - -- * Folds and unfolds over fixed-points of @Shape@s - , unwrap - , interleave - , (%) - , fuse - , translate - , fold - , unfold - , unzipWith - -- , reshape - -- * Rendering 'Shaped' things as structured text - , QName - , Rendered(..) - , RenderLevel(..) - , renderfold - -- * Tools for manually writing instances of 'Shaped' - -- ** Implementing 'Shaped' for primitive types - , Prim(..), unPrim - , projectPrim - , embedPrim - , matchPrim - , flatPrim - , renderPrim - , renderConstant - -- ** Implementing 'Shaped' for container types - , Containing(..) - , projectContainer - , embedContainer - -- * Generic implementation of the methods of 'Shaped' - , GShaped - , GShape(..) - , gProject - , gEmbed - , gMatch - , gRender - ) where - -import Type.Reflection -import Data.Functor.Product -import Data.Bifunctor -import Data.Bifunctor.Flip -import Data.Coerce - -import Generics.SOP hiding ( Shape ) - -import Data.Complex --- import Data.List.NonEmpty (NonEmpty(..)) - -import Test.StrictCheck.Shaped.Flattened - --- TODO: provide instances for all of Base - --- | When a type @a@ is @Shaped@, we know how to convert it into a --- representation parameterized by an arbitrary functor @f@, so that @Shape a f@ --- (the "shape of @a@ parameterized by @f@") is structurally identical to the --- topmost structure of @a@, but with @f@ wrapped around any subfields of @a@. --- --- Note that this is /not/ a recursive representation! The functor @f@ in --- question wraps the original type of the field and /not/ a @Shape@ of that --- field. --- --- For instance, the @Shape@ of @Either a b@ might be: --- --- > data EitherShape a b f --- > = LeftShape (f a) --- > | RightShape (f b) --- > --- > instance Shaped (Either a b) where --- > type Shape (Either a b) = EitherShape a b --- > ... --- --- The shape of a primitive type should be isomorphic to the primitive type, --- with the functor parameter left unused. -class Typeable a => Shaped (a :: *) where - -- | The @Shape@ of an @a@ is a type isomorphic to the outermost level of - -- structure in an @a@, parameterized by the functor @f@, which is wrapped - -- around any fields (of any type) in the original @a@. - type Shape a :: (* -> *) -> * - type Shape a = GShape a - - -- | Given a function to expand any @Shaped@ @x@ into an @f x@, expand an @a@ - -- into a @Shape a f@ - -- - -- That is: convert the top-most level of structure in the given @a@ into a - -- @Shape@, calling the provided function on each field in the @a@ to produce - -- the @f x@ necessary to fill that hole in the produced @Shape a f@. - -- - -- Inverse to 'embed'. - project :: (forall x. Shaped x => x -> f x) -> a -> Shape a f - - default project - :: GShaped a - => (forall x. Shaped x => x -> f x) - -> a - -> Shape a f - project = gProject - - -- | Given a function to collapse any @f x@ into a @Shaped@ @x@, collapse a - -- @Shape a f@ into merely an @a@ - -- - -- That is: eliminate the top-most @Shape@ by calling the provided function on - -- each field in that @Shape a f@, and using the results to fill in the pieces - -- necessary to build an @a@. - -- - -- Inverse to 'project'. - embed :: (forall x. Shaped x => f x -> x) -> Shape a f -> a - - default embed - :: GShaped a - => (forall x. Shaped x => f x -> x) - -> Shape a f - -> a - embed = gEmbed - - -- | Given two @Shape@s of the same type @a@ but parameterized by potentially - -- different functors @f@ and @g@, pattern-match on them to expose a uniform - -- view on their fields (a 'Flattened' @(Shape a)@) to a continuation which - -- may operate on those fields to produce some result - -- - -- If the two supplied @Shape@s do not structurally match, only the fields of - -- the first are given to the continuation. If they do match, the fields of - -- the second are also given, along with type-level proof that the types of - -- the two sets of fields align. - -- - -- This very general operation subsumes equality testing, mapping, zipping, - -- shrinking, and many other structural operations over @Shaped@ things. - -- - -- It is somewhat difficult to manually write instances for this method, but - -- consulting its generic implementation 'gMatch' may prove helpful. - -- - -- See "Test.StrictCheck.Shaped.Flattened" for more information. - match :: Shape a f -> Shape a g - -> (forall xs. All Shaped xs - => Flattened (Shape a) f xs - -> Maybe (Flattened (Shape a) g xs) - -> result) - -> result - - default match :: GShaped a - => Shape a f -> Shape a g - -> (forall xs. All Shaped xs - => Flattened (Shape a) f xs - -> Maybe (Flattened (Shape a) g xs) - -> result) - -> result - match = gMatch - - -- | Convert a @Shape a@ whose fields are some unknown constant type into a - -- 'RenderLevel' filled with that type - -- - -- This is a specialized pretty-printing mechanism which allows for displaying - -- counterexamples in a structured format. See the documentation for - -- 'RenderLevel'. - render :: Shape a (K x) -> RenderLevel x - - default render :: (GShaped a, HasDatatypeInfo a) - => Shape a (K x) -> RenderLevel x - render = gRender - - - --- * Fixed-points of 'Shape's - --- | A value of type @f % a@ has the same structure as an @a@, but with the --- structure of the functor @f@ interleaved at every field (including ones of --- types other than @a@). Read this type aloud as "a interleaved with f's". -newtype (f :: * -> *) % (a :: *) :: * where - Wrap :: f (Shape a ((%) f)) -> f % a - --- | Look inside a single level of an interleaved @f % a@. Inverse to the 'Wrap' --- constructor. -unwrap :: f % a -> f (Shape a ((%) f)) -unwrap (Wrap fs) = fs - - - --- * Folds and unfolds over fixed-points of @Shape@s - --- | Map a function across all the fields in a 'Shape' --- --- This function may change the functor over which the @Shape@ is parameterized. --- It can assume recursively that all the fields in the @Shape@ are themselves --- instances of @Shaped@ (which they should be!). This means that you can nest --- calls to @translate@ recursively. -translate :: forall a f g. Shaped a - => (forall x. Shaped x => f x -> g x) - -> Shape a f -> Shape a g -translate t d = match @a d d $ \flat _ -> - unflatten $ mapFlattened @Shaped t flat - --- | The equivalent of a fold (catamorphism) over recursively 'Shaped' values --- --- Given a function which folds an @f@ containing some @Shape x g@ into a @g x@, --- recursively fold any interleaved @f % a@ into a @g a@. -fold :: forall a f g. (Functor f, Shaped a) - => (forall x. Shaped x => f (Shape x g) -> g x) - -> f % a -> g a -fold alg = alg . fmap (translate @a (fold alg)) . unwrap - --- | The equivalent of an unfold (anamorphism) over recursively 'Shaped' values --- --- Given a function which unfolds an @f x@ into a @g@ containing some @Shape x --- f@, corecursively unfold any @f a@ into an interleaved @g % a@. -unfold :: forall a f g. (Functor g, Shaped a) - => (forall x. Shaped x => f x -> g (Shape x f)) - -> f a -> g % a -unfold coalg = Wrap . fmap (translate @a (unfold coalg)) . coalg - --- TODO: mapM, foldM, unfoldM, ... - --- | Fuse the interleaved @f@-structure out of a recursively interleaved @f % --- a@, given some way of fusing a single level @f x -> x@. --- --- This is a special case of 'fold'. -fuse - :: (Functor f, Shaped a) - => (forall x. f x -> x) - -> (f % a -> a) -fuse e = e . fold (fmap (embed e)) - --- | Interleave an @f@-structure at every recursive level of some @a@, given --- some way of generating a single level of structure @x -> f x@. --- --- This is a special case of 'unfold'. -interleave - :: (Functor f, Shaped a) - => (forall x. x -> f x) - -> (a -> f % a) -interleave p = unfold (fmap (project p)) . p - --- | An infix synonym for 'interleave' -(%) :: forall a f. (Functor f, Shaped a) - => (forall x. x -> f x) - -> a -> f % a -(%) = interleave - --- | A higher-kinded @unzipWith@, operating over interleaved structures --- --- Given a function splitting some @f x@ into a functor-product @Product g h x@, --- recursively split an interleaved @f % a@ into two interleaved structures: --- one built of @g@-shapes and one of @h@-shapes. --- --- Note that @Product ((%) g) ((%) h) a@ is isomorphic to @(g % a, h % a)@; to --- get the latter, pattern-match on the 'Pair' constructor of 'Product'. -unzipWith - :: (All Functor [f, g, h], Shaped a) - => (forall x. f x -> (g x, h x)) - -> (f % a -> (g % a, h % a)) -unzipWith split = - unPair . fold (crunch . pair . split) - where - crunch - :: forall x g h. - (Shaped x, Functor g, Functor h) - => Product g h (Shape x (Product ((%) g) ((%) h))) - -> Product ((%) g) ((%) h) x - crunch = - pair - . bimap (Wrap . fmap (translate @x (fst . unPair))) - (Wrap . fmap (translate @x (snd . unPair))) - . unPair - - pair :: (l x, r x) -> Product l r x - pair = uncurry Pair - - unPair :: Product l r x -> (l x, r x) - unPair (Pair lx rx) = (lx, rx) - --- | TODO: document this strange function -{- -reshape :: forall b a f g. (Shaped a, Shaped b, Functor f) - => (f (Shape b ((%) g)) -> g (Shape b ((%) g))) - -> (forall x. Shaped x => f % x -> g % x) - -> f % a -> g % a -reshape homo hetero d = - case eqTypeRep (typeRep @a) (typeRep @b) of - Nothing -> hetero d - Just HRefl -> - Wrap - $ homo . fmap (translate @a (reshape @b homo hetero)) - $ unwrap d --} - ----------------------------------- --- Rendering shapes for display -- ----------------------------------- - --- | Convert an @f % a@ into a structured pretty-printing representation, --- suitable for further display/processing -renderfold - :: forall a f. (Shaped a, Functor f) - => f % a -> Rendered f -renderfold = unK . fold oneLevel - where - oneLevel :: forall x. Shaped x - => f (Shape x (K (Rendered f))) - -> K (Rendered f) x - oneLevel = K . RWrap . fmap (render @x) - --- | A @QName@ is a qualified name --- --- Note: --- > type ModuleName = String --- > type DatatypeName = String -type QName = (ModuleName, DatatypeName, String) - --- | @RenderLevel@ is a functor whose outer shape contains all the information --- about how to pretty-format the outermost @Shape@ of some value. We use --- parametricity to make it difficult to construct incorrect 'render' methods, --- by asking the user merely to produce a single @RenderLevel@ and stitching --- nested @RenderLevel@s into complete 'Rendered' trees. -data RenderLevel x - = ConstructorD QName [x] - -- ^ A prefix constructor, and a list of its fields - | InfixD QName Associativity Fixity x x - -- ^ An infix constructor, its associativity and fixity, and its two fields - | RecordD QName [(QName, x)] - -- ^ A record constructor, and a list of its field names paired with fields - | CustomD Fixity - [Either (Either String (ModuleName, String)) (Fixity, x)] - -- ^ A custom pretty-printing representation (i.e. for abstract types), which - -- records a fixity and a list of tokens of three varieties: 1) raw strings, - -- 2) qualified strings (from some module), or 3) actual fields, annotated - -- with their fixity - deriving (Eq, Ord, Show, Functor) - --- | @Rendered f@ is the fixed-point of @f@ composed with 'RenderLevel': it --- alternates between @f@ shapes and @RenderLevel@s. Usually, @f@ will be the --- identity functor 'I', but not always. -data Rendered f - = RWrap (f (RenderLevel (Rendered f))) - - ----------------------------------------------------- --- Tools for manually writing instances of Shaped -- ----------------------------------------------------- - --- | The @Shape@ of a spine-strict container (i.e. a @Map@ or @Set@) is the same --- as a container of demands on its elements. However, this does not have the --- right /kind/ to be used as a @Shape@. --- --- The @Containing@ newtype solves this problem. By defining the @Shape@ of some --- container @(C a)@ to be @(C `Containing` a)@, you can use the methods --- @projectContainer@ and @embedContainer@ to implement @project@ and @embed@ --- for your container type (although you will still need to manually define --- @match@ and @render@). -newtype Containing h a f - = Container (h (f a)) - deriving (Eq, Ord, Show) - --- | Generic implementation of @project@ for any container type whose @Shape@ --- is represented as a @Containing@ newtype -projectContainer :: (Functor c, Shaped a) - => (forall x. Shaped x => x -> f x) - -> c a -> Containing c a f -projectContainer p x = Container (fmap p x) - --- | Generic implementation of @embed@ for any container type whose @Shape@ --- is represented as a @Containing@ newtype -embedContainer :: (Functor c, Shaped a) - => (forall x. Shaped x => f x -> x) - -> Containing c a f -> c a -embedContainer e (Container x) = fmap e x - - --- TODO: helper functions for matching and prettying containers - --- | The @Shape@ of a primitive type should be equivalent to the type itself. --- However, this does not have the right /kind/ to be used as a @Shape@. --- --- The @Prim@ newtype solves this problem. By defining the @Shape@ of some --- primitive type @p@ to be @Prim p@, you can use the methods @projectPrim@, --- @embedPrim@, @matchPrim@, and @prettyPrim@ to completely fill in the --- definition of the @Shaped@ class for a primitive type. --- --- __Note:__ It is only appropriate to use this @Shape@ representation when a --- type really is primitive, in that it contains no interesting substructure. --- If you use the @Prim@ representation inappropriately, StrictCheck will not be --- able to inspect the richer structure of the type in question. -newtype Prim (x :: *) (f :: * -> *) - = Prim x - deriving (Eq, Ord, Show) - deriving newtype (Num) - --- | Get the wrapped @x@ out of a @Prim x f@ (inverse to the @Prim@ constructor) -unPrim :: Prim x f -> x -unPrim (Prim x) = x - --- | Generic implementation of @project@ for any primitive type whose @Shape@ is --- is represented as a @Prim@ newtype -projectPrim :: (forall x. Shaped x => x -> f x) -> a -> Prim a f -projectPrim _ = Prim - --- | Generic implementation of @embed@ for any primitive type whose @Shape@ is --- is represented as a @Prim@ newtype -embedPrim :: (forall x. Shaped x => f x -> x) -> Prim a f -> a -embedPrim _ = unPrim - --- | Generic implementation of @match@ for any primitive type whose @Shape@ is --- is represented as a @Prim@ newtype with an underlying @Eq@ instance -matchPrim :: Eq a => Prim a f -> Prim a g - -> (forall xs. All Shaped xs - => Flattened (Prim a) f xs - -> Maybe (Flattened (Prim a) g xs) - -> result) - -> result -matchPrim (Prim a) (Prim b) k = - k (flatPrim a) - (if a == b then (Just (flatPrim b)) else Nothing) - --- | Helper for writing @match@ instances for primitive types which don't have --- @Eq@ instance --- --- This generates a @Flattened@ appropriate for using in the implementation of --- @match@. For more documentation on how to use this, see the documentation of --- 'match'. -flatPrim :: a -> Flattened (Prim a) g '[] -flatPrim x = Flattened (const (Prim x)) Nil - --- | Generic implementation of @render@ for any primitive type whose @Shape@ is --- is represented as a @Prim@ newtype -renderPrim :: Show a => Prim a (K x) -> RenderLevel x -renderPrim (Prim a) = renderConstant (show a) - --- | Given some @string@, generate a custom pretty-printing representation which --- just shows the string -renderConstant :: String -> RenderLevel x -renderConstant s = CustomD 11 [Left (Left s)] - --- TODO: What about demands for abstract types with > 1 type of unbounded-count field? - -{- -withFieldsContainer :: - forall c a f result. - (forall r h. - c (h a) -> - (forall x. Shaped x - => [h x] - -> (forall g. [g x] -> c (g a)) - -> r) - -> r) - -> Containing c a f - -> (forall xs. All Shaped xs - => NP f xs - -> (forall g. NP g xs -> Containing c a g) - -> result) - -> result -withFieldsContainer viaContaining (Container c) cont = - viaContaining c $ - \list un -> - withNP @Shaped list (Container . un) cont - --- TODO: Make this work for any number of lists of fields, by carefully using --- unsafeCoerce to deal with unknown list lengths - -withFieldsViaList :: - forall demand f result. - (forall r h. - demand h -> - (forall x. Shaped x - => [h x] - -> (forall g. [g x] -> demand g) - -> r) - -> r) - -> demand f - -> (forall xs. All Shaped xs - => NP f xs - -> (forall g. NP g xs -> demand g) - -> result) - -> result -withFieldsViaList viaList demand cont = - viaList demand $ - \list un -> - withNP @Shaped list un cont - -withNP :: forall c demand result f x. c x - => [f x] - -> (forall g. [g x] -> demand g) - -> (forall xs. All c xs - => NP f xs -> (forall g. NP g xs -> demand g) -> result) - -> result -withNP list unList cont = - withUnhomogenized @c list $ \np -> - cont np (unList . homogenize) - -withConcatenated :: NP (NP f) xss -> (forall xs. NP f xs -> r) -> r -withConcatenated pop cont = - case pop of - Nil -> cont Nil - (xs :* xss) -> withConcatenated xss (withPrepended xs cont) - where - withPrepended :: - NP f ys -> (forall zs. NP f zs -> r) - -> (forall zs. NP f zs -> r) - withPrepended pre k rest = - case pre of - Nil -> k rest - (x :* xs) -> withPrepended xs (k . (x :*)) rest - -homogenize :: All ((~) a) as => NP f as -> [f a] -homogenize Nil = [] -homogenize (a :* as) = a : homogenize as - -withUnhomogenized :: forall c a f r. - c a => [f a] -> (forall as. (All c as, All ((~) a) as) => NP f as -> r) -> r -withUnhomogenized [] k = k Nil -withUnhomogenized (a : as) k = - withUnhomogenized @c as $ \np -> k (a :* np) --} - - ---------------------------------------------------- --- Generic implementation of the Shaped methods -- ---------------------------------------------------- - --- | The 'Shape' used for generic implementations of 'Shaped' --- --- This wraps a sum-of-products representation from "Generics.SOP". -newtype GShape a f - = GS (NS (NP f) (Code a)) - --- | The collection of constraints necessary for a type to be given a generic --- implementation of the 'Shaped' methods -type GShaped a = - ( Generic a - , Shape a ~ GShape a - , All2 Shaped (Code a) - , SListI (Code a) - , All SListI (Code a) ) - --- | Generic 'project' -gProject :: GShaped a - => (forall x. Shaped x => x -> f x) - -> a -> Shape a f -gProject p !(from -> sop) = - GS (unSOP (hcliftA (Proxy @Shaped) (p . unI) sop)) - --- | Generic 'embed' -gEmbed :: GShaped a - => (forall x. Shaped x => f x -> x) - -> Shape a f -> a -gEmbed e !(GS d) = - to (hcliftA (Proxy @Shaped) (I . e) (SOP d)) - --- | Generic 'match' -gMatch :: forall a f g result. GShaped a - => Shape a f -> Shape a g - -> (forall xs. All Shaped xs - => Flattened (Shape a) f xs - -> Maybe (Flattened (Shape a) g xs) - -> result) - -> result -gMatch !(GS df) !(GS dg) cont = - go @(Code a) df (Just dg) $ \flatF mflatG -> - cont (flatGD flatF) (flatGD <$> mflatG) - where - go :: forall xss r. - (All SListI xss, All2 Shaped xss) - => NS (NP f) xss - -> Maybe (NS (NP g) xss) - -> (forall xs. All Shaped xs - => Flattened (Flip SOP xss) f xs - -> Maybe (Flattened (Flip SOP xss) g xs) - -> r) - -> r - go (Z (fieldsF :: _ xs)) (Just (Z fieldsG)) k = - k @xs (flatZ fieldsF) (Just (flatZ fieldsG)) - go (Z (fieldsF :: _ xs)) _ k = -- Nothing | Just (S _) - k @xs (flatZ fieldsF) Nothing - go (S moreF) Nothing k = - go moreF Nothing $ \(flatF :: _ xs) _ -> - k @xs (flatS flatF) Nothing - go (S moreF) (Just (Z _)) k = - go moreF Nothing $ \(flatF :: _ xs) _ -> - k @xs (flatS flatF) Nothing - go (S moreF) (Just (S moreG)) k = - go moreF (Just moreG) $ \(flatF :: _ xs) mflatG -> - k @xs (flatS flatF) (flatS <$> mflatG) - - flatZ - :: forall h xs xss. NP h xs -> Flattened (Flip SOP (xs : xss)) h xs - flatZ = Flattened (Flip . SOP . Z) - - flatS - :: forall h xs xs' xss. - Flattened (Flip SOP xss) h xs - -> Flattened (Flip SOP (xs' : xss)) h xs - flatS (Flattened un fields) = - Flattened (Flip . SOP . S . coerce . un) fields - - flatGD :: forall t h xs. - Flattened (Flip SOP (Code t)) h xs -> Flattened (GShape t) h xs - flatGD (Flattened un fields) = - Flattened (GS . coerce . un) fields - --- | Generic 'render' -gRender :: forall a x. (HasDatatypeInfo a, GShaped a) - => Shape a (K x) -> RenderLevel x -gRender (GS demand) = - case info of - ADT m d cs -> - renderC m d demand cs - Newtype m d c -> - renderC m d demand (c :* Nil) - where - info = datatypeInfo (Proxy @a) - - renderC :: forall as. ModuleName -> DatatypeName - -> NS (NP (K x)) as - -> NP ConstructorInfo as - -> RenderLevel x - renderC m d subShape constructors = - case (subShape, constructors) of - (Z demandFields, c :* _) -> - case c of - Constructor name -> - ConstructorD (m, d, name) $ - hcollapse demandFields - Infix name associativity fixity -> - case demandFields of - (K a :* K b :* Nil) -> - InfixD (m, d, name) associativity fixity a b - Record name fieldsInfo -> - RecordD (m, d, name) $ - zip ( hcollapse - . hliftA (\(FieldInfo f) -> K (m, d, f)) - $ fieldsInfo ) - (hcollapse demandFields) - (S another, _ :* different) -> - renderC m d another different - - ---------------- --- Instances -- ---------------- - -instance Shaped () -instance Shaped Bool -instance Shaped Ordering -instance Shaped a => Shaped (Maybe a) -instance (Shaped a, Shaped b) => Shaped (Either a b) -instance Shaped a => Shaped [a] - -instance (Typeable a, Typeable b) => Shaped (a -> b) where - type Shape (a -> b) = Prim (a -> b) - project = projectPrim - embed = embedPrim - match (Prim f) (Prim g) k = k (flatPrim f) (Just $ flatPrim g) - render _ = renderConstant (" :: " ++ show (typeRep @(a -> b))) - -instance Shaped Char where - type Shape Char = Prim Char - project = projectPrim - embed = embedPrim - match = matchPrim - render = renderPrim - -instance Shaped Word where - type Shape Word = Prim Word - project = projectPrim - embed = embedPrim - match = matchPrim - render = renderPrim - -instance Shaped Int where - type Shape Int = Prim Int - project = projectPrim - embed = embedPrim - match = matchPrim - render = renderPrim - -instance Shaped Double where - type Shape Double = Prim Double - project = projectPrim - embed = embedPrim - match = matchPrim - render = renderPrim - -instance Shaped Float where - type Shape Float = Prim Float - project = projectPrim - embed = embedPrim - match = matchPrim - render = renderPrim - -instance Shaped Rational where - type Shape Rational = Prim Rational - project = projectPrim - embed = embedPrim - match = matchPrim - render = renderPrim - -instance Shaped Integer where - type Shape Integer = Prim Integer - project = projectPrim - embed = embedPrim - match = matchPrim - render = renderPrim - -instance (Typeable a, Eq a, Show a) => Shaped (Complex a) where - type Shape (Complex a) = Prim (Complex a) - project = projectPrim - embed = embedPrim - match = matchPrim - render = renderPrim - --- instance Generic (NonEmpty a) --- instance HasDatatypeInfo (NonEmpty a) --- instance Shaped a => Shaped (NonEmpty a) where - --- Tree --- Map k --- Seq --- Set --- IntMap --- IntSet - -instance (Shaped a, Shaped b) => Shaped (a, b) -instance (Shaped a, Shaped b, Shaped c) => Shaped (a, b, c) -instance (Shaped a, Shaped b, Shaped c, Shaped d) => Shaped (a, b, c, d) -instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e - ) => Shaped - (a, b, c, d, e) -instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f - ) => Shaped - (a, b, c, d, e, f) -instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f - , Shaped g - ) => Shaped - (a, b, c, d, e, f, g) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h --- ) => Shaped --- (a, b, c, d, e, f, g, h) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i --- ) => Shaped --- (a, b, c, d, e, f, g, h, i) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j, k) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j, k, l) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l --- , Shaped m --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j, k, l, m) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l --- , Shaped m, Shaped n --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j, k, l, m, n) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l --- , Shaped m, Shaped n, Shaped o --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l --- , Shaped m, Shaped n, Shaped o, Shaped p --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l --- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l --- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l --- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r --- , Shaped s --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l --- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r --- , Shaped s, Shaped t --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l --- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r --- , Shaped s, Shaped t, Shaped u --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l --- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r --- , Shaped s, Shaped t, Shaped u, Shaped v --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l --- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r --- , Shaped s, Shaped t, Shaped u, Shaped v, Shaped w --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l --- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r --- , Shaped s, Shaped t, Shaped u, Shaped v, Shaped w, Shaped x --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l --- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r --- , Shaped s, Shaped t, Shaped u, Shaped v, Shaped w, Shaped x --- , Shaped y --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) --- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f --- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l --- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r --- , Shaped s, Shaped t, Shaped u, Shaped v, Shaped w, Shaped x --- , Shaped y, Shaped z --- ) => Shaped --- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z) +{-# language InstanceSigs, DerivingStrategies #-} +{-# language PartialTypeSignatures #-} +{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-} +{-| This module defines the 'Shaped' typeclass, which is used to generically + manipulate values as fixed-points of higher-order functors in order to + analyze their structure, e.g. while observing evaluation. + + If you just care about testing the strictness of functions over datatypes + which are already instances of @Shaped@, you don't need to use this module. + + __Important note:__ To define new instances of 'Shaped' for types which + implement 'GHC.Generic', __an empty instance will suffice__, as all the + methods of 'Shaped' can be filled in by generic implementations. For + example: + + > import GHC.Generics as GHC + > import Generics.SOP as SOP + > + > data D = C deriving (GHC.Generic) + > + > instance SOP.Generic D + > instance SOP.HasDatatypeInfo D + > + > instance Shaped D + + Using the @DeriveAnyClass@ extension, this can be shortened to one line: + + > data D = C deriving (GHC.Generic, SOP.Generic, SOP.HasDatatypeInfo, Shaped) + + Manual instances of 'Shaped' are necessary for types which do not or cannot + implement GHC's @Generic@ typeclass, such as existential types, abstract + types, and GADTs. + + This module is heavily based upon the approach in "Data.Functor.Foldable", + which in turn is modeled after the paper "Functional Programming with + Bananas, Lenses, Envelopes and Barbed Wire" (1991) by Erik Meijer, Maarten + Fokkinga and Ross Paterson. If you don't yet understand recursion schemes + and want to understand this module, it's probably a good idea to familiarize + yourself with "Data.Functor.Foldable" before diving into this higher-order + generalization. +-} +module Test.StrictCheck.Shaped + ( Shaped(..) + , module Test.StrictCheck.Shaped.Flattened + -- * Fixed-points of 'Shape's + , type (%)(..) + -- * Folds and unfolds over fixed-points of @Shape@s + , unwrap + , interleave + , (%) + , fuse + , translate + , fold + , unfold + , unzipWith + -- , reshape + -- * Rendering 'Shaped' things as structured text + , QName + , Rendered(..) + , RenderLevel(..) + , renderfold + -- * Tools for manually writing instances of 'Shaped' + -- ** Implementing 'Shaped' for primitive types + , Prim(..), unPrim + , projectPrim + , embedPrim + , matchPrim + , flatPrim + , renderPrim + , renderConstant + -- ** Implementing 'Shaped' for container types + , Containing(..) + , projectContainer + , embedContainer + -- * Generic implementation of the methods of 'Shaped' + , GShaped + , GShape(..) + , gProject + , gEmbed + , gMatch + , gRender + ) where + +import Type.Reflection +import Data.Functor.Product +import Data.Bifunctor +import Data.Bifunctor.Flip +import Data.Coerce +import Data.Kind (Type) + +import Generics.SOP hiding ( Shape ) + +import Data.Complex +import Data.List.NonEmpty (NonEmpty(..)) + +import Test.StrictCheck.Shaped.Flattened + +-- TODO: provide instances for all of Base + +-- | When a type @a@ is @Shaped@, we know how to convert it into a +-- representation parameterized by an arbitrary functor @f@, so that @Shape a f@ +-- (the "shape of @a@ parameterized by @f@") is structurally identical to the +-- topmost structure of @a@, but with @f@ wrapped around any subfields of @a@. +-- +-- Note that this is /not/ a recursive representation! The functor @f@ in +-- question wraps the original type of the field and /not/ a @Shape@ of that +-- field. +-- +-- For instance, the @Shape@ of @Either a b@ might be: +-- +-- > data EitherShape a b f +-- > = LeftShape (f a) +-- > | RightShape (f b) +-- > +-- > instance Shaped (Either a b) where +-- > type Shape (Either a b) = EitherShape a b +-- > ... +-- +-- The shape of a primitive type should be isomorphic to the primitive type, +-- with the functor parameter left unused. +class Typeable a => Shaped (a :: Type) where + -- | The @Shape@ of an @a@ is a type isomorphic to the outermost level of + -- structure in an @a@, parameterized by the functor @f@, which is wrapped + -- around any fields (of any type) in the original @a@. + type Shape a :: (Type -> Type) -> Type + type Shape a = GShape a + + -- | Given a function to expand any @Shaped@ @x@ into an @f x@, expand an @a@ + -- into a @Shape a f@ + -- + -- That is: convert the top-most level of structure in the given @a@ into a + -- @Shape@, calling the provided function on each field in the @a@ to produce + -- the @f x@ necessary to fill that hole in the produced @Shape a f@. + -- + -- Inverse to 'embed'. + project :: (forall x. Shaped x => x -> f x) -> a -> Shape a f + + default project + :: GShaped a + => (forall x. Shaped x => x -> f x) + -> a + -> Shape a f + project = gProject + + -- | Given a function to collapse any @f x@ into a @Shaped@ @x@, collapse a + -- @Shape a f@ into merely an @a@ + -- + -- That is: eliminate the top-most @Shape@ by calling the provided function on + -- each field in that @Shape a f@, and using the results to fill in the pieces + -- necessary to build an @a@. + -- + -- Inverse to 'project'. + embed :: (forall x. Shaped x => f x -> x) -> Shape a f -> a + + default embed + :: GShaped a + => (forall x. Shaped x => f x -> x) + -> Shape a f + -> a + embed = gEmbed + + -- | Given two @Shape@s of the same type @a@ but parameterized by potentially + -- different functors @f@ and @g@, pattern-match on them to expose a uniform + -- view on their fields (a 'Flattened' @(Shape a)@) to a continuation which + -- may operate on those fields to produce some result + -- + -- If the two supplied @Shape@s do not structurally match, only the fields of + -- the first are given to the continuation. If they do match, the fields of + -- the second are also given, along with type-level proof that the types of + -- the two sets of fields align. + -- + -- This very general operation subsumes equality testing, mapping, zipping, + -- shrinking, and many other structural operations over @Shaped@ things. + -- + -- It is somewhat difficult to manually write instances for this method, but + -- consulting its generic implementation 'gMatch' may prove helpful. + -- + -- See "Test.StrictCheck.Shaped.Flattened" for more information. + match :: Shape a f -> Shape a g + -> (forall xs. All Shaped xs + => Flattened (Shape a) f xs + -> Maybe (Flattened (Shape a) g xs) + -> result) + -> result + + default match :: GShaped a + => Shape a f -> Shape a g + -> (forall xs. All Shaped xs + => Flattened (Shape a) f xs + -> Maybe (Flattened (Shape a) g xs) + -> result) + -> result + match = gMatch + + -- | Convert a @Shape a@ whose fields are some unknown constant type into a + -- 'RenderLevel' filled with that type + -- + -- This is a specialized pretty-printing mechanism which allows for displaying + -- counterexamples in a structured format. See the documentation for + -- 'RenderLevel'. + render :: Shape a (K x) -> RenderLevel x + + default render :: (GShaped a, HasDatatypeInfo a) + => Shape a (K x) -> RenderLevel x + render = gRender + + + +-- * Fixed-points of 'Shape's + +-- | A value of type @f % a@ has the same structure as an @a@, but with the +-- structure of the functor @f@ interleaved at every field (including ones of +-- types other than @a@). Read this type aloud as "a interleaved with f's". +newtype (f :: Type -> Type) % (a :: Type) :: Type where + Wrap :: f (Shape a ((%) f)) -> f % a + +-- | Look inside a single level of an interleaved @f % a@. Inverse to the 'Wrap' +-- constructor. +unwrap :: f % a -> f (Shape a ((%) f)) +unwrap (Wrap fs) = fs + + + +-- * Folds and unfolds over fixed-points of @Shape@s + +-- | Map a function across all the fields in a 'Shape' +-- +-- This function may change the functor over which the @Shape@ is parameterized. +-- It can assume recursively that all the fields in the @Shape@ are themselves +-- instances of @Shaped@ (which they should be!). This means that you can nest +-- calls to @translate@ recursively. +translate :: forall a f g. Shaped a + => (forall x. Shaped x => f x -> g x) + -> Shape a f -> Shape a g +translate t d = match @a d d $ \flat _ -> + unflatten $ mapFlattened @Shaped t flat + +-- | The equivalent of a fold (catamorphism) over recursively 'Shaped' values +-- +-- Given a function which folds an @f@ containing some @Shape x g@ into a @g x@, +-- recursively fold any interleaved @f % a@ into a @g a@. +fold :: forall a f g. (Functor f, Shaped a) + => (forall x. Shaped x => f (Shape x g) -> g x) + -> f % a -> g a +fold alg = alg . fmap (translate @a (fold alg)) . unwrap + +-- | The equivalent of an unfold (anamorphism) over recursively 'Shaped' values +-- +-- Given a function which unfolds an @f x@ into a @g@ containing some @Shape x +-- f@, corecursively unfold any @f a@ into an interleaved @g % a@. +unfold :: forall a f g. (Functor g, Shaped a) + => (forall x. Shaped x => f x -> g (Shape x f)) + -> f a -> g % a +unfold coalg = Wrap . fmap (translate @a (unfold coalg)) . coalg + +-- TODO: mapM, foldM, unfoldM, ... + +-- | Fuse the interleaved @f@-structure out of a recursively interleaved @f % +-- a@, given some way of fusing a single level @f x -> x@. +-- +-- This is a special case of 'fold'. +fuse + :: (Functor f, Shaped a) + => (forall x. f x -> x) + -> (f % a -> a) +fuse e = e . fold (fmap (embed e)) + +-- | Interleave an @f@-structure at every recursive level of some @a@, given +-- some way of generating a single level of structure @x -> f x@. +-- +-- This is a special case of 'unfold'. +interleave + :: (Functor f, Shaped a) + => (forall x. x -> f x) + -> (a -> f % a) +interleave p = unfold (fmap (project p)) . p + +-- | An infix synonym for 'interleave' +(%) :: forall a f. (Functor f, Shaped a) + => (forall x. x -> f x) + -> a -> f % a +(%) = interleave + +-- | A higher-kinded @unzipWith@, operating over interleaved structures +-- +-- Given a function splitting some @f x@ into a functor-product @Product g h x@, +-- recursively split an interleaved @f % a@ into two interleaved structures: +-- one built of @g@-shapes and one of @h@-shapes. +-- +-- Note that @Product ((%) g) ((%) h) a@ is isomorphic to @(g % a, h % a)@; to +-- get the latter, pattern-match on the 'Pair' constructor of 'Product'. +unzipWith + :: (All Functor [f, g, h], Shaped a) + => (forall x. f x -> (g x, h x)) + -> (f % a -> (g % a, h % a)) +unzipWith split = + unPair . fold (crunch . pair . split) + where + crunch + :: forall x g h. + (Shaped x, Functor g, Functor h) + => Product g h (Shape x (Product ((%) g) ((%) h))) + -> Product ((%) g) ((%) h) x + crunch = + pair + . bimap (Wrap . fmap (translate @x (fst . unPair))) + (Wrap . fmap (translate @x (snd . unPair))) + . unPair + + pair :: (l x, r x) -> Product l r x + pair = uncurry Pair + + unPair :: Product l r x -> (l x, r x) + unPair (Pair lx rx) = (lx, rx) + +-- | TODO: document this strange function +{- +reshape :: forall b a f g. (Shaped a, Shaped b, Functor f) + => (f (Shape b ((%) g)) -> g (Shape b ((%) g))) + -> (forall x. Shaped x => f % x -> g % x) + -> f % a -> g % a +reshape homo hetero d = + case eqTypeRep (typeRep @a) (typeRep @b) of + Nothing -> hetero d + Just HRefl -> + Wrap + $ homo . fmap (translate @a (reshape @b homo hetero)) + $ unwrap d +-} + +---------------------------------- +-- Rendering shapes for display -- +---------------------------------- + +-- | Convert an @f % a@ into a structured pretty-printing representation, +-- suitable for further display/processing +renderfold + :: forall a f. (Shaped a, Functor f) + => f % a -> Rendered f +renderfold = unK . fold oneLevel + where + oneLevel :: forall x. Shaped x + => f (Shape x (K (Rendered f))) + -> K (Rendered f) x + oneLevel = K . RWrap . fmap (render @x) + +-- | A @QName@ is a qualified name +-- +-- Note: +-- > type ModuleName = String +-- > type DatatypeName = String +type QName = (ModuleName, DatatypeName, String) + +-- | @RenderLevel@ is a functor whose outer shape contains all the information +-- about how to pretty-format the outermost @Shape@ of some value. We use +-- parametricity to make it difficult to construct incorrect 'render' methods, +-- by asking the user merely to produce a single @RenderLevel@ and stitching +-- nested @RenderLevel@s into complete 'Rendered' trees. +data RenderLevel x + = ConstructorD QName [x] + -- ^ A prefix constructor, and a list of its fields + | InfixD QName Associativity Fixity x x + -- ^ An infix constructor, its associativity and fixity, and its two fields + | RecordD QName [(QName, x)] + -- ^ A record constructor, and a list of its field names paired with fields + | CustomD Fixity + [Either (Either String (ModuleName, String)) (Fixity, x)] + -- ^ A custom pretty-printing representation (i.e. for abstract types), which + -- records a fixity and a list of tokens of three varieties: 1) raw strings, + -- 2) qualified strings (from some module), or 3) actual fields, annotated + -- with their fixity + deriving (Eq, Ord, Show, Functor) + +-- | @Rendered f@ is the fixed-point of @f@ composed with 'RenderLevel': it +-- alternates between @f@ shapes and @RenderLevel@s. Usually, @f@ will be the +-- identity functor 'I', but not always. +data Rendered f + = RWrap (f (RenderLevel (Rendered f))) + + +---------------------------------------------------- +-- Tools for manually writing instances of Shaped -- +---------------------------------------------------- + +-- | The @Shape@ of a spine-strict container (i.e. a @Map@ or @Set@) is the same +-- as a container of demands on its elements. However, this does not have the +-- right /kind/ to be used as a @Shape@. +-- +-- The @Containing@ newtype solves this problem. By defining the @Shape@ of some +-- container @(C a)@ to be @(C `Containing` a)@, you can use the methods +-- @projectContainer@ and @embedContainer@ to implement @project@ and @embed@ +-- for your container type (although you will still need to manually define +-- @match@ and @render@). +newtype Containing h a f + = Container (h (f a)) + deriving (Eq, Ord, Show) + +-- | Generic implementation of @project@ for any container type whose @Shape@ +-- is represented as a @Containing@ newtype +projectContainer :: (Functor c, Shaped a) + => (forall x. Shaped x => x -> f x) + -> c a -> Containing c a f +projectContainer p x = Container (fmap p x) + +-- | Generic implementation of @embed@ for any container type whose @Shape@ +-- is represented as a @Containing@ newtype +embedContainer :: (Functor c, Shaped a) + => (forall x. Shaped x => f x -> x) + -> Containing c a f -> c a +embedContainer e (Container x) = fmap e x + + +-- TODO: helper functions for matching and prettying containers + +-- | The @Shape@ of a primitive type should be equivalent to the type itself. +-- However, this does not have the right /kind/ to be used as a @Shape@. +-- +-- The @Prim@ newtype solves this problem. By defining the @Shape@ of some +-- primitive type @p@ to be @Prim p@, you can use the methods @projectPrim@, +-- @embedPrim@, @matchPrim@, and @prettyPrim@ to completely fill in the +-- definition of the @Shaped@ class for a primitive type. +-- +-- __Note:__ It is only appropriate to use this @Shape@ representation when a +-- type really is primitive, in that it contains no interesting substructure. +-- If you use the @Prim@ representation inappropriately, StrictCheck will not be +-- able to inspect the richer structure of the type in question. +newtype Prim (x :: Type) (f :: Type -> Type) + = Prim x + deriving (Eq, Ord, Show) + deriving newtype (Num) + +-- | Get the wrapped @x@ out of a @Prim x f@ (inverse to the @Prim@ constructor) +unPrim :: Prim x f -> x +unPrim (Prim x) = x + +-- | Generic implementation of @project@ for any primitive type whose @Shape@ is +-- is represented as a @Prim@ newtype +projectPrim :: (forall x. Shaped x => x -> f x) -> a -> Prim a f +projectPrim _ = Prim + +-- | Generic implementation of @embed@ for any primitive type whose @Shape@ is +-- is represented as a @Prim@ newtype +embedPrim :: (forall x. Shaped x => f x -> x) -> Prim a f -> a +embedPrim _ = unPrim + +-- | Generic implementation of @match@ for any primitive type whose @Shape@ is +-- is represented as a @Prim@ newtype with an underlying @Eq@ instance +matchPrim :: Eq a => Prim a f -> Prim a g + -> (forall xs. All Shaped xs + => Flattened (Prim a) f xs + -> Maybe (Flattened (Prim a) g xs) + -> result) + -> result +matchPrim (Prim a) (Prim b) k = + k (flatPrim a) + (if a == b then (Just (flatPrim b)) else Nothing) + +-- | Helper for writing @match@ instances for primitive types which don't have +-- @Eq@ instance +-- +-- This generates a @Flattened@ appropriate for using in the implementation of +-- @match@. For more documentation on how to use this, see the documentation of +-- 'match'. +flatPrim :: a -> Flattened (Prim a) g '[] +flatPrim x = Flattened (const (Prim x)) Nil + +-- | Generic implementation of @render@ for any primitive type whose @Shape@ is +-- is represented as a @Prim@ newtype +renderPrim :: Show a => Prim a (K x) -> RenderLevel x +renderPrim (Prim a) = renderConstant (show a) + +-- | Given some @string@, generate a custom pretty-printing representation which +-- just shows the string +renderConstant :: String -> RenderLevel x +renderConstant s = CustomD 11 [Left (Left s)] + +-- TODO: What about demands for abstract types with > 1 type of unbounded-count field? + +{- +withFieldsContainer :: + forall c a f result. + (forall r h. + c (h a) -> + (forall x. Shaped x + => [h x] + -> (forall g. [g x] -> c (g a)) + -> r) + -> r) + -> Containing c a f + -> (forall xs. All Shaped xs + => NP f xs + -> (forall g. NP g xs -> Containing c a g) + -> result) + -> result +withFieldsContainer viaContaining (Container c) cont = + viaContaining c $ + \list un -> + withNP @Shaped list (Container . un) cont + +-- TODO: Make this work for any number of lists of fields, by carefully using +-- unsafeCoerce to deal with unknown list lengths + +withFieldsViaList :: + forall demand f result. + (forall r h. + demand h -> + (forall x. Shaped x + => [h x] + -> (forall g. [g x] -> demand g) + -> r) + -> r) + -> demand f + -> (forall xs. All Shaped xs + => NP f xs + -> (forall g. NP g xs -> demand g) + -> result) + -> result +withFieldsViaList viaList demand cont = + viaList demand $ + \list un -> + withNP @Shaped list un cont + +withNP :: forall c demand result f x. c x + => [f x] + -> (forall g. [g x] -> demand g) + -> (forall xs. All c xs + => NP f xs -> (forall g. NP g xs -> demand g) -> result) + -> result +withNP list unList cont = + withUnhomogenized @c list $ \np -> + cont np (unList . homogenize) + +withConcatenated :: NP (NP f) xss -> (forall xs. NP f xs -> r) -> r +withConcatenated pop cont = + case pop of + Nil -> cont Nil + (xs :* xss) -> withConcatenated xss (withPrepended xs cont) + where + withPrepended :: + NP f ys -> (forall zs. NP f zs -> r) + -> (forall zs. NP f zs -> r) + withPrepended pre k rest = + case pre of + Nil -> k rest + (x :* xs) -> withPrepended xs (k . (x :*)) rest + +homogenize :: All ((~) a) as => NP f as -> [f a] +homogenize Nil = [] +homogenize (a :* as) = a : homogenize as + +withUnhomogenized :: forall c a f r. + c a => [f a] -> (forall as. (All c as, All ((~) a) as) => NP f as -> r) -> r +withUnhomogenized [] k = k Nil +withUnhomogenized (a : as) k = + withUnhomogenized @c as $ \np -> k (a :* np) +-} + + +--------------------------------------------------- +-- Generic implementation of the Shaped methods -- +--------------------------------------------------- + +-- | The 'Shape' used for generic implementations of 'Shaped' +-- +-- This wraps a sum-of-products representation from "Generics.SOP". +newtype GShape a f + = GS (NS (NP f) (Code a)) + +-- | The collection of constraints necessary for a type to be given a generic +-- implementation of the 'Shaped' methods +type GShaped a = + ( Generic a + , Shape a ~ GShape a + , All2 Shaped (Code a) + , SListI (Code a) + , All SListI (Code a) ) + +-- | Generic 'project' +gProject :: GShaped a + => (forall x. Shaped x => x -> f x) + -> a -> Shape a f +gProject p !(from -> sop) = + GS (unSOP (hcliftA (Proxy @Shaped) (p . unI) sop)) + +-- | Generic 'embed' +gEmbed :: GShaped a + => (forall x. Shaped x => f x -> x) + -> Shape a f -> a +gEmbed e !(GS d) = + to (hcliftA (Proxy @Shaped) (I . e) (SOP d)) + +-- | Generic 'match' +gMatch :: forall a f g result. GShaped a + => Shape a f -> Shape a g + -> (forall xs. All Shaped xs + => Flattened (Shape a) f xs + -> Maybe (Flattened (Shape a) g xs) + -> result) + -> result +gMatch !(GS df) !(GS dg) cont = + go @(Code a) df (Just dg) $ \flatF mflatG -> + cont (flatGD flatF) (flatGD <$> mflatG) + where + go :: forall xss r. + (All SListI xss, All2 Shaped xss) + => NS (NP f) xss + -> Maybe (NS (NP g) xss) + -> (forall xs. All Shaped xs + => Flattened (Flip SOP xss) f xs + -> Maybe (Flattened (Flip SOP xss) g xs) + -> r) + -> r + go (Z (fieldsF :: _ xs)) (Just (Z fieldsG)) k = + k @xs (flatZ fieldsF) (Just (flatZ fieldsG)) + go (Z (fieldsF :: _ xs)) _ k = -- Nothing | Just (S _) + k @xs (flatZ fieldsF) Nothing + go (S moreF) Nothing k = + go moreF Nothing $ \(flatF :: _ xs) _ -> + k @xs (flatS flatF) Nothing + go (S moreF) (Just (Z _)) k = + go moreF Nothing $ \(flatF :: _ xs) _ -> + k @xs (flatS flatF) Nothing + go (S moreF) (Just (S moreG)) k = + go moreF (Just moreG) $ \(flatF :: _ xs) mflatG -> + k @xs (flatS flatF) (flatS <$> mflatG) + + flatZ + :: forall h xs xss. NP h xs -> Flattened (Flip SOP (xs : xss)) h xs + flatZ = Flattened (Flip . SOP . Z) + + flatS + :: forall h xs xs' xss. + Flattened (Flip SOP xss) h xs + -> Flattened (Flip SOP (xs' : xss)) h xs + flatS (Flattened un fields) = + Flattened (Flip . SOP . S . coerce . un) fields + + flatGD :: forall t h xs. + Flattened (Flip SOP (Code t)) h xs -> Flattened (GShape t) h xs + flatGD (Flattened un fields) = + Flattened (GS . coerce . un) fields + +-- | Generic 'render' +gRender :: forall a x. (HasDatatypeInfo a, GShaped a) + => Shape a (K x) -> RenderLevel x +gRender (GS demand) = + case info of + ADT m d cs _s -> + renderC m d demand cs + Newtype m d c -> + renderC m d demand (c :* Nil) + where + info = datatypeInfo (Proxy @a) + + renderC :: forall as. ModuleName -> DatatypeName + -> NS (NP (K x)) as + -> NP ConstructorInfo as + -> RenderLevel x + renderC m d subShape constructors = + case (subShape, constructors) of + (Z demandFields, c :* _) -> + case c of + Constructor name -> + ConstructorD (m, d, name) $ + hcollapse demandFields + Infix name associativity fixity -> + case demandFields of + (K a :* K b :* Nil) -> + InfixD (m, d, name) associativity fixity a b + Record name fieldsInfo -> + RecordD (m, d, name) $ + zip ( hcollapse + . hliftA (\(FieldInfo f) -> K (m, d, f)) + $ fieldsInfo ) + (hcollapse demandFields) + (S another, _ :* different) -> + renderC m d another different + + +--------------- +-- Instances -- +--------------- + +instance Shaped () +instance Shaped Bool +instance Shaped Ordering +instance Shaped a => Shaped (Maybe a) +instance (Shaped a, Shaped b) => Shaped (Either a b) +instance Shaped a => Shaped [a] + +instance (Typeable a, Typeable b) => Shaped (a -> b) where + type Shape (a -> b) = Prim (a -> b) + project = projectPrim + embed = embedPrim + match (Prim f) (Prim g) k = k (flatPrim f) (Just $ flatPrim g) + render _ = renderConstant (" :: " ++ show (typeRep @(a -> b))) + +instance Shaped Char where + type Shape Char = Prim Char + project = projectPrim + embed = embedPrim + match = matchPrim + render = renderPrim + +instance Shaped Word where + type Shape Word = Prim Word + project = projectPrim + embed = embedPrim + match = matchPrim + render = renderPrim + +instance Shaped Int where + type Shape Int = Prim Int + project = projectPrim + embed = embedPrim + match = matchPrim + render = renderPrim + +instance Shaped Double where + type Shape Double = Prim Double + project = projectPrim + embed = embedPrim + match = matchPrim + render = renderPrim + +instance Shaped Float where + type Shape Float = Prim Float + project = projectPrim + embed = embedPrim + match = matchPrim + render = renderPrim + +instance Shaped Rational where + type Shape Rational = Prim Rational + project = projectPrim + embed = embedPrim + match = matchPrim + render = renderPrim + +instance Shaped Integer where + type Shape Integer = Prim Integer + project = projectPrim + embed = embedPrim + match = matchPrim + render = renderPrim + +instance (Typeable a, Eq a, Show a) => Shaped (Complex a) where + type Shape (Complex a) = Prim (Complex a) + project = projectPrim + embed = embedPrim + match = matchPrim + render = renderPrim + +instance Shaped a => Shaped (NonEmpty a) where + +-- Tree +-- Map k +-- Seq +-- Set +-- IntMap +-- IntSet + +instance (Shaped a, Shaped b) => Shaped (a, b) +instance (Shaped a, Shaped b, Shaped c) => Shaped (a, b, c) +instance (Shaped a, Shaped b, Shaped c, Shaped d) => Shaped (a, b, c, d) +instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e + ) => Shaped + (a, b, c, d, e) +instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f + ) => Shaped + (a, b, c, d, e, f) +instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f + , Shaped g + ) => Shaped + (a, b, c, d, e, f, g) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h +-- ) => Shaped +-- (a, b, c, d, e, f, g, h) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j, k) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j, k, l) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l +-- , Shaped m +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j, k, l, m) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l +-- , Shaped m, Shaped n +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j, k, l, m, n) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l +-- , Shaped m, Shaped n, Shaped o +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l +-- , Shaped m, Shaped n, Shaped o, Shaped p +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l +-- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l +-- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l +-- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r +-- , Shaped s +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l +-- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r +-- , Shaped s, Shaped t +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l +-- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r +-- , Shaped s, Shaped t, Shaped u +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l +-- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r +-- , Shaped s, Shaped t, Shaped u, Shaped v +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l +-- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r +-- , Shaped s, Shaped t, Shaped u, Shaped v, Shaped w +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l +-- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r +-- , Shaped s, Shaped t, Shaped u, Shaped v, Shaped w, Shaped x +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l +-- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r +-- , Shaped s, Shaped t, Shaped u, Shaped v, Shaped w, Shaped x +-- , Shaped y +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y) +-- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f +-- , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l +-- , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r +-- , Shaped s, Shaped t, Shaped u, Shaped v, Shaped w, Shaped x +-- , Shaped y, Shaped z +-- ) => Shaped +-- (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z) diff --git a/src/Test/StrictCheck/Shaped/Flattened.hs b/src/Test/StrictCheck/Shaped/Flattened.hs --- a/src/Test/StrictCheck/Shaped/Flattened.hs +++ b/src/Test/StrictCheck/Shaped/Flattened.hs @@ -1,57 +1,57 @@ -{-| The @match@ function in the typeclass 'Test.StrictCheck.Shaped.Shaped' - allows you to uniformly operate over all the fields in a given piece of - data--for instance, consuming them, iterating over them, counting them, - etc. This module defines a uniform representation to allow this to work. - - This is in the nitty-gritty of how StrictCheck works: you do not need to - understand this in order to use StrictCheck, unless you need to declare - custom instances of @Shaped@ for a type not supported by StrictCheck's - generics mechanism (i.e. GADTs, existential types, abstract types). --} - -module Test.StrictCheck.Shaped.Flattened where - -import Generics.SOP - --- | The @Flattened@ type contains all the fields in a piece of data --- (represented as an n-ary product 'NP' from "Generics.SOP"), paired with a way --- to re-assemble them into a value of the original datatype. --- --- @Flattened d f xs@ can be read as "some value of type @d f@, which has been --- separated into an n-ary product @NP f xs@ and a function which can reconstruct --- a value @d h@ for any @h@, given an n-ary product with matching field types --- to the one contained here. --- --- Pay attention to the kinds! @d :: (* -> *) -> *@, @f :: * -> *@, and --- @xs :: [*]@. --- --- For types which are literally a collection of fields with no extra --- information, the reconstruction function merely converts the given list of --- fields back into a value of the original type. For types which contain extra --- information in their values (beyond what StrictCheck considers fields), this --- function should contain that information, and re-attach it to the field --- values it receives. -data Flattened d f xs where - Flattened - :: (forall h. NP h xs -> d h) - -> NP f xs - -> Flattened d f xs - --- | Use the re-assembly close in a @Flattened@ to yield a value of the original --- type from which it was derived. -unflatten :: Flattened d f xs -> d f -unflatten (Flattened u p) = u p - --- | If all the fields in a @Flattened@ satisfy some constraint, map a function --- expecting that constraint across all the fields. This may change the functor --- over which the @Flattened@ value is parameterized. -mapFlattened :: forall c d f g xs. All c xs - => (forall x. c x => f x -> g x) -> Flattened d f xs -> Flattened d g xs -mapFlattened t (Flattened u p) = - Flattened u (hcliftA (Proxy @c) t p) - --- | 'traverseFlattened' is to 'traverse' like 'mapFlattened' is to 'fmap'. -traverseFlattened :: forall c d f g h xs. (All c xs, Applicative h) - => (forall x. c x => f x -> h (g x)) -> Flattened d f xs -> h (Flattened d g xs) -traverseFlattened t (Flattened u p) = - Flattened u <$> hctraverse' (Proxy @c) t p +{-| The @match@ function in the typeclass 'Test.StrictCheck.Shaped.Shaped' + allows you to uniformly operate over all the fields in a given piece of + data--for instance, consuming them, iterating over them, counting them, + etc. This module defines a uniform representation to allow this to work. + + This is in the nitty-gritty of how StrictCheck works: you do not need to + understand this in order to use StrictCheck, unless you need to declare + custom instances of @Shaped@ for a type not supported by StrictCheck's + generics mechanism (i.e. GADTs, existential types, abstract types). +-} + +module Test.StrictCheck.Shaped.Flattened where + +import Generics.SOP + +-- | The @Flattened@ type contains all the fields in a piece of data +-- (represented as an n-ary product 'NP' from "Generics.SOP"), paired with a way +-- to re-assemble them into a value of the original datatype. +-- +-- @Flattened d f xs@ can be read as "some value of type @d f@, which has been +-- separated into an n-ary product @NP f xs@ and a function which can reconstruct +-- a value @d h@ for any @h@, given an n-ary product with matching field types +-- to the one contained here. +-- +-- Pay attention to the kinds! @d :: (Type -> Type) -> Type@, @f :: Type -> Type@, +-- and @xs :: [Type]@. +-- +-- For types which are literally a collection of fields with no extra +-- information, the reconstruction function merely converts the given list of +-- fields back into a value of the original type. For types which contain extra +-- information in their values (beyond what StrictCheck considers fields), this +-- function should contain that information, and re-attach it to the field +-- values it receives. +data Flattened d f xs where + Flattened + :: (forall h. NP h xs -> d h) + -> NP f xs + -> Flattened d f xs + +-- | Use the re-assembly close in a @Flattened@ to yield a value of the original +-- type from which it was derived. +unflatten :: Flattened d f xs -> d f +unflatten (Flattened u p) = u p + +-- | If all the fields in a @Flattened@ satisfy some constraint, map a function +-- expecting that constraint across all the fields. This may change the functor +-- over which the @Flattened@ value is parameterized. +mapFlattened :: forall c d f g xs. All c xs + => (forall x. c x => f x -> g x) -> Flattened d f xs -> Flattened d g xs +mapFlattened t (Flattened u p) = + Flattened u (hcliftA (Proxy @c) t p) + +-- | 'traverseFlattened' is to 'traverse' like 'mapFlattened' is to 'fmap'. +traverseFlattened :: forall c d f g h xs. (All c xs, Applicative h) + => (forall x. c x => f x -> h (g x)) -> Flattened d f xs -> h (Flattened d g xs) +traverseFlattened t (Flattened u p) = + Flattened u <$> hctraverse' (Proxy @c) t p diff --git a/src/Test/StrictCheck/TH.hs b/src/Test/StrictCheck/TH.hs --- a/src/Test/StrictCheck/TH.hs +++ b/src/Test/StrictCheck/TH.hs @@ -1,95 +1,109 @@ -{-| Template Haskell to derive pattern synonyms for working with demands --} -{-# LANGUAGE TemplateHaskell #-} -module Test.StrictCheck.TH - ( derivePatternSynonyms - ) where - -import Generics.SOP (NP(..), NS(..)) -import Test.StrictCheck.Demand -import Test.StrictCheck.Shaped - -import Control.Monad (when) -import Language.Haskell.TH - --- TODO: generate COMPLETE pragmas to avoid partiality warnings - --- | Generates the proper type signature for a pattern. The first --- argument is the list of constructor field types, and the second --- argument is the type of the constructor constructs. This function --- inserts '->' and 'Demand' at the correct places. -patternTypeDec :: [Type] -> Type -> Type -patternTypeDec [] ty = AppT (ConT ''Demand) ty -patternTypeDec (arg:args) ty = AppT (AppT ArrowT $ AppT (ConT ''Demand) arg) - (patternTypeDec args ty) - -prefixPatternDec :: Int -> Name -> [Name] -> Pat -> Dec -prefixPatternDec idx patName binderNames npPat = - PatSynD patName - (PrefixPatSyn binderNames) - ImplBidir - (ConP 'Wrap [ConP 'Eval [ConP 'GS [sumPattern idx npPat]]]) - -infixPatternDec :: Int - -> Name - -> Name -> Name -- LHS then RHS - -> Pat - -> Dec -infixPatternDec idx patName lhsBinder rhsBinder npPat = - PatSynD patName - (InfixPatSyn lhsBinder rhsBinder) - ImplBidir - (ConP 'Wrap [ConP 'Eval [ConP 'GS [sumPattern idx npPat]]]) - -sumPattern :: Int -> Pat -> Pat -sumPattern idx p | idx <= 0 = ConP 'Z [p] - | otherwise = ConP 'S [sumPattern (idx-1) p] - -productPattern :: [Type] -> Q (Pat, [Name]) -productPattern [] = return (ConP 'Nil [], []) -productPattern (_:args) = do - (tailPat, names) <- productPattern args - freshName <- newName "x" - return (InfixP (VarP freshName) '(:*) tailPat, freshName : names) - --- | Turns a constructor into its corresponding pattern synonym --- declaration. The `Int` argument is the index of the constructor. --- For example, Nil would be the 0th constructor, and Cons would be --- the 1st constructor of the type data List a = Nil | Cons a (List a). -constructor2PatternDec :: Type -> Int -> Con -> Q (Dec, Dec) -constructor2PatternDec ty idx (NormalC conName argTypes) = do - (npPat, names) <- productPattern (map snd argTypes) - return (PatSynSigD patDecName (patternTypeDec (map snd argTypes) ty), - prefixPatternDec idx patDecName names npPat) - where patDecName = mkName (nameBase conName ++ "'") -constructor2PatternDec ty idx (InfixC argType1 conName argType2) = do - let argTypes = [argType1, argType2] - (npPat, names) <- productPattern (map snd argTypes) - when (length names /= 2) $ - reportError "The impossible happened: Infix Pattern have more than 2 binders" - let nm1:nm2:_ = names - return (PatSynSigD patDecName (patternTypeDec (map snd argTypes) ty), - infixPatternDec idx patDecName nm1 nm2 npPat) - where patDecName = mkName (nameBase conName ++ "%") -constructor2PatternDec _ _ _ = - fail "Test.StrictCheck.TH cannot derive pattern synonyms for fancy types" - --- | Template Haskell splice to generate pattern synonym declarations for --- working with explicitly-represented demands on a type whose 'Shape' is --- implemented generically as a 'GShape' -derivePatternSynonyms :: Name -> Q [Dec] -derivePatternSynonyms name = do - nameInfo <- reify name - case nameInfo of - TyConI (DataD _ tyName tyVars _ constrs _) -> do - let tyVarTypes = map (\tyVar -> case tyVar of - PlainTV nm -> VarT nm - KindedTV nm kd -> SigT (VarT nm) kd - ) - tyVars - ty = foldl AppT (ConT tyName) tyVarTypes - decs <- mapM (uncurry (constructor2PatternDec ty)) (zip [0..] constrs) - return $ (map fst decs) ++ (map snd decs) - _ -> do - reportError (show name ++ " is not a data type name") - return [] +{-# LANGUAGE TemplateHaskell #-} + +-- | Template Haskell to derive pattern synonyms for working with demands +module Test.StrictCheck.TH + ( derivePatternSynonyms, + ) +where + +import Generics.SOP (NP (..), NS (..)) +import Language.Haskell.TH +import Test.StrictCheck.Demand +import Test.StrictCheck.Shaped + +-- TODO: generate COMPLETE pragmas to avoid partiality warnings + +-- | Generates the proper type signature for a pattern. The first +-- argument is the list of constructor field types, and the second +-- argument is the type of the constructor constructs. This function +-- inserts '->' and 'Demand' at the correct places. +patternTypeDec :: [Type] -> Type -> Type +patternTypeDec [] ty = AppT (ConT ''Demand) ty +patternTypeDec (arg : args) ty = + AppT + (AppT ArrowT $ AppT (ConT ''Demand) arg) + (patternTypeDec args ty) + +prefixPatternDec :: Int -> Name -> [Name] -> Pat -> Dec +prefixPatternDec idx patName binderNames npPat = + PatSynD + patName + (PrefixPatSyn binderNames) + ImplBidir + (ConP 'Wrap [] [ConP 'Eval [] [ConP 'GS [] [sumPattern idx npPat]]]) + +infixPatternDec :: + Int -> + Name -> + Name -> + Name -> -- LHS then RHS + Pat -> + Dec +infixPatternDec idx patName lhsBinder rhsBinder npPat = + PatSynD + patName + (InfixPatSyn lhsBinder rhsBinder) + ImplBidir + (ConP 'Wrap [] [ConP 'Eval [] [ConP 'GS [] [sumPattern idx npPat]]]) + +sumPattern :: Int -> Pat -> Pat +sumPattern idx p + | idx <= 0 = ConP 'Z [] [p] + | otherwise = ConP 'S [] [sumPattern (idx - 1) p] + +productPattern :: [Type] -> Q (Pat, [Name]) +productPattern [] = return (ConP 'Nil [] [], []) +productPattern (_ : args) = do + (tailPat, names) <- productPattern args + freshName <- newName "x" + return (InfixP (VarP freshName) '(:*) tailPat, freshName : names) + +-- | Turns a constructor into its corresponding pattern synonym +-- declaration. The `Int` argument is the index of the constructor. +-- For example, Nil would be the 0th constructor, and Cons would be +-- the 1st constructor of the type data List a = Nil | Cons a (List a). +constructor2PatternDec :: Type -> Int -> Con -> Q (Dec, Dec) +constructor2PatternDec ty idx (NormalC conName argTypes) = do + (npPat, names) <- productPattern (map snd argTypes) + return + ( PatSynSigD patDecName (patternTypeDec (map snd argTypes) ty), + prefixPatternDec idx patDecName names npPat + ) + where + patDecName = mkName (nameBase conName ++ "'") +constructor2PatternDec ty idx (InfixC argType1 conName argType2) = do + let argTypes = [argType1, argType2] + (npPat, names) <- productPattern (map snd argTypes) + case names of + nm1 : nm2 : [] -> + return + ( PatSynSigD patDecName (patternTypeDec (map snd argTypes) ty), + infixPatternDec idx patDecName nm1 nm2 npPat + ) + _ -> fail "The impossible happened: Infix Pattern have more than 2 binders" + where + patDecName = mkName (nameBase conName ++ "%") +constructor2PatternDec _ _ _ = + fail "Test.StrictCheck.TH cannot derive pattern synonyms for fancy types" + +-- | Template Haskell splice to generate pattern synonym declarations for +-- working with explicitly-represented demands on a type whose 'Shape' is +-- implemented generically as a 'GShape' +derivePatternSynonyms :: Name -> Q [Dec] +derivePatternSynonyms name = do + nameInfo <- reify name + case nameInfo of + TyConI (DataD _ tyName tyVars _ constrs _) -> do + let tyVarTypes = + map + ( \tyVar -> case tyVar of + PlainTV nm _ -> VarT nm + KindedTV nm _ kd -> SigT (VarT nm) kd + ) + tyVars + ty = foldl AppT (ConT tyName) tyVarTypes + decs <- mapM (uncurry (constructor2PatternDec ty)) (zip [0 ..] constrs) + return $ (map fst decs) ++ (map snd decs) + _ -> do + reportError (show name ++ " is not a data type name") + return [] diff --git a/tests/RefTrans.hs b/tests/RefTrans.hs --- a/tests/RefTrans.hs +++ b/tests/RefTrans.hs @@ -1,37 +1,37 @@ -{-# LANGUAGE GADTs #-} - -module RefTrans where - -import System.Exit -import System.IO - -import Test.StrictCheck - -notEqualRefTrans :: Eq a => String -> a -> a -> IO Bool -notEqualRefTrans functionName x y = - if x /= y - then return True - else do - putStrLn $ "!!! " ++ functionName ++ " referentially opaque" - return False - -checkRefTrans :: IO () -checkRefTrans = do - let strict = snd (observe1 id (\() -> ()) ()) - let lazy = snd (observe1 id (\_ -> ()) ()) - - observe1_ok <- notEqualRefTrans "observe1" strict lazy - - let strict' = snd (observeNP id (\(I () :* Nil) -> ()) (I () :* Nil)) - let lazy' = snd (observeNP id (\(I _ :* Nil) -> ()) (I () :* Nil)) - - observe_ok <- notEqualRefTrans "observe" strict' lazy' - - let strict'' = snd (observe id (\() -> ()) ()) - let lazy'' = snd (observe id (\_ -> ()) ()) - - observeNP_ok <- notEqualRefTrans "observeNP" strict'' lazy'' - - if and [observe1_ok, observe_ok, observeNP_ok] - then return () - else putStrLn "\n" >> hFlush stdout >> exitFailure +{-# LANGUAGE GADTs #-} + +module RefTrans where + +import System.Exit +import System.IO + +import Test.StrictCheck + +notEqualRefTrans :: Eq a => String -> a -> a -> IO Bool +notEqualRefTrans functionName x y = + if x /= y + then return True + else do + putStrLn $ "!!! " ++ functionName ++ " referentially opaque" + return False + +checkRefTrans :: IO () +checkRefTrans = do + let strict = snd (observe1 id (\() -> ()) ()) + let lazy = snd (observe1 id (\_ -> ()) ()) + + observe1_ok <- notEqualRefTrans "observe1" strict lazy + + let strict' = snd (observeNP id (\(I () :* Nil) -> ()) (I () :* Nil)) + let lazy' = snd (observeNP id (\(I _ :* Nil) -> ()) (I () :* Nil)) + + observe_ok <- notEqualRefTrans "observe" strict' lazy' + + let strict'' = snd (observe id (\() -> ()) ()) + let lazy'' = snd (observe id (\_ -> ()) ()) + + observeNP_ok <- notEqualRefTrans "observeNP" strict'' lazy'' + + if and [observe1_ok, observe_ok, observeNP_ok] + then return () + else putStrLn "\n" >> hFlush stdout >> exitFailure diff --git a/tests/Specs.hs b/tests/Specs.hs --- a/tests/Specs.hs +++ b/tests/Specs.hs @@ -1,38 +1,49 @@ -module Specs where - -import Test.QuickCheck - -import Test.StrictCheck -import Test.StrictCheck.Examples.Lists -import Test.StrictCheck.Examples.Map - -runSpecs :: IO () -runSpecs = do - putStrLn "Checking length_spec..." - strictCheckSpecExact length_spec (length :: [Int] -> Int) - - putStrLn "Checking take_spec..." - strictCheckSpecExact take_spec (take :: Int -> [Int] -> [Int]) - - putStrLn "Checking map_spec..." - strictCheckSpecExact map_spec (map :: (Int -> [Int]) -> [Int] -> [[Int]]) - - putStrLn "Checking rot_spec..." - strictCheckSpecExact rot_spec (rot :: [Int] -> [Int] -> [Int]) - - putStrLn "Checking append_spec..." - strictCheckSpecExact append_spec ((++) :: [Int] -> [Int] -> [Int]) - - putStrLn "Checking reverse_spec..." - strictCheckSpecExact reverse_spec (reverse :: [Int] -> [Int]) - - putStrLn "Checking knapsack..." - strictCheckWithResults - stdArgs{maxSize=100, maxSuccess=500} - shrinkViaArbitrary - genViaProduce - strictnessViaSized - iterSolution_spec - iterSolutionWithKey >>= print - - return () +module Specs where + +import Test.QuickCheck + +import Test.StrictCheck +import Test.StrictCheck.Examples.Lists +import Test.StrictCheck.Examples.Map + +import Control.Monad (when) +import GHC.IO.Encoding (textEncodingName) +import System.IO + +runSpecs :: IO () +runSpecs = do + putStrLn "Checking length_spec..." + strictCheckSpecExact length_spec (length :: [Int] -> Int) + + putStrLn "Checking take_spec..." + strictCheckSpecExact take_spec (take :: Int -> [Int] -> [Int]) + + putStrLn "Checking map_spec..." + strictCheckSpecExact map_spec (map :: (Int -> [Int]) -> [Int] -> [[Int]]) + + putStrLn "Checking rot_spec..." + strictCheckSpecExact rot_spec (rot :: [Int] -> [Int] -> [Int]) + + putStrLn "Checking append_spec..." + strictCheckSpecExact append_spec ((++) :: [Int] -> [Int] -> [Int]) + + putStrLn "Checking reverse_spec..." + strictCheckSpecExact reverse_spec (reverse :: [Int] -> [Int]) + + putStrLn "Checking knapsack..." + strictCheckWithResults + stdArgs{maxSize=100, maxSuccess=500} + shrinkViaArbitrary + genViaProduce + strictnessViaSized + iterSolution_spec + iterSolutionWithKey >>= print + + putStrLn "Checking bad_length_spec (failure is expected!)..." + strictCheckSpecExact bad_length_spec (length :: [Int] -> Int) + + enc <- hGetEncoding stdout + when (fmap textEncodingName enc == Just "UTF-8") $ do + hSetEncoding stdout latin1 + putStrLn "Checking bad_length_spec without Unicode output (failure is expected!)..." + strictCheckSpecExact bad_length_spec (length :: [Int] -> Int) diff --git a/tests/Tests.hs b/tests/Tests.hs --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -1,11 +1,11 @@ -module Main where - -import Specs -import RefTrans - -main :: IO () -main = do - -- specification unit tests - runSpecs - -- regression test for issue #2 (CSE breaks referential transparency) - checkRefTrans +module Main where + +import Specs +import RefTrans + +main :: IO () +main = do + -- specification unit tests + runSpecs + -- regression test for issue #2 (CSE breaks referential transparency) + checkRefTrans