content: {- |
  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
  