hets/Hybrid/HybridSign.hs

{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Hybrid/HybridSign.hs
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 Data.Data
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, Typeable, Data)

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