lustrec / src / types.ml @ 14d694c7
History | View | Annotate | Download (9.44 KB)
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 | aa223e69 | xthirioux | | Tstruct of (ident * type_expr) list |
43 | 0cbf0839 | ploc | | Tarray of dim_expr * type_expr |
44 | | Tstatic of dim_expr * type_expr (* a type carried by a dimension expression *) |
||
45 | | Tlink of type_expr (* During unification, make links instead of substitutions *) |
||
46 | | Tvar (* Monomorphic type variable *) |
||
47 | | Tunivar (* Polymorphic type variable *) |
||
48 | |||
49 | type error = |
||
50 | Unbound_value of ident |
||
51 | | Already_bound of ident |
||
52 | | Already_defined of ident |
||
53 | | Undefined_var of (unit IMap.t) |
||
54 | 0b78e972 | xthirioux | | Declared_but_undefined of ident |
55 | 0cbf0839 | ploc | | Unbound_type of ident |
56 | | Not_a_dimension |
||
57 | | Not_a_constant |
||
58 | | WrongArity of int * int |
||
59 | 14d694c7 | xthirioux | | WrongMorphism of int * int |
60 | 0cbf0839 | ploc | | Type_clash of type_expr * type_expr |
61 | | Poly_imported_node of ident |
||
62 | |||
63 | exception Unify of type_expr * type_expr |
||
64 | exception Error of Location.t * error |
||
65 | |||
66 | (* Pretty-print*) |
||
67 | open Format |
||
68 | aa223e69 | xthirioux | |
69 | let rec print_struct_ty_field fmt (label, ty) = |
||
70 | fprintf fmt "%a : %a" pp_print_string label print_ty ty |
||
71 | and print_ty fmt ty = |
||
72 | 0cbf0839 | ploc | match ty.tdesc with |
73 | | Tvar -> |
||
74 | fprintf fmt "_%s" (name_of_type ty.tid) |
||
75 | | Tint -> |
||
76 | fprintf fmt "int" |
||
77 | | Treal -> |
||
78 | fprintf fmt "real" |
||
79 | | Tbool -> |
||
80 | fprintf fmt "bool" |
||
81 | | Tclock t -> |
||
82 | fprintf fmt "%a clock" print_ty t |
||
83 | | Tstatic (d, t) -> |
||
84 | fprintf fmt "(%a:%a)" Dimension.pp_dimension d print_ty t |
||
85 | | Tconst t -> |
||
86 | fprintf fmt "%s" t |
||
87 | | Trat -> |
||
88 | fprintf fmt "rat" |
||
89 | | Tarrow (ty1,ty2) -> |
||
90 | fprintf fmt "%a->%a" print_ty ty1 print_ty ty2 |
||
91 | | Ttuple tylist -> |
||
92 | fprintf fmt "(%a)" |
||
93 | (Utils.fprintf_list ~sep:"*" print_ty) tylist |
||
94 | | Tenum taglist -> |
||
95 | aa223e69 | xthirioux | fprintf fmt "enum {%a }" |
96 | (Utils.fprintf_list ~sep:", " pp_print_string) taglist |
||
97 | | Tstruct fieldlist -> |
||
98 | fprintf fmt "struct {%a }" |
||
99 | (Utils.fprintf_list ~sep:"; " print_struct_ty_field) fieldlist |
||
100 | 0cbf0839 | ploc | | Tarray (e, ty) -> |
101 | fprintf fmt "%a^%a" print_ty ty Dimension.pp_dimension e |
||
102 | | Tlink ty -> |
||
103 | print_ty fmt ty |
||
104 | | Tunivar -> |
||
105 | fprintf fmt "'%s" (name_of_type ty.tid) |
||
106 | |||
107 | aa223e69 | xthirioux | let rec print_node_struct_ty_field fmt (label, ty) = |
108 | fprintf fmt "%a : %a" pp_print_string label print_node_ty ty |
||
109 | and print_node_ty fmt ty = |
||
110 | 8b3afe43 | xthirioux | match ty.tdesc with |
111 | 0b78e972 | xthirioux | | Tvar -> begin |
112 | 66e38617 | xthirioux | (*Format.eprintf "DEBUG:Types.print_node@.";*) |
113 | 0b78e972 | xthirioux | fprintf fmt "_%s" (name_of_type ty.tid) |
114 | end |
||
115 | 8b3afe43 | xthirioux | | Tint -> |
116 | fprintf fmt "int" |
||
117 | | Treal -> |
||
118 | fprintf fmt "real" |
||
119 | | Tbool -> |
||
120 | fprintf fmt "bool" |
||
121 | | Tclock t -> |
||
122 | fprintf fmt "%a clock" print_ty t |
||
123 | | Tstatic (_, t) -> |
||
124 | fprintf fmt "%a" print_node_ty t |
||
125 | | Tconst t -> |
||
126 | fprintf fmt "%s" t |
||
127 | | Trat -> |
||
128 | fprintf fmt "rat" |
||
129 | | Tarrow (ty1,ty2) -> |
||
130 | fprintf fmt "%a->%a" print_ty ty1 print_ty ty2 |
||
131 | | Ttuple tylist -> |
||
132 | fprintf fmt "(%a)" |
||
133 | (Utils.fprintf_list ~sep:"*" print_ty) tylist |
||
134 | | Tenum taglist -> |
||
135 | aa223e69 | xthirioux | fprintf fmt "enum {%a }" |
136 | (Utils.fprintf_list ~sep:", " pp_print_string) taglist |
||
137 | | Tstruct fieldlist -> |
||
138 | fprintf fmt "struct {%a }" |
||
139 | (Utils.fprintf_list ~sep:"; " print_node_struct_ty_field) fieldlist |
||
140 | 8b3afe43 | xthirioux | | Tarray (e, ty) -> |
141 | fprintf fmt "%a^%a" print_ty ty Dimension.pp_dimension e |
||
142 | | Tlink ty -> |
||
143 | print_ty fmt ty |
||
144 | | Tunivar -> |
||
145 | fprintf fmt "'%s" (name_of_type ty.tid) |
||
146 | |||
147 | 0cbf0839 | ploc | let pp_error fmt = function |
148 | | Unbound_value id -> |
||
149 | fprintf fmt "Unknown value %s@." id |
||
150 | | Unbound_type id -> |
||
151 | fprintf fmt "Unknown type %s@." id |
||
152 | | Already_bound id -> |
||
153 | fprintf fmt "%s is already declared@." id |
||
154 | | Already_defined id -> |
||
155 | fprintf fmt "Multiple definitions of variable %s@." id |
||
156 | | Not_a_constant -> |
||
157 | fprintf fmt "This expression is not a constant@." |
||
158 | | Not_a_dimension -> |
||
159 | fprintf fmt "This expression is not a valid dimension@." |
||
160 | | WrongArity (ar1, ar2) -> |
||
161 | fprintf fmt "Expecting %d argument(s), found %d@." ar1 ar2 |
||
162 | 14d694c7 | xthirioux | | WrongMorphism (ar1, ar2) -> |
163 | fprintf fmt "Expecting %d argument(s) for homomorphic extension, found %d@." ar1 ar2 |
||
164 | 0cbf0839 | ploc | | Undefined_var vmap -> |
165 | fprintf fmt "No definition provided for variable(s): %a@." |
||
166 | (Utils.fprintf_list ~sep:"," pp_print_string) |
||
167 | (fst (Utils.list_of_imap vmap)) |
||
168 | 0b78e972 | xthirioux | | Declared_but_undefined id -> |
169 | fprintf fmt "Node %s is declared but not defined@." id |
||
170 | 0cbf0839 | ploc | | Type_clash (ty1,ty2) -> |
171 | Utils.reset_names (); |
||
172 | fprintf fmt "Expected type %a, got type %a@." print_ty ty1 print_ty ty2 |
||
173 | | Poly_imported_node id -> |
||
174 | fprintf fmt "Imported nodes cannot have a polymorphic type@." |
||
175 | |||
176 | |||
177 | let new_id = ref (-1) |
||
178 | |||
179 | 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 | aa223e69 | 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 | 0cbf0839 | ploc | |
204 | c518d082 | xthirioux | let is_clock_type ty = |
205 | match (repr ty).tdesc with |
||
206 | | Tclock _ -> true |
||
207 | | _ -> false |
||
208 | |||
209 | 0cbf0839 | ploc | let rec is_dimension_type ty = |
210 | match (repr ty).tdesc with |
||
211 | | Tint |
||
212 | | Tbool -> true |
||
213 | | Tclock ty' |
||
214 | | Tstatic (_, ty') -> is_dimension_type ty' |
||
215 | | _ -> false |
||
216 | |||
217 | 14d694c7 | xthirioux | let dynamic_type ty = |
218 | 0cbf0839 | ploc | let ty = repr ty in |
219 | match ty.tdesc with |
||
220 | | Tstatic (_, ty') -> ty' |
||
221 | | _ -> ty |
||
222 | |||
223 | 14d694c7 | xthirioux | let is_tuple_type ty = |
224 | match (repr ty).tdesc with |
||
225 | | Ttuple _ -> true |
||
226 | | _ -> false |
||
227 | |||
228 | let rec is_nested_tuple_type ty = |
||
229 | match (repr ty).tdesc with |
||
230 | | Ttuple tl -> List.exists is_tuple_type tl |
||
231 | | _ -> false |
||
232 | |||
233 | 0cbf0839 | ploc | let map_tuple_type f ty = |
234 | let ty = dynamic_type ty in |
||
235 | match ty.tdesc with |
||
236 | | (Ttuple ty_list) -> { ty with tdesc = Ttuple (List.map f ty_list) } |
||
237 | | _ -> f ty |
||
238 | 51768260 | xthirioux | |
239 | 14d694c7 | xthirioux | let is_struct_type ty = |
240 | 51768260 | xthirioux | match (repr ty).tdesc with |
241 | | Tstruct _ -> true |
||
242 | | _ -> false |
||
243 | |||
244 | 0cbf0839 | ploc | let rec is_array_type ty = |
245 | match (repr ty).tdesc with |
||
246 | | Tarray _ -> true |
||
247 | 51768260 | xthirioux | | Tstatic (_, ty') -> is_array_type ty' (* looks strange !? *) |
248 | 0cbf0839 | ploc | | _ -> false |
249 | |||
250 | let array_type_dimension ty = |
||
251 | match (dynamic_type ty).tdesc with |
||
252 | | Tarray (d, _) -> d |
||
253 | | _ -> assert false |
||
254 | |||
255 | let rec array_type_multi_dimension ty = |
||
256 | match (dynamic_type ty).tdesc with |
||
257 | | Tarray (d, ty') -> d :: array_type_multi_dimension ty' |
||
258 | | _ -> [] |
||
259 | |||
260 | let array_element_type ty = |
||
261 | match (dynamic_type ty).tdesc with |
||
262 | | Tarray (_, ty') -> ty' |
||
263 | | _ -> assert false |
||
264 | |||
265 | let rec array_base_type ty = |
||
266 | let ty = repr ty in |
||
267 | match ty.tdesc with |
||
268 | | Tarray (_, ty') |
||
269 | | Tstatic (_, ty') -> array_base_type ty' |
||
270 | | _ -> ty |
||
271 | |||
272 | 51768260 | xthirioux | let is_address_type ty = |
273 | is_array_type ty || is_struct_type ty |
||
274 | |||
275 | 0cbf0839 | ploc | let rec is_generic_type ty = |
276 | match (dynamic_type ty).tdesc with |
||
277 | | Tarray (d, ty') -> |
||
278 | (not (Dimension.is_dimension_const d)) || (is_generic_type ty') |
||
279 | | _ -> false |
||
280 | |||
281 | (** Splits [ty] into the [lhs,rhs] of an arrow type. Expects an arrow type |
||
282 | (ensured by language syntax) *) |
||
283 | let rec split_arrow ty = |
||
284 | match (repr ty).tdesc with |
||
285 | | Tarrow (tin,tout) -> tin,tout |
||
286 | | Tstatic (_, ty') -> split_arrow ty' |
||
287 | (* Functions are not first order, I don't think the var case |
||
288 | needs to be considered here *) |
||
289 | | _ -> Format.eprintf "%a@." print_ty ty; assert false |
||
290 | |||
291 | (** Returns the type corresponding to a type list. *) |
||
292 | let type_of_type_list tyl = |
||
293 | if (List.length tyl) > 1 then |
||
294 | new_ty (Ttuple tyl) |
||
295 | else |
||
296 | List.hd tyl |
||
297 | |||
298 | let type_list_of_type ty = |
||
299 | match (repr ty).tdesc with |
||
300 | | Ttuple tl -> tl |
||
301 | | _ -> [ty] |
||
302 | |||
303 | (** [is_polymorphic ty] returns true if [ty] is polymorphic. *) |
||
304 | let rec is_polymorphic ty = |
||
305 | match ty.tdesc with |
||
306 | | Tenum _ | Tvar | Tint | Treal | Tbool | Trat | Tconst _ -> false |
||
307 | | Tclock ty -> is_polymorphic ty |
||
308 | | Tarrow (ty1,ty2) -> (is_polymorphic ty1) || (is_polymorphic ty2) |
||
309 | | Ttuple tl -> List.exists (fun t -> is_polymorphic t) tl |
||
310 | aa223e69 | xthirioux | | Tstruct fl -> List.exists (fun (_, t) -> is_polymorphic t) fl |
311 | 0cbf0839 | ploc | | Tlink t' -> is_polymorphic t' |
312 | | Tarray (d, ty) |
||
313 | | Tstatic (d, ty) -> Dimension.is_polymorphic d || is_polymorphic ty |
||
314 | | Tunivar -> true |
||
315 | |||
316 | |||
317 | let mktyptuple nb typ = |
||
318 | let array = Array.make nb typ in |
||
319 | Ttuple (Array.to_list array) |
||
320 | |||
321 | |||
322 | (* Local Variables: *) |
||
323 | (* compile-command:"make -C .." *) |
||
324 | (* End: *) |