+++ /dev/null
-
---==========================================================--
---=== 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) ===--
---==========================================================--
projects / ghc-hetmet.git / blobdiff