{- |
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 :: Kind -> ClassMap -> Result RawKind
anaKindM k :: Kind
k cm :: ClassMap
cm = case Kind
k of
    ClassKind ci :: Id
ci -> if Kind
k Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
universe then RawKind -> Result RawKind
forall (m :: * -> *) a. Monad m => a -> m a
return RawKind
rStar
       else case Id -> ClassMap -> Maybe ClassInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
ci ClassMap
cm of
            Just (ClassInfo rk :: RawKind
rk _) -> RawKind -> Result RawKind
forall (m :: * -> *) a. Monad m => a -> m a
return RawKind
rk
            Nothing -> [Diagnosis] -> Maybe RawKind -> Result RawKind
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "not a class" Id
ci] (Maybe RawKind -> Result RawKind)
-> Maybe RawKind -> Result RawKind
forall a b. (a -> b) -> a -> b
$ RawKind -> Maybe RawKind
forall a. a -> Maybe a
Just RawKind
rStar
    FunKind v :: Variance
v k1 :: Kind
k1 k2 :: Kind
k2 ps :: Range
ps -> do
        RawKind
rk1 <- Kind -> ClassMap -> Result RawKind
anaKindM Kind
k1 ClassMap
cm
        RawKind
rk2 <- Kind -> ClassMap -> Result RawKind
anaKindM Kind
k2 ClassMap
cm
        RawKind -> Result RawKind
forall (m :: * -> *) a. Monad m => a -> m a
return (RawKind -> Result RawKind) -> RawKind -> Result RawKind
forall a b. (a -> b) -> a -> b
$ Variance -> RawKind -> RawKind -> Range -> RawKind
forall a. Variance -> AnyKind a -> AnyKind a -> Range -> AnyKind a
FunKind Variance
v RawKind
rk1 RawKind
rk2 Range
ps

-- | get minimal function kinds of (class) kind
getFunKinds :: Fail.MonadFail m => ClassMap -> Kind -> m (Set.Set Kind)
getFunKinds :: ClassMap -> Kind -> m (Set Kind)
getFunKinds cm :: ClassMap
cm k :: Kind
k = case Kind
k of
    FunKind {} -> Set Kind -> m (Set Kind)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Kind -> m (Set Kind)) -> Set Kind -> m (Set Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Set Kind
forall a. a -> Set a
Set.singleton Kind
k
    ClassKind c :: Id
c -> case Id -> ClassMap -> Maybe ClassInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
c ClassMap
cm of
         Just info :: ClassInfo
info -> do
             [Set Kind]
ks <- (Kind -> m (Set Kind)) -> [Kind] -> m [Set Kind]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ClassMap -> Kind -> m (Set Kind)
forall (m :: * -> *).
MonadFail m =>
ClassMap -> Kind -> m (Set Kind)
getFunKinds ClassMap
cm) ([Kind] -> m [Set Kind]) -> [Kind] -> m [Set Kind]
forall a b. (a -> b) -> a -> b
$ Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList (Set Kind -> [Kind]) -> Set Kind -> [Kind]
forall a b. (a -> b) -> a -> b
$ ClassInfo -> Set Kind
classKinds ClassInfo
info
             Set Kind -> m (Set Kind)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Kind -> m (Set Kind)) -> Set Kind -> m (Set Kind)
forall a b. (a -> b) -> a -> b
$ ClassMap -> [Set Kind] -> Set Kind
keepMinKinds ClassMap
cm [Set Kind]
ks
         _ -> String -> m (Set Kind)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m (Set Kind)) -> String -> m (Set Kind)
forall a b. (a -> b) -> a -> b
$ "not a function kind '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String -> String
showId Id
c "'"

-- | compute arity from a raw kind
kindArity :: RawKind -> Int
kindArity :: RawKind -> Int
kindArity k :: RawKind
k = case RawKind
k of
    ClassKind _ -> 0
    FunKind _ _ rk :: RawKind
rk _ -> 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ RawKind -> Int
kindArity RawKind
rk

-- | check if a class occurs in one of its super kinds
cyclicClassId :: ClassMap -> Id -> Kind -> Bool
cyclicClassId :: ClassMap -> Id -> Kind -> Bool
cyclicClassId cm :: ClassMap
cm ci :: Id
ci k :: Kind
k = case Kind
k of
    FunKind _ k1 :: Kind
