Hets - the Heterogeneous Tool Set

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

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

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 # 

data TH_BASIC_ITEM Source #

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 # 

data TH_FORMULA f Source #

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 # 
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 # 
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 # 
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 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 # 
GetRange Spc_Wrap Source # 
Syntax Hybridize Spc_Wrap Symbol SYMB_ITEMS SYMB_MAP_ITEMS 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 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 # 
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 #