Agda-2.3.0: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Test.Generators

Synopsis

Documentation

data TermConfiguration

Constructors

TermConf 

Fields

tcDefinedNames :: [QName]
 
tcConstructorNames :: [QName]
 
tcFreeVariables :: [Nat]
 
tcLiterals :: UseLiterals
 
tcFrequencies :: Frequencies
 
tcFixSize :: Maybe Int

Maximum size of the generated element. When Nothing this value is initialized from the Test.QuickCheck.size parameter.

tcIsType :: Bool

When this is true no lambdas, literals, or constructors are generated

data TermFreqs

Constructors

TermFreqs 

Fields

nameFreq :: Int
 
litFreq :: Int
 
sortFreq :: Int
 
lamFreq :: Int
 
piFreq :: Int
 
funFreq :: Int
 

Instances

data NameFreqs

Constructors

NameFreqs 

Fields

varFreq :: Int
 
defFreq :: Int
 
conFreq :: Int
 

Instances

data HiddenFreqs

Constructors

HiddenFreqs 

Instances

data SortFreqs

Constructors

SortFreqs 

Fields

setFreqs :: [Int]
 
propFreq :: Int
 

Instances

data UseLiterals

Constructors

UseLit 

Instances

class GenC a where

Methods

genC :: TermConfiguration -> Gen a

Instances

newtype YesType a

Constructors

YesType 

Fields

unYesType :: a
 

Instances

ShrinkC a b => ShrinkC (YesType a) b 

newtype NoType a

Constructors

NoType 

Fields

unNoType :: a
 

Instances

ShrinkC a b => ShrinkC (NoType a) b 

newtype VarName

Constructors

VarName 

Fields

unVarName :: Nat
 

Instances

newtype DefName

Constructors

DefName 

Fields

unDefName :: QName
 

Instances

newtype ConName

Constructors

ConName 

Fields

unConName :: QName
 

Instances

newtype SizedList a

Constructors

SizedList 

Fields

unSizedList :: [a]
 

Instances

GenC a => GenC (SizedList a) 

genConf :: Gen TermConfiguration

Only generates default configurations. Names and free variables varies.

class ShrinkC a b | a -> b where

Methods

shrinkC :: TermConfiguration -> a -> [b]

noShrink :: a -> b

killAbs :: KillVar a => Abs a -> a

class KillVar a where

Methods

killVar :: Nat -> a -> a

Instances

prop_wellScopedVars :: TermConfiguration -> Property

Check that the generated terms don't have any out of scope variables.