Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ 6aeb3388

History | View | Annotate | Download (28.1 KB)

1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - LIFL             *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *) 
10
(*  This file was originally from the Prelude compiler              *)
11
(*                                                                  *) 
12
(********************************************************************)
13

    
14
(** Main typing module. Classic inference algorithm with destructive
15
    unification. *)
16

    
17
let debug fmt args = () (* Format.eprintf "%a"  *)
18
(* Though it shares similarities with the clock calculus module, no code
19
    is shared.  Simple environments, very limited identifier scoping, no
20
    identifier redefinition allowed. *)
21

    
22
open Utils
23
(* Yes, opening both modules is dirty as some type names will be
24
   overwritten, yet this makes notations far lighter.*)
25
open LustreSpec
26
open Corelang
27
open Types
28
open Format
29

    
30
let pp_typing_env fmt env =
31
  Env.pp_env print_ty fmt env
32

    
33
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in
34
    type [ty]. False otherwise. *)
35
let rec occurs tvar ty =
36
  let ty = repr ty in
37
  match ty.tdesc with
38
  | Tvar -> ty=tvar
39
  | Tarrow (t1, t2) ->
40
      (occurs tvar t1) || (occurs tvar t2)
41
  | Ttuple tl ->
42
     List.exists (occurs tvar) tl
43
  | Tstruct fl ->
44
     List.exists (fun (f, t) -> occurs tvar t) fl
45
  | Tarray (_, t)
46
  | Tstatic (_, t)
47
  | Tclock t
48
  | Tlink t -> occurs tvar t
49
  | Tenum _ | Tconst _ | Tunivar | Tint | Treal | Tbool | Trat -> false
50

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

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

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

    
118
(* [coretype_type] is the reciprocal of [type_typecore] *)
119
let rec coretype_type ty =
120
 match (repr ty).tdesc with
121
 | Tvar           -> Tydec_any
122
 | Tint           -> Tydec_int
123
 | Treal          -> Tydec_real
124
 | Tbool          -> Tydec_bool
125
 | Tconst c       -> Tydec_const c
126
 | Tclock t       -> Tydec_clock (coretype_type t)
127
 | Tenum tl       -> Tydec_enum tl
128
 | Tstruct fl     -> Tydec_struct (List.map (fun (f, t) -> (f, coretype_type t)) fl)
129
 | Tarray (d, t)  -> Tydec_array (d, coretype_type t)
130
 | Tstatic (_, t) -> coretype_type t
131
 | _         -> assert false
132

    
133
let get_type_definition tname =
134
  try
135
    type_coretype (fun d -> ()) (Hashtbl.find type_table (Tydec_const tname))
136
  with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
137

    
138
(* Equality on ground types only *)
139
(* Should be used between local variables which must have a ground type *)
140
let rec eq_ground t1 t2 =
141
  let t1 = repr t1 in
142
  let t2 = repr t2 in
143
  t1==t2 ||
144
  match t1.tdesc, t2.tdesc with
145
  | Tint, Tint | Tbool, Tbool | Trat, Trat | Treal, Treal -> true
146
  | Tenum tl, Tenum tl' when tl == tl' -> true
147
  | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> List.for_all2 eq_ground tl tl'
148
  | 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'
149
  | (Tconst t, _) ->
150
    let def_t = get_type_definition t in
151
    eq_ground def_t t2
152
  | (_, Tconst t)  ->
153
    let def_t = get_type_definition t in
154
    eq_ground t1 def_t
155
  | Tarrow (t1,t2), Tarrow (t1',t2') -> eq_ground t1 t1' && eq_ground t2 t2'
156
  | Tclock t1', Tclock t2' -> eq_ground t1' t2'
157
  | Tstatic (e1, t1'), Tstatic (e2, t2')
158
  | Tarray (e1, t1'), Tarray (e2, t2') -> Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'
159
  | _ -> false
160

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

    
231
(* Expected type ty1, got type ty2 *)
232
let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =
233
  try
234
    unify ~sub:sub ~semi:semi ty1 ty2
235
  with
