(* Exercices de programmation du chapitre 1 *)

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

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

(* Substitution d'une variable x par une expression b dans une expression a *)

let rec subst a x b =
  match a with
    Var v -> if v = x then b else a
  | Const n -> a
  | Op o -> a
  | Fun(v, a1) -> if v = x then a else Fun(v, subst a1 x b)
  | App(a1, a2) -> App(subst a1 x b, subst a2 x b)
  | Paire(a1, a2) -> Paire(subst a1 x b, subst a2 x b)
  | Let(v, a1, a2) -> Let(v, subst a1 x b, if v = x then a2 else subst a2 x b)

(* La fonction partielle d'évaluation *)

let rec valeur a =
  match a with
    Const c -> Const c
  | Op o -> Op o
  | Fun(x, a) -> Fun(x, a)
  | App(a1, a2) ->
      begin match valeur a1 with
        Fun(x, a) -> valeur (subst a x (valeur a2))
      | Op "+" -> let (Paire(Const n1, Const n2)) = valeur a2 in Const(n1 + n2)
      | Op "fst" -> let (Paire(v1, v2)) = valeur a2 in v1
      | Op "snd" -> let (Paire(v1, v2)) = valeur a2 in v2
      end
  | Paire(a1, a2) -> Paire(valeur a1, valeur a2)
  | Let(x, a1, a2) -> valeur (subst a2 x (valeur a1))

(* 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 schéma = { quantif: string list; corps: exprtype }

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

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 }

(* Prédicat d'instanciation.
   typ est une instance de sch = forall a1...aN. tau
   s'il existe une substitution S sur les a1...aN telle que typ = S(tau).
   Ici, nous construisons la substitution incrémentalement 
   par récurrence sur typ et tau *)

let instance typ sch =
  let subst = ref [] in
  let rec inst t1 t2 =
    match (t1, t2) with
      (Type_base b1, Type_base b2) -> b1 = b2
    | (Type_var v, _) when List.mem v sch.quantif ->
        begin try
          List.assoc v !subst = t2
        with Not_found ->
          subst := (v, t2) :: !subst; true
        end
    | (Type_var v, Type_var v') -> v = v'
    | (Type_flèche(r1, s1), Type_flèche(r2, s2)) ->
        inst r1 r2 && inst s1 s2
    | (Type_produit(r1, s1), Type_produit(r2, s2)) ->
        inst r1 r2 && inst s1 s2
    | (_, _) -> false
  in inst sch.corps typ