License	GPLv2 or higher, see LICENSE.txt
Maintainer	nevrenato@gmail.com
Stability	experimental
Portability	portable
Safe Haskell	None

TopHybrid.TopHybridSign

Description

Description : Signature for an hybridized logic. Its constituted by the declaration of nominals and modalities, and the signature of the logic below

Documentation

data Sgn_Wrap Source #

Constructors

Logic l sub bs f s sm sign mo sy rw pf => Sgn_Wrap l (THybridSign sign)
EmptySign

Instances

Eq Sgn_Wrap Source #
Methods (==) :: Sgn_Wrap -> Sgn_Wrap -> Bool (/=) :: Sgn_Wrap -> Sgn_Wrap -> Bool
Ord Sgn_Wrap Source #
Methods compare :: Sgn_Wrap -> Sgn_Wrap -> Ordering (<) :: Sgn_Wrap -> Sgn_Wrap -> Bool (<=) :: Sgn_Wrap -> Sgn_Wrap -> Bool (>) :: Sgn_Wrap -> Sgn_Wrap -> Bool (>=) :: Sgn_Wrap -> Sgn_Wrap -> Bool max :: Sgn_Wrap -> Sgn_Wrap -> Sgn_Wrap min :: Sgn_Wrap -> Sgn_Wrap -> Sgn_Wrap
Show Sgn_Wrap Source #
Methods showsPrec :: Int -> Sgn_Wrap -> ShowS show :: Sgn_Wrap -> String showList :: [Sgn_Wrap] -> ShowS
Sentences Hybridize Frm_Wrap Sgn_Wrap Mor Symbol Source #
Methods map_sen :: Hybridize -> Mor -> Frm_Wrap -> Result Frm_Wrap Source # simplify_sen :: Hybridize -> Sgn_Wrap -> Frm_Wrap -> Frm_Wrap Source # negation :: Hybridize -> Frm_Wrap -> Maybe Frm_Wrap Source # print_sign :: Hybridize -> Sgn_Wrap -> Doc Source # print_named :: Hybridize -> Named Frm_Wrap -> Doc Source # sym_of :: Hybridize -> Sgn_Wrap -> [Set Symbol] Source # mostSymsOf :: Hybridize -> Sgn_Wrap -> [Symbol] Source # symmap_of :: Hybridize -> Mor -> EndoMap Symbol Source # sym_name :: Hybridize -> Symbol -> Id Source # sym_label :: Hybridize -> Symbol -> Maybe String Source # fullSymName :: Hybridize -> Symbol -> String Source # symKind :: Hybridize -> Symbol -> String Source # symsOfSen :: Hybridize -> Sgn_Wrap -> Frm_Wrap -> [Symbol] Source # pair_symbols :: Hybridize -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis Hybridize Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS Sgn_Wrap Mor Symbol RawSymbol Source #
Methods basic_analysis :: Hybridize -> Maybe ((Spc_Wrap, Sgn_Wrap, GlobalAnnos) -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap])) Source # sen_analysis :: Hybridize -> Maybe ((Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap) Source # extBasicAnalysis :: Hybridize -> IRI -> LibName -> Spc_Wrap -> Sgn_Wrap -> GlobalAnnos -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap]) Source # stat_symb_map_items :: Hybridize -> Sgn_Wrap -> Maybe Sgn_Wrap -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Hybridize -> Sgn_Wrap -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: Hybridize -> Maybe ((Sgn_Wrap, [Named Frm_Wrap]) -> Spc_Wrap) Source # ensures_amalgamability :: Hybridize -> ([CASLAmalgOpt], Gr Sgn_Wrap (Int, Mor), [(Int, Mor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Hybridize -> Mor -> [Named Frm_Wrap] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source # signature_colimit :: Hybridize -> Gr Sgn_Wrap (Int, Mor) -> Result (Sgn_Wrap, Map Int Mor) Source # qualify :: Hybridize -> SIMPLE_ID -> LibName -> Mor -> Sgn_Wrap -> Result (Mor, [Named Frm_Wrap]) Source # symbol_to_raw :: Hybridize -> Symbol -> RawSymbol Source # id_to_raw :: Hybridize -> Id -> RawSymbol Source # matches :: Hybridize -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Hybridize -> Sgn_Wrap Source # add_symb_to_sign :: Hybridize -> Sgn_Wrap -> Symbol -> Result Sgn_Wrap Source # signature_union :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # signatureDiff :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # intersection :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # final_union :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # morphism_union :: Hybridize -> Mor -> Mor -> Result Mor Source # is_subsig :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Bool Source # subsig_inclusion :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Mor Source # generated_sign :: Hybridize -> Set Symbol -> Sgn_Wrap -> Result Mor Source # cogenerated_sign :: Hybridize -> Set Symbol -> Sgn_Wrap -> Result Mor Source # induced_from_morphism :: Hybridize -> EndoMap RawSymbol -> Sgn_Wrap -> Result Mor Source # induced_from_to_morphism :: Hybridize -> EndoMap RawSymbol -> ExtSign Sgn_Wrap Symbol -> ExtSign Sgn_Wrap Symbol -> Result Mor Source # is_transportable :: Hybridize -> Mor -> Bool Source # is_injective :: Hybridize -> Mor -> Bool Source # theory_to_taxonomy :: Hybridize -> TaxoGraphKind -> MMiSSOntology -> Sgn_Wrap -> [Named Frm_Wrap] -> Result MMiSSOntology Source # corresp2th :: Hybridize -> String -> Bool -> Sgn_Wrap -> Sgn_Wrap -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sgn_Wrap, [Named Frm_Wrap], Sgn_Wrap, Sgn_Wrap, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sgn_Wrap, Sgn_Wrap, Sgn_Wrap, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Hybridize -> [IRI] -> (Sgn_Wrap, [Named Frm_Wrap]) -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source #
Logic Hybridize () Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS Sgn_Wrap Mor Symbol RawSymbol () Source #
Methods parse_basic_sen :: Hybridize -> Maybe (Spc_Wrap -> AParser st Frm_Wrap) Source # stability :: Hybridize -> Stability Source # data_logic :: Hybridize -> Maybe AnyLogic Source # top_sublogic :: Hybridize -> () Source # all_sublogics :: Hybridize -> [()] Source # bottomSublogic :: Hybridize -> Maybe () Source # sublogicDimensions :: Hybridize -> [[()]] Source # parseSublogic :: Hybridize -> String -> Maybe () Source # proj_sublogic_epsilon :: Hybridize -> () -> Sgn_Wrap -> Mor Source # provers :: Hybridize -> [Prover Sgn_Wrap Frm_Wrap Mor () ()] Source # default_prover :: Hybridize -> String Source # cons_checkers :: Hybridize -> [ConsChecker Sgn_Wrap Frm_Wrap () Mor ()] Source # conservativityCheck :: Hybridize -> [ConservativityChecker Sgn_Wrap Frm_Wrap Mor] Source # empty_proof_tree :: Hybridize -> () Source # syntaxTable :: Hybridize -> Sgn_Wrap -> Maybe SyntaxTable Source # omdoc_metatheory :: Hybridize -> Maybe OMCD Source # export_symToOmdoc :: Hybridize -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: Hybridize -> NameMap Symbol -> Frm_Wrap -> Result TCorOMElement Source # export_theoryToOmdoc :: Hybridize -> SigMap Symbol -> Sgn_Wrap -> [Named Frm_Wrap] -> Result [TCElement] Source # omdocToSym :: Hybridize -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: Hybridize -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Frm_Wrap)) Source # addOMadtToTheory :: Hybridize -> SigMapI Symbol -> (Sgn_Wrap, [Named Frm_Wrap]) -> [[OmdADT]] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source # addOmdocToTheory :: Hybridize -> SigMapI Symbol -> (Sgn_Wrap, [Named Frm_Wrap]) -> [TCElement] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source # sublogicOfTheo :: Hybridize -> (Sgn_Wrap, [Frm_Wrap]) -> () Source #

