5056N/A{-# LANGUAGE DeriveDataTypeable #-}

5056N/A{- |

5056N/AModule : ./Modal/ModalSign.hs

5056N/ACopyright : (c) Till Mossakowski, C. Maeder, Uni Bremen 2004

5056N/ALicense : GPLv2 or higher, see LICENSE.txt

5056N/A

5056N/AMaintainer : till@informatik.uni-bremen.de

5056N/AStability : provisional

5056N/APortability : portable

5056N/A

5056N/ASignatures for modal logic, as extension of CASL signatures.

5056N/A-}

5056N/A

5056N/Amodule Modal.ModalSign where

5056N/A

5056N/Aimport Modal.AS_Modal

5056N/A

5056N/Aimport CASL.Sign

5056N/A

5056N/Aimport qualified Common.Lib.MapSet as MapSet

5784N/Aimport Common.Id

5056N/A

5784N/Aimport Data.Data

5784N/Aimport qualified Data.List as List

5784N/Aimport qualified Data.Map as Map

5056N/A

5056N/Adata ModalSign = ModalSign

5056N/A { flexOps :: OpMap

5056N/A , flexPreds :: PredMap

5056N/A , modies :: Map.Map SIMPLE_ID [AnModFORM]

5056N/A , termModies :: Map.Map Id [AnModFORM] -- SORT

5056N/A } deriving (Show, Eq, Ord, Typeable, Data)

5056N/A

5056N/AemptyModalSign :: ModalSign

5056N/AemptyModalSign = ModalSign MapSet.empty MapSet.empty Map.empty Map.empty

5784N/A

5784N/AaddModalSign :: ModalSign -> ModalSign -> ModalSign

5784N/AaddModalSign a b = a

5056N/A { flexOps = addOpMapSet (flexOps a) $ flexOps b

5056N/A , flexPreds = addMapSet (flexPreds a) $ flexPreds b

5056N/A , modies = Map.unionWith List.union (modies a) $ modies b

5056N/A , termModies = Map.unionWith List.union (termModies a) $ termModies b }

5056N/A

5056N/AinterMap :: Ord a => ([b] -> [b] -> [b]) -> Map.Map a [b] -> Map.Map a [b]

5056N/A -> Map.Map a [b]

5152N/AinterMap f m = Map.filter (not . null) . Map.intersectionWith f m

5152N/A

5056N/AinterModalSign :: ModalSign -> ModalSign -> ModalSign

5056N/AinterModalSign a b = a

5056N/A { flexOps = interOpMapSet (flexOps a) $ flexOps b

5056N/A , flexPreds = interMapSet (flexPreds a) $ flexPreds b

5056N/A , modies = interMap List.intersect (modies a) $ modies b

5056N/A , termModies = interMap List.intersect (termModies a) $ termModies b }

diffModalSign :: ModalSign -> ModalSign -> ModalSign

diffModalSign a b = a

{ flexOps = diffOpMapSet (flexOps a) $ flexOps b

, flexPreds = diffMapSet (flexPreds a) $ flexPreds b

, modies = Map.differenceWith diffList (modies a) $ modies b

, termModies = Map.differenceWith diffList (termModies a) $ termModies b

} where diffList c d = let e = c List.\\ d in

if null e then Nothing else Just e

isSubModalSign :: ModalSign -> ModalSign -> Bool

isSubModalSign a b =

isSubOpMap (flexOps a) (flexOps b)

&& isSubMap (flexPreds a) (flexPreds b)

&& Map.isSubmapOfBy sublist (modies a) (modies b)

&& Map.isSubmapOfBy sublist (termModies a) (termModies b)

where sublist l1 l2 = List.union l2 l1 == l2