## lustrec / src / typing.ml @ ef34b4ae

History | View | Annotate | Download (29.2 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 | | Tydec_float -> Type_predef.type_real |
||

107 | | 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 | type_dim d; |
||

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

116 | end |
||

117 | |||

118 | 21485807 | xthirioux | (* [coretype_type] is the reciprocal of [type_typecore] *) |

119 | 22fe1c93 | ploc | let rec coretype_type ty = |

120 | match (repr ty).tdesc with |
||

121 | | Tvar -> Tydec_any |
||

122 | | Tint -> Tydec_int |
||

123 | | Treal -> Tydec_real |
||

124 | | Tbool -> Tydec_bool |
||

125 | | Tconst c -> Tydec_const c |
||

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

127 | | Tenum tl -> Tydec_enum tl |
||

128 | 12af4908 | xthirioux | | Tstruct fl -> Tydec_struct (List.map (fun (f, t) -> (f, coretype_type t)) fl) |

129 | 22fe1c93 | ploc | | Tarray (d, t) -> Tydec_array (d, coretype_type t) |

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

131 | | _ -> assert false |
||

132 | |||

133 | ef34b4ae | xthirioux | let get_coretype_definition tname = |

134 | 22fe1c93 | ploc | try |

135 | ef34b4ae | xthirioux | let top = Hashtbl.find type_table (Tydec_const tname) in |

136 | match top.top_decl_desc with |
||

137 | | TypeDef tdef -> tdef.tydef_desc |
||

138 | | _ -> assert false |
||

139 | 22fe1c93 | ploc | with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname)) |

140 | |||

141 | ef34b4ae | xthirioux | let get_type_definition tname = |

142 | type_coretype (fun d -> ()) (get_coretype_definition tname) |
||

143 | |||

144 | 695d6f2f | xthirioux | (* Equality on ground types only *) |

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

146 | let rec eq_ground t1 t2 = |
||

147 | 28c58de1 | xthirioux | let t1 = repr t1 in |

148 | let t2 = repr t2 in |
||

149 | t1==t2 || |
||

150 | 695d6f2f | xthirioux | match t1.tdesc, t2.tdesc with |

151 | 8a183477 | xthirioux | | Tint, Tint | Tbool, Tbool | Trat, Trat | Treal, Treal -> true |

152 | 695d6f2f | xthirioux | | 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 | 6afa892a | xthirioux | | Tclock t1', Tclock t2' -> eq_ground t1' t2' |

163 | 695d6f2f | xthirioux | | Tstatic (e1, t1'), Tstatic (e2, t2') |

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

165 | | _ -> false |
||

166 | |||

167 | 6afa892a | xthirioux | (** [unify t1 t2] unifies types [t1] and [t2] |

168 | using standard destructive unification. |
||

169 | Raises [Unify (t1,t2)] if the types are not unifiable. |
||

170 | [t1] is a expected/formal/spec type, [t2] is a computed/real/implem type, |
||

171 | so in case of unification error: expected type [t1], got type [t2]. |
||

172 | If [sub]-typing is allowed, [t2] may be a subtype of [t1]. |
||

173 | If [semi] unification is required, |
||

174 | [t1] should furthermore be an instance of [t2] |
||

175 | and constants are handled differently.*) |
||

176 | let unify ?(sub=false) ?(semi=false) t1 t2 = |
||

177 | let rec unif t1 t2 = |
||

178 | let t1 = repr t1 in |
||

179 | let t2 = repr t2 in |
||

180 | 8a183477 | xthirioux | if t1==t2 then |

181 | 6afa892a | xthirioux | () |

182 | else |
||

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

184 | (* strictly subtyping cases first *) |
||

185 | | _ , Tclock t2 when sub && (get_clock_base_type t1 = None) -> |
||

186 | unif t1 t2 |
||

187 | | _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) -> |
||

188 | unif t1 t2 |
||

189 | (* This case is not mandatory but will keep "older" types *) |
||

190 | | Tvar, Tvar -> |
||

