{- |

Module : ./OWL2/ShipSyntax.hs

Copyright : (c) C. Maeder DFKI GmbH

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

different pretty printing for the SHIP tool

-}

module OWL2.ShipSyntax where

import OWL2.AS

import Common.Doc

import Common.DocUtils

import Common.Parsec

import Control.Monad

import Data.Char

import Text.ParserCombinators.Parsec

data Concept

= CName String

| NominalC String

| NotC Concept

| JoinedC (Maybe JunctionType) [Concept] -- Nothing denotes disjoint union

| Quant (Either QuantifierType (CardinalityType, Int)) Role Concept

deriving (Show, Eq, Ord)

topC :: Concept

topC = CName "T"

data NotOrInverse = NotR | InvR deriving (Show, Eq, Ord)

data Role

= RName String

| NominalR String String

| UnOp NotOrInverse Role

| JoinedR (Maybe JunctionType) [Role] -- Nothing denotes composition!

deriving (Show, Eq, Ord)

topR :: Role

topR = RName "TxT"

botR :: Role

botR = UnOp NotR topR

ppJunction :: Bool -> Maybe JunctionType -> Doc

ppJunction c mt = text $ case mt of

Just t -> case t of

UnionOf -> "+ "

IntersectionOf -> "& "

Nothing -> if c then "<+> " else ". "

pppNegConcept :: Concept -> Doc

pppNegConcept c = case c of

JoinedC {} -> parens

_ -> id

$ ppConcept c

pppConcept :: Bool -> Maybe JunctionType -> Concept -> Doc

pppConcept notLast mt c = case c of

Quant {} | notLast -> parens

JoinedC mti _

| mti /= mt && maybe True (const $ maybe False (/= UnionOf) mt) mti

-> parens

_ -> id

$ ppConcept c

ppConcept :: Concept -> Doc

ppConcept co = case co of

CName s -> (if co == topC then keyword else text) s

NominalC s -> braces $ text s

NotC c -> text "~" <> pppNegConcept c

JoinedC t l -> case reverse l of

[] -> ppConcept $ if t == Just IntersectionOf then topC else NotC topC

f : r -> fsep . prepPunctuate (ppJunction True t)

. reverse $ pppConcept False t f : map (pppConcept True t) r

Quant q r c -> fsep [(case q of

Left v -> keyword (showQuant v)

Right (n, i) -> text (showCard n) <+> text (show i)

) <+> ppRole r, dot <+> ppConcept c]

showQuant :: QuantifierType -> String

showQuant v = case v of

AllValuesFrom -> "all"

SomeValuesFrom -> "ex"

showCard :: CardinalityType -> String

showCard n = case n of

MinCardinality -> ">="

MaxCardinality -> "<="

ExactCardinality -> "="

showSame :: SameOrDifferent -> String

showSame s = case s of

Same -> "=="

Different -> "!="

pppRole :: Maybe JunctionType -> Role -> Doc

pppRole mt r = case r of

JoinedR (Just ti) _

| maybe True (\ to -> ti /= to && ti == UnionOf) mt

-> parens

_ -> id

$ ppRole r

ppRole :: Role -> Doc

ppRole ro = case ro of

RName s -> (if ro == topR then keyword else text) s

NominalR s t -> braces $ parens $ text s <> comma <+> text t

UnOp o r -> (case o of

NotR -> text "~"

InvR -> keyword "inv") <> (case r of

JoinedR {} -> parens

_ | o == InvR -> parens

_ -> id) (ppRole r)

JoinedR t l -> case l of

[] -> ppRole $ if t /= Just UnionOf then topR else botR

_ -> fsep . prepPunctuate (ppJunction False t) $ map (pppRole t) l

skip :: CharParser st ()

skip = forget $ many $ single (satisfy isSpace) <|> nestedComment "/*" "*/"

<|> tryString "//" <++> many (noneOf "\n")

myLetter :: CharParser st Char

myLetter = satisfy $ \ c -> isAlphaNum c || elem c "_"

nominal :: CharParser st String

nominal = reserved

["_", "all", "ex", "inv", "not", "if", "effect", "causes", "cond", "exec"]

(many1 myLetter) << skip

key :: String -> CharParser st ()

key s = forget $ try $ string s >> notFollowedBy myLetter

skipKey :: String -> CharParser st ()

skipKey s = key s << skip

quant :: CharParser st QuantifierType

quant = choice $ map (\ a -> key (showQuant a) >> return a)

