1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
|
(***********************************************************************)
(* *)
(* Objective Caml *)
(* *)
(* Pierre Weis, projet Cristal, INRIA Rocquencourt *)
(* *)
(* Copyright 2001 Institut National de Recherche en Informatique et *)
(* en Automatique. All rights reserved. This file is distributed *)
(* only by permission. *)
(* *)
(***********************************************************************)
type type_simple =
| Variable of variable_de_type
| Terme of string * type_simple array
and variable_de_type =
{ mutable niveau: int;
mutable valeur: valeur_d'une_variable }
and valeur_d'une_variable =
| Inconnue
| Connue of type_simple;;
type schma_de_types =
{ paramtres: variable_de_type list;
corps: type_simple };;
exception Conflit of type_simple * type_simple;;
exception Circularit of type_simple * type_simple;;
let type_int = Terme("int", [||])
and type_bool = Terme("bool", [||])
and type_flche t1 t2 = Terme("->", [|t1; t2|])
and type_produit t1 t2 = Terme("*", [|t1; t2|])
and type_liste t = Terme("list", [|t|]);;
let rec valeur_de = function
| Variable({valeur = Connue ty1} as var) ->
let valeur_de_ty1 = valeur_de ty1 in
var.valeur <- Connue valeur_de_ty1;
valeur_de_ty1
| ty -> ty;;
let test_d'occurrence var ty =
let rec test t =
match valeur_de t with
| Variable var' ->
if var == var' then raise(Circularit(Variable var, ty))
| Terme(constructeur, arguments) ->
Array.iter test arguments
in test ty;;
let rec rectifie_niveaux niveau_max ty =
match valeur_de ty with
| Variable var ->
if var.niveau > niveau_max then var.niveau <- niveau_max
| Terme(constructeur, arguments) ->
Array.iter (rectifie_niveaux niveau_max) arguments;;
let rec unifie ty1 ty2 =
let valeur1 = valeur_de ty1
and valeur2 = valeur_de ty2 in
if valeur1 == valeur2 then () else
match (valeur1, valeur2) with
| Variable var, ty ->
test_d'occurrence var ty;
rectifie_niveaux var.niveau ty;
var.valeur <- Connue ty
| ty, Variable var ->
test_d'occurrence var ty;
rectifie_niveaux var.niveau ty;
var.valeur <- Connue ty
| Terme(constr1, arguments1), Terme(constr2, arguments2) ->
if constr1 <> constr2 then
raise (Conflit(valeur1, valeur2))
else
for i = 0 to Array.length arguments1 - 1 do
unifie arguments1.(i) arguments2.(i)
done;;
let niveau_de_liaison = ref 0;;
let dbut_de_dfinition () = incr niveau_de_liaison
and fin_de_dfinition () = decr niveau_de_liaison;;
let nouvelle_inconnue () =
Variable {niveau = !niveau_de_liaison; valeur = Inconnue};;
let gnralisation ty =
let paramtres = ref [] in
let rec trouve_paramtres ty =
match valeur_de ty with
| Variable var ->
if var.niveau > !niveau_de_liaison && not (List.memq var !paramtres)
then paramtres := var :: !paramtres
| Terme(constr, arguments) ->
Array.iter trouve_paramtres arguments in
trouve_paramtres ty;
{paramtres = !paramtres; corps = ty};;
let schma_trivial ty = {paramtres = []; corps = ty};;
let spcialisation schma =
match schma.paramtres with
| [] -> schma.corps
| paramtres ->
let nouvelles_inconnues =
List.map (fun var -> (var, nouvelle_inconnue())) paramtres in
let rec copie ty =
match valeur_de ty with
| Variable var as ty ->
begin try
List.assq var nouvelles_inconnues
with Not_found ->
ty
end
| Terme(constr, arguments) ->
Terme(constr, Array.map copie arguments) in
copie schma.corps;;
let noms_des_variables = ref ([] : (variable_de_type * string) list)
and compteur_de_variables = ref 0;;
let imprime_var var =
print_string "'";
try
print_string (List.assq var !noms_des_variables)
with Not_found ->
let nom =
String.make 1
(char_of_int (int_of_char 'a' + !compteur_de_variables)) in
incr compteur_de_variables;
noms_des_variables := (var, nom) :: !noms_des_variables;
print_string nom;;
let rec imprime ty =
match valeur_de ty with
| Variable var ->
imprime_var var
| Terme(constructeur, arguments) ->
match Array.length arguments with
| 0 -> print_string constructeur
| 1 -> imprime arguments.(0);
print_string " "; print_string constructeur
| 2 -> print_string "("; imprime arguments.(0);
print_string " "; print_string constructeur;
print_string " "; imprime arguments.(1);
print_string ")"
| _ -> failwith "constructeur de type ayant trop d'arguments";;
let imprime_type ty =
noms_des_variables := [];
compteur_de_variables := 0;
imprime ty;;
let imprime_schma schma =
noms_des_variables := [];
compteur_de_variables := 0;
if schma.paramtres <> [] then begin
print_string "pour tout ";
List.iter (fun var -> imprime_var var; print_string " ")
schma.paramtres;
print_string ", "
end;
imprime schma.corps;;
|
