User Tools

Site Tools


typecheck

This page is a draft

Type-checking imperative programs

We want to define a static analysis of IMP programs, so to guarantee that the exception TypeMismatch is never thrown at run-time.

To do that, consider a slight variation of the syntax of declarations, where constants and variables are explicitly typed.

type etype = TBool | TInt | TUnbound;;
 
type tdec =
    TEmpty
  | TConst of ide * exp * etype
  | TVar of ide * etype
  | TDseq of tdec * tdec
;;

First, it is convenient to define some auxiliary functions to manipulate a typing environment, i.e. a mapping from identifiers to types:

type tenv = TEnv of (ide -> etype);;
 
let emptytenv = TEnv (fun x -> TUnbound);;
 
let tbind (TEnv tr) x t = TEnv (fun y -> if y=x then t else tr y);;
 
let applytenv (TEnv tr) x = tr x;;

The function idetypes applied to a typed declaration d and a typing environment tr constructs a typing enviromnent, that extends tr with all the bindings found in d.

val idetypes : tdec -> tenv -> tenv = <fun>

The function typecheck_exp applied to an expression e, a typing environment tr and a type t checks if e has the type t in the environment tr. If the expression is not well-typed (e.g. because it adds a boolean to an integer, etc.), it return false.

val typecheck_exp : exp -> tenv -> etype -> bool = <fun>

The function typecheck_dec applied to a typed declaration d and a typing environment tr evaluates to true if all the initial values assigned to constants have the right type.

val typecheck_tdec : tdec -> tenv -> bool = <fun>

The function typecheck_com analyses a command, and it checks that:

  • all the values assigned to variables have the right type (i.e. the same type declared for the variable)
  • the guards of If and While statements are booleans
val typecheck_com : com -> tenv -> bool = <fun>

Summing up, typechecking a program involves the following steps:

  • constructing a typing enviroment from the (typed) declaration, and using it for:
  • typechecking the declarations, and
  • typechecking the command.
# type tprogram = TProgram of tdec * com;;
 
# let typecheck_prog (TProgram (d,c)) = 
  let tr = idetypes d emptytenv in typecheck_tdec d tr && typecheck_com c tr
;;
 
val typecheck_prog : tprogram -> bool = <fun>

As an example, the following program is well-typed:

# let tfact x = TProgram(
  TDseq(TConst (Ide "n", N x, TInt),TDseq(TVar (Ide "i", TInt),TVar (Ide "f",TInt))),
  Cseq(Cseq(Assign (Ide "i", N 1),Assign (Ide "f", N 1)),
	   While(Leq (Val (Ide "i"), Val (Ide "n")),
			 Cseq(Assign (Ide "f", Mul (Val (Ide "f"),Val (Ide "i"))), 
				  Assign (Ide "i", Add (Val (Ide "i"),N 1))))))
;;
 
# typecheck_prog (tfact 5);;
- : bool = true

Here instead is an example of a non well-typed program (the guard of the While has type TInt):

# let wrong_tfact x = TProgram(
  TDseq(TConst (Ide "n", N x, TInt),TDseq(TVar (Ide "i", TInt),TVar (Ide "f",TInt))),
  Cseq(Cseq(Assign (Ide "i", N 1),Assign (Ide "f", N 1)),
	   While(Add(N 0, Leq (Val (Ide "i"), Val (Ide "n"))),
			 Cseq(Assign (Ide "f", Mul (Val (Ide "f"),Val (Ide "i"))), 
				  Assign (Ide "i", Add (Val (Ide "i"),N 1))))))
;;
 
# typecheck_prog (wrong_tfact 5);;
- : bool = false
typecheck.txt · Last modified: 2015/10/08 15:20 (external edit)