## lustrec/src/types.ml @ c518d082

1 | 0cbf0839 | 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 | ```
(** Types definitions and a few utility functions on types. *)
``` |
||

24 | open Utils |
||

25 | open Dimension |
||

26 | |||

27 | type type_expr = |
||

28 | {mutable tdesc: type_desc; |
||

29 | tid: int} |
||

30 | |||

31 | and type_desc = |
||

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

33 | | Tint |
||

34 | | Treal |
||

35 | | Tbool |
||

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

37 | ```
in a clock declaration *)
``` |
||

38 | | Tclock of type_expr (* An type expression explicitely tagged as carrying a clock *) |
||

39 | | Tarrow of type_expr * type_expr |
||

40 | | Ttuple of type_expr list |
||

41 | | Tenum of ident list |
||

42 | | Tarray of dim_expr * type_expr |
||

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

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

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

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

47 | |||

48 | type error = |
||

49 | Unbound_value of ident |
||

50 | | Already_bound of ident |
||

51 | | Already_defined of ident |
||

52 | | Undefined_var of (unit IMap.t) |
||

53 | | Unbound_type of ident |
||

54 | | Not_a_dimension |
||

55 | | Not_a_constant |
||

56 | | WrongArity of int * int |
||

57 | | Type_clash of type_expr * type_expr |
||

58 | | Poly_imported_node of ident |
||

59 | |||

60 | exception Unify of type_expr * type_expr |
||

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

62 | |||

63 | ```
(* Pretty-print*)
``` |
||

64 | open Format |
||

65 | |||

66 | let rec print_ty fmt ty = |
||

67 | match ty.tdesc with |
||

68 | | Tvar -> |
||

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

70 | | Tint -> |
||

71 | fprintf fmt "int" |
||

72 | | Treal -> |
||

73 | fprintf fmt "real" |
||

74 | | Tbool -> |
||

75 | fprintf fmt "bool" |
||

76 | | Tclock t -> |
||

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

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

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

80 | | Tconst t -> |
||

81 | fprintf fmt "%s" t |
||

82 | | Trat -> |
||

83 | fprintf fmt "rat" |
||

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

85 | fprintf fmt "%a->%a" print_ty ty1 print_ty ty2 |
||

86 | | Ttuple tylist -> |
||

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

88 | (Utils.fprintf_list ~sep:"*" print_ty) tylist |
||

89 | | Tenum taglist -> |
||

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

91 | (Utils.fprintf_list ~sep:" + " pp_print_string) taglist |
||

92 | | Tarray (e, ty) -> |
||

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

94 | | Tlink ty -> |
||

95 | print_ty fmt ty |
||

96 | | Tunivar -> |
||

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

98 | |||

99 | 8b3afe43 | xthirioux | let rec print_node_ty fmt ty = |

100 | match ty.tdesc with |
||

101 | | Tint -> |
||

102 | fprintf fmt "int" |
||

103 | | Treal -> |
||

104 | fprintf fmt "real" |
||

105 | | Tbool -> |
||

106 | fprintf fmt "bool" |
||

107 | | Tclock t -> |
||

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

109 | | Tstatic (_, t) -> |
||

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

111 | | Tconst t -> |
||

112 | fprintf fmt "%s" t |
||

113 | | Trat -> |
||

114 | fprintf fmt "rat" |
||

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

116 | fprintf fmt "%a->%a" print_ty ty1 print_ty ty2 |
||

117 | | Ttuple tylist -> |
||

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

119 | (Utils.fprintf_list ~sep:"*" print_ty) tylist |
||

120 | | Tenum taglist -> |
||

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

122 | (Utils.fprintf_list ~sep:" + " pp_print_string) taglist |
||

123 | | Tarray (e, ty) -> |
||

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

125 | | Tlink ty -> |
||

126 | print_ty fmt ty |
||

127 | | Tunivar -> |
||

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

129 | | _ -> assert false |
||

130 | |||

131 | 0cbf0839 | ploc | let pp_error fmt = function |

