lustrec / src / types.ml @ 66359a5e
History  View  Annotate  Download (16.3 KB)
1 
(********************************************************************) 

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  
14 
(** Types definitions and a few utility functions on types. *) 
15 
open Utils 
16 
open Dimension 
17  
18 
module type BASIC_TYPES = 
19 
sig 
20 
type t 
21 
val pp: Format.formatter > t > unit 
22 
val pp_c: Format.formatter > t > unit 
23 
val is_scalar_type: t > bool 
24 
val is_numeric_type: t > bool 
25 
val is_int_type: t > bool 
26 
val is_real_type: t > bool 
27 
val is_bool_type: t > bool 
28 
val is_dimension_type: t > bool 
29 
val type_int_builder: t 
30 
val type_real_builder: t 
31 
val type_bool_builder: t 
32 
val type_string_builder: t 
33 
val unify: t > t > unit 
34 
val is_unifiable: t > t > bool 
35 
end 
36  
37 
module Basic = 
38 
struct 
39 
type t = 
40 
 Tstring 
41 
 Tint 
42 
 Treal 
43 
 Tbool 
44 
 Trat (* Actually unused for now. Only place where it can appear is 
45 
in a clock declaration *) 
46  
47 
let type_string_builder = Tstring 
48 
let type_int_builder = Tint 
49 
let type_real_builder = Treal 
50 
let type_bool_builder = Tbool 
51  
52 
open Format 
53 
let pp fmt t = 
54 
match t with 
55 
 Tint > 
56 
fprintf fmt "int" 
57 
 Treal > 
58 
fprintf fmt "real" 
59 
 Tstring > 
60 
fprintf fmt "string" 
61 
 Tbool > 
62 
fprintf fmt "bool" 
63 
 Trat > 
64 
fprintf fmt "rat" 
65  
66 
let pp_c = pp 
67 

68 
let is_scalar_type t = 
69 
match t with 
70 
 Tbool 
71 
 Tint 
72 
 Treal > true 
73 
 _ > false 
74  
75  
76 
let is_numeric_type t = 
77 
match t with 
78 
 Tint 
79 
 Treal > true 
80 
 _ > false 
81  
82 
let is_int_type t = t = Tint 
83 
let is_real_type t = t = Treal 
84 
let is_bool_type t = t = Tbool 
85  
86 
let is_dimension_type t = 
87 
match t with 
88 
 Tint 
89 
 Tbool > true 
90 
 _ > false 
91  
92 
let is_unifiable b1 b2 = b1 == b2 
93 
let unify _ _ = () 
94 
end 
95  
96  
97 

98 
module Make(BasicT : BASIC_TYPES) = 
99 
struct 
100  
101 
module BasicT = BasicT 
102 
type basic_type = BasicT.t 
103 
type type_expr = 
104 
{mutable tdesc: type_desc; 
105 
tid: int} 
106 
and type_desc = 
107 
 Tconst of ident (* type constant *) 
108 
 Tbasic of basic_type 
109 
 Tclock of type_expr (* A type expression explicitely tagged as carrying a clock *) 
110 
 Tarrow of type_expr * type_expr 
111 
 Ttuple of type_expr list 
112 
 Tenum of ident list 
113 
 Tstruct of (ident * type_expr) list 
114 
 Tarray of dim_expr * type_expr 
115 
 Tstatic of dim_expr * type_expr (* a type carried by a dimension expression *) 
116 
 Tlink of type_expr (* During unification, make links instead of substitutions *) 
117 
 Tvar (* Monomorphic type variable *) 
118 
 Tunivar (* Polymorphic type variable *) 
119  
120 
(* {mutable tdesc: type_desc; *) 
121 
(* tid: int} *) 
122  
123 
(* and type_desc = *) 
124 
(*  Tconst of ident (\* type constant *\) *) 
125 
(*  Tbasic of BasicT.t *) 
126 
(*  Tclock of type_expr (\* A type expression explicitely tagged as carrying a clock *\) *) 
127 
(*  Tarrow of type_expr * type_expr *) 
128 
(*  Ttuple of type_expr list *) 
129 
(*  Tenum of ident list *) 
130 
(*  Tstruct of (ident * type_expr) list *) 
131 
(*  Tarray of dim_expr * type_expr *) 
132 
(*  Tstatic of dim_expr * type_expr (\* a type carried by a dimension expression *\) *) 
133 
(*  Tlink of type_expr (\* During unification, make links instead of substitutions *\) *) 
134 
(*  Tvar (\* Monomorphic type variable *\) *) 
135 
(*  Tunivar (\* Polymorphic type variable *\) *) 
136  
137 
type error = 
138 
Unbound_value of ident 
139 
 Already_bound of ident 
