{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Useful properties for debugging custom @HasSpec@ instances.
module Constrained.Properties where

import Constrained.Base
import Constrained.Internals
import Constrained.List
import Data.Map (Map)
import Data.Typeable
import Prettyprinter
import Test.QuickCheck qualified as QC

forAllSpecShow ::
  (HasSpec fn a, QC.Testable p) => Specification fn a -> (a -> String) -> (a -> p) -> QC.Property
forAllSpecShow :: forall (fn :: [*] -> * -> *) a p.
(HasSpec fn a, Testable p) =>
Specification fn a -> (a -> String) -> (a -> p) -> Property
forAllSpecShow Specification fn a
spec a -> String
pp a -> p
prop =
  let sspec :: Specification fn a
sspec = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Specification fn a
simplifySpec Specification fn a
spec
   in forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property
QC.forAllShrinkShow (forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec Specification fn a
sspec) (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec Specification fn a
sspec) a -> String
pp forall a b. (a -> b) -> a -> b
$ \a
a ->
        forall (fn :: [*] -> * -> *) p a.
(FunctionLike fn, Testable p) =>
Specification fn a -> a -> p -> Property
monitorSpec Specification fn a
spec a
a forall a b. (a -> b) -> a -> b
$ a -> p
prop a
a

forAllSpec :: (HasSpec fn a, QC.Testable p) => Specification fn a -> (a -> p) -> QC.Property
forAllSpec :: forall (fn :: [*] -> * -> *) a p.
(HasSpec fn a, Testable p) =>
Specification fn a -> (a -> p) -> Property
forAllSpec Specification fn a
spec a -> p
prop = forall (fn :: [*] -> * -> *) a p.
(HasSpec fn a, Testable p) =>
Specification fn a -> (a -> String) -> (a -> p) -> Property
forAllSpecShow Specification fn a
spec forall a. Show a => a -> String
show a -> p
prop

forAllSpecDiscard :: (HasSpec fn a, QC.Testable p) => Specification fn a -> (a -> p) -> QC.Property
forAllSpecDiscard :: forall (fn :: [*] -> * -> *) a p.
(HasSpec fn a, Testable p) =>
Specification fn a -> (a -> p) -> Property
forAllSpecDiscard Specification fn a
spec a -> p
prop =
  let sspec :: Specification fn a
sspec = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Specification fn a
simplifySpec Specification fn a
spec
   in forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
QC.forAllShrinkBlind
        (forall (m :: * -> *) a. GenT m a -> Gen (m a)
strictGen forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT @_ @_ @GE Specification fn a
sspec)
        (forall a b. (a -> b) -> [a] -> [b]
map forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec Specification fn a
sspec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. GE a -> a
errorGE)
        forall a b. (a -> b) -> a -> b
$ \GE a
ge ->
          forall p. Testable p => GE p -> Property
fromGEDiscard forall a b. (a -> b) -> a -> b
$ do
            a
a <- GE a
ge
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
QC.counterexample (forall a. Show a => a -> String
show a
a) forall a b. (a -> b) -> a -> b
$ a -> p
prop a
a

prop_sound ::
  HasSpec fn a =>
  Specification fn a ->
  QC.Property
prop_sound :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Property
prop_sound Specification fn a
spec =
  forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
QC.forAllBlind (forall (m :: * -> *) a. GenT m a -> Gen (m a)
strictGen forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT Specification fn a
spec) forall a b. (a -> b) -> a -> b
$ \GE a
ma ->
    case GE a
ma of
      Result [NonEmpty String]
_ a
a ->
        forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
QC.cover Double
80 Bool
True String
"successful" forall a b. (a -> b) -> a -> b
$
          forall prop. Testable prop => String -> prop -> Property
QC.counterexample (forall a. Show a => a -> String
show a
a) forall a b. (a -> b) -> a -> b
$
            forall (fn :: [*] -> * -> *) p a.
(FunctionLike fn, Testable p) =>
Specification fn a -> a -> p -> Property
monitorSpec Specification fn a
spec a
a forall a b. (a -> b) -> a -> b
$
              forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Property
conformsToSpecProp a
a Specification fn a
spec
      GE a
_ -> forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
QC.cover Double
80 Bool
False String
"successful" Bool
True

prop_constrained_satisfies_sound :: HasSpec fn a => Specification fn a -> QC.Property
prop_constrained_satisfies_sound :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Property
prop_constrained_satisfies_sound Specification fn a
spec = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Property
prop_sound (forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn a
a -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn a
a Specification fn a
spec)

-- | `prop_complete ps` assumes that `ps` is satisfiable
prop_complete :: HasSpec fn a => Specification fn a -> QC.Property
prop_complete :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Property
prop_complete Specification fn a
s =
  forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
QC.forAllBlind (forall (m :: * -> *) a. GenT m a -> Gen (m a)
strictGen forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT Specification fn a
s) forall a b. (a -> b) -> a -> b
$ \GE a
ma -> forall p. Testable p => GE p -> Property
fromGEProp forall a b. (a -> b) -> a -> b
$ do
    a
a <- GE a
ma
    -- Force the value to make sure we don't crash with `error` somewhere
    -- or fall into an inifinite loop
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Show a => a -> String
show a
a) forall a. Ord a => a -> a -> Bool
> Int
0

