{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./CASL_DL/Logic_CASL_DL.hs
Description :  Instance of class Logic for CASL DL
Copyright   :  (c) Klaus Luettich, Uni Bremen 2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Instance of class Logic for CASL DL
-}

module CASL_DL.Logic_CASL_DL (CASL_DL (..), DLMor, DLFORMULA) where

import qualified Data.Set as Set
import qualified Common.Lib.Rel as Rel
import Common.Result
import Common.ProofTree
import Common.DocUtils

import CASL_DL.AS_CASL_DL
import CASL_DL.Sign
import CASL_DL.PredefinedCASLAxioms
import CASL_DL.ATC_CASL_DL ()
import CASL_DL.Parse_AS ()
import CASL_DL.StatAna

import CASL.Sign
import CASL.Morphism
import CASL.SymbolMapAnalysis
import CASL.AS_Basic_CASL
import CASL.Parse_AS_Basic
import CASL.MapSentence
import CASL.SymbolParser
import CASL.Taxonomy
import CASL.SimplifySen
import CASL.Logic_CASL ()
import CASL_DL.Sublogics

import Logic.Logic

data CASL_DL = CASL_DL deriving Show

instance Language CASL_DL where
 description _ = unlines
  [ "CASL_DL is the restriction of CASL to OWL 1 expressivity."
  , "It additionally provides cardinality restrictions in a description logic"
  , "sense; and it limits the expressivity of CASL to the description logic"
  , "SHOIN(D). Hence it provides the following sublogics:"
  , "  * Card -- CASL plus cardinality restrictions on binary relations"
  , "  * DL   -- SHOIN(D)"
  , "  * SHIQ"
  , "  * SHOIQ" ]

type DLMor = Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
type DLFORMULA = FORMULA DL_FORMULA

instance SignExtension CASL_DLSign where
  isSubSignExtension = isSubCASL_DLSign

instance Syntax CASL_DL DL_BASIC_SPEC
                Symbol SYMB_ITEMS SYMB_MAP_ITEMS
      where
         parse_basic_spec CASL_DL = Just $ basicSpec casl_DL_reserved_words
         parse_symb_items CASL_DL = Just $ symbItems casl_DL_reserved_words
         parse_symb_map_items CASL_DL =
             Just $ symbMapItems casl_DL_reserved_words

-- CASL_DL logic

map_DL_FORMULA :: MapSen DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
map_DL_FORMULA mor (Cardinality ct pn varT natT qualT r) =
    Cardinality ct pn' varT' natT' qualT r
    where pn' = mapPrSymb mor pn
          varT' = mapTrm varT
          natT' = mapTrm natT
          mapTrm = mapTerm map_DL_FORMULA mor

instance Sentences CASL_DL DLFORMULA DLSign DLMor Symbol where
      map_sen CASL_DL m = return . mapSen map_DL_FORMULA m
      sym_of CASL_DL = symOf
      symKind CASL_DL = show . pretty . symbolKind . symbType
      symmap_of CASL_DL = morphismToSymbMap
      sym_name CASL_DL = symName
      simplify_sen CASL_DL = simplifySen minDLForm simplifyCD

simplifyCD :: DLSign -> DL_FORMULA -> DL_FORMULA
simplifyCD sign (Cardinality ct ps t1 t2 t3 r) = simpCard
    where simpCard = maybe (card ps)
                           (const $ card $ Pred_name pn)
                           (resultToMaybe $
                            minDLForm sign $ card $ Pred_name pn)
          simp = rmTypesT minDLForm simplifyCD sign
          card psy = Cardinality ct psy (simp t1) (simp t2) t3 r
          pn = case ps of
               Pred_name n -> n
               Qual_pred_name n _pType _ -> n

instance StaticAnalysis CASL_DL DL_BASIC_SPEC DLFORMULA
               SYMB_ITEMS SYMB_MAP_ITEMS
               DLSign
               DLMor
               Symbol RawSymbol where
         basic_analysis CASL_DL = Just basicCASL_DLAnalysis
         stat_symb_map_items CASL_DL s t sml =
             statSymbMapItems s t sml >>= checkSymbolMapDL
         stat_symb_items CASL_DL = statSymbItems

         symbol_to_raw CASL_DL = symbolToRaw
         id_to_raw CASL_DL = idToRaw
         matches CASL_DL = CASL.Morphism.matches

         empty_signature CASL_DL = emptySign emptyCASL_DLSign
         signature_union CASL_DL s = return . addSig addCASL_DLSign s
         morphism_union CASL_DL = plainMorphismUnion addCASL_DLSign
         final_union CASL_DL = finalUnion addCASL_DLSign
         is_subsig CASL_DL = isSubSig isSubCASL_DLSign
         subsig_inclusion CASL_DL = sigInclusion emptyMorExt
         cogenerated_sign CASL_DL = cogeneratedSign emptyMorExt
         generated_sign CASL_DL = generatedSign emptyMorExt
         induced_from_morphism CASL_DL = inducedFromMorphism emptyMorExt
         induced_from_to_morphism CASL_DL =
             inducedFromToMorphism emptyMorExt isSubCASL_DLSign diffCASL_DLSign
         theory_to_taxonomy CASL_DL tgk mo =
             convTaxo tgk mo . extendSortRelWithTopSort

-- | extend the sort relation with sort Thing for the taxonomy display
extendSortRelWithTopSort :: Sign f e -> Sign f e
extendSortRelWithTopSort sig = sig {sortRel = addThing $ sortRel sig}
    where addThing r = Rel.union r (Rel.fromSet
                                    $ Set.map (\ x -> (x, thing))
                                    $ sortSet sig)

instance Logic CASL_DL CASL_DL_SL
               DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               DLSign
               DLMor
               Symbol RawSymbol ProofTree where
         stability _ = Experimental
         top_sublogic _ = SROIQ
         all_sublogics _ = [SROIQ]

instance MinSublogic CASL_DL_SL DLFORMULA where
    minSublogic _ = SROIQ

instance ProjectSublogic CASL_DL_SL DLMor where
    projectSublogic _ = id

instance MinSublogic CASL_DL_SL DLMor where
    minSublogic _ = SROIQ

instance ProjectSublogic CASL_DL_SL DLSign where
    projectSublogic _ = id

instance MinSublogic CASL_DL_SL DLSign where
    minSublogic _ = SROIQ

instance ProjectSublogicM CASL_DL_SL SYMB_MAP_ITEMS where
    projectSublogicM _ = Just

instance ProjectSublogicM CASL_DL_SL SYMB_ITEMS where
    projectSublogicM _ = Just

instance MinSublogic CASL_DL_SL SYMB_MAP_ITEMS where
    minSublogic _ = SROIQ

instance MinSublogic CASL_DL_SL SYMB_ITEMS where
    minSublogic _ = SROIQ

instance ProjectSublogic CASL_DL_SL DL_BASIC_SPEC where
    projectSublogic _ = id

instance MinSublogic CASL_DL_SL DL_BASIC_SPEC where
    minSublogic _ = SROIQ

instance SublogicName CASL_DL_SL where
    sublogicName SROIQ = show SROIQ

instance SemiLatticeWithTop CASL_DL_SL where
    lub _ _ = SROIQ
    top = SROIQ

instance ProjectSublogic CASL_DL_SL Symbol where
    projectSublogic _ = id

instance ProjectSublogicM CASL_DL_SL Symbol where
    projectSublogicM _ = Just

instance MinSublogic CASL_DL_SL Symbol where
    minSublogic _ = SROIQ
