Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ 719f9992

History | View | Annotate | Download (29.6 KB)

1
(* ----------------------------------------------------------------------------
2
 * SchedMCore - A MultiCore Scheduling Framework
3
 * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
4
 *
5
 * This file is part of Prelude
6
 *
7
 * Prelude is free software; you can redistribute it and/or
8
 * modify it under the terms of the GNU Lesser General Public License
9
 * as published by the Free Software Foundation ; either version 2 of
10
 * the License, or (at your option) any later version.
11
 *
12
 * Prelude is distributed in the hope that it will be useful, but
13
 * WITHOUT ANY WARRANTY ; without even the implied warranty of
14
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15
 * Lesser General Public License for more details.
16
 *
17
 * You should have received a copy of the GNU Lesser General Public
18
 * License along with this program ; if not, write to the Free Software
19
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
20
 * USA
21
 *---------------------------------------------------------------------------- *)
22

    
23
(** Main typing module. Classic inference algorithm with destructive
24
    unification. *)
25

    
26
let debug fmt args = () (* Format.eprintf "%a"  *)
27
(* Though it shares similarities with the clock calculus module, no code
28
    is shared.  Simple environments, very limited identifier scoping, no
29
    identifier redefinition allowed. *)
30

    
31
open Utils
32
(* Yes, opening both modules is dirty as some type names will be
33
   overwritten, yet this makes notations far lighter.*)
34
open LustreSpec
35
open Corelang
36
open Types
37
open Format
38

    
39
let pp_typing_env fmt env =
40
  Env.pp_env print_ty fmt env
41

    
42
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in
43
    type [ty]. False otherwise. *)
44
let rec occurs tvar ty =
45
  let ty = repr ty in
46
  match ty.tdesc with
47
  | Tvar -> ty=tvar
48
  | Tarrow (t1, t2) ->
49
      (occurs tvar t1) || (occurs tvar t2)
50
  | Ttuple tl ->
51
     List.exists (occurs tvar) tl
52
  | Tstruct fl ->
53
     List.exists (fun (f, t) -> occurs tvar t) fl
54
  | Tarray (_, t)
55
  | Tstatic (_, t)
56
  | Tclock t
57
  | Tlink t -> occurs tvar t
58
  | Tenum _ | Tconst _ | Tunivar | Tint | Treal | Tbool | Trat -> false
59

    
60
(** Promote monomorphic type variables to polymorphic type variables. *)
61
(* Generalize by side-effects *)
62
let rec generalize ty =
63
  match ty.tdesc with
64
  | Tvar ->
65
      (* No scopes, always generalize *)
66
      ty.tdesc <- Tunivar
67
  | Tarrow (t1,t2) ->
68
      generalize t1; generalize t2
69
  | Ttuple tl ->
70
     List.iter generalize tl
71
  | Tstruct fl ->
72
     List.iter (fun (f, t) -> generalize t) fl
73
  | Tstatic (d, t)
74
  | Tarray (d, t) -> Dimension.generalize d; generalize t
75
  | Tclock t
76
  | Tlink t ->
77
      generalize t
78
  | Tenum _ | Tconst _ | Tunivar | Tint | Treal | Tbool | Trat -> ()
79

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

    
109
(* [type_coretype cty] types the type declaration [cty] *)
110
let rec type_coretype type_dim cty =
111
  match (*get_repr_type*) cty with
112
  | Tydec_any -> new_var ()
113
  | Tydec_int -> Type_predef.type_int
114
  | Tydec_real -> Type_predef.type_real
115
  | Tydec_float -> Type_predef.type_real
116
  | Tydec_bool -> Type_predef.type_bool
117
  | Tydec_clock ty -> Type_predef.type_clock (type_coretype type_dim ty)
118
  | Tydec_const c -> Type_predef.type_const c
119
  | Tydec_enum tl -> Type_predef.type_enum tl
120
  | Tydec_struct fl -> Type_predef.type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl)
121
  | Tydec_array (d, ty) ->
