parser for GDOL, first attempt

Common/Lexer.hs

@@ -291,6 +291,10 @@ commaT = asSeparator ","
 semiT :: CharParser st Token
 semiT = pToken $ string ";" << notFollowedBy (char ';')
 
+-- a double colon
+doubleColonT :: CharParser st Token
+doubleColonT = pToken $ string "::" << notFollowedBy (char ':')
+
 oBraceT :: CharParser st Token
 oBraceT = asSeparator "{"
 

Common/Token.hs

@@ -113,14 +113,15 @@ criticalKeywords = terminatingKeywords ++ startingKeywords
 terminatingKeywords :: [String]
 terminatingKeywords =
     [ andS, endS, extractS, fitS, forgetS, hideS, keepS, rejectS, removeS, 
-      revealS, selectS, thenS, withS, withinS, ofS, forS, toS, intersectS]
+      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 ]
+    , interpretationS, entailmentS, "pattern" ]
 
 -- | keywords that may follow a defining equal sign
 otherStartKeywords :: [String]

Driver/WriteFn.hs

@@ -302,7 +302,7 @@ writeTheory ins nam opts filePrefix ga
                   (printTheory ms OWL2 $ OWL2.prepareBasicTheory th2) "\n"
             showDiags opts ds
             when (null sy)
-                $ case parse (OWL2.basicSpec Map.empty >> eof) f owltext of
+                $ case parse ((OWL2.basicSpec True) Map.empty >> eof) f owltext of
               Left err -> putIfVerbose opts 0 $ show err
               _ -> putIfVerbose opts 3 $ "reparsed: " ++ f
             writeVerbFile opts f owltext

Logic/ExtSign.hs

@@ -21,7 +21,6 @@ import Common.DocUtils
 import Common.ExtSign
 import Logic.Logic
 
-
 ext_sym_of :: Logic lid sublogics
         basic_spec sentence symb_items symb_map_items
         sign morphism symbol raw_symbol proof_tree
@@ -154,7 +153,7 @@ ext_induced_from_to_morphism l r s@(ExtSign p sy) t = do
     checkExtSign l "from" s
     checkExtSign l "to" t
     checkRawMap l r p
-    checkRawSyms l (Map.elems r) $ nonImportedSymbols t
+    -- checkRawSyms l (Map.elems r) $ nonImportedSymbols t
     mor <- induced_from_to_morphism l r s t
     let sysI = Set.toList $ Set.difference (symset_of l p) sy
         morM = symmap_of l mor

Logic/Logic.hs

@@ -257,6 +257,9 @@ class (Language lid, PrintTypeConv basic_spec, GetRange basic_spec,
             Just p -> makeDefault (p, pretty)
          -- | parser for basic specifications
          parse_basic_spec :: lid -> Maybe (PrefixMap -> AParser st basic_spec)
+         -- | parser for macros
+         parse_macro :: lid -> Maybe (PrefixMap -> AParser st basic_spec)
+         parse_macro _ = Nothing
          -- | parser for a single symbol returned as list
          parseSingleSymbItem :: lid -> Maybe (AParser st symb_items)
          -- | parser for symbol lists
@@ -277,6 +280,10 @@ basicSpecParser :: Syntax lid basic_spec symbol symb_items symb_map_items
   => Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec)
 basicSpecParser sm = fmap fst . parserAndPrinter sm
 
+macroParser :: Syntax lid basic_spec symbol symb_items symb_map_items
+  => Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec)
+macroParser _ = parse_macro
+
 basicSpecPrinter :: Syntax lid basic_spec symbol symb_items symb_map_items
   => Maybe IRI -> lid -> Maybe (basic_spec -> Doc)
 basicSpecPrinter sm = fmap snd . parserAndPrinter sm
