Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ 12af4908

History | View | Annotate | Download (28.3 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
  | Tstruct fl ->
53
     List.exists (fun (f, t) -> occurs tvar t) fl
54
  | Tarray (_, t)
55
  | Tstatic (_, t)
56
  | Tclock t
57
  | Tlink t -> occurs tvar t
58
  | Tenum _ | Tconst _ | Tunivar | Tint | Treal | Tbool | Trat -> false
59

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

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

    
109
(* [type_coretype cty] types the type declaration [cty] *)
110
let rec type_coretype type_dim cty =
111
  match (*get_repr_type*) cty with
112
  | Tydec_any -> new_var ()
113
  | Tydec_int -> Type_predef.type_int
114
  | Tydec_real -> Type_predef.type_real
115
  | Tydec_float -> Type_predef.type_real
116
  | Tydec_bool -> Type_predef.type_bool
117
  | Tydec_clock ty -> Type_predef.type_clock (type_coretype type_dim ty)
118
  | Tydec_const c -> Type_predef.type_const c
119
  | Tydec_enum tl -> Type_predef.type_enum tl
120
  | Tydec_struct fl -> Type_predef.type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl)
121
  | Tydec_array (d, ty) ->
122
    begin
123
      type_dim d;
124
      Type_predef.type_array d (type_coretype type_dim ty)
125
    end
126

    
127
(* [coretype_type is the reciprocal of [type_typecore] *)
128
let rec coretype_type ty =
129
 match (repr ty).tdesc with
130
 | Tvar           -> Tydec_any
131
 | Tint           -> Tydec_int
132
 | Treal          -> Tydec_real
133
 | Tbool          -> Tydec_bool
134
 | Tconst c       -> Tydec_const c
135
 | Tclock t       -> Tydec_clock (coretype_type t)
136
 | Tenum tl       -> Tydec_enum tl
137
 | Tstruct fl     -> Tydec_struct (List.map (fun (f, t) -> (f, coretype_type t)) fl)
138
 | Tarray (d, t)  -> Tydec_array (d, coretype_type t)
139
 | Tstatic (_, t) -> coretype_type t
140
 | _         -> assert false
141

    
142
let get_type_definition tname =
143
  try
144
    type_coretype (fun d -> ()) (Hashtbl.find type_table (Tydec_const tname))
145
  with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
146

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

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

    
243
    | Tstatic (e1, t1'), Tstatic (e2, t2')
244
    | Tarray (e1, t1'), Tarray (e2, t2') ->
245
      begin
246
	semi_unify t1' t2';
247
	Dimension.eval Basic_library.eval_env (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c)) e1;
248
	Dimension.eval Basic_library.eval_env (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c)) e2;
249
	Dimension.semi_unify e1 e2;
250
      end
251
    | _,_ -> raise (Unify (t1, t2))
252

    
253
(* Expected type ty1, got type ty2 *)
254
let try_unify ty1 ty2 loc =
255
  try
256
    unify ty1 ty2
257
  with
258
  | Unify _ ->
259
    raise (Error (loc, Type_clash (ty1,ty2)))
260
  | Dimension.Unify _ ->
261
    raise (Error (loc, Type_clash (ty1,ty2)))
262

    
263
let try_semi_unify ty1 ty2 loc =
264
  try
265
    semi_unify ty1 ty2
266
  with
267
  | Unify _ ->
268
    raise (Error (loc, Type_clash (ty1,ty2)))
269
  | Dimension.Unify _ ->
270
    raise (Error (loc, Type_clash (ty1,ty2)))
271

    
272
(* ty1 is a subtype of ty2 *)
273
let rec sub_unify sub ty1 ty2 =
274
  match (repr ty1).tdesc, (repr ty2).tdesc with
275
  | Ttuple [t1]        , Ttuple [t2]        -> sub_unify sub t1 t2
276
  | Ttuple tl1         , Ttuple tl2         ->
277
    if List.length tl1 <> List.length tl2
