{-# 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
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)
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
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
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"
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
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
([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
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)
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
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
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
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
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
| Bool
otherwise = do
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
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)
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
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
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
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
[] -> 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
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)
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
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
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
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)
[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"
[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]
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]
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)]
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
([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
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
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
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)
~(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
$
(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
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)
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)
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)