{-# 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
ms) forall a. a -> [a] -> [a]
: [String]
msgs)
      Gen w
genR
      Int
n
      RngSpec era w
rng
  let domainlist :: [dom]
domainlist = forall a. Set a -> [a]
Set.toList Set dom
dom
      extraPairs :: [(dom, w)]
extraPairs = forall d r era.
(Ord d, Eq r) =>
PairSide
-> Rep era d -> Rep era r -> Map d r -> ([d], [r]) -> [(d, r)]
pairSpecTransform PairSide
varside Rep era dom
dr Rep era w
rr Map dom w
m ([dom]
domainlist, [w]
rangelist)
  case PairSide
varside of
    PairSide
VarOnRight -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map dom w
m (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(dom, w)]
extraPairs))
    PairSide
VarOnLeft -> forall k a. Ord k => Int -> Map k a -> Gen (Map k a)
subMapFromMapWithSize Int
n (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys Map dom w
m (forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(dom, w)]
extraPairs)))

-- | Transform the domain and range lists by removing the (domain,range) pairs from 'm'.
--   for each pair (domain,range) remove domain from 'dlist' and range from 'rlist',
--   then zip together the two remaining lists. The pairs in this list are 'extra'
--   pairs which might me useful.
--   Strategy depends on which term to (SubMap t1 t2) are variables.
--   (SubMap xvar yexp) Break value of yexp into (x + extra), then answer: xvar = x
--   (SubMap xexp yvar) Break value of xexp into (x + extra), then answer: yvar == x + extra
pairSpecTransform ::
  (Ord d, Eq r) => PairSide -> Rep era d -> Rep era r -> Map d r -> ([d], [r]) -> [(d, r)]
pairSpecTransform :: forall d r era.
(Ord d, Eq r) =>
PairSide
-> Rep era d -> Rep era r -> Map d r -> ([d], [r]) -> [(d, r)]
pairSpecTransform PairSide
side Rep era d
drep Rep era r
rrep Map d r
m ([d]
dlist, [r]
rlist) = forall a b. [a] -> [b] -> [(a, b)]
zip [d]
doms [r]
rngs
  where
    accum :: ([d], [r]) -> d -> r -> ([d], [r])
accum ([d]
ds, [r]
rs) d
k r
v = (forall a era.
Eq a =>
PairSide -> String -> Rep era a -> a -> [a] -> [a]
remove PairSide
side String
"domain" Rep era d
drep d
k [d]
ds, forall a era.
Eq a =>
PairSide -> String -> Rep era a -> a -> [a] -> [a]
remove PairSide
side String
"range" Rep era r
rrep r
v [r]
rs)
    ([d]
doms, [r]
rngs) = forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' ([d], [r]) -> d -> r -> ([d], [r])
accum ([d]
dlist, [r]
rlist) Map d r
m

remove :: Eq a => PairSide -> String -> Rep era a -> a -> [a] -> [a]
remove :: forall a era.
Eq a =>
PairSide -> String -> Rep era a -> a -> [a] -> [a]
remove PairSide
side String
part Rep era a
rep a
x (a
y : [a]
ys) =
  if a
x forall a. Eq a => a -> a -> Bool
== a
y then [a]
ys else a
y forall a. a -> [a] -> [a]
: (forall a era.
Eq a =>
PairSide -> String -> Rep era a -> a -> [a] -> [a]
remove PairSide
side String
part Rep era a
rep a
x [a]
ys)
remove PairSide
VarOnLeft String
_part Rep era a
_rep a
_x [] = []
remove PairSide
VarOnRight String
part Rep era a
rep a
x [] =
  forall a. HasCallStack => String -> [String] -> a
errorMess
    ( String
"In SubMap, when the variable is on the right (i.e. (SubMap map var) ) the "
        forall a. [a] -> [a] -> [a]
++ String
part
        forall a. [a] -> [a] -> [a]
++ String
"of map should contain "
        forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era a
rep a
x
        forall a. [a] -> [a] -> [a]
++ String
" which appears in the "
        forall a. [a] -> [a] -> [a]
++ String
part
        forall a. [a] -> [a] -> [a]
++ String
" of the PairSpec."
        forall a. [a] -> [a] -> [a]
++ String
" But it does not."
    )
    [String
"genFromMapSpec"]

genMapSpecIsSound :: Gen Property
genMapSpecIsSound :: Gen Property
genMapSpecIsSound = do
  Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
1, Int
15)
  MapSpec TT Int Word64
spec <- forall era dom w.
(Ord dom, Era era, Ord w, Adds w) =>
Gen dom
-> Rep era dom
-> Rep era w
-> SomeLens era w
-> Int
-> Gen (MapSpec era dom w)
genMapSpec ((Int, Int) -> Gen Int
chooseInt (Int
1, Int
10000)) forall era. Rep era Int
IntR forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Int
n
  Map Int Word64
mp <- forall era w dom.
(Era era, Ord dom) =>
String
-> [String]
-> Gen dom
-> Gen w
-> MapSpec era dom w
-> Gen (Map dom w)
genFromMapSpec @TT String
"mapSpecIsSound" [] (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
10000)) (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
10000)) MapSpec TT Int Word64
spec
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample (String
"spec = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec TT Int Word64
spec forall a. [a] -> [a] -> [a]
++ String
"\nmp = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Map Int Word64
mp) (forall d r era. (Ord d, Eq r) => Map d r -> MapSpec era d r -> Bool
runMapSpec Map Int Word64
mp MapSpec TT Int Word64
spec)

manyMergeMapSpec :: Gen (Int, Int, [String])
manyMergeMapSpec :: Gen (Int, Int, [String])
manyMergeMapSpec = do
  Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
1, Int
10)
  [MapSpec TT Int Word64]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
50 (forall era dom w.
(Ord dom, Era era, Ord w, Adds w) =>
Gen dom
-> Rep era dom
-> Rep era w
-> SomeLens era w
-> Int
-> Gen (MapSpec era dom w)
genMapSpec (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) forall era. Rep era Int
IntR forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Int
n)
  [MapSpec TT Int Word64]
ys <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
50 (forall era dom w.
(Ord dom, Era era, Ord w, Adds w) =>
Gen dom
-> Rep era dom
-> Rep era w
-> SomeLens era w
-> Int
-> Gen (MapSpec era dom w)
genMapSpec (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) forall era. Rep era Int
IntR forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Int
n)
  let check :: (MapSpec TT Int Word64, MapSpec TT Int Word64,
 MapSpec TT Int Word64)
-> Gen
     (MapSpec TT Int Word64, Bool, MapSpec TT Int Word64, Bool,
      Map Int Word64, Bool, MapSpec TT Int Word64)
check (MapSpec TT Int Word64
x, MapSpec TT Int Word64
y, MapSpec TT Int Word64
m) = do
        let msize :: Size
msize = forall era d r. MapSpec era d r -> Size
sizeForMapSpec MapSpec TT Int Word64
m
        Int
i <- Size -> Gen Int
genFromSize Size
msize
        let wordsX :: [String]
wordsX =
              [ String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
msize
              , String
"s1<>s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec TT Int Word64
m
              , String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era d r. MapSpec era d r -> Size
sizeForMapSpec MapSpec TT Int Word64
x)
              , String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec TT Int Word64
x
              , String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era d r. MapSpec era d r -> Size
sizeForMapSpec MapSpec TT Int Word64
y)
              , String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec TT Int Word64
y
              , String
"GenFromMapSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
              ]
        Map Int Word64
z <- forall era w dom.
(Era era, Ord dom) =>
String
-> [String]
-> Gen dom
-> Gen w
-> MapSpec era dom w
-> Gen (Map dom w)
genFromMapSpec @TT String
"manyMergeMap" [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
100)) MapSpec TT Int Word64
m
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (MapSpec TT Int Word64
x, forall d r era. (Ord d, Eq r) => Map d r -> MapSpec era d r -> Bool
runMapSpec Map Int Word64
z MapSpec TT Int Word64
x, MapSpec TT Int Word64
y, forall d r era. (Ord d, Eq r) => Map d r -> MapSpec era d r -> Bool
runMapSpec Map Int Word64
z MapSpec TT Int Word64
y, Map Int Word64
z, forall d r era. (Ord d, Eq r) => Map d r -> MapSpec era d r -> Bool
runMapSpec Map Int Word64
z MapSpec TT Int Word64
m, MapSpec TT Int Word64
m)
      showAns :: (MapSpec era d r, a, MapSpec era d r, a, a, a, MapSpec era d r)
-> String
showAns (MapSpec era d r
s1, a
run1, MapSpec era d r
s2, a
run2, a
v, a
run3, MapSpec era d r
s3) =
        [String] -> String
unlines
          [ String
"\ns1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era d r
s1
          , String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era d r. MapSpec era d r -> Size
sizeForMapSpec MapSpec era d r
s1)
          , String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era d r
s2
          , String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era d r. MapSpec era d r -> Size
sizeForMapSpec MapSpec era d r
s2)
          , String
"s1 <> s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show MapSpec era d r
s3
          , String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era d r. MapSpec era d r -> Size
sizeForMapSpec MapSpec era d r
s3)
          , String
"v = genFromMapSpec (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
v
          , String
"runMapSpec v s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run1
          , String
"runMapSpec v s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run2
          , String
"runMapSpec v (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run3
          ]
      pr :: (MapSpec era d r, Bool, MapSpec era d r, Bool, a, Bool,
 MapSpec era d r)
-> Maybe String
pr x :: (MapSpec era d r, Bool, MapSpec era d r, Bool, a, Bool,
 MapSpec era d r)
x@(MapSpec era d r
_, Bool
a, MapSpec era d r
_, Bool
b, a
_, Bool
c, MapSpec era d r
_) = if Bool -> Bool
not (Bool
a Bool -> Bool -> Bool
&& Bool
b Bool -> Bool -> Bool
&& Bool
c) then forall a. a -> Maybe a
Just (forall {d} {d} {d} {a} {a} {a} {a} {era} {r} {era} {r} {era} {r}.
(Ord d, Ord d, Ord d, Show a, Show a, Show a, Show a) =>
(MapSpec era d r, a, MapSpec era d r, a, a, a, MapSpec era d r)
-> String
showAns (MapSpec era d r, Bool, MapSpec era d r, Bool, a, Bool,
 MapSpec era d r)
x) else forall a. Maybe a
Nothing
  let trips :: [(MapSpec TT Int Word64, MapSpec TT Int Word64,
  MapSpec TT Int Word64)]
trips = [(MapSpec TT Int Word64
x, MapSpec TT Int Word64
y, MapSpec TT Int Word64
m) | MapSpec TT Int Word64
x <- [MapSpec TT Int Word64]
xs, MapSpec TT Int Word64
y <- [MapSpec TT Int Word64]
ys, Just MapSpec TT Int Word64
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent MapSpec TT Int Word64
x MapSpec TT Int Word64
y]]
  [(MapSpec TT Int Word64, Bool, MapSpec TT Int Word64, Bool,
  Map Int Word64, Bool, MapSpec TT Int Word64)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (MapSpec TT Int Word64, MapSpec TT Int Word64,
 MapSpec TT Int Word64)
-> Gen
     (MapSpec TT Int Word64, Bool, MapSpec TT Int Word64, Bool,
      Map Int Word64, Bool, MapSpec TT Int Word64)
check [(MapSpec TT Int Word64, MapSpec TT Int Word64,
  MapSpec TT Int Word64)]
trips
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (Int
n, forall (t :: * -> *) a. Foldable t => t a -> Int
length [(MapSpec TT Int Word64, MapSpec TT Int Word64,
  MapSpec TT Int Word64)]
trips, forall a. [Maybe a] -> [a]
Maybe.catMaybes (forall a b. (a -> b) -> [a] -> [b]
map forall {d} {d} {d} {a} {era} {r} {era} {r} {era} {r}.
(Ord d, Ord d, Ord d, Show a) =>
(MapSpec era d r, Bool, MapSpec era d r, Bool, a, Bool,
 MapSpec era d r)
-> Maybe String
pr [(MapSpec TT Int Word64, Bool, MapSpec TT Int Word64, Bool,
  Map Int Word64, Bool, MapSpec TT Int Word64)]
ts))

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

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

data SetSpec era a where
  SetSpec :: Ord a => Size -> RelSpec era a -> SetSpec era a
  SetNever :: [String] -> SetSpec era a

instance Show (SetSpec era a) where show :: SetSpec era a -> String
show = forall era a. SetSpec era a -> String
showSetSpec

instance Ord a => Semigroup (SetSpec era a) where
  <> :: SetSpec era a -> SetSpec era a -> SetSpec era a
(<>) = forall a era.
Ord a =>
SetSpec era a -> SetSpec era a -> SetSpec era a
mergeSetSpec

instance Ord a => Monoid (SetSpec era a) where
  mempty :: SetSpec era a
mempty = forall a era. Ord a => Size -> RelSpec era a -> SetSpec era a
SetSpec Size
SzAny forall era dom. RelSpec era dom
RelAny

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

showSetSpec :: SetSpec era a -> String
showSetSpec :: forall era a. SetSpec era a -> String
showSetSpec (SetSpec Size
s RelSpec era a
r) = [String] -> String
sepsP [String
"SetSpec", forall a. Show a => a -> String
show Size
s, forall a. Show a => a -> String
show RelSpec era a
r]
showSetSpec (SetNever [String]
_) = String
"SetNever"

mergeSetSpec :: Ord a => SetSpec era a -> SetSpec era a -> SetSpec era a
mergeSetSpec :: forall a era.
Ord a =>
SetSpec era a -> SetSpec era a -> SetSpec era a
mergeSetSpec SetSpec era a
s1 SetSpec era a
s2 = case (SetSpec era a
s1, SetSpec era a
s2) of
  (SetNever [String]
xs, SetNever [String]
ys) -> forall era a. [String] -> SetSpec era a
SetNever ([String]
xs forall a. [a] -> [a] -> [a]
++ [String]
ys)
  (SetNever [String]
xs, SetSpec era a
_) -> forall era a. [String] -> SetSpec era a
SetNever [String]
xs
  (SetSpec era a
_, SetNever [String]
ys) -> forall era a. [String] -> SetSpec era a
SetNever [String]
ys
  (SetSpec Size
SzAny RelSpec era a
RelAny, SetSpec era a
x) -> SetSpec era a
x
  (SetSpec era a
x, SetSpec Size
SzAny RelSpec era a
RelAny) -> SetSpec era a
x
  (SetSpec Size
s11 RelSpec era a
r1, SetSpec Size
s22 RelSpec era a
r2) -> case RelSpec era a
r1 forall a. Semigroup a => a -> a -> a
<> RelSpec era a
r2 of
    RelNever [String]
xs -> forall era a. [String] -> SetSpec era a
SetNever ([String
"The SetSpec's are inconsistent.", String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec era a
s1, String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec era a
s2] forall a. [a] -> [a] -> [a]
++ [String]
xs)
    RelSpec era a
r3 -> forall x. LiftT x => Typed x -> x
dropT (forall a. String -> Typed a -> Typed a
explain (String
"While merging\n  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec era a
s1 forall a. [a] -> [a] -> [a]
++ String
"\n  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec era a
s2) forall a b. (a -> b) -> a -> b
$ forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec (Size
s11 forall a. Semigroup a => a -> a -> a
<> Size
s22) RelSpec era a
r3)

-- | Test the size consistency while building a SetSpec
setSpec :: Ord t => Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec :: forall t era.
Ord t =>
Size -> RelSpec era t -> Typed (SetSpec era t)
setSpec Size
sz1 RelSpec era t
rel = case (Size
sz1 forall a. Semigroup a => a -> a -> a
<> Size
sz2) of
  SzNever [String]
xs ->
    forall a. [String] -> Typed a
failT
      ( [ String
"Creating " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a era. Ord a => Size -> RelSpec era a -> SetSpec era a
SetSpec Size
sz1 RelSpec era t
rel) forall a. [a] -> [a] -> [a]
++ String
" fails."
        , String
"It has size inconsistencies."
        , String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RelSpec era t
rel forall a. [a] -> [a] -> [a]
++ String
" has size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
sz2
        , String
"  " forall a. [a] -> [a] -> [a]
++ String
"the expected size is " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
sz1
        ]
          forall a. [a] -> [a] -> [a]
++ [String]
xs
      )
  Size
