{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | Useful properties for debugging HasSpec instances and this library itself
module Constrained.Test where

import Constrained.API
import Constrained.Base (
  AppRequires,
  BaseW (..),
  HOLE (..),
  appTerm,
  memberSpecList,
  typeSpec,
 )
import Constrained.Conformance (
  monitorSpec,
 )
import Constrained.Core (
  Value (..),
  Var (..),
  unValue,
 )
import Constrained.FunctionSymbol (getWitness)
import Constrained.GenT (
  GE (..),
  fromGEDiscard,
  fromGEProp,
  strictGen,
 )
import Constrained.Generation
import Constrained.List (
  All,
  FunTy,
  List (..),
  ListCtx (..),
  TypeList,
  fillListCtx,
  lengthList,
  listShape,
  mapListCtxC,
  mapMListC,
  uncurryList,
  uncurryList_,
 )
import Constrained.NumOrd (
  IntW (..),
  OrdW (..),
 )
import Constrained.PrettyUtils
import Constrained.Properties
import Constrained.Spec.Map (
  MapW (..),
 )
import Constrained.Spec.SumProd ()
import Constrained.TheKnot
import Data.List (nub)
import qualified Data.List.NonEmpty as NE
import Data.Map (Map)
import Data.Set (Set)
import Data.Typeable (Typeable, typeOf)
import Prettyprinter
import Test.QuickCheck hiding (Fun)
import qualified Test.QuickCheck as QC

prop_sound ::
  HasSpec a =>
  Specification a ->
  QC.Property
prop_sound :: forall a. HasSpec a => Specification a -> Property
prop_sound Specification a
spec =
  Gen (GE a) -> (GE a -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
QC.forAllBlind (GenT GE a -> Gen (GE a)
forall (m :: * -> *) a. GenT m a -> Gen (m a)
strictGen (GenT GE a -> Gen (GE a)) -> GenT GE a -> Gen (GE a)
forall a b. (a -> b) -> a -> b
$ Specification a -> GenT GE a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
spec) ((GE a -> Property) -> Property) -> (GE a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \GE a
ma ->
    case GE a
ma of
      Result a
a ->
        Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
QC.cover Double
80 Bool
True String
"successful" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
QC.counterexample (a -> String
forall a. Show a => a -> String
show a
a) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
            Specification a -> a -> Property -> Property
forall p a. Testable p => Specification a -> a -> p -> Property
monitorSpec Specification a
spec a
a (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
              a -> Specification a -> Property
forall a. HasSpec a => a -> Specification a -> Property
conformsToSpecProp a
a Specification a
spec
      GE a
_ -> Double -> Bool -> String -> Bool -> Property
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 = Specification a -> Property
forall a. HasSpec a => Specification a -> Property
prop_sound ((Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
a -> Term a -> Specification a -> Pred
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 =
  Gen (NonEmpty String) -> (NonEmpty String -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
QC.forAll Gen (NonEmpty String)
forall a. Arbitrary a => Gen a
QC.arbitrary ((NonEmpty String -> Property) -> Property)
-> (NonEmpty String -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \NonEmpty String
es ->
    Specification a -> Property
forall a. HasSpec a => Specification a -> Property
prop_sound (Specification a -> Property) -> Specification a -> Property
forall a b. (a -> b) -> a -> b
$ (Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
x -> NonEmpty String -> Pred -> Pred
forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain NonEmpty String
es (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Term a
x Term a -> Specification a -> Pred
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 =
  Gen (GE a) -> (GE a -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
QC.forAllBlind (GenT GE a -> Gen (GE a)
forall (m :: * -> *) a. GenT m a -> Gen (m a)
strictGen (GenT GE a -> Gen (GE a)) -> GenT GE a -> Gen (GE a)
forall a b. (a -> b) -> a -> b
$ Specification a -> GenT GE a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
s) ((GE a -> Property) -> Property) -> (GE a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \GE a
ma -> GE Bool -> Property
forall p. Testable p => GE p -> Property
fromGEProp (GE Bool -> Property) -> GE Bool -> Property
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
    Bool -> GE Bool
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> GE Bool) -> Bool -> GE Bool
forall a b. (a -> b) -> a -> b
$ String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (a -> String
forall a. Show a => a -> String
show a
a) Int -> Int -> Bool
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 = Specification a -> Property
forall a. HasSpec a => Specification a -> Property
prop_complete ((Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
a -> Term a -> Specification a -> Pred
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 =
  Gen (GE a) -> (GE a -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
QC.forAll (GenT GE a -> Gen (GE a)
forall (m :: * -> *) a. GenT m a -> Gen (m a)
strictGen (GenT GE a -> Gen (GE a)) -> GenT GE a -> Gen (GE a)
forall a b. (a -> b) -> a -> b
$ Specification a -> GenT GE a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
s) ((GE a -> Property) -> Property) -> (GE a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \GE a
ma -> GE Property -> Property
forall p. Testable p => GE p -> Property
fromGEDiscard (GE Property -> Property) -> GE Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    a
a <- GE a
ma
    let shrinks :: [a]
shrinks = Specification a -> a -> [a]
forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification a
s a
a
    Property -> GE Property
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> GE Property) -> Property -> GE Property
forall a b. (a -> b) -> a -> b
$
      Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
QC.cover Double
40 (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
shrinks) String
"non-null shrinks" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        if [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
shrinks
          then Bool -> Property
forall prop. Testable prop => prop -> Property
QC.property Bool
True
          else Gen a -> (a -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
QC.forAll ([a] -> Gen a
forall a. HasCallStack => [a] -> Gen a
QC.elements [a]
shrinks) ((a -> Property) -> Property) -> (a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \a
a' ->
            a -> Specification a -> Property
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 = Bool -> Property
forall prop. Testable prop => prop -> Property
QC.property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ a -> TypeSpec a -> Bool
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 :: t as b)) =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
QC.label (t as b -> String
forall a. Show a => a -> String
show t as b
fn) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
QC.forAllShrinkBlind @QC.Property (forall a. Arbitrary a => Gen a
QC.arbitrary @(TestableCtx as)) TestableCtx as -> [TestableCtx as]
forall a. Arbitrary a => a -> [a]
QC.shrink ((TestableCtx as -> Property) -> Property)
-> (TestableCtx as -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \tc :: TestableCtx as
tc@(TestableCtx ListCtx Value as (HOLE a)
ctx) ->
      Gen (Specification b)
-> (Specification b -> [Specification b])
-> (Specification b -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
QC.forAllShrinkBlind Gen (Specification b)
forall a. Arbitrary a => Gen a
QC.arbitrary Specification b -> [Specification b]
forall a. Arbitrary a => a -> [a]
QC.shrink ((Specification b -> Property) -> Property)
-> (Specification b -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Specification b
spec ->
        String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"\nfn ctx = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ t as b -> TestableCtx as -> String
forall (fn :: [*] -> * -> *) (as :: [*]) b.
AppRequires fn as b =>
fn as b -> TestableCtx as -> String
showCtxWith t as b
fn TestableCtx as
tc) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
QC.counterexample (Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"\nspec =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Specification b -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification b -> Doc ann
pretty Specification b
spec) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
            let sspec :: Specification a
sspec = Specification a -> Specification a
forall a. HasSpec a => Specification a -> Specification a
simplifySpec (t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
forall (as :: [*]) b a.
(AppRequires t as b, HasSpec a) =>
t as b
-> ListCtx Value as (HOLE a) -> Specification b -> Specification a
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 String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any
"propagate ctx spec =" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
/> Specification a -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification a -> Doc ann
pretty Specification a
sspec)) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
                  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (Specification a -> Doc Any
forall a ann. HasSpec a => Specification a -> Doc ann
prettyPlan Specification a
sspec)) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
                    Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
QC.within Int
20_000_000 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
                      Gen (GE a) -> (GE a -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
QC.forAllBlind (GenT GE a -> Gen (GE a)
forall (m :: * -> *) a. GenT m a -> Gen (m a)
strictGen (GenT GE a -> Gen (GE a)) -> GenT GE a -> Gen (GE a)
forall a b. (a -> b) -> a -> b
$ Specification a -> GenT GE a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
sspec) ((GE a -> Property) -> Property) -> (GE a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \GE a
ge ->
                        GE Property -> Property
forall p. Testable p => GE p -> Property
fromGEDiscard (GE Property -> Property) -> GE Property -> Property
forall a b. (a -> b) -> a -> b
$ do
                          a
a <- GE a
ge
                          let res :: b
res = (forall a. Value a -> a) -> FunTy as b -> List Value as -> b
forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
forall (f :: * -> *) r.
(forall a. f a -> a) -> FunTy as r -> List f as -> r
uncurryList_ Value a -> a
forall a. Value a -> a
unValue (t as b -> FunTy as b
forall (d :: [*]) r. t d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t as b
fn) (List Value as -> b) -> List Value as -> b
forall a b. (a -> b) -> a -> b
$ ListCtx Value as (HOLE a)
-> (forall {a}. HOLE a a -> Value a) -> List Value as
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}. HOLE a a -> Value a) -> List Value as)
-> (forall {a}. HOLE a a -> Value a) -> List Value as
forall a b. (a -> b) -> a -> b
$ \HOLE a a
HOLE -> a -> Value a
forall a. Show a => a -> Value a
Value a
a
a
                          Property -> GE Property
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> GE Property) -> Property -> GE Property
forall a b. (a -> b) -> a -> b
$
                            String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"\ngenerated value: a = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
                              String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"\nfn ctx[a] = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Show a => a -> String
show b
res) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
                                b -> Specification b -> Property
forall a. HasSpec a => a -> Specification a -> Property
conformsToSpecProp b
res Specification b
spec

main :: IO ()
main :: IO ()
main = Property -> IO ()
forall prop. Testable prop => prop -> IO ()
QC.quickCheck (Int -> (TestableFn -> Property) -> Property
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 = Specification a -> Specification a
forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification a
spec
   in String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
QC.tabulate String
"specType spec" [Specification a -> String
forall a. Specification a -> String
specType Specification a
spec] (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
QC.tabulate String
"specType (simplifySpec spec)" [Specification a -> String
forall a. Specification a -> String
specType Specification a
sspec] (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (Specification a -> Doc Any
forall a ann. HasSpec a => Specification a -> Doc ann
prettyPlan Specification a
sspec)) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
            Gen (GE a) -> (GE a -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
QC.forAllBlind (GenT GE a -> Gen (GE a)
forall (m :: * -> *) a. GenT m a -> Gen (m a)
strictGen (GenT GE a -> Gen (GE a)) -> GenT GE a -> Gen (GE a)
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) ((GE a -> Property) -> Property) -> (GE a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \GE a
ge ->
              GE Property -> Property
forall p. Testable p => GE p -> Property
fromGEDiscard (GE Property -> Property) -> GE Property -> Property
forall a b. (a -> b) -> a -> b
$ do
                a
a <- GE a
ge
                Property -> GE Property
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> GE Property) -> Property -> GE Property
forall a b. (a -> b) -> a -> b
$
                  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
QC.counterexample (String
"\ngenerated value: a = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
a) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
                    a -> Specification a -> Property
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 [] SpecificationD Deps a
s) = SpecificationD Deps a -> String
forall a. Specification a -> String
specType SpecificationD Deps a
s
specType (ExplainSpec [String]
_ SpecificationD Deps a
s) = String
"(ExplainSpec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecificationD Deps a -> String
forall a. Specification a -> String
specType SpecificationD Deps a
s String -> String -> String
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) = Term b -> String
forall a. Show a => a -> String
show Term b
tm
  where
    tm :: Term b
    tm :: Term b
tm =
      FunTy (MapList Term as) (Term b) -> List Term as -> Term b
forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
FunTy (MapList f ts) r -> List f ts -> r
forall (f :: * -> *) r. FunTy (MapList f as) r -> List f as -> r
uncurryList (fn as b -> FunTy (MapList Term as) (Term b)
forall (t :: [*] -> * -> *) (ds :: [*]) r.
AppRequires t ds r =>
t ds r -> FunTy (MapList Term ds) (Term r)
appTerm fn as b
fn) (List Term as -> Term b) -> List Term as -> Term b
forall a b. (a -> b) -> a -> b
$
        ListCtx Term as (HOLE a)
-> (forall a. HOLE a a -> Term a) -> List Term as
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 @_ @Value @Term (forall a. HasSpec a => a -> Term a
lit @_ (a -> Term a) -> (Value a -> a) -> Value a -> Term a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value a -> a
forall a. Value a -> a
unValue) ListCtx Value as (HOLE a)
ctx) (\HOLE a a
HOLE -> Var a -> Term a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V (Var a -> Term a) -> Var a -> Term a
forall a b. (a -> b) -> a -> b
$ Int -> String -> Var a
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)) =
    t as b -> String
forall a. Show a => a -> String
show t as b
fn String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (FunTy as b -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (FunTy as b
forall a. HasCallStack => a
undefined :: FunTy as b))

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 =
  Gen (GE a) -> (GE a -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
QC.forAll (GenT GE a -> Gen (GE a)
forall (m :: * -> *) a. GenT m a -> Gen (m a)
strictGen (GenT GE a -> Gen (GE a)) -> GenT GE a -> Gen (GE a)
forall a b. (a -> b) -> a -> b
$ Specification a -> GenT GE a
forall a (m :: * -> *).
(HasCallStack, HasSpec a, MonadGenError m) =>
Specification a -> GenT m a
genFromSpecT Specification a
spec) ((GE a -> Property) -> Property) -> (GE a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \GE a
ma -> GE Bool -> Property
forall p. Testable p => GE p -> Property
fromGEDiscard (GE Bool -> Property) -> GE Bool -> Property
forall a b. (a -> b) -> a -> b
$ do
    a
a <- GE a
ma
    Bool -> GE Bool
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> GE Bool) -> Bool -> GE Bool
forall a b. (a -> b) -> a -> b
$ b -> Specification b -> Bool
forall a. HasSpec a => a -> Specification a -> Bool
conformsToSpec (t '[a] b -> FunTy '[a] b
forall (d :: [*]) r. t d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t '[a] b
funsym a
a) (t '[a] b -> Specification a -> Specification b
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 =
  Gen (GE a) -> (GE a -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
QC.forAll (GenT GE a -> Gen (GE a)
forall (m :: * -> *) a. GenT m a -> Gen (m a)
strictGen (GenT GE a -> Gen (GE a)) -> GenT GE a -> Gen (GE a)
forall a b. (a -> b) -> a -> b
$ Fun '[a] b -> Specification a -> b -> GenT GE a
forall (m :: * -> *) a b.
(MonadGenError m, HasSpec a, HasSpec b) =>
Fun '[a] b -> Specification a -> b -> GenT m a
genInverse (t '[a] b -> Fun '[a] b
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun t '[a] b
funsym) Specification a
forall deps a. SpecificationD deps a
TrueSpec b
b) ((GE a -> Property) -> Property) -> (GE a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \GE a
ma -> GE Bool -> Property
forall p. Testable p => GE p -> Property
fromGEDiscard (GE Bool -> Property) -> GE Bool -> Property
forall a b. (a -> b) -> a -> b
$ do
    a
a <- GE a
ma
    Bool -> GE Bool
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> GE Bool) -> Bool -> GE Bool
forall a b. (a -> b) -> a -> b
$ t '[a] b -> FunTy '[a] b
forall (d :: [*]) r. t d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t '[a] b
funsym a
a b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
b

------------------------------------------------------------------------
-- Arbitrary instances for Specifications
------------------------------------------------------------------------

instance (Arbitrary (Specification a), Arbitrary (Specification b)) => Arbitrary (SumSpec a b) where
  arbitrary :: Gen (SumSpec a b)
arbitrary =
    Maybe (Int, Int)
-> Specification a -> Specification b -> SumSpec a b
forall a b.
Maybe (Int, Int)
-> Specification a -> Specification b -> SumSpec a b
SumSpec
      (Maybe (Int, Int)
 -> Specification a -> Specification b -> SumSpec a b)
-> Gen (Maybe (Int, Int))
-> Gen (Specification a -> Specification b -> SumSpec a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, Gen (Maybe (Int, Int)))] -> Gen (Maybe (Int, Int))
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
        [ (Int
3, Maybe (Int, Int) -> Gen (Maybe (Int, Int))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Int, Int)
forall a. Maybe a
Nothing)
        , (Int
10, (Int, Int) -> Maybe (Int, Int)
forall a. a -> Maybe a
Just ((Int, Int) -> Maybe (Int, Int))
-> Gen (Int, Int) -> Gen (Maybe (Int, Int))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((,) (Int -> Int -> (Int, Int)) -> Gen Int -> Gen (Int -> (Int, Int))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
100) Gen (Int -> (Int, Int)) -> Gen Int -> Gen (Int, Int)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
100)))
        , (Int
1, Gen (Maybe (Int, Int))
forall a. Arbitrary a => Gen a
arbitrary)
        ]
      Gen (Specification a -> Specification b -> SumSpec a b)
-> Gen (Specification a) -> Gen (Specification b -> SumSpec a b)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Specification a)
forall a. Arbitrary a => Gen a
arbitrary
      Gen (Specification b -> SumSpec a b)
-> Gen (Specification b) -> Gen (SumSpec a b)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Specification b)
forall a. Arbitrary a => Gen a
arbitrary
  shrink :: SumSpec a b -> [SumSpec a b]
shrink (SumSpec Maybe (Int, Int)
h Specification a
a Specification b
b) = [Maybe (Int, Int)
-> Specification a -> Specification b -> SumSpec a b
forall a b.
Maybe (Int, Int)
-> Specification a -> Specification b -> SumSpec a b
SumSpec Maybe (Int, Int)
h' Specification a
a' Specification b
b' | (Maybe (Int, Int)
h', Specification a
a', Specification b
b') <- (Maybe (Int, Int), Specification a, Specification b)
-> [(Maybe (Int, Int), Specification a, Specification b)]
forall a. Arbitrary a => a -> [a]
shrink (Maybe (Int, Int)
h, Specification a
a, Specification b
b)]

instance (Arbitrary (Specification a), Arbitrary (Specification b)) => Arbitrary (PairSpec a b) where
  arbitrary :: Gen (PairSpec a b)
arbitrary = Specification a -> Specification b -> PairSpec a b
forall a b. Specification a -> Specification b -> PairSpec a b
Cartesian (Specification a -> Specification b -> PairSpec a b)
-> Gen (Specification a) -> Gen (Specification b -> PairSpec a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Specification a)
forall a. Arbitrary a => Gen a
arbitrary Gen (Specification b -> PairSpec a b)
-> Gen (Specification b) -> Gen (PairSpec a b)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Specification b)
forall a. Arbitrary a => Gen a
arbitrary
  shrink :: PairSpec a b -> [PairSpec a b]
shrink (Cartesian Specification a
a Specification b
b) = (Specification a -> Specification b -> PairSpec a b)
-> (Specification a, Specification b) -> PairSpec a b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Specification a -> Specification b -> PairSpec a b
forall a b. Specification a -> Specification b -> PairSpec a b
Cartesian ((Specification a, Specification b) -> PairSpec a b)
-> [(Specification a, Specification b)] -> [PairSpec a b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Specification a, Specification b)
-> [(Specification a, Specification b)]
forall a. Arbitrary a => a -> [a]
shrink (Specification a
a, Specification b
b)

-- TODO: consider making this more interesting to get fewer discarded tests
-- in `prop_gen_sound`
instance
  ( Arbitrary k
  , Arbitrary v
  , Arbitrary (TypeSpec k)
  , Arbitrary (TypeSpec v)
  , Ord k
  , HasSpec k
  , Foldy v
  ) =>
  Arbitrary (MapSpec k v)
  where
  arbitrary :: Gen (MapSpec k v)
arbitrary =
    Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
forall k v.
Maybe Integer
-> Set k
-> [v]
-> Specification Integer
-> Specification (k, v)
-> FoldSpec v
-> MapSpec k v
MapSpec
      (Maybe Integer
 -> Set k
 -> [v]
 -> Specification Integer
 -> Specification (k, v)
 -> FoldSpec v
 -> MapSpec k v)
-> Gen (Maybe Integer)
-> Gen
     (Set k
      -> [v]
      -> Specification Integer
      -> Specification (k, v)
      -> FoldSpec v
      -> MapSpec k v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Maybe Integer)
forall a. Arbitrary a => Gen a
arbitrary
      Gen
  (Set k
   -> [v]
   -> Specification Integer
   -> Specification (k, v)
   -> FoldSpec v
   -> MapSpec k v)
-> Gen (Set k)
-> Gen
     ([v]
      -> Specification Integer
      -> Specification (k, v)
      -> FoldSpec v
      -> MapSpec k v)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Set k)
forall a. Arbitrary a => Gen a
arbitrary
      Gen
  ([v]
   -> Specification Integer
   -> Specification (k, v)
   -> FoldSpec v
   -> MapSpec k v)
-> Gen [v]
-> Gen
     (Specification Integer
      -> Specification (k, v) -> FoldSpec v -> MapSpec k v)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen [v]
forall a. Arbitrary a => Gen a
arbitrary
      Gen
  (Specification Integer
   -> Specification (k, v) -> FoldSpec v -> MapSpec k v)
-> Gen (Specification Integer)
-> Gen (Specification (k, v) -> FoldSpec v -> MapSpec k v)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Specification Integer)
forall a. Arbitrary a => Gen a
arbitrary
      Gen (Specification (k, v) -> FoldSpec v -> MapSpec k v)
-> Gen (Specification (k, v)) -> Gen (FoldSpec v -> MapSpec k v)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Specification (k, v))
forall a. Arbitrary a => Gen a
arbitrary
      Gen (FoldSpec v -> MapSpec k v)
-> Gen (FoldSpec v) -> Gen (MapSpec k v)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [(Int, Gen (FoldSpec v))] -> Gen (FoldSpec v)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
1, FoldSpec v -> Gen (FoldSpec v)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FoldSpec v
forall a. FoldSpec a
NoFold), (Int
1, Gen (FoldSpec v)
forall a. Arbitrary a => Gen a
arbitrary)]
  shrink :: MapSpec k v -> [MapSpec k v]
shrink = MapSpec k v -> [MapSpec k v]
forall a.
(Generic a, RecursivelyShrink (Rep a), GSubterms (Rep a) a) =>
a -> [a]
genericShrink

instance Arbitrary (FoldSpec (Map k v)) where
  arbitrary :: Gen (FoldSpec (Map k v))
arbitrary = FoldSpec (Map k v) -> Gen (FoldSpec (Map k v))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FoldSpec (Map k v)
forall a. FoldSpec a
NoFold

instance (HasSpec a, Arbitrary (TypeSpec a)) => Arbitrary (Specification a) where
  arbitrary :: Gen (Specification a)
arbitrary = do
    Specification a
baseSpec <-
      [(Int, Gen (Specification a))] -> Gen (Specification a)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
        [ (Int
1, Specification a -> Gen (Specification a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Specification a
forall deps a. SpecificationD deps a
TrueSpec)
        ,
          ( Int
7
          , do
              [a]
zs <- [a] -> [a]
forall a. Eq a => [a] -> [a]
nub ([a] -> [a]) -> Gen [a] -> Gen [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a -> Gen [a]
forall a. Gen a -> Gen [a]
listOf1 (Specification a -> Gen a
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification a
forall deps a. SpecificationD deps a
TrueSpec)
              Specification a -> Gen (Specification a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( [a] -> NonEmpty String -> Specification a
forall a. [a] -> NonEmpty String -> Specification a
memberSpecList
                    [a]
zs
                    ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
                        [ String
"In (Arbitrary Specification) this should never happen"
                        , String
"listOf1 generates empty list."
                        ]
                    )
                )
          )
        , (Int
10, TypeSpec a -> Specification a
forall a. HasSpec a => TypeSpec a -> Specification a
typeSpec (TypeSpec a -> Specification a)
-> Gen (TypeSpec a) -> Gen (Specification a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (TypeSpec a)
forall a. Arbitrary a => Gen a
arbitrary)
        ,
          ( Int
1
          , do
              Int
len <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
5)
              TypeSpec a -> [a] -> Specification a
forall a. HasSpec a => TypeSpec a -> [a] -> Specification a
TypeSpec (TypeSpec a -> [a] -> Specification a)
-> Gen (TypeSpec a) -> Gen ([a] -> Specification a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (TypeSpec a)
forall a. Arbitrary a => Gen a
arbitrary Gen ([a] -> Specification a) -> Gen [a] -> Gen (Specification a)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> Gen a -> Gen [a]
forall a. Int -> Gen a -> Gen [a]
vectorOf Int
len (Specification a -> Gen a
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification a
forall deps a. SpecificationD deps a
TrueSpec)
          )
        , (Int
1, NonEmpty String -> Specification a
forall deps a. NonEmpty String -> SpecificationD deps a
ErrorSpec (NonEmpty String -> Specification a)
-> Gen (NonEmpty String) -> Gen (Specification a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (NonEmpty String)
forall a. Arbitrary a => Gen a
arbitrary)
        , -- Recurse to make sure we apply the tricks for generating suspended specs multiple times
          (Int
1, Gen (Specification a)
forall a. Arbitrary a => Gen a
arbitrary)
        ]
    -- TODO: we probably want smarter ways of generating constraints
    [(Int, Gen (Specification a))] -> Gen (Specification a)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
      [ (Int
1, Specification a -> Gen (Specification a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Specification a -> Gen (Specification a))
-> Specification a -> Gen (Specification a)
forall a b. (a -> b) -> a -> b
$ (Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
x -> Term a
x Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
baseSpec)
      , (Int
1, [String] -> Specification a -> Specification a
forall deps a.
[String] -> SpecificationD deps a -> SpecificationD deps a
ExplainSpec [String
"Arbitrary"] (Specification a -> Specification a)
-> Gen (Specification a) -> Gen (Specification a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Specification a)
forall a. Arbitrary a => Gen a
arbitrary)
      ,
        ( Int
1
        , Specification a -> Gen (Specification a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Specification a -> Gen (Specification a))
-> Specification a -> Gen (Specification a)
forall a b. (a -> b) -> a -> b
$ (Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
x -> ((forall b. Term b -> b) -> GE a) -> (Term a -> [Pred]) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
eval -> a -> GE a
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> GE a) -> a -> GE a
forall a b. (a -> b) -> a -> b
$ Term a -> a
forall b. Term b -> b
eval Term a
x) ((Term a -> [Pred]) -> Pred) -> (Term a -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term a
y ->
            [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term a
x Term a -> Term a -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term a
y
            , Term a
y Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
baseSpec
            ]
        )
      , (Int
1, Specification a -> Gen (Specification a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Specification a -> Gen (Specification a))
-> Specification a -> Gen (Specification a)
forall a b. (a -> b) -> a -> b
$ (Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
x -> Term a -> (Term a -> Pred) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind Term a
x ((Term a -> Pred) -> Pred) -> (Term a -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term a
y -> Term a
y Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
baseSpec)
      ,
        ( Int
1
        , Specification a -> Gen (Specification a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Specification a -> Gen (Specification a))
-> Specification a -> Gen (Specification a)
forall a b. (a -> b) -> a -> b
$ (Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
x -> ((forall b. Term b -> b) -> GE Bool) -> (Term Bool -> Pred) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
_ -> Bool -> GE Bool
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) ((Term Bool -> Pred) -> Pred) -> (Term Bool -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Bool
b ->
            Term Bool -> Pred -> Pred -> Pred
forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse Term Bool
b (Term a
x Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
baseSpec) (Term a
x Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
baseSpec)
        )
      ,
        ( Int
1
        , Specification a -> Gen (Specification a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Specification a -> Gen (Specification a))
-> Specification a -> Gen (Specification a)
forall a b. (a -> b) -> a -> b
$ (Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
x -> ((forall b. Term b -> b) -> GE Bool)
-> (Term Bool -> [Pred]) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
_ -> Bool -> GE Bool
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) ((Term Bool -> [Pred]) -> Pred) -> (Term Bool -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Bool
b ->
            [ Term Bool -> Bool -> Pred -> Pred
forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse Term Bool
b Bool
True (Term a
x Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
baseSpec)
            , Term a
x Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
baseSpec
            ]
        )
      ,
        ( Int
1
        , Specification a -> Gen (Specification a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Specification a -> Gen (Specification a))
-> Specification a -> Gen (Specification a)
forall a b. (a -> b) -> a -> b
$ (Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
x -> ((forall b. Term b -> b) -> GE Bool)
-> (Term Bool -> [Pred]) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
_ -> Bool -> GE Bool
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False) ((Term Bool -> [Pred]) -> Pred) -> (Term Bool -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Bool
b ->
            [ Term Bool -> Pred -> Bool -> Pred
forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse Term Bool
b (Term a
x Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
baseSpec) Bool
True
            , Term a
x Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
baseSpec
            ]
        )
      ,
        ( Int
1
        , Specification a -> Gen (Specification a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Specification a -> Gen (Specification a))
-> Specification a -> Gen (Specification a)
forall a b. (a -> b) -> a -> b
$ (Term a -> Pred) -> Specification a
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term a -> Pred) -> Specification a)
-> (Term a -> Pred) -> Specification a
forall a b. (a -> b) -> a -> b
$ \Term a
x -> NonEmpty String -> Pred -> Pred
explanation (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"its very subtle, you won't get it.") (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Term a
x Term a -> Specification a -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification a
baseSpec
        )
      , (Int
10, Specification a -> Gen (Specification a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Specification a
baseSpec)
      ]

instance
  ( Arbitrary a
  , Arbitrary (FoldSpec a)
  , Arbitrary (TypeSpec a)
  , HasSpec a
  ) =>
  Arbitrary (ListSpec a)
  where
  arbitrary :: Gen (ListSpec a)
arbitrary = Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec (Maybe Integer
 -> [a]
 -> Specification Integer
 -> Specification a
 -> FoldSpec a
 -> ListSpec a)
-> Gen (Maybe Integer)
-> Gen
     ([a]
      -> Specification Integer
      -> Specification a
      -> FoldSpec a
      -> ListSpec a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Maybe Integer)
forall a. Arbitrary a => Gen a
arbitrary Gen
  ([a]
   -> Specification Integer
   -> Specification a
   -> FoldSpec a
   -> ListSpec a)
-> Gen [a]
-> Gen
     (Specification Integer
      -> Specification a -> FoldSpec a -> ListSpec a)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen [a]
forall a. Arbitrary a => Gen a
arbitrary Gen
  (Specification Integer
   -> Specification a -> FoldSpec a -> ListSpec a)
-> Gen (Specification Integer)
-> Gen (Specification a -> FoldSpec a -> ListSpec a)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Specification Integer)
forall a. Arbitrary a => Gen a
arbitrary Gen (Specification a -> FoldSpec a -> ListSpec a)
-> Gen (Specification a) -> Gen (FoldSpec a -> ListSpec a)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Specification a)
forall a. Arbitrary a => Gen a
arbitrary Gen (FoldSpec a -> ListSpec a)
-> Gen (FoldSpec a) -> Gen (ListSpec a)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (FoldSpec a)
forall a. Arbitrary a => Gen a
arbitrary
  shrink :: ListSpec a -> [ListSpec a]
shrink (ListSpec Maybe Integer
a [a]
b Specification Integer
c Specification a
d FoldSpec a
e) = [Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
forall a.
Maybe Integer
-> [a]
-> Specification Integer
-> Specification a
-> FoldSpec a
-> ListSpec a
ListSpec Maybe Integer
a' [a]
b' Specification Integer
c' Specification a
d' FoldSpec a
e' | (Maybe Integer
a', [a]
b', Specification Integer
c', Specification a
d', FoldSpec a
e') <- (Maybe Integer, [a], Specification Integer, Specification a,
 FoldSpec a)
-> [(Maybe Integer, [a], Specification Integer, Specification a,
     FoldSpec a)]
forall a. Arbitrary a => a -> [a]
shrink (Maybe Integer
a, [a]
b, Specification Integer
c, Specification a
d, FoldSpec a
e)]

instance {-# OVERLAPPABLE #-} (Arbitrary (Specification a), Foldy a) => Arbitrary (FoldSpec a) where
  arbitrary :: Gen (FoldSpec a)
arbitrary = [Gen (FoldSpec a)] -> Gen (FoldSpec a)
forall a. HasCallStack => [Gen a] -> Gen a
oneof [Fun '[a] a -> Specification a -> FoldSpec a
forall b a.
(HasSpec a, HasSpec b, Foldy b) =>
Fun '[a] b -> Specification b -> FoldSpec a
FoldSpec (FunW '[a] a -> Fun '[a] a
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun FunW '[a] a
forall rng. FunW '[rng] rng
IdW) (Specification a -> FoldSpec a)
-> Gen (Specification a) -> Gen (FoldSpec a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Specification a)
forall a. Arbitrary a => Gen a
arbitrary, FoldSpec a -> Gen (FoldSpec a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FoldSpec a
forall a. FoldSpec a
NoFold]
  shrink :: FoldSpec a -> [FoldSpec a]
shrink FoldSpec a
NoFold = []
  shrink (FoldSpec (Fun (t '[a] b -> Maybe (FunW '[a] b)
forall {k1} {k2} (t :: k1 -> k2 -> *) (t' :: k1 -> k2 -> *)
       (d :: k1) (r :: k2).
(Typeable t, Typeable d, Typeable r, Typeable t') =>
t d r -> Maybe (t' d r)
getWitness -> Just FunW '[a] b
IdW)) Specification b
spec) = Fun '[a] a -> Specification a -> FoldSpec a
forall b a.
(HasSpec a, HasSpec b, Foldy b) =>
Fun '[a] b -> Specification b -> FoldSpec a
FoldSpec (FunW '[a] a -> Fun '[a] a
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
AppRequires t dom rng =>
t dom rng -> Fun dom rng
Fun FunW '[a] a
forall rng. FunW '[rng] rng
IdW) (Specification a -> FoldSpec a)
-> [Specification a] -> [FoldSpec a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Specification a -> [Specification a]
forall a. Arbitrary a => a -> [a]
shrink Specification a
Specification b
spec
  shrink FoldSpec {} = [FoldSpec a
forall a. FoldSpec a
NoFold]

instance (Ord a, Arbitrary (Specification a), Arbitrary a) => Arbitrary (SetSpec a) where
  arbitrary :: Gen (SetSpec a)
arbitrary = Set a -> Specification a -> Specification Integer -> SetSpec a
forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec (Set a -> Specification a -> Specification Integer -> SetSpec a)
-> Gen (Set a)
-> Gen (Specification a -> Specification Integer -> SetSpec a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Set a)
forall a. Arbitrary a => Gen a
arbitrary Gen (Specification a -> Specification Integer -> SetSpec a)
-> Gen (Specification a)
-> Gen (Specification Integer -> SetSpec a)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Specification a)
forall a. Arbitrary a => Gen a
arbitrary Gen (Specification Integer -> SetSpec a)
-> Gen (Specification Integer) -> Gen (SetSpec a)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Specification Integer)
forall a. Arbitrary a => Gen a
arbitrary
  shrink :: SetSpec a -> [SetSpec a]
shrink (SetSpec Set a
a Specification a
b Specification Integer
c) = [Set a -> Specification a -> Specification Integer -> SetSpec a
forall a.
Set a -> Specification a -> Specification Integer -> SetSpec a
SetSpec Set a
a' Specification a
b' Specification Integer
c' | (Set a
a', Specification a
b', Specification Integer
c') <- (Set a, Specification a, Specification Integer)
-> [(Set a, Specification a, Specification Integer)]
forall a. Arbitrary a => a -> [a]
shrink (Set a
a, Specification a
b, Specification Integer
c)]

-- TODO: consider improving this
instance Arbitrary (FoldSpec (Set a)) where
  arbitrary :: Gen (FoldSpec (Set a))
arbitrary = FoldSpec (Set a) -> Gen (FoldSpec (Set a))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FoldSpec (Set a)
forall a. FoldSpec a
NoFold

------------------------------------------------------------------------
-- 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 <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
QC.choose (Int
0, List (Const ()) as -> Int
forall {k} (f :: k -> *) (as :: [k]). List f as -> Int
lengthList List (Const ()) as
shape Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
    Int -> List (Const ()) as -> Gen (TestableCtx as)
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) =
        ListCtx Value as' (HOLE a) -> TestableCtx as'
forall b (as :: [*]).
HasSpec b =>
ListCtx Value as (HOLE b) -> TestableCtx as
TestableCtx (ListCtx Value as' (HOLE a) -> TestableCtx as')
-> (List Value as1 -> ListCtx Value as' (HOLE a))
-> List Value as1
-> TestableCtx as'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HOLE a a
forall a. HOLE a a
HOLE HOLE a a -> List Value as1 -> ListCtx Value (a : as1) (HOLE a)
forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:?) (List Value as1 -> TestableCtx as')
-> Gen (List Value as1) -> Gen (TestableCtx as')
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)
forall (c :: * -> Constraint) (as :: [*]) (f :: * -> *)
       (g :: * -> *) (m :: * -> *).
(Applicative m, All c as) =>
(forall a. c a => f a -> m (g a)) -> List f as -> m (List g as)
mapMListC @HasSpec (\f a
_ -> a -> Value a
forall a. Show a => a -> Value a
Value (a -> Value a) -> Gen a -> Gen (Value a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Specification a -> Gen a
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification a
forall deps a. SpecificationD deps a
TrueSpec) List f as1
as
      go Int
n (f a
_ :> List f as1
as) = do
        TestableCtx ListCtx Value as1 (HOLE a)
ctx <- Int -> List f as1 -> Gen (TestableCtx as1)
forall (f :: * -> *) (as' :: [*]).
All HasSpec as' =>
Int -> List f as' -> Gen (TestableCtx as')
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) List f as1
as
        ListCtx Value as' (HOLE a) -> TestableCtx as'
forall b (as :: [*]).
HasSpec b =>
ListCtx Value as (HOLE b) -> TestableCtx as
TestableCtx (ListCtx Value as' (HOLE a) -> TestableCtx as')
-> (a -> ListCtx Value as' (HOLE a)) -> a -> TestableCtx as'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value a
-> ListCtx Value as1 (HOLE a) -> ListCtx Value (a : as1) (HOLE a)
forall (f :: * -> *) a (as1 :: [*]) (c :: * -> *).
f a -> ListCtx f as1 c -> ListCtx f (a : as1) c
:! ListCtx Value as1 (HOLE a)
ctx) (Value a -> ListCtx Value as' (HOLE a))
-> (a -> Value a) -> a -> ListCtx Value as' (HOLE a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Value a
forall a. Show a => a -> Value a
Value (a -> TestableCtx as') -> Gen a -> Gen (TestableCtx as')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Specification a -> Gen a
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification a
forall deps a. SpecificationD deps a
TrueSpec
      go Int
_ List f as'
_ = String -> Gen (TestableCtx 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) = ListCtx Value as (HOLE a) -> TestableCtx as
forall b (as :: [*]).
HasSpec b =>
ListCtx Value as (HOLE b) -> TestableCtx as
TestableCtx (ListCtx Value as (HOLE a) -> TestableCtx as)
-> [ListCtx Value as (HOLE a)] -> [TestableCtx as]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ListCtx Value as (HOLE a) -> [ListCtx Value as (HOLE a)]
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 c a -> List Value as1 -> ListCtx Value (a : as1) c
forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:?) (List Value as1 -> ListCtx Value as' c)
-> [List Value as1] -> [ListCtx Value as' c]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List Value as1 -> [List Value as1]
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') = (a -> ListCtx Value as' c) -> [a] -> [ListCtx Value as' c]
forall a b. (a -> b) -> [a] -> [b]
map ((Value a -> ListCtx Value as1 c -> ListCtx Value (a : as1) c
forall (f :: * -> *) a (as1 :: [*]) (c :: * -> *).
f a -> ListCtx f as1 c -> ListCtx f (a : as1) c
:! ListCtx Value as1 c
ctx') (Value a -> ListCtx Value as' c)
-> (a -> Value a) -> a -> ListCtx Value as' c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Value a
forall a. Show a => a -> Value a
Value) (Specification a -> a -> [a]
forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification a
forall deps a. SpecificationD deps a
TrueSpec a
a) [ListCtx Value as' c]
-> [ListCtx Value as' c] -> [ListCtx Value as' c]
forall a. [a] -> [a] -> [a]
++ (ListCtx Value as1 c -> ListCtx Value as' c)
-> [ListCtx Value as1 c] -> [ListCtx Value as' c]
forall a b. (a -> b) -> [a] -> [b]
map (a -> Value a
forall a. Show a => a -> Value a
Value a
a Value a -> ListCtx Value as1 c -> ListCtx Value (a : as1) c
forall (f :: * -> *) a (as1 :: [*]) (c :: * -> *).
f a -> ListCtx f as1 c -> ListCtx f (a : as1) c
:!) (ListCtx Value as1 c -> [ListCtx Value 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) = (a -> List Value as') -> [a] -> [List Value as']
forall a b. (a -> b) -> [a] -> [b]
map ((Value a -> List Value as1 -> List Value (a : as1)
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Value as1
as) (Value a -> List Value as')
-> (a -> Value a) -> a -> List Value as'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Value a
forall a. Show a => a -> Value a
Value) (Specification a -> a -> [a]
forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification a
forall deps a. SpecificationD deps a
TrueSpec a
a) [List Value as'] -> [List Value as'] -> [List Value as']
forall a. [a] -> [a] -> [a]
++ (List Value as1 -> List Value as')
-> [List Value as1] -> [List Value as']
forall a b. (a -> b) -> [a] -> [b]
map (a -> Value a
forall a. Show a => a -> Value a
Value a
a Value a -> List Value as1 -> List Value (a : as1)
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:>) (List Value as1 -> [List Value 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 = Gen TestableFn
forall a. Arbitrary a => Gen a
QC.arbitrary

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