{-# 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 #-}

-- | A 'Spec' is a first order data structure that denotes a random generator
--   For example
--   (MapSpec era dom rng) denotes Gen(Map dom rng)
--   (RngSpec era t)       denotes Gen[t]  where the [t] has some Summing properties
--   (RelSep era t)        denotes Gen(Set t) where the set meets some relational properties
--   (Size)                denotes Gen Int, the size of some Map, Set, List etc.
--   (PairSpec era d r)    denotes (([d],[r]) -> ([d],[r])) a transformer
module Test.Cardano.Ledger.Constrained.Spec where

import Cardano.Ledger.Coin (Coin (..), DeltaCoin (..))
import Cardano.Ledger.Core (Era (..))
import qualified Data.List as List
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import qualified Data.Maybe as Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Word (Word64)
import qualified Debug.Trace as Debug
import Lens.Micro hiding (set)
import Test.Cardano.Ledger.Constrained.Ast (Pred (..), Sum (..), Term (..), runPred)
import Test.Cardano.Ledger.Constrained.Classes (
  Adds (..),
  AddsSpec (..),
  OrdCond (..),
  genFromAddsSpec,
  genFromNonNegAddsSpec,
  lensAdds,
  sumAdds,
  varOnLeft,
  varOnRight,
 )
import Test.Cardano.Ledger.Constrained.Combinators (
  addUntilSize,
  errorMess,
  fixSet,
  mapFromSubset,
  setSized,
  subMapFromMapWithSize,
  subsetFromSet,
  suchThatErr,
  superSetFromSet,
  superSetFromSetWithSize,
 )
import Test.Cardano.Ledger.Constrained.Env (Access (No), V (..), emptyEnv, storeVar)
import Test.Cardano.Ledger.Constrained.Monad
import Test.Cardano.Ledger.Constrained.Size (
  Size (..),
  atLeastDelta,
  atMostAny,
  genFromIntRange,
  genFromNonNegIntRange,
  genFromSize,
  runSize,
  seps,
  sepsP,
 )
import Test.Cardano.Ledger.Constrained.TypeRep (
  Rep (..),
  format,
  genRep,
  synopsis,
 )
import Test.Cardano.Ledger.Core.Arbitrary ()
import Test.Cardano.Ledger.Generic.Proof (BabbageEra, Standard)
import Test.Cardano.Ledger.Shelley.Serialisation.EraIndepGenerators ()
import Test.Tasty
import Test.Tasty.QuickCheck hiding (total)

type TestEra = BabbageEra Standard

data SomeLens era t where
  SomeLens :: Adds c => (Lens' t c) -> SomeLens era t

-- ===========================================================
{- TODO, possible extensions and improvements, so we don't forget
1) Redo Size with: data Size = SzNever [String] | SzRange Int (Maybe Int) Move to own file
2) Add newtype Never = Never [String], then instead of (XXXNever xs) we use (XX (Never xs))
3) class Specify
4) A better story about fields in constraints. Maybe add FieldSpec type.
-}

-- =========================================================

-- | used when we run tests, and we have to pick some concrete Era
type TT = BabbageEra Standard

-- ============================================================
-- Operators for Size (Defined in TypeRep.hs)

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

-- | Generate a Size with all positive numbers, This is used where
--   we want Size to denote things that must be >= 0. Coin, Word64, Natural
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))
    ]

-- | Generate a Size denoting an Int range, across both positive
--   and negative numbers. DeltaCoin, Int, Rational. This is used
--   when we use Size to denote OrdCond on types with negative values
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))
    , -- , (1, SzMost <$> choose (n+60,n+90)) -- Without context, it is impossible to tell how big is OK
      (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)

-- =====================================================
-- RelSpec

data RelSpec era dom where
  RelAny ::
    -- | There is no restriction on the set. Denotes the universe.
    RelSpec era dom
  RelNever ::
    -- | Something is inconsistent
    [String] ->
    RelSpec era dom
  -- | Denotes things like: (x == y) equality, (x ⊆ y) subset, ( x ∩ y = ∅) disjointness, (x ⊇ y) superset.
  --   Invariants of r@(RepOper must (Just may) cant)
  -- 1) must is a subset of may
  -- 2) must and may are disjoint from cant
  -- 3) (sizeFromRel r) is realizable E.g.  (SzRng 10 3) is NOT realizable
  RelOper ::
    Ord d =>
    Rep era d ->
    -- | Must set
    Set d ->
    -- | May set, Nothing denotes the universe
    Maybe (Set d) ->
    -- | Can't set
    Set d ->
    RelSpec era d
  -- RelLens :: Ord b => Lens' dom b -> Rep era dom -> Rep era b -> Set b -> RelSpec era dom
  -- Try this
  RelLens :: Ord b => Lens' dom b -> Rep era dom -> Rep era b -> (RelSpec era b) -> RelSpec era dom

relSubset, relSuperset, relDisjoint, relEqual :: Ord t => Rep era t -> Set t -> RelSpec era t
relSubset :: forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSubset Rep era t
r Set t
set = forall d era.
Ord d =>
Rep era d -> Set d -> Maybe (Set d) -> Set d -> RelSpec era d
RelOper Rep era t
r forall a. Set a
Set.empty (forall a. a -> Maybe a
Just Set t
set) forall a. Set a
Set.empty
relSuperset :: forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relSuperset Rep era t
r Set t
set = forall d era.
Ord d =>
Rep era d -> Set d -> Maybe (Set d) -> Set d -> RelSpec era d
RelOper Rep era t
r Set t
set forall a. Maybe a
Nothing forall a. Set a
Set.empty
relDisjoint :: forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relDisjoint Rep era t
r Set t
set = forall d era.
Ord d =>
Rep era d -> Set d -> Maybe (Set d) -> Set d -> RelSpec era d
RelOper Rep era t
r forall a. Set a
Set.empty forall a. Maybe a
Nothing Set t
set
relEqual :: forall t era. Ord t => Rep era t -> Set t -> RelSpec era t
relEqual Rep era t
r Set t
set = forall d era.
Ord d =>
Rep era d -> Set d -> Maybe (Set d) -> Set d -> RelSpec era d
RelOper Rep era t
r Set t
set (forall a. a -> Maybe a
Just Set t
set) forall a. Set a
Set.empty

instance Monoid (RelSpec era dom) where
  mempty :: RelSpec era dom
mempty = forall era dom. RelSpec era dom
RelAny

instance Semigroup (RelSpec era dom) where
  <> :: RelSpec era dom -> RelSpec era dom -> RelSpec era dom
(<>) = forall era dom.
RelSpec era dom -> RelSpec era dom -> RelSpec era dom
mergeRelSpec

instance Show (RelSpec era dom) where
  show :: RelSpec era dom -> String
show = forall era dom. RelSpec era dom -> String
showRelSpec

instance LiftT (RelSpec era a) where
  liftT :: RelSpec era a -> Typed (RelSpec era a)
liftT (RelNever [String]
xs) = forall a. [String] -> Typed a
failT [String]
xs
  liftT RelSpec era a
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure RelSpec era a
x
  dropT :: Typed (RelSpec era a) -> RelSpec era a
dropT (Typed (Left [String]
s)) = forall era dom. [String] -> RelSpec era dom
RelNever [String]
s
  dropT (Typed (Right RelSpec era a
x)) = RelSpec era a
x

