Hets - the Heterogeneous Tool Set
Copyright (c) Dominik Luecke Uni Bremen 2007 GPLv2 or higher, see LICENSE.txt luecke@informatik.uni-bremen.de experimental portable Safe

Propositional.AS_BASIC_Propositional

Description

Definition of abstract syntax for propositional logic

Synopsis

# Documentation

data FORMULA Source #

Datatype for propositional formulas

#### Instances

Instances details
 Eq FORMULA Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methods(==) :: FORMULA -> FORMULA -> Bool(/=) :: FORMULA -> FORMULA -> Bool Data FORMULA Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FORMULA -> c FORMULAgunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FORMULAtoConstr :: FORMULA -> ConstrdataTypeOf :: FORMULA -> DataTypedataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FORMULA)dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FORMULA)gmapT :: (forall b. Data b => b -> b) -> FORMULA -> FORMULAgmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FORMULA -> rgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FORMULA -> rgmapQ :: (forall d. Data d => d -> u) -> FORMULA -> [u]gmapQi :: Int -> (forall d. Data d => d -> u) -> FORMULA -> ugmapM :: Monad m => (forall d. Data d => d -> m d) -> FORMULA -> m FORMULAgmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FORMULA -> m FORMULAgmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA Ord FORMULA Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodscompare :: FORMULA -> FORMULA -> Ordering(<) :: FORMULA -> FORMULA -> Bool(<=) :: FORMULA -> FORMULA -> Bool(>) :: FORMULA -> FORMULA -> Bool(>=) :: FORMULA -> FORMULA -> Boolmax :: FORMULA -> FORMULA -> FORMULAmin :: FORMULA -> FORMULA -> FORMULA Show FORMULA Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional MethodsshowsPrec :: Int -> FORMULA -> ShowSshow :: FORMULA -> StringshowList :: [FORMULA] -> ShowS Generic FORMULA Instance detailsDefined in Propositional.ATC_Propositional Associated Typestype Rep FORMULA :: Type -> Type Methodsfrom :: FORMULA -> Rep FORMULA xto :: Rep FORMULA x -> FORMULA Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional MethodsrangeSpan :: FORMULA -> [Pos] Source # FromJSON FORMULA Instance detailsDefined in Propositional.ATC_Propositional MethodsparseJSON :: Value -> Parser FORMULAparseJSONList :: Value -> Parser [FORMULA] ToJSON FORMULA Instance detailsDefined in Propositional.ATC_Propositional MethodstoJSON :: FORMULA -> ValuetoEncoding :: FORMULA -> EncodingtoJSONList :: [FORMULA] -> ValuetoEncodingList :: [FORMULA] -> Encoding ShATermConvertible FORMULA Instance detailsDefined in Propositional.ATC_Propositional MethodstoShATermAux :: ATermTable -> FORMULA -> IO (ATermTable, Int)toShATermList' :: ATermTable -> [FORMULA] -> IO (ATermTable, Int)fromShATermAux :: Int -> ATermTable -> (ATermTable, FORMULA)fromShATermList' :: Int -> ATermTable -> (ATermTable, [FORMULA]) Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodspretties :: [FORMULA] -> Doc Source # Source # Instance detailsDefined in Propositional.Logic_Propositional MethodsprojectSublogicM :: PropSL -> FORMULA -> Maybe FORMULA Source # Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance of Sentences for propositional logic Instance detailsDefined in Propositional.Logic_Propositional Methodsnegation :: Propositional -> FORMULA -> Maybe FORMULA Source #sym_of :: Propositional -> Sign -> [Set Symbol] Source #sym_label :: Propositional -> Symbol -> Maybe String Source #fullSymName :: Propositional -> Symbol -> String Source #symKind :: Propositional -> Symbol -> String Source # Source # Static Analysis for propositional logic Instance detailsDefined in Propositional.Logic_Propositional Methodsbasic_analysis :: Propositional -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])) Source #sen_analysis :: Propositional -> Maybe ((BASIC_SPEC, Sign, FORMULA) -> Result FORMULA) Source #stat_symb_map_items :: Propositional -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source #convertTheory :: Propositional -> Maybe ((Sign, [Named FORMULA]) -> BASIC_SPEC) Source #ensures_amalgamability :: Propositional -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #signature_colimit :: Propositional -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #matches :: Propositional -> Symbol -> Symbol -> Bool Source #is_subsig :: Propositional -> Sign -> Sign -> Bool Source #is_transportable :: Propositional -> Morphism -> Bool Source #is_injective :: Propositional -> Morphism -> Bool Source #corresp2th :: Propositional -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #equiv2cospan :: Propositional -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #extract_module :: Propositional -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # Source # Instance of Logic for propositional logc Instance detailsDefined in Propositional.Logic_Propositional Methodsparse_basic_sen :: Propositional -> Maybe (BASIC_SPEC -> AParser st FORMULA) Source #data_logic :: Propositional -> Maybe AnyLogic Source #bottomSublogic :: Propositional -> Maybe PropSL Source #parseSublogic :: Propositional -> String -> Maybe PropSL Source #default_prover :: Propositional -> String Source #syntaxTable :: Propositional -> Sign -> Maybe SyntaxTable Source #omdoc_metatheory :: Propositional -> Maybe OMCD Source #export_symToOmdoc :: Propositional -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #omdocToSym :: Propositional -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #omdocToSen :: Propositional -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source #addOMadtToTheory :: Propositional -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source #addOmdocToTheory :: Propositional -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source #sublogicOfTheo :: Propositional -> (Sign, [FORMULA]) -> PropSL Source # Source # Instance detailsDefined in OWL2.Propositional2OWL2 MethodsminSourceTheory :: Propositional2OWL2 -> Maybe (LibName, String) Source #map_theory :: Propositional2OWL2 -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named Axiom]) Source #mapMarkedTheory :: Propositional2OWL2 -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named Axiom]) Source #constituents :: Propositional2OWL2 -> [String] Source #rps :: Propositional2OWL2 -> Bool Source #eps :: Propositional2OWL2 -> Bool Source #isGTC :: Propositional2OWL2 -> Bool Source # Source # Instance detailsDefined in Comorphisms.QBF2Prop MethodsminSourceTheory :: QBF2Prop -> Maybe (LibName, String) Source #mapSublogic :: QBF2Prop -> QBFSL -> Maybe PropSL Source #map_theory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA0]) Source #mapMarkedTheory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA0]) Source #map_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol0 Source #has_model_expansion :: QBF2Prop -> Bool Source #is_weakly_amalgamable :: QBF2Prop -> Bool Source #constituents :: QBF2Prop -> [String] Source #isInclusionComorphism :: QBF2Prop -> Bool Source #rps :: QBF2Prop -> Bool Source #eps :: QBF2Prop -> Bool Source #isGTC :: QBF2Prop -> Bool Source # Source # Instance detailsDefined in Comorphisms.Prop2QBF MethodsminSourceTheory :: Prop2QBF -> Maybe (LibName, String) Source #mapSublogic :: Prop2QBF -> PropSL -> Maybe QBFSL Source #map_theory :: Prop2QBF -> (Sign, [Named FORMULA0]) -> Result (Sign, [Named FORMULA]) Source #mapMarkedTheory :: Prop2QBF -> (Sign, [Named FORMULA0]) -> Result (Sign, [Named FORMULA]) Source #map_symbol :: Prop2QBF -> Sign -> Symbol0 -> Set Symbol Source #has_model_expansion :: Prop2QBF -> Bool Source #is_weakly_amalgamable :: Prop2QBF -> Bool Source #constituents :: Prop2QBF -> [String] Source #isInclusionComorphism :: Prop2QBF -> Bool Source #rps :: Prop2QBF -> Bool Source #eps :: Prop2QBF -> Bool Source #isGTC :: Prop2QBF -> Bool Source # Source # Instance detailsDefined in Comorphisms.Prop2CommonLogic MethodsminSourceTheory :: Prop2CommonLogic -> Maybe (LibName, String) Source #map_theory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source #mapMarkedTheory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source #constituents :: Prop2CommonLogic -> [String] Source #rps :: Prop2CommonLogic -> Bool Source #eps :: Prop2CommonLogic -> Bool Source #isGTC :: Prop2CommonLogic -> Bool Source # Source # Instance detailsDefined in Comorphisms.Prop2CASL MethodsminSourceTheory :: Prop2CASL -> Maybe (LibName, String) Source #mapSublogic :: Prop2CASL -> PropSL -> Maybe CASL_Sublogics Source #map_theory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #mapMarkedTheory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #map_symbol :: Prop2CASL -> Sign -> Symbol -> Set Symbol0 Source #has_model_expansion :: Prop2CASL -> Bool Source #constituents :: Prop2CASL -> [String] Source #rps :: Prop2CASL -> Bool Source #eps :: Prop2CASL -> Bool Source #isGTC :: Prop2CASL -> Bool Source # Source # Instance detailsDefined in Comorphisms.CASL2Prop MethodsminSourceTheory :: CASL2Prop -> Maybe (LibName, String) Source #mapSublogic :: CASL2Prop -> CASL_Sublogics -> Maybe PropSL Source #map_theory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source #mapMarkedTheory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source #map_symbol :: CASL2Prop -> CASLSign -> Symbol0 -> Set Symbol Source #has_model_expansion :: CASL2Prop -> Bool Source #constituents :: CASL2Prop -> [String] Source #rps :: CASL2Prop -> Bool Source #eps :: CASL2Prop -> Bool Source #isGTC :: CASL2Prop -> Bool Source # type Rep FORMULA Instance detailsDefined in Propositional.ATC_Propositional type Rep FORMULA = D1 ('MetaData "FORMULA" "Propositional.AS_BASIC_Propositional" "main" 'False) (((C1 ('MetaCons "False_atom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "True_atom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "Predication" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: C1 ('MetaCons "Negation" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FORMULA) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: ((C1 ('MetaCons "Conjunction" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FORMULA]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "Disjunction" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FORMULA]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "Implication" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FORMULA) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FORMULA) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Equivalence" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FORMULA) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FORMULA) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))))

