{- |
Module : ./Modal/ModalSystems.hs
Copyright : DFKI GmbH 2011
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : portable
-}
-- previously generated via GeneratePatterns and utils/genTransMFormFunc.pl
module Modal.ModalSystems (transSchemaMFormula) where
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
Relation f1 c f2 _ | c /= Equivalence -> Just (f1, f2)
_ -> 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
_ -> Nothing
-- was error ("Modal2CASL: unknown formula: " ++ showDoc f "")
_ -> error "transSchemaMFormula"