(* Source poly.ml *)
open S.
Ast (* Termes non-typés *)
open T.
Type (* Types *)
(* Documentation du module Eq *)
(* Petite abréviation *)
module V =
Eq.
Vars (* Documentation du module Eq.Vars *)
(***************************************)
(* Divers calculs des variables libres *)
(***************************************)
(* Dans un type *)
let rec free t =
match t with
|
Tvar n ->
V.
singleton n
|
Nat ->
V.
empty
|
Arrow (
t1,
t2) ->
V.
union (
free t1) (
free t2)
(* Dans un schéma de type *)
let free_scheme (
xs,
t) =
V.
diff (
free t) (
V.
of_list xs)
(* Dans un environnement de typage *)
let free_env env =
List.
fold_right
(
fun (
_,
sc)
r ->
V.
union (
free_scheme sc)
r)
env V.
empty
(*****************************************)
(* Diverses applications de substitution *)
(*****************************************)
(* À un schéma de type: on suppose que le support de s et vs sont disjoints *)
let subst_scheme s (
xs,
t) =
assert (
V.
disjoint (
Eq.
dom s) (
V.
of_list xs)) ;
(* Ce qui simplifie beaucoup... *)
xs,
Eq.
subst_type s t
(* Application d'une substitution à un environnement *)
let subst_env s env =
List.
map (
fun (
x,
sc) ->
x,
subst_scheme s sc)
env
(****************************************)
(* Instance fraîche d'un schéma de type *)
(****************************************)
(* Fabriquer une substitution qui associe des variables fraîches aux
variables de la liste xs *)
let subst_fresh xs =
List.
fold_right (
fun x r ->
Eq.
comp
(
Eq.
delta x (
Tvar (
Eq.
fresh_var ())))
r)
xs Eq.
id
let freshen (
xs,
t) =
Eq.
subst_type (
subst_fresh xs)
t
(************************************************)
(* Généralisation d'un type en un schéma de type *)
(************************************************)
(* Assez sportif (pas de renommage), mais ils semble
que cela fonctionne.
1. La prise d'instance n'est en rien influencée le nom
exact des xs (freshen ci-dessus)
2. La substitution dans un schéma (subst_scheme)
semble également correcte, car les variables quantifiée
sont justement absentes de l'environnement *)
let generalize env t =
let xs =
V.
elements (
V.
diff (
free t) (
free_env env))
in
xs,
t
(***************************)
(* Inféreur proprement dit *)
(***************************)
exception Error of string
let rec typeof s env t =
match t with
(* Plus que facile *)
|
Num _ ->
Nat,
s
(* Pour l'application voir ci-après *)
|
App (
t1,
t2) ->
typeof_app (
typeof s env t1)
env t2
(* Les deux cas suivants sont des cas particuliers d'application *)
|
Op (
_,
t1,
t2) ->
let t_op =
Arrow (
Nat,
Arrow (
Nat,
Nat))
in
let r =
typeof_app (
t_op,
s)
env t1 in
typeof_app r env t2
|
Ifz (
t1,
t2,
t3) ->
let t_if =
(* Type d'une occurrence d'une hypothétique fonction
ifz : \forall A [Nat -> A -> A] *)
let tv =
Tvar (
Eq.
fresh_var ())
in
Arrow (
Nat,
Arrow (
tv,
Arrow (
tv,
tv)))
in
let r =
typeof_app (
t_if,
s)
env t1 in
let r =
typeof_app r env t2 in
typeof_app r env t3
(* Pas grand chose à remarquer si ce n'est que env est étendu *)
|
Fun (
x,
t1) ->
let tyx =
Tvar (
Eq.
fresh_var ())
in
let ty1,
s =
typeof s ((
x,([],
tyx))::
env)
t1 in
Arrow (
tyx,
ty1),
s
(* Par l'opérateur de pt fixe Y: \forall A [(A -> A) -> A] *)
|
Fix (
x,
t) ->
let t_fix =
let tv =
Eq.
fresh_var ()
in
Arrow (
Arrow (
Tvar tv,
Tvar tv),
Tvar tv)
in
typeof_app (
t_fix,
s)
env (
Fun (
x,
t))
(* Tout le polymorphisme est là, voir aussi freshen et generalize *)
|
Let (
x,
t1,
t2) ->
let ty1,
s =
typeof s env t1 in
let sc1 =
generalize (
subst_env s env) (
Eq.
subst_type s ty1)
in
typeof s ((
x,
sc1)::
env)
t2
|
Var x ->
let sc =
try List.
assoc x env
with Not_found ->
raise (
Error (
"Unbound var: "^
x))
in
freshen sc,
s
(* Traitement de l'application, seul cas de résolution. *)
and typeof_app (
ty_fun,
s)
env t =
(* t_fun,s est le type de la fonction *)
let ty_arg,
s =
typeof s env t in (* typer l'argument *)
let ty_res =
Tvar (
Eq.
fresh_var ())
in
let s =
(* ajouter l'équation ty_fun = ty_arg -> ty_res *)
Eq.
mgu_incr ty_fun (
Arrow (
ty_arg,
ty_res))
s in
ty_res,
s
(***********************)
(* Fonctions exportées *)
(***********************)
(* Typer dans un environnement vide *)
let infer t =
let ty,
s =
typeof Eq.
id []
t in
Eq.
subst_type s ty
let verbose =
List.
mem "-v" (
Array.
to_list Sys.
argv)
(* Pour la boucle interactive *)
let infer_scheme env t =
let ty,
s =
typeof Eq.
id env t in
let ty =
Eq.
subst_type s ty in
(* Généralisaton de toutes les variables de t,
correct si env ne contient aucune variable libre,
ce qui est le cas si les schema de types de env
sont ainsi genéralisés. *)
let xs =
free ty in
assert (
V.
disjoint (
free_env env)
xs) ;
V.
elements xs,
ty
(* Tests...
# Élémentaire
Let x = 1;;
Let y = 1+3;;
Let z = x+y;;
;;
# fonctions
Let id = Fun x -> x;;
Let k1 = Fun x -> Fun y -> y;;
Let k2 = Fun x -> Fun y -> x;;
Let plus = Fun x -> Fun y -> x+y;;
# if + fonctions
Let if1 = Fun x -> Fun y -> Ifz x Then y Else x;;
Let if2 = Fun x -> Fun y -> Ifz x Then x Else y;;
Let if3 = Fun x -> Fun y -> Fun z -> Ifz x Then y Else z;;
Let f1 = Fun x -> Fun y -> x+0 In
Let f2 = Fun x -> Fun y -> y+0 In
Fun z -> Ifz z Then f1 Else f2
;;
# fonctions plus méchant
Let t = Fun t -> Fun f -> t;;
Let f = Fun t -> Fun f -> f;;
Let not = Fun b -> Fun kt -> Fun kf -> b kf kt;;
Let and = Fun b1 -> Fun b2 ->
Fun kt -> Fun kf ->
b1 (b2 kt kf) kf;;
let or = Fun b1 -> Fun b2 -> not (and (not b1) (not b2)) ;;
# Doit avoir le type de f
Let b = and f (or t (or f f));;
# Généralisation
Let test_gen1 = Fun x -> Let y = x in y;;
Let test_gen2 =
Let id = Fun x -> x In
id id id id id
# Et encore
Let app = Fun f -> Fun x -> f x;;
let app1 = fun x ->
let g = fun y -> x y in
g;;
Let app2 = Fun f ->
Let g = Fun x -> f x In
Let h = Fun x -> g x In
h;;
Let x = 1 In Fun f -> Fun z -> f x z;;
# Quelques pt. fixes
Let Rec pow = Fun n -> Ifz n Then 1 Else 2 * pow (n-1);;
Let Rec loop = loop;;
Let Rec loop2 = Fun x -> loop2 x;;
Let Rec loop3 = Fun x -> loop3 (x+x);;
Let Rec loop4 = Fun x -> loop4 (loop4 (x+x));;
# Ne doit pas typer
Let Rec f = Fun x -> Ifz x Then 0 Else f+1;;
# Casse tout
Let pair = Fun x -> Fun y -> Fun p -> p x y In
Let x0 = Fix x -> x In
Let x1 = pair x0 x0 In
Let x2 = pair x1 x1 In
Let x3 = pair x2 x2 In
Let x4 = pair x3 x3 In
Let x5 = pair x4 x4 In
Let x6 = pair x5 x5 In
Let x7 = pair x6 x6 In
Let x8 = pair x7 x7 In
Let x9 = pair x8 x8 In
x9
;;
*)
This document was translated from LATEX by
HEVEA.