hets/CASL_DL/Logic_CASL_DL.hs

	Logic_CASL_DL.hs revision cd6e5706893519bfcf24539afa252fcbed5097dd
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule      :  $Header$
127a36cba0c92b465681ec55ad366aca423735ebChristian MaederCopyright   :  (c) Klaus L�ttich, Uni Bremen 2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense     :  similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu
127a36cba0c92b465681ec55ad366aca423735ebChristian MaederMaintainer  :  luettich@tzi.de
127a36cba0c92b465681ec55ad366aca423735ebChristian MaederStability   :  provisional
127a36cba0c92b465681ec55ad366aca423735ebChristian MaederPortability :  portable
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuInstance of class Logic for CASL DL
127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder-}
127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder
127a36cba0c92b465681ec55ad366aca423735ebChristian Maedermodule CASL_DL.Logic_CASL_DL (CASL_DL(..), DLMor, DLFORMULA) where
6c22726220ce34fe3f30c9ae61a1dfa832beac68Christian Maeder
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maederimport Common.Result
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maederimport qualified Data.Set as Set
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maederimport qualified Common.Lib.Rel as Rel
127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder
57e0b8a9f8dc3a481f34e3a5392aaf6d0b7f94aeKlaus Luettichimport CASL_DL.AS_CASL_DL
57e0b8a9f8dc3a481f34e3a5392aaf6d0b7f94aeKlaus Luettichimport CASL_DL.Sign
127a36cba0c92b465681ec55ad366aca423735ebChristian Maederimport CASL_DL.PredefinedSign
127a36cba0c92b465681ec55ad366aca423735ebChristian Maederimport CASL_DL.ATC_CASL_DL ()
127a36cba0c92b465681ec55ad366aca423735ebChristian Maederimport CASL_DL.Parse_AS ()
127a36cba0c92b465681ec55ad366aca423735ebChristian Maederimport CASL_DL.StatAna
127a36cba0c92b465681ec55ad366aca423735ebChristian Maeder
57e0b8a9f8dc3a481f34e3a5392aaf6d0b7f94aeKlaus Luettichimport CASL.Sign
57e0b8a9f8dc3a481f34e3a5392aaf6d0b7f94aeKlaus Luettichimport CASL.Morphism
7fd28a2052af78b95981d76ee6182a7df046cf77Christian Maederimport CASL.SymbolMapAnalysis
57e0b8a9f8dc3a481f34e3a5392aaf6d0b7f94aeKlaus Luettichimport CASL.Logic_CASL
57e0b8a9f8dc3a481f34e3a5392aaf6d0b7f94aeKlaus Luettichimport CASL.AS_Basic_CASL
127a36cba0c92b465681ec55ad366aca423735ebChristian Maederimport CASL.Parse_AS_Basic
127a36cba0c92b465681ec55ad366aca423735ebChristian Maederimport CASL.MapSentence
6c22726220ce34fe3f30c9ae61a1dfa832beac68Christian Maederimport CASL.SymbolParser
6c22726220ce34fe3f30c9ae61a1dfa832beac68Christian Maederimport CASL.Taxonomy
57e0b8a9f8dc3a481f34e3a5392aaf6d0b7f94aeKlaus Luettichimport CASL.SimplifySen
57e0b8a9f8dc3a481f34e3a5392aaf6d0b7f94aeKlaus Luettich
7fd28a2052af78b95981d76ee6182a7df046cf77Christian Maederimport Logic.Logic
57e0b8a9f8dc3a481f34e3a5392aaf6d0b7f94aeKlaus Luettich
57e0b8a9f8dc3a481f34e3a5392aaf6d0b7f94aeKlaus Luettichdata CASL_DL = CASL_DL deriving Show

instance Language CASL_DL  where
 description _ =
  "CASL_DL is at the same time an extension and a restriction of CASL.\n\
  \It additionally provides cardinality restrictions in a description logic\n\
  \sense; and it limits the expressivity of CASL to the description logic\n\
  \SHOIN(D). Hence it provides the following sublogics: \n\
  \  * Card -- CASL plus cardinality restrictions on binary relations\n\
  \  * DL   -- SHOIN(D)\n\
  \  * SHIQ\n\
  \  * SHOIQ\n"

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

instance Category CASL_DL DLSign DLMor
    where
         -- ide :: id -> object -> morphism
         ide CASL_DL = idMor dummy
         -- comp :: id -> morphism -> morphism -> Maybe morphism
         comp CASL_DL = compose (const id)
         -- dom, cod :: id -> morphism -> object
         dom CASL_DL = msource
         cod CASL_DL = mtarget
         -- legal_obj :: id -> object -> Bool
         legal_obj CASL_DL = legalSign
         -- legal_mor :: id -> morphism -> Bool
         legal_mor CASL_DL = legalMor

-- abstract syntax, parsing (and printing)

instance Syntax CASL_DL DL_BASIC_SPEC
                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 ()
map_DL_FORMULA mor (Cardinality ct pn varT natT r) =
    Cardinality ct pn' varT' natT' 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
      parse_sentence CASL_DL = Nothing
      sym_of CASL_DL = symOf
      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 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) 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 sml =
             statSymbMapItems sml >>= checkSymbolMapDL
         stat_symb_items CASL_DL = statSymbItems
         ensures_amalgamability CASL_DL _ =
             fail "CASL_DL: ensures_amalgamability nyi" -- ???

         sign_to_basic_spec CASL_DL _sigma _sens = Basic_spec [] -- ???

         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
         signature_difference CASL_DL s = return . diffSig diffCASL_DLSign s
         morphism_union CASL_DL = morphismUnion (const id) addCASL_DLSign
         final_union CASL_DL = finalUnion addCASL_DLSign
         is_subsig CASL_DL = isSubSig isSubCASL_DLSign
         inclusion CASL_DL = sigInclusion dummy isSubCASL_DLSign
         cogenerated_sign CASL_DL = cogeneratedSign dummy
         generated_sign CASL_DL = generatedSign dummy
         induced_from_morphism CASL_DL = inducedFromMorphism dummy
         induced_from_to_morphism CASL_DL =
             inducedFromToMorphism dummy isSubCASL_DLSign
         theory_to_taxonomy CASL_DL tgk mo sig sen =
             convTaxo tgk mo (extendSortRelWithTopSort sig) sen

-- |
-- 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,topSort))
                                    $ sortSet sig)

instance Logic CASL_DL ()
               DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               DLSign
               DLMor
               Symbol RawSymbol () where
         stability _ = Unstable
         empty_proof_tree _ = ()