{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- The pattern completeness checker is much weaker before ghc-9.0. Rather than introducing redundant
-- cases and turning off the overlap check in newer ghc versions we disable the check for old
-- versions.
#if __GLASGOW_HASKELL__ < 900
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
#endif

-- | This module contains most of the implementation
-- of the framework.
--
-- NOTE: This is a very big module. Splitting it up would
-- be a nice thing to do but it's not very easy. The problem
-- is that a lot of the things in here depend on each other
-- via a cycle like `Pred` depends on `Term` which depend on
-- `HasSpec` which depends on `Specification` and `Generic` and `Specification`
-- depends in turn on `Pred` and so on.
module Constrained.Base where

import Control.Applicative
import Control.Arrow (first)
import Control.Monad
import Control.Monad.Identity
import Control.Monad.Writer (Writer, runWriter, tell)
import Data.Foldable
import Data.Kind
import Data.List (intersect, isPrefixOf, isSuffixOf, nub, partition, (\\))
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Maybe
import Data.Monoid qualified as Monoid
import Data.Semigroup (Any (..), Max (..), getAll, getMax)
import Data.Semigroup qualified as Semigroup
import Data.Set (Set)
import Data.Set qualified as Set
import Data.String
import Data.Typeable
import Data.Word
import GHC.Generics
import GHC.Int
import GHC.Natural
import GHC.Real
import GHC.Stack
import GHC.TypeLits
import Prettyprinter
import System.Random
import System.Random.Stateful
import Test.QuickCheck hiding (Args, Fun, forAll)
import Test.QuickCheck.Gen
import Test.QuickCheck.Random

import Constrained.Core
import Constrained.Env
import Constrained.GenT
import Constrained.Graph hiding (dependency, irreflexiveDependencyOn, noDependencies)
import Constrained.Graph qualified as Graph
import Constrained.List
import Constrained.Univ
import Data.List.NonEmpty (NonEmpty ((:|)))
import Data.List.NonEmpty qualified as NE

{- NOTE [High level overview of generation from predicates]:

-- The overall strategy ---------------------------------------------------

The strategy for generating things from `Pred`s is relatively straightforward
and relies on one key fact: any constraint that has only one free variable `x`
and where `x` occurs only once can be turned into a `Specification` for `x`.

We say that such constraints _define_ `x` and given a set of constraints `ps`
and a variable `x` we can split `ps` into the constraints that define `x` and
any constraints that don't. We can then generate a value from `x` by computing
a spec for each defining constraint in `ps` and using the `Semigroup` structure
of `Specification`s to combine them and give them to `genFromSpecT`. Once we obtain a
value for `x` we can substitute this value in all other constraints and pick
another variable to solve.

For example, given the following constraints on integers `x` and `y`

  x < 10
  3 <= x
  y < x

we see that `x < 10` and `3 <= x` are defining constraints for `x` and there
are no definining constraints for `y`. We compute a `Specification` for `x` for each
constraint, in this case `x < 10` turns into something like `(-∞,10)` and
`3 <= x` turns into `[3, ∞)`. We combine the specs to form `[3, 10)` from which we
can generate a value, e.g. 4 (chosen by fair dice roll). We then substitute
`[x := 4]` in the remaining constraints and obtain `y < 4`, giving us a defining
constraint for `y`.

-- How to pick the variable order -----------------------------------------

At this point it should be relatively clear that the order we pick for the
variables matters a great deal. If we choose to generate `y` before `x` in our
example we will have no defining constraints for `y` and so we pick a value for
it freely. But that renders `x` unsolveable if `y > 9` - which will result in
the generator failing to generate a value (one could consider backtracking, but
that is very computationally expensive so _relying_ on it would probably not be
wise).

Computing a good choice of variable order that leaves the least room for error
is obviously undecidable and difficult and we choose instead an explicit
syntax-directed variable order. Specifically, variable dependency in terms is
_left-to-right_, meaning that the variables in `x + y < z` will be solved in
the order `z -> y -> x`. On top of that there is a constraint `dependsOn y x`
that allows you to overwrite the order of two variables. Consequently, the
following constraints will be solved in the order `z -> x -> y`:

  x + y < z
  y `dependsOn` x

A consequence of this is that it is possible to form dependency loops by
specifying multiple constraints, e.g. in:

  x < y
  y < x + 10

However, this situation can be addressed by the introduction of `dependsOn` to
settle the order.  It is worth noting that the choice of order in `dependsOn`
is important as it affects the solveability of the constraints (as we saw
above). We leave the choice of `dependsOn` in the example below as an exercise
for the reader.

  x < y
  y < x + 10
  0 < x
  ? `dependsOn` ?

-- The total definition requirement ---------------------------------------

For the sake of efficiency we require that all constraints are dispatched as
definining constraints for a variable before we begin solving. We call this the
total definition requirement. This requirement is necessary because a set of
constraints with left over constraints are unlikely to be solveable.

Consider the following example for `p :: (Int, Int)`

fst p < snd p

in which there is no defining constraint for `p`, which would lead us to
compute the spec `mempty` for `p` during solving - meaning we would pick an
arbitrary `p` that is irrespective of the constraints. This is problematic as
the probability of picking `p = (x, y)` such that `x < y` is roughly `1/2`, as
you add more constraints things get much worse.

The principal problem above is that information that is present in the
constraints is lost, which would force us to rely on a `suchThat` approach to
generation - which will become very slow as constraint systems grow.

-- Let binders ------------------------------------------------------------

A solution to the total definition requirement is to introduce more variables.
We can rewrite the problematic `fst p < snd p` example below as:

fst p = x
snd p = y
x < y

The dependency graph for these constraints will be the following:

x `dependsOn` y
p `dependsOn` x

This configuration is solveable, one picks `y` first, then picks `x < y`
and finally constructs `p = (x, y)`.

Note that (1) we introduced more variables than were initially in the
constraints - these need to be bound somewhere - and (2) the order of
`fst p = x` is important - `p` depends on `x` and not the other way
around.

To do both of these things at the same time we introduce the `letBind` construct
to the language:

letBind tm $ \ x -> preds

Which is semantically equivalent to:

exists $ \ x ->
  tm == x
  preds

-- Reifies ----------------------------------------------------------------

Sometimes it's important to be able to perform complex calculations on data
to obtain values that further constrain later variables. For this purpose
the language contains the the `reify` construct:

reify :: IsPred p fn
      => Term fn a
      -> (a -> b)
      -> (Term fn b -> p)
      -> Pred fn

The important thing about `reify` is that because everything in the term
being reified needs to be solved before the body can be solved, all
variables in the body depend on the term being reified.

-}

------------------------------------------------------------------------
-- Terms and Predicates
------------------------------------------------------------------------

-- | Typed first order terms with function symbols from `fn`.
data Term (fn :: [Type] -> Type -> Type) a where
  App ::
    ( Typeable as
    , TypeList as
    , All (HasSpec fn) as
    , HasSpec fn b
    , BaseUniverse fn
    ) =>
    fn as b ->
    List (Term fn) as ->
    Term fn b
  Lit ::
    Show a =>
    a ->
    Term fn a
  V ::
    HasSpec fn a =>
    Var a ->
    Term fn a

instance HasSpec fn a => Eq (Term fn a) where
  V Var a
x == :: Term fn a -> Term fn a -> Bool
== V Var a
x' = Var a
x forall a. Eq a => a -> a -> Bool
== Var a
x'
  Lit a
a == Lit a
b = a
a forall a. Eq a => a -> a -> Bool
== a
b
  App (fn as a
f :: fn as b) List (Term fn) as
ts == App (fn as a
f' :: fn as' b') List (Term fn) as
ts'
    | Just as :~: as
Refl <- forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @as @as'
    , fn as a
f forall a. Eq a => a -> a -> Bool
== fn as a
f' =
        forall {k} (c :: k -> Constraint) (as :: [k]) (f :: k -> *)
       (g :: k -> *).
All c as =>
(forall (a :: k). c a => f a -> g a) -> List f as -> List g as
mapListC @(HasSpec fn) (forall (fn :: [*] -> * -> *) a (f :: * -> *).
HasSpec fn a =>
f a -> WithHasSpec fn f a
WithHasSpec @fn) List (Term fn) as
ts
          forall a. Eq a => a -> a -> Bool
== forall {k} (c :: k -> Constraint) (as :: [k]) (f :: k -> *)
       (g :: k -> *).
All c as =>
(forall (a :: k). c a => f a -> g a) -> List f as -> List g as
mapListC @(HasSpec fn) (forall (fn :: [*] -> * -> *) a (f :: * -> *).
HasSpec fn a =>
f a -> WithHasSpec fn f a
WithHasSpec @fn) List (Term fn) as
ts'
  Term fn a
_ == Term fn a
_ = Bool
False

-- NOTE: Fourmolu made me do this - it happily breaks the code unless you
-- make this a standalone type synonym.
type HasSpecImpliesEq fn a f = HasSpec fn a => Eq (f a) :: Constraint
deriving instance HasSpecImpliesEq fn a f => Eq (WithHasSpec fn f a)

instance (Ord a, Show a, Typeable a, HasSpec fn (Set a)) => Semigroup (Term fn (Set a)) where
  <> :: Term fn (Set a) -> Term fn (Set a) -> Term fn (Set a)
(<>) = forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app (forall (fn :: [*] -> * -> *) a.
(Member (SetFn fn) fn, Ord a, Show a, Typeable a) =>
fn '[Set a, Set a] (Set a)
unionFn @fn @a)

instance (Ord a, Show a, Typeable a, HasSpec fn (Set a)) => Monoid (Term fn (Set a)) where
  mempty :: Term fn (Set a)
mempty = forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit forall a. Monoid a => a
mempty

data Binder fn a where
  (:->) ::
    HasSpec fn a =>
    Var a ->
    Pred fn ->
    Binder fn a

deriving instance Show (Binder fn a)

data Pred (fn :: [Type] -> Type -> Type) where
  Monitor :: ((forall a. Term fn a -> a) -> Property -> Property) -> Pred fn
  Block ::
    [Pred fn] ->
    Pred fn
  Exists ::
    -- | Constructive recovery function for checking
    -- existential quantification
    ((forall b. Term fn b -> b) -> GE a) ->
    Binder fn a ->
    Pred fn
  Subst ::
    HasSpec fn a =>
    Var a ->
    Term fn a ->
    Pred fn ->
    Pred fn
  Let ::
    Term fn a ->
    Binder fn a ->
    Pred fn
  Assert ::
    BaseUniverse fn =>
    Term fn Bool ->
    Pred fn
  Reifies ::
    ( HasSpec fn a
    , HasSpec fn b
    ) =>
    -- | This depends on the `a` term
    Term fn b ->
    Term fn a ->
    -- | Recover a useable value from the `a` term.
    (a -> b) ->
    Pred fn
  -- TODO: there is good cause for not limiting this to `Term fn a` and `Term fn b`.
  -- However, changing it requires re-working quite a lot of code.
  DependsOn ::
    ( HasSpec fn a
    , HasSpec fn b
    ) =>
    Term fn a ->
    Term fn b ->
    Pred fn
  ForAll ::
    ( Forallable t a
    , HasSpec fn t
    , HasSpec fn a
    ) =>
    Term fn t ->
    Binder fn a ->
    Pred fn
  Case ::
    HasSpec fn (SumOver as) =>
    Term fn (SumOver as) ->
    -- | Each branch of the type is bound with
    -- only one variable because `as` are types.
    -- Constructors with multiple arguments are
    -- encoded with `ProdOver` (c.f. `Constrained.Univ`).
    List (Weighted (Binder fn)) as ->
    Pred fn
  -- monadic-style `when` - if the first argument is False the second
  -- doesn't apply.
  When ::
    HasSpec fn Bool =>
    Term fn Bool ->
    Pred fn ->
    Pred fn
  GenHint ::
    HasGenHint fn a =>
    Hint a ->
    Term fn a ->
    Pred fn
  TruePred :: Pred fn
  FalsePred :: NE.NonEmpty String -> Pred fn
  Explain :: NE.NonEmpty String -> Pred fn -> Pred fn

falsePred1 :: String -> Pred fn
falsePred1 :: forall (fn :: [*] -> * -> *). [Char] -> Pred fn
falsePred1 [Char]
s = forall (fn :: [*] -> * -> *). NonEmpty [Char] -> Pred fn
FalsePred (forall (f :: * -> *) a. Applicative f => a -> f a
pure [Char]
s)

data Weighted f a = Weighted {forall (f :: * -> *) a. Weighted f a -> Maybe Int
weight :: Maybe Int, forall (f :: * -> *) a. Weighted f a -> f a
thing :: f a}
  deriving (forall a b. a -> Weighted f b -> Weighted f a
forall a b. (a -> b) -> Weighted f a -> Weighted f b
forall (f :: * -> *) a b.
Functor f =>
a -> Weighted f b -> Weighted f a
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Weighted f a -> Weighted f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Weighted f b -> Weighted f a
$c<$ :: forall (f :: * -> *) a b.
Functor f =>
a -> Weighted f b -> Weighted f a
fmap :: forall a b. (a -> b) -> Weighted f a -> Weighted f b
$cfmap :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Weighted f a -> Weighted f b
Functor, forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall {f :: * -> *}. Traversable f => Functor (Weighted f)
forall {f :: * -> *}. Traversable f => Foldable (Weighted f)
forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
Weighted f (m a) -> m (Weighted f a)
forall (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
Weighted f (f a) -> f (Weighted f a)
forall (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Weighted f a -> m (Weighted f b)
forall (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Weighted f a -> f (Weighted f b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Weighted f a -> f (Weighted f b)
sequence :: forall (m :: * -> *) a.
Monad m =>
Weighted f (m a) -> m (Weighted f a)
$csequence :: forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
Weighted f (m a) -> m (Weighted f a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Weighted f a -> m (Weighted f b)
$cmapM :: forall (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Weighted f a -> m (Weighted f b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Weighted f (f a) -> f (Weighted f a)
$csequenceA :: forall (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
Weighted f (f a) -> f (Weighted f a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Weighted f a -> f (Weighted f b)
$ctraverse :: forall (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Weighted f a -> f (Weighted f b)
Traversable, forall a. Weighted f a -> Bool
forall m a. Monoid m => (a -> m) -> Weighted f a -> m
forall a b. (a -> b -> b) -> b -> Weighted f a -> b
forall (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> Weighted f a -> Bool
forall (f :: * -> *) a. (Foldable f, Num a) => Weighted f a -> a
forall (f :: * -> *) a. (Foldable f, Ord a) => Weighted f a -> a
forall (f :: * -> *) m. (Foldable f, Monoid m) => Weighted f m -> m
forall (f :: * -> *) a. Foldable f => Weighted f a -> Bool
forall (f :: * -> *) a. Foldable f => Weighted f a -> Int
forall (f :: * -> *) a. Foldable f => Weighted f a -> [a]
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Weighted f a -> a
forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Weighted f a -> m
forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Weighted f a -> b
forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Weighted f a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Weighted f a -> a
$cproduct :: forall (f :: * -> *) a. (Foldable f, Num a) => Weighted f a -> a
sum :: forall a. Num a => Weighted f a -> a
$csum :: forall (f :: * -> *) a. (Foldable f, Num a) => Weighted f a -> a
minimum :: forall a. Ord a => Weighted f a -> a
$cminimum :: forall (f :: * -> *) a. (Foldable f, Ord a) => Weighted f a -> a
maximum :: forall a. Ord a => Weighted f a -> a
$cmaximum :: forall (f :: * -> *) a. (Foldable f, Ord a) => Weighted f a -> a
elem :: forall a. Eq a => a -> Weighted f a -> Bool
$celem :: forall (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> Weighted f a -> Bool
length :: forall a. Weighted f a -> Int
$clength :: forall (f :: * -> *) a. Foldable f => Weighted f a -> Int
null :: forall a. Weighted f a -> Bool
$cnull :: forall (f :: * -> *) a. Foldable f => Weighted f a -> Bool
toList :: forall a. Weighted f a -> [a]
$ctoList :: forall (f :: * -> *) a. Foldable f => Weighted f a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Weighted f a -> a
$cfoldl1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Weighted f a -> a
foldr1 :: forall a. (a -> a -> a) -> Weighted f a -> a
$cfoldr1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Weighted f a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Weighted f a -> b
$cfoldl' :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Weighted f a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Weighted f a -> b
$cfoldl :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Weighted f a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Weighted f a -> b
$cfoldr' :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Weighted f a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Weighted f a -> b
$cfoldr :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Weighted f a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Weighted f a -> m
$cfoldMap' :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Weighted f a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Weighted f a -> m
$cfoldMap :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Weighted f a -> m
fold :: forall m. Monoid m => Weighted f m -> m
$cfold :: forall (f :: * -> *) m. (Foldable f, Monoid m) => Weighted f m -> m
Foldable)

mapWeighted :: (f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted :: forall (f :: * -> *) a (g :: * -> *) b.
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted f a -> g b
f (Weighted Maybe Int
w f a
t) = forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
w (f a -> g b
f f a
t)

traverseWeighted :: Applicative m => (f a -> m (g a)) -> Weighted f a -> m (Weighted g a)
traverseWeighted :: forall (m :: * -> *) (f :: * -> *) a (g :: * -> *).
Applicative m =>
(f a -> m (g a)) -> Weighted f a -> m (Weighted g a)
traverseWeighted f a -> m (g a)
f (Weighted Maybe Int
w f a
t) = forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a -> m (g a)
f f a
t

instance BaseUniverse fn => Semigroup (Pred fn) where
  FalsePred NonEmpty [Char]
xs <> :: Pred fn -> Pred fn -> Pred fn
<> FalsePred NonEmpty [Char]
ys = forall (fn :: [*] -> * -> *). NonEmpty [Char] -> Pred fn
FalsePred (NonEmpty [Char]
xs forall a. Semigroup a => a -> a -> a
<> NonEmpty [Char]
ys)
  FalsePred NonEmpty [Char]
es <> Pred fn
_ = forall (fn :: [*] -> * -> *). NonEmpty [Char] -> Pred fn
FalsePred NonEmpty [Char]
es
  Pred fn
_ <> FalsePred NonEmpty [Char]
es = forall (fn :: [*] -> * -> *). NonEmpty [Char] -> Pred fn
FalsePred NonEmpty [Char]
es
  Pred fn
TruePred <> Pred fn
p = Pred fn
p
  Pred fn
p <> Pred fn
TruePred = Pred fn
p
  Pred fn
p <> Pred fn
p' = forall (fn :: [*] -> * -> *). [Pred fn] -> Pred fn
Block (forall {fn :: [*] -> * -> *}. Pred fn -> [Pred fn]
unpackPred Pred fn
p forall a. [a] -> [a] -> [a]
++ forall {fn :: [*] -> * -> *}. Pred fn -> [Pred fn]
unpackPred Pred fn
p')
    where
      unpackPred :: Pred fn -> [Pred fn]
unpackPred (Block [Pred fn]
ps) = [Pred fn]
ps
      unpackPred Pred fn
p = [Pred fn
p]

instance BaseUniverse fn => Monoid (Pred fn) where
  mempty :: Pred fn
mempty = forall (fn :: [*] -> * -> *). Pred fn
TruePred

-- | Contexts for Terms, basically a term with a _single_ HOLE
-- instead of a variable. This is used to traverse the defining
-- constraints for a variable and turn them into a spec. Each
-- subterm `f vs Ctx vs'` for lists of values `vs` and `vs'`
-- gets given to the `propagateSpecFun` for `f` as
-- `f vs HOLE vs'`.
data Ctx (fn :: [Type] -> Type -> Type) v a where
  -- | A single hole of type `v`
  CtxHOLE ::
    HasSpec fn v =>
    Ctx fn v v
  -- | The application `f vs Ctx vs'`
  CtxApp ::
    ( HasSpec fn b
    , TypeList as
    , Typeable as
    , All (HasSpec fn) as
    ) =>
    fn as b ->
    -- This is basically a `List` where
    -- everything is `Value` except for
    -- one entry which is `Ctx fn v`.
    ListCtx Value as (Ctx fn v) ->
    Ctx fn v b

-- | This is used together with `ListCtx` to form
-- just the arguments to `f vs Ctx vs'` - replacing
-- `Ctx` with `HOLE` - to provide to `propagateSpecFun`.
data HOLE a b where
  HOLE :: HOLE a a

toCtx ::
  forall m fn v a.
  ( BaseUniverse fn
  , Typeable v
  , MonadGenError m
  , HasCallStack
  , HasSpec fn a
  , HasSpec fn v
  ) =>
  Var v ->
  Term fn a ->
  m (Ctx fn v a)
toCtx :: forall (m :: * -> *) (fn :: [*] -> * -> *) v a.
(BaseUniverse fn, Typeable v, MonadGenError m, HasCallStack,
 HasSpec fn a, HasSpec fn v) =>
Var v -> Term fn a -> m (Ctx fn v a)
toCtx Var v
v Term fn a
t
  | forall (fn :: [*] -> * -> *) a.
HasVariables fn a =>
Name fn -> a -> Int
countOf (forall (fn :: [*] -> * -> *) a. HasSpec fn a => Var a -> Name fn
Name Var v
v) Term fn a
t forall a. Ord a => a -> a -> Bool
> Int
1 =
      forall (m :: * -> *) a. MonadGenError m => [Char] -> m a
fatalError1 ([Char]
"Can't build a single-hole context for variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Var v
v forall a. [a] -> [a] -> [a]
++ [Char]
" in term " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term fn a
t)
  | Bool
otherwise = forall b. Term fn b -> m (Ctx fn v b)
go Term fn a
t
  where
    go :: forall b. Term fn b -> m (Ctx fn v b)
    go :: forall b. Term fn b -> m (Ctx fn v b)
go (Lit b
i) = forall (m :: * -> *) a. MonadGenError m => [Char] -> m a
fatalError1 ([Char]
"toCtx has literal: (Lit " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show b
i forall a. [a] -> [a] -> [a]
++ [Char]
")")
    go (App fn as b
f List (Term fn) as
as) = forall (fn :: [*] -> * -> *) b (a :: [*]) v.
(HasSpec fn b, TypeList a, Typeable a, All (HasSpec fn) a) =>
fn a b -> ListCtx Value a (Ctx fn v) -> Ctx fn v b
CtxApp fn as b
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) (fn :: [*] -> * -> *) v (as :: [*]).
(BaseUniverse fn, All (HasSpec fn) as, HasSpec fn v, Typeable v,
 MonadGenError m, HasCallStack) =>
Var v -> List (Term fn) as -> m (ListCtx Value as (Ctx fn v))
toCtxList Var v
v List (Term fn) as
as
    go (V Var b
v')
      | Just v :~: b
Refl <- forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var v
v Var b
v' = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) v. HasSpec fn v => Ctx fn v v
CtxHOLE
      | Bool
otherwise =
          forall (m :: * -> *) a. MonadGenError m => [Char] -> m a
fatalError1
            ( [Char]
"toCtx "
                forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Var v
v
                forall a. [a] -> [a] -> [a]
++ [Char]
"@("
                forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. Typeable a => a -> TypeRep
typeOf Var v
v)
                forall a. [a] -> [a] -> [a]
++ [Char]
") (V "
                forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Var b
v'
                forall a. [a] -> [a] -> [a]
++ [Char]
"@("
                forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. Typeable a => a -> TypeRep
typeOf Var b
v')
                forall a. [a] -> [a] -> [a]
++ [Char]
"))"
            )

toCtxList ::
  forall m fn v as.
  (BaseUniverse fn, All (HasSpec fn) as, HasSpec fn v, Typeable v, MonadGenError m, HasCallStack) =>
  Var v ->
  List (Term fn) as ->
  m (ListCtx Value as (Ctx fn v))
toCtxList :: forall (m :: * -> *) (fn :: [*] -> * -> *) v (as :: [*]).
(BaseUniverse fn, All (HasSpec fn) as, HasSpec fn v, Typeable v,
 MonadGenError m, HasCallStack) =>
Var v -> List (Term fn) as -> m (ListCtx Value as (Ctx fn v))
toCtxList Var v
v = forall (as' :: [*]).
(HasCallStack, All (HasSpec fn) as') =>
List (Term fn) as' -> m (ListCtx Value as' (Ctx fn v))
prefix
  where
    prefix ::
      forall as'.
      (HasCallStack, All (HasSpec fn) as') =>
      List (Term fn) as' ->
      m (ListCtx Value as' (Ctx fn v))
    prefix :: forall (as' :: [*]).
(HasCallStack, All (HasSpec fn) as') =>
List (Term fn) as' -> m (ListCtx Value as' (Ctx fn v))
prefix List (Term fn) as'
Nil = forall (m :: * -> *) a. MonadGenError m => [Char] -> m a
fatalError1 [Char]
"toCtxList without hole"
    prefix (Lit a
l :> List (Term fn) as1
ts) = do
      ListCtx Value as1 (Ctx fn v)
ctx <- forall (as' :: [*]).
(HasCallStack, All (HasSpec fn) as') =>
List (Term fn) as' -> m (ListCtx Value as' (Ctx fn v))
prefix List (Term fn) as1
ts
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> Value a
Value a
l forall (f :: * -> *) a (as1 :: [*]) (c :: * -> *).
f a -> ListCtx f as1 c -> ListCtx f (a : as1) c
:! ListCtx Value as1 (Ctx fn v)
ctx
    prefix (Term fn a
t :> List (Term fn) as1
ts) = do
      Ctx fn v a
hole <- forall (m :: * -> *) (fn :: [*] -> * -> *) v a.
(BaseUniverse fn, Typeable v, MonadGenError m, HasCallStack,
 HasSpec fn a, HasSpec fn v) =>
Var v -> Term fn a -> m (Ctx fn v a)
toCtx Var v
v Term fn a
t
      List Value as1
suf <- forall (as' :: [*]). List (Term fn) as' -> m (List Value as')
suffix List (Term fn) as1
ts
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Ctx fn v a
hole forall (c :: * -> *) a (f :: * -> *) (as1 :: [*]).
c a -> List f as1 -> ListCtx f (a : as1) c
:? List Value as1
suf

    suffix :: forall as'. List (Term fn) as' -> m (List Value as')
    suffix :: forall (as' :: [*]). List (Term fn) as' -> m (List Value as')
suffix List (Term fn) as'
Nil = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (f :: k -> *). List f '[]
Nil
    suffix (Lit a
l :> List (Term fn) as1
ts) = (forall a. Show a => a -> Value a
Value a
l forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (as' :: [*]). List (Term fn) as' -> m (List Value as')
suffix List (Term fn) as1
ts
    suffix (Term fn a
_ :> List (Term fn) as1
_) = forall (m :: * -> *) a. MonadGenError m => [Char] -> m a
fatalError1 [Char]
"toCtxList with too many holes"

------------------------------------------------------------------------
-- Semantics of `Term` and `Pred`
------------------------------------------------------------------------

runTerm :: MonadGenError m => Env -> Term fn a -> m a
runTerm :: forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env = \case
  Lit a
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
  V Var a
v -> forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
Env -> Var a -> m a
findEnv Env
env Var a
v
  App fn as a
f List (Term fn) as
ts -> do
    List Identity as
vs <- forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (as :: [k]).
Applicative m =>
(forall (a :: k). f a -> m (g a)) -> List f as -> m (List g as)
mapMList (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env) List (Term fn) as
ts
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
uncurryList_ forall a. Identity a -> a
runIdentity (forall (fn :: [*] -> * -> *) (as :: [*]) b.
FunctionLike fn =>
fn as b -> FunTy as b
sem fn as a
f) List Identity as
vs

-- | Collect the 'monitor' calls from a specification instantiated to the given value. Typically,
--
--   >>> quickCheck $ forAll (genFromSpec spec) $ \ x -> monitorSpec spec x $ ...
monitorSpec :: (FunctionLike fn, Testable p) => Specification fn a -> a -> p -> Property
monitorSpec :: forall (fn :: [*] -> * -> *) p a.
(FunctionLike fn, Testable p) =>
Specification fn a -> a -> p -> Property
monitorSpec (SuspendedSpec Var a
x Pred fn
p) a
a =
  forall a. GE a -> a
errorGE (forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m (Property -> Property)
monitorPred (forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var a
x a
a) Pred fn
p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall prop. Testable prop => prop -> Property
property
monitorSpec Specification fn a
_ a
_ = forall prop. Testable prop => prop -> Property
property

monitorPred ::
  forall fn m. (FunctionLike fn, MonadGenError m) => Env -> Pred fn -> m (Property -> Property)
monitorPred :: forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m (Property -> Property)
monitorPred Env
env = \case
  Monitor (forall a. Term fn a -> a) -> Property -> Property
m -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ((forall a. Term fn a -> a) -> Property -> Property
m forall a b. (a -> b) -> a -> b
$ forall a. GE a -> a
errorGE forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadGenError m => [Char] -> m a -> m a
explain1 [Char]
"monitorPred: Monitor" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env)
  Subst Var a
x Term fn a
t Pred fn
p -> forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m (Property -> Property)
monitorPred Env
env forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Term fn a -> Pred fn -> Pred fn
substitutePred Var a
x Term fn a
t Pred fn
p
  Assert {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id
  GenHint {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id
  Reifies {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id
  ForAll Term fn t
t (Var a
x :-> Pred fn
p) -> do
    t
set <- forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env Term fn t
t
    forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
        [ forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m (Property -> Property)
monitorPred Env
env' Pred fn
p
        | a
v <- forall t e. Forallable t e => t -> [e]
forAllToList t
set
        , let env' :: Env
env' = forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
v Env
env
        ]
  Case Term fn (SumOver as)
t List (Weighted (Binder fn)) as
bs -> do
    SumOver as
v <- forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env Term fn (SumOver as)
t
    forall (as :: [*]) (fn :: [*] -> * -> *) r.
SumOver as
-> List (Binder fn) as
-> (forall a. HasSpec fn a => Var a -> a -> Pred fn -> r)
-> r
runCaseOn SumOver as
v (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList forall (f :: * -> *) a. Weighted f a -> f a
thing List (Weighted (Binder fn)) as
bs) (\Var a
x a
val Pred fn
ps -> forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m (Property -> Property)
monitorPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
val Env
env) Pred fn
ps)
  When Term fn Bool
b Pred fn
p -> do
    Bool
v <- forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env Term fn Bool
b
    if Bool
v then forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m (Property -> Property)
monitorPred Env
env Pred fn
p else forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id
  Pred fn
TruePred -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id
  FalsePred {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id
  DependsOn {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id
  Block [Pred fn]
ps -> forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m (Property -> Property)
monitorPred Env
env) [Pred fn]
ps
  Let Term fn a
t (Var a
x :-> Pred fn
p) -> do
    a
val <- forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env Term fn a
t
    forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m (Property -> Property)
monitorPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
val Env
env) Pred fn
p
  Exists (forall a. Term fn a -> a) -> GE a
k (Var a
x :-> Pred fn
p) -> do
    case (forall a. Term fn a -> a) -> GE a
k (forall a. GE a -> a
errorGE forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadGenError m => [Char] -> m a -> m a
explain1 [Char]
"monitorPred: Exists" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env) of
      Result [NonEmpty [Char]]
_ a
a -> forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m (Property -> Property)
monitorPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
a Env
env) Pred fn
p
      GE a
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id
  Explain NonEmpty [Char]
es Pred fn
p -> forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a -> m a
explain NonEmpty [Char]
es forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m (Property -> Property)
monitorPred Env
env Pred fn
p

checkPred :: forall fn m. (FunctionLike fn, MonadGenError m) => Env -> Pred fn -> m Bool
checkPred :: forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m Bool
checkPred Env
env = \case
  Monitor {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  Subst Var a
x Term fn a
t Pred fn
p -> forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m Bool
checkPred Env
env forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Term fn a -> Pred fn -> Pred fn
substitutePred Var a
x Term fn a
t Pred fn
p
  Assert Term fn Bool
t -> forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env Term fn Bool
t
  GenHint {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  p :: Pred fn
p@(Reifies Term fn b
t' Term fn a
t a -> b
f) -> do
    a
val <- forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env Term fn a
t
    b
val' <- forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env Term fn b
t'
    forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a -> m a
explain (forall a. [a] -> NonEmpty a
NE.fromList [[Char]
"Reification:", [Char]
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Pred fn
p]) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> b
f a
val forall a. Eq a => a -> a -> Bool
== b
val')
  ForAll Term fn t
t (Var a
x :-> Pred fn
p) -> do
    t
set <- forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env Term fn t
t
    forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
        [ forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m Bool
checkPred Env
env' Pred fn
p
        | a
v <- forall t e. Forallable t e => t -> [e]
forAllToList t
set
        , let env' :: Env
env' = forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
v Env
env
        ]
  Case Term fn (SumOver as)
t List (Weighted (Binder fn)) as
bs -> do
    SumOver as
v <- forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env Term fn (SumOver as)
t
    forall (as :: [*]) (fn :: [*] -> * -> *) r.
SumOver as
-> List (Binder fn) as
-> (forall a. HasSpec fn a => Var a -> a -> Pred fn -> r)
-> r
runCaseOn SumOver as
v (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList forall (f :: * -> *) a. Weighted f a -> f a
thing List (Weighted (Binder fn)) as
bs) (\Var a
x a
val Pred fn
ps -> forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m Bool
checkPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
val Env
env) Pred fn
ps)
  When Term fn Bool
bt Pred fn
p -> do
    Bool
b <- forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env Term fn Bool
bt
    if Bool
b then forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m Bool
checkPred Env
env Pred fn
p else forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  Pred fn
TruePred -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  FalsePred NonEmpty [Char]
es -> forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a -> m a
explain NonEmpty [Char]
es forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
  DependsOn {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  Block [Pred fn]
ps -> forall (m :: * -> *) (t :: * -> *) (fn :: [*] -> * -> *).
(MonadGenError m, Traversable t, FunctionLike fn) =>
Env -> t (Pred fn) -> m Bool
checkPreds Env
env [Pred fn]
ps
  Let Term fn a
t (Var a
x :-> Pred fn
p) -> do
    a
val <- forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env Term fn a
t
    forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m Bool
checkPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
val Env
env) Pred fn
p
  Exists (forall b. Term fn b -> b) -> GE a
k (Var a
x :-> Pred fn
p) -> do
    a
a <- forall (m :: * -> *) r. MonadGenError m => GE r -> m r
runGE forall a b. (a -> b) -> a -> b
$ (forall b. Term fn b -> b) -> GE a
k (forall a. GE a -> a
errorGE forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadGenError m => [Char] -> m a -> m a
explain1 [Char]
"checkPred: Exists" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env)
    forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m Bool
checkPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
a Env
env) Pred fn
p
  Explain NonEmpty [Char]
es Pred fn
p -> forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a -> m a
explain NonEmpty [Char]
es forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m Bool
checkPred Env
env Pred fn
p

checkPreds :: (MonadGenError m, Traversable t, FunctionLike fn) => Env -> t (Pred fn) -> m Bool
checkPreds :: forall (m :: * -> *) (t :: * -> *) (fn :: [*] -> * -> *).
(MonadGenError m, Traversable t, FunctionLike fn) =>
Env -> t (Pred fn) -> m Bool
checkPreds Env
env t (Pred fn)
ps = forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m Bool
checkPred Env
env) t (Pred fn)
ps

checkPredPure :: FunctionLike fn => Env -> Pred fn -> Bool
checkPredPure :: forall (fn :: [*] -> * -> *).
FunctionLike fn =>
Env -> Pred fn -> Bool
checkPredPure Env
env Pred fn
p = forall a. (NonEmpty [Char] -> a) -> GE a -> a
fromGE (forall a b. a -> b -> a
const Bool
False) forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m Bool
checkPred Env
env Pred fn
p

runCaseOn ::
  SumOver as ->
  List (Binder fn) as ->
  (forall a. HasSpec fn a => Var a -> a -> Pred fn -> r) ->
  r
runCaseOn :: forall (as :: [*]) (fn :: [*] -> * -> *) r.
SumOver as
-> List (Binder fn) as
-> (forall a. HasSpec fn a => Var a -> a -> Pred fn -> r)
-> r
runCaseOn SumOver as
_ List (Binder fn) as
Nil forall a. HasSpec fn a => Var a -> a -> Pred fn -> r
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"The impossible happened in runCaseOn"
runCaseOn SumOver as
a ((Var a
x :-> Pred fn
ps) :> List (Binder fn) as1
Nil) forall a. HasSpec fn a => Var a -> a -> Pred fn -> r
f = forall a. HasSpec fn a => Var a -> a -> Pred fn -> r
f Var a
x SumOver as
a Pred fn
ps
runCaseOn SumOver as
s ((Var a
x :-> Pred fn
ps) :> bs :: List (Binder fn) as1
bs@(Binder fn a
_ :> List (Binder fn) as1
_)) forall a. HasSpec fn a => Var a -> a -> Pred fn -> r
f = case SumOver as
s of
  SumLeft a
a -> forall a. HasSpec fn a => Var a -> a -> Pred fn -> r
f Var a
x a
a Pred fn
ps
  SumRight SumOver (a : as1)
a -> forall (as :: [*]) (fn :: [*] -> * -> *) r.
SumOver as
-> List (Binder fn) as
-> (forall a. HasSpec fn a => Var a -> a -> Pred fn -> r)
-> r
runCaseOn SumOver (a : as1)
a List (Binder fn) as1
bs forall a. HasSpec fn a => Var a -> a -> Pred fn -> r
f

------------------------------------------------------------------------
-- Specs
------------------------------------------------------------------------

-- NOTE: in the future one might consider using sets when a type
-- has `Ord` here. Beware, this means that one needs to have a check
-- for instances of Ord at runtime!
type OrdSet a = [a]

-- | A `Specification fn a` denotes a set of `a`s
data Specification fn a where
  -- | Explain a Specification
  ExplainSpec :: [String] -> Specification fn a -> Specification fn a
  -- | Elements of a known set
  MemberSpec ::
    -- | It must be an element of this OrdSet (List). Try hard not to put duplicates in the List.
    NE.NonEmpty a ->
    Specification fn a
  -- | The empty set
  ErrorSpec ::
    NE.NonEmpty String ->
    Specification fn a
  -- | The set described by some predicates
  -- over the bound variable.
  --
  -- TODO: possibly we want to use a `Binder` here
  SuspendedSpec ::
    HasSpec fn a =>
    -- | This variable ranges over values denoted by
    -- the spec
    Var a ->
    -- | And the variable is subject to these constraints
    Pred fn ->
    Specification fn a
  -- | A type-specific spec
  TypeSpec ::
    HasSpec fn a =>
    TypeSpec fn a ->
    -- | It can't be any of the elements of this set
    OrdSet a ->
    Specification fn a
  -- | Anything
  TrueSpec :: Specification fn a

explainSpecOpt :: [String] -> Specification fn a -> Specification fn a
explainSpecOpt :: forall (fn :: [*] -> * -> *) a.
[[Char]] -> Specification fn a -> Specification fn a
explainSpecOpt [] Specification fn a
x = Specification fn a
x
explainSpecOpt [[Char]]
es1 (ExplainSpec [[Char]]
es2 Specification fn a
x) = forall (fn :: [*] -> * -> *) a.
[[Char]] -> Specification fn a -> Specification fn a
explainSpecOpt ([[Char]]
es1 forall a. [a] -> [a] -> [a]
++ [[Char]]
es2) Specification fn a
x
explainSpecOpt [[Char]]
es Specification fn a
spec = forall (fn :: [*] -> * -> *) a.
[[Char]] -> Specification fn a -> Specification fn a
ExplainSpec [[Char]]
es Specification fn a
spec

-- | return a MemberSpec or ans ErrorSpec depending on if 'xs' the null list or not
memberSpecList :: [a] -> NE.NonEmpty String -> Specification fn a
memberSpecList :: forall a (fn :: [*] -> * -> *).
[a] -> NonEmpty [Char] -> Specification fn a
memberSpecList [a]
xs NonEmpty [Char]
messages =
  case forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty [a]
xs of
    Maybe (NonEmpty a)
Nothing -> forall (fn :: [*] -> * -> *) a.
NonEmpty [Char] -> Specification fn a
ErrorSpec NonEmpty [Char]
messages
    Just NonEmpty a
ys -> forall a (fn :: [*] -> * -> *). NonEmpty a -> Specification fn a
MemberSpec NonEmpty a
ys

instance Arbitrary a => Arbitrary (NE.NonEmpty a) where
  arbitrary :: Gen (NonEmpty a)
arbitrary = do
    NonEmpty [a]
xs <- forall a. Arbitrary a => Gen a
arbitrary
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. [a] -> NonEmpty a
NE.fromList [a]
xs)

instance HasSpec fn a => Semigroup (Specification fn a) where
  ExplainSpec [[Char]]
es Specification fn a
x <> :: Specification fn a -> Specification fn a -> Specification fn a
<> Specification fn a
y = forall (fn :: [*] -> * -> *) a.
[[Char]] -> Specification fn a -> Specification fn a
explainSpecOpt [[Char]]
es (Specification fn a
x forall a. Semigroup a => a -> a -> a
<> Specification fn a
y)
  Specification fn a
x <> ExplainSpec [[Char]]
es Specification fn a
y = forall (fn :: [*] -> * -> *) a.
[[Char]] -> Specification fn a -> Specification fn a
explainSpecOpt [[Char]]
es (Specification fn a
x forall a. Semigroup a => a -> a -> a
<> Specification fn a
y)
  Specification fn a
TrueSpec <> Specification fn a
s = Specification fn a
s
  Specification fn a
s <> Specification fn a
TrueSpec = Specification fn a
s
  ErrorSpec NonEmpty [Char]
e <> ErrorSpec NonEmpty [Char]
e' =
    forall (fn :: [*] -> * -> *) a.
NonEmpty [Char] -> Specification fn a
ErrorSpec
      ( NonEmpty [Char]
e
          forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char]
"------ spec <> spec ------ @" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @a)))
          forall a. Semigroup a => a -> a -> a
<> NonEmpty [Char]
e'
      )
  ErrorSpec NonEmpty [Char]
e <> Specification fn a
_ = forall (fn :: [*] -> * -> *) a.
NonEmpty [Char] -> Specification fn a
ErrorSpec NonEmpty [Char]
e
  Specification fn a
_ <> ErrorSpec NonEmpty [Char]
e = forall (fn :: [*] -> * -> *) a.
NonEmpty [Char] -> Specification fn a
ErrorSpec NonEmpty [Char]
e
  MemberSpec NonEmpty a
as <> MemberSpec NonEmpty a
as' =
    forall (fn :: [*] -> * -> *) a.
NonEmpty [Char] -> Specification fn a -> Specification fn a
addToErrorSpec
      ( forall a. [a] -> NonEmpty a
NE.fromList
          [[Char]
"Intersecting: ", [Char]
"  MemberSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as), [Char]
"  MemberSpec " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as')]
      )
      ( forall a (fn :: [*] -> * -> *).
[a] -> NonEmpty [Char] -> Specification fn a
memberSpecList
          (forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a] -> [a]
intersect (forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as) (forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as'))
          (forall (f :: * -> *) a. Applicative f => a -> f a
pure [Char]
"Empty intersection")
      )
  ms :: Specification fn a
ms@(MemberSpec NonEmpty a
as) <> ts :: Specification fn a
ts@TypeSpec {} =
    forall a (fn :: [*] -> * -> *).
[a] -> NonEmpty [Char] -> Specification fn a
memberSpecList
      (forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> NonEmpty a -> [a]
NE.filter (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn a
ts) NonEmpty a
as)
      ( forall a. [a] -> NonEmpty a
NE.fromList
          [ [Char]
"The two " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @a)) forall a. [a] -> [a] -> [a]
++ [Char]
" Specifications are inconsistent."
          , [Char]
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Specification fn a
ms
          , [Char]
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Specification fn a
ts
          ]
      )
  TypeSpec TypeSpec fn a
s [a]
cant <> MemberSpec NonEmpty a
as = forall a (fn :: [*] -> * -> *). NonEmpty a -> Specification fn a
MemberSpec NonEmpty a
as forall a. Semigroup a => a -> a -> a
<> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> OrdSet a -> Specification fn a
TypeSpec TypeSpec fn a
s [a]
cant
  SuspendedSpec Var a
v Pred fn
p <> SuspendedSpec Var a
v' Pred fn
p' = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Pred fn -> Specification fn a
SuspendedSpec Var a
v (Pred fn
p forall a. Semigroup a => a -> a -> a
<> forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var a
v' Var a
v Pred fn
p')
  SuspendedSpec Var a
v Pred fn
ps <> Specification fn a
s = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Pred fn -> Specification fn a
SuspendedSpec Var a
v (Pred fn
ps forall a. Semigroup a => a -> a -> a
<> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies (forall (fn :: [*] -> * -> *) a. HasSpec fn a => Var a -> Term fn a
V Var a
v) Specification fn a
s)
  Specification fn a
s <> SuspendedSpec Var a
v Pred fn
ps = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Pred fn -> Specification fn a
SuspendedSpec Var a
v (Pred fn
ps forall a. Semigroup a => a -> a -> a
<> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies (forall (fn :: [*] -> * -> *) a. HasSpec fn a => Var a -> Term fn a
V Var a
v) Specification fn a
s)
  TypeSpec TypeSpec fn a
s [a]
cant <> TypeSpec TypeSpec fn a
s' [a]
cant' = case forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> TypeSpec fn a -> Specification fn a
combineSpec TypeSpec fn a
s TypeSpec fn a
s' of
    -- NOTE: This might look like an unnecessary case, but doing
    -- it like this avoids looping.
    TypeSpec TypeSpec fn a
s'' [a]
cant'' -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> OrdSet a -> Specification fn a
TypeSpec TypeSpec fn a
s'' ([a]
cant forall a. Semigroup a => a -> a -> a
<> [a]
cant' forall a. Semigroup a => a -> a -> a
<> [a]
cant'')
    Specification fn a
s'' -> Specification fn a
s'' forall a. Semigroup a => a -> a -> a
<> forall (fn :: [*] -> * -> *) a (f :: * -> *).
(HasSpec fn a, Foldable f) =>
f a -> Specification fn a
notMemberSpec ([a]
cant forall a. Semigroup a => a -> a -> a
<> [a]
cant')

instance HasSpec fn a => Monoid (Specification fn a) where
  mempty :: Specification fn a
mempty = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec

instance (HasSpec fn a, Arbitrary (TypeSpec fn a)) => Arbitrary (Specification fn a) where
  arbitrary :: Gen (Specification fn a)
arbitrary = do
    Specification fn a
baseSpec <-
      forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
        [ (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec)
        ,
          ( Int
7
          , do
              [a]
zs <- forall a. Eq a => [a] -> [a]
nub forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Gen a -> Gen [a]
listOf1 (forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec)
              forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( forall a (fn :: [*] -> * -> *).
[a] -> NonEmpty [Char] -> Specification fn a
memberSpecList
                    [a]
zs
                    ( forall a. [a] -> NonEmpty a
NE.fromList
                        [ [Char]
"In (Arbitrary Specification) this should never happen"
                        , [Char]
"listOf1 generates empty list."
                        ]
                    )
                )
          )
        , (Int
10, forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary)
        ,
          ( Int
1
          , do
              Int
len <- forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
5)
              forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> OrdSet a -> Specification fn a
TypeSpec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Int -> Gen a -> Gen [a]
vectorOf Int
len (forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec @fn forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec)
          )
        , (Int
1, forall (fn :: [*] -> * -> *) a.
NonEmpty [Char] -> Specification fn a
ErrorSpec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary)
        , -- Recurse to make sure we apply the tricks for generating suspended specs multiple times
          (Int
1, forall a. Arbitrary a => Gen a
arbitrary)
        ]
    -- TODO: we probably want smarter ways of generating constraints
    forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
      [ (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn a
x -> Term fn a
x forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn a
baseSpec)
      , (Int
1, forall (fn :: [*] -> * -> *) a.
[[Char]] -> Specification fn a -> Specification fn a
ExplainSpec [[Char]
"Arbitrary"] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary)
      ,
        ( Int
1
        , forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn a
x -> forall a p (fn :: [*] -> * -> *).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists (\forall b. Term fn b -> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall b. Term fn b -> b
eval Term fn a
x) forall a b. (a -> b) -> a -> b
$ \Term fn a
y ->
            [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn a
x forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn a
y
            , Term fn a
y forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn a
baseSpec
            ]
        )
      , (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn a
x -> forall (fn :: [*] -> * -> *) a p.
(HasSpec fn a, IsPred p fn) =>
Term fn a -> (Term fn a -> p) -> Pred fn
letBind Term fn a
x forall a b. (a -> b) -> a -> b
$ \Term fn a
y -> Term fn a
y forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn a
baseSpec)
      ,
        ( Int
1
        , forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn a
x -> forall a p (fn :: [*] -> * -> *).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists (\forall b. Term fn b -> b
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) forall a b. (a -> b) -> a -> b
$ \Term fn Bool
b ->
            forall (fn :: [*] -> * -> *) p q.
(BaseUniverse fn, IsPred p fn, IsPred q fn) =>
Term fn Bool -> p -> q -> Pred fn
ifElse Term fn Bool
b (Term fn a
x forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn a
baseSpec) (Term fn a
x forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn a
baseSpec)
        )
      ,
        ( Int
1
        , forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn a
x -> forall a p (fn :: [*] -> * -> *).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists (\forall b. Term fn b -> b
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) forall a b. (a -> b) -> a -> b
$ \Term fn Bool
b ->
            [ forall (fn :: [*] -> * -> *) p q.
(BaseUniverse fn, IsPred p fn, IsPred q fn) =>
Term fn Bool -> p -> q -> Pred fn
ifElse Term fn Bool
b Bool
True (Term fn a
x forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn a
baseSpec)
            , Term fn a
x forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn a
baseSpec
            ]
        )
      ,
        ( Int
1
        , forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn a
x -> forall a p (fn :: [*] -> * -> *).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists (\forall b. Term fn b -> b
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False) forall a b. (a -> b) -> a -> b
$ \Term fn Bool
b ->
            [ forall (fn :: [*] -> * -> *) p q.
(BaseUniverse fn, IsPred p fn, IsPred q fn) =>
Term fn Bool -> p -> q -> Pred fn
ifElse Term fn Bool
b (Term fn a
x forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn a
baseSpec) Bool
True
            , Term fn a
x forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn a
baseSpec
            ]
        )
      ,
        ( Int
1
        , forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn a
x -> forall (fn :: [*] -> * -> *). NonEmpty [Char] -> Pred fn -> Pred fn
explanation (forall (f :: * -> *) a. Applicative f => a -> f a
pure [Char]
"its very subtle, you won't get it.") forall a b. (a -> b) -> a -> b
$ Term fn a
x forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn a
baseSpec
        )
      , (Int
10, forall (f :: * -> *) a. Applicative f => a -> f a
pure Specification fn a
baseSpec)
      ]

  shrink :: Specification fn a -> [Specification fn a]
shrink (ExplainSpec [[Char]]
es Specification fn a
x) =
    forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
      forall a. a -> [a] -> [a]
: forall (fn :: [*] -> * -> *) a.
NonEmpty [Char] -> Specification fn a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char]
"shrink (ExplainSpec msg spec)"))
      forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall (fn :: [*] -> * -> *) a.
[[Char]] -> Specification fn a -> Specification fn a
ExplainSpec [[Char]]
es) (forall a. Arbitrary a => a -> [a]
shrink Specification fn a
x)
  shrink Specification fn a
TrueSpec = []
  shrink (MemberSpec NonEmpty a
ys) = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec forall a. a -> [a] -> [a]
: forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {a} {fn :: [*] -> * -> *}.
Eq a =>
[a] -> Maybe (Specification fn a)
mem (forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec @fn forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec) (forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
ys))
    where
      mem :: [a] -> Maybe (Specification fn a)
mem [a]
xs =
        case forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty (forall a. Eq a => [a] -> [a]
nub [a]
xs) of
          Maybe (NonEmpty a)
Nothing -> forall a. Maybe a
Nothing
          Just NonEmpty a
as -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). NonEmpty a -> Specification fn a
MemberSpec NonEmpty a
as
  shrink (TypeSpec TypeSpec fn a
ts [a]
cant)
    | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
cant =
        forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec forall a. a -> [a] -> [a]
: forall (fn :: [*] -> * -> *) a.
NonEmpty [Char] -> Specification fn a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure [Char]
"From shrinking TypeSpec with null cant") forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec (forall a. Arbitrary a => a -> [a]
shrink TypeSpec fn a
ts)
    | Bool
otherwise =
        [forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec, forall (fn :: [*] -> * -> *) a.
NonEmpty [Char] -> Specification fn a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure [Char]
"From shrinking TypeSpec"), forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec TypeSpec fn a
ts]
          forall a. [a] -> [a] -> [a]
++ ( case forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty (forall a. Eq a => [a] -> [a]
nub [a]
cant) of
                Maybe (NonEmpty a)
Nothing -> []
                Just NonEmpty a
as -> [forall a (fn :: [*] -> * -> *). NonEmpty a -> Specification fn a
MemberSpec NonEmpty a
as]
             )
          forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec (forall a. Arbitrary a => a -> [a]
shrink TypeSpec fn a
ts)
          forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> OrdSet a -> Specification fn a
TypeSpec TypeSpec fn a
ts) (forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec @fn forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec) [a]
cant)
  shrink (SuspendedSpec Var a
x Pred fn
p) =
    [forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec, forall (fn :: [*] -> * -> *) a.
NonEmpty [Char] -> Specification fn a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure [Char]
"From shrinking SuspendedSpec")]
      forall a. [a] -> [a] -> [a]
++ [ Specification fn a
s
         | Result [NonEmpty [Char]]
_ Specification fn a
s <- [forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasCallStack) =>
Var a -> Pred fn -> GE (Specification fn a)
computeSpec Var a
x Pred fn
p]
         , Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a. Specification fn a -> Bool
isSuspendedSpec Specification fn a
s
         ]
      forall a. [a] -> [a] -> [a]
++ [forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Pred fn -> Specification fn a
SuspendedSpec Var a
x Pred fn
p' | Pred fn
p' <- forall {fn :: [*] -> * -> *}. Pred fn -> [Pred fn]
shrinkPred Pred fn
p]
  shrink ErrorSpec {} = [forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec]

shrinkPred :: Pred fn -> [Pred fn]
shrinkPred :: forall {fn :: [*] -> * -> *}. Pred fn -> [Pred fn]
shrinkPred (Block [Pred fn]
ps) = forall (fn :: [*] -> * -> *). Pred fn
TruePred forall a. a -> [a] -> [a]
: forall (fn :: [*] -> * -> *). [Char] -> Pred fn
falsePred1 [Char]
"shrink block" forall a. a -> [a] -> [a]
: [Pred fn]
ps forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall (fn :: [*] -> * -> *). [Pred fn] -> Pred fn
Block (forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList forall {fn :: [*] -> * -> *}. Pred fn -> [Pred fn]
shrinkPred [Pred fn]
ps)
shrinkPred (Assert Term fn Bool
t) =
  [forall (fn :: [*] -> * -> *). Pred fn
TruePred, forall (fn :: [*] -> * -> *). [Char] -> Pred fn
falsePred1 [Char]
"shrink assert", forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Pred fn
Assert Term fn Bool
t]
shrinkPred (Explain NonEmpty [Char]
_ Pred fn
p) = forall (fn :: [*] -> * -> *). Pred fn
TruePred forall a. a -> [a] -> [a]
: forall (fn :: [*] -> * -> *). [Char] -> Pred fn
falsePred1 [Char]
"shrink explain" forall a. a -> [a] -> [a]
: [Pred fn
p]
shrinkPred (When Term fn Bool
b Pred fn
p) = forall (fn :: [*] -> * -> *). Pred fn
TruePred forall a. a -> [a] -> [a]
: forall (fn :: [*] -> * -> *). [Char] -> Pred fn
falsePred1 [Char]
"shrink when" forall a. a -> [a] -> [a]
: Pred fn
p forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall (fn :: [*] -> * -> *).
HasSpec fn Bool =>
Term fn Bool -> Pred fn -> Pred fn
When Term fn Bool
b) (forall {fn :: [*] -> * -> *}. Pred fn -> [Pred fn]
shrinkPred Pred fn
p)
-- NOTE: You can't shrink `Exists` because it might make the `Env -> a` invalid!
-- e.g. you start with
-- `constrained $ \ x -> exists (\eval -> pure $ eval x) $ \ y -> [ x ==. y, 10 <. y ]`
-- and shrink it to
-- `constrained $ \ x -> exists (\eval -> pure $ eval x) $ \ y -> [ 10 <. y ]`
-- and suddenly the thing you're generating is BS w.r.t the checking!
shrinkPred Exists {} = [forall (fn :: [*] -> * -> *). Pred fn
TruePred, forall (fn :: [*] -> * -> *). [Char] -> Pred fn
falsePred1 [Char]
"shrink exists"]
shrinkPred (Subst Var a
x Term fn a
t Pred fn
p) = forall {fn :: [*] -> * -> *}. Pred fn -> [Pred fn]
shrinkPred forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Term fn a -> Pred fn -> Pred fn
substitutePred Var a
x Term fn a
t Pred fn
p
shrinkPred GenHint {} = [forall (fn :: [*] -> * -> *). Pred fn
TruePred, forall (fn :: [*] -> * -> *). [Char] -> Pred fn
falsePred1 [Char]
"shrink hint"]
shrinkPred Monitor {} = [forall (fn :: [*] -> * -> *). Pred fn
TruePred, forall (fn :: [*] -> * -> *). [Char] -> Pred fn
falsePred1 [Char]
"shrink monitor"]
shrinkPred DependsOn {} = [forall (fn :: [*] -> * -> *). Pred fn
TruePred, forall (fn :: [*] -> * -> *). [Char] -> Pred fn
falsePred1 [Char]
"shrink depends"]
-- TODO: fixme
shrinkPred Case {} = [forall (fn :: [*] -> * -> *). Pred fn
TruePred, forall (fn :: [*] -> * -> *). [Char] -> Pred fn
falsePred1 [Char]
"shrink case"]
shrinkPred (Let Term fn a
t (Var a
x :-> Pred fn
p)) = forall (fn :: [*] -> * -> *) a. Term fn a -> Binder fn a -> Pred fn
Let Term fn a
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var a
x forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Pred fn -> Binder fn a
:->) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {fn :: [*] -> * -> *}. Pred fn -> [Pred fn]
shrinkPred Pred fn
p
shrinkPred Pred fn
_ = []

isSuspendedSpec :: Specification fn a -> Bool
isSuspendedSpec :: forall (fn :: [*] -> * -> *) a. Specification fn a -> Bool
isSuspendedSpec (ExplainSpec [[Char]]
_ Specification fn a
x) = forall (fn :: [*] -> * -> *) a. Specification fn a -> Bool
isSuspendedSpec Specification fn a
x
isSuspendedSpec SuspendedSpec {} = Bool
True
isSuspendedSpec Specification fn a
_ = Bool
False

equalSpec :: a -> Specification fn a
equalSpec :: forall a (fn :: [*] -> * -> *). a -> Specification fn a
equalSpec = forall a (fn :: [*] -> * -> *). NonEmpty a -> Specification fn a
MemberSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure

notEqualSpec :: forall fn a. HasSpec fn a => a -> Specification fn a
notEqualSpec :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a
notEqualSpec = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> OrdSet a -> Specification fn a
TypeSpec (forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a
emptySpec @fn @a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure

notMemberSpec :: forall fn a f. (HasSpec fn a, Foldable f) => f a -> Specification fn a
notMemberSpec :: forall (fn :: [*] -> * -> *) a (f :: * -> *).
(HasSpec fn a, Foldable f) =>
f a -> Specification fn a
notMemberSpec = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> OrdSet a -> Specification fn a
typeSpecOpt (forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a
emptySpec @fn @a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

typeSpec :: HasSpec fn a => TypeSpec fn a -> Specification fn a
typeSpec :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec TypeSpec fn a
ts = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> OrdSet a -> Specification fn a
TypeSpec TypeSpec fn a
ts forall a. Monoid a => a
mempty

-- Used to show binary operators like SumSpec and PairSpec
data BinaryShow where
  BinaryShow :: forall a. String -> [Doc a] -> BinaryShow
  NonBinary :: BinaryShow

-- The HasSpec Class ------------------------------------------------------

-- | This class provides the interface that allows you to extend the language
-- to handle a new type. In the case of types that have a generic representation
-- (via `HasSimpleRep`) that already has an instance of `HasSpec` it is sufficient
-- to provide an empty instance. However, for types that are used together with
-- specific functions in the function universe `fn` it may be necessary to provide
-- a specific implementation of `HasSpec`. This is typically necessary when the `TypeSpec`
-- for the generic representation does not permit an implementation of `propagateSpecFun`
-- for some function.
--
-- The basic types provided in the language, `Set`, `[]`, `Map`, `Int`, `Word64`,
-- `(,)`, `Either`, etc. have instances of this class (technically `(,)` and `Either` have
-- instances derived from the instances for their generic `Prod` and `Sum` implementations).
class
  ( Typeable a
  , Eq a
  , Show a
  , Show (TypeSpec fn a)
  , BaseUniverse fn
  ) =>
  HasSpec fn a
  where
  -- | The `TypeSpec fn a` is the type-specific `Specification fn a`.
  type TypeSpec (fn :: [Type] -> Type -> Type) a

  type TypeSpec fn a = TypeSpec fn (SimpleRep a)

  -- `TypeSpec` behaves sort-of like a monoid with a neutral
  -- enement `emptySpec` and a `combineSpec` for combining
  -- two `TypeSpec fn a`. However, in order to provide flexibilty
  -- `combineSpec` takes two `TypeSpec` and provide a `Specification`. This
  -- avoids e.g. having to have a separate implementation of `ErrorSpec`
  -- and `MemberSpec` in `TypeSpec`.

  emptySpec :: TypeSpec fn a
  combineSpec :: TypeSpec fn a -> TypeSpec fn a -> Specification fn a

  -- | Generate a value that satisfies the `TypeSpec`.
  -- The key property for this generator is soundness:
  --  ∀ a ∈ genFromTypeSpec spec. a `conformsTo` spec
  genFromTypeSpec :: (HasCallStack, MonadGenError m) => TypeSpec fn a -> GenT m a

  -- | Check conformance to the spec.
  conformsTo :: HasCallStack => a -> TypeSpec fn a -> Bool

  -- | Shrink an `a` with the aide of a `TypeSpec`
  shrinkWithTypeSpec :: TypeSpec fn a -> a -> [a]

  -- | Convert a spec to predicates:
  -- The key property here is:
  --   ∀ a. a `conformsTo` spec == a `conformsTo` constrained (\t -> toPreds t spec)
  toPreds :: Term fn a -> TypeSpec fn a -> Pred fn

  -- | Compute an upper and lower bound on the number of solutions genFromTypeSpec might return
  cardinalTypeSpec :: TypeSpec fn a -> Specification fn Integer

  -- | A bound on the number of solutions `genFromTypeSpec TrueSpec` can produce.
  --   For a type with finite elements, we can get a much more accurate
  --   answer than TrueSpec
  cardinalTrueSpec :: Specification fn Integer
  cardinalTrueSpec = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec

  -- Each instance can decide if a TypeSpec has an Error, and what String
  -- to pass to ErrorSpec to create an ErrorSpec value. Particulary
  -- useful for type Sum and Prod
  typeSpecHasError :: TypeSpec fn a -> Maybe (NE.NonEmpty String)
  typeSpecHasError TypeSpec fn a
_ = forall a. Maybe a
Nothing

  -- Some binary TypeSpecs, which nest to the right
  -- e.g. something like this (X a (TypeSpec (X b (TypeSpec (X c w))))))
  -- An would look better in Vertical mode as (X [a,b,c] m).
  -- This lets each HasSpec instance decide. Particulary useful for type Sum and Prod
  alternateShow :: TypeSpec fn a -> BinaryShow
  alternateShow TypeSpec fn a
_ = BinaryShow
NonBinary

  monadConformsTo :: a -> TypeSpec fn a -> Writer [String] Bool
  monadConformsTo a
x TypeSpec fn a
spec =
    if forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasCallStack) =>
a -> TypeSpec fn a -> Bool
conformsTo @fn @a a
x TypeSpec fn a
spec
      then forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
      else forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [[Char]
"Fails by " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show TypeSpec fn a
spec] forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

  -- | For some types (especially finite ones) there may be much better ways to construct
  --   a Specification than the default method of just adding a large 'bad' list to TypSpec. This
  --   function allows each HasSpec instance to decide.
  typeSpecOpt :: TypeSpec fn a -> [a] -> Specification fn a
  typeSpecOpt TypeSpec fn a
tySpec [a]
bad = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> OrdSet a -> Specification fn a
TypeSpec TypeSpec fn a
tySpec [a]
bad

  -- | This can be used to detect self inconsistencies in a (TypeSpec fn t)
  guardTypeSpec :: [String] -> TypeSpec fn a -> Specification fn a
  guardTypeSpec [[Char]]
_ TypeSpec fn a
ty = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec TypeSpec fn a
ty

  -- | Prerequisites for the instance that are sometimes necessary
  -- when working with e.g. `Specification`s or functions in the universe.
  type Prerequisites fn a :: Constraint

  type Prerequisites fn a = ()

  -- | Materialize the `Prerequisites` dictionary. It should not be necessary to
  -- implement this function manually.
  prerequisites :: Evidence (Prerequisites fn a)
  default prerequisites :: Prerequisites fn a => Evidence (Prerequisites fn a)
  prerequisites = forall (c :: Constraint). c => Evidence c
Evidence

  {- NOTE: Below follows default implementations for the the functions in this
     class.  They are meant to provide an implementation of `HasSpec fn a` when
     `HasSimpleRep a` and `HasSpec fn (SimpleRep a)`. For example, for a
     newtype wrapper like `newtype Foo = Foo Word64` we can define `SimpleRep
     Foo = Word64` with the requisite instance for `HasSimpleRep` (all of which
     is derived from `Generic Foo`) and the instance for `HasSpec fn Foo` is
     essentially the same as the instance for `Word64`. This is achieved by
     ensuring that `TypeSpec fn Foo = TypeSpec fn Word64` (c.f. the default
     implementation of `TypeSpec` above). To this end, the implementations
     below simply convert the relevant things between `SimpleRep a` and `a`.
     For example, in the implementation of `combineSpec s s'` we treat `s` and
     `s'` (which have type `TypeSpec fn a`) as `TypeSpec fn (SimpleRep a)`,
     combine them, and go from the resulting `Specification fn (SimpleRep a)` to `Specification
     fn a` using `fromSimpleRepSpec`.
   -}

  default emptySpec ::
    (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) => TypeSpec fn a
  emptySpec = forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a
emptySpec @fn @(SimpleRep a)

  default combineSpec ::
    ( HasSimpleRep a
    , HasSpec fn (SimpleRep a)
    , TypeSpec fn a ~ TypeSpec fn (SimpleRep a)
    ) =>
    TypeSpec fn a ->
    TypeSpec fn a ->
    Specification fn a
  combineSpec TypeSpec fn a
s TypeSpec fn a
s' = forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Specification fn (SimpleRep a) -> Specification fn a
fromSimpleRepSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> TypeSpec fn a -> Specification fn a
combineSpec @fn @(SimpleRep a) TypeSpec fn a
s TypeSpec fn a
s'

  default genFromTypeSpec ::
    ( HasSimpleRep a
    , HasSpec fn (SimpleRep a)
    , TypeSpec fn a ~ TypeSpec fn (SimpleRep a)
    ) =>
    (HasCallStack, MonadGenError m) =>
    TypeSpec fn a ->
    GenT m a
  genFromTypeSpec TypeSpec fn a
s = forall a. HasSimpleRep a => SimpleRep a -> a
fromSimpleRep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasSpec fn a, HasCallStack, MonadGenError m) =>
TypeSpec fn a -> GenT m a
genFromTypeSpec @fn TypeSpec fn a
s

  default conformsTo ::
    ( HasSimpleRep a
    , HasSpec fn (SimpleRep a)
    , TypeSpec fn a ~ TypeSpec fn (SimpleRep a)
    ) =>
    HasCallStack =>
    a ->
    TypeSpec fn a ->
    Bool
  a
a `conformsTo` TypeSpec fn a
s = forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasCallStack) =>
a -> TypeSpec fn a -> Bool
conformsTo @fn (forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep a
a) TypeSpec fn a
s

  default toPreds ::
    ( HasSpec fn (SimpleRep a)
    , TypeSpec fn a ~ TypeSpec fn (SimpleRep a)
    , HasSimpleRep a
    ) =>
    Term fn a ->
    TypeSpec fn a ->
    Pred fn
  toPreds Term fn a
v TypeSpec fn a
s = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> TypeSpec fn a -> Pred fn
toPreds (forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Term fn a -> Term fn (SimpleRep a)
toGeneric_ Term fn a
v) TypeSpec fn a
s

  default shrinkWithTypeSpec ::
    ( HasSpec fn (SimpleRep a)
    , TypeSpec fn a ~ TypeSpec fn (SimpleRep a)
    , HasSimpleRep a
    ) =>
    TypeSpec fn a ->
    a ->
    [a]
  shrinkWithTypeSpec TypeSpec fn a
spec a
a = forall a b. (a -> b) -> [a] -> [b]
map forall a. HasSimpleRep a => SimpleRep a -> a
fromSimpleRep forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> a -> [a]
shrinkWithTypeSpec @fn TypeSpec fn a
spec (forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep a
a)

  default cardinalTypeSpec ::
    (HasSpec fn (SimpleRep a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
    TypeSpec fn a ->
    Specification fn Integer
  cardinalTypeSpec = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn Integer
cardinalTypeSpec @fn @(SimpleRep a)

data WithHasSpec fn f a where
  WithHasSpec :: HasSpec fn a => f a -> WithHasSpec fn f a

-- The Forallable class ---------------------------------------------------

class Forallable t e | t -> e where
  fromForAllSpec ::
    (HasSpec fn t, HasSpec fn e, BaseUniverse fn) => Specification fn e -> Specification fn t
  default fromForAllSpec ::
    ( HasSpec fn t
    , HasSpec fn e
    , HasSimpleRep t
    , TypeSpec fn t ~ TypeSpec fn (SimpleRep t)
    , Forallable (SimpleRep t) e
    , HasSpec fn (SimpleRep t)
    ) =>
    Specification fn e ->
    Specification fn t
  fromForAllSpec Specification fn e
es = forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Specification fn (SimpleRep a) -> Specification fn a
fromSimpleRepSpec forall a b. (a -> b) -> a -> b
$ forall t e (fn :: [*] -> * -> *).
(Forallable t e, HasSpec fn t, HasSpec fn e, BaseUniverse fn) =>
Specification fn e -> Specification fn t
fromForAllSpec @(SimpleRep t) @e Specification fn e
es

  forAllToList :: t -> [e]
  default forAllToList ::
    ( HasSimpleRep t
    , Forallable (SimpleRep t) e
    ) =>
    t ->
    [e]
  forAllToList t
t = forall t e. Forallable t e => t -> [e]
forAllToList (forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep t
t)

-- The HasGenHint class ---------------------------------------------------

-- | Hints are things that only affect generation, and not validation. For instance, parameters to
--   control distribution of generated values.
class (HasSpec fn a, Show (Hint a)) => HasGenHint fn a where
  type Hint a
  giveHint :: Hint a -> Specification fn a

-- Semantics of specs -----------------------------------------------------

{-
conformsToSpecM ::
  forall fn a m. (HasSpec fn a, MonadGenError m, Alternative m) => a -> Specification fn a -> m ()
conformsToSpecM _ TrueSpec = pure ()
conformsToSpecM a (MemberSpec as) = explain1 (show a ++ " not an element of " ++ show as) $ guard $ elem a as
conformsToSpecM a (TypeSpec s cant) = guard $ notElem a cant && conformsTo @fn a s
conformsToSpecM a (SuspendedSpec v ps) = guard =<< checkPred (singletonEnv v a) ps
conformsToSpecM _ (ErrorSpec es) = explain es $ guard False
-}

conformsToSpecM ::
  forall fn a m. (HasSpec fn a, MonadGenError m) => a -> Specification fn a -> m ()
conformsToSpecM :: forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasSpec fn a, MonadGenError m) =>
a -> Specification fn a -> m ()
conformsToSpecM a
a (ExplainSpec [] Specification fn a
s) = forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasSpec fn a, MonadGenError m) =>
a -> Specification fn a -> m ()
conformsToSpecM a
a Specification fn a
s
conformsToSpecM a
a (ExplainSpec ([Char]
x : [[Char]]
xs) Specification fn a
s) = forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a -> m a
explain ([Char]
x forall a. a -> [a] -> NonEmpty a
:| [[Char]]
xs) (forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasSpec fn a, MonadGenError m) =>
a -> Specification fn a -> m ()
conformsToSpecM a
a Specification fn a
s)
conformsToSpecM a
_ Specification fn a
TrueSpec = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
conformsToSpecM a
a (MemberSpec NonEmpty a
as) =
  if forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
a NonEmpty a
as
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    else
      forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a
fatalError
        ( forall a. [a] -> NonEmpty a
NE.fromList
            [[Char]
"conformsToSpecM MemberSpec case", [Char]
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
a, [Char]
"  not an element of", [Char]
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show NonEmpty a
as, [Char]
""]
        )
conformsToSpecM a
a spec :: Specification fn a
spec@(TypeSpec TypeSpec fn a
s OrdSet a
cant) =
  if forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem a
a OrdSet a
cant Bool -> Bool -> Bool
&& forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasCallStack) =>
a -> TypeSpec fn a -> Bool
conformsTo @fn a
a TypeSpec fn a
s
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    else
      forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a
fatalError
        ( forall a. [a] -> NonEmpty a
NE.fromList
            [[Char]
"conformsToSpecM TypeSpec case", [Char]
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
a, [Char]
"  (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Specification fn a
spec forall a. [a] -> [a] -> [a]
++ [Char]
")", [Char]
"fails", [Char]
""]
        )
conformsToSpecM a
a spec :: Specification fn a
spec@(SuspendedSpec Var a
v Pred fn
ps) = do
  Bool
ans <- forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m Bool
checkPred (forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var a
v a
a) Pred fn
ps
  if Bool
ans
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    else
      forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a
fatalError
        ( forall a. [a] -> NonEmpty a
NE.fromList
            [[Char]
"conformsToSpecM SuspendedSpec case", [Char]
"  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
a, [Char]
"  (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Specification fn a
spec forall a. [a] -> [a] -> [a]
++ [Char]
")", [Char]
"fails", [Char]
""]
        )
conformsToSpecM a
_ (ErrorSpec NonEmpty [Char]
es) = forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a
fatalError ([Char]
"conformsToSpecM ErrorSpec case" forall a. a -> NonEmpty a -> NonEmpty a
NE.<| NonEmpty [Char]
es)

conformsToSpecProp :: forall fn a. HasSpec fn a => a -> Specification fn a -> Property
conformsToSpecProp :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Property
conformsToSpecProp a
a Specification fn a
s = forall p. Testable p => GE p -> Property
fromGEProp forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasSpec fn a, MonadGenError m) =>
a -> Specification fn a -> m ()
conformsToSpecM a
a (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Specification fn a
simplifySpec Specification fn a
s)

conformsToSpec :: forall fn a. HasSpec fn a => a -> Specification fn a -> Bool
conformsToSpec :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
conformsToSpec a
a Specification fn a
s = forall a. GE a -> Bool
isOk forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasSpec fn a, MonadGenError m) =>
a -> Specification fn a -> m ()
conformsToSpecM a
a Specification fn a
s

satisfies :: forall fn a. HasSpec fn a => Term fn a -> Specification fn a -> Pred fn
satisfies :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn a
e (ExplainSpec [] Specification fn a
s) = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn a
e Specification fn a
s
satisfies Term fn a
e (ExplainSpec ([Char]
x : [[Char]]
xs) Specification fn a
s) = forall (fn :: [*] -> * -> *). NonEmpty [Char] -> Pred fn -> Pred fn
Explain ([Char]
x forall a. a -> [a] -> NonEmpty a
:| [[Char]]
xs) forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn a
e Specification fn a
s
satisfies Term fn a
_ Specification fn a
TrueSpec = forall (fn :: [*] -> * -> *). Pred fn
TruePred
satisfies Term fn a
e (MemberSpec NonEmpty a
nonempty) = forall (fn :: [*] -> * -> *). NonEmpty [Char] -> Pred fn -> Pred fn
Explain (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Show a => a -> [Char]
show Term fn a
e forall a. [a] -> [a] -> [a]
++ [Char]
" `elem` " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [a]
as)) forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Pred fn
Assert forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
HasSpec fn a =>
Term fn a -> Term fn [a] -> Term fn Bool
elem_ Term fn a
e (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit [a]
as)
  where
    as :: [a]
as = forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
nonempty
satisfies Term fn a
t (SuspendedSpec Var a
x Pred fn
p) = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Term fn a -> Pred fn -> Pred fn
Subst Var a
x Term fn a
t Pred fn
p
satisfies Term fn a
e (TypeSpec TypeSpec fn a
s [a]
cant)
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
cant = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> TypeSpec fn a -> Pred fn
toPreds Term fn a
e TypeSpec fn a
s
  | Bool
otherwise =
      forall (fn :: [*] -> * -> *). NonEmpty [Char] -> Pred fn -> Pred fn
Explain (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Show a => a -> [Char]
show Term fn a
e forall a. [a] -> [a] -> [a]
++ [Char]
" `notElem` " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [a]
cant)) (forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Pred fn
Assert (forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ (forall a (fn :: [*] -> * -> *).
HasSpec fn a =>
Term fn a -> Term fn [a] -> Term fn Bool
elem_ Term fn a
e forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit [a]
cant)))
        forall a. Semigroup a => a -> a -> a
<> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> TypeSpec fn a -> Pred fn
toPreds Term fn a
e TypeSpec fn a
s
satisfies Term fn a
_ (ErrorSpec NonEmpty [Char]
e) = forall (fn :: [*] -> * -> *). NonEmpty [Char] -> Pred fn
FalsePred NonEmpty [Char]
e

------------------------------------------------------------------------
-- Generating things
------------------------------------------------------------------------

-- Generating things from specs -------------------------------------------

-- | Generate a value that satisfies the spec. This function can fail if the
-- spec is inconsistent, there is a dependency error, or if the underlying
-- generators are not flexible enough.
genFromSpecT ::
  forall fn a m. (HasCallStack, HasSpec fn a, MonadGenError m) => Specification fn a -> GenT m a
genFromSpecT :: forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Specification fn a
simplifySpec -> Specification fn a
spec) = case Specification fn a
spec of
  ExplainSpec [] Specification fn a
s -> forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT Specification fn a
s
  ExplainSpec [[Char]]
es Specification fn a
s -> forall (m :: * -> *) a.
MonadGenError m =>
[[Char]] -> GenT GE a -> GenT m a
push [[Char]]
es (forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT Specification fn a
s)
  MemberSpec NonEmpty a
as -> forall (m :: * -> *) a. MonadGenError m => [Char] -> m a -> m a
explain1 ([Char]
"genFromSpecT on spec" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Specification fn a
spec) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Applicative m => Gen a -> GenT m a
pureGen (forall a. HasCallStack => [a] -> Gen a
elements (forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as))
  Specification fn a
TrueSpec -> forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT @fn (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a
emptySpec @fn @a)
  SuspendedSpec Var a
x Pred fn
p
    -- NOTE: If `x` isn't free in `p` we still have to try to generate things
    -- from `p` to make sure `p` is sat and then we can throw it away. A better
    -- approach would be to only do this in the case where we don't know if `p`
    -- is sat. The proper way to implement such a sat check is to remove
    -- sat-but-unnecessary variables in the optimiser.
    | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a. HasSpec fn a => Var a -> Name fn
Name Var a
x forall (fn :: [*] -> * -> *) a.
HasVariables fn a =>
Name fn -> a -> Bool
`appearsIn` Pred fn
p -> do
        !Env
_ <- forall (fn :: [*] -> * -> *) (m :: * -> *).
(MonadGenError m, BaseUniverse fn) =>
Env -> Pred fn -> GenT m Env
genFromPreds forall a. Monoid a => a
mempty Pred fn
p
        forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT @fn forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
    | Bool
otherwise -> do
        Env
env <- forall (fn :: [*] -> * -> *) (m :: * -> *).
(MonadGenError m, BaseUniverse fn) =>
Env -> Pred fn -> GenT m Env
genFromPreds forall a. Monoid a => a
mempty Pred fn
p
        forall a (m :: * -> *).
(Typeable a, MonadGenError m) =>
Env -> Var a -> m a
findEnv Env
env Var a
x
  TypeSpec TypeSpec fn a
s OrdSet a
cant -> do
    GenMode
mode <- forall (m :: * -> *). Applicative m => GenT m GenMode
getMode
    forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a -> m a
explain
      ( forall a. [a] -> NonEmpty a
NE.fromList
          [ [Char]
"genFromSpecT at type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep OrdSet a
cant)
          , [Char]
"    " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Specification fn a
spec
          , [Char]
"  with mode " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show GenMode
mode
          , [Char]
"  cant set " forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unlines (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> [Char]
show OrdSet a
cant)
          ]
      )
      forall a b. (a -> b) -> a -> b
$
      -- TODO: we could consider giving `cant` as an argument to `genFromTypeSpec` if this
      -- starts giving us trouble.
      forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasSpec fn a, HasCallStack, MonadGenError m) =>
