content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./Comorphisms/CASL_DL2CASL.hs
  Description :  Inclusion of CASL_DL into CASL
  Copyright   :  (c) Uni Bremen 2007
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  luecke@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  non-portable (via Logic.Logic)
  
  -}
  
  module Comorphisms.CASL_DL2CASL
      (
       CASL_DL2CASL (..)
      )
      where
  
  import Logic.Logic
  import Logic.Comorphism
  
  import Common.AS_Annotation
  import Common.ProofTree
  import Common.Result
  import qualified Common.Lib.Rel as Rel
  import qualified Control.Monad.Fail as Fail
  
  -- CASL_DL = domain
  import CASL_DL.PredefinedCASLAxioms
  import CASL_DL.Logic_CASL_DL
  import CASL_DL.AS_CASL_DL
  import CASL_DL.Sign ()
  import CASL_DL.StatAna -- DLSign
  import CASL_DL.Sublogics
  
  -- CASL = codomain
  import CASL.Logic_CASL
  import CASL.AS_Basic_CASL
  import CASL.Sign
  import CASL.Morphism
  import CASL.Sublogic as Sublogic
  
  import qualified Data.Set as Set
  
  data CASL_DL2CASL = CASL_DL2CASL deriving Show
  
  instance Language CASL_DL2CASL
  
  instance Comorphism
      CASL_DL2CASL    -- comorphism
      CASL_DL         -- lid domain
      CASL_DL_SL      -- sublogics domain
      DL_BASIC_SPEC   -- Basic spec domain
      DLFORMULA       -- sentence domain
      SYMB_ITEMS      -- symbol items domain
      SYMB_MAP_ITEMS  -- symbol map items domain
      DLSign          -- signature domain
      DLMor           -- morphism domain
      Symbol          -- symbol domain
      RawSymbol       -- rawsymbol domain
      ProofTree     -- proof tree codomain
      CASL            -- lid codomain
      CASL_Sublogics  -- sublogics codomain
      CASLBasicSpec   -- Basic spec codomain
      CASLFORMULA     -- sentence codomain
      SYMB_ITEMS      -- symbol items codomain
      SYMB_MAP_ITEMS  -- symbol map items codomain
      CASLSign        -- signature codomain
      CASLMor         -- morphism codomain
      Symbol          -- symbol codomain
      RawSymbol       -- rawsymbol codomain
      ProofTree     -- proof tree domain
      where
        sourceLogic CASL_DL2CASL = CASL_DL
        targetLogic CASL_DL2CASL = CASL
        sourceSublogic CASL_DL2CASL = SROIQ
        mapSublogic CASL_DL2CASL _ = Just $ Sublogic.caslTop
                        { sub_features = LocFilSub
                        , cons_features = emptyMapConsFeature }
        map_symbol CASL_DL2CASL _ = Set.singleton
        map_sentence CASL_DL2CASL = trSentence
        map_morphism CASL_DL2CASL = mapMor
        map_theory CASL_DL2CASL = trTheory
        isInclusionComorphism CASL_DL2CASL = True
        has_model_expansion CASL_DL2CASL = True
  
  {- | mapping of morphims, we just forget the
  additional features -}
  mapMor :: DLMor -> Result CASLMor
  mapMor inMor =
      let
          ms = trSign $ msource inMor
          mt = trSign $ mtarget inMor
          sm = sort_map inMor
          fm = op_map inMor
          pm = pred_map inMor
      in return (embedMorphism () ms mt)
          { sort_map = sm
          , op_map = fm
          , pred_map = pm }
  
  -- | we forget additional information in the signature
  projectToCASL :: DLSign -> CASLSign
  projectToCASL dls = dls
                      {
                        sentences = []
                      , extendedInfo = ()
                      }
  
  {- | Thing is established as the TopSort of all sorts
  defined in the CASL_DL spec, a predefined signature
  is added -}
  trSign :: DLSign -> CASLSign
  trSign inSig =
      let
          inC = projectToCASL inSig `uniteCASLSign` predefSign
          inSorts = sortSet inSig
          inData = sortSet predefSign
      in
        inC
        {
          sortRel = Rel.insertKey thing
            $ Rel.insertKey dataS
            $ Set.fold (`Rel.insertDiffPair` dataS)
                    (Set.fold (`Rel.insertDiffPair` thing)
                     (sortRel inC) inSorts)
            $ Set.delete dataS inData
        }
  
  -- * translation of the signature predefined axioms are added
  
  -- | Translation of theories
  trTheory :: (DLSign, [Named (FORMULA DL_FORMULA)]) ->
              Result (CASLSign, [Named (FORMULA ())])
  trTheory (inSig, inForms) = do
        outForms <- mapR (trNamedSentence inSig) inForms
        return (trSign inSig, predefinedAxioms ++ outForms)
  
  -- | translation of named sentences
  trNamedSentence :: DLSign -> Named (FORMULA DL_FORMULA) ->
                     Result (Named (FORMULA ()))
  trNamedSentence inSig inForm = do
          outSen <- trSentence inSig $ sentence inForm
          return $ mapNamed (const outSen) inForm
  
  -- | translation of sentences
  trSentence :: DLSign -> FORMULA DL_FORMULA -> Result (FORMULA ())
  trSentence inSig inF =
        case inF of
          Quantification qf vs frm rn ->
              do
                outF <- trSentence inSig frm
                return (Quantification qf vs outF rn)
          Junction j fns rn ->
              do
                outF <- mapR (trSentence inSig) fns
                return (Junction j outF rn)
          Relation f1 c f2 rn ->
              do
                out1 <- trSentence inSig f1
                out2 <- trSentence inSig f2
                return (Relation out1 c out2 rn)
          Negation frm rn ->
              do
                outF <- trSentence inSig frm
                return (Negation outF rn)
          Atom b rn -> return (Atom b rn)
          Predication pr trm rn ->
              do
                ot <- mapR (trTerm inSig) trm
                return (Predication pr ot rn)
          Definedness tm rn ->
              do
                ot <- trTerm inSig tm
                return (Definedness ot rn)
          Equation t1 e t2 rn ->
              do
                ot1 <- trTerm inSig t1
                ot2 <- trTerm inSig t2
                return (Equation ot1 e ot2 rn)
          Membership t1 st rn ->
              do
                ot <- trTerm inSig t1
                return (Membership ot st rn)
          Mixfix_formula trm ->
               do
                ot <- trTerm inSig trm
                return (Mixfix_formula ot)
          Unparsed_formula str rn ->
              return (Unparsed_formula str rn)
          Sort_gen_ax cstr ft ->
              return (Sort_gen_ax cstr ft)
          QuantOp {} -> Fail.fail "CASL_DL2CASL.QuantOp"
          QuantPred {} -> Fail.fail "CASL_DL2CASL.QuantPred"
          ExtFORMULA form ->
              case form of
                Cardinality {} ->
                      Fail.fail "Mapping of cardinality not implemented"
  
  -- | translation of terms
  trTerm :: DLSign -> TERM DL_FORMULA -> Result (TERM ())
  trTerm inSig inF =
      case inF of
        Qual_var v s rn -> return (Qual_var v s rn)
        Application os tms rn ->
            do
              ot <- mapR (trTerm inSig) tms
              return (Application os ot rn)
        Sorted_term trm st rn ->
            do
              ot <- trTerm inSig trm
              return (Sorted_term ot st rn)
        Cast trm st rn ->
            do
              ot <- trTerm inSig trm
              return (Cast ot st rn)
        Conditional t1 frm t2 rn ->
            do
              ot1 <- trTerm inSig t1
              ot2 <- trTerm inSig t2
              of1 <- trSentence inSig frm
              return (Conditional ot1 of1 ot2 rn)
        Unparsed_term str rn -> return (Unparsed_term str rn)
        Mixfix_qual_pred ps -> return (Mixfix_qual_pred ps)
        Mixfix_term trm ->
            do
              ot <- mapR (trTerm inSig) trm
              return (Mixfix_term ot)
        Mixfix_token tok -> return (Mixfix_token tok)
        Mixfix_sorted_term st rn -> return (Mixfix_sorted_term st rn)
        Mixfix_cast st rn -> return (Mixfix_cast st rn)
        Mixfix_parenthesized trm rn ->
            do
              ot <- mapR (trTerm inSig) trm
              return (Mixfix_parenthesized ot rn)
        Mixfix_bracketed trm rn ->
            do
              ot <- mapR (trTerm inSig) trm
              return (Mixfix_bracketed ot rn)
        Mixfix_braced trm rn ->
            do
              ot <- mapR (trTerm inSig) trm
              return (Mixfix_braced ot rn)
        ExtTERM _ -> return $ ExtTERM ()
  