forked from esumii/min-caml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
typing.ml
163 lines (155 loc) · 6.24 KB
/
typing.ml
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
(* type inference/reconstruction *)
open Syntax
exception Unify of Type.t * Type.t
exception Error of t * Type.t * Type.t
let extenv = ref M.empty
(* for pretty printing (and type normalization) *)
let rec deref_typ = function (* 型変数を中身でおきかえる関数 (caml2html: typing_deref) *)
| Type.Fun(t1s, t2) -> Type.Fun(List.map deref_typ t1s, deref_typ t2)
| Type.Tuple(ts) -> Type.Tuple(List.map deref_typ ts)
| Type.Array(t) -> Type.Array(deref_typ t)
| Type.Var({ contents = None } as r) ->
Format.eprintf "uninstantiated type variable detected; assuming int@.";
r := Some(Type.Int);
Type.Int
| Type.Var({ contents = Some(t) } as r) ->
let t' = deref_typ t in
r := Some(t');
t'
| t -> t
let rec deref_id_typ (x, t) = (x, deref_typ t)
let rec deref_term = function
| Not(e) -> Not(deref_term e)
| Neg(e) -> Neg(deref_term e)
| Add(e1, e2) -> Add(deref_term e1, deref_term e2)
| Sub(e1, e2) -> Sub(deref_term e1, deref_term e2)
| Eq(e1, e2) -> Eq(deref_term e1, deref_term e2)
| LE(e1, e2) -> LE(deref_term e1, deref_term e2)
| FNeg(e) -> FNeg(deref_term e)
| FAdd(e1, e2) -> FAdd(deref_term e1, deref_term e2)
| FSub(e1, e2) -> FSub(deref_term e1, deref_term e2)
| FMul(e1, e2) -> FMul(deref_term e1, deref_term e2)
| FDiv(e1, e2) -> FDiv(deref_term e1, deref_term e2)
| If(e1, e2, e3) -> If(deref_term e1, deref_term e2, deref_term e3)
| Let(xt, e1, e2) -> Let(deref_id_typ xt, deref_term e1, deref_term e2)
| LetRec({ name = xt; args = yts; body = e1 }, e2) ->
LetRec({ name = deref_id_typ xt;
args = List.map deref_id_typ yts;
body = deref_term e1 },
deref_term e2)
| App(e, es) -> App(deref_term e, List.map deref_term es)
| Tuple(es) -> Tuple(List.map deref_term es)
| LetTuple(xts, e1, e2) -> LetTuple(List.map deref_id_typ xts, deref_term e1, deref_term e2)
| Array(e1, e2) -> Array(deref_term e1, deref_term e2)
| Get(e1, e2) -> Get(deref_term e1, deref_term e2)
| Put(e1, e2, e3) -> Put(deref_term e1, deref_term e2, deref_term e3)
| e -> e
let rec occur r1 = function (* occur check (caml2html: typing_occur) *)
| Type.Fun(t2s, t2) -> List.exists (occur r1) t2s || occur r1 t2
| Type.Tuple(t2s) -> List.exists (occur r1) t2s
| Type.Array(t2) -> occur r1 t2
| Type.Var(r2) when r1 == r2 -> true
| Type.Var({ contents = None }) -> false
| Type.Var({ contents = Some(t2) }) -> occur r1 t2
| _ -> false
let rec unify t1 t2 = (* 型が合うように、型変数への代入をする (caml2html: typing_unify) *)
match t1, t2 with
| Type.Unit, Type.Unit | Type.Bool, Type.Bool | Type.Int, Type.Int | Type.Float, Type.Float -> ()
| Type.Fun(t1s, t1'), Type.Fun(t2s, t2') ->
(try List.iter2 unify t1s t2s
with Invalid_argument(_) -> raise (Unify(t1, t2)));
unify t1' t2'
| Type.Tuple(t1s), Type.Tuple(t2s) ->
(try List.iter2 unify t1s t2s
with Invalid_argument(_) -> raise (Unify(t1, t2)))
| Type.Array(t1), Type.Array(t2) -> unify t1 t2
| Type.Var(r1), Type.Var(r2) when r1 == r2 -> ()
| Type.Var({ contents = Some(t1') }), _ -> unify t1' t2
| _, Type.Var({ contents = Some(t2') }) -> unify t1 t2'
| Type.Var({ contents = None } as r1), _ -> (* 一方が未定義の型変数の場合 (caml2html: typing_undef) *)
if occur r1 t2 then raise (Unify(t1, t2));
r1 := Some(t2)
| _, Type.Var({ contents = None } as r2) ->
if occur r2 t1 then raise (Unify(t1, t2));
r2 := Some(t1)
| _, _ -> raise (Unify(t1, t2))
let rec g env e = (* 型推論ルーチン (caml2html: typing_g) *)
try
match e with
| Unit -> Type.Unit
| Bool(_) -> Type.Bool
| Int(_) -> Type.Int
| Float(_) -> Type.Float
| Not(e) ->
unify Type.Bool (g env e);
Type.Bool
| Neg(e) ->
unify Type.Int (g env e);
Type.Int
| Add(e1, e2) | Sub(e1, e2) -> (* 足し算(と引き算)の型推論 (caml2html: typing_add) *)
unify Type.Int (g env e1);
unify Type.Int (g env e2);
Type.Int
| FNeg(e) ->
unify Type.Float (g env e);
Type.Float
| FAdd(e1, e2) | FSub(e1, e2) | FMul(e1, e2) | FDiv(e1, e2) ->
unify Type.Float (g env e1);
unify Type.Float (g env e2);
Type.Float
| Eq(e1, e2) | LE(e1, e2) ->
unify (g env e1) (g env e2);
Type.Bool
| If(e1, e2, e3) ->
unify (g env e1) Type.Bool;
let t2 = g env e2 in
let t3 = g env e3 in
unify t2 t3;
t2
| Let((x, t), e1, e2) -> (* letの型推論 (caml2html: typing_let) *)
unify t (g env e1);
g (M.add x t env) e2
| Var(x) when M.mem x env -> M.find x env (* 変数の型推論 (caml2html: typing_var) *)
| Var(x) when M.mem x !extenv -> M.find x !extenv
| Var(x) -> (* 外部変数の型推論 (caml2html: typing_extvar) *)
Format.eprintf "free variable %s assumed as external@." x;
let t = Type.gentyp () in
extenv := M.add x t !extenv;
t
| LetRec({ name = (x, t); args = yts; body = e1 }, e2) -> (* let recの型推論 (caml2html: typing_letrec) *)
let env = M.add x t env in
unify t (Type.Fun(List.map snd yts, g (M.add_list yts env) e1));
g env e2
| App(e, es) -> (* 関数適用の型推論 (caml2html: typing_app) *)
let t = Type.gentyp () in
unify (g env e) (Type.Fun(List.map (g env) es, t));
t
| Tuple(es) -> Type.Tuple(List.map (g env) es)
| LetTuple(xts, e1, e2) ->
unify (Type.Tuple(List.map snd xts)) (g env e1);
g (M.add_list xts env) e2
| Array(e1, e2) -> (* must be a primitive for "polymorphic" typing *)
unify (g env e1) Type.Int;
Type.Array(g env e2)
| Get(e1, e2) ->
let t = Type.gentyp () in
unify (Type.Array(t)) (g env e1);
unify Type.Int (g env e2);
t
| Put(e1, e2, e3) ->
let t = g env e3 in
unify (Type.Array(t)) (g env e1);
unify Type.Int (g env e2);
Type.Unit
with Unify(t1, t2) -> raise (Error(deref_term e, deref_typ t1, deref_typ t2))
let f e =
extenv := M.empty;
(*
(match deref_typ (g M.empty e) with
| Type.Unit -> ()
| _ -> Format.eprintf "warning: final result does not have type unit@.");
*)
(try unify Type.Unit (g M.empty e)
with Unify _ -> failwith "top level does not have type unit");
extenv := M.map deref_typ !extenv;
deref_term e