## lustrec / src / typing.ml @ c00d0b42

History | View | Annotate | Download (28.9 KB)

1 |
(* ---------------------------------------------------------------------------- |
---|---|

2 |
* SchedMCore - A MultiCore Scheduling Framework |

3 |
* Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |

4 |
* |

5 |
* This file is part of Prelude |

6 |
* |

7 |
* Prelude is free software; you can redistribute it and/or |

8 |
* modify it under the terms of the GNU Lesser General Public License |

9 |
* as published by the Free Software Foundation ; either version 2 of |

10 |
* the License, or (at your option) any later version. |

11 |
* |

12 |
* Prelude is distributed in the hope that it will be useful, but |

13 |
* WITHOUT ANY WARRANTY ; without even the implied warranty of |

14 |
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |

15 |
* Lesser General Public License for more details. |

16 |
* |

17 |
* You should have received a copy of the GNU Lesser General Public |

18 |
* License along with this program ; if not, write to the Free Software |

19 |
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |

20 |
* USA |

21 |
*---------------------------------------------------------------------------- *) |

22 | |

23 |
(** Main typing module. Classic inference algorithm with destructive |

24 |
unification. *) |

25 | |

26 |
let debug fmt args = () (* Format.eprintf "%a" *) |

27 |
(* Though it shares similarities with the clock calculus module, no code |

28 |
is shared. Simple environments, very limited identifier scoping, no |

29 |
identifier redefinition allowed. *) |

30 | |

31 |
open Utils |

32 |
(* Yes, opening both modules is dirty as some type names will be |

33 |
overwritten, yet this makes notations far lighter.*) |

34 |
open LustreSpec |

35 |
open Corelang |

36 |
open Types |

37 |
open Format |

38 | |

39 |
let pp_typing_env fmt env = |

40 |
Env.pp_env print_ty fmt env |

41 | |

42 |
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in |

43 |
type [ty]. False otherwise. *) |

44 |
let rec occurs tvar ty = |

45 |
let ty = repr ty in |

46 |
match ty.tdesc with |

47 |
| Tvar -> ty=tvar |

48 |
| Tarrow (t1, t2) -> |

49 |
(occurs tvar t1) || (occurs tvar t2) |

50 |
| Ttuple tl -> |

51 |
List.exists (occurs tvar) tl |

52 |
| Tstruct fl -> |

53 |
List.exists (fun (f, t) -> occurs tvar t) fl |

54 |
| Tarray (_, t) |

55 |
| Tstatic (_, t) |

56 |
| Tclock t |

57 |
| Tlink t -> occurs tvar t |

58 |
| Tenum _ | Tconst _ | Tunivar | Tint | Treal | Tbool | Trat -> false |

59 | |

60 |
(** Promote monomorphic type variables to polymorphic type variables. *) |

61 |
(* Generalize by side-effects *) |

62 |
let rec generalize ty = |

63 |
match ty.tdesc with |

64 |
| Tvar -> |

65 |
(* No scopes, always generalize *) |

66 |
ty.tdesc <- Tunivar |

67 |
| Tarrow (t1,t2) -> |

68 |
generalize t1; generalize t2 |

69 |
| Ttuple tl -> |

70 |
List.iter generalize tl |

71 |
| Tstruct fl -> |

72 |
List.iter (fun (f, t) -> generalize t) fl |

73 |
| Tstatic (d, t) |

74 |
| Tarray (d, t) -> Dimension.generalize d; generalize t |

75 |
| Tclock t |

76 |
| Tlink t -> |

77 |
generalize t |

78 |
| Tenum _ | Tconst _ | Tunivar | Tint | Treal | Tbool | Trat -> () |

79 | |

80 |
(** Downgrade polymorphic type variables to monomorphic type variables *) |

81 |
let rec instantiate inst_vars inst_dim_vars ty = |

82 |
let ty = repr ty in |

83 |
match ty.tdesc with |

84 |
| Tenum _ | Tconst _ | Tvar | Tint | Treal | Tbool | Trat -> ty |

85 |
| Tarrow (t1,t2) -> |

86 |
{ty with tdesc = |

87 |
Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))} |

88 |
| Ttuple tlist -> |

89 |
{ty with tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist)} |

90 |
| Tstruct flist -> |

91 |
{ty with tdesc = Tstruct (List.map (fun (f, t) -> (f, instantiate inst_vars inst_dim_vars t)) flist)} |

92 |
| Tclock t -> |

93 |
{ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t)} |

94 |
| Tstatic (d, t) -> |

95 |
{ty with tdesc = Tstatic (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)} |

96 |
| Tarray (d, t) -> |

97 |
{ty with tdesc = Tarray (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)} |

98 |
| Tlink t -> |

99 |
(* should not happen *) |

