content: {- |
  Module      :  ./HasCASL/ClassAna.hs
  Description :  analyse kinds using a class map
  Copyright   :  (c) Christian Maeder and Uni Bremen 2003-2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  experimental
  Portability :  portable
  
  analyse kinds using a class map
  -}
  
  module HasCASL.ClassAna where
  
  import HasCASL.As
  import HasCASL.AsUtils
  import HasCASL.PrintAs ()
  import Common.Id
  import HasCASL.Le
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  import Common.Lib.State
  import Common.Result
  import Common.DocUtils
  import Common.Utils
  import qualified Control.Monad.Fail as Fail
  
  -- * analyse kinds
  
  -- | check the kind and compute the raw kind
  anaKindM :: Kind -> ClassMap -> Result RawKind
  anaKindM k cm = case k of
      ClassKind ci -> if k == universe then return rStar
         else case Map.lookup ci cm of
              Just (ClassInfo rk _) -> return rk
              Nothing -> Result [mkDiag Error "not a class" ci] $ Just rStar
      FunKind v k1 k2 ps -> do
          rk1 <- anaKindM k1 cm
          rk2 <- anaKindM k2 cm
          return $ FunKind v rk1 rk2 ps
  
  -- | get minimal function kinds of (class) kind
  getFunKinds :: Fail.MonadFail m => ClassMap -> Kind -> m (Set.Set Kind)
  getFunKinds cm k = case k of
      FunKind {} -> return $ Set.singleton k
      ClassKind c -> case Map.lookup c cm of
           Just info -> do
               ks <- mapM (getFunKinds cm) $ Set.toList $ classKinds info
               return $ keepMinKinds cm ks
           _ -> Fail.fail $ "not a function kind '" ++ showId c "'"
  
  -- | compute arity from a raw kind
  kindArity :: RawKind -> Int
  kindArity k = case k of
      ClassKind _ -> 0
      FunKind _ _ rk _ -> 1 + kindArity rk
  
  -- | check if a class occurs in one of its super kinds
  cyclicClassId :: ClassMap -> Id -> Kind -> Bool
  cyclicClassId cm ci k = case k of
      FunKind _ k1 k2 _ -> cyclicClassId cm ci k1 || cyclicClassId cm ci k2
      ClassKind cj -> cj /= universeId &&
        (cj == ci || not (Set.null $ Set.filter (cyclicClassId cm ci)
            $ classKinds $ Map.findWithDefault (error "cyclicClassId") cj cm))
  
  -- * subkinding
  
  -- | keep only minimal elements according to 'lesserKind'
  keepMinKinds :: ClassMap -> [Set.Set Kind] -> Set.Set Kind
  keepMinKinds cm = Set.fromDistinctAscList
      . keepMins (lesserKind cm) . Set.toList . Set.unions
  
  -- | no kind of the set is lesser than the new kind
  newKind :: ClassMap -> Kind -> Set.Set Kind -> Bool
  newKind cm k = Set.null . Set.filter (flip (lesserKind cm) k)
  
  -- | add a new kind to a set
  addNewKind :: ClassMap -> Kind -> Set.Set Kind -> Set.Set Kind
  addNewKind cm k = Set.insert k . Set.filter (not . lesserKind cm k)
  
  lesserVariance :: Variance -> Variance -> Bool
  lesserVariance v1 v2 = case v1 of
    InVar -> True
    _ -> case v2 of
           NonVar -> True
           _ -> v1 == v2
  
  -- | revert variance
  revVariance :: Variance -> Variance
  revVariance v = case v of
      InVar -> NonVar
      CoVar -> ContraVar
      ContraVar -> CoVar
      NonVar -> InVar
  
  -- | compute the minimal variance
  minVariance :: Variance -> Variance -> Variance
  minVariance v1 v2 = case v1 of
    NonVar -> v2
    _ -> case v2 of
           NonVar -> v1
           _ -> if v1 == v2 then v1 else InVar
  
  -- | check subkinding (kinds with variances are greater)
  lesserKind :: ClassMap -> Kind -> Kind -> Bool
  lesserKind cm k1 k2 = case k1 of
      ClassKind c1 -> (case k2 of
          ClassKind c2 -> c1 == c2 || (k1 /= universe && k2 == universe)
          _ -> False) ||
            case Map.lookup c1 cm of
            Just info -> not $ newKind cm k2 $ classKinds info
            _ -> False
      FunKind v1 a1 r1 _ -> case k2 of
          FunKind v2 a2 r2 _ -> lesserVariance v1 v2
              && lesserKind cm r1 r2 && lesserKind cm a2 a1
          _ -> False
  
  -- | compare raw kinds
  lesserRawKind :: RawKind -> RawKind -> Bool
  lesserRawKind k1 k2 = case k1 of
      ClassKind _ -> case k2 of
          ClassKind _ -> True
          _ -> False
      FunKind v1 a1 r1 _ -> case k2 of
          FunKind v2 a2 r2 _ -> lesserVariance v1 v2
              && lesserRawKind r1 r2 && lesserRawKind a2 a1
          _ -> False
  
  minRawKind :: Fail.MonadFail m => String -> RawKind -> RawKind -> m RawKind
  minRawKind str k1 k2 = let err = Fail.fail $ diffKindString str k1 k2 in case k1 of
      ClassKind _ -> case k2 of
          ClassKind _ -> return $ ClassKind ()
          _ -> err
      FunKind v1 a1 r1 ps -> case k2 of
          FunKind v2 a2 r2 qs -> do
              a3 <- minRawKind str a2 a1
              r3 <- minRawKind str r1 r2
              return $ FunKind (minVariance v1 v2) a3 r3 $ appRange ps qs
          _ -> err
  
  rawToKind :: RawKind -> Kind
  rawToKind = mapKind (const universeId)
  
  -- * diagnostic messages
  
  -- | create message for different kinds
  diffKindString :: String -> RawKind -> RawKind -> String
  diffKindString a k1 k2 = "incompatible kind of: " ++ a ++
      expected (rawToKind k1) (rawToKind k2)
  
  -- | create diagnostic for different kinds
  diffKindDiag :: (GetRange a, Pretty a) =>
                  a -> RawKind -> RawKind -> [Diagnosis]
  diffKindDiag a k1 k2 =
     [Diag Error (diffKindString (showDoc a "") k1 k2) $ getRange a]
  
  -- | check if raw kinds are compatible
  checkKinds :: (GetRange a, Pretty a) =>
                a -> RawKind -> RawKind -> [Diagnosis]
  checkKinds p k1 k2 =
      maybe (diffKindDiag p k1 k2) (const []) $ minRawKind "" k1 k2
  
  -- | analyse class decls
  anaClassDecls :: ClassDecl -> State Env ClassDecl
  anaClassDecls (ClassDecl cls k ps) =
      do cm <- gets classMap
         let Result ds (Just rk) = anaKindM k cm
         addDiags ds
         let ak = if null ds then k else universe
         mapM_ (addClassDecl rk ak) cls
         return $ ClassDecl cls ak ps
  
  -- | store a class
  addClassDecl :: RawKind -> Kind -> Id -> State Env ()
  -- check with merge
  addClassDecl rk kind ci =
      if ci == universeId then
         addDiags [mkDiag Warning "void universe class declaration" ci]
      else do
         e <- get
         let cm = classMap e
             tm = typeMap e
             tvs = localTypeVars e
         case Map.lookup ci tm of
           Just _ -> addDiags [mkDiag Error "class name already a type" ci]
           Nothing -> case Map.lookup ci tvs of
               Just _ -> addDiags
                   [mkDiag Error "class name already a type variable" ci]
               Nothing -> case Map.lookup ci cm of
                   Nothing -> do
                     addSymbol $ idToClassSymbol ci rk
                     putClassMap $ Map.insert ci
                       (ClassInfo rk $ Set.singleton kind) cm
                   Just (ClassInfo ork superClasses) ->
                     let Result ds mk = minRawKind (showDoc ci "") rk ork
                     in case mk of
                     Nothing -> addDiags ds
                     Just nk ->
                       if cyclicClassId cm ci kind then
                          addDiags [mkDiag Error "cyclic class" ci]
                       else do
                         addSymbol $ idToClassSymbol ci nk
                         if newKind cm kind superClasses then do
                           addDiags [mkDiag Warning "refined class" ci]
                           putClassMap $ Map.insert ci
                             (ClassInfo nk $ addNewKind cm kind superClasses) cm
                          else addDiags [mkDiag Warning "unchanged class" ci]
  