{- | 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