Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ 8b3afe43

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
508

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
689
let uneval_node_generics vdecls =
690
  let inst_typ_vars = ref [] in
691
  let inst_dim_vars = ref [] in
692
  let inst_ty_list = List.map (fun v -> instantiate inst_typ_vars inst_dim_vars v.var_type) vdecls in
693
  List.iter2 (fun v ty -> uneval_vdecl_generics v ty) vdecls inst_ty_list;
694
  List.iter2 (fun v ty -> generalize ty; v.var_type <- ty) vdecls inst_ty_list
695
*)
696
let uneval_vdecl_generics vdecl =
697
 if vdecl.var_dec_const
698
 then
699
   match get_static_value vdecl.var_type with
700
   | None   -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)
701
   | Some d -> Dimension.uneval vdecl.var_id d
702

    
703
let uneval_node_generics vdecls =
704
  List.iter uneval_vdecl_generics vdecls
705

    
706
let uneval_top_generics decl =
707
  match decl.top_decl_desc with
708
  | Node nd ->
709
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
710
  | ImportedNode nd ->
711
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
712
  | ImportedFun nd ->
713
      ()
714
  | Consts clist -> ()
715
  | Open _  -> ()
716

    
717
let uneval_prog_generics prog =
718
 List.iter uneval_top_generics prog
719

    
720
let check_env_compat header declared computed =
721
  (try 
722
     uneval_prog_generics header
723
   with e -> raise e);
724
  Env.iter declared (fun k decl_type_k -> 
725
    let computed_t = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
726
    (*Types.print_ty Format.std_formatter decl_type_k;
727
    Types.print_ty Format.std_formatter computed_t;*)
728
    try_semi_unify decl_type_k computed_t Location.dummy_loc
729
  ) 
730

    
731
(* Local Variables: *)
732
(* compile-command:"make -C .." *)
733
(* End: *)