From febabc4e20f7b57b9ceda576f2b1268966712ff6 Mon Sep 17 00:00:00 2001 From: effectfully Date: Fri, 16 Dec 2022 17:50:20 +0100 Subject: [PATCH] [PIR] [Test] Add term generators (#4949) --- plutus-core/plutus-core.cabal | 15 +- .../src/PlutusCore/Builtin/KnownKind.hs | 21 +- plutus-core/plutus-core/src/Universe/Core.hs | 1 + plutus-core/plutus-ir/test/GeneratorSpec.hs | 36 +- .../plutus-ir/test/GeneratorSpec/Terms.hs | 182 +++++++ .../plutus-ir/test/GeneratorSpec/Types.hs | 2 +- .../Generators/QuickCheck/Builtin.hs | 135 ++++- .../PlutusCore/Generators/QuickCheck/GenTm.hs | 28 +- .../Generators/QuickCheck/ShrinkTypes.hs | 42 +- .../testlib/PlutusIR/Generators/QuickCheck.hs | 5 + .../PlutusIR/Generators/QuickCheck/Common.hs | 110 ++++ .../Generators/QuickCheck/GenerateTerms.hs | 476 ++++++++++++++++++ .../Generators/QuickCheck/ShrinkTerms.hs | 366 ++++++++++++++ 13 files changed, 1358 insertions(+), 61 deletions(-) create mode 100644 plutus-core/plutus-ir/test/GeneratorSpec/Terms.hs create mode 100644 plutus-core/testlib/PlutusIR/Generators/QuickCheck.hs create mode 100644 plutus-core/testlib/PlutusIR/Generators/QuickCheck/Common.hs create mode 100644 plutus-core/testlib/PlutusIR/Generators/QuickCheck/GenerateTerms.hs create mode 100644 plutus-core/testlib/PlutusIR/Generators/QuickCheck/ShrinkTerms.hs diff --git a/plutus-core/plutus-core.cabal b/plutus-core/plutus-core.cabal index 3612bf7e110..2e2fcc60550 100644 --- a/plutus-core/plutus-core.cabal +++ b/plutus-core/plutus-core.cabal @@ -367,6 +367,10 @@ library plutus-core-testlib PlutusCore.Generators.QuickCheck.Utils PlutusCore.Test PlutusIR.Generators.AST + PlutusIR.Generators.QuickCheck + PlutusIR.Generators.QuickCheck.Common + PlutusIR.Generators.QuickCheck.GenerateTerms + PlutusIR.Generators.QuickCheck.ShrinkTerms PlutusIR.Test Test.Tasty.Extras @@ -375,6 +379,7 @@ library plutus-core-testlib , bifunctors , bytestring , containers + , data-default-class , dependent-map >=0.4.0.0 , filepath , hedgehog >=1.0 @@ -467,6 +472,7 @@ test-suite plutus-ir-test GeneratorSpec GeneratorSpec.Builtin GeneratorSpec.Substitution + GeneratorSpec.Terms GeneratorSpec.Types NamesSpec ParserSpec @@ -474,20 +480,23 @@ test-suite plutus-ir-test TypeSpec build-depends: - , base >=4.9 && <5 + , base >=4.9 && <5 , containers , flat + , hashable , hedgehog , lens , megaparsec - , plutus-core ^>=1.1 - , plutus-core-testlib ^>=1.1 + , mtl + , plutus-core ^>=1.1 + , plutus-core-testlib ^>=1.1 , QuickCheck , serialise , tasty , tasty-hedgehog , tasty-quickcheck , text + , unordered-containers test-suite untyped-plutus-core-test import: lang diff --git a/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownKind.hs b/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownKind.hs index d01048dcbd0..e6d6cdba803 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownKind.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Builtin/KnownKind.hs @@ -23,6 +23,14 @@ data SingKind k where SingType :: SingKind GHC.Type SingKindArrow :: SingKind k -> SingKind l -> SingKind (k -> l) +-- | Feed the 'SingKind' version of the given 'Kind' to the given continuation. +withSingKind :: Kind ann -> (forall k. SingKind k -> r) -> r +withSingKind (Type _) k = k SingType +withSingKind (KindArrow _ dom cod) k = + withSingKind dom $ \domS -> + withSingKind cod $ \codS -> + k $ SingKindArrow domS codS + -- | For reifying Haskell kinds representing Plutus kinds at the term level. class KnownKind k where knownKind :: SingKind k @@ -34,12 +42,15 @@ instance rep ~ LiftedRep => KnownKind (TYPE rep) where instance (KnownKind dom, KnownKind cod) => KnownKind (dom -> cod) where knownKind = SingKindArrow (knownKind @dom) (knownKind @cod) +-- | Satisfy the 'KnownKind' constraint of a continuation using the given 'SingKind'. +bringKnownKind :: SingKind k -> (KnownKind k => r) -> r +bringKnownKind SingType r = r +bringKnownKind (SingKindArrow dom cod) r = bringKnownKind dom $ bringKnownKind cod r + withKnownKind :: Kind ann -> (forall k. KnownKind k => Proxy k -> r) -> r -withKnownKind (Type _) k = k $ Proxy @GHC.Type -withKnownKind (KindArrow _ dom cod) k = - withKnownKind dom $ \(_ :: Proxy dom) -> - withKnownKind cod $ \(_ :: Proxy cod) -> - k $ Proxy @(dom -> cod) +withKnownKind kind k = + withSingKind kind $ \(kindS :: SingKind kind) -> + bringKnownKind kindS $ k $ Proxy @kind -- We need this for type checking Plutus, however we get Plutus types/terms/programs by either -- producing them directly or by parsing/decoding them and in both the cases we have access to the diff --git a/plutus-core/plutus-core/src/Universe/Core.hs b/plutus-core/plutus-core/src/Universe/Core.hs index c02e3e9bc2e..d46a73e2e0d 100644 --- a/plutus-core/plutus-core/src/Universe/Core.hs +++ b/plutus-core/plutus-core/src/Universe/Core.hs @@ -44,6 +44,7 @@ module Universe.Core , GShow (..) , gshow , GEq (..) + , defaultEq , deriveGEq , deriveGCompare , (:~:)(..) diff --git a/plutus-core/plutus-ir/test/GeneratorSpec.hs b/plutus-core/plutus-ir/test/GeneratorSpec.hs index 2a262661ea4..a4241700062 100644 --- a/plutus-core/plutus-ir/test/GeneratorSpec.hs +++ b/plutus-core/plutus-ir/test/GeneratorSpec.hs @@ -3,6 +3,7 @@ module GeneratorSpec where import GeneratorSpec.Builtin import GeneratorSpec.Substitution +import GeneratorSpec.Terms import GeneratorSpec.Types import Test.QuickCheck @@ -14,9 +15,34 @@ import Test.Tasty.QuickCheck -- The default for the argument is @1@. generators :: Int -> TestNested generators factor = return $ testGroup "generators" - [ testProperty "prop_genData" $ withMaxSuccess (factor*10000) prop_genData - , testProperty "prop_genKindCorrect" $ withMaxSuccess (factor*100000) (prop_genKindCorrect False) - , testProperty "prop_shrinkTypeSound" $ withMaxSuccess (factor*100000) prop_shrinkTypeSound - , testProperty "prop_substType" $ withMaxSuccess (factor*10000) prop_substType - , testProperty "prop_unify" $ withMaxSuccess (factor*10000) prop_unify + [ testProperty "prop_genData" $ + withMaxSuccess (factor*3000) prop_genData + + , testProperty "prop_genKindCorrect" $ + withMaxSuccess (factor*100000) (prop_genKindCorrect False) + , testProperty "prop_shrinkTypeSound" $ + withMaxSuccess (factor*30000) prop_shrinkTypeSound + + , testProperty "prop_substType" $ + withMaxSuccess (factor*10000) prop_substType + , testProperty "prop_unify" $ + withMaxSuccess (factor*10000) prop_unify + + , testProperty "prop_genTypeCorrect" $ + withMaxSuccess (factor*10000) (prop_genTypeCorrect False) + , testProperty "prop_genWellTypedFullyApplied" $ + withMaxSuccess (factor*1000) prop_genWellTypedFullyApplied + , testProperty "prop_findInstantiation" $ + withMaxSuccess (factor*10000) prop_findInstantiation + , testProperty "prop_inhabited" $ + withMaxSuccess (factor*3000) prop_inhabited +-- These tests sometimes take a long time to run due to +-- a large number of shrinks being generated. +-- See https://github.com/input-output-hk/plutus/pull/4949#discussion_r1029985014 +-- , testProperty "prop_stats_numShrink" $ +-- withMaxSuccess (factor*40) prop_stats_numShrink +-- , testProperty "prop_noTermShrinkLoops" $ +-- withMaxSuccess (factor*40) prop_noTermShrinkLoops +-- , testProperty "prop_shrinkTermSound" $ +-- withMaxSuccess (factor*40) prop_shrinkTermSound ] diff --git a/plutus-core/plutus-ir/test/GeneratorSpec/Terms.hs b/plutus-core/plutus-ir/test/GeneratorSpec/Terms.hs new file mode 100644 index 00000000000..10a2d7aca3b --- /dev/null +++ b/plutus-core/plutus-ir/test/GeneratorSpec/Terms.hs @@ -0,0 +1,182 @@ +-- editorconfig-checker-disable-file +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TupleSections #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module GeneratorSpec.Terms where + +import PlutusCore.Generators.QuickCheck +import PlutusIR.Generators.QuickCheck + +import PlutusCore.Default +import PlutusCore.Name +import PlutusCore.Quote +import PlutusCore.Rename +import PlutusIR +import PlutusIR.Core.Instance.Pretty.Readable + +import Control.Monad.Reader +import Data.Char +import Data.Either +import Data.Function +import Data.Hashable +import Data.HashMap.Strict qualified as HashMap +import Data.List.NonEmpty (NonEmpty (..)) +import Data.Map.Strict qualified as Map +import Test.QuickCheck + +-- | 'rename' a 'Term' and 'show' it afterwards. +showRenameTerm :: Term TyName Name DefaultUni DefaultFun () -> String +showRenameTerm = show . runQuote . rename + +-- | Same as 'nub', but relies on 'Hashable' and is therefore asymptotically faster. +nubHashableOn :: Hashable b => (a -> b) -> [a] -> [a] +nubHashableOn f = HashMap.elems . HashMap.fromList . map (\x -> (f x, x)) + +-- We need this for checking the behavior of the shrinker (in particular, whether a term shrinks +-- to itself, which would be a bug, or how often a term shrinks to the same thing multiple times +-- within a single step). Should we move this to @plutus-ir@ itself? Not sure, but it's safe to +-- place it here, since nothing can depend on a test suite (apart from modules from within this test +-- suite), hence no conflicting orphans can occur. +instance Eq (Term TyName Name DefaultUni DefaultFun ()) where + -- Quick-and-dirty implementation in terms of 'Show'. + -- We generally consider equality modulo alpha, hence the call to 'rename'. + (==) = (==) `on` showRenameTerm + +-- * Core properties for PIR generators + +-- | Test that our generators only result in well-typed terms. +-- Note, the counterexamples from this property are not shrunk (see why below). +-- See Note [Debugging generators that don't generate well-typed/kinded terms/types] +-- and the utility properties below when this property fails. +prop_genTypeCorrect :: Bool -> Property +prop_genTypeCorrect debug = do + -- Note, we don't shrink this term here because a precondition of shrinking is that + -- the term we are shrinking is well-typed. If it is not, the counterexample we get + -- from shrinking will be nonsene. + let gen = if debug then genTypeAndTermDebug_ else genTypeAndTerm_ + forAllDoc "ty,tm" gen (const []) $ \ (ty, tm) -> typeCheckTerm tm ty + +-- | Test that when we generate a fully applied term we end up +-- with a well-typed term. +prop_genWellTypedFullyApplied :: Property +prop_genWellTypedFullyApplied = + forAllDoc "ty, tm" genTypeAndTerm_ shrinkClosedTypedTerm $ \ (ty, tm) -> + -- No shrinking here because if `genFullyApplied` is wrong then the shrinking + -- will be wrong too. See `prop_genTypeCorrect`. + forAllDoc "ty', tm'" (genFullyApplied ty tm) (const []) $ \ (ty', tm') -> + typeCheckTerm tm' ty' + +-- | Test that shrinking a well-typed term results in a well-typed term +prop_shrinkTermSound :: Property +prop_shrinkTermSound = + forAllDoc "ty,tm" genTypeAndTerm_ shrinkClosedTypedTerm $ \ (ty, tm) -> + let shrinks = shrinkClosedTypedTerm (ty, tm) in + -- While we generate well-typed terms we still need this check here for + -- shrinking counterexamples to *this* property. If we find a term whose + -- shrinks aren't well-typed we want to find smaller *well-typed* terms + -- whose shrinks aren't well typed. + -- Importantly, this property is only interesting when + -- shrinking itself is broken, so we can only use the + -- parts of shrinking that happen to be OK. + isRight (typeCheckTerm tm ty) ==> + -- We don't want to let the shrinker get away with being empty, so we ignore empty + -- shrinks. QuickCheck will give up and print an error if the shrinker returns the empty list too + -- often. + not (null shrinks) ==> + assertNoCounterexamples $ lefts + [ ((ty', tm'), ) <$> typeCheckTerm tm' ty' + | (ty', tm') <- shrinks + ] + +-- * Utility tests for debugging generators that behave weirdly + +-- | Test that `findInstantiation` results in a well-typed instantiation. +prop_findInstantiation :: Property +prop_findInstantiation = + forAllDoc "ctx" genCtx (const []) $ \ ctx0 -> + forAllDoc "ty" (genTypeWithCtx ctx0 $ Type ()) (shrinkType ctx0) $ \ ty0 -> + forAllDoc "target" (genTypeWithCtx ctx0 $ Type ()) (shrinkType ctx0) $ \ target -> + assertNoCounterexamples $ lefts + [ (n ,) <$> checkInst ctx0 x0 ty0 insts target + | n <- [0 .. arity ty0 + 3] + , Right insts <- [findInstantiation ctx0 n target ty0] + ] + where + x0 = Name "x" (toEnum 0) + arity (TyForall _ _ _ a) = arity a + arity (TyFun _ _ b) = 1 + arity b + arity _ = 0 + + -- Check that building a "minimal" term that performs the instantiations in + -- `insts` produces a well-typed term. + checkInst ctx1 x1 ty1 insts1 target = typeCheckTermInContext ctx1 tmCtx1 tm1 target + where + -- Build a term and a context from `insts` that consists of + -- `tm @ty` for every `InstApp ty` in `insts` and `tm y` for + -- a fresh variable `y : ty` for every `InstArg ty` in `insts`. + (tmCtx1, tm1) = go (toEnum 1) (Map.singleton x1 ty1) (Var () x1) insts1 + go _ tmCtx tm [] = (tmCtx, tm) + go i tmCtx tm (InstApp ty : insts) = go i tmCtx (TyInst () tm ty) insts + go i tmCtx tm (InstArg ty : insts) = go (succ i) (Map.insert y ty tmCtx) + (Apply () tm (Var () y)) insts + where y = Name "y" i + +-- | Check what's in the leaves of the generated data +prop_stats_leaves :: Property +prop_stats_leaves = + -- No shrinking here because we are only collecting stats + forAllDoc "_,tm" genTypeAndTerm_ (const []) $ \ (_, tm) -> + tabulate "leaves" (map (filter isAlpha . show . prettyPirReadable) $ leaves tm) $ property True + where + -- Figure out what's at the leaves of the AST, + -- including variable names, error, and builtins. + leaves (Var _ x) = [x] + leaves (TyInst _ a _) = leaves a + leaves (Let _ _ _ b) = leaves b + leaves (LamAbs _ _ _ b) = leaves b + leaves (Apply _ a b) = leaves a ++ leaves b + leaves Error{} = [Name "error" $ toEnum 0] + leaves Builtin{} = [Name "builtin" $ toEnum 0] + leaves _ = [] + +-- | Check the ratio of duplicate shrinks +prop_stats_numShrink :: Property +prop_stats_numShrink = + -- No shrinking here because we are only collecting stats + forAllDoc "ty,tm" genTypeAndTerm_ (const []) $ \ (ty, tm) -> + let shrinks = map snd $ shrinkClosedTypedTerm (ty, tm) + n = length shrinks + u = length $ nubHashableOn showRenameTerm shrinks + r | n > 0 = 5 * ((n - u) * 20 `div` n) + | otherwise = 0 + in tabulate "distribution | duplicates" [" | " ++ show r ++ "%"] True + +-- | Specific test that `inhabitType` returns well-typed things +prop_inhabited :: Property +prop_inhabited = + -- No shrinking here because if the generator + -- generates nonsense shrinking will be nonsense. + forAllDoc "ty,tm" (genInhab mempty) (const []) $ \ (ty, tm) -> typeCheckTerm tm ty + where + -- Generate some datatypes and then immediately call + -- `inhabitType` to test `inhabitType` directly instead + -- of through the whole term generator. Quick-ish way + -- of debugging "clever hacks" in `inhabitType`. + genInhab ctx = runGenTm $ local (\ e -> e { geTypes = ctx }) $ + genDatatypeLets $ \ dats -> do + ty <- genType $ Type () + tm <- inhabitType ty + return (ty, foldr (\ dat -> Let () NonRec (DatatypeBind () dat :| [])) tm dats) + +-- | Check that there are no one-step shrink loops +prop_noTermShrinkLoops :: Property +prop_noTermShrinkLoops = + -- Note that we need to remove x from the shrinks of x here because + -- a counterexample to this property is otherwise guaranteed to + -- go into a shrink loop. + forAllDoc "ty,tm" genTypeAndTerm_ + (\(ty', tm') -> filter ((/= tm') . snd) $ shrinkClosedTypedTerm (ty', tm')) $ \(ty, tm) -> + tm `notElem` map snd (shrinkClosedTypedTerm (ty, tm)) diff --git a/plutus-core/plutus-ir/test/GeneratorSpec/Types.hs b/plutus-core/plutus-ir/test/GeneratorSpec/Types.hs index 4640cb2fd09..ed763fde259 100644 --- a/plutus-core/plutus-ir/test/GeneratorSpec/Types.hs +++ b/plutus-core/plutus-ir/test/GeneratorSpec/Types.hs @@ -27,7 +27,7 @@ prop_shrinkTypeSound = -- See discussion about the same trick in 'prop_shrinkTermSound'. isRight (checkKind ctx ty k) ==> assertNoCounterexamples $ lefts - [ (k', ty', ) <$> checkKind ctx ty k + [ (k', ty', ) <$> checkKind ctx ty' k' | (k', ty') <- shrinkKindAndType ctx (k, ty) ] diff --git a/plutus-core/testlib/PlutusCore/Generators/QuickCheck/Builtin.hs b/plutus-core/testlib/PlutusCore/Generators/QuickCheck/Builtin.hs index 1fbc8b1e457..89307194765 100644 --- a/plutus-core/testlib/PlutusCore/Generators/QuickCheck/Builtin.hs +++ b/plutus-core/testlib/PlutusCore/Generators/QuickCheck/Builtin.hs @@ -15,9 +15,9 @@ import PlutusCore.Generators.QuickCheck.Common (genList) import Data.ByteString (ByteString) import Data.Coerce -import Data.Functor import Data.Int import Data.Kind qualified as GHC +import Data.Maybe import Data.Proxy import Data.Text (Text) import Data.Text qualified as Text @@ -25,6 +25,7 @@ import Data.Text.Encoding qualified as Text import Data.Word import Test.QuickCheck import Test.QuickCheck.Instances.ByteString () +import Universe instance Arbitrary Data where arbitrary = sized genData @@ -100,6 +101,10 @@ instance ArbitraryBuiltin Integer where , (1, fromIntegral <$> arbitrary @Int64) ] +-- | +-- +-- >>> shrinkBuiltin $ Text.pack "abcd" +-- ["","cd","ab","bcd","acd","abd","abc","aacd","abad","abbd","abca","abcb","abcc"] instance ArbitraryBuiltin Text where arbitraryBuiltin = Text.pack . getPrintableString <$> arbitrary shrinkBuiltin = map (Text.pack . getPrintableString) . shrink . PrintableString . Text.unpack @@ -134,6 +139,17 @@ data MaybeSomeTypeOf k = NothingSomeType | forall (a :: k). JustSomeType (DefaultUni (Esc a)) +instance Eq (MaybeSomeTypeOf k) where + NothingSomeType == NothingSomeType = True + JustSomeType uni1 == JustSomeType uni2 = uni1 `defaultEq` uni2 + NothingSomeType == JustSomeType{} = False + JustSomeType{} == NothingSomeType = False + +-- | Forget the reflected at the type level kind. +eraseMaybeSomeTypeOf :: MaybeSomeTypeOf k -> Maybe (SomeTypeIn DefaultUni) +eraseMaybeSomeTypeOf NothingSomeType = Nothing +eraseMaybeSomeTypeOf (JustSomeType uni) = Just $ SomeTypeIn uni + -- | Generate a 'DefaultUniApply' if possible. genDefaultUniApply :: KnownKind k => Gen (MaybeSomeTypeOf k) genDefaultUniApply = do @@ -147,10 +163,53 @@ genDefaultUniApply = do -- (because the head of an application can't be of the same kind as the whole application). -- We don't have higher-kinded built-in types, so we don't do this kind of shrinking for any kinds -- other than *. -shrinkDefaultUniApplyStar :: DefaultUni (Esc b) -> [MaybeSomeTypeOf GHC.Type] -shrinkDefaultUniApplyStar (fun `DefaultUniApply` arg) = - [JustSomeType arg | SingType <- [toSingKind arg]] ++ shrinkDefaultUniApplyStar fun -shrinkDefaultUniApplyStar _ = [] +shrinkToStarArgs :: DefaultUni (Esc a) -> [MaybeSomeTypeOf GHC.Type] +shrinkToStarArgs = go [] where + go :: [MaybeSomeTypeOf GHC.Type] -> DefaultUni (Esc b) -> [MaybeSomeTypeOf GHC.Type] + go args (fun `DefaultUniApply` arg) = + go ([JustSomeType arg | SingType <- [toSingKind arg]] ++ args) fun + go args _ = args + +-- | Shrink a built-in type while preserving its kind. +shrinkDropBuiltinSameKind :: DefaultUni (Esc (a :: k)) -> [MaybeSomeTypeOf k] +shrinkDropBuiltinSameKind uni = + case toSingKind uni of + SingType -> case uni of + -- 'DefaultUniUnit' is the "minimal" built-in type, can't shrink it any further. + DefaultUniUnit -> [] + -- Any other built-in type of kind @*@ shrinks to 'DefaultUniUnit' and if it happens to + -- be a built-in type application, then also all suitable arguments of the + -- application that are not 'DefaultUniUnit'. + _ -> + let ju = JustSomeType DefaultUniUnit + in ju : filter (/= ju) (shrinkToStarArgs uni) + -- Any built-in type of kind @* -> *@ can be shrunk to @[] :: * -> *@ as long as the + -- built-in type is not @[]@ already. + -- If we had higher-kinded built-in types, we'd need 'shrinkToStarToStarArgs' here like with + -- 'shrinkToStarArgs' above, so the current approach would need some generalization. But we + -- we don't have higher-kinded built-in types and are unlikely to introduce them, so we opt + -- for not complicating things here. + SingType `SingKindArrow` SingType -> case uni of + DefaultUniProtoList -> [] + _ -> [JustSomeType DefaultUniProtoList] + _ -> [] + +-- | Shrink a function application by shrinking either the function or the argument. +-- The kind is preserved. +shrinkDefaultUniApply :: DefaultUni (Esc (a :: k)) -> [MaybeSomeTypeOf k] +shrinkDefaultUniApply (fun `DefaultUniApply` arg) = concat + [ [ JustSomeType $ fun' `DefaultUniApply` arg + | JustSomeType fun' <- shrinkBuiltinSameKind fun + ] + , [ JustSomeType $ fun `DefaultUniApply` arg' + | JustSomeType arg' <- shrinkBuiltinSameKind arg + ] + ] +shrinkDefaultUniApply _ = [] + +-- | Kind-preserving shrinking for 'DefaultUni'. +shrinkBuiltinSameKind :: DefaultUni (Esc (a :: k)) -> [MaybeSomeTypeOf k] +shrinkBuiltinSameKind uni = shrinkDropBuiltinSameKind uni ++ shrinkDefaultUniApply uni {- Note [Kind-driven generation of built-in types] The @Arbitrary (MaybeSomeTypeOf k)@ instance is responsible for generating built-in types. @@ -189,25 +248,59 @@ instance KnownKind k => Arbitrary (MaybeSomeTypeOf k) where [pure $ JustSomeType DefaultUniProtoPair] _ -> [pure NothingSomeType] - -- No shrinks if you don't have anything to shrink. - shrink NothingSomeType = [] - shrink (JustSomeType uni) = - case knownKind @k of - SingType -> case uni of - -- 'DefaultUniUnit' is the "minimal" built-in type, can't shrink it any further. - DefaultUniUnit -> [] - -- Any other built-in type of kind * shrinks to 'DefaultUniUnit' and if it happens to - -- be a built-in type application, then also all suitable arguments of the - -- application. - _ -> JustSomeType DefaultUniUnit : shrinkDefaultUniApplyStar uni - -- No suitable builtins to shrink to for non-* kinds. - _ -> [] + shrink NothingSomeType = [] -- No shrinks if you don't have anything to shrink. + shrink (JustSomeType uni) = shrinkBuiltinSameKind uni -- | Generate a built-in type of a given kind. genBuiltinTypeOf :: Kind () -> Gen (Maybe (SomeTypeIn DefaultUni)) genBuiltinTypeOf kind = -- See Note [Kind-driven generation of built-in types]. withKnownKind kind $ \(_ :: Proxy kind) -> - arbitrary @(MaybeSomeTypeOf kind) <&> \case - NothingSomeType -> Nothing - JustSomeType uni -> Just $ SomeTypeIn uni + eraseMaybeSomeTypeOf <$> arbitrary @(MaybeSomeTypeOf kind) + +-- | Shrink a built-in type by dropping a part of it or dropping the whole built-in type in favor of +-- a some minimal one (see 'shrinkDropBuiltinSameKind'). The kind is not preserved in the general +-- case. +shrinkDropBuiltin :: DefaultUni (Esc (a :: k)) -> [SomeTypeIn DefaultUni] +shrinkDropBuiltin uni = concat + [ case toSingKind uni of + SingType `SingKindArrow` _ -> shrinkDropBuiltin $ uni `DefaultUniApply` DefaultUniUnit + _ -> [] + , mapMaybe eraseMaybeSomeTypeOf $ shrinkDropBuiltinSameKind uni + ] + +-- TODO: have proper tests +-- >>> :set -XTypeApplications +-- >>> import PlutusCore.Pretty +-- >>> mapM_ (putStrLn . display) . shrinkBuiltinType $ someType @_ @[Bool] +-- unit +-- bool +-- (list unit) +-- >>> mapM_ (putStrLn . display) . shrinkBuiltinType $ someType @_ @(,) +-- unit +-- list +-- >>> mapM_ (putStrLn . display) . shrinkBuiltinType $ someType @_ @((,) Integer) +-- unit +-- integer +-- list +-- (pair unit) +-- >>> mapM_ (putStrLn . display) . shrinkBuiltinType $ someType @_ @((), Integer) +-- unit +-- integer +-- (list integer) +-- (pair unit unit) +-- >>> mapM_ (putStrLn . display) . shrinkBuiltinType $ someType @_ @([Bool], Integer) +-- unit +-- (list bool) +-- integer +-- (list integer) +-- (pair unit integer) +-- (pair bool integer) +-- (pair (list unit) integer) +-- (pair (list bool) unit) +-- | Non-kind-preserving shrinking for 'DefaultUni'. +shrinkBuiltinType :: SomeTypeIn DefaultUni -> [SomeTypeIn DefaultUni] +shrinkBuiltinType (SomeTypeIn uni) = concat + [ shrinkDropBuiltin uni + , mapMaybe eraseMaybeSomeTypeOf $ shrinkDefaultUniApply uni + ] diff --git a/plutus-core/testlib/PlutusCore/Generators/QuickCheck/GenTm.hs b/plutus-core/testlib/PlutusCore/Generators/QuickCheck/GenTm.hs index eb9a85f54c1..5bcba97a144 100644 --- a/plutus-core/testlib/PlutusCore/Generators/QuickCheck/GenTm.hs +++ b/plutus-core/testlib/PlutusCore/Generators/QuickCheck/GenTm.hs @@ -53,6 +53,8 @@ data GenEnv = GenEnv -- ^ Type context , geTerms :: Map Name (Type TyName DefaultUni ()) -- ^ Term context + , geUnboundUsedTyNames :: Set TyName + -- ^ Names that we have generated and don't want to shadow but haven't bound yet. , geEscaping :: AllowEscape -- ^ Are we in a place where we are allowed to generate a datatype binding? , geCustomGen :: Maybe (Type TyName DefaultUni ()) @@ -101,14 +103,15 @@ runGenTmCustom f cg g = do let env = GenEnv { -- Duplicating the QC size parameter that we use to control the size of constants as -- the initial AST size parameter. - geAstSize = n - , geDatas = Map.empty - , geTypes = Map.empty - , geTerms = Map.empty - , geEscaping = YesEscape - , geCustomGen = cg - , geCustomFreq = f - , geDebug = False + geAstSize = n + , geDatas = Map.empty + , geTypes = Map.empty + , geTerms = Map.empty + , geUnboundUsedTyNames = Set.empty + , geEscaping = YesEscape + , geCustomGen = cg + , geCustomFreq = f + , geDebug = False } flip runReader env <$> runGenT g @@ -208,8 +211,8 @@ Overall, this chaotic goodness needs to be sorted out. -- | Get all uniques we have generated and are used in the current context. getUniques :: GenTm (Set Unique) getUniques = do - GenEnv{geDatas = dts, geTypes = tys, geTerms = tms} <- ask - return $ Set.mapMonotonic (_nameUnique . unTyName) (Map.keysSet dts <> Map.keysSet tys) <> + GenEnv{geDatas = dts, geTypes = tys, geTerms = tms, geUnboundUsedTyNames = used} <- ask + return $ Set.mapMonotonic (_nameUnique . unTyName) (Map.keysSet dts <> Map.keysSet tys <> used) <> Set.mapMonotonic _nameUnique (Map.keysSet tms) <> Set.unions [ names d | d <- Map.elems dts ] where @@ -289,6 +292,11 @@ bindTyName x k = local $ \ e -> e bindTyNames :: [(TyName, Kind ())] -> GenTm a -> GenTm a bindTyNames = flip $ foldr (uncurry bindTyName) +-- | Remember that we have generated a type name locally but don't bind it. +-- Useful for non-recursive definitions where we want to control name overlap. +registerTyName :: TyName -> GenTm a -> GenTm a +registerTyName n = local $ \ e -> e { geUnboundUsedTyNames = Set.insert n (geUnboundUsedTyNames e) } + -- | Bind a term to a type in a generator. bindTmName :: Name -> Type TyName DefaultUni () -> GenTm a -> GenTm a bindTmName x ty = local $ \ e -> e { geTerms = Map.insert x ty (geTerms e) } diff --git a/plutus-core/testlib/PlutusCore/Generators/QuickCheck/ShrinkTypes.hs b/plutus-core/testlib/PlutusCore/Generators/QuickCheck/ShrinkTypes.hs index 7316790ae94..2a9ade79ca5 100644 --- a/plutus-core/testlib/PlutusCore/Generators/QuickCheck/ShrinkTypes.hs +++ b/plutus-core/testlib/PlutusCore/Generators/QuickCheck/ShrinkTypes.hs @@ -7,10 +7,12 @@ -- this module or reverse-engineer the shrinker and fix the problem. module PlutusCore.Generators.QuickCheck.ShrinkTypes where +import PlutusCore.Generators.QuickCheck.Builtin import PlutusCore.Generators.QuickCheck.Common import PlutusCore.Generators.QuickCheck.GenerateKinds import PlutusCore.Generators.QuickCheck.GenTm +import PlutusCore.Builtin import PlutusCore.Core import PlutusCore.Default import PlutusCore.MkPlc (mkTyBuiltin) @@ -129,8 +131,10 @@ shrinkKindAndType :: HasCallStack -> (Kind (), Type TyName DefaultUni ()) -> [(Kind (), Type TyName DefaultUni ())] shrinkKindAndType ctx (k0, ty) = + let minK0 = minimalType k0 in -- If we are not already minimal, add the minial type as a possible shrink. - [(k, m) | k <- k0 : shrink k0, let m = minimalType k, m /= ty] ++ + ([(k0, m) | let m = minimalType k0, m /= ty] ++) . filter ((/= minK0) . snd) $ + [(k, m) | k <- shrink k0, let m = minimalType k] ++ case ty of -- Variables shrink to arbitrary "smaller" variables -- Note: the order on variable names here doesn't matter, @@ -160,8 +164,10 @@ shrinkKindAndType ctx (k0, ty) = [ [ (ka, a) | ka `leKind` k0 ] - , [ (k0, typeSubstClosedType x (minimalType ka) b) + , [ (k0, typeSubstClosedType x m b) | TyLam _ x _ b <- [f] + , let m = minimalType ka + , m /= a -- @m == a@ is handled right below. ] , [ (k0, typeSubstClosedType x a b) | TyLam _ x _ b <- [f], null (setOf ftvTy a) @@ -171,20 +177,21 @@ shrinkKindAndType ctx (k0, ty) = -- apply f' to `fixKind ctx a ka'` - which takes `a` and tries to rewrite it -- to something of kind `ka'`. , concat - [ concat - [ case kf' of - Type{} -> [(kf', f')] - KindArrow _ ka' kb' -> - [ (kb', TyApp () f' (fixKind ctx a ka')) - | leKind kb' k0, leKind ka' ka - ] - | (kf', f') <- shrinkKindAndType ctx (KindArrow () ka k0, f) - ] - , -- Here we shrink the argument and fixup the function to have the right kind. - [ (k0, TyApp () (fixKind ctx f (KindArrow () ka' k0)) a') - | (ka', a') <- shrinkKindAndType ctx (ka, a) - ] + [ case kf' of + Type{} -> + [ (kf', f') + | f' /= a -- @f' == a@ is handled above. + ] + KindArrow _ ka' kb' -> + [ (kb', TyApp () f' (fixKind ctx a ka')) + | leKind kb' k0, leKind ka' ka + ] + | (kf', f') <- shrinkKindAndType ctx (KindArrow () ka k0, f) ] + , -- Here we shrink the argument and fixup the function to have the right kind. + [ (k0, TyApp () (fixKind ctx f (KindArrow () ka' k0)) a') + | (ka', a') <- shrinkKindAndType ctx (ka, a) + ] ] where ka = unsafeInferKind ctx a -- type lambdas shrink by either shrinking the kind of the argument or shrinking the body @@ -225,7 +232,10 @@ shrinkKindAndType ctx (k0, ty) = | (_, b') <- shrinkKindAndType (Map.insert x ka ctx) (Type (), b) ] ] - TyBuiltin{} -> [] + TyBuiltin _ builtin -> + [ (kindOfBuiltinType uni', TyBuiltin () $ SomeTypeIn uni') + | SomeTypeIn uni' <- shrinkBuiltinType builtin + ] TyIFix _ pat arg -> concat [ [ (Type (), fixKind ctx pat $ Type ()), (Type (), fixKind ctx arg $ Type ()) ] diff --git a/plutus-core/testlib/PlutusIR/Generators/QuickCheck.hs b/plutus-core/testlib/PlutusIR/Generators/QuickCheck.hs new file mode 100644 index 00000000000..291d19d153f --- /dev/null +++ b/plutus-core/testlib/PlutusIR/Generators/QuickCheck.hs @@ -0,0 +1,5 @@ +module PlutusIR.Generators.QuickCheck (module X) where + +import PlutusIR.Generators.QuickCheck.Common as X +import PlutusIR.Generators.QuickCheck.GenerateTerms as X +import PlutusIR.Generators.QuickCheck.ShrinkTerms as X diff --git a/plutus-core/testlib/PlutusIR/Generators/QuickCheck/Common.hs b/plutus-core/testlib/PlutusIR/Generators/QuickCheck/Common.hs new file mode 100644 index 00000000000..80ac58e099b --- /dev/null +++ b/plutus-core/testlib/PlutusIR/Generators/QuickCheck/Common.hs @@ -0,0 +1,110 @@ +-- editorconfig-checker-disable-file +{-# LANGUAGE TypeApplications #-} + +module PlutusIR.Generators.QuickCheck.Common where + +import PlutusCore.Generators.QuickCheck.Common +import PlutusCore.Generators.QuickCheck.Substitutions +import PlutusCore.Generators.QuickCheck.Unification + +import PlutusCore.Default +import PlutusCore.Name +import PlutusCore.Quote (runQuoteT) +import PlutusCore.Rename +import PlutusIR +import PlutusIR.Compiler +import PlutusIR.Error +import PlutusIR.Subst +import PlutusIR.TypeCheck + +import Control.Monad.Except +import Data.Bifunctor +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as Map +import Data.Set.Lens (setOf) +import Text.PrettyBy + +-- | Compute the datatype declarations that escape from a term. +datatypes :: Term TyName Name DefaultUni DefaultFun () + -> [(TyName, (Kind ()))] +datatypes tm = case tm of + Var _ _ -> mempty + Builtin _ _ -> mempty + Constant _ _ -> mempty + Apply _ _ _ -> mempty + LamAbs _ _ _ tm' -> datatypes tm' + TyAbs _ _ _ tm' -> datatypes tm' + TyInst _ _ _ -> mempty + Let _ _ binds tm' -> foldr addDatatype (datatypes tm') binds + where + addDatatype (DatatypeBind _ (Datatype _ (TyVarDecl _ a k) _ _ _)) = ((a, k):) + addDatatype _ = id + Error _ _ -> mempty + _ -> error "nope" + +-- | Try to infer the type of an expression in a given type and term context. +-- NOTE: one can't just use out-of-the-box type inference here because the +-- `inferType` algorithm happy renames things. +inferTypeInContext :: TypeCtx + -> Map Name (Type TyName DefaultUni ()) + -> Term TyName Name DefaultUni DefaultFun () + -> Either String (Type TyName DefaultUni ()) +inferTypeInContext tyctx ctx tm0 = first display + $ runQuoteT @(Either (Error DefaultUni DefaultFun ())) $ do + -- CODE REVIEW: this algorithm is fragile, it relies on knowing that `inferType` + -- does renaming to compute the `esc` substitution for datatypes. However, there is also + -- not any other way to do this in a way that makes type inference actually useful - you + -- want to do type inference in non-top-level contexts. Ideally I think type inference + -- probably shouldn't do renaming of datatypes... Or alternatively we need to ensure that + -- the renaming behaviour of type inference is documented and maintained. + cfg <- getDefTypeCheckConfig () + -- Infer the type of `tm` by adding the contexts as (type and term) lambdas + Normalized _ty' <- inferType cfg tm' + -- Substitute the free variables and escaping datatypes to get back to the un-renamed type. + let ty' = substEscape (Map.keysSet esc <> foldr (<>) (setOf ftvTy _ty') (setOf ftvTy <$> esc)) esc _ty' -- yuck + -- Get rid of the stuff we had to add for the context. + return $ stripFuns tms $ stripForalls mempty tys ty' + where + tm' = addTyLams tys $ addLams tms tm0 + rntm = case runQuoteT $ rename tm' of + Left _ -> error "impossible" + Right tm'' -> tm'' + + -- Compute the substitution that takes datatypes that escape + -- the scope in the inferred type (given by computing them from the + -- renamed term) and turns them into datatypes in the old type. + esc = Map.fromList (zip dats' $ map (TyVar ()) dats) + + dats' = map fst $ datatypes rntm + dats = map fst $ datatypes tm' + + tys = Map.toList tyctx + tms = Map.toList ctx + + addTyLams [] tm = tm + addTyLams ((x, k) : xs) tm = TyAbs () x k $ addTyLams xs tm + + addLams [] tm = tm + addLams ((x, ty) : xs) tm = LamAbs () x ty $ addLams xs tm + + stripForalls sub [] ty = substTypeParallel sub ty + stripForalls sub ((x, _) : xs) (TyForall _ y _ b) = stripForalls (Map.insert y (TyVar () x) sub) xs b + stripForalls _ _ _ = error "stripForalls" + + stripFuns [] ty = ty + stripFuns (_ : xs) (TyFun _ _ b) = stripFuns xs b + stripFuns _ _ = error "stripFuns" + +typeCheckTerm :: Term TyName Name DefaultUni DefaultFun () + -> Type TyName DefaultUni () + -> Either String () +typeCheckTerm = typeCheckTermInContext Map.empty Map.empty + +typeCheckTermInContext :: TypeCtx + -> Map Name (Type TyName DefaultUni ()) + -> Term TyName Name DefaultUni DefaultFun () + -> Type TyName DefaultUni () + -> Either String () +typeCheckTermInContext tyctx ctx tm ty = void $ do + ty' <- inferTypeInContext tyctx ctx tm + unifyType tyctx mempty ty' ty diff --git a/plutus-core/testlib/PlutusIR/Generators/QuickCheck/GenerateTerms.hs b/plutus-core/testlib/PlutusIR/Generators/QuickCheck/GenerateTerms.hs new file mode 100644 index 00000000000..b1cfcdf4135 --- /dev/null +++ b/plutus-core/testlib/PlutusIR/Generators/QuickCheck/GenerateTerms.hs @@ -0,0 +1,476 @@ +-- editorconfig-checker-disable-file +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PartialTypeSignatures #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} + +{-# OPTIONS_GHC -Wno-name-shadowing #-} +{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} + +module PlutusIR.Generators.QuickCheck.GenerateTerms where + +import PlutusIR.Generators.QuickCheck.Common + +import PlutusCore.Generators.QuickCheck.Builtin +import PlutusCore.Generators.QuickCheck.Common +import PlutusCore.Generators.QuickCheck.GenerateTypes +import PlutusCore.Generators.QuickCheck.GenTm +import PlutusCore.Generators.QuickCheck.ShrinkTypes +import PlutusCore.Generators.QuickCheck.Substitutions +import PlutusCore.Generators.QuickCheck.Unification +import PlutusCore.Generators.QuickCheck.Utils + +import PlutusCore.Builtin +import PlutusCore.Core (argsFunKind) +import PlutusCore.Default +import PlutusCore.MkPlc (mkConstantOf) +import PlutusCore.Name +import PlutusCore.Subst (typeSubstClosedType) +import PlutusIR +import PlutusIR.Compiler +import PlutusIR.Core.Instance.Pretty.Readable +import PlutusIR.Subst + +import Control.Lens ((<&>)) +import Control.Monad.Except +import Control.Monad.Reader +import Data.Bifunctor +import Data.Default.Class +import Data.Either +import Data.List.NonEmpty (NonEmpty (..)) +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as Map +import Data.Maybe +import Data.Proxy +import Data.Set qualified as Set +import Data.Set.Lens (setOf) +import Data.String +import GHC.Stack +import Prettyprinter +import Text.PrettyBy + +-- | This type keeps track of what kind of argument, term argument (`InstArg`) or +-- type argument (`InstApp`) is required for a function. This type is used primarily +-- with `findInstantiation` below where we do unification to figure out if we can +-- use a variable to construct a term of a target type. +data TyInst = InstApp (Type TyName DefaultUni ()) | InstArg (Type TyName DefaultUni ()) + deriving stock Show + +instance PrettyBy config (Type TyName DefaultUni ()) => PrettyBy config TyInst where + prettyBy ctx (InstApp ty) = prettyBy ctx ty + prettyBy ctx (InstArg ty) = brackets (prettyBy ctx ty) + +-- | If successful `findInstantiation n target ty` for an `x :: ty` gives a sequence of `TyInst`s containing `n` +-- `InstArg`s such that `x` instantiated (type application for `InstApp` and applied to a term of +-- the given type for `InstArg`) at the `TyInsts`s has type `target` +findInstantiation :: HasCallStack + => TypeCtx + -> Int + -> Type TyName DefaultUni () + -> Type TyName DefaultUni () + -> Either String [TyInst] +findInstantiation ctx n target ty = do + sub <- unifyType (ctx <> ctx') flex target b + let -- We map any unsolved flexible variable to a 'minimalType'. + defaultSub = minimalType <$> ctx' + doSub :: HasCallStack => _ + doSub = substType defaultSub . substType sub + doSubI (InstApp t) = InstApp (doSub t) + doSubI (InstArg t) = InstArg (doSub t) + pure $ map doSubI insts + where + fvs = setOf ftvTy target <> setOf ftvTy ty <> Map.keysSet ctx + (ctx', flex, insts, b) = view Map.empty Set.empty [] n fvs ty + + -- TODO: documentation! + view ctx' flex insts n fvs (TyForall _ x k b) = view (Map.insert x' k ctx') (Set.insert x' flex) + (InstApp (TyVar () x') : insts) n + (Set.insert x' fvs) b' + where (x', b') | Set.member x fvs = let x' = freshenTyNameWith fvs x in (x', renameVar x x' b) + | otherwise = (x, b) + view ctx' flex insts n fvs (TyFun _ a b) | n > 0 = view ctx' flex (InstArg a : insts) (n - 1) fvs b + view ctx' flex insts _ _ a = (ctx', flex, reverse insts, a) + +genConstant :: SomeTypeIn DefaultUni -> GenTm (Term TyName Name DefaultUni DefaultFun ()) +genConstant (SomeTypeIn b) = case toSingKind b of + SingType -> mkConstantOf () b <$> bring (Proxy @ArbitraryBuiltin) b (liftGen arbitraryBuiltin) + _ -> error "Higher-kinded built-in types cannot be used here" + +-- | Try to inhabit a given type in as simple a way as possible, +-- prefers to not default to `error` +inhabitType :: Type TyName DefaultUni () -> GenTm (Term TyName Name DefaultUni DefaultFun ()) +inhabitType ty0 = local (\ e -> e { geTerms = mempty }) $ do + errOrRes <- runExceptT $ findTm ty0 + pure $ case errOrRes of + Left _ -> Error () ty0 + Right res -> res + where + -- Do the obvious thing as long as target type is not type var + -- When type var: magic (if higher-kinded type var: black magic) + -- Ex: get `a` from D ts ==> get `a` from which ts, get which params from D + -- This function does not fail to error. + -- + -- NOTE: because we make recursive calls to findTm in this function instead of + -- inhabitType we don't risk generating terms that are "mostly ok but something is error", + -- this function will avoid error if possible. + findTm :: Type TyName DefaultUni () + -> ExceptT String GenTm (Term TyName Name DefaultUni DefaultFun ()) + findTm (normalizeTy -> ty) = case ty of + TyFun _ a b -> do + x <- lift $ genLikelyFreshName "x" + LamAbs () x a <$> mapExceptT (bindTmName x a) (findTm b) + TyForall _ x k b -> do + TyAbs () x k <$> mapExceptT (bindTyName x k) (findTm b) + TyBuiltin _ b -> lift $ genConstant b + -- If we have a type-function application + (viewApp [] -> (f, _)) -> + case f of + TyVar () x -> do + _ <- asks geDatas + asks (Map.lookup x . geDatas) >>= \ case + -- If the head is a datatype try to inhabit one of its constructors + Just dat -> foldr mplus mzero $ map (tryCon x ty) (constrTypes dat) + -- If its not a datatype we try to use whatever bound variables + -- we have to inhabit the type + Nothing -> do + vars <- asks geTerms + ctx <- asks geTypes + let cands = Map.toList vars + -- If we are instantiating something simply instantiate every + -- type application with type required by findInstantiation + doInst _ tm (InstApp instTy) = pure $ TyInst () tm instTy + -- If we instantiate an application, only succeed if we find + -- a non-error argument. + doInst _ tm (InstArg argTy) = Apply () tm <$> findTm argTy + -- Go over every type and try to inhabit the type at the arguments + case [ local (\e -> e { geTerms = Map.delete x' (geTerms e) }) + $ foldM (doInst n) (Var () x') insts + | (x', a) <- cands, + n <- [0..typeArity a], + Right insts <- [findInstantiation ctx n ty a], + x `Set.notMember` fvArgs a + ] of + [] -> mzero + g:_ -> g + _ -> mzero + + -- Try to inhabit a constructor `con` of type `conTy` in datatype `d` at type `ty` + tryCon d ty1 (con, conTy) + | Set.member d (fvArgs conTy) = mzero -- <- This is ok, since no mutual recursion + | otherwise = do + -- Check that we haven't banned this constructor + tmctx <- lift $ asks geTerms + if Map.lookup con tmctx == Just conTy + then do + tyctx <- lift $ asks geTypes + insts0 <- liftEither $ findInstantiation tyctx (typeArity conTy) ty1 conTy + let go tm [] = return tm + go tm (InstApp ty : insts) = go (TyInst () tm ty) insts + go tm (InstArg ty : insts) = do + arg <- findTm ty + go (Apply () tm arg) insts + go (Var () con) insts0 + else mzero + + -- CODE REVIEW: wouldn't it be neat if this existed somewhere? + viewApp args (TyApp _ f x) = viewApp (x : args) f + viewApp args ty = (ty, args) + + -- Get the free variables that appear in arguments of a mixed arrow-forall type + fvArgs (TyForall _ x _ b) = Set.delete x (fvArgs b) + fvArgs (TyFun _ a b) = setOf ftvTy a <> fvArgs b + fvArgs _ = mempty + +-- CODE REVIEW: does this exist anywhere? +typeArity :: Num a => Type tyname uni ann -> a +typeArity (TyForall _ _ _ a) = typeArity a +typeArity (TyFun _ _ b) = 1 + typeArity b +typeArity _ = 0 + +-- | Generate as small a term as possible to match a given type. +genAtomicTerm :: Type TyName DefaultUni () -> GenTm (Term TyName Name DefaultUni DefaultFun ()) +genAtomicTerm ty = do + ctx <- asks geTypes + vars <- asks geTerms + -- First try cheap unification + let unifyVar (x, xty) = findInstantiation ctx 0 ty xty + <&> \ tys -> foldl (TyInst ()) (Var () x) [t | InstApp t <- tys] + case rights $ map unifyVar $ Map.toList vars of + -- If unification didn't work try the heavy-handed `inhabitType`. + -- NOTE: We could probably just replace this whole function with + -- `inhabitType` and the generators would run fine, but this method + -- is probably faster a lot of the time and doesn't rely on the + -- order that thins are chosen `inhabitType`. It is also going to generate + -- a more even distribution than `inhabitType` (which for performance reasons + -- always returns the first thing it finds). + [] -> inhabitType ty + gs -> liftGen $ elements gs + +-- | Generate a term of a given type. +-- +-- Requires the type to be of kind *. +genTermOfType :: Type TyName DefaultUni () + -> GenTm (Term TyName Name DefaultUni DefaultFun ()) +genTermOfType ty = snd <$> genTerm (Just ty) + +-- | Generate a term, if the first argument is Nothing then we get something of any type +-- and if the first argument is `Just ty` we get something of type `ty`. +-- +-- Requires the type to be of kind *. +genTerm :: Maybe (Type TyName DefaultUni ()) + -> GenTm (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ()) +genTerm mty = checkInvariants $ do + customF <- asks geCustomFreq + customG <- asks geCustomGen + vars <- asks geTerms + esc <- asks geEscaping + -- Prefer to generate things that bind variables until we have "enough" (20...) + let (letF, lamF, varAppF) = if Map.size vars < 20 + then (30, 50, 10) + else (10, 30, 40) + atomic + | Just ty <- mty = (ty,) <$> genAtomicTerm ty + | otherwise = do + ty <- genType $ Type () + (ty,) <$> genAtomicTerm ty + ifAstSizeZero atomic $ + frequency $ + [ (10, atomic) ] ++ + [ (letF, genLet mty) ] ++ + [ (30, genForall x k a) | Just (TyForall _ x k a) <- [mty] ] ++ + [ (lamF, genLam a b) | Just (a, b) <- [funTypeView mty] ] ++ + [ (varAppF, genVarApp mty) ] ++ + [ (10, genApp mty) ] ++ + [ (1, genError mty) ] ++ + [ (10, genConst mty) | canConst mty ] ++ + [ (10, genDatLet mty) | YesEscape <- [esc] ] ++ + [ (10, genIfTrace) | isNothing mty ] ++ + [ (customF, customG mty) ] + where + + checkInvariants gen = do + (ty, tm) <- gen + debug <- asks geDebug + tyctx <- asks geTypes + tmctx <- asks geTerms + if debug then + case typeCheckTermInContext tyctx tmctx tm ty of + Left err -> + (error . show $ "genTerm - checkInvariants: term " <> prettyPirReadable tm + <> " does not type check at type " <> prettyPirReadable ty + <> " in type context " <> prettyPirReadable tyctx + <> " and term context " <> prettyPirReadable tmctx + <> " with error message " <> fromString err) + _ -> return (ty, tm) + else + return (ty, tm) + + funTypeView Nothing = Just (Nothing, Nothing) + funTypeView (Just (normalizeTy -> TyFun _ a b)) = Just (Just a, Just b) + funTypeView _ = Nothing + + -- Generate builtin ifthenelse and trace calls + genIfTrace = do + fun <- liftGen $ elements [IfThenElse, Trace] + pure (typeOfBuiltinFunction def fun, Builtin () fun) + + genError Nothing = do + ty <- genType $ Type () + return (ty, Error () ty) + genError (Just ty) = return (ty, Error () ty) + + canConst Nothing = True + canConst (Just TyBuiltin{}) = True + canConst (Just _) = False + + genConst Nothing = do + b <- deliver . liftGen . genBuiltinTypeOf $ Type () + (TyBuiltin () b, ) <$> genConstant b + genConst (Just ty@(TyBuiltin _ b)) = (ty,) <$> genConstant b + genConst _ = error "genConst: impossible" + + genDatLet mty = do + rec <- liftGen arbitrary + genDatatypeLet rec $ \ dat -> do + (ty, tm) <- genTerm mty + return $ (ty, Let () (if rec then Rec else NonRec) (DatatypeBind () dat :| []) tm) + + genLet mty = do + -- How many terms to bind + n <- liftGen $ choose (1, 3) + -- Names of the bound terms + xs <- genLikelyFreshNames $ replicate n "f" + -- Types of the bound terms + -- TODO: generate something that matches the target type + as <- onAstSize (`div` 8) $ vectorOf n $ genType (Type ()) + -- Strictness + ss <- vectorOf n $ liftGen $ elements [Strict, NonStrict] + -- Recursive? + r <- liftGen $ frequency [(1, pure True), (6, pure False)] + -- Generate the binding + -- TODO: maybe also generate mutually recursive bindings? + let genBin (x, a) | r = withNoEscape . bindTmName x a . genTermOfType $ a + | otherwise = withNoEscape . genTermOfType $ a + -- Generate both bound terms and body with a size split of 1:7 (note, we are generating up to three bound + -- terms, so the size split is really something like n:7). + (tms, (ty, body)) <- + astSizeSplit_ 1 7 (mapM genBin (zip xs as)) (bindTmNames (zip xs as) $ genTerm mty) + let mkBind (x, a, s) tm = TermBind () s + (VarDecl () x a) tm + b : bs = zipWith mkBind (zip3 xs as ss) tms + pure (ty, Let () (if r then Rec else NonRec) (b :| bs) body) + + genForall x k a = do + -- TODO: this freshenTyName here might be a bit paranoid + y <- freshenTyNameWith (setOf ftvTy a) <$> genLikelyFreshTyName "a" + let ty = TyForall () y k $ renameVar x y a + (ty,) . TyAbs () y k <$> (withNoEscape . bindTyName y k . genTermOfType $ renameVar x y a) + + genLam ma mb = do + x <- genLikelyFreshName "x" + (a, (b, body)) <- + astSizeSplit 1 7 + (maybe (genType $ Type ()) return ma) + (\ a -> bindTmName x a . withNoEscape $ genTerm mb) + pure (TyFun () a b, LamAbs () x a body) + + genApp mty = withNoEscape $ do + ((_, arg), (toResTy, fun)) <- + astSizeSplit 1 4 (genTerm Nothing) (\ (argTy, _) -> genFun argTy mty) + case toResTy of + TyFun _ _ resTy -> pure (resTy, Apply () fun arg) + _ -> error $ display toResTy ++ "\n\n is not a 'TyFun'" + where + genFun argTy mty = genTerm . Just . TyFun () argTy =<< maybe (genType (Type ())) pure mty + + genVarApp :: HasCallStack => _ + genVarApp Nothing = withNoEscape $ do + -- CODE REVIEW: this function exists somewhere maybe? (Maybe even in this module...) + let arity (TyForall _ _ _ b) = 1 + arity b + arity (TyFun _ _ b) = 1 + arity b + arity _ = 0 + + appl :: HasCallStack => Int -> Term TyName Name DefaultUni DefaultFun () -> _ + appl 0 tm b = return (b, tm) + appl n tm (TyForall _ x k b) = do + ty <- genType k + x' <- genLikelyFreshTyName "x" + appl (n - 1) (TyInst () tm ty) (substType (Map.singleton x' ty) $ renameVar x x' b) + appl n tm (TyFun _ a b) = do + (_, arg) <- genTerm (Just a) + appl (n - 1) (Apply () tm arg) b + appl _ _ _ = error "appl" + + genV (x, ty0) = do + let ty = normalizeTy ty0 + n <- liftGen $ choose (0, arity ty) + onAstSize (`div` n) $ appl n (Var () x) ty + asks (Map.toList . geTerms) >>= \ case + [] -> do + ty <- genType $ Type () + (ty,) <$> inhabitType ty + vars -> oneof $ map genV vars + + genVarApp (Just ty) = do + vars <- asks geTerms + ctx <- asks geTypes + let cands = Map.toList vars + doInst _ tm (InstApp instTy) = pure $ TyInst () tm instTy + doInst n tm (InstArg argTy) = onAstSize ((`div` n) . subtract 1) + . withNoEscape + $ Apply () tm <$> genTermOfType argTy + case [ foldM (doInst n) (Var () x) insts + | (x, a) <- cands, + n <- [0..typeArity a], + Right insts <- [findInstantiation ctx n ty a] + ] of + [] -> (ty,) <$> inhabitType ty + gs -> (ty,) <$> oneof gs + +-- | Like 'listOf' except each of the elements is generated with a proportionally smaller size. +scaledListOf :: GenTm a -> GenTm [a] +scaledListOf g = do + sz <- asks geAstSize + n <- choose (0, sz `div` 3) + onAstSize (`div` n) $ replicateM n g + +genDatatypeLet :: Bool -> (Datatype TyName Name DefaultUni () -> GenTm a) -> GenTm a +genDatatypeLet rec cont = do + k0 <- liftGen arbitrary + let ks = argsFunKind k0 + n <- liftGen $ choose (1, 3) + -- Lazy matching to communicate to GHC the fact that this can't fail and thus doesn't require + -- a 'MonadFail' (which 'GenTm' isn't). + ~(d : xs) <- genLikelyFreshTyNames $ "d" : replicate (length ks) "a" + ~(m : cs) <- genLikelyFreshNames $ "m" : replicate n "c" + let dTy = foldl (TyApp ()) (TyVar () d) [TyVar () x | x <- xs] + bty d = if rec + then bindTyName d k0 + else registerTyName d + conArgss <- bty d $ bindTyNames (zip xs ks) $ + -- Using 'listOf' instead if 'scaledListOf' makes the code slower by several + -- times (didn't check how exactly it affects the generated types). + onAstSize (`div` n) $ replicateM n $ scaledListOf (genType $ Type ()) + let dat = Datatype () (TyVarDecl () d k0) [TyVarDecl () x k | (x, k) <- zip xs ks] m + [ VarDecl () c (foldr (TyFun ()) dTy conArgs) + | (c, conArgs) <- zip cs conArgss ] + bindDat dat $ cont dat + +-- | Generate up to 5 datatypes and bind them in a generator. +-- NOTE: despite its name this function does in fact not generate the `Let` binding +-- for the datatypes. +genDatatypeLets :: ([Datatype TyName Name DefaultUni ()] -> GenTm a) -> GenTm a +genDatatypeLets cont = do + n0 <- liftGen $ choose (1, 5 :: Int) + let go 0 k = k [] + go n k = genDatatypeLet False $ \ dat -> go (n - 1) (k . (dat :)) + go n0 cont + +genTypeAndTerm_ :: Gen (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ()) +genTypeAndTerm_ = runGenTm $ do + (ty, body) <- genTerm Nothing + return (ty, body) + +genTypeAndTermDebug_ :: Gen (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ()) +genTypeAndTermDebug_ = runGenTm . withDebug $ do + (ty, body) <- genTerm Nothing + return (ty, body) + +-- | Take a term of a specified type and generate +-- a fully applied term. Useful for generating terms that you want +-- to stick directly in an interpreter. Prefers to generate small arguments. +-- NOTE: The logic of this generating small arguments is that the inner term +-- should already have plenty of complicated arguments to functions to begin +-- with and now we just want to fill out the arguments so that we get +-- something that hopefully evaluates for a non-trivial number of steps. +genFullyApplied :: Type TyName DefaultUni () + -> Term TyName Name DefaultUni DefaultFun () + -> Gen (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ()) +genFullyApplied typ0 trm0 = runGenTm $ go trm0 + where + go trm = case trm of + Let () rec binds body -> second (Let () rec binds) <$> bindBinds binds (go body) + _ -> genArgsApps typ0 trm + genArgsApps (TyForall _ x k typ) trm = do + let ty = minimalType k + genArgsApps (typeSubstClosedType x ty typ) (TyInst () trm ty) + genArgsApps (TyFun _ a b) trm = do + (_, arg) <- withNoEscape $ genTerm (Just a) + genArgsApps b (Apply () trm arg) + genArgsApps ty trm = return (ty, trm) + +-- | Generate a term of a specific type given a type and term context +genTermInContext_ :: TypeCtx + -> Map Name (Type TyName DefaultUni ()) + -> Type TyName DefaultUni () + -> Gen (Term TyName Name DefaultUni DefaultFun ()) +genTermInContext_ tyctx ctx ty = + runGenTm $ local (\ e -> e { geTypes = tyctx, geTerms = ctx, geEscaping = NoEscape }) $ + snd <$> genTerm (Just ty) diff --git a/plutus-core/testlib/PlutusIR/Generators/QuickCheck/ShrinkTerms.hs b/plutus-core/testlib/PlutusIR/Generators/QuickCheck/ShrinkTerms.hs new file mode 100644 index 00000000000..c62d1c41bf4 --- /dev/null +++ b/plutus-core/testlib/PlutusIR/Generators/QuickCheck/ShrinkTerms.hs @@ -0,0 +1,366 @@ +-- editorconfig-checker-disable-file +{-# LANGUAGE GADTs #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PartialTypeSignatures #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ViewPatterns #-} + +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} + +module PlutusIR.Generators.QuickCheck.ShrinkTerms where + +import PlutusIR.Generators.QuickCheck.Common + +import PlutusCore.Generators.QuickCheck.Builtin +import PlutusCore.Generators.QuickCheck.Common +import PlutusCore.Generators.QuickCheck.ShrinkTypes +import PlutusCore.Generators.QuickCheck.Substitutions +import PlutusCore.Generators.QuickCheck.Utils + +import PlutusCore.Builtin +import PlutusCore.Data +import PlutusCore.Default +import PlutusCore.MkPlc (mkConstant, mkConstantOf, mkTyBuiltin) +import PlutusCore.Name +import PlutusCore.Pretty +import PlutusCore.Subst (typeSubstClosedType) +import PlutusIR +import PlutusIR.Subst + +import Data.Bifunctor +import Data.Either +import Data.List.NonEmpty (NonEmpty (..)) +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as Map +import Data.Proxy +import Data.Set qualified as Set +import Data.Set.Lens (setOf) +import GHC.Stack +import Test.QuickCheck (shrinkList) + +addTmBind :: Binding TyName Name DefaultUni DefaultFun () + -> Map Name (Type TyName DefaultUni ()) + -> Map Name (Type TyName DefaultUni ()) +addTmBind (TermBind _ _ (VarDecl _ x a) _) = Map.insert x a +addTmBind (DatatypeBind _ dat) = (Map.fromList (matchType dat : constrTypes dat) <>) +addTmBind _ = id + +shrinkConstant :: DefaultUni (Esc a) -> a -> [Term TyName Name DefaultUni DefaultFun ()] +shrinkConstant uni x = + map (mkConstantOf () uni) $ bring (Proxy @ArbitraryBuiltin) uni $ shrinkBuiltin x + +scopeCheckTyVars :: TypeCtx + -> (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ()) + -> Bool +scopeCheckTyVars tyctx (ty, tm) = setOf ftvTy ty `Set.isSubsetOf` inscope + where + inscope = Map.keysSet tyctx <> Set.fromList (map fst $ datatypes tm) + +-- | Try to find a variable of type `forall x. x` in the context. +findHelp :: Map Name (Type TyName DefaultUni ()) -> Maybe Name +findHelp ctx = + case Map.toList $ Map.filter isHelpType ctx of + [] -> Nothing + (x, _) : _ -> Just x + where + isHelpType (TyForall _ x (Type ()) (TyVar _ x')) = x == x' + isHelpType _ = False + +mkHelp :: Map Name (Type TyName DefaultUni ()) + -> Type TyName DefaultUni () + -> Term TyName Name DefaultUni DefaultFun () +mkHelp _ (TyBuiltin _ b) = minimalBuiltin b +mkHelp (findHelp -> Just help) ty = TyInst () (Var () help) ty +mkHelp _ ty = Error () ty + +-- | Try to take a term from an old context to a new context and a new type. +-- If we can't do the new type we might return a different type. +fixupTerm_ :: TypeCtx + -> Map Name (Type TyName DefaultUni ()) + -> TypeCtx + -> Map Name (Type TyName DefaultUni ()) + -> Type TyName DefaultUni () + -> Term TyName Name DefaultUni DefaultFun () + -> (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ()) +fixupTerm_ tyctxOld ctxOld tyctxNew ctxNew tyNew tm0 = + case inferTypeInContext tyctxNew ctxNew tm0 of + Left _ -> case tm0 of + LamAbs _ x a tm | TyFun () _ b <- tyNew -> bimap (TyFun () a) (LamAbs () x a) + $ fixupTerm_ tyctxOld (Map.insert x a ctxOld) + tyctxNew (Map.insert x a ctxNew) b tm + Apply _ (Apply _ (TyInst _ (Builtin _ Trace) _) s) tm -> + let (ty', tm') = fixupTerm_ tyctxOld ctxOld tyctxNew ctxNew tyNew tm + in (ty', Apply () (Apply () (TyInst () (Builtin () Trace) ty') s) tm') + _ | TyBuiltin _ b <- tyNew -> (tyNew, minimalBuiltin b) + | otherwise -> (tyNew, mkHelp ctxNew tyNew) + Right ty -> (ty, tm0) + +-- | Try to take a term from an old context to a new context and a new type - default to `mkHelp`. +fixupTerm :: TypeCtx + -> Map Name (Type TyName DefaultUni ()) + -> TypeCtx + -> Map Name (Type TyName DefaultUni ()) + -> Type TyName DefaultUni () + -> Term TyName Name DefaultUni DefaultFun () + -> Term TyName Name DefaultUni DefaultFun () +fixupTerm _ _ tyctxNew ctxNew tyNew tm + | isRight (typeCheckTermInContext tyctxNew ctxNew tm tyNew) = tm + | otherwise = mkHelp ctxNew tyNew + +minimalBuiltin :: SomeTypeIn DefaultUni -> Term TyName Name DefaultUni DefaultFun () +minimalBuiltin (SomeTypeIn uni) = case toSingKind uni of + SingType -> mkConstantOf () uni $ go uni + _ -> error "Higher-kinded built-in types cannot be used here" + where + go :: DefaultUni (Esc a) -> a + go DefaultUniUnit = () + go DefaultUniInteger = 0 + go DefaultUniBool = False + go DefaultUniString = "" + go DefaultUniByteString = "" + go DefaultUniData = I 0 + go (DefaultUniProtoList `DefaultUniApply` _) = [] + go (DefaultUniProtoPair `DefaultUniApply` a `DefaultUniApply` b) = (go a, go b) + go (f `DefaultUniApply` _ `DefaultUniApply` _ `DefaultUniApply` _) = noMoreTypeFunctions f + +shrinkBind :: HasCallStack + => Recursivity + -> TypeCtx + -> Map Name (Type TyName DefaultUni ()) + -> Binding TyName Name DefaultUni DefaultFun () + -> [Binding TyName Name DefaultUni DefaultFun ()] +shrinkBind _ tyctx ctx bind = + case bind of + -- Note: this is a bit tricky for recursive binds, if we change a recursive bind we need to + -- fixup all the other binds in the block. Currently we do this with a fixupTerm_ in the + -- structural part of shrinking. In the future this can be made better if we find properties + -- where lets don't shrink well enough to be understandable. + TermBind _ s (VarDecl _ x ty) tm -> [ TermBind () s (VarDecl () x ty') tm' + | (ty', tm') <- shrinkTypedTerm tyctx ctx (ty, tm) + ] ++ + [ TermBind () Strict (VarDecl () x ty) tm | s == NonStrict ] + -- These cases are basically just structural + TypeBind _ (TyVarDecl _ a k) ty -> [ TypeBind () (TyVarDecl () a k') ty' + | (k', ty') <- shrinkKindAndType tyctx (k, ty) ] + DatatypeBind _ dat -> [ DatatypeBind () dat' | dat' <- shrinkDat tyctx dat ] + +shrinkDat :: TypeCtx + -> Datatype TyName Name DefaultUni () + -> [Datatype TyName Name DefaultUni ()] +shrinkDat ctx (Datatype _ dd@(TyVarDecl _ d _) xs m cs) = + [ Datatype () dd xs m cs' | cs' <- shrinkList shrinkCon cs ] + where + ctx' = ctx <> Map.fromList [ (x, k) | TyVarDecl _ x k <- xs ] + shrinkCon (VarDecl _ c ty) = [ VarDecl () c ty'' + | ty' <- shrinkType ctx' ty + , let ty'' = setTarget (getTarget ty) ty' + , ty'' /= ty + , d `Set.notMember` setOf ftvTy (setTarget (mkTyBuiltin @_ @() ()) ty') ] + where + getTarget (TyFun _ _ b) = getTarget b + getTarget b = b + setTarget t (TyFun _ a b) = TyFun () a (setTarget t b) + setTarget t _ = t + +{- +TODO: Note + +nonstructural cases for + + let x1 = y1 + x2 = y2 + in b + +1. drop all bindings +2. drop body and pick one binding as a new body and drop all bindings appearing after it +3. drop a single binding if there are more than one (because we handled a single one in 1) +-} + +{- +TODO: Note + +document terms giving duplicate shrinks like + +a -> a +let x = "abc" in "abc" +let x = "abc" in x +(\a1_1 -> a1_1) unit +-} + +-- | Shrink a typed term in a type and term context. +-- NOTE: if you want to understand what's going on in this function it's a good +-- idea to look at how we do this for types first (it's a lot simpler). +shrinkTypedTerm :: HasCallStack + => TypeCtx + -> Map Name (Type TyName DefaultUni ()) + -> (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ()) + -> [(Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())] +shrinkTypedTerm tyctx0 ctx0 (ty0, tm0) = concat + [ -- TODO: this somehow contributes a huge number of duplicates as reported by the @numShrink@ + -- test. How come? Is it because it's called from 'shrinkBind'? Do we even need this kind of + -- shrinking? + [ (ty', tm') + | not $ isHelp ctx0 tm0 + , ty' <- ty0 : shrinkType (tyctx0 <> Map.fromList (datatypes tm0)) ty0 + , let tm' = mkHelp ctx0 ty' + ] + , go tyctx0 ctx0 (ty0, tm0) + ] + where + isHelp _ (Constant _ _) = True + isHelp ctx (TyInst _ (Var _ x) _) = Just x == findHelp ctx + isHelp _ (Error _ _) = True + isHelp _ _ = False + + addTyBind (TypeBind _ (TyVarDecl _ a k) _) = Map.insert a k + addTyBind (DatatypeBind _ (Datatype _ (TyVarDecl _ a k) _ _ _)) = Map.insert a k + addTyBind _ = id + + addTyBindSubst (TypeBind _ (TyVarDecl _ a _) ty) = Map.insert a ty + addTyBindSubst _ = id + + go :: HasCallStack => _ + go tyctx ctx (ty, tm) = + filter (scopeCheckTyVars tyctx) $ + nonstructural tyctx ctx (ty, tm) ++ + structural tyctx ctx (ty, tm) + + -- TODO: what about 'TyInst'? + -- These are the special cases and "tricks" for shrinking + nonstructural :: HasCallStack => _ + nonstructural tyctx ctx (ty, tm) = + case tm of + -- TODO: shrink Rec to NonRec + Let _ rec bindsL body -> concat + [ -- + [ fixupTerm_ tyctxInner ctxInner tyctx ctx ty body + | let tyctxInner = foldr addTyBind tyctx bindsL + ctxInner = foldr addTmBind ctx bindsL + ] + , -- Make one of the let-bindings the new body dropping the old body and all the + -- bindings appearing after the chosen binding (we don't need them, since the whole + -- 'let' is non-recursive and hence the chosen binding can't reference those appearing + -- after it). + [ (letTy, case binds of + -- If there's no bindings before the chosen one, we don't recreate the 'let'. + [] -> letTm + b:bs -> Let () NonRec (b :| bs) letTm) + | (NonEmptyContext binds _, TermBind _ _ (VarDecl _ _ letTy) letTm) <- + oneHoleContexts bindsL + , rec == NonRec + -- TODO: check that the body is not one of the bound variables? + ] + , -- Drop a single binding. + [ second (Let () rec (b :| binds')) + $ fixupTerm_ tyctxInner ctxInner tyctxInner' ctxInner' ty body + | (NonEmptyContext binds0 binds1, _) <- oneHoleContexts bindsL, + let tyctxInner = foldr addTyBind tyctx bindsL + ctxInner = foldr addTmBind ctx bindsL + binds = binds0 ++ binds1 + tyctxInner' = foldr addTyBind tyctx binds + ctxInner' = foldr addTmBind ctx binds + , b:binds' <- [binds] + ] + ] + + LamAbs _ x a body -> + [ fixupTerm_ tyctx (Map.insert x a ctx) tyctx ctx b body + | TyFun _ _ b <- [ty] + ] + + Apply _ fun arg | Right argTy <- inferTypeInContext tyctx ctx arg -> + -- Drop substerms + [(argTy, arg), (TyFun () argTy ty, fun)] + + TyAbs _ x _ body -> + [ fixupTerm_ (Map.insert x k tyctx) ctx tyctx ctx tyInner' body + | TyForall _ y k tyInner <- [ty] + , let tyInner' = typeSubstClosedType y (minimalType k) tyInner + ] + + -- Builtins can shrink to unit. More fine-grained shrinking is in `structural` below. + Constant _ (Some (ValueOf uni _)) -> case uni of + DefaultUniUnit -> [] + _ -> [(mkTyBuiltin @_ @() (), mkConstant () ())] + + _ -> [] + + -- These are the structural (basically homomorphic) cases in shrinking. + -- They all just try to shrink a single subterm at a time. We also + -- use fixupTerm to adjust types here in a trick similar to how we shrunk + -- types above. + structural :: HasCallStack => _ + structural tyctx ctx (ty, tm) = + case tm of + + -- TODO: this needs a long, long Note... + Let _ rec binds body -> + [ (substTypeParallel subst ty', Let () rec binds body') + | (ty', body') <- go tyctxInner ctxInner (ty, body) ] ++ + [ fix $ second (Let () rec binds') $ + fixupTerm_ tyctxInner ctxInner tyctxInner' ctxInner' ty body + | (context@(NonEmptyContext before _), bind) <- oneHoleContexts binds, + let ctxBind | Rec <- rec = ctxInner + | otherwise = foldr addTmBind ctx before + tyctxBind | Rec <- rec = tyctxInner + | otherwise = foldr addTyBind tyctx before, + bind' <- shrinkBind rec tyctxBind ctxBind bind, + let binds' = plugHole context bind' + tyctxInner' = foldr addTyBind tyctx binds' + ctxInner' = foldr addTmBind ctx binds' + fix = uncurry (fixupTerm_ tyctx ctx tyctx ctx) + ] where subst = foldr addTyBindSubst mempty binds + tyctxInner = foldr addTyBind tyctx binds + ctxInner = foldr addTmBind ctx binds + + -- TODO: shrink the function too! + TyInst _ fun argTy -> case inferTypeInContext tyctx ctx fun of + Right (TyForall _ x k tyInner) -> + [ (substType (Map.singleton x argTy') tyInner', TyInst () fun' argTy') + | (k', argTy') <- shrinkKindAndType tyctx (k, argTy) + , let tyInner' | k == k' = tyInner + -- TODO: use proper fixupType + | otherwise = substType (Map.singleton x $ minimalType k) tyInner + fun' = fixupTerm tyctx ctx tyctx ctx (TyForall () x k' tyInner') fun + ] + Left err -> error $ displayPlcCondensedErrorClassic err + Right tyWrong -> error $ "Expected a 'TyForall', but got " ++ displayPlcDef tyWrong + + -- TODO: shrink the kind too like with the type in @LamAbs@ below. + TyAbs _ x _ body | not $ Map.member x tyctx -> + [ (TyForall () x k tyInner', TyAbs () x k body') + | TyForall _ y k tyInner <- [ty] + , (tyInner', body') <- go (Map.insert x k tyctx) ctx (renameVar y x tyInner, body) + ] + + LamAbs _ x a body -> + [ (TyFun () a b', LamAbs () x a body') + | TyFun _ _ b <- [ty], + (b', body') <- go tyctx (Map.insert x a ctx) (b, body) + ] ++ + [ bimap (TyFun () a') (LamAbs () x a') $ + fixupTerm_ tyctx (Map.insert x a ctx) tyctx (Map.insert x a' ctx) b body + | TyFun _ _ b <- [ty], + a' <- shrinkType tyctx a + ] + + Apply _ fun arg -> case inferTypeInContext tyctx ctx arg of + Left err -> error err + Right argTy -> + [ (ty', Apply () fun' arg') + | (TyFun _ argTy' ty', fun') <- go tyctx ctx (TyFun () argTy ty, fun) + , let arg' = fixupTerm tyctx ctx tyctx ctx argTy' arg + ] ++ + [ (ty, Apply () fun' arg') + | (argTy', arg') <- go tyctx ctx (argTy, arg) + , let fun' = fixupTerm tyctx ctx tyctx ctx (TyFun () argTy' ty) fun + ] + + Constant _ (Some (ValueOf uni x)) -> map ((,) ty) $ shrinkConstant uni x + + -- TODO: handle all the cases explicitly. + _ -> [] + +shrinkClosedTypedTerm :: (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ()) + -> [(Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())] +shrinkClosedTypedTerm = shrinkTypedTerm mempty mempty