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

TopHybrid.TopHybridSign

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

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

Instances

Instances details

Eq Sgn_Wrap Source #
Instance details Defined in TopHybrid.TopHybridSign Methods (==) :: Sgn_Wrap -> Sgn_Wrap -> Bool (/=) :: Sgn_Wrap -> Sgn_Wrap -> Bool
Ord Sgn_Wrap Source #
Instance details Defined in TopHybrid.TopHybridSign 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 #
Instance details Defined in TopHybrid.TopHybridSign Methods showsPrec :: Int -> Sgn_Wrap -> ShowS show :: Sgn_Wrap -> String showList :: [Sgn_Wrap] -> ShowS
FromJSON Sgn_Wrap
Instance details Defined in TopHybrid.StatAna Methods parseJSON :: Value -> Parser Sgn_Wrap parseJSONList :: Value -> Parser [Sgn_Wrap]
ToJSON Sgn_Wrap
Instance details Defined in TopHybrid.StatAna Methods toJSON :: Sgn_Wrap -> Value toEncoding :: Sgn_Wrap -> Encoding toJSONList :: [Sgn_Wrap] -> Value toEncodingList :: [Sgn_Wrap] -> Encoding
ShATermConvertible Sgn_Wrap
Instance details Defined in TopHybrid.StatAna Methods toShATermAux :: ATermTable -> Sgn_Wrap -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Sgn_Wrap] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Sgn_Wrap) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sgn_Wrap])
Pretty Sgn_Wrap Source #
Instance details Defined in TopHybrid.Print_AS Methods pretty :: Sgn_Wrap -> Doc Source # pretties :: [Sgn_Wrap] -> Doc Source #
Category Sgn_Wrap Mor Source #
Instance details Defined in TopHybrid.Logic_TopHybrid Methods ide :: Sgn_Wrap -> Mor Source # composeMorphisms :: Mor -> Mor -> Result Mor Source # dom :: Mor -> Sgn_Wrap Source # cod :: Mor -> Sgn_Wrap Source # inverse :: Mor -> Result Mor Source # isInclusion :: Mor -> Bool Source # legal_mor :: Mor -> Result () Source #
Sentences Hybridize Frm_Wrap Sgn_Wrap Mor Symbol Source #
Instance details Defined in TopHybrid.Logic_TopHybrid 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 #
Instance details Defined in TopHybrid.Logic_TopHybrid 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 #
Instance details Defined in TopHybrid.Logic_TopHybrid 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

Instances details

Eq s => Eq (THybridSign s) Source #
Instance details Defined in TopHybrid.TopHybridSign Methods (==) :: THybridSign s -> THybridSign s -> Bool (/=) :: THybridSign s -> THybridSign s -> Bool
Data s => Data (THybridSign s) Source #
Instance details Defined in TopHybrid.TopHybridSign 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 :: forall r r'. (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 #
Instance details Defined in TopHybrid.TopHybridSign 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 #
Instance details Defined in TopHybrid.TopHybridSign Methods showsPrec :: Int -> THybridSign s -> ShowS show :: THybridSign s -> String showList :: [THybridSign s] -> ShowS
Generic (THybridSign s)
Instance details Defined in TopHybrid.ATC_TopHybrid Associated Types type Rep (THybridSign s) :: Type -> Type Methods from :: THybridSign s -> Rep (THybridSign s) x to :: Rep (THybridSign s) x -> THybridSign s
FromJSON s => FromJSON (THybridSign s)
Instance details Defined in TopHybrid.ATC_TopHybrid Methods parseJSON :: Value -> Parser (THybridSign s) parseJSONList :: Value -> Parser [THybridSign s]
ToJSON s => ToJSON (THybridSign s)
Instance details Defined in TopHybrid.ATC_TopHybrid Methods toJSON :: THybridSign s -> Value toEncoding :: THybridSign s -> Encoding toJSONList :: [THybridSign s] -> Value toEncodingList :: [THybridSign s] -> Encoding
ShATermConvertible s => ShATermConvertible (THybridSign s)
Instance details Defined in TopHybrid.ATC_TopHybrid Methods toShATermAux :: ATermTable -> THybridSign s -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THybridSign s] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THybridSign s) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THybridSign s])
Pretty s => Pretty (THybridSign s) Source #
Instance details Defined in TopHybrid.Print_AS Methods pretty :: THybridSign s -> Doc Source # pretties :: [THybridSign s] -> Doc Source #
type Rep (THybridSign s)
Instance details Defined in TopHybrid.ATC_TopHybrid type Rep (THybridSign s) = D1 ('MetaData "THybridSign" "TopHybrid.TopHybridSign" "main" 'False) (C1 ('MetaCons "THybridSign" 'PrefixI 'True) (S1 ('MetaSel ('Just "modies") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set MODALITY)) :: (S1 ('MetaSel ('Just "nomies") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set NOMINAL)) :: S1 ('MetaSel ('Just "extended") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 s))))

emptyHybridSign :: Sgn_Wrap Source #

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

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