(* Source hindley.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

(*****************************)
(* Fabrication des équations *)
(******************************)

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

let
 infer env t =
   (* fabriquer les équations *)
  let ty,eqs = build env t [] in
  (* les résoudre *)
  let s = Eq.mgu eqs in
  (* Ne pas oublier d'appliquer le mgu *)
  Eq.subst_type s ty

This document was translated from LATEX by HEVEA.