{- |
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 :: ([TypeArg], [TypeArg], [Type]) -> ([TypeArg], [TypeArg], [Type])
etaReduceAux p :: ([TypeArg], [TypeArg], [Type])
p = case ([TypeArg], [TypeArg], [Type])
p of
    (ks :: [TypeArg]
ks, nA :: TypeArg
nA : rAs :: [TypeArg]
rAs , tA :: Type
tA : rArgs :: [Type]
rArgs) | TypeArg -> Type
typeArgToType TypeArg
nA Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
tA ->
              ([TypeArg], [TypeArg], [Type]) -> ([TypeArg], [TypeArg], [Type])
etaReduceAux (TypeArg
nA TypeArg -> [TypeArg] -> [TypeArg]
forall a. a -> [a] -> [a]
: [TypeArg]
ks, [TypeArg]
rAs, [Type]
rArgs)
    _ -> ([TypeArg], [TypeArg], [Type])
p

etaReduce :: Kind -> [TypeArg] -> Type -> Maybe (Kind, [TypeArg], Type)
etaReduce :: Kind -> [TypeArg] -> Type -> Maybe (Kind, [TypeArg], Type)
etaReduce k :: Kind
k nAs :: [TypeArg]
nAs t :: Type
t =
    let (topTy :: Type
topTy, tArgs :: [Type]
tArgs) = Type -> (Type, [Type])
getTypeAppl Type
t
        (ks :: [TypeArg]
ks, newAs :: [TypeArg]
newAs, ts :: [Type]
ts) = ([TypeArg], [TypeArg], [Type]) -> ([TypeArg], [TypeArg], [Type])
etaReduceAux ([], [TypeArg] -> [TypeArg]
forall a. [a] -> [a]
reverse [TypeArg]
nAs, [Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
tArgs)
    in case [TypeArg]
ks of
         _ : _ -> (Kind, [TypeArg], Type) -> Maybe (Kind, [TypeArg], Type)
forall a. a -> Maybe a
Just ([TypeArg] -> Kind -> Kind
typeArgsListToKind [TypeArg]
ks Kind
k,
                        [TypeArg] -> [TypeArg]
forall a. [a] -> [a]
reverse [TypeArg]
newAs, Type -> [Type] -> Type
mkTypeAppl Type
topTy ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ [Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
ts)
         [] -> Maybe (Kind, [TypeArg], Type)
forall a. Maybe a
Nothing

-- | add a supertype to a given type id
addSuperType :: Type -> Kind -> (Id, [TypeArg]) -> State Env ()
addSuperType :: Type -> Kind -> (Id, [TypeArg]) -> State Env ()
addSuperType t :: Type
t ak :: Kind
ak p :: (Id, [TypeArg])
p@(i :: Id
i, nAs :: [TypeArg]
nAs) = case Type
t of
    TypeName j :: Id
j _ v :: Int
v -> if Int
v Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= 0 then
         [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "illegal type variable as supertype" Id
j]
         else Id -> Kind -> Id -> State Env ()
addSuperId Id
i Kind
ak Id
j
    _ -> case Kind -> [TypeArg] -> Type -> Maybe (Kind, [TypeArg], Type)
etaReduce Kind
ak [TypeArg]
nAs Type
t of
        Just (nk :: Kind
nk, rAs :: [TypeArg]
rAs, rT :: Type
rT) -> Type -> Kind -> (Id, [TypeArg]) -> State Env ()
addSuperType Type
rT Kind
nk (Id
i, [TypeArg]
rAs)
        Nothing -> case Type
t of
          TypeAppl (TypeName l :: Id
l _ _) tl :: Type
tl | Id
l Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
              Type -> Kind -> (Id, [TypeArg]) -> State Env ()
addSuperType Type
tl Kind
ak (Id, [TypeArg])
p
          TypeAppl t1 :: Type
t1 t2 :: Type
t2 -> case Type -> Maybe Type
redStep Type
t of
           Just r :: Type
r -> Type -> Kind -> (Id, [TypeArg]) -> State Env ()
addSuperType Type
r Kind
ak (Id, [TypeArg])
p
           Nothing -> do
            Id
j <- Id -> State Env Id
newTypeIdentifier Id
i
            let rk :: RawKind
rk = Type -> RawKind
rawKindOfType Type
t1
                k :: Kind
k = RawKind -> Kind
rawToKind RawKind
rk
                vs :: [Id]
vs = Type -> [Id]
freeTVarIds Type
t1
                newArgs :: [TypeArg]
newArgs = (TypeArg -> Bool) -> [TypeArg] -> [TypeArg]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ a :: TypeArg
a -> TypeArg -> Id
getTypeVar TypeArg
a Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Id]
vs) [TypeArg]
nAs
                jTy :: Type
jTy = Id -> RawKind -> Int -> Type
TypeName Id
j ([TypeArg] -> RawKind -> RawKind
typeArgsListToRawKind [TypeArg]
newArgs RawKind
rk) 0
                aTy :: Type
aTy = Type -> [Type] -> Type
mkTypeAppl Type
jTy ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (TypeArg -> Type) -> [TypeArg] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> Type
typeArgToType [TypeArg]
newArgs
            if [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
vs then Bool -> TypeDefn -> Kind -> Id -> State Env Bool
addTypeId Bool
True TypeDefn
NoTypeDefn Kind
k Id
j else Bool -> State Env Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
            Type -> Kind -> (Id, [TypeArg]) -> State Env ()
addSuperType Type
t1 Kind
k (Id
j, [TypeArg]
newArgs)
            TypeMap
tm <- (Env -> TypeMap) -> State Env TypeMap
forall s a. (s -> a) -> State s a
gets Env -> TypeMap
typeMap
            Bool -> Id -> TypeScheme -> Kind -> State Env Bool
addAliasType Bool
False Id
i
                ([TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [TypeArg]
nAs (TypeMap -> Type -> Type
expandAlias TypeMap
tm (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
TypeAppl Type
aTy Type
t2) Range
nullRange)
                (Kind -> State Env Bool) -> Kind -> State Env Bool
forall a b. (a -> b) -> a -> b
$ [TypeArg] -> Kind -> Kind
typeArgsListToKind [TypeArg]
nAs Kind
ak
            () -> State Env ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          KindedType ty :: Type
ty _ _ -> Type -> Kind -> (Id, [TypeArg]) -> State Env ()
addSuperType Type
ty Kind
ak (Id, [TypeArg])
p
          ExpandedType t1 :: Type
t1 t2 :: Type
t2 -> do
            Type -> Kind -> (Id, [TypeArg]) -> State Env ()
addSuperType Type
t1 Kind
ak (Id, [TypeArg])
p
            Type -> Kind -> (Id, [TypeArg]) -> State Env ()
addSuperType Type
t2 Kind
ak (Id, [TypeArg])
p
          _ -> [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Type -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unexpected type as supertype" Type
t]

-- | generalize a type scheme for an alias type
generalizeT :: TypeScheme -> State Env TypeScheme
generalizeT :: TypeScheme -> State Env TypeScheme
generalizeT sc :: TypeScheme
sc@(TypeScheme args :: [TypeArg]
args ty :: Type
ty p :: Range
p) = do
   [Diagnosis] -> State Env ()
addDiags ([Diagnosis] -> State Env ()) -> [Diagnosis] -> State Env ()
forall a b. (a -> b) -> a -> b
$ Bool -> TypeScheme -> [Diagnosis]
generalizable Bool
True TypeScheme
sc
   TypeScheme -> State Env TypeScheme
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeScheme -> State Env TypeScheme)
-> TypeScheme -> State Env TypeScheme
forall a b. (a -> b) -> a -> b
$ [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme ([TypeArg] -> [TypeArg]
genTypeArgs [TypeArg]
args) ([TypeArg] -> Type -> Type
generalize [TypeArg]
args Type
ty) Range
p

newTypeIdentifier :: Id -> State Env Id
newTypeIdentifier :: Id -> State Env Id
newTypeIdentifier i :: Id
i = do
   Int
n <- State Int Int -> State Env Int
forall a. State Int a -> State Env a
toEnvState State Int Int
inc
   Id -> State Env Id
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> State Env Id) -> Id -> State Env Id
forall a b. (a -> b) -> a -> b
$ [Token] -> [Id] -> Range -> Id
Id [String -> Token
genToken (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ 't' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
n] [Id
i] (Range -> Id) -> Range -> Id
forall a b. (a -> b) -> a -> b
$ Id -> Range
posOfId Id
i

-- | add second identifier as super type of known first identifier
addSuperId :: Id -> Kind -> Id -> State Env ()
addSuperId :: Id -> Kind -> Id -> State Env ()
addSuperId i :: Id
i kind :: Kind
kind j :: Id
j = do
    TypeMap
tm <- (Env -> TypeMap) -> State Env TypeMap
forall s a. (s -> a) -> State s a
gets Env -> TypeMap
typeMap
    ClassMap
cm <- (Env -> ClassMap) -> State Env ClassMap
forall s a. (s -> a) -> State s a
gets Env -> ClassMap
classMap
    Bool -> State Env () -> State Env ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
j) -- silently ignore
      (State Env () -> State Env ()) -> State Env () -> State Env ()
forall a b. (a -> b) -> a -> b
$ case Id -> TypeMap -> Maybe TypeInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i TypeMap
tm of
          Nothing -> () -> State Env ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- previous error
          Just (TypeInfo ok :: RawKind
ok ks :: Set Kind
ks sups :: Set Id
sups defn :: TypeDefn
defn)
           | Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
j Set Id
sups -> [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "repeated supertype" Id
j]
           | Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
i (Set Id -> Bool) -> Set Id -> Bool
forall a b. (a -> b) -> a -> b
$ TypeMap -> Id -> Set Id
superIds TypeMap
tm Id
j -> do
                   [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning
                            ("made '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String -> String
showId Id
i "' an alias of") Id
j]
                   Bool -> Id -> TypeScheme -> Kind -> State Env Bool
addAliasType Bool
False Id
i ([TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [] (Id -> RawKind -> Int -> Type
TypeName Id
j RawKind
ok 0)
                                                    (Range -> TypeScheme) -> Range -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Id -> Range
posOfId Id
j) Kind
kind
                   () -> State Env ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
           | Bool
otherwise -> let Result _ (Just rk :: RawKind
rk) = Kind -> ClassMap -> Result RawKind
anaKindM Kind
kind ClassMap
cm in
                State Env ()
-> (RawKind -> State Env ()) -> Maybe RawKind -> State Env ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Diagnosis] -> State Env ()
addDiags ([Diagnosis] -> State Env ()) -> [Diagnosis] -> State Env ()
forall a b. (a -> b) -> a -> b
$ Id -> RawKind -> RawKind -> [Diagnosis]
forall a.
(GetRange a, Pretty a) =>
a -> RawKind -> RawKind -> [Diagnosis]
diffKindDiag Id
i RawKind
ok RawKind
rk)
                (State Env () -> RawKind -> State Env ()
forall a b. a -> b -> a
const (State Env () -> RawKind -> State Env ())
-> State Env () -> RawKind -> State Env ()
forall a b. (a -> b) -> a -> b
$ TypeMap -> State Env ()
putTypeMap (TypeMap -> State Env ()) -> TypeMap -> State Env ()
forall a b. (a -> b) -> a -> b
$ Id -> TypeInfo -> TypeMap -> TypeMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
i
                          (RawKind -> Set Kind -> Set Id -> TypeDefn -> TypeInfo
TypeInfo RawKind
ok Set Kind
ks (Id -> Set Id -> Set Id
forall a. Ord a => a -> Set a -> Set a
Set.insert Id
j Set Id
sups) TypeDefn
defn) TypeMap
tm)
                (Maybe RawKind -> State Env ()) -> Maybe RawKind -> State Env ()
forall a b. (a -> b) -> a -> b
$ String -> RawKind -> RawKind -> Maybe RawKind
forall (m :: * -> *).
MonadFail m =>
String -> RawKind -> RawKind -> m RawKind
minRawKind "" RawKind
ok RawKind
rk

-- | add an alias type definition
addAliasType :: Bool -> Id -> TypeScheme -> Kind -> State Env Bool
addAliasType :: Bool -> Id -> TypeScheme -> Kind -> State Env Bool
addAliasType b :: Bool
b i :: Id
i sc :: TypeScheme
sc fullKind :: Kind
fullKind = do
    TypeScheme
newSc <- TypeScheme -> State Env TypeScheme
generalizeT TypeScheme
sc
    Bool -> Id -> TypeScheme -> Kind -> State Env Bool
addAliasTypeAux Bool
b Id
i TypeScheme
newSc Kind
fullKind

addAliasTypeAux :: Bool -> Id -> TypeScheme -> Kind -> State Env Bool
addAliasTypeAux :: Bool -> Id -> TypeScheme -> Kind -> State Env Bool
addAliasTypeAux b :: Bool
b i :: Id
i (TypeScheme args :: [TypeArg]
args ty :: Type
ty ps :: Range
ps) fullKind :: Kind
fullKind =
  if Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Id
i ([Id] -> Bool) -> [Id] -> Bool
forall a b. (a -> b) -> a -> b
$ ((Int, (Id, RawKind)) -> Id) -> [(Int, (Id, RawKind))] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map ((Id, RawKind) -> Id
forall a b. (a, b) -> a
fst ((Id, RawKind) -> Id)
-> ((Int, (Id, RawKind)) -> (Id, RawKind))
-> (Int, (Id, RawKind))
-> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (Id, RawKind)) -> (Id, RawKind)
forall a b. (a, b) -> b
snd) ([(Int, (Id, RawKind))] -> [Id]) -> [(Int, (Id, RawKind))] -> [Id]
forall a b. (a -> b) -> a -> b
$ (Int -> Bool) -> Type -> [(Int, (Id, RawKind))]
leaves (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0) Type
ty then do
    [Diagnosis] -> State Env ()
addDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "cyclic alias type" Id
i]
    Bool -> State Env Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  else Bool -> TypeDefn -> Kind -> Id -> State Env Bool
addTypeId Bool
b (Type -> TypeDefn
AliasTypeDefn (Type -> TypeDefn) -> Type -> TypeDefn
forall a b. (a -> b) -> a -> b
$ (TypeArg -> Type -> Type) -> Type -> [TypeArg] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ t :: TypeArg
t y :: Type
y -> TypeArg -> Type -> Range -> Type
TypeAbs TypeArg
t Type
y Range
ps) Type
ty [TypeArg]
args)
        Kind
fullKind Id
i