Hets - the Heterogeneous Tool Set
Copyright(c) Christian Maeder and Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellSafe

CASL.Sign

Description

CASL signatures also serve as local environments for the basic static analysis

Synopsis

Documentation

data OpType Source #

Constructors

OpType 

Fields

Instances

Instances details
Eq OpType Source # 
Instance details

Defined in CASL.Sign

Methods

(==) :: OpType -> OpType -> Bool

(/=) :: OpType -> OpType -> Bool

Data OpType Source # 
Instance details

Defined in CASL.Sign

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpType -> c OpType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpType

toConstr :: OpType -> Constr

dataTypeOf :: OpType -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OpType)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpType)

gmapT :: (forall b. Data b => b -> b) -> OpType -> OpType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpType -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpType -> r

gmapQ :: (forall d. Data d => d -> u) -> OpType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> OpType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpType -> m OpType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpType -> m OpType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpType -> m OpType

Ord OpType Source # 
Instance details

Defined in CASL.Sign

Methods

compare :: OpType -> OpType -> Ordering

(<) :: OpType -> OpType -> Bool

(<=) :: OpType -> OpType -> Bool

(>) :: OpType -> OpType -> Bool

(>=) :: OpType -> OpType -> Bool

max :: OpType -> OpType -> OpType

min :: OpType -> OpType -> OpType

Show OpType Source # 
Instance details

Defined in CASL.Sign

Methods

showsPrec :: Int -> OpType -> ShowS

show :: OpType -> String

showList :: [OpType] -> ShowS

Generic OpType 
Instance details

Defined in CASL.ATC_CASL

Associated Types

type Rep OpType :: Type -> Type

Methods

from :: OpType -> Rep OpType x

to :: Rep OpType x -> OpType

FromJSON OpType 
Instance details

Defined in CASL.ATC_CASL

Methods

parseJSON :: Value -> Parser OpType

parseJSONList :: Value -> Parser [OpType]

ToJSON OpType 
Instance details

Defined in CASL.ATC_CASL

Methods

toJSON :: OpType -> Value

toEncoding :: OpType -> Encoding

toJSONList :: [OpType] -> Value

toEncodingList :: [OpType] -> Encoding

ShATermConvertible OpType 
Instance details

Defined in CASL.ATC_CASL

Methods

toShATermAux :: ATermTable -> OpType -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [OpType] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, OpType)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [OpType])

Pretty OpType Source # 
Instance details

Defined in CASL.Sign

type Rep OpType 
Instance details

Defined in CASL.ATC_CASL

type Rep OpType = D1 ('MetaData "OpType" "CASL.Sign" "main" 'False) (C1 ('MetaCons "OpType" 'PrefixI 'True) (S1 ('MetaSel ('Just "opKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpKind) :*: (S1 ('MetaSel ('Just "opArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SORT]) :*: S1 ('MetaSel ('Just "opRes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT))))

opSorts :: OpType -> [SORT] Source #

result sort added to argument sorts

data PredType Source #

Constructors

PredType 

Fields

Instances

Instances details
Eq PredType Source # 
Instance details

Defined in CASL.Sign

Methods

(==) :: PredType -> PredType -> Bool

(/=) :: PredType -> PredType -> Bool

Data PredType Source # 
Instance details

Defined in CASL.Sign

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PredType -> c PredType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PredType

toConstr :: PredType -> Constr

dataTypeOf :: PredType -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PredType)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredType)

gmapT :: (forall b. Data b => b -> b) -> PredType -> PredType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PredType -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PredType -> r

gmapQ :: (forall d. Data d => d -> u) -> PredType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> PredType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PredType -> m PredType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PredType -> m PredType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PredType -> m PredType

Ord PredType Source # 
Instance details

Defined in CASL.Sign

Methods

compare :: PredType -> PredType -> Ordering

(<) :: PredType -> PredType -> Bool

(<=) :: PredType -> PredType -> Bool

(>) :: PredType -> PredType -> Bool

(>=) :: PredType -> PredType -> Bool

max :: PredType -> PredType -> PredType

min :: PredType -> PredType -> PredType

Show PredType Source # 
Instance details

Defined in CASL.Sign

Methods

showsPrec :: Int -> PredType -> ShowS

show :: PredType -> String

showList :: [PredType] -> ShowS

Generic PredType 
Instance details

Defined in CASL.ATC_CASL

Associated Types

type Rep PredType :: Type -> Type

Methods

from :: PredType -> Rep PredType x

to :: Rep PredType x -> PredType

FromJSON PredType 
Instance details

Defined in CASL.ATC_CASL

Methods

parseJSON :: Value -> Parser PredType

parseJSONList :: Value -> Parser [PredType]

ToJSON PredType 
Instance details

Defined in CASL.ATC_CASL

Methods

toJSON :: PredType -> Value

toEncoding :: PredType -> Encoding

toJSONList :: [PredType] -> Value

toEncodingList :: [PredType] -> Encoding

ShATermConvertible PredType 
Instance details

Defined in CASL.ATC_CASL

Methods

toShATermAux :: ATermTable -> PredType -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [PredType] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, PredType)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [PredType])

Pretty PredType Source # 
Instance details

Defined in CASL.Sign

type Rep PredType 
Instance details

Defined in CASL.ATC_CASL

type Rep PredType = D1 ('MetaData "PredType" "CASL.Sign" "main" 'False) (C1 ('MetaCons "PredType" 'PrefixI 'True) (S1 ('MetaSel ('Just "predArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SORT])))

data SymbType Source #

Instances

Instances details
Eq SymbType Source # 
Instance details

Defined in CASL.Sign

Methods

(==) :: SymbType -> SymbType -> Bool

(/=) :: SymbType -> SymbType -> Bool

Data SymbType Source # 
Instance details

Defined in CASL.Sign

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbType -> c SymbType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbType

toConstr :: SymbType -> Constr

dataTypeOf :: SymbType -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SymbType)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbType)

gmapT :: (forall b. Data b => b -> b) -> SymbType -> SymbType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbType -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbType -> r

gmapQ :: (forall d. Data d => d -> u) -> SymbType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymbType -> m SymbType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbType -> m SymbType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbType -> m SymbType

Ord SymbType Source # 
Instance details

Defined in CASL.Sign

Methods

compare :: SymbType -> SymbType -> Ordering

(<) :: SymbType -> SymbType -> Bool

(<=) :: SymbType -> SymbType -> Bool

(>) :: SymbType -> SymbType -> Bool

(>=) :: SymbType -> SymbType -> Bool

max :: SymbType -> SymbType -> SymbType

min :: SymbType -> SymbType -> SymbType

Show SymbType Source # 
Instance details

Defined in CASL.Sign

Methods

showsPrec :: Int -> SymbType -> ShowS

show :: SymbType -> String

showList :: [SymbType] -> ShowS

Generic SymbType 
Instance details

Defined in CASL.ATC_CASL

Associated Types

type Rep SymbType :: Type -> Type

Methods

from :: SymbType -> Rep SymbType x

to :: Rep SymbType x -> SymbType

FromJSON SymbType 
Instance details

Defined in CASL.ATC_CASL

Methods

parseJSON :: Value -> Parser SymbType

parseJSONList :: Value -> Parser [SymbType]

ToJSON SymbType 
Instance details

Defined in CASL.ATC_CASL

Methods

toJSON :: SymbType -> Value

toEncoding :: SymbType -> Encoding

toJSONList :: [SymbType] -> Value

toEncodingList :: [SymbType] -> Encoding

ShATermConvertible SymbType 
Instance details

Defined in CASL.ATC_CASL

Methods

toShATermAux :: ATermTable -> SymbType -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [SymbType] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, SymbType)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [SymbType])

type Rep SymbType 
Instance details

Defined in CASL.ATC_CASL

type Rep SymbType = D1 ('MetaData "SymbType" "CASL.Sign" "main" 'False) ((C1 ('MetaCons "SortAsItemType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SubsortAsItemType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT))) :+: (C1 ('MetaCons "OpAsItemType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpType)) :+: C1 ('MetaCons "PredAsItemType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PredType))))

data Symbol Source #

Constructors

Symbol 

Fields

Instances

Instances details
Eq Symbol Source # 
Instance details

Defined in CASL.Sign

Methods

(==) :: Symbol -> Symbol -> Bool

(/=) :: Symbol -> Symbol -> Bool

Data Symbol Source # 
Instance details

Defined in CASL.Sign

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Symbol -> c Symbol

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Symbol

toConstr :: Symbol -> Constr

dataTypeOf :: Symbol -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Symbol)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol)

gmapT :: (forall b. Data b => b -> b) -> Symbol -> Symbol

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r

gmapQ :: (forall d. Data d => d -> u) -> Symbol -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Symbol -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol

Ord Symbol Source # 
Instance details

Defined in CASL.Sign

Methods

compare :: Symbol -> Symbol -> Ordering

(<) :: Symbol -> Symbol -> Bool

(<=) :: Symbol -> Symbol -> Bool

(>) :: Symbol -> Symbol -> Bool

(>=) :: Symbol -> Symbol -> Bool

max :: Symbol -> Symbol -> Symbol

min :: Symbol -> Symbol -> Symbol

Show Symbol Source # 
Instance details

Defined in CASL.Sign

Methods

showsPrec :: Int -> Symbol -> ShowS

show :: Symbol -> String

showList :: [Symbol] -> ShowS

Generic Symbol 
Instance details

Defined in CASL.ATC_CASL

Associated Types

type Rep Symbol :: Type -> Type

Methods

from :: Symbol -> Rep Symbol x

to :: Rep Symbol x -> Symbol

GetRange Symbol Source # 
Instance details

Defined in CASL.Sign

FromJSON Symbol 
Instance details

Defined in CASL.ATC_CASL

Methods

parseJSON :: Value -> Parser Symbol

parseJSONList :: Value -> Parser [Symbol]

ToJSON Symbol 
Instance details

Defined in CASL.ATC_CASL

Methods

toJSON :: Symbol -> Value

toEncoding :: Symbol -> Encoding

toJSONList :: [Symbol] -> Value

toEncodingList :: [Symbol] -> Encoding

ShATermConvertible Symbol 
Instance details

Defined in CASL.ATC_CASL

Methods

toShATermAux :: ATermTable -> Symbol -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Symbol] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Symbol)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Symbol])

Pretty Symbol Source # 
Instance details

Defined in CASL.Sign

ProjectSublogicM CASL_DL_SL Symbol Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

ProjectSublogic CASL_DL_SL Symbol Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

MinSublogic CASL_DL_SL Symbol Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Sentences CASL CASLFORMULA CASLSign CASLMor Symbol Source # 
Instance details

Defined in CASL.Logic_CASL

Sentences Modal ModalFORMULA MSign ModalMor Symbol Source # 
Instance details

Defined in Modal.Logic_Modal

Sentences Hybrid HybridFORMULA HSign HybridMor Symbol Source # 
Instance details

Defined in Hybrid.Logic_Hybrid

Sentences Fpl FplForm FplSign FplMor Symbol Source # 
Instance details

Defined in Fpl.Logic_Fpl

Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Sentences ConstraintCASL ConstraintCASLFORMULA ConstraintCASLSign ConstraintCASLMor Symbol Source # 
Instance details

Defined in ConstraintCASL.Logic_ConstraintCASL

Sentences CoCASL CoCASLFORMULA CSign CoCASLMor Symbol Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Sentences COL COLFORMULA CSign COLMor Symbol Source # 
Instance details

Defined in COL.Logic_COL

Sentences CASL_DL DLFORMULA DLSign DLMor Symbol Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Sentences Hybridize Frm_Wrap Sgn_Wrap Mor Symbol Source # 
Instance details

Defined in TopHybrid.Logic_TopHybrid

Sentences VSE Sentence VSESign VSEMor Symbol Source # 
Instance details

Defined in VSE.Logic_VSE

Syntax CASL CASLBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in CASL.Logic_CASL

Syntax Modal M_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in Modal.Logic_Modal

Syntax Hybrid H_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in Hybrid.Logic_Hybrid

Syntax Fpl FplBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in Fpl.Logic_Fpl

Syntax ExtModal EM_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Syntax ConstraintCASL ConstraintCASLBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in ConstraintCASL.Logic_ConstraintCASL

Syntax CoCASL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Syntax COL C_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in COL.Logic_COL

Syntax CASL_DL DL_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Syntax Hybridize Spc_Wrap Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in TopHybrid.Logic_TopHybrid

Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in VSE.Logic_VSE

StaticAnalysis CASL CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

basic_analysis :: CASL -> Maybe ((CASLBasicSpec, CASLSign, GlobalAnnos) -> Result (CASLBasicSpec, ExtSign CASLSign Symbol, [Named CASLFORMULA])) Source #

sen_analysis :: CASL -> Maybe ((CASLBasicSpec, CASLSign, CASLFORMULA) -> Result CASLFORMULA) Source #

extBasicAnalysis :: CASL -> IRI -> LibName -> CASLBasicSpec -> CASLSign -> GlobalAnnos -> Result (CASLBasicSpec, ExtSign CASLSign Symbol, [Named CASLFORMULA]) Source #

stat_symb_map_items :: CASL -> CASLSign -> Maybe CASLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: CASL -> CASLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: CASL -> Maybe ((CASLSign, [Named CASLFORMULA]) -> CASLBasicSpec) Source #

