{-# 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 = (Term (Int, Int) -> PredD Deps) -> Specification (Int, Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Int, Int) -> PredD Deps) -> Specification (Int, Int))
-> (Term (Int, Int) -> PredD Deps) -> Specification (Int, Int)
forall a b. (a -> b) -> a -> b
$ \ Term (Int, Int)
[var| p |] ->
  Term (Int, Int)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (Term Bool)
-> PredD Deps
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> PredD Deps
match Term (Int, Int)
p (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (Term Bool)
 -> PredD Deps)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (Term Bool)
-> PredD Deps
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var| x |] Term Int
[var| y |] ->
    Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
y

simplePairSpec :: Specification (Int, Int)
simplePairSpec :: Specification (Int, Int)
simplePairSpec = (Term (Int, Int) -> PredD Deps) -> Specification (Int, Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Int, Int) -> PredD Deps) -> Specification (Int, Int))
-> (Term (Int, Int) -> PredD Deps) -> Specification (Int, Int)
forall a b. (a -> b) -> a -> b
$ \(String -> Term (Int, Int) -> Term (Int, Int)
forall a. String -> Term a -> Term a
name String
"p" -> Term (Int, Int)
p) ->
  Term (Int, Int)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [PredD Deps]
-> PredD Deps
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> PredD Deps
match Term (Int, Int)
p (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [PredD Deps]
 -> PredD Deps)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [PredD Deps]
-> PredD Deps
forall a b. (a -> b) -> a -> b
$ \(String -> Term Int -> Term Int
forall a. String -> Term a -> Term a
name String
"x" -> Term Int
x) Term Int
y ->
    [ Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term Int
x Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. Term Int
0
    , Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ String -> Term Int -> Term Int
forall a. String -> Term a -> Term a
name String
"y" Term Int
y Term Int -> Term Int -> Term Bool
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) -> PredD Deps
monitor (((forall a. Term a -> a) -> Property -> Property) -> PredD Deps)
-> ((forall a. Term a -> a) -> Property -> Property) -> PredD Deps
forall a b. (a -> b) -> a -> b
$ \forall a. Term a -> a
eval ->
        Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
QC.classify (Term Int -> Int
forall a. Term a -> a
eval Term Int
y Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) String
"positive y"
          (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> String -> Property -> Property
forall prop. Testable prop => Bool -> String -> prop -> Property
QC.classify (Term Int -> Int
forall a. Term a -> a
eval Term Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) String
"positive x"
    ]

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

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

sizeAddOrSub3 :: Specification Integer
sizeAddOrSub3 :: Specification Integer
sizeAddOrSub3 = (Term Integer -> Term Bool) -> Specification Integer
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Integer -> Term Bool) -> Specification Integer)
-> (Term Integer -> Term Bool) -> Specification Integer
forall a b. (a -> b) -> a -> b
$ \Term Integer
s ->
  Term Integer
4 Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
s Term Integer -> Term Integer -> Term Integer
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 = Integer -> Specification Integer
forall a. OrdLike a => a -> Specification a
ltSpec Integer
0 Specification Integer
-> Specification Integer -> Specification Integer
forall a. Semigroup a => a -> a -> a
<> ((Term Integer -> Term Bool) -> Specification Integer
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Integer -> Term Bool) -> Specification Integer)
-> (Term Integer -> Term Bool) -> Specification Integer
forall a b. (a -> b) -> a -> b
$ \Term Integer
s -> Term Integer
4 Term Integer -> Term Integer -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
2 Term Integer -> Term Integer -> Term Integer
forall a. Num a => a -> a -> a
- Term Integer
s)

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

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

