Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / typing.ml @ 7dedc5f0

History | View | Annotate | Download (28.1 KB)

1 b38ffff3 ploc
(********************************************************************)
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 0cbf0839 ploc
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 aa223e69 xthirioux
     List.exists (occurs tvar) tl
43
  | Tstruct fl ->
44
     List.exists (fun (f, t) -> occurs tvar t) fl
45 0cbf0839 ploc
  | 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 aa223e69 xthirioux
  | Ttuple tl ->
61
     List.iter generalize tl
62
  | Tstruct fl ->
63
     List.iter (fun (f, t) -> generalize t) fl
64 0cbf0839 ploc
  | 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 aa223e69 xthirioux
  | Tstruct flist ->
82
      {ty with tdesc = Tstruct (List.map (fun (f, t) -> (f, instantiate inst_vars inst_dim_vars t)) flist)}
83 0cbf0839 ploc
  | 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 aa223e69 xthirioux
  | Tydec_struct fl -> Type_predef.type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl)
112 0cbf0839 ploc
  | Tydec_array (d, ty) ->
113
    begin
114
      type_dim d;
115
      Type_predef.type_array d (type_coretype type_dim ty)
116
    end
117
118 6affc9f5 xthirioux
(* [coretype_type] is the reciprocal of [type_typecore] *)
119 0cbf0839 ploc
let rec coretype_type ty =
120
 match (repr ty).tdesc with
121
 | Tvar           -> Tydec_any
122
 | Tint           -> Tydec_int
123
 | Treal          -> Tydec_real
124
 | Tbool          -> Tydec_bool
125
 | Tconst c       -> Tydec_const c
126
 | Tclock t       -> Tydec_clock (coretype_type t)
127
 | Tenum tl       -> Tydec_enum tl
128 aa223e69 xthirioux
 | Tstruct fl     -> Tydec_struct (List.map (fun (f, t) -> (f, coretype_type t)) fl)
129 0cbf0839 ploc
 | Tarray (d, t)  -> Tydec_array (d, coretype_type t)
130
 | Tstatic (_, t) -> coretype_type t
131
 | _         -> assert false
132
133
let get_type_definition tname =
134
  try
135
    type_coretype (fun d -> ()) (Hashtbl.find type_table (Tydec_const tname))
136
  with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
137
138 d4101ea0 xthirioux
(* Equality on ground types only *)
139
(* Should be used between local variables which must have a ground type *)
140
let rec eq_ground t1 t2 =
141 8fa083d5 xthirioux
  let t1 = repr t1 in
142
  let t2 = repr t2 in
143
  t1==t2 ||
144 d4101ea0 xthirioux
  match t1.tdesc, t2.tdesc with
145 d96d54ac xthirioux
  | Tint, Tint | Tbool, Tbool | Trat, Trat | Treal, Treal -> true
146 d4101ea0 xthirioux
  | Tenum tl, Tenum tl' when tl == tl' -> true
147
  | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> List.for_all2 eq_ground tl tl'
148
  | 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'
149
  | (Tconst t, _) ->
150
    let def_t = get_type_definition t in
151
    eq_ground def_t t2
152
  | (_, Tconst t)  ->
153
    let def_t = get_type_definition t in
154
    eq_ground t1 def_t
155
  | Tarrow (t1,t2), Tarrow (t1',t2') -> eq_ground t1 t1' && eq_ground t2 t2'
156 6b4d172f xthirioux
  | Tclock t1', Tclock t2' -> eq_ground t1' t2'
157 d4101ea0 xthirioux
  | Tstatic (e1, t1'), Tstatic (e2, t2')
158
  | Tarray (e1, t1'), Tarray (e2, t2') -> Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'
159
  | _ -> false
160
161 6b4d172f xthirioux
(** [unify t1 t2] unifies types [t1] and [t2]
162
    using standard destructive unification.
163
    Raises [Unify (t1,t2)] if the types are not unifiable.
164
    [t1] is a expected/formal/spec type, [t2] is a computed/real/implem type,
165
    so in case of unification error: expected type [t1], got type [t2].
166
    If [sub]-typing is allowed, [t2] may be a subtype of [t1].
167
    If [semi] unification is required,
168
    [t1] should furthermore be an instance of [t2]
169
    and constants are handled differently.*)
