{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# 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.API
import Constrained.Base (
  AppRequires,
  BaseW (..),
  HOLE (..),
  appTerm,
  (/>),
 )
import Constrained.Conformance (
  monitorSpec,
 )
import Constrained.Core (
  Value (..),
  Var (..),
  unValue,
 )
import Constrained.GenT (
  GE (..),
  errorGE,
  fromGEDiscard,
  fromGEProp,
  strictGen,
 )
import Constrained.List (
  All,
  FunTy,
  List (..),
  ListCtx (..),
  TypeList,
  fillListCtx,
  lengthList,
  listShape,
  mapListCtxC,
  mapMListC,
  uncurryList,
  uncurryList_,
 )
import Constrained.NumSpec (
  IntW (..),
  NumOrdW (..),
 )
import Constrained.Spec.Map (
  MapW (..),
 )
import Constrained.Spec.Set ()
import Constrained.Spec.SumProd ()
import Constrained.TheKnot (
  BoolW (..),
  ElemW (..),
  EqW (..),
  FunW (..),
  ListW (..),
  ProdW (..),
  SizeW (..),
  SumW (..),
  genInverse,
  mapSpec,
  prettyPlan,
  shrinkWithSpec,
 )

import qualified Data.List.NonEmpty as NE
import Data.Map (Map)
import Data.Typeable (Typeable, typeOf)
import Prettyprinter
import qualified Test.QuickCheck as QC

conformsToSpecProp :: forall a. HasSpec a => a -> Specification a -> QC.Property
conformsToSpecProp :: forall a. HasSpec a => a -> Specification a -> Property
conformsToSpecProp a
a Specification a
s = case forall a.
HasSpec a =>
a -> Specification a -> NonEmpty String -> Maybe (NonEmpty String)
conformsToSpecE a
a (forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification a
s) (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"call to conformsToSpecProp") of
  Maybe (NonEmpty String)
Nothing -> forall prop. Testable prop => prop -> Property
QC.property Bool
True
  Just NonEmpty String
msgs -> forall prop. Testable prop => String -> prop -> Property
QC.counterexample ([String] -> String
unlines (forall a. NonEmpty a -> [a]
NE.toList NonEmpty String
msgs)) Bool
False

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

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

forAllSpecDiscard :: (HasSpec a, QC.Testable p) => Specification a -> (a -> p) -> QC.Property
forAllSpecDiscard :: forall a p.
(HasSpec a, Testable p) =>
Specification a -> (a -> p) -> Property
forAllSpecDiscard Specification a
spec a -> p
prop =
  let sspec :: Specification a
sspec = forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification 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 a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT @_ @GE Specification 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 a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification 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 a =>
  Specification a ->
  QC.Property
prop_sound :: forall a. HasSpec a => Specification a -> Property
prop_sound Specification 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 a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
spec) forall a b. (a -> b) -> a -> b
$ \GE a
ma ->
    case GE a
ma of
      Result 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 p a. Testable p => Specification a -> a -> p -> Property
monitorSpec Specification a
spec a
a forall a b. (a -> b) -> a -> b
$
              forall a. HasSpec a => a -> Specification a -> Property
conformsToSpecProp a
a Specification 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 a => Specification a -> QC.Property
prop_constrained_satisfies_sound :: forall a. HasSpec a => Specification a -> Property
prop_constrained_satisfies_sound Specification a
spec = forall a. HasSpec a => Specification a -> Property
prop_sound (forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term a
a -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term a
a Specification a
spec)

prop_constrained_explained :: HasSpec a => Specification a -> QC.Property
prop_constrained_explained :: forall a. HasSpec a => Specification a -> Property
prop_constrained_explained Specification a
spec =
  forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
QC.forAll forall a. Arbitrary a => Gen a
QC.arbitrary forall a b. (a -> b) -> a -> b
$ \NonEmpty String
es ->
    forall a. HasSpec a => Specification a -> Property
prop_sound forall a b. (a -> b) -> a -> b
$ forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term a
x -> NonEmpty String -> Pred -> Pred
Explain NonEmpty String
es forall a b. (a -> b) -> a -> b
$ Term a
x forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
spec