showRelSpec :: RelSpec era dom -> String
showRelSpec :: forall era dom. RelSpec era dom -> String
showRelSpec RelSpec era dom
RelAny = String
"RelAny"
showRelSpec (RelOper Rep era dom
r Set dom
x (Just Set dom
s) Set dom
y) | forall a. Set a -> Bool
Set.null Set dom
y Bool -> Bool -> Bool
&& Set dom
x forall a. Eq a => a -> a -> Bool
== Set dom
s = [String] -> String
sepsP [String
"RelEqual", forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
x]
showRelSpec (RelOper Rep era dom
r Set dom
x (Just Set dom
s) Set dom
y) | forall a. Set a -> Bool
Set.null Set dom
x Bool -> Bool -> Bool
&& forall a. Set a -> Bool
Set.null Set dom
y = [String] -> String
sepsP [String
"RelSubset", forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
s]
showRelSpec (RelOper Rep era dom
r Set dom
x Maybe (Set dom)
Nothing Set dom
y) | forall a. Set a -> Bool
Set.null Set dom
y = [String] -> String
sepsP [String
"RelSuperset", forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
x]
showRelSpec (RelOper Rep era dom
r Set dom
x Maybe (Set dom)
Nothing Set dom
y) | forall a. Set a -> Bool
Set.null Set dom
x = [String] -> String
sepsP [String
"RelDisjoint", forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
y]
showRelSpec (RelOper Rep era dom
r Set dom
x Maybe (Set dom)
Nothing Set dom
y) = [String] -> String
sepsP [String
"RelOper", forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
x, String
"Univ", forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
y]
showRelSpec (RelOper Rep era dom
r Set dom
x (Just Set dom
y) Set dom
z) = [String] -> String
sepsP [String
"RelOper", forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
x, forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
y, forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era dom
r) Set dom
z]
showRelSpec (RelLens Lens' dom b
_ Rep era dom
repd Rep era b
repb RelSpec era b
relsp) = [String] -> String
sepsP [String
"RelLens", String
"(Lens' " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era dom
repd forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era b
repb forall a. [a] -> [a] -> [a]
++ String
")", forall a. Show a => a -> String
show RelSpec era b
relsp]
showRelSpec (RelNever [String]
_) = String
"RelNever"

mergeRelSpec :: RelSpec era d -> RelSpec era d -> RelSpec era d
mergeRelSpec :: forall era dom.
RelSpec era dom -> RelSpec era dom -> RelSpec era dom
mergeRelSpec (RelNever [String]
xs) (RelNever [String]
ys) = forall era dom. [String] -> RelSpec era dom
RelNever ([String]
xs forall a. [a] -> [a] -> [a]
++ [String]
ys)
mergeRelSpec d :: RelSpec era d
d@(RelNever [String]
_) RelSpec era d
_ = RelSpec era d
d
mergeRelSpec RelSpec era d
_ d :: RelSpec era d
d@(RelNever [String]
_) = RelSpec era d
d
mergeRelSpec RelSpec era d
RelAny RelSpec era d
x = RelSpec era d
x
mergeRelSpec RelSpec era d
x RelSpec era d
RelAny = RelSpec era d
x
mergeRelSpec RelSpec era d
x y :: RelSpec era d
y@RelLens {} = forall era dom.
RelSpec era dom -> RelSpec era dom -> RelSpec era dom
mergeRelSpec RelSpec era d
y RelSpec era d
x
mergeRelSpec a :: RelSpec era d
a@RelLens {} RelSpec era d
b =
  forall era dom. [String] -> RelSpec era dom
RelNever
    [ String
"merging a=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era d
a forall a. [a] -> [a] -> [a]
++ String
"\n        b=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era d
b
    , String
"RelLens is inconsistent with everything, and can't be merged."
    ]
mergeRelSpec a :: RelSpec era d
a@(RelOper Rep era d
r Set d
must1 Maybe (Set d)
may1 Set d
cant1) b :: RelSpec era d
b@(RelOper Rep era d
_ Set d
must2 Maybe (Set d)
may2 Set d
cant2) =
  forall x. LiftT x => Typed x -> x
dropT forall a b. (a -> b) -> a -> b
$
    forall a. String -> Typed a -> Typed a
explain (String
"merging a=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era d
a forall a. [a] -> [a] -> [a]
++ String
"\n        b=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era d
b) forall a b. (a -> b) -> a -> b
$
      forall a. [(Bool, [String])] -> Typed a -> Typed a
requireAll
        [
          ( forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set d
must1 Set d
cant2
          ,
            [ String
"The 'must' set of a("
                forall a. [a] -> [a] -> [a]
++ forall t era. Ord t => Rep era t -> Set t -> String
synSet Rep era d
r Set d
must1
                forall a. [a] -> [a] -> [a]
++ String
") is not disjoint from the 'cant' set of b("
                forall a. [a] -> [a] -> [a]
++ forall t era. Ord t => Rep era t -> Set t -> String
synSet Rep era d
r Set d
cant2
            ]
          )
        ,
          ( forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set d
must2 Set d
cant1
          ,
            [ String
"The 'must' set of b("
                forall a. [a] -> [a] -> [a]
++ forall t era. Ord t => Rep era t -> Set t -> String
synSet Rep era d
r Set d
must2
                forall a. [a] -> [a] -> [a]
++ String
") is not disjoint from the 'cant' set of a("
                forall a. [a] -> [a] -> [a]
++ forall t era. Ord t => Rep era t -> Set t -> String
synSet Rep era d
r Set d
cant1
            ]
          )
        ]
        (forall d era.
Ord d =>
Rep era d
-> Set d -> Maybe (Set d) -> Set d -> Typed (RelSpec era d)
relOper Rep era d
r Set d
must Maybe (Set d)
may Set d
cant)
  where
    must :: Set d
must = forall a. Ord a => Set a -> Set a -> Set a
Set.union Set d
must1 Set d
must2
    cant :: Set d
cant = forall a. Ord a => Set a -> Set a -> Set a
Set.union Set d
cant1 Set d
cant2
    may :: Maybe (Set d)
may = (forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set d
cant) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Ord a => Maybe (Set a) -> Maybe (Set a) -> Maybe (Set a)
interSectM Maybe (Set d)
may1 Maybe (Set d)
may2

-- ==================
-- Helper functions for defining mergeRelSpec and
-- for testing and maintaining RelSpec invariants

-- | The interpretation of (Just set) is set, and of Nothing is the universe (all possible sets)
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)

-- | Test if 's1' is a subset of 's2'
--   Recall, if s2==Nothing, then it denotes the universe
--   and every set is a subset of the universe.
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

-- | Compute the Size that bounds the Size of a set generated from a RelSpec
sizeForRel :: RelSpec era dom -> Size
sizeForRel :: forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era dom
RelAny = Size
SzAny
sizeForRel (RelNever [String]
_) = Size
SzAny
sizeForRel (RelOper Rep era dom
_ Set dom
must Maybe (Set dom)
Nothing Set dom
_) = Int -> Size
SzLeast (forall a. Set a -> Int
Set.size Set dom
must)
sizeForRel (RelOper Rep era dom
_ Set dom
must (Just Set dom
may) Set dom
_) | forall a. Set a -> Bool
Set.null Set dom
must = Int -> Size
SzMost (forall a. Set a -> Int
Set.size Set dom
may)
sizeForRel (RelOper Rep era dom
_ Set dom
must (Just Set dom
may) Set dom
cant) = Int -> Int -> Size
SzRng (forall a. Set a -> Int
Set.size Set dom
must) (forall a. Set a -> Int
Set.size (forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set dom
may Set dom
cant))
sizeForRel (RelLens Lens' dom b
_ Rep era dom
_ Rep era b
_ RelSpec era b
spec) = forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era b
spec