122
    begin
123
      type_dim d;
124
      Type_predef.type_array d (type_coretype type_dim ty)
125
    end
126

    
127
(* [coretype_type] is the reciprocal of [type_typecore] *)
128
let rec coretype_type ty =
129
 match (repr ty).tdesc with
130
 | Tvar           -> Tydec_any
131
 | Tint           -> Tydec_int
132
 | Treal          -> Tydec_real
133
 | Tbool          -> Tydec_bool
134
 | Tconst c       -> Tydec_const c
135
 | Tclock t       -> Tydec_clock (coretype_type t)
136
 | Tenum tl       -> Tydec_enum tl
137
 | Tstruct fl     -> Tydec_struct (List.map (fun (f, t) -> (f, coretype_type t)) fl)
138
 | Tarray (d, t)  -> Tydec_array (d, coretype_type t)
139
 | Tstatic (_, t) -> coretype_type t
140
 | _         -> assert false
141

    
142
let get_type_definition tname =
143
  try
144
    type_coretype (fun d -> ()) (Hashtbl.find type_table (Tydec_const tname))
145
  with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
146

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

    
168
(** [unify t1 t2] unifies types [t1] and [t2]. Raises [Unify
169
    (t1,t2)] if the types are not unifiable.*)
170
(* Standard destructive unification *)
171
let rec unify t1 t2 =
172
  let t1 = repr t1 in
173
  let t2 = repr t2 in
174
  if t1=t2 then
175
    ()
176
  else
177
    (* No type abbreviations resolution for now *)
178
    match t1.tdesc,t2.tdesc with
179
      (* This case is not mandory but will keep "older" types *)
180
    | Tvar, Tvar ->
181
        if t1.tid < t2.tid then
182
          t2.tdesc <- Tlink t1
183
        else
184
          t1.tdesc <- Tlink t2
185
    | (Tvar, _) when (not (occurs t1 t2)) ->
186
        t1.tdesc <- Tlink t2
187
    | (_,Tvar) when (not (occurs t2 t1)) ->
188
        t2.tdesc <- Tlink t1
189
    | Tarrow (t1,t2), Tarrow (t1',t2') ->
190
      begin
191
        unify t1 t1';
192
	unify t2 t2'
193
      end
194
    | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
195
      List.iter2 unify tl tl'
196
    | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
