lustrec / src / typing.ml @ b616fe7a
History | View | Annotate | Download (29.6 KB)
1 |
(* ---------------------------------------------------------------------------- |
---|---|
2 |
* SchedMCore - A MultiCore Scheduling Framework |
3 |
* Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
4 |
* |
5 |
* This file is part of Prelude |
6 |
* |
7 |
* Prelude is free software; you can redistribute it and/or |
8 |
* modify it under the terms of the GNU Lesser General Public License |
9 |
* as published by the Free Software Foundation ; either version 2 of |
10 |
* the License, or (at your option) any later version. |
11 |
* |
12 |
* Prelude is distributed in the hope that it will be useful, but |
13 |
* WITHOUT ANY WARRANTY ; without even the implied warranty of |
14 |
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
15 |
* Lesser General Public License for more details. |
16 |
* |
17 |
* You should have received a copy of the GNU Lesser General Public |
18 |
* License along with this program ; if not, write to the Free Software |
19 |
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
20 |
* USA |
21 |
*---------------------------------------------------------------------------- *) |
22 |
|
23 |
(** Main typing module. Classic inference algorithm with destructive |
24 |
unification. *) |
25 |
|
26 |
let debug fmt args = () (* Format.eprintf "%a" *) |
27 |
(* Though it shares similarities with the clock calculus module, no code |
28 |
is shared. Simple environments, very limited identifier scoping, no |
29 |
identifier redefinition allowed. *) |
30 |
|
31 |
open Utils |
32 |
(* Yes, opening both modules is dirty as some type names will be |
33 |
overwritten, yet this makes notations far lighter.*) |
34 |
open LustreSpec |
35 |
open Corelang |
36 |
open Types |
37 |
open Format |
38 |
|
39 |
let pp_typing_env fmt env = |
40 |
Env.pp_env print_ty fmt env |
41 |
|
42 |
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in |
43 |
type [ty]. False otherwise. *) |
44 |
let rec occurs tvar ty = |
45 |
let ty = repr ty in |
46 |
match ty.tdesc with |
47 |
| Tvar -> ty=tvar |
48 |
| Tarrow (t1, t2) -> |
49 |
(occurs tvar t1) || (occurs tvar t2) |
50 |
| Ttuple tl -> |
51 |
List.exists (occurs tvar) tl |
52 |
| Tstruct fl -> |
53 |
List.exists (fun (f, t) -> occurs tvar t) fl |
54 |
| Tarray (_, t) |
55 |
| Tstatic (_, t) |
56 |
| Tclock t |
57 |
| Tlink t -> occurs tvar t |
58 |
| Tenum _ | Tconst _ | Tunivar | Tint | Treal | Tbool | Trat -> false |
59 |
|
60 |
(** Promote monomorphic type variables to polymorphic type variables. *) |
61 |
(* Generalize by side-effects *) |
62 |
let rec generalize ty = |
63 |
match ty.tdesc with |
64 |
| Tvar -> |
65 |
(* No scopes, always generalize *) |
66 |
ty.tdesc <- Tunivar |
67 |
| Tarrow (t1,t2) -> |
68 |
generalize t1; generalize t2 |
69 |
| Ttuple tl -> |
70 |
List.iter generalize tl |
71 |
| Tstruct fl -> |
72 |
List.iter (fun (f, t) -> generalize t) fl |
73 |
| Tstatic (d, t) |
74 |
| Tarray (d, t) -> Dimension.generalize d; generalize t |
75 |
| Tclock t |
76 |
| Tlink t -> |
77 |
generalize t |
78 |
| Tenum _ | Tconst _ | Tunivar | Tint | Treal | Tbool | Trat -> () |
79 |
|
80 |
(** Downgrade polymorphic type variables to monomorphic type variables *) |
81 |
let rec instantiate inst_vars inst_dim_vars ty = |
82 |
let ty = repr ty in |
83 |
match ty.tdesc with |
84 |
| Tenum _ | Tconst _ | Tvar | Tint | Treal | Tbool | Trat -> ty |
85 |
| Tarrow (t1,t2) -> |
86 |
{ty with tdesc = |
87 |
Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))} |
88 |
| Ttuple tlist -> |
89 |
{ty with tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist)} |
90 |
| Tstruct flist -> |
91 |
{ty with tdesc = Tstruct (List.map (fun (f, t) -> (f, instantiate inst_vars inst_dim_vars t)) flist)} |
92 |
| Tclock t -> |
93 |
{ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t)} |
94 |
| Tstatic (d, t) -> |
95 |
{ty with tdesc = Tstatic (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)} |
96 |
| Tarray (d, t) -> |
97 |
{ty with tdesc = Tarray (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)} |
98 |
| Tlink t -> |
99 |
(* should not happen *) |
100 |
{ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t)} |
101 |
| Tunivar -> |
102 |
try |
103 |
List.assoc ty.tid !inst_vars |
104 |
with Not_found -> |
105 |
let var = new_var () in |
106 |
inst_vars := (ty.tid, var)::!inst_vars; |
107 |
var |
108 |
|
109 |
(* [type_coretype cty] types the type declaration [cty] *) |
110 |
let rec type_coretype type_dim cty = |
111 |
match (*get_repr_type*) cty with |
112 |
| Tydec_any -> new_var () |
113 |
| Tydec_int -> Type_predef.type_int |
114 |
| Tydec_real -> Type_predef.type_real |
115 |
| Tydec_float -> Type_predef.type_real |
116 |
| Tydec_bool -> Type_predef.type_bool |
117 |
| Tydec_clock ty -> Type_predef.type_clock (type_coretype type_dim ty) |
118 |
| Tydec_const c -> Type_predef.type_const c |
119 |
| Tydec_enum tl -> Type_predef.type_enum tl |
120 |
| Tydec_struct fl -> Type_predef.type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl) |
121 |
| Tydec_array (d, ty) -> |
122 |
begin |
123 |
type_dim d; |
124 |
Type_predef.type_array d (type_coretype type_dim ty) |
125 |
end |
126 |
|
127 |
(* [coretype_type] is the reciprocal of [type_typecore] *) |
128 |
let rec coretype_type ty = |
129 |
match (repr ty).tdesc with |
130 |
| Tvar -> Tydec_any |
131 |
| Tint -> Tydec_int |
132 |
| Treal -> Tydec_real |
133 |
| Tbool -> Tydec_bool |
134 |
| Tconst c -> Tydec_const c |
135 |
| Tclock t -> Tydec_clock (coretype_type t) |
136 |
| Tenum tl -> Tydec_enum tl |
137 |
| Tstruct fl -> Tydec_struct (List.map (fun (f, t) -> (f, coretype_type t)) fl) |
138 |
| Tarray (d, t) -> Tydec_array (d, coretype_type t) |
139 |
| Tstatic (_, t) -> coretype_type t |
140 |
| _ -> assert false |
141 |
|
142 |
let get_type_definition tname = |
143 |
try |
144 |
type_coretype (fun d -> ()) (Hashtbl.find type_table (Tydec_const tname)) |
145 |
with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname)) |
146 |
|
147 |
(* Equality on ground types only *) |
148 |
(* Should be used between local variables which must have a ground type *) |
149 |
let rec eq_ground t1 t2 = |
150 |
match t1.tdesc, t2.tdesc with |
151 |
| Tint, Tint | Tbool, Tbool | Trat, Trat -> true |
152 |
| Tenum tl, Tenum tl' when tl == tl' -> true |
153 |
| Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> List.for_all2 eq_ground tl tl' |
154 |
| Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' -> List.for_all2 (fun (_, t) (_, t') -> eq_ground t t') fl fl' |
155 |
| (Tconst t, _) -> |
156 |
let def_t = get_type_definition t in |
157 |
eq_ground def_t t2 |
158 |
| (_, Tconst t) -> |
159 |
let def_t = get_type_definition t in |
160 |
eq_ground t1 def_t |
161 |
| Tarrow (t1,t2), Tarrow (t1',t2') -> eq_ground t1 t1' && eq_ground t2 t2' |
162 |
| Tclock t1', _ -> eq_ground t1' t2 |
163 |
| _, Tclock t2' -> eq_ground t1 t2' |
164 |
| Tstatic (e1, t1'), Tstatic (e2, t2') |
165 |
| Tarray (e1, t1'), Tarray (e2, t2') -> Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2' |
166 |
| _ -> false |
167 |
|
168 |
(** [unify t1 t2] unifies types [t1] and [t2]. Raises [Unify |
169 |
(t1,t2)] if the types are not unifiable.*) |
170 |
(* Standard destructive unification *) |
171 |
let rec unify t1 t2 = |
172 |
let t1 = repr t1 in |
173 |
let t2 = repr t2 in |
174 |
if t1=t2 then |
175 |
() |
176 |
else |
177 |
(* No type abbreviations resolution for now *) |
178 |
match t1.tdesc,t2.tdesc with |
179 |
(* This case is not mandory but will keep "older" types *) |
180 |
| Tvar, Tvar -> |
181 |
if t1.tid < t2.tid then |
182 |
t2.tdesc <- Tlink t1 |
183 |
else |
184 |
t1.tdesc <- Tlink t2 |
185 |
| (Tvar, _) when (not (occurs t1 t2)) -> |
186 |
t1.tdesc <- Tlink t2 |
187 |
| (_,Tvar) when (not (occurs t2 t1)) -> |
188 |
t2.tdesc <- Tlink t1 |
189 |
| Tarrow (t1,t2), Tarrow (t1',t2') -> |
190 |
begin |
191 |
unify t1 t1'; |
192 |
unify t2 t2' |
193 |
end |
194 |
| Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> |
195 |
List.iter2 unify tl tl' |
196 |
| Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' -> |
197 |
List.iter2 (fun (_, t) (_, t') -> unify t t') fl fl' |
198 |
| Tclock _, Tstatic _ |
199 |
| Tstatic _, Tclock _ -> raise (Unify (t1, t2)) |
200 |
| Tclock t1', _ -> unify t1' t2 |
201 |
| _, Tclock t2' -> unify t1 t2' |
202 |
| Tint, Tint | Tbool, Tbool | Trat, Trat |
203 |
| Tunivar, _ | _, Tunivar -> () |
204 |
| (Tconst t, _) -> |
205 |
let def_t = get_type_definition t in |
206 |
unify def_t t2 |
207 |
| (_, Tconst t) -> |
208 |
let def_t = get_type_definition t in |
209 |
unify t1 def_t |
210 |
| Tenum tl, Tenum tl' when tl == tl' -> () |
211 |
| Tstatic (e1, t1'), Tstatic (e2, t2') |
212 |
| Tarray (e1, t1'), Tarray (e2, t2') -> |
213 |
begin |
214 |
unify t1' t2'; |
215 |
Dimension.eval Basic_library.eval_env (fun c -> None) e1; |
216 |
Dimension.eval Basic_library.eval_env (fun c -> None) e2; |
217 |
Dimension.unify e1 e2; |
218 |
end |
219 |
| _,_ -> raise (Unify (t1, t2)) |
220 |
|
221 |
(** [semi_unify t1 t2] checks whether type [t1] is an instance of type [t2]. Raises [Unify |
222 |
(t1,t2)] if the types are not semi-unifiable.*) |
223 |
(* Standard destructive semi-unification *) |
224 |
let rec semi_unify t1 t2 = |
225 |
let t1 = repr t1 in |
226 |
let t2 = repr t2 in |
227 |
if t1=t2 then |
228 |
() |
229 |
else |
230 |
(* No type abbreviations resolution for now *) |
231 |
match t1.tdesc,t2.tdesc with |
232 |
(* This case is not mandory but will keep "older" types *) |
233 |
| Tvar, Tvar -> |
234 |
if t1.tid < t2.tid then |
235 |
t2.tdesc <- Tlink t1 |
236 |
else |
237 |
t1.tdesc <- Tlink t2 |
238 |
| (Tvar, _) -> raise (Unify (t1, t2)) |
239 |
| (_,Tvar) when (not (occurs t2 t1)) -> |
240 |
t2.tdesc <- Tlink t1 |
241 |
| Tarrow (t1,t2), Tarrow (t1',t2') -> |
242 |
begin |
243 |
semi_unify t1 t1'; |
244 |
semi_unify t2 t2' |
245 |
end |
246 |
| Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> |
247 |
List.iter2 semi_unify tl tl' |
248 |
| Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' -> |
249 |
List.iter2 (fun (_, t) (_, t') -> semi_unify t t') fl fl' |
250 |
| Tclock _, Tstatic _ |
251 |
| Tstatic _, Tclock _ -> raise (Unify (t1, t2)) |
252 |
| Tclock t1', _ -> semi_unify t1' t2 |
253 |
| _, Tclock t2' -> semi_unify t1 t2' |
254 |
| Tint, Tint | Tbool, Tbool | Trat, Trat |
255 |
| Tunivar, _ | _, Tunivar -> () |
256 |
| (Tconst t, _) -> |
257 |
let def_t = get_type_definition t in |
258 |
semi_unify def_t t2 |
259 |
| (_, Tconst t) -> |
260 |
let def_t = get_type_definition t in |
261 |
semi_unify t1 def_t |
262 |
| Tenum tl, Tenum tl' when tl == tl' -> () |
263 |
|
264 |
| Tstatic (e1, t1'), Tstatic (e2, t2') |
265 |
| Tarray (e1, t1'), Tarray (e2, t2') -> |
266 |
begin |
267 |
semi_unify t1' t2'; |
268 |
Dimension.eval Basic_library.eval_env (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c)) e1; |
269 |
Dimension.eval Basic_library.eval_env (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c)) e2; |
270 |
Dimension.semi_unify e1 e2; |
271 |
end |
272 |
| _,_ -> raise (Unify (t1, t2)) |
273 |
|
274 |
(* Expected type ty1, got type ty2 *) |
275 |
let try_unify ty1 ty2 loc = |
276 |
try |
277 |
unify ty1 ty2 |
278 |
with |
279 |
| Unify _ -> |
280 |
raise (Error (loc, Type_clash (ty1,ty2))) |
281 |
| Dimension.Unify _ -> |
282 |
raise (Error (loc, Type_clash (ty1,ty2))) |
283 |
|
284 |
let try_semi_unify ty1 ty2 loc = |
285 |
try |
286 |
semi_unify ty1 ty2 |
287 |
with |
288 |
| Unify _ -> |
289 |
raise (Error (loc, Type_clash (ty1,ty2))) |
290 |
| Dimension.Unify _ -> |
291 |
raise (Error (loc, Type_clash (ty1,ty2))) |
292 |
|
293 |
(* ty1 is a subtype of ty2 *) |
294 |
let rec sub_unify sub ty1 ty2 = |
295 |
match (repr ty1).tdesc, (repr ty2).tdesc with |
296 |
| Ttuple tl1 , Ttuple tl2 -> |
297 |
if List.length tl1 <> List.length tl2 |
298 |
then raise (Unify (ty1, ty2)) |
299 |
else List.iter2 (sub_unify sub) tl1 tl2 |
300 |
| Ttuple [t1] , _ -> sub_unify sub t1 ty2 |
301 |
| _ , Ttuple [t2] -> sub_unify sub ty1 t2 |
302 |
| Tstruct tl1 , Tstruct tl2 -> |
303 |
if List.map fst tl1 <> List.map fst tl2 |
304 |
then raise (Unify (ty1, ty2)) |
305 |
else List.iter2 (fun (_, t1) (_, t2) -> sub_unify sub t1 t2) tl1 tl2 |
306 |
| Tclock t1 , Tclock t2 -> sub_unify sub t1 t2 |
307 |
| Tclock t1 , _ when sub -> sub_unify sub t1 ty2 |
308 |
| Tstatic (d1, t1) , Tstatic (d2, t2) -> |
309 |
begin |
310 |
sub_unify sub t1 t2; |
311 |
Dimension.eval Basic_library.eval_env (fun c -> None) d1; |
312 |
Dimension.eval Basic_library.eval_env (fun c -> None) d2; |
313 |
Dimension.unify d1 d2 |
314 |
end |
315 |
| Tstatic (r_d, t1) , _ when sub -> sub_unify sub t1 ty2 |
316 |
| _ -> unify ty1 ty2 |
317 |
|
318 |
let try_sub_unify sub ty1 ty2 loc = |
319 |
try |
320 |
sub_unify sub ty1 ty2 |
321 |
with |
322 |
| Unify _ -> |
323 |
raise (Error (loc, Type_clash (ty1,ty2))) |
324 |
| Dimension.Unify _ -> |
325 |
raise (Error (loc, Type_clash (ty1,ty2))) |
326 |
|
327 |
let rec type_struct_const_field loc (label, c) = |
328 |
if Hashtbl.mem field_table label |
329 |
then let tydec = Hashtbl.find field_table label in |
330 |
let tydec_struct = get_struct_type_fields tydec in |
331 |
let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in |
332 |
begin |
333 |
try_unify ty_label (type_const loc c) loc; |
334 |
type_coretype (fun d -> ()) tydec |
335 |
end |
336 |
else raise (Error (loc, Unbound_value ("struct field " ^ label))) |
337 |
|
338 |
and type_const loc c = |
339 |
match c with |
340 |
| Const_int _ -> Type_predef.type_int |
341 |
| Const_real _ -> Type_predef.type_real |
342 |
| Const_float _ -> Type_predef.type_real |
343 |
| Const_array ca -> let d = Dimension.mkdim_int loc (List.length ca) in |
344 |
let ty = new_var () in |
345 |
List.iter (fun e -> try_unify ty (type_const loc e) loc) ca; |
346 |
Type_predef.type_array d ty |
347 |
| Const_tag t -> |
348 |
if Hashtbl.mem tag_table t |
349 |
then type_coretype (fun d -> ()) (Hashtbl.find tag_table t) |
350 |
else raise (Error (loc, Unbound_value ("enum tag " ^ t))) |
351 |
| Const_struct fl -> |
352 |
let ty_struct = new_var () in |
353 |
begin |
354 |
let used = |
355 |
List.fold_left |
356 |
(fun acc (l, c) -> |
357 |
if List.mem l acc |
358 |
then raise (Error (loc, Already_bound ("struct field " ^ l))) |
359 |
else try_unify ty_struct (type_struct_const_field loc (l, c)) loc; l::acc) |
360 |
[] fl in |
361 |
try |
362 |
let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in |
363 |
(* List.iter (fun l -> Format.eprintf "total: %s@." l) total; |
364 |
List.iter (fun l -> Format.eprintf "used: %s@." l) used; *) |
365 |
let undef = List.find (fun l -> not (List.mem l used)) total |
366 |
in raise (Error (loc, Unbound_value ("struct field " ^ undef))) |
367 |
with Not_found -> |
368 |
ty_struct |
369 |
end |
370 |
|
371 |
(* The following typing functions take as parameter an environment [env] |
372 |
and whether the element being typed is expected to be constant [const]. |
373 |
[env] is a pair composed of: |
374 |
- a map from ident to type, associating to each ident, i.e. |
375 |
variables, constants and (imported) nodes, its type including whether |
376 |
it is constant or not. This latter information helps in checking constant |
377 |
propagation policy in Lustre. |
378 |
- a vdecl list, in order to modify types of declared variables that are |
379 |
later discovered to be clocks during the typing process. |
380 |
*) |
381 |
let check_constant loc const_expected const_real = |
382 |
if const_expected && not const_real |
383 |
then raise (Error (loc, Not_a_constant)) |
384 |
|
385 |
let rec type_standard_args env in_main const expr_list = |
386 |
let ty_list = List.map (fun e -> dynamic_type (type_expr env in_main const e)) expr_list in |
387 |
let ty_res = new_var () in |
388 |
List.iter2 (fun e ty -> try_unify ty_res ty e.expr_loc) expr_list ty_list; |
389 |
ty_res |
390 |
|
391 |
(* emulates a subtyping relation between types t and (d : t), |
392 |
used during node applications and assignments *) |
393 |
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type = |
394 |
let loc = real_arg.expr_loc in |
395 |
let const = const || (Types.get_static_value formal_type <> None) in |
396 |
let real_type = type_expr env in_main const real_arg in |
397 |
let real_type = |
398 |
if const |
399 |
then let d = |
400 |
if is_dimension_type real_type |
401 |
then dimension_of_expr real_arg |
402 |
else Dimension.mkdim_var () in |
403 |
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in |
404 |
Dimension.eval Basic_library.eval_env eval_const d; |
405 |
let real_static_type = Type_predef.type_static d (Types.dynamic_type real_type) in |
406 |
(match Types.get_static_value real_type with |
407 |
| None -> () |
408 |
| Some d' -> try_unify real_type real_static_type loc); |
409 |
real_static_type |
410 |
else real_type in |
411 |
(*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*) |
412 |
try_sub_unify sub real_type formal_type loc |
413 |
|
414 |
and type_ident env in_main loc const id = |
415 |
type_expr env in_main const (expr_of_ident id loc) |
416 |
|
417 |
(* typing an application implies: |
418 |
- checking that const formal parameters match real const (maybe symbolic) arguments |
419 |
- checking type adequation between formal and real arguments |
420 |
An application may embed an homomorphic/internal function, in which case we need to split |
421 |
it in many calls |
422 |
*) |
423 |
and type_appl env in_main loc const f args = |
424 |
let args = expr_list_of_expr args in |
425 |
if Basic_library.is_internal_fun f && List.exists is_tuple_expr args |
426 |
then |
427 |
try |
428 |
let args = Utils.transpose_list (List.map expr_list_of_expr args) in |
429 |
Types.type_of_type_list (List.map (type_call env in_main loc const f) args) |
430 |
with |
431 |
Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l'))) |
432 |
else |
433 |
type_call env in_main loc const f args |
434 |
|
435 |
(* type a (single) call. [args] is here a list of arguments. *) |
436 |
and type_call env in_main loc const f args = |
437 |
let tfun = type_ident env in_main loc const f in |
438 |
let tins, touts = split_arrow tfun in |
439 |
let tins = type_list_of_type tins in |
440 |
if List.length args <> List.length tins then |
441 |
raise (Error (loc, WrongArity (List.length args, List.length tins))) |
442 |
else |
443 |
List.iter2 (type_subtyping_arg env in_main const) args tins; |
444 |
touts |
445 |
|
446 |
(** [type_expr env in_main expr] types expression [expr] in environment |
447 |
[env], expecting it to be [const] or not. *) |
448 |
and type_expr env in_main const expr = |
449 |
let resulting_ty = |
450 |
match expr.expr_desc with |
451 |
| Expr_const c -> |
452 |
let ty = type_const expr.expr_loc c in |
453 |
let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in |
454 |
expr.expr_type <- ty; |
455 |
ty |
456 |
| Expr_ident v -> |
457 |
let tyv = |
458 |
try |
459 |
Env.lookup_value (fst env) v |
460 |
with Not_found -> |
461 |
Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr; |
462 |
raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v))) |
463 |
in |
464 |
let ty = instantiate (ref []) (ref []) tyv in |
465 |
let ty' = |
466 |
if const |
467 |
then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ()) |
468 |
else new_var () in |
469 |
try_unify ty ty' expr.expr_loc; |
470 |
expr.expr_type <- ty; |
471 |
ty |
472 |
| Expr_array elist -> |
473 |
let ty_elt = type_standard_args env in_main const elist in |
474 |
let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in |
475 |
let ty = Type_predef.type_array d ty_elt in |
476 |
expr.expr_type <- ty; |
477 |
ty |
478 |
| Expr_access (e1, d) -> |
479 |
type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int; |
480 |
let ty_elt = new_var () in |
481 |
let d = Dimension.mkdim_var () in |
482 |
type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt); |
483 |
expr.expr_type <- ty_elt; |
484 |
ty_elt |
485 |
| Expr_power (e1, d) -> |
486 |
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in |
487 |
type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int; |
488 |
Dimension.eval Basic_library.eval_env eval_const d; |
489 |
let ty_elt = type_standard_args env in_main const [e1] in |
490 |
let ty = Type_predef.type_array d ty_elt in |
491 |
expr.expr_type <- ty; |
492 |
ty |
493 |
| Expr_tuple elist -> |
494 |
let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in |
495 |
expr.expr_type <- ty; |
496 |
ty |
497 |
| Expr_ite (c, t, e) -> |
498 |
type_subtyping_arg env in_main const c Type_predef.type_bool; |
499 |
let ty = type_standard_args env in_main const [t; e] in |
500 |
expr.expr_type <- ty; |
501 |
ty |
502 |
| Expr_appl (id, args, r) -> |
503 |
(* application of non internal function is not legal in a constant |
504 |
expression *) |
505 |
(match r with |
506 |
| None -> () |
507 |
| Some (x, l) -> |
508 |
check_constant expr.expr_loc const false; |
509 |
let expr_x = expr_of_ident x expr.expr_loc in |
510 |
let typ_l = |
511 |
Type_predef.type_clock |
512 |
(type_const expr.expr_loc (Const_tag l)) in |
513 |
type_subtyping_arg env in_main ~sub:false const expr_x typ_l); |
514 |
let touts = type_appl env in_main expr.expr_loc const id args in |
515 |
expr.expr_type <- touts; |
516 |
touts |
517 |
| Expr_fby (e1,e2) |
518 |
| Expr_arrow (e1,e2) -> |
519 |
(* fby/arrow is not legal in a constant expression *) |
520 |
check_constant expr.expr_loc const false; |
521 |
let ty = type_standard_args env in_main const [e1; e2] in |
522 |
expr.expr_type <- ty; |
523 |
ty |
524 |
| Expr_pre e -> |
525 |
(* pre is not legal in a constant expression *) |
526 |
check_constant expr.expr_loc const false; |
527 |
let ty = type_standard_args env in_main const [e] in |
528 |
expr.expr_type <- ty; |
529 |
ty |
530 |
| Expr_when (e1,c,l) -> |
531 |
(* when is not legal in a constant expression *) |
532 |
check_constant expr.expr_loc const false; |
533 |
let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in |
534 |
let expr_c = expr_of_ident c expr.expr_loc in |
535 |
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; |
536 |
update_clock env in_main c expr.expr_loc typ_l; |
537 |
let ty = type_standard_args env in_main const [e1] in |
538 |
expr.expr_type <- ty; |
539 |
ty |
540 |
| Expr_merge (c,hl) -> |
541 |
(* merge is not legal in a constant expression *) |
542 |
check_constant expr.expr_loc const false; |
543 |
let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in |
544 |
let expr_c = expr_of_ident c expr.expr_loc in |
545 |
let typ_l = Type_predef.type_clock typ_in in |
546 |
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; |
547 |
update_clock env in_main c expr.expr_loc typ_l; |
548 |
expr.expr_type <- typ_out; |
549 |
typ_out |
550 |
| Expr_uclock (e,k) | Expr_dclock (e,k) -> |
551 |
let ty = type_expr env in_main const e in |
552 |
expr.expr_type <- ty; |
553 |
ty |
554 |
| Expr_phclock (e,q) -> |
555 |
let ty = type_expr env in_main const e in |
556 |
expr.expr_type <- ty; |
557 |
ty |
558 |
in |
559 |
Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr Types.print_ty resulting_ty); |
560 |
resulting_ty |
561 |
|
562 |
and type_branches env in_main loc const hl = |
563 |
let typ_in = new_var () in |
564 |
let typ_out = new_var () in |
565 |
try |
566 |
let used_labels = |
567 |
List.fold_left (fun accu (t, h) -> |
568 |
unify typ_in (type_const loc (Const_tag t)); |
569 |
type_subtyping_arg env in_main const h typ_out; |
570 |
if List.mem t accu |
571 |
then raise (Error (loc, Already_bound t)) |
572 |
else t :: accu) [] hl in |
573 |
let type_labels = get_enum_type_tags (coretype_type typ_in) in |
574 |
if List.sort compare used_labels <> List.sort compare type_labels |
575 |
then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in |
576 |
raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag))) |
577 |
else (typ_in, typ_out) |
578 |
with Unify (t1, t2) -> |
579 |
raise (Error (loc, Type_clash (t1,t2))) |
580 |
|
581 |
and update_clock env in_main id loc typ = |
582 |
(*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*) |
583 |
try |
584 |
let vdecl = List.find (fun v -> v.var_id = id) (snd env) |
585 |
in vdecl.var_type <- typ |
586 |
with |
587 |
Not_found -> |
588 |
raise (Error (loc, Unbound_value ("clock " ^ id))) |
589 |
|
590 |
(** [type_eq env eq] types equation [eq] in environment [env] *) |
591 |
let type_eq env in_main undefined_vars eq = |
592 |
(* Check undefined variables, type lhs *) |
593 |
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 |
594 |
let ty_lhs = type_expr env in_main false expr_lhs in |
595 |
(* Check multiple variable definitions *) |
596 |
let define_var id uvars = |
597 |
try |
598 |
ignore(IMap.find id uvars); |
599 |
IMap.remove id uvars |
600 |
with Not_found -> |
601 |
raise (Error (eq.eq_loc, Already_defined id)) |
602 |
in |
603 |
let undefined_vars = |
604 |
List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in |
605 |
(* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned |
606 |
to a (always non-constant) lhs variable *) |
607 |
type_subtyping_arg env in_main false eq.eq_rhs ty_lhs; |
608 |
undefined_vars |
609 |
|
610 |
|
611 |
(* [type_coreclock env ck id loc] types the type clock declaration [ck] |
612 |
in environment [env] *) |
613 |
let type_coreclock env ck id loc = |
614 |
match ck.ck_dec_desc with |
615 |
| Ckdec_any | Ckdec_pclock (_,_) -> () |
616 |
| Ckdec_bool cl -> |
617 |
let dummy_id_expr = expr_of_ident id loc in |
618 |
let when_expr = |
619 |
List.fold_left |
620 |
(fun expr (x, l) -> |
621 |
{expr_tag = new_tag (); |
622 |
expr_desc= Expr_when (expr,x,l); |
623 |
expr_type = new_var (); |
624 |
expr_clock = Clocks.new_var true; |
625 |
expr_delay = Delay.new_var (); |
626 |
expr_loc=loc; |
627 |
expr_annot = None}) |
628 |
dummy_id_expr cl |
629 |
in |
630 |
ignore (type_expr env false false when_expr) |
631 |
|
632 |
let rec check_type_declaration loc cty = |
633 |
match cty with |
634 |
| Tydec_clock ty |
635 |
| Tydec_array (_, ty) -> check_type_declaration loc ty |
636 |
| Tydec_const tname -> |
637 |
if not (Hashtbl.mem type_table cty) |
638 |
then raise (Error (loc, Unbound_type tname)); |
639 |
| _ -> () |
640 |
|
641 |
let type_var_decl vd_env env vdecl = |
642 |
check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc; |
643 |
let eval_const id = Types.get_static_value (Env.lookup_value env id) in |
644 |
let type_dim d = |
645 |
begin |
646 |
type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int; |
647 |
Dimension.eval Basic_library.eval_env eval_const d; |
648 |
end in |
649 |
let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in |
650 |
let ty_status = |
651 |
if vdecl.var_dec_const |
652 |
then Type_predef.type_static (Dimension.mkdim_var ()) ty |
653 |
else ty in |
654 |
let new_env = Env.add_value env vdecl.var_id ty_status in |
655 |
type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc; |
656 |
vdecl.var_type <- ty_status; |
657 |
new_env |
658 |
|
659 |
let type_var_decl_list vd_env env l = |
660 |
List.fold_left (type_var_decl vd_env) env l |
661 |
|
662 |
let type_of_vlist vars = |
663 |
let tyl = List.map (fun v -> v.var_type) vars in |
664 |
type_of_type_list tyl |
665 |
|
666 |
let add_vdecl vd_env vdecl = |
667 |
if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env |
668 |
then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id)) |
669 |
else vdecl::vd_env |
670 |
|
671 |
let check_vd_env vd_env = |
672 |
ignore (List.fold_left add_vdecl [] vd_env) |
673 |
|
674 |
(** [type_node env nd loc] types node [nd] in environment env. The |
675 |
location is used for error reports. *) |
676 |
let type_node env nd loc = |
677 |
let is_main = nd.node_id = !Options.main_node in |
678 |
let vd_env_ol = nd.node_outputs@nd.node_locals in |
679 |
let vd_env = nd.node_inputs@vd_env_ol in |
680 |
check_vd_env vd_env; |
681 |
let init_env = env in |
682 |
let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in |
683 |
let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in |
684 |
let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in |
685 |
let new_env = Env.overwrite env delta_env in |
686 |
let undefined_vars_init = |
687 |
List.fold_left |
688 |
(fun uvs v -> IMap.add v.var_id () uvs) |
689 |
IMap.empty vd_env_ol in |
690 |
let undefined_vars = |
691 |
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs |
692 |
in |
693 |
(* check that table is empty *) |
694 |
if (not (IMap.is_empty undefined_vars)) then |
695 |
raise (Error (loc, Undefined_var undefined_vars)); |
696 |
let ty_ins = type_of_vlist nd.node_inputs in |
697 |
let ty_outs = type_of_vlist nd.node_outputs in |
698 |
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in |
699 |
generalize ty_node; |
700 |
(* TODO ? Check that no node in the hierarchy remains polymorphic ? *) |
701 |
nd.node_type <- ty_node; |
702 |
Env.add_value env nd.node_id ty_node |
703 |
|
704 |
let type_imported_node env nd loc = |
705 |
let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in |
706 |
let vd_env = nd.nodei_inputs@nd.nodei_outputs in |
707 |
check_vd_env vd_env; |
708 |
ignore(type_var_decl_list vd_env new_env nd.nodei_outputs); |
709 |
let ty_ins = type_of_vlist nd.nodei_inputs in |
710 |
let ty_outs = type_of_vlist nd.nodei_outputs in |
711 |
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in |
712 |
generalize ty_node; |
713 |
(* |
714 |
if (is_polymorphic ty_node) then |
715 |
raise (Error (loc, Poly_imported_node nd.nodei_id)); |
716 |
*) |
717 |
let new_env = Env.add_value env nd.nodei_id ty_node in |
718 |
nd.nodei_type <- ty_node; |
719 |
new_env |
720 |
|
721 |
let type_top_consts env clist = |
722 |
List.fold_left (fun env cdecl -> |
723 |
let ty = type_const cdecl.const_loc cdecl.const_value in |
724 |
let d = |
725 |
if is_dimension_type ty |
726 |
then dimension_of_const cdecl.const_loc cdecl.const_value |
727 |
else Dimension.mkdim_var () in |
728 |
let ty = Type_predef.type_static d ty in |
729 |
let new_env = Env.add_value env cdecl.const_id ty in |
730 |
cdecl.const_type <- ty; |
731 |
new_env) env clist |
732 |
|
733 |
let type_top_decl env decl = |
734 |
match decl.top_decl_desc with |
735 |
| Node nd -> ( |
736 |
try |
737 |
type_node env nd decl.top_decl_loc |
738 |
with Error (loc, err) as exc -> ( |
739 |
if !Options.global_inline then |
740 |
Format.eprintf "Type error: failing node@.%a@.@?" |
741 |
Printers.pp_node nd |
742 |
; |
743 |
raise exc) |
744 |
) |
745 |
| ImportedNode nd -> |
746 |
type_imported_node env nd decl.top_decl_loc |
747 |
| Consts clist -> |
748 |
type_top_consts env clist |
749 |
| Open _ -> env |
750 |
|
751 |
let type_prog env decls = |
752 |
try |
753 |
List.fold_left type_top_decl env decls |
754 |
with Failure _ as exc -> raise exc |
755 |
|
756 |
(* Once the Lustre program is fully typed, |
757 |
we must get back to the original description of dimensions, |
758 |
with constant parameters, instead of unifiable internal variables. *) |
759 |
|
760 |
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types, |
761 |
i.e. replacing unifiable second_order variables with the original static parameters. |
762 |
Once restored in this formulation, dimensions may be meaningfully printed. |
763 |
*) |
764 |
let uneval_vdecl_generics vdecl = |
765 |
if vdecl.var_dec_const |
766 |
then |
767 |
match get_static_value vdecl.var_type with |
768 |
| None -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false) |
769 |
| Some d -> Dimension.uneval vdecl.var_id d |
770 |
|
771 |
let uneval_node_generics vdecls = |
772 |
List.iter uneval_vdecl_generics vdecls |
773 |
|
774 |
let uneval_top_generics decl = |
775 |
match decl.top_decl_desc with |
776 |
| Node nd -> |
777 |
uneval_node_generics (nd.node_inputs @ nd.node_outputs) |
778 |
| ImportedNode nd -> |
779 |
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) |
780 |
| Consts clist -> () |
781 |
| Open _ -> () |
782 |
|
783 |
let uneval_prog_generics prog = |
784 |
List.iter uneval_top_generics prog |
785 |
|
786 |
let rec get_imported_node 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 |
792 |
| _ -> get_imported_node q id) |
793 |
|
794 |
let check_env_compat header declared computed = |
795 |
uneval_prog_generics header; |
796 |
Env.iter declared (fun k decl_type_k -> |
797 |
let computed_t = instantiate (ref []) (ref []) |
798 |
(try Env.lookup_value computed k |
799 |
with Not_found -> |
800 |
let loc = (get_imported_node header k).top_decl_loc in |
801 |
raise (Error (loc, Declared_but_undefined k))) in |
802 |
(*Types.print_ty Format.std_formatter decl_type_k; |
803 |
Types.print_ty Format.std_formatter computed_t;*) |
804 |
try_semi_unify decl_type_k computed_t Location.dummy_loc |
805 |
) |
806 |
|
807 |
(* Local Variables: *) |
808 |
(* compile-command:"make -C .." *) |
809 |
(* End: *) |