140 
 Already_defined of ident 
141 
 Undefined_var of ISet.t 
142 
 Declared_but_undefined of ident 
143 
 Unbound_type of ident 
144 
 Not_a_dimension 
145 
 Not_a_constant 
146 
 Assigned_constant of ident 
147 
 WrongArity of int * int 
148 
 WrongMorphism of int * int 
149 
 Type_mismatch of ident 
150 
 Type_clash of type_expr * type_expr 
151 
 Poly_imported_node of ident 
152  
153 
exception Unify of type_expr * type_expr 
154 
exception Error of Location.t * error 
155  
156 
let mk_basic t = Tbasic t 
157  
158 

159 
(* Prettyprint*) 
160 
open Format 
161  
162 
let rec print_struct_ty_field pp_basic fmt (label, ty) = 
163 
fprintf fmt "%a : %a" pp_print_string label (print_ty_param pp_basic) ty 
164 
and print_ty_param pp_basic fmt ty = 
165 
let print_ty = print_ty_param pp_basic in 
166 
match ty.tdesc with 
167 
 Tvar > 
168 
fprintf fmt "_%s" (name_of_type ty.tid) 
169 
 Tbasic t > pp_basic fmt t 
170 
 Tclock t > 
171 
fprintf fmt "%a clock" print_ty t 
172 
 Tstatic (d, t) > 
173 
fprintf fmt "(%a:%a)" Dimension.pp_dimension d print_ty t 
174 
 Tconst t > 
175 
fprintf fmt "%s" t 
176 
 Tarrow (ty1,ty2) > 
177 
fprintf fmt "%a > %a" print_ty ty1 print_ty ty2 
178 
 Ttuple tylist > 
179 
fprintf fmt "(%a)" 
180 
(Utils.fprintf_list ~sep:" * " print_ty) tylist 
181 
 Tenum taglist > 
182 
fprintf fmt "enum {%a }" 
183 
(Utils.fprintf_list ~sep:", " pp_print_string) taglist 
184 
 Tstruct fieldlist > 
185 
fprintf fmt "struct {%a }" 
186 
(Utils.fprintf_list ~sep:"; " (print_struct_ty_field pp_basic)) fieldlist 
187 
 Tarray (e, ty) > 
188 
fprintf fmt "%a^%a" print_ty ty Dimension.pp_dimension e 
189 
 Tlink ty > 
190 
print_ty fmt ty 
191 
 Tunivar > 
192 
fprintf fmt "'%s" (name_of_type ty.tid) 
193  
194 
let print_ty = print_ty_param BasicT.pp 
195 

196 

197 
let rec print_node_struct_ty_field fmt (label, ty) = 
198 
fprintf fmt "%a : %a" pp_print_string label print_node_ty ty 
199 
and print_node_ty fmt ty = 
200 
match ty.tdesc with 
201 
 Tvar > begin 
202 
(*Format.eprintf "DEBUG:Types.print_node@.";*) 
203 
fprintf fmt "_%s" (name_of_type ty.tid) 
204 
end 
205 
 Tbasic t > BasicT.pp fmt t 
206 
 Tclock t > 
207 
fprintf fmt "%a clock" print_node_ty t 
208 
 Tstatic (_, t) > 
209 
fprintf fmt "%a" print_node_ty t 
210 
 Tconst t > 
211 
fprintf fmt "%s" t 
212 
 Tarrow (ty1,ty2) > 
213 
fprintf fmt "%a > %a" print_node_ty ty1 print_node_ty ty2 
214 
 Ttuple tylist > 
215 
fprintf fmt "(%a)" 
216 
(Utils.fprintf_list ~sep:"*" print_node_ty) tylist 
217 
 Tenum taglist > 
218 
fprintf fmt "enum {%a }" 
219 
(Utils.fprintf_list ~sep:", " pp_print_string) taglist 
220 
 Tstruct fieldlist > 
221 
fprintf fmt "struct {%a }" 
222 
(Utils.fprintf_list ~sep:"; " print_node_struct_ty_field) fieldlist 
223 
 Tarray (e, ty) > 
224 
fprintf fmt "%a^%a" print_node_ty ty Dimension.pp_dimension e 
225 
 Tlink ty > 
226 
print_node_ty fmt ty 
227 
 Tunivar > 
228 
fprintf fmt "'%s" (name_of_type ty.tid) 
229  
230 
let pp_error fmt = function 
231 
 Unbound_value id > 
