lustrec / lib / types.ml @ 9b0432bc
History  View  Annotate  Download (16.7 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 
[@@deriving show] 
47  
48 
let type_string_builder = Tstring 
49 
let type_int_builder = Tint 
50 
let type_real_builder = Treal 
51 
let type_bool_builder = Tbool 
52  
53 
open Format 
54 
let pp fmt t = 
55 
match t with 
56 
 Tint > 
57 
fprintf fmt "int" 
58 
 Treal > 
59 
fprintf fmt "real" 
60 
 Tstring > 
61 
fprintf fmt "string" 
62 
 Tbool > 
63 
fprintf fmt "bool" 
64 
 Trat > 
65 
fprintf fmt "rat" 
66  
67 
let pp_c = pp 
68 

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

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

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

199 

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

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

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

558 
module Main : Sbasic = Make (Basic) 
559 
include Main 
560  
561  
562 
(* Local Variables: *) 
563 
(* compilecommand:"make C .." *) 
564 
(* End: *) 