Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ 0d54d8a8

History | View | Annotate | Download (37.2 KB)

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

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

    
29

    
30
module type EXPR_TYPE_HUB =
31
sig
32
  type type_expr 
33
  val import: Types.Main.type_expr -> type_expr
34
  val export: type_expr -> Types.Main.type_expr 
35
end
36

    
37
module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.type_expr) =  
38
  struct
39

    
40
    module TP = Type_predef.Make (T)
41
    include TP
42
    
43
    let pp_typing_env fmt env =
44
      Env.pp_env print_ty fmt env
45

    
46
    (****************************************************************)
47
    (* Generic functions: occurs, instantiate and generalize         *)
48
    (****************************************************************)
49
      
50
    (** [occurs tvar ty] returns true if the type variable [tvar]
51
       occurs in type [ty]. False otherwise. *)
52
    let rec occurs tvar ty =
53
      let ty = repr ty in
54
      match type_desc ty with
55
      | Tvar -> ty=tvar
56
      | Tarrow (t1, t2) ->
57
         (occurs tvar t1) || (occurs tvar t2)
58
      | Ttuple tl ->
59
         List.exists (occurs tvar) tl
60
      | Tstruct fl ->
61
         List.exists (fun (f, t) -> occurs tvar t) fl
62
      | Tarray (_, t)
63
        | Tstatic (_, t)
64
        | Tclock t
65
        | Tlink t -> occurs tvar t
66
      | Tenum _ | Tconst _ | Tunivar | Tbasic _ -> false
67

    
68
    (** Promote monomorphic type variables to polymorphic type
69
       variables. *)
70
    (* Generalize by side-effects *)
71
    let rec generalize ty =
72
      match type_desc ty with
73
      | Tvar ->
74
         (* No scopes, always generalize *)
75
         ty.tdesc <- Tunivar
76
      | Tarrow (t1,t2) ->
77
         generalize t1; generalize t2
78
      | Ttuple tl ->
79
         List.iter generalize tl
80
      | Tstruct fl ->
81
         List.iter (fun (f, t) -> generalize t) fl
82
      | Tstatic (d, t)
83
        | Tarray (d, t) -> Dimension.generalize d; generalize t
84
      | Tclock t
85
        | Tlink t ->
86
         generalize t
87
      | Tenum _ | Tconst _ | Tunivar | Tbasic _ -> ()
88

    
89
    (** Downgrade polymorphic type variables to monomorphic type
90
       variables *)
91
    let rec instantiate inst_vars inst_dim_vars ty =
92
      let ty = repr ty in
93
      match ty.tdesc with
94
      | Tenum _ | Tconst _ | Tvar | Tbasic _  -> ty
95
      | Tarrow (t1,t2) ->
96
         {ty with tdesc =
97
                    Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))}
98
      | Ttuple tlist ->
99
         {ty with tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist)}
100
      | Tstruct flist ->
101
         {ty with tdesc = Tstruct (List.map (fun (f, t) -> (f, instantiate inst_vars inst_dim_vars t)) flist)}
102
      | Tclock t ->
103
	 {ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t)}
104
      | Tstatic (d, t) ->
105
	 {ty with tdesc = Tstatic (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)}
106
      | Tarray (d, t) ->
107
	 {ty with tdesc = Tarray (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)}
108
      | Tlink t ->
109
	 (* should not happen *)
110
	 {ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t)}
111
      | Tunivar ->
112
         try
113
           List.assoc ty.tid !inst_vars
114
         with Not_found ->
115
           let var = new_var () in
116
	   inst_vars := (ty.tid, var)::!inst_vars;
117
	   var
118

    
119

    
120

    
121
    let basic_coretype_type t =
122
      if is_real_type t then Tydec_real else
123
        if is_int_type t then Tydec_int else
124
          if is_bool_type t then Tydec_bool else
125
	    assert false
126

    
127
    (* [type_coretype cty] types the type declaration [cty] *)
128
    let rec type_coretype type_dim cty =
129
      match (*get_repr_type*) cty with
130
      | Tydec_any -> new_var ()
131
      | Tydec_int -> type_int
132
      | Tydec_real -> (* Type_predef. *)type_real
133
      (* | Tydec_float -> Type_predef.type_real *)
134
      | Tydec_bool -> (* Type_predef. *)type_bool
135
      | Tydec_clock ty -> (* Type_predef. *)type_clock (type_coretype type_dim ty)
136
      | Tydec_const c -> (* Type_predef. *)type_const c
137
      | Tydec_enum tl -> (* Type_predef. *)type_enum tl
138
      | Tydec_struct fl -> (* Type_predef. *)type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl)
