Project

General

Profile

Download (39.3 KB) Statistics
| Branch: | Tag: | Revision:
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - LIFL             *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(*  This file was originally from the Prelude compiler              *)
11
(*                                                                  *)
12
(********************************************************************)
13

    
14
(** Main typing module. Classic inference algorithm with destructive
15
    unification. *)
16

    
17
let debug _fmt _args = ()
18

    
19
(* Format.eprintf "%a" *)
20
(* Though it shares similarities with the clock calculus module, no code is
21
   shared. Simple environments, very limited identifier scoping, no identifier
22
   redefinition allowed. *)
23

    
24
open Utils
25

    
26
(* Yes, opening both modules is dirty as some type names will be overwritten,
27
   yet this makes notations far lighter.*)
28
open Lustre_types
29
open Corelang
30

    
31
(* TODO general remark: except in the add_vdecl, it seems to me that all the
32
   pairs (env, vd_env) should be replace with just env, since vd_env is never
33
   used and the env element is always extract with a fst *)
34

    
35
module type EXPR_TYPE_HUB = sig
36
  type type_expr
37

    
38
  val import : Types.Main.type_expr -> type_expr
39

    
40
  val export : type_expr -> Types.Main.type_expr
41
end
42

    
43
module Make
44
    (T : Types.S)
45
    (Expr_type_hub : EXPR_TYPE_HUB with type type_expr = T.type_expr) =
46
struct
47
  module TP = Type_predef.Make (T)
48
  include TP
49

    
50
  let pp_typing_env fmt env = Env.pp_env print_ty fmt env
51

    
52
  (****************************************************************)
53
  (* Generic functions: occurs, instantiate and generalize         *)
54
  (****************************************************************)
55

    
56
  (** [occurs tvar ty] returns true if the type variable [tvar] occurs in type
57
      [ty]. False otherwise. *)
58
  let rec occurs tvar ty =
59
    let ty = repr ty in
60
    match type_desc ty with
61
    | Tvar ->
62
      ty = tvar
63
    | Tarrow (t1, t2) ->
64
      occurs tvar t1 || occurs tvar t2
65
    | Ttuple tl ->
66
      List.exists (occurs tvar) tl
67
    | Tstruct fl ->
68
      List.exists (fun (_, t) -> occurs tvar t) fl
69
    | Tarray (_, t) | Tstatic (_, t) | Tclock t | Tlink t ->
70
      occurs tvar t
71
    | Tenum _ | Tconst _ | Tunivar | Tbasic _ ->
72
      false
73

    
74
  (* Generalize by side-effects *)
75

    
76
  (** Promote monomorphic type variables to polymorphic type variables. *)
77
  let rec generalize ty =
78
    match type_desc ty with
79
    | Tvar ->
80
      (* No scopes, always generalize *)
81
      ty.tdesc <- Tunivar
82
    | Tarrow (t1, t2) ->
83
      generalize t1;
84
      generalize t2
85
    | Ttuple tl ->
86
      List.iter generalize tl
87
    | Tstruct fl ->
88
      List.iter (fun (_, t) -> generalize t) fl
89
    | Tstatic (d, t) | Tarray (d, t) ->
90
      Dimension.generalize d;
91
      generalize t
92
    | Tclock t | Tlink t ->
93
      generalize t
94
    | Tenum _ | Tconst _ | Tunivar | Tbasic _ ->
95
      ()
96

    
97
  (** Downgrade polymorphic type variables to monomorphic type variables *)
98
  let rec instantiate inst_vars inst_dim_vars ty =
99
    let ty = repr ty in
100
    match ty.tdesc with
101
    | Tenum _ | Tconst _ | Tvar | Tbasic _ ->
102
      ty
103
    | Tarrow (t1, t2) ->
104
      {
105
        ty with
106
        tdesc =
107
          Tarrow
108
            ( instantiate inst_vars inst_dim_vars t1,
109
              instantiate inst_vars inst_dim_vars t2 );
110
      }
111
    | Ttuple tlist ->
112
      {
113
        ty with
114
        tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist);
115
      }
116
    | Tstruct flist ->
117
      {
118
        ty with
119
        tdesc =
120
          Tstruct
121
            (List.map
122
               (fun (f, t) -> f, instantiate inst_vars inst_dim_vars t)
123
               flist);
124
      }
125
    | Tclock t ->
126
      { ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t) }
127
    | Tstatic (d, t) ->
128
      {
129
        ty with
130
        tdesc =
131
          Tstatic
132
            ( Dimension.instantiate inst_dim_vars d,
133
              instantiate inst_vars inst_dim_vars t );
134
      }
135
    | Tarray (d, t) ->
136
      {
137
        ty with
138
        tdesc =
139
          Tarray
140
            ( Dimension.instantiate inst_dim_vars d,
141
              instantiate inst_vars inst_dim_vars t );
142
      }
143
    | Tlink t ->
144
      (* should not happen *)
145
      { ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t) }
146
    | Tunivar -> (
147
      try List.assoc ty.tid !inst_vars
148
      with Not_found ->
149
        let var = new_var () in
150
        inst_vars := (ty.tid, var) :: !inst_vars;
151
        var)
152

    
153
  let basic_coretype_type t =
154
    if is_real_type t then Tydec_real
155
    else if is_int_type t then Tydec_int
156
    else if is_bool_type t then Tydec_bool
157
    else assert false
158

    
159
  (* [type_coretype cty] types the type declaration [cty] *)
160
  let rec type_coretype type_dim cty =
161
    match (*get_repr_type*)
162
          cty with
163
    | Tydec_any ->
164
      new_var ()
165
    | Tydec_int ->
