Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ b3381ae8

History | View | Annotate | Download (23.7 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_array (d, ty) ->
115
    begin
116
      type_dim d;
117
      Type_predef.type_array d (type_coretype type_dim ty)
118
    end
119

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

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

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

    
193
let try_unify ty1 ty2 loc =
194
  try
195
    unify ty1 ty2
196
  with
197
  | Unify _ ->
198
    raise (Error (loc, Type_clash (ty1,ty2)))
199
  | Dimension.Unify _ ->
200
    raise (Error (loc, Type_clash (ty1,ty2)))
201

    
202
let rec type_const loc c = 
203
  match c with
204
  | Const_int _ -> Type_predef.type_int
205
  | Const_real _ -> Type_predef.type_real
206
  | Const_float _ -> Type_predef.type_real
207
  | Const_array ca -> let d = Dimension.mkdim_int loc (List.length ca) in
208
		      let ty = new_var () in
209
		      List.iter (fun e -> try_unify (type_const loc e) ty loc) ca;
210
		      Type_predef.type_array d ty
211
  | Const_tag t  ->
212
    if Hashtbl.mem tag_table t
213
    then type_coretype (fun d -> ()) (Hashtbl.find tag_table t)
214
    else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
215

    
216
(* The following typing functions take as parameter an environment [env]
217
   and whether the element being typed is expected to be constant [const]. 
218
   [env] is a pair composed of:
219
  - a map from ident to type, associating to each ident, i.e. 
220
    variables, constants and (imported) nodes, its type including whether
221
    it is constant or not. This latter information helps in checking constant 
222
    propagation policy in Lustre.
223
  - a vdecl list, in order to modify types of declared variables that are
224
    later discovered to be clocks during the typing process.
225
*)
226
let check_constant loc const_expected const_real =
227
  if const_expected && not const_real
228
  then raise (Error (loc, Not_a_constant))
229

    
230
let rec type_standard_args env in_main const expr_list =
231
  let ty_list = List.map (fun e -> dynamic_type (type_expr env in_main const e)) expr_list in
232
  let ty_res = new_var () in
233
  List.iter2 (fun e ty -> try_unify ty_res ty e.expr_loc) expr_list ty_list;
234
  ty_res
235

    
236
(* emulates a subtyping relation between types t and (d : t),
237
   used during node application only *)
238
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
239
  let loc = real_arg.expr_loc in
240
  let const = const || (Types.get_static_value formal_type <> None) in
241
  let real_type = type_expr env in_main const real_arg in
242
  let real_type =
243
    if const
244
    then let d =
245
	   if is_dimension_type real_type
246
	   then dimension_of_expr real_arg
247
	   else Dimension.mkdim_var () in
248
	 let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
249
	 Dimension.eval Basic_library.eval_env eval_const d;
250
	 let real_static_type = Type_predef.type_static d (Types.dynamic_type real_type) in
251
	 (match Types.get_static_value real_type with
252
	 | None    -> ()
253
	 | Some d' -> try_unify real_type real_static_type loc);
254
	 real_static_type
255
    else real_type in
256
(*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;*)
257
  match (repr real_type).tdesc, (repr formal_type).tdesc with
258
  | Tstatic _          , Tstatic _ when sub -> try_unify formal_type real_type loc
259
  | Tstatic (r_d, r_ty), _         when sub -> try_unify formal_type r_ty loc
260
  | _                                       -> try_unify formal_type real_type loc
261

    
262
and type_ident env in_main loc const id =
263
  type_expr env in_main const (expr_of_ident id loc)
264

    
265
(* typing an application implies:
266
   - checking that const formal parameters match real const (maybe symbolic) arguments
267
   - checking type adequation between formal and real arguments
268
*)
269
and type_appl env in_main loc const f args =
270
  let tfun = type_ident env in_main loc const f in
271
  let tins, touts = split_arrow tfun in
272
  let tins = type_list_of_type tins in
273
  let args = expr_list_of_expr args in
274
  List.iter2 (type_subtyping_arg env in_main const) args tins;
275
  touts
276

    
277
(** [type_expr env in_main expr] types expression [expr] in environment
278
    [env], expecting it to be [const] or not. *)
279
and type_expr env in_main const expr =
280
  let res = 
281
  match expr.expr_desc with
282
  | Expr_const c ->
283
    let ty = type_const expr.expr_loc c in
284
    let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in
285
    expr.expr_type <- ty;
286
    ty
287
  | Expr_ident v ->
288
    let tyv =
289
      try
290
        Env.lookup_value (fst env) v
291
      with Not_found ->
292
	Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr;
293
        raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))
294
    in
295
    let ty = instantiate (ref []) (ref []) tyv in
296
    let ty' =