prop_constrained_satisfies_complete :: HasSpec fn a => Specification fn a -> QC.Property
prop_constrained_satisfies_complete :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Property
prop_constrained_satisfies_complete Specification fn a
spec = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Property
prop_complete (forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn a
a -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn a
a Specification fn a
spec)

prop_shrink_sound :: HasSpec fn a => Specification fn a -> QC.Property
prop_shrink_sound :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Property
prop_shrink_sound Specification fn a
s =
  forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
QC.forAll (forall (m :: * -> *) a. GenT m a -> Gen (m a)
strictGen forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT Specification fn a
s) forall a b. (a -> b) -> a -> b
$ \GE a
ma -> forall p. Testable p => GE p -> Property
fromGEDiscard forall a b. (a -> b) -> a -> b
$ do
    a
a <- GE a
ma
    let shrinks :: [a]
shrinks = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec Specification fn a
s a
a
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
      forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
QC.cover Double
40 (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
shrinks) String
"non-null shrinks" forall a b. (a -> b) -> a -> b
$
        if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
shrinks
          then forall prop. Testable prop => prop -> Property
QC.property Bool
True
          else forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
QC.forAll (forall a. HasCallStack => [a] -> Gen a
QC.elements [a]
shrinks) forall a b. (a -> b) -> a -> b
$ \a
a' ->
            forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Property
conformsToSpecProp a
a' Specification fn a
s

prop_conformEmpty ::
  forall fn a.
  HasSpec fn a =>
  a ->
  QC.Property
prop_conformEmpty :: forall (fn :: [*] -> * -> *) a. HasSpec fn a => a -> Property
prop_conformEmpty a
a = forall prop. Testable prop => prop -> Property
QC.property forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasCallStack) =>
a -> TypeSpec fn a -> Bool
conformsTo @fn a
a (forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a
emptySpec @fn @a)

prop_univSound :: forall fn. TestableFn fn -> QC.Property
prop_univSound :: forall (fn :: [*] -> * -> *). TestableFn fn -> Property
prop_univSound (TestableFn fn as b
fn) =
  forall prop. Testable prop => String -> prop -> Property
QC.label (forall a. Show a => a -> String
show fn as b
fn) forall a b. (a -> b) -> a -> b
$
    forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
QC.forAllShrinkBlind forall a. Arbitrary a => Gen a
QC.arbitrary forall a. Arbitrary a => a -> [a]
QC.shrink forall a b. (a -> b) -> a -> b
$ \(TestableCtx ListCtx Value as (HOLE a)
ctx :: TestableCtx fn as) ->
      forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
QC.forAllShrinkBlind forall a. Arbitrary a => Gen a
QC.arbitrary forall a. Arbitrary a => a -> [a]
QC.shrink forall a b. (a -> b) -> a -> b
$ \(Specification fn b
spec :: Specification fn a) ->
        forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"\nfn ctx = " forall a. [a] -> [a] -> [a]
++ forall (fn :: [*] -> * -> *) (as :: [*]) b.
(Typeable as, TypeList as, All (HasSpec fn) as, HasSpec fn b) =>
fn as b -> TestableCtx fn as -> String
showCtxWith fn as b
fn (forall (fn :: [*] -> * -> *) as (as :: [*]).
HasSpec fn as =>
ListCtx Value as (HOLE as) -> TestableCtx fn as
TestableCtx ListCtx Value as (HOLE a)
ctx)) forall a b. (a -> b) -> a -> b
$
          forall prop. Testable prop => String -> prop -> Property
