{-# 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 [
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),
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),
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,
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),
forall a. Typeable a => a -> Instances
inst (forall a. VariableUse -> Use a
Use (Int -> VariableUse
UpTo Int
4) :: Use A),
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),
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,
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)),
forall a. Typeable a => a -> Instances
inst (forall a. NoWarnings a
NoWarnings :: NoWarnings (TestCaseWrapped SymA A)),
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
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
class (Arbitrary test, Ord outcome) => Observe test outcome a | a -> test outcome where
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
(=~=) :: (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 =~=
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))]
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"
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
data TestCase =
TestCase {
TestCase -> Var -> Maybe (Value Identity)
tc_eval_var :: Var -> Maybe (Value Identity),
TestCase -> Value Identity -> Maybe (Value Ordy)
tc_test_result :: Value Identity -> Maybe (Value Ordy) }
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
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)
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
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)
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))
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))
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
'.'
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
_ -> []
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]
..} ->
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
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)
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
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))))
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)
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)
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
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,
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 }
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
|
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
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
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
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
hole :: Term TyCon -> Maybe (Term Constant)
hole Term TyCon
ty = do
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 }
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