lustrec / src / typing.ml @ d4807c3d
History | View | Annotate | Download (28.4 KB)
1 | 22fe1c93 | ploc | (* ---------------------------------------------------------------------------- |
---|---|---|---|
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 | 12af4908 | xthirioux | List.exists (occurs tvar) tl |
52 | | Tstruct fl -> |
||
53 | List.exists (fun (f, t) -> occurs tvar t) fl |
||
54 | 22fe1c93 | ploc | | 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 | 12af4908 | xthirioux | | Ttuple tl -> |
70 | List.iter generalize tl |
||
71 | | Tstruct fl -> |
||
72 | List.iter (fun (f, t) -> generalize t) fl |
||
73 | 22fe1c93 | ploc | | 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 | 12af4908 | xthirioux | | Tstruct flist -> |
91 | {ty with tdesc = Tstruct (List.map (fun (f, t) -> (f, instantiate inst_vars inst_dim_vars t)) flist)} |
||
92 | 22fe1c93 | ploc | | 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 | 12af4908 | xthirioux | | Tydec_struct fl -> Type_predef.type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl) |
121 | 22fe1c93 | ploc | | 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 | 21485807 | xthirioux | (* [coretype_type] is the reciprocal of [type_typecore] *) |
128 | 22fe1c93 | ploc | 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 | 12af4908 | xthirioux | | Tstruct fl -> Tydec_struct (List.map (fun (f, t) -> (f, coretype_type t)) fl) |
138 | 22fe1c93 | ploc | | 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 | 695d6f2f | xthirioux | (* 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 | 7a47b44f | xthirioux | (** [unify t1 t2] unifies types [t1] and [t2]. Raises [Unify |
169 | 22fe1c93 | ploc | (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 | 12af4908 | xthirioux | | 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 | 22fe1c93 | ploc | | 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 | b3381ae8 | xthirioux | Dimension.eval Basic_library.eval_env (fun c -> None) e2; |
217 | 22fe1c93 | ploc | Dimension.unify e1 e2; |
218 | end |
||
219 | | _,_ -> raise (Unify (t1, t2)) |
||
220 | |||
221 | 7a47b44f | xthirioux | (** [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 | 7291cb80 | xthirioux | semi_unify t1 t1'; |
244 | semi_unify t2 t2' |
||
245 | 7a47b44f | xthirioux | end |
246 | 12af4908 | xthirioux | | 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 | 7a47b44f | xthirioux | | 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 | 12af4908 | xthirioux | |
264 | 7a47b44f | xthirioux | | Tstatic (e1, t1'), Tstatic (e2, t2') |
265 | | Tarray (e1, t1'), Tarray (e2, t2') -> |
||
266 | begin |
||
267 | semi_unify t1' t2'; |
||
268 | 7291cb80 | xthirioux | 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 | 7a47b44f | xthirioux | Dimension.semi_unify e1 e2; |
271 | end |
||
272 | | _,_ -> raise (Unify (t1, t2)) |
||
273 | |||
274 | 12af4908 | xthirioux | (* Expected type ty1, got type ty2 *) |
275 | 22fe1c93 | ploc | 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 | 7291cb80 | xthirioux | 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 | 12af4908 | xthirioux | (* 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 | 52cfee34 | xthirioux | | Tclock t1 , Tclock t2 -> sub_unify sub t1 t2 |
307 | | Tclock t1 , _ when sub -> sub_unify sub t1 ty2 |
||
308 | 12af4908 | xthirioux | | 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 | 52cfee34 | xthirioux | | Tstatic (r_d, t1) , _ when sub -> sub_unify sub t1 ty2 |
316 | | _ -> unify ty1 ty2 |
||
317 | 12af4908 | xthirioux | |
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 | 21485807 | xthirioux | let rec type_struct_const_field loc (label, c) = |
328 | 12af4908 | xthirioux | 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 | 21485807 | xthirioux | try_unify ty_label (type_const loc c) loc; |
334 | 12af4908 | xthirioux | type_coretype (fun d -> ()) tydec |
335 | end |
||
336 | else raise (Error (loc, Unbound_value ("struct field " ^ label))) |
||
337 | |||
338 | 21485807 | xthirioux | and type_const loc c = |
339 | 22fe1c93 | ploc | match c with |
340 | 12af4908 | xthirioux | | 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 | 22fe1c93 | ploc | let ty = new_var () in |
345 | 12af4908 | xthirioux | List.iter (fun e -> try_unify ty (type_const loc e) loc) ca; |
346 | 22fe1c93 | ploc | Type_predef.type_array d ty |
347 | 12af4908 | xthirioux | | Const_tag t -> |
348 | 22fe1c93 | ploc | 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 | 12af4908 | xthirioux | | Const_struct fl -> |
352 | let ty_struct = new_var () in |
||
353 | begin |
||
354 | 21485807 | xthirioux | 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 | 12af4908 | xthirioux | end |
370 | 22fe1c93 | ploc | |
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 | 4a840259 | xthirioux | used during node applications and assignments *) |
393 | 22fe1c93 | ploc | 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 | 52cfee34 | 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;*) |
412 | 12af4908 | xthirioux | try_sub_unify sub real_type formal_type loc |
413 | 52cfee34 | xthirioux | |
414 | 22fe1c93 | ploc | 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 | *) |
||
421 | and type_appl env in_main loc const f args = |
||
422 | let tfun = type_ident env in_main loc const f in |
||
423 | let tins, touts = split_arrow tfun in |
||
424 | let tins = type_list_of_type tins in |
||
425 | let args = expr_list_of_expr args in |
||
426 | List.iter2 (type_subtyping_arg env in_main const) args tins; |
||
427 | touts |
||
428 | |||
429 | (** [type_expr env in_main expr] types expression [expr] in environment |
||
430 | [env], expecting it to be [const] or not. *) |
||
431 | and type_expr env in_main const expr = |
||
432 | let res = |
||
433 | match expr.expr_desc with |
||
434 | | Expr_const c -> |
||
435 | let ty = type_const expr.expr_loc c in |
||
436 | let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in |
||
437 | expr.expr_type <- ty; |
||
438 | ty |
||
439 | | Expr_ident v -> |
||
440 | let tyv = |
||
441 | try |
||
442 | Env.lookup_value (fst env) v |
||
443 | with Not_found -> |
||
444 | Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr; |
||
445 | raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v))) |
||
446 | in |
||
447 | let ty = instantiate (ref []) (ref []) tyv in |
||
448 | let ty' = |
||
449 | if const |
||
450 | then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ()) |
||
451 | else new_var () in |
||
452 | try_unify ty ty' expr.expr_loc; |
||
453 | expr.expr_type <- ty; |
||
454 | ty |
||
455 | | Expr_array elist -> |
||
456 | let ty_elt = type_standard_args env in_main const elist in |
||
457 | let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in |
||
458 | let ty = Type_predef.type_array d ty_elt in |
||
459 | expr.expr_type <- ty; |
||
460 | ty |
||
461 | | Expr_access (e1, d) -> |
||
462 | type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int; |
||
463 | let ty_elt = new_var () in |
||
464 | let d = Dimension.mkdim_var () in |
||
465 | type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt); |
||
466 | expr.expr_type <- ty_elt; |
||
467 | ty_elt |
||
468 | | Expr_power (e1, d) -> |
||
469 | let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in |
||
470 | type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int; |
||
471 | Dimension.eval Basic_library.eval_env eval_const d; |
||
472 | let ty_elt = type_standard_args env in_main const [e1] in |
||
473 | let ty = Type_predef.type_array d ty_elt in |
||
474 | expr.expr_type <- ty; |
||
475 | ty |
||
476 | | Expr_tuple elist -> |
||
477 | let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in |
||
478 | expr.expr_type <- ty; |
||
479 | ty |
||
480 | | Expr_ite (c, t, e) -> |
||
481 | type_subtyping_arg env in_main const c Type_predef.type_bool; |
||
482 | let ty = type_standard_args env in_main const [t; e] in |
||
483 | expr.expr_type <- ty; |
||
484 | ty |
||
485 | | Expr_appl (id, args, r) -> |
||
486 | 5c1184ad | ploc | (* application of non internal function is not legal in a constant |
487 | expression *) |
||
488 | 22fe1c93 | ploc | (match r with |
489 | | None -> () |
||
490 | 5c1184ad | ploc | | Some (x, l) -> |
491 | check_constant expr.expr_loc const false; |
||
492 | let expr_x = expr_of_ident x expr.expr_loc in |
||
493 | let typ_l = |
||
494 | Type_predef.type_clock |
||
495 | (type_const expr.expr_loc (Const_tag l)) in |
||
496 | type_subtyping_arg env in_main ~sub:false const expr_x typ_l); |
||
497 | 22fe1c93 | ploc | let touts = type_appl env in_main expr.expr_loc const id args in |
498 | expr.expr_type <- touts; |
||
499 | touts |
||
500 | | Expr_fby (e1,e2) |
||
501 | | Expr_arrow (e1,e2) -> |
||
502 | (* fby/arrow is not legal in a constant expression *) |
||
503 | check_constant expr.expr_loc const false; |
||
504 | let ty = type_standard_args env in_main const [e1; e2] in |
||
505 | expr.expr_type <- ty; |
||
506 | ty |
||
507 | | Expr_pre e -> |
||
508 | (* pre is not legal in a constant expression *) |
||
509 | check_constant expr.expr_loc const false; |
||
510 | let ty = type_standard_args env in_main const [e] in |
||
511 | expr.expr_type <- ty; |
||
512 | ty |
||
513 | | Expr_when (e1,c,l) -> |
||
514 | (* when is not legal in a constant expression *) |
||
515 | check_constant expr.expr_loc const false; |
||
516 | let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in |
||
517 | let expr_c = expr_of_ident c expr.expr_loc in |
||
518 | type_subtyping_arg env in_main ~sub:false const expr_c typ_l; |
||
519 | update_clock env in_main c expr.expr_loc typ_l; |
||
520 | let ty = type_standard_args env in_main const [e1] in |
||
521 | expr.expr_type <- ty; |
||
522 | ty |
||
523 | | Expr_merge (c,hl) -> |
||
524 | (* merge is not legal in a constant expression *) |
||
525 | check_constant expr.expr_loc const false; |
||
526 | let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in |
||
527 | let expr_c = expr_of_ident c expr.expr_loc in |
||
528 | let typ_l = Type_predef.type_clock typ_in in |
||
529 | type_subtyping_arg env in_main ~sub:false const expr_c typ_l; |
||
530 | update_clock env in_main c expr.expr_loc typ_l; |
||
531 | expr.expr_type <- typ_out; |
||
532 | typ_out |
||
533 | | Expr_uclock (e,k) | Expr_dclock (e,k) -> |
||
534 | let ty = type_expr env in_main const e in |
||
535 | expr.expr_type <- ty; |
||
536 | ty |
||
537 | | Expr_phclock (e,q) -> |
||
538 | let ty = type_expr env in_main const e in |
||
539 | expr.expr_type <- ty; |
||
540 | ty |
||
541 | in (*Format.eprintf "typing %B %a at %a = %a@." const Printers.pp_expr expr Location.pp_loc expr.expr_loc Types.print_ty res;*) res |
||
542 | |||
543 | and type_branches env in_main loc const hl = |
||
544 | let typ_in = new_var () in |
||
545 | let typ_out = new_var () in |
||
546 | try |
||
547 | let used_labels = |
||
548 | List.fold_left (fun accu (t, h) -> |
||
549 | unify typ_in (type_const loc (Const_tag t)); |
||
550 | type_subtyping_arg env in_main const h typ_out; |
||
551 | if List.mem t accu |
||
552 | then raise (Error (loc, Already_bound t)) |
||
553 | else t :: accu) [] hl in |
||
554 | let type_labels = get_enum_type_tags (coretype_type typ_in) in |
||
555 | if List.sort compare used_labels <> List.sort compare type_labels |
||
556 | then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in |
||
557 | raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag))) |
||
558 | else (typ_in, typ_out) |
||
559 | with Unify (t1, t2) -> |
||
560 | raise (Error (loc, Type_clash (t1,t2))) |
||
561 | |||
562 | and update_clock env in_main id loc typ = |
||
563 | (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*) |
||
564 | try |
||
565 | let vdecl = List.find (fun v -> v.var_id = id) (snd env) |
||
566 | in vdecl.var_type <- typ |
||
567 | with |
||
568 | Not_found -> |
||
569 | raise (Error (loc, Unbound_value ("clock " ^ id))) |
||
570 | |||
571 | (** [type_eq env eq] types equation [eq] in environment [env] *) |
||
572 | let type_eq env in_main undefined_vars eq = |
||
573 | (* Check undefined variables, type lhs *) |
||
574 | 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 |
||
575 | let ty_lhs = type_expr env in_main false expr_lhs in |
||
576 | (* Check multiple variable definitions *) |
||
577 | let define_var id uvars = |
||
578 | try |
||
579 | ignore(IMap.find id uvars); |
||
580 | IMap.remove id uvars |
||
581 | with Not_found -> |
||
582 | raise (Error (eq.eq_loc, Already_defined id)) |
||
583 | in |
||
584 | let undefined_vars = |
||
585 | List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in |
||
586 | (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned |
||
587 | to a (always non-constant) lhs variable *) |
||
588 | 11242500 | xthirioux | type_subtyping_arg env in_main false eq.eq_rhs ty_lhs; |
589 | 22fe1c93 | ploc | undefined_vars |
590 | |||
591 | |||
592 | (* [type_coreclock env ck id loc] types the type clock declaration [ck] |
||
593 | in environment [env] *) |
||
594 | let type_coreclock env ck id loc = |
||
595 | match ck.ck_dec_desc with |
||
596 | | Ckdec_any | Ckdec_pclock (_,_) -> () |
||
597 | | Ckdec_bool cl -> |
||
598 | let dummy_id_expr = expr_of_ident id loc in |
||
599 | let when_expr = |
||
600 | List.fold_left |
||
601 | (fun expr (x, l) -> |
||
602 | {expr_tag = new_tag (); |
||
603 | expr_desc= Expr_when (expr,x,l); |
||
604 | expr_type = new_var (); |
||
605 | expr_clock = Clocks.new_var true; |
||
606 | expr_delay = Delay.new_var (); |
||
607 | expr_loc=loc; |
||
608 | expr_annot = None}) |
||
609 | dummy_id_expr cl |
||
610 | in |
||
611 | ignore (type_expr env false false when_expr) |
||
612 | |||
613 | let rec check_type_declaration loc cty = |
||
614 | match cty with |
||
615 | | Tydec_clock ty |
||
616 | | Tydec_array (_, ty) -> check_type_declaration loc ty |
||
617 | | Tydec_const tname -> |
||
618 | if not (Hashtbl.mem type_table cty) |
||
619 | then raise (Error (loc, Unbound_type tname)); |
||
620 | | _ -> () |
||
621 | |||
622 | let type_var_decl vd_env env vdecl = |
||
623 | check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc; |
||
624 | let eval_const id = Types.get_static_value (Env.lookup_value env id) in |
||
625 | let type_dim d = |
||
626 | begin |
||
627 | type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int; |
||
628 | Dimension.eval Basic_library.eval_env eval_const d; |
||
629 | end in |
||
630 | let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in |
||
631 | let ty_status = |
||
632 | if vdecl.var_dec_const |
||
633 | then Type_predef.type_static (Dimension.mkdim_var ()) ty |
||
634 | else ty in |
||
635 | let new_env = Env.add_value env vdecl.var_id ty_status in |
||
636 | type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc; |
||
637 | vdecl.var_type <- ty_status; |
||
638 | new_env |
||
639 | |||
640 | let type_var_decl_list vd_env env l = |
||
641 | List.fold_left (type_var_decl vd_env) env l |
||
642 | |||
643 | let type_of_vlist vars = |
||
644 | let tyl = List.map (fun v -> v.var_type) vars in |
||
645 | type_of_type_list tyl |
||
646 | |||
647 | let add_vdecl vd_env vdecl = |
||
648 | if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env |
||
649 | then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id)) |
||
650 | else vdecl::vd_env |
||
651 | |||
652 | let check_vd_env vd_env = |
||
653 | ignore (List.fold_left add_vdecl [] vd_env) |
||
654 | |||
655 | (** [type_node env nd loc] types node [nd] in environment env. The |
||
656 | location is used for error reports. *) |
||
657 | let type_node env nd loc = |
||
658 | let is_main = nd.node_id = !Options.main_node in |
||
659 | let vd_env_ol = nd.node_outputs@nd.node_locals in |
||
660 | let vd_env = nd.node_inputs@vd_env_ol in |
||
661 | check_vd_env vd_env; |
||
662 | let init_env = env in |
||
663 | let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in |
||
664 | let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in |
||
665 | let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in |
||
666 | let new_env = Env.overwrite env delta_env in |
||
667 | let undefined_vars_init = |
||
668 | List.fold_left |
||
669 | (fun uvs v -> IMap.add v.var_id () uvs) |
||
670 | IMap.empty vd_env_ol in |
||
671 | let undefined_vars = |
||
672 | List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs |
||
673 | in |
||
674 | (* check that table is empty *) |
||
675 | if (not (IMap.is_empty undefined_vars)) then |
||
676 | raise (Error (loc, Undefined_var undefined_vars)); |
||
677 | let ty_ins = type_of_vlist nd.node_inputs in |
||
678 | let ty_outs = type_of_vlist nd.node_outputs in |
||
679 | let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in |
||
680 | generalize ty_node; |
||
681 | (* TODO ? Check that no node in the hierarchy remains polymorphic ? *) |
||
682 | nd.node_type <- ty_node; |
||
683 | Env.add_value env nd.node_id ty_node |
||
684 | |||
685 | let type_imported_node env nd loc = |
||
686 | let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in |
||
687 | let vd_env = nd.nodei_inputs@nd.nodei_outputs in |
||
688 | check_vd_env vd_env; |
||
689 | ignore(type_var_decl_list vd_env new_env nd.nodei_outputs); |
||
690 | let ty_ins = type_of_vlist nd.nodei_inputs in |
||
691 | let ty_outs = type_of_vlist nd.nodei_outputs in |
||
692 | let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in |
||
693 | generalize ty_node; |
||
694 | (* |
||
695 | if (is_polymorphic ty_node) then |
||
696 | raise (Error (loc, Poly_imported_node nd.nodei_id)); |
||
697 | *) |
||
698 | let new_env = Env.add_value env nd.nodei_id ty_node in |
||
699 | nd.nodei_type <- ty_node; |
||
700 | new_env |
||
701 | |||
702 | let type_top_consts env clist = |
||
703 | List.fold_left (fun env cdecl -> |
||
704 | let ty = type_const cdecl.const_loc cdecl.const_value in |
||
705 | let d = |
||
706 | if is_dimension_type ty |
||
707 | then dimension_of_const cdecl.const_loc cdecl.const_value |
||
708 | else Dimension.mkdim_var () in |
||
709 | let ty = Type_predef.type_static d ty in |
||
710 | let new_env = Env.add_value env cdecl.const_id ty in |
||
711 | cdecl.const_type <- ty; |
||
712 | new_env) env clist |
||
713 | |||
714 | let type_top_decl env decl = |
||
715 | match decl.top_decl_desc with |
||
716 | e2380d4d | ploc | | Node nd -> ( |
717 | try |
||
718 | type_node env nd decl.top_decl_loc |
||
719 | with Error (loc, err) as exc -> ( |
||
720 | if !Options.global_inline then |
||
721 | Format.eprintf "Type error: failing node@.%a@.@?" |
||
722 | Printers.pp_node nd |
||
723 | ; |
||
724 | raise exc) |
||
725 | ) |
||
726 | 22fe1c93 | ploc | | ImportedNode nd -> |
727 | type_imported_node env nd decl.top_decl_loc |
||
728 | | Consts clist -> |
||
729 | type_top_consts env clist |
||
730 | 5c1184ad | ploc | | Open _ -> env |
731 | 22fe1c93 | ploc | |
732 | let type_prog env decls = |
||
733 | try |
||
734 | 5c1184ad | ploc | List.fold_left type_top_decl env decls |
735 | 22fe1c93 | ploc | with Failure _ as exc -> raise exc |
736 | |||
737 | (* Once the Lustre program is fully typed, |
||
738 | we must get back to the original description of dimensions, |
||
739 | with constant parameters, instead of unifiable internal variables. *) |
||
740 | |||
741 | (* The following functions aims at 'unevaluating' dimension expressions occuring in array types, |
||
742 | i.e. replacing unifiable second_order variables with the original static parameters. |
||
743 | Once restored in this formulation, dimensions may be meaningfully printed. |
||
744 | *) |
||
745 | let uneval_vdecl_generics vdecl = |
||
746 | if vdecl.var_dec_const |
||
747 | then |
||
748 | match get_static_value vdecl.var_type with |
||
749 | | None -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false) |
||
750 | | Some d -> Dimension.uneval vdecl.var_id d |
||
751 | |||
752 | let uneval_node_generics vdecls = |
||
753 | List.iter uneval_vdecl_generics vdecls |
||
754 | |||
755 | let uneval_top_generics decl = |
||
756 | match decl.top_decl_desc with |
||
757 | | Node nd -> |
||
758 | uneval_node_generics (nd.node_inputs @ nd.node_outputs) |
||
759 | | ImportedNode nd -> |
||
760 | uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) |
||
761 | | Consts clist -> () |
||
762 | 5c1184ad | ploc | | Open _ -> () |
763 | 22fe1c93 | ploc | |
764 | let uneval_prog_generics prog = |
||
765 | List.iter uneval_top_generics prog |
||
766 | 5c1184ad | ploc | |
767 | 8f1c7e91 | xthirioux | let check_env_compat header declared computed = |
768 | uneval_prog_generics header; |
||
769 | 5c1184ad | ploc | Env.iter declared (fun k decl_type_k -> |
770 | 7291cb80 | xthirioux | let computed_t = instantiate (ref []) (ref []) (Env.lookup_value computed k) in |
771 | (*Types.print_ty Format.std_formatter decl_type_k; |
||
772 | Types.print_ty Format.std_formatter computed_t;*) |
||
773 | try_semi_unify decl_type_k computed_t Location.dummy_loc |
||
774 | 5c1184ad | ploc | ) |
775 | |||
776 | 22fe1c93 | ploc | (* Local Variables: *) |
777 | (* compile-command:"make -C .." *) |
||
778 | (* End: *) |