Ship.hs

{- |
Module      :  $Header$
Copyright   :  (c) C. Maeder DFKI GmbH
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

monitor syntax
-}

module ExtModal.Ship where

import OWL2.ShipSyntax
import OWL2.AS

import Common.Doc
import Common.DocUtils
import Common.Parsec

import Control.Monad

import Text.ParserCombinators.Parsec

data PreOp = NotF | X | F | G | QuantF QuantifierType [ABox]
  deriving (Show, Eq, Ord)

data BinOp = Until | Impl deriving (Show, Eq, Ord)

data Foltl
  = ABoxass ABox
  | Call Bool String [String] -- True: run a process, but deprecated
  | JoinedF JunctionType [Foltl]
  | PreOp PreOp Foltl
  | BinOp Foltl BinOp Foltl
  deriving (Show, Eq, Ord)

constFoltl :: String -> Foltl
constFoltl s = Call False s []

trueFoltl, falseFoltl :: Foltl
trueFoltl = constFoltl "true"
falseFoltl = constFoltl "false"

negFoltl :: Foltl -> Foltl
negFoltl ftl = let nftl = PreOp NotF ftl in case ftl of
  ABoxass _ -> nftl
  Call {} | trueFoltl == ftl -> falseFoltl
          | falseFoltl == ftl -> trueFoltl
          | otherwise -> nftl
  JoinedF t fs -> JoinedF (case t of
    UnionOf -> IntersectionOf
    IntersectionOf -> UnionOf) $ map negFoltl fs
  PreOp p f -> (case p of
    QuantF q as -> PreOp (QuantF (case q of
      AllValuesFrom -> SomeValuesFrom
      SomeValuesFrom -> AllValuesFrom) as)
    X -> PreOp X
    F -> PreOp G
    G -> PreOp F
    NotF -> id) $ negFoltl f
  BinOp f1 p f2 -> case p of
    Until -> release (negFoltl f1) $ negFoltl f2
    Impl -> JoinedF IntersectionOf [negFoltl f1, negFoltl f2]

-- <http://en.wikipedia.org/wiki/Linear_temporal_logic>
weakUntil :: Foltl -> Foltl -> Foltl
weakUntil f1 f2 = JoinedF UnionOf [BinOp f1 Until f2, PreOp G f1]

release :: Foltl -> Foltl -> Foltl
release f1 f2 = weakUntil f2 $ JoinedF IntersectionOf [f1, f2]

data Header = Header String [String]
  deriving (Show, Eq, Ord)

data Monitor = Monitor Header (Maybe String) Foltl
  deriving (Show, Eq, Ord)

type ABoxLit = (Bool, ABox)

type ABoxDeletes = [Either ABoxLit [String]]

type ABoxs = [ABox]

type ABoxAnds = [ABoxLit]

data CondEffect = CondEffect ABox ABoxDeletes
  deriving (Show, Eq, Ord)

data Exec = Exec String String [String]
  deriving (Show, Eq, Ord)

data Action = Action Header ABoxs ABoxDeletes [CondEffect] (Maybe Exec)
  deriving (Show, Eq, Ord)

data IndEffect = IndEffect String ABoxs ABoxDeletes ABoxs
  deriving (Show, Eq, Ord)

data Process = Process Header Proc
  deriving (Show, Eq, Ord)

data Proc
  = While ABoxAnds Proc
  | Star Proc
  | Quest ABox
  | IfElse ABoxAnds Proc Proc
  | Switch [(Maybe ABoxAnds, Proc)]
  | Forall ABoxAnds Proc
  | Init Foltl
  | CallP String [String]
  | BinP BinP [Proc]
  deriving (Show, Eq, Ord)

data BinP = Semi | Pipe | SeqPlus deriving (Show, Eq, Ord)

data Ship
  = ShipP Process
  | ShipA Action
  | ShipI IndEffect
  deriving (Show, Eq, Ord)

isPrimFoltl :: Foltl -> Bool
isPrimFoltl ftl = case ftl of
  ABoxass _ -> True
  Call {} -> True
  PreOp _ f -> isPrimFoltl f
  _ -> False

lastNotPrim :: [Foltl] -> Bool
lastNotPrim l = not (null l) && not (isPrimFoltl $ last l)

