Hets - the Heterogeneous Tool Set
Copyright(c) T.Mossakowski W.Herding C.Maeder Uni Bremen 2004-2006
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityprovisional
Portabilityportable
Safe HaskellSafe

Modal.AS_Modal

Description

Abstract syntax for modal logic extension of CASL Only the added syntax is specified

Documentation

data M_BASIC_ITEM Source #

Instances

Instances details
Data M_BASIC_ITEM Source # 
Instance details

Defined in Modal.AS_Modal

Methods

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

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

toConstr :: M_BASIC_ITEM -> Constr

dataTypeOf :: M_BASIC_ITEM -> DataType

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

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

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

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

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

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

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

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

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

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

Show M_BASIC_ITEM Source # 
Instance details

Defined in Modal.AS_Modal

Methods

showsPrec :: Int -> M_BASIC_ITEM -> ShowS

show :: M_BASIC_ITEM -> String

showList :: [M_BASIC_ITEM] -> ShowS

Generic M_BASIC_ITEM 
Instance details

Defined in Modal.ATC_Modal

Associated Types

type Rep M_BASIC_ITEM :: Type -> Type

GetRange M_BASIC_ITEM Source # 
Instance details

Defined in Modal.AS_Modal

FromJSON M_BASIC_ITEM 
Instance details

Defined in Modal.ATC_Modal

Methods

parseJSON :: Value -> Parser M_BASIC_ITEM

parseJSONList :: Value -> Parser [M_BASIC_ITEM]

ToJSON M_BASIC_ITEM 
Instance details

Defined in Modal.ATC_Modal

Methods

toJSON :: M_BASIC_ITEM -> Value

toEncoding :: M_BASIC_ITEM -> Encoding

toJSONList :: [M_BASIC_ITEM] -> Value

toEncodingList :: [M_BASIC_ITEM] -> Encoding

ShATermConvertible M_BASIC_ITEM 
Instance details

Defined in Modal.ATC_Modal

Methods

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

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

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

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

Pretty M_BASIC_ITEM Source # 
Instance details

Defined in Modal.Print_AS

AParsable M_BASIC_ITEM Source # 
Instance details

Defined in Modal.Parse_AS

Syntax Modal M_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in Modal.Logic_Modal

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 #

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 #

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

type Rep M_BASIC_ITEM 
Instance details

Defined in Modal.ATC_Modal

