-- editorconfig-checker-disable-file
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE ViewPatterns          #-}

{-# OPTIONS_GHC -Wno-name-shadowing #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}

module PlutusIR.Generators.QuickCheck.GenerateTerms where

import PlutusIR.Generators.QuickCheck.Common

import PlutusCore.Generators.QuickCheck.Builtin
import PlutusCore.Generators.QuickCheck.Common
import PlutusCore.Generators.QuickCheck.GenerateTypes
import PlutusCore.Generators.QuickCheck.GenTm
import PlutusCore.Generators.QuickCheck.ShrinkTypes
import PlutusCore.Generators.QuickCheck.Substitutions
import PlutusCore.Generators.QuickCheck.Unification
import PlutusCore.Generators.QuickCheck.Utils

import PlutusCore.Builtin
import PlutusCore.Core (argsFunKind)
import PlutusCore.Default
import PlutusCore.MkPlc (mkConstantOf)
import PlutusCore.Name.Unique
import PlutusCore.Pretty
import PlutusCore.Subst (typeSubstClosedType)
import PlutusIR
import PlutusIR.Compiler
import PlutusIR.Subst

import Control.Lens ((<&>))
import Control.Monad
import Control.Monad.Except
import Control.Monad.Reader
import Data.Bifunctor
import Data.Default.Class
import Data.Either
import Data.List.NonEmpty (NonEmpty (..))
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Maybe
import Data.Proxy
import Data.Set qualified as Set
import Data.Set.Lens (setOf)
import Data.String
import GHC.Stack
import Prettyprinter

-- | This type keeps track of what kind of argument, term argument (`InstArg`) or
-- type argument (`InstApp`) is required for a function. This type is used primarily
-- with `findInstantiation` below where we do unification to figure out if we can
-- use a variable to construct a term of a target type.
data TyInst = InstApp (Type TyName DefaultUni ()) | InstArg (Type TyName DefaultUni ())
  deriving stock Int -> TyInst -> ShowS
[TyInst] -> ShowS
TyInst -> String
(Int -> TyInst -> ShowS)
-> (TyInst -> String) -> ([TyInst] -> ShowS) -> Show TyInst
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TyInst -> ShowS
showsPrec :: Int -> TyInst -> ShowS
$cshow :: TyInst -> String
show :: TyInst -> String
$cshowList :: [TyInst] -> ShowS
showList :: [TyInst] -> ShowS
Show

instance PrettyBy config (Type TyName DefaultUni ()) => PrettyBy config TyInst where
  prettyBy :: forall ann. config -> TyInst -> Doc ann
prettyBy config
ctx (InstApp Type TyName DefaultUni ()
ty) = config -> Type TyName DefaultUni () -> Doc ann
forall ann. config -> Type TyName DefaultUni () -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
ctx Type TyName DefaultUni ()
ty
  prettyBy config
ctx (InstArg Type TyName DefaultUni ()
ty) = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets (config -> Type TyName DefaultUni () -> Doc ann
forall ann. config -> Type TyName DefaultUni () -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
ctx Type TyName DefaultUni ()
ty)

-- | If successful `findInstantiation n target ty` for an `x :: ty` gives a sequence of `TyInst`s containing `n`
--   `InstArg`s such that `x` instantiated (type application for `InstApp` and applied to a term of
--   the given type for `InstArg`) at the `TyInsts`s has type `target`
findInstantiation :: HasCallStack
                  => TypeCtx
                  -> Int
                  -> Type TyName DefaultUni ()
                  -> Type TyName DefaultUni ()
                  -> Either String [TyInst]
findInstantiation :: HasCallStack =>
TypeCtx
-> Int
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Either String [TyInst]
findInstantiation TypeCtx
ctx Int
n Type TyName DefaultUni ()
target Type TyName DefaultUni ()
ty = do
  TypeSub
sub <- TypeCtx
-> Set TyName
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Either String TypeSub
unifyType (TypeCtx
ctx TypeCtx -> TypeCtx -> TypeCtx
forall a. Semigroup a => a -> a -> a
<> TypeCtx
ctx') Set TyName
flex Type TyName DefaultUni ()
target Type TyName DefaultUni ()
b
  let -- We map any unsolved flexible variable to a 'minimalType'.
      defaultSub :: TypeSub
defaultSub = Kind () -> Type TyName DefaultUni ()
minimalType (Kind () -> Type TyName DefaultUni ()) -> TypeCtx -> TypeSub
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeCtx
ctx'
      doSub :: HasCallStack => _
      doSub :: Type TyName DefaultUni () -> Type TyName DefaultUni ()
doSub = HasCallStack =>
TypeSub -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
TypeSub -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
substType TypeSub
defaultSub (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack =>
TypeSub -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
TypeSub -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
substType TypeSub
sub
      doSubI :: TyInst -> TyInst
doSubI (InstApp Type TyName DefaultUni ()
t) = Type TyName DefaultUni () -> TyInst
InstApp (HasCallStack =>
Type TyName DefaultUni () -> Type TyName DefaultUni ()
Type TyName DefaultUni () -> Type TyName DefaultUni ()
doSub Type TyName DefaultUni ()
t)
      doSubI (InstArg Type TyName DefaultUni ()
t) = Type TyName DefaultUni () -> TyInst
InstArg (HasCallStack =>
Type TyName DefaultUni () -> Type TyName DefaultUni ()
Type TyName DefaultUni () -> Type TyName DefaultUni ()
doSub Type TyName DefaultUni ()
t)
  [TyInst] -> Either String [TyInst]
forall a. a -> Either String a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TyInst] -> Either String [TyInst])
-> [TyInst] -> Either String [TyInst]
forall a b. (a -> b) -> a -> b
$ (TyInst -> TyInst) -> [TyInst] -> [TyInst]
forall a b. (a -> b) -> [a] -> [b]
map TyInst -> TyInst
doSubI [TyInst]
insts
  where
    fvs :: Set TyName
fvs = Getting (Set TyName) (Type TyName DefaultUni ()) TyName
-> Type TyName DefaultUni () -> Set TyName
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set TyName) (Type TyName DefaultUni ()) TyName
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
Traversal' (Type tyname uni ann) tyname
Traversal' (Type TyName DefaultUni ()) TyName
ftvTy Type TyName DefaultUni ()
target Set TyName -> Set TyName -> Set TyName
forall a. Semigroup a => a -> a -> a
<> Getting (Set TyName) (Type TyName DefaultUni ()) TyName
-> Type TyName DefaultUni () -> Set TyName
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set TyName) (Type TyName DefaultUni ()) TyName
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
Traversal' (Type tyname uni ann) tyname
Traversal' (Type TyName DefaultUni ()) TyName
ftvTy Type TyName DefaultUni ()
ty Set TyName -> Set TyName -> Set TyName
forall a. Semigroup a => a -> a -> a
<> TypeCtx -> Set TyName
forall k a. Map k a -> Set k
Map.keysSet TypeCtx
ctx
    (TypeCtx
ctx', Set TyName
flex, [TyInst]
insts, Type TyName DefaultUni ()
b) = TypeCtx
-> Set TyName
-> [TyInst]
-> Int
-> Set TyName
-> Type TyName DefaultUni ()
-> (TypeCtx, Set TyName, [TyInst], Type TyName DefaultUni ())
forall {a}.
(Ord a, Num a) =>
TypeCtx
-> Set TyName
-> [TyInst]
-> a
-> Set TyName
-> Type TyName DefaultUni ()
-> (TypeCtx, Set TyName, [TyInst], Type TyName DefaultUni ())
view TypeCtx
forall k a. Map k a
Map.empty Set TyName
forall a. Set a
Set.empty [] Int
n Set TyName
fvs Type TyName DefaultUni ()
ty

    -- TODO: documentation!
    view :: TypeCtx
