{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ConstraintKinds #-}
module QuickSpec.Internal.Haskell where

import QuickSpec.Internal.Haskell.Resolve
import QuickSpec.Internal.Type
import QuickSpec.Internal.Prop
import QuickSpec.Internal.Pruning
import Test.QuickCheck hiding (total, classify, subterms, Fun)
import Data.Constraint hiding ((\\))
import Data.Proxy
import qualified Twee.Base as Twee
import QuickSpec.Internal.Term
import Data.Functor.Identity
import Data.Maybe
import Data.MemoUgly
import Test.QuickCheck.Gen.Unsafe
import Data.Char
import Data.Ord
import QuickSpec.Internal.Testing
import qualified QuickSpec.Internal.Testing.QuickCheck as QuickCheck
import qualified QuickSpec.Internal.Pruning.Twee as Twee
import QuickSpec.Internal.Explore hiding (quickSpec)
import qualified QuickSpec.Internal.Explore
import QuickSpec.Internal.Explore.Polymorphic(Universe(..), VariableUse(..))
import QuickSpec.Internal.Pruning.Background(Background)
import Control.Monad
import Control.Monad.Trans.State.Strict
import QuickSpec.Internal.Terminal
import Text.Printf
import QuickSpec.Internal.Utils
import Data.Lens.Light
import GHC.TypeLits
import QuickSpec.Internal.Explore.Conditionals hiding (Normal)
import Control.Spoon
import qualified Data.Set as Set
import qualified Test.QuickCheck.Poly as Poly
import Numeric.Natural(Natural)
import Test.QuickCheck.Instances()
import Data.Word
import Data.List.NonEmpty (NonEmpty)
import Data.Complex
import Data.Ratio
import Data.Functor.Compose
import Data.Int
import Data.Void
import Data.Unique
import qualified Data.Monoid as DM
import qualified Data.Semigroup as DS
import qualified Data.Map.Strict as Map
import Test.QuickCheck.Gen
import Test.QuickCheck.Random

baseInstances :: Instances
baseInstances :: Instances
baseInstances =
  forall a. Monoid a => [a] -> a
mconcat [
    -- Generate tuple values (pairs and () are built into findInstance)
    forall a. Typeable a => a -> Instances
inst forall a b. (a -> b) -> a -> b
$ \(A
x :: A) (B
y :: B) (C
z :: C) -> (A
x, B
y, C
z),
    forall a. Typeable a => a -> Instances
inst forall a b. (a -> b) -> a -> b
$ \(A
x :: A) (B
y :: B) (C
z :: C) (D
w :: D) -> (A
x, B
y, C
z, D
w),
    forall a. Typeable a => a -> Instances
inst forall a b. (a -> b) -> a -> b
$ \(A
x :: A) (B
y :: B) (C
z :: C) (D
w :: D) (E
v :: E) -> (A
x, B
y, C
z, D
w, E
v),
    -- Split conjunctions of typeclasses into individuals
    forall a. Typeable a => a -> Instances
inst forall a b. (a -> b) -> a -> b
$ \() -> forall (a :: Constraint). a => Dict a
Dict :: Dict (),
    forall a. Typeable a => a -> Instances
inst forall a b. (a -> b) -> a -> b
$ \(Dict ClassA
Dict :: Dict ClassA) (Dict ClassB
Dict :: Dict ClassB) -> forall (a :: Constraint). a => Dict a
Dict :: Dict (ClassA, ClassB),
    forall a. Typeable a => a -> Instances
inst forall a b. (a -> b) -> a -> b
$ \(Dict ClassA
Dict :: Dict ClassA) (Dict ClassB
Dict :: Dict ClassB) (Dict ClassC
Dict :: Dict ClassC) -> forall (a :: Constraint). a => Dict a
Dict :: Dict (ClassA, ClassB, ClassC),
    forall a. Typeable a => a -> Instances
inst forall a b. (a -> b) -> a -> b
$ \(Dict ClassA
Dict :: Dict ClassA) (Dict ClassB
Dict :: Dict ClassB) (Dict ClassC
Dict :: Dict ClassC) (Dict ClassD
Dict :: Dict ClassD) -> forall (a :: Constraint). a => Dict a
Dict :: Dict (ClassA, ClassB, ClassC, ClassD),
    forall a. Typeable a => a -> Instances
inst forall a b. (a -> b) -> a -> b
$ \(Dict ClassA
Dict :: Dict ClassA) (Dict ClassB
Dict :: Dict ClassB) (Dict ClassC
Dict :: Dict ClassC) (Dict ClassD
Dict :: Dict ClassD) (Dict ClassE
Dict :: Dict ClassE) -> forall (a :: Constraint). a => Dict a
Dict :: Dict (ClassA, ClassB, ClassC, ClassD, ClassE),
    forall a. Typeable a => a -> Instances
inst forall a b. (a -> b) -> a -> b
$ \(Dict ClassA
Dict :: Dict ClassA) (Dict ClassB
Dict :: Dict ClassB) (Dict ClassC
Dict :: Dict ClassC) (Dict ClassD
Dict :: Dict ClassD) (Dict ClassE
Dict :: Dict ClassE) (Dict ClassF
Dict :: Dict ClassF) -> forall (a :: Constraint). a => Dict a
Dict :: Dict (ClassA, ClassB, ClassC, ClassD, ClassE, ClassF),
    -- Derive typeclass instances using (:-)
    -- N.B. flip is there to resolve (:-) first to reduce backtracking
    forall a. Typeable a => a -> Instances
inst forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
$ \(Dict ClassA
Dict :: Dict ClassA) (Sub Dict ClassB
ClassA => Dict ClassB
Dict :: ClassA :- ClassB) -> forall (a :: Constraint). a => Dict a
Dict :: Dict ClassB,
    -- Standard names
    forall a. Typeable a => a -> Instances
inst forall a b. (a -> b) -> a -> b
$ \(Names [String]
names :: Names A) ->
      forall a. [String] -> Names a
Names (forall a b. (a -> b) -> [a] -> [b]
map (forall a. [a] -> [a] -> [a]
++ String
"s") [String]
names) :: Names [A],
    forall a. Typeable a => a -> Instances
inst (forall a. [String] -> Names a
Names [String
"p", String
"q", String
"r"] :: Names (A -> Bool)),
    forall a. Typeable a => a -> Instances
inst (forall a. [String] -> Names a
Names [String
"f", String
"g", String
"h"] :: Names (A -> B)),
    forall a. Typeable a => a -> Instances
inst (forall a. [String] -> Names a
Names [String
"dict"] :: Names (Dict ClassA)),
    forall a. Typeable a => a -> Instances
inst (forall a. [String] -> Names a
Names [String
"x", String
"y", String
"z", String
"w"] :: Names A),
    -- Allow up to 4 variables per type by default
    forall a. Typeable a => a -> Instances
inst (forall a. VariableUse -> Use a
Use (Int -> VariableUse
UpTo Int
4) :: Use A),
    -- Standard instances
    forall (proxy :: * -> *) a.
(Ord a, Arbitrary a, Typeable a) =>
proxy a -> Instances
baseType (forall {k} (t :: k). Proxy t
Proxy :: Proxy ()),
    forall (proxy :: * -> *) a.
(Ord a, Arbitrary a, Typeable a) =>
proxy a -> Instances
baseType (forall {k} (t :: k). Proxy t
Proxy :: Proxy Int),
    forall (proxy :: * -> *) a.
(Ord a, Arbitrary a, Typeable a) =>
proxy a -> Instances
baseType (forall {k} (t :: k). Proxy t
Proxy :: Proxy Integer),
    forall (proxy :: * -> *) a.
(Ord a, Arbitrary a, Typeable a) =>
proxy a -> Instances
baseType (forall {k} (t :: k). Proxy t
Proxy :: Proxy Natural),
    forall (proxy :: * -> *) a.
(Ord a, Arbitrary a, Typeable a) =>
proxy a -> Instances
baseType (forall {k} (t :: k). Proxy t
Proxy :: Proxy Bool),
    forall (proxy :: * -> *) a.
(Ord a, Arbitrary a, Typeable a) =>
proxy a -> Instances
baseType (forall {k} (t :: k). Proxy t
Proxy :: Proxy Char),
    forall (proxy :: * -> *) a.
(Ord a, Arbitrary a, Typeable a) =>
proxy a -> Instances
baseType (forall {k} (t :: k). Proxy t
Proxy :: Proxy Poly.OrdA),
    forall (proxy :: * -> *) a.
(Ord a, Arbitrary a, Typeable a) =>
proxy a -> Instances
baseType (forall {k} (t :: k). Proxy t
Proxy :: Proxy Poly.OrdB),
    forall (proxy :: * -> *) a.
(Ord a, Arbitrary a, Typeable a) =>
proxy a -> Instances
baseType (forall {k} (t :: k). Proxy t
Proxy :: Proxy Poly.OrdC),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: () :- CoArbitrary ()),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: () :- CoArbitrary Int),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: () :- CoArbitrary Integer),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: () :- CoArbitrary Natural),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: () :- CoArbitrary Bool),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: () :- CoArbitrary Char),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: () :- CoArbitrary Poly.OrdA),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: () :- CoArbitrary Poly.OrdB),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: () :- CoArbitrary Poly.OrdC),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: Eq A :- Eq [A]),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: Ord A :- Ord [A]),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: Arbitrary A :- Arbitrary [A]),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: CoArbitrary A :- CoArbitrary [A]),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: Eq A :- Eq (Maybe A)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: Ord A :- Ord (Maybe A)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: Arbitrary A :- Arbitrary (Maybe A)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: CoArbitrary A :- CoArbitrary (Maybe A)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (Eq A, Eq B) :- Eq (Either A B)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (Ord A, Ord B) :- Ord (Either A B)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (Arbitrary A, Arbitrary B) :- Arbitrary (Either A B)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (CoArbitrary A, CoArbitrary B) :- CoArbitrary (Either A B)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (Eq A, Eq B) :- Eq (A, B)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (Ord A, Ord B) :- Ord (A, B)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (Arbitrary A, Arbitrary B) :- Arbitrary (A, B)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (CoArbitrary A, CoArbitrary B) :- CoArbitrary (A, B)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (Eq A, Eq B, Eq C) :- Eq (A, B, C)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (Ord A, Ord B, Ord C) :- Ord (A, B, C)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (Arbitrary A, Arbitrary B, Arbitrary C) :- Arbitrary (A, B, C)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (CoArbitrary A, CoArbitrary B, CoArbitrary C) :- CoArbitrary (A, B, C)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (Eq A, Eq B, Eq C, Eq D) :- Eq (A, B, C, D)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (Ord A, Ord B, Ord C, Ord D) :- Ord (A, B, C, D)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (Arbitrary A, Arbitrary B, Arbitrary C, Arbitrary D) :- Arbitrary (A, B, C, D)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (CoArbitrary A, CoArbitrary B, CoArbitrary C, CoArbitrary D) :- CoArbitrary (A, B, C, D)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (CoArbitrary A, Arbitrary B) :- Arbitrary (A -> B)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: (Arbitrary A, CoArbitrary B) :- CoArbitrary (A -> B)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict :: Ord A :- Eq A),
    -- From Arbitrary to Gen
    forall a. Typeable a => a -> Instances
inst forall a b. (a -> b) -> a -> b
$ \(Dict (Arbitrary A)
Dict :: Dict (Arbitrary A)) -> forall a. Arbitrary a => Gen a
arbitrary :: Gen A,
    -- Observation functions
    forall a. Typeable a => a -> Instances
inst forall a b. (a -> b) -> a -> b
$ \(Dict (Ord A)
Dict :: Dict (Ord A)) -> forall a. Ord a => OrdInstance a
OrdInstance :: OrdInstance A,
    forall a. Typeable a => a -> Instances
inst (\(Dict (Observe A B C)
Dict :: Dict (Observe A B C)) -> forall test outcome a.
Observe test outcome a =>
ObserveData a outcome
observeObs :: ObserveData C B),
    forall a. Typeable a => a -> Instances
inst (\(Dict (Ord A)
Dict :: Dict (Ord A)) -> forall a. Ord a => ObserveData a a
observeOrd :: ObserveData A A),
    forall a. Typeable a => a -> Instances
inst (\(Dict (Arbitrary A)
Dict :: Dict (Arbitrary A)) (ObserveData B C
obs :: ObserveData B C) -> forall a b outcome.
Arbitrary a =>
ObserveData b outcome -> ObserveData (a -> b) outcome
observeFunction ObserveData B C
obs :: ObserveData (A -> B) C),
    forall a. Typeable a => a -> Instances
inst (\(ObserveData A B
obs :: ObserveData A B) -> forall a. Value (ObserveData a) -> WrappedObserveData a
WrappedObserveData (forall (f :: * -> *) a. Typeable a => f a -> Value f
toValue ObserveData A B
obs)),
    -- No warnings for TestCaseWrapped
    forall a. Typeable a => a -> Instances