ppJFoltl :: Bool -> JunctionType -> Foltl -> Doc
ppJFoltl first j f = case f of
    JoinedF t l -> (if t /= j && t == UnionOf
      || first && lastNotPrim l then parens else id) $ ppFoltl f
    _ -> ppBFoltl first f

ppBFoltl :: Bool -> Foltl -> Doc
ppBFoltl first f = case f of
    BinOp {} -> parens
    JoinedF _ l | first && lastNotPrim l
      -> parens
    PreOp {} | first -> parens
    _ -> id
  $ ppFoltl f

ppFoltl :: Foltl -> Doc
ppFoltl ft = case ft of
  ABoxass a -> ppABox a
  Call b s ps -> (if b then keyword "run" else empty)
    <+> text s <> if null ps then empty else ppParams ps
  JoinedF t l -> case reverse l of
    [] -> empty
    f : r -> fsep . prepPunctuate (text $ case t of
      UnionOf -> "or "
      IntersectionOf -> "and ")
      . reverse $ ppJFoltl False t f : map (ppJFoltl True t) r
  PreOp p f -> let
    d1 = ppPreOp p
    d2 = ppFoltl f
    d3 = d1 <+> d2
    in case p of
    QuantF {} -> fsep [d1, bullet <+> d2]
    NotF -> case f of
      PreOp {} -> d3
      _ -> if isPrimFoltl f then d3 else d1 <> parens d2
    _ -> d3
  BinOp f1 o f2 -> fsep
    [ ppBFoltl True f1
    , case o of
              Until -> keyword "U"
              Impl -> implies
    , ppBFoltl False f2 ]

ppPreOp :: PreOp -> Doc
ppPreOp o = case o of
  QuantF q as -> keyword (showQuant q) <+> sepByCommas (map ppABox as)
  NotF -> keyword "not"
  _ -> keyword (show o)

ppHeader :: Header -> Doc
ppHeader (Header name ps) = text name <>
       (if null ps then empty else ppParams ps)
    <+> equals

ppMonitor :: Monitor -> Doc
ppMonitor (Monitor h mc ft) = fsep
  $ (keyword "monitor" <+> ppHeader h)
  : case mc of
      Nothing -> []
      Just c -> [doubleQuotes . text $ filter (/= '"') c]
  ++ [ppFoltl ft]

ppMon :: [Monitor] -> Doc
ppMon = vsep . map ppMonitor

ppABoxLit :: ABoxLit -> Doc
ppABoxLit (b, a) = (if b then empty else keyword "not") <+> ppABox a

ppABoxDelete :: Either ABoxLit [String] -> Doc
ppABoxDelete e = case e of
  Left a -> ppABoxLit a
  Right l -> keyword "delete" <> ppParams l

ppABoxDeletes :: ABoxDeletes -> Doc
ppABoxDeletes = sepByCommas . map ppABoxDelete

ppABoxs :: ABoxs -> Doc
ppABoxs = sepByCommas . map ppABox

ppABoxAnds :: ABoxAnds -> Doc
ppABoxAnds = fsep . prepPunctuate (text "and ") . map ppABoxLit

ppCondEffect :: CondEffect -> Doc
ppCondEffect (CondEffect a as) =
  fsep [keyword "if" <+> parens (ppABox a), ppABoxDeletes as]

eqKey :: String -> Doc
eqKey s = keyword s <+> equals

ppParams :: [String] -> Doc
ppParams = parens . sepByCommas . map text

ppExec :: Exec -> [Doc]
ppExec (Exec s1 s2 ps) =
  [eqKey "exec" <+> text s1 <> dot <> text s2 <> ppParams ps]

ppAction :: Action -> Doc
ppAction (Action h pre eff cs me) = fsep
  [ keyword "action" <+> ppHeader h
  , braces $ vcat
    $ [ if null pre then empty else eqKey "pre" <+> ppABoxs pre
      , if null eff then empty else eqKey "effect" <+> ppABoxDeletes eff]
    ++ map ppCondEffect cs
    ++ maybe [] ppExec me]

ppIndEffect :: IndEffect -> Doc
ppIndEffect (IndEffect n is cs ds) = fsep
  [ keyword "indirect" <+> keyword "effect" <+> ppHeader (Header n [])
  , braces $ vcat
    [ eqKey "init" <+> ppABoxs is
    , eqKey "causes" <+> ppABoxDeletes cs
    , eqKey "cond" <+> ppABoxs ds]]

ppProcess :: Process -> Doc
ppProcess (Process h p) = fsep
  [ keyword "function" <+> ppHeader h, braces $ ppProc p]

ppProc :: Proc -> Doc
ppProc pr = case pr of
  While as p -> fsep
    [keyword "while" <+> parens (ppABoxAnds as), ppProc p]
  Star p -> (if isPrim p then id else parens) (ppProc p) <> text "*"
  Quest a -> ppABox a <> text "?"
  IfElse as p1 p2 -> fsep
    [ keyword "if" <+> parens (ppABoxAnds as), ppProc p1
    , keyword "else" <+> ppProc p2]
  Switch cs -> keyword "switch" <+>
    vcat (map (\ (m, p) -> fsep
      [keyword "case" <+> maybe (text "_") ppABoxAnds m, implies <+> ppProc p])
          cs)
  Forall as p -> fsep
    [keyword "forall" <+> ppABoxAnds as, implies <+> ppProc p]
  Init f -> keyword "init" <+> ppFoltl f
  CallP n ps -> text n <> ppParams ps
  BinP o ps -> case reverse ps of
    [] -> empty
    f : r -> fsep . prepPunctuate (ppBinP o)
      . reverse $ ppBinProc False o f : map (ppBinProc True o) r

isPrim :: Proc -> Bool
isPrim p = case p of
  Star _ -> True
  Quest _ -> True
  CallP {} -> True
  Init {} -> True
  _ -> False

lastIsPrim :: Proc -> Bool
lastIsPrim pr = case pr of
  While _ p -> lastIsPrim p
  IfElse _ _ p -> lastIsPrim p
  Forall _ p -> lastIsPrim p
  Switch l -> null l || lastIsPrim (snd $ last l)
  _ -> isPrim pr

ppBinProc :: Bool -> BinP -> Proc -> Doc
ppBinProc first b p = case p of
      BinP o ps | o <= b -> if first && not (null ps || isPrim (last ps))
                            then parens else id
      _ | first -> if isPrim p then id else parens
      _ | lastIsPrim p -> id
      _ -> parens
  $ ppProc p

ppBinP :: BinP -> Doc
ppBinP b = text $ case b of
  Semi -> "; "
  Pipe -> "| "
  SeqPlus -> "+> "

ppShip :: Ship -> Doc
ppShip s = case s of
  ShipP p -> ppProcess p
  ShipA a -> ppAction a
  ShipI i -> ppIndEffect i

ppShips :: [Ship] -> Doc
ppShips = vsep . map ppShip

aboxVar :: CharParser st [ABox]
aboxVar = liftM2 (\ ns c -> map (`AConcept` c) ns)
  (sepBy nominal commaP)
  (colonP >> concept)

aboxVars :: CharParser st [ABox]
aboxVars = flat $ sepBy aboxVar commaP

foltl, primFoltl, preFoltl, quantFoltl, andFoltl, orFoltl :: CharParser st Foltl

primFoltl = fmap ABoxass (try abox)
  <|> fmap (PreOp NotF) (skipKey "not" >> quantFoltl)
  <|> parent foltl

preFoltl = liftM2 PreOp
   (choice $ map (\ p -> skipKey (show p) >> return p) [X, F, G])
   foltl
   <|> primFoltl

quantFoltl = do
    q <- quant << skip
    as <- aboxVars
    bulletP
    f <- foltl
    return $ PreOp (QuantF q as) f
  <|> preFoltl
  <|> (option False (skipKey "run" >> return True) >>= callFoltl)

andFoltl = binP (JoinedF IntersectionOf) "and" quantFoltl
orFoltl = binP (JoinedF UnionOf) "or" andFoltl

impliesP :: GenParser Char st ()
impliesP = tryString "=>" >> skip

foltl = do
  f <- orFoltl
  option f $ liftM2 (BinOp f)
    ((skipKey "U" >> return Until) <|> (impliesP >> return Impl))
    foltl

