Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ 6560bb94

History | View | Annotate | Download (25.8 KB)

1
(* ----------------------------------------------------------------------------
2
 * SchedMCore - A MultiCore Scheduling Framework
3
 * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
4
 *
5
 * This file is part of Prelude
6
 *
7
 * Prelude is free software; you can redistribute it and/or
8
 * modify it under the terms of the GNU Lesser General Public License
9
 * as published by the Free Software Foundation ; either version 2 of
10
 * the License, or (at your option) any later version.
11
 *
12
 * Prelude is distributed in the hope that it will be useful, but
13
 * WITHOUT ANY WARRANTY ; without even the implied warranty of
14
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15
 * Lesser General Public License for more details.
16
 *
17
 * You should have received a copy of the GNU Lesser General Public
18
 * License along with this program ; if not, write to the Free Software
19
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
20
 * USA
21
 *---------------------------------------------------------------------------- *)
22

    
23
(** Main typing module. Classic inference algorithm with destructive
24
    unification. *)
25

    
26
let debug fmt args = () (* Format.eprintf "%a"  *)
27
(* Though it shares similarities with the clock calculus module, no code
28
    is shared.  Simple environments, very limited identifier scoping, no
29
    identifier redefinition allowed. *)
30

    
31
open Utils
32
(* Yes, opening both modules is dirty as some type names will be
33
   overwritten, yet this makes notations far lighter.*)
34
open LustreSpec
35
open Corelang
36
open Types
37
open Format
38

    
39
let pp_typing_env fmt env =
40
  Env.pp_env print_ty fmt env
41

    
42
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in
43
    type [ty]. False otherwise. *)
44
let rec occurs tvar ty =
45
  let ty = repr ty in
46
  match ty.tdesc with
47
  | Tvar -> ty=tvar
48
  | Tarrow (t1, t2) ->
49
      (occurs tvar t1) || (occurs tvar t2)
50
  | Ttuple tl ->
51
      List.exists (occurs tvar) tl
52
  | Tarray (_, t)
53
  | Tstatic (_, t)
54
  | Tclock t
55
  | Tlink t -> occurs tvar t
56
  | Tenum _ | Tconst _ | Tunivar | Tint | Treal | Tbool | Trat -> false
57

    
58
(** Promote monomorphic type variables to polymorphic type variables. *)
59
(* Generalize by side-effects *)
60
let rec generalize ty =
61
  match ty.tdesc with
62
  | Tvar ->
63
      (* No scopes, always generalize *)
64
      ty.tdesc <- Tunivar
65
  | Tarrow (t1,t2) ->
66
      generalize t1; generalize t2
67
  | Ttuple tlist ->
68
      List.iter generalize tlist
69
  | Tstatic (d, t)
70
  | Tarray (d, t) -> Dimension.generalize d; generalize t
71
  | Tclock t
72
  | Tlink t ->
73
      generalize t
74
  | Tenum _ | Tconst _ | Tunivar | Tint | Treal | Tbool | Trat -> ()
75

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

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

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

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

    
140
(** [unify t1 t2] unifies types [t1] and [t2]. Raises [Unify
141
    (t1,t2)] if the types are not unifiable.*)
142
(* Standard destructive unification *)
143
let rec unify t1 t2 =
144
  let t1 = repr t1 in
145
  let t2 = repr t2 in
146
  if t1=t2 then
147
    ()
148
  else
149
    (* No type abbreviations resolution for now *)
150
    match t1.tdesc,t2.tdesc with
151
      (* This case is not mandory but will keep "older" types *)
152
    | Tvar, Tvar ->
153
        if t1.tid < t2.tid then
154
          t2.tdesc <- Tlink t1
155
        else
156
          t1.tdesc <- Tlink t2
157
    | (Tvar, _) when (not (occurs t1 t2)) ->
158
        t1.tdesc <- Tlink t2
159
    | (_,Tvar) when (not (occurs t2 t1)) ->
160
        t2.tdesc <- Tlink t1
161
    | Tarrow (t1,t2), Tarrow (t1',t2') ->