maybeSynopsis :: Rep e t -> Maybe t -> String
maybeSynopsis :: forall e t. Rep e t -> Maybe t -> String
maybeSynopsis Rep e t
r (Just t
x) = forall e t. Rep e t -> t -> String
format Rep e t
r t
x
maybeSynopsis Rep e t
_ Maybe t
_ = String
""

synSet :: Ord t => Rep era t -> Set t -> String
synSet :: forall t era. Ord t => Rep era t -> Set t -> String
synSet Rep era t
r Set t
s = forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era t
r) Set t
s

-- | Check that RelSpec invariants on the constructor RelOper hold on: spec@(RelOper must may cant)
--   1)  must ⊆ may, checked by 'univSubset must may'
--   2)  (must ∩ cant = ∅), checked by 'Set.disjoint must cant'
--   3)  Set.size must <= Set.size (Set.difference may cant), checked by 'okSize spec'
relOper :: Ord d => Rep era d -> Set d -> Maybe (Set d) -> Set d -> Typed (RelSpec era d)
relOper :: forall d era.
Ord d =>
Rep era d
-> Set d -> Maybe (Set d) -> Set d -> Typed (RelSpec era d)
relOper Rep era d
r Set d
must Maybe (Set d)
may Set d
cant =
  let potential :: RelSpec era d
potential = forall d era.
Ord d =>
Rep era d -> Set d -> Maybe (Set d) -> Set d -> RelSpec era d
RelOper Rep era d
r Set d
must Maybe (Set d)
may Set d
cant
   in forall a. String -> Typed a -> Typed a
explain
        (String
"Checking RelSpec self consistency\n   " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall d era.
Ord d =>
Rep era d -> Set d -> Maybe (Set d) -> Set d -> RelSpec era d
RelOper Rep era d
r Set d
must Maybe (Set d)
may Set d
cant))
        ( forall a. [(Bool, [String])] -> Typed a -> Typed a
requireAll
            [
              ( forall a. Ord a => Set a -> Maybe (Set a) -> Bool
univSubset Set d
must Maybe (Set d)
may
              ,
                [ String
"'must' "
                    forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
format (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era d
r) Set d
must
                    forall a. [a] -> [a] -> [a]
++ String
" Is not a subset of: 'may' "
                    forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> Maybe t -> String
maybeSynopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era d
r) Maybe (Set d)
may
                ]
              )
            ,
              ( forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set d
must Set d
cant
              ,
                [ String
"'must' "
                    forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era d
r) Set d
must
                    forall a. [a] -> [a] -> [a]
++ String
"Is not disjoint from: 'cant' "
                    forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era d
r) Set d
cant
                ]
              )
            ,
              ( forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (\Set d
may' -> forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set d
may' Set d
cant) Maybe (Set d)
may
              ,
                [ String
"'may' "
                    forall a. [a] -> [a] -> [a]
++ forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"Nothing" (forall e t. Rep e t -> t -> String
synopsis forall a b. (a -> b) -> a -> b
$ forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era d
r) Maybe (Set d)
may
                    forall a. [a] -> [a] -> [a]
++ String
"Is not disjoint from: 'cant' "
                    forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era d
r) Set d
cant
                ]
              )
            ,
              ( forall era d. RelSpec era d -> Bool
okSize RelSpec era d
potential
              , case RelSpec era d
potential of
                  rel :: RelSpec era d
rel@(RelOper Rep era d
_ Set d
_ (Just Set d
mayJ) Set d
_) ->
                    [ forall a. Show a => a -> String
show RelSpec era d
potential forall a. [a] -> [a] -> [a]
++ String
" has unrealizable size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era d
rel)
                    , String
"size must("
                        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Set a -> Int
Set.size Set d
must)
                        forall a. [a] -> [a] -> [a]
++ String
") > size(mayJ - cant)("
                        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Set a -> Int
Set.size (forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set d
mayJ Set d
cant))
                        forall a. [a] -> [a] -> [a]
++ String
")"
                    ]
                  RelSpec era d
_ -> []
              )
            ]
            (forall (f :: * -> *) a. Applicative f => a -> f a
pure RelSpec era d
potential)
        )

-- ==============================================
-- The standard operations on RelSpec
-- runRelSpec, genFromRelSpec, genRelSpec

-- | test that a set 's' meets the RelSpec
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

-- | return a generator that always generates things that meet the RelSpec
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 -- The is the (relEqual r s) case
        RelOper Rep era t
_ Set t
must Maybe (Set t)
Nothing Set t
dis ->
          -- add things (not in cant) to 'must' until you get to size 'n'
          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 -- add things (from choices) to 'must' until you get to size 'n'
              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
          -- This case supercedes the "projOnDom" function.
          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
          -- Generate (Set B), we will use these, to fixup a (Set D)
          -- where we overwrite the B field of D
          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 -- Generate the D
                  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
          -- Overwrite the B field of D, and insert the changed value D{B=b}
          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

-- | Generate a random RelSpec
--   We deliberately do NOT generate RelLens, as it is inconsistent with everything.
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)
    ]

-- | Generate another set which is disjoint from the input 'set'
--   Note that the empty set is always a solution.
--   These sets tend to be rather small (size <= atLeastDelta)
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)

-- | Generate another RelSpec, guaranteed to be consistent with the input
--   Where (consistent a b) means:  (a <> b) =/= (RelNever _)
--   See the property test 'genConsistent'
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

-- ==================
-- Actual property tests for Relpec

testConsistentRel :: Gen Property
testConsistentRel :: Gen Property
testConsistentRel = do
  Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
3, Int
10)
  RelSpec Any Int
s1 <- forall dom era.
Ord dom =>
[String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec [String
"testConsistentRel " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n] (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
10000)) forall era. Rep era Int
IntR Int
n
  RelSpec Any Int
s2 <- forall dom era.
[String] -> Gen dom -> RelSpec era dom -> Gen (RelSpec era dom)
genConsistentRelSpec [String
"testConsistentRel " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec Any Int
s1] (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
1000)) RelSpec Any Int
s1
  case RelSpec Any Int
s1 forall a. Semigroup a => a -> a -> a
<> RelSpec Any Int
s2 of
    RelNever [String]
ms -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines ([String
"genConsistent fails", forall a. Show a => a -> String
show RelSpec Any Int
s1, forall a. Show a => a -> String
show RelSpec Any Int
s2] forall a. [a] -> [a] -> [a]
++ [String]
ms)) Bool
False
    RelSpec Any Int
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property Bool
True

testSoundRelSpec :: Gen Property
testSoundRelSpec :: Gen Property
testSoundRelSpec = do
  Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
3, Int
10)
  RelSpec TT Word64
s1 <- forall dom era.
Ord dom =>
[String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec [String
"from testSoundRelSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n] (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
10000)) forall era. Rep era Word64
Word64R Int
n
  Set Word64
ans <- forall era t.
(Era era, Ord t) =>
[String] -> Gen t -> Int -> RelSpec era t -> Gen (Set t)
genFromRelSpec @TT [String
"from testSoundRelSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n] (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
100000)) Int
n RelSpec TT Word64
s1
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample (String
"spec=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Word64
s1 forall a. [a] -> [a] -> [a]
++ String
"\nans=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Set Word64
ans) (forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec TT Word64
s1)

