{- |
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 :: a
n m :: a
m o :: a
o) == :: Obligation a -> Obligation a -> Bool
== (Obligation x :: a
x y :: a
y z :: a
z) =
        (a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x) Bool -> Bool -> Bool
&& ((a
m, a
o) (a, a) -> (a, a) -> Bool
forall a. Eq a => a -> a -> Bool
== (a
y, a
z) Bool -> Bool -> Bool
|| (a
m, a
o) (a, a) -> (a, a) -> Bool
forall a. Eq a => a -> a -> Bool
== (a
z, a
y))
instance Ord a => Ord (Obligation a) where
    compare :: Obligation a -> Obligation a -> Ordering
compare (Obligation n :: a
n m :: a
m o :: a
o) (Obligation x :: a
x y :: a
y z :: a
z)
        | a -> a -> a -> Obligation a
forall a. a -> a -> a -> Obligation a
Obligation a
n a
m a
o Obligation a -> Obligation a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a -> a -> Obligation a
forall a. a -> a -> a -> Obligation a
Obligation a
x a
y a
z = Ordering
EQ
        | Bool
otherwise = (a, a, a) -> (a, a, a) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (a
n, a
m, a
o) (a
x, a
y, a
z)
instance Show a => Show (Obligation a) where
    show :: Obligation a -> String
show (Obligation x :: a
x y :: a
y z :: a
z) = [a] -> String
forall a. Show a => a -> String
show [a
x, a
y, a
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 :: BinaryRelation a -> Set (Obligation a, Set a)
localTops r :: BinaryRelation a
r = (Obligation a -> (Obligation a, Set a))
-> Set (Obligation a) -> Set (Obligation a, Set a)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (\ x :: Obligation a
x -> (Obligation a
x, Obligation a -> Set a
m Obligation a
x)) (BinaryRelation a -> Set (Obligation a)
forall a. Ord a => BinaryRelation a -> Set (Obligation a)
obligations BinaryRelation a
r)
    where m :: Obligation a -> Set a
m = BinaryRelation (a, a) -> Obligation a -> Set a
forall a. Ord a => BinaryRelation (a, a) -> Obligation a -> Set a
findTops (BinaryRelation (a, a) -> Obligation a -> Set a)
-> BinaryRelation (a, a) -> Obligation a -> Set a
forall a b. (a -> b) -> a -> b
$ BinaryRelation a -> BinaryRelation (a, a)
forall a. Ord a => Set a -> Set (a, a)
cartesian BinaryRelation a
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 :: BinaryRelation a -> Set (Obligation a)
obligations r :: BinaryRelation a
r = Set (Maybe (Obligation a)) -> Set (Obligation a)
forall a. Ord a => Set (Maybe a) -> Set a
stripMaybe (Set (Maybe (Obligation a)) -> Set (Obligation a))
-> Set (Maybe (Obligation a)) -> Set (Obligation a)
forall a b. (a -> b) -> a -> b
$ (((a, a), (a, a)) -> Maybe (Obligation a))
-> Set ((a, a), (a, a)) -> Set (Maybe (Obligation a))
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map ((a, a), (a, a)) -> Maybe (Obligation a)
forall a. Eq a => ((a, a), (a, a)) -> Maybe (Obligation a)
isObligation (BinaryRelation a -> Set ((a, a), (a, a))
forall a. Ord a => Set a -> Set (a, a)
cartesian BinaryRelation a
r)
    where isObligation :: ((a, a), (a, a)) -> Maybe (Obligation a)
isObligation ((w :: a
w, x :: a
x), (y :: a
y, z :: a
z)) =
              if (a
w a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y) Bool -> Bool -> Bool
&& (a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
z) Bool -> Bool -> Bool
&& (a
w a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
z) Bool -> Bool -> Bool
&& (a
w a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
x)
              then Obligation a -> Maybe (Obligation a)
forall a. a -> Maybe a
Just (a -> a -> a -> Obligation a
forall a. a -> a -> a -> Obligation a
Obligation a
w a
x a
z)
              else Maybe (Obligation a)
forall a. Maybe a
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 :: BinaryRelation (a, a) -> Obligation a -> Set a
findTops c :: BinaryRelation (a, a)
c cand :: Obligation a
cand = (((a, a), (a, a)) -> a) -> BinaryRelation (a, a) -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map ((a, a), (a, a)) -> a
forall a b a b. ((a, b), (a, b)) -> b
get_top ((((a, a), (a, a)) -> Bool)
-> BinaryRelation (a, a) -> BinaryRelation (a, a)
forall a. (a -> Bool) -> Set a -> Set a
S.filter (Obligation a -> ((a, a), (a, a)) -> Bool
forall a a.
(Eq a, Eq a) =>
Obligation a -> ((a, a), (a, a)) -> Bool
is_top Obligation a
cand) BinaryRelation (a, a)
c)
    where is_top :: Obligation a -> ((a, a), (a, a)) -> Bool
is_top (Obligation _ y :: a
y z :: a
z) ((m :: a
m, n :: a
n), (o :: a
o, p :: a
p)) = (a
m a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y Bool -> Bool -> Bool
&& a
o a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
z) Bool -> Bool -> Bool
&& (a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
p)
          get_top :: ((a, b), (a, b)) -> b
get_top ((_, _), (_, p :: b
p)) = b
p


-- Utility functions.

-- | Cartesian product of a set.
cartesian :: Ord a => S.Set a -> S.Set (a, a)
cartesian :: Set a -> Set (a, a)
cartesian x :: Set a
x = [(a, a)] -> Set (a, a)
forall a. [a] -> Set a
S.fromDistinctAscList [(a
i, a
j) | a
i <- [a]
xs, a
j <- [a]
xs]
    where xs :: [a]
xs = Set a -> [a]
forall a. Set a -> [a]
S.toAscList Set a
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 :: Set (Maybe a) -> Set a
stripMaybe x :: Set (Maybe a)
x = [a] -> Set a
forall a. Ord a => [a] -> Set a
S.fromList ([a] -> Set a) -> [a] -> Set a
forall a b. (a -> b) -> a -> b
$ [Maybe a] -> [a]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe a] -> [a]) -> [Maybe a] -> [a]
forall a b. (a -> b) -> a -> b
$ Set (Maybe a) -> [Maybe a]
forall a. Set a -> [a]
S.toList Set (Maybe a)
x

