Chapter 5. Typechecking (*)
Prev Part I. A Tiny Imperative Language Next

Chapter 5. Typechecking (*)

Table of Contents

5.1. Typechecking
5.2. Example

Work in Progress

This chapter is work in progress. Not all parts have been finished yet. The latest revision of this manual may contain more material. Refer to the online version.

propagation of variable types and type annotation of expressions and statements

5.1. Typechecking

Figure 5.1. file: til/tc/til-typecheck.str

module til-typecheck
imports liblib til-typecheck-stats
strategies

  io-til-typecheck =
    io-wrap(typecheck-program)
    
  typecheck-program =
    Program(typecheck-stats)

Figure 5.2. file: til/tc/til-typecheck-exp.str

module til-typecheck-exp
imports TIL
strategies

  typecheck-exp(typecheck-var) = 
    bottomup(try(
      typecheck-var <+ TypecheckAdd <+ TypecheckMul <+ TypecheckSub <+ TypecheckDiv <+ TypecheckMod
      <+ TypecheckLeq <+ TypecheckGeq <+ TypecheckLt <+ TypecheckGt <+ TypecheckEqu <+ TypecheckNeq
      <+ TypecheckOr <+ TypecheckAnd
      <+ TypecheckInt <+ TypecheckString <+ TypecheckBool
    ))

