{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

module Constrained.Examples.Basic where

import Constrained.API
import GHC.Generics
import Test.QuickCheck qualified as QC

leqPair :: Specification (Int, Int)
leqPair :: Specification (Int, Int)
leqPair = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (Int, Int)
[var| p |] ->
  forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int)
p forall a b. (a -> b) -> a -> b
$ \ Term Int
[var| x |] Term Int
[var| y |] ->
    Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
y

simplePairSpec :: Specification (Int, Int)
simplePairSpec :: Specification (Int, Int)
simplePairSpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \(forall a. String -> Term a -> Term a
name String
"p" -> Term (Int, Int)
p) ->
  forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int)
p forall a b. (a -> b) -> a -> b
$ \(forall a. String -> Term a -> Term a
name String
"x" -> Term Int
x) Term Int
y ->
    [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
x forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Term Int
0
    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. String -> Term a -> Term a
name String
"y" Term Int
y forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Term Int
0
    , -- You can use `monitor` to add QuickCheck property modifiers for
      -- monitoring distribution, like classify, label, and cover, to your
      -- specification
      ((forall a. Term a -> a) -> Property -> Property) -> Pred
monitor forall a b. (a -> b) -> a -> b
$ \forall a. Term a -> a
eval ->
        forall prop. Testable prop => Bool -> String -> prop -> Property
QC.classify (forall a. Term a -> a
eval Term Int
y forall a. Ord a => a -> a -> Bool
> Int
0) String
"positive y"
          forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop. Testable prop => Bool -> String -> prop -> Property
QC.classify (forall a. Term a -> a
eval Term Int
x forall a. Ord a => a -> a -> Bool
> Int
0) String
"positive x"
    ]

sizeAddOrSub1 :: Specification Integer
sizeAddOrSub1 :: Specification Integer
sizeAddOrSub1 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Integer
s ->
  Term Integer
4 forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
s forall a. Num a => a -> a -> a
+ Term Integer
2

sizeAddOrSub2 :: Specification Integer
sizeAddOrSub2 :: Specification Integer
sizeAddOrSub2 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Integer
s ->
  Term Integer
4 forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
2 forall a. Num a => a -> a -> a
+ Term Integer
s

sizeAddOrSub3 :: Specification Integer
sizeAddOrSub3 :: Specification Integer
sizeAddOrSub3 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Integer
s ->
  Term Integer
4 forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
s forall a. Num a => a -> a -> a
- Term Integer
2

-- | We expect a negative Integer, so ltSpec tests for that.
sizeAddOrSub4 :: Specification Integer
sizeAddOrSub4 :: Specification Integer
sizeAddOrSub4 = forall a. OrdLike a => a -> Specification a
ltSpec Integer
0 forall a. Semigroup a => a -> a -> a
<> (forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Integer
s -> Term Integer
4 forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
2 forall a. Num a => a -> a -> a
- Term Integer
s)

sizeAddOrSub5 :: Specification Integer
sizeAddOrSub5 :: Specification Integer
sizeAddOrSub5 = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Integer
s ->
  Term Integer
2 forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
12 forall a. Num a => a -> a -> a
- Term Integer
s

listSubSize :: Specification [Int]
listSubSize :: Specification [Int]
listSubSize = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term [Int]
s ->
  Term Integer
2 forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
12 forall a. Num a => a -> a -> a
- (forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [Int]
s)

orPair :: Specification (Int, Int)
orPair :: Specification (Int, Int)
orPair = forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y ->
  Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
5 Term Bool -> Term Bool -> Term Bool
||. Term Int
y forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
5

trickyCompositional :: Specification (Int, Int)
trickyCompositional :: Specification (Int, Int)
trickyCompositional = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p ->
  forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Int, Int)
p Specification (Int, Int)
simplePairSpec forall a. Semigroup a => a -> a -> a
<> forall p. IsPred p => p -> Pred
assert (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (Int, Int)
p forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
1000)

