{- |

Module : ./CspCASL/LocalTop.hs

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