{-# 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 #-}
#if __GLASGOW_HASKELL__ < 900
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
#endif
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
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
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 ::
((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
) =>
Term fn b ->
Term fn a ->
(a -> b) ->
Pred fn
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) ->
List (Weighted (Binder fn)) as ->
Pred fn
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
data Ctx (fn :: [Type] -> Type -> Type) v a where
CtxHOLE ::
HasSpec fn v =>
Ctx fn v v
CtxApp ::
( HasSpec fn b
, TypeList as
, Typeable as
, All (HasSpec fn) as
) =>
fn as b ->
ListCtx Value as (Ctx fn v) ->
Ctx fn v b
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"
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
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
type OrdSet a = [a]
data Specification fn a where
ExplainSpec :: [String] -> Specification fn a -> Specification fn a
MemberSpec ::
NE.NonEmpty a ->
Specification fn a
ErrorSpec ::
NE.NonEmpty String ->
Specification fn a
SuspendedSpec ::
HasSpec fn a =>
Var a ->
Pred fn ->
Specification fn a
TypeSpec ::
HasSpec fn a =>
TypeSpec fn a ->
OrdSet a ->
Specification fn a
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
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
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)
,
(Int
1, forall a. Arbitrary a => Gen a
arbitrary)
]
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)
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"]
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
data BinaryShow where
BinaryShow :: forall a. String -> [Doc a] -> BinaryShow
NonBinary :: BinaryShow
class
( Typeable a
, Eq a
, Show a
, Show (TypeSpec fn a)
, BaseUniverse fn
) =>
HasSpec fn a
where
type TypeSpec (fn :: [Type] -> Type -> Type) a
type TypeSpec fn a = TypeSpec fn (SimpleRep a)
emptySpec :: TypeSpec fn a
combineSpec :: TypeSpec fn a -> TypeSpec fn a -> Specification fn a
genFromTypeSpec :: (HasCallStack, MonadGenError m) => TypeSpec fn a -> GenT m a
conformsTo :: HasCallStack => a -> TypeSpec fn a -> Bool
shrinkWithTypeSpec :: TypeSpec fn a -> a -> [a]
toPreds :: Term fn a -> TypeSpec fn a -> Pred fn
cardinalTypeSpec :: TypeSpec fn a -> Specification fn Integer
cardinalTrueSpec :: Specification fn Integer
cardinalTrueSpec = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
typeSpecHasError :: TypeSpec fn a -> Maybe (NE.NonEmpty String)
typeSpecHasError TypeSpec fn a
_ = forall a. Maybe a
Nothing
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
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
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
type Prerequisites fn a :: Constraint
type Prerequisites fn a = ()
prerequisites :: Evidence (Prerequisites fn a)
default prerequisites :: Prerequisites fn a => Evidence (Prerequisites fn a)
prerequisites = forall (c :: Constraint). c => Evidence c
Evidence
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
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)
class (HasSpec fn a, Show (Hint a)) => HasGenHint fn a where
type Hint a
giveHint :: Hint a -> Specification fn a
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
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
| 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
$
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]
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
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
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
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!"
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'
|
Env
env' <- forall (fn :: [*] -> * -> *). Env -> SolverPlan fn -> [Env]
shrinkEnvFromPlan Env
initialEnv SolverPlan fn
plan
,
Just a
a' <- [forall a. Typeable a => Env -> Var a -> Maybe a
lookupEnv Env
env' Var a
x]
,
a
a' forall a. Eq a => a -> a -> Bool
/= a
a
]
| Bool
otherwise = forall a. HasCallStack => [Char] -> a
error [Char]
"Bad pred"
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
_ [] = []
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]
[ 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]
]
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
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
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)
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
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
Reifies {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
ForAll {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
Case {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
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)
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
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'
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)
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'
[
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
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
saturatePred :: forall fn. Pred fn -> [Pred fn]
saturatePred :: forall {fn :: [*] -> * -> *}. Pred fn -> [Pred fn]
saturatePred Pred fn
p =
Pred fn
p
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
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)]
Pred fn
_ -> []
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
]
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)
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