Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ 3c3414c5

History | View | Annotate | Download (32.7 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

    
31
module type EXPR_TYPE_HUB =
32
sig
33
  type type_expr 
34
  val import: Types.Main.type_expr -> type_expr
35
  val export: type_expr -> Types.Main.type_expr 
36
end
37

    
38
module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.type_expr) =  
39
struct
40

    
41
  module TP = Type_predef.Make (T)
42
  include TP
43
    
44
let basic_coretype_type t =
45
  if is_real_type t then Tydec_real else
46
    if is_int_type t then Tydec_int else
47
      if is_bool_type t then Tydec_bool else
48
	assert false
49

    
50

    
51

    
52
let pp_typing_env fmt env =
53
  Env.pp_env print_ty fmt env
54

    
55
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in
56
    type [ty]. False otherwise. *)
57
let rec occurs tvar ty =
58
  let ty = repr ty in
59
  match type_desc ty with
60
  | Tvar -> ty=tvar
61
  | Tarrow (t1, t2) ->
62
      (occurs tvar t1) || (occurs tvar t2)
63
  | Ttuple tl ->
64
     List.exists (occurs tvar) tl
65
  | Tstruct fl ->
66
     List.exists (fun (f, t) -> occurs tvar t) fl
67
  | Tarray (_, t)
68
  | Tstatic (_, t)
69
  | Tclock t
70
  | Tlink t -> occurs tvar t
71
  | Tenum _ | Tconst _ | Tunivar | Tbasic _ -> false
72

    
73
(** Promote monomorphic type variables to polymorphic type variables. *)
74
(* Generalize by side-effects *)
75
let rec generalize ty =
76
  match type_desc ty with
77
  | Tvar ->
78
      (* No scopes, always generalize *)
79
      ty.tdesc <- Tunivar
80
  | Tarrow (t1,t2) ->
81
      generalize t1; generalize t2
82
  | Ttuple tl ->
83
     List.iter generalize tl
84
  | Tstruct fl ->
85
     List.iter (fun (f, t) -> generalize t) fl
86
  | Tstatic (d, t)
87
  | Tarray (d, t) -> Dimension.generalize d; generalize t
88
  | Tclock t
89
  | Tlink t ->
90
      generalize t
91
  | Tenum _ | Tconst _ | Tunivar | Tbasic _ -> ()
92

    
93
(** Downgrade polymorphic type variables to monomorphic type variables *)
94
let rec instantiate inst_vars inst_dim_vars ty =
95
  let ty = repr ty in
96
  match ty.tdesc with
97
  | Tenum _ | Tconst _ | Tvar | Tbasic _  -> ty
98
  | Tarrow (t1,t2) ->
99
      {ty with tdesc =
100
       Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))}
101
  | Ttuple tlist ->
102
      {ty with tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist)}
103
  | Tstruct flist ->
104
      {ty with tdesc = Tstruct (List.map (fun (f, t) -> (f, instantiate inst_vars inst_dim_vars t)) flist)}
105
  | Tclock t ->
106
	{ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t)}
107
  | Tstatic (d, t) ->
108
	{ty with tdesc = Tstatic (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)}
109
  | Tarray (d, t) ->
110
	{ty with tdesc = Tarray (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)}
111
  | Tlink t ->
112
	(* should not happen *)
113
	{ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t)}
114
  | Tunivar ->
115
      try
116
        List.assoc ty.tid !inst_vars
117
      with Not_found ->
118
        let var = new_var () in
119
	inst_vars := (ty.tid, var)::!inst_vars;
120
	var
121

    
122
(* [type_coretype cty] types the type declaration [cty] *)
123
let rec type_coretype type_dim cty =
124
  match (*get_repr_type*) cty with
125
  | Tydec_any -> new_var ()
126
  | Tydec_int -> type_int
127
  | Tydec_real -> (* Type_predef. *)type_real
128
  (* | Tydec_float -> Type_predef.type_real *)
129
  | Tydec_bool -> (* Type_predef. *)type_bool
130
  | Tydec_clock ty -> (* Type_predef. *)type_clock (type_coretype type_dim ty)
131
  | Tydec_const c -> (* Type_predef. *)type_const c
132
  | Tydec_enum tl -> (* Type_predef. *)type_enum tl
