-- editorconfig-checker-disable-file
-- | Generators of various PLC things: 'Builtin's, 'IterApp's, 'Term's, etc.

{-# 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 ()

-- | Generators of built-ins supplied to computations that run in the 'PlcGenT' monad.
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
      -- ^ Generates a PLC 'Term' and the corresponding
      -- Haskell value out of a 'TypedBuiltin'.
    }

-- | The type used in generators defined in this module.
-- It's parameterized by a 'BuiltinGensT' which makes it possible to supply
-- different generators of built-in types. For example, 'genTypedBuiltinDiv'
-- never generates a zero, so this generator can be used in order to avoid the
-- divide-by-zero-induced @error@. Supplied generators are of arbitrary complexity
-- and can call the currently running generator recursively, for example.
type PlcGenT uni fun m = GenT (ReaderT (BuiltinGensT uni fun m) m)

-- | A function (called "head") applied to a list of arguments (called "spine").
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

-- | One iterated application of a @head@ to @arg@s represented in three distinct ways.
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  -- ^ As a PLC 'Term'.
    , forall (uni :: * -> *) fun head arg r.
IterAppValue uni fun head arg r -> IterApp head arg
_iterApp  :: IterApp head arg    -- ^ As an 'IterApp'.
    , forall (uni :: * -> *) fun head arg r.
IterAppValue uni fun head arg r -> r
_iterTbv  :: r                   -- ^ As a Haskell value.
    }

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
"}"
        ]

-- | Run a 'PlcGenT' computation by supplying built-ins generators.
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

-- | Get a 'TermOf' out of an 'IterAppValue'.
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

-- | Add to the 'ByteString' representation of a 'Name' its 'Unique'
-- without any additional symbols inbetween.
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

-- TODO: we can generate more types here.
-- | Generate a 'Builtin' and supply its typed version to a continuation.
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
    ]

-- | Generate an 'IterAppValue' from a 'Denotation'.
-- If the 'Denotation' has a functional type, then all arguments are generated and
-- supplied to the denotation. Since 'IterAppValue' consists of three components, we
--   1. grow the 'Term' component by applying it to arguments using 'Apply'
--   2. grow the 'IterApp' component by appending arguments to its spine
--   3. feed arguments to the Haskell function
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  -- Computed the result.
        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  -- Another argument is required.
        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  -- Get a Haskell and the corresponding PLC values.
        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          -- Apply the term to the PLC value.
            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]
:)             -- Append the PLC value to the spine.
            y :: FoldArgs args1 res
y     = FoldArgs args res
arg -> FoldArgs args1 res
f arg
x                      -- Apply the Haskell function to the generated argument.
        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

-- | Generate a PLC 'Term' of the specified type and the corresponding Haskell value.
-- Generates first-order functions and constants including constant applications.
-- Arguments to functions and 'Builtin's are generated recursively.
genTerm
    :: forall uni fun m.
       (uni ~ DefaultUni, Monad m)
    => TypedBuiltinGenT (Plain Term uni fun) m
       -- ^ Ground generators of built-ins. The base case of the recursion.
    -> DenotationContext (Plain Term uni fun)
       -- ^ A context to generate terms in. See for example 'typedBuiltins'.
       -- Gets extended by a variable when an applied lambda is generated.
    -> Int
       -- ^ Depth of recursion.
    -> 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
        -- FIXME: should be using 'variables' but this is now the same as 'recursive'
        | 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)]
            -- Generators of built-ins to feed them to 'genIterAppValue'.
            -- Note that the typed built-ins generator calls 'go' recursively.
            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))
            -- Generate arguments for functions recursively or return a variable.
            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
            -- A list of variables generators.
            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
            -- A list of recursive generators.
            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
            -- Generate a lambda and immediately apply it to a generated argument of a generated type.
            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
                -- Generate a name for the name representing the argument.
                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"
                -- Get the 'Type' of the argument from a generated 'TypedBuiltin'.
                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
                -- Generate the argument.
                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
                -- Generate the body of the lambda abstraction adding the new variable to the context.
                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
                -- Assemble the term.
                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

-- | Generates a 'Term' with rather small values to make out-of-bounds failures less likely.
-- There are still like a half of terms that fail with out-of-bounds errors being evaluated.
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

-- | Generate a 'TypedBuiltin' and a 'TermOf' of the corresponding type,
-- attach the 'TypedBuiltin' to the value part of the 'TermOf' and pass that to a continuation.
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