{- |

Module : ./HasCASL/TypeDecl.hs

Description : analyse type declarations

Copyright : (c) Christian Maeder and Uni Bremen 2002-2005

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

analyse type declarations

-}

module HasCASL.TypeDecl

( anaFormula

, mapAnMaybe

, anaTypeItems

, dataPatToType

, ana1Datatype

, anaDatatype

, addDataSen

) where

import Common.Id

import Common.AS_Annotation

import Common.Lib.State

import qualified Data.Map as Map

import qualified Data.Set as Set

import Common.Result

import HasCASL.As

import HasCASL.AsUtils

import HasCASL.Builtin

import HasCASL.Le

import HasCASL.ClassAna

import HasCASL.TypeAna

import HasCASL.ConvertTypePattern

import HasCASL.DataAna

import HasCASL.Unify

import HasCASL.VarDecl

import HasCASL.SubtypeDecl

import HasCASL.MixAna

import HasCASL.TypeCheck

import Control.Monad

import Data.Maybe

import Data.List (group)

-- | resolve and type check a formula

anaFormula :: Annoted Term -> State Env (Maybe (Annoted Term, Annoted Term))

anaFormula at = do

rt <- resolve $ item at

case rt of

Nothing -> return Nothing

Just t -> do

mt <- typeCheck (mkLazyType unitType) t

return $ case mt of

Nothing -> Nothing

Just e -> Just (at { item = t }, at { item = e })

anaVars :: Env -> Vars -> Type -> Result Term

anaVars te vv t = case vv of

Var v -> return $ QualVar $ VarDecl v t Other $ posOfId v

VarTuple vs ps -> let

(topTy, ts) = getTypeAppl t

n = length ts in

if n > 1 && lesserType te topTy (toProdType n nullRange) then

if n == length vs then

let lrs = zipWith (anaVars te) vs ts

lms = map maybeResult lrs in

if all isJust lms then

return $ TupleTerm (map fromJust lms) ps

else Result (concatMap diags lrs) Nothing

else mkError "wrong arity" topTy

else mkError "product type expected" topTy

-- | lift a analysis function to annotated items

mapAnMaybe :: (Monad m) => (Annoted a -> m (Maybe b)) -> [Annoted a]

-> m [Annoted b]

mapAnMaybe f al = do

il <- mapM f al

return $ map ( \ (i, a) -> replaceAnnoted (fromJust i) a) $

filter (isJust . fst) $ zip il al

-- | analyse annotated type items

anaTypeItems :: GenKind -> [Annoted TypeItem] -> State Env [Annoted TypeItem]

anaTypeItems gk l = do

ul <- mapAnMaybe ana1TypeItem l

tys <- fmap reverse $ foldM ( \ r i -> case item i of

Datatype d -> fmap (: r) $ dataPatToType d

_ -> return r) [] ul

rl <- mapAnMaybe (anaTypeItem gk tys) ul

addDataSen tys

return rl

-- | add sentences for data type definitions

addDataSen :: [DataPat] -> State Env ()

addDataSen tys = do

tm <- gets typeMap

let tis = map ( \ (DataPat _ i _ _ _) -> i) tys

ds = foldr ( \ i dl -> case Map.lookup i tm of

Nothing -> dl

Just ti -> case typeDefn ti of

DatatypeDefn dd -> dd : dl

_ -> dl) [] tis

sen = (makeNamed ("ga_" ++ showSepList (showString "_") showId tis "")

$ DatatypeSen ds) { isDef = True }

unless (null tys) $ appendSentences [sen]

ana1TypeItem :: Annoted TypeItem -> State Env (Maybe TypeItem)

ana1TypeItem t = case item t of

Datatype d -> do

md <- ana1Datatype $ replaceAnnoted d t

return $ fmap Datatype md

i -> return $ Just i

anaTypeDecl :: [TypePattern] -> Kind -> Range -> State Env (Maybe TypeItem)

anaTypeDecl pats kind ps = do

cm <- gets classMap

let Result cs _ = anaKindM kind cm