orPair :: Specification (Int, Int)
orPair :: Specification (Int, Int)
orPair = FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (Term Bool)
-> Specification (Int, Int)
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (Term Bool)
 -> Specification (Int, Int))
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (Term Bool)
-> Specification (Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y ->
  Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
5 Term Bool -> Term Bool -> Term Bool
||. Term Int
y Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
5

trickyCompositional :: Specification (Int, Int)
trickyCompositional :: Specification (Int, Int)
trickyCompositional = (Term (Int, Int) -> PredD Deps) -> Specification (Int, Int)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Int, Int) -> PredD Deps) -> Specification (Int, Int))
-> (Term (Int, Int) -> PredD Deps) -> Specification (Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p ->
  Term (Int, Int) -> Specification (Int, Int) -> PredD Deps
forall a. HasSpec a => Term a -> Specification a -> PredD Deps
satisfies Term (Int, Int)
p Specification (Int, Int)
simplePairSpec PredD Deps -> PredD Deps -> PredD Deps
forall a. Semigroup a => a -> a -> a
<> Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term (Int, Int) -> Term Int
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (Int, Int)
p Term Int -> Term Int -> Term Bool
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
(Int -> Foo -> ShowS)
-> (Foo -> String) -> ([Foo] -> ShowS) -> Show Foo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Foo -> ShowS
showsPrec :: Int -> Foo -> ShowS
$cshow :: Foo -> String
show :: Foo -> String
$cshowList :: [Foo] -> ShowS
showList :: [Foo] -> ShowS
Show, Foo -> Foo -> Bool
(Foo -> Foo -> Bool) -> (Foo -> Foo -> Bool) -> Eq Foo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Foo -> Foo -> Bool
== :: Foo -> Foo -> Bool
$c/= :: Foo -> Foo -> Bool
/= :: Foo -> Foo -> Bool
Eq, Eq Foo
Eq Foo =>
(Foo -> Foo -> Ordering)
-> (Foo -> Foo -> Bool)
-> (Foo -> Foo -> Bool)
-> (Foo -> Foo -> Bool)
-> (Foo -> Foo -> Bool)
-> (Foo -> Foo -> Foo)
-> (Foo -> Foo -> Foo)
-> Ord 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
$ccompare :: Foo -> Foo -> Ordering
compare :: Foo -> Foo -> Ordering
$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
>= :: Foo -> Foo -> Bool
$cmax :: Foo -> Foo -> Foo
max :: Foo -> Foo -> Foo
$cmin :: Foo -> Foo -> Foo
min :: Foo -> Foo -> Foo
Ord, (forall x. Foo -> Rep Foo x)
-> (forall x. Rep Foo x -> Foo) -> Generic Foo
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
$cfrom :: forall x. Foo -> Rep Foo x
from :: forall x. Foo -> Rep Foo x
$cto :: forall x. Rep Foo x -> Foo
to :: forall x. Rep Foo x -> Foo
Generic)

instance HasSimpleRep Foo

instance HasSpec Foo

fooSpec :: Specification Foo
fooSpec :: Specification Foo
fooSpec = (Term Foo -> PredD Deps) -> Specification Foo
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Foo -> PredD Deps) -> Specification Foo)
-> (Term Foo -> PredD Deps) -> Specification Foo
forall a b. (a -> b) -> a -> b
$ \Term Foo
foo ->
  (Term Foo
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep Foo)))
     (PredD Deps)
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a)))
     (PredD Deps)
caseOn Term Foo
foo)
    ( FunTy (MapList Term (Args Int)) [PredD Deps]
-> Weighted (BinderD Deps) Int
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args Int)) [PredD Deps]
 -> Weighted (BinderD Deps) Int)
-> FunTy (MapList Term (Args Int)) [PredD Deps]
-> Weighted (BinderD Deps) Int
forall a b. (a -> b) -> a -> b
$ \Term Int
i ->
        [ Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term Int
0 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
i
        , ((forall a. Term a -> a) -> Property -> Property) -> PredD Deps
monitor (((forall a. Term a -> a) -> Property -> Property) -> PredD Deps)
-> ((forall a. Term a -> a) -> Property -> Property) -> PredD Deps
forall a b. (a -> b) -> a -> b
$ \forall a. Term a -> a
_ -> Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
QC.cover Double
40 Bool
True String
"Foo"
        ]
    )
    ( FunTy (MapList Term (Args (Prod Int Int))) [PredD Deps]
-> Weighted (BinderD Deps) (Prod Int Int)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args (Prod Int Int))) [PredD Deps]
 -> Weighted (BinderD Deps) (Prod Int Int))
