{- |

Module : $Header$

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

Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

Maintainer : hets@tzi.de

Stability : provisional

Portability : non-portable (MonadState)

analyse alternatives of data types

-}

module HasCASL.DataAna where

import Common.Id

import Common.Lib.State

import qualified Common.Lib.Set as Set

import Common.Result

import HasCASL.As

import HasCASL.Le

import HasCASL.VarDecl

import HasCASL.AsUtils

import HasCASL.Unify

import Data.Maybe

anaAlts :: [(Id, Type)] -> Type -> [Alternative] -> State Env [AltDefn]

anaAlts tys dt alts =

do ll <- mapM (anaAlt tys dt) alts

let l = concat ll

addDiags (checkUniqueness $ map ( \ (Construct i _ _ _) -> i) l)

return l

anaAlt :: [(Id, Type)] -> Type -> Alternative -> State Env [AltDefn]

anaAlt _ _ (Subtype _ _) = return []

anaAlt tys dt (Constructor i cs p _) =

do newCs <- mapM (anaComps tys dt) cs

let mts = map fst newCs

if all isJust mts then

do let sels = concatMap snd newCs

con = Construct i (catMaybes mts) p sels

-- check for disjoint selectors

addDiags (checkUniqueness $ map ( \ (Select s _ _) -> s ) sels)

return [con]

else return []

anaComps :: [(Id, Type)] -> Type -> [Component]

-> State Env (Maybe Type, [Selector])

anaComps tys rt cs =

do newCs <- mapM (anaComp tys rt) cs

let mts = map fst newCs

if all isJust mts then return (Just $ mkProductType (catMaybes mts) [],

concatMap snd newCs)

else return (Nothing, [])

anaComp :: [(Id, Type)] -> Type -> Component

-> State Env (Maybe Type, [Selector])

anaComp tys rt (Selector s p t _ _) =

do mt <- anaCompType tys rt t

case mt of

Just ct -> return (mt, [Select s ct p])

_ -> return (Nothing, [])

anaComp tys rt (NoSelector t) =

do mt <- anaCompType tys rt t

return (mt, [])

getSelType :: Type -> Partiality -> Type -> Type

getSelType dt p rt = (case p of

Partial -> addPartiality [dt]

Total -> id) $ FunType dt FunArr rt []

anaCompType :: [(Id, Type)] -> Type -> Type -> State Env (Maybe Type)

anaCompType tys dt t = do

mt <- anaStarType t

case mt of

Nothing -> return Nothing

Just ct -> do mt2 <- unboundTypevars (varsOf dt) ct

case mt2 of

Nothing -> return Nothing

Just ct2 -> do

ms <- mapM

(checkMonomorphRecursion ct2) tys

return $ if and ms then Just ct2

else Nothing

checkMonomorphRecursion :: Type -> (Id, Type) -> State Env Bool

checkMonomorphRecursion t (i, rt) = do

tm <- gets typeMap

if occursIn tm i $ unalias tm t then

if equalSubs tm t rt

then return True

else do addDiags [Diag Error ("illegal polymorphic recursion"

++ expected rt t) $ getMyPos t]

return False

else return True

unboundTypevars :: Set.Set TypeArg -> Type -> State Env (Maybe Type)

unboundTypevars args ct = do

let restVars = varsOf ct Set.\\ args

if Set.isEmpty restVars then do return $ Just ct

else do addDiags [mkDiag Error ("unbound type variable(s)\n\t"

++ showSepList ("," ++) showPretty

(Set.toList restVars) " in") ct]

return Nothing