## lustrec / src / types.ml @ 2823bc51

History | View | Annotate | Download (10.6 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 | (** Types definitions and a few utility functions on types. *) |
||

15 | open Utils |
||

16 | open Dimension |
||

17 | |||

18 | type type_expr = |
||

19 | {mutable tdesc: type_desc; |
||

20 | tid: int} |
||

21 | |||

22 | and type_desc = |
||

23 | | Tconst of ident (* type constant *) |
||

24 | | Tint |
||

25 | | Treal |
||

26 | | Tbool |
||

27 | | Trat (* Actually unused for now. Only place where it can appear is |
||

28 | in a clock declaration *) |
||

29 | 6afa892a | xthirioux | | Tclock of type_expr (* A type expression explicitely tagged as carrying a clock *) |

30 | 22fe1c93 | ploc | | Tarrow of type_expr * type_expr |

31 | | Ttuple of type_expr list |
||

32 | | Tenum of ident list |
||

33 | 12af4908 | xthirioux | | Tstruct of (ident * type_expr) list |

34 | 22fe1c93 | ploc | | Tarray of dim_expr * type_expr |

35 | | Tstatic of dim_expr * type_expr (* a type carried by a dimension expression *) |
||

36 | | Tlink of type_expr (* During unification, make links instead of substitutions *) |
||

37 | | Tvar (* Monomorphic type variable *) |
||

38 | | Tunivar (* Polymorphic type variable *) |
||

39 | |||

40 | type error = |
||

41 | Unbound_value of ident |
||

42 | | Already_bound of ident |
||

43 | | Already_defined of ident |
||

44 | ec433d69 | xthirioux | | Undefined_var of ISet.t |

45 | 96f5fe18 | xthirioux | | Declared_but_undefined of ident |

46 | 22fe1c93 | ploc | | Unbound_type of ident |

47 | | Not_a_dimension |
||

48 | | Not_a_constant |
||

49 | 6afa892a | xthirioux | | Assigned_constant of ident |

50 | 22fe1c93 | ploc | | WrongArity of int * int |

51 | b616fe7a | xthirioux | | WrongMorphism of int * int |

52 | b1655a21 | xthirioux | | Type_mismatch of ident |

53 | 22fe1c93 | ploc | | Type_clash of type_expr * type_expr |

54 | | Poly_imported_node of ident |
||

55 | |||

56 | exception Unify of type_expr * type_expr |
||

57 | exception Error of Location.t * error |
||

58 | |||

59 | (* Pretty-print*) |
||

60 | open Format |
||

61 | 12af4908 | xthirioux | |

62 | let rec print_struct_ty_field fmt (label, ty) = |
||

63 | fprintf fmt "%a : %a" pp_print_string label print_ty ty |
||

64 | and print_ty fmt ty = |
||

65 | 22fe1c93 | ploc | match ty.tdesc with |

66 | | Tvar -> |
||

67 | fprintf fmt "_%s" (name_of_type ty.tid) |
||

68 | | Tint -> |
||

69 | fprintf fmt "int" |
||

70 | | Treal -> |
||

71 | fprintf fmt "real" |
||

72 | | Tbool -> |
||

73 | fprintf fmt "bool" |
||

74 | | Tclock t -> |
||

75 | fprintf fmt "%a clock" print_ty t |
||

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

77 | fprintf fmt "(%a:%a)" Dimension.pp_dimension d print_ty t |
||

78 | | Tconst t -> |
||

79 | fprintf fmt "%s" t |
||

80 | | Trat -> |
||

81 | fprintf fmt "rat" |
||

82 | | Tarrow (ty1,ty2) -> |
||

83 | 719f9992 | xthirioux | fprintf fmt "%a -> %a" print_ty ty1 print_ty ty2 |

84 | 22fe1c93 | ploc | | Ttuple tylist -> |

85 | fprintf fmt "(%a)" |
||

86 | e39f5319 | xthirioux | (Utils.fprintf_list ~sep:" * " print_ty) tylist |

87 | 22fe1c93 | ploc | | Tenum taglist -> |

88 | 12af4908 | xthirioux | fprintf fmt "enum {%a }" |

89 | (Utils.fprintf_list ~sep:", " pp_print_string) taglist |
||

90 | | Tstruct fieldlist -> |
||

91 | fprintf fmt "struct {%a }" |
||

92 | (Utils.fprintf_list ~sep:"; " print_struct_ty_field) fieldlist |
||

93 | 22fe1c93 | ploc | | Tarray (e, ty) -> |

94 | fprintf fmt "%a^%a" print_ty ty Dimension.pp_dimension e |
||

95 | | Tlink ty -> |
||

96 | print_ty fmt ty |
||

97 | | Tunivar -> |
||

98 | fprintf fmt "'%s" (name_of_type ty.tid) |
||

99 | |||

100 | 12af4908 | xthirioux | let rec print_node_struct_ty_field fmt (label, ty) = |

101 | fprintf fmt "%a : %a" pp_print_string label print_node_ty ty |
||

102 | and print_node_ty fmt ty = |
||

103 | 7291cb80 | xthirioux | match ty.tdesc with |

104 | 96f5fe18 | xthirioux | | Tvar -> begin |

105 | b35da910 | xthirioux | (*Format.eprintf "DEBUG:Types.print_node@.";*) |

106 | 96f5fe18 | xthirioux | fprintf fmt "_%s" (name_of_type ty.tid) |

107 | end |
||

108 | 7291cb80 | xthirioux | | Tint -> |

109 | fprintf fmt "int" |
||

110 | | Treal -> |
||

111 | fprintf fmt "real" |
||

112 | | Tbool -> |
||

113 | fprintf fmt "bool" |
||

114 | | Tclock t -> |
||

115 | 6afa892a | xthirioux | fprintf fmt "%a clock" print_node_ty t |

116 | 7291cb80 | xthirioux | | Tstatic (_, t) -> |

117 | fprintf fmt "%a" print_node_ty t |
||

118 | | Tconst t -> |
||

119 | fprintf fmt "%s" t |
||

120 | | Trat -> |
||

121 | fprintf fmt "rat" |
||

122 | | Tarrow (ty1,ty2) -> |
||

123 | 6afa892a | xthirioux | fprintf fmt "%a -> %a" print_node_ty ty1 print_node_ty ty2 |

124 | 7291cb80 | xthirioux | | Ttuple tylist -> |

125 | fprintf fmt "(%a)" |
||

126 | 6afa892a | xthirioux | (Utils.fprintf_list ~sep:"*" print_node_ty) tylist |

127 | 7291cb80 | xthirioux | | Tenum taglist -> |

128 | 12af4908 | xthirioux | fprintf fmt "enum {%a }" |

129 | (Utils.fprintf_list ~sep:", " pp_print_string) taglist |
||

130 | | Tstruct fieldlist -> |
||

131 | fprintf fmt "struct {%a }" |
||

132 | (Utils.fprintf_list ~sep:"; " print_node_struct_ty_field) fieldlist |
||

133 | 7291cb80 | xthirioux | | Tarray (e, ty) -> |

134 | 6afa892a | xthirioux | fprintf fmt "%a^%a" print_node_ty ty Dimension.pp_dimension e |

135 | 7291cb80 | xthirioux | | Tlink ty -> |

136 | 6afa892a | xthirioux | print_node_ty fmt ty |

137 | 7291cb80 | xthirioux | | Tunivar -> |

138 | fprintf fmt "'%s" (name_of_type ty.tid) |
||

139 | |||

140 | 22fe1c93 | ploc | let pp_error fmt = function |

141 | | Unbound_value id -> |
||

142 | fprintf fmt "Unknown value %s@." id |
||

143 | | Unbound_type id -> |
||

144 | fprintf fmt "Unknown type %s@." id |
||

145 | | Already_bound id -> |
||

146 | fprintf fmt "%s is already declared@." id |
||

147 | | Already_defined id -> |
||

148 | fprintf fmt "Multiple definitions of variable %s@." id |
||

149 | | Not_a_constant -> |
||

150 | fprintf fmt "This expression is not a constant@." |
||

151 | 6afa892a | xthirioux | | Assigned_constant id -> |

152 | fprintf fmt "The constant %s cannot be assigned@." id |
||

153 | 22fe1c93 | ploc | | Not_a_dimension -> |

154 | fprintf fmt "This expression is not a valid dimension@." |
||

155 | | WrongArity (ar1, ar2) -> |
||

156 | fprintf fmt "Expecting %d argument(s), found %d@." ar1 ar2 |
||

157 | b616fe7a | xthirioux | | WrongMorphism (ar1, ar2) -> |

158 | fprintf fmt "Expecting %d argument(s) for homomorphic extension, found %d@." ar1 ar2 |
||

159 | b1655a21 | xthirioux | | Type_mismatch id -> |

160 | fprintf fmt "Definition and declaration of type %s don't agree@." id |
||

161 | ec433d69 | xthirioux | | Undefined_var vset -> |

162 | 22fe1c93 | ploc | fprintf fmt "No definition provided for variable(s): %a@." |

163 | (Utils.fprintf_list ~sep:"," pp_print_string) |
||

164 | ec433d69 | xthirioux | (ISet.elements vset) |

165 | 96f5fe18 | xthirioux | | Declared_but_undefined id -> |

166 | ef34b4ae | xthirioux | fprintf fmt "%s is declared but not defined@." id |

167 | 22fe1c93 | ploc | | Type_clash (ty1,ty2) -> |

168 | Utils.reset_names (); |
||

169 | fprintf fmt "Expected type %a, got type %a@." print_ty ty1 print_ty ty2 |
||

170 | | Poly_imported_node id -> |
||

171 | fprintf fmt "Imported nodes cannot have a polymorphic type@." |
||

172 | |||

173 | |||

174 | let new_id = ref (-1) |
||

175 | |||

176 | 04a63d25 | xthirioux | let rec bottom = |

177 | { tdesc = Tlink bottom; tid = -666 } |
||

178 | |||

179 | 22fe1c93 | ploc | let new_ty desc = |

180 | incr new_id; {tdesc = desc; tid = !new_id } |
||

181 | |||

182 | let new_var () = |
||

183 | new_ty Tvar |
||

184 | |||

185 | let new_univar () = |
||

186 | new_ty Tunivar |
||

187 | |||

188 | let rec repr = |
||

189 | function |
||

190 | {tdesc = Tlink t'} -> |
||

191 | repr t' |
||

192 | | t -> t |
||

193 | |||

194 | let get_static_value ty = |
||

195 | 12af4908 | xthirioux | match (repr ty).tdesc with |

196 | | Tstatic (d, _) -> Some d |
||

197 | | _ -> None |
||

198 | |||

199 | let get_field_type ty label = |
||

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

201 | | Tstruct fl -> (try Some (List.assoc label fl) with Not_found -> None) |
||

202 | | _ -> None |
||

203 | 22fe1c93 | ploc | |

204 | 04a63d25 | xthirioux | let rec is_scalar_type ty = |

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

206 | | Tstatic (_, ty) -> is_scalar_type ty |
||

207 | | Tbool |
||

208 | | Tint |
||

209 | | Treal -> true |
||

210 | | _ -> false |
||

211 | |||

212 | let rec is_numeric_type ty = |
||

213 | 6afa892a | xthirioux | match (repr ty).tdesc with |

214 | 04a63d25 | xthirioux | | Tstatic (_, ty) -> is_numeric_type ty |

215 | 6afa892a | xthirioux | | Tint |

216 | | Treal -> true |
||

217 | | _ -> false |
||

218 | |||

219 | 04a63d25 | xthirioux | let rec is_real_type ty = |

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

221 | | Tstatic (_, ty) -> is_real_type ty |
||

222 | | Treal -> true |
||

223 | | _ -> false |
||

224 | |||

225 | let rec is_bool_type ty = |
||

226 | 6afa892a | xthirioux | match (repr ty).tdesc with |

227 | 04a63d25 | xthirioux | | Tstatic (_, ty) -> is_bool_type ty |

228 | 6afa892a | xthirioux | | Tbool -> true |

229 | | _ -> false |
||

230 | |||

231 | let get_clock_base_type ty = |
||

232 | 8f1c7e91 | xthirioux | match (repr ty).tdesc with |

233 | 6afa892a | xthirioux | | Tclock ty -> Some ty |

234 | | _ -> None |
||

235 | 8f1c7e91 | xthirioux | |

236 | e3a4e911 | xthirioux | let unclock_type ty = |

237 | let ty = repr ty in |
||

238 | match ty.tdesc with |
||

239 | | Tclock ty' -> ty' |
||

240 | | _ -> ty |
||

241 | |||

242 | 22fe1c93 | ploc | let rec is_dimension_type ty = |

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

244 | | Tint |
||

245 | | Tbool -> true |
||

246 | | Tclock ty' |
||

247 | | Tstatic (_, ty') -> is_dimension_type ty' |
||

248 | | _ -> false |
||

249 | |||

250 | b616fe7a | xthirioux | let dynamic_type ty = |

251 | 22fe1c93 | ploc | let ty = repr ty in |

252 | match ty.tdesc with |
||

253 | | Tstatic (_, ty') -> ty' |
||

254 | | _ -> ty |
||

255 | |||

256 | b616fe7a | xthirioux | let is_tuple_type ty = |

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

258 | | Ttuple _ -> true |
||

259 | | _ -> false |
||

260 | |||

261 | 22fe1c93 | ploc | let map_tuple_type f ty = |

262 | let ty = dynamic_type ty in |
||

263 | match ty.tdesc with |
||

264 | | (Ttuple ty_list) -> { ty with tdesc = Ttuple (List.map f ty_list) } |
||

265 | | _ -> f ty |
||

266 | b174e673 | xthirioux | |

267 | 8a183477 | xthirioux | let rec is_struct_type ty = |

268 | b174e673 | xthirioux | match (repr ty).tdesc with |

269 | | Tstruct _ -> true |
||

270 | 8a183477 | xthirioux | | Tstatic (_, ty') -> is_struct_type ty' |

271 | b174e673 | xthirioux | | _ -> false |

272 | |||

273 | 2d179f5b | xthirioux | let struct_field_type ty field = |

274 | match (dynamic_type ty).tdesc with |
||

275 | | Tstruct fields -> |
||

276 | (try |
||

277 | List.assoc field fields |
||

278 | with Not_found -> assert false) |
||

279 | | _ -> assert false |
||

280 | |||

281 | 22fe1c93 | ploc | let rec is_array_type ty = |

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

283 | | Tarray _ -> true |
||

284 | b174e673 | xthirioux | | Tstatic (_, ty') -> is_array_type ty' (* looks strange !? *) |

285 | 22fe1c93 | ploc | | _ -> false |

286 | |||

287 | let array_type_dimension ty = |
||

288 | match (dynamic_type ty).tdesc with |
||

289 | | Tarray (d, _) -> d |
||

290 | fc886259 | xthirioux | | _ -> (Format.eprintf "internal error: Types.array_type_dimension %a@." print_ty ty; assert false) |

291 | 22fe1c93 | ploc | |

292 | let rec array_type_multi_dimension ty = |
||

293 | match (dynamic_type ty).tdesc with |
||

294 | | Tarray (d, ty') -> d :: array_type_multi_dimension ty' |
||

295 | | _ -> [] |
||

296 | |||

297 | let array_element_type ty = |
||

298 | match (dynamic_type ty).tdesc with |
||

299 | | Tarray (_, ty') -> ty' |
||

300 | fc886259 | xthirioux | | _ -> (Format.eprintf "internal error: Types.array_element_type %a@." print_ty ty; assert false) |

301 | 22fe1c93 | ploc | |

302 | let rec array_base_type ty = |
||

303 | let ty = repr ty in |
||

304 | match ty.tdesc with |
||

305 | | Tarray (_, ty') |
||

306 | | Tstatic (_, ty') -> array_base_type ty' |
||

307 | | _ -> ty |
||

308 | |||

309 | b174e673 | xthirioux | let is_address_type ty = |

310 | 04a63d25 | xthirioux | is_array_type ty || is_struct_type ty || (is_real_type ty && !Options.mpfr) |

311 | b174e673 | xthirioux | |

312 | 22fe1c93 | ploc | let rec is_generic_type ty = |

313 | match (dynamic_type ty).tdesc with |
||

314 | | Tarray (d, ty') -> |
||

315 | (not (Dimension.is_dimension_const d)) || (is_generic_type ty') |
||

316 | | _ -> false |
||

317 | |||

318 | (** Splits [ty] into the [lhs,rhs] of an arrow type. Expects an arrow type |
||

319 | (ensured by language syntax) *) |
||

320 | let rec split_arrow ty = |
||

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

322 | | Tarrow (tin,tout) -> tin,tout |
||

323 | | Tstatic (_, ty') -> split_arrow ty' |
||

324 | (* Functions are not first order, I don't think the var case |
||

325 | needs to be considered here *) |
||

326 | 870420a0 | ploc | | _ -> Format.eprintf "type %a is not a map@.Unable to split@.@?" print_ty ty; assert false |

327 | 22fe1c93 | ploc | |

328 | (** Returns the type corresponding to a type list. *) |
||

329 | let type_of_type_list tyl = |
||

330 | if (List.length tyl) > 1 then |
||

331 | new_ty (Ttuple tyl) |
||

332 | else |
||

333 | List.hd tyl |
||

334 | |||

335 | 04a63d25 | xthirioux | let rec type_list_of_type ty = |

336 | 22fe1c93 | ploc | match (repr ty).tdesc with |

337 | 04a63d25 | xthirioux | | Tstatic (_, ty) -> type_list_of_type ty |

338 | | Ttuple tl -> tl |
||

339 | | _ -> [ty] |
||

340 | 22fe1c93 | ploc | |

341 | (** [is_polymorphic ty] returns true if [ty] is polymorphic. *) |
||

342 | let rec is_polymorphic ty = |
||

343 | match ty.tdesc with |
||

344 | | Tenum _ | Tvar | Tint | Treal | Tbool | Trat | Tconst _ -> false |
||

345 | | Tclock ty -> is_polymorphic ty |
||

346 | | Tarrow (ty1,ty2) -> (is_polymorphic ty1) || (is_polymorphic ty2) |
||

347 | | Ttuple tl -> List.exists (fun t -> is_polymorphic t) tl |
||

348 | 12af4908 | xthirioux | | Tstruct fl -> List.exists (fun (_, t) -> is_polymorphic t) fl |

349 | 22fe1c93 | ploc | | Tlink t' -> is_polymorphic t' |

350 | | Tarray (d, ty) |
||

351 | | Tstatic (d, ty) -> Dimension.is_polymorphic d || is_polymorphic ty |
||

352 | | Tunivar -> true |
||

353 | |||

354 | |||

355 | let mktyptuple nb typ = |
||

356 | let array = Array.make nb typ in |
||

357 | Ttuple (Array.to_list array) |
||

358 | |||

359 | |||

360 | (* Local Variables: *) |
||

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

362 | (* End: *) |