testMergeRelSpec :: Gen Property
testMergeRelSpec :: Gen Property
testMergeRelSpec = do
  let msg :: [String]
msg = [String
"testMergeRelSpec"]
  Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
0, Int
10)
  RelSpec TT Word64
s1 <- forall dom era.
Ord dom =>
[String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec ((String
"genRelSpec") forall a. a -> [a] -> [a]
: [String]
msg) (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
10000)) forall era. Rep era Word64
Word64R Int
n
  RelSpec TT Word64
s2 <- forall dom era.
[String] -> Gen dom -> RelSpec era dom -> Gen (RelSpec era dom)
genConsistentRelSpec ((String
"genConsistentRepSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Word64
s1) forall a. a -> [a] -> [a]
: [String]
msg) (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) RelSpec TT Word64
s1
  case RelSpec TT Word64
s1 forall a. Semigroup a => a -> a -> a
<> RelSpec TT Word64
s2 of
    RelNever [String]
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall prop. Testable prop => prop -> Property
property Bool
True) -- This test is an implication (consistent (s1 <> s2) => ...)
    RelSpec TT Word64
s4 -> do
      let size :: Size
size = forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec TT Word64
s4
      Int
m <- Size -> Gen Int
genFromSize Size
size
      Set Word64
ans <- forall era t.
(Era era, Ord t) =>
[String] -> Gen t -> Int -> RelSpec era t -> Gen (Set t)
genFromRelSpec @TT [String
"testMergeRelSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Word64
s1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Word64
s2] (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) Int
m RelSpec TT Word64
s4
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        forall prop. Testable prop => String -> prop -> Property
counterexample
          ( String
"s1="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Word64
s1
              forall a. [a] -> [a] -> [a]
++ String
"\ns2="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Word64
s2
              forall a. [a] -> [a] -> [a]
++ String
"\ns1<>s2="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Word64
s4
              forall a. [a] -> [a] -> [a]
++ String
"\nans="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Set Word64
ans
              forall a. [a] -> [a] -> [a]
++ String
"\nrun s1="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec TT Word64
s1)
              forall a. [a] -> [a] -> [a]
++ String
"\nrun s2="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec TT Word64
s2)
              forall a. [a] -> [a] -> [a]
++ String
"\nrun s4="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec TT Word64
s4)
          )
          (forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec TT Word64
s4 Bool -> Bool -> Bool
&& forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec TT Word64
s2 Bool -> Bool -> Bool
&& forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Word64
ans RelSpec TT Word64
s1)

consistent :: (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent :: forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent a
x a
y = case forall x. Typed x -> Either [String] x
runTyped (forall x. LiftT x => x -> Typed x
liftT (a
x forall a. Semigroup a => a -> a -> a
<> a
y)) of
  Left [String]
_ -> forall a. Maybe a
Nothing
  Right a
spec -> forall a. a -> Maybe a
Just a
spec

manyMergeRelSpec :: Gen (Int, Int, [String])
manyMergeRelSpec :: Gen (Int, Int, [String])
manyMergeRelSpec = do
  Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
3, Int
10)
  [RelSpec TT Int]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
60 (forall dom era.
Ord dom =>
[String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec [String
"manyMergeRelSpec xs"] (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) forall era. Rep era Int
IntR Int
n)
  [RelSpec TT Int]
ys <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
60 (forall dom era.
Ord dom =>
[String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec [String
"manyMergeRelSpec ys"] (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) forall era. Rep era Int
IntR Int
n)
  let ok :: RelSpec era dom -> Bool
ok RelSpec era dom
RelAny = Bool
False
      ok RelSpec era dom
_ = Bool
True
      check :: (RelSpec TT Int, RelSpec TT Int, RelSpec TT Int)
-> Gen
     (RelSpec TT Int, Bool, RelSpec TT Int, Bool, Set Int, Bool,
      RelSpec TT Int)
check (RelSpec TT Int
x, RelSpec TT Int
y, RelSpec TT Int
m) = do
        let size :: Size
size = forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec TT Int
m
        Int
i <- Size -> Gen Int
genFromSize Size
size
        let wordsX :: [String]
wordsX =
              [ String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec TT Int
m)
              , String
"s1<>s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Int
m
              , String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec TT Int
x)
              , String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Int
x
              , String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec TT Int
y)
              , String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec TT Int
y
              , String
"GenFromRelSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
              ]
        Set Int
z <- forall era t.
(Era era, Ord t) =>
[String] -> Gen t -> Int -> RelSpec era t -> Gen (Set t)
genFromRelSpec @TT [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) Int
i RelSpec TT Int
m
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (RelSpec TT Int
x, forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Int
z RelSpec TT Int
x, RelSpec TT Int
y, forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Int
z RelSpec TT Int
y, Set Int
z, forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set Int
z RelSpec TT Int
m, RelSpec TT Int
m)
      showAns :: (RelSpec era dom, a, RelSpec era dom, a, a, a, RelSpec era dom)
-> String
showAns (RelSpec era dom
s1, a
run1, RelSpec era dom
s2, a
run2, a
v, a
run3, RelSpec era dom
s3) =
        [String] -> String
unlines
          [ String
"\ns1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era dom
s1
          , String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era dom
s1)
          , String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era dom
s2
          , String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era dom
s2)
          , String
"s1 <> s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era dom
s3
          , String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era dom
s3)
          , String
"v = genFromRelSpec (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
v
          , String
"runRelSpec v s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run1
          , String
"runRelSpec v s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run2
          , String
"runRelSpec v (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run3
          ]
      pr :: (RelSpec era dom, Bool, RelSpec era dom, Bool, a, Bool,
 RelSpec era dom)
-> Maybe String
pr x :: (RelSpec era dom, Bool, RelSpec era dom, Bool, a, Bool,
 RelSpec era dom)
x@(RelSpec era dom
_, Bool
a, RelSpec era dom
_, Bool
b, a
_, Bool
c, RelSpec era dom
_) = if Bool -> Bool
not (Bool
a Bool -> Bool -> Bool
&& Bool
b Bool -> Bool -> Bool
&& Bool
c) then forall a. a -> Maybe a
Just (forall {a} {a} {a} {a} {era} {dom} {era} {dom} {era} {dom}.
(Show a, Show a, Show a, Show a) =>
(RelSpec era dom, a, RelSpec era dom, a, a, a, RelSpec era dom)
-> String
showAns (RelSpec era dom, Bool, RelSpec era dom, Bool, a, Bool,
 RelSpec era dom)
x) else forall a. Maybe a
Nothing
  let trips :: [(RelSpec TT Int, RelSpec TT Int, RelSpec TT Int)]
