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