Copyright	(c) Jonathan von Schroeder DFKI GmbH 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	<jonathan.von_schroeder@dfki.de>
Stability	experimental
Portability	portable
Safe Haskell	Safe

QBF.AS_BASIC_QBF

Description

Definition of abstract syntax for propositional logic extended with QBFs

Ref. http://en.wikipedia.org/wiki/Propositional_logic http://www.voronkov.com/lics.cgi

Synopsis

data FORMULA
- = FalseAtom Range
- | TrueAtom Range
- | Predication Token
- | Negation FORMULA Range
- | Conjunction [FORMULA] Range
- | Disjunction [FORMULA] Range
- | Implication FORMULA FORMULA Range
- | Equivalence FORMULA FORMULA Range
- | ForAll [Token] FORMULA Range
- | Exists [Token] FORMULA Range
data BASICITEMS
- = PredDecl PREDITEM
- | AxiomItems [Annoted FORMULA]
newtype BASICSPEC = BasicSpec [Annoted BASICITEMS]
data SYMBITEMS = SymbItems [SYMB] Range
newtype SYMB = SymbId Token
data SYMBMAPITEMS = SymbMapItems [SYMBORMAP] Range
data SYMBORMAP
- = Symb SYMB
- | SymbMap SYMB SYMB Range
data PREDITEM = PredItem [Token] Range
isPrimForm :: FORMULA -> Bool
data ID = ID Token (Maybe Token)

Documentation

data FORMULA Source #

Datatype for QBF formulas

Instances

Instances details