Constructors

 Pred_decl PRED_ITEM Axiom_items [Annoted FORMULA]

#### Instances

Instances details
 Data BASIC_ITEMS Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BASIC_ITEMS -> c BASIC_ITEMSgunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BASIC_ITEMStoConstr :: BASIC_ITEMS -> ConstrdataTypeOf :: BASIC_ITEMS -> DataTypedataCast1 :: 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_ITEMSgmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_ITEMS -> rgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_ITEMS -> rgmapQ :: (forall d. Data d => d -> u) -> BASIC_ITEMS -> [u]gmapQi :: Int -> (forall d. Data d => d -> u) -> BASIC_ITEMS -> ugmapM :: Monad m => (forall d. Data d => d -> m d) -> BASIC_ITEMS -> m BASIC_ITEMSgmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_ITEMS -> m BASIC_ITEMSgmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_ITEMS -> m BASIC_ITEMS Show BASIC_ITEMS Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional MethodsshowsPrec :: Int -> BASIC_ITEMS -> ShowSshow :: BASIC_ITEMS -> StringshowList :: [BASIC_ITEMS] -> ShowS Generic BASIC_ITEMS Instance detailsDefined in Propositional.ATC_Propositional Associated Typestype Rep BASIC_ITEMS :: Type -> Type Methodsfrom :: BASIC_ITEMS -> Rep BASIC_ITEMS xto :: Rep BASIC_ITEMS x -> BASIC_ITEMS Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methods FromJSON BASIC_ITEMS Instance detailsDefined in Propositional.ATC_Propositional MethodsparseJSON :: Value -> Parser BASIC_ITEMSparseJSONList :: Value -> Parser [BASIC_ITEMS] ToJSON BASIC_ITEMS Instance detailsDefined in Propositional.ATC_Propositional MethodstoJSON :: BASIC_ITEMS -> ValuetoEncoding :: BASIC_ITEMS -> EncodingtoJSONList :: [BASIC_ITEMS] -> ValuetoEncodingList :: [BASIC_ITEMS] -> Encoding ShATermConvertible BASIC_ITEMS Instance detailsDefined in Propositional.ATC_Propositional MethodstoShATermAux :: 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]) Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodspretties :: [BASIC_ITEMS] -> Doc Source # type Rep BASIC_ITEMS Instance detailsDefined 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 #