197
      List.iter2 (fun (_, t) (_, t') -> unify t t') fl fl'
198
    | Tclock _, Tstatic _
199
    | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
200
    | Tclock t1', _ -> unify t1' t2
201
    | _, Tclock t2' -> unify t1 t2'
202
    | Tint, Tint | Tbool, Tbool | Trat, Trat
203
    | Tunivar, _ | _, Tunivar -> ()
204
    | (Tconst t, _) ->
205
      let def_t = get_type_definition t in
206
      unify def_t t2
207
    | (_, Tconst t)  ->
208
      let def_t = get_type_definition t in
209
      unify t1 def_t
210
    | Tenum tl, Tenum tl' when tl == tl' -> ()
211
    | Tstatic (e1, t1'), Tstatic (e2, t2')
212
    | Tarray (e1, t1'), Tarray (e2, t2') ->
213
      begin
214
	unify t1' t2';
215
	Dimension.eval Basic_library.eval_env (fun c -> None) e1;
216
	Dimension.eval Basic_library.eval_env (fun c -> None) e2;
217
	Dimension.unify e1 e2;
218
      end
219
    | _,_ -> raise (Unify (t1, t2))
220

    
221
(** [semi_unify t1 t2] checks whether type [t1] is an instance of type [t2]. Raises [Unify
222
    (t1,t2)] if the types are not semi-unifiable.*)
223
(* Standard destructive semi-unification *)
224
let rec semi_unify t1 t2 =
225
  let t1 = repr t1 in
226
  let t2 = repr t2 in
227
  if t1=t2 then
228
    ()
229
  else
230
    (* No type abbreviations resolution for now *)
231
    match t1.tdesc,t2.tdesc with
232
      (* This case is not mandory but will keep "older" types *)
233
    | Tvar, Tvar ->
234
        if t1.tid < t2.tid then
235
          t2.tdesc <- Tlink t1
236
        else
237
          t1.tdesc <- Tlink t2
238
    | (Tvar, _) -> raise (Unify (t1, t2))
239
    | (_,Tvar) when (not (occurs t2 t1)) ->
240
        t2.tdesc <- Tlink t1
241
    | Tarrow (t1,t2), Tarrow (t1',t2') ->
242
      begin
243
        semi_unify t1 t1';
244
	semi_unify t2 t2'
245
      end
246
    | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
247
      List.iter2 semi_unify tl tl'
248
    | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
249
      List.iter2 (fun (_, t) (_, t') -> semi_unify t t') fl fl'
250
    | Tclock _, Tstatic _
251
    | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
252
    | Tclock t1', _ -> semi_unify t1' t2
253
    | _, Tclock t2' -> semi_unify t1 t2'
254
    | Tint, Tint | Tbool, Tbool | Trat, Trat
255
    | Tunivar, _ | _, Tunivar -> ()
256
    | (Tconst t, _) ->
257
      let def_t = get_type_definition t in
258
      semi_unify def_t t2
259
    | (_, Tconst t)  ->
260
      let def_t = get_type_definition t in
261
      semi_unify t1 def_t
262
    | Tenum tl, Tenum tl' when tl == tl' -> ()
263

    
264
    | Tstatic (e1, t1'), Tstatic (e2, t2')
265
    | Tarray (e1, t1'), Tarray (e2, t2') ->
266
      begin
267
	semi_unify t1' t2';
268
	Dimension.eval Basic_library.eval_env (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c)) e1;
269
	Dimension.eval Basic_library.eval_env (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c)) e2;
270
	Dimension.semi_unify e1 e2;
271
      end
272
    | _,_ -> raise (Unify (t1, t2))
273

    
274
(* Expected type ty1, got type ty2 *)
275
let try_unify ty1 ty2 loc =
276
  try
277
    unify ty1 ty2
278
  with
279
  | Unify _ ->
280
    raise (Error (loc, Type_clash (ty1,ty2)))
281
  | Dimension.Unify _ ->
282
    raise (Error (loc, Type_clash (ty1,ty2)))
283

    
284
let try_semi_unify ty1 ty2 loc =
285
  try
286
    semi_unify ty1 ty2
287
  with
288
  | Unify _ ->
289
    raise (Error (loc, Type_clash (ty1,ty2)))
290
  | Dimension.Unify _ ->
291
    raise (Error (loc, Type_clash (ty1,ty2)))
292

    
293
(* ty1 is a subtype of ty2 *)
294
let rec sub_unify sub ty1 ty2 =
295
  match (repr ty1).tdesc, (repr ty2).tdesc with
296
  | Ttuple tl1         , Ttuple tl2         ->
297
    if List.length tl1 <> List.length tl2
298
    then raise (Unify (ty1, ty2))
299
    else List.iter2 (sub_unify sub) tl1 tl2
300
  | Ttuple [t1]        , _                  -> sub_unify sub t1 ty2
301
  | _                  , Ttuple [t2]        -> sub_unify sub ty1 t2
302
  | Tstruct tl1        , Tstruct tl2        ->
303
    if List.map fst tl1 <> List.map fst tl2
304
    then raise (Unify (ty1, ty2))
305
    else List.iter2 (fun (_, t1) (_, t2) -> sub_unify sub t1 t2) tl1 tl2
306
  | Tclock t1          , Tclock t2          -> sub_unify sub t1 t2
307
  | Tclock t1          , _   when sub       -> sub_unify sub t1 ty2
308
  | Tstatic (d1, t1)   , Tstatic (d2, t2)   ->
309
    begin
310
      sub_unify sub t1 t2;
311
      Dimension.eval Basic_library.eval_env (fun c -> None) d1;
