Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ 2196a0a6

History | View | Annotate | Download (30.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 Corelang
35
open Types
36
open Format
37

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

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

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

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

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

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

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

    
146
(** [unify t1 t2] unifies types [t1] and [t2]. Raises [Unify
147
    (t1,t2)] if the types are not unifiable.*)
148
(* Standard destructive unification *)
149
let rec unify t1 t2 =
150
  let t1 = repr t1 in
151
  let t2 = repr t2 in
152
  if t1=t2 then
153
    ()
154
  else
155
    (* No type abbreviations resolution for now *)
156
    match t1.tdesc,t2.tdesc with
157
      (* This case is not mandory but will keep "older" types *)
158
    | Tvar, Tvar ->
159
        if t1.tid < t2.tid then
160
          t2.tdesc <- Tlink t1
161
        else
162
          t1.tdesc <- Tlink t2
163
    | (Tvar, _) when (not (occurs t1 t2)) ->
164
        t1.tdesc <- Tlink t2
165
    | (_,Tvar) when (not (occurs t2 t1)) ->
166
        t2.tdesc <- Tlink t1
167
    | Tarrow (t1,t2), Tarrow (t1',t2') ->
168
      begin
169
        unify t1 t1';
170
	unify t2 t2'
171
      end
172
    | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
173
      List.iter2 unify tl tl'
174
    | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
175
      List.iter2 (fun (_, t) (_, t') -> unify t t') fl fl'
176
    | Tclock _, Tstatic _
177
    | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
178
    | Tclock t1', _ -> unify t1' t2
179
    | _, Tclock t2' -> unify t1 t2'
180
    | Tint, Tint | Tbool, Tbool | Trat, Trat
181
    | Tunivar, _ | _, Tunivar -> ()
182
    | (Tconst t, _) ->
183
      let def_t = get_type_definition t in
184
      unify def_t t2
185
    | (_, Tconst t)  ->
186
      let def_t = get_type_definition t in
187
      unify t1 def_t
188
    | Tenum tl, Tenum tl' when tl == tl' -> ()
189
    | Tstruct fl, Tstruct fl' when fl == fl' -> ()
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 rec type_struct_const_field loc (label, c) =
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 (type_const loc c) loc;
312
	 type_coretype (fun d -> ()) tydec
313
       end
314
  else raise (Error (loc, Unbound_value ("struct field " ^ label)))
315

    
316
and 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_string _ -> Type_predef.type_string
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
  (* Format.eprintf "Typing function call %s: %a@.@?" f print_ty tfun ; *)
416
  let tins, touts = split_arrow tfun in
417
  let tins = type_list_of_type tins in
418
  let args = expr_list_of_expr args in
419
  List.iter2 (type_subtyping_arg env in_main const) args tins;
420
  touts
421

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

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

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

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

    
589

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

    
611
let rec check_type_declaration loc cty =
612
 match cty with
613
 | Tydec_clock ty
614
 | Tydec_array (_, ty) -> check_type_declaration loc ty
615
 | Tydec_const tname   ->
616
   if not (Hashtbl.mem type_table cty)
617
   then raise (Error (loc, Unbound_type tname));
618
 | _                   -> ()
619

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

    
638
let type_var_decl_list vd_env env l =
639
  List.fold_left (type_var_decl vd_env) env l
640

    
641
let type_of_vlist vars =
642
  let tyl = List.map (fun v -> v.var_type) vars in
643
  type_of_type_list tyl
644

    
645
let add_vdecl vd_env vdecl =
646
 if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
647
 then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
648
 else vdecl::vd_env
649

    
650
let check_vd_env vd_env =
651
  ignore (List.fold_left add_vdecl [] vd_env)
652

    
653
let type_eexpr (env, vdecl) ee =
654
  let quantified_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
655
  let env = type_var_decl_list vdecl env quantified_vars in
656
  let ty = type_expr (env, vdecl) false (* not in main *) false (* not in const *) ee.eexpr_qfexpr in
657
  ee.eexpr_type <- ty
658

    
659
let type_spec env ns =
660
  let type_ee_list l = List.iter (fun e -> ignore (type_eexpr env e) ) l in
661
  let type_beh (_, req, ens, beh_loc) =
662
    type_ee_list req; type_ee_list ens
663
  in 
664
  List.iter type_beh (("default", ns.requires, ns.ensures, ns.spec_loc)::ns.behaviors)
665

    
666
let type_annot env na =
667
  List.iter (fun (_, ee) -> type_eexpr env ee) na.annots
668

    
669
(** [type_node env nd loc] types node [nd] in environment env. The
670
    location is used for error reports. *)
671
let type_node env nd loc =
672
  let is_main = nd.node_id = !Options.main_node in
673
  let vd_env_ol = nd.node_outputs@nd.node_locals in
674
  let vd_env =  nd.node_inputs@vd_env_ol in
675
  check_vd_env vd_env;
676
  let init_env = env in
677
  let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
678
  let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
679

    
680
  (* Typing specification *)
681
  let _ =
682
    match nd.node_spec with
683
    | Some ns -> (
684
      try
685
	(* Format.eprintf "Typing specification: %a@.@?" *)
686
	(*   Printers.pp_spec ns; *)
687
	type_spec (delta_env, vd_env) ns
688
      with _ as exc -> (
689
	Format.eprintf "Error typing specification: %a@."
690
	  Printers.pp_spec ns;
691
	raise exc
692
      )
693
    )	
694
      | None -> ()
695
  in
696

    
697
  (* Typing node content *)
698
  let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
699
  let new_env = Env.overwrite env delta_env in
700
  let undefined_vars_init =
701
    List.fold_left
702
      (fun uvs v -> IMap.add v.var_id () uvs)
703
      IMap.empty vd_env_ol in
704
  let undefined_vars =
705
    List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs
706
  in
707
  (* check that table is empty *)
708
  if (not (IMap.is_empty undefined_vars)) then
709
    raise (Error (loc, Undefined_var undefined_vars));
710
  
711
  (* Typing node annotations *)
712
  let _ = List.map (fun ann -> 
713
		      type_annot (new_env, vd_env) ann
714
  ) nd.node_annot in
715

    
716
  let ty_ins = type_of_vlist nd.node_inputs in
717
  let ty_outs = type_of_vlist nd.node_outputs in
718
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
719
  generalize ty_node;
720
  (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
721
  nd.node_type <- ty_node;
722
  (* Format.eprintf "Node %s type is %a@." nd.node_id Types.print_ty ty_node; *)
723
  Env.add_value env nd.node_id ty_node
724

    
725
let type_imported_node env nd loc =
726
  let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
727
  let vd_env = nd.nodei_inputs@nd.nodei_outputs in
728
  check_vd_env vd_env;
729
  ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
730
  let ty_ins = type_of_vlist nd.nodei_inputs in
731
  let ty_outs = type_of_vlist nd.nodei_outputs in
732
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
733
  generalize ty_node;
734
(*
735
  if (is_polymorphic ty_node) then
736
    raise (Error (loc, Poly_imported_node nd.nodei_id));
737
*)
738
  let new_env = Env.add_value env nd.nodei_id ty_node in
739
  nd.nodei_type <- ty_node;
740
  new_env
741

    
742
let type_imported_fun env nd loc =
743
  let new_env = type_var_decl_list nd.fun_inputs env nd.fun_inputs in
744
  let vd_env =  nd.fun_inputs@nd.fun_outputs in
745
  check_vd_env vd_env;
746
  ignore(type_var_decl_list vd_env new_env nd.fun_outputs);
747
  let ty_ins = type_of_vlist nd.fun_inputs in
748
  let ty_outs = type_of_vlist nd.fun_outputs in
749
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
750
  generalize ty_node;
751
(*
752
  if (is_polymorphic ty_node) then
753
    raise (Error (loc, Poly_imported_node nd.fun_id));
754
*)
755
  let new_env = Env.add_value env nd.fun_id ty_node in
756
  nd.fun_type <- ty_node;
757
  new_env
758

    
759
let type_top_consts env clist =
760
  List.fold_left (fun env cdecl ->
761
    let ty = type_const cdecl.const_loc cdecl.const_value in
762
    let d =
763
      if is_dimension_type ty
764
      then dimension_of_const cdecl.const_loc cdecl.const_value
765
      else Dimension.mkdim_var () in
766
    let ty = Type_predef.type_static d ty in
767
    let new_env = Env.add_value env cdecl.const_id ty in
768
    cdecl.const_type <- ty;
769
    new_env) env clist
770

    
771
let type_top_decl env decl =
772
  match decl.top_decl_desc with
773
  | Node nd -> (
774
      try
775
	type_node env nd decl.top_decl_loc
776
      with Error (loc, err) as exc -> (
777
	if !Options.global_inline then
778
	  Format.eprintf "Type error: failing node@.%a@.@?"
779
	    Printers.pp_node nd
780
	;
781
	raise exc)
782
  )
783
  | ImportedNode nd ->
784
      type_imported_node env nd decl.top_decl_loc
785
  | ImportedFun nd ->
786
      type_imported_fun env nd decl.top_decl_loc
787
  | Consts clist ->
788
      type_top_consts env clist
789
  | Open _  -> env
790

    
791
let type_prog env decls =
792
try
793
  List.fold_left type_top_decl env decls
794
with Failure _ as exc -> raise exc
795

    
796
(* Once the Lustre program is fully typed,
797
   we must get back to the original description of dimensions,
798
   with constant parameters, instead of unifiable internal variables. *)
799

    
800
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types,
801
   i.e. replacing unifiable second_order variables with the original static parameters.
802
   Once restored in this formulation, dimensions may be meaningfully printed.
803
*)
804
let uneval_vdecl_generics vdecl =
805
 if vdecl.var_dec_const
806
 then
807
   match get_static_value vdecl.var_type with
808
   | None   -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)
809
   | Some d -> Dimension.uneval vdecl.var_id d
810

    
811
let uneval_node_generics vdecls =
812
  List.iter uneval_vdecl_generics vdecls
813

    
814
let uneval_top_generics decl =
815
  match decl.top_decl_desc with
816
  | Node nd ->
817
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
818
  | ImportedNode nd ->
819
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
820
  | ImportedFun nd ->
821
      ()
822
  | Consts clist -> ()
823
  | Open _  -> ()
824

    
825
let uneval_prog_generics prog =
826
 List.iter uneval_top_generics prog
827

    
828
let check_env_compat header declared computed = 
829
  uneval_prog_generics header;
830
  Env.iter declared (fun k decl_type_k -> 
831
    let computed_t = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
832
    (*Types.print_ty Format.std_formatter decl_type_k;
833
    Types.print_ty Format.std_formatter computed_t;*)
834
    try_semi_unify decl_type_k computed_t Location.dummy_loc
835
  ) 
836

    
837
(* Local Variables: *)
838
(* compile-command:"make -C .." *)
839
(* End: *)