100 |
{ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t)} |

101 |
| Tunivar -> |

102 |
try |

103 |
List.assoc ty.tid !inst_vars |

104 |
with Not_found -> |

105 |
let var = new_var () in |

106 |
inst_vars := (ty.tid, var)::!inst_vars; |

107 |
var |

108 | |

109 |
(* [type_coretype cty] types the type declaration [cty] *) |

110 |
let rec type_coretype type_dim cty = |

111 |
match (*get_repr_type*) cty with |

112 |
| Tydec_any -> new_var () |

113 |
| Tydec_int -> Type_predef.type_int |

114 |
| Tydec_real -> Type_predef.type_real |

115 |
| Tydec_float -> Type_predef.type_real |

116 |
| Tydec_bool -> Type_predef.type_bool |

117 |
| Tydec_clock ty -> Type_predef.type_clock (type_coretype type_dim ty) |

118 |
| Tydec_const c -> Type_predef.type_const c |

119 |
| Tydec_enum tl -> Type_predef.type_enum tl |

120 |
| Tydec_struct fl -> Type_predef.type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl) |

121 |
| Tydec_array (d, ty) -> |

122 |
begin |

123 |
type_dim d; |

124 |
Type_predef.type_array d (type_coretype type_dim ty) |

125 |
end |

126 | |

127 |
(* [coretype_type] is the reciprocal of [type_typecore] *) |

128 |
let rec coretype_type ty = |

129 |
match (repr ty).tdesc with |

130 |
| Tvar -> Tydec_any |

131 |
| Tint -> Tydec_int |

132 |
| Treal -> Tydec_real |

133 |
| Tbool -> Tydec_bool |

134 |
| Tconst c -> Tydec_const c |

135 |
| Tclock t -> Tydec_clock (coretype_type t) |

136 |
| Tenum tl -> Tydec_enum tl |

137 |
| Tstruct fl -> Tydec_struct (List.map (fun (f, t) -> (f, coretype_type t)) fl) |

138 |
| Tarray (d, t) -> Tydec_array (d, coretype_type t) |

139 |
| Tstatic (_, t) -> coretype_type t |

140 |
| _ -> assert false |

141 | |

142 |
let get_type_definition tname = |

143 |
try |

144 |
type_coretype (fun d -> ()) (Hashtbl.find type_table (Tydec_const tname)) |

145 |
with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname)) |

146 | |

147 |
(* Equality on ground types only *) |

148 |
(* Should be used between local variables which must have a ground type *) |

149 |
let rec eq_ground t1 t2 = |

150 |
match t1.tdesc, t2.tdesc with |

151 |
| Tint, Tint | Tbool, Tbool | Trat, Trat -> true |

152 |
| Tenum tl, Tenum tl' when tl == tl' -> true |

153 |
| Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> List.for_all2 eq_ground tl tl' |

154 |
| Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' -> List.for_all2 (fun (_, t) (_, t') -> eq_ground t t') fl fl' |

155 |
| (Tconst t, _) -> |

156 |
let def_t = get_type_definition t in |

157 |
eq_ground def_t t2 |

158 |
| (_, Tconst t) -> |

159 |
let def_t = get_type_definition t in |

160 |
eq_ground t1 def_t |

161 |
| Tarrow (t1,t2), Tarrow (t1',t2') -> eq_ground t1 t1' && eq_ground t2 t2' |

162 |
| Tclock t1', _ -> eq_ground t1' t2 |

163 |
| _, Tclock t2' -> eq_ground t1 t2' |

164 |
| Tstatic (e1, t1'), Tstatic (e2, t2') |

165 |
| Tarray (e1, t1'), Tarray (e2, t2') -> Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2' |

166 |
| _ -> false |

167 | |

168 |
(** [unify t1 t2] unifies types [t1] and [t2]. Raises [Unify |

169 |
(t1,t2)] if the types are not unifiable.*) |

170 |
(* Standard destructive unification *) |

171 |
let rec unify t1 t2 = |

172 |
let t1 = repr t1 in |

173 |
let t2 = repr t2 in |

174 |
if t1=t2 then |

175 |
() |

176 |
else |

177 |
(* No type abbreviations resolution for now *) |

178 |
match t1.tdesc,t2.tdesc with |

179 |
(* This case is not mandory but will keep "older" types *) |

180 |
| Tvar, Tvar -> |

181 |
if t1.tid < t2.tid then |

182 |
t2.tdesc <- Tlink t1 |

183 |
else |

184 |
t1.tdesc <- Tlink t2 |

185 |
| (Tvar, _) when (not (occurs t1 t2)) -> |

186 |
t1.tdesc <- Tlink t2 |

187 |
| (_,Tvar) when (not (occurs t2 t1)) -> |