133
  | Tydec_struct fl -> (* Type_predef. *)type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl)
134
  | Tydec_array (d, ty) ->
135
    begin
136
      let d = Dimension.copy (ref []) d in
137
      type_dim d;
138
      (* Type_predef. *)type_array d (type_coretype type_dim ty)
139
    end
140

    
141
(* [coretype_type] is the reciprocal of [type_typecore] *)
142
let rec coretype_type ty =
143
 match (repr ty).tdesc with
144
 | Tvar           -> Tydec_any
145
 | Tbasic _       -> basic_coretype_type ty
146
 | Tconst c       -> Tydec_const c
147
 | Tclock t       -> Tydec_clock (coretype_type t)
148
 | Tenum tl       -> Tydec_enum tl
149
 | Tstruct fl     -> Tydec_struct (List.map (fun (f, t) -> (f, coretype_type t)) fl)
150
 | Tarray (d, t)  -> Tydec_array (d, coretype_type t)
151
 | Tstatic (_, t) -> coretype_type t
152
 | _         -> assert false
153

    
154
let get_coretype_definition tname =
155
  try
156
    let top = Hashtbl.find type_table (Tydec_const tname) in
157
    match top.top_decl_desc with
158
    | TypeDef tdef -> tdef.tydef_desc
159
    | _ -> assert false
160
  with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
161

    
162
let get_type_definition tname =
163
    type_coretype (fun d -> ()) (get_coretype_definition tname)
164

    
165
(* Equality on ground types only *)
166
(* Should be used between local variables which must have a ground type *)
167
let rec eq_ground t1 t2 =
168
  let t1 = repr t1 in
169
  let t2 = repr t2 in
170
  t1==t2 ||
171
  match t1.tdesc, t2.tdesc with
172
  | Tbasic t1, Tbasic t2 when t1 == t2 -> true
173
  | Tenum tl, Tenum tl' when tl == tl' -> true
174
  | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> List.for_all2 eq_ground tl tl'
175
  | 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'
176
  | (Tconst t, _) ->
177
    let def_t = get_type_definition t in
178
    eq_ground def_t t2
179
  | (_, Tconst t)  ->
180
    let def_t = get_type_definition t in
181
    eq_ground t1 def_t
182
  | Tarrow (t1,t2), Tarrow (t1',t2') -> eq_ground t1 t1' && eq_ground t2 t2'
183
  | Tclock t1', Tclock t2' -> eq_ground t1' t2'
184
  | Tstatic (e1, t1'), Tstatic (e2, t2')
185
  | Tarray (e1, t1'), Tarray (e2, t2') -> Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'
186
  | _ -> false
187

    
188
(** [unify t1 t2] unifies types [t1] and [t2]
189
    using standard destructive unification.
190
    Raises [Unify (t1,t2)] if the types are not unifiable.
191
    [t1] is a expected/formal/spec type, [t2] is a computed/real/implem type,
192
    so in case of unification error: expected type [t1], got type [t2].
193
    If [sub]-typing is allowed, [t2] may be a subtype of [t1].
194
    If [semi] unification is required,
195
    [t1] should furthermore be an instance of [t2]
196
    and constants are handled differently.*)
197
let unify ?(sub=false) ?(semi=false) t1 t2 =
198
  let rec unif t1 t2 =
199
    let t1 = repr t1 in
200
    let t2 = repr t2 in
201
    if t1==t2 then
202
      ()
203
    else
204
      match t1.tdesc,t2.tdesc with
205
      (* strictly subtyping cases first *)
206
      | _ , Tclock t2 when sub && (get_clock_base_type t1 = None) ->
207
	unif t1 t2
208
      | _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) ->
209
	unif t1 t2
210
      (* This case is not mandatory but will keep "older" types *)
211
      | Tvar, Tvar ->
212
        if t1.tid < t2.tid then
213
          t2.tdesc <- Tlink t1
214
        else
215
          t1.tdesc <- Tlink t2
216
      | Tvar, _ when (not semi) && (not (occurs t1 t2)) ->
217
        t1.tdesc <- Tlink t2
218
      | _, Tvar when (not (occurs t2 t1)) ->
219
        t2.tdesc <- Tlink t1