297
      if const
298
      then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ())
299
      else new_var () in
300
    try_unify ty ty' expr.expr_loc;
301
    expr.expr_type <- ty;
302
    ty 
303
  | Expr_array elist ->
304
    let ty_elt = type_standard_args env in_main const elist in
305
    let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
306
    let ty = Type_predef.type_array d ty_elt in
307
    expr.expr_type <- ty;
308
    ty
309
  | Expr_access (e1, d) ->
310
    type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
311
    let ty_elt = new_var () in
312
    let d = Dimension.mkdim_var () in
313
    type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt);
314
    expr.expr_type <- ty_elt;
315
    ty_elt
316
  | Expr_power (e1, d) ->
317
    let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
318
    type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
319
    Dimension.eval Basic_library.eval_env eval_const d;
320
    let ty_elt = type_standard_args env in_main const [e1] in
321
    let ty = Type_predef.type_array d ty_elt in
322
    expr.expr_type <- ty;
323
    ty
324
  | Expr_tuple elist ->
325
    let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in
326
    expr.expr_type <- ty;
327
    ty
328
  | Expr_ite (c, t, e) ->
329
    type_subtyping_arg env in_main const c Type_predef.type_bool;
330
    let ty = type_standard_args env in_main const [t; e] in
331
    expr.expr_type <- ty;
332
    ty
333
  | Expr_appl (id, args, r) ->
334
    (* application of non internal function is not legal in a constant
335
       expression *)
336
    (match r with
337
    | None        -> ()
338
    | Some (x, l) -> 
339
      check_constant expr.expr_loc const false;
340
      let expr_x = expr_of_ident x expr.expr_loc in	
341
      let typ_l = 
342
	Type_predef.type_clock 
343
	  (type_const expr.expr_loc (Const_tag l)) in
344
      type_subtyping_arg env in_main ~sub:false const expr_x typ_l);
345
    let touts = type_appl env in_main expr.expr_loc const id args in
346
    expr.expr_type <- touts;
347
    touts
348
  | Expr_fby (e1,e2)
349
  | Expr_arrow (e1,e2) ->
350
    (* fby/arrow is not legal in a constant expression *)
351
    check_constant expr.expr_loc const false;
352
    let ty = type_standard_args env in_main const [e1; e2] in
353
    expr.expr_type <- ty;
354
    ty
355
  | Expr_pre e ->
356
    (* pre is not legal in a constant expression *)
357
    check_constant expr.expr_loc const false;
358
    let ty = type_standard_args env in_main const [e] in
359
    expr.expr_type <- ty;
360
    ty
361
  | Expr_when (e1,c,l) ->
362
    (* when is not legal in a constant expression *)
363
    check_constant expr.expr_loc const false;
364
    let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in
365
    let expr_c = expr_of_ident c expr.expr_loc in
366
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
367
    update_clock env in_main c expr.expr_loc typ_l;
368
    let ty = type_standard_args env in_main const [e1] in
369
    expr.expr_type <- ty;
370
    ty
371
  | Expr_merge (c,hl) ->
372
    (* merge is not legal in a constant expression *)
373
    check_constant expr.expr_loc const false;
374
    let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in
375
    let expr_c = expr_of_ident c expr.expr_loc in
376
    let typ_l = Type_predef.type_clock typ_in in
377
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
378
    update_clock env in_main c expr.expr_loc typ_l;
379
    expr.expr_type <- typ_out;
380
    typ_out
381
  | Expr_uclock (e,k) | Expr_dclock (e,k) ->
382
      let ty = type_expr env in_main const e in
383
      expr.expr_type <- ty;
384
      ty
385
  | Expr_phclock (e,q) ->
386
      let ty = type_expr env in_main const e in
387
      expr.expr_type <- ty;
388
      ty
389
  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
390

    
391
and type_branches env in_main loc const hl =
392
  let typ_in = new_var () in
393
  let typ_out = new_var () in
394
  try
395
    let used_labels =
396
      List.fold_left (fun accu (t, h) ->
397
	unify typ_in (type_const loc (Const_tag t));
398
	type_subtyping_arg env in_main const h typ_out;
399
	if List.mem t accu
400
	then raise (Error (loc, Already_bound t))
401
	else t :: accu) [] hl in
402
    let type_labels = get_enum_type_tags (coretype_type typ_in) in
403
    if List.sort compare used_labels <> List.sort compare type_labels
404
    then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in
405
	 raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
406
    else (typ_in, typ_out)
407
  with Unify (t1, t2) ->
408
    raise (Error (loc, Type_clash (t1,t2)))
409

    
410
and update_clock env in_main id loc typ =
411
 (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*)
412
 try