TypeSpec fn a -> GenT m a
genFromTypeSpec @fn TypeSpec fn a
s forall (m :: * -> *) a.
MonadGenError m =>
GenT m a -> (a -> Bool) -> GenT m a
`suchThatT` (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` OrdSet a
cant)
  ErrorSpec NonEmpty [Char]
e -> forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a
genError NonEmpty [Char]
e

shrinkWithSpec :: forall fn a. HasSpec fn a => Specification fn a -> a -> [a]
-- TODO: possibly allow for ignoring the `conformsToSpec` check in the `TypeSpec`
-- case when you know what you're doing
shrinkWithSpec :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> Specification fn a
simplifySpec -> Specification fn a
spec) a
a = forall a. (a -> Bool) -> [a] -> [a]
filter (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn a
spec) forall a b. (a -> b) -> a -> b
$ case Specification fn a
spec of
  ExplainSpec [[Char]]
_ Specification fn a
s -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec Specification fn a
s a
a
  -- TODO: filter on can't if we have a known to be sound shrinker
  TypeSpec TypeSpec fn a
s [a]
_ -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> a -> [a]
shrinkWithTypeSpec @fn TypeSpec fn a
s a
a
  -- TODO: The better way of doing this is to compute the dependency graph,
  -- shrink one variable at a time, and fixup the rest of the variables
  SuspendedSpec {} -> a -> [a]
shr a
a
  MemberSpec {} -> a -> [a]
shr a
a
  Specification fn a
TrueSpec -> a -> [a]
shr a
a
  ErrorSpec {} -> []
  where
    shr :: a -> [a]
shr = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> a -> [a]
shrinkWithTypeSpec @fn (forall (fn :: [*] -> * -> *) a. HasSpec fn a => TypeSpec fn a
emptySpec @fn @a)

shrinkFromPreds :: HasSpec fn a => Pred fn -> Var a -> a -> [a]
shrinkFromPreds :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Pred fn -> Var a -> a -> [a]
shrinkFromPreds Pred fn
p
  | Result [NonEmpty [Char]]
_ SolverPlan fn
plan <- forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Pred fn -> GE (SolverPlan fn)
prepareLinearization Pred fn
p = \Var a
x a
a -> forall a. GE [a] -> [a]
listFromGE forall a b. (a -> b) -> a -> b
$ do
      -- NOTE: we do this to e.g. guard against bad construction functions in Exists
      Bool
xaGood <- forall (fn :: [*] -> * -> *) (m :: * -> *).
(FunctionLike fn, MonadGenError m) =>
Env -> Pred fn -> m Bool
checkPred (forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var a
x a
a) Pred fn
p
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
xaGood forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a. MonadGenError m => [Char] -> m a
fatalError1 [Char]
"Trying to shrink a bad value, don't do that!"
      -- Get an `env` for the original value
      Env
initialEnv <- forall (fn :: [*] -> * -> *). Env -> Pred fn -> GE Env
envFromPred (forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var a
x a
a) Pred fn
p
      forall (m :: * -> *) a. Monad m => a -> m a
return
        [ a
a'
        | -- Shrink the initialEnv
        Env
env' <- forall (fn :: [*] -> * -> *). Env -> SolverPlan fn -> [Env]
shrinkEnvFromPlan Env
initialEnv SolverPlan fn
plan
        , -- Get the value of the constrained variable `x` in the shrunk env
        Just a
a' <- [forall a. Typeable a => Env -> Var a -> Maybe a
lookupEnv Env
env' Var a
x]
        , -- NOTE: this is necessary because it's possible that changing
        -- a particular value in the env during shrinking might not result
        -- in the value of `x` changing and there is no better way to know than
        -- to do this.
        a
a' forall a. Eq a => a -> a -> Bool
/= a
a
        ]
  | Bool
otherwise = forall a. HasCallStack => [Char] -> a
error [Char]
"Bad pred"

-- Start with a valid Env for the plan and try to shrink it
shrinkEnvFromPlan :: Env -> SolverPlan fn -> [Env]
shrinkEnvFromPlan :: forall (fn :: [*] -> * -> *). Env -> SolverPlan fn -> [Env]
shrinkEnvFromPlan Env
initialEnv SolverPlan {[SolverStage fn]
Graph (Name fn)
solverDependencies :: forall (fn :: [*] -> * -> *). SolverPlan fn -> Graph (Name fn)
solverPlan :: forall (fn :: [*] -> * -> *). SolverPlan fn -> [SolverStage fn]
solverDependencies :: Graph (Name fn)
solverPlan :: [SolverStage fn]
..} = Env -> [SolverStage fn] -> [Env]
go forall a. Monoid a => a
mempty [SolverStage fn]
solverPlan
  where
    go :: Env -> [SolverStage fn] -> [Env]
go Env
_ [] = [] -- In this case we decided to keep every variable the same so nothing to return
    go Env
env ((forall (fn :: [*] -> * -> *).
Env -> SolverStage fn -> SolverStage fn
substStage Env
env -> SolverStage {[Pred fn]
Var a
Specification fn a
stageSpec :: ()
stagePreds :: forall (fn :: [*] -> * -> *). SolverStage fn -> [Pred fn]
stageVar :: ()
stageSpec :: Specification fn a
stagePreds :: [Pred fn]
stageVar :: Var a
..}) : [SolverStage fn]
plan) = do
      Just a
a <- [forall a. Typeable a => Env -> Var a -> Maybe a
lookupEnv Env
initialEnv Var a
stageVar]
      -- Two cases:
      --  - either we shrink this value and try to fixup every value later on in the plan or
      [ Env
env' forall a. Semigroup a => a -> a -> a
<> Env
fixedEnv
        | a
a' <- forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec Specification fn a
stageSpec a
a
        , let env' :: Env
env' = forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
stageVar a
a' Env
env
        , Just Env
fixedEnv <- [Env -> [SolverStage fn] -> Maybe Env
fixupPlan Env
env' [SolverStage fn]
plan]
        ]
        --  - we keep this value the way it is and try to shrink some later value
        forall a. [a] -> [a] -> [a]
++ Env -> [SolverStage fn] -> [Env]
go (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
stageVar a
a Env
env) [SolverStage fn]
plan

    -- Fix the rest of the plan given an environment `env` for the plan so far
    fixupPlan :: Env -> [SolverStage fn] -> Maybe Env
fixupPlan Env
env [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
    fixupPlan Env
env ((forall (fn :: [*] -> * -> *).
Env -> SolverStage fn -> SolverStage fn
substStage Env
env -> SolverStage {[Pred fn]
Var a
Specification fn a
stageSpec :: Specification fn a
stagePreds :: [Pred fn]
stageVar :: Var a
stageSpec :: ()
stagePreds :: forall (fn :: [*] -> * -> *). SolverStage fn -> [Pred fn]
stageVar :: ()
..}) : [SolverStage fn]
plan) =
      case forall a. Typeable a => Env -> Var a -> Maybe a
lookupEnv Env
initialEnv Var a
stageVar forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> Maybe a
fixupWithSpec Specification fn a
stageSpec of
        Maybe a
Nothing -> forall a. Maybe a
Nothing
        Just a
a -> Env -> [SolverStage fn] -> Maybe Env
fixupPlan (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
stageVar a
a Env
env) [SolverStage fn]
plan

-- Try to fix a value w.r.t a specification
fixupWithSpec :: forall fn a. HasSpec fn a => Specification fn a -> a -> Maybe a
fixupWithSpec :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> Maybe a
fixupWithSpec Specification fn a
spec a
a
  | a
a forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn a
spec = forall a. a -> Maybe a
Just a
a
  | Bool
otherwise = case Specification fn a
spec of
      MemberSpec (a
a :| [a]
_) -> forall a. a -> Maybe a
Just a
a
      Specification fn a
_ -> forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn a
spec) (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn a -> a -> [a]
shrinkWithSpec @fn forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec a
a)

-- Construct an environment for all variables that show up on the top level
-- (i.e. ones bound in `let` and `exists`) from an environment for all the free
-- variables in the pred. The environment you get out of this function is
-- _bigger_ than the environment you put in. From
-- ```
-- let y = x + 1 in let z = y + 1 in foo x y z
-- ```
-- and an environment with `{x -> 1}` you would get `{x -> 1, y -> 2, z -> 3}`
-- out.
envFromPred :: Env -> Pred fn -> GE Env
envFromPred :: forall (fn :: [*] -> * -> *). Env -> Pred fn -> GE Env
envFromPred Env
env Pred fn
p = case Pred fn
p of
  -- NOTE: these don't bind anything
  Assert {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  DependsOn {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  Monitor {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  TruePred {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  FalsePred {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  GenHint {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  -- NOTE: this is ok because the variables either come from an `Exists`, a `Let`, or from
  -- the top level
  Reifies {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  -- NOTE: variables in here shouldn't escape to the top level
  ForAll {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  Case {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  -- These can introduce binders that show up in the plan
  When Term fn Bool
_ Pred fn
p -> forall (fn :: [*] -> * -> *). Env -> Pred fn -> GE Env
envFromPred Env
env Pred fn
p
  Subst Var a
x Term fn a
a Pred fn
p -> forall (fn :: [*] -> * -> *). Env -> Pred fn -> GE Env
envFromPred Env
env (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Term fn a -> Pred fn -> Pred fn
substitutePred Var a
x Term fn a
a Pred fn
p)
  Let Term fn a
t (Var a
x :-> Pred fn
p) -> do
    a
v <- forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env Term fn a
t
    forall (fn :: [*] -> * -> *). Env -> Pred fn -> GE Env
envFromPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
v Env
env) Pred fn
p
  Explain NonEmpty [Char]
_ Pred fn
p -> forall (fn :: [*] -> * -> *). Env -> Pred fn -> GE Env
envFromPred Env
env Pred fn
p
  Exists (forall b. Term fn b -> b) -> GE a
c (Var a
x :-> Pred fn
p) -> do
    a
v <- (forall b. Term fn b -> b) -> GE a
c (forall a. GE a -> a
errorGE forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadGenError m => [Char] -> m a -> m a
explain1 [Char]
"envFromPred: Exists" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm Env
env)
    forall (fn :: [*] -> * -> *). Env -> Pred fn -> GE Env
envFromPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
v Env
env) Pred fn
p
  Block [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  Block (Pred fn
p : [Pred fn]
ps) -> do
    Env
env' <- forall (fn :: [*] -> * -> *). Env -> Pred fn -> GE Env
envFromPred Env
env Pred fn
p
    forall (fn :: [*] -> * -> *). Env -> Pred fn -> GE Env
envFromPred Env
env' (forall (fn :: [*] -> * -> *). [Pred fn] -> Pred fn
Block [Pred fn]
ps)

-- | A version of `genFromSpecT` that simply errors if the generator fails
genFromSpec :: forall fn a. (HasCallStack, HasSpec fn a) => Specification fn a -> Gen a
genFromSpec :: forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec Specification fn a
spec = do
  GE a
res <- forall (m :: * -> *) a. GenT m a -> Gen (m a)
strictGen forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadGenError m => [Char] -> m a -> m a
explain1 [Char]
"Calling genFromSpec" forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT Specification fn a
spec
  forall a. GE a -> a
errorGE forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) a. Applicative f => a -> f a
pure GE a
res

-- | A version of `genFromSpecT` that takes a seed and a size and gives you a result
genFromSpecWithSeed ::
  forall fn a. (HasCallStack, HasSpec fn a) => Int -> Int -> Specification fn a -> a
genFromSpecWithSeed :: forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Int -> Int -> Specification fn a -> a
genFromSpecWithSeed Int
seed Int
size Specification fn a
spec = forall a. Gen a -> QCGen -> Int -> a
unGen (forall (fn :: [*] -> * -> *) a.
(HasCallStack, HasSpec fn a) =>
Specification fn a -> Gen a
genFromSpec Specification fn a
spec) (Int -> QCGen
mkQCGen Int
seed) Int
size

genInverse ::
  ( MonadGenError m
  , HasSpec fn a
  , Show b
  , Functions fn fn
  , HasSpec fn b
  ) =>
  fn '[a] b ->
  Specification fn a ->
  b ->
  GenT m a
genInverse :: forall (m :: * -> *) (fn :: [*] -> * -> *) a b.
(MonadGenError m, HasSpec fn a, Show b, Functions fn fn,
 HasSpec fn b) =>
fn '[a] b -> Specification fn a -> b -> GenT m a
genInverse fn '[a] b
f Specification fn a
argS b
x =
  let argSpec' :: Specification fn a
argSpec' = Specification fn a
argS forall a. Semigroup a => a -> a -> a
<> forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) a b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn a,
 HasSpec fn b, All (HasSpec fn) as) =>
f as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun fn '[a] b
f (forall (c :: * -> *) a (f :: * -> *). c a -> ListCtx f '[a] c
NilCtx forall a. HOLE a a
HOLE) (forall a (fn :: [*] -> * -> *). a -> Specification fn a
equalSpec b
x)
   in forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a -> m a
explain
        ( forall a. [a] -> NonEmpty a
NE.fromList
            [ [Char]
"genInverse"
            , [Char]
"  f = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show fn '[a] b
f
            , forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Doc Any
"  argS =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Specification fn a
argS
            , [Char]
"  x = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show b
x
            , forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Doc Any
"  argSpec' =" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Specification fn a
argSpec'
            ]
        )
        forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a (m :: * -> *).
(HasCallStack, HasSpec fn a, MonadGenError m) =>
Specification fn a -> GenT m a
genFromSpecT Specification fn a
argSpec'

-- Generating things from predicates --------------------------------------

-- | Flatten nested `Let`, `Exists`, and `Block` in a `Pred fn`. `Let` and
-- `Exists` bound variables become free in the result.
flattenPred :: forall fn. BaseUniverse fn => Pred fn -> [Pred fn]
flattenPred :: forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Pred fn -> [Pred fn]
flattenPred Pred fn
pIn = Set Int -> [Pred fn] -> [Pred fn]
go (forall (fn :: [*] -> * -> *) t. HasVariables fn t => t -> Set Int
freeVarNames Pred fn
pIn) [Pred fn
pIn]
  where
    go :: Set Int -> [Pred fn] -> [Pred fn]
go Set Int
_ [] = []
    go Set Int
fvs (Pred fn
p : [Pred fn]
ps) = case Pred fn
p of
      Block [Pred fn]
ps' -> Set Int -> [Pred fn] -> [Pred fn]
go Set Int
fvs ([Pred fn]
ps' forall a. [a] -> [a] -> [a]
++ [Pred fn]
ps)
      -- NOTE: the order of the arguments to `==.` here are important.
      -- The whole point of `Let` is that it allows us to solve all of `t`
      -- before we solve the variables in `t`.
      Let Term fn a
t Binder fn a
b -> forall a.
Set Int
-> Binder fn a
-> [Pred fn]
-> (HasSpec fn a => Var a -> [Pred fn] -> [Pred fn])
-> [Pred fn]
goBinder Set Int
fvs Binder fn a
b [Pred fn]
ps (\Var a
x -> (forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert (Term fn a
t forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: [*] -> * -> *) a. HasSpec fn a => Var a -> Term fn a
V Var a
x) forall a. a -> [a] -> [a]
:))
      Exists (forall b. Term fn b -> b) -> GE a
_ Binder fn a
b -> forall a.
Set Int
-> Binder fn a
-> [Pred fn]
-> (HasSpec fn a => Var a -> [Pred fn] -> [Pred fn])
-> [Pred fn]
goBinder Set Int
fvs Binder fn a
b [Pred fn]
ps (forall a b. a -> b -> a
const forall a. a -> a
id)
      When Term fn Bool
b Pred fn
p -> forall a b. (a -> b) -> [a] -> [b]
map (forall (fn :: [*] -> * -> *).
HasSpec fn Bool =>
Term fn Bool -> Pred fn -> Pred fn
When Term fn Bool
b) (Set Int -> [Pred fn] -> [Pred fn]
go Set Int
fvs [Pred fn
p]) forall a. [a] -> [a] -> [a]
++ Set Int -> [Pred fn] -> [Pred fn]
go Set Int
fvs [Pred fn]
ps
      Explain NonEmpty [Char]
es Pred fn
p -> forall a b. (a -> b) -> [a] -> [b]
map (forall (fn :: [*] -> * -> *). NonEmpty [Char] -> Pred fn -> Pred fn
explanation NonEmpty [Char]
es) (Set Int -> [Pred fn] -> [Pred fn]
go Set Int
fvs [Pred fn
p]) forall a. [a] -> [a] -> [a]
++ Set Int -> [Pred fn] -> [Pred fn]
go Set Int
fvs [Pred fn]
ps
      Pred fn
_ -> Pred fn
p forall a. a -> [a] -> [a]
: Set Int -> [Pred fn] -> [Pred fn]
go Set Int
fvs [Pred fn]
ps

    goBinder ::
      Set Int ->
      Binder fn a ->
      [Pred fn] ->
      (HasSpec fn a => Var a -> [Pred fn] -> [Pred fn]) ->
      [Pred fn]
    goBinder :: forall a.
Set Int
-> Binder fn a
-> [Pred fn]
-> (HasSpec fn a => Var a -> [Pred fn] -> [Pred fn])
-> [Pred fn]
goBinder Set Int
fvs (Var a
x :-> Pred fn
p) [Pred fn]
ps HasSpec fn a => Var a -> [Pred fn] -> [Pred fn]
k = HasSpec fn a => Var a -> [Pred fn] -> [Pred fn]
k Var a
x' forall a b. (a -> b) -> a -> b
$ Set Int -> [Pred fn] -> [Pred fn]
go (forall a. Ord a => a -> Set a -> Set a
Set.insert (forall a. Var a -> Int
nameOf Var a
x') Set Int
fvs) (Pred fn
p' forall a. a -> [a] -> [a]
: [Pred fn]
ps)
      where
        (Var a
x', Pred fn
p') = forall a t.
(Typeable a, Rename t) =>
Var a -> t -> Set Int -> (Var a, t)
freshen Var a
x Pred fn
p Set Int
fvs

computeDependencies :: Pred fn -> DependGraph fn
computeDependencies :: forall (fn :: [*] -> * -> *). Pred fn -> DependGraph fn
computeDependencies = \case
  Monitor {} -> forall a. Monoid a => a
mempty
  Subst Var a
x Term fn a
t Pred fn
p -> forall (fn :: [*] -> * -> *). Pred fn -> DependGraph fn
computeDependencies (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Term fn a -> Pred fn -> Pred fn
substitutePred Var a
x Term fn a
t Pred fn
p)
  Assert Term fn Bool
t -> forall (fn :: [*] -> * -> *) a. Term fn a -> DependGraph fn
computeTermDependencies Term fn Bool
t
  Reifies Term fn b
t' Term fn a
t a -> b
_ -> Term fn b
t' forall (fn :: [*] -> * -> *) t t'.
(HasVariables fn t, HasVariables fn t') =>
t -> t' -> DependGraph fn
`irreflexiveDependencyOn` Term fn a
t
  ForAll Term fn t
set Binder fn a
b ->
    let innerG :: DependGraph fn
innerG = forall (fn :: [*] -> * -> *) a. Binder fn a -> DependGraph fn
computeBinderDependencies Binder fn a
b
     in DependGraph fn
innerG forall a. Semigroup a => a -> a -> a
<> Term fn t
set forall (fn :: [*] -> * -> *) t t'.
(HasVariables fn t, HasVariables fn t') =>
t -> t' -> DependGraph fn
`irreflexiveDependencyOn` forall node. Graph node -> Set node
nodes DependGraph fn
innerG
  Term fn a
x `DependsOn` Term fn b
y -> Term fn a
x forall (fn :: [*] -> * -> *) t t'.
(HasVariables fn t, HasVariables fn t') =>
t -> t' -> DependGraph fn
`irreflexiveDependencyOn` Term fn b
y
  Case Term fn (SumOver as)
t List (Weighted (Binder fn)) as
bs ->
    let innerG :: DependGraph fn
innerG = forall {k} b (f :: k -> *) (as :: [k]).
Monoid b =>
(forall (a :: k). f a -> b) -> List f as -> b
foldMapList (forall (fn :: [*] -> * -> *) a. Binder fn a -> DependGraph fn
computeBinderDependencies forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Weighted f a -> f a
thing) List (Weighted (Binder fn)) as
bs
     in DependGraph fn
innerG forall a. Semigroup a => a -> a -> a
<> Term fn (SumOver as)
t forall (fn :: [*] -> * -> *) t t'.
(HasVariables fn t, HasVariables fn t') =>
t -> t' -> DependGraph fn
`irreflexiveDependencyOn` forall node. Graph node -> Set node
nodes DependGraph fn
innerG
  When Term fn Bool
b Pred fn
p ->
    let pG :: DependGraph fn
pG = forall (fn :: [*] -> * -> *). Pred fn -> DependGraph fn
computeDependencies Pred fn
p
        oG :: DependGraph fn
oG = forall node. Graph node -> Set node
nodes DependGraph fn
pG forall (fn :: [*] -> * -> *) t t'.
(HasVariables fn t, HasVariables fn t') =>
t -> t' -> DependGraph fn
`irreflexiveDependencyOn` Term fn Bool
b
     in DependGraph fn
oG forall a. Semigroup a => a -> a -> a
<> DependGraph fn
pG
  Pred fn
TruePred -> forall a. Monoid a => a
mempty
  FalsePred {} -> forall a. Monoid a => a
mempty
  Block [Pred fn]
ps -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall (fn :: [*] -> * -> *). Pred fn -> DependGraph fn
computeDependencies [Pred fn]
ps
  Exists (forall b. Term fn b -> b) -> GE a
_ Binder fn a
b -> forall (fn :: [*] -> * -> *) a. Binder fn a -> DependGraph fn
computeBinderDependencies Binder fn a
b
  Let Term fn a
t Binder fn a
b -> forall (fn :: [*] -> * -> *) t.
HasVariables fn t =>
t -> DependGraph fn
noDependencies Term fn a
t forall a. Semigroup a => a -> a -> a
<> forall (fn :: [*] -> * -> *) a. Binder fn a -> DependGraph fn
computeBinderDependencies Binder fn a
b
  GenHint Hint a
_ Term fn a
t -> forall (fn :: [*] -> * -> *) t.
HasVariables fn t =>
t -> DependGraph fn
noDependencies Term fn a
t
  Explain NonEmpty [Char]
_ Pred fn
p -> forall (fn :: [*] -> * -> *). Pred fn -> DependGraph fn
computeDependencies Pred fn
p

data SolverStage fn where
  SolverStage ::
    HasSpec fn a =>
    { ()
stageVar :: Var a
    , forall (fn :: [*] -> * -> *). SolverStage fn -> [Pred fn]
stagePreds :: [Pred fn]
    , ()
stageSpec :: Specification fn a
    } ->
    SolverStage fn

instance Pretty (SolverStage fn) where
  pretty :: forall ann. SolverStage fn -> Doc ann
pretty SolverStage {[Pred fn]
Var a
Specification fn a
stageSpec :: Specification fn a
stagePreds :: [Pred fn]
stageVar :: Var a
stageSpec :: ()
stagePreds :: forall (fn :: [*] -> * -> *). SolverStage fn -> [Pred fn]
stageVar :: ()
..} =
    (Doc ann
"\nSolving for variable " forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Show a => a -> Doc ann
viaShow Var a
stageVar)
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"<-"
        forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [Doc ann] -> Doc ann
vsep'
          ( [forall a ann. Pretty a => a -> Doc ann
pretty Specification fn a
stageSpec | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a. Specification fn a -> Bool
isTrueSpec Specification fn a
stageSpec]
              forall a. [a] -> [a] -> [a]
++ [Doc ann
"---" | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pred fn]
stagePreds, Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a. Specification fn a -> Bool
isTrueSpec Specification fn a
stageSpec]
              forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [Pred fn]
stagePreds
          )

data SolverPlan fn = SolverPlan
  { forall (fn :: [*] -> * -> *). SolverPlan fn -> [SolverStage fn]
solverPlan :: [SolverStage fn]
  , forall (fn :: [*] -> * -> *). SolverPlan fn -> Graph (Name fn)
solverDependencies :: Graph (Name fn)
  }

instance Pretty (SolverPlan fn) where
  pretty :: forall ann. SolverPlan fn -> Doc ann
pretty SolverPlan {[SolverStage fn]
Graph (Name fn)
solverDependencies :: Graph (Name fn)
solverPlan :: [SolverStage fn]
solverDependencies :: forall (fn :: [*] -> * -> *). SolverPlan fn -> Graph (Name fn)
solverPlan :: forall (fn :: [*] -> * -> *). SolverPlan fn -> [SolverStage fn]
..} =
    Doc ann
"\nSolverPlan"
      forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [Doc ann] -> Doc ann
vsep'
        [ -- "\nDependencies:" /> pretty solverDependencies, -- Might be usefull someday
          Doc ann
"\nLinearization:" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall (fn :: [*] -> * -> *) ann. [SolverStage fn] -> Doc ann
prettyLinear [SolverStage fn]
solverPlan
        ]

isTrueSpec :: Specification fn a -> Bool
isTrueSpec :: forall (fn :: [*] -> * -> *) a. Specification fn a -> Bool
isTrueSpec Specification fn a
TrueSpec = Bool
True
isTrueSpec Specification fn a
_ = Bool
False

prettyLinear :: [SolverStage fn] -> Doc ann
prettyLinear :: forall (fn :: [*] -> * -> *) ann. [SolverStage fn] -> Doc ann
prettyLinear = forall ann. [Doc ann] -> Doc ann
vsep' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty

-- | Linearize a predicate, turning it into a list of variables to solve and
-- their defining constraints such that each variable can be solved independently.
prepareLinearization ::
  forall fn. BaseUniverse fn => Pred fn -> GE (SolverPlan fn)
prepareLinearization :: forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Pred fn -> GE (SolverPlan fn)
prepareLinearization Pred fn
p = do
  let preds :: [Pred fn]
preds = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {fn :: [*] -> * -> *}. Pred fn -> [Pred fn]
saturatePred forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Pred fn -> [Pred fn]
flattenPred Pred fn
p
      hints :: Hints fn
hints = forall (fn :: [*] -> * -> *). [Pred fn] -> Hints fn
computeHints [Pred fn]
preds
      graph :: Hints fn
graph = forall node. Ord node => Graph node -> Graph node
transitiveClosure forall a b. (a -> b) -> a -> b
$ Hints fn
hints forall a. Semigroup a => a -> a -> a
<> forall (f :: [*] -> * -> *). Hints f -> Hints f -> Hints f
respecting Hints fn
hints (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall (fn :: [*] -> * -> *). Pred fn -> DependGraph fn
computeDependencies [Pred fn]
preds)
  [SolverStage fn]
plan <-
    forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty [Char] -> m a -> m a
explain
      ( forall a. [a] -> NonEmpty a
NE.fromList
          [ [Char]
"Linearizing"
          , forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Doc Any
"  preds: " forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty [Pred fn]
preds
          , forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ Doc Any
"  graph: " forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Hints fn
graph
          ]
      )
      forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (fn :: [*] -> * -> *).
(MonadGenError m, BaseUniverse fn) =>
[Pred fn] -> DependGraph fn -> m [SolverStage fn]
linearize [Pred fn]
preds Hints fn
graph
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *). SolverPlan fn -> SolverPlan fn
backPropagation forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *).
[SolverStage fn] -> Graph (Name fn) -> SolverPlan fn
SolverPlan [SolverStage fn]
plan Hints fn
graph

-- TODO: generalize this to make it more flexible and extensible
--
-- The idea here is that we turn constraints into _extra_ constraints. C.f. the
-- `mapIsJust` example in `Constrained.Examples.Map`:

--    mapIsJust :: Specification BaseFn (Int, Int)
--    mapIsJust = constrained' $ \ [var| x |] [var| y |] ->
--      assert $ cJust_ x ==. lookup_ y (lit $ Map.fromList [(z, z) | z <- [100 .. 102]])

-- Without this code the example wouldn't work because `y` is completely unconstrained during
-- generation. With this code we essentially rewrite occurences of `cJust_ A == B` to
-- `[cJust A == B, case B of Nothing -> False; Just _ -> True]` to add extra information
-- about the variables in `B`. Consequently, `y` in the example above is
-- constrained to `MemberSpec [100 .. 102]` in the plan.
saturatePred :: forall fn. Pred fn -> [Pred fn]
saturatePred :: forall {fn :: [*] -> * -> *}. Pred fn -> [Pred fn]
saturatePred Pred fn
p =
  Pred fn
p -- <--- if there is an Explain, it is still on 'p' here
    forall a. a -> [a] -> [a]
: case Pred fn
p of
      Explain NonEmpty [Char]
_es Pred fn
x -> forall {fn :: [*] -> * -> *}. Pred fn -> [Pred fn]
saturatePred Pred fn
x -- Note that the Explain is still on the original 'p', so it is not lost
      Assert (Eql (FromG (SLeft Term fn b
_)) Term fn a
t) ->
        [forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> TypeSpec fn a -> Pred fn
toPreds Term fn a
t (forall (fn :: [*] -> * -> *) a b.
Maybe (Int, Int)
-> Specification fn a -> Specification fn b -> SumSpec fn a b
SumSpec forall a. Maybe a
Nothing forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec (forall (fn :: [*] -> * -> *) a.
NonEmpty [Char] -> Specification fn a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure [Char]
"saturatePred")))]
      Assert (Eql (FromG (SRight Term fn c
_)) Term fn a
t) ->
        [forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> TypeSpec fn a -> Pred fn
toPreds Term fn a
t (forall (fn :: [*] -> * -> *) a b.
Maybe (Int, Int)
-> Specification fn a -> Specification fn b -> SumSpec fn a b
SumSpec forall a. Maybe a
Nothing (forall (fn :: [*] -> * -> *) a.
NonEmpty [Char] -> Specification fn a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure [Char]
"saturatePred")) forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec)]
      -- TODO: e.g. `elem (pair x y) (lit zs) -> elem x (lit $ map fst zs)` etc.
      Pred fn
_ -> []

-- | Does nothing if the variable is not in the plan already.
mergeSolverStage :: SolverStage fn -> [SolverStage fn] -> [SolverStage fn]
mergeSolverStage :: forall (fn :: [*] -> * -> *).
SolverStage fn -> [SolverStage fn] -> [SolverStage fn]
mergeSolverStage (SolverStage Var a
x [Pred fn]
ps Specification fn a
spec) [SolverStage fn]
plan =
  [ case forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
x Var a
y of
      Just a :~: a
Refl ->
        forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> [Pred fn] -> Specification fn a -> SolverStage fn
SolverStage
          Var a
y
          ([Pred fn]
ps forall a. [a] -> [a] -> [a]
++ [Pred fn]
ps')
          ( forall (fn :: [*] -> * -> *) a.
NonEmpty [Char] -> Specification fn a -> Specification fn a
addToErrorSpec
              ( forall a. [a] -> NonEmpty a
NE.fromList
                  ( [ [Char]
"Solving var " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Var a
x forall a. [a] -> [a] -> [a]
++ [Char]
" fails."
                    , [Char]
"Merging the Specs"
                    , [Char]
"   1. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Specification fn a
spec
                    , [Char]
"   2. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Specification fn a
spec'
                    ]
                  )
              )
              (Specification fn a
spec forall a. Semigroup a => a -> a -> a
<> Specification fn a
spec')
          )
      Maybe (a :~: a)
Nothing -> SolverStage fn
stage
  | stage :: SolverStage fn
stage@(SolverStage Var a
y [Pred fn]
ps' Specification fn a
spec') <- [SolverStage fn]
plan
  ]

-- | Push as much information we can backwards through the plan.
backPropagation :: forall fn. SolverPlan fn -> SolverPlan fn
backPropagation :: forall (fn :: [*] -> * -> *). SolverPlan fn -> SolverPlan fn
backPropagation (SolverPlan [SolverStage fn]
plan Graph (Name fn)
graph) = forall (fn :: [*] -> * -> *).
[SolverStage fn] -> Graph (Name fn) -> SolverPlan fn
SolverPlan ([SolverStage fn] -> [SolverStage fn] -> [SolverStage fn]
go [] (forall a. [a] -> [a]
reverse [SolverStage fn]
plan)) Graph (Name fn)
graph
  where
    go :: [SolverStage fn] -> [SolverStage fn] -> [SolverStage fn]
go [SolverStage fn]
acc [] = [SolverStage fn]
acc
    go [SolverStage fn]
acc (s :: SolverStage fn
s@(SolverStage (Var a
x :: Var a) [Pred fn]
ps Specification fn a
spec) : [SolverStage fn]
plan) = [SolverStage fn] -> [SolverStage fn] -> [SolverStage fn]
go (SolverStage fn
s forall a. a -> [a] -> [a]
: [SolverStage fn]
acc) [SolverStage fn]
plan'
      where
        newStages :: [SolverStage fn]
newStages = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Specification fn a -> Pred fn -> [SolverStage fn]
newStage Specification fn a
spec) [Pred fn]
ps
        plan' :: [SolverStage fn]
plan' = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall (fn :: [*] -> * -> *).
SolverStage fn -> [SolverStage fn] -> [SolverStage fn]
mergeSolverStage [SolverStage fn]
plan [SolverStage fn]
newStages

        newStage :: Specification fn a -> Pred fn -> [SolverStage fn]
newStage Specification fn a
spec (Assert (Eql (V Var a
x') Term fn a
t)) =
          forall b.
HasSpec fn b =>
Specification fn a -> Var b -> Term fn b -> [SolverStage fn]
termVarEqCases Specification fn a
spec Var a
x' Term fn a
t
        newStage Specification fn a
spec (Assert (Eql Term fn a
t (V Var a
x'))) =
          forall b.
HasSpec fn b =>
Specification fn a -> Var b -> Term fn b -> [SolverStage fn]
termVarEqCases Specification fn a
spec Var a
x' Term fn a
t
        newStage Specification fn a
_ Pred fn
_ = []

        termVarEqCases :: HasSpec fn b => Specification fn a -> Var b -> Term fn b -> [SolverStage fn]
        termVarEqCases :: forall b.
HasSpec fn b =>
Specification fn a -> Var b -> Term fn b -> [SolverStage fn]
termVarEqCases (MemberSpec NonEmpty a
vs) Var b
x' Term fn b
t
          | forall a. a -> Set a
Set.singleton (forall (fn :: [*] -> * -> *) a. HasSpec fn a => Var a -> Name fn
Name Var a
x) forall a. Eq a => a -> a -> Bool
== forall (fn :: [*] -> * -> *) a.
HasVariables fn a =>
a -> Set (Name fn)
freeVarSet Term fn b
t =
              [forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> [Pred fn] -> Specification fn a -> SolverStage fn
SolverStage Var b
x' [] forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). NonEmpty a -> Specification fn a
MemberSpec (forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
v -> forall a. GE a -> a
errorGE forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (fn :: [*] -> * -> *) a.
MonadGenError m =>
Env -> Term fn a -> m a
runTerm (forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var a
x a
v) Term fn b
t) NonEmpty a
vs))]
        termVarEqCases Specification fn a
spec Var b
x' Term fn b
t
          | Just a :~: b
Refl <- forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
x Var b
x'
          , [Name Var a
y] <- forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
HasVariables fn a =>
a -> Set (Name fn)
freeVarSet Term fn b
t
          , Result [NonEmpty [Char]]
_ Ctx fn a b
ctx <- forall (m :: * -> *) (fn :: [*] -> * -> *) v a.
(BaseUniverse fn, Typeable v, MonadGenError m, HasCallStack,
 HasSpec fn a, HasSpec fn v) =>
Var v -> Term fn a -> m (Ctx fn v a)
toCtx Var a
y Term fn b
t =
              [forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> [Pred fn] -> Specification fn a -> SolverStage fn
SolverStage Var a
y [] (forall (fn :: [*] -> * -> *) v a.
HasSpec fn v =>
Specification fn a -> Ctx fn v a -> Specification fn v
propagateSpec Specification fn a
spec Ctx fn a b
ctx)]
        termVarEqCases Specification fn a
_ Var b
_ Term fn b
_ = []

pattern Eql :: forall fn. () => forall a. HasSpec fn a => Term fn a -> Term fn a -> Term fn Bool
pattern $mEql :: forall {r} {fn :: [*] -> * -> *}.
Term fn Bool
-> (forall {a}. HasSpec fn a => Term fn a -> Term fn a -> r)
-> ((# #) -> r)
-> r
Eql a b <- App (extractFn @(EqFn fn) -> Just Equal) (a :> b :> Nil)

pattern FromG ::
  forall fn a.
  () =>
  (HasSpec fn a, HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
  Term fn (SimpleRep a) ->
  Term fn a
pattern $mFromG :: forall {r} {fn :: [*] -> * -> *} {a}.
Term fn a
-> ((HasSpec fn a, HasSimpleRep a,
     TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
    Term fn (SimpleRep a) -> r)
-> ((# #) -> r)
-> r
FromG a <- App (extractFn @(GenericsFn fn) -> Just FromGeneric) (a :> Nil)

pattern SLeft ::
  forall fn a. () => forall b c. (HasSpec fn b, a ~ Sum b c) => Term fn b -> Term fn a
pattern $mSLeft :: forall {r} {fn :: [*] -> * -> *} {a}.
Term fn a
-> (forall {b} {c}. (HasSpec fn b, a ~ Sum b c) => Term fn b -> r)
-> ((# #) -> r)
-> r
SLeft a <- App (extractFn @(SumFn fn) -> Just InjLeft) (a :> Nil)

pattern SRight ::
  forall fn a. () => forall b c. (HasSpec fn c, a ~ Sum b c) => Term fn c -> Term fn a
pattern $mSRight :: forall {r} {fn :: [*] -> * -> *} {a}.
Term fn a
-> (forall {b} {c}. (HasSpec fn c, a ~ Sum b c) => Term fn c -> r)
-> ((# #) -> r)
-> r
SRight a <- App (extractFn @(SumFn fn) -> Just InjRight) (a :> Nil)

-- ====================================================
-- Term patterns on function symbols on Sets, Lists
-- they are used in this
-- instance HasSpec fn a => Pretty (WithPrec (Term fn a)) where ...
-- Which uses: short :: forall a x. (Show a, Typeable a) => [a] -> Doc x
-- To elide large arguments to terms such as (subset_ x (lit y))
-- If 'y' is large, it will be elided.

pattern SubsetPat ::
  forall fn a.
  () =>
  forall b.
  (Ord b, HasSpec fn (Set b), Show b, Typeable b, a ~ Bool) =>
  Term fn (Set b) -> Term fn (Set b) -> Term fn a
pattern $mSubsetPat :: forall {r} {fn :: [*] -> * -> *} {a}.
Term fn a
-> (forall {b}.
    (Ord b, HasSpec fn (Set b), Show b, Typeable b, a ~ Bool) =>
    Term fn (Set b) -> Term fn (Set b) -> r)
-> ((# #) -> r)
-> r
SubsetPat a b <- App (extractFn @(SetFn fn) -> Just Subset) (a :> b :> Nil)

pattern DisjointPat ::
  forall fn a.
  () =>
  forall b.
  (Ord b, HasSpec fn (Set b), Show b, Typeable b, a ~ Bool) =>
  Term fn (Set b) -> Term fn (Set b) -> Term fn a
pattern $mDisjointPat :: forall {r} {fn :: [*] -> * -> *} {a}.
Term fn a
-> (forall {b}.
    (Ord b, HasSpec fn (Set b), Show b, Typeable b, a ~ Bool) =>
    Term fn (Set b) -> Term fn (Set b) -> r)
-> ((# #) -> r)
-> r
DisjointPat a b <- App (extractFn @(SetFn fn) -> Just Disjoint) (a :> b :> Nil)

pattern UnionPat ::
  forall fn a.
  () =>
  forall b.
  (Ord b, HasSpec fn (Set b), Show b, Typeable b, a ~ Set b) =>
  Term fn (Set b) -> Term fn (Set b) -> Term fn a
pattern $mUnionPat :: forall {r} {fn :: [*] -> * -> *} {a}.
Term fn a
-> (forall {b}.
    (Ord b, HasSpec fn (Set b), Show b, Typeable b, a ~ Set b) =>
    Term fn (Set b) -> Term fn (Set b) -> r)
-> ((# #) -> r)
-> r
UnionPat a b <- App (extractFn @(SetFn fn) -> Just Union) (a :> b :> Nil)

pattern MemberPat ::
  forall fn a.
  () =>
  forall b.
  (HasSpec fn b, HasSpec fn (Set b), Show b, Typeable b, a ~ Bool) =>
  Term fn b -> Term fn (Set b) -> Term fn a
pattern $mMemberPat :: forall {r} {fn :: [*] -> * -> *} {a}.
Term fn a
-> (forall {b}.
    (HasSpec fn b, HasSpec fn (Set b), Show b, Typeable b, a ~ Bool) =>
    Term fn b -> Term fn (Set b) -> r)
-> ((# #) -> r)
-> r
MemberPat a b <- App (extractFn @(SetFn fn) -> Just Member) (a :> b :> Nil)

pattern ElemPat ::
  forall fn a.
  () =>
  forall b.
  (HasSpec fn b, HasSpec fn [b], Show b, Typeable b, a ~ Bool) =>
  Term fn b -> Term fn [b] -> Term fn a
pattern $mElemPat :: forall {r} {fn :: [*] -> * -> *} {a}.
Term fn a
-> (forall {b}.
    (HasSpec fn b, HasSpec fn [b], Show b, Typeable b, a ~ Bool) =>
    Term fn b -> Term fn [b] -> r)
-> ((# #) -> r)
-> r
ElemPat a b <- App (extractFn @(SetFn fn) -> Just Elem) (a :> b :> Nil)

pattern AppendPat ::
  forall fn a.
  () =>
  forall b.
  (HasSpec fn [b], Show b, Typeable b, a ~ [b]) => Term fn [b] -> Term fn [b] -> Term fn a
pattern $mAppendPat :: forall {r} {fn :: [*] -> * -> *} {a}.
Term fn a
-> (forall {b}.
    (HasSpec fn [b], Show b, Typeable b, a ~ [b]) =>
    Term fn [b] -> Term fn [b] -> r)
-> ((# #) -> r)
-> r
AppendPat a b <- App (extractFn @(ListFn fn) -> Just AppendFn) (a :> b :> Nil)

short :: forall a x. (Show a, Typeable a) => [a] -> Doc x
short :: forall a x. (Show a, Typeable a) => [a] -> Doc x
short [] = Doc x
"[]"
short [a]
xs =
  let raw :: [Char]
raw = forall a. Show a => a -> [Char]
show [a]
xs
      shrunk :: [Char]
shrunk = if forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
raw forall a. Ord a => a -> a -> Bool
<= Int
20 then [Char]
raw else forall a. Int -> [a] -> [a]
take Int
20 [Char]
raw forall a. [a] -> [a] -> [a]
++ [Char]
" ... "
      refined :: Doc x
refined = Doc x
"[" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a. IsString a => [Char] -> a
fromString [Char]
shrunk forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc x
"]"
      elided :: Doc x
elided</