ensures_amalgamability :: CASL -> ([CASLAmalgOpt], Gr CASLSign (Int, CASLMor), [(Int, CASLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CASL -> CASLMor -> [Named CASLFORMULA] -> Result (CASLSign, [Named CASLFORMULA]) Source #

signature_colimit :: CASL -> Gr CASLSign (Int, CASLMor) -> Result (CASLSign, Map Int CASLMor) Source #

qualify :: CASL -> SIMPLE_ID -> LibName -> CASLMor -> CASLSign -> Result (CASLMor, [Named CASLFORMULA]) Source #

symbol_to_raw :: CASL -> Symbol -> RawSymbol Source #

id_to_raw :: CASL -> Id -> RawSymbol Source #

matches :: CASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: CASL -> CASLSign Source #

add_symb_to_sign :: CASL -> CASLSign -> Symbol -> Result CASLSign Source #

signature_union :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source #

signatureDiff :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source #

intersection :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source #

final_union :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source #

morphism_union :: CASL -> CASLMor -> CASLMor -> Result CASLMor Source #

is_subsig :: CASL -> CASLSign -> CASLSign -> Bool Source #

subsig_inclusion :: CASL -> CASLSign -> CASLSign -> Result CASLMor Source #

generated_sign :: CASL -> Set Symbol -> CASLSign -> Result CASLMor Source #

cogenerated_sign :: CASL -> Set Symbol -> CASLSign -> Result CASLMor Source #

induced_from_morphism :: CASL -> EndoMap RawSymbol -> CASLSign -> Result CASLMor Source #

induced_from_to_morphism :: CASL -> EndoMap RawSymbol -> ExtSign CASLSign Symbol -> ExtSign CASLSign Symbol -> Result CASLMor Source #

is_transportable :: CASL -> CASLMor -> Bool Source #

is_injective :: CASL -> CASLMor -> Bool Source #

theory_to_taxonomy :: CASL -> TaxoGraphKind -> MMiSSOntology -> CASLSign -> [Named CASLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: CASL -> String -> Bool -> CASLSign -> CASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CASLSign, [Named CASLFORMULA], CASLSign, CASLSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CASL -> CASLSign -> CASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CASLSign, CASLSign, CASLSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CASL -> [IRI] -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

StaticAnalysis Modal M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol Source # 
Instance details

Defined in Modal.Logic_Modal

Methods

basic_analysis :: Modal -> Maybe ((M_BASIC_SPEC, MSign, GlobalAnnos) -> Result (M_BASIC_SPEC, ExtSign MSign Symbol, [Named ModalFORMULA])) Source #

sen_analysis :: Modal -> Maybe ((M_BASIC_SPEC, MSign, ModalFORMULA) -> Result ModalFORMULA) Source #

extBasicAnalysis :: Modal -> IRI -> LibName -> M_BASIC_SPEC -> MSign -> GlobalAnnos -> Result (M_BASIC_SPEC, ExtSign MSign Symbol, [Named ModalFORMULA]) Source #

stat_symb_map_items :: Modal -> MSign -> Maybe MSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Modal -> MSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: Modal -> Maybe ((MSign, [Named ModalFORMULA]) -> M_BASIC_SPEC) Source #

ensures_amalgamability :: Modal -> ([CASLAmalgOpt], Gr MSign (Int, ModalMor), [(Int, ModalMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Modal -> ModalMor -> [Named ModalFORMULA] -> Result (MSign, [Named ModalFORMULA]) Source #

signature_colimit :: Modal -> Gr MSign (Int, ModalMor) -> Result (MSign, Map Int ModalMor) Source #

qualify :: Modal -> SIMPLE_ID -> LibName -> ModalMor -> MSign -> Result (ModalMor, [Named ModalFORMULA]) Source #

symbol_to_raw :: Modal -> Symbol -> RawSymbol Source #

id_to_raw :: Modal -> Id -> RawSymbol Source #

matches :: Modal -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: Modal -> MSign Source #

add_symb_to_sign :: Modal -> MSign -> Symbol -> Result MSign Source #

signature_union :: Modal -> MSign -> MSign -> Result MSign Source #

signatureDiff :: Modal -> MSign -> MSign -> Result MSign Source #

intersection :: Modal -> MSign -> MSign -> Result MSign Source #

final_union :: Modal -> MSign -> MSign -> Result MSign Source #

morphism_union :: Modal -> ModalMor -> ModalMor -> Result ModalMor Source #

is_subsig :: Modal -> MSign -> MSign -> Bool Source #

subsig_inclusion :: Modal -> MSign -> MSign -> Result ModalMor Source #

generated_sign :: Modal -> Set Symbol -> MSign -> Result ModalMor Source #

cogenerated_sign :: Modal -> Set Symbol -> MSign -> Result ModalMor Source #

induced_from_morphism :: Modal -> EndoMap RawSymbol -> MSign -> Result ModalMor Source #

induced_from_to_morphism :: Modal -> EndoMap RawSymbol -> ExtSign MSign Symbol -> ExtSign MSign Symbol -> Result ModalMor Source #

is_transportable :: Modal -> ModalMor -> Bool Source #

is_injective :: Modal -> ModalMor -> Bool Source #

theory_to_taxonomy :: Modal -> TaxoGraphKind -> MMiSSOntology -> MSign -> [Named ModalFORMULA] -> Result MMiSSOntology Source #

corresp2th :: Modal -> String -> Bool -> MSign -> MSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (MSign, [Named ModalFORMULA], MSign, MSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Modal -> MSign -> MSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (MSign, MSign, MSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Modal -> [IRI] -> (MSign, [Named ModalFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source #

StaticAnalysis Hybrid H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol Source # 
Instance details

Defined in Hybrid.Logic_Hybrid

Methods

basic_analysis :: Hybrid -> Maybe ((H_BASIC_SPEC, HSign, GlobalAnnos) -> Result (H_BASIC_SPEC, ExtSign HSign Symbol, [Named HybridFORMULA])) Source #

sen_analysis :: Hybrid -> Maybe ((H_BASIC_SPEC, HSign, HybridFORMULA) -> Result HybridFORMULA) Source #

extBasicAnalysis :: Hybrid -> IRI -> LibName -> H_BASIC_SPEC -> HSign -> GlobalAnnos -> Result (H_BASIC_SPEC, ExtSign HSign Symbol, [Named HybridFORMULA]) Source #

stat_symb_map_items :: Hybrid -> HSign -> Maybe HSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Hybrid -> HSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: Hybrid -> Maybe ((HSign, [Named HybridFORMULA]) -> H_BASIC_SPEC) Source #

ensures_amalgamability :: Hybrid -> ([CASLAmalgOpt], Gr HSign (Int, HybridMor), [(Int, HybridMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Hybrid -> HybridMor -> [Named HybridFORMULA] -> Result (HSign, [Named HybridFORMULA]) Source #

signature_colimit :: Hybrid -> Gr HSign (Int, HybridMor) -> Result (HSign, Map Int HybridMor) Source #

qualify :: Hybrid -> SIMPLE_ID -> LibName -> HybridMor -> HSign -> Result (HybridMor, [Named HybridFORMULA]) Source #

symbol_to_raw :: Hybrid -> Symbol -> RawSymbol Source #

id_to_raw :: Hybrid -> Id -> RawSymbol Source #

matches :: Hybrid -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: Hybrid -> HSign Source #

add_symb_to_sign :: Hybrid -> HSign -> Symbol -> Result HSign Source #

signature_union :: Hybrid -> HSign -> HSign -> Result HSign Source #

signatureDiff :: Hybrid -> HSign -> HSign -> Result HSign Source #

intersection :: Hybrid -> HSign -> HSign -> Result HSign Source #

final_union :: Hybrid -> HSign -> HSign -> Result HSign Source #

morphism_union :: Hybrid -> HybridMor -> HybridMor -> Result HybridMor Source #

is_subsig :: Hybrid -> HSign -> HSign -> Bool Source #

subsig_inclusion :: Hybrid -> HSign -> HSign -> Result HybridMor Source #

generated_sign :: Hybrid -> Set Symbol -> HSign -> Result HybridMor Source #

cogenerated_sign :: Hybrid -> Set Symbol -> HSign -> Result HybridMor Source #

induced_from_morphism :: Hybrid -> EndoMap RawSymbol -> HSign -> Result HybridMor Source #

induced_from_to_morphism :: Hybrid -> EndoMap RawSymbol -> ExtSign HSign Symbol -> ExtSign HSign Symbol -> Result HybridMor Source #

is_transportable :: Hybrid -> HybridMor -> Bool Source #

is_injective :: Hybrid -> HybridMor -> Bool Source #

theory_to_taxonomy :: Hybrid -> TaxoGraphKind -> MMiSSOntology -> HSign -> [Named HybridFORMULA] -> Result MMiSSOntology Source #

corresp2th :: Hybrid -> String -> Bool -> HSign -> HSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (HSign, [Named HybridFORMULA], HSign, HSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Hybrid -> HSign -> HSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (HSign, HSign, HSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Hybrid -> [IRI] -> (HSign, [Named HybridFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source #

StaticAnalysis Fpl FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol Source # 
Instance details

Defined in Fpl.Logic_Fpl

Methods

basic_analysis :: Fpl -> Maybe ((FplBasicSpec, FplSign, GlobalAnnos) -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])) Source #

sen_analysis :: Fpl -> Maybe ((FplBasicSpec, FplSign, FplForm) -> Result FplForm) Source #

extBasicAnalysis :: Fpl -> IRI -> LibName -> FplBasicSpec -> FplSign -> GlobalAnnos -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm]) Source #

stat_symb_map_items :: Fpl -> FplSign -> Maybe FplSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Fpl -> FplSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: Fpl -> Maybe ((FplSign, [Named FplForm]) -> FplBasicSpec) Source #

ensures_amalgamability :: Fpl -> ([CASLAmalgOpt], Gr FplSign (Int, FplMor), [(Int, FplMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Fpl -> FplMor -> [Named FplForm] -> Result (FplSign, [Named FplForm]) Source #

signature_colimit :: Fpl -> Gr FplSign (Int, FplMor) -> Result (FplSign, Map Int FplMor) Source #

qualify :: Fpl -> SIMPLE_ID -> LibName -> FplMor -> FplSign -> Result (FplMor, [Named FplForm]) Source #

symbol_to_raw :: Fpl -> Symbol -> RawSymbol Source #

id_to_raw :: Fpl -> Id -> RawSymbol Source #

matches :: Fpl -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: Fpl -> FplSign Source #

add_symb_to_sign :: Fpl -> FplSign -> Symbol -> Result FplSign Source #

signature_union :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

signatureDiff :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

intersection :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

final_union :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

morphism_union :: Fpl -> FplMor -> FplMor -> Result FplMor Source #

is_subsig :: Fpl -> FplSign -> FplSign -> Bool Source #

subsig_inclusion :: Fpl -> FplSign -> FplSign -> Result FplMor Source #

generated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor Source #

cogenerated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor Source #

induced_from_morphism :: Fpl -> EndoMap RawSymbol -> FplSign -> Result FplMor Source #

induced_from_to_morphism :: Fpl -> EndoMap RawSymbol -> ExtSign FplSign Symbol -> ExtSign FplSign Symbol -> Result FplMor Source #

is_transportable :: Fpl -> FplMor -> Bool Source #

is_injective :: Fpl -> FplMor -> Bool Source #

theory_to_taxonomy :: Fpl -> TaxoGraphKind -> MMiSSOntology -> FplSign -> [Named FplForm] -> Result MMiSSOntology Source #

corresp2th :: Fpl -> String -> Bool -> FplSign -> FplSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (FplSign, [Named FplForm], FplSign, FplSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Fpl -> FplSign -> FplSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (FplSign, FplSign, FplSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Fpl -> [IRI] -> (FplSign, [Named FplForm]) -> Result (FplSign, [Named FplForm]) Source #

StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Methods

basic_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, GlobalAnnos) -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA])) Source #

sen_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, ExtModalFORMULA) -> Result ExtModalFORMULA) Source #

extBasicAnalysis :: ExtModal -> IRI -> LibName -> EM_BASIC_SPEC -> ExtModalSign -> GlobalAnnos -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA]) Source #

stat_symb_map_items :: ExtModal -> ExtModalSign -> Maybe ExtModalSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: ExtModal -> ExtModalSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: ExtModal -> Maybe ((ExtModalSign, [Named ExtModalFORMULA]) -> EM_BASIC_SPEC) Source #

ensures_amalgamability :: ExtModal -> ([CASLAmalgOpt], Gr ExtModalSign (Int, ExtModalMorph), [(Int, ExtModalMorph)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: ExtModal -> ExtModalMorph -> [Named ExtModalFORMULA] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

signature_colimit :: ExtModal -> Gr ExtModalSign (Int, ExtModalMorph) -> Result (ExtModalSign, Map Int ExtModalMorph) Source #

qualify :: ExtModal -> SIMPLE_ID -> LibName -> ExtModalMorph -> ExtModalSign -> Result (ExtModalMorph, [Named ExtModalFORMULA]) Source #

symbol_to_raw :: ExtModal -> Symbol -> RawSymbol Source #

id_to_raw :: ExtModal -> Id -> RawSymbol Source #

matches :: ExtModal -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: ExtModal -> ExtModalSign Source #

add_symb_to_sign :: ExtModal -> ExtModalSign -> Symbol -> Result ExtModalSign Source #

signature_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

signatureDiff :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

intersection :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

final_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

morphism_union :: ExtModal -> ExtModalMorph -> ExtModalMorph -> Result ExtModalMorph Source #

is_subsig :: ExtModal -> ExtModalSign -> ExtModalSign -> Bool Source #

subsig_inclusion :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalMorph Source #

generated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source #

cogenerated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source #

induced_from_morphism :: ExtModal -> EndoMap RawSymbol -> ExtModalSign -> Result ExtModalMorph Source #

induced_from_to_morphism :: ExtModal -> EndoMap RawSymbol -> ExtSign ExtModalSign Symbol -> ExtSign ExtModalSign Symbol -> Result ExtModalMorph Source #

is_transportable :: ExtModal -> ExtModalMorph -> Bool Source #

is_injective :: ExtModal -> ExtModalMorph -> Bool Source #

theory_to_taxonomy :: ExtModal -> TaxoGraphKind -> MMiSSOntology -> ExtModalSign -> [Named ExtModalFORMULA] -> Result MMiSSOntology Source #

corresp2th :: ExtModal -> String -> Bool -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (ExtModalSign, [Named ExtModalFORMULA], ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: ExtModal -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (ExtModalSign, ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: ExtModal -> [IRI] -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

StaticAnalysis ConstraintCASL ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol Source # 
Instance details

Defined in ConstraintCASL.Logic_ConstraintCASL

Methods

basic_analysis :: ConstraintCASL -> Maybe ((ConstraintCASLBasicSpec, ConstraintCASLSign, GlobalAnnos) -> Result (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol, [Named ConstraintCASLFORMULA])) Source #

sen_analysis :: ConstraintCASL -> Maybe ((ConstraintCASLBasicSpec, ConstraintCASLSign, ConstraintCASLFORMULA) -> Result ConstraintCASLFORMULA) Source #

extBasicAnalysis :: ConstraintCASL -> IRI -> LibName -> ConstraintCASLBasicSpec -> ConstraintCASLSign -> GlobalAnnos -> Result (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol, [Named ConstraintCASLFORMULA]) Source #

stat_symb_map_items :: ConstraintCASL -> ConstraintCASLSign -> Maybe ConstraintCASLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: ConstraintCASL -> ConstraintCASLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: ConstraintCASL -> Maybe ((ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> ConstraintCASLBasicSpec) Source #

ensures_amalgamability :: ConstraintCASL -> ([CASLAmalgOpt], Gr ConstraintCASLSign (Int, ConstraintCASLMor), [(Int, ConstraintCASLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: ConstraintCASL -> ConstraintCASLMor -> [Named ConstraintCASLFORMULA] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #

signature_colimit :: ConstraintCASL -> Gr ConstraintCASLSign (Int, ConstraintCASLMor) -> Result (ConstraintCASLSign, Map Int ConstraintCASLMor) Source #

qualify :: ConstraintCASL -> SIMPLE_ID -> LibName -> ConstraintCASLMor -> ConstraintCASLSign -> Result (ConstraintCASLMor, [Named ConstraintCASLFORMULA]) Source #

symbol_to_raw :: ConstraintCASL -> Symbol -> RawSymbol Source #

id_to_raw :: ConstraintCASL -> Id -> RawSymbol Source #

matches :: ConstraintCASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: ConstraintCASL -> ConstraintCASLSign Source #

add_symb_to_sign :: ConstraintCASL -> ConstraintCASLSign -> Symbol -> Result ConstraintCASLSign Source #

signature_union :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source #

signatureDiff :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source #

intersection :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source #

final_union :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source #

morphism_union :: ConstraintCASL -> ConstraintCASLMor -> ConstraintCASLMor -> Result ConstraintCASLMor Source #

is_subsig :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Bool Source #

subsig_inclusion :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLMor Source #

generated_sign :: ConstraintCASL -> Set Symbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source #

cogenerated_sign :: ConstraintCASL -> Set Symbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source #

induced_from_morphism :: ConstraintCASL -> EndoMap RawSymbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source #

induced_from_to_morphism :: ConstraintCASL -> EndoMap RawSymbol -> ExtSign ConstraintCASLSign Symbol -> ExtSign ConstraintCASLSign Symbol -> Result ConstraintCASLMor Source #

is_transportable :: ConstraintCASL -> ConstraintCASLMor -> Bool Source #

is_injective :: ConstraintCASL -> ConstraintCASLMor -> Bool Source #

theory_to_taxonomy :: ConstraintCASL -> TaxoGraphKind -> MMiSSOntology -> ConstraintCASLSign -> [Named ConstraintCASLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: ConstraintCASL -> String -> Bool -> ConstraintCASLSign -> ConstraintCASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA], ConstraintCASLSign, ConstraintCASLSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (ConstraintCASLSign, ConstraintCASLSign, ConstraintCASLSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: ConstraintCASL -> [IRI] -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #

StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Methods

basic_analysis :: CoCASL -> Maybe ((C_BASIC_SPEC, CSign, GlobalAnnos) -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named CoCASLFORMULA])) Source #

sen_analysis :: CoCASL -> Maybe ((C_BASIC_SPEC, CSign, CoCASLFORMULA) -> Result CoCASLFORMULA) Source #

extBasicAnalysis :: CoCASL -> IRI -> LibName -> C_BASIC_SPEC -> CSign -> GlobalAnnos -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named CoCASLFORMULA]) Source #

stat_symb_map_items :: CoCASL -> CSign -> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: CoCASL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: CoCASL -> Maybe ((CSign, [Named CoCASLFORMULA]) -> C_BASIC_SPEC) Source #

ensures_amalgamability :: CoCASL -> ([CASLAmalgOpt], Gr CSign (Int, CoCASLMor), [(Int, CoCASLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CoCASL -> CoCASLMor -> [Named CoCASLFORMULA] -> Result (CSign, [Named CoCASLFORMULA]) Source #

signature_colimit :: CoCASL -> Gr CSign (Int, CoCASLMor) -> Result (CSign, Map Int CoCASLMor) Source #

qualify :: CoCASL -> SIMPLE_ID -> LibName -> CoCASLMor -> CSign -> Result (CoCASLMor, [Named CoCASLFORMULA]) Source #

symbol_to_raw :: CoCASL -> Symbol -> RawSymbol Source #

id_to_raw :: CoCASL -> Id -> RawSymbol Source #

matches :: CoCASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: CoCASL -> CSign Source #

add_symb_to_sign :: CoCASL -> CSign -> Symbol -> Result CSign Source #

signature_union :: CoCASL -> CSign -> CSign -> Result CSign Source #

signatureDiff :: CoCASL -> CSign -> CSign -> Result CSign Source #

intersection :: CoCASL -> CSign -> CSign -> Result CSign Source #

final_union :: CoCASL -> CSign -> CSign -> Result CSign Source #

morphism_union :: CoCASL -> CoCASLMor -> CoCASLMor -> Result CoCASLMor Source #

is_subsig :: CoCASL -> CSign -> CSign -> Bool Source #

subsig_inclusion :: CoCASL -> CSign -> CSign -> Result CoCASLMor Source #

generated_sign :: CoCASL -> Set Symbol -> CSign -> Result CoCASLMor Source #

cogenerated_sign :: CoCASL -> Set Symbol -> CSign -> Result CoCASLMor Source #

induced_from_morphism :: CoCASL -> EndoMap RawSymbol -> CSign -> Result CoCASLMor Source #

induced_from_to_morphism :: CoCASL -> EndoMap RawSymbol -> ExtSign CSign Symbol -> ExtSign CSign Symbol -> Result CoCASLMor Source #

is_transportable :: CoCASL -> CoCASLMor -> Bool Source #

is_injective :: CoCASL -> CoCASLMor -> Bool Source #

theory_to_taxonomy :: CoCASL -> TaxoGraphKind -> MMiSSOntology -> CSign -> [Named CoCASLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: CoCASL -> String -> Bool -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CSign, [Named CoCASLFORMULA], CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CoCASL -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CSign, CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CoCASL -> [IRI] -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source #

StaticAnalysis COL C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol Source # 
Instance details

Defined in COL.Logic_COL

Methods

basic_analysis :: COL -> Maybe ((C_BASIC_SPEC, CSign, GlobalAnnos) -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA])) Source #

sen_analysis :: COL -> Maybe ((C_BASIC_SPEC, CSign, COLFORMULA) -> Result COLFORMULA) Source #

extBasicAnalysis :: COL -> IRI -> LibName -> C_BASIC_SPEC -> CSign -> GlobalAnnos -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA]) Source #

stat_symb_map_items :: COL -> CSign -> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: COL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: COL -> Maybe ((CSign, [Named COLFORMULA]) -> C_BASIC_SPEC) Source #

ensures_amalgamability :: COL -> ([CASLAmalgOpt], Gr CSign (Int, COLMor), [(Int, COLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: COL -> COLMor -> [Named COLFORMULA] -> Result (CSign, [Named COLFORMULA]) Source #

signature_colimit :: COL -> Gr CSign (Int, COLMor) -> Result (CSign, Map Int COLMor) Source #

qualify :: COL -> SIMPLE_ID -> LibName -> COLMor -> CSign -> Result (COLMor, [Named COLFORMULA]) Source #

symbol_to_raw :: COL -> Symbol -> RawSymbol Source #

id_to_raw :: COL -> Id -> RawSymbol Source #

matches :: COL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: COL -> CSign Source #

add_symb_to_sign :: COL -> CSign -> Symbol -> Result CSign Source #

signature_union :: COL -> CSign -> CSign -> Result CSign Source #

signatureDiff :: COL -> CSign -> CSign -> Result CSign Source #

intersection :: COL -> CSign -> CSign -> Result CSign Source #

final_union :: COL -> CSign -> CSign -> Result CSign Source #

morphism_union :: COL -> COLMor -> COLMor -> Result COLMor Source #

is_subsig :: COL -> CSign -> CSign -> Bool Source #

subsig_inclusion :: COL -> CSign -> CSign -> Result COLMor Source #

generated_sign :: COL -> Set Symbol -> CSign -> Result COLMor Source #

cogenerated_sign :: COL -> Set Symbol -> CSign -> Result COLMor Source #

induced_from_morphism :: COL -> EndoMap RawSymbol -> CSign -> Result COLMor Source #

induced_from_to_morphism :: COL -> EndoMap RawSymbol -> ExtSign CSign Symbol -> ExtSign CSign Symbol -> Result COLMor Source #

is_transportable :: COL -> COLMor -> Bool Source #

is_injective :: COL -> COLMor -> Bool Source #

theory_to_taxonomy :: COL -> TaxoGraphKind -> MMiSSOntology -> CSign -> [Named COLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: COL -> String -> Bool -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CSign, [Named COLFORMULA], CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: COL -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CSign, CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: COL -> [IRI] -> (CSign, [Named COLFORMULA]) -> Result (CSign, [Named COLFORMULA]) Source #

StaticAnalysis CASL_DL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Methods

basic_analysis :: CASL_DL -> Maybe ((DL_BASIC_SPEC, DLSign, GlobalAnnos) -> Result (DL_BASIC_SPEC, ExtSign DLSign Symbol, [Named DLFORMULA])) Source #

sen_analysis :: CASL_DL -> Maybe ((DL_BASIC_SPEC, DLSign, DLFORMULA) -> Result DLFORMULA) Source #

extBasicAnalysis :: CASL_DL -> IRI -> LibName -> DL_BASIC_SPEC -> DLSign -> GlobalAnnos -> Result (DL_BASIC_SPEC, ExtSign DLSign Symbol, [Named DLFORMULA]) Source #

stat_symb_map_items :: CASL_DL -> DLSign -> Maybe DLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: CASL_DL -> DLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: CASL_DL -> Maybe ((DLSign, [Named DLFORMULA]) -> DL_BASIC_SPEC) Source #

ensures_amalgamability :: CASL_DL -> ([CASLAmalgOpt], Gr DLSign (Int, DLMor), [(Int, DLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CASL_DL -> DLMor -> [Named DLFORMULA] -> Result (DLSign, [Named DLFORMULA]) Source #

signature_colimit :: CASL_DL -> Gr DLSign (Int, DLMor) -> Result (DLSign, Map Int DLMor) Source #

qualify :: CASL_DL -> SIMPLE_ID -> LibName -> DLMor -> DLSign -> Result (DLMor, [Named DLFORMULA]) Source #

symbol_to_raw :: CASL_DL -> Symbol -> RawSymbol Source #

id_to_raw :: CASL_DL -> Id -> RawSymbol Source #

matches :: CASL_DL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: CASL_DL -> DLSign Source #

add_symb_to_sign :: CASL_DL -> DLSign -> Symbol -> Result DLSign Source #

signature_union :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source #

signatureDiff :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source #

intersection :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source #

final_union :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source #

morphism_union :: CASL_DL -> DLMor -> DLMor -> Result DLMor Source #

is_subsig :: CASL_DL -> DLSign -> DLSign -> Bool Source #

subsig_inclusion :: CASL_DL -> DLSign -> DLSign -> Result DLMor Source #

generated_sign :: CASL_DL -> Set Symbol -> DLSign -> Result DLMor Source #

cogenerated_sign :: CASL_DL -> Set Symbol -> DLSign -> Result DLMor Source #

induced_from_morphism :: CASL_DL -> EndoMap RawSymbol -> DLSign -> Result DLMor Source #

induced_from_to_morphism :: CASL_DL -> EndoMap RawSymbol -> ExtSign DLSign Symbol -> ExtSign DLSign Symbol -> Result DLMor Source #

is_transportable :: CASL_DL -> DLMor -> Bool Source #

is_injective :: CASL_DL -> DLMor -> Bool Source #

theory_to_taxonomy :: CASL_DL -> TaxoGraphKind -> MMiSSOntology -> DLSign -> [Named DLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: CASL_DL -> String -> Bool -> DLSign -> DLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (DLSign, [Named DLFORMULA], DLSign, DLSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CASL_DL -> DLSign -> DLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (DLSign, DLSign, DLSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CASL_DL -> [IRI] -> (DLSign, [Named DLFORMULA]) -> Result (DLSign, [Named DLFORMULA]) 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 #

StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source # 
Instance details

Defined in VSE.Logic_VSE

Methods

basic_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, GlobalAnnos) -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])) Source #

sen_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: VSE -> IRI -> LibName -> VSEBasicSpec -> VSESign -> GlobalAnnos -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: VSE -> VSESign -> Maybe VSESign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: VSE -> VSESign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: VSE -> Maybe ((VSESign, [Named Sentence]) -> VSEBasicSpec) Source #

ensures_amalgamability :: VSE -> ([CASLAmalgOpt], Gr VSESign (Int, VSEMor), [(Int, VSEMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: VSE -> VSEMor -> [Named Sentence] -> Result (VSESign, [Named Sentence]) Source #

signature_colimit :: VSE -> Gr VSESign (Int, VSEMor) -> Result (VSESign, Map Int VSEMor) Source #

qualify :: VSE -> SIMPLE_ID -> LibName -> VSEMor -> VSESign -> Result (VSEMor, [Named Sentence]) Source #

symbol_to_raw :: VSE -> Symbol -> RawSymbol Source #

id_to_raw :: VSE -> Id -> RawSymbol Source #

matches :: VSE -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: VSE -> VSESign Source #

add_symb_to_sign :: VSE -> VSESign -> Symbol -> Result VSESign Source #

signature_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

signatureDiff :: VSE -> VSESign -> VSESign -> Result VSESign Source #

intersection :: VSE -> VSESign -> VSESign -> Result VSESign Source #

final_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

morphism_union :: VSE -> VSEMor -> VSEMor -> Result VSEMor Source #

is_subsig :: VSE -> VSESign -> VSESign -> Bool Source #

subsig_inclusion :: VSE -> VSESign -> VSESign -> Result VSEMor Source #

generated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

cogenerated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

induced_from_morphism :: VSE -> EndoMap RawSymbol -> VSESign -> Result VSEMor Source #

induced_from_to_morphism :: VSE -> EndoMap RawSymbol -> ExtSign VSESign Symbol -> ExtSign VSESign Symbol -> Result VSEMor Source #

is_transportable :: VSE -> VSEMor -> Bool Source #

is_injective :: VSE -> VSEMor -> Bool Source #

theory_to_taxonomy :: VSE -> TaxoGraphKind -> MMiSSOntology -> VSESign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: VSE -> String -> Bool -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (VSESign, [Named Sentence], VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: VSE -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (VSESign, VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: VSE -> [IRI] -> (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence]) Source #

Logic CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

parse_basic_sen :: CASL -> Maybe (CASLBasicSpec -> AParser st CASLFORMULA) Source #

stability :: CASL -> Stability Source #

data_logic :: CASL -> Maybe AnyLogic Source #

top_sublogic :: CASL -> CASL_Sublogics Source #

all_sublogics :: CASL -> [CASL_Sublogics] Source #

bottomSublogic :: CASL -> Maybe CASL_Sublogics Source #

sublogicDimensions :: CASL -> [[CASL_Sublogics]] Source #

parseSublogic :: CASL -> String -> Maybe CASL_Sublogics Source #

proj_sublogic_epsilon :: CASL -> CASL_Sublogics -> CASLSign -> CASLMor Source #

provers :: CASL -> [Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree] Source #

default_prover :: CASL -> String Source #

cons_checkers :: CASL -> [ConsChecker CASLSign CASLFORMULA CASL_Sublogics CASLMor ProofTree] Source #

conservativityCheck :: CASL -> [ConservativityChecker CASLSign CASLFORMULA CASLMor] Source #

empty_proof_tree :: CASL -> ProofTree Source #

syntaxTable :: CASL -> CASLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CASL -> Maybe OMCD Source #

export_symToOmdoc :: CASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CASL -> NameMap Symbol -> CASLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: CASL -> SigMap Symbol -> CASLSign -> [Named CASLFORMULA] -> Result [TCElement] Source #

omdocToSym :: CASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CASLFORMULA)) Source #

addOMadtToTheory :: CASL -> SigMapI Symbol -> (CASLSign, [Named CASLFORMULA]) -> [[OmdADT]] -> Result (CASLSign, [Named CASLFORMULA]) Source #

addOmdocToTheory :: CASL -> SigMapI Symbol -> (CASLSign, [Named CASLFORMULA]) -> [TCElement] -> Result (CASLSign, [Named CASLFORMULA]) Source #

sublogicOfTheo :: CASL -> (CASLSign, [CASLFORMULA]) -> CASL_Sublogics Source #

Logic Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source # 
Instance details

Defined in Modal.Logic_Modal

Methods

parse_basic_sen :: Modal -> Maybe (M_BASIC_SPEC -> AParser st ModalFORMULA) Source #

stability :: Modal -> Stability Source #

data_logic :: Modal -> Maybe AnyLogic Source #

top_sublogic :: Modal -> () Source #

all_sublogics :: Modal -> [()] Source #

bottomSublogic :: Modal -> Maybe () Source #

sublogicDimensions :: Modal -> [[()]] Source #

parseSublogic :: Modal -> String -> Maybe () Source #

proj_sublogic_epsilon :: Modal -> () -> MSign -> ModalMor Source #

provers :: Modal -> [Prover MSign ModalFORMULA ModalMor () ()] Source #

default_prover :: Modal -> String Source #

cons_checkers :: Modal -> [ConsChecker MSign ModalFORMULA () ModalMor ()] Source #

conservativityCheck :: Modal -> [ConservativityChecker MSign ModalFORMULA ModalMor] Source #

empty_proof_tree :: Modal -> () Source #

syntaxTable :: Modal -> MSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Modal -> Maybe OMCD Source #

export_symToOmdoc :: Modal -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Modal -> NameMap Symbol -> ModalFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: Modal -> SigMap Symbol -> MSign -> [Named ModalFORMULA] -> Result [TCElement] Source #

omdocToSym :: Modal -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Modal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ModalFORMULA)) Source #

addOMadtToTheory :: Modal -> SigMapI Symbol -> (MSign, [Named ModalFORMULA]) -> [[OmdADT]] -> Result (MSign, [Named ModalFORMULA]) Source #

addOmdocToTheory :: Modal -> SigMapI Symbol -> (MSign, [Named ModalFORMULA]) -> [TCElement] -> Result (MSign, [Named ModalFORMULA]) Source #

sublogicOfTheo :: Modal -> (MSign, [ModalFORMULA]) -> () Source #

Logic Hybrid () H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol () Source # 
Instance details

Defined in Hybrid.Logic_Hybrid

Methods

parse_basic_sen :: Hybrid -> Maybe (H_BASIC_SPEC -> AParser st HybridFORMULA) Source #

stability :: Hybrid -> Stability Source #

data_logic :: Hybrid -> Maybe AnyLogic Source #

top_sublogic :: Hybrid -> () Source #

all_sublogics :: Hybrid -> [()] Source #

bottomSublogic :: Hybrid -> Maybe () Source #

sublogicDimensions :: Hybrid -> [[()]] Source #

parseSublogic :: Hybrid -> String -> Maybe () Source #

proj_sublogic_epsilon :: Hybrid -> () -> HSign -> HybridMor Source #

provers :: Hybrid -> [Prover HSign HybridFORMULA HybridMor () ()] Source #

default_prover :: Hybrid -> String Source #

cons_checkers :: Hybrid -> [ConsChecker HSign HybridFORMULA () HybridMor ()] Source #

conservativityCheck :: Hybrid -> [ConservativityChecker HSign HybridFORMULA HybridMor] Source #

empty_proof_tree :: Hybrid -> () Source #

syntaxTable :: Hybrid -> HSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Hybrid -> Maybe OMCD Source #

export_symToOmdoc :: Hybrid -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Hybrid -> NameMap Symbol -> HybridFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: Hybrid -> SigMap Symbol -> HSign -> [Named HybridFORMULA] -> Result [TCElement] Source #

omdocToSym :: Hybrid -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Hybrid -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named HybridFORMULA)) Source #

addOMadtToTheory :: Hybrid -> SigMapI Symbol -> (HSign, [Named HybridFORMULA]) -> [[OmdADT]] -> Result (HSign, [Named HybridFORMULA]) Source #

addOmdocToTheory :: Hybrid -> SigMapI Symbol -> (HSign, [Named HybridFORMULA]) -> [TCElement] -> Result (HSign, [Named HybridFORMULA]) Source #

sublogicOfTheo :: Hybrid -> (HSign, [HybridFORMULA]) -> () Source #

Logic Fpl () FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol () Source # 
Instance details

Defined in Fpl.Logic_Fpl

Methods

parse_basic_sen :: Fpl -> Maybe (FplBasicSpec -> AParser st FplForm) Source #

stability :: Fpl -> Stability Source #

data_logic :: Fpl -> Maybe AnyLogic Source #

top_sublogic :: Fpl -> () Source #

all_sublogics :: Fpl -> [()] Source #

bottomSublogic :: Fpl -> Maybe () Source #

sublogicDimensions :: Fpl -> [[()]] Source #

parseSublogic :: Fpl -> String -> Maybe () Source #

proj_sublogic_epsilon :: Fpl -> () -> FplSign -> FplMor Source #

provers :: Fpl -> [Prover FplSign FplForm FplMor () ()] Source #

default_prover :: Fpl -> String Source #

cons_checkers :: Fpl -> [ConsChecker FplSign FplForm () FplMor ()] Source #

conservativityCheck :: Fpl -> [ConservativityChecker FplSign FplForm FplMor] Source #

empty_proof_tree :: Fpl -> () Source #

syntaxTable :: Fpl -> FplSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Fpl -> Maybe OMCD Source #

export_symToOmdoc :: Fpl -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Fpl -> NameMap Symbol -> FplForm -> Result TCorOMElement Source #

export_theoryToOmdoc :: Fpl -> SigMap Symbol -> FplSign -> [Named FplForm] -> Result [TCElement] Source #

omdocToSym :: Fpl -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Fpl -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FplForm)) Source #

addOMadtToTheory :: Fpl -> SigMapI Symbol -> (FplSign, [Named FplForm]) -> [[OmdADT]] -> Result (FplSign, [Named FplForm]) Source #

addOmdocToTheory :: Fpl -> SigMapI Symbol -> (FplSign, [Named FplForm]) -> [TCElement] -> Result (FplSign, [Named FplForm]) Source #

sublogicOfTheo :: Fpl -> (FplSign, [FplForm]) -> () Source #

Logic ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Methods

parse_basic_sen :: ExtModal -> Maybe (EM_BASIC_SPEC -> AParser st ExtModalFORMULA) Source #

stability :: ExtModal -> Stability Source #

data_logic :: ExtModal -> Maybe AnyLogic Source #

top_sublogic :: ExtModal -> ExtModalSL Source #

all_sublogics :: ExtModal -> [ExtModalSL] Source #

bottomSublogic :: ExtModal -> Maybe ExtModalSL Source #

sublogicDimensions :: ExtModal -> [[ExtModalSL]] Source #

parseSublogic :: ExtModal -> String -> Maybe ExtModalSL Source #

proj_sublogic_epsilon :: ExtModal -> ExtModalSL -> ExtModalSign -> ExtModalMorph Source #

provers :: ExtModal -> [Prover ExtModalSign ExtModalFORMULA ExtModalMorph ExtModalSL ()] Source #

default_prover :: ExtModal -> String Source #

cons_checkers :: ExtModal -> [ConsChecker ExtModalSign ExtModalFORMULA ExtModalSL ExtModalMorph ()] Source #

conservativityCheck :: ExtModal -> [ConservativityChecker ExtModalSign ExtModalFORMULA ExtModalMorph] Source #

empty_proof_tree :: ExtModal -> () Source #

syntaxTable :: ExtModal -> ExtModalSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: ExtModal -> Maybe OMCD Source #

export_symToOmdoc :: ExtModal -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: ExtModal -> NameMap Symbol -> ExtModalFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: ExtModal -> SigMap Symbol -> ExtModalSign -> [Named ExtModalFORMULA] -> Result [TCElement] Source #

omdocToSym :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ExtModalFORMULA)) Source #

addOMadtToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [[OmdADT]] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

addOmdocToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [TCElement] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

sublogicOfTheo :: ExtModal -> (ExtModalSign, [ExtModalFORMULA]) -> ExtModalSL Source #

Logic ConstraintCASL CASL_Sublogics ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol () Source # 
Instance details

Defined in ConstraintCASL.Logic_ConstraintCASL

Methods

parse_basic_sen :: ConstraintCASL -> Maybe (ConstraintCASLBasicSpec -> AParser st ConstraintCASLFORMULA) Source #

stability :: ConstraintCASL -> Stability Source #

data_logic :: ConstraintCASL -> Maybe AnyLogic Source #

top_sublogic :: ConstraintCASL -> CASL_Sublogics Source #

all_sublogics :: ConstraintCASL -> [CASL_Sublogics] Source #

bottomSublogic :: ConstraintCASL -> Maybe CASL_Sublogics Source #

sublogicDimensions :: ConstraintCASL -> [[CASL_Sublogics]] Source #

parseSublogic :: ConstraintCASL -> String -> Maybe CASL_Sublogics Source #

proj_sublogic_epsilon :: ConstraintCASL -> CASL_Sublogics -> ConstraintCASLSign -> ConstraintCASLMor Source #

provers :: ConstraintCASL -> [Prover ConstraintCASLSign ConstraintCASLFORMULA ConstraintCASLMor CASL_Sublogics ()] Source #

default_prover :: ConstraintCASL -> String Source #

cons_checkers :: ConstraintCASL -> [ConsChecker ConstraintCASLSign ConstraintCASLFORMULA CASL_Sublogics ConstraintCASLMor ()] Source #

conservativityCheck :: ConstraintCASL -> [ConservativityChecker ConstraintCASLSign ConstraintCASLFORMULA ConstraintCASLMor] Source #

empty_proof_tree :: ConstraintCASL -> () Source #

syntaxTable :: ConstraintCASL -> ConstraintCASLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: ConstraintCASL -> Maybe OMCD Source #

export_symToOmdoc :: ConstraintCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: ConstraintCASL -> NameMap Symbol -> ConstraintCASLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: ConstraintCASL -> SigMap Symbol -> ConstraintCASLSign -> [Named ConstraintCASLFORMULA] -> Result [TCElement] Source #

omdocToSym :: ConstraintCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: ConstraintCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ConstraintCASLFORMULA)) Source #

addOMadtToTheory :: ConstraintCASL -> SigMapI Symbol -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> [[OmdADT]] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #

addOmdocToTheory :: ConstraintCASL -> SigMapI Symbol -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> [TCElement] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #

sublogicOfTheo :: ConstraintCASL -> (ConstraintCASLSign, [ConstraintCASLFORMULA]) -> CASL_Sublogics Source #

Logic CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Methods

parse_basic_sen :: CoCASL -> Maybe (C_BASIC_SPEC -> AParser st CoCASLFORMULA) Source #

stability :: CoCASL -> Stability Source #

data_logic :: CoCASL -> Maybe AnyLogic Source #

top_sublogic :: CoCASL -> CoCASL_Sublogics Source #

all_sublogics :: CoCASL -> [CoCASL_Sublogics] Source #

bottomSublogic :: CoCASL -> Maybe CoCASL_Sublogics Source #

sublogicDimensions :: CoCASL -> [[CoCASL_Sublogics]] Source #

parseSublogic :: CoCASL -> String -> Maybe CoCASL_Sublogics Source #

proj_sublogic_epsilon :: CoCASL -> CoCASL_Sublogics -> CSign -> CoCASLMor Source #

provers :: CoCASL -> [Prover CSign CoCASLFORMULA CoCASLMor CoCASL_Sublogics ()] Source #

default_prover :: CoCASL -> String Source #

cons_checkers :: CoCASL -> [ConsChecker CSign CoCASLFORMULA CoCASL_Sublogics CoCASLMor ()] Source #

conservativityCheck :: CoCASL -> [ConservativityChecker CSign CoCASLFORMULA CoCASLMor] Source #

empty_proof_tree :: CoCASL -> () Source #

syntaxTable :: CoCASL -> CSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CoCASL -> Maybe OMCD Source #

export_symToOmdoc :: CoCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CoCASL -> NameMap Symbol -> CoCASLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: CoCASL -> SigMap Symbol -> CSign -> [Named CoCASLFORMULA] -> Result [TCElement] Source #

omdocToSym :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CoCASLFORMULA)) Source #

addOMadtToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [[OmdADT]] -> Result (CSign, [Named CoCASLFORMULA]) Source #

addOmdocToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [TCElement] -> Result (CSign, [Named CoCASLFORMULA]) Source #

sublogicOfTheo :: CoCASL -> (CSign, [CoCASLFORMULA]) -> CoCASL_Sublogics Source #

Logic COL () C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol () Source # 
Instance details

Defined in COL.Logic_COL

Methods

parse_basic_sen :: COL -> Maybe (C_BASIC_SPEC -> AParser st COLFORMULA) Source #

stability :: COL -> Stability Source #

data_logic :: COL -> Maybe AnyLogic Source #

top_sublogic :: COL -> () Source #

all_sublogics :: COL -> [()] Source #

bottomSublogic :: COL -> Maybe () Source #

sublogicDimensions :: COL -> [[()]] Source #

parseSublogic :: COL -> String -> Maybe () Source #

proj_sublogic_epsilon :: COL -> () -> CSign -> COLMor Source #

provers :: COL -> [Prover CSign COLFORMULA COLMor () ()] Source #

default_prover :: COL -> String Source #

cons_checkers :: COL -> [ConsChecker CSign COLFORMULA () COLMor ()] Source #

conservativityCheck :: COL -> [ConservativityChecker CSign COLFORMULA COLMor] Source #

empty_proof_tree :: COL -> () Source #

syntaxTable :: COL -> CSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: COL -> Maybe OMCD Source #

export_symToOmdoc :: COL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: COL -> NameMap Symbol -> COLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: COL -> SigMap Symbol -> CSign -> [Named COLFORMULA] -> Result [TCElement] Source #

omdocToSym :: COL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: COL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named COLFORMULA)) Source #

addOMadtToTheory :: COL -> SigMapI Symbol -> (CSign, [Named COLFORMULA]) -> [[OmdADT]] -> Result (CSign, [Named COLFORMULA]) Source #

addOmdocToTheory :: COL -> SigMapI Symbol -> (CSign, [Named COLFORMULA]) -> [TCElement] -> Result (CSign, [Named COLFORMULA]) Source #

sublogicOfTheo :: COL -> (CSign, [COLFORMULA]) -> () Source #

Logic CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Methods

parse_basic_sen :: CASL_DL -> Maybe (DL_BASIC_SPEC -> AParser st DLFORMULA) Source #

stability :: CASL_DL -> Stability Source #

data_logic :: CASL_DL -> Maybe AnyLogic Source #

top_sublogic :: CASL_DL -> CASL_DL_SL Source #

all_sublogics :: CASL_DL -> [CASL_DL_SL] Source #

bottomSublogic :: CASL_DL -> Maybe CASL_DL_SL Source #

sublogicDimensions :: CASL_DL -> [[CASL_DL_SL]] Source #

parseSublogic :: CASL_DL -> String -> Maybe CASL_DL_SL Source #

proj_sublogic_epsilon :: CASL_DL -> CASL_DL_SL -> DLSign -> DLMor Source #

provers :: CASL_DL -> [Prover DLSign DLFORMULA DLMor CASL_DL_SL ProofTree] Source #

default_prover :: CASL_DL -> String Source #

cons_checkers :: CASL_DL -> [ConsChecker DLSign DLFORMULA CASL_DL_SL DLMor ProofTree] Source #

conservativityCheck :: CASL_DL -> [ConservativityChecker DLSign DLFORMULA DLMor] Source #

empty_proof_tree :: CASL_DL -> ProofTree Source #

syntaxTable :: CASL_DL -> DLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CASL_DL -> Maybe OMCD Source #

export_symToOmdoc :: CASL_DL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CASL_DL -> NameMap Symbol -> DLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: CASL_DL -> SigMap Symbol -> DLSign -> [Named DLFORMULA] -> Result [TCElement] Source #

omdocToSym :: CASL_DL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CASL_DL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named DLFORMULA)) Source #

addOMadtToTheory :: CASL_DL -> SigMapI Symbol -> (DLSign, [Named DLFORMULA]) -> [[OmdADT]] -> Result (DLSign, [Named DLFORMULA]) Source #

addOmdocToTheory :: CASL_DL -> SigMapI Symbol -> (DLSign, [Named DLFORMULA]) -> [TCElement] -> Result (DLSign, [Named DLFORMULA]) Source #

sublogicOfTheo :: CASL_DL -> (DLSign, [DLFORMULA]) -> CASL_DL_SL 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 #

Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Instance details

Defined in VSE.Logic_VSE

Methods

parse_basic_sen :: VSE -> Maybe (VSEBasicSpec -> AParser st Sentence) Source #

stability :: VSE -> Stability Source #

data_logic :: VSE -> Maybe AnyLogic Source #

top_sublogic :: VSE -> () Source #

all_sublogics :: VSE -> [()] Source #

bottomSublogic :: VSE -> Maybe () Source #

sublogicDimensions :: VSE -> [[()]] Source #

parseSublogic :: VSE -> String -> Maybe () Source #

proj_sublogic_epsilon :: VSE -> () -> VSESign -> VSEMor Source #

provers :: VSE -> [Prover VSESign Sentence VSEMor () ()] Source #

default_prover :: VSE -> String Source #

cons_checkers :: VSE -> [ConsChecker VSESign Sentence () VSEMor ()] Source #

conservativityCheck :: VSE -> [ConservativityChecker VSESign Sentence VSEMor] Source #

empty_proof_tree :: VSE -> () Source #

syntaxTable :: VSE -> VSESign -> Maybe SyntaxTable Source #

omdoc_metatheory :: VSE -> Maybe OMCD Source #

export_symToOmdoc :: VSE -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: VSE -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: VSE -> SigMap Symbol -> VSESign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: VSE -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: VSE -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [[OmdADT]] -> Result (VSESign, [Named Sentence]) Source #

addOmdocToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [TCElement] -> Result (VSESign, [Named Sentence]) Source #

sublogicOfTheo :: VSE -> (VSESign, [Sentence]) -> () Source #

Comorphism OWL22CASL OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in OWL2.OWL22CASL

Comorphism CASL2OWL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source # 
Instance details

Defined in OWL2.CASL2OWL

Comorphism ExtModal2OWL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source # 
Instance details

Defined in Comorphisms.ExtModal2OWL

Comorphism RelScheme2CASL RelScheme () RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.RelScheme2CASL

Comorphism Prop2CASL Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.Prop2CASL

Comorphism Modal2CASL Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.Modal2CASL

Comorphism Maude2CASL Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.Maude2CASL

Comorphism ExtModal2CASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.ExtModal2CASL

Comorphism DFOL2CASL DFOL () BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.DFOL2CASL

Comorphism CL2CFOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CommonLogic2CASL

Comorphism CSMOF2CASL CSMOF () Metamodel Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CSMOF2CASL

Comorphism QVTR2CASL QVTR () Transformation Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.QVTR2CASL

Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Comorphisms.CFOL2IsabelleHOL

Comorphism CASL2TopSort CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2TopSort

Comorphism CASL2SubCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2SubCFOL

Comorphism ExtModal2ExtModalTotal ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.ExtModal2ExtModalTotal

Methods

sourceLogic :: ExtModal2ExtModalTotal -> ExtModal Source #

sourceSublogic :: ExtModal2ExtModalTotal -> ExtModalSL Source #

sourceSublogicLossy :: ExtModal2ExtModalTotal -> ExtModalSL Source #

minSourceTheory :: ExtModal2ExtModalTotal -> Maybe (LibName, String) Source #

targetLogic :: ExtModal2ExtModalTotal -> ExtModal Source #

mapSublogic :: ExtModal2ExtModalTotal -> ExtModalSL -> Maybe ExtModalSL Source #

map_theory :: ExtModal2ExtModalTotal -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

mapMarkedTheory :: ExtModal2ExtModalTotal -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

map_morphism :: ExtModal2ExtModalTotal -> ExtModalMorph -> Result ExtModalMorph Source #

map_sentence :: ExtModal2ExtModalTotal -> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA Source #

map_symbol :: ExtModal2ExtModalTotal -> ExtModalSign -> Symbol -> Set Symbol Source #

extractModel :: ExtModal2ExtModalTotal -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

is_model_transportable :: ExtModal2ExtModalTotal -> Bool Source #

has_model_expansion :: ExtModal2ExtModalTotal -> Bool Source #

is_weakly_amalgamable :: ExtModal2ExtModalTotal -> Bool Source #

constituents :: ExtModal2ExtModalTotal -> [String] Source #

isInclusionComorphism :: ExtModal2ExtModalTotal -> Bool Source #

rps :: ExtModal2ExtModalTotal -> Bool Source #

eps :: ExtModal2ExtModalTotal -> Bool Source #

isGTC :: ExtModal2ExtModalTotal -> Bool Source #

Comorphism CASL2Skolem CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2Skolem

Comorphism CASL2Prop CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2Prop

Comorphism CASL2Prenex CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2Prenex

Comorphism CASL2PCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2PCFOL

Comorphism CspCASL2Modal CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CspCASL2Modal

Comorphism ExtModal2ExtModalNoSubsorts ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.ExtModal2ExtModalNoSubsorts

Methods

sourceLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source #

sourceSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source #

sourceSublogicLossy :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source #

minSourceTheory :: ExtModal2ExtModalNoSubsorts -> Maybe (LibName, String) Source #

targetLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source #

mapSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL -> Maybe ExtModalSL Source #

map_theory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

mapMarkedTheory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

map_morphism :: ExtModal2ExtModalNoSubsorts -> ExtModalMorph -> Result ExtModalMorph Source #

map_sentence :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA Source #

map_symbol :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> Symbol -> Set Symbol Source #

extractModel :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

is_model_transportable :: ExtModal2ExtModalNoSubsorts -> Bool Source #

has_model_expansion :: ExtModal2ExtModalNoSubsorts -> Bool Source #

is_weakly_amalgamable :: ExtModal2ExtModalNoSubsorts -> Bool Source #

constituents :: ExtModal2ExtModalNoSubsorts -> [String] Source #

isInclusionComorphism :: ExtModal2ExtModalNoSubsorts -> Bool Source #

rps :: ExtModal2ExtModalNoSubsorts -> Bool Source #

eps :: ExtModal2ExtModalNoSubsorts -> Bool Source #

isGTC :: ExtModal2ExtModalNoSubsorts -> Bool Source #

Comorphism CASL2NNF CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2NNF

Comorphism CASL2Modal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2Modal

Comorphism CASL2Hybrid CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Hybrid () H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2Hybrid

Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2HasCASL

Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.ExtModal2HasCASL

Comorphism CASL2ExtModal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2ExtModal

Comorphism CASL2CspCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2CspCASL

Comorphism Adl2CASL Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.Adl2CASL

Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Comorphisms.CoCFOL2IsabelleHOL

Comorphism CoCASL2CoSubCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CoCASL2CoSubCFOL

Comorphism CoCASL2CoPCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CoCASL2CoPCFOL

Comorphism CASL2CoCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2CoCASL

Comorphism CASL_DL2CASL CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL_DL2CASL

Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2VSERefine

Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2VSEImport

Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2VSE

Modification MODAL_EMBEDDING (InclComorphism CASL CASL_Sublogics) (CompComorphism CASL2Modal Modal2CASL) CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Modifications.ModalEmbedding

Lattice a => ProjectSublogicM (CASL_SL a) Symbol Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

projectSublogicM :: CASL_SL a -> Symbol -> Maybe Symbol Source #

Lattice a => MinSublogic (CASL_SL a) Symbol Source # 
Instance details

Defined in CASL.Logic_CASL

type Rep Symbol 
Instance details

Defined in CASL.ATC_CASL

type Rep Symbol = D1 ('MetaData "Symbol" "CASL.Sign" "main" 'False) (C1 ('MetaCons "Symbol" 'PrefixI 'True) (S1 ('MetaSel ('Just "symName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :*: S1 ('MetaSel ('Just "symbType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SymbType)))

type CASLSign = Sign () () Source #

data Sign f e Source #

the data type for the basic static analysis to accumulate variables, sentences, symbols, diagnostics and annotations, that are removed or ignored when looking at signatures from outside, i.e. during logic-independent processing.

Constructors

Sign 

Fields

Instances

Instances details
ProjectSublogic CASL_DL_SL DLSign Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

MinSublogic CASL_DL_SL DLSign Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Sentences CASL CASLFORMULA CASLSign CASLMor Symbol Source # 
Instance details

Defined in CASL.Logic_CASL

Sentences Modal ModalFORMULA MSign ModalMor Symbol Source # 
Instance details

Defined in Modal.Logic_Modal

Sentences Hybrid HybridFORMULA HSign HybridMor Symbol Source # 
Instance details

Defined in Hybrid.Logic_Hybrid

Sentences Fpl FplForm FplSign FplMor Symbol Source # 
Instance details

Defined in Fpl.Logic_Fpl

Sentences ExtModal ExtModalFORMULA ExtModalSign ExtModalMorph Symbol Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Sentences ConstraintCASL ConstraintCASLFORMULA ConstraintCASLSign ConstraintCASLMor Symbol Source # 
Instance details

Defined in ConstraintCASL.Logic_ConstraintCASL

Sentences CoCASL CoCASLFORMULA CSign CoCASLMor Symbol Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Sentences COL COLFORMULA CSign COLMor Symbol Source # 
Instance details

Defined in COL.Logic_COL

Sentences CASL_DL DLFORMULA DLSign DLMor Symbol Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Sentences VSE Sentence VSESign VSEMor Symbol Source # 
Instance details

Defined in VSE.Logic_VSE

StaticAnalysis CASL CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

basic_analysis :: CASL -> Maybe ((CASLBasicSpec, CASLSign, GlobalAnnos) -> Result (CASLBasicSpec, ExtSign CASLSign Symbol, [Named CASLFORMULA])) Source #

sen_analysis :: CASL -> Maybe ((CASLBasicSpec, CASLSign, CASLFORMULA) -> Result CASLFORMULA) Source #

extBasicAnalysis :: CASL -> IRI -> LibName -> CASLBasicSpec -> CASLSign -> GlobalAnnos -> Result (CASLBasicSpec, ExtSign CASLSign Symbol, [Named CASLFORMULA]) Source #

stat_symb_map_items :: CASL -> CASLSign -> Maybe CASLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: CASL -> CASLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: CASL -> Maybe ((CASLSign, [Named CASLFORMULA]) -> CASLBasicSpec) Source #

ensures_amalgamability :: CASL -> ([CASLAmalgOpt], Gr CASLSign (Int, CASLMor), [(Int, CASLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CASL -> CASLMor -> [Named CASLFORMULA] -> Result (CASLSign, [Named CASLFORMULA]) Source #

signature_colimit :: CASL -> Gr CASLSign (Int, CASLMor) -> Result (CASLSign, Map Int CASLMor) Source #

qualify :: CASL -> SIMPLE_ID -> LibName -> CASLMor -> CASLSign -> Result (CASLMor, [Named CASLFORMULA]) Source #

symbol_to_raw :: CASL -> Symbol -> RawSymbol Source #

id_to_raw :: CASL -> Id -> RawSymbol Source #

matches :: CASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: CASL -> CASLSign Source #

add_symb_to_sign :: CASL -> CASLSign -> Symbol -> Result CASLSign Source #

signature_union :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source #

signatureDiff :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source #

intersection :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source #

final_union :: CASL -> CASLSign -> CASLSign -> Result CASLSign Source #

morphism_union :: CASL -> CASLMor -> CASLMor -> Result CASLMor Source #

is_subsig :: CASL -> CASLSign -> CASLSign -> Bool Source #

subsig_inclusion :: CASL -> CASLSign -> CASLSign -> Result CASLMor Source #

generated_sign :: CASL -> Set Symbol -> CASLSign -> Result CASLMor Source #

cogenerated_sign :: CASL -> Set Symbol -> CASLSign -> Result CASLMor Source #

induced_from_morphism :: CASL -> EndoMap RawSymbol -> CASLSign -> Result CASLMor Source #

induced_from_to_morphism :: CASL -> EndoMap RawSymbol -> ExtSign CASLSign Symbol -> ExtSign CASLSign Symbol -> Result CASLMor Source #

is_transportable :: CASL -> CASLMor -> Bool Source #

is_injective :: CASL -> CASLMor -> Bool Source #

theory_to_taxonomy :: CASL -> TaxoGraphKind -> MMiSSOntology -> CASLSign -> [Named CASLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: CASL -> String -> Bool -> CASLSign -> CASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CASLSign, [Named CASLFORMULA], CASLSign, CASLSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CASL -> CASLSign -> CASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CASLSign, CASLSign, CASLSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CASL -> [IRI] -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

StaticAnalysis Modal M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol Source # 
Instance details

Defined in Modal.Logic_Modal

Methods

basic_analysis :: Modal -> Maybe ((M_BASIC_SPEC, MSign, GlobalAnnos) -> Result (M_BASIC_SPEC, ExtSign MSign Symbol, [Named ModalFORMULA])) Source #

sen_analysis :: Modal -> Maybe ((M_BASIC_SPEC, MSign, ModalFORMULA) -> Result ModalFORMULA) Source #

extBasicAnalysis :: Modal -> IRI -> LibName -> M_BASIC_SPEC -> MSign -> GlobalAnnos -> Result (M_BASIC_SPEC, ExtSign MSign Symbol, [Named ModalFORMULA]) Source #

stat_symb_map_items :: Modal -> MSign -> Maybe MSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Modal -> MSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: Modal -> Maybe ((MSign, [Named ModalFORMULA]) -> M_BASIC_SPEC) Source #

ensures_amalgamability :: Modal -> ([CASLAmalgOpt], Gr MSign (Int, ModalMor), [(Int, ModalMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Modal -> ModalMor -> [Named ModalFORMULA] -> Result (MSign, [Named ModalFORMULA]) Source #

signature_colimit :: Modal -> Gr MSign (Int, ModalMor) -> Result (MSign, Map Int ModalMor) Source #

qualify :: Modal -> SIMPLE_ID -> LibName -> ModalMor -> MSign -> Result (ModalMor, [Named ModalFORMULA]) Source #

symbol_to_raw :: Modal -> Symbol -> RawSymbol Source #

id_to_raw :: Modal -> Id -> RawSymbol Source #

matches :: Modal -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: Modal -> MSign Source #

add_symb_to_sign :: Modal -> MSign -> Symbol -> Result MSign Source #

signature_union :: Modal -> MSign -> MSign -> Result MSign Source #

signatureDiff :: Modal -> MSign -> MSign -> Result MSign Source #

intersection :: Modal -> MSign -> MSign -> Result MSign Source #

final_union :: Modal -> MSign -> MSign -> Result MSign Source #

morphism_union :: Modal -> ModalMor -> ModalMor -> Result ModalMor Source #

is_subsig :: Modal -> MSign -> MSign -> Bool Source #

subsig_inclusion :: Modal -> MSign -> MSign -> Result ModalMor Source #

generated_sign :: Modal -> Set Symbol -> MSign -> Result ModalMor Source #

cogenerated_sign :: Modal -> Set Symbol -> MSign -> Result ModalMor Source #

induced_from_morphism :: Modal -> EndoMap RawSymbol -> MSign -> Result ModalMor Source #

induced_from_to_morphism :: Modal -> EndoMap RawSymbol -> ExtSign MSign Symbol -> ExtSign MSign Symbol -> Result ModalMor Source #

is_transportable :: Modal -> ModalMor -> Bool Source #

is_injective :: Modal -> ModalMor -> Bool Source #

theory_to_taxonomy :: Modal -> TaxoGraphKind -> MMiSSOntology -> MSign -> [Named ModalFORMULA] -> Result MMiSSOntology Source #

corresp2th :: Modal -> String -> Bool -> MSign -> MSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (MSign, [Named ModalFORMULA], MSign, MSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Modal -> MSign -> MSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (MSign, MSign, MSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Modal -> [IRI] -> (MSign, [Named ModalFORMULA]) -> Result (MSign, [Named ModalFORMULA]) Source #

StaticAnalysis Hybrid H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol Source # 
Instance details

Defined in Hybrid.Logic_Hybrid

Methods

basic_analysis :: Hybrid -> Maybe ((H_BASIC_SPEC, HSign, GlobalAnnos) -> Result (H_BASIC_SPEC, ExtSign HSign Symbol, [Named HybridFORMULA])) Source #

sen_analysis :: Hybrid -> Maybe ((H_BASIC_SPEC, HSign, HybridFORMULA) -> Result HybridFORMULA) Source #

extBasicAnalysis :: Hybrid -> IRI -> LibName -> H_BASIC_SPEC -> HSign -> GlobalAnnos -> Result (H_BASIC_SPEC, ExtSign HSign Symbol, [Named HybridFORMULA]) Source #

stat_symb_map_items :: Hybrid -> HSign -> Maybe HSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Hybrid -> HSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: Hybrid -> Maybe ((HSign, [Named HybridFORMULA]) -> H_BASIC_SPEC) Source #

ensures_amalgamability :: Hybrid -> ([CASLAmalgOpt], Gr HSign (Int, HybridMor), [(Int, HybridMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Hybrid -> HybridMor -> [Named HybridFORMULA] -> Result (HSign, [Named HybridFORMULA]) Source #

signature_colimit :: Hybrid -> Gr HSign (Int, HybridMor) -> Result (HSign, Map Int HybridMor) Source #

qualify :: Hybrid -> SIMPLE_ID -> LibName -> HybridMor -> HSign -> Result (HybridMor, [Named HybridFORMULA]) Source #

symbol_to_raw :: Hybrid -> Symbol -> RawSymbol Source #

id_to_raw :: Hybrid -> Id -> RawSymbol Source #

matches :: Hybrid -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: Hybrid -> HSign Source #

add_symb_to_sign :: Hybrid -> HSign -> Symbol -> Result HSign Source #

signature_union :: Hybrid -> HSign -> HSign -> Result HSign Source #

signatureDiff :: Hybrid -> HSign -> HSign -> Result HSign Source #

intersection :: Hybrid -> HSign -> HSign -> Result HSign Source #

final_union :: Hybrid -> HSign -> HSign -> Result HSign Source #

morphism_union :: Hybrid -> HybridMor -> HybridMor -> Result HybridMor Source #

is_subsig :: Hybrid -> HSign -> HSign -> Bool Source #

subsig_inclusion :: Hybrid -> HSign -> HSign -> Result HybridMor Source #

generated_sign :: Hybrid -> Set Symbol -> HSign -> Result HybridMor Source #

cogenerated_sign :: Hybrid -> Set Symbol -> HSign -> Result HybridMor Source #

induced_from_morphism :: Hybrid -> EndoMap RawSymbol -> HSign -> Result HybridMor Source #

induced_from_to_morphism :: Hybrid -> EndoMap RawSymbol -> ExtSign HSign Symbol -> ExtSign HSign Symbol -> Result HybridMor Source #

is_transportable :: Hybrid -> HybridMor -> Bool Source #

is_injective :: Hybrid -> HybridMor -> Bool Source #

theory_to_taxonomy :: Hybrid -> TaxoGraphKind -> MMiSSOntology -> HSign -> [Named HybridFORMULA] -> Result MMiSSOntology Source #

corresp2th :: Hybrid -> String -> Bool -> HSign -> HSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (HSign, [Named HybridFORMULA], HSign, HSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Hybrid -> HSign -> HSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (HSign, HSign, HSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Hybrid -> [IRI] -> (HSign, [Named HybridFORMULA]) -> Result (HSign, [Named HybridFORMULA]) Source #

StaticAnalysis Fpl FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol Source # 
Instance details

Defined in Fpl.Logic_Fpl

Methods

basic_analysis :: Fpl -> Maybe ((FplBasicSpec, FplSign, GlobalAnnos) -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm])) Source #

sen_analysis :: Fpl -> Maybe ((FplBasicSpec, FplSign, FplForm) -> Result FplForm) Source #

extBasicAnalysis :: Fpl -> IRI -> LibName -> FplBasicSpec -> FplSign -> GlobalAnnos -> Result (FplBasicSpec, ExtSign FplSign Symbol, [Named FplForm]) Source #

stat_symb_map_items :: Fpl -> FplSign -> Maybe FplSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: Fpl -> FplSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: Fpl -> Maybe ((FplSign, [Named FplForm]) -> FplBasicSpec) Source #

ensures_amalgamability :: Fpl -> ([CASLAmalgOpt], Gr FplSign (Int, FplMor), [(Int, FplMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Fpl -> FplMor -> [Named FplForm] -> Result (FplSign, [Named FplForm]) Source #

signature_colimit :: Fpl -> Gr FplSign (Int, FplMor) -> Result (FplSign, Map Int FplMor) Source #

qualify :: Fpl -> SIMPLE_ID -> LibName -> FplMor -> FplSign -> Result (FplMor, [Named FplForm]) Source #

symbol_to_raw :: Fpl -> Symbol -> RawSymbol Source #

id_to_raw :: Fpl -> Id -> RawSymbol Source #

matches :: Fpl -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: Fpl -> FplSign Source #

add_symb_to_sign :: Fpl -> FplSign -> Symbol -> Result FplSign Source #

signature_union :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

signatureDiff :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

intersection :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

final_union :: Fpl -> FplSign -> FplSign -> Result FplSign Source #

morphism_union :: Fpl -> FplMor -> FplMor -> Result FplMor Source #

is_subsig :: Fpl -> FplSign -> FplSign -> Bool Source #

subsig_inclusion :: Fpl -> FplSign -> FplSign -> Result FplMor Source #

generated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor Source #

cogenerated_sign :: Fpl -> Set Symbol -> FplSign -> Result FplMor Source #

induced_from_morphism :: Fpl -> EndoMap RawSymbol -> FplSign -> Result FplMor Source #

induced_from_to_morphism :: Fpl -> EndoMap RawSymbol -> ExtSign FplSign Symbol -> ExtSign FplSign Symbol -> Result FplMor Source #

is_transportable :: Fpl -> FplMor -> Bool Source #

is_injective :: Fpl -> FplMor -> Bool Source #

theory_to_taxonomy :: Fpl -> TaxoGraphKind -> MMiSSOntology -> FplSign -> [Named FplForm] -> Result MMiSSOntology Source #

corresp2th :: Fpl -> String -> Bool -> FplSign -> FplSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (FplSign, [Named FplForm], FplSign, FplSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Fpl -> FplSign -> FplSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (FplSign, FplSign, FplSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Fpl -> [IRI] -> (FplSign, [Named FplForm]) -> Result (FplSign, [Named FplForm]) Source #

StaticAnalysis ExtModal EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Methods

basic_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, GlobalAnnos) -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA])) Source #

sen_analysis :: ExtModal -> Maybe ((EM_BASIC_SPEC, ExtModalSign, ExtModalFORMULA) -> Result ExtModalFORMULA) Source #

extBasicAnalysis :: ExtModal -> IRI -> LibName -> EM_BASIC_SPEC -> ExtModalSign -> GlobalAnnos -> Result (EM_BASIC_SPEC, ExtSign ExtModalSign Symbol, [Named ExtModalFORMULA]) Source #

stat_symb_map_items :: ExtModal -> ExtModalSign -> Maybe ExtModalSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: ExtModal -> ExtModalSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: ExtModal -> Maybe ((ExtModalSign, [Named ExtModalFORMULA]) -> EM_BASIC_SPEC) Source #

ensures_amalgamability :: ExtModal -> ([CASLAmalgOpt], Gr ExtModalSign (Int, ExtModalMorph), [(Int, ExtModalMorph)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: ExtModal -> ExtModalMorph -> [Named ExtModalFORMULA] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

signature_colimit :: ExtModal -> Gr ExtModalSign (Int, ExtModalMorph) -> Result (ExtModalSign, Map Int ExtModalMorph) Source #

qualify :: ExtModal -> SIMPLE_ID -> LibName -> ExtModalMorph -> ExtModalSign -> Result (ExtModalMorph, [Named ExtModalFORMULA]) Source #

symbol_to_raw :: ExtModal -> Symbol -> RawSymbol Source #

id_to_raw :: ExtModal -> Id -> RawSymbol Source #

matches :: ExtModal -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: ExtModal -> ExtModalSign Source #

add_symb_to_sign :: ExtModal -> ExtModalSign -> Symbol -> Result ExtModalSign Source #

signature_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

signatureDiff :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

intersection :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

final_union :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalSign Source #

morphism_union :: ExtModal -> ExtModalMorph -> ExtModalMorph -> Result ExtModalMorph Source #

is_subsig :: ExtModal -> ExtModalSign -> ExtModalSign -> Bool Source #

subsig_inclusion :: ExtModal -> ExtModalSign -> ExtModalSign -> Result ExtModalMorph Source #

generated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source #

cogenerated_sign :: ExtModal -> Set Symbol -> ExtModalSign -> Result ExtModalMorph Source #

induced_from_morphism :: ExtModal -> EndoMap RawSymbol -> ExtModalSign -> Result ExtModalMorph Source #

induced_from_to_morphism :: ExtModal -> EndoMap RawSymbol -> ExtSign ExtModalSign Symbol -> ExtSign ExtModalSign Symbol -> Result ExtModalMorph Source #

is_transportable :: ExtModal -> ExtModalMorph -> Bool Source #

is_injective :: ExtModal -> ExtModalMorph -> Bool Source #

theory_to_taxonomy :: ExtModal -> TaxoGraphKind -> MMiSSOntology -> ExtModalSign -> [Named ExtModalFORMULA] -> Result MMiSSOntology Source #

corresp2th :: ExtModal -> String -> Bool -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (ExtModalSign, [Named ExtModalFORMULA], ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: ExtModal -> ExtModalSign -> ExtModalSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (ExtModalSign, ExtModalSign, ExtModalSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: ExtModal -> [IRI] -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

StaticAnalysis ConstraintCASL ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol Source # 
Instance details

Defined in ConstraintCASL.Logic_ConstraintCASL

Methods

basic_analysis :: ConstraintCASL -> Maybe ((ConstraintCASLBasicSpec, ConstraintCASLSign, GlobalAnnos) -> Result (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol, [Named ConstraintCASLFORMULA])) Source #

sen_analysis :: ConstraintCASL -> Maybe ((ConstraintCASLBasicSpec, ConstraintCASLSign, ConstraintCASLFORMULA) -> Result ConstraintCASLFORMULA) Source #

extBasicAnalysis :: ConstraintCASL -> IRI -> LibName -> ConstraintCASLBasicSpec -> ConstraintCASLSign -> GlobalAnnos -> Result (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol, [Named ConstraintCASLFORMULA]) Source #

stat_symb_map_items :: ConstraintCASL -> ConstraintCASLSign -> Maybe ConstraintCASLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: ConstraintCASL -> ConstraintCASLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: ConstraintCASL -> Maybe ((ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> ConstraintCASLBasicSpec) Source #

ensures_amalgamability :: ConstraintCASL -> ([CASLAmalgOpt], Gr ConstraintCASLSign (Int, ConstraintCASLMor), [(Int, ConstraintCASLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: ConstraintCASL -> ConstraintCASLMor -> [Named ConstraintCASLFORMULA] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #

signature_colimit :: ConstraintCASL -> Gr ConstraintCASLSign (Int, ConstraintCASLMor) -> Result (ConstraintCASLSign, Map Int ConstraintCASLMor) Source #

qualify :: ConstraintCASL -> SIMPLE_ID -> LibName -> ConstraintCASLMor -> ConstraintCASLSign -> Result (ConstraintCASLMor, [Named ConstraintCASLFORMULA]) Source #

symbol_to_raw :: ConstraintCASL -> Symbol -> RawSymbol Source #

id_to_raw :: ConstraintCASL -> Id -> RawSymbol Source #

matches :: ConstraintCASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: ConstraintCASL -> ConstraintCASLSign Source #

add_symb_to_sign :: ConstraintCASL -> ConstraintCASLSign -> Symbol -> Result ConstraintCASLSign Source #

signature_union :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source #

signatureDiff :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source #

intersection :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source #

final_union :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLSign Source #

morphism_union :: ConstraintCASL -> ConstraintCASLMor -> ConstraintCASLMor -> Result ConstraintCASLMor Source #

is_subsig :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Bool Source #

subsig_inclusion :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Result ConstraintCASLMor Source #

generated_sign :: ConstraintCASL -> Set Symbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source #

cogenerated_sign :: ConstraintCASL -> Set Symbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source #

induced_from_morphism :: ConstraintCASL -> EndoMap RawSymbol -> ConstraintCASLSign -> Result ConstraintCASLMor Source #

induced_from_to_morphism :: ConstraintCASL -> EndoMap RawSymbol -> ExtSign ConstraintCASLSign Symbol -> ExtSign ConstraintCASLSign Symbol -> Result ConstraintCASLMor Source #

is_transportable :: ConstraintCASL -> ConstraintCASLMor -> Bool Source #

is_injective :: ConstraintCASL -> ConstraintCASLMor -> Bool Source #

theory_to_taxonomy :: ConstraintCASL -> TaxoGraphKind -> MMiSSOntology -> ConstraintCASLSign -> [Named ConstraintCASLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: ConstraintCASL -> String -> Bool -> ConstraintCASLSign -> ConstraintCASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA], ConstraintCASLSign, ConstraintCASLSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (ConstraintCASLSign, ConstraintCASLSign, ConstraintCASLSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: ConstraintCASL -> [IRI] -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #

StaticAnalysis CoCASL C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Methods

basic_analysis :: CoCASL -> Maybe ((C_BASIC_SPEC, CSign, GlobalAnnos) -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named CoCASLFORMULA])) Source #

sen_analysis :: CoCASL -> Maybe ((C_BASIC_SPEC, CSign, CoCASLFORMULA) -> Result CoCASLFORMULA) Source #

extBasicAnalysis :: CoCASL -> IRI -> LibName -> C_BASIC_SPEC -> CSign -> GlobalAnnos -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named CoCASLFORMULA]) Source #

stat_symb_map_items :: CoCASL -> CSign -> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: CoCASL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: CoCASL -> Maybe ((CSign, [Named CoCASLFORMULA]) -> C_BASIC_SPEC) Source #

ensures_amalgamability :: CoCASL -> ([CASLAmalgOpt], Gr CSign (Int, CoCASLMor), [(Int, CoCASLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CoCASL -> CoCASLMor -> [Named CoCASLFORMULA] -> Result (CSign, [Named CoCASLFORMULA]) Source #

signature_colimit :: CoCASL -> Gr CSign (Int, CoCASLMor) -> Result (CSign, Map Int CoCASLMor) Source #

qualify :: CoCASL -> SIMPLE_ID -> LibName -> CoCASLMor -> CSign -> Result (CoCASLMor, [Named CoCASLFORMULA]) Source #

symbol_to_raw :: CoCASL -> Symbol -> RawSymbol Source #

id_to_raw :: CoCASL -> Id -> RawSymbol Source #

matches :: CoCASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: CoCASL -> CSign Source #

add_symb_to_sign :: CoCASL -> CSign -> Symbol -> Result CSign Source #

signature_union :: CoCASL -> CSign -> CSign -> Result CSign Source #

signatureDiff :: CoCASL -> CSign -> CSign -> Result CSign Source #

intersection :: CoCASL -> CSign -> CSign -> Result CSign Source #

final_union :: CoCASL -> CSign -> CSign -> Result CSign Source #

morphism_union :: CoCASL -> CoCASLMor -> CoCASLMor -> Result CoCASLMor Source #

is_subsig :: CoCASL -> CSign -> CSign -> Bool Source #

subsig_inclusion :: CoCASL -> CSign -> CSign -> Result CoCASLMor Source #

generated_sign :: CoCASL -> Set Symbol -> CSign -> Result CoCASLMor Source #

cogenerated_sign :: CoCASL -> Set Symbol -> CSign -> Result CoCASLMor Source #

induced_from_morphism :: CoCASL -> EndoMap RawSymbol -> CSign -> Result CoCASLMor Source #

induced_from_to_morphism :: CoCASL -> EndoMap RawSymbol -> ExtSign CSign Symbol -> ExtSign CSign Symbol -> Result CoCASLMor Source #

is_transportable :: CoCASL -> CoCASLMor -> Bool Source #

is_injective :: CoCASL -> CoCASLMor -> Bool Source #

theory_to_taxonomy :: CoCASL -> TaxoGraphKind -> MMiSSOntology -> CSign -> [Named CoCASLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: CoCASL -> String -> Bool -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CSign, [Named CoCASLFORMULA], CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CoCASL -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CSign, CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CoCASL -> [IRI] -> (CSign, [Named CoCASLFORMULA]) -> Result (CSign, [Named CoCASLFORMULA]) Source #

StaticAnalysis COL C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol Source # 
Instance details

Defined in COL.Logic_COL

Methods

basic_analysis :: COL -> Maybe ((C_BASIC_SPEC, CSign, GlobalAnnos) -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA])) Source #

sen_analysis :: COL -> Maybe ((C_BASIC_SPEC, CSign, COLFORMULA) -> Result COLFORMULA) Source #

extBasicAnalysis :: COL -> IRI -> LibName -> C_BASIC_SPEC -> CSign -> GlobalAnnos -> Result (C_BASIC_SPEC, ExtSign CSign Symbol, [Named COLFORMULA]) Source #

stat_symb_map_items :: COL -> CSign -> Maybe CSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: COL -> CSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: COL -> Maybe ((CSign, [Named COLFORMULA]) -> C_BASIC_SPEC) Source #

ensures_amalgamability :: COL -> ([CASLAmalgOpt], Gr CSign (Int, COLMor), [(Int, COLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: COL -> COLMor -> [Named COLFORMULA] -> Result (CSign, [Named COLFORMULA]) Source #

signature_colimit :: COL -> Gr CSign (Int, COLMor) -> Result (CSign, Map Int COLMor) Source #

qualify :: COL -> SIMPLE_ID -> LibName -> COLMor -> CSign -> Result (COLMor, [Named COLFORMULA]) Source #

symbol_to_raw :: COL -> Symbol -> RawSymbol Source #

id_to_raw :: COL -> Id -> RawSymbol Source #

matches :: COL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: COL -> CSign Source #

add_symb_to_sign :: COL -> CSign -> Symbol -> Result CSign Source #

signature_union :: COL -> CSign -> CSign -> Result CSign Source #

signatureDiff :: COL -> CSign -> CSign -> Result CSign Source #

intersection :: COL -> CSign -> CSign -> Result CSign Source #

final_union :: COL -> CSign -> CSign -> Result CSign Source #

morphism_union :: COL -> COLMor -> COLMor -> Result COLMor Source #

is_subsig :: COL -> CSign -> CSign -> Bool Source #

subsig_inclusion :: COL -> CSign -> CSign -> Result COLMor Source #

generated_sign :: COL -> Set Symbol -> CSign -> Result COLMor Source #

cogenerated_sign :: COL -> Set Symbol -> CSign -> Result COLMor Source #

induced_from_morphism :: COL -> EndoMap RawSymbol -> CSign -> Result COLMor Source #

induced_from_to_morphism :: COL -> EndoMap RawSymbol -> ExtSign CSign Symbol -> ExtSign CSign Symbol -> Result COLMor Source #

is_transportable :: COL -> COLMor -> Bool Source #

is_injective :: COL -> COLMor -> Bool Source #

theory_to_taxonomy :: COL -> TaxoGraphKind -> MMiSSOntology -> CSign -> [Named COLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: COL -> String -> Bool -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (CSign, [Named COLFORMULA], CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: COL -> CSign -> CSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (CSign, CSign, CSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: COL -> [IRI] -> (CSign, [Named COLFORMULA]) -> Result (CSign, [Named COLFORMULA]) Source #

StaticAnalysis CASL_DL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Methods

basic_analysis :: CASL_DL -> Maybe ((DL_BASIC_SPEC, DLSign, GlobalAnnos) -> Result (DL_BASIC_SPEC, ExtSign DLSign Symbol, [Named DLFORMULA])) Source #

sen_analysis :: CASL_DL -> Maybe ((DL_BASIC_SPEC, DLSign, DLFORMULA) -> Result DLFORMULA) Source #

extBasicAnalysis :: CASL_DL -> IRI -> LibName -> DL_BASIC_SPEC -> DLSign -> GlobalAnnos -> Result (DL_BASIC_SPEC, ExtSign DLSign Symbol, [Named DLFORMULA]) Source #

stat_symb_map_items :: CASL_DL -> DLSign -> Maybe DLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: CASL_DL -> DLSign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: CASL_DL -> Maybe ((DLSign, [Named DLFORMULA]) -> DL_BASIC_SPEC) Source #

ensures_amalgamability :: CASL_DL -> ([CASLAmalgOpt], Gr DLSign (Int, DLMor), [(Int, DLMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CASL_DL -> DLMor -> [Named DLFORMULA] -> Result (DLSign, [Named DLFORMULA]) Source #

signature_colimit :: CASL_DL -> Gr DLSign (Int, DLMor) -> Result (DLSign, Map Int DLMor) Source #

qualify :: CASL_DL -> SIMPLE_ID -> LibName -> DLMor -> DLSign -> Result (DLMor, [Named DLFORMULA]) Source #

symbol_to_raw :: CASL_DL -> Symbol -> RawSymbol Source #

id_to_raw :: CASL_DL -> Id -> RawSymbol Source #

matches :: CASL_DL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: CASL_DL -> DLSign Source #

add_symb_to_sign :: CASL_DL -> DLSign -> Symbol -> Result DLSign Source #

signature_union :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source #

signatureDiff :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source #

intersection :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source #

final_union :: CASL_DL -> DLSign -> DLSign -> Result DLSign Source #

morphism_union :: CASL_DL -> DLMor -> DLMor -> Result DLMor Source #

is_subsig :: CASL_DL -> DLSign -> DLSign -> Bool Source #

subsig_inclusion :: CASL_DL -> DLSign -> DLSign -> Result DLMor Source #

generated_sign :: CASL_DL -> Set Symbol -> DLSign -> Result DLMor Source #

cogenerated_sign :: CASL_DL -> Set Symbol -> DLSign -> Result DLMor Source #

induced_from_morphism :: CASL_DL -> EndoMap RawSymbol -> DLSign -> Result DLMor Source #

induced_from_to_morphism :: CASL_DL -> EndoMap RawSymbol -> ExtSign DLSign Symbol -> ExtSign DLSign Symbol -> Result DLMor Source #

is_transportable :: CASL_DL -> DLMor -> Bool Source #

is_injective :: CASL_DL -> DLMor -> Bool Source #

theory_to_taxonomy :: CASL_DL -> TaxoGraphKind -> MMiSSOntology -> DLSign -> [Named DLFORMULA] -> Result MMiSSOntology Source #

corresp2th :: CASL_DL -> String -> Bool -> DLSign -> DLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (DLSign, [Named DLFORMULA], DLSign, DLSign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CASL_DL -> DLSign -> DLSign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (DLSign, DLSign, DLSign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CASL_DL -> [IRI] -> (DLSign, [Named DLFORMULA]) -> Result (DLSign, [Named DLFORMULA]) Source #

StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source # 
Instance details

Defined in VSE.Logic_VSE

Methods

basic_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, GlobalAnnos) -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])) Source #

sen_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: VSE -> IRI -> LibName -> VSEBasicSpec -> VSESign -> GlobalAnnos -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: VSE -> VSESign -> Maybe VSESign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: VSE -> VSESign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: VSE -> Maybe ((VSESign, [Named Sentence]) -> VSEBasicSpec) Source #

ensures_amalgamability :: VSE -> ([CASLAmalgOpt], Gr VSESign (Int, VSEMor), [(Int, VSEMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: VSE -> VSEMor -> [Named Sentence] -> Result (VSESign, [Named Sentence]) Source #

signature_colimit :: VSE -> Gr VSESign (Int, VSEMor) -> Result (VSESign, Map Int VSEMor) Source #

qualify :: VSE -> SIMPLE_ID -> LibName -> VSEMor -> VSESign -> Result (VSEMor, [Named Sentence]) Source #

symbol_to_raw :: VSE -> Symbol -> RawSymbol Source #

id_to_raw :: VSE -> Id -> RawSymbol Source #

matches :: VSE -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: VSE -> VSESign Source #

add_symb_to_sign :: VSE -> VSESign -> Symbol -> Result VSESign Source #

signature_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

signatureDiff :: VSE -> VSESign -> VSESign -> Result VSESign Source #

intersection :: VSE -> VSESign -> VSESign -> Result VSESign Source #

final_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

morphism_union :: VSE -> VSEMor -> VSEMor -> Result VSEMor Source #

is_subsig :: VSE -> VSESign -> VSESign -> Bool Source #

subsig_inclusion :: VSE -> VSESign -> VSESign -> Result VSEMor Source #

generated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

cogenerated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

induced_from_morphism :: VSE -> EndoMap RawSymbol -> VSESign -> Result VSEMor Source #

induced_from_to_morphism :: VSE -> EndoMap RawSymbol -> ExtSign VSESign Symbol -> ExtSign VSESign Symbol -> Result VSEMor Source #

is_transportable :: VSE -> VSEMor -> Bool Source #

is_injective :: VSE -> VSEMor -> Bool Source #

theory_to_taxonomy :: VSE -> TaxoGraphKind -> MMiSSOntology -> VSESign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: VSE -> String -> Bool -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (VSESign, [Named Sentence], VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: VSE -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (VSESign, VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: VSE -> [IRI] -> (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence]) Source #

Logic CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

parse_basic_sen :: CASL -> Maybe (CASLBasicSpec -> AParser st CASLFORMULA) Source #

stability :: CASL -> Stability Source #

data_logic :: CASL -> Maybe AnyLogic Source #

top_sublogic :: CASL -> CASL_Sublogics Source #

all_sublogics :: CASL -> [CASL_Sublogics] Source #

bottomSublogic :: CASL -> Maybe CASL_Sublogics Source #

sublogicDimensions :: CASL -> [[CASL_Sublogics]] Source #

parseSublogic :: CASL -> String -> Maybe CASL_Sublogics Source #

proj_sublogic_epsilon :: CASL -> CASL_Sublogics -> CASLSign -> CASLMor Source #

provers :: CASL -> [Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree] Source #

default_prover :: CASL -> String Source #

cons_checkers :: CASL -> [ConsChecker CASLSign CASLFORMULA CASL_Sublogics CASLMor ProofTree] Source #

conservativityCheck :: CASL -> [ConservativityChecker CASLSign CASLFORMULA CASLMor] Source #

empty_proof_tree :: CASL -> ProofTree Source #

syntaxTable :: CASL -> CASLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CASL -> Maybe OMCD Source #

export_symToOmdoc :: CASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CASL -> NameMap Symbol -> CASLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: CASL -> SigMap Symbol -> CASLSign -> [Named CASLFORMULA] -> Result [TCElement] Source #

omdocToSym :: CASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CASLFORMULA)) Source #

addOMadtToTheory :: CASL -> SigMapI Symbol -> (CASLSign, [Named CASLFORMULA]) -> [[OmdADT]] -> Result (CASLSign, [Named CASLFORMULA]) Source #

addOmdocToTheory :: CASL -> SigMapI Symbol -> (CASLSign, [Named CASLFORMULA]) -> [TCElement] -> Result (CASLSign, [Named CASLFORMULA]) Source #

sublogicOfTheo :: CASL -> (CASLSign, [CASLFORMULA]) -> CASL_Sublogics Source #

Logic Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source # 
Instance details

Defined in Modal.Logic_Modal

Methods

parse_basic_sen :: Modal -> Maybe (M_BASIC_SPEC -> AParser st ModalFORMULA) Source #

stability :: Modal -> Stability Source #

data_logic :: Modal -> Maybe AnyLogic Source #

top_sublogic :: Modal -> () Source #

all_sublogics :: Modal -> [()] Source #

bottomSublogic :: Modal -> Maybe () Source #

sublogicDimensions :: Modal -> [[()]] Source #

parseSublogic :: Modal -> String -> Maybe () Source #

proj_sublogic_epsilon :: Modal -> () -> MSign -> ModalMor Source #

provers :: Modal -> [Prover MSign ModalFORMULA ModalMor () ()] Source #

default_prover :: Modal -> String Source #

cons_checkers :: Modal -> [ConsChecker MSign ModalFORMULA () ModalMor ()] Source #

conservativityCheck :: Modal -> [ConservativityChecker MSign ModalFORMULA ModalMor] Source #

empty_proof_tree :: Modal -> () Source #

syntaxTable :: Modal -> MSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Modal -> Maybe OMCD Source #

export_symToOmdoc :: Modal -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Modal -> NameMap Symbol -> ModalFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: Modal -> SigMap Symbol -> MSign -> [Named ModalFORMULA] -> Result [TCElement] Source #

omdocToSym :: Modal -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Modal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ModalFORMULA)) Source #

addOMadtToTheory :: Modal -> SigMapI Symbol -> (MSign, [Named ModalFORMULA]) -> [[OmdADT]] -> Result (MSign, [Named ModalFORMULA]) Source #

addOmdocToTheory :: Modal -> SigMapI Symbol -> (MSign, [Named ModalFORMULA]) -> [TCElement] -> Result (MSign, [Named ModalFORMULA]) Source #

sublogicOfTheo :: Modal -> (MSign, [ModalFORMULA]) -> () Source #

Logic Hybrid () H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol () Source # 
Instance details

Defined in Hybrid.Logic_Hybrid

Methods

parse_basic_sen :: Hybrid -> Maybe (H_BASIC_SPEC -> AParser st HybridFORMULA) Source #

stability :: Hybrid -> Stability Source #

data_logic :: Hybrid -> Maybe AnyLogic Source #

top_sublogic :: Hybrid -> () Source #

all_sublogics :: Hybrid -> [()] Source #

bottomSublogic :: Hybrid -> Maybe () Source #

sublogicDimensions :: Hybrid -> [[()]] Source #

parseSublogic :: Hybrid -> String -> Maybe () Source #

proj_sublogic_epsilon :: Hybrid -> () -> HSign -> HybridMor Source #

provers :: Hybrid -> [Prover HSign HybridFORMULA HybridMor () ()] Source #

default_prover :: Hybrid -> String Source #

cons_checkers :: Hybrid -> [ConsChecker HSign HybridFORMULA () HybridMor ()] Source #

conservativityCheck :: Hybrid -> [ConservativityChecker HSign HybridFORMULA HybridMor] Source #

empty_proof_tree :: Hybrid -> () Source #

syntaxTable :: Hybrid -> HSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Hybrid -> Maybe OMCD Source #

export_symToOmdoc :: Hybrid -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Hybrid -> NameMap Symbol -> HybridFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: Hybrid -> SigMap Symbol -> HSign -> [Named HybridFORMULA] -> Result [TCElement] Source #

omdocToSym :: Hybrid -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Hybrid -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named HybridFORMULA)) Source #

addOMadtToTheory :: Hybrid -> SigMapI Symbol -> (HSign, [Named HybridFORMULA]) -> [[OmdADT]] -> Result (HSign, [Named HybridFORMULA]) Source #

addOmdocToTheory :: Hybrid -> SigMapI Symbol -> (HSign, [Named HybridFORMULA]) -> [TCElement] -> Result (HSign, [Named HybridFORMULA]) Source #

sublogicOfTheo :: Hybrid -> (HSign, [HybridFORMULA]) -> () Source #

Logic Fpl () FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS FplSign FplMor Symbol RawSymbol () Source # 
Instance details

Defined in Fpl.Logic_Fpl

Methods

parse_basic_sen :: Fpl -> Maybe (FplBasicSpec -> AParser st FplForm) Source #

stability :: Fpl -> Stability Source #

data_logic :: Fpl -> Maybe AnyLogic Source #

top_sublogic :: Fpl -> () Source #

all_sublogics :: Fpl -> [()] Source #

bottomSublogic :: Fpl -> Maybe () Source #

sublogicDimensions :: Fpl -> [[()]] Source #

parseSublogic :: Fpl -> String -> Maybe () Source #

proj_sublogic_epsilon :: Fpl -> () -> FplSign -> FplMor Source #

provers :: Fpl -> [Prover FplSign FplForm FplMor () ()] Source #

default_prover :: Fpl -> String Source #

cons_checkers :: Fpl -> [ConsChecker FplSign FplForm () FplMor ()] Source #

conservativityCheck :: Fpl -> [ConservativityChecker FplSign FplForm FplMor] Source #

empty_proof_tree :: Fpl -> () Source #

syntaxTable :: Fpl -> FplSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Fpl -> Maybe OMCD Source #

export_symToOmdoc :: Fpl -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Fpl -> NameMap Symbol -> FplForm -> Result TCorOMElement Source #

export_theoryToOmdoc :: Fpl -> SigMap Symbol -> FplSign -> [Named FplForm] -> Result [TCElement] Source #

omdocToSym :: Fpl -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Fpl -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named FplForm)) Source #

addOMadtToTheory :: Fpl -> SigMapI Symbol -> (FplSign, [Named FplForm]) -> [[OmdADT]] -> Result (FplSign, [Named FplForm]) Source #

addOmdocToTheory :: Fpl -> SigMapI Symbol -> (FplSign, [Named FplForm]) -> [TCElement] -> Result (FplSign, [Named FplForm]) Source #

sublogicOfTheo :: Fpl -> (FplSign, [FplForm]) -> () Source #

Logic ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

Methods

parse_basic_sen :: ExtModal -> Maybe (EM_BASIC_SPEC -> AParser st ExtModalFORMULA) Source #

stability :: ExtModal -> Stability Source #

data_logic :: ExtModal -> Maybe AnyLogic Source #

top_sublogic :: ExtModal -> ExtModalSL Source #

all_sublogics :: ExtModal -> [ExtModalSL] Source #

bottomSublogic :: ExtModal -> Maybe ExtModalSL Source #

sublogicDimensions :: ExtModal -> [[ExtModalSL]] Source #

parseSublogic :: ExtModal -> String -> Maybe ExtModalSL Source #

proj_sublogic_epsilon :: ExtModal -> ExtModalSL -> ExtModalSign -> ExtModalMorph Source #

provers :: ExtModal -> [Prover ExtModalSign ExtModalFORMULA ExtModalMorph ExtModalSL ()] Source #

default_prover :: ExtModal -> String Source #

cons_checkers :: ExtModal -> [ConsChecker ExtModalSign ExtModalFORMULA ExtModalSL ExtModalMorph ()] Source #

conservativityCheck :: ExtModal -> [ConservativityChecker ExtModalSign ExtModalFORMULA ExtModalMorph] Source #

empty_proof_tree :: ExtModal -> () Source #

syntaxTable :: ExtModal -> ExtModalSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: ExtModal -> Maybe OMCD Source #

export_symToOmdoc :: ExtModal -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: ExtModal -> NameMap Symbol -> ExtModalFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: ExtModal -> SigMap Symbol -> ExtModalSign -> [Named ExtModalFORMULA] -> Result [TCElement] Source #

omdocToSym :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: ExtModal -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ExtModalFORMULA)) Source #

addOMadtToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [[OmdADT]] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

addOmdocToTheory :: ExtModal -> SigMapI Symbol -> (ExtModalSign, [Named ExtModalFORMULA]) -> [TCElement] -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

sublogicOfTheo :: ExtModal -> (ExtModalSign, [ExtModalFORMULA]) -> ExtModalSL Source #

Logic ConstraintCASL CASL_Sublogics ConstraintCASLBasicSpec ConstraintCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ConstraintCASLSign ConstraintCASLMor Symbol RawSymbol () Source # 
Instance details

Defined in ConstraintCASL.Logic_ConstraintCASL

Methods

parse_basic_sen :: ConstraintCASL -> Maybe (ConstraintCASLBasicSpec -> AParser st ConstraintCASLFORMULA) Source #

stability :: ConstraintCASL -> Stability Source #

data_logic :: ConstraintCASL -> Maybe AnyLogic Source #

top_sublogic :: ConstraintCASL -> CASL_Sublogics Source #

all_sublogics :: ConstraintCASL -> [CASL_Sublogics] Source #

bottomSublogic :: ConstraintCASL -> Maybe CASL_Sublogics Source #

sublogicDimensions :: ConstraintCASL -> [[CASL_Sublogics]] Source #

parseSublogic :: ConstraintCASL -> String -> Maybe CASL_Sublogics Source #

proj_sublogic_epsilon :: ConstraintCASL -> CASL_Sublogics -> ConstraintCASLSign -> ConstraintCASLMor Source #

provers :: ConstraintCASL -> [Prover ConstraintCASLSign ConstraintCASLFORMULA ConstraintCASLMor CASL_Sublogics ()] Source #

default_prover :: ConstraintCASL -> String Source #

cons_checkers :: ConstraintCASL -> [ConsChecker ConstraintCASLSign ConstraintCASLFORMULA CASL_Sublogics ConstraintCASLMor ()] Source #

conservativityCheck :: ConstraintCASL -> [ConservativityChecker ConstraintCASLSign ConstraintCASLFORMULA ConstraintCASLMor] Source #

empty_proof_tree :: ConstraintCASL -> () Source #

syntaxTable :: ConstraintCASL -> ConstraintCASLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: ConstraintCASL -> Maybe OMCD Source #

export_symToOmdoc :: ConstraintCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: ConstraintCASL -> NameMap Symbol -> ConstraintCASLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: ConstraintCASL -> SigMap Symbol -> ConstraintCASLSign -> [Named ConstraintCASLFORMULA] -> Result [TCElement] Source #

omdocToSym :: ConstraintCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: ConstraintCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named ConstraintCASLFORMULA)) Source #

addOMadtToTheory :: ConstraintCASL -> SigMapI Symbol -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> [[OmdADT]] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #

addOmdocToTheory :: ConstraintCASL -> SigMapI Symbol -> (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) -> [TCElement] -> Result (ConstraintCASLSign, [Named ConstraintCASLFORMULA]) Source #

sublogicOfTheo :: ConstraintCASL -> (ConstraintCASLSign, [ConstraintCASLFORMULA]) -> CASL_Sublogics Source #

Logic CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

Methods

parse_basic_sen :: CoCASL -> Maybe (C_BASIC_SPEC -> AParser st CoCASLFORMULA) Source #

stability :: CoCASL -> Stability Source #

data_logic :: CoCASL -> Maybe AnyLogic Source #

top_sublogic :: CoCASL -> CoCASL_Sublogics Source #

all_sublogics :: CoCASL -> [CoCASL_Sublogics] Source #

bottomSublogic :: CoCASL -> Maybe CoCASL_Sublogics Source #

sublogicDimensions :: CoCASL -> [[CoCASL_Sublogics]] Source #

parseSublogic :: CoCASL -> String -> Maybe CoCASL_Sublogics Source #

proj_sublogic_epsilon :: CoCASL -> CoCASL_Sublogics -> CSign -> CoCASLMor Source #

provers :: CoCASL -> [Prover CSign CoCASLFORMULA CoCASLMor CoCASL_Sublogics ()] Source #

default_prover :: CoCASL -> String Source #

cons_checkers :: CoCASL -> [ConsChecker CSign CoCASLFORMULA CoCASL_Sublogics CoCASLMor ()] Source #

conservativityCheck :: CoCASL -> [ConservativityChecker CSign CoCASLFORMULA CoCASLMor] Source #

empty_proof_tree :: CoCASL -> () Source #

syntaxTable :: CoCASL -> CSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CoCASL -> Maybe OMCD Source #

export_symToOmdoc :: CoCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CoCASL -> NameMap Symbol -> CoCASLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: CoCASL -> SigMap Symbol -> CSign -> [Named CoCASLFORMULA] -> Result [TCElement] Source #

omdocToSym :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CoCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CoCASLFORMULA)) Source #

addOMadtToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [[OmdADT]] -> Result (CSign, [Named CoCASLFORMULA]) Source #

addOmdocToTheory :: CoCASL -> SigMapI Symbol -> (CSign, [Named CoCASLFORMULA]) -> [TCElement] -> Result (CSign, [Named CoCASLFORMULA]) Source #

sublogicOfTheo :: CoCASL -> (CSign, [CoCASLFORMULA]) -> CoCASL_Sublogics Source #

Logic COL () C_BASIC_SPEC COLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign COLMor Symbol RawSymbol () Source # 
Instance details

Defined in COL.Logic_COL

Methods

parse_basic_sen :: COL -> Maybe (C_BASIC_SPEC -> AParser st COLFORMULA) Source #

stability :: COL -> Stability Source #

data_logic :: COL -> Maybe AnyLogic Source #

top_sublogic :: COL -> () Source #

all_sublogics :: COL -> [()] Source #

bottomSublogic :: COL -> Maybe () Source #

sublogicDimensions :: COL -> [[()]] Source #

parseSublogic :: COL -> String -> Maybe () Source #

proj_sublogic_epsilon :: COL -> () -> CSign -> COLMor Source #

provers :: COL -> [Prover CSign COLFORMULA COLMor () ()] Source #

default_prover :: COL -> String Source #

cons_checkers :: COL -> [ConsChecker CSign COLFORMULA () COLMor ()] Source #

conservativityCheck :: COL -> [ConservativityChecker CSign COLFORMULA COLMor] Source #

empty_proof_tree :: COL -> () Source #

syntaxTable :: COL -> CSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: COL -> Maybe OMCD Source #

export_symToOmdoc :: COL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: COL -> NameMap Symbol -> COLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: COL -> SigMap Symbol -> CSign -> [Named COLFORMULA] -> Result [TCElement] Source #

omdocToSym :: COL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: COL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named COLFORMULA)) Source #

addOMadtToTheory :: COL -> SigMapI Symbol -> (CSign, [Named COLFORMULA]) -> [[OmdADT]] -> Result (CSign, [Named COLFORMULA]) Source #

addOmdocToTheory :: COL -> SigMapI Symbol -> (CSign, [Named COLFORMULA]) -> [TCElement] -> Result (CSign, [Named COLFORMULA]) Source #

sublogicOfTheo :: COL -> (CSign, [COLFORMULA]) -> () Source #

Logic CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

Methods

parse_basic_sen :: CASL_DL -> Maybe (DL_BASIC_SPEC -> AParser st DLFORMULA) Source #

stability :: CASL_DL -> Stability Source #

data_logic :: CASL_DL -> Maybe AnyLogic Source #

top_sublogic :: CASL_DL -> CASL_DL_SL Source #

all_sublogics :: CASL_DL -> [CASL_DL_SL] Source #

bottomSublogic :: CASL_DL -> Maybe CASL_DL_SL Source #

sublogicDimensions :: CASL_DL -> [[CASL_DL_SL]] Source #

parseSublogic :: CASL_DL -> String -> Maybe CASL_DL_SL Source #

proj_sublogic_epsilon :: CASL_DL -> CASL_DL_SL -> DLSign -> DLMor Source #

provers :: CASL_DL -> [Prover DLSign DLFORMULA DLMor CASL_DL_SL ProofTree] Source #

default_prover :: CASL_DL -> String Source #

cons_checkers :: CASL_DL -> [ConsChecker DLSign DLFORMULA CASL_DL_SL DLMor ProofTree] Source #

conservativityCheck :: CASL_DL -> [ConservativityChecker DLSign DLFORMULA DLMor] Source #

empty_proof_tree :: CASL_DL -> ProofTree Source #

syntaxTable :: CASL_DL -> DLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CASL_DL -> Maybe OMCD Source #

export_symToOmdoc :: CASL_DL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CASL_DL -> NameMap Symbol -> DLFORMULA -> Result TCorOMElement Source #

export_theoryToOmdoc :: CASL_DL -> SigMap Symbol -> DLSign -> [Named DLFORMULA] -> Result [TCElement] Source #

omdocToSym :: CASL_DL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CASL_DL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named DLFORMULA)) Source #

addOMadtToTheory :: CASL_DL -> SigMapI Symbol -> (DLSign, [Named DLFORMULA]) -> [[OmdADT]] -> Result (DLSign, [Named DLFORMULA]) Source #

addOmdocToTheory :: CASL_DL -> SigMapI Symbol -> (DLSign, [Named DLFORMULA]) -> [TCElement] -> Result (DLSign, [Named DLFORMULA]) Source #

sublogicOfTheo :: CASL_DL -> (DLSign, [DLFORMULA]) -> CASL_DL_SL Source #

Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Instance details

Defined in VSE.Logic_VSE

Methods

parse_basic_sen :: VSE -> Maybe (VSEBasicSpec -> AParser st Sentence) Source #

stability :: VSE -> Stability Source #

data_logic :: VSE -> Maybe AnyLogic Source #

top_sublogic :: VSE -> () Source #

all_sublogics :: VSE -> [()] Source #

bottomSublogic :: VSE -> Maybe () Source #

sublogicDimensions :: VSE -> [[()]] Source #

parseSublogic :: VSE -> String -> Maybe () Source #

proj_sublogic_epsilon :: VSE -> () -> VSESign -> VSEMor Source #

provers :: VSE -> [Prover VSESign Sentence VSEMor () ()] Source #

default_prover :: VSE -> String Source #

cons_checkers :: VSE -> [ConsChecker VSESign Sentence () VSEMor ()] Source #

conservativityCheck :: VSE -> [ConservativityChecker VSESign Sentence VSEMor] Source #

empty_proof_tree :: VSE -> () Source #

syntaxTable :: VSE -> VSESign -> Maybe SyntaxTable Source #

omdoc_metatheory :: VSE -> Maybe OMCD Source #

export_symToOmdoc :: VSE -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: VSE -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: VSE -> SigMap Symbol -> VSESign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: VSE -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: VSE -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [[OmdADT]] -> Result (VSESign, [Named Sentence]) Source #

addOmdocToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [TCElement] -> Result (VSESign, [Named Sentence]) Source #

sublogicOfTheo :: VSE -> (VSESign, [Sentence]) -> () Source #

Comorphism OWL22CASL OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in OWL2.OWL22CASL

Comorphism CASL2OWL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source # 
Instance details

Defined in OWL2.CASL2OWL

Comorphism ExtModal2OWL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree Source # 
Instance details

Defined in Comorphisms.ExtModal2OWL

Comorphism RelScheme2CASL RelScheme () RSScheme Sentence () () Sign RSMorphism RSSymbol RSRawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.RelScheme2CASL

Comorphism Prop2CASL Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.Prop2CASL

Comorphism Modal2CASL Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.Modal2CASL

Comorphism Maude2CASL Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.Maude2CASL

Comorphism ExtModal2CASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.ExtModal2CASL

Comorphism DFOL2CASL DFOL () BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.DFOL2CASL

Comorphism CL2CFOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CommonLogic2CASL

Comorphism CSMOF2CASL CSMOF () Metamodel Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CSMOF2CASL

Comorphism QVTR2CASL QVTR () Transformation Sen () () Sign Morphism () () () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.QVTR2CASL

Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Comorphisms.CFOL2IsabelleHOL

Comorphism CASL2TopSort CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2TopSort

Comorphism CASL2SubCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2SubCFOL

Comorphism ExtModal2ExtModalTotal ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.ExtModal2ExtModalTotal

Methods

sourceLogic :: ExtModal2ExtModalTotal -> ExtModal Source #

sourceSublogic :: ExtModal2ExtModalTotal -> ExtModalSL Source #

sourceSublogicLossy :: ExtModal2ExtModalTotal -> ExtModalSL Source #

minSourceTheory :: ExtModal2ExtModalTotal -> Maybe (LibName, String) Source #

targetLogic :: ExtModal2ExtModalTotal -> ExtModal Source #

mapSublogic :: ExtModal2ExtModalTotal -> ExtModalSL -> Maybe ExtModalSL Source #

map_theory :: ExtModal2ExtModalTotal -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

mapMarkedTheory :: ExtModal2ExtModalTotal -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

map_morphism :: ExtModal2ExtModalTotal -> ExtModalMorph -> Result ExtModalMorph Source #

map_sentence :: ExtModal2ExtModalTotal -> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA Source #

map_symbol :: ExtModal2ExtModalTotal -> ExtModalSign -> Symbol -> Set Symbol Source #

extractModel :: ExtModal2ExtModalTotal -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

is_model_transportable :: ExtModal2ExtModalTotal -> Bool Source #

has_model_expansion :: ExtModal2ExtModalTotal -> Bool Source #

is_weakly_amalgamable :: ExtModal2ExtModalTotal -> Bool Source #

constituents :: ExtModal2ExtModalTotal -> [String] Source #

isInclusionComorphism :: ExtModal2ExtModalTotal -> Bool Source #

rps :: ExtModal2ExtModalTotal -> Bool Source #

eps :: ExtModal2ExtModalTotal -> Bool Source #

isGTC :: ExtModal2ExtModalTotal -> Bool Source #

Comorphism CASL2Skolem CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2Skolem

Comorphism CASL2Prop CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2Prop

Comorphism CASL2Prenex CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2Prenex

Comorphism CASL2PCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2PCFOL

Comorphism CspCASL2Modal CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CspCASL2Modal

Comorphism ExtModal2ExtModalNoSubsorts ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.ExtModal2ExtModalNoSubsorts

Methods

sourceLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source #

sourceSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source #

sourceSublogicLossy :: ExtModal2ExtModalNoSubsorts -> ExtModalSL Source #

minSourceTheory :: ExtModal2ExtModalNoSubsorts -> Maybe (LibName, String) Source #

targetLogic :: ExtModal2ExtModalNoSubsorts -> ExtModal Source #

mapSublogic :: ExtModal2ExtModalNoSubsorts -> ExtModalSL -> Maybe ExtModalSL Source #

map_theory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

mapMarkedTheory :: ExtModal2ExtModalNoSubsorts -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

map_morphism :: ExtModal2ExtModalNoSubsorts -> ExtModalMorph -> Result ExtModalMorph Source #

map_sentence :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> ExtModalFORMULA -> Result ExtModalFORMULA Source #

map_symbol :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> Symbol -> Set Symbol Source #

extractModel :: ExtModal2ExtModalNoSubsorts -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source #

is_model_transportable :: ExtModal2ExtModalNoSubsorts -> Bool Source #

has_model_expansion :: ExtModal2ExtModalNoSubsorts -> Bool Source #

is_weakly_amalgamable :: ExtModal2ExtModalNoSubsorts -> Bool Source #

constituents :: ExtModal2ExtModalNoSubsorts -> [String] Source #

isInclusionComorphism :: ExtModal2ExtModalNoSubsorts -> Bool Source #

rps :: ExtModal2ExtModalNoSubsorts -> Bool Source #

eps :: ExtModal2ExtModalNoSubsorts -> Bool Source #

isGTC :: ExtModal2ExtModalNoSubsorts -> Bool Source #

Comorphism CASL2NNF CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL2NNF

Comorphism CASL2Modal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Modal () M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS MSign ModalMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2Modal

Comorphism CASL2Hybrid CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Hybrid () H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS HSign HybridMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2Hybrid

Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2HasCASL

Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.ExtModal2HasCASL

Comorphism CASL2ExtModal CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2ExtModal

Comorphism CASL2CspCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CspCASL () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2CspCASL

Comorphism Adl2CASL Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.Adl2CASL

Comorphism CoCFOL2IsabelleHOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Instance details

Defined in Comorphisms.CoCFOL2IsabelleHOL

Comorphism CoCASL2CoSubCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CoCASL2CoSubCFOL

Comorphism CoCASL2CoPCFOL CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CoCASL2CoPCFOL

Comorphism CASL2CoCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CoCASL CoCASL_Sublogics C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CSign CoCASLMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2CoCASL

Comorphism CASL_DL2CASL CASL_DL CASL_DL_SL DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS DLSign DLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Comorphisms.CASL_DL2CASL

Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2VSERefine

Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2VSEImport

Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Instance details

Defined in Comorphisms.CASL2VSE

Modification MODAL_EMBEDDING (InclComorphism CASL CASL_Sublogics) (CompComorphism CASL2Modal Modal2CASL) CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Instance details

Defined in Modifications.ModalEmbedding

Show a => Sentences (GenCspCASL a) CspCASLSen CspCASLSign CspCASLMorphism CspSymbol Source #

Instance of Sentences for CspCASL

Instance details

Defined in CspCASL.Logic_CspCASL

Show a => StaticAnalysis (GenCspCASL a) CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol Source #

Static Analysis for CspCASL

Instance details

Defined in CspCASL.Logic_CspCASL

Methods

basic_analysis :: GenCspCASL a -> Maybe ((CspBasicSpec, CspCASLSign, GlobalAnnos) -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen])) Source #

sen_analysis :: GenCspCASL a -> Maybe ((CspBasicSpec, CspCASLSign, CspCASLSen) -> Result CspCASLSen) Source #

extBasicAnalysis :: GenCspCASL a -> IRI -> LibName -> CspBasicSpec -> CspCASLSign -> GlobalAnnos -> Result (CspBasicSpec, ExtSign CspCASLSign CspSymbol, [Named CspCASLSen]) Source #

stat_symb_map_items :: GenCspCASL a -> CspCASLSign -> Maybe CspCASLSign -> [CspSymbMapItems] -> Result (EndoMap CspRawSymbol) Source #

stat_symb_items :: GenCspCASL a -> CspCASLSign -> [CspSymbItems] -> Result [CspRawSymbol] Source #

convertTheory :: GenCspCASL a -> Maybe ((CspCASLSign, [Named CspCASLSen]) -> CspBasicSpec) Source #

ensures_amalgamability :: GenCspCASL a -> ([CASLAmalgOpt], Gr CspCASLSign (Int, CspCASLMorphism), [(Int, CspCASLMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: GenCspCASL a -> CspCASLMorphism -> [Named CspCASLSen] -> Result (CspCASLSign, [Named CspCASLSen]) Source #

signature_colimit :: GenCspCASL a -> Gr CspCASLSign (Int, CspCASLMorphism) -> Result (CspCASLSign, Map Int CspCASLMorphism) Source #

qualify :: GenCspCASL a -> SIMPLE_ID -> LibName -> CspCASLMorphism -> CspCASLSign -> Result (CspCASLMorphism, [Named CspCASLSen]) Source #

symbol_to_raw :: GenCspCASL a -> CspSymbol -> CspRawSymbol Source #

id_to_raw :: GenCspCASL a -> Id -> CspRawSymbol Source #

matches :: GenCspCASL a -> CspSymbol -> CspRawSymbol -> Bool Source #

empty_signature :: GenCspCASL a -> CspCASLSign Source #

add_symb_to_sign :: GenCspCASL a -> CspCASLSign -> CspSymbol -> Result CspCASLSign Source #

signature_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

signatureDiff :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

intersection :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

final_union :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLSign Source #

morphism_union :: GenCspCASL a -> CspCASLMorphism -> CspCASLMorphism -> Result CspCASLMorphism Source #

is_subsig :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Bool Source #

subsig_inclusion :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> Result CspCASLMorphism Source #

generated_sign :: GenCspCASL a -> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism Source #

cogenerated_sign :: GenCspCASL a -> Set CspSymbol -> CspCASLSign -> Result CspCASLMorphism Source #

induced_from_morphism :: GenCspCASL a -> EndoMap CspRawSymbol -> CspCASLSign -> Result CspCASLMorphism Source #

induced_from_to_morphism :: GenCspCASL a -> EndoMap CspRawSymbol -> ExtSign CspCASLSign CspSymbol -> ExtSign CspCASLSign CspSymbol -> Result CspCASLMorphism Source #

is_transportable :: GenCspCASL a -> CspCASLMorphism -> Bool Source #

is_injective :: GenCspCASL a -> CspCASLMorphism -> Bool Source #

theory_to_taxonomy :: GenCspCASL a -> TaxoGraphKind -> MMiSSOntology -> CspCASLSign -> [Named CspCASLSen] -> Result MMiSSOntology Source #

corresp2th :: GenCspCASL a -> String -> Bool -> CspCASLSign -> CspCASLSign -> [CspSymbItems] -> [CspSymbItems] -> EndoMap CspSymbol -> EndoMap CspSymbol -> REL_REF -> Result (CspCASLSign, [Named CspCASLSen], CspCASLSign, CspCASLSign, EndoMap CspSymbol, EndoMap CspSymbol) Source #

equiv2cospan :: GenCspCASL a -> CspCASLSign -> CspCASLSign -> [CspSymbItems] -> [CspSymbItems] -> Result (CspCASLSign, CspCASLSign, CspCASLSign, EndoMap CspSymbol, EndoMap CspSymbol) Source #

extract_module :: GenCspCASL a -> [IRI] -> (CspCASLSign, [Named CspCASLSen]) -> Result (CspCASLSign, [Named CspCASLSen]) Source #

CspCASLSemantics a => Logic (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source #

Instance of Logic for CspCASL

Instance details

Defined in CspCASL.Logic_CspCASL

Methods

parse_basic_sen :: GenCspCASL a -> Maybe (CspBasicSpec -> AParser st CspCASLSen) Source #

stability :: GenCspCASL a -> Stability Source #

data_logic :: GenCspCASL a -> Maybe AnyLogic Source #

top_sublogic :: GenCspCASL a -> () Source #

all_sublogics :: GenCspCASL a -> [()] Source #

bottomSublogic :: GenCspCASL a -> Maybe () Source #

sublogicDimensions :: GenCspCASL a -> [[()]] Source #

parseSublogic :: GenCspCASL a -> String -> Maybe () Source #

proj_sublogic_epsilon :: GenCspCASL a -> () -> CspCASLSign -> CspCASLMorphism Source #

provers :: GenCspCASL a -> [Prover CspCASLSign CspCASLSen CspCASLMorphism () ()] Source #

default_prover :: GenCspCASL a -> String Source #

cons_checkers :: GenCspCASL a -> [ConsChecker CspCASLSign CspCASLSen () CspCASLMorphism ()] Source #

conservativityCheck :: GenCspCASL a -> [ConservativityChecker CspCASLSign CspCASLSen CspCASLMorphism] Source #

empty_proof_tree :: GenCspCASL a -> () Source #

syntaxTable :: GenCspCASL a -> CspCASLSign -> Maybe SyntaxTable Source #

omdoc_metatheory :: GenCspCASL a -> Maybe OMCD Source #

export_symToOmdoc :: GenCspCASL a -> NameMap CspSymbol -> CspSymbol -> String -> Result TCElement Source #

export_senToOmdoc :: GenCspCASL a -> NameMap CspSymbol -> CspCASLSen -> Result TCorOMElement Source #

export_theoryToOmdoc :: GenCspCASL a -> SigMap CspSymbol -> CspCASLSign -> [Named CspCASLSen] -> Result [TCElement] Source #

omdocToSym :: GenCspCASL a -> SigMapI CspSymbol -> TCElement -> String -> Result CspSymbol Source #

omdocToSen :: GenCspCASL a -> SigMapI CspSymbol -> TCElement -> String -> Result (Maybe (Named CspCASLSen)) Source #

addOMadtToTheory :: GenCspCASL a -> SigMapI CspSymbol -> (CspCASLSign, [Named CspCASLSen]) -> [[OmdADT]] -> Result (CspCASLSign, [Named CspCASLSen]) Source #

addOmdocToTheory :: GenCspCASL a -> SigMapI CspSymbol -> (CspCASLSign, [Named CspCASLSen]) -> [TCElement] -> Result (CspCASLSign, [Named CspCASLSen]) Source #

sublogicOfTheo :: GenCspCASL a -> (CspCASLSign, [CspCASLSen]) -> () Source #

MinSL a e => ProjectSublogic (CASL_SL a) (Sign f e) Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

projectSublogic :: CASL_SL a -> Sign f e -> Sign f e Source #

MinSL a e => MinSublogic (CASL_SL a) (Sign f e) Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

minSublogic :: Sign f e -> CASL_SL a Source #

Eq e => Eq (Sign f e) Source # 
Instance details

Defined in CASL.Sign

Methods

(==) :: Sign f e -> Sign f e -> Bool

(/=) :: Sign f e -> Sign f e -> Bool

(Data f, Data e) => Data (Sign f e) Source # 
Instance details

Defined in CASL.Sign

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sign f e -> c (Sign f e)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Sign f e)

toConstr :: Sign f e -> Constr

dataTypeOf :: Sign f e -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Sign f e))

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (Sign f e))

gmapT :: (forall b. Data b => b -> b) -> Sign f e -> Sign f e

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign f e -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign f e -> r

gmapQ :: (forall d. Data d => d -> u) -> Sign f e -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Sign f e -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sign f e -> m (Sign f e)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sign f e -> m (Sign f e)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sign f e -> m (Sign f e)

Ord e => Ord (Sign f e) Source # 
Instance details

Defined in CASL.Sign

Methods

compare :: Sign f e -> Sign f e -> Ordering

(<) :: Sign f e -> Sign f e -> Bool

(<=) :: Sign f e -> Sign f e -> Bool

(>) :: Sign f e -> Sign f e -> Bool

(>=) :: Sign f e -> Sign f e -> Bool

max :: Sign f e -> Sign f e -> Sign f e

min :: Sign f e -> Sign f e -> Sign f e

(Show f, Show e) => Show (Sign f e) Source # 
Instance details

Defined in CASL.Sign

Methods

showsPrec :: Int -> Sign f e -> ShowS

show :: Sign f e -> String

showList :: [Sign f e] -> ShowS

Generic (Sign f e) 
Instance details

Defined in CASL.ATC_CASL

Associated Types

type Rep (Sign f e) :: Type -> Type

Methods

from :: Sign f e -> Rep (Sign f e) x

to :: Rep (Sign f e) x -> Sign f e

(FromJSON f, FromJSON e) => FromJSON (Sign f e) 
Instance details

Defined in CASL.ATC_CASL

Methods

parseJSON :: Value -> Parser (Sign f e)

parseJSONList :: Value -> Parser [Sign f e]

(ToJSON f, ToJSON e) => ToJSON (Sign f e) 
Instance details

Defined in CASL.ATC_CASL

Methods

toJSON :: Sign f e -> Value

toEncoding :: Sign f e -> Encoding

toJSONList :: [Sign f e] -> Value

toEncodingList :: [Sign f e] -> Encoding

(ShATermConvertible f, ShATermConvertible e) => ShATermConvertible (Sign f e) 
Instance details

Defined in CASL.ATC_CASL

Methods

toShATermAux :: ATermTable -> Sign f e -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Sign f e] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Sign f e)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sign f e])

(Show f, Pretty e) => Pretty (Sign f e) Source # 
Instance details

Defined in CASL.Sign

Methods

pretty :: Sign f e -> Doc Source #

pretties :: [Sign f e] -> Doc Source #

(CspCASLSemantics a, CspCASLSemantics b) => Comorphism (CspCASL2CspCASL a b) (GenCspCASL a) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () (GenCspCASL b) () CspBasicSpec CspCASLSen CspSymbItems CspSymbMapItems CspCASLSign CspCASLMorphism CspSymbol CspRawSymbol () Source # 
Instance details

Defined in CspCASL.Comorphisms

(Ord f, Ord e, Ord m, MorphismExtension e m) => Category (Sign f e) (Morphism f e m) Source # 
Instance details

Defined in CASL.Logic_CASL

Methods

ide :: Sign f e -> Morphism f e m Source #

composeMorphisms :: Morphism f e m -> Morphism f e m -> Result (Morphism f e m) Source #

dom :: Morphism f e m -> Sign f e Source #

cod :: Morphism f e m -> Sign f e Source #

inverse :: Morphism f e m -> Result (Morphism f e m) Source #

isInclusion :: Morphism f e m -> Bool Source #

legal_mor :: Morphism f e m -> Result () Source #

type Rep (Sign f e) 
Instance details

Defined in CASL.ATC_CASL

type Rep (Sign f e) = D1 ('MetaData "Sign" "CASL.Sign" "main" 'False) (C1 ('MetaCons "Sign" 'PrefixI 'True) (((S1 ('MetaSel ('Just "sortRel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Rel SORT)) :*: (S1 ('MetaSel ('Just "revSortRel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Rel SORT))) :*: S1 ('MetaSel ('Just "emptySortSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set SORT)))) :*: (S1 ('MetaSel ('Just "opMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpMap) :*: (S1 ('MetaSel ('Just "assocOps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpMap) :*: S1 ('MetaSel ('Just "predMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PredMap)))) :*: ((S1 ('MetaSel ('Just "varMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map SIMPLE_ID SORT)) :*: (S1 ('MetaSel ('Just "sentences") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Named (FORMULA f)]) :*: S1 ('MetaSel ('Just "declaredSymbols") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Symbol)))) :*: ((S1 ('MetaSel ('Just "envDiags") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Diagnosis]) :*: S1 ('MetaSel ('Just "annoMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AnnoMap)) :*: (S1 ('MetaSel ('Just "globAnnos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GlobalAnnos) :*: S1 ('MetaSel ('Just "extendedInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 e))))))

sortSet :: Sign f e -> Set SORT Source #

emptySign :: e -> Sign f e Source #

embedSign :: e -> Sign f1 e1 -> Sign f e Source #

mapForm :: f -> FORMULA f1 -> FORMULA f Source #

embedTheory :: (FORMULA f1 -> FORMULA f) -> e -> (Sign f1 e1, [Named (FORMULA f1)]) -> (Sign f e, [Named (FORMULA f)]) Source #

embedCASLTheory :: e -> (Sign f1 e1, [Named (FORMULA f1)]) -> (Sign f e, [Named (FORMULA f)]) Source #

class SignExtension e where Source #

Methods

isSubSignExtension :: e -> e -> Bool Source #

Instances

Instances details
SignExtension () Source # 
Instance details

Defined in CASL.Sign

Methods

isSubSignExtension :: () -> () -> Bool Source #

SignExtension COLSign Source # 
Instance details

Defined in COL.Logic_COL

SignExtension CASL_DLSign Source # 
Instance details

Defined in CASL_DL.Logic_CASL_DL

SignExtension CoCASLSign Source # 
Instance details

Defined in CoCASL.Logic_CoCASL

SignExtension CspSign Source #

Instance for CspCASL signature extension

Instance details

Defined in CspCASL.Morphism

SignExtension EModalSign Source # 
Instance details

Defined in ExtModal.Logic_ExtModal

SignExtension SignExt Source # 
Instance details

Defined in Fpl.Logic_Fpl

SignExtension HybridSign Source # 
Instance details

Defined in Hybrid.Logic_Hybrid

SignExtension ModalSign Source # 
Instance details

Defined in Modal.Logic_Modal

SignExtension Procs Source # 
Instance details

Defined in VSE.Logic_VSE

Methods

isSubSignExtension :: Procs -> Procs -> Bool Source #

subsortsOf :: SORT -> Sign f e -> Set SORT Source #

proper subsorts (possibly excluding input sort)

supersortsOf :: SORT -> Sign f e -> Set SORT Source #

proper supersorts (possibly excluding input sort)

eqAndSubsorts :: Bool -> Rel SORT -> ([[SORT]], [(SORT, [SORT])]) Source #

printSign :: (e -> Doc) -> Sign f e -> Doc Source #

closeSortRel :: Sign f e -> Sign f e Source #

isTotal :: OpType -> Bool Source #

rmOrAddParts :: Bool -> Set OpType -> Set OpType Source #

remove (True) or add (False) partial op if it is included as total

diffSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e Source #

addSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e Source #

interRel :: (Show a, Ord a) => Rel a -> Rel a -> Rel a Source #

interSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e Source #

isSubOpMap :: OpMap -> OpMap -> Bool Source #

isSubSig :: (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool Source #

mapSetToList :: MapSet a b -> [(a, b)] Source #

addDiags :: [Diagnosis] -> State (Sign f e) () Source #

addAnnoSet :: Annoted a -> Symbol -> State (Sign f e) () Source #

addSort :: SortsKind -> Annoted a -> SORT -> State (Sign f e) () Source #

checkSorts :: [SORT] -> State (Sign f e) () Source #

addSubsort :: SORT -> SORT -> State (Sign f e) () Source #

addSubsortOrIso :: Bool -> SORT -> SORT -> State (Sign f e) () Source #

alsoWarning :: String -> String -> Id -> [Diagnosis] Source #

checkWithMap :: String -> String -> Map Id a -> Id -> [Diagnosis] Source #

checkWithOtherMap :: String -> String -> MapSet Id a -> Id -> [Diagnosis] Source #

addVar :: SORT -> SIMPLE_ID -> State (Sign f e) () Source #

type VarSet = Set (VAR, SORT) Source #

class TermExtension f where Source #

extract the sort and free variables from an analysed term. The input signature for free variables is (currently only) used for statements in the VSE logic. The conversion for boolean terms to formulas is only used for FPL.

Minimal complete definition

Nothing

Instances

Instances details
TermExtension () Source # 
Instance details

Defined in CASL.Sign

Methods

freeVarsOfExt :: Sign () e -> () -> VarSet Source #

optTermSort :: () -> Maybe SORT Source #

sortOfTerm :: () -> SORT Source #

termToFormula :: TERM () -> Result (FORMULA ()) Source #

TermExtension C_FORMULA Source # 
Instance details

Defined in CoCASL.StatAna

TermExtension DL_FORMULA Source # 
Instance details

Defined in CASL_DL.StatAna

TermExtension ConstraintFORMULA Source # 
Instance details

Defined in ConstraintCASL.StaticAna

TermExtension CspSen Source # 
Instance details

Defined in CspCASL.SignCSP

TermExtension EM_FORMULA Source # 
Instance details

Defined in ExtModal.StatAna

TermExtension TermExt Source # 
Instance details

Defined in Fpl.StatAna

TermExtension H_FORMULA Source # 
Instance details

Defined in Hybrid.StatAna

TermExtension M_FORMULA Source # 
Instance details

Defined in Modal.StatAna

TermExtension Dlformula Source # 
Instance details

Defined in VSE.Ana

TermExtension f => TermExtension (TERM f) Source # 
Instance details

Defined in CASL.Sign

optSortOfTerm :: (f -> Maybe SORT) -> TERM f -> Maybe SORT Source #

mkAxName :: String -> SORT -> SORT -> String Source #

mkAxNameSingle :: String -> SORT -> String Source #

mkSortGenName :: [SORT] -> String Source #

toSortGenNamed :: FORMULA f -> [SORT] -> Named (FORMULA f) Source #

The sort generation constraint is given a generated name, built from the sort list

addSymbToSign :: Sign e f -> Symbol -> Result (Sign e f) Source #

adds a symbol to a given signature