-> FunTy (MapList Term (Args (Prod Int Int))) [PredD Deps]
-> Weighted (BinderD Deps) (Prod Int Int)
forall a b. (a -> b) -> a -> b
$ \Term Int
i Term Int
j ->
        [ Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term Int
i Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
j
        , ((forall a. Term a -> a) -> Property -> Property) -> PredD Deps
monitor (((forall a. Term a -> a) -> Property -> Property) -> PredD Deps)
-> ((forall a. Term a -> a) -> Property -> Property) -> PredD Deps
forall a b. (a -> b) -> a -> b
$ \forall a. Term a -> a
_ -> Double -> Bool -> String -> Property -> Property
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 = FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (PredD Deps)
-> Specification (Int, Int)
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (PredD Deps)
 -> Specification (Int, Int))
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (PredD Deps)
-> Specification (Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term Int
a Term Int
b ->
  Term Int -> (Int -> Int) -> (Term Int -> Term Bool) -> PredD Deps
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> PredD Deps
reify Term Int
a (Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
10) ((Term Int -> Term Bool) -> PredD Deps)
-> (Term Int -> Term Bool) -> PredD Deps
forall a b. (a -> b) -> a -> b
$ \Term Int
a' -> Term Int
b Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
a'

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

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

testRewriteSpec :: Specification ((Int, Int), (Int, Int))
testRewriteSpec :: Specification ((Int, Int), (Int, Int))
testRewriteSpec = FunTy
  (MapList Term (Args (SimpleRep ((Int, Int), (Int, Int)))))
  (Term Bool)
-> Specification ((Int, Int), (Int, Int))
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep ((Int, Int), (Int, Int)))))
   (Term Bool)
 -> Specification ((Int, Int), (Int, Int)))
-> FunTy
     (MapList Term (Args (SimpleRep ((Int, Int), (Int, Int)))))
     (Term Bool)
-> Specification ((Int, Int), (Int, Int))
forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
x Term (Int, Int)
y ->
  Term (Int, Int)
x Term (Int, Int) -> Term (Int, Int) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (SimpleRep (Int, Int)) -> Term (Int, Int)
forall a.
(GenericRequires a, AppRequires BaseW '[SimpleRep a] a) =>
Term (SimpleRep a) -> Term a
fromGeneric_ (Term (Int, Int) -> Term (SimpleRep (Int, Int))
forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term (Int, Int)
y)

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

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

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

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

dependencyWeirdness :: Specification (Int, Int, Int)
dependencyWeirdness :: Specification (Int, Int, Int)
dependencyWeirdness = FunTy
  (MapList Term (Args (SimpleRep (Int, Int, Int)))) (PredD Deps)
-> Specification (Int, Int, Int)
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep (Int, Int, Int)))) (PredD Deps)
 -> Specification (Int, Int, Int))
-> FunTy
     (MapList Term (Args (SimpleRep (Int, Int, Int)))) (PredD Deps)
-> Specification (Int, Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y Term Int
z ->
  Term Int -> (Int -> Int) -> (Term Int -> Term Bool) -> PredD Deps
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> PredD Deps
reify (Term Int
x Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
y) Int -> Int
forall a. a -> a
id ((Term Int -> Term Bool) -> PredD Deps)
-> (Term Int -> Term Bool) -> PredD Deps
forall a b. (a -> b) -> a -> b
$ \Term Int
zv -> Term Int
z Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
zv

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

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

reifyYucky :: Specification (Int, Int, Int)
reifyYucky :: Specification (Int, Int, Int)
reifyYucky = FunTy
  (MapList Term (Args (SimpleRep (Int, Int, Int)))) [PredD Deps]
-> Specification (Int, Int, Int)
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep (Int, Int, Int)))) [PredD Deps]
 -> Specification (Int, Int, Int))
-> FunTy
     (MapList Term (Args (SimpleRep (Int, Int, Int)))) [PredD Deps]
-> Specification (Int, Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y Term Int
z ->
  [ Term Int -> (Int -> Int) -> (Term Int -> [Term Bool]) -> PredD Deps
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> PredD Deps
reify Term Int
x Int -> Int
forall a. a -> a
id ((Term Int -> [Term Bool]) -> PredD Deps)
-> (Term Int -> [Term Bool]) -> PredD Deps
forall a b. (a -> b) -> a -> b
$ \Term Int
w ->
      [ Term Int
y Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
w
      , Term Int
z Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
w
      ]
  , Term Int
z Term Int -> Term Int -> PredD Deps
forall a b.
(HasSpec a, HasSpec b) =>
Term a -> Term b -> PredD Deps
`dependsOn` Term Int
y
  ]

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

canFollowLike :: Specification ((Int, Int), (Int, Int))
canFollowLike :: Specification ((Int, Int), (Int, Int))
canFollowLike = FunTy
  (MapList Term (Args (SimpleRep ((Int, Int), (Int, Int)))))
  (PredD Deps)
-> Specification ((Int, Int), (Int, Int))
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep ((Int, Int), (Int, Int)))))
   (PredD Deps)
 -> Specification ((Int, Int), (Int, Int)))
