content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./Comorphisms/ExtModal2ExtModalNoSubsorts.hs
  Description :  coding out subsorting
  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)
  
  Coding out subsorting (SubPCFOL= -> PCFOL=),
     following Chap. III:3.1 of the CASL Reference Manual
  -}
  
  module Comorphisms.ExtModal2ExtModalNoSubsorts where
  
  import Logic.Logic
  import Logic.Comorphism
  
  import qualified Data.Set as Set
  
  import Common.AS_Annotation
  
  -- CASL
  import CASL.AS_Basic_CASL
  import CASL.Sign
  import CASL.Morphism
  import CASL.Inject
  import CASL.Project
  import CASL.Monoton
  import CASL.Sublogic
  
  import ExtModal.Logic_ExtModal
  import ExtModal.AS_ExtModal
  import ExtModal.StatAna
  import ExtModal.Sublogic as EM
  
  import Comorphisms.CASL2PCFOL
  
  -- | The identity of the comorphism
  data ExtModal2ExtModalNoSubsorts = ExtModal2ExtModalNoSubsorts deriving Show
  
  instance Language ExtModal2ExtModalNoSubsorts -- default definition is okay
  
  instance Comorphism ExtModal2ExtModalNoSubsorts
                 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 () where
      sourceLogic ExtModal2ExtModalNoSubsorts = ExtModal
      sourceSublogic ExtModal2ExtModalNoSubsorts = mkTop maxSublogic
      targetLogic ExtModal2ExtModalNoSubsorts = ExtModal
      mapSublogic ExtModal2ExtModalNoSubsorts sl = Just
        $ if has_sub sl then -- subsorting is coded out
              sl { sub_features = NoSub
                 , has_part = True
                 , which_logic = max Horn $ which_logic sl
                 , has_eq = True}
          else sl
      map_theory ExtModal2ExtModalNoSubsorts = mkTheoryMapping (\ sig ->
        let e = encodeSig sig in
        return (e, map (mapNamed injEMFormula) (monotonicities sig)
                   ++ generateAxioms sig))
        (map_sentence ExtModal2ExtModalNoSubsorts)
      map_morphism ExtModal2ExtModalNoSubsorts mor = return
        (mor { msource = encodeSig $ msource mor,
                mtarget = encodeSig $ mtarget mor })
      map_sentence ExtModal2ExtModalNoSubsorts _ =
        return . projEMFormula . injEMFormula
      map_symbol ExtModal2ExtModalNoSubsorts _ = Set.singleton . id
      has_model_expansion ExtModal2ExtModalNoSubsorts = True
      is_weakly_amalgamable ExtModal2ExtModalNoSubsorts = True
  
  projEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
  projEMFormula = projFormula Partial projEM
  
  projEM :: EM_FORMULA -> EM_FORMULA
  projEM = mapExtForm projEMFormula
  
  injEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
  injEMFormula = injFormula injEM
  
  injEM :: EM_FORMULA -> EM_FORMULA
  injEM = mapExtForm injEMFormula
  