Result ds (Just is) = convertTypePatterns pats

addDiags $ cs ++ ds

let ak = if null cs then kind else universe

mis <- mapM (addTypePattern NoTypeDefn ak) is

let newPats = map toTypePattern $ catMaybes mis

return $ if null newPats then Nothing else Just $ TypeDecl newPats ak ps

anaIsoDecl :: [TypePattern] -> Range -> State Env (Maybe TypeItem)

anaIsoDecl pats ps = do

let Result ds (Just is) = convertTypePatterns pats

addDiags ds

mis <- mapM (addTypePattern NoTypeDefn universe) is

case catMaybes mis of

[] -> return Nothing

nis -> do

let (i, _) : ris = reverse nis

mapM_ (\ (j, _) -> addAliasType False j

(TypeScheme [] (TypeName i rStar 0) $ posOfId j) universe) ris

return $ Just $ IsoDecl (map toTypePattern nis) ps

setTypePatternVars :: [(Id, [TypeArg])] -> State Env [(Id, [TypeArg])]

setTypePatternVars ol = do

l <- mapM ( \ (i, tArgs) -> do

e <- get

newAs <- mapM anaddTypeVarDecl tArgs

put e

return (i, catMaybes newAs)) ol

let g = group $ map snd l

case g of

[_ : _] -> do

newAs <- mapM anaddTypeVarDecl $ snd $ head l

return $ map ( \ (i, _) -> (i, catMaybes newAs)) l

_ -> do

addDiags [mkDiag Error

"variables must be identical for all types within one item" l]

return []

anaSubtypeDecl :: [TypePattern] -> Type -> Range -> State Env (Maybe TypeItem)

anaSubtypeDecl pats t ps = do

let Result ds (Just is) = convertTypePatterns pats

addDiags ds

tvs <- gets localTypeVars

nis <- setTypePatternVars is

let newPats = map toTypePattern nis

te <- get

putLocalTypeVars tvs

let Result es mp = anaTypeM (Nothing, t) te

case mp of

Nothing -> do

mapM_ (addTypePattern NoTypeDefn universe) is

if null newPats then return Nothing else case t of

TypeToken tt -> do

let tid = simpleIdToId tt

newT = TypeName tid rStar 0

addTypeId False NoTypeDefn universe tid

mapM_ (addSuperType newT universe) nis

return $ Just $ SubtypeDecl newPats newT ps

_ -> do

addDiags es

return $ Just $ TypeDecl newPats universe ps

Just ((rk, ks), newT) -> nonUniqueKind ks rk t $ \ kind -> do

mapM_ (addTypePattern NoTypeDefn kind) is

mapM_ (addSuperType newT $ rawToKind rk) nis

return $ if null nis then Nothing else

Just $ SubtypeDecl newPats newT ps

anaSubtypeDefn :: Annoted TypeItem -> TypePattern -> Vars -> Type

-> Annoted Term -> Range -> State Env (Maybe TypeItem)

anaSubtypeDefn aitm pat v t f ps = do

let Result ds m = convertTypePattern pat

addDiags ds

case m of

Nothing -> return Nothing

Just (i, tArgs) -> do

tvs <- gets localTypeVars

newAs <- mapM anaddTypeVarDecl tArgs

mt <- anaStarType t

putLocalTypeVars tvs

case mt of

Nothing -> return Nothing

Just ty -> do

let nAs = catMaybes newAs

fullKind = typeArgsListToKind nAs universe

jTy = TypeName i (typeArgsListToRawKind nAs rStar) 0

aTy = mkTypeAppl jTy $ map typeArgToType nAs

e <- get

let Result es mvds = anaVars e v $ monoType ty

addDiags es

if cyclicType i ty then do

addDiags [mkDiag Error

"illegal recursive subtype definition" ty]

return Nothing

else case mvds of

Nothing -> return Nothing

Just vtt -> do

let vds = extractVars vtt

checkUniqueVars vds

vs <- gets localVars

mapM_ (addLocalVar True) vds

mf <- anaFormula f

putLocalVars vs

