{-# LANGUAGE FlexibleInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module PlutusCore.Generators.QuickCheck.GenerateKinds where
import PlutusCore.Generators.QuickCheck.GenTm
import PlutusCore
leKind :: Kind () -> Kind () -> Bool
leKind :: Kind () -> Kind () -> Bool
leKind Kind ()
k1 Kind ()
k2 = [Kind ()] -> [Kind ()] -> Bool
go ([Kind ()] -> [Kind ()]
forall a. [a] -> [a]
reverse ([Kind ()] -> [Kind ()]) -> [Kind ()] -> [Kind ()]
forall a b. (a -> b) -> a -> b
$ Kind () -> [Kind ()]
forall ann. Kind ann -> [Kind ann]
argsFunKind Kind ()
k1) ([Kind ()] -> [Kind ()]
forall a. [a] -> [a]
reverse ([Kind ()] -> [Kind ()]) -> [Kind ()] -> [Kind ()]
forall a b. (a -> b) -> a -> b
$ Kind () -> [Kind ()]
forall ann. Kind ann -> [Kind ann]
argsFunKind Kind ()
k2)
where
go :: [Kind ()] -> [Kind ()] -> Bool
go [] [Kind ()]
_ = Bool
True
go [Kind ()]
_ [] = Bool
False
go (Kind ()
k : [Kind ()]
ks) (Kind ()
k' : [Kind ()]
ks')
| Kind () -> Kind () -> Bool
leKind Kind ()
k Kind ()
k' = [Kind ()] -> [Kind ()] -> Bool
go [Kind ()]
ks [Kind ()]
ks'
| Bool
otherwise = [Kind ()] -> [Kind ()] -> Bool
go (Kind ()
k Kind () -> [Kind ()] -> [Kind ()]
forall a. a -> [a] -> [a]
: [Kind ()]
ks) [Kind ()]
ks'
ltKind :: Kind () -> Kind () -> Bool
ltKind :: Kind () -> Kind () -> Bool
ltKind Kind ()
k Kind ()
k' = Kind ()
k Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind ()
k' Bool -> Bool -> Bool
&& Kind () -> Kind () -> Bool
leKind Kind ()
k Kind ()
k'
instance Arbitrary (Kind ()) where
arbitrary :: Gen (Kind ())
arbitrary = (Int -> Gen (Kind ())) -> Gen (Kind ())
forall a. (Int -> Gen a) -> Gen a
forall (g :: * -> *) a. MonadGen g => (Int -> g a) -> g a
sized ((Int -> Gen (Kind ())) -> Gen (Kind ()))
-> (Int -> Gen (Kind ())) -> Gen (Kind ())
forall a b. (a -> b) -> a -> b
$ Int -> Gen (Kind ())
forall {t} {f :: * -> *}.
(MonadGen f, Integral t) =>
t -> f (Kind ())
arb (Int -> Gen (Kind ())) -> (Int -> Int) -> Int -> Gen (Kind ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
3)
where
arb :: t -> f (Kind ())
arb t
0 = Kind () -> f (Kind ())
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> f (Kind ())) -> Kind () -> f (Kind ())
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
arb t
n = [(Int, f (Kind ()))] -> f (Kind ())
forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
frequency [(Int
4, Kind () -> f (Kind ())
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind () -> f (Kind ())) -> Kind () -> f (Kind ())
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()),
(Int
1, () -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () (Kind () -> Kind () -> Kind ())
-> f (Kind ()) -> f (Kind () -> Kind ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> f (Kind ())
arb (t -> t -> t
forall a. Integral a => a -> a -> a
div t
n t
6) f (Kind () -> Kind ()) -> f (Kind ()) -> f (Kind ())
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> f (Kind ())
arb (t -> t -> t
forall a. Integral a => a -> a -> a
div (t
5 t -> t -> t
forall a. Num a => a -> a -> a
* t
n) t
6))]
shrink :: Kind () -> [Kind ()]
shrink (Type ()
_) = []
shrink (KindArrow ()
_ Kind ()
a Kind ()
b) = Kind ()
b Kind () -> [Kind ()] -> [Kind ()]
forall a. a -> [a] -> [a]
: [() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
a' Kind ()
b' | (Kind ()
a', Kind ()
b') <- (Kind (), Kind ()) -> [(Kind (), Kind ())]
forall a. Arbitrary a => a -> [a]
shrink (Kind ()
a, Kind ()
b)]