trips = [(RelSpec TT Int
x, RelSpec TT Int
y, RelSpec TT Int
m) | RelSpec TT Int
x <- [RelSpec TT Int]
xs, RelSpec TT Int
y <- [RelSpec TT Int]
ys, forall era d. RelSpec era d -> Bool
ok RelSpec TT Int
x Bool -> Bool -> Bool
&& forall era d. RelSpec era d -> Bool
ok RelSpec TT Int
y, Just RelSpec TT Int
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent RelSpec TT Int
x RelSpec TT Int
y]]
  [(RelSpec TT Int, Bool, RelSpec TT Int, Bool, Set Int, Bool,
  RelSpec TT Int)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (RelSpec TT Int, RelSpec TT Int, RelSpec TT Int)
-> Gen
     (RelSpec TT Int, Bool, RelSpec TT Int, Bool, Set Int, Bool,
      RelSpec TT Int)
check [(RelSpec TT Int, RelSpec TT Int, RelSpec TT Int)]
trips
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (Int
n, forall (t :: * -> *) a. Foldable t => t a -> Int
length [(RelSpec TT Int, RelSpec TT Int, RelSpec TT Int)]
trips, forall a b. (a -> Maybe b) -> [a] -> [b]
Maybe.mapMaybe forall {a} {era} {dom} {era} {dom} {era} {dom}.
Show a =>
(RelSpec era dom, Bool, RelSpec era dom, Bool, a, Bool,
 RelSpec era dom)
-> Maybe String
pr [(RelSpec TT Int, Bool, RelSpec TT Int, Bool, Set Int, Bool,
  RelSpec TT Int)]
ts)

reportManyMergeRelSpec :: IO ()
reportManyMergeRelSpec :: IO ()
reportManyMergeRelSpec = do
  (Int
n, Int
passed, [String]
bad) <- forall a. Gen a -> IO a
generate Gen (Int, Int, [String])
manyMergeRelSpec
  if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
bad
    then String -> IO ()
putStrLn (String
"passed " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
passed forall a. [a] -> [a] -> [a]
++ String
" tests. Spec size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n)
    else do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn [String]
bad; forall a. HasCallStack => String -> a
error String
"TestFails"

-- ==========================================================

-- | Indicates which constraints (if any) the range of a Map must adhere to
--   There are 3 cases RngSum, RngProj, and RngRel. They are all mutually inconsistent.
--   So while any Map may constrain its range, it can only choose ONE of the cases.
data RngSpec era rng where
  -- | The set must have Adds instance and add up to 'rng'
  RngSum ::
    Adds rng =>
    rng -> -- the smallest element in the partition (usually 0 or 1)
    Size -> -- the sum of all the elements must fall in the range denoted by the Size
    RngSpec era rng
  RngProj ::
    Adds c =>
    c -> -- the smallest element in the partition (usually 0 or 1)
    Rep era x ->
    Lens' x c ->
    Size -> -- the sum of all the elements must fall in the range denoted by the Size
    RngSpec era x
  -- | The range has exactly these elements
  RngElem :: Eq r => Rep era r -> [r] -> RngSpec era r
  -- | The range must hold on the relation specified
  RngRel :: Ord x => RelSpec era x -> RngSpec era x
  -- | There are no constraints on the range (random generator will do)
  RngAny :: RngSpec era rng
  -- | Something was inconsistent
  RngNever :: [String] -> RngSpec era rng

instance Show (RngSpec era t) where
  show :: RngSpec era t -> String
show = forall era t. RngSpec era t -> String
showRngSpec

instance Era era => Monoid (RngSpec era rng) where
  mempty :: RngSpec era rng
mempty = forall era rng. RngSpec era rng
RngAny

instance Era era => Semigroup (RngSpec era rng) where
  <> :: RngSpec era rng -> RngSpec era rng -> RngSpec era rng
(<>) = forall r era. RngSpec era r -> RngSpec era r -> RngSpec era r
mergeRngSpec

instance LiftT (RngSpec era a) where
  liftT :: RngSpec era a -> Typed (RngSpec era a)
liftT (RngNever [String]
xs) = forall a. [String] -> Typed a
failT [String]
xs
  liftT RngSpec era a
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure RngSpec era a
x
  dropT :: Typed (RngSpec era a) -> RngSpec era a
dropT (Typed (Left [String]
s)) = forall era rng. [String] -> RngSpec era rng
RngNever [String]
s
  dropT (Typed (Right RngSpec era a
x)) = RngSpec era a
x

showRngSpec :: RngSpec era t -> String
showRngSpec :: forall era t. RngSpec era t -> String
showRngSpec (RngSum t
small Size
sz) = [String] -> String
sepsP [String
"RngSum", forall a. Show a => a -> String
show t
small, forall a. Show a => a -> String
show Size
sz]
showRngSpec (RngProj c
small Rep era t
xrep Lens' t c
_l Size
sz) = [String] -> String
sepsP [String
"RngProj", forall a. Show a => a -> String
show c
small, forall a. Show a => a -> String
show Rep era t
xrep, forall a. Show a => a -> String
show Size
sz]
showRngSpec (RngElem Rep era t
r [t]
cs) = [String] -> String
sepsP [String
"RngElem", forall a. Show a => a -> String
show Rep era t
r, forall e t. Rep e t -> t -> String
synopsis (forall era c. Rep era c -> Rep era [c]
ListR Rep era t
r) [t]
cs]
showRngSpec (RngRel RelSpec era t
x) = [String] -> String
sepsP [String
"RngRel", forall a. Show a => a -> String
show RelSpec era t
x]
showRngSpec RngSpec era t
RngAny = String
"RngAny"
showRngSpec (RngNever [String]
_) = String
"RngNever"

mergeRngSpec :: forall r era. RngSpec era r -> RngSpec era r -> RngSpec era r
mergeRngSpec :: forall r era. RngSpec era r -> RngSpec era r -> RngSpec era r
mergeRngSpec RngSpec era r
RngAny RngSpec era r
x = RngSpec era r
x
mergeRngSpec RngSpec era r
x RngSpec era r
RngAny = RngSpec era r
x
mergeRngSpec (RngRel RelSpec era r
RelAny) RngSpec era r
x = RngSpec era r
x
mergeRngSpec RngSpec era r
x (RngRel RelSpec era r
RelAny) = RngSpec era r
x
mergeRngSpec RngSpec era r
_ (RngNever [String]
xs) = forall era rng. [String] -> RngSpec era rng
RngNever [String]
xs
mergeRngSpec (RngNever [String]
xs) RngSpec era r
_ = forall era rng. [String] -> RngSpec era rng
RngNever [String]
xs
mergeRngSpec a :: RngSpec era r
a@(RngElem Rep era r
_ [r]
xs) RngSpec era r
b
  | forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [r]
xs RngSpec era r
b = RngSpec era r
a
  | Bool
otherwise = forall era rng. [String] -> RngSpec era rng
RngNever [String
"The RngSpec's are inconsistent.\n  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
a forall a. [a] -> [a] -> [a]
++ String
"\n  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
b]
mergeRngSpec RngSpec era r
a b :: RngSpec era r
b@(RngElem Rep era r
_ [r]
xs)
  | forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [r]
xs RngSpec era r
a = RngSpec era r
b
  | Bool
otherwise = forall era rng. [String] -> RngSpec era rng
RngNever [String
"The RngSpec's are inconsistent.\n  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
a forall a. [a] -> [a] -> [a]
++ String
"\n  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
b]
mergeRngSpec a :: RngSpec era r
a@(RngSum r
small1 Size
sz1) b :: RngSpec era r
b@(RngSum r
small2 Size
sz2) =
  case Size
sz1 forall a. Semigroup a => a -> a -> a
<> Size
sz2 of
    SzNever [String]
xs -> forall era rng. [String] -> RngSpec era rng
RngNever ([String
"The RngSpec's are inconsistent.\n  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
a forall a. [a] -> [a] -> [a]
++ String
"\n  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
b] forall a. [a] -> [a] -> [a]
++ [String]
xs)
    Size
sz3 -> forall rng era. Adds rng => rng -> Size -> RngSpec era rng
RngSum (forall x. Adds x => x -> x -> x
smallerOf r
small1 r
small2) Size
sz3
mergeRngSpec a :: RngSpec era r
a@(RngRel RelSpec era r
r1) b :: RngSpec era r
b@(RngRel RelSpec era r
r2) =
  case RelSpec era r
r1 forall a. Semigroup a => a -> a -> a
<> RelSpec era r
r2 of
    RelNever [String]
xs -> forall era rng. [String] -> RngSpec era rng
RngNever ([String
"The RngSpec's are inconsistent.\n  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
a forall a. [a] -> [a] -> [a]
++ String
"\n  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
b] forall a. [a] -> [a] -> [a]
++ [String]
xs)
    RelSpec era r
r3 -> forall x era. Ord x => RelSpec era x -> RngSpec era x
RngRel RelSpec era r
r3
mergeRngSpec RngSpec era r
a RngSpec era r
b = forall era rng. [String] -> RngSpec era rng
RngNever [String
"The RngSpec's are inconsistent.\n  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
a forall a. [a] -> [a] -> [a]
++ String
"\n  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
b]

-- ===================================================================

-- | Compute the Size that is appropriate for a RngSpec
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

-- ------------------------------------------
-- generators for test functions.

-- | Generate an arbitrary size [r] for a particular size 'n'
--   The generated list is consistent with the RngSpec given as input.
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

-- | Generate a random RngSpec, appropriate for a given size. In order to accomodate any OrdCond
--   (EQL, LTH, LTE, GTE, GTH) in RngSum and RngProj, we make the total a bit larger than 'n'
genRngSpec ::
  forall w era.
  (Ord w, Adds w) =>
  Gen w ->
  Rep era w ->
  -- Rep era c ->
  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 -- Chooses smallest appropriate for type '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

-- ------------------------------------------
-- generators for RngSpec

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 -- Make the smaller bigger
    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)

-- Tests

testConsistentRng :: Gen Property
testConsistentRng :: Gen Property
testConsistentRng = do
  Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
3, Int
10)
  (RngSpec TT Word64
s1, RngSpec TT Word64
s2) <- forall era w c.
(Ord w, Adds w) =>
Int
-> Gen w
-> Rep era w
-> Rep era c
-> SomeLens era w
-> Gen (RngSpec era w, RngSpec era w)
genConsistentRngSpec @TestEra Int
n (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) forall era. Rep era Word64
Word64R forall era. Rep era Coin
CoinR (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL)
  case RngSpec TT Word64
