f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

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

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

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst SchulzMaintainer : maeder@tzi.de

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst SchulzStability : provisional

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst SchulzPortability : non-portable (MonadState)

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulzanalyse generic var (or type var) decls

1b353d403dbdb365ae93a568f32b3ebf5698cab5Ewaryst Schulz

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz-}

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulzmodule HasCASL.VarDecl where

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulzimport Data.Maybe

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulzimport Data.List

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz

4d82cd7c26bfde17669c8bcb3986d62ef0e47d05Christian Maederimport qualified Common.Lib.Map as Map

4d82cd7c26bfde17669c8bcb3986d62ef0e47d05Christian Maederimport qualified Common.Lib.Set as Set

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulzimport Common.Id

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulzimport Common.AS_Annotation

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulzimport Common.Lib.State

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulzimport Common.Result

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulzimport HasCASL.As

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulzimport HasCASL.Le

4d82cd7c26bfde17669c8bcb3986d62ef0e47d05Christian Maederimport HasCASL.ClassAna

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulzimport HasCASL.TypeAna

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulzimport HasCASL.Unify

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport HasCASL.Merge

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz-- | add diagnostic messages

4d82cd7c26bfde17669c8bcb3986d62ef0e47d05Christian MaederaddDiags :: [Diagnosis] -> State Env ()

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst SchulzaddDiags ds =

4d82cd7c26bfde17669c8bcb3986d62ef0e47d05Christian Maeder do e <- get

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz put $ e {envDiags = ds ++ envDiags e}

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz-- | add sentences

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst SchulzappendSentences :: [Named Sentence] -> State Env ()

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst SchulzappendSentences fs =

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz do e <- get

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz put $ e {sentences = sentences e ++ fs}

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst SchulzanaStarType :: Type -> State Env (Maybe Type)

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst SchulzanaStarType t = do mp <- fromResult (anaType (Just star, t) . typeMap)

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz return $ fmap snd mp

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst SchulzanaInstTypes :: [Type] -> State Env [Type]

4d82cd7c26bfde17669c8bcb3986d62ef0e47d05Christian MaederanaInstTypes ts = if null ts then return []

4d82cd7c26bfde17669c8bcb3986d62ef0e47d05Christian Maeder else do mp <- fromResult (anaType (Nothing, head ts) . typeMap)

4442a735444b0696aa5d81e78023a570f17d3a31Christian Maeder rs <- anaInstTypes $ tail ts

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz return $ case mp of

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz Nothing -> rs

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz Just (_, ty) -> ty:rs

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz

4d82cd7c26bfde17669c8bcb3986d62ef0e47d05Christian MaederanaTypeScheme :: TypeScheme -> State Env (Maybe TypeScheme)

4442a735444b0696aa5d81e78023a570f17d3a31Christian MaederanaTypeScheme (TypeScheme tArgs (q :=> ty) p) =

4d82cd7c26bfde17669c8bcb3986d62ef0e47d05Christian Maeder do tm <- gets typeMap -- save global variables

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz mArgs <- mapM anaTypeVarDecl tArgs

4442a735444b0696aa5d81e78023a570f17d3a31Christian Maeder let newArgs = catMaybes mArgs

4442a735444b0696aa5d81e78023a570f17d3a31Christian Maeder checkUniqueTypevars newArgs

4442a735444b0696aa5d81e78023a570f17d3a31Christian Maeder mt <- anaStarType ty

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz putTypeMap tm -- forget local variables

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz case mt of

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz Nothing -> return Nothing

75f241761ba1566fbec547ae45d276683e5a8e80Ewaryst Schulz Just newTy -> return $ Just $ TypeScheme newArgs (q :=> newTy) p

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz

24ec53d5bdce82359ca637fc98a17b3023dbd1a5Eugen KuksaanaKind :: Kind -> State Env Kind

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst SchulzanaKind k = toState star $ anaKindM k

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst Schulz

75f241761ba1566fbec547ae45d276683e5a8e80Ewaryst SchulztoState :: a -> (Env -> Result a) -> State Env a

f0a8cb240fea2ac6868275be657f48f4470d9932Ewaryst SchulztoState bot r = do

75f241761ba1566fbec547ae45d276683e5a8e80Ewaryst Schulz ma <- fromResult r

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case ma of

Nothing -> return bot

Just a -> return a

fromResult :: (Env -> Result a) -> State Env (Maybe a)

fromResult f = do

e <- get

let r = f e

addDiags $ diags r

return $ maybeResult r

-- ---------------------------------------------------------------------------

-- storing type ids with their kind and definition

-- ---------------------------------------------------------------------------

-- | store a complete type map

putTypeMap :: TypeMap -> State Env ()

putTypeMap tk = do { e <- get; put e { typeMap = tk } }