inst (forall a. NoWarnings a
NoWarnings :: NoWarnings (TestCaseWrapped SymA A)),
    -- Needed for typeclass-polymorphic predicates to work currently
    forall a. Typeable a => a -> Instances
inst (\(Dict ClassA
Dict :: Dict ClassA) -> forall (a :: Constraint). a => Dict a
Dict :: Dict (Arbitrary (Dict ClassA)))]

data OrdInstance a where
  OrdInstance :: Ord a => OrdInstance a

-- A token used in the instance list for types that shouldn't generate warnings
data NoWarnings a = NoWarnings

data Use a = Use VariableUse

instance c => Arbitrary (Dict c) where
  arbitrary :: Gen (Dict c)
arbitrary = forall (m :: * -> *) a. Monad m => a -> m a
return forall (a :: Constraint). a => Dict a
Dict

-- | A typeclass for types which support observational equality, typically used
-- for types that have no `Ord` instance.
--
-- An instance @Observe test outcome a@ declares that values of type @a@ can be
-- /tested/ for equality by random testing. You supply a function
-- @observe :: test -> outcome -> a@. Then, two values @x@ and @y@ are considered
-- equal, if for many random values of type @test@, @observe test x == observe test y@.
--
-- The function `QuickSpec.monoTypeObserve` declares a monomorphic
-- type with an observation function. For polymorphic types, use
-- `QuickSpec.inst` to declare the `Observe` instance.
--
-- For an example of using observational equality, see @<https://github.com/nick8325/quickspec/tree/master/examples/PrettyPrinting.hs PrettyPrinting.hs>@.
class (Arbitrary test, Ord outcome) => Observe test outcome a | a -> test outcome where
  -- | Make an observation on a value. Should satisfy the following law: if
  -- @x /= y@, then there exists a value of @test@ such that @observe test x /= observe test y@.
  observe :: test -> a -> outcome

  default observe :: (test ~ (), outcome ~ a) => test -> a -> outcome
  observe test
_ a
x = a
x

instance (Arbitrary a, Observe test outcome b) => Observe (a, test) outcome (a -> b) where
  observe :: (a, test) -> (a -> b) -> outcome
observe (a
x, test
obs) a -> b
f = forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe test
obs (a -> b
f a
x)

instance Observe () Int Int
instance Observe () Int8 Int8
instance Observe () Int16 Int16
instance Observe () Int32 Int32
instance Observe () Int64 Int64
instance Observe () Float Float
instance Observe () Double Double
instance Observe () Word Word
instance Observe () Word8 Word8
instance Observe () Word16 Word16
instance Observe () Word32 Word32
instance Observe () Word64 Word64
instance Observe () Integer Integer
instance Observe () Char Char
instance Observe () Bool Bool
instance Observe () Ordering Ordering
instance Observe () Void Void
instance Observe () Unique Unique
instance Observe () Natural Natural
instance Observe () DS.All DS.All
instance Observe () DS.Any DS.Any
instance Observe () () ()
instance (Observe xt xo x, Observe yt yo y)
      => Observe (xt, yt) (xo, yo) (x, y) where
  observe :: (xt, yt) -> (x, y) -> (xo, yo)
observe (xt
xt, yt
yt) (x
x, y
y)
    = (forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe xt
xt x
x, forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe yt
yt y
y)
instance (Observe xt xo x, Observe yt yo y, Observe zt zo z)
      => Observe (xt, yt, zt) (xo, yo, zo) (x, y, z) where
  observe :: (xt, yt, zt) -> (x, y, z) -> (xo, yo, zo)
observe (xt
xt, yt
yt, zt
zt) (x
x, y
y, z
z)
    = (forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe xt
xt x
x, forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe yt
yt y
y, forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe zt
zt z
z)
instance (Observe xt xo x, Observe yt yo y, Observe zt zo z, Observe wt wo w)
      => Observe (xt, yt, zt, wt) (xo, yo, zo, wo) (x, y, z, w) where
  observe :: (xt, yt, zt, wt) -> (x, y, z, w) -> (xo, yo, zo, wo)
observe (xt
xt, yt
yt, zt
zt, wt
wt) (x
x, y
y, z
z, w
w)
    = (forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe xt
xt x
x, forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe yt
yt y
y, forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe zt
zt z
z, forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe wt
wt w
w)
instance Observe t p a => Observe t [p] [a] where
  observe :: t -> [a] -> [p]
observe t
t [a]
ps = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t) [a]
ps
instance Observe t p a => Observe t (NonEmpty p) (NonEmpty a) where
  observe :: t -> NonEmpty a -> NonEmpty p
observe t
t NonEmpty a
ps = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t) NonEmpty a
ps
instance Observe t p a => Observe (t, t) (p, p) (Complex a) where
  observe :: (t, t) -> Complex a -> (p, p)
observe (t
t1, t
t2) (a
p1 :+ a
p2) = (forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t1 a
p1, forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t2 a
p2)
instance Observe t p a => Observe (t, t) (p, p) (Ratio a) where
  observe :: (t, t) -> Ratio a -> (p, p)
observe (t
t1, t
t2) (Ratio a
p)
    = (forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t1 forall a b. (a -> b) -> a -> b
$ forall a. Ratio a -> a
numerator Ratio a
p, forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t2 forall a b. (a -> b) -> a -> b
$ forall a. Ratio a -> a
denominator Ratio a
p)
instance Observe t p a => Observe t p (Identity a) where
  observe :: t -> Identity a -> p
observe t
t = forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Identity a -> a
runIdentity
instance Observe t p (f (g a)) => Observe t p (Compose f g a) where
  observe :: t -> Compose f g a -> p
observe t
t = forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose
instance (Observe at ao a, Observe bt bo b)
      => Observe (at, bt) (Either ao bo) (Either a b) where
  observe :: (at, bt) -> Either a b -> Either ao bo
observe (at
at, bt
_) (Left a
a)  = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe at
at a
a
  observe (at
_, bt
bt) (Right b
b) = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe bt
bt b
b
instance Observe t p a => Observe t p (DS.Sum a) where
  observe :: t -> Sum a -> p
observe t
t = forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Sum a -> a
DS.getSum
instance Observe t p a => Observe t p (DS.Product a) where
  observe :: t -> Product a -> p
observe t
t = forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Product a -> a
DS.getProduct
instance Observe t p a => Observe t p (DS.First a) where
  observe :: t -> First a -> p
observe t
t = forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. First a -> a
DS.getFirst
instance Observe t p a => Observe t p (DS.Last a) where
  observe :: t -> Last a -> p
observe t
t = forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Last a -> a
DS.getLast
instance Observe t p a => Observe t p (DS.Dual a) where
  observe :: t -> Dual a -> p
observe t
t = forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Dual a -> a
DS.getDual
instance Observe t p a => Observe t p (DS.Min a) where
  observe :: t -> Min a -> p
observe t
t = forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Min a -> a
DS.getMin
instance Observe t p a => Observe t p (DS.Max a) where
  observe :: t -> Max a -> p
observe t
t = forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Max a -> a
DS.getMax
instance Observe t p a => Observe t p (DS.WrappedMonoid a) where
  observe :: t -> WrappedMonoid a -> p
observe t
t = forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. WrappedMonoid m -> m
DS.unwrapMonoid
instance Observe t p (f a) => Observe t p (DM.Alt f a) where
  observe :: t -> Alt f a -> p
observe t
t = forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). Alt f a -> f a
DM.getAlt
instance Observe t p (f a) => Observe t p (DM.Ap f a) where
  observe :: t -> Ap f a -> p
observe t
t = forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). Ap f a -> f a
DM.getAp
instance Observe t p a => Observe t (Maybe p) (DM.First a) where
  observe :: t -> First a -> Maybe p
observe t
t = forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. First a -> Maybe a
DM.getFirst
instance Observe t p a => Observe t (Maybe p) (DM.Last a) where
  observe :: t -> Last a -> Maybe p
observe t
t = forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Last a -> Maybe a
DM.getLast
#if !MIN_VERSION_base(4,16,0)
instance Observe t p a => Observe t (Maybe p) (DS.Option a) where
  observe t = observe t . DS.getOption
#endif
instance Observe t p a => Observe t (Maybe p) (Maybe a) where
  observe :: t -> Maybe a -> Maybe p
observe t
t (Just a
a) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe t
t a
a
  observe t
_ Maybe a
Nothing  = forall a. Maybe a
Nothing
instance (Arbitrary a, Observe t p a) => Observe (a, t) p (DS.Endo a) where
  observe :: (a, t) -> Endo a -> p
observe (a, t)
t = forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe (a, t)
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Endo a -> a -> a
DS.appEndo


-- | Like 'Test.QuickCheck.===', but using the 'Observe' typeclass instead of 'Eq'.
(=~=) :: (Show test, Show outcome, Observe test outcome a) => a -> a -> Property
a
a =~= :: forall test outcome a.
(Show test, Show outcome, Observe test outcome a) =>
a -> a -> Property
=~= a
b = forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ \test
test -> forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe test
test a
a forall a. (Eq a, Show a) => a -> a -> Property
Test.QuickCheck.=== forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe test
test a
b
infix 4 =~=

-- An observation function along with instances.
-- The parameters are in this order so that we can use findInstance to get at appropriate Wrappers.
data ObserveData a outcome where
  ObserveData :: (Arbitrary test, Ord outcome) => (test -> a -> outcome) -> ObserveData a outcome
newtype WrappedObserveData a = WrappedObserveData (Value (ObserveData a))

observeOrd :: Ord a => ObserveData a a
observeOrd :: forall a. Ord a => ObserveData a a
observeOrd = forall test outcome a.
(Arbitrary test, Ord outcome) =>
(test -> a -> outcome) -> ObserveData a outcome
ObserveData (\() a
x -> a
x)

observeFunction :: Arbitrary a => ObserveData b outcome -> ObserveData (a -> b) outcome
observeFunction :: forall a b outcome.
Arbitrary a =>
ObserveData b outcome -> ObserveData (a -> b) outcome
observeFunction (ObserveData test -> b -> outcome
obs) =
  forall test outcome a.
(Arbitrary test, Ord outcome) =>
(test -> a -> outcome) -> ObserveData a outcome
ObserveData (\(a
x, test
test) a -> b
f -> test -> b -> outcome
obs test
test (a -> b
f a
x))

observeObs :: Observe test outcome a => ObserveData a outcome
observeObs :: forall test outcome a.
Observe test outcome a =>
ObserveData a outcome
observeObs = forall test outcome a.
(Arbitrary test, Ord outcome) =>
(test -> a -> outcome) -> ObserveData a outcome
ObserveData forall test outcome a.
Observe test outcome a =>
test -> a -> outcome
observe

baseType :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => proxy a -> Instances
baseType :: forall (proxy :: * -> *) a.
(Ord a, Arbitrary a, Typeable a) =>
proxy a -> Instances
baseType proxy a
_ =
  forall a. Monoid a => [a] -> a
mconcat [
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint). a => Dict a
Dict :: Dict (Ord a)),
    forall a. Typeable a => a -> Instances
inst (forall (a :: Constraint). a => Dict a
Dict :: Dict (Arbitrary a))]

-- Declares what variable names should be used for values of a particular type.
newtype Names a = Names { forall a. Names a -> [String]
getNames :: [String] }

names :: Instances -> Type -> [String]
names :: Instances -> Term TyCon -> [String]
names Instances
insts Term TyCon
ty =
  case forall (f :: * -> *).
Typeable f =>
Instances -> Term TyCon -> Maybe (Value f)
findInstance Instances
insts (forall a. Typed a => a -> a
skolemiseTypeVars Term TyCon
ty) of
    Just Value Names
x  -> forall {k} (f :: k -> *) b.
(forall (a :: k). f a -> b) -> Value f -> b
ofValue forall a. Names a -> [String]
getNames Value Names
x
    Maybe (Value Names)
Nothing -> forall a. HasCallStack => String -> a
error String
"don't know how to name variables"

-- An Ordy a represents a value of type a together with its Ord instance.
-- A Value Ordy is a value of unknown type which implements Ord.
data Ordy a where Ordy :: Ord a => a -> Ordy a
instance Eq (Value Ordy) where Value Ordy
x == :: Value Ordy -> Value Ordy -> Bool
== Value Ordy
y = forall a. Ord a => a -> a -> Ordering
compare Value Ordy
x Value Ordy
y forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance Ord (Value Ordy) where
  compare :: Value Ordy -> Value Ordy -> Ordering
compare Value Ordy
x Value Ordy
y =
    case forall {k} (f :: k -> *). Value f -> Unwrapped f
unwrap Value Ordy
x of
      Ordy a
xv `In` Wrapper a
w ->
        let Ordy a
yv = forall {k} (a :: k).
Wrapper a -> forall (g :: k -> *). Value g -> g a
reunwrap Wrapper a
w Value Ordy
y in
        forall a. Ord a => a -> a -> Ordering
compare a
xv a
yv

