ExtModal2ExtModalNoSubsorts.hs revision 914b90f3d6644fd464c5b26712b65d515a58c037
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder{- |
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederModule : $Header$
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederDescription : coding out subsorting
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederCopyright : (c) C. Maeder DFKI GmbH 2012
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederMaintainer : Christian.Maeder@dfki.de
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederStability : provisional
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederPortability : non-portable (imports Logic.Logic)
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederCoding out subsorting (SubPCFOL= -> PCFOL=),
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder following Chap. III:3.1 of the CASL Reference Manual
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder-}
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maedermodule Comorphisms.ExtModal2ExtModalNoSubsorts where
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport Logic.Logic
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport Logic.Comorphism
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport qualified Data.Set as Set
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport Common.AS_Annotation
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder-- CASL
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport CASL.AS_Basic_CASL
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport CASL.Sign
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport CASL.Morphism
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport CASL.Inject
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport CASL.Project
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport CASL.Monoton
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport ExtModal.Logic_ExtModal
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport ExtModal.AS_ExtModal
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport ExtModal.StatAna
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport ExtModal.Sublogic as EM
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport Comorphisms.CASL2PCFOL
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder-- | The identity of the comorphism
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederdata ExtModal2ExtModalNoSubsorts = ExtModal2ExtModalNoSubsorts deriving Show
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederinstance Language ExtModal2ExtModalNoSubsorts -- default definition is okay
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederinstance Comorphism ExtModal2ExtModalNoSubsorts
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder ExtModal Sublogic EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder Symbol RawSymbol ()
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder ExtModal Sublogic EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder Symbol RawSymbol () where
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder sourceLogic ExtModal2ExtModalNoSubsorts = ExtModal
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder sourceSublogic ExtModal2ExtModalNoSubsorts = maxSublogic
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder targetLogic ExtModal2ExtModalNoSubsorts = ExtModal
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder mapSublogic ExtModal2ExtModalNoSubsorts = Just
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder map_theory ExtModal2ExtModalNoSubsorts = mkTheoryMapping (\ sig ->
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder let e = encodeSig sig in
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder return (e, map (mapNamed injEMFormula) (monotonicities sig)
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder ++ generateAxioms sig))
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder (map_sentence ExtModal2ExtModalNoSubsorts)
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder map_morphism ExtModal2ExtModalNoSubsorts mor = return
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder (mor { msource = encodeSig $ msource mor,
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder mtarget = encodeSig $ mtarget mor })
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder map_sentence ExtModal2ExtModalNoSubsorts _ =
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder return . projEMFormula . injEMFormula
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder map_symbol ExtModal2ExtModalNoSubsorts _ = Set.singleton . id
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder has_model_expansion ExtModal2ExtModalNoSubsorts = True
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder is_weakly_amalgamable ExtModal2ExtModalNoSubsorts = True
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederprojEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederprojEMFormula = projFormula Partial projEM
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederprojEM :: EM_FORMULA -> EM_FORMULA
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederprojEM = mapExtForm projEMFormula
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederinjEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederinjEMFormula = injFormula injEM
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederinjEM :: EM_FORMULA -> EM_FORMULA
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederinjEM = mapExtForm injEMFormula