[AllValuesFrom, SomeValuesFrom]

card :: CharParser st CardinalityType

card = choice $ map (\ a -> tryString (showCard a) >> return a)

[MinCardinality, MaxCardinality, ExactCardinality]

quantOrCard :: CharParser st (Either QuantifierType (CardinalityType, Int))

quantOrCard = fmap Left quant

<|> do

c <- card << skip

i <- many1 digit

return $ Right (c, read i)

skipChar :: Char -> CharParser st ()

skipChar c = char c >> skip

commaP, colonP, equalP, bulletP :: CharParser st ()

commaP = skipChar ','

colonP = skipChar ':'

equalP = skipChar '='

bulletP = skipChar '.'

primConcept :: CharParser st Concept

primConcept = do

q <- quantOrCard << skip

r <- primRole

bulletP

fmap (Quant q r) concept

<|> ((key "not" <|> skipChar '~') >> skip >> fmap NotC primConcept)

<|> braced (fmap NominalC nominal) -- allow more nominals

<|> parent concept

<|> fmap CName nominal

braced :: CharParser st a -> CharParser st a

braced p = skipChar '{' >> p << skipChar '}'

parent :: CharParser st a -> CharParser st a

parent p = skipChar '(' >> p << skipChar ')'

binPP :: ([a] -> a) -> CharParser st sep -> CharParser st a -> CharParser st a

binPP f sp p = do

a <- p

l <- many $ sp >> p

return $ if null l then a else f $ a : l

binP :: ([a] -> a) -> String -> CharParser st a -> CharParser st a

binP f s = binPP f $ tryString s >> skip

binC :: ([a] -> a) -> Char -> CharParser st a -> CharParser st a

binC f c = binPP f $ skipChar c

andConcept :: CharParser st Concept

andConcept = binC (JoinedC $ Just IntersectionOf) '&' primConcept

plus :: CharParser st ()

plus = try $ char '+' >> notFollowedBy (char '>') >> skip

orConcept :: CharParser st Concept

orConcept = binPP (JoinedC $ Just UnionOf) plus andConcept

concept :: CharParser st Concept

concept = binP (JoinedC Nothing) "<+>" orConcept

notOrInv :: CharParser st NotOrInverse

notOrInv = (char '~' >> return NotR)

<|> (key "inv" >> return InvR)

nomPair :: (String -> String -> a) -> CharParser st a

nomPair f = parent $ liftM2 f nominal $ commaP >> nominal

primRole :: CharParser st Role

primRole = do

o <- notOrInv << skip

fmap (UnOp o) primRole

<|> braced (nomPair NominalR)

<|> parent role

<|> fmap RName nominal

compRole :: CharParser st Role

compRole = binC (JoinedR Nothing) '.' primRole

andRole :: CharParser st Role

andRole = binC (JoinedR $ Just IntersectionOf) '&' compRole

role :: CharParser st Role

role = binPP (JoinedR $ Just UnionOf) plus andRole

data EqOrLess = Eq | Less deriving (Show, Eq, Ord)

data RoleType = RoleType Concept Concept deriving (Show, Eq, Ord)

-- a missing rhs may be modelled as "< T" or by no constructors

data ConceptRhs

= ADTCons [TBoxCons]

| ConceptRel EqOrLess Concept

deriving (Show, Eq, Ord)

data TBoxCons = TBoxCons Concept [(Role, Concept)]

deriving (Show, Eq, Ord)

data TBox

= ConceptDecl Concept ConceptRhs

| DisjointCs [Concept]

deriving (Show, Eq, Ord)

data RBox

= RoleDecl Role RoleType

| RoleRel Role EqOrLess Role

| RoleProp Character Role

deriving (Show, Eq, Ord)

-- | assertions

data ABox

= AConcept String Concept

| ARole String String Role

| AIndividual String SameOrDifferent String

deriving (Show, Eq, Ord)

data Box = Box [TBox] [RBox] [ABox]

deriving (Show, Eq, Ord)

ppEqOrLess :: EqOrLess -> Doc

ppEqOrLess s = case s of

Eq -> equals

Less -> less

ppRoleType :: RoleType -> Doc

ppRoleType (RoleType s t) =

fsep [colon <+> ppConcept s, cross <+> ppConcept t]

ppConceptRhs :: ConceptRhs -> Doc

ppConceptRhs rhs = case rhs of

ADTCons cs -> if null cs then empty else

