(* 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)::
env)
t k in
Arrow (
Tvar n,
ty),
k
|
Fix (
x,
t) ->
let n =
Eq.
fresh_var ()
in
let ty,
k =
build ((
x,
Tvar n)::
env)
t k in
ty,((
Tvar n,
ty)::
k)
|
Let (
x,
t1,
t2) ->
let ty1,
k =
build env t1 k in
build ((
x,
ty1)::
env)
t2 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.