312
      Dimension.eval Basic_library.eval_env (fun c -> None) d2;
313
      Dimension.unify d1 d2
314
    end
315
  | Tstatic (r_d, t1)  , _         when sub -> sub_unify sub t1 ty2
316
  | _                                       -> unify ty1 ty2
317

    
318
let try_sub_unify sub ty1 ty2 loc =
319
  try
320
    sub_unify sub ty1 ty2
321
  with
322
  | Unify _ ->
323
    raise (Error (loc, Type_clash (ty1,ty2)))
324
  | Dimension.Unify _ ->
325
    raise (Error (loc, Type_clash (ty1,ty2)))
326

    
327
let rec type_struct_const_field loc (label, c) =
328
  if Hashtbl.mem field_table label
329
  then let tydec = Hashtbl.find field_table label in
330
       let tydec_struct = get_struct_type_fields tydec in
331
       let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
332
       begin
333
	 try_unify ty_label (type_const loc c) loc;
334
	 type_coretype (fun d -> ()) tydec
335
       end
336
  else raise (Error (loc, Unbound_value ("struct field " ^ label)))
337

    
338
and type_const loc c = 
339
  match c with
340
  | Const_int _     -> Type_predef.type_int
341
  | Const_real _    -> Type_predef.type_real
342
  | Const_float _   -> Type_predef.type_real
343
  | Const_array ca  -> let d = Dimension.mkdim_int loc (List.length ca) in
344
		      let ty = new_var () in
345
		      List.iter (fun e -> try_unify ty (type_const loc e) loc) ca;
346
		      Type_predef.type_array d ty
347
  | Const_tag t     ->
348
    if Hashtbl.mem tag_table t
349
    then type_coretype (fun d -> ()) (Hashtbl.find tag_table t)
350
    else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
351
  | Const_struct fl ->
352
    let ty_struct = new_var () in
353
    begin
354
      let used =
355
	List.fold_left
356
	  (fun acc (l, c) ->
357
	    if List.mem l acc
358
	    then raise (Error (loc, Already_bound ("struct field " ^ l)))
359
	    else try_unify ty_struct (type_struct_const_field loc (l, c)) loc; l::acc)
360
	  [] fl in
361
      try
362
	let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in
363
(*	List.iter (fun l -> Format.eprintf "total: %s@." l) total;
364
	List.iter (fun l -> Format.eprintf "used: %s@." l) used; *)
365
	let undef = List.find (fun l -> not (List.mem l used)) total
366
	in raise (Error (loc, Unbound_value ("struct field " ^ undef)))
367
      with Not_found -> 
368
	ty_struct
369
    end
370

    
371
(* The following typing functions take as parameter an environment [env]
372
   and whether the element being typed is expected to be constant [const]. 
373
   [env] is a pair composed of:
374
  - a map from ident to type, associating to each ident, i.e. 
375
    variables, constants and (imported) nodes, its type including whether
376
    it is constant or not. This latter information helps in checking constant 
377
    propagation policy in Lustre.
378
  - a vdecl list, in order to modify types of declared variables that are
379
    later discovered to be clocks during the typing process.
380
*)
381
let check_constant loc const_expected const_real =
382
  if const_expected && not const_real
383
  then raise (Error (loc, Not_a_constant))
384

    
385
let rec type_standard_args env in_main const expr_list =
386
  let ty_list = List.map (fun e -> dynamic_type (type_expr env in_main const e)) expr_list in
387
  let ty_res = new_var () in
388
  List.iter2 (fun e ty -> try_unify ty_res ty e.expr_loc) expr_list ty_list;
389
  ty_res
390

    
391
(* emulates a subtyping relation between types t and (d : t),
392
   used during node applications and assignments *)
393
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
394
  let loc = real_arg.expr_loc in
395
  let const = const || (Types.get_static_value formal_type <> None) in
396
  let real_type = type_expr env in_main const real_arg in
397
  let real_type =
398
    if const
399
    then let d =
400
	   if is_dimension_type real_type
