License	GPLv2 or higher, see LICENSE.txt
Stability	provisional
Portability	portable
Safe Haskell	Safe

Hybrid.HybridSign

Description

Signatures for hybrid logic, as extension of CASL signatures.

Documentation

data HybridSign Source #

Constructors

HybridSign
Fields rigidOps :: OpMap rigidPreds :: PredMap modies :: Map SIMPLE_ID [AnHybFORM] nomies :: Map SIMPLE_ID [AnHybFORM] termModies :: Map Id [AnHybFORM]

Instances

Instances details

Eq HybridSign Source #
Instance details Defined in Hybrid.HybridSign Methods (==) :: HybridSign -> HybridSign -> Bool (/=) :: HybridSign -> HybridSign -> Bool
Data HybridSign Source #
Instance details Defined in Hybrid.HybridSign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HybridSign -> c HybridSign gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HybridSign toConstr :: HybridSign -> Constr dataTypeOf :: HybridSign -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HybridSign) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HybridSign) gmapT :: (forall b. Data b => b -> b) -> HybridSign -> HybridSign gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HybridSign -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HybridSign -> r gmapQ :: (forall d. Data d => d -> u) -> HybridSign -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> HybridSign -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> HybridSign -> m HybridSign gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HybridSign -> m HybridSign gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HybridSign -> m HybridSign
Ord HybridSign Source #
Instance details Defined in Hybrid.HybridSign Methods compare :: HybridSign -> HybridSign -> Ordering (<) :: HybridSign -> HybridSign -> Bool (<=) :: HybridSign -> HybridSign -> Bool (>) :: HybridSign -> HybridSign -> Bool (>=) :: HybridSign -> HybridSign -> Bool max :: HybridSign -> HybridSign -> HybridSign min :: HybridSign -> HybridSign -> HybridSign
Show HybridSign Source #
Instance details Defined in Hybrid.HybridSign Methods showsPrec :: Int -> HybridSign -> ShowS show :: HybridSign -> String showList :: [HybridSign] -> ShowS
Generic HybridSign
Instance details Defined in Hybrid.ATC_Hybrid Associated Types type Rep HybridSign :: Type -> Type Methods from :: HybridSign -> Rep HybridSign x to :: Rep HybridSign x -> HybridSign
FromJSON HybridSign
Instance details Defined in Hybrid.ATC_Hybrid Methods parseJSON :: Value -> Parser HybridSign parseJSONList :: Value -> Parser [HybridSign]
ToJSON HybridSign
Instance details Defined in Hybrid.ATC_Hybrid Methods toJSON :: HybridSign -> Value toEncoding :: HybridSign -> Encoding toJSONList :: [HybridSign] -> Value toEncodingList :: [HybridSign] -> Encoding
ShATermConvertible HybridSign
Instance details Defined in Hybrid.ATC_Hybrid Methods toShATermAux :: ATermTable -> HybridSign -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [HybridSign] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, HybridSign) fromShATermList' :: Int -> ATermTable -> (ATermTable, [HybridSign])
Pretty HybridSign Source #
Instance details Defined in Hybrid.Print_AS Methods pretty :: HybridSign -> Doc Source # pretties :: [HybridSign] -> Doc Source #
SignExtension HybridSign Source #
Instance details Defined in Hybrid.Logic_Hybrid Methods isSubSignExtension :: HybridSign -> HybridSign -> Bool Source #
Sentences Hybrid HybridFORMULA HSign HybridMor Symbol Source #
Instance details Defined in Hybrid.Logic_Hybrid Methods map_sen :: Hybrid -> HybridMor -> HybridFORMULA -> Result HybridFORMULA Source # simplify_sen :: Hybrid -> HSign -> HybridFORMULA -> HybridFORMULA Source # negation :: Hybrid -> HybridFORMULA -> Maybe HybridFORMULA Source # print_sign :: Hybrid -> HSign -> Doc Source # print_named :: Hybrid -> Named HybridFORMULA -> Doc Source # sym_of :: Hybrid -> HSign -> [Set Symbol] Source # mostSymsOf :: Hybrid -> HSign -> [Symbol] Source # symmap_of :: Hybrid -> HybridMor -> EndoMap Symbol Source # sym_name :: Hybrid -> Symbol -> Id Source # sym_label :: Hybrid -> Symbol -> Maybe String Source # fullSymName :: Hybrid -> Symbol -> String Source # symKind :: Hybrid -> Symbol -> String Source # symsOfSen :: Hybrid -> HSign -> HybridFORMULA -> [Symbol] Source # pair_symbols :: Hybrid -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis Hybrid H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol Source #
Instance details Defined in Hybrid.Logic_Hybrid Methods basic_analysis :: Hybrid -> Maybe ((H_BASIC_SPEC, HSign, GlobalAnnos) -> Result (H_BASIC_SPEC, ExtSign HSign Symbol, [Named HybridFORMULA])) Source # sen_analysis :: Hybrid -> Maybe ((H_BASIC_SPEC, HSign, HybridFORMULA) -> Result HybridFORMULA) Source # extBasicAnalysis :: Hybrid -> IRI -> LibName -> H_BASIC_SPEC -> HSign -> GlobalAnnos -> Result (H_BASIC_SPEC, ExtSign HSign Symbol, [Named HybridFORMULA]) Source # stat_symb_map_items :: Hybrid -> HSign -> Maybe HSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Hybrid -> HSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: Hybrid -> Maybe ((HSign, [Named HybridFORMULA]) -> H_BASIC_SPEC) Source # ensures_amalgamability :: Hybrid -> ([CASLAmalgOpt], Gr HSign (Int, HybridMor), [(Int, HybridMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Hybrid -> HybridMor -> [Named HybridFORMULA] -> Result (HSign, [Named HybridFORMULA]) Source # signature_colimit :: Hybrid -> Gr HSign (Int, HybridMor) -> Result (HSign, Map Int HybridMor) Source # qualify :: Hybrid -> SIMPLE_ID -> LibName -> HybridMor -> HSign -> Result (HybridMor, [Named HybridFORMULA]) Source # symbol_to_raw :: Hybrid -> Symbol -> RawSymbol Source # id_to_raw :: Hybrid -> Id -> RawSymbol Source # matches :: Hybrid -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Hybrid -> HSign Source # add_symb_to_sign :: Hybrid -> HSign -> Symbol -> Result HSign Source # signature_union :: Hybrid -> HSign -> HSign -> Result HSign Source # signatureDiff :: Hybrid -> HSign -> HSign -> Result HSign Source # intersection :: Hybrid -> HSign -> HSign -> Result HSign Source # final_union :: Hybrid -> HSign -> HSign -> Result HSign Source # morphism_union :: Hybrid -> HybridMor -> HybridMor -> Result HybridMor Source # is_subsig :: Hybrid -> HSign -> HSign -> Bool Source # subsig_inclusion :: Hybrid -> HSign -> HSign -> Result HybridMor Source # generated_sign :: Hybrid -> Set Symbol -> HSign -> Result HybridMor Source # cogenerated_sign :: Hybrid -> Set Symbol -> HSign -> Result HybridMor Source # induced_from_morphism :: Hybrid -> EndoMap RawSymbol -> HSign -> Result HybridMor Source # induced_from_to_morphism :: Hybrid -> EndoMap RawSymbol -> ExtSign HSign Symbol -> ExtSign HSign Symbol -> Result HybridMor Source # is_transportable :: Hybrid -> HybridMor -> Bool Source # is_injective :: Hybrid -> HybridMor -> Bool Source # theory_to_taxonomy :: Hybrid -> TaxoGraphKind -> MMiSSOntology -> HSign -> [Named HybridFORMULA] -> Result MMiSSOntology Source # corresp2th :: Hybrid -> String -> Bool -> HSign -> HSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (HSign, [Named HybridFORMULA], HSign, HSign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Hybrid -> HSign -> HSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (HSign, HSign, HSign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Hybrid -> [IRI] -> (HSign, [Named HybridFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source #
Logic Hybrid () H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol () Source #
Instance details Defined in Hybrid.Logic_Hybrid Methods parse_basic_sen :: Hybrid -> Maybe (H_BASIC_SPEC -> AParser st HybridFORMULA) Source # stability :: Hybrid -> Stability Source # data_logic :: Hybrid -> Maybe AnyLogic Source # top_sublogic :: Hybrid -> () Source # all_sublogics :: Hybrid -> [()] Source # bottomSublogic :: Hybrid -> Maybe () Source # sublogicDimensions :: Hybrid -> [[()]] Source # parseSublogic :: Hybrid -> String -> Maybe () Source # proj_sublogic_epsilon :: Hybrid -> () -> HSign -> HybridMor Source # provers :: Hybrid -> [Prover HSign HybridFORMULA HybridMor () ()] Source # default_prover :: Hybrid -> String Source # cons_checkers :: Hybrid -> [ConsChecker HSign HybridFORMULA () HybridMor ()] Source # conservativityCheck :: Hybrid -> [ConservativityChecker HSign HybridFORMULA HybridMor] Source # empty_proof_tree :: Hybrid -> () Source # syntaxTable :: Hybrid -> HSign -> Maybe SyntaxTable Source # omdoc_metatheory :: Hybrid -> Maybe OMCD Source # export_symToOmdoc :: Hybrid -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: Hybrid -> NameMap Symbol -> HybridFORMULA -> Result TCorOMElement Source # export_theoryToOmdoc :: Hybrid -> SigMap Symbol -> HSign -> [Named HybridFORMULA] -> Result [TCElement] Source # omdocToSym :: Hybrid -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: Hybrid -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named HybridFORMULA)) Source # addOMadtToTheory :: Hybrid -> SigMapI Symbol -> (HSign, [Named HybridFORMULA]) -> [[OmdADT]] -> Result (HSign, [Named HybridFORMULA]) Source # addOmdocToTheory :: Hybrid -> SigMapI Symbol -> (HSign, [Named HybridFORMULA]) -> [TCElement] -> Result (HSign, [Named HybridFORMULA]) Source # sublogicOfTheo :: Hybrid -> (HSign, [HybridFORMULA]) -> () Source #
Comorphism CASL2Hybrid CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Hybrid () H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2Hybrid Methods sourceLogic :: CASL2Hybrid -> CASL Source # sourceSublogic :: CASL2Hybrid -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2Hybrid -> CASL_Sublogics Source # minSourceTheory :: CASL2Hybrid -> Maybe (LibName, String) Source # targetLogic :: CASL2Hybrid -> Hybrid Source # mapSublogic :: CASL2Hybrid -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2Hybrid -> (CASLSign, [Named CASLFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source # mapMarkedTheory :: CASL2Hybrid -> (CASLSign, [Named CASLFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source # map_morphism :: CASL2Hybrid -> CASLMor -> Result HybridMor Source # map_sentence :: CASL2Hybrid -> CASLSign -> CASLFORMULA -> Result HybridFORMULA Source # map_symbol :: CASL2Hybrid -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2Hybrid -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2Hybrid -> Bool Source # has_model_expansion :: CASL2Hybrid -> Bool Source # is_weakly_amalgamable :: CASL2Hybrid -> Bool Source # constituents :: CASL2Hybrid -> [String] Source # isInclusionComorphism :: CASL2Hybrid -> Bool Source # rps :: CASL2Hybrid -> Bool Source # eps :: CASL2Hybrid -> Bool Source # isGTC :: CASL2Hybrid -> Bool Source #
type Rep HybridSign
Instance details Defined in Hybrid.ATC_Hybrid type Rep HybridSign = D1 ('MetaData "HybridSign" "Hybrid.HybridSign" "main" 'False) (C1 ('MetaCons "HybridSign" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rigidOps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpMap) :: S1 ('MetaSel ('Just "rigidPreds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PredMap)) :: (S1 ('MetaSel ('Just "modies") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map SIMPLE_ID [AnHybFORM])) :: (S1 ('MetaSel ('Just "nomies") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map SIMPLE_ID [AnHybFORM])) :: S1 ('MetaSel ('Just "termModies") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Id [AnHybFORM]))))))

emptyHybridSign :: HybridSign Source #

addHybridSign :: HybridSign -> HybridSign -> HybridSign Source #

interMap :: Ord a => ([b] -> [b] -> [b]) -> Map a [b] -> Map a [b] -> Map a [b] Source #

interHybridSign :: HybridSign -> HybridSign -> HybridSign Source #

diffHybridSign :: HybridSign -> HybridSign -> HybridSign Source #

isSubHybridSign :: HybridSign -> HybridSign -> Bool Source #