191 | 22fe1c93 | ploc | if t1.tid < t2.tid then |

192 | t2.tdesc <- Tlink t1 |
||

193 | else |
||

194 | t1.tdesc <- Tlink t2 |
||

195 | 6afa892a | xthirioux | | Tvar, _ when (not semi) && (not (occurs t1 t2)) -> |

196 | 22fe1c93 | ploc | t1.tdesc <- Tlink t2 |

197 | 6afa892a | xthirioux | | _, Tvar when (not (occurs t2 t1)) -> |

198 | 7a47b44f | xthirioux | t2.tdesc <- Tlink t1 |

199 | 6afa892a | xthirioux | | Tarrow (t1,t2), Tarrow (t1',t2') -> |

200 | begin |
||

201 | unif t2 t2'; |
||

202 | unif t1' t1 |
||

203 | end |
||

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

205 | List.iter2 unif tl tl' |
||

206 | | Ttuple [t1] , _ -> unif t1 t2 |
||

207 | | _ , Ttuple [t2] -> unif t1 t2 |
||

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

209 | List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl' |
||

210 | | Tclock _, Tstatic _ |
||

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

212 | | Tclock t1', Tclock t2' -> unif t1' t2' |
||

213 | 8a183477 | xthirioux | | Tint, Tint | Tbool, Tbool | Trat, Trat | Treal, Treal |

214 | 6afa892a | xthirioux | | Tunivar, _ | _, Tunivar -> () |

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

216 | let def_t = get_type_definition t in |
||

217 | unif def_t t2 |
||

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

219 | let def_t = get_type_definition t in |
||

220 | unif t1 def_t |
||

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

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

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

224 | let eval_const = |
||

225 | if semi |
||

226 | then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c)) |
||

227 | else (fun c -> None) in |
||

228 | begin |
||

229 | unif t1' t2'; |
||

230 | Dimension.eval Basic_library.eval_env eval_const e1; |
||

231 | Dimension.eval Basic_library.eval_env eval_const e2; |
||

232 | Dimension.unify ~semi:semi e1 e2; |
||

233 | end |
||

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

235 | in unif t1 t2 |
||

236 | 7a47b44f | xthirioux | |

237 | 12af4908 | xthirioux | (* Expected type ty1, got type ty2 *) |

238 | 6afa892a | xthirioux | let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc = |

239 | 7291cb80 | xthirioux | try |

240 | 6afa892a | xthirioux | unify ~sub:sub ~semi:semi ty1 ty2 |

241 | 7291cb80 | xthirioux | with |

242 | | Unify _ -> |
||

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

244 | | Dimension.Unify _ -> |
||

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

246 | |||

247 | 21485807 | xthirioux | let rec type_struct_const_field loc (label, c) = |

248 | 12af4908 | xthirioux | if Hashtbl.mem field_table label |

249 | ef34b4ae | xthirioux | then let tydef = Hashtbl.find field_table label in |

250 | let tydec = (typedef_of_top tydef).tydef_desc in |
||

251 | 12af4908 | xthirioux | let tydec_struct = get_struct_type_fields tydec in |

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

253 | begin |
||

254 | 21485807 | xthirioux | try_unify ty_label (type_const loc c) loc; |

255 | 12af4908 | xthirioux | type_coretype (fun d -> ()) tydec |

256 | end |
||

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

258 | |||

259 | 21485807 | xthirioux | and type_const loc c = |

260 | 22fe1c93 | ploc | match c with |

261 | 12af4908 | xthirioux | | Const_int _ -> Type_predef.type_int |

262 | | Const_real _ -> Type_predef.type_real |
||

263 | | Const_float _ -> Type_predef.type_real |
||

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

265 | 22fe1c93 | ploc | let ty = new_var () in |

266 | 12af4908 | xthirioux | List.iter (fun e -> try_unify ty (type_const loc e) loc) ca; |

267 | 22fe1c93 | ploc | Type_predef.type_array d ty |

268 | 12af4908 | xthirioux | | Const_tag t -> |