Constructors

 Basic_spec [Annoted BASIC_ITEMS]

#### Instances

Instances details
 Data BASIC_SPEC Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BASIC_SPEC -> c BASIC_SPECgunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BASIC_SPECtoConstr :: BASIC_SPEC -> ConstrdataTypeOf :: BASIC_SPEC -> DataTypedataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BASIC_SPEC)dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASIC_SPEC)gmapT :: (forall b. Data b => b -> b) -> BASIC_SPEC -> BASIC_SPECgmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_SPEC -> rgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_SPEC -> rgmapQ :: (forall d. Data d => d -> u) -> BASIC_SPEC -> [u]gmapQi :: Int -> (forall d. Data d => d -> u) -> BASIC_SPEC -> ugmapM :: Monad m => (forall d. Data d => d -> m d) -> BASIC_SPEC -> m BASIC_SPECgmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_SPEC -> m BASIC_SPECgmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_SPEC -> m BASIC_SPEC Show BASIC_SPEC Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional MethodsshowsPrec :: Int -> BASIC_SPEC -> ShowSshow :: BASIC_SPEC -> StringshowList :: [BASIC_SPEC] -> ShowS Generic BASIC_SPEC Instance detailsDefined in Propositional.ATC_Propositional Associated Typestype Rep BASIC_SPEC :: Type -> Type Methodsfrom :: BASIC_SPEC -> Rep BASIC_SPEC xto :: Rep BASIC_SPEC x -> BASIC_SPEC Semigroup BASIC_SPEC Instance detailsDefined in Propositional.Logic_Propositional Methodssconcat :: NonEmpty BASIC_SPEC -> BASIC_SPECstimes :: Integral b => b -> BASIC_SPEC -> BASIC_SPEC Monoid BASIC_SPEC Instance detailsDefined in Propositional.Logic_Propositional Methodsmconcat :: [BASIC_SPEC] -> BASIC_SPEC Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methods FromJSON BASIC_SPEC Instance detailsDefined in Propositional.ATC_Propositional MethodsparseJSON :: Value -> Parser BASIC_SPECparseJSONList :: Value -> Parser [BASIC_SPEC] ToJSON BASIC_SPEC Instance detailsDefined in Propositional.ATC_Propositional MethodstoJSON :: BASIC_SPEC -> ValuetoEncoding :: BASIC_SPEC -> EncodingtoJSONList :: [BASIC_SPEC] -> ValuetoEncodingList :: [BASIC_SPEC] -> Encoding ShATermConvertible BASIC_SPEC Instance detailsDefined in Propositional.ATC_Propositional MethodstoShATermAux :: ATermTable -> BASIC_SPEC -> IO (ATermTable, Int)toShATermList' :: ATermTable -> [BASIC_SPEC] -> IO (ATermTable, Int)fromShATermAux :: Int -> ATermTable -> (ATermTable, BASIC_SPEC)fromShATermList' :: Int -> ATermTable -> (ATermTable, [BASIC_SPEC]) Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodspretties :: [BASIC_SPEC] -> Doc Source # Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional MethodsparsersAndPrinters :: Propositional -> Map String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc) Source #parse_basic_spec :: Propositional -> Maybe (PrefixMap -> AParser st BASIC_SPEC) Source #parseSingleSymbItem :: Propositional -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source #parse_symb_items :: Propositional -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source #symb_items_name :: Propositional -> SYMB_ITEMS -> [String] Source # Source # Static Analysis for propositional logic Instance detailsDefined in Propositional.Logic_Propositional Methodsbasic_analysis :: Propositional -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])) Source #sen_analysis :: Propositional -> Maybe ((BASIC_SPEC, Sign, FORMULA) -> Result FORMULA) Source #stat_symb_map_items :: Propositional -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source #convertTheory :: Propositional -> Maybe ((Sign, [Named FORMULA]) -> BASIC_SPEC) Source #ensures_amalgamability :: Propositional -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #signature_colimit :: Propositional -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #matches :: Propositional -> Symbol -> Symbol -> Bool Source #is_subsig :: Propositional -> Sign -> Sign -> Bool Source #is_transportable :: Propositional -> Morphism -> Bool Source #is_injective :: Propositional -> Morphism -> Bool Source #corresp2th :: Propositional -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #equiv2cospan :: Propositional -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #extract_module :: Propositional -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # Source # Instance of Logic for propositional logc Instance detailsDefined in Propositional.Logic_Propositional Methodsparse_basic_sen :: Propositional -> Maybe (BASIC_SPEC -> AParser st FORMULA) Source #data_logic :: Propositional -> Maybe AnyLogic Source #bottomSublogic :: Propositional -> Maybe PropSL Source #parseSublogic :: Propositional -> String -> Maybe PropSL Source #default_prover :: Propositional -> String Source #syntaxTable :: Propositional -> Sign -> Maybe SyntaxTable Source #omdoc_metatheory :: Propositional -> Maybe OMCD Source #export_symToOmdoc :: Propositional -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #omdocToSym :: Propositional -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #omdocToSen :: Propositional -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source #addOMadtToTheory :: Propositional -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source #addOmdocToTheory :: Propositional -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source #sublogicOfTheo :: Propositional -> (Sign, [FORMULA]) -> PropSL Source # Source # Instance detailsDefined in OWL2.Propositional2OWL2 MethodsminSourceTheory :: Propositional2OWL2 -> Maybe (LibName, String) Source #map_theory :: Propositional2OWL2 -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named Axiom]) Source #mapMarkedTheory :: Propositional2OWL2 -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named Axiom]) Source #constituents :: Propositional2OWL2 -> [String] Source #rps :: Propositional2OWL2 -> Bool Source #eps :: Propositional2OWL2 -> Bool Source #isGTC :: Propositional2OWL2 -> Bool Source # Source # Instance detailsDefined in Comorphisms.QBF2Prop MethodsminSourceTheory :: QBF2Prop -> Maybe (LibName, String) Source #mapSublogic :: QBF2Prop -> QBFSL -> Maybe PropSL Source #map_theory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA0]) Source #mapMarkedTheory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA0]) Source #map_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol0 Source #has_model_expansion :: QBF2Prop -> Bool Source #is_weakly_amalgamable :: QBF2Prop -> Bool Source #constituents :: QBF2Prop -> [String] Source #isInclusionComorphism :: QBF2Prop -> Bool Source #rps :: QBF2Prop -> Bool Source #eps :: QBF2Prop -> Bool Source #isGTC :: QBF2Prop -> Bool Source # Source # Instance detailsDefined in Comorphisms.Prop2QBF MethodsminSourceTheory :: Prop2QBF -> Maybe (LibName, String) Source #mapSublogic :: Prop2QBF -> PropSL -> Maybe QBFSL Source #map_theory :: Prop2QBF -> (Sign, [Named FORMULA0]) -> Result (Sign, [Named FORMULA]) Source #mapMarkedTheory :: Prop2QBF -> (Sign, [Named FORMULA0]) -> Result (Sign, [Named FORMULA]) Source #map_symbol :: Prop2QBF -> Sign -> Symbol0 -> Set Symbol Source #has_model_expansion :: Prop2QBF -> Bool Source #is_weakly_amalgamable :: Prop2QBF -> Bool Source #constituents :: Prop2QBF -> [String] Source #isInclusionComorphism :: Prop2QBF -> Bool Source #rps :: Prop2QBF -> Bool Source #eps :: Prop2QBF -> Bool Source #isGTC :: Prop2QBF -> Bool Source # Source # Instance detailsDefined in Comorphisms.Prop2CommonLogic MethodsminSourceTheory :: Prop2CommonLogic -> Maybe (LibName, String) Source #map_theory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source #mapMarkedTheory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source #constituents :: Prop2CommonLogic -> [String] Source #rps :: Prop2CommonLogic -> Bool Source #eps :: Prop2CommonLogic -> Bool Source #isGTC :: Prop2CommonLogic -> Bool Source # Source # Instance detailsDefined in Comorphisms.Prop2CASL MethodsminSourceTheory :: Prop2CASL -> Maybe (LibName, String) Source #mapSublogic :: Prop2CASL -> PropSL -> Maybe CASL_Sublogics Source #map_theory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #mapMarkedTheory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #map_symbol :: Prop2CASL -> Sign -> Symbol -> Set Symbol0 Source #has_model_expansion :: Prop2CASL -> Bool Source #constituents :: Prop2CASL -> [String] Source #rps :: Prop2CASL -> Bool Source #eps :: Prop2CASL -> Bool Source #isGTC :: Prop2CASL -> Bool Source # Source # Instance detailsDefined in Comorphisms.CASL2Prop MethodsminSourceTheory :: CASL2Prop -> Maybe (LibName, String) Source #mapSublogic :: CASL2Prop -> CASL_Sublogics -> Maybe PropSL Source #map_theory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source #mapMarkedTheory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source #map_symbol :: CASL2Prop -> CASLSign -> Symbol0 -> Set Symbol Source #has_model_expansion :: CASL2Prop -> Bool Source #constituents :: CASL2Prop -> [String] Source #rps :: CASL2Prop -> Bool Source #eps :: CASL2Prop -> Bool Source #isGTC :: CASL2Prop -> Bool Source # type Rep BASIC_SPEC Instance detailsDefined in Propositional.ATC_Propositional type Rep BASIC_SPEC = D1 ('MetaData "BASIC_SPEC" "Propositional.AS_BASIC_Propositional" "main" 'True) (C1 ('MetaCons "Basic_spec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted BASIC_ITEMS])))