-> Set TyName
-> [TyInst]
-> a
-> Set TyName
-> Type TyName DefaultUni ()
-> (TypeCtx, Set TyName, [TyInst], Type TyName DefaultUni ())
view TypeCtx
ctx' Set TyName
flex [TyInst]
insts a
n Set TyName
fvs (TyForall ()
_ TyName
x Kind ()
k Type TyName DefaultUni ()
b) = TypeCtx
-> Set TyName
-> [TyInst]
-> a
-> Set TyName
-> Type TyName DefaultUni ()
-> (TypeCtx, Set TyName, [TyInst], Type TyName DefaultUni ())
view (TyName -> Kind () -> TypeCtx -> TypeCtx
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TyName
x' Kind ()
k TypeCtx
ctx') (TyName -> Set TyName -> Set TyName
forall a. Ord a => a -> Set a -> Set a
Set.insert TyName
x' Set TyName
flex)
                                                         (Type TyName DefaultUni () -> TyInst
InstApp (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
x') TyInst -> [TyInst] -> [TyInst]
forall a. a -> [a] -> [a]
: [TyInst]
insts) a
n
                                                         (TyName -> Set TyName -> Set TyName
forall a. Ord a => a -> Set a -> Set a
Set.insert TyName
x' Set TyName
fvs) Type TyName DefaultUni ()
b'
      where (TyName
x', Type TyName DefaultUni ()
b') | TyName -> Set TyName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member TyName
x Set TyName
fvs = let x' :: TyName
x' = Set TyName -> TyName -> TyName
freshenTyNameWith Set TyName
fvs TyName
x in (TyName
x', TyName
-> TyName -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
renameVar TyName
x TyName
x' Type TyName DefaultUni ()
b)
                     | Bool
otherwise        = (TyName
x, Type TyName DefaultUni ()
b)
    view TypeCtx
ctx' Set TyName
flex [TyInst]
insts a
n Set TyName
fvs (TyFun ()
_ Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b) | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 = TypeCtx
-> Set TyName
-> [TyInst]
-> a
-> Set TyName
-> Type TyName DefaultUni ()
-> (TypeCtx, Set TyName, [TyInst], Type TyName DefaultUni ())
view TypeCtx
ctx' Set TyName
flex (Type TyName DefaultUni () -> TyInst
InstArg Type TyName DefaultUni ()
a TyInst -> [TyInst] -> [TyInst]
forall a. a -> [a] -> [a]
: [TyInst]
insts) (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1) Set TyName
fvs Type TyName DefaultUni ()
b
    view TypeCtx
ctx' Set TyName
flex [TyInst]
insts a
_ Set TyName
_ Type TyName DefaultUni ()
a = (TypeCtx
ctx', Set TyName
flex, [TyInst] -> [TyInst]
forall a. [a] -> [a]
reverse [TyInst]
insts, Type TyName DefaultUni ()
a)

genConstant :: SomeTypeIn DefaultUni -> GenTm (Term TyName Name DefaultUni DefaultFun ())
genConstant :: SomeTypeIn DefaultUni
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
genConstant (SomeTypeIn DefaultUni (Esc a)
b) = case DefaultUni (Esc a) -> SingKind k
forall k (a :: k). DefaultUni (Esc a) -> SingKind k
forall (uni :: * -> *) k (a :: k).
ToKind uni =>
uni (Esc a) -> SingKind k
toSingKind DefaultUni (Esc a)
b of
    SingKind k
SingType -> ()
-> DefaultUni (Esc a)
-> a
-> Term TyName Name DefaultUni DefaultFun ()
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
TermLike term tyname name uni fun =>
ann -> uni (Esc a) -> a -> term ann
mkConstantOf () DefaultUni (Esc a)
DefaultUni (Esc a)
b (a -> Term TyName Name DefaultUni DefaultFun ())
-> GenT (ReaderT GenEnv Identity) a
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy ArbitraryBuiltin
-> DefaultUni (Esc a)
-> (ArbitraryBuiltin a => GenT (ReaderT GenEnv Identity) a)
-> GenT (ReaderT GenEnv Identity) a
forall (uni :: * -> *) (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
forall (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
Everywhere DefaultUni constr =>
proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
bring (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @ArbitraryBuiltin) DefaultUni (Esc a)
DefaultUni (Esc a)
b (Gen a -> GenT (ReaderT GenEnv Identity) a
forall a. Gen a -> GenT (ReaderT GenEnv Identity) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen Gen a
forall a. ArbitraryBuiltin a => Gen a
arbitraryBuiltin)
    SingKind k
_        -> String -> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. HasCallStack => String -> a
error String
"Higher-kinded built-in types cannot be used here"

-- | Try to inhabit a given type in as simple a way as possible,
-- prefers to not default to `error`
inhabitType :: Type TyName DefaultUni () -> GenTm (Term TyName Name DefaultUni DefaultFun ())
inhabitType :: Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
inhabitType Type TyName DefaultUni ()
ty0 = (GenEnv -> GenEnv)
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a.
(GenEnv -> GenEnv)
-> GenT (ReaderT GenEnv Identity) a
-> GenT (ReaderT GenEnv Identity) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ GenEnv
e -> GenEnv
e { geTerms = mempty }) (GenTm (Term TyName Name DefaultUni DefaultFun ())
 -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ do
    Either String (Term TyName Name DefaultUni DefaultFun ())
errOrRes <- ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenTm
     (Either String (Term TyName Name DefaultUni DefaultFun ()))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
 -> GenTm
      (Either String (Term TyName Name DefaultUni DefaultFun ())))
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenTm
     (Either String (Term TyName Name DefaultUni DefaultFun ()))
forall a b. (a -> b) -> a -> b
$ Type TyName DefaultUni ()
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
findTm Type TyName DefaultUni ()
ty0
    Term TyName Name DefaultUni DefaultFun ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. a -> GenT (ReaderT GenEnv Identity) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name DefaultUni DefaultFun ()
 -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ case Either String (Term TyName Name DefaultUni DefaultFun ())
errOrRes of
        Left  String
_   -> ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> Type tyname uni a -> Term tyname name uni fun a
Error () Type TyName DefaultUni ()
ty0
        Right Term TyName Name DefaultUni DefaultFun ()
res -> Term TyName Name DefaultUni DefaultFun ()
res
  where
    -- Do the obvious thing as long as target type is not type var
    -- When type var: magic (if higher-kinded type var: black magic)
    -- Ex: get `a` from D ts ==> get `a` from which ts, get which params from D
    -- This function does not fail to error.
    --
    -- NOTE: because we make recursive calls to findTm in this function instead of
    -- inhabitType we don't risk generating terms that are "mostly ok but something is error",
    -- this function will avoid error if possible.
    findTm :: Type TyName DefaultUni ()
           -> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
    findTm :: Type TyName DefaultUni ()
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
findTm (Type TyName DefaultUni () -> Type TyName DefaultUni ()
normalizeTy -> Type TyName DefaultUni ()
ty) = case Type TyName DefaultUni ()
ty of
      TyFun ()
_ Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b -> do
        Name
x <- GenT (ReaderT GenEnv Identity) Name -> ExceptT String GenTm Name
forall (m :: * -> *) a. Monad m => m a -> ExceptT String m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (GenT (ReaderT GenEnv Identity) Name -> ExceptT String GenTm Name)
-> GenT (ReaderT GenEnv Identity) Name -> ExceptT String GenTm Name
forall a b. (a -> b) -> a -> b
$ String -> GenT (ReaderT GenEnv Identity) Name
genLikelyFreshName String
"x"
        ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs () Name
x Type TyName DefaultUni ()
a (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GenTm (Either String (Term TyName Name DefaultUni DefaultFun ()))
 -> GenTm
      (Either String (Term TyName Name DefaultUni DefaultFun ())))
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *) e a (n :: * -> *) e' b.
(m (Either e a) -> n (Either e' b))
-> ExceptT e m a -> ExceptT e' n b
mapExceptT (Name
-> Type TyName DefaultUni ()
-> GenTm
     (Either String (Term TyName Name DefaultUni DefaultFun ()))
-> GenTm
     (Either String (Term TyName Name DefaultUni DefaultFun ()))
forall a. Name -> Type TyName DefaultUni () -> GenTm a -> GenTm a
bindTmName Name
x Type TyName DefaultUni ()
a) (Type TyName DefaultUni ()
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
findTm Type TyName DefaultUni ()
b)
      TyForall ()
_ TyName
x Kind ()
k Type TyName DefaultUni ()
b -> do
        ()
-> TyName
-> Kind ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs () TyName
x Kind ()
k (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GenTm (Either String (Term TyName Name DefaultUni DefaultFun ()))
 -> GenTm
      (Either String (Term TyName Name DefaultUni DefaultFun ())))
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *) e a (n :: * -> *) e' b.
(m (Either e a) -> n (Either e' b))
-> ExceptT e m a -> ExceptT e' n b
mapExceptT (TyName
-> Kind ()
-> GenTm
     (Either String (Term TyName Name DefaultUni DefaultFun ()))
-> GenTm
     (Either String (Term TyName Name DefaultUni DefaultFun ()))
forall a. TyName -> Kind () -> GenTm a -> GenTm a
bindTyName TyName
x Kind ()
k) (Type TyName DefaultUni ()
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
findTm Type TyName DefaultUni ()
b)
      TyBuiltin ()
_ SomeTypeIn DefaultUni
someUni -> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *) a. Monad m => m a -> ExceptT String m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (GenTm (Term TyName Name DefaultUni DefaultFun ())
 -> ExceptT
      String GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ SomeTypeIn DefaultUni
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
genConstant SomeTypeIn DefaultUni
someUni
      -- If we have a type-function application
      ([Type TyName DefaultUni ()]
-> Type TyName DefaultUni ()
-> (Type TyName DefaultUni (), [Type TyName DefaultUni ()])
forall {tyname} {uni :: * -> *} {ann}.
[Type tyname uni ann]
-> Type tyname uni ann
-> (Type tyname uni ann, [Type tyname uni ann])
viewApp [] -> (Type TyName DefaultUni ()
f, [Type TyName DefaultUni ()]
_)) ->
        case Type TyName DefaultUni ()
f of
          TyVar () TyName
x  -> do
            Map TyName (Datatype TyName Name DefaultUni ())
_ <- (GenEnv -> Map TyName (Datatype TyName Name DefaultUni ()))
-> ExceptT
     String GenTm (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
            (GenEnv -> Maybe (Datatype TyName Name DefaultUni ()))
-> ExceptT
     String GenTm (Maybe (Datatype TyName Name DefaultUni ()))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (TyName
-> Map TyName (Datatype TyName Name DefaultUni ())
-> Maybe (Datatype TyName Name DefaultUni ())
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TyName
x (Map TyName (Datatype TyName Name DefaultUni ())
 -> Maybe (Datatype TyName Name DefaultUni ()))
-> (GenEnv -> Map TyName (Datatype TyName Name DefaultUni ()))
-> GenEnv
-> Maybe (Datatype TyName Name DefaultUni ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenEnv -> Map TyName (Datatype TyName Name DefaultUni ())
geDatas) ExceptT String GenTm (Maybe (Datatype TyName Name DefaultUni ()))
-> (Maybe (Datatype TyName Name DefaultUni ())
    -> ExceptT
         String GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a b.
ExceptT String GenTm a
-> (a -> ExceptT String GenTm b) -> ExceptT String GenTm b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
              -- If the head is a datatype try to inhabit one of its constructors
              Just Datatype TyName Name DefaultUni ()
dat -> (ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
 -> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
 -> ExceptT
      String GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
-> [ExceptT
      String GenTm (Term TyName Name DefaultUni DefaultFun ())]
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a.
ExceptT String GenTm a
-> ExceptT String GenTm a -> ExceptT String GenTm a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. ExceptT String GenTm a
forall (m :: * -> *) a. MonadPlus m => m a
mzero ([ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())]
 -> ExceptT
      String GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> [ExceptT
      String GenTm (Term TyName Name DefaultUni DefaultFun ())]
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ((Name, Type TyName DefaultUni ())
 -> ExceptT
      String GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> [(Name, Type TyName DefaultUni ())]
-> [ExceptT
      String GenTm (Term TyName Name DefaultUni DefaultFun ())]
forall a b. (a -> b) -> [a] -> [b]
map (TyName
-> Type TyName DefaultUni ()
-> (Name, Type TyName DefaultUni ())
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
tryCon TyName
x Type TyName DefaultUni ()
ty) (Datatype TyName Name DefaultUni ()
-> [(Name, Type TyName DefaultUni ())]
constrTypes Datatype TyName Name DefaultUni ()
dat)
              -- If its not a datatype we try to use whatever bound variables
              -- we have to inhabit the type
              Maybe (Datatype TyName Name DefaultUni ())
Nothing  -> do
                Map Name (Type TyName DefaultUni ())
vars <- (GenEnv -> Map Name (Type TyName DefaultUni ()))
-> ExceptT String GenTm (Map Name (Type TyName DefaultUni ()))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> Map Name (Type TyName DefaultUni ())
geTerms
                TypeCtx
ctx  <- (GenEnv -> TypeCtx) -> ExceptT String GenTm TypeCtx
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> TypeCtx
geTypes
                let cands :: [(Name, Type TyName DefaultUni ())]
cands = Map Name (Type TyName DefaultUni ())
-> [(Name, Type TyName DefaultUni ())]
forall k a. Map k a -> [(k, a)]
Map.toList Map Name (Type TyName DefaultUni ())
vars
                    -- If we are instantiating something simply instantiate every
                    -- type application with type required by findInstantiation
                    doInst :: p
-> Term TyName Name DefaultUni DefaultFun ()
-> TyInst
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
doInst p
_ Term TyName Name DefaultUni DefaultFun ()
tm (InstApp Type TyName DefaultUni ()
instTy) = Term TyName Name DefaultUni DefaultFun ()
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. a -> ExceptT String GenTm a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name DefaultUni DefaultFun ()
 -> ExceptT
      String GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst () Term TyName Name DefaultUni DefaultFun ()
tm Type TyName DefaultUni ()
instTy
                    -- If we instantiate an application, only succeed if we find
                    -- a non-error argument.
                    doInst p
_ Term TyName Name DefaultUni DefaultFun ()
tm (InstArg Type TyName DefaultUni ()
argTy)  = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply () Term TyName Name DefaultUni DefaultFun ()
tm (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName DefaultUni ()
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
findTm Type TyName DefaultUni ()
argTy
                -- Go over every type and try to inhabit the type at the arguments
                case [ (GenEnv -> GenEnv)
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a.
(GenEnv -> GenEnv)
-> ExceptT String GenTm a -> ExceptT String GenTm a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\GenEnv
e -> GenEnv
e { geTerms = Map.delete x' (geTerms e) })
                       (ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
 -> ExceptT
      String GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ (Term TyName Name DefaultUni DefaultFun ()
 -> TyInst
 -> ExceptT
      String GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> [TyInst]
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Int
-> Term TyName Name DefaultUni DefaultFun ()
-> TyInst
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall {p}.
p
-> Term TyName Name DefaultUni DefaultFun ()
-> TyInst
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
doInst Int
n) (() -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var () Name
x') [TyInst]
insts
                     | (Name
x', Type TyName DefaultUni ()
a)     <- [(Name, Type TyName DefaultUni ())]
cands,
                       Int
n           <- [Int
0..Type TyName DefaultUni () -> Int
forall a tyname (uni :: * -> *) ann.
Num a =>
Type tyname uni ann -> a
typeArity Type TyName DefaultUni ()
a],
                       Right [TyInst]
insts <- [HasCallStack =>
TypeCtx
-> Int
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Either String [TyInst]
TypeCtx
-> Int
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Either String [TyInst]
findInstantiation TypeCtx
ctx Int
n Type TyName DefaultUni ()
ty Type TyName DefaultUni ()
a],
                       TyName
x TyName -> Set TyName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Type TyName DefaultUni () -> Set TyName
forall {unique} {a} {uni :: * -> *} {ann}.
(Coercible unique Int, Ord a, HasUnique a unique) =>
Type a uni ann -> Set a
fvArgs Type TyName DefaultUni ()
a
                     ] of
                  []  -> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. ExceptT String GenTm a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
                  ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
g:[ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())]
_ -> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
g
          Type TyName DefaultUni ()
_ -> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. ExceptT String GenTm a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

    -- Try to inhabit a constructor `con` of type `conTy` in datatype `d` at type `ty`
    tryCon :: TyName
-> Type TyName DefaultUni ()
-> (Name, Type TyName DefaultUni ())
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
tryCon TyName
d Type TyName DefaultUni ()
ty1 (Name
con, Type TyName DefaultUni ()
conTy)
      | TyName -> Set TyName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member TyName
d (Type TyName DefaultUni () -> Set TyName
forall {unique} {a} {uni :: * -> *} {ann}.
(Coercible unique Int, Ord a, HasUnique a unique) =>
Type a uni ann -> Set a
fvArgs Type TyName DefaultUni ()
conTy) = ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. ExceptT String GenTm a
forall (m :: * -> *) a. MonadPlus m => m a
mzero   -- <- This is ok, since no mutual recursion
      | Bool
otherwise = do
          -- Check that we haven't banned this constructor
          Map Name (Type TyName DefaultUni ())
tmctx <- GenTm (Map Name (Type TyName DefaultUni ()))
-> ExceptT String GenTm (Map Name (Type TyName DefaultUni ()))
forall (m :: * -> *) a. Monad m => m a -> ExceptT String m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (GenTm (Map Name (Type TyName DefaultUni ()))
 -> ExceptT String GenTm (Map Name (Type TyName DefaultUni ())))
-> GenTm (Map Name (Type TyName DefaultUni ()))
-> ExceptT String GenTm (Map Name (Type TyName DefaultUni ()))
forall a b. (a -> b) -> a -> b
$ (GenEnv -> Map Name (Type TyName DefaultUni ()))
-> GenTm (Map Name (Type TyName DefaultUni ()))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> Map Name (Type TyName DefaultUni ())
geTerms
          if Name
-> Map Name (Type TyName DefaultUni ())
-> Maybe (Type TyName DefaultUni ())
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
con Map Name (Type TyName DefaultUni ())
tmctx Maybe (Type TyName DefaultUni ())
-> Maybe (Type TyName DefaultUni ()) -> Bool
forall a. Eq a => a -> a -> Bool
== Type TyName DefaultUni () -> Maybe (Type TyName DefaultUni ())
forall a. a -> Maybe a
Just Type TyName DefaultUni ()
conTy
          then do
            TypeCtx
tyctx <- GenTm TypeCtx -> ExceptT String GenTm TypeCtx
forall (m :: * -> *) a. Monad m => m a -> ExceptT String m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (GenTm TypeCtx -> ExceptT String GenTm TypeCtx)
-> GenTm TypeCtx -> ExceptT String GenTm TypeCtx
forall a b. (a -> b) -> a -> b
$ (GenEnv -> TypeCtx) -> GenTm TypeCtx
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> TypeCtx
geTypes
            [TyInst]
insts0 <- Either String [TyInst] -> ExceptT String GenTm [TyInst]
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either String [TyInst] -> ExceptT String GenTm [TyInst])
-> Either String [TyInst] -> ExceptT String GenTm [TyInst]
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
TypeCtx
-> Int
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Either String [TyInst]
TypeCtx
-> Int
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Either String [TyInst]
findInstantiation TypeCtx
tyctx (Type TyName DefaultUni () -> Int
forall a tyname (uni :: * -> *) ann.
Num a =>
Type tyname uni ann -> a
typeArity Type TyName DefaultUni ()
conTy) Type TyName DefaultUni ()
ty1 Type TyName DefaultUni ()
conTy
            let go :: Term TyName Name DefaultUni DefaultFun ()
-> [TyInst]
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
go Term TyName Name DefaultUni DefaultFun ()
tm [] = Term TyName Name DefaultUni DefaultFun ()
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. a -> ExceptT String GenTm a
forall (m :: * -> *) a. Monad m => a -> m a
return Term TyName Name DefaultUni DefaultFun ()
tm
                go Term TyName Name DefaultUni DefaultFun ()
tm (InstApp Type TyName DefaultUni ()
ty : [TyInst]
insts) = Term TyName Name DefaultUni DefaultFun ()
-> [TyInst]
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
go (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst () Term TyName Name DefaultUni DefaultFun ()
tm Type TyName DefaultUni ()
ty) [TyInst]
insts
                go Term TyName Name DefaultUni DefaultFun ()
tm (InstArg Type TyName DefaultUni ()
ty : [TyInst]
insts) = do
                  Term TyName Name DefaultUni DefaultFun ()
arg <- Type TyName DefaultUni ()
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
findTm Type TyName DefaultUni ()
ty
                  Term TyName Name DefaultUni DefaultFun ()
-> [TyInst]
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
go (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply () Term TyName Name DefaultUni DefaultFun ()
tm Term TyName Name DefaultUni DefaultFun ()
arg) [TyInst]
insts
            Term TyName Name DefaultUni DefaultFun ()
-> [TyInst]
-> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
go (() -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var () Name
con) [TyInst]
insts0
          else ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. ExceptT String GenTm a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

    -- CODE REVIEW: wouldn't it be neat if this existed somewhere?
    viewApp :: [Type tyname uni ann]
-> Type tyname uni ann
-> (Type tyname uni ann, [Type tyname uni ann])
viewApp [Type tyname uni ann]
args (TyApp ann
_ Type tyname uni ann
f Type tyname uni ann
x) = [Type tyname uni ann]
-> Type tyname uni ann
-> (Type tyname uni ann, [Type tyname uni ann])
viewApp (Type tyname uni ann
x Type tyname uni ann
-> [Type tyname uni ann] -> [Type tyname uni ann]
forall a. a -> [a] -> [a]
: [Type tyname uni ann]
args) Type tyname uni ann
f
    viewApp [Type tyname uni ann]
args Type tyname uni ann
ty            = (Type tyname uni ann
ty, [Type tyname uni ann]
args)

    -- Get the free variables that appear in arguments of a mixed arrow-forall type
    fvArgs :: Type a uni ann -> Set a
fvArgs (TyForall ann
_ a
x Kind ann
_ Type a uni ann
b) = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.delete a
x (Type a uni ann -> Set a
fvArgs Type a uni ann
b)
    fvArgs (TyFun ann
_ Type a uni ann
a Type a uni ann
b)      = Getting (Set a) (Type a uni ann) a -> Type a uni ann -> Set a
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set a) (Type a uni ann) a
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
Traversal' (Type tyname uni ann) tyname
Traversal' (Type a uni ann) a
ftvTy Type a uni ann
a Set a -> Set a -> Set a
forall a. Semigroup a => a -> a -> a
<> Type a uni ann -> Set a
fvArgs Type a uni ann
b
    fvArgs Type a uni ann
_                  = Set a
forall a. Monoid a => a
mempty

-- CODE REVIEW: does this exist anywhere?
typeArity :: Num a => Type tyname uni ann -> a
typeArity :: forall a tyname (uni :: * -> *) ann.
Num a =>
Type tyname uni ann -> a
typeArity (TyForall ann
_ tyname
_ Kind ann
_ Type tyname uni ann
a) = Type tyname uni ann -> a
forall a tyname (uni :: * -> *) ann.
Num a =>
Type tyname uni ann -> a
typeArity Type tyname uni ann
a
typeArity (TyFun ann
_ Type tyname uni ann
_ Type tyname uni ann
b)      = a
1 a -> a -> a
forall a. Num a => a -> a -> a
+ Type tyname uni ann -> a
forall a tyname (uni :: * -> *) ann.
Num a =>
Type tyname uni ann -> a
typeArity Type tyname uni ann
b
typeArity Type tyname uni ann
_                  = a
0

-- | Generate as small a term as possible to match a given type.
genAtomicTerm :: Type TyName DefaultUni () -> GenTm (Term TyName Name DefaultUni DefaultFun ())
genAtomicTerm :: Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
genAtomicTerm Type TyName DefaultUni ()
ty = do
  TypeCtx
ctx  <- (GenEnv -> TypeCtx) -> GenTm TypeCtx
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> TypeCtx
geTypes
  Map Name (Type TyName DefaultUni ())
vars <- (GenEnv -> Map Name (Type TyName DefaultUni ()))
-> GenTm (Map Name (Type TyName DefaultUni ()))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> Map Name (Type TyName DefaultUni ())
geTerms
  -- First try cheap unification
  let unifyVar :: (Name, Type TyName DefaultUni ())
-> Either String (Term TyName Name DefaultUni DefaultFun ())
unifyVar (Name
x, Type TyName DefaultUni ()
xty) = HasCallStack =>
TypeCtx
-> Int
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Either String [TyInst]
TypeCtx
-> Int
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Either String [TyInst]
findInstantiation TypeCtx
ctx Int
0 Type TyName DefaultUni ()
ty Type TyName DefaultUni ()
xty
                       Either String [TyInst]
-> ([TyInst] -> Term TyName Name DefaultUni DefaultFun ())
-> Either String (Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ [TyInst]
tys -> (Term TyName Name DefaultUni DefaultFun ()
 -> Type TyName DefaultUni ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> [Type TyName DefaultUni ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst ()) (() -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var () Name
x) [Type TyName DefaultUni ()
t | InstApp Type TyName DefaultUni ()
t <- [TyInst]
tys]
  case [Either String (Term TyName Name DefaultUni DefaultFun ())]
-> [Term TyName Name DefaultUni DefaultFun ()]
forall a b. [Either a b] -> [b]
rights ([Either String (Term TyName Name DefaultUni DefaultFun ())]
 -> [Term TyName Name DefaultUni DefaultFun ()])
-> [Either String (Term TyName Name DefaultUni DefaultFun ())]
-> [Term TyName Name DefaultUni DefaultFun ()]
forall a b. (a -> b) -> a -> b
$ ((Name, Type TyName DefaultUni ())
 -> Either String (Term TyName Name DefaultUni DefaultFun ()))
-> [(Name, Type TyName DefaultUni ())]
-> [Either String (Term TyName Name DefaultUni DefaultFun ())]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type TyName DefaultUni ())
-> Either String (Term TyName Name DefaultUni DefaultFun ())
unifyVar ([(Name, Type TyName DefaultUni ())]
 -> [Either String (Term TyName Name DefaultUni DefaultFun ())])
-> [(Name, Type TyName DefaultUni ())]
-> [Either String (Term TyName Name DefaultUni DefaultFun ())]
forall a b. (a -> b) -> a -> b
$ Map Name (Type TyName DefaultUni ())
-> [(Name, Type TyName DefaultUni ())]
forall k a. Map k a -> [(k, a)]
Map.toList Map Name (Type TyName DefaultUni ())
vars of
    -- If unification didn't work try the heavy-handed `inhabitType`.
    -- NOTE: We could probably just replace this whole function with
    -- `inhabitType` and the generators would run fine, but this method
    -- is probably faster a lot of the time and doesn't rely on the
    -- order that thins are chosen `inhabitType`. It is also going to generate
    -- a more even distribution than `inhabitType` (which for performance reasons
    -- always returns the first thing it finds).
    [] -> Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
inhabitType Type TyName DefaultUni ()
ty
    [Term TyName Name DefaultUni DefaultFun ()]
gs -> Gen (Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. Gen a -> GenT (ReaderT GenEnv Identity) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen (Gen (Term TyName Name DefaultUni DefaultFun ())
 -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> Gen (Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ [Term TyName Name DefaultUni DefaultFun ()]
-> Gen (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *) a. MonadGen m => [a] -> m a
elements [Term TyName Name DefaultUni DefaultFun ()]
gs

-- | Generate a term of a given type.
--
-- Requires the type to be of kind *.
genTermOfType :: Type TyName DefaultUni ()
              -> GenTm (Term TyName Name DefaultUni DefaultFun ())
genTermOfType :: Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
genTermOfType Type TyName DefaultUni ()
ty = (Type TyName DefaultUni (),
 Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a, b) -> b
snd ((Type TyName DefaultUni (),
  Term TyName Name DefaultUni DefaultFun ())
 -> Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genTerm (Type TyName DefaultUni () -> Maybe (Type TyName DefaultUni ())
forall a. a -> Maybe a
Just Type TyName DefaultUni ()
ty)

-- | Generate a term, if the first argument is Nothing then we get something of any type
-- and if the first argument is `Just ty` we get something of type `ty`.
--
-- Requires the type to be of kind *.
genTerm :: Maybe (Type TyName DefaultUni ())
        -> GenTm (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
genTerm :: Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genTerm Maybe (Type TyName DefaultUni ())
mty = GenT
  (ReaderT GenEnv Identity)
  (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall {m :: * -> *}.
MonadReader GenEnv m =>
m (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
-> m (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
checkInvariants (GenT
   (ReaderT GenEnv Identity)
   (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ do
  Int
customF <- (GenEnv -> Int) -> GenT (ReaderT GenEnv Identity) Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> Int
geCustomFreq
  Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
customG <- (GenEnv
 -> Maybe (Type TyName DefaultUni ())
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Maybe (Type TyName DefaultUni ())
      -> GenT
           (ReaderT GenEnv Identity)
           (Type TyName DefaultUni (),
            Term TyName Name DefaultUni DefaultFun ()))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv
-> Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
geCustomGen
  Map Name (Type TyName DefaultUni ())
vars <- (GenEnv -> Map Name (Type TyName DefaultUni ()))
-> GenTm (Map Name (Type TyName DefaultUni ()))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> Map Name (Type TyName DefaultUni ())
geTerms
  AllowEscape
esc <- (GenEnv -> AllowEscape)
-> GenT (ReaderT GenEnv Identity) AllowEscape
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> AllowEscape
geEscaping
  -- Prefer to generate things that bind variables until we have "enough" (20...)
  let (Int
letF, Int
lamF, Int
varAppF) = if Map Name (Type TyName DefaultUni ()) -> Int
forall k a. Map k a -> Int
Map.size Map Name (Type TyName DefaultUni ())
vars Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
20
                              then (Int
30, Int
50, Int
10)
                              else (Int
10, Int
30, Int
40)
      atomic :: GenT
  (ReaderT GenEnv Identity)
  (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
atomic
          | Just Type TyName DefaultUni ()
ty <- Maybe (Type TyName DefaultUni ())
mty = (Type TyName DefaultUni ()
ty,) (Term TyName Name DefaultUni DefaultFun ()
 -> (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
genAtomicTerm Type TyName DefaultUni ()
ty
          | Bool
otherwise      = do
              Type TyName DefaultUni ()
ty <- 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 ()
              (Type TyName DefaultUni ()
ty,) (Term TyName Name DefaultUni DefaultFun ()
 -> (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
genAtomicTerm Type TyName DefaultUni ()
ty
  GenT
  (ReaderT GenEnv Identity)
  (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. GenTm a -> GenTm a -> GenTm a
ifAstSizeZero GenT
  (ReaderT GenEnv Identity)
  (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
atomic (GenT
   (ReaderT GenEnv Identity)
   (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$
    [(Int,
  GenT
    (ReaderT GenEnv Identity)
    (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))]
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
frequency ([(Int,
   GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ()))]
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$
      [ (Int
10, GenT
  (ReaderT GenEnv Identity)
  (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
atomic) ]                                             [(Int,
  GenT
    (ReaderT GenEnv Identity)
    (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
forall a. [a] -> [a] -> [a]
++
      [ (Int
letF, Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genLet Maybe (Type TyName DefaultUni ())
mty) ]                                       [(Int,
  GenT
    (ReaderT GenEnv Identity)
    (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
forall a. [a] -> [a] -> [a]
++
      [ (Int
30, TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genForall TyName
x Kind ()
k Type TyName DefaultUni ()
a) | Just (TyForall ()
_ TyName
x Kind ()
k Type TyName DefaultUni ()
a) <- [Maybe (Type TyName DefaultUni ())
mty] ] [(Int,
  GenT
    (ReaderT GenEnv Identity)
    (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
forall a. [a] -> [a] -> [a]
++
      [ (Int
lamF, Maybe (Type TyName DefaultUni ())
-> Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genLam Maybe (Type TyName DefaultUni ())
a Maybe (Type TyName DefaultUni ())
b)    | Just (Maybe (Type TyName DefaultUni ())
a, Maybe (Type TyName DefaultUni ())
b) <- [Maybe (Type TyName DefaultUni ())
-> Maybe
     (Maybe (Type TyName DefaultUni ()),
      Maybe (Type TyName DefaultUni ()))
funTypeView Maybe (Type TyName DefaultUni ())
mty] ] [(Int,
  GenT
    (ReaderT GenEnv Identity)
    (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
forall a. [a] -> [a] -> [a]
++
      [ (Int
varAppF, HasCallStack =>
Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genVarApp Maybe (Type TyName DefaultUni ())
mty) ]                                 [(Int,
  GenT
    (ReaderT GenEnv Identity)
    (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
forall a. [a] -> [a] -> [a]
++
      [ (Int
10, Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genApp Maybe (Type TyName DefaultUni ())
mty) ]                                         [(Int,
  GenT
    (ReaderT GenEnv Identity)
    (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
forall a. [a] -> [a] -> [a]
++
      [ (Int
1, Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall {name} {fun}.
Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (), Term TyName name DefaultUni fun ())
genError Maybe (Type TyName DefaultUni ())
mty) ]                                        [(Int,
  GenT
    (ReaderT GenEnv Identity)
    (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
forall a. [a] -> [a] -> [a]
++
      [ (Int
10, Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall {tyname}.
Maybe (Type tyname DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type tyname DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genConst Maybe (Type TyName DefaultUni ())
mty)    | Maybe (Type TyName DefaultUni ()) -> Bool
forall {tyname} {uni :: * -> *} {ann}.
Maybe (Type tyname uni ann) -> Bool
canConst Maybe (Type TyName DefaultUni ())
mty ]                     [(Int,
  GenT
    (ReaderT GenEnv Identity)
    (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
forall a. [a] -> [a] -> [a]
++
      [ (Int
10, Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genDatLet Maybe (Type TyName DefaultUni ())
mty)   | AllowEscape
YesEscape <- [AllowEscape
esc] ]               [(Int,
  GenT
    (ReaderT GenEnv Identity)
    (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
forall a. [a] -> [a] -> [a]
++
      [ (Int
10, GenT
  (ReaderT GenEnv Identity)
  (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
forall {tyname} {name} {uni :: * -> *}.
GenT
  (ReaderT GenEnv Identity)
  (Type TyName DefaultUni (), Term tyname name uni DefaultFun ())
genIfTrace)      | Maybe (Type TyName DefaultUni ()) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (Type TyName DefaultUni ())
mty ]                    [(Int,
  GenT
    (ReaderT GenEnv Identity)
    (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
-> [(Int,
     GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))]
forall a. [a] -> [a] -> [a]
++
      [ (Int
customF, Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
customG Maybe (Type TyName DefaultUni ())
mty) ]
  where

    checkInvariants :: m (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
-> m (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
checkInvariants m (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
gen = do
      (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm) <- m (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
gen
      Bool
debug    <- (GenEnv -> Bool) -> m Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> Bool
geDebug
      TypeCtx
tyctx    <- (GenEnv -> TypeCtx) -> m TypeCtx
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> TypeCtx
geTypes
      Map Name (Type TyName DefaultUni ())
tmctx    <- (GenEnv -> Map Name (Type TyName DefaultUni ()))
-> m (Map Name (Type TyName DefaultUni ()))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> Map Name (Type TyName DefaultUni ())
geTerms
      if Bool
debug then
        case TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Either String ()
typeCheckTermInContext TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
tmctx Term TyName Name DefaultUni DefaultFun ()
tm Type TyName DefaultUni ()
ty of
          Left String
err ->
             (String
-> m (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. HasCallStack => String -> a
error (String
 -> m (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> (Doc Any -> String)
-> Doc Any
-> m (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Any -> String
forall a. Show a => a -> String
show (Doc Any
 -> m (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> Doc Any
-> m (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Doc Any
"genTerm - checkInvariants: term " Doc Any -> Doc Any -> Doc Any
forall a. Semigroup a => a -> a -> a
<> Term TyName Name DefaultUni DefaultFun () -> Doc Any
forall a ann. PrettyReadable a => a -> Doc ann
prettyReadable Term TyName Name DefaultUni DefaultFun ()
tm
                           Doc Any -> Doc Any -> Doc Any
forall a. Semigroup a => a -> a -> a
<> Doc Any
" does not type check at 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 -> Doc Any -> Doc Any
forall a. Semigroup a => a -> a -> a
<> Doc Any
" in type 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
tyctx
                           Doc Any -> Doc Any -> Doc Any
forall a. Semigroup a => a -> a -> a
<> Doc Any
" and term context " Doc Any -> Doc Any -> Doc Any
forall a. Semigroup a => a -> a -> a
<> Map Name (Type TyName DefaultUni ()) -> Doc Any
forall a ann. PrettyReadable a => a -> Doc ann
prettyReadable Map Name (Type TyName DefaultUni ())
tmctx
                           Doc Any -> Doc Any -> Doc Any
forall a. Semigroup a => a -> a -> a
<> 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)
          Either String ()
_ -> (Type TyName DefaultUni (),
 Term TyName Name DefaultUni DefaultFun ())
-> m (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm)
      else
        (Type TyName DefaultUni (),
 Term TyName Name DefaultUni DefaultFun ())
-> m (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm)

    funTypeView :: Maybe (Type TyName DefaultUni ())
-> Maybe
     (Maybe (Type TyName DefaultUni ()),
      Maybe (Type TyName DefaultUni ()))
funTypeView Maybe (Type TyName DefaultUni ())
Nothing                             = (Maybe (Type TyName DefaultUni ()),
 Maybe (Type TyName DefaultUni ()))
-> Maybe
     (Maybe (Type TyName DefaultUni ()),
      Maybe (Type TyName DefaultUni ()))
forall a. a -> Maybe a
Just (Maybe (Type TyName DefaultUni ())
forall a. Maybe a
Nothing, Maybe (Type TyName DefaultUni ())
forall a. Maybe a
Nothing)
    funTypeView (Just (Type TyName DefaultUni () -> Type TyName DefaultUni ()
normalizeTy -> TyFun ()
_ Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b)) = (Maybe (Type TyName DefaultUni ()),
 Maybe (Type TyName DefaultUni ()))
-> Maybe
     (Maybe (Type TyName DefaultUni ()),
      Maybe (Type TyName DefaultUni ()))
forall a. a -> Maybe a
Just (Type TyName DefaultUni () -> Maybe (Type TyName DefaultUni ())
forall a. a -> Maybe a
Just Type TyName DefaultUni ()
a, Type TyName DefaultUni () -> Maybe (Type TyName DefaultUni ())
forall a. a -> Maybe a
Just Type TyName DefaultUni ()
b)
    funTypeView Maybe (Type TyName DefaultUni ())
_                                   = Maybe
  (Maybe (Type TyName DefaultUni ()),
   Maybe (Type TyName DefaultUni ()))
forall a. Maybe a
Nothing

    -- Generate builtin ifthenelse and trace calls
    genIfTrace :: GenT
  (ReaderT GenEnv Identity)
  (Type TyName DefaultUni (), Term tyname name uni DefaultFun ())
genIfTrace = do
      DefaultFun
fun <- Gen DefaultFun -> GenT (ReaderT GenEnv Identity) DefaultFun
forall a. Gen a -> GenT (ReaderT GenEnv Identity) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen (Gen DefaultFun -> GenT (ReaderT GenEnv Identity) DefaultFun)
-> Gen DefaultFun -> GenT (ReaderT GenEnv Identity) DefaultFun
forall a b. (a -> b) -> a -> b
$ [DefaultFun] -> Gen DefaultFun
forall (m :: * -> *) a. MonadGen m => [a] -> m a
elements [DefaultFun
IfThenElse, DefaultFun
Trace]
      (Type TyName DefaultUni (), Term tyname name uni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (), Term tyname name uni DefaultFun ())
forall a. a -> GenT (ReaderT GenEnv Identity) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BuiltinSemanticsVariant DefaultFun
-> DefaultFun -> Type TyName DefaultUni ()
forall (uni :: * -> *) fun.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun -> fun -> Type TyName uni ()
typeOfBuiltinFunction BuiltinSemanticsVariant DefaultFun
forall a. Default a => a
def DefaultFun
fun, () -> DefaultFun -> Term tyname name uni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> fun -> Term tyname name uni fun a
Builtin () DefaultFun
fun)

    genError :: Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (), Term TyName name DefaultUni fun ())
genError Maybe (Type TyName DefaultUni ())
Nothing = do
      Type TyName DefaultUni ()
ty <- 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 ()
      (Type TyName DefaultUni (), Term TyName name DefaultUni fun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (), Term TyName name DefaultUni fun ())
forall a. a -> GenT (ReaderT GenEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type TyName DefaultUni ()
ty, ()
-> Type TyName DefaultUni () -> Term TyName name DefaultUni fun ()
forall tyname name (uni :: * -> *) fun a.
a -> Type tyname uni a -> Term tyname name uni fun a
Error () Type TyName DefaultUni ()
ty)
    genError (Just Type TyName DefaultUni ()
ty) = (Type TyName DefaultUni (), Term TyName name DefaultUni fun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (), Term TyName name DefaultUni fun ())
forall a. a -> GenT (ReaderT GenEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type TyName DefaultUni ()
ty, ()
-> Type TyName DefaultUni () -> Term TyName name DefaultUni fun ()
forall tyname name (uni :: * -> *) fun a.
a -> Type tyname uni a -> Term tyname name uni fun a
Error () Type TyName DefaultUni ()
ty)

    canConst :: Maybe (Type tyname uni ann) -> Bool
canConst Maybe (Type tyname uni ann)
Nothing            = Bool
True
    canConst (Just TyBuiltin{}) = Bool
True
    canConst (Just Type tyname uni ann
_)           = Bool
False

    genConst :: Maybe (Type tyname DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type tyname DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genConst Maybe (Type tyname DefaultUni ())
Nothing = do
      SomeTypeIn DefaultUni
someUni <- GenT (ReaderT GenEnv Identity) (Maybe (SomeTypeIn DefaultUni))
-> GenT (ReaderT GenEnv Identity) (SomeTypeIn DefaultUni)
forall (m :: * -> *) a. Monad m => GenT m (Maybe a) -> GenT m a
deliver (GenT (ReaderT GenEnv Identity) (Maybe (SomeTypeIn DefaultUni))
 -> GenT (ReaderT GenEnv Identity) (SomeTypeIn DefaultUni))
-> (Kind ()
    -> GenT (ReaderT GenEnv Identity) (Maybe (SomeTypeIn DefaultUni)))
-> Kind ()
-> GenT (ReaderT GenEnv Identity) (SomeTypeIn DefaultUni)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (Maybe (SomeTypeIn DefaultUni))
-> GenT (ReaderT GenEnv Identity) (Maybe (SomeTypeIn DefaultUni))
forall a. Gen a -> GenT (ReaderT GenEnv Identity) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen (Gen (Maybe (SomeTypeIn DefaultUni))
 -> GenT (ReaderT GenEnv Identity) (Maybe (SomeTypeIn DefaultUni)))
-> (Kind () -> Gen (Maybe (SomeTypeIn DefaultUni)))
-> Kind ()
-> GenT (ReaderT GenEnv Identity) (Maybe (SomeTypeIn DefaultUni))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind () -> Gen (Maybe (SomeTypeIn DefaultUni))
genBuiltinTypeOf (Kind () -> GenT (ReaderT GenEnv Identity) (SomeTypeIn DefaultUni))
-> Kind ()
-> GenT (ReaderT GenEnv Identity) (SomeTypeIn DefaultUni)
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
      (() -> SomeTypeIn DefaultUni -> Type tyname DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> SomeTypeIn uni -> Type tyname uni ann
TyBuiltin () SomeTypeIn DefaultUni
someUni, ) (Term TyName Name DefaultUni DefaultFun ()
 -> (Type tyname DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type tyname DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SomeTypeIn DefaultUni
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
genConstant SomeTypeIn DefaultUni
someUni
    genConst (Just ty :: Type tyname DefaultUni ()
ty@(TyBuiltin ()
_ SomeTypeIn DefaultUni
someUni)) = (Type tyname DefaultUni ()
ty,) (Term TyName Name DefaultUni DefaultFun ()
 -> (Type tyname DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type tyname DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SomeTypeIn DefaultUni
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
genConstant SomeTypeIn DefaultUni
someUni
    genConst Maybe (Type tyname DefaultUni ())
_ = String
-> GenT
     (ReaderT GenEnv Identity)
     (Type tyname DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. HasCallStack => String -> a
error String
"genConst: impossible"

    genDatLet :: Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genDatLet Maybe (Type TyName DefaultUni ())
mty = do
      Bool
rec <- Gen Bool -> GenT (ReaderT GenEnv Identity) Bool
forall a. Gen a -> GenT (ReaderT GenEnv Identity) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen Gen Bool
forall a. Arbitrary a => Gen a
arbitrary
      Bool
-> (Datatype TyName Name DefaultUni ()
    -> GenT
         (ReaderT GenEnv Identity)
         (Type TyName DefaultUni (),
          Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a.
Bool -> (Datatype TyName Name DefaultUni () -> GenTm a) -> GenTm a
genDatatypeLet Bool
rec ((Datatype TyName Name DefaultUni ()
  -> GenT
       (ReaderT GenEnv Identity)
       (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> (Datatype TyName Name DefaultUni ()
    -> GenT
         (ReaderT GenEnv Identity)
         (Type TyName DefaultUni (),
          Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ \ Datatype TyName Name DefaultUni ()
dat -> do
        (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm) <- Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genTerm Maybe (Type TyName DefaultUni ())
mty
        (Type TyName DefaultUni (),
 Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. a -> GenT (ReaderT GenEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Type TyName DefaultUni (),
  Term TyName Name DefaultUni DefaultFun ())
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ (Type TyName DefaultUni ()
ty, ()
-> Recursivity
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let () (if Bool
rec then Recursivity
Rec else Recursivity
NonRec) (()
-> Datatype TyName Name DefaultUni ()
-> Binding TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind () Datatype TyName Name DefaultUni ()
dat Binding TyName Name DefaultUni DefaultFun ()
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
forall a. a -> [a] -> NonEmpty a
:| []) Term TyName Name DefaultUni DefaultFun ()
tm)

    genLet :: Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genLet Maybe (Type TyName DefaultUni ())
mty = do
      -- How many terms to bind
      Int
n   <- Gen Int -> GenT (ReaderT GenEnv Identity) Int
forall a. Gen a -> GenT (ReaderT GenEnv Identity) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen (Gen Int -> GenT (ReaderT GenEnv Identity) Int)
-> Gen Int -> GenT (ReaderT GenEnv Identity) Int
forall a b. (a -> b) -> a -> b
$ (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
1, Int
3)
      -- Names of the bound terms
      [Name]
xs  <- [String] -> GenTm [Name]
genLikelyFreshNames ([String] -> GenTm [Name]) -> [String] -> GenTm [Name]
forall a b. (a -> b) -> a -> b
$ Int -> String -> [String]
forall a. Int -> a -> [a]
replicate Int
n String
"f"
      -- Types of the bound terms
      -- TODO: generate something that matches the target type
      [Type TyName DefaultUni ()]
as  <- (Int -> Int)
-> GenTm [Type TyName DefaultUni ()]
-> GenTm [Type TyName DefaultUni ()]
forall a. (Int -> Int) -> GenTm a -> GenTm a
onAstSize (Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
8) (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]
vectorOf Int
n (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 ()
forall ann. ann -> Kind ann
Type ())
      -- Strictness
      [Strictness]
ss  <- Int
-> GenT (ReaderT GenEnv Identity) Strictness
-> GenT (ReaderT GenEnv Identity) [Strictness]
forall (m :: * -> *) a. MonadGen m => Int -> m a -> m [a]
vectorOf Int
n (GenT (ReaderT GenEnv Identity) Strictness
 -> GenT (ReaderT GenEnv Identity) [Strictness])
-> GenT (ReaderT GenEnv Identity) Strictness
-> GenT (ReaderT GenEnv Identity) [Strictness]
forall a b. (a -> b) -> a -> b
$ Gen Strictness -> GenT (ReaderT GenEnv Identity) Strictness
forall a. Gen a -> GenT (ReaderT GenEnv Identity) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen (Gen Strictness -> GenT (ReaderT GenEnv Identity) Strictness)
-> Gen Strictness -> GenT (ReaderT GenEnv Identity) Strictness
forall a b. (a -> b) -> a -> b
$ [Strictness] -> Gen Strictness
forall (m :: * -> *) a. MonadGen m => [a] -> m a
elements [Strictness
Strict, Strictness
NonStrict]
      -- Recursive?
      Bool
r   <- Gen Bool -> GenT (ReaderT GenEnv Identity) Bool
forall a. Gen a -> GenT (ReaderT GenEnv Identity) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen (Gen Bool -> GenT (ReaderT GenEnv Identity) Bool)
-> Gen Bool -> GenT (ReaderT GenEnv Identity) Bool
forall a b. (a -> b) -> a -> b
$ [(Int, Gen Bool)] -> Gen Bool
forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
frequency [(Int
1, Bool -> Gen Bool
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True), (Int
6, Bool -> Gen Bool
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False)]
      -- Generate the binding
      -- TODO: maybe also generate mutually recursive bindings?
      let genBin :: (Name, Type TyName DefaultUni ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
genBin (Name
x, Type TyName DefaultUni ()
a) | Bool
r         = GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. GenTm a -> GenTm a
withNoEscape (GenTm (Term TyName Name DefaultUni DefaultFun ())
 -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni ()
    -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name
-> Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. Name -> Type TyName DefaultUni () -> GenTm a -> GenTm a
bindTmName Name
x Type TyName DefaultUni ()
a (GenTm (Term TyName Name DefaultUni DefaultFun ())
 -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni ()
    -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
genTermOfType (Type TyName DefaultUni ()
 -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Type TyName DefaultUni ()
a
                        | Bool
otherwise = GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. GenTm a -> GenTm a
withNoEscape (GenTm (Term TyName Name DefaultUni DefaultFun ())
 -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni ()
    -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
genTermOfType (Type TyName DefaultUni ()
 -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Type TyName DefaultUni ()
a
      -- Generate both bound terms and body with a size split of 1:7 (note, we are generating up to three bound
      -- terms, so the size split is really something like n:7).
      ([Term TyName Name DefaultUni DefaultFun ()]
tms, (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
body)) <-
          Int
-> Int
-> GenTm [Term TyName Name DefaultUni DefaultFun ()]
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenTm
     ([Term TyName Name DefaultUni DefaultFun ()],
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
forall a b. Int -> Int -> GenTm a -> GenTm b -> GenTm (a, b)
astSizeSplit_ Int
1 Int
7 (((Name, Type TyName DefaultUni ())
 -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> [(Name, Type TyName DefaultUni ())]
-> GenTm [Term TyName Name DefaultUni DefaultFun ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Name, Type TyName DefaultUni ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
genBin ([Name]
-> [Type TyName DefaultUni ()]
-> [(Name, Type TyName DefaultUni ())]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
xs [Type TyName DefaultUni ()]
as)) ([(Name, Type TyName DefaultUni ())]
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. [(Name, Type TyName DefaultUni ())] -> GenTm a -> GenTm a
bindTmNames ([Name]
-> [Type TyName DefaultUni ()]
-> [(Name, Type TyName DefaultUni ())]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
xs [Type TyName DefaultUni ()]
as) (GenT
   (ReaderT GenEnv Identity)
   (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genTerm Maybe (Type TyName DefaultUni ())
mty)
      let mkBind :: (name, Type tyname uni (), Strictness)
-> Term tyname name uni fun () -> Binding tyname name uni fun ()
mkBind (name
x, Type tyname uni ()
a, Strictness
s) Term tyname name uni fun ()
tm = ()
-> Strictness
-> VarDecl tyname name uni ()
-> Term tyname name uni fun ()
-> Binding tyname name uni fun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind () Strictness
s
                                  (() -> name -> Type tyname uni () -> VarDecl tyname name uni ()
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl () name
x Type tyname uni ()
a) Term tyname name uni fun ()
tm
          Binding TyName Name DefaultUni DefaultFun ()
b : [Binding TyName Name DefaultUni DefaultFun ()]
bs = ((Name, Type TyName DefaultUni (), Strictness)
 -> Term TyName Name DefaultUni DefaultFun ()
 -> Binding TyName Name DefaultUni DefaultFun ())
-> [(Name, Type TyName DefaultUni (), Strictness)]
-> [Term TyName Name DefaultUni DefaultFun ()]
-> [Binding TyName Name DefaultUni DefaultFun ()]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Name, Type TyName DefaultUni (), Strictness)
-> Term TyName Name DefaultUni DefaultFun ()
-> Binding TyName Name DefaultUni DefaultFun ()
forall {name} {tyname} {uni :: * -> *} {fun}.
(name, Type tyname uni (), Strictness)
-> Term tyname name uni fun () -> Binding tyname name uni fun ()
mkBind ([Name]
-> [Type TyName DefaultUni ()]
-> [Strictness]
-> [(Name, Type TyName DefaultUni (), Strictness)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Name]
xs [Type TyName DefaultUni ()]
as [Strictness]
ss) [Term TyName Name DefaultUni DefaultFun ()]
tms
      (Type TyName DefaultUni (),
 Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. a -> GenT (ReaderT GenEnv Identity) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName DefaultUni ()
ty, ()
-> Recursivity
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let () (if Bool
r then Recursivity
Rec else Recursivity
NonRec) (Binding TyName Name DefaultUni DefaultFun ()
b Binding TyName Name DefaultUni DefaultFun ()
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
forall a. a -> [a] -> NonEmpty a
:| [Binding TyName Name DefaultUni DefaultFun ()]
bs) Term TyName Name DefaultUni DefaultFun ()
body)

    genForall :: TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genForall TyName
x Kind ()
k Type TyName DefaultUni ()
a = do
      -- TODO: this freshenTyName here might be a bit paranoid
      TyName
y <- Set TyName -> TyName -> TyName
freshenTyNameWith (Getting (Set TyName) (Type TyName DefaultUni ()) TyName
-> Type TyName DefaultUni () -> Set TyName
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set TyName) (Type TyName DefaultUni ()) TyName
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
Traversal' (Type tyname uni ann) tyname
Traversal' (Type TyName DefaultUni ()) TyName
ftvTy Type TyName DefaultUni ()
a) (TyName -> TyName)
-> GenT (ReaderT GenEnv Identity) TyName
-> GenT (ReaderT GenEnv Identity) TyName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> GenT (ReaderT GenEnv Identity) TyName
genLikelyFreshTyName String
"a"
      let ty :: Type TyName DefaultUni ()
ty = ()
-> 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
y Kind ()
k (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ TyName
-> TyName -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
renameVar TyName
x TyName
y Type TyName DefaultUni ()
a
      (Type TyName DefaultUni ()
ty,) (Term TyName Name DefaultUni DefaultFun ()
 -> (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))
-> (Term TyName Name DefaultUni DefaultFun ()
    -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> TyName
-> Kind ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs () TyName
y Kind ()
k (Term TyName Name DefaultUni DefaultFun ()
 -> (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. GenTm a -> GenTm a
withNoEscape (GenTm (Term TyName Name DefaultUni DefaultFun ())
 -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni ()
    -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyName
-> Kind ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. TyName -> Kind () -> GenTm a -> GenTm a
bindTyName TyName
y Kind ()
k (GenTm (Term TyName Name DefaultUni DefaultFun ())
 -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni ()
    -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
genTermOfType (Type TyName DefaultUni ()
 -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ TyName
-> TyName -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
renameVar TyName
x TyName
y Type TyName DefaultUni ()
a)

    genLam :: Maybe (Type TyName DefaultUni ())
-> Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genLam Maybe (Type TyName DefaultUni ())
ma Maybe (Type TyName DefaultUni ())
mb = do
      Name
x <- String -> GenT (ReaderT GenEnv Identity) Name
genLikelyFreshName String
"x"
      (Type TyName DefaultUni ()
a, (Type TyName DefaultUni ()
b, Term TyName Name DefaultUni DefaultFun ()
body)) <-
        Int
-> Int
-> GenTm (Type TyName DefaultUni ())
-> (Type TyName DefaultUni ()
    -> GenT
         (ReaderT GenEnv Identity)
         (Type TyName DefaultUni (),
          Term TyName Name DefaultUni DefaultFun ()))
-> GenTm
     (Type TyName DefaultUni (),
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
forall a b. Int -> Int -> GenTm a -> (a -> GenTm b) -> GenTm (a, b)
astSizeSplit Int
1 Int
7
          (GenTm (Type TyName DefaultUni ())
-> (Type TyName DefaultUni () -> GenTm (Type TyName DefaultUni ()))
-> Maybe (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (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 ()) Type TyName DefaultUni () -> GenTm (Type TyName DefaultUni ())
forall a. a -> GenT (ReaderT GenEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Type TyName DefaultUni ())
ma)
          (\ Type TyName DefaultUni ()
a -> Name
-> Type TyName DefaultUni ()
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. Name -> Type TyName DefaultUni () -> GenTm a -> GenTm a
bindTmName Name
x Type TyName DefaultUni ()
a (GenT
   (ReaderT GenEnv Identity)
   (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> (GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ())
    -> GenT
         (ReaderT GenEnv Identity)
         (Type TyName DefaultUni (),
          Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenT
  (ReaderT GenEnv Identity)
  (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. GenTm a -> GenTm a
withNoEscape (GenT
   (ReaderT GenEnv Identity)
   (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genTerm Maybe (Type TyName DefaultUni ())
mb)
      (Type TyName DefaultUni (),
 Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. a -> GenT (ReaderT GenEnv Identity) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (()
-> 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 ()
a Type TyName DefaultUni ()
b, ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs () Name
x Type TyName DefaultUni ()
a Term TyName Name DefaultUni DefaultFun ()
body)

    genApp :: Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genApp Maybe (Type TyName DefaultUni ())
mty = GenT
  (ReaderT GenEnv Identity)
  (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. GenTm a -> GenTm a
withNoEscape (GenT
   (ReaderT GenEnv Identity)
   (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ do
        ((Type TyName DefaultUni ()
_, Term TyName Name DefaultUni DefaultFun ()
arg), (Type TyName DefaultUni ()
toResTy, Term TyName Name DefaultUni DefaultFun ()
fun)) <-
          Int
-> Int
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> ((Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())
    -> GenT
         (ReaderT GenEnv Identity)
         (Type TyName DefaultUni (),
          Term TyName Name DefaultUni DefaultFun ()))
-> GenTm
     ((Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()),
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
forall a b. Int -> Int -> GenTm a -> (a -> GenTm b) -> GenTm (a, b)
astSizeSplit Int
1 Int
4 (Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genTerm Maybe (Type TyName DefaultUni ())
forall a. Maybe a
Nothing) (\ (Type TyName DefaultUni ()
argTy, Term TyName Name DefaultUni DefaultFun ()
_) -> Type TyName DefaultUni ()
-> Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genFun Type TyName DefaultUni ()
argTy Maybe (Type TyName DefaultUni ())
mty)
        case Type TyName DefaultUni ()
toResTy of
          TyFun ()
_ Type TyName DefaultUni ()
_ Type TyName DefaultUni ()
resTy -> (Type TyName DefaultUni (),
 Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. a -> GenT (ReaderT GenEnv Identity) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName DefaultUni ()
resTy, ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply () Term TyName Name DefaultUni DefaultFun ()
fun Term TyName Name DefaultUni DefaultFun ()
arg)
          Type TyName DefaultUni ()
_               -> String
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. HasCallStack => String -> a
error (String
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> String
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Type TyName DefaultUni () -> String
forall str a. (Pretty a, Render str) => a -> str
display Type TyName DefaultUni ()
toResTy String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\n is not a 'TyFun'"
      where
        genFun :: Type TyName DefaultUni ()
-> Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genFun Type TyName DefaultUni ()
argTy Maybe (Type TyName DefaultUni ())
mty = Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genTerm (Maybe (Type TyName DefaultUni ())
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni () -> Maybe (Type TyName DefaultUni ()))
-> Type TyName DefaultUni ()
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type TyName DefaultUni () -> Maybe (Type TyName DefaultUni ())
forall a. a -> Maybe a
Just (Type TyName DefaultUni () -> Maybe (Type TyName DefaultUni ()))
-> (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Maybe (Type TyName DefaultUni ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> 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 ()
argTy (Type TyName DefaultUni ()
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> GenTm (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< GenTm (Type TyName DefaultUni ())
-> (Type TyName DefaultUni () -> GenTm (Type TyName DefaultUni ()))
-> Maybe (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni ())
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Kind () -> GenTm (Type TyName DefaultUni ())
genType (() -> Kind ()
forall ann. ann -> Kind ann
Type ())) Type TyName DefaultUni () -> GenTm (Type TyName DefaultUni ())
forall a. a -> GenT (ReaderT GenEnv Identity) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Type TyName DefaultUni ())
mty

    genVarApp :: HasCallStack => _
    genVarApp :: Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genVarApp Maybe (Type TyName DefaultUni ())
Nothing = GenT
  (ReaderT GenEnv Identity)
  (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. GenTm a -> GenTm a
withNoEscape (GenT
   (ReaderT GenEnv Identity)
   (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ do
      -- CODE REVIEW: this function exists somewhere maybe? (Maybe even in this module...)
      let arity :: Type tyname uni ann -> a
arity (TyForall ann
_ tyname
_ Kind ann
_ Type tyname uni ann
b) = a
1 a -> a -> a
forall a. Num a => a -> a -> a
+ Type tyname uni ann -> a
arity Type tyname uni ann
b
          arity (TyFun ann
_ Type tyname uni ann
_ Type tyname uni ann
b)      = a
1 a -> a -> a
forall a. Num a => a -> a -> a
+ Type tyname uni ann -> a
arity Type tyname uni ann
b
          arity Type tyname uni ann
_                  = a
0

          appl :: HasCallStack => Int -> Term TyName Name DefaultUni DefaultFun () -> _
          appl :: Int
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
appl Int
0 Term TyName Name DefaultUni DefaultFun ()
tm Type TyName DefaultUni ()
b = (Type TyName DefaultUni (),
 Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. a -> GenT (ReaderT GenEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type TyName DefaultUni ()
b, Term TyName Name DefaultUni DefaultFun ()
tm)
          appl Int
n Term TyName Name DefaultUni DefaultFun ()
tm (TyForall ()
_ TyName
x Kind ()
k Type TyName DefaultUni ()
b) = do
            Type TyName DefaultUni ()
ty <- Kind () -> GenTm (Type TyName DefaultUni ())
genType Kind ()
k
            TyName
x' <- String -> GenT (ReaderT GenEnv Identity) TyName
genLikelyFreshTyName String
"x"
            Int
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
appl (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst () Term TyName Name DefaultUni DefaultFun ()
tm Type TyName DefaultUni ()
ty) (HasCallStack =>
TypeSub -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
TypeSub -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
substType (TyName -> Type TyName DefaultUni () -> TypeSub
forall k a. k -> a -> Map k a
Map.singleton TyName
x' Type TyName DefaultUni ()
ty) (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ TyName
-> TyName -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
renameVar TyName
x TyName
x' Type TyName DefaultUni ()
b)
          appl Int
n Term TyName Name DefaultUni DefaultFun ()
tm (TyFun ()
_ Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b) = do
            (Type TyName DefaultUni ()
_, Term TyName Name DefaultUni DefaultFun ()
arg) <- Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genTerm (Type TyName DefaultUni () -> Maybe (Type TyName DefaultUni ())
forall a. a -> Maybe a
Just Type TyName DefaultUni ()
a)
            Int
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
appl (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply () Term TyName Name DefaultUni DefaultFun ()
tm Term TyName Name DefaultUni DefaultFun ()
arg) Type TyName DefaultUni ()
b
          appl Int
_ Term TyName Name DefaultUni DefaultFun ()
_ Type TyName DefaultUni ()
_ = String
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. HasCallStack => String -> a
error String
"appl"

          genV :: (Name, Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genV (Name
x, Type TyName DefaultUni ()
ty0) = do
            let ty :: Type TyName DefaultUni ()
ty = Type TyName DefaultUni () -> Type TyName DefaultUni ()
normalizeTy Type TyName DefaultUni ()
ty0
            Int
n <- Gen Int -> GenT (ReaderT GenEnv Identity) Int
forall a. Gen a -> GenT (ReaderT GenEnv Identity) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen (Gen Int -> GenT (ReaderT GenEnv Identity) Int)
-> Gen Int -> GenT (ReaderT GenEnv Identity) Int
forall a b. (a -> b) -> a -> b
$ (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, Type TyName DefaultUni () -> Int
forall a tyname (uni :: * -> *) ann.
Num a =>
Type tyname uni ann -> a
arity Type TyName DefaultUni ()
ty)
            (Int -> Int)
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. (Int -> Int) -> GenTm a -> GenTm a
onAstSize (Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
n) (GenT
   (ReaderT GenEnv Identity)
   (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
Int
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
Int
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
appl Int
n (() -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var () Name
x) Type TyName DefaultUni ()
ty
      (GenEnv -> [(Name, Type TyName DefaultUni ())])
-> GenT
     (ReaderT GenEnv Identity) [(Name, Type TyName DefaultUni ())]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Map Name (Type TyName DefaultUni ())
-> [(Name, Type TyName DefaultUni ())]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Name (Type TyName DefaultUni ())
 -> [(Name, Type TyName DefaultUni ())])
-> (GenEnv -> Map Name (Type TyName DefaultUni ()))
-> GenEnv
-> [(Name, Type TyName DefaultUni ())]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenEnv -> Map Name (Type TyName DefaultUni ())
geTerms) GenT (ReaderT GenEnv Identity) [(Name, Type TyName DefaultUni ())]
-> ([(Name, Type TyName DefaultUni ())]
    -> GenT
         (ReaderT GenEnv Identity)
         (Type TyName DefaultUni (),
          Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b.
GenT (ReaderT GenEnv Identity) a
-> (a -> GenT (ReaderT GenEnv Identity) b)
-> GenT (ReaderT GenEnv Identity) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
        []   -> do
          Type TyName DefaultUni ()
ty <- 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 ()
          (Type TyName DefaultUni ()
ty,) (Term TyName Name DefaultUni DefaultFun ()
 -> (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
inhabitType Type TyName DefaultUni ()
ty
        [(Name, Type TyName DefaultUni ())]
vars -> [GenT
   (ReaderT GenEnv Identity)
   (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())]
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *) a. MonadGen m => [m a] -> m a
oneof ([GenT
    (ReaderT GenEnv Identity)
    (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> [GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ())]
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ((Name, Type TyName DefaultUni ())
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> [(Name, Type TyName DefaultUni ())]
-> [GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ())]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genV [(Name, Type TyName DefaultUni ())]
vars

    genVarApp (Just Type TyName DefaultUni ()
ty) = do
      Map Name (Type TyName DefaultUni ())
vars <- (GenEnv -> Map Name (Type TyName DefaultUni ()))
-> GenTm (Map Name (Type TyName DefaultUni ()))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> Map Name (Type TyName DefaultUni ())
geTerms
      TypeCtx
ctx  <- (GenEnv -> TypeCtx) -> GenTm TypeCtx
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> TypeCtx
geTypes
      let cands :: [(Name, Type TyName DefaultUni ())]
cands = Map Name (Type TyName DefaultUni ())
-> [(Name, Type TyName DefaultUni ())]
forall k a. Map k a -> [(k, a)]
Map.toList Map Name (Type TyName DefaultUni ())
vars
          doInst :: Int
-> Term TyName Name DefaultUni DefaultFun ()
-> TyInst
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
doInst Int
_ Term TyName Name DefaultUni DefaultFun ()
tm (InstApp Type TyName DefaultUni ()
instTy) = Term TyName Name DefaultUni DefaultFun ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. a -> GenT (ReaderT GenEnv Identity) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name DefaultUni DefaultFun ()
 -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst () Term TyName Name DefaultUni DefaultFun ()
tm Type TyName DefaultUni ()
instTy
          doInst Int
n Term TyName Name DefaultUni DefaultFun ()
tm (InstArg Type TyName DefaultUni ()
argTy)  = (Int -> Int)
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. (Int -> Int) -> GenTm a -> GenTm a
onAstSize ((Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
n) (Int -> Int) -> (Int -> Int) -> Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract Int
1)
                                       (GenTm (Term TyName Name DefaultUni DefaultFun ())
 -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> (GenTm (Term TyName Name DefaultUni DefaultFun ())
    -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a. GenTm a -> GenTm a
withNoEscape
                                       (GenTm (Term TyName Name DefaultUni DefaultFun ())
 -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply () Term TyName Name DefaultUni DefaultFun ()
tm (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
genTermOfType Type TyName DefaultUni ()
argTy
      case [ (Term TyName Name DefaultUni DefaultFun ()
 -> TyInst -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> [TyInst]
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Int
-> Term TyName Name DefaultUni DefaultFun ()
-> TyInst
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
doInst Int
n) (() -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var () Name
x) [TyInst]
insts
           | (Name
x, Type TyName DefaultUni ()
a)      <- [(Name, Type TyName DefaultUni ())]
cands,
             Int
n           <- [Int
0..Type TyName DefaultUni () -> Int
forall a tyname (uni :: * -> *) ann.
Num a =>
Type tyname uni ann -> a
typeArity Type TyName DefaultUni ()
a],
             Right [TyInst]
insts <- [HasCallStack =>
TypeCtx
-> Int
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Either String [TyInst]
TypeCtx
-> Int
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Either String [TyInst]
findInstantiation TypeCtx
ctx Int
n Type TyName DefaultUni ()
ty Type TyName DefaultUni ()
a]
           ] of
        [] -> (Type TyName DefaultUni ()
ty,) (Term TyName Name DefaultUni DefaultFun ()
 -> (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName DefaultUni ()
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
inhabitType Type TyName DefaultUni ()
ty
        [GenTm (Term TyName Name DefaultUni DefaultFun ())]
gs -> (Type TyName DefaultUni ()
ty,) (Term TyName Name DefaultUni DefaultFun ()
 -> (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GenTm (Term TyName Name DefaultUni DefaultFun ())]
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall (m :: * -> *) a. MonadGen m => [m a] -> m a
oneof [GenTm (Term TyName Name DefaultUni DefaultFun ())]
gs

-- | Like 'listOf' except each of the elements is generated with a proportionally smaller size.
scaledListOf :: GenTm a -> GenTm [a]
scaledListOf :: forall a. GenTm a -> GenTm [a]
scaledListOf GenTm a
g = do
  Int
sz <- (GenEnv -> Int) -> GenT (ReaderT GenEnv Identity) Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> Int
geAstSize
  Int
n  <- (Int, Int) -> GenT (ReaderT GenEnv Identity) Int
forall a. Random a => (a, a) -> GenT (ReaderT GenEnv Identity) a
forall (g :: * -> *) a. (MonadGen g, Random a) => (a, a) -> g a
choose (Int
0, Int
sz Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
3)
  (Int -> Int) -> GenTm [a] -> GenTm [a]
forall a. (Int -> Int) -> GenTm a -> GenTm a
onAstSize (Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
n) (GenTm [a] -> GenTm [a]) -> GenTm [a] -> GenTm [a]
forall a b. (a -> b) -> a -> b
$ Int -> GenTm a -> GenTm [a]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n GenTm a
g

genDatatypeLet :: Bool -> (Datatype TyName Name DefaultUni () -> GenTm a) -> GenTm a
genDatatypeLet :: forall a.
Bool -> (Datatype TyName Name DefaultUni () -> GenTm a) -> GenTm a
genDatatypeLet Bool
rec Datatype TyName Name DefaultUni () -> GenTm a
cont = do
    Kind ()
k0 <- Gen (Kind ()) -> GenT (ReaderT GenEnv Identity) (Kind ())
forall a. Gen a -> GenT (ReaderT GenEnv Identity) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen Gen (Kind ())
forall a. Arbitrary a => Gen a
arbitrary
    let ks :: [Kind ()]
ks = Kind () -> [Kind ()]
forall ann. Kind ann -> [Kind ann]
argsFunKind Kind ()
k0
    Int
n <- Gen Int -> GenT (ReaderT GenEnv Identity) Int
forall a. Gen a -> GenT (ReaderT GenEnv Identity) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen (Gen Int -> GenT (ReaderT GenEnv Identity) Int)
-> Gen Int -> GenT (ReaderT GenEnv Identity) Int
forall a b. (a -> b) -> a -> b
$ (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
1, Int
3)
    -- Lazy matching to communicate to GHC the fact that this can't fail and thus doesn't require
    -- a 'MonadFail' (which 'GenTm' isn't).
    ~(TyName
d : [TyName]
xs) <- [String] -> GenTm [TyName]
genLikelyFreshTyNames ([String] -> GenTm [TyName]) -> [String] -> GenTm [TyName]
forall a b. (a -> b) -> a -> b
$ String
"d" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: Int -> String -> [String]
forall a. Int -> a -> [a]
replicate ([Kind ()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind ()]
ks) String
"a"
    ~(Name
m : [Name]
cs) <- [String] -> GenTm [Name]
genLikelyFreshNames   ([String] -> GenTm [Name]) -> [String] -> GenTm [Name]
forall a b. (a -> b) -> a -> b
$ String
"m" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: Int -> String -> [String]
forall a. Int -> a -> [a]
replicate Int
n String
"c"
    let dTy :: Type TyName DefaultUni ()
dTy = (Type TyName DefaultUni ()
 -> Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> [Type TyName DefaultUni ()]
-> Type TyName DefaultUni ()
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (()
-> 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 ()) (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
d) [() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
x | TyName
x <- [TyName]
xs]
        bty :: TyName
-> GenTm [[Type TyName DefaultUni ()]]
-> GenTm [[Type TyName DefaultUni ()]]
bty TyName
d = if Bool
rec
                then TyName
-> Kind ()
-> GenTm [[Type TyName DefaultUni ()]]
-> GenTm [[Type TyName DefaultUni ()]]
forall a. TyName -> Kind () -> GenTm a -> GenTm a
bindTyName TyName
d Kind ()
k0
                else TyName
-> GenTm [[Type TyName DefaultUni ()]]
-> GenTm [[Type TyName DefaultUni ()]]
forall a. TyName -> GenTm a -> GenTm a
registerTyName TyName
d
    [[Type TyName DefaultUni ()]]
conArgss <- TyName
-> GenTm [[Type TyName DefaultUni ()]]
-> GenTm [[Type TyName DefaultUni ()]]
bty TyName
d (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
bindTyNames ([TyName] -> [Kind ()] -> [(TyName, Kind ())]
forall a b. [a] -> [b] -> [(a, b)]
zip [TyName]
xs [Kind ()]
ks) (GenTm [[Type TyName DefaultUni ()]]
 -> GenTm [[Type TyName DefaultUni ()]])
-> GenTm [[Type TyName DefaultUni ()]]
-> GenTm [[Type TyName DefaultUni ()]]
forall a b. (a -> b) -> a -> b
$
                  -- Using 'listOf' instead if 'scaledListOf' makes the code slower by several
                  -- times (didn't check how exactly it affects the generated types).
                  (Int -> Int)
-> GenTm [[Type TyName DefaultUni ()]]
-> GenTm [[Type TyName DefaultUni ()]]
forall a. (Int -> Int) -> GenTm a -> GenTm a
onAstSize (Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
n) (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. Applicative m => Int -> m a -> m [a]
replicateM Int
n (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 ()]
forall a. GenTm a -> GenTm [a]
scaledListOf (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 ())
    let dat :: Datatype TyName Name DefaultUni ()
dat = ()
-> TyVarDecl TyName ()
-> [TyVarDecl TyName ()]
-> Name
-> [VarDecl TyName Name DefaultUni ()]
-> Datatype TyName Name DefaultUni ()
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
Datatype () (() -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
d Kind ()
k0) [() -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
x Kind ()
k | (TyName
x, Kind ()
k) <- [TyName] -> [Kind ()] -> [(TyName, Kind ())]
forall a b. [a] -> [b] -> [(a, b)]
zip [TyName]
xs [Kind ()]
ks] Name
m
                       [ ()
-> Name
-> Type TyName DefaultUni ()
-> VarDecl TyName Name DefaultUni ()
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl () Name
c ((Type TyName DefaultUni ()
 -> Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> [Type TyName DefaultUni ()]
-> Type TyName DefaultUni ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (()
-> 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 ()
dTy [Type TyName DefaultUni ()]
conArgs)
                       | (Name
c, [Type TyName DefaultUni ()]
conArgs) <- [Name]
-> [[Type TyName DefaultUni ()]]
-> [(Name, [Type TyName DefaultUni ()])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
cs [[Type TyName DefaultUni ()]]
conArgss ]
    Datatype TyName Name DefaultUni () -> GenTm a -> GenTm a
forall a. Datatype TyName Name DefaultUni () -> GenTm a -> GenTm a
bindDat Datatype TyName Name DefaultUni ()
dat (GenTm a -> GenTm a) -> GenTm a -> GenTm a
forall a b. (a -> b) -> a -> b
$ Datatype TyName Name DefaultUni () -> GenTm a
cont Datatype TyName Name DefaultUni ()
dat

-- | Generate up to 5 datatypes and bind them in a generator.
-- NOTE: despite its name this function does in fact not generate the `Let` binding
-- for the datatypes.
genDatatypeLets :: ([Datatype TyName Name DefaultUni ()] -> GenTm a) -> GenTm a
genDatatypeLets :: forall a.
([Datatype TyName Name DefaultUni ()] -> GenTm a) -> GenTm a
genDatatypeLets [Datatype TyName Name DefaultUni ()] -> GenTm a
cont = do
  Int
n0 <- Gen Int -> GenT (ReaderT GenEnv Identity) Int
forall a. Gen a -> GenT (ReaderT GenEnv Identity) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen (Gen Int -> GenT (ReaderT GenEnv Identity) Int)
-> Gen Int -> GenT (ReaderT GenEnv Identity) Int
forall a b. (a -> b) -> a -> b
$ (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
1, Int
5 :: Int)
  let go :: t -> ([Datatype TyName Name DefaultUni ()] -> GenTm a) -> GenTm a
go t
0 [Datatype TyName Name DefaultUni ()] -> GenTm a
k = [Datatype TyName Name DefaultUni ()] -> GenTm a
k []
      go t
n [Datatype TyName Name DefaultUni ()] -> GenTm a
k = Bool -> (Datatype TyName Name DefaultUni () -> GenTm a) -> GenTm a
forall a.
Bool -> (Datatype TyName Name DefaultUni () -> GenTm a) -> GenTm a
genDatatypeLet Bool
False ((Datatype TyName Name DefaultUni () -> GenTm a) -> GenTm a)
-> (Datatype TyName Name DefaultUni () -> GenTm a) -> GenTm a
forall a b. (a -> b) -> a -> b
$ \ Datatype TyName Name DefaultUni ()
dat -> t -> ([Datatype TyName Name DefaultUni ()] -> GenTm a) -> GenTm a
go (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1) ([Datatype TyName Name DefaultUni ()] -> GenTm a
k ([Datatype TyName Name DefaultUni ()] -> GenTm a)
-> ([Datatype TyName Name DefaultUni ()]
    -> [Datatype TyName Name DefaultUni ()])
-> [Datatype TyName Name DefaultUni ()]
-> GenTm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Datatype TyName Name DefaultUni ()
dat Datatype TyName Name DefaultUni ()
-> [Datatype TyName Name DefaultUni ()]
-> [Datatype TyName Name DefaultUni ()]
forall a. a -> [a] -> [a]
:))
  Int -> ([Datatype TyName Name DefaultUni ()] -> GenTm a) -> GenTm a
forall {t} {a}.
(Eq t, Num t) =>
t -> ([Datatype TyName Name DefaultUni ()] -> GenTm a) -> GenTm a
go Int
n0 [Datatype TyName Name DefaultUni ()] -> GenTm a
cont

genTypeAndTerm_ :: Gen (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
genTypeAndTerm_ :: Gen
  (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
genTypeAndTerm_ = GenT
  (ReaderT GenEnv Identity)
  (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
-> Gen
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. GenTm a -> Gen a
runGenTm (GenT
   (ReaderT GenEnv Identity)
   (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
 -> Gen
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> Gen
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ do
  (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
body) <- Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genTerm Maybe (Type TyName DefaultUni ())
forall a. Maybe a
Nothing
  (Type TyName DefaultUni (),
 Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. a -> GenT (ReaderT GenEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
body)

genTypeAndTermDebug_ :: Gen (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
genTypeAndTermDebug_ :: Gen
  (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
genTypeAndTermDebug_ = GenT
  (ReaderT GenEnv Identity)
  (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
-> Gen
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. GenTm a -> Gen a
runGenTm (GenT
   (ReaderT GenEnv Identity)
   (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
 -> Gen
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> (GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ())
    -> GenT
         (ReaderT GenEnv Identity)
         (Type TyName DefaultUni (),
          Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> Gen
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenT
  (ReaderT GenEnv Identity)
  (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. GenTm a -> GenTm a
withDebug (GenT
   (ReaderT GenEnv Identity)
   (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
 -> Gen
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> Gen
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ do
  (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
body) <- Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genTerm Maybe (Type TyName DefaultUni ())
forall a. Maybe a
Nothing
  (Type TyName DefaultUni (),
 Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. a -> GenT (ReaderT GenEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
body)

-- | Take a term of a specified type and generate
-- a fully applied term. Useful for generating terms that you want
-- to stick directly in an interpreter. Prefers to generate small arguments.
-- NOTE: The logic of this generating small arguments is that the inner term
-- should already have plenty of complicated arguments to functions to begin
-- with and now we just want to fill out the arguments so that we get
-- something that hopefully evaluates for a non-trivial number of steps.
genFullyApplied :: Type TyName DefaultUni ()
                -> Term TyName Name DefaultUni DefaultFun ()
                -> Gen (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
genFullyApplied :: Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Gen
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genFullyApplied Type TyName DefaultUni ()
typ0 Term TyName Name DefaultUni DefaultFun ()
trm0 = GenT
  (ReaderT GenEnv Identity)
  (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
-> Gen
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. GenTm a -> Gen a
runGenTm (GenT
   (ReaderT GenEnv Identity)
   (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
 -> Gen
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> Gen
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Term TyName Name DefaultUni DefaultFun ()
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
go Term TyName Name DefaultUni DefaultFun ()
trm0
  where
    go :: Term TyName Name DefaultUni DefaultFun ()
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
go Term TyName Name DefaultUni DefaultFun ()
trm = case Term TyName Name DefaultUni DefaultFun ()
trm of
      Let () Recursivity
rec NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds Term TyName Name DefaultUni DefaultFun ()
body -> (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (()
-> Recursivity
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let () Recursivity
rec NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds) ((Type TyName DefaultUni (),
  Term TyName Name DefaultUni DefaultFun ())
 -> (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a.
Foldable f =>
f (Binding TyName Name DefaultUni DefaultFun ())
-> GenTm a -> GenTm a
bindBinds NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds (Term TyName Name DefaultUni DefaultFun ()
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
go Term TyName Name DefaultUni DefaultFun ()
body)
      Term TyName Name DefaultUni DefaultFun ()
_                     -> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genArgsApps Type TyName DefaultUni ()
typ0 Term TyName Name DefaultUni DefaultFun ()
trm
    genArgsApps :: Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genArgsApps (TyForall ()
_ TyName
x Kind ()
k Type TyName DefaultUni ()
typ) Term TyName Name DefaultUni DefaultFun ()
trm = do
      let ty :: Type TyName DefaultUni ()
ty = Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
k
      Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genArgsApps (TyName
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) a.
Eq tyname =>
tyname
-> Type tyname uni a -> Type tyname uni a -> Type tyname uni a
typeSubstClosedType TyName
x Type TyName DefaultUni ()
ty Type TyName DefaultUni ()
typ) (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst () Term TyName Name DefaultUni DefaultFun ()
trm Type TyName DefaultUni ()
ty)
    genArgsApps (TyFun ()
_ Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b) Term TyName Name DefaultUni DefaultFun ()
trm = do
      (Type TyName DefaultUni ()
_, Term TyName Name DefaultUni DefaultFun ()
arg) <- GenT
  (ReaderT GenEnv Identity)
  (Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. GenTm a -> GenTm a
withNoEscape (GenT
   (ReaderT GenEnv Identity)
   (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
 -> GenT
      (ReaderT GenEnv Identity)
      (Type TyName DefaultUni (),
       Term TyName Name DefaultUni DefaultFun ()))
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genTerm (Type TyName DefaultUni () -> Maybe (Type TyName DefaultUni ())
forall a. a -> Maybe a
Just Type TyName DefaultUni ()
a)
      Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genArgsApps Type TyName DefaultUni ()
b (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply () Term TyName Name DefaultUni DefaultFun ()
trm Term TyName Name DefaultUni DefaultFun ()
arg)
    genArgsApps Type TyName DefaultUni ()
ty Term TyName Name DefaultUni DefaultFun ()
trm = (Type TyName DefaultUni (),
 Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
forall a. a -> GenT (ReaderT GenEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
trm)

-- | Generate a term of a specific type given a type and term context
genTermInContext_ :: TypeCtx
                  -> Map Name (Type TyName DefaultUni ())
                  -> Type TyName DefaultUni ()
                  -> Gen (Term TyName Name DefaultUni DefaultFun ())
genTermInContext_ :: TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Gen (Term TyName Name DefaultUni DefaultFun ())
genTermInContext_ TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Type TyName DefaultUni ()
ty =
  GenTm (Term TyName Name DefaultUni DefaultFun ())
-> Gen (Term TyName Name DefaultUni DefaultFun ())
forall a. GenTm a -> Gen a
runGenTm (GenTm (Term TyName Name DefaultUni DefaultFun ())
 -> Gen (Term TyName Name DefaultUni DefaultFun ()))
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> Gen (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ (GenEnv -> GenEnv)
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a.
(GenEnv -> GenEnv)
-> GenT (ReaderT GenEnv Identity) a
-> GenT (ReaderT GenEnv Identity) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ GenEnv
e -> GenEnv
e { geTypes = tyctx, geTerms = ctx, geEscaping = NoEscape }) (GenTm (Term TyName Name DefaultUni DefaultFun ())
 -> GenTm (Term TyName Name DefaultUni DefaultFun ()))
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$
    (Type TyName DefaultUni (),
 Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a, b) -> b
snd ((Type TyName DefaultUni (),
  Term TyName Name DefaultUni DefaultFun ())
 -> Term TyName Name DefaultUni DefaultFun ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
-> GenTm (Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Type TyName DefaultUni ())
-> GenT
     (ReaderT GenEnv Identity)
     (Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())
genTerm (Type TyName DefaultUni () -> Maybe (Type TyName DefaultUni ())
forall a. a -> Maybe a
Just Type TyName DefaultUni ()
ty)