Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ 59020713

History | View | Annotate | Download (38.6 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
(* TODO general remark: except in the add_vdecl, it seems to me that
31
   all the pairs (env, vd_env) should be replace with just env, since
32
   vd_env is never used and the env element is always extract with a
33
   fst *)
34

    
35
   
36
module type EXPR_TYPE_HUB =
37
sig
38
  type type_expr 
39
  val import: Types.Main.type_expr -> type_expr
40
  val export: type_expr -> Types.Main.type_expr 
41
end
42

    
43
module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.type_expr) =  
44
  struct
45

    
46
    module TP = Type_predef.Make (T)
47
    include TP
48
    
49
    let pp_typing_env fmt env =
50
      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]
57
       occurs in type [ty]. False otherwise. *)
58
    let rec occurs tvar ty =
59
      let ty = repr ty in
60
      match type_desc ty with
61
      | Tvar -> ty=tvar
62
      | Tarrow (t1, t2) ->
63
         (occurs tvar t1) || (occurs tvar t2)
64
      | Ttuple tl ->
65
         List.exists (occurs tvar) tl
66
      | Tstruct fl ->
67
         List.exists (fun (f, t) -> occurs tvar t) fl
68
      | Tarray (_, t)
69
        | Tstatic (_, t)
70
        | Tclock t
71
        | Tlink t -> occurs tvar t
72
      | Tenum _ | Tconst _ | Tunivar | Tbasic _ -> false
73

    
74
    (** Promote monomorphic type variables to polymorphic type
75
       variables. *)
76
    (* Generalize by side-effects *)
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; generalize t2
84
      | Ttuple tl ->
85
         List.iter generalize tl
86
      | Tstruct fl ->
87
         List.iter (fun (f, t) -> generalize t) fl
88
      | Tstatic (d, t)
89
        | Tarray (d, t) -> Dimension.generalize d; generalize t
90
      | Tclock t
91
        | Tlink t ->
92
         generalize t
93
      | Tenum _ | Tconst _ | Tunivar | Tbasic _ -> ()
94

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

    
125

    
126

    
127
    let basic_coretype_type t =
128
      if is_real_type t then Tydec_real else
129
        if is_int_type t then Tydec_int else
130
          if is_bool_type t then Tydec_bool else
131
	    assert false
132

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

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

    
165
    let get_coretype_definition tname =
166
      try
167
        let top = Hashtbl.find type_table (Tydec_const tname) in
168
        match top.top_decl_desc with
169
        | TypeDef tdef -> tdef.tydef_desc
170
        | _ -> assert false
171
      with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
172

    
173
    let get_type_definition tname =
174
      type_coretype (fun d -> ()) (get_coretype_definition tname)
175

    
176
    (* Equality on ground types only *)
177
    (* Should be used between local variables which must have a ground type *)
178
    let rec eq_ground t1 t2 =
179
      let t1 = repr t1 in
180
      let t2 = repr t2 in
181
      t1==t2 ||
182
        match t1.tdesc, t2.tdesc with
183
        | Tbasic t1, Tbasic t2 when t1 == t2 -> true
184
        | Tenum tl, Tenum tl' when tl == tl' -> true
185
        | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> List.for_all2 eq_ground tl tl'
186
        | 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'
187
        | (Tconst t, _) ->
188
           let def_t = get_type_definition t in
189
           eq_ground def_t t2
190
        | (_, Tconst t)  ->
191
           let def_t = get_type_definition t in
192
           eq_ground t1 def_t
193
        | Tarrow (t1,t2), Tarrow (t1',t2') -> eq_ground t1 t1' && eq_ground t2 t2'
194
        | Tclock t1', Tclock t2' -> eq_ground t1' t2'
195
        | Tstatic (e1, t1'), Tstatic (e2, t2')
196
          | Tarray (e1, t1'), Tarray (e2, t2') -> Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'
197
        | _ -> false
198

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

    
273
    (* Expected type ty1, got type ty2 *)
274
    let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =
275
      try
276
        unify ~sub:sub ~semi:semi ty1 ty2
277
      with
278
      | Unify _ ->
279
         raise (Error (loc, Type_clash (ty1,ty2)))
280
      | Dimension.Unify _ ->
281
         raise (Error (loc, Type_clash (ty1,ty2)))
282

    
283

    
284
    (************************************************)
285
    (* Typing function for each basic AST construct *)
286
    (************************************************)
287

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

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

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

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

    
370
    (* emulates a subtyping relation between types t and (d : t),
371
   used during node applications and assignments *)
372
    and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
