{-# 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 Cardano.Ledger.Coin
import Cardano.Ledger.Core (Era)
import Cardano.Ledger.Shelley
import Control.Arrow (first)
import Control.Monad
import Data.Foldable (fold)
import Data.Group
import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
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 Test.Cardano.Ledger.Constrained.Ast
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)
import Prelude hiding (subtract)

{-

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
[GenEnv era] -> ShowS
GenEnv era -> String
(Depth -> GenEnv era -> ShowS)
-> (GenEnv era -> String)
-> ([GenEnv era] -> ShowS)
-> Show (GenEnv era)
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
$cshowsPrec :: forall era. Depth -> GenEnv era -> ShowS
showsPrec :: Depth -> GenEnv era -> ShowS
$cshow :: forall era. GenEnv era -> String
show :: GenEnv era -> String
$cshowList :: forall era. [GenEnv era] -> ShowS
showList :: [GenEnv era] -> ShowS
Show)

type Depth = Int

instance Arbitrary OrderInfo where
  arbitrary :: Gen OrderInfo
arbitrary = Bool -> Bool -> Bool -> OrderInfo
OrderInfo (Bool -> Bool -> Bool -> OrderInfo)
-> Gen Bool -> Gen (Bool -> Bool -> OrderInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Bool
forall a. Arbitrary a => Gen a
arbitrary Gen (Bool -> Bool -> OrderInfo)
-> Gen Bool -> Gen (Bool -> OrderInfo)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Bool
forall a. Arbitrary a => Gen a
arbitrary Gen (Bool -> OrderInfo) -> Gen Bool -> Gen OrderInfo
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Bool
forall a. Arbitrary a => Gen a
arbitrary
  shrink :: OrderInfo -> [OrderInfo]
shrink OrderInfo
info = [OrderInfo
standardOrderInfo | OrderInfo
info OrderInfo -> OrderInfo -> Bool
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 = storeVar vvar val $ gEnv 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.unionWith max new (gSolved env)}
  where
    new :: Map (Name era) Depth
new = (Name era -> Depth) -> Set (Name era) -> Map (Name era) Depth
forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (Depth -> Name era -> Depth
forall a b. a -> b -> a
const Depth
d) (HashSet (Name era) -> Set (Name era)
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 = HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved (Name era -> HashSet (Name era)
forall a. Hashable a => a -> HashSet a
HashSet.singleton (Name era -> HashSet (Name era)) -> Name era -> HashSet (Name era)
forall a b. (a -> b) -> a -> b
$ V era t -> Name era
forall era t. V era t -> Name era
Name V era t
vvar) Depth
d (GenEnv era -> GenEnv era)
-> (GenEnv era -> GenEnv era) -> GenEnv era -> GenEnv era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. V era t -> t -> GenEnv era -> GenEnv era
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 = Depth -> Name era -> Map (Name era) Depth -> Depth
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Depth
0 Name era
x (GenEnv era -> Map (Name era) Depth
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 = [Depth] -> Depth
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Depth] -> Depth) -> [Depth] -> Depth
forall a b. (a -> b) -> a -> b
$ Depth
0 Depth -> [Depth] -> [Depth]
forall a. a -> [a] -> [a]
: (Name era -> Depth) -> [Name era] -> [Depth]
forall a b. (a -> b) -> [a] -> [b]
map (GenEnv era -> Name era -> Depth
forall era. GenEnv era -> Name era -> Depth
depthOfName GenEnv era
env) (HashSet (Name era) -> [Name era]
forall a. HashSet a -> [a]
HashSet.toList (HashSet (Name era) -> [Name era])
-> HashSet (Name era) -> [Name era]
forall a b. (a -> b) -> a -> b
$ Term era t -> HashSet (Name era)
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 -> GenEnv era -> Term era (Map a c) -> Depth
forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env Term era (Map a c)
t
  SumList Term era [c]
t -> GenEnv era -> Term era [c] -> Depth
forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env Term era [c]
t
  One Term era c
t -> GenEnv era -> Term era c -> Depth
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 -> GenEnv era -> Term era x -> Depth
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 -> GenEnv era -> Term era (Map a x) -> Depth
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 -> Rep era a -> Gen (Set a)
forall a. Ord a => Rep era a -> Gen (Set a)
setLiteral Rep era a
erep
    MapR Rep era a
_ Rep era b
_ -> Rep era t -> Gen t
forall a. Rep era a -> Gen a
unconstrained Rep era t
rep -- TODO: more clever generation for maps
    Rep era t
_ -> Rep era t -> Gen 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 = Rep era a -> Gen a
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) <- Env era -> Rep era (Set a) -> [(V era (Set a), Set a)]
forall era t. Era era => Env era -> Rep era t -> [(V era t, t)]
envVarsOfType (GenEnv era -> Env era
forall era. GenEnv era -> Env era
gEnv GenEnv era
env) (Rep era a -> Rep era (Set a)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era a
erep)]
          gen :: Gen (Set a)
gen = [Gen (Set a)] -> Gen (Set a)
forall a. HasCallStack => [Gen a] -> Gen a
oneof ([Gen (Set a)] -> Gen (Set a)) -> [Gen (Set a)] -> Gen (Set a)
forall a b. (a -> b) -> a -> b
$ Rep era (Set a) -> Gen (Set a)
forall era b. Rep era b -> Gen b
genRep (Rep era a -> Rep era (Set a)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era a
erep) Gen (Set a) -> [Gen (Set a)] -> [Gen (Set a)]
forall a. a -> [a] -> [a]
: (Set a -> Gen (Set a)) -> [Set a] -> [Gen (Set a)]
forall a b. (a -> b) -> [a] -> [b]
map Set a -> Gen (Set a)
forall a. a -> Gen a
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 <- [Set a -> Set a -> Set a] -> Gen (Set a -> Set a -> Set a)
forall a. HasCallStack => [a] -> Gen a
elements [Set a -> Set a -> Set a
forall a b. a -> b -> a
const, (Set a -> Set a) -> Set a -> Set a -> Set a
forall a b. a -> b -> a
const Set a -> Set a
forall a. a -> a
id, Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union, Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection, Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.difference, (Set a -> Set a -> Set a) -> Set a -> Set a -> Set a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.difference]
      Set a -> Gen (Set a)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set a -> Gen (Set a)) -> Set a -> Gen (Set a)
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 = [String] -> Gen String
forall a. HasCallStack => [a] -> Gen a
elements ([String] -> Gen String)
-> (GenEnv era -> [String]) -> GenEnv era -> Gen String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenEnv era -> [String]
forall {era}. GenEnv era -> [String]
varNames
  where
    allTheNames :: [String]
allTheNames = [String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char
c] | String
s <- String
"" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
allTheNames, Char
c <- [Char
'A' .. Char
'Z']]
    varNames :: GenEnv era -> [String]