-- | `prop_complete ps` assumes that `ps` is satisfiable
prop_complete :: HasSpec a => Specification a -> QC.Property
prop_complete :: forall a. HasSpec a => Specification a -> Property
prop_complete Specification 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 a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification 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 a => Specification a -> QC.Property
prop_constrained_satisfies_complete :: forall a. HasSpec a => Specification a -> Property
prop_constrained_satisfies_complete Specification a
spec = forall a. HasSpec a => Specification a -> Property
prop_complete (forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term a
a -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term a
a Specification a
spec)

prop_shrink_sound :: HasSpec a => Specification a -> QC.Property
prop_shrink_sound :: forall a. HasSpec a => Specification a -> Property
prop_shrink_sound Specification 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 a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification 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 a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification 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 a. HasSpec a => a -> Specification a -> Property
conformsToSpecProp a
a' Specification a
s

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

prop_univSound :: TestableFn -> QC.Property
prop_univSound :: TestableFn -> Property
prop_univSound (TestableFn t as b
fn) =
  forall prop. Testable prop => String -> prop -> Property
QC.label (forall a. Show a => a -> String
show t 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
$ \tc :: TestableCtx as
tc@(TestableCtx ListCtx Value as (HOLE a)
ctx) ->
      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 b
spec ->
        forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"\nfn ctx = " forall a. [a] -> [a] -> [a]
++ forall (fn :: [*] -> * -> *) (as :: [*]) b.
AppRequires fn as b =>
fn as b -> TestableCtx as -> String
showCtxWith t as b
fn TestableCtx as
tc) 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 b
spec) forall a b. (a -> b) -> a -> b
$
            let sspec :: Specification a
sspec = forall a. HasSpec a => Specification a -> Specification a
simplifySpec (forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
propagate t as b
fn ListCtx Value as (HOLE a)
ctx Specification 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
"propagate ctx spec =" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall a ann. Pretty a => a -> Doc ann
pretty Specification 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 a ann. HasSpec a => Specification a -> Doc ann
prettyPlan Specification a
sspec)) forall a b. (a -> b) -> a -> b
$
                    forall prop. Testable prop => Int -> prop -> Property
QC.within Int
20_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 a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification 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 (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t 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 a. HasSpec a => a -> Specification a -> Property
conformsToSpecProp b
res Specification b
spec
main :: IO ()
main :: IO ()
main = forall prop. Testable prop => prop -> IO ()
QC.quickCheck (forall prop. Testable prop => Int -> prop -> Property
QC.withMaxSuccess Int
10000 TestableFn -> Property
prop_univSound)

prop_gen_sound :: forall a. HasSpec a => Specification a -> QC.Property
prop_gen_sound :: forall a. HasSpec a => Specification a -> Property
prop_gen_sound Specification a
spec =
  let sspec :: Specification a
sspec = forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification a
spec
   in forall prop.
Testable prop =>
String -> [String] -> prop -> Property
QC.tabulate String
"specType spec" [forall a. Specification a -> String
specType Specification a
spec] forall a b. (a -> b) -> a -> b
$
        forall prop.
Testable prop =>
String -> [String] -> prop -> Property
QC.tabulate String
"specType (simplifySpec spec)" [forall a. Specification a -> String
specType Specification 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 a ann. HasSpec a => Specification a -> Doc ann
prettyPlan Specification 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 a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT @a @GE Specification 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 a. HasSpec a => a -> Specification a -> Property
conformsToSpecProp a
a Specification a
spec

specType :: Specification a -> String
specType :: forall a. Specification a -> String
specType (ExplainSpec [] Specification a
s) = forall a. Specification a -> String
specType Specification a
s
specType (ExplainSpec [String]
_ Specification a
s) = String
"(ExplainSpec " forall a. [a] -> [a] -> [a]
++ forall a. Specification a -> String
specType Specification a
s forall a. [a] -> [a] -> [a]
++ String
")"
specType SuspendedSpec {} = String
"SuspendedSpec"
specType ErrorSpec {} = String
"ErrorSpec"
specType MemberSpec {} = String
"MemberSpec"
specType TypeSpec {} = String
"TypeSpec"
specType TrueSpec {} = String
"TrueSpec"

-- ============================================================
-- An abstraction that hides everything about a function symbol
-- But includes inside in the constraints, everything needed to
-- use the function symbol

showCtxWith ::
  forall fn as b.
  AppRequires fn as b =>
  fn as b ->
  TestableCtx as ->
  String
showCtxWith :: forall (fn :: [*] -> * -> *) (as :: [*]) b.
AppRequires fn as b =>
fn as b -> TestableCtx as -> String
showCtxWith fn as b
fn (TestableCtx ListCtx Value as (HOLE a)
ctx) = forall a. Show a => a -> String
show Term b
tm
  where
    tm :: Term b
    tm :: Term b
tm =
      forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
FunTy (MapList f ts) r -> List f ts -> r
uncurryList (forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm 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 (forall a. HasSpec a => a -> Term a
lit @_ 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 a. HasSpec a => Var a -> Term a
V forall a b. (a -> b) -> a -> b
$ forall a. Int -> String -> Var a
Var Int
0 String
"v")

data TestableFn where
  TestableFn ::
    ( QC.Arbitrary (Specification b)
    , Typeable (FunTy as b)
    , AppRequires t as b
    ) =>
    t as b ->
    TestableFn

instance Show TestableFn where
  show :: TestableFn -> String
show (TestableFn (t as b
fn :: t as b)) =
    forall a. Show a => a -> String
show t 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))

-- ===========================================================
-- Random contexts
-- ===========================================================

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

instance forall as. (All HasSpec as, TypeList as) => QC.Arbitrary (TestableCtx as) where
  arbitrary :: Gen (TestableCtx 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 as' =>
Int -> List f as' -> Gen (TestableCtx as')
go Int
idx List (Const ()) as
shape
    where
      go :: forall f as'. All HasSpec as' => Int -> List f as' -> QC.Gen (TestableCtx as')
      go :: forall (f :: * -> *) (as' :: [*]).
All HasSpec as' =>
Int -> List f as' -> Gen (TestableCtx as')
go Int
0 (f a
_ :> List f as1
as) =
        forall b (as :: [*]).
