StrictCheck 0.3.0 → 0.4.0

raw patch · 24 files changed

+3742/−3610 lines, 24 filesdep −HUnitdep −deepseqdep ~QuickCheckdep ~bifunctorsdep ~containerssetup-changednew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies removed: HUnit, deepseq

Dependency ranges changed: QuickCheck, bifunctors, containers, generics-sop, template-haskell

API changes (from Hackage documentation)

Files

• CHANGELOG.md +41/−0
• LICENSE +21/−21
• README.md +12/−10
• Setup.hs +2/−2
• StrictCheck.cabal +84/−86
• src/Test/StrictCheck.hs +572/−514
• src/Test/StrictCheck/Consume.hs +275/−275
• src/Test/StrictCheck/Curry.hs +148/−147
• src/Test/StrictCheck/Demand.hs +310/−310
• src/Test/StrictCheck/Examples/Lists.hs +272/−266
• src/Test/StrictCheck/Examples/Map.hs +198/−198
• src/Test/StrictCheck/Internal/Inputs.hs +58/−58
• src/Test/StrictCheck/Internal/Omega.hs +35/−35
• src/Test/StrictCheck/Internal/Shrink.hs +98/−98
• src/Test/StrictCheck/Internal/Unevaluated.hs +23/−23
• src/Test/StrictCheck/Observe.hs +148/−148
• src/Test/StrictCheck/Observe/Unsafe.hs +76/−76
• src/Test/StrictCheck/Produce.hs +231/−229
• src/Test/StrictCheck/Shaped.hs +875/−876
• src/Test/StrictCheck/Shaped/Flattened.hs +57/−57
• src/Test/StrictCheck/TH.hs +109/−95
• tests/RefTrans.hs +37/−37
• tests/Specs.hs +49/−38
• tests/Tests.hs +11/−11