Constructors

 Symb_items [SYMB] Range

#### Instances

Instances details
 Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methods(==) :: SYMB_ITEMS -> SYMB_ITEMS -> Bool(/=) :: SYMB_ITEMS -> SYMB_ITEMS -> Bool Data SYMB_ITEMS Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB_ITEMS -> c SYMB_ITEMSgunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMB_ITEMStoConstr :: SYMB_ITEMS -> ConstrdataTypeOf :: SYMB_ITEMS -> DataTypedataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SYMB_ITEMS)dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_ITEMS)gmapT :: (forall b. Data b => b -> b) -> SYMB_ITEMS -> SYMB_ITEMSgmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> rgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> rgmapQ :: (forall d. Data d => d -> u) -> SYMB_ITEMS -> [u]gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_ITEMS -> ugmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMSgmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMSgmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS Ord SYMB_ITEMS Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodscompare :: SYMB_ITEMS -> SYMB_ITEMS -> Ordering(<) :: SYMB_ITEMS -> SYMB_ITEMS -> Bool(<=) :: SYMB_ITEMS -> SYMB_ITEMS -> Bool(>) :: SYMB_ITEMS -> SYMB_ITEMS -> Bool(>=) :: SYMB_ITEMS -> SYMB_ITEMS -> Bool Show SYMB_ITEMS Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional MethodsshowsPrec :: Int -> SYMB_ITEMS -> ShowSshow :: SYMB_ITEMS -> StringshowList :: [SYMB_ITEMS] -> ShowS Generic SYMB_ITEMS Instance detailsDefined in Propositional.ATC_Propositional Associated Typestype Rep SYMB_ITEMS :: Type -> Type Methodsfrom :: SYMB_ITEMS -> Rep SYMB_ITEMS xto :: Rep SYMB_ITEMS x -> SYMB_ITEMS Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methods FromJSON SYMB_ITEMS Instance detailsDefined in Propositional.ATC_Propositional MethodsparseJSON :: Value -> Parser SYMB_ITEMSparseJSONList :: Value -> Parser [SYMB_ITEMS] ToJSON SYMB_ITEMS Instance detailsDefined in Propositional.ATC_Propositional MethodstoJSON :: SYMB_ITEMS -> ValuetoEncoding :: SYMB_ITEMS -> EncodingtoJSONList :: [SYMB_ITEMS] -> ValuetoEncodingList :: [SYMB_ITEMS] -> Encoding ShATermConvertible SYMB_ITEMS Instance detailsDefined in Propositional.ATC_Propositional MethodstoShATermAux :: ATermTable -> SYMB_ITEMS -> IO (ATermTable, Int)toShATermList' :: ATermTable -> [SYMB_ITEMS] -> IO (ATermTable, Int)fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_ITEMS)fromShATermList' :: Int -> ATermTable -> (ATermTable, [SYMB_ITEMS]) Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodspretties :: [SYMB_ITEMS] -> Doc Source # Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional MethodsparsersAndPrinters :: Propositional -> Map String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc) Source #parse_basic_spec :: Propositional -> Maybe (PrefixMap -> AParser st BASIC_SPEC) Source #parseSingleSymbItem :: Propositional -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source #parse_symb_items :: Propositional -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source #symb_items_name :: Propositional -> SYMB_ITEMS -> [String] Source # Source # Static Analysis for propositional logic Instance detailsDefined in Propositional.Logic_Propositional Methodsbasic_analysis :: Propositional -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])) Source #sen_analysis :: Propositional -> Maybe ((BASIC_SPEC, Sign, FORMULA) -> Result FORMULA) Source #stat_symb_map_items :: Propositional -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source #convertTheory :: Propositional -> Maybe ((Sign, [Named FORMULA]) -> BASIC_SPEC) Source #ensures_amalgamability :: Propositional -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #signature_colimit :: Propositional -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #matches :: Propositional -> Symbol -> Symbol -> Bool Source #is_subsig :: Propositional -> Sign -> Sign -> Bool Source #is_transportable :: Propositional -> Morphism -> Bool Source #is_injective :: Propositional -> Morphism -> Bool Source #corresp2th :: Propositional -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #equiv2cospan :: Propositional -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #extract_module :: Propositional -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # Source # Instance of Logic for propositional logc Instance detailsDefined in Propositional.Logic_Propositional Methodsparse_basic_sen :: Propositional -> Maybe (BASIC_SPEC -> AParser st FORMULA) Source #data_logic :: Propositional -> Maybe AnyLogic Source #bottomSublogic :: Propositional -> Maybe PropSL Source #parseSublogic :: Propositional -> String -> Maybe PropSL Source #default_prover :: Propositional -> String Source #syntaxTable :: Propositional -> Sign -> Maybe SyntaxTable Source #omdoc_metatheory :: Propositional -> Maybe OMCD Source #export_symToOmdoc :: Propositional -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #omdocToSym :: Propositional -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #omdocToSen :: Propositional -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source #addOMadtToTheory :: Propositional -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source #addOmdocToTheory :: Propositional -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source #sublogicOfTheo :: Propositional -> (Sign, [FORMULA]) -> PropSL Source # Source # Instance detailsDefined in OWL2.Propositional2OWL2 MethodsminSourceTheory :: Propositional2OWL2 -> Maybe (LibName, String) Source #map_theory :: Propositional2OWL2 -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named Axiom]) Source #mapMarkedTheory :: Propositional2OWL2 -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named Axiom]) Source #constituents :: Propositional2OWL2 -> [String] Source #rps :: Propositional2OWL2 -> Bool Source #eps :: Propositional2OWL2 -> Bool Source #isGTC :: Propositional2OWL2 -> Bool Source # Source # Instance detailsDefined in Comorphisms.QBF2Prop MethodsminSourceTheory :: QBF2Prop -> Maybe (LibName, String) Source #mapSublogic :: QBF2Prop -> QBFSL -> Maybe PropSL Source #map_theory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA0]) Source #mapMarkedTheory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA0]) Source #map_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol0 Source #has_model_expansion :: QBF2Prop -> Bool Source #is_weakly_amalgamable :: QBF2Prop -> Bool Source #constituents :: QBF2Prop -> [String] Source #isInclusionComorphism :: QBF2Prop -> Bool Source #rps :: QBF2Prop -> Bool Source #eps :: QBF2Prop -> Bool Source #isGTC :: QBF2Prop -> Bool Source # Source # Instance detailsDefined in Comorphisms.Prop2QBF MethodsminSourceTheory :: Prop2QBF -> Maybe (LibName, String) Source #mapSublogic :: Prop2QBF -> PropSL -> Maybe QBFSL Source #map_theory :: Prop2QBF -> (Sign, [Named FORMULA0]) -> Result (Sign, [Named FORMULA]) Source #mapMarkedTheory :: Prop2QBF -> (Sign, [Named FORMULA0]) -> Result (Sign, [Named FORMULA]) Source #map_symbol :: Prop2QBF -> Sign -> Symbol0 -> Set Symbol Source #has_model_expansion :: Prop2QBF -> Bool Source #is_weakly_amalgamable :: Prop2QBF -> Bool Source #constituents :: Prop2QBF -> [String] Source #isInclusionComorphism :: Prop2QBF -> Bool Source #rps :: Prop2QBF -> Bool Source #eps :: Prop2QBF -> Bool Source #isGTC :: Prop2QBF -> Bool Source # Source # Instance detailsDefined in Comorphisms.Prop2CommonLogic MethodsminSourceTheory :: Prop2CommonLogic -> Maybe (LibName, String) Source #map_theory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source #mapMarkedTheory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source #constituents :: Prop2CommonLogic -> [String] Source #rps :: Prop2CommonLogic -> Bool Source #eps :: Prop2CommonLogic -> Bool Source #isGTC :: Prop2CommonLogic -> Bool Source # Source # Instance detailsDefined in Comorphisms.Prop2CASL MethodsminSourceTheory :: Prop2CASL -> Maybe (LibName, String) Source #mapSublogic :: Prop2CASL -> PropSL -> Maybe CASL_Sublogics Source #map_theory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #mapMarkedTheory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #map_symbol :: Prop2CASL -> Sign -> Symbol -> Set Symbol0 Source #has_model_expansion :: Prop2CASL -> Bool Source #constituents :: Prop2CASL -> [String] Source #rps :: Prop2CASL -> Bool Source #eps :: Prop2CASL -> Bool Source #isGTC :: Prop2CASL -> Bool Source # Source # Instance detailsDefined in Comorphisms.CASL2Prop MethodsminSourceTheory :: CASL2Prop -> Maybe (LibName, String) Source #mapSublogic :: CASL2Prop -> CASL_Sublogics -> Maybe PropSL Source #map_theory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source #mapMarkedTheory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source #map_symbol :: CASL2Prop -> CASLSign -> Symbol0 -> Set Symbol Source #has_model_expansion :: CASL2Prop -> Bool Source #constituents :: CASL2Prop -> [String] Source #rps :: CASL2Prop -> Bool Source #eps :: CASL2Prop -> Bool Source #isGTC :: CASL2Prop -> Bool Source # type Rep SYMB_ITEMS Instance detailsDefined in Propositional.ATC_Propositional type Rep SYMB_ITEMS = D1 ('MetaData "SYMB_ITEMS" "Propositional.AS_BASIC_Propositional" "main" 'False) (C1 ('MetaCons "Symb_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SYMB]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

