(* 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)::env) t2
| App (t1, t2) ->
    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)::env) t in
    Arrow (tx,ty)
| Fix (x,tx,t) ->
    let ty = check ((x,tx)::env) t 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")