case mf of

Nothing -> return Nothing

Just (newF, resF) -> do

addTypeId True NoTypeDefn fullKind i

addSuperType ty universe (i, nAs)

let lab1 = getRLabel resF

lab = if null lab1 then getRLabel aitm else lab1

appendSentences [makeNamed lab

$ Formula $ mkEnvForall e (

mkForall (map GenVarDecl vds)

$ mkLogTerm eqvId ps

(TypedTerm vtt InType aTy ps) $ item resF) ps]

return $ Just $ SubtypeDefn (TypePattern i nAs nullRange)

v ty newF ps

anaAliasType :: TypePattern -> Maybe Kind -> TypeScheme

-> Range -> State Env (Maybe TypeItem)

anaAliasType pat mk sc ps = do

let Result ds m = convertTypePattern pat

addDiags ds

case m of

Nothing -> return Nothing

Just (i, tArgs) -> do

tvs <- gets localTypeVars -- save variables

newAs <- mapM anaddTypeVarDecl tArgs

(ik, mt) <- anaPseudoType mk sc

putLocalTypeVars tvs

case mt of

Nothing -> return Nothing

Just (TypeScheme args ty qs) ->

if cyclicType i ty then do

addDiags [mkDiag Error "illegal recursive type synonym" ty]

return Nothing

else do

let nAs = catMaybes newAs

allArgs = nAs ++ args

fullKind = typeArgsListToKind nAs ik

allSc = TypeScheme allArgs ty qs

b <- addAliasType True i allSc fullKind

tm <- gets typeMap

putTypeMap $ Map.map ( \ ti -> case typeDefn ti of

AliasTypeDefn y -> ti

{ typeDefn = AliasTypeDefn $ expandAux tm y }

_ -> ti) tm

return $ if b then Just $ AliasType

(TypePattern i [] nullRange) (Just fullKind) allSc ps

else Nothing

-- | analyse a 'TypeItem'

anaTypeItem :: GenKind -> [DataPat] -> Annoted TypeItem

-> State Env (Maybe TypeItem)

anaTypeItem gk tys aitm = case item aitm of

TypeDecl pats kind ps -> anaTypeDecl pats kind ps

SubtypeDecl pats t ps -> anaSubtypeDecl pats t ps

IsoDecl pats ps -> anaIsoDecl pats ps

SubtypeDefn pat v t f ps -> anaSubtypeDefn aitm pat v t f ps

AliasType pat mk sc ps -> anaAliasType pat mk sc ps

Datatype d -> do

mD <- anaDatatype gk tys $ replaceAnnoted d aitm

case mD of

Nothing -> return Nothing

Just newD -> return $ Just $ Datatype newD

-- | pre-analyse a data type for 'anaDatatype'

ana1Datatype :: Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl)

ana1Datatype aitm = do

let DatatypeDecl pat kind alts derivs ps = item aitm

cm <- gets classMap

let Result cs (Just rk) = anaKindM kind cm

k = if null cs then kind else universe

addDiags $ checkKinds pat rStar rk ++ cs

let rms = map ( \ c -> anaKindM (ClassKind c) cm) derivs

mcs = map maybeResult rms

jcs = catMaybes mcs

newDerivs = map fst $ filter (isJust . snd) $ zip derivs mcs

Result ds m = convertTypePattern pat

addDiags (ds ++ concatMap diags rms)

addDiags $ concatMap (checkKinds pat rStar) jcs

case m of

Nothing -> return Nothing

Just (i, tArgs) -> do

tvs <- gets localTypeVars

newAs <- mapM anaddTypeVarDecl tArgs

putLocalTypeVars tvs

let nAs = catMaybes newAs

fullKind = typeArgsListToKind nAs k

addDiags $ checkUniqueTypevars nAs

b <- addTypeId False PreDatatype fullKind i

return $ if b then Just $ DatatypeDecl

(TypePattern i nAs nullRange) k alts newDerivs ps

else Nothing

-- | convert a data type with an analysed type pattern to a data pattern