188 |
t2.tdesc <- Tlink t1 |

189 |
| Tarrow (t1,t2), Tarrow (t1',t2') -> |

190 |
begin |

191 |
unify t1 t1'; |

192 |
unify t2 t2' |

193 |
end |

194 |
| Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> |

195 |
List.iter2 unify tl tl' |

196 |
| Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' -> |

197 |
List.iter2 (fun (_, t) (_, t') -> unify t t') fl fl' |

198 |
| Tclock _, Tstatic _ |

199 |
| Tstatic _, Tclock _ -> raise (Unify (t1, t2)) |

200 |
| Tclock t1', _ -> unify t1' t2 |

201 |
| _, Tclock t2' -> unify t1 t2' |

202 |
| Tint, Tint | Tbool, Tbool | Trat, Trat |

203 |
| Tunivar, _ | _, Tunivar -> () |

204 |
| (Tconst t, _) -> |

205 |
let def_t = get_type_definition t in |

206 |
unify def_t t2 |

207 |
| (_, Tconst t) -> |

208 |
let def_t = get_type_definition t in |

209 |
unify t1 def_t |

210 |
| Tenum tl, Tenum tl' when tl == tl' -> () |

211 |
| Tstatic (e1, t1'), Tstatic (e2, t2') |

212 |
| Tarray (e1, t1'), Tarray (e2, t2') -> |

213 |
begin |

214 |
unify t1' t2'; |

215 |
Dimension.eval Basic_library.eval_env (fun c -> None) e1; |

216 |
Dimension.eval Basic_library.eval_env (fun c -> None) e2; |

217 |
Dimension.unify e1 e2; |

218 |
end |

219 |
| _,_ -> raise (Unify (t1, t2)) |

220 | |

221 |
(** [semi_unify t1 t2] checks whether type [t1] is an instance of type [t2]. Raises [Unify |

222 |
(t1,t2)] if the types are not semi-unifiable.*) |

223 |
(* Standard destructive semi-unification *) |

224 |
let rec semi_unify t1 t2 = |

225 |
let t1 = repr t1 in |

226 |
let t2 = repr t2 in |

227 |
if t1=t2 then |

228 |
() |

229 |
else |

230 |
(* No type abbreviations resolution for now *) |

231 |
match t1.tdesc,t2.tdesc with |

232 |
(* This case is not mandory but will keep "older" types *) |

233 |
| Tvar, Tvar -> |

234 |
if t1.tid < t2.tid then |

235 |
t2.tdesc <- Tlink t1 |

236 |
else |

237 |
t1.tdesc <- Tlink t2 |

238 |
| (Tvar, _) -> raise (Unify (t1, t2)) |

239 |
| (_,Tvar) when (not (occurs t2 t1)) -> |

240 |
t2.tdesc <- Tlink t1 |

241 |
| Tarrow (t1,t2), Tarrow (t1',t2') -> |

242 |
begin |

243 |
semi_unify t1 t1'; |

244 |
semi_unify t2 t2' |

245 |
end |

246 |
| Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> |

247 |
List.iter2 semi_unify tl tl' |

248 |
| Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' -> |

249 |
List.iter2 (fun (_, t) (_, t') -> semi_unify t t') fl fl' |

250 |
| Tclock _, Tstatic _ |

251 |
| Tstatic _, Tclock _ -> raise (Unify (t1, t2)) |

252 |
| Tclock t1', _ -> semi_unify t1' t2 |

253 |
| _, Tclock t2' -> semi_unify t1 t2' |

254 |
| Tint, Tint | Tbool, Tbool | Trat, Trat |

255 |
| Tunivar, _ | _, Tunivar -> () |

256 |
| (Tconst t, _) -> |

257 |
let def_t = get_type_definition t in |

258 |
semi_unify def_t t2 |

259 |
| (_, Tconst t) -> |

260 |
let def_t = get_type_definition t in |

261 |
semi_unify t1 def_t |

262 |
| Tenum tl, Tenum tl' when tl == tl' -> () |

263 | |

264 |
| Tstatic (e1, t1'), Tstatic (e2, t2') |

265 |
| Tarray (e1, t1'), Tarray (e2, t2') -> |

266 |
begin |

267 |
semi_unify t1' t2'; |

268 |
Dimension.eval Basic_library.eval_env (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c)) e1; |

269 |
Dimension.eval Basic_library.eval_env (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c)) e2; |

270 |
Dimension.semi_unify e1 e2; |

271 |
end |

272 |
| _,_ -> raise (Unify (t1, t2)) |

273 | |

274 |
(* Expected type ty1, got type ty2 *) |

275 |
let try_unify ty1 ty2 loc = |

276 |
try |

277 |
unify ty1 ty2 |

278 |
with |

279 |
| Unify _ -> |

