| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Test.Generators

Synopsis

data TermConfiguration = TermConf {

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

}

data Frequencies = Freqs {

hiddenFreqs :: HiddenFreqs
nameFreqs :: NameFreqs
sortFreqs :: SortFreqs
termFreqs :: TermFreqs

}

data TermFreqs = TermFreqs {

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

}

data NameFreqs = NameFreqs {

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

}

data HiddenFreqs = HiddenFreqs {

hiddenFreq :: Int
notHiddenFreq :: Int

}

data SortFreqs = SortFreqs {

setFreqs :: [Int]
propFreq :: Int

}

defaultFrequencies :: Frequencies
noProp :: TermConfiguration -> TermConfiguration

data UseLiterals = UseLit {

useLitInt :: Bool
useLitFloat :: Bool
useLitString :: Bool
useLitChar :: Bool

}

noLiterals :: UseLiterals
fixSizeConf :: Int -> TermConfiguration -> TermConfiguration
resizeConf :: (Int -> Int) -> TermConfiguration -> TermConfiguration
decrConf :: TermConfiguration -> TermConfiguration
divConf :: TermConfiguration -> Int -> TermConfiguration
isTypeConf :: TermConfiguration -> TermConfiguration
isntTypeConf :: TermConfiguration -> TermConfiguration
extendConf :: TermConfiguration -> TermConfiguration
extendWithTelConf :: Telescope -> TermConfiguration -> TermConfiguration
makeConfiguration :: [String] -> [String] -> [Nat] -> TermConfiguration
class GenC a where

genC :: TermConfiguration -> Gen a

newtype YesType a = YesType {

unYesType :: a

}

newtype NoType a = NoType {

unNoType :: a

}

newtype VarName = VarName {

unVarName :: Nat

}

newtype DefName = DefName {

unDefName :: QName

}

newtype ConName = ConName {

unConName :: QName

}

newtype SizedList a = SizedList {

unSizedList :: [a]

}

fixSize :: TermConfiguration -> Gen a -> Gen a
genArgs :: TermConfiguration -> Gen Args
genConf :: Gen TermConfiguration
class ShrinkC a b | a -> b where

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

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

killVar :: Nat -> a -> a

isWellScoped :: Free a => TermConfiguration -> a -> Bool
prop_wellScopedVars :: TermConfiguration -> Property

Documentation

data TermConfiguration | Source

Constructors

TermConf |

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

Instances

Show TermConfiguration
Arbitrary TermConfiguration

data Frequencies | Source

Constructors

Freqs |

hiddenFreqs :: HiddenFreqs |
nameFreqs :: NameFreqs |
sortFreqs :: SortFreqs |
termFreqs :: TermFreqs |

Instances

Show Frequencies

data TermFreqs | Source

Constructors

TermFreqs |

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

Instances

Show TermFreqs

data NameFreqs | Source

Constructors

NameFreqs |

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

Instances

Show NameFreqs

data HiddenFreqs | Source

Constructors

HiddenFreqs |

hiddenFreq :: Int |
notHiddenFreq :: Int |

Instances

Show HiddenFreqs

data SortFreqs | Source

Constructors

SortFreqs |

setFreqs :: [Int] |
propFreq :: Int |

Instances

Show SortFreqs

defaultFrequencies :: Frequencies | Source

noProp :: TermConfiguration -> TermConfiguration | Source

data UseLiterals | Source

Constructors

UseLit |

useLitInt :: Bool |
useLitFloat :: Bool |
useLitString :: Bool |
useLitChar :: Bool |

Instances

Show UseLiterals

noLiterals :: UseLiterals | Source

fixSizeConf :: Int -> TermConfiguration -> TermConfiguration | Source

resizeConf :: (Int -> Int) -> TermConfiguration -> TermConfiguration | Source

decrConf :: TermConfiguration -> TermConfiguration | Source

divConf :: TermConfiguration -> Int -> TermConfiguration | Source

isTypeConf :: TermConfiguration -> TermConfiguration | Source

isntTypeConf :: TermConfiguration -> TermConfiguration | Source

extendConf :: TermConfiguration -> TermConfiguration | Source

extendWithTelConf :: Telescope -> TermConfiguration -> TermConfiguration | Source

makeConfiguration :: [String] -> [String] -> [Nat] -> TermConfiguration | Source

class GenC a where | Source

Methods

genC :: TermConfiguration -> Gen a | Source

Instances

GenC Char
GenC Double
GenC Integer
GenC Range
GenC Literal
GenC Hiding
GenC Telescope
GenC Sort
GenC Type
GenC Term
GenC a => GenC ([] a)
GenC a => GenC (Arg a)
GenC a => GenC (Abs a)
GenC a => GenC (SizedList a)
(GenC a, GenC b) => GenC ((,) a b)

newtype YesType a | Source

Constructors

YesType |

unYesType :: a |

Instances

ShrinkC a b => ShrinkC (YesType a) b

newtype NoType a | Source

Constructors

NoType |

unNoType :: a |

Instances

ShrinkC a b => ShrinkC (NoType a) b

newtype VarName | Source

Constructors

VarName |

unVarName :: Nat |

Instances

ShrinkC VarName Nat

newtype DefName | Source

Constructors

DefName |

unDefName :: QName |

Instances

ShrinkC DefName QName

newtype ConName | Source

Constructors

ConName |

unConName :: QName |

Instances

ShrinkC ConName QName

newtype SizedList a | Source

Constructors

SizedList |

unSizedList :: [a] |

Instances

GenC a => GenC (SizedList a)

fixSize :: TermConfiguration -> Gen a -> Gen a | Source

genArgs :: TermConfiguration -> Gen Args | Source

genConf :: Gen TermConfiguration | Source

Only generates default configurations. Names and free variables varies.

class ShrinkC a b | a -> b where | Source

Methods

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

noShrink :: a -> b | Source

Instances

ShrinkC Char Char
ShrinkC Literal Literal
ShrinkC Hiding Hiding
ShrinkC Telescope Telescope
ShrinkC Sort Sort
ShrinkC Type Type
ShrinkC Term Term
ShrinkC ConName QName
ShrinkC ConName QName
ShrinkC DefName QName
ShrinkC DefName QName
ShrinkC VarName Nat
ShrinkC VarName Nat
ShrinkC a b => ShrinkC (NoType a) b
ShrinkC a b => ShrinkC (YesType a) b
ShrinkC a b => ShrinkC ([] a) ([] b)
ShrinkC a b => ShrinkC (Arg a) (Arg b)
ShrinkC a b => ShrinkC (Abs a) (Abs b)
ShrinkC a b => ShrinkC (Blocked a) (Blocked b)
(ShrinkC a a', ShrinkC b b') => ShrinkC ((,) a b) ((,) a' b')

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

class KillVar a where | Source

Methods

killVar :: Nat -> a -> a | Source

Instances

KillVar Telescope
KillVar Type
KillVar Term
KillVar a => KillVar ([] a)
KillVar a => KillVar (Arg a)
KillVar a => KillVar (Abs a)
(KillVar a, KillVar b) => KillVar ((,) a b)

isWellScoped :: Free a => TermConfiguration -> a -> Bool | Source

prop_wellScopedVars :: TermConfiguration -> Property | Source

Check that the generated terms don't have any out of scope variables.
Produced by Haddock version 2.4.2