ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu{- |

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae BungiuModule : $Header$

734257b9ea9fcaa18d4e3627f54f5295a99aa1f7Felix Gabriel ManceDescription : Instance of class Logic for CASL DL

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae BungiuCopyright : (c) Klaus L�ttich, Uni Bremen 2005

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae BungiuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae BungiuMaintainer : luecke@informatik.uni-bremen.de

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae BungiuStability : provisional

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae BungiuPortability : portable

c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Mance

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae BungiuInstance of class Logic for CASL DL

15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance-}

734257b9ea9fcaa18d4e3627f54f5295a99aa1f7Felix Gabriel Mance

c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Mancemodule CASL_DL.Logic_CASL_DL (CASL_DL(..), DLMor, DLFORMULA) where

c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Mance

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiuimport Common.Result

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiuimport qualified Data.Set as Set

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiuimport qualified Common.Lib.Rel as Rel

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu

ed1b8e97e72b2e3e92edaf2eb22a4b5373d705f1Felix Gabriel Manceimport CASL_DL.AS_CASL_DL

5180a08007989fd364622fc9bc01f82141643f7bFelix Gabriel Manceimport CASL_DL.Sign

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiuimport CASL_DL.PredefinedSign

12078a24d49ba36b83cda9d07c8e8a480c493fe8Felix Gabriel Manceimport CASL_DL.ATC_CASL_DL ()

734257b9ea9fcaa18d4e3627f54f5295a99aa1f7Felix Gabriel Manceimport CASL_DL.Parse_AS ()

c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Manceimport CASL_DL.StatAna

0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Mance

0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Manceimport CASL.Sign

3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Manceimport CASL.Morphism

3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Manceimport CASL.SymbolMapAnalysis

0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Manceimport CASL.AS_Basic_CASL

e5dc5119231bdeb5c604f7709e0fa197fd2c4829Felix Gabriel Manceimport CASL.Parse_AS_Basic

e5dc5119231bdeb5c604f7709e0fa197fd2c4829Felix Gabriel Manceimport CASL.MapSentence

0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Manceimport CASL.SymbolParser

0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Manceimport CASL.Taxonomy

30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Manceimport CASL.SimplifySen

30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mance

e5dc5119231bdeb5c604f7709e0fa197fd2c4829Felix Gabriel Manceimport Logic.Logic

30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mance

2c0c0264249b8d2a3f465e22cb3c6d9c4ac8924aFelix Gabriel Mancedata CASL_DL = CASL_DL deriving Show

2c0c0264249b8d2a3f465e22cb3c6d9c4ac8924aFelix Gabriel Mance

2c0c0264249b8d2a3f465e22cb3c6d9c4ac8924aFelix Gabriel Manceinstance Language CASL_DL where

2c0c0264249b8d2a3f465e22cb3c6d9c4ac8924aFelix Gabriel Mance description _ =

2c0c0264249b8d2a3f465e22cb3c6d9c4ac8924aFelix Gabriel Mance "CASL_DL is at the same time an extension and a restriction of CASL.\n\

2c0c0264249b8d2a3f465e22cb3c6d9c4ac8924aFelix Gabriel Mance \It additionally provides cardinality restrictions in a description logic\n\

2c0c0264249b8d2a3f465e22cb3c6d9c4ac8924aFelix Gabriel Mance \sense; and it limits the expressivity of CASL to the description logic\n\

2c0c0264249b8d2a3f465e22cb3c6d9c4ac8924aFelix Gabriel Mance \SHOIN(D). Hence it provides the following sublogics: \n\

2c0c0264249b8d2a3f465e22cb3c6d9c4ac8924aFelix Gabriel Mance \ * Card -- CASL plus cardinality restrictions on binary relations\n\

2c0c0264249b8d2a3f465e22cb3c6d9c4ac8924aFelix Gabriel Mance \ * DL -- SHOIN(D)\n\