278
    then raise (Unify (ty1, ty2))
279
    else List.iter2 (sub_unify sub) tl1 tl2
280
  | Ttuple [t1]        , _                  -> sub_unify sub t1 ty2
281
  | _                  , Ttuple [t2]        -> sub_unify sub ty1 t2
282
  | Tstruct tl1        , Tstruct tl2        ->
283
    if List.map fst tl1 <> List.map fst tl2
284
    then raise (Unify (ty1, ty2))
285
    else List.iter2 (fun (_, t1) (_, t2) -> sub_unify sub t1 t2) tl1 tl2
286
  | Tstatic (d1, t1)   , Tstatic (d2, t2)   ->
287
    begin
288
      sub_unify sub t1 t2;
289
      Dimension.eval Basic_library.eval_env (fun c -> None) d1;
290
      Dimension.eval Basic_library.eval_env (fun c -> None) d2;
291
      Dimension.unify d1 d2
292
    end
293
  | Tstatic (r_d, t1)  , _         when sub -> sub_unify sub ty2 t1
294
  | _                                       -> unify ty2 ty1
295

    
296
let try_sub_unify sub ty1 ty2 loc =
297
  try
298
    sub_unify sub ty1 ty2
299
  with
300
  | Unify _ ->
301
    raise (Error (loc, Type_clash (ty1,ty2)))
302
  | Dimension.Unify _ ->
303
    raise (Error (loc, Type_clash (ty1,ty2)))
304

    
305
let type_struct_field loc ftyp (label, f) =
306
  if Hashtbl.mem field_table label
307
  then let tydec = Hashtbl.find field_table label in
308
       let tydec_struct = get_struct_type_fields tydec in
309
       let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
310
       begin
311
	 try_unify ty_label (ftyp loc f) loc;
312
	 type_coretype (fun d -> ()) tydec
313
       end
314
  else raise (Error (loc, Unbound_value ("struct field " ^ label)))
315

    
316
let rec type_const loc c = 
317
  match c with
318
  | Const_int _     -> Type_predef.type_int
319
  | Const_real _    -> Type_predef.type_real
320
  | Const_float _   -> Type_predef.type_real
321
  | Const_array ca  -> let d = Dimension.mkdim_int loc (List.length ca) in
322
		      let ty = new_var () in
323
		      List.iter (fun e -> try_unify ty (type_const loc e) loc) ca;
324
		      Type_predef.type_array d ty
325
  | Const_tag t     ->
326
    if Hashtbl.mem tag_table t
327
    then type_coretype (fun d -> ()) (Hashtbl.find tag_table t)
328
    else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
329
  | Const_struct fl ->
330
    let ty_struct = new_var () in
331
    begin
332
      List.iter (fun f -> try_unify ty_struct (type_struct_field loc type_const f) loc) fl;
333
      ty_struct
334
    end
335

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

    
350
let rec type_standard_args env in_main const expr_list =
351
  let ty_list = List.map (fun e -> dynamic_type (type_expr env in_main const e)) expr_list in
352
  let ty_res = new_var () in
353
  List.iter2 (fun e ty -> try_unify ty_res ty e.expr_loc) expr_list ty_list;
354
  ty_res
355

    
356
(* emulates a subtyping relation between types t and (d : t),
357
   used during node applications and assignments *)
358
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
359
  let loc = real_arg.expr_loc in
360
  let const = const || (Types.get_static_value formal_type <> None) in
361
  let real_type = type_expr env in_main const real_arg in
362
  let real_type =
363
    if const
364
    then let d =
365
	   if is_dimension_type real_type
366
	   then dimension_of_expr real_arg
367
	   else Dimension.mkdim_var () in
368
	 let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
369
	 Dimension.eval Basic_library.eval_env eval_const d;
370
	 let real_static_type = Type_predef.type_static d (Types.dynamic_type real_type) in