166
      type_int
167
    | Tydec_real ->
168
      (* Type_predef. *)
169
      type_real
170
    (* | Tydec_float -> Type_predef.type_real *)
171
    | Tydec_bool ->
172
      (* Type_predef. *)
173
      type_bool
174
    | Tydec_clock ty ->
175
      (* Type_predef. *)
176
      type_clock (type_coretype type_dim ty)
177
    | Tydec_const c ->
178
      (* Type_predef. *)
179
      type_const c
180
    | Tydec_enum tl ->
181
      (* Type_predef. *)
182
      type_enum tl
183
    | Tydec_struct fl ->
184
      (* Type_predef. *)
185
      type_struct (List.map (fun (f, ty) -> f, type_coretype type_dim ty) fl)
186
    | Tydec_array (d, ty) ->
187
      let d = Dimension.copy (ref []) d in
188
      type_dim d;
189
      (* Type_predef. *)
190
      type_array d (type_coretype type_dim ty)
191

    
192
  (* [coretype_type] is the reciprocal of [type_typecore] *)
193
  let rec coretype_type ty =
194
    match (repr ty).tdesc with
195
    | Tvar ->
196
      Tydec_any
197
    | Tbasic _ ->
198
      basic_coretype_type ty
199
    | Tconst c ->
200
      Tydec_const c
201
    | Tclock t ->
202
      Tydec_clock (coretype_type t)
203
    | Tenum tl ->
204
      Tydec_enum tl
205
    | Tstruct fl ->
206
      Tydec_struct (List.map (fun (f, t) -> f, coretype_type t) fl)
207
    | Tarray (d, t) ->
208
      Tydec_array (d, coretype_type t)
209
    | Tstatic (_, t) ->
210
      coretype_type t
211
    | _ ->
212
      assert false
213

    
214
  let get_coretype_definition tname =
215
    try
216
      let top = Hashtbl.find type_table (Tydec_const tname) in
217
      match top.top_decl_desc with
218
      | TypeDef tdef ->
219
        tdef.tydef_desc
220
      | _ ->
221
        assert false
222
    with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
223

    
224
  let get_type_definition tname =
225
    type_coretype (fun _ -> ()) (get_coretype_definition tname)
226

    
227
  (* Equality on ground types only *)
228
  (* Should be used between local variables which must have a ground type *)
229
  let rec eq_ground t1 t2 =
230
    let t1 = repr t1 in
231
    let t2 = repr t2 in
232
    t1 == t2
233
    ||
234
    match t1.tdesc, t2.tdesc with
235
    | Tbasic t1, Tbasic t2 when t1 == t2 ->
236
      true
237
    | Tenum tl, Tenum tl' when tl == tl' ->
238
      true
239
    | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
240
      List.for_all2 eq_ground tl tl'
241
    | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
