Copyright	(c) C. Maeder DFKI GmbH 2012
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	non-portable (imports Logic.Logic)
Safe Haskell	None

Comorphisms.ExtModal2ExtModalTotal

Description

Coding out subsorting (SubPCFOL= -> PCFOL=), following Chap. III:3.1 of the CASL Reference Manual

Synopsis

data ExtModal2ExtModalTotal = ExtModal2ExtModalTotal
emEncodeSig :: Set SORT -> Sign f EModalSign -> Sign f EModalSign
emsortsWithBottom :: Sign f e -> Set SORT
simplifyEM :: EM_FORMULA -> EM_FORMULA
simplifyEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
noCondsEM :: EM_FORMULA -> EM_FORMULA
noCondsEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
codeEM :: Set SORT -> EM_FORMULA -> EM_FORMULA
codeEMFormula :: Set SORT -> FORMULA EM_FORMULA -> FORMULA EM_FORMULA

Documentation

data ExtModal2ExtModalTotal Source #

The identity of the comorphism

Constructors

ExtModal2ExtModalTotal

Instances

Instances details

Show ExtModal2ExtModalTotal Source #
Instance details Defined in Comorphisms.ExtModal2ExtModalTotal Methods showsPrec :: Int -> ExtModal2ExtModalTotal -> ShowS show :: ExtModal2ExtModalTotal -> String showList :: [ExtModal2ExtModalTotal] -> ShowS
Language ExtModal2ExtModalTotal Source #
Instance details Defined in Comorphisms.ExtModal2ExtModalTotal Methods language_name :: ExtModal2ExtModalTotal -> String Source # description :: ExtModal2ExtModalTotal -> String Source #
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 #

emEncodeSig :: Set SORT -> Sign f EModalSign -> Sign f EModalSign Source #

emsortsWithBottom :: Sign f e -> Set SORT Source #

simplifyEM :: EM_FORMULA -> EM_FORMULA Source #

simplifyEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA Source #

noCondsEM :: EM_FORMULA -> EM_FORMULA Source #

noCondsEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA Source #

codeEM :: Set SORT -> EM_FORMULA -> EM_FORMULA Source #

codeEMFormula :: Set SORT -> FORMULA EM_FORMULA -> FORMULA EM_FORMULA Source #