170
let unify ?(sub=false) ?(semi=false) t1 t2 =
171
  let rec unif t1 t2 =
172
    let t1 = repr t1 in
173
    let t2 = repr t2 in
174 d96d54ac xthirioux
    if t1==t2 then
175 6b4d172f xthirioux
      ()
176
    else
177
      match t1.tdesc,t2.tdesc with
178
      (* strictly subtyping cases first *)
179
      | _ , Tclock t2 when sub && (get_clock_base_type t1 = None) ->
180
	unif t1 t2
181
      | _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) ->
182
	unif t1 t2
183
      (* This case is not mandatory but will keep "older" types *)
184
      | Tvar, Tvar ->
185 0cbf0839 ploc
        if t1.tid < t2.tid then
186
          t2.tdesc <- Tlink t1
187
        else
188
          t1.tdesc <- Tlink t2
189 6b4d172f xthirioux
      | Tvar, _ when (not semi) && (not (occurs t1 t2)) ->
190 0cbf0839 ploc
        t1.tdesc <- Tlink t2
191 6b4d172f xthirioux
      | _, Tvar when (not (occurs t2 t1)) ->
192 b878abe5 xthirioux
        t2.tdesc <- Tlink t1
193 6b4d172f xthirioux
      | Tarrow (t1,t2), Tarrow (t1',t2') ->
194
	begin
195
          unif t2 t2';
196
	  unif t1' t1
197
	end
198
      | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
199
	List.iter2 unif tl tl'
200
      | Ttuple [t1]        , _                  -> unif t1 t2
201
      | _                  , Ttuple [t2]        -> unif t1 t2
202
      | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
203
	List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'
204
      | Tclock _, Tstatic _
205
      | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
206
      | Tclock t1', Tclock t2' -> unif t1' t2'
207 d96d54ac xthirioux
      | Tint, Tint | Tbool, Tbool | Trat, Trat | Treal, Treal
208 6b4d172f xthirioux
      | Tunivar, _ | _, Tunivar -> ()
209
      | (Tconst t, _) ->
210
	let def_t = get_type_definition t in
211
	unif def_t t2
212
      | (_, Tconst t)  ->
213
	let def_t = get_type_definition t in
214
	unif t1 def_t
215
      | Tenum tl, Tenum tl' when tl == tl' -> ()
216
      | Tstatic (e1, t1'), Tstatic (e2, t2')
217
      | Tarray (e1, t1'), Tarray (e2, t2') ->
218
	let eval_const =
219
	  if semi
220
	  then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c))
221
	  else (fun c -> None) in
222
	begin
223
	  unif t1' t2';
224
	  Dimension.eval Basic_library.eval_env eval_const e1;
225
	  Dimension.eval Basic_library.eval_env eval_const e2;
226
	  Dimension.unify ~semi:semi e1 e2;
227
	end
228
      | _,_ -> raise (Unify (t1, t2))
229
  in unif t1 t2
230 b878abe5 xthirioux
231 aa223e69 xthirioux
(* Expected type ty1, got type ty2 *)
232 6b4d172f xthirioux
let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =
233 8b3afe43 xthirioux
  try
234 6b4d172f xthirioux
    unify ~sub:sub ~semi:semi ty1 ty2
235 8b3afe43 xthirioux
  with
236
  | Unify _ ->
237
    raise (Error (loc, Type_clash (ty1,ty2)))
238
  | Dimension.Unify _ ->
239
    raise (Error (loc, Type_clash (ty1,ty2)))
240
241 6affc9f5 xthirioux
let rec type_struct_const_field loc (label, c) =
242 aa223e69 xthirioux
  if Hashtbl.mem field_table label
243
  then let tydec = Hashtbl.find field_table label in
244
       let tydec_struct = get_struct_type_fields tydec in
245
       let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
246
       begin
247 6affc9f5 xthirioux
	 try_unify ty_label (type_const loc c) loc;
248 aa223e69 xthirioux
	 type_coretype (fun d -> ()) tydec
249
       end
250
  else raise (Error (loc, Unbound_value ("struct field " ^ label)))
251
252 6affc9f5 xthirioux
and type_const loc c = 
253 0cbf0839 ploc
  match c with
254 aa223e69 xthirioux
  | Const_int _     -> Type_predef.type_int
255
  | Const_real _    -> Type_predef.type_real
256
  | Const_float _   -> Type_predef.type_real
