CSC448: Phases: Typechecking [4/8]

Contexts have the form:

    G ::= empty
        | G,x:T                (variable declaration)
        | G,f:(S1,...,Sn)->T   (function declaration)

The judgments are written:

      |- extdecl1 ... extdecln : Program
    G |- extdecl : Declaration
    G |- stat : Statement<declaredReturnType>
    G |- exp : T
      |- exp is lvalue

Every variable and array access is an lvalue. Nothing else is an lvalue.

    -----------------------------
      |- (expA[expI]) is lvalue

    ----------------
      |- x is lvalue

To check a bunch of global variable and function declarations, we put them in the context, then start checking them; this allows mutually recursive definitions.

    context(extdecl1 ... extdecln) |- extdecl1 : Declaration
    ...
    context(extdecl1 ... extdecln) |- extdecln : Declaration
    ------------------------------------------------------------------
                                   |- extdecl1 ... extdecln : Program

To check a variable declaration, we just need to make sure that the initializer has the correct type:

    ------------------------------
    G |- (T x;) : Declaration

    G |- exp : T
    -------------------------------
    G |- (T x = exp;) : Declaration

To check a function declaration, we check the body:

    G,x1:S1,...,xn:Sn |- compoundStat : Statement<T>
    -------------------------------------------------------
    G |- (T f (S1 x1,...,Sn xn) compoundStat) : Declaration

To check a statement, do a case analysis.

case StatCompound:

    G,x1:T1,...,xn:Tn |- (T1 x1 = exp1;) : Declaration
    ...
    G,x1:T1,...,xn:Tn |- (Tn xn = expn;) : Declaration
    G,x1:T1,...,xn:Tn |- stat1 : Statement<T>
    ...
    G,x1:T1,...,xn:Tn |- statm : Statement<T>
    -----------------------------------------------------------------------
    G |- { T1 x1 = exp1; ... Tn xn = expn; stat1 ... statm } : Statement<T>

case StatExp:

    G |- exp : S    (for some type S)
    ---------------------------------------
    G |- (exp;) : Statement<T>

case StatGoto:

    -----------------------------------
    G |- (goto l;) : Statement<T>

case StatIf:

    G |- exp : int
    G |- statT : Statement<T>
    G |- statF : Statement<T>
    -----------------------------------------------------
    G |- (if (exp) statT else statF) : Statement<T>

case StatReturn:

    ---------------------------------------
    G |- (return;) : Statement<void>

    G |- exp : T
    ---------------------------------------
    G |- (return exp;) : Statement<T>

case StatSkip:

    ---------------------------------
    G |- (skip;) : Statement<T>

case StatWhile:

    G |- exp : int
    G |- statW : Statement<T>
    -----------------------------------------------------
    G |- (while (exp) statW) : Statement<T>

To check an expression, do a case analysis.

case ExpInt:

    ------------
    G |- n : int

case ExpVar:

    G(x) = T
    ----------
    G |- x : T

case ExpString:

    --------------------
    G |- "value" : int[]

case ExpNew:

    G |- exp : int
    --------------------------------------------
    G |- (new T[exp]) : T[]

case ExpArrayAccess:

    G |- expA : T[]
    G |- expI : int
    -----------------------------
    G |- (expA[expI]) : T

case ExpAssign:

    G |- expL : T
    G |- expR : T
      |- expL is lval
    ------------------------------
    G |- (expL = expR) : T

case ExpUnOp:

    G |- exp : int
    ---------------------
    G |- (unop exp) : int

case ExpBinOp:

    G |- expL : int
    G |- expR : int
    -----------------------------------
    G |- (expL binop expR) : int

case ExpComma:

    G |- expL : S
    G |- expR : T
    -----------------------------
    G |- (expL , expR) : T

case ExpFunCall:

    G(f) = (S1,...,Sn)->T
    G |- exp1 : S1
    ...
    G |- expn : Sn
    ------------------------------------
    G |- (f(exp1,...,expn)) : T