Agda.TypeChecking.Test.Generators

Documentation

data TermConfiguration

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

Methods

showsPrec :: Int -> TermConfiguration -> ShowS

show :: TermConfiguration -> String

showList :: [TermConfiguration] -> ShowS

Arbitrary TermConfiguration

Methods

arbitrary :: Gen TermConfiguration

shrink :: TermConfiguration -> [TermConfiguration]

data Frequencies

Constructors

Freqs

Fields

• hiddenFreqs :: HiddenFreqs
• elimFreqs :: ElimFreqs
• sortFreqs :: SortFreqs
• termFreqs :: TermFreqs

Instances

Show Frequencies

Methods

showsPrec :: Int -> Frequencies -> ShowS

show :: Frequencies -> String

showList :: [Frequencies] -> ShowS

data TermFreqs

Constructors

TermFreqs

Fields

• varFreq :: Int
• defFreq :: Int
• conFreq :: Int
• litFreq :: Int
• sortFreq :: Int
• lamFreq :: Int
• piFreq :: Int
• funFreq :: Int

Instances

Show TermFreqs

Methods

showsPrec :: Int -> TermFreqs -> ShowS

show :: TermFreqs -> String

showList :: [TermFreqs] -> ShowS

data ElimFreqs

Constructors

ElimFreqs

Fields

• applyFreq :: Int
• projFreq :: Int

Instances

Show ElimFreqs

Methods

showsPrec :: Int -> ElimFreqs -> ShowS

show :: ElimFreqs -> String

showList :: [ElimFreqs] -> ShowS

data HiddenFreqs

Constructors

HiddenFreqs

Fields

• hiddenFreq :: Int
• notHiddenFreq :: Int

Instances

Show HiddenFreqs

Methods

showsPrec :: Int -> HiddenFreqs -> ShowS

show :: HiddenFreqs -> String

showList :: [HiddenFreqs] -> ShowS

data SortFreqs

Constructors

SortFreqs

Fields

• setFreqs :: [Int]
• propFreq :: Int

Instances

Show SortFreqs

Methods

showsPrec :: Int -> SortFreqs -> ShowS

show :: SortFreqs -> String

showList :: [SortFreqs] -> ShowS

defaultFrequencies :: Frequencies

noProp :: TermConfiguration -> TermConfiguration

data UseLiterals

Constructors

UseLit

Fields

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

Instances

Show UseLiterals

Methods

showsPrec :: Int -> UseLiterals -> ShowS

show :: UseLiterals -> String

showList :: [UseLiterals] -> ShowS

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

class GenC a where

Minimal complete definition

genC

Methods

genC :: TermConfiguration -> Gen a

Instances

GenC Char

Methods

genC :: TermConfiguration -> Gen Char

GenC Double

Methods

genC :: TermConfiguration -> Gen Double

GenC Integer

Methods

genC :: TermConfiguration -> Gen Integer

GenC Range

Methods

genC :: TermConfiguration -> Gen Range

GenC Hiding

Methods

genC :: TermConfiguration -> Gen Hiding

GenC Literal

Methods

genC :: TermConfiguration -> Gen Literal

GenC Sort

Methods

genC :: TermConfiguration -> Gen Sort

GenC Telescope

Methods

genC :: TermConfiguration -> Gen Telescope

GenC Type

Methods

genC :: TermConfiguration -> Gen Type

GenC Term

Methods

genC :: TermConfiguration -> Gen Term

GenC ProjName

Methods

genC :: TermConfiguration -> Gen ProjName

GenC DefName

Methods

genC :: TermConfiguration -> Gen DefName

GenC a => GenC [a]

Methods

genC :: TermConfiguration -> Gen [a]

GenC a => GenC (Dom a)

Methods

genC :: TermConfiguration -> Gen (Dom a)

GenC a => GenC (Arg a)

Methods

genC :: TermConfiguration -> Gen (Arg a)

GenC a => GenC (Abs a)

Methods

genC :: TermConfiguration -> Gen (Abs a)

