/
GeneratorSpec.hs
277 lines (249 loc) · 12 KB
/
GeneratorSpec.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}
module GeneratorSpec where
import PlutusCore.Generators.PIR
import Control.Monad.Reader
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set qualified as Set
import Data.Char
import Data.List hiding (insert)
import Data.List.NonEmpty (NonEmpty (..))
import Text.Printf
import PlutusCore.Default
import PlutusCore.Name
import PlutusCore.Quote (runQuoteT)
import PlutusCore.Rename
import PlutusIR
import PlutusIR.Core.Instance.Pretty.Readable
import Data.Maybe
import Data.String
import Test.QuickCheck
import Test.Tasty
import Test.Tasty.Extras
import Test.Tasty.QuickCheck
-- CODE REVIEW: The property below checks that when we run a generated PIR term through the compiler
-- we actually get something out. As the generators are supposed to generate reasonable stuff this is
-- a test of the compiler. I think we
-- 1. Want this somewhere
-- 2. Don't want it here
-- Where do we want something like this?
-- Also, the code below is a giant hack to "conenct to" the compiler at the "right" place (as judged
-- by us when we were ripping the compiler apart to extract something that did something reasonable-ish)
--
-- TODO: we want this property somewhere!
-- compile :: Term TyName Name DefaultUni DefaultFun ()
-- -> Either (CompileError DefaultUni DefaultFun) (CompiledCode a)
-- compile _tm = either Left Right $ runQuoteT $ do
-- -- Make sure that names are unique (that's not guaranteed by QuickCheck)
-- tm <- rename _tm
-- plcTcConfig <- PLC.getDefTypeCheckConfig PIR.noProvenance
-- let hints = UPLC.InlineHints $ \a _ -> case a of
-- PIR.DatatypeComponent PIR.Destructor _ -> True
-- _ -> False
-- pirCtx = PIR.toDefaultCompilationCtx plcTcConfig
-- & set (PIR.ccOpts . PIR.coOptimize) True
-- & set (PIR.ccOpts . PIR.coPedantic) False
-- & set (PIR.ccOpts . PIR.coVerbose) False
-- & set (PIR.ccOpts . PIR.coDebug) False
-- & set (PIR.ccOpts . PIR.coMaxSimplifierIterations)
-- (PIR.defaultCompilationOpts ^. PIR.coMaxSimplifierIterations)
-- & set PIR.ccTypeCheckConfig Nothing
-- uplcSimplOpts = UPLC.defaultSimplifyOpts
-- & set UPLC.soMaxSimplifierIterations (PIR.defaultCompilationOpts ^. PIR.coMaxSimplifierIterations)
-- & set UPLC.soInlineHints hints
--
-- plcT <- flip runReaderT pirCtx $ PIR.compileReadableToPlc $ fmap Original tm
-- plcTcError <- runExceptT @(PLC.Error _ _ _)
-- $ UPLC.deBruijnTerm =<< UPLC.simplifyTerm uplcSimplOpts (UPLC.erase plcT)
-- case plcTcError of
-- Left _ -> error "wrong"
-- Right cc -> return $ DeserializedCode (UPLC.Program () (PLC.defaultVersion ()) $ void cc) Nothing mempty
--
-- prop_compile :: Property
-- prop_compile =
-- forAllDoc "_,tm" genTypeAndTermNoHelp_ (shrinkTypedTerm mempty mempty) $ \ (_, tm) ->
-- isRight $ compile tm
generators :: TestNested
generators = return $ testGroup "generators"
[ testProperty "prop_genKindCorrect" $ withMaxSuccess 1000 prop_genKindCorrect
, testProperty "prop_shrinkTypeSound" $ prop_shrinkTypeSound
, testProperty "prop_genTypeCorrect" $ withMaxSuccess 1000 prop_genTypeCorrect
, testProperty "prop_shrinkTermSound" $ withMaxSuccess 20 prop_shrinkTermSound
]
-- * Core properties for PIR generators
-- | Check that the types we generate are kind-correct
-- See Note [Debugging generators that don't generate well-typed/kinded terms/types]
-- when this property fails.
prop_genKindCorrect :: Property
prop_genKindCorrect =
forAllDoc "ctx" genCtx (const []) $ \ ctx ->
-- Note, no shrinking here because shrinking relies on well-kindedness.
forAllDoc "k,ty" genKindAndType (const []) $ \ (k, ty) ->
checkKind ctx ty k
-- | Check that shrinking types maintains kinds
prop_shrinkTypeSound :: Property
prop_shrinkTypeSound =
forAllDoc "k,ty" genKindAndType (shrinkKindAndType Map.empty) $ \ (k, ty) ->
-- See discussion about the same trick in `prop_shrinkTermSound`
checkKind Map.empty ty k ==>
checkNoCounterexamples [ (k, ty) | (k, ty) <- shrinkKindAndType Map.empty (k, ty)
, not $ checkKind Map.empty ty k ]
-- | 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]
-- when this property fails.
prop_genTypeCorrect :: Property
prop_genTypeCorrect =
-- 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.
forAllDoc "ty,tm" genTypeAndTerm_ (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_ (shrinkTypedTerm mempty mempty) $ \ (ty, tm) ->
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 =
forAllShrinkBlind (pure False) (\ sh -> [ True | not sh ]) $ \ _ ->
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.
typeCheckTerm tm ty ==>
not (null shrinks) ==>
checkNoCounterexamples [ (ty, tm, scopeCheckTyVars Map.empty (ty, tm))
| (ty, tm) <- shrinks, not $ typeCheckTerm tm ty ]
-- * Utility tests for debugging generators that behave weirdly
-- | Test that `typeInstTerm` results in a well-typed instantiation.
prop_typeInstTerm :: Property
prop_typeInstTerm =
forAllDoc "ctx" genCtx (const []) $ \ ctx ->
forAllDoc "ty" (genTypeWithCtx ctx $ Star) (shrinkType ctx) $ \ ty ->
forAllDoc "target" (genTypeWithCtx ctx $ Star) (shrinkType ctx) $ \ target ->
checkNoCounterexamples [ (n, insts)
| n <- [0..arity ty+3]
, Just insts <- [typeInstTerm ctx n target ty]
, not $ checkInst ctx x ty insts target
]
where
x = Name "x" (toEnum 0)
arity (TyForall _ _ _ a) = arity a
arity (TyFun _ _ b) = 1 + arity b
arity _ = 0
checkInst ctx x ty insts target = typeCheckTermInContext ctx tmCtx tm target
where
(tmCtx, tm) = go (toEnum 1) (Map.singleton x ty) (Var () x) insts
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.
leavesish (Var _ x) = [x]
leavesish (TyInst _ a _) = leavesish a
leavesish (Let _ _ _ b) = leavesish b
leavesish (LamAbs _ _ _ b) = leavesish b
leavesish (Apply _ a b) = leavesish a ++ leavesish b
leavesish Error{} = [Name "error" $ toEnum 0]
leavesish Builtin{} = [Name "builtin" $ toEnum 0]
leavesish _ = []
-- | 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 = shrinkClosedTypedTerm (ty, tm)
n = fromIntegral (length shrinks)
u = fromIntegral (length $ nub shrinks)
r | n > 0 = (n - u) / n :: Double
| otherwise = 0
in tabulate "r" [printf "%0.1f" r] True
-- | Specific test that `inhabitType` returns well-typed things
prop_inhabited :: Property
prop_inhabited =
forAllDoc "ty,tm" (genInhab mempty) (shrinkTypedTerm mempty mempty) $ \ (ty, tm) -> typeCheckTerm tm ty
where
genInhab ctx = runGenTm $ local (\ e -> e { geTypes = ctx }) $
genDatatypeLets $ \ dats -> do
ty <- genType Star
tm <- inhabitType ty
return (ty, foldr (\ dat -> Let () NonRec (DatatypeBind () dat :| [])) tm dats)
-- | Test that shrinking types results in smaller types. Useful for debugging shrinking.
prop_shrinkTypeSmaller :: Property
prop_shrinkTypeSmaller =
forAllDoc "k,ty" genKindAndType (shrinkKindAndType Map.empty) $ \ (k, ty) ->
checkNoCounterexamples [ (k', ty') | (k', ty') <- shrinkKindAndType Map.empty (k, ty), not $ leKind k' k ]
-- | Test that shrinking kinds generates smaller kinds
prop_shrinkKindSmaller :: Property
prop_shrinkKindSmaller =
forAllDoc "k" arbitrary shrink $ \ k ->
checkNoCounterexamples [ k' | k' <- shrink k, not $ ltKind k' k ]
-- | Test that fixKind actually gives you something of the right kind
prop_fixKind :: Property
prop_fixKind =
forAllDoc "k,ty" genKindAndType (shrinkKindAndType Map.empty) $ \ (k, ty) ->
checkNoCounterexamples [ (ty', k') | k' <- shrink k
, let ty' = fixKind Map.empty ty k'
, not $ checkKind Map.empty ty' k' ]
-- * Tests for unification and substitution
-- | Check that unification does the right thing.
prop_unify :: Property
prop_unify =
forAllDoc "n" arbitrary shrink $ \ (NonNegative n) ->
forAllDoc "m" (choose (0, n)) shrink $ \ m ->
letCE "xs" (take n allTheVarsCalledX) $ \ xs ->
forAllDoc "ks"
(vectorOf n arbitrary)
(filter ((== n) . length) . shrink) $ \ ks ->
letCE "ctx" (Map.fromList $ zip xs ks) $ \ ctx ->
forAllDoc "ty1"
(genTypeWithCtx ctx $ Star)
(shrinkType ctx) $ \ ty1 ->
forAllDoc "ty2"
(genTypeWithCtx ctx $ Star)
(shrinkType ctx) $ \ ty2 ->
letCE "nty1" (normalizeTy ty1) $ \ _ ->
letCE "nty2" (normalizeTy ty2) $ \ _ ->
letCE "res" (unifyType ctx (Set.fromList $ take m xs) Map.empty ty1 ty2) $ \ res ->
isJust res ==>
let sub = fromJust res
checkSub (x, ty) = letCE "x,ty" (x, ty) $ \ _ ->
letCE "k" (ctx Map.! x) $ \ k -> checkKind ctx ty k
in
letCE "sty1" (substType sub ty1) $ \ sty1 ->
letCE "sty2" (substType sub ty2) $ \ sty2 ->
letCE "nsty1" (normalizeTy sty1) $ \ nsty1 ->
letCE "nsty2" (normalizeTy sty2) $ \ nsty2 ->
tabulate "sizes" [show $ min (Set.size $ fvType ty1) (Set.size $ fvType ty2)] $
foldr (.&&.) (property $ nsty1 == nsty2) (map checkSub (Map.toList sub))
where
allTheVarsCalledX = [ TyName $ Name (fromString $ "x" ++ show i) (toEnum i) | i <- [1..] ]
-- | Check that a type unifies with a renaming of itself
prop_unifyRename :: Property
prop_unifyRename =
forAllDoc "_, ty" genKindAndType (shrinkKindAndType mempty) $ \ (_, ty) ->
letCE "rename ty" (runQuote $ rename ty) $ \ rnty ->
isJust $ unifyType mempty mempty mempty ty rnty
-- | Check that substitution gets rid of all the right variables
prop_substType :: Property
prop_substType =
forAllDoc "ctx" genCtx (const []) $ \ ctx ->
forAllDoc "ty" (genTypeWithCtx ctx Star) (shrinkType ctx) $ \ ty ->
forAllDoc "sub" (genSubst ctx) (shrinkSubst ctx) $ \ sub ->
letCE "res" (substType sub ty) $ \ res ->
fvTypeR sub ty == fvType res && checkKind ctx res Star