newtype SYMB Source #

Constructors

 Symb_id Token

#### Instances

Instances details
 Eq SYMB Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methods(==) :: SYMB -> SYMB -> Bool(/=) :: SYMB -> SYMB -> Bool Data SYMB Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB -> c SYMBgunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMBtoConstr :: SYMB -> ConstrdataTypeOf :: SYMB -> DataTypedataCast1 :: 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 -> SYMBgmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB -> rgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB -> rgmapQ :: (forall d. Data d => d -> u) -> SYMB -> [u]gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB -> ugmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB -> m SYMBgmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB -> m SYMBgmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB -> m SYMB Ord SYMB Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodscompare :: SYMB -> SYMB -> Ordering(<) :: SYMB -> SYMB -> Bool(<=) :: SYMB -> SYMB -> Bool(>) :: SYMB -> SYMB -> Bool(>=) :: SYMB -> SYMB -> Boolmax :: SYMB -> SYMB -> SYMBmin :: SYMB -> SYMB -> SYMB Show SYMB Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional MethodsshowsPrec :: Int -> SYMB -> ShowSshow :: SYMB -> StringshowList :: [SYMB] -> ShowS Generic SYMB Instance detailsDefined in Propositional.ATC_Propositional Associated Typestype Rep SYMB :: Type -> Type Methodsfrom :: SYMB -> Rep SYMB xto :: Rep SYMB x -> SYMB Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional MethodsrangeSpan :: SYMB -> [Pos] Source # FromJSON SYMB Instance detailsDefined in Propositional.ATC_Propositional MethodsparseJSON :: Value -> Parser SYMBparseJSONList :: Value -> Parser [SYMB] ToJSON SYMB Instance detailsDefined in Propositional.ATC_Propositional MethodstoJSON :: SYMB -> ValuetoEncoding :: SYMB -> EncodingtoJSONList :: [SYMB] -> ValuetoEncodingList :: [SYMB] -> Encoding ShATermConvertible SYMB Instance detailsDefined in Propositional.ATC_Propositional MethodstoShATermAux :: ATermTable -> SYMB -> IO (ATermTable, Int)toShATermList' :: ATermTable -> [SYMB] -> IO (ATermTable, Int)fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB)fromShATermList' :: Int -> ATermTable -> (ATermTable, [SYMB]) Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodspretties :: [SYMB] -> Doc Source # type Rep SYMB Instance detailsDefined in Propositional.ATC_Propositional type Rep SYMB = D1 ('MetaData "SYMB" "Propositional.AS_BASIC_Propositional" "main" 'True) (C1 ('MetaCons "Symb_id" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))

