{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
-- Orphan Arbitrary instance for OrderInfo
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Constrained.Tests where

import Control.Arrow (first)
import Control.Monad
import Data.Foldable (fold)
import Data.Group
import Data.List (intercalate, isPrefixOf)
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Prelude hiding (subtract)

import Test.Cardano.Ledger.Constrained.Ast

import Cardano.Ledger.Coin
import Cardano.Ledger.Core (Era)
import Cardano.Ledger.Shelley
import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import Test.Cardano.Ledger.Constrained.Classes
import Test.Cardano.Ledger.Constrained.Combinators
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Monad
import Test.Cardano.Ledger.Constrained.Rewrite
import Test.Cardano.Ledger.Constrained.Shrink
import Test.Cardano.Ledger.Constrained.Size (Size (SzRng))
import Test.Cardano.Ledger.Constrained.Solver
import Test.Cardano.Ledger.Constrained.TypeRep
import Test.QuickCheck hiding (getSize, total)

{-

One property that we'd like to test is the soundness property for the constraint solver: if it
successfully generates a solution to a set of constraints, this solution *actually* satisfies the
constraints.

In order to test this we need to generate random satisfiable constraints. The approach we take is to
generate constraints in a given fixed environment, and take care to only generate ones that hold in
this particular environment.

To ensure we generate constraints that have a linear dependency graph we keep track of which
variables in the environment are solved by an already generated constraint and the "depth" at which
it was solved. When generating constraints between solved variables we require the depth to respect
the dependency order. For instance, a constraints S ⊆ T (assuming we solve supersets before subsets)
must have `depthOf T < depthOf S`.

This doesn't always work, because the solver substitutes equalities in a way that does not respect
our dependencies (`Rewrite.removeEqual`)

The soundness property discards cases where we fail to find a solution to the constraints, but it's
still interesting to know when this happens, since we try our best to generate solvable constraints.
There is a strict version of the property (`prop_soundness' True`) that fails instead. Currently it
fails in these cases:
  - When the existence of a solution to a later variable depends on the value picked for an earlier
    variable. For instance, [Sized 3 A, B ⊆ A, C ⊆ B, Sized 1 C]. Here B needs to be solved with a
    non-empty set for C to have a solution.

Current limitations of the tests
  - Only CoinR and SetR CoinR types (and Word64R for size constraints)
  - Only generates Sized, Subset, Disjoint, and SumsTo(SumSet) constraints

Known limitations of the code that the tests avoid
  - Can't solve `Sized n (Rng X)` (see TODO/sizedRng)
  - Random X, N < Σ sum X can pick X = {} (N :: Coin) and then crash on the sum constraint
    (TODO/negativeCoin)

-}

-- Generators ---

data GenEnv era = GenEnv
  { forall era. GenEnv era -> OrderInfo
gOrder :: OrderInfo
  , forall era. GenEnv era -> Env era
gEnv :: Env era
  , forall era. GenEnv era -> Map (Name era) Depth
gSolved :: Map (Name era) Depth
  -- ^ Which variables in the environment have we "solved", i.e. generated
  --   a constraint that allows solving them. Also track the "depth" of
  --   the variable in the dependency order (depth = 1 + depth of
  --   dependencies).
  }
  deriving (Depth -> GenEnv era -> ShowS
forall era. Depth -> GenEnv era -> ShowS
forall era. [GenEnv era] -> ShowS
forall era. GenEnv era -> String
forall a.
(Depth -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GenEnv era] -> ShowS
$cshowList :: forall era. [GenEnv era] -> ShowS
show :: GenEnv era -> String
$cshow :: forall era. GenEnv era -> String
showsPrec :: Depth -> GenEnv era -> ShowS
$cshowsPrec :: forall era. Depth -> GenEnv era -> ShowS
Show)

type Depth = Int

instance Arbitrary OrderInfo where
  arbitrary :: Gen OrderInfo
arbitrary = Bool -> Bool -> Bool -> OrderInfo
OrderInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary
  shrink :: OrderInfo -> [OrderInfo]
shrink OrderInfo
info = [OrderInfo
standardOrderInfo | OrderInfo
info forall a. Eq a => a -> a -> Bool
/= OrderInfo
standardOrderInfo]

addVar :: V era t -> t -> GenEnv era -> GenEnv era
addVar :: forall era t. V era t -> t -> GenEnv era -> GenEnv era
addVar V era t
vvar t
val GenEnv era
env = GenEnv era
env {gEnv :: Env era
gEnv = forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
vvar t
val forall a b. (a -> b) -> a -> b
$ forall era. GenEnv era -> Env era
gEnv GenEnv era
env}

markSolved :: HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved :: forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved HashSet (Name era)
solved Depth
d GenEnv era
env = GenEnv era
env {gSolved :: Map (Name era) Depth
gSolved = forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Ord a => a -> a -> a
max Map (Name era) Depth
new (forall era. GenEnv era -> Map (Name era) Depth
gSolved GenEnv era
env)}
  where
    new :: Map (Name era) Depth
new = forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (forall a b. a -> b -> a
const Depth
d) (forall a. Ord a => HashSet a -> Set a
hashSetToSet HashSet (Name era)
solved)

addSolvedVar :: V era t -> t -> Depth -> GenEnv era -> GenEnv era
addSolvedVar :: forall era t. V era t -> t -> Depth -> GenEnv era -> GenEnv era
addSolvedVar vvar :: V era t
vvar@(V String
_ Rep era t
_ Access era s t
_) t
val Depth
d = forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved (forall a. Hashable a => a -> HashSet a
HashSet.singleton forall a b. (a -> b) -> a -> b
$ forall era t. V era t -> Name era
Name V era t
vvar) Depth
d forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era t. V era t -> t -> GenEnv era -> GenEnv era
addVar V era t
vvar t
val

depthOfName :: GenEnv era -> Name era -> Depth
depthOfName :: forall era. GenEnv era -> Name era -> Depth
depthOfName GenEnv era
env Name era
x = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Depth
0 Name era
x (forall era. GenEnv era -> Map (Name era) Depth
gSolved GenEnv era
env)

depthOf :: GenEnv era -> Term era t -> Depth
depthOf :: forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env Term era t
t = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall a b. (a -> b) -> a -> b
$ Depth
0 forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall era. GenEnv era -> Name era -> Depth
depthOfName GenEnv era
env) (forall a. HashSet a -> [a]
HashSet.toList forall a b. (a -> b) -> a -> b
$ forall era t. Term era t -> HashSet (Name era)
vars Term era t
t)

depthOfSum :: GenEnv era -> Sum era c -> Depth
depthOfSum :: forall era c. GenEnv era -> Sum era c -> Depth
depthOfSum GenEnv era
env = \case
  SumMap Term era (Map a c)
t -> forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env Term era (Map a c)
t
  SumList Term era [c]
t -> forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env Term era [c]
t
  One Term era c
t -> forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env Term era c
t
  ProjOne Lens' x c
_ Rep era c
_ Term era x
t -> forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env Term era x
t
  ProjMap Rep era c
_ Lens' x c
_ Term era (Map a x)
t -> forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env Term era (Map a x)
t

genLiteral :: forall era t. Era era => GenEnv era -> Rep era t -> Gen t
genLiteral :: forall era t. Era era => GenEnv era -> Rep era t -> Gen t
genLiteral GenEnv era
env Rep era t
rep =
  case Rep era t
rep of
    SetR Rep era a
erep -> forall a. Ord a => Rep era a -> Gen (Set a)
setLiteral Rep era a
erep
    MapR Rep era a
_ Rep era b
_ -> forall a. Rep era a -> Gen a
unconstrained Rep era t
rep -- TODO: more clever generation for maps
    Rep era t
_ -> forall a. Rep era a -> Gen a
unconstrained Rep era t
rep
  where
    unconstrained :: forall a. Rep era a -> Gen a
    unconstrained :: forall a. Rep era a -> Gen a
unconstrained Rep era a
r = forall era b. Rep era b -> Gen b
genRep Rep era a
r

    setLiteral :: forall a. Ord a => Rep era a -> Gen (Set a)
    setLiteral :: forall a. Ord a => Rep era a -> Gen (Set a)
setLiteral Rep era a
erep = do
      let knownSets :: [Set a]
knownSets = [Set a
val | (V era (Set a)
_, Set a
val) <- forall era t. Era era => Env era -> Rep era t -> [(V era t, t)]
envVarsOfType (forall era. GenEnv era -> Env era
gEnv GenEnv era
env) (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era a
erep)]
          gen :: Gen (Set a)
gen = forall a. HasCallStack => [Gen a] -> Gen a
oneof forall a b. (a -> b) -> a -> b
$ forall era b. Rep era b -> Gen b
genRep (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era a
erep) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall (f :: * -> *) a. Applicative f => a -> f a
pure [Set a]
knownSets
      Set a
set1 <- Gen (Set a)
gen
      Set a
set2 <- Gen (Set a)
gen
      Set a -> Set a -> Set a
op <- forall a. HasCallStack => [a] -> Gen a
elements [forall a b. a -> b -> a
const, forall a b. a -> b -> a
const forall a. a -> a
id, forall a. Ord a => Set a -> Set a -> Set a
Set.union, forall a. Ord a => Set a -> Set a -> Set a
Set.intersection, forall a. Ord a => Set a -> Set a -> Set a
Set.difference, forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Ord a => Set a -> Set a -> Set a
Set.difference]
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Set a -> Set a -> Set a
op Set a
set1 Set a
set2

