Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / types.ml @ 37419cf4

History | View | Annotate | Download (10.6 KB)

1 a2d97a3e ploc
(********************************************************************)
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 22fe1c93 ploc
14
(** Types definitions and a few utility functions on types. *)
15
open Utils
16
open Dimension
17
18
type type_expr =
19
    {mutable tdesc: type_desc;
20
     tid: int}
21
22
and type_desc =
23
  | Tconst of ident (* type constant *)
24
  | Tint
25
  | Treal
26
  | Tbool
27
  | Trat (* Actually unused for now. Only place where it can appear is
28
            in a clock declaration *)
29 6afa892a xthirioux
  | Tclock of type_expr (* A type expression explicitely tagged as carrying a clock *)
30 22fe1c93 ploc
  | Tarrow of type_expr * type_expr
31
  | Ttuple of type_expr list
32
  | Tenum of ident list
33 12af4908 xthirioux
  | Tstruct of (ident * type_expr) list
34 22fe1c93 ploc
  | Tarray of dim_expr * type_expr
35
  | Tstatic of dim_expr * type_expr (* a type carried by a dimension expression *)
36
  | Tlink of type_expr (* During unification, make links instead of substitutions *)
37
  | Tvar (* Monomorphic type variable *)
38
  | Tunivar (* Polymorphic type variable *)
39
40
type error =
41
    Unbound_value of ident  
42
  | Already_bound of ident
43
  | Already_defined of ident
44 ec433d69 xthirioux
  | Undefined_var of ISet.t
45 96f5fe18 xthirioux
  | Declared_but_undefined of ident
46 22fe1c93 ploc
  | Unbound_type of ident
47
  | Not_a_dimension
48
  | Not_a_constant
49 6afa892a xthirioux
  | Assigned_constant of ident
50 22fe1c93 ploc
  | WrongArity of int * int
51 b616fe7a xthirioux
  | WrongMorphism of int * int
52 b1655a21 xthirioux
  | Type_mismatch of ident
53 22fe1c93 ploc
  | Type_clash of type_expr * type_expr
54
  | Poly_imported_node of ident
55
56
exception Unify of type_expr * type_expr
57
exception Error of Location.t * error
58
59
(* Pretty-print*)
60
open Format
61 12af4908 xthirioux
62
let rec print_struct_ty_field fmt (label, ty) =
63
  fprintf fmt "%a : %a" pp_print_string label print_ty ty
64
and print_ty fmt ty =
65 22fe1c93 ploc
  match ty.tdesc with
66
  | Tvar ->
67
    fprintf fmt "_%s" (name_of_type ty.tid)
68
  | Tint ->
69
    fprintf fmt "int"
70
  | Treal ->
71
    fprintf fmt "real"
72
  | Tbool ->
73
    fprintf fmt "bool"
74
  | Tclock t ->
75
    fprintf fmt "%a clock" print_ty t
76
  | Tstatic (d, t) ->
77
    fprintf fmt "(%a:%a)" Dimension.pp_dimension d print_ty t
78
  | Tconst t ->
79
    fprintf fmt "%s" t
80
  | Trat ->
81
    fprintf fmt "rat"
82
  | Tarrow (ty1,ty2) ->
83 719f9992 xthirioux
    fprintf fmt "%a -> %a" print_ty ty1 print_ty ty2
84 22fe1c93 ploc
  | Ttuple tylist ->
85
    fprintf fmt "(%a)"
86 e39f5319 xthirioux
      (Utils.fprintf_list ~sep:" * " print_ty) tylist
87 22fe1c93 ploc
  | Tenum taglist ->
88 12af4908 xthirioux
    fprintf fmt "enum {%a }"
89
      (Utils.fprintf_list ~sep:", " pp_print_string) taglist
90
  | Tstruct fieldlist ->
91
    fprintf fmt "struct {%a }"
92
      (Utils.fprintf_list ~sep:"; " print_struct_ty_field) fieldlist
93 22fe1c93 ploc
  | Tarray (e, ty) ->
94
    fprintf fmt "%a^%a" print_ty ty Dimension.pp_dimension e
