Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ 53206908

History | View | Annotate | Download (30.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
      let d = Dimension.copy (ref []) d in
115
      type_dim d;
116
      Type_predef.type_array d (type_coretype type_dim ty)
117
    end
118

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

    
134
let get_coretype_definition tname =
135
  try
136
    let top = Hashtbl.find type_table (Tydec_const tname) in
137
    match top.top_decl_desc with
138
    | TypeDef tdef -> tdef.tydef_desc
139
    | _ -> assert false
140
  with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
141

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

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

    
238
(* Expected type ty1, got type ty2 *)
239
let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =
240
  try
241
    unify ~sub:sub ~semi:semi ty1 ty2
242
  with
243
  | Unify _ ->
244
    raise (Error (loc, Type_clash (ty1,ty2)))
245
  | Dimension.Unify _ ->
246
    raise (Error (loc, Type_clash (ty1,ty2)))
247

    
248
let rec type_struct_const_field loc (label, c) =
249
  if Hashtbl.mem field_table label
250
  then let tydef = Hashtbl.find field_table label in
251
       let tydec = (typedef_of_top tydef).tydef_desc in 
252
       let tydec_struct = get_struct_type_fields tydec in
253
       let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
254
       begin
255
	 try_unify ty_label (type_const loc c) loc;
256
	 type_coretype (fun d -> ()) tydec
257
       end
258
  else raise (Error (loc, Unbound_value ("struct field " ^ label)))
259

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

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

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

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

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

    
357
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)
358
and type_dependent_call env in_main loc const f targs =
359
(*Format.eprintf "Typing.type_dependent_call %s@." f;*)
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 args_list = expr_list_of_expr args in
451
    let touts = type_appl env in_main expr.expr_loc const id args_list in
452
    args.expr_type <- new_ty (Ttuple (List.map (fun a -> a.expr_type) args_list));
453
    expr.expr_type <- touts;
454
    touts
455
  | Expr_fby (e1,e2)
456
  | Expr_arrow (e1,e2) ->
457
    (* fby/arrow is not legal in a constant expression *)
458
    check_constant expr.expr_loc const false;
459
    let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in
460
    expr.expr_type <- ty;
461
    ty
462
  | Expr_pre e ->
463
    (* pre is not legal in a constant expression *)
464
    check_constant expr.expr_loc const false;
465
    let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in
466
    expr.expr_type <- ty;
467
    ty
468
  | Expr_when (e1,c,l) ->
469
    (* when is not legal in a constant expression *)
470
    check_constant expr.expr_loc const false;
471
    let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in
472
    let expr_c = expr_of_ident c expr.expr_loc in
473
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
474
    let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in
475
    expr.expr_type <- ty;
476
    ty
477
  | Expr_merge (c,hl) ->
478
    (* merge is not legal in a constant expression *)
479
    check_constant expr.expr_loc const false;
480
    let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in
481
    let expr_c = expr_of_ident c expr.expr_loc in
482
    let typ_l = Type_predef.type_clock typ_in in
483
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
484
    expr.expr_type <- typ_out;
485
    typ_out
486
  in 
487
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr Types.print_ty resulting_ty);
488
  resulting_ty
489

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

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

    
538

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

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

    
569
let type_var_decl vd_env env vdecl =
570
(*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*)
571
  check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
572
  let eval_const id = Types.get_static_value (Env.lookup_value env id) in
573
  let type_dim d =
574
    begin
575
      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;
576
      Dimension.eval Basic_library.eval_env eval_const d;
577
    end in
578
  let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
579

    
580
  let ty_static =
581
    if vdecl.var_dec_const
582
    then Type_predef.type_static (Dimension.mkdim_var ()) ty
583
    else ty in
584
  (match vdecl.var_dec_value with
585
  | None   -> ()
586
  | Some v -> type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static);
587
  try_unify ty_static vdecl.var_type vdecl.var_loc;