Eq FORMULA Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods (==) :: FORMULA -> FORMULA -> Bool (/=) :: FORMULA -> FORMULA -> Bool
Data FORMULA Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FORMULA -> c FORMULA gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FORMULA toConstr :: FORMULA -> Constr dataTypeOf :: FORMULA -> DataType dataCast1 :: 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 -> FORMULA gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FORMULA -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FORMULA -> r gmapQ :: (forall d. Data d => d -> u) -> FORMULA -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FORMULA -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FORMULA -> m FORMULA
Ord FORMULA Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods compare :: FORMULA -> FORMULA -> Ordering (<) :: FORMULA -> FORMULA -> Bool (<=) :: FORMULA -> FORMULA -> Bool (>) :: FORMULA -> FORMULA -> Bool (>=) :: FORMULA -> FORMULA -> Bool max :: FORMULA -> FORMULA -> FORMULA min :: FORMULA -> FORMULA -> FORMULA
Show FORMULA Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods showsPrec :: Int -> FORMULA -> ShowS show :: FORMULA -> String showList :: [FORMULA] -> ShowS
Generic FORMULA
Instance details Defined in QBF.ATC_QBF Associated Types type Rep FORMULA :: Type -> Type Methods from :: FORMULA -> Rep FORMULA x to :: Rep FORMULA x -> FORMULA
GetRange FORMULA Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods getRange :: FORMULA -> Range Source # rangeSpan :: FORMULA -> [Pos] Source #
FromJSON FORMULA
Instance details Defined in QBF.ATC_QBF Methods parseJSON :: Value -> Parser FORMULA parseJSONList :: Value -> Parser [FORMULA]
ToJSON FORMULA
Instance details Defined in QBF.ATC_QBF Methods toJSON :: FORMULA -> Value toEncoding :: FORMULA -> Encoding toJSONList :: [FORMULA] -> Value toEncodingList :: [FORMULA] -> Encoding
ShATermConvertible FORMULA
Instance details Defined in QBF.ATC_QBF Methods toShATermAux :: ATermTable -> FORMULA -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FORMULA] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FORMULA) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FORMULA])
Pretty FORMULA Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods pretty :: FORMULA -> Doc Source # pretties :: [FORMULA] -> Doc Source #
ProjectSublogicM QBFSL FORMULA Source #
Instance details Defined in QBF.Logic_QBF Methods projectSublogicM :: QBFSL -> FORMULA -> Maybe FORMULA Source #
MinSublogic QBFSL FORMULA Source #
Instance details Defined in QBF.Logic_QBF Methods minSublogic :: FORMULA -> QBFSL Source #
Sentences QBF FORMULA Sign Morphism Symbol Source #	Instance of Sentences for propositional logic
Instance details Defined in QBF.Logic_QBF Methods map_sen :: QBF -> Morphism -> FORMULA -> Result FORMULA Source # simplify_sen :: QBF -> Sign -> FORMULA -> FORMULA Source # negation :: QBF -> FORMULA -> Maybe FORMULA Source # print_sign :: QBF -> Sign -> Doc Source # print_named :: QBF -> Named FORMULA -> Doc Source # sym_of :: QBF -> Sign -> [Set Symbol] Source # mostSymsOf :: QBF -> Sign -> [Symbol] Source # symmap_of :: QBF -> Morphism -> EndoMap Symbol Source # sym_name :: QBF -> Symbol -> Id Source # sym_label :: QBF -> Symbol -> Maybe String Source # fullSymName :: QBF -> Symbol -> String Source # symKind :: QBF -> Symbol -> String Source # symsOfSen :: QBF -> Sign -> FORMULA -> [Symbol] Source # pair_symbols :: QBF -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis QBF BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol Source #	Static Analysis for propositional logic
Instance details Defined in QBF.Logic_QBF Methods basic_analysis :: QBF -> Maybe ((BASICSPEC, Sign, GlobalAnnos) -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])) Source # sen_analysis :: QBF -> Maybe ((BASICSPEC, Sign, FORMULA) -> Result FORMULA) Source # extBasicAnalysis :: QBF -> IRI -> LibName -> BASICSPEC -> Sign -> GlobalAnnos -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA]) Source # stat_symb_map_items :: QBF -> Sign -> Maybe Sign -> [SYMBMAPITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: QBF -> Sign -> [SYMBITEMS] -> Result [Symbol] Source # convertTheory :: QBF -> Maybe ((Sign, [Named FORMULA]) -> BASICSPEC) Source # ensures_amalgamability :: QBF -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: QBF -> Morphism -> [Named FORMULA] -> Result (Sign, [Named FORMULA]) Source # signature_colimit :: QBF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: QBF -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named FORMULA]) Source # symbol_to_raw :: QBF -> Symbol -> Symbol Source # id_to_raw :: QBF -> Id -> Symbol Source # matches :: QBF -> Symbol -> Symbol -> Bool Source # empty_signature :: QBF -> Sign Source # add_symb_to_sign :: QBF -> Sign -> Symbol -> Result Sign Source # signature_union :: QBF -> Sign -> Sign -> Result Sign Source # signatureDiff :: QBF -> Sign -> Sign -> Result Sign Source # intersection :: QBF -> Sign -> Sign -> Result Sign Source # final_union :: QBF -> Sign -> Sign -> Result Sign Source # morphism_union :: QBF -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: QBF -> Sign -> Sign -> Bool Source # subsig_inclusion :: QBF -> Sign -> Sign -> Result Morphism Source # generated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: QBF -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: QBF -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: QBF -> Morphism -> Bool Source # is_injective :: QBF -> Morphism -> Bool Source # theory_to_taxonomy :: QBF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named FORMULA] -> Result MMiSSOntology Source # corresp2th :: QBF -> String -> Bool -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: QBF -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: QBF -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source #
Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source #	Instance of Logic for propositional logc
Instance details Defined in QBF.Logic_QBF Methods parse_basic_sen :: QBF -> Maybe (BASICSPEC -> AParser st FORMULA) Source # stability :: QBF -> Stability Source # data_logic :: QBF -> Maybe AnyLogic Source # top_sublogic :: QBF -> QBFSL Source # all_sublogics :: QBF -> [QBFSL] Source # bottomSublogic :: QBF -> Maybe QBFSL Source # sublogicDimensions :: QBF -> [[QBFSL]] Source # parseSublogic :: QBF -> String -> Maybe QBFSL Source # proj_sublogic_epsilon :: QBF -> QBFSL -> Sign -> Morphism Source # provers :: QBF -> [Prover Sign FORMULA Morphism QBFSL ProofTree] Source # default_prover :: QBF -> String Source # cons_checkers :: QBF -> [ConsChecker Sign FORMULA QBFSL Morphism ProofTree] Source # conservativityCheck :: QBF -> [ConservativityChecker Sign FORMULA Morphism] Source # empty_proof_tree :: QBF -> ProofTree Source # syntaxTable :: QBF -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: QBF -> Maybe OMCD Source # export_symToOmdoc :: QBF -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: QBF -> NameMap Symbol -> FORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: QBF -> SigMap Symbol -> Sign -> [Named FORMULA] -> Result [TCElement] Source # omdocToSym :: QBF -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: QBF -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source # addOMadtToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source # addOmdocToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source # sublogicOfTheo :: QBF -> (Sign, [FORMULA]) -> QBFSL Source #
Comorphism QBF2Prop QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.QBF2Prop Methods sourceLogic :: QBF2Prop -> QBF Source # sourceSublogic :: QBF2Prop -> QBFSL Source # sourceSublogicLossy :: QBF2Prop -> QBFSL Source # minSourceTheory :: QBF2Prop -> Maybe (LibName, String) Source # targetLogic :: QBF2Prop -> Propositional 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_morphism :: QBF2Prop -> Morphism -> Result Morphism0 Source # map_sentence :: QBF2Prop -> Sign -> FORMULA -> Result FORMULA0 Source # map_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: QBF2Prop -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source # is_model_transportable :: QBF2Prop -> Bool 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 #
Comorphism Prop2QBF Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.Prop2QBF Methods sourceLogic :: Prop2QBF -> Propositional Source # sourceSublogic :: Prop2QBF -> PropSL Source # sourceSublogicLossy :: Prop2QBF -> PropSL Source # minSourceTheory :: Prop2QBF -> Maybe (LibName, String) Source # targetLogic :: Prop2QBF -> QBF 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_morphism :: Prop2QBF -> Morphism0 -> Result Morphism Source # map_sentence :: Prop2QBF -> Sign -> FORMULA0 -> Result FORMULA Source # map_symbol :: Prop2QBF -> Sign -> Symbol0 -> Set Symbol Source # extractModel :: Prop2QBF -> Sign -> ProofTree -> Result (Sign, [Named FORMULA0]) Source # is_model_transportable :: Prop2QBF -> Bool 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 #
type Rep FORMULA
Instance details Defined in QBF.ATC_QBF type Rep FORMULA = D1 ('MetaData "FORMULA" "QBF.AS_BASIC_QBF" "main" 'False) (((C1 ('MetaCons "FalseAtom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "TrueAtom" '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))) :+: (C1 ('MetaCons "ForAll" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Token]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FORMULA) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Exists" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Token]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FORMULA) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))))))

data BASICITEMS Source #

Constructors

PredDecl PREDITEM
AxiomItems [Annoted FORMULA]

Instances

Instances details

Data BASICITEMS Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BASICITEMS -> c BASICITEMS gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BASICITEMS toConstr :: BASICITEMS -> Constr dataTypeOf :: BASICITEMS -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BASICITEMS) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASICITEMS) gmapT :: (forall b. Data b => b -> b) -> BASICITEMS -> BASICITEMS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASICITEMS -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASICITEMS -> r gmapQ :: (forall d. Data d => d -> u) -> BASICITEMS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BASICITEMS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASICITEMS -> m BASICITEMS
Show BASICITEMS Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods showsPrec :: Int -> BASICITEMS -> ShowS show :: BASICITEMS -> String showList :: [BASICITEMS] -> ShowS
Generic BASICITEMS
Instance details Defined in QBF.ATC_QBF Associated Types type Rep BASICITEMS :: Type -> Type Methods from :: BASICITEMS -> Rep BASICITEMS x to :: Rep BASICITEMS x -> BASICITEMS
GetRange BASICITEMS Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods getRange :: BASICITEMS -> Range Source # rangeSpan :: BASICITEMS -> [Pos] Source #
FromJSON BASICITEMS
Instance details Defined in QBF.ATC_QBF Methods parseJSON :: Value -> Parser BASICITEMS parseJSONList :: Value -> Parser [BASICITEMS]
ToJSON BASICITEMS
Instance details Defined in QBF.ATC_QBF Methods toJSON :: BASICITEMS -> Value toEncoding :: BASICITEMS -> Encoding toJSONList :: [BASICITEMS] -> Value toEncodingList :: [BASICITEMS] -> Encoding
ShATermConvertible BASICITEMS
Instance details Defined in QBF.ATC_QBF Methods toShATermAux :: ATermTable -> BASICITEMS -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [BASICITEMS] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, BASICITEMS) fromShATermList' :: Int -> ATermTable -> (ATermTable, [BASICITEMS])
Pretty BASICITEMS Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods pretty :: BASICITEMS -> Doc Source # pretties :: [BASICITEMS] -> Doc Source #
type Rep BASICITEMS
Instance details Defined in QBF.ATC_QBF type Rep BASICITEMS = D1 ('MetaData "BASICITEMS" "QBF.AS_BASIC_QBF" "main" 'False) (C1 ('MetaCons "PredDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PREDITEM)) :+: C1 ('MetaCons "AxiomItems" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted FORMULA])))

