From 792866245d2a07619868b9a207c84cfd894cf054 Mon Sep 17 00:00:00 2001 From: mcodescu Date: Sun, 14 Aug 2016 13:43:06 +0200 Subject: [PATCH 1/8] almost no datatypes for now --- CASL_DL/PredefinedCASLAxioms.hs | 11 ++++++++++- Logic/Logic.hs | 19 +++++++++++++++---- OWL2/OWL22CASL.hs | 29 +++++++++++++++++++---------- 3 files changed, 44 insertions(+), 15 deletions(-) diff --git a/CASL_DL/PredefinedCASLAxioms.hs b/CASL_DL/PredefinedCASLAxioms.hs index da657bebc4..6db96a9395 100644 --- a/CASL_DL/PredefinedCASLAxioms.hs +++ b/CASL_DL/PredefinedCASLAxioms.hs @@ -13,6 +13,7 @@ Portability : portable module CASL_DL.PredefinedCASLAxioms ( predefSign , predefinedSign + , predefSign2 , thing , nothing , conceptPred @@ -231,6 +232,14 @@ 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 () + predefinedSign :: e -> Sign f e predefinedSign e = (emptySign e) { sortRel = Rel.insertKey (stringToId "Char") @@ -287,7 +296,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..4e384f3046 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 sl = let + dts = Set.map uriToCaslId $ SL.datatype $ sublogic sl + in (emptySign ()) { sortRel = + Rel.transClosure . Rel.fromSet . + Set.map (\ d -> (d, dataS)) + $ dts } 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], + reverse cSens) + -- predefinedAxioms ++ (reverse cSens)) -- | mapping of OWL to CASL_DL formulae mapSentence :: CASLSign -> Named Axiom -> Result ([Named CASLFORMULA], CASLSign) From cbf18ccbf3ad68bda986ef38192362a1b1c6d4c1 Mon Sep 17 00:00:00 2001 From: mcodescu Date: Sun, 14 Aug 2016 14:23:45 +0200 Subject: [PATCH 2/8] nicer names via translation --- OWL2/OWL22CASL.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/OWL2/OWL22CASL.hs b/OWL2/OWL22CASL.hs index 4e384f3046..9771b1727f 100644 --- a/OWL2/OWL22CASL.hs +++ b/OWL2/OWL22CASL.hs @@ -123,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 From 006ed46f1e5892ef5dd031f1a691b6414ba72af9 Mon Sep 17 00:00:00 2001 From: mcodescu Date: Sun, 14 Aug 2016 17:00:08 +0200 Subject: [PATCH 3/8] added back the predefined axioms --- OWL2/OWL22CASL.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/OWL2/OWL22CASL.hs b/OWL2/OWL22CASL.hs index 9771b1727f..4e2791dd95 100644 --- a/OWL2/OWL22CASL.hs +++ b/OWL2/OWL22CASL.hs @@ -280,8 +280,7 @@ mapTheory (owlSig, owlSens) = let (sen, sig) <- mapSentence y z return (sen ++ x, uniteCASLSign sig y)) ([], cSig) owlSens return (foldl1 uniteCASLSign [nSig, pSig], -- , dTypes], - reverse cSens) - -- predefinedAxioms ++ (reverse cSens)) + predefinedAxioms ++ (reverse cSens)) -- | mapping of OWL to CASL_DL formulae mapSentence :: CASLSign -> Named Axiom -> Result ([Named CASLFORMULA], CASLSign) From ab197492a2668a2fdf1d188b43076264d497c19a Mon Sep 17 00:00:00 2001 From: mcodescu Date: Sun, 14 Aug 2016 21:21:51 +0200 Subject: [PATCH 4/8] split signatures of datatypes --- CASL_DL/PredefinedCASLAxioms.hs | 100 ++++++++++++++++++++++++++++++++ OWL2/OWL22CASL.hs | 11 ++-- 2 files changed, 106 insertions(+), 5 deletions(-) diff --git a/CASL_DL/PredefinedCASLAxioms.hs b/CASL_DL/PredefinedCASLAxioms.hs index 6db96a9395..110625e43e 100644 --- a/CASL_DL/PredefinedCASLAxioms.hs +++ b/CASL_DL/PredefinedCASLAxioms.hs @@ -14,6 +14,7 @@ module CASL_DL.PredefinedCASLAxioms ( predefSign , predefinedSign , predefSign2 + , datatypeSigns , thing , nothing , conceptPred @@ -53,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 @@ -240,6 +243,45 @@ predefinedSign2 e = (emptySign e) { 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") @@ -282,6 +324,64 @@ 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]) + , (cons, [consTy]) + ] + , 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]) + ] + } + +stringSign :: CASLSign +stringSign = (emptySign ()) + { sortRel = + Rel.transClosure $ Rel.fromList + [ (stringS, dataS) ] + , opMap = MapSet.fromList + $ + [ + (emptyString, [emptyStringTy]) + ] + , globAnnos = emptyGlobalAnnos + { literal_annos = emptyLiteralAnnos + { + string_lit = Just (emptyString, cons) }} + } + +datatypeSigns :: Map.Map SORT CASLSign +datatypeSigns = Map.fromList + [ (charS, charSign) + , (integer, integerSign) + , (float, floatSign) + , (boolS, boolSign) + , (stringS, stringSign)] + predefSign :: CASLSign predefSign = predefinedSign () diff --git a/OWL2/OWL22CASL.hs b/OWL2/OWL22CASL.hs index 4e2791dd95..c9a8bec220 100644 --- a/OWL2/OWL22CASL.hs +++ b/OWL2/OWL22CASL.hs @@ -259,13 +259,14 @@ mapSign sig = , opMap = tMp indiConst . cvrt $ OS.individuals sig } -loadDataInformation :: ProfSub -> Sign f () +loadDataInformation :: ProfSub -> CASLSign loadDataInformation sl = let dts = Set.map uriToCaslId $ SL.datatype $ sublogic sl - in (emptySign ()) { sortRel = - Rel.transClosure . Rel.fromSet . - Set.map (\ d -> (d, dataS)) - $ dts } + 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 From 2c5c007c8f164dce4a11b5e28d56405bb29fd182 Mon Sep 17 00:00:00 2001 From: mcodescu Date: Sun, 14 Aug 2016 22:12:52 +0200 Subject: [PATCH 5/8] put the char cons in char sign --- CASL_DL/PredefinedCASLAxioms.hs | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/CASL_DL/PredefinedCASLAxioms.hs b/CASL_DL/PredefinedCASLAxioms.hs index 110625e43e..8e90d94510 100644 --- a/CASL_DL/PredefinedCASLAxioms.hs +++ b/CASL_DL/PredefinedCASLAxioms.hs @@ -339,7 +339,6 @@ floatSign = integerSign (unMinus, [minusTy, minusFloat]) , (dec, [decTy]) , (eId, [expTy]) - , (cons, [consTy]) ] , globAnnos = (globAnnos integerSign) { literal_annos = (literal_annos $ globAnnos integerSign) @@ -358,8 +357,8 @@ boolSign = (emptySign ()) ] } -stringSign :: CASLSign -stringSign = (emptySign ()) +stringSignAux :: CASLSign +stringSignAux = (emptySign ()) { sortRel = Rel.transClosure $ Rel.fromList [ (stringS, dataS) ] @@ -367,6 +366,7 @@ stringSign = (emptySign ()) $ [ (emptyString, [emptyStringTy]) + , (cons, [consTy]) ] , globAnnos = emptyGlobalAnnos { literal_annos = emptyLiteralAnnos @@ -374,6 +374,9 @@ stringSign = (emptySign ()) string_lit = Just (emptyString, cons) }} } +stringSign :: CASLSign +stringSign = uniteCASLSign stringSignAux charSign + datatypeSigns :: Map.Map SORT CASLSign datatypeSigns = Map.fromList [ (charS, charSign) From b976101276ba712d070f53c40a90c03f94331a90 Mon Sep 17 00:00:00 2001 From: mcodescu Date: Sun, 14 Aug 2016 22:33:46 +0200 Subject: [PATCH 6/8] quickfix for data properties --- OWL2/OWL22CASL.hs | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/OWL2/OWL22CASL.hs b/OWL2/OWL22CASL.hs index c9a8bec220..a6c10d37fb 100644 --- a/OWL2/OWL22CASL.hs +++ b/OWL2/OWL22CASL.hs @@ -264,7 +264,7 @@ loadDataInformation sl = let dts = Set.map uriToCaslId $ SL.datatype $ sublogic sl eSig x = (emptySign ()) { sortRel = Rel.fromList [(x, dataS)]} - sigs = Set.toList $ + sigs = Set.toList $ Set.map (\x -> Map.findWithDefault (eSig x) x datatypeSigns) dts in foldl uniteCASLSign (emptySign ()) sigs @@ -649,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) @@ -734,7 +745,7 @@ mapListFrameBit cSig ex rel lfb = . 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 @@ -827,6 +838,6 @@ mapKey cSig ce pl npl p i h = do $ mkExist (keyDecl h i) $ conjunct $ pl ++ [un], s) mapAxioms :: CASLSign -> Axiom -> Result ([CASLFORMULA], CASLSign) -mapAxioms cSig (PlainAxiom ex fb) = case fb of +mapAxioms cSig ax@(PlainAxiom ex fb) = case fb of ListFrameBit rel lfb -> mapListFrameBit cSig ex rel lfb AnnFrameBit ans afb -> mapAnnFrameBit cSig ex ans afb From 4eeb7bc70856f8e18b175908c5f6d63fb6324143 Mon Sep 17 00:00:00 2001 From: mcodescu Date: Sun, 14 Aug 2016 22:39:45 +0200 Subject: [PATCH 7/8] more data vars --- OWL2/OWL22CASL.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/OWL2/OWL22CASL.hs b/OWL2/OWL22CASL.hs index a6c10d37fb..46ba0583d0 100644 --- a/OWL2/OWL22CASL.hs +++ b/OWL2/OWL22CASL.hs @@ -736,7 +736,7 @@ 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 From 141e21396e265245fe0af6c2b4415b27ea61386f Mon Sep 17 00:00:00 2001 From: mcodescu Date: Sun, 14 Aug 2016 22:45:47 +0200 Subject: [PATCH 8/8] subpropertyof for data properties --- OWL2/OWL22CASL.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/OWL2/OWL22CASL.hs b/OWL2/OWL22CASL.hs index 46ba0583d0..0f342d4ec5 100644 --- a/OWL2/OWL22CASL.hs +++ b/OWL2/OWL22CASL.hs @@ -740,7 +740,7 @@ mapListFrameBit cSig ex rel lfb = 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 @@ -838,6 +838,6 @@ mapKey cSig ce pl npl p i h = do $ mkExist (keyDecl h i) $ conjunct $ pl ++ [un], s) mapAxioms :: CASLSign -> Axiom -> Result ([CASLFORMULA], CASLSign) -mapAxioms cSig ax@(PlainAxiom ex fb) = case fb of +mapAxioms cSig (PlainAxiom ex fb) = case fb of ListFrameBit rel lfb -> mapListFrameBit cSig ex rel lfb AnnFrameBit ans afb -> mapAnnFrameBit cSig ex ans afb