size -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a era. Ord a => Size -> RelSpec era a -> SetSpec era a
SetSpec Size
size RelSpec era t
rel)
  where
    sz2 :: Size
sz2 = forall era dom. RelSpec era dom -> Size
sizeForRel RelSpec era t
rel

runSetSpec :: Set a -> SetSpec era a -> Bool
runSetSpec :: forall a era. Set a -> SetSpec era a -> Bool
runSetSpec Set a
s (SetSpec Size
sz RelSpec era a
rel) = Int -> Size -> Bool
runSize (forall a. Set a -> Int
Set.size Set a
s) Size
sz Bool -> Bool -> Bool
&& forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec Set a
s RelSpec era a
rel
runSetSpec Set a
_ (SetNever [String]
msgs) = forall a. HasCallStack => String -> [String] -> a
errorMess String
"runSetSpec applied to SetNever" [String]
msgs

sizeForSetSpec :: SetSpec era a -> Size
sizeForSetSpec :: forall era a. SetSpec era a -> Size
sizeForSetSpec (SetSpec Size
sz RelSpec era a
_) = Size
sz
sizeForSetSpec (SetNever [String]
_) = Size
SzAny

genSetSpec :: Ord s => [String] -> Gen s -> Rep era s -> Int -> Gen (SetSpec era s)
genSetSpec :: forall s era.
Ord s =>
[String] -> Gen s -> Rep era s -> Int -> Gen (SetSpec era s)
genSetSpec [String]
msgs Gen s
genS Rep era s
repS Int
size = do
  RelSpec era s
r <- forall dom era.
Ord dom =>
[String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec (String
"from genSetSpec" forall a. a -> [a] -> [a]
: [String]
msgs) Gen s
genS Rep era s
repS Int
size
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a era. Ord a => Size -> RelSpec era a -> SetSpec era a
SetSpec (Int -> Size
SzExact Int
size) RelSpec era s
r)

genFromSetSpec :: forall era a. Era era => [String] -> Gen a -> SetSpec era a -> Gen (Set a)
genFromSetSpec :: forall era a.
Era era =>
[String] -> Gen a -> SetSpec era a -> Gen (Set a)
genFromSetSpec [String]
msgs Gen a
genS (SetSpec Size
sz RelSpec era a
rp) = do
  Int
n <- Size -> Gen Int
genFromSize Size
sz
  forall era t.
(Era era, Ord t) =>
[String] -> Gen t -> Int -> RelSpec era t -> Gen (Set t)
genFromRelSpec (String
"genFromSetSpec" forall a. a -> [a] -> [a]
: [String]
msgs) Gen a
genS Int
n RelSpec era a
rp
genFromSetSpec [String]
_ Gen a
_ (SetNever [String]
msgs) = forall a. HasCallStack => String -> [String] -> a
errorMess String
"genFromSetSpec applied to SetNever" [String]
msgs

genSetSpecIsSound :: Gen Property
genSetSpecIsSound :: Gen Property
genSetSpecIsSound = do
  Int
size <- (Int, Int) -> Gen Int
chooseInt (Int
0, Int
10)
  SetSpec TT Int
spec <- forall s era.
Ord s =>
[String] -> Gen s -> Rep era s -> Int -> Gen (SetSpec era s)
genSetSpec [String]
msgs ((Int, Int) -> Gen Int
chooseInt (Int
1, Int
1000)) forall era. Rep era Int
IntR Int
size
  Set Int
mp <- forall era a.
Era era =>
[String] -> Gen a -> SetSpec era a -> Gen (Set a)
genFromSetSpec @TT [String]
msgs (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
10000)) SetSpec TT Int
spec
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample (String
"spec = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec TT Int
spec forall a. [a] -> [a] -> [a]
++ String
"\nmp = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Set Int
mp) (forall a era. Set a -> SetSpec era a -> Bool
runSetSpec Set Int
mp SetSpec TT Int
spec)
  where
    msgs :: [String]
msgs = [String
"genSetSpecIsSound"]

manyMergeSetSpec :: Gen (Int, Int, [String])
manyMergeSetSpec :: Gen (Int, Int, [String])
manyMergeSetSpec = do
  Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
1, Int
10)
  [SetSpec TT Int]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
50 (forall s era.
Ord s =>
[String] -> Gen s -> Rep era s -> Int -> Gen (SetSpec era s)
genSetSpec [] (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) forall era. Rep era Int
IntR Int
n)
  [SetSpec TT Int]
ys <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
50 (forall s era.
Ord s =>
[String] -> Gen s -> Rep era s -> Int -> Gen (SetSpec era s)
genSetSpec [] (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) forall era. Rep era Int
IntR Int
n)
  let check :: (SetSpec TT Int, SetSpec TT Int, SetSpec TT Int)
-> Gen
     (SetSpec TT Int, Bool, SetSpec TT Int, Bool, Set Int, Bool,
      SetSpec TT Int)
check (SetSpec TT Int
x, SetSpec TT Int
y, SetSpec TT Int
m) = do
        let msize :: Size
msize = forall era a. SetSpec era a -> Size
sizeForSetSpec SetSpec TT Int
m
        Int
i <- Size -> Gen Int
genFromSize Size
msize
        let wordsX :: [String]
wordsX =
              [ String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
msize
              , String
"s1<>s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec TT Int
m
              , String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era a. SetSpec era a -> Size
sizeForSetSpec SetSpec TT Int
x)
              , String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec TT Int
x
              , String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era a. SetSpec era a -> Size
sizeForSetSpec SetSpec TT Int
y)
              , String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec TT Int
y
              , String
"GenFromSetSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" n=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n
              ]
        Set Int
z <- forall era a.
Era era =>
[String] -> Gen a -> SetSpec era a -> Gen (Set a)
genFromSetSpec @TT [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
100)) SetSpec TT Int
m
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (SetSpec TT Int
x, forall a era. Set a -> SetSpec era a -> Bool
runSetSpec Set Int
z SetSpec TT Int
x, SetSpec TT Int
y, forall a era. Set a -> SetSpec era a -> Bool
runSetSpec Set Int
z SetSpec TT Int
y, Set Int
z, forall a era. Set a -> SetSpec era a -> Bool
runSetSpec Set Int
z SetSpec TT Int
m, SetSpec TT Int
m)
      showAns :: (SetSpec era a, a, SetSpec era a, a, a, a, SetSpec era a) -> String
showAns (SetSpec era a
s1, a
run1, SetSpec era a
s2, a
run2, a
v, a
run3, SetSpec era a
s3) =
        [String] -> String
unlines
          [ String
"\ns1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec era a
s1
          , String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era a. SetSpec era a -> Size
sizeForSetSpec SetSpec era a
s1)
          , String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec era a
s2
          , String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era a. SetSpec era a -> Size
sizeForSetSpec SetSpec era a
s2)
          , String
"s1 <> s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SetSpec era a
s3
          , String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era a. SetSpec era a -> Size
sizeForSetSpec SetSpec era a
s3)
          , String
"v = genFromSetSpec (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
v
          , String
"runSetSpec v s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run1
          , String
"runSetSpec v s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run2
          , String
"runSetSpec v (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run3
          ]
      pr :: (SetSpec era a, Bool, SetSpec era a, Bool, a, Bool, SetSpec era a)
-> Maybe String
pr x :: (SetSpec era a, Bool, SetSpec era a, Bool, a, Bool, SetSpec era a)
x@(SetSpec era a
_, Bool
a, SetSpec era a
_, Bool
b, a
_, Bool
c, SetSpec era a
_) = if Bool -> Bool
not (Bool
a Bool -> Bool -> Bool
&& Bool
b Bool -> Bool -> Bool
&& Bool
c) then forall a. a -> Maybe a
Just (forall {a} {a} {a} {a} {era} {a} {era} {a} {era} {a}.
(Show a, Show a, Show a, Show a) =>
(SetSpec era a, a, SetSpec era a, a, a, a, SetSpec era a) -> String
showAns (SetSpec era a, Bool, SetSpec era a, Bool, a, Bool, SetSpec era a)
x) else forall a. Maybe a
Nothing
  let trips :: [(SetSpec TT Int, SetSpec TT Int, SetSpec TT Int)]
trips = [(SetSpec TT Int
x, SetSpec TT Int
y, SetSpec TT Int
m) | SetSpec TT Int
x <- [SetSpec TT Int]
xs, SetSpec TT Int
y <- [SetSpec TT Int]
ys, Just SetSpec TT Int
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent SetSpec TT Int
x SetSpec TT Int
y]]
  [(SetSpec TT Int, Bool, SetSpec TT Int, Bool, Set Int, Bool,
  SetSpec TT Int)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SetSpec TT Int, SetSpec TT Int, SetSpec TT Int)
-> Gen
     (SetSpec TT Int, Bool, SetSpec TT Int, Bool, Set Int, Bool,
      SetSpec TT Int)
check [(SetSpec TT Int, SetSpec TT Int, SetSpec 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 [(SetSpec TT Int, SetSpec TT Int, SetSpec TT Int)]
trips, forall a. [Maybe a] -> [a]
Maybe.catMaybes (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {era} {a} {era} {a} {era} {a}.
Show a =>
(SetSpec era a, Bool, SetSpec era a, Bool, a, Bool, SetSpec era a)
-> Maybe String
pr [(SetSpec TT Int, Bool, SetSpec TT Int, Bool, Set Int, Bool,
  SetSpec TT Int)]
ts))

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

-- =======================================================
-- Specifications for Lists

data ElemSpec era t where
  -- | The set must add up to 'tot', which is any number in the scope of Size
  ElemSum ::
    Adds t =>
    t -> -- The smallest allowed
    Size ->
    ElemSpec era t
  -- | The range must sum upto 'c', which is any number in the scope of Size,
  --   through the projection witnessed by the (Sums t c) class
  ElemProj ::
    Adds c =>
    c -> -- The smallest allowed
    Rep era x ->
    Lens' x c ->
    Size ->
    ElemSpec era x
  -- | The range has exactly these elements
  ElemEqual :: Eq t => Rep era t -> [t] -> ElemSpec era t
  -- In the future we will want to add somethig like:
  -- ElemOrd :: Ord t => Rep era t -> t -> OrdCond -> t -> ElemSpec era tS
  ElemNever :: [String] -> ElemSpec era t
  ElemAny :: ElemSpec era t

instance Show (ElemSpec era a) where
  show :: ElemSpec era a -> String
show = forall era a. ElemSpec era a -> String
showElemSpec

instance Era era => Semigroup (ElemSpec era a) where
  <> :: ElemSpec era a -> ElemSpec era a -> ElemSpec era a
(<>) = forall era a.
Era era =>
ElemSpec era a -> ElemSpec era a -> ElemSpec era a
mergeElemSpec

instance Era era => Monoid (ElemSpec era a) where
  mempty :: ElemSpec era a
mempty = forall era t. ElemSpec era t
ElemAny

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

showElemSpec :: ElemSpec era a -> String
showElemSpec :: forall era a. ElemSpec era a -> String
showElemSpec (ElemSum a
small Size
sz) = [String] -> String
sepsP [String
"ElemSum", forall a. Show a => a -> String
show a
small, forall a. Show a => a -> String
show Size
sz]
showElemSpec (ElemProj c
small Rep era a
r Lens' a c
_l Size
sz) = [String] -> String
sepsP [String
"ElemProj", forall a. Show a => a -> String
show c
small, forall a. Show a => a -> String
show Rep era a
r, forall a. Show a => a -> String
show Size
sz]
showElemSpec (ElemEqual Rep era a
r [a]
xs) = [String] -> String
sepsP [String
"ElemEqual", forall a. Show a => a -> String
show Rep era a
r, forall e t. Rep e t -> t -> String
synopsis (forall era c. Rep era c -> Rep era [c]
ListR Rep era a
r) [a]
xs]
showElemSpec (ElemNever [String]
_) = String
"ElemNever"
showElemSpec ElemSpec era a
ElemAny = String
"ElemAny"

mergeElemSpec :: Era era => ElemSpec era a -> ElemSpec era a -> ElemSpec era a
mergeElemSpec :: forall era a.
Era era =>
ElemSpec era a -> ElemSpec era a -> ElemSpec era a
mergeElemSpec (ElemNever [String]
xs) (ElemNever [String]
ys) = forall era t. [String] -> ElemSpec era t
ElemNever ([String]
xs forall a. [a] -> [a] -> [a]
++ [String]
ys)
mergeElemSpec (ElemNever [String]
xs) ElemSpec era a
_ = forall era t. [String] -> ElemSpec era t
ElemNever [String]
xs
mergeElemSpec ElemSpec era a
_ (ElemNever [String]
ys) = forall era t. [String] -> ElemSpec era t
ElemNever [String]
ys
mergeElemSpec ElemSpec era a
ElemAny ElemSpec era a
x = ElemSpec era a
x
mergeElemSpec ElemSpec era a
x ElemSpec era a
ElemAny = ElemSpec era a
x
mergeElemSpec a :: ElemSpec era a
a@(ElemEqual Rep era a
r [a]
xs) b :: ElemSpec era a
b@(ElemEqual Rep era a
_ [a]
ys) =
  if [a]
xs forall a. Eq a => a -> a -> Bool
== [a]
ys
    then forall t era. Eq t => Rep era t -> [t] -> ElemSpec era t
ElemEqual Rep era a
r [a]
xs
    else
      forall era t. [String] -> ElemSpec era t
ElemNever
        [ String
"The ElemSpec's are inconsistent."
        , String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
a
        , String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
b
        , forall e t. Rep e t -> t -> String
synopsis (forall era c. Rep era c -> Rep era [c]
ListR Rep era a
r) [a]
xs forall a. [a] -> [a] -> [a]
++ String
" =/= " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall era c. Rep era c -> Rep era [c]
ListR Rep era a
r) [a]
ys
        ]
