HaRe-0.6: tools/base/TC/BaseTypeCheckRec.hs
-- $Id: BaseTypeCheckRec.hs,v 1.2 2001/09/29 00:08:23 diatchki Exp $
module BaseTypeCheckRec where
import BaseSyntaxStruct
import TypeGenerics
import List(nub)
--------------------------------------------------------------------
type Type a = U a Kind T
type NGV a = [(HsName, U a Kind T)]
type Env a = [(HsName, Scheme Kind (U a Kind T))]
type Genfun a = String -> Im a Error HsName
type Alt = HsAlt HsDecl HsExp HsPat
type Stmt = HsStmt HsDecl HsExp HsPat
type EnvNew a = [Assump HsName Kind (U a Kind T)]
data GEnv a = GEnv [(HsName,Class a)] (NGV a) [Assump HsName Kind (U a Kind T)]
data Class a = Class HsName [Class a] [Inst a]
type Inst a = ([Pred (U a Kind T)], (Pred (U a Kind T)))
name (GEnv cs ngv ass) x = let Class nm sup inst = look cs x in nm
super (GEnv cs ngv ass) x = let Class nm sup inst = look cs x in sup
insts (GEnv cs ngv ass) x = let Class nm sup inst = look cs x in ass
------------------------------------------------------------------------
-- Instance declaration to make the T functor from HsSyn.hs appropriate
-- for doing type checking ala Hmx.hs
instance G T where
seqG = seqT
mapG = mapT
accG = accT
instance Name T HsName where
isName (HsTyVar s) = Just s
isName _ = Nothing
fromName s = HsTyVar s
instance Gensym a HsName where
newGensym =
do { seed <- newRef (1::Int)
; let gensym s = do { n <- readVar seed
; writeVar seed (n+1)
; return (UnQual (s ++ (show n)))
}
in return gensym
}
gensym s = do { n <- nextN
; return (UnQual (s ++ (show n)))
}
data Error
= MatchError String (Vis T) (Vis T)
| KErr String (Vis K) (Vis K)
instance TypeError Error T Kind where
hmxError s x y =
do { (nms,[x',y']) <- visible (generic []) [x,y]
; raise (MatchError s x' y')
}
-----------------------------------------------------------
type NGVars a = [(HsName,U a Kind T)]
emptyNGVars :: NGVars a
emptyNGVars = []
extendNGVars :: HsName -> U a Kind T -> NGVars a -> NGVars a
extendNGVars s t ngvars = (s,t):ngvars
generic :: NGVars a -> U a Kind T -> Im a e Bool
generic ngvars v = do { b <- occursInList v ngvars; return (not b) }
where occursInList v l =
do { (TVar v') <- prune v
; bools <- mapM (\ (a,b) -> occursIn v' b) l
; return (or bools)
}
--------- Show Instances ----------------------------------
instance Show(U a k T) where
showsPrec n (S x) = shows x
showsPrec n (TGen m) = showString "%" . shows m
showsPrec n (TVar _) = showString "?"
instance Show(Vis T) where
showsPrec n (VN a) = showString a
showsPrec n (VS x) = shows x
instance Show a => Show(Pred a) where
show (IsIn n ts) = "(" ++ n ++ " " ++ (show ts) ++ ")"
instance Show a => Show (Scheme Kind a) where
show (Sch x p t) = "(all " ++ (show x) ++"." ++ (show p) ++ " => " ++ (show t) ++ ")"
----------------------- Instantiate unification ------------------------------
unifyShape unify ( x @ (S tx)) (y @ (S ty)) =
case (tx,ty) of
(HsTyFun x1 x2,HsTyFun y1 y2) ->
do { xs <- unify x1 y1
; ys <- unify x2 y2
; return (xs++ys) }
(HsTyTuple xs,HsTyTuple ys) ->
if (length xs) == (length ys)
then do { xss <- mapM (uncurry unify) (zip xs ys)
; return (concat xss)
}
else hmxError "TupleLengthMatch" x y
(HsTyApp x1 x2,HsTyApp y1 y2) ->
do { xs <- unify x1 y1
; ys <- unify x2 y2
; return (xs++ys) }
(HsTyVar n1,HsTyVar n2) ->
if n1 == n2
then return []
else hmxError "NameMatch" x y
(HsTyCon n1,HsTyCon n2) ->
if n1 == n2
then return []
else hmxError "NameMatch" x y
(tx,ty) -> hmxError "ShapeMatch" x y
unify :: (U a Kind T) -> (U a Kind T) -> Im a Error [p]
unify = unifier (hmxError "OccursCheck") unifyShape
------------------ Kind inference -----------------------
data Sort = Sort
type Knd a = U a Sort K
instance G K where
mapG = mapK
seqG = seqK
accG f = flip (accK f)
instance TypeError Error K Sort where
hmxError s x y =
do { (nms,[x',y']) <- visible (\ x -> return False) [x,y]
; raise (KErr s x' y')
}
unifyK unify ( x @ (S tx)) (y @ (S ty)) =
case (tx,ty) of
(Kstar,Kstar) -> return []
(Kfun x1 x2,Kfun y1 y2) ->
do { xs <- unify x1 y1
; ys <- unify x2 y2
; return (xs++ys) }
(tx,ty) -> hmxError "KindShapeMatch" x y
unifyKind :: (U a Sort K) -> (U a Sort K) -> Im a Error [p]
unifyKind = unifier (hmxError "OccursCheck") unifyK
star = S Kstar
inferK :: (HsName -> U a Sort K) -> U a Sort K -> HsType -> Im a Error (U a Sort K)
inferK env hint (Typ typ) =
case typ of
(HsTyFun x y) ->
do { x' <- inferK env star x
; y' <- inferK env star y
; unifyKind hint star
; return hint
}
(HsTyTuple ts) ->
do { sequence (map (inferK env star) ts)
; unifyKind hint star
; return star
}
(HsTyApp x y) ->
do { a <- newVar Sort
; b <- newVar Sort
; x' <- inferK env (S(Kfun a hint)) x
; y' <- inferK env a y
; return hint
}
(HsTyVar nm) ->
do { unifyKind hint (env nm)
; return hint
}
(HsTyCon nm) ->
do { unifyKind hint (env nm)
; return hint
}
kindOf :: (HsName -> U a Sort K) -> HsType -> Im a Error Kind
kindOf envf x = do { hint <- newVar Sort
; inferK envf hint x
; k <- uaSortK_to_Kind hint
; return k
}
----------------------------------------------------------------------------
-- After Kind inference some of the Kind Vars may still be un-instantiated
-- Since we do not have a "polymorphic" Kind system we must instantiate
-- these Kind vars. We fix them to kind "Knd Kstar", and then turn the
-- resulting (U a Sort K) thing into a "Kind" type.
uaSortK_to_Kind :: (U a Sort K) -> Im a e Kind
uaSortK_to_Kind (S x) = do { x' <- seqG(mapG uaSortK_to_Kind x); return (Knd x')}
uaSortK_to_Kind (TGen m) = error "no TGen in kinds"
uaSortK_to_Kind (t @ (TVar x)) = follow finish uaSortK_to_Kind t
where finish :: (Tyvar a Sort K) -> Im a e Kind
finish (Tyvar ref s) = do { writeVar ref (Just star)
; return (Knd Kstar) }
--------------- Environment function and types --------------------------
extend f s t = (s,t) : f
lambdaExt :: [(name,Scheme a c)] -> name -> c -> [(name,Scheme a c)]
lambdaExt env vname vtyp = extend env vname (Sch [] [] vtyp)
envf [] s = error ("variable not found: "++(show s)++"\n")
envf ((x,t):m) s = if x==s then t else envf m s
-------- Type constructors and types of literal constants ------------
tArrow x y = S(HsTyFun x y)
tTuple ts = S(HsTyTuple ts)
tInteger = S(HsTyCon (UnQual "Integer"))
tChar = S(HsTyCon (UnQual "Char"))
tString = tlist tChar
tRational = S(HsTyCon (UnQual "Rational"))
tBool = S(HsTyCon (UnQual "Bool"))
tStringHash = S(HsTyCon (UnQual "stringHash"))
tCharHash = S(HsTyCon (UnQual "CharHash"))
tIntHash = S(HsTyCon (UnQual "IntHash"))
tRationalHash = S(HsTyCon (UnQual "RationalHash"))
tlist x = S(HsTyApp tlistCon x)
tlistCon = (S(HsTyCon (UnQual "[]")))
tcode x = S(HsTyApp tcodeCon x)
tcodeCon = (S(HsTyCon (UnQual "Code")))
litTyp (HsInt _) = tInteger
litTyp (HsChar _) = tChar
litTyp (HsString _) = tString
litTyp (HsFrac _) = tRational
litTyp (HsCharPrim _) = tCharHash
litTyp (HsStringPrim _) = tStringHash
litTyp (HsIntPrim _) = tIntHash
litTyp (HsFloatPrim _) = tRationalHash
litTyp (HsDoublePrim _) = tRationalHash
------------------------ Predefined Class predicates ----------------
num x = IsIn "Num" [x]
monad x = IsIn "Monad" [x]
enum x = IsIn "Enum" [x]
-------------------------------------------------------------------------
-- unArrow [p1,p2,p3] (t1 -> t2 -> t3 -> t4) ---> (t4,[(p1,t1),(p2,t2),(p3,t3)])
unArrow :: [HsPat] -> Type a -> Im a Error (Type a,[(HsPat,Type a)])
unArrow ps t = do { t' <- col t; flat ps t' }
where flat (p:ps) (S(HsTyFun dom rng)) =
do { (t,ts) <- (flat ps rng) ; return (t,(p,dom) : ts) }
flat [] t = return (t,[])
flat (p:ps) t = error "Too many arguments to pattern"
patExtTup [] env = return ([],[],[])
patExtTup ((p,t):m) env =
do { (t1,e1,c1) <- patExt p t env
; (ts,e2,cs) <- patExtTup m env
; return(t1:ts,e1++e2,c1 ++ cs)
}
patExtList [] elemtyp env cs = return (tlist elemtyp,[],cs)
patExtList (p:m) elemtyp env cs =
do { (t1,e1,c1) <- patExt p elemtyp env
; (listOfelem,e2,cs) <- patExtList m elemtyp env c1
; return(listOfelem,e1 ++ e2,c1++cs)
}
patExt :: HsPat -> Type a -> Env a -> Im a Error (Type a,NGV a,[Pred (Type a)])
patExt (Pat p) typ env =
case p of
(HsPVar name) -> return (typ,[(name,typ)],[])
(HsPLit l) ->
do { let t = litTyp l
; cs <- unify t typ
; return (t,[],cs)
}
(HsPNeg x) -> error "whats this?"
(HsPInfixApp x n y) -> patExt (Pat(HsPApp n [x,y])) typ env
(HsPApp nm ps) ->
do { (cs1 :=> ctyp) <- instan (envf env nm)
; (t,patTypeList) <- unArrow ps ctyp
; cs2 <- unify t typ
; (ts2,env2,cs3) <- patExtTup patTypeList env
; return (t,env2,cs1 ++ cs2 ++ cs3)
}
(HsPTuple ps) ->
do { ts <- sequence (map (\ x -> (newVar kstar)) ps)
; cs2 <- unify (tTuple ts) typ
; (ts,ngv3,cs3) <- patExtTup (zip ps ts) env
; return (tTuple ts,ngv3,cs2 ++ cs3)
}
(HsPList ps ) ->
do { elemtyp <- newVar kstar
; (listtyp,ngv2,cs) <- patExtList ps elemtyp env []
; cs2 <- unify listtyp (tlist elemtyp)
; return (listtyp,ngv2,cs ++ cs2)
}
(HsPParen x) -> patExt x typ env
(HsPRec n pairs) -> error "not yet"
(HsPRecUpdate nm pairs) -> error "not yet"
(HsPAsPat name x) ->
do { (t,ngv1,cs1) <- patExt x typ env
; return (t,(name,t):ngv1,cs1)
}
(HsPWildCard) -> do { t <- newVar kstar ; return (t,[],[]) }
(HsPIrrPat x) -> patExt x typ env
inferPats :: [HsPat] -> NGV a -> Env a ->
Im a Error ([Type a],NGV a,Env a,[Pred (Type a)])
inferPats ps ngvars env =
do { pairs <- sequence (map (\ p -> do { t <- newVar kstar; return (p,t) }) ps)
; (t1,ngv1,cs1) <- patExtTup pairs env
; return (t1,ngv1 ++ ngvars,g ngv1 env,cs1)
} where g [] env = env
g ((v,t):more) env = lambdaExt (g more env) v t
inferPat p ngvars env hint =
do { (_,ngv1,cs1) <- patExt p hint env
; return (ngv1 ++ ngvars,g ngv1 env,cs1)
} where g [] env = env
g ((v,t):more) env = lambdaExt (g more env) v t
-------------------------------------------------------------
infer :: Genfun a -> NGV a -> Env a -> Type a ->
HsExp -> Im a Error (Type a,[Pred (Type a)])
infer gensym ngvars env hint (exp @ (Exp e)) =
let check env hint x = infer gensym ngvars env hint x
in
case e of
HsVar nm ->
do { (cs :=> t) <- instan (envf env nm)
; cs2 <- unify t hint
; return (t,cs ++ cs2)
}
HsCon nm ->
do { (cs :=> t) <- instan (envf env nm)
; cs2 <- unify t hint
; return (t,cs++cs2)
}
HsLit n ->
do { let t = litTyp n
; cs <- unify t hint
; return (t,cs)
}
HsInfixApp x f y -> check env hint (Exp(HsApp (Exp (HsApp f x)) y))
HsApp f x ->
do { xtyp <- newVar kstar
; let ftyp = tArrow xtyp hint
; (_,cs2) <- check env xtyp x
; (_,cs3) <- check env ftyp f
; return (hint,cs2++cs3)
}
HsNegApp x ->
do { (t,cs) <- check env hint x
; return (t,num t : cs)
}
HsLambda ps x ->
do { (ptyps,ngv2,env2,cs) <- inferPats ps ngvars env
; result <- newVar kstar
-- f [t1,t2,t3] r --> (t1 -> t2 -> t3 -> r)
; let f [] rng = rng
f (t:ts) rng = tArrow t (f ts rng)
; (_,cs2) <- infer gensym ngv2 env2 result x
; return (f ptyps result,cs ++ cs2)
}
HsLet ds e ->
do { (ngv2,env2,cs2) <- inferDecls gensym ngvars env ds
; infer gensym ngv2 env2 hint e
}
HsIf x y z ->
do { t <- newVar kstar
; (_,cs1) <- check env tBool x
; (_,cs2) <- check env t y
; (_,cs3) <- check env t z
; return (t,cs1 ++ cs2 ++ cs3)
}
HsCase e alts ->
do { argtyp <- newVar kstar
; (ptyp,cs1) <- check env argtyp e
; csAll <- mapM (inferAlt gensym ngvars env ptyp hint) alts
; return (hint, cs1 ++ concat csAll)
}
HsDo stmt ->
do { mtyp <- newVar (karrow kstar kstar)
; let m x = (S(HsTyApp mtyp x))
; a <- newVar kstar
; cs2 <- unify hint (m a)
; cs3 <- inferStmt gensym ngvars env mtyp (m a) False stmt
; return (hint,(monad mtyp) : cs2 ++ cs3)
}
HsTuple xs ->
do { pairs <- sequence (map (\ x -> do { t <- newVar kstar; return (t,x) }) xs)
; let tupletyp = tTuple(map fst pairs)
; cs1 <- unify hint tupletyp
; ts <- mapM (uncurry (check env)) pairs
; return (hint,foldr (\ (t,c) cs -> c ++ cs) cs1 ts)
}
HsList xs ->
do { elemtyp <- newVar kstar
; cs1 <- unify hint (tlist elemtyp)
; pairs <- mapM (check env elemtyp) xs
; return (hint,foldr (\ (t,c) cs -> c ++ cs) cs1 pairs)
}
HsParen x -> check env hint x
HsRightSection oper arg -> -- i.e. (+ 3) }
do { ltyp <- newVar kstar
; rtyp <- newVar kstar
; anstyp <- newVar kstar
; cs1 <- unify (tArrow ltyp anstyp) hint
; (_,cs2) <- check env (tArrow ltyp (tArrow rtyp anstyp)) oper
; (_,cs3) <- check env rtyp arg
; return (hint,cs1 ++ cs2 ++ cs3)
}
HsLeftSection arg oper -> -- i.e. (3 +)
do { ltyp <- newVar kstar
; rtyp <- newVar kstar
; anstyp <- newVar kstar
; cs1 <- unify (tArrow rtyp anstyp) hint
; (_,cs2) <- check env (tArrow ltyp (tArrow rtyp anstyp)) oper
; (_,cs3) <- check env ltyp arg
; return (hint,cs1 ++ cs2 ++ cs3)
}
HsRecConstr name fields -> error "not yet"
HsRecUpdate arg fields -> error "not yet"
HsEnumFrom x -> -- [x ..] :: Enum a => [a]
do { a <- newVar kstar
; cs1 <- unify hint (tlist a)
; (_,cs2) <- check env a x
; return (hint,(enum a) : cs1 ++ cs2)
}
HsEnumFromTo x y -> -- [x .. y] :: Enum a => a -> a -> [a]
do { a <- newVar kstar
; cs0 <- unify hint (tlist a)
; (_,cs1) <- check env a x
; (_,cs2) <- check env a y
; return (hint,(enum a) : cs0 ++ cs1 ++ cs2)
}
HsEnumFromThen x y -> -- [x, y ..] : Enum a => a -> a -> [a]
do { a <- newVar kstar
; cs0 <- unify hint (tlist a)
; (_,cs1) <- check env a x
; (_,cs2) <- check env a y
; return (hint,(enum a) : cs0 ++ cs1 ++ cs2)
}
HsEnumFromThenTo x y z -> -- [x,y .. z] :: Enum a => a -> a -> a -> [a]
do { a <- newVar kstar
; cs0 <- unify hint (tlist a)
; (_,cs1) <- check env a x
; (_,cs2) <- check env a y
; (_,cs3) <- check env a z
; return (hint,(enum a) : cs0 ++ cs1 ++ cs2 ++ cs3)
}
HsListComp stmt ->
do { let mtyp = tlistCon
; let m x = (S(HsTyApp mtyp x))
; a <- newVar kstar
; cs2 <- unify hint (m a)
; cs3 <- inferStmt gensym ngvars env mtyp a True stmt
; return (hint,cs2 ++ cs3)
}
HsExpTypeSig loc e qt ->
do { s <- hsQual2Sch qt
; (cs1 :=> typ) <- instan s
; cs2 <- unify typ hint
; (_,cs3) <- check env typ e
; return (typ,cs1 ++ cs2 ++ cs3)
}
HsAsPat nm e -> error "pattern only"
HsWildCard -> error "pattern only"
HsIrrPat e -> error "pattern only"
HsMetaBracket e -> -- MetaHUGS extension <| exp |>
do { a <- newVar kstar
; cs1 <- unify hint (tcode a)
; (_,cs2) <- check env a e
; return (hint,cs1 ++ cs2)
}
HsMetaEscape e -> -- MetaHUGS extansion ^exp
do { (_,cs1) <- check env (tcode hint) e
; return (hint,cs1)
}
----------------------------------------------------------------------------------
-- inferStmt is used to infer the type of both Do stmts and list comprehensions
-- [ A | p <- e ; f ] has the same structure as (do { P <- e; f ; A })
-- but the type rules differ slightly for both "A" and "f". We've parameterized
-- inferStmt to handle this
inferStmt :: Genfun a -> NGV a -> Env a -> Type a -> Type a -> Bool ->
Stmt -> Im a Error [Pred (Type a)]
inferStmt gensym ngvars env mtyp lasttyp isListComp stmt =
let m x = (S(HsTyApp mtyp x)) in
case stmt of
HsGenerator p e next -> -- p <- e ; next
do { ptyp <- newVar kstar
; (_,cs2) <- infer gensym ngvars env (m ptyp) e
; (ngv2,env2,cs3) <- inferPat p ngvars env ptyp
; cs4 <- inferStmt gensym ngv2 env2 mtyp lasttyp isListComp next
; return (cs2 ++ cs3 ++ cs4)
}
HsQualifier e next -> -- e ; next
do { typ <- if isListComp then return tBool else fmap m (newVar kstar)
; (_,cs2) <- infer gensym ngvars env typ e
; return cs2
}
HsLetStmt ds next -> -- let ds ; next
do { (ngv2,env2,cs2) <- inferDecls gensym ngvars env ds
; cs3 <- inferStmt gensym ngv2 env2 mtyp lasttyp isListComp next
; return (cs2 ++ cs3)
}
HsLast e -> do { (_,cs) <- infer gensym ngvars env lasttyp e; return cs }
inferAlt :: Genfun a -> NGV a -> Env a -> Type a -> Type a ->
Alt -> Im a Error [Pred (Type a)]
inferAlt gensym ngvars env pathint bodyhint (HsAlt s p rhs ds) =
do { (ngv2,env2,cs2) <- inferPat p ngvars env pathint
; (ngv3,env3,cs3) <- inferDecls gensym ngv2 env2 ds
; (_,cs4) <-
case rhs of
(HsBody e) -> infer gensym ngv3 env3 bodyhint e
(HsGuard ms) -> g ms
where g [] = return (bodyhint,[])
g ((s,guard,e):ws) =
do { (_,cs4) <- infer gensym ngv3 env3 tBool guard
; (t,cs5) <- infer gensym ngv3 env3 bodyhint e
; (_,cs6) <- g ws
; return (t,cs4 ++ cs5 ++ cs6)
}
; return (cs2 ++ cs3 ++ cs4)
}
inferDecls :: Genfun a -> NGV a -> Env a ->
[HsDecl] -> Im a Error (NGV a,Env a,[Pred (Type a)])
inferDecls gensym ngvars env ds = return (ngvars,env,[])
---------------------------------------------------------------------
-- The Parser produces HsQualType data structures, we must turn these
-- into Scheme data structures, while doing to we should kind-check
-- all the type information.
hsQual2Sch (HsQualType preds x) = scheme preds x
hsQual2Sch (HsUnQualType t) = scheme [] t
scheme :: [(HsName,HsName)] -> HsType -> Im a Error (Scheme Kind (U a Kind T))
scheme preds t =
do { newks <- sequence(map (const (newVar Sort)) names)
-- A new Kind var for each of the free type variables in "t"
; let env = zip names newks -- Map each Type Var to its kind Var
; mainK <- kindOf (look env) t
; argKs <- sequence (map uaSortK_to_Kind newks)
; return (Sch argKs (map transPred preds) (trans sub t))
}
where names = namesT t -- All the free Type Variables in "t"
sub = zipWith (\ t n -> (t,TGen n)) names [0..]
trans sub (Typ (HsTyVar nm)) = look sub nm
trans sub (Typ z) = (S(mapT (trans sub) z))
transPred (cla,arg) = IsIn (show cla) [trans sub (Typ(HsTyVar arg))]