k1 k2 :: Kind
k2 _ -> ClassMap -> Id -> Kind -> Bool
cyclicClassId ClassMap
cm Id
ci Kind
k1 Bool -> Bool -> Bool
|| ClassMap -> Id -> Kind -> Bool
cyclicClassId ClassMap
cm Id
ci Kind
k2
    ClassKind cj :: Id
cj -> Id
cj Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
/= Id
universeId Bool -> Bool -> Bool
&&
      (Id
cj Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
ci Bool -> Bool -> Bool
|| Bool -> Bool
not (Set Kind -> Bool
forall a. Set a -> Bool
Set.null (Set Kind -> Bool) -> Set Kind -> Bool
forall a b. (a -> b) -> a -> b
$ (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (ClassMap -> Id -> Kind -> Bool
cyclicClassId ClassMap
cm Id
ci)
          (Set Kind -> Set Kind) -> Set Kind -> Set Kind
forall a b. (a -> b) -> a -> b
$ ClassInfo -> Set Kind
classKinds (ClassInfo -> Set Kind) -> ClassInfo -> Set Kind
forall a b. (a -> b) -> a -> b
$ ClassInfo -> Id -> ClassMap -> ClassInfo
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> ClassInfo
forall a. HasCallStack => String -> a
error "cyclicClassId") Id
cj ClassMap
cm))

-- * subkinding

-- | keep only minimal elements according to 'lesserKind'
keepMinKinds :: ClassMap -> [Set.Set Kind] -> Set.Set Kind
keepMinKinds :: ClassMap -> [Set Kind] -> Set Kind
keepMinKinds cm :: ClassMap
cm = [Kind] -> Set Kind
forall a. [a] -> Set a
Set.fromDistinctAscList
    ([Kind] -> Set Kind)
-> ([Set Kind] -> [Kind]) -> [Set Kind] -> Set Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Kind -> Kind -> Bool) -> [Kind] -> [Kind]
forall a. (a -> a -> Bool) -> [a] -> [a]
keepMins (ClassMap -> Kind -> Kind -> Bool
lesserKind ClassMap
cm) ([Kind] -> [Kind])
-> ([Set Kind] -> [Kind]) -> [Set Kind] -> [Kind]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList (Set Kind -> [Kind])
-> ([Set Kind] -> Set Kind) -> [Set Kind] -> [Kind]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Set Kind] -> Set Kind
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions

-- | no kind of the set is lesser than the new kind
newKind :: ClassMap -> Kind -> Set.Set Kind -> Bool
newKind :: ClassMap -> Kind -> Set Kind -> Bool
newKind cm :: ClassMap
cm k :: Kind
k = Set Kind -> Bool
forall a. Set a -> Bool
Set.null (Set Kind -> Bool) -> (Set Kind -> Set Kind) -> Set Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((Kind -> Kind -> Bool) -> Kind -> Kind -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ClassMap -> Kind -> Kind -> Bool
lesserKind ClassMap
cm) Kind
k)

-- | add a new kind to a set
addNewKind :: ClassMap -> Kind -> Set.Set Kind -> Set.Set Kind
addNewKind :: ClassMap -> Kind -> Set Kind -> Set Kind
addNewKind cm :: ClassMap
cm k :: Kind
k = Kind -> Set Kind -> Set Kind
forall a. Ord a => a -> Set a -> Set a
Set.insert Kind
k (Set Kind -> Set Kind)
-> (Set Kind -> Set Kind) -> Set Kind -> Set Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (Kind -> Bool) -> Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClassMap -> Kind -> Kind -> Bool
lesserKind ClassMap
cm Kind
k)

lesserVariance :: Variance -> Variance -> Bool
lesserVariance :: Variance -> Variance -> Bool
lesserVariance v1 :: Variance
v1 v2 :: Variance
v2 = case Variance
v1 of
  InVar -> Bool
True
  _ -> case Variance
v2 of
         NonVar -> Bool
True
         _ -> Variance
v1 Variance -> Variance -> Bool
forall a. Eq a => a -> a -> Bool
== Variance
v2

-- | revert variance
revVariance :: Variance -> Variance
revVariance :: Variance -> Variance
revVariance v :: Variance
v = case Variance
v of
    InVar -> Variance
NonVar
    CoVar -> Variance
ContraVar
    ContraVar -> Variance
CoVar
    NonVar -> Variance
InVar

-- | compute the minimal variance
minVariance :: Variance -> Variance -> Variance
minVariance :: Variance -> Variance -> Variance
minVariance v1 :: Variance
v1 v2 :: Variance
v2 = case Variance
v1 of
  NonVar -> Variance
v2
  _ -> case Variance