mergeElemSpec a :: ElemSpec era a
a@(ElemEqual Rep era a
_ [a]
xs) b :: ElemSpec era a
b@(ElemSum a
_ Size
sz) =
  let computed :: a
computed = forall (t :: * -> *) c. (Foldable t, Adds c) => t c -> c
sumAdds [a]
xs
   in if Int -> Size -> Bool
runSize (forall x. Adds x => x -> Int
toI a
computed) Size
sz
        then ElemSpec era a
a
        else
          forall era t. [String] -> ElemSpec era t
ElemNever
            [ String
"The ElemSpec's are inconsistent."
            , String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
a
            , String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
b
            , String
"The computed sum("
                forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
computed
                forall a. [a] -> [a] -> [a]
++ String
") is not in the allowed range of the Size("
                forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
sz
                forall a. [a] -> [a] -> [a]
++ String
")"
            ]
mergeElemSpec b :: ElemSpec era a
b@(ElemSum a
_ Size
_) a :: ElemSpec era a
a@(ElemEqual Rep era a
_ [a]
_) = forall era a.
Era era =>
ElemSpec era a -> ElemSpec era a -> ElemSpec era a
mergeElemSpec ElemSpec era a
a ElemSpec era a
b
mergeElemSpec a :: ElemSpec era a
a@(ElemSum a
sm1 Size
sz1) b :: ElemSpec era a
b@(ElemSum a
sm2 Size
sz2) =
  case Size
sz1 forall a. Semigroup a => a -> a -> a
<> Size
sz2 of
    SzNever [String]
xs -> forall era t. [String] -> ElemSpec era t
ElemNever ([String] -> String
sepsP [String
"The ElemSpec's are inconsistent.", forall a. Show a => a -> String
show ElemSpec era a
a, forall a. Show a => a -> String
show ElemSpec era a
b] forall a. a -> [a] -> [a]
: [String]
xs)
    Size
sz3 -> forall t era. Adds t => t -> Size -> ElemSpec era t
ElemSum (forall x. Adds x => x -> x -> x
smallerOf a
sm1 a
sm2) Size
sz3
{-
mergeElemSpec a@(ElemProj sm1 r1 _l1 sz1) b@(ElemProj sm2 r2 _l2 sz2) = -- TODO FIXME ElemProj cannot be merged
  case testEql r1 r2 of
    Just Refl ->
      case sz1 <> sz2 of
        SzNever xs -> ElemNever ((sepsP ["The ElemSpec's are inconsistent.", show a, show b]) : xs)
        sz3 -> ElemProj (smallerOf sm1 sm2) r1 sz3
    Nothing -> ElemNever ["The ElemSpec's are inconsistent.", "  " ++ show a, "  " ++ show b]
-}
mergeElemSpec ElemSpec era a
a ElemSpec era a
b = forall era t. [String] -> ElemSpec era t
ElemNever [String
"The ElemSpec's are inconsistent.", String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
a, String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
b]

sizeForElemSpec :: forall a era. ElemSpec era a -> Size
sizeForElemSpec :: forall a era. ElemSpec era a -> Size
sizeForElemSpec (ElemNever [String]
_) = Size
SzAny
sizeForElemSpec ElemSpec era a
ElemAny = Size
SzAny
sizeForElemSpec (ElemEqual Rep era a
_ [a]
x) = Int -> Size
SzExact (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
x)
sizeForElemSpec (ElemSum a
smallest Size
sz) =
  if forall x. Adds x => x -> Int
toI a
smallest forall a. Ord a => a -> a -> Bool
> Int
0
    then Int -> Int -> Size
SzRng Int
1 (Size -> Int
minSize Size
sz forall a. Integral a => a -> a -> a
`div` forall x. Adds x => x -> Int
toI a
smallest)
    else Int -> Size
SzLeast Int
1
sizeForElemSpec (ElemProj c
smallest (Rep era a
_r :: (Rep era c)) Lens' a c
_l Size
sz) =
  if forall x. Adds x => x -> Int
toI c
smallest forall a. Ord a => a -> a -> Bool
> Int
0
    then Int -> Int -> Size
SzRng Int
1 (Size -> Int
minSize Size
sz forall a. Integral a => a -> a -> a
`div` forall x. Adds x => x -> Int
toI c
smallest)
    else Int -> Size
SzLeast Int
1

runElemSpec :: [a] -> ElemSpec era a -> Bool
runElemSpec :: forall a era. [a] -> ElemSpec era a -> Bool
runElemSpec [a]
xs ElemSpec era a
spec = case ElemSpec era a
spec of
  ElemNever [String]
_ -> Bool
False -- ErrorMess "ElemNever in runElemSpec" []
  ElemSpec era a
ElemAny -> Bool
True
  ElemEqual Rep era a
_ [a]
ys -> [a]
xs forall a. Eq a => a -> a -> Bool
== [a]
ys
  ElemSum a
_ Size
sz -> Int -> Size -> Bool
runSize (forall x. Adds x => x -> Int
toI (forall (t :: * -> *) c. (Foldable t, Adds c) => t c -> c
sumAdds [a]
xs)) Size
sz
  ElemProj c
_ Rep era a
_ Lens' a c
l Size
sz -> Int -> Size -> Bool
runSize (forall x. Adds x => x -> Int
toI (forall (t :: * -> *) b a.
(Foldable t, Adds b) =>
Lens' a b -> t a -> b
lensAdds Lens' a c
l [a]
xs)) Size
sz

genElemSpec ::
  forall w era.
  Adds w =>
  Rep era w ->
  -- Rep era c ->
  SomeLens era w ->
  Size ->
  Gen (ElemSpec era w)
genElemSpec :: forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ElemSpec era w)
genElemSpec Rep era w
repw (SomeLens (Lens' w c
l :: Lens' w c)) Size
siz = do
  let lo :: Int
lo = Size -> Int
minSize Size
siz
      hi :: Int
hi = Size -> Int
maxSize Size
siz
  if Int
lo forall a. Ord a => a -> a -> Bool
>= Int
1
    then
      forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency -- Can't really generate Sums, when size (n) is 0.
        [
          ( Int
2
          , 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
hi))
              forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall t era. Adds t => t -> Size -> ElemSpec era t
ElemSum (forall x. Adds x => [String] -> Int -> x
fromI [String
"genRngSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
siz] Int
smallest) Size
sz)
          )
        ,
          ( Int
2
          , do
              Int
smallest <- forall x. Adds x => Gen Int
genSmall @c
              Size
sz <- Int -> Gen Size
genBigSize (forall a. Ord a => a -> a -> a
max Int
1 (Int
smallest forall a. Num a => a -> a -> a
* Int
hi))
              forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall c era x.
Adds c =>
c -> Rep era x -> Lens' x c -> Size -> ElemSpec era x
ElemProj (forall x. Adds x => [String] -> Int -> x
fromI [String
"genRngSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
siz] Int
smallest) Rep era w
repw Lens' w c
l Size
sz)
          )
        , (Int
2, forall t era. Eq t => Rep era t -> [t] -> ElemSpec era t
ElemEqual Rep era w
repw forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Int
n <- Size -> Gen Int
genFromSize Size
siz; forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n (forall era b. Rep era b -> Gen b
genRep Rep era w
repw))
        , (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era t. ElemSpec era t
ElemAny)
        ]
    else
      forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
        [ (Int
3, forall t era. Eq t => Rep era t -> [t] -> ElemSpec era t
ElemEqual Rep era w
repw forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Int
n <- Size -> Gen Int
genFromSize Size
siz; forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n (forall era b. Rep era b -> Gen b
genRep Rep era w
repw))
        , (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era t. ElemSpec era t
ElemAny)
        ]

genFromElemSpec ::
  forall era r.
  [String] ->
  Gen r ->
  Int ->
  ElemSpec era r ->
  Gen [r]
genFromElemSpec :: forall era r. [String] -> Gen r -> Int -> ElemSpec era r -> Gen [r]
genFromElemSpec [String]
msgs Gen r
genr Int
n ElemSpec era r
x = case ElemSpec era r
x of
  (ElemNever [String]
xs) -> forall a. HasCallStack => String -> [String] -> a
errorMess String
"RngNever in genFromElemSpec" [String]
xs
  ElemSpec era r
ElemAny -> forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n Gen r
genr
  (ElemEqual Rep era r
_ [r]
xs) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [r]
xs
  (ElemSum r
small Size
sz) -> do
    Int
tot <- Size -> Gen Int
genFromIntRange Size
sz
    forall x. Adds x => x -> [String] -> Int -> x -> Gen [x]
partition r
small [String]
msgs Int
n (forall x. Adds x => [String] -> Int -> x
fromI (String
msg forall a. a -> [a] -> [a]
: [String]
msgs) Int
tot)
  (ElemProj c
small Rep era r
xrep Lens' r c
l Size
sz) -> do
    Int
tot <- Size -> Gen Int
genFromIntRange Size
sz
    [c]
rs <- forall x. Adds x => x -> [String] -> Int -> x -> Gen [x]
partition c
small [String]
msgs Int
n (forall x. Adds x => [String] -> Int -> x
fromI (String
msg forall a. a -> [a] -> [a]
: [String]
msgs) Int
tot)
    forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\c
r -> do r
ans <- forall era b. Rep era b -> Gen b
genRep Rep era r
xrep; forall (f :: * -> *) a. Applicative f => a -> f a
pure (r
ans forall a b. a -> (a -> b) -> b
& Lens' r c
l forall s t a b. ASetter s t a b -> b -> s -> t
.~ c
r)) [c]
rs
  where
    msg :: String
msg = String
"genFromElemSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era r
x

manyMergeElemSpec :: Gen (Size, Int, [String])
manyMergeElemSpec :: Gen (Size, Int, [String])
manyMergeElemSpec = do
  Size
size <- Gen Size
genSize
  [ElemSpec TT Word64]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
40 (forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ElemSpec era w)
genElemSpec forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Size
size)
  [ElemSpec TT Word64]
ys <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
40 (forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ElemSpec era w)
genElemSpec forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Size
size)
  let check :: (ElemSpec TT Word64, ElemSpec TT Word64, ElemSpec TT Word64)
-> Gen
     (ElemSpec TT Word64, Bool, ElemSpec TT Word64, Bool, [Word64],
      Bool, ElemSpec TT Word64)
check (ElemSpec TT Word64
x, ElemSpec TT Word64
y, ElemSpec TT Word64
m) = do
        let msize :: Size
msize = forall a era. ElemSpec era a -> Size
sizeForElemSpec ElemSpec TT Word64
m
        Int
i <- Size -> Gen Int
genFromSize Size
msize
        let wordsX :: [String]
wordsX =
              [ String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
msize
              , String
"s1<>s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec TT Word64
m
              , String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a era. ElemSpec era a -> Size
sizeForElemSpec ElemSpec TT Word64
x)
              , String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec TT Word64
x
              , String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a era. ElemSpec era a -> Size
sizeForElemSpec ElemSpec TT Word64
y)
              , String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec TT Word64
y
              , String
"GenFromElemSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" size=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
size
              ]
        [Word64]
z <- forall era r. [String] -> Gen r -> Int -> ElemSpec era r -> Gen [r]
genFromElemSpec @TT [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
100)) Int
i ElemSpec TT Word64
m
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (ElemSpec TT Word64
x, forall a era. [a] -> ElemSpec era a -> Bool
runElemSpec [Word64]
z ElemSpec TT Word64
x, ElemSpec TT Word64
y, forall a era. [a] -> ElemSpec era a -> Bool
runElemSpec [Word64]
z ElemSpec TT Word64
y, [Word64]
z, forall a era. [a] -> ElemSpec era a -> Bool
runElemSpec [Word64]
z ElemSpec TT Word64
m, ElemSpec TT Word64
m)
      showAns :: (ElemSpec era a, a, ElemSpec era a, a, a, a, ElemSpec era a)
-> String
showAns (ElemSpec era a
s1, a
run1, ElemSpec era a
s2, a
run2, a
v, a
run3, ElemSpec era a
s3) =
        [String] -> String
unlines
          [ String
"\ns1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
s1
          , String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a era. ElemSpec era a -> Size
sizeForElemSpec ElemSpec era a
s1)
          , String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
s2
          , String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a era. ElemSpec era a -> Size
sizeForElemSpec ElemSpec era a
s2)
          , String