95
  | Tlink ty ->
96
      print_ty fmt ty
97
  | Tunivar ->
98
    fprintf fmt "'%s" (name_of_type ty.tid)
99
100 12af4908 xthirioux
let rec print_node_struct_ty_field fmt (label, ty) =
101
  fprintf fmt "%a : %a" pp_print_string label print_node_ty ty
102
and print_node_ty fmt ty =
103 7291cb80 xthirioux
  match ty.tdesc with
104 96f5fe18 xthirioux
  | Tvar -> begin
105 b35da910 xthirioux
(*Format.eprintf "DEBUG:Types.print_node@.";*)
106 96f5fe18 xthirioux
    fprintf fmt "_%s" (name_of_type ty.tid)
107
end
108 7291cb80 xthirioux
  | Tint ->
109
    fprintf fmt "int"
110
  | Treal ->
111
    fprintf fmt "real"
112
  | Tbool ->
113
    fprintf fmt "bool"
114
  | Tclock t ->
115 6afa892a xthirioux
    fprintf fmt "%a clock" print_node_ty t
116 7291cb80 xthirioux
  | Tstatic (_, t) ->
117
    fprintf fmt "%a" print_node_ty t
118
  | Tconst t ->
119
    fprintf fmt "%s" t
120
  | Trat ->
121
    fprintf fmt "rat"
122
  | Tarrow (ty1,ty2) ->
123 6afa892a xthirioux
    fprintf fmt "%a -> %a" print_node_ty ty1 print_node_ty ty2
124 7291cb80 xthirioux
  | Ttuple tylist ->
125
    fprintf fmt "(%a)"
126 6afa892a xthirioux
      (Utils.fprintf_list ~sep:"*" print_node_ty) tylist
127 7291cb80 xthirioux
  | Tenum taglist ->
128 12af4908 xthirioux
    fprintf fmt "enum {%a }"
129
      (Utils.fprintf_list ~sep:", " pp_print_string) taglist
130
  | Tstruct fieldlist ->
131
    fprintf fmt "struct {%a }"
132
      (Utils.fprintf_list ~sep:"; " print_node_struct_ty_field) fieldlist
133 7291cb80 xthirioux
  | Tarray (e, ty) ->
134 6afa892a xthirioux
    fprintf fmt "%a^%a" print_node_ty ty Dimension.pp_dimension e
135 7291cb80 xthirioux
  | Tlink ty ->
136 6afa892a xthirioux
      print_node_ty fmt ty
137 7291cb80 xthirioux
  | Tunivar ->
138
    fprintf fmt "'%s" (name_of_type ty.tid)
139
140 22fe1c93 ploc
let pp_error fmt = function
141
  | Unbound_value id ->
142
    fprintf fmt "Unknown value %s@." id
143
  | Unbound_type id ->
144
    fprintf fmt "Unknown type %s@." id
145
  | Already_bound id ->
146
    fprintf fmt "%s is already declared@." id
147
  | Already_defined id ->
148
    fprintf fmt "Multiple definitions of variable %s@." id
149
  | Not_a_constant ->
150
    fprintf fmt "This expression is not a constant@."
151 6afa892a xthirioux
  | Assigned_constant id ->
152
    fprintf fmt "The constant %s cannot be assigned@." id
153 22fe1c93 ploc
  | Not_a_dimension ->
154
    fprintf fmt "This expression is not a valid dimension@."
155
  | WrongArity (ar1, ar2) ->
156
    fprintf fmt "Expecting %d argument(s), found %d@." ar1 ar2
157 b616fe7a xthirioux
  | WrongMorphism (ar1, ar2) ->
158
    fprintf fmt "Expecting %d argument(s) for homomorphic extension, found %d@." ar1 ar2
159 b1655a21 xthirioux
  | Type_mismatch id ->
160
    fprintf fmt "Definition and declaration of type %s don't agree@." id
161 ec433d69 xthirioux
  | Undefined_var vset ->
162 22fe1c93 ploc
    fprintf fmt "No definition provided for variable(s): %a@."
163
      (Utils.fprintf_list ~sep:"," pp_print_string)