413
   let vdecl = List.find (fun v -> v.var_id = id) (snd env)
414
   in vdecl.var_type <- typ
415
 with
416
   Not_found ->
417
   raise (Error (loc, Unbound_value ("clock " ^ id)))
418

    
419
(** [type_eq env eq] types equation [eq] in environment [env] *)
420
let type_eq env in_main undefined_vars eq =
421
  (* Check undefined variables, type lhs *)
422
  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
423
  let ty_lhs = type_expr env in_main false expr_lhs in
424
  (* Check multiple variable definitions *)
425
  let define_var id uvars =
426
    try
427
      ignore(IMap.find id uvars);
428
      IMap.remove id uvars
429
    with Not_found ->
430
      raise (Error (eq.eq_loc, Already_defined id))
431
  in
432
  let undefined_vars =
433
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
434
  (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
435
     to a (always non-constant) lhs variable *)
436
  type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
437
  undefined_vars
438

    
439

    
440
(* [type_coreclock env ck id loc] types the type clock declaration [ck]
441
   in environment [env] *)
442
let type_coreclock env ck id loc =
443
  match ck.ck_dec_desc with
444
  | Ckdec_any | Ckdec_pclock (_,_) -> ()
445
  | Ckdec_bool cl ->
446
      let dummy_id_expr = expr_of_ident id loc in
447
      let when_expr =
448
        List.fold_left
449
          (fun expr (x, l) ->
450
                {expr_tag = new_tag ();
451
                 expr_desc= Expr_when (expr,x,l);
452
                 expr_type = new_var ();
453
                 expr_clock = Clocks.new_var true;
454
                 expr_delay = Delay.new_var ();
455
                 expr_loc=loc;
456
		 expr_annot = None})
457
          dummy_id_expr cl
458
      in
459
Format.eprintf "yiihii@.";
460
      ignore (type_expr env false false when_expr)
461

    
462
let rec check_type_declaration loc cty =
463
 match cty with
464
 | Tydec_clock ty
465
 | Tydec_array (_, ty) -> check_type_declaration loc ty
466
 | Tydec_const tname   ->
467
   if not (Hashtbl.mem type_table cty)
468
   then raise (Error (loc, Unbound_type tname));
469
 | _                   -> ()
470

    
471
let type_var_decl vd_env env vdecl =
472
  check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
473
  let eval_const id = Types.get_static_value (Env.lookup_value env id) in
474
  let type_dim d =
475
    begin
476
      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;
477
      Dimension.eval Basic_library.eval_env eval_const d;
478
    end in
479
  let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
480
  let ty_status =
481
    if vdecl.var_dec_const
482
    then Type_predef.type_static (Dimension.mkdim_var ()) ty
483
    else ty in
484
  let new_env = Env.add_value env vdecl.var_id ty_status in
485
  type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
486
  vdecl.var_type <- ty_status;
487
  new_env
488

    
489
let type_var_decl_list vd_env env l =
490
  List.fold_left (type_var_decl vd_env) env l
491

    
492
let type_of_vlist vars =
493
  let tyl = List.map (fun v -> v.var_type) vars in
494
  type_of_type_list tyl
495

    
496
let add_vdecl vd_env vdecl =
497
 if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
498
 then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
499
 else vdecl::vd_env
500

    
501
let check_vd_env vd_env =
502
  ignore (List.fold_left add_vdecl [] vd_env)
503

    
504
(** [type_node env nd loc] types node [nd] in environment env. The
505
    location is used for error reports. *)
506
let type_node env nd loc =
507
  let is_main = nd.node_id = !Options.main_node in
508
  let vd_env_ol = nd.node_outputs@nd.node_locals in
509
  let vd_env =  nd.node_inputs@vd_env_ol in
510
  check_vd_env vd_env;
511
  let init_env = env in
512
  let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
513
  let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
514
  let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
515
  let new_env = Env.overwrite env delta_env in
516
  let undefined_vars_init =
517
    List.fold_left
518
      (fun uvs v -> IMap.add v.var_id () uvs)
519
      IMap.empty vd_env_ol in
520
  let undefined_vars =
521
    List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs
522
  in
523
  (* check that table is empty *)
524
  if (not (IMap.is_empty undefined_vars)) then
525
    raise (Error (loc, Undefined_var undefined_vars));
526
  let ty_ins = type_of_vlist nd.node_inputs in
527
  let ty_outs = type_of_vlist nd.node_outputs in
528
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
529
  generalize ty_node;