257
  | Const_array ca  -> let d = Dimension.mkdim_int loc (List.length ca) in
258 0cbf0839 ploc
		      let ty = new_var () in
259 aa223e69 xthirioux
		      List.iter (fun e -> try_unify ty (type_const loc e) loc) ca;
260 0cbf0839 ploc
		      Type_predef.type_array d ty
261 aa223e69 xthirioux
  | Const_tag t     ->
262 0cbf0839 ploc
    if Hashtbl.mem tag_table t
263
    then type_coretype (fun d -> ()) (Hashtbl.find tag_table t)
264
    else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
265 aa223e69 xthirioux
  | Const_struct fl ->
266
    let ty_struct = new_var () in
267
    begin
268 6affc9f5 xthirioux
      let used =
269
	List.fold_left
270
	  (fun acc (l, c) ->
271
	    if List.mem l acc
272
	    then raise (Error (loc, Already_bound ("struct field " ^ l)))
273
	    else try_unify ty_struct (type_struct_const_field loc (l, c)) loc; l::acc)
274
	  [] fl in
275
      try
276
	let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in
277
(*	List.iter (fun l -> Format.eprintf "total: %s@." l) total;
278
	List.iter (fun l -> Format.eprintf "used: %s@." l) used; *)
279
	let undef = List.find (fun l -> not (List.mem l used)) total
280
	in raise (Error (loc, Unbound_value ("struct field " ^ undef)))
281
      with Not_found -> 
282
	ty_struct
283 aa223e69 xthirioux
    end
284 0038002e ploc
  | Const_string _ -> assert false (* string should only appear in annotations *)
285 0cbf0839 ploc
286
(* The following typing functions take as parameter an environment [env]
287
   and whether the element being typed is expected to be constant [const]. 
288
   [env] is a pair composed of:
289
  - a map from ident to type, associating to each ident, i.e. 
290
    variables, constants and (imported) nodes, its type including whether
291
    it is constant or not. This latter information helps in checking constant 
292
    propagation policy in Lustre.
293
  - a vdecl list, in order to modify types of declared variables that are
294
    later discovered to be clocks during the typing process.
295
*)
296
let check_constant loc const_expected const_real =
297
  if const_expected && not const_real
298
  then raise (Error (loc, Not_a_constant))
299
300 2cf39a8e xthirioux
let rec type_add_const env const arg targ =
301
  if const
302
  then let d =
303
	 if is_dimension_type targ
304
	 then dimension_of_expr arg
305
	 else Dimension.mkdim_var () in
306
       let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
307
       Dimension.eval Basic_library.eval_env eval_const d;
308
       let real_static_type = Type_predef.type_static d (Types.dynamic_type targ) in
309
       (match Types.get_static_value targ with
310
       | None    -> ()
311
       | Some d' -> try_unify targ real_static_type arg.expr_loc);
312
       real_static_type
313
  else targ
314 0cbf0839 ploc
315
(* emulates a subtyping relation between types t and (d : t),
316 b580c8f8 xthirioux
   used during node applications and assignments *)
317 0cbf0839 ploc
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
318
  let loc = real_arg.expr_loc in
319
  let const = const || (Types.get_static_value formal_type <> None) in
320 2cf39a8e xthirioux
  let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in
321 d3e4c22f xthirioux
  (*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;*)
322 6b4d172f xthirioux
  try_unify ~sub:sub formal_type real_type loc
323 d3e4c22f xthirioux
324 0cbf0839 ploc
and type_ident env in_main loc const id =
325
  type_expr env in_main const (expr_of_ident id loc)
326
327
(* typing an application implies:
328
   - checking that const formal parameters match real const (maybe symbolic) arguments
329
   - checking type adequation between formal and real arguments
330 14d694c7 xthirioux
   An application may embed an homomorphic/internal function, in which case we need to split
331
   it in many calls
332 0cbf0839 ploc
*)
333
and type_appl env in_main loc const f args =
334 2cf39a8e xthirioux
  let targs = List.map (type_expr env in_main const) args in
335
  if Basic_library.is_internal_fun f && List.exists is_tuple_type targs
336 14d694c7 xthirioux
  then
337
    try
338 2cf39a8e xthirioux
      let targs = Utils.transpose_list (List.map type_list_of_type targs) in
339
      Types.type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)
