{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Test.Cardano.Ledger.Constrained.Spec where
import Cardano.Ledger.Coin (Coin (..), DeltaCoin (..))
import Cardano.Ledger.Core (Era (..))
import qualified Data.List as List
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import qualified Data.Maybe as Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Word (Word64)
import qualified Debug.Trace as Debug
import Lens.Micro hiding (set)
import Test.Cardano.Ledger.Constrained.Ast (Pred (..), Sum (..), Term (..), runPred)
import Test.Cardano.Ledger.Constrained.Classes (
Adds (..),
AddsSpec (..),
OrdCond (..),
genFromAddsSpec,
genFromNonNegAddsSpec,
lensAdds,
sumAdds,
varOnLeft,
varOnRight,
)
import Test.Cardano.Ledger.Constrained.Combinators (
addUntilSize,
errorMess,
fixSet,
mapFromSubset,
setSized,
subMapFromMapWithSize,
subsetFromSet,
suchThatErr,
superSetFromSet,
superSetFromSetWithSize,
)
import Test.Cardano.Ledger.Constrained.Env (Access (No), V (..), emptyEnv, storeVar)
import Test.Cardano.Ledger.Constrained.Monad
import Test.Cardano.Ledger.Constrained.Size (
Size (..),
atLeastDelta,
atMostAny,
genFromIntRange,
genFromNonNegIntRange,
genFromSize,
runSize,
seps,
sepsP,
)
import Test.Cardano.Ledger.Constrained.TypeRep (
Rep (..),
format,
genRep,
synopsis,
)
import Test.Cardano.Ledger.Core.Arbitrary ()
import Test.Cardano.Ledger.Generic.Proof (BabbageEra, Standard)
import Test.Cardano.Ledger.Shelley.Serialisation.EraIndepGenerators ()
import Test.Tasty
import Test.Tasty.QuickCheck hiding (total)
type TestEra = BabbageEra Standard
data SomeLens era t where
SomeLens :: Adds c => (Lens' t c) -> SomeLens era t
type TT = BabbageEra Standard
maxSize :: Size -> Int
maxSize :: Size -> Int
maxSize Size
SzAny = Int
atMostAny
maxSize (SzLeast Int
i) = Int
i forall a. Num a => a -> a -> a
+ Int
atLeastDelta
maxSize (SzMost Int
n) = Int
n
maxSize (SzRng Int
_ Int
j) = Int
j
maxSize (SzNever [String]
xs) = forall a. HasCallStack => String -> [String] -> a
errorMess String
"SzNever in maxSize" [String]
xs
minSize :: Size -> Int
minSize :: Size -> Int
minSize Size
SzAny = Int
0
minSize (SzLeast Int
n) = Int
n
minSize (SzMost Int
_) = Int
0
minSize (SzRng Int
i Int
_) = Int
i
minSize (SzNever [String]
xs) = forall a. HasCallStack => String -> [String] -> a
errorMess String
"SzNever in minSize" [String]
xs
genSize :: Gen Size
genSize :: Gen Size
genSize =
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
[ (Int
1, Int -> Size
SzLeast forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. TestAdd t => Gen t
pos)
, (Int
1, Int -> Size
SzMost forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> Gen Int
chooseInt (Int
0, Int
atMostAny))
, (Int
1, (\Int
x -> Int -> Int -> Size
SzRng Int
x Int
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. TestAdd t => Gen t
pos)
, (Int
1, do Int
lo <- (Int, Int) -> Gen Int
chooseInt (Int
0, Int
atMostAny); Int
hi <- forall a. Random a => (a, a) -> Gen a
choose (Int
lo forall a. Num a => a -> a -> a
+ Int
1, Int
lo forall a. Num a => a -> a -> a
+ Int
6); forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Int -> Size
SzRng Int
lo Int
hi))
]
genSizeRange :: Gen Size
genSizeRange :: Gen Size
genSizeRange =
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
[ (Int
1, Int -> Size
SzLeast forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
someInt)
, (Int
1, Int -> Size
SzMost forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
someInt)
, (Int
1, (\Int
x -> Int -> Int -> Size
SzRng Int
x Int
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
someInt)
, (Int
1, do Int
lo <- Gen Int
someInt; Int
hi <- forall a. Random a => (a, a) -> Gen a
choose (Int
lo forall a. Num a => a -> a -> a
+ Int
1, Int
lo forall a. Num a => a -> a -> a
+ Int
atMostAny); forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Int -> Size
SzRng Int
lo Int
hi))
]
where
someInt :: Gen Int
someInt = (Int, Int) -> Gen Int
chooseInt (-Int
atMostAny, Int
atMostAny)
genBigSize :: Int -> Gen Size
genBigSize :: Int -> Gen Size
genBigSize Int
n =
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
[ (Int
1, Int -> Size
SzLeast forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Int
n forall a. Num a => a -> a -> a
+ Int
1, Int
n forall a. Num a => a -> a -> a
+ Int
30))
,
(Int
1, (\Int
x -> Int -> Int -> Size
SzRng Int
x Int
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Int
n forall a. Num a => a -> a -> a
+ Int
1, Int
n forall a. Num a => a -> a -> a
+ Int
30))
, (Int
1, do Int
lo <- forall a. Random a => (a, a) -> Gen a
choose (Int
n forall a. Num a => a -> a -> a
+ Int
1, Int
n forall a. Num a => a -> a -> a
+ Int
30); Int
hi <- forall a. Random a => (a, a) -> Gen a
choose (Int
lo forall a. Num a => a -> a -> a
+ Int
1, Int
lo forall a. Num a => a -> a -> a
+ Int
30); forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Int -> Size
SzRng Int
lo Int
hi))
]
testSoundSize :: Gen Bool
testSoundSize :: Gen Bool
testSoundSize = do
Size
spec <- Gen Size
genSize
Int
ans <- Size -> Gen Int
genFromSize Size
spec
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Int -> Size -> Bool
runSize Int
ans Size
spec
testNonNegSize :: Gen Bool
testNonNegSize :: Gen Bool
testNonNegSize = do
Size
spec <- Gen Size
genSize
Int
ans <- Size -> Gen Int
genFromSize Size
spec
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Int
ans forall a. Ord a => a -> a -> Bool
>= Int
0
testMergeSize :: Gen Bool
testMergeSize :: Gen Bool
testMergeSize = do
Size
spec1 <- Gen Size
genSize
Size
spec2 <- Gen Size
genSize
case Size
spec1 forall a. Semigroup a => a -> a -> a
<> Size
spec2 of
SzNever [String]
_xs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
Size
SzAny -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
Size
spec -> do
Int
ans <- Size -> Gen Int
genFromSize Size
spec
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Int -> Size -> Bool
runSize Int
ans Size
spec Bool -> Bool -> Bool
&& Int -> Size -> Bool
runSize Int
ans Size
spec1 Bool -> Bool -> Bool
&& Int -> Size -> Bool
runSize Int
ans Size
spec2
genSizeByRep :: forall t era. Adds t => Rep era t -> Gen Size
genSizeByRep :: forall t era. Adds t => Rep era t -> Gen Size
genSizeByRep Rep era t
IntR = Gen Size
genSizeRange
genSizeByRep Rep era t
DeltaCoinR = Gen Size
genSizeRange
genSizeByRep Rep era t
RationalR = Gen Size
genSizeRange
genSizeByRep Rep era t
Word64R = Gen Size
genSize
genSizeByRep Rep era t
CoinR = Gen Size
genSize
genSizeByRep Rep era t
NaturalR = Gen Size
genSize
genSizeByRep Rep era t
r = forall a. HasCallStack => String -> a
error (String
"genSizeByRep " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era t
r forall a. [a] -> [a] -> [a]
++ String
" does not have an Adds instance." forall a. [a] -> [a] -> [a]
++ seq :: forall a b. a -> b -> b
seq (forall x. Adds x => x
zero @t) String
"")
genFromSizeByRep :: forall t era. Adds t => Rep era t -> Size -> Gen Int
genFromSizeByRep :: forall t era. Adds t => Rep era t -> Size -> Gen Int
genFromSizeByRep Rep era t
IntR = Size -> Gen Int
genFromIntRange
genFromSizeByRep Rep era t
DeltaCoinR = Size -> Gen Int
genFromIntRange
genFromSizeByRep Rep era t
RationalR = Size -> Gen Int
genFromIntRange
genFromSizeByRep Rep era t
Word64R = Size -> Gen Int
genFromNonNegIntRange
genFromSizeByRep Rep era t
CoinR = Size -> Gen Int
genFromNonNegIntRange
genFromSizeByRep Rep era t
NaturalR = Size -> Gen Int
genFromNonNegIntRange
genFromSizeByRep Rep era t
r = forall a. HasCallStack => String -> a
error (String
"genFromSizeByRep " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era t
r forall a. [a] -> [a] -> [a]
++ String
", does not have an Adds instance." forall a. [a] -> [a] -> [a]
++ seq :: forall a b. a -> b -> b
seq (forall x. Adds x => x
zero @t) String
"")
data SomeAdd era where Some :: Adds t => Rep era t -> SomeAdd era
instance Show (SomeAdd era) where
show :: SomeAdd era -> String
show (Some Rep era t
x) = forall a. Show a => a -> String
show Rep era t
x
genAddsRep :: Gen (SomeAdd era)
genAddsRep :: forall era. Gen (SomeAdd era)
genAddsRep = forall a. HasCallStack => [a] -> Gen a
elements [forall c era. Adds c => Rep era c -> SomeAdd era
Some forall era. Rep era Int
IntR, forall c era. Adds c => Rep era c -> SomeAdd era
Some forall era. Rep era DeltaCoin
DeltaCoinR, forall c era. Adds c => Rep era c -> SomeAdd era
Some forall era. Rep era (Ratio Integer)
RationalR, forall c era. Adds c => Rep era c -> SomeAdd era
Some forall era. Rep era Word64
Word64R, forall c era. Adds c => Rep era c -> SomeAdd era
Some forall era. Rep era Coin
CoinR, forall c era. Adds c => Rep era c -> SomeAdd era
Some forall era. Rep era Natural
NaturalR]
testMergeSize2 :: Gen Property
testMergeSize2 :: Gen Property
testMergeSize2 = do
Some Rep Any t
rep <- forall era. Gen (SomeAdd era)
genAddsRep
Size
spec1 <- forall t era. Adds t => Rep era t -> Gen Size
genSizeByRep Rep Any t
rep
Size
spec2 <- forall t era. Adds t => Rep era t -> Gen Size
genSizeByRep Rep Any t
rep
case Size
spec1 forall a. Semigroup a => a -> a -> a
<> Size
spec2 of
SzNever [String]
_xs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property Bool
True
Size
SzAny -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property Bool
True
Size
spec -> do
Int
ans <- forall t era. Adds t => Rep era t -> Size -> Gen Int
genFromSizeByRep Rep Any t
rep Size
spec
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
forall prop. Testable prop => String -> prop -> Property
counterexample
( String
"at type="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep Any t
rep
forall a. [a] -> [a] -> [a]
++ String
", spec1="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
spec1
forall a. [a] -> [a] -> [a]
++ String
", spec2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
spec2
forall a. [a] -> [a] -> [a]
++ String
", spec1<>spec2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
spec
forall a. [a] -> [a] -> [a]
++ String
", ans="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
ans
)
(Int -> Size -> Bool
runSize Int
ans Size
spec Bool -> Bool -> Bool
&& Int -> Size -> Bool
runSize Int
ans Size
spec1 Bool -> Bool -> Bool
&& Int -> Size -> Bool
runSize Int
ans Size
spec2)
data RelSpec era dom where
RelAny ::
RelSpec era dom
RelNever ::
[String] ->
RelSpec era dom
RelOper ::
Ord d =>
Rep era d ->
Set d ->
Maybe (Set d) ->
Set d ->
RelSpec era d
RelLens :: Ord b => Lens' dom b -> Rep era dom -> Rep era b -> (RelSpec era b) -> RelSpec era dom
relSubset, relSuperset, relDisjoint, relEqual :: Ord t => Rep era t -> Set t -> RelSpec era t
relSubset :: forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era t
r Set t
set = forall d era.
Ord d =>
Rep era d -> Set d -> Maybe (Set d) -> Set d -> RelSpec era d
RelOper Rep era t
r forall a. Set a
Set.empty (forall a. a -> Maybe a
Just Set t
set) forall a. Set a
Set.empty
relSuperset :: forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era t
r Set t
set = forall d era.
Ord d =>
Rep era d -> Set d -> Maybe (Set d) -> Set d -> RelSpec era d
RelOper Rep era t
r Set t
set forall a. Maybe a
Nothing forall a. Set a
Set.empty
relDisjoint :: forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era t
r Set t
set = forall d era.
Ord d =>
Rep era d -> Set d -> Maybe (Set d) -> Set d -> RelSpec era d
RelOper Rep era t
r forall a. Set a
Set.empty forall a. Maybe a
Nothing Set t
set
relEqual :: forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era t
r Set t
set = forall d era.
Ord d =>
Rep era d -> Set d -> Maybe (Set d) -> Set d -> RelSpec era d
RelOper Rep era t
r Set t
set (forall a. a -> Maybe a
Just Set t
set) forall a. Set a
Set.empty
instance Monoid (RelSpec era dom) where
mempty :: RelSpec era dom
mempty = forall era dom. RelSpec era dom
RelAny
instance Semigroup (RelSpec era dom) where
<> :: RelSpec era dom -> RelSpec era dom -> RelSpec era dom
(<>) = forall era dom.
RelSpec era dom -> RelSpec era dom -> RelSpec era dom
mergeRelSpec
instance Show (RelSpec era dom) where
show :: RelSpec era dom -> String
show = forall era dom. RelSpec era dom -> String
showRelSpec
instance LiftT (RelSpec era a) where
liftT :: RelSpec era a -> Typed (RelSpec era a)
liftT (RelNever [String]
xs) = forall a. [String] -> Typed a
failT [String]
xs
liftT RelSpec era a
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure RelSpec era a
x
dropT :: Typed (RelSpec era a) -> RelSpec era a
dropT (Typed (Left [String]
s)) = forall era dom. [String] -> RelSpec era dom
RelNever [String]
s
dropT (Typed (Right RelSpec era a
x)) = RelSpec era a
x
showRelSpec :: RelSpec era dom -> String
showRelSpec :: forall era dom. RelSpec era dom -> String
showRelSpec RelSpec era dom
RelAny = String
"RelAny"
showRelSpec (RelOper Rep era dom
r Set dom
x (Just Set dom
s) Set dom
y) | forall a. Set a -> Bool
Set.null Set dom
y Bool -> Bool -> Bool
&& Set dom
x forall a. Eq a => a -> a -> Bool
== Set dom
s = [String] -> String
sepsP [String
"RelEqual", forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
x]
showRelSpec (RelOper Rep era dom
r Set dom
x (Just Set dom
s) Set dom
y) | forall a. Set a -> Bool
Set.null Set dom
x Bool -> Bool -> Bool
&& forall a. Set a -> Bool
Set.null Set dom
y = [String] -> String
sepsP [String
"RelSubset", forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
s]
showRelSpec (RelOper Rep era dom
r Set dom
x Maybe (Set dom)
Nothing Set dom
y) | forall a. Set a -> Bool
Set.null Set dom
y = [String] -> String
sepsP [String
"RelSuperset", forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
x]
showRelSpec (RelOper Rep era dom
r Set dom
x Maybe (Set dom)
Nothing Set dom
y) | forall a. Set a -> Bool
Set.null Set dom
x = [String] -> String
sepsP [String
"RelDisjoint", forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
y]
showRelSpec (RelOper Rep era dom
r Set dom
x Maybe (Set dom)
Nothing Set dom
y) = [String] -> String
sepsP [String
"RelOper", forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
x, String
"Univ", forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
y]
showRelSpec (RelOper Rep era dom
r Set dom
x (Just Set dom
y) Set dom
z) = [String] -> String
sepsP [String
"RelOper", forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
x, forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
y, forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
z]
showRelSpec (RelLens Lens' dom b
_ Rep era dom
repd Rep era b
repb RelSpec era b
relsp) = [String] -> String
sepsP [String
"RelLens", String
"(Lens' " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era dom
repd forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era b
repb forall a. [a] -> [a] -> [a]
++ String
")", forall a. Show a => a -> String
show RelSpec era b
relsp]
showRelSpec (RelNever [String]
_) = String
"RelNever"
mergeRelSpec :: RelSpec era d -> RelSpec era d -> RelSpec era d
mergeRelSpec :: forall era dom.
RelSpec era dom -> RelSpec era dom -> RelSpec era dom
mergeRelSpec (RelNever [String]
xs) (RelNever [String]
ys) = forall era dom. [String] -> RelSpec era dom
RelNever ([String]
xs forall a. [a] -> [a] -> [a]
++ [String]
ys)
mergeRelSpec d :: RelSpec era d
d@(RelNever [String]
_) RelSpec era d
_ = RelSpec era d
d
mergeRelSpec RelSpec era d
_ d :: RelSpec era d
d@(RelNever [String]
_) = RelSpec era d
d
mergeRelSpec RelSpec era d
RelAny RelSpec era d
x = RelSpec era d
x
mergeRelSpec RelSpec era d
x RelSpec era d
RelAny = RelSpec era d
x
mergeRelSpec RelSpec era d
x y :: RelSpec era d
y@RelLens {} = forall era dom.
RelSpec era dom -> RelSpec era dom -> RelSpec era dom
mergeRelSpec RelSpec era d
y RelSpec era d
x
mergeRelSpec a :: RelSpec era d
a@RelLens {} RelSpec era d
b =
forall era dom. [String] -> RelSpec era dom
RelNever
[ String
"merging a=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era d
a forall a. [a] -> [a] -> [a]
++ String
"\n b=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era d
b
, String
"RelLens is inconsistent with everything, and can't be merged."
]
mergeRelSpec a :: RelSpec era d
a@(RelOper Rep era d
r Set d
must1 Maybe (Set d)
may1 Set d
cant1) b :: RelSpec era d
b@(RelOper Rep era d
_ Set d
must2 Maybe (Set d)
may2 Set d
cant2) =
forall x. LiftT x => Typed x -> x
dropT forall a b. (a -> b) -> a -> b
$
forall a. String -> Typed a -> Typed a
explain (String
"merging a=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era d
a forall a. [a] -> [a] -> [a]
++ String
"\n b=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era d
b) forall a b. (a -> b) -> a -> b
$
forall a. [(Bool, [String])] -> Typed a -> Typed a
requireAll
[
( forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set d
must1 Set d
cant2
,
[ String
"The 'must' set of a("
forall a. [a] -> [a] -> [a]
++ forall t era. Ord t => Rep era t -> Set t -> String
synSet Rep era d
r Set d
must1
forall a. [a] -> [a] -> [a]
++ String
") is not disjoint from the 'cant' set of b("
forall a. [a] -> [a] -> [a]
++ forall t era. Ord t => Rep era t -> Set t -> String
synSet Rep era d
r Set d
cant2
]
)
,
( forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set d
must2 Set d
cant1
,
[ String
"The 'must' set of b("
forall a. [a] -> [a] -> [a]
++ forall t era. Ord t => Rep era t -> Set t -> String
synSet Rep era d
r Set d
must2
forall a. [a] -> [a] -> [a]
++ String
") is not disjoint from the 'cant' set of a("
forall a. [a] -> [a] -> [a]
++ forall t era. Ord t => Rep era t -> Set t -> String
synSet Rep era d
r Set d
cant1
]
)
]
(forall d era.
Ord d =>
Rep era d
-> Set d -> Maybe (Set d) -> Set d -> Typed (RelSpec era d)
relOper Rep era d
r Set d
must Maybe (Set d)
may Set d
cant)
where
must :: Set d
must = forall a. Ord a => Set a -> Set a -> Set a
Set.union Set d
must1 Set d
must2
cant :: Set d
cant = forall a. Ord a => Set a -> Set a -> Set a
Set.union Set d
cant1 Set d
cant2
may :: Maybe (Set d)
may = (forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set d
cant) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Ord a => Maybe (Set a) -> Maybe (Set a) -> Maybe (Set a)
interSectM Maybe (Set d)
may1 Maybe (Set d)
may2
interSectM :: Ord a => Maybe (Set a) -> Maybe (Set a) -> Maybe (Set a)
interSectM :: forall a. Ord a => Maybe (Set a) -> Maybe (Set a) -> Maybe (Set a)
interSectM Maybe (Set a)
Nothing Maybe (Set a)
Nothing = forall a. Maybe a
Nothing
interSectM Maybe (Set a)
Nothing Maybe (Set a)
x = Maybe (Set a)
x
interSectM Maybe (Set a)
x Maybe (Set a)
Nothing = Maybe (Set a)
x
interSectM (Just Set a
x) (Just Set a
y) = forall a. a -> Maybe a
Just (forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set a
x Set a
y)
univSubset :: Ord a => Set a -> Maybe (Set a) -> Bool
univSubset :: forall a. Ord a => Set a -> Maybe (Set a) -> Bool
univSubset Set a
_ Maybe (Set a)
Nothing = Bool
True
univSubset Set a
s1 (Just Set a
s2) = forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set a
s1 Set a
s2
okSize :: RelSpec era d -> Bool
okSize :: forall era d. RelSpec era d -> Bool
okSize (RelOper Rep era d
_ Set d
must (Just Set d
may) Set d
cant) =
forall a. Set a -> Int
Set.size Set d
must forall a. Ord a => a -> a -> Bool
<= forall a. Set a -> Int
Set.size (forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set d
may Set d
cant)
okSize RelSpec era d
_ = Bool
True
sizeForRel :: RelSpec era dom -> Size
sizeForRel :: forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era dom
RelAny = Size
SzAny
sizeForRel (RelNever [String]
_) = Size
SzAny
sizeForRel (RelOper Rep era dom
_ Set dom
must Maybe (Set dom)
Nothing Set dom
_) = Int -> Size
SzLeast (forall a. Set a -> Int
Set.size Set dom
must)
sizeForRel (RelOper Rep era dom
_ Set dom
must (Just Set dom
may) Set dom
_) | forall a. Set a -> Bool
Set.null Set dom
must = Int -> Size
SzMost (forall a. Set a -> Int
Set.size Set dom
may)
sizeForRel (RelOper Rep era dom
_ Set dom
must (Just Set dom
may) Set dom
cant) = Int -> Int -> Size
SzRng (forall a. Set a -> Int
Set.size Set dom
must) (forall a. Set a -> Int
Set.size (forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set dom
may Set dom
cant))
sizeForRel (RelLens Lens' dom b
_ Rep era dom
_ Rep era b
_ RelSpec era b
spec) = forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era b
spec
maybeSynopsis :: Rep e t -> Maybe t -> String
maybeSynopsis :: forall e t. Rep e t -> Maybe t -> String
maybeSynopsis Rep e t
r (Just t
x) = forall e t. Rep e t -> t -> String
format Rep e t
r t
x
maybeSynopsis Rep e t
_ Maybe t
_ = String
""
synSet :: Ord t => Rep era t -> Set t -> String
synSet :: forall t era. Ord t => Rep era t -> Set t -> String
synSet Rep era t
r Set t
s = forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era t
r) Set t
s
relOper :: Ord d => Rep era d -> Set d -> Maybe (Set d) -> Set d -> Typed (RelSpec era d)
relOper :: forall d era.
Ord d =>
Rep era d
-> Set d -> Maybe (Set d) -> Set d -> Typed (RelSpec era d)
relOper Rep era d
r Set d
must Maybe (Set d)
may Set d
cant =
let potential :: RelSpec era d
potential = forall d era.
Ord d =>
Rep era d -> Set d -> Maybe (Set d) -> Set d -> RelSpec era d
RelOper Rep era d
r Set d
must Maybe (Set d)
may Set d
cant
in forall a. String -> Typed a -> Typed a
explain
(String
"Checking RelSpec self consistency\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall d era.
Ord d =>
Rep era d -> Set d -> Maybe (Set d) -> Set d -> RelSpec era d
RelOper Rep era d
r Set d
must Maybe (Set d)
may Set d
cant))
( forall a. [(Bool, [String])] -> Typed a -> Typed a
requireAll
[
( forall a. Ord a => Set a -> Maybe (Set a) -> Bool
univSubset Set d
must Maybe (Set d)
may
,
[ String
"'must' "
forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
format (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era d
r) Set d
must
forall a. [a] -> [a] -> [a]
++ String
" Is not a subset of: 'may' "
forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> Maybe t -> String
maybeSynopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era d
r) Maybe (Set d)
may
]
)
,
( forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set d
must Set d
cant
,
[ String
"'must' "
forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era d
r) Set d
must
forall a. [a] -> [a] -> [a]
++ String
"Is not disjoint from: 'cant' "
forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era d
r) Set d
cant
]
)
,
( forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (\Set d
may' -> forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set d
may' Set d
cant) Maybe (Set d)
may
,
[ String
"'may' "
forall a. [a] -> [a] -> [a]
++ forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"Nothing" (forall e t. Rep e t -> t -> String
synopsis forall a b. (a -> b) -> a -> b
$ forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era d
r) Maybe (Set d)
may
forall a. [a] -> [a] -> [a]
++ String
"Is not disjoint from: 'cant' "
forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era d
r) Set d
cant
]
)
,
( forall era d. RelSpec era d -> Bool
okSize RelSpec era d
potential
, case RelSpec era d
potential of
rel :: RelSpec era d
rel@(RelOper Rep era d
_ Set d
_ (Just Set d
mayJ) Set d
_) ->
[ forall a. Show a => a -> String
show RelSpec era d
potential forall a. [a] -> [a] -> [a]
++ String
" has unrealizable size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era d
rel)
, String
"size must("
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Set a -> Int
Set.size Set d
must)
forall a. [a] -> [a] -> [a]
++ String
") > size(mayJ - cant)("
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Set a -> Int
Set.size (forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set d
mayJ Set d
cant))
forall a. [a] -> [a] -> [a]
++ String
")"
]
RelSpec era d
_ -> []
)
]
(forall (f :: * -> *) a. Applicative f => a -> f a
pure RelSpec era d
potential)
)
runRelSpec :: Ord t => Set t -> RelSpec era t -> Bool
runRelSpec :: forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set t
_ RelSpec era t
RelAny = Bool
True
runRelSpec Set t
_ (RelNever [String]
xs) = forall a. HasCallStack => String -> [String] -> a
errorMess String
"RelNever in call to runRelSpec" [String]
xs
runRelSpec Set t
s (RelOper Rep era t
_ Set t
must Maybe (Set t)
Nothing Set t
cant) = forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set t
must Set t
s Bool -> Bool -> Bool
&& forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set t
s Set t
cant
runRelSpec Set t
s (RelOper Rep era t
_ Set t
must (Just Set t
may) Set t
cant) = forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set t
must Set t
s Bool -> Bool -> Bool
&& forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set t
s Set t
may Bool -> Bool -> Bool
&& forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set t
s Set t
cant
runRelSpec Set t
s (RelLens Lens' t b
lensdb Rep era t
_ Rep era b
_ RelSpec era b
spec) = forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec (forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\t
x -> t
x forall s a. s -> Getting a s a -> a
^. Lens' t b
lensdb) Set t
s) RelSpec era b
spec
genFromRelSpec ::
forall era t. (Era era, Ord t) => [String] -> Gen t -> Int -> RelSpec era t -> Gen (Set t)
genFromRelSpec :: forall era t.
(Era era, Ord t) =>
[String] -> Gen t -> Int -> RelSpec era t -> Gen (Set t)
genFromRelSpec [String]
msgs Gen t
g Int
n RelSpec era t
spec =
let msg :: String
msg = String
"genFromRelSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era t
spec
in case RelSpec era t
spec of
RelNever [String]
xs -> forall a. HasCallStack => String -> [String] -> a
errorMess String
"RelNever in genFromSpecT" ([String]
msgs forall a. [a] -> [a] -> [a]
++ [String]
xs)
RelSpec era t
RelAny -> forall a. Ord a => [String] -> Int -> Gen a -> Gen (Set a)
setSized (String
msg forall a. a -> [a] -> [a]
: [String]
msgs) Int
n Gen t
g
RelOper Rep era t
_ Set t
must (Just Set t
may) Set t
cant | Set t
must forall a. Eq a => a -> a -> Bool
== Set t
may Bool -> Bool -> Bool
&& forall a. Set a -> Bool
Set.null Set t
cant -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Set t
must
RelOper Rep era t
_ Set t
must Maybe (Set t)
Nothing Set t
dis ->
forall a.
Ord a =>
[String] -> Int -> Int -> Gen a -> Set a -> Gen (Set a)
fixSet (String
msg forall a. a -> [a] -> [a]
: [String]
msgs) Int
1000 Int
n (forall a. [String] -> Gen a -> (a -> Bool) -> Gen a
suchThatErr (String
msg forall a. a -> [a] -> [a]
: [String]
msgs) Gen t
g (forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set t
dis)) Set t
must
RelOper Rep era t
_ Set t
must (Just Set t
may) Set t
dis ->
let choices :: Set t
choices = forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set t
may Set t
dis
m :: Int
m = forall a. Set a -> Int
Set.size Set t
choices
in
case forall a. Ord a => a -> a -> Ordering
compare Int
m Int
n of
Ordering
EQ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Set t
choices
Ordering
LT ->
forall a. HasCallStack => String -> [String] -> a
errorMess
( String
"Size inconsistency. We need "
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
forall a. [a] -> [a] -> [a]
++ String
". The most we can get from (may-cant) is "
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
m
)
(String
msg forall a. a -> [a] -> [a]
: [String]
msgs)
Ordering
GT -> forall a. Ord a => [String] -> Set a -> Set a -> Int -> Gen (Set a)
addUntilSize (String
msg forall a. a -> [a] -> [a]
: [String]
msgs) Set t
must Set t
choices Int
n
RelLens Lens' t b
lensDB Rep era t
repD Rep era b
repB RelSpec era b
specB -> do
Set b
setB <- forall era t.
(Era era, Ord t) =>
[String] -> Gen t -> Int -> RelSpec era t -> Gen (Set t)
genFromRelSpec [String]
msgs (forall era b. Rep era b -> Gen b
genRep Rep era b
repB) Int
n RelSpec era b
specB
let accum :: Gen (Set t) -> b -> Gen (Set t)
accum Gen (Set t)
ansG b
b =
do
Set t
ans <- Gen (Set t)
ansG
t
d <- forall era b. Rep era b -> Gen b
genRep Rep era t
repD
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
Set.insert (t
d forall a b. a -> (a -> b) -> b
& Lens' t b
lensDB forall s t a b. ASetter s t a b -> b -> s -> t
.~ b
b) Set t
ans
forall a b. (a -> b -> a) -> a -> Set b -> a
Set.foldl' Gen (Set t) -> b -> Gen (Set t)
accum (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Set a
Set.empty) Set b
setB
genRelSpec :: Ord dom => [String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec :: forall dom era.
Ord dom =>
[String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec [String]
_ Gen dom
_ Rep era dom
r Int
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era dom
r forall a. Set a
Set.empty
genRelSpec [String]
msg Gen dom
genD Rep era dom
r Int
n = do
Int
smaller <- forall a. Random a => (a, a) -> Gen a
choose (Int
1, forall a. Ord a => a -> a -> a
min Int
2 (Int
n forall a. Num a => a -> a -> a
- Int
1))
Int
larger <- forall a. Random a => (a, a) -> Gen a
choose (Int
n forall a. Num a => a -> a -> a
+ Int
5, Int
n forall a. Num a => a -> a -> a
+ Int
7)
let msgs :: [String]
msgs =
([String] -> String
sepsP [String
"genRelSpec ", forall a. Show a => a -> String
show Int
n, forall a. Show a => a -> String
show Rep era dom
r, String
" smaller=", forall a. Show a => a -> String
show Int
smaller, String
", larger=", forall a. Show a => a -> String
show Int
larger]) forall a. a -> [a] -> [a]
: [String]
msg
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
[
( Int
1
, do
Set dom
must <- forall a. Ord a => [String] -> Int -> Gen a -> Gen (Set a)
setSized (String
"must of RelOper Nothing" forall a. a -> [a] -> [a]
: [String]
msgs) Int
smaller Gen dom
genD
Set dom
dis <-
forall t. Ord t => Gen t -> Gen (Set t)
someSet
(forall a. [String] -> Gen a -> (a -> Bool) -> Gen a
suchThatErr ((String
"dis of RelOper Nothing " forall a. [a] -> [a] -> [a]
++ forall t era. Ord t => Rep era t -> Set t -> String
synSet Rep era dom
r Set dom
must) forall a. a -> [a] -> [a]
: [String]
msgs) Gen dom
genD (forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set dom
must))
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall d era.
Ord d =>
Rep era d
-> Set d -> Maybe (Set d) -> Set d -> Typed (RelSpec era d)
relOper Rep era dom
r Set dom
must forall a. Maybe a
Nothing Set dom
dis)
)
,
( Int
2
, do
Set dom
must <- forall a. Ord a => [String] -> Int -> Gen a -> Gen (Set a)
setSized (String
"must of RelOper Just" forall a. a -> [a] -> [a]
: [String]
msgs) Int
smaller Gen dom
genD
Set dom
may <- forall a. Ord a => [String] -> Int -> Gen a -> Set a -> Gen (Set a)
superSetFromSetWithSize (String
"may of RelOper Just" forall a. a -> [a] -> [a]
: [String]
msgs) Int
larger Gen dom
genD Set dom
must
Set dom
dis <-
forall a. Ord a => [String] -> Int -> Gen a -> Gen (Set a)
setSized
(String
"dis of RelOper Some" forall a. a -> [a] -> [a]
: [String]
msgs)
Int
3
( forall a. [String] -> Gen a -> (a -> Bool) -> Gen a
suchThatErr
((String
"dis of RelOper Some must=" forall a. [a] -> [a] -> [a]
++ forall t era. Ord t => Rep era t -> Set t -> String
synSet Rep era dom
r Set dom
must forall a. [a] -> [a] -> [a]
++ String
" may=" forall a. [a] -> [a] -> [a]
++ forall t era. Ord t => Rep era t -> Set t -> String
synSet Rep era dom
r Set dom
may) forall a. a -> [a] -> [a]
: [String]
msgs)
Gen dom
genD
(forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set dom
may)
)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall d era.
Ord d =>
Rep era d
-> Set d -> Maybe (Set d) -> Set d -> Typed (RelSpec era d)
relOper Rep era dom
r Set dom
must (forall a. a -> Maybe a
Just Set dom
may) Set dom
dis)
)
, (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era dom. RelSpec era dom
RelAny)
]
genDisjoint :: Ord a => Set a -> Gen a -> Gen (Set a)
genDisjoint :: forall a. Ord a => Set a -> Gen a -> Gen (Set a)
genDisjoint Set a
set Gen a
gen = Int -> Set a -> Gen (Set a)
help Int
atLeastDelta forall a. Set a
Set.empty
where
help :: Int -> Set a -> Gen (Set a)
help Int
n !Set a
answer | Int
n forall a. Ord a => a -> a -> Bool
< Int
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Set a
answer
help Int
n !Set a
answer = do
a
x <- Gen a
gen
Int -> Set a -> Gen (Set a)
help (Int
n forall a. Num a => a -> a -> a
- Int
1) (if forall a. Ord a => a -> Set a -> Bool
Set.member a
x Set a
set then Set a
answer else forall a. Ord a => a -> Set a -> Set a
Set.insert a
x Set a
answer)
genConsistentRelSpec :: [String] -> Gen dom -> RelSpec era dom -> Gen (RelSpec era dom)
genConsistentRelSpec :: forall dom era.
[String] -> Gen dom -> RelSpec era dom -> Gen (RelSpec era dom)
genConsistentRelSpec [String]
msg Gen dom
g RelSpec era dom
x = case RelSpec era dom
x of
r :: RelSpec era dom
r@(RelLens {}) -> forall a. HasCallStack => String -> a
error (String
"Can't generate a consistent spec for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era dom
r)
RelOper Rep era dom
r Set dom
must Maybe (Set dom)
Nothing Set dom
cant ->
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
[ (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era dom. RelSpec era dom
RelAny)
,
( Int
1
, do
Set dom
cant2 <- forall a. Ord a => Set a -> Gen a -> Gen (Set a)
genDisjoint Set dom
must Gen dom
g
Set dom
must2 <- forall a. Ord a => Set a -> Gen a -> Gen (Set a)
genDisjoint (Set dom
cant forall a. Semigroup a => a -> a -> a
<> Set dom
cant2) Gen dom
g
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall d era.
Ord d =>
Rep era d -> Set d -> Maybe (Set d) -> Set d -> RelSpec era d
RelOper Rep era dom
r Set dom
must2 forall a. Maybe a
Nothing Set dom
cant2
)
,
( Int
1
, do
Set dom
may2 <- (forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set dom
cant) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Ord a => Gen a -> Set a -> Gen (Set a)
superSetFromSet Gen dom
g Set dom
must
Set dom
must2 <- forall a. Ord a => [String] -> Set a -> Gen (Set a)
subsetFromSet ((forall a. Show a => a -> String
show RelSpec era dom
x forall a. [a] -> [a] -> [a]
++ String
" gen may") forall a. a -> [a] -> [a]
: [String]
msgs) Set dom
must
Set dom
cant2 <- forall a. Ord a => Set a -> Gen a -> Gen (Set a)
genDisjoint Set dom
may2 Gen dom
g
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall d era.
Ord d =>
Rep era d -> Set d -> Maybe (Set d) -> Set d -> RelSpec era d
RelOper Rep era dom
r Set dom
must2 (forall a. a -> Maybe a
Just Set dom
may2) Set dom
cant2
)
]
RelOper Rep era dom
r Set dom
must (Just Set dom
may) Set dom
cant ->
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
[ (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era dom. RelSpec era dom
RelAny)
,
( Int
1
, do
Set dom
cant2 <- forall a. Ord a => Set a -> Gen a -> Gen (Set a)
genDisjoint Set dom
may Gen dom
g
Set dom
must2 <- forall a. Ord a => [String] -> Set a -> Gen (Set a)
subsetFromSet ((forall a. Show a => a -> String
show RelSpec era dom
x forall a. [a] -> [a] -> [a]
++ String
" gen must") forall a. a -> [a] -> [a]
: [String]
msgs) Set dom
may
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall d era.
Ord d =>
Rep era d -> Set d -> Maybe (Set d) -> Set d -> RelSpec era d
RelOper Rep era dom
r Set dom
must2 forall a. Maybe a
Nothing Set dom
cant2
)
,
( Int
1
, do
Set dom
may2 <- (forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set dom
cant) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Ord a => Gen a -> Set a -> Gen (Set a)
superSetFromSet Gen dom
g Set dom
must
Set dom
must2 <- forall a. Ord a => [String] -> Set a -> Gen (Set a)
subsetFromSet ((forall a. Show a => a -> String
show RelSpec era dom
x forall a. [a] -> [a] -> [a]
++ String
" gen must") forall a. a -> [a] -> [a]
: [String]
msgs) Set dom
must
Set dom
cant2 <- forall a. Ord a => Set a -> Gen a -> Gen (Set a)
genDisjoint (Set dom
may forall a. Semigroup a => a -> a -> a
<> Set dom
may2) Gen dom
g
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall d era.
Ord d =>
Rep era d -> Set d -> Maybe (Set d) -> Set d -> RelSpec era d
RelOper Rep era dom
r Set dom
must2 (forall a. a -> Maybe a
Just (Set dom
may forall a. Semigroup a => a -> a -> a
<> Set dom
may2)) Set dom
cant2
)
]
RelSpec era dom
RelAny -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era dom. RelSpec era dom
RelAny
RelNever [String]
_ -> forall a. HasCallStack => String -> a
error String
"RelNever in genConsistentRelSpec"
where
msgs :: [String]
msgs = (String
"genConsistentRelSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era dom
x) forall a. a -> [a] -> [a]
: [String]
msg
testConsistentRel :: Gen Property
testConsistentRel :: Gen Property
testConsistentRel = do
Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
3, Int
10)
RelSpec Any Int
s1 <- forall dom era.
Ord dom =>
[String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec [String
"testConsistentRel " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n] (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
10000)) forall era. Rep era Int
IntR Int
n
RelSpec Any Int
s2 <- forall dom era.
[String] -> Gen dom -> RelSpec era dom -> Gen (RelSpec era dom)
genConsistentRelSpec [String
"testConsistentRel " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec Any Int
s1] (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
1000)) RelSpec Any Int
s1
case RelSpec Any Int
s1 forall a. Semigroup a => a -> a -> a
<> RelSpec Any Int
s2 of
RelNever [String]
ms -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines ([String
"genConsistent fails", forall a. Show a => a -> String
show RelSpec Any Int
s1, forall a. Show a => a -> String
show RelSpec Any Int
s2] forall a. [a] -> [a] -> [a]
++ [String]
ms)) Bool
False
RelSpec Any Int
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property Bool
True
testSoundRelSpec :: Gen Property
testSoundRelSpec :: Gen Property
testSoundRelSpec = do
Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
3, Int
10)
RelSpec TT Word64
s1 <- forall dom era.
Ord dom =>
[String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec [String
"from testSoundRelSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n] (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
10000)) forall era. Rep era Word64
Word64R Int
n
Set Word64
ans <- forall era t.
(Era era, Ord t) =>
[String] -> Gen t -> Int -> RelSpec era t -> Gen (Set t)
genFromRelSpec @TT [String
"from testSoundRelSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n] (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
100000)) Int
n RelSpec TT Word64
s1
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample (String
"spec=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Word64
s1 forall a. [a] -> [a] -> [a]
++ String
"\nans=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Set Word64
ans) (forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec TT Word64
s1)
testMergeRelSpec :: Gen Property
testMergeRelSpec :: Gen Property
testMergeRelSpec = do
let msg :: [String]
msg = [String
"testMergeRelSpec"]
Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
0, Int
10)
RelSpec TT Word64
s1 <- forall dom era.
Ord dom =>
[String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec ((String
"genRelSpec") forall a. a -> [a] -> [a]
: [String]
msg) (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
10000)) forall era. Rep era Word64
Word64R Int
n
RelSpec TT Word64
s2 <- forall dom era.
[String] -> Gen dom -> RelSpec era dom -> Gen (RelSpec era dom)
genConsistentRelSpec ((String
"genConsistentRepSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Word64
s1) forall a. a -> [a] -> [a]
: [String]
msg) (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) RelSpec TT Word64
s1
case RelSpec TT Word64
s1 forall a. Semigroup a => a -> a -> a
<> RelSpec TT Word64
s2 of
RelNever [String]
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall prop. Testable prop => prop -> Property
property Bool
True)
RelSpec TT Word64
s4 -> do
let size :: Size
size = forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec TT Word64
s4
Int
m <- Size -> Gen Int
genFromSize Size
size
Set Word64
ans <- forall era t.
(Era era, Ord t) =>
[String] -> Gen t -> Int -> RelSpec era t -> Gen (Set t)
genFromRelSpec @TT [String
"testMergeRelSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Word64
s1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Word64
s2] (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) Int
m RelSpec TT Word64
s4
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
forall prop. Testable prop => String -> prop -> Property
counterexample
( String
"s1="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Word64
s1
forall a. [a] -> [a] -> [a]
++ String
"\ns2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Word64
s2
forall a. [a] -> [a] -> [a]
++ String
"\ns1<>s2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Word64
s4
forall a. [a] -> [a] -> [a]
++ String
"\nans="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Set Word64
ans
forall a. [a] -> [a] -> [a]
++ String
"\nrun s1="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec TT Word64
s1)
forall a. [a] -> [a] -> [a]
++ String
"\nrun s2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec TT Word64
s2)
forall a. [a] -> [a] -> [a]
++ String
"\nrun s4="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec TT Word64
s4)
)
(forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec TT Word64
s4 Bool -> Bool -> Bool
&& forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec TT Word64
s2 Bool -> Bool -> Bool
&& forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec TT Word64
s1)
consistent :: (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent :: forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent a
x a
y = case forall x. Typed x -> Either [String] x
runTyped (forall x. LiftT x => x -> Typed x
liftT (a
x forall a. Semigroup a => a -> a -> a
<> a
y)) of
Left [String]
_ -> forall a. Maybe a
Nothing
Right a
spec -> forall a. a -> Maybe a
Just a
spec
manyMergeRelSpec :: Gen (Int, Int, [String])
manyMergeRelSpec :: Gen (Int, Int, [String])
manyMergeRelSpec = do
Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
3, Int
10)
[RelSpec TT Int]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
60 (forall dom era.
Ord dom =>
[String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec [String
"manyMergeRelSpec xs"] (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) forall era. Rep era Int
IntR Int
n)
[RelSpec TT Int]
ys <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
60 (forall dom era.
Ord dom =>
[String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec [String
"manyMergeRelSpec ys"] (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) forall era. Rep era Int
IntR Int
n)
let ok :: RelSpec era dom -> Bool
ok RelSpec era dom
RelAny = Bool
False
ok RelSpec era dom
_ = Bool
True
check :: (RelSpec TT Int, RelSpec TT Int, RelSpec TT Int)
-> Gen
(RelSpec TT Int, Bool, RelSpec TT Int, Bool, Set Int, Bool,
RelSpec TT Int)
check (RelSpec TT Int
x, RelSpec TT Int
y, RelSpec TT Int
m) = do
let size :: Size
size = forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec TT Int
m
Int
i <- Size -> Gen Int
genFromSize Size
size
let wordsX :: [String]
wordsX =
[ String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec TT Int
m)
, String
"s1<>s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Int
m
, String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec TT Int
x)
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Int
x
, String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec TT Int
y)
, String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Int
y
, String
"GenFromRelSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
]
Set Int
z <- forall era t.
(Era era, Ord t) =>
[String] -> Gen t -> Int -> RelSpec era t -> Gen (Set t)
genFromRelSpec @TT [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) Int
i RelSpec TT Int
m
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RelSpec TT Int
x, forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Int
z RelSpec TT Int
x, RelSpec TT Int
y, forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Int
z RelSpec TT Int
y, Set Int
z, forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Int
z RelSpec TT Int
m, RelSpec TT Int
m)
showAns :: (RelSpec era dom, a, RelSpec era dom, a, a, a, RelSpec era dom)
-> String
showAns (RelSpec era dom
s1, a
run1, RelSpec era dom
s2, a
run2, a
v, a
run3, RelSpec era dom
s3) =
[String] -> String
unlines
[ String
"\ns1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era dom
s1
, String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era dom
s1)
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era dom
s2
, String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era dom
s2)
, String
"s1 <> s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era dom
s3
, String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era dom
s3)
, String
"v = genFromRelSpec (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
v
, String
"runRelSpec v s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run1
, String
"runRelSpec v s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run2
, String
"runRelSpec v (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run3
]
pr :: (RelSpec era dom, Bool, RelSpec era dom, Bool, a, Bool,
RelSpec era dom)
-> Maybe String
pr x :: (RelSpec era dom, Bool, RelSpec era dom, Bool, a, Bool,
RelSpec era dom)
x@(RelSpec era dom
_, Bool
a, RelSpec era dom
_, Bool
b, a
_, Bool
c, RelSpec era dom
_) = if Bool -> Bool
not (Bool
a Bool -> Bool -> Bool
&& Bool
b Bool -> Bool -> Bool
&& Bool
c) then forall a. a -> Maybe a
Just (forall {a} {a} {a} {a} {era} {dom} {era} {dom} {era} {dom}.
(Show a, Show a, Show a, Show a) =>
(RelSpec era dom, a, RelSpec era dom, a, a, a, RelSpec era dom)
-> String
showAns (RelSpec era dom, Bool, RelSpec era dom, Bool, a, Bool,
RelSpec era dom)
x) else forall a. Maybe a
Nothing
let trips :: [(RelSpec TT Int, RelSpec TT Int, RelSpec TT Int)]
trips = [(RelSpec TT Int
x, RelSpec TT Int
y, RelSpec TT Int
m) | RelSpec TT Int
x <- [RelSpec TT Int]
xs, RelSpec TT Int
y <- [RelSpec TT Int]
ys, forall era d. RelSpec era d -> Bool
ok RelSpec TT Int
x Bool -> Bool -> Bool
&& forall era d. RelSpec era d -> Bool
ok RelSpec TT Int
y, Just RelSpec TT Int
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent RelSpec TT Int
x RelSpec TT Int
y]]
[(RelSpec TT Int, Bool, RelSpec TT Int, Bool, Set Int, Bool,
RelSpec TT Int)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (RelSpec TT Int, RelSpec TT Int, RelSpec TT Int)
-> Gen
(RelSpec TT Int, Bool, RelSpec TT Int, Bool, Set Int, Bool,
RelSpec TT Int)
check [(RelSpec TT Int, RelSpec TT Int, RelSpec TT Int)]
trips
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (Int
n, forall (t :: * -> *) a. Foldable t => t a -> Int
length [(RelSpec TT Int, RelSpec TT Int, RelSpec TT Int)]
trips, forall a b. (a -> Maybe b) -> [a] -> [b]
Maybe.mapMaybe forall {a} {era} {dom} {era} {dom} {era} {dom}.
Show a =>
(RelSpec era dom, Bool, RelSpec era dom, Bool, a, Bool,
RelSpec era dom)
-> Maybe String
pr [(RelSpec TT Int, Bool, RelSpec TT Int, Bool, Set Int, Bool,
RelSpec TT Int)]
ts)
reportManyMergeRelSpec :: IO ()
reportManyMergeRelSpec :: IO ()
reportManyMergeRelSpec = do
(Int
n, Int
passed, [String]
bad) <- forall a. Gen a -> IO a
generate Gen (Int, Int, [String])
manyMergeRelSpec
if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
bad
then String -> IO ()
putStrLn (String
"passed " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
passed forall a. [a] -> [a] -> [a]
++ String
" tests. Spec size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n)
else do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn [String]
bad; forall a. HasCallStack => String -> a
error String
"TestFails"
data RngSpec era rng where
RngSum ::
Adds rng =>
rng ->
Size ->
RngSpec era rng
RngProj ::
Adds c =>
c ->
Rep era x ->
Lens' x c ->
Size ->
RngSpec era x
RngElem :: Eq r => Rep era r -> [r] -> RngSpec era r
RngRel :: Ord x => RelSpec era x -> RngSpec era x
RngAny :: RngSpec era rng
RngNever :: [String] -> RngSpec era rng
instance Show (RngSpec era t) where
show :: RngSpec era t -> String
show = forall era t. RngSpec era t -> String
showRngSpec
instance Era era => Monoid (RngSpec era rng) where
mempty :: RngSpec era rng
mempty = forall era rng. RngSpec era rng
RngAny
instance Era era => Semigroup (RngSpec era rng) where
<> :: RngSpec era rng -> RngSpec era rng -> RngSpec era rng
(<>) = forall r era. RngSpec era r -> RngSpec era r -> RngSpec era r
mergeRngSpec
instance LiftT (RngSpec era a) where
liftT :: RngSpec era a -> Typed (RngSpec era a)
liftT (RngNever [String]
xs) = forall a. [String] -> Typed a
failT [String]
xs
liftT RngSpec era a
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure RngSpec era a
x
dropT :: Typed (RngSpec era a) -> RngSpec era a
dropT (Typed (Left [String]
s)) = forall era rng. [String] -> RngSpec era rng
RngNever [String]
s
dropT (Typed (Right RngSpec era a
x)) = RngSpec era a
x
showRngSpec :: RngSpec era t -> String
showRngSpec :: forall era t. RngSpec era t -> String
showRngSpec (RngSum t
small Size
sz) = [String] -> String
sepsP [String
"RngSum", forall a. Show a => a -> String
show t
small, forall a. Show a => a -> String
show Size
sz]
showRngSpec (RngProj c
small Rep era t
xrep Lens' t c
_l Size
sz) = [String] -> String
sepsP [String
"RngProj", forall a. Show a => a -> String
show c
small, forall a. Show a => a -> String
show Rep era t
xrep, forall a. Show a => a -> String
show Size
sz]
showRngSpec (RngElem Rep era t
r [t]
cs) = [String] -> String
sepsP [String
"RngElem", forall a. Show a => a -> String
show Rep era t
r, forall e t. Rep e t -> t -> String
synopsis (forall era c. Rep era c -> Rep era [c]
ListR Rep era t
r) [t]
cs]
showRngSpec (RngRel RelSpec era t
x) = [String] -> String
sepsP [String
"RngRel", forall a. Show a => a -> String
show RelSpec era t
x]
showRngSpec RngSpec era t
RngAny = String
"RngAny"
showRngSpec (RngNever [String]
_) = String
"RngNever"
mergeRngSpec :: forall r era. RngSpec era r -> RngSpec era r -> RngSpec era r
mergeRngSpec :: forall r era. RngSpec era r -> RngSpec era r -> RngSpec era r
mergeRngSpec RngSpec era r
RngAny RngSpec era r
x = RngSpec era r
x
mergeRngSpec RngSpec era r
x RngSpec era r
RngAny = RngSpec era r
x
mergeRngSpec (RngRel RelSpec era r
RelAny) RngSpec era r
x = RngSpec era r
x
mergeRngSpec RngSpec era r
x (RngRel RelSpec era r
RelAny) = RngSpec era r
x
mergeRngSpec RngSpec era r
_ (RngNever [String]
xs) = forall era rng. [String] -> RngSpec era rng
RngNever [String]
xs
mergeRngSpec (RngNever [String]
xs) RngSpec era r
_ = forall era rng. [String] -> RngSpec era rng
RngNever [String]
xs
mergeRngSpec a :: RngSpec era r
a@(RngElem Rep era r
_ [r]
xs) RngSpec era r
b
| forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [r]
xs RngSpec era r
b = RngSpec era r
a
| Bool
otherwise = forall era rng. [String] -> RngSpec era rng
RngNever [String
"The RngSpec's are inconsistent.\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
a forall a. [a] -> [a] -> [a]
++ String
"\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
b]
mergeRngSpec RngSpec era r
a b :: RngSpec era r
b@(RngElem Rep era r
_ [r]
xs)
| forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [r]
xs RngSpec era r
a = RngSpec era r
b
| Bool
otherwise = forall era rng. [String] -> RngSpec era rng
RngNever [String
"The RngSpec's are inconsistent.\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
a forall a. [a] -> [a] -> [a]
++ String
"\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
b]
mergeRngSpec a :: RngSpec era r
a@(RngSum r
small1 Size
sz1) b :: RngSpec era r
b@(RngSum r
small2 Size
sz2) =
case Size
sz1 forall a. Semigroup a => a -> a -> a
<> Size
sz2 of
SzNever [String]
xs -> forall era rng. [String] -> RngSpec era rng
RngNever ([String
"The RngSpec's are inconsistent.\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
a forall a. [a] -> [a] -> [a]
++ String
"\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
b] forall a. [a] -> [a] -> [a]
++ [String]
xs)
Size
sz3 -> forall rng era. Adds rng => rng -> Size -> RngSpec era rng
RngSum (forall x. Adds x => x -> x -> x
smallerOf r
small1 r
small2) Size
sz3
mergeRngSpec a :: RngSpec era r
a@(RngRel RelSpec era r
r1) b :: RngSpec era r
b@(RngRel RelSpec era r
r2) =
case RelSpec era r
r1 forall a. Semigroup a => a -> a -> a
<> RelSpec era r
r2 of
RelNever [String]
xs -> forall era rng. [String] -> RngSpec era rng
RngNever ([String
"The RngSpec's are inconsistent.\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
a forall a. [a] -> [a] -> [a]
++ String
"\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
b] forall a. [a] -> [a] -> [a]
++ [String]
xs)
RelSpec era r
r3 -> forall x era. Ord x => RelSpec era x -> RngSpec era x
RngRel RelSpec era r
r3
mergeRngSpec RngSpec era r
a RngSpec era r
b = forall era rng. [String] -> RngSpec era rng
RngNever [String
"The RngSpec's are inconsistent.\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
a forall a. [a] -> [a] -> [a]
++ String
"\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
b]
sizeForRng :: forall dom era. RngSpec era dom -> Size
sizeForRng :: forall dom era. RngSpec era dom -> Size
sizeForRng (RngRel RelSpec era dom
x) = forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era dom
x
sizeForRng (RngSum dom
small Size
sz) =
if forall x. Adds x => x -> Int
toI dom
small forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Size -> Int
minSize Size
sz forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& (Size -> Int
minSize Size
sz forall a. Integral a => a -> a -> a
`div` forall x. Adds x => x -> Int
toI dom
small) forall a. Ord a => a -> a -> Bool
> Int
0
then Int -> Int -> Size
SzRng Int
1 (Size -> Int
minSize Size
sz forall a. Integral a => a -> a -> a
`div` forall x. Adds x => x -> Int
toI dom
small)
else Int -> Size
SzLeast Int
1
sizeForRng (RngProj c
small Rep era dom
_ Lens' dom c
_l Size
sz) =
if forall x. Adds x => x -> Int
toI c
small forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Size -> Int
minSize Size
sz forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& (Size -> Int
minSize Size
sz forall a. Integral a => a -> a -> a
`div` forall x. Adds x => x -> Int
toI c
small) forall a. Ord a => a -> a -> Bool
> Int
0
then Int -> Int -> Size
SzRng Int
1 (Size -> Int
minSize Size
sz forall a. Integral a => a -> a -> a
`div` forall x. Adds x => x -> Int
toI c
small)
else Int -> Size
SzLeast Int
1
sizeForRng (RngElem Rep era dom
_ [dom]
xs) = Int -> Size
SzExact (forall (t :: * -> *) a. Foldable t => t a -> Int
length [dom]
xs)
sizeForRng RngSpec era dom
RngAny = Size
SzAny
sizeForRng (RngNever [String]
_) = Size
SzAny
genFromRngSpec :: forall era r. Era era => [String] -> Gen r -> Int -> RngSpec era r -> Gen [r]
genFromRngSpec :: forall era r.
Era era =>
[String] -> Gen r -> Int -> RngSpec era r -> Gen [r]
genFromRngSpec [String]
msgs Gen r
genr Int
n RngSpec era r
x = case RngSpec era r
x of
(RngNever [String]
xs) -> forall a. HasCallStack => String -> [String] -> a
errorMess String
"RngNever in genFromRngSpec" ([String]
xs forall a. [a] -> [a] -> [a]
++ (String
msg forall a. a -> [a] -> [a]
: [String]
msgs))
RngSpec era r
RngAny -> forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n Gen r
genr
(RngSum r
small Size
sz) -> do
Int
tot <- Size -> Gen Int
genFromIntRange Size
sz
forall x. Adds x => x -> [String] -> Int -> x -> Gen [x]
partition r
small (String
msg forall a. a -> [a] -> [a]
: [String]
msgs) Int
n (forall x. Adds x => [String] -> Int -> x
fromI (String
msg forall a. a -> [a] -> [a]
: [String]
msgs) Int
tot)
(RngProj c
small Rep era r
xrep Lens' r c
l Size
sz) -> do
Int
tot <- Size -> Gen Int
genFromIntRange Size
sz
[c]
rs <- forall x. Adds x => x -> [String] -> Int -> x -> Gen [x]
partition c
small ((String
"partition " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
tot) forall a. a -> [a] -> [a]
: String
msg forall a. a -> [a] -> [a]
: [String]
msgs) Int
n (forall x. Adds x => [String] -> Int -> x
fromI (String
msg forall a. a -> [a] -> [a]
: [String]
msgs) Int
tot)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\c
r -> do r
ans <- forall era b. Rep era b -> Gen b
genRep Rep era r
xrep; forall (f :: * -> *) a. Applicative f => a -> f a
pure (r
ans forall a b. a -> (a -> b) -> b
& Lens' r c
l forall s t a b. ASetter s t a b -> b -> s -> t
.~ c
r)) [c]
rs
(RngRel RelSpec era r
relspec) -> forall a. Set a -> [a]
Set.toList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era t.
(Era era, Ord t) =>
[String] -> Gen t -> Int -> RelSpec era t -> Gen (Set t)
genFromRelSpec (String
msg forall a. a -> [a] -> [a]
: [String]
msgs) Gen r
genr Int
n RelSpec era r
relspec
(RngElem Rep era r
_ [r]
xs) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [r]
xs
where
msg :: String
msg = String
"genFromRngSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
x
genRngSpec ::
forall w era.
(Ord w, Adds w) =>
Gen w ->
Rep era w ->
SomeLens era w ->
Int ->
Gen (RngSpec era w)
genRngSpec :: forall w era.
(Ord w, Adds w) =>
Gen w -> Rep era w -> SomeLens era w -> Int -> Gen (RngSpec era w)
genRngSpec Gen w
_ Rep era w
repw SomeLens era w
_ Int
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall x era. Ord x => RelSpec era x -> RngSpec era x
RngRel (forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era w
repw forall a. Set a
Set.empty)
genRngSpec Gen w
g Rep era w
repw (SomeLens (Lens' w c
l :: Lens' w c)) Int
n = do
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
[
( Int
3
, do
Int
smallest <- forall x. Adds x => Gen Int
genSmall @w
Size
sz <- Int -> Gen Size
genBigSize (forall a. Ord a => a -> a -> a
max Int
1 (Int
smallest forall a. Num a => a -> a -> a
* Int
n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall rng era. Adds rng => rng -> Size -> RngSpec era rng
RngSum (forall x. Adds x => [String] -> Int -> x
fromI [String
"genRngSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n] Int
smallest) Size
sz)
)
,
( Int
2
, do
Int
smallest <- forall x. Adds x => Gen Int
genSmall @c
Size
sz <- Int -> Gen Size
genBigSize (forall a. Ord a => a -> a -> a
max Int
1 (Int
smallest forall a. Num a => a -> a -> a
* Int
n))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall c era x.
Adds c =>
c -> Rep era x -> Lens' x c -> Size -> RngSpec era x
RngProj (forall x. Adds x => [String] -> Int -> x
fromI [String
"genRngSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n] Int
smallest) Rep era w
repw Lens' w c
l Size
sz)
)
, (Int
4, forall x era. Ord x => RelSpec era x -> RngSpec era x
RngRel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall dom era.
Ord dom =>
[String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec @w [String
"genRngSpec "] Gen w
g Rep era w
repw Int
n)
, (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era rng. RngSpec era rng
RngAny)
, (Int
2, forall r era. Eq r => Rep era r -> [r] -> RngSpec era r
RngElem Rep era w
repw forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n Gen w
g)
]
runRngSpec :: [r] -> RngSpec era r -> Bool
runRngSpec :: forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [r]
_ (RngNever [String]
_) = Bool
False
runRngSpec [r]
_ RngSpec era r
RngAny = Bool
True
runRngSpec [r]
ll (RngElem Rep era r
_ [r]
xs) = [r]
ll forall a. Eq a => a -> a -> Bool
== [r]
xs
runRngSpec [r]
ll (RngSum r
_ Size
sz) = Int -> Size -> Bool
runSize (forall x. Adds x => x -> Int
toI (forall (t :: * -> *) c. (Foldable t, Adds c) => t c -> c
sumAdds [r]
ll)) Size
sz
runRngSpec [r]
ll (RngProj c
_ Rep era r
_ Lens' r c
l Size
sz) = Int -> Size -> Bool
runSize (forall x. Adds x => x -> Int
toI (forall (t :: * -> *) b a.
(Foldable t, Adds b) =>
Lens' a b -> t a -> b
lensAdds Lens' r c
l [r]
ll)) Size
sz
runRngSpec [r]
ll (RngRel RelSpec era r
rspec) = forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec (forall a. Ord a => [a] -> Set a
Set.fromList [r]
ll) RelSpec era r
rspec
genConsistentRngSpec ::
forall era w c.
(Ord w, Adds w) =>
Int ->
Gen w ->
Rep era w ->
Rep era c ->
SomeLens era w ->
Gen (RngSpec era w, RngSpec era w)
genConsistentRngSpec :: forall era w c.
(Ord w, Adds w) =>
Int
-> Gen w
-> Rep era w
-> Rep era c
-> SomeLens era w
-> Gen (RngSpec era w, RngSpec era w)
genConsistentRngSpec Int
n Gen w
g Rep era w
repw Rep era c
repc sl :: SomeLens era w
sl@(SomeLens Lens' w c
l) = do
RngSpec era w
x1 <- forall w era.
(Ord w, Adds w) =>
Gen w -> Rep era w -> SomeLens era w -> Int -> Gen (RngSpec era w)
genRngSpec Gen w
g Rep era w
repw SomeLens era w
sl Int
n
RngSpec era w
x2 <- case RngSpec era w
x1 of
RngSpec era w
RngAny -> forall w era.
(Ord w, Adds w) =>
Gen w -> Rep era w -> SomeLens era w -> Int -> Gen (RngSpec era w)
genRngSpec Gen w
g Rep era w
repw SomeLens era w
sl Int
n
RngRel RelSpec era w
RelAny -> forall w era.
(Ord w, Adds w) =>
Gen w -> Rep era w -> SomeLens era w -> Int -> Gen (RngSpec era w)
genRngSpec Gen w
g Rep era w
repw SomeLens era w
sl Int
n
RngRel RelSpec era w
x -> forall x era. Ord x => RelSpec era x -> RngSpec era x
RngRel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall dom era.
[String] -> Gen dom -> RelSpec era dom -> Gen (RelSpec era dom)
genConsistentRelSpec [String]
msgs Gen w
g RelSpec era w
x
RngSum w
sm Size
sz -> do
Size
sz2 <- forall a. Gen a -> (a -> Bool) -> Gen a
suchThat Gen Size
genSize (forall a. Maybe a -> Bool
Maybe.isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent Size
sz)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall rng era. Adds rng => rng -> Size -> RngSpec era rng
RngSum (forall x. Adds x => x -> x -> x
add w
sm (forall x. Adds x => [String] -> Int -> x
fromI [String]
msgs Int
2)) Size
sz2
RngProj c
_sm Rep era w
_rep Lens' w c
_l Size
_sz -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era rng. RngSpec era rng
RngAny
RngElem Rep era w
_ [w]
xs ->
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
[ (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall rng era. Adds rng => rng -> Size -> RngSpec era rng
RngSum (forall x. Adds x => [String] -> Int -> x
fromI [String]
msgs Int
1) (Int -> Size
SzExact (forall x. Adds x => x -> Int
toI (forall (t :: * -> *) c. (Foldable t, Adds c) => t c -> c
sumAdds [w]
xs))))
, (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall c era x.
Adds c =>
c -> Rep era x -> Lens' x c -> Size -> RngSpec era x
RngProj (forall x. Adds x => [String] -> Int -> x
fromI [String]
msgs Int
1) Rep era w
repw Lens' w c
l (Int -> Size
SzExact (forall x. Adds x => x -> Int
toI (forall (t :: * -> *) b a.
(Foldable t, Adds b) =>
Lens' a b -> t a -> b
lensAdds Lens' w c
l [w]
xs))))
]
RngNever [String]
xs -> forall a. HasCallStack => String -> [String] -> a
errorMess String
"RngNever in genConsistentRngSpec" [String]
xs
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RngSpec era w
x1, RngSpec era w
x2)
where
msgs :: [String]
msgs = [[String] -> String
seps [String
"genConsistentRngSpec", forall a. Show a => a -> String
show Rep era w
repw, forall a. Show a => a -> String
show Rep era c
repc]]
word64CoinL :: Lens' Word64 Coin
word64CoinL :: Lens' Word64 Coin
word64CoinL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (Integer -> Coin
Coin forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral) (\Word64
_w (Coin Integer
n) -> forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n)
testConsistentRng :: Gen Property
testConsistentRng :: Gen Property
testConsistentRng = do
Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
3, Int
10)
(RngSpec TT Word64
s1, RngSpec TT Word64
s2) <- forall era w c.
(Ord w, Adds w) =>
Int
-> Gen w
-> Rep era w
-> Rep era c
-> SomeLens era w
-> Gen (RngSpec era w, RngSpec era w)
genConsistentRngSpec @TestEra Int
n (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) forall era. Rep era Word64
Word64R forall era. Rep era Coin
CoinR (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL)
case RngSpec TT Word64
s1 forall a. Semigroup a => a -> a -> a
<> RngSpec TT Word64
s2 of
RngNever [String]
ms -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines ([String
"genConsistentRng fails", forall a. Show a => a -> String
show RngSpec TT Word64
s1, forall a. Show a => a -> String
show RngSpec TT Word64
s2] forall a. [a] -> [a] -> [a]
++ [String]
ms)) Bool
False
RngSpec TT Word64
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample String
"" Bool
True
testSoundRngSpec :: Gen Property
testSoundRngSpec :: Gen Property
testSoundRngSpec = do
Int
n <- forall a. Random a => (a, a) -> Gen a
choose (Int
2, Int
8)
RngSpec TT Word64
spec <- forall w era.
(Ord w, Adds w) =>
Gen w -> Rep era w -> SomeLens era w -> Int -> Gen (RngSpec era w)
genRngSpec (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Int
n
let msgs :: [String]
msgs = [String
"testSoundRngSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
spec]
[Word64]
list <- forall era r.
Era era =>
[String] -> Gen r -> Int -> RngSpec era r -> Gen [r]
genFromRngSpec @TT [String]
msgs (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) Int
n RngSpec TT Word64
spec
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
forall prop. Testable prop => String -> prop -> Property
counterexample
(String
"spec=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
spec forall a. [a] -> [a] -> [a]
++ String
"\nlist=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Word64]
list)
(forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Word64]
list RngSpec TT Word64
spec)
testMergeRngSpec :: Gen Property
testMergeRngSpec :: Gen Property
testMergeRngSpec = do
(RngSpec TT Word64
s1, RngSpec TT Word64
s2) <- forall era w c.
(Ord w, Adds w) =>
Int
-> Gen w
-> Rep era w
-> Rep era c
-> SomeLens era w
-> Gen (RngSpec era w, RngSpec era w)
genConsistentRngSpec Int
3 (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) forall era. Rep era Word64
Word64R forall era. Rep era Coin
CoinR (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL)
case RngSpec TT Word64
s1 forall a. Semigroup a => a -> a -> a
<> RngSpec TT Word64
s2 of
RngNever [String]
_ ->
forall a. String -> a -> a
Debug.trace (String
"inconsistent RngSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
s1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
s2) (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall prop. Testable prop => String -> prop -> Property
counterexample String
"" Bool
True))
RngSpec TT Word64
s3 -> do
let size :: Size
size = forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec TT Word64
s3
Int
n <- Size -> Gen Int
genFromSize Size
size
let wordsX :: [String]
wordsX =
[ String
"s1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
s1
, String
"s2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
s2
, String
"s3=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
s3
, String
"size=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
size
, String
"n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
, String
"testMergeRngSpec"
]
[Word64]
list <- forall era r.
Era era =>
[String] -> Gen r -> Int -> RngSpec era r -> Gen [r]
genFromRngSpec @TT [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) Int
n RngSpec TT Word64
s3
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
forall prop. Testable prop => String -> prop -> Property
counterexample
( String
"s1="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
s1
forall a. [a] -> [a] -> [a]
++ String
"\n s2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
s2
forall a. [a] -> [a] -> [a]
++ String
"\n s3="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
s3
forall a. [a] -> [a] -> [a]
++ String
"\n size="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
size
forall a. [a] -> [a] -> [a]
++ String
"\n n="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
forall a. [a] -> [a] -> [a]
++ String
"\n list="
forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall era c. Rep era c -> Rep era [c]
ListR forall era. Rep era Word64
Word64R) [Word64]
list
forall a. [a] -> [a] -> [a]
++ String
"\n run1="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Word64]
list RngSpec TT Word64
s1)
forall a. [a] -> [a] -> [a]
++ String
"\n run2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Word64]
list RngSpec TT Word64
s2)
)
(forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Word64]
list RngSpec TT Word64
s1 Bool -> Bool -> Bool
&& forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Word64]
list RngSpec TT Word64
s2)
intDeltaCoinL :: Lens' Int DeltaCoin
intDeltaCoinL :: Lens' Int DeltaCoin
intDeltaCoinL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (Integer -> DeltaCoin
DeltaCoin forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral) (\Int
_i (DeltaCoin Integer
d) -> forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
d)
manyMergeRngSpec :: Gen (Int, Int, [String])
manyMergeRngSpec :: Gen (Int, Int, [String])
manyMergeRngSpec = do
Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
3, Int
10)
[RngSpec TT Int]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
50 (forall w era.
(Ord w, Adds w) =>
Gen w -> Rep era w -> SomeLens era w -> Int -> Gen (RngSpec era w)
genRngSpec (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) forall era. Rep era Int
IntR (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Int DeltaCoin
intDeltaCoinL) Int
n)
[RngSpec TT Int]
ys <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
50 (forall w era.
(Ord w, Adds w) =>
Gen w -> Rep era w -> SomeLens era w -> Int -> Gen (RngSpec era w)
genRngSpec (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) forall era. Rep era Int
IntR (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Int DeltaCoin
intDeltaCoinL) Int
n)
let check :: (RngSpec TT Int, RngSpec TT Int, RngSpec TT Int)
-> Gen
(RngSpec TT Int, Bool, RngSpec TT Int, Bool, [Int], Bool,
RngSpec TT Int)
check (RngSpec TT Int
x, RngSpec TT Int
y, RngSpec TT Int
m) = do
let size :: Size
size = forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec TT Int
m
Int
i <- Size -> Gen Int
genFromSize Size
size
let wordsX :: [String]
wordsX =
[ String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec TT Int
m)
, String
"s1<>s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Int
m
, String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec TT Int
x)
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Int
x
, String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec TT Int
y)
, String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Int
y
, String
"GenFromRngSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
]
[Int]
z <- forall era r.
Era era =>
[String] -> Gen r -> Int -> RngSpec era r -> Gen [r]
genFromRngSpec @TT [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) Int
i RngSpec TT Int
m
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RngSpec TT Int
x, forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Int]
z RngSpec TT Int
x, RngSpec TT Int
y, forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Int]
z RngSpec TT Int
y, [Int]
z, forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Int]
z RngSpec TT Int
m, RngSpec TT Int
m)
showAns :: (RngSpec era dom, a, RngSpec era dom, a, a, a, RngSpec era dom)
-> String
showAns (RngSpec era dom
s1, a
run1, RngSpec era dom
s2, a
run2, a
v, a
run3, RngSpec era dom
s3) =
[String] -> String
unlines
[ String
"\ns1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era dom
s1
, String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec era dom
s1)
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era dom
s2
, String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec era dom
s2)
, String
"s1 <> s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era dom
s3
, String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec era dom
s3)
, String
"v = genFromRngSpec (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
v
, String
"runRngSpec v s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run1
, String
"runRngSpec v s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run2
, String
"runRngSpec v (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run3
]
pr :: (RngSpec era dom, Bool, RngSpec era dom, Bool, a, Bool,
RngSpec era dom)
-> Maybe String
pr x :: (RngSpec era dom, Bool, RngSpec era dom, Bool, a, Bool,
RngSpec era dom)
x@(RngSpec era dom
_, Bool
a, RngSpec era dom
_, Bool
b, a
_, Bool
c, RngSpec era dom
_) = if Bool -> Bool
not (Bool
a Bool -> Bool -> Bool
&& Bool
b Bool -> Bool -> Bool
&& Bool
c) then forall a. a -> Maybe a
Just (forall {a} {a} {a} {a} {era} {dom} {era} {dom} {era} {dom}.
(Show a, Show a, Show a, Show a) =>
(RngSpec era dom, a, RngSpec era dom, a, a, a, RngSpec era dom)
-> String
showAns (RngSpec era dom, Bool, RngSpec era dom, Bool, a, Bool,
RngSpec era dom)
x) else forall a. Maybe a
Nothing
let trips :: [(RngSpec TT Int, RngSpec TT Int, RngSpec TT Int)]
trips = [(RngSpec TT Int
x, RngSpec TT Int
y, RngSpec TT Int
m) | RngSpec TT Int
x <- [RngSpec TT Int]
xs, RngSpec TT Int
y <- [RngSpec TT Int]
ys, Just RngSpec TT Int
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent RngSpec TT Int
x RngSpec TT Int
y]]
[(RngSpec TT Int, Bool, RngSpec TT Int, Bool, [Int], Bool,
RngSpec TT Int)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (RngSpec TT Int, RngSpec TT Int, RngSpec TT Int)
-> Gen
(RngSpec TT Int, Bool, RngSpec TT Int, Bool, [Int], Bool,
RngSpec TT Int)
check [(RngSpec TT Int, RngSpec TT Int, RngSpec TT Int)]
trips
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (Int
n, forall (t :: * -> *) a. Foldable t => t a -> Int
length [(RngSpec TT Int, RngSpec TT Int, RngSpec TT Int)]
trips, forall a b. (a -> Maybe b) -> [a] -> [b]
Maybe.mapMaybe forall {a} {era} {dom} {era} {dom} {era} {dom}.
Show a =>
(RngSpec era dom, Bool, RngSpec era dom, Bool, a, Bool,
RngSpec era dom)
-> Maybe String
pr [(RngSpec TT Int, Bool, RngSpec TT Int, Bool, [Int], Bool,
RngSpec TT Int)]
ts)
reportManyMergeRngSpec :: IO ()
reportManyMergeRngSpec :: IO ()
reportManyMergeRngSpec = do
(Int
n, Int
passed, [String]
bad) <- forall a. Gen a -> IO a
generate Gen (Int, Int, [String])
manyMergeRngSpec
if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
bad
then String -> IO ()
putStrLn (String
"passed " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
passed forall a. [a] -> [a] -> [a]
++ String
" tests. Spec size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n)
else do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn [String]
bad; forall a. HasCallStack => String -> a
error String
"TestFails"
data MapSpec era dom rng where
MapSpec ::
Size ->
RelSpec era dom ->
PairSpec era dom rng ->
RngSpec era rng ->
MapSpec era dom rng
MapNever :: [String] -> MapSpec era dom rng
instance Ord d => Show (MapSpec w d r) where
show :: MapSpec w d r -> String
show = forall era dom rng. MapSpec era dom rng -> String
showMapSpec
instance (Ord dom, Era era) => Semigroup (MapSpec era dom rng) where
<> :: MapSpec era dom rng -> MapSpec era dom rng -> MapSpec era dom rng
(<>) = forall dom era rng.
Ord dom =>
MapSpec era dom rng -> MapSpec era dom rng -> MapSpec era dom rng
mergeMapSpec
instance (Ord dom, Era era) => Monoid (MapSpec era dom rng) where
mempty :: MapSpec era dom rng
mempty = forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
SzAny forall era dom. RelSpec era dom
RelAny forall era a b. PairSpec era a b
PairAny forall era rng. RngSpec era rng
RngAny
instance LiftT (MapSpec era a b) where
liftT :: MapSpec era a b -> Typed (MapSpec era a b)
liftT (MapNever [String]
xs) = forall a. [String] -> Typed a
failT [String]
xs
liftT MapSpec era a b
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure MapSpec era a b
x
dropT :: Typed (MapSpec era a b) -> MapSpec era a b
dropT (Typed (Left [String]
s)) = forall era dom rng. [String] -> MapSpec era dom rng
MapNever [String]
s
dropT (Typed (Right MapSpec era a b
x)) = MapSpec era a b
x
showMapSpec :: MapSpec era dom rng -> String
showMapSpec :: forall era dom rng. MapSpec era dom rng -> String
showMapSpec (MapSpec Size
w RelSpec era dom
d PairSpec era dom rng
p RngSpec era rng
r) =
String
"("
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines
[ String
"MapSpec"
, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
w
, String
" "
forall a. [a] -> [a] -> [a]
++ String
" "
forall a. [a] -> [a] -> [a]
++ forall era dom. RelSpec era dom -> String
showRelSpec RelSpec era dom
d
, String
" " forall a. [a] -> [a] -> [a]
++ forall era dom rng. PairSpec era dom rng -> String
showPairSpec PairSpec era dom rng
p
, String
" " forall a. [a] -> [a] -> [a]
++ forall era t. RngSpec era t -> String
showRngSpec RngSpec era rng
r
]
forall a. [a] -> [a] -> [a]
++ String
")"
showMapSpec (MapNever [String]
_) = String
"MapNever"
mergeMapSpec :: Ord dom => MapSpec era dom rng -> MapSpec era dom rng -> MapSpec era dom rng
mergeMapSpec :: forall dom era rng.
Ord dom =>
MapSpec era dom rng -> MapSpec era dom rng -> MapSpec era dom rng
mergeMapSpec MapSpec era dom rng
spec1 MapSpec era dom rng
spec2 = case (MapSpec era dom rng
spec1, MapSpec era dom rng
spec2) of
(MapNever [String]
s, MapNever [String]
t) -> forall era dom rng. [String] -> MapSpec era dom rng
MapNever ([String]
s forall a. [a] -> [a] -> [a]
++ [String]
t)
(MapNever [String]
_, MapSpec era dom rng
y) -> MapSpec era dom rng
y
(MapSpec era dom rng
x, MapNever [String]
_) -> MapSpec era dom rng
x
(MapSpec Size
SzAny RelSpec era dom
RelAny PairSpec era dom rng
PairAny RngSpec era rng
RngAny, MapSpec era dom rng
x) -> MapSpec era dom rng
x
(MapSpec era dom rng
x, MapSpec Size
SzAny RelSpec era dom
RelAny PairSpec era dom rng
PairAny RngSpec era rng
RngAny) -> MapSpec era dom rng
x
(MapSpec Size
s1 RelSpec era dom
d1 PairSpec era dom rng
p1 RngSpec era rng
r1, MapSpec Size
s2 RelSpec era dom
d2 PairSpec era dom rng
p2 RngSpec era rng
r2) -> case forall r era. RngSpec era r -> RngSpec era r -> RngSpec era r
mergeRngSpec RngSpec era rng
r1 RngSpec era rng
r2 of
RngNever [String]
msgs -> forall era dom rng. [String] -> MapSpec era dom rng
MapNever ([String
"The MapSpec's are inconsistent.", String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era dom rng
spec1, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era dom rng
spec2] forall a. [a] -> [a] -> [a]
++ [String]
msgs)
RngSpec era rng
r -> case forall era dom.
RelSpec era dom -> RelSpec era dom -> RelSpec era dom
mergeRelSpec RelSpec era dom
d1 RelSpec era dom
d2 of
RelNever [String]
msgs -> forall era dom rng. [String] -> MapSpec era dom rng
MapNever ([String
"The MapSpec's are inconsistent.", String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era dom rng
spec1, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era dom rng
spec2] forall a. [a] -> [a] -> [a]
++ [String]
msgs)
RelSpec era dom
d -> case forall era a b.
PairSpec era a b -> PairSpec era a b -> PairSpec era a b
mergePairSpec PairSpec era dom rng
p1 PairSpec era dom rng
p2 of
PairNever [String]
msgs -> forall era dom rng. [String] -> MapSpec era dom rng
MapNever ([String
"The MapSpec's are inconsistent.", String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era dom rng
spec1, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era dom rng
spec2] forall a. [a] -> [a] -> [a]
++ [String]
msgs)
PairSpec era dom rng
p ->
forall x. LiftT x => Typed x -> x
dropT
(forall a. String -> Typed a -> Typed a
explain (String
"While merging\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era dom rng
spec1 forall a. [a] -> [a] -> [a]
++ String
"\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era dom rng
spec2) (forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec (Size
s1 forall a. Semigroup a => a -> a -> a
<> Size
s2) RelSpec era dom
d PairSpec era dom rng
p RngSpec era rng
r))
mapSpec ::
Ord d => Size -> RelSpec era d -> PairSpec era d r -> RngSpec era r -> Typed (MapSpec era d r)
mapSpec :: forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
sz1 RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng =
let sz2 :: Size
sz2 = forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era d
rel
sz3 :: Size
sz3 = forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec era r
rng
sz4 :: Size
sz4 = forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec era d r
pair
in case Size
sz1 forall a. Semigroup a => a -> a -> a
<> Size
sz2 forall a. Semigroup a => a -> a -> a
<> Size
sz3 forall a. Semigroup a => a -> a -> a
<> Size
sz4 of
SzNever [String]
xs ->
forall a. [String] -> Typed a
failT
( [ String
"Creating " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
sz1 RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng) forall a. [a] -> [a] -> [a]
++ String
" fails."
, String
"It has size inconsistencies."
, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era d
rel forall a. [a] -> [a] -> [a]
++ String
" has size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
sz2
, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era d r
pair forall a. [a] -> [a] -> [a]
++ String
" has size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
sz4
, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
rng forall a. [a] -> [a] -> [a]
++ String
" has size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
sz3
]
forall a. [a] -> [a] -> [a]
++ [String]
xs
)
Size
size ->
case (RelSpec era d
rel, PairSpec era d r
pair, RngSpec era r
rng) of
(RelSpec era d
_, PairSpec era d r
PairAny, RngSpec era r
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
size RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng)
((RelOper Rep era d
_ Set d
mustd Maybe (Set d)
_ Set d
_), PairSpec Rep era d
d Rep era r
r PairSide
VarOnRight Map d r
m, (RngRel (RelOper Rep era r
_ Set r
mustr Maybe (Set r)
_ Set r
_))) ->
forall a. String -> Typed a -> Typed a
explain
(String
"Creating " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
sz1 RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng) forall a. [a] -> [a] -> [a]
++ String
" fails.")
( forall a. [(Bool, [String])] -> Typed a -> Typed a
requireAll
[
( (forall k a. Map k a -> Set k
Map.keysSet Map d r
m forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set d
mustd)
,
[ String
"sizes " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Size
sz1, Size
sz2, Size
sz3, Size
sz4)
, String
"It has PairSpec inconsistencies. The domain of"
, String
" " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era b.
Ord c =>
Rep era c -> Rep era b -> Rep era (Map c b)
MapR Rep era d
d Rep era r
r) Map d r
m forall a. [a] -> [a] -> [a]
++ String
" is not a subset of the of the mustSet"
, String
" " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era d
d) Set d
mustd
, String
" TEST " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall k a. Map k a -> Set k
Map.keysSet Map d r
m forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set d
mustd)
]
)
,
( (forall a. Ord a => [a] -> Set a
Set.fromList (forall k a. Map k a -> [a]
Map.elems Map d r
m) forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set r
mustr)
,
[ String
"It has PairSpec inconsistencies. The range of"
, String
" " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era b.
Ord c =>
Rep era c -> Rep era b -> Rep era (Map c b)
MapR Rep era d
d Rep era r
r) Map d r
m forall a. [a] -> [a] -> [a]
++ String
" is not a subset of the of the mustSet"
, String
" " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era r
r) Set r
mustr
, String
" TEST " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall k a. Map k a -> Set k
Map.keysSet Map d r
m forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set d
mustd)
]
)
]
(forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
size RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng))
)
((RelOper Rep era d
_ Set d
mustd Maybe (Set d)
_ Set d
_), PairSpec Rep era d
d Rep era r
r PairSide
VarOnLeft Map d r
m, (RngRel (RelOper Rep era r
_ Set r
mustr Maybe (Set r)
_ Set r
_))) ->
forall a. String -> Typed a -> Typed a
explain
(String
"Creating " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
sz1 RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng) forall a. [a] -> [a] -> [a]
++ String
" fails.")
( forall a. [(Bool, [String])] -> Typed a -> Typed a
requireAll
[
( (Set d
mustd forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` forall k a. Map k a -> Set k
Map.keysSet Map d r
m)
,
[ String
"sizes " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Size
sz1, Size
sz2, Size
sz3, Size
sz4)
, String
"It has PairSpec inconsistencies. The domain of"
, String
" " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era b.
Ord c =>
Rep era c -> Rep era b -> Rep era (Map c b)
MapR Rep era d
d Rep era r
r) Map d r
m forall a. [a] -> [a] -> [a]
++ String
" is not a subset of the of the mustSet"
, String
" " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era d
d) Set d
mustd
, String
" TEST " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall k a. Map k a -> Set k
Map.keysSet Map d r
m forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set d
mustd)
]
)
,
( (Set r
mustr forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` forall a. Ord a => [a] -> Set a
Set.fromList (forall k a. Map k a -> [a]
Map.elems Map d r
m))
,
[ String
"It has PairSpec inconsistencies. The range of"
, String
" " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era b.
Ord c =>
Rep era c -> Rep era b -> Rep era (Map c b)
MapR Rep era d
d Rep era r
r) Map d r
m forall a. [a] -> [a] -> [a]
++ String
" is not a subset of the of the mustSet"
, String
" " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era r
r) Set r
mustr
, String
" TEST " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall k a. Map k a -> Set k
Map.keysSet Map d r
m forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set d
mustd)
]
)
]
(forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
size RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng))
)
(RelSpec era d
_, PairSpec Rep era d
_d Rep era r
_r PairSide
_side Map d r
_m, RngSpec era r
_) ->
forall a. [String] -> Typed a
failT
[ String
"Creating " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
sz1 RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng) forall a. [a] -> [a] -> [a]
++ String
" fails."
, String
"This spec has a non-PairAny PairSpec"
, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era d r
pair
, String
"so to be consistent it must have both a RelOper RelSpec, and a RngRel RelSpec."
, String
"But it does not:"
, String
" RelSpec = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era d
rel
, String
" RngSpec = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
rng
]
(RelSpec era d
_, PairSpec era d r
p, RngSpec era r
_) | forall era d r. PairSpec era d r -> Bool
anyPairSpec PairSpec era d r
p -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
size RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng)
(RelSpec era d
_, PairNever [String]
msgs, RngSpec era r
_) ->
forall a. [String] -> Typed a
failT
((String
"Creating " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
sz1 RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng) forall a. [a] -> [a] -> [a]
++ String
" fails.") forall a. a -> [a] -> [a]
: [String]
msgs)
runMapSpec :: (Ord d, Eq r) => Map d r -> MapSpec era d r -> Bool
runMapSpec :: forall d r era. (Ord d, Eq r) => Map d r -> MapSpec era d r -> Bool
runMapSpec Map d r
_ (MapNever [String]
xs) = forall a. HasCallStack => String -> [String] -> a
errorMess String
"MapNever in runMapSpec" [String]
xs
runMapSpec Map d r
_ (MapSpec Size
SzAny RelSpec era d
RelAny PairSpec era d r
PairAny RngSpec era r
RngAny) = Bool
True
runMapSpec Map d r
m (MapSpec Size
sz RelSpec era d
dom PairSpec era d r
pair RngSpec era r
rng) =
Int -> Size -> Bool
runSize (forall k a. Map k a -> Int
Map.size Map d r
m) Size
sz
Bool -> Bool -> Bool
&& forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec (forall k a. Map k a -> Set k
Map.keysSet Map d r
m) RelSpec era d
dom
Bool -> Bool -> Bool
&& forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map d r
m PairSpec era d r
pair
Bool -> Bool -> Bool
&& forall r era. [r] -> RngSpec era r -> Bool
runRngSpec (forall k a. Map k a -> [a]
Map.elems Map d r
m) RngSpec era r
rng
sizeForMapSpec :: MapSpec era d r -> Size
sizeForMapSpec :: forall era d r. MapSpec era d r -> Size
sizeForMapSpec (MapSpec Size
sz RelSpec era d
_ PairSpec era d r
_ RngSpec era r
_) = Size
sz
sizeForMapSpec (MapNever [String]
_) = Size
SzAny
genMapSpec ::
forall era dom w.
(Ord dom, Era era, Ord w, Adds w) =>
Gen dom ->
Rep era dom ->
Rep era w ->
SomeLens era w ->
Int ->
Gen (MapSpec era dom w)
genMapSpec :: forall era dom w.
(Ord dom, Era era, Ord w, Adds w) =>
Gen dom
-> Rep era dom
-> Rep era w
-> SomeLens era w
-> Int
-> Gen (MapSpec era dom w)
genMapSpec Gen dom
genD Rep era dom
repd Rep era w
repw SomeLens era w
l Int
n = forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty), (Int
6, Gen (MapSpec era dom w)
genmapspec)]
where
genmapspec :: Gen (MapSpec era dom w)
genmapspec = do
RelSpec era dom
relspec <- forall dom era.
Ord dom =>
[String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec [String
"genMapSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era dom
repd] Gen dom
genD Rep era dom
repd Int
n
RngSpec era w
rngspec <- forall w era.
(Ord w, Adds w) =>
Gen w -> Rep era w -> SomeLens era w -> Int -> Gen (RngSpec era w)
genRngSpec (forall era b. Rep era b -> Gen b
genRep @era Rep era w
repw) Rep era w
repw SomeLens era w
l Int
n
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec (Int -> Size
SzExact Int
n) RelSpec era dom
relspec forall era a b. PairSpec era a b
PairAny RngSpec era w
rngspec)
genFromMapSpec ::
forall era w dom.
(Era era, Ord dom) =>
String ->
[String] ->
Gen dom ->
Gen w ->
MapSpec era dom w ->
Gen (Map dom w)
genFromMapSpec :: forall era w dom.
(Era era, Ord dom) =>
String
-> [String]
-> Gen dom
-> Gen w
-> MapSpec era dom w
-> Gen (Map dom w)
genFromMapSpec String
nm [String]
msgs Gen dom
_ Gen w
_ (MapSpec Size
_size RelSpec era dom
_ (PairNever [String]
xs) RngSpec era w
_) =
forall a. HasCallStack => String -> [String] -> a
errorMess (String
"genFromMapSpec " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
" (PairNever _) fails") ([String]
msgs forall a. [a] -> [a] -> [a]
++ [String]
xs)
genFromMapSpec String
nm [String]
_ Gen dom
_ Gen w
_ (MapNever [String]
xs) =
forall a. HasCallStack => String -> [String] -> a
errorMess (String
"genFromMapSpec " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
" (MapNever _) fails") [String]
xs
genFromMapSpec String
nm [String]
msgs Gen dom
genD Gen w
genR ms :: MapSpec era dom w
ms@(MapSpec Size
size RelSpec era dom
rel PairSpec era dom w
PairAny RngSpec era w
rng) = do
Int
n <- Size -> Gen Int
genFromSize Size
size
Set dom
dom <-
forall era t.
(Era era, Ord t) =>
[String] -> Gen t -> Int -> RelSpec era t -> Gen (Set t)
genFromRelSpec
((String
"GenFromMapSpec " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
"\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era dom w
ms) forall a. a -> [a] -> [a]
: [String]
msgs)
Gen dom
genD
Int
n
RelSpec era dom
rel
[w]
rangelist <-
forall era r.
Era era =>
[String] -> Gen r -> Int -> RngSpec era r -> Gen [r]
genFromRngSpec
((String
"genFromMapSpec " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
"\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era dom w
ms) forall a. a -> [a] -> [a]
: [String]
msgs)
Gen w
genR
Int
n
RngSpec era w
rng
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Set a -> [a]
Set.toList Set dom
dom) [w]
rangelist))
genFromMapSpec String
nm [String]
msgs Gen dom
genD Gen w
genR ms :: MapSpec era dom w
ms@(MapSpec Size
size RelSpec era dom
rel (PairSpec Rep era dom
dr Rep era w
rr PairSide
varside Map dom w
m) RngSpec era w
rng) = do
Int
n <- Size -> Gen Int
genFromSize Size
size
Set dom
dom <-
forall era t.
(Era era, Ord t) =>
[String] -> Gen t -> Int -> RelSpec era t -> Gen (Set t)
genFromRelSpec
((String
"GenFromMapSpec " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
"\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era dom w
ms) forall a. a -> [a] -> [a]
: [String]
msgs)
Gen dom
genD
Int
n
RelSpec era dom
rel
[w]
rangelist <-
forall era r.
Era era =>
[String] -> Gen r -> Int -> RngSpec era r -> Gen [r]
genFromRngSpec
((String
"genFromMapSpec " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
"\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era dom w