{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Constrained.Examples.CheatSheet where
import Data.Set (Set)
import Data.Set qualified as Set
import GHC.Generics
import Test.QuickCheck (Property, label)
import Constrained.API
import Constrained.Properties (forAllSpec)
specInt :: Specification Int
specInt :: Specification Int
specInt = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained 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
i 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
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
i
]
specInt' :: Specification Int
specInt' :: Specification Int
specInt' = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term Int
i ->
[ Term Int
i 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
i
]
specProd :: Specification (Int, Int)
specProd :: Specification (Int, Int)
specProd = 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 x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (Int, Int)
p forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
10
, forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (Int, Int)
p forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
100
]
specProd0 :: Specification (Int, Int)
specProd0 :: Specification (Int, Int)
specProd0 = 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. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x
fst_ Term (Int, Int)
p forall a. OrdLike a => Term a -> Term a -> Term Bool
<. forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (Int, Int)
p
specProd1 :: Specification (Int, Int)
specProd1 :: Specification (Int, Int)
specProd1 = 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 ->
Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
y
nested :: Specification ((Int, Int), (Int, Int))
nested :: Specification ((Int, Int), (Int, Int))
nested =
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term ((Int, Int), (Int, Int))
pp ->
forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term ((Int, Int), (Int, Int))
pp forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
p1 Term (Int, Int)
p2 ->
forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int)
p1 forall a b. (a -> b) -> a -> b
$ \Term Int
x1 Term Int
y1 ->
forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Int, Int)
p2 forall a b. (a -> b) -> a -> b
$ \Term Int
x2 Term Int
y2 ->
[Term Int
x1 forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
y1, Term Int
y1 forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
x2, Term Int
x2 forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
y2]
specProd2 :: Specification (Int, Int)
specProd2 :: Specification (Int, Int)
specProd2 = 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
y
solverOrder :: Specification (Int, Int)
solverOrder :: Specification (Int, Int)
solverOrder = 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
y
, Term Int
y forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
10
]
solverOrder' :: Specification (Int, Int)
solverOrder' :: Specification (Int, Int)
solverOrder' = 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|x|] Term Int
[var|y|] ->
[ Term Int
x 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
10
]
tightFit0 :: Specification (Int, Int)
tightFit0 :: Specification (Int, Int)
tightFit0 = 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
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
x
, Term Int
x forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
y
]
tightFit1 :: Specification (Int, Int)
tightFit1 :: Specification (Int, Int)
tightFit1 = 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
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. 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
y
, Term Int
y forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term Int
x
]
booleanExample :: Specification (Int, Int)
booleanExample :: Specification (Int, Int)
booleanExample = 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 q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
(Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
x)
(Term Int
y forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
10)
(Term Int
y forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int
20)
validPVPVersion :: Specification (Int, Int)
validPVPVersion :: Specification (Int, Int)
validPVPVersion = 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
ma Term Int
mi -> [Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
ma, Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Int
mi]
canFollowExample :: Specification ((Int, Int), (Int, Int))
canFollowExample :: Specification ((Int, Int), (Int, Int))
canFollowExample = 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
]
, Term (Int, Int)
p forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (Int, Int)
validPVPVersion
, Term (Int, Int)
q forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (Int, Int)
validPVPVersion
]
sumExample :: Specification (Either Int Bool)
sumExample :: Specification (Either Int Bool)
sumExample = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Either Int Bool)
e ->
(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 (Either Int Bool)
e)
(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
i forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
0)
(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
b -> Term Bool -> Term Bool
not_ Term Bool
b)
sumExampleTwo :: Specification (Int, Either Int Bool)
sumExampleTwo :: Specification (Int, Either Int Bool)
sumExampleTwo = 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
i Term (Either Int Bool)
e ->
[ 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 (Either Int Bool)
e
(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
j -> Term Int
i forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
j)
(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
b -> Term Bool -> Term Bool
not_ Term Bool
b)
, forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
20 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
i
]
setExample :: Specification (Set Int, Set Int, Set Int)
setExample :: Specification (Set Int, Set Int, Set Int)
setExample = 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 (Set Int)
xs Term (Set Int)
ys Term (Set Int)
zs ->
[ Term (Set Int)
xs forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` (Term (Set Int)
ys forall a. Semigroup a => a -> a -> a
<> Term (Set Int)
zs)
, forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Set Int)
ys forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
10
]
forAllFollow0 :: Specification ((Int, Int), Set (Int, Int))
forAllFollow0 :: Specification ((Int, Int), Set (Int, Int))
forAllFollow0 = 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 (Set (Int, Int))
qs ->
[ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Int, Int))
qs forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
q -> forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term (Int, Int)
p Term (Int, Int)
q forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification ((Int, Int), (Int, Int))
canFollowExample
]
forAllFollow :: Specification ((Int, Int), Set (Int, Int))
forAllFollow :: Specification ((Int, Int), Set (Int, Int))
forAllFollow = 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 (Set (Int, Int))
qs ->
[ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set (Int, Int))
qs forall a b. (a -> b) -> a -> b
$ \Term (Int, Int)
q -> forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term (Int, Int)
p Term (Int, Int)
q forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification ((Int, Int), (Int, Int))
canFollowExample
, Term (Int, Int)
p forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Specification (Int, Int)
validPVPVersion
]
existentials :: Specification (Set Int, Set Int)
existentials :: Specification (Set Int, Set Int)
existentials = 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 (Set Int)
xs Term (Set Int)
ys ->
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (forall b. Term b -> b
eval Term (Set Int)
xs) (forall b. Term b -> b
eval Term (Set Int)
ys)) forall a b. (a -> b) -> a -> b
$ \Term (Set Int)
zs ->
[ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Bool
null_ Term (Set Int)
zs
, forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Set Int)
zs forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Term (Set Int)
xs
, forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Set Int)
zs forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Term (Set Int)
ys
, Term (Set Int)
xs forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term (Set Int)
zs
, Term (Set Int)
ys forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term (Set Int)
zs
]
data FooBarBaz = Foo Int Int | Bar Bool | Baz deriving (FooBarBaz -> FooBarBaz -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FooBarBaz -> FooBarBaz -> Bool
$c/= :: FooBarBaz -> FooBarBaz -> Bool
== :: FooBarBaz -> FooBarBaz -> Bool
$c== :: FooBarBaz -> FooBarBaz -> Bool
Eq, Int -> FooBarBaz -> ShowS
[FooBarBaz] -> ShowS
FooBarBaz -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FooBarBaz] -> ShowS
$cshowList :: [FooBarBaz] -> ShowS
show :: FooBarBaz -> String
$cshow :: FooBarBaz -> String
showsPrec :: Int -> FooBarBaz -> ShowS
$cshowsPrec :: Int -> FooBarBaz -> ShowS
Show, forall x. Rep FooBarBaz x -> FooBarBaz
forall x. FooBarBaz -> Rep FooBarBaz x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep FooBarBaz x -> FooBarBaz
$cfrom :: forall x. FooBarBaz -> Rep FooBarBaz x
Generic)
instance HasSimpleRep FooBarBaz
instance HasSpec FooBarBaz
fooBarBaz :: Specification FooBarBaz
fooBarBaz :: Specification FooBarBaz
fooBarBaz = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term FooBarBaz
fbb ->
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 FooBarBaz
fbb
(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 -> Term Int
i forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
j)
(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
b -> Term Bool -> Term Bool
not_ Term Bool
b)
(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)
reifyExample :: Specification (Int, Int)
reifyExample :: Specification (Int, Int)
reifyExample = 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|a|] Term Int
[var|b|] ->
forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
reifies Term Int
b Term Int
a forall a b. (a -> b) -> a -> b
$ \Int
x -> forall a. Integral a => a -> a -> a
mod Int
x Int
10
reifyExample' :: Specification (Int, Int)
reifyExample' :: Specification (Int, Int)
reifyExample' = 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 p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Int
b forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Int -> Term Int -> Term Int
mod_ Term Int
a Term Int
10
, Term Int
b forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term Int
a
]
where
mod_ :: Term Int -> Term Int -> Term Int
mod_ :: Term Int -> Term Int -> Term Int
mod_ = forall a. HasCallStack => String -> a
error String
"This doesn't exist"
monitorExample :: Specification (Either Int Int)
monitorExample :: Specification (Either Int Int)
monitorExample = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Either Int Int)
e ->
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 (Either Int Int)
e
(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 Int
_ -> ((forall b. Term b -> b) -> Property -> Property) -> Pred
monitor forall a b. (a -> b) -> a -> b
$ \forall b. Term b -> b
_ -> forall prop. Testable prop => String -> prop -> Property
label String
"Left")
(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 Int
_ -> ((forall b. Term b -> b) -> Property -> Property) -> Pred
monitor forall a b. (a -> b) -> a -> b
$ \forall b. Term b -> b
_ -> forall prop. Testable prop => String -> prop -> Property
label String
"Right")
prop_monitoring :: Property
prop_monitoring :: Property
prop_monitoring = forall a p.
(HasSpec a, Testable p) =>
Specification a -> (a -> p) -> Property
forAllSpec Specification (Either Int Int)
monitorExample forall a b. (a -> b) -> a -> b
$ \Either Int Int
_ -> Bool
True
chooseSpecExample :: Specification Int
chooseSpecExample :: Specification Int
chooseSpecExample =
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 b. (a -> b) -> a -> b
$ \Term Int
i -> Term Int
i 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 forall a b. (a -> b) -> a -> b
$ \Term Int
i -> Term Int
0 forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Int
i)
prop_chooseSpec :: Property
prop_chooseSpec :: Property
prop_chooseSpec = forall a p.
(HasSpec a, Testable p) =>
Specification a -> (a -> p) -> Property
forAllSpec Specification Int
chooseSpecExample forall a b. (a -> b) -> a -> b
$ \Int
i ->
forall prop. Testable prop => String -> prop -> Property
label (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. Num a => a -> a
signum Int
i) Bool
True