{-# LANGUAGE FlexibleInstances #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

module PlutusCore.Generators.QuickCheck.GenerateKinds where

import PlutusCore.Generators.QuickCheck.GenTm

import PlutusCore

{- Note [Shriking order on kinds]
A kind @k1 = foldr (->) * ks1@ is less than or equal to a kind @k2 = foldr (->) * ks2@ when @ks1@
can be constructed by dropping and shrinking kinds in @ks2@.

This shrinking order means that @* -> (* -> * -> * -> *) -> *@ can shrink to @* -> *@ or @* -> (* ->
*) -> *@ but not to @* -> * -> * -> *@. Not allowing this final shrink is important as we are
guaranteed to only ever reduce the number of type arguments we need to provide when shrinking - thus
allowing us to guarantee that e.g. generated datatypes never increase their number of
parameters. This restriction is important because once the number of parameters starts to grow
during shrinking it is difficult to ensure that the size of generated types and terms doesn't baloon
and cause a shrink-loop.
-}

-- See Note [Shriking order on kinds].
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'

-- | Strict shrinking order on kinds.
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))]

  -- See Note [Shriking order on kinds].
  shrink :: Kind () -> [Kind ()]
shrink (Type ()
_)          = []
  -- Reminder: @a@ can have bigger arity than @a -> b@ so don't shrink to it!
  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)]