diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/StrictCheck.cabal b/StrictCheck.cabal new file mode 100644 --- /dev/null +++ b/StrictCheck.cabal @@ -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 diff --git a/src/Test/StrictCheck.hs b/src/Test/StrictCheck.hs new file mode 100644 --- /dev/null +++ b/src/Test/StrictCheck.hs @@ -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" + ++ " '[" ++ 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 diff --git a/src/Test/StrictCheck/Consume.hs b/src/Test/StrictCheck/Consume.hs new file mode 100644 --- /dev/null +++ b/src/Test/StrictCheck/Consume.hs @@ -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) diff --git a/src/Test/StrictCheck/Curry.hs b/src/Test/StrictCheck/Curry.hs new file mode 100644 --- /dev/null +++ b/src/Test/StrictCheck/Curry.hs @@ -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) diff --git a/src/Test/StrictCheck/Demand.hs b/src/Test/StrictCheck/Demand.hs new file mode 100644 --- /dev/null +++ b/src/Test/StrictCheck/Demand.hs @@ -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: +-- . +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 diff --git a/src/Test/StrictCheck/Examples/Lists.hs b/src/Test/StrictCheck/Examples/Lists.hs new file mode 100644 --- /dev/null +++ b/src/Test/StrictCheck/Examples/Lists.hs @@ -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 diff --git a/src/Test/StrictCheck/Examples/Map.hs b/src/Test/StrictCheck/Examples/Map.hs new file mode 100644 --- /dev/null +++ b/src/Test/StrictCheck/Examples/Map.hs @@ -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 diff --git a/src/Test/StrictCheck/Internal/Inputs.hs b/src/Test/StrictCheck/Internal/Inputs.hs new file mode 100644 --- /dev/null +++ b/src/Test/StrictCheck/Internal/Inputs.hs @@ -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) diff --git a/src/Test/StrictCheck/Internal/Omega.hs b/src/Test/StrictCheck/Internal/Omega.hs new file mode 100644 --- /dev/null +++ b/src/Test/StrictCheck/Internal/Omega.hs @@ -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' diff --git a/src/Test/StrictCheck/Internal/Shrink.hs b/src/Test/StrictCheck/Internal/Shrink.hs new file mode 100644 --- /dev/null +++ b/src/Test/StrictCheck/Internal/Shrink.hs @@ -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 diff --git a/src/Test/StrictCheck/Internal/Unevaluated.hs b/src/Test/StrictCheck/Internal/Unevaluated.hs new file mode 100644 --- /dev/null +++ b/src/Test/StrictCheck/Internal/Unevaluated.hs @@ -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 diff --git a/src/Test/StrictCheck/Observe.hs b/src/Test/StrictCheck/Observe.hs new file mode 100644 --- /dev/null +++ b/src/Test/StrictCheck/Observe.hs @@ -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)) diff --git a/src/Test/StrictCheck/Observe/Unsafe.hs b/src/Test/StrictCheck/Observe/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/Test/StrictCheck/Observe/Unsafe.hs @@ -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 diff --git a/src/Test/StrictCheck/Produce.hs b/src/Test/StrictCheck/Produce.hs new file mode 100644 --- /dev/null +++ b/src/Test/StrictCheck/Produce.hs @@ -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) + ] diff --git a/src/Test/StrictCheck/Shaped.hs b/src/Test/StrictCheck/Shaped.hs new file mode 100644 --- /dev/null +++ b/src/Test/StrictCheck/Shaped.hs @@ -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 (" :: " ++ 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) diff --git a/src/Test/StrictCheck/Shaped/Flattened.hs b/src/Test/StrictCheck/Shaped/Flattened.hs new file mode 100644 --- /dev/null +++ b/src/Test/StrictCheck/Shaped/Flattened.hs @@ -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) diff --git a/src/Test/StrictCheck/TH.hs b/src/Test/StrictCheck/TH.hs new file mode 100644 --- /dev/null +++ b/src/Test/StrictCheck/TH.hs @@ -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 [] diff --git a/tests/Specs.hs b/tests/Specs.hs new file mode 100644 --- /dev/null +++ b/tests/Specs.hs @@ -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 () diff --git a/tests/Tests.hs b/tests/Tests.hs new file mode 100644 --- /dev/null +++ b/tests/Tests.hs @@ -0,0 +1,6 @@ +module Main where + +import Specs + +main :: IO () +main = runSpecs