v2 of
         NonVar -> Variance
v1
         _ -> if Variance
v1 Variance -> Variance -> Bool
forall a. Eq a => a -> a -> Bool
== Variance
v2 then Variance
v1 else Variance
InVar

-- | check subkinding (kinds with variances are greater)
lesserKind :: ClassMap -> Kind -> Kind -> Bool
lesserKind :: ClassMap -> Kind -> Kind -> Bool
lesserKind cm :: ClassMap
cm k1 :: Kind
k1 k2 :: Kind
k2 = case Kind
k1 of
    ClassKind c1 :: Id
c1 -> (case Kind
k2 of
        ClassKind c2 :: Id
c2 -> Id
c1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
c2 Bool -> Bool -> Bool
|| (Kind
k1 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
universe Bool -> Bool -> Bool
&& Kind
k2 Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
universe)
        _ -> Bool
False) Bool -> Bool -> Bool
||
          case Id -> ClassMap -> Maybe ClassInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
c1 ClassMap
cm of
          Just info :: ClassInfo
info -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ClassMap -> Kind -> Set Kind -> Bool
newKind ClassMap
cm Kind
k2 (Set Kind -> Bool) -> Set Kind -> Bool
forall a b. (a -> b) -> a -> b
$ ClassInfo -> Set Kind
classKinds ClassInfo
info
          _ -> Bool
False
    FunKind v1 :: Variance
v1 a1 :: Kind
a1 r1 :: Kind
r1 _ -> case Kind
k2 of
        FunKind v2 :: Variance
v2 a2 :: Kind
a2 r2 :: Kind
r2 _ -> Variance -> Variance -> Bool
lesserVariance Variance
v1 Variance
v2
            Bool -> Bool -> Bool
&& ClassMap -> Kind -> Kind -> Bool
lesserKind ClassMap
cm Kind
r1 Kind
r2 Bool -> Bool -> Bool
&& ClassMap -> Kind -> Kind -> Bool
lesserKind ClassMap
cm Kind
a2 Kind
a1
        _ -> Bool
False

-- | compare raw kinds
lesserRawKind :: RawKind -> RawKind -> Bool
lesserRawKind :: RawKind -> RawKind -> Bool
lesserRawKind k1 :: RawKind
k1 k2 :: RawKind
k2 = case RawKind
k1 of
    ClassKind _ -> case RawKind
k2 of
        ClassKind _ -> Bool
True
        _ -> Bool
False
    FunKind v1 :: Variance
v1 a1 :: RawKind
a1 r1 :: RawKind
r1 _ -> case RawKind
k2 of
        FunKind v2 :: Variance
v2 a2 :: RawKind
a2 r2 :: RawKind
r2 _ -> Variance -> Variance -> Bool
lesserVariance Variance
v1 Variance
v2
            Bool -> Bool -> Bool
&& RawKind -> RawKind -> Bool
lesserRawKind RawKind
r1 RawKind
r2 Bool -> Bool -> Bool
&& RawKind -> RawKind -> Bool
lesserRawKind RawKind
a2 RawKind
a1
        _ -> Bool
False

minRawKind :: Fail.MonadFail m => String -> RawKind -> RawKind -> m RawKind
minRawKind :: String -> RawKind -> RawKind -> m RawKind
minRawKind str :: String
str k1 :: RawKind
k1 k2 :: RawKind
k2 = let err :: m a
err = String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String -> RawKind -> RawKind -> String
diffKindString String
str RawKind
k1 RawKind
k2 in case RawKind
k1 of
    ClassKind _ -> case RawKind
k2 of
        ClassKind _ -> RawKind -> m RawKind
forall (m :: * -> *) a. Monad m => a -> m a
return (RawKind -> m RawKind) -> RawKind -> m RawKind
forall a b. (a -> b) -> a -> b
$ () -> RawKind
forall a. a -> AnyKind a
ClassKind ()
        _ -> m RawKind
forall a. m a
err
    FunKind v1 :: Variance
v1 a1 :: RawKind
a1 r1 :: RawKind
r1 ps :: Range
ps -> case RawKind
k2 of
        FunKind v2 :: Variance
v2 a2 :: RawKind
a2 r2 :: RawKind
r2 qs :: Range
qs -> do
            RawKind
a3 <- String -> RawKind -> RawKind -> m RawKind
forall (m :: * -> *).
MonadFail m =>
String -> RawKind -> RawKind -> m RawKind
minRawKind String
str RawKind
a2 RawKind
a1
            RawKind