-- | A test case is everything you need to evaluate a Haskell term.
data TestCase =
  TestCase {
    -- | Evaluate a variable. Returns @Nothing@ if no `Arbitrary` instance was found.
    TestCase -> Var -> Maybe (Value Identity)
tc_eval_var :: Var -> Maybe (Value Identity),
    -- | Apply an observation function to get a value implementing `Ord`.
    -- Returns @Nothing@ if no observer was found.
    TestCase -> Value Identity -> Maybe (Value Ordy)
tc_test_result :: Value Identity -> Maybe (Value Ordy) }

-- | Generate a random test case.
arbitraryTestCase :: Type -> Instances -> Gen TestCase
arbitraryTestCase :: Term TyCon -> Instances -> Gen TestCase
arbitraryTestCase Term TyCon
def Instances
insts =
  (Var -> Maybe (Value Identity))
-> (Value Identity -> Maybe (Value Ordy)) -> TestCase
TestCase forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term TyCon -> Instances -> Gen (Var -> Maybe (Value Identity))
arbitraryValuation Term TyCon
def Instances
insts forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term TyCon
-> Instances -> Gen (Value Identity -> Maybe (Value Ordy))
arbitraryObserver Term TyCon
def Instances
insts

-- | Generate a random variable valuation.
arbitraryValuation :: Type -> Instances -> Gen (Var -> Maybe (Value Identity))
arbitraryValuation :: Term TyCon -> Instances -> Gen (Var -> Maybe (Value Identity))
arbitraryValuation Term TyCon
def Instances
insts = do
  forall a b. Ord a => (a -> b) -> a -> b
memo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. CoArbitrary a => (a -> Gen b) -> Gen (a -> b)
arbitraryFunction (forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyCon
-> Instances -> Term TyCon -> Maybe (Gen (Value Identity))
findGenerator Term TyCon
def Instances
insts forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Term TyCon
var_ty)

-- | Generate a random observation.
arbitraryObserver :: Type -> Instances -> Gen (Value Identity -> Maybe (Value Ordy))
arbitraryObserver :: Term TyCon
-> Instances -> Gen (Value Identity -> Maybe (Value Ordy))
arbitraryObserver Term TyCon
def Instances
insts = do
  Term TyCon -> Maybe (Value Identity -> Value Ordy)
find <- forall a b. CoArbitrary a => (a -> Gen b) -> Gen (a -> b)
arbitraryFunction forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instances
-> Term TyCon -> Maybe (Gen (Value Identity -> Value Ordy))
findObserver Instances
insts
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \Value Identity
x -> do
    Value Identity -> Value Ordy
obs <- Term TyCon -> Maybe (Value Identity -> Value Ordy)
find (forall a. Typed a => Term TyCon -> a -> a
defaultTo Term TyCon
def (forall a. Typed a => a -> Term TyCon
typ Value Identity
x))
    forall (m :: * -> *) a. Monad m => a -> m a
return (Value Identity -> Value Ordy
obs Value Identity
x)

findGenerator :: Type -> Instances -> Type -> Maybe (Gen (Value Identity))
findGenerator :: Term TyCon
-> Instances -> Term TyCon -> Maybe (Gen (Value Identity))
findGenerator Term TyCon
def Instances
insts Term TyCon
ty =
  forall (f :: * -> *). Functor f => Value f -> f (Value Identity)
bringFunctor forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (f :: * -> *).
Typeable f =>
Instances -> Term TyCon -> Maybe (Value f)
findInstance Instances
insts (forall a. Typed a => Term TyCon -> a -> a
defaultTo Term TyCon
def Term TyCon
ty) :: Maybe (Value Gen))

findOrdInstance :: Instances -> Type -> Maybe (Value OrdInstance)
findOrdInstance :: Instances -> Term TyCon -> Maybe (Value OrdInstance)
findOrdInstance Instances
insts Term TyCon
ty = forall (f :: * -> *).
Typeable f =>
Instances -> Term TyCon -> Maybe (Value f)
findInstance Instances
insts Term TyCon
ty

findObserver :: Instances -> Type -> Maybe (Gen (Value Identity -> Value Ordy))
findObserver :: Instances
-> Term TyCon -> Maybe (Gen (Value Identity -> Value Ordy))
findObserver Instances
insts Term TyCon
ty = do
  Value WrappedObserveData
inst <- forall (f :: * -> *).
Typeable f =>
Instances -> Term TyCon -> Maybe (Value f)
findInstance Instances
insts Term TyCon
ty :: Maybe (Value WrappedObserveData)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    case forall {k} (f :: k -> *). Value f -> Unwrapped f
unwrap Value WrappedObserveData
inst of
      WrappedObserveData Value (ObserveData a)
val `In` Wrapper a
valueWrapper ->
        case forall {k} (f :: k -> *). Value f -> Unwrapped f
unwrap Value (ObserveData a)
val of
          -- This brings Arbitrary and Ord instances into scope
          ObserveData test -> a -> a
obs `In` Wrapper a
outcomeWrapper -> do
            test
test <- forall a. Arbitrary a => Gen a
arbitrary
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \Value Identity
x ->
              let value :: a
value = forall a. Identity a -> a
runIdentity (forall {k} (a :: k).
Wrapper a -> forall (g :: k -> *). Value g -> g a
reunwrap Wrapper a
valueWrapper Value Identity
x)
                  outcome :: a
outcome = test -> a -> a
obs test
test a
value
              in forall {k} (a :: k).
Wrapper a -> forall (g :: k -> *). g a -> Value g
wrap Wrapper a
outcomeWrapper (forall a. Ord a => a -> Ordy a
Ordy a
outcome)

-- | Generate a random function. Should be in QuickCheck.
arbitraryFunction :: CoArbitrary a => (a -> Gen b) -> Gen (a -> b)
arbitraryFunction :: forall a b. CoArbitrary a => (a -> Gen b) -> Gen (a -> b)
arbitraryFunction a -> Gen b
gen = forall (m :: * -> *) a. Monad m => m (Gen a) -> Gen (m a)
promote (\a
x -> forall a b. CoArbitrary a => a -> Gen b -> Gen b
coarbitrary a
x (a -> Gen b
gen a
x))

-- | Evaluate a Haskell term in an environment.
evalHaskell :: Type -> Instances -> TestCase -> Term Constant -> Maybe (Value Ordy)
evalHaskell :: Term TyCon
-> Instances -> TestCase -> Term Constant -> Maybe (Value Ordy)
evalHaskell Term TyCon
def Instances
insts (TestCase Var -> Maybe (Value Identity)
env Value Identity -> Maybe (Value Ordy)
obs) Term Constant
t = do
  let eval :: (Var -> Maybe (Value Identity))
-> Term Constant -> Maybe (Value Identity)
eval Var -> Maybe (Value Identity)
env Term Constant
t = forall fun a (m :: * -> *).
(Typed fun, Apply a, Monad m) =>
(Var -> m a) -> (fun -> m a) -> Term fun -> m a
evalTerm Var -> Maybe (Value Identity)
env (Instances -> Constant -> Maybe (Value Identity)
evalConstant Instances
insts) Term Constant
t
  Identity a
val `In` Wrapper a
w <- forall {k} (f :: k -> *). Value f -> Unwrapped f
unwrap forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var -> Maybe (Value Identity))
-> Term Constant -> Maybe (Value Identity)
eval Var -> Maybe (Value Identity)
env (forall a. Typed a => Term TyCon -> a -> a
defaultTo Term TyCon
def Term Constant
t)
  Value Ordy
res <- Value Identity -> Maybe (Value Ordy)
obs (forall {k} (a :: k).
Wrapper a -> forall (g :: k -> *). g a -> Value g
wrap Wrapper a
w (forall a. a -> Identity a
Identity a
val))
  -- Don't allow partial results to enter the decision tree
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall {k} (f :: k -> *) b.
Value f -> (forall (a :: k). f a -> b) -> b
withValue Value Ordy
res (\(Ordy a
x) -> forall a. Maybe a -> Bool
isJust (forall a. a -> Maybe a
teaspoon (a
x forall a. Eq a => a -> a -> Bool
== a
x))))
  forall (m :: * -> *) a. Monad m => a -> m a
return Value Ordy
res

data Constant =
  Constant {
    Constant -> String
con_name  :: String,
    Constant -> TermStyle
con_style :: TermStyle,
    Constant -> Value Identity
con_value :: Value Identity,
    Constant -> Term TyCon
con_type :: Type,
    Constant -> [Term TyCon]
con_constraints :: [Type],
    Constant -> Int
con_size :: Int,
    Constant -> Classification Constant
con_classify :: Classification Constant,
    Constant -> Bool
con_is_hole :: Bool }

instance Eq Constant where
  Constant
x == :: Constant -> Constant -> Bool
== Constant
y =
    Constant -> String
con_name Constant
x forall a. Eq a => a -> a -> Bool
== Constant -> String
con_name Constant
y Bool -> Bool -> Bool
&& forall a. Typed a => a -> Term TyCon
typ (Constant -> Value Identity
con_value Constant
x) forall a. Eq a => a -> a -> Bool
== forall a. Typed a => a -> Term TyCon
typ (Constant -> Value Identity
con_value Constant
y)

instance Ord Constant where
  compare :: Constant -> Constant -> Ordering
compare =
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a b. (a -> b) -> a -> b
$ \Constant
con ->
      (Term TyCon -> Int
typeArity (forall a. Typed a => a -> Term TyCon
typ Constant
con), forall a. Typed a => a -> Term TyCon
typ Constant
con, Constant -> String
con_name Constant
con)

instance Background Constant

con :: Typeable a => String -> a -> Constant
con :: forall a. Typeable a => String -> a -> Constant
con String
name a
val =
  String -> Value Identity -> Constant
constant' String
name (forall (f :: * -> *) a. Typeable a => f a -> Value f
toValue (forall a. a -> Identity a
Identity a
val))

constant' :: String -> Value Identity -> Constant
constant' :: String -> Value Identity -> Constant
constant' String
name Value Identity
val =
  Constant {
    con_name :: String
con_name = String
name,
    con_style :: TermStyle
con_style =
      case () of
        ()
_ | String
name forall a. Eq a => a -> a -> Bool
== String
"()" -> TermStyle
curried
          | forall a. Int -> [a] -> [a]
take Int
1 String
name forall a. Eq a => a -> a -> Bool
== String
"," -> Int -> TermStyle -> TermStyle
fixedArity (forall (t :: * -> *) a. Foldable t => t a -> Int
length String
nameforall a. Num a => a -> a -> a
+Int
1) TermStyle
tupleStyle
          | forall a. Int -> [a] -> [a]
take Int
2 String
name forall a. Eq a => a -> a -> Bool
== String
"(," -> Int -> TermStyle -> TermStyle
fixedArity (forall (t :: * -> *) a. Foldable t => t a -> Int
length String
nameforall a. Num a => a -> a -> a
-Int
1) TermStyle
tupleStyle
          | String -> Bool
isOp String
name Bool -> Bool -> Bool
&& Term TyCon -> Int
typeArity (forall a. Typed a => a -> Term TyCon
typ Value Identity
val) forall a. Ord a => a -> a -> Bool
>= Int
2 -> Int -> TermStyle
infixStyle Int
5
          | String -> Bool
isOp String
name -> TermStyle
prefix
          | Bool
otherwise -> TermStyle
curried,
    con_value :: Value Identity
con_value = Value Identity
val,
    con_type :: Term TyCon
con_type = Term TyCon
ty,
    con_constraints :: [Term TyCon]
con_constraints = [Term TyCon]
constraints,
    con_size :: Int
con_size = Int
1,
    con_classify :: Classification Constant
con_classify = forall fun. Classification fun
Function,
    con_is_hole :: Bool
con_is_hole = Bool
False }
  where
    ([Term TyCon]
constraints, Term TyCon
ty) = Term TyCon -> ([Term TyCon], Term TyCon)
splitConstrainedType (forall a. Typed a => a -> Term TyCon
typ Value Identity
val)

isOp :: String -> Bool
isOp :: String -> Bool
isOp String
"[]" = Bool
False
isOp (Char
'"':String
_) = Bool
False
isOp String
xs | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== Char
'.') String
xs = Bool
True
isOp String
xs = Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isIdent String
xs)
  where
    isIdent :: Char -> Bool
isIdent Char
x = Char -> Bool
isAlphaNum Char
x Bool -> Bool -> Bool
|| Char
x forall a. Eq a => a -> a -> Bool
== Char
'\'' Bool -> Bool -> Bool
|| Char
x forall a. Eq a => a -> a -> Bool
== Char
'_' Bool -> Bool -> Bool
|| Char
x forall a. Eq a => a -> a -> Bool
== Char
'.'

-- Get selectors of a predicate
selectors :: Constant -> [Constant]
selectors :: Constant -> [Constant]
selectors Constant
con =
  case Constant -> Classification Constant
con_classify Constant
con of
    Predicate{[Constant]
Term TyCon
Term Constant
clas_true :: forall fun. Classification fun -> Term fun
clas_test_case :: forall fun. Classification fun -> Term TyCon
clas_selectors :: forall fun. Classification fun -> [fun]
clas_true :: Term Constant
clas_test_case :: Term TyCon
clas_selectors :: [Constant]
..} -> [Constant]
clas_selectors
    Classification Constant
