Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 IntMaximum size of the generated element. When Nothing this value is initialized from the Test.QuickCheck.size parameter.
tcIsType :: BoolWhen this is true no lambdas, literals, or constructors are generated
data Frequencies Source
Constructors
Freqs
hiddenFreqs :: HiddenFreqs
nameFreqs :: NameFreqs
sortFreqs :: SortFreqs
termFreqs :: TermFreqs
data TermFreqs Source
Constructors
TermFreqs
nameFreq :: Int
litFreq :: Int
sortFreq :: Int
lamFreq :: Int
piFreq :: Int
funFreq :: Int
data NameFreqs Source
Constructors
NameFreqs
varFreq :: Int
defFreq :: Int
conFreq :: Int
data HiddenFreqs Source
Constructors
HiddenFreqs
hiddenFreq :: Int
notHiddenFreq :: Int
data SortFreqs Source
Constructors
SortFreqs
setFreqs :: [Int]
propFreq :: Int
defaultFrequencies :: FrequenciesSource
noProp :: TermConfiguration -> TermConfigurationSource
data UseLiterals Source
Constructors
UseLit
useLitInt :: Bool
useLitFloat :: Bool
useLitString :: Bool
useLitChar :: Bool
noLiterals :: UseLiteralsSource
fixSizeConf :: Int -> TermConfiguration -> TermConfigurationSource
resizeConf :: (Int -> Int) -> TermConfiguration -> TermConfigurationSource
decrConf :: TermConfiguration -> TermConfigurationSource
divConf :: TermConfiguration -> Int -> TermConfigurationSource
isTypeConf :: TermConfiguration -> TermConfigurationSource
isntTypeConf :: TermConfiguration -> TermConfigurationSource
extendConf :: TermConfiguration -> TermConfigurationSource
extendWithTelConf :: Telescope -> TermConfiguration -> TermConfigurationSource
makeConfiguration :: [String] -> [String] -> [Nat] -> TermConfigurationSource
class GenC a whereSource
Methods
genC :: TermConfiguration -> Gen aSource
newtype YesType a Source
Constructors
YesType
unYesType :: a
newtype NoType a Source
Constructors
NoType
unNoType :: a
newtype VarName Source
Constructors
VarName
unVarName :: Nat
newtype DefName Source
Constructors
DefName
unDefName :: QName
newtype ConName Source
Constructors
ConName
unConName :: QName
newtype SizedList a Source
Constructors
SizedList
unSizedList :: [a]
fixSize :: TermConfiguration -> Gen a -> Gen aSource
genArgs :: TermConfiguration -> Gen ArgsSource
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
isWellScoped :: Free a => TermConfiguration -> a -> BoolSource
prop_wellScopedVars :: TermConfiguration -> PropertySource
Check that the generated terms don't have any out of scope variables.
Produced by Haddock version 2.6.1