{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}

module PlutusCore.Generators.QuickCheck.GenerateTypes where

import PlutusCore.Generators.QuickCheck.Builtin
import PlutusCore.Generators.QuickCheck.Common
import PlutusCore.Generators.QuickCheck.GenTm
import PlutusCore.Generators.QuickCheck.GenerateKinds ()

import PlutusCore.Builtin
import PlutusCore.Core
import PlutusCore.Default
import PlutusCore.Name.Unique
import PlutusCore.Normalize
import PlutusCore.Pretty
import PlutusCore.Quote (runQuote)
import PlutusIR

import Control.Monad (replicateM, when)
import Control.Monad.Reader (asks, local)
import Data.Foldable
import Data.Map.Strict qualified as Map
import Data.Maybe
import Data.String
import Test.QuickCheck (chooseInt, shuffle)

{- Note [Debugging generators that don't generate well-typed/kinded terms/types]
    This module implements generators for well-typed terms and well-kinded types.
    If you came here after a property like `prop_genTypeCorrect` failed and you
    didn't get a minimal counterexample (because shrinking requries well-typed terms)
    you need to use a different trick. One trick that often works is to add the well-typedness
    check in the generators - e.g. in `genTerm` you can do something like this:
    ```
    genTerm ... = myCheck $ do
      ...
      where
        myCheck gen = do
          (trm, type) <- gen
          if notConformingToExpectedInvariant trm type then
            error (show trm ++ " " ++ show type)
          else
            return (trm, type)
    ```
-}

-- * Generators for well-kinded types

{-| Generate "small" types at a given kind such as builtins, bound variables, bound datatypes,
and lambda abstractions \ t0 ... tn. T -}
genAtomicType :: Kind () -> GenTm (Type TyName DefaultUni ())
genAtomicType :: Kind () -> GenTm (Type TyName DefaultUni ())
genAtomicType Kind ()
k = do
  TypeCtx
tys <- (GenEnv -> TypeCtx) -> GenT (Reader GenEnv) TypeCtx
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> TypeCtx
geTypes
  Map TyName (Datatype TyName Name DefaultUni ())
dts <- (GenEnv -> Map TyName (Datatype TyName Name DefaultUni ()))
-> GenT
     (Reader GenEnv) (Map TyName (Datatype TyName Name DefaultUni ()))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> Map TyName (Datatype TyName Name DefaultUni ())
geDatas
  let atoms :: [Type TyName uni ()]
atoms =
        [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
x | (TyName
x, Kind ()
k') <- TypeCtx -> [(TyName, Kind ())]
forall k a. Map k a -> [(k, a)]
Map.toList TypeCtx
tys, Kind ()
k Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== Kind ()
k']
          [Type TyName uni ()]
-> [Type TyName uni ()] -> [Type TyName uni ()]
forall a. [a] -> [a] -> [a]
++ [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
x | (TyName
x, Datatype ()
_ (TyVarDecl ()
_ TyName
_ Kind ()
k') [TyVarDecl TyName ()]
_ Name
_ [VarDecl TyName Name DefaultUni ()]
_) <- Map TyName (Datatype TyName Name DefaultUni ())
-> [(TyName, Datatype TyName Name DefaultUni ())]
forall k a. Map k a -> [(k, a)]
Map.toList Map TyName (Datatype TyName Name DefaultUni ())
dts, Kind ()
k Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== Kind ()
k']
      genBuiltin :: Gen (Maybe (Type tyname DefaultUni ()))
genBuiltin = (SomeTypeIn DefaultUni -> Type tyname DefaultUni ())
-> Maybe (SomeTypeIn DefaultUni)
-> Maybe (Type tyname DefaultUni ())
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (() -> SomeTypeIn DefaultUni -> Type tyname DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> SomeTypeIn uni -> Type tyname uni ann
TyBuiltin ()) (Maybe (SomeTypeIn DefaultUni)
 -> Maybe (Type tyname DefaultUni ()))
-> Gen (Maybe (SomeTypeIn DefaultUni))
-> Gen (Maybe (Type tyname DefaultUni ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind () -> Gen (Maybe (SomeTypeIn DefaultUni))
genBuiltinTypeOf Kind ()
k
      lam :: Kind () -> Kind () -> GenTm (Type TyName DefaultUni ())
lam Kind ()
k1 Kind ()
k2 = do
        TyName
x <- String -> GenTm TyName
genMaybeFreshTyName String
"a"
        ()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
x Kind ()
k1 (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyName
-> Kind ()
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a. TyName -> Kind () -> GenTm a -> GenTm a
bindTyName TyName
x Kind ()
k1 (Kind () -> GenTm (Type TyName DefaultUni ())
genAtomicType Kind ()
k2)
  -- There's always an atomic type of a given kind, hence the usage of 'deliver': we definitely have
  -- builtin types of kind @*@, and for all other kinds we can generate type lambdas.
  GenT (Reader GenEnv) (Maybe (Type TyName DefaultUni ()))
-> GenTm (Type TyName DefaultUni ())
forall (m :: * -> *) a. Monad m => GenT m (Maybe a) -> GenT m a
deliver (GenT (Reader GenEnv) (Maybe (Type TyName DefaultUni ()))
 -> GenTm (Type TyName DefaultUni ()))
-> GenT (Reader GenEnv) (Maybe (Type TyName DefaultUni ()))
-> GenTm (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$
    [(Int, GenT (Reader GenEnv) (Maybe (Type TyName DefaultUni ())))]
-> GenT (Reader GenEnv) (Maybe (Type TyName DefaultUni ()))
forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
frequency
      [ (Int
7, if [Type TyName Any ()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type TyName Any ()]
forall {uni :: * -> *}. [Type TyName uni ()]
atoms then Maybe (Type TyName DefaultUni ())
-> GenT (Reader GenEnv) (Maybe (Type TyName DefaultUni ()))
forall a. a -> GenT (Reader GenEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Type TyName DefaultUni ())
forall a. Maybe a
Nothing else Type TyName DefaultUni () -> Maybe (Type TyName DefaultUni ())
forall a. a -> Maybe a
Just (Type TyName DefaultUni () -> Maybe (Type TyName DefaultUni ()))
-> GenTm (Type TyName DefaultUni ())
-> GenT (Reader GenEnv) (Maybe (Type TyName DefaultUni ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type TyName DefaultUni ()] -> GenTm (Type TyName DefaultUni ())
forall (m :: * -> *) a. MonadGen m => [a] -> m a
elements [Type TyName DefaultUni ()]
forall {uni :: * -> *}. [Type TyName uni ()]
atoms)
      , (Int
1, Gen (Maybe (Type TyName DefaultUni ()))
-> GenT (Reader GenEnv) (Maybe (Type TyName DefaultUni ()))
forall a. Gen a -> GenT (Reader GenEnv) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen Gen (Maybe (Type TyName DefaultUni ()))
forall {tyname}. Gen (Maybe (Type tyname DefaultUni ()))
genBuiltin)
      , -- There may not be a type variable or a built-in type of the given type, hence we have to
        -- resort to generating a lambda occasionally. Plus it's a lambda that ignores the bound
        -- variable in its body, so it's fine to call it "atomic".
        (Int
3, Maybe (GenTm (Type TyName DefaultUni ()))
-> GenT (Reader GenEnv) (Maybe (Type TyName DefaultUni ()))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => Maybe (m a) -> m (Maybe a)
sequence (Maybe (GenTm (Type TyName DefaultUni ()))
 -> GenT (Reader GenEnv) (Maybe (Type TyName DefaultUni ())))
-> Maybe (GenTm (Type TyName DefaultUni ()))
-> GenT (Reader GenEnv) (Maybe (Type TyName DefaultUni ()))
forall a b. (a -> b) -> a -> b
$ [GenTm (Type TyName DefaultUni ())]
-> Maybe (GenTm (Type TyName DefaultUni ()))
forall a. [a] -> Maybe a
listToMaybe [Kind () -> Kind () -> GenTm (Type TyName DefaultUni ())
lam Kind ()
k1 Kind ()
k2 | KindArrow ()
_ Kind ()
k1 Kind ()
k2 <- [Kind ()
k]])
      ]

-- | Generate a type at a given kind
genType :: Kind () -> GenTm (Type TyName DefaultUni ())
genType :: Kind () -> GenTm (Type TyName DefaultUni ())
genType Kind ()
k = do
  Type TyName DefaultUni ()
ty <-
    (Int -> Int)
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a. (Int -> Int) -> GenTm a -> GenTm a
onAstSize (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
10) (GenTm (Type TyName DefaultUni ())
 -> GenTm (Type TyName DefaultUni ()))
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$
      GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a. GenTm a -> GenTm a -> GenTm a
ifAstSizeZero (Kind () -> GenTm (Type TyName DefaultUni ())
genAtomicType Kind ()
k) (GenTm (Type TyName DefaultUni ())
 -> GenTm (Type TyName DefaultUni ()))
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$
        [(Int, GenTm (Type TyName DefaultUni ()))]
-> GenTm (Type TyName DefaultUni ())
forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
frequency ([(Int, GenTm (Type TyName DefaultUni ()))]
 -> GenTm (Type TyName DefaultUni ()))
-> [(Int, GenTm (Type TyName DefaultUni ()))]
-> GenTm (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$
          [[(Int, GenTm (Type TyName DefaultUni ()))]]
-> [(Int, GenTm (Type TyName DefaultUni ()))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ [(Int
5, Kind () -> GenTm (Type TyName DefaultUni ())
genAtomicType Kind ()
k)]
            , [(Int
10, GenTm (Type TyName DefaultUni ())
genFun) | Kind ()
k Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== () -> Kind ()
forall ann. ann -> Kind ann
Type ()]
            , [(Int
5, GenTm (Type TyName DefaultUni ())
genForall) | Kind ()
k Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== () -> Kind ()
forall ann. ann -> Kind ann
Type ()]
            , [(Int
1, GenTm (Type TyName DefaultUni ())
genIFix) | Kind ()
k Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== () -> Kind ()
forall ann. ann -> Kind ann
Type ()]
            , [(Int
5, Kind () -> Kind () -> GenTm (Type TyName DefaultUni ())
genLam Kind ()
k1 Kind ()
k2) | KindArrow ()
_ Kind ()
k1 Kind ()
k2 <- [Kind ()
k]]
            , [(Int
5, GenTm (Type TyName DefaultUni ())
genApp)]
            , [(Int
3, GenTm (Type TyName DefaultUni ())
genSOP) | Kind ()
k Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== () -> Kind ()
forall ann. ann -> Kind ann
Type ()]
            ]
  Bool
debug <- (GenEnv -> Bool) -> GenT (Reader GenEnv) Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> Bool
geDebug
  Bool -> GenT (Reader GenEnv) () -> GenT (Reader GenEnv) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debug (GenT (Reader GenEnv) () -> GenT (Reader GenEnv) ())
-> GenT (Reader GenEnv) () -> GenT (Reader GenEnv) ()
forall a b. (a -> b) -> a -> b
$ do
    TypeCtx
ctx <- (GenEnv -> TypeCtx) -> GenT (Reader GenEnv) TypeCtx
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> TypeCtx
geTypes
    case TypeCtx -> Type TyName DefaultUni () -> Kind () -> Either String ()
checkKind TypeCtx
ctx Type TyName DefaultUni ()
ty Kind ()
k of
      Right ()
_ -> () -> GenT (Reader GenEnv) ()
forall a. a -> GenT (Reader GenEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      Left String
err ->
        String -> GenT (Reader GenEnv) ()
forall a. HasCallStack => String -> a
error (String -> GenT (Reader GenEnv) ())
-> (Doc Any -> String) -> Doc Any -> GenT (Reader GenEnv) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> GenT (Reader GenEnv) ())
-> Doc Any -> GenT (Reader GenEnv) ()
forall a b. (a -> b) -> a -> b
$
          [Doc Any] -> Doc Any
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
            [ Doc Any
"genType - checkInvariants: type " Doc Any -> Doc Any -> Doc Any
forall a. Semigroup a => a -> a -> a
<> Type TyName DefaultUni () -> Doc Any
forall a ann. PrettyReadable a => a -> Doc ann
prettyReadable Type TyName DefaultUni ()
ty
            , Doc Any
" does not match kind " Doc Any -> Doc Any -> Doc Any
forall a. Semigroup a => a -> a -> a
<> Kind () -> Doc Any
forall a ann. PrettyReadable a => a -> Doc ann
prettyReadable Kind ()
k
            , Doc Any
" in context " Doc Any -> Doc Any -> Doc Any
forall a. Semigroup a => a -> a -> a
<> TypeCtx -> Doc Any
forall a ann. PrettyReadable a => a -> Doc ann
prettyReadable TypeCtx
ctx
            , Doc Any
" with error message " Doc Any -> Doc Any -> Doc Any
forall a. Semigroup a => a -> a -> a
<> String -> Doc Any
forall a. IsString a => String -> a
fromString String
err
            ]
  Type TyName DefaultUni () -> GenTm (Type TyName DefaultUni ())
forall a. a -> GenT (Reader GenEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type TyName DefaultUni ()
ty
  where
    -- This size split keeps us from generating ridiculous types that
    -- grow huge to the left of an arrow or abstraction (See also the
    -- genApp case below). This ratio of 1:7 was not scientifically
    -- established, if you are unhappy about the compleixty of the
    -- type of arguments that are generated tweaking this might
    -- be a good idea.
    genFun :: GenTm (Type TyName DefaultUni ())
genFun = (Type TyName DefaultUni ()
 -> Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> (Type TyName DefaultUni (), Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun ()) ((Type TyName DefaultUni (), Type TyName DefaultUni ())
 -> Type TyName DefaultUni ())
-> GenT
     (Reader GenEnv)
     (Type TyName DefaultUni (), Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> Int
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
-> GenT
     (Reader GenEnv)
     (Type TyName DefaultUni (), Type TyName DefaultUni ())
forall a b. Int -> Int -> GenTm a -> GenTm b -> GenTm (a, b)
astSizeSplit_ Int
1 Int
7 (Kind () -> GenTm (Type TyName DefaultUni ())
genType Kind ()
k) (Kind () -> GenTm (Type TyName DefaultUni ())
genType Kind ()
k)

    genForall :: GenTm (Type TyName DefaultUni ())
genForall = do
      TyName
a <- String -> GenTm TyName
genMaybeFreshTyName String
"a"
      Kind ()
k' <- Gen (Kind ()) -> GenT (Reader GenEnv) (Kind ())
forall a. Gen a -> GenT (Reader GenEnv) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen Gen (Kind ())
forall a. Arbitrary a => Gen a
arbitrary
      (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a b.
(a -> b) -> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
a Kind ()
k') (GenTm (Type TyName DefaultUni ())
 -> GenTm (Type TyName DefaultUni ()))
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ (Int -> Int)
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a. (Int -> Int) -> GenTm a -> GenTm a
onAstSize (Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract Int
1) (GenTm (Type TyName DefaultUni ())
 -> GenTm (Type TyName DefaultUni ()))
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ TyName
-> Kind ()
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a. TyName -> Kind () -> GenTm a -> GenTm a
bindTyName TyName
a Kind ()
k' (GenTm (Type TyName DefaultUni ())
 -> GenTm (Type TyName DefaultUni ()))
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ Kind () -> GenTm (Type TyName DefaultUni ())
genType (Kind () -> GenTm (Type TyName DefaultUni ()))
-> Kind () -> GenTm (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()

    genLam :: Kind () -> Kind () -> GenTm (Type TyName DefaultUni ())
genLam Kind ()
k1 Kind ()
k2 = do
      TyName
a <- String -> GenTm TyName
genMaybeFreshTyName String
"a"
      (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a b.
(a -> b) -> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
a Kind ()
k1) (GenTm (Type TyName DefaultUni ())
 -> GenTm (Type TyName DefaultUni ()))
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ (Int -> Int)
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a. (Int -> Int) -> GenTm a -> GenTm a
onAstSize (Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract Int
1) (GenTm (Type TyName DefaultUni ())
 -> GenTm (Type TyName DefaultUni ()))
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ TyName
-> Kind ()
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a. TyName -> Kind () -> GenTm a -> GenTm a
bindTyName TyName
a Kind ()
k1 (Kind () -> GenTm (Type TyName DefaultUni ())
genType Kind ()
k2)

    genApp :: GenTm (Type TyName DefaultUni ())
genApp = do
      Kind ()
k' <- Gen (Kind ()) -> GenT (Reader GenEnv) (Kind ())
forall a. Gen a -> GenT (Reader GenEnv) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen Gen (Kind ())
forall a. Arbitrary a => Gen a
arbitrary
      (Type TyName DefaultUni ()
 -> Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> (Type TyName DefaultUni (), Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp ()) ((Type TyName DefaultUni (), Type TyName DefaultUni ())
 -> Type TyName DefaultUni ())
-> GenT
     (Reader GenEnv)
     (Type TyName DefaultUni (), Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> Int
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
-> GenT
     (Reader GenEnv)
     (Type TyName DefaultUni (), Type TyName DefaultUni ())
forall a b. Int -> Int -> GenTm a -> GenTm b -> GenTm (a, b)
astSizeSplit_ Int
1 Int
7 (Kind () -> GenTm (Type TyName DefaultUni ())
genType (Kind () -> GenTm (Type TyName DefaultUni ()))
-> Kind () -> GenTm (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ () -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
k' Kind ()
k) (Kind () -> GenTm (Type TyName DefaultUni ())
genType Kind ()
k')

    genIFix :: GenTm (Type TyName DefaultUni ())
genIFix = do
      Kind ()
k' <- Gen (Kind ()) -> GenT (Reader GenEnv) (Kind ())
forall a. Gen a -> GenT (Reader GenEnv) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen Gen (Kind ())
forall a. Arbitrary a => Gen a
arbitrary
      (Type TyName DefaultUni ()
 -> Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> (Type TyName DefaultUni (), Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix ())
        ((Type TyName DefaultUni (), Type TyName DefaultUni ())
 -> Type TyName DefaultUni ())
-> GenT
     (Reader GenEnv)
     (Type TyName DefaultUni (), Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> Int
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
-> GenT
     (Reader GenEnv)
     (Type TyName DefaultUni (), Type TyName DefaultUni ())
forall a b. Int -> Int -> GenTm a -> GenTm b -> GenTm (a, b)
astSizeSplit_
          Int
5
          Int
2
          (Kind () -> GenTm (Type TyName DefaultUni ())
genType (Kind () -> GenTm (Type TyName DefaultUni ()))
-> Kind () -> GenTm (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ Kind () -> Kind ()
toPatFuncKind Kind ()
k')
          (Kind () -> GenTm (Type TyName DefaultUni ())
genType Kind ()
k')

    genSOP :: GenTm (Type TyName DefaultUni ())
genSOP = do
      Int
n <- (GenEnv -> Int) -> GenT (Reader GenEnv) Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> Int
geAstSize
      -- Generate up to five constructors or fewer than that if we don't have much size left.
      Int
iSum <- Gen Int -> GenT (Reader GenEnv) Int
forall a. Gen a -> GenT (Reader GenEnv) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen (Gen Int -> GenT (Reader GenEnv) Int)
-> Gen Int -> GenT (Reader GenEnv) Int
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> Gen Int
chooseInt (Int
0, Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
5 (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
5)
      [Int]
jsProd <-
        Gen [Int] -> GenT (Reader GenEnv) [Int]
forall a. Gen a -> GenT (Reader GenEnv) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen (Gen [Int] -> GenT (Reader GenEnv) [Int])
-> (Gen Int -> Gen [Int]) -> Gen Int -> GenT (Reader GenEnv) [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Gen Int -> Gen [Int]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
iSum (Gen Int -> GenT (Reader GenEnv) [Int])
-> Gen Int -> GenT (Reader GenEnv) [Int]
forall a b. (a -> b) -> a -> b
$
          -- The more constructors a data type has, the less arguments each of them can have.
          -- This is so that we don't generate data types with a large number of constructors each
          -- which takes a large number of arguments.
          (Int, Int) -> Gen Int
chooseInt (Int
0, Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (Int
7 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
iSum) (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
iSum))
      Int
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a. Int -> GenTm a -> GenTm a
withAstSize (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Int]
jsProd) (GenTm (Type TyName DefaultUni ())
 -> GenTm (Type TyName DefaultUni ()))
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$
        () -> [[Type TyName DefaultUni ()]] -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP () ([[Type TyName DefaultUni ()]] -> Type TyName DefaultUni ())
-> GenT (Reader GenEnv) [[Type TyName DefaultUni ()]]
-> GenTm (Type TyName DefaultUni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> GenT (Reader GenEnv) [Type TyName DefaultUni ()])
-> [Int] -> GenT (Reader GenEnv) [[Type TyName DefaultUni ()]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\Int
j -> Int
-> GenTm (Type TyName DefaultUni ())
-> GenT (Reader GenEnv) [Type TyName DefaultUni ()]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
j (GenTm (Type TyName DefaultUni ())
 -> GenT (Reader GenEnv) [Type TyName DefaultUni ()])
-> (Kind () -> GenTm (Type TyName DefaultUni ()))
-> Kind ()
-> GenT (Reader GenEnv) [Type TyName DefaultUni ()]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind () -> GenTm (Type TyName DefaultUni ())
genType (Kind () -> GenT (Reader GenEnv) [Type TyName DefaultUni ()])
-> Kind () -> GenT (Reader GenEnv) [Type TyName DefaultUni ()]
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()) [Int]
jsProd

-- | Generate a closed type at a given kind
genClosedType :: Kind () -> Gen (Type TyName DefaultUni ())
genClosedType :: Kind () -> Gen (Type TyName DefaultUni ())
genClosedType = TypeCtx -> Kind () -> Gen (Type TyName DefaultUni ())
genTypeWithCtx TypeCtx
forall a. Monoid a => a
mempty

-- | Generate a closed type at a given kind
genClosedTypeDebug :: Kind () -> Gen (Type TyName DefaultUni ())
genClosedTypeDebug :: Kind () -> Gen (Type TyName DefaultUni ())
genClosedTypeDebug = TypeCtx -> Kind () -> Gen (Type TyName DefaultUni ())
genTypeWithCtxDebug TypeCtx
forall a. Monoid a => a
mempty

-- | Generate a type in the given context with the given kind.
genTypeWithCtx :: TypeCtx -> Kind () -> Gen (Type TyName DefaultUni ())
genTypeWithCtx :: TypeCtx -> Kind () -> Gen (Type TyName DefaultUni ())
genTypeWithCtx TypeCtx
ctx Kind ()
k = GenTm (Type TyName DefaultUni ())
-> Gen (Type TyName DefaultUni ())
forall a. GenTm a -> Gen a
runGenTm (GenTm (Type TyName DefaultUni ())
 -> Gen (Type TyName DefaultUni ()))
-> GenTm (Type TyName DefaultUni ())
-> Gen (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ (GenEnv -> GenEnv)
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a.
(GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\GenEnv
e -> GenEnv
e {geTypes = ctx}) (Kind () -> GenTm (Type TyName DefaultUni ())
genType Kind ()
k)

-- | Generate a type in the given context with the given kind.
genTypeWithCtxDebug :: TypeCtx -> Kind () -> Gen (Type TyName DefaultUni ())
genTypeWithCtxDebug :: TypeCtx -> Kind () -> Gen (Type TyName DefaultUni ())
genTypeWithCtxDebug TypeCtx
ctx Kind ()
k = GenTm (Type TyName DefaultUni ())
-> Gen (Type TyName DefaultUni ())
forall a. GenTm a -> Gen a
runGenTm (GenTm (Type TyName DefaultUni ())
 -> Gen (Type TyName DefaultUni ()))
-> GenTm (Type TyName DefaultUni ())
-> Gen (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ (GenEnv -> GenEnv)
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a.
(GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\GenEnv
e -> GenEnv
e {geTypes = ctx}) (GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a. GenTm a -> GenTm a
withDebug (GenTm (Type TyName DefaultUni ())
 -> GenTm (Type TyName DefaultUni ()))
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ Kind () -> GenTm (Type TyName DefaultUni ())
genType Kind ()
k)

-- | Generate a well-kinded type and its kind in a given context
genKindAndTypeWithCtx :: TypeCtx -> Gen (Kind (), Type TyName DefaultUni ())
genKindAndTypeWithCtx :: TypeCtx -> Gen (Kind (), Type TyName DefaultUni ())
genKindAndTypeWithCtx TypeCtx
ctx = do
  Kind ()
k <- Gen (Kind ())
forall a. Arbitrary a => Gen a
arbitrary
  GenTm (Kind (), Type TyName DefaultUni ())
-> Gen (Kind (), Type TyName DefaultUni ())
forall a. GenTm a -> Gen a
runGenTm (GenTm (Kind (), Type TyName DefaultUni ())
 -> Gen (Kind (), Type TyName DefaultUni ()))
-> GenTm (Kind (), Type TyName DefaultUni ())
-> Gen (Kind (), Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ (GenEnv -> GenEnv)
-> GenTm (Kind (), Type TyName DefaultUni ())
-> GenTm (Kind (), Type TyName DefaultUni ())
forall a.
(GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\GenEnv
e -> GenEnv
e {geTypes = ctx}) ((Kind ()
k,) (Type TyName DefaultUni () -> (Kind (), Type TyName DefaultUni ()))
-> GenTm (Type TyName DefaultUni ())
-> GenTm (Kind (), Type TyName DefaultUni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind () -> GenTm (Type TyName DefaultUni ())
genType Kind ()
k)

-- | Get the kind of a builtin
builtinKind :: SomeTypeIn DefaultUni -> Kind ()
builtinKind :: SomeTypeIn DefaultUni -> Kind ()
builtinKind (SomeTypeIn DefaultUni (Esc a)
t) = DefaultUni (Esc a) -> Kind ()
forall {k} (uni :: * -> *) (a :: k).
ToKind uni =>
uni (Esc a) -> Kind ()
kindOfBuiltinType DefaultUni (Esc a)
t

-- | Generate an arbitrary kind and closed type of that kind.
genKindAndType :: Gen (Kind (), Type TyName DefaultUni ())
genKindAndType :: Gen (Kind (), Type TyName DefaultUni ())
genKindAndType = do
  Kind ()
k <- Gen (Kind ())
forall a. Arbitrary a => Gen a
arbitrary
  Type TyName DefaultUni ()
t <- Kind () -> Gen (Type TyName DefaultUni ())
genClosedType Kind ()
k
  (Kind (), Type TyName DefaultUni ())
-> Gen (Kind (), Type TyName DefaultUni ())
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind ()
k, Type TyName DefaultUni ()
t)

-- | Generate an arbitrary kind and closed type of that kind.
genKindAndTypeDebug :: Gen (Kind (), Type TyName DefaultUni ())
genKindAndTypeDebug :: Gen (Kind (), Type TyName DefaultUni ())
genKindAndTypeDebug = do
  Kind ()
k <- Gen (Kind ())
forall a. Arbitrary a => Gen a
arbitrary
  Type TyName DefaultUni ()
t <- Kind () -> Gen (Type TyName DefaultUni ())
genClosedTypeDebug Kind ()
k
  (Kind (), Type TyName DefaultUni ())
-> Gen (Kind (), Type TyName DefaultUni ())
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind ()
k, Type TyName DefaultUni ()
t)

-- | Normalize a type.
normalizeTy :: Type TyName DefaultUni () -> Type TyName DefaultUni ()
normalizeTy :: Type TyName DefaultUni () -> Type TyName DefaultUni ()
normalizeTy = Normalized (Type TyName DefaultUni ()) -> Type TyName DefaultUni ()
forall a. Normalized a -> a
unNormalized (Normalized (Type TyName DefaultUni ())
 -> Type TyName DefaultUni ())
-> (Type TyName DefaultUni ()
    -> Normalized (Type TyName DefaultUni ()))
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quote (Normalized (Type TyName DefaultUni ()))
-> Normalized (Type TyName DefaultUni ())
forall a. Quote a -> a
runQuote (Quote (Normalized (Type TyName DefaultUni ()))
 -> Normalized (Type TyName DefaultUni ()))
-> (Type TyName DefaultUni ()
    -> Quote (Normalized (Type TyName DefaultUni ())))
-> Type TyName DefaultUni ()
-> Normalized (Type TyName DefaultUni ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type TyName DefaultUni ()
-> Quote (Normalized (Type TyName DefaultUni ()))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann -> m (Normalized (Type tyname uni ann))
normalizeType

-- See Note [Chaotic Good fresh name generation].
-- | Generate a context of free type variables with kinds
genCtx :: Gen TypeCtx
genCtx :: Gen TypeCtx
genCtx = do
  let m :: Int
m = Int
20
  Int
n <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
forall (g :: * -> *) a. (MonadGen g, Random a) => (a, a) -> g a
choose (Int
0, Int
m)
  let xVars :: [TyName]
xVars = [Name -> TyName
TyName (Name -> TyName) -> Name -> TyName
forall a b. (a -> b) -> a -> b
$ Text -> Unique -> Name
Name (String -> Text
forall a. IsString a => String -> a
fromString (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i) (Int -> Unique
forall a. Enum a => Int -> a
toEnum Int
i) | Int
i <- [Int
1 .. Int
m]]
  [TyName]
shuf <- [TyName] -> Gen [TyName]
forall a. [a] -> Gen [a]
shuffle [TyName]
xVars
  let xs :: [TyName]
xs = Int -> [TyName] -> [TyName]
forall a. Int -> [a] -> [a]
take Int
n [TyName]
shuf
  [Kind ()]
ks <- Int -> Gen (Kind ()) -> Gen [Kind ()]
forall (m :: * -> *) a. MonadGen m => Int -> m a -> m [a]
vectorOf Int
n Gen (Kind ())
forall a. Arbitrary a => Gen a
arbitrary
  TypeCtx -> Gen TypeCtx
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeCtx -> Gen TypeCtx) -> TypeCtx -> Gen TypeCtx
forall a b. (a -> b) -> a -> b
$ [(TyName, Kind ())] -> TypeCtx
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(TyName, Kind ())] -> TypeCtx) -> [(TyName, Kind ())] -> TypeCtx
forall a b. (a -> b) -> a -> b
$ [TyName] -> [Kind ()] -> [(TyName, Kind ())]
forall a b. [a] -> [b] -> [(a, b)]
zip [TyName]
xs [Kind ()]
ks