{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module PlutusCore.Generators.Hedgehog.Entity
( PlcGenT
, IterApp(..)
, IterAppValue(..)
, runPlcT
, withTypedBuiltinGen
, genIterAppValue
, genTerm
, genTermLoose
, withAnyTermLoose
) where
import PlutusPrelude
import PlutusCore.Generators.Hedgehog.Denotation
import PlutusCore.Generators.Hedgehog.TypedBuiltinGen
import PlutusCore.Generators.Hedgehog.Utils
import PlutusCore.Builtin
import PlutusCore.Core
import PlutusCore.Default
import PlutusCore.Name.Unique
import PlutusCore.Pretty (PrettyConst, botRenderContext, prettyConst)
import PlutusCore.Quote
import Control.Monad.Morph qualified as Morph
import Control.Monad.Reader
import Data.ByteString qualified as BS
import Data.Kind as GHC
import Data.Proxy
import Hedgehog hiding (Size, Var)
import Hedgehog.Gen qualified as Gen
import Prettyprinter
import Type.Reflection
type Plain f (uni :: GHC.Type -> GHC.Type) (fun :: GHC.Type) = f TyName Name uni fun ()
newtype BuiltinGensT uni fun m = BuiltinGensT
{ forall (uni :: * -> *) fun (m :: * -> *).
BuiltinGensT uni fun m -> TypedBuiltinGenT (Plain Term uni fun) m
_builtinGensTyped :: TypedBuiltinGenT (Plain Term uni fun) m
}
type PlcGenT uni fun m = GenT (ReaderT (BuiltinGensT uni fun m) m)
data IterApp head arg = IterApp
{ forall head arg. IterApp head arg -> head
_iterAppHead :: head
, forall head arg. IterApp head arg -> [arg]
_iterAppSpine :: [arg]
}
instance (PrettyBy config head, PrettyBy config arg) => PrettyBy config (IterApp head arg) where
prettyBy :: forall ann. config -> IterApp head arg -> Doc ann
prettyBy config
config (IterApp head
appHead [arg]
appSpine) =
Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ (Doc ann -> arg -> Doc ann) -> Doc ann -> [arg] -> Doc ann
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Doc ann
fun arg
arg -> Doc ann
fun Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> config -> arg -> Doc ann
forall ann. config -> arg -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config arg
arg) (config -> head -> Doc ann
forall ann. config -> head -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config head
appHead) [arg]
appSpine
data IterAppValue uni fun head arg r = IterAppValue
{ forall (uni :: * -> *) fun head arg r.
IterAppValue uni fun head arg r -> Plain Term uni fun
_iterTerm :: Plain Term uni fun
, forall (uni :: * -> *) fun head arg r.
IterAppValue uni fun head arg r -> IterApp head arg
_iterApp :: IterApp head arg
, forall (uni :: * -> *) fun head arg r.
IterAppValue uni fun head arg r -> r
_iterTbv :: r
}
instance ( PrettyBy config (Plain Term uni fun)
, PrettyBy config head, PrettyBy config arg, PrettyConst r
) => PrettyBy config (IterAppValue uni fun head arg r) where
prettyBy :: forall ann. config -> IterAppValue uni fun head arg r -> Doc ann
prettyBy config
config (IterAppValue Plain Term uni fun
term IterApp head arg
pia r
y) = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
[ Doc ann
"{ ", config -> Plain Term uni fun -> Doc ann
forall ann. config -> Plain Term uni fun -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config Plain Term uni fun
term, Doc ann
forall ann. Doc ann
line
, Doc ann
"| ", config -> IterApp head arg -> Doc ann
forall ann. config -> IterApp head arg -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config IterApp head arg
pia, Doc ann
forall ann. Doc ann
line
, Doc ann
"| ", RenderContext -> r -> Doc ann
forall a ann. PrettyConst a => RenderContext -> a -> Doc ann
prettyConst RenderContext
botRenderContext r
y, Doc ann
forall ann. Doc ann
line
, Doc ann
"}"
]
runPlcT :: Monad m => TypedBuiltinGenT (Plain Term uni fun) m -> PlcGenT uni fun m a -> GenT m a
runPlcT :: forall (m :: * -> *) (uni :: * -> *) fun a.
Monad m =>
TypedBuiltinGenT (Plain Term uni fun) m
-> PlcGenT uni fun m a -> GenT m a
runPlcT TypedBuiltinGenT (Plain Term uni fun) m
genTb = BuiltinGensT uni fun m
-> GenT (ReaderT (BuiltinGensT uni fun m) m) a -> GenT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) r a.
(MFunctor t, Monad m) =>
r -> t (ReaderT r m) a -> t m a
hoistSupply (BuiltinGensT uni fun m
-> GenT (ReaderT (BuiltinGensT uni fun m) m) a -> GenT m a)
-> BuiltinGensT uni fun m
-> GenT (ReaderT (BuiltinGensT uni fun m) m) a
-> GenT m a
forall a b. (a -> b) -> a -> b
$ TypedBuiltinGenT (Plain Term uni fun) m -> BuiltinGensT uni fun m
forall (uni :: * -> *) fun (m :: * -> *).
TypedBuiltinGenT (Plain Term uni fun) m -> BuiltinGensT uni fun m
BuiltinGensT TypeRep a -> GenT m (TermOf (Plain Term uni fun) a)
TypedBuiltinGenT (Plain Term uni fun) m
genTb
iterAppValueToTermOf :: IterAppValue uni fun head arg r -> TermOf (Plain Term uni fun) r
iterAppValueToTermOf :: forall (uni :: * -> *) fun head arg r.
IterAppValue uni fun head arg r -> TermOf (Plain Term uni fun) r
iterAppValueToTermOf (IterAppValue Plain Term uni fun
term IterApp head arg
_ r
y) = Plain Term uni fun -> r -> TermOf (Plain Term uni fun) r
forall term a. term -> a -> TermOf term a
TermOf Plain Term uni fun
term r
y
revealUnique :: Name -> Name
revealUnique :: Name -> Name
revealUnique (Name Text
name Unique
uniq) =
Text -> Unique -> Name
Name (Text
name Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall str a. (Pretty a, Render str) => a -> str
display (Unique -> Int
unUnique Unique
uniq)) Unique
uniq
withTypedBuiltinGen
:: Monad m
=> Proxy fun
-> (forall a. (KnownTypeAst TyName DefaultUni a, MakeKnown (Plain Term DefaultUni fun) a) =>
TypeRep a -> GenT m c)
-> GenT m c
withTypedBuiltinGen :: forall (m :: * -> *) fun c.
Monad m =>
Proxy fun
-> (forall a.
(KnownTypeAst TyName DefaultUni a,
MakeKnown (Plain Term DefaultUni fun) a) =>
TypeRep a -> GenT m c)
-> GenT m c
withTypedBuiltinGen Proxy fun
_ forall a.
(KnownTypeAst TyName DefaultUni a,
MakeKnown (Plain Term DefaultUni fun) a) =>
TypeRep a -> GenT m c
k = [GenT m c] -> GenT m c
forall (m :: * -> *) a. MonadGen m => [m a] -> m a
Gen.choice
[ forall a.
(KnownTypeAst TyName DefaultUni a,
MakeKnown (Plain Term DefaultUni fun) a) =>
TypeRep a -> GenT m c
k @Integer TypeRep Integer
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
, forall a.
(KnownTypeAst TyName DefaultUni a,
MakeKnown (Plain Term DefaultUni fun) a) =>
TypeRep a -> GenT m c
k @BS.ByteString TypeRep ByteString
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
, forall a.
(KnownTypeAst TyName DefaultUni a,
MakeKnown (Plain Term DefaultUni fun) a) =>
TypeRep a -> GenT m c
k @Bool TypeRep Bool
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
]
genIterAppValue
:: forall head uni fun res m. Monad m
=> Denotation (Plain Term uni fun) head res
-> PlcGenT uni fun m (IterAppValue uni fun head (Plain Term uni fun) res)
genIterAppValue :: forall head (uni :: * -> *) fun res (m :: * -> *).
Monad m =>
Denotation (Plain Term uni fun) head res
-> PlcGenT
uni fun m (IterAppValue uni fun head (Plain Term uni fun) res)
genIterAppValue (Denotation head
object head -> Plain Term uni fun
embed FoldArgs args res
meta TypeScheme (Plain Term uni fun) args res
scheme) = PlcGenT
uni fun m (IterAppValue uni fun head (Plain Term uni fun) res)
result where
result :: PlcGenT
uni fun m (IterAppValue uni fun head (Plain Term uni fun) res)
result = TypeScheme (Plain Term uni fun) args res
-> Plain Term uni fun
-> ([Plain Term uni fun] -> [Plain Term uni fun])
-> FoldArgs args res
-> PlcGenT
uni fun m (IterAppValue uni fun head (Plain Term uni fun) res)
forall (args :: [*]).
TypeScheme (Plain Term uni fun) args res
-> Plain Term uni fun
-> ([Plain Term uni fun] -> [Plain Term uni fun])
-> FoldArgs args res
-> PlcGenT
uni fun m (IterAppValue uni fun head (Plain Term uni fun) res)
go TypeScheme (Plain Term uni fun) args res
scheme (head -> Plain Term uni fun
embed head
object) [Plain Term uni fun] -> [Plain Term uni fun]
forall a. a -> a
id FoldArgs args res
meta
go
:: TypeScheme (Plain Term uni fun) args res
-> Plain Term uni fun
-> ([Plain Term uni fun] -> [Plain Term uni fun])
-> FoldArgs args res
-> PlcGenT uni fun m (IterAppValue uni fun head (Plain Term uni fun) res)
go :: forall (args :: [*]).
TypeScheme (Plain Term uni fun) args res
-> Plain Term uni fun
-> ([Plain Term uni fun] -> [Plain Term uni fun])
-> FoldArgs args res
-> PlcGenT
uni fun m (IterAppValue uni fun head (Plain Term uni fun) res)
go TypeScheme (Plain Term uni fun) args res
TypeSchemeResult Plain Term uni fun
term [Plain Term uni fun] -> [Plain Term uni fun]
args FoldArgs args res
y = do
let pia :: IterApp head (Plain Term uni fun)
pia = head -> [Plain Term uni fun] -> IterApp head (Plain Term uni fun)
forall head arg. head -> [arg] -> IterApp head arg
IterApp head
object ([Plain Term uni fun] -> IterApp head (Plain Term uni fun))
-> [Plain Term uni fun] -> IterApp head (Plain Term uni fun)
forall a b. (a -> b) -> a -> b
$ [Plain Term uni fun] -> [Plain Term uni fun]
args []
IterAppValue uni fun head (Plain Term uni fun) res
-> PlcGenT
uni fun m (IterAppValue uni fun head (Plain Term uni fun) res)
forall a. a -> GenT (ReaderT (BuiltinGensT uni fun m) m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (IterAppValue uni fun head (Plain Term uni fun) res
-> PlcGenT
uni fun m (IterAppValue uni fun head (Plain Term uni fun) res))
-> IterAppValue uni fun head (Plain Term uni fun) res
-> PlcGenT
uni fun m (IterAppValue uni fun head (Plain Term uni fun) res)
forall a b. (a -> b) -> a -> b
$ Plain Term uni fun
-> IterApp head (Plain Term uni fun)
-> res
-> IterAppValue uni fun head (Plain Term uni fun) res
forall (uni :: * -> *) fun head arg r.
Plain Term uni fun
-> IterApp head arg -> r -> IterAppValue uni fun head arg r
IterAppValue Plain Term uni fun
term IterApp head (Plain Term uni fun)
pia res
FoldArgs args res
y
go (TypeSchemeArrow TypeScheme (Plain Term uni fun) args1 res
schB) Plain Term uni fun
term [Plain Term uni fun] -> [Plain Term uni fun]
args FoldArgs args res
f = do
BuiltinGensT TypedBuiltinGenT (Plain Term uni fun) m
genTb <- GenT (ReaderT (BuiltinGensT uni fun m) m) (BuiltinGensT uni fun m)
forall r (m :: * -> *). MonadReader r m => m r
ask
TermOf Plain Term uni fun
v arg
x <- GenT m (TermOf (Plain Term uni fun) arg)
-> GenT
(ReaderT (BuiltinGensT uni fun m) m)
(TermOf (Plain Term uni fun) arg)
forall (t :: (* -> *) -> * -> *) (s :: (* -> *) -> * -> *)
(m :: * -> *) a.
(MFunctor t, MonadTrans s, Monad m) =>
t m a -> t (s m) a
liftT (GenT m (TermOf (Plain Term uni fun) arg)
-> GenT
(ReaderT (BuiltinGensT uni fun m) m)
(TermOf (Plain Term uni fun) arg))
-> GenT m (TermOf (Plain Term uni fun) arg)
-> GenT
(ReaderT (BuiltinGensT uni fun m) m)
(TermOf (Plain Term uni fun) arg)
forall a b. (a -> b) -> a -> b
$ TypeRep arg -> GenT m (TermOf (Plain Term uni fun) arg)
TypedBuiltinGenT (Plain Term uni fun) m
genTb TypeRep arg
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
let term' :: Plain Term uni fun
term' = ()
-> Plain Term uni fun -> Plain Term uni fun -> Plain Term uni fun
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Plain Term uni fun
term Plain Term uni fun
v
args' :: [Plain Term uni fun] -> [Plain Term uni fun]
args' = [Plain Term uni fun] -> [Plain Term uni fun]
args ([Plain Term uni fun] -> [Plain Term uni fun])
-> ([Plain Term uni fun] -> [Plain Term uni fun])
-> [Plain Term uni fun]
-> [Plain Term uni fun]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Plain Term uni fun
v Plain Term uni fun -> [Plain Term uni fun] -> [Plain Term uni fun]
forall a. a -> [a] -> [a]
:)
y :: FoldArgs args1 res
y = FoldArgs args res
arg -> FoldArgs args1 res
f arg
x
TypeScheme (Plain Term uni fun) args1 res
-> Plain Term uni fun
-> ([Plain Term uni fun] -> [Plain Term uni fun])
-> FoldArgs args1 res
-> PlcGenT
uni fun m (IterAppValue uni fun head (Plain Term uni fun) res)
forall (args :: [*]).
TypeScheme (Plain Term uni fun) args res
-> Plain Term uni fun
-> ([Plain Term uni fun] -> [Plain Term uni fun])
-> FoldArgs args res
-> PlcGenT
uni fun m (IterAppValue uni fun head (Plain Term uni fun) res)
go TypeScheme (Plain Term uni fun) args1 res
schB Plain Term uni fun
term' [Plain Term uni fun] -> [Plain Term uni fun]
args' FoldArgs args1 res
y
go (TypeSchemeAll Proxy '(text, uniq, kind)
_ TypeScheme (Plain Term uni fun) args res
schK) Plain Term uni fun
term [Plain Term uni fun] -> [Plain Term uni fun]
args FoldArgs args res
f =
TypeScheme (Plain Term uni fun) args res
-> Plain Term uni fun
-> ([Plain Term uni fun] -> [Plain Term uni fun])
-> FoldArgs args res
-> PlcGenT
uni fun m (IterAppValue uni fun head (Plain Term uni fun) res)
forall (args :: [*]).
TypeScheme (Plain Term uni fun) args res
-> Plain Term uni fun
-> ([Plain Term uni fun] -> [Plain Term uni fun])
-> FoldArgs args res
-> PlcGenT
uni fun m (IterAppValue uni fun head (Plain Term uni fun) res)
go TypeScheme (Plain Term uni fun) args res
schK Plain Term uni fun
term [Plain Term uni fun] -> [Plain Term uni fun]
args FoldArgs args res
f
genTerm
:: forall uni fun m.
(uni ~ DefaultUni, Monad m)
=> TypedBuiltinGenT (Plain Term uni fun) m
-> DenotationContext (Plain Term uni fun)
-> Int
-> TypedBuiltinGenT (Plain Term uni fun) m
genTerm :: forall (uni :: * -> *) fun (m :: * -> *).
(uni ~ DefaultUni, Monad m) =>
TypedBuiltinGenT (Plain Term uni fun) m
-> DenotationContext (Plain Term uni fun)
-> Int
-> TypedBuiltinGenT (Plain Term uni fun) m
genTerm TypedBuiltinGenT (Plain Term uni fun) m
genBase DenotationContext (Plain Term uni fun)
context0 Int
depth0 = (forall a. QuoteT m a -> m a)
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) a)
-> GenT m (TermOf (Plain Term uni fun) a)
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
(b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
forall (m :: * -> *) (n :: * -> *) b.
Monad m =>
(forall a. m a -> n a) -> GenT m b -> GenT n b
Morph.hoist QuoteT m a -> m a
forall a. QuoteT m a -> m a
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT (GenT (QuoteT m) (TermOf (Plain Term uni fun) a)
-> GenT m (TermOf (Plain Term uni fun) a))
-> (TypeRep a -> GenT (QuoteT m) (TermOf (Plain Term uni fun) a))
-> TypeRep a
-> GenT m (TermOf (Plain Term uni fun) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DenotationContext (Plain Term uni fun)
-> Int
-> TypeRep a
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) a)
forall r.
DenotationContext (Plain Term uni fun)
-> Int
-> TypeRep r
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
go DenotationContext (Plain Term uni fun)
context0 Int
depth0 where
go
:: DenotationContext (Plain Term uni fun)
-> Int
-> TypeRep r
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
go :: forall r.
DenotationContext (Plain Term uni fun)
-> Int
-> TypeRep r
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
go DenotationContext (Plain Term uni fun)
context Int
depth TypeRep r
tr
| Int
depth Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
-> [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall (m :: * -> *) a.
Monad m =>
GenT m a -> [GenT m a] -> GenT m a
choiceDef (GenT m (TermOf (Plain Term uni fun) r)
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall (t :: (* -> *) -> * -> *) (s :: (* -> *) -> * -> *)
(m :: * -> *) a.
(MFunctor t, MonadTrans s, Monad m) =>
t m a -> t (s m) a
liftT (GenT m (TermOf (Plain Term uni fun) r)
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r))
-> GenT m (TermOf (Plain Term uni fun) r)
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall a b. (a -> b) -> a -> b
$ TypeRep r -> GenT m (TermOf (Plain Term uni fun) r)
TypedBuiltinGenT (Plain Term uni fun) m
genBase TypeRep r
tr) []
| Int
depth Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
-> [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall (m :: * -> *) a.
Monad m =>
GenT m a -> [GenT m a] -> GenT m a
choiceDef (GenT m (TermOf (Plain Term uni fun) r)
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall (t :: (* -> *) -> * -> *) (s :: (* -> *) -> * -> *)
(m :: * -> *) a.
(MFunctor t, MonadTrans s, Monad m) =>
t m a -> t (s m) a
liftT (GenT m (TermOf (Plain Term uni fun) r)
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r))
-> GenT m (TermOf (Plain Term uni fun) r)
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall a b. (a -> b) -> a -> b
$ TypeRep r -> GenT m (TermOf (Plain Term uni fun) r)
TypedBuiltinGenT (Plain Term uni fun) m
genBase TypeRep r
tr) ([GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r))
-> [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall a b. (a -> b) -> a -> b
$ [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
variables [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
-> [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
-> [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
forall a. [a] -> [a] -> [a]
++ [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
recursive
| Int
depth Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 = [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
Gen.frequency ([(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r))
-> [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall a b. (a -> b) -> a -> b
$ [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
stopOrDeeper [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
-> [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
-> [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
forall a. [a] -> [a] -> [a]
++ (GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
-> (Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r)))
-> [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
-> [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
forall a b. (a -> b) -> [a] -> [b]
map (Int
3 ,) [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
variables [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
-> [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
-> [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
forall a. [a] -> [a] -> [a]
++ (GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
-> (Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r)))
-> [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
-> [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
forall a b. (a -> b) -> [a] -> [b]
map (Int
5 ,) [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
recursive
| Int
depth Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
3 = [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
Gen.frequency ([(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r))
-> [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall a b. (a -> b) -> a -> b
$ [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
stopOrDeeper [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
-> [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
-> [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
forall a. [a] -> [a] -> [a]
++ (GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
-> (Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r)))
-> [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
-> [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
forall a b. (a -> b) -> [a] -> [b]
map (Int
3 ,) [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
recursive
| Bool
otherwise = [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
Gen.frequency [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
stopOrDeeper
where
stopOrDeeper :: [(Int, GenT (QuoteT m) (TermOf (Plain Term uni fun) r))]
stopOrDeeper = [(Int
1, GenT m (TermOf (Plain Term uni fun) r)
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall (t :: (* -> *) -> * -> *) (s :: (* -> *) -> * -> *)
(m :: * -> *) a.
(MFunctor t, MonadTrans s, Monad m) =>
t m a -> t (s m) a
liftT (GenT m (TermOf (Plain Term uni fun) r)
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r))
-> GenT m (TermOf (Plain Term uni fun) r)
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall a b. (a -> b) -> a -> b
$ TypeRep r -> GenT m (TermOf (Plain Term uni fun) r)
TypedBuiltinGenT (Plain Term uni fun) m
genBase TypeRep r
tr), (Int
5, GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
lambdaApply)]
builtinGens :: BuiltinGensT DefaultUni fun (QuoteT m)
builtinGens = TypedBuiltinGenT (Plain Term DefaultUni fun) (QuoteT m)
-> BuiltinGensT DefaultUni fun (QuoteT m)
forall (uni :: * -> *) fun (m :: * -> *).
TypedBuiltinGenT (Plain Term uni fun) m -> BuiltinGensT uni fun m
BuiltinGensT ((GenT (QuoteT m) (TermOf (Plain Term DefaultUni fun) a)
-> (TermOf (Plain Term DefaultUni fun) a
-> TermOf (Plain Term DefaultUni fun) a)
-> GenT (QuoteT m) (TermOf (Plain Term DefaultUni fun) a))
-> (TermOf (Plain Term DefaultUni fun) a
-> TermOf (Plain Term DefaultUni fun) a)
-> GenT (QuoteT m) (TermOf (Plain Term DefaultUni fun) a)
-> GenT (QuoteT m) (TermOf (Plain Term DefaultUni fun) a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip GenT (QuoteT m) (TermOf (Plain Term DefaultUni fun) a)
-> (TermOf (Plain Term DefaultUni fun) a
-> TermOf (Plain Term DefaultUni fun) a)
-> GenT (QuoteT m) (TermOf (Plain Term DefaultUni fun) a)
forall (m :: * -> *) a. MonadGen m => m a -> (a -> a) -> m a
Gen.subterm TermOf (Plain Term DefaultUni fun) a
-> TermOf (Plain Term DefaultUni fun) a
forall a. a -> a
id (GenT (QuoteT m) (TermOf (Plain Term DefaultUni fun) a)
-> GenT (QuoteT m) (TermOf (Plain Term DefaultUni fun) a))
-> (TypeRep a
-> GenT (QuoteT m) (TermOf (Plain Term DefaultUni fun) a))
-> TypeRep a
-> GenT (QuoteT m) (TermOf (Plain Term DefaultUni fun) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DenotationContext (Plain Term uni fun)
-> Int
-> TypeRep a
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) a)
forall r.
DenotationContext (Plain Term uni fun)
-> Int
-> TypeRep r
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
go DenotationContext (Plain Term uni fun)
context (Int
depth Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
proceed :: DenotationContextMember (Plain Term uni fun) r
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
proceed (DenotationContextMember Denotation (Plain Term uni fun) object r
denotation) =
(IterAppValue DefaultUni fun object (Plain Term DefaultUni fun) r
-> TermOf (Plain Term DefaultUni fun) r)
-> GenT
(QuoteT m)
(IterAppValue DefaultUni fun object (Plain Term DefaultUni fun) r)
-> GenT (QuoteT m) (TermOf (Plain Term DefaultUni fun) r)
forall a b. (a -> b) -> GenT (QuoteT m) a -> GenT (QuoteT m) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IterAppValue DefaultUni fun object (Plain Term DefaultUni fun) r
-> TermOf (Plain Term DefaultUni fun) r
forall (uni :: * -> *) fun head arg r.
IterAppValue uni fun head arg r -> TermOf (Plain Term uni fun) r
iterAppValueToTermOf (GenT
(QuoteT m)
(IterAppValue DefaultUni fun object (Plain Term DefaultUni fun) r)
-> GenT (QuoteT m) (TermOf (Plain Term DefaultUni fun) r))
-> (GenT
(ReaderT (BuiltinGensT DefaultUni fun (QuoteT m)) (QuoteT m))
(IterAppValue DefaultUni fun object (Plain Term DefaultUni fun) r)
-> GenT
(QuoteT m)
(IterAppValue DefaultUni fun object (Plain Term DefaultUni fun) r))
-> GenT
(ReaderT (BuiltinGensT DefaultUni fun (QuoteT m)) (QuoteT m))
(IterAppValue DefaultUni fun object (Plain Term DefaultUni fun) r)
-> GenT (QuoteT m) (TermOf (Plain Term DefaultUni fun) r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinGensT DefaultUni fun (QuoteT m)
-> GenT
(ReaderT (BuiltinGensT DefaultUni fun (QuoteT m)) (QuoteT m))
(IterAppValue DefaultUni fun object (Plain Term DefaultUni fun) r)
-> GenT
(QuoteT m)
(IterAppValue DefaultUni fun object (Plain Term DefaultUni fun) r)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) r a.
(MFunctor t, Monad m) =>
r -> t (ReaderT r m) a -> t m a
hoistSupply BuiltinGensT DefaultUni fun (QuoteT m)
builtinGens (GenT
(ReaderT (BuiltinGensT DefaultUni fun (QuoteT m)) (QuoteT m))
(IterAppValue DefaultUni fun object (Plain Term DefaultUni fun) r)
-> GenT (QuoteT m) (TermOf (Plain Term DefaultUni fun) r))
-> GenT
(ReaderT (BuiltinGensT DefaultUni fun (QuoteT m)) (QuoteT m))
(IterAppValue DefaultUni fun object (Plain Term DefaultUni fun) r)
-> GenT (QuoteT m) (TermOf (Plain Term DefaultUni fun) r)
forall a b. (a -> b) -> a -> b
$ Denotation (Plain Term DefaultUni fun) object r
-> GenT
(ReaderT (BuiltinGensT DefaultUni fun (QuoteT m)) (QuoteT m))
(IterAppValue DefaultUni fun object (Plain Term DefaultUni fun) r)
forall head (uni :: * -> *) fun res (m :: * -> *).
Monad m =>
Denotation (Plain Term uni fun) head res
-> PlcGenT
uni fun m (IterAppValue uni fun head (Plain Term uni fun) res)
genIterAppValue Denotation (Plain Term uni fun) object r
Denotation (Plain Term DefaultUni fun) object r
denotation
variables :: [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
variables = (DenotationContextMember (Plain Term uni fun) r
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r))
-> [DenotationContextMember (Plain Term uni fun) r]
-> [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
forall a b. (a -> b) -> [a] -> [b]
map DenotationContextMember (Plain Term uni fun) r
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
proceed ([DenotationContextMember (Plain Term uni fun) r]
-> [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)])
-> [DenotationContextMember (Plain Term uni fun) r]
-> [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
forall a b. (a -> b) -> a -> b
$ TypeRep r
-> DenotationContext (Plain Term uni fun)
-> [DenotationContextMember (Plain Term uni fun) r]
forall a term.
TypeRep a
-> DenotationContext term -> [DenotationContextMember term a]
lookupInContext TypeRep r
tr DenotationContext (Plain Term uni fun)
context
recursive :: [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
recursive = (DenotationContextMember (Plain Term uni fun) r
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r))
-> [DenotationContextMember (Plain Term uni fun) r]
-> [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
forall a b. (a -> b) -> [a] -> [b]
map DenotationContextMember (Plain Term uni fun) r
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
proceed ([DenotationContextMember (Plain Term uni fun) r]
-> [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)])
-> [DenotationContextMember (Plain Term uni fun) r]
-> [GenT (QuoteT m) (TermOf (Plain Term uni fun) r)]
forall a b. (a -> b) -> a -> b
$ TypeRep r
-> DenotationContext (Plain Term uni fun)
-> [DenotationContextMember (Plain Term uni fun) r]
forall a term.
TypeRep a
-> DenotationContext term -> [DenotationContextMember term a]
lookupInContext TypeRep r
tr DenotationContext (Plain Term uni fun)
context
lambdaApply :: GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
lambdaApply = Proxy fun
-> (forall a.
(KnownTypeAst TyName DefaultUni a,
MakeKnown (Plain Term DefaultUni fun) a) =>
TypeRep a -> GenT (QuoteT m) (TermOf (Plain Term uni fun) r))
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall (m :: * -> *) fun c.
Monad m =>
Proxy fun
-> (forall a.
(KnownTypeAst TyName DefaultUni a,
MakeKnown (Plain Term DefaultUni fun) a) =>
TypeRep a -> GenT m c)
-> GenT m c
withTypedBuiltinGen (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @fun) ((forall a.
(KnownTypeAst TyName DefaultUni a,
MakeKnown (Plain Term DefaultUni fun) a) =>
TypeRep a -> GenT (QuoteT m) (TermOf (Plain Term uni fun) r))
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r))
-> (forall a.
(KnownTypeAst TyName DefaultUni a,
MakeKnown (Plain Term DefaultUni fun) a) =>
TypeRep a -> GenT (QuoteT m) (TermOf (Plain Term uni fun) r))
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall a b. (a -> b) -> a -> b
$ \TypeRep a
argTr -> do
Name
name <- QuoteT m Name -> GenT (QuoteT m) Name
forall (m :: * -> *) a. Monad m => m a -> GenT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (QuoteT m Name -> GenT (QuoteT m) Name)
-> QuoteT m Name -> GenT (QuoteT m) Name
forall a b. (a -> b) -> a -> b
$ Name -> Name
revealUnique (Name -> Name) -> QuoteT m Name -> QuoteT m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> QuoteT m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
let argTy :: Type TyName uni ()
argTy = TypeRep a -> Type TyName uni ()
forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst tyname uni x =>
proxy x -> Type tyname uni ()
toTypeAst TypeRep a
argTr
TermOf Plain Term uni fun
arg a
x <- DenotationContext (Plain Term uni fun)
-> Int
-> TypeRep a
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) a)
forall r.
DenotationContext (Plain Term uni fun)
-> Int
-> TypeRep r
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
go DenotationContext (Plain Term uni fun)
context (Int
depth Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) TypeRep a
argTr
TermOf Plain Term uni fun
body r
y <- DenotationContext (Plain Term uni fun)
-> Int
-> TypeRep r
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall r.
DenotationContext (Plain Term uni fun)
-> Int
-> TypeRep r
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
go (Name
-> TypeRep a
-> a
-> DenotationContext (Plain Term uni fun)
-> DenotationContext (Plain Term uni fun)
forall (uni :: * -> *) fun a.
KnownType (Term TyName Name uni fun ()) a =>
Name
-> TypeRep a
-> a
-> DenotationContext (Term TyName Name uni fun ())
-> DenotationContext (Term TyName Name uni fun ())
insertVariable Name
name TypeRep a
argTr a
x DenotationContext (Plain Term uni fun)
context) (Int
depth Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) TypeRep r
tr
let term :: Plain Term uni fun
term = ()
-> Plain Term uni fun -> Plain Term uni fun -> Plain Term uni fun
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (()
-> Name
-> Type TyName uni ()
-> Plain Term uni fun
-> Plain Term uni fun
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
name Type TyName uni ()
argTy Plain Term uni fun
body) Plain Term uni fun
arg
TermOf (Plain Term uni fun) r
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall a. a -> GenT (QuoteT m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermOf (Plain Term uni fun) r
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r))
-> TermOf (Plain Term uni fun) r
-> GenT (QuoteT m) (TermOf (Plain Term uni fun) r)
forall a b. (a -> b) -> a -> b
$ Plain Term uni fun -> r -> TermOf (Plain Term uni fun) r
forall term a. term -> a -> TermOf term a
TermOf Plain Term uni fun
term r
y
genTermLoose :: Monad m => TypedBuiltinGenT (Plain Term DefaultUni DefaultFun) m
genTermLoose :: forall (m :: * -> *).
Monad m =>
TypedBuiltinGenT (Plain Term DefaultUni DefaultFun) m
genTermLoose = TypedBuiltinGenT (Plain Term DefaultUni DefaultFun) m
-> DenotationContext (Plain Term DefaultUni DefaultFun)
-> Int
-> TypedBuiltinGenT (Plain Term DefaultUni DefaultFun) m
forall (uni :: * -> *) fun (m :: * -> *).
(uni ~ DefaultUni, Monad m) =>
TypedBuiltinGenT (Plain Term uni fun) m
-> DenotationContext (Plain Term uni fun)
-> Int
-> TypedBuiltinGenT (Plain Term uni fun) m
genTerm TypeRep a -> GenT m (TermOf (Plain Term DefaultUni DefaultFun) a)
TypedBuiltinGenT (Plain Term DefaultUni DefaultFun) m
forall term (m :: * -> *).
(HasConstantIn DefaultUni term, Monad m) =>
TypedBuiltinGenT term m
genTypedBuiltinDef DenotationContext (Plain Term DefaultUni DefaultFun)
typedBuiltins Int
4
withAnyTermLoose
:: (uni ~ DefaultUni, fun ~ DefaultFun, Monad m)
=> (forall a. KnownType (Plain Term uni fun) a => TermOf (Plain Term uni fun) a -> GenT m c)
-> GenT m c
withAnyTermLoose :: forall (uni :: * -> *) fun (m :: * -> *) c.
(uni ~ DefaultUni, fun ~ DefaultFun, Monad m) =>
(forall a.
KnownType (Plain Term uni fun) a =>
TermOf (Plain Term uni fun) a -> GenT m c)
-> GenT m c
withAnyTermLoose forall a.
KnownType (Plain Term uni fun) a =>
TermOf (Plain Term uni fun) a -> GenT m c
k = Proxy DefaultFun
-> (forall {a}.
(KnownTypeAst TyName DefaultUni a,
MakeKnown (Plain Term DefaultUni DefaultFun) a) =>
TypeRep a -> GenT m c)
-> GenT m c
forall (m :: * -> *) fun c.
Monad m =>
Proxy fun
-> (forall a.
(KnownTypeAst TyName DefaultUni a,
MakeKnown (Plain Term DefaultUni fun) a) =>
TypeRep a -> GenT m c)
-> GenT m c
withTypedBuiltinGen (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @DefaultFun) ((forall {a}.
(KnownTypeAst TyName DefaultUni a,
MakeKnown (Plain Term DefaultUni DefaultFun) a) =>
TypeRep a -> GenT m c)
-> GenT m c)
-> (forall {a}.
(KnownTypeAst TyName DefaultUni a,
MakeKnown (Plain Term DefaultUni DefaultFun) a) =>
TypeRep a -> GenT m c)
-> GenT m c
forall a b. (a -> b) -> a -> b
$ \TypeRep a
tr -> TypeRep a -> GenT m (TermOf (Plain Term DefaultUni DefaultFun) a)
TypedBuiltinGenT (Plain Term DefaultUni DefaultFun) m
forall (m :: * -> *).
Monad m =>
TypedBuiltinGenT (Plain Term DefaultUni DefaultFun) m
genTermLoose TypeRep a
tr GenT m (TermOf (Plain Term DefaultUni DefaultFun) a)
-> (TermOf (Plain Term DefaultUni DefaultFun) a -> GenT m c)
-> GenT m c
forall a b. GenT m a -> (a -> GenT m b) -> GenT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TermOf (Plain Term uni fun) a -> GenT m c
TermOf (Plain Term DefaultUni DefaultFun) a -> GenT m c
forall a.
KnownType (Plain Term uni fun) a =>
TermOf (Plain Term uni fun) a -> GenT m c
k