(*** Exercice 1 ***) (*** Exercice 2 ***) (*************************************************************) (* Simple grammar for types, all beginning with Ty. *) (*************************************************************) type ty = | TyBool | TyNat | TyArr of ty * ty | TyId of string (* Exception for error handling *) exception Exn of string (*************************************************************) (* Simple grammar for terms, all beginning with Tm. *) (*************************************************************) type term = | TmTrue | TmFalse | TmZero | TmSucc of term | TmIf of term * term * term * ty (* Typed condition *) | TmIfU of term * term * term (* Untyped condition *) | TmVar of string * ty (* Typed variable *) | TmVarU of string (* Untyped variable *) | TmAbs of string * ty * term (* Typed abstraction *) | TmAbsU of string * term (* Untyped abstraction *) | TmApp of term * term (* Application *) type context = Ctx of (string * ty) list type constraints = Con of (ty * ty) list (*************************************************************) (* Helper functions *) (*************************************************************) (* Mostly, these functions convert the values into strings that can be displayed. *) let red_string s = "\x1B[31;1m"^s^"\x1B[0m" let blue_string s = "\x1B[34;1m"^s^"\x1B[0m" let bold_string s = "\x1B[1m"^s^"\x1B[0m " let rec ty_to_string t = match t with | TyBool -> "Bool" | TyNat -> "Nat" | TyArr (x,y) -> "("^(ty_to_string x)^" -> "^(ty_to_string y)^")" | TyId s -> red_string s let rec term_to_string t = match t with | TmTrue -> "T" | TmFalse -> "F" | TmZero -> "0" | TmSucc t -> (bold_string "S")^(term_to_string t) | TmIf (i,t,e,ty) -> (bold_string "if")^(term_to_string i)^ " : Bool "^(bold_string "then")^(term_to_string t)^ " : "^(ty_to_string ty)^" "^(bold_string "else")^ (term_to_string e)^" : "^(ty_to_string ty) | TmIfU (i,t,e) -> "if ("^(term_to_string i)^ ") then "^(term_to_string t)^" else "^(term_to_string e) | TmVar (s,t) -> (blue_string s)^" : "^(ty_to_string t) | TmVarU s -> blue_string s | TmAbs (v,t,e) -> "( "^(bold_string "λ")^(blue_string v)^ " : "^(ty_to_string t)^ " . "^(term_to_string e)^" )" | TmAbsU (v,e) -> "( "^(bold_string "λ")^v^" . "^ (term_to_string e)^" )" | TmApp (a,b) -> (term_to_string a)^" "^(term_to_string b) let context_to_string (Ctx c) = Printf.printf "--- Context : \n"; List.iter (fun (s,t) -> Printf.printf "%s : %s" s (ty_to_string t)) c; Printf.printf "--------------------------\n";; let constraints_to_string (Con c) = Printf.printf "--- Constraints : \n"; List.iter (fun (s,t) -> Printf.printf ". %s = %s\n" (ty_to_string s) (ty_to_string t)) c;; (*************************************************************) (* Fresh variable names generator - with imperative features inside. A function that, each time it is called, returns a new variable name. *) (*************************************************************) let fresh_var_name_gen = let x = ref 0 in let rec gen_rec () = incr x; "X_"^(string_of_int !x) in gen_rec;; let gen = fresh_var_name_gen;; (* shorter name *) (*************************************************************) (* Constraints inference *) (*************************************************************) (* The algorithm follows the exercise from the Pierce. Arguments : - a context (possibly empty, at least at the beginning), - and a term. It returns : - a type, - a list of constraints - and an equivalent term that is typed. *) let rec compute_constraints (Ctx ct:context) (t:term) = match t with | TmTrue -> (TyBool, Con [], t) | TmFalse -> (TyBool, Con [], t) | TmZero -> (TyNat, Con [], t) | TmSucc u -> let (nt, Con ncon, _) = compute_constraints (Ctx ct) u in (TyNat, Con ((nt, TyNat)::ncon), t) | TmVar (s,ty) -> (ty, Con [], t) | TmVarU s -> begin try let nt = List.assoc s ct in (nt, Con [], TmVar(s, nt)) with Not_found -> let newty = TyId (gen()) in (newty, Con [], TmVar(s, newty)) end | TmIf (i,t,e,ty) -> let (ni, Con icon, _) = compute_constraints (Ctx ct) i in let (nt, Con tcon, _) = compute_constraints (Ctx ct) t in let (ne, Con econ, _) = compute_constraints (Ctx ct) e in (nt, Con ((ni, TyBool)::(nt, ne)::(ty,nt)::(icon@tcon@econ)), t) | TmIfU (i,t,e) -> let (ni, Con icon, _) = compute_constraints (Ctx ct) i in let (nt, Con tcon, _) = compute_constraints (Ctx ct) t in let (ne, Con econ, _) = compute_constraints (Ctx ct) e in (nt, Con ((ni, TyBool)::(nt, ne)::(icon@tcon@econ)), TmIf (i,t,e,nt)) | TmAbs (x,ty,e) -> let (nt, Con ncon, te) = compute_constraints (Ctx ((x,ty)::ct)) e in (TyArr (ty,nt), Con ncon, TmAbs (x,ty,te)) | TmAbsU (x,e) -> let newty = TyId (gen()) in let (nt, Con ncon, te) = compute_constraints (Ctx ((x,newty)::ct)) e in let resty = TyArr (newty,nt) in (resty, Con ncon, TmAbs(x,resty,te)) | TmApp (a,b) -> let (na, Con acon, ta) = compute_constraints (Ctx ct) a in let (nb, Con bcon, tb) = compute_constraints (Ctx ct) b in let newty = TyId (gen()) in (newty, Con ((na, TyArr (nb, newty))::(acon@bcon)), t) (*************************************************************) (* Helper functions on type transformations *) (*************************************************************) (* Types transformation functions *) (* Apply a transformation on a list of constraints or a context *) let apply_simple_constraints_transform cl (f:ty -> ty) = List.map (fun (u,v) -> (f u,f v)) cl;; (* Apply a recursive renaming to a type. May not terminate *) let rec apply_rename (f:ty -> ty) (t:ty) = match t with | TyBool -> TyBool | TyNat -> TyNat | TyId i -> let fi = f (TyId i) in if (fi = TyId i) then TyId i else apply_rename f fi | TyArr (a,b) -> TyArr (apply_rename f a, apply_rename f b);; (* Apply recursive transformation on a list of constraints or a context. May not terminate. *) let apply_constraints_transform cl (f:ty -> ty) = List.map (fun (u,v) -> (apply_rename f u, apply_rename f v)) cl;; (* Create a simple transformation mapping a variable into a term *) let simple_transform s t = let f x = if (x = TyId s) then t else x in f;; (* Computation of the free variables in a term *) let rec belongs_to (s:string) (t:ty) = match t with | TyBool -> false | TyNat -> false | TyId i -> (i=s) | TyArr (a,b) -> (belongs_to s a) || (belongs_to s b);; let rec free_vars t = match t with | TyBool -> [] | TyNat -> [] | TyId i -> [TyId i] | TyArr (a,b) -> (free_vars a) @ (free_vars b);; (* Remove doubles from a list, terminal recursive version *) let uniq_list (l:'a list) = let rec uniq_rec m r = match m with | [] -> List.rev r | [x] -> List.rev (x::r) | x::y::xs -> if (x = y) then uniq_rec (y::xs) r else uniq_rec (y::xs) (x::r) in uniq_rec (List.sort compare l) [];; (* Get the list of free variables in a list of constraints *) let constraint_free_vars (Con c) = let fv = List.fold_left (fun l (u,v) -> (free_vars u)@(free_vars v)@l) [] c in uniq_list fv;; (* Compute the fixed point of the transformation f *) let fixed_point (f:ty -> ty) = let rec g x = if (f x = x) then x else g (f x) in g;; (*************************************************************) (* Unification part *) (*************************************************************) (* Takes a list of constraints and returns a function on types *) let compute_unification (Con cs) = let f (x : ty) = x in let rec compute_rec l g = match l with | [] -> g | (s,t)::cs -> begin if s = t then compute_rec cs g else match (s,t) with | (TyId ss, _) -> if (not(belongs_to ss t)) then let tr = simple_transform ss t in compute_rec (apply_simple_constraints_transform cs tr) (fun x -> g (tr x)) else raise (Exn "Impossible to unify") | (_, TyId tt) -> if (not(belongs_to tt s)) then let tr = simple_transform tt s in compute_rec (apply_simple_constraints_transform cs tr) (fun x -> g (tr x)) else raise (Exn "Impossible to unify") | (TyArr(s1,s2),TyArr(t1,t2)) -> compute_rec ((s1,t1)::(s2,t2)::cs) g | _ -> raise (Exn (Printf.sprintf "Cannot unify %s with %s" (ty_to_string s) (ty_to_string t))) end in fixed_point (compute_rec cs f);; (*************************************************************) (* Final diagnostic function *) (*************************************************************) let display_inference (t:term) = Printf.printf "----------------------------------------------------------\n"; let (ty,Con c,nt) = compute_constraints (Ctx []) t in let unif = compute_unification (Con c) in Printf.printf "--- Term : %s\n" (term_to_string nt); Printf.printf "--- Type : %s\n" (ty_to_string ty); Printf.printf "--- Free variables : "; List.iter (fun s -> Printf.printf "(%s -> %s), " (ty_to_string s) (ty_to_string (unif s))) (constraint_free_vars (Con c)); print_newline(); constraints_to_string (Con c); Printf.printf "--- After unification "; constraints_to_string (Con (apply_constraints_transform c unif)); Printf.printf "--- Inferred type : %s\n" (ty_to_string (apply_rename unif ty));; (*********************) (* Examples of terms *) (*********************) let rec int_to_term n = if (n == 0) then TmZero else TmSucc (int_to_term (n-1));; let terms = [ TmSucc (TmZero); ];; let untypable_terms = [ (* TmIfU (TmTrue, (int_to_term 1), TmFalse); *) ];; (*************************************************************) (* Main *) (*************************************************************) let main = print_string (bold_string "Tests OK :\n"); List.iter display_inference terms; print_string (bold_string "\nTests KO :\n"); List.iter (fun t -> try display_inference t with Exn s -> Printf.printf "!!! Inference failed : %s\n" s) untypable_terms;; let f0 = fun x -> (x,x) in let f1 = fun y -> f0 (f0 y) in let f2 = fun y -> f1 (f1 y) in let f3 = fun y -> f2 (f2 y) in let f4 = fun y -> f3 (f3 y) in let f5 = fun y -> f4 (f4 y) in f5 (fun z -> z) (*** Exercice 3 ***) let zero = 0;; let succ x = x+1;; let is_zero x = (x = 0);; let empty = [];; (* the empty list *) let cons x e = x::e;; (* cons of a head and a tail *) let is_empty l = (l = []);; (* tests if a list is empty or not *) let head l = List.hd l;; (* returns the first element of a list *) let tail l = List.tl l;; (* returns the list deprived from its head *) cons 1 (cons 2 (cons 3 empty));; (* the list [1;2;3] *)