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

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 :: Frequencies Source

noProp :: TermConfiguration -> TermConfiguration Source

data UseLiterals Source

Constructors UseLit useLitInt :: Bool useLitFloat :: Bool useLitString :: Bool useLitChar :: Bool

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

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 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

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

class KillVar a where Source

Methods killVar :: Nat -> a -> a Source

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.6.0