269 | 22fe1c93 | ploc | if Hashtbl.mem tag_table t |

270 | ef34b4ae | xthirioux | then |

271 | let tydef = typedef_of_top (Hashtbl.find tag_table t) in |
||

272 | let tydec = |
||

273 | if is_user_type tydef.tydef_desc |
||

274 | then Tydec_const tydef.tydef_id |
||

275 | else tydef.tydef_desc in |
||

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

277 | 22fe1c93 | ploc | else raise (Error (loc, Unbound_value ("enum tag " ^ t))) |

278 | 12af4908 | xthirioux | | Const_struct fl -> |

279 | let ty_struct = new_var () in |
||

280 | begin |
||

281 | 21485807 | xthirioux | let used = |

282 | List.fold_left |
||

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

284 | if List.mem l acc |
||

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

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

287 | [] fl in |
||

288 | try |
||

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

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

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

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

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

294 | with Not_found -> |
||

295 | ty_struct |
||

296 | 12af4908 | xthirioux | end |

297 | 01c7d5e1 | ploc | | Const_string _ -> assert false (* string should only appear in annotations *) |

298 | 22fe1c93 | ploc | |

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

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

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

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

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

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

305 | propagation policy in Lustre. |
||

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

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

308 | *) |
||

309 | let check_constant loc const_expected const_real = |
||

310 | if const_expected && not const_real |
||

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

312 | |||

313 | a38c681e | xthirioux | let rec type_add_const env const arg targ = |

314 | if const |
||

315 | then let d = |
||

316 | if is_dimension_type targ |
||

317 | then dimension_of_expr arg |
||

318 | else Dimension.mkdim_var () in |
||

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

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

321 | let real_static_type = Type_predef.type_static d (Types.dynamic_type targ) in |
||

322 | (match Types.get_static_value targ with |
||

323 | | None -> () |
||

324 | | Some d' -> try_unify targ real_static_type arg.expr_loc); |
||

325 | real_static_type |
||

326 | else targ |
||

327 | 22fe1c93 | ploc | |

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

329 | 4a840259 | xthirioux | used during node applications and assignments *) |

330 | 22fe1c93 | ploc | and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type = |

331 | let loc = real_arg.expr_loc in |
||

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

333 | a38c681e | xthirioux | let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in |

334 | 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;*) |

335 | 6afa892a | xthirioux | try_unify ~sub:sub formal_type real_type loc |

336 | 52cfee34 | xthirioux | |

337 | 22fe1c93 | ploc | and type_ident env in_main loc const id = |

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

339 | |||

340 | (* typing an application implies: |
||

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

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

343 | b616fe7a | xthirioux | An application may embed an homomorphic/internal function, in which case we need to split |

344 | it in many calls |
||

345 | 22fe1c93 | ploc | *) |

346 | and type_appl env in_main loc const f args = |
||

347 | a38c681e | xthirioux | let targs = List.map (type_expr env in_main const) args in |

348 | if Basic_library.is_internal_fun f && List.exists is_tuple_type targs |
||

349 | b616fe7a | xthirioux | then |

350 | try |
||

351 | a38c681e | xthirioux | let targs = Utils.transpose_list (List.map type_list_of_type targs) in |

352 | Types.type_of_type_list (List.map (type_simple_call env in_main loc const f) targs) |
||

353 | b616fe7a | xthirioux | with |

354 | Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l'))) |
||

355 | else |
||

356 | a38c681e | xthirioux | type_dependent_call env in_main loc const f (List.combine args targs) |

357 | b616fe7a | xthirioux | |

358 | a38c681e | xthirioux | (* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *) |

359 | and type_dependent_call env in_main loc const f targs = |
||

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 | in try_unify ~sub:true ti t' a.expr_loc) targs tins; |
||

371 | touts |
||

372 | 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 | type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int; |
||

420 | 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 | 5c1184ad | ploc | | Some (x, l) -> |

448 | check_constant expr.expr_loc const false; |
||

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

450 | let typ_l = |
||