-- | store type id and check kind arity (warn on redeclared types)

addTypeId :: Bool -> TypeDefn -> Instance -> Kind -> Id -> State Env (Maybe Id)

addTypeId warn defn _ kind i =

do let nk = rawKind kind

if placeCount i <= kindArity TopLevel nk then

do addTypeKind warn defn i kind

return $ Just i

else do addDiags [mkDiag Error "wrong arity of" i]

return Nothing

-- | store type as is (warn on redeclared types)

addTypeKind :: Bool -> TypeDefn -> Id -> Kind -> State Env ()

addTypeKind warn d i k =

do tk <- gets typeMap

c <- gets counter

let rk = rawKind k

case Map.lookup i tk of

Nothing -> putTypeMap $ Map.insert i

(TypeInfo rk [k] [] d) tk

Just (TypeInfo ok ks sups defn) ->

if rk == ok

then do let isKnownInst = k `elem` ks

insts = if isKnownInst then ks else

mkIntersection (k:ks)

Result ds mDef = mergeTypeDefn tk c defn d

if warn && isKnownInst && case (defn, d) of

(PreDatatype, DatatypeDefn _) -> False

_ -> True

then

addDiags [mkDiag Hint

"redeclared type" i]

else return ()

case mDef of

Just newDefn -> putTypeMap $ Map.insert i

(TypeInfo ok insts sups newDefn) tk

Nothing -> addDiags $ map (improveDiag i) ds

else addDiags $ diffKindDiag i ok rk

-- | analyse a type argument and look up a missing kind

anaTypeVarDecl :: TypeArg -> State Env (Maybe TypeArg)

anaTypeVarDecl(TypeArg t k s ps) =

case k of

MissingKind -> do

tk <- gets typeMap

let rm = getIdKind tk t

case maybeResult rm of

Nothing -> anaTypeVarDecl(TypeArg t star s ps)

Just oldK -> addTypeVarDecl False (TypeArg t oldK s ps)

_ -> do nk <- anaKind k

addTypeVarDecl True $ TypeArg t nk s ps

-- | add an analysed type argument (warn on redeclared types)

addTypeVarDecl :: Bool -> TypeArg -> State Env (Maybe TypeArg)

addTypeVarDecl warn ta@(TypeArg t k _ _) =

do mi <- addTypeId warn TypeVarDefn Plain k t

return $ fmap (const ta) mi

-- | compute arity from a 'Kind'

kindArity :: ApplMode -> Kind -> Int

kindArity m k =

case k of

FunKind k1 k2 _ -> case m of

TopLevel -> kindArity OnlyArg k1 +

kindArity TopLevel k2

OnlyArg -> 1

Universe _ -> case m of

TopLevel -> 0

OnlyArg -> 1

ClassKind _ ck -> kindArity m ck

Downset _ _ dk _ -> kindArity m dk

Intersection (k1:_) _ -> kindArity m k1

ExtKind ek _ _ -> kindArity m ek

_ -> error "kindArity"

-- ---------------------------------------------------------------------------

-- for storing selectors and constructors

-- ---------------------------------------------------------------------------

-- | store assumptions

putAssumps :: Assumps -> State Env ()

putAssumps as = do { e <- get; put e { assumps = as } }

-- | get matching information of uninstantiated identifier

findOpId :: Env -> UninstOpId -> TypeScheme -> Maybe OpInfo

findOpId e i sc = listToMaybe $ fst $ partitionOpId e i sc

-- | partition information of an uninstantiated identifier

partitionOpId :: Env -> UninstOpId -> TypeScheme -> ([OpInfo], [OpInfo])

partitionOpId e i sc =

let l = Map.findWithDefault (OpInfos []) i $ assumps e

in partition (isUnifiable (typeMap e) (counter e) sc . opType) $ opInfos l

-- | storing an operation

addOpId :: UninstOpId -> TypeScheme -> [OpAttr] -> OpDefn

-> State Env (Maybe UninstOpId)

addOpId i sc attrs defn =

do e <- get

let tm = typeMap e

as = assumps e

c = counter e

(TypeScheme _ (_ :=> ty) _) = sc

ds = if placeCount i > 1 then case unalias tm ty of

FunType (ProductType ts _) _ _ _ ->

if placeCount i /= length ts then

[mkDiag Error "wrong number of places in" i]

else []

_ -> [mkDiag Error "expected tuple argument for" i]

else []

(l,r) = partitionOpId e i sc

oInfo = OpInfo sc attrs defn

if null ds then

if null l then do putAssumps $ Map.insert i

(OpInfos (oInfo : r )) as

return $ Just i

else do let Result es mo = mergeOpInfo tm c (head l) oInfo

addDiags $ map (improveDiag i) es

case mo of

Nothing -> return Nothing

Just oi -> do putAssumps $ Map.insert i