s1 forall a. Semigroup a => a -> a -> a
<> RngSpec TT Word64
s2 of
    RngNever [String]
ms -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines ([String
"genConsistentRng fails", forall a. Show a => a -> String
show RngSpec TT Word64
s1, forall a. Show a => a -> String
show RngSpec TT Word64
s2] forall a. [a] -> [a] -> [a]
++ [String]
ms)) Bool
False
    RngSpec TT Word64
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample String
"" Bool
True

testSoundRngSpec :: Gen Property
testSoundRngSpec :: Gen Property
testSoundRngSpec = do
  Int
n <- forall a. Random a => (a, a) -> Gen a
choose (Int
2, Int
8)
  RngSpec TT Word64
spec <- forall w era.
(Ord w, Adds w) =>
Gen w -> Rep era w -> SomeLens era w -> Int -> Gen (RngSpec era w)
genRngSpec (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Int
n
  let msgs :: [String]
msgs = [String
"testSoundRngSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
spec]
  [Word64]
list <- forall era r.
Era era =>
[String] -> Gen r -> Int -> RngSpec era r -> Gen [r]
genFromRngSpec @TT [String]
msgs (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) Int
n RngSpec TT Word64
spec
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => String -> prop -> Property
counterexample
      (String
"spec=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
spec forall a. [a] -> [a] -> [a]
++ String
"\nlist=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Word64]
list)
      (forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Word64]
list RngSpec TT Word64
spec)

testMergeRngSpec :: Gen Property
testMergeRngSpec :: Gen Property
testMergeRngSpec = do
  (RngSpec TT Word64
s1, RngSpec TT Word64
s2) <- forall era w c.
(Ord w, Adds w) =>
Int
-> Gen w
-> Rep era w
-> Rep era c
-> SomeLens era w
-> Gen (RngSpec era w, RngSpec era w)
genConsistentRngSpec Int
3 (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) forall era. Rep era Word64
Word64R forall era. Rep era Coin
CoinR (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL)
  case RngSpec TT Word64
s1 forall a. Semigroup a => a -> a -> a
<> RngSpec TT Word64
s2 of
    RngNever [String]
_ ->
      forall a. String -> a -> a
Debug.trace (String
"inconsistent RngSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
s1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
s2) (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall prop. Testable prop => String -> prop -> Property
counterexample String
"" Bool
True))
    RngSpec TT Word64
s3 -> do
      let size :: Size
size = forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec TT Word64
s3
      Int
n <- Size -> Gen Int
genFromSize Size
size
      let wordsX :: [String]
wordsX =
            [ String
"s1=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
s1
            , String
"s2=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
s2
            , String
"s3=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
s3
            , String
"size=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
size
            , String
"n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
            , String
"testMergeRngSpec"
            ]
      [Word64]
list <- forall era r.
Era era =>
[String] -> Gen r -> Int -> RngSpec era r -> Gen [r]
genFromRngSpec @TT [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) Int
n RngSpec TT Word64
s3
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        forall prop. Testable prop => String -> prop -> Property
counterexample
          ( String
"s1="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
s1
              forall a. [a] -> [a] -> [a]
++ String
"\n  s2="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
s2
              forall a. [a] -> [a] -> [a]
++ String
"\n  s3="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Word64
s3
              forall a. [a] -> [a] -> [a]
++ String
"\n  size="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
size
              forall a. [a] -> [a] -> [a]
++ String
"\n  n="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
              forall a. [a] -> [a] -> [a]
++ String
"\n  list="
              forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall era c. Rep era c -> Rep era [c]
ListR forall era. Rep era Word64
Word64R) [Word64]
list
              forall a. [a] -> [a] -> [a]
++ String
"\n  run1="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Word64]
list RngSpec TT Word64
s1)
              forall a. [a] -> [a] -> [a]
++ String
"\n run2="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Word64]
list RngSpec TT Word64
s2)
          )
          (forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Word64]
list RngSpec TT Word64
s1 Bool -> Bool -> Bool
&& forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Word64]
list RngSpec TT Word64
s2)

intDeltaCoinL :: Lens' Int DeltaCoin
intDeltaCoinL :: Lens' Int DeltaCoin
intDeltaCoinL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (Integer -> DeltaCoin
DeltaCoin forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral) (\Int
_i (DeltaCoin Integer
d) -> forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
d)

manyMergeRngSpec :: Gen (Int, Int, [String])
manyMergeRngSpec :: Gen (Int, Int, [String])
manyMergeRngSpec = do
  Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
3, Int
10)
  [RngSpec TT Int]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
50 (forall w era.
(Ord w, Adds w) =>
Gen w -> Rep era w -> SomeLens era w -> Int -> Gen (RngSpec era w)
genRngSpec (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) forall era. Rep era Int
IntR (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Int DeltaCoin
intDeltaCoinL) Int
n)
  [RngSpec TT Int]
ys <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
50 (forall w era.
(Ord w, Adds w) =>
Gen w -> Rep era w -> SomeLens era w -> Int -> Gen (RngSpec era w)
genRngSpec (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) forall era. Rep era Int
IntR (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Int DeltaCoin
intDeltaCoinL) Int
n)
  let check :: (RngSpec TT Int, RngSpec TT Int, RngSpec TT Int)