"s1 <> s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era a
s3
          , String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a era. ElemSpec era a -> Size
sizeForElemSpec ElemSpec era a
s3)
          , String
"v = genFromElemSpec (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
v
          , String
"runElemSpec v s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run1
          , String
"runElemSpec v s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run2
          , String
"runElemSpec v (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run3
          ]
      pr :: (ElemSpec era a, Bool, ElemSpec era a, Bool, a, Bool,
 ElemSpec era a)
-> Maybe String
pr x :: (ElemSpec era a, Bool, ElemSpec era a, Bool, a, Bool,
 ElemSpec era a)
x@(ElemSpec era a
_, Bool
a, ElemSpec era a
_, Bool
b, a
_, Bool
c, ElemSpec era a
_) = if Bool -> Bool
not (Bool
a Bool -> Bool -> Bool
&& Bool
b Bool -> Bool -> Bool
&& Bool
c) then forall a. a -> Maybe a
Just (forall {a} {a} {a} {a} {era} {a} {era} {a} {era} {a}.
(Show a, Show a, Show a, Show a) =>
(ElemSpec era a, a, ElemSpec era a, a, a, a, ElemSpec era a)
-> String
showAns (ElemSpec era a, Bool, ElemSpec era a, Bool, a, Bool,
 ElemSpec era a)
x) else forall a. Maybe a
Nothing
  let trips :: [(ElemSpec TT Word64, ElemSpec TT Word64, ElemSpec TT Word64)]
trips = [(ElemSpec TT Word64
x, ElemSpec TT Word64
y, ElemSpec TT Word64
m) | ElemSpec TT Word64
x <- [ElemSpec TT Word64]
xs, ElemSpec TT Word64
y <- [ElemSpec TT Word64]
ys, Just ElemSpec TT Word64
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent ElemSpec TT Word64
x ElemSpec TT Word64
y]]
  [(ElemSpec TT Word64, Bool, ElemSpec TT Word64, Bool, [Word64],
  Bool, ElemSpec TT Word64)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ElemSpec TT Word64, ElemSpec TT Word64, ElemSpec TT Word64)
-> Gen
     (ElemSpec TT Word64, Bool, ElemSpec TT Word64, Bool, [Word64],
      Bool, ElemSpec TT Word64)
check [(ElemSpec TT Word64, ElemSpec TT Word64, ElemSpec TT Word64)]
trips
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (Size
size, forall (t :: * -> *) a. Foldable t => t a -> Int
length [(ElemSpec TT Word64, ElemSpec TT Word64, ElemSpec TT Word64)]
trips, forall a. [Maybe a] -> [a]
Maybe.catMaybes (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {era} {a} {era} {a} {era} {a}.
Show a =>
(ElemSpec era a, Bool, ElemSpec era a, Bool, a, Bool,
 ElemSpec era a)
-> Maybe String
pr [(ElemSpec TT Word64, Bool, ElemSpec TT Word64, Bool, [Word64],
  Bool, ElemSpec TT Word64)]
ts))

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

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

-- | Specs for lists have two parts, the Size, and the elements
data ListSpec era t where
  ListSpec :: Size -> ElemSpec era t -> ListSpec era t
  ListNever :: [String] -> ListSpec era t

instance Show (ListSpec era a) where
  show :: ListSpec era a -> String
show = forall era a. ListSpec era a -> String
showListSpec

instance Era era => Semigroup (ListSpec era a) where
  <> :: ListSpec era a -> ListSpec era a -> ListSpec era a
(<>) = forall era a.
Era era =>
ListSpec era a -> ListSpec era a -> ListSpec era a
mergeListSpec

instance Era era => Monoid (ListSpec era a) where
  mempty :: ListSpec era a
mempty = forall era t. Size -> ElemSpec era t -> ListSpec era t
ListSpec Size
SzAny forall era t. ElemSpec era t
ElemAny

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

showListSpec :: ListSpec era a -> String
showListSpec :: forall era a. ListSpec era a -> String
showListSpec (ListSpec Size
s ElemSpec era a
xs) = [String] -> String
sepsP [String
"ListSpec", forall a. Show a => a -> String
show Size
s, forall a. Show a => a -> String
show ElemSpec era a
xs]
showListSpec (ListNever [String]
_) = String
"ListNever"

mergeListSpec :: Era era => ListSpec era a -> ListSpec era a -> ListSpec era a
mergeListSpec :: forall era a.
Era era =>
ListSpec era a -> ListSpec era a -> ListSpec era a
mergeListSpec (ListNever [String]
xs) (ListNever [String]
ys) = forall era t. [String] -> ListSpec era t
ListNever ([String]
xs forall a. [a] -> [a] -> [a]
++ [String]
ys)
mergeListSpec (ListNever [String]
xs) (ListSpec Size
_ ElemSpec era a
_) = forall era t. [String] -> ListSpec era t
ListNever [String]
xs
mergeListSpec (ListSpec Size
_ ElemSpec era a
_) (ListNever [String]
xs) = forall era t. [String] -> ListSpec era t
ListNever [String]
xs
mergeListSpec a :: ListSpec era a
a@(ListSpec Size
s1 ElemSpec era a
e1) b :: ListSpec era a
b@(ListSpec Size
s2 ElemSpec era a
e2) =
  case ElemSpec era a
e1 forall a. Semigroup a => a -> a -> a
<> ElemSpec era a
e2 of
    ElemNever [String]
xs ->
      forall era t. [String] -> ListSpec era t
ListNever ([String
"The ListSpec's are inconsistent.", String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec era a
a, String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec era a
b] forall a. [a] -> [a] -> [a]
++ [String]
xs)
    ElemSpec era a
e3 -> forall x. LiftT x => Typed x -> x
dropT (forall a. String -> Typed a -> Typed a
explain (String
"While merging\n  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec era a
a forall a. [a] -> [a] -> [a]
++ String
"\n  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec era a
b) forall a b. (a -> b) -> a -> b
$ forall era t. Size -> ElemSpec era t -> Typed (ListSpec era t)
listSpec (Size
s1 forall a. Semigroup a => a -> a -> a
<> Size
s2) ElemSpec era a
e3)

-- | Test the size consistency while building a ListSpec
listSpec :: Size -> ElemSpec era t -> Typed (ListSpec era t)
listSpec :: forall era t. Size -> ElemSpec era t -> Typed (ListSpec era t)
listSpec Size
sz1 ElemSpec era t
el = case (Size
sz1 forall a. Semigroup a => a -> a -> a
<> Size
sz2) of
  SzNever [String]
xs ->
    forall a. [String] -> Typed a
failT
      ( [ String
"Creating " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era t. Size -> ElemSpec era t -> ListSpec era t
ListSpec Size
sz1 ElemSpec era t
el) forall a. [a] -> [a] -> [a]
++ String
" fails."
        , String
"It has size inconsistencies."
        , String
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec era t
el forall a. [a] -> [a] -> [a]
++ String
" has size " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
sz2
        , String
"  " forall a. [a] -> [a] -> [a]
++ String
"the expected size is " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
sz1
        ]
          forall a. [a] -> [a] -> [a]
++ [String]
xs
      )
  Size
size -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era t. Size -> ElemSpec era t -> ListSpec era t
ListSpec Size
size ElemSpec era t
el)
  where
    sz2 :: Size
sz2 = forall a era. ElemSpec era a -> Size
sizeForElemSpec ElemSpec era t
el

sizeForListSpec :: ListSpec era t -> Size
sizeForListSpec :: forall era t. ListSpec era t -> Size
sizeForListSpec (ListSpec Size
sz ElemSpec era t
_) = Size
sz
sizeForListSpec (ListNever [String]
_) = Size
SzAny

runListSpec :: [a] -> ListSpec era a -> Bool
runListSpec :: forall a era. [a] -> ListSpec era a -> Bool
runListSpec [a]
xs ListSpec era a
spec = case ListSpec era a
spec of
  ListNever [String]
_ -> Bool
False
  ListSpec Size
sx ElemSpec era a
es -> Int -> Size -> Bool
runSize (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs) Size
sx Bool -> Bool -> Bool
&& forall a era. [a] -> ElemSpec era a -> Bool
runElemSpec [a]
xs ElemSpec era a
es

genListSpec ::
  forall w era.
  Adds w =>
  Rep era w ->
  -- Rep era c ->
  SomeLens era w ->
  Size ->
  Gen (ListSpec era w)
genListSpec :: forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ListSpec era w)
genListSpec Rep era w
repw SomeLens era w
l Size
size = do
  ElemSpec era w
e <- forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ElemSpec era w)
genElemSpec Rep era w
repw SomeLens era w
l Size
size
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era t. Size -> ElemSpec era t -> ListSpec era t
ListSpec Size
size ElemSpec era w
e)

genFromListSpec ::
  forall era r.
  [String] ->
  Gen r ->
  ListSpec era r ->
  Gen [r]
genFromListSpec :: forall era r. [String] -> Gen r -> ListSpec era r -> Gen [r]
genFromListSpec [String]
_ Gen r
_ (ListNever [String]
xs) = forall a. HasCallStack => String -> [String] -> a
errorMess String
"ListNever in genFromListSpec" [String]
xs
genFromListSpec [String]
msgs Gen r
genr (ListSpec Size
size ElemSpec era r
e) = do
  Int
n <- Size -> Gen Int
genFromSize Size
size
  forall era r. [String] -> Gen r -> Int -> ElemSpec era r -> Gen [r]
genFromElemSpec (String
"genFromListSpec" forall a. a -> [a] -> [a]
: [String]
msgs) Gen r
genr Int
n ElemSpec era r
e

-- List and Elem tests

testSoundElemSpec :: Gen Property
testSoundElemSpec :: Gen Property
testSoundElemSpec = do
  Size
size <- Gen Size
genSize
  ElemSpec TT Word64
spec <- forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ElemSpec era w)
genElemSpec forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Size
size
  Int
n <- Size -> Gen Int
genFromSize Size
size
  [Word64]
list <-
    forall era r. [String] -> Gen r -> Int -> ElemSpec era r -> Gen [r]
genFromElemSpec @TT [String
"testSoundElemSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec TT Word64
spec forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n] (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) Int
n ElemSpec 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
"size=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
size forall a. [a] -> [a] -> [a]
++ String
"\nspec=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ElemSpec TT Word64
spec forall a. [a] -> [a] -> [a]
++ String
"\nlist=" forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall era c. Rep era c -> Rep era [c]
ListR forall era. Rep era Word64
Word64R) [Word64]
list)
      (forall a era. [a] -> ElemSpec era a -> Bool
runElemSpec [Word64]
list ElemSpec TT Word64
spec)

testSoundListSpec :: Gen Property
testSoundListSpec :: Gen Property
testSoundListSpec = do
  Size
size <- Gen Size
genSize
  ListSpec TT Word64
spec <- forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ListSpec era w)
genListSpec forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Size
size
  [Word64]
list <- forall era r. [String] -> Gen r -> ListSpec era r -> Gen [r]
genFromListSpec @TT [String
"testSoundListSpec"] (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
1000)) ListSpec 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 ListSpec TT Word64
spec forall a. [a] -> [a] -> [a]
++ String
"\nlist=" forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall era c. Rep era c -> Rep era [c]
ListR forall era. Rep era Word64
Word64R) [Word64]
list)
      (forall a era. [a] -> ListSpec era a -> Bool
runListSpec [Word64]
list ListSpec TT Word64
spec)

manyMergeListSpec :: Gen (Size, Int, [String])
manyMergeListSpec :: Gen (Size, Int, [String])
manyMergeListSpec = do
  Size
size <- Gen Size
genSize
  [ListSpec TT Word64]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
40 (forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ListSpec era w)
genListSpec forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Size
size)
  [ListSpec TT Word64]
ys <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
40 (forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ListSpec era w)
genListSpec forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Size
size)
  let check :: (ListSpec TT Word64, ListSpec TT Word64, ListSpec TT Word64)
-> Gen
     (ListSpec TT Word64, Bool, ListSpec TT Word64, Bool, [Word64],
      Bool, ListSpec TT Word64)
check (ListSpec TT Word64
x, ListSpec TT Word64
y, ListSpec TT Word64
m) = do
        let msize :: Size
msize = forall era t. ListSpec era t -> Size
sizeForListSpec ListSpec TT Word64
m
        Int
i <- Size -> Gen Int
genFromSize Size
msize
        let wordsX :: [String]
wordsX =
              [ String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
msize
              , String
"s1<>s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec TT Word64
m
              , String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era t. ListSpec era t -> Size
sizeForListSpec ListSpec TT Word64
x)
              , String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec TT Word64
x
              , String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era t. ListSpec era t -> Size
sizeForListSpec ListSpec TT Word64
y)
              , String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec TT Word64
y
              , String
"GenFromListSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" size=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Size
size
              ]
        [Word64]
z <- forall era r. [String] -> Gen r -> ListSpec era r -> Gen [r]
genFromListSpec @TT [String]
wordsX (forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
100)) ListSpec TT Word64
m
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (ListSpec TT Word64
x, forall a era. [a] -> ListSpec era a -> Bool
runListSpec [Word64]
z ListSpec TT Word64
x, ListSpec TT Word64
y, forall a era. [a] -> ListSpec era a -> Bool
runListSpec [Word64]
z ListSpec TT Word64
y, [Word64]
z, forall a era. [a] -> ListSpec era a -> Bool
runListSpec [Word64]
z ListSpec TT Word64
m, ListSpec TT Word64
m)
      showAns :: (ListSpec era t, a, ListSpec era t, a, a, a, ListSpec era t)
-> String
showAns (ListSpec era t
s1, a
run1, ListSpec era t
s2, a
run2, a
v, a
run3, ListSpec era t
s3) =
        [String] -> String
unlines
          [ String
"\ns1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec era t
s1
          , String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era t. ListSpec era t -> Size
sizeForListSpec ListSpec era t
s1)
          , String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec era t
s2
          , String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era t. ListSpec era t -> Size
sizeForListSpec ListSpec era t
s2)
          , String
"s1 <> s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListSpec era t
s3
          , String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era t. ListSpec era t -> Size
sizeForListSpec ListSpec era t
s3)
          , String