(OpInfos (oi : r )) as

return $ Just i

else do addDiags ds

return Nothing

----------------------------------------------------------------------------

-- GenVarDecl

-----------------------------------------------------------------------------

addGenVarDecl :: GenVarDecl -> State Env (Maybe GenVarDecl)

addGenVarDecl(GenVarDecl v) = do mv <- addVarDecl v

return $ fmap GenVarDecl mv

addGenVarDecl(GenTypeVarDecl t) = do mt <- addTypeVarDecl True t

return $ fmap GenTypeVarDecl mt

anaGenVarDecl :: GenVarDecl -> State Env (Maybe GenVarDecl)

anaGenVarDecl(GenVarDecl v) = optAnaVarDecl v

anaGenVarDecl(GenTypeVarDecl t) =

anaTypeVarDecl t >>= (return . fmap GenTypeVarDecl)

convertTypeToKind :: Type -> State Env (Maybe Kind)

convertTypeToKind (FunType t1 FunArr t2 ps) =

do mk1 <- convertTypeToKind t1

mk2 <- convertTypeToKind t2

case (mk1, mk2) of

(Just k1, Just k2) -> case k2 of

ExtKind _ _ _ -> return Nothing

_ -> return $ Just $ FunKind k1 k2 ps

_ -> return Nothing

convertTypeToKind (BracketType Parens [] _) =

return Nothing

convertTypeToKind (BracketType Parens [t] _) =

convertTypeToKind t

convertTypeToKind (BracketType Parens ts ps) =

do cs <- mapM convertTypeToKind ts

if all isJust cs then

do let k:ks = catMaybes cs

rk = rawKind k

if all ((==rk) . rawKind) ks then

return $ Just $ Intersection (k:ks) ps

else return Nothing

else return Nothing

convertTypeToKind (MixfixType [t1, TypeToken t]) =

let s = tokStr t

v = case s of

"+" -> CoVar

"-" -> ContraVar

_ -> InVar

in case v of

InVar -> do return Nothing

_ -> do mk1 <- convertTypeToKind t1

case mk1 of

Just k1 -> return $ Just $ ExtKind k1 v [tokPos t]

_ -> return Nothing

convertTypeToKind(TypeToken t) =

if tokStr t == "Type" then return $ Just $ Universe [tokPos t] else do

let ci = simpleIdToId t

cm <- gets classMap

let rm = anaClassId ci cm

case maybeResult rm of

Nothing -> return Nothing

Just k -> return $ Just $ ClassKind ci k

convertTypeToKind _ =

do return Nothing

optAnaVarDecl :: VarDecl -> State Env (Maybe GenVarDecl)

optAnaVarDecl vd@(VarDecl v t s q) =

let varDecl = do mvd <- anaVarDecl vd

case mvd of

Nothing -> return Nothing

Just nvd -> do mmvd <- addVarDecl $ makeMonomorph nvd

return $ fmap GenVarDecl mmvd

in if isSimpleId v then

do mk <- convertTypeToKind t

case mk of

Just k -> do addDiags [mkDiag Hint "is type variable" v]

tv <- anaTypeVarDecl $ TypeArg v k s q

return $ fmap GenTypeVarDecl tv

_ -> varDecl

else varDecl

makeMonomorph :: VarDecl -> VarDecl

makeMonomorph (VarDecl v t sk ps) =

let s = Map.fromAscList $ map ( \ a@(TypeArg i k _ _) ->

(a, TypeName i k 0)) $

Set.toList $ varsOf t

in VarDecl v (subst s t) sk ps

-- | analyse

anaVarDecl :: VarDecl -> State Env (Maybe VarDecl)

anaVarDecl(VarDecl v oldT sk ps) =

do mt <- anaStarType oldT

return $ case mt of

Nothing -> Nothing

Just t -> Just $ VarDecl v t sk ps

-- | add a local variable with an analysed type

addVarDecl :: VarDecl -> State Env (Maybe VarDecl)

addVarDecl vd@(VarDecl v t _ _) =

do newV <- addOpId v (simpleTypeScheme t) [] VarDefn

return $ fmap (const vd) newV

-- | get the variable

getVar :: VarDecl -> Id

getVar(VarDecl v _ _ _) = v

-- | check uniqueness of variables

checkUniqueVars :: [VarDecl] -> State Env ()

checkUniqueVars = addDiags . checkUniqueness . map getVar

-- | check uniqueness of type variables

checkUniqueTypevars :: [TypeArg] -> State Env ()

checkUniqueTypevars = addDiags . checkUniqueness

. map getTypeVar

-- | filter out assumption

filterAssumps :: (OpInfo -> Bool) -> Assumps -> Assumps

filterAssumps p =

Map.filter (not . null . opInfos) .

Map.map (OpInfos . filter p . opInfos)