{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module PlutusCore.Generators.QuickCheck.GenTm
( module PlutusCore.Generators.QuickCheck.GenTm
, module Export
, Arbitrary (..)
, Gen
) where
import PlutusCore.Generators.QuickCheck.Common
import PlutusCore.Generators.QuickCheck.Utils
import PlutusCore.Default
import PlutusCore.Name.Unique
import PlutusIR
import PlutusIR.Compiler
import PlutusIR.Subst
import Control.Monad.Reader
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Maybe
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Set.Lens (setOf)
import Data.String
import Test.QuickCheck (Arbitrary (..), Gen)
import Test.QuickCheck qualified as QC
import Test.QuickCheck.GenT as Export hiding (var)
instance MonadReader r m => MonadReader r (GenT m) where
ask :: GenT m r
ask = m r -> GenT m r
forall (m :: * -> *) a. Monad m => m a -> GenT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m r
forall r (m :: * -> *). MonadReader r m => m r
ask
local :: forall a. (r -> r) -> GenT m a -> GenT m a
local r -> r
f (GenT QCGen -> Int -> m a
k) = (QCGen -> Int -> m a) -> GenT m a
forall (m :: * -> *) a. (QCGen -> Int -> m a) -> GenT m a
GenT ((QCGen -> Int -> m a) -> GenT m a)
-> (QCGen -> Int -> m a) -> GenT m a
forall a b. (a -> b) -> a -> b
$ \QCGen
qc Int
size -> (r -> r) -> m a -> m a
forall a. (r -> r) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local r -> r
f (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ QCGen -> Int -> m a
k QCGen
qc Int
size
type GenTm = GenT (Reader GenEnv)
data GenEnv = GenEnv
{ GenEnv -> Int
geAstSize :: Int
, GenEnv -> Map TyName (Datatype TyName Name DefaultUni ())
geDatas :: Map TyName (Datatype TyName Name DefaultUni ())
, GenEnv -> TypeCtx
geTypes :: TypeCtx
, GenEnv -> Map Name (Type TyName DefaultUni ())
geTerms :: Map Name (Type TyName DefaultUni ())
, GenEnv -> Set TyName
geUnboundUsedTyNames :: Set TyName
, GenEnv -> AllowEscape
geEscaping :: AllowEscape
, GenEnv
-> Maybe (Type TyName DefaultUni ())
-> GenTm
(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
geCustomGen :: Maybe (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
, GenEnv -> Int
geCustomFreq :: Int
, GenEnv -> Bool
geDebug :: Bool
}
withDebug :: GenTm a -> GenTm a
withDebug :: forall a. GenTm a -> GenTm a
withDebug GenTm a
gen = (GenEnv -> GenEnv) -> GenTm a -> GenTm a
forall a.
(GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\GenEnv
env -> GenEnv
env { geDebug = True }) GenTm a
gen
runGenTm :: GenTm a -> Gen a
runGenTm :: forall a. GenTm a -> Gen a
runGenTm = Int
-> (Maybe (Type TyName DefaultUni ())
-> GenTm
(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ()))
-> GenTm a
-> Gen a
forall a.
Int
-> (Maybe (Type TyName DefaultUni ())
-> GenTm
(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ()))
-> GenTm a
-> Gen a
runGenTmCustom Int
0 ([Char]
-> Maybe (Type TyName DefaultUni ())
-> GenTm
(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
forall a. HasCallStack => [Char] -> a
error [Char]
"No custom generator.")
runGenTmCustom :: Int
-> (Maybe (Type TyName DefaultUni ())
-> GenTm (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ()))
-> GenTm a
-> Gen a
runGenTmCustom :: forall a.
Int
-> (Maybe (Type TyName DefaultUni ())
-> GenTm
(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ()))
-> GenTm a
-> Gen a
runGenTmCustom Int
f Maybe (Type TyName DefaultUni ())
-> GenTm
(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
cg GenTm a
g = do
(Int -> Gen a) -> Gen a
forall a. (Int -> Gen a) -> Gen a
forall (g :: * -> *) a. MonadGen g => (Int -> g a) -> g a
sized ((Int -> Gen a) -> Gen a) -> (Int -> Gen a) -> Gen a
forall a b. (a -> b) -> a -> b
$ \ Int
n -> do
let env :: GenEnv
env = GenEnv
{
geAstSize :: Int
geAstSize = Int
n
, geDatas :: Map TyName (Datatype TyName Name DefaultUni ())
geDatas = Map TyName (Datatype TyName Name DefaultUni ())
forall k a. Map k a
Map.empty
, geTypes :: TypeCtx
geTypes = TypeCtx
forall k a. Map k a
Map.empty
, geTerms :: Map Name (Type TyName DefaultUni ())
geTerms = Map Name (Type TyName DefaultUni ())
forall k a. Map k a
Map.empty
, geUnboundUsedTyNames :: Set TyName
geUnboundUsedTyNames = Set TyName
forall a. Set a
Set.empty
, geEscaping :: AllowEscape
geEscaping = AllowEscape
YesEscape
, geCustomGen :: Maybe (Type TyName DefaultUni ())
-> GenTm
(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
geCustomGen = Maybe (Type TyName DefaultUni ())
-> GenTm
(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
cg
, geCustomFreq :: Int
geCustomFreq = Int
f
, geDebug :: Bool
geDebug = Bool
False
}
(Reader GenEnv a -> GenEnv -> a) -> GenEnv -> Reader GenEnv a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Reader GenEnv a -> GenEnv -> a
forall r a. Reader r a -> r -> a
runReader GenEnv
env (Reader GenEnv a -> a) -> Gen (Reader GenEnv a) -> Gen a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenTm a -> Gen (Reader GenEnv a)
forall (m :: * -> *) a. GenT m a -> Gen (m a)
runGenT GenTm a
g
suchThatMap :: Monad m => GenT m a -> (a -> Maybe b) -> GenT m b
GenT m a
gen suchThatMap :: forall (m :: * -> *) a b.
Monad m =>
GenT m a -> (a -> Maybe b) -> GenT m b
`suchThatMap` a -> Maybe b
f = (Maybe b -> b) -> GenT m (Maybe b) -> GenT m b
forall a b. (a -> b) -> GenT m a -> GenT m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe b -> b
forall a. HasCallStack => Maybe a -> a
fromJust (GenT m (Maybe b) -> GenT m b) -> GenT m (Maybe b) -> GenT m b
forall a b. (a -> b) -> a -> b
$ (a -> Maybe b) -> GenT m a -> GenT m (Maybe b)
forall a b. (a -> b) -> GenT m a -> GenT m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Maybe b
f GenT m a
gen GenT m (Maybe b) -> (Maybe b -> Bool) -> GenT m (Maybe b)
forall (m :: * -> *) a. MonadGen m => m a -> (a -> Bool) -> m a
`suchThat` Maybe b -> Bool
forall a. Maybe a -> Bool
isJust
deliver :: Monad m => GenT m (Maybe a) -> GenT m a
deliver :: forall (m :: * -> *) a. Monad m => GenT m (Maybe a) -> GenT m a
deliver GenT m (Maybe a)
gen = GenT m (Maybe a)
gen GenT m (Maybe a) -> (Maybe a -> Maybe a) -> GenT m a
forall (m :: * -> *) a b.
Monad m =>
GenT m a -> (a -> Maybe b) -> GenT m b
`suchThatMap` Maybe a -> Maybe a
forall a. a -> a
id
withNoEscape :: GenTm a -> GenTm a
withNoEscape :: forall a. GenTm a -> GenTm a
withNoEscape = (GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a
forall a.
(GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a)
-> (GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a
-> GenT (Reader GenEnv) a
forall a b. (a -> b) -> a -> b
$ \GenEnv
env -> GenEnv
env { geEscaping = NoEscape }
onAstSize :: (Int -> Int) -> GenTm a -> GenTm a
onAstSize :: forall a. (Int -> Int) -> GenTm a -> GenTm a
onAstSize Int -> Int
f = (GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a
forall a.
(GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a)
-> (GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a
-> GenT (Reader GenEnv) a
forall a b. (a -> b) -> a -> b
$ \ GenEnv
env -> GenEnv
env { geAstSize = f (geAstSize env) }
ifAstSizeZero :: GenTm a -> GenTm a -> GenTm a
ifAstSizeZero :: forall a. GenTm a -> GenTm a -> GenTm a
ifAstSizeZero GenTm a
ifZ GenTm a
nonZ = do
Int
n <- (GenEnv -> Int) -> GenT (Reader GenEnv) Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> Int
geAstSize
if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 then GenTm a
ifZ else GenTm a
nonZ
withAstSize :: Int -> GenTm a -> GenTm a
withAstSize :: forall a. Int -> GenTm a -> GenTm a
withAstSize = (Int -> Int) -> GenTm a -> GenTm a
forall a. (Int -> Int) -> GenTm a -> GenTm a
onAstSize ((Int -> Int) -> GenTm a -> GenTm a)
-> (Int -> Int -> Int) -> Int -> GenTm a -> GenTm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Int
forall a b. a -> b -> a
const
astSizeSplit_ :: Int -> Int -> GenTm a -> GenTm b -> GenTm (a, b)
astSizeSplit_ :: forall a b. Int -> Int -> GenTm a -> GenTm b -> GenTm (a, b)
astSizeSplit_ Int
a Int
b GenTm a
ga GenTm b
gb = Int -> Int -> GenTm a -> (a -> GenTm b) -> GenTm (a, b)
forall a b. Int -> Int -> GenTm a -> (a -> GenTm b) -> GenTm (a, b)
astSizeSplit Int
a Int
b GenTm a
ga (GenTm b -> a -> GenTm b
forall a b. a -> b -> a
const GenTm b
gb)
astSizeSplit :: Int -> Int -> GenTm a -> (a -> GenTm b) -> GenTm (a, b)
astSizeSplit :: forall a b. Int -> Int -> GenTm a -> (a -> GenTm b) -> GenTm (a, b)
astSizeSplit Int
a Int
b GenTm a
ga a -> GenTm b
gb = do
Int
n <- (GenEnv -> Int) -> GenT (Reader GenEnv) Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks GenEnv -> Int
geAstSize
let na :: Int
na = (Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` (Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
b)
nb :: Int
nb = (Int
b Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` (Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
b)
a
x <- Int -> GenTm a -> GenTm a
forall a. Int -> GenTm a -> GenTm a
withAstSize Int
na GenTm a
ga
(,) a
x (b -> (a, b)) -> GenTm b -> GenTm (a, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> GenTm b -> GenTm b
forall a. Int -> GenTm a -> GenTm a
withAstSize Int
nb (a -> GenTm b
gb a
x)
getUniques :: GenTm (Set Unique)
getUniques :: GenTm (Set Unique)
getUniques = do
GenEnv{geDatas :: GenEnv -> Map TyName (Datatype TyName Name DefaultUni ())
geDatas = Map TyName (Datatype TyName Name DefaultUni ())
dts, geTypes :: GenEnv -> TypeCtx
geTypes = TypeCtx
tys, geTerms :: GenEnv -> Map Name (Type TyName DefaultUni ())
geTerms = Map Name (Type TyName DefaultUni ())
tms, geUnboundUsedTyNames :: GenEnv -> Set TyName
geUnboundUsedTyNames = Set TyName
used} <- GenT (Reader GenEnv) GenEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
Set Unique -> GenTm (Set Unique)
forall a. a -> GenT (Reader GenEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Unique -> GenTm (Set Unique))
-> Set Unique -> GenTm (Set Unique)
forall a b. (a -> b) -> a -> b
$ (TyName -> Unique) -> Set TyName -> Set Unique
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (Name -> Unique
_nameUnique (Name -> Unique) -> (TyName -> Name) -> TyName -> Unique
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyName -> Name
unTyName) (Map TyName (Datatype TyName Name DefaultUni ()) -> Set TyName
forall k a. Map k a -> Set k
Map.keysSet Map TyName (Datatype TyName Name DefaultUni ())
dts 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
tys Set TyName -> Set TyName -> Set TyName
forall a. Semigroup a => a -> a -> a
<> Set TyName
used) Set Unique -> Set Unique -> Set Unique
forall a. Semigroup a => a -> a -> a
<>
(Name -> Unique) -> Set Name -> Set Unique
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic Name -> Unique
_nameUnique (Map Name (Type TyName DefaultUni ()) -> Set Name
forall k a. Map k a -> Set k
Map.keysSet Map Name (Type TyName DefaultUni ())
tms) Set Unique -> Set Unique -> Set Unique
forall a. Semigroup a => a -> a -> a
<>
[Set Unique] -> Set Unique
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [ Datatype TyName Name DefaultUni () -> Set Unique
forall {tyname} {uni :: * -> *} {a}.
Datatype tyname Name uni a -> Set Unique
names Datatype TyName Name DefaultUni ()
d | Datatype TyName Name DefaultUni ()
d <- Map TyName (Datatype TyName Name DefaultUni ())
-> [Datatype TyName Name DefaultUni ()]
forall k a. Map k a -> [a]
Map.elems Map TyName (Datatype TyName Name DefaultUni ())
dts ]
where
names :: Datatype tyname Name uni a -> Set Unique
names (Datatype a
_ TyVarDecl tyname a
_ [TyVarDecl tyname a]
_ Name
m [VarDecl tyname Name uni a]
cs) = [Unique] -> Set Unique
forall a. Ord a => [a] -> Set a
Set.fromList ([Unique] -> Set Unique) -> [Unique] -> Set Unique
forall a b. (a -> b) -> a -> b
$ Name -> Unique
_nameUnique Name
m Unique -> [Unique] -> [Unique]
forall a. a -> [a] -> [a]
: [ Name -> Unique
_nameUnique Name
c | VarDecl a
_ Name
c Type tyname uni a
_ <- [VarDecl tyname Name uni a]
cs ]
genLikelyFreshName :: String -> GenTm Name
genLikelyFreshName :: [Char] -> GenTm Name
genLikelyFreshName [Char]
s = [Name] -> Name
forall a. HasCallStack => [a] -> a
head ([Name] -> Name) -> GenT (Reader GenEnv) [Name] -> GenTm Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Char]] -> GenT (Reader GenEnv) [Name]
genLikelyFreshNames [[Char]
s]
genLikelyFreshNames :: [String] -> GenTm [Name]
genLikelyFreshNames :: [[Char]] -> GenT (Reader GenEnv) [Name]
genLikelyFreshNames [[Char]]
ss = do
Set Unique
used <- GenTm (Set Unique)
getUniques
let i :: Int
i = Unique -> Int
forall a. Enum a => a -> Int
fromEnum (Unique -> Int) -> Unique -> Int
forall a b. (a -> b) -> a -> b
$ Set Unique -> Unique
forall a. Set a -> a
Set.findMax (Set Unique -> Unique) -> Set Unique -> Unique
forall a b. (a -> b) -> a -> b
$ Unique -> Set Unique -> Set Unique
forall a. Ord a => a -> Set a -> Set a
Set.insert (Int -> Unique
Unique Int
0) Set Unique
used
js :: [Int]
js = [ Int
j | Int
j <- [Int
1..Int
i], Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> Unique
Unique Int
j Unique -> Set Unique -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Unique
used ]
is :: [Int]
is = [Int]
js [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take ([[Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Char]]
ss Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
10) [Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1..]
[Int]
is' <- Gen [Int] -> GenT (Reader GenEnv) [Int]
forall a. Gen a -> GenT (Reader GenEnv) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen (Gen [Int] -> GenT (Reader GenEnv) [Int])
-> Gen [Int] -> GenT (Reader GenEnv) [Int]
forall a b. (a -> b) -> a -> b
$ [Int] -> Gen [Int]
forall a. [a] -> Gen [a]
QC.shuffle [Int]
is
[Name] -> GenT (Reader GenEnv) [Name]
forall a. a -> GenT (Reader GenEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Text -> Unique -> Name
Name ([Char] -> Text
forall a. IsString a => [Char] -> a
fromString ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
j) (Int -> Unique
forall a. Enum a => Int -> a
toEnum Int
j) | ([Char]
s, Int
j) <- [[Char]] -> [Int] -> [([Char], Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [[Char]]
ss [Int]
is']
genLikelyFreshTyName :: String -> GenTm TyName
genLikelyFreshTyName :: [Char] -> GenTm TyName
genLikelyFreshTyName [Char]
s = Name -> TyName
TyName (Name -> TyName) -> GenTm Name -> GenTm TyName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> GenTm Name
genLikelyFreshName [Char]
s
genLikelyFreshTyNames :: [String] -> GenTm [TyName]
genLikelyFreshTyNames :: [[Char]] -> GenTm [TyName]
genLikelyFreshTyNames [[Char]]
ss = (Name -> TyName) -> [Name] -> [TyName]
forall a b. (a -> b) -> [a] -> [b]
map Name -> TyName
TyName ([Name] -> [TyName])
-> GenT (Reader GenEnv) [Name] -> GenTm [TyName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Char]] -> GenT (Reader GenEnv) [Name]
genLikelyFreshNames [[Char]]
ss
genLikelyNotFreshName :: String -> GenTm Name
genLikelyNotFreshName :: [Char] -> GenTm Name
genLikelyNotFreshName [Char]
s = do
[Unique]
used <- Set Unique -> [Unique]
forall a. Set a -> [a]
Set.toList (Set Unique -> [Unique])
-> GenTm (Set Unique) -> GenT (Reader GenEnv) [Unique]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenTm (Set Unique)
getUniques
case [Unique]
used of
[] -> [Char] -> GenTm Name
genLikelyFreshName [Char]
s
[Unique]
_ -> Gen Name -> GenTm Name
forall a. Gen a -> GenT (Reader GenEnv) a
forall (g :: * -> *) a. MonadGen g => Gen a -> g a
liftGen (Gen Name -> GenTm Name) -> Gen Name -> GenTm Name
forall a b. (a -> b) -> a -> b
$ [Name] -> Gen Name
forall (m :: * -> *) a. MonadGen m => [a] -> m a
elements [ Text -> Unique -> Name
Name ([Char] -> Text
forall a. IsString a => [Char] -> a
fromString ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Unique -> Int
unUnique Unique
i)) Unique
i | Unique
i <- [Unique]
used ]
genMaybeFreshName :: String -> GenTm Name
genMaybeFreshName :: [Char] -> GenTm Name
genMaybeFreshName [Char]
s = [(Int, GenTm Name)] -> GenTm Name
forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
frequency [(Int
3, [Char] -> GenTm Name
genLikelyFreshName [Char]
s), (Int
1, [Char] -> GenTm Name
genLikelyNotFreshName [Char]
s)]
genMaybeFreshTyName :: String -> GenTm TyName
genMaybeFreshTyName :: [Char] -> GenTm TyName
genMaybeFreshTyName [Char]
s = Name -> TyName
TyName (Name -> TyName) -> GenTm Name -> GenTm TyName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> GenTm Name
genMaybeFreshName [Char]
s
bindTyName :: TyName -> Kind () -> GenTm a -> GenTm a
bindTyName :: forall a. TyName -> Kind () -> GenTm a -> GenTm a
bindTyName TyName
x Kind ()
k = (GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a
forall a.
(GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a)
-> (GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a
-> GenT (Reader GenEnv) a
forall a b. (a -> b) -> a -> b
$ \ GenEnv
e -> GenEnv
e
{ geTypes = Map.insert x k (geTypes e)
, geTerms = Map.filter (\Type TyName DefaultUni ()
ty -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ TyName
x TyName -> Set TyName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` 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) (geTerms e)
, geDatas = Map.delete x (geDatas e)
}
bindTyNames :: [(TyName, Kind ())] -> GenTm a -> GenTm a
bindTyNames :: forall a. [(TyName, Kind ())] -> GenTm a -> GenTm a
bindTyNames = (GenTm a -> [(TyName, Kind ())] -> GenTm a)
-> [(TyName, Kind ())] -> GenTm a -> GenTm a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((GenTm a -> [(TyName, Kind ())] -> GenTm a)
-> [(TyName, Kind ())] -> GenTm a -> GenTm a)
-> (GenTm a -> [(TyName, Kind ())] -> GenTm a)
-> [(TyName, Kind ())]
-> GenTm a
-> GenTm a
forall a b. (a -> b) -> a -> b
$ ((TyName, Kind ()) -> GenTm a -> GenTm a)
-> GenTm a -> [(TyName, Kind ())] -> GenTm a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((TyName -> Kind () -> GenTm a -> GenTm a)
-> (TyName, Kind ()) -> GenTm a -> GenTm a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TyName -> Kind () -> GenTm a -> GenTm a
forall a. TyName -> Kind () -> GenTm a -> GenTm a
bindTyName)
registerTyName :: TyName -> GenTm a -> GenTm a
registerTyName :: forall a. TyName -> GenTm a -> GenTm a
registerTyName TyName
n = (GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a
forall a.
(GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a)
-> (GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a
-> GenT (Reader GenEnv) a
forall a b. (a -> b) -> a -> b
$ \ GenEnv
e -> GenEnv
e { geUnboundUsedTyNames = Set.insert n (geUnboundUsedTyNames e) }
bindTmName :: Name -> Type TyName DefaultUni () -> GenTm a -> GenTm a
bindTmName :: forall a. Name -> Type TyName DefaultUni () -> GenTm a -> GenTm a
bindTmName Name
x Type TyName DefaultUni ()
ty = (GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a
forall a.
(GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a)
-> (GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a
-> GenT (Reader GenEnv) a
forall a b. (a -> b) -> a -> b
$ \ GenEnv
e -> GenEnv
e { geTerms = Map.insert x ty (geTerms e) }
bindTmNames :: [(Name, Type TyName DefaultUni ())] -> GenTm a -> GenTm a
bindTmNames :: forall a. [(Name, Type TyName DefaultUni ())] -> GenTm a -> GenTm a
bindTmNames = (GenTm a -> [(Name, Type TyName DefaultUni ())] -> GenTm a)
-> [(Name, Type TyName DefaultUni ())] -> GenTm a -> GenTm a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((GenTm a -> [(Name, Type TyName DefaultUni ())] -> GenTm a)
-> [(Name, Type TyName DefaultUni ())] -> GenTm a -> GenTm a)
-> (GenTm a -> [(Name, Type TyName DefaultUni ())] -> GenTm a)
-> [(Name, Type TyName DefaultUni ())]
-> GenTm a
-> GenTm a
forall a b. (a -> b) -> a -> b
$ ((Name, Type TyName DefaultUni ()) -> GenTm a -> GenTm a)
-> GenTm a -> [(Name, Type TyName DefaultUni ())] -> GenTm a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Name -> Type TyName DefaultUni () -> GenTm a -> GenTm a)
-> (Name, Type TyName DefaultUni ()) -> GenTm a -> GenTm a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Type TyName DefaultUni () -> GenTm a -> GenTm a
forall a. Name -> Type TyName DefaultUni () -> GenTm a -> GenTm a
bindTmName)
bindLikelyFreshTmName :: String -> Type TyName DefaultUni () -> (Name -> GenTm a) -> GenTm a
bindLikelyFreshTmName :: forall a.
[Char] -> Type TyName DefaultUni () -> (Name -> GenTm a) -> GenTm a
bindLikelyFreshTmName [Char]
name Type TyName DefaultUni ()
ty Name -> GenTm a
k = do
Name
x <- [Char] -> GenTm Name
genLikelyFreshName [Char]
name
Name -> Type TyName DefaultUni () -> GenTm a -> GenTm a
forall a. Name -> Type TyName DefaultUni () -> GenTm a -> GenTm a
bindTmName Name
x Type TyName DefaultUni ()
ty (Name -> GenTm a
k Name
x)
bindDat :: Datatype TyName Name DefaultUni ()
-> GenTm a
-> GenTm a
bindDat :: forall a. Datatype TyName Name DefaultUni () -> GenTm a -> GenTm a
bindDat dat :: Datatype TyName Name DefaultUni ()
dat@(Datatype ()
_ (TyVarDecl ()
_ TyName
a Kind ()
k) [TyVarDecl TyName ()]
_ Name
_ [VarDecl TyName Name DefaultUni ()]
_) GenTm a
cont =
TyName -> Kind () -> GenTm a -> GenTm a
forall a. TyName -> Kind () -> GenTm a -> GenTm a
bindTyName TyName
a Kind ()
k (GenTm a -> GenTm a) -> GenTm a -> GenTm a
forall a b. (a -> b) -> a -> b
$
(GenEnv -> GenEnv) -> GenTm a -> GenTm a
forall a.
(GenEnv -> GenEnv)
-> GenT (Reader GenEnv) a -> GenT (Reader GenEnv) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\ GenEnv
e -> GenEnv
e { geDatas = Map.insert a dat (geDatas e) }) (GenTm a -> GenTm a) -> GenTm a -> GenTm a
forall a b. (a -> b) -> a -> b
$
((Name, Type TyName DefaultUni ()) -> GenTm a -> GenTm a)
-> GenTm a -> [(Name, Type TyName DefaultUni ())] -> GenTm a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Name -> Type TyName DefaultUni () -> GenTm a -> GenTm a)
-> (Name, Type TyName DefaultUni ()) -> GenTm a -> GenTm a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Type TyName DefaultUni () -> GenTm a -> GenTm a
forall a. Name -> Type TyName DefaultUni () -> GenTm a -> GenTm a
bindTmName) GenTm a
cont (Datatype TyName Name DefaultUni ()
-> (Name, Type TyName DefaultUni ())
matchType Datatype TyName Name DefaultUni ()
dat (Name, Type TyName DefaultUni ())
-> [(Name, Type TyName DefaultUni ())]
-> [(Name, Type TyName DefaultUni ())]
forall a. a -> [a] -> [a]
: Datatype TyName Name DefaultUni ()
-> [(Name, Type TyName DefaultUni ())]
constrTypes Datatype TyName Name DefaultUni ()
dat)
bindBind :: Binding TyName Name DefaultUni DefaultFun ()
-> GenTm a
-> GenTm a
bindBind :: forall a.
Binding TyName Name DefaultUni DefaultFun () -> GenTm a -> GenTm a
bindBind (DatatypeBind ()
_ Datatype TyName Name DefaultUni ()
dat) = Datatype TyName Name DefaultUni () -> GenTm a -> GenTm a
forall a. Datatype TyName Name DefaultUni () -> GenTm a -> GenTm a
bindDat Datatype TyName Name DefaultUni ()
dat
bindBind (TermBind ()
_ Strictness
_ (VarDecl ()
_ Name
x Type TyName DefaultUni ()
ty) Term TyName Name DefaultUni DefaultFun ()
_) = Name -> Type TyName DefaultUni () -> GenTm a -> GenTm a
forall a. Name -> Type TyName DefaultUni () -> GenTm a -> GenTm a
bindTmName Name
x Type TyName DefaultUni ()
ty
bindBind Binding TyName Name DefaultUni DefaultFun ()
_ = [Char] -> GenTm a -> GenTm a
forall a. HasCallStack => [Char] -> a
error [Char]
"unreachable"
bindBinds :: Foldable f => f (Binding TyName Name DefaultUni DefaultFun ()) -> GenTm a -> GenTm a
bindBinds :: forall (f :: * -> *) a.
Foldable f =>
f (Binding TyName Name DefaultUni DefaultFun ())
-> GenTm a -> GenTm a
bindBinds = (GenTm a
-> f (Binding TyName Name DefaultUni DefaultFun ()) -> GenTm a)
-> f (Binding TyName Name DefaultUni DefaultFun ())
-> GenTm a
-> GenTm a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Binding TyName Name DefaultUni DefaultFun ()
-> GenTm a -> GenTm a)
-> GenTm a
-> f (Binding TyName Name DefaultUni DefaultFun ())
-> GenTm a
forall a b. (a -> b -> b) -> b -> f a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun () -> GenTm a -> GenTm a
forall a.
Binding TyName Name DefaultUni DefaultFun () -> GenTm a -> GenTm a
bindBind)