--==========================================================-- --=== A type-checker -- v5 File: TypeCheck5.m (1) ===-- --=== Corrected version for 0.210a ===-- --==========================================================-- module TypeCheck5 where import BaseDefs import Utils import MyUtils --==========================================================-- --=== Formatting of results ===-- --==========================================================-- tcMapAnnExpr :: (a -> b) -> AnnExpr c a -> AnnExpr c b tcMapAnnExpr f (ann, node) = (f ann, mapAnnExpr' node) where mapAnnExpr' (AVar v) = AVar v mapAnnExpr' (ANum n) = ANum n mapAnnExpr' (AConstr c) = AConstr c mapAnnExpr' (AAp ae1 ae2) = AAp (tcMapAnnExpr f ae1) (tcMapAnnExpr f ae2) mapAnnExpr' (ALet recFlag annDefs mainExpr) = ALet recFlag (map mapAnnDefn annDefs) (tcMapAnnExpr f mainExpr) mapAnnExpr' (ACase switchExpr annAlts) = ACase (tcMapAnnExpr f switchExpr) (map mapAnnAlt annAlts) mapAnnExpr' (ALam vs e) = ALam vs (tcMapAnnExpr f e) mapAnnDefn (naam, expr) = (naam, tcMapAnnExpr f expr) mapAnnAlt (naam, (pars, resExpr)) = (naam, (pars, tcMapAnnExpr f resExpr)) --======================================================-- -- tcSubstAnnTree :: Subst -> AnnExpr Naam TExpr -> AnnExpr Naam TExpr tcSubstAnnTree phi tree = tcMapAnnExpr (tcSub_type phi) tree --======================================================-- -- tcTreeToEnv :: AnnExpr Naam TExpr -> TypeEnv tcTreeToEnv tree = t2e tree where t2e (nodeType, node) = t2e' node t2e' (AVar v) = [] t2e' (ANum n) = [] t2e' (AConstr c) = [] t2e' (AAp ae1 ae2) = (t2e ae1) ++ (t2e ae2) t2e' (ALam cs e) = t2e e t2e' (ALet rf dl me) = (concat (map aFN dl)) ++ (t2e me) t2e' (ACase sw alts) = (t2e sw) ++ (concat (map (t2e.second.second) alts)) aFN (naam, (tijp, body)) = (naam, tijp):(t2e' body) --======================================================-- -- tcShowtExpr :: TExpr -> [Char] tcShowtExpr t = pretty' False t where pretty' b (TVar tvname) = [' ', chr (96+(lookup tvname tvdict))] pretty' b (TCons "int" []) = " int" pretty' b (TCons "bool" []) = " bool" pretty' b (TCons "char" []) = " char" pretty' True (TArr t1 t2) = " (" ++ (pretty' True t1) ++ " -> " ++ (pretty' False t2) ++ ")" pretty' False (TArr t1 t2) = (pretty' True t1) ++ " -> " ++ (pretty' False t2) pretty' b (TCons notArrow cl) = " (" ++ notArrow ++ concat (map (pretty' True) cl) ++ ")" lookup tvname [] = panic "tcShowtExpr: Type name lookup failed" lookup tvname (t:ts) | t==tvname = 1 | otherwise = 1 + (lookup tvname ts) tvdict = nub (tvdict' t) tvdict' (TVar t) = [t] tvdict' (TCons c ts) = concat (map tvdict' ts) tvdict' (TArr t1 t2) = tvdict' t1 ++ tvdict' t2 --======================================================-- -- tcPretty :: (Naam, TExpr) -> [Char] tcPretty (naam, tipe) = "\n " ++ (ljustify 25 (naam ++ " :: ")) ++ (tcShowtExpr tipe) --======================================================-- tcCheck :: TcTypeEnv -> TypeNameSupply -> AtomicProgram -> ([Char], Reply (AnnExpr Naam TExpr, TypeEnv) Message) tcCheck baseTypes ns (tdefs, expr) = if good tcResult then (fullEnvWords, Ok (rootTree, fullEnv)) else ("", Fail "No type") where tcResult = tc (tdefs++builtInTypes) (baseTypes++finalConstrTypes) finalNs expr good (Ok x) = True good (Fail x2) = False (rootSubst, rootType, annoTree) = f tcResult where f (Ok x) = x rootTree = tcSubstAnnTree rootSubst annoTree rootEnv = tcTreeToEnv rootTree fullEnv = rootEnv ++ map f finalConstrTypes where f (naam, (Scheme vs t)) = (naam, t) fullEnvWords = concat (map tcPretty fullEnv) (finalNs, constrTypes) = mapAccuml tcConstrTypeSchemes ns (tdefs++builtInTypes) finalConstrTypes = concat constrTypes builtInTypes = [ ("bool", [], [("True", []), ("False", [])]) ] --==========================================================-- --=== 9.2 Representation of type expressions ===-- --==========================================================-- ----======================================================-- --tcArrow :: TExpr -> -- TExpr -> -- TExpr -- --tcArrow t1 t2 = TArr t1 t2 --======================================================-- tcInt :: TExpr tcInt = TCons "int" [] --======================================================-- tcBool :: TExpr tcBool = TCons "bool" [] --======================================================-- tcTvars_in :: TExpr -> [TVName] tcTvars_in t = tvars_in' t [] where tvars_in' (TVar x) l = x:l tvars_in' (TCons y ts) l = foldr tvars_in' l ts tvars_in' (TArr t1 t2) l = tvars_in' t1 (tvars_in' t2 l) --==========================================================-- --=== 9.41 Substitutions ===-- --==========================================================-- --======================================================-- tcApply_sub :: Subst -> TVName -> TExpr tcApply_sub phi tvn = if TVar tvn == lookUpResult then TVar tvn else tcSub_type phi lookUpResult where lookUpResult = utLookupDef phi tvn (TVar tvn) --======================================================-- tcSub_type :: Subst -> TExpr -> TExpr tcSub_type phi (TVar tvn) = tcApply_sub phi tvn tcSub_type phi (TCons tcn ts) = TCons tcn (map (tcSub_type phi) ts) tcSub_type phi (TArr t1 t2) = TArr (tcSub_type phi t1) (tcSub_type phi t2) --======================================================-- tcScomp :: Subst -> Subst -> Subst tcScomp sub2 sub1 = sub1 ++ sub2 --======================================================-- tcId_subst :: Subst tcId_subst = [] --======================================================-- tcDelta :: TVName -> TExpr -> Subst -- all TVar -> TVar substitutions lead downhill tcDelta tvn (TVar tvn2) | tvn == tvn2 = [] | tvn > tvn2 = [(tvn, TVar tvn2)] | tvn < tvn2 = [(tvn2, TVar tvn)] tcDelta tvn non_var_texpr = [(tvn, non_var_texpr)] --==========================================================-- --=== 9.42 Unification ===-- --==========================================================-- --======================================================-- tcExtend :: Subst -> TVName -> TExpr -> Reply Subst Message tcExtend phi tvn t | t == TVar tvn = Ok phi | tvn `notElem` (tcTvars_in t) = Ok ((tcDelta tvn t) `tcScomp` phi) | otherwise = fail ( "Type error in source program:\n\n" ++ "Circular substitution:\n " ++ tcShowtExpr (TVar tvn) ++ "\n going to\n" ++ " " ++ tcShowtExpr t ++ "\n") --======================================================-- tcUnify :: Subst -> (TExpr, TExpr) -> Reply Subst Message tcUnify phi (TVar tvn, t) = if phitvn == TVar tvn then tcExtend phi tvn phit else tcUnify phi (phitvn, phit) where phitvn = tcApply_sub phi tvn phit = tcSub_type phi t tcUnify phi (p@(TCons _ _), q@(TVar _)) = tcUnify phi (q, p) tcUnify phi (p@(TArr _ _), q@(TVar _)) = tcUnify phi (q, p) tcUnify phi (TArr t1 t2, TArr t1' t2') = tcUnifyl phi [(t1, t1'), (t2, t2')] tcUnify phi (TCons tcn ts, TCons tcn' ts') | tcn == tcn' = tcUnifyl phi (ts `zip` ts') tcUnify phi (t1, t2) = fail ( "Type error in source program:\n\n" ++ "Cannot unify\n " ++ tcShowtExpr t1 ++ "\n with\n " ++ tcShowtExpr t2 ++ "\n" ) --======================================================-- tcUnifyl :: Subst -> [(TExpr, TExpr)] -> Reply Subst Message tcUnifyl phi eqns = foldr unify' (Ok phi) eqns where unify' eqn (Ok phi) = tcUnify phi eqn unify' eqn (Fail m) = Fail m --==========================================================-- --=== 9.42.2 Merging of substitutions ===-- --==========================================================-- --======================================================-- tcMergeSubs :: Subst -> Subst tcMergeSubs phi = if newBinds == [] then unifiedOlds else tcMergeSubs (unifiedOlds ++ newBinds) where (newBinds, unifiedOlds) = tcMergeSubsMain phi --======================================================-- tcMergeSubsMain :: Subst -> (Subst, Subst) -- pair of new binds, unified olds tcMergeSubsMain phi = (concat newUnifiersChecked, zip oldVars (tcOldUnified newUnifiersChecked oldGroups)) where oldVars = nub (utDomain phi) oldGroups = map (utLookupAll phi) oldVars newUnifiers = map (tcUnifySet tcId_subst) oldGroups newUnifiersChecked = map tcCheckUnifier newUnifiers --======================================================-- tcCheckUnifier :: Reply Subst Message -> Subst tcCheckUnifier (Ok r) = r tcCheckUnifier (Fail m) = panic ("tcCheckUnifier: " ++ m) --======================================================-- tcOldUnified :: [Subst] -> [[TExpr]] -> [TExpr] tcOldUnified [] [] = [] tcOldUnified (u:us) (og:ogs) = (tcSub_type u (head og)): tcOldUnified us ogs --==========================================================-- --=== 9.5 Keeping track of types ===-- --==========================================================-- --======================================================-- tcUnknowns_scheme :: TypeScheme -> [TVName] tcUnknowns_scheme (Scheme scvs t) = tcTvars_in t `tcBar` scvs --======================================================-- tcBar :: (Eq a) => [a] -> [a] -> [a] tcBar xs ys = [ x | x <- xs, not (x `elem` ys)] --======================================================-- tcSub_scheme :: Subst -> TypeScheme -> TypeScheme tcSub_scheme phi (Scheme scvs t) = Scheme scvs (tcSub_type (tcExclude phi scvs) t) where tcExclude phi scvs = [(n,e) | (n,e) <- phi, not (n `elem` scvs)] --==========================================================-- --=== 9.53 Association lists ===-- --==========================================================-- --======================================================-- tcCharVal :: AList Naam b -> Naam -> b tcCharVal al k = utLookupDef al k (panic ("tcCharVal: no such variable: " ++ k)) --======================================================-- tcUnknowns_te :: TcTypeEnv -> [TVName] tcUnknowns_te gamma = concat (map tcUnknowns_scheme (utRange gamma)) --======================================================-- tcSub_te :: Subst -> TcTypeEnv -> TcTypeEnv tcSub_te phi gamma = [(x, tcSub_scheme phi st) | (x, st) <- gamma] --==========================================================-- --=== 9.6 New variables ===-- --==========================================================-- --======================================================-- tcNext_name :: TypeNameSupply -> TVName tcNext_name ns@(f, s) = ns --======================================================-- tcDeplete :: TypeNameSupply -> TypeNameSupply tcDeplete (f, s) = (f, tcNSSucc s) --======================================================-- tcSplit :: TypeNameSupply -> (TypeNameSupply, TypeNameSupply) tcSplit (f, s) = ((f2, [0]), (tcNSSucc f2, [0])) where f2 = tcNSDouble f --======================================================-- tcName_sequence :: TypeNameSupply -> [TVName] tcName_sequence ns = tcNext_name ns: tcName_sequence (tcDeplete ns) --======================================================-- tcNSSucc :: [Int] -> [Int] tcNSSucc [] = [1] tcNSSucc (n:ns) | n < tcNSslimit = n+1: ns | otherwise = 0: tcNSSucc ns --======================================================-- tcNSDouble :: [Int] -> [Int] tcNSDouble [] = [] tcNSDouble (n:ns) = 2*n': ns' where n' | n > tcNSdlimit = n - tcNSdlimit | otherwise = n ns' | n' == n = tcNSDouble ns | otherwise = tcNSSucc (tcNSDouble ns) tcNSdlimit :: Int tcNSdlimit = 2^30 tcNSslimit :: Int tcNSslimit = tcNSdlimit + (tcNSdlimit - 1) --==========================================================-- --=== 9.7 The type-checker ===-- --==========================================================-- --======================================================-- tc :: [TypeDef] -> TcTypeEnv -> TypeNameSupply -> CExpr -> Reply TypeInfo Message tc tds gamma ns (ENum n) = Ok (tcId_subst, TCons "int" [], (TCons "int" [], ANum n)) tc tds gamma ns (EVar x) = tcvar tds gamma ns x tc tds gamma ns (EConstr c) = tcvar tds gamma ns c tc tds gamma ns (EAp e1 e2) = tcap tds gamma ns e1 e2 tc tds gamma ns (ELam [] e) = tc tds gamma ns e tc tds gamma ns (ELam [x] e) = tclambda tds gamma ns x e tc tds gamma ns (ELam (x:y:xs) e) = tclambda tds gamma ns x (ELam (y:xs) e) tc tds gamma ns (ELet recursive dl e) = if not recursive then tclet tds gamma ns xs es e else tcletrec tds gamma ns xs es e where (xs, es) = unzip2 dl tc tds gamma ns (ECase switch alts) = tccase tds gamma ns switch constructors arglists exprs where (constructors, alters) = unzip2 alts (arglists, exprs) = unzip2 alters --==========================================================-- --=== 0.00 Type-checking case-expressions ===-- --==========================================================-- tcConstrTypeSchemes :: TypeNameSupply -> TypeDef -> (TypeNameSupply, AList Naam TypeScheme) tcConstrTypeSchemes ns (tn, stvs, cal) = (finalNameSupply, map2nd enScheme cAltsCurried) where -- associates new type vars with each poly var -- in the type newTVs = tcNewTypeVars (tn, stvs, cal) ns -- the actual type variables themselves tVs = map second newTVs -- the types of the constructor functions cAltsCurried = map2nd (foldr TArr tdSignature) cAltsXLated cAltsXLated = map2nd (map (tcTDefSubst newTVs)) cal tdSignature = TCons tn (map TVar tVs) enScheme texp = Scheme ((nub.tcTvars_in) texp) texp -- the revised name supply finalNameSupply = applyNtimes ( length tVs + 2) tcDeplete ns -- apply a function n times to an arg applyNtimes n func arg | n ==0 = arg | otherwise = applyNtimes (n-1) func (func arg) --======================================================-- -- tccase :: [TypeDef] -> -- constructor type definitions TcTypeEnv -> -- current type bindings TypeNameSupply -> -- name supply CExpr -> -- switch expression [Naam] -> -- constructors [[Naam]] -> -- argument lists [CExpr] -> -- resulting expressions Reply TypeInfo Message tccase tds gamma ns sw cs als res -- get the type definition in use, & an association of -- variables therein to type vars & pass -- Also, reorder the argument lists -- and resulting expressions so as to reflect the -- sequence of constructors in the definition = if length tdCNames /= length (nub cs) then fail "Error in source program: missing alternatives in CASE" else tccase1 tds gamma ns1 sw reOals reOres newTVs tdInUse where tdInUse = tcGetTypeDef tds cs newTVs = tcNewTypeVars tdInUse ns2 (ns1, ns2) = tcSplit ns merge = zip cs (zip als res) tdCNames = map first (tcK33 tdInUse) (reOals, reOres) = unzip2 (tcReorder tdCNames merge) --======================================================-- -- tcReorder :: [Naam] -> [(Naam,b)] -> [b] tcReorder [] uol = [] tcReorder (k:ks) uol = (utLookupDef uol k (fail ("Error in source program: undeclared constructor '" ++ k ++ "' in CASE") ) ) : tcReorder ks uol --======================================================-- -- Projection functions and similar rubbish. tcDeOksel (Ok x) = x tcDeOksel (Fail m) = panic ("tcDeOkSel: " ++ m) tcOk13sel (Ok (a, b, c)) = a tcOk13sel (Fail m) = panic ("tcOk13sel: " ++ m) tcOk23sel (Ok (a, b, c)) = b tcOk23sel (Fail m) = panic ("tcOk23sel: " ++ m) tcOk33sel (Ok (a, b, c)) = c tcOk33sel (Fail m) = panic ("tcOk33sel: " ++ m) tcK31sel (a, b, c) = a tcK33 (a,b,c) = c --======================================================-- -- tccase1 :: [TypeDef] -> TcTypeEnv -> TypeNameSupply -> CExpr -> [[Naam]] -> [CExpr] -> AList Naam TVName -> TypeDef -> Reply TypeInfo Message tccase1 tds gamma ns sw reOals reOres newTVs tdInUse -- calculate all the gammas for the RHS's -- call tc for each RHS, so as to gather all the -- sigmas and types for each RHS, then pass on = tccase2 tds gamma ns2 sw reOals newTVs tdInUse rhsTcs where rhsGammas = tcGetAllGammas newTVs (tcK33 tdInUse) reOals rhsTcs = rhsTc1 ns1 rhsGammas reOres rhsTc1 nsl [] [] = [] rhsTc1 nsl (g:gs) (r:rs) = tc tds (g++gamma) nsl1 r : rhsTc1 nsl2 gs rs where (nsl1, nsl2) = tcSplit nsl (ns1, ns2) = tcSplit ns --======================================================-- -- tccase2 :: [TypeDef] -> TcTypeEnv -> TypeNameSupply -> CExpr -> [[Naam]] -> AList Naam TVName -> TypeDef -> [Reply TypeInfo Message] -> Reply TypeInfo Message tccase2 tds gamma ns sw reOals newTVs tdInUse rhsTcs -- get the unifiers for T1 to Tk and hence the unifier for all -- type variables in the type definition. Also compute the -- unifier of the result types. = tccase3 tds gamma ns sw reOals newTVs tdInUse rhsTcs phi_1_to_n tau_1_to_n phi_rhs where phi_1_to_n = map tcOk13sel rhsTcs tau_1_to_n = map tcOk23sel rhsTcs phi_rhs = tcDeOksel (tcUnifySet tcId_subst tau_1_to_n) --======================================================-- -- tccase3 :: [TypeDef] -> -- tds TcTypeEnv -> -- gamma TypeNameSupply -> -- ns CExpr -> -- sw [[Naam]] -> -- reOals AList Naam TVName -> -- newTVs TypeDef -> -- tdInUse [Reply TypeInfo Message] -> -- rhsTcs [Subst] -> -- phi_1_to_n [TExpr] -> -- tau_1_to_n Subst -> -- phi_rhs Reply TypeInfo Message tccase3 tds gamma ns sw reOals newTVs tdInUse rhsTcs phi_1_to_n tau_1_to_n phi_rhs -- make up substitutions for each of the unknown tvars -- merge the substitutions into one -- apply the substitution to the typedef's signature to get the -- most general allowable input type -- call tc to get the type of the switch expression -- check that this is an instance of the deduced input type -- gather the new bindings from the RHSs and switch expression -- return Ok (the big substitution, the result type, gathered bindings) = Ok (phi_Big, tau_final, (tau_final, ACase tree_s (zip tdCNames (zip reOals annotatedRHSs)))) where phi_sTau_sTree_s = tc tds gamma ns sw phi_s = tcOk13sel phi_sTau_sTree_s tau_s = tcOk23sel phi_sTau_sTree_s tree_s = tcOk33sel phi_sTau_sTree_s phi = tcMergeSubs (concat phi_1_to_n ++ phi_rhs ++ phi_s) tau_lhs = tcSub_type phi tdSignature phi_lhs = tcUnify tcId_subst (tau_lhs, tau_s) -- reverse these? phi_Big = tcMergeSubs (tcDeOksel phi_lhs ++ phi) tau_final = tcSub_type phi_Big (head (map tcOk23sel rhsTcs)) annotatedRHSs = map tcOk33sel rhsTcs tVs = map second newTVs tdSignature = TCons (tcK31sel tdInUse) (map TVar tVs) tdCNames = map first (tcK33 tdInUse) --======================================================-- -- tcUnifySet :: Subst -> [TExpr] -> Reply Subst Message tcUnifySet sub (e1:[]) = Ok sub tcUnifySet sub (e1:e2:[]) = tcUnify sub (e1, e2) tcUnifySet sub (e1:e2:e3:es) = tcUnifySet newSub (e2:e3:es) where newSub = tcDeOksel (tcUnify sub (e1, e2)) --======================================================-- -- tcNewTypeVars :: TypeDef -> TypeNameSupply -> AList Naam TVName tcNewTypeVars (t, vl, c) ns = zip vl (tcName_sequence ns) --======================================================-- -- tcGetGammaN :: AList Naam TVName -> ConstrAlt -> [Naam] -> AList Naam TypeScheme tcGetGammaN tvl (cname, cal) cparams = zip cparams (map (Scheme [] . tcTDefSubst tvl) cal) --======================================================-- -- tcTDefSubst :: AList Naam TVName -> TDefExpr -> TExpr tcTDefSubst nameMap (TDefVar n) = f result where f (Just tvn) = TVar tvn f Nothing = TCons n [] result = utLookup nameMap n tcTDefSubst nameMap (TDefCons c al) = TCons c (map (tcTDefSubst nameMap) al) --======================================================-- -- tcGetAllGammas :: AList Naam TVName -> [ConstrAlt] -> [[Naam]] -> [AList Naam TypeScheme] tcGetAllGammas tvl [] [] = [] -- note param lists cparamss must be ordered in -- accordance with calts tcGetAllGammas tvl (calt:calts) (cparams:cparamss) = tcGetGammaN tvl calt cparams : tcGetAllGammas tvl calts cparamss --======================================================-- -- tcGetTypeDef :: [TypeDef] -> -- type definitions [Naam] -> -- list of constructors used here TypeDef tcGetTypeDef tds cs = if length tdefset == 0 then fail "Undeclared constructors in use" else if length tdefset > 1 then fail "CASE expression contains mixed constructors" else head tdefset where tdefset = nub [ (tname, ftvs, cl) | (tname, ftvs, cl) <- tds, usedc <- cs, usedc `elem` (map first cl) ] --==========================================================-- --=== 9.71 Type-checking lists of expressions ===-- --==========================================================-- --======================================================-- -- tcl :: [TypeDef] -> TcTypeEnv -> TypeNameSupply -> [CExpr] -> Reply (Subst, [TExpr], [AnnExpr Naam TExpr]) Message tcl tds gamma ns [] = Ok (tcId_subst, [], []) tcl tds gamma ns (e:es) = tcl1 tds gamma ns0 es (tc tds gamma ns1 e) where (ns0, ns1) = tcSplit ns --======================================================-- -- tcl1 tds gamma ns es (Fail m) = Fail m tcl1 tds gamma ns es (Ok (phi, t, annotatedE)) = tcl2 phi t (tcl tds (tcSub_te phi gamma) ns es) annotatedE --======================================================-- -- tcl2 phi t (Fail m) annotatedE = Fail m tcl2 phi t (Ok (psi, ts, annotatedEs)) annotatedE = Ok (psi `tcScomp` phi, (tcSub_type psi t):ts, annotatedE:annotatedEs) --==========================================================-- --=== 9.72 Type-checking variables ===-- --==========================================================-- --======================================================-- -- tcvar :: [TypeDef] -> TcTypeEnv -> TypeNameSupply -> Naam -> Reply TypeInfo Message tcvar tds gamma ns x = Ok (tcId_subst, finalType, (finalType, AVar x)) where scheme = tcCharVal gamma x finalType = tcNewinstance ns scheme --======================================================-- -- tcNewinstance :: TypeNameSupply -> TypeScheme -> TExpr tcNewinstance ns (Scheme scvs t) = tcSub_type phi t where al = scvs `zip` (tcName_sequence ns) phi = tcAl_to_subst al --======================================================-- -- tcAl_to_subst :: AList TVName TVName -> Subst tcAl_to_subst al = map2nd TVar al --==========================================================-- --=== 9.73 Type-checking applications ===-- --==========================================================-- --======================================================-- -- tcap :: [TypeDef] -> TcTypeEnv -> TypeNameSupply -> CExpr -> CExpr -> Reply TypeInfo Message tcap tds gamma ns e1 e2 = tcap1 tvn (tcl tds gamma ns' [e1, e2]) where tvn = tcNext_name ns ns' = tcDeplete ns --======================================================-- -- tcap1 tvn (Fail m) = Fail m tcap1 tvn (Ok (phi, [t1, t2], [ae1, ae2])) = tcap2 tvn (tcUnify phi (t1, t2 `TArr` (TVar tvn))) [ae1, ae2] --======================================================-- -- tcap2 tvn (Fail m) [ae1, ae2] = Fail m tcap2 tvn (Ok phi) [ae1, ae2] = Ok (phi, finalType, (finalType, AAp ae1 ae2)) where finalType = tcApply_sub phi tvn --==========================================================-- --=== 9.74 Type-checking lambda abstractions ===-- --==========================================================-- --======================================================-- -- tclambda :: [TypeDef] -> TcTypeEnv -> TypeNameSupply -> Naam -> CExpr -> Reply TypeInfo Message tclambda tds gamma ns x e = tclambda1 tvn x (tc tds gamma' ns' e) where ns' = tcDeplete ns gamma' = tcNew_bvar (x, tvn): gamma tvn = tcNext_name ns --======================================================-- -- tclambda1 tvn x (Fail m) = Fail m tclambda1 tvn x (Ok (phi, t, annotatedE)) = Ok (phi, finalType, (finalType, ALam [x] annotatedE)) where finalType = (tcApply_sub phi tvn) `TArr` t --======================================================-- -- tcNew_bvar (x, tvn) = (x, Scheme [] (TVar tvn)) --==========================================================-- --=== 9.75 Type-checking let-expressions ===-- --==========================================================-- --======================================================-- -- tclet :: [TypeDef] -> TcTypeEnv -> TypeNameSupply -> [Naam] -> [CExpr] -> CExpr -> Reply TypeInfo Message tclet tds gamma ns xs es e = tclet1 tds gamma ns0 xs e rhsTypes where (ns0, ns1) = tcSplit ns rhsTypes = tcl tds gamma ns1 es --======================================================-- -- tclet1 tds gamma ns xs e (Fail m) = Fail m tclet1 tds gamma ns xs e (Ok (phi, ts, rhsAnnExprs)) = tclet2 phi xs False (tc tds gamma'' ns1 e) rhsAnnExprs where gamma'' = tcAdd_decls gamma' ns0 xs ts gamma' = tcSub_te phi gamma (ns0, ns1) = tcSplit ns --======================================================-- -- tclet2 phi xs recFlag (Fail m) rhsAnnExprs = Fail m tclet2 phi xs recFlag (Ok (phi', t, annotatedE)) rhsAnnExprs = Ok (phi' `tcScomp` phi, t, (t, ALet recFlag (zip xs rhsAnnExprs) annotatedE)) --======================================================-- -- tcAdd_decls :: TcTypeEnv -> TypeNameSupply -> [Naam] -> [TExpr] -> TcTypeEnv tcAdd_decls gamma ns xs ts = (xs `zip` schemes) ++ gamma where schemes = map (tcGenbar unknowns ns) ts unknowns = tcUnknowns_te gamma --======================================================-- -- tcGenbar unknowns ns t = Scheme (map second al) t' where al = scvs `zip` (tcName_sequence ns) scvs = (nub (tcTvars_in t)) `tcBar` unknowns t' = tcSub_type (tcAl_to_subst al) t --==========================================================-- --=== 9.76 Type-checking letrec-expressions ===-- --==========================================================-- --======================================================-- -- tcletrec :: [TypeDef] -> TcTypeEnv -> TypeNameSupply -> [Naam] -> [CExpr] -> CExpr -> Reply TypeInfo Message tcletrec tds gamma ns xs es e = tcletrec1 tds gamma ns0 xs nbvs e (tcl tds (nbvs ++ gamma) ns1 es) where (ns0, ns') = tcSplit ns (ns1, ns2) = tcSplit ns' nbvs = tcNew_bvars xs ns2 --======================================================-- -- tcNew_bvars xs ns = map tcNew_bvar (xs `zip` (tcName_sequence ns)) --======================================================-- -- tcletrec1 tds gamma ns xs nbvs e (Fail m) = (Fail m) tcletrec1 tds gamma ns xs nbvs e (Ok (phi, ts, rhsAnnExprs)) = tcletrec2 tds gamma' ns xs nbvs' e (tcUnifyl phi (ts `zip` ts')) rhsAnnExprs where ts' = map tcOld_bvar nbvs' nbvs' = tcSub_te phi nbvs gamma' = tcSub_te phi gamma --======================================================-- -- tcOld_bvar (x, Scheme [] t) = t --======================================================-- -- tcletrec2 tds gamma ns xs nbvs e (Fail m) rhsAnnExprs = (Fail m) tcletrec2 tds gamma ns xs nbvs e (Ok phi) rhsAnnExprs = tclet2 phi xs True (tc tds gamma'' ns1 e) rhsAnnExprs where ts = map tcOld_bvar nbvs' nbvs' = tcSub_te phi nbvs gamma' = tcSub_te phi gamma gamma'' = tcAdd_decls gamma' ns0 (map first nbvs) ts (ns0, ns1) = tcSplit ns subnames = map first nbvs --==========================================================-- --=== End TypeCheck5.m (1) ===-- --==========================================================--