371
	 (match Types.get_static_value real_type with
372
	 | None    -> ()
373
	 | Some d' -> try_unify real_type real_static_type loc);
374
	 real_static_type
375
    else real_type in
376
(*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*)
377
  try_sub_unify sub real_type formal_type loc
378
(*
379
and type_subtyping_tuple loc real_type formal_type =
380
  let real_types   = type_list_of_type real_type in
381
  let formal_types = type_list_of_type formal_type in
382
  if (List.length real_types) <> (List.length formal_types)
383
  then raise (Unify (real_type, formal_type))
384
  else List.iter2 (type_subtyping loc sub) real_types formal_types
385

    
386
and type_subtyping loc sub real_type formal_type =
387
  match (repr real_type).tdesc, (repr formal_type).tdesc with
388
  | Tstatic _          , Tstatic _ when sub -> try_unify formal_type real_type loc
389
  | Tstatic (r_d, r_ty), _         when sub -> try_unify formal_type r_ty loc
390
  | _                                       -> try_unify formal_type real_type loc
391
*)
392
and type_ident env in_main loc const id =
393
  type_expr env in_main const (expr_of_ident id loc)
394

    
395
(* typing an application implies:
396
   - checking that const formal parameters match real const (maybe symbolic) arguments
397
   - checking type adequation between formal and real arguments
398
*)
399
and type_appl env in_main loc const f args =
400
  let tfun = type_ident env in_main loc const f in
401
  let tins, touts = split_arrow tfun in
402
  let tins = type_list_of_type tins in
403
  let args = expr_list_of_expr args in
404
  List.iter2 (type_subtyping_arg env in_main const) args tins;
405
  touts
406

    
407
(** [type_expr env in_main expr] types expression [expr] in environment
408
    [env], expecting it to be [const] or not. *)
409
and type_expr env in_main const expr =
410
  let res = 
411
  match expr.expr_desc with
412
  | Expr_const c ->
413
    let ty = type_const expr.expr_loc c in
414
    let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in
415
    expr.expr_type <- ty;
416
    ty
417
  | Expr_ident v ->
418
    let tyv =
419
      try
420
        Env.lookup_value (fst env) v
421
      with Not_found ->
422
	Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr;
423
        raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))
424
    in
425
    let ty = instantiate (ref []) (ref []) tyv in
426
    let ty' =
427
      if const
428
      then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ())
429
      else new_var () in
430
    try_unify ty ty' expr.expr_loc;
431
    expr.expr_type <- ty;
432
    ty 
433
  | Expr_array elist ->
434
    let ty_elt = type_standard_args env in_main const elist in
435
    let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
436
    let ty = Type_predef.type_array d ty_elt in
437
    expr.expr_type <- ty;
438
    ty
439
  | Expr_access (e1, d) ->
440
    type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
441
    let ty_elt = new_var () in
442
    let d = Dimension.mkdim_var () in
443
    type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt);
444
    expr.expr_type <- ty_elt;
445
    ty_elt
446
  | Expr_power (e1, d) ->
447
    let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
448
    type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
449
    Dimension.eval Basic_library.eval_env eval_const d;
450
    let ty_elt = type_standard_args env in_main const [e1] in
451
    let ty = Type_predef.type_array d ty_elt in
452
    expr.expr_type <- ty;
453
    ty
454
  | Expr_tuple elist ->
455
    let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in
456
    expr.expr_type <- ty;
457
    ty
458
  | Expr_ite (c, t, e) ->
459
    type_subtyping_arg env in_main const c Type_predef.type_bool;
460
    let ty = type_standard_args env in_main const [t; e] in
461
    expr.expr_type <- ty;
462
    ty
463
  | Expr_appl (id, args, r) ->
464
    (* application of non internal function is not legal in a constant
465
       expression *)
466
    (match r with
467
    | None        -> ()
468
    | Some (x, l) -> 
469
      check_constant expr.expr_loc const false;
470
      let expr_x = expr_of_ident x expr.expr_loc in	
471
      let typ_l = 
472
	Type_predef.type_clock 
473
	  (type_const expr.expr_loc (Const_tag l)) in
474
      type_subtyping_arg env in_main ~sub:false const expr_x typ_l);
