module Type.Type(typeTopDecls) where
import List(partition)
import TokenId
import Syntax
import SyntaxPos
import IdKind
import State
import NT
import Type.Lib(typeUnify,typeUnifyMany,typeUnifyApply,typePatCon,typeExpCon
,typeIdentDict,getIdent,getTypeErrors,typeError
,typeNewTVar,typeIdentDef,checkExist,funType,extendEnv,getEnv
,getState,setState,msgPatGdExps,msgPatGd
,msgFun,msgPat,msgLit,msgBool,msgGdExps,msgAltExps,msgCase
,msgAltPats,msgIf,msgApply,msgList,msgExpType,msgAs,msgNK)
import Type.Env(initEnv,envDecls,tvarsInEnv,envPats,envPat)
import Util.Extra
import Util.MergeSort(group,unique)
import Type.Subst
import Type.Ctx
import Type.Data
import IntState
import Type.Util(ntIS)
import Type.Unify(unify)
import Nice
import Bind(identPat)
import Extract(type2NT)
import qualified Data.Map as Map
import Remove1_3
import Id(Id)
import Maybe
--import PPSyntax -- just for debugging
--import StrSyntax -- just for debugging
typeTopDecls :: ((TokenId,IdKind) -> Id)
-> Maybe [Id]
-> IntState
-> [ClassCode (Exp Id) Id]
-> Decls Id
-> ([ClassCode (Exp Id) Id],Decls Id,IntState)
typeTopDecls tidFun defaults state code topdecls =
let defaults' =
case defaults of
Nothing -> [tidFun (tInteger,TCon),tidFun (tDouble,TCon)]
Just def -> def
result = typeTopDeclScc topdecls tidFun defaults' finalState state
finalState = snd result
in case result of
(topdecls,state) ->
case mapS typeCode code tidFun state of
(code,state) ->
(code,topdecls,state)
typeCode :: ClassCode (Exp Id) Id
-> State t IntState (ClassCode (Exp Id) Id) IntState
typeCode d@(CodeClass pos cls) tidFun state = (d,state)
typeCode (CodeInstance pos cls typ _ _ ms) tidFun state =
let clsInfo = fromJust (lookupIS state cls)
sc = superclassesI clsInfo
(_,free,ctxs) = fromJust (Map.lookup typ (instancesI clsInfo))
in case uniqueISs state ctxs of
(ctxsi,state) ->
(CodeInstance pos cls typ (map snd ctxsi)
(map (buildCtx state noPos (map (mapFst (mapSnd mkNTvar)) ctxsi) . ( \ cls -> TypeDict cls (mkNTcons typ (map mkNTvar free)) [(toEnum 0,pos)])) sc) ms
,state)
typeTopDeclScc :: Decls Id
-> ((TokenId,IdKind) -> Id)
-> [Id] -> a
-> IntState
-> (Decls Id,IntState)
typeTopDeclScc (DeclsScc xs) tidFun defaults finalState state =
case mapS typeDepend xs (TypeDown initEnv tidFun defaults [] []) (TypeState state idSubst initCtxs []) of
(xs,TypeState state phi ctxs ectxsi) -> (DeclsScc (concat xs),state)
typeDeclScc :: Decls Id -> TypeMonad (Decls Id)
typeDeclScc (DeclsScc xs) =
mapS typeDepend xs >>>= \ xs ->
unitS (DeclsScc (concat xs))
typeDepend :: DeclsDepend Id
-> TypeMonad [DeclsDepend Id]
typeDepend (DeclsNoRec d13) =
fixDecl13 d13 >>>= \ d ->
typeScc [d] >>>= \ (dicts,[d]) ->
unitS (map DeclsNoRec dicts ++ [DeclsNoRec d])
typeDepend (DeclsRec ds13) =
mapS fixDecl13 ds13 >>>= \ ds ->
typeScc ds >>>= \ (dicts,ds) ->
unitS (map DeclsNoRec dicts ++ [DeclsRec ds])
--- ======== The hairy part
typeScc :: [Decl Id] -> TypeMonad ([Decl Id],[Decl Id])
typeScc decls down@(TypeDown env tidFun defaults ctxsDict envDict)
up@(TypeState state phi inCtxs ectxsi) =
let -- ctxs should only get up but the monad can not handle that!
trueExp :: Exp Id -- this expression has become superfluous,
-- but it is a lot of work to remove it from the code
trueExp = ExpCon noPos (tidFun (tTrue,Con))
nextTvar :: Id
(nextTvar,_) = uniqueIS state -- take a look at the next type variable
envHere :: [(Id, NT)]
(envHere,up') =
envDecls decls () (TypeState state phi initCtxs [])
decls' :: [Decl Id]
(decls', TypeState state'' phi'' ctxs'' existCtxsi) =
mapS typeDecl decls
(TypeDown (envHere++env) tidFun defaults
(usedCtx ++ ctxsDict)
(derivedDict ++ envDict))
up'
phiEnv :: [(Id,NT)]
phiEnv = substEnv phi'' env
phiEnvHere :: [(Id,NT)]
phiEnvHere = substEnv phi'' envHere
phiCtxs :: [TypeDict]
phiCtxs = substCtxs phi'' ctxs''
globalTVars :: [Id]
globalTVars = (unique . tvarsInEnv) phiEnv
uniqueCtxs :: [TypeDict]
uniqueCtxs = -- These contexts are needed
( map (\(TypeDict c v ip:cvips) ->
TypeDict c v (ip++concatMap (\(TypeDict c v ip)-> ip)
cvips))
. group
) phiCtxs
existCtxs :: [(Id,NT)]
existCtxs = map fst existCtxsi
globalCtxs :: [(Id,NT)]
localCtxs0 :: [(Id,NT)]
(globalCtxs,localCtxs0) = -- These are the simplified context
-- that are needed
( partition ( \ (c,nt) -> stripNT nt `elem` globalTVars)
. ctxsReduce state
. concatMap (ctxsSimplify (map getPos decls) state [])
-- . map ( \ (TypeDict c nt _) -> (c,nt))
) uniqueCtxs
localCtxs :: [(Id,NT)]
localCtxs = filter (`notElem` existCtxs) localCtxs0
-- get some unique identifiers
globalCtxsi :: [((Id,NT),Id)]
(globalCtxsi,state1) = uniqueISs state'' globalCtxs
localCtxsi :: [((Id,NT),Id)]
(localCtxsi,state2) = uniqueISs state1 localCtxs
-- Contexts that depend on type variables that are not all quantified
outCtxs :: [TypeDict]
outCtxs = map ( \ ((c,nt),i) -> TypeDict c nt [(i,noPos)]) globalCtxsi
-- Set up argument and available dictionaries for identifiers
-- without a given type
derivedArgs :: [(Id,Exp Id)]
derivedArgs = map (\((c,nt),i) -> (stripNT nt,ExpVar noPos i)) localCtxsi
derivedDict :: [(Id,[Exp Id])]
derivedDict = map (\(i,nt) -> (i, (map snd
. filter ((`elem` freeNT nt) . fst))
derivedArgs)
) phiEnvHere -- default is fixed in bindType
-- Create mapping from Int to expression for requested dictionary
usedCtx :: [(Id,Exp Id)]
usedCtx = concatMap (\(TypeDict c nt ips) ->
let dict = buildCtx state noPos
(existCtxsi++localCtxsi++globalCtxsi)
(TypeDict c nt ips)
in map (\(i,p) -> (i,dict)) ips
) uniqueCtxs
-- Insert types into state (comparing with given type if such exist)
-- and add dictionary arguments
declsDict :: [Decl Id]
declsDict = map (\(_,i) ->
case lookup i ctxsDict of
Just exp -> DeclFun noPos i [Fun [] (Unguarded exp)
(DeclsScc [])]
) globalCtxsi
(decls'',state3) = mapS bindType decls'
(globalTVars,trueExp,localCtxsi
,phiEnvHere,defaults)
state2
in
{-
strace ("usedCtx = " ++ show (map fst usedCtx)) $
strace ("globalCtxs = " ++ show globalCtxs) $
strace ("localCtxs0 = " ++ show localCtxs0) $
strace ("existCtxs = " ++ show existCtxs) $
strace ("phi'' = " ++ show phi'') $
strace ("ctxs'' = " ++ show ctxs'') $
strace ("phiCtxs = " ++ show phiCtxs) $
-}
((declsDict,decls'')
,TypeState state3 (stripSubst phi'' nextTvar) (outCtxs++inCtxs) existCtxsi)
--------------------- Fix arguments and types
isExist :: NT -> Bool
isExist (NTexist _ _) = True
isExist _ = False
bindType :: Decl Id
-> State ([Id], Exp Id, [((Id, NT), Id)], [(Id, NT)], [Id])
IntState
(Decl Id)
IntState
bindType decl@(DeclPat (Alt pat gdexps decls))
down@(globalTVars,trueExp,[],envHere,defaults) state =
-- No context for left hand patterns!
case mapS0 checkType (identPat pat) down state of
state -> (decl,state)
where
checkType (pos,ident) (globalTVars,trueExp,localCtxi,envHere,defaults) state =
case lookup ident envHere of
Nothing -> strace ("Nothing derived for " ++ show ident ++
" at "++strPos pos) state
Just derivedNT ->
let derivedFree = filter (`notElem` globalTVars)
(snub (freeNT derivedNT))
in case ntIS state ident of
(NoType,state) ->
updateIS state ident (newNT
(NewType derivedFree [] []
[polyNT derivedFree derivedNT]))
(given@(NewType givenFree [] givenCtx [givenNT]),state) ->
if length givenFree /= length derivedFree
then addError state
("Derived type " ++ show derivedFree
++ niceNT Nothing state (mkALNT derivedNT) derivedNT
++ " is not an instance of "
++ show givenFree
++ niceNT Nothing state (mkAL givenFree) givenNT
++ " at " ++ strPos pos)
else state
bindType decl@(DeclPat (Alt pat gdexps decls))
down@(globalTVars,trueExp,localCtxsi,envHere,defaults) state =
-- No context for left hand patterns!
(decl,addError (foldr typeError state (identPat pat)) errmsg)
where
errmsg = "Context for " ++ mixCommaAnd ((map (strIS state) . unique .
map (fst . fst)) localCtxsi)
++ " needed in left hand pattern at " ++ strPos (getPos pat) ++ "."
nt = NewType [toEnum 1] [] [] [mkNTvar (toEnum 1)] -- Used instead of derived type, not sure
-- if it is any idea
typeError (pos,ident) state = (updateIS state ident (newNT nt))
bindType decl@(DeclPrimitive pos fun arity typ) down state =
(decl,state)
bindType decl@(DeclForeignImp pos conv str fun arity cast typ _) down state =
(decl,state)
bindType decl@(DeclForeignExp pos conv str fun typ) down state =
(decl,state)
bindType decl@(DeclFun pos fun funs)
(globalTVars,trueExp,localCtxi,envHere,defaults) state =
case ntIS state fun of
(NoType,state) ->
let derivedNT = assocDef envHere (error "162") fun
derivedFree = filter (`notElem` globalTVars) (snub (freeNT derivedNT))
derivedCtxi :: [((Id,NT),Id)]
defaultCtxi :: [((Id,NT),Id)]
(derivedCtxi,defaultCtxi) = partition ((`elem` derivedFree) . stripNT
. snd . fst) localCtxi
in case filter (isExist . snd . fst) defaultCtxi of
[] ->
case buildDefaults pos defaultCtxi trueExp defaults state of
(defaultDecls,state) ->
(DeclFun pos fun
(map (bindFun (map (\ (c_v,i) -> ExpVar pos i)
derivedCtxi)
(map DeclsNoRec defaultDecls)) funs)
,updateIS state fun
(newNT (NewType derivedFree []
(map (mapSnd stripNT . fst)
derivedCtxi)
[polyNT derivedFree derivedNT]))
)
er -> (decl, addError state ("Dictionary can not be found "
++ "for existential types, "
++ "error detected at " ++ strPos pos)
)
(given@(NewType givenFree [] givenCtx [givenNT]),state) ->
let derivedNT = assocDef envHere (error "171") fun
in
case unify state idSubst (derivedNT,givenNT) of
Left (phi,err) ->
(decl
,addError state
("Derived type for " ++ strIS state fun ++ " at " ++ strPos pos
++" can not be unified with given type due to " ++ err
++"\nDerived:"++niceNT Nothing state (mkALNT derivedNT) derivedNT
++"\nGiven :" ++ niceNT Nothing state (mkAL givenFree) givenNT))
Right phi ->
let phis = ( foldr (\ (k,v) t -> Map.insertWith (++) k [v] t) Map.empty
. map fixSubst
. Map.toList
) phi
al = mkAL (givenFree ++ freeNT derivedNT)
fixSubst (v,NTvar v' k) = if v`elem`givenFree then (v',NTvar v k)
else (v,NTvar v' k)
fixSubst (v,NTany v') = if v`elem`givenFree then (v',mkNTvar v)
else (v,mkNTvar v')
fixSubst p = p
one2many phi = ( filter ((/= 1).length.snd)
. Map.toList) phis
freebound phi = ( filter ((`elem` givenFree).fst)
. filter ((== 1).length . snd)
. Map.toList
) phis
safePhi phi v =
case Map.lookup v phi of
Nothing -> Just v
Just xs -> findV xs
findV [NTvar v _] = Just v
findV [NTany v] = Just v
findV _ = Nothing
sameNT (NTany _) v = NTany v
sameNT (NTvar _ k) v = NTvar v k
sameNT (NTexist _ k) v = NTexist v k
localCtxi' = ( map fromJust
. filter isJust
. map (\((c,nt),i) ->
case safePhi phis (stripNT nt) of
Just v -> Just ((c,sameNT nt v),i)
Nothing -> Nothing) -- either one2many
-- of freebound
) localCtxi
(derivedCtxi,defaultCtxi) =
partition ((`elem` givenFree) . stripNT .snd.fst) localCtxi'
derivedIntPairI = map (mapFst (mapSnd stripNT)) derivedCtxi
ctxcheck ctxi = filter ((`notElem` givenCtx) . fst) ctxi
in
case (one2many phis,freebound phis,ctxcheck derivedIntPairI) of
([],[],[]) ->
-- Type is ok, but we need to introduce new unique ints
-- for excessive contexts, eg, (Eq a,Ord a)
let (mGivenCtxi',state2) =
(uniqueISs state . zip givenCtx
. map (\cv-> lookup cv derivedIntPairI)) givenCtx
givenCtxi' = map stripAndFix mGivenCtxi'
stripAndFix ((c,Nothing),u) = (c,u)
stripAndFix ((c,Just v),u) = (c,v)
in
case filter (isExist . snd . fst) defaultCtxi of
[] ->
case buildDefaults pos defaultCtxi trueExp
defaults state2 of
(defaultDecls,state3) ->
(DeclFun pos fun
(map (bindFun (map (\(c_v,i)-> ExpVar pos i)
givenCtxi')
(map DeclsNoRec defaultDecls))
funs)
,state3
)
er ->
(decl
,addError state
("Dictionary can not be found for existential types, "
++ "error detected at " ++ strPos pos
++ " (signature given)"))
(eOne2Many,eFreeBound,eCtxs) ->
let sOne2Many xs =
concatMap (\(v,nts)->
"\n type variable "
++ niceNT Nothing state al (mkNTvar v)
++ " bound to "
++ mixCommaAnd (map (niceNT Nothing state al)
nts)
) xs
sFreeBound [] = []
sFreeBound [(v,t)] =
"\n given free variable "
++ niceNT Nothing state al (mkNTvar v)
++ " is bound to " ++ niceNT Nothing state al (head t)
sFreeBound xs =
"\n given free variables "
++ mixCommaAnd (map (niceNT Nothing state al
. mkNTvar . fst) xs)
++ " are bound to "
++ mixCommaAnd (map (niceNT Nothing state al
. head . snd) xs)
++ " respectively"
sCtxs [] = ""
sCtxs xs = "\n different contexts"
in
(decl
,addError state
("Derived type for " ++ strIS state fun
++ " at " ++ strPos pos ++ " does not match due to:"
++ sOne2Many eOne2Many ++ sFreeBound eFreeBound
++ sCtxs eCtxs
++ "\nDerived:"
++ niceCtxs Nothing state al (map fst derivedIntPairI)
++ niceNT Nothing state al derivedNT
++ "\nGiven :"
++ niceCtxs Nothing state al givenCtx
++ niceNT Nothing state al givenNT))
bindFun dictArgs defaultDecls (Fun args gdexps (DeclsScc decls)) =
Fun (dictArgs++args) gdexps (DeclsScc (defaultDecls ++ decls))
--------------------- Nice
typeDecl :: Decl Id -> TypeMonad (Decl Id)
typeDecl d@(DeclPrimitive pos fun arity typ) =
unitS d
typeDecl d@(DeclForeignImp pos conv str fun arity cast typ _) =
unitS d
typeDecl d@(DeclForeignExp pos conv str fun typ) =
unitS d
typeDecl (DeclPat (Alt pat rhs decls)) =
typePat pat >>>= \(pat,patT,eTVar) ->
typeDeclScc decls >>>= \decls ->
typeRhs rhs >>>= \(rhs,rhsT) ->
typeUnify (msgPat pat) patT rhsT >>>= \_ ->
-- checkExist [] eTVar >>>
unitS (DeclPat (Alt pat rhs decls))
typeDecl (DeclFun pos fun funs) =
typeIdentDef id pos fun >>>= \ (_,funT) ->
typeNewTVar >>>= \retT ->
getIdent (t_Arrow,TCon) >>>= \arrow ->
mapS (typeFun fun arrow funT retT) funs >>>= \funs ->
{-
typeIdentDef id pos fun >>>= \ (_,funT) ->
(\down up@(TypeState state _ _ _) ->
trace ('\n':'\n': niceInt Nothing state fun
('\n': niceNT Nothing state (map (\x-> (x,'a':show x)) [1..]) funT))
(True,up)) >>>= \True ->
-}
unitS (DeclFun pos fun funs)
typeFun :: Id -> Id -> NT -> NT -> Fun Id
-> TypeMonad (Fun Id)
typeFun fun arrow funT retT (Fun args13 rhs decls) =
mapS fixPat13 args13 >>>= \ args ->
envPats args >>>= \ argsE ->
getEnv >>>= \ oldEnv ->
extendEnv argsE >=>
mapS typePat args >>>= \args ->
case unzip3 args of
(args,argsT,eTVar) ->
typeUnify (msgFun rhs) funT (funType arrow (argsT++[retT])) >>>= \_ ->
{-
(\down up@(TypeState state _ _ _) ->
trace ("\n\ntypeFun: " ++ show (length argsT) ++ " " ++
niceInt Nothing state fun
('\n': niceNT Nothing state
(map (\x -> (x, 'a':show x)) [1..]) funT))
(True,up)) >>>= \True ->
-}
typeDeclScc decls >>>= \decls ->
typeRhs rhs >>>= \(rhs,rhsT) ->
typeUnify (msgFun rhs) retT rhsT >>>= \_ ->
checkExist oldEnv (concat eTVar) >>>
unitS (Fun args rhs decls) -- ,funType arrow (argsT++[gdexpsT])))
typeLit :: Exp Id -> TypeMonad (Exp Id, NT)
typeLit e@(ExpLit pos (LitInteger _ _)) = --- Add fromInteger
getIdent (tInteger,TCon) >>>= \ tcon ->
getIdent (tfromInteger,Var) >>>= \ tfromInteger ->
typeIdentDict (ExpVar pos) pos tfromInteger >>>= \ (exp,expT) ->
typeUnifyApply (msgLit pos "integer") [expT,mkNTcons tcon []] >>>= \ t ->
unitS (ExpApplication pos [exp,e],t)
typeLit e@(ExpLit pos (LitRational _ _)) = --- Add fromRational
getIdent (tRational,TCon) >>>= \ tcon ->
getIdent (tfromRational,Var) >>>= \ tfromRational ->
typeIdentDict (ExpVar pos) pos tfromRational >>>= \ (exp,expT) ->
typeUnifyApply (msgLit pos "rational") [expT,mkNTcons tcon []] >>>= \ t ->
unitS (ExpApplication pos [exp,e],t)
typeLit e@(ExpLit pos (LitString _ _)) = getIdent (tString,TCon) >>>= \tcon ->
unitS (e,mkNTcons tcon [])
typeLit e@(ExpLit pos (LitInt _ _)) = getIdent (tInt,TCon) >>>= \tcon ->
unitS (e,mkNTcons tcon [])
typeLit e@(ExpLit pos (LitFloat _ _)) = getIdent (tFloat,TCon) >>>= \tcon ->
unitS (e,mkNTcons tcon [])
typeLit e@(ExpLit pos (LitDouble _ _)) = getIdent (tDouble,TCon) >>>= \tcon ->
unitS (e,mkNTcons tcon [])
typeLit e@(ExpLit pos (LitChar _ _)) = getIdent (tChar,TCon) >>>= \tcon ->
unitS (e,mkNTcons tcon [])
typeUnifyBool :: Exp id -> NT -> TypeMonad NT
typeUnifyBool g t =
getIdent (tBool,TCon) >>>= \ tcon ->
typeUnify (msgBool g) (mkNTcons tcon []) t
{-
typeGdExp :: (Exp Id, Exp Id) -> TypeMonad ((Exp Id, Exp Id), NT)
typeGdExp (g,e) =
typeExp g >>>= \(g,gT) ->
typeUnifyBool g gT >>>= \_ ->
typeExp e >>>= \(e,eT) ->
unitS ((g,e),eT)
-}
typePatGdExp (qs,e) =
mapS typeQual qs >>>= \ qs ->
typeExp e >>>= \ (e,eT) ->
unitS ((qs,e),eT)
typeRhs :: Rhs Id -> TypeMonad (Rhs Id, NT)
typeRhs (Unguarded e) = typeExp e >>>= \(e,eT) -> unitS (Unguarded e,eT)
typeRhs (PatGuard gdexps) =
mapS typePatGdExp gdexps >>>= \ gdexps ->
case unzip gdexps of
(gdexps,gdexpsT) ->
typeUnifyMany (msgPatGdExps gdexps) gdexpsT >>>= \ t ->
unitS (PatGuard gdexps,t)
typeQual (QualExp e) =
typeExp e >>>= \ (e,eT) ->
typeUnifyBool e eT >>>= \ _ ->
unitS (QualExp e)
typeQual (QualPatExp p e) =
typeExp e >>>= \ (e,eT) ->
typePat p >>>= \ (p,pT,eTVar) -> -- MW: maybe look at typeAlt for clues
typeUnify (msgPatGd p e) pT eT >>>= \ _ ->
unitS (QualPatExp p e)
typeQual (QualLet ds) =
typeDeclScc ds >>>= \ ds ->
unitS (QualLet ds)
typeAlt :: Alt Id -> TypeMonad (Alt Id, (NT, NT))
typeAlt (Alt pat13 rhs decls) =
fixPat13 pat13 >>>= \pat ->
envPat pat >>>= \patE ->
getEnv >>>= \ oldEnv ->
extendEnv patE >=>
typePat pat >>>= \ (pat,patT,eTVar) ->
typeDeclScc decls >>>= \decls ->
typeRhs rhs >>>= \(rhs,rhsT) ->
checkExist oldEnv eTVar >>>
unitS (Alt pat rhs decls,(patT,rhsT))
typeExp :: Exp Id -> TypeDown -> TypeState -> ((Exp Id,NT),TypeState)
typeExp (ExpRecord exp fields) = removeExpRecord exp fields >>>= typeExp
typeExp (ExpDo pos stmts) = removeDo stmts >>>= typeExp
typeExp (ExpCase pos exp alts) =
typeExp exp >>>= \(exp,expT) ->
mapS typeAlt alts >>>= \alts ->
case unzip alts of
(alts,altsT) ->
case unzip altsT of
(altsTP,altsTE) ->
typeUnifyMany (msgAltPats alts) altsTP >>>= \ patT ->
typeUnify (msgCase exp) expT patT >>>= \ _ ->
typeUnifyMany (msgAltExps alts) altsTE >>>= \ t ->
unitS (ExpCase pos exp alts,t)
typeExp (ExpIf pos cond exp1 exp2) =
typeExp cond >>>= \ (cond,condT) ->
typeUnifyBool cond condT >>>= \_ ->
typeExp exp1 >>>= \ (exp1,exp1T) ->
typeExp exp2 >>>= \ (exp2,exp2T) ->
typeUnify (msgIf exp1 exp2) exp1T exp2T >>>= \ t ->
unitS (ExpIf pos cond exp1 exp2,t)
typeExp (ExpApplication pos es) =
mapS typeExp es >>>= \es' ->
case unzip es' of
(es'',esT) ->
typeUnifyApply (msgApply es'') esT >>>= \ t ->
unitS (ExpApplication pos es'',t)
typeExp e@(ExpVar pos ident) =
typeIdentDict (ExpVar pos) pos ident >>>= \ (e',nt) ->
-- typeRep stuff
getState >>>= \ st ->
let def = unitS (e',nt) in
case lookupIS st ident of
Just info ->
if (tidI info) == ttypeRep then
unitS (ExpTypeRep pos nt, nt)
else
def
Nothing -> def
typeExp (ExpCon pos ident) =
typeExpCon pos ident
typeExp e@(ExpLit pos lit) =
typeLit e
typeExp (ExpList pos es) =
mapS typeExp es >>>= \es ->
case unzip es of
(es,esT) ->
typeUnifyMany (msgList es) esT >>>= \t ->
getIdent (t_List,TCon) >>>= \tcon ->
unitS (ExpList pos es,mkNTcons tcon [t])
typeExp (ExpLambda pos pats13 exp) =
-- phiMark >>>= \ mark ->
mapS fixPat13 pats13 >>>= \ pats ->
envPats pats >>>= \ patsE ->
getEnv >>>= \ oldEnv ->
extendEnv patsE >=>
mapS typePat pats >>>= \ pats ->
typeExp exp >>>= \ (exp,expT) ->
getIdent (t_Arrow,TCon) >>>= \arrow ->
case unzip3 pats of
(pats,patsT,eTVar) -> -- phiPrune2 "Lambda" patsE (funType arrow (patsT++[expT])) >>>= \ t ->
checkExist oldEnv (concat eTVar) >>>
unitS (ExpLambda pos pats exp,funType arrow (patsT++[expT]))
typeExp (ExpLet pos decls exp) =
typeDeclScc decls >>>= \decls ->
typeExp exp >>>= \(exp,expT) ->
unitS (ExpLet pos decls exp,expT)
typeExp (ExpType pos exp ctxs t) = -- Ignoring ctx and doesn't check if the
-- free variables really are free !!!
(if not (null ctxs)
then strace ("Context at " ++ strPos (getPos ctxs)
++ " in type-annotated expression is ignored :-(\n")
else id) $
typeExp exp >>>= \ (exp,expT) ->
let nt = type2NT t
free = snub (freeNT nt)
in
mapS (\ _ -> typeNewTVar) free >>>= \ free' ->
let phi = list2Subst (zip free (map (\(NTany a) -> mkNTvar a) free'))
in typeUnify (msgExpType pos) (subst phi nt) expT >>>= \ expT ->
case exp of
ExpTypeRep pos _ -> unitS (ExpTypeRep pos expT, expT)
_ -> unitS (exp,expT)
typeExp (PatWildcard pos) =
typeNewTVar >>>= \tvar ->
unitS (PatWildcard pos,tvar)
typeExp e =
getTypeErrors >>>= \errs->
error ("when typing expression at " ++ strPos (getPos e) ++ "\n"++
unlines errs) -- ++ "\n" ++ ppExp False dummyIntState e 0)
-------------------
typePat :: Pat Id -> TypeMonad (Pat Id, NT, [Id])
typePat (ExpApplication pos es) =
mapS typePat es >>>= \es ->
case unzip3 es of
(es,esT,eTVar) ->
typeUnifyApply (msgApply es) esT >>>= \ t ->
unitS (ExpApplication pos es,t,concat eTVar)
typePat e@(ExpVar pos ident) =
typeIdentDict (ExpVar pos) pos ident >>>= \ (e,t) ->
unitS (e,t,[])
typePat (ExpCon pos ident) =
typePatCon pos ident
typePat e@(ExpLit pos lit) =
typeLit e >>>= \ (e,t) ->
unitS (e,t,[])
typePat (ExpList pos es) =
mapS typePat es >>>= \es ->
case unzip3 es of
(es,esT,eTVar) ->
typeUnifyMany (msgList es) esT >>>= \t ->
getIdent (t_List,TCon) >>>= \tcon ->
unitS (ExpList pos es,mkNTcons tcon [t],concat eTVar)
typePat (ExpType pos exp ctxs t) = -- Ignoring ctx and doesn't check if the
-- free variables really are free !!!
(if not (null ctxs)
then strace ("Context at " ++ strPos (getPos ctxs)
++ " in type-annotated pattern is ignored :-(\n")
else id) $
typePat exp >>>= \ (exp,expT,eTVar) ->
let nt = type2NT t
free = snub (freeNT nt)
in
mapS (\ _ -> typeNewTVar) free >>>= \ free' ->
let phi = list2Subst (zip free (map (\(NTany a) -> mkNTvar a) free'))
in typeUnify (msgExpType pos) (subst phi nt) expT >>>= \ expT ->
unitS (exp,expT,eTVar)
typePat (PatAs pos ident pat) =
typeIdentDef (PatAs pos) pos ident >>>= \ (patas,identT) ->
typePat pat >>>= \ (pat,patT,eTVar) ->
typeUnify (msgAs pos) identT patT >>>= \ t ->
unitS (patas pat,t,eTVar)
typePat e@(PatWildcard pos) =
typeNewTVar >>>= \tvar ->
unitS (e,tvar,[])
typePat (PatIrrefutable pos pat) =
typePat pat >>>= \ (pat,patT,eTVar) ->
unitS (PatIrrefutable pos pat,patT,eTVar)
typePat (PatNplusK pos n n' k le sub) =
typeIdentDict (ExpVar pos) pos n >>>= \ (ExpVar _ n, typN) ->
typeIdentDict (ExpVar pos) pos n' >>>= \ (ExpVar _ n', typN') ->
typeExp k >>>= \ (k,typK) ->
typeExp le >>>= \ (le,typLE) ->
typeUnifyBool le typLE >>>= \ _ ->
typeExp sub >>>= \ (sub,typSUB) ->
typeUnify (msgNK pos) typK typN >>>= \ t ->
typeUnify (msgNK pos) typN' typN >>>= \ t ->
typeUnify (msgNK pos) typSUB typN >>>= \ t ->
unitS (PatNplusK pos n n' k le sub,t,[])
typePat e = error ("typePat " ++ strPos (getPos e))
-------------------
-- fixPat13 change 1.3 patterns into 1.2 patterns
-- that is, it removes record patterns.
-- No InfixList at this point!
fixDecl13 :: Decl Id -> TypeMonad (Decl Id)
fixDecl13 (DeclPat (Alt pat gdexps decls)) =
fixPat13 pat >>>= \ pat -> unitS (DeclPat (Alt pat gdexps decls))
fixDecl13 decl = unitS decl
fixPat13 :: Exp Id -> TypeMonad (Exp Id)
fixPat13 (ExpRecord exp fields) =
removeExpRecord exp fields >>>= fixPat13
fixPat13 (ExpApplication pos pats) =
unitS (ExpApplication pos) =>>> mapS fixPat13 pats
fixPat13 (ExpList pos pats) =
unitS (ExpList pos) =>>> mapS fixPat13 pats
fixPat13 (PatAs pos tid pat) =
unitS (PatAs pos tid) =>>> fixPat13 pat
fixPat13 (PatIrrefutable pos pat) =
unitS (PatIrrefutable pos) =>>> fixPat13 pat
fixPat13 pat = unitS pat
removeExpRecord :: Exp Id -> [Field Id] -> TypeMonad (Exp Id)
removeExpRecord exp fields =
getState >>>= \state ->
case translateExpRecord exp fields state of
(Right transExp,state') -> setState state' >>> unitS transExp
(Left error,state') -> setState state' >>> typeError error
|