236
  | Unify _ ->
237
    raise (Error (loc, Type_clash (ty1,ty2)))
238
  | Dimension.Unify _ ->
239
    raise (Error (loc, Type_clash (ty1,ty2)))
240

    
241
let rec type_struct_const_field loc (label, c) =
242
  if Hashtbl.mem field_table label
243
  then let tydec = Hashtbl.find field_table label in
244
       let tydec_struct = get_struct_type_fields tydec in
245
       let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
246
       begin
247
	 try_unify ty_label (type_const loc c) loc;
248
	 type_coretype (fun d -> ()) tydec
249
       end
250
  else raise (Error (loc, Unbound_value ("struct field " ^ label)))
251

    
252
and type_const loc c = 
253
  match c with
254
  | Const_int _     -> Type_predef.type_int
255
  | Const_real _    -> Type_predef.type_real
256
  | Const_float _   -> Type_predef.type_real
257
  | Const_array ca  -> let d = Dimension.mkdim_int loc (List.length ca) in
258
		      let ty = new_var () in
259
		      List.iter (fun e -> try_unify ty (type_const loc e) loc) ca;
260
		      Type_predef.type_array d ty
261
  | Const_tag t     ->
262
    if Hashtbl.mem tag_table t
263
    then type_coretype (fun d -> ()) (Hashtbl.find tag_table t)
264
    else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
265
  | Const_struct fl ->
266
    let ty_struct = new_var () in
267
    begin
268
      let used =
269
	List.fold_left
270
	  (fun acc (l, c) ->
271
	    if List.mem l acc
272
	    then raise (Error (loc, Already_bound ("struct field " ^ l)))
273
	    else try_unify ty_struct (type_struct_const_field loc (l, c)) loc; l::acc)
274
	  [] fl in
275
      try
276
	let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in
277
(*	List.iter (fun l -> Format.eprintf "total: %s@." l) total;
278
	List.iter (fun l -> Format.eprintf "used: %s@." l) used; *)
279
	let undef = List.find (fun l -> not (List.mem l used)) total
280
	in raise (Error (loc, Unbound_value ("struct field " ^ undef)))
281
      with Not_found -> 
282
	ty_struct
283
    end
284
  | Const_string _ -> assert false (* string should only appear in annotations *)
285

    
286
(* The following typing functions take as parameter an environment [env]
287
   and whether the element being typed is expected to be constant [const]. 
288
   [env] is a pair composed of:
289
  - a map from ident to type, associating to each ident, i.e. 
290
    variables, constants and (imported) nodes, its type including whether
291
    it is constant or not. This latter information helps in checking constant 
292
    propagation policy in Lustre.
293
  - a vdecl list, in order to modify types of declared variables that are
294
    later discovered to be clocks during the typing process.
295
*)
296
let check_constant loc const_expected const_real =
297
  if const_expected && not const_real
298
  then raise (Error (loc, Not_a_constant))
299

    
300
let rec type_add_const env const arg targ =
301
  if const
302
  then let d =
303
	 if is_dimension_type targ
304
	 then dimension_of_expr arg
305
	 else Dimension.mkdim_var () in
306
       let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
307
       Dimension.eval Basic_library.eval_env eval_const d;
308
       let real_static_type = Type_predef.type_static d (Types.dynamic_type targ) in
309
       (match Types.get_static_value targ with
310
       | None    -> ()
311
       | Some d' -> try_unify targ real_static_type arg.expr_loc);
312
       real_static_type
313
  else targ
314

    
315
(* emulates a subtyping relation between types t and (d : t),
316
   used during node applications and assignments *)
317
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
318
  let loc = real_arg.expr_loc in
319
  let const = const || (Types.get_static_value formal_type <> None) in
320
  let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in
321
  (*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;*)
322
  try_unify ~sub:sub formal_type real_type loc
323

    
324
and type_ident env in_main loc const id =
325
  type_expr env in_main const (expr_of_ident id loc)
326

    
327
(* typing an application implies:
328
   - checking that const formal parameters match real const (maybe symbolic) arguments
329
   - checking type adequation between formal and real arguments
330
   An application may embed an homomorphic/internal function, in which case we need to split
331
   it in many calls
332
*)
333
and type_appl env in_main loc const f args =
334
  let targs = List.map (type_expr env in_main const) args in
335
  if Basic_library.is_internal_fun f && List.exists is_tuple_type targs
336
  then
337
    try
338
      let targs = Utils.transpose_list (List.map type_list_of_type targs) in
339
      Types.type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)
