summaryrefslogtreecommitdiff
path: root/typing.ml
blob: 13598d49690720f9f9b6d2392c9621db796a1915 (plain)
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
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
open Ast

module Int =
    struct
        type t = int
        let compare x y = x - y
    end

module Imap = Map.Make(Int)

let rec head = function
    | Tvar tvar ->
        begin
        match tvar.def with
            | None -> Tvar tvar
            | Some t -> head t
        end
    | t -> t

let rec canon t =
    match head t with
        | Tarrow (t1, t2) -> Tarrow (canon t1, canon t2)
        | Tproduct l -> Tproduct (List.map canon l)
        | Tlist t -> Tlist (canon t)
        | t -> t

let canon_string t tvar_names =
    let next_tvar_char = ref 97
    and tvar_names = ref tvar_names
    in
    let rec canon_aux t = 
        match canon t with
            | Tint -> "int"
            | Tstring -> "string"
            | Tunit -> "unit"
            | Tbool -> "bool"
            | Tarrow (t1, t2) ->
                Printf.sprintf "(%s -> %s)" (canon_aux t1) (canon_aux t2)
            | Tproduct (t::l) ->
                Printf.sprintf "(%s)"
                    (List.fold_left (fun base t ->
                                    Printf.sprintf "%s * %s"
                                                   base (canon_aux t))
                                    (canon_aux t)
                                    l)
            | Tproduct _ -> failwith "canon_aux : Unreachable matching"
            | Tlist t ->
                Printf.sprintf "%s list" (canon_aux t)
            | Tvar tvar ->
                try
                    Imap.find tvar.id !tvar_names
                with Not_found ->
                    let tvar_name =
                        (Printf.sprintf "'%c" (char_of_int !next_tvar_char))
                    in
                        incr next_tvar_char;
                        tvar_names := Imap.add tvar.id tvar_name !tvar_names;
                        tvar_name
    in
        let s = canon_aux t
        in
            s, !tvar_names

let print_canon_string t =
    let s, _ = (canon_string t Imap.empty)
    in
        Printf.printf "%s\n" s

exception TypingFailure of loc option * string

let typing_error l err = raise (TypingFailure (l, err))

let unification_error l t1 t2 =
    let t1s, tvar_names = canon_string t1 Imap.empty
    in
        let t2s, _ = canon_string t2 tvar_names
        in
            let err = Printf.sprintf "Cette expression a le type %s mais est \
                                      ici utilisée avec le type %s" t1s t2s
            in
                typing_error l err

let rec occur var t_raw =
    match head t_raw with
        | Tarrow (t1, t2) -> (occur var t1) || (occur var t2)
        | Tproduct l -> List.exists (occur var) l
        | Tlist t -> occur var t
        | Tvar tvar when tvar.id = var.id -> true
        | t -> false

