From 69e6eaf599a2962fe722885dadc5179190304312 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Mon, 20 Jul 2015 21:15:43 +0200 Subject: [PATCH 01/22] Remove keyword 'distributed-ontology' It's no longer part of the standard, so there's no need to parse it anymore. 'library' is sufficient. --- Syntax/Parse_AS_Library.hs | 2 +- test/DOL/parserTest.dol | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Syntax/Parse_AS_Library.hs b/Syntax/Parse_AS_Library.hs index 8eae3f2dc2..78e20e66ad 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 diff --git a/test/DOL/parserTest.dol b/test/DOL/parserTest.dol index bae84fa9dc..161670f14f 100644 --- a/test/DOL/parserTest.dol +++ b/test/DOL/parserTest.dol @@ -13,7 +13,7 @@ bar: )% -distributed-ontology foo:chocolate +library foo:chocolate logic CommonLogic serialization CLIF From 4fd2ecb9b6b8caa4bd774cc8138aaf8a7f31fdc5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Mon, 20 Jul 2015 21:26:19 +0200 Subject: [PATCH 02/22] Remove 'CommonLogic' parts from DOL test See the comments in the file for an explanation. In short: those parts make the parser choke, but not because of DOL related problems. So they have to go until those unrelated problems have been fixed. --- test/DOL/parserTest.dol | 50 +++++++++++++++++++++++++++-------------- 1 file changed, 33 insertions(+), 17 deletions(-) diff --git a/test/DOL/parserTest.dol b/test/DOL/parserTest.dol index 161670f14f..1b31e5c76c 100644 --- a/test/DOL/parserTest.dol +++ b/test/DOL/parserTest.dol @@ -15,18 +15,31 @@ bar: library 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 +%% 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 = {} @@ -102,8 +115,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 From d1f1f845f4fd853e8d75230037202443792c7858 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Mon, 20 Jul 2015 21:39:53 +0200 Subject: [PATCH 03/22] Remove 'mapsto' alignment relation from DOL test It's not part of the DOL grammar and that's how it should be as it's also not part of the alignment API. --- test/DOL/parserTest.dol | 2 -- 1 file changed, 2 deletions(-) diff --git a/test/DOL/parserTest.dol b/test/DOL/parserTest.dol index 1b31e5c76c..68b9a3b6ad 100644 --- a/test/DOL/parserTest.dol +++ b/test/DOL/parserTest.dol @@ -85,14 +85,12 @@ alignment a8 : foo:owltime_instant_l to bar:owltime_le , eRef1 % (0.1) ERef2 , eRef1 $\ni$ (0.1) ERef2 , eRef1 $\in$ (0.1) ERef2 -, eRef1 $\mapsto$ (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} , relation < {eRef1 ERef2} , relation (0.1) {eRef1 ERef2} From 6fce3e819f3dca2bd9a991dc83d1eaa35c7f59d2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Mon, 20 Jul 2015 21:47:31 +0200 Subject: [PATCH 04/22] Fix LaTex'isms in DOL test The DOL Standard doesn't allow those. Should be plain text keywords instead. --- test/DOL/parserTest.dol | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/test/DOL/parserTest.dol b/test/DOL/parserTest.dol index 68b9a3b6ad..ec60089da3 100644 --- a/test/DOL/parserTest.dol +++ b/test/DOL/parserTest.dol @@ -83,14 +83,14 @@ alignment a8 : foo:owltime_instant_l to bar:owltime_le , eRef1 > (0.1) ERef2 , eRef1 = (0.1) ERef2 , eRef1 % (0.1) ERef2 -, eRef1 $\ni$ (0.1) ERef2 -, eRef1 $\in$ (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 ni ERef2 +, eRef1 in ERef2 , relation < (0.1) {eRef1 ERef2} , relation < {eRef1 ERef2} , relation (0.1) {eRef1 ERef2} From 77cd3cfa9052ddba2b09b142dd6334408c5164e1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Mon, 20 Jul 2015 21:50:29 +0200 Subject: [PATCH 05/22] Fix confidence declarations in DOL test The standard says they should simply be doubles, not enclosed in parentheses. --- test/DOL/parserTest.dol | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/test/DOL/parserTest.dol b/test/DOL/parserTest.dol index ec60089da3..160b655e09 100644 --- a/test/DOL/parserTest.dol +++ b/test/DOL/parserTest.dol @@ -63,37 +63,37 @@ 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 < 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 -, relation < (0.1) {eRef1 ERef2} +, relation < 0.1 {eRef1 ERef2} , relation < {eRef1 ERef2} -, relation (0.1) {eRef1 ERef2} +, relation 0.1 {eRef1 ERef2} , relation {eRef1 ERef2} end From 0ada09287190b0c52e99bfe4bfed35e2b5366841 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Mon, 20 Jul 2015 21:57:38 +0200 Subject: [PATCH 06/22] Add "AlignmentSemantics" test case --- test/DOL/parserTest.dol | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/test/DOL/parserTest.dol b/test/DOL/parserTest.dol index 160b655e09..b3370d2231 100644 --- a/test/DOL/parserTest.dol +++ b/test/DOL/parserTest.dol @@ -97,6 +97,10 @@ alignment a8 : foo:owltime_instant_l to bar:owltime_le , 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 From 0c63db2aab268c2db1d526b659b6adb62f2d48c9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Sun, 1 Nov 2015 22:32:12 +0100 Subject: [PATCH 07/22] Add `oms` keyword --- Common/Keywords.hs | 3 +++ Common/Token.hs | 2 +- Syntax/Parse_AS_Library.hs | 2 +- 3 files changed, 5 insertions(+), 2 deletions(-) diff --git a/Common/Keywords.hs b/Common/Keywords.hs index 4459e6e2f2..35a786d272 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" diff --git a/Common/Token.hs b/Common/Token.hs index 2c1e243b41..9ccba83c74 100644 --- a/Common/Token.hs +++ b/Common/Token.hs @@ -119,7 +119,7 @@ terminatingKeywords = startingKeywords :: [String] startingKeywords = [ archS, fromS, logicS, newlogicS, refinementS, specS, unitS, viewS - , ontologyS, alignmentS, networkS, equivalenceS, newcomorphismS + , omsS, ontologyS, alignmentS, networkS, equivalenceS, newcomorphismS , interpretationS, entailmentS ] -- | keywords that may follow a defining equal sign diff --git a/Syntax/Parse_AS_Library.hs b/Syntax/Parse_AS_Library.hs index 78e20e66ad..77d3506109 100644 --- a/Syntax/Parse_AS_Library.hs +++ b/Syntax/Parse_AS_Library.hs @@ -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 From 7877253d1ac97667debfa354be2f028960b8cbe3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Mon, 2 Nov 2015 21:00:10 +0100 Subject: [PATCH 08/22] Make `= OMSOrNetwork` optional in `equivalence` If the `= ...` part is omitted it now defaults to the empty specification/oms/network. --- Syntax/Parse_AS_Library.hs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/Syntax/Parse_AS_Library.hs b/Syntax/Parse_AS_Library.hs index 77d3506109..3c5b956aa7 100644 --- a/Syntax/Parse_AS_Library.hs +++ b/Syntax/Parse_AS_Library.hs @@ -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 From 4eb2e3a23a70c242db5559b5515c2fad946a97ed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Tue, 3 Nov 2015 18:23:56 +0100 Subject: [PATCH 09/22] Make "extract" and "remove" proper keywords It's a minuscule change but that way, it stays in line with how the rest of Hets is organized. --- Syntax/Print_AS_Structured.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From 1e54913e3e9df912d6ddf364596cf72d958c5353 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Tue, 3 Nov 2015 18:28:34 +0100 Subject: [PATCH 10/22] Add `extractS`/`removeS` to `terminatingKeywords` Don't know whether that's the correct way, but it's my stab at getting `OMS Extraction` to work. From what I gathered by reading the code this should be the right way to do it. --- Common/Token.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Common/Token.hs b/Common/Token.hs index 9ccba83c74..d05a3ed175 100644 --- a/Common/Token.hs +++ b/Common/Token.hs @@ -112,7 +112,7 @@ 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 From dee2df574c212def5631126c3ae16eb8908cbd51 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Tue, 3 Nov 2015 22:12:46 +0100 Subject: [PATCH 11/22] Change casing of `DOL` in known prefixes --- Logic/KnownIris.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Logic/KnownIris.hs b/Logic/KnownIris.hs index 2e16aa8aee..0c909d68d1 100644 --- a/Logic/KnownIris.hs +++ b/Logic/KnownIris.hs @@ -16,8 +16,8 @@ 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/" logicNames :: Map.Map String String logicNames = -- IRI -> local name From 6d3719d3911071c7cf9eecbb453aa54938da9445 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Tue, 3 Nov 2015 22:13:51 +0100 Subject: [PATCH 12/22] Strip '<' and '>' from IRI before logic lookup For some reason Hets leaves the angular brackets in there, when parsing IRIs at least in this small code sample. This prevents logic lookup from working properly. I opted for this short hack, as it I don't know whether other code relies on the brackets being there and removing them just before looking up the logic is the option that is least likely to break other code. --- Syntax/Parse_AS_Structured.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Syntax/Parse_AS_Structured.hs b/Syntax/Parse_AS_Structured.hs index e701eba2d9..2f32aceaee 100644 --- a/Syntax/Parse_AS_Structured.hs +++ b/Syntax/Parse_AS_Structured.hs @@ -91,7 +91,7 @@ sublogicChars = many $ satisfy $ \ c -> notElem c ":./\\" && isSignChar c lookupLogicM :: IRI -> AParser st String lookupLogicM i = if isSimple i then return l - else case lookupLogicName l of + else case lookupLogicName (filter (not . (`elem` "<>")) l) of Just s -> return s Nothing -> fail $ "logic " ++ show i ++ " not found" where l = iriToStringUnsecure i From 53e80ad58dd8610ad9a5aa413e03200b965ded42 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Tue, 3 Nov 2015 22:17:18 +0100 Subject: [PATCH 13/22] Use explicit import list for `Logic.KnownIris` Since only one function is used in the importing module, I'd like to make that explicit. --- Syntax/Parse_AS_Structured.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Syntax/Parse_AS_Structured.hs b/Syntax/Parse_AS_Structured.hs index 2f32aceaee..a7c92f2fd5 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 From 0624400f8fc571f09316b275821f107f9f319f01 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Wed, 4 Nov 2015 19:14:53 +0100 Subject: [PATCH 14/22] Allow comment lines in prefix annotations --- Common/AnnoParser.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Common/AnnoParser.hs b/Common/AnnoParser.hs index ee370a39a8..11962be1e8 100644 --- a/Common/AnnoParser.hs +++ b/Common/AnnoParser.hs @@ -27,6 +27,7 @@ module Common.AnnoParser , newlineOrEof ) where +import Text.Parsec.Char (endOfLine) import Text.ParserCombinators.Parsec import Text.ParserCombinators.Parsec.Error import Text.ParserCombinators.Parsec.Pos as Pos @@ -237,7 +238,8 @@ floatingAnno ps = literal2idsAnno ps Float_anno prefixAnno :: Range -> GenParser Char st Annotation prefixAnno ps = do - prefixes <- many $ do + prefixes <- many $ skipMany (commentLine >> endOfLine) >> do + spaces p <- (string colonS >> return "") <|> (IRI.ncname << string colonS) spaces From 82ccbe9abbc6bd4719113d22de7ba157b3e02b36 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Fri, 6 Nov 2015 00:03:22 +0100 Subject: [PATCH 15/22] Shim for parsing `SROIQ` when prefixed Logic `OWL`, sublogic `NP-sROIQ-D|-|` should be correct but Hets errors out saying it doesn't know the logic `NP-sROIQ-D|-|`. For now simply using `OWL` seems to work, but it's a hack that should be corrected at some point. --- Logic/KnownIris.hs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Logic/KnownIris.hs b/Logic/KnownIris.hs index 0c909d68d1..615082ce8a 100644 --- a/Logic/KnownIris.hs +++ b/Logic/KnownIris.hs @@ -24,7 +24,10 @@ logicNames = -- IRI -> local name Map.fromList [ (logPrefix ++ "CommonLogic", "CommonLogic"), (logPrefix ++ "Propositional", "Propositional"), - (logPrefix ++ "OWL2", "OWL") ] + (logPrefix ++ "OWL2", "OWL"), + (logPrefix ++ "SROIQ", "OWL")] -- should be "NP-sROIQ-D|-|" instead of + -- "OWL" but Hets doesn't know that logic + -- yet for some reason... lookupLogicName :: String -> Maybe String lookupLogicName = (`Map.lookup` logicNames) From 9f000430f5584f8182f37e1f475a9277673113e0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Fri, 6 Nov 2015 00:19:03 +0100 Subject: [PATCH 16/22] Filter angular brackets in `lookupSerialization` Same (maybe) problem as in `lookupLogicName`. The IRI passed in as a parameter is still enclosed in angular brackets which is not expected by those functions. Filtering the brackets might only address the symptom of a bigger issue but it fixes the problem at hand and has the least effects on the remaining codebase. --- Logic/KnownIris.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Logic/KnownIris.hs b/Logic/KnownIris.hs index 615082ce8a..4176b2e4c5 100644 --- a/Logic/KnownIris.hs +++ b/Logic/KnownIris.hs @@ -44,4 +44,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` "<>")) From 92bedc99085f70a59a6242b05d3d5cc5e37addcd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Fri, 6 Nov 2015 00:28:11 +0100 Subject: [PATCH 17/22] Move the '<>' fix into `lookupLogicName` This reverts commit 17aa52c88e7300367630ef3df882138acd2845c5 and instead applies the fix closer to logic name lookup inside the function doing the lookup. That way both fixes for serialization and logic name lookup (which are identical) are grouped in one file. --- Logic/KnownIris.hs | 2 +- Syntax/Parse_AS_Structured.hs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Logic/KnownIris.hs b/Logic/KnownIris.hs index 4176b2e4c5..34c5ce5168 100644 --- a/Logic/KnownIris.hs +++ b/Logic/KnownIris.hs @@ -30,7 +30,7 @@ logicNames = -- IRI -> local name -- yet for some reason... lookupLogicName :: String -> Maybe String -lookupLogicName = (`Map.lookup` logicNames) +lookupLogicName = (`Map.lookup` logicNames) . filter (not . (`elem` "<>")) serializations :: String -> Map.Map String String serializations l diff --git a/Syntax/Parse_AS_Structured.hs b/Syntax/Parse_AS_Structured.hs index a7c92f2fd5..4795e51eb6 100644 --- a/Syntax/Parse_AS_Structured.hs +++ b/Syntax/Parse_AS_Structured.hs @@ -91,7 +91,7 @@ sublogicChars = many $ satisfy $ \ c -> notElem c ":./\\" && isSignChar c lookupLogicM :: IRI -> AParser st String lookupLogicM i = if isSimple i then return l - else case lookupLogicName (filter (not . (`elem` "<>")) l) of + else case lookupLogicName l of Just s -> return s Nothing -> fail $ "logic " ++ show i ++ " not found" where l = iriToStringUnsecure i From fe4e8513a9591cbaeb5ca1c381c120d4eab7e492 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Fri, 6 Nov 2015 00:50:23 +0100 Subject: [PATCH 18/22] Expand comment --- Logic/KnownIris.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Logic/KnownIris.hs b/Logic/KnownIris.hs index 34c5ce5168..7bf612082c 100644 --- a/Logic/KnownIris.hs +++ b/Logic/KnownIris.hs @@ -25,9 +25,9 @@ logicNames = -- IRI -> local name [ (logPrefix ++ "CommonLogic", "CommonLogic"), (logPrefix ++ "Propositional", "Propositional"), (logPrefix ++ "OWL2", "OWL"), - (logPrefix ++ "SROIQ", "OWL")] -- should be "NP-sROIQ-D|-|" instead of - -- "OWL" but Hets doesn't know that logic - -- yet for some reason... + (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) . filter (not . (`elem` "<>")) From d779d24e29a627dbb8429bfbdd2a5fa1e2326144 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Sun, 8 Nov 2015 14:40:59 +0100 Subject: [PATCH 19/22] Add `languageS` as a proper keyword --- Common/Keywords.hs | 3 +++ Common/Token.hs | 6 +++--- OWL2/Keywords.hs | 2 +- Syntax/Parse_AS_Structured.hs | 2 +- 4 files changed, 8 insertions(+), 5 deletions(-) diff --git a/Common/Keywords.hs b/Common/Keywords.hs index 35a786d272..8fcb98bee5 100644 --- a/Common/Keywords.hs +++ b/Common/Keywords.hs @@ -507,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 d05a3ed175..ad240f6ef1 100644 --- a/Common/Token.hs +++ b/Common/Token.hs @@ -118,9 +118,9 @@ terminatingKeywords = -- | keywords starting a library item startingKeywords :: [String] startingKeywords = - [ archS, fromS, logicS, newlogicS, refinementS, specS, unitS, viewS - , omsS, 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/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_Structured.hs b/Syntax/Parse_AS_Structured.hs index 4795e51eb6..d6f4004ad9 100644 --- a/Syntax/Parse_AS_Structured.hs +++ b/Syntax/Parse_AS_Structured.hs @@ -119,7 +119,7 @@ qualification :: LogicGraph -> AParser st (Token, LogicDescr) qualification l = pair (asKey logicS) (logicDescr l) <|> do - s <- asKey serializationS <|> asKey "language" + s <- asKey serializationS <|> asKey languageS i <- iriCurie skipSmart return (s, From e92efafa189fe6e1c6a797221b826883ad436c68 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Sun, 8 Nov 2015 16:41:57 +0100 Subject: [PATCH 20/22] Add hacky standalone `language` declaration support As the comments says, theres a proper way to do it by using the information stored in the `LanguageQual` that is the result of parsing the `language` declaration. But this would entail expanding a possible prefix of the `LanguageQual` and I don't have time to implement this right now. I'll open an issue for this so that I can work on it later. For now, parsing the DOL examples is more important so I added this hack to get an intermediate working solution. --- Logic/KnownIris.hs | 7 +++++++ Syntax/Parse_AS_Structured.hs | 7 ++++++- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/Logic/KnownIris.hs b/Logic/KnownIris.hs index 7bf612082c..7fe3061cce 100644 --- a/Logic/KnownIris.hs +++ b/Logic/KnownIris.hs @@ -18,11 +18,18 @@ logPrefix, serPrefix :: String logPrefix = "http://purl.net/DOL/logics/" serPrefix = "http://purl.net/DOL/serializations/" +lngPrefix = "http://purl.net/DOL/languages/" logicNames :: Map.Map String String logicNames = -- IRI -> local name Map.fromList [ (logPrefix ++ "CommonLogic", "CommonLogic"), + -- TODO: Properly support `language` declarations + -- 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. + (lngPrefix ++ "CommonLogic", "CommonLogic"), (logPrefix ++ "Propositional", "Propositional"), (logPrefix ++ "OWL2", "OWL"), (logPrefix ++ "SROIQ", "OWL")] -- should be "NP-sROIQ-D|-|" diff --git a/Syntax/Parse_AS_Structured.hs b/Syntax/Parse_AS_Structured.hs index d6f4004ad9..e3f0d13051 100644 --- a/Syntax/Parse_AS_Structured.hs +++ b/Syntax/Parse_AS_Structured.hs @@ -117,7 +117,12 @@ 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 languageS i <- iriCurie From 2381fb3ce3c753d33e9e888186f32f4aebab4c6f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Mon, 9 Nov 2015 01:45:56 +0100 Subject: [PATCH 21/22] Expand `language` declaration hack Now it also adds support for more logics/languages and various translations. --- Logic/KnownIris.hs | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/Logic/KnownIris.hs b/Logic/KnownIris.hs index 7fe3061cce..a22430cf16 100644 --- a/Logic/KnownIris.hs +++ b/Logic/KnownIris.hs @@ -19,17 +19,26 @@ logPrefix, serPrefix :: String 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 - -- 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`. + -- 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 ++ "SROIQ", "OWL")] -- should be "NP-sROIQ-D|-|" From c49913bef08ba82298900e160cc0d60295f27b4a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Stephan=20G=C3=BCnther?= Date: Fri, 19 Aug 2016 16:25:01 +0200 Subject: [PATCH 22/22] Use `spaces` instead of `endOfLine` Thanks @cmaeder for the suggestion. Using `spaces` has two benefits. It gets rid of a dependency issue resulting in a compilation error and it allows me to be consistent and only eat up whitespace at the end of lines. --- Common/AnnoParser.hs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Common/AnnoParser.hs b/Common/AnnoParser.hs index 11962be1e8..7f027fbd7e 100644 --- a/Common/AnnoParser.hs +++ b/Common/AnnoParser.hs @@ -27,7 +27,6 @@ module Common.AnnoParser , newlineOrEof ) where -import Text.Parsec.Char (endOfLine) import Text.ParserCombinators.Parsec import Text.ParserCombinators.Parsec.Error import Text.ParserCombinators.Parsec.Pos as Pos @@ -238,8 +237,7 @@ floatingAnno ps = literal2idsAnno ps Float_anno prefixAnno :: Range -> GenParser Char st Annotation prefixAnno ps = do - prefixes <- many $ skipMany (commentLine >> endOfLine) >> do - spaces + prefixes <- many $ skipMany (commentLine >> spaces) >> do p <- (string colonS >> return "") <|> (IRI.ncname << string colonS) spaces