340
    with
341
      Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l')))
342
  else
343
    type_dependent_call env in_main loc const f (List.combine args targs)
344

    
345
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)
346
and type_dependent_call env in_main loc const f targs =
347
  let tins, touts = new_var (), new_var () in
348
  let tfun = Type_predef.type_arrow tins touts in
349
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
350
  let tins = type_list_of_type tins in
351
  if List.length targs <> List.length tins then
352
    raise (Error (loc, WrongArity (List.length tins, List.length targs)))
353
  else
354
    begin
355
      List.iter2 (fun (a,t) ti ->
356
	let t' = type_add_const env (const || Types.get_static_value ti <> None) a t
357
	in try_unify ~sub:true ti t' a.expr_loc) targs tins;
358
      touts
359
    end
360

    
361
(* type a simple call without dependent types 
362
   but possible homomorphic extension.
363
   [targs] is here a list of arguments' types. *)
364
and type_simple_call env in_main loc const f targs =
365
  let tins, touts = new_var (), new_var () in
366
  let tfun = Type_predef.type_arrow tins touts in
367
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
368
  (*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*)
369
  try_unify ~sub:true tins (type_of_type_list targs) loc;
370
  touts
371

    
372
(** [type_expr env in_main expr] types expression [expr] in environment
373
    [env], expecting it to be [const] or not. *)
374
and type_expr env in_main const expr =
375
  let resulting_ty = 
376
  match expr.expr_desc with
377
  | Expr_const c ->
378
    let ty = type_const expr.expr_loc c in
379
    let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in
380
    expr.expr_type <- ty;
381
    ty
382
  | Expr_ident v ->
383
    let tyv =
384
      try
385
        Env.lookup_value (fst env) v
386
      with Not_found ->
387
	Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr;
388
        raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))
389
    in
390
    let ty = instantiate (ref []) (ref []) tyv in
391
    let ty' =
392
      if const
393
      then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ())
394
      else new_var () in
395
    try_unify ty ty' expr.expr_loc;
396
    expr.expr_type <- ty;
397
    ty 
398
  | Expr_array elist ->
399
    let ty_elt = new_var () in
400
    List.iter (fun e -> try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist;
401
    let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
402
    let ty = Type_predef.type_array d ty_elt in
403
    expr.expr_type <- ty;
404
    ty
405
  | Expr_access (e1, d) ->
406
    type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
407
    let ty_elt = new_var () in
408
    let d = Dimension.mkdim_var () in
409
    type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt);
410
    expr.expr_type <- ty_elt;
411
    ty_elt
412
  | Expr_power (e1, d) ->
413
    let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
414
    type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
415
    Dimension.eval Basic_library.eval_env eval_const d;
416
    let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in
417
    let ty = Type_predef.type_array d ty_elt in
418
    expr.expr_type <- ty;
419
    ty
420
  | Expr_tuple elist ->
421
    let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in
422
    expr.expr_type <- ty;
423
    ty
424
  | Expr_ite (c, t, e) ->
425
    type_subtyping_arg env in_main const c Type_predef.type_bool;
426
    let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in
427
    expr.expr_type <- ty;
428
    ty
429
  | Expr_appl (id, args, r) ->
430
    (* application of non internal function is not legal in a constant
431
       expression *)
432
    (match r with
433
    | None        -> ()
434
    | Some (x, l) -> 
435
      check_constant expr.expr_loc const false;
436
      let expr_x = expr_of_ident x expr.expr_loc in	
437
      let typ_l = 
438
	Type_predef.type_clock 
439
	  (type_const expr.expr_loc (Const_tag l)) in
440
      type_subtyping_arg env in_main ~sub:false const expr_x typ_l);
