content: {-# 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 . const $ symbItems casl_DL_reserved_words
           parse_symb_map_items CASL_DL =
                Just . const $ 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
  