{- |
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 :: FORMULA f -> Maybe (FORMULA f, FORMULA f)
isImpl form :: FORMULA f
form = case FORMULA f
form of
  Relation f1 :: FORMULA f
f1 c :: Relation
c f2 :: FORMULA f
f2 _ | Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
/= Relation
Equivalence -> (FORMULA f, FORMULA f) -> Maybe (FORMULA f, FORMULA f)
forall a. a -> Maybe a
Just (FORMULA f
f1, FORMULA f
f2)
  _ -> Maybe (FORMULA f, FORMULA f)
forall a. Maybe a
Nothing

isBoxOrDiamond :: FORMULA M_FORMULA -> Maybe (Bool, MODALITY, FORMULA M_FORMULA)
isBoxOrDiamond :: FORMULA M_FORMULA -> Maybe (Bool, MODALITY, FORMULA M_FORMULA)
isBoxOrDiamond form :: FORMULA M_FORMULA
form = case FORMULA M_FORMULA
form of
  ExtFORMULA (BoxOrDiamond b :: Bool
b m :: MODALITY
m f :: FORMULA M_FORMULA
f _) -> (Bool, MODALITY, FORMULA M_FORMULA)
-> Maybe (Bool, MODALITY, FORMULA M_FORMULA)
forall a. a -> Maybe a
Just (Bool
b, MODALITY
m, FORMULA M_FORMULA
f)
  _ -> Maybe (Bool, MODALITY, FORMULA M_FORMULA)
forall a. Maybe a
Nothing

isPred :: FORMULA f -> Bool
isPred :: FORMULA f -> Bool
isPred form :: FORMULA f
form = case FORMULA f
form of
  Predication {} -> Bool
True
  _ -> Bool
False

-- matches: [](p=>q) => []p => []q
isBoxDistrImpl :: FORMULA M_FORMULA -> Maybe [MODALITY]
isBoxDistrImpl :: FORMULA M_FORMULA -> Maybe [MODALITY]
isBoxDistrImpl form :: FORMULA M_FORMULA
form = case FORMULA M_FORMULA -> Maybe (FORMULA M_FORMULA, FORMULA M_FORMULA)
forall f. FORMULA f -> Maybe (FORMULA f, FORMULA f)
isImpl FORMULA M_FORMULA
form of
  Just (f1 :: FORMULA M_FORMULA
f1, f2 :: FORMULA M_FORMULA
f2) -> case (FORMULA M_FORMULA -> Maybe (Bool, MODALITY, FORMULA M_FORMULA)
isBoxOrDiamond FORMULA M_FORMULA
f1, FORMULA M_FORMULA -> Maybe (FORMULA M_FORMULA, FORMULA M_FORMULA)
forall f. FORMULA f -> Maybe (FORMULA f, FORMULA f)
isImpl FORMULA M_FORMULA
f2) of
    (Just (True, m1 :: MODALITY
m1, f3 :: FORMULA M_FORMULA
f3), Just (f4 :: FORMULA M_FORMULA
f4, f5 :: FORMULA M_FORMULA
f5)) ->
        case (FORMULA M_FORMULA -> Maybe (FORMULA M_FORMULA, FORMULA M_FORMULA)
forall f. FORMULA f -> Maybe (FORMULA f, FORMULA f)
isImpl FORMULA M_FORMULA
f3, FORMULA M_FORMULA -> Maybe (Bool, MODALITY, FORMULA M_FORMULA)
isBoxOrDiamond FORMULA M_FORMULA
f4, FORMULA M_FORMULA -> Maybe (Bool, MODALITY, FORMULA M_FORMULA)
isBoxOrDiamond FORMULA M_FORMULA
f5) of
          (Just (p1 :: FORMULA M_FORMULA
p1, p2 :: FORMULA M_FORMULA
p2), Just (True, m2 :: MODALITY
m2, p3 :: FORMULA M_FORMULA
p3), Just (True, m3 :: MODALITY
m3, p4 :: FORMULA M_FORMULA
p4))
            | FORMULA M_FORMULA -> Bool
forall f. FORMULA f -> Bool
isPred FORMULA M_FORMULA
p1 Bool -> Bool -> Bool
&& FORMULA M_FORMULA
p1 FORMULA M_FORMULA -> FORMULA M_FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA M_FORMULA
p3 Bool -> Bool -> Bool
&& FORMULA M_FORMULA -> Bool
forall f. FORMULA f -> Bool
isPred FORMULA M_FORMULA
p2 Bool -> Bool -> Bool
&& FORMULA M_FORMULA
p2 FORMULA M_FORMULA -> FORMULA M_FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA M_FORMULA
p4
            -> [MODALITY] -> Maybe [MODALITY]
forall a. a -> Maybe a
Just [MODALITY
m1, MODALITY
m2, MODALITY
m3]
          _ -> Maybe [MODALITY]
forall a. Maybe a
Nothing
    _ -> Maybe [MODALITY]
forall a. Maybe a
Nothing
  _ -> Maybe [MODALITY]
forall a. Maybe a
Nothing

-- matches: []p => <>p
isSerial :: FORMULA M_FORMULA -> Maybe [MODALITY]
isSerial :: FORMULA M_FORMULA -> Maybe [MODALITY]
isSerial form :: FORMULA M_FORMULA
form = case FORMULA M_FORMULA -> Maybe (FORMULA M_FORMULA, FORMULA M_FORMULA)
forall f. FORMULA f -> Maybe (FORMULA f, FORMULA f)
isImpl FORMULA M_FORMULA
form of
  Just (f1 :: FORMULA M_FORMULA
f1, f2 :: FORMULA M_FORMULA
f2) -> case (FORMULA M_FORMULA -> Maybe (Bool, MODALITY, FORMULA M_FORMULA)
isBoxOrDiamond FORMULA M_FORMULA
f1, FORMULA M_FORMULA -> Maybe (Bool, MODALITY, FORMULA M_FORMULA)
isBoxOrDiamond FORMULA M_FORMULA
f2) of
    (Just (True, m1 :: MODALITY
m1, p1 :: FORMULA M_FORMULA
p1), Just (False, m2 :: MODALITY
m2, p2 :: FORMULA M_FORMULA
p2))
      | FORMULA M_FORMULA -> Bool
forall f. FORMULA f -> Bool
isPred FORMULA M_FORMULA
p1 Bool -> Bool -> Bool
&& FORMULA M_FORMULA
p1 FORMULA M_FORMULA -> FORMULA M_FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA M_FORMULA
p2 -> [MODALITY] -> Maybe [MODALITY]
forall a. a -> Maybe a
Just [MODALITY
m1, MODALITY
m2]
    _ -> Maybe [MODALITY]
forall a. Maybe a
Nothing
  Nothing -> Maybe [MODALITY]
forall a. Maybe a
Nothing

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

serialSen :: VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
serialSen :: VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
serialSen v1 :: VAR_DECL
v1 v2 :: VAR_DECL
v2 _ relP :: RELPRED
relP =
    [Char] -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed "Serial_D"
    (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
v1] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist [VAR_DECL
v2]
    (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ RELPRED
relP (VAR_DECL -> TERM ()
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
v1) (TERM () -> CASLFORMULA) -> TERM () -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ VAR_DECL -> TERM ()
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
v2

-- matches: []p => p
isReflex :: FORMULA M_FORMULA -> Maybe [MODALITY]
isReflex :: FORMULA M_FORMULA -> Maybe [MODALITY]
isReflex form :: FORMULA M_FORMULA
form = case FORMULA M_FORMULA -> Maybe (FORMULA M_FORMULA, FORMULA M_FORMULA)
forall f. FORMULA f -> Maybe (FORMULA f, FORMULA f)
isImpl FORMULA M_FORMULA
form of
  Just (f1 :: FORMULA M_FORMULA
f1, p1 :: FORMULA M_FORMULA
p1) | FORMULA M_FORMULA -> Bool
forall f. FORMULA f -> Bool
isPred FORMULA M_FORMULA
p1 -> case FORMULA M_FORMULA -> Maybe (Bool, MODALITY, FORMULA M_FORMULA)
isBoxOrDiamond FORMULA M_FORMULA
f1 of
    Just (True, m1 :: MODALITY
m1, p2 :: FORMULA M_FORMULA
p2) | FORMULA M_FORMULA
p1 FORMULA M_FORMULA -> FORMULA M_FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA M_FORMULA
p2 -> [MODALITY] -> Maybe [MODALITY]
forall a. a -> Maybe a
Just [MODALITY
m1]
    _ -> Maybe [MODALITY]
forall a. Maybe a
Nothing
  _ -> Maybe [MODALITY]
forall a. Maybe a
Nothing

reflexSen :: VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
reflexSen :: VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
reflexSen v1 :: VAR_DECL
v1 _ _ relP :: RELPRED
relP = let t :: TERM f
t = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
v1 in
    [Char] -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed "Reflexive_M"
    (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
v1] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ RELPRED
relP TERM ()
forall f. TERM f
t TERM ()
forall f. TERM f
t

-- matches: []p => [][]p
isTrans :: FORMULA M_FORMULA -> Maybe [MODALITY]
isTrans :: FORMULA M_FORMULA -> Maybe [MODALITY]
isTrans form :: FORMULA M_FORMULA
form = case FORMULA M_FORMULA -> Maybe (FORMULA M_FORMULA, FORMULA M_FORMULA)
forall f. FORMULA f -> Maybe (FORMULA f, FORMULA f)
isImpl FORMULA M_FORMULA
form of
  Just (f1 :: FORMULA M_FORMULA
f1, f2 :: FORMULA M_FORMULA
f2) -> case (FORMULA M_FORMULA -> Maybe (Bool, MODALITY, FORMULA M_FORMULA)
isBoxOrDiamond FORMULA M_FORMULA
f1, FORMULA M_FORMULA -> Maybe (Bool, MODALITY, FORMULA M_FORMULA)
isBoxOrDiamond FORMULA M_FORMULA
f2) of
    (Just (True, m1 :: MODALITY
m1, p1 :: FORMULA M_FORMULA
p1), Just (True, m2 :: MODALITY
m2, f3 :: FORMULA M_FORMULA
f3)) | FORMULA M_FORMULA -> Bool
forall f. FORMULA f -> Bool
isPred FORMULA M_FORMULA
p1 ->
        case FORMULA M_FORMULA -> Maybe (Bool, MODALITY, FORMULA M_FORMULA)
isBoxOrDiamond FORMULA M_FORMULA
f3 of
          Just (True, m3 :: MODALITY
m3, p2 :: FORMULA M_FORMULA
p2) | FORMULA M_FORMULA
p1 FORMULA M_FORMULA -> FORMULA M_FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA M_FORMULA
p2 -> [MODALITY] -> Maybe [MODALITY]
forall a. a -> Maybe a
Just [MODALITY
m1, MODALITY
m2, MODALITY
m3]
          _ -> Maybe [MODALITY]
forall a. Maybe a
Nothing
    _ -> Maybe [MODALITY]
forall a. Maybe a
Nothing
  Nothing -> Maybe [MODALITY]
forall a. Maybe a
Nothing

transSen :: Bool -> VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED
  -> Named CASLFORMULA
transSen :: Bool
-> VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
transSen b :: Bool
b v1 :: VAR_DECL
v1 v2 :: VAR_DECL
v2 v3 :: VAR_DECL
v3 relP :: RELPRED
relP = let
  t1 :: TERM f
t1 = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
v1
  t2 :: TERM f
t2 = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
v2
  t3 :: TERM f
t3 = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
v3
  in [Char] -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed "Transitive_4"
    (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
v1, VAR_DECL
v2, VAR_DECL
v3] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl
      ([CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [RELPRED
relP TERM ()
forall f. TERM f
t1 TERM ()
forall f. TERM f
t2, RELPRED
relP (if Bool
b then TERM ()
forall f. TERM f
t2 else TERM ()
forall f. TERM f
t1) TERM ()
forall f. TERM f
t3])
      (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ RELPRED
relP (if Bool
b then TERM ()
forall f. TERM f
t1 else TERM ()
forall f. TERM f
t2) TERM ()
forall f. TERM f
t3

isBoxDiamond :: FORMULA M_FORMULA -> Maybe (FORMULA M_FORMULA, [MODALITY])
isBoxDiamond :: FORMULA M_FORMULA -> Maybe (FORMULA M_FORMULA, [MODALITY])
isBoxDiamond form :: FORMULA M_FORMULA
form = case FORMULA M_FORMULA -> Maybe (Bool, MODALITY, FORMULA M_FORMULA)
isBoxOrDiamond FORMULA M_FORMULA
form of
  Just (True, m1 :: MODALITY
m1, f :: FORMULA M_FORMULA
f) -> case FORMULA M_FORMULA -> Maybe (Bool, MODALITY, FORMULA M_FORMULA)
isBoxOrDiamond FORMULA M_FORMULA
f of
    Just (False, m2 :: MODALITY
m2, p :: FORMULA M_FORMULA
p) -> (FORMULA M_FORMULA, [MODALITY])
-> Maybe (FORMULA M_FORMULA, [MODALITY])
forall a. a -> Maybe a
Just (FORMULA M_FORMULA
p, [MODALITY
m1, MODALITY
m2])
    _ -> Maybe (FORMULA M_FORMULA, [MODALITY])
forall a. Maybe a
Nothing
  _ -> Maybe (FORMULA M_FORMULA, [MODALITY])
forall a. Maybe a
Nothing

-- matches: p => []<>p
isSym :: FORMULA M_FORMULA -> Maybe [MODALITY]
isSym :: FORMULA M_FORMULA -> Maybe [MODALITY]
isSym form :: FORMULA M_FORMULA
form = case FORMULA M_FORMULA -> Maybe (FORMULA M_FORMULA, FORMULA M_FORMULA)
forall f. FORMULA f -> Maybe (FORMULA f, FORMULA f)
isImpl FORMULA M_FORMULA
form of
  Just (p1 :: FORMULA M_FORMULA
p1, f1 :: FORMULA M_FORMULA
f1) | FORMULA M_FORMULA -> Bool
forall f. FORMULA f -> Bool
isPred FORMULA M_FORMULA
p1 -> case FORMULA M_FORMULA -> Maybe (FORMULA M_FORMULA, [MODALITY])
isBoxDiamond FORMULA M_FORMULA
f1 of
    Just (p2 :: FORMULA M_FORMULA
p2, l :: [MODALITY]
l) | FORMULA M_FORMULA
p1 FORMULA M_FORMULA -> FORMULA M_FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA M_FORMULA
p2 -> [MODALITY] -> Maybe [MODALITY]
forall a. a -> Maybe a
Just [MODALITY]
l
    _ -> Maybe [MODALITY]
forall a. Maybe a
Nothing
  _ -> Maybe [MODALITY]
forall a. Maybe a
Nothing

symSen :: VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
symSen :: VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
symSen v1 :: VAR_DECL
v1 v2 :: VAR_DECL
v2 _ relP :: RELPRED
relP = let
  t1 :: TERM f
t1 = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
v1
  t2 :: TERM f
t2 = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
v2
  in [Char] -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed "Symmetric_B"
    (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
v1, VAR_DECL
v2] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl (RELPRED
relP TERM ()
forall f. TERM f
t1 TERM ()
forall f. TERM f
t2) (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ RELPRED
relP TERM ()
forall f. TERM f
t2 TERM ()
forall f. TERM f
t1

-- matches: <>p => []<>p
isEuklid :: FORMULA M_FORMULA -> Maybe [MODALITY]
isEuklid :: FORMULA M_FORMULA -> Maybe [MODALITY]
isEuklid form :: FORMULA M_FORMULA
form = case FORMULA M_FORMULA -> Maybe (FORMULA M_FORMULA, FORMULA M_FORMULA)
forall f. FORMULA f -> Maybe (FORMULA f, FORMULA f)
isImpl FORMULA M_FORMULA
form of
  Just (f1 :: FORMULA M_FORMULA
f1, f2 :: FORMULA M_FORMULA
f2) -> case FORMULA M_FORMULA -> Maybe (Bool, MODALITY, FORMULA M_FORMULA)
isBoxOrDiamond FORMULA M_FORMULA
f1 of
    Just (False, m1 :: MODALITY
m1, p1 :: FORMULA M_FORMULA
p1) | FORMULA M_FORMULA -> Bool
forall f. FORMULA f -> Bool
isPred FORMULA M_FORMULA
p1 -> case FORMULA M_FORMULA -> Maybe (FORMULA M_FORMULA, [MODALITY])
isBoxDiamond FORMULA M_FORMULA
f2 of
      Just (p2 :: FORMULA M_FORMULA
p2, l :: [MODALITY]
l) | FORMULA M_FORMULA
p1 FORMULA M_FORMULA -> FORMULA M_FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA M_FORMULA
p2 -> [MODALITY] -> Maybe [MODALITY]
forall a. a -> Maybe a
Just ([MODALITY] -> Maybe [MODALITY]) -> [MODALITY] -> Maybe [MODALITY]
forall a b. (a -> b) -> a -> b
$ MODALITY
m1 MODALITY -> [MODALITY] -> [MODALITY]
forall a. a -> [a] -> [a]
: [MODALITY]
l
      _ -> Maybe [MODALITY]
forall a. Maybe a
Nothing
    _ -> Maybe [MODALITY]
forall a. Maybe a
Nothing
  Nothing -> Maybe [MODALITY]
forall a. Maybe a
Nothing

euklidSen :: VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
euklidSen :: VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
euklidSen = Bool
-> VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
transSen Bool
False

transSchemaMFormula :: ([VAR] -> TERM M_FORMULA -> TERM ())
                    -> SORT -> PRED_NAME -> [VAR]
                    -> AnModFORM -> Maybe (Named CASLFORMULA)
transSchemaMFormula :: ([VAR] -> TERM M_FORMULA -> TERM ())
-> SORT -> SORT -> [VAR] -> AnModFORM -> Maybe (Named CASLFORMULA)
transSchemaMFormula mapT :: [VAR] -> TERM M_FORMULA -> TERM ()
mapT world :: SORT
world rel :: SORT
rel vars :: [VAR]
vars anMF :: AnModFORM
anMF = case [VAR]
vars of
  w1 :: VAR
w1 : w2 :: VAR
w2 : w3 :: VAR
w3 : _ -> let
    m :: [(FORMULA M_FORMULA -> Maybe [MODALITY],
  VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA)]
m = [ (FORMULA M_FORMULA -> Maybe [MODALITY]
isSerial, VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
serialSen)
        , (FORMULA M_FORMULA -> Maybe [MODALITY]
isReflex, VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
reflexSen)
        , (FORMULA M_FORMULA -> Maybe [MODALITY]
isTrans, Bool
-> VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
transSen Bool
True)
        , (FORMULA M_FORMULA -> Maybe [MODALITY]
isSym, VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
symSen)
        , (FORMULA M_FORMULA -> Maybe [MODALITY]
isEuklid, VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
euklidSen) ]
    relPred :: TERM f -> TERM f -> FORMULA f
relPred t1 :: TERM f
t1 t2 :: TERM f
t2 = PRED_SYMB -> [TERM f] -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication
      (SORT -> PRED_TYPE -> PRED_SYMB
mkQualPred SORT
rel (PRED_TYPE -> PRED_SYMB) -> PRED_TYPE -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ [SORT] -> Range -> PRED_TYPE
Pred_type [SORT
world, SORT
world] Range
nullRange)
      [TERM f
t1, TERM f
t2]
   in case (AnModFORM -> [Char]
forall a. Annoted a -> [Char]
getRLabel AnModFORM
anMF, AnModFORM -> FORMULA M_FORMULA
forall a. Annoted a -> a
item AnModFORM
anMF) of
      (_label :: [Char]
_label, f :: FORMULA M_FORMULA
f) -> case FORMULA M_FORMULA -> Maybe [MODALITY]
isBoxDistrImpl FORMULA M_FORMULA
f of
          Just l :: [MODALITY]
l -> ([VAR] -> TERM M_FORMULA -> TERM ())
-> SORT
-> [Maybe (TERM M_FORMULA)]
-> [VAR]
-> Maybe (Named CASLFORMULA)
-> Maybe (Named CASLFORMULA)
addTerm [VAR] -> TERM M_FORMULA -> TERM ()
mapT SORT
rel ((MODALITY -> Maybe (TERM M_FORMULA))
-> [MODALITY] -> [Maybe (TERM M_FORMULA)]
forall a b. (a -> b) -> [a] -> [b]
map MODALITY -> Maybe (TERM M_FORMULA)
modToTerm [MODALITY]
l) [VAR]
vars Maybe (Named CASLFORMULA)
forall a. Maybe a
Nothing
          _ -> case ((Maybe [MODALITY],
  VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA)
 -> Bool)
-> [(Maybe [MODALITY],
     VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA)]
-> [(Maybe [MODALITY],
     VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe [MODALITY] -> Bool
forall a. Maybe a -> Bool
isJust (Maybe [MODALITY] -> Bool)
-> ((Maybe [MODALITY],
     VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA)
    -> Maybe [MODALITY])
-> (Maybe [MODALITY],
    VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe [MODALITY],
 VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA)
-> Maybe [MODALITY]
forall a b. (a, b) -> a
fst) ([(Maybe [MODALITY],
   VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA)]
 -> [(Maybe [MODALITY],
      VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA)])
-> [(Maybe [MODALITY],
     VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA)]
-> [(Maybe [MODALITY],
     VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA)]
forall a b. (a -> b) -> a -> b
$ ((FORMULA M_FORMULA -> Maybe [MODALITY],
  VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA)
 -> (Maybe [MODALITY],
     VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA))
-> [(FORMULA M_FORMULA -> Maybe [MODALITY],
     VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA)]
-> [(Maybe [MODALITY],
     VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: FORMULA M_FORMULA -> Maybe [MODALITY]
p, cf :: VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
cf) -> (FORMULA M_FORMULA -> Maybe [MODALITY]
p FORMULA M_FORMULA
f, VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
cf)) [(FORMULA M_FORMULA -> Maybe [MODALITY],
  VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA)]
m of
            (Just l :: [MODALITY]
l, cf :: VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
cf) : _ -> ([VAR] -> TERM M_FORMULA -> TERM ())
-> SORT
-> [Maybe (TERM M_FORMULA)]
-> [VAR]
-> Maybe (Named CASLFORMULA)
-> Maybe (Named CASLFORMULA)
addTerm [VAR] -> TERM M_FORMULA -> TERM ()
mapT SORT
rel ((MODALITY -> Maybe (TERM M_FORMULA))
-> [MODALITY] -> [Maybe (TERM M_FORMULA)]
forall a b. (a -> b) -> [a] -> [b]
map MODALITY -> Maybe (TERM M_FORMULA)
modToTerm [MODALITY]
l) [VAR]
vars
               (Maybe (Named CASLFORMULA) -> Maybe (Named CASLFORMULA))
-> Maybe (Named CASLFORMULA) -> Maybe (Named CASLFORMULA)
forall a b. (a -> b) -> a -> b
$ Named CASLFORMULA -> Maybe (Named CASLFORMULA)
forall a. a -> Maybe a
Just (Named CASLFORMULA -> Maybe (Named CASLFORMULA))
-> Named CASLFORMULA -> Maybe (Named CASLFORMULA)
forall a b. (a -> b) -> a -> b
$ VAR_DECL -> VAR_DECL -> VAR_DECL -> RELPRED -> Named CASLFORMULA
cf (VAR -> SORT -> VAR_DECL
mkVarDecl VAR
w1 SORT
world) (VAR -> SORT -> VAR_DECL
mkVarDecl VAR
w2 SORT
world)
                 (VAR -> SORT -> VAR_DECL
mkVarDecl VAR
w3 SORT
world) RELPRED
forall f. TERM f -> TERM f -> FORMULA f
relPred
            _ -> Maybe (Named CASLFORMULA)
forall a. Maybe a
Nothing
              -- was error ("Modal2CASL: unknown formula: " ++ showDoc f "")
  _ -> [Char] -> Maybe (Named CASLFORMULA)
forall a. HasCallStack => [Char] -> a
error "transSchemaMFormula"