Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ c1adf235

History | View | Annotate | Download (28.6 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
(* Equality on ground types only *)
148
(* Should be used between local variables which must have a ground type *)
149
let rec eq_ground t1 t2 =
150
  match t1.tdesc, t2.tdesc with
151
  | Tint, Tint | Tbool, Tbool | Trat, Trat -> true
152
  | Tenum tl, Tenum tl' when tl == tl' -> true
153
  | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> List.for_all2 eq_ground tl tl'
154
  | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' -> List.for_all2 (fun (_, t) (_, t') -> eq_ground t t') fl fl'
155
  | (Tconst t, _) ->
156
    let def_t = get_type_definition t in
157
    eq_ground def_t t2
158
  | (_, Tconst t)  ->
159
    let def_t = get_type_definition t in
160
    eq_ground t1 def_t
161
  | Tarrow (t1,t2), Tarrow (t1',t2') -> eq_ground t1 t1' && eq_ground t2 t2'
162
  | Tclock t1', Tclock t2' -> eq_ground t1' t2'
163
  | Tstatic (e1, t1'), Tstatic (e2, t2')
164
  | Tarray (e1, t1'), Tarray (e2, t2') -> Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'
165
  | _ -> false
166

    
167
(** [unify t1 t2] unifies types [t1] and [t2]
168
    using standard destructive unification.
169
    Raises [Unify (t1,t2)] if the types are not unifiable.
170
    [t1] is a expected/formal/spec type, [t2] is a computed/real/implem type,
171
    so in case of unification error: expected type [t1], got type [t2].
172
    If [sub]-typing is allowed, [t2] may be a subtype of [t1].
173
    If [semi] unification is required,
174
    [t1] should furthermore be an instance of [t2]
175
    and constants are handled differently.*)
176
let unify ?(sub=false) ?(semi=false) t1 t2 =
177
  let rec unif t1 t2 =
178
    let t1 = repr t1 in
179
    let t2 = repr t2 in
180
    if t1=t2 then
181
      ()
182
    else
183
      match t1.tdesc,t2.tdesc with
184
      (* strictly subtyping cases first *)
185
      | _ , Tclock t2 when sub && (get_clock_base_type t1 = None) ->
186
	unif t1 t2
187
      | _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) ->
188
	unif t1 t2
189
      (* This case is not mandatory but will keep "older" types *)
190
      | Tvar, Tvar ->
191
        if t1.tid < t2.tid then
192
          t2.tdesc <- Tlink t1
193
        else
194
          t1.tdesc <- Tlink t2
195
      | Tvar, _ when (not semi) && (not (occurs t1 t2)) ->
196
        t1.tdesc <- Tlink t2
197
      | _, Tvar when (not (occurs t2 t1)) ->
198
        t2.tdesc <- Tlink t1
199
      | Tarrow (t1,t2), Tarrow (t1',t2') ->
200
	begin
201
          unif t2 t2';
202
	  unif t1' t1
203
	end
204
      | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
205
	List.iter2 unif tl tl'
206
      | Ttuple [t1]        , _                  -> unif t1 t2
207
      | _                  , Ttuple [t2]        -> unif t1 t2
208
      | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
209
	List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'
210
      | Tclock _, Tstatic _
211
      | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
212
      | Tclock t1', Tclock t2' -> unif t1' t2'
213
      | Tint, Tint | Tbool, Tbool | Trat, Trat
214
      | Tunivar, _ | _, Tunivar -> ()
215
      | (Tconst t, _) ->
216
	let def_t = get_type_definition t in
217
	unif def_t t2
218
      | (_, Tconst t)  ->
219
	let def_t = get_type_definition t in
220
	unif t1 def_t
221
      | Tenum tl, Tenum tl' when tl == tl' -> ()
222
      | Tstatic (e1, t1'), Tstatic (e2, t2')
223
      | Tarray (e1, t1'), Tarray (e2, t2') ->
224
	let eval_const =
225
	  if semi
226
	  then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c))
227
	  else (fun c -> None) in
228
	begin
229
	  unif t1' t2';
230
	  Dimension.eval Basic_library.eval_env eval_const e1;
231
	  Dimension.eval Basic_library.eval_env eval_const e2;
232
	  Dimension.unify ~semi:semi e1 e2;
233
	end
234
      | _,_ -> raise (Unify (t1, t2))
235
  in unif t1 t2
236

    
237
(* Expected type ty1, got type ty2 *)
238
let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =
239
  try
240
    unify ~sub:sub ~semi:semi ty1 ty2
241
  with
242
  | Unify _ ->