GenC a => GenC (Elim' a)

Methods

genC :: TermConfiguration -> Gen (Elim' a)

GenC a => GenC (SizedList a)

Methods

genC :: TermConfiguration -> Gen (SizedList a)

(GenC a, GenC b) => GenC (a, b)

Methods

genC :: TermConfiguration -> Gen (a, b)

newtype YesType a

Constructors

YesType

Fields

• unYesType :: a

Instances

ShrinkC a b => ShrinkC (YesType a) b

Methods

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

noShrink :: YesType a -> b

newtype NoType a

Constructors

NoType

Fields

• unNoType :: a

Instances

ShrinkC a b => ShrinkC (NoType a) b

Methods

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

noShrink :: NoType a -> b

newtype VarName

Constructors

VarName

Fields

• unVarName :: Nat

Instances

ShrinkC VarName Nat

Methods

shrinkC :: TermConfiguration -> VarName -> [Nat]

noShrink :: VarName -> Nat

newtype DefName

Constructors

DefName

Fields

• unDefName :: QName

Instances

GenC DefName

Methods

genC :: TermConfiguration -> Gen DefName

ShrinkC DefName QName

Methods

shrinkC :: TermConfiguration -> DefName -> [QName]

noShrink :: DefName -> QName

newtype ConName

Constructors

ConName

Fields

• unConName :: ConHead

Instances

ShrinkC ConName ConHead

Methods

shrinkC :: TermConfiguration -> ConName -> [ConHead]

noShrink :: ConName -> ConHead

newtype ProjName

Constructors

ProjName

Fields

• unProjName :: QName

Instances

GenC ProjName

Methods

genC :: TermConfiguration -> Gen ProjName

newtype SizedList a

Constructors

SizedList

Fields

• unSizedList :: [a]

Instances

GenC a => GenC (SizedList a)

Methods

genC :: TermConfiguration -> Gen (SizedList a)

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

genArgs :: TermConfiguration -> Gen Args

genElims :: TermConfiguration -> Gen Elims

genConf :: Gen TermConfiguration

Only generates default configurations. Names and free variables varies.

class ShrinkC a b | a -> b where

Minimal complete definition

shrinkC, noShrink

Methods

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

noShrink :: a -> b

Instances

ShrinkC Char Char

Methods

shrinkC :: TermConfiguration -> Char -> [Char]

noShrink :: Char -> Char

ShrinkC Hiding Hiding

Methods

shrinkC :: TermConfiguration -> Hiding -> [Hiding]

noShrink :: Hiding -> Hiding

ShrinkC Literal Literal

Methods

shrinkC :: TermConfiguration -> Literal -> [Literal]

noShrink :: Literal -> Literal

ShrinkC Sort Sort

Methods

shrinkC :: TermConfiguration -> Sort -> [Sort]

noShrink :: Sort -> Sort

ShrinkC Telescope Telescope

Methods

shrinkC :: TermConfiguration -> Telescope -> [Telescope]

noShrink :: Telescope -> Telescope

ShrinkC Type Type

Methods

shrinkC :: TermConfiguration -> Type -> [Type]

noShrink :: Type -> Type

ShrinkC Term Term

Methods

shrinkC :: TermConfiguration -> Term -> [Term]

noShrink :: Term -> Term

ShrinkC ConName ConHead

Methods

shrinkC :: TermConfiguration -> ConName -> [ConHead]

noShrink :: ConName -> ConHead

ShrinkC DefName QName

Methods

shrinkC :: TermConfiguration -> DefName -> [QName]

noShrink :: DefName -> QName

ShrinkC VarName Nat

Methods

shrinkC :: TermConfiguration -> VarName -> [Nat]

noShrink :: VarName -> Nat

ShrinkC a b => ShrinkC (NoType a) b

Methods

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

noShrink :: NoType a -> b

ShrinkC a b => ShrinkC (YesType a) b

Methods

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

noShrink :: YesType a -> b

ShrinkC a b => ShrinkC [a] [b]

Methods

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

noShrink :: [a] -> [b]

ShrinkC a b => ShrinkC (Dom a) (Dom b)

Methods

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

noShrink :: Dom a -> Dom b

ShrinkC a b => ShrinkC (Arg a) (Arg b)

Methods

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

noShrink :: Arg a -> Arg b

ShrinkC a b => ShrinkC (Blocked a) (Blocked b)

Methods

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

noShrink :: Blocked a -> Blocked b

ShrinkC a b => ShrinkC (Abs a) (Abs b)

Methods

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

noShrink :: Abs a -> Abs b

ShrinkC a b => ShrinkC (Elim' a) (Elim' b)

Methods

shrinkC :: TermConfiguration -> Elim' a -> [Elim' b]

noShrink :: Elim' a -> Elim' b

(ShrinkC a a', ShrinkC b b') => ShrinkC (a, b) (a', b')

Methods

shrinkC :: TermConfiguration -> (a, b) -> [(a', b')]

noShrink :: (a, b) -> (a', b')

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

class KillVar a where

Minimal complete definition

killVar

Methods

killVar :: Nat -> a -> a

Instances

KillVar Telescope

Methods

killVar :: Nat -> Telescope -> Telescope

KillVar Type

Methods

killVar :: Nat -> Type -> Type

KillVar Term

Methods

killVar :: Nat -> Term -> Term

KillVar a => KillVar [a]

Methods

killVar :: Nat -> [a] -> [a]

KillVar a => KillVar (Maybe a)

Methods

killVar :: Nat -> Maybe a -> Maybe a

KillVar a => KillVar (Dom a)

Methods

killVar :: Nat -> Dom a -> Dom a

KillVar a => KillVar (Arg a)

Methods

killVar :: Nat -> Arg a -> Arg a

KillVar a => KillVar (Abs a)

Methods

killVar :: Nat -> Abs a -> Abs a

KillVar a => KillVar (Elim' a)

Methods

killVar :: Nat -> Elim' a -> Elim' a

(KillVar a, KillVar b) => KillVar (a, b)

Methods

killVar :: Nat -> (a, b) -> (a, b)

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

prop_wellScopedVars :: TermConfiguration -> Property

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