-- | Given a binary relation, compute its reflexive closure.
reflexiveClosure :: Ord a => BinaryRelation a -> BinaryRelation a
reflexiveClosure :: BinaryRelation a -> BinaryRelation a
reflexiveClosure r :: BinaryRelation a
r = ((a, a) -> BinaryRelation a -> BinaryRelation a)
-> BinaryRelation a -> BinaryRelation a -> BinaryRelation a
forall a b. (a -> b -> b) -> b -> Set a -> b
S.fold (a, a) -> BinaryRelation a -> BinaryRelation a
forall b. Ord b => (b, b) -> Set (b, b) -> Set (b, b)
add_refl BinaryRelation a
r BinaryRelation a
r
    where add_refl :: (b, b) -> Set (b, b) -> Set (b, b)
add_refl (x :: b
x, y :: b
y) r' :: Set (b, b)
r' = (b
x, b
x) (b, b) -> Set (b, b) -> Set (b, b)
forall a. Ord a => a -> Set a -> Set a
`S.insert` ((b
y, b
y) (b, b) -> Set (b, b) -> Set (b, b)
forall a. Ord a => a -> Set a -> Set a
`S.insert` Set (b, b)
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 :: [(a, a)] -> [Obligation a]
unmetObs r :: [(a, a)]
r = [Obligation a]
unmets
    where l :: [(Obligation a, Set a)]
l = Set (Obligation a, Set a) -> [(Obligation a, Set a)]
forall a. Set a -> [a]
S.toList (Set (Obligation a, Set a) -> [(Obligation a, Set a)])
-> Set (Obligation a, Set a) -> [(Obligation a, Set a)]
forall a b. (a -> b) -> a -> b
$ BinaryRelation a -> Set (Obligation a, Set a)
forall a. Ord a => BinaryRelation a -> Set (Obligation a, Set a)
localTops (BinaryRelation a -> Set (Obligation a, Set a))
-> BinaryRelation a -> Set (Obligation a, Set a)
forall a b. (a -> b) -> a -> b
$ BinaryRelation a -> BinaryRelation a
forall a. Ord a => BinaryRelation a -> BinaryRelation a
reflexiveClosure (BinaryRelation a -> BinaryRelation a)
-> BinaryRelation a -> BinaryRelation a
forall a b. (a -> b) -> a -> b
$ [(a, a)] -> BinaryRelation a
forall a. Ord a => [a] -> Set a
S.fromList [(a, a)]
r
          unmets :: [Obligation a]
unmets = ((Obligation a, Set a) -> Obligation a)
-> [(Obligation a, Set a)] -> [Obligation a]
forall a b. (a -> b) -> [a] -> [b]
map (Obligation a, Set a) -> Obligation a
forall a b. (a, b) -> a
fst ([(Obligation a, Set a)] -> [Obligation a])
-> [(Obligation a, Set a)] -> [Obligation a]
forall a b. (a -> b) -> a -> b
$ ((Obligation a, Set a) -> Bool)
-> [(Obligation a, Set a)] -> [(Obligation a, Set a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Set a -> Bool
forall a. Set a -> Bool
S.null (Set a -> Bool)
-> ((Obligation a, Set a) -> Set a)
-> (Obligation a, Set a)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Obligation a, Set a) -> Set a
forall a b. (a, b) -> b
snd) [(Obligation a, Set a)]
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 SORT -> Diagnosis
lteError (Obligation x :: SORT
x y :: SORT
y z :: SORT
z) = DiagKind -> String -> () -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error String
msg ()
    where msg :: String
msg = "local top element obligation ("
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ " < " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
z
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") 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 :: Rel SORT -> [Diagnosis]
checkLocalTops sr :: Rel SORT
sr =
    let obs :: [Obligation SORT]
obs = [(SORT, SORT)] -> [Obligation SORT]
forall a. Ord a => [(a, a)] -> [Obligation a]
unmetObs (Rel SORT -> [(SORT, SORT)]
forall a. Rel a -> [(a, a)]
Rel.toList (Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transClosure Rel SORT
sr))
    in (Obligation SORT -> Diagnosis) -> [Obligation SORT] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map Obligation SORT -> Diagnosis
lteError [Obligation SORT]
obs