Safe Haskell | None |
---|---|
Language | Haskell98 |
- data TermConfiguration = TermConf {
- tcDefinedNames :: [QName]
- tcConstructorNames :: [QName]
- tcProjectionNames :: [QName]
- tcFreeVariables :: [Nat]
- tcLiterals :: UseLiterals
- tcFrequencies :: Frequencies
- tcFixSize :: Maybe Int
- tcIsType :: Bool
- data Frequencies = Freqs {}
- data TermFreqs = TermFreqs {}
- data ElimFreqs = ElimFreqs {}
- data HiddenFreqs = HiddenFreqs {
- hiddenFreq :: Int
- notHiddenFreq :: Int
- data SortFreqs = SortFreqs {}
- 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 :: [RawName] -> [RawName] -> [RawName] -> [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 {}
- newtype DefName = DefName {}
- newtype ConName = ConName {}
- newtype ProjName = ProjName {
- unProjName :: QName
- newtype SizedList a = SizedList {
- unSizedList :: [a]
- fixSize :: TermConfiguration -> Gen a -> Gen a
- genArgs :: TermConfiguration -> Gen Args
- genElims :: TermConfiguration -> Gen Elims
- 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
- isWellScoped :: Free a => TermConfiguration -> a -> Bool
- prop_wellScopedVars :: TermConfiguration -> Property
Documentation
data TermConfiguration Source
TermConf | |
|
data Frequencies Source
data UseLiterals Source
UseLit | |
|
resizeConf :: (Int -> Int) -> TermConfiguration -> TermConfiguration Source
divConf :: TermConfiguration -> Int -> TermConfiguration Source
makeConfiguration :: [RawName] -> [RawName] -> [RawName] -> [Nat] -> TermConfiguration Source
genC :: TermConfiguration -> Gen a Source
GenC Char | |
GenC Double | |
GenC Integer | |
GenC Range | |
GenC Hiding | |
GenC Literal | |
GenC Sort | |
GenC Telescope | |
GenC Type | |
GenC Term | |
GenC ProjName | |
GenC DefName | |
GenC a => GenC [a] | |
GenC a => GenC (Abs a) | |
GenC a => GenC (Elim' a) | |
GenC a => GenC (SizedList a) | |
(GenC a, GenC b) => GenC (a, b) | |
(GenC c, GenC a) => GenC (Dom c a) | |
(GenC c, GenC a) => GenC (Arg c a) |
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
shrinkC :: TermConfiguration -> a -> [b] Source
ShrinkC Char Char | |
ShrinkC Hiding Hiding | |
ShrinkC Literal Literal | |
ShrinkC Sort Sort | |
ShrinkC Telescope Telescope | |
ShrinkC Type Type | |
ShrinkC Term Term | |
ShrinkC ConName ConHead | |
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 (Blocked a) (Blocked b) | |
ShrinkC a b => ShrinkC (Abs a) (Abs b) | |
ShrinkC a b => ShrinkC (Elim' a) (Elim' b) | |
ShrinkC a b => ShrinkC (Dom a) (Dom b) | |
ShrinkC a b => ShrinkC (Arg a) (Arg b) | |
(ShrinkC a a', ShrinkC b b') => ShrinkC (a, b) (a', b') |
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.