content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./Comorphisms/CoCASL2CoPCFOL.hs
  Description :  Extension of CASL2PCFOL to CoCASL
  Copyright   :  (c) Till Mossakowski, Uni Bremen 2002-2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  till@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  portable
  
  Coding out subsorting, lifted tot eh level of CoCASL
  -}
  
  module Comorphisms.CoCASL2CoPCFOL where
  
  import Logic.Logic
  import Logic.Comorphism
  import qualified Data.Set as Set
  import Common.AS_Annotation
  
  -- CoCASL
  import CoCASL.Logic_CoCASL
  import CoCASL.AS_CoCASL
  import CoCASL.StatAna
  import CoCASL.Sublogic
  import CASL.Sublogic as SL
  import CASL.AS_Basic_CASL
  import CASL.Sign
  import CASL.Morphism
  import CASL.Inject
  import CASL.Project
  import CASL.Monoton
  import Comorphisms.CASL2PCFOL
  
  -- | The identity of the comorphism
  data CoCASL2CoPCFOL = CoCASL2CoPCFOL deriving Show
  
  instance Language CoCASL2CoPCFOL -- default definition is okay
  
  instance Comorphism CoCASL2CoPCFOL
                 CoCASL CoCASL_Sublogics
                 C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
                 CSign
                 CoCASLMor
                 Symbol RawSymbol ()
                 CoCASL CoCASL_Sublogics
                 C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
                 CSign
                 CoCASLMor
                 Symbol RawSymbol () where
      sourceLogic CoCASL2CoPCFOL = CoCASL
      sourceSublogic CoCASL2CoPCFOL = SL.caslTop
      targetLogic CoCASL2CoPCFOL = CoCASL
      mapSublogic CoCASL2CoPCFOL sl = Just $
            sublogics_max need_horn sl
              { sub_features = NoSub  -- subsorting is coded out
              , has_part = True
              , has_eq = True
              }
      map_theory CoCASL2CoPCFOL = mkTheoryMapping ( \ sig ->
        let e = encodeSig sig in return
        (e, map (mapNamed $ injFormula injC_Formula) (monotonicities sig)
            ++ map (mapNamed mapFORMULA) (generateAxioms sig)))
        (map_sentence CoCASL2CoPCFOL)
      map_morphism CoCASL2CoPCFOL mor = return
        (mor { msource = encodeSig $ msource mor
             , mtarget = encodeSig $ mtarget mor })
        -- other components need not to be adapted!
      map_sentence CoCASL2CoPCFOL _ = return . cf2CFormula
      map_symbol CoCASL2CoPCFOL _ = Set.singleton . id
      has_model_expansion CoCASL2CoPCFOL = True
      is_weakly_amalgamable CoCASL2CoPCFOL = True
  
  cf2CFormula :: FORMULA C_FORMULA -> FORMULA C_FORMULA
  cf2CFormula = projFormula Partial projC_Formula . injFormula injC_Formula
  
  projC_Formula :: C_FORMULA -> C_FORMULA
  projC_Formula = foldC_Formula (projRecord Partial projC_Formula) mapCoRecord
  
  injC_Formula :: C_FORMULA -> C_FORMULA
  injC_Formula = foldC_Formula (injRecord injC_Formula) mapCoRecord
  