340 14d694c7 xthirioux
    with
341
      Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l')))
342
  else
343 2cf39a8e xthirioux
    type_dependent_call env in_main loc const f (List.combine args targs)
344 14d694c7 xthirioux
345 2cf39a8e xthirioux
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)
346
and type_dependent_call env in_main loc const f targs =
347 f6fa97f9 xthirioux
  let tins, touts = new_var (), new_var () in
348
  let tfun = Type_predef.type_arrow tins touts in
349
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
350 0cbf0839 ploc
  let tins = type_list_of_type tins in
351 2cf39a8e xthirioux
  if List.length targs <> List.length tins then
352
    raise (Error (loc, WrongArity (List.length tins, List.length targs)))
353 c00d0b42 ploc
  else
354 2cf39a8e xthirioux
    begin
355
      List.iter2 (fun (a,t) ti ->
356
	let t' = type_add_const env (const || Types.get_static_value ti <> None) a t
357
	in try_unify ~sub:true ti t' a.expr_loc) targs tins;
358
      touts
359
    end
360
361
(* type a simple call without dependent types 
362
   but possible homomorphic extension.
363
   [targs] is here a list of arguments' types. *)
364
and type_simple_call env in_main loc const f targs =
365
  let tins, touts = new_var (), new_var () in
366
  let tfun = Type_predef.type_arrow tins touts in
367
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
368
  (*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*)
369
  try_unify ~sub:true tins (type_of_type_list targs) loc;
370 0cbf0839 ploc
  touts
371
372
(** [type_expr env in_main expr] types expression [expr] in environment
373
    [env], expecting it to be [const] or not. *)
374
and type_expr env in_main const expr =
375 14d694c7 xthirioux
  let resulting_ty = 
376 0cbf0839 ploc
  match expr.expr_desc with
377
  | Expr_const c ->
378
    let ty = type_const expr.expr_loc c in
379
    let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in
380
    expr.expr_type <- ty;
381
    ty
382
  | Expr_ident v ->
383
    let tyv =
384
      try
385
        Env.lookup_value (fst env) v
386
      with Not_found ->
387
	Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr;
388
        raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))
389
    in
390
    let ty = instantiate (ref []) (ref []) tyv in
391
    let ty' =
392
      if const
393
      then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ())
394
      else new_var () in
395
    try_unify ty ty' expr.expr_loc;
396
    expr.expr_type <- ty;
397
    ty 
398
  | Expr_array elist ->
399 2cf39a8e xthirioux
    let ty_elt = new_var () in
400
    List.iter (fun e -> try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist;
401 0cbf0839 ploc
    let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
402
    let ty = Type_predef.type_array d ty_elt in
403
    expr.expr_type <- ty;
404
    ty
405
  | Expr_access (e1, d) ->
406
    type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
407
    let ty_elt = new_var () in
408
    let d = Dimension.mkdim_var () in
409
    type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt);
410
    expr.expr_type <- ty_elt;
411
    ty_elt
412
  | Expr_power (e1, d) ->
413
    let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
414
    type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
415
    Dimension.eval Basic_library.eval_env eval_const d;
416 2cf39a8e xthirioux
    let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in
417 0cbf0839 ploc
    let ty = Type_predef.type_array d ty_elt in
418
    expr.expr_type <- ty;
419
    ty
420
  | Expr_tuple elist ->
421
    let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in
422
    expr.expr_type <- ty;
423
    ty
424
  | Expr_ite (c, t, e) ->
425
    type_subtyping_arg env in_main const c Type_predef.type_bool;
426 2cf39a8e xthirioux
    let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in
427 0cbf0839 ploc
    expr.expr_type <- ty;
428
    ty
429
  | Expr_appl (id, args, r) ->
430 f22632aa ploc
    (* application of non internal function is not legal in a constant
431
       expression *)
432 0cbf0839 ploc
    (match r with
433
    | None        -> ()
434 f22632aa ploc
    | Some (x, l) -> 
435
      check_constant expr.expr_loc const false;
436
      let expr_x = expr_of_ident x expr.expr_loc in	
437
      let typ_l = 
438
	Type_predef.type_clock 
439
	  (type_const expr.expr_loc (Const_tag l)) in
440
      type_subtyping_arg env in_main ~sub:false const expr_x typ_l);
