-- The Timber compiler -- -- Copyright 2008 Johan Nordlander -- All rights reserved. -- -- Redistribution and use in source and binary forms, with or without -- modification, are permitted provided that the following conditions -- are met: -- -- 1. Redistributions of source code must retain the above copyright -- notice, this list of conditions and the following disclaimer. -- -- 2. Redistributions in binary form must reproduce the above copyright -- notice, this list of conditions and the following disclaimer in the -- documentation and/or other materials provided with the distribution. -- -- 3. Neither the names of the copyright holder and any identified -- contributors, nor the names of their affiliations, may be used to -- endorse or promote products derived from this software without -- specific prior written permission. -- -- THIS SOFTWARE IS PROVIDED BY THE CONTRIBUTORS ``AS IS'' AND ANY EXPRESS -- OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -- WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -- DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR -- ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -- DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS -- OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) -- HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, -- STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN -- ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE -- POSSIBILITY OF SUCH DAMAGE. module Type2 where import Common import Core import Env import Decls import PP typecheck2 e2 m = t2Module e2 m t2Module (xs',ds',ws',bs') (Module v ns xs ds ws bss) = do bss <- t2BindsList env2 bss return (Module v ns xs ds ws bss) where env2 = addTEnv0 te2 (addKEnv0 ke2 env1) te2 = tenvSelsCons ds ke2 = ksigsOf ds env1 = addTEnv0 te1 (addKEnv0 ke1 env0) te1 = tsigsOf bs' ++ tenvSelsCons ds' ke1 = ksigsOf ds' env0 = addTEnv0 primPredEnv (initEnv v) t2BindsList env [] = return [] t2BindsList env (bs:bss) = do bs <- t2Binds0 env bs bss <- t2BindsList (addTEnv (tsigsOf bs) env) bss return (bs:bss) -- t2Binds0 is a variant of t2Binds that is optimized for use on the program top level, where the only free -- occurrences of unification variables are in partial type signatures. After type-checking a right-hand side, -- all unification variables that still remain will be generalized before a dependent binding group is checked. -- Thus there is no need to propagate any substitution from one top-level binding group to the next; and -- furthermore, the only fragment of a substitution that can possibly affect the type of a binding whithin -- the *same* group must have the free unification variables of the corresponding type signature as its domain. -- Hence the restriction of s1 to the tvars of sc below. Note: this optimization has considerable impact on -- the efficiency of the Type2 pass! -- Another difference between t2Binds0 and t2Binds is that t2Binds0 also applies the computed substitution to -- the top-level *term* of a binding, so that nested signatures inside the right-hand side term may be properly -- updated and named according to System F-like principles. Note that this is done as early as possible -- (immediately after a right-hand side has been checked), in order to allow the computed substitution to be -- restricted before it is applied to any sibling bindings. t2Binds0 env (Binds r te eqs) = do (s,eqs') <- t2Eqs eqs scs' <- mapM (t2Gen (tevars env)) (subst s scs) return (Binds r (xs `zip` scs') eqs') where env1 = addTEnv te env (xs,scs) = unzip te t2Eqs [] = return (nullSubst, []) t2Eqs ((x,e):eqs) = do (s1,e) <- t2ExpTscoped env1 sc e (s2,eqs) <- t2Eqs eqs return (mergeSubsts [restrict s1 (tvars sc),s2], (x, subst s1 e):eqs) where sc = lookup' te x t2Binds env (Binds r te eqs) = do (s,eqs') <- t2Eqs eqs let scs1 = subst s scs tvs0 = concat [ tvars sc | (sc,eq) <- scs1 `zip` eqs, isNewAp (snd eq) ] scs2 <- mapM (t2Gen (tevars (subst s env) ++ tvs0)) (subst s scs1) return (s, Binds r (xs `zip` scs2) eqs') where env1 = addTEnv te env (xs,scs) = unzip te t2Eqs [] = return (nullSubst, []) t2Eqs ((x,e):eqs) = do (s1,e) <- t2ExpTscoped env1 sc e (s2,eqs) <- t2Eqs eqs return (mergeSubsts [s1,s2], (x,e):eqs) where sc = lookup' te x -- Note: the program is known to be typeable at this point, thus there is no need to generalize, freshly -- instantiate, and then match an inferred type against a skolemized version of the expected type scheme -- (together with checking for escaping skolem variables). Instead, all we need to ensure is that any -- type equalities implied by the match are captured in the resulting substitution, treating all-quantified -- variables as scoped constants once we are inside the scope of a type signature (t2ExpTscoped), or using -- a freshly alpha-converted copy when matching against a polymorphic signature whose bound variables are -- not in scope (t2ExpT). -- -- Moreover, in order to enable subsequent translation into the System F-like type system of Kindle, the -- type abstraction and application points are encoded in the resulting terms as uniquely shaped let-bindings. t2ExpTscoped env sc e = do (s1,rh,e) <- t2Exp env e s2 <- mgi rh (quickSkolem sc) e <- encodeTAbs env (quant sc) e return (mergeSubsts [s1,s2], e) t2ExpT env (Scheme t qs []) e = t2ExpTscoped env (Scheme t qs []) e t2ExpT env sc e = do sc' <- ac nullSubst sc t2ExpTscoped env sc' e t2ExpTs env [] [] = return (nullSubst, []) t2ExpTs env (sc:scs) (e:es) = do (s1,e) <- t2ExpT env sc e (s2,es) <- t2ExpTs env scs es return (mergeSubsts [s1,s2], e:es) t2Exps env [] = return (nullSubst, [], []) t2Exps env (e:es) = do (s1,t,e) <- t2Exp env e (s2,ts,es) <- t2Exps env es let s = mergeSubsts [s1,s2] return (s, subst s (t:ts), e:es) t2Exp env (ELit l) = return (nullSubst, R (litType l), ELit l) t2Exp env (EVar x) = do (rh,ts) <- t2Inst (findType env x) e <- encodeTApp env ts (EVar x) return (nullSubst, rh, e) t2Exp env (ECon k) = do (rh,ts) <- t2Inst (findType env k) e <- encodeTApp env ts (ECon k) return (nullSubst, rh, e) t2Exp env (ESel e l) = do (F (sc:scs) rh,ts) <- t2Inst (findType env l) (s,e) <- t2ExpT env sc e e' <- encodeTApp env ts (ESel e l) -- NOTE: the *full* instantiation of l is remembered here, return (s, subst s (tFun scs rh), e') -- including the actual struct type arguments (C.f.: c2k.cExp) t2Exp env (ELam te e) = do (s,rh,e) <- t2Exp (addTEnv te env) e return (s, F (subst s (rng te)) rh, ELam te e) t2Exp env (EAp e es) = do (s,rh,e) <- t2Exp env e t2Ap env s rh e es t2Exp env (ELet bs e) = do (s1,bs) <- t2Binds env bs (s2,rh,e) <- t2Exp (addTEnv (subst s1 (tsigsOf bs)) env) e return (mergeSubsts [s1,s2], rh, ELet bs e) t2Exp env (ERec c eqs) = do alphas <- mapM newTVar (kArgs (findKind env c)) (t,scs) <- t2Lhs env (foldl TAp (TId c) alphas) t2Sel ls (s,es) <- t2ExpTs env scs es e <- encodeTApp env (snd (tFlat t)) (ERec c (ls `zip` es)) return (s, R (subst s t), e) where (ls,es) = unzip eqs t2Sel env x l = t2Exp env (ESel (EVar x) l) t2Exp env (ECase e alts) = do alpha <- newTVar Star (TFun [t0] t1,scs) <- t2Lhs env alpha t2Pat ps (s0,e) <- t2ExpT env (scheme t0) e (s1,es) <- t2ExpTs env scs es let s = mergeSubsts [s0,s1] return (s, R (subst s t1), ECase e (ps `zip` es)) where (ps,es) = unzip alts t2Pat env x (PLit l) = t2Exp env (EAp (EVar x) [ELit l]) t2Pat env x (PCon k) = do (rh,_) <- t2Inst (findType env k) te <- newEnv paramSym (funArgs rh) t2Exp env (eLam te (EAp (EVar x) [eAp (ECon k) (map EVar (dom te))])) t2Pat env x (PWild) = do y <- newName tempSym t <- newTVar Star t2Exp (addTEnv [(y,scheme t)] env) (EAp (EVar x) [EVar y]) t2Exp env (EReq e1 e2) = do alpha <- newTVar Star beta <- newTVar Star (s1,e1) <- t2ExpT env (scheme (tRef alpha)) e1 (s2,e2) <- t2ExpT env (scheme (tCmd alpha beta)) e2 let s = mergeSubsts [s1,s2] return (s, R (tRequest (subst s beta)), EReq e1 e2) t2Exp env (EAct e1 e2) = do alpha <- newTVar Star beta <- newTVar Star (s1,e1) <- t2ExpT env (scheme (tRef alpha)) e1 (s2,e2) <- t2ExpT env (scheme (tCmd alpha beta)) e2 let s = mergeSubsts [s1,s2] return (s, R tAction, EAct e1 e2) t2Exp env (EDo x tx c) = do (s1,t,c) <- t2Cmd (setSelf x tx env) c let s2 = case stateT env of Nothing -> nullSubst; Just t' -> unif [(t',tx)] s = mergeSubsts [s1,s2] return (s, R (subst s (tCmd tx t)), EDo x tx c) t2Exp env (ETempl x tx te c) = do (s,t,c) <- t2Cmd (setSelf x tx (addTEnv te env)) c return (s, R (tClass t), ETempl x tx te c) t2Cmd env (CRet e) = do alpha <- newTVar Star (s,e) <- t2ExpT env (scheme alpha) e return (s, subst s alpha, CRet e) t2Cmd env (CExp e) = do alpha <- newTVar Star (s,e) <- t2ExpT env (scheme (tCmd (fromJust (stateT env)) alpha)) e return (s, subst s alpha, CExp e) t2Cmd env (CGen x tx e c) = do (s1,e) <- t2ExpT env (scheme (tCmd (fromJust (stateT env)) tx)) e (s2,t,c) <- t2Cmd (addTEnv [(x,scheme tx)] env) c let s = mergeSubsts [s1,s2] return (s, subst s t, CGen x tx e c) t2Cmd env (CAss x e c) = do (s1,e) <- t2ExpT env (findType env x) e (s2,t,c) <- t2Cmd env c let s = mergeSubsts [s1,s2] return (s, subst s t, CAss x e c) t2Cmd env (CLet bs c) = do (s1,bs) <- t2Binds env bs (s2,t,c) <- t2Cmd (addTEnv (tsigsOf bs) env) c let s = mergeSubsts [s1,s2] return (s, subst s t, CLet bs c) t2Ap env s1 (F scs rh) e es = do (s2,es) <- t2ExpTs env scs es let s = mergeSubsts [s1,s2] return (s, subst s rh, EAp e es) t2Ap env s1 rh e es = do (s2,rhs,es) <- t2Exps env es t <- newTVar Star s3 <- mgi rh (F (map scheme' rhs) (R t)) let s = mergeSubsts [s1,s2,s3] return (s, R (subst s t), EAp e es) t2Lhs env alpha t2X xs = do x <- newName tempSym let env' = addTEnv [(x,scheme alpha)] env (ss,rhs,_) <- fmap unzip3 (mapM (t2X env' x) xs) let s = mergeSubsts ss scs <- mapM (t2Gen (tevars (subst s env')) . scheme') (subst s rhs) return (subst s alpha, scs) t2Gen tvs0 (Scheme rh ps ke) = do ids <- newNames tyvarSym (length tvs) let s = tvs `zip` map TId ids return (Scheme (subst s rh) ps (ke ++ ids `zip` map tvKind tvs)) where tvs = nub (filter (`notElem` tvs0) (tvars rh)) t2Inst (Scheme rh ps ke) = do ts <- mapM newTVar ks return (subst (vs `zip` ts) (tFun ps rh), ts) where (vs,ks) = unzip ke -- Skolemize a type scheme, relying on the uniqueness of all bound type variables quickSkolem (Scheme rh ps ke) = tFun ps rh mgi (R t) (R u) = return (unif [(t,u)]) mgi (F ts t) (F us u) = do s <- mgi t u ss <- mapM mgiSc (us `zip` ts) return (mergeSubsts (s:ss)) mgi (R (TFun ts t)) rh = mgi (F (map scheme ts) (R t)) rh mgi rh (R (TFun us u)) = mgi rh (F (map scheme us) (R u)) mgi (R t) (F us u) = do (t':ts) <- mapM newTVar (replicate (length us + 1) Star) let s1 = unif [(t,TFun ts t')] s2 <- mgi (R (subst s1 t)) (F us u) return (s2@@s1) mgi (F ts t) (R u) = do (u':us) <- mapM newTVar (replicate (length ts + 1) Star) let s1 = unif [(u,TFun us u')] s2 <- mgi (F ts t) (R (subst s1 u)) return (s2@@s1) mgiSc (Scheme rh [] [], Scheme rh' [] []) = mgi rh rh' mgiSc (sc, sc') = do (rh,_) <- t2Inst sc mgi rh (quickSkolem sc') unif [] = nullSubst unif ((TVar n,t):eqs) | t == TVar n = unif eqs | otherwise = let s = n +-> t; s' = unif (subst s eqs) in s' @@ s unif ((t,TVar n):eqs) = let s = n +-> t; s' = unif (subst s eqs) in s' @@ s unif ((TAp t u, TAp t' u'):eqs) = unif ((t,t'):(u,u'):eqs) unif ((TId c, TId c'):eqs) | c == c' = unif eqs unif ((TFun ts t, TFun us u):eqs) | length ts == length us = unif ((t,u) : (ts `zip` us) ++ eqs) unif eqs = internalError0 ("Type2.unif " ++ show eqs) mergeSubsts ss = unif (mapFst TVar (concat ss))