@@ -0,0 +1,41 @@+# Releases
+
+All notable changes to this project will be documented in this file.
+
+The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
+and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/).
+
+## [0.4.0] - 2025-08-30
+
+- Compatibility with GHC 9.2 - 9.12
+- Add `Shaped` and `Produce` instances for `NonEmpty`
+- Fix output for non-Unicode locales
+
+## [0.3.0] - 2019-11-01
+
+- Add `Show` instance for `Demand`
+
+## [0.2.0] - 2018-10-08
+
+### Added
+
+- Expose instrumentation of data structures as a safe interface in the `IO` monad.
+- Add monadic folds and unfolds `translateA`, `foldM`, `unfoldM`, and `unzipWithM` to `Test.StrictCheck.Shaped`.
+
+### Removed
+
+- Remove the referentially opaque observation primitives in `Test.StrictCheck.Unsafe`.
+
+### Changed
+
+- Improve type inference by making `Shape` an injective type family.
+
+## [0.1.1] - 2018-10-01
+
+### Fixed
+
+- Fix critical semantic [bug #2](https://github.com/kwf/StrictCheck/issues/2) which caused violation of referential transparency when compiling with optimizations on GHC 8.6.
+
+## [0.1.0] - 2018-06-22
+
+First release of StrictCheck. This version matches the reviewed artifact submitted to ICFP, archived on the ACM DL, with the exception of some small documentation tweaks.

@@ -1,21 +1,21 @@-MIT License--Copyright (c) 2018 Kenneth Foner, Hengchu Zhang, and Leonidas Lampropoulos--Permission is hereby granted, free of charge, to any person obtaining a copy-of this software and associated documentation files (the "Software"), to deal-in the Software without restriction, including without limitation the rights-to use, copy, modify, merge, publish, distribute, sublicense, and/or sell-copies of the Software, and to permit persons to whom the Software is-furnished to do so, subject to the following conditions:--The above copyright notice and this permission notice shall be included in all-copies or substantial portions of the Software.--THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR-IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,-FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE-AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER-LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,-OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE-SOFTWARE.+MIT License
+
+Copyright (c) 2018 Kenneth Foner, Hengchu Zhang, and Leonidas Lampropoulos
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

@@ -1,10 +1,12 @@-  # StrictCheck: Keep Your Laziness In Check-  -  StrictCheck is a property-based random testing framework for-  observing, specifying, and testing the strictness behaviors of Haskell-  functions. Strictness behavior is traditionally considered a non-functional-  property; StrictCheck allows it to be tested as if it were one, by reifying-  demands on data structures so they can be manipulated and examined within-  Haskell.-  -  For details, see the library on Hackage: <https://hackage.haskell.org/package/StrictCheck>.+# StrictCheck: Keep Your Laziness In Check
+  
+[![Hackage](https://img.shields.io/hackage/v/StrictCheck.svg)](https://hackage.haskell.org/package/StrictCheck)
+
+StrictCheck is a property-based random testing framework for
+observing, specifying, and testing the strictness behaviors of Haskell
+functions. Strictness behavior is traditionally considered a non-functional
+property; StrictCheck allows it to be tested as if it were one, by reifying
+demands on data structures so they can be manipulated and examined within
+Haskell.
+
+For details, see the library on Hackage: <https://hackage.haskell.org/package/StrictCheck>.

@@ -1,2 +1,2 @@-import Distribution.Simple-main = defaultMain+import Distribution.Simple
+main = defaultMain

@@ -1,86 +1,84 @@-name:                StrictCheck-version:             0.3.0-synopsis:            StrictCheck: Keep Your Laziness In Check-description: StrictCheck is a property-based random testing framework for-             observing, specifying, and testing the strictness behaviors of Haskell-             functions. Strictness behavior is traditionally considered a non-functional-             property; StrictCheck allows it to be tested as if it were one, by reifying-             demands on data structures so they can be manipulated and examined within-             Haskell.-homepage:            https://github.com/kwf/StrictCheck#readme-license:             MIT-license-file:        LICENSE-author:              Kenneth Foner, Hengchu Zhang, and Leo Lampropoulos-maintainer:          kwf@very.science-copyright:           (c) 2018 Kenneth Foner, Hengchu Zhang, and Leo Lampropoulos-category:            Testing-build-type:          Simple-cabal-version:       >=1.10-extra-source-files:  README.md--source-repository this-  type: git-  branch: master-  tag: master-  location: https://github.com/kwf/StrictCheck--library-  hs-source-dirs:      src-  default-language:    Haskell2010-  build-depends:       base             >= 4.7   && < 5,-                       QuickCheck       >= 2.10  && < 2.12,-                       containers       >= 0.5   && < 0.7,-                       generics-sop     >= 0.3.2 && < 0.4,-                       bifunctors       >= 5.5   && < 5.6,-                       template-haskell >= 2.12  && < 2.15-  exposed-modules:     Test.StrictCheck-                       Test.StrictCheck.Curry,-                       Test.StrictCheck.Consume,-                       Test.StrictCheck.Produce,-                       Test.StrictCheck.Demand,-                       Test.StrictCheck.Observe,-                       Test.StrictCheck.Observe.Unsafe,-                       Test.StrictCheck.Shaped,-                       Test.StrictCheck.Shaped.Flattened,-                       Test.StrictCheck.Internal.Inputs,-                       Test.StrictCheck.Internal.Unevaluated,-                       Test.StrictCheck.Internal.Shrink,-                       Test.StrictCheck.Internal.Omega,-                       Test.StrictCheck.TH,-                       Test.StrictCheck.Examples.Lists,-                       Test.StrictCheck.Examples.Map-  default-extensions:  DataKinds, GADTs, BangPatterns, TypeFamilies, RankNTypes,-                       AllowAmbiguousTypes, DefaultSignatures, TypeApplications,-                       ScopedTypeVariables, FlexibleContexts,-                       UndecidableInstances, ConstraintKinds, DeriveFunctor,-                       FlexibleInstances, StandaloneDeriving, DeriveGeneric,-                       DeriveAnyClass, TypeOperators, PolyKinds,-                       GeneralizedNewtypeDeriving,-                       ViewPatterns, LambdaCase, TupleSections, ImplicitParams,-                       NamedFieldPuns, PatternSynonyms-  ghc-options:         -Wall -Wno-unticked-promoted-constructors-                       -Wredundant-constraints--test-suite test-strictcheck-  type:                 exitcode-stdio-1.0-  hs-source-dirs:       tests-  main-is:              Tests.hs-  other-modules:        Specs, RefTrans-  default-language:     Haskell2010-  default-extensions:   DataKinds, GADTs, BangPatterns, TypeFamilies, RankNTypes,-                        AllowAmbiguousTypes, UndecidableInstances,-                        DefaultSignatures, TypeApplications, ScopedTypeVariables,-                        FlexibleContexts, ConstraintKinds, DeriveFunctor,-                        FlexibleInstances, StandaloneDeriving, DeriveGeneric,-                        DeriveAnyClass, TypeOperators, PolyKinds, LambdaCase,-                        TupleSections, TypeFamilyDependencies,-                        MultiParamTypeClasses,-                        GeneralizedNewtypeDeriving, ViewPatterns,-                        PatternSynonyms-  ghc-options:         -Wall -fno-warn-unused-imports -O2-  build-depends:        base,-                        HUnit,-                        generics-sop,-                        deepseq,-                        StrictCheck,-                        QuickCheck+name:                StrictCheck
+version:             0.4.0
+synopsis:            StrictCheck: Keep Your Laziness In Check
+description: StrictCheck is a property-based random testing framework for
+             observing, specifying, and testing the strictness behaviors of Haskell
+             functions. Strictness behavior is traditionally considered a non-functional
+             property; StrictCheck allows it to be tested as if it were one, by reifying
+             demands on data structures so they can be manipulated and examined within
+             Haskell.
+homepage:            https://github.com/kwf/StrictCheck#readme
+license:             MIT
+license-file:        LICENSE
+author:              Kenneth Foner, Hengchu Zhang, and Leo Lampropoulos
+maintainer:          lysxia@gmail.com
+copyright:           (c) 2018 Kenneth Foner, Hengchu Zhang, and Leo Lampropoulos
+category:            Testing
+build-type:          Simple
+cabal-version:       2.0
+extra-doc-files:     README.md, CHANGELOG.md
+tested-with:         GHC == 9.12.2, GHC == 9.6.7, GHC == 9.2.8
+
+source-repository this
+  type: git
+  branch: master
+  tag: master
+  location: https://github.com/kwf/StrictCheck
+
+library
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+  build-depends:       base             >= 4.7   && < 5,
+                       template-haskell >= 2.18  && < 2.24,
+                       QuickCheck       >= 2.10  && < 2.17,
+                       containers       >= 0.5   && < 0.9,
+                       generics-sop     >= 0.3.2 && < 0.6,
+                       bifunctors       >= 5.5   && < 5.7
+  exposed-modules:     Test.StrictCheck
+                       Test.StrictCheck.Curry,
+                       Test.StrictCheck.Consume,
+                       Test.StrictCheck.Produce,
+                       Test.StrictCheck.Demand,
+                       Test.StrictCheck.Observe,
+                       Test.StrictCheck.Observe.Unsafe,
+                       Test.StrictCheck.Shaped,
+                       Test.StrictCheck.Shaped.Flattened,
+                       Test.StrictCheck.Internal.Inputs,
+                       Test.StrictCheck.Internal.Unevaluated,
+                       Test.StrictCheck.Internal.Shrink,
+                       Test.StrictCheck.Internal.Omega,
+                       Test.StrictCheck.TH,
+                       Test.StrictCheck.Examples.Lists,
+                       Test.StrictCheck.Examples.Map
+  default-extensions:  DataKinds, GADTs, BangPatterns, TypeFamilies, RankNTypes,
+                       AllowAmbiguousTypes, DefaultSignatures, TypeApplications,
+                       ScopedTypeVariables, FlexibleContexts,
+                       UndecidableInstances, ConstraintKinds, DeriveFunctor,
+                       FlexibleInstances, StandaloneDeriving, DeriveGeneric,
+                       DeriveAnyClass, TypeOperators, PolyKinds,
+                       GeneralizedNewtypeDeriving,
+                       ViewPatterns, LambdaCase, TupleSections, ImplicitParams,
+                       NamedFieldPuns, PatternSynonyms
+  ghc-options:         -Wall -Wno-unticked-promoted-constructors
+                       -Wredundant-constraints
+
+test-suite test-strictcheck
+  type:                 exitcode-stdio-1.0
+  hs-source-dirs:       tests
+  main-is:              Tests.hs
+  other-modules:        Specs, RefTrans
+  default-language:     Haskell2010
+  default-extensions:   DataKinds, GADTs, BangPatterns, TypeFamilies, RankNTypes,
+                        AllowAmbiguousTypes, UndecidableInstances,
+                        DefaultSignatures, TypeApplications, ScopedTypeVariables,
+                        FlexibleContexts, ConstraintKinds, DeriveFunctor,
+                        FlexibleInstances, StandaloneDeriving, DeriveGeneric,
+                        DeriveAnyClass, TypeOperators, PolyKinds, LambdaCase,
+                        TupleSections, TypeFamilyDependencies,
+                        MultiParamTypeClasses,
+                        GeneralizedNewtypeDeriving, ViewPatterns,
+                        PatternSynonyms
+  ghc-options:         -Wall -fno-warn-unused-imports
+  build-depends:        base,
+                        StrictCheck,
+                        QuickCheck

@@ -1,514 +1,572 @@-{-| The top-level interface to the StrictCheck library for random strictness-    testing.--    __Quick Start:__--    Want to explore the strictness of functions before you write specifications?-    Go to "Test.StrictCheck.Observe" and look at the functions 'observe1' and-    'observe'.--    Want to check the strictness of a function against a specification of its-    strictness?--    1. Write a 'Spec' describing your expectation of the function's behavior.-       See "Test.StrictCheck.Demand" for more on working with demands, and-       "Test.StrictCheck.Examples.Lists" for examples of some specifications of-       functions on lists.-    2. Check your function using 'strictCheckSpecExact', like so:--    > strictCheckSpecExact spec function--    If your function passes testing, you'll get a success message just like in-    "Test.QuickCheck"; if a counterexample to your specification is found, you-    will see a pretty Unicode box diagram describing the mismatch.--    __Hint:__ StrictCheck, just like QuickCheck, doesn't work with polymorphic-    functions. If you get baffling type errors, first make sure that all your-    types are totally concrete.--}--{-# language DerivingStrategies #-}--module Test.StrictCheck-  ( -- * Specifying demand behavior-    Spec(..)-  , getSpec-  -- * Checking specifications-  , StrictCheck-  , strictCheckSpecExact-  , strictCheckWithResults-  -- * Providing arguments for 'strictCheckWithResults'-  , genViaProduce-  , Shrink(..)-  , shrinkViaArbitrary-  , Strictness-  , strictnessViaSized-  -- * Representing individual evaluations of functions-  , Evaluation(..)-  , evaluationForall-  , shrinkEvalWith-  -- * Comparing demands-  , DemandComparison(..)-  , compareToSpecWith-  , equalToSpec-    -- * Re-exported n-ary products from "Generics.SOP"-  , NP(..), I(..), All-  -- * Re-exports of the rest of the library-  , module Test.StrictCheck.Demand-  , module Test.StrictCheck.Observe-  , module Test.StrictCheck.Produce-  , module Test.StrictCheck.Consume-  , module Test.StrictCheck.Shaped-  )-  where--import Test.StrictCheck.Curry as Curry-import Test.StrictCheck.Produce-import Test.StrictCheck.Consume-import Test.StrictCheck.Observe-import Test.StrictCheck.Demand-import Test.StrictCheck.Shaped--import Test.StrictCheck.Internal.Omega-import Test.StrictCheck.Internal.Shrink-         ( Shrink(..), axialShrinks, fairInterleave )--import Generics.SOP hiding (Shape)--import Test.QuickCheck as Exported hiding (Args, Result, function)-import qualified Test.QuickCheck as QC--import Data.List-import Data.Maybe-import Data.IORef-import Type.Reflection---- | The default comparison of demands: exact equality-compareEquality :: All Shaped xs => NP DemandComparison xs-compareEquality = hcpure (Proxy @Shaped) (DemandComparison (==))---- | The default way to generate inputs: via 'Produce'-genViaProduce :: All Produce xs => NP Gen xs-genViaProduce = hcpure (Proxy @Produce) (freely produce)---- | The default way to shrink inputs: via 'shrink' (from "Test.QuickCheck"'s--- 'Arbitrary' typeclass)-shrinkViaArbitrary :: All Arbitrary xs => NP Shrink xs-shrinkViaArbitrary = hcpure (Proxy @Arbitrary) (Shrink shrink)---- | The default way to generate random strictnesses: uniformly choose between--- 1 and the test configuration's @size@ parameter-strictnessViaSized :: Gen Strictness-strictnessViaSized =-  Strictness <$> (choose . (1,) =<< getSize)---- | A newtype for wrapping a comparison on demands------ This is useful when constructing an 'NP' n-ary product of such comparisons.-newtype DemandComparison a =-  DemandComparison (Demand a -> Demand a -> Bool)---- | A demand specification for some function @f@ is itself a function which--- manipulates demand values for some function's arguments and results------ A @Spec@ for @f@ wraps a function which takes, in order:------ * a continuation @predict@ which accepts all of @f@'s argument types in order,--- * an implicit representation of a demand on @f@'s result (embedded in @f@'s---   actual result type using special bottom values, see the documentation for---   "Test.StrictCheck.Demand" for details), and--- * all of @f@'s original arguments in order------ The intention is that the @Spec@ will call @predict@ on some set of demands--- representing the demands it predicts that @f@ will exert on its inputs,--- given the provided demand on @f@'s outputs.------ For example, here is a correct @Spec@ for 'take':------ > take_spec :: Spec '[Int, [a]] [a]--- > take_spec =--- >  Spec $ \predict d n xs ->--- >    predict n (if n > length xs then d else d ++ thunk)------ See the documentation for "Test.StrictCheck.Demand" for information about how--- to manipulate these implicit demand representations when writing @Spec@s, and--- see the documentation for "Test.StrictCheck.Examples.Lists" for more examples--- of writing specifications.-newtype Spec (args :: [*]) (result :: *)-  = Spec (forall r. (args ⋯-> r) -> result -> args ⋯-> r)---- | Unwrap a @Spec@ constructor, returning the contained CPS-ed specification------ Conceptually, this is the inverse to the @Spec@ constructor, but because--- @Spec@ is variadic, @getSpec . Spec@ and @Spec . getSpec@ don't typecheck--- without additional type annotation.-getSpec-  :: forall r args result.-  Spec args result-  -> (args ⋯-> r)-  -> result-  -> args ⋯-> r-getSpec (Spec s) k d = s @r k d---- | Given a list of ways to compare demands, a demand specification, and an--- evaluation of a particular function, determine if the function met the--- specification, as decided by the comparisons. If so, return the prediction--- of the specification.-compareToSpecWith-  :: forall args result.-  (All Shaped args, Curry args, Shaped result)-  => NP DemandComparison args-  -> Spec args result-  -> Evaluation args result-  -> Maybe (NP Demand args)-compareToSpecWith comparisons spec (Evaluation inputs inputsD resultD) =-  let prediction =-        Curry.uncurry-          (getSpec @(NP Demand args)-             spec-             collectDemands-             (fromDemand $ E resultD))-          inputs-      correct =-        all id . hcollapse $-          hcliftA3 (Proxy @Shaped)-          (\(DemandComparison c) iD iD' -> K $ iD `c` iD')-            comparisons-            inputsD-            prediction-  in if correct then Nothing else Just prediction-  where-    collectDemands :: args ⋯-> NP Demand args-    collectDemands =-      curryCollect @args (hcmap (Proxy @Shaped) (toDemand . unI))--curryCollect-  :: forall (xs :: [*]) r. Curry xs => (NP I xs -> r) -> xs ⋯-> r-curryCollect k = Curry.curry @xs k---- | Checks if a given 'Evaluation' exactly matches the prediction of a given--- 'Spec', returning the prediction of that @Spec@ if not------ __Note:__ In the case of __success__ this returns @Nothing@; in the case of--- __failure__ this returns @Just@ the incorrect prediction.-equalToSpec-  :: forall args result.-  (All Shaped args, Shaped result, Curry args)-  => Spec args result-  -> Evaluation args result-  -> Maybe (NP Demand args)-equalToSpec spec e =-  compareToSpecWith compareEquality spec e---- | A @Strictness@ represents (roughly) how strict a randomly generated--- function or evaluation context should be------ An evaluation context generated with some strictness @s@ (i.e. through--- 'evaluationForall') will consume at most @s@ constructors of its input,--- although it might consume fewer.-newtype Strictness-  = Strictness Int-  deriving stock (Eq, Ord)-  deriving newtype (Show, Num)---- | A function can be checked against a specification if it meets the--- @StrictCheck@ constraint-type StrictCheck function =-  ( Shaped (Result function)-  , Consume (Result function)-  , Curry (Args function)-  , All Typeable (Args function)-  , All Shaped (Args function) )---- | The most general function for random strictness testing: all of the more--- convenient such functions can be derived from this one------ Given some function @f@, this takes as arguments:------ * A 'QC.Args' record describing arguments to pass to the underlying---   QuickCheck engine--- * An 'NP' n-ary product of 'Shrink' shrinkers, one for each argument of @f@--- * An 'NP' n-ary product of 'Gen' generators, one for each argument of @f@--- * A 'Gen' generator for strictnesses to be tested--- * A predicate on 'Evaluation's: if the 'Evaluation' passes the predicate,---   it should return @Nothing@; otherwise, it should return @Just@ some---   @evidence@ representing the failure (when checking 'Spec's, this evidence---   comes in the form of a @Spec@'s (incorrect) prediction)--- * the function @f@ to be tested------ If all tests succeed, @(Nothing, result)@ is returned, where @result@ is the--- underlying 'QC.Result' type from "Test.QuickCheck". If there is a test--- failure, it also returns @Just@ the failed 'Evaluation' as well as whatever--- @evidence@ was produced by the predicate.-strictCheckWithResults ::-  forall function evidence.-  StrictCheck function-  => QC.Args-  -> NP Shrink (Args function)  -- TODO: allow dependent shrinking-  -> NP Gen (Args function)     -- TODO: allow dependent generation-  -> Gen Strictness-  -> (Evaluation (Args function) (Result function) -> Maybe evidence)-  -> function-  -> IO ( Maybe ( Evaluation (Args function) (Result function)-                , evidence )-        , QC.Result )-strictCheckWithResults-  qcArgs shrinks gens strictness predicate function = do-    ref <- newIORef Nothing-    result <--      quickCheckWithResult qcArgs{chatty = False{-, maxSuccess = 10000-}} $-        forAllShrink-          (evaluationForall @function gens strictness function)-          (shrinkEvalWith @function shrinks function) $-            \example ->-              case predicate example of-                Nothing ->-                  property True-                Just evidence ->-                  whenFail (writeIORef ref $ Just (example, evidence)) False-    readIORef ref >>= \case-      Nothing      -> pure (Nothing,      result)-      Just example -> pure (Just example, result)---- | Check a function to see whether it exactly meets a strictness specification------ If the function fails to meet the specification, a counterexample is--- pretty-printed in a box-drawn diagram illustrating how the specification--- failed to match the real observed behavior of the function.-strictCheckSpecExact-  :: forall function.-  ( StrictCheck function-  , All Arbitrary (Args function)-  , All Produce (Args function)-  ) => Spec (Args function) (Result function)-    -> function-    -> IO ()-strictCheckSpecExact spec function =-  do (maybeExample, result) <--       strictCheckWithResults-         stdArgs-         shrinkViaArbitrary-         genViaProduce-         strictnessViaSized-         (equalToSpec spec)-         function-     (putStrLn . head . lines) (output result)-     case maybeExample of-       Nothing -> return ()-       Just example ->-         putStrLn (Prelude.uncurry displayCounterSpec example)----------------------------------------------------------------- An Evaluation is what we generate when StrictCheck-ing ------------------------------------------------------------------- | A snapshot of the observed strictness behavior of a function------ An @Evaluation@ contains the 'inputs' at which a function was called, the--- 'inputDemands' which were induced upon those inputs, and the 'resultDemand'--- which induced that demand on the inputs.-data Evaluation args result =-  Evaluation-    { inputs       :: NP I      args    -- ^ Inputs to a function-    , inputDemands :: NP Demand args    -- ^ Demands on the input-    , resultDemand :: PosDemand result  -- ^ Demand on the result-    }--instance (All Typeable args, Typeable result)-  => Show (Evaluation args result) where-  show _ =-    "<Evaluation> :: Evaluation"-    ++ " '[" ++ intercalate ", " argTypes ++ "]"-    ++ " " ++ show (typeRep :: TypeRep result)-    where-      argTypes :: [String]-      argTypes =-        hcollapse-        $ hliftA (K . show)-        $ (hcpure (Proxy @Typeable) typeRep :: NP TypeRep args)----------------------------------------- Generating random evaluations ------------------------------------------ | Given a list of generators for a function's arguments and a generator for--- random strictnesses (measured in number of constructors evaluated), create--- a generator for random 'Evaluation's of that function in random contexts-evaluationForall-  :: forall f.-  ( Curry (Args f)-  , Consume (Result f)-  , Shaped (Result f)-  , All Shaped (Args f)-  ) => NP Gen (Args f)-    -> Gen Strictness-    -> f-    -> Gen (Evaluation (Args f) (Result f))-evaluationForall gens strictnessGen function = do-  inputs     <- hsequence gens-  strictness <- strictnessGen-  toOmega    <- freely produce-  return (go strictness toOmega inputs)-  where-    -- If context is fully lazy, increase strictness until it forces something-    go :: Strictness-       -> (Result f -> Omega)-       -> NP I (Args f)-       -> Evaluation (Args f) (Result f)-    go (Strictness s) tO is =-      let (resultD, inputsD) =-            observeNP (forceOmega s . tO) (uncurryAll @f function) is-      in case resultD of-        T -> go (Strictness s + 1) tO is-        E posResultD ->-          Evaluation is inputsD posResultD--------------------------------- Shrinking evaluations ---------------------------------- | Given a shrinker for each of the arguments of a function, the function--- itself, and some 'Evaluation' of that function, produce a list of smaller--- @Evaluation@s of that function-shrinkEvalWith-  :: forall f.-  ( Curry (Args f)-  , Shaped (Result f)-  , All Shaped (Args f)-  ) => NP Shrink (Args f)-    -> f-    -> Evaluation (Args f) (Result f)-    -> [Evaluation (Args f) (Result f)]-shrinkEvalWith-  shrinks (uncurryAll -> function) (Evaluation inputs _ resultD) =-    let shrunkDemands   = shrinkDemand @(Result f) resultD-        shrunkInputs    = fairInterleave (axialShrinks shrinks inputs)-        shrinkingDemand = mapMaybe      (reObserve inputs)  shrunkDemands-        shrinkingInputs = mapMaybe (flip reObserve resultD) shrunkInputs-    in fairInterleave [ shrinkingDemand, shrinkingInputs ]-  where-    reObserve-      :: NP I (Args f)-      -> PosDemand (Result f)-      -> Maybe (Evaluation (Args f) (Result f))-    reObserve is rD =-      let (rD', isD) = observeNP (evaluateDemand rD) function is-      in fmap (Evaluation is isD) $-           case rD' of-             T     -> Nothing-             E pos -> Just pos----- | Render a counter-example to a specification (that is, an 'Evaluation'--- paired with some expected input demands it doesn't match) as a Unicode--- box-drawing sketch-displayCounterSpec-  :: forall args result.-  (Shaped result, All Shaped args)-  => Evaluation args result-  -> NP Demand args-  -> String-displayCounterSpec (Evaluation inputs inputsD resultD) predictedInputsD =-  beside inputBox ("   " : "───" : repeat "   ") resultBox-  ++ (flip replicate ' ' $-       (2 `max` (subtract 2 $ (lineMax [inputString] `div` 2))))-  ++ "🡓 🡓 🡓\n"-  ++ beside-       actualBox-       ("       " : "       " : "  ═╱═  " : repeat "       ")-       predictedBox-  where-    inputBox =-      box "┌" '─'         "┐"-          "│" inputHeader "├"-          "├" '─'         "┤"-          "│" inputString "│"-          "└" '─'         "┘"--    resultBox =-      box "┌" '─'          "┐"-          "┤" resultHeader "│"-          "├" '─'          "┤"-          "│" resultString "│"-          "└" '─'          "┘"--    actualBox =-      box "┌" '─'                "┐"-          "│" actualHeader       "│"-          "├" '─'                "┤"-          "│" actualDemandString "│"-          "└" '─'                "┘"--    predictedBox =-      box "┌" '─'                   "┐"-          "│" predictedHeader       "│"-          "├" '─'                   "┤"-          "│" predictedDemandString "│"-          "└" '─'                   "┘"--    inputHeader = " Input" ++ plural-    resultHeader = " Demand on result"-    actualHeader = " Actual input demand" ++ plural-    predictedHeader = " Spec's input demand" ++ plural--    inputString =-      showBulletedNPWith @Shaped (prettyDemand . interleave Eval . unI) inputs-    resultString = " " ++ prettyDemand @result (E resultD)-    actualDemandString =-      showBulletedNPWith @Shaped prettyDemand inputsD-    predictedDemandString =-      showBulletedNPWith @Shaped prettyDemand predictedInputsD--    rule w l c r = frame w l (replicate w c) r ++ "\n"--    frame w before str after =-      before ++ str-      ++ (replicate (w - length str) ' ')-      ++ after--    frames w before para after =-      unlines $ map (\str -> frame w before str after) (lines para)--    beside l cs r =-      unlines . take (length ls `max` length rs) $-        zipWith3-          (\x c y -> x ++ c ++ y)-          (ls ++ repeat (replicate (lineMax [l]) ' '))-          cs-          (rs ++ repeat "")-      where-        ls = lines l-        rs = lines r--    box top_l    top    top_r-        header_l header header_r-        div_l    div_c  div_r-        body_l   body   body_r-        bottom_l bottom bottom_r =-      let w = lineMax [header, body]-      in rule   w top_l    top    top_r-      ++ frames w header_l header header_r-      ++ rule   w div_l    div_c  div_r-      ++ frames w body_l   body   body_r-      ++ rule   w bottom_l bottom bottom_r--    lineMax strs =-      (maximum . map-        (\(lines -> ls) -> maximum (map length ls) + 1) $ strs)--    plural = case inputs of-      (_ :* Nil) -> ""-      _          -> "s"--    showBulletedNPWith-      :: forall c g xs. All c xs-      => (forall x. c x => g x -> String) -> NP g xs -> String-    -- showBulletedNPWith display (x :* Nil) = " " ++ display x ++ "\n"-    showBulletedNPWith display list = showNPWith' list-      where-        showNPWith' :: forall ys. All c ys => NP g ys -> String-        showNPWith'      Nil = ""-        showNPWith' (y :* ys) =-          " • " ++ display y ++ "\n" ++ showNPWith' ys+{-| The top-level interface to the StrictCheck library for random strictness
+    testing.
+
+    __Quick Start:__
+
+    Want to explore the strictness of functions before you write specifications?
+    Go to "Test.StrictCheck.Observe" and look at the functions 'observe1' and
+    'observe'.
+
+    Want to check the strictness of a function against a specification of its
+    strictness?
+
+    1. Write a 'Spec' describing your expectation of the function's behavior.
+       See "Test.StrictCheck.Demand" for more on working with demands, and
+       "Test.StrictCheck.Examples.Lists" for examples of some specifications of
+       functions on lists.
+    2. Check your function using 'strictCheckSpecExact', like so:
+
+    > strictCheckSpecExact spec function
+
+    If your function passes testing, you'll get a success message just like in
+    "Test.QuickCheck"; if a counterexample to your specification is found, you
+    will see a pretty Unicode box diagram describing the mismatch.
+
+    __Hint:__ StrictCheck, just like QuickCheck, doesn't work with polymorphic
+    functions. If you get baffling type errors, first make sure that all your
+    types are totally concrete.
+-}
+
+{-# language DerivingStrategies #-}
+
+module Test.StrictCheck
+  ( -- * Specifying demand behavior
+    Spec(..)
+  , getSpec
+  -- * Checking specifications
+  , StrictCheck
+  , strictCheckSpecExact
+  , strictCheckWithResults
+  -- * Providing arguments for 'strictCheckWithResults'
+  , genViaProduce
+  , Shrink(..)
+  , shrinkViaArbitrary
+  , Strictness
+  , strictnessViaSized
+  -- * Representing individual evaluations of functions
+  , Evaluation(..)
+  , evaluationForall
+  , shrinkEvalWith
+  -- * Comparing demands
+  , DemandComparison(..)
+  , compareToSpecWith
+  , equalToSpec
+    -- * Re-exported n-ary products from "Generics.SOP"
+  , NP(..), I(..), All
+  -- * Re-exports of the rest of the library
+  , module Test.StrictCheck.Demand
+  , module Test.StrictCheck.Observe
+  , module Test.StrictCheck.Produce
+  , module Test.StrictCheck.Consume
+  , module Test.StrictCheck.Shaped
+  )
+  where
+
+import Test.StrictCheck.Curry as Curry
+import Test.StrictCheck.Produce
+import Test.StrictCheck.Consume
+import Test.StrictCheck.Observe
+import Test.StrictCheck.Demand
+import Test.StrictCheck.Shaped
+
+import Test.StrictCheck.Internal.Omega
+import Test.StrictCheck.Internal.Shrink
+         ( Shrink(..), axialShrinks, fairInterleave )
+
+import Generics.SOP hiding (Shape)
+
+import Test.QuickCheck as Exported hiding (Args, Result, function)
+import qualified Test.QuickCheck as QC
+
+import Data.Char (ord)
+import Data.Function (on)
+import Data.Kind (Type)
+import Data.List
+import Data.Maybe
+import Data.IORef
+import GHC.IO.Encoding (textEncodingName)
+import qualified System.IO as IO
+import Type.Reflection
+
+-- | The default comparison of demands: exact equality
+compareEquality :: All Shaped xs => NP DemandComparison xs
+compareEquality = hcpure (Proxy @Shaped) (DemandComparison (==))
+
+-- | The default way to generate inputs: via 'Produce'
+genViaProduce :: All Produce xs => NP Gen xs
+genViaProduce = hcpure (Proxy @Produce) (freely produce)
+
+-- | The default way to shrink inputs: via 'shrink' (from "Test.QuickCheck"'s
+-- 'Arbitrary' typeclass)
+shrinkViaArbitrary :: All Arbitrary xs => NP Shrink xs
+shrinkViaArbitrary = hcpure (Proxy @Arbitrary) (Shrink shrink)
+
+-- | The default way to generate random strictnesses: uniformly choose between
+-- 1 and the test configuration's @size@ parameter
+strictnessViaSized :: Gen Strictness
+strictnessViaSized =
+  Strictness <$> (choose . (1,) =<< getSize)
+
+-- | A newtype for wrapping a comparison on demands
+--
+-- This is useful when constructing an 'NP' n-ary product of such comparisons.
+newtype DemandComparison a =
+  DemandComparison (Demand a -> Demand a -> Bool)
+
+-- | A demand specification for some function @f@ is itself a function which
+-- manipulates demand values for some function's arguments and results
+--
+-- A @Spec@ for @f@ wraps a function which takes, in order:
+--
+-- * a continuation @predict@ which accepts all of @f@'s argument types in order,
+-- * an implicit representation of a demand on @f@'s result (embedded in @f@'s
+--   actual result type using special bottom values, see the documentation for
+--   "Test.StrictCheck.Demand" for details), and
+-- * all of @f@'s original arguments in order
+--
+-- The intention is that the @Spec@ will call @predict@ on some set of demands
+-- representing the demands it predicts that @f@ will exert on its inputs,
+-- given the provided demand on @f@'s outputs.
+--
+-- For example, here is a correct @Spec@ for 'take':
+--
+-- > take_spec :: Spec '[Int, [a]] [a]
+-- > take_spec =
+-- >  Spec $ \predict d n xs ->
+-- >    predict n (if n > length xs then d else d ++ thunk)
+--
+-- See the documentation for "Test.StrictCheck.Demand" for information about how
+-- to manipulate these implicit demand representations when writing @Spec@s, and
+-- see the documentation for "Test.StrictCheck.Examples.Lists" for more examples
+-- of writing specifications.
+newtype Spec (args :: [Type]) (result :: Type)
+  = Spec (forall r. (args ⋯-> r) -> result -> args ⋯-> r)
+
+-- | Unwrap a @Spec@ constructor, returning the contained CPS-ed specification
+--
+-- Conceptually, this is the inverse to the @Spec@ constructor, but because
+-- @Spec@ is variadic, @getSpec . Spec@ and @Spec . getSpec@ don't typecheck
+-- without additional type annotation.
+getSpec
+  :: forall r args result.
+  Spec args result
+  -> (args ⋯-> r)
+  -> result
+  -> args ⋯-> r
+getSpec (Spec s) k d = s @r k d
+
+-- | Given a list of ways to compare demands, a demand specification, and an
+-- evaluation of a particular function, determine if the function met the
+-- specification, as decided by the comparisons. If so, return the prediction
+-- of the specification.
+compareToSpecWith
+  :: forall args result.
+  (All Shaped args, Curry args, Shaped result)
+  => NP DemandComparison args
+  -> Spec args result
+  -> Evaluation args result
+  -> Maybe (NP Demand args)
+compareToSpecWith comparisons spec (Evaluation inputs inputsD resultD) =
+  let prediction =
+        Curry.uncurry
+          (getSpec @(NP Demand args)
+             spec
+             collectDemands
+             (fromDemand $ E resultD))
+          inputs
+      correct =
+        all id . hcollapse $
+          hcliftA3 (Proxy @Shaped)
+          (\(DemandComparison c) iD iD' -> K $ iD `c` iD')
+            comparisons
+            inputsD
+            prediction
+  in if correct then Nothing else Just prediction
+  where
+    collectDemands :: args ⋯-> NP Demand args
+    collectDemands =
+      curryCollect @args (hcmap (Proxy @Shaped) (toDemand . unI))
+
+curryCollect
+  :: forall (xs :: [Type]) r. Curry xs => (NP I xs -> r) -> xs ⋯-> r
+curryCollect k = Curry.curry @xs k
+
+-- | Checks if a given 'Evaluation' exactly matches the prediction of a given
+-- 'Spec', returning the prediction of that @Spec@ if not
+--
+-- __Note:__ In the case of __success__ this returns @Nothing@; in the case of
+-- __failure__ this returns @Just@ the incorrect prediction.
+equalToSpec
+  :: forall args result.
+  (All Shaped args, Shaped result, Curry args)
+  => Spec args result
+  -> Evaluation args result
+  -> Maybe (NP Demand args)
+equalToSpec spec e =
+  compareToSpecWith compareEquality spec e
+
+-- | A @Strictness@ represents (roughly) how strict a randomly generated
+-- function or evaluation context should be
+--
+-- An evaluation context generated with some strictness @s@ (i.e. through
+-- 'evaluationForall') will consume at most @s@ constructors of its input,
+-- although it might consume fewer.
+newtype Strictness
+  = Strictness Int
+  deriving stock (Eq, Ord)
+  deriving newtype (Show, Num)
+
+-- | A function can be checked against a specification if it meets the
+-- @StrictCheck@ constraint
+type StrictCheck function =
+  ( Shaped (Result function)
+  , Consume (Result function)
+  , Curry (Args function)
+  , All Typeable (Args function)
+  , All Shaped (Args function) )
+
+-- | The most general function for random strictness testing: all of the more
+-- convenient such functions can be derived from this one
+--
+-- Given some function @f@, this takes as arguments:
+--
+-- * A 'QC.Args' record describing arguments to pass to the underlying
+--   QuickCheck engine
+-- * An 'NP' n-ary product of 'Shrink' shrinkers, one for each argument of @f@
+-- * An 'NP' n-ary product of 'Gen' generators, one for each argument of @f@
+-- * A 'Gen' generator for strictnesses to be tested
+-- * A predicate on 'Evaluation's: if the 'Evaluation' passes the predicate,
+--   it should return @Nothing@; otherwise, it should return @Just@ some
+--   @evidence@ representing the failure (when checking 'Spec's, this evidence
+--   comes in the form of a @Spec@'s (incorrect) prediction)
+-- * the function @f@ to be tested
+--
+-- If all tests succeed, @(Nothing, result)@ is returned, where @result@ is the
+-- underlying 'QC.Result' type from "Test.QuickCheck". If there is a test
+-- failure, it also returns @Just@ the failed 'Evaluation' as well as whatever
+-- @evidence@ was produced by the predicate.
+strictCheckWithResults ::
+  forall function evidence.
+  StrictCheck function
+  => QC.Args
+  -> NP Shrink (Args function)  -- TODO: allow dependent shrinking
+  -> NP Gen (Args function)     -- TODO: allow dependent generation
+  -> Gen Strictness
+  -> (Evaluation (Args function) (Result function) -> Maybe evidence)
+  -> function
+  -> IO ( Maybe ( Evaluation (Args function) (Result function)
+                , evidence )
+        , QC.Result )
+strictCheckWithResults
+  qcArgs shrinks gens strictness predicate function = do
+    ref <- newIORef Nothing
+    result <-
+      quickCheckWithResult qcArgs{chatty = False{-, maxSuccess = 10000-}} $
+        forAllShrink
+          (evaluationForall @function gens strictness function)
+          (shrinkEvalWith @function shrinks function) $
+            \example ->
+              case predicate example of
+                Nothing ->
+                  property True
+                Just evidence ->
+                  whenFail (writeIORef ref $ Just (example, evidence)) False
+    readIORef ref >>= \case
+      Nothing      -> pure (Nothing,      result)
+      Just example -> pure (Just example, result)
+
+-- | Check a function to see whether it exactly meets a strictness specification
+--
+-- If the function fails to meet the specification, a counterexample is
+-- pretty-printed in a box-drawn diagram illustrating how the specification
+-- failed to match the real observed behavior of the function.
+strictCheckSpecExact
+  :: forall function.
+  ( StrictCheck function
+  , All Arbitrary (Args function)
+  , All Produce (Args function)
+  ) => Spec (Args function) (Result function)
+    -> function
+    -> IO ()
+strictCheckSpecExact spec function =
+  do (maybeExample, result) <-
+       strictCheckWithResults
+         stdArgs
+         shrinkViaArbitrary
+         genViaProduce
+         strictnessViaSized
+         (equalToSpec spec)
+         function
+     case lines (output result) of
+       line0 : _ -> putStrLn line0
+       [] -> pure ()
+     case maybeExample of
+       Nothing -> return ()
+       Just example -> do
+         unicode <- doesStdoutAcceptUnicode
+         putStrLn (Prelude.uncurry (displayCounterSpec unicode) example)
+
+doesStdoutAcceptUnicode :: IO Bool
+doesStdoutAcceptUnicode = do
+  encoding <- IO.hGetEncoding IO.stdout
+  case encoding of
+    Nothing -> pure False
+    Just enc -> pure (any (((==) `on` textEncodingName) enc) [IO.utf8, IO.utf8_bom, IO.utf16, IO.utf16le, IO.utf16be, IO.utf32, IO.utf32le, IO.utf32be])
+
+------------------------------------------------------------
+-- An Evaluation is what we generate when StrictCheck-ing --
+------------------------------------------------------------
+
+-- | A snapshot of the observed strictness behavior of a function
+--
+-- An @Evaluation@ contains the 'inputs' at which a function was called, the
+-- 'inputDemands' which were induced upon those inputs, and the 'resultDemand'
+-- which induced that demand on the inputs.
+data Evaluation args result =
+  Evaluation
+    { inputs       :: NP I      args    -- ^ Inputs to a function
+    , inputDemands :: NP Demand args    -- ^ Demands on the input
+    , resultDemand :: PosDemand result  -- ^ Demand on the result
+    }
+
+instance (All Typeable args, Typeable result)
+  => Show (Evaluation args result) where
+  show _ =
+    "<Evaluation> :: Evaluation"
+    ++ " '[" ++ intercalate ", " argTypes ++ "]"
+    ++ " " ++ show (typeRep :: TypeRep result)
+    where
+      argTypes :: [String]
+      argTypes =
+        hcollapse
+        $ hliftA (K . show)
+        $ (hcpure (Proxy @Typeable) typeRep :: NP TypeRep args)
+
+
+-----------------------------------
+-- Generating random evaluations --
+-----------------------------------
+
+-- | Given a list of generators for a function's arguments and a generator for
+-- random strictnesses (measured in number of constructors evaluated), create
+-- a generator for random 'Evaluation's of that function in random contexts
+evaluationForall
+  :: forall f.
+  ( Curry (Args f)
+  , Consume (Result f)
+  , Shaped (Result f)
+  , All Shaped (Args f)
+  ) => NP Gen (Args f)
+    -> Gen Strictness
+    -> f
+    -> Gen (Evaluation (Args f) (Result f))
+evaluationForall gens strictnessGen function = do
+  inputs     <- hsequence gens
+  strictness <- strictnessGen
+  toOmega    <- freely produce
+  return (go strictness toOmega inputs)
+  where
+    -- If context is fully lazy, increase strictness until it forces something
+    go :: Strictness
+       -> (Result f -> Omega)
+       -> NP I (Args f)
+       -> Evaluation (Args f) (Result f)
+    go (Strictness s) tO is =
+      let (resultD, inputsD) =
+            observeNP (forceOmega s . tO) (uncurryAll @f function) is
+      in case resultD of
+        T -> go (Strictness s + 1) tO is
+        E posResultD ->
+          Evaluation is inputsD posResultD
+
+
+---------------------------
+-- Shrinking evaluations --
+---------------------------
+
+-- | Given a shrinker for each of the arguments of a function, the function
+-- itself, and some 'Evaluation' of that function, produce a list of smaller
+-- @Evaluation@s of that function
+shrinkEvalWith
+  :: forall f.
+  ( Curry (Args f)
+  , Shaped (Result f)
+  , All Shaped (Args f)
+  ) => NP Shrink (Args f)
+    -> f
+    -> Evaluation (Args f) (Result f)
+    -> [Evaluation (Args f) (Result f)]
+shrinkEvalWith
+  shrinks (uncurryAll -> function) (Evaluation inputs _ resultD) =
+    let shrunkDemands   = shrinkDemand @(Result f) resultD
+        shrunkInputs    = fairInterleave (axialShrinks shrinks inputs)
+        shrinkingDemand = mapMaybe      (reObserve inputs)  shrunkDemands
+        shrinkingInputs = mapMaybe (flip reObserve resultD) shrunkInputs
+    in fairInterleave [ shrinkingDemand, shrinkingInputs ]
+  where
+    reObserve
+      :: NP I (Args f)
+      -> PosDemand (Result f)
+      -> Maybe (Evaluation (Args f) (Result f))
+    reObserve is rD =
+      let (rD', isD) = observeNP (evaluateDemand rD) function is
+      in fmap (Evaluation is isD) $
+           case rD' of
+             T     -> Nothing
+             E pos -> Just pos
+
+-- | If 'False' (unicode output is disabled), replace all non-ASCII characters with '?'.
+sanitize :: Bool -> String -> String
+sanitize True = id
+sanitize False = fmap (\c -> if ord c < 128 then c else '?')
+
+-- | Render a counter-example to a specification (that is, an 'Evaluation'
+-- paired with some expected input demands it doesn't match) as a
+-- box-drawing sketch (in Unicode or ASCII depending on whether the
+-- first argument is 'True' or 'False')
+displayCounterSpec
+  :: forall args result.
+  (Shaped result, All Shaped args)
+  => Bool  -- ^ 'True' to enable prettier Unicode output
+  -> Evaluation args result
+  -> NP Demand args
+  -> String
+displayCounterSpec unicode (Evaluation inputs inputsD resultD) predictedInputsD =
+  sanitize unicode $
+  beside inputBox ("   " : threeDashes : repeat "   ") resultBox
+  ++ (flip replicate ' ' $
+       (2 `max` (subtract 2 $ (lineMax [inputString] `div` 2))))
+  ++ threeArrows
+  ++ beside
+       actualBox
+       ("       " : "       " : notEqual : repeat "       ")
+       predictedBox
+  where
+    threeDashes | unicode = "───"
+                | otherwise = "---"
+    threeArrows | unicode = "🡓 🡓 🡓\n"
+                | otherwise = "v v v\n"
+    notEqual | unicode = "  ═╱═  "
+             | otherwise = "  =/=  "
+    inputBox
+      | unicode =
+      box "┌" '─'         "┐"
+          "│" inputHeader "├"
+          "├" '─'         "┤"
+          "│" inputString "│"
+          "└" '─'         "┘"
+      | otherwise =
+      box "+" '-'         "+"
+          "|" inputHeader "+"
+          "+" '-'         "+"
+          "|" inputString "|"
+          "+" '-'         "+"
+
+    resultBox
+      | unicode =
+      box "┌" '─'          "┐"
+          "┤" resultHeader "│"
+          "├" '─'          "┤"
+          "│" resultString "│"
+          "└" '─'          "┘"
+      | otherwise =
+      box "+" '-'          "+"
+          "+" resultHeader "|"
+          "+" '-'          "+"
+          "|" resultString "|"
+          "+" '-'          "+"
+
+    actualBox
+      | unicode =
+      box "┌" '─'                "┐"
+          "│" actualHeader       "│"
+          "├" '─'                "┤"
+          "│" actualDemandString "│"
+          "└" '─'                "┘"
+      | otherwise =
+      box "+" '-'                "+"
+          "|" actualHeader       "|"
+          "+" '-'                "+"
+          "|" actualDemandString "|"
+          "+" '-'                "+"
+
+    predictedBox
+      | unicode =
+      box "┌" '─'                   "┐"
+          "│" predictedHeader       "│"
+          "├" '─'                   "┤"
+          "│" predictedDemandString "│"
+          "└" '─'                   "┘"
+      | otherwise =
+      box "+" '-'                   "+"
+          "|" predictedHeader       "|"
+          "+" '-'                   "+"
+          "|" predictedDemandString "|"
+          "+" '-'                   "+"
+
+    inputHeader = " Input" ++ plural
+    resultHeader = " Demand on result"
+    actualHeader = " Actual input demand" ++ plural
+    predictedHeader = " Spec's input demand" ++ plural
+
+    inputString =
+      showBulletedNPWith @Shaped (prettyDemand . interleave Eval . unI) inputs
+    resultString = " " ++ prettyDemand @result (E resultD)
+    actualDemandString =
+      showBulletedNPWith @Shaped prettyDemand inputsD
+    predictedDemandString =
+      showBulletedNPWith @Shaped prettyDemand predictedInputsD
+
+    rule w l c r = frame w l (replicate w c) r ++ "\n"
+
+    frame w before str after =
+      before ++ str
+      ++ (replicate (w - length str) ' ')
+      ++ after
+
+    frames w before para after =
+      unlines $ map (\str -> frame w before str after) (lines para)
+
+    beside l cs r =
+      unlines . take (length ls `max` length rs) $
+        zipWith3
+          (\x c y -> x ++ c ++ y)
+          (ls ++ repeat (replicate (lineMax [l]) ' '))
+          cs
+          (rs ++ repeat "")
+      where
+        ls = lines l
+        rs = lines r
+
+    box top_l    top    top_r
+        header_l header header_r
+        div_l    div_c  div_r
+        body_l   body   body_r
+        bottom_l bottom bottom_r =
+      let w = lineMax [header, body]
+      in rule   w top_l    top    top_r
+      ++ frames w header_l header header_r
+      ++ rule   w div_l    div_c  div_r
+      ++ frames w body_l   body   body_r
+      ++ rule   w bottom_l bottom bottom_r
+
+    lineMax strs =
+      (maximum . map
+        (\(lines -> ls) -> maximum (map length ls) + 1) $ strs)
+
+    plural = case inputs of
+      (_ :* Nil) -> ""
+      _          -> "s"
+
+    showBulletedNPWith
+      :: forall c g xs. All c xs
+      => (forall x. c x => g x -> String) -> NP g xs -> String
+    -- showBulletedNPWith display (x :* Nil) = " " ++ display x ++ "\n"
+    showBulletedNPWith display list = showNPWith' list
+      where
+        showNPWith' :: forall ys. All c ys => NP g ys -> String
+        showNPWith'      Nil = ""
+        showNPWith' (y :* ys) =
+          bullet ++ display y ++ "\n" ++ showNPWith' ys
+    bullet | unicode = " • "
+           | otherwise = " * "

@@ -1,275 +1,275 @@-{-| This module defines the 'Consume' typeclass, used for incrementally-    destructing inputs to random non-strict functions.--    Calling 'consume' on some value lazily returns an abstract type of 'Input',-    which contains all the entropy present in the original value. Paired with-    'Test.StrictCheck.Produce', these @Input@ values can be used to generate-    random non-strict functions, whose strictness behavior is dependent on the-    values given to them.--}-module Test.StrictCheck.Consume-  ( -- * Incrementally consuming input-    Input-  , Inputs-  , Consume(..)-  -- * Manually writing 'Consume' instances-  , constructor-  , normalize-  , consumeTrivial-  , consumePrimitive-  -- * Generically deriving 'Consume' instances-  , GConsume-  , gConsume-  ) where--import Test.QuickCheck-import Generics.SOP-import Generics.SOP.NS--import Test.StrictCheck.Internal.Inputs--import Data.Complex--import Data.Foldable as Fold-import Data.List.NonEmpty (NonEmpty(..))-import Data.Tree     as Tree-import Data.Set      as Set-import Data.Map      as Map-import Data.Sequence as Seq-import Data.IntMap   as IntMap-import Data.IntSet   as IntSet----- | Lazily monomorphize some input value, by converting it into an @Input@.--- This is an incremental version of QuickCheck's @CoArbitrary@ typeclass.--- It can also be seen as a generalization of the @NFData@ class.------ Instances of @Consume@ can be derived automatically for any type implementing--- the @Generic@ class from "GHC.Generics". Using the @DeriveAnyClass@--- extension, we can say:------ > import GHC.Generics as GHC--- > import Generics.SOP as SOP--- >--- > data D x y--- >   = A--- >   | B (x, y)--- >   deriving (GHC.Generic, SOP.Generic, Consume)------ This automatic derivation follows these rules, which you can follow too if--- you're manually writing an instance for some type which is not @Generic@:------ For each distinct constructor, make a single call to 'constructor' with--- a distinct @Int@, and a list of @Input@s, each created by recursively calling--- 'consume' on every field in that constructor. For abstract types (e.g. sets),--- the same procedure can be used upon an extracted list representation of the--- contents.-class Consume a where-  -- | Convert an @a@ into an @Input@ by recursively destructing it using calls-  -- to @consume@-  consume :: a -> Input-  default consume :: GConsume a => a -> Input-  consume = gConsume---- | Reassemble pieces of input into a larger Input: this is to be called on the--- result of @consume@-ing subparts of input-constructor :: Int -> [Input] -> Input-constructor n !is =-  Input (Variant (variant n)) is---- | Use the CoArbitrary instance for a type to consume it------ This should only be used for "flat" types, i.e. those which contain no--- interesting consumable substructure, as it's fully strict (non-incremental)-consumePrimitive :: CoArbitrary a => a -> Input-consumePrimitive !a =-  Input (Variant (coarbitrary a)) []---- | Consume a type which has no observable structure whatsoever------ This should only be used for types for which there is only one inhabitant, or--- for which inhabitants cannot be distinguished at all.-consumeTrivial :: a -> Input-consumeTrivial !_ =-  Input mempty []---- | Fully normalize something which can be consumed-normalize :: Consume a => a -> ()-normalize (consume -> input) = go input-  where-    go (Input _ is) = Fold.foldr seq () (fmap go is)------------------------------------------------- Deriving Consume instances generically --------------------------------------------------- | The constraints necessary to generically @consume@ something-type GConsume a = (Generic a, All2 Consume (Code a))---- | Generic 'consume'-gConsume :: GConsume a => a -> Input-gConsume !(from -> sop) =-  constructor (index_SOP sop)-  . hcollapse-  . hcliftA (Proxy @Consume) (K . consume . unI)-  $ sop--------------------- Instances --------------------instance Consume (a -> b)  where consume = consumeTrivial-instance Consume (Proxy p) where consume = consumeTrivial--instance Consume Char     where consume = consumePrimitive-instance Consume Word     where consume = consumePrimitive-instance Consume Int      where consume = consumePrimitive-instance Consume Double   where consume = consumePrimitive-instance Consume Float    where consume = consumePrimitive-instance Consume Rational where consume = consumePrimitive-instance Consume Integer  where consume = consumePrimitive-instance (CoArbitrary a, RealFloat a) => Consume (Complex a) where-  consume = consumePrimitive--instance Consume ()-instance Consume Bool-instance Consume Ordering-instance Consume a => Consume (Maybe a)-instance (Consume a, Consume b) => Consume (Either a b)-instance Consume a => Consume [a]---instance Consume a => Consume (NonEmpty a) where-  consume (a :| as) = constructor 0 [consume a, consume as]--instance Consume a => Consume (Tree a) where-  consume (Node a as) = constructor 0 [consume a, consume as]--instance Consume v => Consume (Map k v) where-  consume = constructor 0 . fmap (consume . snd) . Map.toList--consumeContainer :: (Consume a, Foldable t) => t a -> Input-consumeContainer = constructor 0 . fmap consume . Fold.toList--instance Consume v => Consume (Seq v)    where consume = consumeContainer-instance Consume v => Consume (Set v)    where consume = consumeContainer-instance Consume v => Consume (IntMap v) where consume = consumeContainer-instance Consume IntSet where-  consume = consumeContainer . IntSet.toList---- TODO: instances for the rest of Containers--instance (Consume a, Consume b) => Consume (a, b)-instance (Consume a, Consume b, Consume c) => Consume (a, b, c)-instance (Consume a, Consume b, Consume c, Consume d) => Consume (a, b, c, d)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e-         ) => Consume-  (a, b, c, d, e)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         ) => Consume-  (a, b, c, d, e, f)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g-         ) => Consume-  (a, b, c, d, e, f, g)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h-         ) => Consume-  (a, b, c, d, e, f, g, h)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i-         ) => Consume-  (a, b, c, d, e, f, g, h, i)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j-         ) => Consume-  (a, b, c, d, e, f, g, h, i, j)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j, Consume k-         ) => Consume-  (a, b, c, d, e, f, g, h, i, j, k)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l-         ) => Consume-  (a, b, c, d, e, f, g, h, i, j, k, l)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l-         , Consume m-         ) => Consume-  (a, b, c, d, e, f, g, h, i, j, k, l, m)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l-         , Consume m, Consume n-         ) => Consume-  (a, b, c, d, e, f, g, h, i, j, k, l, m, n)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l-         , Consume m, Consume n, Consume o-         ) => Consume-  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l-         , Consume m, Consume n, Consume o, Consume p-         ) => Consume-  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l-         , Consume m, Consume n, Consume o, Consume p, Consume q-         ) => Consume-  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l-         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r-         ) => Consume-  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l-         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r-         , Consume s-         ) => Consume-  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l-         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r-         , Consume s, Consume t-         ) => Consume-  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l-         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r-         , Consume s, Consume t, Consume u-         ) => Consume-  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l-         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r-         , Consume s, Consume t, Consume u, Consume v-         ) => Consume-  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l-         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r-         , Consume s, Consume t, Consume u, Consume v, Consume w-         ) => Consume-  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l-         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r-         , Consume s, Consume t, Consume u, Consume v, Consume w, Consume x-          ) => Consume-  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l-         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r-         , Consume s, Consume t, Consume u, Consume v, Consume w, Consume x-         , Consume y-         ) => Consume-  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y)-instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f-         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l-         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r-         , Consume s, Consume t, Consume u, Consume v, Consume w, Consume x-         , Consume y, Consume z-         ) => Consume-  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z)+{-| This module defines the 'Consume' typeclass, used for incrementally
+    destructing inputs to random non-strict functions.
+
+    Calling 'consume' on some value lazily returns an abstract type of 'Input',
+    which contains all the entropy present in the original value. Paired with
+    'Test.StrictCheck.Produce', these @Input@ values can be used to generate
+    random non-strict functions, whose strictness behavior is dependent on the
+    values given to them.
+-}
+module Test.StrictCheck.Consume
+  ( -- * Incrementally consuming input
+    Input
+  , Inputs
+  , Consume(..)
+  -- * Manually writing 'Consume' instances
+  , constructor
+  , normalize
+  , consumeTrivial
+  , consumePrimitive
+  -- * Generically deriving 'Consume' instances
+  , GConsume
+  , gConsume
+  ) where
+
+import Test.QuickCheck
+import Generics.SOP
+import Generics.SOP.NS
+
+import Test.StrictCheck.Internal.Inputs
+
+import Data.Complex
+
+import Data.Foldable as Fold
+import Data.List.NonEmpty (NonEmpty(..))
+import Data.Tree     as Tree
+import Data.Set      as Set
+import Data.Map      as Map
+import Data.Sequence as Seq
+import Data.IntMap   as IntMap
+import Data.IntSet   as IntSet
+
+
+-- | Lazily monomorphize some input value, by converting it into an @Input@.
+-- This is an incremental version of QuickCheck's @CoArbitrary@ typeclass.
+-- It can also be seen as a generalization of the @NFData@ class.
+--
+-- Instances of @Consume@ can be derived automatically for any type implementing
+-- the @Generic@ class from "GHC.Generics". Using the @DeriveAnyClass@
+-- extension, we can say:
+--
+-- > import GHC.Generics as GHC
+-- > import Generics.SOP as SOP
+-- >
+-- > data D x y
+-- >   = A
+-- >   | B (x, y)
+-- >   deriving (GHC.Generic, SOP.Generic, Consume)
+--
+-- This automatic derivation follows these rules, which you can follow too if
+-- you're manually writing an instance for some type which is not @Generic@:
+--
+-- For each distinct constructor, make a single call to 'constructor' with
+-- a distinct @Int@, and a list of @Input@s, each created by recursively calling
+-- 'consume' on every field in that constructor. For abstract types (e.g. sets),
+-- the same procedure can be used upon an extracted list representation of the
+-- contents.
+class Consume a where
+  -- | Convert an @a@ into an @Input@ by recursively destructing it using calls
+  -- to @consume@
+  consume :: a -> Input
+  default consume :: GConsume a => a -> Input
+  consume = gConsume
+
+-- | Reassemble pieces of input into a larger Input: this is to be called on the
+-- result of @consume@-ing subparts of input
+constructor :: Int -> [Input] -> Input
+constructor n !is =
+  Input (Variant (variant n)) is
+
+-- | Use the CoArbitrary instance for a type to consume it
+--
+-- This should only be used for "flat" types, i.e. those which contain no
+-- interesting consumable substructure, as it's fully strict (non-incremental)
+consumePrimitive :: CoArbitrary a => a -> Input
+consumePrimitive !a =
+  Input (Variant (coarbitrary a)) []
+
+-- | Consume a type which has no observable structure whatsoever
+--
+-- This should only be used for types for which there is only one inhabitant, or
+-- for which inhabitants cannot be distinguished at all.
+consumeTrivial :: a -> Input
+consumeTrivial !_ =
+  Input mempty []
+
+-- | Fully normalize something which can be consumed
+normalize :: Consume a => a -> ()
+normalize (consume -> input) = go input
+  where
+    go (Input _ is) = Fold.foldr seq () (fmap go is)
+
+--------------------------------------------
+-- Deriving Consume instances generically --
+--------------------------------------------
+
+-- | The constraints necessary to generically @consume@ something
+type GConsume a = (Generic a, All2 Consume (Code a))
+
+-- | Generic 'consume'
+gConsume :: GConsume a => a -> Input
+gConsume !(from -> sop) =
+  constructor (index_SOP sop)
+  . hcollapse
+  . hcliftA (Proxy @Consume) (K . consume . unI)
+  $ sop
+
+
+---------------
+-- Instances --
+---------------
+
+instance Consume (a -> b)  where consume = consumeTrivial
+instance Consume (Proxy p) where consume = consumeTrivial
+
+instance Consume Char     where consume = consumePrimitive
+instance Consume Word     where consume = consumePrimitive
+instance Consume Int      where consume = consumePrimitive
+instance Consume Double   where consume = consumePrimitive
+instance Consume Float    where consume = consumePrimitive
+instance Consume Rational where consume = consumePrimitive
+instance Consume Integer  where consume = consumePrimitive
+instance CoArbitrary a => Consume (Complex a) where
+  consume = consumePrimitive
+
+instance Consume ()
+instance Consume Bool
+instance Consume Ordering
+instance Consume a => Consume (Maybe a)
+instance (Consume a, Consume b) => Consume (Either a b)
+instance Consume a => Consume [a]
+
+
+instance Consume a => Consume (NonEmpty a) where
+  consume (a :| as) = constructor 0 [consume a, consume as]
+
+instance Consume a => Consume (Tree a) where
+  consume (Node a as) = constructor 0 [consume a, consume as]
+
+instance Consume v => Consume (Map k v) where
+  consume = constructor 0 . fmap (consume . snd) . Map.toList
+
+consumeContainer :: (Consume a, Foldable t) => t a -> Input
+consumeContainer = constructor 0 . fmap consume . Fold.toList
+
+instance Consume v => Consume (Seq v)    where consume = consumeContainer
+instance Consume v => Consume (Set v)    where consume = consumeContainer
+instance Consume v => Consume (IntMap v) where consume = consumeContainer
+instance Consume IntSet where
+  consume = consumeContainer . IntSet.toList
+
+-- TODO: instances for the rest of Containers
+
+instance (Consume a, Consume b) => Consume (a, b)
+instance (Consume a, Consume b, Consume c) => Consume (a, b, c)
+instance (Consume a, Consume b, Consume c, Consume d) => Consume (a, b, c, d)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e
+         ) => Consume
+  (a, b, c, d, e)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         ) => Consume
+  (a, b, c, d, e, f)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g
+         ) => Consume
+  (a, b, c, d, e, f, g)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h
+         ) => Consume
+  (a, b, c, d, e, f, g, h)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i, j)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j, Consume k
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i, j, k)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i, j, k, l)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l
+         , Consume m
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i, j, k, l, m)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l
+         , Consume m, Consume n
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i, j, k, l, m, n)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l
+         , Consume m, Consume n, Consume o
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l
+         , Consume m, Consume n, Consume o, Consume p
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l
+         , Consume m, Consume n, Consume o, Consume p, Consume q
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l
+         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l
+         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r
+         , Consume s
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l
+         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r
+         , Consume s, Consume t
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l
+         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r
+         , Consume s, Consume t, Consume u
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l
+         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r
+         , Consume s, Consume t, Consume u, Consume v
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l
+         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r
+         , Consume s, Consume t, Consume u, Consume v, Consume w
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l
+         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r
+         , Consume s, Consume t, Consume u, Consume v, Consume w, Consume x
+          ) => Consume
+  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l
+         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r
+         , Consume s, Consume t, Consume u, Consume v, Consume w, Consume x
+         , Consume y
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y)
+instance ( Consume a, Consume b, Consume c, Consume d, Consume e, Consume f
+         , Consume g, Consume h, Consume i, Consume j, Consume k, Consume l
+         , Consume m, Consume n, Consume o, Consume p, Consume q, Consume r
+         , Consume s, Consume t, Consume u, Consume v, Consume w, Consume x
+         , Consume y, Consume z
+         ) => Consume
+  (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z)