451 | Type_predef.type_clock |
||

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

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

454 | a38c681e | xthirioux | let touts = type_appl env in_main expr.expr_loc const id (expr_list_of_expr args) in |

455 | 22fe1c93 | ploc | expr.expr_type <- touts; |

456 | touts |
||

457 | | Expr_fby (e1,e2) |
||

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

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

460 | check_constant expr.expr_loc const false; |
||

461 | a38c681e | xthirioux | let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in |

462 | 22fe1c93 | ploc | expr.expr_type <- ty; |

463 | ty |
||

464 | | Expr_pre e -> |
||

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

466 | check_constant expr.expr_loc const false; |
||

467 | a38c681e | xthirioux | let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in |

468 | 22fe1c93 | ploc | expr.expr_type <- ty; |

469 | ty |
||

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

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

472 | check_constant expr.expr_loc const false; |
||

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

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

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

476 | a38c681e | xthirioux | let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in |

477 | 22fe1c93 | ploc | expr.expr_type <- ty; |

478 | ty |
||

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

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

481 | check_constant expr.expr_loc const false; |
||

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

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

484 | let typ_l = Type_predef.type_clock typ_in in |
||

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

486 | expr.expr_type <- typ_out; |
||

487 | typ_out |
||

488 | b616fe7a | xthirioux | in |

489 | Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr Types.print_ty resulting_ty); |
||

490 | resulting_ty |
||

491 | 22fe1c93 | ploc | |

492 | and type_branches env in_main loc const hl = |
||

493 | let typ_in = new_var () in |
||

494 | let typ_out = new_var () in |
||

495 | try |
||

496 | let used_labels = |
||

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

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

499 | type_subtyping_arg env in_main const h typ_out; |
||

500 | if List.mem t accu |
||

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

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

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

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

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

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

507 | else (typ_in, typ_out) |
||

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

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

510 | a38c681e | xthirioux | |

511 | 22fe1c93 | ploc | (** [type_eq env eq] types equation [eq] in environment [env] *) |

512 | let type_eq env in_main undefined_vars eq = |
||

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

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

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

516 | (* Check multiple variable definitions *) |
||

517 | let define_var id uvars = |
||

518 | try |
||

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

520 | IMap.remove id uvars |
||

521 | with Not_found -> |
||

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

523 | in |
||

524 | 6afa892a | xthirioux | (* check assignment of declared constant, assignment of clock *) |

525 | let ty_lhs = |
||

526 | type_of_type_list |
||

527 | (List.map2 (fun ty id -> |
||

528 | if get_static_value ty <> None |
||

529 | then raise (Error (eq.eq_loc, Assigned_constant id)) else |
||

530 | match get_clock_base_type ty with |
||

531 | | None -> ty |
||

532 | | Some ty -> ty) |
||

533 | (type_list_of_type ty_lhs) eq.eq_lhs) in |
||

534 | 22fe1c93 | ploc | let undefined_vars = |

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

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

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

538 | 11242500 | xthirioux | type_subtyping_arg env in_main false eq.eq_rhs ty_lhs; |

539 | 22fe1c93 | ploc | undefined_vars |

540 | |||

541 | |||

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

543 | in environment [env] *) |
||

544 | let type_coreclock env ck id loc = |
||

545 | match ck.ck_dec_desc with |
||

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

547 | | Ckdec_bool cl -> |
||

548 | let dummy_id_expr = expr_of_ident id loc in |
||

549 | let when_expr = |
||

550 | List.fold_left |
||

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

552 | {expr_tag = new_tag (); |
||

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

554 | expr_type = new_var (); |
||

555 | expr_clock = Clocks.new_var true; |
||

556 | expr_delay = Delay.new_var (); |
||

557 | expr_loc=loc; |
||

558 | expr_annot = None}) |
||

559 | dummy_id_expr cl |
||

560 | in |
||

561 | ignore (type_expr env false false when_expr) |
||

562 | |||

563 | let rec check_type_declaration loc cty = |
||

564 | match cty with |
||

565 | | Tydec_clock ty |
||

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