120b4b5a0f61d93eeaa17ff2c7867f58c7325e3bFelix Gabriel Mance \ * SHIQ\n\

120b4b5a0f61d93eeaa17ff2c7867f58c7325e3bFelix Gabriel Mance \ * SHOIQ\n"

120b4b5a0f61d93eeaa17ff2c7867f58c7325e3bFelix Gabriel Mance

120b4b5a0f61d93eeaa17ff2c7867f58c7325e3bFelix Gabriel Mancetype DLMor = Morphism DL_FORMULA CASL_DLSign ()

120b4b5a0f61d93eeaa17ff2c7867f58c7325e3bFelix Gabriel Mancetype DLFORMULA = FORMULA DL_FORMULA

120b4b5a0f61d93eeaa17ff2c7867f58c7325e3bFelix Gabriel Mance

120b4b5a0f61d93eeaa17ff2c7867f58c7325e3bFelix Gabriel Manceinstance Category CASL_DL DLSign DLMor

120b4b5a0f61d93eeaa17ff2c7867f58c7325e3bFelix Gabriel Mance where

120b4b5a0f61d93eeaa17ff2c7867f58c7325e3bFelix Gabriel Mance -- ide :: id -> object -> morphism

120b4b5a0f61d93eeaa17ff2c7867f58c7325e3bFelix Gabriel Mance ide CASL_DL = idMor ()

120b4b5a0f61d93eeaa17ff2c7867f58c7325e3bFelix Gabriel Mance -- comp :: id -> morphism -> morphism -> Maybe morphism

120b4b5a0f61d93eeaa17ff2c7867f58c7325e3bFelix Gabriel Mance comp CASL_DL = compose (const id)

12078a24d49ba36b83cda9d07c8e8a480c493fe8Felix Gabriel Mance -- dom, cod :: id -> morphism -> object

12078a24d49ba36b83cda9d07c8e8a480c493fe8Felix Gabriel Mance dom CASL_DL = msource

12078a24d49ba36b83cda9d07c8e8a480c493fe8Felix Gabriel Mance cod CASL_DL = mtarget

12078a24d49ba36b83cda9d07c8e8a480c493fe8Felix Gabriel Mance -- legal_obj :: id -> object -> Bool

12078a24d49ba36b83cda9d07c8e8a480c493fe8Felix Gabriel Mance legal_obj CASL_DL = legalSign

12078a24d49ba36b83cda9d07c8e8a480c493fe8Felix Gabriel Mance -- legal_mor :: id -> morphism -> Bool

12078a24d49ba36b83cda9d07c8e8a480c493fe8Felix Gabriel Mance legal_mor CASL_DL = legalMor

0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Mance

30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mance-- abstract syntax, parsing (and printing)

30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mance

0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Manceinstance Syntax CASL_DL DL_BASIC_SPEC

30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mance SYMB_ITEMS SYMB_MAP_ITEMS

3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance where

3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance parse_basic_spec CASL_DL = Just $ basicSpec casl_DL_reserved_words

9c3f6477a95da46a907326206673b4a5c2164164Felix Gabriel Mance parse_symb_items CASL_DL = Just $ symbItems casl_DL_reserved_words

3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance parse_symb_map_items CASL_DL =

3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance Just $ symbMapItems casl_DL_reserved_words

30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mance

3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance-- CASL_DL logic

3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance

30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mancemap_DL_FORMULA :: MapSen DL_FORMULA CASL_DLSign ()

9c3f6477a95da46a907326206673b4a5c2164164Felix Gabriel Mancemap_DL_FORMULA mor (Cardinality ct pn varT natT qualT r) =

316ef492799cd45fea0f5c26932f49adddfda3f7Felix Gabriel Mance Cardinality ct pn' varT' natT' qualT' r

3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance where pn' = mapPrSymb mor pn

31a5ba51cd6d24e28a23abf64ce4043a45eabbefFelix Gabriel Mance varT' = mapTrm varT

30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mance natT' = mapTrm natT