data Foo = Foo Int | Bar Int Int
  deriving (Int -> Foo -> ShowS
[Foo] -> ShowS
Foo -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Foo] -> ShowS
$cshowList :: [Foo] -> ShowS
show :: Foo -> String
$cshow :: Foo -> String
showsPrec :: Int -> Foo -> ShowS
$cshowsPrec :: Int -> Foo -> ShowS
Show, Foo -> Foo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Foo -> Foo -> Bool
$c/= :: Foo -> Foo -> Bool
== :: Foo -> Foo -> Bool
$c== :: Foo -> Foo -> Bool
Eq, Eq Foo
Foo -> Foo -> Bool
Foo -> Foo -> Ordering
Foo -> Foo -> Foo
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Foo -> Foo -> Foo
$cmin :: Foo -> Foo -> Foo
max :: Foo -> Foo -> Foo
$cmax :: Foo -> Foo -> Foo
>= :: Foo -> Foo -> Bool
$c>= :: Foo -> Foo -> Bool
> :: Foo -> Foo -> Bool
$c> :: Foo -> Foo -> Bool
<= :: Foo -> Foo -> Bool
$c<= :: Foo -> Foo -> Bool
< :: Foo -> Foo -> Bool
$c< :: Foo -> Foo -> Bool
compare :: Foo -> Foo -> Ordering
$ccompare :: Foo -> Foo -> Ordering
Ord, forall x. Rep Foo x -> Foo
forall x. Foo -> Rep Foo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Foo x -> Foo
$cfrom :: forall x. Foo -> Rep Foo x
Generic)

instance HasSimpleRep Foo
instance HasSpec Foo

fooSpec :: Specification Foo
fooSpec :: Specification Foo
fooSpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Foo
foo ->
  (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term Foo
foo)
    ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
i ->
        [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
i
        , ((forall a. Term a -> a) -> Property -> Property) -> Pred
monitor forall a b. (a -> b) -> a -> b
$ \forall a. Term a -> a
_ -> forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
QC.cover Double
40 Bool
True String
"Foo"
        ]
    )
    ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term Int
i Term Int
j ->
        [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
i forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
j
        , ((forall a. Term a -> a) -> Property -> Property) -> Pred
monitor forall a b. (a -> b) -> a -> b
$ \forall a. Term a -> a
_ -> forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
QC.cover Double
40 Bool
True String
"Bar"
        ]
    )

intSpec :: Specification (Int, Int)
intSpec :: Specification (Int, Int)
intSpec = forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term Int
a Term Int
b ->
  forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term Int
a (forall a. Integral a => a -> a -> a
`mod` Int
10) forall a b. (a -> b) -> a -> b
$ \Term Int
a' -> Term Int
b forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
a'

mapElemKeySpec :: Specification Int
mapElemKeySpec :: Specification Int
mapElemKeySpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Int
n ->
  forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term Int
n forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => a -> Term a
lit (Bool
False, Int
4)) forall a b. (a -> b) -> a -> b
$ \(Term (Int, (Bool, Int))
p :: Term (Int, (Bool, Int))) ->
    forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (Int, (Bool, Int))
p)) forall a b. (a -> b) -> a -> b
$ \Term Int
x ->
      [Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
10, Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
x, Term Bool -> Term Bool
not_ forall a b. (a -> b) -> a -> b
$ forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ Term Int
n forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => a -> Term a
lit []]

intRangeSpec :: Int -> Specification Int
intRangeSpec :: Int -> Specification Int
intRangeSpec Int
a = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Int
n -> Term Int
n forall a. OrdLike a => Term a -> Term a -> Term Bool
<. forall a. HasSpec a => a -> Term a
lit Int
a

testRewriteSpec :: Specification ((Int, Int), (Int, Int))
testRewriteSpec :: Specification ((Int, Int), (Int, Int))
testRewriteSpec = forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
x Term (Int, Int)
y ->
  Term (Int, Int)
x forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a.
(GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ (forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term (Int, Int)
y)

pairSingletonSpec :: Specification (Int, Int)
pairSingletonSpec :: Specification (Int, Int)
pairSingletonSpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
q ->
  forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (forall a. (Ord a, HasSpec a) => Term a -> Term (Set a)
singleton_ Term (Int, Int)
q) forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p ->
    forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (Int, Int)
p) forall a b. (a -> b) -> a -> b
$ \Term Int
x ->
      forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (Int, Int)
p) forall a b. (a -> b) -> a -> b
$ \Term Int
y ->
        Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
y

parallelLet :: Specification (Int, Int)
parallelLet :: Specification (Int, Int)
parallelLet = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p ->
  [ forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (Int, Int)
p) forall a b. (a -> b) -> a -> b
$ \Term Int
x -> Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
x
  , forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (Int, Int)
p) forall a b. (a -> b) -> a -> b
$ \Term Int
x -> Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
0
  ]

letExists :: Specification (Int, Int)
letExists :: Specification (Int, Int)
letExists = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p ->
  [ forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (Int, Int)
p) forall a b. (a -> b) -> a -> b
$ \Term Int
x -> Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
x
  , forall a p.
(HasSpec a, IsPred p) =>
((forall a. Term a -> a) -> GE a) -> (Term a -> p) -> Pred
exists (\forall a. Term a -> a
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd (forall a. Term a -> a
eval Term (Int, Int)
p)) forall a b. (a -> b) -> a -> b
$
      \Term Int
x ->
        [ Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
0
        , forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (Int, Int)
p forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
x
        ]
  ]

letExistsLet :: Specification (Int, Int)
letExistsLet :: Specification (Int, Int)
letExistsLet = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p ->
  [ forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (Int, Int)
p) forall a b. (a -> b) -> a -> b
$ \Term Int
x -> Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
x
  , forall a p.
(HasSpec a, IsPred p) =>
((forall a. Term a -> a) -> GE a) -> (Term a -> p) -> Pred
exists (\forall a. Term a -> a
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd (forall a. Term a -> a
eval Term (Int, Int)
p)) forall a b. (a -> b) -> a -> b
$
      \Term Int
x ->
        [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
0
        , forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (Int, Int)
p) forall a b. (a -> b) -> a -> b
$ \Term Int
y ->
            [ Term Int
x forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
y
            , Term Int
y forall a. OrdLike a => Term a -> Term a -> Term Bool
<. -Term Int
1
            ]
        ]
  ]

dependencyWeirdness :: Specification (Int, Int, Int)
dependencyWeirdness :: Specification (Int, Int, Int)
dependencyWeirdness = forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y Term Int
z ->
  forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify (Term Int
x forall a. Num a => a -> a -> a
+ Term Int
y) forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \Term Int
zv -> Term Int
z forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
zv

parallelLetPair :: Specification (Int, Int)
parallelLetPair :: Specification (Int, Int)
parallelLetPair = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p ->
  [ forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int)
p forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y ->
      [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
y
      , Term Int
y forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term Int
x
      ]
  , forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int)
p forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y -> Term Int
y forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
x
  ]

existsUnfree :: Specification Int
existsUnfree :: Specification Int
existsUnfree = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Int
_ -> forall a p.
(HasSpec a, IsPred p) =>
((forall a. Term a -> a) -> GE a) -> (Term a -> p) -> Pred
exists (\forall a. Term a -> a
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
1) forall a b. (a -> b) -> a -> b
$ \Term Int
y -> Term Int
y forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall a. HasSpec a => a -> Term a
lit [Int
1, Int
2 :: Int]

reifyYucky :: Specification (Int, Int, Int)
reifyYucky :: Specification (Int, Int, Int)
reifyYucky = forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y Term Int
z ->
  [ forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term Int
x forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \Term Int
w ->
      [ Term Int
y forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
w
      , Term Int
z forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
w
      ]
  , Term Int
z forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term Int
y
  ]

