hets/HasCASL/ClassAna.hs

	ClassAna.hs revision 97018cf5fa25b494adffd7e9b4e87320dae6bf47
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay{- |
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemayModule      :  $Header$
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemayCopyright   :  (c) Christian Maeder and Uni Bremen 2003
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemayLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemayMaintainer  :  maeder@tzi.de
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemayStability   :  experimental
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemayPortability :  portable
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay   auxiliary functions for raw kinds
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay-}
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemaymodule HasCASL.ClassAna where
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemayimport HasCASL.As
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemayimport HasCASL.AsUtils
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemayimport Common.Id
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemayimport HasCASL.Le
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemayimport Common.PrettyPrint
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemayimport qualified Common.Lib.Map as Map
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemayimport qualified Common.Lib.Set as Set
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemayimport Common.Result
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemayanaClassId :: ClassId -> ClassMap -> Result Kind
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemayanaClassId ci cMap =
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay       case Map.lookup ci cMap of
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay            Nothing -> mkError "undeclared class" ci
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay            Just (ClassInfo l) -> return $ ClassKind ci $ toIntersection l []
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemaytoIntersection :: [Kind] -> [Pos] -> Kind
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemaytoIntersection l ps = case Set.toList $ mkIntersection l of
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay                          [] -> Intersection [] ps
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay                          [h] -> h
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay                          is -> Intersection is ps
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemaymkIntersection :: [Kind] -> Set.Set Kind
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemaymkIntersection = Set.unions . map ( \ k -> case k of
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay                                 Intersection lk _ -> mkIntersection lk
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay                                 _ -> Set.singleton k)
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemayrawKind :: Kind -> Kind
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemayrawKind c =
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay    case c of
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay    MissingKind -> error "rawKind"
35a0c21a3150b1c01572f6075d6240eebd301415Jason Lemay    ClassKind _ rk -> rawKind rk
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay    Downset _ _ rk _ -> rawKind rk
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay    Intersection l _ -> if null l then c
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay                        else rawKind $ head l
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay    FunKind e k ps  -> FunKind (rawKind e) (rawKind k) ps
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay    ExtKind k v ps -> ExtKind (rawKind k) v ps
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemaycheckIntersection :: Kind -> [Kind] -> [Diagnosis]
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemaycheckIntersection _ [] = []
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason LemaycheckIntersection k (f:r) =
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay        case k == rawKind f of
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay        False ->
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay              Diag Error ("incompatible kind of: " ++ showPretty f ""
5f22ff8ce7baf0b39668468cc854eec3eb946003Jason Lemay                ++  "\n  for raw kind: " ++ showPretty k "")
              (posOf [f]) : checkIntersection k r
        True -> checkIntersection k r

diffKindDiag :: (PosItem a, PrettyPrint a) =>
                 a -> Kind -> Kind -> [Diagnosis]
diffKindDiag a k1 k2 =
           [ Diag Error
              ("incompatible kind of: " ++ showPretty a "" ++ expected k1 k2)
            $ posOf [a] ]

checkKinds :: (PosItem a, PrettyPrint a) =>
              a -> Kind -> Kind -> [Diagnosis]
checkKinds p k1 k2 =
    do let k3 = rawKind k1
           k4 = rawKind k2
       if k3 == k4 then []
          else diffKindDiag p k1 k2

cyclicClassId :: ClassId -> Kind -> Bool
cyclicClassId ci k =
    case k of
           FunKind k1 k2 _ -> cyclicClassId ci k1 || cyclicClassId ci k2
           ExtKind ek _ _ -> cyclicClassId ci ek
           ClassKind cj ck -> cj == ci || cyclicClassId ci ck
           Downset _ _ dk _ -> cyclicClassId ci dk
           Intersection l _ -> any (cyclicClassId ci) l
           _ -> False