data THybridSign s Source #

Constructors

THybridSign
Fields modies :: Set MODALITY nomies :: Set NOMINAL extended :: s

Instances

Eq s => Eq (THybridSign s) Source #
Methods (==) :: THybridSign s -> THybridSign s -> Bool (/=) :: THybridSign s -> THybridSign s -> Bool
Data s => Data (THybridSign s) Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THybridSign s -> c (THybridSign s) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (THybridSign s) toConstr :: THybridSign s -> Constr dataTypeOf :: THybridSign s -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (THybridSign s)) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (THybridSign s)) gmapT :: (forall b. Data b => b -> b) -> THybridSign s -> THybridSign s gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THybridSign s -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THybridSign s -> r gmapQ :: (forall d. Data d => d -> u) -> THybridSign s -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THybridSign s -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THybridSign s -> m (THybridSign s) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THybridSign s -> m (THybridSign s) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THybridSign s -> m (THybridSign s)
Ord s => Ord (THybridSign s) Source #
Methods compare :: THybridSign s -> THybridSign s -> Ordering (<) :: THybridSign s -> THybridSign s -> Bool (<=) :: THybridSign s -> THybridSign s -> Bool (>) :: THybridSign s -> THybridSign s -> Bool (>=) :: THybridSign s -> THybridSign s -> Bool max :: THybridSign s -> THybridSign s -> THybridSign s min :: THybridSign s -> THybridSign s -> THybridSign s
Show s => Show (THybridSign s) Source #
Methods showsPrec :: Int -> THybridSign s -> ShowS show :: THybridSign s -> String showList :: [THybridSign s] -> ShowS

emptyHybridSign :: Sgn_Wrap Source #

isSubTHybSgn :: Sgn_Wrap -> Sgn_Wrap -> Bool Source #

sgnDiff :: Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source #