Partially solve 1494 parse dol standard examples

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

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"
 

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]

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` "<>"))

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 =

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

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,

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

test/DOL/parserTest.dol

@@ -13,20 +13,33 @@ bar: <http://www.example.com/bar.dol#>
 
 )%
 
-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