{- ****************************************************************************** * H M T C * * * * Module: TypeChcker * * Purpose: MiniTriangle Type Checker * * Authors: Henrik Nilsson * * * * Copyright (c) Henrik Nilsson, 2006 - 2015 * * * ****************************************************************************** -} -- | MiniTriangle Type Checker. -- Substantially re-written autumn 2013 module TypeChecker ( typeCheck, -- :: A.AST -> D MTIR testTypeChecker -- :: String -> [(Name,Type)] -> IO () ) where -- Standard library imports import Data.List ((\\), nub, sort, intersperse) import Data.Maybe (fromJust) import Control.Monad (mapAndUnzipM, unless) import Control.Monad.Fix (mfix) import Debug.Trace (trace, traceShow) -- HMTC module imports import SrcPos import Diagnostics import Name import ScopeLevel import Type import Symbol import Env import MTStdEnv import qualified AST as A import MTIR import PPMTIR import Parser (parse) -- | Type checks a complete MiniTriangle program in the standard environment -- and reports any errors. Hence a computation in the diagnostics monad 'D'. -- Additionally, translates the program into the type-annotated, intermediate -- representation MTIR, including eliminating implicit dereferencing at the -- source level by inserting explicit dereferencing operations. -- See the Coursework Description Part II for an explanation of the concepts -- and principles behind this type checker, along with the typing rules that -- define the MiniTriangle type system which this type checker implements. -- In particular, comments like "T-IF", "env(x) = s" and "env |- e : t" -- refers to those typing rules, with the following naming conventions: -- -- Type set typing rule ASCII Comments -- -------------------- -------------- -- Capital gamma "env" -- turnstile "|-" -- vector notation (e.g. "e" overlined) plural "s" suffix, e.g. "es" typeCheck :: A.AST -> D MTIR typeCheck (A.AST {A.astCmd = c}) = do c' <- chkCmd mtStdEnv c return (MTIR {mtirCmd = c'}) ------------------------------------------------------------------------------ -- Implementation of main typing rules ------------------------------------------------------------------------------ -- Check that command is well-formed in the given environment: -- -- env |- c chkCmd :: Env -> A.Command -> D Command -- T-ASSIGN chkCmd env (A.CmdAssign {A.caVar = x, A.caVal = e, A.cmdSrcPos = sp}) = do (s, x') <- infTpExp env x -- env |- x : s (t, x'')<- sinks_nonreftype s x' -- sinks(s,t), not reftype(t) e' <- chkTpExp env e t -- env |- e : t return (CmdAssign {caVar = x'', caVal = e', cmdSrcPos = sp}) -- T-CALL chkCmd env (A.CmdCall {A.ccProc = p, A.ccArgs = es, A.cmdSrcPos = sp}) = do (ss, es') <- mapAndUnzipM (infTpExp env) es (ts, t, p') <- infArrTpExp env p ss -- env |- p : ts->Void require (t == Void) sp (notProcMsg t) es'' <- zipWith3M sources ss ts es' -- env |- es : ts return (CmdCall {ccProc = p', ccArgs = es'', cmdSrcPos = sp}) where notProcMsg t = "Not a procedure; return type is " ++ show t -- T-SEQ (generalized to sequence of any length) chkCmd env (A.CmdSeq {A.csCmds = cs, A.cmdSrcPos = sp}) = do cs' <- mapM (chkCmd env) cs -- env |- cs return (CmdSeq {csCmds = cs', cmdSrcPos = sp}) -- T-IF chkCmd env (A.CmdIf {A.ciCondThens = ecs, A.ciMbElse = mbce, A.cmdSrcPos=sp}) = do ecs' <- mapM (tcCondThen env) ecs -- env |- es : Boolean -- env |- cs mbce' <- case mbce of Nothing -> return Nothing Just ce -> do ce' <- chkCmd env ce -- env |- ce return (Just ce') return (CmdIf {ciCondThens = ecs', ciMbElse = mbce', cmdSrcPos = sp}) where tcCondThen :: Env -> (A.Expression, A.Command) -> D (Expression, Command) tcCondThen env (e, c) = do e' <- chkTpExp env e Boolean c' <- chkCmd env c return (e', c') -- T-WHILE chkCmd env (A.CmdWhile {A.cwCond = e, A.cwBody = c, A.cmdSrcPos = sp}) = do e' <- chkTpExp env e Boolean -- env |- e : Boolean c' <- chkCmd env c -- env |- c return (CmdWhile {cwCond = e', cwBody = c', cmdSrcPos = sp}) -- T-REPEAT chkCmd env (A.CmdRepeat {A.crBody = c, A.crCond = e, A.cmdSrcPos = sp}) = do c' <- chkCmd env c -- env |- c e' <- chkTpExp env e Boolean -- env |- e : Boolean return (CmdRepeat {crBody = c', crCond = e', cmdSrcPos = sp}) -- T-LET chkCmd env (A.CmdLet {A.clDecls = ds, A.clBody = c, A.cmdSrcPos = sp}) = do (ds', env') <- mfix $ \ ~(_, env') -> -- env;env'|- ds | env' chkDeclarations (openMinScope env) env' ds c' <- chkCmd env' c -- env' |- c return (CmdLet {clDecls = ds', clBody = c', cmdSrcPos = sp}) -- Check that declarations/definitions are well-typed in given environment -- and environmant for function/procedure bodies and compute extended -- environment: -- -- env; envB |- ds | env' -- -- [For future reference: If user defined types were allowed, envB should -- perhaps be used in place of env for elaboarting types and computing -- function/procedure types if it is desired to allow (mutually) recursive -- type definitions.] chkDeclarations :: Env -> Env -> [A.Declaration] -> D ([Declaration], Env) -- T-DECLEMPTY chkDeclarations env envB [] = return ([], env) -- T-DECLCONST chkDeclarations env envB (A.DeclConst {A.dcConst = x, A.dcVal = e, A.dcType = t, A.declSrcPos=sp} : ds) = do t' <- chkDclType env t e' <- chkTpExp env e t' -- env |- e : t case enterIntTermSym x (Src t') sp env of -- env' = env, x : Src t Left old -> do emitErrD sp (redeclaredMsg old) chkDeclarations env envB ds Right (env', x') -> do wellinit (itmsLvl x') e' (ds', env'') <- chkDeclarations env' -- env'; envB |- ds | env'' envB ds return (DeclConst {dcConst = x', dcVal = e'} : ds', env'') -- T-DECLVAR chkDeclarations env envB (A.DeclVar {A.dvVar = x, A.dvType = t, A.dvMbVal = Nothing, A.declSrcPos=sp} : ds) = do t' <- chkDclType env t case enterIntTermSym x (Ref t') sp env of -- env' = env, x : Ref t Left old -> do emitErrD sp (redeclaredMsg old) chkDeclarations env envB ds Right (env', x') -> do (ds', env'') <- chkDeclarations env' -- env'; envB |- ds | env'' envB ds return (DeclVar {dvVar = x', dvMbVal = Nothing} : ds', env'') -- T-DECLINITVAR chkDeclarations env envB (A.DeclVar {A.dvVar = x, A.dvType = t, A.dvMbVal = Just e, A.declSrcPos=sp} : ds) = do t' <- chkDclType env t e' <- chkTpExp env e t' -- env |- e : t case enterIntTermSym x (Ref t') sp env of -- env' = env, x : Ref t Left old -> do emitErrD sp (redeclaredMsg old) chkDeclarations env envB ds Right (env', x') -> do wellinit (itmsLvl x') e' (ds', env'') <- chkDeclarations env' -- env'; envB |- ds | env'' envB ds return (DeclVar {dvVar = x', dvMbVal = Just e'} : ds', env'') -- T-DECLFUN chkDeclarations env envB (A.DeclFun {A.dfFun = f, A.dfOvrld = o, A.dfArgDecls = as, A.dfType = t, A.dfBody = e, A.declSrcPos = sp} : ds) = do ~(as', envB') <- chkArgDecls (openMajScope envB) as -- envB |- as | envB' tf <- funType env as t e' <- chkTpExp envB' e (retType tf) -- envB' |- e : t case enterSym f tf sp env of -- env' = env, f: tf Left old -> do emitErrD sp (redeclaredMsg old) chkDeclarations env envB ds Right (env', f') -> do (ds', env'') <- chkDeclarations env' -- env'; envB |- ds | env'' envB ds return (DeclFun {dfFun = f', dfArgs = as', dfBody = e'} : ds', env'') where enterSym = if o then enterOvrldIntTermSym else enterIntTermSym -- T-DECLPROC chkDeclarations env envB (A.DeclProc {A.dpProc = p, A.dpOvrld = o, A.dpArgDecls = as, A.dpBody = c, A.declSrcPos = sp} : ds) = do ~(as', envB') <- chkArgDecls (openMajScope envB) as -- envB |- as | envB' c' <- chkCmd envB' c -- envB' |- c tp <- procType env as case enterSym p tp sp env of -- env' = env, f: tf Left old -> do emitErrD sp (redeclaredMsg old) chkDeclarations env envB ds Right (env', p') -> do (ds', env'') <- chkDeclarations env' -- env'; envB |- ds | env'' envB ds return (DeclProc {dpProc = p', dpArgs = as', dpBody = c'} : ds', env'') where enterSym = if o then enterOvrldIntTermSym else enterIntTermSym -- Check that function/procedure argument declarations are well-typed in -- given environment and compute extended environment: -- -- env |- as | env' chkArgDecls :: Env -> [A.ArgDecl] -> D ([IntTermSym], Env) -- T-DECLARGEMPTY chkArgDecls env [] = return ([], env) -- T-DECLARG, T-DECLINARG, T-DECLOUTARG, T-DECLVARARG chkArgDecls env (A.ArgDecl {A.adArg = x, A.adArgMode = am, A.adType = td, A.adSrcPos=sp} : as) = do t <- chkDclType env td case enterIntTermSym x (Src (amType am t)) sp env of -- env' = env, x: ... Left old -> do emitErrD sp (redeclaredMsg old) chkArgDecls env as Right (env', x') -> do (as', env'') <- chkArgDecls env' as -- env' |- as | env'' return (x' : as', env'') redeclaredMsg :: IntTermSym -> String redeclaredMsg itms = "Identifier \"" ++ itmsName itms ++ "\" redeclared; already declared at " ++ show (itmsSrcPos itms) procType :: Env -> [A.ArgDecl] -> D Type procType env as = do ts <- chkArgTypes env as return (Arr ts Void) funType :: Env -> [A.ArgDecl] -> A.TypeDenoter -> D Type funType env as td = do ts <- chkArgTypes env as t <- chkDclType env td return (Arr ts t) chkArgTypes :: Env -> [A.ArgDecl] -> D [Type] chkArgTypes env [] = return [] chkArgTypes env (A.ArgDecl {A.adArgMode = am, A.adType = td} : as) = do t <- chkDclType env td ts <- chkArgTypes env as return (amType am t : ts) -- Checks that a given type is defined and translate into internal type -- representation. chkDclType :: Env -> A.TypeDenoter -> D Type chkDclType env (A.TDBaseType {A.tdbtName = t, A.tdSrcPos = sp}) = case lookupTypeSym t env of Nothing -> do emitErrD sp ("Undefined type \"" ++ t ++ "\"") return SomeType Just tps -> return (tpsType tps) chkDclType env (A.TDArray {A.tdaEltType = t, A.tdaSize = s, A.tdSrcPos = sp}) = do t' <- chkDclType env t s' <- toMTInt s sp return (Ary t' s') chkDclType env (A.TDRecord {A.tdrFldTypes = fts}) = do -- Note: Ensures record fields are sorted (invariant of Rcd) let (xs,ts) = unzip fts ts' <- mapM (chkDclType env) ts return (Rcd (sortRcdFlds (zip xs ts'))) -- Type representation corresponding to given argument mode amType :: A.ArgMode -> (Type -> Type) amType A.ByValue = id -- Call-by-value amType A.ByRefIn = Src -- Call-by-ref input amType A.ByRefOut = Snk -- Call-by-ref output amType A.ByRefVar = Ref -- Call-by-ref variable -- Check that expression has type t in given environment: -- -- env |- e : t -- -- This is an algorithmic version of the typing relation for expressions -- to be used when the desired type is known. Knowing the target type -- makes it easy to use the rule T-SOURCES. chkTpExp :: Env -> A.Expression -> Type -> D Expression -- T-SOURCES chkTpExp env e t = do (s, e') <- infTpExp env e -- env |- e : s, sources(s,t) sources s t e' -- Check that expression is well-typed in the given environment and -- infer its type assuming no (top-level) implicit dereferencing: -- -- env |- e : t -- -- This is an algorithmic version of the typing relation for expressions -- to be used when the desired type is not known and leaving the option -- for further dereferencing open. infTpExp :: Env -> A.Expression -> D (Type, Expression) -- T-LITCHR infTpExp env e@(A.ExpLitChr {A.elcVal = c, A.expSrcPos = sp}) = do c' <- toMTChr c sp return (Character, -- env |- c : Character ExpLitChr {elcVal = c', expType = Character, expSrcPos = sp}) -- T-LITINT infTpExp env e@(A.ExpLitInt {A.eliVal = n, A.expSrcPos = sp}) = do n' <- toMTInt n sp return (Integer, -- env |- n : Integer ExpLitInt {eliVal = n', expType = Integer, expSrcPos = sp}) -- T-VAR infTpExp env (A.ExpVar {A.evVar = x, A.expSrcPos = sp}) = do tms <- case lookupTermSym x env of -- env(x) = t, sources(t,t) Nothing -> do emitErrD sp ("Variable \"" ++ x ++ "\" undefined") return (dummyTmS x) Just tms -> return tms return (tmsType tms, tmsToExp tms sp) -- T-APP infTpExp env (A.ExpApp {A.eaFun = f, A.eaArgs = es, A.expSrcPos = sp}) = do (ss, es') <- mapAndUnzipM (infTpExp env) es (ts, t, f') <- infArrTpExp env f ss -- env |- f : ts -> t es'' <- zipWith3M sources ss ts es' -- env |- es : ts return (t, ExpApp {eaFun = f', eaArgs = es'', expType = t, expSrcPos = sp}) infTpExp env (A.ExpCond {A.ecCond = e1, A.ecTrue = e2, A.ecFalse = e3, A.expSrcPos = sp}) = do e1' <- chkTpExp env e1 Boolean -- Env |- e1 : Boolean (t, e2') <- infNonRefTpExp env e2 -- Env |- e2 : t (t', e3') <- infNonRefTpExp env e3 -- Env |- e3 : t' require (t == t') sp ("Conditional branches have to have the same \ \types; " ++ "got " ++ show t ++ " and " ++ show t') return (t, ExpCond {ecCond = e1', ecTrue = e2', ecFalse = e3', expType = t, expSrcPos = sp}) -- T-ARY, empty case handled specially infTpExp env (A.ExpAry {A.eaElts = [], A.expSrcPos = sp}) = do let t = Ary SomeType 0 return (t, ExpAry {eaElts = [], expType = t, expSrcPos = sp}) infTpExp env (A.ExpAry {A.eaElts = ees@(e:es), A.expSrcPos = sp}) = do (t, e') <- infNonRefTpExp env e -- env |- e : t, not reftype(t) es' <- mapM (\e -> chkTpExp env e t) es -- env |- es : t let ta = Ary t (fromIntegral (length ees)) return (ta, ExpAry {eaElts = e':es', expType = ta, expSrcPos = sp}) -- T-IX infTpExp env (A.ExpIx {A.eiAry = a, A.eiIx = i, A.expSrcPos = sp}) = do (rat, a') <- infRefAryTpExp env a -- env |- a : R(T[n]) i' <- chkTpExp env i Integer -- end |- i : Integer let rt = mapRfcdType eltType rat return (rt, ExpIx {eiAry = a', eiIx = i', expType = rt, expSrcPos = sp}) -- T-RCD infTpExp env (A.ExpRcd {A.erFldDefs = fds, A.expSrcPos = sp}) = do -- Note: Ensures record fields are sorted (invariant of ExpRcd and Rcd) let (xs, es) = unzip (sortRcdFlds fds) tes' <- mapM (infNonRefTpExp env) es -- env |- es : ts require (allDistinct xs) sp (repeatedMsg xs) let (ts, es') = unzip tes' let fds' = zip xs es' let tr = Rcd (zip xs ts) return (tr, ExpRcd {erFldDefs = fds', expType = tr, expSrcPos = sp}) where allDistinct xs = xs == nub xs repeatedMsg xs = "Repeated record field name(s): \"" ++ concat (intersperse "\", \"" (nub (xs \\ nub xs))) ++ "\"" -- T-PRJ infTpExp env (A.ExpPrj {A.epRcd = e, A.epFld = f, A.expSrcPos = sp}) = do (rrt, e') <- infRefRcdTpExp env e -- env |- e : R({xs:ts}) require (fldExists f (rfcdType rrt)) sp (notAFieldMsg f (rfcdType rrt)) let rt = mapRfcdType (fldType f) rrt return (rt, ExpPrj {epRcd = e', epFld = f, expType = rt, expSrcPos = sp}) where notAFieldMsg f rt = "The type \"" ++ show rt ++ "\" does not contain any field \"" ++ f ++ "\"" -- Check that expression is well-typed in the given environment and -- infer its type assuming it should be an non-reference type: -- -- env |- e : t, not reftype(t) -- -- This is an algorithmic version of the typing relation for expressions -- to be used when the desired type is known to be a non-reference type. infNonRefTpExp :: Env -> A.Expression -> D (Type, Expression) infNonRefTpExp env e = do (t, e') <- infTpExp env e sources_pred (not . refType) "non-reference type" t e' -- Check that expression is well-typed in the given environment and -- infer its type assuming it should be an arrow type and given the -- inferred but not dereferenced types of the actual arguments: -- -- env |- e : ts -> t -- -- The caller is responsible for checking that the type of each actual -- argument can source the type of the corresponding formal argument and -- dereference the argument expression as necessary (use "sources"). -- -- This is an algorithmic version of the typing relation for expressions -- to be used when the desired type is known to be an arrow type. -- -- The number of actual arguments is used to check the arity of expression -- type, reporting any mismatch and guaranteeing that the arity of the -- returned type agrees. -- -- The number and types of the actual arguments are used for resolving -- overloading in the case of *manifest* calls (the name of the procedure -- or function given directly as opposed to a procedure or function being -- computed). infArrTpExp :: Env -> A.Expression -> [Type] -> D ([Type], Type, Expression) infArrTpExp env e@(A.ExpVar {A.evVar = x}) ss | null tmss = do emitErrD sp ("No procedure or function called \"" ++ x ++ "\"") return (ensureArity a [], SomeType, tmsToExp (dummyTmS x) sp) | arrType (tmsType (head tmss)) = -- Manifest procedure or function call. Overloading resolution only carried -- out for manifest calls. A call is considered manifest if at least the -- first of any overloadings of the applied symbol is a manifest procedure -- or function (arrow type). case tmssCA of [] -> do emitErrD sp ("No instance of \"" ++ x ++ "\" has expected arity " ++ show a) return (ensureArity a [], SomeType, tmsToExp (dummyTmS x) sp) [tms] -> case tmsType tms of Arr ts t -> return (ts, t, tmsToExp tms sp) _ -> tcErr "infArrTpExp" "Expected arrow type" _ -> case tmssCS of [] -> do emitErrD sp ("No instance of \"" ++ x ++ "\" has a signature that agrees with \ \the types of the actual arguments: " ++ concat(intersperse ", " (map show ss))) return (ensureArity a [], SomeType, tmsToExp (dummyTmS x) sp) [tms] -> case tmsType tms of Arr ts t -> return (ts, t, tmsToExp tms sp) _ -> tcErr "infArrTpExp" "Expected arrow type" (tms : _) -> do emitWngD sp ("Ambiguous overloading of \"" ++ x ++ "\": more than one instance have \ \a signature that agrees with the \ \types of the actual arguments") case tmsType tms of Arr ts t -> return (ts, t, tmsToExp tms sp) _ -> tcErr "infArrTpExp" "Expected arrow type" where sp = srcPos e a = length ss -- Expected arity tmss = lookupOvrldTermSym x env tmssCA = [ tms -- Tm syms with Correct Arity | tms <- tmss, let t = tmsType tms, arrType t && arity t == a ] tmssCS = [ tms -- Tm syms with Compatible Sig. | tms <- tmssCA, and (zipWith sourcesp ss (argTypes (tmsType tms))) ] infArrTpExp env e ss = do -- This is the case of a computation yielding (a reference to) a -- procedure or function. No overloading resolution in this case. (s, e') <- infNonRefTpExp env e case s of Arr ts t -> do require (length ts == a) sp ("Bad arity: expected " ++ show (length ts) ++ " arguments, got " ++ show a) return (ensureArity a ts, t, e') SomeType -> do return (ensureArity a [], SomeType, e') _ -> do emitErrD sp "Not a function or procedure" return (ensureArity a [], SomeType, e') where sp = srcPos e a = length ss -- Expected arity ensureArity :: Int -> [Type] -> [Type] ensureArity a ts = take a (ts ++ repeat SomeType) -- Check that expression is well-typed in the given environment and -- infer its type assuming it should be a reference to an array: -- -- env |- e : R (t[n]), R in {Src, Snk, Ref} -- -- This is an algorithmic version of the typing relation for expressions -- to be used when the desired type is known to be a reference to an array. infRefAryTpExp :: Env -> A.Expression -> D (Type, Expression) infRefAryTpExp env e = do (t, e') <- infTpExp env e sources_pred refAry "reference to array" t e' where refAry (Src (Ary _ _)) = True refAry (Snk (Ary _ _)) = True refAry (Ref (Ary _ _)) = True refAry _ = False -- Check that expression is well-typed in the given environment and -- infer its type assuming it should be a reference to a record: -- -- env |- e : R ({a : t, ...}), R in {Src, Snk, Ref} -- -- This is an algorithmic version of the typing relation for expressions -- to be used when the desired type is known to be a reference to a record. infRefRcdTpExp :: Env -> A.Expression -> D (Type, Expression) infRefRcdTpExp env e = do (t, e') <- infTpExp env e sources_pred refRcd "reference to record" t e' where refRcd (Src (Rcd _)) = True refRcd (Snk (Rcd _)) = True refRcd (Ref (Rcd _)) = True refRcd _ = False -- Convert Integer to MTInt (MiniTriangle integer), ensuring it is -- representable as such. toMTInt :: Integer -> SrcPos -> D MTInt toMTInt n sp = if isMTInt n then return (fromInteger n) else do emitErrD sp ("Integer literal " ++ show n ++ " outside the range of " ++ "representable MiniTriangle integers") return 0 -- Convert Char to MTChr (MiniTriangle character), ensuring it is -- representable as such. toMTChr :: Char -> SrcPos -> D MTChr toMTChr c sp = if isMTChr c then return c -- MTChr is currently just a type synonym else do emitErrD sp ("Character literal " ++ show c ++ " outside the range of " ++ "representable MiniTriangle characters") return '?' -- Converts an (internal or external) term symbol into an MTIR expression: -- a variable for internal symbols, or constant/external reference for -- an external symbol. tmsToExp :: TermSym -> SrcPos -> Expression tmsToExp (Left (ExtTermSym {etmsVal = v, etmsType = t})) sp = case v of ESVBool b -> ExpLitBool {elbVal = b, expType = t, expSrcPos = sp} ESVInt n -> ExpLitInt {eliVal = n, expType = t, expSrcPos = sp} ESVChar c -> ExpLitChr {elcVal = c, expType = t, expSrcPos = sp} ESVLbl l -> ExpExtRef {eerVal = l, expType = t, expSrcPos = sp} tmsToExp (Right itms@(IntTermSym {itmsType = t})) sp = ExpVar { evVar = itms, expType = t, expSrcPos = sp } ------------------------------------------------------------------------------ -- Implementation of auxiliary predicates ------------------------------------------------------------------------------ -- Check if the value of an expression of the given type can source a value -- of the other given type. This is a version of the predicate "sources" -- from the type system specification turned into a function assuming both -- types are known. -- Additionally "coerces" the type of the expression by embedding it in -- the appropriate number of dereferencing operations. sources :: Type -> Type -> Expression -> D Expression sources s t e | s <: t = return e sources (Ref s) t e = sources s t (deref e) sources (Src s) t e = sources s t (deref e) sources s t e = do emitErrD (srcPos e) ("Expected type \"" ++ show t ++ "\", got \"" ++ show s ++ "\"") return e -- Predicate version of the above. sourcesp :: Type -> Type -> Bool sourcesp s t | s <: t = True sourcesp (Ref s) t = sourcesp s t sourcesp (Src s) t = sourcesp s t sourcesp _ _ = False {- -- Alternative definition without explicit use of subtyping for reference. -- Somewhat less flexible and a bit more verbose, but adequate for -- MiniTriangle as it stands, and avoiding subtyping is a simplification. sources :: Type -> Type -> Expression -> D Expression sources s t e | s == t = return e sources (Ref s) (Snk t) e | s == t = return e sources (Ref s) (Src t) e | s == t = return e sources (Ref s) t e = sources s t (deref e) sources (Src s) t e = sources s t (deref e) sources s t e = do emitErrD (srcPos e) ("Expected type \"" ++ show t ++ "\", got \"" ++ show s ++ "\"") return e -} -- Check if the value of an expression of the given type can source a type -- satisfying an additinal predicate p. That is, an implementation of the -- combination: -- -- sources(s,t), p(t) -- -- assuming type "s" is given and "t" is to be computed. -- Additionally "coerces" the type of the expression by embedding it in -- the appropriate number of dereferencing operations. sources_pred :: (Type -> Bool) -> String -> Type -> Expression -> D (Type, Expression) sources_pred p et t e | p t = return (t, e) sources_pred p et (Ref t) e = sources_pred p et t (deref e) sources_pred p et (Src t) e = sources_pred p et t (deref e) sources_pred p et t e = do emitErrD (srcPos e) ("Expected " ++ et ++ ", got \"" ++ show t ++ "\"") return (SomeType, e) -- Check if the value of an expression of the given type can sink a non- -- reference type. That is, an implementation of the combination: -- -- sinks(s,t), not reftype(t) -- -- assuming type "s" is given and "t" is to be computed. -- Additionally "coerces" the type of the expression by embedding it in -- the appropriate number of dereferencing operations. sinks_nonreftype :: Type -> Expression -> D (Type, Expression) sinks_nonreftype (Snk t) e | not (refType t) = return (t, e) | otherwise = do emitErrD (srcPos e) "Cannot assign value of non-reference type to this variable" return (SomeType, e) sinks_nonreftype (Src t) e = sinks_nonreftype t (deref e) sinks_nonreftype (Ref t) e | not (refType t) = return (t, e) | otherwise = sinks_nonreftype t (deref e) sinks_nonreftype SomeType e = return (SomeType, e) sinks_nonreftype _ e = do emitErrD (srcPos e) "Does not denote an assignable variable" return (SomeType, e) -- Embeds an expression in a dereferencing operation. deref :: Expression -> Expression deref e = ExpDeref { edArg = e, expType = rfcdType (expType e), expSrcPos = srcPos e } -- Check that an initialiser (expression defining a constant or initialising -- a variable) is well-initialised; i.e. does not call a function defined -- at the present scope level as this means it could refer to constants -- or variables that have not yet been initialised or even allocated. -- This is defined on MTIR rather than AST, simplifying the definition -- as the scope level of a variable is directly available, meaning that -- there is no need to look up variables in the environment. -- -- [For future reference: -- Note that this restriction could be relaxed. For example, one could -- for each function compute the set of constants/variables from the -- same block to which it refers directly or indirectly, and then -- flag a problem only if a function referring to constants/variables -- currently not in scope are called. But, as functions may be mutually -- recursive, this requires computing strongly connected components or -- an iterative fixed-point computation. -- -- Or one could implement initialization in dependency order, combined -- with a static check that there are no cycles. Or one could reorder -- declaration lists, moving procedures and functions to the end, -- either after type checking and then possibly combined with adapted -- code generation strategies, or before type checking, combined with -- changed scope rules (bringing all functions and procedures into scope -- at the start of a block) and possibly with adapted code generation -- strategies.] wellinit :: ScopeLvl -> Expression -> D () wellinit _ (ExpLitBool {}) = return () wellinit _ (ExpLitInt {}) = return () wellinit _ (ExpLitChr {}) = return () wellinit _ (ExpExtRef {}) = return () wellinit _ (ExpVar {}) = return () wellinit l (ExpDeref {edArg = e}) = wellinit l e wellinit l (ExpApp {eaFun = f, eaArgs = es}) = do case f of ExpLitBool {} -> return () -- Type error, will have been caught ExpLitInt {} -> return () -- Type error, will have been caught ExpLitChr {} -> return () -- Type error, will have been caught ExpExtRef {} -> return () -- Defined outside present scope ExpVar {evVar = IntTermSym {itmsLvl = l', itmsName = n}, expSrcPos = sp} | l' == l -> emitErrD sp ("Function \"" ++ n ++ "\" may not be called from initializers in the \ \same block as in which it is defined.") | otherwise -> return () e -> emitErrD (srcPos e) "Only known functions may be called in initializers." mapM_ (wellinit l) es wellinit l (ExpCond {ecCond = e1, ecTrue = e2, ecFalse = e3}) = wellinit l e1 >> wellinit l e2 >> wellinit l e3 wellinit l (ExpAry {eaElts = es}) = mapM_ (wellinit l) es wellinit l (ExpIx {eiAry = a, eiIx = i}) = wellinit l a >> wellinit l i wellinit l (ExpRcd {erFldDefs = fds}) = mapM_ (wellinit l . snd) fds wellinit l (ExpPrj {epRcd = e}) = wellinit l e ------------------------------------------------------------------------------ -- Error reporting utilities ------------------------------------------------------------------------------ -- Report an error unless the condition is true. require :: Bool -> SrcPos -> String -> D () require p sp m = unless p (emitErrD sp m) ------------------------------------------------------------------------------ -- Monadic utilities ------------------------------------------------------------------------------ -- Generalisation of zipWithM zipWith3M :: Monad m => (a -> b -> c -> m d) -> [a] -> [b] -> [c] -> m [d] zipWith3M f (a:as) (b:bs) (c:cs) = do d <- f a b c ds <- zipWith3M f as bs cs return (d:ds) zipWith3M _ _ _ _ = return [] ------------------------------------------------------------------------------ -- Test utilities ------------------------------------------------------------------------------ -- | Test utility. Attempts to parse and then type check the given string -- input in the standard MT environment extended with any given bindings. -- If successful, pretty-prints the resulting MTIR representation. testTypeChecker :: String -> [(Name,Type)] -> IO () testTypeChecker s bs = do putStrLn "Diagnostics:" mapM_ (putStrLn . ppDMsg) (snd result) putStrLn "" case fst result of Just mtir -> do putStrLn "MTIR:" putStrLn (ppMTIR mtir) Nothing -> putStrLn "Parsing and typechecking produced no result." putStrLn "" where result :: (Maybe MTIR, [DMsg]) result = runDF (parseCheck s (extend mtStdEnv bs)) extend env [] = env extend env ((n,t):bs) = case enterIntTermSym n t NoSrcPos env of Left _ -> error "Extending MT Standard Environment failed!" Right (env', _) -> extend env' bs parseCheck s env = do ast <- parse s failIfErrorsD c <- dToDF (chkCmd env (A.astCmd ast)) return (MTIR {mtirCmd = c}) ------------------------------------------------------------------------------ -- Internal error reporting ------------------------------------------------------------------------------ tcErr :: String -> String -> a tcErr = internalError "TypeChecker"