diff --git a/Common/AnnoParser.hs b/Common/AnnoParser.hs index ee370a39a8..7f027fbd7e 100644 --- a/Common/AnnoParser.hs +++ b/Common/AnnoParser.hs @@ -237,7 +237,7 @@ floatingAnno ps = literal2idsAnno ps Float_anno prefixAnno :: Range -> GenParser Char st Annotation prefixAnno ps = do - prefixes <- many $ do + prefixes <- many $ skipMany (commentLine >> spaces) >> do p <- (string colonS >> return "") <|> (IRI.ncname << string colonS) spaces diff --git a/Common/Keywords.hs b/Common/Keywords.hs index 4459e6e2f2..8fcb98bee5 100644 --- a/Common/Keywords.hs +++ b/Common/Keywords.hs @@ -309,6 +309,9 @@ interpretationS = "interpretation" moduleS :: String moduleS = "module" +omsS :: String +omsS = "oms" + ontologyS :: String ontologyS = "ontology" @@ -504,6 +507,9 @@ intersectS = "intersect" lambdaS :: String lambdaS = "lambda" +languageS :: String +languageS = "language" + left_assocS :: String left_assocS = "left_assoc" diff --git a/Common/Token.hs b/Common/Token.hs index 2c1e243b41..ad240f6ef1 100644 --- a/Common/Token.hs +++ b/Common/Token.hs @@ -112,15 +112,15 @@ criticalKeywords = terminatingKeywords ++ startingKeywords -- | keywords terminating a basic spec terminatingKeywords :: [String] terminatingKeywords = - [ andS, endS, extractS, fitS, forgetS, hideS, keepS, rejectS, removeS, + [ andS, endS, extractS, fitS, forgetS, hideS, keepS, rejectS, removeS, revealS, selectS, thenS, withS, withinS, ofS, forS, toS, intersectS] -- | keywords starting a library item startingKeywords :: [String] startingKeywords = - [ archS, fromS, logicS, newlogicS, refinementS, specS, unitS, viewS - , ontologyS, alignmentS, networkS, equivalenceS, newcomorphismS - , interpretationS, entailmentS ] + [ archS, fromS, languageS, logicS, newlogicS, refinementS, specS, unitS + , viewS , omsS, ontologyS, alignmentS, networkS, equivalenceS + , newcomorphismS , interpretationS, entailmentS ] -- | keywords that may follow a defining equal sign otherStartKeywords :: [String] diff --git a/Logic/KnownIris.hs b/Logic/KnownIris.hs index 2e16aa8aee..a22430cf16 100644 --- a/Logic/KnownIris.hs +++ b/Logic/KnownIris.hs @@ -16,18 +16,37 @@ import qualified Data.Map as Map logPrefix, serPrefix :: String -logPrefix = "http://purl.net/dol/logics/" -serPrefix = "http://purl.net/dol/serializations/" +logPrefix = "http://purl.net/DOL/logics/" +serPrefix = "http://purl.net/DOL/serializations/" +lngPrefix = "http://purl.net/DOL/languages/" +trlPrefix = "http://purl.net/DOL/translations/" logicNames :: Map.Map String String logicNames = -- IRI -> local name Map.fromList [ (logPrefix ++ "CommonLogic", "CommonLogic"), + -- TODO: Properly support `language` declarations + -- Everything up to the `logPrefix` lines below is part of a hack to + -- support `translation` declarations and `language` declarations without + -- an accompanying `logic` declaration by essentially treating `language` + -- the same as `logic`. + -- This should probably be done properly instead, but it works for now. + (lngPrefix ++ "CASL", "CASL"), + (lngPrefix ++ "CommonLogic", "CommonLogic"), + (lngPrefix ++ "HasCASL", "HasCASL"), + (lngPrefix ++ "Propositional", "Propositional"), + (lngPrefix ++ "OWL", "OWL"), + (lngPrefix ++ "OWL2", "OWL"), + (trlPrefix ++ "SROIQtoCL", "OWL22CommonLogic"), + (trlPrefix ++ "PropositionalToSROIQ", "Propositional2OWL2"), (logPrefix ++ "Propositional", "Propositional"), - (logPrefix ++ "OWL2", "OWL") ] + (logPrefix ++ "OWL2", "OWL"), + (logPrefix ++ "SROIQ", "OWL")] -- should be "NP-sROIQ-D|-|" + -- (or "OWL.NP-sROIQ-D|-|"?) instead of + -- "OWL" but Hets claims not to kow both. lookupLogicName :: String -> Maybe String -lookupLogicName = (`Map.lookup` logicNames) +lookupLogicName = (`Map.lookup` logicNames) . filter (not . (`elem` "<>")) serializations :: String -> Map.Map String String serializations l @@ -41,4 +60,5 @@ serializations l | otherwise = Map.empty lookupSerialization :: String -> String -> Maybe String -lookupSerialization l = (`Map.lookup` serializations l) +lookupSerialization l = (`Map.lookup` serializations l) . + filter (not . (`elem` "<>")) diff --git a/OWL2/Keywords.hs b/OWL2/Keywords.hs index 767e804b68..158c311607 100644 --- a/OWL2/Keywords.hs +++ b/OWL2/Keywords.hs @@ -15,7 +15,7 @@ plus owl, xsd, rdf and rdfs reserved keywords. All identifiers are mixed case module OWL2.Keywords where -import Common.Keywords +import Common.Keywords hiding (languageS) keywords :: [String] keywords = diff --git a/Syntax/Parse_AS_Library.hs b/Syntax/Parse_AS_Library.hs index 8eae3f2dc2..3c5b956aa7 100644 --- a/Syntax/Parse_AS_Library.hs +++ b/Syntax/Parse_AS_Library.hs @@ -54,7 +54,7 @@ library :: LogicGraph -> AParser st LIB_DEFN library lG = do (lG1, an1) <- lGAnnos lG (ps, ln) <- option (nullRange, iriLibName nullIRI) $ do - s1 <- asKey libraryS <|> asKey "distributed-ontology" + s1 <- asKey libraryS n <- libName lG1 return (tokPos s1, n) (lG2, an2) <- lGAnnos lG1 @@ -115,7 +115,7 @@ emptyParams = Genericity (Params []) (Imported []) nullRange specDefn :: LogicGraph -> AParser st LIB_ITEM specDefn l = do s <- choice $ map asKey - ["specification", specS, ontologyS, "onto", "model", "OMS"] + ["specification", specS, ontologyS, "onto", "model", omsS] n <- hetIRI l g <- generics l e <- equalT @@ -213,11 +213,15 @@ libItem l = specDefn l en <- hetIRI l s2 <- colonT et <- equivType l - s3 <- equalT - sp <- fmap MkOms $ aSpec l + (ms3, sp) <- option (Nothing, MkOms $ emptyAnno $ EmptySpec nullRange) + (do s3 <- equalT + sp <- fmap MkOms $ aSpec l + return (Just s3, sp)) ep <- optEnd return . Equiv_defn en et sp - . catRange $ s1 : s2 : s3 : maybeToList ep + . catRange $ s1 : s2 : case ms3 of + Just s3 -> s3 : maybeToList ep + Nothing -> maybeToList ep <|> -- align defn do s1 <- asKey alignmentS an <- hetIRI l diff --git a/Syntax/Parse_AS_Structured.hs b/Syntax/Parse_AS_Structured.hs index e701eba2d9..e3f0d13051 100644 --- a/Syntax/Parse_AS_Structured.hs +++ b/Syntax/Parse_AS_Structured.hs @@ -35,7 +35,7 @@ module Syntax.Parse_AS_Structured import Logic.Logic import Logic.Comorphism import Logic.Grothendieck -import Logic.KnownIris +import Logic.KnownIris (lookupLogicName) import Syntax.AS_Structured @@ -117,9 +117,14 @@ logicName l = do qualification :: LogicGraph -> AParser st (Token, LogicDescr) qualification l = - pair (asKey logicS) (logicDescr l) + -- TODO: Properly support `language` declarations + -- The `<|> asKey languageS` part in the line below is part of a hack to + -- support `language` declarations without an accompanying `logic` + -- declaration by essentially treating `language` the same as `logic`. + -- This should probably be done properly instead, but it works for now. + pair (asKey logicS <|> asKey languageS) (logicDescr l) <|> do - s <- asKey serializationS <|> asKey "language" + s <- asKey serializationS <|> asKey languageS i <- iriCurie skipSmart return (s, diff --git a/Syntax/Print_AS_Structured.hs b/Syntax/Print_AS_Structured.hs index f85f7ec772..ec297a365e 100644 --- a/Syntax/Print_AS_Structured.hs +++ b/Syntax/Print_AS_Structured.hs @@ -155,7 +155,7 @@ instance Pretty EXTRACTION where printEXTRACTION :: EXTRACTION -> Doc printEXTRACTION (ExtractOrRemove b aa _) = - keyword (if b then "extract" else "remove") <+> fsep (map pretty aa) + keyword (if b then extractS else removeS) <+> fsep (map pretty aa) instance Pretty RENAMING where pretty = printRENAMING diff --git a/test/DOL/parserTest.dol b/test/DOL/parserTest.dol index bae84fa9dc..b3370d2231 100644 --- a/test/DOL/parserTest.dol +++ b/test/DOL/parserTest.dol @@ -13,20 +13,33 @@ bar: )% -distributed-ontology foo:chocolate - -logic CommonLogic serialization CLIF - -ontology o1 = -(and (P x) - (Q x) - ((that (exists (x) (R x)))) // possible in IKL - (iff (R x) ((that (R x)))) // a tautology - (forall (p) (iff (p) ((that (p))))) // another one - (forall (p) (= p (that (p)))) // NOT a tautology (see IKL-SPEC) - (= ('foo') foo) // should become a tautology - ) -end +library foo:chocolate + +%% TODO: logics should be complete IRIs (either full or prefixed) (legacy?) +%% relates to DOL issue #161 + +%% The commented lines are problematic because there is courrently no symbol +%% parser for 'CommonLogic' which means that some of the symbols in the +%% alignments further down lead to parse errors. As this is not a problem +%% relating to the DOL parser, the logic/serialization declaration and the +%% 'CommonLogic' specific parts have been commented out. +%% This means the logic at work is now CASL which can parse nearly everything +%% and thus all errors should be DOL related. Once we have a proper +%% 'CommonLogic' symbol parser, the commented lines can go active again +%% providing ready made test cases. + +%% logic CommonLogic serialization CLIF + +%%ontology o1 = +%%(and (P x) +%% (Q x) +%% ((that (exists (x) (R x)))) // possible in IKL +%% (iff (R x) ((that (R x)))) // a tautology +%% (forall (p) (iff (p) ((that (p))))) // another one +%% (forall (p) (= p (that (p)))) // NOT a tautology (see IKL-SPEC) +%% (= ('foo') foo) // should become a tautology +%% ) +%%end ontology foo:a = {} ontology bar:b = {} @@ -50,42 +63,44 @@ alignment a7 : foo:foo_bar to foo:baz end alignment a8 : foo:owltime_instant_l to bar:owltime_le -= eRef1 rRef (0.1) ERef2 %( corrId )% -, eRef1 rRef (0.1) ERef2 += eRef1 rRef 0.1 ERef2 %( corrId )% +, eRef1 rRef 0.1 ERef2 , eRef1 rRef ERef2 %( corrId )% , eRef1 rRef ERef2 -, eRef1 rRef (0.1) ERef2 %( corrId )% -, eRef1 rRef (0.1) ERef2 +, eRef1 rRef 0.1 ERef2 %( corrId )% +, eRef1 rRef 0.1 ERef2 , eRef1 rRef ERef2 %( corrId )% , eRef1 rRef ERef2 -, eRef1 (0.1) ERef2 %( corrId )% -, eRef1 (0.1) ERef2 +, eRef1 0.1 ERef2 %( corrId )% +, eRef1 0.1 ERef2 , eRef1 ERef2 %( corrId )% , eRef1 ERef2 -, eRef1 (0.1) ERef2 %( corrId )% -, eRef1 (0.1) ERef2 +, eRef1 0.1 ERef2 %( corrId )% +, eRef1 0.1 ERef2 , eRef1 ERef2 %( corrId )% , eRef1 ERef2 -, eRef1 < (0.1) ERef2 -, eRef1 > (0.1) ERef2 -, eRef1 = (0.1) ERef2 -, eRef1 % (0.1) ERef2 -, eRef1 $\ni$ (0.1) ERef2 -, eRef1 $\in$ (0.1) ERef2 -, eRef1 $\mapsto$ (0.1) ERef2 +, eRef1 < 0.1 ERef2 +, eRef1 > 0.1 ERef2 +, eRef1 = 0.1 ERef2 +, eRef1 % 0.1 ERef2 +, eRef1 ni 0.1 ERef2 +, eRef1 in 0.1 ERef2 , eRef1 < ERef2 , eRef1 > ERef2 , eRef1 = ERef2 , eRef1 % ERef2 -, eRef1 $\ni$ ERef2 -, eRef1 $\in$ ERef2 -, eRef1 $\mapsto$ ERef2 -, relation < (0.1) {eRef1 ERef2} +, eRef1 ni ERef2 +, eRef1 in ERef2 +, relation < 0.1 {eRef1 ERef2} , relation < {eRef1 ERef2} -, relation (0.1) {eRef1 ERef2} +, relation 0.1 {eRef1 ERef2} , relation {eRef1 ERef2} end +alignment a9 : foo:owltime_instant_l to bar:owltime_le += eRef1 rRef 0.1 ERef2 %( corrId )% +assuming SingleDomain +end alignment a10 align-arity-forward 1 align-arity-backward 1 : foo:foo_bar to foo:baz end @@ -102,8 +117,11 @@ end alignment a14 align-arity-forward ? align-arity-backward 1 : foo:foo_bar to foo:baz end -module m20 : - (P x) - of - (Q x) - for FOO +%% See the commented directly after the library declaration at the top if you +%% want to know why this has been commented out. + +%% module m20 : +%% (P x) +%% of +%% (Q x) +%% for FOO