QC.counterexample (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"\nspec =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Specification fn b
spec) forall a b. (a -> b) -> a -> b
$
            let sspec :: Specification fn a
sspec = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Specification fn a
simplifySpec (forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) a b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn a,
 HasSpec fn b, All (HasSpec fn) as) =>
f as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun fn as b
fn ListCtx Value as (HOLE a)
ctx Specification fn b
spec)
             in forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Doc Any
"propagateSpecFun fn ctx spec =" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall a ann. Pretty a => a -> Doc ann
pretty Specification fn a
sspec)) forall a b. (a -> b) -> a -> b
$
                  forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (fn :: [*] -> * -> *) a ann.
HasSpec fn a =>
Specification fn a -> Doc ann
prettyPlan Specification fn a
sspec)) forall a b. (a -> b) -> a -> b
$
                    forall prop. Testable prop => Int -> prop -> Property
QC.within Int
10_000_000 forall a b. (a -> b) -> a -> b
$
                      forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
QC.forAllBlind (forall (m :: * -> *) a. GenT m a -> Gen (m a)
strictGen forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT @_ @_ Specification fn a
sspec) forall a b. (a -> b) -> a -> b
$ \GE a
ge ->
                        forall p. Testable p => GE p -> Property
fromGEDiscard forall a b. (a -> b) -> a -> b
$ do
                          a
a <- GE a
ge
                          let res :: b
res = forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
uncurryList_ forall a. Value a -> a
unValue (forall (fn :: [*] -> * -> *) (as :: [*]) b.
FunctionLike fn =>
fn as b -> FunTy as b
sem fn as b
fn) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (as :: [*]) (c :: * -> *).
ListCtx f as c -> (forall a. c a -> f a) -> List f as
fillListCtx ListCtx Value as (HOLE a)
ctx forall a b. (a -> b) -> a -> b
$ \HOLE a a
HOLE -> forall a. Show a => a -> Value a
Value a
a
                          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
                            forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"\ngenerated value: a = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
a) forall a b. (a -> b) -> a -> b
$
                              forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"\nfn ctx[a] = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show b
res) forall a b. (a -> b) -> a -> b
$
                                forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Property
conformsToSpecProp b
res Specification fn b
spec

prop_gen_sound :: forall fn a. HasSpec fn a => Specification fn a -> QC.Property
prop_gen_sound :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Property
prop_gen_sound Specification fn a
spec =
  let sspec :: Specification fn a
sspec = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Specification fn a
simplifySpec Specification fn a
spec
   in forall prop.
Testable prop =>
String -> [String] -> prop -> Property
QC.tabulate String
"specType spec" [forall (fn :: [*] -> * -> *) a. Specification fn a -> String
specType Specification fn a
spec] forall a b. (a -> b) -> a -> b
$
        forall prop.
Testable prop =>
String -> [String] -> prop -> Property
QC.tabulate String
"specType (simplifySpec spec)" [forall (fn :: [*] -> * -> *) a. Specification fn a -> String
specType Specification fn a
sspec] forall a b. (a -> b) -> a -> b
$
          forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (fn :: [*] -> * -> *) a ann.
HasSpec fn a =>
Specification fn a -> Doc ann
prettyPlan Specification fn a
sspec)) forall a b. (a -> b) -> a -> b
$
            forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
QC.forAllBlind (forall (m :: * -> *) a. GenT m a -> Gen (m a)
strictGen forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT @_ @_ @GE Specification fn a
sspec) forall a b. (a -> b) -> a -> b
$ \GE a
ge ->
              forall p. Testable p => GE p -> Property
fromGEDiscard forall a b. (a -> b) -> a -> b
$ do
                a
a <- GE a
ge
                forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
                  forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"\ngenerated value: a = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
a) forall a b. (a -> b) -> a -> b
$
                    forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Property
conformsToSpecProp a
a Specification fn a
spec

specType :: Specification fn a -> String
specType :: forall (fn :: [*] -> * -> *) a. Specification fn a -> String
specType TrueSpec {} = String
"TrueSpec"
specType SuspendedSpec {} = String
"SuspendedSpec"
specType ErrorSpec {} = String
"ErrorSpec"
specType MemberSpec {} = String
"MemberSpec"
specType TypeSpec {} = String
"TypeSpec"