r3 <- String -> RawKind -> RawKind -> m RawKind
forall (m :: * -> *).
MonadFail m =>
String -> RawKind -> RawKind -> m RawKind
minRawKind String
str RawKind
r1 RawKind
r2
            RawKind -> m RawKind
forall (m :: * -> *) a. Monad m => a -> m a
return (RawKind -> m RawKind) -> RawKind -> m RawKind
forall a b. (a -> b) -> a -> b
$ Variance -> RawKind -> RawKind -> Range -> RawKind
forall a. Variance -> AnyKind a -> AnyKind a -> Range -> AnyKind a
FunKind (Variance -> Variance -> Variance
minVariance Variance
v1 Variance
v2) RawKind
a3 RawKind
r3 (Range -> RawKind) -> Range -> RawKind
forall a b. (a -> b) -> a -> b
$ Range -> Range -> Range
appRange Range
ps Range
qs
        _ -> m RawKind
forall a. m a
err

rawToKind :: RawKind -> Kind
rawToKind :: RawKind -> Kind
rawToKind = (() -> Id) -> RawKind -> Kind
forall a b. (a -> b) -> AnyKind a -> AnyKind b
mapKind (Id -> () -> Id
forall a b. a -> b -> a
const Id
universeId)

-- * diagnostic messages

-- | create message for different kinds
diffKindString :: String -> RawKind -> RawKind -> String
diffKindString :: String -> RawKind -> RawKind -> String
diffKindString a :: String
a k1 :: RawKind
k1 k2 :: RawKind
k2 = "incompatible kind of: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++
    Kind -> Kind -> String
forall a. Pretty a => a -> a -> String
expected (RawKind -> Kind
rawToKind RawKind
k1) (RawKind -> Kind
rawToKind RawKind
k2)

-- | create diagnostic for different kinds
diffKindDiag :: (GetRange a, Pretty a) =>
                a -> RawKind -> RawKind -> [Diagnosis]
diffKindDiag :: a -> RawKind -> RawKind -> [Diagnosis]
diffKindDiag a :: a
a k1 :: RawKind
k1 k2 :: RawKind
k2 =
   [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error (String -> RawKind -> RawKind -> String
diffKindString (a -> String -> String
forall a. Pretty a => a -> String -> String
showDoc a
a "") RawKind
k1 RawKind
k2) (Range -> Diagnosis) -> Range -> Diagnosis
forall a b. (a -> b) -> a -> b
$ a -> Range
forall a. GetRange a => a -> Range
getRange a
a]

-- | check if raw kinds are compatible
checkKinds :: (GetRange a, Pretty a) =>
              a -> RawKind -> RawKind -> [Diagnosis]
checkKinds :: a -> RawKind -> RawKind -> [Diagnosis]
checkKinds p :: a
p k1 :: RawKind
k1 k2 :: RawKind
k2 =
    [Diagnosis]
-> (RawKind -> [Diagnosis]) -> Maybe RawKind -> [Diagnosis]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (a -> RawKind -> RawKind -> [Diagnosis]
forall a.
(GetRange a, Pretty a) =>
a -> RawKind -> RawKind -> [Diagnosis]
diffKindDiag a
p RawKind
k1 RawKind
k2) ([Diagnosis] -> RawKind -> [Diagnosis]
forall a b. a -> b -> a
const []) (Maybe RawKind -> [Diagnosis]) -> Maybe RawKind -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ String -> RawKind -> RawKind -> Maybe RawKind
forall (m :: * -> *).
MonadFail m =>
String -> RawKind -> RawKind -> m RawKind
minRawKind "" RawKind
k1 RawKind
k2

-- | analyse class decls
anaClassDecls :: ClassDecl -> State Env ClassDecl
anaClassDecls :: ClassDecl -> State Env ClassDecl
anaClassDecls (ClassDecl cls :: [Id]
cls k :: Kind
k ps :: Range
ps) =
    do ClassMap
cm <- (Env -> ClassMap) -> State Env ClassMap
forall s a. (s -> a) -> State s a
gets Env -> ClassMap
classMap
       let Result ds :: [Diagnosis]
ds (Just rk :: RawKind
rk) = Kind -> ClassMap -> Result RawKind
anaKindM Kind
k ClassMap
cm
       [Diagnosis] -> State Env ()
addDiags [Diagnosis]
ds
       let ak :: Kind