_ -> []

-- Move the constraints of a constant back into the main type
unhideConstraint :: Constant -> Constant
unhideConstraint :: Constant -> Constant
unhideConstraint Constant
con =
  Constant
con {
    con_type :: Term TyCon
con_type = forall a. Typed a => a -> Term TyCon
typ (Constant -> Value Identity
con_value Constant
con),
    con_constraints :: [Term TyCon]
con_constraints = [] }

instance Typed Constant where
  typ :: Constant -> Term TyCon
typ = Constant -> Term TyCon
con_type
  otherTypesDL :: Constant -> DList (Term TyCon)
otherTypesDL Constant
con =
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Typed a => a -> Term TyCon
typ (Constant -> Value Identity
con_value Constant
con)) forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
    case Constant -> Classification Constant
con_classify Constant
con of
      Predicate{[Constant]
Term TyCon
Term Constant
clas_true :: Term Constant
clas_test_case :: Term TyCon
clas_selectors :: [Constant]
clas_true :: forall fun. Classification fun -> Term fun
clas_test_case :: forall fun. Classification fun -> Term TyCon
clas_selectors :: forall fun. Classification fun -> [fun]
..} ->
        -- Don't call typesDL on clas_selectors because it in turn
        -- contains a reference to the predicate
        forall a. Typed a => a -> DList (Term TyCon)
typesDL (forall a b. (a -> b) -> [a] -> [b]
map Constant -> Value Identity
con_value [Constant]
clas_selectors) forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. Typed a => a -> DList (Term TyCon)
typesDL Term TyCon
clas_test_case forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. Typed a => a -> DList (Term TyCon)
typesDL Term Constant
clas_true
      Selector{Int
Term TyCon
Constant
clas_pred :: forall fun. Classification fun -> fun
clas_index :: forall fun. Classification fun -> Int
clas_test_case :: Term TyCon
clas_pred :: Constant
clas_index :: Int
clas_test_case :: forall fun. Classification fun -> Term TyCon
..} ->
        forall a. Typed a => a -> DList (Term TyCon)
typesDL Constant
clas_pred forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. Typed a => a -> DList (Term TyCon)
typesDL Term TyCon
clas_test_case
      Classification Constant
Function -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
  typeSubst_ :: (Var -> Builder TyCon) -> Constant -> Constant
typeSubst_ Var -> Builder TyCon
sub Constant
con =
    Constant
con { con_value :: Value Identity
con_value = forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub (Constant -> Value Identity
con_value Constant
con),
          con_type :: Term TyCon
con_type = forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub (Constant -> Term TyCon
con_type Constant
con),
          con_constraints :: [Term TyCon]
con_constraints = forall a b. (a -> b) -> [a] -> [b]
map (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub) (Constant -> [Term TyCon]
con_constraints Constant
con),
          con_classify :: Classification Constant
con_classify = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub) (Constant -> Classification Constant
con_classify Constant
con) }

instance Pretty Constant where
  pPrint :: Constant -> Doc
pPrint = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> String
con_name

instance PrettyTerm Constant where
  termStyle :: Constant -> TermStyle
termStyle = Constant -> TermStyle
con_style

instance Sized Constant where
  size :: Constant -> Int
size = Constant -> Int
con_size

instance Predicate Constant where
  classify :: Constant -> Classification Constant
classify = Constant -> Classification Constant
con_classify

evalConstant :: Instances -> Constant -> Maybe (Value Identity)
evalConstant :: Instances -> Constant -> Maybe (Value Identity)
evalConstant Instances
insts Constant{Bool
Int
String
[Term TyCon]
TermStyle
Term TyCon
Value Identity
Classification Constant
con_is_hole :: Bool
con_classify :: Classification Constant
con_size :: Int
con_constraints :: [Term TyCon]
con_type :: Term TyCon
con_value :: Value Identity
con_style :: TermStyle
con_name :: String
con_is_hole :: Constant -> Bool
con_classify :: Constant -> Classification Constant
con_size :: Constant -> Int
con_constraints :: Constant -> [Term TyCon]
con_type :: Constant -> Term TyCon
con_value :: Constant -> Value Identity
con_style :: Constant -> TermStyle
con_name :: Constant -> String
..} = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Value Identity -> Term TyCon -> Maybe (Value Identity)
app Value Identity
con_value [Term TyCon]
con_constraints
  where
    app :: Value Identity -> Term TyCon -> Maybe (Value Identity)
app Value Identity
val Term TyCon
constraint = do
      Value Identity
dict <- Instances -> Term TyCon -> Maybe (Value Identity)
findValue Instances
insts Term TyCon
constraint
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Apply a => a -> a -> a
apply Value Identity
val Value Identity
dict)

class Predicateable a where
  -- A test case for predicates of type a
  -- if `a ~ A -> B -> C -> Bool` we get `TestCase a ~ (A, (B, (C, ())))`
  --
  -- Some speedup should be possible by using unboxed tuples instead...
  type PredicateTestCase a
  type PredicateResult a
  uncrry :: a -> PredicateTestCase a -> PredicateResult a
  true :: proxy a -> Constant

instance Predicateable Bool where
  type PredicateTestCase Bool = ()
  type PredicateResult Bool = Bool
  uncrry :: Bool -> PredicateTestCase Bool -> PredicateResult Bool
uncrry = forall a b. a -> b -> a
const
  true :: forall (proxy :: * -> *). proxy Bool -> Constant
true proxy Bool
_ = forall a. Typeable a => String -> a -> Constant
con String
"True" Bool
True

instance forall a b. (Predicateable b, Typeable a) => Predicateable (a -> b) where
  type PredicateTestCase (a -> b) = (a, PredicateTestCase b)
  type PredicateResult (a -> b) = PredicateResult b
  uncrry :: (a -> b) -> PredicateTestCase (a -> b) -> PredicateResult (a -> b)
uncrry a -> b
f (a
a, PredicateTestCase b
b) = forall a.
Predicateable a =>
a -> PredicateTestCase a -> PredicateResult a
uncrry (a -> b
f a
a) PredicateTestCase b
b
  true :: forall (proxy :: * -> *). proxy (a -> b) -> Constant
true proxy (a -> b)
_ = forall a (proxy :: * -> *). Predicateable a => proxy a -> Constant
true (forall {k} (t :: k). Proxy t
Proxy :: Proxy b)

-- A more user-friendly type for PredicateTestCase.
type FriendlyPredicateTestCase a = Friendly (PredicateTestCase a)
class HasFriendly a where
  type Friendly a
  unfriendly :: Friendly a -> a
instance HasFriendly () where
  type Friendly () = ()
  unfriendly :: Friendly () -> ()
unfriendly () = ()
instance HasFriendly (a, ()) where
  type Friendly (a, ()) = a
  unfriendly :: Friendly (a, ()) -> (a, ())
unfriendly Friendly (a, ())
a = (Friendly (a, ())
a, ())
instance HasFriendly (a, (b, ())) where
  type Friendly (a, (b, ())) = (a, b)
  unfriendly :: Friendly (a, (b, ())) -> (a, (b, ()))
unfriendly (a
a, b
b) = (a
a, (b
b, ()))
instance HasFriendly (a, (b, (c, ()))) where
  type Friendly (a, (b, (c, ()))) = (a, b, c)
  unfriendly :: Friendly (a, (b, (c, ()))) -> (a, (b, (c, ())))
unfriendly (a
a, b
b, c
c) = (a
a, (b
b, (c
c, ())))
instance HasFriendly (a, (b, (c, (d, ())))) where
  type Friendly (a, (b, (c, (d, ())))) = (a, b, c, d)
  unfriendly :: Friendly (a, (b, (c, (d, ())))) -> (a, (b, (c, (d, ()))))
unfriendly (a
a, b
b, c
c, d
d) = (a
a, (b
b, (c
c, (d
d, ()))))

data TestCaseWrapped (t :: Symbol) a = TestCaseWrapped { forall (t :: Symbol) a. TestCaseWrapped t a -> a
unTestCaseWrapped :: a }

unfriendlyPredicateGen :: forall a b. ( Predicateable a
                       , Typeable a
                       , Typeable b
                       , Typeable (PredicateTestCase a))
                       => String -> a -> (b -> Gen (PredicateTestCase a)) -> (Instances, Constant)
unfriendlyPredicateGen :: forall a b.
(Predicateable a, Typeable a, Typeable b,
 Typeable (PredicateTestCase a)) =>
String
-> a -> (b -> Gen (PredicateTestCase a)) -> (Instances, Constant)
unfriendlyPredicateGen String
name a
pred b -> Gen (PredicateTestCase a)
gen =
  let
    -- The following doesn't compile on GHC 7.10:
    -- ty = typeRep (Proxy :: Proxy (TestCaseWrapped sym (PredicateTestCase a)))
    -- (where sym was created using someSymbolVal)
    -- So do it by hand instead:
    ty :: Term TyCon
ty = forall a. Typed a => a -> a
addName (forall k (a :: k) (proxy :: k -> *).
Typeable a =>
proxy a -> Term TyCon
typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy (TestCaseWrapped SymA (PredicateTestCase a))))

    -- Replaces SymA with 'String name'
    -- (XXX: not correct if the type 'a' also contains SymA)
    addName :: forall a. Typed a => a -> a
    addName :: forall a. Typed a => a -> a
addName = forall a s.
(Typed a, Substitution s, SubstFun s ~ TyCon) =>
s -> a -> a
typeSubst Var -> Builder (BuildFun (Term TyCon))
sub
      where
        sub :: Var -> Builder (BuildFun (Term TyCon))
sub Var
x
          | forall a. Build a => a -> Term (BuildFun a)
Twee.build (forall f. Var -> Builder f
Twee.var Var
x) forall a. Eq a => a -> a -> Bool
== forall k (a :: k) (proxy :: k -> *).
Typeable a =>
proxy a -> Term TyCon
typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy SymA) =
            forall a. Build a => a -> Builder (BuildFun a)
Twee.builder (TyCon -> Term TyCon
typeFromTyCon (String -> TyCon
String String
name))
          | Bool
otherwise = forall f. Var -> Builder f
Twee.var Var
x

    instances :: Instances
instances =
      forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Value Identity -> Instances
valueInst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Typed a => a -> a
addName)
        [forall (f :: * -> *) a. Typeable a => f a -> Value f
toValue (forall a. a -> Identity a
Identity b -> Gen (TestCaseWrapped SymA (PredicateTestCase a))
inst1), forall (f :: * -> *) a. Typeable a => f a -> Value f
toValue (forall a. a -> Identity a
Identity Names (TestCaseWrapped SymA (PredicateTestCase a))
inst2)]

    inst1 :: b -> Gen (TestCaseWrapped SymA (PredicateTestCase a))
    inst1 :: b -> Gen (TestCaseWrapped SymA (PredicateTestCase a))
inst1 b
x = forall (t :: Symbol) a. a -> TestCaseWrapped t a
TestCaseWrapped forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> Gen (PredicateTestCase a)
gen b
x

    inst2 :: Names (TestCaseWrapped SymA (PredicateTestCase a))
    inst2 :: Names (TestCaseWrapped SymA (PredicateTestCase a))
inst2 = forall a. [String] -> Names a
Names [String
name forall a. [a] -> [a] -> [a]
++ String
"_var"]

    conPred :: Constant
conPred = (forall a. Typeable a => String -> a -> Constant
con String
name a
pred) { con_classify :: Classification Constant
con_classify = forall fun. [fun] -> Term TyCon -> Term fun -> Classification fun
Predicate [Constant]
conSels Term TyCon
ty (forall f. f -> Term f
Fun (forall a (proxy :: * -> *). Predicateable a => proxy a -> Constant
true (forall {k} (t :: k). Proxy t
Proxy :: Proxy a))) }
    conSels :: [Constant]
conSels = [ (String -> Value Identity -> Constant
constant' (String
name forall a. [a] -> [a] -> [a]
++ String
"_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i) (Int -> Value Identity
select (Int
i forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length (Constant -> [Term TyCon]
con_constraints Constant
conPred)))) { con_classify :: Classification Constant
con_classify = forall fun. Int -> fun -> Term TyCon -> Classification fun
Selector Int
i Constant
conPred Term TyCon
ty, con_size :: Int
con_size = Int
0 } | Int
i <- [Int
0..Term TyCon -> Int
typeArity (forall a. Typed a => a -> Term TyCon
typ Constant
conPred)forall a. Num a => a -> a -> a
-Int
1] ]

    select :: Int -> Value Identity
select Int
i =
      forall a. HasCallStack => Maybe a -> a
fromJust (forall a. Typed a => Term TyCon -> a -> Maybe a
cast ([Term TyCon] -> Term TyCon -> Term TyCon
arrowType [Term TyCon
ty] (Term TyCon -> [Term TyCon]
typeArgs (forall a. Typeable a => a -> Term TyCon
typeOf a
pred) forall a. [a] -> Int -> a
!! Int
i)) (forall a. Poly a -> a
unPoly (Poly (Value Identity)
-> Poly (Value Identity) -> Poly (Value Identity)
compose (Int -> Poly (Value Identity)
sel Int
i) Poly (Value Identity)
unwrapV)))
      where
        compose :: Poly (Value Identity)