showCtxWith ::
  forall fn as b.
  (Typeable as, TypeList as, All (HasSpec fn) as, HasSpec fn b) =>
  fn as b ->
  TestableCtx fn as ->
  String
showCtxWith :: forall (fn :: [*] -> * -> *) (as :: [*]) b.
(Typeable as, TypeList as, All (HasSpec fn) as, HasSpec fn b) =>
fn as b -> TestableCtx fn as -> String
showCtxWith fn as b
fn (TestableCtx ListCtx Value as (HOLE a)
ctx) = forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty Term fn b
tm
  where
    tm :: Term fn b
    tm :: Term fn b
tm =
      forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
FunTy (MapList f ts) r -> List f ts -> r
uncurryList (forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app fn as b
fn) forall a b. (a -> b) -> a -> b
$
        forall (f :: * -> *) (as :: [*]) (c :: * -> *).
ListCtx f as c -> (forall a. c a -> f a) -> List f as
fillListCtx (forall (c :: * -> Constraint) (as :: [*]) (f :: * -> *)
       (g :: * -> *) (h :: * -> *).
All c as =>
(forall a. c a => f a -> g a) -> ListCtx f as h -> ListCtx g as h
mapListCtxC @(HasSpec fn) (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit @_ @fn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Value a -> a
unValue) ListCtx Value as (HOLE a)
ctx) (\HOLE a a
HOLE -> forall (fn :: [*] -> * -> *) a. HasSpec fn a => Var a -> Term fn a
V forall a b. (a -> b) -> a -> b
$ forall a. Int -> String -> Var a
Var Int
0 String
"v")

data TestableFn fn where
  TestableFn ::
    ( All (HasSpec fn) as
    , TypeList as
    , HasSpec fn b
    , Typeable as
    , QC.Arbitrary (Specification fn b)
    , Typeable (FunTy as b)
    ) =>
    fn as b ->
    TestableFn fn

instance BaseUniverse fn => Show (TestableFn fn) where
  show :: TestableFn fn -> String
show (TestableFn (fn as b
fn :: fn as b)) =
    forall a. Show a => a -> String
show fn as b
fn forall a. [a] -> [a] -> [a]
++ String
" :: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: FunTy as b))

data TestableCtx fn as where
  TestableCtx ::
    HasSpec fn a =>
    ListCtx Value as (HOLE a) ->
    TestableCtx fn as

instance forall fn as. (All (HasSpec fn) as, TypeList as) => QC.Arbitrary (TestableCtx fn as) where
  arbitrary :: Gen (TestableCtx fn as)
arbitrary = do
    let shape :: List (Const ()) as
shape = forall (as :: [*]). TypeList as => List (Const ()) as
listShape @as
    Int
idx <- forall a. Random a => (a, a) -> Gen a
QC.choose (Int
0, forall {k} (f :: k -> *) (as :: [k]). List f as -> Int
lengthList List (Const ()) as
shape forall a. Num a => a -> a -> a
- Int
1)
    forall (f :: * -> *) (as' :: [*]).
All (HasSpec fn) as' =>
Int -> List f as' -> Gen (TestableCtx fn as')
go Int
idx List (Const ()) as
shape
    where
      go :: forall f as'. All (HasSpec fn) as' => Int -> List f as' -> QC.Gen (TestableCtx fn as')
      go :: forall (f :: * -> *) (as' :: [*]).
All (HasSpec fn) as' =>
Int -> List f as' -> Gen (TestableCtx fn as')
go Int
0 (f a
_ :> List f as1
as) =
        forall (fn :: [*] -> * -> *) as (as :: [*]).
HasSpec fn as =>
ListCtx Value as (HOLE as) -> TestableCtx fn as
TestableCtx forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. HOLE a a
HOLE forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:?) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (c :: k -> Constraint) (as :: [k]) (f :: k -> *)
       (g :: k -> *) (m :: * -> *).
(Applicative m, All c as) =>
(forall (a :: k). c a => f a -> m (g a))
-> List f as -> m (List g as)
mapMListC @(HasSpec fn) (\f a
_ -> forall a. Show a => a -> Value a
Value forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec) List f as1
as
      go Int
n (f a
_ :> List f as1
as) = do
        TestableCtx ListCtx Value as1 (HOLE a)
