Unsuccessful attempt to generalize 'TypedBuiltinGen'

language-plutus-core/generators/Language/PlutusCore/Generators/Interesting.hs

@@ -45,13 +45,13 @@ import qualified Hedgehog.Gen                             as Gen
 import qualified Hedgehog.Range                           as Range
 
 -- | The type of terms-and-their-values generators.
-type TermGen uni a = Gen (TermOf uni a)
+type TermGen uni a = Gen (TermOf (Term TyName Name uni ()) a)
 
 -- | Generates application of a builtin that returns a function, immediately saturated afterwards.
 --
 -- > ifThenElse {integer -> integer -> integer} (lessThanInteger i j) addInteger subtractInteger i j
 -- >     == if i < j then i + j else i - j
-genOverapplication :: Generatable uni => TermGen uni Integer
+genOverapplication :: Generatable (Term TyName Name uni ()) => TermGen uni Integer
 genOverapplication = do
     let typedInteger = AsKnownType
         integer = toTypeAst typedInteger
@@ -142,7 +142,7 @@ genNaiveFib = do
 -- defined in terms of generic fix (see 'Fix') and return the result
 -- along with the original 'Integer'
 genNatRoundtrip
-    :: forall uni. Generatable uni => TermGen uni Integer
+    :: forall uni. Generatable (Term TyName Name uni ()) => TermGen uni Integer
 genNatRoundtrip = do
     let typedInt = AsKnownType @uni
     TermOf _ iv <- Gen.filter ((>= 0) . _termOfValue) $ genTypedBuiltinDef typedInt
@@ -170,7 +170,7 @@ natSum = runQuote $ do
 
 -- | Generate a list of 'Integer's, turn it into a Scott-encoded PLC @List@ (see 'List'),
 -- sum elements of the list (see 'Sum') and return it along with the sum of the original list.
-genListSum :: Generatable uni => TermGen uni Integer
+genListSum :: Generatable (Term TyName Name uni ()) => TermGen uni Integer
 genListSum = do
     let typedInt = AsKnownType
         intS = toTypeAst typedInt
@@ -182,7 +182,7 @@ genListSum = do
 
 -- | Generate a @boolean@ and two @integer@s and check whether @if b then i1 else i2@
 -- means the same thing in Haskell and PLC. Terms are generated using 'genTermLoose'.
-genIfIntegers :: Generatable uni => TermGen uni Integer
+genIfIntegers :: Generatable (Term TyName Name uni ()) => TermGen uni Integer
 genIfIntegers = do
     let typedInt = AsKnownType
         int = toTypeAst typedInt
@@ -198,7 +198,7 @@ genIfIntegers = do
     return $ TermOf term value
 
 -- | Check that builtins can be partially applied.
-genApplyAdd1 :: Generatable uni => TermGen uni Integer
+genApplyAdd1 :: Generatable (Term TyName Name uni ()) => TermGen uni Integer
 genApplyAdd1 = do
     let typedInt = AsKnownType
         int = toTypeAst typedInt
@@ -212,7 +212,7 @@ genApplyAdd1 = do
     return . TermOf term $ iv + jv
 
 -- | Check that builtins can be partially applied.
-genApplyAdd2 :: Generatable uni => TermGen uni Integer
+genApplyAdd2 :: Generatable (Term TyName Name uni ()) => TermGen uni Integer
 genApplyAdd2 = do
     let typedInt = AsKnownType
         int = toTypeAst typedInt
@@ -227,15 +227,17 @@ genApplyAdd2 = do
     return . TermOf term $ iv + jv
 
 -- | Check that division by zero results in 'Error'.
-genDivideByZero :: Generatable uni => TermGen uni (EvaluationResult Integer)
+genDivideByZero :: Generatable (Term TyName Name uni ()) => TermGen uni (EvaluationResult Integer)
 genDivideByZero = do
     op <- Gen.element [DivideInteger, QuotientInteger, ModInteger, RemainderInteger]
     TermOf i _ <- genTermLoose $ AsKnownType @_ @Integer
     let term = mkIterApp () (builtinNameAsTerm op) [i, mkConstant @Integer () 0]
     return $ TermOf term EvaluationFailure
 
 -- | Check that division by zero results in 'Error' even if a function doesn't use that argument.
-genDivideByZeroDrop :: Generatable uni => TermGen uni (EvaluationResult Integer)
+genDivideByZeroDrop
+    :: Generatable (Term TyName Name uni ())
+    => TermGen uni (EvaluationResult Integer)
 genDivideByZeroDrop = do
     op <- Gen.element [DivideInteger, QuotientInteger, ModInteger, RemainderInteger]
     let typedInt = AsKnownType
