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