401
	   then dimension_of_expr real_arg
402
	   else Dimension.mkdim_var () in
403
	 let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
404
	 Dimension.eval Basic_library.eval_env eval_const d;
405
	 let real_static_type = Type_predef.type_static d (Types.dynamic_type real_type) in
406
	 (match Types.get_static_value real_type with
407
	 | None    -> ()
408
	 | Some d' -> try_unify real_type real_static_type loc);
409
	 real_static_type
410
    else real_type in
411
  (*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;*)
412
  try_sub_unify sub real_type formal_type loc
413

    
414
and type_ident env in_main loc const id =
415
  type_expr env in_main const (expr_of_ident id loc)
416

    
417
(* typing an application implies:
418
   - checking that const formal parameters match real const (maybe symbolic) arguments
419
   - checking type adequation between formal and real arguments
420
   An application may embed an homomorphic/internal function, in which case we need to split
421
   it in many calls
422
*)
423
and type_appl env in_main loc const f args =
424
  let args = expr_list_of_expr args in
425
  if Basic_library.is_internal_fun f && List.exists is_tuple_expr args
426
  then
427
    try
428
      let args = Utils.transpose_list (List.map expr_list_of_expr args) in
429
      Types.type_of_type_list (List.map (type_call env in_main loc const f) args)
430
    with
431
      Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l')))
432
  else
433
    type_call env in_main loc const f args
434

    
435
(* type a (single) call. [args] is here a list of arguments. *)
436
and type_call env in_main loc const f args =
437
  let tins, touts = new_var (), new_var () in
438
  let tfun = Type_predef.type_arrow tins touts in
439
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
440
  let tins = type_list_of_type tins in
441
  if List.length args <> List.length tins then
442
    raise (Error (loc, WrongArity (List.length args, List.length tins)))
443
  else
444
    List.iter2 (type_subtyping_arg env in_main const) args tins;
445
  touts
446

    
447
(** [type_expr env in_main expr] types expression [expr] in environment
448
    [env], expecting it to be [const] or not. *)
449
and type_expr env in_main const expr =
450
  let resulting_ty = 
451
  match expr.expr_desc with
452
  | Expr_const c ->
453
    let ty = type_const expr.expr_loc c in
454
    let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in
455
    expr.expr_type <- ty;
456
    ty
457
  | Expr_ident v ->
458
    let tyv =
459
      try
460
        Env.lookup_value (fst env) v
461
      with Not_found ->
462
	Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr;
463
        raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))
464
    in
465
    let ty = instantiate (ref []) (ref []) tyv in
466
    let ty' =
467
      if const
468
      then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ())
469
      else new_var () in
470
    try_unify ty ty' expr.expr_loc;
471
    expr.expr_type <- ty;
472
    ty 
473
  | Expr_array elist ->
474
    let ty_elt = type_standard_args env in_main const elist in
475
    let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
476
    let ty = Type_predef.type_array d ty_elt in
477
    expr.expr_type <- ty;
478
    ty
479
  | Expr_access (e1, d) ->
480
    type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
481
    let ty_elt = new_var () in
482
    let d = Dimension.mkdim_var () in
483
    type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt);
484
    expr.expr_type <- ty_elt;
485
    ty_elt
486
  | Expr_power (e1, d) ->
487
    let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
488
    type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
489
    Dimension.eval Basic_library.eval_env eval_const d;
490
    let ty_elt = type_standard_args env in_main const [e1] in
491
    let ty = Type_predef.type_array d ty_elt in
492
    expr.expr_type <- ty;
493
    ty
494
  | Expr_tuple elist ->
495
    let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in
496
    expr.expr_type <- ty;
497
    ty
498
  | Expr_ite (c, t, e) ->
499
    type_subtyping_arg env in_main const c Type_predef.type_bool;
500
    let ty = type_standard_args env in_main const [t; e] in
501
    expr.expr_type <- ty;
502
    ty
503
  | Expr_appl (id, args, r) ->