@@ -250,7 +252,7 @@ genDivideByZeroDrop = do
 
 -- | Apply a function to all interesting generators and collect the results.
 fromInterestingTermGens
-    :: Generatable uni
+    :: Generatable (Term TyName Name uni ())
     => (forall a. KnownType (Term TyName Name uni ()) a => String -> TermGen uni a -> c) -> [c]
 fromInterestingTermGens f =
     [ f "overapplication"  genOverapplication

language-plutus-core/generators/Language/PlutusCore/Generators/Internal/Denotation.hs

@@ -56,7 +56,8 @@ data DenotationContextMember uni res =
 --   2. a bound variable of functional type with the result being @integer@
 --   3. the 'AddInteger' 'BuiltinName' or any other 'BuiltinName' which returns an @integer@.
 newtype DenotationContext uni = DenotationContext
-    { unDenotationContext :: DMap (AsKnownType uni) (Compose [] (DenotationContextMember uni))
+    { unDenotationContext ::
+        DMap (AsKnownType (Term TyName Name uni ())) (Compose [] (DenotationContextMember uni))
     }
 
 -- Here the only search that we need to perform is the search for things that return an appropriate
@@ -65,7 +66,9 @@ newtype DenotationContext uni = DenotationContext
 -- (without @Void@).
 
 -- | The resulting type of a 'TypeScheme'.
-typeSchemeResult :: TypeScheme (Term TyName Name uni ()) args res -> AsKnownType uni res
+typeSchemeResult
+    :: TypeScheme (Term TyName Name uni ()) args res
+    -> AsKnownType (Term TyName Name uni ()) res
 typeSchemeResult (TypeSchemeResult _)       = AsKnownType
 typeSchemeResult (TypeSchemeArrow _ schB)   = typeSchemeResult schB
 typeSchemeResult (TypeSchemeAllType _ schK) = typeSchemeResult $ schK Proxy

language-plutus-core/generators/Language/PlutusCore/Generators/Internal/Dependent.hs

@@ -4,8 +4,9 @@
 
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
-{-# LANGUAGE GADTs            #-}
-{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE TypeApplications     #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module Language.PlutusCore.Generators.Internal.Dependent
     ( AsKnownType (..)
@@ -16,7 +17,6 @@ import           PlutusPrelude
 
 import           Language.PlutusCore.Constant
 import           Language.PlutusCore.Core
-import           Language.PlutusCore.Name
 import           Language.PlutusCore.Universe
 
 import           Data.GADT.Compare
@@ -28,13 +28,13 @@ liftOrdering EQ = error "'liftOrdering': 'Eq'"
 liftOrdering GT = GGT
 
 -- | Contains a proof that @a@ is a 'KnownType'.
-data AsKnownType uni a where
-    AsKnownType :: KnownType (Term TyName Name uni ()) a => AsKnownType uni a
+data AsKnownType term a where
+    AsKnownType :: KnownType term a => AsKnownType term a
 
-instance GShow uni => Pretty (AsKnownType uni a) where
-    pretty a@AsKnownType = pretty $ toTypeAst @uni a
+instance GShow (UniOf term) => Pretty (AsKnownType term a) where
+    pretty a@AsKnownType = pretty $ toTypeAst @(UniOf term) a
 
-instance GShow uni => GEq (AsKnownType uni) where
+instance GShow (UniOf term) => GEq (AsKnownType term) where
     a `geq` b = do
         -- TODO: there is a HUGE problem here. @EvaluationResult a@ and @a@ have the same string
         -- representation currently, so we need to either fix that or come up with a more sensible
@@ -45,11 +45,11 @@ instance GShow uni => GEq (AsKnownType uni) where
         guard $ display @String a == display b
         Just $ unsafeCoerce Refl
 
-instance GShow uni => GCompare (AsKnownType uni) where
+instance GShow (UniOf term) => GCompare (AsKnownType term) where
     a `gcompare` b
         | Just Refl <- a `geq` b = GEQ
         | otherwise              = liftOrdering $ display @String a `compare` display b
 
 -- | Turn any @proxy a@ into an @AsKnownType a@ provided @a@ is a 'KnownType'.
-proxyAsKnownType :: KnownType (Term TyName Name uni ()) a => proxy a -> AsKnownType uni a
+proxyAsKnownType :: KnownType term a => proxy a -> AsKnownType term a
 proxyAsKnownType _ = AsKnownType

language-plutus-core/generators/Language/PlutusCore/Generators/Internal/Entity.hs

@@ -53,8 +53,9 @@ import qualified Hedgehog.Gen                                            as Gen
 
 -- | Generators of built-ins supplied to computations that run in the 'PlcGenT' monad.
 newtype BuiltinGensT uni m = BuiltinGensT
-    { _builtinGensTyped :: TypedBuiltinGenT uni m  -- ^ Generates a PLC 'Term' and the corresponding
-                                                   -- Haskell value out of a 'TypedBuiltin'.
+    { _builtinGensTyped :: TypedBuiltinGenT (Plain Term uni) m
+      -- ^ Generates a PLC 'Term' and the corresponding
+      -- Haskell value out of a 'TypedBuiltin'.
     }
 
 -- | The type used in generators defined in this module.
@@ -67,12 +68,12 @@ type PlcGenT uni m = GenT (ReaderT (BuiltinGensT uni m) m)
 
 -- | One iterated application of a @head@ to @arg@s represented in three distinct ways.
 data IterAppValue uni head arg r = IterAppValue
-    { _iterTerm :: Term TyName Name uni ()  -- ^ As a PLC 'Term'.
-    , _iterApp  :: IterApp head arg         -- ^ As an 'IterApp'.
-    , _iterTbv  :: r                        -- ^ As a Haskell value.
+    { _iterTerm :: EvaluationResult (Plain Term uni)    -- ^ As a PLC 'Term'.
+    , _iterApp  :: IterApp head (EvaluationResult arg)  -- ^ As an 'IterApp'.
+    , _iterTbv  :: r                                    -- ^ As a Haskell value.
     }
 
-instance ( PrettyBy config (Term TyName Name uni ())
+instance ( PrettyBy config (Plain Term uni)
          , PrettyBy config head, PrettyBy config arg, PrettyConst r
          ) => PrettyBy config (IterAppValue uni head arg r) where
     prettyBy config (IterAppValue term pia y) = parens $ fold
@@ -83,11 +84,11 @@ instance ( PrettyBy config (Term TyName Name uni ())
         ]
 
 -- | Run a 'PlcGenT' computation by supplying built-ins generators.
-runPlcT :: Monad m => TypedBuiltinGenT uni m -> PlcGenT uni m a -> GenT m a
+runPlcT :: Monad m => TypedBuiltinGenT (Plain Term uni) m -> PlcGenT uni m a -> GenT m a
 runPlcT genTb = hoistSupply $ BuiltinGensT genTb
 
 -- | Get a 'TermOf' out of an 'IterAppValue'.
-iterAppValueToTermOf :: IterAppValue uni head arg r -> TermOf uni r
+iterAppValueToTermOf :: IterAppValue uni head arg r -> TermOf (Plain Term uni) r
 iterAppValueToTermOf (IterAppValue term _ y) = TermOf term y
 
 -- | Add to the 'ByteString' representation of a 'Name' its 'Unique'
@@ -109,9 +110,13 @@ withTypedBuiltinGen k = Gen.choice
 -- | Generate a 'Term' along with the value it computes to,
 -- having a generator of terms of built-in types.
 withCheckedTermGen
-    :: (Generatable uni, Monad m, Closed uni, uni `EverywhereAll` [Eq, PrettyConst, ExMemoryUsage])
-    => TypedBuiltinGenT uni m
-    -> (forall a. AsKnownType uni a -> TermOf uni (EvaluationResult (Term TyName Name uni ())) -> GenT m c)
+    :: ( Generatable (Plain Term uni), Monad m
+       , Closed uni, uni `EverywhereAll` [Eq, PrettyConst, ExMemoryUsage]
+       )
+    => TypedBuiltinGenT (Plain Term uni) m
+    -> (forall a. AsKnownType (Plain Term uni) a ->
+            TermOf (Plain Term uni) (EvaluationResult (Plain Term uni)) ->
+                GenT m c)
     -> GenT m c
 withCheckedTermGen genTb k =
     withTypedBuiltinGen $ \akt@AsKnownType -> do
@@ -128,23 +133,23 @@ withCheckedTermGen genTb k =
 genIterAppValue
     :: forall head uni res m. Monad m
     => Denotation uni head res
-    -> PlcGenT uni m (IterAppValue uni head (Term TyName Name uni ()) res)
+    -> PlcGenT uni m (IterAppValue uni head (Plain Term uni) res)
 genIterAppValue (Denotation object embed meta scheme) = result where
-    result = go scheme (embed object) id meta
+    result = go scheme (EvaluationSuccess $ embed object) id meta
 
     go
         :: TypeScheme (Plain Term uni) args res
-        -> Term TyName Name uni ()
-        -> ([Term TyName Name uni ()] -> [Term TyName Name uni ()])
+        -> EvaluationResult (Plain Term uni)
+        -> ([EvaluationResult (Plain Term uni)] -> [EvaluationResult (Plain Term uni)])
         -> FoldArgs args res
-        -> PlcGenT uni m (IterAppValue uni head (Term TyName Name uni ()) res)
+        -> PlcGenT uni m (IterAppValue uni head (Plain Term uni) res)
     go (TypeSchemeResult _)       term args y = do  -- Computed the result.
         let pia = IterApp object $ args []
         return $ IterAppValue term pia y
     go (TypeSchemeArrow _ schB)   term args f = do  -- Another argument is required.
         BuiltinGensT genTb <- ask
         TermOf v x <- liftT $ genTb AsKnownType  -- Get a Haskell and the correspoding PLC values.
-        let term' = Apply () term v              -- Apply the term to the PLC value.
+        let term' = Apply () <$> term <*> v      -- Apply the term to the PLC value.
             args' = args . (v :)                 -- Append the PLC value to the spine.
             y     = f x                          -- Apply the Haskell function to the generated argument.
         go schB term' args' y
@@ -156,14 +161,21 @@ genIterAppValue (Denotation object embed meta scheme) = result where
 -- Arguments to functions and 'BuiltinName's are generated recursively.
 genTerm
     :: forall uni m.
-       (Generatable uni, Monad m)
-    => TypedBuiltinGenT uni m      -- ^ Ground generators of built-ins. The base case of the recursion.
-    -> DenotationContext uni       -- ^ A context to generate terms in. See for example 'typedBuiltinNames'.
-                                   -- Gets extended by a variable when an applied lambda is generated.
-    -> Int                         -- ^ Depth of recursion.
-    -> TypedBuiltinGenT uni m
+       (Generatable (Plain Term uni), Monad m)
+    => TypedBuiltinGenT (Plain Term uni) m
+       -- ^ Ground generators of built-ins. The base case of the recursion.
+    -> DenotationContext uni
+       -- ^ A context to generate terms in. See for example 'typedBuiltinNames'.
+       -- Gets extended by a variable when an applied lambda is generated.
+    -> Int
+       -- ^ Depth of recursion.
+    -> TypedBuiltinGenT (Plain Term uni) m
 genTerm genBase context0 depth0 = Morph.hoist runQuoteT . go context0 depth0 where
-    go :: DenotationContext uni -> Int -> AsKnownType uni r -> GenT (QuoteT m) (TermOf uni r)
+    go
+        :: DenotationContext uni
+        -> Int
+        -> AsKnownType (Plain Term uni) r
+        -> GenT (QuoteT m) (TermOf (Plain Term uni) r)
     go context depth akt
         -- FIXME: should be using 'variables' but this is now the same as 'recursive'
         | depth == 0 = choiceDef (liftT $ genBase akt) []
@@ -193,23 +205,24 @@ genTerm genBase context0 depth0 = Morph.hoist runQuoteT . go context0 depth0 whe
                 -- Get the 'Type' of the argument from a generated 'TypedBuiltin'.
                 let argTy = toTypeAst argKt
                 -- Generate the argument.
-                TermOf arg  x <- go context (depth - 1) argKt
+                TermOf getArg  x <- go context (depth - 1) argKt
                 -- Generate the body of the lambda abstraction adding the new variable to the context.
-                TermOf body y <- go (insertVariable name x context) (depth - 1) akt
+                TermOf getBody y <- go (insertVariable name x context) (depth - 1) akt
                 -- Assemble the term.
-                let term = Apply () (LamAbs () name argTy body) arg
+                let term = Apply () . LamAbs () name argTy <$> getBody <*> getArg
                 return $ TermOf term 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
-     :: (Generatable uni, Monad m)
-     => TypedBuiltinGenT uni m
+     :: (Generatable (Plain Term uni), Monad m)
+     => TypedBuiltinGenT (Plain Term uni) m
 genTermLoose = genTerm genTypedBuiltinDef typedBuiltinNames 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
-     :: (Generatable uni, Monad m)
-     => (forall a. KnownType (Plain Term uni) a => TermOf uni a -> GenT m c) -> GenT m c
+     :: (Generatable (Plain Term uni), Monad m)
+     => (forall a. KnownType (Plain Term uni) a => TermOf (Plain Term uni) a -> GenT m c)
+     -> GenT m c
 withAnyTermLoose k = withTypedBuiltinGen $ \akt@AsKnownType -> genTermLoose akt >>= k