{- |

Module : $Header$

Description : Local top element analysis for CspCASL specifications

Copyright : (c) Andy Gimblett, Swansea University 2007

License : GPLv2 or higher, see LICENSE.txt

Maintainer : a.m.gimblett@swan.ac.uk

Stability : provisional

Portability : portable

Analysis of relations for presence of local top elements. Used by

CspCASL static analysis.

-}

module CspCASL.LocalTop (

checkLocalTops,

cartesian

) where

import CASL.AS_Basic_CASL (SORT)

import qualified Common.Lib.Rel as Rel

import Common.Result (Diagnosis(..), mkDiag, DiagKind(..))

import qualified Data.Set as S

import Data.Maybe

-- | A relation is a set of pairs.

type Relation a b = S.Set (a, b)

type BinaryRelation a = Relation a a

-- | We're interested in triples where two elements are both in relation

-- with some third object. We represent this as a Obligation, where

-- the first element is the shared one. It's important to note that

-- (Obligation x y z) == (Obligation x z y), which we encode here. For

-- every obligation, we look for any corresponding top elements.

data Obligation a = Obligation a a a

instance Eq a => Eq (Obligation a) where

(Obligation n m o) == (Obligation x y z) =

(n==x) && ((m,o)==(y,z) || (m,o)==(z,y))

instance Ord a => Ord (Obligation a) where

compare (Obligation n m o) (Obligation x y z)

| (Obligation n m o) == (Obligation x y z) = EQ

| otherwise = compare (n,m,o) (x,y,z)

instance Show a => Show (Obligation a) where

show (Obligation x y z) = show [x,y,z]

-- | Turn a binary relation into a set mapping its obligation elements to

-- their corresponding local top elements (if any).

localTops :: Ord a => BinaryRelation a -> S.Set (Obligation a, S.Set a)

localTops r = S.map (\x -> (x, m x)) (obligations r)

where m = findTops $ cartesian r

-- | Find all the obligations in a binary relation, by searching its

-- cartesian product for elements of the right form.

obligations :: Ord a => BinaryRelation a -> S.Set (Obligation a)

obligations r = stripMaybe $ S.map isObligation (cartesian r)

where isObligation ((w,x),(y,z)) =

if (w==y) && (x /= z) && (w /= z) && (w /= x)

then Just (Obligation w x z)

else Nothing

-- | Given a binary relation's cartesian product and a obligation, look

-- for corresponding top elements in that product.

findTops :: Ord a => BinaryRelation (a,a) -> (Obligation a) -> S.Set a

findTops c cand = S.map get_top (S.filter (is_top cand) c)

where is_top (Obligation _ y z) ((m,n),(o,p))=((m==y)&&(o==z)&&(n==p))

get_top ((_,_),(_,p)) = p

-- Utility functions.

-- | Cartesian product of a set.

cartesian :: Ord a => S.Set a -> S.Set (a,a)

cartesian x = S.fromDistinctAscList [(i,j) | i <- xs, j <- xs]

where xs = S.toAscList x

-- fromDistinctAscList sorted precondition satisfied by construction

-- | Given a set of Maybes, filter to keep only the Justs

stripMaybe :: Ord a => S.Set (Maybe a) -> S.Set a

stripMaybe x = S.fromList $ catMaybes $ S.toList x

-- | Given a binary relation, compute its reflexive closure.

reflexiveClosure :: Ord a => BinaryRelation a -> BinaryRelation a

reflexiveClosure r = S.fold add_refl r r

where add_refl (x, y) r' = (x, x) `S.insert` ((y, y) `S.insert` r')

-- | Main function for CspCASL LTE checks: given a

-- transitively-closed subsort relation as a list of pairs, return a

-- list of unfulfilled LTE obligations.

unmetObs :: Ord a => [(a,a)] -> [Obligation a]

unmetObs r = unmets

where l = S.toList $ localTops $ reflexiveClosure $ S.fromList r

unmets = map fst $ filter (S.null . snd) l

-- Wrapper functions follow that allow easy calling for various situations

-- (static analysis and signature union).

-- | Add diagnostic error message for every unmet local top element

-- obligation.

lteError :: Obligation SORT -> Diagnosis

lteError (Obligation x y z) = mkDiag Error msg ()

where msg = ("local top element obligation ("

++ (show x) ++ " < " ++ (show y) ++ ", " ++ (show z)

++ ") unfulfilled")

-- | This is the main interface for the LTE check. Check a CspCASL signature

-- (actually just the sort relation) for local top elements in its subsort

-- relation. Returns empty list for sucess or a list of diags for failure where

-- diags is a list of diagnostic errors resulting from the check.

checkLocalTops :: Rel.Rel SORT -> [Diagnosis]

checkLocalTops sr =

let obs = unmetObs $ Rel.toList $ Rel.transClosure $ sr

in map lteError obs