Constructors

 Symb_map_items [SYMB_OR_MAP] Range

#### Instances

Instances details
 Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methods(==) :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool(/=) :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool Data SYMB_MAP_ITEMS Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB_MAP_ITEMS -> c SYMB_MAP_ITEMSgunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMB_MAP_ITEMStoConstr :: SYMB_MAP_ITEMS -> ConstrdataTypeOf :: SYMB_MAP_ITEMS -> DataTypedataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SYMB_MAP_ITEMS)dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_MAP_ITEMS)gmapT :: (forall b. Data b => b -> b) -> SYMB_MAP_ITEMS -> SYMB_MAP_ITEMSgmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_MAP_ITEMS -> rgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_MAP_ITEMS -> rgmapQ :: (forall d. Data d => d -> u) -> SYMB_MAP_ITEMS -> [u]gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_MAP_ITEMS -> ugmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMSgmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMSgmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodscompare :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Ordering(<) :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool(<=) :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool(>) :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool(>=) :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool Show SYMB_MAP_ITEMS Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional MethodsshowsPrec :: Int -> SYMB_MAP_ITEMS -> ShowSshow :: SYMB_MAP_ITEMS -> StringshowList :: [SYMB_MAP_ITEMS] -> ShowS Generic SYMB_MAP_ITEMS Instance detailsDefined in Propositional.ATC_Propositional Associated Typestype Rep SYMB_MAP_ITEMS :: Type -> Type Methodsfrom :: SYMB_MAP_ITEMS -> Rep SYMB_MAP_ITEMS xto :: Rep SYMB_MAP_ITEMS x -> SYMB_MAP_ITEMS Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methods FromJSON SYMB_MAP_ITEMS Instance detailsDefined in Propositional.ATC_Propositional MethodsparseJSON :: Value -> Parser SYMB_MAP_ITEMSparseJSONList :: Value -> Parser [SYMB_MAP_ITEMS] ToJSON SYMB_MAP_ITEMS Instance detailsDefined in Propositional.ATC_Propositional MethodstoJSON :: SYMB_MAP_ITEMS -> ValuetoEncoding :: SYMB_MAP_ITEMS -> EncodingtoJSONList :: [SYMB_MAP_ITEMS] -> ValuetoEncodingList :: [SYMB_MAP_ITEMS] -> Encoding ShATermConvertible SYMB_MAP_ITEMS Instance detailsDefined in Propositional.ATC_Propositional MethodstoShATermAux :: ATermTable -> SYMB_MAP_ITEMS -> IO (ATermTable, Int)toShATermList' :: ATermTable -> [SYMB_MAP_ITEMS] -> IO (ATermTable, Int)fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMB_MAP_ITEMS)fromShATermList' :: Int -> ATermTable -> (ATermTable, [SYMB_MAP_ITEMS]) Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodspretties :: [SYMB_MAP_ITEMS] -> Doc Source # Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional Methods Source # Instance detailsDefined in Propositional.Logic_Propositional MethodsparsersAndPrinters :: Propositional -> Map String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc) Source #parse_basic_spec :: Propositional -> Maybe (PrefixMap -> AParser st BASIC_SPEC) Source #parseSingleSymbItem :: Propositional -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source #parse_symb_items :: Propositional -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source #symb_items_name :: Propositional -> SYMB_ITEMS -> [String] Source # Source # Static Analysis for propositional logic Instance detailsDefined in Propositional.Logic_Propositional Methodsbasic_analysis :: Propositional -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])) Source #sen_analysis :: Propositional -> Maybe ((BASIC_SPEC, Sign, FORMULA) -> Result FORMULA) Source #stat_symb_map_items :: Propositional -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source #convertTheory :: Propositional -> Maybe ((Sign, [Named FORMULA]) -> BASIC_SPEC) Source #ensures_amalgamability :: Propositional -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #signature_colimit :: Propositional -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #matches :: Propositional -> Symbol -> Symbol -> Bool Source #is_subsig :: Propositional -> Sign -> Sign -> Bool Source #is_transportable :: Propositional -> Morphism -> Bool Source #is_injective :: Propositional -> Morphism -> Bool Source #corresp2th :: Propositional -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #equiv2cospan :: Propositional -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #extract_module :: Propositional -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source # Source # Instance of Logic for propositional logc Instance detailsDefined in Propositional.Logic_Propositional Methodsparse_basic_sen :: Propositional -> Maybe (BASIC_SPEC -> AParser st FORMULA) Source #data_logic :: Propositional -> Maybe AnyLogic Source #bottomSublogic :: Propositional -> Maybe PropSL Source #parseSublogic :: Propositional -> String -> Maybe PropSL Source #default_prover :: Propositional -> String Source #syntaxTable :: Propositional -> Sign -> Maybe SyntaxTable Source #omdoc_metatheory :: Propositional -> Maybe OMCD Source #export_symToOmdoc :: Propositional -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #omdocToSym :: Propositional -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #omdocToSen :: Propositional -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source #addOMadtToTheory :: Propositional -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source #addOmdocToTheory :: Propositional -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source #sublogicOfTheo :: Propositional -> (Sign, [FORMULA]) -> PropSL Source # Source # Instance detailsDefined in OWL2.Propositional2OWL2 MethodsminSourceTheory :: Propositional2OWL2 -> Maybe (LibName, String) Source #map_theory :: Propositional2OWL2 -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named Axiom]) Source #mapMarkedTheory :: Propositional2OWL2 -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named Axiom]) Source #constituents :: Propositional2OWL2 -> [String] Source #rps :: Propositional2OWL2 -> Bool Source #eps :: Propositional2OWL2 -> Bool Source #isGTC :: Propositional2OWL2 -> Bool Source # Source # Instance detailsDefined in Comorphisms.QBF2Prop MethodsminSourceTheory :: QBF2Prop -> Maybe (LibName, String) Source #mapSublogic :: QBF2Prop -> QBFSL -> Maybe PropSL Source #map_theory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA0]) Source #mapMarkedTheory :: QBF2Prop -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA0]) Source #map_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol0 Source #has_model_expansion :: QBF2Prop -> Bool Source #is_weakly_amalgamable :: QBF2Prop -> Bool Source #constituents :: QBF2Prop -> [String] Source #isInclusionComorphism :: QBF2Prop -> Bool Source #rps :: QBF2Prop -> Bool Source #eps :: QBF2Prop -> Bool Source #isGTC :: QBF2Prop -> Bool Source # Source # Instance detailsDefined in Comorphisms.Prop2QBF MethodsminSourceTheory :: Prop2QBF -> Maybe (LibName, String) Source #mapSublogic :: Prop2QBF -> PropSL -> Maybe QBFSL Source #map_theory :: Prop2QBF -> (Sign, [Named FORMULA0]) -> Result (Sign, [Named FORMULA]) Source #mapMarkedTheory :: Prop2QBF -> (Sign, [Named FORMULA0]) -> Result (Sign, [Named FORMULA]) Source #map_symbol :: Prop2QBF -> Sign -> Symbol0 -> Set Symbol Source #has_model_expansion :: Prop2QBF -> Bool Source #is_weakly_amalgamable :: Prop2QBF -> Bool Source #constituents :: Prop2QBF -> [String] Source #isInclusionComorphism :: Prop2QBF -> Bool Source #rps :: Prop2QBF -> Bool Source #eps :: Prop2QBF -> Bool Source #isGTC :: Prop2QBF -> Bool Source # Source # Instance detailsDefined in Comorphisms.Prop2CommonLogic MethodsminSourceTheory :: Prop2CommonLogic -> Maybe (LibName, String) Source #map_theory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source #mapMarkedTheory :: Prop2CommonLogic -> (Sign, [Named FORMULA]) -> Result (Sign0, [Named TEXT_META]) Source #constituents :: Prop2CommonLogic -> [String] Source #rps :: Prop2CommonLogic -> Bool Source #eps :: Prop2CommonLogic -> Bool Source #isGTC :: Prop2CommonLogic -> Bool Source # Source # Instance detailsDefined in Comorphisms.Prop2CASL MethodsminSourceTheory :: Prop2CASL -> Maybe (LibName, String) Source #mapSublogic :: Prop2CASL -> PropSL -> Maybe CASL_Sublogics Source #map_theory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #mapMarkedTheory :: Prop2CASL -> (Sign, [Named FORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #map_symbol :: Prop2CASL -> Sign -> Symbol -> Set Symbol0 Source #has_model_expansion :: Prop2CASL -> Bool Source #constituents :: Prop2CASL -> [String] Source #rps :: Prop2CASL -> Bool Source #eps :: Prop2CASL -> Bool Source #isGTC :: Prop2CASL -> Bool Source # Source # Instance detailsDefined in Comorphisms.CASL2Prop MethodsminSourceTheory :: CASL2Prop -> Maybe (LibName, String) Source #mapSublogic :: CASL2Prop -> CASL_Sublogics -> Maybe PropSL Source #map_theory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source #mapMarkedTheory :: CASL2Prop -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named FORMULA]) Source #map_symbol :: CASL2Prop -> CASLSign -> Symbol0 -> Set Symbol Source #has_model_expansion :: CASL2Prop -> Bool Source #constituents :: CASL2Prop -> [String] Source #rps :: CASL2Prop -> Bool Source #eps :: CASL2Prop -> Bool Source #isGTC :: CASL2Prop -> Bool Source # type Rep SYMB_MAP_ITEMS Instance detailsDefined in Propositional.ATC_Propositional type Rep SYMB_MAP_ITEMS = D1 ('MetaData "SYMB_MAP_ITEMS" "Propositional.AS_BASIC_Propositional" "main" 'False) (C1 ('MetaCons "Symb_map_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SYMB_OR_MAP]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

