Copyright	(c) Eugen Kuksa Uni Bremen 2011
License	GPLv2 or higher, see LICENSE.txt
Maintainer	eugenk@informatik.uni-bremen.de
Stability	experimental (not complete: typleclass-instances missing)
Portability	non-portable (via Logic.Logic)
Safe Haskell	None

Comorphisms.CommonLogicModuleElimination

Description

Translating comorphism from CommonLogic to CommonLogic in order to eliminate modules.

Documentation

data CommonLogicModuleElimination Source #

Constructors

CommonLogicModuleElimination

Instances

Instances details

Show CommonLogicModuleElimination Source #
Instance details Defined in Comorphisms.CommonLogicModuleElimination Methods showsPrec :: Int -> CommonLogicModuleElimination -> ShowS show :: CommonLogicModuleElimination -> String showList :: [CommonLogicModuleElimination] -> ShowS
Language CommonLogicModuleElimination Source #
Instance details Defined in Comorphisms.CommonLogicModuleElimination Methods language_name :: CommonLogicModuleElimination -> String Source # description :: CommonLogicModuleElimination -> String Source #
Comorphism CommonLogicModuleElimination CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.CommonLogicModuleElimination Methods sourceLogic :: CommonLogicModuleElimination -> CommonLogic Source # sourceSublogic :: CommonLogicModuleElimination -> CommonLogicSL Source # sourceSublogicLossy :: CommonLogicModuleElimination -> CommonLogicSL Source # minSourceTheory :: CommonLogicModuleElimination -> Maybe (LibName, String) Source # targetLogic :: CommonLogicModuleElimination -> CommonLogic Source # mapSublogic :: CommonLogicModuleElimination -> CommonLogicSL -> Maybe CommonLogicSL Source # map_theory :: CommonLogicModuleElimination -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source # mapMarkedTheory :: CommonLogicModuleElimination -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source # map_morphism :: CommonLogicModuleElimination -> Morphism -> Result Morphism Source # map_sentence :: CommonLogicModuleElimination -> Sign -> TEXT_META -> Result TEXT_META Source # map_symbol :: CommonLogicModuleElimination -> Sign -> Symbol -> Set Symbol Source # extractModel :: CommonLogicModuleElimination -> Sign -> ProofTree -> Result (Sign, [Named TEXT_META]) Source # is_model_transportable :: CommonLogicModuleElimination -> Bool Source # has_model_expansion :: CommonLogicModuleElimination -> Bool Source # is_weakly_amalgamable :: CommonLogicModuleElimination -> Bool Source # constituents :: CommonLogicModuleElimination -> [String] Source # isInclusionComorphism :: CommonLogicModuleElimination -> Bool Source # rps :: CommonLogicModuleElimination -> Bool Source # eps :: CommonLogicModuleElimination -> Bool Source # isGTC :: CommonLogicModuleElimination -> Bool Source #