{- |

Module : ./ExtModal/Ship.hs

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