914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./Comorphisms/ExtModal2ExtModalNoSubsorts.hs
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
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maederimport CASL.Sublogic
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
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder Symbol RawSymbol ()
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder Symbol RawSymbol () where
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder sourceLogic ExtModal2ExtModalNoSubsorts = ExtModal
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder sourceSublogic ExtModal2ExtModalNoSubsorts = mkTop maxSublogic
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder targetLogic ExtModal2ExtModalNoSubsorts = ExtModal
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder mapSublogic ExtModal2ExtModalNoSubsorts sl = Just
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder $ if has_sub sl then -- subsorting is coded out
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder sl { sub_features = NoSub
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder , has_part = True
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder , which_logic = max Horn $ which_logic sl
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder , has_eq = True}
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder else sl
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