280 |
raise (Error (loc, Type_clash (ty1,ty2))) |

281 |
| Dimension.Unify _ -> |

282 |
raise (Error (loc, Type_clash (ty1,ty2))) |

283 | |

284 |
let try_semi_unify ty1 ty2 loc = |

285 |
try |

286 |
semi_unify ty1 ty2 |

287 |
with |

288 |
| Unify _ -> |

289 |
raise (Error (loc, Type_clash (ty1,ty2))) |

290 |
| Dimension.Unify _ -> |

291 |
raise (Error (loc, Type_clash (ty1,ty2))) |

292 | |

293 |
(* ty1 is a subtype of ty2 *) |

294 |
let rec sub_unify sub ty1 ty2 = |

295 |
match (repr ty1).tdesc, (repr ty2).tdesc with |

296 |
| Ttuple tl1 , Ttuple tl2 -> |

297 |
if List.length tl1 <> List.length tl2 |

298 |
then raise (Unify (ty1, ty2)) |

299 |
else List.iter2 (sub_unify sub) tl1 tl2 |

300 |
| Ttuple [t1] , _ -> sub_unify sub t1 ty2 |

301 |
| _ , Ttuple [t2] -> sub_unify sub ty1 t2 |

302 |
| Tstruct tl1 , Tstruct tl2 -> |

303 |
if List.map fst tl1 <> List.map fst tl2 |

304 |
then raise (Unify (ty1, ty2)) |

305 |
else List.iter2 (fun (_, t1) (_, t2) -> sub_unify sub t1 t2) tl1 tl2 |

306 |
| Tclock t1 , Tclock t2 -> sub_unify sub t1 t2 |

307 |
| Tclock t1 , _ when sub -> sub_unify sub t1 ty2 |

308 |
| Tstatic (d1, t1) , Tstatic (d2, t2) -> |

309 |
begin |

310 |
sub_unify sub t1 t2; |

311 |
Dimension.eval Basic_library.eval_env (fun c -> None) d1; |

312 |
Dimension.eval Basic_library.eval_env (fun c -> None) d2; |

313 |
Dimension.unify d1 d2 |

314 |
end |

315 |
| Tstatic (r_d, t1) , _ when sub -> sub_unify sub t1 ty2 |

316 |
| _ -> unify ty1 ty2 |

317 | |

318 |
let try_sub_unify sub ty1 ty2 loc = |

319 |
try |

320 |
sub_unify sub ty1 ty2 |

321 |
with |

322 |
| Unify _ -> |

323 |
raise (Error (loc, Type_clash (ty1,ty2))) |

324 |
| Dimension.Unify _ -> |

325 |
raise (Error (loc, Type_clash (ty1,ty2))) |

326 | |

327 |
let rec type_struct_const_field loc (label, c) = |

328 |
if Hashtbl.mem field_table label |

329 |
then let tydec = Hashtbl.find field_table label in |

330 |
let tydec_struct = get_struct_type_fields tydec in |

331 |
let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in |

332 |
begin |

333 |
try_unify ty_label (type_const loc c) loc; |

334 |
type_coretype (fun d -> ()) tydec |

335 |
end |

336 |
else raise (Error (loc, Unbound_value ("struct field " ^ label))) |

337 | |

338 |
and type_const loc c = |

339 |
match c with |

340 |
| Const_int _ -> Type_predef.type_int |

341 |
| Const_real _ -> Type_predef.type_real |

342 |
| Const_float _ -> Type_predef.type_real |

343 |
| Const_array ca -> let d = Dimension.mkdim_int loc (List.length ca) in |

344 |
let ty = new_var () in |

345 |
List.iter (fun e -> try_unify ty (type_const loc e) loc) ca; |

346 |
Type_predef.type_array d ty |

347 |
| Const_tag t -> |

348 |
if Hashtbl.mem tag_table t |

349 |
then type_coretype (fun d -> ()) (Hashtbl.find tag_table t) |

350 |
else raise (Error (loc, Unbound_value ("enum tag " ^ t))) |

351 |
| Const_struct fl -> |

352 |
let ty_struct = new_var () in |

353 |
begin |

354 |
let used = |

355 |
List.fold_left |

356 |
(fun acc (l, c) -> |

357 |
if List.mem l acc |

358 |
then raise (Error (loc, Already_bound ("struct field " ^ l))) |

359 |
else try_unify ty_struct (type_struct_const_field loc (l, c)) loc; l::acc) |

360 |
[] fl in |

361 |
try |

362 |
let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in |

363 |
(* List.iter (fun l -> Format.eprintf "total: %s@." l) total; |

364 |
List.iter (fun l -> Format.eprintf "used: %s@." l) used; *) |

365 |
let undef = List.find (fun l -> not (List.mem l used)) total |

