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 :: FreeVS a => TermConfiguration -> a -> Bool
- prop_wellScopedVars :: TermConfiguration -> Property
Documentation
data TermConfiguration Source
TermConf | |
|
Show TermConfiguration Source | |
Arbitrary TermConfiguration Source |
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 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 (Dom a) Source | |
GenC a => GenC (Arg 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 |
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 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 (Dom a) (Dom b) Source | |
ShrinkC a b => ShrinkC (Arg a) (Arg 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 a', ShrinkC b b') => ShrinkC (a, b) (a', b') Source |
KillVar Telescope Source | |
KillVar Type Source | |
KillVar Term Source | |
KillVar a => KillVar [a] Source | |
KillVar a => KillVar (Maybe a) Source | |
KillVar a => KillVar (Dom a) Source | |
KillVar a => KillVar (Arg a) Source | |
KillVar a => KillVar (Abs a) Source | |
KillVar a => KillVar (Elim' 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.