content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./Comorphisms/CoCASL2CoSubCFOL.hs
  Description :  Extension of CASL2SubCFOL to CoCASL
  Copyright   :  (c) Till Mossakowski, C.Maeder, Uni Bremen 2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable (imports Logic.Comorphism)
  
  coding out partiality, lifted to the level of CoCASL
  -}
  
  module Comorphisms.CoCASL2CoSubCFOL where
  
  import Logic.Logic
  import Logic.Comorphism
  
  -- 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.Fold
  import CASL.Simplify
  import Comorphisms.CASL2SubCFOL
  
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  import Common.AS_Annotation
  import Common.ProofUtils
  
  -- | The identity of the comorphism
  data CoCASL2CoSubCFOL = CoCASL2CoSubCFOL deriving (Show)
  
  instance Language CoCASL2CoSubCFOL -- default definition is okay
  
  instance Comorphism CoCASL2CoSubCFOL
                 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 CoCASL2CoSubCFOL = CoCASL
      sourceSublogic CoCASL2CoSubCFOL = SL.caslTop
      targetLogic CoCASL2CoSubCFOL = CoCASL
      mapSublogic CoCASL2CoSubCFOL sl = Just $
         if has_part sl then sl
          { has_part = False -- partiality is coded out
          , has_pred = True
          , which_logic = max Horn $ which_logic sl
          , has_eq = True} else sl
      map_theory CoCASL2CoSubCFOL (sig, sens) =
          let bsrts = sortsWithBottom (formulaTreatment defaultCASL2SubCFOL)
                sig $ Set.unions $ map (botCoFormulaSorts . sentence) sens
              e = encodeSig bsrts sig
              sens1 = map (mapNamed mapFORMULA) $ generateAxioms
                      (uniqueBottom defaultCASL2SubCFOL) bsrts sig
              sens2 = map (mapNamed (simplifyFormula simC_FORMULA
                                     . codeCoFormula bsrts)) sens
          in return (e, nameAndDisambiguate $ sens1 ++ sens2)
      map_morphism CoCASL2CoSubCFOL mor@Morphism {msource = src, mtarget = tar} =
          let mkBSrts s = sortsWithBottom
                (formulaTreatment defaultCASL2SubCFOL) s Set.empty
          in return mor
              { msource = encodeSig (mkBSrts src) src
              , mtarget = encodeSig (mkBSrts tar) tar
              , op_map = Map.map (\ (i, _) -> (i, Total)) $ op_map mor }
      map_sentence CoCASL2CoSubCFOL sig sen =
          return $ simplifyFormula simC_FORMULA $ codeCoFormula
             (sortsWithBottom (formulaTreatment defaultCASL2SubCFOL)
              sig $ botCoFormulaSorts sen) sen
      map_symbol CoCASL2CoSubCFOL _ s =
          Set.singleton s {symbType = totalizeSymbType $ symbType s}
      has_model_expansion CoCASL2CoSubCFOL = True
      is_weakly_amalgamable CoCASL2CoSubCFOL = True
  
  codeCoRecord :: Set.Set SORT
               -> Record C_FORMULA (FORMULA C_FORMULA) (TERM C_FORMULA)
  codeCoRecord bsrts =
      codeRecord (uniqueBottom defaultCASL2SubCFOL) bsrts $ codeC_FORMULA bsrts
  
  codeCoFormula :: Set.Set SORT -> FORMULA C_FORMULA -> FORMULA C_FORMULA
  codeCoFormula = foldFormula . codeCoRecord
  
  codeC_FORMULA :: Set.Set SORT -> C_FORMULA -> C_FORMULA
  codeC_FORMULA bsrts = foldC_Formula (codeCoRecord bsrts) mapCoRecord
    {foldCoSort_gen_ax = \ _ s o b -> CoSort_gen_ax s (map totalizeOpSymb o) b}
  
  simC_FORMULA :: C_FORMULA -> C_FORMULA
  simC_FORMULA = foldC_Formula (simplifyRecord simC_FORMULA) mapCoRecord
  
  botCoSorts :: C_FORMULA -> Set.Set SORT
  botCoSorts =
      foldC_Formula (botSorts botCoSorts) (constCoRecord Set.unions Set.empty)
  
  botCoFormulaSorts :: FORMULA C_FORMULA -> Set.Set SORT
  botCoFormulaSorts = foldFormula $ botSorts botCoSorts
  