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
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]
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
addSuperId :: Id -> Kind -> Id -> State Env ()
addSuperId i kind j = do
tm <- gets typeMap
cm <- gets classMap
unless (i == j)
$ case Map.lookup i tm of
Nothing -> return ()
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
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