232 
fprintf fmt "Unknown value %s@." id 
233 
 Unbound_type id > 
234 
fprintf fmt "Unknown type %s@." id 
235 
 Already_bound id > 
236 
fprintf fmt "%s is already declared@." id 
237 
 Already_defined id > 
238 
fprintf fmt "Multiple definitions of variable %s@." id 
239 
 Not_a_constant > 
240 
fprintf fmt "This expression is not a constant@." 
241 
 Assigned_constant id > 
242 
fprintf fmt "The constant %s cannot be assigned@." id 
243 
 Not_a_dimension > 
244 
fprintf fmt "This expression is not a valid dimension@." 
245 
 WrongArity (ar1, ar2) > 
246 
fprintf fmt "Expecting %d argument(s), found %d@." ar1 ar2 
247 
 WrongMorphism (ar1, ar2) > 
248 
fprintf fmt "Expecting %d argument(s) for homomorphic extension, found %d@." ar1 ar2 
249 
 Type_mismatch id > 
250 
fprintf fmt "Definition and declaration of type %s don't agree@." id 
251 
 Undefined_var vset > 
252 
fprintf fmt "No definition provided for variable(s): %a@." 
253 
(Utils.fprintf_list ~sep:"," pp_print_string) 
254 
(ISet.elements vset) 
255 
 Declared_but_undefined id > 
256 
fprintf fmt "%s is declared but not defined@." id 
257 
 Type_clash (ty1,ty2) > 
258 
Utils.reset_names (); 
259 
fprintf fmt "Expected type %a, got type %a@." print_ty ty1 print_ty ty2 
260 
 Poly_imported_node id > 