530
  (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
531
  nd.node_type <- ty_node;
532
  Env.add_value env nd.node_id ty_node
533

    
534
let type_imported_node env nd loc =
535
  let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
536
  let vd_env = nd.nodei_inputs@nd.nodei_outputs in
537
  check_vd_env vd_env;
538
  ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
539
  let ty_ins = type_of_vlist nd.nodei_inputs in
540
  let ty_outs = type_of_vlist nd.nodei_outputs in
541
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
542
  generalize ty_node;
543
(*
544
  if (is_polymorphic ty_node) then
545
    raise (Error (loc, Poly_imported_node nd.nodei_id));
546
*)
547
  let new_env = Env.add_value env nd.nodei_id ty_node in
548
  nd.nodei_type <- ty_node;
549
  new_env
550

    
551
let type_imported_fun env nd loc =
552
  let new_env = type_var_decl_list nd.fun_inputs env nd.fun_inputs in
553
  let vd_env =  nd.fun_inputs@nd.fun_outputs in
554
  check_vd_env vd_env;
555
  ignore(type_var_decl_list vd_env new_env nd.fun_outputs);
556
  let ty_ins = type_of_vlist nd.fun_inputs in
557
  let ty_outs = type_of_vlist nd.fun_outputs in
558
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
559
  generalize ty_node;
560
(*
561
  if (is_polymorphic ty_node) then
562
    raise (Error (loc, Poly_imported_node nd.fun_id));
563
*)
564
  let new_env = Env.add_value env nd.fun_id ty_node in
565
  nd.fun_type <- ty_node;
566
  new_env
567

    
568
let type_top_consts env clist =
569
  List.fold_left (fun env cdecl ->
570
    let ty = type_const cdecl.const_loc cdecl.const_value in
571
    let d =
572
      if is_dimension_type ty
573
      then dimension_of_const cdecl.const_loc cdecl.const_value
574
      else Dimension.mkdim_var () in
575
    let ty = Type_predef.type_static d ty in
576
    let new_env = Env.add_value env cdecl.const_id ty in
577
    cdecl.const_type <- ty;
578
    new_env) env clist
579

    
580
let type_top_decl env decl =
581
  match decl.top_decl_desc with
582
  | Node nd ->
583
      type_node env nd decl.top_decl_loc
584
  | ImportedNode nd ->
585
      type_imported_node env nd decl.top_decl_loc
586
  | ImportedFun nd ->
587
      type_imported_fun env nd decl.top_decl_loc
588
  | Consts clist ->
589
      type_top_consts env clist
590
  | Open _  -> env
591

    
592
let type_prog env decls =
593
try
594
  List.fold_left type_top_decl env decls
595
with Failure _ as exc -> raise exc
596

    
597
(* Once the Lustre program is fully typed,
598
   we must get back to the original description of dimensions,
599
   with constant parameters, instead of unifiable internal variables. *)
600

    
601
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types,
602
   i.e. replacing unifiable second_order variables with the original static parameters.
603
   Once restored in this formulation, dimensions may be meaningfully printed.
604
*)
605
(*
606
let uneval_vdecl_generics vdecl ty =
607
 if vdecl.var_dec_const
608
 then
609
   match get_static_value ty with
610
   | None   -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)
611
   | Some d -> Dimension.unify d (Dimension.mkdim_ident vdecl.var_loc vdecl.var_id)
612

    
613
let uneval_node_generics vdecls =
614
  let inst_typ_vars = ref [] in
615
  let inst_dim_vars = ref [] in
616
  let inst_ty_list = List.map (fun v -> instantiate inst_typ_vars inst_dim_vars v.var_type) vdecls in
617
  List.iter2 (fun v ty -> uneval_vdecl_generics v ty) vdecls inst_ty_list;
618
  List.iter2 (fun v ty -> generalize ty; v.var_type <- ty) vdecls inst_ty_list
619
*)
620
let uneval_vdecl_generics vdecl =
621
 if vdecl.var_dec_const
622
 then
623
   match get_static_value vdecl.var_type with
624
   | None   -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)
625
   | Some d -> Dimension.uneval vdecl.var_id d
626

    
627
let uneval_node_generics vdecls =
628
  List.iter uneval_vdecl_generics vdecls
629

    
630
let uneval_top_generics decl =
631
  match decl.top_decl_desc with
632
  | Node nd ->
633
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
634
  | ImportedNode nd ->
635
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
636
  | ImportedFun nd ->
637
      ()
638
  | Consts clist -> ()
639
  | Open _  -> ()
640

    
641
let uneval_prog_generics prog =
642
 List.iter uneval_top_generics prog
643

    
644
let check_env_compat declared computed =
645
  Env.iter declared (fun k decl_type_k -> 
646
    let computed_t = Env.lookup_value computed k in
647
    try_unify decl_type_k computed_t Location.dummy_loc
648
  ) 
649

    
650
(* Local Variables: *)
651
(* compile-command:"make -C .." *)
652
(* End: *)