139
      | Tydec_array (d, ty) ->
140
         begin
141
           let d = Dimension.copy (ref []) d in
142
           type_dim d;
143
           (* Type_predef. *)type_array d (type_coretype type_dim ty)
144
         end
145

    
146
    (* [coretype_type] is the reciprocal of [type_typecore] *)
147
    let rec coretype_type ty =
148
      match (repr ty).tdesc with
149
      | Tvar           -> Tydec_any
150
      | Tbasic _       -> basic_coretype_type ty
151
      | Tconst c       -> Tydec_const c
152
      | Tclock t       -> Tydec_clock (coretype_type t)
153
      | Tenum tl       -> Tydec_enum tl
154
      | Tstruct fl     -> Tydec_struct (List.map (fun (f, t) -> (f, coretype_type t)) fl)
155
      | Tarray (d, t)  -> Tydec_array (d, coretype_type t)
156
      | Tstatic (_, t) -> coretype_type t
157
      | _         -> assert false
158

    
159
    let get_coretype_definition tname =
160
      try
161
        let top = Hashtbl.find type_table (Tydec_const tname) in
162
        match top.top_decl_desc with
163
        | TypeDef tdef -> tdef.tydef_desc
164
        | _ -> assert false
165
      with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
166

    
167
    let get_type_definition tname =
168
      type_coretype (fun d -> ()) (get_coretype_definition tname)
169

    
170
    (* Equality on ground types only *)
171
    (* Should be used between local variables which must have a ground type *)
172
    let rec eq_ground t1 t2 =
173
      let t1 = repr t1 in
174
      let t2 = repr t2 in
175
      t1==t2 ||
176
        match t1.tdesc, t2.tdesc with
177
        | Tbasic t1, Tbasic t2 when t1 == t2 -> true
178
        | Tenum tl, Tenum tl' when tl == tl' -> true
179
        | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> List.for_all2 eq_ground tl tl'
180
        | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' -> List.for_all2 (fun (_, t) (_, t') -> eq_ground t t') fl fl'
181
        | (Tconst t, _) ->
182
           let def_t = get_type_definition t in
183
           eq_ground def_t t2
184
        | (_, Tconst t)  ->
185
           let def_t = get_type_definition t in
186
           eq_ground t1 def_t
187
        | Tarrow (t1,t2), Tarrow (t1',t2') -> eq_ground t1 t1' && eq_ground t2 t2'
188
        | Tclock t1', Tclock t2' -> eq_ground t1' t2'
189
        | Tstatic (e1, t1'), Tstatic (e2, t2')
190
          | Tarray (e1, t1'), Tarray (e2, t2') -> Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'
191
        | _ -> false
192

    
193
    (** [unify t1 t2] unifies types [t1] and [t2]
194
    using standard destructive unification.
195
    Raises [Unify (t1,t2)] if the types are not unifiable.
196
    [t1] is a expected/formal/spec type, [t2] is a computed/real/implem type,
197
    so in case of unification error: expected type [t1], got type [t2].
198
    If [sub]-typing is allowed, [t2] may be a subtype of [t1].
199
    If [semi] unification is required,
200
    [t1] should furthermore be an instance of [t2]
201
    and constants are handled differently.*)
202
    let unify ?(sub=false) ?(semi=false) t1 t2 =
203
      let rec unif t1 t2 =
204
        let t1 = repr t1 in
205
        let t2 = repr t2 in
206
        if t1==t2 then
207
          ()
208
        else
209
          match t1.tdesc,t2.tdesc with
210
          (* strictly subtyping cases first *)
211
          | _ , Tclock t2 when sub && (get_clock_base_type t1 = None) ->
212
	     unif t1 t2
213
          | _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) ->
214
	     unif t1 t2
215
          (* This case is not mandatory but will keep "older" types *)
216
          | Tvar, Tvar ->
217
             if t1.tid < t2.tid then
218
               t2.tdesc <- Tlink t1
219
             else
220
               t1.tdesc <- Tlink t2
221
          | Tvar, _ when (not semi) && (not (occurs t1 t2)) ->
222
             t1.tdesc <- Tlink t2
223
          | _, Tvar when (not (occurs t2 t1)) ->
224
             t2.tdesc <- Tlink t1
225
          | Tarrow (t1,t2), Tarrow (t1',t2') ->
226
	     begin
227
               unif t2 t2';
228
	       unif t1' t1
229
	     end
230
          | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
231
	     List.iter2 unif tl tl'
232
          | Ttuple [t1]        , _                  -> unif t1 t2
233
          | _                  , Ttuple [t2]        -> unif t1 t2
234
          | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
