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