-> Gen
     (RngSpec TT Int, Bool, RngSpec TT Int, Bool, [Int], Bool,
      RngSpec TT Int)
check (RngSpec TT Int
x, RngSpec TT Int
y, RngSpec TT Int
m) = do
        let size :: Size
size = forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec TT Int
m
        Int
i <- Size -> Gen Int
genFromSize Size
size
        let wordsX :: [String]
wordsX =
              [ String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec TT Int
m)
              , String
"s1<>s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Int
m
              , String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec TT Int
x)
              , String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Int
x
              , String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec TT Int
y)
              , String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec TT Int
y
              , String
"GenFromRngSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
              ]
        [Int]
z <- forall era r.
Era era =>
[String] -> Gen r -> Int -> RngSpec era r -> Gen [r]
genFromRngSpec @TT [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) Int
i RngSpec TT Int
m
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (RngSpec TT Int
x, forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Int]
z RngSpec TT Int
x, RngSpec TT Int
y, forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Int]
z RngSpec TT Int
y, [Int]
z, forall r era. [r] -> RngSpec era r -> Bool
runRngSpec [Int]
z RngSpec TT Int
m, RngSpec TT Int
m)
      showAns :: (RngSpec era dom, a, RngSpec era dom, a, a, a, RngSpec era dom)
-> String
showAns (RngSpec era dom
s1, a
run1, RngSpec era dom
s2, a
run2, a
v, a
run3, RngSpec era dom
s3) =
        [String] -> String
unlines
          [ String
"\ns1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era dom
s1
          , String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec era dom
s1)
          , String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era dom
s2
          , String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec era dom
s2)
          , String
"s1 <> s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era dom
s3
          , String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec era dom
s3)
          , String
"v = genFromRngSpec (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
v
          , String
"runRngSpec v s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run1
          , String
"runRngSpec v s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run2
          , String
"runRngSpec v (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run3
          ]
      pr :: (RngSpec era dom, Bool, RngSpec era dom, Bool, a, Bool,
 RngSpec era dom)
-> Maybe String
pr x :: (RngSpec era dom, Bool, RngSpec era dom, Bool, a, Bool,
 RngSpec era dom)
x@(RngSpec era dom
_, Bool
a, RngSpec era dom
_, Bool
b, a
_, Bool
c, RngSpec era dom
_) = if Bool -> Bool
not (Bool
a Bool -> Bool -> Bool
&& Bool
b Bool -> Bool -> Bool
&& Bool
c) then forall a. a -> Maybe a
Just (forall {a} {a} {a} {a} {era} {dom} {era} {dom} {era} {dom}.
(Show a, Show a, Show a, Show a) =>
(RngSpec era dom, a, RngSpec era dom, a, a, a, RngSpec era dom)
-> String
showAns (RngSpec era dom, Bool, RngSpec era dom, Bool, a, Bool,
 RngSpec era dom)
x) else forall a. Maybe a
Nothing
  let trips :: [(RngSpec TT Int, RngSpec TT Int, RngSpec TT Int)]
trips = [(RngSpec TT Int
x, RngSpec TT Int
y, RngSpec TT Int
m) | RngSpec TT Int
x <- [RngSpec TT Int]
xs, RngSpec TT Int
y <- [RngSpec TT Int]
ys, Just RngSpec TT Int
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent RngSpec TT Int
x RngSpec TT Int
y]]
  [(RngSpec TT Int, Bool, RngSpec TT Int, Bool, [Int], Bool,
  RngSpec TT Int)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (RngSpec TT Int, RngSpec TT Int, RngSpec TT Int)
-> Gen
     (RngSpec TT Int, Bool, RngSpec TT Int, Bool, [Int], Bool,
      RngSpec TT Int)
check [(RngSpec TT Int, RngSpec TT Int, RngSpec TT Int)]
trips
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (Int
n, forall (t :: * -> *) a. Foldable t => t a -> Int
length [(RngSpec TT Int, RngSpec TT Int, RngSpec TT Int)]
trips, forall a b. (a -> Maybe b) -> [a] -> [b]
Maybe.mapMaybe forall {a} {era} {dom} {era} {dom} {era} {dom}.
Show a =>
(RngSpec era dom, Bool, RngSpec era dom, Bool, a, Bool,
 RngSpec era dom)
-> Maybe String
pr [(RngSpec TT Int, Bool, RngSpec TT Int, Bool, [Int], Bool,
  RngSpec TT Int)]
ts)

reportManyMergeRngSpec :: IO ()
reportManyMergeRngSpec :: IO ()
reportManyMergeRngSpec = do
  (Int
n, Int
passed, [String]
bad) <- forall a. Gen a -> IO a
generate Gen (Int, Int, [String])
manyMergeRngSpec
  if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
bad
    then String -> IO ()
putStrLn (String
"passed " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
passed forall a. [a] -> [a] -> [a]
++ String
" tests. Spec size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n)
    else do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn [String]
bad; forall a. HasCallStack => String -> a
error String
"TestFails"

-- =====================================================

-- | Indicates which constraints (if any) a Map must adhere to
data MapSpec era dom rng where
  -- | The map may be constrained 3 ways. 1) Its size(Size) 2) its domain(RelSpec) 3) its range(RngSpec)
  MapSpec ::
    Size ->
    RelSpec era dom ->
    PairSpec era dom rng ->
    RngSpec era rng ->
    MapSpec era dom rng
  -- | Something is inconsistent
  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))

-- | Use 'mapSpec' instead of 'MapSpec' to check size and PairSpec consistency at creation time.
--   Runs in the type monad, so errors are caught and reported as Solver-time errors.
--   This should avoid many Gen-time errors, as many of those are cause by size
--   inconsistencies. We can also use this in mergeMapSpec, to catch size
--   inconsistencies there as well as (\ a b c -> dropT (mapSpec a b c)) has the same
--   type as MapSpec, but pushes the reports of inconsistencies into MapNever.
mapSpec ::
  Ord d => Size -> RelSpec era d -> PairSpec era d r -> RngSpec era r -> Typed (MapSpec era d r)
mapSpec :: forall d era r.
Ord d =>
Size
-> RelSpec era d
-> PairSpec era d r
-> RngSpec era r
-> Typed (MapSpec era d r)
mapSpec Size
sz1 RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng =
  let sz2 :: Size
sz2 = forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era d
rel
      sz3 :: Size
sz3 = forall dom era. RngSpec era dom -> Size
sizeForRng RngSpec era r
rng
      sz4 :: Size
sz4 = forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec era d r
pair
   in case Size
sz1 forall a. Semigroup a => a -> a -> a
<> Size
sz2 forall a. Semigroup a => a -> a -> a
<> Size
sz3 forall a. Semigroup a => a -> a -> a
<> Size
sz4 of
        SzNever [String]
xs ->
          forall a. [String] -> Typed a
failT
            ( [ String
"Creating " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
sz1 RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng) forall a. [a] -> [a] -> [a]
++ String
" fails."
              , String
"It has size inconsistencies."
              , String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era d
rel forall a. [a] -> [a] -> [a]
++ String
" has size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
sz2
              , String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era d r
pair forall a. [a] -> [a] -> [a]
++ String
" has size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
sz4
              , String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
rng forall a. [a] -> [a] -> [a]
++ String
" has size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
sz3
              ]
                forall a. [a] -> [a] -> [a]
++ [String]
xs
            )
        Size