441
    let touts = type_appl env in_main expr.expr_loc const id (expr_list_of_expr args) in
442
    expr.expr_type <- touts;
443
    touts
444
  | Expr_fby (e1,e2)
445
  | Expr_arrow (e1,e2) ->
446
    (* fby/arrow is not legal in a constant expression *)
447
    check_constant expr.expr_loc const false;
448
    let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in
449
    expr.expr_type <- ty;
450
    ty
451
  | Expr_pre e ->
452
    (* pre is not legal in a constant expression *)
453
    check_constant expr.expr_loc const false;
454
    let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in
455
    expr.expr_type <- ty;
456
    ty
457
  | Expr_when (e1,c,l) ->
458
    (* when is not legal in a constant expression *)
459
    check_constant expr.expr_loc const false;
460
    let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in
461
    let expr_c = expr_of_ident c expr.expr_loc in
462
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
463
    let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in
464
    expr.expr_type <- ty;
465
    ty
466
  | Expr_merge (c,hl) ->
467
    (* merge is not legal in a constant expression *)
468
    check_constant expr.expr_loc const false;
469
    let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in
470
    let expr_c = expr_of_ident c expr.expr_loc in
471
    let typ_l = Type_predef.type_clock typ_in in
472
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
473
    expr.expr_type <- typ_out;
474
    typ_out
475
  in 
476
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr Types.print_ty resulting_ty);
477
  resulting_ty
478

    
479
and type_branches env in_main loc const hl =
480
  let typ_in = new_var () in
481
  let typ_out = new_var () in
482
  try
483
    let used_labels =
484
      List.fold_left (fun accu (t, h) ->
485
	unify typ_in (type_const loc (Const_tag t));
486
	type_subtyping_arg env in_main const h typ_out;
487
	if List.mem t accu
488
	then raise (Error (loc, Already_bound t))
489
	else t :: accu) [] hl in
490
    let type_labels = get_enum_type_tags (coretype_type typ_in) in
491
    if List.sort compare used_labels <> List.sort compare type_labels
492
    then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in
493
	 raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
494
    else (typ_in, typ_out)
495
  with Unify (t1, t2) ->
496
    raise (Error (loc, Type_clash (t1,t2)))
497

    
498
(** [type_eq env eq] types equation [eq] in environment [env] *)
499
let type_eq env in_main undefined_vars eq =
500
  (* Check undefined variables, type lhs *)
501
  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
502
  let ty_lhs = type_expr env in_main false expr_lhs in
503
  (* Check multiple variable definitions *)
504
  let define_var id uvars =
505
    try
506
      ignore(IMap.find id uvars);
507
      IMap.remove id uvars
508
    with Not_found ->
509
      raise (Error (eq.eq_loc, Already_defined id))
510
  in
511
  (* check assignment of declared constant, assignment of clock *)
512
  let ty_lhs =
513
    type_of_type_list
514
      (List.map2 (fun ty id ->
515
	if get_static_value ty <> None
516
	then raise (Error (eq.eq_loc, Assigned_constant id)) else
517
	match get_clock_base_type ty with
518
	| None -> ty
519
	| Some ty -> ty)
520
	 (type_list_of_type ty_lhs) eq.eq_lhs) in
521
  let undefined_vars =
522
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
523
  (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
524
     to a (always non-constant) lhs variable *)
525
  type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
526
  undefined_vars
527

    
528

    
529
(* [type_coreclock env ck id loc] types the type clock declaration [ck]
530
   in environment [env] *)
531
let type_coreclock env ck id loc =
532
  match ck.ck_dec_desc with
533
  | Ckdec_any | Ckdec_pclock (_,_) -> ()
534
  | Ckdec_bool cl ->
535
      let dummy_id_expr = expr_of_ident id loc in
536
      let when_expr =
537
        List.fold_left