164 ec433d69 xthirioux
      (ISet.elements vset)
165 96f5fe18 xthirioux
  | Declared_but_undefined id ->
166 ef34b4ae xthirioux
     fprintf fmt "%s is declared but not defined@." id
167 22fe1c93 ploc
  | Type_clash (ty1,ty2) ->
168
      Utils.reset_names ();
169
    fprintf fmt "Expected type %a, got type %a@." print_ty ty1 print_ty ty2
170
  | Poly_imported_node id ->
171
    fprintf fmt "Imported nodes cannot have a polymorphic type@."
172
173
174
let new_id = ref (-1)
175
176 04a63d25 xthirioux
let rec bottom =
177
  { tdesc = Tlink bottom; tid = -666 }
178
179 22fe1c93 ploc
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 12af4908 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 22fe1c93 ploc
204 04a63d25 xthirioux
let rec is_scalar_type ty =
205
  match (repr ty).tdesc with
206
  | Tstatic (_, ty) -> is_scalar_type ty
207
  | Tbool
208
  | Tint
209
  | Treal -> true
210
  | _     -> false
211
212
let rec is_numeric_type ty =
213 6afa892a xthirioux
 match (repr ty).tdesc with
214 04a63d25 xthirioux
 | Tstatic (_, ty) -> is_numeric_type ty
215 6afa892a xthirioux
 | Tint
216
 | Treal -> true
217
 | _     -> false
218
219 04a63d25 xthirioux
let rec is_real_type ty =
220
 match (repr ty).tdesc with
221
 | Tstatic (_, ty) -> is_real_type ty
222
 | Treal -> true
223
 | _     -> false
224
225
let rec is_bool_type ty =
226 6afa892a xthirioux
 match (repr ty).tdesc with
227 04a63d25 xthirioux
 | Tstatic (_, ty) -> is_bool_type ty
228 6afa892a xthirioux
 | Tbool -> true
229
 | _     -> false
230
231
let get_clock_base_type ty =
232 8f1c7e91 xthirioux
 match (repr ty).tdesc with
233 6afa892a xthirioux
 | Tclock ty -> Some ty
234
 | _         -> None
235 8f1c7e91 xthirioux
236 e3a4e911 xthirioux
let unclock_type ty =
237
  let ty = repr ty in
238
  match ty.tdesc with
239
  | Tclock ty' -> ty'
240
  | _          -> ty
241
242 22fe1c93 ploc
let rec is_dimension_type ty =
243
 match (repr ty).tdesc with
244
 | Tint
245
 | Tbool -> true
246
 | Tclock ty'
