Copyright | (c) Kristina Sojakova DFKI Bremen 2009 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | k.sojakova@jacobs-university.de |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe |
DFOL.AS_DFOL
Description
Documentation
data BASIC_SPEC Source #
Constructors
Basic_spec [Annoted BASIC_ITEM] |
Instances
data BASIC_ITEM Source #
Constructors
Decl_item DECL | |
Axiom_item FORMULA |
Instances
Show BASIC_ITEM Source # | |
Methods showsPrec :: Int -> BASIC_ITEM -> ShowS show :: BASIC_ITEM -> String showList :: [BASIC_ITEM] -> ShowS | |
Pretty BASIC_ITEM Source # | |
Instances
Eq TYPE Source # | |
Data TYPE Source # | |
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TYPE -> c TYPE gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TYPE dataTypeOf :: TYPE -> DataType dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c TYPE) dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TYPE) gmapT :: (forall b. Data b => b -> b) -> TYPE -> TYPE gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TYPE -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TYPE -> r gmapQ :: (forall d. Data d => d -> u) -> TYPE -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TYPE -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TYPE -> m TYPE gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TYPE -> m TYPE gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TYPE -> m TYPE | |
Ord TYPE Source # | |
Show TYPE Source # | |
Pretty TYPE Source # | |
Translatable TYPE Source # | |
Constructors
Identifier NAME | |
Appl TERM [TERM] |
Instances
Eq TERM Source # | |
Data TERM Source # | |
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TERM -> c TERM gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TERM dataTypeOf :: TERM -> DataType dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c TERM) dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TERM) gmapT :: (forall b. Data b => b -> b) -> TERM -> TERM gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TERM -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TERM -> r gmapQ :: (forall d. Data d => d -> u) -> TERM -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TERM -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TERM -> m TERM gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TERM -> m TERM gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TERM -> m TERM | |
Ord TERM Source # | |
Show TERM Source # | |
Pretty TERM Source # | |
Translatable TERM Source # | |
Constructors
T | |
F | |
Pred TERM | |
Equality TERM TERM | |
Negation FORMULA | |
Conjunction [FORMULA] | |
Disjunction [FORMULA] | |
Implication FORMULA FORMULA | |
Equivalence FORMULA FORMULA | |
Forall [DECL] FORMULA | |
Exists [DECL] FORMULA |
Instances
data SYMB_ITEMS Source #
Constructors
Symb_items [SYMB] |
Instances
data SYMB_MAP_ITEMS Source #
Constructors
Symb_map_items [SYMB_OR_MAP] |
Instances
data SYMB_OR_MAP Source #
Instances
Eq SYMB_OR_MAP Source # | |
Data SYMB_OR_MAP Source # | |
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB_OR_MAP -> c SYMB_OR_MAP gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMB_OR_MAP toConstr :: SYMB_OR_MAP -> Constr dataTypeOf :: SYMB_OR_MAP -> DataType dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SYMB_OR_MAP) dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_OR_MAP) gmapT :: (forall b. Data b => b -> b) -> SYMB_OR_MAP -> SYMB_OR_MAP gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_OR_MAP -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_OR_MAP -> r gmapQ :: (forall d. Data d => d -> u) -> SYMB_OR_MAP -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_OR_MAP -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP | |
Show SYMB_OR_MAP Source # | |
Methods showsPrec :: Int -> SYMB_OR_MAP -> ShowS show :: SYMB_OR_MAP -> String showList :: [SYMB_OR_MAP] -> ShowS | |
Pretty SYMB_OR_MAP Source # | |
termRecForm :: TERM -> TERM Source #
typeRecForm :: TYPE -> TYPE Source #
typeFlatForm :: TYPE -> TYPE Source #
formulaRecForm :: FORMULA -> FORMULA Source #
formulaFlatForm :: FORMULA -> FORMULA Source #
printNames :: [NAME] -> Doc Source #
printDecls :: [DECL] -> Doc Source #
getVarsFromDecls :: [DECL] -> [NAME] Source #
compactDecls :: [DECL] -> [DECL] Source #
expandDecls :: [DECL] -> [SDECL] Source #
class Translatable a where Source #
Minimal complete definition
Instances
getFreeVars :: TYPE -> Set NAME Source #