242
      List.for_all2 (fun (_, t) (_, t') -> eq_ground t t') fl fl'
243
    | Tconst t, _ ->
244
      let def_t = get_type_definition t in
245
      eq_ground def_t t2
246
    | _, Tconst t ->
247
      let def_t = get_type_definition t in
248
      eq_ground t1 def_t
249
    | Tarrow (t1, t2), Tarrow (t1', t2') ->
250
      eq_ground t1 t1' && eq_ground t2 t2'
251
    | Tclock t1', Tclock t2' ->
252
      eq_ground t1' t2'
253
    | Tstatic (e1, t1'), Tstatic (e2, t2') | Tarray (e1, t1'), Tarray (e2, t2')
254
      ->
255
      Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'
256
    | _ ->
257
      false
258

    
259
  (** [unify t1 t2] unifies types [t1] and [t2] using standard destructive
260
      unification. Raises [Unify (t1,t2)] if the types are not unifiable. [t1]
261
      is a expected/formal/spec type, [t2] is a computed/real/implem type, so in
262
      case of unification error: expected type [t1], got type [t2]. If
263
      [sub]-typing is allowed, [t2] may be a subtype of [t1]. If [semi]
264
      unification is required, [t1] should furthermore be an instance of [t2]
265
      and constants are handled differently.*)
266
  let unify ?(sub = false) ?(semi = false) t1 t2 =
267
    let rec unif t1 t2 =
268
      let t1 = repr t1 in
269
      let t2 = repr t2 in
270
      if t1 == t2 then ()
271
      else
272
        match t1.tdesc, t2.tdesc with
273
        (* strictly subtyping cases first *)
274
        | _, Tclock t2 when sub && get_clock_base_type t1 = None ->
275
          unif t1 t2
276
        | _, Tstatic (_, t2) when sub && get_static_value t1 = None ->
277
          unif t1 t2
278
        (* This case is not mandatory but will keep "older" types *)
279
        | Tvar, Tvar ->
280
          if t1.tid < t2.tid then t2.tdesc <- Tlink t1 else t1.tdesc <- Tlink t2
281
        | Tvar, _ when (not semi) && not (occurs t1 t2) ->
282
          t1.tdesc <- Tlink t2
283
        | _, Tvar when not (occurs t2 t1) ->
284
          t2.tdesc <- Tlink t1
285
        | Tarrow (t1, t2), Tarrow (t1', t2') ->
286
          unif t2 t2';
287
          unif t1' t1
288
        | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
289
          List.iter2 unif tl tl'
290
        | Ttuple [ t1 ], _ ->
291
          unif t1 t2
292
        | _, Ttuple [ t2 ] ->
293
          unif t1 t2
294
        | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
295
          List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'
296
        | Tclock _, Tstatic _ | Tstatic _, Tclock _ ->
297
          raise (Unify (t1, t2))
298
        | Tclock t1', Tclock t2' ->
299
          unif t1' t2'
300
        (* | Tbasic t1, Tbasic t2 when t1 == t2 -> () *)
301
        | Tunivar, _ | _, Tunivar ->
302
          ()
303
        | Tconst t, _ ->
304
          let def_t = get_type_definition t in
305
          unif def_t t2
306
        | _, Tconst t ->
307
          let def_t = get_type_definition t in
308
          unif t1 def_t
309
        | Tenum tl, Tenum tl' when tl == tl' ->
310
          ()
311
        | Tstatic (e1, t1'), Tstatic (e2, t2')
312
        | Tarray (e1, t1'), Tarray (e2, t2') ->
313
          let eval_const =
314
            if semi then fun c ->
315
              Some (Dimension.mkdim_ident Location.dummy_loc c)
316
            else fun _ -> None
317
          in
318
          unif t1' t2';
319
          Dimension.eval Basic_library.eval_dim_env eval_const e1;
320
          Dimension.eval Basic_library.eval_dim_env eval_const e2;
321
          Dimension.unify ~semi e1 e2
322
        (* Special cases for machine_types. Rules to unify static types infered
323
           for numerical constants with non static ones for variables with
324
           possible machine types *)
325
        | Tbasic bt1, Tbasic bt2 when BasicT.is_unifiable bt1 bt2 ->
326
          BasicT.unify bt1 bt2
327
        | _, _ ->
328
          raise (Unify (t1, t2))
329
    in
330
    unif t1 t2
331

    
332
  (* Expected type ty1, got type ty2 *)
333
  let try_unify ?(sub = false) ?(semi = false) ty1 ty2 loc =
334
    try unify ~sub ~semi ty1 ty2 with
335
    | Unify (t1', t2') ->
336
      raise (Error (loc, Type_clash (ty1, ty2)))
337
    | Dimension.Unify _ ->
338
      raise (Error (loc, Type_clash (ty1, ty2)))
339

    
340
  (************************************************)
341
  (* Typing function for each basic AST construct *)
342
  (************************************************)
343

    
344
  let rec type_struct_const_field ?(is_annot = false) loc (label, c) =
345
    if Hashtbl.mem field_table label then (
346
      let tydef = Hashtbl.find field_table label in
347
      let tydec = (typedef_of_top tydef).tydef_desc in
348
      let tydec_struct = get_struct_type_fields tydec in
349
      let ty_label =
350
        type_coretype (fun _ -> ()) (List.assoc label tydec_struct)
351
      in
352
      try_unify ty_label (type_const ~is_annot loc c) loc;
353
      type_coretype (fun _ -> ()) tydec)
354
    else raise (Error (loc, Unbound_value ("struct field " ^ label)))
355

    
356
  and type_const ?(is_annot = false) loc c =
357
    match c with
358
    | Const_int _ ->
359
      (* Type_predef. *)
360
      type_int
361
    | Const_real _ ->
362
      (* Type_predef. *)
363
      type_real
364
    | Const_array ca ->
365
      let d = Dimension.mkdim_int loc (List.length ca) in
366
      let ty = new_var () in
367
      List.iter (fun e -> try_unify ty (type_const ~is_annot loc e) loc) ca;
368
      (* Type_predef. *)
369
      type_array d ty
370
    | Const_tag t ->
371
      if Hashtbl.mem tag_table t then
372
        let tydef = typedef_of_top (Hashtbl.find tag_table t) in
373
        let tydec =
374
          if is_user_type tydef.tydef_desc then Tydec_const tydef.tydef_id
375
          else tydef.tydef_desc
376
        in
377
        type_coretype (fun _ -> ()) tydec
378
      else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
379
    | Const_struct fl -> (
380
      let ty_struct = new_var () in
381
      let used =
382
        List.fold_left
383
          (fun acc (l, c) ->
384
            if List.mem l acc then
385
              raise (Error (loc, Already_bound ("struct field " ^ l)))
386
            else
387
              try_unify ty_struct
388
                (type_struct_const_field ~is_annot loc (l, c))
389
                loc;
390
            l :: acc)
391
          [] fl
392
      in
393
      try
394
        let total =
395
          List.map fst (get_struct_type_fields (coretype_type ty_struct))
396
        in
397
        (* List.iter (fun l -> Format.eprintf "total: %s@." l) total; List.iter
398
           (fun l -> Format.eprintf "used: %s@." l) used; *)
399
        let undef = List.find (fun l -> not (List.mem l used)) total in
400
        raise (Error (loc, Unbound_value ("struct field " ^ undef)))
401
      with Not_found -> ty_struct)
402
    | Const_string s | Const_modeid s ->
403
      if is_annot then (* Type_predef. *)
404
        type_string
405
      else (
406
        Format.eprintf "Typing string %s outisde of annot scope@.@?" s;
407
        assert false (* string datatype should only appear in annotations *))
408

    
409
  (* The following typing functions take as parameter an environment [env] and
410
     whether the element being typed is expected to be constant [const]. [env]
411
     is a pair composed of: - a map from ident to type, associating to each
412
     ident, i.e. variables, constants and (imported) nodes, its type including
413
     whether it is constant or not. This latter information helps in checking
414
     constant propagation policy in Lustre. - a vdecl list, in order to modify
415
     types of declared variables that are later discovered to be clocks during
416
     the typing process. *)
417
  let check_constant loc const_expected const_real =
418
    if const_expected && not const_real then raise (Error (loc, Not_a_constant))
419

    
420
  let rec type_add_const env const arg targ =
421
    (*Format.eprintf "Typing.type_add_const %a %a@." Printers.pp_expr arg
422
      Types.print_ty targ;*)
423
    if const then (
424
      let d =
425
        if is_dimension_type targ then dimension_of_expr arg
426
        else Dimension.mkdim_var ()
427
      in
428
      let eval_const id =
429
        (* Types. *)
430
        get_static_value (Env.lookup_value (fst env) id)
431
      in
432
      Dimension.eval Basic_library.eval_dim_env eval_const d;
433
      let real_static_type =
434
        (* Type_predef. *)
435
        type_static d ((* Types. *)
436
                       dynamic_type targ)
437
      in
438
      (match (* Types. *)
439
             get_static_value targ with
440
      | None ->
441
        ()
442
      | Some _ ->
443
        try_unify targ real_static_type arg.expr_loc);
444
      real_static_type)
445
    else targ
446

    
447
  (* emulates a subtyping relation between types t and (d : t), used during node
448
     applications and assignments *)
449
  and type_subtyping_arg env in_main ?(sub = true) const real_arg formal_type =
450
    let loc = real_arg.expr_loc in
451
    let const =
452
      const
453
      || (* Types. *)
454
      get_static_value formal_type <> None
455
    in
456
    let real_type =
457
      type_add_const env const real_arg (type_expr env in_main const real_arg)
458
    in
459
    (*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const
460
      Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty
461
      formal_type;*)
462
    try_unify ~sub formal_type real_type loc
463

    
464
  (* typing an application implies: - checking that const formal parameters
465
     match real const (maybe symbolic) arguments - checking type adequation
466
     between formal and real arguments An application may embed an
467
     homomorphic/internal function, in which case we need to split it in many
468
     calls *)
469
  and type_appl env in_main loc const f args =
470
    let targs = List.map (type_expr env in_main const) args in
471
    if Basic_library.is_homomorphic_fun f && List.exists is_tuple_type targs
472
    then
473
      try
474
        let targs = Utils.transpose_list (List.map type_list_of_type targs) in
475
        (* Types. *)
476
        type_of_type_list
477
          (List.map (type_simple_call env in_main loc const f) targs)
478
      with Utils.TransposeError (l, l') ->
479
        raise (Error (loc, WrongMorphism (l, l')))
480
    else type_dependent_call env in_main loc const f (List.combine args targs)
481

    
482
  (* type a call with possible dependent types. [targs] is here a list of
483
     (argument, type) pairs. *)
484
  and type_dependent_call env in_main loc const f targs =
485
    (* Format.eprintf "Typing.type_dependent_call %s@." f; *)
486
    let tins, touts = new_var (), new_var () in
487
    (* Format.eprintf "tin=%a, tout=%a@." print_ty tins print_ty touts; *)
488
    let tfun =
489
      (* Type_predef. *)
490
      type_arrow tins touts
491
    in
492
    (* Format.eprintf "fun=%a@." print_ty tfun; *)
493
    type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
494
    (* Format.eprintf "type subtyping@."; *)
495
    let tins = type_list_of_type tins in
496
    if List.length targs <> List.length tins then
497
      raise (Error (loc, WrongArity (List.length tins, List.length targs)))
498
    else (
499
      List.iter2
500
        (fun (a, t) ti ->
501
          let t' =
502
            type_add_const env
503
              (const
504
              || (* Types. *)
505
              get_static_value ti <> None)
506
              a t
507
          in
508
          (* Format.eprintf "uniying ti=%a t'=%a touts=%a@." print_ty ti
509
             print_ty t' print_ty touts; *)
510
          try_unify ~sub:true ti t' a.expr_loc
511
          (* Format.eprintf "unified ti=%a t'=%a touts=%a@." print_ty ti
512
             print_ty t' print_ty touts; *))
513
        targs tins;
514
      touts)
515

    
516
  (* type a simple call without dependent types but possible homomorphic
517
     extension. [targs] is here a list of arguments' types. *)
518
  and type_simple_call env in_main loc const f targs =
519
    let tins, touts = new_var (), new_var () in
520
    let tfun =
521
      (* Type_predef. *)
522
      type_arrow tins touts
523
    in
524
    type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
525
    (*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty
526
      (type_of_type_list targs);*)
527
    try_unify ~sub:true tins (type_of_type_list targs) loc;
528
    touts
529

    
530
  (** [type_expr env in_main expr] types expression [expr] in environment [env],
531
      expecting it to be [const] or not. *)
532
  and type_expr ?(is_annot = false) env in_main const expr =
533
    let resulting_ty =
534
      match expr.expr_desc with
535
      | Expr_const c ->
536
        let ty = type_const ~is_annot expr.expr_loc c in
537
        let ty =
538
          (* Type_predef. *)
539
          type_static (Dimension.mkdim_var ()) ty
540
        in
541
        expr.expr_type <- Expr_type_hub.export ty;
542
        ty
543
      | Expr_ident v ->
544
        let tyv =
545
          try Env.lookup_value (fst env) v
546
          with Not_found ->
547
            Format.eprintf
548
              "Failure in typing expr %a. Not in typing environement@."
549
              Printers.pp_expr expr;
550
            raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))
551
        in
552
        let ty = instantiate (ref []) (ref []) tyv in
553
        let ty' =
554
          if const then
555
            (* Type_predef. *)
556
            type_static (Dimension.mkdim_var ()) (new_var ())
557
          else new_var ()
558
        in
559
        try_unify ty ty' expr.expr_loc;
560
        expr.expr_type <- Expr_type_hub.export ty;
561
        ty
562
      | Expr_array elist ->
563
        let ty_elt = new_var () in
564
        List.iter
565
          (fun e ->
566
            try_unify ty_elt
567
              (type_appl env in_main expr.expr_loc const "uminus" [ e ])
568
              e.expr_loc)
569
          elist;
570
        let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
571
        let ty =
572
          (* Type_predef. *)
573
          type_array d ty_elt
574
        in
575
        expr.expr_type <- Expr_type_hub.export ty;
576
        ty
577
      | Expr_access (e1, d) ->
578
        type_subtyping_arg env in_main false
579
          (* not necessary a constant *)
580
          (expr_of_dimension d)
581
          (* Type_predef. *)
582
          type_int;
583
        let ty_elt = new_var () in
584
        let d = Dimension.mkdim_var () in
585
        type_subtyping_arg env in_main const e1
586
          ((* Type_predef. *)
587
           type_array d ty_elt);
588
        expr.expr_type <- Expr_type_hub.export ty_elt;
589
        ty_elt
590
      | Expr_power (e1, d) ->
591
        let eval_const id =
592
          (* Types. *)
593
          get_static_value (Env.lookup_value (fst env) id)
594
        in
595
        type_subtyping_arg env in_main true (expr_of_dimension d)
596
          (* Type_predef. *)
597
          type_int;
598
        Dimension.eval Basic_library.eval_dim_env eval_const d;
599
        let ty_elt =
600
          type_appl env in_main expr.expr_loc const "uminus" [ e1 ]
601
        in
602
        let ty =
603
          (* Type_predef. *)
604
          type_array d ty_elt
605
        in
606
        expr.expr_type <- Expr_type_hub.export ty;
607
        ty
608
      | Expr_tuple elist ->
609
        let ty =
610
          new_ty
611
            (Ttuple (List.map (type_expr ~is_annot env in_main const) elist))
612
        in
613
        expr.expr_type <- Expr_type_hub.export ty;
614
        ty
615
      | Expr_ite (c, t, e) ->
616
        type_subtyping_arg env in_main const c (* Type_predef. *) type_bool;
617
        let ty = type_appl env in_main expr.expr_loc const "+" [ t; e ] in
618
        expr.expr_type <- Expr_type_hub.export ty;
619
        ty
620
      | Expr_appl (id, args, r) ->
621
        (* application of non internal function is not legal in a constant
622
           expression *)
623
        (match r with
624
        | None ->
625
          ()
626
        | Some c ->
627
          check_constant expr.expr_loc const false;
628
          type_subtyping_arg env in_main const c (* Type_predef. *) type_bool);
629
        let args_list = expr_list_of_expr args in
630
        let touts = type_appl env in_main expr.expr_loc const id args_list in
631
        let targs =
632
          new_ty
633
            (Ttuple
634
               (List.map (fun a -> Expr_type_hub.import a.expr_type) args_list))
635
        in
636
        args.expr_type <- Expr_type_hub.export targs;
637
        expr.expr_type <- Expr_type_hub.export touts;
638
        touts
639
      | Expr_fby (e1, e2) | Expr_arrow (e1, e2) ->
640
        (* fby/arrow is not legal in a constant expression *)
641
        check_constant expr.expr_loc const false;
642
        let ty = type_appl env in_main expr.expr_loc const "+" [ e1; e2 ] in
643
        expr.expr_type <- Expr_type_hub.export ty;
644
        ty
645
      | Expr_pre e ->
646
        (* pre is not legal in a constant expression *)
647
        check_constant expr.expr_loc const false;
648
        let ty = type_appl env in_main expr.expr_loc const "uminus" [ e ] in
649
        expr.expr_type <- Expr_type_hub.export ty;
650
        ty
651
      | Expr_when (e1, c, l) ->
652
        (* when is not legal in a constant expression *)
653
        check_constant expr.expr_loc const false;
654
        let typ_l =
655
          (* Type_predef. *)
656
          type_clock (type_const ~is_annot expr.expr_loc (Const_tag l))
657
        in
658
        let expr_c = expr_of_ident c expr.expr_loc in
659
        type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
660
        let ty = type_appl env in_main expr.expr_loc const "uminus" [ e1 ] in
661
        expr.expr_type <- Expr_type_hub.export ty;
662
        ty
663
      | Expr_merge (c, hl) ->
664
        (* merge is not legal in a constant expression *)
665
        check_constant expr.expr_loc const false;
666
        let typ_in, typ_out =
667
          type_branches env in_main expr.expr_loc const hl
668
        in
669
        let expr_c = expr_of_ident c expr.expr_loc in
670
        let typ_l =
671
          (* Type_predef. *)
672
          type_clock typ_in
673
        in
674
        type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
675
        expr.expr_type <- Expr_type_hub.export typ_out;
676
        typ_out
677
    in
678
    Log.report ~level:3 (fun fmt ->
679
        Format.fprintf fmt "Type of expr %a: %a@ " Printers.pp_expr expr
680
          (* Types. *)
681
          print_ty resulting_ty);
682
    resulting_ty
683

    
684
  and type_branches ?(is_annot = false) env in_main loc const hl =
685
    let typ_in = new_var () in
686
    let typ_out = new_var () in
687
    try
688
      let used_labels =
689
        List.fold_left
690
          (fun accu (t, h) ->
691
            unify typ_in (type_const ~is_annot loc (Const_tag t));
692
            type_subtyping_arg env in_main const h typ_out;
693
            if List.mem t accu then raise (Error (loc, Already_bound t))
694
            else t :: accu)
695
          [] hl
696
      in
697
      let type_labels = get_enum_type_tags (coretype_type typ_in) in
698
      if List.sort compare used_labels <> List.sort compare type_labels then
699
        let unbound_tag =
700
          List.find (fun t -> not (List.mem t used_labels)) type_labels
701
        in
702
        raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
703
      else typ_in, typ_out
704
    with Unify (t1, t2) -> raise (Error (loc, Type_clash (t1, t2)))
705

    
706
  (* Eexpr are always in annotations. TODO: add the quantifiers variables to the
707
     env *)
708
  let type_eexpr env eexpr =
709
    type_expr ~is_annot:true env false (* not in main *) false (* not a const *)
710
      eexpr.eexpr_qfexpr
711

    
712
  (** [type_eq env eq] types equation [eq] in environment [env] *)
713
  let type_eq env in_main undefined_vars eq =
714
    (*Format.eprintf "Typing.type_eq %a@." Printers.pp_node_eq eq;*)
715
    (* Check undefined variables, type lhs *)
716
    let expr_lhs =
717
      expr_of_expr_list eq.eq_loc
718
        (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs)
719
    in
720
    let ty_lhs = type_expr env in_main false expr_lhs in
721
    (* Check multiple variable definitions *)
722
    let define_var id uvars =
723
      if ISet.mem id uvars then ISet.remove id uvars
724
      else raise (Error (eq.eq_loc, Already_defined id))
725
    in
726
    (* check assignment of declared constant, assignment of clock *)
727
    let ty_lhs =
728
      type_of_type_list
729
        (List.map2
730
           (fun ty id ->
731
             if get_static_value ty <> None then
732
               raise (Error (eq.eq_loc, Assigned_constant id))
733
             else match get_clock_base_type ty with None -> ty | Some ty -> ty)
734
           (type_list_of_type ty_lhs) eq.eq_lhs)
735
    in
736
    let undefined_vars =
737
      List.fold_left
738
        (fun uvars v -> define_var v uvars)
739
        undefined_vars eq.eq_lhs
740
    in
741
    (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be
742
       assigned to a (always non-constant) lhs variable *)
743
    type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
744
    undefined_vars
745

    
746
  (* [type_coreclock env ck id loc] types the type clock declaration [ck] in
747
     environment [env] *)
748
  let type_coreclock env ck id loc =
749
    match ck.ck_dec_desc with
750
    | Ckdec_any ->
751
      ()
752
    | Ckdec_bool cl ->
753
      let dummy_id_expr = expr_of_ident id loc in
754
      let when_expr =
755
        List.fold_left
756
          (fun expr (x, l) ->
757
            {
758
              expr_tag = new_tag ();
759
              expr_desc = Expr_when (expr, x, l);
760
              expr_type = Types.Main.new_var ();
761
              expr_clock = Clocks.new_var true;
762
              expr_delay = Delay.new_var ();
763
              expr_loc = loc;
764
              expr_annot = None;
765
            })
766
          dummy_id_expr cl
767
      in
768
      ignore (type_expr env false false when_expr)
769

    
770
  let rec check_type_declaration loc cty =
771
    match cty with
772
    | Tydec_clock ty | Tydec_array (_, ty) ->
773
      check_type_declaration loc ty
774
    | Tydec_const tname ->
775
      (* Format.eprintf "TABLE: %a@." print_type_table (); *)
776
      if not (Hashtbl.mem type_table cty) then
777
        raise (Error (loc, Unbound_type tname))
778
    | _ ->
779
      ()
780

    
781
  let type_var_decl vd_env env vdecl =
782
    (*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl
783
      Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*)
784
    check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
785
    let eval_const id =
786
      (* Types. *)
787
      get_static_value (Env.lookup_value env id)
788
    in
789
    let type_dim d =
790
      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d)
791
        (* Type_predef. *)
792
        type_int;
793
      Dimension.eval Basic_library.eval_dim_env eval_const d
794
    in
795
    let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
796

    
797
    let ty_static =
798
      if vdecl.var_dec_const then
799
        (* Type_predef. *)
800
        type_static (Dimension.mkdim_var ()) ty
801
      else ty
802
    in
803
    (match vdecl.var_dec_value with
804
    | None ->
805
      ()
806
    | Some v ->
807
      type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static);
808
    try_unify ty_static (Expr_type_hub.import vdecl.var_type) vdecl.var_loc;
809
    let new_env = Env.add_value env vdecl.var_id ty_static in
810
    type_coreclock (new_env, vd_env) vdecl.var_dec_clock vdecl.var_id
811
      vdecl.var_loc;
812
    (*Format.eprintf "END %a@." Types.print_ty ty_static;*)
813
    new_env
814

    
815
  let type_var_decl_list vd_env env l =
816
    List.fold_left (type_var_decl vd_env) env l
817

    
818
  let type_of_vlist vars =
819
    let tyl = List.map (fun v -> Expr_type_hub.import v.var_type) vars in
820
    type_of_type_list tyl
821

    
822
  let add_vdecl vd_env vdecl =
823
    if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env then
824
      raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
825
    else vdecl :: vd_env
826

    
827
  let check_vd_env vd_env = ignore (List.fold_left add_vdecl [] vd_env)
828

    
829
  let type_contract env c =
830
    let vd_env = c.consts @ c.locals in
831
    check_vd_env vd_env;
832
    let env =
833
      type_var_decl_list
834
        (* this argument seems useless to me, cf TODO at top of the file*)
835
        vd_env env vd_env
836
    in
837
    (* typing stmts *)
838
    let eqs =
839
      List.map (fun s -> match s with Eq eq -> eq | _ -> assert false) c.stmts
840
    in
841
    let undefined_vars_init =
842
      List.fold_left (fun uvs v -> ISet.add v.var_id uvs) ISet.empty c.locals
843
    in
844
    let _ =
845
      List.fold_left
846
        (type_eq (env, vd_env) false (*is_main*))
847
        undefined_vars_init eqs
848
    in
849
    (* Typing each predicate expr *)
850
    let type_pred_ee ee : unit =
851
      type_subtyping_arg (env, vd_env) false (* not in main *) false
852
        (* not a const *)
853
        ee.eexpr_qfexpr type_bool
854
    in
855
    List.iter type_pred_ee
856
      (c.assume @ c.guarantees
857
      @ List.flatten (List.map (fun m -> m.ensure @ m.require) c.modes));
858
    (*TODO enrich env locally with locals and consts type each pre/post as a
859
      boolean expr I don't know if we want to update the global env with locally
860
      typed variables. For the moment, returning the provided env *)
861
    env
862

    
863
  let rec type_spec env spec =
864
    match spec with Contract c -> type_contract env c | NodeSpec _ -> env
865

    
866
  (** [type_node env nd loc] types node [nd] in environment env. The location is
867
      used for error reports. *)
868
  and type_node env nd loc =
869
    (* Format.eprintf "Typing node %s@." nd.node_id; *)
870
    let is_main = nd.node_id = !Options.main_node in
871
    (* In contracts, outputs are considered as input values *)
872
    let vd_env_ol =
873
      if nd.node_iscontract then nd.node_locals
874
      else nd.node_outputs @ nd.node_locals
875
    in
876
    let vd_env = nd.node_inputs @ nd.node_outputs @ nd.node_locals in
877
    check_vd_env vd_env;
878
    let init_env = env in
879
    let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
880
    let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
881
    let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
882
    let new_env = Env.overwrite env delta_env in
883
    let undefined_vars_init =
884
      List.fold_left (fun uvs v -> ISet.add v.var_id uvs) ISet.empty vd_env_ol
885
    in
886
    let undefined_vars =
887
      let eqs, _ = get_node_eqs nd in
888
      (* TODO XXX: il faut typer les handlers de l'automate *)
889
      List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs
890
    in
891
    (* Typing asserts *)
892
    List.iter
893
      (fun assert_ ->
894
        let assert_expr = assert_.assert_expr in
895
        type_subtyping_arg (new_env, vd_env) is_main false assert_expr
896
          (* Type_predef. *)
897
          type_bool)
898
      nd.node_asserts;
899
    (* Typing spec/contracts *)
900
    (match nd.node_spec with
901
    | None ->
902
      ()
903
    | Some spec ->
904
      ignore (type_spec new_env spec));
905
    (* Typing annots *)
906
    List.iter
907
      (fun annot ->
908
        List.iter
909
          (fun (_, eexpr) -> ignore (type_eexpr (new_env, vd_env) eexpr))
910
          annot.annots)
911
      nd.node_annot;
912

    
913
    (* check that table is empty *)
914
    let local_consts =
915
      List.fold_left
916
        (fun res vdecl ->
917
          if vdecl.var_dec_const then ISet.add vdecl.var_id res else res)
918
        ISet.empty nd.node_locals
919
    in
920
    let undefined_vars = ISet.diff undefined_vars local_consts in
921

    
922
    if not (ISet.is_empty undefined_vars) then
923
      raise (Error (loc, Undefined_var undefined_vars));
924
    let ty_ins = type_of_vlist nd.node_inputs in
925
    let ty_outs = type_of_vlist nd.node_outputs in
926
    let ty_node = new_ty (Tarrow (ty_ins, ty_outs)) in
927
    generalize ty_node;
928
    (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
929
    nd.node_type <- Expr_type_hub.export ty_node;
930
    Env.add_value env nd.node_id ty_node
931

    
932
  let type_imported_node env nd _loc =
933
    let vd_env = nd.nodei_inputs @ nd.nodei_outputs in
934
    check_vd_env vd_env;
935
    let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in
936
    let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in
937
    let new_env = Env.overwrite env delta_env in
938
    (* Typing spec *)
939
    (match nd.nodei_spec with
940
    | None ->
941
      ()
942
    | Some spec ->
943
      ignore (type_spec new_env spec));
944
    let ty_ins = type_of_vlist nd.nodei_inputs in
945
    let ty_outs = type_of_vlist nd.nodei_outputs in
946
    let ty_node = new_ty (Tarrow (ty_ins, ty_outs)) in
947
    generalize ty_node;
948
    (* if (is_polymorphic ty_node) then raise (Error (loc, Poly_imported_node
949
       nd.nodei_id)); *)
950
    let new_env = Env.add_value env nd.nodei_id ty_node in
951
    nd.nodei_type <- Expr_type_hub.export ty_node;
952
    new_env
953

    
954
  let type_top_const env cdecl =
955
    let ty = type_const cdecl.const_loc cdecl.const_value in
956
    let d =
957
      if is_dimension_type ty then
958
        dimension_of_const cdecl.const_loc cdecl.const_value
959
      else Dimension.mkdim_var ()
960
    in
961
    let ty =
962
      (* Type_predef. *)
963
      type_static d ty
964
    in
965
    let new_env = Env.add_value env cdecl.const_id ty in
966
    cdecl.const_type <- Expr_type_hub.export ty;
967
    new_env
968

    
969
  let type_top_consts env clist = List.fold_left type_top_const env clist
970

    
971
  let rec type_top_decl env decl =
972
    match decl.top_decl_desc with
973
    | Node nd -> (
974
      try type_node env nd decl.top_decl_loc
975
      with Error _ as exc ->
976
        if !Options.global_inline then
977
          Format.eprintf "Type error: failing node@.%a@.@?" Printers.pp_node nd;
978
        raise exc)
979
    | ImportedNode nd ->
980
      type_imported_node env nd decl.top_decl_loc
981
    | Const c ->
982
      type_top_const env c
983
    | TypeDef _ ->
984
      List.fold_left type_top_decl env (consts_of_enum_type decl)
985
    | Include _ | Open _ ->
986
      env
987

    
988
  let get_type_of_call decl =
989
    match decl.top_decl_desc with
990
    | Node nd ->
991
      let in_typ, out_typ = split_arrow (Expr_type_hub.import nd.node_type) in
992
      type_list_of_type in_typ, type_list_of_type out_typ
993
    | ImportedNode nd ->
994
      let in_typ, out_typ = split_arrow (Expr_type_hub.import nd.nodei_type) in
995
      type_list_of_type in_typ, type_list_of_type out_typ
996
    | _ ->
997
      assert false
998

    
999
  let type_prog env decls =
1000
    try List.fold_left type_top_decl env decls
1001
    with Failure _ as exc -> raise exc
1002

    
1003
  (* Once the Lustre program is fully typed, we must get back to the original
1004
     description of dimensions, with constant parameters, instead of unifiable
1005
     internal variables. *)
1006

    
1007
  (* The following functions aims at 'unevaluating' dimension expressions
1008
     occuring in array types, i.e. replacing unifiable second_order variables
1009
     with the original static parameters. Once restored in this formulation,
1010
     dimensions may be meaningfully printed. *)
1011
  let uneval_vdecl_generics vdecl =
1012
    if vdecl.var_dec_const then
1013
      match get_static_value (Expr_type_hub.import vdecl.var_type) with
1014
      | None ->
1015
        Format.eprintf "internal error: %a@." (* Types. *) print_ty
1016
          (Expr_type_hub.import vdecl.var_type);
1017
        assert false
1018
      | Some d ->
1019
        Dimension.uneval vdecl.var_id d
1020

    
1021
  let uneval_node_generics vdecls = List.iter uneval_vdecl_generics vdecls
1022

    
1023
  let uneval_spec_generics spec =
1024
    List.iter uneval_vdecl_generics (spec.consts @ spec.locals)
1025

    
1026
  let uneval_top_generics decl =
1027
    match decl.top_decl_desc with
1028
    | Node nd ->
1029
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
1030
    | ImportedNode nd ->
1031
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
1032
    | Const _ | TypeDef _ | Open _ | Include _ ->
1033
      ()
1034

    
1035
  let uneval_prog_generics prog = List.iter uneval_top_generics prog
1036

    
1037
  let rec get_imported_symbol decls id =
1038
    match decls with
1039
    | [] ->
1040
      assert false
1041
    | decl :: q -> (
1042
      match decl.top_decl_desc with
1043
      | ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf ->
1044
        decl
1045
      | Const c when id = c.const_id && decl.top_decl_itf ->
1046
        decl
1047
      | TypeDef _ ->
1048
        get_imported_symbol (consts_of_enum_type decl @ q) id
1049
      | _ ->
1050
        get_imported_symbol q id)
1051

    
1052
  let check_env_compat header declared computed =
1053
    uneval_prog_generics header;
1054
    Env.iter declared (fun k decl_type_k ->
1055
        let top = get_imported_symbol header k in
1056
        let loc = top.top_decl_loc in
1057
        try
1058
          let computed_t = Env.lookup_value computed k in
1059
          let computed_t = instantiate (ref []) (ref []) computed_t in
1060
          (* Types.print_ty Format.std_formatter decl_type_k; Types.print_ty
1061
             Format.std_formatter computed_t;*)
1062
          try_unify ~sub:true ~semi:true decl_type_k computed_t loc
1063
        with Not_found -> (
1064
          (* If top is a contract we do not require the lustre file to provide
1065
             the same definition. *)
1066
          match top.top_decl_desc with
1067
          | Node nd -> (
1068
            match nd.node_spec with
1069
            | Some (Contract _) ->
1070
              ()
1071
            | _ ->
1072
              raise (Error (loc, Declared_but_undefined k)))
1073
          | _ ->
1074
            raise (Error (loc, Declared_but_undefined k))))
1075

    
1076
  let check_typedef_top decl =
1077
    (*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*)
1078
    (*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*)
1079
    (*Format.eprintf "%a" Corelang.print_type_table ();*)
1080
    match decl.top_decl_desc with
1081
    | TypeDef ty -> (
1082
      let owner = decl.top_decl_owner in
1083
      let itf = decl.top_decl_itf in
1084
      let decl' =
1085
        try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id)
1086
        with Not_found ->
1087
          raise
1088
            (Error
1089
               ( decl.top_decl_loc,
1090
                 Declared_but_undefined ("type " ^ ty.tydef_id) ))
1091
      in
1092
      let owner' = decl'.top_decl_owner in
1093
      (*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*)
1094
      let itf' = decl'.top_decl_itf in
1095
      match decl'.top_decl_desc with
1096
      | Const _ | Node _ | ImportedNode _ ->
1097
        assert false
1098
      | TypeDef ty'
1099
        when coretype_equal ty'.tydef_desc ty.tydef_desc
1100
             && owner' = owner && itf && not itf' ->
1101
        ()
1102
      | _ ->
1103
        raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id)))
1104
    | _ ->
1105
      ()
1106

    
1107
  let check_typedef_compat header = List.iter check_typedef_top header
1108
end
1109

    
1110
include
1111
  Make
1112
    (Types.Main)
1113
    (struct
1114
      type type_expr = Types.Main.type_expr
1115

    
1116
      let import x = x
1117

    
1118
      let export x = x
1119
    end)
1120
(* Local Variables: *)
1121
(* compile-command:"make -C .." *)
1122
(* End: *)
(62-62/66)