StrictCheck (empty) → 0.1.0
raw patch · 22 files changed
+3512/−0 lines, 22 filesdep +HUnitdep +QuickCheckdep +StrictChecksetup-changed
Dependencies added: HUnit, QuickCheck, StrictCheck, base, bifunctors, containers, deepseq, generics-sop, template-haskell
Files
- LICENSE +0/−0
- README.md +0/−0
- Setup.hs +2/−0
- StrictCheck.cabal +80/−0
- src/Test/StrictCheck.hs +517/−0
- src/Test/StrictCheck/Consume.hs +275/−0
- src/Test/StrictCheck/Curry.hs +147/−0
- src/Test/StrictCheck/Demand.hs +303/−0
- src/Test/StrictCheck/Examples/Lists.hs +266/−0
- src/Test/StrictCheck/Examples/Map.hs +198/−0
- src/Test/StrictCheck/Internal/Inputs.hs +59/−0
- src/Test/StrictCheck/Internal/Omega.hs +35/−0
- src/Test/StrictCheck/Internal/Shrink.hs +98/−0
- src/Test/StrictCheck/Internal/Unevaluated.hs +23/−0
- src/Test/StrictCheck/Observe.hs +138/−0
- src/Test/StrictCheck/Observe/Unsafe.hs +76/−0
- src/Test/StrictCheck/Produce.hs +229/−0
- src/Test/StrictCheck/Shaped.hs +876/−0
- src/Test/StrictCheck/Shaped/Flattened.hs +51/−0
- src/Test/StrictCheck/TH.hs +95/−0
- tests/Specs.hs +38/−0
- tests/Tests.hs +6/−0
+ LICENSE view
+ README.md view
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ StrictCheck.cabal view
@@ -0,0 +1,80 @@+name: StrictCheck+version: 0.1.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++library+ hs-source-dirs: src+ default-language: Haskell2010+ build-depends: base >= 4.7 && < 5,+ QuickCheck >= 2.10 && < 2.11,+ containers >= 0.5 && < 0.6,+ generics-sop >= 0.3.2 && < 0.4,+ bifunctors >= 5.5 && < 5.6,+ template-haskell >= 2.12 && < 2.13+ 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+ 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,+ HUnit,+ generics-sop,+ deepseq,+ StrictCheck,+ QuickCheck
+ src/Test/StrictCheck.hs view
@@ -0,0 +1,517 @@+{-| 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+++-- TODO: IMPORTANT: Add short descriptions to Haddock module headers++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> :: 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
+ src/Test/StrictCheck/Consume.hs view
@@ -0,0 +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)
+ src/Test/StrictCheck/Curry.hs view
@@ -0,0 +1,147 @@+{-| 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)
+ src/Test/StrictCheck/Demand.hs view
@@ -0,0 +1,303 @@+{-| 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:+-- <https://stackoverflow.com/questions/27471937/43639618#43639618>.+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+prettyDemand :: Shaped a => Demand a -> String+prettyDemand d =+ showPrettyFieldThunkS False "_" 0 (renderfold d) ""++-- | Print a demand to standard output+--+-- > printDemand = putStrLn . prettyDemand+printDemand :: Shaped a => Demand a -> IO ()+printDemand = putStrLn . prettyDemand++-- 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
+ src/Test/StrictCheck/Examples/Lists.hs view
@@ -0,0 +1,266 @@+{-| 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
+ src/Test/StrictCheck/Examples/Map.hs view
@@ -0,0 +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
+ src/Test/StrictCheck/Internal/Inputs.hs view
@@ -0,0 +1,59 @@+{-| __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)+import Data.Semigroup+++--------------------------------------------------+-- 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)
+ src/Test/StrictCheck/Internal/Omega.hs view
@@ -0,0 +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'
+ src/Test/StrictCheck/Internal/Shrink.hs view
@@ -0,0 +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
+ src/Test/StrictCheck/Internal/Unevaluated.hs view
@@ -0,0 +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
+ src/Test/StrictCheck/Observe.hs view
@@ -0,0 +1,138 @@+{-| 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.+observe1+ :: (Shaped a, Shaped b)+ => (b -> ()) -> (a -> b) -> a -> (Demand b, Demand a)+observe1 context function input =+ let (input', inputD) =+ entangleShape input -- (1)+ (result', resultD) =+ entangleShape (function input') -- (2)+ in let !_ = context result' -- (3)+ in (resultD, inputD) -- (4)++-- | 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.+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 . entangleShape . unI)+ inputs+ (inputs', inputsD) =+ (hliftA (\(Pair r _) -> r) entangled,+ hliftA (\(Pair _ l) -> l) entangled)+ (result', resultD) = entangleShape (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))
+ src/Test/StrictCheck/Observe/Unsafe.hs view
@@ -0,0 +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 entangleShape #-}+entangleShape :: Shaped a => a -> (a, Demand a)+entangleShape =+ first (fuse unI)+ . unzipWith entangle'+ . interleave I+ where+ entangle' :: I x -> (I x, Thunk x)+ entangle' =+ first I . entangle . unI
+ src/Test/StrictCheck/Produce.hs view
@@ -0,0 +1,229 @@+{-| 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)+ ]
+ src/Test/StrictCheck/Shaped.hs view
@@ -0,0 +1,876 @@+{-# 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 ("<function> :: " ++ 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)
+ src/Test/StrictCheck/Shaped/Flattened.hs view
@@ -0,0 +1,51 @@+{-| 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 paramaterized.+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)
+ src/Test/StrictCheck/TH.hs view
@@ -0,0 +1,95 @@+{-| 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 []
+ tests/Specs.hs view
@@ -0,0 +1,38 @@+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 ()
+ tests/Tests.hs view
@@ -0,0 +1,6 @@+module Main where++import Specs++main :: IO ()+main = runSpecs