Logic_CASL_DL.hs revision d6c6b2543c509ec7f6213e4cba675d96304a7fd6
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
09249711700a6acbc40a2e337688b434d7aafa28Christian MaederModule : $Header$
76647324ed70f33b95a881b536d883daccf9568dChristian MaederDescription : Instance of class Logic for CASL DL
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Klaus Luettich, Uni Bremen 2005
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederMaintainer : luecke@informatik.uni-bremen.de
76647324ed70f33b95a881b536d883daccf9568dChristian MaederStability : provisional
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederInstance of class Logic for CASL DL
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule CASL_DL.Logic_CASL_DL (CASL_DL (..), DLMor, DLFORMULA) where
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport qualified Data.Set as Set
950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maederimport qualified Common.Lib.Rel as Rel
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maederdata CASL_DL = CASL_DL deriving Show
76647324ed70f33b95a881b536d883daccf9568dChristian Maederinstance Language CASL_DL where
d48085f765fca838c1d972d2123601997174583dChristian Maeder description _ = unlines
d48085f765fca838c1d972d2123601997174583dChristian Maeder [ "CASL_DL is at the same time an extension and a restriction of CASL."
d48085f765fca838c1d972d2123601997174583dChristian Maeder , "It additionally provides cardinality restrictions in a description logic"
d48085f765fca838c1d972d2123601997174583dChristian Maeder , "sense; and it limits the expressivity of CASL to the description logic"
d48085f765fca838c1d972d2123601997174583dChristian Maeder , "SHOIN(D). Hence it provides the following sublogics:"
05ae87b9efa19655024b0b6ac344d250b96567cdChristian Maeder , " * Card -- CASL plus cardinality restrictions on binary relations"
d48085f765fca838c1d972d2123601997174583dChristian Maeder , " * DL -- SHOIN(D)"
a716971174535184da7713ed308423e355a4aa66Christian Maeder , " * SHOIQ" ]
793945d4ac7c0f22760589c87af8e71427c76118Christian Maedertype DLMor = Morphism DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
5e5c3fbbf8c22b883d551d83429b9f8d8041f1e0Christian Maedertype DLFORMULA = FORMULA DL_FORMULA
f2c2b420e386a90d940c758c631d16f12952d2b7Christian Maederinstance SignExtension CASL_DLSign where
f2c2b420e386a90d940c758c631d16f12952d2b7Christian Maeder isSubSignExtension = isSubCASL_DLSign
793945d4ac7c0f22760589c87af8e71427c76118Christian Maederinstance Syntax CASL_DL DL_BASIC_SPEC
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder SYMB_ITEMS SYMB_MAP_ITEMS
a716971174535184da7713ed308423e355a4aa66Christian Maeder parse_basic_spec CASL_DL = Just $ basicSpec casl_DL_reserved_words
5e5c3fbbf8c22b883d551d83429b9f8d8041f1e0Christian Maeder parse_symb_items CASL_DL = Just $ symbItems casl_DL_reserved_words
a716971174535184da7713ed308423e355a4aa66Christian Maeder parse_symb_map_items CASL_DL =
a716971174535184da7713ed308423e355a4aa66Christian Maeder Just $ symbMapItems casl_DL_reserved_words
a716971174535184da7713ed308423e355a4aa66Christian Maeder-- CASL_DL logic
793945d4ac7c0f22760589c87af8e71427c76118Christian Maedermap_DL_FORMULA :: MapSen DL_FORMULA CASL_DLSign (DefMorExt CASL_DLSign)
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maedermap_DL_FORMULA mor (Cardinality ct pn varT natT qualT r) =
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder Cardinality ct pn' varT' natT' qualT r
9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian Maeder where pn' = mapPrSymb mor pn
9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian Maeder varT' = mapTrm varT
fd2dcd5c071e938c07338fd3a32296819b8a2333Christian Maeder natT' = mapTrm natT
fd2dcd5c071e938c07338fd3a32296819b8a2333Christian Maeder mapTrm = mapTerm map_DL_FORMULA mor
fd2dcd5c071e938c07338fd3a32296819b8a2333Christian Maederinstance Sentences CASL_DL DLFORMULA DLSign DLMor Symbol where
9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian Maeder map_sen CASL_DL m = return . mapSen map_DL_FORMULA m
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder sym_of CASL_DL = symOf
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder symmap_of CASL_DL = morphismToSymbMap
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder sym_name CASL_DL = symName
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder simplify_sen CASL_DL = simplifySen minDLForm simplifyCD
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian MaedersimplifyCD :: DLSign -> DL_FORMULA -> DL_FORMULA
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian MaedersimplifyCD sign (Cardinality ct ps t1 t2 t3 r) = simpCard
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder where simpCard = maybe (card ps)
d48085f765fca838c1d972d2123601997174583dChristian Maeder (const $ card $ Pred_name pn)
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder (resultToMaybe $
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder minDLForm sign $ card $ Pred_name pn)
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder simp = rmTypesT minDLForm simplifyCD sign
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder card psy = Cardinality ct psy (simp t1) (simp t2) t3 r
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder pn = case ps of
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder Pred_name n -> n
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder Qual_pred_name n _pType _ -> n
a716971174535184da7713ed308423e355a4aa66Christian Maederinstance StaticAnalysis CASL_DL DL_BASIC_SPEC DLFORMULA
a716971174535184da7713ed308423e355a4aa66Christian Maeder SYMB_ITEMS SYMB_MAP_ITEMS
67a14e04c885a87e4273a300eef60e680531088cChristian Maeder Symbol RawSymbol where
d48085f765fca838c1d972d2123601997174583dChristian Maeder basic_analysis CASL_DL = Just basicCASL_DLAnalysis
d48085f765fca838c1d972d2123601997174583dChristian Maeder stat_symb_map_items CASL_DL s t sml =
d48085f765fca838c1d972d2123601997174583dChristian Maeder statSymbMapItems s t sml >>= checkSymbolMapDL
d48085f765fca838c1d972d2123601997174583dChristian Maeder stat_symb_items CASL_DL = statSymbItems
d48085f765fca838c1d972d2123601997174583dChristian Maeder symbol_to_raw CASL_DL = symbolToRaw
d48085f765fca838c1d972d2123601997174583dChristian Maeder id_to_raw CASL_DL = idToRaw
d48085f765fca838c1d972d2123601997174583dChristian Maeder empty_signature CASL_DL = emptySign emptyCASL_DLSign
d48085f765fca838c1d972d2123601997174583dChristian Maeder signature_union CASL_DL s = return . addSig addCASL_DLSign s
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder morphism_union CASL_DL = plainMorphismUnion addCASL_DLSign
d48085f765fca838c1d972d2123601997174583dChristian Maeder final_union CASL_DL = finalUnion addCASL_DLSign
d48085f765fca838c1d972d2123601997174583dChristian Maeder is_subsig CASL_DL = isSubSig isSubCASL_DLSign
d48085f765fca838c1d972d2123601997174583dChristian Maeder subsig_inclusion CASL_DL = sigInclusion emptyMorExt
d48085f765fca838c1d972d2123601997174583dChristian Maeder cogenerated_sign CASL_DL = cogeneratedSign emptyMorExt
d48085f765fca838c1d972d2123601997174583dChristian Maeder generated_sign CASL_DL = generatedSign emptyMorExt
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder induced_from_morphism CASL_DL = inducedFromMorphism emptyMorExt
d48085f765fca838c1d972d2123601997174583dChristian Maeder induced_from_to_morphism CASL_DL =
d48085f765fca838c1d972d2123601997174583dChristian Maeder inducedFromToMorphism emptyMorExt isSubCASL_DLSign diffCASL_DLSign
d48085f765fca838c1d972d2123601997174583dChristian Maeder theory_to_taxonomy CASL_DL tgk mo =
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder convTaxo tgk mo . extendSortRelWithTopSort
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- | extend the sort relation with sort Thing for the taxonomy display
d48085f765fca838c1d972d2123601997174583dChristian MaederextendSortRelWithTopSort :: Sign f e -> Sign f e
76647324ed70f33b95a881b536d883daccf9568dChristian MaederextendSortRelWithTopSort sig = sig {sortRel = addThing $ sortRel sig}
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder where addThing r = Rel.union r (Rel.fromSet
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder $ Set.map (\ x -> (x, topSort))
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder $ sortSet sig)
d48085f765fca838c1d972d2123601997174583dChristian Maederinstance Logic CASL_DL CASL_DL_SL
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder Symbol RawSymbol ProofTree where
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder stability _ = Unstable
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder top_sublogic _ = SROIQ
35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder all_sublogics _ = [SROIQ]
76647324ed70f33b95a881b536d883daccf9568dChristian Maederinstance MinSublogic CASL_DL_SL DLFORMULA where
d48085f765fca838c1d972d2123601997174583dChristian Maeder minSublogic _ = SROIQ
d48085f765fca838c1d972d2123601997174583dChristian Maederinstance ProjectSublogic CASL_DL_SL DLMor where
d48085f765fca838c1d972d2123601997174583dChristian Maeder projectSublogic _ = id
d48085f765fca838c1d972d2123601997174583dChristian Maederinstance MinSublogic CASL_DL_SL DLMor where
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder minSublogic _ = SROIQ
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maederinstance ProjectSublogic CASL_DL_SL DLSign where
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder projectSublogic _ = id
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maederinstance MinSublogic CASL_DL_SL DLSign where
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maeder minSublogic _ = SROIQ
3eb7ebab2dd79ac5277f087b18e8f05b9e9f0f9bChristian Maederinstance ProjectSublogicM CASL_DL_SL SYMB_MAP_ITEMS where
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder projectSublogicM _ = Just
6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian Maederinstance ProjectSublogicM CASL_DL_SL SYMB_ITEMS where
6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian Maeder projectSublogicM _ = Just
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederinstance MinSublogic CASL_DL_SL SYMB_MAP_ITEMS where
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder minSublogic _ = SROIQ
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederinstance MinSublogic CASL_DL_SL SYMB_ITEMS where
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder minSublogic _ = SROIQ
9a44a07ffc79da9852b6319bd6d9df81efe99809Christian Maederinstance ProjectSublogic CASL_DL_SL DL_BASIC_SPEC where
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder projectSublogic _ = id
76647324ed70f33b95a881b536d883daccf9568dChristian Maederinstance MinSublogic CASL_DL_SL DL_BASIC_SPEC where
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder minSublogic _ = SROIQ
a39a820684c1974350f46593025e0bb279f41bc6Christian Maederinstance SublogicName CASL_DL_SL where
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder sublogicName SROIQ = show SROIQ
a39a820684c1974350f46593025e0bb279f41bc6Christian Maederinstance SemiLatticeWithTop CASL_DL_SL where
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder join _ _ = SROIQ
d48085f765fca838c1d972d2123601997174583dChristian Maederinstance ProjectSublogic CASL_DL_SL Symbol where
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder projectSublogic _ = id
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maederinstance ProjectSublogicM CASL_DL_SL Symbol where
d48085f765fca838c1d972d2123601997174583dChristian Maeder projectSublogicM _ = Just
d48085f765fca838c1d972d2123601997174583dChristian Maederinstance MinSublogic CASL_DL_SL Symbol where
e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maeder minSublogic _ = SROIQ