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
|
(***********************************************************************)
(* *)
(* 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. *)
(* *)
(***********************************************************************)
open Syntaxe;;
open Types;;
type environnement = (string * schma_de_types) list;;
exception Erreur of string;;
let rec type_motif env = function
| Motif_variable id ->
let ty = nouvelle_inconnue() in
(ty, (id, schma_trivial ty) :: env)
| Motif_boolen b ->
(type_bool, env)
| Motif_nombre n ->
(type_int, env)
| Motif_paire(m1, m2) ->
let (ty1, env1) = type_motif env m1 in
let (ty2, env2) = type_motif env1 m2 in
(type_produit ty1 ty2, env2)
| Motif_nil ->
(type_liste (nouvelle_inconnue()), env)
| Motif_cons(m1, m2) ->
let (ty1, env1) = type_motif env m1 in
let (ty2, env2) = type_motif env1 m2 in
unifie (type_liste ty1) ty2;
(ty2, env2);;
let rec type_exp env = function
| Variable id ->
begin try spcialisation (List.assoc id env)
with Not_found -> raise (Erreur (id ^ " est inconnu"))
end
| Fonction liste_de_cas ->
let type_argument = nouvelle_inconnue()
and type_rsultat = nouvelle_inconnue() in
let type_cas (motif, expr) =
let (type_motif, env_tendu) = type_motif env motif in
unifie type_motif type_argument;
let type_expr = type_exp env_tendu expr in
unifie type_expr type_rsultat in
List.iter type_cas liste_de_cas;
type_flche type_argument type_rsultat
| Application(fonction, argument) ->
let type_fonction = type_exp env fonction in
let type_argument = type_exp env argument in
let type_rsultat = nouvelle_inconnue() in
unifie type_fonction (type_flche type_argument type_rsultat);
type_rsultat
| Let(df, corps) -> type_exp (type_df env df) corps
| Boolen b -> type_bool
| Nombre n -> type_int
| Paire(e1, e2) -> type_produit (type_exp env e1) (type_exp env e2)
| Nil -> type_liste (nouvelle_inconnue())
| Cons(e1, e2) ->
let type_e1 = type_exp env e1 in
let type_e2 = type_exp env e2 in
unifie (type_liste type_e1) type_e2;
type_e2
and type_df env df =
dbut_de_dfinition();
let type_expr =
match df.rcursive with
| false -> type_exp env df.expr
| true ->
let type_provisoire = nouvelle_inconnue() in
let type_expr =
type_exp ((df.nom, schma_trivial type_provisoire) :: env)
df.expr in
unifie type_expr type_provisoire;
type_expr in
fin_de_dfinition();
(df.nom, gnralisation type_expr) :: env;;
|
