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