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