235
	     List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'
236
          | Tclock _, Tstatic _
237
            | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
238
          | Tclock t1', Tclock t2' -> unif t1' t2'
239
          | Tbasic t1, Tbasic t2 when t1 == t2 -> ()
240
          | Tunivar, _ | _, Tunivar -> ()
241
          | (Tconst t, _) ->
242
	     let def_t = get_type_definition t in
243
	     unif def_t t2
244
          | (_, Tconst t)  ->
245
	     let def_t = get_type_definition t in
246
	     unif t1 def_t
247
          | Tenum tl, Tenum tl' when tl == tl' -> ()
248
          | Tstatic (e1, t1'), Tstatic (e2, t2')
249
            | Tarray (e1, t1'), Tarray (e2, t2') ->
250
	     let eval_const =
251
	       if semi
252
	       then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c))
253
	       else (fun c -> None) in
254
	     begin
255
	       unif t1' t2';
256
	       Dimension.eval Basic_library.eval_env eval_const e1;
257
	       Dimension.eval Basic_library.eval_env eval_const e2;
258
	       Dimension.unify ~semi:semi e1 e2;
259
	     end
260
          (* Special cases for machine_types. Rules to unify static types infered
261
      	 for numerical constants with non static ones for variables with
262
      	 possible machine types *)
263
          | Tbasic bt1, Tbasic bt2 when BasicT.is_unifiable bt1 bt2 -> BasicT.unify bt1 bt2
264
          | _,_ -> raise (Unify (t1, t2))
265
      in unif t1 t2
266

    
267
    (* Expected type ty1, got type ty2 *)
268
    let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =
269
      try
270
        unify ~sub:sub ~semi:semi ty1 ty2
271
      with
272
      | Unify _ ->
273
         raise (Error (loc, Type_clash (ty1,ty2)))
274
      | Dimension.Unify _ ->
275
         raise (Error (loc, Type_clash (ty1,ty2)))
276

    
277

    
278
    (************************************************)
279
    (* Typing function for each basic AST construct *)
280
    (************************************************)
281

    
282
    let rec type_struct_const_field ?(is_annot=false) loc (label, c) =
283
      if Hashtbl.mem field_table label
284
      then let tydef = Hashtbl.find field_table label in
285
           let tydec = (typedef_of_top tydef).tydef_desc in 
286
           let tydec_struct = get_struct_type_fields tydec in
287
           let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
288
           begin
289
	     try_unify ty_label (type_const ~is_annot loc c) loc;
290
	     type_coretype (fun d -> ()) tydec
291
           end
292
      else raise (Error (loc, Unbound_value ("struct field " ^ label)))
293

    
294
    and type_const ?(is_annot=false) loc c = 
295
      match c with
296
      | Const_int _     -> (* Type_predef. *)type_int
297
      | Const_real _    -> (* Type_predef. *)type_real
298
      | Const_array ca  -> let d = Dimension.mkdim_int loc (List.length ca) in
299
		           let ty = new_var () in
300
		           List.iter (fun e -> try_unify ty (type_const ~is_annot loc e) loc) ca;
301
		           (* Type_predef. *)type_array d ty
302
      | Const_tag t     ->
303
         if Hashtbl.mem tag_table t
304
         then 
305
           let tydef = typedef_of_top (Hashtbl.find tag_table t) in
306
           let tydec =
307
	     if is_user_type tydef.tydef_desc
308
	     then Tydec_const tydef.tydef_id
309
	     else tydef.tydef_desc in
310
           type_coretype (fun d -> ()) tydec
311
         else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
312
      | Const_struct fl ->
313
         let ty_struct = new_var () in
314
         begin
315
           let used =
316
	     List.fold_left
317
	       (fun acc (l, c) ->
318
	         if List.mem l acc
319
	         then raise (Error (loc, Already_bound ("struct field " ^ l)))
320
	         else try_unify ty_struct (type_struct_const_field ~is_annot loc (l, c)) loc; l::acc)
321
	       [] fl in
322
           try
323
	     let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in
324
             (*	List.iter (fun l -> Format.eprintf "total: %s@." l) total;
325
	List.iter (fun l -> Format.eprintf "used: %s@." l) used; *)
326
	     let undef = List.find (fun l -> not (List.mem l used)) total
327
	     in raise (Error (loc, Unbound_value ("struct field " ^ undef)))
328
           with Not_found -> 
329
	     ty_struct
330
         end
331
      | Const_string _ | Const_modeid _     -> 
332
         if is_annot then (* Type_predef. *)type_string else  assert false (* string datatype should only appear in annotations *)