Constructors

 Symb SYMB Symb_map SYMB SYMB Range

#### Instances

Instances details
 Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methods(==) :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool(/=) :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool Data SYMB_OR_MAP Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB_OR_MAP -> c SYMB_OR_MAPgunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMB_OR_MAPtoConstr :: SYMB_OR_MAP -> ConstrdataTypeOf :: SYMB_OR_MAP -> DataTypedataCast1 :: 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_MAPgmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_OR_MAP -> rgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_OR_MAP -> rgmapQ :: (forall d. Data d => d -> u) -> SYMB_OR_MAP -> [u]gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_OR_MAP -> ugmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAPgmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAPgmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP Ord SYMB_OR_MAP Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodscompare :: 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 Show SYMB_OR_MAP Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional MethodsshowsPrec :: Int -> SYMB_OR_MAP -> ShowSshow :: SYMB_OR_MAP -> StringshowList :: [SYMB_OR_MAP] -> ShowS Generic SYMB_OR_MAP Instance detailsDefined in Propositional.ATC_Propositional Associated Typestype Rep SYMB_OR_MAP :: Type -> Type Methodsfrom :: SYMB_OR_MAP -> Rep SYMB_OR_MAP xto :: Rep SYMB_OR_MAP x -> SYMB_OR_MAP Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methods FromJSON SYMB_OR_MAP Instance detailsDefined in Propositional.ATC_Propositional MethodsparseJSON :: Value -> Parser SYMB_OR_MAPparseJSONList :: Value -> Parser [SYMB_OR_MAP] ToJSON SYMB_OR_MAP Instance detailsDefined in Propositional.ATC_Propositional MethodstoJSON :: SYMB_OR_MAP -> ValuetoEncoding :: SYMB_OR_MAP -> EncodingtoJSONList :: [SYMB_OR_MAP] -> ValuetoEncodingList :: [SYMB_OR_MAP] -> Encoding ShATermConvertible SYMB_OR_MAP Instance detailsDefined in Propositional.ATC_Propositional MethodstoShATermAux :: 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]) Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodspretties :: [SYMB_OR_MAP] -> Doc Source # type Rep SYMB_OR_MAP Instance detailsDefined 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))))