"v = genFromListSpec (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
v
          , String
"runListSpec v s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run1
          , String
"runListSpec v s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run2
          , String
"runListSpec v (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run3
          ]
      pr :: (ListSpec era t, Bool, ListSpec era t, Bool, a, Bool,
 ListSpec era t)
-> Maybe String
pr x :: (ListSpec era t, Bool, ListSpec era t, Bool, a, Bool,
 ListSpec era t)
x@(ListSpec era t
_, Bool
a, ListSpec era t
_, Bool
b, a
_, Bool
c, ListSpec era t
_) = if Bool -> Bool
not (Bool
a Bool -> Bool -> Bool
&& Bool
b Bool -> Bool -> Bool
&& Bool
c) then forall a. a -> Maybe a
Just (forall {a} {a} {a} {a} {era} {t} {era} {t} {era} {t}.
(Show a, Show a, Show a, Show a) =>
(ListSpec era t, a, ListSpec era t, a, a, a, ListSpec era t)
-> String
showAns (ListSpec era t, Bool, ListSpec era t, Bool, a, Bool,
 ListSpec era t)
x) else forall a. Maybe a
Nothing
  let trips :: [(ListSpec TT Word64, ListSpec TT Word64, ListSpec TT Word64)]
trips = [(ListSpec TT Word64
x, ListSpec TT Word64
y, ListSpec TT Word64
m) | ListSpec TT Word64
x <- [ListSpec TT Word64]
xs, ListSpec TT Word64
y <- [ListSpec TT Word64]
ys, Just ListSpec TT Word64
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent ListSpec TT Word64
x ListSpec TT Word64
y]]
  [(ListSpec TT Word64, Bool, ListSpec TT Word64, Bool, [Word64],
  Bool, ListSpec TT Word64)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ListSpec TT Word64, ListSpec TT Word64, ListSpec TT Word64)
-> Gen
     (ListSpec TT Word64, Bool, ListSpec TT Word64, Bool, [Word64],
      Bool, ListSpec TT Word64)
check [(ListSpec TT Word64, ListSpec TT Word64, ListSpec TT Word64)]
trips
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (Size
size, forall (t :: * -> *) a. Foldable t => t a -> Int
length [(ListSpec TT Word64, ListSpec TT Word64, ListSpec TT Word64)]
trips, forall a. [Maybe a] -> [a]
Maybe.catMaybes (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {era} {t} {era} {t} {era} {t}.
Show a =>
(ListSpec era t, Bool, ListSpec era t, Bool, a, Bool,
 ListSpec era t)
-> Maybe String
pr [(ListSpec TT Word64, Bool, ListSpec TT Word64, Bool, [Word64],
  Bool, ListSpec TT Word64)]
ts))

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

-- ================================================
-- Synthetic classes used to control the size of
-- things in the tests.

class (Arbitrary t, Adds t) => TestAdd t where
  anyAdds :: Gen t
  pos :: Gen t

instance TestAdd Word64 where
  anyAdds :: Gen Word64
anyAdds = forall a. Random a => (a, a) -> Gen a
choose (Word64
0, Word64
12)
  pos :: Gen Word64
pos = forall a. Random a => (a, a) -> Gen a
choose (Word64
1, Word64
12)

instance TestAdd Coin where
  anyAdds :: Gen Coin
anyAdds = Integer -> Coin
Coin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Integer
0, Integer
8)
  pos :: Gen Coin
pos = Integer -> Coin
Coin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Integer
1, Integer
8)

instance TestAdd Int where
  anyAdds :: Gen Int
anyAdds = (Int, Int) -> Gen Int
chooseInt (Int
0, Int
atMostAny)
  pos :: Gen Int
pos = (Int, Int) -> Gen Int
chooseInt (Int
1, Int
atMostAny)

-- =============================================
-- Some simple generators tied to TestAdd class

-- | Only the size of the set uses TestAdd
genSet :: Ord t => Int -> Gen t -> Gen (Set t)
genSet :: forall t. Ord t => Int -> Gen t -> Gen (Set t)
genSet Int
n Gen t
gen = do
  [t]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
20 Gen t
gen
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Ord a => [a] -> Set a
Set.fromList (forall a. Int -> [a] -> [a]
take Int
n (forall a. Eq a => [a] -> [a]
List.nub [t]
xs)))

testSet :: (Ord t, TestAdd t) => Gen (Set t)
testSet :: forall t. (Ord t, TestAdd t) => Gen (Set t)
testSet = do
  Int
n <- forall t. TestAdd t => Gen t
pos @Int
  forall a. Ord a => [a] -> Set a
Set.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n forall t. TestAdd t => Gen t
anyAdds

someSet :: Ord t => Gen t -> Gen (Set t)
someSet :: forall t. Ord t => Gen t -> Gen (Set t)
someSet Gen t
g = do
  Int
n <- forall t. TestAdd t => Gen t
pos @Int
  forall a. Ord a => [a] -> Set a
Set.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n Gen t
g

someMap :: forall era t d. (Ord d, TestAdd t) => Rep era d -> Gen (Map d t)
someMap :: forall era t d. (Ord d, TestAdd t) => Rep era d -> Gen (Map d t)
someMap Rep era d
r = do
  Int
n <- forall t. TestAdd t => Gen t
pos @Int
  [t]
rs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n forall t. TestAdd t => Gen t
anyAdds
  [d]
ds <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n (forall era b. Rep era b -> Gen b
genRep Rep era d
r)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [d]
ds [t]
rs)

-- ===================================
-- Some proto-tests, to be fixed soon

aMap :: Era era => Gen (MapSpec era Int Word64)
aMap :: forall era. Era era => Gen (MapSpec era Int Word64)
aMap = forall era dom w.
(Ord dom, Era era, Ord w, Adds w) =>
Gen dom
-> Rep era dom
-> Rep era w
-> SomeLens era w
-> Int
-> Gen (MapSpec era dom w)
genMapSpec ((Int, Int) -> Gen Int
chooseInt (Int
1, Int
1000)) forall era. Rep era Int
IntR forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) Int
4

testm :: Gen (MapSpec TT Int Word64)
testm :: Gen (MapSpec TT Int Word64)
testm = do
  MapSpec TT Int Word64
a <- forall era. Era era => Gen (MapSpec era Int Word64)
aMap @TT
  MapSpec TT Int Word64
b <- forall era. Era era => Gen (MapSpec era Int Word64)
aMap
  forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall x. LiftT x => x -> Typed x
liftT (MapSpec TT Int Word64
a forall a. Semigroup a => a -> a -> a
<> MapSpec TT Int Word64
b))

aList :: Gen (ListSpec era Word64)
aList :: forall era. Gen (ListSpec era Word64)
aList = Gen Size
genSize forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ListSpec era w)
genListSpec forall era. Rep era Word64
Word64R (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL)

testl :: Gen (ListSpec TT Word64)
testl :: Gen (ListSpec TT Word64)
testl = do
  ListSpec TT Word64
a <- forall era. Gen (ListSpec era Word64)
aList @TT
  ListSpec TT Word64
b <- forall era. Gen (ListSpec era Word64)
aList
  forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall x. LiftT x => x -> Typed x
liftT (ListSpec TT Word64
a forall a. Semigroup a => a -> a -> a
<> ListSpec TT Word64
b))

-- =======================================================================
-- Operations on AddsSpec (defined in Classes.hs)

testV :: Era era => V era DeltaCoin
testV :: forall era. Era era => V era DeltaCoin
testV = (forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
"x" forall era. Rep era DeltaCoin
DeltaCoinR forall era s t. Access era s t
No)

genSumsTo :: Era era => Gen (Pred era)
genSumsTo :: forall era. Era era => Gen (Pred era)
genSumsTo = do
  OrdCond
c <- Gen OrdCond
genOrdCond
  let v :: Term era DeltaCoin
v = forall era t. V era t -> Term era t
Var forall era. Era era => V era DeltaCoin
testV
  Term era DeltaCoin
rhs <- (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era DeltaCoin
DeltaCoinR forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> DeltaCoin
DeltaCoin) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (-Integer
10, Integer
10)
  Term era DeltaCoin
lhs <- (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era DeltaCoin
DeltaCoinR forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> DeltaCoin
DeltaCoin) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (-Integer
10, Integer
10)
  forall a. HasCallStack => [a] -> Gen a
elements
    [forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. a -> Either a b
Left (Integer -> DeltaCoin
DeltaCoin Integer
1)) Term era DeltaCoin
v OrdCond
c [forall era c. Term era c -> Sum era c
One Term era DeltaCoin
rhs], forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. a -> Either a b
Left (Integer -> DeltaCoin
DeltaCoin Integer
1)) Term era DeltaCoin
lhs OrdCond
c [forall era c. Term era c -> Sum era c
One Term era DeltaCoin
rhs, forall era c. Term era c -> Sum era c
One Term era DeltaCoin
v]]

solveSumsTo :: Pred era -> AddsSpec DeltaCoin
solveSumsTo :: forall era. Pred era -> AddsSpec DeltaCoin
solveSumsTo (SumsTo Direct c
_ (Lit Rep era c
DeltaCoinR c
n) OrdCond
cond [One (Lit Rep era c
DeltaCoinR c
m), One (Var (V String
nam Rep era c
_ Access era s c
_))]) =
  forall a c.
Adds a =>
[String] -> a -> OrdCond -> a -> String -> AddsSpec c
varOnRight @DeltaCoin [String
"solveSumsTo"] c
n OrdCond
cond c
m String
nam
solveSumsTo (SumsTo Direct c
_ (Var (V String
nam Rep era c
DeltaCoinR Access era s c
_)) OrdCond
cond [One (Lit Rep era c
DeltaCoinR c
m)]) =
  forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
nam OrdCond
cond c
m
solveSumsTo Pred era
x = forall c. [String] -> AddsSpec c
AddsSpecNever [String
"solveSumsTo " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Pred era
x]

condReverse :: Gen Property
condReverse :: Gen Property
condReverse = do
  Pred TT
predicate <- forall era. Era era => Gen (Pred era)
genSumsTo
  let addsSpec :: AddsSpec DeltaCoin
addsSpec = forall era. Pred era -> AddsSpec DeltaCoin
solveSumsTo Pred TT
predicate
  let msgs :: [String]
msgs = [String
"condFlip", forall a. Show a => a -> String
show Pred TT
predicate, forall a. Show a => a -> String
show AddsSpec DeltaCoin
addsSpec]
  Int
n <- forall c. [String] -> AddsSpec c -> Gen Int
genFromAddsSpec [String]
msgs AddsSpec DeltaCoin
addsSpec
  let env :: Env TT
env = forall era t. V era t -> t -> Env era -> Env era
storeVar forall era. Era era => V era DeltaCoin
testV (forall x. Adds x => [String] -> Int -> x
fromI (forall a. Show a => a -> String
show Int
n forall a. a -> [a] -> [a]
: [String]
msgs) Int
n) forall era. Env era
emptyEnv
  case forall x. Typed x -> Either [String] x
runTyped (forall era. Env era -> Pred era -> Typed Bool
runPred @(BabbageEra Standard) Env TT
env Pred TT
predicate) of
    Right Bool
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines (forall a. Show a => a -> String
show Int
n forall a. a -> [a] -> [a]
: [String]
msgs)) Bool
x)
    Left [String]
xs -> forall a. HasCallStack => String -> [String] -> a
errorMess String
"runTyped in condFlip fails" ([String]
xs forall a. [a] -> [a] -> [a]
++ (forall a. Show a => a -> String
show Int
n forall a. a -> [a] -> [a]
: [String]
msgs))

genAddsSpec :: forall c. Adds c => Gen (AddsSpec c)
genAddsSpec :: forall c. Adds c => Gen (AddsSpec c)
genAddsSpec = do
  String
v <- forall a. HasCallStack => [a] -> Gen a
elements [String
"x", String
"y"]
  OrdCond
c <- Gen OrdCond
genOrdCond
  c
rhs <- forall x. Adds x => [String] -> Int -> x
fromI @c [String
"genAddsSpec"] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose @Int (-Int
25, Int
25)
  c
lhs <- forall x. Adds x => [String] -> Int -> x
fromI @c [String
"genAddsSpec"] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose @Int (-Int
25, Int
25)
  forall a. HasCallStack => [a] -> Gen a
elements [forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
v OrdCond
c c
rhs, forall a c.
Adds a =>
[String] -> a -> OrdCond -> a -> String -> AddsSpec c
varOnRight [String
"genAddsSpec"] c
lhs OrdCond
c c
rhs String
v]

genNonNegAddsSpec :: forall c. Adds c => Gen (AddsSpec c)
genNonNegAddsSpec :: forall c. Adds c => Gen (AddsSpec c)
genNonNegAddsSpec = do
  String
v <- forall a. HasCallStack => [a] -> Gen a
elements [String
"x", String
"y"]
  OrdCond
c <- Gen OrdCond
genOrdCond
  Int
lhs <- forall a. Random a => (a, a) -> Gen a
choose @Int (Int
10, Int
30)
  Int
rhs <- forall a. Random a => (a, a) -> Gen a
choose @Int (Int
1, Int
lhs forall a. Num a => a -> a -> a
- Int
1)
  let lhs' :: Int
lhs' = case OrdCond
c of
        OrdCond
LTH -> Int
lhs forall a. Num a => a -> a -> a
+ Int
1
        OrdCond
_ -> Int
lhs
      fromX :: Int -> c
fromX Int
x = forall x. Adds x => [String] -> Int -> x
fromI @c [String
"genNonNegAddsSpec"] Int
x
  forall a. HasCallStack => [a] -> Gen a
