Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.Test.Generators

Synopsis

Documentation

data TermConfiguration Source

Constructors

TermConf
Fields tcDefinedNames :: [QName] tcConstructorNames :: [QName] tcProjectionNames :: [QName] tcFreeVariables :: [Nat] tcLiterals :: UseLiterals tcFrequencies :: Frequencies tcFixSize :: Maybe Int Maximum size of the generated element. When `Nothing` this value is initialized from the `size` parameter. tcIsType :: Bool When this is true no lambdas, literals, or constructors are generated

Instances

Show TermConfiguration Source
Arbitrary TermConfiguration Source

data Frequencies Source

Constructors

Freqs
Fields hiddenFreqs :: HiddenFreqs elimFreqs :: ElimFreqs sortFreqs :: SortFreqs termFreqs :: TermFreqs

Instances

Show Frequencies Source

data TermFreqs Source

Constructors

TermFreqs
Fields varFreq :: Int defFreq :: Int conFreq :: Int litFreq :: Int sortFreq :: Int lamFreq :: Int piFreq :: Int funFreq :: Int

Instances

Show TermFreqs Source

data ElimFreqs Source

Constructors

ElimFreqs
Fields applyFreq :: Int projFreq :: Int

Instances

Show ElimFreqs Source

data HiddenFreqs Source

Constructors

HiddenFreqs
Fields hiddenFreq :: Int notHiddenFreq :: Int

Instances

Show HiddenFreqs Source

data SortFreqs Source

Constructors

SortFreqs
Fields setFreqs :: [Int] propFreq :: Int

Instances

Show SortFreqs Source

defaultFrequencies :: Frequencies Source

noProp :: TermConfiguration -> TermConfiguration Source

data UseLiterals Source

Constructors

UseLit
Fields useLitInt :: Bool useLitFloat :: Bool useLitString :: Bool useLitChar :: Bool

Instances

Show UseLiterals Source

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 :: [RawName] -> [RawName] -> [RawName] -> [Nat] -> TermConfiguration Source

class GenC a where Source

Methods

genC :: TermConfiguration -> Gen a Source

Instances

GenC Char Source
GenC Double Source
GenC Integer Source
GenC Range Source
GenC Hiding Source
GenC Literal Source
GenC Sort Source
GenC Telescope Source
GenC Type Source
GenC Term Source
GenC ProjName Source
GenC DefName Source
GenC a => GenC [a] Source
GenC a => GenC (Abs a) Source
GenC a => GenC (Elim' a) Source
GenC a => GenC (SizedList a) Source
(GenC a, GenC b) => GenC (a, b) Source
(GenC c, GenC a) => GenC (Dom c a) Source
(GenC c, GenC a) => GenC (Arg c a) Source

newtype YesType a Source

Constructors

YesType
Fields unYesType :: a

Instances

ShrinkC a b => ShrinkC (YesType a) b Source

newtype NoType a Source

Constructors

NoType
Fields unNoType :: a

Instances

ShrinkC a b => ShrinkC (NoType a) b Source

newtype VarName Source

Constructors

VarName
Fields unVarName :: Nat

Instances

ShrinkC VarName Nat Source

newtype DefName Source

Constructors

DefName
Fields unDefName :: QName

Instances

GenC DefName Source
ShrinkC DefName QName Source

newtype ConName Source

Constructors

ConName
Fields unConName :: ConHead

Instances

ShrinkC ConName ConHead Source

newtype ProjName Source

Constructors

ProjName
Fields unProjName :: QName

Instances

GenC ProjName Source

newtype SizedList a Source

Constructors

SizedList
Fields unSizedList :: [a]

Instances

GenC a => GenC (SizedList a) Source

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

genArgs :: TermConfiguration -> Gen Args Source

genElims :: TermConfiguration -> Gen Elims 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 Source
ShrinkC Hiding Hiding Source
ShrinkC Literal Literal Source
ShrinkC Sort Sort Source
ShrinkC Telescope Telescope Source
ShrinkC Type Type Source
ShrinkC Term Term Source
ShrinkC ConName ConHead Source
ShrinkC DefName QName Source
ShrinkC VarName Nat Source
ShrinkC a b => ShrinkC (NoType a) b Source
ShrinkC a b => ShrinkC (YesType a) b Source
ShrinkC a b => ShrinkC [a] [b] Source
ShrinkC a b => ShrinkC (Blocked a) (Blocked b) Source
ShrinkC a b => ShrinkC (Abs a) (Abs b) Source
ShrinkC a b => ShrinkC (Elim' a) (Elim' b) Source
ShrinkC a b => ShrinkC (Dom a) (Dom b) Source
ShrinkC a b => ShrinkC (Arg a) (Arg b) Source
(ShrinkC a a', ShrinkC b b') => ShrinkC (a, b) (a', b') Source

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

class KillVar a where Source

Methods

killVar :: Nat -> a -> a Source

Instances

KillVar Telescope Source
KillVar Type Source
KillVar Term Source
KillVar a => KillVar [a] Source
KillVar a => KillVar (Maybe a) Source
KillVar a => KillVar (Abs a) Source
KillVar a => KillVar (Elim' a) Source
KillVar a => KillVar (Dom a) Source
KillVar a => KillVar (Arg a) Source
(KillVar a, KillVar b) => KillVar (a, b) Source

isWellScoped :: FreeVS a => TermConfiguration -> a -> Bool Source

prop_wellScopedVars :: TermConfiguration -> Property Source

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