366 |
in raise (Error (loc, Unbound_value ("struct field " ^ undef))) |

367 |
with Not_found -> |

368 |
ty_struct |

369 |
end |

370 | |

371 |
(* The following typing functions take as parameter an environment [env] |

372 |
and whether the element being typed is expected to be constant [const]. |

373 |
[env] is a pair composed of: |

374 |
- a map from ident to type, associating to each ident, i.e. |

375 |
variables, constants and (imported) nodes, its type including whether |

376 |
it is constant or not. This latter information helps in checking constant |

377 |
propagation policy in Lustre. |

378 |
- a vdecl list, in order to modify types of declared variables that are |

379 |
later discovered to be clocks during the typing process. |

380 |
*) |

381 |
let check_constant loc const_expected const_real = |

382 |
if const_expected && not const_real |

383 |
then raise (Error (loc, Not_a_constant)) |

384 | |

385 |
let rec type_standard_args env in_main const expr_list = |

386 |
let ty_list = List.map (fun e -> dynamic_type (type_expr env in_main const e)) expr_list in |

387 |
let ty_res = new_var () in |

388 |
List.iter2 (fun e ty -> try_unify ty_res ty e.expr_loc) expr_list ty_list; |

389 |
ty_res |

390 | |

391 |
(* emulates a subtyping relation between types t and (d : t), |

392 |
used during node applications and assignments *) |

393 |
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type = |

394 |
let loc = real_arg.expr_loc in |

395 |
let const = const || (Types.get_static_value formal_type <> None) in |

396 |
let real_type = type_expr env in_main const real_arg in |

397 |
let real_type = |

398 |
if const |

399 |
then let d = |

400 |
if is_dimension_type real_type |

401 |
then dimension_of_expr real_arg |

402 |
else Dimension.mkdim_var () in |

403 |
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in |

404 |
Dimension.eval Basic_library.eval_env eval_const d; |

405 |
let real_static_type = Type_predef.type_static d (Types.dynamic_type real_type) in |

406 |
(match Types.get_static_value real_type with |

407 |
| None -> () |

408 |
| Some d' -> try_unify real_type real_static_type loc); |

409 |
real_static_type |

410 |
else real_type in |

411 |
(*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*) |

412 |
try_sub_unify sub real_type formal_type loc |

413 | |

414 |
and type_ident env in_main loc const id = |

415 |
type_expr env in_main const (expr_of_ident id loc) |

416 | |

417 |
(* typing an application implies: |

418 |
- checking that const formal parameters match real const (maybe symbolic) arguments |

419 |
- checking type adequation between formal and real arguments |

420 |
*) |

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 |
if List.length args <> List.length tins then |

427 |
raise (Error (loc, WrongArity (List.length args, List.length tins))) |

428 |
else |

429 |
List.iter2 (type_subtyping_arg env in_main const) args tins; |

430 |
touts |

431 | |

432 |
(** [type_expr env in_main expr] types expression [expr] in environment |

433 |
[env], expecting it to be [const] or not. *) |

434 |
and type_expr env in_main const expr = |

435 |
let res = |

436 |
match expr.expr_desc with |

437 |
| Expr_const c -> |

438 |
let ty = type_const expr.expr_loc c in |

439 |
let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in |

440 |
expr.expr_type <- ty; |

441 |
ty |

442 |
| Expr_ident v -> |

443 |
let tyv = |

444 |
try |

445 |
Env.lookup_value (fst env) v |

446 |
with Not_found -> |

447 |
Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr; |

448 |
raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v))) |

449 |
in |

450 |
let ty = instantiate (ref []) (ref []) tyv in |

451 |
let ty' = |

452 |
if const |

453 |
then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ()) |

454 |
else new_var () in |

455 |
try_unify ty ty' expr.expr_loc; |

456 |
expr.expr_type <- ty; |

457 |
ty |

458 |
| Expr_array elist -> |

459 |
let ty_elt = type_standard_args env in_main const elist in |

460 |
let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in |

461 |
let ty = Type_predef.type_array d ty_elt in |

462 |
expr.expr_type <- ty; |

463 |
ty |

464 |
| Expr_access (e1, d) -> |

465 |
type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int; |

466 |
let ty_elt = new_var () in |

467 |
let d = Dimension.mkdim_var () in |

468 |
type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt); |

469 |
expr.expr_type <- ty_elt; |

470 |
ty_elt |

471 |
| Expr_power (e1, d) -> |

472 |
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in |

473 |
type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int; |

474 |
Dimension.eval Basic_library.eval_env eval_const d; |

475 |
let ty_elt = type_standard_args env in_main const [e1] in |

476 |
let ty = Type_predef.type_array d ty_elt in |

477 |
expr.expr_type <- ty; |