162
      begin
163
        unify t1 t1';
164
	unify t2 t2'
165
      end
166
    | Ttuple tlist1, Ttuple tlist2 ->
167
        if (List.length tlist1) <> (List.length tlist2) then
168
	  raise (Unify (t1, t2))
169
	else
170
          List.iter2 unify tlist1 tlist2
171
    | Tclock _, Tstatic _
172
    | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
173
    | Tclock t1', _ -> unify t1' t2
174
    | _, Tclock t2' -> unify t1 t2'
175
    | Tint, Tint | Tbool, Tbool | Trat, Trat
176
    | Tunivar, _ | _, Tunivar -> ()
177
    | (Tconst t, _) ->
178
      let def_t = get_type_definition t in
179
      unify def_t t2
180
    | (_, Tconst t)  ->
181
      let def_t = get_type_definition t in
182
      unify t1 def_t
183
    | Tenum tl, Tenum tl' when tl == tl' -> ()
184
    | Tstatic (e1, t1'), Tstatic (e2, t2')
185
    | Tarray (e1, t1'), Tarray (e2, t2') ->
186
      begin
187
	unify t1' t2';
188
	Dimension.eval Basic_library.eval_env (fun c -> None) e1;
189
	Dimension.eval Basic_library.eval_env (fun c -> None) e2;
190
	Dimension.unify e1 e2;
191
      end
192
    | _,_ -> raise (Unify (t1, t2))
193

    
194
(** [semi_unify t1 t2] checks whether type [t1] is an instance of type [t2]. Raises [Unify
195
    (t1,t2)] if the types are not semi-unifiable.*)
196
(* Standard destructive semi-unification *)
197
let rec semi_unify t1 t2 =
198
  let t1 = repr t1 in
199
  let t2 = repr t2 in
200
  if t1=t2 then
201
    ()
202
  else
203
    (* No type abbreviations resolution for now *)
204
    match t1.tdesc,t2.tdesc with
205
      (* This case is not mandory but will keep "older" types *)
206
    | Tvar, Tvar ->
207
        if t1.tid < t2.tid then
208
          t2.tdesc <- Tlink t1
209
        else
210
          t1.tdesc <- Tlink t2
211
    | (Tvar, _) -> raise (Unify (t1, t2))
212
    | (_,Tvar) when (not (occurs t2 t1)) ->
213
        t2.tdesc <- Tlink t1
214
    | Tarrow (t1,t2), Tarrow (t1',t2') ->
215
      begin
216
        semi_unify t1 t1';
217
	semi_unify t2 t2'
218
      end
219
    | Ttuple tlist1, Ttuple tlist2 ->
220
        if (List.length tlist1) <> (List.length tlist2) then
221
	  raise (Unify (t1, t2))
222
	else
223
          List.iter2 semi_unify tlist1 tlist2
224
    | Tclock _, Tstatic _
225
    | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
226
    | Tclock t1', _ -> semi_unify t1' t2
227
    | _, Tclock t2' -> semi_unify t1 t2'
228
    | Tint, Tint | Tbool, Tbool | Trat, Trat
229
    | Tunivar, _ | _, Tunivar -> ()
230
    | (Tconst t, _) ->
231
      let def_t = get_type_definition t in
232
      semi_unify def_t t2
233
    | (_, Tconst t)  ->
234
      let def_t = get_type_definition t in
235
      semi_unify t1 def_t
236
    | Tenum tl, Tenum tl' when tl == tl' -> ()
237
    | Tstatic (e1, t1'), Tstatic (e2, t2')
238
    | Tarray (e1, t1'), Tarray (e2, t2') ->
239
      begin
240
	semi_unify t1' t2';
241
	Dimension.eval Basic_library.eval_env (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c)) e1;
242
	Dimension.eval Basic_library.eval_env (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c)) e2;
243
	Dimension.semi_unify e1 e2;
244
      end
245
    | _,_ -> raise (Unify (t1, t2))
246

    
247
let try_unify ty1 ty2 loc =
248
  try