basicSpec :: Specification Int
basicSpec :: Specification Int
basicSpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Int
x ->
  forall a p.
(HasSpec a, IsPred p) =>
((forall a. Term a -> a) -> GE a) -> (Term a -> p) -> Pred
exists (\forall a. Term a -> a
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. Term a -> a
eval Term Int
x) forall a b. (a -> b) -> a -> b
$ \Term Int
y ->
    forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term Int
x forall a b. (a -> b) -> a -> b
$ forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Int
x' ->
      Term Int
x' forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
1 forall a. Num a => a -> a -> a
+ Term Int
y

canFollowLike :: Specification ((Int, Int), (Int, Int))
canFollowLike :: Specification ((Int, Int), (Int, Int))
canFollowLike = forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p Term (Int, Int)
q ->
  forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int)
p forall a b. (a -> b) -> a -> b
$ \Term Int
ma Term Int
mi ->
    forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int)
q forall a b. (a -> b) -> a -> b
$ \Term Int
ma' Term Int
mi' ->
      [ forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
          (Term Int
ma' forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
ma)
          (Term Int
mi' forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
mi forall a. Num a => a -> a -> a
+ Term Int
1)
          (Term Int
mi' forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
0)
      , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
ma' forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
ma forall a. Num a => a -> a -> a
+ Term Int
1
      , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
ma forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
ma'
      , Term Int
ma' forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term Int
ma
      ]

ifElseBackwards :: Specification (Int, Int)
ifElseBackwards :: Specification (Int, Int)
ifElseBackwards = forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term Int
p Term Int
q ->
  [ forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
      (Term Int
p forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
1)
      (Term Int
q forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
0)
      (Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
q)
  , Term Int
p forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term Int
q
  ]

assertReal :: Specification Int
assertReal :: Specification Int
assertReal = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Int
x ->
  [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
10
  , forall a.
(HasSpec Bool, HasSpec a) =>
Term a -> (a -> Bool) -> Pred
assertReified Term Int
x (forall a. Ord a => a -> a -> Bool
<= Int
10)
  ]

assertRealMultiple :: Specification (Int, Int)
assertRealMultiple :: Specification (Int, Int)
assertRealMultiple = forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y ->
  [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
10
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
11 forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
y
  , forall a.
(HasSpec Bool, HasSpec a) =>
Term a -> (a -> Bool) -> Pred
assertReified (forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term Int
x Term Int
y) forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Eq a => a -> a -> Bool
(/=)
  ]

reifiesMultiple :: Specification (Int, Int, Int)
reifiesMultiple :: Specification (Int, Int, Int)
reifiesMultiple = forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y Term Int
z ->
  [ forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
reifies (Term Int
x forall a. Num a => a -> a -> a
+ Term Int
y) Term Int
z forall a. a -> a
id
  , Term Int
x forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term Int
y
  ]

data Three = One | Two | Three deriving (Eq Three
Three -> Three -> Bool
Three -> Three -> Ordering
Three -> Three -> Three
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Three -> Three -> Three
$cmin :: Three -> Three -> Three
max :: Three -> Three -> Three
$cmax :: Three -> Three -> Three
>= :: Three -> Three -> Bool
$c>= :: Three -> Three -> Bool
> :: Three -> Three -> Bool
$c> :: Three -> Three -> Bool
<= :: Three -> Three -> Bool
$c<= :: Three -> Three -> Bool
< :: Three -> Three -> Bool
$c< :: Three -> Three -> Bool
compare :: Three -> Three -> Ordering
$ccompare :: Three -> Three -> Ordering
Ord, Three -> Three -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Three -> Three -> Bool
$c/= :: Three -> Three -> Bool
== :: Three -> Three -> Bool
$c== :: Three -> Three -> Bool
Eq, Int -> Three -> ShowS
[Three] -> ShowS
Three -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Three] -> ShowS
$cshowList :: [Three] -> ShowS
show :: Three -> String
$cshow :: Three -> String
showsPrec :: Int -> Three -> ShowS
$cshowsPrec :: Int -> Three -> ShowS
Show, forall x. Rep Three x -> Three
forall x. Three -> Rep Three x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Three x -> Three
$cfrom :: forall x. Three -> Rep Three x
Generic)
instance HasSimpleRep Three
instance HasSpec Three