text "::=" <+> vcat (prepPunctuate (text "| ") $ map ppTBoxCons cs)

ConceptRel o c -> ppEqOrLess o <+> ppConcept c

ppTBoxCons :: TBoxCons -> Doc

ppTBoxCons (TBoxCons c sels) =

ppConcept c <> if null sels then empty else

parens . sepByCommas $ map

(\ (r, a) -> ppRole r <+> colon <+> ppConcept a) sels

ppTBox :: TBox -> Doc

ppTBox b = case b of

ConceptDecl d m -> ppConcept d <+> ppConceptRhs m

DisjointCs cs -> keyword "Disjoint" <> parens (sepByCommas $ map ppConcept cs)

ppRBox :: RBox -> Doc

ppRBox b = case b of

RoleDecl r t -> fsep [ppRole r, ppRoleType t]

RoleRel r o t -> fsep [ppRole r, ppEqOrLess o <+> ppRole t]

RoleProp c s -> keyword (showCharacter c) <> parens (ppRole s)

ppABox :: ABox -> Doc

ppABox b = case b of

AConcept n c -> text n <> colon <> ppConcept c

ARole s t r -> parens (text s <> comma <+> text t)

<> colon <> ppRole r

AIndividual s c t -> text s <> text (showSame c) <> text t

ppBox :: Box -> Doc

ppBox (Box ts rs as) = let ppM c = keyword $ '%' : c : "BOX" in

vcat $ ppM 'T' : map ppTBox ts ++ ppM 'R' : map ppRBox rs

++ ppM 'A' : map ppABox as

showCharacter :: Character -> String

showCharacter c = case c of

Functional -> "Func"

InverseFunctional -> "FuncInv"

Reflexive -> "Ref"

Irreflexive -> "Irref"

Symmetric -> "Sym"

Asymmetric -> "Asym"

Antisymmetric -> "Dis"

Transitive -> "Trans"

character :: CharParser st Character

character = choice $ map (\ a -> key (showCharacter a) >> return a)

[minBound .. maxBound]

eqOrLess :: CharParser st EqOrLess

eqOrLess = (equalP >> return Eq) <|> (skipChar '<' >> return Less)

tbox :: CharParser st TBox

tbox = (key "Disjoint" >> fmap DisjointCs

(parent $ concept <:> many (commaP >> concept)))

<|> try (liftM2 ConceptDecl concept

(liftM2 ConceptRel eqOrLess concept

<|> fmap ADTCons

((tryString "::=" >> skip >> sepBy tboxCons (skipChar '|'))

<|> (char ':' >> pzero)

<|> (string "==" >> pzero)

<|> (string "!=" >> pzero)

<|> return [])))

tboxCons :: CharParser st TBoxCons

tboxCons = liftM2 TBoxCons concept

. optionL . parent . flip sepBy commaP

. pair role $ colonP >> concept

rbox :: CharParser st RBox

rbox = liftM2 RoleProp character (parent role)

<|> try (do

r <- role

liftM2 (RoleRel r) eqOrLess role

<|> fmap (RoleDecl r) (liftM2 RoleType

(colonP >> concept)

$ skipChar '*' >> concept)) -- added try to recognize abox

abox :: CharParser st ABox

abox = liftM2 ($) (nomPair ARole) (colonP >> role)

<|> do

n <- nominal

fmap (AConcept n) (colonP >> concept)

<|> liftM2 (AIndividual n) (pSame << skip) nominal

pSame :: CharParser st SameOrDifferent

pSame = choice $ map (\ a -> tryString (showSame a) >> return a)

[Same, Different]

box :: CharParser st Box

box = do

forget $ many imprts

optional $ skipKey "%TBOX"

ts <- many tbox

optional $ skipKey "%RBOX"

rs <- many rbox

optional $ skipKey "%ABOX"

as <- many abox

return $ Box ts rs as

imprts :: CharParser st ()

imprts = skipKey "import" << many1 (myLetter <|> char '.') << skip

<< optional rename

rename :: CharParser st ()

rename = do

skipKey "with"

optional $ skipKey "concepts" << nmap

optional $ skipKey "roles" << nmap

optional $ skipKey "individuals" << nmap

return ()

nmap :: GenParser Char st [()]

nmap = sepBy1 (nominal >> skipKey "as" << nominal) commaP

ppp :: (a -> Doc) -> CharParser () a -> String -> String

ppp pr pa s = case parse (skip >> pa << eof) "" s of

Right a -> show $ pr a

Left e -> show e