varNames GenEnv era
env = Depth -> [String] -> [String]
forall a. Depth -> [a] -> [a]
take Depth
10 ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> Map String (Payload era) -> Bool
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 = GenEnv era -> Env era
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 = ((String, Payload era) -> [(V era t, t)])
-> [(String, Payload era)] -> [(V era t, t)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, Payload era) -> [(V era t, t)]
wellTyped ([(String, Payload era)] -> [(V era t, t)])
-> [(String, Payload era)] -> [(V era t, t)]
forall a b. (a -> b) -> a -> b
$ Map String (Payload era) -> [(String, Payload era)]
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 Rep era t -> Rep era t -> Maybe (t :~: t)
forall i j. Rep era i -> Rep era j -> Maybe (i :~: j)
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 -> [(String -> Rep era t -> Access era s t -> V era t
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 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
(VarSpec -> VarSpec -> Bool)
-> (VarSpec -> VarSpec -> Bool) -> Eq VarSpec
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: VarSpec -> VarSpec -> Bool
== :: VarSpec -> VarSpec -> Bool
$c/= :: VarSpec -> VarSpec -> Bool
/= :: VarSpec -> VarSpec -> Bool
Eq, Depth -> VarSpec -> ShowS
[VarSpec] -> ShowS
VarSpec -> String
(Depth -> VarSpec -> ShowS)
-> (VarSpec -> String) -> ([VarSpec] -> ShowS) -> Show VarSpec
forall a.
(Depth -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Depth -> VarSpec -> ShowS
showsPrec :: Depth -> VarSpec -> ShowS
$cshow :: VarSpec -> String
show :: VarSpec -> String
$cshowList :: [VarSpec] -> ShowS
showList :: [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 = GenEnv era
-> Rep era t
-> (t -> Bool)
-> Gen t
-> VarSpec
-> Gen (Term era t, GenEnv era)
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 (Bool -> t -> Bool
forall a b. a -> b -> a
const Bool
True) (GenEnv era -> Rep era t -> Gen t
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 =
  [(Depth, Gen (Term era t, GenEnv era))]
-> Gen (Term era t, GenEnv era)
forall a. HasCallStack => [(Depth, Gen a)] -> Gen a
frequency ([(Depth, Gen (Term era t, GenEnv era))]
 -> Gen (Term era t, GenEnv era))
-> [(Depth, Gen (Term era t, GenEnv era))]
-> Gen (Term era t, GenEnv era)
forall a b. (a -> b) -> a -> b
$
    [(Depth
5, Gen (Term era t, GenEnv era)
genFixed) | VarSpec
vspec VarSpec -> VarSpec -> Bool
forall a. Eq a => a -> a -> Bool
== VarSpec
KnownTerm]
      [(Depth, Gen (Term era t, GenEnv era))]
-> [(Depth, Gen (Term era t, GenEnv era))]
-> [(Depth, Gen (Term era t, GenEnv era))]
forall a. [a] -> [a] -> [a]
++ [(Depth
5, Gen (Term era t, GenEnv era)
genExistingVar) | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [V era t] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [V era t]
allowedVars]
      [(Depth, Gen (Term era t, GenEnv era))]
-> [(Depth, Gen (Term era t, GenEnv era))]
-> [(Depth, Gen (Term era t, GenEnv era))]
forall a. [a] -> [a] -> [a]
++ [(Depth
1, Gen (Term era t, GenEnv era)
genFreshVar) | VarTerm {} <- [VarSpec
vspec]]
      [(Depth, Gen (Term era t, GenEnv era))]
-> [(Depth, Gen (Term era t, GenEnv era))]
-> [(Depth, Gen (Term era t, GenEnv era))]
forall a. [a] -> [a] -> [a]
++ [(Depth
2, Rep era a -> Gen (Term era (Set a), GenEnv era)
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]]
      [(Depth, Gen (Term era t, GenEnv era))]
-> [(Depth, Gen (Term era t, GenEnv era))]
-> [(Depth, Gen (Term era t, GenEnv era))]
forall a. [a] -> [a] -> [a]
++ [(Depth
2, Rep era a -> Gen (Term era (Set a), GenEnv era)
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 = ((V era t, t) -> V era t) -> [(V era t, t)] -> [V era t]
forall a b. (a -> b) -> [a] -> [b]
map (V era t, t) -> V era t
forall a b. (a, b) -> a
fst ([(V era t, t)] -> [V era t]) -> [(V era t, t)] -> [V era t]
forall a b. (a -> b) -> a -> b
$ ((V era t, t) -> Bool) -> [(V era t, t)] -> [(V era t, t)]
forall a. (a -> Bool) -> [a] -> [a]
filter (V era t, t) -> Bool
isValid ([(V era t, t)] -> [(V era t, t)])
-> [(V era t, t)] -> [(V era t, t)]
forall a b. (a -> b) -> a -> b
$ Env era -> Rep era t -> [(V era t, t)]
forall era t. Era era => Env era -> Rep era t -> [(V era t, t)]
envVarsOfType (GenEnv era -> Env era
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 -> (V era t -> Bool) -> [V era t] -> [V era t]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Depth -> Depth -> Bool
forall a. Ord a => a -> a -> Bool
>= Depth
d) (Depth -> Bool) -> (V era t -> Depth) -> V era t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenEnv era -> Name era -> Depth
forall era. GenEnv era -> Name era -> Depth
depthOfName GenEnv era
env (Name era -> Depth) -> (V era t -> Name era) -> V era t -> Depth
forall b c a. (b -> c) -> (a -> b) -> a -> c
. V era t -> Name era
forall era t. V era t -> Name era
Name) [V era t]
existingVars
      VarSpec
KnownTerm -> (V era t -> Bool) -> [V era t] -> [V era t]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Name era -> Map (Name era) Depth -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` GenEnv era -> Map (Name era) Depth
forall era. GenEnv era -> Map (Name era) Depth
gSolved GenEnv era
env) (Name era -> Bool) -> (V era t -> Name era) -> V era t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. V era t -> Name era
forall era t. V era t -> Name era
Name) [V era t]
existingVars

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

    genFreshVar :: Gen (Term era t, GenEnv era)
genFreshVar = do
      String
name <- GenEnv era -> Gen String
forall era. GenEnv era -> Gen String
genFreshVarName GenEnv era
env
      t
val <- Gen t
genLit
      let vvar :: V era t
vvar = String -> Rep era t -> Access era Any t -> V era t
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 Any t
forall era s t. Access era s t
No
      (Term era t, GenEnv era) -> Gen (Term era t, GenEnv era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (V era t -> Term era t
forall era t. V era t -> Term era t
Var V era t
vvar, V era t -> t -> GenEnv era -> GenEnv era
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 <- Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genValType
      (Term era (Map k t)
m, GenEnv era
env') <-
        GenEnv era
-> Rep era (Map k t)
-> (Map k t -> Bool)
-> Gen (Map k t)
-> VarSpec
-> Gen (Term era (Map k t), GenEnv era)
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 k -> Rep era t -> Rep era (Map k t)
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 (t -> Bool) -> (Map k t -> t) -> Map k t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map k t -> t
Map k t -> Set k
forall k a. Map k a -> Set k
Map.keysSet)
          (Gen t
genLit Gen t -> (t -> Gen (Map k t)) -> Gen (Map k t)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= GenEnv era -> Rep era t -> Set k -> Gen (Map k t)
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
      (Term era (Set k), GenEnv era)
-> Gen (Term era (Set k), GenEnv era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term era (Map k t) -> Term era (Set k)
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 <- Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genKeyType
      (Term era (Map t v)
m, GenEnv era
env') <-
        GenEnv era
-> Rep era (Map t v)
-> (Map t v -> Bool)
-> Gen (Map t v)
-> VarSpec
-> Gen (Term era (Map t v), GenEnv era)
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 era v -> Rep era (Map t v)
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 (t -> Bool) -> (Map t v -> t) -> Map t v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [v] -> t
[v] -> Set v
forall a. Ord a => [a] -> Set a
Set.fromList ([v] -> t) -> (Map t v -> [v]) -> Map t v -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map t v -> [v]
forall k a. Map k a -> [a]
Map.elems)
          (Gen t
genLit Gen t -> (t -> Gen (Map t v)) -> Gen (Map t v)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= GenEnv era -> Rep era t -> Set v -> Gen (Map t v)
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
      (Term era (Set v), GenEnv era)
-> Gen (Term era (Set v), GenEnv era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term era (Map t v) -> Term era (Set v)
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 = GenEnv era -> Rep era v -> Gen v
forall era t. Era era => GenEnv era -> Rep era t -> Gen t
genLiteral GenEnv era
env Rep era v
vrep
  (() -> Gen v) -> Map k () -> Gen (Map k v)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map k a -> f (Map k b)
traverse (\()
_ -> Gen v
genVal) ((k -> ()) -> Set k -> Map k ()
forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (() -> k -> ()
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 <- [String] -> Depth -> Gen k -> Gen (Set k)
forall a. Ord a => [String] -> Depth -> Gen a -> Gen (Set a)
setSized [] (Set v -> Depth
forall a. Set a -> Depth
Set.size Set v
vals) (GenEnv era -> Rep era k -> Gen k
forall era t. Era era => GenEnv era -> Rep era t -> Gen t
genLiteral GenEnv era
env Rep era k
krep)
  [v]
valsList <- [v] -> Gen [v]
forall a. [a] -> Gen [a]
shuffle ([v] -> Gen [v]) -> [v] -> Gen [v]
forall a b. (a -> b) -> a -> b
$ Set v -> [v]
forall a. Set a -> [a]
Set.toList Set v
vals
  Map k v -> Gen (Map k v)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map k v -> Gen (Map k v)) -> Map k v -> Gen (Map k v)
forall a b. (a -> b) -> a -> b
$ [(k, v)] -> Map k v
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(k, v)] -> Map k v) -> [(k, v)] -> Map k v
forall a b. (a -> b) -> a -> b
$ [k] -> [v] -> [(k, v)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Set k -> [k]
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 = [TypeInEra era] -> Gen (TypeInEra era)
forall a. HasCallStack => [a] -> Gen a
elements [Rep era Depth -> TypeInEra era
forall t era. (Show t, Ord t) => Rep era t -> TypeInEra era
TypeInEra Rep era Depth
forall era. Rep era Depth
IntR]

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

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

genType :: Gen (TypeInEra era)
genType :: forall era. Gen (TypeInEra era)
genType =
  [Gen (TypeInEra era)] -> Gen (TypeInEra era)
forall a. HasCallStack => [Gen a] -> Gen a
oneof
    [ Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genBaseType
    , TypeInEra era -> TypeInEra era
forall {era}. TypeInEra era -> TypeInEra era
setR (TypeInEra era -> TypeInEra era)
-> Gen (TypeInEra era) -> Gen (TypeInEra era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genValType
    , TypeInEra era -> TypeInEra era
forall {era}. TypeInEra era -> TypeInEra era
listR (TypeInEra era -> TypeInEra era)
-> Gen (TypeInEra era) -> Gen (TypeInEra era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genValType
    , TypeInEra era -> TypeInEra era -> TypeInEra era
forall {era}. TypeInEra era -> TypeInEra era -> TypeInEra era
mapR (TypeInEra era -> TypeInEra era -> TypeInEra era)
-> Gen (TypeInEra era) -> Gen (TypeInEra era -> TypeInEra era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genKeyType Gen (TypeInEra era -> TypeInEra era)
-> Gen (TypeInEra era) -> Gen (TypeInEra era)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genValType
    ]
  where
    setR :: TypeInEra era -> TypeInEra era
setR (TypeInEra Rep era t
t) = Rep era (Set t) -> TypeInEra era
forall t era. (Show t, Ord t) => Rep era t -> TypeInEra era
TypeInEra (Rep era t -> Rep era (Set t)
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) = Rep era [t] -> TypeInEra era
forall t era. (Show t, Ord t) => Rep era t -> TypeInEra era
TypeInEra (Rep era t -> Rep era [t]
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) = Rep era (Map t t) -> TypeInEra era
forall t era. (Show t, Ord t) => Rep era t -> TypeInEra era
TypeInEra (Rep era t -> Rep era t -> Rep era (Map t t)
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 = Rep era [String] -> [String] -> Term era [String]
forall era t. Rep era t -> t -> Term era t
Lit (Rep era String -> Rep era [String]
forall era a. Rep era a -> Rep era [a]
ListR Rep era String
forall era. Rep era String
stringR) [String
"Errors:"] Term era [String] -> Term era [String] -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Rep era [String] -> [String] -> Term era [String]
forall era t. Rep era t -> t -> Term era t
Lit (Rep era String -> Rep era [String]
forall era a. Rep era a -> Rep era [a]
ListR Rep era String
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 (Set Depth -> Set Depth) -> Gen (Set Depth) -> Gen (Set Depth)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Set Depth)
forall a. Arbitrary a => Gen a
arbitrary
  where
    fixUp :: Set Depth -> Set Depth
fixUp Set Depth
s
      | Depth
missing Depth -> Depth -> Bool
forall a. Eq a => a -> a -> Bool
== Depth
0 = Set Depth
s
      | Bool
otherwise =
          if Depth -> Set Depth -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Depth
missing Set Depth
s
            then Depth -> Set Depth -> Set Depth
forall a. Ord a => a -> Set a -> Set a
Set.insert Depth
missing Set Depth
s
            else Depth -> Set Depth
forall a. a -> Set a
Set.singleton Depth
n
      where
        missing :: Depth
missing = Depth
n Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
- Set Depth -> Depth
forall a. Num a => Set 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 ([Coin] -> [Coin]) -> Gen [Coin] -> Gen [Coin]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen [Coin]
forall a. Arbitrary a => Gen a
arbitrary
  where
    fixUp :: [Coin] -> [Coin]
fixUp [Coin]
s
      | Coin
missing Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Coin
Coin Integer
0 = [Coin]
s
      | Bool
otherwise = Coin
missing Coin -> [Coin] -> [Coin]
forall a. a -> [a] -> [a]
: [Coin]
s
      where
        missing :: Coin
missing = Coin
n Coin -> Coin -> Coin
forall m. Group m => m -> m -> m
~~ [Coin] -> Coin
forall m. Monoid 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 <- Set Coin -> [Coin]
forall a. Set a -> [a]
Set.toList (Set Coin -> [Coin]) -> Gen (Set Coin) -> Gen [Coin]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String] -> Depth -> Gen Coin -> Gen (Set Coin)
forall a. Ord a => [String] -> Depth -> Gen a -> Gen (Set a)
setSized [] ([Coin] -> Depth
forall a. [a] -> Depth
forall (t :: * -> *) a. Foldable t => t a -> Depth
length [Coin]
rng) Gen Coin
forall a. Arbitrary a => Gen a
arbitrary
  Map Coin Coin -> Gen (Map Coin Coin)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map Coin Coin -> Gen (Map Coin Coin))
-> Map Coin Coin -> Gen (Map Coin Coin)
forall a b. (a -> b) -> a -> b
$ [(Coin, Coin)] -> Map Coin Coin
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Coin, Coin)] -> Map Coin Coin)
-> [(Coin, Coin)] -> Map Coin Coin
forall a b. (a -> b) -> a -> b
$ [Coin] -> [Coin] -> [(Coin, Coin)]
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 = c -> Gen c
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure c
n
genFromOrdCond OrdCond
cond Bool
canBeNegative c
n =
  [String] -> Gen c -> (c -> Bool) -> Gen c
forall a. [String] -> Gen a -> (a -> Bool) -> Gen a
suchThatErr
    [String
"genFromOrdCond " String -> ShowS
forall a. [a] -> [a] -> [a]
++ OrdCond -> String
forall a. Show a => a -> String
show OrdCond
cond String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ c -> String
forall a. Show a => a -> String
show c
n]
    ( [(Depth, Gen c)] -> Gen c
forall a. HasCallStack => [(Depth, Gen a)] -> Gen a
frequency ([(Depth, Gen c)] -> Gen c) -> [(Depth, Gen c)] -> Gen c
forall a b. (a -> b) -> a -> b
$
        [(Depth
1, c -> Gen c
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (c -> Gen c) -> c -> Gen c
forall a b. (a -> b) -> a -> b
$ [String] -> c -> c -> c
forall x. Adds x => [String] -> x -> x -> x
minus [String
"genFromOrdCond"] c
n ([String] -> Depth -> c
forall x. Adds x => [String] -> Depth -> x
fromI [] Depth
1)) | OrdCond -> c -> c -> Bool
forall x. Adds x => OrdCond -> x -> x -> Bool
runOrdCondition OrdCond
GTH c
n c
forall x. Adds x => x
zero Bool -> Bool -> Bool
|| Bool
canBeNegative]
          [(Depth, Gen c)] -> [(Depth, Gen c)] -> [(Depth, Gen c)]
forall a. [a] -> [a] -> [a]
++ [ (Depth
1, c -> Gen c
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure c
n)
             , (Depth
1, c -> Gen c
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (c -> Gen c) -> c -> Gen c
forall a b. (a -> b) -> a -> b
$ c -> c -> c
forall x. Adds x => x -> x -> x
add c
n ([String] -> Depth -> c
forall x. Adds x => [String] -> Depth -> x
fromI [] Depth
1))
             , (Depth
10, Gen c
forall a. Arbitrary a => Gen a
arbitrary)
             ]
    )
    ((c -> c -> Bool) -> c -> c -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (OrdCond -> c -> c -> Bool
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 =
  [(Depth, Gen (Pred era, GenEnv era))] -> Gen (Pred era, GenEnv era)
forall a. HasCallStack => [(Depth, Gen a)] -> Gen a
frequency ([(Depth, Gen (Pred era, GenEnv era))]
 -> Gen (Pred era, GenEnv era))
-> [(Depth, Gen (Pred era, GenEnv era))]
-> Gen (Pred era, GenEnv era)
forall a b. (a -> b) -> a -> b
$
    [(Depth
1, Gen (Pred era, GenEnv era)
fixedSizedC)]
      [(Depth, Gen (Pred era, GenEnv era))]
-> [(Depth, Gen (Pred era, GenEnv era))]
-> [(Depth, Gen (Pred era, GenEnv era))]
forall a. [a] -> [a] -> [a]
++ [(Depth
1, Gen (Pred era, GenEnv era)
varSizedC)]
      [(Depth, Gen (Pred era, GenEnv era))]
-> [(Depth, Gen (Pred era, GenEnv era))]
-> [(Depth, Gen (Pred era, GenEnv era))]
forall a. [a] -> [a] -> [a]
++ [(Depth
1, Gen (Pred era, GenEnv era)
eqC)]
      [(Depth, Gen (Pred era, GenEnv era))]
-> [(Depth, Gen (Pred era, GenEnv era))]
-> [(Depth, Gen (Pred era, GenEnv era))]
forall a. [a] -> [a] -> [a]
++ [(Depth
1, Gen (Pred era, GenEnv era)
subsetC)]
      [(Depth, Gen (Pred era, GenEnv era))]
-> [(Depth, Gen (Pred era, GenEnv era))]
-> [(Depth, Gen (Pred era, GenEnv era))]
forall a. [a] -> [a] -> [a]
++ [(Depth
1, Gen (Pred era, GenEnv era)
disjointC)]
      [(Depth, Gen (Pred era, GenEnv era))]
-> [(Depth, Gen (Pred era, GenEnv era))]
-> [(Depth, Gen (Pred era, GenEnv era))]
forall a. [a] -> [a] -> [a]
++ [(Depth
1, Gen (Pred era, GenEnv era)
sumsToC)]
      [(Depth, Gen (Pred era, GenEnv era))]
-> [(Depth, Gen (Pred era, GenEnv era))]
-> [(Depth, Gen (Pred era, GenEnv era))]
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 Typed t -> Either [String] t
forall x. Typed x -> Either [String] x
runTyped (Typed t -> Either [String] t) -> Typed t -> Either [String] t
forall a b. (a -> b) -> a -> b
$ Env era -> Term era t -> Typed t
forall era t. Env era -> Term era t -> Typed t
runTerm (GenEnv era -> Env era
forall era. GenEnv era -> Env era
gEnv GenEnv era
env') Term era t
tm of
        Left [String]
errs -> (Pred era, GenEnv era) -> Gen (Pred era, GenEnv era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([String] -> Pred era
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 = (Gen (Pred era, GenEnv era)
 -> ((Pred era, GenEnv era) -> Bool) -> Gen (Pred era, GenEnv era))
-> ((Pred era, GenEnv era) -> Bool)
-> Gen (Pred era, GenEnv era)
-> Gen (Pred era, GenEnv era)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Gen (Pred era, GenEnv era)
-> ((Pred era, GenEnv era) -> Bool) -> Gen (Pred era, GenEnv era)
forall a. Gen a -> (a -> Bool) -> Gen a
suchThat (Pred era, GenEnv era) -> Bool
forall {era} {b}. (Pred era, b) -> Bool
goodSized (Gen (Pred era, GenEnv era) -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era) -> Gen (Pred era, GenEnv era)
forall a b. (a -> b) -> a -> b
$ do
      TypeInEra Rep era t
rep <- Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genValType
      Gen (Term era (Set t), GenEnv era)
-> (Term era (Set t)
    -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 (GenEnv era
-> Rep era (Set t) -> VarSpec -> Gen (Term era (Set t), GenEnv era)
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 era (Set t)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep) (Depth -> VarSpec
VarTerm Depth
1)) ((Term era (Set t)
  -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
 -> Gen (Pred era, GenEnv era))
-> (Term era (Set t)
    -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
forall a b. (a -> b) -> a -> b
$ \Term era (Set t)
set Set t
val GenEnv era
env' ->
        let n :: Term era Size
n = Depth -> Term era Size
forall era. Era era => Depth -> Term era Size
ExactSize (Set t -> Depth
forall t. Sizeable t => t -> Depth
getSize Set t
val)
         in (Pred era, GenEnv era) -> Gen (Pred era, GenEnv era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term era Size -> Term era (Set t) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized Term era Size
n Term era (Set t)
set, HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved (Term era (Set t) -> HashSet (Name era)
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 <- Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genValType
      Gen (Term era (Set t), GenEnv era)
-> (Term era (Set t)
    -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 (GenEnv era
-> Rep era (Set t) -> VarSpec -> Gen (Term era (Set t), GenEnv era)
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 era (Set t)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep) VarSpec
KnownTerm) ((Term era (Set t)
  -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
 -> Gen (Pred era, GenEnv era))
-> (Term era (Set t)
    -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
forall a b. (a -> b) -> a -> b
$ \Term era (Set t)
set Set t
val GenEnv era
env' -> do
        String
name <- GenEnv era -> Gen String
forall era. GenEnv era -> Gen String
genFreshVarName GenEnv era
env'
        let vvar :: V era Size
vvar = String -> Rep era Size -> Access era Any Size -> V era Size
forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
name Rep era Size
forall era. Rep era Size
SizeR Access era Any Size
forall era s t. Access era s t
No
            intn :: Depth
intn = Set t -> Depth
forall t. Sizeable t => t -> Depth
getSize Set t
val
        (Pred era, GenEnv era) -> Gen (Pred era, GenEnv era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term era Size -> Term era (Set t) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (V era Size -> Term era Size
forall era t. V era t -> Term era t
Var V era Size
vvar) Term era (Set t)
set, V era Size -> Size -> Depth -> GenEnv era -> GenEnv era
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 Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+ GenEnv era -> Term era (Set t) -> Depth
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 <- Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genType
      Gen (Term era t, GenEnv era)
-> (Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 (GenEnv era -> Rep era t -> VarSpec -> Gen (Term era t, GenEnv era)
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) ((Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era))
 -> Gen (Pred era, GenEnv era))
-> (Term era t -> t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
forall a b. (a -> b) -> a -> b
$ \Term era t
lhs t
val GenEnv era
env' -> do
        let d :: Depth
d = Depth
1 Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+ GenEnv era -> Term era t -> Depth
forall era t. GenEnv era -> Term era t -> Depth
depthOf GenEnv era
env' Term era t
lhs
        (Term era t
rhs, GenEnv era
env'') <- GenEnv era
-> Rep era t
-> (t -> Bool)
-> Gen t
-> VarSpec
-> Gen (Term era t, GenEnv era)
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 -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
val) (t -> Gen t
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
val) (Depth -> VarSpec
VarTerm Depth
d)
        (Pred era, GenEnv era) -> Gen (Pred era, GenEnv era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term era t
lhs Term era t -> Term era t -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era t
rhs, HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved (Term era t -> HashSet (Name era)
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 (GenEnv era -> OrderInfo
forall era. GenEnv era -> OrderInfo
gOrder GenEnv era
env) = do
          -- Known superset
          TypeInEra Rep era t
rep <- Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genValType
          Gen (Term era (Set t), GenEnv era)
-> (Term era (Set t)
    -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 (GenEnv era
-> Rep era (Set t) -> VarSpec -> Gen (Term era (Set t), GenEnv era)
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 era (Set t)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep) VarSpec
KnownTerm) ((Term era (Set t)
  -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
 -> Gen (Pred era, GenEnv era))
-> (Term era (Set t)
    -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+ GenEnv era -> Term era (Set t) -> Depth
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'') <-
              GenEnv era
-> Rep era (Set t)
-> (Set t -> Bool)
-> Gen (Set t)
-> VarSpec
-> Gen (Term era (Set t), GenEnv era)
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 era (Set t)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep)
                (Set t -> Set t -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set t
val)
                ([String] -> Set t -> Gen (Set t)
forall a. Ord a => [String] -> Set a -> Gen (Set a)
subsetFromSet [String
"From genPredicate subsetC"] Set t
val)
                (Depth -> VarSpec
VarTerm Depth
d)
            (Pred era, GenEnv era) -> Gen (Pred era, GenEnv era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term era (Set t)
sub Term era (Set t) -> Term era (Set t) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` Term era (Set t)
sup, HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved (Term era (Set t) -> HashSet (Name era)
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 <- Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genValType
          Gen (Term era (Set t), GenEnv era)
-> (Term era (Set t)
    -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 (GenEnv era
-> Rep era (Set t) -> VarSpec -> Gen (Term era (Set t), GenEnv era)
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 era (Set t)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep) VarSpec
KnownTerm) ((Term era (Set t)
  -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
 -> Gen (Pred era, GenEnv era))
-> (Term era (Set t)
    -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+ GenEnv era -> Term era (Set t) -> Depth
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'') <-
              GenEnv era
-> Rep era (Set t)
-> (Set t -> Bool)
-> Gen (Set t)
-> VarSpec
-> Gen (Term era (Set t), GenEnv era)
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 era (Set t)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep)
                (Set t -> Set t -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set t
val)
                (Set t -> Set t -> Set t
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set t
val (Set t -> Set t) -> Gen (Set t) -> Gen (Set t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rep era (Set t) -> Gen (Set t)
forall era b. Rep era b -> Gen b
genRep (Rep era t -> Rep era (Set t)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep))
                (Depth -> VarSpec
VarTerm Depth
d)
            (Pred era, GenEnv era) -> Gen (Pred era, GenEnv era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term era (Set t)
sub Term era (Set t) -> Term era (Set t) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` Term era (Set t)
sup, HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved (Term era (Set t) -> HashSet (Name era)
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 <- Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genValType
      Gen (Term era (Set t), GenEnv era)
-> (Term era (Set t)
    -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 (GenEnv era
-> Rep era (Set t) -> VarSpec -> Gen (Term era (Set t), GenEnv era)
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 era (Set t)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep) VarSpec
KnownTerm) ((Term era (Set t)
  -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
 -> Gen (Pred era, GenEnv era))
-> (Term era (Set t)
    -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+ GenEnv era -> Term era (Set t) -> Depth
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'') <-
          GenEnv era
-> Rep era (Set t)
-> (Set t -> Bool)
-> Gen (Set t)
-> VarSpec
-> Gen (Term era (Set t), GenEnv era)
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 era (Set t)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep)
            (Set t -> Set t -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set t
val)
            ((Set t -> Set t -> Set t
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set t
val) (Set t -> Set t) -> Gen (Set t) -> Gen (Set t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rep era (Set t) -> Gen (Set t)
forall era b. Rep era b -> Gen b
genRep (Rep era t -> Rep era (Set t)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
rep))
            (Depth -> VarSpec
VarTerm Depth
d)
        (Pred era, GenEnv era) -> Gen (Pred era, GenEnv era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term era (Set t) -> Term era (Set t) -> Pred era
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, HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved (Term era (Set t) -> HashSet (Name era)
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 (GenEnv era -> OrderInfo
forall era. GenEnv era -> OrderInfo
gOrder GenEnv era
env) =
          -- Known sum
          Gen (Term era Coin, GenEnv era)
-> (Term era Coin
    -> Coin -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 (GenEnv era
-> Rep era Coin
-> (Coin -> Bool)
-> Gen Coin
-> VarSpec
-> Gen (Term era Coin, GenEnv era)
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 Coin
forall era. Rep era Coin
CoinR (Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
> Integer -> Coin
Coin Integer
10) ((Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> Integer -> Coin
Coin Integer
10) (Coin -> Coin) -> Gen Coin -> Gen Coin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Coin
forall a. Arbitrary a => Gen a
arbitrary) VarSpec
KnownTerm) ((Term era Coin
  -> Coin -> GenEnv era -> Gen (Pred era, GenEnv era))
 -> Gen (Pred era, GenEnv era))
-> (Term era Coin
    -> Coin -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
forall a b. (a -> b) -> a -> b
$ \Term era Coin
sumTm Coin
val GenEnv era
env' -> do
            let d :: Depth
d = Depth
1 Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+ GenEnv era -> Term era Coin -> Depth
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 = ([Sum era Coin], GenEnv era) -> Gen ([Sum era Coin], GenEnv era)
forall a. a -> Gen a
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) <-
                    GenEnv era
-> Rep era (Map Coin Coin)
-> (Map Coin Coin -> Bool)
-> Gen (Map Coin Coin)
-> VarSpec
-> Gen (Term era (Map Coin Coin), GenEnv era)
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
                      (Rep era Coin -> Rep era Coin -> Rep era (Map Coin Coin)
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era Coin
forall era. Rep era Coin
CoinR Rep era Coin
forall era. Rep era Coin
CoinR)
                      ((Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
== Coin
n) (Coin -> Bool) -> (Map Coin Coin -> Coin) -> Map Coin Coin -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Coin Coin -> Coin
forall m. Monoid m => Map Coin m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold)
                      (Coin -> Gen (Map Coin Coin)
mapWithSum Coin
n)
                      (Depth -> VarSpec
VarTerm Depth
d)
                  ([Sum era Coin] -> [Sum era Coin])
-> ([Sum era Coin], GenEnv era) -> ([Sum era Coin], GenEnv era)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (Term era (Map Coin Coin) -> Sum era Coin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map Coin Coin)
t Sum era Coin -> [Sum era Coin] -> [Sum era Coin]
forall a. a -> [a] -> [a]
:) (([Sum era Coin], GenEnv era) -> ([Sum era Coin], GenEnv era))
-> Gen ([Sum era Coin], GenEnv era)
-> Gen ([Sum era Coin], GenEnv era)
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 <- Coin -> [String] -> Depth -> Coin -> Gen [Coin]
forall x. Adds x => x -> [String] -> Depth -> x -> Gen [x]
partition ([String] -> Depth -> Coin
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
            (Pred era, GenEnv era) -> Gen (Pred era, GenEnv era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
              ( Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. a -> Either a b
Left ([String] -> Depth -> Coin
forall x. Adds x => [String] -> Depth -> x
fromI [] Depth
small)) Term era Coin
sumTm OrdCond
EQL [Sum era Coin]
parts
              , HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved ((Sum era Coin -> HashSet (Name era))
-> [Sum era Coin] -> HashSet (Name era)
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (HashSet (Name era) -> Sum era Coin -> HashSet (Name era)
forall era r. HashSet (Name era) -> Sum era r -> HashSet (Name era)
varsOfSum HashSet (Name era)
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 =
          [Gen (Pred era, GenEnv era)] -> Gen (Pred era, GenEnv era)
forall a. HasCallStack => [Gen a] -> Gen a
oneof
            [ Rep era Coin -> Bool -> Gen (Pred era, GenEnv era)
forall c.
(Adds c, Arbitrary c) =>
Rep era c -> Bool -> Gen (Pred era, GenEnv era)
sumCKnownSets Rep era Coin
forall era. Rep era Coin
CoinR Bool
False
            , Rep era DeltaCoin -> Bool -> Gen (Pred era, GenEnv era)
forall c.
(Adds c, Arbitrary c) =>
Rep era c -> Bool -> Gen (Pred era, GenEnv era)
sumCKnownSets Rep era DeltaCoin
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) =
      [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
        [ HashSet (Name era) -> HashSet (Name era) -> Bool
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 <- [HashSet (Name era)] -> [[HashSet (Name era)]]
forall a. [a] -> [[a]]
List.tails ([HashSet (Name era)] -> [[HashSet (Name era)]])
-> [HashSet (Name era)] -> [[HashSet (Name era)]]
forall a b. (a -> b) -> a -> b
$ (Sum era c -> HashSet (Name era))
-> [Sum era c] -> [HashSet (Name era)]
forall a b. (a -> b) -> [a] -> [b]
map (HashSet (Name era) -> Sum era c -> HashSet (Name era)
forall era r. HashSet (Name era) -> Sum era r -> HashSet (Name era)
varsOfSum HashSet (Name era)
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 = (Gen (Pred era, GenEnv era)
 -> ((Pred era, GenEnv era) -> Bool) -> Gen (Pred era, GenEnv era))
-> ((Pred era, GenEnv era) -> Bool)
-> Gen (Pred era, GenEnv era)
-> Gen (Pred era, GenEnv era)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Gen (Pred era, GenEnv era)
-> ((Pred era, GenEnv era) -> Bool) -> Gen (Pred era, GenEnv era)
forall a. Gen a -> (a -> Bool) -> Gen a
suchThat (Pred era -> Bool
forall {era}. Pred era -> Bool
uniqueVars (Pred era -> Bool)
-> ((Pred era, GenEnv era) -> Pred era)
-> (Pred era, GenEnv era)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pred era, GenEnv era) -> Pred era
forall a b. (a, b) -> a
fst) (Gen (Pred era, GenEnv era) -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era) -> Gen (Pred era, GenEnv era)
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 [] c
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 <- Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genKeyType
            Gen (Term era (Map t c), GenEnv era)
-> (Term era (Map t c)
    -> Map t c -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 (GenEnv era
-> Rep era (Map t c)
-> VarSpec
-> Gen (Term era (Map t c), GenEnv era)
forall era t.
Era era =>
GenEnv era -> Rep era t -> VarSpec -> Gen (Term era t, GenEnv era)
genTerm GenEnv era
env0 (Rep era t -> Rep era c -> Rep era (Map t c)
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) ((Term era (Map t c)
  -> Map t c -> GenEnv era -> Gen (Pred era, GenEnv era))
 -> Gen (Pred era, GenEnv era))
-> (Term era (Map t c)
    -> Map t c -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
- Depth
1) GenEnv era
env1 (([Sum era c] -> c -> GenEnv era -> Gen (Pred era, GenEnv era))
 -> Gen (Pred era, GenEnv era))
-> ([Sum era c] -> c -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 (Term era (Map t c) -> Sum era c
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map t c)
expr Sum era c -> [Sum era c] -> [Sum era c]
forall a. a -> [a] -> [a]
: [Sum era c]
parts) (c -> c -> c
forall x. Adds x => x -> x -> x
add (Map t c -> c
forall (t :: * -> *) c. (Foldable t, Adds c) => t c -> c
sumAdds Map t c
val) c
tot)
      Depth
count <- (Depth, Depth) -> Gen Depth
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 (([Sum era c] -> c -> GenEnv era -> Gen (Pred era, GenEnv era))
 -> Gen (Pred era, GenEnv era))
-> ([Sum era c] -> c -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
forall a b. (a -> b) -> a -> b
$ \[Sum era c]
parts c
tot GenEnv era
env' -> do
        OrdCond
cmp <- [OrdCond] -> Gen OrdCond
forall a. HasCallStack => [a] -> Gen a
elements ([OrdCond] -> Gen OrdCond) -> [OrdCond] -> Gen OrdCond
forall a b. (a -> b) -> a -> b
$ [OrdCond
EQL, OrdCond
LTE, OrdCond
GTH, OrdCond
GTE] [OrdCond] -> [OrdCond] -> [OrdCond]
forall a. [a] -> [a] -> [a]
++ [OrdCond
LTH | Bool
canBeNegative] -- TODO/negativeCoin
        let d :: Depth
d = Depth
1 Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+ [Depth] -> Depth
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Depth
0 Depth -> [Depth] -> [Depth]
forall a. a -> [a] -> [a]
: (Sum era c -> Depth) -> [Sum era c] -> [Depth]
forall a b. (a -> b) -> [a] -> [b]
map (GenEnv era -> Sum era c -> Depth
forall era c. GenEnv era -> Sum era c -> Depth
depthOfSum GenEnv era
env') [Sum era c]
parts)
        (Term era c
sumTm, GenEnv era
env'') <-
          GenEnv era
-> Rep era c
-> (c -> Bool)
-> Gen c
-> VarSpec
-> Gen (Term era c, GenEnv era)
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
            ((c -> c -> Bool) -> c -> c -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (OrdCond -> c -> c -> Bool
forall x. Adds x => OrdCond -> x -> x -> Bool
runOrdCondition OrdCond
cmp) c
tot)
            (OrdCond -> Bool -> c -> Gen c
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
        (Pred era, GenEnv era) -> Gen (Pred era, GenEnv era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (c -> Direct c
forall a b. b -> Either a b
Right ([String] -> Depth -> c
forall x. Adds x => [String] -> Depth -> x
fromI [] Depth
small)) Term era c
sumTm OrdCond
cmp [Sum era c]
parts, HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
forall era. HashSet (Name era) -> Depth -> GenEnv era -> GenEnv era
markSolved (Term era c -> HashSet (Name era)
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 =
      [Gen (Pred era, GenEnv era)] -> Gen (Pred era, GenEnv era)
forall a. HasCallStack => [Gen a] -> Gen a
oneof
        [ do
            -- Known map
            TypeInEra Rep era t
krep <- Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genKeyType
            TypeInEra Rep era t
vrep <- Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genValType
            Gen (Term era (Map t t), GenEnv era)
-> (Term era (Map t t)
    -> Map t t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 (GenEnv era
-> Rep era (Map t t)
-> VarSpec
-> Gen (Term era (Map t t), GenEnv era)
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 era t -> Rep era (Map t t)
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) ((Term era (Map t t)
  -> Map t t -> GenEnv era -> Gen (Pred era, GenEnv era))
 -> Gen (Pred era, GenEnv era))
-> (Term era (Map t t)
    -> Map t t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+ GenEnv era -> Term era (Map t t) -> Depth
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'') <-
                GenEnv era
-> Rep era (Set t)
-> (Set t -> Bool)
-> Gen (Set t)
-> VarSpec
-> Gen (Term era (Set t), GenEnv era)
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 era (Set t)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
krep)
                  (Set t -> Set t -> Bool
forall a. Eq a => a -> a -> Bool
== Map t t -> Set t
forall k a. Map k a -> Set k
Map.keysSet Map t t
val)
                  (Set t -> Gen (Set t)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set t -> Gen (Set t)) -> Set t -> Gen (Set t)
forall a b. (a -> b) -> a -> b
$ Map t t -> Set t
forall k a. Map k a -> Set k
Map.keysSet Map t t
val)
                  (Depth -> VarSpec
VarTerm Depth
d)
              (Pred era, GenEnv era) -> Gen (Pred era, GenEnv era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term era (Map t t) -> Term era (Set t)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map t t)
mapTm Term era (Set t) -> Term era (Set t) -> Pred era
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 <- Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genKeyType
            TypeInEra Rep era t
vrep <- Gen (TypeInEra era)
forall era. Gen (TypeInEra era)
genValType
            Gen (Term era (Set t), GenEnv era)
-> (Term era (Set t)
    -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 (GenEnv era
-> Rep era (Set t) -> VarSpec -> Gen (Term era (Set t), GenEnv era)
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 era (Set t)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era t
krep) VarSpec
KnownTerm) ((Term era (Set t)
  -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
 -> Gen (Pred era, GenEnv era))
-> (Term era (Set t)
    -> Set t -> GenEnv era -> Gen (Pred era, GenEnv era))
-> Gen (Pred era, GenEnv era)
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 Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+ GenEnv era -> Term era (Set t) -> Depth
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'') <-
                GenEnv era
-> Rep era (Map t t)
-> (Map t t -> Bool)
-> Gen (Map t t)
-> VarSpec
-> Gen (Term era (Map t t), GenEnv era)
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 era t -> Rep era (Map t t)
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 Set t -> Set t -> Bool
forall a. Eq a => a -> a -> Bool
==) (Set t -> Bool) -> (Map t t -> Set t) -> Map t t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map t t -> Set t
forall k a. Map k a -> Set k
Map.keysSet)
                  (GenEnv era -> Rep era t -> Set t -> Gen (Map t t)
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)
              (Pred era, GenEnv era) -> Gen (Pred era, GenEnv era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term era (Set t)
domTm Term era (Set t) -> Term era (Set t) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map t t) -> Term era (Set t)
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 <- (Depth, Depth) -> Gen Depth
forall a. Random a => (a, a) -> Gen a
choose (Depth
1, Depth
40)
  Depth -> GenEnv era -> Gen ([Pred era], GenEnv era)
forall {era} {t}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 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 t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0 = ([Pred era], GenEnv era) -> Gen ([Pred era], GenEnv era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], GenEnv era
env)
      | Bool
otherwise = do
          (Pred era
pr, GenEnv era
env') <- GenEnv era -> Gen (Pred era, GenEnv era)
forall era. Era era => GenEnv era -> Gen (Pred era, GenEnv era)
genPredicate GenEnv era
env
          ([Pred era] -> [Pred era])
-> ([Pred era], GenEnv era) -> ([Pred era], GenEnv era)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (Pred era
pr Pred era -> [Pred era] -> [Pred era]
forall a. a -> [a] -> [a]
:) (([Pred era], GenEnv era) -> ([Pred era], GenEnv era))
-> Gen ([Pred era], GenEnv era) -> Gen ([Pred era], GenEnv era)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> GenEnv era -> Gen ([Pred era], GenEnv era)
loop (t
n t -> t -> t
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 = Rep era a -> (Eq a => a) -> Maybe a
forall era t a. Rep era t -> (Eq t => a) -> Maybe a
withEq Rep era a
r a
Eq t => a
Eq a => a
cont
withEq (MapR Rep era a
kr Rep era b
vr) Eq t => a
cont = Maybe (Maybe a) -> Maybe a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe a) -> Maybe a) -> Maybe (Maybe a) -> Maybe a
forall a b. (a -> b) -> a -> b
$ Rep era a -> (Eq a => Maybe a) -> Maybe (Maybe a)
forall era t a. Rep era t -> (Eq t => a) -> Maybe a
withEq Rep era a
kr (Rep era b -> (Eq b => a) -> Maybe a
forall era t a. Rep era t -> (Eq t => a) -> Maybe a
withEq Rep era b
vr a
Eq t => a
Eq b => a
cont)
withEq Rep era t
CoinR Eq t => a
cont = a -> Maybe a
forall a. a -> Maybe a
Just a
Eq t => a
cont
withEq Rep era t
_ Eq t => a
_ = Maybe 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' <- (Pred era -> [Pred era]) -> [Pred era] -> [[Pred era]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList Pred era -> [Pred era]
shrinkPred [Pred era]
preds
  , let defined :: HashSet (Name era)
defined = (Pred era -> HashSet (Name era))
-> [Pred era] -> HashSet (Name era)
forall m a. Monoid m => (a -> m) -> [a] -> m
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 = pruneEnv defined (gEnv env)}
  , HashSet (Name era) -> [Pred era] -> Bool
depCheck HashSet (Name era)
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 = (Pred era -> Bool) -> [Pred era] -> [Pred era]
forall a. (a -> Bool) -> [a] -> [a]
filter (Pred era -> Pred era -> Bool
checkDefs Pred era
c) ([Pred era] -> [Pred era]) -> [Pred era] -> [Pred era]
forall a b. (a -> b) -> a -> b
$ Pred era -> [Pred era]
shrinkToValue Pred era
c [Pred era] -> [Pred era] -> [Pred era]
forall a. [a] -> [a] -> [a]
++ Pred era -> [Pred era]
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 HashSet (Name era) -> HashSet (Name era) -> Bool
forall a. Eq a => a -> a -> Bool
== Pred era -> HashSet (Name era)
def Pred era
shrunk Bool -> Bool -> Bool
&& Bool -> Bool
not (HashSet (Name era) -> Bool
forall a. HashSet a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (HashSet (Name era) -> Bool) -> HashSet (Name era) -> Bool
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
_) <- HashSet (Name era) -> [Name era]
forall a. HashSet a -> [a]
HashSet.toList (HashSet (Name era) -> [Name era])
-> HashSet (Name era) -> [Name era]
forall a b. (a -> b) -> a -> b
$ Pred era -> HashSet (Name era)
def Pred era
c
      , Right t
v <- [Typed t -> Either [String] t
forall x. Typed x -> Either [String] x
runTyped (Typed t -> Either [String] t) -> Typed t -> Either [String] t
forall a b. (a -> b) -> a -> b
$ Env era -> Term era t -> Typed t
forall era t. Env era -> Term era t -> Typed t
runTerm (GenEnv era -> Env era
forall era. GenEnv era -> Env era
gEnv GenEnv era
env) (V era t -> Term era t
forall era t. V era t -> Term era t
Var V era t
x)]
      , Just Pred era
c' <- [Rep era t -> (Eq t => Pred era) -> Maybe (Pred era)
forall era t a. Rep era t -> (Eq t => a) -> Maybe a
withEq Rep era t
r ((Eq t => Pred era) -> Maybe (Pred era))
-> (Eq t => Pred era) -> Maybe (Pred era)
forall a b. (a -> b) -> a -> b
$ Rep era t -> t -> Term era t
forall era t. Rep era t -> t -> Term era t
Lit Rep era t
r t
v Term era t -> Term era t -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: V era t -> Term era t
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 {}) <- Pred era -> [Pred era]
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) = [Term era Size -> Pred era
forall era t. Term era t -> Pred era
Random Term era Size
n, Term era t -> Pred era
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) = [Term era (Set a) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Set a)
s, Term era (Set a) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Set a)
t]
    randoms (Term era a
s :=: Term era a
t) = [Term era a -> Pred era
forall era t. Term era t -> Pred era
Random Term era a
s, Term era a -> Pred era
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) = [Term era (Set a) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Set a)
s, Term era (Set a) -> Pred era
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) = Map String (Payload era) -> Env era
forall era. Map String (Payload era) -> Env era
Env (Map String (Payload era) -> Env era)
-> Map String (Payload era) -> Env era
forall a b. (a -> b) -> a -> b
$ (String -> Payload era -> Bool)
-> Map String (Payload era) -> Map String (Payload era)
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\String
name Payload era
_ -> String -> HashSet String -> Bool
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 = (Name era -> String) -> HashSet (Name era) -> HashSet String
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'
      | [Pred era] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pred era]
rdy = Bool
False
      | Bool
otherwise = HashSet (Name era) -> [Pred era] -> Bool
depCheck ((Pred era -> HashSet (Name era))
-> [Pred era] -> HashSet (Name era)
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Pred era -> HashSet (Name era)
def [Pred era]
rdy HashSet (Name era) -> HashSet (Name era) -> HashSet (Name era)
forall a. Semigroup a => a -> a -> a
<> HashSet (Name era)
solved) [Pred era]
rest
      where
        ([Pred era]
rdy, [Pred era]
rest) = (Pred era -> Bool) -> [Pred era] -> ([Pred era], [Pred era])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition Pred era -> Bool
canSolve [Pred era]
preds'
        canSolve :: Pred era -> Bool
canSolve Pred era
c = HashSet (Name era) -> HashSet (Name era) -> Bool
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 = OrderInfo
-> Map (Name era) (HashSet (Name era))
-> Pred era
-> Map (Name era) (HashSet (Name era))
forall era.
Era era =>
OrderInfo
-> Map (Name era) (HashSet (Name era))
-> Pred era
-> Map (Name era) (HashSet (Name era))
accumdep (GenEnv era -> OrderInfo
forall era. GenEnv era -> OrderInfo
gOrder GenEnv era
env) Map (Name era) (HashSet (Name era))
forall a. Monoid a => a
mempty Pred era
c
    def :: Pred era -> HashSet (Name era)
def Pred era
x = ([Name era] -> HashSet (Name era)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.fromList ([Name era] -> HashSet (Name era))
-> (Pred era -> [Name era]) -> Pred era -> HashSet (Name era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Name era) -> [Name era]
forall a. Set a -> [a]
Set.toList (Set (Name era) -> [Name era])
-> (Pred era -> Set (Name era)) -> Pred era -> [Name era]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Name era) (HashSet (Name era)) -> Set (Name era)
forall k a. Map k a -> Set k
Map.keysSet (Map (Name era) (HashSet (Name era)) -> Set (Name era))
-> (Pred era -> Map (Name era) (HashSet (Name era)))
-> Pred era
-> Set (Name era)
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 = Map (Name era) (HashSet (Name era)) -> HashSet (Name era)
forall m. Monoid m => Map (Name era) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Map (Name era) (HashSet (Name era)) -> HashSet (Name era))
-> (Pred era -> Map (Name era) (HashSet (Name era)))
-> Pred era
-> HashSet (Name era)
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 = Map String (Payload ShelleyEra) -> Env ShelleyEra
forall era. Map String (Payload era) -> Env era
Env (Map String (Payload ShelleyEra) -> Env ShelleyEra)
-> Map String (Payload ShelleyEra) -> Env ShelleyEra
forall a b. (a -> b) -> a -> b
$ [(String, Payload ShelleyEra)] -> Map String (Payload ShelleyEra)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(String
"A", Rep ShelleyEra Coin
-> Coin -> Access ShelleyEra Any Coin -> Payload ShelleyEra
forall era t s. Rep era t -> t -> Access era s t -> Payload era
Payload Rep ShelleyEra Coin
forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
5) Access ShelleyEra Any Coin
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
_ = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines [String]
errs) Bool
False
ensureRight (Right a
x) a -> prop
prop = prop -> Property
forall prop. Testable prop => prop -> Property
property (prop -> Property) -> prop -> 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 Bool -> Bool -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> Bool
False
ifRight (Right a
x) a -> prop
prop = prop -> Property
forall prop. Testable prop => prop -> Property
property (prop -> Property) -> prop -> 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 = Either [String] a -> (a -> prop) -> Property
forall prop a.
Testable prop =>
Either [String] a -> (a -> prop) -> Property
ensureRight (Either [String] a -> (a -> prop) -> Property)
-> (Typed a -> Either [String] a)
-> Typed a
-> (a -> prop)
-> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Typed a -> Either [String] a
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 = Either [String] a -> (a -> prop) -> Property
forall prop a.
Testable prop =>
Either [String] a -> (a -> prop) -> Property
ifRight (Either [String] a -> (a -> prop) -> Property)
-> (Typed a -> Either [String] a)
-> Typed a
-> (a -> prop)
-> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Typed a -> Either [String] a
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 = Env ShelleyEra
forall era. Env era
emptyEnv
    , gSolved :: Map (Name ShelleyEra) Depth
gSolved = Map (Name ShelleyEra) Depth
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
"{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Rep era a -> a -> String
forall era t. Rep era t -> t -> String
synopsis Rep era a
r) (Set a -> [a]
forall a. Set a -> [a]
Set.toList t
Set a
t)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
showVal (MapR Rep era a
kr Rep era b
vr) t
t =
  String
"{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [Rep era a -> a -> String
forall era t. Rep era t -> t -> String
synopsis Rep era a
kr a
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rep era b -> b -> String
forall era t. Rep era t -> t -> String
synopsis Rep era b
vr b
v | (a
k, b
v) <- Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
Map.toList t
Map a b
t] String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
showVal Rep era t
rep t
t = Rep era t -> t -> String
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) = Rep era t -> t -> String
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 " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term era (Map a b) -> String
forall era t. Term era t -> String
showTerm Term era (Map a b)
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
showTerm (Rng Term era (Map a b)
t) = String
"(Rng " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term era (Map a b) -> String
forall era t. Term era t -> String
showTerm Term era (Map a b)
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
showTerm Term era t
t = Term era t -> String
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) = Term era (Set a) -> String
forall era t. Term era t -> String
showTerm Term era (Set a)
sub String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ⊆ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term era (Set a) -> String
forall era t. Term era t -> String
showTerm Term era (Set a)
sup
showPred (Term era a
sub :=: Term era a
sup) = Term era a -> String
forall era t. Term era t -> String
showTerm Term era a
sub String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" == " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term era a -> String
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 " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term era (Set a) -> String
forall era t. Term era t -> String
showTerm Term era (Set a)
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term era (Set a) -> String
forall era t. Term era t -> String
showTerm Term era (Set a)
t
showPred Pred era
pr = Pred era -> String
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 ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((String, Payload era) -> String)
-> [(String, Payload era)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Payload era) -> String
forall {era}. (String, Payload era) -> String
pr (Map String (Payload era) -> [(String, Payload era)]
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rep era t -> String
forall a. Show a => a -> String
show Rep era t
rep String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rep era t -> t -> String
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 =
  Gen ([Pred ShelleyEra], GenEnv ShelleyEra)
-> (([Pred ShelleyEra], GenEnv ShelleyEra)
    -> [([Pred ShelleyEra], GenEnv ShelleyEra)])
-> (([Pred ShelleyEra], GenEnv ShelleyEra) -> Property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrink (GenEnv ShelleyEra -> Gen ([Pred ShelleyEra], GenEnv ShelleyEra)
forall era. Era era => GenEnv era -> Gen ([Pred era], GenEnv era)
genPreds (GenEnv ShelleyEra -> Gen ([Pred ShelleyEra], GenEnv ShelleyEra))
-> GenEnv ShelleyEra -> Gen ([Pred ShelleyEra], GenEnv ShelleyEra)
forall a b. (a -> b) -> a -> b
$ OrderInfo -> GenEnv ShelleyEra
initEnv OrderInfo
info) ([Pred ShelleyEra], GenEnv ShelleyEra)
-> [([Pred ShelleyEra], GenEnv ShelleyEra)]
forall era.
Era era =>
([Pred era], GenEnv era) -> [([Pred era], GenEnv era)]
shrinkPreds ((([Pred ShelleyEra], GenEnv ShelleyEra) -> Property) -> Property)
-> (([Pred ShelleyEra], GenEnv ShelleyEra) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \([Pred ShelleyEra]
preds, GenEnv ShelleyEra
genenv) ->
    String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"\n-- Order --\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ OrderInfo -> String
forall a. Show a => a -> String
show OrderInfo
info) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
      String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"\n-- Constraints --\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines ((Pred ShelleyEra -> String) -> [Pred ShelleyEra] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Pred ShelleyEra -> String
forall era. Pred era -> String
showPred [Pred ShelleyEra]
preds)) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"-- Model solution --\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env ShelleyEra -> String
forall era. Env era -> String
showEnv (GenEnv ShelleyEra -> Env ShelleyEra
forall era. GenEnv era -> Env era
gEnv GenEnv ShelleyEra
genenv)) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          Typed (DependGraph ShelleyEra)
-> (DependGraph ShelleyEra -> Property) -> Property
checkTyped (OrderInfo -> [Pred ShelleyEra] -> Typed (DependGraph ShelleyEra)
forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile OrderInfo
info [Pred ShelleyEra]
preds) ((DependGraph ShelleyEra -> Property) -> Property)
-> (DependGraph ShelleyEra -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \DependGraph ShelleyEra
graph ->
            Gen (Either [String] (Subst ShelleyEra))
-> (Either [String] (Subst ShelleyEra) -> Property) -> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind (Bool
-> Proof ShelleyEra
-> DependGraph ShelleyEra
-> Gen (Either [String] (Subst ShelleyEra))
forall era.
Bool
-> Proof era
-> DependGraph era
-> Gen (Either [String] (Subst era))
genDependGraph Bool
False Proof ShelleyEra
testProof DependGraph ShelleyEra
graph) ((Either [String] (Subst ShelleyEra) -> Property) -> Property)
-> ((Subst ShelleyEra -> Property)
    -> Either [String] (Subst ShelleyEra) -> Property)
-> (Subst ShelleyEra -> Property)
-> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either [String] (Subst ShelleyEra)
 -> (Subst ShelleyEra -> Property) -> Property)
-> (Subst ShelleyEra -> Property)
-> Either [String] (Subst ShelleyEra)
-> Property
forall a b c. (a -> b -> c) -> b -> a -> c
flip Either [String] (Subst ShelleyEra)
-> (Subst ShelleyEra -> Property) -> Property
checkRight ((Subst ShelleyEra -> Property) -> Property)
-> (Subst ShelleyEra -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Subst ShelleyEra
subst ->
              let env :: Env ShelleyEra
env = Typed (Env ShelleyEra) -> Env ShelleyEra
forall t. HasCallStack => Typed t -> t
errorTyped (Typed (Env ShelleyEra) -> Env ShelleyEra)
-> Typed (Env ShelleyEra) -> Env ShelleyEra
forall a b. (a -> b) -> a -> b
$ Subst ShelleyEra -> Env ShelleyEra -> Typed (Env ShelleyEra)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst ShelleyEra
subst Env ShelleyEra
forall era. Env era
emptyEnv
                  n :: Depth
n = let Env Map String (Payload ShelleyEra)
e = GenEnv ShelleyEra -> Env ShelleyEra
forall era. GenEnv era -> Env era
gEnv GenEnv ShelleyEra
genenv in Map String (Payload ShelleyEra) -> Depth
forall k a. Map k a -> Depth
Map.size Map String (Payload ShelleyEra)
e
               in String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Var count" [Depth -> String
forall a. Show a => a -> String
show Depth
n] (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
                    String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Constraint types" ((Pred ShelleyEra -> String) -> [Pred ShelleyEra] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Pred ShelleyEra -> String
forall era. Pred era -> String
predConstr [Pred ShelleyEra]
preds) (Property -> Property) -> Property -> Property
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 = Either [String] (DependGraph ShelleyEra)
-> (DependGraph ShelleyEra -> Property) -> Property
forall prop a.
Testable prop =>
Either [String] a -> (a -> prop) -> Property
checkWhitelist (Either [String] (DependGraph ShelleyEra)
 -> (DependGraph ShelleyEra -> Property) -> Property)
-> (Typed (DependGraph ShelleyEra)
    -> Either [String] (DependGraph ShelleyEra))
-> Typed (DependGraph ShelleyEra)
-> (DependGraph ShelleyEra -> Property)
-> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Typed (DependGraph ShelleyEra)
-> Either [String] (DependGraph ShelleyEra)
forall x. Typed x -> Either [String] x
runTyped
      | Bool
otherwise = Typed (DependGraph ShelleyEra)
-> (DependGraph ShelleyEra -> Property) -> Property
forall prop a. Testable prop => Typed a -> (a -> prop) -> Property
ifTyped
    checkRight :: Either [String] (Subst ShelleyEra)
-> (Subst ShelleyEra -> Property) -> Property
checkRight
      | Bool
strict = Either [String] (Subst ShelleyEra)
-> (Subst ShelleyEra -> Property) -> Property
forall prop a.
Testable prop =>
Either [String] a -> (a -> prop) -> Property
checkWhitelist
      | Bool
otherwise = Either [String] (Subst ShelleyEra)
-> (Subst ShelleyEra -> Property) -> Property
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
_ =
      [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
        [ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
white String
err
        | String
white <- [String]
whitelist
        , String
err <- [String]
errs
        ]
        Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample ([String] -> String
unlines [String]
errs) Bool
False
    checkWhitelist (Right a
x) a -> prop
k = prop -> Property
forall prop. Testable prop => prop -> Property
property (prop -> Property) -> prop -> 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 =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"-- Solution --\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env era -> String
forall era. Env era -> String
showEnv Env era
env) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property) -> [Property] -> Property
forall a b. (a -> b) -> a -> b
$
      (Pred era -> Property) -> [Pred era] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map Pred era -> Property
checkPred [Pred era]
preds
  where
    checkPred :: Pred era -> Property
checkPred Pred era
pr = String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Failed: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Pred era -> String
forall era. Pred era -> String
showPred Pred era
pr) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Typed Bool -> (Bool -> Bool) -> Property
forall prop a. Testable prop => Typed a -> (a -> prop) -> Property
ensureTyped (Env era -> Pred era -> Typed Bool
forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env Pred era
pr) Bool -> Bool
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 <- Either [String] (DependGraph ShelleyEra)
-> IO (Either [String] (DependGraph ShelleyEra))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [String] (DependGraph ShelleyEra)
 -> IO (Either [String] (DependGraph ShelleyEra)))
-> Either [String] (DependGraph ShelleyEra)
-> IO (Either [String] (DependGraph ShelleyEra))
forall a b. (a -> b) -> a -> b
$ Typed (DependGraph ShelleyEra)
-> Either [String] (DependGraph ShelleyEra)
forall x. Typed x -> Either [String] x
runTyped (Typed (DependGraph ShelleyEra)
 -> Either [String] (DependGraph ShelleyEra))
-> Typed (DependGraph ShelleyEra)
-> Either [String] (DependGraph ShelleyEra)
forall a b. (a -> b) -> a -> b
$ OrderInfo -> [Pred ShelleyEra] -> Typed (DependGraph ShelleyEra)
forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile OrderInfo
info [Pred ShelleyEra]
ps
  Either [String] (Subst ShelleyEra)
subst <- Gen (Either [String] (Subst ShelleyEra))
-> IO (Either [String] (Subst ShelleyEra))
forall a. Gen a -> IO a
generate (Gen (Either [String] (Subst ShelleyEra))
 -> IO (Either [String] (Subst ShelleyEra)))
-> Gen (Either [String] (Subst ShelleyEra))
-> IO (Either [String] (Subst ShelleyEra))
forall a b. (a -> b) -> a -> b
$ Bool
-> Proof ShelleyEra
-> DependGraph ShelleyEra
-> Gen (Either [String] (Subst ShelleyEra))
forall era.
Bool
-> Proof era
-> DependGraph era
-> Gen (Either [String] (Subst era))
genDependGraph Bool
True Proof ShelleyEra
testProof DependGraph ShelleyEra
g
  Either [String] (Subst ShelleyEra) -> IO ()
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 (([Pred ShelleyEra]
  -> DependGraph ShelleyEra -> Env ShelleyEra -> Property)
 -> Property)
-> ([Pred ShelleyEra]
    -> DependGraph ShelleyEra -> Env ShelleyEra -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \[Pred ShelleyEra]
preds DependGraph ShelleyEra
_graph Env ShelleyEra
env ->
    [Pred ShelleyEra] -> Env ShelleyEra -> Property
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 (([Pred ShelleyEra]
  -> DependGraph ShelleyEra -> Env ShelleyEra -> Property)
 -> Property)
-> ([Pred ShelleyEra]
    -> DependGraph ShelleyEra -> Env ShelleyEra -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \[Pred ShelleyEra]
preds DependGraph ShelleyEra
graph Env ShelleyEra
env ->
    String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"-- Original solution --\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Env ShelleyEra -> String
forall era. Env era -> String
showEnv Env ShelleyEra
env) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
      let envs :: [Env ShelleyEra]
envs = DependGraph ShelleyEra -> Env ShelleyEra -> [Env ShelleyEra]
forall era. DependGraph era -> Env era -> [Env era]
shrinkEnv DependGraph ShelleyEra
graph Env ShelleyEra
env
       in String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Shrinkings" [Depth -> String
forall a. Show a => a -> String
show (Depth -> String) -> Depth -> String
forall a b. (a -> b) -> a -> b
$ [Env ShelleyEra] -> Depth
forall a. [a] -> Depth
forall (t :: * -> *) a. Foldable t => t a -> Depth
length [Env ShelleyEra]
envs] (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
            [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property) -> [Property] -> Property
forall a b. (a -> b) -> a -> b
$
              (Env ShelleyEra -> Property) -> [Env ShelleyEra] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map ([Pred ShelleyEra] -> Env ShelleyEra -> Property
forall era. [Pred era] -> Env era -> Property
checkPredicates [Pred ShelleyEra]
preds) [Env ShelleyEra]
envs