{-# LANGUAGE ExistentialQuantification, DeriveDataTypeable #-}

{- |

Module : $Header$

License : GPLv2 or higher, see LICENSE.txt

Maintainer : nevrenato@gmail.com

Stability : experimental

Portability : portable

Description :

Signature for an hybridized logic. Its constituted by

the declaration of nominals and modalities, and the signature

of the logic below

-}

module TopHybrid.TopHybridSign where

import TopHybrid.AS_TopHybrid

import Logic.Logic

import Common.Result

import Common.Id

import Data.Typeable

import Data.Set

import Unsafe.Coerce

import Control.Monad (liftM)

{- Prototype; a datatype that wraps the signature and the base logic

so that we can know which is the underlying logic, by only looking

to the signature

We have a total different constructor to represent the empty signagture;

we can't compute the an empty signature, without knowing the logic below,

hence we use the different constructor for that, which doesn't have the lid. -}

data Sgn_Wrap = forall l sub bs f s sm sign mo sy rw pf .

(Logic l sub bs f s sm sign mo sy rw pf) =>

Sgn_Wrap l (THybridSign sign)

| EmptySign

deriving Typeable

instance Show Sgn_Wrap where

show c = case c of

Sgn_Wrap l s -> "Sgn_Wrap " ++ show l ++ " (" ++ show s ++ ")"

EmptySign -> "EmptySign"

data THybridSign s = THybridSign

{

modies :: Set MODALITY

, nomies :: Set NOMINAL

, extended :: s

} deriving (Show, Eq, Ord)

emptyHybridSign :: Sgn_Wrap

emptyHybridSign = EmptySign

{- Unfortunately, the typechecker can't know that if (l == l') then

the extended signatures are the same. Thus, we will have to use unsafe

functions here. Also unfortunately the datatype Lids can't be directly compared

so we have to use their string representation, which is bijective, hence we can

compare in this way. -}

isSubTHybSgn :: Sgn_Wrap -> Sgn_Wrap -> Bool

isSubTHybSgn (Sgn_Wrap l s) (Sgn_Wrap l' s') = final

where

resExt = (show l == show l') &&

is_subsig l (extended s) (unsafeCoerce $ extended s')

final = isSubsetOf (modies s) (modies s') &&

isSubsetOf (nomies s) (nomies s') &&

resExt

-- An empty set is always contained in any other set

isSubTHybSgn EmptySign _ = True

-- A non empty set is never contained in an empty set

isSubTHybSgn _ EmptySign = False

{- Computes the difference between two signatures. If they belong to

different logics then throw an error -}

sgnDiff :: Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap

-- The difference between an emptySign and any other Sig results in an emptySig

sgnDiff EmptySign _ = return EmptySign

-- The difference between any sig and a empty sig results in the original sig

sgnDiff s EmptySign = return s

sgnDiff (Sgn_Wrap l s) (Sgn_Wrap l' s') =

if show l /= show l'

then Result [Diag Error "signatures belong to different logics"

nullRange] Nothing

else liftM (Sgn_Wrap l) ds

where

dn = difference (nomies s) $ nomies s'

dm = difference (modies s) $ modies s'

ds = liftM (THybridSign dm dn) $ signatureDiff l

(extended s) (unsafeCoerce $ extended s')

-- --- instances needed

instance Eq Sgn_Wrap where

(==) a b = isSubTHybSgn a b && isSubTHybSgn b a

instance Ord Sgn_Wrap where

compare a b = if a == b then EQ else GT