-> FunTy
     (MapList Term (Args (SimpleRep ((Int, Int), (Int, Int)))))
     (PredD Deps)
-> Specification ((Int, Int), (Int, Int))
forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p Term (Int, Int)
q ->
  Term (Int, Int)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (PredD Deps)
-> PredD Deps
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> PredD Deps
match Term (Int, Int)
p (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (PredD Deps)
 -> PredD Deps)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) (PredD Deps)
-> PredD Deps
forall a b. (a -> b) -> a -> b
$ \Term Int
ma Term Int
mi ->
    Term (Int, Int)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [PredD Deps]
-> PredD Deps
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> PredD Deps
match Term (Int, Int)
q (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [PredD Deps]
 -> PredD Deps)
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [PredD Deps]
-> PredD Deps
forall a b. (a -> b) -> a -> b
$ \Term Int
ma' Term Int
mi' ->
      [ Term Bool -> Term Bool -> Term Bool -> PredD Deps
forall p q.
(IsPred p, IsPred q) =>
Term Bool -> p -> q -> PredD Deps
ifElse
          (Term Int
ma' Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
ma)
          (Term Int
mi' Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
mi Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
1)
          (Term Int
mi' Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
0)
      , Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term Int
ma' Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
ma Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
1
      , Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term Int
ma Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
ma'
      , Term Int
ma' Term Int -> Term Int -> PredD Deps
forall a b.
(HasSpec a, HasSpec b) =>
Term a -> Term b -> PredD Deps
`dependsOn` Term Int
ma
      ]

ifElseBackwards :: Specification (Int, Int)
ifElseBackwards :: Specification (Int, Int)
ifElseBackwards = FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [PredD Deps]
-> Specification (Int, Int)
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [PredD Deps]
 -> Specification (Int, Int))
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [PredD Deps]
-> Specification (Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term Int
p Term Int
q ->
  [ Term Bool -> Term Bool -> Term Bool -> PredD Deps
forall p q.
(IsPred p, IsPred q) =>
Term Bool -> p -> q -> PredD Deps
ifElse
      (Term Int
p Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
1)
      (Term Int
q Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
0)
      (Term Int
0 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
q)
  , Term Int
p Term Int -> Term Int -> PredD Deps
forall a b.
(HasSpec a, HasSpec b) =>
Term a -> Term b -> PredD Deps
`dependsOn` Term Int
q
  ]

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

assertRealMultiple :: Specification (Int, Int)
assertRealMultiple :: Specification (Int, Int)
assertRealMultiple = FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [PredD Deps]
-> Specification (Int, Int)
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [PredD Deps]
 -> Specification (Int, Int))
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [PredD Deps]
-> Specification (Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y ->
  [ Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
10
  , Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term Int
11 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
y
  , Term (Int, Int) -> ((Int, Int) -> Bool) -> PredD Deps
forall a.
(HasSpec Bool, HasSpec a) =>
Term a -> (a -> Bool) -> PredD Deps
assertReified (Term Int -> Term Int -> Term (Int, Int)
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) (((Int, Int) -> Bool) -> PredD Deps)
-> ((Int, Int) -> Bool) -> PredD Deps
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Bool) -> (Int, Int) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(/=)
  ]

reifiesMultiple :: Specification (Int, Int, Int)
reifiesMultiple :: Specification (Int, Int, Int)
reifiesMultiple = FunTy
  (MapList Term (Args (SimpleRep (Int, Int, Int)))) [PredD Deps]
-> Specification (Int, Int, Int)
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep (Int, Int, Int)))) [PredD Deps]
 -> Specification (Int, Int, Int))
-> FunTy
     (MapList Term (Args (SimpleRep (Int, Int, Int)))) [PredD Deps]