trueSpecUniform :: Specification Three
trueSpecUniform :: Specification Three
trueSpecUniform = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Three
o -> ((forall a. Term a -> a) -> Property -> Property) -> Pred
monitor forall a b. (a -> b) -> a -> b
$ \forall a. Term a -> a
eval -> forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
QC.cover Double
30 Bool
True (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. Term a -> a
eval Term Three
o)

three :: Specification Three
three :: Specification Three
three = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Three
o ->
  [ forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn
      Term Three
o
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Bool
True)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Bool
True)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Bool
True)
  , ((forall a. Term a -> a) -> Property -> Property) -> Pred
monitor forall a b. (a -> b) -> a -> b
$ \forall a. Term a -> a
eval -> forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
QC.cover Double
30 Bool
True (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. Term a -> a
eval Term Three
o)
  ]

three' :: Specification Three
three' :: Specification Three
three' = Specification Three
three forall a. Semigroup a => a -> a -> a
<> Specification Three
three

threeSpecific :: Specification Three
threeSpecific :: Specification Three
threeSpecific = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Three
o ->
  [ forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn
      Term Three
o
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Bool
True)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
1 forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Bool
True)
      (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted Binder a
branchW Int
2 forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Bool
True)
  , ((forall a. Term a -> a) -> Property -> Property) -> Pred
monitor forall a b. (a -> b) -> a -> b
$ \forall a. Term a -> a
eval ->
      forall prop.
Testable prop =>
String -> [(String, Double)] -> prop -> Property
QC.coverTable String
"TheValue" [(String
"One", Double
22), (String
"Two", Double
22), (String
"Three", Double
47)]
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop.
Testable prop =>
String -> [String] -> prop -> Property
QC.tabulate String
"TheValue" [forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. Term a -> a
eval Term Three
o]
  ]

threeSpecific' :: Specification Three
threeSpecific' :: Specification Three
threeSpecific' = Specification Three
threeSpecific forall a. Semigroup a => a -> a -> a
<> Specification Three
threeSpecific

