{-# 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