content: {- |
  Module      :  ./HasCASL/SubtypeDecl.hs
  Description :  analysis of subtype declarations
  Copyright   :  (c) Christian Maeder and Uni Bremen 2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  analyse subtype decls
  -}
  
  module HasCASL.SubtypeDecl
      ( addSuperType
      , addAliasType
      ) where
  
  import Common.Id
  import Common.Lib.State
  import Common.Result
  
  import HasCASL.As
  import HasCASL.FoldType
  import HasCASL.AsUtils
  import HasCASL.Le
  import HasCASL.TypeAna
  import HasCASL.ClassAna
  import HasCASL.Unify
  import HasCASL.VarDecl
  
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  
  import Control.Monad
  
  etaReduceAux :: ([TypeArg], [TypeArg], [Type])
               -> ([TypeArg], [TypeArg], [Type])
  etaReduceAux p = case p of
      (ks, nA : rAs , tA : rArgs) | typeArgToType nA == tA ->
                etaReduceAux (nA : ks, rAs, rArgs)
      _ -> p
  
  etaReduce :: Kind -> [TypeArg] -> Type -> Maybe (Kind, [TypeArg], Type)
  etaReduce k nAs t =
      let (topTy, tArgs) = getTypeAppl t
          (ks, newAs, ts) = etaReduceAux ([], reverse nAs, reverse tArgs)
      in case ks of
           _ : _ -> Just (typeArgsListToKind ks k,
                          reverse newAs, mkTypeAppl topTy $ reverse ts)
           [] -> Nothing
  
  -- | add a supertype to a given type id
  addSuperType :: Type -> Kind -> (Id, [TypeArg]) -> State Env ()
  addSuperType t ak p@(i, nAs) = case t of
      TypeName j _ v -> if v /= 0 then
           addDiags [mkDiag Error "illegal type variable as supertype" j]
           else addSuperId i ak j
      _ -> case etaReduce ak nAs t of
          Just (nk, rAs, rT) -> addSuperType rT nk (i, rAs)
          Nothing -> case t of
            TypeAppl (TypeName l _ _) tl | l == lazyTypeId ->
                addSuperType tl ak p
            TypeAppl t1 t2 -> case redStep t of
             Just r -> addSuperType r ak p
             Nothing -> do
              j <- newTypeIdentifier i
              let rk = rawKindOfType t1
                  k = rawToKind rk
                  vs = freeTVarIds t1
                  newArgs = filter ( \ a -> getTypeVar a `elem` vs) nAs
                  jTy = TypeName j (typeArgsListToRawKind newArgs rk) 0
                  aTy = mkTypeAppl jTy $ map typeArgToType newArgs
              if null vs then addTypeId True NoTypeDefn k j else return True
              addSuperType t1 k (j, newArgs)
              tm <- gets typeMap
              addAliasType False i
                  (TypeScheme nAs (expandAlias tm $ TypeAppl aTy t2) nullRange)
                  $ typeArgsListToKind nAs ak
              return ()
            KindedType ty _ _ -> addSuperType ty ak p
            ExpandedType t1 t2 -> do
              addSuperType t1 ak p
              addSuperType t2 ak p
            _ -> addDiags [mkDiag Error "unexpected type as supertype" t]
  
  -- | generalize a type scheme for an alias type
  generalizeT :: TypeScheme -> State Env TypeScheme
  generalizeT sc@(TypeScheme args ty p) = do
     addDiags $ generalizable True sc
     return $ TypeScheme (genTypeArgs args) (generalize args ty) p
  
  newTypeIdentifier :: Id -> State Env Id
  newTypeIdentifier i = do
     n <- toEnvState inc
     return $ Id [genToken $ 't' : show n] [i] $ posOfId i
  
  -- | add second identifier as super type of known first identifier
  addSuperId :: Id -> Kind -> Id -> State Env ()
  addSuperId i kind j = do
      tm <- gets typeMap
      cm <- gets classMap
      unless (i == j) -- silently ignore
        $ case Map.lookup i tm of
            Nothing -> return () -- previous error
            Just (TypeInfo ok ks sups defn)
             | Set.member j sups -> addDiags [mkDiag Hint "repeated supertype" j]
             | Set.member i $ superIds tm j -> do
                     addDiags [mkDiag Warning
                              ("made '" ++ showId i "' an alias of") j]
                     addAliasType False i (TypeScheme [] (TypeName j ok 0)
                                                      $ posOfId j) kind
                     return ()
             | otherwise -> let Result _ (Just rk) = anaKindM kind cm in
                  maybe (addDiags $ diffKindDiag i ok rk)
                  (const $ putTypeMap $ Map.insert i
                            (TypeInfo ok ks (Set.insert j sups) defn) tm)
                  $ minRawKind "" ok rk
  
  -- | add an alias type definition
  addAliasType :: Bool -> Id -> TypeScheme -> Kind -> State Env Bool
  addAliasType b i sc fullKind = do
      newSc <- generalizeT sc
      addAliasTypeAux b i newSc fullKind
  
  addAliasTypeAux :: Bool -> Id -> TypeScheme -> Kind -> State Env Bool
  addAliasTypeAux b i (TypeScheme args ty ps) fullKind =
    if elem i $ map (fst . snd) $ leaves (== 0) ty then do
      addDiags [mkDiag Error "cyclic alias type" i]
      return False
    else addTypeId b (AliasTypeDefn $ foldr ( \ t y -> TypeAbs t y ps) ty args)
          fullKind i
  