Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ 6affc9f5

History | View | Annotate | Download (28.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
  | 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
    | Tstruct fl, Tstruct fl' when fl == fl' -> ()
191
    | Tstatic (e1, t1'), Tstatic (e2, t2')
192
    | Tarray (e1, t1'), Tarray (e2, t2') ->
193
      begin
194
	unify t1' t2';
195
	Dimension.eval Basic_library.eval_env (fun c -> None) e1;
196
	Dimension.eval Basic_library.eval_env (fun c -> None) e2;
197
	Dimension.unify e1 e2;
198
      end
199
    | _,_ -> raise (Unify (t1, t2))
200

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

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

    
254
(* Expected type ty1, got type ty2 *)
255
let try_unify ty1 ty2 loc =
256
  try
257
    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 try_semi_unify ty1 ty2 loc =
265
  try
266
    semi_unify ty1 ty2
267
  with
268
  | Unify _ ->
269
    raise (Error (loc, Type_clash (ty1,ty2)))
270
  | Dimension.Unify _ ->
271
    raise (Error (loc, Type_clash (ty1,ty2)))
272

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

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

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

    
317
and type_const loc c = 
318
  match c with
319
  | Const_int _     -> Type_predef.type_int
320
  | Const_real _    -> Type_predef.type_real
321
  | Const_float _   -> Type_predef.type_real
322
  | Const_array ca  -> let d = Dimension.mkdim_int loc (List.length ca) in
323
		      let ty = new_var () in
324
		      List.iter (fun e -> try_unify ty (type_const loc e) loc) ca;
325
		      Type_predef.type_array d ty
326
  | Const_tag t     ->
327
    if Hashtbl.mem tag_table t
328
    then type_coretype (fun d -> ()) (Hashtbl.find tag_table t)
329
    else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
330
  | Const_struct fl ->
331
    let ty_struct = new_var () in
332
    begin
333
      let used =
334
	List.fold_left
335
	  (fun acc (l, c) ->
336
	    if List.mem l acc
337
	    then raise (Error (loc, Already_bound ("struct field " ^ l)))
338
	    else try_unify ty_struct (type_struct_const_field loc (l, c)) loc; l::acc)
339
	  [] fl in
340
      try
341
	let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in
342
(*	List.iter (fun l -> Format.eprintf "total: %s@." l) total;
343
	List.iter (fun l -> Format.eprintf "used: %s@." l) used; *)
344
	let undef = List.find (fun l -> not (List.mem l used)) total
345
	in raise (Error (loc, Unbound_value ("struct field " ^ undef)))
346
      with Not_found -> 
347
	ty_struct
348
    end
349

    
350
(* The following typing functions take as parameter an environment [env]
351
   and whether the element being typed is expected to be constant [const]. 
352
   [env] is a pair composed of:
353
  - a map from ident to type, associating to each ident, i.e. 
354
    variables, constants and (imported) nodes, its type including whether
355
    it is constant or not. This latter information helps in checking constant 
356
    propagation policy in Lustre.
357
  - a vdecl list, in order to modify types of declared variables that are
358
    later discovered to be clocks during the typing process.
359
*)
360
let check_constant loc const_expected const_real =
361
  if const_expected && not const_real
362
  then raise (Error (loc, Not_a_constant))
363

    
364
let rec type_standard_args env in_main const expr_list =
365
  let ty_list = List.map (fun e -> dynamic_type (type_expr env in_main const e)) expr_list in
366
  let ty_res = new_var () in
367
  List.iter2 (fun e ty -> try_unify ty_res ty e.expr_loc) expr_list ty_list;
368
  ty_res
369

    
370
(* emulates a subtyping relation between types t and (d : t),
371
   used during node applications and assignments *)
372
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
373
  let loc = real_arg.expr_loc in
374
  let const = const || (Types.get_static_value formal_type <> None) in
375
  let real_type = type_expr env in_main const real_arg in
376
  let real_type =
377
    if const
378
    then let d =
379
	   if is_dimension_type real_type
380
	   then dimension_of_expr real_arg
381
	   else Dimension.mkdim_var () in
382
	 let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
383
	 Dimension.eval Basic_library.eval_env eval_const d;
384
	 let real_static_type = Type_predef.type_static d (Types.dynamic_type real_type) in
385
	 (match Types.get_static_value real_type with
386
	 | None    -> ()
387
	 | Some d' -> try_unify real_type real_static_type loc);
388
	 real_static_type
389
    else real_type in
390
(*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;*)
391
  try_sub_unify sub real_type formal_type loc
392
(*
393
and type_subtyping_tuple loc real_type formal_type =
394
  let real_types   = type_list_of_type real_type in
395
  let formal_types = type_list_of_type formal_type in
396
  if (List.length real_types) <> (List.length formal_types)
397
  then raise (Unify (real_type, formal_type))
398
  else List.iter2 (type_subtyping loc sub) real_types formal_types
399

    
400
and type_subtyping loc sub real_type formal_type =
401
  match (repr real_type).tdesc, (repr formal_type).tdesc with
402
  | Tstatic _          , Tstatic _ when sub -> try_unify formal_type real_type loc
403
  | Tstatic (r_d, r_ty), _         when sub -> try_unify formal_type r_ty loc
404
  | _                                       -> try_unify formal_type real_type loc
405
*)
406
and type_ident env in_main loc const id =
407
  type_expr env in_main const (expr_of_ident id loc)
408

    
409
(* typing an application implies:
410
   - checking that const formal parameters match real const (maybe symbolic) arguments
411
   - checking type adequation between formal and real arguments
412
*)
413
and type_appl env in_main loc const f args =
414
  let tfun = type_ident env in_main loc const f in
415
  let tins, touts = split_arrow tfun in
416
  let tins = type_list_of_type tins in
417
  let args = expr_list_of_expr args in
418
  List.iter2 (type_subtyping_arg env in_main const) args tins;
419
  touts
420

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

    
535
and type_branches env in_main loc const hl =
536
  let typ_in = new_var () in
537
  let typ_out = new_var () in
538
  try
539
    let used_labels =
540
      List.fold_left (fun accu (t, h) ->
541
	unify typ_in (type_const loc (Const_tag t));
542
	type_subtyping_arg env in_main const h typ_out;
543
	if List.mem t accu
544
	then raise (Error (loc, Already_bound t))
545
	else t :: accu) [] hl in
546
    let type_labels = get_enum_type_tags (coretype_type typ_in) in
547
    if List.sort compare used_labels <> List.sort compare type_labels
548
    then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in
549
	 raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
550
    else (typ_in, typ_out)
551
  with Unify (t1, t2) ->
552
    raise (Error (loc, Type_clash (t1,t2)))
553

    
554
and update_clock env in_main id loc typ =
555
 (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*)
556
 try
557
   let vdecl = List.find (fun v -> v.var_id = id) (snd env)
558
   in vdecl.var_type <- typ
559
 with
560
   Not_found ->
561
   raise (Error (loc, Unbound_value ("clock " ^ id)))
562

    
563
(** [type_eq env eq] types equation [eq] in environment [env] *)
564
let type_eq env in_main undefined_vars eq =
565
  (* Check undefined variables, type lhs *)
566
  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
567
  let ty_lhs = type_expr env in_main false expr_lhs in
568
  (* Check multiple variable definitions *)
569
  let define_var id uvars =
570
    try
571
      ignore(IMap.find id uvars);
572
      IMap.remove id uvars
573
    with Not_found ->
574
      raise (Error (eq.eq_loc, Already_defined id))
575
  in
576
  let undefined_vars =
577
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
578
  (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
579
     to a (always non-constant) lhs variable *)
580
  type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
581
  undefined_vars
582

    
583

    
584
(* [type_coreclock env ck id loc] types the type clock declaration [ck]
585
   in environment [env] *)
586
let type_coreclock env ck id loc =
587
  match ck.ck_dec_desc with
588
  | Ckdec_any | Ckdec_pclock (_,_) -> ()
589
  | Ckdec_bool cl ->
590
      let dummy_id_expr = expr_of_ident id loc in
591
      let when_expr =
592
        List.fold_left
593
          (fun expr (x, l) ->
594
                {expr_tag = new_tag ();
595
                 expr_desc= Expr_when (expr,x,l);
596
                 expr_type = new_var ();
597
                 expr_clock = Clocks.new_var true;
598
                 expr_delay = Delay.new_var ();
599
                 expr_loc=loc;
600
		 expr_annot = None})
601
          dummy_id_expr cl
602
      in
603
      ignore (type_expr env false false when_expr)
604

    
605
let rec check_type_declaration loc cty =
606
 match cty with
607
 | Tydec_clock ty
608
 | Tydec_array (_, ty) -> check_type_declaration loc ty
609
 | Tydec_const tname   ->
610
   if not (Hashtbl.mem type_table cty)
611
   then raise (Error (loc, Unbound_type tname));
612
 | _                   -> ()
613

    
614
let type_var_decl vd_env env vdecl =
615
  check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
616
  let eval_const id = Types.get_static_value (Env.lookup_value env id) in
617
  let type_dim d =
618
    begin
619
      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;
620
      Dimension.eval Basic_library.eval_env eval_const d;
621
    end in
622
  let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
623
  let ty_status =
624
    if vdecl.var_dec_const
625
    then Type_predef.type_static (Dimension.mkdim_var ()) ty
626
    else ty in
627
  let new_env = Env.add_value env vdecl.var_id ty_status in
628
  type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
629
  vdecl.var_type <- ty_status;
630
  new_env
631

    
632
let type_var_decl_list vd_env env l =
633
  List.fold_left (type_var_decl vd_env) env l
634

    
635
let type_of_vlist vars =
636
  let tyl = List.map (fun v -> v.var_type) vars in
637
  type_of_type_list tyl
638

    
639
let add_vdecl vd_env vdecl =
640
 if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
641
 then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
642
 else vdecl::vd_env
643

    
644
let check_vd_env vd_env =
645
  ignore (List.fold_left add_vdecl [] vd_env)
646

    
647
(** [type_node env nd loc] types node [nd] in environment env. The
648
    location is used for error reports. *)
649
let type_node env nd loc =
650
  let is_main = nd.node_id = !Options.main_node in
651
  let vd_env_ol = nd.node_outputs@nd.node_locals in
652
  let vd_env =  nd.node_inputs@vd_env_ol in
653
  check_vd_env vd_env;
654
  let init_env = env in
655
  let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
656
  let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
657
  let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
658
  let new_env = Env.overwrite env delta_env in
659
  let undefined_vars_init =
660
    List.fold_left
661
      (fun uvs v -> IMap.add v.var_id () uvs)
662
      IMap.empty vd_env_ol in
663
  let undefined_vars =
664
    List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs
665
  in
666
  (* check that table is empty *)
667
  if (not (IMap.is_empty undefined_vars)) then
668
    raise (Error (loc, Undefined_var undefined_vars));
669
  let ty_ins = type_of_vlist nd.node_inputs in
670
  let ty_outs = type_of_vlist nd.node_outputs in
671
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
672
  generalize ty_node;
673
  (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
674
  nd.node_type <- ty_node;
675
  Env.add_value env nd.node_id ty_node
676

    
677
let type_imported_node env nd loc =
678
  let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
679
  let vd_env = nd.nodei_inputs@nd.nodei_outputs in
680
  check_vd_env vd_env;
681
  ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
682
  let ty_ins = type_of_vlist nd.nodei_inputs in
683
  let ty_outs = type_of_vlist nd.nodei_outputs in
684
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
685
  generalize ty_node;
686
(*
687
  if (is_polymorphic ty_node) then
688
    raise (Error (loc, Poly_imported_node nd.nodei_id));
689
*)
690
  let new_env = Env.add_value env nd.nodei_id ty_node in
691
  nd.nodei_type <- ty_node;
692
  new_env
693

    
694
let type_imported_fun env nd loc =
695
  let new_env = type_var_decl_list nd.fun_inputs env nd.fun_inputs in
696
  let vd_env =  nd.fun_inputs@nd.fun_outputs in
697
  check_vd_env vd_env;
698
  ignore(type_var_decl_list vd_env new_env nd.fun_outputs);
699
  let ty_ins = type_of_vlist nd.fun_inputs in
700
  let ty_outs = type_of_vlist nd.fun_outputs in
701
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
702
  generalize ty_node;
703
(*
704
  if (is_polymorphic ty_node) then
705
    raise (Error (loc, Poly_imported_node nd.fun_id));
706
*)
707
  let new_env = Env.add_value env nd.fun_id ty_node in
708
  nd.fun_type <- ty_node;
709
  new_env
710

    
711
let type_top_consts env clist =
712
  List.fold_left (fun env cdecl ->
713
    let ty = type_const cdecl.const_loc cdecl.const_value in
714
    let d =
715
      if is_dimension_type ty
716
      then dimension_of_const cdecl.const_loc cdecl.const_value
717
      else Dimension.mkdim_var () in
718
    let ty = Type_predef.type_static d ty in
719
    let new_env = Env.add_value env cdecl.const_id ty in
720
    cdecl.const_type <- ty;
721
    new_env) env clist
722

    
723
let type_top_decl env decl =
724
  match decl.top_decl_desc with
725
  | Node nd -> (
726
      try
727
	type_node env nd decl.top_decl_loc
728
      with Error (loc, err) as exc -> (
729
	if !Options.global_inline then
730
	  Format.eprintf "Type error: failing node@.%a@.@?"
731
	    Printers.pp_node nd
732
	;
733
	raise exc)
734
  )
735
  | ImportedNode nd ->
736
      type_imported_node env nd decl.top_decl_loc
737
  | ImportedFun nd ->
738
      type_imported_fun env nd decl.top_decl_loc
739
  | Consts clist ->
740
      type_top_consts env clist
741
  | Open _  -> env
742

    
743
let type_prog env decls =
744
try
745
  List.fold_left type_top_decl env decls
746
with Failure _ as exc -> raise exc
747

    
748
(* Once the Lustre program is fully typed,
749
   we must get back to the original description of dimensions,
750
   with constant parameters, instead of unifiable internal variables. *)
751

    
752
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types,
753
   i.e. replacing unifiable second_order variables with the original static parameters.
754
   Once restored in this formulation, dimensions may be meaningfully printed.
755
*)
756
let uneval_vdecl_generics vdecl =
757
 if vdecl.var_dec_const
758
 then
759
   match get_static_value vdecl.var_type with
760
   | None   -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)
761
   | Some d -> Dimension.uneval vdecl.var_id d
762

    
763
let uneval_node_generics vdecls =
764
  List.iter uneval_vdecl_generics vdecls
765

    
766
let uneval_top_generics decl =
767
  match decl.top_decl_desc with
768
  | Node nd ->
769
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
770
  | ImportedNode nd ->
771
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
772
  | ImportedFun nd ->
773
      ()
774
  | Consts clist -> ()
775
  | Open _  -> ()
776

    
777
let uneval_prog_generics prog =
778
 List.iter uneval_top_generics prog
779

    
780
let check_env_compat header declared computed = 
781
  uneval_prog_generics header;
782
  Env.iter declared (fun k decl_type_k -> 
783
    let computed_t = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
784
    (*Types.print_ty Format.std_formatter decl_type_k;
785
    Types.print_ty Format.std_formatter computed_t;*)
786
    try_semi_unify decl_type_k computed_t Location.dummy_loc
787
  ) 
788

    
789
(* Local Variables: *)
790
(* compile-command:"make -C .." *)
791
(* End: *)