elements [forall a c. Adds a => String -> OrdCond -> a -> AddsSpec c
varOnLeft String
v OrdCond
c forall a b. (a -> b) -> a -> b
$ Int -> c
fromX Int
rhs, forall a c.
Adds a =>
[String] -> a -> OrdCond -> a -> String -> AddsSpec c
varOnRight [String
"genNonNegAddsSpec"] (Int -> c
fromX Int
lhs') OrdCond
c (Int -> c
fromX Int
rhs) String
v]

genOrdCond :: Gen OrdCond
genOrdCond :: Gen OrdCond
genOrdCond = forall a. HasCallStack => [a] -> Gen a
elements [OrdCond
EQL, OrdCond
LTH, OrdCond
LTE, OrdCond
GTH, OrdCond
GTE]

runAddsSpec :: forall c. Adds c => c -> AddsSpec c -> Bool
runAddsSpec :: forall c. Adds c => c -> AddsSpec c -> Bool
runAddsSpec c
c (AddsSpecSize String
_ Size
size) = Int -> Size -> Bool
runSize (forall x. Adds x => x -> Int
toI c
c) Size
size
runAddsSpec c
_ AddsSpec c
AddsSpecAny = Bool
True
runAddsSpec c
_ (AddsSpecNever [String]
_) = Bool
False

-- | Not sure how to interpret this? As the possible totals that make the implicit OrdCond True?
sizeForAddsSpec :: AddsSpec c -> Size
sizeForAddsSpec :: forall c. AddsSpec c -> Size
sizeForAddsSpec (AddsSpecSize String
_ Size
s) = Size
s
sizeForAddsSpec AddsSpec c
AddsSpecAny = Size
SzAny
sizeForAddsSpec (AddsSpecNever [String]
xs) = [String] -> Size
SzNever [String]
xs

tryManyAddsSpec ::
  Gen (AddsSpec Int) -> ([String] -> AddsSpec Int -> Gen Int) -> Gen (Int, [String])
tryManyAddsSpec :: Gen (AddsSpec Int)
-> ([String] -> AddsSpec Int -> Gen Int) -> Gen (Int, [String])
tryManyAddsSpec Gen (AddsSpec Int)
genSum [String] -> AddsSpec Int -> Gen Int
genFromSum = do
  [AddsSpec Int]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
25 Gen (AddsSpec Int)
genSum
  [AddsSpec Int]
ys <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
25 Gen (AddsSpec Int)
genSum
  let check :: (AddsSpec Int, AddsSpec Int, AddsSpec Int)
-> Gen
     (AddsSpec Int, Bool, AddsSpec Int, Bool, Int, Bool, AddsSpec Int)
check (AddsSpec Int
x, AddsSpec Int
y, AddsSpec Int
m) = do
        Int
z <- [String] -> AddsSpec Int -> Gen Int
genFromSum [String
"test tryManyAddsSpec"] AddsSpec Int
m
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (AddsSpec Int
x, forall c. Adds c => c -> AddsSpec c -> Bool
runAddsSpec Int
z AddsSpec Int
x, AddsSpec Int
y, forall c. Adds c => c -> AddsSpec c -> Bool
runAddsSpec Int
z AddsSpec Int
y, Int
z, forall c. Adds c => c -> AddsSpec c -> Bool
runAddsSpec Int
z AddsSpec Int
m, AddsSpec Int
m)
      showAns :: (AddsSpec c, Bool, AddsSpec c, Bool, Int, Bool, AddsSpec c) -> String
      showAns :: forall c.
(AddsSpec c, Bool, AddsSpec c, Bool, Int, Bool, AddsSpec c)
-> String
showAns (AddsSpec c
s1, Bool
run1, AddsSpec c
s2, Bool
run2, Int
v, Bool
run3, AddsSpec c
s3) =
        [String] -> String
unlines
          [ String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AddsSpec c
s1
          , String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AddsSpec c
s2
          , String
"s1 <> s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AddsSpec c
s3
          , String
"v = genFromAdsSpec (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
v
          , String
"runAddsSpec s1 v = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Bool
run1
          , String
"runAddsSpec s2 v = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Bool
run2
          , String
"runAddsSpec (s1 <> s2) v = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Bool
run3
          ]
      pr :: (AddsSpec c, Bool, AddsSpec c, Bool, Int, Bool, AddsSpec c)
-> Maybe String
pr x :: (AddsSpec c, Bool, AddsSpec c, Bool, Int, Bool, AddsSpec c)
x@(AddsSpec c
_, Bool
a, AddsSpec c
_, Bool
b, Int
_, Bool
c, AddsSpec c
_) = if Bool -> Bool
not (Bool
a Bool -> Bool -> Bool
&& Bool
b Bool -> Bool -> Bool
&& Bool
c) then forall a. a -> Maybe a
Just (forall c.
(AddsSpec c, Bool, AddsSpec c, Bool, Int, Bool, AddsSpec c)
-> String
showAns (AddsSpec c, Bool, AddsSpec c, Bool, Int, Bool, AddsSpec c)
x) else forall a. Maybe a
Nothing
  let trips :: [(AddsSpec Int, AddsSpec Int, AddsSpec Int)]
trips = [(AddsSpec Int
x, AddsSpec Int
y, AddsSpec Int
m) | AddsSpec Int
x <- [AddsSpec Int]
xs, AddsSpec Int
y <- [AddsSpec Int]
ys, Just AddsSpec Int
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent AddsSpec Int
x AddsSpec Int
y]]
  [(AddsSpec Int, Bool, AddsSpec Int, Bool, Int, Bool, AddsSpec Int)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (AddsSpec Int, AddsSpec Int, AddsSpec Int)
-> Gen
     (AddsSpec Int, Bool, AddsSpec Int, Bool, Int, Bool, AddsSpec Int)
check [(AddsSpec Int, AddsSpec Int, AddsSpec Int)]
trips
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(AddsSpec Int, AddsSpec Int, AddsSpec Int)]
trips, forall a. [Maybe a] -> [a]
Maybe.catMaybes (forall a b. (a -> b) -> [a] -> [b]
map forall {c}.
(AddsSpec c, Bool, AddsSpec c, Bool, Int, Bool, AddsSpec c)
-> Maybe String
pr [(AddsSpec Int, Bool, AddsSpec Int, Bool, Int, Bool, AddsSpec Int)]
ts))

reportManyAddsSpec :: IO ()
reportManyAddsSpec :: IO ()
reportManyAddsSpec = do
  (Int
passed, [String]
bad) <- forall a. Gen a -> IO a
generate (Gen (AddsSpec Int)
-> ([String] -> AddsSpec Int -> Gen Int) -> Gen (Int, [String])
tryManyAddsSpec forall c. Adds c => Gen (AddsSpec c)
genAddsSpec forall c. [String] -> AddsSpec c -> Gen Int
genFromAddsSpec)
  if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
bad
    then String -> IO ()
putStrLn (String
"passed " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
passed forall a. [a] -> [a] -> [a]
++ String
" tests.")
    else do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn [String]
bad; forall a. HasCallStack => String -> a
error String
"TestFails"

reportManyNonNegAddsSpec :: IO ()
reportManyNonNegAddsSpec :: IO ()
reportManyNonNegAddsSpec = do
  (Int
passed, [String]
bad) <- forall a. Gen a -> IO a
generate (Gen (AddsSpec Int)
-> ([String] -> AddsSpec Int -> Gen Int) -> Gen (Int, [String])
tryManyAddsSpec forall c. Adds c => Gen (AddsSpec c)
genNonNegAddsSpec forall c. [String] -> AddsSpec c -> Gen Int
genFromNonNegAddsSpec)
  if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
bad
    then String -> IO ()
putStrLn (String
"passed " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
passed forall a. [a] -> [a] -> [a]
++ String
" tests.")
    else do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn [String]
bad; forall a. HasCallStack => String -> a
error String
"TestFails"

testSoundNonNegAddsSpec :: Gen Property
testSoundNonNegAddsSpec :: Gen Property
testSoundNonNegAddsSpec = do
  AddsSpec Int
spec <- forall c. Adds c => Gen (AddsSpec c)
genNonNegAddsSpec @Int
  Int
c <- forall c. [String] -> AddsSpec c -> Gen Int
genFromNonNegAddsSpec [String
"testSoundAddsSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AddsSpec Int
spec] AddsSpec Int
spec
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => String -> prop -> Property
counterexample
      (String
"AddsSpec=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AddsSpec Int
spec forall a. [a] -> [a] -> [a]
++ String
"\ngenerated value " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
c)
      (forall c. Adds c => c -> AddsSpec c -> Bool
runAddsSpec Int
c AddsSpec Int
spec)

testSoundAddsSpec :: Gen Property
testSoundAddsSpec :: Gen Property
testSoundAddsSpec = do
  AddsSpec DeltaCoin
spec <- forall c. Adds c => Gen (AddsSpec c)
genAddsSpec @DeltaCoin
  Int
c <- forall c. [String] -> AddsSpec c -> Gen Int
genFromAddsSpec [String
"testSoundAddsSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AddsSpec DeltaCoin
spec] AddsSpec DeltaCoin
spec
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => String -> prop -> Property
counterexample
      (String
"AddsSpec=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show AddsSpec DeltaCoin
spec forall a. [a] -> [a] -> [a]
++ String
"\ngenerated value " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
c)
      (forall c. Adds c => c -> AddsSpec c -> Bool
runAddsSpec (forall x. Adds x => [String] -> Int -> x
fromI [String
"testSoundAddsSpec"] Int
c) AddsSpec DeltaCoin
spec)

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

allSpecTests :: TestTree
allSpecTests :: TestTree
allSpecTests =
  String -> [TestTree] -> TestTree
testGroup
    String
"Spec tests"
    [ forall a. Testable a => String -> a -> TestTree
testProperty String
"reversing OrdCond" Gen Property
condReverse
    , String -> [TestTree] -> TestTree
testGroup
        String
"Size test"
        [ forall a. Testable a => String -> a -> TestTree
testProperty String
"test Size sound" Gen Bool
testSoundSize
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test genFromSize is non-negative" Gen Bool
testNonNegSize
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test merging Size" Gen Bool
testMergeSize
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test alternate merge Size" Gen Property
testMergeSize2
        ]
    , String -> [TestTree] -> TestTree
testGroup
        String
"RelSpec tests"
        [ forall a. Testable a => String -> a -> TestTree
testProperty String
"we generate consistent RelSpecs" Gen Property
testConsistentRel
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test RelSpec sound" Gen Property
testSoundRelSpec
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test mergeRelSpec" Gen Property
testMergeRelSpec
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test More consistent RelSpec" IO ()
reportManyMergeRelSpec
        ]
    , String -> [TestTree] -> TestTree
testGroup
        String
"RngSpec tests"
        [ forall a. Testable a => String -> a -> TestTree
testProperty String
"we generate consistent RngSpec" Gen Property
testConsistentRng
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test RngSpec sound" Gen Property
testSoundRngSpec
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test mergeRngSpec" Gen Property
testMergeRngSpec
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test More consistent RngSpec" IO ()
reportManyMergeRngSpec
        ]
    , String -> [TestTree] -> TestTree
testGroup
        String
"MapSpec tests"
        [ forall a. Testable a => String -> a -> TestTree
testProperty String
"test MapSpec sound" Gen Property
genMapSpecIsSound
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test More consistent MapSpec" IO ()
reportManyMergeMapSpec
        ]
    , String -> [TestTree] -> TestTree
testGroup
        String
"SetSpec tests"
        [ forall a. Testable a => String -> a -> TestTree
testProperty String
"test SetSpec sound" Gen Property
genSetSpecIsSound
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test More consistent SetSpec" IO ()
reportManyMergeSetSpec
        ]
    , String -> [TestTree] -> TestTree
testGroup
        String
"ListSpec tests"
        [ forall a. Testable a => String -> a -> TestTree
testProperty String
"test ElemSpec sound" Gen Property
testSoundElemSpec
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test consistent ElemSpec" IO ()
reportManyMergeElemSpec
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test ListSpec sound" Gen Property
testSoundListSpec
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test consistent ListSpec" IO ()
reportManyMergeListSpec
        ]
    , String -> [TestTree] -> TestTree
testGroup
        String
"AddsSpec tests"
        [ forall a. Testable a => String -> a -> TestTree
testProperty String
"test Sound MergeAddsSpec" IO ()
reportManyAddsSpec
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test Sound non-negative MergeAddsSpec" IO ()
reportManyNonNegAddsSpec
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test Sound non-negative AddsSpec" Gen Property
testSoundNonNegAddsSpec
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test Sound any AddsSpec" Gen Property
testSoundAddsSpec
        ]
    , String -> [TestTree] -> TestTree
testGroup
        String
"PairSpec test"
        [ forall a. Testable a => String -> a -> TestTree
testProperty String
"test sound PairSpec" Gen Property
testSoundPairSpec
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test ConsistentPair" Gen Property
testConsistentPair
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test merge PairSpec" Gen Property
testMergePairSpec
        , forall a. Testable a => String -> a -> TestTree
testProperty String
"test More consistent PairSpec" IO ()
reportManyMergePairSpec
        ]
    ]

main :: IO ()
main :: IO ()
main = TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$ TestTree
allSpecTests

-- :main --quickcheck-replay=740521

data PairSide = VarOnLeft | VarOnRight
  deriving (Int -> PairSide -> ShowS
[PairSide] -> ShowS
PairSide -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PairSide] -> ShowS
$cshowList :: [PairSide] -> ShowS
show :: PairSide -> String
$cshow :: PairSide -> String
showsPrec :: Int -> PairSide -> ShowS
$cshowsPrec :: Int -> PairSide -> ShowS
Show, PairSide -> PairSide -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PairSide -> PairSide -> Bool
$c/= :: PairSide -> PairSide -> Bool
== :: PairSide -> PairSide -> Bool
$c== :: PairSide -> PairSide -> Bool
Eq)

-- | A map 'm1' meets the '(PairSpec _ _ m2)' specification if every
--   (key,value) pair in 'm2' is in 'm1'.
data PairSpec era a b where
  PairSpec :: (Ord a, Eq b) => Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
  PairNever :: [String] -> PairSpec era a b
  PairAny :: PairSpec era a b

-- TODO Add a second map to PairSpec
-- PairSpec :: (Ord a, Eq b) => Rep era a -> Rep era b -> Map a b -> Maybe(Map a b) -> PairSpec era a b
-- This way (PairSpec d r m1 (Just m2))     Implies  m1 <= x <= m2,  where (<=) is the Map.isSubmapOf relation
-- This way (PairSpec d r empty (Just m2))  Implies  x <= m2,
-- This way (PairSpec d r m1 Nothing)       Implies  m1 <= x         Note that Nothing denotes the Map that contains every pair
-- This way we can get rid of the PairSide argument, and make chains like m1 <= x <= m2,

