Copyright	(c) Till Mossakowski C. Maeder Uni Bremen 2004
License	GPLv2 or higher, see LICENSE.txt
Maintainer	till@informatik.uni-bremen.de
Stability	provisional
Portability	portable
Safe Haskell	Safe

COL.COLSign

Description

Signatures of COL as extension of CASL signatures.

Documentation

data COLSign Source #

Constructors

COLSign
Fields constructors :: Set Id observers :: Map Id Int

Instances

Instances details

Eq COLSign Source #
Instance details Defined in COL.COLSign Methods (==) :: COLSign -> COLSign -> Bool (/=) :: COLSign -> COLSign -> Bool
Data COLSign Source #
Instance details Defined in COL.COLSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> COLSign -> c COLSign gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c COLSign toConstr :: COLSign -> Constr dataTypeOf :: COLSign -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c COLSign) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c COLSign) gmapT :: (forall b. Data b => b -> b) -> COLSign -> COLSign gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> COLSign -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> COLSign -> r gmapQ :: (forall d. Data d => d -> u) -> COLSign -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> COLSign -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> COLSign -> m COLSign gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> COLSign -> m COLSign gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> COLSign -> m COLSign
Ord COLSign Source #
Instance details Defined in COL.COLSign Methods compare :: COLSign -> COLSign -> Ordering (<) :: COLSign -> COLSign -> Bool (<=) :: COLSign -> COLSign -> Bool (>) :: COLSign -> COLSign -> Bool (>=) :: COLSign -> COLSign -> Bool max :: COLSign -> COLSign -> COLSign min :: COLSign -> COLSign -> COLSign
Show COLSign Source #
Instance details Defined in COL.COLSign Methods showsPrec :: Int -> COLSign -> ShowS show :: COLSign -> String showList :: [COLSign] -> ShowS
Generic COLSign
Instance details Defined in COL.ATC_COL Associated Types type Rep COLSign :: Type -> Type Methods from :: COLSign -> Rep COLSign x to :: Rep COLSign x -> COLSign
FromJSON COLSign
Instance details Defined in COL.ATC_COL Methods parseJSON :: Value -> Parser COLSign parseJSONList :: Value -> Parser [COLSign]
ToJSON COLSign
Instance details Defined in COL.ATC_COL Methods toJSON :: COLSign -> Value toEncoding :: COLSign -> Encoding toJSONList :: [COLSign] -> Value toEncodingList :: [COLSign] -> Encoding
ShATermConvertible COLSign
Instance details Defined in COL.ATC_COL Methods toShATermAux :: ATermTable -> COLSign -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [COLSign] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, COLSign) fromShATermList' :: Int -> ATermTable -> (ATermTable, [COLSign])
Pretty COLSign Source #
Instance details Defined in COL.Print_AS Methods pretty :: COLSign -> Doc Source # pretties :: [COLSign] -> Doc Source #
SignExtension COLSign Source #
Instance details Defined in COL.Logic_COL Methods isSubSignExtension :: COLSign -> COLSign -> Bool Source #
Sentences COL COLFORMULA CSign COLMor Symbol Source #
Instance details Defined in COL.Logic_COL Methods map_sen :: COL -> COLMor -> COLFORMULA -> Result COLFORMULA Source # simplify_sen :: COL -> CSign -> COLFORMULA -> COLFORMULA Source # negation :: COL -> COLFORMULA -> Maybe COLFORMULA Source # print_sign :: COL -> CSign -> Doc Source # print_named :: COL -> Named COLFORMULA -> Doc Source # sym_of :: COL -> CSign -> [Set Symbol] Source # mostSymsOf :: COL -> CSign -> [Symbol] Source # symmap_of :: COL -> COLMor -> EndoMap Symbol Source # sym_name :: COL -> Symbol -> Id Source # sym_label :: COL -> Symbol -> Maybe String Source # fullSymName :: COL -> Symbol -> String Source # symKind :: COL -> Symbol -> String Source # symsOfSen :: COL -> CSign -> COLFORMULA -> [Symbol] Source # pair_symbols :: COL -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis COL C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol Source #
Instance details Defined in COL.Logic_COL Methods basic_analysis :: COL -> Maybe ((C_BASIC_SPEC, CSign, GlobalAnnos) -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA])) Source # sen_analysis :: COL -> Maybe ((C_BASIC_SPEC, CSign, COLFORMULA) -> Result COLFORMULA) Source # extBasicAnalysis :: COL -> IRI -> LibName -> C_BASIC_SPEC -> CSign -> GlobalAnnos -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA]) Source # stat_symb_map_items :: COL -> CSign -> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: COL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: COL -> Maybe ((CSign, [Named COLFORMULA]) -> C_BASIC_SPEC) Source # ensures_amalgamability :: COL -> ([CASLAmalgOpt], Gr CSign (Int, COLMor), [(Int, COLMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: COL -> COLMor -> [Named COLFORMULA] -> Result (CSign, [Named COLFORMULA]) Source # signature_colimit :: COL -> Gr CSign (Int, COLMor) -> Result (CSign, Map Int COLMor) Source # qualify :: COL -> SIMPLE_ID -> LibName -> COLMor -> CSign -> Result (COLMor, [Named COLFORMULA]) Source # symbol_to_raw :: COL -> Symbol -> RawSymbol Source # id_to_raw :: COL -> Id -> RawSymbol Source # matches :: COL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: COL -> CSign Source # add_symb_to_sign :: COL -> CSign -> Symbol -> Result CSign Source # signature_union :: COL -> CSign -> CSign -> Result CSign Source # signatureDiff :: COL -> CSign -> CSign -> Result CSign Source # intersection :: COL -> CSign -> CSign -> Result CSign Source # final_union :: COL -> CSign -> CSign -> Result CSign Source # morphism_union :: COL -> COLMor -> COLMor -> Result COLMor Source # is_subsig :: COL -> CSign -> CSign -> Bool Source # subsig_inclusion :: COL -> CSign -> CSign -> Result COLMor Source # generated_sign :: COL -> Set Symbol -> CSign -> Result COLMor Source # cogenerated_sign :: COL -> Set Symbol -> CSign -> Result COLMor Source # induced_from_morphism :: COL -> EndoMap RawSymbol -> CSign -> Result COLMor Source # induced_from_to_morphism :: COL -> EndoMap RawSymbol -> ExtSign CSign Symbol -> ExtSign CSign Symbol -> Result COLMor Source # is_transportable :: COL -> COLMor -> Bool Source # is_injective :: COL -> COLMor -> Bool Source # theory_to_taxonomy :: COL -> TaxoGraphKind -> MMiSSOntology -> CSign -> [Named COLFORMULA] -> Result MMiSSOntology Source # corresp2th :: COL -> String -> Bool -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CSign, [Named COLFORMULA], CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: COL -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CSign, CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: COL -> [IRI] -> (CSign, [Named COLFORMULA]) -> Result (CSign, [Named COLFORMULA]) Source #
Logic COL () C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol () Source #
Instance details Defined in COL.Logic_COL Methods parse_basic_sen :: COL -> Maybe (C_BASIC_SPEC -> AParser st COLFORMULA) Source # stability :: COL -> Stability Source # data_logic :: COL -> Maybe AnyLogic Source # top_sublogic :: COL -> () Source # all_sublogics :: COL -> [()] Source # bottomSublogic :: COL -> Maybe () Source # sublogicDimensions :: COL -> [[()]] Source # parseSublogic :: COL -> String -> Maybe () Source # proj_sublogic_epsilon :: COL -> () -> CSign -> COLMor Source # provers :: COL -> [Prover CSign COLFORMULA COLMor () ()] Source # default_prover :: COL -> String Source # cons_checkers :: COL -> [ConsChecker CSign COLFORMULA () COLMor ()] Source # conservativityCheck :: COL -> [ConservativityChecker CSign COLFORMULA COLMor] Source # empty_proof_tree :: COL -> () Source # syntaxTable :: COL -> CSign -> Maybe SyntaxTable Source # omdoc_metatheory :: COL -> Maybe OMCD Source # export_symToOmdoc :: COL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: COL -> NameMap Symbol -> COLFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: COL -> SigMap Symbol -> CSign -> [Named COLFORMULA] -> Result [TCElement] Source # omdocToSym :: COL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: COL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named COLFORMULA)) Source # addOMadtToTheory :: COL -> SigMapI Symbol -> (CSign, [Named COLFORMULA]) -> [[OmdADT]] -> Result (CSign, [Named COLFORMULA]) Source # addOmdocToTheory :: COL -> SigMapI Symbol -> (CSign, [Named COLFORMULA]) -> [TCElement] -> Result (CSign, [Named COLFORMULA]) Source # sublogicOfTheo :: COL -> (CSign, [COLFORMULA]) -> () Source #
type Rep COLSign
Instance details Defined in COL.ATC_COL type Rep COLSign = D1 ('MetaData "COLSign" "COL.COLSign" "main" 'False) (C1 ('MetaCons "COLSign" 'PrefixI 'True) (S1 ('MetaSel ('Just "constructors") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Id)) :*: S1 ('MetaSel ('Just "observers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Id Int))))

emptyCOLSign :: COLSign Source #

addCOLSign :: COLSign -> COLSign -> COLSign Source #

diffCOLSign :: COLSign -> COLSign -> COLSign Source #

isSubCOLSign :: COLSign -> COLSign -> Bool Source #