-
Notifications
You must be signed in to change notification settings - Fork 479
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[PIR] [Test] Add term generators (#4949)
- Loading branch information
1 parent
56e893f
commit febabc4
Showing
13 changed files
with
1,358 additions
and
61 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.