data PRED_ITEM Source #

predicates = propotions

Constructors

 Pred_item [Token] Range

#### Instances

Instances details
 Data PRED_ITEM Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PRED_ITEM -> c PRED_ITEMgunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PRED_ITEMtoConstr :: PRED_ITEM -> ConstrdataTypeOf :: PRED_ITEM -> DataTypedataCast1 :: 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_ITEMgmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PRED_ITEM -> rgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PRED_ITEM -> rgmapQ :: (forall d. Data d => d -> u) -> PRED_ITEM -> [u]gmapQi :: Int -> (forall d. Data d => d -> u) -> PRED_ITEM -> ugmapM :: Monad m => (forall d. Data d => d -> m d) -> PRED_ITEM -> m PRED_ITEMgmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PRED_ITEM -> m PRED_ITEMgmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PRED_ITEM -> m PRED_ITEM Show PRED_ITEM Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional MethodsshowsPrec :: Int -> PRED_ITEM -> ShowSshow :: PRED_ITEM -> StringshowList :: [PRED_ITEM] -> ShowS Generic PRED_ITEM Instance detailsDefined in Propositional.ATC_Propositional Associated Typestype Rep PRED_ITEM :: Type -> Type Methodsfrom :: PRED_ITEM -> Rep PRED_ITEM xto :: Rep PRED_ITEM x -> PRED_ITEM Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional MethodsrangeSpan :: PRED_ITEM -> [Pos] Source # FromJSON PRED_ITEM Instance detailsDefined in Propositional.ATC_Propositional MethodsparseJSON :: Value -> Parser PRED_ITEMparseJSONList :: Value -> Parser [PRED_ITEM] ToJSON PRED_ITEM Instance detailsDefined in Propositional.ATC_Propositional MethodstoJSON :: PRED_ITEM -> ValuetoEncoding :: PRED_ITEM -> EncodingtoJSONList :: [PRED_ITEM] -> ValuetoEncodingList :: [PRED_ITEM] -> Encoding ShATermConvertible PRED_ITEM Instance detailsDefined in Propositional.ATC_Propositional MethodstoShATermAux :: 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]) Source # Instance detailsDefined in Propositional.AS_BASIC_Propositional Methodspretties :: [PRED_ITEM] -> Doc Source # type Rep PRED_ITEM Instance detailsDefined 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)))