373
      let loc = real_arg.expr_loc in
374
      let const = const || ((* Types. *)get_static_value formal_type <> None) in
375
      let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in
376
      (*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;*)
377
      try_unify ~sub:sub formal_type real_type loc
378

    
379
    (* typing an application implies:
380
   - checking that const formal parameters match real const (maybe symbolic) arguments
381
   - checking type adequation between formal and real arguments
382
   An application may embed an homomorphic/internal function, in which case we need to split
383
   it in many calls
384
     *)
385
    and type_appl env in_main loc const f args =
386
      let targs = List.map (type_expr env in_main const) args in
387
      if Basic_library.is_homomorphic_fun f && List.exists is_tuple_type targs
388
      then
389
        try
390
          let targs = Utils.transpose_list (List.map type_list_of_type targs) in
391
          (* Types. *)type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)
392
        with 
393
          Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l')))
394
	                                
395
      else (
396
        type_dependent_call env in_main loc const f (List.combine args targs)
397
      )
398
      
399
    (* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)
400
    and type_dependent_call env in_main loc const f targs =
401
      (* Format.eprintf "Typing.type_dependent_call %s@." f; *)
402
      let tins, touts = new_var (), new_var () in
403
      (* Format.eprintf "tin=%a, tout=%a@." print_ty tins print_ty touts; *)
404
      let tfun = (* Type_predef. *)type_arrow tins touts in
405
      (* Format.eprintf "fun=%a@." print_ty tfun; *)
406
      type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
407
      (* Format.eprintf "type subtyping@."; *)
408
      let tins = type_list_of_type tins in
409
      if List.length targs <> List.length tins then
410
        raise (Error (loc, WrongArity (List.length tins, List.length targs)))
411
      else
412
        begin