249
    unify ty1 ty2
250
  with
251
  | Unify _ ->
252
    raise (Error (loc, Type_clash (ty1,ty2)))
253
  | Dimension.Unify _ ->
254
    raise (Error (loc, Type_clash (ty1,ty2)))
255

    
256
let try_semi_unify ty1 ty2 loc =
257
  try
258
    semi_unify ty1 ty2
259
  with
260
  | Unify _ ->
261
    raise (Error (loc, Type_clash (ty1,ty2)))
262
  | Dimension.Unify _ ->
263
    raise (Error (loc, Type_clash (ty1,ty2)))
264

    
265
let rec type_const loc c = 
266
  match c with
267
  | Const_int _ -> Type_predef.type_int
268
  | Const_real _ -> Type_predef.type_real
269
  | Const_float _ -> Type_predef.type_real
270
  | Const_array ca -> let d = Dimension.mkdim_int loc (List.length ca) in
271
		      let ty = new_var () in
272
		      List.iter (fun e -> try_unify (type_const loc e) ty loc) ca;
273
		      Type_predef.type_array d ty
274
  | Const_tag t  ->
275
    if Hashtbl.mem tag_table t
276
    then type_coretype (fun d -> ()) (Hashtbl.find tag_table t)
277
    else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
278

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

    
293
let rec type_standard_args env in_main const expr_list =
294
  let ty_list = List.map (fun e -> dynamic_type (type_expr env in_main const e)) expr_list in
295
  let ty_res = new_var () in
296
  List.iter2 (fun e ty -> try_unify ty_res ty e.expr_loc) expr_list ty_list;
297
  ty_res
298

    
299
(* emulates a subtyping relation between types t and (d : t),
300
   used during node applications and assignments *)
301
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
302
  let loc = real_arg.expr_loc in
303
  let const = const || (Types.get_static_value formal_type <> None) in
304
  let real_type = type_expr env in_main const real_arg in
305
  let real_type =
306
    if const
307
    then let d =
308
	   if is_dimension_type real_type
309
	   then dimension_of_expr real_arg
310
	   else Dimension.mkdim_var () in
311
	 let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
312
	 Dimension.eval Basic_library.eval_env eval_const d;
313
	 let real_static_type = Type_predef.type_static d (Types.dynamic_type real_type) in
314
	 (match Types.get_static_value real_type with
315
	 | None    -> ()
316
	 | Some d' -> try_unify real_type real_static_type loc);
317
	 real_static_type
318
    else real_type in
319
(*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;*)
320
  let real_types   = type_list_of_type real_type in
321
  let formal_types = type_list_of_type formal_type in
322
  if (List.length real_types) <> (List.length formal_types)
323
  then raise (Unify (real_type, formal_type))
324
  else List.iter2 (type_subtyping loc sub) real_types formal_types
325

    
326
and type_subtyping loc sub real_type formal_type =
327
  match (repr real_type).tdesc, (repr formal_type).tdesc with
328
  | Tstatic _          , Tstatic _ when sub -> try_unify formal_type real_type loc
329
  | Tstatic (r_d, r_ty), _         when sub -> try_unify formal_type r_ty loc
330
  | _                                       -> try_unify formal_type real_type loc
331

    
332
and type_ident env in_main loc const id =
333
  type_expr env in_main const (expr_of_ident id loc)
334

    
335
(* typing an application implies:
336
   - checking that const formal parameters match real const (maybe symbolic) arguments
337
   - checking type adequation between formal and real arguments
338
*)
339
and type_appl env in_main loc const f args =
340
  let tfun = type_ident env in_main loc const f in
341
  let tins, touts = split_arrow tfun in
342
  let tins = type_list_of_type tins in
343
  let args = expr_list_of_expr args in
344
  List.iter2 (type_subtyping_arg env in_main const) args tins;
345
  touts
346

    
347
(** [type_expr env in_main expr] types expression [expr] in environment
348
    [env], expecting it to be [const] or not. *)
349
and type_expr env in_main const expr =
350
  let res = 
351
  match expr.expr_desc with
352
  | Expr_const c ->
353
    let ty = type_const expr.expr_loc c in
354
    let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in
355
    expr.expr_type <- ty;
356
    ty
357
  | Expr_ident v ->
358
    let tyv =
359
      try
360
        Env.lookup_value (fst env) v
361
      with Not_found ->
362
	Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr;
363
        raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))