220
      | Tarrow (t1,t2), Tarrow (t1',t2') ->
221
	begin
222
          unif t2 t2';
223
	  unif t1' t1
224
	end
225
      | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
226
	List.iter2 unif tl tl'
227
      | Ttuple [t1]        , _                  -> unif t1 t2
228
      | _                  , Ttuple [t2]        -> unif t1 t2
229
      | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
230
	List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'
231
      | Tclock _, Tstatic _
232
      | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
233
      | Tclock t1', Tclock t2' -> unif t1' t2'
234
      | Tbasic t1, Tbasic t2 when t1 == t2 -> ()
235
      | Tunivar, _ | _, Tunivar -> ()
236
      | (Tconst t, _) ->
237
	let def_t = get_type_definition t in
238
	unif def_t t2
239
      | (_, Tconst t)  ->
240
	let def_t = get_type_definition t in
241
	unif t1 def_t
242
      | Tenum tl, Tenum tl' when tl == tl' -> ()
243
      | Tstatic (e1, t1'), Tstatic (e2, t2')
244
      | Tarray (e1, t1'), Tarray (e2, t2') ->
245
	let eval_const =
246
	  if semi
247
	  then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c))
248
	  else (fun c -> None) in
249
	begin
250
	  unif t1' t2';
251
	  Dimension.eval Basic_library.eval_env eval_const e1;
252
	  Dimension.eval Basic_library.eval_env eval_const e2;
253
	  Dimension.unify ~semi:semi e1 e2;
254
	end
255
      (* Special cases for machine_types. Rules to unify static types infered
256
      	 for numerical constants with non static ones for variables with
257
      	 possible machine types *)
258
      | Tbasic bt1, Tbasic bt2 when BasicT.is_unifiable bt1 bt2 -> BasicT.unify bt1 bt2
259
      | _,_ -> raise (Unify (t1, t2))
260
  in unif t1 t2
261

    
262
(* Expected type ty1, got type ty2 *)
263
let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =
264
  try
265
    unify ~sub:sub ~semi:semi ty1 ty2
266
  with
267
  | Unify _ ->
268
    raise (Error (loc, Type_clash (ty1,ty2)))
269
  | Dimension.Unify _ ->
270
    raise (Error (loc, Type_clash (ty1,ty2)))
271

    
272
let rec type_struct_const_field ?(is_annot=false) loc (label, c) =
273
  if Hashtbl.mem field_table label
274
  then let tydef = Hashtbl.find field_table label in
275
       let tydec = (typedef_of_top tydef).tydef_desc in 
276
       let tydec_struct = get_struct_type_fields tydec in
277
       let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
278
       begin
279
	 try_unify ty_label (type_const ~is_annot loc c) loc;
280
	 type_coretype (fun d -> ()) tydec
281
       end
282
  else raise (Error (loc, Unbound_value ("struct field " ^ label)))
283

    
284
and type_const ?(is_annot=false) loc c = 
285
  match c with
286
  | Const_int _     -> (* Type_predef. *)type_int
287
  | Const_real _    -> (* Type_predef. *)type_real
288
  (* | Const_float _   -> Type_predef.type_real *)
289
  | Const_array ca  -> let d = Dimension.mkdim_int loc (List.length ca) in
290
		      let ty = new_var () in
291
		      List.iter (fun e -> try_unify ty (type_const ~is_annot loc e) loc) ca;
292
		      (* Type_predef. *)type_array d ty
293
  | Const_tag t     ->
294
    if Hashtbl.mem tag_table t
295
    then 
296
      let tydef = typedef_of_top (Hashtbl.find tag_table t) in
297
      let tydec =
298
	if is_user_type tydef.tydef_desc
299
	then Tydec_const tydef.tydef_id
300
	else tydef.tydef_desc in
301
      type_coretype (fun d -> ()) tydec
302
    else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
303
  | Const_struct fl ->
304
    let ty_struct = new_var () in
305
    begin
306
      let used =
307
	List.fold_left
308
	  (fun acc (l, c) ->
309
	    if List.mem l acc
310
	    then raise (Error (loc, Already_bound ("struct field " ^ l)))
311
	    else try_unify ty_struct (type_struct_const_field ~is_annot loc (l, c)) loc; l::acc)