-> Specification (Int, Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y Term Int
z ->
  [ Term Int -> Term Int -> (Int -> Int) -> PredD Deps
forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> PredD Deps
reifies (Term Int
x Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
y) Term Int
z Int -> Int
forall a. a -> a
id
  , Term Int
x Term Int -> Term Int -> PredD Deps
forall a b.
(HasSpec a, HasSpec b) =>
Term a -> Term b -> PredD Deps
`dependsOn` Term Int
y
  ]

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

instance HasSimpleRep Three

instance HasSpec Three

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

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

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

threeSpecific :: Specification Three
threeSpecific :: Specification Three
threeSpecific = (Term Three -> [PredD Deps]) -> Specification Three
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Three -> [PredD Deps]) -> Specification Three)
-> (Term Three -> [PredD Deps]) -> Specification Three
forall a b. (a -> b) -> a -> b
$ \Term Three
o ->
  [ Term Three
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep Three)))
     (PredD Deps)
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a)))
     (PredD Deps)
caseOn
      Term Three
o
      (Int
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
True)
      (Int
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
1 (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
True)
      (Int
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
Int -> FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branchW Int
2 (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
True)
  , ((forall a. Term a -> a) -> Property -> Property) -> PredD Deps
monitor (((forall a. Term a -> a) -> Property -> Property) -> PredD Deps)
-> ((forall a. Term a -> a) -> Property -> Property) -> PredD Deps
forall a b. (a -> b) -> a -> b
$ \forall a. Term a -> a
eval ->
      String -> [(String, Double)] -> Property -> Property
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)]
        (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
QC.tabulate String
"TheValue" [Three -> String
forall a. Show a => a -> String
show (Three -> String) -> Three -> String
forall a b. (a -> b) -> a -> b
$ Term Three -> Three
forall a. Term a -> a
eval Term Three
o]
  ]

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

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

ifElseMany :: Specification (Bool, Int, Int)
ifElseMany :: Specification (Bool, Int, Int)
ifElseMany = FunTy
  (MapList Term (Args (SimpleRep (Bool, Int, Int)))) (PredD Deps)
-> Specification (Bool, Int, Int)
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep (Bool, Int, Int)))) (PredD Deps)
 -> Specification (Bool, Int, Int))
-> FunTy
     (MapList Term (Args (SimpleRep (Bool, Int, Int)))) (PredD Deps)
-> Specification (Bool, Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term Bool
b Term Int
x Term Int
y ->
  Term Bool -> [Term Bool] -> [Term Bool] -> PredD Deps
forall p q.
(IsPred p, IsPred q) =>
Term Bool -> p -> q -> PredD Deps
ifElse
    Term Bool
b
    [ Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
0
    , Term Int
y Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
10
    ]
    [ Term Int
0 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
x
    , Term Int
10 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
y
    ]

propBack :: Specification (Int, Int)
propBack :: Specification (Int, Int)
propBack = FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
-> Specification (Int, Int)
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
 -> Specification (Int, Int))
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
-> Specification (Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y ->
  [ Term Int
x Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
y Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
10
  , Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
20
  , Term Int
8 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
y
  ]

propBack' :: Specification (Int, Int)
propBack' :: Specification (Int, Int)
propBack' = FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
-> Specification (Int, Int)
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
 -> Specification (Int, Int))
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [Term Bool]
-> Specification (Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y ->
  [ Term Int
y Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
x Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
- Term Int
10
  , Term Int
20 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>. Term Int
x
  , Term Int
8 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>. Term Int
y
  , Term Int
y Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>. Term Int
x Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
- Term Int
20
  ]

propBack'' :: Specification (Int, Int)
propBack'' :: Specification (Int, Int)
propBack'' = FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [PredD Deps]
-> Specification (Int, Int)
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [PredD Deps]
 -> Specification (Int, Int))
-> FunTy (MapList Term (Args (SimpleRep (Int, Int)))) [PredD Deps]
-> Specification (Int, Int)
forall a b. (a -> b) -> a -> b
$ \Term Int
x Term Int
y ->
  [ Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term Int
y Term Int -> Term Int -> Term Int
forall a. Num a => a -> a -> a
+ Term Int
10 Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
x
  , Term Int
x Term Int -> Term Int -> PredD Deps
forall a b.
(HasSpec a, HasSpec b) =>
Term a -> Term b -> PredD Deps
`dependsOn` Term Int
y
  , Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term Int
x Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
20
  , Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term Int
8 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
y
  ]