@@ -372,6 +379,9 @@ class (Language lid, Category sign morphism, Ord sentence,
       -- | symbols have a name, see CASL RefMan p. 192
       sym_name :: lid -> symbol -> Id
       sym_name l _ = statError l "sym_name"
+      -- | allow to change name
+      rename_symbol :: lid -> symbol -> Id -> symbol
+      rename_symbol lid _ _ = error $ "symbol renaming nyi for logic " ++ show lid
       -- | some symbols have a label for better readability
       sym_label :: lid -> symbol -> Maybe String
       sym_label _ _ = Nothing
@@ -387,6 +397,9 @@ class (Language lid, Category sign morphism, Ord sentence,
       -- | combine two symbols into another one
       pair_symbols :: lid -> symbol -> symbol -> Result symbol
       pair_symbols lid _ _ = error $ "pair_symbols nyi for logic " ++ show lid
+      -- | create symbol from a name and a kind
+      new_symbol :: lid -> IRI -> String -> symbol
+      new_symbol _ _ _ = error "new_symbol nyi"
 
 -- | makes a singleton list from the given value
 singletonList :: a -> [a]
@@ -481,6 +494,10 @@ class ( Syntax lid basic_spec symbol symb_items symb_map_items
          convertTheory :: lid -> Maybe ((sign, [Named sentence]) -> basic_spec)
          convertTheory _ = Nothing
 
+         -- | convert a pair of symbols to symb_map_items
+         convertSymbols :: lid -> Maybe(symbol -> symbol -> symb_map_items)
+         convertSymbols _ = Nothing 
+
          {- ----------------------- amalgamation ---------------------------
             Computation of colimits of signature diagram.
             Indeed, it suffices to compute a cocone that is weakly amalgamable
@@ -625,6 +642,70 @@ class ( Syntax lid basic_spec symbol symb_items symb_map_items
          extract_module :: lid -> [IRI] -> (sign, [Named sentence])
                         -> Result (sign, [Named sentence])
          extract_module _ _ = return
+         -- solving symbols in patterns
+         solve_symbols :: lid -> Set.Set symbol -> PatternVarMap -> basic_spec -> Result basic_spec
+         solve_symbols _ _ _ = error "solve_symbols nyi"
+         -- instantiating macros
+         instantiate_macro :: lid -> PatternVarMap -> GSubst -> basic_spec -> Result basic_spec
+         instantiate_macro _ _ _ _ = error "instantiate_macro nyi"
+         -- delete all occurences of a set of symbols in a solved macro
+         delete_symbols_macro :: lid -> Set.Set symbol -> basic_spec -> Result basic_spec
+         delete_symbols_macro _ _ _ = error "delete_symbols_macro nyi"
+
+
+type GSubst = Map.Map (IRI, String) GSubstVal -- TODO: use GSubstVal instead of IRI!
+
+data GSubstVal = PlainVal IRI | 
+                 ListVal String [IRI] -- the string stores the kind!
+                 deriving (Eq, Show)
+
+getIRIVal :: GSubstVal -> IRI
+getIRIVal v = case v of
+               PlainVal x -> x
+               _ -> error $ "expecting plain value but got list:" ++ show v
+
+-- instantiate paramerized names
+-- p[X] becomes p[V] if subst maps X to V
+-- the string argument is the kind
+
+instParamName :: GSubst -> IRI -> IRI
+instParamName subst p =
+ p{iriPath = solveId subst (iriPath p)}
+
+solveId :: GSubst -> Id -> Id
+solveId subst t =
+ case getComps t of
+  [] -> let tIRI = idToIRI t
+            k = let tSubsts = filter (\(x,_) -> x == tIRI) $ Map.keys subst
+                 in case tSubsts of 
+                      [(_,b)] -> b
+                      []-> "Class" -- does not matter  
+                      (_, b):_ -> b
+         in iriPath $ getIRIVal $ Map.findWithDefault (PlainVal tIRI) (tIRI,k) subst
+  cs -> let its' = map (solveToken subst) $ getTokens t
+            ts' =  concatMap getTokens its'
+            cs'' = concatMap getComps its' 
+            cs' = map (solveId subst) cs
+        in t{getTokens = ts', getComps = cs'' ++ cs'}
+
+solveToken :: GSubst -> Token  -> Id
+solveToken subst tok = 
+ let tIRI = idToIRI $ mkId [tok]
+     k = let tSubsts = filter (\(x,_) -> x == tIRI) $ Map.keys subst
+                 in case tSubsts of 
+                      [(_,b)] -> b
+                      []-> "Class" -- does not matter  
+                      (_,b):_ -> b
+     idVal = iriPath $ getIRIVal $ Map.findWithDefault (PlainVal tIRI) (tIRI,k) subst
+ in idVal --case getComps idVal of
+    -- [] -> head $ getTokens idVal
+    -- _ -> error $  "expecting simple id but got a composed one: " ++ show idVal
+
+type PatternVarMap = Map.Map IRI (Bool, String)
+-- Bool is true for list- and false for non-list variables
+-- TODO: ideally we should have logic-dependent kinds, but strings will do
+-- TODO: this does not allow to have same name for different kinds. 
+-- One idea would be to work with lists of strings. Future work, should be easy.
 
 -- | print a whole theory
 printTheory :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items

OWL2/AS.hs

@@ -348,6 +348,14 @@ data Entity = Entity
   , cutIRI :: IRI }
   deriving (Show, Typeable, Data)
 
+newSymbol :: IRI -> String -> Entity
+newSymbol i s = 
+ case s of
+  "Class" -> mkEntity Class i
+  "ObjectProperty" -> mkEntity ObjectProperty i
+  "Individual" -> mkEntity NamedIndividual i
+  _ -> error $ "nyi:" ++ show s
+
 mkEntity :: EntityType -> IRI -> Entity
 mkEntity = Entity Nothing
 
@@ -371,6 +379,7 @@ data EntityType =
   | DataProperty
   | AnnotationProperty
   | NamedIndividual
+  | UnsolvedEntity
     deriving (Enum, Bounded, Show, Read, Eq, Ord, Typeable, Data)
 
 showEntityType :: EntityType -> String
@@ -385,6 +394,9 @@ showEntityType e = case e of
 entityTypes :: [EntityType]
 entityTypes = [minBound .. maxBound]
 
+renameSymbol :: Entity -> Id -> Entity
+renameSymbol e i = e {cutIRI = idToIRI i}
+
 pairSymbols :: Entity -> Entity -> Result Entity -- TODO: improve!
 pairSymbols (Entity lb1 k1 i1) (Entity lb2 k2 i2) =
   if k1 /= k2 then
@@ -409,7 +421,7 @@ pairSymbols (Entity lb1 k1 i1) (Entity lb2 k2 i2) =
 data TypedOrUntyped = Typed Datatype | Untyped (Maybe LanguageTag)
     deriving (Show, Eq, Ord, Typeable, Data)
 
-data Literal = Literal LexicalForm TypedOrUntyped | NumberLit FloatLit
+data Literal = Literal LexicalForm TypedOrUntyped | NumberLit FloatLit | LiteralVar IRI
     deriving (Show, Eq, Ord, Typeable, Data)
 
 -- | non-negative integers given by the sequence of digits
@@ -515,12 +527,15 @@ type InverseObjectProperty = ObjectPropertyExpression
 
 data ObjectPropertyExpression = ObjectProp ObjectProperty
   | ObjectInverseOf InverseObjectProperty
+  | ObjectPropertyVar Bool IRI
+  | UnsolvedObjProp IRI
         deriving (Show, Eq, Ord, Typeable, Data)
 
 objPropToIRI :: ObjectPropertyExpression -> Individual
 objPropToIRI opExp = case opExp of
     ObjectProp u -> u
     ObjectInverseOf objProp -> objPropToIRI objProp
+    _ -> error "nyi"
 
 type DataPropertyExpression = DataProperty
 
@@ -533,10 +548,12 @@ data DataRange =
   | DataOneOf [Literal]
     deriving (Show, Eq, Ord, Typeable, Data)
 
--- * CLASS EXPERSSIONS
+-- * CLASS EXPRESSIONS
 
 data ClassExpression =
     Expression Class
+  | UnsolvedClass IRI
+  | VarExpression MVarOrTerm
   | ObjectJunction JunctionType [ClassExpression]
   | ObjectComplementOf ClassExpression
   | ObjectOneOf [Individual]
@@ -549,6 +566,19 @@ data ClassExpression =
   | DataCardinality (Cardinality DataPropertyExpression DataRange)
     deriving (Show, Eq, Ord, Typeable, Data)
 
+data MVarOrTerm = MVar Bool IRI | MUnion IRI IRI 
+ -- the name of the head and the name of the tail TODO: should be extended with other terms
+ -- True for lists!
+ deriving (Show, Eq, Ord, Typeable, Data)
+
+-- * INDIVIDUAL EXPRESSIONS
+
+data IndExpression = 
+   IndAsExpression Individual
+ | UnsolvedInd IRI
+ | IndVar IRI
+   deriving (Show, Eq, Ord, Typeable, Data)
+
 -- * ANNOTATIONS
 
 data Annotation = Annotation [Annotation] AnnotationProperty AnnotationValue

OWL2/DMU2OWL2.hs

@@ -81,7 +81,7 @@ runOntoDMU str = if null str then return "" else do
   return out
 
 readOWL :: Monad m => String -> m (Sign, [Named Axiom])
-readOWL str = case runParser (liftM2 const (basicSpec Map.empty) eof) () "" str of
+readOWL str = case runParser (liftM2 const ((basicSpec True) Map.empty) eof) () "" str of
   Left er -> fail $ show er
   Right ontoFile -> let
     newont = function Expand (StringMap $ prefixDeclaration ontoFile) ontoFile

OWL2/Function.hs

@@ -134,6 +134,7 @@ instance Function ObjectPropertyExpression where
     function t s opr = case opr of
         ObjectProp op -> ObjectProp $ cutWith ObjectProperty t s op
         ObjectInverseOf op -> ObjectInverseOf $ function t s op
+        _ -> error $ show opr
 
 instance Function DataRange where
     function t s dra = case dra of
@@ -162,6 +163,7 @@ instance Function ClassExpression where
             $ function t s l
         DataCardinality (Cardinality ct i dp mdr) -> DataCardinality
               $ Cardinality ct i (cutWith DataProperty t s dp) $ maybeDo t s mdr
+        _ -> error $ show cle
 
 instance Function Annotation where
     function t s (Annotation al ap av) = Annotation (map (function t s) al)

OWL2/Logic_OWL2.hs

@@ -57,6 +57,9 @@ import OWL2.Symbols
 import OWL2.Taxonomy
 import OWL2.Theorem
 import OWL2.ExtractModule
+-- import OWL2.Macros
+
+import Debug.Trace
 
 data OWL2 = OWL2
 
@@ -86,9 +89,10 @@ instance Monoid OntologyDocument where
       OntologyDocument (Map.union p1 p2) $ mappend o1 o2
 
 instance Syntax OWL2 OntologyDocument Entity SymbItems SymbMapItems where
-    parsersAndPrinters OWL2 = addSyntax "Ship" (basicSpec, ppShipOnt)
-      $ addSyntax "Manchester" (basicSpec, pretty)
-      $ makeDefault (basicSpec, pretty)
+    parsersAndPrinters OWL2 = addSyntax "Ship" (basicSpec True, ppShipOnt)
+      $ addSyntax "Manchester" (basicSpec True, pretty)
+      $ makeDefault (basicSpec True, pretty)
+    parse_macro OWL2 = Just (basicSpec False)
     parseSingleSymbItem OWL2 = Just symbItem
     parse_symb_items OWL2 = Just symbItems
     parse_symb_map_items OWL2 = Just symbMapItems
@@ -100,6 +104,7 @@ instance Sentences OWL2 Axiom Sign OWLMorphism Entity where
     sym_of OWL2 = singletonList . symOf
     symmap_of OWL2 = symMapOf
     sym_name OWL2 = entityToId
+    rename_symbol OWL2 = renameSymbol
     sym_label OWL2 = label
     fullSymName OWL2 s = let
       i = cutIRI s
@@ -108,6 +113,7 @@ instance Sentences OWL2 Axiom Sign OWLMorphism Entity where
     symKind OWL2 = takeWhile isAlpha . showEntityType . entityKind
     symsOfSen OWL2 _ = Set.toList . symsOfAxiom
     pair_symbols OWL2 = pairSymbols
+    new_symbol OWL2 = newSymbol
 
 inducedFromToMor :: Map.Map RawSymb RawSymb -> 
                     ExtSign Sign Entity -> 
@@ -138,7 +144,7 @@ inducedFromToMorphismAux :: Map.Map RawSymb RawSymb ->
                     ExtSign Sign Entity -> 
                     ExtSign Sign Entity -> 
                     Result OWLMorphism
-inducedFromToMorphismAux rm s@(ExtSign ssig _) t@(ExtSign tsig _) = do
+inducedFromToMorphismAux rm s@(ExtSign ssig _) t@(ExtSign tsig _) = do -- trace ("\n aux ssig:" ++ show ssig ++ "\ntsig:" ++ show tsig ++ "\nrm:" ++ show rm) $ do
     mor <- inducedFromMor rm ssig
     let csig = cod mor
     incl <- inclusion OWL2 csig tsig              
@@ -153,6 +159,7 @@ instance StaticAnalysis OWL2 OntologyDocument Axiom
       stat_symb_items OWL2 s = return . statSymbItems s
       stat_symb_map_items OWL2 = statSymbMapItems
       convertTheory OWL2 = Just convertBasicTheory
+      convertSymbols OWL2 = Just convertEntities
       empty_signature OWL2 = emptySign
       signature_union OWL2 = uniteSign
       intersection OWL2 = intersectSign
@@ -173,9 +180,13 @@ instance StaticAnalysis OWL2 OntologyDocument Axiom
       corresp2th OWL2 = corr2theo
       equiv2cospan OWL2 = addEquiv
       extract_module OWL2 = extractModule
+      solve_symbols OWL2 = solveSymbols
+      instantiate_macro OWL2 = instantiateMacro
+      delete_symbols_macro OWL2 = deleteSymbolsMacro
 #ifdef UNI_PACKAGE
       theory_to_taxonomy OWL2 = onto2Tax
 #endif
+
 instance Logic OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems
                Sign
                OWLMorphism Entity RawSymb ProofTree where

OWL2/MS.hs

@@ -35,6 +35,7 @@ data Extended =
   | ClassEntity ClassExpression
   | ObjectEntity ObjectPropertyExpression
   | SimpleEntity Entity
+  | IndividualVar IRI
     deriving (Show, Eq, Ord, Typeable, Data)
 
 -- | frames with annotated lists