type Rep M_BASIC_ITEM = D1 ('MetaData "M_BASIC_ITEM" "Modal.AS_Modal" "main" 'False) (C1 ('MetaCons "Simple_mod_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted SIMPLE_ID]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AnModFORM]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Term_mod_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted SORT]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AnModFORM]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data RIGOR Source #

Constructors

Rigid 
Flexible 

Instances

Instances details
Data RIGOR Source # 
Instance details

Defined in Modal.AS_Modal

Methods

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

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

toConstr :: RIGOR -> Constr

dataTypeOf :: RIGOR -> DataType

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

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

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

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

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

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

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

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

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

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

Show RIGOR Source # 
Instance details

Defined in Modal.AS_Modal

Methods

showsPrec :: Int -> RIGOR -> ShowS

show :: RIGOR -> String

showList :: [RIGOR] -> ShowS

Generic RIGOR 
Instance details

Defined in Modal.ATC_Modal

Associated Types

type Rep RIGOR :: Type -> Type

Methods

from :: RIGOR -> Rep RIGOR x

to :: Rep RIGOR x -> RIGOR

GetRange RIGOR Source # 
Instance details

Defined in Modal.AS_Modal

FromJSON RIGOR 
Instance details

Defined in Modal.ATC_Modal

Methods

parseJSON :: Value -> Parser RIGOR

parseJSONList :: Value -> Parser [RIGOR]

ToJSON RIGOR 
Instance details

Defined in Modal.ATC_Modal

Methods

toJSON :: RIGOR -> Value

toEncoding :: RIGOR -> Encoding

toJSONList :: [RIGOR] -> Value

toEncodingList :: [RIGOR] -> Encoding

ShATermConvertible RIGOR 
Instance details

Defined in Modal.ATC_Modal

Methods

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

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

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

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

Pretty RIGOR Source # 
Instance details

Defined in Modal.Print_AS

type Rep RIGOR 
Instance details

Defined in Modal.ATC_Modal

type Rep RIGOR = D1 ('MetaData "RIGOR" "Modal.AS_Modal" "main" 'False) (C1 ('MetaCons "Rigid" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Flexible" 'PrefixI 'False) (U1 :: Type -> Type))

data M_SIG_ITEM Source #

Instances

Instances details
Data M_SIG_ITEM Source # 
Instance details

Defined in Modal.AS_Modal

Methods

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

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

toConstr :: M_SIG_ITEM -> Constr

dataTypeOf :: M_SIG_ITEM -> DataType

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

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

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

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

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

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

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

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

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

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

Show M_SIG_ITEM Source # 
Instance details

Defined in Modal.AS_Modal

Methods

showsPrec :: Int -> M_SIG_ITEM -> ShowS

show :: M_SIG_ITEM -> String

showList :: [M_SIG_ITEM] -> ShowS

Generic M_SIG_ITEM 
Instance details

Defined in Modal.ATC_Modal

Associated Types

type Rep M_SIG_ITEM :: Type -> Type

Methods

from :: M_SIG_ITEM -> Rep M_SIG_ITEM x

to :: Rep M_SIG_ITEM x -> M_SIG_ITEM

GetRange M_SIG_ITEM Source # 
Instance details

Defined in Modal.AS_Modal

FromJSON M_SIG_ITEM 
Instance details

Defined in Modal.ATC_Modal

Methods

parseJSON :: Value -> Parser M_SIG_ITEM

parseJSONList :: Value -> Parser [M_SIG_ITEM]

ToJSON M_SIG_ITEM 
Instance details

Defined in Modal.ATC_Modal

Methods

toJSON :: M_SIG_ITEM -> Value

toEncoding :: M_SIG_ITEM -> Encoding

toJSONList :: [M_SIG_ITEM] -> Value

toEncodingList :: [M_SIG_ITEM] -> Encoding

ShATermConvertible M_SIG_ITEM 
Instance details

Defined in Modal.ATC_Modal

Methods

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

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

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

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

Pretty M_SIG_ITEM Source # 
Instance details

Defined in Modal.Print_AS

AParsable M_SIG_ITEM Source # 
Instance details

Defined in Modal.Parse_AS

Syntax Modal M_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in Modal.Logic_Modal

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 #

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 #

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

type Rep M_SIG_ITEM 
Instance details

Defined in Modal.ATC_Modal

type Rep M_SIG_ITEM = D1 ('MetaData "M_SIG_ITEM" "Modal.AS_Modal" "main" 'False) (C1 ('MetaCons "Rigid_op_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RIGOR) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (OP_ITEM M_FORMULA)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: C1 ('MetaCons "Rigid_pred_items" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RIGOR) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted (PRED_ITEM M_FORMULA)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data MODALITY Source #

Instances

Instances details
Eq MODALITY Source # 
Instance details

Defined in Modal.AS_Modal

Methods

(==) :: MODALITY -> MODALITY -> Bool

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

Data MODALITY Source # 
Instance details

Defined in Modal.AS_Modal

Methods

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

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

toConstr :: MODALITY -> Constr

dataTypeOf :: MODALITY -> DataType

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

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

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

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

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

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

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

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

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

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

Ord MODALITY Source # 
Instance details

Defined in Modal.AS_Modal

Methods

compare :: MODALITY -> MODALITY -> Ordering

(<) :: MODALITY -> MODALITY -> Bool

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

(>) :: MODALITY -> MODALITY -> Bool

(>=) :: MODALITY -> MODALITY -> Bool

max :: MODALITY -> MODALITY -> MODALITY

min :: MODALITY -> MODALITY -> MODALITY

Show MODALITY Source # 
Instance details

Defined in Modal.AS_Modal

Methods

showsPrec :: Int -> MODALITY -> ShowS

show :: MODALITY -> String

showList :: [MODALITY] -> ShowS

Generic MODALITY 
Instance details

Defined in Modal.ATC_Modal

Associated Types

type Rep MODALITY :: Type -> Type

Methods

from :: MODALITY -> Rep MODALITY x

to :: Rep MODALITY x -> MODALITY

GetRange MODALITY Source # 
Instance details

Defined in Modal.AS_Modal

FromJSON MODALITY 
Instance details

Defined in Modal.ATC_Modal

Methods

parseJSON :: Value -> Parser MODALITY

parseJSONList :: Value -> Parser [MODALITY]

ToJSON MODALITY 
Instance details

Defined in Modal.ATC_Modal

Methods

toJSON :: MODALITY -> Value

toEncoding :: MODALITY -> Encoding

toJSONList :: [MODALITY] -> Value

toEncodingList :: [MODALITY] -> Encoding

ShATermConvertible MODALITY 
Instance details

Defined in Modal.ATC_Modal

Methods

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

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

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

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

Pretty MODALITY Source # 
Instance details

Defined in Modal.Print_AS

type Rep MODALITY 
Instance details

Defined in Modal.ATC_Modal

type Rep MODALITY = D1 ('MetaData "MODALITY" "Modal.AS_Modal" "main" 'False) (C1 ('MetaCons "Simple_mod" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SIMPLE_ID)) :+: C1 ('MetaCons "Term_mod" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TERM M_FORMULA))))

data M_FORMULA Source #

Instances

Instances details
Eq M_FORMULA Source # 
Instance details

Defined in Modal.AS_Modal

Methods

(==) :: M_FORMULA -> M_FORMULA -> Bool

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

Data M_FORMULA Source # 
Instance details

Defined in Modal.AS_Modal

Methods

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

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

toConstr :: M_FORMULA -> Constr

dataTypeOf :: M_FORMULA -> DataType

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

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

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

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

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

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

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

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

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

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

Ord M_FORMULA Source # 
Instance details

Defined in Modal.AS_Modal

Methods

compare :: M_FORMULA -> M_FORMULA -> Ordering

(<) :: M_FORMULA -> M_FORMULA -> Bool

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

(>) :: M_FORMULA -> M_FORMULA -> Bool

(>=) :: M_FORMULA -> M_FORMULA -> Bool

max :: M_FORMULA -> M_FORMULA -> M_FORMULA

min :: M_FORMULA -> M_FORMULA -> M_FORMULA

Show M_FORMULA Source # 
Instance details

Defined in Modal.AS_Modal

Methods

showsPrec :: Int -> M_FORMULA -> ShowS

show :: M_FORMULA -> String

showList :: [M_FORMULA] -> ShowS

Generic M_FORMULA 
Instance details

Defined in Modal.ATC_Modal

Associated Types

type Rep M_FORMULA :: Type -> Type

Methods

from :: M_FORMULA -> Rep M_FORMULA x

to :: Rep M_FORMULA x -> M_FORMULA

GetRange M_FORMULA Source # 
Instance details

Defined in Modal.AS_Modal

FromJSON M_FORMULA 
Instance details

Defined in Modal.ATC_Modal

Methods

parseJSON :: Value -> Parser M_FORMULA

parseJSONList :: Value -> Parser [M_FORMULA]

ToJSON M_FORMULA 
Instance details

Defined in Modal.ATC_Modal

Methods

toJSON :: M_FORMULA -> Value

toEncoding :: M_FORMULA -> Encoding

toJSONList :: [M_FORMULA] -> Value

toEncodingList :: [M_FORMULA] -> Encoding

ShATermConvertible M_FORMULA 
Instance details

Defined in Modal.ATC_Modal

Methods

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

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

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

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

Pretty M_FORMULA Source # 
Instance details

Defined in Modal.Print_AS

FormExtension M_FORMULA Source # 
Instance details

Defined in Modal.Print_AS

TermExtension M_FORMULA Source # 
Instance details

Defined in Modal.StatAna

TermParser M_FORMULA Source # 
Instance details

Defined in Modal.Parse_AS

Methods

termParser :: Bool -> AParser st M_FORMULA Source #

Sentences Modal ModalFORMULA MSign ModalMor Symbol Source # 
Instance details

Defined in Modal.Logic_Modal

Syntax Modal M_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in Modal.Logic_Modal

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 #

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 #

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

type Rep M_FORMULA 
Instance details

Defined in Modal.ATC_Modal

type Rep M_FORMULA = D1 ('MetaData "M_FORMULA" "Modal.AS_Modal" "main" 'False) (C1 ('MetaCons "BoxOrDiamond" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MODALITY)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FORMULA M_FORMULA)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))