rules

  typeof :
    e{t*} -> t
    where <fetch-elem(is-type)> t* => t
    
  is-type = 
    ?TypeName(_)
    
  TypecheckInt :
    Int(i) -> Int(i){TypeName("int")}

  TypecheckString :
    String(x) -> String(x){TypeName("string")}

  TypecheckBool :
    True() -> True(){TypeName("bool")}
    
  TypecheckBool :
    False() -> False(){TypeName("bool")}
    
  TypecheckAdd :
    Add(e1, e2) -> Add(e1, e2){TypeName("string")}
    where <typeof> e1 => TypeName("string")
        ; <typeof> e2 => TypeName("string")

  TypecheckAdd :
    Add(e1, e2) -> Add(e1, e2){TypeName("int")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")

  TypecheckMul :
    Mul(e1, e2) -> Mul(e1, e2){TypeName("int")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")

  TypecheckSub :
    Sub(e1, e2) -> Sub(e1, e2){TypeName("int")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")

  TypecheckDiv :
    Div(e1, e2) -> Div(e1, e2){TypeName("int")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")
 
  TypecheckMod :
    Mod(e1, e2) -> Mod(e1, e2){TypeName("int")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")

  TypecheckLt :
    Lt(e1, e2) -> Lt(e1, e2){TypeName("bool")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")

  TypecheckGt :
    Gt(e1, e2) -> Gt(e1, e2){TypeName("bool")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")
   
  TypecheckLeq :
    Leq(e1, e2) -> Leq(e1, e2){TypeName("bool")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")
        
  TypecheckGeq :
    Geq(e1, e2) -> Geq(e1, e2){TypeName("bool")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")
 
  TypecheckEqu :
    Equ(e1, e2) -> Equ(e1, e2){TypeName("bool")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")
        
  TypecheckNeq :
    Neq(e1, e2) -> Neq(e1, e2){TypeName("bool")}
    where <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")
           
  TypecheckAnd :
    And(e1, e2) -> And(e1, e2){TypeName("bool")}
    where <typeof> e1 => TypeName("bool")
        ; <typeof> e2 => TypeName("bool")
           
  TypecheckOr :
    Or(e1, e2) -> Or(e1, e2){TypeName("bool")}
    where <typeof> e1 => TypeName("bool")
        ; <typeof> e2 => TypeName("bool")

Figure 5.3. file: til/tc/til-typecheck-stats.str

module til-typecheck-stats
imports til-typecheck-var
strategies

  typecheck-block = 
    Block(typecheck-stats)

  typecheck-stats = 
    {| TypeOf : map(typecheck-stat) |}

  typecheck-stat = 
    typecheck-block
    <+ typecheck-declaration
    <+ Assign(id, typecheck-exp)
       ; try(TypecheckAssign)
    <+ IfElse(typecheck-exp, typecheck-stats, typecheck-stats)
       ; TypecheckIf
    <+ IfThen(typecheck-exp, typecheck-stats)
       ; TypecheckIf
    <+ While(typecheck-exp, typecheck-stats)
       ; TypecheckWhile
    <+ ProcCall(id, map(typecheck-exp))
       ; typecheck-proccall
    <+ For(id, typecheck-exp, typecheck-exp, typecheck-stats)
       ; TypecheckFor
    <+ debug(!"unknown statement: ")
       ; <exit> 1

  TypecheckIf :
    IfElse(e, st1*, st2*) -> IfElse(e, st1*, st2*){TypeName("void")}
    where <typeof> e => TypeName("bool")
    
  TypecheckIf :
    IfThen(e, st*) -> IfThen(e, st*){TypeName("void")}
    where <typeof> e => TypeName("bool")

  TypecheckWhile : 
    While(e, st*) -> While(e, st*){TypeName("void")}
    where <typeof> e => TypeName("bool")

  TypecheckFor : 
    For(x, e1, e2, st*) -> For(x, e1, e2, st*){TypeName("void")}
    where <TypeOf> x => TypeName("int")
        ; <typeof> e1 => TypeName("int")
        ; <typeof> e2 => TypeName("int")

Figure 5.4. file: til/tc/til-typecheck-var.str

module til-typecheck-var
imports til-typecheck-exp
strategies

  typecheck-declaration = 
    ?Declaration(x)
    ; rules( TypeOf+x : x -> TypeName("int") )

  typecheck-declaration = 
    ?DeclarationTyped(x, t)
    ; rules( TypeOf+x : x -> t )
 
  TypecheckVar :
    Var(x) -> Var(x){t}
    where <TypeOf> x => t

  TypecheckAssign :
    Assign(x, e) -> Assign(x, e){TypeName("void")}
    where <typeof> e => t
    	; <TypeOf> x => t
    
strategies // expressions with variables and calls

  typecheck-exp = 
    typecheck-exp(TypecheckVar <+ typecheck-funcall)
    
  typecheck-funcall = 
    TypecheckRead <+ TypecheckS2I <+ TypecheckI2S <+ TypecheckB2S
    
  typecheck-proccall =
    TypecheckWrite
	
strategies // built-in functions
 
  TypecheckS2I :
    FunCall("string2int", [e]) -> FunCall("string2int", [e]){TypeName("int")}
    where <typeof> e => TypeName("string")
    
  TypecheckI2S :
    FunCall("int2string", [e]) -> FunCall("int2string", [e]){TypeName("string")}
    where <typeof> e => TypeName("int")
    
  TypecheckB2S :
    FunCall("bool2string", [e]) -> FunCall("bool2string", [e]){TypeName("string")}
    where <typeof> e => TypeName("bool")
    
  TypecheckRead :
    FunCall("read", []) -> FunCall("read", []){TypeName("string")}
    
  TypecheckRead :
    FunCall("readint", []) -> FunCall("readint", []){TypeName("int")}

strategies // built-in procedures

  TypecheckWrite :
    ProcCall("write", [e]) -> ProcCall("write", [e]){TypeName("void")}
    where <typeof> e => TypeName("string")

  TypecheckWrite :
    ProcCall("writeint", [e]) -> ProcCall("writeint", [e]){TypeName("void")}
    where <typeof> e => TypeName("int")

5.2. Example

Figure 5.5. file: til/xmpl/typecheck-test1

# typecheck test1.til after parsing 
../tc/til-typecheck -i test1.atil | pp-aterm > test1.tc

Table 5.1. files: til/xmpl/test1.til, til/xmpl/test1.tc

beforeafter
// TIL program computing the factorial

var n;
n := readint();
var x;
var fact;
fact := 1;
for x := 1 to n do
  fact := x * fact;
end
write("factorial of ");
writeint(n);
write(" is ");
writeint(fact);
write("\n");

Program(
  [ Declaration("n")
  , Assign("n", FunCall("readint", []){TypeName("int")}){TypeName("void")}
  , Declaration("x")
  , Declaration("fact")
  , Assign("fact", Int("1"){TypeName("int")}){TypeName("void")}
  , For(
      "x"
    , Int("1"){TypeName("int")}
    , Var("n"){TypeName("int")}
    , [Assign("fact", Mul(Var("x"){TypeName("int")}, Var("fact"){TypeName("int")}){TypeName("int")}){TypeName("void")}]
    ){TypeName("void")}
  , ProcCall("write", [String("\"factorial of \""){TypeName("string")}]){TypeName("void")}
  , ProcCall("writeint", [Var("n"){TypeName("int")}]){TypeName("void")}
  , ProcCall("write", [String("\" is \""){TypeName("string")}]){TypeName("void")}
  , ProcCall("writeint", [Var("fact"){TypeName("int")}]){TypeName("void")}
  , ProcCall("write", [String("\"\\n\""){TypeName("string")}]){TypeName("void")}
  ]
)

Prev Up Next
Chapter 4. Bound Variable Renaming (*) Home Chapter 6. Interpretation