Hets - the Heterogeneous Tool Set

LicenseGPLv2 or higher, see LICENSE.txt
Maintainernevrenato@gmail.com
Stabilityexperimental
Portabilityportable
Safe HaskellNone

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 # 
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 #

data THybridSign s Source #

Constructors

THybridSign 

Fields

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