Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ 01c7d5e1

History | View | Annotate | Download (28.5 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 | Treal, Treal -> 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 | Treal, Treal
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
  | Const_string _ -> assert false (* string should only appear in annotations *)
318

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

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

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

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

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

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

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

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

    
567

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

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

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

    
616
let type_var_decl_list vd_env env l =
617
  List.fold_left (type_var_decl vd_env) env l
618

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

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

    
628
let check_vd_env vd_env =
629
  ignore (List.fold_left add_vdecl [] vd_env)
630

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

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

    
678
let type_top_consts env clist =
679
  List.fold_left (fun env cdecl ->
680
    let ty = type_const cdecl.const_loc cdecl.const_value in
681
    let d =
682
      if is_dimension_type ty
683
      then dimension_of_const cdecl.const_loc cdecl.const_value
684
      else Dimension.mkdim_var () in
685
    let ty = Type_predef.type_static d ty in
686
    let new_env = Env.add_value env cdecl.const_id ty in
687
    cdecl.const_type <- ty;
688
    new_env) env clist
689

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

    
708
let type_prog env decls =
709
try
710
  List.fold_left type_top_decl env decls
711
with Failure _ as exc -> raise exc
712

    
713
(* Once the Lustre program is fully typed,
714
   we must get back to the original description of dimensions,
715
   with constant parameters, instead of unifiable internal variables. *)
716

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

    
728
let uneval_node_generics vdecls =
729
  List.iter uneval_vdecl_generics vdecls
730

    
731
let uneval_top_generics decl =
732
  match decl.top_decl_desc with
733
  | Node nd ->
734
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
735
  | ImportedNode nd ->
736
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
737
  | Consts clist -> ()
738
  | Open _  -> ()
739

    
740
let uneval_prog_generics prog =
741
 List.iter uneval_top_generics prog
742

    
743
let rec get_imported_node decls id =
744
  match decls with
745
  | [] -> assert false
746
  | decl::q ->
747
     (match decl.top_decl_desc with
748
      | ImportedNode nd when id = nd.nodei_id -> decl
749
      | _ -> get_imported_node q id)
750

    
751
let check_env_compat header declared computed = 
752
  uneval_prog_generics header;
753
  Env.iter declared (fun k decl_type_k -> 
754
    let computed_t = instantiate (ref []) (ref []) 
755
				 (try Env.lookup_value computed k
756
				  with Not_found ->
757
				    let loc = (get_imported_node header k).top_decl_loc in 
758
				    raise (Error (loc, Declared_but_undefined k))) in
759
    (*Types.print_ty Format.std_formatter decl_type_k;
760
    Types.print_ty Format.std_formatter computed_t;*)
761
    try_unify ~sub:true ~semi:true decl_type_k computed_t Location.dummy_loc
762
		    )
763

    
764
(* Local Variables: *)
765
(* compile-command:"make -C .." *)
766
(* End: *)