-- | This module defines the 'TypedBuiltinGen' type and functions of this type.

{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE UndecidableInstances  #-}

module PlutusCore.Generators.Hedgehog.TypedBuiltinGen
    ( TermOf(..)
    , TypedBuiltinGenT
    , TypedBuiltinGen
    , genLowerBytes
    , genTypedBuiltinFail
    , genTypedBuiltinDef
    ) where

import PlutusPrelude

import PlutusCore
import PlutusCore.Builtin
import PlutusCore.Pretty

import Data.ByteString qualified as BS
import Data.Functor.Identity
import Hedgehog hiding (Size, Var)
import Hedgehog.Gen qualified as Gen
import Hedgehog.Range qualified as Range
import Prettyprinter
import Type.Reflection

-- | Generate a UTF-8 lazy 'ByteString' containing lower-case letters.
genLowerBytes :: Monad m => Range Int -> GenT m BS.ByteString
genLowerBytes :: forall (m :: * -> *). Monad m => Range Int -> GenT m ByteString
genLowerBytes Range Int
range = Range Int -> GenT m Char -> GenT m ByteString
forall (m :: * -> *).
MonadGen m =>
Range Int -> m Char -> m ByteString
Gen.utf8 Range Int
range GenT m Char
forall (m :: * -> *). MonadGen m => m Char
Gen.lower

-- TODO: rename me to @TermWith@.
-- | A @term@ along with the corresponding Haskell value.
data TermOf term a = TermOf
    { forall term a. TermOf term a -> term
_termOfTerm  :: term  -- ^ The term
    , forall term a. TermOf term a -> a
_termOfValue :: a     -- ^ The Haskell value.
    } deriving stock ((forall a b. (a -> b) -> TermOf term a -> TermOf term b)
-> (forall a b. a -> TermOf term b -> TermOf term a)
-> Functor (TermOf term)
forall a b. a -> TermOf term b -> TermOf term a
forall a b. (a -> b) -> TermOf term a -> TermOf term b
forall term a b. a -> TermOf term b -> TermOf term a
forall term a b. (a -> b) -> TermOf term a -> TermOf term b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall term a b. (a -> b) -> TermOf term a -> TermOf term b
fmap :: forall a b. (a -> b) -> TermOf term a -> TermOf term b
$c<$ :: forall term a b. a -> TermOf term b -> TermOf term a
<$ :: forall a b. a -> TermOf term b -> TermOf term a
Functor, (forall m. Monoid m => TermOf term m -> m)
-> (forall m a. Monoid m => (a -> m) -> TermOf term a -> m)
-> (forall m a. Monoid m => (a -> m) -> TermOf term a -> m)
-> (forall a b. (a -> b -> b) -> b -> TermOf term a -> b)
-> (forall a b. (a -> b -> b) -> b -> TermOf term a -> b)
-> (forall b a. (b -> a -> b) -> b -> TermOf term a -> b)
-> (forall b a. (b -> a -> b) -> b -> TermOf term a -> b)
-> (forall a. (a -> a -> a) -> TermOf term a -> a)
-> (forall a. (a -> a -> a) -> TermOf term a -> a)
-> (forall a. TermOf term a -> [a])
-> (forall a. TermOf term a -> Bool)
-> (forall a. TermOf term a -> Int)
-> (forall a. Eq a => a -> TermOf term a -> Bool)
-> (forall a. Ord a => TermOf term a -> a)
-> (forall a. Ord a => TermOf term a -> a)
-> (forall a. Num a => TermOf term a -> a)
-> (forall a. Num a => TermOf term a -> a)
-> Foldable (TermOf term)
forall a. Eq a => a -> TermOf term a -> Bool
forall a. Num a => TermOf term a -> a
forall a. Ord a => TermOf term a -> a
forall m. Monoid m => TermOf term m -> m
forall a. TermOf term a -> Bool
forall a. TermOf term a -> Int
forall a. TermOf term a -> [a]
forall a. (a -> a -> a) -> TermOf term a -> a
forall term a. Eq a => a -> TermOf term a -> Bool
forall term a. Num a => TermOf term a -> a
forall term a. Ord a => TermOf term a -> a
forall m a. Monoid m => (a -> m) -> TermOf term a -> m
forall term m. Monoid m => TermOf term m -> m
forall term a. TermOf term a -> Bool
forall term a. TermOf term a -> Int
forall term a. TermOf term a -> [a]
forall b a. (b -> a -> b) -> b -> TermOf term a -> b
forall a b. (a -> b -> b) -> b -> TermOf term a -> b
forall term a. (a -> a -> a) -> TermOf term a -> a
forall term m a. Monoid m => (a -> m) -> TermOf term a -> m
forall term b a. (b -> a -> b) -> b -> TermOf term a -> b
forall term a b. (a -> b -> b) -> b -> TermOf term a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall term m. Monoid m => TermOf term m -> m
fold :: forall m. Monoid m => TermOf term m -> m
$cfoldMap :: forall term m a. Monoid m => (a -> m) -> TermOf term a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> TermOf term a -> m
$cfoldMap' :: forall term m a. Monoid m => (a -> m) -> TermOf term a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> TermOf term a -> m
$cfoldr :: forall term a b. (a -> b -> b) -> b -> TermOf term a -> b
foldr :: forall a b. (a -> b -> b) -> b -> TermOf term a -> b
$cfoldr' :: forall term a b. (a -> b -> b) -> b -> TermOf term a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> TermOf term a -> b
$cfoldl :: forall term b a. (b -> a -> b) -> b -> TermOf term a -> b
foldl :: forall b a. (b -> a -> b) -> b -> TermOf term a -> b
$cfoldl' :: forall term b a. (b -> a -> b) -> b -> TermOf term a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> TermOf term a -> b
$cfoldr1 :: forall term a. (a -> a -> a) -> TermOf term a -> a
foldr1 :: forall a. (a -> a -> a) -> TermOf term a -> a
$cfoldl1 :: forall term a. (a -> a -> a) -> TermOf term a -> a
foldl1 :: forall a. (a -> a -> a) -> TermOf term a -> a
$ctoList :: forall term a. TermOf term a -> [a]
toList :: forall a. TermOf term a -> [a]
$cnull :: forall term a. TermOf term a -> Bool
null :: forall a. TermOf term a -> Bool
$clength :: forall term a. TermOf term a -> Int
length :: forall a. TermOf term a -> Int
$celem :: forall term a. Eq a => a -> TermOf term a -> Bool
elem :: forall a. Eq a => a -> TermOf term a -> Bool
$cmaximum :: forall term a. Ord a => TermOf term a -> a
maximum :: forall a. Ord a => TermOf term a -> a
$cminimum :: forall term a. Ord a => TermOf term a -> a
minimum :: forall a. Ord a => TermOf term a -> a
$csum :: forall term a. Num a => TermOf term a -> a
sum :: forall a. Num a => TermOf term a -> a
$cproduct :: forall term a. Num a => TermOf term a -> a
product :: forall a. Num a => TermOf term a -> a
Foldable, Functor (TermOf term)
Foldable (TermOf term)
(Functor (TermOf term), Foldable (TermOf term)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> TermOf term a -> f (TermOf term b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    TermOf term (f a) -> f (TermOf term a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TermOf term a -> m (TermOf term b))
-> (forall (m :: * -> *) a.
    Monad m =>
    TermOf term (m a) -> m (TermOf term a))
-> Traversable (TermOf term)
forall term. Functor (TermOf term)
forall term. Foldable (TermOf term)
forall term (m :: * -> *) a.
Monad m =>
TermOf term (m a) -> m (TermOf term a)
forall term (f :: * -> *) a.
Applicative f =>
TermOf term (f a) -> f (TermOf term a)
forall term (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TermOf term a -> m (TermOf term b)
forall term (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TermOf term a -> f (TermOf term b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
TermOf term (m a) -> m (TermOf term a)
forall (f :: * -> *) a.
Applicative f =>
TermOf term (f a) -> f (TermOf term a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TermOf term a -> m (TermOf term b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TermOf term a -> f (TermOf term b)
$ctraverse :: forall term (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TermOf term a -> f (TermOf term b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TermOf term a -> f (TermOf term b)
$csequenceA :: forall term (f :: * -> *) a.
Applicative f =>
TermOf term (f a) -> f (TermOf term a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
TermOf term (f a) -> f (TermOf term a)
$cmapM :: forall term (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TermOf term a -> m (TermOf term b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TermOf term a -> m (TermOf term b)
$csequence :: forall term (m :: * -> *) a.
Monad m =>
TermOf term (m a) -> m (TermOf term a)
sequence :: forall (m :: * -> *) a.
Monad m =>
TermOf term (m a) -> m (TermOf term a)
Traversable)

-- | A function of this type generates values of built-in typed (see 'TypedBuiltin' for
-- the list of such types) and returns it along with the corresponding PLC value.
type TypedBuiltinGenT term m = forall a. TypeRep a -> GenT m (TermOf term a)

-- | 'TypedBuiltinGenT' specified to 'Identity'.
type TypedBuiltinGen term = TypedBuiltinGenT term Identity

instance (PrettyBy config a, PrettyBy config term) =>
        PrettyBy config (TermOf term a) where
    prettyBy :: forall ann. config -> TermOf term a -> Doc ann
prettyBy config
config (TermOf term
t a
x) = config -> term -> Doc ann
forall ann. config -> term -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config term
t Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"~>" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> config -> a -> Doc ann
forall ann. config -> a -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy config
config a
x

attachCoercedTerm
    :: (Monad m, MakeKnown term a, PrettyConst a)
    => GenT m a -> GenT m (TermOf term a)
attachCoercedTerm :: forall (m :: * -> *) term a.
(Monad m, MakeKnown term a, PrettyConst a) =>
GenT m a -> GenT m (TermOf term a)
attachCoercedTerm GenT m a
a = do
    a
x <- GenT m a
a
    case a -> EvaluationResult (HeadSpine term)
forall (uni :: * -> *) val a.
MakeKnownIn uni val a =>
a -> EvaluationResult (HeadSpine val)
makeKnownOrFail a
x of
        -- I've attempted to implement support for generating 'EvaluationFailure',
        -- but it turned out to be too much of a pain for something that we do not really need.
        EvaluationResult (HeadSpine term)
EvaluationFailure -> [Char] -> GenT m (TermOf term a)
forall a. [Char] -> GenT m a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> GenT m (TermOf term a))
-> [Char] -> GenT m (TermOf term a)
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ [Char]
"Got 'EvaluationFailure' when generating a value of a built-in type: "
            , Doc Any -> [Char]
forall ann. Doc ann -> [Char]
forall str ann. Render str => Doc ann -> str
render (Doc Any -> [Char]) -> Doc Any -> [Char]
forall a b. (a -> b) -> a -> b
$ RenderContext -> a -> Doc Any
forall a ann. PrettyConst a => RenderContext -> a -> Doc ann
prettyConst RenderContext
botRenderContext a
x
            ]
        EvaluationSuccess HeadSpine term
res -> case HeadSpine term
res of
            HeadOnly term
v -> TermOf term a -> GenT m (TermOf term a)
forall a. a -> GenT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TermOf term a -> GenT m (TermOf term a))
-> TermOf term a -> GenT m (TermOf term a)
forall a b. (a -> b) -> a -> b
$ term -> a -> TermOf term a
forall term a. term -> a -> TermOf term a
TermOf term
v a
x
            HeadSpine term
_          -> [Char] -> GenT m (TermOf term a)
forall a. [Char] -> GenT m a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
"Iterated application is not supported"

-- | Update a typed built-ins generator by overwriting the generator for a certain built-in.
updateTypedBuiltinGen
    :: forall a term m. (Typeable a, MakeKnown term a, PrettyConst a, Monad m)
    => GenT m a                  -- ^ A new generator.
    -> TypedBuiltinGenT term m   -- ^ An old typed built-ins generator.
    -> TypedBuiltinGenT term m   -- ^ The updated typed built-ins generator.
updateTypedBuiltinGen :: forall a term (m :: * -> *).
(Typeable a, MakeKnown term a, PrettyConst a, Monad m) =>
GenT m a -> TypedBuiltinGenT term m -> TypedBuiltinGenT term m
updateTypedBuiltinGen GenT m a
genX TypedBuiltinGenT term m
genTb TypeRep a
tr
    | Just a :~: a
Refl <- forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a TypeRep a -> TypeRep a -> Maybe (a :~: a)
forall a b. TypeRep a -> TypeRep b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
`geq` TypeRep a
tr = GenT m a -> GenT m (TermOf term a)
forall (m :: * -> *) term a.
(Monad m, MakeKnown term a, PrettyConst a) =>
GenT m a -> GenT m (TermOf term a)
attachCoercedTerm GenT m a
GenT m a
genX
    | Bool
otherwise                        = TypeRep a -> GenT m (TermOf term a)
TypedBuiltinGenT term m
genTb TypeRep a
tr

-- | A built-ins generator that always fails.
genTypedBuiltinFail :: Monad m => TypedBuiltinGenT term m
genTypedBuiltinFail :: forall (m :: * -> *) term. Monad m => TypedBuiltinGenT term m
genTypedBuiltinFail TypeRep a
tb = [Char] -> GenT m (TermOf term a)
forall a. [Char] -> GenT m a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> GenT m (TermOf term a))
-> [Char] -> GenT m (TermOf term a)
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
    [ [Char]
"A generator for the following built-in is not implemented: "
    , TypeRep a -> [Char]
forall a. Show a => a -> [Char]
show TypeRep a
tb
    ]

-- | A default built-ins generator.
genTypedBuiltinDef
    :: (HasConstantIn DefaultUni term, Monad m)
    => TypedBuiltinGenT term m
genTypedBuiltinDef :: forall term (m :: * -> *).
(HasConstantIn DefaultUni term, Monad m) =>
TypedBuiltinGenT term m
genTypedBuiltinDef
    = forall a term (m :: * -> *).
(Typeable a, MakeKnown term a, PrettyConst a, Monad m) =>
GenT m a -> TypedBuiltinGenT term m -> TypedBuiltinGenT term m
updateTypedBuiltinGen @Integer (Range Integer -> GenT m Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Range Integer -> GenT m Integer)
-> Range Integer -> GenT m Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer -> Range Integer
forall a. Integral a => a -> a -> a -> Range a
Range.linearFrom Integer
0 Integer
0 Integer
10)
    ((forall {a}. TypeRep a -> GenT m (TermOf term a))
 -> forall {a}. TypeRep a -> GenT m (TermOf term a))
-> (forall {a}. TypeRep a -> GenT m (TermOf term a))
-> forall {a}. TypeRep a -> GenT m (TermOf term a)
forall a b. (a -> b) -> a -> b
$ GenT m ByteString
-> (forall {a}. TypeRep a -> GenT m (TermOf term a))
-> forall {a}. TypeRep a -> GenT m (TermOf term a)
forall a term (m :: * -> *).
(Typeable a, MakeKnown term a, PrettyConst a, Monad m) =>
GenT m a -> TypedBuiltinGenT term m -> TypedBuiltinGenT term m
updateTypedBuiltinGen (Range Int -> GenT m ByteString
forall (m :: * -> *). Monad m => Range Int -> GenT m ByteString
genLowerBytes (Int -> Int -> Range Int
forall a. Integral a => a -> a -> Range a
Range.linear Int
0 Int
10))
    ((forall {a}. TypeRep a -> GenT m (TermOf term a))
 -> forall {a}. TypeRep a -> GenT m (TermOf term a))
-> (forall {a}. TypeRep a -> GenT m (TermOf term a))
-> forall {a}. TypeRep a -> GenT m (TermOf term a)
forall a b. (a -> b) -> a -> b
$ GenT m Bool
-> (forall {a}. TypeRep a -> GenT m (TermOf term a))
-> forall {a}. TypeRep a -> GenT m (TermOf term a)
forall a term (m :: * -> *).
(Typeable a, MakeKnown term a, PrettyConst a, Monad m) =>
GenT m a -> TypedBuiltinGenT term m -> TypedBuiltinGenT term m
updateTypedBuiltinGen GenT m Bool
forall (m :: * -> *). MonadGen m => m Bool
Gen.bool
    ((forall {a}. TypeRep a -> GenT m (TermOf term a))
 -> forall {a}. TypeRep a -> GenT m (TermOf term a))
-> (forall {a}. TypeRep a -> GenT m (TermOf term a))
-> forall {a}. TypeRep a -> GenT m (TermOf term a)
forall a b. (a -> b) -> a -> b
$ TypeRep a -> GenT m (TermOf term a)
forall {a}. TypeRep a -> GenT m (TermOf term a)
forall (m :: * -> *) term. Monad m => TypedBuiltinGenT term m
genTypedBuiltinFail