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
- 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
- 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 | |
|
data Frequencies Source #
data UseLiterals Source #
UseLit | |
|
fixSizeConf :: Int -> TermConfiguration -> TermConfiguration Source #
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 # | |
genConf :: Gen TermConfiguration Source #
Only generates default configurations. Names and free variables varies.
class ShrinkC a b | a -> b where 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 # | |
class KillVar a where 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.