@@ -1,147 +1,148 @@-{-| This module defines a flexible and efficient way to curry and uncurry-    functions of any arity. This is useful in the context of StrictCheck to-    provide a lightweight interface to test developers which does not require-    them to directly work with heterogeneous lists.--}-module Test.StrictCheck.Curry-  ( -- * Computing the types of curried functions-    type (⋯->)-  , type (-..->)-  , Args-  , Result-  -- * Currying functions at all arities-  , Curry(..)-  , curryAll-  , uncurryAll-  , withCurryIdentity-  -- * Generalized to any heterogeneous list-  , List(..)-  ) where---import Prelude hiding (curry, uncurry)--import Data.Type.Equality-import qualified Unsafe.Coerce as UNSAFE--import qualified Generics.SOP as SOP------------------------------------------------------- Manipulating the types of curried functions -------------------------------------------------------- | Given a function type, return a list of all its argument types------ For example:------ > Args (Int -> Bool -> Char)  ~  [Int, Bool]-type family Args (f :: *) :: [*] where-  Args (a -> rest) = a : Args rest-  Args x           = '[]---- | Given a list of argument types and the "rest" of a function type, return a--- curried function type which takes the specified argument types in order,--- before returning the given rest------ For example:------ > [Int, Bool] ⋯-> Char  ~  Int -> Bool -> Char------ This infix unicode symbol is meant to evoke a function arrow with an--- ellipsis.-type family (args :: [*]) ⋯-> (rest :: *) :: * where-  '[]        ⋯-> rest = rest-  (a : args) ⋯-> rest = a -> args ⋯-> rest---- | For those who don't want to type in unicode, we provide this ASCII synonym--- for the ellipsis function arrow @(⋯->)@-type args -..-> rest = args ⋯-> rest---- | Strip all arguments from a function type, yielding its (non-function-type)--- result------ For example:------ > Result (Int -> Bool -> Char)  ~  Char-type family Result (f :: *) :: * where-  Result (a -> rest) = Result rest-  Result r           = r--curryIdentity :: forall function.-  function :~: (Args function ⋯-> Result function)-curryIdentity = UNSAFE.unsafeCoerce (Refl :: () :~: ())---- | For any function type @function@, it is always true that------ > function  ~  (Args function ⋯-> Result function)------ GHC doesn't know this, however, so @withCurryIdentity@ provides this proof to--- the enclosed computation, by discharging this wanted equality constraint.-withCurryIdentity :: forall function r.-  (function ~ (Args function ⋯-> Result function) => r) -> r-withCurryIdentity r =-  case curryIdentity @function of Refl -> r------------------------------ Partial uncurrying ------------------------------- | This currying mechanism is agnostic to the concrete heterogeneous list type--- used to carry arguments. The @List@ class abstracts over the nil and cons--- operations of a heterogeneous list: to use your own, just define an instance.-class List (list :: [*] -> *) where-  nil    :: list '[]-  cons   :: x -> list xs -> list (x : xs)-  uncons :: list (x : xs) -> (x, list xs)---- | The Curry class witnesses that for any list of arguments, it is always--- possible to curry/uncurry at that arity-class Curry (args :: [*]) where-  uncurry-    :: forall result list.-    List list => (args ⋯-> result) -> list args -> result-  curry-    :: forall result list.-    List list => (list args -> result) -> args ⋯-> result--instance Curry '[] where-  uncurry x = \(!_) -> x-  curry   f = f nil--instance Curry xs => Curry (x : xs) where-  uncurry f = \(uncons -> (x, xs)) -> uncurry (f x) xs-  curry   f = \x -> curry (\xs -> f (cons x xs))-------------------------------------------------------------- Variadic uncurrying/currying, aka (un)curryAll-ing --------------------------------------------------------------- | Uncurry all arguments to a function type------ This is a special case of 'uncurry', and may ease type inference.-uncurryAll-  :: forall function list. (List list, Curry (Args function))-  => function -> (list (Args function) -> Result function)-uncurryAll = withCurryIdentity @function uncurry---- | Curry all arguments to a function from a heterogeneous list to a result------ This is a special case of 'curry', and may ease type inference.-curryAll-  :: forall args result list. (List list, Curry args)-  => (list args -> result)-  -> (args ⋯-> result)-curryAll = curry-------------------------------- Instances for HLists -------------------------------instance List (SOP.NP SOP.I) where-  nil = SOP.Nil-  cons x xs = SOP.I x SOP.:* xs-  uncons (SOP.I x SOP.:* xs) = (x, xs)+{-| This module defines a flexible and efficient way to curry and uncurry
+    functions of any arity. This is useful in the context of StrictCheck to
+    provide a lightweight interface to test developers which does not require
+    them to directly work with heterogeneous lists.
+-}
+module Test.StrictCheck.Curry
+  ( -- * Computing the types of curried functions
+    type (⋯->)
+  , type (-..->)
+  , Args
+  , Result
+  -- * Currying functions at all arities
+  , Curry(..)
+  , curryAll
+  , uncurryAll
+  , withCurryIdentity
+  -- * Generalized to any heterogeneous list
+  , List(..)
+  ) where
+
+
+import Prelude hiding (curry, uncurry)
+
+import Data.Kind (Type)
+import Data.Type.Equality
+import qualified Unsafe.Coerce as UNSAFE
+
+import qualified Generics.SOP as SOP
+
+
+-------------------------------------------------
+-- Manipulating the types of curried functions --
+-------------------------------------------------
+
+-- | Given a function type, return a list of all its argument types
+--
+-- For example:
+--
+-- > Args (Int -> Bool -> Char)  ~  [Int, Bool]
+type family Args (f :: Type) :: [Type] where
+  Args (a -> rest) = a : Args rest
+  Args x           = '[]
+
+-- | Given a list of argument types and the "rest" of a function type, return a
+-- curried function type which takes the specified argument types in order,
+-- before returning the given rest
+--
+-- For example:
+--
+-- > [Int, Bool] ⋯-> Char  ~  Int -> Bool -> Char
+--
+-- This infix unicode symbol is meant to evoke a function arrow with an
+-- ellipsis.
+type family (args :: [Type]) ⋯-> (rest :: Type) :: Type where
+  '[]        ⋯-> rest = rest
+  (a : args) ⋯-> rest = a -> args ⋯-> rest
+
+-- | For those who don't want to type in unicode, we provide this ASCII synonym
+-- for the ellipsis function arrow @(⋯->)@
+type args -..-> rest = args ⋯-> rest
+
+-- | Strip all arguments from a function type, yielding its (non-function-type)
+-- result
+--
+-- For example:
+--
+-- > Result (Int -> Bool -> Char)  ~  Char
+type family Result (f :: Type) :: Type where
+  Result (a -> rest) = Result rest
+  Result r           = r
+
+curryIdentity :: forall function.
+  function :~: (Args function ⋯-> Result function)
+curryIdentity = UNSAFE.unsafeCoerce (Refl :: () :~: ())
+
+-- | For any function type @function@, it is always true that
+--
+-- > function  ~  (Args function ⋯-> Result function)
+--
+-- GHC doesn't know this, however, so @withCurryIdentity@ provides this proof to
+-- the enclosed computation, by discharging this wanted equality constraint.
+withCurryIdentity :: forall function r.
+  (function ~ (Args function ⋯-> Result function) => r) -> r
+withCurryIdentity r =
+  case curryIdentity @function of Refl -> r
+
+
+------------------------
+-- Partial uncurrying --
+------------------------
+
+-- | This currying mechanism is agnostic to the concrete heterogeneous list type
+-- used to carry arguments. The @List@ class abstracts over the nil and cons
+-- operations of a heterogeneous list: to use your own, just define an instance.
+class List (list :: [Type] -> Type) where
+  nil    :: list '[]
+  cons   :: x -> list xs -> list (x : xs)
+  uncons :: list (x : xs) -> (x, list xs)
+
+-- | The Curry class witnesses that for any list of arguments, it is always
+-- possible to curry/uncurry at that arity
+class Curry (args :: [Type]) where
+  uncurry
+    :: forall result list.
+    List list => (args ⋯-> result) -> list args -> result
+  curry
+    :: forall result list.
+    List list => (list args -> result) -> args ⋯-> result
+
+instance Curry '[] where
+  uncurry x = \(!_) -> x
+  curry   f = f nil
+
+instance Curry xs => Curry (x : xs) where
+  uncurry f = \(uncons -> (x, xs)) -> uncurry (f x) xs
+  curry   f = \x -> curry (\xs -> f (cons x xs))
+
+
+--------------------------------------------------------
+-- Variadic uncurrying/currying, aka (un)curryAll-ing --
+--------------------------------------------------------
+
+-- | Uncurry all arguments to a function type
+--
+-- This is a special case of 'uncurry', and may ease type inference.
+uncurryAll
+  :: forall function list. (List list, Curry (Args function))
+  => function -> (list (Args function) -> Result function)
+uncurryAll = withCurryIdentity @function uncurry
+
+-- | Curry all arguments to a function from a heterogeneous list to a result
+--
+-- This is a special case of 'curry', and may ease type inference.
+curryAll
+  :: forall args result list. (List list, Curry args)
+  => (list args -> result)
+  -> (args ⋯-> result)
+curryAll = curry
+
+
+--------------------------
+-- Instances for HLists --
+--------------------------
+
+instance List (SOP.NP SOP.I) where
+  nil = SOP.Nil
+  cons x xs = SOP.I x SOP.:* xs
+  uncons (SOP.I x SOP.:* xs) = (x, xs)