441 2cf39a8e xthirioux
    let touts = type_appl env in_main expr.expr_loc const id (expr_list_of_expr args) in
442 0cbf0839 ploc
    expr.expr_type <- touts;
443
    touts
444
  | Expr_fby (e1,e2)
445
  | Expr_arrow (e1,e2) ->
446
    (* fby/arrow is not legal in a constant expression *)
447
    check_constant expr.expr_loc const false;
448 2cf39a8e xthirioux
    let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in
449 0cbf0839 ploc
    expr.expr_type <- ty;
450
    ty
451
  | Expr_pre e ->
452
    (* pre is not legal in a constant expression *)
453
    check_constant expr.expr_loc const false;
454 2cf39a8e xthirioux
    let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in
455 0cbf0839 ploc
    expr.expr_type <- ty;
456
    ty
457
  | Expr_when (e1,c,l) ->
458
    (* when is not legal in a constant expression *)
459
    check_constant expr.expr_loc const false;
460
    let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in
461
    let expr_c = expr_of_ident c expr.expr_loc in
462
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
463 2cf39a8e xthirioux
    let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in
464 0cbf0839 ploc
    expr.expr_type <- ty;
465
    ty
466
  | Expr_merge (c,hl) ->
467
    (* merge is not legal in a constant expression *)
468
    check_constant expr.expr_loc const false;
469
    let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in
470
    let expr_c = expr_of_ident c expr.expr_loc in
471
    let typ_l = Type_predef.type_clock typ_in in
472
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
473
    expr.expr_type <- typ_out;
474
    typ_out
475 14d694c7 xthirioux
  in 
476
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr Types.print_ty resulting_ty);
477
  resulting_ty
478 0cbf0839 ploc
479
and type_branches env in_main loc const hl =
480
  let typ_in = new_var () in
481
  let typ_out = new_var () in
482
  try
483
    let used_labels =
484
      List.fold_left (fun accu (t, h) ->
485
	unify typ_in (type_const loc (Const_tag t));
486
	type_subtyping_arg env in_main const h typ_out;
487
	if List.mem t accu
488
	then raise (Error (loc, Already_bound t))
489
	else t :: accu) [] hl in
490
    let type_labels = get_enum_type_tags (coretype_type typ_in) in
491
    if List.sort compare used_labels <> List.sort compare type_labels
492
    then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in
493
	 raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
494
    else (typ_in, typ_out)
495
  with Unify (t1, t2) ->
496
    raise (Error (loc, Type_clash (t1,t2)))
497 2cf39a8e xthirioux
498 0cbf0839 ploc
(** [type_eq env eq] types equation [eq] in environment [env] *)
499
let type_eq env in_main undefined_vars eq =
500
  (* Check undefined variables, type lhs *)
501
  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
502
  let ty_lhs = type_expr env in_main false expr_lhs in
503
  (* Check multiple variable definitions *)
504
  let define_var id uvars =
505
    try
506
      ignore(IMap.find id uvars);
507
      IMap.remove id uvars
508
    with Not_found ->
509
      raise (Error (eq.eq_loc, Already_defined id))
510
  in
511 6b4d172f xthirioux
  (* check assignment of declared constant, assignment of clock *)
512
  let ty_lhs =
513
    type_of_type_list
514
      (List.map2 (fun ty id ->
515
	if get_static_value ty <> None
516
	then raise (Error (eq.eq_loc, Assigned_constant id)) else
517
	match get_clock_base_type ty with
518
	| None -> ty
519
	| Some ty -> ty)
520
	 (type_list_of_type ty_lhs) eq.eq_lhs) in
521 0cbf0839 ploc
  let undefined_vars =
522
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
523
  (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
524
     to a (always non-constant) lhs variable *)
525 fbda2f96 xthirioux
  type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
526 0cbf0839 ploc
  undefined_vars
527
528
529
(* [type_coreclock env ck id loc] types the type clock declaration [ck]
530
   in environment [env] *)
531
let type_coreclock env ck id loc =
532
  match ck.ck_dec_desc with
533
  | Ckdec_any | Ckdec_pclock (_,_) -> ()
534
  | Ckdec_bool cl ->
535
      let dummy_id_expr = expr_of_ident id loc in
536
      let when_expr =
537
        List.fold_left
