{-# 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)
import Test.Cardano.Ledger.Shelley.Serialisation.EraIndepGenerators ()
import Test.Tasty
import Test.Tasty.QuickCheck hiding (total)
data SomeLens era t where
SomeLens :: Adds c => (Lens' t c) -> SomeLens era t
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 a era. Ord a => Rep era a -> Rep era (Set a)
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 a era. Ord a => Rep era a -> Rep era (Set a)
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 a era. Ord a => Rep era a -> Rep era (Set a)
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 a era. Ord a => Rep era a -> Rep era (Set a)
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 a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era dom
r) Set dom
x, String
"Univ", forall e t. Rep e t -> t -> String
synopsis (forall a era. Ord a => Rep era a -> Rep era (Set a)
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 a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era dom
r) Set dom
x, forall e t. Rep e t -> t -> String
synopsis (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era dom
r) Set dom
y, forall e t. Rep e t -> t -> String
synopsis (forall a era. Ord a => Rep era a -> Rep era (Set a)
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 a era. Ord a => Rep era a -> Rep era (Set a)
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 a era. Ord a => Rep era a -> Rep era (Set a)
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 a era. Ord a => Rep era a -> Rep era (Set a)
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 a era. Ord a => Rep era a -> Rep era (Set a)
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 a era. Ord a => Rep era a -> Rep era (Set a)
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 a era. Ord a => Rep era a -> Rep era (Set a)
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 a era. Ord a => Rep era a -> Rep era (Set a)
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 BabbageEra 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 @BabbageEra [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 BabbageEra 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 BabbageEra 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 BabbageEra 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 BabbageEra 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 BabbageEra 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 BabbageEra Word64
s1) forall a. a -> [a] -> [a]
: [String]
msg) (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) RelSpec BabbageEra Word64
s1
case RelSpec BabbageEra Word64
s1 forall a. Semigroup a => a -> a -> a
<> RelSpec BabbageEra Word64
s2 of
RelNever [String]
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall prop. Testable prop => prop -> Property
property Bool
True)
RelSpec BabbageEra Word64
s4 -> do
let size :: Size
size = forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec BabbageEra 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 @BabbageEra
[String
"testMergeRelSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec BabbageEra Word64
s1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec BabbageEra Word64
s2]
(forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000))
Int
m
RelSpec BabbageEra 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 BabbageEra Word64
s1
forall a. [a] -> [a] -> [a]
++ String
"\ns2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec BabbageEra Word64
s2
forall a. [a] -> [a] -> [a]
++ String
"\ns1<>s2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec BabbageEra 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 BabbageEra 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 BabbageEra 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 BabbageEra Word64
s4)
)
(forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec BabbageEra Word64
s4 Bool -> Bool -> Bool
&& forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec BabbageEra Word64
s2 Bool -> Bool -> Bool
&& forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec BabbageEra 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 BabbageEra 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 BabbageEra 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 BabbageEra Int, RelSpec BabbageEra Int,
RelSpec BabbageEra Int)
-> Gen
(RelSpec BabbageEra Int, Bool, RelSpec BabbageEra Int, Bool,
Set Int, Bool, RelSpec BabbageEra Int)
check (RelSpec BabbageEra Int
x, RelSpec BabbageEra Int
y, RelSpec BabbageEra Int
m) = do
let size :: Size
size = forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec BabbageEra 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 BabbageEra Int
m)
, String
"s1<>s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec BabbageEra 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 BabbageEra Int
x)
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec BabbageEra 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 BabbageEra Int
y)
, String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec BabbageEra 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 @BabbageEra [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) Int
i RelSpec BabbageEra Int
m
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RelSpec BabbageEra Int
x, forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Int
z RelSpec BabbageEra Int
x, RelSpec BabbageEra Int
y, forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Int
z RelSpec BabbageEra Int
y, Set Int
z, forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Int
z RelSpec BabbageEra Int
m, RelSpec BabbageEra 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 BabbageEra Int, RelSpec BabbageEra Int,
RelSpec BabbageEra Int)]
trips = [(RelSpec BabbageEra Int
x, RelSpec BabbageEra Int
y, RelSpec BabbageEra Int
m) | RelSpec BabbageEra Int
x <- [RelSpec BabbageEra Int]
xs, RelSpec BabbageEra Int
y <- [RelSpec BabbageEra Int]
ys, forall era d. RelSpec era d -> Bool
ok RelSpec BabbageEra Int
x Bool -> Bool -> Bool
&& forall era d. RelSpec era d -> Bool
ok RelSpec BabbageEra Int
y, Just RelSpec BabbageEra Int
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent RelSpec BabbageEra Int
x RelSpec BabbageEra Int
y]]
[(RelSpec BabbageEra Int, Bool, RelSpec BabbageEra Int, Bool,
Set Int, Bool, RelSpec BabbageEra Int)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (RelSpec BabbageEra Int, RelSpec BabbageEra Int,
RelSpec BabbageEra Int)
-> Gen
(RelSpec BabbageEra Int, Bool, RelSpec BabbageEra Int, Bool,
Set Int, Bool, RelSpec BabbageEra Int)
check [(RelSpec BabbageEra Int, RelSpec BabbageEra Int,
RelSpec BabbageEra 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 BabbageEra Int, RelSpec BabbageEra Int,
RelSpec BabbageEra 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 BabbageEra Int, Bool, RelSpec BabbageEra Int, Bool,
Set Int, Bool, RelSpec BabbageEra 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 a. Rep era a -> Rep era [a]
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 BabbageEra Word64
s1, RngSpec BabbageEra 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 @BabbageEra 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 BabbageEra Word64
s1 forall a. Semigroup a => a -> a -> a
<> RngSpec BabbageEra 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 BabbageEra Word64
s1, forall a. Show a => a -> String
show RngSpec BabbageEra Word64
s2] forall a. [a] -> [a] -> [a]
++ [String]
ms)) Bool
False
RngSpec BabbageEra 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 BabbageEra 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 BabbageEra Word64
spec]
[Word64]
list <- forall era r.
Era era =>
[String] -> Gen r -> Int -> RngSpec era r -> Gen [r]
genFromRngSpec @BabbageEra [String]
msgs (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) Int
n RngSpec BabbageEra 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 BabbageEra 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 BabbageEra Word64
spec)
testMergeRngSpec :: Gen Property
testMergeRngSpec :: Gen Property
testMergeRngSpec = do
(RngSpec BabbageEra Word64
s1, RngSpec BabbageEra 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 BabbageEra Word64
s1 forall a. Semigroup a => a -> a -> a
<> RngSpec BabbageEra 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 BabbageEra Word64
s1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec BabbageEra Word64
s2) (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall prop. Testable prop => String -> prop -> Property
counterexample String
"" Bool
True))
RngSpec BabbageEra Word64
s3 -> do
let size :: Size
size = forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec BabbageEra 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 BabbageEra Word64
s1
, String
"s2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec BabbageEra Word64
s2
, String
"s3=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec BabbageEra 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 @BabbageEra [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) Int
n RngSpec BabbageEra 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 BabbageEra Word64
s1
forall a. [a] -> [a] -> [a]
++ String
"\n s2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec BabbageEra Word64
s2
forall a. [a] -> [a] -> [a]
++ String
"\n s3="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec BabbageEra 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 a. Rep era a -> Rep era [a]
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 BabbageEra 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 BabbageEra Word64
s2)
)
(forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Word64]
list RngSpec BabbageEra Word64
s1 Bool -> Bool -> Bool
&& forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Word64]
list RngSpec BabbageEra 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 BabbageEra 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 BabbageEra 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 BabbageEra Int, RngSpec BabbageEra Int,
RngSpec BabbageEra Int)
-> Gen
(RngSpec BabbageEra Int, Bool, RngSpec BabbageEra Int, Bool, [Int],
Bool, RngSpec BabbageEra Int)
check (RngSpec BabbageEra Int
x, RngSpec BabbageEra Int
y, RngSpec BabbageEra Int
m) = do
let size :: Size
size = forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec BabbageEra 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 BabbageEra Int
m)
, String
"s1<>s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec BabbageEra 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 BabbageEra Int
x)
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec BabbageEra 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 BabbageEra Int
y)
, String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec BabbageEra 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 @BabbageEra [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) Int
i RngSpec BabbageEra Int
m
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RngSpec BabbageEra Int
x, forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Int]
z RngSpec BabbageEra Int
x, RngSpec BabbageEra Int
y, forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Int]
z RngSpec BabbageEra Int
y, [Int]
z, forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Int]
z RngSpec BabbageEra Int
m, RngSpec BabbageEra 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 BabbageEra Int, RngSpec BabbageEra Int,
RngSpec BabbageEra Int)]
trips = [(RngSpec BabbageEra Int
x, RngSpec BabbageEra Int
y, RngSpec BabbageEra Int
m) | RngSpec BabbageEra Int
x <- [RngSpec BabbageEra Int]
xs, RngSpec BabbageEra Int
y <- [RngSpec BabbageEra Int]
ys, Just RngSpec BabbageEra Int
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent RngSpec BabbageEra Int
x RngSpec BabbageEra Int
y]]
[(RngSpec BabbageEra Int, Bool, RngSpec BabbageEra Int, Bool,
[Int], Bool, RngSpec BabbageEra Int)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (RngSpec BabbageEra Int, RngSpec BabbageEra Int,
RngSpec BabbageEra Int)
-> Gen
(RngSpec BabbageEra Int, Bool, RngSpec BabbageEra Int, Bool, [Int],
Bool, RngSpec BabbageEra Int)
check [(RngSpec BabbageEra Int, RngSpec BabbageEra Int,
RngSpec BabbageEra 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 BabbageEra Int, RngSpec BabbageEra Int,
RngSpec BabbageEra 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 BabbageEra Int, Bool, RngSpec BabbageEra Int, Bool,
[Int], Bool, RngSpec BabbageEra 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 a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a 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 a era. Ord a => Rep era a -> Rep era (Set a)
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 a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a 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 a era. Ord a => Rep era a -> Rep era (Set a)
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 a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a 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 a era. Ord a => Rep era a -> Rep era (Set a)
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 a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a 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 a era. Ord a => Rep era a -> Rep era (Set a)
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
ms) forall a. a -> [a] -> [a]
: [String]
msgs)
Gen w
genR
Int
n
RngSpec era w
rng
let domainlist :: [dom]
domainlist = forall a. Set a -> [a]
Set.toList Set dom
dom
extraPairs :: [(dom, w)]
extraPairs = forall d r era.
(Ord d, Eq r) =>
PairSide
-> Rep era d -> Rep era r -> Map d r -> ([d], [r]) -> [(d, r)]
pairSpecTransform PairSide
varside Rep era dom
dr Rep era w
rr Map dom w
m ([dom]
domainlist, [w]
rangelist)
case PairSide
varside of
PairSide
VarOnRight -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map dom w
m (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(dom, w)]
extraPairs))
PairSide
VarOnLeft -> forall k a. Ord k => Int -> Map k a -> Gen (Map k a)
subMapFromMapWithSize Int
n (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys Map dom w
m (forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(dom, w)]
extraPairs)))
pairSpecTransform ::
(Ord d, Eq r) => PairSide -> Rep era d -> Rep era r -> Map d r -> ([d], [r]) -> [(d, r)]
pairSpecTransform :: forall d r era.
(Ord d, Eq r) =>
PairSide
-> Rep era d -> Rep era r -> Map d r -> ([d], [r]) -> [(d, r)]
pairSpecTransform PairSide
side Rep era d
drep Rep era r
rrep Map d r
m ([d]
dlist, [r]
rlist) = forall a b. [a] -> [b] -> [(a, b)]
zip [d]
doms [r]
rngs
where
accum :: ([d], [r]) -> d -> r -> ([d], [r])
accum ([d]
ds, [r]
rs) d
k r
v = (forall a era.
Eq a =>
PairSide -> String -> Rep era a -> a -> [a] -> [a]
remove PairSide
side String
"domain" Rep era d
drep d
k [d]
ds, forall a era.
Eq a =>
PairSide -> String -> Rep era a -> a -> [a] -> [a]
remove PairSide
side String
"range" Rep era r
rrep r
v [r]
rs)
([d]
doms, [r]
rngs) = forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' ([d], [r]) -> d -> r -> ([d], [r])
accum ([d]
dlist, [r]
rlist) Map d r
m
remove :: Eq a => PairSide -> String -> Rep era a -> a -> [a] -> [a]
remove :: forall a era.
Eq a =>
PairSide -> String -> Rep era a -> a -> [a] -> [a]
remove PairSide
side String
part Rep era a
rep a
x (a
y : [a]
ys) =
if a
x forall a. Eq a => a -> a -> Bool
== a
y then [a]
ys else a
y forall a. a -> [a] -> [a]
: (forall a era.
Eq a =>
PairSide -> String -> Rep era a -> a -> [a] -> [a]
remove PairSide
side String
part Rep era a
rep a
x [a]
ys)
remove PairSide
VarOnLeft String
_part Rep era a
_rep a
_x [] = []
remove PairSide
VarOnRight String
part Rep era a
rep a
x [] =
forall a. HasCallStack => String -> [String] -> a
errorMess
( String
"In SubMap, when the variable is on the right (i.e. (SubMap map var) ) the "
forall a. [a] -> [a] -> [a]
++ String
part
forall a. [a] -> [a] -> [a]
++ String
"of map should contain "
forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era a
rep a
x
forall a. [a] -> [a] -> [a]
++ String
" which appears in the "
forall a. [a] -> [a] -> [a]
++ String
part
forall a. [a] -> [a] -> [a]
++ String
" of the PairSpec."
forall a. [a] -> [a] -> [a]
++ String
" But it does not."
)
[String
"genFromMapSpec"]
genMapSpecIsSound :: Gen Property
genMapSpecIsSound :: Gen Property
genMapSpecIsSound = do
Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
1, Int
15)
MapSpec BabbageEra Int Word64
spec <- 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 ((Int, Int) -> Gen Int
chooseInt (Int
1, Int
10000)) forall era. Rep era Int
IntR 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
Map Int Word64
mp <- forall era w dom.
(Era era, Ord dom) =>
String
-> [String]
-> Gen dom
-> Gen w
-> MapSpec era dom w
-> Gen (Map dom w)
genFromMapSpec @BabbageEra String
"mapSpecIsSound" [] (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
10000)) (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
10000)) MapSpec BabbageEra Int 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 MapSpec BabbageEra Int Word64
spec forall a. [a] -> [a] -> [a]
++ String
"\nmp = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Map Int Word64
mp) (forall d r era. (Ord d, Eq r) => Map d r -> MapSpec era d r -> Bool
runMapSpec Map Int Word64
mp MapSpec BabbageEra Int Word64
spec)
manyMergeMapSpec :: Gen (Int, Int, [String])
manyMergeMapSpec :: Gen (Int, Int, [String])
manyMergeMapSpec = do
Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
1, Int
10)
[MapSpec BabbageEra Int Word64]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
50 (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 a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) forall era. Rep era Int
IntR 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)
[MapSpec BabbageEra Int Word64]
ys <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
50 (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 a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) forall era. Rep era Int
IntR 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 check :: (MapSpec BabbageEra Int Word64, MapSpec BabbageEra Int Word64,
MapSpec BabbageEra Int Word64)
-> Gen
(MapSpec BabbageEra Int Word64, Bool,
MapSpec BabbageEra Int Word64, Bool, Map Int Word64, Bool,
MapSpec BabbageEra Int Word64)
check (MapSpec BabbageEra Int Word64
x, MapSpec BabbageEra Int Word64
y, MapSpec BabbageEra Int Word64
m) = do
let msize :: Size
msize = forall era d r. MapSpec era d r -> Size
sizeForMapSpec MapSpec BabbageEra Int Word64
m
Int
i <- Size -> Gen Int
genFromSize Size
msize
let wordsX :: [String]
wordsX =
[ String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
msize
, String
"s1<>s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec BabbageEra Int Word64
m
, String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era d r. MapSpec era d r -> Size
sizeForMapSpec MapSpec BabbageEra Int Word64
x)
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec BabbageEra Int Word64
x
, String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era d r. MapSpec era d r -> Size
sizeForMapSpec MapSpec BabbageEra Int Word64
y)
, String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec BabbageEra Int Word64
y
, String
"GenFromMapSpec " 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
]
Map Int Word64
z <- forall era w dom.
(Era era, Ord dom) =>
String
-> [String]
-> Gen dom
-> Gen w
-> MapSpec era dom w
-> Gen (Map dom w)
genFromMapSpec @BabbageEra String
"manyMergeMap" [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
100)) MapSpec BabbageEra Int Word64
m
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MapSpec BabbageEra Int Word64
x, forall d r era. (Ord d, Eq r) => Map d r -> MapSpec era d r -> Bool
runMapSpec Map Int Word64
z MapSpec BabbageEra Int Word64
x, MapSpec BabbageEra Int Word64
y, forall d r era. (Ord d, Eq r) => Map d r -> MapSpec era d r -> Bool
runMapSpec Map Int Word64
z MapSpec BabbageEra Int Word64
y, Map Int Word64
z, forall d r era. (Ord d, Eq r) => Map d r -> MapSpec era d r -> Bool
runMapSpec Map Int Word64
z MapSpec BabbageEra Int Word64
m, MapSpec BabbageEra Int Word64
m)
showAns :: (MapSpec era d r, a, MapSpec era d r, a, a, a, MapSpec era d r)
-> String
showAns (MapSpec era d r
s1, a
run1, MapSpec era d r
s2, a
run2, a
v, a
run3, MapSpec era d r
s3) =
[String] -> String
unlines
[ String
"\ns1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era d r
s1
, String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era d r. MapSpec era d r -> Size
sizeForMapSpec MapSpec era d r
s1)
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era d r
s2
, String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era d r. MapSpec era d r -> Size
sizeForMapSpec MapSpec era d r
s2)
, String
"s1 <> s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era d r
s3
, String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era d r. MapSpec era d r -> Size
sizeForMapSpec MapSpec era d r
s3)
, String
"v = genFromMapSpec (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
v
, String
"runMapSpec v s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run1
, String
"runMapSpec v s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run2
, String
"runMapSpec v (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run3
]
pr :: (MapSpec era d r, Bool, MapSpec era d r, Bool, a, Bool,
MapSpec era d r)
-> Maybe String
pr x :: (MapSpec era d r, Bool, MapSpec era d r, Bool, a, Bool,
MapSpec era d r)
x@(MapSpec era d r
_, Bool
a, MapSpec era d r
_, Bool
b, a
_, Bool
c, MapSpec era d r
_) = if Bool -> Bool
not (Bool
a Bool -> Bool -> Bool
&& Bool
b Bool -> Bool -> Bool
&& Bool
c) then forall a. a -> Maybe a
Just (forall {d} {d} {d} {a} {a} {a} {a} {era} {r} {era} {r} {era} {r}.
(Ord d, Ord d, Ord d, Show a, Show a, Show a, Show a) =>
(MapSpec era d r, a, MapSpec era d r, a, a, a, MapSpec era d r)
-> String
showAns (MapSpec era d r, Bool, MapSpec era d r, Bool, a, Bool,
MapSpec era d r)
x) else forall a. Maybe a
Nothing
let trips :: [(MapSpec BabbageEra Int Word64, MapSpec BabbageEra Int Word64,
MapSpec BabbageEra Int Word64)]
trips = [(MapSpec BabbageEra Int Word64
x, MapSpec BabbageEra Int Word64
y, MapSpec BabbageEra Int Word64
m) | MapSpec BabbageEra Int Word64
x <- [MapSpec BabbageEra Int Word64]
xs, MapSpec BabbageEra Int Word64
y <- [MapSpec BabbageEra Int Word64]
ys, Just MapSpec BabbageEra Int Word64
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent MapSpec BabbageEra Int Word64
x MapSpec BabbageEra Int Word64
y]]
[(MapSpec BabbageEra Int Word64, Bool,
MapSpec BabbageEra Int Word64, Bool, Map Int Word64, Bool,
MapSpec BabbageEra Int Word64)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (MapSpec BabbageEra Int Word64, MapSpec BabbageEra Int Word64,
MapSpec BabbageEra Int Word64)
-> Gen
(MapSpec BabbageEra Int Word64, Bool,
MapSpec BabbageEra Int Word64, Bool, Map Int Word64, Bool,
MapSpec BabbageEra Int Word64)
check [(MapSpec BabbageEra Int Word64, MapSpec BabbageEra Int Word64,
MapSpec BabbageEra Int Word64)]
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 [(MapSpec BabbageEra Int Word64, MapSpec BabbageEra Int Word64,
MapSpec BabbageEra Int Word64)]
trips, forall a. [Maybe a] -> [a]
Maybe.catMaybes (forall a b. (a -> b) -> [a] -> [b]
map forall {d} {d} {d} {a} {era} {r} {era} {r} {era} {r}.
(Ord d, Ord d, Ord d, Show a) =>
(MapSpec era d r, Bool, MapSpec era d r, Bool, a, Bool,
MapSpec era d r)
-> Maybe String
pr [(MapSpec BabbageEra Int Word64, Bool,
MapSpec BabbageEra Int Word64, Bool, Map Int Word64, Bool,
MapSpec BabbageEra Int Word64)]
ts))
reportManyMergeMapSpec :: IO ()
reportManyMergeMapSpec :: IO ()
reportManyMergeMapSpec = do
(Int
n, Int
passed, [String]
bad) <- forall a. Gen a -> IO a
generate Gen (Int, Int, [String])
manyMergeMapSpec
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 SetSpec era a where
SetSpec :: Ord a => Size -> RelSpec era a -> SetSpec era a
SetNever :: [String] -> SetSpec era a
instance Show (SetSpec era a) where show :: SetSpec era a -> String
show = forall era a. SetSpec era a -> String
showSetSpec
instance Ord a => Semigroup (SetSpec era a) where
<> :: SetSpec era a -> SetSpec era a -> SetSpec era a
(<>) = forall a era.
Ord a =>
SetSpec era a -> SetSpec era a -> SetSpec era a
mergeSetSpec
instance Ord a => Monoid (SetSpec era a) where
mempty :: SetSpec era a
mempty = forall a era. Ord a => Size -> RelSpec era a -> SetSpec era a
SetSpec Size
SzAny forall era dom. RelSpec era dom
RelAny
instance LiftT (SetSpec era t) where
liftT :: SetSpec era t -> Typed (SetSpec era t)
liftT (SetNever [String]
xs) = forall a. [String] -> Typed a
failT [String]
xs
liftT SetSpec era t
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure SetSpec era t
x
dropT :: Typed (SetSpec era t) -> SetSpec era t
dropT (Typed (Left [String]
s)) = forall era a. [String] -> SetSpec era a
SetNever [String]
s
dropT (Typed (Right SetSpec era t
x)) = SetSpec era t
x
showSetSpec :: SetSpec era a -> String
showSetSpec :: forall era a. SetSpec era a -> String
showSetSpec (SetSpec Size
s RelSpec era a
r) = [String] -> String
sepsP [String
"SetSpec", forall a. Show a => a -> String
show Size
s, forall a. Show a => a -> String
show RelSpec era a
r]
showSetSpec (SetNever [String]
_) = String
"SetNever"
mergeSetSpec :: Ord a => SetSpec era a -> SetSpec era a -> SetSpec era a
mergeSetSpec :: forall a era.
Ord a =>
SetSpec era a -> SetSpec era a -> SetSpec era a
mergeSetSpec SetSpec era a
s1 SetSpec era a
s2 = case (SetSpec era a
s1, SetSpec era a
s2) of
(SetNever [String]
xs, SetNever [String]
ys) -> forall era a. [String] -> SetSpec era a
SetNever ([String]
xs forall a. [a] -> [a] -> [a]
++ [String]
ys)
(SetNever [String]
xs, SetSpec era a
_) -> forall era a. [String] -> SetSpec era a
SetNever [String]
xs
(SetSpec era a
_, SetNever [String]
ys) -> forall era a. [String] -> SetSpec era a
SetNever [String]
ys
(SetSpec Size
SzAny RelSpec era a
RelAny, SetSpec era a
x) -> SetSpec era a
x
(SetSpec era a
x, SetSpec Size
SzAny RelSpec era a
RelAny) -> SetSpec era a
x
(SetSpec Size
s11 RelSpec era a
r1, SetSpec Size
s22 RelSpec era a
r2) -> case RelSpec era a
r1 forall a. Semigroup a => a -> a -> a
<> RelSpec era a
r2 of
RelNever [String]
xs -> forall era a. [String] -> SetSpec era a
SetNever ([String
"The SetSpec's are inconsistent.", String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec era a
s1, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec era a
s2] forall a. [a] -> [a] -> [a]
++ [String]
xs)
RelSpec era a
r3 -> 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 SetSpec era a
s1 forall a. [a] -> [a] -> [a]
++ String
"\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec era a
s2) forall a b. (a -> b) -> a -> b
$ forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Size
s11 forall a. Semigroup a => a -> a -> a
<> Size
s22) RelSpec era a
r3)
setSpec :: Ord t => Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec :: forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec Size
sz1 RelSpec era t
rel = case (Size
sz1 forall a. Semigroup a => a -> a -> a
<> Size
sz2) 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 a era. Ord a => Size -> RelSpec era a -> SetSpec era a
SetSpec Size
sz1 RelSpec era t
rel) 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 t
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]
++ String
"the expected size is " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
sz1
]
forall a. [a] -> [a] -> [a]
++ [String]
xs
)
Size
size -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a era. Ord a => Size -> RelSpec era a -> SetSpec era a
SetSpec Size
size RelSpec era t
rel)
where
sz2 :: Size
sz2 = forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era t
rel
runSetSpec :: Set a -> SetSpec era a -> Bool
runSetSpec :: forall a era. Set a -> SetSpec era a -> Bool
runSetSpec Set a
s (SetSpec Size
sz RelSpec era a
rel) = Int -> Size -> Bool
runSize (forall a. Set a -> Int
Set.size Set a
s) Size
sz Bool -> Bool -> Bool
&& forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set a
s RelSpec era a
rel
runSetSpec Set a
_ (SetNever [String]
msgs) = forall a. HasCallStack => String -> [String] -> a
errorMess String
"runSetSpec applied to SetNever" [String]
msgs
sizeForSetSpec :: SetSpec era a -> Size
sizeForSetSpec :: forall era a. SetSpec era a -> Size
sizeForSetSpec (SetSpec Size
sz RelSpec era a
_) = Size
sz
sizeForSetSpec (SetNever [String]
_) = Size
SzAny
genSetSpec :: Ord s => [String] -> Gen s -> Rep era s -> Int -> Gen (SetSpec era s)
genSetSpec :: forall s era.
Ord s =>
[String] -> Gen s -> Rep era s -> Int -> Gen (SetSpec era s)
genSetSpec [String]
msgs Gen s
genS Rep era s
repS Int
size = do
RelSpec era s
r <- forall dom era.
Ord dom =>
[String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec (String
"from genSetSpec" forall a. a -> [a] -> [a]
: [String]
msgs) Gen s
genS Rep era s
repS Int
size
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a era. Ord a => Size -> RelSpec era a -> SetSpec era a
SetSpec (Int -> Size
SzExact Int
size) RelSpec era s
r)
genFromSetSpec :: forall era a. Era era => [String] -> Gen a -> SetSpec era a -> Gen (Set a)
genFromSetSpec :: forall era a.
Era era =>
[String] -> Gen a -> SetSpec era a -> Gen (Set a)
genFromSetSpec [String]
msgs Gen a
genS (SetSpec Size
sz RelSpec era a
rp) = do
Int
n <- Size -> Gen Int
genFromSize Size
sz
forall era t.
(Era era, Ord t) =>
[String] -> Gen t -> Int -> RelSpec era t -> Gen (Set t)
genFromRelSpec (String
"genFromSetSpec" forall a. a -> [a] -> [a]
: [String]
msgs) Gen a
genS Int
n RelSpec era a
rp
genFromSetSpec [String]
_ Gen a
_ (SetNever [String]
msgs) = forall a. HasCallStack => String -> [String] -> a
errorMess String
"genFromSetSpec applied to SetNever" [String]
msgs
genSetSpecIsSound :: Gen Property
genSetSpecIsSound :: Gen Property
genSetSpecIsSound = do
Int
size <- (Int, Int) -> Gen Int
chooseInt (Int
0, Int
10)
SetSpec BabbageEra Int
spec <- forall s era.
Ord s =>
[String] -> Gen s -> Rep era s -> Int -> Gen (SetSpec era s)
genSetSpec [String]
msgs ((Int, Int) -> Gen Int
chooseInt (Int
1, Int
1000)) forall era. Rep era Int
IntR Int
size
Set Int
mp <- forall era a.
Era era =>
[String] -> Gen a -> SetSpec era a -> Gen (Set a)
genFromSetSpec @BabbageEra [String]
msgs (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
10000)) SetSpec BabbageEra Int
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 SetSpec BabbageEra Int
spec forall a. [a] -> [a] -> [a]
++ String
"\nmp = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Set Int
mp) (forall a era. Set a -> SetSpec era a -> Bool
runSetSpec Set Int
mp SetSpec BabbageEra Int
spec)
where
msgs :: [String]
msgs = [String
"genSetSpecIsSound"]
manyMergeSetSpec :: Gen (Int, Int, [String])
manyMergeSetSpec :: Gen (Int, Int, [String])
manyMergeSetSpec = do
Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
1, Int
10)
[SetSpec BabbageEra Int]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
50 (forall s era.
Ord s =>
[String] -> Gen s -> Rep era s -> Int -> Gen (SetSpec era s)
genSetSpec [] (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) forall era. Rep era Int
IntR Int
n)
[SetSpec BabbageEra Int]
ys <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
50 (forall s era.
Ord s =>
[String] -> Gen s -> Rep era s -> Int -> Gen (SetSpec era s)
genSetSpec [] (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) forall era. Rep era Int
IntR Int
n)
let check :: (SetSpec BabbageEra Int, SetSpec BabbageEra Int,
SetSpec BabbageEra Int)
-> Gen
(SetSpec BabbageEra Int, Bool, SetSpec BabbageEra Int, Bool,
Set Int, Bool, SetSpec BabbageEra Int)
check (SetSpec BabbageEra Int
x, SetSpec BabbageEra Int
y, SetSpec BabbageEra Int
m) = do
let msize :: Size
msize = forall era a. SetSpec era a -> Size
sizeForSetSpec SetSpec BabbageEra Int
m
Int
i <- Size -> Gen Int
genFromSize Size
msize
let wordsX :: [String]
wordsX =
[ String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
msize
, String
"s1<>s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec BabbageEra Int
m
, String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era a. SetSpec era a -> Size
sizeForSetSpec SetSpec BabbageEra Int
x)
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec BabbageEra Int
x
, String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era a. SetSpec era a -> Size
sizeForSetSpec SetSpec BabbageEra Int
y)
, String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec BabbageEra Int
y
, String
"GenFromSetSpec " 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 a.
Era era =>
[String] -> Gen a -> SetSpec era a -> Gen (Set a)
genFromSetSpec @BabbageEra [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) SetSpec BabbageEra Int
m
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SetSpec BabbageEra Int
x, forall a era. Set a -> SetSpec era a -> Bool
runSetSpec Set Int
z SetSpec BabbageEra Int
x, SetSpec BabbageEra Int
y, forall a era. Set a -> SetSpec era a -> Bool
runSetSpec Set Int
z SetSpec BabbageEra Int
y, Set Int
z, forall a era. Set a -> SetSpec era a -> Bool
runSetSpec Set Int
z SetSpec BabbageEra Int
m, SetSpec BabbageEra Int
m)
showAns :: (SetSpec era a, a, SetSpec era a, a, a, a, SetSpec era a) -> String
showAns (SetSpec era a
s1, a
run1, SetSpec era a
s2, a
run2, a
v, a
run3, SetSpec era a
s3) =
[String] -> String
unlines
[ String
"\ns1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec era a
s1
, String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era a. SetSpec era a -> Size
sizeForSetSpec SetSpec era a
s1)
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec era a
s2
, String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era a. SetSpec era a -> Size
sizeForSetSpec SetSpec era a
s2)
, String
"s1 <> s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec era a
s3
, String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era a. SetSpec era a -> Size
sizeForSetSpec SetSpec era a
s3)
, String
"v = genFromSetSpec (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
v
, String
"runSetSpec v s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run1
, String
"runSetSpec v s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run2
, String
"runSetSpec v (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run3
]
pr :: (SetSpec era a, Bool, SetSpec era a, Bool, a, Bool, SetSpec era a)
-> Maybe String
pr x :: (SetSpec era a, Bool, SetSpec era a, Bool, a, Bool, SetSpec era a)
x@(SetSpec era a
_, Bool
a, SetSpec era a
_, Bool
b, a
_, Bool
c, SetSpec era a
_) = 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} {a} {era} {a} {era} {a}.
(Show a, Show a, Show a, Show a) =>
(SetSpec era a, a, SetSpec era a, a, a, a, SetSpec era a) -> String
showAns (SetSpec era a, Bool, SetSpec era a, Bool, a, Bool, SetSpec era a)
x) else forall a. Maybe a
Nothing
let trips :: [(SetSpec BabbageEra Int, SetSpec BabbageEra Int,
SetSpec BabbageEra Int)]
trips = [(SetSpec BabbageEra Int
x, SetSpec BabbageEra Int
y, SetSpec BabbageEra Int
m) | SetSpec BabbageEra Int
x <- [SetSpec BabbageEra Int]
xs, SetSpec BabbageEra Int
y <- [SetSpec BabbageEra Int]
ys, Just SetSpec BabbageEra Int
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent SetSpec BabbageEra Int
x SetSpec BabbageEra Int
y]]
[(SetSpec BabbageEra Int, Bool, SetSpec BabbageEra Int, Bool,
Set Int, Bool, SetSpec BabbageEra Int)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SetSpec BabbageEra Int, SetSpec BabbageEra Int,
SetSpec BabbageEra Int)
-> Gen
(SetSpec BabbageEra Int, Bool, SetSpec BabbageEra Int, Bool,
Set Int, Bool, SetSpec BabbageEra Int)
check [(SetSpec BabbageEra Int, SetSpec BabbageEra Int,
SetSpec BabbageEra 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 [(SetSpec BabbageEra Int, SetSpec BabbageEra Int,
SetSpec BabbageEra Int)]
trips, forall a. [Maybe a] -> [a]
Maybe.catMaybes (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {era} {a} {era} {a} {era} {a}.
Show a =>
(SetSpec era a, Bool, SetSpec era a, Bool, a, Bool, SetSpec era a)
-> Maybe String
pr [(SetSpec BabbageEra Int, Bool, SetSpec BabbageEra Int, Bool,
Set Int, Bool, SetSpec BabbageEra Int)]
ts))
reportManyMergeSetSpec :: IO ()
reportManyMergeSetSpec :: IO ()
reportManyMergeSetSpec = do
(Int
n, Int
passed, [String]
bad) <- forall a. Gen a -> IO a
generate Gen (Int, Int, [String])
manyMergeSetSpec
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 ElemSpec era t where
ElemSum ::
Adds t =>
t ->
Size ->
ElemSpec era t
ElemProj ::
Adds c =>
c ->
Rep era x ->
Lens' x c ->
Size ->
ElemSpec era x
ElemEqual :: Eq t => Rep era t -> [t] -> ElemSpec era t
ElemNever :: [String] -> ElemSpec era t
ElemAny :: ElemSpec era t
instance Show (ElemSpec era a) where
show :: ElemSpec era a -> String
show = forall era a. ElemSpec era a -> String
showElemSpec
instance Era era => Semigroup (ElemSpec era a) where
<> :: ElemSpec era a -> ElemSpec era a -> ElemSpec era a
(<>) = forall era a.
Era era =>
ElemSpec era a -> ElemSpec era a -> ElemSpec era a
mergeElemSpec
instance Era era => Monoid (ElemSpec era a) where
mempty :: ElemSpec era a
mempty = forall era t. ElemSpec era t
ElemAny
instance LiftT (ElemSpec era t) where
liftT :: ElemSpec era t -> Typed (ElemSpec era t)
liftT (ElemNever [String]
xs) = forall a. [String] -> Typed a
failT [String]
xs
liftT ElemSpec era t
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure ElemSpec era t
x
dropT :: Typed (ElemSpec era t) -> ElemSpec era t
dropT (Typed (Left [String]
s)) = forall era t. [String] -> ElemSpec era t
ElemNever [String]
s
dropT (Typed (Right ElemSpec era t
x)) = ElemSpec era t
x
showElemSpec :: ElemSpec era a -> String
showElemSpec :: forall era a. ElemSpec era a -> String
showElemSpec (ElemSum a
small Size
sz) = [String] -> String
sepsP [String
"ElemSum", forall a. Show a => a -> String
show a
small, forall a. Show a => a -> String
show Size
sz]
showElemSpec (ElemProj c
small Rep era a
r Lens' a c
_l Size
sz) = [String] -> String
sepsP [String
"ElemProj", forall a. Show a => a -> String
show c
small, forall a. Show a => a -> String
show Rep era a
r, forall a. Show a => a -> String
show Size
sz]
showElemSpec (ElemEqual Rep era a
r [a]
xs) = [String] -> String
sepsP [String
"ElemEqual", forall a. Show a => a -> String
show Rep era a
r, forall e t. Rep e t -> t -> String
synopsis (forall era a. Rep era a -> Rep era [a]
ListR Rep era a
r) [a]
xs]
showElemSpec (ElemNever [String]
_) = String
"ElemNever"
showElemSpec ElemSpec era a
ElemAny = String
"ElemAny"
mergeElemSpec :: Era era => ElemSpec era a -> ElemSpec era a -> ElemSpec era a
mergeElemSpec :: forall era a.
Era era =>
ElemSpec era a -> ElemSpec era a -> ElemSpec era a
mergeElemSpec (ElemNever [String]
xs) (ElemNever [String]
ys) = forall era t. [String] -> ElemSpec era t
ElemNever ([String]
xs forall a. [a] -> [a] -> [a]
++ [String]
ys)
mergeElemSpec (ElemNever [String]
xs) ElemSpec era a
_ = forall era t. [String] -> ElemSpec era t
ElemNever [String]
xs
mergeElemSpec ElemSpec era a
_ (ElemNever [String]
ys) = forall era t. [String] -> ElemSpec era t
ElemNever [String]
ys
mergeElemSpec ElemSpec era a
ElemAny ElemSpec era a
x = ElemSpec era a
x
mergeElemSpec ElemSpec era a
x ElemSpec era a
ElemAny = ElemSpec era a
x
mergeElemSpec a :: ElemSpec era a
a@(ElemEqual Rep era a
r [a]
xs) b :: ElemSpec era a
b@(ElemEqual Rep era a
_ [a]
ys) =
if [a]
xs forall a. Eq a => a -> a -> Bool
== [a]
ys
then forall t era. Eq t => Rep era t -> [t] -> ElemSpec era t
ElemEqual Rep era a
r [a]
xs
else
forall era t. [String] -> ElemSpec era t
ElemNever
[ String
"The ElemSpec's are inconsistent."
, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
a
, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
b
, forall e t. Rep e t -> t -> String
synopsis (forall era a. Rep era a -> Rep era [a]
ListR Rep era a
r) [a]
xs forall a. [a] -> [a] -> [a]
++ String
" =/= " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall era a. Rep era a -> Rep era [a]
ListR Rep era a
r) [a]
ys
]
mergeElemSpec a :: ElemSpec era a
a@(ElemEqual Rep era a
_ [a]
xs) b :: ElemSpec era a
b@(ElemSum a
_ Size
sz) =
let computed :: a
computed = forall (t :: * -> *) c. (Foldable t, Adds c) => t c -> c
sumAdds [a]
xs
in if Int -> Size -> Bool
runSize (forall x. Adds x => x -> Int
toI a
computed) Size
sz
then ElemSpec era a
a
else
forall era t. [String] -> ElemSpec era t
ElemNever
[ String
"The ElemSpec's are inconsistent."
, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
a
, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
b
, String
"The computed sum("
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
computed
forall a. [a] -> [a] -> [a]
++ String
") is not in the allowed range of the Size("
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
sz
forall a. [a] -> [a] -> [a]
++ String
")"
]
mergeElemSpec b :: ElemSpec era a
b@(ElemSum a
_ Size
_) a :: ElemSpec era a
a@(ElemEqual Rep era a
_ [a]
_) = forall era a.
Era era =>
ElemSpec era a -> ElemSpec era a -> ElemSpec era a
mergeElemSpec ElemSpec era a
a ElemSpec era a
b
mergeElemSpec a :: ElemSpec era a
a@(ElemSum a
sm1 Size
sz1) b :: ElemSpec era a
b@(ElemSum a
sm2 Size
sz2) =
case Size
sz1 forall a. Semigroup a => a -> a -> a
<> Size
sz2 of
SzNever [String]
xs -> forall era t. [String] -> ElemSpec era t
ElemNever ([String] -> String
sepsP [String
"The ElemSpec's are inconsistent.", forall a. Show a => a -> String
show ElemSpec era a
a, forall a. Show a => a -> String
show ElemSpec era a
b] forall a. a -> [a] -> [a]
: [String]
xs)
Size
sz3 -> forall t era. Adds t => t -> Size -> ElemSpec era t
ElemSum (forall x. Adds x => x -> x -> x
smallerOf a
sm1 a
sm2) Size
sz3
mergeElemSpec ElemSpec era a
a ElemSpec era a
b = forall era t. [String] -> ElemSpec era t
ElemNever [String
"The ElemSpec's are inconsistent.", String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
a, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
b]
sizeForElemSpec :: forall a era. ElemSpec era a -> Size
sizeForElemSpec :: forall a era. ElemSpec era a -> Size
sizeForElemSpec (ElemNever [String]
_) = Size
SzAny
sizeForElemSpec ElemSpec era a
ElemAny = Size
SzAny
sizeForElemSpec (ElemEqual Rep era a
_ [a]
x) = Int -> Size
SzExact (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
x)
sizeForElemSpec (ElemSum a
smallest Size
sz) =
if forall x. Adds x => x -> Int
toI a
smallest 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 a
smallest)
else Int -> Size
SzLeast Int
1
sizeForElemSpec (ElemProj c
smallest (Rep era a
_r :: (Rep era c)) Lens' a c
_l Size
sz) =
if forall x. Adds x => x -> Int
toI c
smallest 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
smallest)
else Int -> Size
SzLeast Int
1
runElemSpec :: [a] -> ElemSpec era a -> Bool
runElemSpec :: forall a era. [a] -> ElemSpec era a -> Bool
runElemSpec [a]
xs ElemSpec era a
spec = case ElemSpec era a
spec of
ElemNever [String]
_ -> Bool
False
ElemSpec era a
ElemAny -> Bool
True
ElemEqual Rep era a
_ [a]
ys -> [a]
xs forall a. Eq a => a -> a -> Bool
== [a]
ys
ElemSum a
_ Size
sz -> Int -> Size -> Bool
runSize (forall x. Adds x => x -> Int
toI (forall (t :: * -> *) c. (Foldable t, Adds c) => t c -> c
sumAdds [a]
xs)) Size
sz
ElemProj c
_ Rep era a
_ Lens' a 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' a c
l [a]
xs)) Size
sz
genElemSpec ::
forall w era.
Adds w =>
Rep era w ->
SomeLens era w ->
Size ->
Gen (ElemSpec era w)
genElemSpec :: forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ElemSpec era w)
genElemSpec Rep era w
repw (SomeLens (Lens' w c
l :: Lens' w c)) Size
siz = do
let lo :: Int
lo = Size -> Int
minSize Size
siz
hi :: Int
hi = Size -> Int
maxSize Size
siz
if Int
lo forall a. Ord a => a -> a -> Bool
>= Int
1
then
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
[
( Int
2
, 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
hi))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall t era. Adds t => t -> Size -> ElemSpec era t
ElemSum (forall x. Adds x => [String] -> Int -> x
fromI [String
"genRngSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
siz] 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
hi))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall c era x.
Adds c =>
c -> Rep era x -> Lens' x c -> Size -> ElemSpec era x
ElemProj (forall x. Adds x => [String] -> Int -> x
fromI [String
"genRngSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
siz] Int
smallest) Rep era w
repw Lens' w c
l Size
sz)
)
, (Int
2, forall t era. Eq t => Rep era t -> [t] -> ElemSpec era t
ElemEqual Rep era w
repw forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Int
n <- Size -> Gen Int
genFromSize Size
siz; forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n (forall era b. Rep era b -> Gen b
genRep Rep era w
repw))
, (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era t. ElemSpec era t
ElemAny)
]
else
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
[ (Int
3, forall t era. Eq t => Rep era t -> [t] -> ElemSpec era t
ElemEqual Rep era w
repw forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Int
n <- Size -> Gen Int
genFromSize Size
siz; forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n (forall era b. Rep era b -> Gen b
genRep Rep era w
repw))
, (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era t. ElemSpec era t
ElemAny)
]
genFromElemSpec ::
forall era r.
[String] ->
Gen r ->
Int ->
ElemSpec era r ->
Gen [r]
genFromElemSpec :: forall era r. [String] -> Gen r -> Int -> ElemSpec era r -> Gen [r]
genFromElemSpec [String]
msgs Gen r
genr Int
n ElemSpec era r
x = case ElemSpec era r
x of
(ElemNever [String]
xs) -> forall a. HasCallStack => String -> [String] -> a
errorMess String
"RngNever in genFromElemSpec" [String]
xs
ElemSpec era r
ElemAny -> forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n Gen r
genr
(ElemEqual Rep era r
_ [r]
xs) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [r]
xs
(ElemSum 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]
msgs Int
n (forall x. Adds x => [String] -> Int -> x
fromI (String
msg forall a. a -> [a] -> [a]
: [String]
msgs) Int
tot)
(ElemProj 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]
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
where
msg :: String
msg = String
"genFromElemSpec " 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 ElemSpec era r
x
manyMergeElemSpec :: Gen (Size, Int, [String])
manyMergeElemSpec :: Gen (Size, Int, [String])
manyMergeElemSpec = do
Size
size <- Gen Size
genSize
[ElemSpec BabbageEra Word64]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
40 (forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ElemSpec era w)
genElemSpec forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Size
size)
[ElemSpec BabbageEra Word64]
ys <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
40 (forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ElemSpec era w)
genElemSpec forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Size
size)
let check :: (ElemSpec BabbageEra Word64, ElemSpec BabbageEra Word64,
ElemSpec BabbageEra Word64)
-> Gen
(ElemSpec BabbageEra Word64, Bool, ElemSpec BabbageEra Word64,
Bool, [Word64], Bool, ElemSpec BabbageEra Word64)
check (ElemSpec BabbageEra Word64
x, ElemSpec BabbageEra Word64
y, ElemSpec BabbageEra Word64
m) = do
let msize :: Size
msize = forall a era. ElemSpec era a -> Size
sizeForElemSpec ElemSpec BabbageEra Word64
m
Int
i <- Size -> Gen Int
genFromSize Size
msize
let wordsX :: [String]
wordsX =
[ String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
msize
, String
"s1<>s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec BabbageEra Word64
m
, String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a era. ElemSpec era a -> Size
sizeForElemSpec ElemSpec BabbageEra Word64
x)
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec BabbageEra Word64
x
, String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a era. ElemSpec era a -> Size
sizeForElemSpec ElemSpec BabbageEra Word64
y)
, String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec BabbageEra Word64
y
, String
"GenFromElemSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" size=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
size
]
[Word64]
z <- forall era r. [String] -> Gen r -> Int -> ElemSpec era r -> Gen [r]
genFromElemSpec @BabbageEra [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
100)) Int
i ElemSpec BabbageEra Word64
m
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ElemSpec BabbageEra Word64
x, forall a era. [a] -> ElemSpec era a -> Bool
runElemSpec [Word64]
z ElemSpec BabbageEra Word64
x, ElemSpec BabbageEra Word64
y, forall a era. [a] -> ElemSpec era a -> Bool
runElemSpec [Word64]
z ElemSpec BabbageEra Word64
y, [Word64]
z, forall a era. [a] -> ElemSpec era a -> Bool
runElemSpec [Word64]
z ElemSpec BabbageEra Word64
m, ElemSpec BabbageEra Word64
m)
showAns :: (ElemSpec era a, a, ElemSpec era a, a, a, a, ElemSpec era a)
-> String
showAns (ElemSpec era a
s1, a
run1, ElemSpec era a
s2, a
run2, a
v, a
run3, ElemSpec era a
s3) =
[String] -> String
unlines
[ String
"\ns1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
s1
, String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a era. ElemSpec era a -> Size
sizeForElemSpec ElemSpec era a
s1)
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
s2
, String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a era. ElemSpec era a -> Size
sizeForElemSpec ElemSpec era a
s2)
, String
"s1 <> s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
s3
, String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a era. ElemSpec era a -> Size
sizeForElemSpec ElemSpec era a
s3)
, String
"v = genFromElemSpec (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
v
, String
"runElemSpec v s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run1
, String
"runElemSpec v s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run2
, String
"runElemSpec v (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run3
]
pr :: (ElemSpec era a, Bool, ElemSpec era a, Bool, a, Bool,
ElemSpec era a)
-> Maybe String
pr x :: (ElemSpec era a, Bool, ElemSpec era a, Bool, a, Bool,
ElemSpec era a)
x@(ElemSpec era a
_, Bool
a, ElemSpec era a
_, Bool
b, a
_, Bool
c, ElemSpec era a
_) = 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} {a} {era} {a} {era} {a}.
(Show a, Show a, Show a, Show a) =>
(ElemSpec era a, a, ElemSpec era a, a, a, a, ElemSpec era a)
-> String
showAns (ElemSpec era a, Bool, ElemSpec era a, Bool, a, Bool,
ElemSpec era a)
x) else forall a. Maybe a
Nothing
let trips :: [(ElemSpec BabbageEra Word64, ElemSpec BabbageEra Word64,
ElemSpec BabbageEra Word64)]
trips = [(ElemSpec BabbageEra Word64
x, ElemSpec BabbageEra Word64
y, ElemSpec BabbageEra Word64
m) | ElemSpec BabbageEra Word64
x <- [ElemSpec BabbageEra Word64]
xs, ElemSpec BabbageEra Word64
y <- [ElemSpec BabbageEra Word64]
ys, Just ElemSpec BabbageEra Word64
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent ElemSpec BabbageEra Word64
x ElemSpec BabbageEra Word64
y]]
[(ElemSpec BabbageEra Word64, Bool, ElemSpec BabbageEra Word64,
Bool, [Word64], Bool, ElemSpec BabbageEra Word64)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ElemSpec BabbageEra Word64, ElemSpec BabbageEra Word64,
ElemSpec BabbageEra Word64)
-> Gen
(ElemSpec BabbageEra Word64, Bool, ElemSpec BabbageEra Word64,
Bool, [Word64], Bool, ElemSpec BabbageEra Word64)
check [(ElemSpec BabbageEra Word64, ElemSpec BabbageEra Word64,
ElemSpec BabbageEra Word64)]
trips
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (Size
size, forall (t :: * -> *) a. Foldable t => t a -> Int
length [(ElemSpec BabbageEra Word64, ElemSpec BabbageEra Word64,
ElemSpec BabbageEra Word64)]
trips, forall a. [Maybe a] -> [a]
Maybe.catMaybes (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {era} {a} {era} {a} {era} {a}.
Show a =>
(ElemSpec era a, Bool, ElemSpec era a, Bool, a, Bool,
ElemSpec era a)
-> Maybe String
pr [(ElemSpec BabbageEra Word64, Bool, ElemSpec BabbageEra Word64,
Bool, [Word64], Bool, ElemSpec BabbageEra Word64)]
ts))
reportManyMergeElemSpec :: IO ()
reportManyMergeElemSpec :: IO ()
reportManyMergeElemSpec = do
(Size
size, Int
passed, [String]
bad) <- forall a. Gen a -> IO a
generate Gen (Size, Int, [String])
manyMergeElemSpec
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 Size
size)
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 ListSpec era t where
ListSpec :: Size -> ElemSpec era t -> ListSpec era t
ListNever :: [String] -> ListSpec era t
instance Show (ListSpec era a) where
show :: ListSpec era a -> String
show = forall era a. ListSpec era a -> String
showListSpec
instance Era era => Semigroup (ListSpec era a) where
<> :: ListSpec era a -> ListSpec era a -> ListSpec era a
(<>) = forall era a.
Era era =>
ListSpec era a -> ListSpec era a -> ListSpec era a
mergeListSpec
instance Era era => Monoid (ListSpec era a) where
mempty :: ListSpec era a
mempty = forall era t. Size -> ElemSpec era t -> ListSpec era t
ListSpec Size
SzAny forall era t. ElemSpec era t
ElemAny
instance LiftT (ListSpec era t) where
liftT :: ListSpec era t -> Typed (ListSpec era t)
liftT (ListNever [String]
xs) = forall a. [String] -> Typed a
failT [String]
xs
liftT ListSpec era t
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure ListSpec era t
x
dropT :: Typed (ListSpec era t) -> ListSpec era t
dropT (Typed (Left [String]
s)) = forall era t. [String] -> ListSpec era t
ListNever [String]
s
dropT (Typed (Right ListSpec era t
x)) = ListSpec era t
x
showListSpec :: ListSpec era a -> String
showListSpec :: forall era a. ListSpec era a -> String
showListSpec (ListSpec Size
s ElemSpec era a
xs) = [String] -> String
sepsP [String
"ListSpec", forall a. Show a => a -> String
show Size
s, forall a. Show a => a -> String
show ElemSpec era a
xs]
showListSpec (ListNever [String]
_) = String
"ListNever"
mergeListSpec :: Era era => ListSpec era a -> ListSpec era a -> ListSpec era a
mergeListSpec :: forall era a.
Era era =>
ListSpec era a -> ListSpec era a -> ListSpec era a
mergeListSpec (ListNever [String]
xs) (ListNever [String]
ys) = forall era t. [String] -> ListSpec era t
ListNever ([String]
xs forall a. [a] -> [a] -> [a]
++ [String]
ys)
mergeListSpec (ListNever [String]
xs) (ListSpec Size
_ ElemSpec era a
_) = forall era t. [String] -> ListSpec era t
ListNever [String]
xs
mergeListSpec (ListSpec Size
_ ElemSpec era a
_) (ListNever [String]
xs) = forall era t. [String] -> ListSpec era t
ListNever [String]
xs
mergeListSpec a :: ListSpec era a
a@(ListSpec Size
s1 ElemSpec era a
e1) b :: ListSpec era a
b@(ListSpec Size
s2 ElemSpec era a
e2) =
case ElemSpec era a
e1 forall a. Semigroup a => a -> a -> a
<> ElemSpec era a
e2 of
ElemNever [String]
xs ->
forall era t. [String] -> ListSpec era t
ListNever ([String
"The ListSpec's are inconsistent.", String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec era a
a, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec era a
b] forall a. [a] -> [a] -> [a]
++ [String]
xs)
ElemSpec era a
e3 -> 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 ListSpec era a
a forall a. [a] -> [a] -> [a]
++ String
"\n " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec era a
b) forall a b. (a -> b) -> a -> b
$ forall era t. Size -> ElemSpec era t -> Typed (ListSpec era t)
listSpec (Size
s1 forall a. Semigroup a => a -> a -> a
<> Size
s2) ElemSpec era a
e3)
listSpec :: Size -> ElemSpec era t -> Typed (ListSpec era t)
listSpec :: forall era t. Size -> ElemSpec era t -> Typed (ListSpec era t)
listSpec Size
sz1 ElemSpec era t
el = case (Size
sz1 forall a. Semigroup a => a -> a -> a
<> Size
sz2) 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 t. Size -> ElemSpec era t -> ListSpec era t
ListSpec Size
sz1 ElemSpec era t
el) 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 ElemSpec era t
el 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]
++ String
"the expected size is " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
sz1
]
forall a. [a] -> [a] -> [a]
++ [String]
xs
)
Size
size -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era t. Size -> ElemSpec era t -> ListSpec era t
ListSpec Size
size ElemSpec era t
el)
where
sz2 :: Size
sz2 = forall a era. ElemSpec era a -> Size
sizeForElemSpec ElemSpec era t
el
sizeForListSpec :: ListSpec era t -> Size
sizeForListSpec :: forall era t. ListSpec era t -> Size
sizeForListSpec (ListSpec Size
sz ElemSpec era t
_) = Size
sz
sizeForListSpec (ListNever [String]
_) = Size
SzAny
runListSpec :: [a] -> ListSpec era a -> Bool
runListSpec :: forall a era. [a] -> ListSpec era a -> Bool
runListSpec [a]
xs ListSpec era a
spec = case ListSpec era a
spec of
ListNever [String]
_ -> Bool
False
ListSpec Size
sx ElemSpec era a
es -> Int -> Size -> Bool
runSize (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs) Size
sx Bool -> Bool -> Bool
&& forall a era. [a] -> ElemSpec era a -> Bool
runElemSpec [a]
xs ElemSpec era a
es
genListSpec ::
forall w era.
Adds w =>
Rep era w ->
SomeLens era w ->
Size ->
Gen (ListSpec era w)
genListSpec :: forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ListSpec era w)
genListSpec Rep era w
repw SomeLens era w
l Size
size = do
ElemSpec era w
e <- forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ElemSpec era w)
genElemSpec Rep era w
repw SomeLens era w
l Size
size
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era t. Size -> ElemSpec era t -> ListSpec era t
ListSpec Size
size ElemSpec era w
e)
genFromListSpec ::
forall era r.
[String] ->
Gen r ->
ListSpec era r ->
Gen [r]
genFromListSpec :: forall era r. [String] -> Gen r -> ListSpec era r -> Gen [r]
genFromListSpec [String]
_ Gen r
_ (ListNever [String]
xs) = forall a. HasCallStack => String -> [String] -> a
errorMess String
"ListNever in genFromListSpec" [String]
xs
genFromListSpec [String]
msgs Gen r
genr (ListSpec Size
size ElemSpec era r
e) = do
Int
n <- Size -> Gen Int
genFromSize Size
size
forall era r. [String] -> Gen r -> Int -> ElemSpec era r -> Gen [r]
genFromElemSpec (String
"genFromListSpec" forall a. a -> [a] -> [a]
: [String]
msgs) Gen r
genr Int
n ElemSpec era r
e
testSoundElemSpec :: Gen Property
testSoundElemSpec :: Gen Property
testSoundElemSpec = do
Size
size <- Gen Size
genSize
ElemSpec BabbageEra Word64
spec <- forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ElemSpec era w)
genElemSpec forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Size
size
Int
n <- Size -> Gen Int
genFromSize Size
size
[Word64]
list <-
forall era r. [String] -> Gen r -> Int -> ElemSpec era r -> Gen [r]
genFromElemSpec @BabbageEra
[String
"testSoundElemSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec BabbageEra Word64
spec forall a. [a] -> [a] -> [a]
++ String
" " 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
1000))
Int
n
ElemSpec BabbageEra 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
"size=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
size forall a. [a] -> [a] -> [a]
++ String
"\nspec=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec BabbageEra Word64
spec forall a. [a] -> [a] -> [a]
++ String
"\nlist=" forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall era a. Rep era a -> Rep era [a]
ListR forall era. Rep era Word64
Word64R) [Word64]
list)
(forall a era. [a] -> ElemSpec era a -> Bool
runElemSpec [Word64]
list ElemSpec BabbageEra Word64
spec)
testSoundListSpec :: Gen Property
testSoundListSpec :: Gen Property
testSoundListSpec = do
Size
size <- Gen Size
genSize
ListSpec BabbageEra Word64
spec <- forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ListSpec era w)
genListSpec forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Size
size
[Word64]
list <- forall era r. [String] -> Gen r -> ListSpec era r -> Gen [r]
genFromListSpec @BabbageEra [String
"testSoundListSpec"] (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) ListSpec BabbageEra 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 ListSpec BabbageEra Word64
spec forall a. [a] -> [a] -> [a]
++ String
"\nlist=" forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall era a. Rep era a -> Rep era [a]
ListR forall era. Rep era Word64
Word64R) [Word64]
list)
(forall a era. [a] -> ListSpec era a -> Bool
runListSpec [Word64]
list ListSpec BabbageEra Word64
spec)
manyMergeListSpec :: Gen (Size, Int, [String])
manyMergeListSpec :: Gen (Size, Int, [String])
manyMergeListSpec = do
Size
size <- Gen Size
genSize
[ListSpec BabbageEra Word64]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
40 (forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ListSpec era w)
genListSpec forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Size
size)
[ListSpec BabbageEra Word64]
ys <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
40 (forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ListSpec era w)
genListSpec forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Size
size)
let check :: (ListSpec BabbageEra Word64, ListSpec BabbageEra Word64,
ListSpec BabbageEra Word64)
-> Gen
(ListSpec BabbageEra Word64, Bool, ListSpec BabbageEra Word64,
Bool, [Word64], Bool, ListSpec BabbageEra Word64)
check (ListSpec BabbageEra Word64
x, ListSpec BabbageEra Word64
y, ListSpec BabbageEra Word64
m) = do
let msize :: Size
msize = forall era t. ListSpec era t -> Size
sizeForListSpec ListSpec BabbageEra Word64
m
Int
i <- Size -> Gen Int
genFromSize Size
msize
let wordsX :: [String]
wordsX =
[ String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
msize
, String
"s1<>s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec BabbageEra Word64
m
, String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era t. ListSpec era t -> Size
sizeForListSpec ListSpec BabbageEra Word64
x)
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec BabbageEra Word64
x
, String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era t. ListSpec era t -> Size
sizeForListSpec ListSpec BabbageEra Word64
y)
, String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec BabbageEra Word64
y
, String
"GenFromListSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" size=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
size
]
[Word64]
z <- forall era r. [String] -> Gen r -> ListSpec era r -> Gen [r]
genFromListSpec @BabbageEra [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
100)) ListSpec BabbageEra Word64
m
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ListSpec BabbageEra Word64
x, forall a era. [a] -> ListSpec era a -> Bool
runListSpec [Word64]
z ListSpec BabbageEra Word64
x, ListSpec BabbageEra Word64
y, forall a era. [a] -> ListSpec era a -> Bool
runListSpec [Word64]
z ListSpec BabbageEra Word64
y, [Word64]
z, forall a era. [a] -> ListSpec era a -> Bool
runListSpec [Word64]
z ListSpec BabbageEra Word64
m, ListSpec BabbageEra Word64
m)
showAns :: (ListSpec era t, a, ListSpec era t, a, a, a, ListSpec era t)
-> String
showAns (ListSpec era t
s1, a
run1, ListSpec era t
s2, a
run2, a
v, a
run3, ListSpec era t
s3) =
[String] -> String
unlines
[ String
"\ns1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec era t
s1
, String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era t. ListSpec era t -> Size
sizeForListSpec ListSpec era t
s1)
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec era t
s2
, String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era t. ListSpec era t -> Size
sizeForListSpec ListSpec era t
s2)
, String
"s1 <> s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec era t
s3
, String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era t. ListSpec era t -> Size
sizeForListSpec ListSpec era t
s3)
, String
"v = genFromListSpec (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
v
, String
"runListSpec v s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run1
, String
"runListSpec v s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run2
, String
"runListSpec v (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run3
]
pr :: (ListSpec era t, Bool, ListSpec era t, Bool, a, Bool,
ListSpec era t)
-> Maybe String
pr x :: (ListSpec era t, Bool, ListSpec era t, Bool, a, Bool,
ListSpec era t)
x@(ListSpec era t
_, Bool
a, ListSpec era t
_, Bool
b, a
_, Bool
c, ListSpec era t
_) = 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} {t} {era} {t} {era} {t}.
(Show a, Show a, Show a, Show a) =>
(ListSpec era t, a, ListSpec era t, a, a, a, ListSpec era t)
-> String
showAns (ListSpec era t, Bool, ListSpec era t, Bool, a, Bool,
ListSpec era t)
x) else forall a. Maybe a
Nothing
let trips :: [(ListSpec BabbageEra Word64, ListSpec BabbageEra Word64,
ListSpec BabbageEra Word64)]
trips = [(ListSpec BabbageEra Word64
x, ListSpec BabbageEra Word64
y, ListSpec BabbageEra Word64
m) | ListSpec BabbageEra Word64
x <- [ListSpec BabbageEra Word64]
xs, ListSpec BabbageEra Word64
y <- [ListSpec BabbageEra Word64]
ys, Just ListSpec BabbageEra Word64
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent ListSpec BabbageEra Word64
x ListSpec BabbageEra Word64
y]]
[(ListSpec BabbageEra Word64, Bool, ListSpec BabbageEra Word64,
Bool, [Word64], Bool, ListSpec BabbageEra Word64)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ListSpec BabbageEra Word64, ListSpec BabbageEra Word64,
ListSpec BabbageEra Word64)
-> Gen
(ListSpec BabbageEra Word64, Bool, ListSpec BabbageEra Word64,
Bool, [Word64], Bool, ListSpec BabbageEra Word64)
check [(ListSpec BabbageEra Word64, ListSpec BabbageEra Word64,
ListSpec BabbageEra Word64)]
trips
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (Size
size, forall (t :: * -> *) a. Foldable t => t a -> Int
length [(ListSpec BabbageEra Word64, ListSpec BabbageEra Word64,
ListSpec BabbageEra Word64)]
trips, forall a. [Maybe a] -> [a]
Maybe.catMaybes (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {era} {t} {era} {t} {era} {t}.
Show a =>
(ListSpec era t, Bool, ListSpec era t, Bool, a, Bool,
ListSpec era t)
-> Maybe String
pr [(ListSpec BabbageEra Word64, Bool, ListSpec BabbageEra Word64,
Bool, [Word64], Bool, ListSpec BabbageEra Word64)]
ts))
reportManyMergeListSpec :: IO ()
reportManyMergeListSpec :: IO ()
reportManyMergeListSpec = do
(Size
size, Int
passed, [String]
bad) <- forall a. Gen a -> IO a
generate Gen (Size, Int, [String])
manyMergeListSpec
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 Size
size)
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"
class (Arbitrary t, Adds t) => TestAdd t where
anyAdds :: Gen t
pos :: Gen t
instance TestAdd Word64 where
anyAdds :: Gen Word64
anyAdds = forall a. Random a => (a, a) -> Gen a
choose (Word64
0, Word64
12)
pos :: Gen Word64
pos = forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
12)
instance TestAdd Coin where
anyAdds :: Gen Coin
anyAdds = Integer -> Coin
Coin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Integer
0, Integer
8)
pos :: Gen Coin
pos = Integer -> Coin
Coin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Integer
1, Integer
8)
instance TestAdd Int where
anyAdds :: Gen Int
anyAdds = (Int, Int) -> Gen Int
chooseInt (Int
0, Int
atMostAny)
pos :: Gen Int
pos = (Int, Int) -> Gen Int
chooseInt (Int
1, Int
atMostAny)
genSet :: Ord t => Int -> Gen t -> Gen (Set t)
genSet :: forall t. Ord t => Int -> Gen t -> Gen (Set t)
genSet Int
n Gen t
gen = do
[t]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
20 Gen t
gen
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Ord a => [a] -> Set a
Set.fromList (forall a. Int -> [a] -> [a]
take Int
n (forall a. Eq a => [a] -> [a]
List.nub [t]
xs)))
testSet :: (Ord t, TestAdd t) => Gen (Set t)
testSet :: forall t. (Ord t, TestAdd t) => Gen (Set t)
testSet = do
Int
n <- forall t. TestAdd t => Gen t
pos @Int
forall a. Ord a => [a] -> Set a
Set.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n forall t. TestAdd t => Gen t
anyAdds
someSet :: Ord t => Gen t -> Gen (Set t)
someSet :: forall t. Ord t => Gen t -> Gen (Set t)
someSet Gen t
g = do
Int
n <- forall t. TestAdd t => Gen t
pos @Int
forall a. Ord a => [a] -> Set a
Set.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n Gen t
g
someMap :: forall era t d. (Ord d, TestAdd t) => Rep era d -> Gen (Map d t)
someMap :: forall era t d. (Ord d, TestAdd t) => Rep era d -> Gen (Map d t)
someMap Rep era d
r = do
Int
n <- forall t. TestAdd t => Gen t
pos @Int
[t]
rs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n forall t. TestAdd t => Gen t
anyAdds
[d]
ds <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n (forall era b. Rep era b -> Gen b
genRep Rep era d
r)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [d]
ds [t]
rs)
aMap :: Era era => Gen (MapSpec era Int Word64)
aMap :: forall era. Era era => Gen (MapSpec era Int Word64)
aMap = 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 ((Int, Int) -> Gen Int
chooseInt (Int
1, Int
1000)) forall era. Rep era Int
IntR forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Int
4
testm :: Gen (MapSpec BabbageEra Int Word64)
testm :: Gen (MapSpec BabbageEra Int Word64)
testm = do
MapSpec BabbageEra Int Word64
a <- forall era. Era era => Gen (MapSpec era Int Word64)
aMap @BabbageEra
MapSpec BabbageEra Int Word64
b <- forall era. Era era => Gen (MapSpec era Int Word64)
aMap
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall x. LiftT x => x -> Typed x
liftT (MapSpec BabbageEra Int Word64
a forall a. Semigroup a => a -> a -> a
<> MapSpec BabbageEra Int Word64
b))
aList :: Gen (ListSpec era Word64)
aList :: forall era. Gen (ListSpec era Word64)
aList = Gen Size
genSize forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ListSpec era w)
genListSpec forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL)
testl :: Gen (ListSpec BabbageEra Word64)
testl :: Gen (ListSpec BabbageEra Word64)
testl = do
ListSpec BabbageEra Word64
a <- forall era. Gen (ListSpec era Word64)
aList @BabbageEra
ListSpec BabbageEra Word64
b <- forall era. Gen (ListSpec era Word64)
aList
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall x. LiftT x => x -> Typed x
liftT (ListSpec BabbageEra Word64
a forall a. Semigroup a => a -> a -> a
<> ListSpec BabbageEra Word64
b))
testV :: Era era => V era DeltaCoin
testV :: forall era. Era era => V era DeltaCoin
testV = (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"x" forall era. Rep era DeltaCoin
DeltaCoinR forall era s t. Access era s t
No)
genSumsTo :: Era era => Gen (Pred era)
genSumsTo :: forall era. Era era => Gen (Pred era)
genSumsTo = do
OrdCond
c <- Gen OrdCond
genOrdCond
let v :: Term era DeltaCoin
v = forall era t. V era t -> Term era t
Var forall era. Era era => V era DeltaCoin
testV
Term era DeltaCoin
rhs <- (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era DeltaCoin
DeltaCoinR forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> DeltaCoin
DeltaCoin) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (-Integer
10, Integer
10)
Term era DeltaCoin
lhs <- (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era DeltaCoin
DeltaCoinR forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> DeltaCoin
DeltaCoin) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (-Integer
10, Integer
10)
forall a. HasCallStack => [a] -> Gen a
elements
[forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. a -> Either a b
Left (Integer -> DeltaCoin
DeltaCoin Integer
1)) Term era DeltaCoin
v OrdCond
c [forall era c. Term era c -> Sum era c
One Term era DeltaCoin
rhs], forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. a -> Either a b
Left (Integer -> DeltaCoin
DeltaCoin Integer
1)) Term era DeltaCoin
lhs OrdCond
c [forall era c. Term era c -> Sum era c
One Term era DeltaCoin
rhs, forall era c. Term era c -> Sum era c
One Term era DeltaCoin
v]]
solveSumsTo :: Pred era -> AddsSpec DeltaCoin
solveSumsTo :: forall era. Pred era -> AddsSpec DeltaCoin
solveSumsTo (SumsTo Direct c
_ (Lit Rep era c
DeltaCoinR c
n) OrdCond
cond [One (Lit Rep era c
DeltaCoinR c
m), One (Var (V String
nam Rep era c
_ Access era s c
_))]) =
forall a c.
Adds a =>
[String] -> a -> OrdCond -> a -> String -> AddsSpec c
varOnRight @DeltaCoin [String
"solveSumsTo"] c
n OrdCond
cond c
m String
nam
solveSumsTo (SumsTo Direct c
_ (Var (V String
nam Rep era c
DeltaCoinR Access era s c
_)) OrdCond
cond [One (Lit Rep era c
DeltaCoinR c
m)]) =
forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
nam OrdCond
cond c
m
solveSumsTo Pred era
x = forall c. [String] -> AddsSpec c
AddsSpecNever [String
"solveSumsTo " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred era
x]
condReverse :: Gen Property
condReverse :: Gen Property
condReverse = do
Pred BabbageEra
predicate <- forall era. Era era => Gen (Pred era)
genSumsTo
let addsSpec :: AddsSpec DeltaCoin
addsSpec = forall era. Pred era -> AddsSpec DeltaCoin
solveSumsTo Pred BabbageEra
predicate
let msgs :: [String]
msgs = [String
"condFlip", forall a. Show a => a -> String
show Pred BabbageEra
predicate, forall a. Show a => a -> String
show AddsSpec DeltaCoin
addsSpec]
Int
n <- forall c. [String] -> AddsSpec c -> Gen Int
genFromAddsSpec [String]
msgs AddsSpec DeltaCoin
addsSpec
let env :: Env BabbageEra
env = forall era t. V era t -> t -> Env era -> Env era
storeVar forall era. Era era => V era DeltaCoin
testV (forall x. Adds x => [String] -> Int -> x
fromI (forall a. Show a => a -> String
show Int
n forall a. a -> [a] -> [a]
: [String]
msgs) Int
n) forall era. Env era
emptyEnv
case forall x. Typed x -> Either [String] x
runTyped (forall era. Env era -> Pred era -> Typed Bool
runPred @BabbageEra Env BabbageEra
env Pred BabbageEra
predicate) of
Right Bool
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines (forall a. Show a => a -> String
show Int
n forall a. a -> [a] -> [a]
: [String]
msgs)) Bool
x)
Left [String]
xs -> forall a. HasCallStack => String -> [String] -> a
errorMess String
"runTyped in condFlip fails" ([String]
xs forall a. [a] -> [a] -> [a]
++ (forall a. Show a => a -> String
show Int
n forall a. a -> [a] -> [a]
: [String]
msgs))
genAddsSpec :: forall c. Adds c => Gen (AddsSpec c)
genAddsSpec :: forall c. Adds c => Gen (AddsSpec c)
genAddsSpec = do
String
v <- forall a. HasCallStack => [a] -> Gen a
elements [String
"x", String
"y"]
OrdCond
c <- Gen OrdCond
genOrdCond
c
rhs <- forall x. Adds x => [String] -> Int -> x
fromI @c [String
"genAddsSpec"] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose @Int (-Int
25, Int
25)
c
lhs <- forall x. Adds x => [String] -> Int -> x
fromI @c [String
"genAddsSpec"] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose @Int (-Int
25, Int
25)
forall a. HasCallStack => [a] -> Gen a
elements [forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
v OrdCond
c c
rhs, forall a c.
Adds a =>
[String] -> a -> OrdCond -> a -> String -> AddsSpec c
varOnRight [String
"genAddsSpec"] c
lhs OrdCond
c c
rhs String
v]
genNonNegAddsSpec :: forall c. Adds c => Gen (AddsSpec c)
genNonNegAddsSpec :: forall c. Adds c => Gen (AddsSpec c)
genNonNegAddsSpec = do
String
v <- forall a. HasCallStack => [a] -> Gen a
elements [String
"x", String
"y"]
OrdCond
c <- Gen OrdCond
genOrdCond
Int
lhs <- forall a. Random a => (a, a) -> Gen a
choose @Int (Int
10, Int
30)
Int
rhs <- forall a. Random a => (a, a) -> Gen a
choose @Int (Int
1, Int
lhs forall a. Num a => a -> a -> a
- Int
1)
let lhs' :: Int
lhs' = case OrdCond
c of
OrdCond
LTH -> Int
lhs forall a. Num a => a -> a -> a
+ Int
1
OrdCond
_ -> Int
lhs
fromX :: Int -> c
fromX Int
x = forall x. Adds x => [String] -> Int -> x
fromI @c [String
"genNonNegAddsSpec"] Int
x
forall a. HasCallStack => [a] -> Gen a
elements [forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
v OrdCond
c forall a b. (a -> b) -> a -> b
$ Int -> c
fromX Int
rhs, forall a c.
Adds a =>
[String] -> a -> OrdCond -> a -> String -> AddsSpec c
varOnRight [String
"genNonNegAddsSpec"] (Int -> c
fromX Int
lhs') OrdCond
c (Int -> c
fromX Int
rhs) String
v]
genOrdCond :: Gen OrdCond
genOrdCond :: Gen OrdCond
genOrdCond = forall a. HasCallStack => [a] -> Gen a
elements [OrdCond
EQL, OrdCond
LTH, OrdCond
LTE, OrdCond
GTH, OrdCond
GTE]
runAddsSpec :: forall c. Adds c => c -> AddsSpec c -> Bool
runAddsSpec :: forall c. Adds c => c -> AddsSpec c -> Bool
runAddsSpec c
c (AddsSpecSize String
_ Size
size) = Int -> Size -> Bool
runSize (forall x. Adds x => x -> Int
toI c
c) Size
size
runAddsSpec c
_ AddsSpec c
AddsSpecAny = Bool
True
runAddsSpec c
_ (AddsSpecNever [String]
_) = Bool
False
sizeForAddsSpec :: AddsSpec c -> Size
sizeForAddsSpec :: forall c. AddsSpec c -> Size
sizeForAddsSpec (AddsSpecSize String
_ Size
s) = Size
s
sizeForAddsSpec AddsSpec c
AddsSpecAny = Size
SzAny
sizeForAddsSpec (AddsSpecNever [String]
xs) = [String] -> Size
SzNever [String]
xs
tryManyAddsSpec ::
Gen (AddsSpec Int) -> ([String] -> AddsSpec Int -> Gen Int) -> Gen (Int, [String])
tryManyAddsSpec :: Gen (AddsSpec Int)
-> ([String] -> AddsSpec Int -> Gen Int) -> Gen (Int, [String])
tryManyAddsSpec Gen (AddsSpec Int)
genSum [String] -> AddsSpec Int -> Gen Int
genFromSum = do
[AddsSpec Int]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
25 Gen (AddsSpec Int)
genSum
[AddsSpec Int]
ys <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
25 Gen (AddsSpec Int)
genSum
let check :: (AddsSpec Int, AddsSpec Int, AddsSpec Int)
-> Gen
(AddsSpec Int, Bool, AddsSpec Int, Bool, Int, Bool, AddsSpec Int)
check (AddsSpec Int
x, AddsSpec Int
y, AddsSpec Int
m) = do
Int
z <- [String] -> AddsSpec Int -> Gen Int
genFromSum [String
"test tryManyAddsSpec"] AddsSpec Int
m
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AddsSpec Int
x, forall c. Adds c => c -> AddsSpec c -> Bool
runAddsSpec Int
z AddsSpec Int
x, AddsSpec Int
y, forall c. Adds c => c -> AddsSpec c -> Bool
runAddsSpec Int
z AddsSpec Int
y, Int
z, forall c. Adds c => c -> AddsSpec c -> Bool
runAddsSpec Int
z AddsSpec Int
m, AddsSpec Int
m)
showAns :: (AddsSpec c, Bool, AddsSpec c, Bool, Int, Bool, AddsSpec c) -> String
showAns :: forall c.
(AddsSpec c, Bool, AddsSpec c, Bool, Int, Bool, AddsSpec c)
-> String
showAns (AddsSpec c
s1, Bool
run1, AddsSpec c
s2, Bool
run2, Int
v, Bool
run3, AddsSpec c
s3) =
[String] -> String
unlines
[ String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AddsSpec c
s1
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AddsSpec c
s2
, String
"s1 <> s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AddsSpec c
s3
, String
"v = genFromAdsSpec (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
v
, String
"runAddsSpec s1 v = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Bool
run1
, String
"runAddsSpec s2 v = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Bool
run2
, String
"runAddsSpec (s1 <> s2) v = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Bool
run3
]
pr :: (AddsSpec c, Bool, AddsSpec c, Bool, Int, Bool, AddsSpec c)
-> Maybe String
pr x :: (AddsSpec c, Bool, AddsSpec c, Bool, Int, Bool, AddsSpec c)
x@(AddsSpec c
_, Bool
a, AddsSpec c
_, Bool
b, Int
_, Bool
c, AddsSpec c
_) = if Bool -> Bool
not (Bool
a Bool -> Bool -> Bool
&& Bool
b Bool -> Bool -> Bool
&& Bool
c) then forall a. a -> Maybe a
Just (forall c.
(AddsSpec c, Bool, AddsSpec c, Bool, Int, Bool, AddsSpec c)
-> String
showAns (AddsSpec c, Bool, AddsSpec c, Bool, Int, Bool, AddsSpec c)
x) else forall a. Maybe a
Nothing
let trips :: [(AddsSpec Int, AddsSpec Int, AddsSpec Int)]
trips = [(AddsSpec Int
x, AddsSpec Int
y, AddsSpec Int
m) | AddsSpec Int
x <- [AddsSpec Int]
xs, AddsSpec Int
y <- [AddsSpec Int]
ys, Just AddsSpec Int
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent AddsSpec Int
x AddsSpec Int
y]]
[(AddsSpec Int, Bool, AddsSpec Int, Bool, Int, Bool, AddsSpec Int)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (AddsSpec Int, AddsSpec Int, AddsSpec Int)
-> Gen
(AddsSpec Int, Bool, AddsSpec Int, Bool, Int, Bool, AddsSpec Int)
check [(AddsSpec Int, AddsSpec Int, AddsSpec Int)]
trips
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(AddsSpec Int, AddsSpec Int, AddsSpec Int)]
trips, forall a. [Maybe a] -> [a]
Maybe.catMaybes (forall a b. (a -> b) -> [a] -> [b]
map forall {c}.
(AddsSpec c, Bool, AddsSpec c, Bool, Int, Bool, AddsSpec c)
-> Maybe String
pr [(AddsSpec Int, Bool, AddsSpec Int, Bool, Int, Bool, AddsSpec Int)]
ts))
reportManyAddsSpec :: IO ()
reportManyAddsSpec :: IO ()
reportManyAddsSpec = do
(Int
passed, [String]
bad) <- forall a. Gen a -> IO a
generate (Gen (AddsSpec Int)
-> ([String] -> AddsSpec Int -> Gen Int) -> Gen (Int, [String])
tryManyAddsSpec forall c. Adds c => Gen (AddsSpec c)
genAddsSpec forall c. [String] -> AddsSpec c -> Gen Int
genFromAddsSpec)
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.")
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"
reportManyNonNegAddsSpec :: IO ()
reportManyNonNegAddsSpec :: IO ()
reportManyNonNegAddsSpec = do
(Int
passed, [String]
bad) <- forall a. Gen a -> IO a
generate (Gen (AddsSpec Int)
-> ([String] -> AddsSpec Int -> Gen Int) -> Gen (Int, [String])
tryManyAddsSpec forall c. Adds c => Gen (AddsSpec c)
genNonNegAddsSpec forall c. [String] -> AddsSpec c -> Gen Int
genFromNonNegAddsSpec)
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.")
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"
testSoundNonNegAddsSpec :: Gen Property
testSoundNonNegAddsSpec :: Gen Property
testSoundNonNegAddsSpec = do
AddsSpec Int
spec <- forall c. Adds c => Gen (AddsSpec c)
genNonNegAddsSpec @Int
Int
c <- forall c. [String] -> AddsSpec c -> Gen Int
genFromNonNegAddsSpec [String
"testSoundAddsSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AddsSpec Int
spec] AddsSpec Int
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
"AddsSpec=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AddsSpec Int
spec forall a. [a] -> [a] -> [a]
++ String
"\ngenerated value " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
c)
(forall c. Adds c => c -> AddsSpec c -> Bool
runAddsSpec Int
c AddsSpec Int
spec)
testSoundAddsSpec :: Gen Property
testSoundAddsSpec :: Gen Property
testSoundAddsSpec = do
AddsSpec DeltaCoin
spec <- forall c. Adds c => Gen (AddsSpec c)
genAddsSpec @DeltaCoin
Int
c <- forall c. [String] -> AddsSpec c -> Gen Int
genFromAddsSpec [String
"testSoundAddsSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AddsSpec DeltaCoin
spec] AddsSpec DeltaCoin
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
"AddsSpec=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AddsSpec DeltaCoin
spec forall a. [a] -> [a] -> [a]
++ String
"\ngenerated value " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
c)
(forall c. Adds c => c -> AddsSpec c -> Bool
runAddsSpec (forall x. Adds x => [String] -> Int -> x
fromI [String
"testSoundAddsSpec"] Int
c) AddsSpec DeltaCoin
spec)
allSpecTests :: TestTree
allSpecTests :: TestTree
allSpecTests =
String -> [TestTree] -> TestTree
testGroup
String
"Spec tests"
[ forall a. Testable a => String -> a -> TestTree
testProperty String
"reversing OrdCond" Gen Property
condReverse
, String -> [TestTree] -> TestTree
testGroup
String
"Size test"
[ forall a. Testable a => String -> a -> TestTree
testProperty String
"test Size sound" Gen Bool
testSoundSize
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test genFromSize is non-negative" Gen Bool
testNonNegSize
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test merging Size" Gen Bool
testMergeSize
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test alternate merge Size" Gen Property
testMergeSize2
]
, String -> [TestTree] -> TestTree
testGroup
String
"RelSpec tests"
[ forall a. Testable a => String -> a -> TestTree
testProperty String
"we generate consistent RelSpecs" Gen Property
testConsistentRel
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test RelSpec sound" Gen Property
testSoundRelSpec
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test mergeRelSpec" Gen Property
testMergeRelSpec
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test More consistent RelSpec" IO ()
reportManyMergeRelSpec
]
, String -> [TestTree] -> TestTree
testGroup
String
"RngSpec tests"
[ forall a. Testable a => String -> a -> TestTree
testProperty String
"we generate consistent RngSpec" Gen Property
testConsistentRng
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test RngSpec sound" Gen Property
testSoundRngSpec
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test mergeRngSpec" Gen Property
testMergeRngSpec
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test More consistent RngSpec" IO ()
reportManyMergeRngSpec
]
, String -> [TestTree] -> TestTree
testGroup
String
"MapSpec tests"
[ forall a. Testable a => String -> a -> TestTree
testProperty String
"test MapSpec sound" Gen Property
genMapSpecIsSound
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test More consistent MapSpec" IO ()
reportManyMergeMapSpec
]
, String -> [TestTree] -> TestTree
testGroup
String
"SetSpec tests"
[ forall a. Testable a => String -> a -> TestTree
testProperty String
"test SetSpec sound" Gen Property
genSetSpecIsSound
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test More consistent SetSpec" IO ()
reportManyMergeSetSpec
]
, String -> [TestTree] -> TestTree
testGroup
String
"ListSpec tests"
[ forall a. Testable a => String -> a -> TestTree
testProperty String
"test ElemSpec sound" Gen Property
testSoundElemSpec
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test consistent ElemSpec" IO ()
reportManyMergeElemSpec
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test ListSpec sound" Gen Property
testSoundListSpec
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test consistent ListSpec" IO ()
reportManyMergeListSpec
]
, String -> [TestTree] -> TestTree
testGroup
String
"AddsSpec tests"
[ forall a. Testable a => String -> a -> TestTree
testProperty String
"test Sound MergeAddsSpec" IO ()
reportManyAddsSpec
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test Sound non-negative MergeAddsSpec" IO ()
reportManyNonNegAddsSpec
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test Sound non-negative AddsSpec" Gen Property
testSoundNonNegAddsSpec
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test Sound any AddsSpec" Gen Property
testSoundAddsSpec
]
, String -> [TestTree] -> TestTree
testGroup
String
"PairSpec test"
[ forall a. Testable a => String -> a -> TestTree
testProperty String
"test sound PairSpec" Gen Property
testSoundPairSpec
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test ConsistentPair" Gen Property
testConsistentPair
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test merge PairSpec" Gen Property
testMergePairSpec
, forall a. Testable a => String -> a -> TestTree
testProperty String
"test More consistent PairSpec" IO ()
reportManyMergePairSpec
]
]
main :: IO ()
main :: IO ()
main = TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$ TestTree
allSpecTests
data PairSide = VarOnLeft | VarOnRight
deriving (Int -> PairSide -> ShowS
[PairSide] -> ShowS
PairSide -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PairSide] -> ShowS
$cshowList :: [PairSide] -> ShowS
show :: PairSide -> String
$cshow :: PairSide -> String
showsPrec :: Int -> PairSide -> ShowS
$cshowsPrec :: Int -> PairSide -> ShowS
Show, PairSide -> PairSide -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PairSide -> PairSide -> Bool
$c/= :: PairSide -> PairSide -> Bool
== :: PairSide -> PairSide -> Bool
$c== :: PairSide -> PairSide -> Bool
Eq)
data PairSpec era a b where
PairSpec :: (Ord a, Eq b) => Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairNever :: [String] -> PairSpec era a b
PairAny :: PairSpec era a b
anyPairSpec :: PairSpec era d r -> Bool
anyPairSpec :: forall era d r. PairSpec era d r -> Bool
anyPairSpec PairSpec era d r
PairAny = Bool
True
anyPairSpec (PairSpec Rep era d
_ Rep era r
_ PairSide
_ Map d r
m) = forall k a. Map k a -> Bool
Map.null Map d r
m
anyPairSpec PairSpec era d r
_ = Bool
False
instance Monoid (PairSpec era a b) where
mempty :: PairSpec era a b
mempty = forall era a b. PairSpec era a b
PairAny
instance Semigroup (PairSpec era dom rng) where
<> :: PairSpec era dom rng
-> PairSpec era dom rng -> PairSpec era dom rng
(<>) = forall era a b.
PairSpec era a b -> PairSpec era a b -> PairSpec era a b
mergePairSpec
instance Show (PairSpec era dom rng) where
show :: PairSpec era dom rng -> String
show = forall era dom rng. PairSpec era dom rng -> String
showPairSpec
instance LiftT (PairSpec era dom rng) where
liftT :: PairSpec era dom rng -> Typed (PairSpec era dom rng)
liftT (PairNever [String]
xs) = forall a. [String] -> Typed a
failT [String]
xs
liftT PairSpec era dom rng
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure PairSpec era dom rng
x
dropT :: Typed (PairSpec era dom rng) -> PairSpec era dom rng
dropT (Typed (Left [String]
s)) = forall era a b. [String] -> PairSpec era a b
PairNever [String]
s
dropT (Typed (Right PairSpec era dom rng
x)) = PairSpec era dom rng
x
showPairSpec :: PairSpec era dom rng -> String
showPairSpec :: forall era dom rng. PairSpec era dom rng -> String
showPairSpec (PairNever [String]
_) = String
"PairNever"
showPairSpec PairSpec era dom rng
PairAny = String
"PairAny"
showPairSpec (PairSpec Rep era dom
dom Rep era rng
rng PairSide
side Map dom rng
mp) = [String] -> String
sepsP [String
"PairSpec", forall a. Show a => a -> String
show Rep era dom
dom, forall a. Show a => a -> String
show Rep era rng
rng, forall a. Show a => a -> String
show PairSide
side, forall e t. Rep e t -> t -> String
synopsis (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era dom
dom Rep era rng
rng) Map dom rng
mp]
mergePairSpec :: PairSpec era a b -> PairSpec era a b -> PairSpec era a b
mergePairSpec :: forall era a b.
PairSpec era a b -> PairSpec era a b -> PairSpec era a b
mergePairSpec (PairNever [String]
xs) (PairNever [String]
ys) = forall era a b. [String] -> PairSpec era a b
PairNever ([String]
xs forall a. [a] -> [a] -> [a]
++ [String]
ys)
mergePairSpec d :: PairSpec era a b
d@(PairNever [String]
_) PairSpec era a b
_ = PairSpec era a b
d
mergePairSpec PairSpec era a b
_ d :: PairSpec era a b
d@(PairNever [String]
_) = PairSpec era a b
d
mergePairSpec PairSpec era a b
PairAny PairSpec era a b
x = PairSpec era a b
x
mergePairSpec PairSpec era a b
x PairSpec era a b
PairAny = PairSpec era a b
x
mergePairSpec (PairSpec Rep era a
d Rep era b
r PairSide
VarOnRight Map a b
m1) (PairSpec Rep era a
_ Rep era b
_ PairSide
VarOnRight Map a b
m2) =
let accum :: Either [String] (Map a b) -> a -> b -> Either [String] (Map a b)
accum (Right Map a b
zs) a
key b
v =
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
key Map a b
zs of
Maybe b
Nothing -> forall a b. b -> Either a b
Right (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
key b
v Map a b
zs)
Just b
u ->
if b
u forall a. Eq a => a -> a -> Bool
== b
v
then forall a b. b -> Either a b
Right (Map a b
zs)
else
forall a b. a -> Either a b
Left
[ String
"The PairSpecs with VarOnRight"
, String
" " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
format (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era a
d Rep era b
r) Map a b
m1 forall a. [a] -> [a] -> [a]
++ String
" and"
, String
" " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
format (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era a
d Rep era b
r) Map a b
m2
, String
" are inconsistent."
, String
"The key "
forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era a
d a
key
forall a. [a] -> [a] -> [a]
++ String
" has multiple values: "
forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era b
r b
v
forall a. [a] -> [a] -> [a]
++ String
" and "
forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era b
r b
u
]
accum (Left [String]
xs) a
_ b
_ = forall a b. a -> Either a b
Left [String]
xs
in case forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' Either [String] (Map a b) -> a -> b -> Either [String] (Map a b)
accum (forall a b. b -> Either a b
Right Map a b
m1) Map a b
m2 of
Left [String]
xs -> forall era a b. [String] -> PairSpec era a b
PairNever [String]
xs
Right Map a b
m3 -> forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era a
d Rep era b
r PairSide
VarOnRight Map a b
m3
mergePairSpec (PairSpec Rep era a
d Rep era b
r PairSide
VarOnLeft Map a b
m1) (PairSpec Rep era a
_ Rep era b
_ PairSide
VarOnLeft Map a b
m2) =
let accum :: Either [String] (Map a b) -> a -> b -> Either [String] (Map a b)
accum (Right Map a b
zs) a
key b
v =
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
key Map a b
m1 of
Maybe b
Nothing -> forall a b. b -> Either a b
Right Map a b
zs
Just b
u ->
if b
u forall a. Eq a => a -> a -> Bool
== b
v
then forall a b. b -> Either a b
Right (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
key b
u Map a b
zs)
else
forall a b. a -> Either a b
Left
[ String
"The PairSpecs with VarOnLeft"
, String
" " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
format (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era a
d Rep era b
r) Map a b
m1 forall a. [a] -> [a] -> [a]
++ String
" and"
, String
" " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
format (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era a
d Rep era b
r) Map a b
m2
, String
"are inconsistent."
, String
"The key "
forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era a
d a
key
forall a. [a] -> [a] -> [a]
++ String
" has multiple values: "
forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era b
r b
v
forall a. [a] -> [a] -> [a]
++ String
" and "
forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era a
d Rep era b
r) Map a b
m1
]
accum (Left [String]
xs) a
_ b
_ = forall a b. a -> Either a b
Left [String]
xs
in case forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' Either [String] (Map a b) -> a -> b -> Either [String] (Map a b)
accum (forall a b. b -> Either a b
Right forall k a. Map k a
Map.empty) Map a b
m2 of
Left [String]
xs -> forall era a b. [String] -> PairSpec era a b
PairNever [String]
xs
Right Map a b
m3 -> forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era a
d Rep era b
r PairSide
VarOnLeft Map a b
m3
mergePairSpec PairSpec era a b
a PairSpec era a b
b =
forall era a b. [String] -> PairSpec era a b
PairNever
[ String
"The PairSpecs"
, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era a b
a forall a. [a] -> [a] -> [a]
++ String
" and"
, String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era a b
b
, String
" are inconsistent."
, String
"They have the var on different sides."
]
sizeForPairSpec :: PairSpec era dom rng -> Size
sizeForPairSpec :: forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec era dom rng
PairAny = Size
SzAny
sizeForPairSpec (PairNever [String]
msgs) = [String] -> Size
SzNever ([String]
msgs forall a. [a] -> [a] -> [a]
++ [String
"From sizeForPairSpec."])
sizeForPairSpec (PairSpec Rep era dom
_ Rep era rng
_ PairSide
VarOnRight Map dom rng
m) = Int -> Size
SzLeast (forall k a. Map k a -> Int
Map.size Map dom rng
m)
sizeForPairSpec (PairSpec Rep era dom
_ Rep era rng
_ PairSide
VarOnLeft Map dom rng
m) = Int -> Size
SzMost (forall k a. Map k a -> Int
Map.size Map dom rng
m)
runPairSpec :: (Ord dom, Eq rng) => Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec :: forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map dom rng
_ PairSpec era dom rng
PairAny = Bool
True
runPairSpec Map dom rng
_ (PairNever [String]
xs) = forall a. HasCallStack => String -> [String] -> a
errorMess String
"PairNever in call to runPairSpec" [String]
xs
runPairSpec Map dom rng
m1 (PairSpec Rep era dom
_ Rep era rng
_ PairSide
VarOnRight Map dom rng
m2) = forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
Map.isSubmapOf Map dom rng
m2 Map dom rng
m1
runPairSpec Map dom rng
m1 (PairSpec Rep era dom
_ Rep era rng
_ PairSide
VarOnLeft Map dom rng
m2) = forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
Map.isSubmapOf Map dom rng
m1 Map dom rng
m2
genPairSpec ::
forall era dom rng. (Ord dom, Eq rng) => Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec :: forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec Rep era dom
domr Rep era rng
rngr =
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
[ (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era a b. PairSpec era a b
PairAny)
, (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
domr Rep era rng
rngr PairSide
VarOnRight forall k a. Map k a
Map.empty))
, (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
domr Rep era rng
rngr PairSide
VarOnLeft forall k a. Map k a
Map.empty))
, (Int
4, forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
domr Rep era rng
rngr PairSide
VarOnRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall k a. k -> a -> Map k a
Map.singleton forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era b. Rep era b -> Gen b
genRep Rep era dom
domr forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era b. Rep era b -> Gen b
genRep Rep era rng
rngr))
, (Int
4, forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
domr Rep era rng
rngr PairSide
VarOnLeft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall k a. k -> a -> Map k a
Map.singleton forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era b. Rep era b -> Gen b
genRep Rep era dom
domr forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era b. Rep era b -> Gen b
genRep Rep era rng
rngr))
,
( Int
4
, do
dom
d1 <- forall era b. Rep era b -> Gen b
genRep Rep era dom
domr
dom
d2 <- forall era b. Rep era b -> Gen b
genRep Rep era dom
domr
rng
r1 <- forall era b. Rep era b -> Gen b
genRep Rep era rng
rngr
rng
r2 <- forall era b. Rep era b -> Gen b
genRep Rep era rng
rngr
forall a. HasCallStack => [a] -> Gen a
elements
[ forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
domr Rep era rng
rngr PairSide
VarOnRight (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(dom
d1, rng
r1), (dom
d2, rng
r2)])
, forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
domr Rep era rng
rngr PairSide
VarOnRight (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(dom
d1, rng
r1), (dom
d2, rng
r2)])
]
)
]
fixSide :: PairSide -> PairSpec era a b -> PairSpec era a b
fixSide :: forall era a b. PairSide -> PairSpec era a b -> PairSpec era a b
fixSide PairSide
_ (PairNever [String]
xs) = forall era a b. [String] -> PairSpec era a b
PairNever [String]
xs
fixSide PairSide
_ PairSpec era a b
PairAny = forall era a b. PairSpec era a b
PairAny
fixSide PairSide
side (PairSpec Rep era a
d Rep era b
r PairSide
_ Map a b
m) = forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era a
d Rep era b
r PairSide
side Map a b
m
genConsistentPairSpec ::
(Ord dom, Eq rng) =>
Rep era dom ->
Rep era rng ->
PairSpec era dom rng ->
Gen (PairSpec era dom rng)
genConsistentPairSpec :: forall dom rng era.
(Ord dom, Eq rng) =>
Rep era dom
-> Rep era rng
-> PairSpec era dom rng
-> Gen (PairSpec era dom rng)
genConsistentPairSpec Rep era dom
_domr Rep era rng
_rngr (PairNever [String]
xs) = forall a. HasCallStack => String -> [String] -> a
errorMess String
"PairNever in genConsistentPairSpec" [String]
xs
genConsistentPairSpec Rep era dom
domr Rep era rng
rngr PairSpec era dom rng
PairAny = forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec Rep era dom
domr Rep era rng
rngr
genConsistentPairSpec Rep era dom
domr Rep era rng
rngr (PairSpec Rep era dom
_d Rep era rng
_r PairSide
VarOnRight Map dom rng
m) | forall k a. Map k a -> Bool
Map.null Map dom rng
m = forall era a b. PairSide -> PairSpec era a b -> PairSpec era a b
fixSide PairSide
VarOnRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec Rep era dom
domr Rep era rng
rngr
genConsistentPairSpec Rep era dom
domr Rep era rng
rngr (PairSpec Rep era dom
_d Rep era rng
_r PairSide
VarOnLeft Map dom rng
m) | forall k a. Map k a -> Bool
Map.null Map dom rng
m = forall era a b. PairSide -> PairSpec era a b -> PairSpec era a b
fixSide PairSide
VarOnLeft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec Rep era dom
domr Rep era rng
rngr
genConsistentPairSpec Rep era dom
_ Rep era rng
_ (PairSpec Rep era dom
d Rep era rng
r PairSide
VarOnRight Map dom rng
m) =
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
[ (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era a b. PairSpec era a b
PairAny)
, (Int
1, do Int
n <- forall a. Random a => (a, a) -> Gen a
choose (Int
0, forall k a. Map k a -> Int
Map.size Map dom rng
m forall a. Num a => a -> a -> a
- Int
1); forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
d Rep era rng
r PairSide
VarOnRight (forall k a. Int -> Map k a -> Map k a
Map.deleteAt Int
n Map dom rng
m)))
,
( Int
1
, do
dom
d1 <- forall a. [String] -> Gen a -> (a -> Bool) -> Gen a
suchThatErr [String
"genConsistentPairSpec"] (forall era b. Rep era b -> Gen b
genRep Rep era dom
d) (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map dom rng
m))
rng
r1 <- forall era b. Rep era b -> Gen b
genRep Rep era rng
r
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
d Rep era rng
r PairSide
VarOnRight (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert dom
d1 rng
r1 Map dom rng
m))
)
]
genConsistentPairSpec Rep era dom
_ Rep era rng
_ (PairSpec Rep era dom
d Rep era rng
r PairSide
VarOnLeft Map dom rng
m) =
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
[ (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era a b. PairSpec era a b
PairAny)
, (Int
1, do Int
n <- forall a. Random a => (a, a) -> Gen a
choose (Int
0, forall k a. Map k a -> Int
Map.size Map dom rng
m forall a. Num a => a -> a -> a
- Int
1); forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
d Rep era rng
r PairSide
VarOnLeft (forall k a. Int -> Map k a -> Map k a
Map.deleteAt Int
n Map dom rng
m)))
,
( Int
1
, do
dom
d1 <- forall a. [String] -> Gen a -> (a -> Bool) -> Gen a
suchThatErr [String
"genConsistentPairSpec"] (forall era b. Rep era b -> Gen b
genRep Rep era dom
d) (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map dom rng
m))
rng
r1 <- forall era b. Rep era b -> Gen b
genRep Rep era rng
r
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
d Rep era rng
r PairSide
VarOnLeft (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert dom
d1 rng
r1 Map dom rng
m))
)
]
genFromPairSpec ::
forall era dom rng. Ord dom => [String] -> PairSpec era dom rng -> Gen (Map dom rng)
genFromPairSpec :: forall era dom rng.
Ord dom =>
[String] -> PairSpec era dom rng -> Gen (Map dom rng)
genFromPairSpec [String]
msgs (PairNever [String]
xs) = forall a. HasCallStack => String -> [String] -> a
errorMess String
"genFromPairSpec failed due to PairNever" ([String]
msgs forall a. [a] -> [a] -> [a]
++ [String]
xs)
genFromPairSpec [String]
_msgs PairSpec era dom rng
PairAny = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Map k a
Map.empty
genFromPairSpec [String]
msgs p :: PairSpec era dom rng
p@(PairSpec Rep era dom
domr Rep era rng
rngr PairSide
VarOnRight Map dom rng
mp) = do
Int
n <- (forall a. Num a => a -> a -> a
+ (forall k a. Map k a -> Int
Map.size Map dom rng
mp)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
10)
forall a b.
Ord a =>
[String] -> Map a b -> Int -> Gen a -> Gen b -> Gen (Map a b)
mapFromSubset ([String]
msgs forall a. [a] -> [a] -> [a]
++ [String
"genFromPairSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era dom rng
p]) Map dom rng
mp Int
n (forall era b. Rep era b -> Gen b
genRep Rep era dom
domr) (forall era b. Rep era b -> Gen b
genRep Rep era rng
rngr)
genFromPairSpec [String]
msgs (PairSpec Rep era dom
_domr Rep era rng
_rngr PairSide
VarOnLeft Map dom rng
mp) = do
Set dom
domset <- forall a. Ord a => [String] -> Set a -> Gen (Set a)
subsetFromSet ([String]
msgs forall a. [a] -> [a] -> [a]
++ [String
"from genFromPairSpec VarOnLeft"]) (forall k a. Map k a -> Set k
Map.keysSet Map dom rng
mp)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map dom rng
mp Set dom
domset)
testConsistentPair :: Gen Property
testConsistentPair :: Gen Property
testConsistentPair = do
PairSpec BabbageEra Int Int
s1 <- forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec @BabbageEra forall era. Rep era Int
IntR forall era. Rep era Int
IntR
PairSpec BabbageEra Int Int
s2 <- forall dom rng era.
(Ord dom, Eq rng) =>
Rep era dom
-> Rep era rng
-> PairSpec era dom rng
-> Gen (PairSpec era dom rng)
genConsistentPairSpec forall era. Rep era Int
IntR forall era. Rep era Int
IntR PairSpec BabbageEra Int Int
s1
case PairSpec BabbageEra Int Int
s1 forall a. Semigroup a => a -> a -> a
<> PairSpec BabbageEra Int Int
s2 of
PairNever [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
"genConsistentPair fails", forall a. Show a => a -> String
show PairSpec BabbageEra Int Int
s1, forall a. Show a => a -> String
show PairSpec BabbageEra Int Int
s2] forall a. [a] -> [a] -> [a]
++ [String]
ms)) Bool
False
PairSpec BabbageEra Int 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
testSoundPairSpec :: Gen Property
testSoundPairSpec :: Gen Property
testSoundPairSpec = do
PairSpec BabbageEra Int Word64
s1 <- forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec forall era. Rep era Int
IntR forall era. Rep era Word64
Word64R
Map Int Word64
ans <- forall era dom rng.
Ord dom =>
[String] -> PairSpec era dom rng -> Gen (Map dom rng)
genFromPairSpec @BabbageEra [String
"testSoundPairSpec"] PairSpec BabbageEra Int 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 PairSpec BabbageEra Int Word64
s1 forall a. [a] -> [a] -> [a]
++ String
"\nans=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Map Int Word64
ans) (forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map Int Word64
ans PairSpec BabbageEra Int Word64
s1)
testMergePairSpec :: Gen Property
testMergePairSpec :: Gen Property
testMergePairSpec = do
PairSpec BabbageEra Word64 Int
s1 <- forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec forall era. Rep era Word64
Word64R forall era. Rep era Int
IntR
PairSpec BabbageEra Word64 Int
s2 <- forall dom rng era.
(Ord dom, Eq rng) =>
Rep era dom
-> Rep era rng
-> PairSpec era dom rng
-> Gen (PairSpec era dom rng)
genConsistentPairSpec forall era. Rep era Word64
Word64R forall era. Rep era Int
IntR PairSpec BabbageEra Word64 Int
s1
case PairSpec BabbageEra Word64 Int
s1 forall a. Semigroup a => a -> a -> a
<> PairSpec BabbageEra Word64 Int
s2 of
PairNever [String]
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall prop. Testable prop => prop -> Property
property Bool
True)
PairSpec BabbageEra Word64 Int
s4 -> do
Map Word64 Int
ans <- forall era dom rng.
Ord dom =>
[String] -> PairSpec era dom rng -> Gen (Map dom rng)
genFromPairSpec @BabbageEra [String
"testMergePairSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec BabbageEra Word64 Int
s1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec BabbageEra Word64 Int
s2] PairSpec BabbageEra Word64 Int
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 PairSpec BabbageEra Word64 Int
s1
forall a. [a] -> [a] -> [a]
++ String
"\ns2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec BabbageEra Word64 Int
s2
forall a. [a] -> [a] -> [a]
++ String
"\ns1<>s2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec BabbageEra Word64 Int
s4
forall a. [a] -> [a] -> [a]
++ String
"\nans="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Map Word64 Int
ans
forall a. [a] -> [a] -> [a]
++ String
"\nrun s1="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map Word64 Int
ans PairSpec BabbageEra Word64 Int
s1)
forall a. [a] -> [a] -> [a]
++ String
"\nrun s2="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map Word64 Int
ans PairSpec BabbageEra Word64 Int
s2)
forall a. [a] -> [a] -> [a]
++ String
"\nrun s4="
forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map Word64 Int
ans PairSpec BabbageEra Word64 Int
s4)
)
(forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map Word64 Int
ans PairSpec BabbageEra Word64 Int
s4 Bool -> Bool -> Bool
&& forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map Word64 Int
ans PairSpec BabbageEra Word64 Int
s2 Bool -> Bool -> Bool
&& forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map Word64 Int
ans PairSpec BabbageEra Word64 Int
s1)
manyMergePairSpec :: Gen (Int, [String])
manyMergePairSpec :: Gen (Int, [String])
manyMergePairSpec = do
[PairSpec BabbageEra Word64 Int]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
60 (forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec forall era. Rep era Word64
Word64R forall era. Rep era Int
IntR)
[PairSpec BabbageEra Word64 Int]
ys <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
60 (forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec forall era. Rep era Word64
Word64R forall era. Rep era Int
IntR)
let ok :: PairSpec era a b -> Bool
ok PairSpec era a b
PairAny = Bool
False
ok PairSpec era a b
_ = Bool
True
check :: (PairSpec era dom rng, PairSpec era dom rng,
PairSpec BabbageEra dom rng)
-> Gen
(PairSpec era dom rng, Bool, PairSpec era dom rng, Bool,
Map dom rng, Bool, PairSpec BabbageEra dom rng)
check (PairSpec era dom rng
x, PairSpec era dom rng
y, PairSpec BabbageEra dom rng
m) = do
let size :: Size
size = forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec BabbageEra dom rng
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 rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec BabbageEra dom rng
m)
, String
"s1<>s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec BabbageEra dom rng
m
, String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec era dom rng
x)
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era dom rng
x
, String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec era dom rng
y)
, String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era dom rng
y
, String
"GenFromPairSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
]
Map dom rng
z <- forall era dom rng.
Ord dom =>
[String] -> PairSpec era dom rng -> Gen (Map dom rng)
genFromPairSpec @BabbageEra [String]
wordsX PairSpec BabbageEra dom rng
m
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PairSpec era dom rng
x, forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map dom rng
z PairSpec era dom rng
x, PairSpec era dom rng
y, forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map dom rng
z PairSpec era dom rng
y, Map dom rng
z, forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map dom rng
z PairSpec BabbageEra dom rng
m, PairSpec BabbageEra dom rng
m)
showAns :: (PairSpec era dom rng, a, PairSpec era dom rng, a, a, a,
PairSpec era dom rng)
-> String
showAns (PairSpec era dom rng
s1, a
run1, PairSpec era dom rng
s2, a
run2, a
v, a
run3, PairSpec era dom rng
s3) =
[String] -> String
unlines
[ String
"\ns1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era dom rng
s1
, String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec era dom rng
s1)
, String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era dom rng
s2
, String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec era dom rng
s2)
, String
"s1 <> s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era dom rng
s3
, String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec era dom rng
s3)
, String
"v = genFromPairSpec (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
v
, String
"runPairSpec v s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run1
, String
"runPairSpec v s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run2
, String
"runPairSpec v (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run3
]
pr :: (PairSpec era dom rng, Bool, PairSpec era dom rng, Bool, a, Bool,
PairSpec era dom rng)
-> Maybe String
pr x :: (PairSpec era dom rng, Bool, PairSpec era dom rng, Bool, a, Bool,
PairSpec era dom rng)
x@(PairSpec era dom rng
_, Bool
a, PairSpec era dom rng
_, Bool
b, a
_, Bool
c, PairSpec era dom rng
_) = 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} {rng} {era} {dom} {rng} {era}
{dom} {rng}.
(Show a, Show a, Show a, Show a) =>
(PairSpec era dom rng, a, PairSpec era dom rng, a, a, a,
PairSpec era dom rng)
-> String
showAns (PairSpec era dom rng, Bool, PairSpec era dom rng, Bool, a, Bool,
PairSpec era dom rng)
x) else forall a. Maybe a
Nothing
let trips :: [(PairSpec BabbageEra Word64 Int, PairSpec BabbageEra Word64 Int,
PairSpec BabbageEra Word64 Int)]
trips = [(PairSpec BabbageEra Word64 Int
x, PairSpec BabbageEra Word64 Int
y, PairSpec BabbageEra Word64 Int
m) | PairSpec BabbageEra Word64 Int
x <- [PairSpec BabbageEra Word64 Int]
xs, PairSpec BabbageEra Word64 Int
y <- [PairSpec BabbageEra Word64 Int]
ys, forall era d r. PairSpec era d r -> Bool
ok PairSpec BabbageEra Word64 Int
x Bool -> Bool -> Bool
&& forall era d r. PairSpec era d r -> Bool
ok PairSpec BabbageEra Word64 Int
y, Just PairSpec BabbageEra Word64 Int
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent PairSpec BabbageEra Word64 Int
x PairSpec BabbageEra Word64 Int
y]]
[(PairSpec BabbageEra Word64 Int, Bool,
PairSpec BabbageEra Word64 Int, Bool, Map Word64 Int, Bool,
PairSpec BabbageEra Word64 Int)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {dom} {rng} {era} {era}.
(Ord dom, Eq rng) =>
(PairSpec era dom rng, PairSpec era dom rng,
PairSpec BabbageEra dom rng)
-> Gen
(PairSpec era dom rng, Bool, PairSpec era dom rng, Bool,
Map dom rng, Bool, PairSpec BabbageEra dom rng)
check [(PairSpec BabbageEra Word64 Int, PairSpec BabbageEra Word64 Int,
PairSpec BabbageEra Word64 Int)]
trips
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(PairSpec BabbageEra Word64 Int, PairSpec BabbageEra Word64 Int,
PairSpec BabbageEra Word64 Int)]
trips, forall a b. (a -> Maybe b) -> [a] -> [b]
Maybe.mapMaybe forall {a} {era} {dom} {rng} {era} {dom} {rng} {era} {dom} {rng}.
Show a =>
(PairSpec era dom rng, Bool, PairSpec era dom rng, Bool, a, Bool,
PairSpec era dom rng)
-> Maybe String
pr [(PairSpec BabbageEra Word64 Int, Bool,
PairSpec BabbageEra Word64 Int, Bool, Map Word64 Int, Bool,
PairSpec BabbageEra Word64 Int)]
ts)
reportManyMergePairSpec :: IO ()
reportManyMergePairSpec :: IO ()
reportManyMergePairSpec = do
(Int
passed, [String]
bad) <- forall a. Gen a -> IO a
generate Gen (Int, [String])
manyMergePairSpec
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")
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"