364
    in
365
    let ty = instantiate (ref []) (ref []) tyv in
366
    let ty' =
367
      if const
368
      then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ())
369
      else new_var () in
370
    try_unify ty ty' expr.expr_loc;
371
    expr.expr_type <- ty;
372
    ty 
373
  | Expr_array elist ->
374
    let ty_elt = type_standard_args env in_main const elist in
375
    let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
376
    let ty = Type_predef.type_array d ty_elt in
377
    expr.expr_type <- ty;
378
    ty
379
  | Expr_access (e1, d) ->
380
    type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
381
    let ty_elt = new_var () in
382
    let d = Dimension.mkdim_var () in
383
    type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt);
384
    expr.expr_type <- ty_elt;
385
    ty_elt
386
  | Expr_power (e1, d) ->
387
    let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
388
    type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
389
    Dimension.eval Basic_library.eval_env eval_const d;
390
    let ty_elt = type_standard_args env in_main const [e1] in
391
    let ty = Type_predef.type_array d ty_elt in
392
    expr.expr_type <- ty;
393
    ty
394
  | Expr_tuple elist ->
395
    let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in
396
    expr.expr_type <- ty;
397
    ty
398
  | Expr_ite (c, t, e) ->
399
    type_subtyping_arg env in_main const c Type_predef.type_bool;
400
    let ty = type_standard_args env in_main const [t; e] in
401
    expr.expr_type <- ty;
402
    ty
403
  | Expr_appl (id, args, r) ->
404
    (* application of non internal function is not legal in a constant
405
       expression *)
406
    (match r with
407
    | None        -> ()
408
    | Some (x, l) -> 
409
      check_constant expr.expr_loc const false;
410
      let expr_x = expr_of_ident x expr.expr_loc in	
411
      let typ_l = 
412
	Type_predef.type_clock 
413
	  (type_const expr.expr_loc (Const_tag l)) in
414
      type_subtyping_arg env in_main ~sub:false const expr_x typ_l);
415
    let touts = type_appl env in_main expr.expr_loc const id args in
416
    expr.expr_type <- touts;
417
    touts
418
  | Expr_fby (e1,e2)
419
  | Expr_arrow (e1,e2) ->
420
    (* fby/arrow is not legal in a constant expression *)
421
    check_constant expr.expr_loc const false;
422
    let ty = type_standard_args env in_main const [e1; e2] in
423
    expr.expr_type <- ty;
424
    ty
425
  | Expr_pre e ->
426
    (* pre is not legal in a constant expression *)
427
    check_constant expr.expr_loc const false;
428
    let ty = type_standard_args env in_main const [e] in
429
    expr.expr_type <- ty;
430
    ty
431
  | Expr_when (e1,c,l) ->
432
    (* when is not legal in a constant expression *)
433
    check_constant expr.expr_loc const false;
434
    let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in
435
    let expr_c = expr_of_ident c expr.expr_loc in
436
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
437
    update_clock env in_main c expr.expr_loc typ_l;
438
    let ty = type_standard_args env in_main const [e1] in
439
    expr.expr_type <- ty;
440
    ty
441
  | Expr_merge (c,hl) ->
442
    (* merge is not legal in a constant expression *)
443
    check_constant expr.expr_loc const false;
444
    let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in
445
    let expr_c = expr_of_ident c expr.expr_loc in
446
    let typ_l = Type_predef.type_clock typ_in in
447
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
448
    update_clock env in_main c expr.expr_loc typ_l;
449
    expr.expr_type <- typ_out;
450
    typ_out
451
  | Expr_uclock (e,k) | Expr_dclock (e,k) ->
452
      let ty = type_expr env in_main const e in
453
      expr.expr_type <- ty;