dataPatToType :: DatatypeDecl -> State Env DataPat

dataPatToType d = case d of

DatatypeDecl (TypePattern i nAs _) k _ _ _ -> do

rk <- anaKind k

return $ DataPat Map.empty i nAs rk $ patToType i nAs rk

_ -> error "dataPatToType"

addDataSubtype :: DataPat -> Kind -> Type -> State Env ()

addDataSubtype (DataPat _ _ nAs _ rt) k st = case st of

TypeName i _ _ -> addSuperType rt k (i, nAs)

_ -> addDiags [mkDiag Warning "data subtype ignored" st]

-- | analyse a pre-analysed data type given all data patterns of the type item

anaDatatype :: GenKind -> [DataPat]

-> Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl)

anaDatatype genKind tys d = case item d of

itd@(DatatypeDecl (TypePattern i nAs _) k alts _ _) -> do

-- recompute data pattern rather than looking it up in tys

dt@(DataPat _ _ _ rk _) <- dataPatToType itd

let fullKind = typeArgsListToKind nAs k

tvs <- gets localTypeVars

mapM_ (addTypeVarDecl False . nonVarTypeArg) nAs

mNewAlts <- fromResult $ anaAlts genKind tys dt (map item alts)

putLocalTypeVars tvs

case mNewAlts of

Nothing -> return Nothing

Just newAlts -> do

mapM_ (addDataSubtype dt fullKind) $ foldr

( \ (Construct mc ts _ _) l -> case mc of

Nothing -> ts ++ l

Just _ -> l) [] newAlts

let gArgs = genTypeArgs nAs

iMap = Map.fromList $ map (\ (DataPat _ j _ _ _) -> (j, j)) tys

de = DataEntry iMap i genKind gArgs rk

$ Set.fromList newAlts

dp = toDataPat de

mapM_ ( \ (Construct mc tc p sels) -> case mc of

Nothing -> return ()

Just c -> do

let sc = getConstrScheme dp p tc

addOpId c sc Set.empty (ConstructData i)

mapM_ ( \ (Select ms ts pa) -> case ms of

Just s ->

addOpId s (getSelScheme dp pa ts) Set.empty $ SelectData

(Set.singleton $ ConstrInfo c sc) i

Nothing -> return False) $ concat sels) newAlts

addTypeId True (DatatypeDefn de) fullKind i

appendSentences $ makeDataSelEqs dp newAlts

return $ Just itd

_ -> error "anaDatatype (not preprocessed)"

-- | analyse a pseudo type (represented as a 'TypeScheme')

anaPseudoType :: Maybe Kind -> TypeScheme -> State Env (Kind, Maybe TypeScheme)

anaPseudoType mk (TypeScheme tArgs ty p) = do

cm <- gets classMap

let k = case mk of

Nothing -> Nothing

Just j -> let Result cs _ = anaKindM j cm

in Just $ if null cs then j else universe

nAs <- mapM anaddTypeVarDecl tArgs

let ntArgs = catMaybes nAs

mp <- anaType (Nothing, ty)

case mp of

Nothing -> return (universe, Nothing)

Just ((_, sks), newTy) -> case Set.toList sks of

[sk] -> do

let newK = typeArgsListToKind ntArgs sk

irk <- anaKind newK

case k of

Nothing -> return ()

Just j -> do

grk <- anaKind j

addDiags $ checkKinds ty grk irk

return (newK, Just $ TypeScheme ntArgs newTy p)

_ -> return (universe, Nothing)

-- | add a type pattern

addTypePattern :: TypeDefn -> Kind -> (Id, [TypeArg])

-> State Env (Maybe (Id, [TypeArg]))

addTypePattern defn kind (i, tArgs) = do

tvs <- gets localTypeVars

newAs <- mapM anaddTypeVarDecl tArgs

putLocalTypeVars tvs

let nAs = catMaybes newAs

fullKind = typeArgsListToKind nAs kind

addDiags $ checkUniqueTypevars nAs

b <- addTypeId True defn fullKind i

return $ if b then Just (i, nAs) else Nothing