size ->
          case (RelSpec era d
rel, PairSpec era d r
pair, RngSpec era r
rng) of
            (RelSpec era d
_, PairSpec era d r
PairAny, RngSpec era r
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
size RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng)
            ((RelOper Rep era d
_ Set d
mustd Maybe (Set d)
_ Set d
_), PairSpec Rep era d
d Rep era r
r PairSide
VarOnRight Map d r
m, (RngRel (RelOper Rep era r
_ Set r
mustr Maybe (Set r)
_ Set r
_))) ->
              forall a. String -> Typed a -> Typed a
explain
                (String
"Creating " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
sz1 RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng) forall a. [a] -> [a] -> [a]
++ String
" fails.")
                ( forall a. [(Bool, [String])] -> Typed a -> Typed a
requireAll
                    [
                      ( (forall k a. Map k a -> Set k
Map.keysSet Map d r
m forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set d
mustd)
                      ,
                        [ String
"sizes " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Size
sz1, Size
sz2, Size
sz3, Size
sz4)
                        , String
"It has PairSpec inconsistencies. The domain of"
                        , String
"   " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era b.
Ord c =>
Rep era c -> Rep era b -> Rep era (Map c b)
MapR Rep era d
d Rep era r
r) Map d r
m forall a. [a] -> [a] -> [a]
++ String
" is not a subset of the of the mustSet"
                        , String
"   " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era d
d) Set d
mustd
                        , String
"   TEST " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall k a. Map k a -> Set k
Map.keysSet Map d r
m forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set d
mustd)
                        ]
                      )
                    ,
                      ( (forall a. Ord a => [a] -> Set a
Set.fromList (forall k a. Map k a -> [a]
Map.elems Map d r
m) forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set r
mustr)
                      ,
                        [ String
"It has PairSpec inconsistencies. The range of"
                        , String
"   " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era b.
Ord c =>
Rep era c -> Rep era b -> Rep era (Map c b)
MapR Rep era d
d Rep era r
r) Map d r
m forall a. [a] -> [a] -> [a]
++ String
" is not a subset of the of the mustSet"
                        , String
"   " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era r
r) Set r
mustr
                        , String
"   TEST " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall k a. Map k a -> Set k
Map.keysSet Map d r
m forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set d
mustd)
                        ]
                      )
                    ]
                    (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
size RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng))
                )
            ((RelOper Rep era d
_ Set d
mustd Maybe (Set d)
_ Set d
_), PairSpec Rep era d
d Rep era r
r PairSide
VarOnLeft Map d r
m, (RngRel (RelOper Rep era r
_ Set r
mustr Maybe (Set r)
_ Set r
_))) ->
              forall a. String -> Typed a -> Typed a
explain
                (String
"Creating " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
sz1 RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng) forall a. [a] -> [a] -> [a]
++ String
" fails.")
                ( forall a. [(Bool, [String])] -> Typed a -> Typed a
requireAll
                    [
                      ( (Set d
mustd forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` forall k a. Map k a -> Set k
Map.keysSet Map d r
m)
                      ,
                        [ String
"sizes " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Size
sz1, Size
sz2, Size
sz3, Size
sz4)
                        , String
"It has PairSpec inconsistencies. The domain of"
                        , String
"   " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era b.
Ord c =>
Rep era c -> Rep era b -> Rep era (Map c b)
MapR Rep era d
d Rep era r
r) Map d r
m forall a. [a] -> [a] -> [a]
++ String
" is not a subset of the of the mustSet"
                        , String
"   " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era d
d) Set d
mustd
                        , String
"   TEST " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall k a. Map k a -> Set k
Map.keysSet Map d r
m forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set d
mustd)
                        ]
                      )
                    ,
                      ( (Set r
mustr forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` forall a. Ord a => [a] -> Set a
Set.fromList (forall k a. Map k a -> [a]
Map.elems Map d r
m))
                      ,
                        [ String
"It has PairSpec inconsistencies. The range of"
                        , String
"   " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era b.
Ord c =>
Rep era c -> Rep era b -> Rep era (Map c b)
MapR Rep era d
d Rep era r
r) Map d r
m forall a. [a] -> [a] -> [a]
++ String
" is not a subset of the of the mustSet"
                        , String
"   " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era. Ord c => Rep era c -> Rep era (Set c)
SetR Rep era r
r) Set r
mustr
                        , String
"   TEST " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall k a. Map k a -> Set k
Map.keysSet Map d r
m forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set d
mustd)
                        ]
                      )
                    ]
                    (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
size RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng))
                )
            (RelSpec era d
_, PairSpec Rep era d
_d Rep era r
_r PairSide
_side Map d r
_m, RngSpec era r
_) ->
              forall a. [String] -> Typed a
failT
                [ String
"Creating " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
sz1 RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng) forall a. [a] -> [a] -> [a]
++ String
" fails."
                , String
"This spec has a non-PairAny PairSpec"
                , String
"   " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era d r
pair
                , String
"so to be consistent it must have both a RelOper RelSpec, and a RngRel RelSpec."
                , String
"But it does not:"
                , String
"   RelSpec = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era d
rel
                , String
"   RngSpec = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RngSpec era r
rng
                ]
            (RelSpec era d
_, PairSpec era d r
p, RngSpec era r
_) | forall era d r. PairSpec era d r -> Bool
anyPairSpec PairSpec era d r
p -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
size RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng)
            (RelSpec era d
_, PairNever [String]
msgs, RngSpec era r
_) ->
              forall a. [String] -> Typed a
failT
                ((String
"Creating " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng.
Size
-> RelSpec era dom
-> PairSpec era dom rng
-> RngSpec era rng
-> MapSpec era dom rng
MapSpec Size
sz1 RelSpec era d
rel PairSpec era d r
pair RngSpec era r
rng) forall a. [a] -> [a] -> [a]
++ String
" fails.") forall a. a -> [a] -> [a]
: [String]
msgs)

-- ------------------------------------------
-- MapSpec test functions

-- | test a Map against a MapSpec
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

-- | compute a Size that bounds a MapSpec
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

-- ----------------------------------------
-- MapSpec generators

-- | Generate a random MapSpec
genMapSpec ::
  forall era dom w.
  (Ord dom, Era era, Ord w, Adds w) =>
  Gen dom ->
  Rep era dom ->
  Rep era w ->
  -- Rep era c ->
  -- (forall c. Adds c => Lens' w c) ->
  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)

-- | Generate a (Map d t) from a (MapSpec era d r)
-- genFromMapSpec ::
--   forall era w dom.
--   (Era era, Ord dom) =>
--   (V era (Map dom w)) ->
--   [String] ->
--   Gen dom ->
--   Gen w ->
--   MapSpec era dom w ->
--   Gen (Map dom w)
-- genFromMapSpec nm _ _ _ (MapNever xs) = errorMess ("genFromMapSpec " ++ (show nm) ++ " (MapNever _) fails") xs
-- genFromMapSpec nm msgs genD genR ms@(MapSpec size rel pair rng) = do
--   n <- genFromSize size
--   dom <-
--     genFromRelSpec
--       (("GenFromMapSpec " ++ (show nm) ++ "\n   " ++ show ms) : msgs)
--       genD
--       n
--       rel
--   rangelist <-
--     genFromRngSpec
--       (("genFromMapSpec " ++ (show nm) ++ "\n   " ++ show ms) : msgs)
--       genR
--       n
--       rng
--   pure (Map.fromList (zip (Set.toList dom) rangelist))
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