ctx <- forall (f :: * -> *) (as' :: [*]).
All (HasSpec fn) as' =>
Int -> List f as' -> Gen (TestableCtx fn as')
go (Int
n forall a. Num a => a -> a -> a
- Int
1) List f as1
as
        forall (fn :: [*] -> * -> *) as (as :: [*]).
HasSpec fn as =>
ListCtx Value as (HOLE as) -> TestableCtx fn as
TestableCtx forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (f :: * -> *) a (as1 :: [*]) (c :: * -> *).
f a -> ListCtx f as1 c -> ListCtx f (a : as1) c
:! ListCtx Value as1 (HOLE a)
ctx) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> Value a
Value forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
      go Int
_ List f as'
_ = forall a. HasCallStack => String -> a
error String
"The impossible happened in Arbitrary for TestableCtx"

  shrink :: TestableCtx fn as -> [TestableCtx fn as]
shrink (TestableCtx ListCtx Value as (HOLE a)
ctx) = forall (fn :: [*] -> * -> *) as (as :: [*]).
HasSpec fn as =>
ListCtx Value as (HOLE as) -> TestableCtx fn as
TestableCtx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: * -> *) (as' :: [*]).
All (HasSpec fn) as' =>
ListCtx Value as' c -> [ListCtx Value as' c]
shrinkCtx ListCtx Value as (HOLE a)
ctx
    where
      shrinkCtx :: forall c as'. All (HasSpec fn) as' => ListCtx Value as' c -> [ListCtx Value as' c]
      shrinkCtx :: forall (c :: * -> *) (as' :: [*]).
All (HasSpec fn) as' =>
ListCtx Value as' c -> [ListCtx Value as' c]
shrinkCtx (c a
c :? List Value as1
as) = (c a
c forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:?) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (as' :: [*]).
All (HasSpec fn) as' =>
List Value as' -> [List Value as']
go List Value as1
as
      shrinkCtx (Value a
a :! ListCtx Value as1 c
ctx') = forall a b. (a -> b) -> [a] -> [b]
map ((forall (f :: * -> *) a (as1 :: [*]) (c :: * -> *).
f a -> ListCtx f as1 c -> ListCtx f (a : as1) c
:! ListCtx Value as1 c
ctx') forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> Value a
Value) (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec @fn forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec a
a) forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Show a => a -> Value a
Value a
a forall (f :: * -> *) a (as1 :: [*]) (c :: * -> *).
f a -> ListCtx f as1 c -> ListCtx f (a : as1) c
:!) (forall (c :: * -> *) (as' :: [*]).
All (HasSpec fn) as' =>
ListCtx Value as' c -> [ListCtx Value as' c]
shrinkCtx ListCtx Value as1 c
ctx')

      go :: forall as'. All (HasSpec fn) as' => List Value as' -> [List Value as']
      go :: forall (as' :: [*]).
All (HasSpec fn) as' =>
List Value as' -> [List Value as']
go List Value as'
Nil = []
      go (Value a
a :> List Value as1
as) = forall a b. (a -> b) -> [a] -> [b]
map ((forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Value as1
as) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> Value a
Value) (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec @fn forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec a
a) forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Show a => a -> Value a
Value a
a forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:>) (forall (as' :: [*]).
All (HasSpec fn) as' =>
List Value as' -> [List Value as']
go List Value as1
as)

-- TODO: we should improve these
instance fn ~ BaseFn => QC.Arbitrary (TestableFn fn) where
  arbitrary :: Gen (TestableFn fn)
arbitrary =
    forall a. HasCallStack => [a] -> Gen a