504
    (* application of non internal function is not legal in a constant
505
       expression *)
506
    (match r with
507
    | None        -> ()
508
    | Some (x, l) -> 
509
      check_constant expr.expr_loc const false;
510
      let expr_x = expr_of_ident x expr.expr_loc in	
511
      let typ_l = 
512
	Type_predef.type_clock 
513
	  (type_const expr.expr_loc (Const_tag l)) in
514
      type_subtyping_arg env in_main ~sub:false const expr_x typ_l);
515
    let touts = type_appl env in_main expr.expr_loc const id args in
516
    expr.expr_type <- touts;
517
    touts
518
  | Expr_fby (e1,e2)
519
  | Expr_arrow (e1,e2) ->
520
    (* fby/arrow is not legal in a constant expression *)
521
    check_constant expr.expr_loc const false;
522
    let ty = type_standard_args env in_main const [e1; e2] in
523
    expr.expr_type <- ty;
524
    ty
525
  | Expr_pre e ->
526
    (* pre is not legal in a constant expression *)
527
    check_constant expr.expr_loc const false;
528
    let ty = type_standard_args env in_main const [e] in
529
    expr.expr_type <- ty;
530
    ty
531
  | Expr_when (e1,c,l) ->
532
    (* when is not legal in a constant expression *)
533
    check_constant expr.expr_loc const false;
534
    let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in
535
    let expr_c = expr_of_ident c expr.expr_loc in
536
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
537
    update_clock env in_main c expr.expr_loc typ_l;
538
    let ty = type_standard_args env in_main const [e1] in
539
    expr.expr_type <- ty;
540
    ty
541
  | Expr_merge (c,hl) ->
542
    (* merge is not legal in a constant expression *)
543
    check_constant expr.expr_loc const false;
544
    let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in
545
    let expr_c = expr_of_ident c expr.expr_loc in
546
    let typ_l = Type_predef.type_clock typ_in in
547
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
548
    update_clock env in_main c expr.expr_loc typ_l;
549
    expr.expr_type <- typ_out;
550
    typ_out
551
  | Expr_uclock (e,k) | Expr_dclock (e,k) ->
552
      let ty = type_expr env in_main const e in
553
      expr.expr_type <- ty;
554
      ty
555
  | Expr_phclock (e,q) ->
556
      let ty = type_expr env in_main const e in
557
      expr.expr_type <- ty;
558
      ty
559
  in 
560
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr Types.print_ty resulting_ty);
561
  resulting_ty
562

    
563
and type_branches env in_main loc const hl =
564
  let typ_in = new_var () in
565
  let typ_out = new_var () in
566
  try
567
    let used_labels =
568
      List.fold_left (fun accu (t, h) ->
569
	unify typ_in (type_const loc (Const_tag t));
570
	type_subtyping_arg env in_main const h typ_out;
571
	if List.mem t accu
572
	then raise (Error (loc, Already_bound t))
573
	else t :: accu) [] hl in
574
    let type_labels = get_enum_type_tags (coretype_type typ_in) in
575
    if List.sort compare used_labels <> List.sort compare type_labels
576
    then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in
577
	 raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
578
    else (typ_in, typ_out)
579
  with Unify (t1, t2) ->
580
    raise (Error (loc, Type_clash (t1,t2)))
581

    
582
and update_clock env in_main id loc typ =
583
 (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*)
584
 try
585
   let vdecl = List.find (fun v -> v.var_id = id) (snd env)
586
   in vdecl.var_type <- typ
587
 with
588
   Not_found ->
589
   raise (Error (loc, Unbound_value ("clock " ^ id)))
590

    
591
(** [type_eq env eq] types equation [eq] in environment [env] *)
592
let type_eq env in_main undefined_vars eq =
593
  (* Check undefined variables, type lhs *)
594
  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
595
  let ty_lhs = type_expr env in_main false expr_lhs in
596
  (* Check multiple variable definitions *)
597
  let define_var id uvars =
598
    try
599
      ignore(IMap.find id uvars);