478 |
ty |

479 |
| Expr_tuple elist -> |

480 |
let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in |

481 |
expr.expr_type <- ty; |

482 |
ty |

483 |
| Expr_ite (c, t, e) -> |

484 |
type_subtyping_arg env in_main const c Type_predef.type_bool; |

485 |
let ty = type_standard_args env in_main const [t; e] in |

486 |
expr.expr_type <- ty; |

487 |
ty |

488 |
| Expr_appl (id, args, r) -> |

489 |
(* application of non internal function is not legal in a constant |

490 |
expression *) |

491 |
(match r with |

492 |
| None -> () |

493 |
| Some (x, l) -> |

494 |
check_constant expr.expr_loc const false; |

495 |
let expr_x = expr_of_ident x expr.expr_loc in |

496 |
let typ_l = |

497 |
Type_predef.type_clock |

498 |
(type_const expr.expr_loc (Const_tag l)) in |

499 |
type_subtyping_arg env in_main ~sub:false const expr_x typ_l); |

500 |
let touts = type_appl env in_main expr.expr_loc const id args in |

501 |
expr.expr_type <- touts; |

502 |
touts |

503 |
| Expr_fby (e1,e2) |

504 |
| Expr_arrow (e1,e2) -> |

505 |
(* fby/arrow is not legal in a constant expression *) |

506 |
check_constant expr.expr_loc const false; |

507 |
let ty = type_standard_args env in_main const [e1; e2] in |

508 |
expr.expr_type <- ty; |

509 |
ty |

510 |
| Expr_pre e -> |

511 |
(* pre is not legal in a constant expression *) |

512 |
check_constant expr.expr_loc const false; |

513 |
let ty = type_standard_args env in_main const [e] in |

514 |
expr.expr_type <- ty; |

515 |
ty |

516 |
| Expr_when (e1,c,l) -> |

517 |
(* when is not legal in a constant expression *) |

518 |
check_constant expr.expr_loc const false; |

519 |
let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in |

520 |
let expr_c = expr_of_ident c expr.expr_loc in |

521 |
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; |

522 |
update_clock env in_main c expr.expr_loc typ_l; |

523 |
let ty = type_standard_args env in_main const [e1] in |

524 |
expr.expr_type <- ty; |

525 |
ty |

526 |
| Expr_merge (c,hl) -> |

527 |
(* merge is not legal in a constant expression *) |

528 |
check_constant expr.expr_loc const false; |

529 |
let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in |

530 |
let expr_c = expr_of_ident c expr.expr_loc in |

531 |
let typ_l = Type_predef.type_clock typ_in in |

532 |
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; |

533 |
update_clock env in_main c expr.expr_loc typ_l; |

534 |
expr.expr_type <- typ_out; |

535 |
typ_out |

536 |
| Expr_uclock (e,k) | Expr_dclock (e,k) -> |

537 |
let ty = type_expr env in_main const e in |

538 |
expr.expr_type <- ty; |

539 |
ty |

540 |
| Expr_phclock (e,q) -> |

541 |
let ty = type_expr env in_main const e in |

542 |
expr.expr_type <- ty; |

543 |
ty |

544 |
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 |

545 | |

546 |
and type_branches env in_main loc const hl = |

547 |
let typ_in = new_var () in |

548 |
let typ_out = new_var () in |

549 |
try |

550 |
let used_labels = |

551 |
List.fold_left (fun accu (t, h) -> |

552 |
unify typ_in (type_const loc (Const_tag t)); |

553 |
type_subtyping_arg env in_main const h typ_out; |

554 |
if List.mem t accu |

555 |
then raise (Error (loc, Already_bound t)) |

556 |
else t :: accu) [] hl in |

557 |
let type_labels = get_enum_type_tags (coretype_type typ_in) in |

558 |
if List.sort compare used_labels <> List.sort compare type_labels |

559 |
then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in |

560 |
raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag))) |

561 |
else (typ_in, typ_out) |

562 |
with Unify (t1, t2) -> |

563 |
raise (Error (loc, Type_clash (t1,t2))) |

564 | |

565 |
and update_clock env in_main id loc typ = |

566 |
(*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*) |

567 |
try |

568 |
let vdecl = List.find (fun v -> v.var_id = id) (snd env) |

569 |
in vdecl.var_type <- typ |

570 |
with |

571 |
Not_found -> |

572 |
raise (Error (loc, Unbound_value ("clock " ^ id))) |

573 | |

574 |
(** [type_eq env eq] types equation [eq] in environment [env] *) |

575 |
let type_eq env in_main undefined_vars eq = |

576 |
(* Check undefined variables, type lhs *) |

577 |
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 |

578 |
let ty_lhs = type_expr env in_main false expr_lhs in |

