5394N/ACopyright : (c) Klaus L�ttich, Uni Bremen 2005
5394N/AMaintainer : luecke@informatik.uni-bremen.de
5394N/AInstance of class Logic for CASL DL
5394N/Adata CASL_DL = CASL_DL deriving Show
5394N/Ainstance Language CASL_DL where
5394N/A "CASL_DL is at the same time an extension and a restriction of CASL.\n\
5394N/A \It additionally provides cardinality restrictions in a description logic\n\
5394N/A \sense; and it limits the expressivity of CASL to the description logic\n\
5394N/A \SHOIN(D). Hence it provides the following sublogics: \n\
5394N/A \ * Card -- CASL plus cardinality restrictions on binary relations\n\
5394N/Atype DLMor = Morphism DL_FORMULA CASL_DLSign ()
5394N/Atype DLFORMULA = FORMULA DL_FORMULA
5394N/Ainstance Category CASL_DL DLSign DLMor
5394N/A -- ide :: id -> object -> morphism
5394N/A -- comp :: id -> morphism -> morphism -> Maybe morphism
5394N/A comp CASL_DL = compose (const id)
5394N/A -- dom, cod :: id -> morphism -> object
5394N/A -- legal_obj :: id -> object -> Bool
5394N/A legal_obj CASL_DL = legalSign
5394N/A -- legal_mor :: id -> morphism -> Bool
5394N/A legal_mor CASL_DL = legalMor
5394N/A-- abstract syntax, parsing (and printing)
5394N/Ainstance Syntax CASL_DL DL_BASIC_SPEC
5947N/A parse_basic_spec CASL_DL = Just $ basicSpec casl_DL_reserved_words
5947N/A parse_symb_items CASL_DL = Just $ symbItems casl_DL_reserved_words
5947N/A parse_symb_map_items CASL_DL =
5947N/A Just $ symbMapItems casl_DL_reserved_words
5947N/Amap_DL_FORMULA :: MapSen DL_FORMULA CASL_DLSign ()
5947N/Amap_DL_FORMULA mor (Cardinality ct pn varT natT r) =
5947N/A Cardinality ct pn' varT' natT' r
5947N/A where pn' = mapPrSymb mor pn
5947N/A mapTrm = mapTerm map_DL_FORMULA mor
5947N/Ainstance Sentences CASL_DL DLFORMULA DLSign DLMor Symbol where
5947N/A map_sen CASL_DL m = return . mapSen map_DL_FORMULA m
5947N/A parse_sentence CASL_DL = Nothing
5394N/A symmap_of CASL_DL = morphismToSymbMap
5394N/A simplify_sen CASL_DL = simplifySen minDLForm simplifyCD
5394N/AsimplifyCD :: DLSign -> DL_FORMULA -> DL_FORMULA
5394N/AsimplifyCD sign (Cardinality ct ps t1 t2 r) = simpCard
5394N/A where simpCard = maybe (card ps)
5394N/A (const $ card $ Pred_name pn)
5394N/A minDLForm sign $ card $ Pred_name pn)
5394N/A simp = rmTypesT minDLForm simplifyCD sign
5394N/A card psy = Cardinality ct psy (simp t1) (simp t2) r
5394N/A Qual_pred_name n _pType _ -> n
5394N/Ainstance StaticAnalysis CASL_DL DL_BASIC_SPEC DLFORMULA
5394N/A basic_analysis CASL_DL = Just $ basicCASL_DLAnalysis
5394N/A stat_symb_map_items CASL_DL sml =
5394N/A statSymbMapItems sml >>= checkSymbolMapDL
5394N/A stat_symb_items CASL_DL = statSymbItems
5394N/A ensures_amalgamability CASL_DL _ =
5394N/A fail "CASL_DL: ensures_amalgamability nyi" -- ???
5457N/A sign_to_basic_spec CASL_DL _sigma _sens = Basic_spec [] -- ???
5394N/A symbol_to_raw CASL_DL = symbolToRaw
5394N/A id_to_raw CASL_DL = idToRaw
5947N/A empty_signature CASL_DL = emptySign emptyCASL_DLSign
5947N/A signature_union CASL_DL s = return . addSig addCASL_DLSign s
5947N/A signature_difference CASL_DL s = return . diffSig diffCASL_DLSign s
5947N/A morphism_union CASL_DL = morphismUnion (const id) addCASL_DLSign
5947N/A final_union CASL_DL = finalUnion addCASL_DLSign
5947N/A is_subsig CASL_DL = isSubSig isSubCASL_DLSign
5947N/A inclusion CASL_DL = sigInclusion dummy isSubCASL_DLSign
5947N/A cogenerated_sign CASL_DL = cogeneratedSign dummy
5947N/A generated_sign CASL_DL = generatedSign dummy
5947N/A induced_from_morphism CASL_DL = inducedFromMorphism dummy
5947N/A induced_from_to_morphism CASL_DL =
5443N/A inducedFromToMorphism dummy isSubCASL_DLSign
5423N/A theory_to_taxonomy CASL_DL tgk mo sig sen =
5423N/A convTaxo tgk mo (extendSortRelWithTopSort sig) sen
5423N/A-- extend the sort relation with sort Thing for the taxonomy display
5454N/AextendSortRelWithTopSort :: Sign f e -> Sign f e
5454N/AextendSortRelWithTopSort sig = sig {sortRel = addThing $ sortRel sig}
5443N/A DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS