Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ b38ffff3

History | View | Annotate | Download (27.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 LustreSpec
26
open Corelang
27
open Types
28
open Format
29

    
30
let pp_typing_env fmt env =
31
  Env.pp_env print_ty fmt env
32

    
33
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in
34
    type [ty]. False otherwise. *)
35
let rec occurs tvar ty =
36
  let ty = repr ty in
37
  match ty.tdesc with
38
  | Tvar -> ty=tvar
39
  | Tarrow (t1, t2) ->
40
      (occurs tvar t1) || (occurs tvar t2)
41
  | Ttuple tl ->
42
     List.exists (occurs tvar) tl
43
  | Tstruct fl ->
44
     List.exists (fun (f, t) -> occurs tvar t) fl
45
  | Tarray (_, t)
46
  | Tstatic (_, t)
47
  | Tclock t
48
  | Tlink t -> occurs tvar t
49
  | Tenum _ | Tconst _ | Tunivar | Tint | Treal | Tbool | Trat -> false
50

    
51
(** Promote monomorphic type variables to polymorphic type variables. *)
52
(* Generalize by side-effects *)
53
let rec generalize ty =
54
  match ty.tdesc with
55
  | Tvar ->
56
      (* No scopes, always generalize *)
57
      ty.tdesc <- Tunivar
58
  | Tarrow (t1,t2) ->
59
      generalize t1; generalize t2
60
  | Ttuple tl ->
61
     List.iter generalize tl
62
  | Tstruct fl ->
63
     List.iter (fun (f, t) -> generalize t) fl
64
  | Tstatic (d, t)
65
  | Tarray (d, t) -> Dimension.generalize d; generalize t
66
  | Tclock t
67
  | Tlink t ->
68
      generalize t
69
  | Tenum _ | Tconst _ | Tunivar | Tint | Treal | Tbool | Trat -> ()
70

    
71
(** Downgrade polymorphic type variables to monomorphic type variables *)
72
let rec instantiate inst_vars inst_dim_vars ty =
73
  let ty = repr ty in
74
  match ty.tdesc with
75
  | Tenum _ | Tconst _ | Tvar | Tint | Treal | Tbool | Trat -> ty
76
  | Tarrow (t1,t2) ->
77
      {ty with tdesc =
78
       Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))}
79
  | Ttuple tlist ->
80
      {ty with tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist)}
81
  | Tstruct flist ->
82
      {ty with tdesc = Tstruct (List.map (fun (f, t) -> (f, instantiate inst_vars inst_dim_vars t)) flist)}
83
  | Tclock t ->
84
	{ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t)}
85
  | Tstatic (d, t) ->
86
	{ty with tdesc = Tstatic (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)}
87
  | Tarray (d, t) ->
88
	{ty with tdesc = Tarray (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)}
89
  | Tlink t ->
90
	(* should not happen *)
91
	{ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t)}
92
  | Tunivar ->
93
      try
94
        List.assoc ty.tid !inst_vars
95
      with Not_found ->
96
        let var = new_var () in
97
	inst_vars := (ty.tid, var)::!inst_vars;
98
	var
99

    
100
(* [type_coretype cty] types the type declaration [cty] *)
101
let rec type_coretype type_dim cty =
102
  match (*get_repr_type*) cty with
103
  | Tydec_any -> new_var ()
104
  | Tydec_int -> Type_predef.type_int
105
  | Tydec_real -> Type_predef.type_real
106
  | Tydec_float -> Type_predef.type_real
107
  | Tydec_bool -> Type_predef.type_bool
108
  | Tydec_clock ty -> Type_predef.type_clock (type_coretype type_dim ty)
109
  | Tydec_const c -> Type_predef.type_const c
110
  | Tydec_enum tl -> Type_predef.type_enum tl
111
  | Tydec_struct fl -> Type_predef.type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl)
112
  | Tydec_array (d, ty) ->
113
    begin
114
      type_dim d;
115
      Type_predef.type_array d (type_coretype type_dim ty)
116
    end
117

    
118
(* [coretype_type] is the reciprocal of [type_typecore] *)
119
let rec coretype_type ty =
120
 match (repr ty).tdesc with
121
 | Tvar           -> Tydec_any
122
 | Tint           -> Tydec_int
123
 | Treal          -> Tydec_real
124
 | Tbool          -> Tydec_bool
125
 | Tconst c       -> Tydec_const c
126
 | Tclock t       -> Tydec_clock (coretype_type t)
127
 | Tenum tl       -> Tydec_enum tl
128
 | Tstruct fl     -> Tydec_struct (List.map (fun (f, t) -> (f, coretype_type t)) fl)
129
 | Tarray (d, t)  -> Tydec_array (d, coretype_type t)
130
 | Tstatic (_, t) -> coretype_type t
131
 | _         -> assert false
132

    
133
let get_type_definition tname =
134
  try
135
    type_coretype (fun d -> ()) (Hashtbl.find type_table (Tydec_const tname))
136
  with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
137

    
138
(* Equality on ground types only *)
139
(* Should be used between local variables which must have a ground type *)
140
let rec eq_ground t1 t2 =
141
  match t1.tdesc, t2.tdesc with
142
  | Tint, Tint | Tbool, Tbool | Trat, Trat | Treal, Treal -> true
143
  | Tenum tl, Tenum tl' when tl == tl' -> true
144
  | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> List.for_all2 eq_ground tl tl'
145
  | 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'
146
  | (Tconst t, _) ->
147
    let def_t = get_type_definition t in
148
    eq_ground def_t t2
149
  | (_, Tconst t)  ->
150
    let def_t = get_type_definition t in
151
    eq_ground t1 def_t
152
  | Tarrow (t1,t2), Tarrow (t1',t2') -> eq_ground t1 t1' && eq_ground t2 t2'
153
  | Tclock t1', Tclock t2' -> eq_ground t1' t2'
154
  | Tstatic (e1, t1'), Tstatic (e2, t2')
155
  | Tarray (e1, t1'), Tarray (e2, t2') -> Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'
156
  | _ -> false
157

    
158
(** [unify t1 t2] unifies types [t1] and [t2]
159
    using standard destructive unification.
160
    Raises [Unify (t1,t2)] if the types are not unifiable.
161
    [t1] is a expected/formal/spec type, [t2] is a computed/real/implem type,
162
    so in case of unification error: expected type [t1], got type [t2].
163
    If [sub]-typing is allowed, [t2] may be a subtype of [t1].
164
    If [semi] unification is required,
165
    [t1] should furthermore be an instance of [t2]
166
    and constants are handled differently.*)
167
let unify ?(sub=false) ?(semi=false) t1 t2 =
168
  let rec unif t1 t2 =
169
    let t1 = repr t1 in
170
    let t2 = repr t2 in
171
    if t1==t2 then
172
      ()
173
    else
174
      match t1.tdesc,t2.tdesc with
175
      (* strictly subtyping cases first *)
176
      | _ , Tclock t2 when sub && (get_clock_base_type t1 = None) ->
177
	unif t1 t2
178
      | _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) ->
179
	unif t1 t2
180
      (* This case is not mandatory but will keep "older" types *)
181
      | Tvar, Tvar ->
182
        if t1.tid < t2.tid then
183
          t2.tdesc <- Tlink t1
184
        else
185
          t1.tdesc <- Tlink t2
186
      | Tvar, _ when (not semi) && (not (occurs t1 t2)) ->
187
        t1.tdesc <- Tlink t2
188
      | _, Tvar when (not (occurs t2 t1)) ->
189
        t2.tdesc <- Tlink t1
190
      | Tarrow (t1,t2), Tarrow (t1',t2') ->
191
	begin
192
          unif t2 t2';
193
	  unif t1' t1
194
	end
195
      | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
196
	List.iter2 unif tl tl'
197
      | Ttuple [t1]        , _                  -> unif t1 t2
198
      | _                  , Ttuple [t2]        -> unif t1 t2
199
      | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
200
	List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'
201
      | Tclock _, Tstatic _
202
      | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
203
      | Tclock t1', Tclock t2' -> unif t1' t2'
204
      | Tint, Tint | Tbool, Tbool | Trat, Trat | Treal, Treal
205
      | Tunivar, _ | _, Tunivar -> ()
206
      | (Tconst t, _) ->
207
	let def_t = get_type_definition t in
208
	unif def_t t2
209
      | (_, Tconst t)  ->
210
	let def_t = get_type_definition t in
211
	unif t1 def_t
212
      | Tenum tl, Tenum tl' when tl == tl' -> ()
213
      | Tstatic (e1, t1'), Tstatic (e2, t2')
214
      | Tarray (e1, t1'), Tarray (e2, t2') ->
215
	let eval_const =
216
	  if semi
217
	  then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c))
218
	  else (fun c -> None) in
219
	begin
220
	  unif t1' t2';
221
	  Dimension.eval Basic_library.eval_env eval_const e1;
222
	  Dimension.eval Basic_library.eval_env eval_const e2;
223
	  Dimension.unify ~semi:semi e1 e2;
224
	end
225
      | _,_ -> raise (Unify (t1, t2))
226
  in unif t1 t2
227

    
228
(* Expected type ty1, got type ty2 *)
229
let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =
230
  try
231
    unify ~sub:sub ~semi:semi ty1 ty2
232
  with
233
  | Unify _ ->
234
    raise (Error (loc, Type_clash (ty1,ty2)))
235
  | Dimension.Unify _ ->
236
    raise (Error (loc, Type_clash (ty1,ty2)))
237

    
238
let rec type_struct_const_field loc (label, c) =
239
  if Hashtbl.mem field_table label
240
  then let tydec = Hashtbl.find field_table label in
241
       let tydec_struct = get_struct_type_fields tydec in
242
       let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
243
       begin
244
	 try_unify ty_label (type_const loc c) loc;
245
	 type_coretype (fun d -> ()) tydec
246
       end
247
  else raise (Error (loc, Unbound_value ("struct field " ^ label)))
248

    
249
and type_const loc c = 
250
  match c with
251
  | Const_int _     -> Type_predef.type_int
252
  | Const_real _    -> Type_predef.type_real
253
  | Const_float _   -> Type_predef.type_real
254
  | Const_array ca  -> let d = Dimension.mkdim_int loc (List.length ca) in
255
		      let ty = new_var () in
256
		      List.iter (fun e -> try_unify ty (type_const loc e) loc) ca;
257
		      Type_predef.type_array d ty
258
  | Const_tag t     ->
259
    if Hashtbl.mem tag_table t
260
    then type_coretype (fun d -> ()) (Hashtbl.find tag_table t)
261
    else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
262
  | Const_struct fl ->
263
    let ty_struct = new_var () in
264
    begin
265
      let used =
266
	List.fold_left
267
	  (fun acc (l, c) ->
268
	    if List.mem l acc
269
	    then raise (Error (loc, Already_bound ("struct field " ^ l)))
270
	    else try_unify ty_struct (type_struct_const_field loc (l, c)) loc; l::acc)
271
	  [] fl in
272
      try
273
	let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in
274
(*	List.iter (fun l -> Format.eprintf "total: %s@." l) total;
275
	List.iter (fun l -> Format.eprintf "used: %s@." l) used; *)
276
	let undef = List.find (fun l -> not (List.mem l used)) total
277
	in raise (Error (loc, Unbound_value ("struct field " ^ undef)))
278
      with Not_found -> 
279
	ty_struct
280
    end
281
  | Const_string _ -> assert false (* string should only appear in annotations *)
282

    
283
(* The following typing functions take as parameter an environment [env]
284
   and whether the element being typed is expected to be constant [const]. 
285
   [env] is a pair composed of:
286
  - a map from ident to type, associating to each ident, i.e. 
287
    variables, constants and (imported) nodes, its type including whether
288
    it is constant or not. This latter information helps in checking constant 
289
    propagation policy in Lustre.
290
  - a vdecl list, in order to modify types of declared variables that are
291
    later discovered to be clocks during the typing process.
292
*)
293
let check_constant loc const_expected const_real =
294
  if const_expected && not const_real
295
  then raise (Error (loc, Not_a_constant))
296

    
297
let rec type_add_const env const arg targ =
298
  if const
299
  then let d =
300
	 if is_dimension_type targ
301
	 then dimension_of_expr arg
302
	 else Dimension.mkdim_var () in
303
       let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
304
       Dimension.eval Basic_library.eval_env eval_const d;
305
       let real_static_type = Type_predef.type_static d (Types.dynamic_type targ) in
306
       (match Types.get_static_value targ with
307
       | None    -> ()
308
       | Some d' -> try_unify targ real_static_type arg.expr_loc);
309
       real_static_type
310
  else targ
311

    
312
(* emulates a subtyping relation between types t and (d : t),
313
   used during node applications and assignments *)
314
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
315
  let loc = real_arg.expr_loc in
316
  let const = const || (Types.get_static_value formal_type <> None) in
317
  let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in
318
  (*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;*)
319
  try_unify ~sub:sub formal_type real_type loc
320

    
321
and type_ident env in_main loc const id =
322
  type_expr env in_main const (expr_of_ident id loc)
323

    
324
(* typing an application implies:
325
   - checking that const formal parameters match real const (maybe symbolic) arguments
326
   - checking type adequation between formal and real arguments
327
   An application may embed an homomorphic/internal function, in which case we need to split
328
   it in many calls
329
*)
330
and type_appl env in_main loc const f args =
331
  let targs = List.map (type_expr env in_main const) args in
332
  if Basic_library.is_internal_fun f && List.exists is_tuple_type targs
333
  then
334
    try
335
      let targs = Utils.transpose_list (List.map type_list_of_type targs) in
336
      Types.type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)
337
    with
338
      Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l')))
339
  else
340
    type_dependent_call env in_main loc const f (List.combine args targs)
341

    
342
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)
343
and type_dependent_call env in_main loc const f targs =
344
  let tins, touts = new_var (), new_var () in
345
  let tfun = Type_predef.type_arrow tins touts in
346
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
347
  let tins = type_list_of_type tins in
348
  if List.length targs <> List.length tins then
349
    raise (Error (loc, WrongArity (List.length tins, List.length targs)))
350
  else
351
    begin
352
      List.iter2 (fun (a,t) ti ->
353
	let t' = type_add_const env (const || Types.get_static_value ti <> None) a t
354
	in try_unify ~sub:true ti t' a.expr_loc) targs tins;
355
      touts
356
    end
357

    
358
(* type a simple call without dependent types 
359
   but possible homomorphic extension.
360
   [targs] is here a list of arguments' types. *)
361
and type_simple_call env in_main loc const f targs =
362
  let tins, touts = new_var (), new_var () in
363
  let tfun = Type_predef.type_arrow tins touts in
364
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
365
  (*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*)
366
  try_unify ~sub:true tins (type_of_type_list targs) loc;
367
  touts
368

    
369
(** [type_expr env in_main expr] types expression [expr] in environment
370
    [env], expecting it to be [const] or not. *)
371
and type_expr env in_main const expr =
372
  let resulting_ty = 
373
  match expr.expr_desc with
374
  | Expr_const c ->
375
    let ty = type_const expr.expr_loc c in
376
    let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in
377
    expr.expr_type <- ty;
378
    ty
379
  | Expr_ident v ->
380
    let tyv =
381
      try
382
        Env.lookup_value (fst env) v
383
      with Not_found ->
384
	Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr;
385
        raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))
386
    in
387
    let ty = instantiate (ref []) (ref []) tyv in
388
    let ty' =
389
      if const
390
      then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ())
391
      else new_var () in
392
    try_unify ty ty' expr.expr_loc;
393
    expr.expr_type <- ty;
394
    ty 
395
  | Expr_array elist ->
396
    let ty_elt = new_var () in
397
    List.iter (fun e -> try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist;
398
    let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
399
    let ty = Type_predef.type_array d ty_elt in
400
    expr.expr_type <- ty;
401
    ty
402
  | Expr_access (e1, d) ->
403
    type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
404
    let ty_elt = new_var () in
405
    let d = Dimension.mkdim_var () in
406
    type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt);
407
    expr.expr_type <- ty_elt;
408
    ty_elt
409
  | Expr_power (e1, d) ->
410
    let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
411
    type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
412
    Dimension.eval Basic_library.eval_env eval_const d;
413
    let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in
414
    let ty = Type_predef.type_array d ty_elt in
415
    expr.expr_type <- ty;
416
    ty
417
  | Expr_tuple elist ->
418
    let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in
419
    expr.expr_type <- ty;
420
    ty
421
  | Expr_ite (c, t, e) ->
422
    type_subtyping_arg env in_main const c Type_predef.type_bool;
423
    let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in
424
    expr.expr_type <- ty;
425
    ty
426
  | Expr_appl (id, args, r) ->
427
    (* application of non internal function is not legal in a constant
428
       expression *)
429
    (match r with
430
    | None        -> ()
431
    | Some (x, l) -> 
432
      check_constant expr.expr_loc const false;
433
      let expr_x = expr_of_ident x expr.expr_loc in	
434
      let typ_l = 
435
	Type_predef.type_clock 
436
	  (type_const expr.expr_loc (Const_tag l)) in
437
      type_subtyping_arg env in_main ~sub:false const expr_x typ_l);
438
    let touts = type_appl env in_main expr.expr_loc const id (expr_list_of_expr args) in
439
    expr.expr_type <- touts;
440
    touts
441
  | Expr_fby (e1,e2)
442
  | Expr_arrow (e1,e2) ->
443
    (* fby/arrow is not legal in a constant expression *)
444
    check_constant expr.expr_loc const false;
445
    let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in
446
    expr.expr_type <- ty;
447
    ty
448
  | Expr_pre e ->
449
    (* pre is not legal in a constant expression *)
450
    check_constant expr.expr_loc const false;
451
    let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in
452
    expr.expr_type <- ty;
453
    ty
454
  | Expr_when (e1,c,l) ->
455
    (* when is not legal in a constant expression *)
456
    check_constant expr.expr_loc const false;
457
    let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in
458
    let expr_c = expr_of_ident c expr.expr_loc in
459
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
460
    let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in
461
    expr.expr_type <- ty;
462
    ty
463
  | Expr_merge (c,hl) ->
464
    (* merge is not legal in a constant expression *)
465
    check_constant expr.expr_loc const false;
466
    let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in
467
    let expr_c = expr_of_ident c expr.expr_loc in
468
    let typ_l = Type_predef.type_clock typ_in in
469
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
470
    expr.expr_type <- typ_out;
471
    typ_out
472
  in 
473
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr Types.print_ty resulting_ty);
474
  resulting_ty
475

    
476
and type_branches env in_main loc const hl =
477
  let typ_in = new_var () in
478
  let typ_out = new_var () in
479
  try
480
    let used_labels =
481
      List.fold_left (fun accu (t, h) ->
482
	unify typ_in (type_const loc (Const_tag t));
483
	type_subtyping_arg env in_main const h typ_out;
484
	if List.mem t accu
485
	then raise (Error (loc, Already_bound t))
486
	else t :: accu) [] hl in
487
    let type_labels = get_enum_type_tags (coretype_type typ_in) in
488
    if List.sort compare used_labels <> List.sort compare type_labels
489
    then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in
490
	 raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
491
    else (typ_in, typ_out)
492
  with Unify (t1, t2) ->
493
    raise (Error (loc, Type_clash (t1,t2)))
494

    
495
(** [type_eq env eq] types equation [eq] in environment [env] *)
496
let type_eq env in_main undefined_vars eq =
497
  (* Check undefined variables, type lhs *)
498
  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
499
  let ty_lhs = type_expr env in_main false expr_lhs in
500
  (* Check multiple variable definitions *)
501
  let define_var id uvars =
502
    try
503
      ignore(IMap.find id uvars);
504
      IMap.remove id uvars
505
    with Not_found ->
506
      raise (Error (eq.eq_loc, Already_defined id))
507
  in
508
  (* check assignment of declared constant, assignment of clock *)
509
  let ty_lhs =
510
    type_of_type_list
511
      (List.map2 (fun ty id ->
512
	if get_static_value ty <> None
513
	then raise (Error (eq.eq_loc, Assigned_constant id)) else
514
	match get_clock_base_type ty with
515
	| None -> ty
516
	| Some ty -> ty)
517
	 (type_list_of_type ty_lhs) eq.eq_lhs) in
518
  let undefined_vars =
519
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
520
  (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
521
     to a (always non-constant) lhs variable *)
522
  type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
523
  undefined_vars
524

    
525

    
526
(* [type_coreclock env ck id loc] types the type clock declaration [ck]
527
   in environment [env] *)
528
let type_coreclock env ck id loc =
529
  match ck.ck_dec_desc with
530
  | Ckdec_any | Ckdec_pclock (_,_) -> ()
531
  | Ckdec_bool cl ->
532
      let dummy_id_expr = expr_of_ident id loc in
533
      let when_expr =
534
        List.fold_left
535
          (fun expr (x, l) ->
536
                {expr_tag = new_tag ();
537
                 expr_desc= Expr_when (expr,x,l);
538
                 expr_type = new_var ();
539
                 expr_clock = Clocks.new_var true;
540
                 expr_delay = Delay.new_var ();
541
                 expr_loc=loc;
542
		 expr_annot = None})
543
          dummy_id_expr cl
544
      in
545
      ignore (type_expr env false false when_expr)
546

    
547
let rec check_type_declaration loc cty =
548
 match cty with
549
 | Tydec_clock ty
550
 | Tydec_array (_, ty) -> check_type_declaration loc ty
551
 | Tydec_const tname   ->
552
   if not (Hashtbl.mem type_table cty)
553
   then raise (Error (loc, Unbound_type tname));
554
 | _                   -> ()
555

    
556
let type_var_decl vd_env env vdecl =
557
  check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
558
  let eval_const id = Types.get_static_value (Env.lookup_value env id) in
559
  let type_dim d =
560
    begin
561
      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;
562
      Dimension.eval Basic_library.eval_env eval_const d;
563
    end in
564
  let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
565
  let ty_status =
566
    if vdecl.var_dec_const
567
    then Type_predef.type_static (Dimension.mkdim_var ()) ty
568
    else ty in
569
  let new_env = Env.add_value env vdecl.var_id ty_status in
570
  type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
571
  vdecl.var_type <- ty_status;
572
  new_env
573

    
574
let type_var_decl_list vd_env env l =
575
  List.fold_left (type_var_decl vd_env) env l
576

    
577
let type_of_vlist vars =
578
  let tyl = List.map (fun v -> v.var_type) vars in
579
  type_of_type_list tyl
580

    
581
let add_vdecl vd_env vdecl =
582
 if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
583
 then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
584
 else vdecl::vd_env
585

    
586
let check_vd_env vd_env =
587
  ignore (List.fold_left add_vdecl [] vd_env)
588

    
589
(** [type_node env nd loc] types node [nd] in environment env. The
590
    location is used for error reports. *)
591
let type_node env nd loc =
592
  let is_main = nd.node_id = !Options.main_node in
593
  let vd_env_ol = nd.node_outputs@nd.node_locals in
594
  let vd_env =  nd.node_inputs@vd_env_ol in
595
  check_vd_env vd_env;
596
  let init_env = env in
597
  let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
598
  let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
599
  let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
600
  let new_env = Env.overwrite env delta_env in
601
  let undefined_vars_init =
602
    List.fold_left
603
      (fun uvs v -> IMap.add v.var_id () uvs)
604
      IMap.empty vd_env_ol in
605
  let undefined_vars =
606
    List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs
607
  in
608
  (* Typing asserts *)
609
  List.iter (fun assert_ ->
610
    let assert_expr =  assert_.assert_expr in
611
    type_subtyping_arg (new_env, vd_env) is_main false assert_expr Type_predef.type_bool
612
  )  nd.node_asserts;
613
  
614
  (* check that table is empty *)
615
  if (not (IMap.is_empty undefined_vars)) then
616
    raise (Error (loc, Undefined_var undefined_vars));
617
  let ty_ins = type_of_vlist nd.node_inputs in
618
  let ty_outs = type_of_vlist nd.node_outputs in
619
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
620
  generalize ty_node;