538
          (fun expr (x, l) ->
539
                {expr_tag = new_tag ();
540
                 expr_desc= Expr_when (expr,x,l);
541
                 expr_type = new_var ();
542
                 expr_clock = Clocks.new_var true;
543
                 expr_delay = Delay.new_var ();
544
                 expr_loc=loc;
545
		 expr_annot = None})
546
          dummy_id_expr cl
547
      in
548
      ignore (type_expr env false false when_expr)
549
550
let rec check_type_declaration loc cty =
551
 match cty with
552
 | Tydec_clock ty
553
 | Tydec_array (_, ty) -> check_type_declaration loc ty
554
 | Tydec_const tname   ->
555
   if not (Hashtbl.mem type_table cty)
556
   then raise (Error (loc, Unbound_type tname));
557
 | _                   -> ()
558
559
let type_var_decl vd_env env vdecl =
560
  check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
561
  let eval_const id = Types.get_static_value (Env.lookup_value env id) in
562
  let type_dim d =
563
    begin
564
      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;
565
      Dimension.eval Basic_library.eval_env eval_const d;
566
    end in
567
  let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
568
  let ty_status =
569
    if vdecl.var_dec_const
570
    then Type_predef.type_static (Dimension.mkdim_var ()) ty
571
    else ty in
572
  let new_env = Env.add_value env vdecl.var_id ty_status in
573
  type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
574
  vdecl.var_type <- ty_status;
575
  new_env
576
577
let type_var_decl_list vd_env env l =
578
  List.fold_left (type_var_decl vd_env) env l
579
580
let type_of_vlist vars =
581
  let tyl = List.map (fun v -> v.var_type) vars in
582
  type_of_type_list tyl
583
584
let add_vdecl vd_env vdecl =
585
 if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
586
 then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
587
 else vdecl::vd_env
588
589
let check_vd_env vd_env =
590
  ignore (List.fold_left add_vdecl [] vd_env)
591
592
(** [type_node env nd loc] types node [nd] in environment env. The
593
    location is used for error reports. *)
594
let type_node env nd loc =
595
  let is_main = nd.node_id = !Options.main_node in
596
  let vd_env_ol = nd.node_outputs@nd.node_locals in
597
  let vd_env =  nd.node_inputs@vd_env_ol in
598
  check_vd_env vd_env;
599
  let init_env = env in
600
  let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
601
  let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
602
  let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
603
  let new_env = Env.overwrite env delta_env in
604
  let undefined_vars_init =
605
    List.fold_left
606
      (fun uvs v -> IMap.add v.var_id () uvs)
607
      IMap.empty vd_env_ol in
608
  let undefined_vars =
609
    List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs
610
  in
611 36454535 ploc
  (* Typing asserts *)
612
  List.iter (fun assert_ ->
613
    let assert_expr =  assert_.assert_expr in
614
    type_subtyping_arg (new_env, vd_env) is_main false assert_expr Type_predef.type_bool
615
  )  nd.node_asserts;
616
  
617 0cbf0839 ploc
  (* check that table is empty *)
618
  if (not (IMap.is_empty undefined_vars)) then
619
    raise (Error (loc, Undefined_var undefined_vars));
620
  let ty_ins = type_of_vlist nd.node_inputs in
621
  let ty_outs = type_of_vlist nd.node_outputs in
622
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
623
  generalize ty_node;
