2
{-# LANGUAGE FlexibleInstances #-}
2
{-# LANGUAGE FlexibleInstances #-}
3
3
{-# LANGUAGE FunctionalDependencies #-}
4
{-# LANGUAGE MultiParamTypeClasses #-}
5
{-# LANGUAGE TypeSynonymInstances #-}
6
{-# LANGUAGE UndecidableInstances #-}
4
{-# LANGUAGE MultiParamTypeClasses #-}
5
{-# LANGUAGE TypeSynonymInstances #-}
6
{-# LANGUAGE UndecidableInstances #-}
8
8
module Agda.TypeChecking.Test.Generators where
25
25
import Agda.Utils.TestHelpers
26
26
import qualified Agda.Utils.VarSet as Set
28
#include "../../undefined.h"
28
#include "undefined.h"
29
29
import Agda.Utils.Impossible
31
31
data TermConfiguration = TermConf
32
{ tcDefinedNames :: [QName]
32
{ tcDefinedNames :: [QName]
33
33
, tcConstructorNames :: [QName]
34
34
, tcProjectionNames :: [QName]
35
, tcFreeVariables :: [Nat]
36
, tcLiterals :: UseLiterals
37
, tcFrequencies :: Frequencies
38
, tcFixSize :: Maybe Int
39
-- ^ Maximum size of the generated element. When @Nothing@ this value
40
-- is initialized from the 'Test.QuickCheck.size' parameter.
42
-- ^ When this is true no lambdas, literals, or constructors are
35
, tcFreeVariables :: [Nat]
36
, tcLiterals :: UseLiterals
37
, tcFrequencies :: Frequencies
38
, tcFixSize :: Maybe Int
39
-- ^ Maximum size of the generated element. When @Nothing@ this value
40
-- is initialized from the 'Test.QuickCheck.size' parameter.
42
-- ^ When this is true no lambdas, literals, or constructors are
85
85
defaultFrequencies :: Frequencies
86
86
defaultFrequencies = Freqs
87
{ termFreqs = TermFreqs { varFreq = 24, defFreq = 8, conFreq = 8, litFreq = 1, sortFreq = 2, lamFreq = 10, piFreq = 5, funFreq = 5 }
87
{ termFreqs = TermFreqs { varFreq = 24, defFreq = 8, conFreq = 8, litFreq = 1, sortFreq = 2, lamFreq = 10, piFreq = 5, funFreq = 5 }
88
88
, elimFreqs = ElimFreqs { applyFreq = 9, projFreq = 1 }
89
89
, hiddenFreqs = HiddenFreqs { hiddenFreq = 1, notHiddenFreq = 5 }
90
, sortFreqs = SortFreqs { setFreqs = [3, 1], propFreq = 1 }
90
, sortFreqs = SortFreqs { setFreqs = [3, 1], propFreq = 1 }
93
93
noProp :: TermConfiguration -> TermConfiguration
94
94
noProp conf = conf { tcFrequencies = fq { sortFreqs = sfq { propFreq = 0 } } }
96
fq = tcFrequencies conf
96
fq = tcFrequencies conf
99
99
data UseLiterals = UseLit
100
100
{ useLitInt :: Bool
138
138
, tcProjectionNames = projs
139
139
, tcFreeVariables = List.sort $ List.nub vs
140
140
, tcFrequencies = defaultFrequencies
141
, tcLiterals = noLiterals
142
, tcFixSize = Nothing
141
, tcLiterals = noLiterals
142
, tcFixSize = Nothing
146
146
(defs, cons, projs) = flip evalState 0 $ do
152
152
return $ QName { qnameModule = MName []
154
{ nameId = NameId n 1
155
, nameConcrete = C.Name noRange [C.Id s]
156
, nameBindingSite = noRange
157
, nameFixity = defaultFixity'
154
{ nameId = NameId n 1
155
, nameConcrete = C.Name noRange [C.Id s]
156
, nameBindingSite = noRange
157
, nameFixity = defaultFixity'
161
161
class GenC a where
162
162
genC :: TermConfiguration -> Gen a
164
newtype YesType a = YesType { unYesType :: a }
165
newtype NoType a = NoType { unNoType :: a }
166
newtype VarName = VarName { unVarName :: Nat }
167
newtype DefName = DefName { unDefName :: QName }
168
newtype ConName = ConName { unConName :: ConHead }
164
newtype YesType a = YesType { unYesType :: a }
165
newtype NoType a = NoType { unNoType :: a }
166
newtype VarName = VarName { unVarName :: Nat }
167
newtype DefName = DefName { unDefName :: QName }
168
newtype ConName = ConName { unConName :: ConHead }
169
169
newtype ProjName = ProjName { unProjName :: QName }
170
170
newtype SizedList a = SizedList { unSizedList :: [a] }
194
194
genC conf = frequency [ (hideF, return Hidden), (nohideF, return NotHidden) ]
196
196
HiddenFreqs {hiddenFreq = hideF, notHiddenFreq = nohideF } =
197
hiddenFreqs $ tcFrequencies conf
197
hiddenFreqs $ tcFrequencies conf
199
199
instance (GenC c, GenC a) => GenC (Common.Arg c a) where
200
200
genC conf = (\ (h, a) -> Arg (setHiding h defaultArgInfo) a) <$> genC conf
211
211
, (projF, Proj . unProjName <$> genC conf) ]
213
213
ElimFreqs {applyFreq = applyF, projFreq = projF } =
214
elimFreqs $ tcFrequencies conf
214
elimFreqs $ tcFrequencies conf
216
216
instance GenC DefName where
217
217
genC conf = DefName <$> do elements $ tcDefinedNames conf
246
246
instance GenC Literal where
247
247
genC conf = oneof (concat $ zipWith gen useLits
248
[ uncurry LitInt <$> genC conf
249
, uncurry LitFloat <$> genC conf
250
, uncurry LitString <$> genC conf
251
, uncurry LitChar <$> genC conf
248
[ uncurry LitInt <$> genC conf
249
, uncurry LitFloat <$> genC conf
250
, uncurry LitString <$> genC conf
251
, uncurry LitChar <$> genC conf
255
255
useLits = map ($ tcLiterals conf) [ useLitInt, useLitFloat, useLitString, useLitChar ]
270
270
genC conf = case tcFixSize conf of
271
271
Nothing -> sized $ \n -> genC $ fixSizeConf n conf
272
272
Just n | n <= 0 -> genLeaf
273
| otherwise -> frequency
274
[ (varF, genVar $ genElims conf)
275
, (defF, genDef $ genElims conf)
276
, (conF, genCon $ genArgs conf)
277
, (litF, Lit <$> genC conf)
278
, (sortF, Sort <$> genC conf)
273
| otherwise -> frequency
274
[ (varF, genVar $ genElims conf)
275
, (defF, genDef $ genElims conf)
276
, (conF, genCon $ genArgs conf)
277
, (litF, Lit <$> genC conf)
278
, (sortF, Sort <$> genC conf)
283
283
defs = tcDefinedNames conf
284
284
cons = tcConstructorNames conf
288
288
useLits = map ($ tcLiterals conf) [ useLitInt, useLitFloat, useLitString, useLitChar ]
290
290
varF | null vars = 0
291
| otherwise = freq (varFreq . termFreqs)
291
| otherwise = freq (varFreq . termFreqs)
292
292
defF | null defs = 0
293
| otherwise = freq (defFreq . termFreqs)
293
| otherwise = freq (defFreq . termFreqs)
294
294
conF | null cons || isType = 0
295
| otherwise = freq (conFreq . termFreqs)
295
| otherwise = freq (conFreq . termFreqs)
296
296
litF | or useLits && not isType = freq (litFreq . termFreqs)
298
298
lamF | isType = 0
299
| otherwise = freq (lamFreq . termFreqs)
299
| otherwise = freq (lamFreq . termFreqs)
300
300
sortF = freq (sortFreq . termFreqs)
301
301
piF = freq (piFreq . termFreqs)
311
311
genDef args = Def <$> elements defs <*> args
313
313
genCon :: Gen Args -> Gen Term
314
genCon args = Con <$> (flip ConHead [] <$> elements cons) <*> args
314
genCon args = Con <$> ((\ c -> ConHead c Inductive []) <$> elements cons) <*> args
316
316
genLeaf :: Gen Term
317
317
genLeaf = frequency
318
[ (varF, genVar $ return [])
319
, (defF, genDef $ return [])
320
, (conF, genCon $ return [])
321
, (litF, Lit <$> genC conf)
322
, (sortF, Sort <$> genC conf)
318
[ (varF, genVar $ return [])
319
, (defF, genDef $ return [])
320
, (conF, genCon $ return [])
321
, (litF, Lit <$> genC conf)
322
, (sortF, Sort <$> genC conf)
325
325
-- | Only generates default configurations. Names and free variables varies.
326
326
genConf :: Gen TermConfiguration
395
395
noShrink = unDefName
397
397
instance ShrinkC ConName ConHead where
398
shrinkC conf (ConName (ConHead{conName = c})) = map (flip ConHead []) $ takeWhile (/= c) $ tcConstructorNames conf
398
shrinkC conf (ConName (ConHead{conName = c})) = map (\ c -> ConHead c Inductive []) $ takeWhile (/= c) $ tcConstructorNames conf
399
399
noShrink = unConName
401
401
instance ShrinkC Literal Literal where
402
402
shrinkC _ (LitInt _ 0) = []
403
shrinkC conf l = LitInt noRange 0 : case l of
403
shrinkC conf l = LitInt noRange 0 : case l of
404
404
LitInt r n -> LitInt r <$> shrink n
405
405
LitString r s -> LitString r <$> shrinkC conf s
406
406
LitChar r c -> LitChar r <$> shrinkC conf c
455
455
instance ShrinkC Telescope Telescope where
456
shrinkC conf EmptyTel = []
456
shrinkC conf EmptyTel = []
457
457
shrinkC conf (ExtendTel a tel) =
458
458
killAbs tel : (uncurry ExtendTel <$> shrinkC conf (a, tel))
465
465
instance ShrinkC Term Term where
466
466
shrinkC conf (DontCare _) = []
467
467
shrinkC conf (Sort Prop) = []
468
shrinkC conf t = filter validType $ case ignoreSharing t of
468
shrinkC conf t = filter validType $ case ignoreSharing t of
469
469
Var i es -> map unArg (argsFromElims es) ++
470
(uncurry Var <$> shrinkC conf (VarName i, NoType es))
470
(uncurry Var <$> shrinkC conf (VarName i, NoType es))
471
471
Def d es -> map unArg (argsFromElims es) ++
472
(uncurry Def <$> shrinkC conf (DefName d, NoType es))
472
(uncurry Def <$> shrinkC conf (DefName d, NoType es))
473
473
Con c args -> map unArg args ++
474
(uncurry Con <$> shrinkC conf (ConName c, NoType args))
475
Lit l -> Lit <$> shrinkC conf l
474
(uncurry Con <$> shrinkC conf (ConName c, NoType args))
475
Lit l -> Lit <$> shrinkC conf l
476
476
Level l -> [] -- TODO
477
477
Lam info b -> killAbs b : ((\(h,x) -> Lam (setHiding h defaultArgInfo) x)
478
478
<$> shrinkC conf (argInfoHiding info, b))
479
479
Pi a b -> unEl (unDom a) : unEl (killAbs b) :
480
(uncurry Pi <$> shrinkC conf (a, b))
480
(uncurry Pi <$> shrinkC conf (a, b))
481
481
Sort s -> Sort <$> shrinkC conf s
482
482
MetaV m es -> map unArg (argsFromElims es) ++
483
483
(MetaV m <$> shrinkC conf (NoType es))
485
485
Shared{} -> __IMPOSSIBLE__
486
ExtLam _ _ -> __IMPOSSIBLE__
488
| not (tcIsType conf) = True
489
| otherwise = case t of
489
| not (tcIsType conf) = True
490
| otherwise = case t of
496
497
killAbs :: KillVar a => Abs a -> a
503
504
instance KillVar Term where
504
505
killVar i t = case ignoreSharing t of
505
Var j args | j == i -> DontCare (Var j [])
506
| j > i -> Var (j - 1) $ killVar i args
507
| otherwise -> Var j $ killVar i args
508
Def c args -> Def c $ killVar i args
509
Con c args -> Con c $ killVar i args
506
Var j args | j == i -> DontCare (Var j [])
507
| j > i -> Var (j - 1) $ killVar i args
508
| otherwise -> Var j $ killVar i args
509
Def c args -> Def c $ killVar i args
510
Con c args -> Con c $ killVar i args
511
512
Level l -> Level l -- TODO
513
Lam h b -> Lam h $ killVar i b
514
Pi a b -> uncurry Pi $ killVar i (a, b)
515
MetaV m args -> MetaV m $ killVar i args
514
Lam h b -> Lam h $ killVar i b
515
Pi a b -> uncurry Pi $ killVar i (a, b)
516
MetaV m args -> MetaV m $ killVar i args
516
517
DontCare mv -> DontCare $ killVar i mv
517
518
Shared{} -> __IMPOSSIBLE__
519
ExtLam _ _ -> __IMPOSSIBLE__
519
521
instance KillVar Type where
520
522
killVar i (El s t) = El s $ killVar i t
522
524
instance KillVar Telescope where
523
killVar i EmptyTel = EmptyTel
525
killVar i EmptyTel = EmptyTel
524
526
killVar i (ExtendTel a tel) = uncurry ExtendTel $ killVar i (a, tel)
526
528
instance KillVar a => KillVar (Elim' a) where
added
removed
src/full/Agda/TypeChecking/Test/Generators.hs
