Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ fc886259

History | View | Annotate | Download (29.3 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_coretype_definition tname =
134
  try
135
    let top = Hashtbl.find type_table (Tydec_const tname) in
136
    match top.top_decl_desc with
137
    | TypeDef tdef -> tdef.tydef_desc
138
    | _ -> assert false
139
  with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
140

    
141
let get_type_definition tname =
142
    type_coretype (fun d -> ()) (get_coretype_definition tname)
143

    
144
(* Equality on ground types only *)
145
(* Should be used between local variables which must have a ground type *)
146
let rec eq_ground t1 t2 =
147
  let t1 = repr t1 in
148
  let t2 = repr t2 in
149
  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
let rec type_struct_const_field loc (label, c) =
248
  if Hashtbl.mem field_table label
249
  then let tydef = Hashtbl.find field_table label in
250
       let tydec = (typedef_of_top tydef).tydef_desc in 
251
       let tydec_struct = get_struct_type_fields tydec in
252
       let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
253
       begin
254
	 try_unify ty_label (type_const loc c) loc;
255
	 type_coretype (fun d -> ()) tydec
256
       end
257
  else raise (Error (loc, Unbound_value ("struct field " ^ label)))
258

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

    
299
(* The following typing functions take as parameter an environment [env]
300
   and whether the element being typed is expected to be constant [const]. 
301
   [env] is a pair composed of:
302
  - a map from ident to type, associating to each ident, i.e. 
303
    variables, constants and (imported) nodes, its type including whether
304
    it is constant or not. This latter information helps in checking constant 
305
    propagation policy in Lustre.
306
  - a vdecl list, in order to modify types of declared variables that are
307
    later discovered to be clocks during the typing process.
308
*)
309
let check_constant loc const_expected const_real =
310
  if const_expected && not const_real
311
  then raise (Error (loc, Not_a_constant))
312

    
313
let rec type_add_const env const arg targ =
314
  if const
315
  then let d =
316
	 if is_dimension_type targ
317
	 then dimension_of_expr arg
318
	 else Dimension.mkdim_var () in
319
       let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
320
       Dimension.eval Basic_library.eval_env eval_const d;
321
       let real_static_type = Type_predef.type_static d (Types.dynamic_type targ) in
322
       (match Types.get_static_value targ with
323
       | None    -> ()
324
       | Some d' -> try_unify targ real_static_type arg.expr_loc);
325
       real_static_type
326
  else targ
327

    
328
(* emulates a subtyping relation between types t and (d : t),
329
   used during node applications and assignments *)
330
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
331
  let loc = real_arg.expr_loc in
332
  let const = const || (Types.get_static_value formal_type <> None) in
333
  let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in
334
  (*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;*)
335
  try_unify ~sub:sub formal_type real_type loc
336

    
337
and type_ident env in_main loc const id =
338
  type_expr env in_main const (expr_of_ident id loc)
339

    
340
(* typing an application implies:
341
   - checking that const formal parameters match real const (maybe symbolic) arguments
342
   - checking type adequation between formal and real arguments
343
   An application may embed an homomorphic/internal function, in which case we need to split
344
   it in many calls
345
*)
346
and type_appl env in_main loc const f args =
347
  let targs = List.map (type_expr env in_main const) args in
348
  if Basic_library.is_internal_fun f && List.exists is_tuple_type targs
349
  then
350
    try
351
      let targs = Utils.transpose_list (List.map type_list_of_type targs) in
352
      Types.type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)
353
    with
354
      Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l')))
355
  else
356
    type_dependent_call env in_main loc const f (List.combine args targs)
357

    
358
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)
359
and type_dependent_call env in_main loc const f targs =
360
  let tins, touts = new_var (), new_var () in
361
  let tfun = Type_predef.type_arrow tins touts in
362
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
363
  let tins = type_list_of_type tins in
364
  if List.length targs <> List.length tins then
365
    raise (Error (loc, WrongArity (List.length tins, List.length targs)))
366
  else
367
    begin