@@ -1,310 +1,310 @@-{-| A 'Demand' on some value of type @T@ is shaped like a @T@, but possibly-    truncated, to represent partial evaluation. This module defines the type of-    demands, and functions to manipulate them for the purpose of constructing-    demand specifications.--    A demand for some type @T@ can be represented one of two interconvertible-    ways:--    * explicitly, as a recursively interleaved @Shape@ of @T@-    * implicitly, as a value of @T@ with specially-tagged bottom values-      which represent un-evaluated portions of that value--   The explicit representation is useful for writing traversals and other such-   manipulations of demand values, while the implicit representation can prove-   convenient for writing demand specifications. The implicit representation is-   the default when writing specifications, but through the use of 'toDemand'-   and 'fromDemand', either representation can be used wherever it is most-   appropriate.--}-module Test.StrictCheck.Demand-  ( -- * The explicit @Demand@ interface-    Thunk(..)-  , Demand, PosDemand-  , pattern E, pattern T-  -- ** Manipulating explicit @Demand@s-  , evaluateDemand-  , shrinkDemand-  , prettyDemand, printDemand-  , eqDemand-  , showPrettyFieldThunkS-  -- * The implicit @Demand@ interface-  , thunk, isThunk-  -- * Converting between explicit and implicit representations-  , toDemand, fromDemand-  ) where--import qualified Control.Exception as Exception-import qualified GHC.Generics as GHC-import Control.Applicative-import Data.Bifunctor-import System.IO.Unsafe-import Data.Monoid ( Endo(..) )-import Generics.SOP hiding (Shape)--import Test.StrictCheck.Shaped-import Test.StrictCheck.Internal.Unevaluated------------------------------------------------------------- The basic types which make up a demand description --------------------------------------------------------------- | A @Thunk a@ is either an @a@ or a @Thunk@------ When we interleave this type into the @Shape@ of some type, we get the type--- of demands on that type.------ @Thunk a@ is isomorphic to a (strict) @Maybe a@.-data Thunk a-  = Eval !a-  | Thunk-  deriving (Eq, Ord, Show, Functor, GHC.Generic)--instance Applicative Thunk where-  pure = Eval-  Thunk  <*> _      = Thunk-  _      <*> Thunk  = Thunk-  Eval f <*> Eval a = Eval (f a)--instance Num a => Num (Thunk a) where-  (+)         = liftA2 (+)-  (-)         = liftA2 (-)-  (*)         = liftA2 (*)-  abs         = fmap abs-  signum      = fmap signum-  fromInteger = Eval . fromInteger---- | A @Demand@ on some type @a@ is the same shape as that original @a@, but with--- possible @Thunk@s interleaved into it-type Demand-  = (%) Thunk---- | A @PosDemand@ is a "strictly positive" demand, i.e. one where the topmost--- level of the demanded value has definitely been forced------ This is the one-level unwrapping of @Demand@, and is useful to express some--- invariants in specifications-type PosDemand a-  = Shape a Demand--{-# COMPLETE E, T #-}---- | Pattern synonym to abbreviate demand manipulation: @E a = Wrap (Eval a)@-pattern E :: Shape a Demand -> Demand a-pattern E a = Wrap (Eval a)---- | Pattern synonym to abbreviate demand manipulation: @T = Wrap Thunk@-pattern T :: Demand a-pattern T = Wrap Thunk------------------------------ Implicit interface -------------------------------- | A bottom value (inhabiting all types) which StrictCheck interprets as--- an unevaluated subpart of a data structure------ > toDemand thunk  ==  T--- > fromDemand T    ==  thunk-thunk :: forall a. a-thunk = Exception.throw Unevaluated---- | Tests if a particular value is an implicit 'thunk'------ In order to work, this function evaluates its input to weak-head normal form;--- keep this in mind if you care about laziness.-isThunk :: Shaped a => a -> Bool-isThunk a =-  case toDemand a of-    T -> True-    _ -> False---- | Given an @a@ whose substructures may contain 'thunk's (i.e. an implicit--- demand representation), convert it to an explicit 'Demand'------ Inverse to 'fromDemand'.-toDemand :: Shaped a => a -> Demand a-toDemand = interleave toThunk-  where-    {-# NOINLINE toThunk #-}-    toThunk :: a -> Thunk a-    toThunk a = unsafePerformIO $-      Exception.catch-        (let !_ = a in return (Eval a))-        (\(_ :: Unevaluated) -> return Thunk)---- | Given an explicit @Demand@ for some type @a@, convert it to a value of type--- @a@, substituting a 'thunk' for each 'T' found in the explicit demand------ Inverse to 'toDemand'.-fromDemand :: Shaped a => Demand a -> a-fromDemand = fuse fromThunk-  where-    {-# NOINLINE fromThunk #-}-    fromThunk :: Thunk a -> a-    fromThunk (Eval a) = a-    fromThunk Thunk =-      Exception.throw Unevaluated---------------------------- Shrinking demands ------------------------------ | Shrink a non-zero demand (analogous to QuickCheck's @shrink@)------ While QuickCheck's typical @shrink@ instances reduce the size of a value by--- slicing off the top-most structure, @shrinkDemand@ reduces the size of a--- demand by pruning it's deepest /leaves/. This ensures that all resultant--- shrunken demands are strict sub-demands of the original.-shrinkDemand :: forall a. Shaped a => PosDemand a -> [PosDemand a]-shrinkDemand d =-  match @a d d $ \(Flattened un flat) _ ->-    un <$> shrinkOne flat-  where-    shrinkOne :: All Shaped xs => NP Demand xs -> [NP Demand xs]-    shrinkOne Nil = []-    shrinkOne (T :* xs) =-      (T :*) <$> shrinkOne xs-    shrinkOne ((E f :: Demand x) :* xs) =-      fmap ((:* xs) . E) (shrinkDemand @x f)-      ++ fmap (E f :* ) (shrinkOne xs)------------------------------------------ Evaluating demands as contexts ------------------------------------------- | Evaluate some value of type @a@ to the degree specified by the given demand------ If the demand and the value diverge (they pick a different side of a sum),--- evaluation will stop at this point. Usually, @evaluateDemand@ is only called--- on demands which are known to be structurally-compatible with the--- accompanying value, although nothing really goes wrong if this is not true.-evaluateDemand :: forall a. Shaped a => PosDemand a -> a -> ()-evaluateDemand demand value =-  go @a (E demand) (I % value)-  where-    go :: forall x. Shaped x => Thunk % x -> I % x -> ()-    go T     _            = ()-    go (E d) (Wrap (I v)) =-      match @x d v $-        \(Flattened _ fieldsD) -> maybe () $-        \(Flattened _ fieldsV) ->-            foldr seq () . hcollapse $-              hcliftA2 (Proxy @Shaped) ((K .) . go) fieldsD fieldsV----------------------------------- Pretty-printing demands ------------------------------------ | A very general 'showsPrec' style function for printing demands------ @showPrettyFieldThunkS q t p r@ returns a function @(String -> String)@ which--- appends its input to a pretty-printed representation of a demand.------ Specifically:--- * @q@ is a boolean flag determining if names should be printed--- as qualified--- * @t@ is a string which is to be printed when a thunk is encountered--- * @p@ is the precedence context of this function call--- * @r@ is the 'Rendered Thunk' representing some demand------ This is very general, but we expose it in its complexity just in case some--- person wants to build a different pretty-printer.------ The precedence-aware pretty-printing algorithm used here is adapted from a--- solution given by Brian Huffman on StackOverflow:--- <https://stackoverflow.com/questions/27471937/43639618#43639618>.-showPrettyFieldThunkS-  :: Bool -> String -> Int -> Rendered Thunk -> String -> String-showPrettyFieldThunkS _            t _    (RWrap Thunk)      = (t ++)-showPrettyFieldThunkS qualifyNames t prec (RWrap (Eval pd)) =-  case pd of-    ConstructorD name fields ->-      showParen (prec > 10 && length fields > 0) $-        showString (qualify name)-        . flip foldMapCompose fields-          (((' ' :) .) . showPrettyFieldThunkS qualifyNames t 11)-    RecordD name recfields ->-      showParen (prec > 10) $-        showString (qualify name)-        . flip foldMapCompose recfields-          (\(fName, x) ->-             ((((" " ++ qualify fName ++ " = ") ++) .) $-             showPrettyFieldThunkS qualifyNames t 11 x))-    InfixD name assoc fixity l r ->-      showParen (prec > fixity) $-        let (lprec, rprec) =-              case assoc of-                LeftAssociative  -> (fixity,     fixity + 1)-                RightAssociative -> (fixity + 1, fixity)-                NotAssociative   -> (fixity + 1, fixity + 1)-        in showPrettyFieldThunkS qualifyNames t lprec l-         . showString (" " ++ qualify name ++ " ")-         . showPrettyFieldThunkS qualifyNames t rprec r-    CustomD fixity list ->-      showParen (prec > fixity) $-        foldr (.) id $ flip fmap list $-          extractEither-          . bimap (showString . qualifyEither)-                  (\(f, pf) -> showPrettyFieldThunkS qualifyNames t f pf)-  where-    qualify (m, _, n) =-      if qualifyNames then (m ++ "." ++ n) else n--    qualifyEither (Left s) = s-    qualifyEither (Right (m, n)) =-      if qualifyNames then (m ++ "." ++ n) else n--    extractEither (Left x)  = x-    extractEither (Right x) = x--    foldMapCompose :: (a -> (b -> b)) -> [a] -> (b -> b)-    foldMapCompose f = appEndo . foldMap (Endo . f)---- | Pretty-print a demand for display, given the precendence context-prettyDemandPrec :: Shaped a => Int -> Demand a -> ShowS-prettyDemandPrec prec d =-  showPrettyFieldThunkS False "_" prec (renderfold d)---- | Pretty-print a demand for display-prettyDemand :: Shaped a => Demand a -> String-prettyDemand d = prettyDemandPrec 0 d ""---- | Print a demand to standard output------ > printDemand = putStrLn . prettyDemand-printDemand :: Shaped a => Demand a -> IO ()-printDemand = putStrLn . prettyDemand--instance Shaped a => Show (Demand a) where-  showsPrec = prettyDemandPrec---- TODO: Comparisons module?---- | Determine if two demands are exactly equal------ This relies on the @match@ method from the @Shaped@ instance for the two--- demands, and does not require the underlying types to have @Eq@ instances.--- However, this means that types whose @match@ methods are more coarse than--- their equality will be compared differently by @eqDemand@. In particular,--- the demand representations of functions will all be compared to be equal.-eqDemand :: forall a. Shaped a => Demand a -> Demand a -> Bool-eqDemand T      T      = True-eqDemand T      (E _)  = False-eqDemand (E _)  T      = False-eqDemand (E d1) (E d2) =-  match @a d1 d2 $-    \(Flattened _ flatD1) -> maybe False $-    \(Flattened _ flatD2) ->-      all id . hcollapse $-        hcliftA2 (Proxy @Shaped)-          ((K .) . eqDemand) flatD1 flatD2---- | 'Demand's are compared for equality using 'eqDemand'; see its documentation--- for details-instance Shaped a => Eq (Demand a) where-  (==) = eqDemand+{-| A 'Demand' on some value of type @T@ is shaped like a @T@, but possibly
+    truncated, to represent partial evaluation. This module defines the type of
+    demands, and functions to manipulate them for the purpose of constructing
+    demand specifications.
+
+    A demand for some type @T@ can be represented one of two interconvertible
+    ways:
+
+    * explicitly, as a recursively interleaved @Shape@ of @T@
+    * implicitly, as a value of @T@ with specially-tagged bottom values
+      which represent un-evaluated portions of that value
+
+   The explicit representation is useful for writing traversals and other such
+   manipulations of demand values, while the implicit representation can prove
+   convenient for writing demand specifications. The implicit representation is
+   the default when writing specifications, but through the use of 'toDemand'
+   and 'fromDemand', either representation can be used wherever it is most
+   appropriate.
+-}
+module Test.StrictCheck.Demand
+  ( -- * The explicit @Demand@ interface
+    Thunk(..)
+  , Demand, PosDemand
+  , pattern E, pattern T
+  -- ** Manipulating explicit @Demand@s
+  , evaluateDemand
+  , shrinkDemand
+  , prettyDemand, printDemand
+  , eqDemand
+  , showPrettyFieldThunkS
+  -- * The implicit @Demand@ interface
+  , thunk, isThunk
+  -- * Converting between explicit and implicit representations
+  , toDemand, fromDemand
+  ) where
+
+import qualified Control.Exception as Exception
+import qualified GHC.Generics as GHC
+import Control.Applicative (liftA2) -- for GHC 9.2
+import Data.Bifunctor
+import System.IO.Unsafe
+import Data.Monoid ( Endo(..) )
+import Generics.SOP hiding (Shape)
+
+import Test.StrictCheck.Shaped
+import Test.StrictCheck.Internal.Unevaluated
+
+--------------------------------------------------------
+-- The basic types which make up a demand description --
+--------------------------------------------------------
+
+-- | A @Thunk a@ is either an @a@ or a @Thunk@
+--
+-- When we interleave this type into the @Shape@ of some type, we get the type
+-- of demands on that type.
+--
+-- @Thunk a@ is isomorphic to a (strict) @Maybe a@.
+data Thunk a
+  = Eval !a
+  | Thunk
+  deriving (Eq, Ord, Show, Functor, GHC.Generic)
+
+instance Applicative Thunk where
+  pure = Eval
+  Thunk  <*> _      = Thunk
+  _      <*> Thunk  = Thunk
+  Eval f <*> Eval a = Eval (f a)
+
+instance Num a => Num (Thunk a) where
+  (+)         = liftA2 (+)
+  (-)         = liftA2 (-)
+  (*)         = liftA2 (*)
+  abs         = fmap abs
+  signum      = fmap signum
+  fromInteger = Eval . fromInteger
+
+-- | A @Demand@ on some type @a@ is the same shape as that original @a@, but with
+-- possible @Thunk@s interleaved into it
+type Demand
+  = (%) Thunk
+
+-- | A @PosDemand@ is a "strictly positive" demand, i.e. one where the topmost
+-- level of the demanded value has definitely been forced
+--
+-- This is the one-level unwrapping of @Demand@, and is useful to express some
+-- invariants in specifications
+type PosDemand a
+  = Shape a Demand
+
+{-# COMPLETE E, T #-}
+
+-- | Pattern synonym to abbreviate demand manipulation: @E a = Wrap (Eval a)@
+pattern E :: Shape a Demand -> Demand a
+pattern E a = Wrap (Eval a)
+
+-- | Pattern synonym to abbreviate demand manipulation: @T = Wrap Thunk@
+pattern T :: Demand a
+pattern T = Wrap Thunk
+
+
+------------------------
+-- Implicit interface --
+------------------------
+
+
+-- | A bottom value (inhabiting all types) which StrictCheck interprets as
+-- an unevaluated subpart of a data structure
+--
+-- > toDemand thunk  ==  T
+-- > fromDemand T    ==  thunk
+thunk :: forall a. a
+thunk = Exception.throw Unevaluated
+
+-- | Tests if a particular value is an implicit 'thunk'
+--
+-- In order to work, this function evaluates its input to weak-head normal form;
+-- keep this in mind if you care about laziness.
+isThunk :: Shaped a => a -> Bool
+isThunk a =
+  case toDemand a of
+    T -> True
+    _ -> False
+
+-- | Given an @a@ whose substructures may contain 'thunk's (i.e. an implicit
+-- demand representation), convert it to an explicit 'Demand'
+--
+-- Inverse to 'fromDemand'.
+toDemand :: Shaped a => a -> Demand a
+toDemand = interleave toThunk
+  where
+    {-# NOINLINE toThunk #-}
+    toThunk :: a -> Thunk a
+    toThunk a = unsafePerformIO $
+      Exception.catch
+        (let !_ = a in return (Eval a))
+        (\(_ :: Unevaluated) -> return Thunk)
+
+-- | Given an explicit @Demand@ for some type @a@, convert it to a value of type
+-- @a@, substituting a 'thunk' for each 'T' found in the explicit demand
+--
+-- Inverse to 'toDemand'.
+fromDemand :: Shaped a => Demand a -> a
+fromDemand = fuse fromThunk
+  where
+    {-# NOINLINE fromThunk #-}
+    fromThunk :: Thunk a -> a
+    fromThunk (Eval a) = a
+    fromThunk Thunk =
+      Exception.throw Unevaluated
+
+-----------------------
+-- Shrinking demands --
+-----------------------
+
+-- | Shrink a non-zero demand (analogous to QuickCheck's @shrink@)
+--
+-- While QuickCheck's typical @shrink@ instances reduce the size of a value by
+-- slicing off the top-most structure, @shrinkDemand@ reduces the size of a
+-- demand by pruning it's deepest /leaves/. This ensures that all resultant
+-- shrunken demands are strict sub-demands of the original.
+shrinkDemand :: forall a. Shaped a => PosDemand a -> [PosDemand a]
+shrinkDemand d =
+  match @a d d $ \(Flattened un flat) _ ->
+    un <$> shrinkOne flat
+  where
+    shrinkOne :: All Shaped xs => NP Demand xs -> [NP Demand xs]
+    shrinkOne Nil = []
+    shrinkOne (T :* xs) =
+      (T :*) <$> shrinkOne xs
+    shrinkOne ((E f :: Demand x) :* xs) =
+      fmap ((:* xs) . E) (shrinkDemand @x f)
+      ++ fmap (E f :* ) (shrinkOne xs)
+
+
+------------------------------------
+-- Evaluating demands as contexts --
+------------------------------------
+
+-- | Evaluate some value of type @a@ to the degree specified by the given demand
+--
+-- If the demand and the value diverge (they pick a different side of a sum),
+-- evaluation will stop at this point. Usually, @evaluateDemand@ is only called
+-- on demands which are known to be structurally-compatible with the
+-- accompanying value, although nothing really goes wrong if this is not true.
+evaluateDemand :: forall a. Shaped a => PosDemand a -> a -> ()
+evaluateDemand demand value =
+  go @a (E demand) (I % value)
+  where
+    go :: forall x. Shaped x => Thunk % x -> I % x -> ()
+    go T     _            = ()
+    go (E d) (Wrap (I v)) =
+      match @x d v $
+        \(Flattened _ fieldsD) -> maybe () $
+        \(Flattened _ fieldsV) ->
+            foldr seq () . hcollapse $
+              hcliftA2 (Proxy @Shaped) ((K .) . go) fieldsD fieldsV
+
+
+-----------------------------
+-- Pretty-printing demands --
+-----------------------------
+
+-- | A very general 'showsPrec' style function for printing demands
+--
+-- @showPrettyFieldThunkS q t p r@ returns a function @(String -> String)@ which
+-- appends its input to a pretty-printed representation of a demand.
+--
+-- Specifically:
+-- * @q@ is a boolean flag determining if names should be printed
+-- as qualified
+-- * @t@ is a string which is to be printed when a thunk is encountered
+-- * @p@ is the precedence context of this function call
+-- * @r@ is the 'Rendered Thunk' representing some demand
+--
+-- This is very general, but we expose it in its complexity just in case some
+-- person wants to build a different pretty-printer.
+--
+-- The precedence-aware pretty-printing algorithm used here is adapted from a
+-- solution given by Brian Huffman on StackOverflow:
+-- <https://stackoverflow.com/questions/27471937/43639618#43639618>.
+showPrettyFieldThunkS
+  :: Bool -> String -> Int -> Rendered Thunk -> String -> String
+showPrettyFieldThunkS _            t _    (RWrap Thunk)      = (t ++)
+showPrettyFieldThunkS qualifyNames t prec (RWrap (Eval pd)) =
+  case pd of
+    ConstructorD name fields ->
+      showParen (prec > 10 && length fields > 0) $
+        showString (qualify name)
+        . flip foldMapCompose fields
+          (((' ' :) .) . showPrettyFieldThunkS qualifyNames t 11)
+    RecordD name recfields ->
+      showParen (prec > 10) $
+        showString (qualify name)
+        . flip foldMapCompose recfields
+          (\(fName, x) ->
+             ((((" " ++ qualify fName ++ " = ") ++) .) $
+             showPrettyFieldThunkS qualifyNames t 11 x))
+    InfixD name assoc fixity l r ->
+      showParen (prec > fixity) $
+        let (lprec, rprec) =
+              case assoc of
+                LeftAssociative  -> (fixity,     fixity + 1)
+                RightAssociative -> (fixity + 1, fixity)
+                NotAssociative   -> (fixity + 1, fixity + 1)
+        in showPrettyFieldThunkS qualifyNames t lprec l
+         . showString (" " ++ qualify name ++ " ")
+         . showPrettyFieldThunkS qualifyNames t rprec r
+    CustomD fixity list ->
+      showParen (prec > fixity) $
+        foldr (.) id $ flip fmap list $
+          extractEither
+          . bimap (showString . qualifyEither)
+                  (\(f, pf) -> showPrettyFieldThunkS qualifyNames t f pf)
+  where
+    qualify (m, _, n) =
+      if qualifyNames then (m ++ "." ++ n) else n
+
+    qualifyEither (Left s) = s
+    qualifyEither (Right (m, n)) =
+      if qualifyNames then (m ++ "." ++ n) else n
+
+    extractEither (Left x)  = x
+    extractEither (Right x) = x
+
+    foldMapCompose :: (a -> (b -> b)) -> [a] -> (b -> b)
+    foldMapCompose f = appEndo . foldMap (Endo . f)
+
+-- | Pretty-print a demand for display, given the precendence context
+prettyDemandPrec :: Shaped a => Int -> Demand a -> ShowS
+prettyDemandPrec prec d =
+  showPrettyFieldThunkS False "_" prec (renderfold d)
+
+-- | Pretty-print a demand for display
+prettyDemand :: Shaped a => Demand a -> String
+prettyDemand d = prettyDemandPrec 0 d ""
+
+-- | Print a demand to standard output
+--
+-- > printDemand = putStrLn . prettyDemand
+printDemand :: Shaped a => Demand a -> IO ()
+printDemand = putStrLn . prettyDemand
+
+instance Shaped a => Show (Demand a) where
+  showsPrec = prettyDemandPrec
+
+-- TODO: Comparisons module?
+
+-- | Determine if two demands are exactly equal
+--
+-- This relies on the @match@ method from the @Shaped@ instance for the two
+-- demands, and does not require the underlying types to have @Eq@ instances.
+-- However, this means that types whose @match@ methods are more coarse than
+-- their equality will be compared differently by @eqDemand@. In particular,
+-- the demand representations of functions will all be compared to be equal.
+eqDemand :: forall a. Shaped a => Demand a -> Demand a -> Bool
+eqDemand T      T      = True
+eqDemand T      (E _)  = False
+eqDemand (E _)  T      = False
+eqDemand (E d1) (E d2) =
+  match @a d1 d2 $
+    \(Flattened _ flatD1) -> maybe False $
+    \(Flattened _ flatD2) ->
+      all id . hcollapse $
+        hcliftA2 (Proxy @Shaped)
+          ((K .) . eqDemand) flatD1 flatD2
+
+-- | 'Demand's are compared for equality using 'eqDemand'; see its documentation
+-- for details
+instance Shaped a => Eq (Demand a) where
+  (==) = eqDemand

@@ -1,266 +1,272 @@-{-| This module defines a variety of specifications for functions on lists,-    demonstrating the specification interface of StrictCheck. See the-    documentation of "Test.StrictCheck" (specifically 'strictCheckSpecExact')-    for details on how to test these specifications.--    This module's primary utility is to teach how specifications work. Because-    Haddock omits the definitions of values, you'll learn the most by viewing-    the source of this module.--}-module Test.StrictCheck.Examples.Lists where--import Test.StrictCheck-import Data.Functor---- * Specifying some simple functions on lists---- | A correct specification for 'length'-length_spec :: Spec '[[a]] Int-length_spec =-  Spec $ \predict _ xs ->-    predict (xs $> thunk)---- | A naive specification for 'take', which is wrong-take_spec_too_easy :: Spec '[Int, [a]] [a]-take_spec_too_easy =-  Spec $ \predict _d n xs ->-    predict n xs---- | A correct specification for 'take'-take_spec :: Spec '[Int, [a]] [a]-take_spec =-  Spec $ \predict d n xs ->-    predict n (if n > length xs then d else d ++ thunk)---- | A functionally correct implementation of 'take' which has subtly different--- strictness properties------ This will fail when tested against 'take_spec'.-take' :: Int -> [a] -> [a]-take' _      [] = []-take' n (x : xs)-  | n > 0     = x : take' (n-1) xs-  | otherwise = []---- | A correct specification of '(++)'-append_spec :: Shaped a => Spec '[[a], [a]] [a]-append_spec =-  Spec $ \predict d ls rs ->-    let spineLen   = length . cap $ d ++ [undefined]  -- number of spine thunks forced-        overLs     = spineLen > length ls             -- forced all of ls?-        overRs     = spineLen > length ls + length rs -- forced all of bs?-        (ls', rs') = splitAt (length ls) (cap d)-    in predict-         (ls' ++ if overLs then [] else thunk)-         (rs' ++ if overRs then [] else thunk)---- | A correct specification of 'reverse'-reverse_spec :: Shaped a => Spec '[[a]] [a]-reverse_spec =-  Spec $ \predict d xs ->-    let padLen = length xs - length (cap d)-        spinePad = replicate padLen thunk-    in  predict $ spinePad ++ (reverse (cap d))---- | A correct specification for 'zip'-zip_spec :: (Shaped a, Shaped b) => Spec '[[a], [b]] [(a, b)]-zip_spec =-  Spec $ \predict d as bs ->-    let (d_as, d_bs) = unzip d-    in predict-         (if      length (cap d_bs) > length as-          && not (length (cap d_as) > length bs)-          then d_as-          else d_as ++ thunk)-         (if length (cap d_as) > length bs-          && not (length (cap d_bs) > length as)-          then d_bs-          else d_bs ++ thunk)---- | A functionally correct implementation of 'zip' which has subtly different--- strictness properties------ This will fail when tested against 'zip_spec'.-zip' :: [a] -> [b] -> [(a, b)]-zip' [      ] [      ] = []-zip' (_ : as) [      ] = zip' as []-zip' [      ] (_ : bs) = zip' [] bs-zip' (a : as) (b : bs) = (a, b) : zip' as bs---- | A correct specification for 'map', demonstrating specifications for--- higher-order functions-map_spec-  :: forall a b. (Shaped a, Shaped b)-  => Spec '[a -> b, [a]] [b]-map_spec =-  Spec $ \predict d f xs ->-    predict-      (if all isThunk (cap d) then thunk else f)-      (zipWith (specify1 f) d xs)---- * Specifying the productive rotate function from Okasaki's purely functional--- queue implementation (see paper for more details)---- | Given three lists @xs@, @ys@, and @zs@, compute @xs ++ reverse ys ++ zs@,--- but with more uniform strictness------ Specifically, if @ys@ is shorter than @xs@, the work necessary to reverse it--- will have already occurred by the time @xs@ is traversed.-rotate :: [a] -> [a] -> [a] -> [a]-rotate [      ] [      ] as =                       as-rotate [      ] (b : bs) as =     rotate [] bs (b : as)-rotate (f : fs) [      ] as = f : rotate fs []      as-rotate (f : fs) (b : bs) as = f : rotate fs bs (b : as)---- | Specialization of 'rotate': @rot xs ys = rotate xs ys []@-rot :: [a] -> [a] -> [a]-rot fs bs = rotate fs bs []---- | The naive version of 'rot': @rot' xs ys = xs ++ reverse ys@------ This is functionally equivalent to 'rot' but not equivalent in strictness--- behavior.-rot' :: [a] -> [a] -> [a]-rot' fs bs = fs ++ reverse bs---- | A previous iteration of `rot_spec'`, this one is also correct, but may be--- less readable.-rot_spec :: Shaped a => Spec '[[a], [a]] [a]-rot_spec =-  Spec $ \predict d fs bs ->-    let (fs', bs') = splitAt (length fs) (cap d)-        spineLen  = length (cap (d ++ [undefined]))  -- # of spine thunks forced-        overflow  = spineLen       > length fs  -- begun taking from bs?-        overrot   = length (cap d) > length bs  -- forced all of bs?-        padLength =-          length bs `min`-            if overflow-            then length bs - length bs'-            else length (cap d)-        spinePad = replicate padLength thunk-    in predict-         (                    fs' ++ if overflow            then [] else thunk)-         (spinePad ++ reverse bs' ++ if overflow || overrot then [] else thunk)---- | A correct specification of `rot`, this is also the version we presented in--- the paper.-rot_spec' :: Shaped a => Spec '[[a], [a]] [a]-rot_spec' =-  Spec $ \predict d fs bs ->-    let demandOnFs-          | length (cap d) > length fs =-              take (length fs) (cap d)-          | otherwise = d-        demandOnBs-          | length (cap $ d ++ [undefined]) > length fs =-              reverse $ take (length bs)-                      $ drop (length fs) (cap d) ++ repeat thunk-          | length (cap d) > length bs =-              reverse $ drop (length fs) (cap d) ++ replicate (length bs) thunk-          | otherwise =-              (reverse $ drop (length fs) (cap d) ++ replicate (length (cap d)) thunk) ++ thunk-    in predict demandOnFs demandOnBs---   where predictedFsDemand---           | outputDemandLength < length fs =---               outputDemand ++ thunk---           | otherwise =---               fsPartOfOutDemand---         predictedBsDemand---           | outputDemandLength < length bs =------           | otherwise =------     let (fs', bs') = splitAt (length fs) (cap d)---         spineLen  = length (cap (d ++ [undefined]))  -- # of spine thunks forced---         overflow  = spineLen       > length fs  -- begun taking from bs?---         overrot   = length (cap d) > length bs  -- forced all of bs?---         padLength =---           length bs `min`---             if overflow---             then length bs - length bs'---             else length (cap d)---         spinePad = replicate padLength thunk---     in predict---          (                    fs' ++ if overflow            then [] else thunk)---          (spinePad ++ reverse bs' ++ if overflow || overrot then [] else thunk)----rot_spec' :: Shaped a => Spec '[[a], [a]] [a]---rot_spec' = rot_spec---- | An incorrect specification for `rot` that miscalculates the number of cells--- forced.-rot_simple_spec :: Shaped a => Spec '[[a], [a]] [a]-rot_simple_spec =-  Spec $ \predict d fs bs ->-    let demandOnFs-          | length (cap d) > length fs =-              take (length fs) d-          | otherwise = d-        demandOnBs-          | length (cap d) > length fs ||-            (null bs && length fs == length (cap d) && length fs /= length (cap $ d ++ [thunk])) =-              reverse $ take (length bs) $ (drop (length fs) (cap d)) ++ repeat thunk-          | otherwise =-              thunk-    in predict demandOnFs demandOnBs--test_rot :: [Int] -> [Int] -> [Int] -> IO ()-test_rot d xs ys =-  (\(x :* y :* Nil) -> printDemand x >> printDemand y)-  . snd $ observe (toContext d) (rot @Int) xs ys---- * Utilities for working with demands over lists---- | If the tail of the second list is 'thunk', replace it with the first list-replaceThunk :: Shaped a => [a] -> [a] -> [a]-replaceThunk r xs       | isThunk xs = r-replaceThunk _ [      ] = []-replaceThunk r (x : xs) = x : replaceThunk r xs---- | If the tail of the list is 'thunk', replace it with @[]@------ This is a special case of 'replaceThunk'.-cap :: Shaped a => [a] -> [a]-cap = replaceThunk []---- | Lift an ordinary function to apply to explicit 'Demand's------ It is true that @Demand@s are a functor, but they can't be a Haskell--- 'Functor' because they're a type family-(%$) :: (Shaped a, Shaped b) => (a -> b) -> Demand a -> Demand b-(%$) f = toDemand . f . fromDemand---- | Apply a 'Demand' on a function to a 'Demand' on a value------ It is true that @Demand@s are an applicative functor, but they can't be a--- Haskell 'Functor' because they're a type family-(%*) :: (Shaped a, Shaped b) => Demand (a -> b) -> Demand a -> Demand b-f %* a = toDemand $ fromDemand f (fromDemand a)---- TODO: make n-ary version of this (CPS-ed)--- | Given a unary function, an implicit demand on its result, and its input,--- compute its actual demand on its input in that context------ This demand is calculated using 'observe1', so it is guaranteed to be--- correct.-specify1 :: forall a b. (Shaped a, Shaped b)-         => (a -> b) -> b -> a -> a-specify1 f b a =-  fromDemand . snd $ observe1 (toContext b) f a---- | Given an implicit demand, convert it to an evaluation context------ That is, @toContext d a@ evaluates @a@ to the degree that @d@ is a defined--- value. This uses the function 'evaluateDemand'; refer to its documentation--- for details about how demands are used to evaluate values.-toContext :: Shaped b => b -> b -> ()-toContext b =-  case toDemand b of-    T    -> const ()-    E b' -> evaluateDemand b'---- | Assert at runtime that a value is /not/ a 'thunk', failing with an error--- if it is-expectTotal :: Shaped a => a -> a-expectTotal a =-  if isThunk a then error "expectTotal: given thunk" else a+{-| This module defines a variety of specifications for functions on lists,
+    demonstrating the specification interface of StrictCheck. See the
+    documentation of "Test.StrictCheck" (specifically 'strictCheckSpecExact')
+    for details on how to test these specifications.
+
+    This module's primary utility is to teach how specifications work. Because
+    Haddock omits the definitions of values, you'll learn the most by viewing
+    the source of this module.
+-}
+module Test.StrictCheck.Examples.Lists where
+
+import Test.StrictCheck
+import Data.Functor (($>))
+
+-- * Specifying some simple functions on lists
+
+-- | A correct specification for 'length'
+length_spec :: Spec '[[a]] Int
+length_spec =
+  Spec $ \predict _ xs ->
+    predict (xs $> thunk)
+
+-- | An incorrect specification for 'length' (to test the pretty printer)
+bad_length_spec :: Spec '[[a]] Int
+bad_length_spec =
+  Spec $ \predict _ xs ->
+    predict (take 1 xs $> thunk)
+
+-- | A naive specification for 'take', which is wrong
+take_spec_too_easy :: Spec '[Int, [a]] [a]
+take_spec_too_easy =
+  Spec $ \predict _d n xs ->
+    predict n xs
+
+-- | A correct specification for 'take'
+take_spec :: Spec '[Int, [a]] [a]
+take_spec =
+  Spec $ \predict d n xs ->
+    predict n (if n > length xs then d else d ++ thunk)
+
+-- | A functionally correct implementation of 'take' which has subtly different
+-- strictness properties
+--
+-- This will fail when tested against 'take_spec'.
+take' :: Int -> [a] -> [a]
+take' _      [] = []
+take' n (x : xs)
+  | n > 0     = x : take' (n-1) xs
+  | otherwise = []
+
+-- | A correct specification of '(++)'
+append_spec :: Shaped a => Spec '[[a], [a]] [a]
+append_spec =
+  Spec $ \predict d ls rs ->
+    let spineLen   = length . cap $ d ++ [undefined]  -- number of spine thunks forced
+        overLs     = spineLen > length ls             -- forced all of ls?
+        overRs     = spineLen > length ls + length rs -- forced all of bs?
+        (ls', rs') = splitAt (length ls) (cap d)
+    in predict
+         (ls' ++ if overLs then [] else thunk)
+         (rs' ++ if overRs then [] else thunk)
+
+-- | A correct specification of 'reverse'
+reverse_spec :: Shaped a => Spec '[[a]] [a]
+reverse_spec =
+  Spec $ \predict d xs ->
+    let padLen = length xs - length (cap d)
+        spinePad = replicate padLen thunk
+    in  predict $ spinePad ++ (reverse (cap d))
+
+-- | A correct specification for 'zip'
+zip_spec :: (Shaped a, Shaped b) => Spec '[[a], [b]] [(a, b)]
+zip_spec =
+  Spec $ \predict d as bs ->
+    let (d_as, d_bs) = unzip d
+    in predict
+         (if      length (cap d_bs) > length as
+          && not (length (cap d_as) > length bs)
+          then d_as
+          else d_as ++ thunk)
+         (if length (cap d_as) > length bs
+          && not (length (cap d_bs) > length as)
+          then d_bs
+          else d_bs ++ thunk)
+
+-- | A functionally correct implementation of 'zip' which has subtly different
+-- strictness properties
+--
+-- This will fail when tested against 'zip_spec'.
+zip' :: [a] -> [b] -> [(a, b)]
+zip' [      ] [      ] = []
+zip' (_ : as) [      ] = zip' as []
+zip' [      ] (_ : bs) = zip' [] bs
+zip' (a : as) (b : bs) = (a, b) : zip' as bs
+
+-- | A correct specification for 'map', demonstrating specifications for
+-- higher-order functions
+map_spec
+  :: forall a b. (Shaped a, Shaped b)
+  => Spec '[a -> b, [a]] [b]
+map_spec =
+  Spec $ \predict d f xs ->
+    predict
+      (if all isThunk (cap d) then thunk else f)
+      (zipWith (specify1 f) d xs)
+
+-- * Specifying the productive rotate function from Okasaki's purely functional
+-- queue implementation (see paper for more details)
+
+-- | Given three lists @xs@, @ys@, and @zs@, compute @xs ++ reverse ys ++ zs@,
+-- but with more uniform strictness
+--
+-- Specifically, if @ys@ is shorter than @xs@, the work necessary to reverse it
+-- will have already occurred by the time @xs@ is traversed.
+rotate :: [a] -> [a] -> [a] -> [a]
+rotate [      ] [      ] as =                       as
+rotate [      ] (b : bs) as =     rotate [] bs (b : as)
+rotate (f : fs) [      ] as = f : rotate fs []      as
+rotate (f : fs) (b : bs) as = f : rotate fs bs (b : as)
+
+-- | Specialization of 'rotate': @rot xs ys = rotate xs ys []@
+rot :: [a] -> [a] -> [a]
+rot fs bs = rotate fs bs []
+
+-- | The naive version of 'rot': @rot' xs ys = xs ++ reverse ys@
+--
+-- This is functionally equivalent to 'rot' but not equivalent in strictness
+-- behavior.
+rot' :: [a] -> [a] -> [a]
+rot' fs bs = fs ++ reverse bs
+
+-- | A previous iteration of `rot_spec'`, this one is also correct, but may be
+-- less readable.
+rot_spec :: Shaped a => Spec '[[a], [a]] [a]
+rot_spec =
+  Spec $ \predict d fs bs ->
+    let (fs', bs') = splitAt (length fs) (cap d)
+        spineLen  = length (cap (d ++ [undefined]))  -- # of spine thunks forced
+        overflow  = spineLen       > length fs  -- begun taking from bs?
+        overrot   = length (cap d) > length bs  -- forced all of bs?
+        padLength =
+          length bs `min`
+            if overflow
+            then length bs - length bs'
+            else length (cap d)
+        spinePad = replicate padLength thunk
+    in predict
+         (                    fs' ++ if overflow            then [] else thunk)
+         (spinePad ++ reverse bs' ++ if overflow || overrot then [] else thunk)
+
+-- | A correct specification of `rot`, this is also the version we presented in
+-- the paper.
+rot_spec' :: Shaped a => Spec '[[a], [a]] [a]
+rot_spec' =
+  Spec $ \predict d fs bs ->
+    let demandOnFs
+          | length (cap d) > length fs =
+              take (length fs) (cap d)
+          | otherwise = d
+        demandOnBs
+          | length (cap $ d ++ [undefined]) > length fs =
+              reverse $ take (length bs)
+                      $ drop (length fs) (cap d) ++ repeat thunk
+          | length (cap d) > length bs =
+              reverse $ drop (length fs) (cap d) ++ replicate (length bs) thunk
+          | otherwise =
+              (reverse $ drop (length fs) (cap d) ++ replicate (length (cap d)) thunk) ++ thunk
+    in predict demandOnFs demandOnBs
+--   where predictedFsDemand
+--           | outputDemandLength < length fs =
+--               outputDemand ++ thunk
+--           | otherwise =
+--               fsPartOfOutDemand
+--         predictedBsDemand
+--           | outputDemandLength < length bs =
+--
+--           | otherwise =
+--
+--     let (fs', bs') = splitAt (length fs) (cap d)
+--         spineLen  = length (cap (d ++ [undefined]))  -- # of spine thunks forced
+--         overflow  = spineLen       > length fs  -- begun taking from bs?
+--         overrot   = length (cap d) > length bs  -- forced all of bs?
+--         padLength =
+--           length bs `min`
+--             if overflow
+--             then length bs - length bs'
+--             else length (cap d)
+--         spinePad = replicate padLength thunk
+--     in predict
+--          (                    fs' ++ if overflow            then [] else thunk)
+--          (spinePad ++ reverse bs' ++ if overflow || overrot then [] else thunk)
+
+--rot_spec' :: Shaped a => Spec '[[a], [a]] [a]
+--rot_spec' = rot_spec
+
+-- | An incorrect specification for `rot` that miscalculates the number of cells
+-- forced.
+rot_simple_spec :: Shaped a => Spec '[[a], [a]] [a]
+rot_simple_spec =
+  Spec $ \predict d fs bs ->
+    let demandOnFs
+          | length (cap d) > length fs =
+              take (length fs) d
+          | otherwise = d
+        demandOnBs
+          | length (cap d) > length fs ||
+            (null bs && length fs == length (cap d) && length fs /= length (cap $ d ++ [thunk])) =
+              reverse $ take (length bs) $ (drop (length fs) (cap d)) ++ repeat thunk
+          | otherwise =
+              thunk
+    in predict demandOnFs demandOnBs
+
+test_rot :: [Int] -> [Int] -> [Int] -> IO ()
+test_rot d xs ys =
+  (\(x :* y :* Nil) -> printDemand x >> printDemand y)
+  . snd $ observe (toContext d) (rot @Int) xs ys
+
+-- * Utilities for working with demands over lists
+
+-- | If the tail of the second list is 'thunk', replace it with the first list
+replaceThunk :: Shaped a => [a] -> [a] -> [a]
+replaceThunk r xs       | isThunk xs = r
+replaceThunk _ [      ] = []
+replaceThunk r (x : xs) = x : replaceThunk r xs
+
+-- | If the tail of the list is 'thunk', replace it with @[]@
+--
+-- This is a special case of 'replaceThunk'.
+cap :: Shaped a => [a] -> [a]
+cap = replaceThunk []
+
+-- | Lift an ordinary function to apply to explicit 'Demand's
+--
+-- It is true that @Demand@s are a functor, but they can't be a Haskell
+-- 'Functor' because they're a type family
+(%$) :: (Shaped a, Shaped b) => (a -> b) -> Demand a -> Demand b
+(%$) f = toDemand . f . fromDemand
+
+-- | Apply a 'Demand' on a function to a 'Demand' on a value
+--
+-- It is true that @Demand@s are an applicative functor, but they can't be a
+-- Haskell 'Functor' because they're a type family
+(%*) :: (Shaped a, Shaped b) => Demand (a -> b) -> Demand a -> Demand b
+f %* a = toDemand $ fromDemand f (fromDemand a)
+
+-- TODO: make n-ary version of this (CPS-ed)
+-- | Given a unary function, an implicit demand on its result, and its input,
+-- compute its actual demand on its input in that context
+--
+-- This demand is calculated using 'observe1', so it is guaranteed to be
+-- correct.
+specify1 :: forall a b. (Shaped a, Shaped b)
+         => (a -> b) -> b -> a -> a
+specify1 f b a =
+  fromDemand . snd $ observe1 (toContext b) f a
+
+-- | Given an implicit demand, convert it to an evaluation context
+--
+-- That is, @toContext d a@ evaluates @a@ to the degree that @d@ is a defined
+-- value. This uses the function 'evaluateDemand'; refer to its documentation
+-- for details about how demands are used to evaluate values.
+toContext :: Shaped b => b -> b -> ()
+toContext b =
+  case toDemand b of
+    T    -> const ()
+    E b' -> evaluateDemand b'
+
+-- | Assert at runtime that a value is /not/ a 'thunk', failing with an error
+-- if it is
+expectTotal :: Shaped a => a -> a
+expectTotal a =
+  if isThunk a then error "expectTotal: given thunk" else a

@@ -1,198 +1,198 @@-{-# LANGUAGE TemplateHaskell, BangPatterns, DerivingStrategies #-}--{- | This module showcases another type of specification different from those in-   "Test.StrictCheck.Examples.Lists". Here, we demonstrate that StrictCheck is-   able to distinguish value-lazy maps from value-strict maps.--   In this module, we first develop the solution of the Knapsack dynamic-   programming problem by taking the fixpoint of a step function of the solution-   table. We represent the solution table with a map, and write a specification-   that is critical for the termination of this solution.--}-module Test.StrictCheck.Examples.Map where--import Prelude hiding (lookup)-import Debug.Trace--import qualified GHC.Generics as GHC-import Generics.SOP (Generic, HasDatatypeInfo, NS(..), hd, tl)--import Test.StrictCheck-import Test.StrictCheck.TH--import Data.Maybe-import Data.Function--import Test.QuickCheck---- | We roll our own map type to avoid dealing with abstract types.-data Map k v = Bin (Map k v) k v (Map k v) -- ^ A node that contains a key value pair-             | Empty                       -- ^ An empty node-             deriving stock    (GHC.Generic, Show, Eq, Ord)-             deriving anyclass (Generic, HasDatatypeInfo, Consume, Shaped)---- | A specialized map useful for knapsack. The pair of ints represent the two--- parameters to each knapsack sub-problem solved along the way. These two--- parameters determine the subsequence of items each sub-problem is concerned--- with, and the weight limit.-type KMap = Map (Int, Int) Int--$(derivePatternSynonyms ''Map)---- | This replaces the thunk in a map partial value with the `r` parameter. This--- is very similar to the `cap` function in the lists example.-replaceThunk :: (Shaped k, Shaped v) => Map k v -> Map k v -> Map k v-replaceThunk r m     | isThunk m = r-replaceThunk _ Empty             = Empty-replaceThunk r (Bin ml k v mr)   = Bin (replaceThunk r ml) k v (replaceThunk r mr)---- | A helper for building a map from a list of values.-fromList :: [((Int, Int), Int)] -> KMap-fromList = foldr (\(k, v) acc -> insert k v acc) Empty---- | A simplified insert that ignores rebalancing since rebalancing is not--- important for the spec we will write.-insert :: (Ord k) => k -> v -> Map k v -> Map k v-insert key value Empty = Bin Empty key value Empty-insert key value (Bin ml k v mr) | key < k   = Bin (insert key value ml) k v mr-                                 | key > k   = Bin ml k v (insert key value mr)-                                 | otherwise = Bin ml key value mr---- | The lookup function specialized for knapsack.-lookup :: KMap -> (Int, Int) -> Maybe Int-lookup Empty _                        = Nothing-lookup (Bin ml k' v mr) k | k == k'   = Just v-                          | k <  k'   = lookup ml k-                          | otherwise = lookup mr k---- | This function extracts all of the keys of a map.-keys :: Map k v -> [k]-keys Empty           = []-keys (Bin ml k _ mr) = keys ml ++ [k] ++ keys mr---- | A lookup function that returns the default value `0` for keys that are not--- in the map. This saves us from doing repeated pattern matching when querying--- the solution table.-(!) :: KMap -> (Int, Int) -> Int-(!) m k = case lookup m k of-            Nothing -> 0-            Just v  -> v---- | Weight parameters to the knapsack problem.-weights :: [Int]-weights = [10, 20, 30]---- | Value parameters to the knapsack problem, note that this must be the same--- length as `weights`.-values :: [Int]-values = [60, 100, 120]---- | The weight limit of the knapsack problem.-limit :: Int-limit = 50---- | One step of the knapsack computation. This is a direct translation from the--- recurrence relation of the knapsack problem.-solutionStep :: Map (Int, Int) Int -> Map (Int, Int) Int-solutionStep soln =-  fromList [((j, k), knapsack j k) | j <- [0 .. length weights-1], k <- [0 .. limit]]-  where-    knapsack j k = if j - 1 < 0 || k - weights !! j < 0-                   then if j >= 0 && weights !! j <= k then values !! j else 0-                   else max (soln ! (j-1, k))-                            (soln ! (j-1, k - weights !! j) + values !! j)---- | The fixpoint of the recurrence relation, which is also the solution for the--- knapsack problem.-solution :: Map (Int, Int) Int-solution = fix solutionStep---- | A pattern synonym for extracting demands of each component from the demand--- of a pair.-pattern Pair' :: Demand a -> Demand b -> Demand (a, b)-pattern Pair' x y = Wrap (Eval (GS (Z (x :* y :* Nil))))---- | This function computes the nth pre-fixpoint of the knapsack solution, and--- looks up the value at the specified cell from the pre-fixpoint.-iterSolution :: (Int, Int) -> Int -> Map (Int, Int) Int -> Maybe Int-iterSolution k n soln = lookup m k-  where m | n <= 0    = soln-          | otherwise = (iterate solutionStep soln) !! n---- | This is the same as `iterSolution`, but uses a newtype wrapper for the--- index into the map since we want to write a customized `Arbitrary` instance--- for `Key`.-iterSolutionWithKey :: Key -> Int -> Map (Int, Int) Int -> Maybe Int-iterSolutionWithKey (Key k) = iterSolution k---- | The newtype wrapper of index into the knapsack solution table.-newtype Key = Key { getKey :: (Int, Int) }-  deriving stock    (GHC.Generic, Show, Eq, Ord)-  deriving anyclass (Generic, HasDatatypeInfo, Consume, Shaped)---- | The customized generator for `Key` that only generates valid keys given the--- problem parameters.-instance Arbitrary Key where-  -- Just to make sure keys are within the parameters of the problem-  arbitrary = fmap Key $-    (,) <$> elements [0 .. length weights - 1] <*> elements [0 .. limit]---- | The customized generator for solution tables that only generates valid--- pre-fixpoints.-instance Arbitrary KMap where-  -- I need to generate only valid pre-fixpoints, which is either-  -- Empty (iterated 0 times), or iterate once on Empty, or twice, and-  -- so on-  arbitrary = do-    NonNegative n <- arbitrary-    return $ (iterate solutionStep Empty) !! n---- | A dummy produce instance for the solution table.-instance Produce KMap where-  -- I don't need lazy functions on KMaps. Since the spec only checks-  -- whether a particular entry in the KMap is evaluated or not.-  produce = arbitrary---- | A dummy produce instance for the index into the solution table.-instance Produce Key where-  -- I don't need lazy functions on keys either.-  produce = arbitrary---- | This IO action ties the spec together with everything built so far, and--- runs the StrictCheck randomized testing framework.-runMapTest :: IO ()-runMapTest = strictCheckWithResults-               stdArgs{maxSize=100, maxSuccess=1000}-               shrinkViaArbitrary-               genViaProduce-               strictnessViaSized-               iterSolution_spec-               iterSolutionWithKey >>= print---- | This is the specification that establishes a property important for the--- termination of `solution`: given any pre-fixpoint of `pre-solution`, forcing--- the value at pre-solution[i][j] should not induce a demand at the (i, j) cell--- of the input that steps to pre-solution, since otherwise this would be an--- infinite loop in the fixpoint.--- The value-lazy `Map` defined in this module satisfies this property. However,--- if we make this `Map` value-strict using BangPatterns, StrictCheck will--- report a failure when `runMapTest` is executed.-iterSolution_spec :: Evaluation '[Key, Int, KMap] (Maybe Int) -> Maybe (Int, Int)-iterSolution_spec (Evaluation args demands dOut) =-  let I (Key evalK) = hd args-      I nIter       = hd (tl args)-      dInM          = hd (tl (tl demands))-      inM           = replaceThunk Empty (fromDemand @KMap dInM)-      evalV         = lookup inM evalK-  in  if (inM == Empty)   ||-         isBaseCase evalK ||-         nIter <= 0       ||-         isThunk evalV    ||-         isNothing evalV-      then Nothing-      else trace ("KeyD: " ++ show evalK) $-           trace ("InD: " ++ prettyDemand dInM) $-           trace ("OutD: " ++ prettyDemand @(Maybe Int) (E dOut)) $-           trace ("isT: " ++ (show . isThunk $ lookup inM evalK)) $-           Just evalK-  where isBaseCase (j, k) = j - 1 < 0 || k - weights !! j < 0+{-# LANGUAGE TemplateHaskell, BangPatterns, DerivingStrategies #-}
+
+{- | This module showcases another type of specification different from those in
+   "Test.StrictCheck.Examples.Lists". Here, we demonstrate that StrictCheck is
+   able to distinguish value-lazy maps from value-strict maps.
+
+   In this module, we first develop the solution of the Knapsack dynamic
+   programming problem by taking the fixpoint of a step function of the solution
+   table. We represent the solution table with a map, and write a specification
+   that is critical for the termination of this solution.
+-}
+module Test.StrictCheck.Examples.Map where
+
+import Prelude hiding (lookup)
+import Debug.Trace
+
+import qualified GHC.Generics as GHC
+import Generics.SOP (Generic, HasDatatypeInfo, NS(..), hd, tl)
+
+import Test.StrictCheck
+import Test.StrictCheck.TH
+
+import Data.Maybe
+import Data.Function
+
+import Test.QuickCheck
+
+-- | We roll our own map type to avoid dealing with abstract types.
+data Map k v = Bin (Map k v) k v (Map k v) -- ^ A node that contains a key value pair
+             | Empty                       -- ^ An empty node
+             deriving stock    (GHC.Generic, Show, Eq, Ord)
+             deriving anyclass (Generic, HasDatatypeInfo, Consume, Shaped)
+
+-- | A specialized map useful for knapsack. The pair of ints represent the two
+-- parameters to each knapsack sub-problem solved along the way. These two
+-- parameters determine the subsequence of items each sub-problem is concerned
+-- with, and the weight limit.
+type KMap = Map (Int, Int) Int
+
+$(derivePatternSynonyms ''Map)
+
+-- | This replaces the thunk in a map partial value with the `r` parameter. This
+-- is very similar to the `cap` function in the lists example.
+replaceThunk :: (Shaped k, Shaped v) => Map k v -> Map k v -> Map k v
+replaceThunk r m     | isThunk m = r
+replaceThunk _ Empty             = Empty
+replaceThunk r (Bin ml k v mr)   = Bin (replaceThunk r ml) k v (replaceThunk r mr)
+
+-- | A helper for building a map from a list of values.
+fromList :: [((Int, Int), Int)] -> KMap
+fromList = foldr (\(k, v) acc -> insert k v acc) Empty
+
+-- | A simplified insert that ignores rebalancing since rebalancing is not
+-- important for the spec we will write.
+insert :: (Ord k) => k -> v -> Map k v -> Map k v
+insert key value Empty = Bin Empty key value Empty
+insert key value (Bin ml k v mr) | key < k   = Bin (insert key value ml) k v mr
+                                 | key > k   = Bin ml k v (insert key value mr)
+                                 | otherwise = Bin ml key value mr
+
+-- | The lookup function specialized for knapsack.
+lookup :: KMap -> (Int, Int) -> Maybe Int
+lookup Empty _                        = Nothing
+lookup (Bin ml k' v mr) k | k == k'   = Just v
+                          | k <  k'   = lookup ml k
+                          | otherwise = lookup mr k
+
+-- | This function extracts all of the keys of a map.
+keys :: Map k v -> [k]
+keys Empty           = []
+keys (Bin ml k _ mr) = keys ml ++ [k] ++ keys mr
+
+-- | A lookup function that returns the default value `0` for keys that are not
+-- in the map. This saves us from doing repeated pattern matching when querying
+-- the solution table.
+(!) :: KMap -> (Int, Int) -> Int
+(!) m k = case lookup m k of
+            Nothing -> 0
+            Just v  -> v
+
+-- | Weight parameters to the knapsack problem.
+weights :: [Int]
+weights = [10, 20, 30]
+
+-- | Value parameters to the knapsack problem, note that this must be the same
+-- length as `weights`.
+values :: [Int]
+values = [60, 100, 120]
+
+-- | The weight limit of the knapsack problem.
+limit :: Int
+limit = 50
+
+-- | One step of the knapsack computation. This is a direct translation from the
+-- recurrence relation of the knapsack problem.
+solutionStep :: Map (Int, Int) Int -> Map (Int, Int) Int
+solutionStep soln =
+  fromList [((j, k), knapsack j k) | j <- [0 .. length weights-1], k <- [0 .. limit]]
+  where
+    knapsack j k = if j - 1 < 0 || k - weights !! j < 0
+                   then if j >= 0 && weights !! j <= k then values !! j else 0
+                   else max (soln ! (j-1, k))
+                            (soln ! (j-1, k - weights !! j) + values !! j)
+
+-- | The fixpoint of the recurrence relation, which is also the solution for the
+-- knapsack problem.
+solution :: Map (Int, Int) Int
+solution = fix solutionStep
+
+-- | A pattern synonym for extracting demands of each component from the demand
+-- of a pair.
+pattern Pair' :: Demand a -> Demand b -> Demand (a, b)
+pattern Pair' x y = Wrap (Eval (GS (Z (x :* y :* Nil))))
+
+-- | This function computes the nth pre-fixpoint of the knapsack solution, and
+-- looks up the value at the specified cell from the pre-fixpoint.
+iterSolution :: (Int, Int) -> Int -> Map (Int, Int) Int -> Maybe Int
+iterSolution k n soln = lookup m k
+  where m | n <= 0    = soln
+          | otherwise = (iterate solutionStep soln) !! n
+
+-- | This is the same as `iterSolution`, but uses a newtype wrapper for the
+-- index into the map since we want to write a customized `Arbitrary` instance
+-- for `Key`.
+iterSolutionWithKey :: Key -> Int -> Map (Int, Int) Int -> Maybe Int
+iterSolutionWithKey (Key k) = iterSolution k
+
+-- | The newtype wrapper of index into the knapsack solution table.
+newtype Key = Key { getKey :: (Int, Int) }
+  deriving stock    (GHC.Generic, Show, Eq, Ord)
+  deriving anyclass (Generic, HasDatatypeInfo, Consume, Shaped)
+
+-- | The customized generator for `Key` that only generates valid keys given the
+-- problem parameters.
+instance Arbitrary Key where
+  -- Just to make sure keys are within the parameters of the problem
+  arbitrary = fmap Key $
+    (,) <$> elements [0 .. length weights - 1] <*> elements [0 .. limit]
+
+-- | The customized generator for solution tables that only generates valid
+-- pre-fixpoints.
+instance Arbitrary KMap where
+  -- I need to generate only valid pre-fixpoints, which is either
+  -- Empty (iterated 0 times), or iterate once on Empty, or twice, and
+  -- so on
+  arbitrary = do
+    NonNegative n <- arbitrary
+    return $ (iterate solutionStep Empty) !! n
+
+-- | A dummy produce instance for the solution table.
+instance Produce KMap where
+  -- I don't need lazy functions on KMaps. Since the spec only checks
+  -- whether a particular entry in the KMap is evaluated or not.
+  produce = arbitrary
+
+-- | A dummy produce instance for the index into the solution table.
+instance Produce Key where
+  -- I don't need lazy functions on keys either.
+  produce = arbitrary
+
+-- | This IO action ties the spec together with everything built so far, and
+-- runs the StrictCheck randomized testing framework.
+runMapTest :: IO ()
+runMapTest = strictCheckWithResults
+               stdArgs{maxSize=100, maxSuccess=1000}
+               shrinkViaArbitrary
+               genViaProduce
+               strictnessViaSized
+               iterSolution_spec
+               iterSolutionWithKey >>= print
+
+-- | This is the specification that establishes a property important for the
+-- termination of `solution`: given any pre-fixpoint of `pre-solution`, forcing
+-- the value at pre-solution[i][j] should not induce a demand at the (i, j) cell
+-- of the input that steps to pre-solution, since otherwise this would be an
+-- infinite loop in the fixpoint.
+-- The value-lazy `Map` defined in this module satisfies this property. However,
+-- if we make this `Map` value-strict using BangPatterns, StrictCheck will
+-- report a failure when `runMapTest` is executed.
+iterSolution_spec :: Evaluation '[Key, Int, KMap] (Maybe Int) -> Maybe (Int, Int)
+iterSolution_spec (Evaluation args demands dOut) =
+  let I (Key evalK) = hd args
+      I nIter       = hd (tl args)
+      dInM          = hd (tl (tl demands))
+      inM           = replaceThunk Empty (fromDemand @KMap dInM)
+      evalV         = lookup inM evalK
+  in  if (inM == Empty)   ||
+         isBaseCase evalK ||
+         nIter <= 0       ||
+         isThunk evalV    ||
+         isNothing evalV
+      then Nothing
+      else trace ("KeyD: " ++ show evalK) $
+           trace ("InD: " ++ prettyDemand dInM) $
+           trace ("OutD: " ++ prettyDemand @(Maybe Int) (E dOut)) $
+           trace ("isT: " ++ (show . isThunk $ lookup inM evalK)) $
+           Just evalK
+  where isBaseCase (j, k) = j - 1 < 0 || k - weights !! j < 0

@@ -1,58 +1,58 @@-{-| __Internal module__: This module does not make any stability guarantees, and-    may not adhere to the PVP.--    This module implements the rose-tree data structure used by StrictCheck to-    monomorphize inputs to functions. We decouple the consumption of input from-    the production of output by converting any input to an @Input@: a lazily-    constructed rose tree with nodes each containing a @(Gen a -> Gen a)@ which-    captures a random perturbation associated with the shape of the value-    consumed. The tree-shape of an @Input@ matches that of the entire consumed-    value, and evaluating any subpart of it forces the evaluation of the-    corresponding part of the original value.--}-module Test.StrictCheck.Internal.Inputs-  ( Variant(..)-  , Input(..)-  , Inputs(..)-  , draw-  , destruct-  ) where--import Test.QuickCheck (Gen)-------------------------------------------------------- The core user-facing types: Input and Inputs --------------------------------------------------------- | A variant which can be applied to any generator--kept in a newtype to get--- around lack of impredicativity.-newtype Variant-  = Variant { vary :: forall a. Gen a -> Gen a }--instance Semigroup Variant where-  v <> w = Variant (vary v . vary w)--instance Monoid Variant where-  mappend = (<>)-  mempty = Variant id---- | A tree representing all possible destruction sequences for a value--- Unfolding the contained lists forces a particular random control path--- for destructing the datatype.-data Input-  = Input Variant [Input]  -- ^ Not exposed in safe API---- | A list of inputs given to a function, in abstract form. This lazy structure--- is evaluated piecewise during the course of producing a function, thus--- triggering the partial evaluation of the original input to the function.-newtype Inputs-  = Inputs [Input]  -- ^ Not exposed in safe API---- | Extract the list of @Input@s from an @Inputs@-destruct :: Inputs -> [Input]-destruct (Inputs is) = is---- | Extract the entropy and subfield-@Input@s from a given @Input@-draw :: Input -> (Variant, [Input])-draw (Input v is) = (v, is)+{-| __Internal module__: This module does not make any stability guarantees, and
+    may not adhere to the PVP.
+
+    This module implements the rose-tree data structure used by StrictCheck to
+    monomorphize inputs to functions. We decouple the consumption of input from
+    the production of output by converting any input to an @Input@: a lazily
+    constructed rose tree with nodes each containing a @(Gen a -> Gen a)@ which
+    captures a random perturbation associated with the shape of the value
+    consumed. The tree-shape of an @Input@ matches that of the entire consumed
+    value, and evaluating any subpart of it forces the evaluation of the
+    corresponding part of the original value.
+-}
+module Test.StrictCheck.Internal.Inputs
+  ( Variant(..)
+  , Input(..)
+  , Inputs(..)
+  , draw
+  , destruct
+  ) where
+
+import Test.QuickCheck (Gen)
+
+
+--------------------------------------------------
+-- The core user-facing types: Input and Inputs --
+--------------------------------------------------
+
+-- | A variant which can be applied to any generator--kept in a newtype to get
+-- around lack of impredicativity.
+newtype Variant
+  = Variant { vary :: forall a. Gen a -> Gen a }
+
+instance Semigroup Variant where
+  v <> w = Variant (vary v . vary w)
+
+instance Monoid Variant where
+  mappend = (<>)
+  mempty = Variant id
+
+-- | A tree representing all possible destruction sequences for a value
+-- Unfolding the contained lists forces a particular random control path
+-- for destructing the datatype.
+data Input
+  = Input Variant [Input]  -- ^ Not exposed in safe API
+
+-- | A list of inputs given to a function, in abstract form. This lazy structure
+-- is evaluated piecewise during the course of producing a function, thus
+-- triggering the partial evaluation of the original input to the function.
+newtype Inputs
+  = Inputs [Input]  -- ^ Not exposed in safe API
+
+-- | Extract the list of @Input@s from an @Inputs@
+destruct :: Inputs -> [Input]
+destruct (Inputs is) = is
+
+-- | Extract the entropy and subfield-@Input@s from a given @Input@
+draw :: Input -> (Variant, [Input])
+draw (Input v is) = (v, is)

@@ -1,35 +1,35 @@-{-| __Internal module__: This module does not make any stability guarantees, and-    may not adhere to the PVP.--    This module defines the 'Omega' type, which has only one inhabitant: the-    infinite chain of successors. Any function which consumes an @Omega@ is-    functionally equivalent to any other; likewise for those which produce an-    @Omega@. However, they may have radically differing strictness behaviors. It-    is for this reason that we have use for this type in the course of random-    example generation.--}-module Test.StrictCheck.Internal.Omega-  ( Omega(..)-  , forceOmega-  ) where--import Test.StrictCheck.Produce-import Test.StrictCheck.Shaped--import qualified GHC.Generics as GHC-import Generics.SOP---- | The type with one inhabitant: the infinite chain of successors-data Omega = Succ Omega-  deriving (GHC.Generic, Generic, HasDatatypeInfo, Shaped)--instance Produce Omega where-  produce = Succ <$> recur---- | Evaluate @n@ constructors of a given @Omega@ value, returning unit-forceOmega :: Int -> Omega -> ()-forceOmega n o-  | n <= 0-  = ()-  | Succ o' <- o-  = forceOmega (n - 1) o'+{-| __Internal module__: This module does not make any stability guarantees, and
+    may not adhere to the PVP.
+
+    This module defines the 'Omega' type, which has only one inhabitant: the
+    infinite chain of successors. Any function which consumes an @Omega@ is
+    functionally equivalent to any other; likewise for those which produce an
+    @Omega@. However, they may have radically differing strictness behaviors. It
+    is for this reason that we have use for this type in the course of random
+    example generation.
+-}
+module Test.StrictCheck.Internal.Omega
+  ( Omega(..)
+  , forceOmega
+  ) where
+
+import Test.StrictCheck.Produce
+import Test.StrictCheck.Shaped
+
+import qualified GHC.Generics as GHC
+import Generics.SOP
+
+-- | The type with one inhabitant: the infinite chain of successors
+data Omega = Succ Omega
+  deriving (GHC.Generic, Generic, HasDatatypeInfo, Shaped)
+
+instance Produce Omega where
+  produce = Succ <$> recur
+
+-- | Evaluate @n@ constructors of a given @Omega@ value, returning unit
+forceOmega :: Int -> Omega -> ()
+forceOmega n o
+  | n <= 0
+  = ()
+  | Succ o' <- o
+  = forceOmega (n - 1) o'

@@ -1,98 +1,98 @@-{-| __Internal module__: This module does not make any stability guarantees, and-    may not adhere to the PVP.--    This module defines several utilities useful for shrinking demands and-    evaluations.--    Of these, only 'axialShrinks' and 'fairInterleave' are used by StrictCheck;-    nevertheless, we expose the 'DZipper' type and its associated functions in-    this internal module just in case.--}-module Test.StrictCheck.Internal.Shrink-  ( Shrink(..)-  , axialShrinks-  , fairInterleave-  -- * CPS-based zippers through heterogeneous products-  , DZipper(..)-  , next-  , positions-  , dzipper-  , dzip-  ) where--import Generics.SOP-import Data.Functor.Product---- Fair n-ary axial shrinking (a.k.a. *fair* generalization of shrink on tuples)---- | Newtype allowing us to construct 'NP' n-ary products of shrinkers-newtype Shrink a-  = Shrink (a -> [a])---- | A @DZipper@ is a suspended traversal through a non-empty 'NP' n-ary product------ The position of the traversal within that product is existentially--- quantified.-data DZipper f whole where-  DZipper :: (NP f (c : rs) -> NP f whole)-          -> f c-          -> NP f rs-          -> DZipper f whole---- | Step one to the right in a @DZipper@, returning @Nothing@ if this is not--- possible-next :: DZipper f whole -> Maybe (DZipper f whole)-next (DZipper _  _       Nil)  = Nothing-next (DZipper ls c (r :* rs')) =-  Just $ DZipper (ls . (c :*)) r rs'---- | Given an n-ary product of @xs@, get a list of @DZipper@s, each focused in--- sequence on the values of the input product------ This is similar to the @duplicate@ operation on comonads.-positions :: NP f xs -> [DZipper f xs]-positions (dzipper -> mstart) =-  maybe [] go mstart-  where-    go start = start : maybe [] go (next start)---- | Convert an n-ary product into a @DZipper@, returning @Nothing@ if the--- input product is empty-dzipper :: NP f xs -> Maybe (DZipper f xs)-dzipper       Nil = Nothing-dzipper (c :* rs) = Just $ DZipper id c rs---- | Collapse a @DZipper@ back into the n-ary product it represents-dzip :: DZipper f xs -> NP f xs-dzip (DZipper ls c rs) = ls (c :* rs)---- | Given a list of shrinkers and a list of values-to-be-shrunk, generate--- a list of shrunken lists-of-values, each inner list being one potential--- "axis" for shrinking------ That is, the first element of the result is all the ways the original--- product could be shrunken by /only/ shrinking its first component, etc.-axialShrinks :: SListI xs => NP Shrink xs -> NP I xs -> [[NP I xs]]-axialShrinks shrinks xs =-  fmap (hliftA (\(Pair _ v) -> v) . dzip)-  . centerIter <$> positions withShrinks-  where-    iter (Pair (Shrink s) (I v)) =-      Pair (Shrink s) . I <$> (s v)--    centerIter (DZipper ls c rs) =-      map (\c' -> DZipper ls c' rs) (iter c)--    withShrinks =-      hliftA2 Pair shrinks xs---- | Fairly interleave a list of lists in a round-robin fashion-fairInterleave :: [[a]] -> [a]-fairInterleave = roundRobin id-  where-    roundRobin k ((x : xs) : xss) = x : roundRobin (k . (xs :)) xss-    roundRobin k ([      ] : xss) = roundRobin k xss-    roundRobin k [              ] =-      case k [] of-        [ ] -> []-        xss -> roundRobin id xss+{-| __Internal module__: This module does not make any stability guarantees, and
+    may not adhere to the PVP.
+
+    This module defines several utilities useful for shrinking demands and
+    evaluations.
+
+    Of these, only 'axialShrinks' and 'fairInterleave' are used by StrictCheck;
+    nevertheless, we expose the 'DZipper' type and its associated functions in
+    this internal module just in case.
+-}
+module Test.StrictCheck.Internal.Shrink
+  ( Shrink(..)
+  , axialShrinks
+  , fairInterleave
+  -- * CPS-based zippers through heterogeneous products
+  , DZipper(..)
+  , next
+  , positions
+  , dzipper
+  , dzip
+  ) where
+
+import Generics.SOP
+import Data.Functor.Product
+
+-- Fair n-ary axial shrinking (a.k.a. *fair* generalization of shrink on tuples)
+
+-- | Newtype allowing us to construct 'NP' n-ary products of shrinkers
+newtype Shrink a
+  = Shrink (a -> [a])
+
+-- | A @DZipper@ is a suspended traversal through a non-empty 'NP' n-ary product
+--
+-- The position of the traversal within that product is existentially
+-- quantified.
+data DZipper f whole where
+  DZipper :: (NP f (c : rs) -> NP f whole)
+          -> f c
+          -> NP f rs
+          -> DZipper f whole
+
+-- | Step one to the right in a @DZipper@, returning @Nothing@ if this is not
+-- possible
+next :: DZipper f whole -> Maybe (DZipper f whole)
+next (DZipper _  _       Nil)  = Nothing
+next (DZipper ls c (r :* rs')) =
+  Just $ DZipper (ls . (c :*)) r rs'
+
+-- | Given an n-ary product of @xs@, get a list of @DZipper@s, each focused in
+-- sequence on the values of the input product
+--
+-- This is similar to the @duplicate@ operation on comonads.
+positions :: NP f xs -> [DZipper f xs]
+positions (dzipper -> mstart) =
+  maybe [] go mstart
+  where
+    go start = start : maybe [] go (next start)
+
+-- | Convert an n-ary product into a @DZipper@, returning @Nothing@ if the
+-- input product is empty
+dzipper :: NP f xs -> Maybe (DZipper f xs)
+dzipper       Nil = Nothing
+dzipper (c :* rs) = Just $ DZipper id c rs
+
+-- | Collapse a @DZipper@ back into the n-ary product it represents
+dzip :: DZipper f xs -> NP f xs
+dzip (DZipper ls c rs) = ls (c :* rs)
+
+-- | Given a list of shrinkers and a list of values-to-be-shrunk, generate
+-- a list of shrunken lists-of-values, each inner list being one potential
+-- "axis" for shrinking
+--
+-- That is, the first element of the result is all the ways the original
+-- product could be shrunken by /only/ shrinking its first component, etc.
+axialShrinks :: SListI xs => NP Shrink xs -> NP I xs -> [[NP I xs]]
+axialShrinks shrinks xs =
+  fmap (hliftA (\(Pair _ v) -> v) . dzip)
+  . centerIter <$> positions withShrinks
+  where
+    iter (Pair (Shrink s) (I v)) =
+      Pair (Shrink s) . I <$> (s v)
+
+    centerIter (DZipper ls c rs) =
+      map (\c' -> DZipper ls c' rs) (iter c)
+
+    withShrinks =
+      hliftA2 Pair shrinks xs
+
+-- | Fairly interleave a list of lists in a round-robin fashion
+fairInterleave :: [[a]] -> [a]
+fairInterleave = roundRobin id
+  where
+    roundRobin k ((x : xs) : xss) = x : roundRobin (k . (xs :)) xss
+    roundRobin k ([      ] : xss) = roundRobin k xss
+    roundRobin k [              ] =
+      case k [] of
+        [ ] -> []
+        xss -> roundRobin id xss

@@ -1,23 +1,23 @@-{-| __Internal module__: This module does not make any stability guarantees, and-    may not adhere to the PVP.--    This module defines the internal exception type used to implement the-    to/from-Demand methods in "Test.StrictCheck.Demand". We don't export this-    type from the library to discourage users from interacting with this-    mechanism.--}--module Test.StrictCheck.Internal.Unevaluated-  ( Unevaluated(..)-  ) where--import Control.Exception---- | In @fromDemand@, this exception is (purely, lazily) thrown whenever a--- @Thunk@ is encountered. In @toDemand@, it is caught and converted back to a--- @Thunk@.-data Unevaluated-  = Unevaluated-  deriving Show--instance Exception Unevaluated+{-| __Internal module__: This module does not make any stability guarantees, and
+    may not adhere to the PVP.
+
+    This module defines the internal exception type used to implement the
+    to/from-Demand methods in "Test.StrictCheck.Demand". We don't export this
+    type from the library to discourage users from interacting with this
+    mechanism.
+-}
+
+module Test.StrictCheck.Internal.Unevaluated
+  ( Unevaluated(..)
+  ) where
+
+import Control.Exception
+
+-- | In @fromDemand@, this exception is (purely, lazily) thrown whenever a
+-- @Thunk@ is encountered. In @toDemand@, it is caught and converted back to a
+-- @Thunk@.
+data Unevaluated
+  = Unevaluated
+  deriving Show
+
+instance Exception Unevaluated

@@ -1,148 +1,148 @@-{-| This module implements the core "trick" of StrictCheck: observing the-    demand behavior of a function in a purely functional way.--    All the functions in this module are safe and referentially transparent.--    Observing the evaluation of a function using these functions incurs at most-    a small constant multiple of overhead compared to just executing the function-    with no observation.--}-module Test.StrictCheck.Observe-  ( observe1-  , observe-  , observeNP-  ) where--import Data.Bifunctor-import Data.Functor.Product--import Generics.SOP hiding (Shape)--import Test.StrictCheck.Curry hiding (curry, uncurry)-import Test.StrictCheck.Shaped-import Test.StrictCheck.Observe.Unsafe-import Test.StrictCheck.Demand----------------------------------------------------------- Observing demand behavior of arbitrary functions ------------------------------------------------------------- | Observe the demand behavior------ * in a given evaluation context,--- * of a given __unary function__,--- * called upon a given input,------ returning a pair of------ * the demand on its output exerted by the evaluation context, and--- * the demand on its input this induced------ Suppose we want to see how strict @reverse@ is when we evaluate its result--- to weak-head normal form:------ >>> (b, a) = observe1 (`seq` ()) (reverse @Int) [1, 2, 3]--- >>> printDemand b  -- output demand--- _ : _--- >>> printDemand a  -- input demand--- _ : _ : _ : _ : []------ This tells us that our context did indeed evaluate the result of @reverse@--- to force only its first constructor, and that doing so required the entire--- spine of the list to be evaluated, but did not evaluate any of its elements.-{-# NOINLINE observe1 #-}-observe1-  :: (Shaped a, Shaped b)-  => (b -> ()) -> (a -> b) -> a -> (Demand b, Demand a)-observe1 context function input =-  let (input', inputD)  =-        instrument input              -- (1)-      (result', resultD) =-        instrument (function input')  -- (2)-  in let !_ = context result'         -- (3)-  in (resultD, inputD)                -- (4)-  -  -- NOTE: The observation function:-  -- (1) instruments the input-  -- (2) instruments the result of the function applied to the input-  -- (3) evaluates the instrumented result of the function in the context, and-  -- (4) returns the observed demands on the result and the input.---- | Observe the demand behavior------ * in a given evaluation context--- * of a given __uncurried n-ary function__ (taking as input an n-ary--- product of inputs represented as an 'NP' 'I' from "Generics.SOP")--- * called upon all of its inputs (provided as curried ordinary inputs),------ returning a pair of------ * the demand on its output exerted by the evaluation context, and--- * the demands on its inputs this induced, represented as an 'NP' 'Demand'--- from "Generics.SOP"------ This is mostly useful for implementing the internals of StrictCheck;--- 'observe' is more ergonomic for exploration by end-users.-{-# NOINLINE observeNP #-}-observeNP-  :: (All Shaped inputs, Shaped result)-  => (result -> ())-  -> (NP I inputs -> result)-  -> NP I inputs-  -> ( Demand result-     , NP Demand inputs )-observeNP context function inputs =-  let entangled =-        hcliftA-          (Proxy @Shaped)-          (uncurry Pair . first I . instrument . unI)-          inputs-      (inputs', inputsD) =-        (hliftA (\(Pair r _) -> r) entangled,-          hliftA (\(Pair _ l) -> l) entangled)-      (result', resultD) = instrument (function inputs')-  in let !_ = context result'-  in (resultD, inputsD)---- | Observe the demand behavior------ * in a given evaluation context--- * of a given __curried n-ary function__--- * called upon all of its inputs (provided as curried ordinary inputs),------ returning a pair of------ * the demand on its output exerted by the evaluation context, and--- * the demands on its inputs this induced, represented as an 'NP' 'Demand'--- from "Generics.SOP"------ This function is variadic and curried: it takes @n + 2@ arguments, where--- @n@ is the total number of arguments taken by the observed function.------ Suppose we want to see how strict @zipWith (*)@ is when we evaluate its--- result completely (to normal form):------ >>> productZip = zipWith ((*) @Int)--- >>> (zs, (xs :* ys :* Nil)) = observe normalize productZip [10, 20] [30, 40]--- >>> printDemand zs  -- output demand--- 300 : 800 : []--- >>> printDemand xs  -- input demand #1--- 10 : 20 : []--- >>> printDemand ys  -- input demand #2--- 30 : 40 : _------ If you haven't thought very carefully about the strictness behavior of @zip@,--- this may be a surprising result; this is part of the fun!-observe-  :: ( All Shaped (Args function)-     , Shaped (Result function)-     , Curry (Args function) )-  => (Result function -> ())-  -> function-  -> Args function-  ⋯-> ( Demand (Result function)-       , NP Demand (Args function) )-observe context function =-  curryAll (observeNP context (uncurryAll function))---- NOTE: We don't need a NOINLINE annotation here because this wraps observeNP.+{-| This module implements the core "trick" of StrictCheck: observing the
+    demand behavior of a function in a purely functional way.
+
+    All the functions in this module are safe and referentially transparent.
+
+    Observing the evaluation of a function using these functions incurs at most
+    a small constant multiple of overhead compared to just executing the function
+    with no observation.
+-}
+module Test.StrictCheck.Observe
+  ( observe1
+  , observe
+  , observeNP
+  ) where
+
+import Data.Bifunctor
+import Data.Functor.Product
+
+import Generics.SOP hiding (Shape)
+
+import Test.StrictCheck.Curry hiding (curry, uncurry)
+import Test.StrictCheck.Shaped
+import Test.StrictCheck.Observe.Unsafe
+import Test.StrictCheck.Demand
+
+------------------------------------------------------
+-- Observing demand behavior of arbitrary functions --
+------------------------------------------------------
+
+-- | Observe the demand behavior
+--
+-- * in a given evaluation context,
+-- * of a given __unary function__,
+-- * called upon a given input,
+--
+-- returning a pair of
+--
+-- * the demand on its output exerted by the evaluation context, and
+-- * the demand on its input this induced
+--
+-- Suppose we want to see how strict @reverse@ is when we evaluate its result
+-- to weak-head normal form:
+--
+-- >>> (b, a) = observe1 (`seq` ()) (reverse @Int) [1, 2, 3]
+-- >>> printDemand b  -- output demand
+-- _ : _
+-- >>> printDemand a  -- input demand
+-- _ : _ : _ : _ : []
+--
+-- This tells us that our context did indeed evaluate the result of @reverse@
+-- to force only its first constructor, and that doing so required the entire
+-- spine of the list to be evaluated, but did not evaluate any of its elements.
+{-# NOINLINE observe1 #-}
+observe1
+  :: (Shaped a, Shaped b)
+  => (b -> ()) -> (a -> b) -> a -> (Demand b, Demand a)
+observe1 context function input =
+  let (input', inputD)  =
+        instrument input              -- (1)
+      (result', resultD) =
+        instrument (function input')  -- (2)
+  in let !_ = context result'         -- (3)
+  in (resultD, inputD)                -- (4)
+  
+  -- NOTE: The observation function:
+  -- (1) instruments the input
+  -- (2) instruments the result of the function applied to the input
+  -- (3) evaluates the instrumented result of the function in the context, and
+  -- (4) returns the observed demands on the result and the input.
+
+-- | Observe the demand behavior
+--
+-- * in a given evaluation context
+-- * of a given __uncurried n-ary function__ (taking as input an n-ary
+-- product of inputs represented as an 'NP' 'I' from "Generics.SOP")
+-- * called upon all of its inputs (provided as curried ordinary inputs),
+--
+-- returning a pair of
+--
+-- * the demand on its output exerted by the evaluation context, and
+-- * the demands on its inputs this induced, represented as an 'NP' 'Demand'
+-- from "Generics.SOP"
+--
+-- This is mostly useful for implementing the internals of StrictCheck;
+-- 'observe' is more ergonomic for exploration by end-users.
+{-# NOINLINE observeNP #-}
+observeNP
+  :: (All Shaped inputs, Shaped result)
+  => (result -> ())
+  -> (NP I inputs -> result)
+  -> NP I inputs
+  -> ( Demand result
+     , NP Demand inputs )
+observeNP context function inputs =
+  let entangled =
+        hcliftA
+          (Proxy @Shaped)
+          (uncurry Pair . first I . instrument . unI)
+          inputs
+      (inputs', inputsD) =
+        (hliftA (\(Pair r _) -> r) entangled,
+          hliftA (\(Pair _ l) -> l) entangled)
+      (result', resultD) = instrument (function inputs')
+  in let !_ = context result'
+  in (resultD, inputsD)
+
+-- | Observe the demand behavior
+--
+-- * in a given evaluation context
+-- * of a given __curried n-ary function__
+-- * called upon all of its inputs (provided as curried ordinary inputs),
+--
+-- returning a pair of
+--
+-- * the demand on its output exerted by the evaluation context, and
+-- * the demands on its inputs this induced, represented as an 'NP' 'Demand'
+-- from "Generics.SOP"
+--
+-- This function is variadic and curried: it takes @n + 2@ arguments, where
+-- @n@ is the total number of arguments taken by the observed function.
+--
+-- Suppose we want to see how strict @zipWith (*)@ is when we evaluate its
+-- result completely (to normal form):
+--
+-- >>> productZip = zipWith ((*) @Int)
+-- >>> (zs, (xs :* ys :* Nil)) = observe normalize productZip [10, 20] [30, 40]
+-- >>> printDemand zs  -- output demand
+-- 300 : 800 : []
+-- >>> printDemand xs  -- input demand #1
+-- 10 : 20 : []
+-- >>> printDemand ys  -- input demand #2
+-- 30 : 40 : _
+--
+-- If you haven't thought very carefully about the strictness behavior of @zip@,
+-- this may be a surprising result; this is part of the fun!
+observe
+  :: ( All Shaped (Args function)
+     , Shaped (Result function)
+     , Curry (Args function) )
+  => (Result function -> ())
+  -> function
+  -> Args function
+  ⋯-> ( Demand (Result function)
+       , NP Demand (Args function) )
+observe context function =
+  curryAll (observeNP context (uncurryAll function))
+
+-- NOTE: We don't need a NOINLINE annotation here because this wraps observeNP.

@@ -1,76 +1,76 @@-{-| This module defines the underlying __unsafe__ primitives StrictCheck uses-    to implement purely functional observation of evaluation.--    The "functions" in this module are __not referentially transparent__!--}-module Test.StrictCheck.Observe.Unsafe where--import System.IO.Unsafe-import Data.IORef--import Data.Bifunctor-import Generics.SOP (I(..), unI)--import Test.StrictCheck.Shaped-import Test.StrictCheck.Demand---- | From some value of any type, produce a pair: a copy of the original value,--- and a 'Thunk' of that same type, with their values determined by the--- /order/ in which their values themselves are evaluated------ If the copy of the value is evaluated to weak-head normal form before the--- returned @Thunk@, then any future inspection of the @Thunk@ will show that it--- is equal to the original value wrapped in an @Eval@. However, if the copy of--- the value is /not/ evaluated by the time the @Thunk@ is evaluated, any future--- inspection of the @Thunk@ will show that it is equal to @Thunk@.------ A picture may be worth 1000 words:------ >>> x = "hello," ++ " world"--- >>> (x', t) = entangle x--- >>> x'--- "hello, world"--- >>> t--- Eval "hello, world"------ >>> x = "hello," ++ " world"--- >>> (x', t) = entangle x--- >>> t--- Thunk--- >>> x'--- "hello, world"--- >>> t--- Thunk-{-# NOINLINE entangle #-}-entangle :: forall a. a -> (a, Thunk a)-entangle a =-  unsafePerformIO $ do-    ref <- newIORef Thunk-    return ( unsafePerformIO $ do-               writeIORef ref (Eval a)-               return a-           , unsafePerformIO $ readIORef ref )---- | Recursively 'entangle' an @a@, producing not merely a @Thunk@, but an--- entire @Demand@ which is piecewise entangled with that value. Whatever--- portion of the entangled value is evaluated before the corresponding portion--- of the returned @Demand@ will be represented in the shape of that @Demand@.--- However, any part of the returned @Demand@ which is evaluated before the--- corresponding portion of the entangled value will be forever equal to--- @Thunk@.------ The behavior of this function is even more tricky to predict than that of--- 'entangle', especially when evaluation of the entangled value and the--- corresponding @Demand@ happen at the same time. In StrictCheck, all--- evaluation of the entangled value occurs before any evaluation of the--- @Demand@; we never interleave their evaluation.-{-# NOINLINE instrument #-}-instrument :: Shaped a => a -> (a, Demand a)-instrument =-  first (fuse unI)-  . unzipWith entangle'-  . interleave I-  where-    entangle' :: I x -> (I x, Thunk x)-    entangle' =-      first I . entangle . unI+{-| This module defines the underlying __unsafe__ primitives StrictCheck uses
+    to implement purely functional observation of evaluation.
+
+    The "functions" in this module are __not referentially transparent__!
+-}
+module Test.StrictCheck.Observe.Unsafe where
+
+import System.IO.Unsafe
+import Data.IORef
+
+import Data.Bifunctor
+import Generics.SOP (I(..), unI)
+
+import Test.StrictCheck.Shaped
+import Test.StrictCheck.Demand
+
+-- | From some value of any type, produce a pair: a copy of the original value,
+-- and a 'Thunk' of that same type, with their values determined by the
+-- /order/ in which their values themselves are evaluated
+--
+-- If the copy of the value is evaluated to weak-head normal form before the
+-- returned @Thunk@, then any future inspection of the @Thunk@ will show that it
+-- is equal to the original value wrapped in an @Eval@. However, if the copy of
+-- the value is /not/ evaluated by the time the @Thunk@ is evaluated, any future
+-- inspection of the @Thunk@ will show that it is equal to @Thunk@.
+--
+-- A picture may be worth 1000 words:
+--
+-- >>> x = "hello," ++ " world"
+-- >>> (x', t) = entangle x
+-- >>> x'
+-- "hello, world"
+-- >>> t
+-- Eval "hello, world"
+--
+-- >>> x = "hello," ++ " world"
+-- >>> (x', t) = entangle x
+-- >>> t
+-- Thunk
+-- >>> x'
+-- "hello, world"
+-- >>> t
+-- Thunk
+{-# NOINLINE entangle #-}
+entangle :: forall a. a -> (a, Thunk a)
+entangle a =
+  unsafePerformIO $ do
+    ref <- newIORef Thunk
+    return ( unsafePerformIO $ do
+               writeIORef ref (Eval a)
+               return a
+           , unsafePerformIO $ readIORef ref )
+
+-- | Recursively 'entangle' an @a@, producing not merely a @Thunk@, but an
+-- entire @Demand@ which is piecewise entangled with that value. Whatever
+-- portion of the entangled value is evaluated before the corresponding portion
+-- of the returned @Demand@ will be represented in the shape of that @Demand@.
+-- However, any part of the returned @Demand@ which is evaluated before the
+-- corresponding portion of the entangled value will be forever equal to
+-- @Thunk@.
+--
+-- The behavior of this function is even more tricky to predict than that of
+-- 'entangle', especially when evaluation of the entangled value and the
+-- corresponding @Demand@ happen at the same time. In StrictCheck, all
+-- evaluation of the entangled value occurs before any evaluation of the
+-- @Demand@; we never interleave their evaluation.
+{-# NOINLINE instrument #-}
+instrument :: Shaped a => a -> (a, Demand a)
+instrument =
+  first (fuse unI)
+  . unzipWith entangle'
+  . interleave I
+  where
+    entangle' :: I x -> (I x, Thunk x)
+    entangle' =
+      first I . entangle . unI

@@ -1,229 +1,231 @@-{-| This module defines the 'Produce' typeclass, used for generating random-    values for testing in StrictCheck.--    'Produce' is a strict generalization of "Test.QuickCheck"'s 'Arbitrary'-    typeclass. Paired with 'Consume' (a generalization of 'CoArbitrary') it can-    be used to create random non-strict functions, whose strictness behavior is-    dependent on the values given to them.--}--module Test.StrictCheck.Produce-  ( Produce(..)-  -- * Tools for writing 'Produce' instances-  , recur-  , build-  -- * Producing non-strict functions-  , returning-  , variadic-  -- * Integration with "Test.QuickCheck"'s @Arbitrary@-  , Lazy(..)-  , freely-  -- * Abstract types representing input to a function-  , Input-  , Inputs-  -- * The traversal distribution for processing @Input@s-  , draws-  ) where--import Test.QuickCheck hiding (variant)-import Test.QuickCheck.Gen.Unsafe--import Test.StrictCheck.Internal.Inputs-import Test.StrictCheck.Consume-import Test.StrictCheck.Curry--import Generics.SOP-import Data.Complex-import Data.Monoid ((<>))------------------------------------------------------------- The user interface for creating Produce instances -------------------------------------------------------------- TODO: parameterize over destruction pattern?---- | Produce an arbitrary value of type @b@, such that destructing that value--- incrementally evaluates some input to a function.------ Writing instances of @Produce@ is very similar to writing instances of--- QuickCheck's 'Arbitrary'. The distinction: when making a recursive call to--- produce a subfield of a structure, __always__ use 'build' or 'recur', and--- __never__ a direct call to 'produce' itself. This ensures that the input can--- potentially be demanded at any step of evaluation of the produced value.------ If, in the course of generating a value of type @b@, you need to generate a--- random value of some other type, which is /not/ going to be a subpart of the--- resultant @b@ (e.g. a length or depth), use a direct call to @arbitrary@ or--- some other generator which does not consume input.------ An example instance of @Produce@:------ > data D a--- >   = X a--- >   | Y [Int]--- >--- > instance Produce a => Produce (D a) where--- >   produce =--- >     oneof [ fmap X recur--- >           , fmap Y recur--- >           ]-class Produce b where-  produce :: (?inputs::Inputs) => Gen b--theInputs :: (?inputs::Inputs) => [Input]-theInputs = destruct ?inputs---- | Given an input-consuming producer, wrap it in an outer layer of input--- consumption, so that this consumption can be interleaved when the producer is--- called recursively to generate a subfield of a larger produced datatype.-build :: (?inputs::Inputs) => ((?inputs::Inputs) => Gen a) -> Gen a-build gen = do-  (v, is') <- draws theInputs-  vary v $ let ?inputs = Inputs is' in gen---- | Destruct some inputs to generate an output. This function handles the--- interleaving of input destruction with output construction. When producing a--- data type, it should be called to produce each subfield -- *not* produce--- itself.-recur :: (Produce a, ?inputs::Inputs) => Gen a-recur = build produce--------------------------------------------- How to make random lazy functions ---------------------------------------------- NOTE: This instance must be defined in this module, as it has to break the--- abstraction of the Inputs type. No other instance needs to break this.--- Incidentally, it also must break Gen's abstraction barrier, because it needs--- to use promote to make a function.--instance (Consume a, Produce b) => Produce (a -> b) where-  produce = returning produce---- | Create an input-consuming producer of input-consuming functions, given an--- input-consuming producer for results of that function.-returning-  :: (Consume a, ?inputs::Inputs)-  => ((?inputs::Inputs) => Gen b)-  -> Gen (a -> b)-returning out =-  promote $ \a ->-    let ?inputs = Inputs (consume a : theInputs)-    in build out---- | Create an input-consuming producer of input-consuming functions, of any--- arity. This will usually be used in conjuntion with type application, to--- specify the type(s) of the argument(s) to the function.-variadic ::-  forall args result.-  (All Consume args, Curry args, ?inputs::Inputs)-  => ((?inputs::Inputs) => Gen result)-  -> Gen (args ⋯-> result)-variadic out =-  fmap (curryAll @args @_ @(NP I)) . promote $ \args ->-    let ?inputs =-          Inputs . (++ theInputs) $-            hcollapse $ hcliftA (Proxy @Consume) (K . consume . unI) args-    in build out------------------------------------------------------------------------------- Random destruction of the original input, as transformed into Input -------------------------------------------------------------------------------- | Destruct a random subpart of the given 'Input's, returning the 'Variant'--- corresponding to the combined information harvested during this process, and--- the remaining "leaves" of the inputs yet to be destructed------ To maximize the likelihood that different random consumption paths through--- the same value will diverge (desirable when generating functions with--- interesting strictness), @draws@ destructs the forest of @Input@s as a--- depth-first random traversal with a budget sampled from a geometric--- distribution with expectation 1.-draws :: [Input] -> Gen (Variant, [Input])-draws inputs = go [inputs]-  where-    -- Mutually recursive:-    go, inwardFrom :: [[Input]] -> Gen (Variant, [Input])--    go levels =-      oneof                               -- 50% choice between:-        [ return (mempty, concat levels)  -- stop consuming input, or-        , inwardFrom levels ]             -- keep consuming input--    inwardFrom levels =-      case levels of-        [            ] -> return mempty         -- if no more input: stop-        [  ] : outside -> inwardFrom outside    -- if nothing here: backtrack-        here : outside -> do                    -- if something here: go deeper-          (Input v inside, here') <- pick here-          vary v $ do-            (entropy, levels') <- go (inside : here' : outside)  -- back to 'go'-            return (v <> entropy, levels')--    -- Pick a random list element and the remaining list-    pick :: [a] -> Gen (a, [a])-    pick as = do-      index <- choose (0, length as - 1)-      let (before, picked : after) = splitAt index as-      return (picked, before ++ after)---------------------------------------------------- Integration with QuickCheck's Arbitrary ---------------------------------------------------- | We hook into QuickCheck's existing Arbitrary infrastructure by using--- a newtype to differentiate our special way of generating things.-newtype Lazy a-  = Lazy { runLazy :: a }--instance Produce a => Arbitrary (Lazy a) where-  arbitrary = Lazy <$> freely produce---- | Actually produce an output, given an input-consuming producer. If a--- function is to be produced, it will be almost-certainly non-strict.-freely :: ((?inputs::Inputs) => Gen a) -> Gen a-freely p = let ?inputs = Inputs [] in p--------------------- Instances --------------------instance Produce ()       where produce = arbitrary-instance Produce Bool     where produce = arbitrary-instance Produce Ordering where produce = arbitrary--instance Produce Char     where produce = arbitrary-instance Produce Word     where produce = arbitrary-instance Produce Int      where produce = arbitrary-instance Produce Double   where produce = arbitrary-instance Produce Float    where produce = arbitrary-instance Produce Rational where produce = arbitrary-instance Produce Integer  where produce = arbitrary--instance (Arbitrary a, RealFloat a) => Produce (Complex a) where-  produce = arbitrary--instance Produce a => Produce (Maybe a) where-  produce =-    oneof [ return Nothing-          , Just <$> recur-          ]--instance (Produce a, Produce b) => Produce (Either a b) where-  produce =-    oneof [ Left <$> recur-          , Right <$> recur-          ]--instance (Produce a) => Produce [a] where-  produce =-    frequency [ (1, return [])-              , (1, (:) <$> recur-                        <*> recur)-              ]+{-| This module defines the 'Produce' typeclass, used for generating random
+    values for testing in StrictCheck.
+
+    'Produce' is a strict generalization of "Test.QuickCheck"'s 'Arbitrary'
+    typeclass. Paired with 'Consume' (a generalization of 'CoArbitrary') it can
+    be used to create random non-strict functions, whose strictness behavior is
+    dependent on the values given to them.
+-}
+
+module Test.StrictCheck.Produce
+  ( Produce(..)
+  -- * Tools for writing 'Produce' instances
+  , recur
+  , build
+  -- * Producing non-strict functions
+  , returning
+  , variadic
+  -- * Integration with "Test.QuickCheck"'s @Arbitrary@
+  , Lazy(..)
+  , freely
+  -- * Abstract types representing input to a function
+  , Input
+  , Inputs
+  -- * The traversal distribution for processing @Input@s
+  , draws
+  ) where
+
+import Test.QuickCheck hiding (variant)
+import Test.QuickCheck.Gen.Unsafe
+
+import Test.StrictCheck.Internal.Inputs
+import Test.StrictCheck.Consume
+import Test.StrictCheck.Curry
+
+import Generics.SOP
+import Data.Complex
+import Data.List.NonEmpty (NonEmpty(..))
+
+-------------------------------------------------------
+-- The user interface for creating Produce instances --
+-------------------------------------------------------
+
+-- TODO: parameterize over destruction pattern?
+
+-- | Produce an arbitrary value of type @b@, such that destructing that value
+-- incrementally evaluates some input to a function.
+--
+-- Writing instances of @Produce@ is very similar to writing instances of
+-- QuickCheck's 'Arbitrary'. The distinction: when making a recursive call to
+-- produce a subfield of a structure, __always__ use 'build' or 'recur', and
+-- __never__ a direct call to 'produce' itself. This ensures that the input can
+-- potentially be demanded at any step of evaluation of the produced value.
+--
+-- If, in the course of generating a value of type @b@, you need to generate a
+-- random value of some other type, which is /not/ going to be a subpart of the
+-- resultant @b@ (e.g. a length or depth), use a direct call to @arbitrary@ or
+-- some other generator which does not consume input.
+--
+-- An example instance of @Produce@:
+--
+-- > data D a
+-- >   = X a
+-- >   | Y [Int]
+-- >
+-- > instance Produce a => Produce (D a) where
+-- >   produce =
+-- >     oneof [ fmap X recur
+-- >           , fmap Y recur
+-- >           ]
+class Produce b where
+  produce :: (?inputs::Inputs) => Gen b
+
+theInputs :: (?inputs::Inputs) => [Input]
+theInputs = destruct ?inputs
+
+-- | Given an input-consuming producer, wrap it in an outer layer of input
+-- consumption, so that this consumption can be interleaved when the producer is
+-- called recursively to generate a subfield of a larger produced datatype.
+build :: (?inputs::Inputs) => ((?inputs::Inputs) => Gen a) -> Gen a
+build gen = do
+  (v, is') <- draws theInputs
+  vary v $ let ?inputs = Inputs is' in gen
+
+-- | Destruct some inputs to generate an output. This function handles the
+-- interleaving of input destruction with output construction. When producing a
+-- data type, it should be called to produce each subfield -- *not* produce
+-- itself.
+recur :: (Produce a, ?inputs::Inputs) => Gen a
+recur = build produce
+
+
+---------------------------------------
+-- How to make random lazy functions --
+---------------------------------------
+
+-- NOTE: This instance must be defined in this module, as it has to break the
+-- abstraction of the Inputs type. No other instance needs to break this.
+-- Incidentally, it also must break Gen's abstraction barrier, because it needs
+-- to use promote to make a function.
+
+instance (Consume a, Produce b) => Produce (a -> b) where
+  produce = returning produce
+
+-- | Create an input-consuming producer of input-consuming functions, given an
+-- input-consuming producer for results of that function.
+returning
+  :: (Consume a, ?inputs::Inputs)
+  => ((?inputs::Inputs) => Gen b)
+  -> Gen (a -> b)
+returning out =
+  promote $ \a ->
+    let ?inputs = Inputs (consume a : theInputs)
+    in build out
+
+-- | Create an input-consuming producer of input-consuming functions, of any
+-- arity. This will usually be used in conjuntion with type application, to
+-- specify the type(s) of the argument(s) to the function.
+variadic ::
+  forall args result.
+  (All Consume args, Curry args, ?inputs::Inputs)
+  => ((?inputs::Inputs) => Gen result)
+  -> Gen (args ⋯-> result)
+variadic out =
+  fmap (curryAll @args @_ @(NP I)) . promote $ \args ->
+    let ?inputs =
+          Inputs . (++ theInputs) $
+            hcollapse $ hcliftA (Proxy @Consume) (K . consume . unI) args
+    in build out
+
+
+-------------------------------------------------------------------------
+-- Random destruction of the original input, as transformed into Input --
+-------------------------------------------------------------------------
+
+-- | Destruct a random subpart of the given 'Input's, returning the 'Variant'
+-- corresponding to the combined information harvested during this process, and
+-- the remaining "leaves" of the inputs yet to be destructed
+--
+-- To maximize the likelihood that different random consumption paths through
+-- the same value will diverge (desirable when generating functions with
+-- interesting strictness), @draws@ destructs the forest of @Input@s as a
+-- depth-first random traversal with a budget sampled from a geometric
+-- distribution with expectation 1.
+draws :: [Input] -> Gen (Variant, [Input])
+draws inputs = go [inputs]
+  where
+    -- Mutually recursive:
+    go, inwardFrom :: [[Input]] -> Gen (Variant, [Input])
+
+    go levels =
+      oneof                               -- 50% choice between:
+        [ return (mempty, concat levels)  -- stop consuming input, or
+        , inwardFrom levels ]             -- keep consuming input
+
+    inwardFrom levels =
+      case levels of
+        [            ] -> return mempty         -- if no more input: stop
+        [  ] : outside -> inwardFrom outside    -- if nothing here: backtrack
+        here : outside -> do                    -- if something here: go deeper
+          (Input v inside, here') <- pick here
+          vary v $ do
+            (entropy, levels') <- go (inside : here' : outside)  -- back to 'go'
+            return (v <> entropy, levels')
+
+    -- Pick a random list element and the remaining list
+    pick :: [a] -> Gen (a, [a])
+    pick as = do
+      index <- choose (0, length as - 1)
+      case splitAt index as of
+        (before, picked : after) -> return (picked, before ++ after)
+        _ -> error "pick: empty list"
+
+
+---------------------------------------------
+-- Integration with QuickCheck's Arbitrary --
+---------------------------------------------
+
+-- | We hook into QuickCheck's existing Arbitrary infrastructure by using
+-- a newtype to differentiate our special way of generating things.
+newtype Lazy a
+  = Lazy { runLazy :: a }
+
+instance Produce a => Arbitrary (Lazy a) where
+  arbitrary = Lazy <$> freely produce
+
+-- | Actually produce an output, given an input-consuming producer. If a
+-- function is to be produced, it will be almost-certainly non-strict.
+freely :: ((?inputs::Inputs) => Gen a) -> Gen a
+freely p = let ?inputs = Inputs [] in p
+
+
+---------------
+-- Instances --
+---------------
+
+instance Produce ()       where produce = arbitrary
+instance Produce Bool     where produce = arbitrary
+instance Produce Ordering where produce = arbitrary
+
+instance Produce Char     where produce = arbitrary
+instance Produce Word     where produce = arbitrary
+instance Produce Int      where produce = arbitrary
+instance Produce Double   where produce = arbitrary
+instance Produce Float    where produce = arbitrary
+instance Produce Rational where produce = arbitrary
+instance Produce Integer  where produce = arbitrary
+
+instance Arbitrary a => Produce (Complex a) where
+  produce = arbitrary
+
+instance Produce a => Produce (Maybe a) where
+  produce =
+    oneof [ return Nothing
+          , Just <$> recur
+          ]
+
+instance (Produce a, Produce b) => Produce (Either a b) where
+  produce =
+    oneof [ Left <$> recur
+          , Right <$> recur
+          ]
+
+instance (Produce a) => Produce [a] where
+  produce =
+    frequency [ (1, return [])
+              , (1, (:) <$> recur
+                        <*> recur)
+              ]
+
+instance Produce a => Produce (NonEmpty a) where
+  produce = (:|) <$> recur <*> recur

@@ -1,876 +1,875 @@-{-# language InstanceSigs, DerivingStrategies #-}-{-# language PartialTypeSignatures #-}-{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-}-{-| This module defines the 'Shaped' typeclass, which is used to generically-    manipulate values as fixed-points of higher-order functors in order to-    analyze their structure, e.g. while observing evaluation.--    If you just care about testing the strictness of functions over datatypes-    which are already instances of @Shaped@, you don't need to use this module.--    __Important note:__ To define new instances of 'Shaped' for types which-    implement 'GHC.Generic', __an empty instance will suffice__, as all the-    methods of 'Shaped' can be filled in by generic implementations. For-    example:--    > import GHC.Generics as GHC-    > import Generics.SOP as SOP-    >-    > data D = C deriving (GHC.Generic)-    >-    > instance SOP.Generic D-    > instance SOP.HasDatatypeInfo D-    >-    > instance Shaped D--    Using the @DeriveAnyClass@ extension, this can be shortened to one line:--    > data D = C deriving (GHC.Generic, SOP.Generic, SOP.HasDatatypeInfo, Shaped)--    Manual instances of 'Shaped' are necessary for types which do not or cannot-    implement GHC's @Generic@ typeclass, such as existential types, abstract-    types, and GADTs.--    This module is heavily based upon the approach in "Data.Functor.Foldable",-    which in turn is modeled after the paper "Functional Programming with-    Bananas, Lenses, Envelopes and Barbed Wire" (1991) by Erik Meijer, Maarten-    Fokkinga and Ross Paterson. If you don't yet understand recursion schemes-    and want to understand this module, it's probably a good idea to familiarize-    yourself with "Data.Functor.Foldable" before diving into this higher-order-    generalization.--}-module Test.StrictCheck.Shaped-  ( Shaped(..)-  , module Test.StrictCheck.Shaped.Flattened-  -- * Fixed-points of 'Shape's-  , type (%)(..)-  -- * Folds and unfolds over fixed-points of @Shape@s-  , unwrap-  , interleave-  , (%)-  , fuse-  , translate-  , fold-  , unfold-  , unzipWith-  -- , reshape-  -- * Rendering 'Shaped' things as structured text-  , QName-  , Rendered(..)-  , RenderLevel(..)-  , renderfold-  -- * Tools for manually writing instances of 'Shaped'-  -- ** Implementing 'Shaped' for primitive types-  , Prim(..), unPrim-  , projectPrim-  , embedPrim-  , matchPrim-  , flatPrim-  , renderPrim-  , renderConstant-  -- ** Implementing 'Shaped' for container types-  , Containing(..)-  , projectContainer-  , embedContainer-  -- * Generic implementation of the methods of 'Shaped'-  , GShaped-  , GShape(..)-  , gProject-  , gEmbed-  , gMatch-  , gRender-  ) where--import Type.Reflection-import Data.Functor.Product-import Data.Bifunctor-import Data.Bifunctor.Flip-import Data.Coerce--import Generics.SOP hiding ( Shape )--import Data.Complex--- import Data.List.NonEmpty (NonEmpty(..))--import Test.StrictCheck.Shaped.Flattened---- TODO: provide instances for all of Base---- | When a type @a@ is @Shaped@, we know how to convert it into a--- representation parameterized by an arbitrary functor @f@, so that @Shape a f@--- (the "shape of @a@ parameterized by @f@") is structurally identical to the--- topmost structure of @a@, but with @f@ wrapped around any subfields of @a@.------ Note that this is /not/ a recursive representation! The functor @f@ in--- question wraps the original type of the field and /not/ a @Shape@ of that--- field.------ For instance, the @Shape@ of @Either a b@ might be:------ > data EitherShape a b f--- >   = LeftShape  (f a)--- >   | RightShape (f b)--- >--- > instance Shaped (Either a b) where--- >   type Shape (Either a b) = EitherShape a b--- >   ...------ The shape of a primitive type should be isomorphic to the primitive type,--- with the functor parameter left unused.-class Typeable a => Shaped (a :: *) where-  -- | The @Shape@ of an @a@ is a type isomorphic to the outermost level of-  -- structure in an @a@, parameterized by the functor @f@, which is wrapped-  -- around any fields (of any type) in the original @a@.-  type Shape a :: (* -> *) -> *-  type Shape a = GShape a--  -- | Given a function to expand any @Shaped@ @x@ into an @f x@, expand an @a@-  -- into a @Shape a f@-  ---  -- That is: convert the top-most level of structure in the given @a@ into a-  -- @Shape@, calling the provided function on each field in the @a@ to produce-  -- the @f x@ necessary to fill that hole in the produced @Shape a f@.-  ---  -- Inverse to 'embed'.-  project :: (forall x. Shaped x => x -> f x) -> a -> Shape a f--  default project-    :: GShaped a-    => (forall x. Shaped x => x -> f x)-    -> a-    -> Shape a f-  project = gProject--  -- | Given a function to collapse any @f x@ into a @Shaped@ @x@, collapse a-  -- @Shape a f@ into merely an @a@-  ---  -- That is: eliminate the top-most @Shape@ by calling the provided function on-  -- each field in that @Shape a f@, and using the results to fill in the pieces-  -- necessary to build an @a@.-  ---  -- Inverse to 'project'.-  embed :: (forall x. Shaped x => f x -> x) -> Shape a f -> a--  default embed-    :: GShaped a-    => (forall x. Shaped x => f x -> x)-    -> Shape a f-    -> a-  embed = gEmbed--  -- | Given two @Shape@s of the same type @a@ but parameterized by potentially-  -- different functors @f@ and @g@, pattern-match on them to expose a uniform-  -- view on their fields (a 'Flattened' @(Shape a)@) to a continuation which-  -- may operate on those fields to produce some result-  ---  -- If the two supplied @Shape@s do not structurally match, only the fields of-  -- the first are given to the continuation. If they do match, the fields of-  -- the second are also given, along with type-level proof that the types of-  -- the two sets of fields align.-  ---  -- This very general operation subsumes equality testing, mapping, zipping,-  -- shrinking, and many other structural operations over @Shaped@ things.-  ---  -- It is somewhat difficult to manually write instances for this method, but-  -- consulting its generic implementation 'gMatch' may prove helpful.-  ---  -- See "Test.StrictCheck.Shaped.Flattened" for more information.-  match :: Shape a f -> Shape a g-        -> (forall xs. All Shaped xs-              => Flattened (Shape a) f xs-              -> Maybe (Flattened (Shape a) g xs)-              -> result)-        -> result--  default match :: GShaped a-        => Shape a f -> Shape a g-        -> (forall xs. All Shaped xs-              => Flattened (Shape a) f xs-              -> Maybe (Flattened (Shape a) g xs)-              -> result)-        -> result-  match = gMatch--  -- | Convert a @Shape a@ whose fields are some unknown constant type into a-  -- 'RenderLevel' filled with that type-  ---  -- This is a specialized pretty-printing mechanism which allows for displaying-  -- counterexamples in a structured format. See the documentation for-  -- 'RenderLevel'.-  render :: Shape a (K x) -> RenderLevel x--  default render :: (GShaped a, HasDatatypeInfo a)-          => Shape a (K x) -> RenderLevel x-  render = gRender------ * Fixed-points of 'Shape's---- | A value of type @f % a@ has the same structure as an @a@, but with the--- structure of the functor @f@ interleaved at every field (including ones of--- types other than @a@). Read this type aloud as "a interleaved with f's".-newtype (f :: * -> *) % (a :: *) :: * where-  Wrap :: f (Shape a ((%) f)) -> f % a---- | Look inside a single level of an interleaved @f % a@. Inverse to the 'Wrap'--- constructor.-unwrap :: f % a -> f (Shape a ((%) f))-unwrap (Wrap fs) = fs------ * Folds and unfolds over fixed-points of @Shape@s---- | Map a function across all the fields in a 'Shape'------ This function may change the functor over which the @Shape@ is parameterized.--- It can assume recursively that all the fields in the @Shape@ are themselves--- instances of @Shaped@ (which they should be!). This means that you can nest--- calls to @translate@ recursively.-translate :: forall a f g. Shaped a-          => (forall x. Shaped x => f x -> g x)-          -> Shape a f -> Shape a g-translate t d = match @a d d $ \flat _ ->-  unflatten $ mapFlattened @Shaped t flat---- | The equivalent of a fold (catamorphism) over recursively 'Shaped' values------ Given a function which folds an @f@ containing some @Shape x g@ into a @g x@,--- recursively fold any interleaved @f % a@ into a @g a@.-fold :: forall a f g. (Functor f, Shaped a)-     => (forall x. Shaped x => f (Shape x g) -> g x)-     -> f % a -> g a-fold alg = alg . fmap (translate @a (fold alg)) . unwrap---- | The equivalent of an unfold (anamorphism) over recursively 'Shaped' values------ Given a function which unfolds an @f x@ into a @g@ containing some @Shape x--- f@, corecursively unfold any @f a@ into an interleaved @g % a@.-unfold :: forall a f g. (Functor g, Shaped a)-       => (forall x. Shaped x => f x -> g (Shape x f))-       -> f a -> g % a-unfold coalg = Wrap . fmap (translate @a (unfold coalg)) . coalg---- TODO: mapM, foldM, unfoldM, ...---- | Fuse the interleaved @f@-structure out of a recursively interleaved @f %--- a@, given some way of fusing a single level @f x -> x@.------ This is a special case of 'fold'.-fuse-  :: (Functor f, Shaped a)-  => (forall x. f x -> x)-  -> (f % a -> a)-fuse e = e . fold (fmap (embed e))---- | Interleave an @f@-structure at every recursive level of some @a@, given--- some way of generating a single level of structure @x -> f x@.------ This is a special case of 'unfold'.-interleave-  :: (Functor f, Shaped a)-  => (forall x. x -> f x)-  -> (a -> f % a)-interleave p = unfold (fmap (project p)) . p---- | An infix synonym for 'interleave'-(%) :: forall a f. (Functor f, Shaped a)-    => (forall x. x -> f x)-    -> a -> f % a-(%) = interleave---- | A higher-kinded @unzipWith@, operating over interleaved structures------ Given a function splitting some @f x@ into a functor-product @Product g h x@,--- recursively split an interleaved @f % a@ into two interleaved structures:--- one built of @g@-shapes and one of @h@-shapes.------ Note that @Product ((%) g) ((%) h) a@ is isomorphic to @(g % a, h % a)@; to--- get the latter, pattern-match on the 'Pair' constructor of 'Product'.-unzipWith-  :: (All Functor [f, g, h], Shaped a)-  => (forall x. f x -> (g x, h x))-  -> (f % a -> (g % a, h % a))-unzipWith split =-  unPair . fold (crunch . pair . split)-  where-    crunch-      :: forall x g h.-      (Shaped x, Functor g, Functor h)-      => Product g h (Shape x (Product ((%) g) ((%) h)))-      -> Product ((%) g) ((%) h) x-    crunch =-      pair-      . bimap (Wrap . fmap (translate @x (fst . unPair)))-              (Wrap . fmap (translate @x (snd . unPair)))-      . unPair--    pair :: (l x, r x) -> Product l r x-    pair = uncurry Pair--    unPair :: Product l r x -> (l x, r x)-    unPair (Pair lx rx) = (lx, rx)---- | TODO: document this strange function-{--reshape :: forall b a f g. (Shaped a, Shaped b, Functor f)-        => (f (Shape b ((%) g)) -> g (Shape b ((%) g)))-        -> (forall x. Shaped x => f % x -> g % x)-        -> f % a -> g % a-reshape homo hetero d =-  case eqTypeRep (typeRep @a) (typeRep @b) of-    Nothing    -> hetero d-    Just HRefl ->-      Wrap-      $ homo . fmap (translate @a (reshape @b homo hetero))-      $ unwrap d--}--------------------------------------- Rendering shapes for display ----------------------------------------- | Convert an @f % a@ into a structured pretty-printing representation,--- suitable for further display/processing-renderfold-  :: forall a f. (Shaped a, Functor f)-  => f % a -> Rendered f-renderfold = unK . fold oneLevel-  where-    oneLevel :: forall x. Shaped x-             => f (Shape x (K (Rendered f)))-             -> K (Rendered f) x-    oneLevel = K . RWrap . fmap (render @x)---- | A @QName@ is a qualified name------ Note:--- > type ModuleName   = String--- > type DatatypeName = String-type QName = (ModuleName, DatatypeName, String)---- | @RenderLevel@ is a functor whose outer shape contains all the information--- about how to pretty-format the outermost @Shape@ of some value. We use--- parametricity to make it difficult to construct incorrect 'render' methods,--- by asking the user merely to produce a single @RenderLevel@ and stitching--- nested @RenderLevel@s into complete 'Rendered' trees.-data RenderLevel x-  = ConstructorD QName [x]-  -- ^ A prefix constructor, and a list of its fields-  | InfixD QName Associativity Fixity x x-  -- ^ An infix constructor, its associativity and fixity, and its two fields-  | RecordD QName [(QName, x)]-  -- ^ A record constructor, and a list of its field names paired with fields-  | CustomD Fixity-    [Either (Either String (ModuleName, String)) (Fixity, x)]-  -- ^ A custom pretty-printing representation (i.e. for abstract types), which-  -- records a fixity and a list of tokens of three varieties: 1) raw strings,-  -- 2) qualified strings (from some module), or 3) actual fields, annotated-  -- with their fixity-  deriving (Eq, Ord, Show, Functor)---- | @Rendered f@ is the fixed-point of @f@ composed with 'RenderLevel': it--- alternates between @f@ shapes and @RenderLevel@s. Usually, @f@ will be the--- identity functor 'I', but not always.-data Rendered f-  = RWrap (f (RenderLevel (Rendered f)))---------------------------------------------------------- Tools for manually writing instances of Shaped ----------------------------------------------------------- | The @Shape@ of a spine-strict container (i.e. a @Map@ or @Set@) is the same--- as a container of demands on its elements. However, this does not have the--- right /kind/ to be used as a @Shape@.------ The @Containing@ newtype solves this problem. By defining the @Shape@ of some--- container @(C a)@ to be @(C `Containing` a)@, you can use the methods--- @projectContainer@ and @embedContainer@ to implement @project@ and @embed@--- for your container type (although you will still need to manually define--- @match@ and @render@).-newtype Containing h a f-  = Container (h (f a))-  deriving (Eq, Ord, Show)---- | Generic implementation of @project@ for any container type whose @Shape@--- is represented as a @Containing@ newtype-projectContainer :: (Functor c, Shaped a)-  => (forall x. Shaped x => x -> f x)-  -> c a -> Containing c a f-projectContainer p x = Container (fmap p x)---- | Generic implementation of @embed@ for any container type whose @Shape@--- is represented as a @Containing@ newtype-embedContainer :: (Functor c, Shaped a)-  => (forall x. Shaped x => f x -> x)-  -> Containing c a f -> c a-embedContainer e (Container x) = fmap e x----- TODO: helper functions for matching and prettying containers---- | The @Shape@ of a primitive type should be equivalent to the type itself.--- However, this does not have the right /kind/ to be used as a @Shape@.------ The @Prim@ newtype solves this problem. By defining the @Shape@ of some--- primitive type @p@ to be @Prim p@, you can use the methods @projectPrim@,--- @embedPrim@, @matchPrim@, and @prettyPrim@ to completely fill in the--- definition of the @Shaped@ class for a primitive type.------ __Note:__ It is only appropriate to use this @Shape@ representation when a--- type really is primitive, in that it contains no interesting substructure.--- If you use the @Prim@ representation inappropriately, StrictCheck will not be--- able to inspect the richer structure of the type in question.-newtype Prim (x :: *) (f :: * -> *)-  = Prim x-  deriving (Eq, Ord, Show)-  deriving newtype (Num)---- | Get the wrapped @x@ out of a @Prim x f@ (inverse to the @Prim@ constructor)-unPrim :: Prim x f -> x-unPrim (Prim x) = x---- | Generic implementation of @project@ for any primitive type whose @Shape@ is--- is represented as a @Prim@ newtype-projectPrim :: (forall x. Shaped x => x -> f x) -> a -> Prim a f-projectPrim _ = Prim---- | Generic implementation of @embed@ for any primitive type whose @Shape@ is--- is represented as a @Prim@ newtype-embedPrim :: (forall x. Shaped x => f x -> x) -> Prim a f -> a-embedPrim _ = unPrim---- | Generic implementation of @match@ for any primitive type whose @Shape@ is--- is represented as a @Prim@ newtype with an underlying @Eq@ instance-matchPrim :: Eq a => Prim a f -> Prim a g-           -> (forall xs. All Shaped xs-                => Flattened (Prim a) f xs-                -> Maybe (Flattened (Prim a) g xs)-                -> result)-           -> result-matchPrim (Prim a) (Prim b) k =-  k (flatPrim a)-     (if a == b then (Just (flatPrim b)) else Nothing)---- | Helper for writing @match@ instances for primitive types which don't have--- @Eq@ instance------ This generates a @Flattened@ appropriate for using in the implementation of--- @match@. For more documentation on how to use this, see the documentation of--- 'match'.-flatPrim :: a -> Flattened (Prim a) g '[]-flatPrim x = Flattened (const (Prim x)) Nil---- | Generic implementation of @render@ for any primitive type whose @Shape@ is--- is represented as a @Prim@ newtype-renderPrim :: Show a => Prim a (K x) -> RenderLevel x-renderPrim (Prim a) = renderConstant (show a)---- | Given some @string@, generate a custom pretty-printing representation which--- just shows the string-renderConstant :: String -> RenderLevel x-renderConstant s = CustomD 11 [Left (Left s)]---- TODO: What about demands for abstract types with > 1 type of unbounded-count field?--{--withFieldsContainer ::-  forall c a f result.-     (forall r h.-        c (h a) ->-        (forall x. Shaped x-           => [h x]-           -> (forall g. [g x] -> c (g a))-           -> r)-        -> r)-  -> Containing c a f-  -> (forall xs. All Shaped xs-        => NP f xs-        -> (forall g. NP g xs -> Containing c a g)-        -> result)-  -> result-withFieldsContainer viaContaining (Container c) cont =-  viaContaining c $-    \list un ->-       withNP @Shaped list (Container . un) cont---- TODO: Make this work for any number of lists of fields, by carefully using--- unsafeCoerce to deal with unknown list lengths--withFieldsViaList ::-  forall demand f result.-     (forall r h.-        demand h ->-        (forall x. Shaped x-           => [h x]-           -> (forall g. [g x] -> demand g)-           -> r)-        -> r)-  -> demand f-  -> (forall xs. All Shaped xs-        => NP f xs-        -> (forall g. NP g xs -> demand g)-        -> result)-  -> result-withFieldsViaList viaList demand cont =-  viaList demand $-    \list un ->-       withNP @Shaped list un cont--withNP :: forall c demand result f x. c x-       => [f x]-       -> (forall g. [g x] -> demand g)-       -> (forall xs. All c xs-             => NP f xs -> (forall g. NP g xs -> demand g) -> result)-       -> result-withNP list unList cont =-  withUnhomogenized @c list $ \np ->-    cont np (unList . homogenize)--withConcatenated :: NP (NP f) xss -> (forall xs. NP f xs -> r) -> r-withConcatenated pop cont =-  case pop of-    Nil         -> cont Nil-    (xs :* xss) -> withConcatenated xss (withPrepended xs cont)-  where-    withPrepended ::-      NP f ys -> (forall zs. NP f zs -> r)-              -> (forall zs. NP f zs -> r)-    withPrepended pre k rest =-      case pre of-        Nil        -> k rest-        (x :* xs)  -> withPrepended xs (k . (x :*)) rest--homogenize :: All ((~) a) as => NP f as -> [f a]-homogenize      Nil  = []-homogenize (a :* as) = a : homogenize as--withUnhomogenized :: forall c a f r.-  c a => [f a] -> (forall as. (All c as, All ((~) a) as) => NP f as -> r) -> r-withUnhomogenized      []  k = k Nil-withUnhomogenized (a : as) k =-  withUnhomogenized @c as $ \np -> k (a :* np)--}--------------------------------------------------------- Generic implementation of the Shaped methods ---------------------------------------------------------- | The 'Shape' used for generic implementations of 'Shaped'------ This wraps a sum-of-products representation from "Generics.SOP".-newtype GShape a f-  = GS (NS (NP f) (Code a))---- | The collection of constraints necessary for a type to be given a generic--- implementation of the 'Shaped' methods-type GShaped a =-  ( Generic a-  , Shape a ~ GShape a-  , All2 Shaped (Code a)-  , SListI (Code a)-  , All SListI (Code a) )---- | Generic 'project'-gProject :: GShaped a-         => (forall x. Shaped x => x -> f x)-         -> a -> Shape a f-gProject p !(from -> sop) =-  GS (unSOP (hcliftA (Proxy @Shaped) (p . unI) sop))---- | Generic 'embed'-gEmbed :: GShaped a-       => (forall x. Shaped x => f x -> x)-       -> Shape a f -> a-gEmbed e !(GS d) =-  to (hcliftA (Proxy @Shaped) (I . e) (SOP d))---- | Generic 'match'-gMatch :: forall a f g result. GShaped a-       => Shape a f -> Shape a g-       -> (forall xs. All Shaped xs-             => Flattened (Shape a) f xs-             -> Maybe (Flattened (Shape a) g xs)-             -> result)-       -> result-gMatch !(GS df) !(GS dg) cont =-  go @(Code a) df (Just dg) $ \flatF mflatG ->-    cont (flatGD flatF) (flatGD <$> mflatG)-  where-    go :: forall xss r.-      (All SListI xss, All2 Shaped xss)-       => NS (NP f) xss-       -> Maybe (NS (NP g) xss)-       -> (forall xs. All Shaped xs-             => Flattened (Flip SOP xss) f xs-             -> Maybe (Flattened (Flip SOP xss) g xs)-             -> r)-       -> r-    go (Z (fieldsF :: _ xs)) (Just (Z fieldsG)) k =-      k @xs (flatZ fieldsF)  (Just (flatZ fieldsG))-    go (Z (fieldsF :: _ xs)) _ k =   -- Nothing | Just (S _)-      k @xs (flatZ fieldsF)  Nothing-    go (S moreF) Nothing k =-      go moreF Nothing $ \(flatF :: _ xs) _ ->-        k @xs (flatS flatF) Nothing-    go (S moreF) (Just (Z _)) k =-      go moreF Nothing $ \(flatF :: _ xs) _ ->-        k @xs (flatS flatF) Nothing-    go (S moreF) (Just (S moreG)) k =-      go moreF (Just moreG) $ \(flatF :: _ xs) mflatG ->-        k @xs (flatS flatF) (flatS <$> mflatG)--    flatZ-      :: forall h xs xss. NP h xs -> Flattened (Flip SOP (xs : xss)) h xs-    flatZ = Flattened (Flip . SOP . Z)--    flatS-      :: forall h xs xs' xss.-      Flattened (Flip SOP xss) h xs-      -> Flattened (Flip SOP (xs' : xss)) h xs-    flatS (Flattened un fields) =-      Flattened (Flip . SOP . S . coerce . un) fields--    flatGD :: forall t h xs.-      Flattened (Flip SOP (Code t)) h xs -> Flattened (GShape t) h xs-    flatGD (Flattened un fields) =-      Flattened (GS . coerce . un) fields---- | Generic 'render'-gRender :: forall a x. (HasDatatypeInfo a, GShaped a)-         => Shape a (K x) -> RenderLevel x-gRender (GS demand) =-  case info of-    ADT m d cs ->-      renderC m d demand cs-    Newtype m d c ->-      renderC m d demand (c :* Nil)-  where-    info = datatypeInfo (Proxy @a)--    renderC :: forall as. ModuleName -> DatatypeName-            -> NS (NP (K x)) as-            -> NP ConstructorInfo as-            -> RenderLevel x-    renderC m d subShape constructors =-      case (subShape, constructors) of-        (Z demandFields, c :* _) ->-          case c of-            Constructor name ->-              ConstructorD (m, d, name) $-                hcollapse demandFields-            Infix name associativity fixity ->-              case demandFields of-                (K a :* K b :* Nil) ->-                  InfixD (m, d, name) associativity fixity a b-            Record name fieldsInfo ->-              RecordD (m, d, name) $-                zip ( hcollapse-                    . hliftA (\(FieldInfo f) -> K (m, d, f))-                    $ fieldsInfo )-                    (hcollapse demandFields)-        (S another, _ :* different) ->-          renderC m d another different--------------------- Instances --------------------instance Shaped ()-instance Shaped Bool-instance Shaped Ordering-instance Shaped a => Shaped (Maybe a)-instance (Shaped a, Shaped b) => Shaped (Either a b)-instance Shaped a => Shaped [a]--instance (Typeable a, Typeable b) => Shaped (a -> b) where-  type Shape (a -> b) = Prim (a -> b)-  project = projectPrim-  embed = embedPrim-  match (Prim f) (Prim g) k = k (flatPrim f) (Just $ flatPrim g)-  render _ = renderConstant ("<function> :: " ++ show (typeRep @(a -> b)))--instance Shaped Char where-  type Shape Char = Prim Char-  project = projectPrim-  embed   = embedPrim-  match   = matchPrim-  render  = renderPrim--instance Shaped Word where-  type Shape Word = Prim Word-  project = projectPrim-  embed   = embedPrim-  match   = matchPrim-  render  = renderPrim--instance Shaped Int where-  type Shape Int = Prim Int-  project = projectPrim-  embed   = embedPrim-  match   = matchPrim-  render  = renderPrim--instance Shaped Double where-  type Shape Double = Prim Double-  project = projectPrim-  embed   = embedPrim-  match   = matchPrim-  render  = renderPrim--instance Shaped Float where-  type Shape Float = Prim Float-  project = projectPrim-  embed   = embedPrim-  match   = matchPrim-  render  = renderPrim--instance Shaped Rational where-  type Shape Rational = Prim Rational-  project = projectPrim-  embed   = embedPrim-  match   = matchPrim-  render  = renderPrim--instance Shaped Integer where-  type Shape Integer = Prim Integer-  project = projectPrim-  embed   = embedPrim-  match   = matchPrim-  render  = renderPrim--instance (Typeable a, Eq a, Show a) => Shaped (Complex a) where-  type Shape (Complex a) = Prim (Complex a)-  project = projectPrim-  embed   = embedPrim-  match   = matchPrim-  render  = renderPrim---- instance Generic (NonEmpty a)--- instance HasDatatypeInfo (NonEmpty a)--- instance Shaped a => Shaped (NonEmpty a) where---- Tree--- Map k--- Seq--- Set--- IntMap--- IntSet--instance (Shaped a, Shaped b) => Shaped (a, b)-instance (Shaped a, Shaped b, Shaped c) => Shaped (a, b, c)-instance (Shaped a, Shaped b, Shaped c, Shaped d) => Shaped (a, b, c, d)-instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e-         ) => Shaped-  (a, b, c, d, e)-instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f-         ) => Shaped-  (a, b, c, d, e, f)-instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f-         , Shaped g-         ) => Shaped-  (a, b, c, d, e, f, g)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h---          ) => Shaped---   (a, b, c, d, e, f, g, h)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i---          ) => Shaped---   (a, b, c, d, e, f, g, h, i)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j---          ) => Shaped---   (a, b, c, d, e, f, g, h, i, j)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k---          ) => Shaped---   (a, b, c, d, e, f, g, h, i, j, k)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l---          ) => Shaped---   (a, b, c, d, e, f, g, h, i, j, k, l)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l---          , Shaped m---          ) => Shaped---   (a, b, c, d, e, f, g, h, i, j, k, l, m)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l---          , Shaped m, Shaped n---          ) => Shaped---   (a, b, c, d, e, f, g, h, i, j, k, l, m, n)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l---          , Shaped m, Shaped n, Shaped o---          ) => Shaped---   (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l---          , Shaped m, Shaped n, Shaped o, Shaped p---          ) => Shaped---   (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l---          , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q---          ) => Shaped---   (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l---          , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r---          ) => Shaped---   (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l---          , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r---          , Shaped s---          ) => Shaped---   (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l---          , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r---          , Shaped s, Shaped t---          ) => Shaped---   (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l---          , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r---          , Shaped s, Shaped t, Shaped u---          ) => Shaped---   (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l---          , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r---          , Shaped s, Shaped t, Shaped u, Shaped v---          ) => Shaped---   (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l---          , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r---          , Shaped s, Shaped t, Shaped u, Shaped v, Shaped w---          ) => Shaped---   (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l---          , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r---          , Shaped s, Shaped t, Shaped u, Shaped v, Shaped w, Shaped x---           ) => Shaped---   (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l---          , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r---          , Shaped s, Shaped t, Shaped u, Shaped v, Shaped w, Shaped x---          , Shaped y---          ) => Shaped---   (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y)--- instance ( Shaped a, Shaped b, Shaped c, Shaped d, Shaped e, Shaped f---          , Shaped g, Shaped h, Shaped i, Shaped j, Shaped k, Shaped l---          , Shaped m, Shaped n, Shaped o, Shaped p, Shaped q, Shaped r---          , Shaped s, Shaped t, Shaped u, Shaped v, Shaped w, Shaped x---          , Shaped y, Shaped z---          ) => Shaped---   (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z)+{-# language InstanceSigs, DerivingStrategies #-}
+{-# language PartialTypeSignatures #-}
+{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-}
+{-| This module defines the 'Shaped' typeclass, which is used to generically
+    manipulate values as fixed-points of higher-order functors in order to
+    analyze their structure, e.g. while observing evaluation.
+
+    If you just care about testing the strictness of functions over datatypes
+    which are already instances of @Shaped@, you don't need to use this module.
+
+    __Important note:__ To define new instances of 'Shaped' for types which
+    implement 'GHC.Generic', __an empty instance will suffice__, as all the
+    methods of 'Shaped' can be filled in by generic implementations. For
+    example:
+
+    > import GHC.Generics as GHC
+    > import Generics.SOP as SOP
+    >
+    > data D = C deriving (GHC.Generic)
+    >
+    > instance SOP.Generic D
+    > instance SOP.HasDatatypeInfo D
+    >
+    > instance Shaped D
+
+    Using the @DeriveAnyClass@ extension, this can be shortened to one line:
+
+    > data D = C deriving (GHC.Generic, SOP.Generic, SOP.HasDatatypeInfo, Shaped)
+
+    Manual instances of 'Shaped' are necessary for types which do not or cannot
+    implement GHC's @Generic@ typeclass, such as existential types, abstract
+    types, and GADTs.
+
+    This module is heavily based upon the approach in "Data.Functor.Foldable",
+    which in turn is modeled after the paper "Functional Programming with
+    Bananas, Lenses, Envelopes and Barbed Wire" (1991) by Erik Meijer, Maarten
+    Fokkinga and Ross Paterson. If you don't yet understand recursion schemes
+    and want to understand this module, it's probably a good idea to familiarize
+    yourself with "Data.Functor.Foldable" before diving into this higher-order
+    generalization.
+-}
+module Test.StrictCheck.Shaped
+  ( Shaped(..)
+  , module Test.StrictCheck.Shaped.Flattened
+  -- * Fixed-points of 'Shape's
+  , type (%)(..)
+  -- * Folds and unfolds over fixed-points of @Shape@s
+  , unwrap
+  , interleave
+  , (%)
+  , fuse
+  , translate
+  , fold
+  , unfold
+  , unzipWith
+  -- , reshape
+  -- * Rendering 'Shaped' things as structured text
+  , QName
+  , Rendered(..)
+  , RenderLevel(..)
+  , renderfold
+  -- * Tools for manually writing instances of 'Shaped'
+  -- ** Implementing 'Shaped' for primitive types
+  , Prim(..), unPrim
+  , projectPrim
+  , embedPrim
+  , matchPrim
+  , flatPrim
+  , renderPrim
+  , renderConstant
+  -- ** Implementing 'Shaped' for container types
+  , Containing(..)
+  , projectContainer
+  , embedContainer
+  -- * Generic implementation of the methods of 'Shaped'
+  , GShaped
+  , GShape(..)
+  , gProject
+  , gEmbed
+  , gMatch
+  , gRender
+  ) where
+
+import Type.Reflection
+import Data.Functor.Product
+import Data.Bifunctor
+import Data.Bifunctor.Flip
+import Data.Coerce
+import Data.Kind (Type)
+
+import Generics.SOP hiding ( Shape )
+
+import Data.Complex
+import Data.List.NonEmpty (NonEmpty(..))
+
+import Test.StrictCheck.Shaped.Flattened
+
+-- TODO: provide instances for all of Base
+
+-- | When a type @a@ is @Shaped@, we know how to convert it into a
+-- representation parameterized by an arbitrary functor @f@, so that @Shape a f@
+-- (the "shape of @a@ parameterized by @f@") is structurally identical to the
+-- topmost structure of @a@, but with @f@ wrapped around any subfields of @a@.
+--
+-- Note that this is /not/ a recursive representation! The functor @f@ in
+-- question wraps the original type of the field and /not/ a @Shape@ of that
+-- field.
+--
+-- For instance, the @Shape@ of @Either a b@ might be:
+--
+-- > data EitherShape a b f
+-- >   = LeftShape  (f a)
+-- >   | RightShape (f b)
+-- >
+-- > instance Shaped (Either a b) where
+-- >   type Shape (Either a b) = EitherShape a b
+-- >   ...
+--
+-- The shape of a primitive type should be isomorphic to the primitive type,
+-- with the functor parameter left unused.
+class Typeable a => Shaped (a :: Type) where
+  -- | The @Shape@ of an @a@ is a type isomorphic to the outermost level of
+  -- structure in an @a@, parameterized by the functor @f@, which is wrapped
+  -- around any fields (of any type) in the original @a@.
+  type Shape a :: (Type -> Type) -> Type
+  type Shape a = GShape a
+
+  -- | Given a function to expand any @Shaped@ @x@ into an @f x@, expand an @a@
+  -- into a @Shape a f@
+  --
+  -- That is: convert the top-most level of structure in the given @a@ into a
+  -- @Shape@, calling the provided function on each field in the @a@ to produce
+  -- the @f x@ necessary to fill that hole in the produced @Shape a f@.
+  --
+  -- Inverse to 'embed'.
+  project :: (forall x. Shaped x => x -> f x) -> a -> Shape a f
+
+  default project
+    :: GShaped a
+    => (forall x. Shaped x => x -> f x)
+    -> a
+    -> Shape a f
+  project = gProject
+
+  -- | Given a function to collapse any @f x@ into a @Shaped@ @x@, collapse a
+  -- @Shape a f@ into merely an @a@
+  --
+  -- That is: eliminate the top-most @Shape@ by calling the provided function on
+  -- each field in that @Shape a f@, and using the results to fill in the pieces
+  -- necessary to build an @a@.
+  --
+  -- Inverse to 'project'.
+  embed :: (forall x. Shaped x => f x -> x) -> Shape a f -> a
+
+  default embed
+    :: GShaped a
+    => (forall x. Shaped x => f x -> x)
+    -> Shape a f
+    -> a
+  embed = gEmbed
+
+  -- | Given two @Shape@s of the same type @a@ but parameterized by potentially
+  -- different functors @f@ and @g@, pattern-match on them to expose a uniform
+  -- view on their fields (a 'Flattened' @(Shape a)@) to a continuation which
+  -- may operate on those fields to produce some result
+  --
+  -- If the two supplied @Shape@s do not structurally match, only the fields of
+  -- the first are given to the continuation. If they do match, the fields of
+  -- the second are also given, along with type-level proof that the types of
+  -- the two sets of fields align.
+  --
+  -- This very general operation subsumes equality testing, mapping, zipping,
+  -- shrinking, and many other structural operations over @Shaped@ things.
+  --
+  -- It is somewhat difficult to manually write instances for this method, but
+  -- consulting its generic implementation 'gMatch' may prove helpful.
+  --
+  -- See "Test.StrictCheck.Shaped.Flattened" for more information.
+  match :: Shape a f -> Shape a g
+        -> (forall xs. All Shaped xs
+              => Flattened (Shape a) f xs
+              -> Maybe (Flattened (Shape a) g xs)
+              -> result)
+        -> result
+
+  default match :: GShaped a
+        => Shape a f -> Shape a g
+        -> (forall xs. All Shaped xs
+              => Flattened (Shape a) f xs
+              -> Maybe (Flattened (Shape a) g xs)
+              -> result)
+        -> result
+  match = gMatch
+
+  -- | Convert a @Shape a@ whose fields are some unknown constant type into a
+  -- 'RenderLevel' filled with that type
+  --
+  -- This is a specialized pretty-printing mechanism which allows for displaying
+  -- counterexamples in a structured format. See the documentation for
+  -- 'RenderLevel'.
+  render :: Shape a (K x) -> RenderLevel x
+
+  default render :: (GShaped a, HasDatatypeInfo a)
+          => Shape a (K x) -> RenderLevel x
+  render = gRender
+
+
+
+-- * Fixed-points of 'Shape's
+
+-- | A value of type @f % a@ has the same structure as an @a@, but with the
+-- structure of the functor @f@ interleaved at every field (including ones of
+-- types other than @a@). Read this type aloud as "a interleaved with f's".
+newtype (f :: Type -> Type) % (a :: Type) :: Type where
+  Wrap :: f (Shape a ((%) f)) -> f % a
+
+-- | Look inside a single level of an interleaved @f % a@. Inverse to the 'Wrap'
+-- constructor.
+unwrap :: f % a -> f (Shape a ((%) f))
+unwrap (Wrap fs) = fs
+
+
+
+-- * Folds and unfolds over fixed-points of @Shape@s
+
+-- | Map a function across all the fields in a 'Shape'
+--
+-- This function may change the functor over which the @Shape@ is parameterized.
+-- It can assume recursively that all the fields in the @Shape@ are themselves
+-- instances of @Shaped@ (which they should be!). This means that you can nest
+-- calls to @translate@ recursively.
+translate :: forall a f g. Shaped a
+          => (forall x. Shaped x => f x -> g x)
+          -> Shape a f -> Shape a g
+translate t d = match @a d d $ \flat _ ->
+  unflatten $ mapFlattened @Shaped t flat
+
+-- | The equivalent of a fold (catamorphism) over recursively 'Shaped' values
+--
+-- Given a function which folds an @f@ containing some @Shape x g@ into a @g x@,
+-- recursively fold any interleaved @f % a@ into a @g a@.
+fold :: forall a f g. (Functor f, Shaped a)
+     => (forall x. Shaped x => f (Shape x g) -> g x)
+     -> f % a -> g a
+fold alg = alg . fmap (translate @a (fold alg)) . unwrap
+
+-- | The equivalent of an unfold (anamorphism) over recursively 'Shaped' values
+--
+-- Given a function which unfolds an @f x@ into a @g@ containing some @Shape x
+-- f@, corecursively unfold any @f a@ into an interleaved @g % a@.
+unfold :: forall a f g. (Functor g, Shaped a)
+       => (forall x. Shaped x => f x -> g (Shape x f))
+       -> f a -> g % a
+unfold coalg = Wrap . fmap (translate @a (unfold coalg)) . coalg
+
+-- TODO: mapM, foldM, unfoldM, ...
+
+-- | Fuse the interleaved @f@-structure out of a recursively interleaved @f %
+-- a@, given some way of fusing a single level @f x -> x@.
+--
+-- This is a special case of 'fold'.
+fuse
+  :: (Functor f, Shaped a)
+  => (forall x. f x -> x)
+  -> (f % a -> a)
+fuse e = e . fold (fmap (embed e))
+
+-- | Interleave an @f@-structure at every recursive level of some @a@, given
+-- some way of generating a single level of structure @x -> f x@.
+--
+-- This is a special case of 'unfold'.
+interleave
+  :: (Functor f, Shaped a)
+  => (forall x. x -> f x)
+  -> (a -> f % a)
+interleave p = unfold (fmap (project p)) . p
+
+-- | An infix synonym for 'interleave'
+(%) :: forall a f. (Functor f, Shaped a)
+    => (forall x. x -> f x)
+    -> a -> f % a
+(%) = interleave
+
+-- | A higher-kinded @unzipWith@, operating over interleaved structures
+--
+-- Given a function splitting some @f x@ into a functor-product @Product g h x@,
+-- recursively split an interleaved @f % a@ into two interleaved structures:
+-- one built of @g@-shapes and one of @h@-shapes.
+--
+-- Note that @Product ((%) g) ((%) h) a@ is isomorphic to @(g % a, h % a)@; to
+-- get the latter, pattern-match on the 'Pair' constructor of 'Product'.
+unzipWith
+  :: (All Functor [f, g, h], Shaped a)
+  => (forall x. f x -> (g x, h x))
+  -> (f % a -> (g % a, h % a))
+unzipWith split =
+  unPair . fold (crunch . pair . split)
+  where
+    crunch
+      :: forall x g h.
+      (Shaped x, Functor g, Functor h)
+      => Product g h (Shape x (Product ((%) g) ((%) h)))
+      -> Product ((%) g) ((%) h) x
+    crunch =
+      pair
+      . bimap (Wrap . fmap (translate @x (fst . unPair)))
+              (Wrap . fmap (translate @x (snd . unPair)))
+      . unPair
+
+    pair :: (l x, r x) -> Product l r x
+    pair = uncurry Pair
+
+    unPair :: Product l r x -> (l x, r x)
+    unPair (Pair lx rx) = (lx, rx)
+
+-- | TODO: document this strange function
+{-
+reshape :: forall b a f g. (Shaped a, Shaped b, Functor f)
+        => (f (Shape b ((%) g)) -> g (Shape b ((%) g)))
+        -> (forall x. Shaped x => f % x -> g % x)
+        -> f % a -> g % a
+reshape homo hetero d =
+  case eqTypeRep (typeRep @a) (typeRep @b) of
+    Nothing    -> hetero d
+    Just HRefl ->
+      Wrap
+      $ homo . fmap (translate @a (reshape @b homo hetero))
+      $ unwrap d
+-}
+
+----------------------------------
+-- Rendering shapes for display --
+----------------------------------
+
+-- | Convert an @f % a@ into a structured pretty-printing representation,
+-- suitable for further display/processing
+renderfold
+  :: forall a f. (Shaped a, Functor f)
+  => f % a -> Rendered f
+renderfold = unK . fold oneLevel
+  where
+    oneLevel :: forall x. Shaped x
+             => f (Shape x (K (Rendered f)))
+             -> K (Rendered f) x
+    oneLevel = K . RWrap . fmap (render @x)
+
+-- | A @QName@ is a qualified name
+--
+-- Note:
+-- > type ModuleName   = String
+-- > type DatatypeName = String
+type QName = (ModuleName, DatatypeName, String)
+
+-- | @RenderLevel@ is a functor whose outer shape contains all the information
+-- about how to pretty-format the outermost @Shape@ of some value. We use
+-- parametricity to make it difficult to construct incorrect 'render' methods,
+-- by asking the user merely to produce a single @RenderLevel@ and stitching
+-- nested @RenderLevel@s into complete 'Rendered' trees.
+data RenderLevel x
+  = ConstructorD QName [x]
+  -- ^ A prefix constructor, and a list of its fields
+  | InfixD QName Associativity Fixity x x
+  -- ^ An infix constructor, its associativity and fixity, and its two fields
+  | RecordD QName [(QName, x)]
+  -- ^ A record constructor, and a list of its field names paired with fields
+  | CustomD Fixity
+    [Either (Either String (ModuleName, String)) (Fixity, x)]
+  -- ^ A custom pretty-printing representation (i.e. for abstract types), which
+  -- records a fixity and a list of tokens of three varieties: 1) raw strings,
+  -- 2) qualified strings (from some module), or 3) actual fields, annotated
+  -- with their fixity
+  deriving (Eq, Ord, Show, Functor)
+
+-- | @Rendered f@ is the fixed-point of @f@ composed with 'RenderLevel': it
+-- alternates between @f@ shapes and @RenderLevel@s. Usually, @f@ will be the
+-- identity functor 'I', but not always.
+data Rendered f
+  = RWrap (f (RenderLevel (Rendered f)))
+
+
+----------------------------------------------------
+-- Tools for manually writing instances of Shaped --
+----------------------------------------------------
+
+-- | The @Shape@ of a spine-strict container (i.e. a @Map@ or @Set@) is the same
+-- as a container of demands on its elements. However, this does not have the
+-- right /kind/ to be used as a @Shape@.
+--
+-- The @Containing@ newtype solves this problem. By defining the @Shape@ of some
+-- container @(C a)@ to be @(C `Containing` a)@, you can use the methods
+-- @projectContainer@ and @embedContainer@ to implement @project@ and @embed@
+-- for your container type (although you will still need to manually define
+-- @match@ and @render@).
+newtype Containing h a f
+  = Container (h (f a))
+  deriving (Eq, Ord, Show)
+
+-- | Generic implementation of @project@ for any container type whose @Shape@
+-- is represented as a @Containing@ newtype
+projectContainer :: (Functor c, Shaped a)
+  => (forall x. Shaped x => x -> f x)
+  -> c a -> Containing c a f
+projectContainer p x = Container (fmap p x)
+
+-- | Generic implementation of @embed@ for any container type whose @Shape@
+-- is represented as a @Containing@ newtype
+embedContainer :: (Functor c, Shaped a)
+  => (forall x. Shaped x => f x -> x)
+  -> Containing c a f -> c a
+embedContainer e (Container x) = fmap e x
+
+
+-- TODO: helper functions for matching and prettying containers
+
+-- | The @Shape@ of a primitive type should be equivalent to the type itself.
+-- However, this does not have the right /kind/ to be used as a @Shape@.
+--
+-- The @Prim@ newtype solves this problem. By defining the @Shape@ of some
+-- primitive type @p@ to be @Prim p@, you can use the methods @projectPrim@,
+-- @embedPrim@, @matchPrim@, and @prettyPrim@ to completely fill in the
+-- definition of the @Shaped@ class for a primitive type.
+--
+-- __Note:__ It is only appropriate to use this @Shape@ representation when a
+-- type really is primitive, in that it contains no interesting substructure.
+-- If you use the @Prim@ representation inappropriately, StrictCheck will not be
+-- able to inspect the richer structure of the type in question.
+newtype Prim (x :: Type) (f :: Type -> Type)
+  = Prim x
+  deriving (Eq, Ord, Show)
+  deriving newtype (Num)
+
+-- | Get the wrapped @x@ out of a @Prim x f@ (inverse to the @Prim@ constructor)
+unPrim :: Prim x f -> x
+unPrim (Prim x) = x
+
+-- | Generic implementation of @project@ for any primitive type whose @Shape@ is
+-- is represented as a @Prim@ newtype
+projectPrim :: (forall x. Shaped x => x -> f x) -> a -> Prim a f
+projectPrim _ = Prim
+
+-- | Generic implementation of @embed@ for any primitive type whose @Shape@ is
+-- is represented as a @Prim@ newtype
+embedPrim :: (forall x. Shaped x => f x -> x) -> Prim a f -> a
+embedPrim _ = unPrim
+
+-- | Generic implementation of @match@ for any primitive type whose @Shape@ is
+-- is represented as a @Prim@ newtype with an underlying @Eq@ instance
+matchPrim :: Eq a => Prim a f -> Prim a g
+           -> (forall xs. All Shaped xs
+                => Flattened (Prim a) f xs
+                -> Maybe (Flattened (Prim a) g xs)
+                -> result)
+           -> result
+matchPrim (Prim a) (Prim b) k =
+  k (flatPrim a)
+     (if a == b then (Just (flatPrim b)) else Nothing)
+
+-- | Helper for writing @match@ instances for primitive types which don't have
+-- @Eq@ instance
+--
+-- This generates a @Flattened@ appropriate for using in the implementation of
+-- @match@. For more documentation on how to use this, see the documentation of
+-- 'match'.
+flatPrim :: a -> Flattened (Prim a) g '[]
+flatPrim x = Flattened (const (Prim x)) Nil
+
+-- | Generic implementation of @render@ for any primitive type whose @Shape@ is
+-- is represented as a @Prim@ newtype
+renderPrim :: Show a => Prim a (K x) -> RenderLevel x
+renderPrim (Prim a) = renderConstant (show a)
+
+-- | Given some @string@, generate a custom pretty-printing representation which
+-- just shows the string
+renderConstant :: String -> RenderLevel x
+renderConstant s = CustomD 11 [Left (Left s)]
+
+-- TODO: What about demands for abstract types with > 1 type of unbounded-count field?
+
+{-
+withFieldsContainer ::
+  forall c a f result.
+     (forall r h.
+        c (h a) ->
+        (forall x. Shaped x
+           => [h x]
+           -> (forall g. [g x] -> c (g a))
+           -> r)
+        -> r)
+  -> Containing c a f
+  -> (forall xs. All Shaped xs
+        => NP f xs
+        -> (forall g. NP g xs -> Containing c a g)
+        -> result)
+  -> result
+withFieldsContainer viaContaining (Container c) cont =
+  viaContaining c $
+    \list un ->
+       withNP @Shaped list (Container . un) cont
+
+-- TODO: Make this work for any number of lists of fields, by carefully using
+-- unsafeCoerce to deal with unknown list lengths
+
+withFieldsViaList ::
+  forall demand f result.
+     (forall r h.
+        demand h ->
+        (forall x. Shaped x
+           => [h x]
+           -> (forall g. [g x] -> demand g)
+           -> r)
+        -> r)
+  -> demand f
+  -> (forall xs. All Shaped xs
+        => NP f xs
+        -> (forall g. NP g xs -> demand g)
+        -> result)
+  -> result
+withFieldsViaList viaList demand cont =
+  viaList demand $
+    \list un ->
+       withNP @Shaped list un cont
+
+withNP :: forall c demand result f x. c x
+       => [f x]
+       -> (forall g. [g x] -> demand g)
+       -> (forall xs. All c xs
+             => NP f xs -> (forall g. NP g xs -> demand g) -> result)
+       -> result
+withNP list unList cont =
+  withUnhomogenized @c list $ \np ->
+    cont np (unList . homogenize)
+
+withConcatenated :: NP (NP f) xss -> (forall xs. NP f xs -> r) -> r
+withConcatenated pop cont =
+  case pop of
+    Nil         -> cont Nil
+    (xs :* xss) -> withConcatenated xss (withPrepended xs cont)
+  where
+    withPrepended ::
+      NP f ys -> (forall zs. NP f zs -> r)
+              -> (forall zs. NP f zs -> r)
+    withPrepended pre k rest =
+      case pre of
+        Nil        -> k rest
+        (x :* xs)  -> withPrepended xs (k . (x :*)) rest
+
+homogenize :: All ((~) a) as => NP f as -> [f a]
+homogenize      Nil  = []
+homogenize (a :* as) = a : homogenize as
+
+withUnhomogenized :: forall c a f r.
+  c a => [f a] -> (forall as. (All c as, All ((~) a) as) => NP f as -> r) -> r
+withUnhomogenized      []  k = k Nil
+withUnhomogenized (a : as) k =
+  withUnhomogenized @c as $ \np -> k (a :* np)
+-}
+
+
+---------------------------------------------------
+-- Generic implementation of the Shaped methods --
+---------------------------------------------------
+
+-- | The 'Shape' used for generic implementations of 'Shaped'
+--
+-- This wraps a sum-of-products representation from "Generics.SOP".
+newtype GShape a f
+  = GS (NS (NP f) (Code a))
+
+-- | The collection of constraints necessary for a type to be given a generic
+-- implementation of the 'Shaped' methods
+type GShaped a =
+  ( Generic a
+  , Shape a ~ GShape a
+  , All2 Shaped (Code a)
+  , SListI (Code a)
+  , All SListI (Code a) )
+
+-- | Generic 'project'
+gProject :: GShaped a
+         => (forall x. Shaped x => x -> f x)
+         -> a -> Shape a f
+gProject p !(from -> sop) =
+  GS (unSOP (hcliftA (Proxy @Shaped) (p . unI) sop))
+
+-- | Generic 'embed'
+gEmbed :: GShaped a
+       => (forall x. Shaped x => f x -> x)
+       -> Shape a f -> a
+gEmbed e !(GS d) =
+  to (hcliftA (Proxy @Shaped) (I . e) (SOP d))
+
+-- | Generic 'match'
+gMatch :: forall a f g result. GShaped a
+       => Shape a f -> Shape a g
+       -> (forall xs. All Shaped xs
+             => Flattened (Shape a) f xs
+             -> Maybe (Flattened (Shape a) g xs)
+             -> result)
+       -> result
+gMatch !(GS df) !(GS dg) cont =
+  go @(Code a) df (Just dg) $ \flatF mflatG ->
+    cont (flatGD flatF) (flatGD <$> mflatG)
+  where
+    go :: forall xss r.
+      (All SListI xss, All2 Shaped xss)
+       => NS (NP f) xss
+       -> Maybe (NS (NP g) xss)
+       -> (forall xs. All Shaped xs
+             => Flattened (Flip SOP xss) f xs
+             -> Maybe (Flattened (Flip SOP xss) g xs)
+             -> r)
+       -> r
+    go (Z (fieldsF :: _ xs)) (Just (Z fieldsG)) k =
+      k @xs (flatZ fieldsF)  (Just (flatZ fieldsG))
+    go (Z (fieldsF :: _ xs)) _ k =   -- Nothing | Just (S _)
+      k @xs (flatZ fieldsF)  Nothing
+    go (S moreF) Nothing k =
+      go moreF Nothing $ \(flatF :: _ xs) _ ->
+        k @xs (flatS flatF) Nothing
+    go (S moreF) (Just (Z _)) k =
+      go moreF Nothing $ \(flatF :: _ xs) _ ->
+        k @xs (flatS flatF) Nothing
+    go (S moreF) (Just (S moreG)) k =
+      go moreF (Just moreG) $ \(flatF :: _ xs) mflatG ->
+        k @xs (flatS flatF) (flatS <$> mflatG)
+
+    flatZ
+      :: forall h xs xss. NP h xs -> Flattened (Flip SOP (xs : xss)) h xs
+    flatZ = Flattened (Flip . SOP . Z)
+
+    flatS
+      :: forall h xs xs' xss.
+      Flattened (Flip SOP xss) h xs
+      -> Flattened (Flip SOP (xs' : xss)) h xs
+    flatS (Flattened un fields) =
+      Flattened (Flip . SOP . S . coerce . un) fields
+
+    flatGD :: forall t h xs.
+      Flattened (Flip SOP (Code t)) h xs -> Flattened (GShape t) h xs
+    flatGD (Flattened un fields) =
+      Flattened (GS . coerce . un) fields
+
+-- | Generic 'render'
+gRender :: forall a x. (HasDatatypeInfo a, GShaped a)
+         => Shape a (K x) -> RenderLevel x
+gRender (GS demand) =
+  case info of
+    ADT m d cs _s ->
+      renderC m d demand cs
+    Newtype m d c ->
+      renderC m d demand (c :* Nil)
+  where
+    info = datatypeInfo (Proxy @a)
+
+    renderC :: forall as. ModuleName -> DatatypeName
+            -> NS (NP (K x)) as
+            -> NP ConstructorInfo as
+            -> RenderLevel x
+    renderC m d subShape constructors =
+      case (subShape, constructors) of
+        (Z demandFields, c :* _) ->
+          case c of
+            Constructor name ->
+              ConstructorD (m, d, name) $
+                hcollapse demandFields
+            Infix name associativity fixity ->
+              case demandFields of
+                (K a :* K b :* Nil) ->
+                  InfixD (m, d, name) associativity fixity a b
+            Record name fieldsInfo ->
+              RecordD (m, d, name) $
+                zip ( hcollapse
+                    . hliftA (\(FieldInfo f) -> K (m, d, f))
+                    $ fieldsInfo )
+                    (hcollapse demandFields)
+        (S another, _ :* different) ->
+          renderC m d another different
+
+
+---------------
+-- Instances --
+---------------
+
+instance Shaped ()
+instance Shaped Bool
+instance Shaped Ordering
+instance Shaped a => Shaped (Maybe a)
+instance (Shaped a, Shaped b) => Shaped (Either a b)
+instance Shaped a => Shaped [a]
+
+instance (Typeable a, Typeable b) => Shaped (a -> b) where
+  type Shape (a -> b) = Prim (a -> b)
+  project = projectPrim
+  embed = embedPrim
+  match (Prim f) (Prim g) k = k (flatPrim f) (Just $ flatPrim g)
+  render _ = renderConstant ("<function> :: " ++ show (typeRep @(a -> b)))
+
+instance Shaped Char where
+  type Shape Char = Prim Char
+  project = projectPrim
+  embed   = embedPrim
+  match   = matchPrim
+  render  = renderPrim
+
+instance Shaped Word where
+  type Shape Word = Prim Word
+  project = projectPrim
+  embed   = embedPrim
+  match   = matchPrim
+  render  = renderPrim
+
+instance Shaped Int where
+  type Shape Int = Prim Int
+  project = projectPrim
+  embed   = embedPrim
+  match   = matchPrim
+  render  = renderPrim
+
+instance Shaped Double where
+  type Shape Double = Prim Double
+  project = projectPrim
+  embed   = embedPrim
+  match   = matchPrim
+  render  = renderPrim
+
+instance Shaped Float where
+  type Shape Float = Prim Float
+  project = projectPrim
+  embed   = embedPrim
+  match   = matchPrim
+  render  = renderPrim
+
+instance Shaped Rational where
+  type Shape Rational = Prim Rational
+  project = projectPrim
+  embed   = embedPrim
+  match   = matchPrim
+  render  = renderPrim
+
+instance Shaped Integer where
+  type Shape Integer = Prim Integer
+  project = projectPrim
+  embed   = embedPrim
+  match   = matchPrim
+  render  = renderPrim
+
+instance (Typeable a, Eq a, Show a) => Shaped (Complex a) where
+  type Shape (Complex a) = Prim (Complex a)
+  project = projectPrim
+  embed   = embedPrim
+  match   = matchPrim
+  render  = renderPrim
+
+instance 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)

@@ -1,57 +1,57 @@-{-| The @match@ function in the typeclass 'Test.StrictCheck.Shaped.Shaped'-    allows you to uniformly operate over all the fields in a given piece of-    data--for instance, consuming them, iterating over them, counting them,-    etc. This module defines a uniform representation to allow this to work.--    This is in the nitty-gritty of how StrictCheck works: you do not need to-    understand this in order to use StrictCheck, unless you need to declare-    custom instances of @Shaped@ for a type not supported by StrictCheck's-    generics mechanism (i.e. GADTs, existential types, abstract types).--}--module Test.StrictCheck.Shaped.Flattened where--import Generics.SOP---- | The @Flattened@ type contains all the fields in a piece of data--- (represented as an n-ary product 'NP' from "Generics.SOP"), paired with a way--- to re-assemble them into a value of the original datatype.------ @Flattened d f xs@ can be read as "some value of type @d f@, which has been--- separated into an n-ary product @NP f xs@ and a function which can reconstruct--- a value @d h@ for any @h@, given an n-ary product with matching field types--- to the one contained here.------ Pay attention to the kinds! @d :: (* -> *) -> *@, @f :: * -> *@, and--- @xs :: [*]@.------ For types which are literally a collection of fields with no extra--- information, the reconstruction function merely converts the given list of--- fields back into a value of the original type. For types which contain extra--- information in their values (beyond what StrictCheck considers fields), this--- function should contain that information, and re-attach it to the field--- values it receives.-data Flattened d f xs where-  Flattened-    :: (forall h. NP h xs -> d h)-    -> NP f xs-    -> Flattened d f xs---- | Use the re-assembly close in a @Flattened@ to yield a value of the original--- type from which it was derived.-unflatten :: Flattened d f xs -> d f-unflatten (Flattened u p) = u p---- | If all the fields in a @Flattened@ satisfy some constraint, map a function--- expecting that constraint across all the fields. This may change the functor--- over which the @Flattened@ value is parameterized.-mapFlattened :: forall c d f g xs. All c xs-  => (forall x. c x => f x -> g x) -> Flattened d f xs -> Flattened d g xs-mapFlattened t (Flattened u p) =-  Flattened u (hcliftA (Proxy @c) t p)---- | 'traverseFlattened' is to 'traverse' like 'mapFlattened' is to 'fmap'.-traverseFlattened :: forall c d f g h xs. (All c xs, Applicative h)-  => (forall x. c x => f x -> h (g x)) -> Flattened d f xs -> h (Flattened d g xs)-traverseFlattened t (Flattened u p) =-  Flattened u <$> hctraverse' (Proxy @c) t p+{-| The @match@ function in the typeclass 'Test.StrictCheck.Shaped.Shaped'
+    allows you to uniformly operate over all the fields in a given piece of
+    data--for instance, consuming them, iterating over them, counting them,
+    etc. This module defines a uniform representation to allow this to work.
+
+    This is in the nitty-gritty of how StrictCheck works: you do not need to
+    understand this in order to use StrictCheck, unless you need to declare
+    custom instances of @Shaped@ for a type not supported by StrictCheck's
+    generics mechanism (i.e. GADTs, existential types, abstract types).
+-}
+
+module Test.StrictCheck.Shaped.Flattened where
+
+import Generics.SOP
+
+-- | The @Flattened@ type contains all the fields in a piece of data
+-- (represented as an n-ary product 'NP' from "Generics.SOP"), paired with a way
+-- to re-assemble them into a value of the original datatype.
+--
+-- @Flattened d f xs@ can be read as "some value of type @d f@, which has been
+-- separated into an n-ary product @NP f xs@ and a function which can reconstruct
+-- a value @d h@ for any @h@, given an n-ary product with matching field types
+-- to the one contained here.
+--
+-- Pay attention to the kinds! @d :: (Type -> Type) -> Type@, @f :: Type -> Type@,
+-- and @xs :: [Type]@.
+--
+-- For types which are literally a collection of fields with no extra
+-- information, the reconstruction function merely converts the given list of
+-- fields back into a value of the original type. For types which contain extra
+-- information in their values (beyond what StrictCheck considers fields), this
+-- function should contain that information, and re-attach it to the field
+-- values it receives.
+data Flattened d f xs where
+  Flattened
+    :: (forall h. NP h xs -> d h)
+    -> NP f xs
+    -> Flattened d f xs
+
+-- | Use the re-assembly close in a @Flattened@ to yield a value of the original
+-- type from which it was derived.
+unflatten :: Flattened d f xs -> d f
+unflatten (Flattened u p) = u p
+
+-- | If all the fields in a @Flattened@ satisfy some constraint, map a function
+-- expecting that constraint across all the fields. This may change the functor
+-- over which the @Flattened@ value is parameterized.
+mapFlattened :: forall c d f g xs. All c xs
+  => (forall x. c x => f x -> g x) -> Flattened d f xs -> Flattened d g xs
+mapFlattened t (Flattened u p) =
+  Flattened u (hcliftA (Proxy @c) t p)
+
+-- | 'traverseFlattened' is to 'traverse' like 'mapFlattened' is to 'fmap'.
+traverseFlattened :: forall c d f g h xs. (All c xs, Applicative h)
+  => (forall x. c x => f x -> h (g x)) -> Flattened d f xs -> h (Flattened d g xs)
+traverseFlattened t (Flattened u p) =
+  Flattened u <$> hctraverse' (Proxy @c) t p

@@ -1,95 +1,109 @@-{-| Template Haskell to derive pattern synonyms for working with demands--}-{-# LANGUAGE TemplateHaskell #-}-module Test.StrictCheck.TH-  ( derivePatternSynonyms-  ) where--import Generics.SOP (NP(..), NS(..))-import Test.StrictCheck.Demand-import Test.StrictCheck.Shaped--import Control.Monad (when)-import Language.Haskell.TH---- TODO: generate COMPLETE pragmas to avoid partiality warnings---- | Generates the proper type signature for a pattern. The first--- argument is the list of constructor field types, and the second--- argument is the type of the constructor constructs. This function--- inserts '->' and 'Demand' at the correct places.-patternTypeDec :: [Type] -> Type -> Type-patternTypeDec []         ty = AppT (ConT ''Demand) ty-patternTypeDec (arg:args) ty = AppT (AppT ArrowT $ AppT (ConT ''Demand) arg)-                                    (patternTypeDec args ty)--prefixPatternDec :: Int -> Name -> [Name] -> Pat -> Dec-prefixPatternDec idx patName binderNames npPat =-  PatSynD patName-          (PrefixPatSyn binderNames)-          ImplBidir-          (ConP 'Wrap [ConP 'Eval [ConP 'GS [sumPattern idx npPat]]])--infixPatternDec :: Int-                -> Name-                -> Name -> Name -- LHS then RHS-                -> Pat-                -> Dec-infixPatternDec idx patName lhsBinder rhsBinder npPat =-  PatSynD patName-          (InfixPatSyn lhsBinder rhsBinder)-          ImplBidir-          (ConP 'Wrap [ConP 'Eval [ConP 'GS [sumPattern idx npPat]]])--sumPattern :: Int -> Pat -> Pat-sumPattern idx p | idx <= 0  = ConP 'Z [p]-                 | otherwise = ConP 'S [sumPattern (idx-1) p]--productPattern :: [Type] -> Q (Pat, [Name])-productPattern []       = return (ConP 'Nil [], [])-productPattern (_:args) = do-  (tailPat, names) <- productPattern args-  freshName <- newName "x"-  return (InfixP (VarP freshName) '(:*) tailPat, freshName : names)---- | Turns a constructor into its corresponding pattern synonym--- declaration. The `Int` argument is the index of the constructor.--- For example, Nil would be the 0th constructor, and Cons would be--- the 1st constructor of the type data List a = Nil | Cons a (List a).-constructor2PatternDec :: Type -> Int -> Con -> Q (Dec, Dec)-constructor2PatternDec ty idx (NormalC conName argTypes) = do-  (npPat, names) <- productPattern (map snd argTypes)-  return (PatSynSigD patDecName (patternTypeDec (map snd argTypes) ty),-          prefixPatternDec idx patDecName names npPat)-  where patDecName = mkName (nameBase conName ++ "'")-constructor2PatternDec ty idx (InfixC argType1 conName argType2) = do-  let argTypes = [argType1, argType2]-  (npPat, names) <- productPattern (map snd argTypes)-  when (length names /= 2) $-    reportError "The impossible happened: Infix Pattern have more than 2 binders"-  let nm1:nm2:_ = names-  return (PatSynSigD patDecName (patternTypeDec (map snd argTypes) ty),-          infixPatternDec idx patDecName nm1 nm2 npPat)-  where patDecName = mkName (nameBase conName ++ "%")-constructor2PatternDec _ _ _ =-  fail "Test.StrictCheck.TH cannot derive pattern synonyms for fancy types"---- | Template Haskell splice to generate pattern synonym declarations for--- working with explicitly-represented demands on a type whose 'Shape' is--- implemented generically as a 'GShape'-derivePatternSynonyms :: Name -> Q [Dec]-derivePatternSynonyms name = do-  nameInfo <- reify name-  case nameInfo of-    TyConI (DataD _ tyName tyVars _ constrs _) -> do-      let tyVarTypes = map (\tyVar -> case tyVar of-                               PlainTV nm -> VarT nm-                               KindedTV nm kd -> SigT (VarT nm) kd-                           )-                           tyVars-          ty = foldl AppT (ConT tyName) tyVarTypes-      decs <- mapM (uncurry (constructor2PatternDec ty)) (zip [0..] constrs)-      return $ (map fst decs) ++ (map snd decs)-    _ -> do-      reportError (show name ++ " is not a data type name")-      return []+{-# LANGUAGE TemplateHaskell #-}
+
+-- | Template Haskell to derive pattern synonyms for working with demands
+module Test.StrictCheck.TH
+  ( derivePatternSynonyms,
+  )
+where
+
+import Generics.SOP (NP (..), NS (..))
+import Language.Haskell.TH
+import Test.StrictCheck.Demand
+import Test.StrictCheck.Shaped
+
+-- TODO: generate COMPLETE pragmas to avoid partiality warnings
+
+-- | Generates the proper type signature for a pattern. The first
+-- argument is the list of constructor field types, and the second
+-- argument is the type of the constructor constructs. This function
+-- inserts '->' and 'Demand' at the correct places.
+patternTypeDec :: [Type] -> Type -> Type
+patternTypeDec [] ty = AppT (ConT ''Demand) ty
+patternTypeDec (arg : args) ty =
+  AppT
+    (AppT ArrowT $ AppT (ConT ''Demand) arg)
+    (patternTypeDec args ty)
+
+prefixPatternDec :: Int -> Name -> [Name] -> Pat -> Dec
+prefixPatternDec idx patName binderNames npPat =
+  PatSynD
+    patName
+    (PrefixPatSyn binderNames)
+    ImplBidir
+    (ConP 'Wrap [] [ConP 'Eval [] [ConP 'GS [] [sumPattern idx npPat]]])
+
+infixPatternDec ::
+  Int ->
+  Name ->
+  Name ->
+  Name -> -- LHS then RHS
+  Pat ->
+  Dec
+infixPatternDec idx patName lhsBinder rhsBinder npPat =
+  PatSynD
+    patName
+    (InfixPatSyn lhsBinder rhsBinder)
+    ImplBidir
+    (ConP 'Wrap [] [ConP 'Eval [] [ConP 'GS [] [sumPattern idx npPat]]])
+
+sumPattern :: Int -> Pat -> Pat
+sumPattern idx p
+  | idx <= 0 = ConP 'Z [] [p]
+  | otherwise = ConP 'S [] [sumPattern (idx - 1) p]
+
+productPattern :: [Type] -> Q (Pat, [Name])
+productPattern [] = return (ConP 'Nil [] [], [])
+productPattern (_ : args) = do
+  (tailPat, names) <- productPattern args
+  freshName <- newName "x"
+  return (InfixP (VarP freshName) '(:*) tailPat, freshName : names)
+
+-- | Turns a constructor into its corresponding pattern synonym
+-- declaration. The `Int` argument is the index of the constructor.
+-- For example, Nil would be the 0th constructor, and Cons would be
+-- the 1st constructor of the type data List a = Nil | Cons a (List a).
+constructor2PatternDec :: Type -> Int -> Con -> Q (Dec, Dec)
+constructor2PatternDec ty idx (NormalC conName argTypes) = do
+  (npPat, names) <- productPattern (map snd argTypes)
+  return
+    ( PatSynSigD patDecName (patternTypeDec (map snd argTypes) ty),
+      prefixPatternDec idx patDecName names npPat
+    )
+  where
+    patDecName = mkName (nameBase conName ++ "'")
+constructor2PatternDec ty idx (InfixC argType1 conName argType2) = do
+  let argTypes = [argType1, argType2]
+  (npPat, names) <- productPattern (map snd argTypes)
+  case names of
+    nm1 : nm2 : [] ->
+      return
+        ( PatSynSigD patDecName (patternTypeDec (map snd argTypes) ty),
+          infixPatternDec idx patDecName nm1 nm2 npPat
+        )
+    _ -> fail "The impossible happened: Infix Pattern have more than 2 binders"
+  where
+    patDecName = mkName (nameBase conName ++ "%")
+constructor2PatternDec _ _ _ =
+  fail "Test.StrictCheck.TH cannot derive pattern synonyms for fancy types"
+
+-- | Template Haskell splice to generate pattern synonym declarations for
+-- working with explicitly-represented demands on a type whose 'Shape' is
+-- implemented generically as a 'GShape'
+derivePatternSynonyms :: Name -> Q [Dec]
+derivePatternSynonyms name = do
+  nameInfo <- reify name
+  case nameInfo of
+    TyConI (DataD _ tyName tyVars _ constrs _) -> do
+      let tyVarTypes =
+            map
+              ( \tyVar -> case tyVar of
+                  PlainTV nm _ -> VarT nm
+                  KindedTV nm _ kd -> SigT (VarT nm) kd
+              )
+              tyVars
+          ty = foldl AppT (ConT tyName) tyVarTypes
+      decs <- mapM (uncurry (constructor2PatternDec ty)) (zip [0 ..] constrs)
+      return $ (map fst decs) ++ (map snd decs)
+    _ -> do
+      reportError (show name ++ " is not a data type name")
+      return []

@@ -1,37 +1,37 @@-{-# LANGUAGE GADTs #-}--module RefTrans where--import System.Exit-import System.IO--import Test.StrictCheck--notEqualRefTrans :: Eq a => String -> a -> a -> IO Bool-notEqualRefTrans functionName x y =-  if x /= y-  then return True-  else do-    putStrLn $ "!!! " ++ functionName ++ " referentially opaque"-    return False--checkRefTrans :: IO ()-checkRefTrans = do-  let strict = snd (observe1 id (\() -> ()) ())-  let lazy   = snd (observe1 id (\_  -> ()) ())--  observe1_ok <- notEqualRefTrans "observe1" strict lazy--  let strict' = snd (observeNP id (\(I () :* Nil) -> ()) (I () :* Nil))-  let lazy'   = snd (observeNP id (\(I _  :* Nil) -> ()) (I () :* Nil))--  observe_ok <- notEqualRefTrans "observe" strict' lazy'--  let strict'' = snd (observe id (\() -> ()) ())-  let lazy''   = snd (observe id (\_  -> ()) ())--  observeNP_ok <- notEqualRefTrans "observeNP" strict'' lazy''--  if and [observe1_ok, observe_ok, observeNP_ok]-    then return ()-    else putStrLn "\n" >> hFlush stdout >> exitFailure+{-# LANGUAGE GADTs #-}
+
+module RefTrans where
+
+import System.Exit
+import System.IO
+
+import Test.StrictCheck
+
+notEqualRefTrans :: Eq a => String -> a -> a -> IO Bool
+notEqualRefTrans functionName x y =
+  if x /= y
+  then return True
+  else do
+    putStrLn $ "!!! " ++ functionName ++ " referentially opaque"
+    return False
+
+checkRefTrans :: IO ()
+checkRefTrans = do
+  let strict = snd (observe1 id (\() -> ()) ())
+  let lazy   = snd (observe1 id (\_  -> ()) ())
+
+  observe1_ok <- notEqualRefTrans "observe1" strict lazy
+
+  let strict' = snd (observeNP id (\(I () :* Nil) -> ()) (I () :* Nil))
+  let lazy'   = snd (observeNP id (\(I _  :* Nil) -> ()) (I () :* Nil))
+
+  observe_ok <- notEqualRefTrans "observe" strict' lazy'
+
+  let strict'' = snd (observe id (\() -> ()) ())
+  let lazy''   = snd (observe id (\_  -> ()) ())
+
+  observeNP_ok <- notEqualRefTrans "observeNP" strict'' lazy''
+
+  if and [observe1_ok, observe_ok, observeNP_ok]
+    then return ()
+    else putStrLn "\n" >> hFlush stdout >> exitFailure

@@ -1,38 +1,49 @@-module Specs where--import Test.QuickCheck--import Test.StrictCheck-import Test.StrictCheck.Examples.Lists-import Test.StrictCheck.Examples.Map--runSpecs :: IO ()-runSpecs = do-  putStrLn "Checking length_spec..."-  strictCheckSpecExact length_spec (length :: [Int] -> Int)--  putStrLn "Checking take_spec..."-  strictCheckSpecExact take_spec (take :: Int -> [Int] -> [Int])--  putStrLn "Checking map_spec..."-  strictCheckSpecExact map_spec (map :: (Int -> [Int]) -> [Int] -> [[Int]])--  putStrLn "Checking rot_spec..."-  strictCheckSpecExact rot_spec (rot :: [Int] -> [Int] -> [Int])--  putStrLn "Checking append_spec..."-  strictCheckSpecExact append_spec ((++) :: [Int] -> [Int] -> [Int])--  putStrLn "Checking reverse_spec..."-  strictCheckSpecExact reverse_spec (reverse :: [Int] -> [Int])--  putStrLn "Checking knapsack..."-  strictCheckWithResults-    stdArgs{maxSize=100, maxSuccess=500}-    shrinkViaArbitrary-    genViaProduce-    strictnessViaSized-    iterSolution_spec-    iterSolutionWithKey >>= print--  return ()+module Specs where
+
+import Test.QuickCheck
+
+import Test.StrictCheck
+import Test.StrictCheck.Examples.Lists
+import Test.StrictCheck.Examples.Map
+
+import Control.Monad (when)
+import GHC.IO.Encoding (textEncodingName)
+import System.IO
+
+runSpecs :: IO ()
+runSpecs = do
+  putStrLn "Checking length_spec..."
+  strictCheckSpecExact length_spec (length :: [Int] -> Int)
+
+  putStrLn "Checking take_spec..."
+  strictCheckSpecExact take_spec (take :: Int -> [Int] -> [Int])
+
+  putStrLn "Checking map_spec..."
+  strictCheckSpecExact map_spec (map :: (Int -> [Int]) -> [Int] -> [[Int]])
+
+  putStrLn "Checking rot_spec..."
+  strictCheckSpecExact rot_spec (rot :: [Int] -> [Int] -> [Int])
+
+  putStrLn "Checking append_spec..."
+  strictCheckSpecExact append_spec ((++) :: [Int] -> [Int] -> [Int])
+
+  putStrLn "Checking reverse_spec..."
+  strictCheckSpecExact reverse_spec (reverse :: [Int] -> [Int])
+
+  putStrLn "Checking knapsack..."
+  strictCheckWithResults
+    stdArgs{maxSize=100, maxSuccess=500}
+    shrinkViaArbitrary
+    genViaProduce
+    strictnessViaSized
+    iterSolution_spec
+    iterSolutionWithKey >>= print
+
+  putStrLn "Checking bad_length_spec (failure is expected!)..."
+  strictCheckSpecExact bad_length_spec (length :: [Int] -> Int)
+
+  enc <- hGetEncoding stdout
+  when (fmap textEncodingName enc == Just "UTF-8") $ do
+    hSetEncoding stdout latin1
+    putStrLn "Checking bad_length_spec without Unicode output (failure is expected!)..."
+    strictCheckSpecExact bad_length_spec (length :: [Int] -> Int)

@@ -1,11 +1,11 @@-module Main where--import Specs-import RefTrans--main :: IO ()-main = do-  -- specification unit tests-  runSpecs-  -- regression test for issue #2 (CSE breaks referential transparency)-  checkRefTrans+module Main where
+
+import Specs
+import RefTrans
+
+main :: IO ()
+main = do
+  -- specification unit tests
+  runSpecs
+  -- regression test for issue #2 (CSE breaks referential transparency)
+  checkRefTrans