anyPairSpec :: PairSpec era d r -> Bool
anyPairSpec :: forall era d r. PairSpec era d r -> Bool
anyPairSpec PairSpec era d r
PairAny = Bool
True
anyPairSpec (PairSpec Rep era d
_ Rep era r
_ PairSide
_ Map d r
m) = forall k a. Map k a -> Bool
Map.null Map d r
m
anyPairSpec PairSpec era d r
_ = Bool
False

instance Monoid (PairSpec era a b) where
  mempty :: PairSpec era a b
mempty = forall era a b. PairSpec era a b
PairAny

instance Semigroup (PairSpec era dom rng) where
  <> :: PairSpec era dom rng
-> PairSpec era dom rng -> PairSpec era dom rng
(<>) = forall era a b.
PairSpec era a b -> PairSpec era a b -> PairSpec era a b
mergePairSpec

instance Show (PairSpec era dom rng) where
  show :: PairSpec era dom rng -> String
show = forall era dom rng. PairSpec era dom rng -> String
showPairSpec

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

showPairSpec :: PairSpec era dom rng -> String
showPairSpec :: forall era dom rng. PairSpec era dom rng -> String
showPairSpec (PairNever [String]
_) = String
"PairNever"
showPairSpec PairSpec era dom rng
PairAny = String
"PairAny"
showPairSpec (PairSpec Rep era dom
dom Rep era rng
rng PairSide
side Map dom rng
mp) = [String] -> String
sepsP [String
"PairSpec", forall a. Show a => a -> String
show Rep era dom
dom, forall a. Show a => a -> String
show Rep era rng
rng, forall a. Show a => a -> String
show PairSide
side, forall e t. Rep e t -> t -> String
synopsis (forall c era b.
Ord c =>
Rep era c -> Rep era b -> Rep era (Map c b)
MapR Rep era dom
dom Rep era rng
rng) Map dom rng
mp]

mergePairSpec :: PairSpec era a b -> PairSpec era a b -> PairSpec era a b
mergePairSpec :: forall era a b.
PairSpec era a b -> PairSpec era a b -> PairSpec era a b
mergePairSpec (PairNever [String]
xs) (PairNever [String]
ys) = forall era a b. [String] -> PairSpec era a b
PairNever ([String]
xs forall a. [a] -> [a] -> [a]
++ [String]
ys)
mergePairSpec d :: PairSpec era a b
d@(PairNever [String]
_) PairSpec era a b
_ = PairSpec era a b
d
mergePairSpec PairSpec era a b
_ d :: PairSpec era a b
d@(PairNever [String]
_) = PairSpec era a b
d
mergePairSpec PairSpec era a b
PairAny PairSpec era a b
x = PairSpec era a b
x
mergePairSpec PairSpec era a b
x PairSpec era a b
PairAny = PairSpec era a b
x
mergePairSpec (PairSpec Rep era a
d Rep era b
r PairSide
VarOnRight Map a b
m1) (PairSpec Rep era a
_ Rep era b
_ PairSide
VarOnRight Map a b
m2) =
  let accum :: Either [String] (Map a b) -> a -> b -> Either [String] (Map a b)
accum (Right Map a b
zs) a
key b
v =
        case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
key Map a b
zs of
          Maybe b
Nothing -> forall a b. b -> Either a b
Right (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
key b
v Map a b
zs)
          Just b
u ->
            if b
u forall a. Eq a => a -> a -> Bool
== b
v
              then forall a b. b -> Either a b
Right (Map a b
zs)
              else
                forall a b. a -> Either a b
Left
                  [ String
"The PairSpecs with VarOnRight"
                  , String
"   " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
format (forall c era b.
Ord c =>
Rep era c -> Rep era b -> Rep era (Map c b)
MapR Rep era a
d Rep era b
r) Map a b
m1 forall a. [a] -> [a] -> [a]
++ String
" and"
                  , String
"   " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
format (forall c era b.
Ord c =>
Rep era c -> Rep era b -> Rep era (Map c b)
MapR Rep era a
d Rep era b
r) Map a b
m2
                  , String
" are inconsistent."
                  , String
"The key "
                      forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era a
d a
key
                      forall a. [a] -> [a] -> [a]
++ String
" has multiple values: "
                      forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era b
r b
v
                      forall a. [a] -> [a] -> [a]
++ String
" and "
                      forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era b
r b
u
                  ]
      accum (Left [String]
xs) a
_ b
_ = forall a b. a -> Either a b
Left [String]
xs
   in case forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' Either [String] (Map a b) -> a -> b -> Either [String] (Map a b)
accum (forall a b. b -> Either a b
Right Map a b
m1) Map a b
m2 of
        Left [String]
xs -> forall era a b. [String] -> PairSpec era a b
PairNever [String]
xs
        Right Map a b
m3 -> forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era a
d Rep era b
r PairSide
VarOnRight Map a b
m3
mergePairSpec (PairSpec Rep era a
d Rep era b
r PairSide
VarOnLeft Map a b
m1) (PairSpec Rep era a
_ Rep era b
_ PairSide
VarOnLeft Map a b
m2) =
  let accum :: Either [String] (Map a b) -> a -> b -> Either [String] (Map a b)
accum (Right Map a b
zs) a
key b
v =
        -- Testing that the instersection of the domains, map to the same range.
        case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
key Map a b
m1 of -- If that is True, we use this intersection as the new map
          Maybe b
Nothing -> forall a b. b -> Either a b
Right Map a b
zs
          Just b
u ->
            if b
u forall a. Eq a => a -> a -> Bool
== b
v
              then forall a b. b -> Either a b
Right (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
key b
u Map a b
zs)
              else
                forall a b. a -> Either a b
Left
                  [ String
"The PairSpecs with VarOnLeft"
                  , String
"   " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
format (forall c era b.
Ord c =>
Rep era c -> Rep era b -> Rep era (Map c b)
MapR Rep era a
d Rep era b
r) Map a b
m1 forall a. [a] -> [a] -> [a]
++ String
" and"
                  , String
"   " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
format (forall c era b.
Ord c =>
Rep era c -> Rep era b -> Rep era (Map c b)
MapR Rep era a
d Rep era b
r) Map a b
m2
                  , String
"are inconsistent."
                  , String
"The key "
                      forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era a
d a
key
                      forall a. [a] -> [a] -> [a]
++ String
" has multiple values: "
                      forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era b
r b
v
                      forall a. [a] -> [a] -> [a]
++ String
" and "
                      forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis (forall c era b.
Ord c =>
Rep era c -> Rep era b -> Rep era (Map c b)
MapR Rep era a
d Rep era b
r) Map a b
m1
                  ]
      accum (Left [String]
xs) a
_ b
_ = forall a b. a -> Either a b
Left [String]
xs
   in case forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' Either [String] (Map a b) -> a -> b -> Either [String] (Map a b)
accum (forall a b. b -> Either a b
Right forall k a. Map k a
Map.empty) Map a b
m2 of
        Left [String]
xs -> forall era a b. [String] -> PairSpec era a b
PairNever [String]
xs
        Right Map a b
m3 -> forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era a
d Rep era b
r PairSide
VarOnLeft Map a b
m3
mergePairSpec PairSpec era a b
a PairSpec era a b
b =
  forall era a b. [String] -> PairSpec era a b
PairNever
    [ String
"The PairSpecs"
    , String
"   " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era a b
a forall a. [a] -> [a] -> [a]
++ String
" and"
    , String
"   " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era a b
b
    , String
" are inconsistent."
    , String
"They have the var on different sides."
    ]

sizeForPairSpec :: PairSpec era dom rng -> Size
sizeForPairSpec :: forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec era dom rng
PairAny = Size
SzAny
sizeForPairSpec (PairNever [String]
msgs) = [String] -> Size
SzNever ([String]
msgs forall a. [a] -> [a] -> [a]
++ [String
"From sizeForPairSpec."])
sizeForPairSpec (PairSpec Rep era dom
_ Rep era rng
_ PairSide
VarOnRight Map dom rng
m) = Int -> Size
SzLeast (forall k a. Map k a -> Int
Map.size Map dom rng
m)
sizeForPairSpec (PairSpec Rep era dom
_ Rep era rng
_ PairSide
VarOnLeft Map dom rng
m) = Int -> Size
SzMost (forall k a. Map k a -> Int
Map.size Map dom rng
m)

runPairSpec :: (Ord dom, Eq rng) => Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec :: forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map dom rng
_ PairSpec era dom rng
PairAny = Bool
True
runPairSpec Map dom rng
_ (PairNever [String]
xs) = forall a. HasCallStack => String -> [String] -> a
errorMess String
"PairNever in call to runPairSpec" [String]
xs
runPairSpec Map dom rng
m1 (PairSpec Rep era dom
_ Rep era rng
_ PairSide
VarOnRight Map dom rng
m2) = forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
Map.isSubmapOf Map dom rng
m2 Map dom rng
m1
-- all pairs in m2 are in m1
-- So when we say (SubMap expr var) we store the pairs from expr in 'm2'
-- and insist that when solving 'var' it contains the pairs from 'm2' and possibly more pairs
runPairSpec Map dom rng
m1 (PairSpec Rep era dom
_ Rep era rng
_ PairSide
VarOnLeft Map dom rng
m2) = forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
Map.isSubmapOf Map dom rng
m1 Map dom rng
m2

genPairSpec ::
  forall era dom rng. (Ord dom, Eq rng) => Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec :: forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec Rep era dom
domr Rep era rng
rngr =
  forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
    [ (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era a b. PairSpec era a b
PairAny)
    , (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
domr Rep era rng
rngr PairSide
VarOnRight forall k a. Map k a
Map.empty))
    , (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
domr Rep era rng
rngr PairSide
VarOnLeft forall k a. Map k a
Map.empty))
    , (Int
4, forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
domr Rep era rng
rngr PairSide
VarOnRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall k a. k -> a -> Map k a
Map.singleton forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era b. Rep era b -> Gen b
genRep Rep era dom
domr forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era b. Rep era b -> Gen b
genRep Rep era rng
rngr))
    , (Int
4, forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
domr Rep era rng
rngr PairSide
VarOnLeft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall k a. k -> a -> Map k a
Map.singleton forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era b. Rep era b -> Gen b
genRep Rep era dom
domr forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era b. Rep era b -> Gen b
genRep Rep era rng
rngr))
    ,
      ( Int
4
      , do
          dom
d1 <- forall era b. Rep era b -> Gen b
genRep Rep era dom
domr
          dom
d2 <- forall era b. Rep era b -> Gen b
genRep Rep era dom
domr
          rng
r1 <- forall era b. Rep era b -> Gen b
genRep Rep era rng
rngr
          rng
r2 <- forall era b. Rep era b -> Gen b
genRep Rep era rng
rngr
          forall a. HasCallStack => [a] -> Gen a
elements
            [ forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
domr Rep era rng
rngr PairSide
VarOnRight (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(dom
d1, rng
r1), (dom
d2, rng
r2)])
            , forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
domr Rep era rng
rngr PairSide
VarOnRight (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(dom
d1, rng
r1), (dom
d2, rng
r2)])
            ]
      )
    ]

fixSide :: PairSide -> PairSpec era a b -> PairSpec era a b
fixSide :: forall era a b. PairSide -> PairSpec era a b -> PairSpec era a b
fixSide PairSide
_ (PairNever [String]
xs) = forall era a b. [String] -> PairSpec era a b
PairNever [String]
xs
fixSide PairSide
_ PairSpec era a b
PairAny = forall era a b. PairSpec era a b
PairAny
fixSide PairSide
side (PairSpec Rep era a
d Rep era b
r PairSide
_ Map a b
m) = forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era a
d Rep era b
r PairSide
side Map a b
m

genConsistentPairSpec ::
  (Ord dom, Eq rng) =>
  Rep era dom ->
  Rep era rng ->
  PairSpec era dom rng ->
  Gen (PairSpec era dom rng)
genConsistentPairSpec :: forall dom rng era.
(Ord dom, Eq rng) =>
Rep era dom
-> Rep era rng
-> PairSpec era dom rng
-> Gen (PairSpec era dom rng)
genConsistentPairSpec Rep era dom
_domr Rep era rng
_rngr (PairNever [String]
xs) = forall a. HasCallStack => String -> [String] -> a
errorMess String
"PairNever in genConsistentPairSpec" [String]
xs
genConsistentPairSpec Rep era dom
domr Rep era rng
rngr PairSpec era dom rng
PairAny = forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec Rep era dom
domr Rep era rng
rngr
genConsistentPairSpec Rep era dom
domr Rep era rng
rngr (PairSpec Rep era dom
_d Rep era rng
_r PairSide
VarOnRight Map dom rng
m) | forall k a. Map k a -> Bool
Map.null Map dom rng
m = forall era a b. PairSide -> PairSpec era a b -> PairSpec era a b
fixSide PairSide
VarOnRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec Rep era dom
domr Rep era rng
rngr
genConsistentPairSpec Rep era dom
domr Rep era rng
rngr (PairSpec Rep era dom
_d Rep era rng
_r PairSide
VarOnLeft Map dom rng
m) | forall k a. Map k a -> Bool
Map.null Map dom rng
m = forall era a b. PairSide -> PairSpec era a b -> PairSpec era a b
fixSide PairSide
VarOnLeft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec Rep era dom
domr Rep era rng
rngr
genConsistentPairSpec Rep era dom
_ Rep era rng
_ (PairSpec Rep era dom
d Rep era rng
r PairSide
VarOnRight Map dom rng
m) =
  forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
    [ (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era a b. PairSpec era a b
PairAny)
    , (Int
1, do Int
n <- forall a. Random a => (a, a) -> Gen a
choose (Int
0, forall k a. Map k a -> Int
Map.size Map dom rng
m forall a. Num a => a -> a -> a
- Int
1); forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
d Rep era rng
r PairSide
VarOnRight (forall k a. Int -> Map k a -> Map k a
Map.deleteAt Int
n Map dom rng
m)))
    ,
      ( Int
1
      , do
          dom
d1 <- forall a. [String] -> Gen a -> (a -> Bool) -> Gen a
suchThatErr [String
"genConsistentPairSpec"] (forall era b. Rep era b -> Gen b
genRep Rep era dom
d) (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map dom rng
m))
          rng