579 |
(* Check multiple variable definitions *) |

580 |
let define_var id uvars = |

581 |
try |

582 |
ignore(IMap.find id uvars); |

583 |
IMap.remove id uvars |

584 |
with Not_found -> |

585 |
raise (Error (eq.eq_loc, Already_defined id)) |

586 |
in |

587 |
let undefined_vars = |

588 |
List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in |

589 |
(* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned |

590 |
to a (always non-constant) lhs variable *) |

591 |
type_subtyping_arg env in_main false eq.eq_rhs ty_lhs; |

592 |
undefined_vars |

593 | |

594 | |

595 |
(* [type_coreclock env ck id loc] types the type clock declaration [ck] |

596 |
in environment [env] *) |

597 |
let type_coreclock env ck id loc = |

598 |
match ck.ck_dec_desc with |

599 |
| Ckdec_any | Ckdec_pclock (_,_) -> () |

600 |
| Ckdec_bool cl -> |

601 |
let dummy_id_expr = expr_of_ident id loc in |

602 |
let when_expr = |

603 |
List.fold_left |

604 |
(fun expr (x, l) -> |

605 |
{expr_tag = new_tag (); |

606 |
expr_desc= Expr_when (expr,x,l); |

607 |
expr_type = new_var (); |

608 |
expr_clock = Clocks.new_var true; |

609 |
expr_delay = Delay.new_var (); |

610 |
expr_loc=loc; |

611 |
expr_annot = None}) |

612 |
dummy_id_expr cl |

613 |
in |

614 |
ignore (type_expr env false false when_expr) |

615 | |

616 |
let rec check_type_declaration loc cty = |

617 |
match cty with |

618 |
| Tydec_clock ty |

619 |
| Tydec_array (_, ty) -> check_type_declaration loc ty |

620 |
| Tydec_const tname -> |

621 |
if not (Hashtbl.mem type_table cty) |

622 |
then raise (Error (loc, Unbound_type tname)); |

623 |
| _ -> () |

624 | |

625 |
let type_var_decl vd_env env vdecl = |

626 |
check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc; |

627 |
let eval_const id = Types.get_static_value (Env.lookup_value env id) in |

628 |
let type_dim d = |

629 |
begin |

630 |
type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int; |

631 |
Dimension.eval Basic_library.eval_env eval_const d; |

632 |
end in |

633 |
let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in |

634 |
let ty_status = |

635 |
if vdecl.var_dec_const |

636 |
then Type_predef.type_static (Dimension.mkdim_var ()) ty |

637 |
else ty in |

638 |
let new_env = Env.add_value env vdecl.var_id ty_status in |

639 |
type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc; |

640 |
vdecl.var_type <- ty_status; |

641 |
new_env |

642 | |

643 |
let type_var_decl_list vd_env env l = |

644 |
List.fold_left (type_var_decl vd_env) env l |

645 | |

646 |
let type_of_vlist vars = |

647 |
let tyl = List.map (fun v -> v.var_type) vars in |

648 |
type_of_type_list tyl |

649 | |

650 |
let add_vdecl vd_env vdecl = |

651 |
if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env |

652 |
then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id)) |

653 |
else vdecl::vd_env |

654 | |

655 |
let check_vd_env vd_env = |

656 |
ignore (List.fold_left add_vdecl [] vd_env) |

657 | |

658 |
(** [type_node env nd loc] types node [nd] in environment env. The |

659 |
location is used for error reports. *) |

660 |
let type_node env nd loc = |

661 |
let is_main = nd.node_id = !Options.main_node in |

662 |
let vd_env_ol = nd.node_outputs@nd.node_locals in |

663 |
let vd_env = nd.node_inputs@vd_env_ol in |

664 |
check_vd_env vd_env; |

665 |
let init_env = env in |

666 |
let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in |

667 |
let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in |

668 |
let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in |

669 |
let new_env = Env.overwrite env delta_env in |

670 |
let undefined_vars_init = |

671 |
List.fold_left |

672 |
(fun uvs v -> IMap.add v.var_id () uvs) |

673 |
IMap.empty vd_env_ol in |

674 |
let undefined_vars = |

675 |
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs |

676 |
in |

677 |
(* check that table is empty *) |

678 |
if (not (IMap.is_empty undefined_vars)) then |

679 |
raise (Error (loc, Undefined_var undefined_vars)); |

680 |
let ty_ins = type_of_vlist nd.node_inputs in |

681 |
let ty_outs = type_of_vlist nd.node_outputs in |

682 |
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in |

683 |
generalize ty_node; |

684 |
(* TODO ? Check that no node in the hierarchy remains polymorphic ? *) |

685 |
nd.node_type <- ty_node; |

686 |
Env.add_value env nd.node_id ty_node |