genFreshVarName :: GenEnv era -> Gen String
genFreshVarName :: forall era. GenEnv era -> Gen String
genFreshVarName = forall a. HasCallStack => [a] -> Gen a
elements forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {era}. GenEnv era -> [String]
varNames
  where
    allTheNames :: [String]
allTheNames = [String
s forall a. [a] -> [a] -> [a]
++ [Char
c] | String
s <- String
"" forall a. a -> [a] -> [a]
: [String]
allTheNames, Char
c <- [Char
'A' .. Char
'Z']]
    varNames :: GenEnv era -> [String]
varNames GenEnv era
env = forall a. Depth -> [a] -> [a]
take Depth
10 forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` Map String (Payload era)
vmap) [String]
allTheNames
      where
        Env Map String (Payload era)
vmap = forall era. GenEnv era -> Env era
gEnv GenEnv era
env

envVarsOfType :: Era era => Env era -> Rep era t -> [(V era t, t)]
envVarsOfType :: forall era t. Era era => Env era -> Rep era t -> [(V era t, t)]
envVarsOfType (Env Map String (Payload era)
env) Rep era t
rep = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, Payload era) -> [(V era t, t)]
wellTyped forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList Map String (Payload era)
env
  where
    wellTyped :: (String, Payload era) -> [(V era t, t)]
wellTyped (String
name, Payload Rep era t
rep' t
val Access era s t
access) =
      case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql Rep era t
rep Rep era t
rep' of
        Just t :~: t
Refl -> [(forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
name Rep era t
rep Access era s t
access, t
val)]
        Maybe (t :~: t)
Nothing -> []

data VarSpec
  = -- | Must contain a variable (either unsolved, or solved at least the given depth).
    --   Requiring a minimum depth let's us avoid introducing cycles in
    --   already solved variables.
    VarTerm Depth
  | -- | Can only use solved variables
    KnownTerm
  deriving (VarSpec -> VarSpec -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VarSpec -> VarSpec -> Bool
$c/= :: VarSpec -> VarSpec -> Bool
== :: VarSpec -> VarSpec -> Bool
$c== :: VarSpec -> VarSpec -> Bool
Eq, Depth -> VarSpec -> ShowS
[VarSpec] -> ShowS
VarSpec -> String
forall a.
(Depth -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VarSpec] -> ShowS
$cshowList :: [VarSpec] -> ShowS
show :: VarSpec -> String
$cshow :: VarSpec -> String
showsPrec :: Depth -> VarSpec -> ShowS
$cshowsPrec :: Depth -> VarSpec -> ShowS
Show)

genTerm :: Era era => GenEnv era -> Rep era t -> VarSpec -> Gen (Term era t, GenEnv era)
genTerm :: forall era t.
Era era =>
GenEnv era -> Rep era t -> VarSpec -> Gen (Term era t, GenEnv era)
genTerm GenEnv era
env Rep era t
rep VarSpec
vspec = forall era t.
Era era =>
GenEnv era
-> Rep era t
-> (t -> Bool)
-> Gen t
-> VarSpec
-> Gen (Term era t, GenEnv era)
genTerm' GenEnv era
env Rep era t
rep (forall a b. a -> b -> a
const Bool
True) (forall era t. Era era => GenEnv era -> Rep era t -> Gen t
genLiteral GenEnv era
env Rep era t
rep) VarSpec
vspec

genTerm' ::
  forall era t.
  Era era =>
  GenEnv era ->
  Rep era t ->
  (t -> Bool) ->
  Gen t ->
  VarSpec ->
  Gen (Term era t, GenEnv era)
genTerm' :: forall era t.
Era era =>
GenEnv era
-> Rep era t
-> (t -> Bool)
-> Gen t
-> VarSpec
-> Gen (Term era t, GenEnv era)
genTerm' GenEnv era
env Rep era t
rep t -> Bool
valid Gen t
genLit VarSpec
vspec =
  forall a. HasCallStack => [(Depth, Gen a)] -> Gen a
frequency forall a b. (a -> b) -> a -> b
$
    [(Depth
5, Gen (Term era t, GenEnv era)
genFixed) | VarSpec
vspec forall a. Eq a => a -> a -> Bool
== VarSpec
KnownTerm]
      forall a. [a] -> [a] -> [a]
++ [(Depth
5, Gen (Term era t, GenEnv era)
genExistingVar) | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [V era t]
allowedVars]
      forall a. [a] -> [a] -> [a]
++ [(Depth
1, Gen (Term era t, GenEnv era)
genFreshVar) | VarTerm {} <- [VarSpec
vspec]]
      forall a. [a] -> [a] -> [a]
++ [(Depth
2, forall k.
(t ~ Set k, Ord k) =>
Rep era k -> Gen (Term era (Set k), GenEnv era)
genDom Rep era a
krep) | SetR Rep era a
krep <- [Rep era t
rep]]
      forall a. [a] -> [a] -> [a]
++ [(Depth
2, forall k.
(t ~ Set k, Ord k) =>
Rep era k -> Gen (Term era (Set k), GenEnv era)
genRng Rep era a
vrep) | SetR Rep era a
vrep <- [Rep era t
rep]]
  where
    isValid :: (V era t, t) -> Bool
isValid (V era t
_, t
val) = t -> Bool
valid t
val
    existingVars :: [V era t]
existingVars = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (V era t, t) -> Bool
isValid forall a b. (a -> b) -> a -> b
$ forall era t. Era era => Env era -> Rep era t -> [(V era t, t)]
envVarsOfType (forall era. GenEnv era -> Env era
gEnv GenEnv era
env) Rep era t
rep
    allowedVars :: [V era t]
allowedVars = case VarSpec
vspec of
      VarTerm Depth
d -> forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> a -> Bool
>= Depth
d) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. GenEnv era -> Name era -> Depth
depthOfName GenEnv era
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era t. V era t -> Name era
Name) [V era t]
existingVars
      VarSpec
KnownTerm -> forall a. (a -> Bool) -> [a] -> [a]
filter ((forall k a. Ord k => k -> Map k a -> Bool
`Map.member` forall era. GenEnv era -> Map (Name era) Depth
gSolved GenEnv era
env) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era t. V era t -> Name era
Name) [V era t]
existingVars

    genFixed :: Gen (Term era t, GenEnv era)
genFixed = (,GenEnv era
env) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era t. Rep era t -> t -> Term era t
Lit Rep era t
rep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen t
genLit
    genExistingVar :: Gen (Term era t, GenEnv era)
genExistingVar = (,GenEnv era
env) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era t. V era t -> Term era t
Var forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. HasCallStack => [a] -> Gen a
elements [V era t]
allowedVars

    genFreshVar :: Gen (Term era t, GenEnv era)
genFreshVar = do
      String
name <- forall era. GenEnv era -> Gen String
genFreshVarName GenEnv era
env
      t
val <- Gen t
genLit
      let vvar :: V era t
vvar = forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
name Rep era t
rep forall era s t. Access era s t
No
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era t. V era t -> Term era t
Var V era t
vvar, forall era t. V era t -> t -> GenEnv era -> GenEnv era
addVar V era t
vvar t
val GenEnv era
env)

    genDom :: forall k. (t ~ Set k, Ord k) => Rep era k -> Gen (Term era (Set k), GenEnv era)
    genDom :: forall k.
(t ~ Set k, Ord k) =>
Rep era k -> Gen (Term era (Set k), GenEnv era)
genDom Rep era k
krep = do
      TypeInEra Rep era t
vrep <- forall era. Gen (TypeInEra era)
genValType
      (Term era (Map k t)
m, GenEnv era
env') <-
        forall era t.
Era era =>
GenEnv era
-> Rep era t
-> (t -> Bool)
-> Gen t
-> VarSpec
-> Gen (Term era t, GenEnv era)
genTerm'
          GenEnv era
env
          (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era k
krep Rep era t
vrep)
          (t -> Bool
valid forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> Set k
Map.keysSet)
          (Gen t
genLit forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era v k.
Era era =>
GenEnv era -> Rep era v -> Set k -> Gen (Map k v)
genMapLiteralWithDom GenEnv era
env Rep era t
vrep)
          VarSpec
vspec
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map k t)
m, GenEnv era
env')

    genRng :: forall v. (t ~ Set v, Ord v) => Rep era v -> Gen (Term era (Set v), GenEnv era)
    genRng :: forall k.
(t ~ Set k, Ord k) =>
Rep era k -> Gen (Term era (Set k), GenEnv era)
genRng Rep era v
vrep = do
      TypeInEra Rep era t
krep <- forall era. Gen (TypeInEra era)
genKeyType
      (Term era (Map t v)
m, GenEnv era
env') <-
        forall era t.
Era era =>
GenEnv era
-> Rep era t
-> (t -> Bool)
-> Gen t
-> VarSpec
-> Gen (Term era t, GenEnv era)
genTerm'
          GenEnv era
env
          (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era t
krep Rep era v
vrep)
          (t -> Bool
valid forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
Map.elems)
          (Gen t
genLit forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era k v.
(Era era, Ord k) =>
GenEnv era -> Rep era k -> Set v -> Gen (Map k v)
genMapLiteralWithRng GenEnv era
env Rep era t
krep)
          VarSpec
vspec
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map t v)
m, GenEnv era
env')

genMapLiteralWithDom :: Era era => GenEnv era -> Rep era v -> Set k -> Gen (Map k v)
genMapLiteralWithDom :: forall era v k.
Era era =>
GenEnv era -> Rep era v -> Set k -> Gen (Map k v)
genMapLiteralWithDom GenEnv era
env Rep era v
vrep Set k
keys = do
  let genVal :: Gen v
genVal = forall era t. Era era => GenEnv era -> Rep era t -> Gen t
genLiteral GenEnv era
env Rep era v
vrep
  forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\()
_ -> Gen v
genVal) (forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (forall a b. a -> b -> a
const ()) Set k
keys)

genMapLiteralWithRng :: (Era era, Ord k) => GenEnv era -> Rep era k -> Set v -> Gen (Map k v)
genMapLiteralWithRng :: forall era k v.
(Era era, Ord k) =>
GenEnv era -> Rep era k -> Set v -> Gen (Map k v)
genMapLiteralWithRng GenEnv era
env Rep era k
krep Set v
vals = do
  Set k
keys <- forall a. Ord a => [String] -> Depth -> Gen a -> Gen (Set a)
setSized [] (forall a. Set a -> Depth
Set.size Set v
vals) (forall era t. Era era => GenEnv era -> Rep era t -> Gen t
genLiteral GenEnv era
env Rep era k
krep)
  [v]
valsList <- forall a. [a] -> Gen [a]
shuffle forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set v
vals
  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
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Set a -> [a]
Set.toList Set k
keys) [v]
valsList

data TypeInEra era where
  TypeInEra :: (Show t, Ord t) => Rep era t -> TypeInEra era

genKeyType :: Gen (TypeInEra era)
genKeyType :: forall era. Gen (TypeInEra era)
genKeyType = forall a. HasCallStack => [a] -> Gen a
elements [forall t era. (Show t, Ord t) => Rep era t -> TypeInEra era
TypeInEra forall era. Rep era Depth
IntR]

genValType :: Gen (TypeInEra era)
genValType :: forall era. Gen (TypeInEra era)
genValType = forall a. HasCallStack => [a] -> Gen a
elements [forall t era. (Show t, Ord t) => Rep era t -> TypeInEra era
TypeInEra forall era. Rep era Coin
CoinR, forall t era. (Show t, Ord t) => Rep era t -> TypeInEra era
TypeInEra forall era. Rep era DeltaCoin
DeltaCoinR] -- Possible future use , TypeInEra (PairR CoinR CoinR)]

genBaseType :: Gen (TypeInEra era)
genBaseType :: forall era. Gen (TypeInEra era)
genBaseType = forall a. HasCallStack => [Gen a] -> Gen a
oneof [forall era. Gen (TypeInEra era)
genKeyType, forall era. Gen (TypeInEra era)
genValType]

genType :: Gen (TypeInEra era)
genType :: forall era. Gen (TypeInEra era)
genType =
  forall a. HasCallStack => [Gen a] -> Gen a
oneof
    [ forall era. Gen (TypeInEra era)
genBaseType
    , forall {era}. TypeInEra era -> TypeInEra era
setR forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era. Gen (TypeInEra era)
genValType
    , forall {era}. TypeInEra era -> TypeInEra era
listR forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era. Gen (TypeInEra era)
genValType
    , forall {era}. TypeInEra era -> TypeInEra era -> TypeInEra era
mapR forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era. Gen (TypeInEra era)
genKeyType forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall era. Gen (TypeInEra era)
genValType
    ]
  where
    setR :: TypeInEra era -> TypeInEra era
setR (TypeInEra Rep era t
t) = forall t era. (Show t, Ord t) => Rep era t -> TypeInEra era
TypeInEra (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
t)
    listR :: TypeInEra era -> TypeInEra era
listR (TypeInEra Rep era t
t) = forall t era. (Show t, Ord t) => Rep era t -> TypeInEra era
TypeInEra (forall era a. Rep era a -> Rep era [a]
ListR Rep era t
t)
    mapR :: TypeInEra era -> TypeInEra era -> TypeInEra era
mapR (TypeInEra Rep era t
s) (TypeInEra Rep era t
t) = forall t era. (Show t, Ord t) => Rep era t -> TypeInEra era
TypeInEra (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era t
s Rep era t
t)

-- | Unsatisfiable constraint returned if we fail during constraint generation.
errPred :: [String] -> Pred era
errPred :: forall era. [String] -> Pred era
errPred [String]
errs = forall era t. Rep era t -> t -> Term era t
Lit (forall era a. Rep era a -> Rep era [a]
ListR forall era. Rep era String
stringR) [String
"Errors:"] forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era t. Rep era t -> t -> Term era t
Lit (forall era a. Rep era a -> Rep era [a]
ListR forall era. Rep era String
stringR) [String]
errs

-- This is very ad hoc
setWithSum :: Int -> Gen (Set Int)
setWithSum :: Depth -> Gen (Set Depth)
setWithSum Depth
n = Set Depth -> Set Depth
fixUp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary
  where
    fixUp :: Set Depth -> Set Depth
fixUp Set Depth
s
      | Depth
missing forall a. Eq a => a -> a -> Bool
== Depth
0 = Set Depth
s
      | Bool
otherwise =
          if forall a. Ord a => a -> Set a -> Bool
Set.notMember Depth
missing Set Depth
s
            then forall a. Ord a => a -> Set a -> Set a
Set.insert Depth
missing Set Depth
s
            else forall a. a -> Set a
Set.singleton Depth
n
      where
        missing :: Depth
missing = Depth
n forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum Set Depth
s

listWithSum :: Coin -> Gen [Coin]
listWithSum :: Coin -> Gen [Coin]
listWithSum Coin
n = [Coin] -> [Coin]
fixUp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary
  where
    fixUp :: [Coin] -> [Coin]
fixUp [Coin]
s
      | Coin
missing forall a. Eq a => a -> a -> Bool
== Integer -> Coin
Coin Integer
0 = [Coin]
s
      | Bool
otherwise = Coin
missing forall a. a -> [a] -> [a]
: [Coin]
s
      where
        missing :: Coin
missing = Coin
n forall m. Group m => m -> m -> m
~~ forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold [Coin]
s

mapWithSum :: Coin -> Gen (Map Coin Coin)
mapWithSum :: Coin -> Gen (Map Coin Coin)
mapWithSum Coin
n = do
  [Coin]
rng <- Coin -> Gen [Coin]
listWithSum Coin
n
  [Coin]
dom <- forall a. Set a -> [a]
Set.toList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Ord a => [String] -> Depth -> Gen a -> Gen (Set a)
setSized [] (forall (t :: * -> *) a. Foldable t => t a -> Depth
length [Coin]
rng) forall a. Arbitrary a => Gen a
arbitrary
  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
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Coin]
dom [Coin]
rng

genFromOrdCond :: (Arbitrary c, Adds c) => OrdCond -> Bool -> c -> Gen c
genFromOrdCond :: forall c. (Arbitrary c, Adds c) => OrdCond -> Bool -> c -> Gen c
genFromOrdCond OrdCond
EQL Bool
_ c
n = forall (f :: * -> *) a. Applicative f => a -> f a
pure c
n
genFromOrdCond OrdCond
cond Bool
canBeNegative c
n =
  forall a. [String] -> Gen a -> (a -> Bool) -> Gen a
suchThatErr
    [String
"genFromOrdCond " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show OrdCond
cond forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show c
n]
    ( forall a. HasCallStack => [(Depth, Gen a)] -> Gen a
frequency forall a b. (a -> b) -> a -> b
$
        [(Depth
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall x. Adds x => [String] -> x -> x -> x
minus [String
"genFromOrdCond"] c
n (forall x. Adds x => [String] -> Depth -> x
fromI [] Depth
1)) | forall x. Adds x => OrdCond -> x -> x -> Bool
runOrdCondition OrdCond
GTH c
n forall x. Adds x => x
zero Bool -> Bool -> Bool
|| Bool
canBeNegative]
          forall a. [a] -> [a] -> [a]
++ [ (Depth
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure c
n)
             , (Depth
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall x. Adds x => x -> x -> x
add c
n (forall x. Adds x => [String] -> Depth -> x
fromI [] Depth
1))
             , (Depth
10, forall a. Arbitrary a => Gen a
arbitrary)
             ]
    )
    (forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall x. Adds x => OrdCond -> x -> x -> Bool
runOrdCondition OrdCond
cond) c
n)

genPredicate :: forall era. Era era => GenEnv era -> Gen (Pred era, GenEnv era)
genPredicate :: forall era. Era era => GenEnv era -> Gen (Pred era, GenEnv era)
genPredicate GenEnv era
env =
  forall a. HasCallStack => [(Depth, Gen a)] -> Gen a
frequency forall a b. (a -> b) -> a -> b
$
    [(Depth
1, Gen (Pred era, GenEnv era)
fixedSizedC)]
      forall a. [a] -> [a] -> [a]
++ [(Depth
1, Gen (Pred era, GenEnv era)
varSizedC)]
      forall a. [a] -> [a] -> [a]
++ [(Depth
1, Gen (Pred era, GenEnv era)
eqC)]
      forall a. [a] -> [a] -> [a]
++ [(Depth
1, Gen (Pred era, GenEnv era)
subsetC)]
      forall a. [a] -> [a] -> [a]
++ [(Depth
1, Gen (Pred era, GenEnv era)
disjointC)]
      forall a. [a] -> [a] -> [a]
++ [(Depth
1, Gen (Pred era, GenEnv era)
sumsToC)]
      forall a. [a] -> [a] -> [a]
++ [(Depth
1, Gen (Pred era, GenEnv era)
hasDomC)]
  where
    withValue ::
      forall t.
      Gen (Term era t, GenEnv era) ->
      (Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era)) ->
      Gen (Pred era, GenEnv era)
    withValue :: forall t.
Gen (Term era t, GenEnv era)
-> (Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
withValue Gen (Term era t, GenEnv era)
genTm Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era)
k = do
      (Term era t
tm, GenEnv era
env') <- Gen (Term era t, GenEnv era)
genTm
      case forall x. Typed x -> Either [String] x
runTyped forall a b. (a -> b) -> a -> b
$ forall era t. Env era -> Term era t -> Typed t
runTerm (forall era. GenEnv era -> Env era
gEnv GenEnv era
env') Term era t
tm of
        Left [String]
errs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era. [String] -> Pred era
errPred [String]
errs, GenEnv era
env')
        Right t
val -> Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era)
k Term era t
tm t
val GenEnv era
env'

    goodSized :: (Pred era, b) -> Bool
goodSized (Sized Term era Size
_ Rng {}, b
_) = Bool
False -- TODO/sizedRng
    goodSized (Pred era, b)
_ = Bool
True

    -- Fixed size
    fixedSizedC :: Gen (Pred era, GenEnv era)
fixedSizedC = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Gen a -> (a -> Bool) -> Gen a
suchThat forall {era} {b}. (Pred era, b) -> Bool
goodSized forall a b. (a -> b) -> a -> b
$ do
      TypeInEra Rep era t
rep <- forall era. Gen (TypeInEra era)
genValType
      forall t.
Gen (Term era t, GenEnv era)
-> (Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
withValue (forall era t.
Era era =>
GenEnv era -> Rep era t -> VarSpec -> Gen (Term era t, GenEnv era)
genTerm GenEnv era
env (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep) (Depth -> VarSpec
VarTerm Depth
1)) forall a b. (a -> b) -> a -> b
$ \Term era (Set t)
set Set t
val GenEnv era
env' ->
        let n :: Term era Size
n = forall era. Era era => Depth -> Term era Size
ExactSize (forall t. Sizeable t => t -> Depth
getSize Set t
val)
         in forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized Term era Size
n Term era (Set t)
set, forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved (forall era t. Term era t -> HashSet (Name era)
vars Term era (Set t)
set) Depth
1 GenEnv era
env')

    -- Fresh variable for size.
    varSizedC :: Gen (Pred era, GenEnv era)
varSizedC = do
      TypeInEra Rep era t
rep <- forall era. Gen (TypeInEra era)
genValType
      forall t.
Gen (Term era t, GenEnv era)
-> (Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
withValue (forall era t.
Era era =>
GenEnv era -> Rep era t -> VarSpec -> Gen (Term era t, GenEnv era)
genTerm GenEnv era
env (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep) VarSpec
KnownTerm) forall a b. (a -> b) -> a -> b
$ \Term era (Set t)
set Set t
val GenEnv era
env' -> do
        String
name <- forall era. GenEnv era -> Gen String
genFreshVarName GenEnv era
env'
        let vvar :: V era Size
vvar = forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
name forall era. Rep era Size
SizeR forall era s t. Access era s t
No
            intn :: Depth
intn = forall t. Sizeable t => t -> Depth
getSize Set t
val
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era t. V era t -> Term era t
Var V era Size
vvar) Term era (Set t)
set, forall era t. V era t -> t -> Depth -> GenEnv era -> GenEnv era
addSolvedVar V era Size
vvar (Depth -> Depth -> Size
SzRng Depth
intn Depth
intn) (Depth
1 forall a. Num a => a -> a -> a
+ forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env' Term era (Set t)
set) GenEnv era
env')

    eqC :: Gen (Pred era, GenEnv era)
eqC = do
      TypeInEra Rep era t
rep <- forall era. Gen (TypeInEra era)
genType
      forall t.
Gen (Term era t, GenEnv era)
-> (Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
withValue (forall era t.
Era era =>
GenEnv era -> Rep era t -> VarSpec -> Gen (Term era t, GenEnv era)
genTerm GenEnv era
env Rep era t
rep VarSpec
KnownTerm) forall a b. (a -> b) -> a -> b
$ \Term era t
lhs t
val GenEnv era
env' -> do
        let d :: Depth
d = Depth
1 forall a. Num a => a -> a -> a
+ forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env' Term era t
lhs
        (Term era t
rhs, GenEnv era
env'') <- forall era t.
Era era =>
GenEnv era
-> Rep era t
-> (t -> Bool)
-> Gen t
-> VarSpec
-> Gen (Term era t, GenEnv era)
genTerm' GenEnv era
env' Rep era t
rep (forall a. Eq a => a -> a -> Bool
== t
val) (forall (f :: * -> *) a. Applicative f => a -> f a
pure t
val) (Depth -> VarSpec
VarTerm Depth
d)
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term era t
lhs forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era t
rhs, forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved (forall era t. Term era t -> HashSet (Name era)
vars Term era t
rhs) Depth
d GenEnv era
env'')

    subsetC :: Gen (Pred era, GenEnv era)
subsetC
      | OrderInfo -> Bool
setBeforeSubset (forall era. GenEnv era -> OrderInfo
gOrder GenEnv era
env) = do
          -- Known superset
          TypeInEra Rep era t
rep <- forall era. Gen (TypeInEra era)
genValType
          forall t.
Gen (Term era t, GenEnv era)
-> (Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
withValue (forall era t.
Era era =>
GenEnv era -> Rep era t -> VarSpec -> Gen (Term era t, GenEnv era)
genTerm GenEnv era
env (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep) VarSpec
KnownTerm) forall a b. (a -> b) -> a -> b
$ \Term era (Set t)
sup Set t
val GenEnv era
env' -> do
            let d :: Depth
d = Depth
1 forall a. Num a => a -> a -> a
+ forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env' Term era (Set t)
sup
            (Term era (Set t)
sub, GenEnv era
env'') <-
              forall era t.
Era era =>
GenEnv era
-> Rep era t
-> (t -> Bool)
-> Gen t
-> VarSpec
-> Gen (Term era t, GenEnv era)
genTerm'
                GenEnv era
env'
                (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep)
                (forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set t
val)
                (forall a. Ord a => [String] -> Set a -> Gen (Set a)
subsetFromSet [String
"From genPredicate subsetC"] Set t
val)
                (Depth -> VarSpec
VarTerm Depth
d)
            forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term era (Set t)
sub forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` Term era (Set t)
sup, forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved (forall era t. Term era t -> HashSet (Name era)
vars Term era (Set t)
sub) Depth
d GenEnv era
env'')
      | Bool