QC.elements
      [ forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a. NumLike fn a => fn '[a, a] a
addFn @fn @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a. NumLike fn a => fn '[a] a
negateFn @fn @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, Member (SizeFn fn) fn, Sized a) =>
fn '[a] Integer
sizeOfFn @fn @(Map Int Int)
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(Member (SetFn fn) fn, Ord a) =>
fn '[a, Set a] Bool
memberFn @fn @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *).
Member (BoolFn fn) fn =>
fn '[Bool] Bool
notFn @fn
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(Member (SetFn fn) fn, Ord a) =>
fn '[Set a, Set a] Bool
disjointFn @fn @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(Member (SetFn fn) fn, Ord a) =>
fn '[Set a, Set a] Bool
subsetFn @fn @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(Member (SetFn fn) fn, Ord a) =>
fn '[Set a, Set a] Bool
subsetFn @fn @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(Member (SetFn fn) fn, Eq a) =>
fn '[a, [a]] Bool
elemFn @fn @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *).
Member (BoolFn fn) fn =>
fn '[Bool, Bool] Bool
orFn @fn
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(Ord a, OrdLike fn a) =>
fn '[a, a] Bool
lessFn @fn @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(Ord a, OrdLike fn a) =>
fn '[a, a] Bool
lessOrEqualFn @fn @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(Eq a, Member (EqFn fn) fn) =>
fn '[a, a] Bool
equalFn @fn @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] a
fstFn @fn @Int @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] b
sndFn @fn @Int @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[a, b] (Prod a b)
pairFn @fn @Int @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a b.
Member (SumFn fn) fn =>
fn '[b] (Sum a b)
injRightFn @fn @Int @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(Member (SetFn fn) fn, Ord a) =>
fn '[a] (Set a)
singletonFn @fn @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(Member (SetFn fn) fn, Ord a) =>
fn '[Set a, Set a] (Set a)
unionFn @fn @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, Foldy fn b, Show (fn '[a] b), Eq (fn '[a] b)) =>
fn '[a] b -> fn '[[a]] b
foldMapFn @fn @Int forall (fn :: [*] -> * -> *) a. Member (FunFn fn) fn => fn '[a] a
idFn
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) k v.
Member (MapFn fn) fn =>
fn '[Map k v] [v]
rngFn @fn @Int @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) k v.
(Member (MapFn fn) fn, Ord k) =>
fn '[Map k v] (Set k)
domFn @fn @Int @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(Member (SetFn fn) fn, Ord a) =>
fn '[[a]] (Set a)
fromListFn @fn @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) k v.
(Member (MapFn fn) fn, Ord k) =>
fn '[k, Map k v] (Maybe v)
lookupFn @fn @Int @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a. HasSpec fn a => fn '[a] [a]
singletonListFn @fn @Int
      , forall (fn :: [*] -> * -> *) (as :: [*]) b.
(All (HasSpec fn) as, TypeList as, HasSpec fn b, Typeable as,
 Arbitrary (Specification fn b), Typeable (FunTy as b)) =>
fn as b -> TestableFn fn
TestableFn forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a. HasSpec fn a => fn '[[a], [a]] [a]
appendFn @fn @Int
      ]

prop_mapSpec ::
  ( HasSpec fn a
  , HasSpec fn b
  ) =>
  fn '[a] b ->
  Specification fn a ->
  QC.Property
prop_mapSpec :: forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
fn '[a] b -> Specification fn a -> Property
prop_mapSpec fn '[a] b
fn Specification fn a
spec =
  forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
QC.forAll (forall (m :: * -> *) a. GenT m a -> Gen (m a)
strictGen forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT Specification fn a
spec) forall a b. (a -> b) -> a -> b
$ \GE a
ma -> forall p. Testable p => GE p -> Property
fromGEDiscard forall a b. (a -> b) -> a -> b
$ do
    a
a <- GE a
ma
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
conformsToSpec (forall (fn :: [*] -> * -> *) (as :: [*]) b.
FunctionLike fn =>
fn as b -> FunTy as b
sem fn '[a] b
fn a
a) (forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
fn '[a] b -> Specification fn a -> Specification fn b
mapSpec fn '[a] b
fn Specification fn a
spec)

prop_propagateSpecSound ::
  ( HasSpec fn a
  , HasSpec fn b
  ) =>
  fn '[a] b ->
  b ->
  QC.Property
prop_propagateSpecSound :: forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
fn '[a] b -> b -> Property
prop_propagateSpecSound fn '[a] b
fn b
b =
  forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
QC.forAll (forall (m :: * -> *) a. GenT m a -> Gen (m a)
strictGen forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (fn :: [*] -> * -> *) a b.
(MonadGenError m, HasSpec fn a, Show b, Functions fn fn,
 HasSpec fn b) =>
fn '[a] b -> Specification fn a -> b -> GenT m a
genInverse fn '[a] b
fn forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec b
b) forall a b. (a -> b) -> a -> b
$ \GE a
ma -> forall p. Testable p => GE p -> Property
fromGEDiscard forall a b. (a -> b) -> a -> b
$ do
    a
a <- GE a
ma
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) (as :: [*]) b.
FunctionLike fn =>
fn as b -> FunTy as b
sem fn '[a] b
fn a
a forall a. Eq a => a -> a -> Bool
== b
b