312
	  [] fl in
313
      try
314
	let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in
315
(*	List.iter (fun l -> Format.eprintf "total: %s@." l) total;
316
	List.iter (fun l -> Format.eprintf "used: %s@." l) used; *)
317
	let undef = List.find (fun l -> not (List.mem l used)) total
318
	in raise (Error (loc, Unbound_value ("struct field " ^ undef)))
319
      with Not_found -> 
320
	ty_struct
321
    end
322
  | Const_string _ -> if is_annot then (* Type_predef. *)type_string else  assert false (* string should only appear in annotations *)
323

    
324
(* The following typing functions take as parameter an environment [env]
325
   and whether the element being typed is expected to be constant [const]. 
326
   [env] is a pair composed of:
327
  - a map from ident to type, associating to each ident, i.e. 
328
    variables, constants and (imported) nodes, its type including whether
329
    it is constant or not. This latter information helps in checking constant 
330
    propagation policy in Lustre.
331
  - a vdecl list, in order to modify types of declared variables that are
332
    later discovered to be clocks during the typing process.
333
*)
334
let check_constant loc const_expected const_real =
335
  if const_expected && not const_real
336
  then raise (Error (loc, Not_a_constant))
337

    
338
let rec type_add_const env const arg targ =
339
(*Format.eprintf "Typing.type_add_const %a %a@." Printers.pp_expr arg Types.print_ty targ;*)
340
  if const
341
  then let d =
342
	 if is_dimension_type targ
343
	 then dimension_of_expr arg
344
	 else Dimension.mkdim_var () in
345
       let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in
346
       Dimension.eval Basic_library.eval_env eval_const d;
347
       let real_static_type = (* Type_predef. *)type_static d ((* Types. *)dynamic_type targ) in
348
       (match (* Types. *)get_static_value targ with
349
       | None    -> ()
350
       | Some d' -> try_unify targ real_static_type arg.expr_loc);
351
       real_static_type
352
  else targ
353

    
354
(* emulates a subtyping relation between types t and (d : t),
355
   used during node applications and assignments *)
356
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
357
  let loc = real_arg.expr_loc in
358
  let const = const || ((* Types. *)get_static_value formal_type <> None) in
359
  let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in
360
  (*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;*)
361
  try_unify ~sub:sub formal_type real_type loc
362

    
363
(* typing an application implies:
364
   - checking that const formal parameters match real const (maybe symbolic) arguments
365
   - checking type adequation between formal and real arguments
366
   An application may embed an homomorphic/internal function, in which case we need to split
367
   it in many calls
368
*)
369
and type_appl env in_main loc const f args =
370
  let targs = List.map (type_expr env in_main const) args in
371
  if Basic_library.is_homomorphic_fun f && List.exists is_tuple_type targs
372
  then
373
    try
374
      let targs = Utils.transpose_list (List.map type_list_of_type targs) in
375
      (* Types. *)type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)
376
    with 
377
      Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l')))
378
	
379
  else (
380
    type_dependent_call env in_main loc const f (List.combine args targs)
381
  )
382

    
383
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)
384
and type_dependent_call env in_main loc const f targs =
385
(* Format.eprintf "Typing.type_dependent_call %s@." f; *)
386
  let tins, touts = new_var (), new_var () in
387
  (* Format.eprintf "tin=%a, tout=%a@." print_ty tins print_ty touts; *)
388
  let tfun = (* Type_predef. *)type_arrow tins touts in
389
  (* Format.eprintf "fun=%a@." print_ty tfun; *)
390
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
391
  (* Format.eprintf "type subtyping@."; *)
392
  let tins = type_list_of_type tins in
393
  if List.length targs <> List.length tins then
394
    raise (Error (loc, WrongArity (List.length tins, List.length targs)))
395
  else
396
    begin