243
    raise (Error (loc, Type_clash (ty1,ty2)))
244
  | Dimension.Unify _ ->
245
    raise (Error (loc, Type_clash (ty1,ty2)))
246

    
247
(* ty1 is a subtype of ty2 *)
248
(*
249
let rec sub_unify sub ty1 ty2 =
250
  match (repr ty1).tdesc, (repr ty2).tdesc with
251
  | Ttuple tl1         , Ttuple tl2         ->
252
    if List.length tl1 <> List.length tl2
253
    then raise (Unify (ty1, ty2))
254
    else List.iter2 (sub_unify sub) tl1 tl2
255
  | Ttuple [t1]        , _                  -> sub_unify sub t1 ty2
256
  | _                  , Ttuple [t2]        -> sub_unify sub ty1 t2
257
  | Tstruct tl1        , Tstruct tl2        ->
258
    if List.map fst tl1 <> List.map fst tl2
259
    then raise (Unify (ty1, ty2))
260
    else List.iter2 (fun (_, t1) (_, t2) -> sub_unify sub t1 t2) tl1 tl2
261
  | Tclock t1          , Tclock t2          -> sub_unify sub t1 t2
262
  | Tclock t1          , _   when sub       -> sub_unify sub t1 ty2
263
  | Tstatic (d1, t1)   , Tstatic (d2, t2)   ->
264
    begin
265
      sub_unify sub t1 t2;
266
      Dimension.eval Basic_library.eval_env (fun c -> None) d1;
267
      Dimension.eval Basic_library.eval_env (fun c -> None) d2;
268
      Dimension.unify d1 d2
269
    end
270
  | Tstatic (r_d, t1)  , _         when sub -> sub_unify sub t1 ty2
271
  | _                                       -> unify ty1 ty2
272
*)
273

    
274
let rec type_struct_const_field loc (label, c) =
275
  if Hashtbl.mem field_table label
276
  then let tydec = Hashtbl.find field_table label in
277
       let tydec_struct = get_struct_type_fields tydec in
278
       let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
279
       begin
280
	 try_unify ty_label (type_const loc c) loc;
281
	 type_coretype (fun d -> ()) tydec
282
       end
283
  else raise (Error (loc, Unbound_value ("struct field " ^ label)))
284

    
285
and type_const loc c = 
286
  match c with
287
  | Const_int _     -> Type_predef.type_int
288
  | Const_real _    -> Type_predef.type_real
289
  | Const_float _   -> Type_predef.type_real
290
  | Const_array ca  -> let d = Dimension.mkdim_int loc (List.length ca) in
291
		      let ty = new_var () in
292
		      List.iter (fun e -> try_unify ty (type_const loc e) loc) ca;
293
		      Type_predef.type_array d ty
294
  | Const_tag t     ->
295
    if Hashtbl.mem tag_table t
296
    then type_coretype (fun d -> ()) (Hashtbl.find tag_table t)
297
    else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
298
  | Const_struct fl ->
299
    let ty_struct = new_var () in
300
    begin
301
      let used =
302
	List.fold_left
303
	  (fun acc (l, c) ->
304
	    if List.mem l acc
305
	    then raise (Error (loc, Already_bound ("struct field " ^ l)))
306
	    else try_unify ty_struct (type_struct_const_field loc (l, c)) loc; l::acc)
307
	  [] fl in
308
      try
309
	let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in
310
(*	List.iter (fun l -> Format.eprintf "total: %s@." l) total;
311
	List.iter (fun l -> Format.eprintf "used: %s@." l) used; *)
312
	let undef = List.find (fun l -> not (List.mem l used)) total
313
	in raise (Error (loc, Unbound_value ("struct field " ^ undef)))
314
      with Not_found -> 
315
	ty_struct
316
    end
317

    
318
(* The following typing functions take as parameter an environment [env]
319
   and whether the element being typed is expected to be constant [const]. 
320
   [env] is a pair composed of:
321
  - a map from ident to type, associating to each ident, i.e. 
322
    variables, constants and (imported) nodes, its type including whether
323
    it is constant or not. This latter information helps in checking constant 
324
    propagation policy in Lustre.
325
  - a vdecl list, in order to modify types of declared variables that are
326
    later discovered to be clocks during the typing process.
327
*)
328
let check_constant loc const_expected const_real =
329
  if const_expected && not const_real
330
  then raise (Error (loc, Not_a_constant))
331

    
332
let rec type_standard_args env in_main const expr_list =
333
  let ty_list =
334
    List.map