r1 <- forall era b. Rep era b -> Gen b
genRep Rep era rng
r
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
d Rep era rng
r PairSide
VarOnRight (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert dom
d1 rng
r1 Map dom rng
m))
      )
    ]
genConsistentPairSpec Rep era dom
_ Rep era rng
_ (PairSpec Rep era dom
d Rep era rng
r PairSide
VarOnLeft Map dom rng
m) =
  forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
    [ (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era a b. PairSpec era a b
PairAny)
    , (Int
1, do Int
n <- forall a. Random a => (a, a) -> Gen a
choose (Int
0, forall k a. Map k a -> Int
Map.size Map dom rng
m forall a. Num a => a -> a -> a
- Int
1); forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
d Rep era rng
r PairSide
VarOnLeft (forall k a. Int -> Map k a -> Map k a
Map.deleteAt Int
n Map dom rng
m)))
    ,
      ( Int
1
      , do
          dom
d1 <- forall a. [String] -> Gen a -> (a -> Bool) -> Gen a
suchThatErr [String
"genConsistentPairSpec"] (forall era b. Rep era b -> Gen b
genRep Rep era dom
d) (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map dom rng
m))
          rng
r1 <- forall era b. Rep era b -> Gen b
genRep Rep era rng
r
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b era.
(Ord a, Eq b) =>
Rep era a -> Rep era b -> PairSide -> Map a b -> PairSpec era a b
PairSpec Rep era dom
d Rep era rng
r PairSide
VarOnLeft (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert dom
d1 rng
r1 Map dom rng
m))
      )
    ]

genFromPairSpec ::
  forall era dom rng. Ord dom => [String] -> PairSpec era dom rng -> Gen (Map dom rng)
genFromPairSpec :: forall era dom rng.
Ord dom =>
[String] -> PairSpec era dom rng -> Gen (Map dom rng)
genFromPairSpec [String]
msgs (PairNever [String]
xs) = forall a. HasCallStack => String -> [String] -> a
errorMess String
"genFromPairSpec failed due to PairNever" ([String]
msgs forall a. [a] -> [a] -> [a]
++ [String]
xs)
genFromPairSpec [String]
_msgs PairSpec era dom rng
PairAny = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Map k a
Map.empty
genFromPairSpec [String]
msgs p :: PairSpec era dom rng
p@(PairSpec Rep era dom
domr Rep era rng
rngr PairSide
VarOnRight Map dom rng
mp) = do
  Int
n <- (forall a. Num a => a -> a -> a
+ (forall k a. Map k a -> Int
Map.size Map dom rng
mp)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
10)
  forall a b.
Ord a =>
[String] -> Map a b -> Int -> Gen a -> Gen b -> Gen (Map a b)
mapFromSubset ([String]
msgs forall a. [a] -> [a] -> [a]
++ [String
"genFromPairSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era dom rng
p]) Map dom rng
mp Int
n (forall era b. Rep era b -> Gen b
genRep Rep era dom
domr) (forall era b. Rep era b -> Gen b
genRep Rep era rng
rngr)
genFromPairSpec [String]
msgs (PairSpec Rep era dom
_domr Rep era rng
_rngr PairSide
VarOnLeft Map dom rng
mp) = do
  Set dom
domset <- forall a. Ord a => [String] -> Set a -> Gen (Set a)
subsetFromSet ([String]
msgs forall a. [a] -> [a] -> [a]
++ [String
"from genFromPairSpec VarOnLeft"]) (forall k a. Map k a -> Set k
Map.keysSet Map dom rng
mp)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map dom rng
mp Set dom
domset)

-- ============================================
-- tests for Pair Spec

testConsistentPair :: Gen Property
testConsistentPair :: Gen Property
testConsistentPair = do
  PairSpec TT Int Int
s1 <- forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec @TT forall era. Rep era Int
IntR forall era. Rep era Int
IntR
  PairSpec TT Int Int
s2 <- forall dom rng era.
(Ord dom, Eq rng) =>
Rep era dom
-> Rep era rng
-> PairSpec era dom rng
-> Gen (PairSpec era dom rng)
genConsistentPairSpec forall era. Rep era Int
IntR forall era. Rep era Int
IntR PairSpec TT Int Int
s1
  case PairSpec TT Int Int
s1 forall a. Semigroup a => a -> a -> a
<> PairSpec TT Int Int
s2 of
    PairNever [String]
ms ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines ([String
"genConsistentPair fails", forall a. Show a => a -> String
show PairSpec TT Int Int
s1, forall a. Show a => a -> String
show PairSpec TT Int Int
s2] forall a. [a] -> [a] -> [a]
++ [String]
ms)) Bool
False
    PairSpec TT Int Int
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => prop -> Property
property Bool
True

testSoundPairSpec :: Gen Property
testSoundPairSpec :: Gen Property
testSoundPairSpec = do
  PairSpec TT Int Word64
s1 <- forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec forall era. Rep era Int
IntR forall era. Rep era Word64
Word64R
  Map Int Word64
ans <- forall era dom rng.
Ord dom =>
[String] -> PairSpec era dom rng -> Gen (Map dom rng)
genFromPairSpec @TT [String
"testSoundPairSpec"] PairSpec TT Int Word64
s1
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample (String
"spec=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec TT Int Word64
s1 forall a. [a] -> [a] -> [a]
++ String
"\nans=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Map Int Word64
ans) (forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map Int Word64
ans PairSpec TT Int Word64
s1)

testMergePairSpec :: Gen Property
testMergePairSpec :: Gen Property
testMergePairSpec = do
  -- let msg = ["testMergePairSpec"]
  PairSpec TT Word64 Int
s1 <- forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec forall era. Rep era Word64
Word64R forall era. Rep era Int
IntR
  PairSpec TT Word64 Int
s2 <- forall dom rng era.
(Ord dom, Eq rng) =>
Rep era dom
-> Rep era rng
-> PairSpec era dom rng
-> Gen (PairSpec era dom rng)
genConsistentPairSpec forall era. Rep era Word64
Word64R forall era. Rep era Int
IntR PairSpec TT Word64 Int
s1
  case PairSpec TT Word64 Int
s1 forall a. Semigroup a => a -> a -> a
<> PairSpec TT Word64 Int
s2 of
    PairNever [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) => ...)
    PairSpec TT Word64 Int
s4 -> do
      Map Word64 Int
ans <- forall era dom rng.
Ord dom =>
[String] -> PairSpec era dom rng -> Gen (Map dom rng)
genFromPairSpec @TT [String
"testMergePairSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec TT Word64 Int
s1 forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec TT Word64 Int
s2] PairSpec TT Word64 Int
s4
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        forall prop. Testable prop => String -> prop -> Property
counterexample
          ( String
"s1="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec TT Word64 Int
s1
              forall a. [a] -> [a] -> [a]
++ String
"\ns2="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec TT Word64 Int
s2
              forall a. [a] -> [a] -> [a]
++ String
"\ns1<>s2="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec TT Word64 Int
s4
              forall a. [a] -> [a] -> [a]
++ String
"\nans="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Map Word64 Int
ans
              forall a. [a] -> [a] -> [a]
++ String
"\nrun s1="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map Word64 Int
ans PairSpec TT Word64 Int
s1)
              forall a. [a] -> [a] -> [a]
++ String
"\nrun s2="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map Word64 Int
ans PairSpec TT Word64 Int
s2)
              forall a. [a] -> [a] -> [a]
++ String
"\nrun s4="
              forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map Word64 Int
ans PairSpec TT Word64 Int
s4)
          )
          (forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map Word64 Int
ans PairSpec TT Word64 Int
s4 Bool -> Bool -> Bool
&& forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map Word64 Int
ans PairSpec TT Word64 Int
s2 Bool -> Bool -> Bool
&& forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map Word64 Int
ans PairSpec TT Word64 Int
s1)

manyMergePairSpec :: Gen (Int, [String])
manyMergePairSpec :: Gen (Int, [String])
manyMergePairSpec = do
  [PairSpec TT Word64 Int]
xs <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
60 (forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec forall era. Rep era Word64
Word64R forall era. Rep era Int
IntR)
  [PairSpec TT Word64 Int]
ys <- forall a. Int -> Gen a -> Gen [a]
vectorOf Int
60 (forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec forall era. Rep era Word64
Word64R forall era. Rep era Int
IntR)
  let ok :: PairSpec era a b -> Bool
ok PairSpec era a b
PairAny = Bool
False
      ok PairSpec era a b
_ = Bool
True
      check :: (PairSpec era dom rng, PairSpec era dom rng, PairSpec TT dom rng)
-> Gen
     (PairSpec era dom rng, Bool, PairSpec era dom rng, Bool,
      Map dom rng, Bool, PairSpec TT dom rng)
check (PairSpec era dom rng
x, PairSpec era dom rng
y, PairSpec TT dom rng
m) = do
        let size :: Size
size = forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec TT dom rng
m
        Int
i <- Size -> Gen Int
genFromSize Size
size
        let wordsX :: [String]
wordsX =
              [ String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec TT dom rng
m)
              , String
"s1<>s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec TT dom rng
m
              , String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec era dom rng
x)
              , String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era dom rng
x
              , String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec era dom rng
y)
              , String
"s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era dom rng
y
              , String
"GenFromPairSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
              ]
        Map dom rng
z <- forall era dom rng.
Ord dom =>
[String] -> PairSpec era dom rng -> Gen (Map dom rng)
genFromPairSpec @TT [String]
wordsX PairSpec TT dom rng
m
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (PairSpec era dom rng
x, forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map dom rng
z PairSpec era dom rng
x, PairSpec era dom rng
y, forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map dom rng
z PairSpec era dom rng
y, Map dom rng
z, forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec Map dom rng
z PairSpec TT dom rng
m, PairSpec TT dom rng
m)
      showAns :: (PairSpec era dom rng, a, PairSpec era dom rng, a, a, a,
 PairSpec era dom rng)
-> String
showAns (PairSpec era dom rng
s1, a
run1, PairSpec era dom rng
s2, a
run2, a
v, a
run3, PairSpec era dom rng
s3) =
        [String] -> String
unlines
          [ String
"\ns1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era dom rng
s1
          , String
"s1 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec era dom rng
s1)
          , String
"s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era dom rng
s2
          , String
"s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec era dom rng
s2)
          , String
"s1 <> s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PairSpec era dom rng
s3
          , String
"s1<>s2 Size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec PairSpec era dom rng
s3)
          , String
"v = genFromPairSpec (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
v
          , String
"runPairSpec v s1 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run1
          , String
"runPairSpec v s2 = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run2
          , String
"runPairSpec v (s1 <> s2) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
run3
          ]
      pr :: (PairSpec era dom rng, Bool, PairSpec era dom rng, Bool, a, Bool,
 PairSpec era dom rng)
-> Maybe String
pr x :: (PairSpec era dom rng, Bool, PairSpec era dom rng, Bool, a, Bool,
 PairSpec era dom rng)
x@(PairSpec era dom rng
_, Bool
a, PairSpec era dom rng
_, Bool
b, a
_, Bool
c, PairSpec era dom rng
_) = if Bool -> Bool
not (Bool
a Bool -> Bool -> Bool
&& Bool
b Bool -> Bool -> Bool
&& Bool
c) then forall a. a -> Maybe a
Just (forall {a} {a} {a} {a} {era} {dom} {rng} {era} {dom} {rng} {era}
       {dom} {rng}.
(Show a, Show a, Show a, Show a) =>
(PairSpec era dom rng, a, PairSpec era dom rng, a, a, a,
 PairSpec era dom rng)
-> String
showAns (PairSpec era dom rng, Bool, PairSpec era dom rng, Bool, a, Bool,
 PairSpec era dom rng)
x) else forall a. Maybe a
Nothing
  let trips :: [(PairSpec TT Word64 Int, PairSpec TT Word64 Int,
  PairSpec TT Word64 Int)]
trips = [(PairSpec TT Word64 Int
x, PairSpec TT Word64 Int
y, PairSpec TT Word64 Int
m) | PairSpec TT Word64 Int
x <- [PairSpec TT Word64 Int]
xs, PairSpec TT Word64 Int
y <- [PairSpec TT Word64 Int]
ys, forall era d r. PairSpec era d r -> Bool
ok PairSpec TT Word64 Int
x Bool -> Bool -> Bool
&& forall era d r. PairSpec era d r -> Bool
ok PairSpec TT Word64 Int
y, Just PairSpec TT Word64 Int
m <- [forall a. (LiftT a, Semigroup a) => a -> a -> Maybe a
consistent PairSpec TT Word64 Int
x PairSpec TT Word64 Int
y]]
  [(PairSpec TT Word64 Int, Bool, PairSpec TT Word64 Int, Bool,
  Map Word64 Int, Bool, PairSpec TT Word64 Int)]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {dom} {rng} {era} {era}.
(Ord dom, Eq rng) =>
(PairSpec era dom rng, PairSpec era dom rng, PairSpec TT dom rng)
-> Gen
     (PairSpec era dom rng, Bool, PairSpec era dom rng, Bool,
      Map dom rng, Bool, PairSpec TT dom rng)
check [(PairSpec TT Word64 Int, PairSpec TT Word64 Int,
  PairSpec TT Word64 Int)]
trips
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(PairSpec TT Word64 Int, PairSpec TT Word64 Int,
  PairSpec TT Word64 Int)]
trips, forall a b. (a -> Maybe b) -> [a] -> [b]
Maybe.mapMaybe forall {a} {era} {dom} {rng} {era} {dom} {rng} {era} {dom} {rng}.
Show a =>
(PairSpec era dom rng, Bool, PairSpec era dom rng, Bool, a, Bool,
 PairSpec era dom rng)
-> Maybe String
pr [(PairSpec TT Word64 Int, Bool, PairSpec TT Word64 Int, Bool,
  Map Word64 Int, Bool, PairSpec TT Word64 Int)]
ts)

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