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

Hybrid.AS_Hybrid

Description

Abstract syntax for hybrid logic extension of CASL Only the added syntax is specified

Documentation

type H_BASIC_SPEC = BASIC_SPEC H_BASIC_ITEM H_SIG_ITEM H_FORMULA Source #

type AnHybFORM = Annoted (FORMULA H_FORMULA) Source #

data H_BASIC_ITEM Source #

Constructors

Simple_mod_decl [Annoted SIMPLE_ID] [AnHybFORM] Range
Term_mod_decl [Annoted SORT] [AnHybFORM] Range
Simple_nom_decl [Annoted SIMPLE_ID] [AnHybFORM] Range

Instances

Instances details

Data H_BASIC_ITEM Source #
Instance details Defined in Hybrid.AS_Hybrid Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> H_BASIC_ITEM -> c H_BASIC_ITEM gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c H_BASIC_ITEM toConstr :: H_BASIC_ITEM -> Constr dataTypeOf :: H_BASIC_ITEM -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c H_BASIC_ITEM) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c H_BASIC_ITEM) gmapT :: (forall b. Data b => b -> b) -> H_BASIC_ITEM -> H_BASIC_ITEM gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> H_BASIC_ITEM -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> H_BASIC_ITEM -> r gmapQ :: (forall d. Data d => d -> u) -> H_BASIC_ITEM -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> H_BASIC_ITEM -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> H_BASIC_ITEM -> m H_BASIC_ITEM gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> H_BASIC_ITEM -> m H_BASIC_ITEM gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> H_BASIC_ITEM -> m H_BASIC_ITEM
Show H_BASIC_ITEM Source #
Instance details Defined in Hybrid.AS_Hybrid Methods showsPrec :: Int -> H_BASIC_ITEM -> ShowS show :: H_BASIC_ITEM -> String showList :: [H_BASIC_ITEM] -> ShowS
Generic H_BASIC_ITEM
Instance details Defined in Hybrid.ATC_Hybrid Associated Types type Rep H_BASIC_ITEM :: Type -> Type Methods from :: H_BASIC_ITEM -> Rep H_BASIC_ITEM x to :: Rep H_BASIC_ITEM x -> H_BASIC_ITEM
GetRange H_BASIC_ITEM Source #
Instance details Defined in Hybrid.AS_Hybrid Methods getRange :: H_BASIC_ITEM -> Range Source # rangeSpan :: H_BASIC_ITEM -> [Pos] Source #
FromJSON H_BASIC_ITEM
Instance details Defined in Hybrid.ATC_Hybrid Methods parseJSON :: Value -> Parser H_BASIC_ITEM parseJSONList :: Value -> Parser [H_BASIC_ITEM]
ToJSON H_BASIC_ITEM
Instance details Defined in Hybrid.ATC_Hybrid Methods toJSON :: H_BASIC_ITEM -> Value toEncoding :: H_BASIC_ITEM -> Encoding toJSONList :: [H_BASIC_ITEM] -> Value toEncodingList :: [H_BASIC_ITEM] -> Encoding
ShATermConvertible H_BASIC_ITEM
Instance details Defined in Hybrid.ATC_Hybrid Methods toShATermAux :: ATermTable -> H_BASIC_ITEM -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [H_BASIC_ITEM] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, H_BASIC_ITEM) fromShATermList' :: Int -> ATermTable -> (ATermTable, [H_BASIC_ITEM])
Pretty H_BASIC_ITEM Source #
Instance details Defined in Hybrid.Print_AS Methods pretty :: H_BASIC_ITEM -> Doc Source # pretties :: [H_BASIC_ITEM] -> Doc Source #
AParsable H_BASIC_ITEM Source #
Instance details Defined in Hybrid.Parse_AS Methods aparser :: AParser st H_BASIC_ITEM Source #
Syntax Hybrid H_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in Hybrid.Logic_Hybrid Methods parsersAndPrinters :: Hybrid -> Map String (PrefixMap -> AParser st H_BASIC_SPEC, H_BASIC_SPEC -> Doc) Source # parse_basic_spec :: Hybrid -> Maybe (PrefixMap -> AParser st H_BASIC_SPEC) Source # parseSingleSymbItem :: Hybrid -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: Hybrid -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: Hybrid -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: Hybrid -> H_BASIC_SPEC -> Item Source # symb_items_name :: Hybrid -> SYMB_ITEMS -> [String] 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 H_BASIC_ITEM
Instance details Defined in Hybrid.ATC_Hybrid type Rep H_BASIC_ITEM = D1 ('MetaData "H_BASIC_ITEM" "Hybrid.AS_Hybrid" "main" 'False) (C1 ('MetaCons "Simple_mod_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted SIMPLE_ID]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AnHybFORM]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "Term_mod_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted SORT]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AnHybFORM]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Simple_nom_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted SIMPLE_ID]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AnHybFORM]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))))

data RIGOR Source #

Constructors

Rigid
Flexible

Instances

Instances details

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

data H_SIG_ITEM Source #

Constructors

Rigid_op_items RIGOR [Annoted (OP_ITEM H_FORMULA)] Range
Rigid_pred_items RIGOR [Annoted (PRED_ITEM H_FORMULA)] Range

Instances

Instances details

Data H_SIG_ITEM Source #
Instance details Defined in Hybrid.AS_Hybrid Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> H_SIG_ITEM -> c H_SIG_ITEM gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c H_SIG_ITEM toConstr :: H_SIG_ITEM -> Constr dataTypeOf :: H_SIG_ITEM -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c H_SIG_ITEM) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c H_SIG_ITEM) gmapT :: (forall b. Data b => b -> b) -> H_SIG_ITEM -> H_SIG_ITEM gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> H_SIG_ITEM -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> H_SIG_ITEM -> r gmapQ :: (forall d. Data d => d -> u) -> H_SIG_ITEM -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> H_SIG_ITEM -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> H_SIG_ITEM -> m H_SIG_ITEM gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> H_SIG_ITEM -> m H_SIG_ITEM gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> H_SIG_ITEM -> m H_SIG_ITEM
Show H_SIG_ITEM Source #
Instance details Defined in Hybrid.AS_Hybrid Methods showsPrec :: Int -> H_SIG_ITEM -> ShowS show :: H_SIG_ITEM -> String showList :: [H_SIG_ITEM] -> ShowS
Generic H_SIG_ITEM
Instance details Defined in Hybrid.ATC_Hybrid Associated Types type Rep H_SIG_ITEM :: Type -> Type Methods from :: H_SIG_ITEM -> Rep H_SIG_ITEM x to :: Rep H_SIG_ITEM x -> H_SIG_ITEM
GetRange H_SIG_ITEM Source #
Instance details Defined in Hybrid.AS_Hybrid Methods getRange :: H_SIG_ITEM -> Range Source # rangeSpan :: H_SIG_ITEM -> [Pos] Source #
FromJSON H_SIG_ITEM
Instance details Defined in Hybrid.ATC_Hybrid Methods parseJSON :: Value -> Parser H_SIG_ITEM parseJSONList :: Value -> Parser [H_SIG_ITEM]
ToJSON H_SIG_ITEM
Instance details Defined in Hybrid.ATC_Hybrid Methods toJSON :: H_SIG_ITEM -> Value toEncoding :: H_SIG_ITEM -> Encoding toJSONList :: [H_SIG_ITEM] -> Value toEncodingList :: [H_SIG_ITEM] -> Encoding
ShATermConvertible H_SIG_ITEM
Instance details Defined in Hybrid.ATC_Hybrid Methods toShATermAux :: ATermTable -> H_SIG_ITEM -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [H_SIG_ITEM] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, H_SIG_ITEM) fromShATermList' :: Int -> ATermTable -> (ATermTable, [H_SIG_ITEM])
Pretty H_SIG_ITEM Source #
Instance details Defined in Hybrid.Print_AS Methods pretty :: H_SIG_ITEM -> Doc Source # pretties :: [H_SIG_ITEM] -> Doc Source #
AParsable H_SIG_ITEM Source #
Instance details Defined in Hybrid.Parse_AS Methods aparser :: AParser st H_SIG_ITEM Source #
Syntax Hybrid H_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in Hybrid.Logic_Hybrid Methods parsersAndPrinters :: Hybrid -> Map String (PrefixMap -> AParser st H_BASIC_SPEC, H_BASIC_SPEC -> Doc) Source # parse_basic_spec :: Hybrid -> Maybe (PrefixMap -> AParser st H_BASIC_SPEC) Source # parseSingleSymbItem :: Hybrid -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: Hybrid -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: Hybrid -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: Hybrid -> H_BASIC_SPEC -> Item Source # symb_items_name :: Hybrid -> SYMB_ITEMS -> [String] 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 H_SIG_ITEM
Instance details Defined in Hybrid.ATC_Hybrid type Rep H_SIG_ITEM = D1 ('MetaData "H_SIG_ITEM" "Hybrid.AS_Hybrid" "main" 'False) (C1 ('MetaCons "Rigid_op_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RIGOR) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (OP_ITEM H_FORMULA)]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Rigid_pred_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RIGOR) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (PRED_ITEM H_FORMULA)]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data MODALITY Source #

Constructors

Simple_mod SIMPLE_ID
Term_mod (TERM H_FORMULA)

Instances

Instances details

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

data NOMINAL Source #

Constructors

Simple_nom SIMPLE_ID

Instances

Instances details

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

data H_FORMULA Source #

Constructors

At NOMINAL (FORMULA H_FORMULA) Range
BoxOrDiamond Bool MODALITY (FORMULA H_FORMULA) Range
Here NOMINAL Range
Univ NOMINAL (FORMULA H_FORMULA) Range
Exist NOMINAL (FORMULA H_FORMULA) Range

Instances

Instances details

Eq H_FORMULA Source #
Instance details Defined in Hybrid.AS_Hybrid Methods (==) :: H_FORMULA -> H_FORMULA -> Bool (/=) :: H_FORMULA -> H_FORMULA -> Bool
Data H_FORMULA Source #
Instance details Defined in Hybrid.AS_Hybrid Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> H_FORMULA -> c H_FORMULA gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c H_FORMULA toConstr :: H_FORMULA -> Constr dataTypeOf :: H_FORMULA -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c H_FORMULA) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c H_FORMULA) gmapT :: (forall b. Data b => b -> b) -> H_FORMULA -> H_FORMULA gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> H_FORMULA -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> H_FORMULA -> r gmapQ :: (forall d. Data d => d -> u) -> H_FORMULA -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> H_FORMULA -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> H_FORMULA -> m H_FORMULA gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> H_FORMULA -> m H_FORMULA gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> H_FORMULA -> m H_FORMULA
Ord H_FORMULA Source #
Instance details Defined in Hybrid.AS_Hybrid Methods compare :: H_FORMULA -> H_FORMULA -> Ordering (<) :: H_FORMULA -> H_FORMULA -> Bool (<=) :: H_FORMULA -> H_FORMULA -> Bool (>) :: H_FORMULA -> H_FORMULA -> Bool (>=) :: H_FORMULA -> H_FORMULA -> Bool max :: H_FORMULA -> H_FORMULA -> H_FORMULA min :: H_FORMULA -> H_FORMULA -> H_FORMULA
Show H_FORMULA Source #
Instance details Defined in Hybrid.AS_Hybrid Methods showsPrec :: Int -> H_FORMULA -> ShowS show :: H_FORMULA -> String showList :: [H_FORMULA] -> ShowS
Generic H_FORMULA
Instance details Defined in Hybrid.ATC_Hybrid Associated Types type Rep H_FORMULA :: Type -> Type Methods from :: H_FORMULA -> Rep H_FORMULA x to :: Rep H_FORMULA x -> H_FORMULA
GetRange H_FORMULA Source #
Instance details Defined in Hybrid.AS_Hybrid Methods getRange :: H_FORMULA -> Range Source # rangeSpan :: H_FORMULA -> [Pos] Source #
FromJSON H_FORMULA
Instance details Defined in Hybrid.ATC_Hybrid Methods parseJSON :: Value -> Parser H_FORMULA parseJSONList :: Value -> Parser [H_FORMULA]
ToJSON H_FORMULA
Instance details Defined in Hybrid.ATC_Hybrid Methods toJSON :: H_FORMULA -> Value toEncoding :: H_FORMULA -> Encoding toJSONList :: [H_FORMULA] -> Value toEncodingList :: [H_FORMULA] -> Encoding
ShATermConvertible H_FORMULA
Instance details Defined in Hybrid.ATC_Hybrid Methods toShATermAux :: ATermTable -> H_FORMULA -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [H_FORMULA] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, H_FORMULA) fromShATermList' :: Int -> ATermTable -> (ATermTable, [H_FORMULA])
Pretty H_FORMULA Source #
Instance details Defined in Hybrid.Print_AS Methods pretty :: H_FORMULA -> Doc Source # pretties :: [H_FORMULA] -> Doc Source #
FormExtension H_FORMULA Source #
Instance details Defined in Hybrid.Print_AS Methods isQuantifierLike :: H_FORMULA -> Bool Source # prefixExt :: H_FORMULA -> Doc -> Doc Source #
TermExtension H_FORMULA Source #
Instance details Defined in Hybrid.StatAna Methods freeVarsOfExt :: Sign H_FORMULA e -> H_FORMULA -> VarSet Source # optTermSort :: H_FORMULA -> Maybe SORT Source # sortOfTerm :: H_FORMULA -> SORT Source # termToFormula :: TERM H_FORMULA -> Result (FORMULA H_FORMULA) Source #
TermParser H_FORMULA Source #
Instance details Defined in Hybrid.Parse_AS Methods termParser :: Bool -> AParser st H_FORMULA 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 #
Syntax Hybrid H_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in Hybrid.Logic_Hybrid Methods parsersAndPrinters :: Hybrid -> Map String (PrefixMap -> AParser st H_BASIC_SPEC, H_BASIC_SPEC -> Doc) Source # parse_basic_spec :: Hybrid -> Maybe (PrefixMap -> AParser st H_BASIC_SPEC) Source # parseSingleSymbItem :: Hybrid -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: Hybrid -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: Hybrid -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: Hybrid -> H_BASIC_SPEC -> Item Source # symb_items_name :: Hybrid -> SYMB_ITEMS -> [String] 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 H_FORMULA
Instance details Defined in Hybrid.ATC_Hybrid type Rep H_FORMULA = D1 ('MetaData "H_FORMULA" "Hybrid.AS_Hybrid" "main" 'False) ((C1 ('MetaCons "At" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NOMINAL) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FORMULA H_FORMULA)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "BoxOrDiamond" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MODALITY)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FORMULA H_FORMULA)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))) :+: (C1 ('MetaCons "Here" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NOMINAL) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: (C1 ('MetaCons "Univ" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NOMINAL) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FORMULA H_FORMULA)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Exist" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NOMINAL) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FORMULA H_FORMULA)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))))