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

Agda.TypeChecking.Test.Generators

Synopsis

Documentation

data TermConfiguration Source

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 Source

Constructors

TermFreqs 

Fields

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

Instances

data NameFreqs Source

Constructors

NameFreqs 

Fields

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

Instances

data HiddenFreqs Source

Constructors

HiddenFreqs 

Instances

data SortFreqs Source

Constructors

SortFreqs 

Fields

setFreqs :: [Int]
 
propFreq :: Int
 

Instances

class GenC a whereSource

Instances

newtype YesType a Source

Constructors

YesType 

Fields

unYesType :: a
 

Instances

ShrinkC a b => ShrinkC (YesType a) b 

newtype NoType a Source

Constructors

NoType 

Fields

unNoType :: a
 

Instances

ShrinkC a b => ShrinkC (NoType a) b 

newtype VarName Source

Constructors

VarName 

Fields

unVarName :: Nat
 

Instances

newtype DefName Source

Constructors

DefName 

Fields

unDefName :: QName
 

Instances

newtype ConName Source

Constructors

ConName 

Fields

unConName :: QName
 

Instances

newtype SizedList a Source

Constructors

SizedList 

Fields

unSizedList :: [a]
 

Instances

GenC a => GenC (SizedList a) 

genConf :: Gen TermConfigurationSource

Only generates default configurations. Names and free variables varies.

class ShrinkC a b | a -> b whereSource

Methods

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

noShrink :: a -> bSource

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

class KillVar a whereSource

Methods

killVar :: Nat -> a -> aSource

Instances

prop_wellScopedVars :: TermConfiguration -> PropertySource

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