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

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

554 
module Main : Sbasic = Make (Basic) 
555 
include Main 
556  
557  
558 
(* Local Variables: *) 
559 
(* compilecommand:"make C .." *) 
560 
(* End: *) 