diff --git a/CASL_DL/PredefinedCASLAxioms.hs b/CASL_DL/PredefinedCASLAxioms.hs index da657bebc4..8e90d94510 100644 --- a/CASL_DL/PredefinedCASLAxioms.hs +++ b/CASL_DL/PredefinedCASLAxioms.hs @@ -13,6 +13,8 @@ Portability : portable module CASL_DL.PredefinedCASLAxioms ( predefSign , predefinedSign + , predefSign2 + , datatypeSigns , thing , nothing , conceptPred @@ -52,6 +54,8 @@ import Common.GlobalAnnotations import qualified Common.Lib.Rel as Rel import qualified Common.Lib.MapSet as MapSet +import qualified Data.Map as Map + import Data.Char hetsPrefix :: String @@ -231,6 +235,53 @@ noThing = Qual_pred_name nothing classPredType n intTypes :: [PredType] intTypes = map (\ t -> PredType [t]) [integer, nonNegInt] +predefinedSign2 :: e -> Sign f e +predefinedSign2 e = (emptySign e) { + sortRel = Rel.insertKey thing $ Rel.insertKey dataS Rel.empty + } + +predefSign2 :: CASLSign +predefSign2 = predefinedSign2 () + +-- | instead of one big signature, several small ones + +charSign :: CASLSign +charSign = (emptySign ()) + { sortRel = Rel.insertKey (stringToId "Char") Rel.empty + , opMap = MapSet.fromList + $ map (\ c -> (charToId c, [charT])) + [chr 0 .. chr 127] + } + +integerSign :: CASLSign +integerSign = (emptySign ()) + { sortRel = + Rel.transClosure $ Rel.fromList + [(negIntS, nonPosInt), + (nonNegInt, integer), + (nonPosInt, integer), + (posInt, nonNegInt), + (integer, dataS)] + , predMap = + MapSet.fromList + $ + map ( \ o -> (stringToId o, intTypes)) + ["even", "odd"] + , opMap = MapSet.fromList + $ map (\ i -> (stringToId $ show i, [natT])) + [0 .. 9 :: Int] + ++ + [ + (atAt, [atAtTy]) + ] + , globAnnos = emptyGlobalAnnos + { literal_annos = emptyLiteralAnnos + { number_lit = Just atAt + }} + } + + + predefinedSign :: e -> Sign f e predefinedSign e = (emptySign e) { sortRel = Rel.insertKey (stringToId "Char") @@ -273,6 +324,67 @@ predefinedSign e = (emptySign e) , string_lit = Just (emptyString, cons) }} } +floatSign :: CASLSign +floatSign = integerSign + { sortRel = Rel.union (sortRel integerSign) + $ Rel.transClosure $ Rel.fromList + [ + (integer, float), + (float, dataS) + ] + + , opMap = MapSet.union (opMap integerSign) $ MapSet.fromList + $ + [ + (unMinus, [minusTy, minusFloat]) + , (dec, [decTy]) + , (eId, [expTy]) + ] + , globAnnos = (globAnnos integerSign) + { literal_annos = (literal_annos $ globAnnos integerSign) + { float_lit = Just (dec, eId) + }} + } + +boolSign :: CASLSign +boolSign = (emptySign ()) + { sortRel = Rel.transClosure $ Rel.fromList + [(boolS, dataS)] + , opMap = MapSet.fromList + $ + [ (trueS, [boolT]) + , (falseS, [boolT]) + ] + } + +stringSignAux :: CASLSign +stringSignAux = (emptySign ()) + { sortRel = + Rel.transClosure $ Rel.fromList + [ (stringS, dataS) ] + , opMap = MapSet.fromList + $ + [ + (emptyString, [emptyStringTy]) + , (cons, [consTy]) + ] + , globAnnos = emptyGlobalAnnos + { literal_annos = emptyLiteralAnnos + { + string_lit = Just (emptyString, cons) }} + } + +stringSign :: CASLSign +stringSign = uniteCASLSign stringSignAux charSign + +datatypeSigns :: Map.Map SORT CASLSign +datatypeSigns = Map.fromList + [ (charS, charSign) + , (integer, integerSign) + , (float, floatSign) + , (boolS, boolSign) + , (stringS, stringSign)] + predefSign :: CASLSign predefSign = predefinedSign () @@ -287,7 +399,7 @@ predefinedAxioms = let mkNNameAux :: Int -> String mkNNameAux k = genNamePrefix ++ "x" ++ show k - + -- | Build a name mkNName :: Int -> Token mkNName i = mkSimpleId $ hetsPrefix ++ mkNNameAux i diff --git a/Logic/Logic.hs b/Logic/Logic.hs index 67a1859115..74937c5432 100644 --- a/Logic/Logic.hs +++ b/Logic/Logic.hs @@ -395,14 +395,14 @@ symset_of :: forall lid sentence sign morphism symbol . symset_of lid sig = Set.unions $ sym_of lid sig -- | check that all sentence names in a theory do not appear as symbol names -checkSenNames :: forall lid sentence sign morphism symbol . +checkSenNames :: forall lid sentence sign morphism symbol . Sentences lid sentence sign morphism symbol => lid -> sign -> [Named sentence] -> Set.Set String -checkSenNames lid aSig nsens = +checkSenNames lid aSig nsens = let senNames = map senAttr nsens symNames = map (show . (sym_name lid)) $ Set.toList $ symset_of lid aSig - in Set.intersection (Set.fromList symNames) $ Set.fromList senNames + in Set.intersection (Set.fromList symNames) $ Set.fromList senNames -- | dependency ordered list of symbols for a signature symlist_of :: forall lid sentence sign morphism symbol . @@ -627,7 +627,7 @@ class ( Syntax lid basic_spec symbol symb_items symb_map_items equiv2cospan :: lid -> sign -> sign -> [symb_items] -> [symb_items] -> Result (sign, sign, sign, EndoMap symbol, EndoMap symbol) equiv2cospan _ _ _ _ _ = error "equiv2cospan nyi" - -- | extract the module + -- | extract the module extract_module :: lid -> [IRI] -> (sign, [Named sentence]) -> Result (sign, [Named sentence]) extract_module _ _ = return @@ -850,6 +850,17 @@ class (StaticAnalysis lid -- no logic should throw an error here addOmdocToTheory _ _ t _ = return t + +-- | sublogic of a theory +sublogicOfTheo :: (Logic lid sublogics + basic_spec sentence symb_items symb_map_items + sign morphism symbol raw_symbol proof_tree) => + lid -> (sign, [sentence]) -> sublogics +sublogicOfTheo _ (sig, axs) = + foldl lub (minSublogic sig) $ + map minSublogic axs + + {- The class of logics which can be used as logical frameworks, in which object logics can be specified by the user. Currently the only logics implementing this class are LF, Maude, and Isabelle, with the latter two only having diff --git a/OWL2/OWL22CASL.hs b/OWL2/OWL22CASL.hs index f3ab7aea35..0f342d4ec5 100644 --- a/OWL2/OWL22CASL.hs +++ b/OWL2/OWL22CASL.hs @@ -39,6 +39,7 @@ import OWL2.ManchesterPrint () import OWL2.Morphism import OWL2.Symbols import qualified OWL2.Sign as OS +import qualified OWL2.Sublogic as SL -- CASL_DL = codomain import CASL.Logic_CASL import CASL.AS_Basic_CASL @@ -122,13 +123,13 @@ uriToCaslId urI = let in if ((isDatatypeKey urI) && (isThing urI)) then getId $ localPart urI - else + else {- let ePart = expandedIRI urI in if ePart /= "" then getId $ expandedIRI urI - else + else -} getId $ localPart urI tokDecl :: Token -> VAR_DECL @@ -252,27 +253,35 @@ mapSign sig = [ tMp conceptPred cPreds , tMp objectPropPred oPreds , tMp dataPropPred dPreds ] - in return $ uniteCASLSign predefSign (emptySign ()) + in return $ uniteCASLSign predefSign2 + (emptySign ()) { predMap = aPreds , opMap = tMp indiConst . cvrt $ OS.individuals sig } -loadDataInformation :: ProfSub -> Sign f () -loadDataInformation _ = let dts = Set.fromList $ map stringToId datatypeKeys - in (emptySign ()) { sortRel = Rel.fromKeysSet dts } +loadDataInformation :: ProfSub -> CASLSign +loadDataInformation sl = let + dts = Set.map uriToCaslId $ SL.datatype $ sublogic sl + eSig x = (emptySign ()) { sortRel = + Rel.fromList [(x, dataS)]} + sigs = Set.toList $ + Set.map (\x -> Map.findWithDefault (eSig x) x datatypeSigns) dts + in foldl uniteCASLSign (emptySign ()) sigs mapTheory :: (OS.Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA]) -mapTheory (owlSig, owlSens) = let sl = topS in do +mapTheory (owlSig, owlSens) = let + sl = sublogicOfTheo OWL2 (owlSig, map sentence owlSens) + in do cSig <- mapSign owlSig let pSig = loadDataInformation sl - dTypes = (emptySign ()) {sortRel = Rel.transClosure . Rel.fromSet + {- dTypes = (emptySign ()) {sortRel = Rel.transClosure . Rel.fromSet . Set.map (\ d -> (uriToCaslId d, dataS)) - . Set.union predefIRIs $ OS.datatypes owlSig} + . Set.union predefIRIs $ OS.datatypes owlSig} -} (cSens, nSig) <- foldM (\ (x, y) z -> do (sen, sig) <- mapSentence y z return (sen ++ x, uniteCASLSign sig y)) ([], cSig) owlSens - return (foldl1 uniteCASLSign [nSig, pSig, dTypes], - predefinedAxioms ++ (reverse cSens)) + return (foldl1 uniteCASLSign [nSig, pSig], -- , dTypes], + predefinedAxioms ++ (reverse cSens)) -- | mapping of OWL to CASL_DL formulae mapSentence :: CASLSign -> Named Axiom -> Result ([Named CASLFORMULA], CASLSign) @@ -640,6 +649,17 @@ mkEDPairs s il mr pairs = do _ -> error "expected EDRelation") pairs return (ls, s) +mkEDPairs' :: CASLSign -> [Int] -> Maybe O.Relation -> [(FORMULA f, FORMULA f)] + -> Result ([FORMULA f], CASLSign) +mkEDPairs' s [i1, i2] mr pairs = do + let ls = map (\ (x, y) -> mkVDecl [i1] $ mkVDataDecl [i2] + $ case fromMaybe (error "expected EDRelation") mr of + EDRelation Equivalent -> mkEqv x y + EDRelation Disjoint -> mkNC [x, y] + _ -> error "expected EDRelation") pairs + return (ls, s) +mkEDPairs' _ _ _ _ = error "wrong call of mkEDPairs'" + -- | Mapping of ListFrameBit mapListFrameBit :: CASLSign -> Extended -> Maybe O.Relation -> ListFrameBit -> Result ([CASLFORMULA], CASLSign) @@ -716,16 +736,16 @@ mapListFrameBit cSig ex rel lfb = Just r -> case ex of Misc _ -> do pairs <- mapComDataPropsList cSig Nothing dl 1 2 - mkEDPairs cSig [1, 2] rel pairs + mkEDPairs' cSig [1, 2] rel pairs SimpleEntity (Entity _ DataProperty iri) -> case r of SubPropertyOf -> do os1 <- mapM (\ o1 -> mapDataProp cSig o1 1 2) dl - o2 <- mapDataProp cSig iri 2 1 + o2 <- mapDataProp cSig iri 1 2 -- was 2 1 return (map (mkForall [thingDecl 1, dataDecl 2] . mkImpl o2) os1, cSig) EDRelation _ -> do pairs <- mapComDataPropsList cSig (Just iri) dl 1 2 - mkEDPairs cSig [1, 2] rel pairs + mkEDPairs' cSig [1, 2] rel pairs _ -> return ([], cSig) _ -> err IndividualSameOrDifferent al -> case rel of