-> Poly (Value Identity) -> Poly (Value Identity)
compose Poly (Value Identity)
f Poly (Value Identity)
g = forall a. Apply a => a -> a -> a
apply (forall a. Apply a => a -> a -> a
apply Poly (Value Identity)
cmpV Poly (Value Identity)
f) Poly (Value Identity)
g
        sel :: Int -> Poly (Value Identity)
sel Int
0 = Poly (Value Identity)
fstV
        sel Int
n = Poly (Value Identity)
-> Poly (Value Identity) -> Poly (Value Identity)
compose (Int -> Poly (Value Identity)
sel (Int
nforall a. Num a => a -> a -> a
-Int
1)) Poly (Value Identity)
sndV
        fstV :: Poly (Value Identity)
fstV = forall (f :: * -> *) a.
(Applicative f, Typeable a) =>
a -> Poly (Value f)
toPolyValue (forall a b. (a, b) -> a
fst :: (A, B) -> A)
        sndV :: Poly (Value Identity)
sndV = forall (f :: * -> *) a.
(Applicative f, Typeable a) =>
a -> Poly (Value f)
toPolyValue (forall a b. (a, b) -> b
snd :: (A, B) -> B)
        cmpV :: Poly (Value Identity)
cmpV = forall (f :: * -> *) a.
(Applicative f, Typeable a) =>
a -> Poly (Value f)
toPolyValue (forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) :: (B -> C) -> (A -> B) -> A -> C)
        unwrapV :: Poly (Value Identity)
unwrapV = forall (f :: * -> *) a.
(Applicative f, Typeable a) =>
a -> Poly (Value f)
toPolyValue (forall (t :: Symbol) a. TestCaseWrapped t a -> a
unTestCaseWrapped :: TestCaseWrapped SymA A -> A)
  in
    (Instances
instances, Constant
conPred)

-- | Declare a predicate with a given name and value.
-- The predicate should have type @... -> Bool@.
-- Uses an explicit generator.
predicateGen :: forall a. ( Predicateable a
             , Typeable a
             , Typeable (PredicateTestCase a)
             , HasFriendly (PredicateTestCase a))
             => String -> a -> (Gen (FriendlyPredicateTestCase a)) -> (Instances, Constant)
predicateGen :: forall a.
(Predicateable a, Typeable a, Typeable (PredicateTestCase a),
 HasFriendly (PredicateTestCase a)) =>
String
-> a -> Gen (FriendlyPredicateTestCase a) -> (Instances, Constant)
predicateGen String
name a
pred Gen (FriendlyPredicateTestCase a)
gen =
  forall a b.
(Predicateable a, Typeable a, Typeable b,
 Typeable (PredicateTestCase a)) =>
String
-> a -> (b -> Gen (PredicateTestCase a)) -> (Instances, Constant)
unfriendlyPredicateGen String
name a
pred (\() -> forall a. HasFriendly a => Friendly a -> a
unfriendly forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (FriendlyPredicateTestCase a)
gen)

-- | Declare a predicate with a given name and value.
-- The predicate should have type @... -> Bool@.
predicate :: forall a. ( Predicateable a
          , PredicateResult a ~ Bool
          , Typeable a
          , Typeable (PredicateTestCase a))
          => String -> a -> (Instances, Constant)
predicate :: forall a.
(Predicateable a, PredicateResult a ~ Bool, Typeable a,
 Typeable (PredicateTestCase a)) =>
String -> a -> (Instances, Constant)
predicate String
name a
pred = forall a b.
(Predicateable a, Typeable a, Typeable b,
 Typeable (PredicateTestCase a)) =>
String
-> a -> (b -> Gen (PredicateTestCase a)) -> (Instances, Constant)
unfriendlyPredicateGen String
name a
pred Dict (Arbitrary (PredicateTestCase a)) -> Gen (PredicateTestCase a)
inst
  where
    inst :: Dict (Arbitrary (PredicateTestCase a)) -> Gen (PredicateTestCase a)
    inst :: Dict (Arbitrary (PredicateTestCase a)) -> Gen (PredicateTestCase a)