335
      (fun e -> let ty = dynamic_type (type_expr env in_main const e) in
336
		match get_clock_base_type ty with
337
		| None    -> ty
338
		| Some ty -> ty)
339
      expr_list in
340
  let ty_res = new_var () in
341
  List.iter2 (fun e ty -> try_unify ty_res ty e.expr_loc) expr_list ty_list;
342
  ty_res
343

    
344
(* emulates a subtyping relation between types t and (d : t),
345
   used during node applications and assignments *)
346
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
347
  let loc = real_arg.expr_loc in
348
  let const = const || (Types.get_static_value formal_type <> None) in
349
  let real_type = type_expr env in_main const real_arg in
350
  let real_type =
351
    if const
352
    then let d =
353
	   if is_dimension_type real_type
354
	   then dimension_of_expr real_arg
355
	   else Dimension.mkdim_var () in
356
	 let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
357
	 Dimension.eval Basic_library.eval_env eval_const d;
358
	 let real_static_type = Type_predef.type_static d (Types.dynamic_type real_type) in
359
	 (match Types.get_static_value real_type with
360
	 | None    -> ()
361
	 | Some d' -> try_unify real_type real_static_type loc);
362
	 real_static_type
363
    else real_type in
364
  (*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;*)
365
  try_unify ~sub:sub formal_type real_type loc
366

    
367
and type_ident env in_main loc const id =
368
  type_expr env in_main const (expr_of_ident id loc)
369

    
370
(* typing an application implies:
371
   - checking that const formal parameters match real const (maybe symbolic) arguments
372
   - checking type adequation between formal and real arguments
373
   An application may embed an homomorphic/internal function, in which case we need to split
374
   it in many calls
375
*)
376
and type_appl env in_main loc const f args =
377
  let args = expr_list_of_expr args in
378
  if Basic_library.is_internal_fun f && List.exists is_tuple_expr args
379
  then
380
    try
381
      let args = Utils.transpose_list (List.map expr_list_of_expr args) in
382
      Types.type_of_type_list (List.map (type_call env in_main loc const f) args)
383
    with
384
      Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l')))
385
  else
386
    type_call env in_main loc const f args
387

    
388
(* type a (single) call. [args] is here a list of arguments. *)
389
and type_call env in_main loc const f args =
390
  let tins, touts = new_var (), new_var () in
391
  let tfun = Type_predef.type_arrow tins touts in
392
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
393
  let tins = type_list_of_type tins in
394
  if List.length args <> List.length tins then
395
    raise (Error (loc, WrongArity (List.length tins, List.length args)))
396
  else
397
    List.iter2 (type_subtyping_arg env in_main const) args tins;
398
  touts
399

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

    
516
and type_branches env in_main loc const hl =
517
  let typ_in = new_var () in
518
  let typ_out = new_var () in
519
  try
520
    let used_labels =
521
      List.fold_left (fun accu (t, h) ->
522
	unify typ_in (type_const loc (Const_tag t));
523
	type_subtyping_arg env in_main const h typ_out;
524
	if List.mem t accu
525
	then raise (Error (loc, Already_bound t))
526
	else t :: accu) [] hl in
527
    let type_labels = get_enum_type_tags (coretype_type typ_in) in
528
    if List.sort compare used_labels <> List.sort compare type_labels
529
    then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in
530
	 raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
531
    else (typ_in, typ_out)
532
  with Unify (t1, t2) ->
533
    raise (Error (loc, Type_clash (t1,t2)))
534
(*
535
and update_clock env in_main id loc typ =
536
 (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*)
537
 try
538
   let vdecl = List.find (fun v -> v.var_id = id) (snd env)
539
   in vdecl.var_type <- typ
540
 with
541
   Not_found ->
542
   raise (Error (loc, Unbound_value ("clock " ^ id)))
543
*)
544
(** [type_eq env eq] types equation [eq] in environment [env] *)
545
let type_eq env in_main undefined_vars eq =
546
  (* Check undefined variables, type lhs *)
547
  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
548
  let ty_lhs = type_expr env in_main false expr_lhs in
549
  (* Check multiple variable definitions *)
550
  let define_var id uvars =
551
    try
552
      ignore(IMap.find id uvars);
553
      IMap.remove id uvars
554
    with Not_found ->
555
      raise (Error (eq.eq_loc, Already_defined id))
556
  in
557
  (* check assignment of declared constant, assignment of clock *)
558
  let ty_lhs =
559
    type_of_type_list
560
      (List.map2 (fun ty id ->
561
	if get_static_value ty <> None
562
	then raise (Error (eq.eq_loc, Assigned_constant id)) else
563
	match get_clock_base_type ty with
564
	| None -> ty
565
	| Some ty -> ty)
566
	 (type_list_of_type ty_lhs) eq.eq_lhs) in
567
  let undefined_vars =
568
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
569
  (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
570
     to a (always non-constant) lhs variable *)
571
  type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
572
  undefined_vars
573

    
574

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

    
596
let rec check_type_declaration loc cty =
597
 match cty with
598
 | Tydec_clock ty
599
 | Tydec_array (_, ty) -> check_type_declaration loc ty
600
 | Tydec_const tname   ->
601
   if not (Hashtbl.mem type_table cty)
602
   then raise (Error (loc, Unbound_type tname));
603
 | _                   -> ()
604

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

    
623
let type_var_decl_list vd_env env l =
624
  List.fold_left (type_var_decl vd_env) env l
625

    
626
let type_of_vlist vars =
627
  let tyl = List.map (fun v -> v.var_type) vars in
628
  type_of_type_list tyl
629

    
630
let add_vdecl vd_env vdecl =
631
 if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
632
 then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
633
 else vdecl::vd_env
634

    
635
let check_vd_env vd_env =
636
  ignore (List.fold_left add_vdecl [] vd_env)
637

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

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

    
685
let type_top_consts env clist =
686
  List.fold_left (fun env cdecl ->
687
    let ty = type_const cdecl.const_loc cdecl.const_value in
688
    let d =
689
      if is_dimension_type ty
690
      then dimension_of_const cdecl.const_loc cdecl.const_value
691
      else Dimension.mkdim_var () in
692
    let ty = Type_predef.type_static d ty in
693
    let new_env = Env.add_value env cdecl.const_id ty in
694
    cdecl.const_type <- ty;
695
    new_env) env clist
696

    
697
let type_top_decl env decl =
698
  match decl.top_decl_desc with
699
  | Node nd -> (
700
      try
701
	type_node env nd decl.top_decl_loc
702
      with Error (loc, err) as exc -> (
703
	if !Options.global_inline then
704
	  Format.eprintf "Type error: failing node@.%a@.@?"
705
	    Printers.pp_node nd
706
	;
707
	raise exc)
708
  )
709
  | ImportedNode nd ->
710
      type_imported_node env nd decl.top_decl_loc
711
  | Consts clist ->
712
      type_top_consts env clist
713
  | Open _  -> env
714

    
715
let type_prog env decls =
716
try
717
  List.fold_left type_top_decl env decls
718
with Failure _ as exc -> raise exc
719

    
720
(* Once the Lustre program is fully typed,
721
   we must get back to the original description of dimensions,
722
   with constant parameters, instead of unifiable internal variables. *)
723

    
724
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types,
725
   i.e. replacing unifiable second_order variables with the original static parameters.
726
   Once restored in this formulation, dimensions may be meaningfully printed.
727
*)
728
let uneval_vdecl_generics vdecl =
729
 if vdecl.var_dec_const