chooseBackwards :: Specification (Int, [Int])
chooseBackwards :: Specification (Int, [Int])
chooseBackwards = (Term (Int, [Int]) -> [PredD Deps]) -> Specification (Int, [Int])
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Int, [Int]) -> [PredD Deps]) -> Specification (Int, [Int]))
-> (Term (Int, [Int]) -> [PredD Deps])
-> Specification (Int, [Int])
forall a b. (a -> b) -> a -> b
$ \Term (Int, [Int])
xy ->
  [ Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term (Int, [Int])
xy Term (Int, [Int]) -> Term [(Int, [Int])] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` [(Int, [Int])] -> Term [(Int, [Int])]
forall a. HasSpec a => a -> Term a
lit [(Int
1, [Int
1001 .. Int
1005]), (Int
2, [Int
1006 .. Int
1010])]
  , Term (Int, [Int])
-> FunTy
     (MapList Term (Args (SimpleRep (Int, [Int])))) (PredD Deps)
-> PredD Deps
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> PredD Deps
match Term (Int, [Int])
xy (FunTy (MapList Term (Args (SimpleRep (Int, [Int])))) (PredD Deps)
 -> PredD Deps)
-> FunTy
     (MapList Term (Args (SimpleRep (Int, [Int])))) (PredD Deps)
-> PredD Deps
forall a b. (a -> b) -> a -> b
$ \Term Int
_ Term [Int]
ys ->
      Term [Int] -> (Term Int -> Term Bool) -> PredD Deps
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> PredD Deps
forAll Term [Int]
ys ((Term Int -> Term Bool) -> PredD Deps)
-> (Term Int -> Term Bool) -> PredD Deps
forall a b. (a -> b) -> a -> b
$ \Term Int
y -> Term Int
0 Term Int -> Term Int -> Term Bool
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' = FunTy
  (MapList Term (Args (SimpleRep ([(Int, [Int])], (Int, [Int])))))
  [PredD Deps]
-> Specification ([(Int, [Int])], (Int, [Int]))
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep ([(Int, [Int])], (Int, [Int])))))
   [PredD Deps]
 -> Specification ([(Int, [Int])], (Int, [Int])))
-> FunTy
     (MapList Term (Args (SimpleRep ([(Int, [Int])], (Int, [Int])))))
     [PredD Deps]
-> Specification ([(Int, [Int])], (Int, [Int]))
forall a b. (a -> b) -> a -> b
$ \ Term [(Int, [Int])]
[var| xys |] Term (Int, [Int])
[var| xy |] ->
  [ Term [(Int, [Int])]
-> FunTy
     (MapList Term (Args (SimpleRep (Int, [Int])))) (PredD Deps)
-> PredD Deps
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),
 IsProductType a, HasSpec a, GenericRequires a,
 ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> PredD Deps
forAll' Term [(Int, [Int])]
xys (FunTy (MapList Term (Args (SimpleRep (Int, [Int])))) (PredD Deps)
 -> PredD Deps)
-> FunTy
     (MapList Term (Args (SimpleRep (Int, [Int])))) (PredD Deps)
-> PredD Deps
forall a b. (a -> b) -> a -> b
$ \Term Int
_ Term [Int]
[var| ys |] ->
      Term [Int] -> (Term Int -> Term Bool) -> PredD Deps
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> PredD Deps
forAll Term [Int]
ys ((Term Int -> Term Bool) -> PredD Deps)
-> (Term Int -> Term Bool) -> PredD Deps
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var| y |] -> Term Int
1000 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
y
  , Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term Integer
0 Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term [(Int, [Int])] -> Term Integer
forall a. HasSpec a => Term [a] -> Term Integer
length_ Term [(Int, [Int])]
xys
  , Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ Term (Int, [Int])
xy Term (Int, [Int]) -> Term [(Int, [Int])] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` Term [(Int, [Int])]
xys
  , Term (Int, [Int])
-> FunTy
     (MapList Term (Args (SimpleRep (Int, [Int])))) (PredD Deps)
-> PredD Deps
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> PredD Deps
match Term (Int, [Int])
xy (FunTy (MapList Term (Args (SimpleRep (Int, [Int])))) (PredD Deps)
 -> PredD Deps)
-> FunTy
     (MapList Term (Args (SimpleRep (Int, [Int])))) (PredD Deps)
-> PredD Deps
forall a b. (a -> b) -> a -> b
$ \Term Int
_ Term [Int]
[var| ys |] ->
      Term [Int] -> (Term Int -> Term Bool) -> PredD Deps
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> PredD Deps
forAll Term [Int]
ys ((Term Int -> Term Bool) -> PredD Deps)
-> (Term Int -> Term Bool) -> PredD Deps
forall a b. (a -> b) -> a -> b
$ \ Term Int
[var| y |] -> Term Int
0 Term Int -> Term Int -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
y
  ]

