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

TopHybrid.AS_TopHybrid

Description

Description : Abstract syntax for an hybridized logic. Declaration of the basic specification. Underlying Spec; Declaration of nominals and modalities, and axioms.

Documentation

data TH_BSPEC s Source #

Constructors

Bspec
Fields bitems :: [TH_BASIC_ITEM] und :: s

Instances

Data s => Data (TH_BSPEC s) Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TH_BSPEC s -> c (TH_BSPEC s) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TH_BSPEC s) toConstr :: TH_BSPEC s -> Constr dataTypeOf :: TH_BSPEC s -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (TH_BSPEC s)) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TH_BSPEC s)) gmapT :: (forall b. Data b => b -> b) -> TH_BSPEC s -> TH_BSPEC s gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TH_BSPEC s -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TH_BSPEC s -> r gmapQ :: (forall d. Data d => d -> u) -> TH_BSPEC s -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TH_BSPEC s -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s)
Show s => Show (TH_BSPEC s) Source #
Methods showsPrec :: Int -> TH_BSPEC s -> ShowS show :: TH_BSPEC s -> String showList :: [TH_BSPEC s] -> ShowS
GetRange s => GetRange (TH_BSPEC s) Source #
Methods getRange :: TH_BSPEC s -> Range Source # rangeSpan :: TH_BSPEC s -> [Pos] Source #

data TH_BASIC_ITEM Source #

Constructors

Simple_mod_decl [MODALITY]
Simple_nom_decl [NOMINAL]

Instances

Data TH_BASIC_ITEM Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TH_BASIC_ITEM -> c TH_BASIC_ITEM gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TH_BASIC_ITEM toConstr :: TH_BASIC_ITEM -> Constr dataTypeOf :: TH_BASIC_ITEM -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c TH_BASIC_ITEM) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TH_BASIC_ITEM) gmapT :: (forall b. Data b => b -> b) -> TH_BASIC_ITEM -> TH_BASIC_ITEM gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TH_BASIC_ITEM -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TH_BASIC_ITEM -> r gmapQ :: (forall d. Data d => d -> u) -> TH_BASIC_ITEM -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TH_BASIC_ITEM -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM
Show TH_BASIC_ITEM Source #
Methods showsPrec :: Int -> TH_BASIC_ITEM -> ShowS show :: TH_BASIC_ITEM -> String showList :: [TH_BASIC_ITEM] -> ShowS
GetRange TH_BASIC_ITEM Source #
Methods getRange :: TH_BASIC_ITEM -> Range Source # rangeSpan :: TH_BASIC_ITEM -> [Pos] Source #

type MODALITY = SIMPLE_ID Source #

type NOMINAL = SIMPLE_ID Source #

data TH_FORMULA f Source #

Constructors

At NOMINAL (TH_FORMULA f)
Uni NOMINAL (TH_FORMULA f)
Exist NOMINAL (TH_FORMULA f)
Box MODALITY (TH_FORMULA f)
Dia MODALITY (TH_FORMULA f)
UnderLogic f
Conjunction (TH_FORMULA f) (TH_FORMULA f)
Disjunction (TH_FORMULA f) (TH_FORMULA f)
Implication (TH_FORMULA f) (TH_FORMULA f)
BiImplication (TH_FORMULA f) (TH_FORMULA f)
Here NOMINAL
Neg (TH_FORMULA f)
Par (TH_FORMULA f)
TrueA
FalseA

Instances

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

data Frm_Wrap Source #

Constructors

Logic l sub bs f s sm si mo sy rw pf => Frm_Wrap l (TH_FORMULA f)

Instances

Eq Frm_Wrap Source #
Methods (==) :: Frm_Wrap -> Frm_Wrap -> Bool (/=) :: Frm_Wrap -> Frm_Wrap -> Bool
Ord Frm_Wrap Source #
Methods compare :: Frm_Wrap -> Frm_Wrap -> Ordering (<) :: Frm_Wrap -> Frm_Wrap -> Bool (<=) :: Frm_Wrap -> Frm_Wrap -> Bool (>) :: Frm_Wrap -> Frm_Wrap -> Bool (>=) :: Frm_Wrap -> Frm_Wrap -> Bool max :: Frm_Wrap -> Frm_Wrap -> Frm_Wrap min :: Frm_Wrap -> Frm_Wrap -> Frm_Wrap
Show Frm_Wrap Source #
Methods showsPrec :: Int -> Frm_Wrap -> ShowS show :: Frm_Wrap -> String showList :: [Frm_Wrap] -> ShowS
GetRange Frm_Wrap Source #
Methods getRange :: Frm_Wrap -> Range Source # rangeSpan :: Frm_Wrap -> [Pos] Source #
ToJson Frm_Wrap Source #
Methods asJson :: Frm_Wrap -> Json Source #
ToXml Frm_Wrap Source #
Methods asXml :: Frm_Wrap -> Element Source #
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 Spc_Wrap Source #

Constructors

Logic l sub bs sen si smi sign mor symb raw pf => Spc_Wrap l (TH_BSPEC bs) [Annoted Frm_Wrap]

Instances

Eq Spc_Wrap Source #
Methods (==) :: Spc_Wrap -> Spc_Wrap -> Bool (/=) :: Spc_Wrap -> Spc_Wrap -> Bool
Ord Spc_Wrap Source #
Methods compare :: Spc_Wrap -> Spc_Wrap -> Ordering (<) :: Spc_Wrap -> Spc_Wrap -> Bool (<=) :: Spc_Wrap -> Spc_Wrap -> Bool (>) :: Spc_Wrap -> Spc_Wrap -> Bool (>=) :: Spc_Wrap -> Spc_Wrap -> Bool max :: Spc_Wrap -> Spc_Wrap -> Spc_Wrap min :: Spc_Wrap -> Spc_Wrap -> Spc_Wrap
Show Spc_Wrap Source #
Methods showsPrec :: Int -> Spc_Wrap -> ShowS show :: Spc_Wrap -> String showList :: [Spc_Wrap] -> ShowS
Monoid Spc_Wrap Source #
Methods mempty :: Spc_Wrap mappend :: Spc_Wrap -> Spc_Wrap -> Spc_Wrap mconcat :: [Spc_Wrap] -> Spc_Wrap
GetRange Spc_Wrap Source #
Methods getRange :: Spc_Wrap -> Range Source # rangeSpan :: Spc_Wrap -> [Pos] Source #
Syntax Hybridize Spc_Wrap Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Methods parsersAndPrinters :: Hybridize -> Map String (PrefixMap -> AParser st Spc_Wrap, Spc_Wrap -> Doc) Source # parse_basic_spec :: Hybridize -> Maybe (PrefixMap -> AParser st Spc_Wrap) Source # parseSingleSymbItem :: Hybridize -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_items :: Hybridize -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_map_items :: Hybridize -> Maybe (AParser st SYMB_MAP_ITEMS) Source # toItem :: Hybridize -> Spc_Wrap -> Item Source # symb_items_name :: Hybridize -> SYMB_ITEMS -> [String] 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 Mor Source #

Constructors

Mor

Instances

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