454
      ty
455
  | Expr_phclock (e,q) ->
456
      let ty = type_expr env in_main const e in
457
      expr.expr_type <- ty;
458
      ty
459
  in (*Format.eprintf "typing %B %a at %a = %a@." const Printers.pp_expr expr Location.pp_loc expr.expr_loc Types.print_ty res;*) res
460

    
461
and type_branches env in_main loc const hl =
462
  let typ_in = new_var () in
463
  let typ_out = new_var () in
464
  try
465
    let used_labels =
466
      List.fold_left (fun accu (t, h) ->
467
	unify typ_in (type_const loc (Const_tag t));
468
	type_subtyping_arg env in_main const h typ_out;
469
	if List.mem t accu
470
	then raise (Error (loc, Already_bound t))
471
	else t :: accu) [] hl in
472
    let type_labels = get_enum_type_tags (coretype_type typ_in) in
473
    if List.sort compare used_labels <> List.sort compare type_labels
474
    then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in
475
	 raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
476
    else (typ_in, typ_out)
477
  with Unify (t1, t2) ->
478
    raise (Error (loc, Type_clash (t1,t2)))
479

    
480
and update_clock env in_main id loc typ =
481
 (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*)
482
 try
483
   let vdecl = List.find (fun v -> v.var_id = id) (snd env)
484
   in vdecl.var_type <- typ
485
 with
486
   Not_found ->
487
   raise (Error (loc, Unbound_value ("clock " ^ id)))
488

    
489
(** [type_eq env eq] types equation [eq] in environment [env] *)
490
let type_eq env in_main undefined_vars eq =
491
  (* Check undefined variables, type lhs *)
492
  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
493
  let ty_lhs = type_expr env in_main false expr_lhs in
494
  (* Check multiple variable definitions *)
495
  let define_var id uvars =
496
    try
497
      ignore(IMap.find id uvars);
498
      IMap.remove id uvars
499
    with Not_found ->
500
      raise (Error (eq.eq_loc, Already_defined id))
501
  in
502
  let undefined_vars =
503
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
504
  (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
505
     to a (always non-constant) lhs variable *)
506
  type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
507
  undefined_vars
508

    
509

    
510
(* [type_coreclock env ck id loc] types the type clock declaration [ck]
511
   in environment [env] *)
512
let type_coreclock env ck id loc =
513
  match ck.ck_dec_desc with
514
  | Ckdec_any | Ckdec_pclock (_,_) -> ()
515
  | Ckdec_bool cl ->
516
      let dummy_id_expr = expr_of_ident id loc in
517
      let when_expr =
518
        List.fold_left
519
          (fun expr (x, l) ->
520
                {expr_tag = new_tag ();
521
                 expr_desc= Expr_when (expr,x,l);
522
                 expr_type = new_var ();
523
                 expr_clock = Clocks.new_var true;
524
                 expr_delay = Delay.new_var ();
525
                 expr_loc=loc;
526
		 expr_annot = None})
527
          dummy_id_expr cl
528
      in
529
      ignore (type_expr env false false when_expr)
530

    
531
let rec check_type_declaration loc cty =
532
 match cty with
533
 | Tydec_clock ty
534
 | Tydec_array (_, ty) -> check_type_declaration loc ty
535
 | Tydec_const tname   ->
536
   if not (Hashtbl.mem type_table cty)
537
   then raise (Error (loc, Unbound_type tname));
538
 | _                   -> ()
539

    
540
let type_var_decl vd_env env vdecl =
541
  check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
542
  let eval_const id = Types.get_static_value (Env.lookup_value env id) in
543
  let type_dim d =
544
    begin
545
      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;
546
      Dimension.eval Basic_library.eval_env eval_const d;
547
    end in
548
  let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
549
  let ty_status =
550
    if vdecl.var_dec_const
551
    then Type_predef.type_static (Dimension.mkdim_var ()) ty
552
    else ty in
553
  let new_env = Env.add_value env vdecl.var_id ty_status in
554
  type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
