Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ a38c681e

History | View | Annotate | Download (27.8 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
let rec type_struct_const_field loc (label, c) =
248
  if Hashtbl.mem field_table label
249
  then let tydec = Hashtbl.find field_table label in
250
       let tydec_struct = get_struct_type_fields tydec in
251
       let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
252
       begin
253
	 try_unify ty_label (type_const loc c) loc;
254
	 type_coretype (fun d -> ()) tydec
255
       end
256
  else raise (Error (loc, Unbound_value ("struct field " ^ label)))
257

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

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

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

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

    
330
and type_ident env in_main loc const id =
331
  type_expr env in_main const (expr_of_ident id loc)
332

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

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

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

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

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

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

    
534

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

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

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

    
583
let type_var_decl_list vd_env env l =
584
  List.fold_left (type_var_decl vd_env) env l
585

    
586
let type_of_vlist vars =
587
  let tyl = List.map (fun v -> v.var_type) vars in
588
  type_of_type_list tyl
589

    
590
let add_vdecl vd_env vdecl =
591
 if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
592
 then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
593
 else vdecl::vd_env
594

    
595
let check_vd_env vd_env =
596
  ignore (List.fold_left add_vdecl [] vd_env)
597

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

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

    
651
let type_top_consts env clist =
652
  List.fold_left (fun env cdecl ->
653
    let ty = type_const cdecl.const_loc cdecl.const_value in
654
    let d =
655
      if is_dimension_type ty
656
      then dimension_of_const cdecl.const_loc cdecl.const_value
657
      else Dimension.mkdim_var () in
658
    let ty = Type_predef.type_static d ty in
659
    let new_env = Env.add_value env cdecl.const_id ty in
660
    cdecl.const_type <- ty;
661
    new_env) env clist
662

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

    
681
let type_prog env decls =
682
try
683
  List.fold_left type_top_decl env decls
684
with Failure _ as exc -> raise exc
685

    
686
(* Once the Lustre program is fully typed,
687
   we must get back to the original description of dimensions,
688
   with constant parameters, instead of unifiable internal variables. *)
689

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

    
701
let uneval_node_generics vdecls =
702
  List.iter uneval_vdecl_generics vdecls
703

    
704
let uneval_top_generics decl =
705
  match decl.top_decl_desc with
706
  | Node nd ->
707
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
708
  | ImportedNode nd ->
709
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
710
  | Consts clist -> ()
711
  | Open _  -> ()
712

    
713
let uneval_prog_generics prog =
714
 List.iter uneval_top_generics prog
715

    
716
let rec get_imported_node decls id =
717
  match decls with
718
  | [] -> assert false
719
  | decl::q ->
720
     (match decl.top_decl_desc with
721
      | ImportedNode nd when id = nd.nodei_id -> decl
722
      | _ -> get_imported_node q id)
723

    
724
let check_env_compat header declared computed = 
725
  uneval_prog_generics header;
726
  Env.iter declared (fun k decl_type_k -> 
727
    let computed_t = instantiate (ref []) (ref []) 
728
				 (try Env.lookup_value computed k
729
				  with Not_found ->
730
				    let loc = (get_imported_node header k).top_decl_loc in 
731
				    raise (Error (loc, Declared_but_undefined k))) in
732
    (*Types.print_ty Format.std_formatter decl_type_k;
733
    Types.print_ty Format.std_formatter computed_t;*)
734
    try_unify ~sub:true ~semi:true decl_type_k computed_t Location.dummy_loc
735
		    )
736

    
737
(* Local Variables: *)
738
(* compile-command:"make -C .." *)
739
(* End: *)