Copyright | (c) Dominik Luecke Uni Bremen 2007 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | luecke@informatik.uni-bremen.de |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe |
Propositional.AS_BASIC_Propositional
Description
Definition of abstract syntax for propositional logic
Synopsis
- data FORMULA
- data BASIC_ITEMS
- newtype BASIC_SPEC = Basic_spec [Annoted BASIC_ITEMS]
- data SYMB_ITEMS = Symb_items [SYMB] Range
- newtype SYMB = Symb_id Token
- data SYMB_MAP_ITEMS = Symb_map_items [SYMB_OR_MAP] Range
- data SYMB_OR_MAP
- data PRED_ITEM = Pred_item [Token] Range
- isPrimForm :: FORMULA -> Bool
Documentation
Datatype for propositional formulas
Constructors
False_atom Range | |
True_atom Range | |
Predication Token | |
Negation FORMULA Range | |
Conjunction [FORMULA] Range | |
Disjunction [FORMULA] Range | |
Implication FORMULA FORMULA Range | |
Equivalence FORMULA FORMULA Range |
Instances
data BASIC_ITEMS Source #
Constructors
Pred_decl PRED_ITEM | |
Axiom_items [Annoted FORMULA] |
Instances
Data BASIC_ITEMS Source # | |
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BASIC_ITEMS -> c BASIC_ITEMS gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BASIC_ITEMS toConstr :: BASIC_ITEMS -> Constr dataTypeOf :: BASIC_ITEMS -> DataType dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c BASIC_ITEMS) dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASIC_ITEMS) gmapT :: (forall b. Data b => b -> b) -> BASIC_ITEMS -> BASIC_ITEMS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_ITEMS -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_ITEMS -> r gmapQ :: (forall d. Data d => d -> u) -> BASIC_ITEMS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BASIC_ITEMS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BASIC_ITEMS -> m BASIC_ITEMS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_ITEMS -> m BASIC_ITEMS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_ITEMS -> m BASIC_ITEMS | |
Show BASIC_ITEMS Source # | |
Methods showsPrec :: Int -> BASIC_ITEMS -> ShowS show :: BASIC_ITEMS -> String showList :: [BASIC_ITEMS] -> ShowS | |
GetRange BASIC_ITEMS Source # | |
Pretty BASIC_ITEMS Source # | |
newtype BASIC_SPEC Source #
Constructors
Basic_spec [Annoted BASIC_ITEMS] |
Instances
data SYMB_ITEMS Source #
Constructors
Symb_items [SYMB] Range |
Instances
Instances
Eq SYMB Source # | |
Data SYMB Source # | |
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB -> c SYMB gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMB dataTypeOf :: SYMB -> DataType dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SYMB) dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB) gmapT :: (forall b. Data b => b -> b) -> SYMB -> SYMB gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB -> r gmapQ :: (forall d. Data d => d -> u) -> SYMB -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB -> m SYMB gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB -> m SYMB gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB -> m SYMB | |
Ord SYMB Source # | |
Show SYMB Source # | |
GetRange SYMB Source # | |
Pretty SYMB Source # | |
data SYMB_MAP_ITEMS Source #
Constructors
Symb_map_items [SYMB_OR_MAP] Range |
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 | |
Ord SYMB_OR_MAP Source # | |
Methods compare :: SYMB_OR_MAP -> SYMB_OR_MAP -> Ordering (<) :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool (<=) :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool (>) :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool (>=) :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool max :: SYMB_OR_MAP -> SYMB_OR_MAP -> SYMB_OR_MAP min :: SYMB_OR_MAP -> SYMB_OR_MAP -> 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 | |
GetRange SYMB_OR_MAP Source # | |
Pretty SYMB_OR_MAP Source # | |
predicates = propotions
Instances
Data PRED_ITEM Source # | |
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PRED_ITEM -> c PRED_ITEM gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PRED_ITEM toConstr :: PRED_ITEM -> Constr dataTypeOf :: PRED_ITEM -> DataType dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c PRED_ITEM) dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PRED_ITEM) gmapT :: (forall b. Data b => b -> b) -> PRED_ITEM -> PRED_ITEM gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PRED_ITEM -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PRED_ITEM -> r gmapQ :: (forall d. Data d => d -> u) -> PRED_ITEM -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> PRED_ITEM -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> PRED_ITEM -> m PRED_ITEM gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PRED_ITEM -> m PRED_ITEM gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PRED_ITEM -> m PRED_ITEM | |
Show PRED_ITEM Source # | |
GetRange PRED_ITEM Source # | |
Pretty PRED_ITEM Source # | |
isPrimForm :: FORMULA -> Bool Source #