475
    let touts = type_appl env in_main expr.expr_loc const id args in
476
    expr.expr_type <- touts;
477
    touts
478
  | Expr_fby (e1,e2)
479
  | Expr_arrow (e1,e2) ->
480
    (* fby/arrow is not legal in a constant expression *)
481
    check_constant expr.expr_loc const false;
482
    let ty = type_standard_args env in_main const [e1; e2] in
483
    expr.expr_type <- ty;
484
    ty
485
  | Expr_pre e ->
486
    (* pre is not legal in a constant expression *)
487
    check_constant expr.expr_loc const false;
488
    let ty = type_standard_args env in_main const [e] in
489
    expr.expr_type <- ty;
490
    ty
491
  | Expr_when (e1,c,l) ->
492
    (* when is not legal in a constant expression *)
493
    check_constant expr.expr_loc const false;
494
    let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in
495
    let expr_c = expr_of_ident c expr.expr_loc in
496
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
497
    update_clock env in_main c expr.expr_loc typ_l;
498
    let ty = type_standard_args env in_main const [e1] in
499
    expr.expr_type <- ty;
500
    ty
501
  | Expr_merge (c,hl) ->
502
    (* merge is not legal in a constant expression *)
503
    check_constant expr.expr_loc const false;
504
    let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in
505
    let expr_c = expr_of_ident c expr.expr_loc in
506
    let typ_l = Type_predef.type_clock typ_in in
507
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
508
    update_clock env in_main c expr.expr_loc typ_l;
509
    expr.expr_type <- typ_out;
510
    typ_out
511
  | Expr_uclock (e,k) | Expr_dclock (e,k) ->
512
      let ty = type_expr env in_main const e in
513
      expr.expr_type <- ty;
514
      ty
515
  | Expr_phclock (e,q) ->
516
      let ty = type_expr env in_main const e in
517
      expr.expr_type <- ty;
518
      ty
519
  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
520

    
521
and type_branches env in_main loc const hl =
522
  let typ_in = new_var () in
523
  let typ_out = new_var () in
524
  try
525
    let used_labels =
526
      List.fold_left (fun accu (t, h) ->
527
	unify typ_in (type_const loc (Const_tag t));
528
	type_subtyping_arg env in_main const h typ_out;
529
	if List.mem t accu
530
	then raise (Error (loc, Already_bound t))
531
	else t :: accu) [] hl in
532
    let type_labels = get_enum_type_tags (coretype_type typ_in) in
533
    if List.sort compare used_labels <> List.sort compare type_labels
534
    then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in
535
	 raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
536
    else (typ_in, typ_out)
537
  with Unify (t1, t2) ->
538
    raise (Error (loc, Type_clash (t1,t2)))
539

    
540
and update_clock env in_main id loc typ =
541
 (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*)
542
 try
543
   let vdecl = List.find (fun v -> v.var_id = id) (snd env)
544
   in vdecl.var_type <- typ
545
 with
546
   Not_found ->
547
   raise (Error (loc, Unbound_value ("clock " ^ id)))
548

    
549
(** [type_eq env eq] types equation [eq] in environment [env] *)
550
let type_eq env in_main undefined_vars eq =
551
  (* Check undefined variables, type lhs *)
552
  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
553
  let ty_lhs = type_expr env in_main false expr_lhs in
554
  (* Check multiple variable definitions *)
555
  let define_var id uvars =
556
    try
557
      ignore(IMap.find id uvars);
558
      IMap.remove id uvars
559
    with Not_found ->
560
      raise (Error (eq.eq_loc, Already_defined id))
561
  in
562
  let undefined_vars =
563
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
564
  (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
565
     to a (always non-constant) lhs variable *)
566
  type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
567
  undefined_vars
568

    
569

    
570
(* [type_coreclock env ck id loc] types the type clock declaration [ck]
571
   in environment [env] *)