567 | | Tydec_const tname -> |
||

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

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

570 | | _ -> () |
||

571 | |||

572 | let type_var_decl vd_env env vdecl = |
||

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

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

575 | let type_dim d = |
||

576 | begin |
||

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

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

579 | end in |
||

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

581 | let ty_status = |
||

582 | if vdecl.var_dec_const |
||

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

584 | else ty in |
||

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

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

587 | vdecl.var_type <- ty_status; |
||

588 | new_env |
||

589 | |||

590 | let type_var_decl_list vd_env env l = |
||

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

592 | |||

593 | let type_of_vlist vars = |
||

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

595 | type_of_type_list tyl |
||

596 | |||

597 | let add_vdecl vd_env vdecl = |
||

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

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

600 | else vdecl::vd_env |
||

601 | |||

602 | let check_vd_env vd_env = |
||

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

604 | |||

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

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

607 | let type_node env nd loc = |
||

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

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

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

611 | check_vd_env vd_env; |
||

612 | let init_env = env in |
||

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

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

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

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

617 | let undefined_vars_init = |
||

618 | List.fold_left |
||

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

620 | IMap.empty vd_env_ol in |
||

621 | let undefined_vars = |
||

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

623 | in |
||

624 | af5af1e8 | ploc | (* Typing asserts *) |

625 | List.iter (fun assert_ -> |
||

626 | let assert_expr = assert_.assert_expr in |
||

627 | type_subtyping_arg (new_env, vd_env) is_main false assert_expr Type_predef.type_bool |
||

628 | ) nd.node_asserts; |
||

629 | |||

630 | 22fe1c93 | ploc | (* check that table is empty *) |

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

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

633 | let ty_ins = type_of_vlist nd.node_inputs in |
||

634 | let ty_outs = type_of_vlist nd.node_outputs in |
||

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

636 | generalize ty_node; |
||

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

638 | nd.node_type <- ty_node; |
||

639 | Env.add_value env nd.node_id ty_node |
||

640 | |||

641 | let type_imported_node env nd loc = |
||

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

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

644 | check_vd_env vd_env; |
||

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

646 | let ty_ins = type_of_vlist nd.nodei_inputs in |
||

647 | let ty_outs = type_of_vlist nd.nodei_outputs in |
||

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

649 | generalize ty_node; |
||

650 | (* |
||

651 | if (is_polymorphic ty_node) then |
||

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

653 | *) |
||

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

655 | nd.nodei_type <- ty_node; |
||

656 | new_env |
||

657 | |||

658 | ef34b4ae | xthirioux | let type_top_const env cdecl = |

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

660 | let d = |
||

661 | if is_dimension_type ty |
||

662 | then dimension_of_const cdecl.const_loc cdecl.const_value |
||

663 | else Dimension.mkdim_var () in |
||

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

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

666 | cdecl.const_type <- ty; |
||

667 | new_env |
||

668 | |||

669 | 22fe1c93 | ploc | let type_top_consts env clist = |

670 | ef34b4ae | xthirioux | List.fold_left type_top_const env clist |

671 | |||

672 | let rec type_top_decl env decl = |
||

673 | 22fe1c93 | ploc | match decl.top_decl_desc with |

674 | e2380d4d | ploc | | Node nd -> ( |

675 | try |
||

676 | type_node env nd decl.top_decl_loc |
||

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

678 | if !Options.global_inline then |
||

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

680 | Printers.pp_node nd |
||

681 | ; |
||

682 | raise exc) |
||

683 | ) |
||

684 | 22fe1c93 | ploc | | ImportedNode nd -> |

685 | type_imported_node env nd decl.top_decl_loc |
||

686 | ef34b4ae | xthirioux | | Const c -> |

687 | type_top_const env c |
||

688 | | TypeDef _ -> List.fold_left type_top_decl env (consts_of_enum_type decl) |
||

689 | 5c1184ad | ploc | | Open _ -> env |

690 | 22fe1c93 | ploc | |

691 | let type_prog env decls = |
||

