{- |

Module : $Header$

License : GPLv2 or higher, see LICENSE.txt

Stability : provisional

Portability : portable

Signatures for hybrid logic, as extension of CASL signatures.

-}

module Hybrid.HybridSign where

import Hybrid.AS_Hybrid

import CASL.Sign

import qualified Common.Lib.MapSet as MapSet

import Common.Id

import qualified Data.List as List

import qualified Data.Map as Map

data HybridSign = HybridSign

{ rigidOps :: OpMap

, rigidPreds :: PredMap

, modies :: Map.Map SIMPLE_ID [AnHybFORM]

, nomies :: Map.Map SIMPLE_ID [AnHybFORM]

, termModies :: Map.Map Id [AnHybFORM] -- SORT

} deriving (Show, Eq, Ord)

emptyHybridSign :: HybridSign

emptyHybridSign = HybridSign MapSet.empty MapSet.empty

Map.empty Map.empty Map.empty

addHybridSign :: HybridSign -> HybridSign -> HybridSign

addHybridSign a b = a

{ rigidOps = addOpMapSet (rigidOps a) $ rigidOps b

, rigidPreds = addMapSet (rigidPreds a) $ rigidPreds b

, modies = Map.unionWith List.union (modies a) $ modies b

, nomies = Map.unionWith List.union (nomies a) (nomies b)

, termModies = Map.unionWith List.union (termModies a) $ termModies b }

interMap :: Ord a => ([b] -> [b] -> [b]) -> Map.Map a [b] -> Map.Map a [b]

-> Map.Map a [b]

interMap f m = Map.filter (not . null) . Map.intersectionWith f m

interHybridSign :: HybridSign -> HybridSign -> HybridSign

interHybridSign a b = a

{ rigidOps = interOpMapSet (rigidOps a) $ rigidOps b

, rigidPreds = interMapSet (rigidPreds a) $ rigidPreds b

, modies = interMap List.intersect (modies a) $ modies b

, nomies = interMap List.intersect (nomies a) (nomies b)

, termModies = interMap List.intersect (termModies a) $ termModies b }

diffHybridSign :: HybridSign -> HybridSign -> HybridSign

diffHybridSign a b = a

{ rigidOps = diffOpMapSet (rigidOps a) $ rigidOps b

, rigidPreds = diffMapSet (rigidPreds a) $ rigidPreds b

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

, nomies = Map.differenceWith diffList (nomies a) (nomies 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

isSubHybridSign :: HybridSign -> HybridSign -> Bool

isSubHybridSign a b =

isSubOpMap (rigidOps a) (rigidOps b)

&& isSubMap (rigidPreds a) (rigidPreds b)

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

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

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

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