572
let type_coreclock env ck id loc =
573
  match ck.ck_dec_desc with
574
  | Ckdec_any | Ckdec_pclock (_,_) -> ()
575
  | Ckdec_bool cl ->
576
      let dummy_id_expr = expr_of_ident id loc in
577
      let when_expr =
578
        List.fold_left
579
          (fun expr (x, l) ->
580
                {expr_tag = new_tag ();
581
                 expr_desc= Expr_when (expr,x,l);
582
                 expr_type = new_var ();
583
                 expr_clock = Clocks.new_var true;
584
                 expr_delay = Delay.new_var ();
585
                 expr_loc=loc;
586
		 expr_annot = None})
587
          dummy_id_expr cl
588
      in
589
      ignore (type_expr env false false when_expr)
590

    
591
let rec check_type_declaration loc cty =
592
 match cty with
593
 | Tydec_clock ty
594
 | Tydec_array (_, ty) -> check_type_declaration loc ty
595
 | Tydec_const tname   ->
596
   if not (Hashtbl.mem type_table cty)
597
   then raise (Error (loc, Unbound_type tname));
598
 | _                   -> ()
599

    
600
let type_var_decl vd_env env vdecl =
601
  check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
602
  let eval_const id = Types.get_static_value (Env.lookup_value env id) in
603
  let type_dim d =
604
    begin
605
      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;
606
      Dimension.eval Basic_library.eval_env eval_const d;
607
    end in
608
  let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
609
  let ty_status =
610
    if vdecl.var_dec_const
611
    then Type_predef.type_static (Dimension.mkdim_var ()) ty
612
    else ty in
613
  let new_env = Env.add_value env vdecl.var_id ty_status in
614
  type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
615
  vdecl.var_type <- ty_status;
616
  new_env
617

    
618
let type_var_decl_list vd_env env l =
619
  List.fold_left (type_var_decl vd_env) env l
620

    
621
let type_of_vlist vars =
622
  let tyl = List.map (fun v -> v.var_type) vars in
623
  type_of_type_list tyl
624

    
625
let add_vdecl vd_env vdecl =
626
 if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
627
 then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
628
 else vdecl::vd_env
629

    
630
let check_vd_env vd_env =
631
  ignore (List.fold_left add_vdecl [] vd_env)
632

    
633
(** [type_node env nd loc] types node [nd] in environment env. The
634
    location is used for error reports. *)
635
let type_node env nd loc =
636
  let is_main = nd.node_id = !Options.main_node in
637
  let vd_env_ol = nd.node_outputs@nd.node_locals in
638
  let vd_env =  nd.node_inputs@vd_env_ol in
639
  check_vd_env vd_env;
640
  let init_env = env in
641
  let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
642
  let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
643
  let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
644
  let new_env = Env.overwrite env delta_env in
645
  let undefined_vars_init =
646
    List.fold_left
647
      (fun uvs v -> IMap.add v.var_id () uvs)
648
      IMap.empty vd_env_ol in
649
  let undefined_vars =
650
    List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs
651
  in
652
  (* check that table is empty *)
653
  if (not (IMap.is_empty undefined_vars)) then
654
    raise (Error (loc, Undefined_var undefined_vars));
655
  let ty_ins = type_of_vlist nd.node_inputs in
656
  let ty_outs = type_of_vlist nd.node_outputs in
657
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
658
  generalize ty_node;
