1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# LANGUAGE DeriveDataTypeable #-}
d183a4514d8a5b6a5d48d15a8dff52d0c96691eaChristian MaederCopyright : (c) Till Mossakowski, C. Maeder, Uni Bremen 2004
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : till@informatik.uni-bremen.de
2a693c01b154f1e25931ff6c754d2d02096e2662Till MossakowskiStability : provisional
2a693c01b154f1e25931ff6c754d2d02096e2662Till MossakowskiPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederSignatures for modal logic, as extension of CASL signatures.
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Common.Lib.MapSet as MapSet
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederimport qualified Data.List as List
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Data.Map as Map
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maederdata ModalSign = ModalSign
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder { flexOps :: OpMap
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder , flexPreds :: PredMap
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder , modies :: Map.Map SIMPLE_ID [AnModFORM]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , termModies :: Map.Map Id [AnModFORM] -- SORT
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder } deriving (Show, Eq, Ord, Typeable, Data)
3a761fd74f4f3c5587a199553c0ee7383e5d8ff3Christian MaederemptyModalSign :: ModalSign
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederemptyModalSign = ModalSign MapSet.empty MapSet.empty Map.empty Map.empty
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederaddModalSign :: ModalSign -> ModalSign -> ModalSign
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederaddModalSign a b = a
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder { flexOps = addOpMapSet (flexOps a) $ flexOps b
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder , flexPreds = addMapSet (flexPreds a) $ flexPreds b
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , modies = Map.unionWith List.union (modies a) $ modies b
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder , termModies = Map.unionWith List.union (termModies a) $ termModies b }
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian MaederinterMap :: Ord a => ([b] -> [b] -> [b]) -> Map.Map a [b] -> Map.Map a [b]
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian MaederinterMap f m = Map.filter (not . null) . Map.intersectionWith f m
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian MaederinterModalSign :: ModalSign -> ModalSign -> ModalSign
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian MaederinterModalSign a b = a
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder { flexOps = interOpMapSet (flexOps a) $ flexOps b
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder , flexPreds = interMapSet (flexPreds a) $ flexPreds b
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder , modies = interMap List.intersect (modies a) $ modies b
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder , termModies = interMap List.intersect (termModies a) $ termModies b }
df6f4a9e6b3d0542ecc181fbc1bcec2affca1d30Christian MaederdiffModalSign :: ModalSign -> ModalSign -> ModalSign
df6f4a9e6b3d0542ecc181fbc1bcec2affca1d30Christian MaederdiffModalSign a b = a
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder { flexOps = diffOpMapSet (flexOps a) $ flexOps b
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder , flexPreds = diffMapSet (flexPreds a) $ flexPreds b
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder , modies = Map.differenceWith diffList (modies a) $ modies b
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder , termModies = Map.differenceWith diffList (termModies a) $ termModies b
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder } where diffList c d = let e = c List.\\ d in
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder if null e then Nothing else Just e
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederisSubModalSign :: ModalSign -> ModalSign -> Bool
9f29e77d1b758a260223874ac6956e290134cb9dChristian MaederisSubModalSign a b =
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder isSubOpMap (flexOps a) (flexOps b)
a9d7121d1cc6979e01f7968d5e51574fefb5b801Christian Maeder && isSubMap (flexPreds a) (flexPreds b)
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder && Map.isSubmapOfBy sublist (modies a) (modies b)
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder && Map.isSubmapOfBy sublist (termModies a) (termModies b)
42842d65f653c8c19dd15fe509f87c8d6e277a12Christian Maeder where sublist l1 l2 = List.union l2 l1 == l2