whenTrueExists :: Specification Int
whenTrueExists :: Specification Int
whenTrueExists = (Term Int -> PredD Deps) -> Specification Int
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term Int -> PredD Deps) -> Specification Int)
-> (Term Int -> PredD Deps) -> Specification Int
forall a b. (a -> b) -> a -> b
$ \Term Int
x ->
  Term Bool -> PredD Deps -> PredD Deps
forall p. IsPred p => Term Bool -> p -> PredD Deps
whenTrue ([var| x |] Term Int -> Term Int -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
0) (PredD Deps -> PredD Deps) -> PredD Deps -> PredD Deps
forall a b. (a -> b) -> a -> b
$
    ((forall a. Term a -> a) -> GE Bool)
-> (Term Bool -> [Term Bool]) -> PredD Deps
forall a p.
(HasSpec a, IsPred p) =>
((forall a. Term a -> a) -> GE a) -> (Term a -> p) -> PredD Deps
exists (\forall a. Term a -> a
_ -> Bool -> GE Bool
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False) ((Term Bool -> [Term Bool]) -> PredD Deps)
-> (Term Bool -> [Term Bool]) -> PredD Deps
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 = FunTy
  (MapList Term (Args (SimpleRep ([Int], Maybe ((), [Int])))))
  (PredD Deps)
-> Specification ([Int], Maybe ((), [Int]))
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, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep ([Int], Maybe ((), [Int])))))
   (PredD Deps)
 -> Specification ([Int], Maybe ((), [Int])))
-> FunTy
     (MapList Term (Args (SimpleRep ([Int], Maybe ((), [Int])))))
     (PredD Deps)
-> Specification ([Int], Maybe ((), [Int]))
forall a b. (a -> b) -> a -> b
$ \ Term [Int]
[var| options |] Term (Maybe ((), [Int]))
[var| mpair |] ->
  Term (Maybe ((), [Int]))
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep (Maybe ((), [Int])))))
     (PredD Deps)
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a)))
     (PredD Deps)
caseOn
    Term (Maybe ((), [Int]))
mpair
    (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
False)
    ( FunTy (MapList Term (Args ((), [Int]))) (PredD Deps)
-> Weighted (BinderD Deps) ((), [Int])
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ((), [Int]))) (PredD Deps)
 -> Weighted (BinderD Deps) ((), [Int]))
-> FunTy (MapList Term (Args ((), [Int]))) (PredD Deps)
-> Weighted (BinderD Deps) ((), [Int])
forall a b. (a -> b) -> a -> b
$ \Term ((), [Int])
pair -> Term ((), [Int])
-> FunTy (MapList Term (ProductAsList ((), [Int]))) [PredD Deps]
-> PredD Deps
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> PredD Deps
match Term ((), [Int])
pair (FunTy (MapList Term (ProductAsList ((), [Int]))) [PredD Deps]
 -> PredD Deps)
-> FunTy (MapList Term (ProductAsList ((), [Int]))) [PredD Deps]
-> PredD Deps
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
unit Term [Int]
ints ->
        [ Term [Int] -> (Term Int -> PredD Deps) -> PredD Deps
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> PredD Deps
forAll Term [Int]
ints ((Term Int -> PredD Deps) -> PredD Deps)
-> (Term Int -> PredD Deps) -> PredD Deps
forall a b. (a -> b) -> a -> b
$ \Term Int
int -> Term [Int]
-> ([Int] -> [Int]) -> (Term [Int] -> Term Bool) -> PredD Deps
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> PredD Deps
reify Term [Int]
options [Int] -> [Int]
forall a. a -> a
id ((Term [Int] -> Term Bool) -> PredD Deps)
-> (Term [Int] -> Term Bool) -> PredD Deps
forall a b. (a -> b) -> a -> b
$ \Term [Int]
xs -> Term Int
int Term Int -> Term [Int] -> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` Term [Int]
xs
        , Term Bool -> PredD Deps
forall p. IsPred p => p -> PredD Deps
assert (Term Bool -> PredD Deps) -> Term Bool -> PredD Deps
forall a b. (a -> b) -> a -> b
$ TermD Deps ()
unit TermD Deps () -> TermD Deps () -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. () -> TermD Deps ()
forall a. HasSpec a => a -> Term a
lit ()
        ]
    )