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 |
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
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 #
Instances
Data BASIC_ITEMS Source # | |
Defined in Propositional.AS_BASIC_Propositional 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 :: forall r r'. (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 # | |
Defined in Propositional.AS_BASIC_Propositional showsPrec :: Int -> BASIC_ITEMS -> ShowS show :: BASIC_ITEMS -> String showList :: [BASIC_ITEMS] -> ShowS | |
Generic BASIC_ITEMS | |
Defined in Propositional.ATC_Propositional type Rep BASIC_ITEMS :: Type -> Type from :: BASIC_ITEMS -> Rep BASIC_ITEMS x to :: Rep BASIC_ITEMS x -> BASIC_ITEMS | |
GetRange BASIC_ITEMS Source # | |
Defined in Propositional.AS_BASIC_Propositional getRange :: BASIC_ITEMS -> Range Source # rangeSpan :: BASIC_ITEMS -> [Pos] Source # | |
FromJSON BASIC_ITEMS | |
Defined in Propositional.ATC_Propositional parseJSON :: Value -> Parser BASIC_ITEMS parseJSONList :: Value -> Parser [BASIC_ITEMS] | |
ToJSON BASIC_ITEMS | |
Defined in Propositional.ATC_Propositional toJSON :: BASIC_ITEMS -> Value toEncoding :: BASIC_ITEMS -> Encoding toJSONList :: [BASIC_ITEMS] -> Value toEncodingList :: [BASIC_ITEMS] -> Encoding | |
ShATermConvertible BASIC_ITEMS | |
Defined in Propositional.ATC_Propositional toShATermAux :: ATermTable -> BASIC_ITEMS -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [BASIC_ITEMS] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_ITEMS) fromShATermList' :: Int -> ATermTable -> (ATermTable, [BASIC_ITEMS]) | |
Pretty BASIC_ITEMS Source # | |
Defined in Propositional.AS_BASIC_Propositional pretty :: BASIC_ITEMS -> Doc Source # pretties :: [BASIC_ITEMS] -> Doc Source # | |
type Rep BASIC_ITEMS | |
Defined in Propositional.ATC_Propositional type Rep BASIC_ITEMS = D1 ('MetaData "BASIC_ITEMS" "Propositional.AS_BASIC_Propositional" "main" 'False) (C1 ('MetaCons "Pred_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PRED_ITEM)) :+: C1 ('MetaCons "Axiom_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted FORMULA]))) |
newtype BASIC_SPEC Source #
Instances
data SYMB_ITEMS Source #
Instances
Instances
Eq SYMB Source # | |
Data SYMB Source # | |
Defined in Propositional.AS_BASIC_Propositional 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 :: forall r r'. (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 # | |
Generic SYMB | |
GetRange SYMB Source # | |
FromJSON SYMB | |
Defined in Propositional.ATC_Propositional parseJSON :: Value -> Parser SYMB parseJSONList :: Value -> Parser [SYMB] | |
ToJSON SYMB | |
Defined in Propositional.ATC_Propositional | |
ShATermConvertible SYMB | |
Defined in Propositional.ATC_Propositional toShATermAux :: ATermTable -> SYMB -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SYMB] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SYMB]) | |
Pretty SYMB Source # | |
type Rep SYMB | |
Defined in Propositional.ATC_Propositional |
data SYMB_MAP_ITEMS Source #
Instances
data SYMB_OR_MAP Source #
Instances
Eq SYMB_OR_MAP Source # | |
Defined in Propositional.AS_BASIC_Propositional (==) :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool (/=) :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool | |
Data SYMB_OR_MAP Source # | |
Defined in Propositional.AS_BASIC_Propositional 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 :: forall r r'. (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 # | |
Defined in Propositional.AS_BASIC_Propositional 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 # | |
Defined in Propositional.AS_BASIC_Propositional showsPrec :: Int -> SYMB_OR_MAP -> ShowS show :: SYMB_OR_MAP -> String showList :: [SYMB_OR_MAP] -> ShowS | |
Generic SYMB_OR_MAP | |
Defined in Propositional.ATC_Propositional type Rep SYMB_OR_MAP :: Type -> Type from :: SYMB_OR_MAP -> Rep SYMB_OR_MAP x to :: Rep SYMB_OR_MAP x -> SYMB_OR_MAP | |
GetRange SYMB_OR_MAP Source # | |
Defined in Propositional.AS_BASIC_Propositional getRange :: SYMB_OR_MAP -> Range Source # rangeSpan :: SYMB_OR_MAP -> [Pos] Source # | |
FromJSON SYMB_OR_MAP | |
Defined in Propositional.ATC_Propositional parseJSON :: Value -> Parser SYMB_OR_MAP parseJSONList :: Value -> Parser [SYMB_OR_MAP] | |
ToJSON SYMB_OR_MAP | |
Defined in Propositional.ATC_Propositional toJSON :: SYMB_OR_MAP -> Value toEncoding :: SYMB_OR_MAP -> Encoding toJSONList :: [SYMB_OR_MAP] -> Value toEncodingList :: [SYMB_OR_MAP] -> Encoding | |
ShATermConvertible SYMB_OR_MAP | |
Defined in Propositional.ATC_Propositional toShATermAux :: ATermTable -> SYMB_OR_MAP -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SYMB_OR_MAP] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_OR_MAP) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SYMB_OR_MAP]) | |
Pretty SYMB_OR_MAP Source # | |
Defined in Propositional.AS_BASIC_Propositional pretty :: SYMB_OR_MAP -> Doc Source # pretties :: [SYMB_OR_MAP] -> Doc Source # | |
type Rep SYMB_OR_MAP | |
Defined in Propositional.ATC_Propositional type Rep SYMB_OR_MAP = D1 ('MetaData "SYMB_OR_MAP" "Propositional.AS_BASIC_Propositional" "main" 'False) (C1 ('MetaCons "Symb" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SYMB)) :+: C1 ('MetaCons "Symb_map" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SYMB) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SYMB) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) |
predicates = propotions
Instances
Data PRED_ITEM Source # | |
Defined in Propositional.AS_BASIC_Propositional 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 :: forall r r'. (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 # | |
Generic PRED_ITEM | |
GetRange PRED_ITEM Source # | |
FromJSON PRED_ITEM | |
Defined in Propositional.ATC_Propositional parseJSON :: Value -> Parser PRED_ITEM parseJSONList :: Value -> Parser [PRED_ITEM] | |
ToJSON PRED_ITEM | |
Defined in Propositional.ATC_Propositional toEncoding :: PRED_ITEM -> Encoding toJSONList :: [PRED_ITEM] -> Value toEncodingList :: [PRED_ITEM] -> Encoding | |
ShATermConvertible PRED_ITEM | |
Defined in Propositional.ATC_Propositional toShATermAux :: ATermTable -> PRED_ITEM -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [PRED_ITEM] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, PRED_ITEM) fromShATermList' :: Int -> ATermTable -> (ATermTable, [PRED_ITEM]) | |
Pretty PRED_ITEM Source # | |
type Rep PRED_ITEM | |
Defined in Propositional.ATC_Propositional type Rep PRED_ITEM = D1 ('MetaData "PRED_ITEM" "Propositional.AS_BASIC_Propositional" "main" 'False) (C1 ('MetaCons "Pred_item" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Token]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) |
isPrimForm :: FORMULA -> Bool Source #