ak = if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds then Kind
k else Kind
universe
       (Id -> State Env ()) -> [Id] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (RawKind -> Kind -> Id -> State Env ()
addClassDecl RawKind
rk Kind
ak) [Id]
cls
       ClassDecl -> State Env ClassDecl
forall (m :: * -> *) a. Monad m => a -> m a
return (ClassDecl -> State Env ClassDecl)
-> ClassDecl -> State Env ClassDecl
forall a b. (a -> b) -> a -> b
$ [Id] -> Kind -> Range -> ClassDecl
ClassDecl [Id]
cls Kind
ak Range
ps

-- | store a class
addClassDecl :: RawKind -> Kind -> Id -> State Env ()
-- check with merge
addClassDecl :: RawKind -> Kind -> Id -> State Env ()
addClassDecl rk :: RawKind
rk kind :: Kind
kind ci :: Id
ci =
    if Id
ci Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
universeId then
       [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "void universe class declaration" Id
ci]
    else do
       Env
e <- State Env Env
forall s. State s s
get
       let cm :: ClassMap
cm = Env -> ClassMap
classMap Env
e
           tm :: TypeMap
tm = Env -> TypeMap
typeMap Env
e
           tvs :: LocalTypeVars
tvs = Env -> LocalTypeVars
localTypeVars Env
e
       case Id -> TypeMap -> Maybe TypeInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
ci TypeMap
tm of
         Just _ -> [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "class name already a type" Id
ci]
         Nothing -> case Id -> LocalTypeVars -> Maybe TypeVarDefn
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
ci LocalTypeVars
tvs of
             Just _ -> [Diagnosis] -> State Env ()
addDiags
                 [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "class name already a type variable" Id
ci]
             Nothing -> case Id -> ClassMap -> Maybe ClassInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
ci ClassMap
cm of
                 Nothing -> do
                   Symbol -> State Env ()
addSymbol (Symbol -> State Env ()) -> Symbol -> State Env ()
forall a b. (a -> b) -> a -> b
$ Id -> RawKind -> Symbol
idToClassSymbol Id
ci RawKind
rk
                   ClassMap -> State Env ()
putClassMap (ClassMap -> State Env ()) -> ClassMap -> State Env ()
forall a b. (a -> b) -> a -> b
$ Id -> ClassInfo -> ClassMap -> ClassMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
ci
                     (RawKind -> Set Kind -> ClassInfo
ClassInfo RawKind
rk (Set Kind -> ClassInfo) -> Set Kind -> ClassInfo
forall a b. (a -> b) -> a -> b
$ Kind -> Set Kind
forall a. a -> Set a
Set.singleton Kind
kind) ClassMap
cm
                 Just (ClassInfo ork :: RawKind
ork superClasses :: Set Kind
superClasses) ->
                   let Result ds :: [Diagnosis]
ds mk :: Maybe RawKind
mk = String -> RawKind -> RawKind -> Result RawKind
forall (m :: * -> *).
MonadFail m =>
String -> RawKind -> RawKind -> m RawKind
minRawKind (Id -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Id
ci "") RawKind
rk RawKind
ork
                   in case Maybe RawKind
mk of
                   Nothing -> [Diagnosis] -> State Env ()
addDiags [Diagnosis]
ds
                   Just nk :: RawKind
nk ->
                     if ClassMap -> Id -> Kind -> Bool
cyclicClassId ClassMap
cm Id
ci Kind
kind then
                        [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "cyclic class" Id
ci]
                     else do
                       Symbol -> State Env ()
addSymbol (Symbol -> State Env ()) -> Symbol -> State Env ()
forall a b. (a -> b) -> a -> b
$ Id -> RawKind -> Symbol
idToClassSymbol Id
ci RawKind
nk
                       if ClassMap -> Kind -> Set Kind -> Bool
newKind ClassMap
cm Kind
kind Set Kind
superClasses then do
                         [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "refined class" Id
ci]
                         ClassMap -> State Env ()
putClassMap (ClassMap -> State Env ()) -> ClassMap -> State Env ()
forall a b. (a -> b) -> a -> b
$ Id -> ClassInfo -> ClassMap -> ClassMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
ci
                           (RawKind -> Set Kind -> ClassInfo
ClassInfo RawKind
nk (Set Kind -> ClassInfo) -> Set Kind -> ClassInfo
forall a b. (a -> b) -> a -> b
$ ClassMap -> Kind -> Set Kind -> Set Kind
addNewKind ClassMap
cm Kind
kind Set Kind
superClasses) ClassMap
cm
                        else [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "unchanged class" Id
ci]