inst Dict (Arbitrary (PredicateTestCase a))
Dict = forall a. Arbitrary a => Gen a
arbitrary forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` forall a.
Predicateable a =>
a -> PredicateTestCase a -> PredicateResult a
uncrry a
pred

-- | How QuickSpec should style equations.
data PrintStyle
  = ForHumans
  | ForQuickCheck
  deriving (PrintStyle -> PrintStyle -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PrintStyle -> PrintStyle -> Bool
$c/= :: PrintStyle -> PrintStyle -> Bool
== :: PrintStyle -> PrintStyle -> Bool
$c== :: PrintStyle -> PrintStyle -> Bool
Eq, Eq PrintStyle
PrintStyle -> PrintStyle -> Bool
PrintStyle -> PrintStyle -> Ordering
PrintStyle -> PrintStyle -> PrintStyle
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: PrintStyle -> PrintStyle -> PrintStyle
$cmin :: PrintStyle -> PrintStyle -> PrintStyle
max :: PrintStyle -> PrintStyle -> PrintStyle
$cmax :: PrintStyle -> PrintStyle -> PrintStyle
>= :: PrintStyle -> PrintStyle -> Bool
$c>= :: PrintStyle -> PrintStyle -> Bool
> :: PrintStyle -> PrintStyle -> Bool
$c> :: PrintStyle -> PrintStyle -> Bool
<= :: PrintStyle -> PrintStyle -> Bool
$c<= :: PrintStyle -> PrintStyle -> Bool
< :: PrintStyle -> PrintStyle -> Bool
$c< :: PrintStyle -> PrintStyle -> Bool
compare :: PrintStyle -> PrintStyle -> Ordering
$ccompare :: PrintStyle -> PrintStyle -> Ordering
Ord, Int -> PrintStyle -> String -> String
[PrintStyle] -> String -> String
PrintStyle -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [PrintStyle] -> String -> String
$cshowList :: [PrintStyle] -> String -> String
show :: PrintStyle -> String
$cshow :: PrintStyle -> String
showsPrec :: Int -> PrintStyle -> String -> String
$cshowsPrec :: Int -> PrintStyle -> String -> String
Show, ReadPrec [PrintStyle]
ReadPrec PrintStyle
Int -> ReadS PrintStyle
ReadS [PrintStyle]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [PrintStyle]
$creadListPrec :: ReadPrec [PrintStyle]
readPrec :: ReadPrec PrintStyle
$creadPrec :: ReadPrec PrintStyle
readList :: ReadS [PrintStyle]
$creadList :: ReadS [PrintStyle]
readsPrec :: Int -> ReadS PrintStyle
$creadsPrec :: Int -> ReadS PrintStyle
Read, PrintStyle
forall a. a -> a -> Bounded a
maxBound :: PrintStyle
$cmaxBound :: PrintStyle
minBound :: PrintStyle
$cminBound :: PrintStyle
Bounded, Int -> PrintStyle
PrintStyle -> Int
PrintStyle -> [PrintStyle]
PrintStyle -> PrintStyle
PrintStyle -> PrintStyle -> [PrintStyle]
PrintStyle -> PrintStyle -> PrintStyle -> [PrintStyle]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: PrintStyle -> PrintStyle -> PrintStyle -> [PrintStyle]
$cenumFromThenTo :: PrintStyle -> PrintStyle -> PrintStyle -> [PrintStyle]
enumFromTo :: PrintStyle -> PrintStyle -> [PrintStyle]
$cenumFromTo :: PrintStyle -> PrintStyle -> [PrintStyle]
enumFromThen :: PrintStyle -> PrintStyle -> [PrintStyle]
$cenumFromThen :: PrintStyle -> PrintStyle -> [PrintStyle]
enumFrom :: PrintStyle -> [PrintStyle]
$cenumFrom :: PrintStyle -> [PrintStyle]
fromEnum :: PrintStyle -> Int
$cfromEnum :: PrintStyle -> Int
toEnum :: Int -> PrintStyle
$ctoEnum :: Int -> PrintStyle
pred :: PrintStyle -> PrintStyle
$cpred :: PrintStyle -> PrintStyle
succ :: PrintStyle -> PrintStyle
$csucc :: PrintStyle -> PrintStyle
Enum)

data Config =
  Config {
    Config -> Config
cfg_quickCheck :: QuickCheck.Config,
    Config -> Config
cfg_twee :: Twee.Config,
    Config -> Int
cfg_max_size :: Int,
    Config -> Int
cfg_max_commutative_size :: Int,
    Config -> Int
cfg_max_functions :: Int,
    Config -> Instances
cfg_instances :: Instances,
    -- This represents the constants for a series of runs of QuickSpec.
    -- Each index in cfg_constants represents one run of QuickSpec.
    -- head cfg_constants contains all the background functions.
    Config -> [[Constant]]
cfg_constants :: [[Constant]],
    Config -> Term TyCon
cfg_default_to :: Type,
    Config -> Bool
cfg_infer_instance_types :: Bool,
    Config -> [Prop (Term Constant)]
cfg_background :: [Prop (Term Constant)],
    Config -> Prop (Term Constant) -> Bool
cfg_print_filter :: Prop (Term Constant) -> Bool,
    Config -> PrintStyle
cfg_print_style :: PrintStyle,
    Config -> Bool
cfg_check_consistency :: Bool
    }

lens_quickCheck :: Lens Config Config
lens_quickCheck = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> Config
cfg_quickCheck (\Config
x Config
y -> Config
y { cfg_quickCheck :: Config
cfg_quickCheck = Config
x })
lens_twee :: Lens Config Config
lens_twee = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> Config
cfg_twee (\Config
x Config
y -> Config
y { cfg_twee :: Config
cfg_twee = Config
x })
lens_max_size :: Lens Config Int
lens_max_size = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> Int
cfg_max_size (\Int
x Config
y -> Config
y { cfg_max_size :: Int
cfg_max_size = Int
x })
lens_max_commutative_size :: Lens Config Int
lens_max_commutative_size = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> Int
cfg_max_commutative_size (\Int
x Config
y -> Config
y { cfg_max_commutative_size :: Int
cfg_max_commutative_size = Int
x })
lens_max_functions :: Lens Config Int
lens_max_functions = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> Int
cfg_max_functions (\Int
x Config
y -> Config
y { cfg_max_functions :: Int
cfg_max_functions = Int
x })
lens_instances :: Lens Config Instances
lens_instances = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> Instances
cfg_instances (\Instances
x Config
y -> Config
y { cfg_instances :: Instances
cfg_instances = Instances
x })
lens_constants :: Lens Config [[Constant]]
lens_constants = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> [[Constant]]
cfg_constants (\[[Constant]]
x Config
y -> Config
y { cfg_constants :: [[Constant]]
cfg_constants = [[Constant]]
x })
lens_default_to :: Lens Config (Term TyCon)
lens_default_to = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> Term TyCon
cfg_default_to (\Term TyCon
x Config
y -> Config
y { cfg_default_to :: Term TyCon
cfg_default_to = Term TyCon
x })
lens_infer_instance_types :: Lens Config Bool
lens_infer_instance_types = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> Bool
cfg_infer_instance_types (\Bool
x Config
y -> Config
y { cfg_infer_instance_types :: Bool
cfg_infer_instance_types = Bool
x })
lens_background :: Lens Config [Prop (Term Constant)]
lens_background = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> [Prop (Term Constant)]
cfg_background (\[Prop (Term Constant)]
x Config
y -> Config
y { cfg_background :: [Prop (Term Constant)]
cfg_background = [Prop (Term Constant)]
x })
lens_print_filter :: Lens Config (Prop (Term Constant) -> Bool)
lens_print_filter = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> Prop (Term Constant) -> Bool
cfg_print_filter (\Prop (Term Constant) -> Bool
x Config
y -> Config
y { cfg_print_filter :: Prop (Term Constant) -> Bool
cfg_print_filter = Prop (Term Constant) -> Bool
x })
lens_print_style :: Lens Config PrintStyle
lens_print_style = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> PrintStyle
cfg_print_style (\PrintStyle
x Config
y -> Config
y { cfg_print_style :: PrintStyle
cfg_print_style = PrintStyle
x })
lens_check_consistency :: Lens Config Bool
lens_check_consistency = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens Config -> Bool
cfg_check_consistency (\Bool
x Config
y -> Config
y { cfg_check_consistency :: Bool
cfg_check_consistency = Bool
x })

defaultConfig :: Config
defaultConfig :: Config
defaultConfig =
  Config {
    cfg_quickCheck :: Config
cfg_quickCheck = QuickCheck.Config { cfg_num_tests :: Int
QuickCheck.cfg_num_tests = Int
1000, cfg_max_test_size :: Int
QuickCheck.cfg_max_test_size = Int
100, cfg_fixed_seed :: Maybe QCGen
QuickCheck.cfg_fixed_seed = forall a. Maybe a
Nothing },
    cfg_twee :: Config
cfg_twee = Twee.Config { cfg_max_term_size :: Int
Twee.cfg_max_term_size = forall a. Bounded a => a
minBound, cfg_max_cp_depth :: Int
Twee.cfg_max_cp_depth = forall a. Bounded a => a
maxBound },
    cfg_max_size :: Int
cfg_max_size = Int
7,
    cfg_max_commutative_size :: Int
cfg_max_commutative_size = Int
5,
    cfg_max_functions :: Int
cfg_max_functions = forall a. Bounded a => a
maxBound,
    cfg_instances :: Instances
cfg_instances = forall a. Monoid a => a
mempty,
    cfg_constants :: [[Constant]]
cfg_constants = [],
    cfg_default_to :: Term TyCon
cfg_default_to = forall k (a :: k) (proxy :: k -> *).
Typeable a =>
proxy a -> Term TyCon
typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy Int),
    cfg_infer_instance_types :: Bool
cfg_infer_instance_types = Bool
False,
    cfg_background :: [Prop (Term Constant)]
cfg_background = [],
    cfg_print_filter :: Prop (Term Constant) -> Bool
cfg_print_filter = \Prop (Term Constant)
_ -> Bool
True,
    cfg_print_style :: PrintStyle
cfg_print_style = PrintStyle
ForHumans,
    cfg_check_consistency :: Bool
cfg_check_consistency = Bool
False }

-- Extra types for the universe that come from in-scope instances.
instanceTypes :: Instances -> Config -> [Type]
instanceTypes :: Instances -> Config -> [Term TyCon]
instanceTypes Instances
insts Config{Bool
Int
[[Constant]]
[Prop (Term Constant)]
Term TyCon
Instances
Config
Config
PrintStyle
Prop (Term Constant) -> Bool
cfg_check_consistency :: Bool
cfg_print_style :: PrintStyle
cfg_print_filter :: Prop (Term Constant) -> Bool
cfg_background :: [Prop (Term Constant)]
cfg_infer_instance_types :: Bool
cfg_default_to :: Term TyCon
cfg_constants :: [[Constant]]
cfg_instances :: Instances
cfg_max_functions :: Int
cfg_max_commutative_size :: Int
cfg_max_size :: Int
cfg_twee :: Config
cfg_quickCheck :: Config
cfg_check_consistency :: Config -> Bool
cfg_print_style :: Config -> PrintStyle
cfg_print_filter :: Config -> Prop (Term Constant) -> Bool
cfg_background :: Config -> [Prop (Term Constant)]
cfg_infer_instance_types :: Config -> Bool
cfg_default_to :: Config -> Term TyCon
cfg_constants :: Config -> [[Constant]]
cfg_instances :: Config -> Instances
cfg_max_functions :: Config -> Int
cfg_max_commutative_size :: Config -> Int
cfg_max_size :: Config -> Int
cfg_twee :: Config -> Config
cfg_quickCheck :: Config -> Config
..}
  | Bool -> Bool
not Bool
cfg_infer_instance_types = []
  | Bool
otherwise =
    [ Term TyCon
tv
    | Term TyCon
cls <- [Term TyCon]
dicts,
      Term TyCon
inst <- [Term TyCon]
groundInstances,
      Subst TyCon
sub <- forall a. Maybe a -> [a]
maybeToList (Term TyCon -> Term TyCon -> Maybe (Subst TyCon)
matchType Term TyCon
cls Term TyCon
inst),
      (Var
_, Term TyCon
tv) <- forall f. Subst f -> [(Var, Term f)]
Twee.substToList Subst TyCon
sub ]
  where
    dicts :: [Term TyCon]
dicts =
      forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Constant -> [Term TyCon]
con_constraints (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Constant]]
cfg_constants) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
      forall a. Maybe a -> [a]
maybeToList forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyCon -> Maybe (Term TyCon)
getDictionary

    groundInstances :: [Type]
    groundInstances :: [Term TyCon]
groundInstances =
      [ Term TyCon
dict
      | -- () :- dict
        Twee.App Fun TyCon
tc (Twee.Cons (Twee.App Fun TyCon
unit TermList TyCon
Twee.Empty) (Twee.Cons Term TyCon
dict TermList TyCon
Twee.Empty)) <-
        forall a b. (a -> b) -> [a] -> [b]
map (Term TyCon -> Term TyCon
typeRes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Typed a => a -> Term TyCon
typ) (Instances -> [Poly (Value Identity)]
is_instances Instances
insts),
        forall f. Labelled f => Fun f -> f
Twee.fun_value Fun TyCon
tc forall a. Eq a => a -> a -> Bool
== forall {k} (a :: k) (proxy :: k -> *).
Typeable a =>
proxy a -> TyCon
tyCon (forall {k} (t :: k). Proxy t
Proxy :: Proxy (:-)),
        forall f. Labelled f => Fun f -> f
Twee.fun_value Fun TyCon
unit forall a. Eq a => a -> a -> Bool
== forall {k} (a :: k) (proxy :: k -> *).
Typeable a =>
proxy a -> TyCon
tyCon (forall {k} (t :: k). Proxy t
Proxy :: Proxy (() :: Constraint)),
        forall a. Symbolic a => a -> Bool
Twee.isGround Term TyCon
dict ]

data Warnings =
  Warnings {
    Warnings -> [Term TyCon]
warn_no_generator :: [Type],
    Warnings -> [Term TyCon]
warn_no_observer :: [Type] }

warnings :: Universe -> Instances -> Config -> Warnings
warnings :: Universe -> Instances -> Config -> Warnings
warnings Universe
univ Instances
insts Config{Bool
Int
[[Constant]]
[Prop (Term Constant)]
Term TyCon
Instances
Config
Config
PrintStyle
Prop (Term Constant) -> Bool
cfg_check_consistency :: Bool
cfg_print_style :: PrintStyle
cfg_print_filter :: Prop (Term Constant) -> Bool
cfg_background :: [Prop (Term Constant)]
cfg_infer_instance_types :: Bool
cfg_default_to :: Term TyCon
cfg_constants :: [[Constant]]
cfg_instances :: Instances
cfg_max_functions :: Int
cfg_max_commutative_size :: Int
cfg_max_size :: Int
cfg_twee :: Config
cfg_quickCheck :: Config
cfg_check_consistency :: Config -> Bool
cfg_print_style :: Config -> PrintStyle
cfg_print_filter :: Config -> Prop (Term Constant) -> Bool
cfg_background :: Config -> [Prop (Term Constant)]
cfg_infer_instance_types :: Config -> Bool
cfg_default_to :: Config -> Term TyCon
cfg_constants :: Config -> [[Constant]]
cfg_instances :: Config -> Instances
cfg_max_functions :: Config -> Int
cfg_max_commutative_size :: Config -> Int
cfg_max_size :: Config -> Int
cfg_twee :: Config -> Config
cfg_quickCheck :: Config -> Config
..} =
  Warnings {
    warn_no_generator :: [Term TyCon]
warn_no_generator =
      [ Term TyCon
ty | Term TyCon
ty <- [Term TyCon]
types, forall a. Maybe a -> Bool
isNothing (Term TyCon
-> Instances -> Term TyCon -> Maybe (Gen (Value Identity))
findGenerator Term TyCon
cfg_default_to Instances
insts Term TyCon
ty) ],
    warn_no_observer :: [Term TyCon]
warn_no_observer =
      [ Term TyCon
ty | Term TyCon
ty <- [Term TyCon]
types, forall a. Maybe a -> Bool
isNothing (Instances
-> Term TyCon -> Maybe (Gen (Value Identity -> Value Ordy))
findObserver Instances
insts Term TyCon
ty) ] }
  where
    -- Check after defaulting types to Int (or whatever it is)
    types :: [Term TyCon]
types =
      [ Term TyCon
ty
      | Term TyCon
ty <- forall a. Typed a => Term TyCon -> a -> a
defaultTo Term TyCon
cfg_default_to forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. Universe -> Set (Term TyCon)
univ_types forall a b. (a -> b) -> a -> b
$ Universe
univ,
        forall a. Maybe a -> Bool
isNothing (forall (f :: * -> *).
Typeable f =>
Instances -> Term TyCon -> Maybe (Value f)
findInstance Instances
insts Term TyCon
ty :: Maybe (Value NoWarnings)) ]

instance Pretty Warnings where
  pPrint :: Warnings -> Doc
pPrint Warnings{[Term TyCon]
warn_no_observer :: [Term TyCon]
warn_no_generator :: [Term TyCon]
warn_no_observer :: Warnings -> [Term TyCon]
warn_no_generator :: Warnings -> [Term TyCon]
..} =
    [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$
      [Doc -> [Term TyCon] -> Doc
section Doc
genDoc [Term TyCon]
warn_no_generator] forall a. [a] -> [a] -> [a]
++
      [Doc -> [Term TyCon] -> Doc
section Doc
obsDoc [Term TyCon]
warn_no_observer] forall a. [a] -> [a] -> [a]
++
      [String -> Doc
text String
"" | Bool
warnings ]
    where
      warnings :: Bool
warnings = Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term TyCon]
warn_no_generator) Bool -> Bool -> Bool
|| Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term TyCon]
warn_no_observer)
      section :: Doc -> [Term TyCon] -> Doc
section Doc
_ [] = Doc
pPrintEmpty
      section Doc
doc [Term TyCon]
xs =
        Doc
doc Doc -> Doc -> Doc
$$
        Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map Term TyCon -> Doc
pPrintType [Term TyCon]
xs)) Doc -> Doc -> Doc
$$
        String -> Doc
text String
""

      genDoc :: Doc
genDoc =
        String -> Doc
text String
"WARNING: The following types have no 'Arbitrary' instance declared." Doc -> Doc -> Doc
$$
        String -> Doc
text String
"You will not get any variables of the following types:"

      obsDoc :: Doc
obsDoc =
        String -> Doc
text String
"WARNING: The following types have no 'Ord' or 'Observe' instance declared." Doc -> Doc -> Doc
$$
        String -> Doc
text String
"You will not get any equations about the following types:"

quickSpec :: Config -> IO [Prop (Term Constant)]
quickSpec :: Config -> IO [Prop (Term Constant)]
quickSpec cfg :: Config
cfg@Config{Bool
Int
[[Constant]]
[Prop (Term Constant)]
Term TyCon
Instances
Config
Config
PrintStyle
Prop (Term Constant) -> Bool
cfg_check_consistency :: Bool
cfg_print_style :: PrintStyle
cfg_print_filter :: Prop (Term Constant) -> Bool
cfg_background :: [Prop (Term Constant)]
cfg_infer_instance_types :: Bool
cfg_default_to :: Term TyCon
cfg_constants :: [[Constant]]
cfg_instances :: Instances
cfg_max_functions :: Int
cfg_max_commutative_size :: Int
cfg_max_size :: Int
cfg_twee :: Config
cfg_quickCheck :: Config
cfg_check_consistency :: Config -> Bool
cfg_print_style :: Config -> PrintStyle
cfg_print_filter :: Config -> Prop (Term Constant) -> Bool
cfg_background :: Config -> [Prop (Term Constant)]
cfg_infer_instance_types :: Config -> Bool
cfg_default_to :: Config -> Term TyCon
cfg_constants :: Config -> [[Constant]]
cfg_instances :: Config -> Instances
cfg_max_functions :: Config -> Int
cfg_max_commutative_size :: Config -> Int
cfg_max_size :: Config -> Int
cfg_twee :: Config -> Config
cfg_quickCheck :: Config -> Config
..} = do
  let
    constantsOf :: ([[Constant]] -> [Constant]) -> [Constant]
constantsOf [[Constant]] -> [Constant]
f =
      forall a. Ord a => [a] -> [a]
usort (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall f a. Symbolic f a => a -> [f]
funs forall a b. (a -> b) -> a -> b
$
        [Term Constant
clas_true | Predicate{[Constant]
Term TyCon
Term Constant
clas_test_case :: Term TyCon
clas_selectors :: [Constant]
clas_true :: Term Constant
clas_true :: forall fun. Classification fun -> Term fun
clas_test_case :: forall fun. Classification fun -> Term TyCon
clas_selectors :: forall fun. Classification fun -> [fun]
..} <- forall a b. (a -> b) -> [a] -> [b]
map forall fun. Predicate fun => fun -> Classification fun
classify ([[Constant]] -> [Constant]
f [[Constant]]
cfg_constants)] forall a. [a] -> [a] -> [a]
++
        [forall fun. Classification fun -> Term fun
clas_true (forall fun. Predicate fun => fun -> Classification fun
classify Constant
clas_pred) | Selector{Int
Term TyCon
Constant
clas_test_case :: Term TyCon
clas_index :: Int
clas_pred :: Constant
clas_pred :: forall fun. Classification fun -> fun
clas_index :: forall fun. Classification fun -> Int
clas_test_case :: forall fun. Classification fun -> Term TyCon
..} <- forall a b. (a -> b) -> [a] -> [b]
map forall fun. Predicate fun => fun -> Classification fun
classify ([[Constant]] -> [Constant]
f [[Constant]]
cfg_constants)]) forall a. [a] -> [a] -> [a]
++
      [[Constant]] -> [Constant]
f [[Constant]]
cfg_constants forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Constant -> [Constant]
selectors ([[Constant]] -> [Constant]
f [[Constant]]
cfg_constants)
    constants :: [Constant]
constants = ([[Constant]] -> [Constant]) -> [Constant]
constantsOf forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat

    univ :: Universe
univ = forall fun.
(Typed fun, Predicate fun) =>
[Term TyCon] -> [fun] -> Universe
conditionalsUniverse (Instances -> Config -> [Term TyCon]
instanceTypes Instances
instances Config
cfg) [Constant]
constants
    instances :: Instances
instances = Instances
cfg_instances forall a. Monoid a => a -> a -> a
`mappend` Instances
baseInstances

    eval :: TestCase -> Term Constant -> Maybe (Value Ordy)
eval = Term TyCon
-> Instances -> TestCase -> Term Constant -> Maybe (Value Ordy)
evalHaskell Term TyCon
cfg_default_to Instances
instances
    was_observed :: Term TyCon -> Bool
was_observed = forall a. Maybe a -> Bool
isNothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instances -> Term TyCon -> Maybe (Value OrdInstance)
findOrdInstance Instances
instances  -- it was observed if there is no Ord instance directly in scope

    prettierProp :: [fun] -> (Term fun -> norm) -> Prop (Term fun) -> Prop (Term fun)
prettierProp [fun]
funs Term fun -> norm
norm = forall fun. Eq fun => [fun] -> Prop (Term fun) -> Prop (Term fun)
prettyDefinition [fun]
funs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f norm.
(Eq f, Eq norm) =>
(Term f -> norm) -> Prop (Term f) -> Prop (Term f)
prettyAC Term fun -> norm
norm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall fun.
(PrettyTerm fun, Typed fun, Ord fun, Predicate fun) =>
Prop (Term fun) -> Prop (Term fun)
conditionalise
    prettiestProp :: [Constant]
-> (Term Constant
    -> Norm (Tagged (PartiallyApplied (WithConstructor Constant))))
-> Prop (Term Constant)
-> Doc
prettiestProp [Constant]
funs Term Constant
-> Norm (Tagged (PartiallyApplied (WithConstructor Constant)))
norm = forall fun.
(Typed fun, Apply (Term fun), PrettyTerm fun) =>
(Term TyCon -> [String]) -> Prop (Term fun) -> Doc
prettyProp (Instances -> Term TyCon -> [String]
names Instances
instances) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {fun} {norm}.
(Eq norm, PrettyTerm fun, Typed fun, Ord fun, Predicate fun) =>
[fun] -> (Term fun -> norm) -> Prop (Term fun) -> Prop (Term fun)
prettierProp [Constant]
funs Term Constant
-> Norm (Tagged (PartiallyApplied (WithConstructor Constant)))
norm

    present :: [Constant]
-> Prop (Term Constant)
-> StateT
     (Int, [Prop (Term Constant)])
     (Conditionals
        (Pruner
           (WithConstructor Constant)
           (Tester TestCase (Term Constant) (Value Ordy) Terminal)))
     ()
present [Constant]
funs Prop (Term Constant)
prop = do
      Term Constant
-> Norm (Tagged (PartiallyApplied (WithConstructor Constant)))
norm <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
m (term -> norm)
normaliser
      let prop' :: Prop (Term Constant)
prop' = forall {fun} {norm}.
(Eq norm, PrettyTerm fun, Typed fun, Ord fun, Predicate fun) =>
[fun] -> (Term fun -> norm) -> Prop (Term fun) -> Prop (Term fun)
prettierProp [Constant]
funs Term Constant
-> Norm (Tagged (PartiallyApplied (WithConstructor Constant)))
norm Prop (Term Constant)
prop
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Prop (Term Constant) -> Bool
hasBackgroundPredicates Prop (Term Constant)
prop') Bool -> Bool -> Bool
&& Bool -> Bool
not (Prop (Term Constant) -> Bool
isBackgroundProp Prop (Term Constant)
prop') Bool -> Bool -> Bool
&& Prop (Term Constant) -> Bool
cfg_print_filter Prop (Term Constant)
prop) forall a b. (a -> b) -> a -> b
$ do
        (Int
n :: Int, [Prop (Term Constant)]
props) <- forall (m :: * -> *) s. Monad m => StateT s m s
get
        forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Int
nforall a. Num a => a -> a -> a
+Int
1, [Prop (Term Constant)]
props)
        forall (m :: * -> *). MonadTerminal m => String -> m ()
putLine forall a b. (a -> b) -> a -> b
$
          case PrintStyle
cfg_print_style of
            PrintStyle
ForHumans ->
              forall r. PrintfType r => String -> r
printf String
"%3d. %s" Int
n forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$
                [Constant]
-> (Term Constant
    -> Norm (Tagged (PartiallyApplied (WithConstructor Constant))))
-> Prop (Term Constant)
-> Doc
prettiestProp [Constant]
funs Term Constant
-> Norm (Tagged (PartiallyApplied (WithConstructor Constant)))
norm Prop (Term Constant)
prop Doc -> Doc -> Doc
<+> forall fun. Prop (Term fun) -> Doc
disambiguatePropType Prop (Term Constant)
prop
            PrintStyle
ForQuickCheck ->
              Style -> Doc -> String
renderStyle (Style
style {lineLength :: Int
lineLength = Int
78}) forall a b. (a -> b) -> a -> b
$ Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$
                forall fun.
(Typed fun, Apply (Term fun), PrettyTerm fun) =>
Term TyCon
-> (Term TyCon -> Bool)
-> Int
-> (Term TyCon -> [String])
-> Prop (Term fun)
-> Doc
prettyPropQC
                  Term TyCon
cfg_default_to
                  Term TyCon -> Bool
was_observed
                  Int
n
                  (Instances -> Term TyCon -> [String]
names Instances
instances)
                  Prop (Term Constant)
prop'
                  Doc -> Doc -> Doc
<+> forall fun. Prop (Term fun) -> Doc
disambiguatePropType Prop (Term Constant)
prop

    hasBackgroundPredicates :: Prop (Term Constant) -> Bool
hasBackgroundPredicates ([Equation (Term Constant)]
_ :=>: Term Constant
t :=: Term Constant
u)
      | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Constant
p | Constant
p <- forall f a. Symbolic f a => a -> [f]
funs Term Constant
t, Constant -> Bool
isBackgroundPredicate Constant
p]),
        Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Constant
q | Constant
q <- forall f a. Symbolic f a => a -> [f]
funs Term Constant
u, Constant -> Bool
isBackgroundPredicate Constant
q]) =
        Bool
True
    hasBackgroundPredicates Prop (Term Constant)
_ = Bool
False
    isBackgroundPredicate :: Constant -> Bool
isBackgroundPredicate Constant
p =
      Constant
p forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a. Int -> [a] -> [a]
take Int
1 [[Constant]]
cfg_constants) Bool -> Bool -> Bool
&&
      case forall fun. Predicate fun => fun -> Classification fun
classify Constant
p of
        Predicate{} -> Bool
True
        Classification Constant
_ -> Bool
False

    isBackgroundProp :: Prop (Term Constant) -> Bool
isBackgroundProp Prop (Term Constant)
p =
      Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Constant]
fs) Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Constant
f forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a. Int -> [a] -> [a]
take Int
1 [[Constant]]
cfg_constants) | Constant
f <- [Constant]
fs]
      where
        fs :: [Constant]
fs = forall f a. Symbolic f a => a -> [f]
funs Prop (Term Constant)
p

    -- XXX do this during testing
    constraintsOk :: Constant -> Bool
constraintsOk = forall a b. Ord a => (a -> b) -> a -> b
memo forall a b. (a -> b) -> a -> b
$ \Constant
con ->
      forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ forall a. Maybe a -> Bool
isJust (Instances -> Term TyCon -> Maybe (Value Identity)
findValue Instances
instances (forall a. Typed a => Term TyCon -> a -> a
defaultTo Term TyCon
cfg_default_to Term TyCon
constraint)) | Term TyCon
constraint <- Constant -> [Term TyCon]
con_constraints (forall a s.
(Typed a, Substitution s, SubstFun s ~ TyCon) =>
s -> a -> a
typeSubst Subst TyCon
sub Constant
con) ]
         | Term TyCon
ty <- forall a. Set a -> [a]
Set.toList (Universe -> Set (Term TyCon)
univ_types Universe
univ),
           Subst TyCon
sub <- forall a. Maybe a -> [a]
maybeToList (Term TyCon -> Term TyCon -> Maybe (Subst TyCon)
matchType (Term TyCon -> Term TyCon
typeRes (forall a. Typed a => a -> Term TyCon
typ Constant
con)) Term TyCon
ty) ]

    enumerator :: [Term Constant] -> Enumerator (Term Constant)
enumerator [Term Constant]
cons =
      forall b a. Ord b => (a -> b) -> Enumerator a -> Enumerator a
sortTerms forall f. (Sized f, Typed f) => Term f -> Measure f
measure forall a b. (a -> b) -> a -> b
$
      forall a. (a -> Bool) -> Enumerator a -> Enumerator a
filterEnumerator (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Constant -> Bool
constraintsOk forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f a. Symbolic f a => a -> [f]
funs) forall a b. (a -> b) -> a -> b
$
      forall a. (a -> Bool) -> Enumerator a -> Enumerator a
filterEnumerator (\Term Constant
t -> forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Ord a => [a] -> [a]
usort (forall f a. Symbolic f a => a -> [f]
funs Term Constant
t)) forall a. Ord a => a -> a -> Bool
<= Int
cfg_max_functions) forall a b. (a -> b) -> a -> b
$
      forall a. (a -> Bool) -> Enumerator a -> Enumerator a
filterEnumerator (\Term Constant
t -> forall a. Sized a => a -> Int
size Term Constant
t forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall {a} {a}. (Ord a, Symbolic a a, Predicate a) => a -> [a]
conditions Term Constant
t) forall a. Ord a => a -> a -> Bool
<= Int
cfg_max_size) forall a b. (a -> b) -> a -> b
$
      forall a. Sized a => [a] -> Enumerator a
enumerateConstants [Term Constant]
atomic forall a. Monoid a => a -> a -> a
`mappend` forall a. Apply a => Enumerator a
enumerateApplications
      where
        atomic :: [Term Constant]
atomic = [Term Constant]
cons forall a. [a] -> [a] -> [a]
++ [forall f. Var -> Term f
Var (Term TyCon -> Int -> Var
V Term TyCon
typeVar Int
0)]

    conditions :: a -> [a]
conditions a
t = forall a. Ord a => [a] -> [a]
usort [a
p | a
f <- forall f a. Symbolic f a => a -> [f]
funs a
t, Selector Int
_ a
p Term TyCon
_ <- [forall fun. Predicate fun => fun -> Classification fun
classify a
f]]

    use :: Term TyCon -> VariableUse
use Term TyCon
ty =
      forall {k} (f :: k -> *) b.
(forall (a :: k). f a -> b) -> Value f -> b
ofValue (\(Use VariableUse
x) -> VariableUse
x) forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$
      (forall (f :: * -> *).
Typeable f =>
Instances -> Term TyCon -> Maybe (Value f)
findInstance Instances
instances Term TyCon
ty :: Maybe (Value Use))

    mainOf :: Int
-> ([[Constant]] -> [Constant])
-> ([[Constant]] -> [Constant])
-> StateT
     (Int, [Prop (Term Constant)])
     (Conditionals
        (Pruner
           (WithConstructor Constant)
           (Tester TestCase (Term Constant) (Value Ordy) Terminal)))
     ()
mainOf Int
n [[Constant]] -> [Constant]
f [[Constant]] -> [Constant]
g = do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([[Constant]] -> [Constant]
f [[Constant]]
cfg_constants)) forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *). MonadTerminal m => String -> m ()
putLine forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. (Pretty a, Typed a) => [a] -> Doc
pPrintSignature
          (forall a b. (a -> b) -> [a] -> [b]
map (forall f. f -> Term f
Fun forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Constant
unhideConstraint) ([[Constant]] -> [Constant]
f [[Constant]]
cfg_constants))
        forall (m :: * -> *). MonadTerminal m => String -> m ()
putLine String
""
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
n forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *). MonadTerminal m => String -> m ()
putText (forall a. Pretty a => a -> String
prettyShow (Universe -> Instances -> Config -> Warnings
warnings Universe
univ Instances
instances Config
cfg))
        forall (m :: * -> *). MonadTerminal m => String -> m ()
putLine String
"== Laws =="
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (PrintStyle
cfg_print_style forall a. Eq a => a -> a -> Bool
== PrintStyle
ForQuickCheck) forall a b. (a -> b) -> a -> b
$ do
          forall (m :: * -> *). MonadTerminal m => String -> m ()
putLine String
"quickspec_laws :: [(String, Property)]"
          forall (m :: * -> *). MonadTerminal m => String -> m ()
putLine String
"quickspec_laws ="
      let
        pres :: Prop (Term Constant)
-> StateT
     (Int, [Prop (Term Constant)])
     (Conditionals
        (Pruner
           (WithConstructor Constant)
           (Tester TestCase (Term Constant) (Value Ordy) Terminal)))
     ()
pres Prop (Term Constant)
prop = do
          forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify forall a b. (a -> b) -> a -> b
$ \(Int
k, [Prop (Term Constant)]
props) -> (Int
k, Prop (Term Constant)
propforall a. a -> [a] -> [a]
:[Prop (Term Constant)]
props)
          if Int
n forall a. Eq a => a -> a -> Bool
== Int
0 then forall (m :: * -> *) a. Monad m => a -> m a
return () else [Constant]
-> Prop (Term Constant)
-> StateT
     (Int, [Prop (Term Constant)])
     (Conditionals
        (Pruner
           (WithConstructor Constant)
           (Tester TestCase (Term Constant) (Value Ordy) Terminal)))
     ()
present (([[Constant]] -> [Constant]) -> [Constant]
constantsOf [[Constant]] -> [Constant]
f) Prop (Term Constant)
prop
      forall fun norm result (m :: * -> *) testcase.
(Ord fun, Ord norm, Sized fun, Typed fun, Ord result,
 PrettyTerm fun, MonadPruner (Term fun) norm m,
 MonadTester testcase (Term fun) m, MonadTerminal m) =>
(Prop (Term fun) -> m ())
-> (Term fun -> testcase -> Maybe result)
-> Int
-> Int
-> (Term TyCon -> VariableUse)
-> Universe
-> Enumerator (Term fun)
-> m ()
QuickSpec.Internal.Explore.quickSpec Prop (Term Constant)
-> StateT
     (Int, [Prop (Term Constant)])
     (Conditionals
        (Pruner
           (WithConstructor Constant)
           (Tester TestCase (Term Constant) (Value Ordy) Terminal)))
     ()
pres (forall a b c. (a -> b -> c) -> b -> a -> c
flip TestCase -> Term Constant -> Maybe (Value Ordy)
eval) Int
cfg_max_size Int
cfg_max_commutative_size Term TyCon -> VariableUse
use Universe
univ
        ([Term Constant] -> Enumerator (Term Constant)
enumerator (forall a b. (a -> b) -> [a] -> [b]
map forall f. f -> Term f
Fun (([[Constant]] -> [Constant]) -> [Constant]
constantsOf [[Constant]] -> [Constant]
g)))
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
n forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$ do
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (PrintStyle
cfg_print_style forall a. Eq a => a -> a -> Bool
== PrintStyle
ForQuickCheck) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadTerminal m => String -> m ()
putLine String
"  ]"
        forall (m :: * -> *). MonadTerminal m => String -> m ()
putLine String
""

    main :: StateT
  (Int, [Prop (Term Constant)])
  (Conditionals
     (Pruner
        (WithConstructor Constant)
        (Tester TestCase (Term Constant) (Value Ordy) Terminal)))
  ()
main = do
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Prop (Term Constant)]
cfg_background forall a b. (a -> b) -> a -> b
$ \Prop (Term Constant)
prop -> do
        forall term norm (m :: * -> *).
MonadPruner term norm m =>
Prop term -> m Bool
add Prop (Term Constant)
prop
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Int
-> StateT
     (Int, [Prop (Term Constant)])
     (Conditionals
        (Pruner
           (WithConstructor Constant)
           (Tester TestCase (Term Constant) (Value Ordy) Terminal)))
     ()
round [Int
0..Int
roundsforall a. Num a => a -> a -> a
-Int
1]
      where
        round :: Int
-> StateT
     (Int, [Prop (Term Constant)])
     (Conditionals
        (Pruner
           (WithConstructor Constant)
           (Tester TestCase (Term Constant) (Value Ordy) Terminal)))
     ()
round Int
n = Int
-> ([[Constant]] -> [Constant])
-> ([[Constant]] -> [Constant])
-> StateT
     (Int, [Prop (Term Constant)])
     (Conditionals
        (Pruner
           (WithConstructor Constant)
           (Tester TestCase (Term Constant) (Value Ordy) Terminal)))
     ()
mainOf Int
n (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
take Int
1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
drop Int
n) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
take (Int
nforall a. Num a => a -> a -> a
+Int
1))
        rounds :: Int
rounds = forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Constant]]
cfg_constants

    -- Used in checkConsistency. Generate a term to be used when a
    -- Twee proof contains a hole ("?"), i.e. a don't-care variable.
    hole :: Term TyCon -> Maybe (Term Constant)
hole Term TyCon
ty = do
      -- It doesn't matter what the value of the variable is, so
      -- generate a single random value and use that.
      Value Gen
vgen <- forall (f :: * -> *).
Typeable f =>
Instances -> Term TyCon -> Maybe (Value f)
findInstance Instances
instances Term TyCon
ty :: Maybe (Value Gen)
      let runGen :: Gen a -> Identity a
runGen Gen a
g = forall a. a -> Identity a
Identity (forall a. Gen a -> QCGen -> Int -> a
unGen Gen a
g (Int -> QCGen
mkQCGen Int
1234) Int
5)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall f. f -> Term f
Fun forall a b. (a -> b) -> a -> b
$ (String -> Value Identity -> Constant
constant' String
"hole" (forall {k} (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a) -> Value f -> Value g
mapValue forall {a}. Gen a -> Identity a
runGen Value Gen
vgen)) { con_is_hole :: Bool
con_is_hole = Bool
True }

    -- Remove holes by replacing them with a fresh variable.
    removeHoles :: Prop (Term Constant) -> Prop (Term Constant)
removeHoles Prop (Term Constant)
prop = forall fun1 fun2.
(Term fun1 -> Term fun2) -> Prop (Term fun1) -> Prop (Term fun2)
mapTerm (forall f g. (f -> Term g) -> Term f -> Term g
flatMapFun Constant -> Term Constant
f) Prop (Term Constant)
prop
      where
        f :: Constant -> Term Constant
f Constant
con
          | Constant -> Bool
con_is_hole Constant
con = forall f. Var -> Term f
Var (Term TyCon -> Int -> Var
V (forall a. Typed a => a -> Term TyCon
typ Constant
con) Int
n)
          | Bool
otherwise = forall f. f -> Term f
Fun Constant
con
        n :: Int
n = forall f a. Symbolic f a => a -> Int
freeVar Prop (Term Constant)
prop

    checkConsistency :: StateT
  (Map (Prop (Term Constant)) (Set (Prop (Term Constant))))
  (Conditionals
     (Pruner
        (WithConstructor Constant)
        (Tester TestCase (Term Constant) (Value Ordy) Terminal)))
  ()
checkConsistency = do
      [Theorem (Term Constant)]
thms <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
(Term TyCon -> Maybe term) -> m [Theorem term]
theorems Term TyCon -> Maybe (Term Constant)
hole
      let numThms :: Int
numThms = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Theorem (Term Constant)]
thms
      Term Constant
-> Norm (Tagged (PartiallyApplied (WithConstructor Constant)))
norm <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
m (term -> norm)
normaliser

      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1 :: Int ..] [Theorem (Term Constant)]
thms) forall a b. (a -> b) -> a -> b
$ \(Int
i, Theorem (Term Constant)
thm) -> do
        forall (m :: * -> *). MonadTerminal m => String -> m ()
putStatus (forall r. PrintfType r => String -> r
printf String
"checking laws for consistency: %d/%d" Int
i Int
numThms)
        TestResult TestCase
res <- forall testcase term (m :: * -> *).
MonadTester testcase term m =>
Prop term -> m (TestResult testcase)
test (forall norm. Theorem norm -> Prop norm
prop Theorem (Term Constant)
thm)
        case TestResult TestCase
res of
          TestFailed TestCase
testcase -> do
            forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall norm. Theorem norm -> [(Prop norm, [Prop norm])]
axiomsUsed Theorem (Term Constant)
thm) forall a b. (a -> b) -> a -> b
$ \(Prop (Term Constant)
ax, [Prop (Term Constant)]
insts) ->
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Prop (Term Constant)]
insts forall a b. (a -> b) -> a -> b
$ \Prop (Term Constant)
inst -> do
                TestResult TestCase
res <- forall testcase term (m :: * -> *).
MonadTester testcase term m =>
testcase -> Prop term -> m (TestResult testcase)
retest TestCase
testcase Prop (Term Constant)
inst
                forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall testcase. TestResult testcase -> TestResult ()
testResult TestResult TestCase
res forall a. Eq a => a -> a -> Bool
== forall testcase. testcase -> TestResult testcase
TestFailed ()) forall a b. (a -> b) -> a -> b
$ do
                  forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify (forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith forall a. Ord a => Set a -> Set a -> Set a
Set.union (Prop (Term Constant) -> Prop (Term Constant)
removeHoles Prop (Term Constant)
ax) (forall a. a -> Set a
Set.singleton (Prop (Term Constant) -> Prop (Term Constant)
removeHoles Prop (Term Constant)
inst)))
          TestResult TestCase
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

      Map (Prop (Term Constant)) (Set (Prop (Term Constant)))
falseProps <- forall (m :: * -> *) s. Monad m => StateT s m s
get
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall k a. Map k a -> [(k, a)]
Map.toList Map (Prop (Term Constant)) (Set (Prop (Term Constant)))
falseProps) forall a b. (a -> b) -> a -> b
$ \(Prop (Term Constant)
ax, Set (Prop (Term Constant))
insts) -> do
        forall (m :: * -> *). MonadTerminal m => String -> m ()
putLine (forall r. PrintfType r => String -> r
printf String
"*** Law %s is false!" (forall a. Pretty a => a -> String
prettyShow ([Constant]
-> (Term Constant
    -> Norm (Tagged (PartiallyApplied (WithConstructor Constant))))
-> Prop (Term Constant)
-> Doc
prettiestProp [Constant]
constants Term Constant
-> Norm (Tagged (PartiallyApplied (WithConstructor Constant)))
norm Prop (Term Constant)
ax)))
        forall (m :: * -> *). MonadTerminal m => String -> m ()
putLine String
"False instances:"
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Set a -> [a]
Set.toList Set (Prop (Term Constant))
insts) forall a b. (a -> b) -> a -> b
$ \Prop (Term Constant)
inst -> do
          forall (m :: * -> *). MonadTerminal m => String -> m ()
putLine (forall r. PrintfType r => String -> r
printf String
"  %s is false" (forall a. Pretty a => a -> String
prettyShow ([Constant]
-> (Term Constant
    -> Norm (Tagged (PartiallyApplied (WithConstructor Constant))))
-> Prop (Term Constant)
-> Doc
prettiestProp [Constant]
constants Term Constant
-> Norm (Tagged (PartiallyApplied (WithConstructor Constant)))
norm Prop (Term Constant)
inst)))
        forall (m :: * -> *). MonadTerminal m => String -> m ()
putLine String
""

  forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Terminal a -> IO a
withStdioTerminal forall a b. (a -> b) -> a -> b
$
    forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$
    forall testcase term result (m :: * -> *) a.
Config
-> Gen testcase
-> (testcase -> term -> Maybe result)
-> Tester testcase term result m a
-> Gen (m a)
QuickCheck.run Config
cfg_quickCheck (Term TyCon -> Instances -> Gen TestCase
arbitraryTestCase Term TyCon
cfg_default_to Instances
instances) TestCase -> Term Constant -> Maybe (Value Ordy)
eval forall a b. (a -> b) -> a -> b
$
    forall fun (m :: * -> *) a.
(Sized fun, Typeable fun, Ord fun, Monad m) =>
Config -> Pruner fun m a -> m a
Twee.run Config
cfg_twee { cfg_max_term_size :: Int
Twee.cfg_max_term_size = Config -> Int
Twee.cfg_max_term_size Config
cfg_twee forall a. Ord a => a -> a -> a
`max` Int
cfg_max_size } forall a b. (a -> b) -> a -> b
$
    forall fun norm (m :: * -> *) a.
(PrettyTerm fun, Ord norm,
 MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun,
 MonadTerminal m) =>
[fun] -> Conditionals m a -> m a
runConditionals [Constant]
constants forall a b. (a -> b) -> a -> b
$ do
      [Prop (Term Constant)]
result <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Int
1, []) StateT
  (Int, [Prop (Term Constant)])
  (Conditionals
     (Pruner
        (WithConstructor Constant)
        (Tester TestCase (Term Constant) (Value Ordy) Terminal)))
  ()
main
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
cfg_check_consistency forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT StateT
  (Map (Prop (Term Constant)) (Set (Prop (Term Constant))))
  (Conditionals
     (Pruner
        (WithConstructor Constant)
        (Tester TestCase (Term Constant) (Value Ordy) Terminal)))
  ()
checkConsistency forall k a. Map k a
Map.empty
      forall (m :: * -> *) a. Monad m => a -> m a
return [Prop (Term Constant)]
result