692 | try |
||

693 | 5c1184ad | ploc | List.fold_left type_top_decl env decls |

694 | 22fe1c93 | ploc | with Failure _ as exc -> raise exc |

695 | |||

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

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

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

699 | |||

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

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

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

703 | *) |
||

704 | let uneval_vdecl_generics vdecl = |
||

705 | if vdecl.var_dec_const |
||

706 | then |
||

707 | match get_static_value vdecl.var_type with |
||

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

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

710 | |||

711 | let uneval_node_generics vdecls = |
||

712 | List.iter uneval_vdecl_generics vdecls |
||

713 | |||

714 | let uneval_top_generics decl = |
||

715 | match decl.top_decl_desc with |
||

716 | | Node nd -> |
||

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

718 | | ImportedNode nd -> |
||

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

720 | ef34b4ae | xthirioux | | Const _ |

721 | | TypeDef _ |
||

722 | 5c1184ad | ploc | | Open _ -> () |

723 | 22fe1c93 | ploc | |

724 | let uneval_prog_generics prog = |
||

725 | List.iter uneval_top_generics prog |
||

726 | 5c1184ad | ploc | |

727 | ef34b4ae | xthirioux | let rec get_imported_symbol decls id = |

728 | 96f5fe18 | xthirioux | match decls with |

729 | | [] -> assert false |
||

730 | | decl::q -> |
||

731 | (match decl.top_decl_desc with |
||

732 | ef34b4ae | xthirioux | | ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf -> decl |

733 | | Const c when id = c.const_id && decl.top_decl_itf -> decl |
||

734 | | TypeDef _ -> get_imported_symbol (consts_of_enum_type decl @ q) id |
||

735 | | _ -> get_imported_symbol q id) |
||

736 | 96f5fe18 | xthirioux | |

737 | 8f1c7e91 | xthirioux | let check_env_compat header declared computed = |

738 | uneval_prog_generics header; |
||

739 | ef34b4ae | xthirioux | Env.iter declared (fun k decl_type_k -> |

740 | let loc = (get_imported_symbol header k).top_decl_loc in |
||

741 | let computed_t = |
||

742 | instantiate (ref []) (ref []) |
||

743 | (try Env.lookup_value computed k |
||

744 | with Not_found -> raise (Error (loc, Declared_but_undefined k))) in |
||

745 | 7291cb80 | xthirioux | (*Types.print_ty Format.std_formatter decl_type_k; |

746 | ef34b4ae | xthirioux | Types.print_ty Format.std_formatter computed_t;*) |

747 | try_unify ~sub:true ~semi:true decl_type_k computed_t loc |
||

748 | ) |
||

749 | |||

750 | b1655a21 | xthirioux | let check_typedef_top decl = |

751 | ef34b4ae | xthirioux | (*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*) |

752 | (*Printers.pp_var_type_dec_desc (typedef_of_top decl).tydef_id*) |
||

753 | (*Format.eprintf "%a" Corelang.print_type_table ();*) |
||

754 | b1655a21 | xthirioux | match decl.top_decl_desc with |

755 | ef34b4ae | xthirioux | | TypeDef ty -> |

756 | let owner = decl.top_decl_owner in |
||

757 | let itf = decl.top_decl_itf in |
||

758 | let decl' = |
||

759 | try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id) |
||

760 | with Not_found -> raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in |
||

761 | let owner' = decl'.top_decl_owner in |
||

762 | let itf' = decl'.top_decl_itf in |
||

763 | (match decl'.top_decl_desc with |
||

764 | | Const _ | Node _ | ImportedNode _ -> assert false |
||

765 | | TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') -> () |
||

766 | | _ -> raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id))) |
||

767 | b1655a21 | xthirioux | | _ -> () |

768 | |||

769 | let check_typedef_compat header = |
||

770 | List.iter check_typedef_top header |
||

771 | 5c1184ad | ploc | |

772 | 22fe1c93 | ploc | (* Local Variables: *) |

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

774 | (* End: *) |