Logic_CASL_DL.hs revision 34bff097c14521b5e57ce37279a34256e1f78aa5
5394N/A{- |
5394N/AModule : $Header$
5394N/ACopyright : (c) Klaus L�ttich, Uni Bremen 2005
5394N/ALicense : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
5394N/A
5394N/AMaintainer : luecke@informatik.uni-bremen.de
5394N/AStability : provisional
5394N/APortability : portable
5394N/A
5394N/AInstance of class Logic for CASL DL
5394N/A-}
5394N/A
5394N/Amodule CASL_DL.Logic_CASL_DL (CASL_DL(..), DLMor, DLFORMULA) where
5394N/A
5394N/Aimport Common.Result
5394N/Aimport qualified Data.Set as Set
5394N/Aimport qualified Common.Lib.Rel as Rel
5394N/A
5394N/Aimport CASL_DL.AS_CASL_DL
5394N/Aimport CASL_DL.Sign
5394N/Aimport CASL_DL.PredefinedSign
5394N/Aimport CASL_DL.ATC_CASL_DL ()
5394N/Aimport CASL_DL.Parse_AS ()
5394N/Aimport CASL_DL.StatAna
6238N/A
5394N/Aimport CASL.Sign
5394N/Aimport CASL.Morphism
5394N/Aimport CASL.SymbolMapAnalysis
5394N/Aimport CASL.Logic_CASL
5394N/Aimport CASL.AS_Basic_CASL
5394N/Aimport CASL.Parse_AS_Basic
5394N/Aimport CASL.MapSentence
5394N/Aimport CASL.SymbolParser
5394N/Aimport CASL.Taxonomy
5394N/Aimport CASL.SimplifySen
5394N/A
5394N/Aimport Logic.Logic
5394N/A
5394N/Adata CASL_DL = CASL_DL deriving Show
5394N/A
5394N/Ainstance Language CASL_DL where
5394N/A description _ =
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/A \ * DL -- SHOIN(D)\n\
5394N/A \ * SHIQ\n\
5394N/A \ * SHOIQ\n"
5714N/A
5394N/Atype DLMor = Morphism DL_FORMULA CASL_DLSign ()
5394N/Atype DLFORMULA = FORMULA DL_FORMULA
5394N/A
5394N/Ainstance Category CASL_DL DLSign DLMor
5394N/A where
5394N/A -- ide :: id -> object -> morphism
5394N/A ide CASL_DL = idMor dummy
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 dom CASL_DL = msource
5394N/A cod CASL_DL = mtarget
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
5394N/A-- abstract syntax, parsing (and printing)
5394N/A
5394N/Ainstance Syntax CASL_DL DL_BASIC_SPEC
6238N/A SYMB_ITEMS SYMB_MAP_ITEMS
5947N/A where
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/A
5947N/A-- CASL_DL logic
5947N/A
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 varT' = mapTrm varT
5947N/A natT' = mapTrm natT
5947N/A mapTrm = mapTerm map_DL_FORMULA mor
5947N/A
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 sym_of CASL_DL = symOf
5394N/A symmap_of CASL_DL = morphismToSymbMap
5395N/A sym_name CASL_DL = symName
5394N/A simplify_sen CASL_DL = simplifySen minDLForm simplifyCD
5394N/A
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)
5947N/A (resultToMaybe $
5394N/A minDLForm sign $ card $ Pred_name pn)
5394N/A
5394N/A simp = rmTypesT minDLForm simplifyCD sign
5394N/A
5394N/A card psy = Cardinality ct psy (simp t1) (simp t2) r
5394N/A
5394N/A pn = case ps of
5394N/A Pred_name n -> n
5394N/A Qual_pred_name n _pType _ -> n
5394N/A
5394N/A
5394N/Ainstance StaticAnalysis CASL_DL DL_BASIC_SPEC DLFORMULA
5394N/A SYMB_ITEMS SYMB_MAP_ITEMS
5394N/A DLSign
5394N/A DLMor
5394N/A Symbol RawSymbol where
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" -- ???
5394N/A
5457N/A sign_to_basic_spec CASL_DL _sigma _sens = Basic_spec [] -- ???
5394N/A
5394N/A symbol_to_raw CASL_DL = symbolToRaw
5394N/A id_to_raw CASL_DL = idToRaw
5423N/A matches CASL_DL = CASL.Morphism.matches
5947N/A
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
5454N/A
5423N/A-- |
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}
5454N/A where addThing r = Rel.union r (Rel.fromSet
5454N/A $ Set.map (\ x -> (x,topSort))
5423N/A $ sortSet sig)
5423N/A
5423N/Ainstance Logic CASL_DL ()
5443N/A DL_BASIC_SPEC DLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
5443N/A DLSign
5423N/A DLMor
5423N/A Symbol RawSymbol () where
5423N/A stability _ = Unstable
5423N/A empty_proof_tree _ = ()
5423N/A