{- |

Module : $Header$

Copyright : DFKI GmbH 2011

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

-}

module Modal.ModalSystems (transSchemaMFormula) where

import Common.DocUtils

import Common.AS_Annotation

import Common.Id

-- CASL

import CASL.AS_Basic_CASL

-- ModalCASL

import Modal.AS_Modal

import Modal.Print_AS ()

import Modal.Utils

import Data.Maybe (isJust)

isImpl :: FORMULA f -> Maybe (FORMULA f, FORMULA f)

isImpl form = case form of

Implication f1 f2 b _ -> if b then Just (f1, f2) else Just (f2, f1)

_ -> Nothing

isBoxOrDiamond :: FORMULA M_FORMULA -> Maybe (Bool, MODALITY, FORMULA M_FORMULA)

isBoxOrDiamond form = case form of

ExtFORMULA (BoxOrDiamond b m f _) -> Just (b, m, f)

_ -> Nothing

isPred :: FORMULA f -> Bool

isPred form = case form of

Predication _ _ _ -> True

_ -> False

-- matches: [](p=>q) => []p => []q

isBoxDistrImpl :: FORMULA M_FORMULA -> Maybe [MODALITY]

isBoxDistrImpl form = case isImpl form of

Just (f1, f2) -> case (isBoxOrDiamond f1, isImpl f2) of

(Just (True, m1, f3), Just (f4, f5)) ->

case (isImpl f3, isBoxOrDiamond f4, isBoxOrDiamond f5) of

(Just (p1, p2), Just (True, m2, p3), Just (True, m3, p4))

| isPred p1 && p1 == p3 && isPred p2 && p2 == p4

-> Just [m1, m2, m3]

_ -> Nothing

_ -> Nothing

_ -> Nothing

-- matches: []p => <>p

isSerial :: FORMULA M_FORMULA -> Maybe [MODALITY]

isSerial form = case isImpl form of

Just (f1, f2) -> case (isBoxOrDiamond f1, isBoxOrDiamond f2) of

(Just (True, m1, p1), Just (False, m2, p2))

| isPred p1 && p1 == p2 -> Just [m1, m2]

_ -> Nothing

Nothing -> Nothing

type RELPRED = TERM () -> TERM () -> CASLFORMULA

serialSen :: VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA

serialSen v1 v2 _ relP =

makeNamed "Serial_D"

$ mkForall [v1] $ mkExist [v2]

$ relP (toQualVar v1) $ toQualVar v2

-- matches: []p => p

isReflex :: FORMULA M_FORMULA -> Maybe [MODALITY]

isReflex form = case isImpl form of

Just (f1, p1) | isPred p1 -> case isBoxOrDiamond f1 of

Just (True, m1, p2) | p1 == p2 -> Just [m1]

_ -> Nothing

_ -> Nothing

reflexSen :: VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA

reflexSen v1 _ _ relP = let t = toQualVar v1 in

makeNamed "Reflexive_M"

$ mkForall [v1] $ relP t t

-- matches: []p => [][]p

isTrans :: FORMULA M_FORMULA -> Maybe [MODALITY]

isTrans form = case isImpl form of

Just (f1, f2) -> case (isBoxOrDiamond f1, isBoxOrDiamond f2) of

(Just (True, m1, p1), Just (True, m2, f3)) | isPred p1 ->

case isBoxOrDiamond f3 of

Just (True, m3, p2) | p1 == p2 -> Just [m1, m2, m3]

_ -> Nothing

_ -> Nothing

Nothing -> Nothing

transSen :: Bool -> VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED

-> Named CASLFORMULA

transSen b v1 v2 v3 relP = let

t1 = toQualVar v1

t2 = toQualVar v2

t3 = toQualVar v3

in makeNamed "Transitive_4"

$ mkForall [v1, v2, v3] $ mkImpl

(conjunct [relP t1 t2, relP (if b then t2 else t1) t3])

$ relP (if b then t1 else t2) t3

isBoxDiamond :: FORMULA M_FORMULA -> Maybe (FORMULA M_FORMULA, [MODALITY])

isBoxDiamond form = case isBoxOrDiamond form of

Just (True, m1, f) -> case isBoxOrDiamond f of

Just (False, m2, p) -> Just (p, [m1, m2])

_ -> Nothing

_ -> Nothing

-- matches: p => []<>p

isSym :: FORMULA M_FORMULA -> Maybe [MODALITY]

isSym form = case isImpl form of

Just (p1, f1) | isPred p1 -> case isBoxDiamond f1 of

Just (p2, l) | p1 == p2 -> Just l

_ -> Nothing

_ -> Nothing

symSen :: VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA

symSen v1 v2 _ relP = let

t1 = toQualVar v1

t2 = toQualVar v2

in makeNamed "Symmetric_B"

$ mkForall [v1, v2] $ mkImpl (relP t1 t2) $ relP t2 t1

-- matches: <>p => []<>p

isEuklid :: FORMULA M_FORMULA -> Maybe [MODALITY]

isEuklid form = case isImpl form of

Just (f1, f2) -> case isBoxOrDiamond f1 of

Just (False, m1, p1) | isPred p1 -> case isBoxDiamond f2 of

Just (p2, l) | p1 == p2 -> Just $ m1 : l

_ -> Nothing

_ -> Nothing

Nothing -> Nothing

euklidSen :: VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA

euklidSen = transSen False

transSchemaMFormula :: ([VAR] -> TERM M_FORMULA -> TERM ())

-> SORT -> PRED_NAME -> [VAR]

-> AnModFORM -> Maybe (Named CASLFORMULA)

transSchemaMFormula mapT world rel vars anMF = case vars of

w1 : w2 : w3 : _ -> let

m = [ (isSerial, serialSen)

, (isReflex, reflexSen)

, (isTrans, transSen True)

, (isSym, symSen)

, (isEuklid, euklidSen) ]

relPred t1 t2 = mkPredication

(mkQualPred rel $ Pred_type [world, world] nullRange)

[t1, t2]

in case (getRLabel anMF, item anMF) of

(_label, f) -> case isBoxDistrImpl f of

Just l -> addTerm mapT rel (map modToTerm l) vars Nothing

_ -> case filter (isJust . fst) $ map (\ (p, cf) -> (p f, cf)) m of

(Just l, cf) : _ -> addTerm mapT rel (map modToTerm l) vars

$ Just $ cf (mkVarDecl w1 world) (mkVarDecl w2 world)

(mkVarDecl w3 world) relPred

_ -> error ("Modal2CASL: unknown formula: " ++ showDoc f "") Nothing

_ -> error "transSchemaMFormula"