newtype BASICSPEC Source #

Constructors

BasicSpec [Annoted BASICITEMS]

Instances

Instances details

Data BASICSPEC Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BASICSPEC -> c BASICSPEC gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BASICSPEC toConstr :: BASICSPEC -> Constr dataTypeOf :: BASICSPEC -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BASICSPEC) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASICSPEC) gmapT :: (forall b. Data b => b -> b) -> BASICSPEC -> BASICSPEC gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASICSPEC -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASICSPEC -> r gmapQ :: (forall d. Data d => d -> u) -> BASICSPEC -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BASICSPEC -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASICSPEC -> m BASICSPEC
Show BASICSPEC Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods showsPrec :: Int -> BASICSPEC -> ShowS show :: BASICSPEC -> String showList :: [BASICSPEC] -> ShowS
Generic BASICSPEC
Instance details Defined in QBF.ATC_QBF Associated Types type Rep BASICSPEC :: Type -> Type Methods from :: BASICSPEC -> Rep BASICSPEC x to :: Rep BASICSPEC x -> BASICSPEC
Semigroup BASICSPEC
Instance details Defined in QBF.Logic_QBF Methods (<>) :: BASICSPEC -> BASICSPEC -> BASICSPEC # sconcat :: NonEmpty BASICSPEC -> BASICSPEC stimes :: Integral b => b -> BASICSPEC -> BASICSPEC
Monoid BASICSPEC
Instance details Defined in QBF.Logic_QBF Methods mempty :: BASICSPEC mappend :: BASICSPEC -> BASICSPEC -> BASICSPEC mconcat :: [BASICSPEC] -> BASICSPEC
GetRange BASICSPEC Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods getRange :: BASICSPEC -> Range Source # rangeSpan :: BASICSPEC -> [Pos] Source #
FromJSON BASICSPEC
Instance details Defined in QBF.ATC_QBF Methods parseJSON :: Value -> Parser BASICSPEC parseJSONList :: Value -> Parser [BASICSPEC]
ToJSON BASICSPEC
Instance details Defined in QBF.ATC_QBF Methods toJSON :: BASICSPEC -> Value toEncoding :: BASICSPEC -> Encoding toJSONList :: [BASICSPEC] -> Value toEncodingList :: [BASICSPEC] -> Encoding
ShATermConvertible BASICSPEC
Instance details Defined in QBF.ATC_QBF Methods toShATermAux :: ATermTable -> BASICSPEC -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [BASICSPEC] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, BASICSPEC) fromShATermList' :: Int -> ATermTable -> (ATermTable, [BASICSPEC])
Pretty BASICSPEC Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods pretty :: BASICSPEC -> Doc Source # pretties :: [BASICSPEC] -> Doc Source #
ProjectSublogic QBFSL BASICSPEC Source #
Instance details Defined in QBF.Logic_QBF Methods projectSublogic :: QBFSL -> BASICSPEC -> BASICSPEC Source #
MinSublogic QBFSL BASICSPEC Source #
Instance details Defined in QBF.Logic_QBF Methods minSublogic :: BASICSPEC -> QBFSL Source #
Syntax QBF BASICSPEC Symbol SYMBITEMS SYMBMAPITEMS Source #	Syntax of Propositional logic
Instance details Defined in QBF.Logic_QBF Methods parsersAndPrinters :: QBF -> Map String (PrefixMap -> AParser st BASICSPEC, BASICSPEC -> Doc) Source # parse_basic_spec :: QBF -> Maybe (PrefixMap -> AParser st BASICSPEC) Source # parseSingleSymbItem :: QBF -> Maybe (PrefixMap -> AParser st SYMBITEMS) Source # parse_symb_items :: QBF -> Maybe (PrefixMap -> AParser st SYMBITEMS) Source # parse_symb_map_items :: QBF -> Maybe (PrefixMap -> AParser st SYMBMAPITEMS) Source # toItem :: QBF -> BASICSPEC -> Item Source # symb_items_name :: QBF -> SYMBITEMS -> [String] Source #
StaticAnalysis QBF BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol Source #	Static Analysis for propositional logic
Instance details Defined in QBF.Logic_QBF Methods basic_analysis :: QBF -> Maybe ((BASICSPEC, Sign, GlobalAnnos) -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])) Source # sen_analysis :: QBF -> Maybe ((BASICSPEC, Sign, FORMULA) -> Result FORMULA) Source # extBasicAnalysis :: QBF -> IRI -> LibName -> BASICSPEC -> Sign -> GlobalAnnos -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA]) Source # stat_symb_map_items :: QBF -> Sign -> Maybe Sign -> [SYMBMAPITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: QBF -> Sign -> [SYMBITEMS] -> Result [Symbol] Source # convertTheory :: QBF -> Maybe ((Sign, [Named FORMULA]) -> BASICSPEC) Source # ensures_amalgamability :: QBF -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: QBF -> Morphism -> [Named FORMULA] -> Result (Sign, [Named FORMULA]) Source # signature_colimit :: QBF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: QBF -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named FORMULA]) Source # symbol_to_raw :: QBF -> Symbol -> Symbol Source # id_to_raw :: QBF -> Id -> Symbol Source # matches :: QBF -> Symbol -> Symbol -> Bool Source # empty_signature :: QBF -> Sign Source # add_symb_to_sign :: QBF -> Sign -> Symbol -> Result Sign Source # signature_union :: QBF -> Sign -> Sign -> Result Sign Source # signatureDiff :: QBF -> Sign -> Sign -> Result Sign Source # intersection :: QBF -> Sign -> Sign -> Result Sign Source # final_union :: QBF -> Sign -> Sign -> Result Sign Source # morphism_union :: QBF -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: QBF -> Sign -> Sign -> Bool Source # subsig_inclusion :: QBF -> Sign -> Sign -> Result Morphism Source # generated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: QBF -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: QBF -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: QBF -> Morphism -> Bool Source # is_injective :: QBF -> Morphism -> Bool Source # theory_to_taxonomy :: QBF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named FORMULA] -> Result MMiSSOntology Source # corresp2th :: QBF -> String -> Bool -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: QBF -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: QBF -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source #
Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source #	Instance of Logic for propositional logc
Instance details Defined in QBF.Logic_QBF Methods parse_basic_sen :: QBF -> Maybe (BASICSPEC -> AParser st FORMULA) Source # stability :: QBF -> Stability Source # data_logic :: QBF -> Maybe AnyLogic Source # top_sublogic :: QBF -> QBFSL Source # all_sublogics :: QBF -> [QBFSL] Source # bottomSublogic :: QBF -> Maybe QBFSL Source # sublogicDimensions :: QBF -> [[QBFSL]] Source # parseSublogic :: QBF -> String -> Maybe QBFSL Source # proj_sublogic_epsilon :: QBF -> QBFSL -> Sign -> Morphism Source # provers :: QBF -> [Prover Sign FORMULA Morphism QBFSL ProofTree] Source # default_prover :: QBF -> String Source # cons_checkers :: QBF -> [ConsChecker Sign FORMULA QBFSL Morphism ProofTree] Source # conservativityCheck :: QBF -> [ConservativityChecker Sign FORMULA Morphism] Source # empty_proof_tree :: QBF -> ProofTree Source # syntaxTable :: QBF -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: QBF -> Maybe OMCD Source # export_symToOmdoc :: QBF -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: QBF -> NameMap Symbol -> FORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: QBF -> SigMap Symbol -> Sign -> [Named FORMULA] -> Result [TCElement] Source # omdocToSym :: QBF -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: QBF -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source # addOMadtToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source # addOmdocToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source # sublogicOfTheo :: QBF -> (Sign, [FORMULA]) -> QBFSL Source #
Comorphism QBF2Prop QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.QBF2Prop Methods sourceLogic :: QBF2Prop -> QBF Source # sourceSublogic :: QBF2Prop -> QBFSL Source # sourceSublogicLossy :: QBF2Prop -> QBFSL Source # minSourceTheory :: QBF2Prop -> Maybe (LibName, String) Source # targetLogic :: QBF2Prop -> Propositional 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_morphism :: QBF2Prop -> Morphism -> Result Morphism0 Source # map_sentence :: QBF2Prop -> Sign -> FORMULA -> Result FORMULA0 Source # map_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: QBF2Prop -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source # is_model_transportable :: QBF2Prop -> Bool 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 #
Comorphism Prop2QBF Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.Prop2QBF Methods sourceLogic :: Prop2QBF -> Propositional Source # sourceSublogic :: Prop2QBF -> PropSL Source # sourceSublogicLossy :: Prop2QBF -> PropSL Source # minSourceTheory :: Prop2QBF -> Maybe (LibName, String) Source # targetLogic :: Prop2QBF -> QBF 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_morphism :: Prop2QBF -> Morphism0 -> Result Morphism Source # map_sentence :: Prop2QBF -> Sign -> FORMULA0 -> Result FORMULA Source # map_symbol :: Prop2QBF -> Sign -> Symbol0 -> Set Symbol Source # extractModel :: Prop2QBF -> Sign -> ProofTree -> Result (Sign, [Named FORMULA0]) Source # is_model_transportable :: Prop2QBF -> Bool 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 #
type Rep BASICSPEC
Instance details Defined in QBF.ATC_QBF type Rep BASICSPEC = D1 ('MetaData "BASICSPEC" "QBF.AS_BASIC_QBF" "main" 'True) (C1 ('MetaCons "BasicSpec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted BASICITEMS])))

data SYMBITEMS Source #

Constructors

SymbItems [SYMB] Range

Instances

Instances details

Eq SYMBITEMS Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods (==) :: SYMBITEMS -> SYMBITEMS -> Bool (/=) :: SYMBITEMS -> SYMBITEMS -> Bool
Data SYMBITEMS Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMBITEMS -> c SYMBITEMS gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMBITEMS toConstr :: SYMBITEMS -> Constr dataTypeOf :: SYMBITEMS -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SYMBITEMS) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMBITEMS) gmapT :: (forall b. Data b => b -> b) -> SYMBITEMS -> SYMBITEMS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMBITEMS -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMBITEMS -> r gmapQ :: (forall d. Data d => d -> u) -> SYMBITEMS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMBITEMS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMBITEMS -> m SYMBITEMS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMBITEMS -> m SYMBITEMS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMBITEMS -> m SYMBITEMS
Ord SYMBITEMS Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods compare :: SYMBITEMS -> SYMBITEMS -> Ordering (<) :: SYMBITEMS -> SYMBITEMS -> Bool (<=) :: SYMBITEMS -> SYMBITEMS -> Bool (>) :: SYMBITEMS -> SYMBITEMS -> Bool (>=) :: SYMBITEMS -> SYMBITEMS -> Bool max :: SYMBITEMS -> SYMBITEMS -> SYMBITEMS min :: SYMBITEMS -> SYMBITEMS -> SYMBITEMS
Show SYMBITEMS Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods showsPrec :: Int -> SYMBITEMS -> ShowS show :: SYMBITEMS -> String showList :: [SYMBITEMS] -> ShowS
Generic SYMBITEMS
Instance details Defined in QBF.ATC_QBF Associated Types type Rep SYMBITEMS :: Type -> Type Methods from :: SYMBITEMS -> Rep SYMBITEMS x to :: Rep SYMBITEMS x -> SYMBITEMS
GetRange SYMBITEMS Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods getRange :: SYMBITEMS -> Range Source # rangeSpan :: SYMBITEMS -> [Pos] Source #
FromJSON SYMBITEMS
Instance details Defined in QBF.ATC_QBF Methods parseJSON :: Value -> Parser SYMBITEMS parseJSONList :: Value -> Parser [SYMBITEMS]
ToJSON SYMBITEMS
Instance details Defined in QBF.ATC_QBF Methods toJSON :: SYMBITEMS -> Value toEncoding :: SYMBITEMS -> Encoding toJSONList :: [SYMBITEMS] -> Value toEncodingList :: [SYMBITEMS] -> Encoding
ShATermConvertible SYMBITEMS
Instance details Defined in QBF.ATC_QBF Methods toShATermAux :: ATermTable -> SYMBITEMS -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SYMBITEMS] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMBITEMS) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SYMBITEMS])
Pretty SYMBITEMS Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods pretty :: SYMBITEMS -> Doc Source # pretties :: [SYMBITEMS] -> Doc Source #
ProjectSublogicM QBFSL SYMBITEMS Source #
Instance details Defined in QBF.Logic_QBF Methods projectSublogicM :: QBFSL -> SYMBITEMS -> Maybe SYMBITEMS Source #
MinSublogic QBFSL SYMBITEMS Source #
Instance details Defined in QBF.Logic_QBF Methods minSublogic :: SYMBITEMS -> QBFSL Source #
Syntax QBF BASICSPEC Symbol SYMBITEMS SYMBMAPITEMS Source #	Syntax of Propositional logic
Instance details Defined in QBF.Logic_QBF Methods parsersAndPrinters :: QBF -> Map String (PrefixMap -> AParser st BASICSPEC, BASICSPEC -> Doc) Source # parse_basic_spec :: QBF -> Maybe (PrefixMap -> AParser st BASICSPEC) Source # parseSingleSymbItem :: QBF -> Maybe (PrefixMap -> AParser st SYMBITEMS) Source # parse_symb_items :: QBF -> Maybe (PrefixMap -> AParser st SYMBITEMS) Source # parse_symb_map_items :: QBF -> Maybe (PrefixMap -> AParser st SYMBMAPITEMS) Source # toItem :: QBF -> BASICSPEC -> Item Source # symb_items_name :: QBF -> SYMBITEMS -> [String] Source #
StaticAnalysis QBF BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol Source #	Static Analysis for propositional logic
Instance details Defined in QBF.Logic_QBF Methods basic_analysis :: QBF -> Maybe ((BASICSPEC, Sign, GlobalAnnos) -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])) Source # sen_analysis :: QBF -> Maybe ((BASICSPEC, Sign, FORMULA) -> Result FORMULA) Source # extBasicAnalysis :: QBF -> IRI -> LibName -> BASICSPEC -> Sign -> GlobalAnnos -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA]) Source # stat_symb_map_items :: QBF -> Sign -> Maybe Sign -> [SYMBMAPITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: QBF -> Sign -> [SYMBITEMS] -> Result [Symbol] Source # convertTheory :: QBF -> Maybe ((Sign, [Named FORMULA]) -> BASICSPEC) Source # ensures_amalgamability :: QBF -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: QBF -> Morphism -> [Named FORMULA] -> Result (Sign, [Named FORMULA]) Source # signature_colimit :: QBF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: QBF -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named FORMULA]) Source # symbol_to_raw :: QBF -> Symbol -> Symbol Source # id_to_raw :: QBF -> Id -> Symbol Source # matches :: QBF -> Symbol -> Symbol -> Bool Source # empty_signature :: QBF -> Sign Source # add_symb_to_sign :: QBF -> Sign -> Symbol -> Result Sign Source # signature_union :: QBF -> Sign -> Sign -> Result Sign Source # signatureDiff :: QBF -> Sign -> Sign -> Result Sign Source # intersection :: QBF -> Sign -> Sign -> Result Sign Source # final_union :: QBF -> Sign -> Sign -> Result Sign Source # morphism_union :: QBF -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: QBF -> Sign -> Sign -> Bool Source # subsig_inclusion :: QBF -> Sign -> Sign -> Result Morphism Source # generated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: QBF -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: QBF -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: QBF -> Morphism -> Bool Source # is_injective :: QBF -> Morphism -> Bool Source # theory_to_taxonomy :: QBF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named FORMULA] -> Result MMiSSOntology Source # corresp2th :: QBF -> String -> Bool -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: QBF -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: QBF -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source #
Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source #	Instance of Logic for propositional logc
Instance details Defined in QBF.Logic_QBF Methods parse_basic_sen :: QBF -> Maybe (BASICSPEC -> AParser st FORMULA) Source # stability :: QBF -> Stability Source # data_logic :: QBF -> Maybe AnyLogic Source # top_sublogic :: QBF -> QBFSL Source # all_sublogics :: QBF -> [QBFSL] Source # bottomSublogic :: QBF -> Maybe QBFSL Source # sublogicDimensions :: QBF -> [[QBFSL]] Source # parseSublogic :: QBF -> String -> Maybe QBFSL Source # proj_sublogic_epsilon :: QBF -> QBFSL -> Sign -> Morphism Source # provers :: QBF -> [Prover Sign FORMULA Morphism QBFSL ProofTree] Source # default_prover :: QBF -> String Source # cons_checkers :: QBF -> [ConsChecker Sign FORMULA QBFSL Morphism ProofTree] Source # conservativityCheck :: QBF -> [ConservativityChecker Sign FORMULA Morphism] Source # empty_proof_tree :: QBF -> ProofTree Source # syntaxTable :: QBF -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: QBF -> Maybe OMCD Source # export_symToOmdoc :: QBF -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: QBF -> NameMap Symbol -> FORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: QBF -> SigMap Symbol -> Sign -> [Named FORMULA] -> Result [TCElement] Source # omdocToSym :: QBF -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: QBF -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source # addOMadtToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source # addOmdocToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source # sublogicOfTheo :: QBF -> (Sign, [FORMULA]) -> QBFSL Source #
Comorphism QBF2Prop QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.QBF2Prop Methods sourceLogic :: QBF2Prop -> QBF Source # sourceSublogic :: QBF2Prop -> QBFSL Source # sourceSublogicLossy :: QBF2Prop -> QBFSL Source # minSourceTheory :: QBF2Prop -> Maybe (LibName, String) Source # targetLogic :: QBF2Prop -> Propositional 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_morphism :: QBF2Prop -> Morphism -> Result Morphism0 Source # map_sentence :: QBF2Prop -> Sign -> FORMULA -> Result FORMULA0 Source # map_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: QBF2Prop -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source # is_model_transportable :: QBF2Prop -> Bool 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 #
Comorphism Prop2QBF Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.Prop2QBF Methods sourceLogic :: Prop2QBF -> Propositional Source # sourceSublogic :: Prop2QBF -> PropSL Source # sourceSublogicLossy :: Prop2QBF -> PropSL Source # minSourceTheory :: Prop2QBF -> Maybe (LibName, String) Source # targetLogic :: Prop2QBF -> QBF 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_morphism :: Prop2QBF -> Morphism0 -> Result Morphism Source # map_sentence :: Prop2QBF -> Sign -> FORMULA0 -> Result FORMULA Source # map_symbol :: Prop2QBF -> Sign -> Symbol0 -> Set Symbol Source # extractModel :: Prop2QBF -> Sign -> ProofTree -> Result (Sign, [Named FORMULA0]) Source # is_model_transportable :: Prop2QBF -> Bool 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 #
type Rep SYMBITEMS
Instance details Defined in QBF.ATC_QBF type Rep SYMBITEMS = D1 ('MetaData "SYMBITEMS" "QBF.AS_BASIC_QBF" "main" 'False) (C1 ('MetaCons "SymbItems" '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

SymbId Token

Instances

Instances details

Eq SYMB Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods (==) :: SYMB -> SYMB -> Bool (/=) :: SYMB -> SYMB -> Bool
Data SYMB Source #
Instance details Defined in QBF.AS_BASIC_QBF 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 toConstr :: SYMB -> Constr 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 #
Instance details Defined in QBF.AS_BASIC_QBF Methods compare :: SYMB -> SYMB -> Ordering (<) :: SYMB -> SYMB -> Bool (<=) :: SYMB -> SYMB -> Bool (>) :: SYMB -> SYMB -> Bool (>=) :: SYMB -> SYMB -> Bool max :: SYMB -> SYMB -> SYMB min :: SYMB -> SYMB -> SYMB
Show SYMB Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods showsPrec :: Int -> SYMB -> ShowS show :: SYMB -> String showList :: [SYMB] -> ShowS
Generic SYMB
Instance details Defined in QBF.ATC_QBF Associated Types type Rep SYMB :: Type -> Type Methods from :: SYMB -> Rep SYMB x to :: Rep SYMB x -> SYMB
GetRange SYMB Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods getRange :: SYMB -> Range Source # rangeSpan :: SYMB -> [Pos] Source #
FromJSON SYMB
Instance details Defined in QBF.ATC_QBF Methods parseJSON :: Value -> Parser SYMB parseJSONList :: Value -> Parser [SYMB]
ToJSON SYMB
Instance details Defined in QBF.ATC_QBF Methods toJSON :: SYMB -> Value toEncoding :: SYMB -> Encoding toJSONList :: [SYMB] -> Value toEncodingList :: [SYMB] -> Encoding
ShATermConvertible SYMB
Instance details Defined in QBF.ATC_QBF Methods 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 #
Instance details Defined in QBF.AS_BASIC_QBF Methods pretty :: SYMB -> Doc Source # pretties :: [SYMB] -> Doc Source #
type Rep SYMB
Instance details Defined in QBF.ATC_QBF type Rep SYMB = D1 ('MetaData "SYMB" "QBF.AS_BASIC_QBF" "main" 'True) (C1 ('MetaCons "SymbId" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))

data SYMBMAPITEMS Source #

Constructors

SymbMapItems [SYMBORMAP] Range

Instances

Instances details

Eq SYMBMAPITEMS Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods (==) :: SYMBMAPITEMS -> SYMBMAPITEMS -> Bool (/=) :: SYMBMAPITEMS -> SYMBMAPITEMS -> Bool
Data SYMBMAPITEMS Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMBMAPITEMS -> c SYMBMAPITEMS gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMBMAPITEMS toConstr :: SYMBMAPITEMS -> Constr dataTypeOf :: SYMBMAPITEMS -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SYMBMAPITEMS) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMBMAPITEMS) gmapT :: (forall b. Data b => b -> b) -> SYMBMAPITEMS -> SYMBMAPITEMS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMBMAPITEMS -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMBMAPITEMS -> r gmapQ :: (forall d. Data d => d -> u) -> SYMBMAPITEMS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMBMAPITEMS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMBMAPITEMS -> m SYMBMAPITEMS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMBMAPITEMS -> m SYMBMAPITEMS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMBMAPITEMS -> m SYMBMAPITEMS
Ord SYMBMAPITEMS Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods compare :: SYMBMAPITEMS -> SYMBMAPITEMS -> Ordering (<) :: SYMBMAPITEMS -> SYMBMAPITEMS -> Bool (<=) :: SYMBMAPITEMS -> SYMBMAPITEMS -> Bool (>) :: SYMBMAPITEMS -> SYMBMAPITEMS -> Bool (>=) :: SYMBMAPITEMS -> SYMBMAPITEMS -> Bool max :: SYMBMAPITEMS -> SYMBMAPITEMS -> SYMBMAPITEMS min :: SYMBMAPITEMS -> SYMBMAPITEMS -> SYMBMAPITEMS
Show SYMBMAPITEMS Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods showsPrec :: Int -> SYMBMAPITEMS -> ShowS show :: SYMBMAPITEMS -> String showList :: [SYMBMAPITEMS] -> ShowS
Generic SYMBMAPITEMS
Instance details Defined in QBF.ATC_QBF Associated Types type Rep SYMBMAPITEMS :: Type -> Type Methods from :: SYMBMAPITEMS -> Rep SYMBMAPITEMS x to :: Rep SYMBMAPITEMS x -> SYMBMAPITEMS
GetRange SYMBMAPITEMS Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods getRange :: SYMBMAPITEMS -> Range Source # rangeSpan :: SYMBMAPITEMS -> [Pos] Source #
FromJSON SYMBMAPITEMS
Instance details Defined in QBF.ATC_QBF Methods parseJSON :: Value -> Parser SYMBMAPITEMS parseJSONList :: Value -> Parser [SYMBMAPITEMS]
ToJSON SYMBMAPITEMS
Instance details Defined in QBF.ATC_QBF Methods toJSON :: SYMBMAPITEMS -> Value toEncoding :: SYMBMAPITEMS -> Encoding toJSONList :: [SYMBMAPITEMS] -> Value toEncodingList :: [SYMBMAPITEMS] -> Encoding
ShATermConvertible SYMBMAPITEMS
Instance details Defined in QBF.ATC_QBF Methods toShATermAux :: ATermTable -> SYMBMAPITEMS -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SYMBMAPITEMS] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMBMAPITEMS) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SYMBMAPITEMS])
Pretty SYMBMAPITEMS Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods pretty :: SYMBMAPITEMS -> Doc Source # pretties :: [SYMBMAPITEMS] -> Doc Source #
ProjectSublogicM QBFSL SYMBMAPITEMS Source #
Instance details Defined in QBF.Logic_QBF Methods projectSublogicM :: QBFSL -> SYMBMAPITEMS -> Maybe SYMBMAPITEMS Source #
MinSublogic QBFSL SYMBMAPITEMS Source #
Instance details Defined in QBF.Logic_QBF Methods minSublogic :: SYMBMAPITEMS -> QBFSL Source #
Syntax QBF BASICSPEC Symbol SYMBITEMS SYMBMAPITEMS Source #	Syntax of Propositional logic
Instance details Defined in QBF.Logic_QBF Methods parsersAndPrinters :: QBF -> Map String (PrefixMap -> AParser st BASICSPEC, BASICSPEC -> Doc) Source # parse_basic_spec :: QBF -> Maybe (PrefixMap -> AParser st BASICSPEC) Source # parseSingleSymbItem :: QBF -> Maybe (PrefixMap -> AParser st SYMBITEMS) Source # parse_symb_items :: QBF -> Maybe (PrefixMap -> AParser st SYMBITEMS) Source # parse_symb_map_items :: QBF -> Maybe (PrefixMap -> AParser st SYMBMAPITEMS) Source # toItem :: QBF -> BASICSPEC -> Item Source # symb_items_name :: QBF -> SYMBITEMS -> [String] Source #
StaticAnalysis QBF BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol Source #	Static Analysis for propositional logic
Instance details Defined in QBF.Logic_QBF Methods basic_analysis :: QBF -> Maybe ((BASICSPEC, Sign, GlobalAnnos) -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])) Source # sen_analysis :: QBF -> Maybe ((BASICSPEC, Sign, FORMULA) -> Result FORMULA) Source # extBasicAnalysis :: QBF -> IRI -> LibName -> BASICSPEC -> Sign -> GlobalAnnos -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA]) Source # stat_symb_map_items :: QBF -> Sign -> Maybe Sign -> [SYMBMAPITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: QBF -> Sign -> [SYMBITEMS] -> Result [Symbol] Source # convertTheory :: QBF -> Maybe ((Sign, [Named FORMULA]) -> BASICSPEC) Source # ensures_amalgamability :: QBF -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: QBF -> Morphism -> [Named FORMULA] -> Result (Sign, [Named FORMULA]) Source # signature_colimit :: QBF -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: QBF -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named FORMULA]) Source # symbol_to_raw :: QBF -> Symbol -> Symbol Source # id_to_raw :: QBF -> Id -> Symbol Source # matches :: QBF -> Symbol -> Symbol -> Bool Source # empty_signature :: QBF -> Sign Source # add_symb_to_sign :: QBF -> Sign -> Symbol -> Result Sign Source # signature_union :: QBF -> Sign -> Sign -> Result Sign Source # signatureDiff :: QBF -> Sign -> Sign -> Result Sign Source # intersection :: QBF -> Sign -> Sign -> Result Sign Source # final_union :: QBF -> Sign -> Sign -> Result Sign Source # morphism_union :: QBF -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: QBF -> Sign -> Sign -> Bool Source # subsig_inclusion :: QBF -> Sign -> Sign -> Result Morphism Source # generated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: QBF -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: QBF -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: QBF -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: QBF -> Morphism -> Bool Source # is_injective :: QBF -> Morphism -> Bool Source # theory_to_taxonomy :: QBF -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named FORMULA] -> Result MMiSSOntology Source # corresp2th :: QBF -> String -> Bool -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named FORMULA], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: QBF -> Sign -> Sign -> [SYMBITEMS] -> [SYMBITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: QBF -> [IRI] -> (Sign, [Named FORMULA]) -> Result (Sign, [Named FORMULA]) Source #
Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source #	Instance of Logic for propositional logc
Instance details Defined in QBF.Logic_QBF Methods parse_basic_sen :: QBF -> Maybe (BASICSPEC -> AParser st FORMULA) Source # stability :: QBF -> Stability Source # data_logic :: QBF -> Maybe AnyLogic Source # top_sublogic :: QBF -> QBFSL Source # all_sublogics :: QBF -> [QBFSL] Source # bottomSublogic :: QBF -> Maybe QBFSL Source # sublogicDimensions :: QBF -> [[QBFSL]] Source # parseSublogic :: QBF -> String -> Maybe QBFSL Source # proj_sublogic_epsilon :: QBF -> QBFSL -> Sign -> Morphism Source # provers :: QBF -> [Prover Sign FORMULA Morphism QBFSL ProofTree] Source # default_prover :: QBF -> String Source # cons_checkers :: QBF -> [ConsChecker Sign FORMULA QBFSL Morphism ProofTree] Source # conservativityCheck :: QBF -> [ConservativityChecker Sign FORMULA Morphism] Source # empty_proof_tree :: QBF -> ProofTree Source # syntaxTable :: QBF -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: QBF -> Maybe OMCD Source # export_symToOmdoc :: QBF -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: QBF -> NameMap Symbol -> FORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: QBF -> SigMap Symbol -> Sign -> [Named FORMULA] -> Result [TCElement] Source # omdocToSym :: QBF -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: QBF -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FORMULA)) Source # addOMadtToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [[OmdADT]] -> Result (Sign, [Named FORMULA]) Source # addOmdocToTheory :: QBF -> SigMapI Symbol -> (Sign, [Named FORMULA]) -> [TCElement] -> Result (Sign, [Named FORMULA]) Source # sublogicOfTheo :: QBF -> (Sign, [FORMULA]) -> QBFSL Source #
Comorphism QBF2Prop QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.QBF2Prop Methods sourceLogic :: QBF2Prop -> QBF Source # sourceSublogic :: QBF2Prop -> QBFSL Source # sourceSublogicLossy :: QBF2Prop -> QBFSL Source # minSourceTheory :: QBF2Prop -> Maybe (LibName, String) Source # targetLogic :: QBF2Prop -> Propositional 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_morphism :: QBF2Prop -> Morphism -> Result Morphism0 Source # map_sentence :: QBF2Prop -> Sign -> FORMULA -> Result FORMULA0 Source # map_symbol :: QBF2Prop -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: QBF2Prop -> Sign -> ProofTree -> Result (Sign, [Named FORMULA]) Source # is_model_transportable :: QBF2Prop -> Bool 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 #
Comorphism Prop2QBF Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.Prop2QBF Methods sourceLogic :: Prop2QBF -> Propositional Source # sourceSublogic :: Prop2QBF -> PropSL Source # sourceSublogicLossy :: Prop2QBF -> PropSL Source # minSourceTheory :: Prop2QBF -> Maybe (LibName, String) Source # targetLogic :: Prop2QBF -> QBF 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_morphism :: Prop2QBF -> Morphism0 -> Result Morphism Source # map_sentence :: Prop2QBF -> Sign -> FORMULA0 -> Result FORMULA Source # map_symbol :: Prop2QBF -> Sign -> Symbol0 -> Set Symbol Source # extractModel :: Prop2QBF -> Sign -> ProofTree -> Result (Sign, [Named FORMULA0]) Source # is_model_transportable :: Prop2QBF -> Bool 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 #
type Rep SYMBMAPITEMS
Instance details Defined in QBF.ATC_QBF type Rep SYMBMAPITEMS = D1 ('MetaData "SYMBMAPITEMS" "QBF.AS_BASIC_QBF" "main" 'False) (C1 ('MetaCons "SymbMapItems" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SYMBORMAP]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

data SYMBORMAP Source #

Constructors

Symb SYMB
SymbMap SYMB SYMB Range

Instances

Instances details

Eq SYMBORMAP Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods (==) :: SYMBORMAP -> SYMBORMAP -> Bool (/=) :: SYMBORMAP -> SYMBORMAP -> Bool
Data SYMBORMAP Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMBORMAP -> c SYMBORMAP gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMBORMAP toConstr :: SYMBORMAP -> Constr dataTypeOf :: SYMBORMAP -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SYMBORMAP) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMBORMAP) gmapT :: (forall b. Data b => b -> b) -> SYMBORMAP -> SYMBORMAP gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMBORMAP -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMBORMAP -> r gmapQ :: (forall d. Data d => d -> u) -> SYMBORMAP -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMBORMAP -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMBORMAP -> m SYMBORMAP
Ord SYMBORMAP Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods compare :: SYMBORMAP -> SYMBORMAP -> Ordering (<) :: SYMBORMAP -> SYMBORMAP -> Bool (<=) :: SYMBORMAP -> SYMBORMAP -> Bool (>) :: SYMBORMAP -> SYMBORMAP -> Bool (>=) :: SYMBORMAP -> SYMBORMAP -> Bool max :: SYMBORMAP -> SYMBORMAP -> SYMBORMAP min :: SYMBORMAP -> SYMBORMAP -> SYMBORMAP
Show SYMBORMAP Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods showsPrec :: Int -> SYMBORMAP -> ShowS show :: SYMBORMAP -> String showList :: [SYMBORMAP] -> ShowS
Generic SYMBORMAP
Instance details Defined in QBF.ATC_QBF Associated Types type Rep SYMBORMAP :: Type -> Type Methods from :: SYMBORMAP -> Rep SYMBORMAP x to :: Rep SYMBORMAP x -> SYMBORMAP
GetRange SYMBORMAP Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods getRange :: SYMBORMAP -> Range Source # rangeSpan :: SYMBORMAP -> [Pos] Source #
FromJSON SYMBORMAP
Instance details Defined in QBF.ATC_QBF Methods parseJSON :: Value -> Parser SYMBORMAP parseJSONList :: Value -> Parser [SYMBORMAP]
ToJSON SYMBORMAP
Instance details Defined in QBF.ATC_QBF Methods toJSON :: SYMBORMAP -> Value toEncoding :: SYMBORMAP -> Encoding toJSONList :: [SYMBORMAP] -> Value toEncodingList :: [SYMBORMAP] -> Encoding
ShATermConvertible SYMBORMAP
Instance details Defined in QBF.ATC_QBF Methods toShATermAux :: ATermTable -> SYMBORMAP -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SYMBORMAP] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SYMBORMAP) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SYMBORMAP])
Pretty SYMBORMAP Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods pretty :: SYMBORMAP -> Doc Source # pretties :: [SYMBORMAP] -> Doc Source #
type Rep SYMBORMAP
Instance details Defined in QBF.ATC_QBF type Rep SYMBORMAP = D1 ('MetaData "SYMBORMAP" "QBF.AS_BASIC_QBF" "main" 'False) (C1 ('MetaCons "Symb" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SYMB)) :+: C1 ('MetaCons "SymbMap" '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 PREDITEM Source #

predicates = propositions

Constructors

PredItem [Token] Range

Instances

Instances details

Data PREDITEM Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PREDITEM -> c PREDITEM gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PREDITEM toConstr :: PREDITEM -> Constr dataTypeOf :: PREDITEM -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PREDITEM) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PREDITEM) gmapT :: (forall b. Data b => b -> b) -> PREDITEM -> PREDITEM gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PREDITEM -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PREDITEM -> r gmapQ :: (forall d. Data d => d -> u) -> PREDITEM -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> PREDITEM -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PREDITEM -> m PREDITEM
Show PREDITEM Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods showsPrec :: Int -> PREDITEM -> ShowS show :: PREDITEM -> String showList :: [PREDITEM] -> ShowS
Generic PREDITEM
Instance details Defined in QBF.ATC_QBF Associated Types type Rep PREDITEM :: Type -> Type Methods from :: PREDITEM -> Rep PREDITEM x to :: Rep PREDITEM x -> PREDITEM
GetRange PREDITEM Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods getRange :: PREDITEM -> Range Source # rangeSpan :: PREDITEM -> [Pos] Source #
FromJSON PREDITEM
Instance details Defined in QBF.ATC_QBF Methods parseJSON :: Value -> Parser PREDITEM parseJSONList :: Value -> Parser [PREDITEM]
ToJSON PREDITEM
Instance details Defined in QBF.ATC_QBF Methods toJSON :: PREDITEM -> Value toEncoding :: PREDITEM -> Encoding toJSONList :: [PREDITEM] -> Value toEncodingList :: [PREDITEM] -> Encoding
ShATermConvertible PREDITEM
Instance details Defined in QBF.ATC_QBF Methods toShATermAux :: ATermTable -> PREDITEM -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [PREDITEM] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, PREDITEM) fromShATermList' :: Int -> ATermTable -> (ATermTable, [PREDITEM])
Pretty PREDITEM Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods pretty :: PREDITEM -> Doc Source # pretties :: [PREDITEM] -> Doc Source #
type Rep PREDITEM
Instance details Defined in QBF.ATC_QBF type Rep PREDITEM = D1 ('MetaData "PREDITEM" "QBF.AS_BASIC_QBF" "main" 'False) (C1 ('MetaCons "PredItem" '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 #

data ID Source #

Constructors

ID Token (Maybe Token)

Instances

Instances details

Eq ID Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods (==) :: ID -> ID -> Bool (/=) :: ID -> ID -> Bool
Data ID Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ID -> c ID gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ID toConstr :: ID -> Constr dataTypeOf :: ID -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ID) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ID) gmapT :: (forall b. Data b => b -> b) -> ID -> ID gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ID -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ID -> r gmapQ :: (forall d. Data d => d -> u) -> ID -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ID -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ID -> m ID gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ID -> m ID gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ID -> m ID
Generic ID
Instance details Defined in QBF.ATC_QBF Associated Types type Rep ID :: Type -> Type Methods from :: ID -> Rep ID x to :: Rep ID x -> ID
GetRange ID Source #
Instance details Defined in QBF.AS_BASIC_QBF Methods getRange :: ID -> Range Source # rangeSpan :: ID -> [Pos] Source #
FromJSON ID
Instance details Defined in QBF.ATC_QBF Methods parseJSON :: Value -> Parser ID parseJSONList :: Value -> Parser [ID]
ToJSON ID
Instance details Defined in QBF.ATC_QBF Methods toJSON :: ID -> Value toEncoding :: ID -> Encoding toJSONList :: [ID] -> Value toEncodingList :: [ID] -> Encoding
ShATermConvertible ID
Instance details Defined in QBF.ATC_QBF Methods toShATermAux :: ATermTable -> ID -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ID] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ID) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ID])
type Rep ID
Instance details Defined in QBF.ATC_QBF type Rep ID = D1 ('MetaData "ID" "QBF.AS_BASIC_QBF" "main" 'False) (C1 ('MetaCons "ID" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Token))))

FalseAtom Range
TrueAtom Range
Predication Token
Negation FORMULA Range
Conjunction [FORMULA] Range
Disjunction [FORMULA] Range
Implication FORMULA FORMULA Range
Equivalence FORMULA FORMULA Range
ForAll [Token] FORMULA Range
Exists [Token] FORMULA Range