Project

General

Profile

Download (39.9 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
(* Though it shares similarities with the clock calculus module, no code is
18
   shared. Simple environments, very limited identifier scoping, no identifier
19
   redefinition allowed. *)
20

    
21
open Utils
22

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

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

    
32
module type EXPR_TYPE_HUB = sig
33
  type type_expr
34

    
35
  val import : Types.t -> type_expr
36

    
37
  val export : type_expr -> Types.t
38
end
39

    
40
module Make
41
    (T : Types.S)
42
    (Expr_type_hub : EXPR_TYPE_HUB with type type_expr = T.t) =
43
struct
44
  module TP = Type_predef.Make (T)
45
  include TP
46

    
47
  (* XXX: UNUSED *)
48
  (* let pp_typing_env fmt env = Env.pp print_ty fmt env *)
49

    
50
  (****************************************************************)
51
  (* Generic functions: occurs, instantiate and generalize         *)
52
  (****************************************************************)
53

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

    
72
  (* Generalize by side-effects *)
73

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

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

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

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

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

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

    
222
  let get_type_definition tname =
223
    type_coretype (fun _ -> ()) (get_coretype_definition tname)
224

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

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

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

    
337
  (************************************************)
338
  (* Typing function for each basic AST construct *)
339
  (************************************************)
340

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

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

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

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

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

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

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

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

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

    
706
  and type_branches ?(is_annot = false) env in_main loc const hl =
707
    let typ_in = new_var () in
708
    let typ_out = new_var () in
709
    try
710
      let used_labels =
711
        List.fold_left
712
          (fun accu (t, h) ->
713
            unify typ_in (type_const ~is_annot loc (Const_tag t));
714
            type_subtyping_arg env in_main const h typ_out;
715
            if List.mem t accu then raise (Error (loc, Already_bound t))
716
            else t :: accu)
717
          []
718
          hl
719
      in
720
      let type_labels = get_enum_type_tags (coretype_type typ_in) in
721
      if List.sort compare used_labels <> List.sort compare type_labels then
722
        let unbound_tag =
723
          List.find (fun t -> not (List.mem t used_labels)) type_labels
724
        in
725
        raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
726
      else typ_in, typ_out
727
    with Unify (t1, t2) -> raise (Error (loc, Type_clash (t1, t2)))
728

    
729
  (* Eexpr are always in annotations. TODO: add the quantifiers variables to the
730
     env *)
731
  let type_eexpr env eexpr =
732
    type_expr
733
      ~is_annot:true
734
      env
735
      false
736
      (* not in main *) false (* not a const *)
737
      eexpr.eexpr_qfexpr
738

    
739
  (** [type_eq env eq] types equation [eq] in environment [env] *)
740
  let type_eq env in_main undefined_vars eq =
741
    (*Format.eprintf "Typing.type_eq %a@." Printers.pp_node_eq eq;*)
742
    (* Check undefined variables, type lhs *)
743
    let expr_lhs =
744
      expr_of_expr_list
745
        eq.eq_loc
746
        (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs)
747
    in
748
    let ty_lhs = type_expr env in_main false expr_lhs in
749
    (* Check multiple variable definitions *)
750
    let define_var id uvars =
751
      if ISet.mem id uvars then ISet.remove id uvars
752
      else raise (Error (eq.eq_loc, Already_defined id))
753
    in
754
    (* check assignment of declared constant, assignment of clock *)
755
    let ty_lhs =
756
      type_of_type_list
757
        (List.map2
758
           (fun ty id ->
759
             if get_static_value ty <> None then
760
               raise (Error (eq.eq_loc, Assigned_constant id))
761
             else match get_clock_base_type ty with None -> ty | Some ty -> ty)
762
           (type_list_of_type ty_lhs)
763
           eq.eq_lhs)
764
    in
765
    let undefined_vars =
766
      List.fold_left
767
        (fun uvars v -> define_var v uvars)
768
        undefined_vars
769
        eq.eq_lhs
770
    in
771
    (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be
772
       assigned to a (always non-constant) lhs variable *)
773
    type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
774
    undefined_vars
775

    
776
  (* [type_coreclock env ck id loc] types the type clock declaration [ck] in
777
     environment [env] *)
778
  let type_coreclock env ck id loc =
779
    match ck.ck_dec_desc with
780
    | Ckdec_any ->
781
      ()
782
    | Ckdec_bool cl ->
783
      let dummy_id_expr = expr_of_ident id loc in
784
      let when_expr =
785
        List.fold_left
786
          (fun expr (x, l) ->
787
            {
788
              expr_tag = new_tag ();
789
              expr_desc = Expr_when (expr, x, l);
790
              expr_type = Types.new_var ();
791
              expr_clock = Clocks.new_var true;
792
              expr_delay = Delay.new_var ();
793
              expr_loc = loc;
794
              expr_annot = None;
795
            })
796
          dummy_id_expr
797
          cl
798
      in
799
      ignore (type_expr env false false when_expr)
800

    
801
  let rec check_type_declaration loc cty =
802
    match cty with
803
    | Tydec_clock ty | Tydec_array (_, ty) ->
804
      check_type_declaration loc ty
805
    | Tydec_const tname ->
806
      (* Format.eprintf "TABLE: %a@." pp_type_table (); *)
807
      if not (Hashtbl.mem type_table cty) then
808
        raise (Error (loc, Unbound_type tname))
809
    | _ ->
810
      ()
811

    
812
  let type_var_decl vd_env env vdecl =
813
    (*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl
814
      Printers.pp_dec_ty vdecl.var_dec_type.ty_dec_desc;*)
815
    check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
816
    let eval_const id =
817
      (* Types. *)
818
      get_static_value (Env.lookup_value env id)
819
    in
820
    let type_dim d =
821
      type_subtyping_arg
822
        (env, vd_env)
823
        false
824
        true
825
        (expr_of_dimension d)
826
        (* Type_predef. *)
827
        type_int;
828
      Dimension.eval Basic_library.eval_dim_env eval_const d
829
    in
830
    let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
831

    
832
    let ty_static =
833
      if vdecl.var_dec_const then
834
        (* Type_predef. *)
835
        type_static (Dimension.mkdim_var ()) ty
836
      else ty
837
    in
838
    (match vdecl.var_dec_value with
839
    | None ->
840
      ()
841
    | Some v ->
842
      type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static);
843
    try_unify ty_static (Expr_type_hub.import vdecl.var_type) vdecl.var_loc;
844
    let new_env = Env.add_value env vdecl.var_id ty_static in
845
    type_coreclock
846
      (new_env, vd_env)
847
      vdecl.var_dec_clock
848
      vdecl.var_id
849
      vdecl.var_loc;
850
    (*Format.eprintf "END %a@." Types.pp ty_static;*)
851
    new_env
852

    
853
  let type_var_decl_list vd_env env l =
854
    List.fold_left (type_var_decl vd_env) env l
855

    
856
  let type_of_vlist vars =
857
    let tyl = List.map (fun v -> Expr_type_hub.import v.var_type) vars in
858
    type_of_type_list tyl
859

    
860
  let add_vdecl vd_env vdecl =
861
    if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env then
862
      raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
863
    else vdecl :: vd_env
864

    
865
  let check_vd_env vd_env = ignore (List.fold_left add_vdecl [] vd_env)
866

    
867
  let type_contract env c =
868
    let vd_env = c.consts @ c.locals in
869
    check_vd_env vd_env;
870
    let env =
871
      type_var_decl_list
872
        (* this argument seems useless to me, cf TODO at top of the file*)
873
        vd_env
874
        env
875
        vd_env
876
    in
877
    (* typing stmts *)
878
    let eqs =
879
      List.map (fun s -> match s with Eq eq -> eq | _ -> assert false) c.stmts
880
    in
881
    let undefined_vars_init =
882
      List.fold_left (fun uvs v -> ISet.add v.var_id uvs) ISet.empty c.locals
883
    in
884
    let _ =
885
      List.fold_left
886
        (type_eq (env, vd_env) false (*is_main*))
887
        undefined_vars_init
888
        eqs
889
    in
890
    (* Typing each predicate expr *)
891
    let type_pred_ee ee : unit =
892
      type_subtyping_arg
893
        (env, vd_env)
894
        false
895
        (* not in main *) false
896
        (* not a const *)
897
        ee.eexpr_qfexpr
898
        type_bool
899
    in
900
    List.iter
901
      type_pred_ee
902
      (c.assume @ c.guarantees
903
      @ List.flatten (List.map (fun m -> m.ensure @ m.require) c.modes));
904
    (*TODO enrich env locally with locals and consts type each pre/post as a
905
      boolean expr I don't know if we want to update the global env with locally
906
      typed variables. For the moment, returning the provided env *)
907
    env
908

    
909
  let rec type_spec env spec =
910
    match spec with Contract c -> type_contract env c | NodeSpec _ -> env
911

    
912
  (** [type_node env nd loc] types node [nd] in environment env. The location is
913
      used for error reports. *)
914
  and type_node env nd loc =
915
    (* Format.eprintf "Typing node %s@." nd.node_id; *)
916
    let is_main = nd.node_id = !Options.main_node in
917
    (* In contracts, outputs are considered as input values *)
918
    let vd_env_ol =
919
      if nd.node_iscontract then nd.node_locals
920
      else nd.node_outputs @ nd.node_locals
921
    in
922
    let vd_env = nd.node_inputs @ nd.node_outputs @ nd.node_locals in
923
    check_vd_env vd_env;
924
    let init_env = env in
925
    let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
926
    let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
927
    let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
928
    let new_env = Env.overwrite env delta_env in
929
    let undefined_vars_init =
930
      List.fold_left (fun uvs v -> ISet.add v.var_id uvs) ISet.empty vd_env_ol
931
    in
932
    let undefined_vars =
933
      let eqs, _ = get_node_eqs nd in
934
      (* TODO XXX: il faut typer les handlers de l'automate *)
935
      List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs
936
    in
937
    (* Typing asserts *)
938
    List.iter
939
      (fun assert_ ->
940
        let assert_expr = assert_.assert_expr in
941
        type_subtyping_arg
942
          (new_env, vd_env)
943
          is_main
944
          false
945
          assert_expr
946
          (* Type_predef. *)
947
          type_bool)
948
      nd.node_asserts;
949
    (* Typing spec/contracts *)
950
    (match nd.node_spec with
951
    | None ->
952
      ()
953
    | Some spec ->
954
      ignore (type_spec new_env spec));
955
    (* Typing annots *)
956
    List.iter
957
      (fun annot ->
958
        List.iter
959
          (fun (_, eexpr) -> ignore (type_eexpr (new_env, vd_env) eexpr))
960
          annot.annots)
961
      nd.node_annot;
962

    
963
    (* check that table is empty *)
964
    let local_consts =
965
      List.fold_left
966
        (fun res vdecl ->
967
          if vdecl.var_dec_const then ISet.add vdecl.var_id res else res)
968
        ISet.empty
969
        nd.node_locals
970
    in
971
    let undefined_vars = ISet.diff undefined_vars local_consts in
972

    
973
    if not (ISet.is_empty undefined_vars) then
974
      raise (Error (loc, Undefined_var undefined_vars));
975
    let ty_ins = type_of_vlist nd.node_inputs in
976
    let ty_outs = type_of_vlist nd.node_outputs in
977
    let ty_node = new_ty (Tarrow (ty_ins, ty_outs)) in
978
    generalize ty_node;
979
    (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
980
    nd.node_type <- Expr_type_hub.export ty_node;
981
    Env.add_value env nd.node_id ty_node
982

    
983
  let type_imported_node env nd _loc =
984
    let vd_env = nd.nodei_inputs @ nd.nodei_outputs in
985
    check_vd_env vd_env;
986
    let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in
987
    let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in
988
    let new_env = Env.overwrite env delta_env in
989
    (* Typing spec *)
990
    (match nd.nodei_spec with
991
    | None ->
992
      ()
993
    | Some spec ->
994
      ignore (type_spec new_env spec));
995
    let ty_ins = type_of_vlist nd.nodei_inputs in
996
    let ty_outs = type_of_vlist nd.nodei_outputs in
997
    let ty_node = new_ty (Tarrow (ty_ins, ty_outs)) in
998
    generalize ty_node;
999
    (* if (is_polymorphic ty_node) then raise (Error (loc, Poly_imported_node
1000
       nd.nodei_id)); *)
1001
    let new_env = Env.add_value env nd.nodei_id ty_node in
1002
    nd.nodei_type <- Expr_type_hub.export ty_node;
1003
    new_env
1004

    
1005
  let type_top_const env cdecl =
1006
    let ty = type_const cdecl.const_loc cdecl.const_value in
1007
    let d =
1008
      if is_dimension_type ty then
1009
        dimension_of_const cdecl.const_loc cdecl.const_value
1010
      else Dimension.mkdim_var ()
1011
    in
1012
    let ty =
1013
      (* Type_predef. *)
1014
      type_static d ty
1015
    in
1016
    let new_env = Env.add_value env cdecl.const_id ty in
1017
    cdecl.const_type <- Expr_type_hub.export ty;
1018
    new_env
1019

    
1020
  (* XXX: UNUSED *)
1021
  (* let type_top_consts env clist = List.fold_left type_top_const env clist *)
1022

    
1023
  let rec type_top_decl env decl =
1024
    match decl.top_decl_desc with
1025
    | Node nd -> (
1026
      try type_node env nd decl.top_decl_loc
1027
      with Error _ as exc ->
1028
        if !Options.global_inline then
1029
          Format.eprintf "Type error: failing node@.%a@.@?" Printers.pp_node nd;
1030
        raise exc)
1031
    | ImportedNode nd ->
1032
      type_imported_node env nd decl.top_decl_loc
1033
    | Const c ->
1034
      type_top_const env c
1035
    | TypeDef _ ->
1036
      List.fold_left type_top_decl env (consts_of_enum_type decl)
1037
    | Include _ | Open _ ->
1038
      env
1039

    
1040
  (* XXX: UNUSED *)
1041
  (* let get_type_of_call decl =
1042
   *   match decl.top_decl_desc with
1043
   *   | Node nd ->
1044
   *     let in_typ, out_typ = split_arrow (Expr_type_hub.import nd.node_type) in
1045
   *     type_list_of_type in_typ, type_list_of_type out_typ
1046
   *   | ImportedNode nd ->
1047
   *     let in_typ, out_typ = split_arrow (Expr_type_hub.import nd.nodei_type) in
1048
   *     type_list_of_type in_typ, type_list_of_type out_typ
1049
   *   | _ ->
1050
   *     assert false *)
1051

    
1052
  let type_prog env decls =
1053
    (* try *)
1054
    List.fold_left type_top_decl env decls
1055
  (* with Failure _ as exc -> raise exc *)
1056

    
1057
  (* Once the Lustre program is fully typed, we must get back to the original
1058
     description of dimensions, with constant parameters, instead of unifiable
1059
     internal variables. *)
1060

    
1061
  (* The following functions aims at 'unevaluating' dimension expressions
1062
     occuring in array types, i.e. replacing unifiable second_order variables
1063
     with the original static parameters. Once restored in this formulation,
1064
     dimensions may be meaningfully printed. *)
1065
  let uneval_vdecl_generics vdecl =
1066
    if vdecl.var_dec_const then
1067
      match get_static_value (Expr_type_hub.import vdecl.var_type) with
1068
      | None ->
1069
        Format.eprintf
1070
          "internal error: %a@."
1071
          (* Types. *) pp
1072
          (Expr_type_hub.import vdecl.var_type);
1073
        assert false
1074
      | Some d ->
1075
        Dimension.uneval vdecl.var_id d
1076

    
1077
  let uneval_node_generics vdecls = List.iter uneval_vdecl_generics vdecls
1078

    
1079
  (* XXX: UNUSED *)
1080
  (* let uneval_spec_generics spec =
1081
   *   List.iter uneval_vdecl_generics (spec.consts @ spec.locals) *)
1082

    
1083
  let uneval_top_generics decl =
1084
    match decl.top_decl_desc with
1085
    | Node nd ->
1086
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
1087
    | ImportedNode nd ->
1088
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
1089
    | Const _ | TypeDef _ | Open _ | Include _ ->
1090
      ()
1091

    
1092
  let uneval_prog_generics prog = List.iter uneval_top_generics prog
1093

    
1094
  let rec get_imported_symbol decls id =
1095
    match decls with
1096
    | [] ->
1097
      assert false
1098
    | decl :: q -> (
1099
      match decl.top_decl_desc with
1100
      | ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf ->
1101
        decl
1102
      | Const c when id = c.const_id && decl.top_decl_itf ->
1103
        decl
1104
      | TypeDef _ ->
1105
        get_imported_symbol (consts_of_enum_type decl @ q) id
1106
      | _ ->
1107
        get_imported_symbol q id)
1108

    
1109
  let check_env_compat header declared computed =
1110
    uneval_prog_generics header;
1111
    Env.iter declared (fun k decl_type_k ->
1112
        let top = get_imported_symbol header k in
1113
        let loc = top.top_decl_loc in
1114
        try
1115
          let computed_t = Env.lookup_value computed k in
1116
          let computed_t = instantiate (ref []) (ref []) computed_t in
1117
          (* Types.pp Format.std_formatter decl_type_k; Types.pp
1118
             Format.std_formatter computed_t;*)
1119
          try_unify ~sub:true ~semi:true decl_type_k computed_t loc
1120
        with Not_found -> (
1121
          (* If top is a contract we do not require the lustre file to provide
1122
             the same definition. *)
1123
          match top.top_decl_desc with
1124
          | Node nd -> (
1125
            match nd.node_spec with
1126
            | Some (Contract _) ->
1127
              ()
1128
            | _ ->
1129
              raise (Error (loc, Declared_but_undefined k)))
1130
          | _ ->
1131
            raise (Error (loc, Declared_but_undefined k))))
1132

    
1133
  let check_typedef_top decl =
1134
    (*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*)
1135
    (*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*)
1136
    (*Format.eprintf "%a" Corelang.pp_type_table ();*)
1137
    match decl.top_decl_desc with
1138
    | TypeDef ty -> (
1139
      let owner = decl.top_decl_owner in
1140
      let itf = decl.top_decl_itf in
1141
      let decl' =
1142
        try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id)
1143
        with Not_found ->
1144
          raise
1145
            (Error
1146
               ( decl.top_decl_loc,
1147
                 Declared_but_undefined ("type " ^ ty.tydef_id) ))
1148
      in
1149
      let owner' = decl'.top_decl_owner in
1150
      (*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*)
1151
      let itf' = decl'.top_decl_itf in
1152
      match decl'.top_decl_desc with
1153
      | Const _ | Node _ | ImportedNode _ ->
1154
        assert false
1155
      | TypeDef ty'
1156
        when coretype_equal ty'.tydef_desc ty.tydef_desc
1157
             && owner' = owner && itf && not itf' ->
1158
        ()
1159
      | _ ->
1160
        raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id)))
1161
    | _ ->
1162
      ()
1163

    
1164
  let check_typedef_compat header = List.iter check_typedef_top header
1165
end
1166

    
1167
module Expr_type_hub : EXPR_TYPE_HUB with type type_expr = Types.t = struct
1168
  type type_expr = Types.t
1169

    
1170
  let import x = x
1171

    
1172
  let export x = x
1173
end
1174

    
1175
include Make (Types) (Expr_type_hub)
1176

    
1177
(* Local Variables: *)
1178
(* compile-command:"make -C .." *)
1179
(* End: *)
(91-91/99)