User Tools

Site Tools


typecheck

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

typecheck [2015/10/08 15:20] (current)
Line 1: Line 1:
 +<note warning>​This page is a draft</​note>​
  
 +====== 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.
 +
 +<code ocaml>
 +type etype = TBool | TInt | TUnbound;;
 +
 +type tdec =
 +    TEmpty
 +  | TConst of ide * exp * etype
 +  | TVar of ide * etype
 +  | TDseq of tdec * tdec
 +;;
 +</​code>​
 +
 +First, it is convenient to define some auxiliary functions to manipulate a //typing environment//,​
 +i.e. a mapping from identifiers to types:
 +<code ocaml>
 +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;;
 +</​code>​
 +
 +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''​. ​
 +<code ocaml>
 +val idetypes : tdec -> tenv -> tenv = <fun>
 +</​code>​
 +
 +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''​.  ​
 +<code ocaml>
 +val typecheck_exp : exp -> tenv -> etype -> bool = <fun>
 +</​code>​
 +
 +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.
 +<code ocaml>
 +val typecheck_tdec : tdec -> tenv -> bool = <fun>
 +</​code>​
 +
 +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
 +
 +<code ocaml>
 +val typecheck_com : com -> tenv -> bool = <fun>
 +</​code>​
 +
 +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.
 +
 +<code ocaml>
 +# 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>
 +</​code>​
 +
 +As an example, the following program is well-typed:
 +<code ocaml>
 +# 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
 +</​code>​
 +
 +Here instead is an example of a non well-typed program (the guard of the ''​While''​ has type ''​TInt''​):​
 +
 +<code ocaml>
 +# 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
 +</​code>​
typecheck.txt ยท Last modified: 2015/10/08 15:20 (external edit)