(* 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
This document was translated from LATEX by
HEVEA.