(*** Exercice 1 ***) (* Types for types :P *) type ty = TyNat | TyBool exception TyErr of string;; let ty_to_string ty = match ty with | TyNat -> "Nat" | TyBool -> "Bool" (* Type inference algorithm *) let rec infer_type t = match t with | TmZero -> TyNat | TmSucc u -> let subty = infer_type u in if (subty == TyNat) then TyNat else raise (TyErr (Printf.sprintf "Type error : expected Nat, got %s" (ty_to_string subty))) | TmTrue | TmFalse -> TyBool | TmIsZ u -> let subty = infer_type u in if (subty == TyNat) then TyBool else raise (TyErr (Printf.sprintf "Type error : expected Nat, got %s" (ty_to_string subty))) | TmIf (i,th,el) -> let ifty = infer_type i in let thty = infer_type th in let elty = infer_type el in if (ifty == TyBool) then if (thty == elty) then elty else raise (TyErr (Printf.sprintf "Type error : expected %s, got %s" (ty_to_string thty) (ty_to_string elty))) else raise (TyErr (Printf.sprintf "Type error : expected Bool, got %s" (ty_to_string ifty)));; (* Typed derivation tree *) let typed_derivation_tree t = let term_type_string t = (term_to_string t)^":" ^(vio_string (ty_to_string (deduce_type t))) in let rec typed_derivation_tree_int t = match t with | TmZero | TmTrue | TmFalse -> "\\AxiomC{}\n" ^(leftlabel "Ax") ^"\\UnaryInfC{" ^(term_type_string t)^"}\n" | TmSucc u -> (typed_derivation_tree_int u) ^(leftlabel "Succ") ^"\\UnaryInfC{"^(term_type_string t)^"}\n" | TmIsZ u -> (typed_derivation_tree_int u) ^(leftlabel "IsZero") ^"\\UnaryInfC{"^(term_type_string t)^"}\n" | TmIf(i,u,e) -> (typed_derivation_tree_int i) ^(typed_derivation_tree_int u) ^(typed_derivation_tree_int e) ^(leftlabel "If") ^"\\TrinaryInfC{"^(term_type_string t)^"}\n" in "\\begin{prooftree}\n\sffamily\n" ^(typed_derivation_tree_int t) ^"\\end{prooftree}\n";; (*** Exercice 2 ***)