(* Corrigé des exercices de programmation du chapitre 3 *)

(********** Exercice 3.1: propagation des types pour ML monomorphe *********)

(* L'algèbre de types (comme au chapitre 1) *)

type exprtype =
    Type_base of string
  | Type_var of string
  | Type_flèche of exprtype * exprtype
  | Type_produit of exprtype * exprtype

(* La syntaxe abstraite des expressions mini-ML avec annotation de type
   sur les paramètres des "fun" *)

type expression =
    Var of string
  | Const of int
  | Op of string
  | Fun of string * exprtype * expression
  | App of expression * expression
  | Paire of expression * expression
  | Let of string * expression * expression

(* Type des opérateurs (monomorphes) *)

let type_opérateur op =
  match op with
    "+" | "-" | "*" | "/" ->
      Type_flèche(Type_produit(Type_base "int", Type_base "int"),
                  Type_base "int")
  | "fix" ->
      let int_f_int = Type_flèche(Type_base "int", Type_base "int") in
      Type_flèche(Type_flèche(int_f_int, int_f_int), int_f_int)
  | "ifzero" ->
      Type_flèche(Type_produit(Type_base "int",
                               Type_produit(Type_base "int", Type_base "int")),
                  Type_base "int")

(* La fonction de propagation de types *)

exception Erreur_de_type

let rec type_de env a =
  match a with
    Var x -> List.assoc x env
  | Const c -> Type_base "int"
  | Op op -> type_opérateur op
  | Fun(x, tau, b) -> Type_flèche(tau, type_de ((x, tau) :: env) b)
  | App(b, c) ->
      begin match type_de env b with
        Type_flèche(ty_arg, ty_rés) ->
          if ty_arg = type_de env c then ty_rés else raise Erreur_de_type
      | _ -> raise Erreur_de_type
      end
  | Paire(b, c) -> Type_produit(type_de env b, type_de env c)
  | Let(x, b, c) ->
      let ty_b = type_de env b in
      type_de ((x, ty_b) :: env) c

(****************** Exercice 3.2: construction de C(a) *********************)

(* La syntaxe abstraite des expressions mini-ML (comme au chapitre 1) *)

type expression =
    Var of string
  | Const of int
  | Op of string
  | Fun of string * expression
  | App of expression * expression
  | Paire of expression * expression
  | Let of string * expression * expression

(* Génération de nouvelles variables de types a1, a2, a3, ... *)

let compteur_de_variables = ref 0

let nouvelle_variable() =
  incr compteur_de_variables;
  "a" ^ string_of_int !compteur_de_variables

(* Associer de nouvelles variables de type à chaque identificateur et
   à chaque sous-expression d'une expression *)

type identificateur_typé =
  { id : string; type_id: exprtype }

type expression_typée = 
  { descr: expression_typée_descr; type_expr: exprtype }

and expression_typée_descr =
    TVar of identificateur_typé
  | TConst of int
  | TOp of string
  | TFun of identificateur_typé * expression_typée
  | TApp of expression_typée * expression_typée
  | TPaire of expression_typée * expression_typée
  | TLet of identificateur_typé * expression_typée * expression_typée

let rec annotation env expr =
  let descr =
    match expr with
      Var x -> TVar(List.assoc x env)
    | Const c -> TConst c
    | Op op -> TOp op
    | Fun(x, a) ->
        let tx = {id = x; type_id = Type_var(nouvelle_variable())} in
        TFun(tx, annotation ((x, tx) :: env) a)
    | App(a, b) ->
        TApp(annotation env a, annotation env b)
    | Paire(a, b) ->
        TPaire(annotation env a, annotation env b)
    | Let(x, a, b) ->
        let tx = {id = x; type_id = Type_var(nouvelle_variable())} in
        TLet(tx, annotation env a, annotation ((x, tx) :: env) b)
  in
    { descr = descr; type_expr = Type_var(nouvelle_variable()) }

(* Génération de l'ensemble d'équations C(a) pour une expression annotée a *)

let rec équations a =
  match a.descr with
    TVar id -> [a.type_expr, id.type_id]
  | TConst c -> [a.type_expr, Type_base "int"]
  | TOp op -> [a.type_expr, type_opérateur op]
  | TFun(id, b) ->
      (a.type_expr, Type_flèche(id.type_id, b.type_expr)) :: équations b
  | TApp(b, c) ->
      (b.type_expr, Type_flèche(c.type_expr, a.type_expr)) ::
      équations b @ équations c
  | TPaire(b, c) ->
      (a.type_expr, Type_produit(b.type_expr, c.type_expr)) ::
      équations b @ équations c
  | TLet(x, b, c) ->
      (a.type_expr, c.type_expr) ::
      (x.type_id, b.type_expr) ::
      équations b @ équations c

(******************** Exercice 3.3: unification **************************)

(* Représentation des substitutions par des fonctions des types dans les
   types *)

(* La substitution élémentaire [alpha_i <- tau_i] *)

let subst alpha_tau_list =
  let rec do_subst tau =
    match tau with
      Type_var alpha ->
        begin try
          List.assoc alpha alpha_tau_list
        with Not_found ->
          tau
        end
    | Type_base b -> tau
    | Type_flèche(tau1, tau2) -> Type_flèche(do_subst tau1, do_subst tau2)
    | Type_produit(tau1, tau2) -> Type_produit(do_subst tau1, do_subst tau2)
  in
    do_subst

(* La composition de substitutions et la substitution identité *)

let compose subst1 subst2 = fun typ -> subst1(subst2(typ))

let identité = fun typ -> typ

(* Appliquer une substitution à un ensemble d'équations entre types
   (une liste de paires de types) *)

let subst_equations sigma c =
  List.map (fun (tau1, tau2) -> (sigma tau1, sigma tau2)) c

(* Test d'occurrence d'une variable dans un type *)

let rec occurrence alpha tau =
  match tau with
    Type_base b -> false
  | Type_var beta -> alpha = beta
  | Type_flèche(tau1, tau2) -> occurrence alpha tau1 || occurrence alpha tau2
  | Type_produit(tau1, tau2) -> occurrence alpha tau1 || occurrence alpha tau2

(* Le calcul de l'unificateur principal *)

exception Non_unifiable

let rec mgu c =
  match c with
    [] -> identité
  | (Type_var alpha, Type_var beta) :: c' when alpha = beta -> mgu c'
  | (Type_var alpha, tau) :: c' when not(occurrence alpha tau) ->
      let s = subst [alpha, tau] in 
      compose (mgu(subst_equations s c')) s
  | (tau, Type_var alpha) :: c' when not(occurrence alpha tau) ->
      let s = subst [alpha, tau] in 
      compose (mgu(subst_equations s c')) s
  | (Type_base b1, Type_base b2) :: c' when b1 = b2 -> mgu c'
  | (Type_flèche(tau1, tau2), Type_flèche(tau1', tau2')) :: c' ->
      mgu((tau1, tau1') :: (tau2, tau2') :: c')
  | (Type_produit(tau1, tau2), Type_produit(tau1', tau2')) :: c' ->
      mgu((tau1, tau1') :: (tau2, tau2') :: c')
  | _ ->
      raise Non_unifiable

(******************* Exercice 3.4: l'algorithme I **************************)

type résultat = Err | Type of exprtype

let inférence_monomorphe a =
  try
    let a' = annotation [] a in
    let phi = mgu(équations a') in
    Type(phi(a'.type_expr))
  with Non_unifiable ->
    Err

(******************** Exercice 3.5: l'algorithme W ***********************)

(* Les schémas de types (comme au chapitre 1) *)

type schéma = { quantif: string list; corps: exprtype }

(* Prendre une instance triviale d'un schéma *)

let instance_triviale sigma =
  (* On génère les variables nouvelles beta1... betaN *)
  let vars_inst =
    List.map (fun alpha -> Type_var(nouvelle_variable())) sigma.quantif in
  (* On construit la substitution alphai <- betai *)
  let s = subst (List.combine sigma.quantif vars_inst) in
  (* On l'applique au corps du schéma *)
  s sigma.corps

(* Calcul des variables libres -- comme au chapitre 1 *)

let rec union l1 l2 =
  match l1 with
    [] -> l2
  | hd :: tl -> union tl (if List.mem hd l2 then l2 else hd :: l2)

let rec variables_libres t =
  match t with
    Type_base b -> []
  | Type_var v -> [v]
  | Type_flèche(t1, t2) -> union (variables_libres t1) (variables_libres t2)
  | Type_produit(t1, t2) -> union (variables_libres t1) (variables_libres t2)

let rec différence l1 l2 =
  match l1 with
    [] -> []
  | hd :: tl ->
      if List.mem hd l2 then différence tl l2 else hd :: différence tl l2

let variables_libres_schéma s =
  différence (variables_libres s.corps) s.quantif

let rec variables_libres_env env =
  match env with
    [] -> []
  | (ident, schéma) :: reste ->
      union (variables_libres_schéma schéma) (variables_libres_env reste)

(* Généralisation d'un type en un schéma *)

let généralisation typ env =
  { quantif = différence (variables_libres typ) (variables_libres_env env);
    corps = typ }

(* Appliquer une substitution à un schéma *)
(* Pour éviter les problèmes de capture de variables liées, on renomme
   toutes les variables liées dans le schéma en de nouvelles variables *)

let subst_schéma phi sigma =
  (* On génère de nouvelles variables beta1... betaN *)
  let quantif' = List.map (fun alpha -> nouvelle_variable()) sigma.quantif in
  (* On construit la substitution [alphai <- betai] o phi *)
  let psi =
    compose (subst (List.map2 (fun alpha beta -> (alpha, Type_var beta))
                              sigma.quantif quantif'))
            phi in
  (* On renvoie le schéma V betai. psi(tau) *)
  { quantif = quantif'; corps = psi sigma.corps }

(* Appliquer une substitution à un environnement *)

let subst_env phi env =
  List.map (fun (ident, schéma) -> (ident, subst_schéma phi schéma)) env

(* Type des opérateurs (polymorphes) *)

let type_opérateur op =
  match op with
    "+" | "-" | "*" | "/" ->
      { quantif = [];
        corps = Type_flèche(Type_produit(Type_base "int", Type_base "int"),
                            Type_base "int") }
  | "fix" ->
      let alpha = nouvelle_variable() in
      { quantif = [alpha];
        corps = Type_flèche(Type_flèche(Type_var alpha, Type_var alpha),
                            Type_var alpha) }
  | "fst" ->
      let alpha = nouvelle_variable() in
      let beta = nouvelle_variable() in
      { quantif = [alpha; beta];
        corps = Type_flèche(Type_produit(Type_var alpha, Type_var beta),
                            Type_var alpha) }
  | "snd" ->
      let alpha = nouvelle_variable() in
      let beta = nouvelle_variable() in
      { quantif = [alpha; beta];
        corps = Type_flèche(Type_produit(Type_var alpha, Type_var beta),
                            Type_var beta) }
  | "ifzero" ->
      let alpha = nouvelle_variable() in
      { quantif = [alpha];
        corps = Type_flèche(Type_produit(Type_base "int",
                               Type_produit(Type_var alpha, Type_var alpha)),
                            Type_var alpha) }

(* L'algorithme W *)

exception Erreur_de_typage

let rec inférence env a =
  match a with
    Var x ->
      begin try
        let schéma_x = List.assoc x env in
        (instance_triviale schéma_x, identité)
      with Not_found ->
        (* la variable x n'est pas dans le domaine de env *)
        raise Erreur_de_typage
      end
  | Const n ->
      (Type_base "int", identité)
  | Op op ->
      (instance_triviale(type_opérateur op), identité)
  | Fun(x, a1) ->
      let alpha = Type_var(nouvelle_variable()) in
      let schéma_alpha = {quantif = []; corps = alpha} in
      let (tau1, phi1) = inférence ((x, schéma_alpha) :: env) a1 in
      (Type_flèche(phi1 alpha, tau1), phi1)
  | App(a1, a2) ->
      let (tau1, phi1) = inférence env a1 in
      let (tau2, phi2) = inférence (subst_env phi1 env) a2 in
      let alpha = Type_var(nouvelle_variable()) in
      let mu = mgu [phi2 tau1, Type_flèche(tau2, alpha)] in
      (mu alpha, compose mu (compose phi2 phi1))
  | Paire(a1, a2) ->
      let (tau1, phi1) = inférence env a1 in
      let (tau2, phi2) = inférence (subst_env phi1 env) a2 in
      (Type_produit(phi2 tau1, tau2), compose phi2 phi1)
  | Let(x, a1, a2) ->
      let (tau1, phi1) = inférence env a1 in
      let phi1_env = subst_env phi1 env in
      let sigma_x = généralisation tau1 phi1_env in
      let (tau2, phi2) = inférence ((x, sigma_x) :: phi1_env) a2 in
      (tau2, compose phi2 phi1)

(* Pour tester:
inférence [] (App(Op "+", Paire(Const 1, Const 2)));;
inférence [] (Let("x", Op "+", App(Var "x", Paire(Const 1, Const 2))));;
inférence [] (Let("id", Fun("x", Var "x"),
                  Paire(App(Var "id", Const 1), App(Var "id", Var "id"))));;
inférence [] (Fun("x", Paire(App(Op "snd", Var "x"), App(Op "fst", Var "x"))));;
inférence [] (Fun("f", App(Var "f", Var "f")));;
*)