HasSpec b =>
ListCtx Value as (HOLE b) -> TestableCtx as
TestableCtx forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall {k} (a :: k). 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 (\f a
_ -> forall a. Show a => a -> Value a
Value forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec forall a. Specification 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 as' =>
Int -> List f as' -> Gen (TestableCtx as')
go (Int
n forall a. Num a => a -> a -> a
- Int
1) List f as1
as
        forall b (as :: [*]).
HasSpec b =>
ListCtx Value as (HOLE b) -> TestableCtx 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 a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec forall a. Specification a
TrueSpec
      go Int
_ List f as'
_ = forall a. HasCallStack => String -> a
error String
"The impossible happened in Arbitrary for TestableCtx"

  shrink :: TestableCtx as -> [TestableCtx as]
shrink (TestableCtx ListCtx Value as (HOLE a)
ctx) = forall b (as :: [*]).
HasSpec b =>
ListCtx Value as (HOLE b) -> TestableCtx as
TestableCtx forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: * -> *) (as' :: [*]).
All HasSpec as' =>
ListCtx Value as' c -> [ListCtx Value as' c]
shrinkCtx ListCtx Value as (HOLE a)
ctx
    where
      shrinkCtx :: forall c as'. All HasSpec as' => ListCtx Value as' c -> [ListCtx Value as' c]
      shrinkCtx :: forall (c :: * -> *) (as' :: [*]).
All HasSpec 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 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 a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec forall a. Specification 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 as' =>
ListCtx Value as' c -> [ListCtx Value as' c]
shrinkCtx ListCtx Value as1 c
ctx')

      go :: forall as'. All HasSpec as' => List Value as' -> [List Value as']
      go :: forall (as' :: [*]).
All HasSpec 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 a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec forall a. Specification 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 as' =>
List Value as' -> [List Value as']
go List Value as1
as)

genTestableFn :: QC.Gen TestableFn
genTestableFn :: Gen TestableFn
genTestableFn = forall a. Arbitrary a => Gen a
QC.arbitrary

instance QC.Arbitrary TestableFn where
  arbitrary :: Gen TestableFn
arbitrary =
    forall a. HasCallStack => [a] -> Gen a