let rec unify loc t1 t2 =
    match (head t1, head t2) with
        | (a, b) when a = b -> ()
        | (Tarrow (t1a, t1b), Tarrow (t2a, t2b)) ->
            unify loc t1a t2a;
            unify loc t1b t2b
        | (Tproduct p1, Tproduct p2) when unify_products loc p1 p2 -> ()
        | (Tproduct p1, Tproduct p2) -> unification_error loc t1 t2
        | (Tlist t1, Tlist t2) -> unify loc t1 t2
        | (Tvar tv1, t2) when not (occur tv1 t2) -> (* tv1.def = None puisque
                                                       c'est le head de t1 *)
            tv1.def <- Some t2
        | (Tvar tv1, t2) -> unification_error loc (Tvar tv1) t2
        | (t1, Tvar tv2) ->
            unify loc (Tvar tv2) t1
        | (t1, t2) -> unification_error loc t1 t2
and unify_products loc p1 p2 =
    match (p1, p2) with
        | [], [] -> true
        | [], l -> false
        | l, [] -> false
        | t1::l1, t2::l2 ->
            unify loc t1 t2;
            unify_products loc l1 l2

module V = struct
    type t = tvar
    let compare v1 v2 = Pervasives.compare v1.id v2.id
    let create = let r = ref 0 in fun () -> incr r; { id = !r; def = None }
end

module Vset = Set.Make(V)

let rec fvars = function
    | Tint
    | Tstring
    | Tbool
    | Tunit -> Vset.empty
    | Tarrow (t1, t2) -> Vset.union (fvars t1) (fvars t2)
    | Tproduct l ->
        List.fold_left
            (fun base t -> Vset.union base (fvars t)) Vset.empty l
    | Tlist t -> fvars t
    | Tvar { def = Some t } -> fvars t
    | Tvar tv -> Vset.singleton tv

type schema = { vars : Vset.t; typ : typ }
module Smap = Map.Make(String)
type env = { bindings : schema Smap.t; fvars : Vset.t }

let print_fvars fvars = Vset.iter (function tv -> Printf.printf "%d " tv.id) fvars; print_newline ()

let rec print_type = function
    | Tint -> "int"
    | Tstring -> "string"
    | Tbool -> "bool"
    | Tunit -> "unit"
    | Tarrow (t1, t2) -> Printf.sprintf "%s -> %s" (print_type t1) (print_type t2)
    | Tproduct (t::l) ->
        List.fold_left (fun base t ->
                            Printf.sprintf "%s * %s" base (print_type t))
                       (print_type t)
                       l
    | Tproduct _ -> failwith "print_type : Unreachable matching"
    | Tlist t ->
        Printf.sprintf "%s list" (print_type t)
    | Tvar { id = id ; def = Some t } ->
        Printf.sprintf "var { %d : %s }" id (print_type t)
    | Tvar tvar ->
        Printf.sprintf "var %d" tvar.id

let empty_env = { bindings = Smap.empty ; fvars = Vset.empty }

let add ident t env =
    { bindings = Smap.add ident { vars = Vset.empty ; typ = t } env.bindings;
      fvars = Vset.union env.fvars (fvars t) }

let verify_fvars_folder tv current =
    match head (Tvar tv) with
        | Tvar tv -> Vset.add tv current
        | _ -> current

let add_gen ident t env =
    let envfvars =
        Vset.fold verify_fvars_folder env.fvars Vset.empty
    in
        let binding_vars = Vset.diff (fvars t) envfvars
        in
            { bindings = Smap.add ident
                                  { vars = binding_vars ; typ = t }
                                  env.bindings ;
            fvars = envfvars }

let rec replace_var orig new_tv = function
    | Tarrow (t1, t2) ->
        Tarrow (replace_var orig new_tv t1, replace_var orig new_tv t2)
    | Tproduct l ->
        Tproduct (List.map (replace_var orig new_tv) l)
    | Tlist t ->
        Tlist (replace_var orig new_tv t)
    | Tvar tv when tv.id = orig ->
        new_tv
    | Tvar { id = id ; def = Some t } ->
        Tvar { id = id ; def = Some (replace_var orig new_tv t) }
    | t -> t

let use_freshvar tv t =
    match head (Tvar tv) with
        | Tvar tv -> replace_var tv.id (Tvar (V.create())) t
        | _ -> t

let find ident env =
    let binding = Smap.find ident env.bindings
    in
        Vset.fold use_freshvar binding.vars binding.typ

module Sset = Set.Make(String)

let rec motif_vars loc vars m =
    match m.m with
        | Munderscore -> vars
        | Mident ident when Sset.mem ident vars ->
                typing_error loc
                             (Printf.sprintf "Variable %s non unique \
                                              dans ce motif" ident)
        | Mident ident -> Sset.add ident vars
        | Mtuple l -> List.fold_left (motif_vars loc) vars l

let rec add_motif_base add_func env m t =
    match m.m with
        | Munderscore -> env
        | Mident ident -> add_func ident t env
        | Mtuple l ->
            begin
                match head t with
                    | Tproduct lp ->
                        List.fold_left2 (fun env m t -> add_motif_base add_func
                                                                       env
                                                                       m
                                                                       t)
                                        env
                                        l
                                        lp
                    | _ -> failwith "add_motif_base : Unreachable matching"
            end

let add_motif_gen env m t = add_motif_base add_gen env m t
and add_motif env m t = add_motif_base add env m t

let rec w env e =
    let w_aux e =
        match e.e with
            | Eident ident ->
                begin
                try
                    find ident env
                with Not_found ->
                    typing_error e.loc
                                 (Printf.sprintf "Identifiant invalide : %s"
                                                 ident)
                end
            | Econst (Cint _) -> Tint
            | Econst (Cstring _) -> Tstring
            | Econst (Cbool _) -> Tbool
            | Econst Cunit -> Tunit
            | Econst (Cemptylist) ->
                Tlist (Tvar (V.create ()))
            | Etuple l ->
                Tproduct (List.map (w env) l)
            | Ebinop (e1, OAnd, e2)
            | Ebinop (e1, OOr, e2) ->
                let t1 = w env e1
                and t2 = w env e2
                in
                    unify e1.loc t1 Tbool;
                    unify e2.loc t2 Tbool;
                    Tbool
            | Ebinop (e1, OEq, e2)
            | Ebinop (e1, ONeq, e2)
            | Ebinop (e1, OLt, e2)
            | Ebinop (e1, OLe, e2)
            | Ebinop (e1, OGt, e2)
            | Ebinop (e1, OGe, e2) ->
                let t1 = w env e1
                and t2 = w env e2
                in
                    unify e1.loc t1 Tint;
                    unify e2.loc t2 Tint;
                    Tbool
            | Ebinop (e1, OAdd, e2)
            | Ebinop (e1, OSub, e2)
            | Ebinop (e1, OMul, e2)
            | Ebinop (e1, ODiv, e2) ->
                let t1 = w env e1
                and t2 = w env e2
                in
                    unify e1.loc t1 Tint;
                    unify e2.loc t2 Tint;
                    Tint
            | Eunop (ONot, e) ->
                let t = w env e
                in
                    unify e.loc t Tbool;
                    Tbool
            | Eunop (ONeg, e) ->
                let t = w env e
                in
                    unify e.loc t Tint;
                    Tint
            | Eletin (m, val_expr, body_expr) ->
                let m_t = w_motif m
                and val_t = w env val_expr
                in
                    unify val_expr.loc m_t val_t;
                    let env2 = add_motif_gen env m val_t
                    in
                        w env2 body_expr
            | Efunc f when not f.recursive ->
                let arg_t = w_motif f.arg
                in
                    let env2 = add_motif env f.arg arg_t
                    in
                        let return_t = w env2 f.body
                        in
                            Tarrow (arg_t, return_t)
            | Efunc f -> (* f.recursive = true *)
                let arg_t = w_motif f.arg
                and return_t = Tvar (V.create ())
                in
                    let env2 =
                        let fname = match f.name with
                            | Some name -> name
                            | None -> failwith "w : Unreachable matching"
                        in
                            add fname (Tarrow (arg_t, return_t)) env
                    in
                        let env2 = add_motif env2 f.arg arg_t
                        in
                            unify f.body.loc (w env2 f.body) return_t;
                            Tarrow (arg_t, return_t)
            | Eif (cond, then_expr, else_expr) ->
                let cond_t = w env cond
                and then_t = w env then_expr
                and else_t = w env else_expr
                in
                    unify cond.loc cond_t Tbool;
                    unify else_expr.loc else_t then_t;
                    then_t
            | Elistcons (head, tail) ->
                let head_t = w env head
                and tail_t = w env tail
                in
                    unify head.loc (Tlist head_t) tail_t;
                    Tlist head_t
            | Ecall (func_expr, arg) ->
                let func_t = w env func_expr
                and arg_t = w env arg
                and alpha_t = Tvar (V.create ())
                in
                    unify func_expr.loc func_t (Tarrow (arg_t, alpha_t));
                    alpha_t
            | Ematch (match_expr, empty_expr, head_m, tail_m, expr) ->
                let match_t = w env match_expr
                and empty_t = w env empty_expr
                and head_t = w_motif head_m
                and tail_t = w_motif tail_m
                in
                    unify match_expr.loc match_t (Tlist head_t);
                    let vars_base =
                        match tail_m.m with
                            | Mtuple _ ->
                                typing_error e.loc "Motif interdit dans le \
                                                    filtrage de la queue de \
                                                    liste"
                            | Mident ident -> Sset.singleton ident
                            | Munderscore -> Sset.empty
                    in
                        unify match_expr.loc tail_t (Tlist head_t);
                        let env2 = add_motif (add_motif env head_m head_t)
                                             tail_m
                                             tail_t
                        and _ = motif_vars e.loc vars_base head_m
                        in
                            let result_t = w env2 expr
                            in
                                unify expr.loc result_t empty_t;
                                result_t
            | Eclos _ -> failwith "w : Unreachable matching"
    in
        let t = w_aux e
        in
            e.t <- Some t;
            t
and w_motif m =
    let vars = ref Sset.empty
    in
        let rec aux m =
            match m.m with
                | Munderscore -> Tvar (V.create ())
                | Mident ident when Sset.mem ident !vars ->
                    typing_error m.motif_loc
                                 (Printf.sprintf "Variable %s non unique \
                                                  dans ce motif" ident)
                | Mident ident ->
                    let t = Tvar (V.create ())
                    in
                        vars := Sset.add ident !vars;
                        t
                | Mtuple l ->
                    Tproduct (List.map aux l)
        in
            let t = aux m
            in
                m.motif_t <- Some t;
                t

let base_env =
    add "print_int" (Tarrow (Tint, Tunit))
        (add "print_string" (Tarrow (Tstring, Tunit))
            (add "print_newline" (Tarrow (Tunit, Tunit))
                (add "read_int" (Tarrow (Tunit, Tint))
                    (add "read_line" (Tarrow (Tunit, Tstring)) empty_env))))

let type_ast a =
    w base_env a