247
 | Tstatic (_, ty') -> is_dimension_type ty'
248
 | _                -> false
249
250 b616fe7a xthirioux
let dynamic_type ty =
251 22fe1c93 ploc
  let ty = repr ty in
252
  match ty.tdesc with
253
  | Tstatic (_, ty') -> ty'
254
  | _                -> ty
255
256 b616fe7a xthirioux
let is_tuple_type ty =
257
 match (repr ty).tdesc with
258
 | Ttuple _         -> true
259
 | _                -> false
260
261 22fe1c93 ploc
let map_tuple_type f ty =
262
  let ty = dynamic_type ty in
263
  match ty.tdesc with
264
  | (Ttuple ty_list) -> { ty with tdesc = Ttuple (List.map f ty_list) }
265
  | _                -> f ty
266 b174e673 xthirioux
267 8a183477 xthirioux
let rec is_struct_type ty =
268 b174e673 xthirioux
 match (repr ty).tdesc with
269
 | Tstruct _        -> true
270 8a183477 xthirioux
 | Tstatic (_, ty') -> is_struct_type ty'
271 b174e673 xthirioux
 | _                -> false
272
273 2d179f5b xthirioux
let struct_field_type ty field =
274
  match (dynamic_type ty).tdesc with
275
  | Tstruct fields ->
276
    (try
277
       List.assoc field fields
278
     with Not_found -> assert false)
279
  | _              -> assert false
280
281 22fe1c93 ploc
let rec is_array_type ty =
282
 match (repr ty).tdesc with
283
 | Tarray _         -> true
284 b174e673 xthirioux
 | Tstatic (_, ty') -> is_array_type ty' (* looks strange !? *)
285 22fe1c93 ploc
 | _                -> false
286
287
let array_type_dimension ty =
288
  match (dynamic_type ty).tdesc with
289
  | Tarray (d, _) -> d
290 fc886259 xthirioux
  | _             -> (Format.eprintf "internal error: Types.array_type_dimension %a@." print_ty ty; assert false)
291 22fe1c93 ploc
292
let rec array_type_multi_dimension ty =
293
  match (dynamic_type ty).tdesc with
294
  | Tarray (d, ty') -> d :: array_type_multi_dimension ty'
295
  | _               -> []
296
297
let array_element_type ty =
298
  match (dynamic_type ty).tdesc with
299
  | Tarray (_, ty') -> ty'
300 fc886259 xthirioux
  | _               -> (Format.eprintf "internal error: Types.array_element_type %a@." print_ty ty; assert false)
301 22fe1c93 ploc
302
let rec array_base_type ty =
303
  let ty = repr ty in
304
  match ty.tdesc with
305
  | Tarray (_, ty')
306
  | Tstatic (_, ty') -> array_base_type ty'
307
  | _                -> ty
308
309 b174e673 xthirioux
let is_address_type ty =
310 04a63d25 xthirioux
  is_array_type ty || is_struct_type ty || (is_real_type ty && !Options.mpfr)
311 b174e673 xthirioux
312 22fe1c93 ploc
let rec is_generic_type ty =
313
 match (dynamic_type ty).tdesc with
314
  | Tarray (d, ty') ->
315
    (not (Dimension.is_dimension_const d)) || (is_generic_type ty')
316
  | _               -> false
317
318
(** Splits [ty] into the [lhs,rhs] of an arrow type. Expects an arrow type
319
    (ensured by language syntax) *)
320
let rec split_arrow ty =
321
  match (repr ty).tdesc with
322
  | Tarrow (tin,tout) -> tin,tout
323
  | Tstatic (_, ty')  -> split_arrow ty'
324
    (* Functions are not first order, I don't think the var case
325
       needs to be considered here *)
326 870420a0 ploc
  | _ -> Format.eprintf "type %a is not a map@.Unable to split@.@?" print_ty ty; assert false
327 22fe1c93 ploc
328
(** Returns the type corresponding to a type list. *)
329
let type_of_type_list tyl =
330
  if (List.length tyl) > 1 then
331
    new_ty (Ttuple tyl)
332
  else
333
    List.hd tyl
334
335 04a63d25 xthirioux
let rec type_list_of_type ty =
336 22fe1c93 ploc
 match (repr ty).tdesc with
337 04a63d25 xthirioux
 | Tstatic (_, ty) -> type_list_of_type ty
338
 | Ttuple tl       -> tl
339
 | _               -> [ty]
340 22fe1c93 ploc
341
(** [is_polymorphic ty] returns true if [ty] is polymorphic. *)
342
let rec is_polymorphic ty =
343
  match ty.tdesc with
344
  | Tenum _ | Tvar | Tint | Treal | Tbool | Trat | Tconst _ -> false
345
  | Tclock ty -> is_polymorphic ty
346
  | Tarrow (ty1,ty2) -> (is_polymorphic ty1) || (is_polymorphic ty2)
347
  | Ttuple tl -> List.exists (fun t -> is_polymorphic t) tl
348 12af4908 xthirioux
  | Tstruct fl -> List.exists (fun (_, t) -> is_polymorphic t) fl
349 22fe1c93 ploc
  | Tlink t' -> is_polymorphic t'
350
  | Tarray (d, ty)
351
  | Tstatic (d, ty) -> Dimension.is_polymorphic d || is_polymorphic ty
352
  | Tunivar -> true
353
354
355
let mktyptuple nb typ =
356
  let array = Array.make nb typ in
357
  Ttuple (Array.to_list array)
358
359
360
(* Local Variables: *)
361
(* compile-command:"make -C .." *)
362
(* End: *)