Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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
(* Pretty-print*)
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
(* compile-command:"make -C .." *)
564
(* End: *)