397
      List.iter2 (
398
	fun (a,t) ti ->
399
	  let t' = type_add_const env (const || (* Types. *)get_static_value ti <> None) a t in
400
	  (* Format.eprintf "uniying ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts;  *)
401
	  try_unify ~sub:true ti t' a.expr_loc;
402
	  (* Format.eprintf "unified ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts;  *)
403
	    
404
      )
405
	targs
406
	tins;
407
      touts
408
    end
409

    
410
(* type a simple call without dependent types 
411
   but possible homomorphic extension.
412
   [targs] is here a list of arguments' types. *)
413
and type_simple_call env in_main loc const f targs =
414
  let tins, touts = new_var (), new_var () in
415
  let tfun = (* Type_predef. *)type_arrow tins touts in
416
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
417
  (*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*)
418
  try_unify ~sub:true tins (type_of_type_list targs) loc;
419
  touts
420

    
421
(** [type_expr env in_main expr] types expression [expr] in environment
422
    [env], expecting it to be [const] or not. *)
423
and type_expr ?(is_annot=false) env in_main const expr =
424
  let resulting_ty = 
425
  match expr.expr_desc with
426
  | Expr_const c ->
427
    let ty = type_const ~is_annot expr.expr_loc c in
428
    let ty = (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty in
429
    expr.expr_type <- Expr_type_hub.export ty;
430
    ty
431
  | Expr_ident v ->
432
    let tyv =
433
      try
434
        Env.lookup_value (fst env) v
435
      with Not_found ->
436
	Format.eprintf "Failure in typing expr %a. Not in typing environement@." Printers.pp_expr expr;
437
        raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))
438
    in
439
    let ty = instantiate (ref []) (ref []) tyv in
440
    let ty' =
441
      if const
442
      then (* Type_predef. *)type_static (Dimension.mkdim_var ()) (new_var ())
443
      else new_var () in
444
    try_unify ty ty' expr.expr_loc;
445
    expr.expr_type <- Expr_type_hub.export ty;
446
    ty 
447
  | Expr_array elist ->
448
    let ty_elt = new_var () in
449
    List.iter (fun e -> try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist;
450
    let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
451
    let ty = (* Type_predef. *)type_array d ty_elt in
452
    expr.expr_type <- Expr_type_hub.export ty;
453
    ty
454
  | Expr_access (e1, d) ->
455
    type_subtyping_arg env in_main false (* not necessary a constant *) (expr_of_dimension d) (* Type_predef. *)type_int;
456
    let ty_elt = new_var () in
457
    let d = Dimension.mkdim_var () in
458
    type_subtyping_arg env in_main const e1 ((* Type_predef. *)type_array d ty_elt);
459
    expr.expr_type <- Expr_type_hub.export ty_elt;
460
    ty_elt
461
  | Expr_power (e1, d) ->
462
    let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in
463
    type_subtyping_arg env in_main true (expr_of_dimension d) (* Type_predef. *)type_int;
464
    Dimension.eval Basic_library.eval_env eval_const d;
465
    let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in
466
    let ty = (* Type_predef. *)type_array d ty_elt in
467
    expr.expr_type <- Expr_type_hub.export ty;
468
    ty
469
  | Expr_tuple elist ->
470
    let ty = new_ty (Ttuple (List.map (type_expr ~is_annot env in_main const) elist)) in
471
    expr.expr_type <- Expr_type_hub.export ty;
472
    ty
473
  | Expr_ite (c, t, e) ->
474
    type_subtyping_arg env in_main const c (* Type_predef. *)type_bool;
475
    let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in
476
    expr.expr_type <- Expr_type_hub.export ty;
477
    ty
478
  | Expr_appl (id, args, r) ->
479
    (* application of non internal function is not legal in a constant
480
       expression *)
481
    (match r with
482
    | None        -> ()
483
    | Some c -> 
484
      check_constant expr.expr_loc const false;	
485
      type_subtyping_arg env in_main const c (* Type_predef. *)type_bool);
486
    let args_list = expr_list_of_expr args in
487
    let targs = new_ty (Ttuple (List.map (fun a -> Expr_type_hub.import a.expr_type) args_list)) in
488
    args.expr_type <- Expr_type_hub.export targs;
489
    let touts = type_appl env in_main expr.expr_loc const id args_list in
490
    expr.expr_type <- Expr_type_hub.export touts;
491
    touts
492
  | Expr_fby (e1,e2)
493
  | Expr_arrow (e1,e2) ->
494
    (* fby/arrow is not legal in a constant expression *)
495
    check_constant expr.expr_loc const false;
496
    let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in
497
    expr.expr_type <- Expr_type_hub.export ty;
498
    ty
499
  | Expr_pre e ->
500
    (* pre is not legal in a constant expression *)
501
    check_constant expr.expr_loc const false;
502
    let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in
503
    expr.expr_type <- Expr_type_hub.export ty;
504
    ty
505
  | Expr_when (e1,c,l) ->
506
    (* when is not legal in a constant expression *)
507
    check_constant expr.expr_loc const false;
508
    let typ_l = (* Type_predef. *)type_clock (type_const ~is_annot expr.expr_loc (Const_tag l)) in
509
    let expr_c = expr_of_ident c expr.expr_loc in
510
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
511
    let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in
512
    expr.expr_type <- Expr_type_hub.export ty;
513
    ty
514
  | Expr_merge (c,hl) ->
515
    (* merge is not legal in a constant expression *)
516
    check_constant expr.expr_loc const false;
517
    let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in
518
    let expr_c = expr_of_ident c expr.expr_loc in
519
    let typ_l = (* Type_predef. *)type_clock typ_in in
520
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
521
    expr.expr_type <- Expr_type_hub.export typ_out;
522
    typ_out
523
  in 
524
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr (* Types. *)print_ty resulting_ty);
525
  resulting_ty
526

    
527
and type_branches ?(is_annot=false) env in_main loc const hl =
528
  let typ_in = new_var () in
529
  let typ_out = new_var () in
530
  try
531
    let used_labels =
532
      List.fold_left (fun accu (t, h) ->
533
	unify typ_in (type_const ~is_annot loc (Const_tag t));
534
	type_subtyping_arg env in_main const h typ_out;
535
	if List.mem t accu
536
	then raise (Error (loc, Already_bound t))
537
	else t :: accu) [] hl in
538
    let type_labels = get_enum_type_tags (coretype_type typ_in) in
539
    if List.sort compare used_labels <> List.sort compare type_labels
540
    then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in
541
	 raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
542
    else (typ_in, typ_out)
543
  with Unify (t1, t2) ->
544
    raise (Error (loc, Type_clash (t1,t2)))
545

    
546
(** [type_eq env eq] types equation [eq] in environment [env] *)
547
let type_eq env in_main undefined_vars eq =
548
(*Format.eprintf "Typing.type_eq %a@." Printers.pp_node_eq eq;*)
549
  (* Check undefined variables, type lhs *)
550
  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
551
  let ty_lhs = type_expr env in_main false expr_lhs in
552
  (* Check multiple variable definitions *)
553
  let define_var id uvars =
554
    if ISet.mem id uvars
555
    then ISet.remove id uvars
556
    else raise (Error (eq.eq_loc, Already_defined id))
557
  in
558
  (* check assignment of declared constant, assignment of clock *)
559
  let ty_lhs =
560
    type_of_type_list
561
      (List.map2 (fun ty id ->
562
	if get_static_value ty <> None
563
	then raise (Error (eq.eq_loc, Assigned_constant id)) else
564
	match get_clock_base_type ty with
565
	| None -> ty
566
	| Some ty -> ty)
567
	 (type_list_of_type ty_lhs) eq.eq_lhs) in
568
  let undefined_vars =
569
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
570
  (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
571
     to a (always non-constant) lhs variable *)
572
  type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
573
  undefined_vars
574

    
575

    
576
(* [type_coreclock env ck id loc] types the type clock declaration [ck]
577
   in environment [env] *)
578
let type_coreclock env ck id loc =
579
  match ck.ck_dec_desc with
580
  | Ckdec_any -> ()
581
  | Ckdec_bool cl ->
582
      let dummy_id_expr = expr_of_ident id loc in
583
      let when_expr =
584
        List.fold_left
585
          (fun expr (x, l) ->
586
                {expr_tag = new_tag ();
587
                 expr_desc= Expr_when (expr,x,l);
588
                 expr_type = Types.Main.new_var ();
589
                 expr_clock = Clocks.new_var true;
590
                 expr_delay = Delay.new_var ();
591
                 expr_loc=loc;
592
		 expr_annot = None})
593
          dummy_id_expr cl
594
      in
595
      ignore (type_expr env false false when_expr)
596

    
597
let rec check_type_declaration loc cty =
598
 match cty with
599
 | Tydec_clock ty
600
 | Tydec_array (_, ty) -> check_type_declaration loc ty
601
 | Tydec_const tname   ->
602
    (* Format.eprintf "TABLE: %a@." print_type_table (); *)
603
    if not (Hashtbl.mem type_table cty)
604
    then raise (Error (loc, Unbound_type tname));
605
 | _                   -> ()
606

    
607
let type_var_decl vd_env env vdecl =
608
(*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*)
609
  check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
610
  let eval_const id = (* Types. *)get_static_value (Env.lookup_value env id) in
611
  let type_dim d =
612
    begin
613
      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) (* Type_predef. *)type_int;
614
      Dimension.eval Basic_library.eval_env eval_const d;
615
    end in
616
  let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
617

    
618
  let ty_static =
619
    if vdecl.var_dec_const
620
    then (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty
621
    else ty in
622
  (match vdecl.var_dec_value with
623
  | None   -> ()
624
  | Some v -> type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static);
625
  try_unify ty_static (Expr_type_hub.import vdecl.var_type) vdecl.var_loc;
626
  let new_env = Env.add_value env vdecl.var_id ty_static in
627
  type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
628
(*Format.eprintf "END %a@." Types.print_ty ty_static;*)
629
  new_env
630

    
631
let type_var_decl_list vd_env env l =
632
  List.fold_left (type_var_decl vd_env) env l
633

    
634
let type_of_vlist vars =
635
  let tyl = List.map (fun v -> Expr_type_hub.import v.var_type) vars in
636
  type_of_type_list tyl
637

    
638
let add_vdecl vd_env vdecl =
639
 if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
640
 then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
641
 else vdecl::vd_env
642

    
643
let check_vd_env vd_env =
644
  ignore (List.fold_left add_vdecl [] vd_env)
645

    
646
(** [type_node env nd loc] types node [nd] in environment env. The
647
    location is used for error reports. *)
648
let type_node env nd loc =
649
  let is_main = nd.node_id = !Options.main_node in
650
  let vd_env_ol = nd.node_outputs@nd.node_locals in
651
  let vd_env =  nd.node_inputs@vd_env_ol in
652
  check_vd_env vd_env;
653
  let init_env = env in
654
  let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
655
  let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
656
  let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
657
  let new_env = Env.overwrite env delta_env in
658
  let undefined_vars_init =
659
    List.fold_left
660
      (fun uvs v -> ISet.add v.var_id uvs)
661
      ISet.empty vd_env_ol in
662
  let undefined_vars =
663
    let eqs, auts = get_node_eqs nd in
664
    (* TODO XXX: il faut typer les handlers de l'automate *)
665
    List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs
666
  in
667
  (* Typing asserts *)
668
  List.iter (fun assert_ ->
669
    let assert_expr =  assert_.assert_expr in
670
    type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool
671
  )  nd.node_asserts;
672
  (* Typing annots *)
673
  List.iter (fun annot ->
674
    List.iter (fun (_, eexpr) -> ignore (type_expr ~is_annot:true (new_env, vd_env) false false eexpr.eexpr_qfexpr)) annot.annots
675
  ) nd.node_annot;
676
  
677
  (* check that table is empty *)
678
  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
679
  let undefined_vars = ISet.diff undefined_vars local_consts in
680
  if (not (ISet.is_empty undefined_vars)) then
681
    raise (Error (loc, Undefined_var undefined_vars));
682
  let ty_ins = type_of_vlist nd.node_inputs in
683
  let ty_outs = type_of_vlist nd.node_outputs in
684
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
685
  generalize ty_node;
686
  (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
687
  nd.node_type <- Expr_type_hub.export ty_node;
688
  Env.add_value env nd.node_id ty_node
689

    
690
let type_imported_node env nd loc =
691
  let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
692
  let vd_env = nd.nodei_inputs@nd.nodei_outputs in
693
  check_vd_env vd_env;
694
  ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
695
  let ty_ins = type_of_vlist nd.nodei_inputs in
696
  let ty_outs = type_of_vlist nd.nodei_outputs in
697
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
698
  generalize ty_node;
699
(*
700
  if (is_polymorphic ty_node) then
701
    raise (Error (loc, Poly_imported_node nd.nodei_id));
702
*)
703
  let new_env = Env.add_value env nd.nodei_id ty_node in
704
  nd.nodei_type <- Expr_type_hub.export ty_node;
705
  new_env
706

    
707
let type_top_const env cdecl =
708
  let ty = type_const cdecl.const_loc cdecl.const_value in
709
  let d =
710
    if is_dimension_type ty
711
    then dimension_of_const cdecl.const_loc cdecl.const_value
712
    else Dimension.mkdim_var () in
713
  let ty = (* Type_predef. *)type_static d ty in
714
  let new_env = Env.add_value env cdecl.const_id ty in
715
  cdecl.const_type <- Expr_type_hub.export ty;
716
  new_env
717

    
718
let type_top_consts env clist =
719
  List.fold_left type_top_const env clist
720

    
721
let rec type_top_decl env decl =
722
  match decl.top_decl_desc with
723
  | Node nd -> (
724
    try
725
      type_node env nd decl.top_decl_loc
726
    with Error (loc, err) as exc -> (
727
      if !Options.global_inline then
728
	Format.eprintf "Type error: failing node@.%a@.@?"
729
	  Printers.pp_node nd
730
      ;
731
      raise exc)
732
  )
733
  | ImportedNode nd ->
734
    type_imported_node env nd decl.top_decl_loc
735
  | Const c ->
736
    type_top_const env c
737
  | TypeDef _ -> List.fold_left type_top_decl env (consts_of_enum_type decl)
738
  | Open _  -> env
739

    
740
let get_type_of_call decl =
741
  match decl.top_decl_desc with
742
  | Node nd         ->
743
    let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.node_type) in
744
    type_list_of_type in_typ, type_list_of_type out_typ
745
  | ImportedNode nd ->
746
    let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.nodei_type) in
747
    type_list_of_type in_typ, type_list_of_type out_typ
748
  | _               -> assert false
749

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

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

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

    
770
let uneval_node_generics vdecls =
771
  List.iter uneval_vdecl_generics vdecls
772

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

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

    
786
let rec get_imported_symbol decls id =
787
  match decls with
788
  | [] -> assert false
789
  | decl::q ->
790
     (match decl.top_decl_desc with
791
      | ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf -> decl
792
      | Const c when id = c.const_id && decl.top_decl_itf -> decl
793
      | TypeDef _ -> get_imported_symbol (consts_of_enum_type decl @ q) id
794
      | _ -> get_imported_symbol q id)
795

    
796
let check_env_compat header declared computed = 
797
  uneval_prog_generics header;
798
  Env.iter declared (fun k decl_type_k ->
799
    let loc = (get_imported_symbol header k).top_decl_loc in 
800
    let computed_t =
801
      instantiate (ref []) (ref []) 
802
	(try Env.lookup_value computed k
803
	 with Not_found -> raise (Error (loc, Declared_but_undefined k))) in
804
    (*Types.print_ty Format.std_formatter decl_type_k;
805
      Types.print_ty Format.std_formatter computed_t;*)
806
    try_unify ~sub:true ~semi:true decl_type_k computed_t loc
807
  )
808

    
809
let check_typedef_top decl =
810
(*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*)
811
(*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*)
812
(*Format.eprintf "%a" Corelang.print_type_table ();*)
813
  match decl.top_decl_desc with
814
  | TypeDef ty ->
815
     let owner = decl.top_decl_owner in
816
     let itf = decl.top_decl_itf in
817
     let decl' =
818
       try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id)
819
       with Not_found -> raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in
820
     let owner' = decl'.top_decl_owner in
821
(*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*)
822
     let itf' = decl'.top_decl_itf in
823
     (match decl'.top_decl_desc with
824
     | Const _ | Node _ | ImportedNode _ -> assert false
825
     | TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') -> ()
826
     | _ -> raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id)))
827
  | _  -> ()
828

    
829
let check_typedef_compat header =
830
  List.iter check_typedef_top header
831
end
832

    
833
include  Make(Types.Main) (struct
834
  type type_expr  = Types.Main.type_expr
835
  let import x = x
836
  let export x = x
837
end)
838
(* Local Variables: *)
839
(* compile-command:"make -C .." *)
840
(* End: *)