730
 then
731
   match get_static_value vdecl.var_type with
732
   | None   -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)
733
   | Some d -> Dimension.uneval vdecl.var_id d
734

    
735
let uneval_node_generics vdecls =
736
  List.iter uneval_vdecl_generics vdecls
737

    
738
let uneval_top_generics decl =
739
  match decl.top_decl_desc with
740
  | Node nd ->
741
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
742
  | ImportedNode nd ->
743
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
744
  | Consts clist -> ()
745
  | Open _  -> ()
746

    
747
let uneval_prog_generics prog =
748
 List.iter uneval_top_generics prog
749

    
750
let rec get_imported_node decls id =
751
  match decls with
752
  | [] -> assert false
753
  | decl::q ->
754
     (match decl.top_decl_desc with
755
      | ImportedNode nd when id = nd.nodei_id -> decl
756
      | _ -> get_imported_node q id)
757

    
758
let check_env_compat header declared computed = 
759
  uneval_prog_generics header;
760
  Env.iter declared (fun k decl_type_k -> 
761
    let computed_t = instantiate (ref []) (ref []) 
762
				 (try Env.lookup_value computed k
763
				  with Not_found ->
764
				    let loc = (get_imported_node header k).top_decl_loc in 
765
				    raise (Error (loc, Declared_but_undefined k))) in
766
    (*Types.print_ty Format.std_formatter decl_type_k;
767
    Types.print_ty Format.std_formatter computed_t;*)
768
    try_unify ~sub:true ~semi:true decl_type_k computed_t Location.dummy_loc
769
		    )
770

    
771
(* Local Variables: *)
772
(* compile-command:"make -C .." *)
773
(* End: *)