588
  let new_env = Env.add_value env vdecl.var_id ty_static in
589
  type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
590
(*Format.eprintf "END %a@." Types.print_ty ty_static;*)
591
  new_env
592

    
593
let type_var_decl_list vd_env env l =
594
  List.fold_left (type_var_decl vd_env) env l
595

    
596
let type_of_vlist vars =
597
  let tyl = List.map (fun v -> v.var_type) vars in
598
  type_of_type_list tyl
599

    
600
let add_vdecl vd_env vdecl =
601
 if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
602
 then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
603
 else vdecl::vd_env
604

    
605
let check_vd_env vd_env =
606
  ignore (List.fold_left add_vdecl [] vd_env)
607

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

    
646
let type_imported_node env nd loc =
647
  let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
648
  let vd_env = nd.nodei_inputs@nd.nodei_outputs in
649
  check_vd_env vd_env;
650
  ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
651
  let ty_ins = type_of_vlist nd.nodei_inputs in
652
  let ty_outs = type_of_vlist nd.nodei_outputs in
653
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
654
  generalize ty_node;
655
(*
656
  if (is_polymorphic ty_node) then
657
    raise (Error (loc, Poly_imported_node nd.nodei_id));
658
*)
659
  let new_env = Env.add_value env nd.nodei_id ty_node in
660
  nd.nodei_type <- ty_node;
661
  new_env
662

    
663
let type_top_const env cdecl =
664
  let ty = type_const cdecl.const_loc cdecl.const_value in
665
  let d =
666
    if is_dimension_type ty
667
    then dimension_of_const cdecl.const_loc cdecl.const_value
668
    else Dimension.mkdim_var () in
669
  let ty = Type_predef.type_static d ty in
670
  let new_env = Env.add_value env cdecl.const_id ty in
671
  cdecl.const_type <- ty;
672
  new_env
673

    
674
let type_top_consts env clist =
675
  List.fold_left type_top_const env clist
676

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

    
696
let get_type_of_call decl =
697
  match decl.top_decl_desc with
698
  | Node nd         ->
699
    let (in_typ, out_typ) = split_arrow nd.node_type in
700
    type_list_of_type in_typ, type_list_of_type out_typ
701
  | ImportedNode nd ->
702
    let (in_typ, out_typ) = split_arrow nd.nodei_type in
703
    type_list_of_type in_typ, type_list_of_type out_typ
704
  | _               -> assert false
705

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

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

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

    
726
let uneval_node_generics vdecls =
727
  List.iter uneval_vdecl_generics vdecls
728

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

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

    
742
let rec get_imported_symbol decls id =
743
  match decls with
744
  | [] -> assert false
745
  | decl::q ->
746
     (match decl.top_decl_desc with
747
      | ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf -> decl
748
      | Const c when id = c.const_id && decl.top_decl_itf -> decl
749
      | TypeDef _ -> get_imported_symbol (consts_of_enum_type decl @ q) id
750
      | _ -> get_imported_symbol q id)
751

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

    
765
let check_typedef_top decl =
766
(*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*)
767
(*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*)
768
(*Format.eprintf "%a" Corelang.print_type_table ();*)
769
  match decl.top_decl_desc with
770
  | TypeDef ty ->
771
     let owner = decl.top_decl_owner in
772
     let itf = decl.top_decl_itf in
773
     let decl' =
774
       try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id)
775
       with Not_found -> raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in
776
     let owner' = decl'.top_decl_owner in
777
(*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*)
778
     let itf' = decl'.top_decl_itf in
779
     (match decl'.top_decl_desc with
780
     | Const _ | Node _ | ImportedNode _ -> assert false
781
     | TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') -> ()
782
     | _ -> raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id)))
783
  | _  -> ()
784

    
785
let check_typedef_compat header =
786
  List.iter check_typedef_top header
787

    
788
(* Local Variables: *)
789
(* compile-command:"make -C .." *)
790
(* End: *)