368
      List.iter2 (fun (a,t) ti ->
369
	let t' = type_add_const env (const || Types.get_static_value ti <> None) a t
370
	in try_unify ~sub:true ti t' a.expr_loc) targs tins;
371
      touts
372
    end
373

    
374
(* type a simple call without dependent types 
375
   but possible homomorphic extension.
376
   [targs] is here a list of arguments' types. *)
377
and type_simple_call env in_main loc const f targs =
378
  let tins, touts = new_var (), new_var () in
379
  let tfun = Type_predef.type_arrow tins touts in
380
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
381
  (*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*)
382
  try_unify ~sub:true tins (type_of_type_list targs) loc;
383
  touts
384

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

    
488
and type_branches env in_main loc const hl =
489
  let typ_in = new_var () in
490
  let typ_out = new_var () in
491
  try
492
    let used_labels =
493
      List.fold_left (fun accu (t, h) ->
494
	unify typ_in (type_const loc (Const_tag t));
495
	type_subtyping_arg env in_main const h typ_out;
496
	if List.mem t accu
497
	then raise (Error (loc, Already_bound t))
498
	else t :: accu) [] hl in
499
    let type_labels = get_enum_type_tags (coretype_type typ_in) in
500
    if List.sort compare used_labels <> List.sort compare type_labels
501
    then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in
502
	 raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
503
    else (typ_in, typ_out)
504
  with Unify (t1, t2) ->
505
    raise (Error (loc, Type_clash (t1,t2)))
506

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

    
537

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

    
559
let rec check_type_declaration loc cty =
560
 match cty with
561
 | Tydec_clock ty
562
 | Tydec_array (_, ty) -> check_type_declaration loc ty
563
 | Tydec_const tname   ->
564
   if not (Hashtbl.mem type_table cty)
565
   then raise (Error (loc, Unbound_type tname));
566
 | _                   -> ()
567

    
568
let type_var_decl vd_env env vdecl =
569
(*Format.eprintf "Typing.type_var_decl START %a@." Printers.pp_var vdecl;*)
570
  check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
571
  let eval_const id = Types.get_static_value (Env.lookup_value env id) in
572
  let type_dim d =
573
    begin
574
      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;
575
      Dimension.eval Basic_library.eval_env eval_const d;
576
    end in
577
  let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
578
  let ty_status =
579
    if vdecl.var_dec_const
580
    then Type_predef.type_static (Dimension.mkdim_var ()) ty
581
    else ty in
582
  let new_env = Env.add_value env vdecl.var_id ty_status in
583
  type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
584
  vdecl.var_type <- ty_status;
585
(*Format.eprintf "END@.";*)
586
  new_env
587

    
588
let type_var_decl_list vd_env env l =
589
  List.fold_left (type_var_decl vd_env) env l
590

    
591
let type_of_vlist vars =
592
  let tyl = List.map (fun v -> v.var_type) vars in
593
  type_of_type_list tyl
594

    
595
let add_vdecl vd_env vdecl =
596
 if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
597
 then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
598
 else vdecl::vd_env
599

    
600
let check_vd_env vd_env =
601
  ignore (List.fold_left add_vdecl [] vd_env)
602

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

    
639
let type_imported_node env nd loc =
640
  let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
641
  let vd_env = nd.nodei_inputs@nd.nodei_outputs in
642
  check_vd_env vd_env;
643
  ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
644
  let ty_ins = type_of_vlist nd.nodei_inputs in
645
  let ty_outs = type_of_vlist nd.nodei_outputs in
646
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
647
  generalize ty_node;
648
(*
649
  if (is_polymorphic ty_node) then
650
    raise (Error (loc, Poly_imported_node nd.nodei_id));
651
*)
652
  let new_env = Env.add_value env nd.nodei_id ty_node in
653
  nd.nodei_type <- ty_node;
654
  new_env
655

    
656
let type_top_const env cdecl =
657
  let ty = type_const cdecl.const_loc cdecl.const_value in
658
  let d =
659
    if is_dimension_type ty
660
    then dimension_of_const cdecl.const_loc cdecl.const_value
661
    else Dimension.mkdim_var () in
662
  let ty = Type_predef.type_static d ty in
663
  let new_env = Env.add_value env cdecl.const_id ty in
664
  cdecl.const_type <- ty;
665
  new_env
666

    
667
let type_top_consts env clist =
668
  List.fold_left type_top_const env clist
669

    
670
let rec type_top_decl env decl =
671
  match decl.top_decl_desc with
672
  | Node nd -> (
673
      try
674
	type_node env nd decl.top_decl_loc
675
      with Error (loc, err) as exc -> (
676
	if !Options.global_inline then
677
	  Format.eprintf "Type error: failing node@.%a@.@?"
678
	    Printers.pp_node nd
679
	;
680
	raise exc)
681
  )
682
  | ImportedNode nd ->
683
      type_imported_node env nd decl.top_decl_loc
684
  | Const c ->
685
      type_top_const env c
686
  | TypeDef _ -> List.fold_left type_top_decl env (consts_of_enum_type decl)
687
  | Open _  -> env
688

    
689
let type_prog env decls =
690
try
691
  List.fold_left type_top_decl env decls
692
with Failure _ as exc -> raise exc
693

    
694
(* Once the Lustre program is fully typed,
695
   we must get back to the original description of dimensions,
696
   with constant parameters, instead of unifiable internal variables. *)
697

    
698
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types,
699
   i.e. replacing unifiable second_order variables with the original static parameters.
700
   Once restored in this formulation, dimensions may be meaningfully printed.
701
*)
702
let uneval_vdecl_generics vdecl =
703
 if vdecl.var_dec_const
704
 then
705
   match get_static_value vdecl.var_type with
706
   | None   -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)