QC.elements
      [ -- data IntW
        forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall b. NumLike b => IntW '[b, b] b
AddW @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall b. NumLike b => IntW '[b] b
NegateW @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall n. (Sized n, HasSpec n) => SizeW '[n] Integer
SizeOfW @(Map Int Int)
      , -- data BaseW
        forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a1. (Eq a1, HasSpec a1) => EqW '[a1, a1] Bool
EqualW @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall b b1. (HasSpec b, HasSpec b1) => ProdW '[Prod b b1] b
ProdFstW @Int @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a1 b. (HasSpec a1, HasSpec b) => ProdW '[Prod a1 b] b
ProdSndW @Int @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a1 b1.
(HasSpec a1, HasSpec b1) =>
ProdW '[a1, b1] (Prod a1 b1)
ProdW @Int @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a b. (HasSpec a, HasSpec b) => SumW '[b] (Sum a b)
InjRightW @Int @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a b. (HasSpec a, HasSpec b) => SumW '[a] (Sum a b)
InjLeftW @Int @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a1. HasSpec a1 => ElemW '[a1, [a1]] Bool
ElemW @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall rng. GenericRequires rng => BaseW '[SimpleRep rng] rng
FromGenericW @Bool -- These require GenericC constraints
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a. GenericRequires a => BaseW '[a] (SimpleRep a)
ToGenericW @(Either Int Bool)
      , -- data SetW
        forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Ord a) => SetW '[a] (Set a)
SingletonW @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Ord a) => SetW '[Set a, Set a] (Set a)
UnionW @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a.
(HasSpec a, Ord a, HasSpec a) =>
SetW '[Set a, Set a] Bool
SubsetW @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Ord a) => SetW '[a, Set a] Bool
MemberW @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Ord a) => SetW '[Set a, Set a] Bool
DisjointW @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Ord a) => SetW '[[a]] (Set a)
FromListW @Int
      , -- data BoolW
        forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ BoolW '[Bool] Bool
NotW
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ BoolW '[Bool, Bool] Bool
OrW
      , -- data NumOrdW
        forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a. OrdLike a => NumOrdW '[a, a] Bool
LessW @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a. OrdLike a => NumOrdW '[a, a] Bool
LessOrEqualW @Int
      , -- data MapW
        forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall k v.
(HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) =>
MapW '[Map k v] [v]
RngW @Int @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall k v.
(HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) =>
MapW '[Map k v] (Set k)
DomW @Int @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall k v.
(HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) =>
MapW '[k, Map k v] (Maybe v)
LookupW @Int @Int
      , -- data ListW
        forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a res.
(Foldy res, HasSpec a) =>
Fun '[a] res -> ListW '[[a]] res
FoldMapW @Int (forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun forall rng. FunW '[rng] rng
IdW)
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => ListW '[a] [a]
SingletonListW @Int
      , forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Typeable a, Show a) => ListW '[[a], [a]] [a]
AppendW @Int
      ]
  shrink :: TestableFn -> [TestableFn]
shrink TestableFn
_ = []

-- ==========================================================
-- More Properties
-- ==========================================================

prop_mapSpec ::
  ( HasSpec a
  , AppRequires t '[a] b
  ) =>
  t '[a] b ->
  Specification a ->
  QC.Property
prop_mapSpec :: forall a (t :: [*] -> * -> *) b.
(HasSpec a, AppRequires t '[a] b) =>
t '[a] b -> Specification a -> Property
prop_mapSpec t '[a] b
funsym Specification 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 a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification 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 a. HasSpec a => a -> Specification a -> Bool
conformsToSpec (forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t '[a] b
funsym a
a) (forall (t :: [*] -> * -> *) a b.
AppRequires t '[a] b =>
t '[a] b -> Specification a -> Specification b
mapSpec t '[a] b
funsym Specification a
spec)

prop_propagateSpecSound ::
  ( HasSpec a
  , AppRequires t '[a] b
  ) =>
  t '[a] b ->
  b ->
  QC.Property
prop_propagateSpecSound :: forall a (t :: [*] -> * -> *) b.
(HasSpec a, AppRequires t '[a] b) =>
t '[a] b -> b -> Property
prop_propagateSpecSound t '[a] b
funsym 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 :: * -> *) a b.
(MonadGenError m, HasSpec a, HasSpec b) =>
Fun '[a] b -> Specification a -> b -> GenT m a
genInverse (forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun t '[a] b
funsym) forall a. Specification 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 (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t '[a] b
funsym a
a forall a. Eq a => a -> a -> Bool
== b
b