687 | |

688 |
let type_imported_node env nd loc = |

689 |
let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in |

690 |
let vd_env = nd.nodei_inputs@nd.nodei_outputs in |

691 |
check_vd_env vd_env; |

692 |
ignore(type_var_decl_list vd_env new_env nd.nodei_outputs); |

693 |
let ty_ins = type_of_vlist nd.nodei_inputs in |

694 |
let ty_outs = type_of_vlist nd.nodei_outputs in |

695 |
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in |

696 |
generalize ty_node; |

697 |
(* |

698 |
if (is_polymorphic ty_node) then |

699 |
raise (Error (loc, Poly_imported_node nd.nodei_id)); |

700 |
*) |

701 |
let new_env = Env.add_value env nd.nodei_id ty_node in |

702 |
nd.nodei_type <- ty_node; |

703 |
new_env |

704 | |

705 |
let type_top_consts env clist = |

706 |
List.fold_left (fun env cdecl -> |

707 |
let ty = type_const cdecl.const_loc cdecl.const_value in |

708 |
let d = |

709 |
if is_dimension_type ty |

710 |
then dimension_of_const cdecl.const_loc cdecl.const_value |

711 |
else Dimension.mkdim_var () in |

712 |
let ty = Type_predef.type_static d ty in |

713 |
let new_env = Env.add_value env cdecl.const_id ty in |

714 |
cdecl.const_type <- ty; |

715 |
new_env) env clist |

716 | |

717 |
let type_top_decl env decl = |

718 |
match decl.top_decl_desc with |

719 |
| Node nd -> ( |

720 |
try |

721 |
type_node env nd decl.top_decl_loc |

722 |
with Error (loc, err) as exc -> ( |

723 |
if !Options.global_inline then |

724 |
Format.eprintf "Type error: failing node@.%a@.@?" |

725 |
Printers.pp_node nd |

726 |
; |

727 |
raise exc) |

728 |
) |

729 |
| ImportedNode nd -> |

730 |
type_imported_node env nd decl.top_decl_loc |

731 |
| Consts clist -> |

732 |
type_top_consts env clist |

733 |
| Open _ -> env |

734 | |

735 |
let type_prog env decls = |

736 |
try |

737 |
List.fold_left type_top_decl env decls |

738 |
with Failure _ as exc -> raise exc |

739 | |

740 |
(* Once the Lustre program is fully typed, |

741 |
we must get back to the original description of dimensions, |

742 |
with constant parameters, instead of unifiable internal variables. *) |

743 | |

744 |
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types, |

745 |
i.e. replacing unifiable second_order variables with the original static parameters. |

746 |
Once restored in this formulation, dimensions may be meaningfully printed. |

747 |
*) |

748 |
let uneval_vdecl_generics vdecl = |

749 |
if vdecl.var_dec_const |

750 |
then |

751 |
match get_static_value vdecl.var_type with |

752 |
| None -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false) |

753 |
| Some d -> Dimension.uneval vdecl.var_id d |

754 | |

755 |
let uneval_node_generics vdecls = |

756 |
List.iter uneval_vdecl_generics vdecls |

757 | |

758 |
let uneval_top_generics decl = |

759 |
match decl.top_decl_desc with |

760 |
| Node nd -> |

761 |
uneval_node_generics (nd.node_inputs @ nd.node_outputs) |

762 |
| ImportedNode nd -> |

763 |
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) |

764 |
| Consts clist -> () |

765 |
| Open _ -> () |

766 | |

767 |
let uneval_prog_generics prog = |

768 |
List.iter uneval_top_generics prog |

769 | |

770 |
let rec get_imported_node decls id = |

771 |
match decls with |

772 |
| [] -> assert false |

773 |
| decl::q -> |

774 |
(match decl.top_decl_desc with |

775 |
| ImportedNode nd when id = nd.nodei_id -> decl |

776 |
| _ -> get_imported_node q id) |

777 | |

778 |
let check_env_compat header declared computed = |

779 |
uneval_prog_generics header; |

780 |
Env.iter declared (fun k decl_type_k -> |

781 |
let computed_t = instantiate (ref []) (ref []) |

782 |
(try Env.lookup_value computed k |

783 |
with Not_found -> |

784 |
let loc = (get_imported_node header k).top_decl_loc in |

785 |
raise (Error (loc, Declared_but_undefined k))) in |

786 |
(*Types.print_ty Format.std_formatter decl_type_k; |

787 |
Types.print_ty Format.std_formatter computed_t;*) |

788 |
try_semi_unify decl_type_k computed_t Location.dummy_loc |

789 |
) |

790 | |

791 |
(* Local Variables: *) |

792 |
(* compile-command:"make -C .." *) |

793 |
(* End: *) |