538
          (fun expr (x, l) ->
539
                {expr_tag = new_tag ();
540
                 expr_desc= Expr_when (expr,x,l);
541
                 expr_type = new_var ();
542
                 expr_clock = Clocks.new_var true;
543
                 expr_delay = Delay.new_var ();
544
                 expr_loc=loc;
545
		 expr_annot = None})
546
          dummy_id_expr cl
547
      in
548
      ignore (type_expr env false false when_expr)
549

    
550
let rec check_type_declaration loc cty =
551
 match cty with
552
 | Tydec_clock ty
553
 | Tydec_array (_, ty) -> check_type_declaration loc ty
554
 | Tydec_const tname   ->
555
   if not (Hashtbl.mem type_table cty)
556
   then raise (Error (loc, Unbound_type tname));
557
 | _                   -> ()
558

    
559
let type_var_decl vd_env env vdecl =
560
  check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
561
  let eval_const id = Types.get_static_value (Env.lookup_value env id) in
562
  let type_dim d =
563
    begin
564
      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;
565
      Dimension.eval Basic_library.eval_env eval_const d;
566
    end in
567
  let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
568
  let ty_status =
569
    if vdecl.var_dec_const
570
    then Type_predef.type_static (Dimension.mkdim_var ()) ty
571
    else ty in
572
  let new_env = Env.add_value env vdecl.var_id ty_status in
573
  type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
574
  vdecl.var_type <- ty_status;
575
  new_env
576

    
577
let type_var_decl_list vd_env env l =
578
  List.fold_left (type_var_decl vd_env) env l
579

    
580
let type_of_vlist vars =
581
  let tyl = List.map (fun v -> v.var_type) vars in
582
  type_of_type_list tyl
583

    
584
let add_vdecl vd_env vdecl =
585
 if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
586
 then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
587
 else vdecl::vd_env
588

    
589
let check_vd_env vd_env =
590
  ignore (List.fold_left add_vdecl [] vd_env)
591

    
592
(** [type_node env nd loc] types node [nd] in environment env. The
593
    location is used for error reports. *)
594
let type_node env nd loc =
595
  let is_main = nd.node_id = !Options.main_node in
596
  let vd_env_ol = nd.node_outputs@nd.node_locals in
597
  let vd_env =  nd.node_inputs@vd_env_ol in
598
  check_vd_env vd_env;
599
  let init_env = env in
600
  let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
601
  let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
602
  let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
603
  let new_env = Env.overwrite env delta_env in
604
  let undefined_vars_init =
605
    List.fold_left
606
      (fun uvs v -> IMap.add v.var_id () uvs)
607
      IMap.empty vd_env_ol in
608
  let undefined_vars =
609
    List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs
610
  in
611
  (* Typing asserts *)
612
  List.iter (fun assert_ ->
613
    let assert_expr =  assert_.assert_expr in
614
    type_subtyping_arg (new_env, vd_env) is_main false assert_expr Type_predef.type_bool
615
  )  nd.node_asserts;
616
  
617
  (* check that table is empty *)
618
  if (not (IMap.is_empty undefined_vars)) then
619
    raise (Error (loc, Undefined_var undefined_vars));
620
  let ty_ins = type_of_vlist nd.node_inputs in
621
  let ty_outs = type_of_vlist nd.node_outputs in
622
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
623
  generalize ty_node;