707
   | Some d -> Dimension.uneval vdecl.var_id d
708

    
709
let uneval_node_generics vdecls =
710
  List.iter uneval_vdecl_generics vdecls
711

    
712
let uneval_top_generics decl =
713
  match decl.top_decl_desc with
714
  | Node nd ->
715
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
716
  | ImportedNode nd ->
717
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
718
  | Const _
719
  | TypeDef _
720
  | Open _  -> ()
721

    
722
let uneval_prog_generics prog =
723
 List.iter uneval_top_generics prog
724

    
725
let rec get_imported_symbol decls id =
726
  match decls with
727
  | [] -> assert false
728
  | decl::q ->
729
     (match decl.top_decl_desc with
730
      | ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf -> decl
731
      | Const c when id = c.const_id && decl.top_decl_itf -> decl
732
      | TypeDef _ -> get_imported_symbol (consts_of_enum_type decl @ q) id
733
      | _ -> get_imported_symbol q id)
734

    
735
let check_env_compat header declared computed = 
736
  uneval_prog_generics header;
737
  Env.iter declared (fun k decl_type_k ->
738
    let loc = (get_imported_symbol header k).top_decl_loc in 
739
    let computed_t =
740
      instantiate (ref []) (ref []) 
741
	(try Env.lookup_value computed k
742
	 with Not_found -> raise (Error (loc, Declared_but_undefined k))) in
743
    (*Types.print_ty Format.std_formatter decl_type_k;
744
      Types.print_ty Format.std_formatter computed_t;*)
745
    try_unify ~sub:true ~semi:true decl_type_k computed_t loc
746
  )
747

    
748
let check_typedef_top decl =
749
(*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*)
750
(*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*)
751
(*Format.eprintf "%a" Corelang.print_type_table ();*)
752
  match decl.top_decl_desc with
753
  | TypeDef ty ->
754
     let owner = decl.top_decl_owner in
755
     let itf = decl.top_decl_itf in
756
     let decl' =
757
       try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id)
758
       with Not_found -> raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in
759
     let owner' = decl'.top_decl_owner in
760
(*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*)
761
     let itf' = decl'.top_decl_itf in
762
     (match decl'.top_decl_desc with
763
     | Const _ | Node _ | ImportedNode _ -> assert false
764
     | TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') -> ()
765
     | _ -> raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id)))
766
  | _  -> ()
767

    
768
let check_typedef_compat header =
769
  List.iter check_typedef_top header
770

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