Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

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

Constructors

TermConf |

Fields

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 `size` parameter.

tcIsType :: Bool

  When this is true no lambdas, literals, or constructors are generated

Instances

Show TermConfiguration |
Arbitrary TermConfiguration |

data Frequencies

Constructors

Freqs |

Fields

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

Instances

Show Frequencies |

data TermFreqs

Constructors

TermFreqs |

Fields

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

Instances

Show TermFreqs |

data NameFreqs

Constructors

NameFreqs |

Fields

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

Instances

Show NameFreqs |

data HiddenFreqs

Constructors

HiddenFreqs |

Fields

hiddenFreq :: Int
notHiddenFreq :: Int

Instances

Show HiddenFreqs |

data SortFreqs

Constructors

SortFreqs |

Fields

setFreqs :: [Int]
propFreq :: Int

Instances

Show SortFreqs |

defaultFrequencies :: Frequencies

noProp :: TermConfiguration -> TermConfiguration

data UseLiterals

Constructors

UseLit |

Fields

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

Instances

Show UseLiterals |

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

Methods

genC :: TermConfiguration -> Gen a

Instances

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

newtype YesType a

Constructors

YesType |

Fields

unYesType :: a

Instances

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

newtype NoType a

Constructors

NoType |

Fields

unNoType :: a

Instances

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

newtype VarName

Constructors

VarName |

Fields

unVarName :: Nat

Instances

ShrinkC VarName Nat |

newtype DefName

Constructors

DefName |

Fields

unDefName :: QName

Instances

ShrinkC DefName QName |

newtype ConName

Constructors

ConName |

Fields

unConName :: QName

Instances

ShrinkC ConName QName |

newtype SizedList a

Constructors

SizedList |

Fields

unSizedList :: [a]

Instances

GenC a => GenC (SizedList a) |

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

genArgs :: TermConfiguration -> Gen Args

genConf :: Gen TermConfiguration

Only generates default configurations. Names and free variables varies.

class ShrinkC a b | a -> b where

Methods

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

noShrink :: a -> b

Instances

ShrinkC Char Char |
ShrinkC Hiding Hiding |
ShrinkC Literal Literal |
ShrinkC Sort Sort |
ShrinkC Telescope Telescope |
ShrinkC Type Type |
ShrinkC Term Term |
ShrinkC ConName QName |
ShrinkC DefName QName |
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 (Dom a) (Dom b) |
ShrinkC a b => ShrinkC (Blocked a) (Blocked b) |
ShrinkC a b => ShrinkC (Abs a) (Abs b) |
(ShrinkC a a', ShrinkC b b') => ShrinkC (a, b) (a', b') |

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

class KillVar a where

Methods

killVar :: Nat -> a -> a

Instances

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

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

prop_wellScopedVars :: TermConfiguration -> Property

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