333

    
334
    (* The following typing functions take as parameter an environment [env]
335
   and whether the element being typed is expected to be constant [const]. 
336
   [env] is a pair composed of:
337
  - a map from ident to type, associating to each ident, i.e. 
338
    variables, constants and (imported) nodes, its type including whether
339
    it is constant or not. This latter information helps in checking constant 
340
    propagation policy in Lustre.
341
  - a vdecl list, in order to modify types of declared variables that are
342
    later discovered to be clocks during the typing process.
343
     *)
344
    let check_constant loc const_expected const_real =
345
      if const_expected && not const_real
346
      then raise (Error (loc, Not_a_constant))
347

    
348
    let rec type_add_const env const arg targ =
349
      (*Format.eprintf "Typing.type_add_const %a %a@." Printers.pp_expr arg Types.print_ty targ;*)
350
      if const
351
      then let d =
352
	     if is_dimension_type targ
353
	     then dimension_of_expr arg
354
	     else Dimension.mkdim_var () in
355
           let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in
356
           Dimension.eval Basic_library.eval_env eval_const d;
357
           let real_static_type = (* Type_predef. *)type_static d ((* Types. *)dynamic_type targ) in
358
           (match (* Types. *)get_static_value targ with
359
            | None    -> ()
360
            | Some d' -> try_unify targ real_static_type arg.expr_loc);
361
           real_static_type
362
      else targ
363

    
364
    (* emulates a subtyping relation between types t and (d : t),
365
   used during node applications and assignments *)
366
    and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
367
      let loc = real_arg.expr_loc in
368
      let const = const || ((* Types. *)get_static_value formal_type <> None) in
369
      let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in
370
      (*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*)
371
      try_unify ~sub:sub formal_type real_type loc
372

    
373
    (* typing an application implies:
374
   - checking that const formal parameters match real const (maybe symbolic) arguments
375
   - checking type adequation between formal and real arguments
376
   An application may embed an homomorphic/internal function, in which case we need to split
377
   it in many calls
378
     *)
379
    and type_appl env in_main loc const f args =
380
      let targs = List.map (type_expr env in_main const) args in
381
      if Basic_library.is_homomorphic_fun f && List.exists is_tuple_type targs
382
      then
383
        try
384
          let targs = Utils.transpose_list (List.map type_list_of_type targs) in
385
          (* Types. *)type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)
386
        with 
387
          Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l')))
388
	                                
389
      else (
390
        type_dependent_call env in_main loc const f (List.combine args targs)
391
      )
392

    
393
    (* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)
394
    and type_dependent_call env in_main loc const f targs =
395
      (* Format.eprintf "Typing.type_dependent_call %s@." f; *)
396
      let tins, touts = new_var (), new_var () in
397
      (* Format.eprintf "tin=%a, tout=%a@." print_ty tins print_ty touts; *)
398
      let tfun = (* Type_predef. *)type_arrow tins touts in
399
      (* Format.eprintf "fun=%a@." print_ty tfun; *)
400
      type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
401
      (* Format.eprintf "type subtyping@."; *)
402
      let tins = type_list_of_type tins in
403
      if List.length targs <> List.length tins then
404
        raise (Error (loc, WrongArity (List.length tins, List.length targs)))
405
      else
406
        begin