621
  (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
622
  nd.node_type <- ty_node;
623
  Env.add_value env nd.node_id ty_node
624

    
625
let type_imported_node env nd loc =
626
  let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
627
  let vd_env = nd.nodei_inputs@nd.nodei_outputs in
628
  check_vd_env vd_env;
629
  ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
630
  let ty_ins = type_of_vlist nd.nodei_inputs in
631
  let ty_outs = type_of_vlist nd.nodei_outputs in
632
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
633
  generalize ty_node;
634
(*
635
  if (is_polymorphic ty_node) then
636
    raise (Error (loc, Poly_imported_node nd.nodei_id));
637
*)
638
  let new_env = Env.add_value env nd.nodei_id ty_node in
639
  nd.nodei_type <- ty_node;
640
  new_env
641

    
642
let type_top_consts env clist =
643
  List.fold_left (fun env cdecl ->
644
    let ty = type_const cdecl.const_loc cdecl.const_value in
645
    let d =
646
      if is_dimension_type ty
647
      then dimension_of_const cdecl.const_loc cdecl.const_value
648
      else Dimension.mkdim_var () in
649
    let ty = Type_predef.type_static d ty in
650
    let new_env = Env.add_value env cdecl.const_id ty in
651
    cdecl.const_type <- ty;
652
    new_env) env clist
653

    
654
let type_top_decl env decl =
655
  match decl.top_decl_desc with
656
  | Node nd -> (
657
      try
658
	type_node env nd decl.top_decl_loc
659
      with Error (loc, err) as exc -> (
660
	if !Options.global_inline then
661
	  Format.eprintf "Type error: failing node@.%a@.@?"
662
	    Printers.pp_node nd
663
	;
664
	raise exc)
665
  )
666
  | ImportedNode nd ->
667
      type_imported_node env nd decl.top_decl_loc
668
  | Consts clist ->
669
      type_top_consts env clist
670
  | Open _  -> env
671

    
672
let type_prog env decls =
673
try
674
  List.fold_left type_top_decl env decls
675
with Failure _ as exc -> raise exc
676

    
677
(* Once the Lustre program is fully typed,
678
   we must get back to the original description of dimensions,
679
   with constant parameters, instead of unifiable internal variables. *)
680

    
681
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types,
682
   i.e. replacing unifiable second_order variables with the original static parameters.
683
   Once restored in this formulation, dimensions may be meaningfully printed.
684
*)
685
let uneval_vdecl_generics vdecl =
686
 if vdecl.var_dec_const
687
 then
688
   match get_static_value vdecl.var_type with
689
   | None   -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)
690
   | Some d -> Dimension.uneval vdecl.var_id d
691

    
692
let uneval_node_generics vdecls =
693
  List.iter uneval_vdecl_generics vdecls
694

    
695
let uneval_top_generics decl =
696
  match decl.top_decl_desc with
697
  | Node nd ->
698
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
699
  | ImportedNode nd ->
700
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
701
  | Consts clist -> ()
702
  | Open _  -> ()
703

    
704
let uneval_prog_generics prog =
705
 List.iter uneval_top_generics prog
706

    
707
let rec get_imported_node decls id =
708
  match decls with
709
  | [] -> assert false
710
  | decl::q ->
711
     (match decl.top_decl_desc with
712
      | ImportedNode nd when id = nd.nodei_id -> decl
713
      | _ -> get_imported_node q id)
714

    
715
let check_env_compat header declared computed = 
716
  uneval_prog_generics header;
717
  Env.iter declared (fun k decl_type_k -> 
718
    let computed_t = instantiate (ref []) (ref []) 
719
				 (try Env.lookup_value computed k
720
				  with Not_found ->
721
				    let loc = (get_imported_node header k).top_decl_loc in 
722
				    raise (Error (loc, Declared_but_undefined k))) in
723
    (*Types.print_ty Format.std_formatter decl_type_k;
724
    Types.print_ty Format.std_formatter computed_t;*)
725
    try_unify ~sub:true ~semi:true decl_type_k computed_t Location.dummy_loc
726
		    )
727

    
728
(* Local Variables: *)
729
(* compile-command:"make -C .." *)
730
(* End: *)