261 
fprintf fmt "Imported nodes cannot have a polymorphic type@." 
262  
263  
264 
let new_id = ref (1) 
265  
266 
let rec bottom = 
267 
{ tdesc = Tlink bottom; tid = 666 } 
268  
269 
let new_ty desc = 
270 
incr new_id; {tdesc = desc; tid = !new_id } 
271  
272 
let new_var () = 
273 
new_ty Tvar 
274  
275 
let new_univar () = 
276 
new_ty Tunivar 
277  
278 
let rec repr = 
279 
function 
280 
{tdesc = Tlink t'} > 
281 
repr t' 
282 
 t > t 
283  
284 
let get_static_value ty = 
285 
match (repr ty).tdesc with 
286 
 Tstatic (d, _) > Some d 
287 
 _ > None 
288  
289 
let get_field_type ty label = 
290 
match (repr ty).tdesc with 
291 
 Tstruct fl > (try Some (List.assoc label fl) with Not_found > None) 
292 
 _ > None 
293  
294 
let rec is_static_type ty = 
295 
match (repr ty).tdesc with 
296 
 Tstatic (_, ty) > true 
297 
 _ > false 
298  
299 
let rec is_scalar_type ty = 
300 
match (repr ty).tdesc with 
301 
 Tstatic (_, ty) > is_scalar_type ty 
302 
 Tbasic t > BasicT.is_scalar_type t 
303 
 _ > false 
304  
305 
let rec is_numeric_type ty = 
306 
match (repr ty).tdesc with 
307 
 Tstatic (_, ty) > is_numeric_type ty 
308 
 Tbasic t > BasicT.is_numeric_type t 
309 
 _ > false 
310 

311 
let rec is_real_type ty = 
312 
match (repr ty).tdesc with 
313 
 Tstatic (_, ty) > is_real_type ty 
314 
 Tbasic t > BasicT.is_real_type t 
315 
 _ > false 
316  
317 
let rec is_int_type ty = 
318 
match (repr ty).tdesc with 
319 
 Tstatic (_, ty) > is_int_type ty 
320 
 Tbasic t > BasicT.is_int_type t 
321 
 _ > false 
322  
323 
let rec is_bool_type ty = 
324 
match (repr ty).tdesc with 
325 
 Tstatic (_, ty) > is_bool_type ty 
326 
 Tbasic t > BasicT.is_bool_type t 
327 
 _ > false 
328  
329 
let get_clock_base_type ty = 
330 
match (repr ty).tdesc with 
331 
 Tclock ty > Some ty 
332 
 _ > None 
333  
334 
let unclock_type ty = 
335 
let ty = repr ty in 
336 
match ty.tdesc with 
337 
 Tclock ty' > ty' 
338 
 _ > ty 
339  
340 
let rec is_dimension_type ty = 
341 
match (repr ty).tdesc with 
342 
 Tbasic t > BasicT.is_dimension_type t 
343 
 Tclock ty' 
344 
 Tstatic (_, ty') > is_dimension_type ty' 
345 
 _ > false 
346  
347 
let dynamic_type ty = 
348 
let ty = repr ty in 
349 
match ty.tdesc with 
350 
 Tstatic (_, ty') > ty' 
351 
 _ > ty 
352  
353 
let is_tuple_type ty = 
354 
match (repr ty).tdesc with 
355 
 Ttuple _ > true 
356 
 _ > false 
357  
358 
let map_tuple_type f ty = 
359 
let ty = dynamic_type ty in 
360 
match ty.tdesc with 
361 
 (Ttuple ty_list) > { ty with tdesc = Ttuple (List.map f ty_list) } 
362 
 _ > f ty 
363  
364 
let rec is_struct_type ty = 
365 
match (repr ty).tdesc with 
366 
 Tstruct _ > true 
367 
 Tstatic (_, ty') > is_struct_type ty' 
368 
 _ > false 
369  
370 
let struct_field_type ty field = 
371 
match (dynamic_type ty).tdesc with 
372 
 Tstruct fields > 
373 
(try 
374 
List.assoc field fields 
375 
with Not_found > assert false) 
376 
 _ > assert false 
377  
378 
let rec is_array_type ty = 
379 
match (repr ty).tdesc with 
380 
 Tarray _ > true 
381 
 Tstatic (_, ty') > is_array_type ty' (* looks strange !? *) 
382 
 _ > false 
383  
384 
let array_type_dimension ty = 
385 
match (dynamic_type ty).tdesc with 
386 
 Tarray (d, _) > d 
387 
 _ > (Format.eprintf "internal error: Types.array_type_dimension %a@." print_ty ty; assert false) 
388  
389 
let rec array_type_multi_dimension ty = 
390 
match (dynamic_type ty).tdesc with 
391 
 Tarray (d, ty') > d :: array_type_multi_dimension ty' 
392 
 _ > [] 
393  
394 
let array_element_type ty = 
395 
match (dynamic_type ty).tdesc with 
396 
 Tarray (_, ty') > ty' 
397 
 _ > (Format.eprintf "internal error: Types.array_element_type %a@." print_ty ty; assert false) 
398  
399 
let rec array_base_type ty = 
400 
let ty = repr ty in 
401 
match ty.tdesc with 
402 
 Tarray (_, ty') 
403 
 Tstatic (_, ty') > array_base_type ty' 
404 
 _ > ty 
405  
406 
let is_address_type ty = 
407 
is_array_type ty  is_struct_type ty  (is_real_type ty && !Options.mpfr) 
408  
409 
let rec is_generic_type ty = 
410 
match (dynamic_type ty).tdesc with 
411 
 Tarray (d, ty') > 
412 
(not (Dimension.is_dimension_const d))  (is_generic_type ty') 
413 
 _ > false 
414  
415 
(** Splits [ty] into the [lhs,rhs] of an arrow type. Expects an arrow type 
416 
(ensured by language syntax) *) 
417 
let rec split_arrow ty = 
418 
match (repr ty).tdesc with 
419 
 Tarrow (tin,tout) > tin,tout 
420 
 Tstatic (_, ty') > split_arrow ty' 
421 
(* Functions are not first order, I don't think the var case 
422 
needs to be considered here *) 
423 
 _ > Format.eprintf "type %a is not a map@.Unable to split@.@?" print_ty ty; assert false 
424  
425 
(** Returns the type corresponding to a type list. *) 
426 
let type_of_type_list tyl = 
427 
if (List.length tyl) > 1 then 
428 
new_ty (Ttuple tyl) 
429 
else 
430 
List.hd tyl 
431  
432 
let rec type_list_of_type ty = 
433 
match (repr ty).tdesc with 
434 
 Tstatic (_, ty) > type_list_of_type ty 
435 
 Ttuple tl > tl 
436 
 _ > [ty] 
437  
438 
(** [is_polymorphic ty] returns true if [ty] is polymorphic. *) 
439 
let rec is_polymorphic ty = 
440 
match ty.tdesc with 
441 
 Tenum _  Tvar  Tbasic _  Tconst _ > false 
442 
 Tclock ty > is_polymorphic ty 
443 
 Tarrow (ty1,ty2) > (is_polymorphic ty1)  (is_polymorphic ty2) 
444 
 Ttuple tl > List.exists (fun t > is_polymorphic t) tl 
445 
 Tstruct fl > List.exists (fun (_, t) > is_polymorphic t) fl 
446 
 Tlink t' > is_polymorphic t' 
447 
 Tarray (d, ty) 
448 
 Tstatic (d, ty) > Dimension.is_polymorphic d  is_polymorphic ty 
449 
 Tunivar > true 
450  
451  
452 
let mktyptuple nb typ = 
453 
let array = Array.make nb typ in 
454 
Ttuple (Array.to_list array) 
455  
456 
let type_desc t = t.tdesc 
457  
458  
459  
460 
let type_int = mk_basic BasicT.type_int_builder 
461 
let type_real = mk_basic BasicT.type_real_builder 
462 
let type_bool = mk_basic BasicT.type_bool_builder 
463 
let type_string = mk_basic BasicT.type_string_builder 
464 

465 
end 
466  
467  
468 
module type S = 
469 
sig 
470 
module BasicT: BASIC_TYPES 
471 
type basic_type = BasicT.t 
472 
type type_expr = 
473 
{mutable tdesc: type_desc; 
474 
tid: int} 
475 
and type_desc = 
476 
 Tconst of ident (* type constant *) 
477 
 Tbasic of basic_type 
478 
 Tclock of type_expr (* A type expression explicitely tagged as carrying a clock *) 
479 
 Tarrow of type_expr * type_expr 
480 
 Ttuple of type_expr list 
481 
 Tenum of ident list 
482 
 Tstruct of (ident * type_expr) list 
483 
 Tarray of dim_expr * type_expr 
484 
 Tstatic of dim_expr * type_expr (* a type carried by a dimension expression *) 
485 
 Tlink of type_expr (* During unification, make links instead of substitutions *) 
486 
 Tvar (* Monomorphic type variable *) 
487 
 Tunivar (* Polymorphic type variable *) 
488  
489 
type error = 
490 
Unbound_value of ident 
491 
 Already_bound of ident 
492 
 Already_defined of ident 
493 
 Undefined_var of ISet.t 
494 
 Declared_but_undefined of ident 
495 
 Unbound_type of ident 
496 
 Not_a_dimension 
497 
 Not_a_constant 
498 
 Assigned_constant of ident 
499 
 WrongArity of int * int 
500 
 WrongMorphism of int * int 
501 
 Type_mismatch of ident 
502 
 Type_clash of type_expr * type_expr 
503 
 Poly_imported_node of ident 
504  
505 
exception Unify of type_expr * type_expr 
506 
exception Error of Location.t * error 
507  
508 
val is_real_type: type_expr > bool 
509 
val is_int_type: type_expr > bool 
510 
val is_bool_type: type_expr > bool 
511 
val is_static_type: type_expr > bool 
512 
val is_array_type: type_expr > bool 
513 
val is_dimension_type: type_expr > bool 
514 
val is_address_type: type_expr > bool 
515 
val is_generic_type: type_expr > bool 
516 
val print_ty: Format.formatter > type_expr > unit 
517 
val repr: type_expr > type_expr 
518 
val dynamic_type: type_expr > type_expr 
519 
val type_desc: type_expr > type_desc 
520 
val new_var: unit > type_expr 
521 
val new_univar: unit > type_expr 
522 
val new_ty: type_desc > type_expr 
523 
val type_int: type_desc 
524 
val type_real: type_desc 
525 
val type_bool: type_desc 
526 
val type_string: type_desc 
527 
val array_element_type: type_expr > type_expr 
528 
val type_list_of_type: type_expr > type_expr list 
529 
val print_node_ty: Format.formatter > type_expr > unit 
530 
val get_clock_base_type: type_expr > type_expr option 
531 
val get_static_value: type_expr > Dimension.dim_expr option 
532 
val is_tuple_type: type_expr > bool 
533 
val type_of_type_list: type_expr list > type_expr 
534 
val split_arrow: type_expr > type_expr * type_expr 
535 
val unclock_type: type_expr > type_expr 
536 
val bottom: type_expr 
537 
val map_tuple_type: (type_expr > type_expr) > type_expr > type_expr 
538 
val array_base_type: type_expr > type_expr 
539 
val array_type_dimension: type_expr > Dimension.dim_expr 
540 
val pp_error: Format.formatter > error > unit 
541 
val struct_field_type: type_expr > ident > type_expr 
542 
val array_type_multi_dimension: type_expr > Dimension.dim_expr list 
543 
end (* with type type_expr = BasicT.t type_expr_gen *) 
544  
545 
module type Sbasic = S with type BasicT.t = Basic.t 
546 

547 
module Main : Sbasic = Make (Basic) 
548 
include Main 
549  
550  
551 
(* Local Variables: *) 
552 
(* compilecommand:"make C .." *) 
553 
(* End: *) 