(* Source hindley2.ml *)

open S
open Ast
open T.Type


(* Voir la documentation du module Eq, qui définit les équations,
   les substitutions etc. *)

exception Error of string

(*******************************************************)
(* Algorithme de synthèse de type simples (de hindley) *)
(* avec résolution immédiate                           *)
(*******************************************************)


let rec typeof env t s = match t with
| Num n -> Nat,s
| Var x ->
    let ty =
      try List.assoc x env
      with Not_found ->
        raise (Error ("Unbound var: "^x)) in
    ty,s
| Op (_op,t1,t2) ->
    let ty1,s = typeof env t1 s in
    let s = Eq.mgu_incr ty1 Nat s in
    let ty2,s = typeof env t2 s in
    let s = Eq.mgu_incr ty2 Nat s in
    Nat,s
| Ifz (t1,t2,t3) ->
    let ty1,s = typeof env t1 s in
    let s = Eq.mgu_incr ty1 Nat s in
    let ty2,s = typeof env t2 s in
    let ty3,s = typeof env t3 s in
    let s = Eq.mgu_incr ty2 ty3 s in
    ty3,s
| App (t1,t2) ->
    let ty1,s = typeof env t1 s in
    let ty2,s = typeof env t2 s in
    let n = Eq.fresh_var() in
    let s = Eq.mgu_incr ty1 (Arrow (ty2,Tvar n)) s in
    Tvar n,s
| Fun (x,t) ->
    let n = Eq.fresh_var () in
    let ty,s = typeof ((x,Tvar n)::env) t s in
    Arrow (Tvar n, ty),s
| Fix (x,t) ->
    let n = Eq.fresh_var () in
    let ty,s = typeof ((x,Tvar n)::env) t s in
    let s = Eq.mgu_incr (Tvar n) ty s in
    ty,s
| Let (x,t1,t2) ->
    let ty1,s = typeof env t1 s in
    typeof ((x,ty1)::env) t2 s

let infer env t =
   (* fabriquer les équations *)
  let ty,s = typeof env t Eq.id in
  (* Ne pas oublier d'appliquer le mgu *)
  Eq.subst_type s ty