otherwise = do
          -- Known subset
          TypeInEra Rep era t
rep <- forall era. Gen (TypeInEra era)
genValType
          forall t.
Gen (Term era t, GenEnv era)
-> (Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
withValue (forall era t.
Era era =>
GenEnv era -> Rep era t -> VarSpec -> Gen (Term era t, GenEnv era)
genTerm GenEnv era
env (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep) VarSpec
KnownTerm) forall a b. (a -> b) -> a -> b
$ \Term era (Set t)
sub Set t
val GenEnv era
env' -> do
            let d :: Depth
d = Depth
1 forall a. Num a => a -> a -> a
+ forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env' Term era (Set t)
sub
            (Term era (Set t)
sup, GenEnv era
env'') <-
              forall era t.
Era era =>
GenEnv era
-> Rep era t
-> (t -> Bool)
-> Gen t
-> VarSpec
-> Gen (Term era t, GenEnv era)
genTerm'
                GenEnv era
env'
                (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep)
                (forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set t
val)
                (forall a. Ord a => Set a -> Set a -> Set a
Set.union Set t
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era b. Rep era b -> Gen b
genRep (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep))
                (Depth -> VarSpec
VarTerm Depth
d)
            forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term era (Set t)
sub forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` Term era (Set t)
sup, forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved (forall era t. Term era t -> HashSet (Name era)
vars Term era (Set t)
sup) Depth
d GenEnv era
env'')

    -- Disjoint, left KnownTerm and right VarTerm
    disjointC :: Gen (Pred era, GenEnv era)
disjointC = do
      TypeInEra Rep era t
rep <- forall era. Gen (TypeInEra era)
genValType
      forall t.
Gen (Term era t, GenEnv era)
-> (Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
withValue (forall era t.
Era era =>
GenEnv era -> Rep era t -> VarSpec -> Gen (Term era t, GenEnv era)
genTerm GenEnv era
env (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep) VarSpec
KnownTerm) forall a b. (a -> b) -> a -> b
$ \Term era (Set t)
lhs Set t
val GenEnv era
env' -> do
        let d :: Depth
d = Depth
1 forall a. Num a => a -> a -> a
+ forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env' Term era (Set t)
lhs
        (Term era (Set t)
rhs, GenEnv era
env'') <-
          forall era t.
Era era =>
GenEnv era
-> Rep era t
-> (t -> Bool)
-> Gen t
-> VarSpec
-> Gen (Term era t, GenEnv era)
genTerm'
            GenEnv era
env'
            (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep)
            (forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set t
val)
            ((forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set t
val) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era b. Rep era b -> Gen b
genRep (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep))
            (Depth -> VarSpec
VarTerm Depth
d)
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint Term era (Set t)
lhs Term era (Set t)
rhs, forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved (forall era t. Term era t -> HashSet (Name era)
vars Term era (Set t)
rhs) Depth
d GenEnv era
env'')

    -- SumsTo constraint, only Map Int Int at the moment.
    sumsToC :: Gen (Pred era, GenEnv era)
sumsToC
      | OrderInfo -> Bool
sumBeforeParts (forall era. GenEnv era -> OrderInfo
gOrder GenEnv era
env) =
          -- Known sum
          forall t.
Gen (Term era t, GenEnv era)
-> (Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
withValue (forall era t.
Era era =>
GenEnv era
-> Rep era t
-> (t -> Bool)
-> Gen t
-> VarSpec
-> Gen (Term era t, GenEnv era)
genTerm' GenEnv era
env forall era. Rep era Coin
CoinR (forall a. Ord a => a -> a -> Bool
> Integer -> Coin
Coin Integer
10) ((forall a. Semigroup a => a -> a -> a
<> Integer -> Coin
Coin Integer
10) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary) VarSpec
KnownTerm) forall a b. (a -> b) -> a -> b
$ \Term era Coin
sumTm Coin
val GenEnv era
env' -> do
            let d :: Depth
d = Depth
1 forall a. Num a => a -> a -> a
+ forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env' Term era Coin
sumTm

                genParts :: [Coin] -> GenEnv era -> Gen ([Sum era Coin], GenEnv era)
genParts [] GenEnv era
env0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], GenEnv era
env0)
                genParts (Coin
n : [Coin]
ns) GenEnv era
env0 = do
                  (Term era (Map Coin Coin)
t, GenEnv era
env1) <-
                    forall era t.
Era era =>
GenEnv era
-> Rep era t
-> (t -> Bool)
-> Gen t
-> VarSpec
-> Gen (Term era t, GenEnv era)
genTerm'
                      GenEnv era
env0
                      (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Rep era Coin
CoinR forall era. Rep era Coin
CoinR)
                      ((forall a. Eq a => a -> a -> Bool
== Coin
n) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold)
                      (Coin -> Gen (Map Coin Coin)
mapWithSum Coin
n)
                      (Depth -> VarSpec
VarTerm Depth
d)
                  forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map Coin Coin)
t forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Coin] -> GenEnv era -> Gen ([Sum era Coin], GenEnv era)
genParts [Coin]
ns GenEnv era
env1
            -- TODO: It's unclear what the requirements are on the parts when solving sumBeforeParts.
            -- The solver fails if you have multiple unknown variables. Generating only a single part
            -- for now, since sumBeforeParts is anyway disabled due to TODO/SumSet.
            -- count <- choose (1, min 3 val)
            let count :: Depth
count = Depth
1
            Depth
small <- forall x. Adds x => Gen Depth
genSmall @Coin
            [Coin]
partSums <- forall x. Adds x => x -> [String] -> Depth -> x -> Gen [x]
partition (forall x. Adds x => [String] -> Depth -> x
fromI [] Depth
small) [String
"sumdToC in Tests.hs"] Depth
count Coin
val
            ([Sum era Coin]
parts, GenEnv era
env'') <- [Coin] -> GenEnv era -> Gen ([Sum era Coin], GenEnv era)
genParts [Coin]
partSums GenEnv era
env'
            -- At some point we should generate a random TestCond other than EQL
            forall (f :: * -> *) a. Applicative f => a -> f a
pure
              ( 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 (forall x. Adds x => [String] -> Depth -> x
fromI [] Depth
small)) Term era Coin
sumTm OrdCond
EQL [Sum era Coin]
parts
              , forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall era r. HashSet (Name era) -> Sum era r -> HashSet (Name era)
varsOfSum forall a. Monoid a => a
mempty) [Sum era Coin]
parts) Depth
d GenEnv era
env''
              )
      -- FIXME Left means that sumTm is known. Not sure if that is what is needed here.
      | Bool
otherwise =
          forall a. HasCallStack => [Gen a] -> Gen a
oneof
            [ forall c.
(Adds c, Arbitrary c) =>
Rep era c -> Bool -> Gen (Pred era, GenEnv era)
sumCKnownSets forall era. Rep era Coin
CoinR Bool
False
            , forall c.
(Adds c, Arbitrary c) =>
Rep era c -> Bool -> Gen (Pred era, GenEnv era)
sumCKnownSets forall era. Rep era DeltaCoin
DeltaCoinR Bool
True
            ]

    -- Avoid constraints where the same variable appears in multiple parts, since we can't solve
    -- these when the variable is unknown.
    uniqueVars :: Pred era -> Bool
uniqueVars (SumsTo Direct c
_ Term era c
_ OrdCond
_ [Sum era c]
parts) =
      forall (t :: * -> *). Foldable t => t Bool -> Bool
and
        [ forall a. Hashable a => HashSet a -> HashSet a -> Bool
hashSetDisjoint HashSet (Name era)
us HashSet (Name era)
vs
        | HashSet (Name era)
us : [HashSet (Name era)]
vss <- forall a. [a] -> [[a]]
List.tails forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall era r. HashSet (Name era) -> Sum era r -> HashSet (Name era)
varsOfSum forall a. Monoid a => a
mempty) [Sum era c]
parts
        , HashSet (Name era)
vs <- [HashSet (Name era)]
vss
        ]
    uniqueVars Pred era
_ = Bool
True

    sumCKnownSets ::
      forall c.
      (Adds c, Arbitrary c) =>
      Rep era c ->
      Bool ->
      Gen (Pred era, GenEnv era)
    sumCKnownSets :: forall c.
(Adds c, Arbitrary c) =>
Rep era c -> Bool -> Gen (Pred era, GenEnv era)
sumCKnownSets Rep era c
rep Bool
canBeNegative = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Gen a -> (a -> Bool) -> Gen a
suchThat (forall {era}. Pred era -> Bool
uniqueVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ do
      let genParts :: Depth
-> GenEnv era
-> ([Sum era c] -> c -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
genParts Depth
0 GenEnv era
env0 [Sum era c] -> c -> GenEnv era -> Gen (Pred era, GenEnv era)
k = [Sum era c] -> c -> GenEnv era -> Gen (Pred era, GenEnv era)
k [] forall x. Adds x => x
zero GenEnv era
env0
          genParts Depth
n GenEnv era
env0 [Sum era c] -> c -> GenEnv era -> Gen (Pred era, GenEnv era)
k = do
            TypeInEra Rep era t
krep <- forall era. Gen (TypeInEra era)
genKeyType
            forall t.
Gen (Term era t, GenEnv era)
-> (Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
withValue (forall era t.
Era era =>
GenEnv era -> Rep era t -> VarSpec -> Gen (Term era t, GenEnv era)
genTerm GenEnv era
env0 (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era t
krep Rep era c
rep) VarSpec
KnownTerm) forall a b. (a -> b) -> a -> b
$ \Term era (Map t c)
expr Map t c
val GenEnv era
env1 ->
              Depth
-> GenEnv era
-> ([Sum era c] -> c -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
genParts (Depth
n forall a. Num a => a -> a -> a
- Depth
1) GenEnv era
env1 forall a b. (a -> b) -> a -> b
$ \[Sum era c]
parts c
tot ->
                [Sum era c] -> c -> GenEnv era -> Gen (Pred era, GenEnv era)
k (forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map t c)
expr forall a. a -> [a] -> [a]
: [Sum era c]
parts) (forall x. Adds x => x -> x -> x
add (forall (t :: * -> *) c. (Foldable t, Adds c) => t c -> c
sumAdds Map t c
val) c
tot)
      Depth
count <- forall a. Random a => (a, a) -> Gen a
choose (Depth
1, Depth
3 :: Int)
      Depth
-> GenEnv era
-> ([Sum era c] -> c -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
genParts Depth
count GenEnv era
env forall a b. (a -> b) -> a -> b
$ \[Sum era c]
parts c
tot GenEnv era
env' -> do
        OrdCond
cmp <- forall a. HasCallStack => [a] -> Gen a
elements forall a b. (a -> b) -> a -> b
$ [OrdCond
EQL, OrdCond
LTE, OrdCond
GTH, OrdCond
GTE] forall a. [a] -> [a] -> [a]
++ [OrdCond
LTH | Bool
canBeNegative] -- TODO/negativeCoin
        let d :: Depth
d = Depth
1 forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Depth
0 forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall era c. GenEnv era -> Sum era c -> Depth
depthOfSum GenEnv era
env') [Sum era c]
parts)
        (Term era c
sumTm, GenEnv era
env'') <-
          forall era t.
Era era =>
GenEnv era
-> Rep era t
-> (t -> Bool)
-> Gen t
-> VarSpec
-> Gen (Term era t, GenEnv era)
genTerm'
            GenEnv era
env'
            Rep era c
rep
            (forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall x. Adds x => OrdCond -> x -> x -> Bool
runOrdCondition OrdCond
cmp) c
tot)
            (forall c. (Arbitrary c, Adds c) => OrdCond -> Bool -> c -> Gen c
genFromOrdCond OrdCond
cmp Bool
canBeNegative c
tot)
            (Depth -> VarSpec
VarTerm Depth
d)
        Depth
small <- forall x. Adds x => Gen Depth
genSmall @c
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (forall x. Adds x => [String] -> Depth -> x
fromI [] Depth
small)) Term era c
sumTm OrdCond
cmp [Sum era c]
parts, forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved (forall era t. Term era t -> HashSet (Name era)
vars Term era c
sumTm) Depth
d GenEnv era
env'')
    -- FIXME Right means that the parts are all known. Not sure if that is what is needed here.

    hasDomC :: Gen (Pred era, GenEnv era)
hasDomC =
      forall a. HasCallStack => [Gen a] -> Gen a
oneof
        [ do
            -- Known map
            TypeInEra Rep era t
krep <- forall era. Gen (TypeInEra era)
genKeyType
            TypeInEra Rep era t
vrep <- forall era. Gen (TypeInEra era)
genValType
            forall t.
Gen (Term era t, GenEnv era)
-> (Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
withValue (forall era t.
Era era =>
GenEnv era -> Rep era t -> VarSpec -> Gen (Term era t, GenEnv era)
genTerm GenEnv era
env (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era t
krep Rep era t
vrep) VarSpec
KnownTerm) forall a b. (a -> b) -> a -> b
$ \Term era (Map t t)
mapTm Map t t
val GenEnv era
env' -> do
              let d :: Depth
d = Depth
1 forall a. Num a => a -> a -> a
+ forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env' Term era (Map t t)
mapTm
              (Term era (Set t)
domTm, GenEnv era
env'') <-
                forall era t.
Era era =>
GenEnv era
-> Rep era t
-> (t -> Bool)
-> Gen t
-> VarSpec
-> Gen (Term era t, GenEnv era)
genTerm'
                  GenEnv era
env'
                  (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
krep)
                  (forall a. Eq a => a -> a -> Bool
== forall k a. Map k a -> Set k
Map.keysSet Map t t
val)
                  (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> Set k
Map.keysSet Map t t
val)
                  (Depth -> VarSpec
VarTerm Depth
d)
              forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map t t)
mapTm forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Set t)
domTm, GenEnv era
env'')
        , do
            -- Known domain
            TypeInEra Rep era t
krep <- forall era. Gen (TypeInEra era)
genKeyType
            TypeInEra Rep era t
vrep <- forall era. Gen (TypeInEra era)
genValType
            forall t.
Gen (Term era t, GenEnv era)
-> (Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
withValue (forall era t.
Era era =>
GenEnv era -> Rep era t -> VarSpec -> Gen (Term era t, GenEnv era)
genTerm GenEnv era
env (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
krep) VarSpec
KnownTerm) forall a b. (a -> b) -> a -> b
$ \Term era (Set t)
domTm Set t
val GenEnv era
env' -> do
              let d :: Depth
d = Depth
1 forall a. Num a => a -> a -> a
+ forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env' Term era (Set t)
domTm
              (Term era (Map t t)
mapTm, GenEnv era
env'') <-
                forall era t.
Era era =>
GenEnv era
-> Rep era t
-> (t -> Bool)
-> Gen t
-> VarSpec
-> Gen (Term era t, GenEnv era)
genTerm'
                  GenEnv era
env'
                  (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era t
krep Rep era t
vrep)
                  ((Set t
val forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> Set k
Map.keysSet)
                  (forall era v k.
Era era =>
GenEnv era -> Rep era v -> Set k -> Gen (Map k v)
genMapLiteralWithDom GenEnv era
env Rep era t
vrep Set t
val)
                  (Depth -> VarSpec
VarTerm Depth
d)
              forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term era (Set t)
domTm forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map t t)
mapTm, GenEnv era
env'')
        ]

genPreds :: Era era => GenEnv era -> Gen ([Pred era], GenEnv era)
genPreds :: forall era. Era era => GenEnv era -> Gen ([Pred era], GenEnv era)
genPreds = \GenEnv era
env -> do
  Depth
n <- forall a. Random a => (a, a) -> Gen a
choose (Depth
1, Depth
40)
  forall {t} {era}.
(Eq t, Num t, Era era) =>
t -> GenEnv era -> Gen ([Pred era], GenEnv era)
loop (Depth
n :: Int) GenEnv era
env
  where
    loop :: t -> GenEnv era -> Gen ([Pred era], GenEnv era)
loop t
n GenEnv era
env
      | t
n forall a. Eq a => a -> a -> Bool
== t
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], GenEnv era
env)
      | Bool
otherwise = do
          (Pred era
pr, GenEnv era
env') <- forall era. Era era => GenEnv era -> Gen (Pred era, GenEnv era)
genPredicate GenEnv era
env
          forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (Pred era
pr forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> GenEnv era -> Gen ([Pred era], GenEnv era)
loop (t
n forall a. Num a => a -> a -> a
- t
1) GenEnv era
env'

withEq :: Rep era t -> (Eq t => a) -> Maybe a
withEq :: forall era t a. Rep era t -> (Eq t => a) -> Maybe a
withEq (SetR Rep era a
r) Eq t => a
cont = forall era t a. Rep era t -> (Eq t => a) -> Maybe a
withEq Rep era a
r Eq t => a
cont
withEq (MapR Rep era a
kr Rep era b
vr) Eq t => a
cont = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall era t a. Rep era t -> (Eq t => a) -> Maybe a
withEq Rep era a
kr (forall era t a. Rep era t -> (Eq t => a) -> Maybe a
withEq Rep era b
vr Eq t => a
cont)
withEq Rep era t
CoinR Eq t => a
cont = forall a. a -> Maybe a
Just Eq t => a
cont
withEq Rep era t
_ Eq t => a
_ = forall a. Maybe a
Nothing

-- We can't drop constraints due to dependency limitations. There needs to be at least one
-- constraint to solve each variable. We can replace constraints by Random though!
shrinkPreds :: forall era. Era era => ([Pred era], GenEnv era) -> [([Pred era], GenEnv era)]
shrinkPreds :: forall era.
Era era =>
([Pred era], GenEnv era) -> [([Pred era], GenEnv era)]
shrinkPreds ([Pred era]
preds, GenEnv era
env) =
  [ ([Pred era]
preds', GenEnv era
env')
  | [Pred era]
preds' <- forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList Pred era -> [Pred era]
shrinkPred [Pred era]
preds
  , let defined :: HashSet (Name era)
defined = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Pred era -> HashSet (Name era)
def [Pred era]
preds'
        env' :: GenEnv era
env' = GenEnv era
env {gEnv :: Env era
gEnv = forall {era} {era}. HashSet (Name era) -> Env era -> Env era
pruneEnv HashSet (Name era)
defined (forall era. GenEnv era -> Env era
gEnv GenEnv era
env)}
  , HashSet (Name era) -> [Pred era] -> Bool
depCheck forall a. Monoid a => a
mempty [Pred era]
preds'
  ]
  where
    -- Shrink to a Random constraint defining the same variables. The makes sure we respect the
    -- OrderInfo.
    shrinkPred :: Pred era -> [Pred era]
shrinkPred Random {} = []
    shrinkPred Pred era
c = forall a. (a -> Bool) -> [a] -> [a]
filter (Pred era -> Pred era -> Bool
checkDefs Pred era
c) forall a b. (a -> b) -> a -> b
$ Pred era -> [Pred era]
shrinkToValue Pred era
c forall a. [a] -> [a] -> [a]
++ forall {era}. Pred era -> [Pred era]
shrinkToRandom Pred era
c

    checkDefs :: Pred era -> Pred era -> Bool
checkDefs Pred era
orig Pred era
shrunk = Pred era -> HashSet (Name era)
def Pred era
orig forall a. Eq a => a -> a -> Bool
== Pred era -> HashSet (Name era)
def Pred era
shrunk Bool -> Bool -> Bool
&& Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ Pred era -> HashSet (Name era)
def Pred era
shrunk)

    shrinkToValue :: Pred era -> [Pred era]
shrinkToValue (Lit {} :=: Var {}) = []
    shrinkToValue Pred era
c =
      [ Pred era
c'
      | Name x :: V era t
x@(V String
_ Rep era t
r Access era s t
_) <- forall a. HashSet a -> [a]
HashSet.toList forall a b. (a -> b) -> a -> b
$ Pred era -> HashSet (Name era)
def Pred era
c
      , Right t
v <- [forall x. Typed x -> Either [String] x
runTyped forall a b. (a -> b) -> a -> b
$ forall era t. Env era -> Term era t -> Typed t
runTerm (forall era. GenEnv era -> Env era
gEnv GenEnv era
env) (forall era t. V era t -> Term era t
Var V era t
x)]
      , Just Pred era
c' <- [forall era t a. Rep era t -> (Eq t => a) -> Maybe a
withEq Rep era t
r forall a b. (a -> b) -> a -> b
$ forall era t. Rep era t -> t -> Term era t
Lit Rep era t
r t
v forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era t. V era t -> Term era t
Var V era t
x]
      ]

    shrinkToRandom :: Pred era -> [Pred era]
shrinkToRandom Pred era
c = [Pred era
r | r :: Pred era
r@(Random Var {}) <- forall {era}. Pred era -> [Pred era]
randoms Pred era
c]

    randoms :: Pred era -> [Pred era]
randoms (Sized Term era Size
n Term era t
t) = [forall era t. Term era t -> Pred era
Random Term era Size
n, forall era t. Term era t -> Pred era
Random Term era t
t]
    randoms (Term era (Set a)
s `Subset` Term era (Set a)
t) = [forall era t. Term era t -> Pred era
Random Term era (Set a)
s, forall era t. Term era t -> Pred era
Random Term era (Set a)
t]
    randoms (Term era a
s :=: Term era a
t) = [forall era t. Term era t -> Pred era
Random Term era a
s, forall era t. Term era t -> Pred era
Random Term era a
t]
    randoms (Disjoint Term era (Set a)
s Term era (Set a)
t) = [forall era t. Term era t -> Pred era
Random Term era (Set a)
s, forall era t. Term era t -> Pred era
Random Term era (Set a)
t]
    randoms Pred era
_ = []

    pruneEnv :: HashSet (Name era) -> Env era -> Env era
pruneEnv HashSet (Name era)
defs (Env Map String (Payload era)
vmap) = forall era. Map String (Payload era) -> Env era
Env forall a b. (a -> b) -> a -> b
$ forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\String
name Payload era
_ -> forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member String
name HashSet String
defNames) Map String (Payload era)
vmap
      where
        defNames :: HashSet String
defNames = forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
HashSet.map (\(Name (V String
name Rep era t
_ Access era s t
_)) -> String
name) HashSet (Name era)
defs

    depCheck :: HashSet (Name era) -> [Pred era] -> Bool
    depCheck :: HashSet (Name era) -> [Pred era] -> Bool
depCheck HashSet (Name era)
_ [] = Bool
True
    depCheck HashSet (Name era)
solved [Pred era]
preds'
      | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pred era]
rdy = Bool
False
      | Bool
otherwise = HashSet (Name era) -> [Pred era] -> Bool
depCheck (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Pred era -> HashSet (Name era)
def [Pred era]
rdy forall a. Semigroup a => a -> a -> a
<> HashSet (Name era)
solved) [Pred era]
rest
      where
        ([Pred era]
rdy, [Pred era]
rest) = forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition Pred era -> Bool
canSolve [Pred era]
preds'
        canSolve :: Pred era -> Bool
canSolve Pred era
c = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> Bool
HashSet.isSubsetOf (Pred era -> HashSet (Name era)
use Pred era
c) HashSet (Name era)
solved

    deps :: Pred era -> Map (Name era) (HashSet (Name era))
deps Pred era
c = forall era.
Era era =>
OrderInfo
-> Map (Name era) (HashSet (Name era))
-> Pred era
-> Map (Name era) (HashSet (Name era))
accumdep (forall era. GenEnv era -> OrderInfo
gOrder GenEnv era
env) forall a. Monoid a => a
mempty Pred era
c
    def :: Pred era -> HashSet (Name era)
def Pred era
x = (forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> Set k
Map.keysSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred era -> Map (Name era) (HashSet (Name era))
deps) Pred era
x
    use :: Pred era -> HashSet (Name era)
use = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred era -> Map (Name era) (HashSet (Name era))
deps

-- Tests ---

testProof :: Proof ShelleyEra
testProof :: Proof ShelleyEra
testProof = Proof ShelleyEra
Shelley

testEnv :: Env ShelleyEra
testEnv :: Env ShelleyEra
testEnv = forall era. Map String (Payload era) -> Env era
Env forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(String
"A", forall era t s. Rep era t -> t -> Access era s t -> Payload era
Payload forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
5) forall era s t. Access era s t
No)]

ensureRight :: Testable prop => Either [String] a -> (a -> prop) -> Property
ensureRight :: forall prop a.
Testable prop =>
Either [String] a -> (a -> prop) -> Property
ensureRight (Left [String]
errs) a -> prop
_ = forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines [String]
errs) Bool
False
ensureRight (Right a
x) a -> prop
prop = forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ a -> prop
prop a
x

ifRight :: Testable prop => Either [String] a -> (a -> prop) -> Property
ifRight :: forall prop a.
Testable prop =>
Either [String] a -> (a -> prop) -> Property
ifRight Left {} a -> prop
_ = Bool
False forall prop. Testable prop => Bool -> prop -> Property
==> Bool
False
ifRight (Right a
x) a -> prop
prop = forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ a -> prop
prop a
x

ensureTyped :: Testable prop => Typed a -> (a -> prop) -> Property
ensureTyped :: forall prop a. Testable prop => Typed a -> (a -> prop) -> Property
ensureTyped = forall prop a.
Testable prop =>
Either [String] a -> (a -> prop) -> Property
ensureRight forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. Typed x -> Either [String] x
runTyped

ifTyped :: Testable prop => Typed a -> (a -> prop) -> Property
ifTyped :: forall prop a. Testable prop => Typed a -> (a -> prop) -> Property
ifTyped = forall prop a.
Testable prop =>
Either [String] a -> (a -> prop) -> Property
ifRight forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. Typed x -> Either [String] x
runTyped

initEnv :: OrderInfo -> GenEnv ShelleyEra
initEnv :: OrderInfo -> GenEnv ShelleyEra
initEnv OrderInfo
info =
  GenEnv
    { gOrder :: OrderInfo
gOrder = OrderInfo
info
    , gEnv :: Env ShelleyEra
gEnv = forall era. Env era
emptyEnv
    , gSolved :: Map (Name ShelleyEra) Depth
gSolved = forall a. Monoid a => a
mempty
    }

showVal :: Rep era t -> t -> String
showVal :: forall era t. Rep era t -> t -> String
showVal (SetR Rep era a
r) t
t = String
"{" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map (forall era t. Rep era t -> t -> String
synopsis Rep era a
r) (forall a. Set a -> [a]
Set.toList t
t)) forall a. [a] -> [a] -> [a]
++ String
"}"
showVal (MapR Rep era a
kr Rep era b
vr) t
t =
  String
"{" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " [forall era t. Rep era t -> t -> String
synopsis Rep era a
kr a
k forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall era t. Rep era t -> t -> String
synopsis Rep era b
vr b
v | (a
k, b
v) <- forall k a. Map k a -> [(k, a)]
Map.toList t
t] forall a. [a] -> [a] -> [a]
++ String
"}"
showVal Rep era t
rep t
t = forall era t. Rep era t -> t -> String
synopsis Rep era t
rep t
t

showTerm :: Term era t -> String
showTerm :: forall era t. Term era t -> String
showTerm (Lit Rep era t
rep t
t) = forall era t. Rep era t -> t -> String
showVal Rep era t
rep t
t
showTerm (Dom Term era (Map a b)
t) = String
"(Dom " forall a. [a] -> [a] -> [a]
++ forall era t. Term era t -> String
showTerm Term era (Map a b)
t forall a. [a] -> [a] -> [a]
++ String
")"
showTerm (Rng Term era (Map a b)
t) = String
"(Rng " forall a. [a] -> [a] -> [a]
++ forall era t. Term era t -> String
showTerm Term era (Map a b)
t forall a. [a] -> [a] -> [a]
++ String
")"
showTerm Term era t
t = forall a. Show a => a -> String
show Term era t
t

showPred :: Pred era -> String
showPred :: forall era. Pred era -> String
showPred (Term era (Set a)
sub `Subset` Term era (Set a)
sup) = forall era t. Term era t -> String
showTerm Term era (Set a)
sub forall a. [a] -> [a] -> [a]
++ String
" ⊆ " forall a. [a] -> [a] -> [a]
++ forall era t. Term era t -> String
showTerm Term era (Set a)
sup
showPred (Term era a
sub :=: Term era a
sup) = forall era t. Term era t -> String
showTerm Term era a
sub forall a. [a] -> [a] -> [a]
++ String
" == " forall a. [a] -> [a] -> [a]
++ forall era t. Term era t -> String
showTerm Term era a
sup
showPred (Disjoint Term era (Set a)
s Term era (Set a)
t) = String
"Disjoint " forall a. [a] -> [a] -> [a]
++ forall era t. Term era t -> String
showTerm Term era (Set a)
s forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall era t. Term era t -> String
showTerm Term era (Set a)
t
showPred Pred era
pr = forall a. Show a => a -> String
show Pred era
pr

showEnv :: Env era -> String
showEnv :: forall era. Env era -> String
showEnv (Env Map String (Payload era)
vmap) = [String] -> String
unlines forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {era}. (String, Payload era) -> String
pr (forall k a. Map k a -> [(k, a)]
Map.toList Map String (Payload era)
vmap)
  where
    pr :: (String, Payload era) -> String
pr (String
name, Payload Rep era t
rep t
t Access era s t
_) = String
name forall a. [a] -> [a] -> [a]
++ String
" :: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era t
rep forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall era t. Rep era t -> t -> String
showVal Rep era t
rep t
t

predConstr :: Pred era -> String
predConstr :: forall era. Pred era -> String
predConstr MetaSize {} = String
"MetaSize"
predConstr Sized {} = String
"Sized"
predConstr (Term era a
_ :=: Term era a
_) = String
":=:"
predConstr (Term era (Set a)
_ `Subset` Term era (Set a)
_) = String
"Subset"
predConstr Disjoint {} = String
"Disjoint"
predConstr SumsTo {} = String
"SumsTo"
predConstr SumSplit {} = String
"SumSplit"
predConstr Random {} = String
"Random"
predConstr Component {} = String
"Component"
predConstr CanFollow {} = String
"CanFollow"
predConstr Member {} = String
"Member"
predConstr NotMember {} = String
"NotMember"
predConstr MapMember {} = String
"MapMember"
predConstr (:<-:) {} = String
":<-:"
predConstr List {} = String
"List"
predConstr Choose {} = String
"Choose"
predConstr Maybe {} = String
"Maybe"
predConstr GenFrom {} = String
"GenFrom"
predConstr ForEach {} = String
"ForEach"
predConstr SubMap {} = String
"SubMap"
predConstr If {} = String
"If"
predConstr Before {} = String
"Before"
predConstr Oneof {} = String
"Oneof"
predConstr ListWhere {} = String
"ListWhere"

constraintProperty ::
  Bool ->
  [String] ->
  OrderInfo ->
  ([Pred ShelleyEra] -> DependGraph ShelleyEra -> Env ShelleyEra -> Property) ->
  Property
constraintProperty :: Bool
-> [String]
-> OrderInfo
-> ([Pred ShelleyEra]
    -> DependGraph ShelleyEra -> Env ShelleyEra -> Property)
-> Property
constraintProperty Bool
strict [String]
whitelist OrderInfo
info [Pred ShelleyEra]
-> DependGraph ShelleyEra -> Env ShelleyEra -> Property
prop =
  forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrink (forall era. Era era => GenEnv era -> Gen ([Pred era], GenEnv era)
genPreds forall a b. (a -> b) -> a -> b
$ OrderInfo -> GenEnv ShelleyEra
initEnv OrderInfo
info) forall era.
Era era =>
([Pred era], GenEnv era) -> [([Pred era], GenEnv era)]
shrinkPreds forall a b. (a -> b) -> a -> b
$ \([Pred ShelleyEra]
preds, GenEnv ShelleyEra
genenv) ->
    forall prop. Testable prop => String -> prop -> Property
counterexample (String
"\n-- Order --\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show OrderInfo
info) forall a b. (a -> b) -> a -> b
$
      forall prop. Testable prop => String -> prop -> Property
counterexample (String
"\n-- Constraints --\n" forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines (forall a b. (a -> b) -> [a] -> [b]
map forall era. Pred era -> String
showPred [Pred ShelleyEra]
preds)) forall a b. (a -> b) -> a -> b
$
        forall prop. Testable prop => String -> prop -> Property
counterexample (String
"-- Model solution --\n" forall a. [a] -> [a] -> [a]
++ forall era. Env era -> String
showEnv (forall era. GenEnv era -> Env era
gEnv GenEnv ShelleyEra
genenv)) forall a b. (a -> b) -> a -> b
$
          Typed (DependGraph ShelleyEra)
-> (DependGraph ShelleyEra -> Property) -> Property
checkTyped (forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile OrderInfo
info [Pred ShelleyEra]
preds) forall a b. (a -> b) -> a -> b
$ \DependGraph ShelleyEra
graph ->
            forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind (forall era.
Bool
-> Proof era
-> DependGraph era
-> Gen (Either [String] (Subst era))
genDependGraph Bool
False Proof ShelleyEra
testProof DependGraph ShelleyEra
graph) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip Either [String] (Subst ShelleyEra)
-> (Subst ShelleyEra -> Property) -> Property
checkRight forall a b. (a -> b) -> a -> b
$ \Subst ShelleyEra
subst ->
              let env :: Env ShelleyEra
env = forall t. HasCallStack => Typed t -> t
errorTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst ShelleyEra
subst forall era. Env era
emptyEnv
                  n :: Depth
n = let Env Map String (Payload ShelleyEra)
e = forall era. GenEnv era -> Env era
gEnv GenEnv ShelleyEra
genenv in forall k a. Map k a -> Depth
Map.size Map String (Payload ShelleyEra)
e
               in forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Var count" [forall a. Show a => a -> String
show Depth
n] forall a b. (a -> b) -> a -> b
$
                    forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Constraint types" (forall a b. (a -> b) -> [a] -> [b]
map forall era. Pred era -> String
predConstr [Pred ShelleyEra]
preds) forall a b. (a -> b) -> a -> b
$
                      [Pred ShelleyEra]
-> DependGraph ShelleyEra -> Env ShelleyEra -> Property
prop [Pred ShelleyEra]
preds DependGraph ShelleyEra
graph Env ShelleyEra
env
  where
    checkTyped :: Typed (DependGraph ShelleyEra)
-> (DependGraph ShelleyEra -> Property) -> Property
checkTyped
      | Bool
strict = forall prop a.
Testable prop =>
Either [String] a -> (a -> prop) -> Property
checkWhitelist forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. Typed x -> Either [String] x
runTyped
      | Bool
otherwise = forall prop a. Testable prop => Typed a -> (a -> prop) -> Property
ifTyped
    checkRight :: Either [String] (Subst ShelleyEra)
-> (Subst ShelleyEra -> Property) -> Property
checkRight
      | Bool
strict = forall prop a.
Testable prop =>
Either [String] a -> (a -> prop) -> Property
checkWhitelist
      | Bool
otherwise = forall prop a.
Testable prop =>
Either [String] a -> (a -> prop) -> Property
ifRight

    checkWhitelist :: Testable prop => Either [String] a -> (a -> prop) -> Property
    checkWhitelist :: forall prop a.
Testable prop =>
Either [String] a -> (a -> prop) -> Property
checkWhitelist (Left [String]
errs) a -> prop
_ =
      forall (t :: * -> *). Foldable t => t Bool -> Bool
and
        [ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
white String
err
        | String
white <- [String]
whitelist
        , String
err <- [String]
errs
        ]
        forall prop. Testable prop => Bool -> prop -> Property
==> forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines [String]
errs) Bool
False
    checkWhitelist (Right a
x) a -> prop
k = forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ a -> prop
k a
x

checkPredicates :: [Pred era] -> Env era -> Property
checkPredicates :: forall era. [Pred era] -> Env era -> Property
checkPredicates [Pred era]
preds Env era
env =
  forall prop. Testable prop => String -> prop -> Property
counterexample (String
"-- Solution --\n" forall a. [a] -> [a] -> [a]
++ forall era. Env era -> String
showEnv Env era
env) forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map Pred era -> Property
checkPred [Pred era]
preds
  where
    checkPred :: Pred era -> Property
checkPred Pred era
pr = forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Failed: " forall a. [a] -> [a] -> [a]
++ forall era. Pred era -> String
showPred Pred era
pr) forall a b. (a -> b) -> a -> b
$ forall prop a. Testable prop => Typed a -> (a -> prop) -> Property
ensureTyped (forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env Pred era
pr) forall a. a -> a
id

runPreds :: [Pred ShelleyEra] -> IO ()
runPreds :: [Pred ShelleyEra] -> IO ()
runPreds [Pred ShelleyEra]
ps = do
  let info :: OrderInfo
info = OrderInfo
standardOrderInfo
  Right DependGraph ShelleyEra
g <- forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall x. Typed x -> Either [String] x
runTyped forall a b. (a -> b) -> a -> b
$ forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile OrderInfo
info [Pred ShelleyEra]
ps
  Either [String] (Subst ShelleyEra)
subst <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall era.
Bool
-> Proof era
-> DependGraph era
-> Gen (Either [String] (Subst era))
genDependGraph Bool
True Proof ShelleyEra
testProof DependGraph ShelleyEra
g
  forall a. Show a => a -> IO ()
print Either [String] (Subst ShelleyEra)
subst

-- | Generate a set of satisfiable constraints and check that we can generate a solution and that it
--   actually satisfies the constraints.
prop_soundness :: OrderInfo -> Property
prop_soundness :: OrderInfo -> Property
prop_soundness OrderInfo
x = Bool -> [String] -> OrderInfo -> Property
prop_soundness' Bool
False [] OrderInfo
x

defaultWhitelist :: [String]
defaultWhitelist :: [String]
defaultWhitelist = [String
"Size specifications", String
"The SetSpec's are inconsistent", String
"The MapSpec's are inconsistent"]

-- | If argument is True, fail property if constraints cannot be solved. Otherwise discard unsolved
--   constraints.
prop_soundness' :: Bool -> [String] -> OrderInfo -> Property
prop_soundness' :: Bool -> [String] -> OrderInfo -> Property
prop_soundness' Bool
strict [String]
whitelist OrderInfo
info =
  Bool
-> [String]
-> OrderInfo
-> ([Pred ShelleyEra]
    -> DependGraph ShelleyEra -> Env ShelleyEra -> Property)
-> Property
constraintProperty Bool
strict [String]
whitelist OrderInfo
info forall a b. (a -> b) -> a -> b
$ \[Pred ShelleyEra]
preds DependGraph ShelleyEra
_graph Env ShelleyEra
env ->
    forall era. [Pred era] -> Env era -> Property
checkPredicates [Pred ShelleyEra]
preds Env ShelleyEra
env

-- | Check that shrinking is sound, i.e. that all shrink steps preserves constraint satisfaction.
prop_shrinking :: OrderInfo -> Property
prop_shrinking :: OrderInfo -> Property
prop_shrinking = Bool -> [String] -> OrderInfo -> Property
prop_shrinking' Bool
False []

prop_shrinking' :: Bool -> [String] -> OrderInfo -> Property
prop_shrinking' :: Bool -> [String] -> OrderInfo -> Property
prop_shrinking' Bool
strict [String]
whitelist OrderInfo
info =
  Bool
-> [String]
-> OrderInfo
-> ([Pred ShelleyEra]
    -> DependGraph ShelleyEra -> Env ShelleyEra -> Property)
-> Property
constraintProperty Bool
strict [String]
whitelist OrderInfo
info forall a b. (a -> b) -> a -> b
$ \[Pred ShelleyEra]
preds DependGraph ShelleyEra
graph Env ShelleyEra
env ->
    forall prop. Testable prop => String -> prop -> Property
counterexample (String
"-- Original solution --\n" forall a. [a] -> [a] -> [a]
++ forall era. Env era -> String
showEnv Env ShelleyEra
env) forall a b. (a -> b) -> a -> b
$
      let envs :: [Env ShelleyEra]
envs = forall era. DependGraph era -> Env era -> [Env era]
shrinkEnv DependGraph ShelleyEra
graph Env ShelleyEra
env
       in forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Shrinkings" [forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Depth
length [Env ShelleyEra]
envs] forall a b. (a -> b) -> a -> b
$
            forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$
              forall a b. (a -> b) -> [a] -> [b]
map (forall era. [Pred era] -> Env era -> Property
checkPredicates [Pred ShelleyEra]
preds) [Env ShelleyEra]
envs