posNegDistr :: Specification Int
posNegDistr :: Specification Int
posNegDistr =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Int
x ->
    [ ((forall a. Term a -> a) -> Property -> Property) -> Pred
monitor forall a b. (a -> b) -> a -> b
$ \forall a. Term a -> a
eval -> forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
QC.cover Double
60 (Int
0 forall a. Ord a => a -> a -> Bool
< forall a. Term a -> a
eval Term Int
x) String
"x positive"
    , Term Int
x forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` forall a.
HasSpec a =>
(Int, Specification a) -> (Int, Specification a) -> Specification a
chooseSpec (Int
1, forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained (forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
0)) (Int
2, forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained (Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<.))
    ]

ifElseMany :: Specification (Bool, Int, Int)
ifElseMany :: Specification (Bool, Int, Int)
ifElseMany = forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term Bool
b Term Int
x Term Int
y ->
  forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
    Term Bool
b
    [ Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
0
    , Term Int
y forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
10
    ]
    [ Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
x
    , Term Int
10 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
y
    ]

propBack :: Specification (Int, Int)
propBack :: Specification (Int, Int)
propBack = forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y ->
  [ Term Int
x forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
y forall a. Num a => a -> a -> a
+ Term Int
10
  , Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
20
  , Term Int
8 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
y
  ]

propBack' :: Specification (Int, Int)
propBack' :: Specification (Int, Int)
propBack' = forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y ->
  [ Term Int
y forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
x forall a. Num a => a -> a -> a
- Term Int
10
  , Term Int
20 forall a. OrdLike a => Term a -> Term a -> Term Bool
>. Term Int
x
  , Term Int
8 forall a. OrdLike a => Term a -> Term a -> Term Bool
>. Term Int
y
  , Term Int
y forall a. OrdLike a => Term a -> Term a -> Term Bool
>. Term Int
x forall a. Num a => a -> a -> a
- Term Int
20
  ]

propBack'' :: Specification (Int, Int)
propBack'' :: Specification (Int, Int)
propBack'' = forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y ->
  [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
y forall a. Num a => a -> a -> a
+ Term Int
10 forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
x
  , Term Int
x forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term Int
y
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
20
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
8 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
y
  ]

chooseBackwards :: Specification (Int, [Int])
chooseBackwards :: Specification (Int, [Int])
chooseBackwards = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Int, [Int])
xy ->
  [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Int, [Int])
xy forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall a. HasSpec a => a -> Term a
lit [(Int
1, [Int
1001 .. Int
1005]), (Int
2, [Int
1006 .. Int
1010])]
  , forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, [Int])
xy forall a b. (a -> b) -> a -> b
$ \Term Int
_ Term [Int]
ys ->
      forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
ys forall a b. (a -> b) -> a -> b
$ \Term Int
y -> Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
y
  ]

chooseBackwards' :: Specification ([(Int, [Int])], (Int, [Int]))
chooseBackwards' :: Specification ([(Int, [Int])], (Int, [Int]))
chooseBackwards' = forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \ Term [(Int, [Int])]
[var| xys |] Term (Int, [Int])
[var| xy |] ->
  [ forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
 HasSpec (SimpleRep a), HasSimpleRep a,
 All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
 HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term [(Int, [Int])]
xys forall a b. (a -> b) -> a -> b
$ \Term Int
_ Term [Int]
[var| ys |] ->
      forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
ys forall a b. (a -> b) -> a -> b
$ \ Term Int
[var| y |] -> Term Int
1000 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
y
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Integer
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. forall a. HasSpec a => Term [a] -> Term Integer
length_ Term [(Int, [Int])]
xys
  , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Int, [Int])
xy forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` Term [(Int, [Int])]
xys
  , forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, [Int])
xy forall a b. (a -> b) -> a -> b
$ \Term Int
_ Term [Int]
[var| ys |] ->
      forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
ys forall a b. (a -> b) -> a -> b
$ \ Term Int
[var| y |] -> Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
y
  ]

whenTrueExists :: Specification Int
whenTrueExists :: Specification Int
whenTrueExists = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Int
x ->
  forall p. IsPred p => Term Bool -> p -> Pred
whenTrue ([var| x |] forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
0) forall a b. (a -> b) -> a -> b
$
    forall a p.
(HasSpec a, IsPred p) =>
((forall a. Term a -> a) -> GE a) -> (Term a -> p) -> Pred
exists (\forall a. Term a -> a
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False) forall a b. (a -> b) -> a -> b
$ \Term Bool
b ->
      [ Term Bool -> Term Bool
not_ [var| b |]
      , Term Bool -> Term Bool
not_ (Term Bool -> Term Bool
not_ Term Bool
b)
      ]

wtfSpec :: Specification ([Int], Maybe ((), [Int]))
wtfSpec :: Specification ([Int], Maybe ((), [Int]))
wtfSpec = forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \ Term [Int]
[var| options |] Term (Maybe ((), [Int]))
[var| mpair |] ->
  forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
 TypeSpec a ~ TypeSpec (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn
    Term (Maybe ((), [Int]))
mpair
    (forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> Bool
False)
    ( forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ((), [Int])
pair -> forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term ((), [Int])
pair forall a b. (a -> b) -> a -> b
$ \Term ()
unit Term [Int]
ints ->
        [ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Int]
ints forall a b. (a -> b) -> a -> b
$ \Term Int
int -> forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term [Int]
options forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \Term [Int]
xs -> Term Int
int forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` Term [Int]
xs
        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term ()
unit forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit ()
        ]
    )