624
  (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
625
  nd.node_type <- ty_node;
626
  Env.add_value env nd.node_id ty_node
627

    
628
let type_imported_node env nd loc =
629
  let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
630
  let vd_env = nd.nodei_inputs@nd.nodei_outputs in
631
  check_vd_env vd_env;
632
  ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
633
  let ty_ins = type_of_vlist nd.nodei_inputs in
634
  let ty_outs = type_of_vlist nd.nodei_outputs in
635
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
636
  generalize ty_node;
637
(*
638
  if (is_polymorphic ty_node) then
639
    raise (Error (loc, Poly_imported_node nd.nodei_id));
640
*)
641
  let new_env = Env.add_value env nd.nodei_id ty_node in
642
  nd.nodei_type <- ty_node;
643
  new_env
644

    
645
let type_top_consts env clist =
646
  List.fold_left (fun env cdecl ->
647
    let ty = type_const cdecl.const_loc cdecl.const_value in
648
    let d =
649
      if is_dimension_type ty
650
      then dimension_of_const cdecl.const_loc cdecl.const_value
651
      else Dimension.mkdim_var () in
652
    let ty = Type_predef.type_static d ty in
653
    let new_env = Env.add_value env cdecl.const_id ty in
654
    cdecl.const_type <- ty;
655
    new_env) env clist
656

    
657
let type_top_decl env decl =
658
  match decl.top_decl_desc with
659
  | Node nd -> (
660
      try
661
	type_node env nd decl.top_decl_loc
662
      with Error (loc, err) as exc -> (
663
	if !Options.global_inline then
664
	  Format.eprintf "Type error: failing node@.%a@.@?"
665
	    Printers.pp_node nd
666
	;
667
	raise exc)
668
  )
669
  | ImportedNode nd ->
670
      type_imported_node env nd decl.top_decl_loc
671
  | Consts clist ->
672
      type_top_consts env clist
673
  | Type _
674
  | Open _  -> env
675

    
676
let type_prog env decls =
677
try
678
  List.fold_left type_top_decl env decls
679
with Failure _ as exc -> raise exc
680

    
681
(* Once the Lustre program is fully typed,
682
   we must get back to the original description of dimensions,
683
   with constant parameters, instead of unifiable internal variables. *)
684

    
685
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types,
686
   i.e. replacing unifiable second_order variables with the original static parameters.
687
   Once restored in this formulation, dimensions may be meaningfully printed.
688
*)
689
let uneval_vdecl_generics vdecl =
690
 if vdecl.var_dec_const
691
 then
692
   match get_static_value vdecl.var_type with
693
   | None   -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)
694
   | Some d -> Dimension.uneval vdecl.var_id d
695

    
696
let uneval_node_generics vdecls =
697
  List.iter uneval_vdecl_generics vdecls
698

    
699
let uneval_top_generics decl =
700
  match decl.top_decl_desc with
701
  | Node nd ->
702
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
703
  | ImportedNode nd ->
704
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
705
  | Consts _
706
  | Type _
707
  | Open _  -> ()
708

    
709
let uneval_prog_generics prog =
710
 List.iter uneval_top_generics prog
711

    
712
let rec get_imported_node decls id =
713
  match decls with
714
  | [] -> assert false
715
  | decl::q ->
716
     (match decl.top_decl_desc with
717
      | ImportedNode nd when id = nd.nodei_id -> decl
718
      | _ -> get_imported_node q id)
719

    
720
let check_env_compat header declared computed = 
721
  uneval_prog_generics header;
722
  Env.iter declared (fun k decl_type_k -> 
723
    let computed_t = instantiate (ref []) (ref []) 
724
				 (try Env.lookup_value computed k
725
				  with Not_found ->
726
				    let loc = (get_imported_node header k).top_decl_loc in 
727
				    raise (Error (loc, Declared_but_undefined k))) in
728
    (*Types.print_ty Format.std_formatter decl_type_k;
729
    Types.print_ty Format.std_formatter computed_t;*)
730
    try_unify ~sub:true ~semi:true decl_type_k computed_t Location.dummy_loc
731
		    )
732
let check_typedef_top decl =
733
  match decl.top_decl_desc with
734
  | Type ty ->
735
Format.eprintf "check_typedef %a %a@." Printers.pp_var_type_dec_desc ty.ty_def_desc Printers.pp_var_type_dec_desc (Hashtbl.find type_table (Tydec_const ty.ty_def_id));
736
    if coretype_equal ty.ty_def_desc (Hashtbl.find type_table (Tydec_const ty.ty_def_id)) then ()
737
    else raise (Error (decl.top_decl_loc, Type_mismatch ty.ty_def_id))
738
  | _  -> ()
739

    
740
let check_typedef_compat header =
741
  List.iter check_typedef_top header
742

    
743
(* Local Variables: *)
744
(* compile-command:"make -C .." *)
745
(* End: *)