optNoms :: GenParser Char st [String]
optNoms = optionL . parent $ sepBy nominal commaP

callFoltl :: Bool -> GenParser Char st Foltl
callFoltl b = liftM2 (Call b)
    (reserved (map show [X, F, G]
                   ++ ["run", "monitor", "and", "or", "U"]) nominal)
    optNoms

header :: CharParser st Header
header = liftM2 Header nominal optNoms << equalP

monitor :: CharParser st Monitor
monitor = do
  skipKey "monitor"
  h <- header
  mc <- optionMaybe $ char '"' >> many (noneOf "\n\"") << skipChar '"'
  f <- foltl
  return $ Monitor h mc f

mon :: CharParser st [Monitor]
mon = many1 monitor

aBoxLit :: CharParser st ABoxLit
aBoxLit = pair (option True $ skipKey "not" >> return False) abox

aBoxDelete :: CharParser st (Either ABoxLit [String])
aBoxDelete = fmap Right (skipKey "delete" >> parent (sepBy nominal commaP))
  <|> fmap Left aBoxLit

aBoxDeletes :: CharParser st ABoxDeletes
aBoxDeletes = sepBy aBoxDelete commaP

aBoxs :: CharParser st ABoxs
aBoxs = sepBy abox commaP

aBoxAnds :: CharParser st ABoxAnds
aBoxAnds = sepBy1 aBoxLit (skipKey "and")

condEffect :: CharParser st CondEffect
condEffect = skipKey "fi" >> liftM2 CondEffect (parent abox) aBoxDeletes

skipEqKey :: String -> CharParser st ()
skipEqKey s = skipKey s >> equalP

exec :: CharParser st Exec
exec = do
  let name = many1 myLetter
  skipEqKey "exec"
  s1 <- name << char '.'
  s2 <- name << skip
  ps <- optNoms
  return $ Exec s1 s2 ps

action :: CharParser st Action
action = do
  h <- skipKey "action" >> header
  braced $ do
    as <- optionL $ skipEqKey "pre" >> aBoxs
    ds <- optionL $ skipEqKey "effect" >> aBoxDeletes
    cs <- many condEffect
    me <- optionMaybe exec
    return $ Action h as ds cs me

indEffect :: CharParser st IndEffect
indEffect = do
  s <- skipKey "indirect" >> skipKey "effect" >> nominal
  equalP
  braced $ do
    as <- skipEqKey "init" >> aBoxs
    cs <- skipEqKey "causes" >> aBoxDeletes
    ds <- skipEqKey "cond" >> aBoxs
    return $ IndEffect s as cs ds

process :: CharParser st Process
process = skipKey "function" >> liftM2 Process header proc

primProc, starProc, preProc, semiProc, pipeProc, proc :: CharParser st Proc

primProc = braced proc
  <|> parent proc
  <|> fmap Init (try $ skipKey "init" >> foltl)
  <|> fmap Quest (try $ abox << skipChar '?')
  <|> liftM2 CallP
      (reserved ["while", "forall", "if", "switch"] nominal)
      optNoms

starProc = do
  p <- primProc
  ls <- many $ skipChar '*'
  return $ if null ls then p else Star p

preProc = liftM2 While (skipKey "while" >> parent aBoxAnds) proc
  <|> liftM3 IfElse (skipKey "if" >> parent aBoxAnds) proc
          (skipKey "else" >> proc)
  <|> liftM2 Forall (skipKey "forall" >> aBoxAnds) (impliesP >> proc)
  <|> fmap Switch (skipKey "switch" >>
         many (skipKey "case" >> pair
               (fmap Just aBoxAnds <|> (skipChar '_' >> return Nothing))
               (impliesP >> proc)))
  <|> starProc

semiProc = binC (BinP Semi) ';' preProc
pipeProc = binC (BinP Pipe) '|' semiProc
proc = binPP (BinP SeqPlus) ((tryString "+>" >> skip) <|> skipChar '+') pipeProc

ship :: CharParser st Ship
ship = fmap ShipP process <|> fmap ShipA action <|> fmap ShipI indEffect

ships :: CharParser st [Ship]
ships = many ship