555
  vdecl.var_type <- ty_status;
556
  new_env
557

    
558
let type_var_decl_list vd_env env l =
559
  List.fold_left (type_var_decl vd_env) env l
560

    
561
let type_of_vlist vars =
562
  let tyl = List.map (fun v -> v.var_type) vars in
563
  type_of_type_list tyl
564

    
565
let add_vdecl vd_env vdecl =
566
 if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
567
 then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
568
 else vdecl::vd_env
569

    
570
let check_vd_env vd_env =
571
  ignore (List.fold_left add_vdecl [] vd_env)
572

    
573
(** [type_node env nd loc] types node [nd] in environment env. The
574
    location is used for error reports. *)
575
let type_node env nd loc =
576
  let is_main = nd.node_id = !Options.main_node in
577
  let vd_env_ol = nd.node_outputs@nd.node_locals in
578
  let vd_env =  nd.node_inputs@vd_env_ol in
579
  check_vd_env vd_env;
580
  let init_env = env in
581
  let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
582
  let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
583
  let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
584
  let new_env = Env.overwrite env delta_env in
585
  let undefined_vars_init =
586
    List.fold_left
587
      (fun uvs v -> IMap.add v.var_id () uvs)
588
      IMap.empty vd_env_ol in
589
  let undefined_vars =
590
    List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs
591
  in
592
  (* check that table is empty *)
593
  if (not (IMap.is_empty undefined_vars)) then
594
    raise (Error (loc, Undefined_var undefined_vars));
595
  let ty_ins = type_of_vlist nd.node_inputs in
596
  let ty_outs = type_of_vlist nd.node_outputs in
597
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
598
  generalize ty_node;
599
  (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
600
  nd.node_type <- ty_node;
601
  Env.add_value env nd.node_id ty_node
602

    
603
let type_imported_node env nd loc =
604
  let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
605
  let vd_env = nd.nodei_inputs@nd.nodei_outputs in
606
  check_vd_env vd_env;
607
  ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
608
  let ty_ins = type_of_vlist nd.nodei_inputs in
609
  let ty_outs = type_of_vlist nd.nodei_outputs in
610
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
611
  generalize ty_node;
612
(*
613
  if (is_polymorphic ty_node) then
614
    raise (Error (loc, Poly_imported_node nd.nodei_id));
615
*)
616
  let new_env = Env.add_value env nd.nodei_id ty_node in
617
  nd.nodei_type <- ty_node;
618
  new_env
619

    
620
let type_imported_fun env nd loc =
621
  let new_env = type_var_decl_list nd.fun_inputs env nd.fun_inputs in
622
  let vd_env =  nd.fun_inputs@nd.fun_outputs in
623
  check_vd_env vd_env;
624
  ignore(type_var_decl_list vd_env new_env nd.fun_outputs);
625
  let ty_ins = type_of_vlist nd.fun_inputs in
626
  let ty_outs = type_of_vlist nd.fun_outputs in
627
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
628
  generalize ty_node;
629
(*
630
  if (is_polymorphic ty_node) then
631
    raise (Error (loc, Poly_imported_node nd.fun_id));
632
*)
633
  let new_env = Env.add_value env nd.fun_id ty_node in
634
  nd.fun_type <- ty_node;
635
  new_env
636

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

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

    
669
let type_prog env decls =
670
try
671
  List.fold_left type_top_decl env decls
672
with Failure _ as exc -> raise exc
673

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

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

    
689
let uneval_node_generics vdecls =
690
  List.iter uneval_vdecl_generics vdecls
691

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

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

    
706
let check_env_compat header declared computed = 
707
  uneval_prog_generics header;
708
  Env.iter declared (fun k decl_type_k -> 
709
    let computed_t = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
710
    (*Types.print_ty Format.std_formatter decl_type_k;
711
    Types.print_ty Format.std_formatter computed_t;*)
712
    try_semi_unify decl_type_k computed_t Location.dummy_loc
713
  ) 
714

    
715
(* Local Variables: *)
716
(* compile-command:"make -C .." *)
717
(* End: *)