600
      IMap.remove id uvars
601
    with Not_found ->
602
      raise (Error (eq.eq_loc, Already_defined id))
603
  in
604
  let undefined_vars =
605
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
606
  (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
607
     to a (always non-constant) lhs variable *)
608
  type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
609
  undefined_vars
610

    
611

    
612
(* [type_coreclock env ck id loc] types the type clock declaration [ck]
613
   in environment [env] *)
614
let type_coreclock env ck id loc =
615
  match ck.ck_dec_desc with
616
  | Ckdec_any | Ckdec_pclock (_,_) -> ()
617
  | Ckdec_bool cl ->
618
      let dummy_id_expr = expr_of_ident id loc in
619
      let when_expr =
620
        List.fold_left
621
          (fun expr (x, l) ->
622
                {expr_tag = new_tag ();
623
                 expr_desc= Expr_when (expr,x,l);
624
                 expr_type = new_var ();
625
                 expr_clock = Clocks.new_var true;
626
                 expr_delay = Delay.new_var ();
627
                 expr_loc=loc;
628
		 expr_annot = None})
629
          dummy_id_expr cl
630
      in
631
      ignore (type_expr env false false when_expr)
632

    
633
let rec check_type_declaration loc cty =
634
 match cty with
635
 | Tydec_clock ty
636
 | Tydec_array (_, ty) -> check_type_declaration loc ty
637
 | Tydec_const tname   ->
638
   if not (Hashtbl.mem type_table cty)
639
   then raise (Error (loc, Unbound_type tname));
640
 | _                   -> ()
641

    
642
let type_var_decl vd_env env vdecl =
643
  check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
644
  let eval_const id = Types.get_static_value (Env.lookup_value env id) in
645
  let type_dim d =
646
    begin
647
      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;
648
      Dimension.eval Basic_library.eval_env eval_const d;
649
    end in
650
  let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
651
  let ty_status =
652
    if vdecl.var_dec_const
653
    then Type_predef.type_static (Dimension.mkdim_var ()) ty
654
    else ty in
655
  let new_env = Env.add_value env vdecl.var_id ty_status in
656
  type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
657
  vdecl.var_type <- ty_status;
658
  new_env
659

    
660
let type_var_decl_list vd_env env l =
661
  List.fold_left (type_var_decl vd_env) env l
662

    
663
let type_of_vlist vars =
664
  let tyl = List.map (fun v -> v.var_type) vars in
665
  type_of_type_list tyl
666

    
667
let add_vdecl vd_env vdecl =
668
 if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
669
 then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
670
 else vdecl::vd_env
671

    
672
let check_vd_env vd_env =
673
  ignore (List.fold_left add_vdecl [] vd_env)
674

    
675
(** [type_node env nd loc] types node [nd] in environment env. The
676
    location is used for error reports. *)
677
let type_node env nd loc =
678
  let is_main = nd.node_id = !Options.main_node in
679
  let vd_env_ol = nd.node_outputs@nd.node_locals in
680
  let vd_env =  nd.node_inputs@vd_env_ol in
681
  check_vd_env vd_env;
682
  let init_env = env in
683
  let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
684
  let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
685
  let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
686
  let new_env = Env.overwrite env delta_env in
687
  let undefined_vars_init =
688
    List.fold_left
689
      (fun uvs v -> IMap.add v.var_id () uvs)
690
      IMap.empty vd_env_ol in
691
  let undefined_vars =
692
    List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs
693
  in
694
  (* check that table is empty *)
695
  if (not (IMap.is_empty undefined_vars)) then
696
    raise (Error (loc, Undefined_var undefined_vars));
697
  let ty_ins = type_of_vlist nd.node_inputs in
698
  let ty_outs = type_of_vlist nd.node_outputs in
699
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
700
  generalize ty_node;
