{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-} -- The Timber compiler -- -- Copyright 2008-2009 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 <- t2TopBinds 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) -- Note 1: During type-checking of a top-level right-hand side, all unification variables found 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 t2TopBinds env [] = return [] t2TopBinds env (bs:bss) = do (_,bs) <- t2Binds env bs bss <- t2TopBinds (addTEnv (tsigsOf bs) env) bss return (bs:bss) -- Note 2: 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 (see encodeTAbs and encodeTApp defined in Core). t2Binds env (Binds r te eqs) = do (s0,eqs') <- t2Eqs eqs let mono = [ t | (x,e) <- eqs, let t = lookup' te x, monoRestrict r t e ] tvs0 = tevars (subst s0 env) ++ tvars (subst s0 mono) quants <- mapM (t2Quant tvs0) (subst s0 te) let env2 = addTEnv te' env te' = [ (x,t) | (x,(t,_,_)) <- quants ] ss = [ (x,s) | (x,(_,s,_)) <- quants ] s1 = [ (x,e) | (x,(_,_,e)) <- quants, e /= EVar x ] eqs'' <- mapM (t2Gen env2 s0 ss s1) eqs' return (s0, Binds r te' eqs'') where env1 = addTEnv te env 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 t2Quant tvs0 (x,t) = do ids <- newNames tyvarSym (length tvs) let ts = map TId ids s = tvs `zip` ts ke' = ke ++ ids `zip` map tvKind tvs e <- encodeTApp ts (EVar x) return (x, (Scheme (subst s rh) (subst s ps) ke', s, e)) where tvs = nub (filter (`notElem` tvs0) (tvars rh)) Scheme rh ps ke = t t2Gen env s ss s1 (x,e) = do e' <- encodeTAbs ke (subst s1 (subst s0 e)) return (x, e') where s0 = mergeSubsts [lookup' ss x, s] ke = quant (findType env x) -- Note 3: 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. t2ExpTscoped env sc e = do (s1,rh,e') <- t2Exp env e s2 <- mgi rh (quickSkolem sc) return (mergeSubsts [s1,s2], e') t2ExpT env (Scheme t qs []) e = t2ExpTscoped env (Scheme t qs []) e t2ExpT env sc e = do (s,e) <- t2ExpTscoped env sc e e <- encodeTAbs (quant sc) e return (s, 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 ts (EVar x) return (nullSubst, rh, e) t2Exp env (ECon k) = do (rh,ts) <- t2Inst (findType env k) e <- encodeTApp 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 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 (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'))) (subst s rhs) return (subst s alpha, scs) where t2Gen tvs0 rh = do ids <- newNames tyvarSym (length tvs) let s = tvs `zip` map TId ids return (Scheme (subst s rh) [] (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\n" ++ render (nest 4 (vpr eqs))) mergeSubsts ss = unif (mapFst TVar (concat ss))