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

(********** Exercice 6.1: l'algorithme d'unification ***************)

(* L'algèbre de types *)

type exprtype =
    Type_base of string
  | Type_var of string
  | Type_flèche of exprtype * exprtype
  | Type_produit of exprtype * exprtype
  | Type_enreg of exprtype
  | Type_vide                                  (* la rangée vide *)
  | Type_champ of string * exprtype * exprtype (* e : tau1; tau2 *)
  | Type_abs
  | Type_pre of exprtype

(* Représentation des substitutions par des fonctions des types dans les
   types (comme dans l'exercice 3.3) *)

(* 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)
    | Type_enreg tau -> Type_enreg(do_subst tau)
    | Type_vide -> Type_vide
    | Type_champ(étiq, tau1, tau2) ->
        Type_champ(étiq, do_subst tau1, do_subst tau2)
    | Type_abs -> Type_abs
    | Type_pre tau -> Type_pre(do_subst tau)
  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 subst c =
  List.map (fun (tau1, tau2) -> (subst tau1, subst 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
  | Type_enreg tau -> occurrence alpha tau
  | Type_vide -> false
  | Type_champ(étiq, tau1, tau2) ->
      occurrence alpha tau1 || occurrence alpha tau2
  | Type_abs -> false
  | Type_pre tau -> occurrence alpha tau

(* 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

(* 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')
  | (Type_enreg tau, Type_enreg tau') :: c' ->
      mgu((tau, tau') :: c')
  (* Unification entre rangées *)
  | (Type_vide, Type_vide) :: c' -> mgu c'
  | (Type_vide, Type_champ(étiq, tau1, tau2)) :: c' ->
      mgu((tau1, Type_abs) :: (tau2, Type_vide) :: c')
  | (Type_champ(étiq, tau1, tau2), Type_vide) :: c' ->
      mgu((tau1, Type_abs) :: (tau2, Type_vide) :: c')
  | (Type_champ(étiq, tau1, tau2), Type_champ(étiq', tau1', tau2')) :: c' ->
      if étiq = étiq' then
        mgu((tau1, tau1') :: (tau2, tau2') :: c')
      else
        let alpha = nouvelle_variable() in
        mgu((tau2, Type_champ(étiq', tau1', Type_var alpha)) ::
            (tau2', Type_champ(étiq, tau1, Type_var alpha)) :: c')
  (* Unification entre infos de présence *)
  | (Type_abs, Type_abs) :: c' -> mgu c'
  | (Type_pre tau, Type_pre tau') :: c' ->
      mgu((tau, tau') :: c')
  | _ ->
      raise Non_unifiable

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

(* La syntaxe abstraite des expressions mini-ML avec enregistrements *)

type expression =
    Var of string
  | Const of int
  | Op of string
  | Proj of string                            (* les opérateurs .étiq *)
  | Exten of string                           (* les opérateurs @ étiq *)
  | Fun of string * expression
  | App of expression * expression
  | Paire of expression * expression
  | Let of string * expression * expression
  | Enreg of (string * expression) list       (* {étiq_i = expr_i} *)

(* 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 *)

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)
  | Type_enreg t -> variables_libres t
  | Type_vide -> []
  | Type_champ(étiq, t1, t2) ->
      union (variables_libres t1) (variables_libres t2)
  | Type_abs -> []
  | Type_pre t -> variables_libres t

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) (comme dans l'exercice 3.5) *)

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) }

(* Type de l'opérateur proj_étiq *)

let type_proj étiq =
  let alpha = nouvelle_variable()
  and beta = nouvelle_variable() in
  { quantif = [alpha; beta];
    corps = Type_flèche(Type_enreg(Type_champ(étiq, Type_pre(Type_var alpha),
                                                    Type_var beta)),
                        Type_var alpha) }

(* Type de l'opérateur exten_étiq *)

let type_exten étiq =
  let alpha = nouvelle_variable()
  and beta = nouvelle_variable()
  and gamma = nouvelle_variable() in
  { quantif = [alpha; beta; gamma];
    corps = 
      Type_flèche(Type_produit(Type_enreg(Type_champ(étiq, Type_var alpha,
                                                           Type_var beta)),
                               Type_var gamma),
                  Type_enreg(Type_champ(étiq, Type_pre(Type_var gamma),
                                              Type_var beta))) }

(* 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é)
  | Proj étiq ->
      (instance_triviale(type_proj étiq), identité)
  | Exten étiq ->
      (instance_triviale(type_exten étiq), 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)
  | Enreg étiq_expr_list ->
      let (rangée, phi, _) = infer_enreg env identité étiq_expr_list in
      (Type_enreg rangée, phi)

(* Pour typer { étiq_1 = expr_1; ...; étiq_N = expr_N } :
      (tau_1, phi_1) = inférence env expr_1
      (tau_2, phi_2) = inférence (phi_1 env) expr_2 
      ...
      résultat final:
        (Type_enreg(Type_champ(étiq_1, Pre (phi_N o ... o phi_2)(tau_1),
                    Type_champ(étiq_2, Pre (phi_N o ... o phi_3)(tau_2),
                    ...
                    Type_champ(étiq_N, Pre tau_N, Type_vide)))),
         phi_N o ... o phi_1
   La fonction infer_enreg effectue ce calcul par récursion sur
   la liste [...; (étiq_i, expr_i); ...]
   Entrée: env = l'environnement substitué par psi
           psi = la composition phi_{i-1} o ... o phi_1
           étiq_expr_list = [(étiq_i, expr_i); ...; (étiq_N, expr_N)]
   Sortie: un triplet comprenant
           - la rangée Type_champ(étiq_i, Pre (phi_N o ... o phi_{i+1})(tau_i),
                                  ...
                                  Type_champ(étiq_N, Pre tau_N, Type_vide))
           - la substitution phi_i o ... o phi_1
           - la substitution phi_N o ... o phi_i
*)

and infer_enreg env psi étiq_expr_list =
  match étiq_expr_list with
    [] -> (Type_vide, psi, identité)
  | (étiq, expr) :: reste ->
      if List.mem_assoc étiq reste then raise Erreur_de_typage;
      let (tau, phi) = inférence env expr in
      let psi' = compose phi psi in
      let (rangée,  psi_finale, theta) =
            infer_enreg (subst_env phi env) psi' reste in
      (Type_champ(étiq, Type_pre (theta tau), rangée),
       psi_finale,
       compose theta phi)

(* Pour tester: (le parser et le lexer sont sur le site Web du cours) *)

#use "parser.ml";;
#use "lexer.ml";;

let parse s = (expression token (Lexing.from_string s) : expression);;

inférence [] (parse "+(1,2)");;
inférence [] (parse "let x = + in x (1,2)");;
inférence [] (parse "let id = fun x -> x in (id 1, id id)");;
inférence [] (parse "fun x -> (snd x, fst x)");;
inférence [] (parse "fun f -> f f");;
inférence [] (parse "{ a = 1; b = (fun x -> x)}");;
inférence [] (parse "{ a = 1; b = (fun x -> x)}.a");;
inférence [] (parse "{ a = 1; b = (fun x -> x)}.b");;
inférence [] (parse "{ a = 1; b = (fun x -> x)}.c");;
inférence [] (parse "fun x -> +(x.a, x.b)");;
inférence [] (parse "let f = fun x -> +(x.a, x.b) in f { b = 10; a = 1 }");;
inférence [] (parse "let f = fun x -> +(x.a, x.b) in f { b = 10 }");;
inférence [] (parse "{ a = 1 } @ { b = 2 }");;
inférence [] (parse "{ a = 1 } @ { a = (fun x -> x) }");;
inférence [] (parse "fun x -> x @ { a = 1 } @ { b = 2 }");;
*)