(* Source check.ml *)
open T
open
 Type
open
 Ast

exception
 Error of string

(* L'écriture du code est relativement mécanique, à partir des règles du cours *)

let rec check env t = match t with
Num _ -> Nat
Var x ->
    begin
      try List.assoc x env with
      | Not_found -> raise (Error ("Variable inconnue: "^x))
 (* Bonne idée de changer Not_found en une exception plus spécifique *)
    end
Op (_,t1,t2) ->
    check_nat env t1 ; (* Voir ci-après *)
    check_nat env t2 ;
    Nat
Ifz (t1,t2,t3) ->
    check_nat env t1 ;
    let tt2 = check env t2
    and tt3 = check env t3 in
    if tt2 <> tt3 then raise (Error "Same") ;
    tt3
Let (x,t1,t2) ->
    let ty1 = check env t1 in
    check ((x,ty1)::envt2
App (t1t2) ->
    let ty1,ty2 = check_fun env t1
    and ty3 = check env t2 in
    if ty1 <> ty3 then raise (Error "App") ;
    ty2
Fun (x,tx,t) ->
    let ty = check ((x,tx)::envt in
    Arrow (tx,ty)
Fix (x,tx,t) ->
    let ty = check ((x,tx)::envt in
    if tx <> ty then raise (Error "Fix") ;
    tx

(* Noter l'usage de fonctions auxiliaires pour traiter
   les cas qui surviennent plusieurs fois *)


and check_nat env t = match check env t with
Nat -> ()
_   -> raise (Error "Nat")

and check_fun env t =  match check env t with
Arrow (ty1,ty2) -> ty1,ty2
_ -> raise (Error "Arrow")

This document was translated from LATEX by HEVEA.