3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance qualT' = case qualT of

316ef492799cd45fea0f5c26932f49adddfda3f7Felix Gabriel Mance Nothing -> Nothing

316ef492799cd45fea0f5c26932f49adddfda3f7Felix Gabriel Mance Just x -> Just $ mapTrm x

316ef492799cd45fea0f5c26932f49adddfda3f7Felix Gabriel Mance mapTrm = mapTerm map_DL_FORMULA mor

316ef492799cd45fea0f5c26932f49adddfda3f7Felix Gabriel Mance

31a5ba51cd6d24e28a23abf64ce4043a45eabbefFelix Gabriel Manceinstance Sentences CASL_DL DLFORMULA DLSign DLMor Symbol where

0be7a9c012366ada63d587898a15c551b499b76dFelix Gabriel Mance map_sen CASL_DL m = return . mapSen map_DL_FORMULA m

30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mance parse_sentence CASL_DL = Nothing

e5e3f128bbd44dd393e1038718038bd323f5e415Felix Gabriel Mance sym_of CASL_DL = symOf

e5e3f128bbd44dd393e1038718038bd323f5e415Felix Gabriel Mance symmap_of CASL_DL = morphismToSymbMap

e5e3f128bbd44dd393e1038718038bd323f5e415Felix Gabriel Mance sym_name CASL_DL = symName

e5e3f128bbd44dd393e1038718038bd323f5e415Felix Gabriel Mance simplify_sen CASL_DL = simplifySen minDLForm simplifyCD

e5e3f128bbd44dd393e1038718038bd323f5e415Felix Gabriel Mance

e5e3f128bbd44dd393e1038718038bd323f5e415Felix Gabriel MancesimplifyCD :: DLSign -> DL_FORMULA -> DL_FORMULA

e5e3f128bbd44dd393e1038718038bd323f5e415Felix Gabriel MancesimplifyCD sign (Cardinality ct ps t1 t2 t3 r) = simpCard

734257b9ea9fcaa18d4e3627f54f5295a99aa1f7Felix Gabriel Mance where simpCard = maybe (card ps)

31a5ba51cd6d24e28a23abf64ce4043a45eabbefFelix Gabriel Mance (const $ card $ Pred_name pn)

3e0eb79b52a3078a12531efc3f66d0d94fd9938dFelix Gabriel Mance (resultToMaybe $

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance minDLForm sign $ card $ Pred_name pn)

15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance

15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance simp = rmTypesT minDLForm simplifyCD sign

e5e3f128bbd44dd393e1038718038bd323f5e415Felix Gabriel Mance

dda7065c0c0f383558d7d4e8072969c8c41a8ed7Francisc Nicolae Bungiu card psy = Cardinality ct psy (simp t1) (simp t2)

15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance (case t3 of

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance Nothing -> Nothing

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance Just x -> Just $ simp x

dda7065c0c0f383558d7d4e8072969c8c41a8ed7Francisc Nicolae Bungiu )r

734257b9ea9fcaa18d4e3627f54f5295a99aa1f7Felix Gabriel Mance

c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance pn = case ps of

30e9cf458094e5970bc06be667558961c2eccff4Felix Gabriel Mance Pred_name n -> n

12078a24d49ba36b83cda9d07c8e8a480c493fe8Felix Gabriel Mance Qual_pred_name n _pType _ -> n

12078a24d49ba36b83cda9d07c8e8a480c493fe8Felix Gabriel Mance

12078a24d49ba36b83cda9d07c8e8a480c493fe8Felix Gabriel Mance

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

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 () isSubCASL_DLSign diffCASL_DLSign

cogenerated_sign CASL_DL = cogeneratedSign ()

generated_sign CASL_DL = generatedSign ()

induced_from_morphism CASL_DL = inducedFromMorphism ()

induced_from_to_morphism CASL_DL =

inducedFromToMorphism () isSubCASL_DLSign diffCASL_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 _ = ()