413
          List.iter2 (
414
	      fun (a,t) ti ->
415
	      let t' = type_add_const env (const || (* Types. *)get_static_value ti <> None) a t in
416
	      (* Format.eprintf "uniying ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts;  *)
417
	      try_unify ~sub:true ti t' a.expr_loc;
418
	    (* Format.eprintf "unified ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts;  *)
419
	      
420
            )
421
	    targs
422
	    tins;
423
          touts
424
        end
425

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

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

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

    
562
    (* Eexpr are always in annotations. TODO: add the quantifiers variables to the env *)
563
    let type_eexpr env eexpr = 
564
      (type_expr
565
         ~is_annot:true
566
         env
567
         false (* not in main *)
568
         false (* not a const *)
569
         eexpr.eexpr_qfexpr)
570

    
571

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

    
601

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

    
623
    let rec check_type_declaration loc cty =
624
      match cty with
625
      | Tydec_clock ty
626
        | Tydec_array (_, ty) -> check_type_declaration loc ty
627
      | Tydec_const tname   ->
628
         (* Format.eprintf "TABLE: %a@." print_type_table (); *)
629
         if not (Hashtbl.mem type_table cty)
630
         then raise (Error (loc, Unbound_type tname));
631
      | _                   -> ()
632

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

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

    
657
    let type_var_decl_list vd_env env l =
658
      List.fold_left (type_var_decl vd_env) env l
659

    
660
    let type_of_vlist vars =
661
      let tyl = List.map (fun v -> Expr_type_hub.import v.var_type) vars in
662
      type_of_type_list tyl
663

    
664
    let add_vdecl vd_env vdecl =
665
      if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
666
      then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
667
      else vdecl::vd_env
668

    
669
    let check_vd_env vd_env =
670
      ignore (List.fold_left add_vdecl [] vd_env)
671

    
672
    let type_spec env spec =
673
      let vd_env = spec.consts @ spec.locals in
674
      check_vd_env vd_env;
675
      let env = type_var_decl_list ((* this argument seems useless to me, cf TODO at top of the file*) vd_env) env vd_env in
676
      (* typing stmts *)
677
      let eqs = List.map (fun s -> match s with Eq eq -> eq | _ -> assert false) spec.stmts  in
678
      let undefined_vars_init =
679
        List.fold_left
680
          (fun uvs v -> ISet.add v.var_id uvs)
681
          ISet.empty spec.locals
682
      in
683
      let _ =
684
        List.fold_left
685
          (type_eq (env, vd_env) (false (*is_main*)))
686
          undefined_vars_init
687
          eqs
688
      in
689
      (* Typing each predicate expr *)
690
      let type_pred_ee ee : unit=
691
        type_subtyping_arg (env, vd_env) (false (* not in main *)) (false (* not a const *)) ee.eexpr_qfexpr type_bool
692
      in
693
      List.iter type_pred_ee
694
        (
695
          spec.assume 
696
          @ spec.guarantees
697
          @ List.flatten (List.map (fun m -> m.ensure @ m.require) spec.modes) 
698
        );
699
      (*TODO 
700
        enrich env locally with locals and consts
701
        type each pre/post as a boolean expr
702
        I don't know if we want to update the global env with locally typed variables. 
703
        For the moment, returning the provided env           
704
       *)
705
      env
706
      
707
    (** [type_node env nd loc] types node [nd] in environment env. The
708
    location is used for error reports. *)
709
    let type_node env nd loc =
710
      let is_main = nd.node_id = !Options.main_node in
711
      let vd_env_ol = nd.node_outputs@nd.node_locals in
712
      let vd_env =  nd.node_inputs@vd_env_ol in
713
      check_vd_env vd_env;
714
      let init_env = env in
715
      let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
716
      let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
717
      let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
718
      let new_env = Env.overwrite env delta_env in
719
      let undefined_vars_init =
720
        List.fold_left
721
          (fun uvs v -> ISet.add v.var_id uvs)
722
          ISet.empty vd_env_ol in
723
      let undefined_vars =
724
        let eqs, auts = get_node_eqs nd in
725
        (* TODO XXX: il faut typer les handlers de l'automate *)
726
        List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs
727
      in
728
      (* Typing asserts *)
729
      List.iter (fun assert_ ->
730
          let assert_expr =  assert_.assert_expr in
731
          type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool
732
        )  nd.node_asserts;
733
      (* Typing spec/contracts *)
734
      (match nd.node_spec with None -> () | Some spec -> ignore (type_spec new_env spec));
735
      (* Typing annots *)
736
      List.iter (fun annot ->
737
          List.iter (fun (_, eexpr) -> ignore (type_eexpr (new_env, vd_env) eexpr)) annot.annots
738
        ) nd.node_annot;
739
      
740
      (* check that table is empty *)
741
      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
742
      let undefined_vars = ISet.diff undefined_vars local_consts in
743
      if (not (ISet.is_empty undefined_vars)) then
744
        raise (Error (loc, Undefined_var undefined_vars));
745
      let ty_ins = type_of_vlist nd.node_inputs in
746
      let ty_outs = type_of_vlist nd.node_outputs in
747
      let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
748
      generalize ty_node;
749
      (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
750
      nd.node_type <- Expr_type_hub.export ty_node;
751
      Env.add_value env nd.node_id ty_node
752

    
753
    let type_imported_node env nd loc =
754
      let vd_env = nd.nodei_inputs@nd.nodei_outputs in
755
      check_vd_env vd_env;
756
      let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in
757
      let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in
758
      let new_env = Env.overwrite env delta_env in
759
      (* Typing spec *)
760
      (match nd.nodei_spec with None -> () | Some spec -> ignore (type_spec new_env spec)); 
761
      let ty_ins = type_of_vlist nd.nodei_inputs in
762
      let ty_outs = type_of_vlist nd.nodei_outputs in
763
      let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
764
      generalize ty_node;
765
      (*
766
  if (is_polymorphic ty_node) then
767
    raise (Error (loc, Poly_imported_node nd.nodei_id));
768
       *)
769
      let new_env = Env.add_value env nd.nodei_id ty_node in
770
      nd.nodei_type <- Expr_type_hub.export ty_node;
771
      new_env
772

    
773
    let type_top_const env cdecl =
774
      let ty = type_const cdecl.const_loc cdecl.const_value in
775
      let d =
776
        if is_dimension_type ty
777
        then dimension_of_const cdecl.const_loc cdecl.const_value
778
        else Dimension.mkdim_var () in
779
      let ty = (* Type_predef. *)type_static d ty in
780
      let new_env = Env.add_value env cdecl.const_id ty in
781
      cdecl.const_type <- Expr_type_hub.export ty;
782
      new_env
783

    
784
    let type_top_consts env clist =
785
      List.fold_left type_top_const env clist
786

    
787
    let rec type_top_decl env decl =
788
      match decl.top_decl_desc with
789
      | Node nd -> (
790
        try
791
          type_node env nd decl.top_decl_loc
792
        with Error (loc, err) as exc -> (
793
          if !Options.global_inline then
794
	    Format.eprintf "Type error: failing node@.%a@.@?"
795
	      Printers.pp_node nd
796
          ;
797
            raise exc)
798
      )
799
      | ImportedNode nd ->
800
         type_imported_node env nd decl.top_decl_loc
801
      | Const c ->
802
         type_top_const env c
803
      | TypeDef _ -> List.fold_left type_top_decl env (consts_of_enum_type decl)
804
      | Include _ | Open _  -> env
805
    
806
    let get_type_of_call decl =
807
      match decl.top_decl_desc with
808
      | Node nd         ->
809
         let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.node_type) in
810
         type_list_of_type in_typ, type_list_of_type out_typ
811
      | ImportedNode nd ->
812
         let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.nodei_type) in
813
         type_list_of_type in_typ, type_list_of_type out_typ
814
      | _               -> assert false
815

    
816
    let type_prog env decls =
817
      try
818
        List.fold_left type_top_decl env decls
819
      with Failure _ as exc -> raise exc
820

    
821
    (* Once the Lustre program is fully typed, we must get back to the
822
       original description of dimensions, with constant parameters,
823
       instead of unifiable internal variables. *)
824

    
825
    (* The following functions aims at 'unevaluating' dimension
826
       expressions occuring in array types, i.e. replacing unifiable
827
       second_order variables with the original static parameters.
828
       Once restored in this formulation, dimensions may be
829
       meaningfully printed.  *)
830
    let uneval_vdecl_generics vdecl =
831
      if vdecl.var_dec_const
832
      then
833
        match get_static_value (Expr_type_hub.import vdecl.var_type) with
834
        | None   -> (Format.eprintf "internal error: %a@." (* Types. *)print_ty (Expr_type_hub.import vdecl.var_type); assert false)
835
        | Some d -> Dimension.uneval vdecl.var_id d
836

    
837
    let uneval_node_generics vdecls =
838
      List.iter uneval_vdecl_generics vdecls
839

    
840
    let uneval_spec_generics spec =
841
      List.iter uneval_vdecl_generics (spec.consts@spec.locals)
842
      
843
    let uneval_top_generics decl =
844
      match decl.top_decl_desc with
845
      | Node nd ->
846
         uneval_node_generics (nd.node_inputs @ nd.node_outputs)
847
      | ImportedNode nd ->
848
         uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
849
      | Const _ | TypeDef _ | Open _ | Include _ 
850
        -> ()
851

    
852
    let uneval_prog_generics prog =
853
      List.iter uneval_top_generics prog
854

    
855
    let rec get_imported_symbol decls id =
856
      match decls with
857
      | [] -> assert false
858
      | decl::q ->
859
         (match decl.top_decl_desc with
860
          | ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf -> decl
861
          | Const c when id = c.const_id && decl.top_decl_itf -> decl
862
          | TypeDef _ -> get_imported_symbol (consts_of_enum_type decl @ q) id
863
          | _ -> get_imported_symbol q id)
864

    
865
    let check_env_compat header declared computed = 
866
      uneval_prog_generics header;
867
      Env.iter declared (fun k decl_type_k ->
868
          let loc = (get_imported_symbol header k).top_decl_loc in 
869
          let computed_t =
870
            instantiate (ref []) (ref []) 
871
	      (try Env.lookup_value computed k
872
	       with Not_found -> raise (Error (loc, Declared_but_undefined k))) in
873
          (*Types.print_ty Format.std_formatter decl_type_k;
874
      Types.print_ty Format.std_formatter computed_t;*)
875
          try_unify ~sub:true ~semi:true decl_type_k computed_t loc
876
        )
877

    
878
    let check_typedef_top decl =
879
      (*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*)
880
      (*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*)
881
      (*Format.eprintf "%a" Corelang.print_type_table ();*)
882
      match decl.top_decl_desc with
883
      | TypeDef ty ->
884
         let owner = decl.top_decl_owner in
885
         let itf = decl.top_decl_itf in
886
         let decl' =
887
           try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id)
888
           with Not_found -> raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in
889
         let owner' = decl'.top_decl_owner in
890
         (*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*)
891
         let itf' = decl'.top_decl_itf in
892
         (match decl'.top_decl_desc with
893
          | Const _ | Node _ | ImportedNode _ -> assert false
894
          | TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') -> ()
895
          | _ -> raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id)))
896
      | _  -> ()
897

    
898
    let check_typedef_compat header =
899
      List.iter check_typedef_top header
900
  end
901

    
902
include  Make(Types.Main) (struct
903
             type type_expr  = Types.Main.type_expr
904
             let import x = x
905
             let export x = x
906
           end)
907
             (* Local Variables: *)
908
             (* compile-command:"make -C .." *)
909
(* End: *)