## lustrec / src / typing.ml @ 1411704e

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: *) |