132 | | Unbound_value id -> |
||

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

134 | | Unbound_type id -> |
||

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

136 | | Already_bound id -> |
||

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

138 | | Already_defined id -> |
||

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

140 | | Not_a_constant -> |
||

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

142 | | Not_a_dimension -> |
||

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

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

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

146 | | Undefined_var vmap -> |
||

147 | fprintf fmt "No definition provided for variable(s): %a@." |
||

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

149 | (fst (Utils.list_of_imap vmap)) |
||

150 | | Type_clash (ty1,ty2) -> |
||

151 | Utils.reset_names (); |
||

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

153 | | Poly_imported_node id -> |
||

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

155 | |||

156 | |||

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

158 | |||

159 | let new_ty desc = |
||

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

161 | |||

162 | let new_var () = |
||

163 | new_ty Tvar |
||

164 | |||

165 | let new_univar () = |
||

166 | new_ty Tunivar |
||

167 | |||

168 | let rec repr = |
||

169 | ```
function
``` |
||

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

171 | repr t' |
||

172 | | t -> t |
||

173 | |||

174 | let get_static_value ty = |
||

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

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

177 | | _ -> None |
||

178 | |||

179 | c518d082 | xthirioux | let is_clock_type ty = |

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

181 | | Tclock _ -> true |
||

182 | | _ -> false |
||

183 | |||

184 | 0cbf0839 | ploc | let rec is_dimension_type ty = |

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

186 | | Tint |
||

187 | | Tbool -> true |
||

188 | | Tclock ty' |
||

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

190 | | _ -> false |
||

191 | |||

192 | let rec dynamic_type ty = |
||

193 | let ty = repr ty in |
||

194 | match ty.tdesc with |
||

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

196 | | _ -> ty |
||

197 | |||

198 | let map_tuple_type f ty = |
||

199 | let ty = dynamic_type ty in |
||

200 | match ty.tdesc with |
||

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

202 | | _ -> f ty |
||

203 | let rec is_array_type ty = |
||

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

205 | | Tarray _ -> true |
||

206 | | Tstatic (_, ty') -> is_array_type ty' |
||

207 | | _ -> false |
||

208 | |||

209 | let array_type_dimension ty = |
||

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

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

212 | | _ -> assert false |
||

213 | |||

214 | let rec array_type_multi_dimension ty = |
||

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

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

217 | | _ -> [] |
||

218 | |||

219 | let array_element_type ty = |
||

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

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

222 | | _ -> assert false |
||

223 | |||

224 | let rec array_base_type ty = |
||

225 | let ty = repr ty in |
||

226 | match ty.tdesc with |
||

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

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

229 | | _ -> ty |
||

230 | |||

231 | let rec is_generic_type ty = |
||

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

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

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

235 | | _ -> false |
||

236 | |||

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

238 | ```
(ensured by language syntax) *)
``` |
||

239 | let rec split_arrow ty = |
||

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

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

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

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

244 | ```
needs to be considered here *)
``` |
||

245 | | _ -> Format.eprintf "%a@." print_ty ty; assert false |
||

246 | |||

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

248 | let type_of_type_list tyl = |
||

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

250 | new_ty (Ttuple tyl) |
||

251 | ```
else
``` |
||

252 | List.hd tyl |
||

253 | |||

254 | let type_list_of_type ty = |
||

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

256 | | Ttuple tl -> tl |
||

257 | | _ -> [ty] |
||

258 | |||

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

260 | let rec is_polymorphic ty = |
||

261 | match ty.tdesc with |
||

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

263 | | Tclock ty -> is_polymorphic ty |
||

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

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

266 | | Tlink t' -> is_polymorphic t' |
||

267 | | Tarray (d, ty) |
||

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

269 | | Tunivar -> true |
||

270 | |||

271 | |||

272 | let mktyptuple nb typ = |
||

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

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

275 | |||

276 | |||

277 | ```
(* Local Variables: *)
``` |
||

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

279 | ```
(* End: *)
``` |