{-# 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.PrettyUtils
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 a -> Specification a -> NonEmpty String -> Maybe (NonEmpty String)
forall a.
HasSpec a =>
a -> Specification a -> NonEmpty String -> Maybe (NonEmpty String)
conformsToSpecE a
a (Specification a -> Specification a
forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification a
s) (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"call to conformsToSpecProp") of
  Maybe (NonEmpty String)
Nothing -> Bool -> Property
forall prop. Testable prop => prop -> Property
QC.property Bool
True
  Just NonEmpty String
msgs -> String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
QC.counterexample ([String] -> String
unlines (NonEmpty String -> [String]
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 = Specification a -> Specification a
forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification a
spec
   in Gen a -> (a -> [a]) -> (a -> String) -> (a -> Property) -> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property
QC.forAllShrinkShow (Specification a -> Gen a
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec Specification a
sspec) (Specification a -> a -> [a]
forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification a
sspec) a -> String
pp ((a -> Property) -> Property) -> (a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \a
a ->
        Specification a -> a -> p -> Property
forall p a. Testable p => Specification a -> a -> p -> Property
monitorSpec Specification a
spec a
a (p -> Property) -> p -> Property
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 = Specification a -> (a -> String) -> (a -> p) -> Property
forall a p.
(HasSpec a, Testable p) =>
Specification a -> (a -> String) -> (a -> p) -> Property
forAllSpecShow Specification a
spec a -> String
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 = Specification a -> Specification a
forall a. HasSpec a => Specification a -> Specification a
simplifySpec Specification a
spec
   in Gen (GE a) -> (GE a -> [GE a]) -> (GE a -> Property) -> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
QC.forAllShrinkBlind
        (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 @_ @GE Specification a
sspec)
        ((a -> GE a) -> [a] -> [GE a]
forall a b. (a -> b) -> [a] -> [b]
map a -> GE a
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([a] -> [GE a]) -> (GE a -> [a]) -> GE a -> [GE a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Specification a -> a -> [a]
forall a. HasSpec a => Specification a -> a -> [a]
shrinkWithSpec Specification a
sspec (a -> [a]) -> (GE a -> a) -> GE a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GE a -> a
forall a. GE a -> a
errorGE)
        ((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 -> p -> Property
forall prop. Testable prop => String -> prop -> Property
QC.counterexample (a -> String
forall a. Show a => a -> String
show a
a) (p -> Property) -> p -> Property
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 =
  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))

-- ===========================================================
-- 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 {k} (a :: k). 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 a b. (HasSpec a, HasSpec b) => 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. (HasSpec a, HasSpec 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 Bool] Bool -> TestableFn
forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn (BaseW '[SimpleRep Bool] Bool -> TestableFn)
-> BaseW '[SimpleRep Bool] Bool -> TestableFn
forall a b. (a -> b) -> a -> b
$ forall rng. GenericRequires rng => BaseW '[SimpleRep rng] rng
FromGenericW @Bool -- These require GenericC constraints
      , 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 NumOrdW
        NumOrdW '[Int, Int] Bool -> TestableFn
forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn (NumOrdW '[Int, Int] Bool -> TestableFn)
-> NumOrdW '[Int, Int] Bool -> TestableFn
forall a b. (a -> b) -> a -> b
$ forall a. OrdLike a => NumOrdW '[a, a] Bool
LessW @Int
      , NumOrdW '[Int, Int] Bool -> TestableFn
forall b (as :: [*]) (t :: [*] -> * -> *).
(Arbitrary (Specification b), Typeable (FunTy as b),
 AppRequires t as b) =>
t as b -> TestableFn
TestableFn (NumOrdW '[Int, Int] Bool -> TestableFn)
-> NumOrdW '[Int, Int] Bool -> TestableFn
forall a b. (a -> b) -> a -> b
$ forall a. OrdLike a => NumOrdW '[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
_ = []

-- ==========================================================
-- 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 =
  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