407
          List.iter2 (
408
	      fun (a,t) ti ->
409
	      let t' = type_add_const env (const || (* Types. *)get_static_value ti <> None) a t in
410
	      (* Format.eprintf "uniying ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts;  *)
411
	      try_unify ~sub:true ti t' a.expr_loc;
412
	    (* Format.eprintf "unified ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts;  *)
413
	      
414
            )
415
	    targs
416
	    tins;
417
          touts
418
        end
419

    
420
    (* type a simple call without dependent types 
421
   but possible homomorphic extension.
422
   [targs] is here a list of arguments' types. *)
423
    and type_simple_call env in_main loc const f targs =
424
      let tins, touts = new_var (), new_var () in
425
      let tfun = (* Type_predef. *)type_arrow tins touts in
426
      type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
427
      (*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*)
428
      try_unify ~sub:true tins (type_of_type_list targs) loc;
429
      touts
430

    
431
    (** [type_expr env in_main expr] types expression [expr] in environment
432
    [env], expecting it to be [const] or not. *)
433
    and type_expr ?(is_annot=false) env in_main const expr =
434
      let resulting_ty = 
435
        match expr.expr_desc with
436
        | Expr_const c ->
437
           let ty = type_const ~is_annot expr.expr_loc c in
438
           let ty = (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty in
439
           expr.expr_type <- Expr_type_hub.export ty;
440
           ty
441
        | Expr_ident v ->
442
           let tyv =
443
             try
444
               Env.lookup_value (fst env) v
445
             with Not_found ->
446
	       Format.eprintf "Failure in typing expr %a. Not in typing environement@." Printers.pp_expr expr;
447
               raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))
448
           in
449
           let ty = instantiate (ref []) (ref []) tyv in
450
           let ty' =
451
             if const
452
             then (* Type_predef. *)type_static (Dimension.mkdim_var ()) (new_var ())
453
             else new_var () in
454
           try_unify ty ty' expr.expr_loc;
455
           expr.expr_type <- Expr_type_hub.export ty;
456
           ty 
457
        | Expr_array elist ->
458
           let ty_elt = new_var () in
459
           List.iter (fun e -> try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist;
460
           let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
461
           let ty = (* Type_predef. *)type_array d ty_elt in
462
           expr.expr_type <- Expr_type_hub.export ty;
463
           ty
464
        | Expr_access (e1, d) ->
465
           type_subtyping_arg env in_main false (* not necessary a constant *) (expr_of_dimension d) (* Type_predef. *)type_int;
466
           let ty_elt = new_var () in
467
           let d = Dimension.mkdim_var () in
468
           type_subtyping_arg env in_main const e1 ((* Type_predef. *)type_array d ty_elt);
469
           expr.expr_type <- Expr_type_hub.export ty_elt;
470
           ty_elt
471
        | Expr_power (e1, d) ->
472
           let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in
473
           type_subtyping_arg env in_main true (expr_of_dimension d) (* Type_predef. *)type_int;
474
           Dimension.eval Basic_library.eval_env eval_const d;
475
           let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in
476
           let ty = (* Type_predef. *)type_array d ty_elt in
477
           expr.expr_type <- Expr_type_hub.export ty;
478
           ty
479
        | Expr_tuple elist ->
480
           let ty = new_ty (Ttuple (List.map (type_expr ~is_annot env in_main const) elist)) in
481
           expr.expr_type <- Expr_type_hub.export ty;
482
           ty
483
        | Expr_ite (c, t, e) ->
484
           type_subtyping_arg env in_main const c (* Type_predef. *)type_bool;
485
           let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in
486
           expr.expr_type <- Expr_type_hub.export ty;
487
           ty
488
        | Expr_appl (id, args, r) ->
489
           (* application of non internal function is not legal in a constant
490
       expression *)
491
           (match r with
492
            | None        -> ()
493
            | Some c -> 
494
               check_constant expr.expr_loc const false;	
495
               type_subtyping_arg env in_main const c (* Type_predef. *)type_bool);
496
           let args_list = expr_list_of_expr args in
497
           let targs = new_ty (Ttuple (List.map (fun a -> Expr_type_hub.import a.expr_type) args_list)) in
498
           args.expr_type <- Expr_type_hub.export targs;
499
           let touts = type_appl env in_main expr.expr_loc const id args_list in
500
           expr.expr_type <- Expr_type_hub.export touts;
501
           touts
502
        | Expr_fby (e1,e2)
503
          | Expr_arrow (e1,e2) ->
504
           (* fby/arrow is not legal in a constant expression *)
505
           check_constant expr.expr_loc const false;
506
           let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in
507
           expr.expr_type <- Expr_type_hub.export ty;
508
           ty
509
        | Expr_pre e ->
510
           (* pre is not legal in a constant expression *)
511
           check_constant expr.expr_loc const false;
512
           let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in
513
           expr.expr_type <- Expr_type_hub.export ty;
514
           ty
515
        | Expr_when (e1,c,l) ->
516
           (* when is not legal in a constant expression *)
517
           check_constant expr.expr_loc const false;
518
           let typ_l = (* Type_predef. *)type_clock (type_const ~is_annot expr.expr_loc (Const_tag l)) in
519
           let expr_c = expr_of_ident c expr.expr_loc in
520
           type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
521
           let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in
522
           expr.expr_type <- Expr_type_hub.export ty;
523
           ty
524
        | Expr_merge (c,hl) ->
525
           (* merge is not legal in a constant expression *)
526
           check_constant expr.expr_loc const false;
527
           let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in
528
           let expr_c = expr_of_ident c expr.expr_loc in
529
           let typ_l = (* Type_predef. *)type_clock typ_in in
530
           type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
531
           expr.expr_type <- Expr_type_hub.export typ_out;
532
           typ_out
533
      in 
534
      Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr (* Types. *)print_ty resulting_ty);
535
      resulting_ty
536

    
537
    and type_branches ?(is_annot=false) env in_main loc const hl =
538
      let typ_in = new_var () in
539
      let typ_out = new_var () in
540
      try
541
        let used_labels =
542
          List.fold_left (fun accu (t, h) ->
543
	      unify typ_in (type_const ~is_annot loc (Const_tag t));
544
	      type_subtyping_arg env in_main const h typ_out;
545
	      if List.mem t accu
546
	      then raise (Error (loc, Already_bound t))
547
	      else t :: accu) [] hl in
548
        let type_labels = get_enum_type_tags (coretype_type typ_in) in
549
        if List.sort compare used_labels <> List.sort compare type_labels
550
        then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in
551
	     raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
552
        else (typ_in, typ_out)
553
      with Unify (t1, t2) ->
554
        raise (Error (loc, Type_clash (t1,t2)))
555

    
556
    (* Eexpr are always in annotations. TODO: add the quantifiers variables to the env *)
557
    let type_eexpr env eexpr = 
558
      (type_expr
559
         ~is_annot:true
560
         env
561
         false (* not in main *)
562
         false (* not a const *)
563
         eexpr.eexpr_qfexpr)
564

    
565

    
566
    (** [type_eq env eq] types equation [eq] in environment [env] *)
567
    let type_eq env in_main undefined_vars eq =
568
      (*Format.eprintf "Typing.type_eq %a@." Printers.pp_node_eq eq;*)
569
      (* Check undefined variables, type lhs *)
570
      let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in
571
      let ty_lhs = type_expr env in_main false expr_lhs in
572
      (* Check multiple variable definitions *)
573
      let define_var id uvars =
574
        if ISet.mem id uvars
575
        then ISet.remove id uvars
576
        else raise (Error (eq.eq_loc, Already_defined id))
577
      in
578
      (* check assignment of declared constant, assignment of clock *)
579
      let ty_lhs =
580
        type_of_type_list
581
          (List.map2 (fun ty id ->
582
	       if get_static_value ty <> None
583
	       then raise (Error (eq.eq_loc, Assigned_constant id)) else
584
	         match get_clock_base_type ty with
585
	         | None -> ty
586
	         | Some ty -> ty)
587
	     (type_list_of_type ty_lhs) eq.eq_lhs) in
588
      let undefined_vars =
589
        List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
590
      (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
591
     to a (always non-constant) lhs variable *)
592
      type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
593
      undefined_vars
594

    
595

    
596
    (* [type_coreclock env ck id loc] types the type clock declaration [ck]
597
   in environment [env] *)
598
    let type_coreclock env ck id loc =
599
      match ck.ck_dec_desc with
600
      | Ckdec_any -> ()
601
      | Ckdec_bool cl ->
602
         let dummy_id_expr = expr_of_ident id loc in
603
         let when_expr =
604
           List.fold_left
605
             (fun expr (x, l) ->
606
               {expr_tag = new_tag ();
607
                expr_desc= Expr_when (expr,x,l);
608
                expr_type = Types.Main.new_var ();
609
                expr_clock = Clocks.new_var true;
610
                expr_delay = Delay.new_var ();
611
                expr_loc=loc;
612
		expr_annot = None})
613
             dummy_id_expr cl
614
         in
615
         ignore (type_expr env false false when_expr)
616

    
617
    let rec check_type_declaration loc cty =
618
      match cty with
619
      | Tydec_clock ty
620
        | Tydec_array (_, ty) -> check_type_declaration loc ty
621
      | Tydec_const tname   ->
622
         (* Format.eprintf "TABLE: %a@." print_type_table (); *)
623
         if not (Hashtbl.mem type_table cty)
624
         then raise (Error (loc, Unbound_type tname));
625
      | _                   -> ()
626

    
627
    let type_var_decl vd_env env vdecl =
628
      (*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*)
629
      check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
630
      let eval_const id = (* Types. *)get_static_value (Env.lookup_value env id) in
631
      let type_dim d =
632
        begin
633
          type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) (* Type_predef. *)type_int;
634
          Dimension.eval Basic_library.eval_env eval_const d;
635
        end in
636
      let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
637

    
638
      let ty_static =
639
        if vdecl.var_dec_const
640
        then (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty
641
        else ty in
642
      (match vdecl.var_dec_value with
643
       | None   -> ()
644
       | Some v -> type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static);
645
      try_unify ty_static (Expr_type_hub.import vdecl.var_type) vdecl.var_loc;
646
      let new_env = Env.add_value env vdecl.var_id ty_static in
647
      type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
648
      (*Format.eprintf "END %a@." Types.print_ty ty_static;*)
649
      new_env
650

    
651
    let type_var_decl_list vd_env env l =
652
      List.fold_left (type_var_decl vd_env) env l
653

    
654
    let type_of_vlist vars =
655
      let tyl = List.map (fun v -> Expr_type_hub.import v.var_type) vars in
656
      type_of_type_list tyl
657

    
658
    let add_vdecl vd_env vdecl =
659
      if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
660
      then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
661
      else vdecl::vd_env
662

    
663
    let check_vd_env vd_env =
664
      ignore (List.fold_left add_vdecl [] vd_env)
665

    
666
    let type_spec env c =
667
      (*TODO 
668
        enrich env locally with locals and consts
669
        type each pre/post as a boolean expr
670
        I don't know if we want to update the global env with locally typed variables. 
671
        For the moment, returning the provided env           
672
       *)
673
      env
674
      
675
    (** [type_node env nd loc] types node [nd] in environment env. The
676
    location is used for error reports. *)
677
    let type_node env nd loc =
678
      let is_main = nd.node_id = !Options.main_node in
679
      let vd_env_ol = nd.node_outputs@nd.node_locals in
680
      let vd_env =  nd.node_inputs@vd_env_ol in
681
      check_vd_env vd_env;
682
      let init_env = env in
683
      let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
684
      let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
685
      let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
686
      let new_env = Env.overwrite env delta_env in
687
      let undefined_vars_init =
688
        List.fold_left
689
          (fun uvs v -> ISet.add v.var_id uvs)
690
          ISet.empty vd_env_ol in
691
      let undefined_vars =
692
        let eqs, auts = get_node_eqs nd in
693
        (* TODO XXX: il faut typer les handlers de l'automate *)
694
        List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs
695
      in
696
      (* Typing asserts *)
697
      List.iter (fun assert_ ->
698
          let assert_expr =  assert_.assert_expr in
699
          type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool
700
        )  nd.node_asserts;
701
      (* Typing spec/contracts *)
702
      (match nd.node_spec with None -> () | Some spec -> ignore (type_spec (new_env, vd_env) spec));
703
      (* Typing annots *)
704
      List.iter (fun annot ->
705
          List.iter (fun (_, eexpr) -> ignore (type_eexpr (new_env, vd_env) eexpr)) annot.annots
706
        ) nd.node_annot;
707
      
708
      (* check that table is empty *)
709
      let local_consts = List.fold_left (fun res vdecl -> if vdecl.var_dec_const then ISet.add vdecl.var_id res else res) ISet.empty nd.node_locals in
710
      let undefined_vars = ISet.diff undefined_vars local_consts in
711
      if (not (ISet.is_empty undefined_vars)) then
712
        raise (Error (loc, Undefined_var undefined_vars));
713
      let ty_ins = type_of_vlist nd.node_inputs in
714
      let ty_outs = type_of_vlist nd.node_outputs in
715
      let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
716
      generalize ty_node;
717
      (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
718
      nd.node_type <- Expr_type_hub.export ty_node;
719
      Env.add_value env nd.node_id ty_node
720

    
721
    let type_imported_node env nd loc =
722
      let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
723
      let vd_env = nd.nodei_inputs@nd.nodei_outputs in
724
      check_vd_env vd_env;
725
      ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
726
      let ty_ins = type_of_vlist nd.nodei_inputs in
727
      let ty_outs = type_of_vlist nd.nodei_outputs in
728
      let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
729
      generalize ty_node;
730
      (*
731
  if (is_polymorphic ty_node) then
732
    raise (Error (loc, Poly_imported_node nd.nodei_id));
733
       *)
734
      let new_env = Env.add_value env nd.nodei_id ty_node in
735
      nd.nodei_type <- Expr_type_hub.export ty_node;
736
      new_env
737

    
738
    let type_top_const env cdecl =
739
      let ty = type_const cdecl.const_loc cdecl.const_value in
740
      let d =
741
        if is_dimension_type ty
742
        then dimension_of_const cdecl.const_loc cdecl.const_value
743
        else Dimension.mkdim_var () in
744
      let ty = (* Type_predef. *)type_static d ty in
745
      let new_env = Env.add_value env cdecl.const_id ty in
746
      cdecl.const_type <- Expr_type_hub.export ty;
747
      new_env
748

    
749
    let type_top_consts env clist =
750
      List.fold_left type_top_const env clist
751

    
752
    let rec type_top_decl env decl =
753
      match decl.top_decl_desc with
754
      | Node nd -> (
755
        try
756
          type_node env nd decl.top_decl_loc
757
        with Error (loc, err) as exc -> (
758
          if !Options.global_inline then
759
	    Format.eprintf "Type error: failing node@.%a@.@?"
760
	      Printers.pp_node nd
761
          ;
762
            raise exc)
763
      )
764
      | ImportedNode nd ->
765
         type_imported_node env nd decl.top_decl_loc
766
      | Const c ->
767
         type_top_const env c
768
      | TypeDef _ -> List.fold_left type_top_decl env (consts_of_enum_type decl)
769
      | Open _  -> env
770
    
771
    let get_type_of_call decl =
772
      match decl.top_decl_desc with
773
      | Node nd         ->
774
         let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.node_type) in
775
         type_list_of_type in_typ, type_list_of_type out_typ
776
      | ImportedNode nd ->
777
         let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.nodei_type) in
778
         type_list_of_type in_typ, type_list_of_type out_typ
779
      | _               -> assert false
780

    
781
    let type_prog env decls =
782
      try
783
        List.fold_left type_top_decl env decls
784
      with Failure _ as exc -> raise exc
785

    
786
    (* Once the Lustre program is fully typed, we must get back to the
787
       original description of dimensions, with constant parameters,
788
       instead of unifiable internal variables. *)
789

    
790
    (* The following functions aims at 'unevaluating' dimension
791
       expressions occuring in array types, i.e. replacing unifiable
792
       second_order variables with the original static parameters.
793
       Once restored in this formulation, dimensions may be
794
       meaningfully printed.  *)
795
    let uneval_vdecl_generics vdecl =
796
      if vdecl.var_dec_const
797
      then
798
        match get_static_value (Expr_type_hub.import vdecl.var_type) with
799
        | None   -> (Format.eprintf "internal error: %a@." (* Types. *)print_ty (Expr_type_hub.import vdecl.var_type); assert false)
800
        | Some d -> Dimension.uneval vdecl.var_id d
801

    
802
    let uneval_node_generics vdecls =
803
      List.iter uneval_vdecl_generics vdecls
804

    
805
    let uneval_spec_generics spec =
806
      List.iter uneval_vdecl_generics (spec.consts@spec.locals)
807
      
808
    let uneval_top_generics decl =
809
      match decl.top_decl_desc with
810
      | Node nd ->
811
         uneval_node_generics (nd.node_inputs @ nd.node_outputs)
812
      | ImportedNode nd ->
813
         uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
814
      | Const _
815
        | TypeDef _
816
        | Open _
817
        -> ()
818

    
819
    let uneval_prog_generics prog =
820
      List.iter uneval_top_generics prog
821

    
822
    let rec get_imported_symbol decls id =
823
      match decls with
824
      | [] -> assert false
825
      | decl::q ->
826
         (match decl.top_decl_desc with
827
          | ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf -> decl
828
          | Const c when id = c.const_id && decl.top_decl_itf -> decl
829
          | TypeDef _ -> get_imported_symbol (consts_of_enum_type decl @ q) id
830
          | _ -> get_imported_symbol q id)
831

    
832
    let check_env_compat header declared computed = 
833
      uneval_prog_generics header;
834
      Env.iter declared (fun k decl_type_k ->
835
          let loc = (get_imported_symbol header k).top_decl_loc in 
836
          let computed_t =
837
            instantiate (ref []) (ref []) 
838
	      (try Env.lookup_value computed k
839
	       with Not_found -> raise (Error (loc, Declared_but_undefined k))) in
840
          (*Types.print_ty Format.std_formatter decl_type_k;
841
      Types.print_ty Format.std_formatter computed_t;*)
842
          try_unify ~sub:true ~semi:true decl_type_k computed_t loc
843
        )
844

    
845
    let check_typedef_top decl =
846
      (*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*)
847
      (*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*)
848
      (*Format.eprintf "%a" Corelang.print_type_table ();*)
849
      match decl.top_decl_desc with
850
      | TypeDef ty ->
851
         let owner = decl.top_decl_owner in
852
         let itf = decl.top_decl_itf in
853
         let decl' =
854
           try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id)
855
           with Not_found -> raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in
856
         let owner' = decl'.top_decl_owner in
857
         (*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*)
858
         let itf' = decl'.top_decl_itf in
859
         (match decl'.top_decl_desc with
860
          | Const _ | Node _ | ImportedNode _ -> assert false
861
          | TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') -> ()
862
          | _ -> raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id)))
863
      | _  -> ()
864

    
865
    let check_typedef_compat header =
866
      List.iter check_typedef_top header
867
  end
868

    
869
include  Make(Types.Main) (struct
870
             type type_expr  = Types.Main.type_expr
871
             let import x = x
872
             let export x = x
873
           end)
874
             (* Local Variables: *)
875
             (* compile-command:"make -C .." *)
876
(* End: *)