659
  (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
660
  nd.node_type <- ty_node;
661
  Env.add_value env nd.node_id ty_node
662

    
663
let type_imported_node env nd loc =
664
  let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
665
  let vd_env = nd.nodei_inputs@nd.nodei_outputs in
666
  check_vd_env vd_env;
667
  ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
668
  let ty_ins = type_of_vlist nd.nodei_inputs in
669
  let ty_outs = type_of_vlist nd.nodei_outputs in
670
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
671
  generalize ty_node;
672
(*
673
  if (is_polymorphic ty_node) then
674
    raise (Error (loc, Poly_imported_node nd.nodei_id));
675
*)
676
  let new_env = Env.add_value env nd.nodei_id ty_node in
677
  nd.nodei_type <- ty_node;
678
  new_env
679

    
680
let type_imported_fun env nd loc =
681
  let new_env = type_var_decl_list nd.fun_inputs env nd.fun_inputs in
682
  let vd_env =  nd.fun_inputs@nd.fun_outputs in
683
  check_vd_env vd_env;
684
  ignore(type_var_decl_list vd_env new_env nd.fun_outputs);
685
  let ty_ins = type_of_vlist nd.fun_inputs in
686
  let ty_outs = type_of_vlist nd.fun_outputs in
687
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
688
  generalize ty_node;
689
(*
690
  if (is_polymorphic ty_node) then
691
    raise (Error (loc, Poly_imported_node nd.fun_id));
692
*)
693
  let new_env = Env.add_value env nd.fun_id ty_node in
694
  nd.fun_type <- ty_node;
695
  new_env
696

    
697
let type_top_consts env clist =
698
  List.fold_left (fun env cdecl ->
699
    let ty = type_const cdecl.const_loc cdecl.const_value in
700
    let d =
701
      if is_dimension_type ty
702
      then dimension_of_const cdecl.const_loc cdecl.const_value
703
      else Dimension.mkdim_var () in
704
    let ty = Type_predef.type_static d ty in
705
    let new_env = Env.add_value env cdecl.const_id ty in
706
    cdecl.const_type <- ty;
707
    new_env) env clist
708

    
709
let type_top_decl env decl =
710
  match decl.top_decl_desc with
711
  | Node nd -> (
712
      try
713
	type_node env nd decl.top_decl_loc
714
      with Error (loc, err) as exc -> (
715
	if !Options.global_inline then
716
	  Format.eprintf "Type error: failing node@.%a@.@?"
717
	    Printers.pp_node nd
718
	;
719
	raise exc)
720
  )
721
  | ImportedNode nd ->
722
      type_imported_node env nd decl.top_decl_loc
723
  | ImportedFun nd ->
724
      type_imported_fun env nd decl.top_decl_loc
725
  | Consts clist ->
726
      type_top_consts env clist
727
  | Open _  -> env
728

    
729
let type_prog env decls =
730
try
731
  List.fold_left type_top_decl env decls
732
with Failure _ as exc -> raise exc
733

    
734
(* Once the Lustre program is fully typed,
735
   we must get back to the original description of dimensions,
736
   with constant parameters, instead of unifiable internal variables. *)
737

    
738
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types,
739
   i.e. replacing unifiable second_order variables with the original static parameters.
740
   Once restored in this formulation, dimensions may be meaningfully printed.
741
*)
742
let uneval_vdecl_generics vdecl =
743
 if vdecl.var_dec_const
744
 then
745
   match get_static_value vdecl.var_type with
746
   | None   -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)
747
   | Some d -> Dimension.uneval vdecl.var_id d
748

    
749
let uneval_node_generics vdecls =
750
  List.iter uneval_vdecl_generics vdecls
751

    
752
let uneval_top_generics decl =
753
  match decl.top_decl_desc with
754
  | Node nd ->
755
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
756
  | ImportedNode nd ->
757
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
758
  | ImportedFun nd ->
759
      ()
760
  | Consts clist -> ()
761
  | Open _  -> ()
762

    
763
let uneval_prog_generics prog =
764
 List.iter uneval_top_generics prog
765

    
766
let check_env_compat header declared computed = 
767
  uneval_prog_generics header;
768
  Env.iter declared (fun k decl_type_k -> 
769
    let computed_t = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
770
    (*Types.print_ty Format.std_formatter decl_type_k;
771
    Types.print_ty Format.std_formatter computed_t;*)
772
    try_semi_unify decl_type_k computed_t Location.dummy_loc
773
  ) 
774

    
775
(* Local Variables: *)
776
(* compile-command:"make -C .." *)
777
(* End: *)