701
  (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
702
  nd.node_type <- ty_node;
703
  Env.add_value env nd.node_id ty_node
704

    
705
let type_imported_node env nd loc =
706
  let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
707
  let vd_env = nd.nodei_inputs@nd.nodei_outputs in
708
  check_vd_env vd_env;
709
  ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
710
  let ty_ins = type_of_vlist nd.nodei_inputs in
711
  let ty_outs = type_of_vlist nd.nodei_outputs in
712
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
713
  generalize ty_node;
714
(*
715
  if (is_polymorphic ty_node) then
716
    raise (Error (loc, Poly_imported_node nd.nodei_id));
717
*)
718
  let new_env = Env.add_value env nd.nodei_id ty_node in
719
  nd.nodei_type <- ty_node;
720
  new_env
721

    
722
let type_top_consts env clist =
723
  List.fold_left (fun env cdecl ->
724
    let ty = type_const cdecl.const_loc cdecl.const_value in
725
    let d =
726
      if is_dimension_type ty
727
      then dimension_of_const cdecl.const_loc cdecl.const_value
728
      else Dimension.mkdim_var () in
729
    let ty = Type_predef.type_static d ty in
730
    let new_env = Env.add_value env cdecl.const_id ty in
731
    cdecl.const_type <- ty;
732
    new_env) env clist
733

    
734
let type_top_decl env decl =
735
  match decl.top_decl_desc with
736
  | Node nd -> (
737
      try
738
	type_node env nd decl.top_decl_loc
739
      with Error (loc, err) as exc -> (
740
	if !Options.global_inline then
741
	  Format.eprintf "Type error: failing node@.%a@.@?"
742
	    Printers.pp_node nd
743
	;
744
	raise exc)
745
  )
746
  | ImportedNode nd ->
747
      type_imported_node env nd decl.top_decl_loc
748
  | Consts clist ->
749
      type_top_consts env clist
750
  | Open _  -> env
751

    
752
let type_prog env decls =
753
try
754
  List.fold_left type_top_decl env decls
755
with Failure _ as exc -> raise exc
756

    
757
(* Once the Lustre program is fully typed,
758
   we must get back to the original description of dimensions,
759
   with constant parameters, instead of unifiable internal variables. *)
760

    
761
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types,
762
   i.e. replacing unifiable second_order variables with the original static parameters.
763
   Once restored in this formulation, dimensions may be meaningfully printed.
764
*)
765
let uneval_vdecl_generics vdecl =
766
 if vdecl.var_dec_const
767
 then
768
   match get_static_value vdecl.var_type with
769
   | None   -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)
770
   | Some d -> Dimension.uneval vdecl.var_id d
771

    
772
let uneval_node_generics vdecls =
773
  List.iter uneval_vdecl_generics vdecls
774

    
775
let uneval_top_generics decl =
776
  match decl.top_decl_desc with
777
  | Node nd ->
778
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
779
  | ImportedNode nd ->
780
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
781
  | Consts clist -> ()
782
  | Open _  -> ()
783

    
784
let uneval_prog_generics prog =
785
 List.iter uneval_top_generics prog
786

    
787
let rec get_imported_node decls id =
788
  match decls with
789
  | [] -> assert false
790
  | decl::q ->
791
     (match decl.top_decl_desc with
792
      | ImportedNode nd when id = nd.nodei_id -> decl
793
      | _ -> get_imported_node q id)
794

    
795
let check_env_compat header declared computed = 
796
  uneval_prog_generics header;
797
  Env.iter declared (fun k decl_type_k -> 
798
    let computed_t = instantiate (ref []) (ref []) 
799
				 (try Env.lookup_value computed k
800
				  with Not_found ->
801
				    let loc = (get_imported_node header k).top_decl_loc in 
802
				    raise (Error (loc, Declared_but_undefined k))) in
803
    (*Types.print_ty Format.std_formatter decl_type_k;
804
    Types.print_ty Format.std_formatter computed_t;*)
805
    try_semi_unify decl_type_k computed_t Location.dummy_loc
806
		    )
807

    
808
(* Local Variables: *)
809
(* compile-command:"make -C .." *)
810
(* End: *)