624
  (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
625
  nd.node_type <- ty_node;
626
  Env.add_value env nd.node_id ty_node
627
628
let type_imported_node env nd loc =
629
  let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
630
  let vd_env = nd.nodei_inputs@nd.nodei_outputs in
631
  check_vd_env vd_env;
632
  ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
633
  let ty_ins = type_of_vlist nd.nodei_inputs in
634
  let ty_outs = type_of_vlist nd.nodei_outputs in
635
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
636
  generalize ty_node;
637
(*
638
  if (is_polymorphic ty_node) then
639
    raise (Error (loc, Poly_imported_node nd.nodei_id));
640
*)
641
  let new_env = Env.add_value env nd.nodei_id ty_node in
642
  nd.nodei_type <- ty_node;
643
  new_env
644
645
let type_top_consts env clist =
646
  List.fold_left (fun env cdecl ->
647
    let ty = type_const cdecl.const_loc cdecl.const_value in
648
    let d =
649
      if is_dimension_type ty
650
      then dimension_of_const cdecl.const_loc cdecl.const_value
651
      else Dimension.mkdim_var () in
652
    let ty = Type_predef.type_static d ty in
653
    let new_env = Env.add_value env cdecl.const_id ty in
654
    cdecl.const_type <- ty;
655
    new_env) env clist
656
657
let type_top_decl env decl =
658
  match decl.top_decl_desc with
659 c02d255e ploc
  | Node nd -> (
660
      try
661
	type_node env nd decl.top_decl_loc
662
      with Error (loc, err) as exc -> (
663
	if !Options.global_inline then
664
	  Format.eprintf "Type error: failing node@.%a@.@?"
665
	    Printers.pp_node nd
666
	;
667
	raise exc)
668
  )
669 0cbf0839 ploc
  | ImportedNode nd ->
670
      type_imported_node env nd decl.top_decl_loc
671
  | Consts clist ->
672
      type_top_consts env clist
673 6aeb3388 xthirioux
  | Type _
674 f22632aa ploc
  | Open _  -> env
675 0cbf0839 ploc
676
let type_prog env decls =
677
try
678 f22632aa ploc
  List.fold_left type_top_decl env decls
679 0cbf0839 ploc
with Failure _ as exc -> raise exc
680
681
(* Once the Lustre program is fully typed,
682
   we must get back to the original description of dimensions,
683
   with constant parameters, instead of unifiable internal variables. *)
684
685
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types,
686
   i.e. replacing unifiable second_order variables with the original static parameters.
687
   Once restored in this formulation, dimensions may be meaningfully printed.
688
*)
689
let uneval_vdecl_generics vdecl =
690
 if vdecl.var_dec_const
691
 then
692
   match get_static_value vdecl.var_type with
693
   | None   -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)
694
   | Some d -> Dimension.uneval vdecl.var_id d
695
696
let uneval_node_generics vdecls =
697
  List.iter uneval_vdecl_generics vdecls
698
699
let uneval_top_generics decl =
700
  match decl.top_decl_desc with
701
  | Node nd ->
702
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
703
  | ImportedNode nd ->
704
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
705 6aeb3388 xthirioux
  | Consts _
706
  | Type _
707 f22632aa ploc
  | Open _  -> ()
708 0cbf0839 ploc
709
let uneval_prog_generics prog =
710
 List.iter uneval_top_generics prog
711 f22632aa ploc
712 0b78e972 xthirioux
let rec get_imported_node decls id =
713
  match decls with
714
  | [] -> assert false
715
  | decl::q ->
716
     (match decl.top_decl_desc with
717
      | ImportedNode nd when id = nd.nodei_id -> decl
718
      | _ -> get_imported_node q id)
719
720 c518d082 xthirioux
let check_env_compat header declared computed = 
721
  uneval_prog_generics header;
722 f22632aa ploc
  Env.iter declared (fun k decl_type_k -> 
723 0b78e972 xthirioux
    let computed_t = instantiate (ref []) (ref []) 
724
				 (try Env.lookup_value computed k
725
				  with Not_found ->
726
				    let loc = (get_imported_node header k).top_decl_loc in 
727
				    raise (Error (loc, Declared_but_undefined k))) in
728 8b3afe43 xthirioux
    (*Types.print_ty Format.std_formatter decl_type_k;
729
    Types.print_ty Format.std_formatter computed_t;*)
730 6b4d172f xthirioux
    try_unify ~sub:true ~semi:true decl_type_k computed_t Location.dummy_loc
731 0b78e972 xthirioux
		    )
732 6aeb3388 xthirioux
let check_typedef_top decl =
733
  match decl.top_decl_desc with
734
  | Type ty ->
735
Format.eprintf "check_typedef %a %a@." Printers.pp_var_type_dec_desc ty.ty_def_desc Printers.pp_var_type_dec_desc (Hashtbl.find type_table (Tydec_const ty.ty_def_id));
736
    if coretype_equal ty.ty_def_desc (Hashtbl.find type_table (Tydec_const ty.ty_def_id)) then ()
737
    else raise (Error (decl.top_decl_loc, Type_mismatch ty.ty_def_id))
738
  | _  -> ()
739
740
let check_typedef_compat header =
741
  List.iter check_typedef_top header
742 f22632aa ploc
743 0cbf0839 ploc
(* Local Variables: *)
744
(* compile-command:"make -C .." *)
745
(* End: *)