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
|
(** Main typing module. Classic inference algorithm with destructive
|
15
|
unification. *)
|
16
|
|
17
|
let debug fmt args = () (* Format.eprintf "%a" *)
|
18
|
(* Though it shares similarities with the clock calculus module, no code
|
19
|
is shared. Simple environments, very limited identifier scoping, no
|
20
|
identifier redefinition allowed. *)
|
21
|
|
22
|
open Utils
|
23
|
(* Yes, opening both modules is dirty as some type names will be
|
24
|
overwritten, yet this makes notations far lighter.*)
|
25
|
open LustreSpec
|
26
|
open Corelang
|
27
|
(* open Types *)
|
28
|
open Format
|
29
|
|
30
|
|
31
|
module type EXPR_TYPE_HUB =
|
32
|
sig
|
33
|
type type_expr
|
34
|
val import: Types.Main.type_expr -> type_expr
|
35
|
val export: type_expr -> Types.Main.type_expr
|
36
|
end
|
37
|
|
38
|
module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.type_expr) =
|
39
|
struct
|
40
|
|
41
|
module TP = Type_predef.Make (T)
|
42
|
include TP
|
43
|
|
44
|
let basic_coretype_type t =
|
45
|
if is_real_type t then Tydec_real else
|
46
|
if is_int_type t then Tydec_int else
|
47
|
if is_bool_type t then Tydec_bool else
|
48
|
assert false
|
49
|
|
50
|
|
51
|
|
52
|
let pp_typing_env fmt env =
|
53
|
Env.pp_env print_ty fmt env
|
54
|
|
55
|
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in
|
56
|
type [ty]. False otherwise. *)
|
57
|
let rec occurs tvar ty =
|
58
|
let ty = repr ty in
|
59
|
match type_desc ty with
|
60
|
| Tvar -> ty=tvar
|
61
|
| Tarrow (t1, t2) ->
|
62
|
(occurs tvar t1) || (occurs tvar t2)
|
63
|
| Ttuple tl ->
|
64
|
List.exists (occurs tvar) tl
|
65
|
| Tstruct fl ->
|
66
|
List.exists (fun (f, t) -> occurs tvar t) fl
|
67
|
| Tarray (_, t)
|
68
|
| Tstatic (_, t)
|
69
|
| Tclock t
|
70
|
| Tlink t -> occurs tvar t
|
71
|
| Tenum _ | Tconst _ | Tunivar | Tbasic _ -> false
|
72
|
|
73
|
(** Promote monomorphic type variables to polymorphic type variables. *)
|
74
|
(* Generalize by side-effects *)
|
75
|
let rec generalize ty =
|
76
|
match type_desc ty with
|
77
|
| Tvar ->
|
78
|
(* No scopes, always generalize *)
|
79
|
ty.tdesc <- Tunivar
|
80
|
| Tarrow (t1,t2) ->
|
81
|
generalize t1; generalize t2
|
82
|
| Ttuple tl ->
|
83
|
List.iter generalize tl
|
84
|
| Tstruct fl ->
|
85
|
List.iter (fun (f, t) -> generalize t) fl
|
86
|
| Tstatic (d, t)
|
87
|
| Tarray (d, t) -> Dimension.generalize d; generalize t
|
88
|
| Tclock t
|
89
|
| Tlink t ->
|
90
|
generalize t
|
91
|
| Tenum _ | Tconst _ | Tunivar | Tbasic _ -> ()
|
92
|
|
93
|
(** Downgrade polymorphic type variables to monomorphic type variables *)
|
94
|
let rec instantiate inst_vars inst_dim_vars ty =
|
95
|
let ty = repr ty in
|
96
|
match ty.tdesc with
|
97
|
| Tenum _ | Tconst _ | Tvar | Tbasic _ -> ty
|
98
|
| Tarrow (t1,t2) ->
|
99
|
{ty with tdesc =
|
100
|
Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))}
|
101
|
| Ttuple tlist ->
|
102
|
{ty with tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist)}
|
103
|
| Tstruct flist ->
|
104
|
{ty with tdesc = Tstruct (List.map (fun (f, t) -> (f, instantiate inst_vars inst_dim_vars t)) flist)}
|
105
|
| Tclock t ->
|
106
|
{ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t)}
|
107
|
| Tstatic (d, t) ->
|
108
|
{ty with tdesc = Tstatic (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)}
|
109
|
| Tarray (d, t) ->
|
110
|
{ty with tdesc = Tarray (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)}
|
111
|
| Tlink t ->
|
112
|
(* should not happen *)
|
113
|
{ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t)}
|
114
|
| Tunivar ->
|
115
|
try
|
116
|
List.assoc ty.tid !inst_vars
|
117
|
with Not_found ->
|
118
|
let var = new_var () in
|
119
|
inst_vars := (ty.tid, var)::!inst_vars;
|
120
|
var
|
121
|
|
122
|
(* [type_coretype cty] types the type declaration [cty] *)
|
123
|
let rec type_coretype type_dim cty =
|
124
|
match (*get_repr_type*) cty with
|
125
|
| Tydec_any -> new_var ()
|
126
|
| Tydec_int -> type_int
|
127
|
| Tydec_real -> (* Type_predef. *)type_real
|
128
|
(* | Tydec_float -> Type_predef.type_real *)
|
129
|
| Tydec_bool -> (* Type_predef. *)type_bool
|
130
|
| Tydec_clock ty -> (* Type_predef. *)type_clock (type_coretype type_dim ty)
|
131
|
| Tydec_const c -> (* Type_predef. *)type_const c
|
132
|
| Tydec_enum tl -> (* Type_predef. *)type_enum tl
|
133
|
| Tydec_struct fl -> (* Type_predef. *)type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl)
|
134
|
| Tydec_array (d, ty) ->
|
135
|
begin
|
136
|
let d = Dimension.copy (ref []) d in
|
137
|
type_dim d;
|
138
|
(* Type_predef. *)type_array d (type_coretype type_dim ty)
|
139
|
end
|
140
|
|
141
|
(* [coretype_type] is the reciprocal of [type_typecore] *)
|
142
|
let rec coretype_type ty =
|
143
|
match (repr ty).tdesc with
|
144
|
| Tvar -> Tydec_any
|
145
|
| Tbasic _ -> basic_coretype_type ty
|
146
|
| Tconst c -> Tydec_const c
|
147
|
| Tclock t -> Tydec_clock (coretype_type t)
|
148
|
| Tenum tl -> Tydec_enum tl
|
149
|
| Tstruct fl -> Tydec_struct (List.map (fun (f, t) -> (f, coretype_type t)) fl)
|
150
|
| Tarray (d, t) -> Tydec_array (d, coretype_type t)
|
151
|
| Tstatic (_, t) -> coretype_type t
|
152
|
| _ -> assert false
|
153
|
|
154
|
let get_coretype_definition tname =
|
155
|
try
|
156
|
let top = Hashtbl.find type_table (Tydec_const tname) in
|
157
|
match top.top_decl_desc with
|
158
|
| TypeDef tdef -> tdef.tydef_desc
|
159
|
| _ -> assert false
|
160
|
with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
|
161
|
|
162
|
let get_type_definition tname =
|
163
|
type_coretype (fun d -> ()) (get_coretype_definition tname)
|
164
|
|
165
|
(* Equality on ground types only *)
|
166
|
(* Should be used between local variables which must have a ground type *)
|
167
|
let rec eq_ground t1 t2 =
|
168
|
let t1 = repr t1 in
|
169
|
let t2 = repr t2 in
|
170
|
t1==t2 ||
|
171
|
match t1.tdesc, t2.tdesc with
|
172
|
| Tbasic t1, Tbasic t2 when t1 == t2 -> true
|
173
|
| Tenum tl, Tenum tl' when tl == tl' -> true
|
174
|
| Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> List.for_all2 eq_ground tl tl'
|
175
|
| Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' -> List.for_all2 (fun (_, t) (_, t') -> eq_ground t t') fl fl'
|
176
|
| (Tconst t, _) ->
|
177
|
let def_t = get_type_definition t in
|
178
|
eq_ground def_t t2
|
179
|
| (_, Tconst t) ->
|
180
|
let def_t = get_type_definition t in
|
181
|
eq_ground t1 def_t
|
182
|
| Tarrow (t1,t2), Tarrow (t1',t2') -> eq_ground t1 t1' && eq_ground t2 t2'
|
183
|
| Tclock t1', Tclock t2' -> eq_ground t1' t2'
|
184
|
| Tstatic (e1, t1'), Tstatic (e2, t2')
|
185
|
| Tarray (e1, t1'), Tarray (e2, t2') -> Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'
|
186
|
| _ -> false
|
187
|
|
188
|
(** [unify t1 t2] unifies types [t1] and [t2]
|
189
|
using standard destructive unification.
|
190
|
Raises [Unify (t1,t2)] if the types are not unifiable.
|
191
|
[t1] is a expected/formal/spec type, [t2] is a computed/real/implem type,
|
192
|
so in case of unification error: expected type [t1], got type [t2].
|
193
|
If [sub]-typing is allowed, [t2] may be a subtype of [t1].
|
194
|
If [semi] unification is required,
|
195
|
[t1] should furthermore be an instance of [t2]
|
196
|
and constants are handled differently.*)
|
197
|
let unify ?(sub=false) ?(semi=false) t1 t2 =
|
198
|
let rec unif t1 t2 =
|
199
|
let t1 = repr t1 in
|
200
|
let t2 = repr t2 in
|
201
|
if t1==t2 then
|
202
|
()
|
203
|
else
|
204
|
match t1.tdesc,t2.tdesc with
|
205
|
(* strictly subtyping cases first *)
|
206
|
| _ , Tclock t2 when sub && (get_clock_base_type t1 = None) ->
|
207
|
unif t1 t2
|
208
|
| _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) ->
|
209
|
unif t1 t2
|
210
|
(* This case is not mandatory but will keep "older" types *)
|
211
|
| Tvar, Tvar ->
|
212
|
if t1.tid < t2.tid then
|
213
|
t2.tdesc <- Tlink t1
|
214
|
else
|
215
|
t1.tdesc <- Tlink t2
|
216
|
| Tvar, _ when (not semi) && (not (occurs t1 t2)) ->
|
217
|
t1.tdesc <- Tlink t2
|
218
|
| _, Tvar when (not (occurs t2 t1)) ->
|
219
|
t2.tdesc <- Tlink t1
|
220
|
| Tarrow (t1,t2), Tarrow (t1',t2') ->
|
221
|
begin
|
222
|
unif t2 t2';
|
223
|
unif t1' t1
|
224
|
end
|
225
|
| Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
|
226
|
List.iter2 unif tl tl'
|
227
|
| Ttuple [t1] , _ -> unif t1 t2
|
228
|
| _ , Ttuple [t2] -> unif t1 t2
|
229
|
| Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
|
230
|
List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'
|
231
|
| Tclock _, Tstatic _
|
232
|
| Tstatic _, Tclock _ -> raise (Unify (t1, t2))
|
233
|
| Tclock t1', Tclock t2' -> unif t1' t2'
|
234
|
| Tbasic t1, Tbasic t2 when t1 == t2 -> ()
|
235
|
| Tunivar, _ | _, Tunivar -> ()
|
236
|
| (Tconst t, _) ->
|
237
|
let def_t = get_type_definition t in
|
238
|
unif def_t t2
|
239
|
| (_, Tconst t) ->
|
240
|
let def_t = get_type_definition t in
|
241
|
unif t1 def_t
|
242
|
| Tenum tl, Tenum tl' when tl == tl' -> ()
|
243
|
| Tstatic (e1, t1'), Tstatic (e2, t2')
|
244
|
| Tarray (e1, t1'), Tarray (e2, t2') ->
|
245
|
let eval_const =
|
246
|
if semi
|
247
|
then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c))
|
248
|
else (fun c -> None) in
|
249
|
begin
|
250
|
unif t1' t2';
|
251
|
Dimension.eval Basic_library.eval_env eval_const e1;
|
252
|
Dimension.eval Basic_library.eval_env eval_const e2;
|
253
|
Dimension.unify ~semi:semi e1 e2;
|
254
|
end
|
255
|
(* Special cases for machine_types. Rules to unify static types infered
|
256
|
for numerical constants with non static ones for variables with
|
257
|
possible machine types *)
|
258
|
| Tbasic bt1, Tbasic bt2 when BasicT.is_unifiable bt1 bt2 -> BasicT.unify bt1 bt2
|
259
|
| _,_ -> raise (Unify (t1, t2))
|
260
|
in unif t1 t2
|
261
|
|
262
|
(* Expected type ty1, got type ty2 *)
|
263
|
let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =
|
264
|
try
|
265
|
unify ~sub:sub ~semi:semi ty1 ty2
|
266
|
with
|
267
|
| Unify _ ->
|
268
|
raise (Error (loc, Type_clash (ty1,ty2)))
|
269
|
| Dimension.Unify _ ->
|
270
|
raise (Error (loc, Type_clash (ty1,ty2)))
|
271
|
|
272
|
let rec type_struct_const_field ?(is_annot=false) loc (label, c) =
|
273
|
if Hashtbl.mem field_table label
|
274
|
then let tydef = Hashtbl.find field_table label in
|
275
|
let tydec = (typedef_of_top tydef).tydef_desc in
|
276
|
let tydec_struct = get_struct_type_fields tydec in
|
277
|
let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
|
278
|
begin
|
279
|
try_unify ty_label (type_const ~is_annot loc c) loc;
|
280
|
type_coretype (fun d -> ()) tydec
|
281
|
end
|
282
|
else raise (Error (loc, Unbound_value ("struct field " ^ label)))
|
283
|
|
284
|
and type_const ?(is_annot=false) loc c =
|
285
|
match c with
|
286
|
| Const_int _ -> (* Type_predef. *)type_int
|
287
|
| Const_real _ -> (* Type_predef. *)type_real
|
288
|
(* | Const_float _ -> Type_predef.type_real *)
|
289
|
| Const_array ca -> let d = Dimension.mkdim_int loc (List.length ca) in
|
290
|
let ty = new_var () in
|
291
|
List.iter (fun e -> try_unify ty (type_const ~is_annot loc e) loc) ca;
|
292
|
(* Type_predef. *)type_array d ty
|
293
|
| Const_tag t ->
|
294
|
if Hashtbl.mem tag_table t
|
295
|
then
|
296
|
let tydef = typedef_of_top (Hashtbl.find tag_table t) in
|
297
|
let tydec =
|
298
|
if is_user_type tydef.tydef_desc
|
299
|
then Tydec_const tydef.tydef_id
|
300
|
else tydef.tydef_desc in
|
301
|
type_coretype (fun d -> ()) tydec
|
302
|
else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
|
303
|
| Const_struct fl ->
|
304
|
let ty_struct = new_var () in
|
305
|
begin
|
306
|
let used =
|
307
|
List.fold_left
|
308
|
(fun acc (l, c) ->
|
309
|
if List.mem l acc
|
310
|
then raise (Error (loc, Already_bound ("struct field " ^ l)))
|
311
|
else try_unify ty_struct (type_struct_const_field ~is_annot loc (l, c)) loc; l::acc)
|
312
|
[] fl in
|
313
|
try
|
314
|
let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in
|
315
|
(* List.iter (fun l -> Format.eprintf "total: %s@." l) total;
|
316
|
List.iter (fun l -> Format.eprintf "used: %s@." l) used; *)
|
317
|
let undef = List.find (fun l -> not (List.mem l used)) total
|
318
|
in raise (Error (loc, Unbound_value ("struct field " ^ undef)))
|
319
|
with Not_found ->
|
320
|
ty_struct
|
321
|
end
|
322
|
| Const_string _ -> if is_annot then (* Type_predef. *)type_string else assert false (* string should only appear in annotations *)
|
323
|
|
324
|
(* The following typing functions take as parameter an environment [env]
|
325
|
and whether the element being typed is expected to be constant [const].
|
326
|
[env] is a pair composed of:
|
327
|
- a map from ident to type, associating to each ident, i.e.
|
328
|
variables, constants and (imported) nodes, its type including whether
|
329
|
it is constant or not. This latter information helps in checking constant
|
330
|
propagation policy in Lustre.
|
331
|
- a vdecl list, in order to modify types of declared variables that are
|
332
|
later discovered to be clocks during the typing process.
|
333
|
*)
|
334
|
let check_constant loc const_expected const_real =
|
335
|
if const_expected && not const_real
|
336
|
then raise (Error (loc, Not_a_constant))
|
337
|
|
338
|
let rec type_add_const env const arg targ =
|
339
|
(*Format.eprintf "Typing.type_add_const %a %a@." Printers.pp_expr arg Types.print_ty targ;*)
|
340
|
if const
|
341
|
then let d =
|
342
|
if is_dimension_type targ
|
343
|
then dimension_of_expr arg
|
344
|
else Dimension.mkdim_var () in
|
345
|
let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in
|
346
|
Dimension.eval Basic_library.eval_env eval_const d;
|
347
|
let real_static_type = (* Type_predef. *)type_static d ((* Types. *)dynamic_type targ) in
|
348
|
(match (* Types. *)get_static_value targ with
|
349
|
| None -> ()
|
350
|
| Some d' -> try_unify targ real_static_type arg.expr_loc);
|
351
|
real_static_type
|
352
|
else targ
|
353
|
|
354
|
(* emulates a subtyping relation between types t and (d : t),
|
355
|
used during node applications and assignments *)
|
356
|
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
|
357
|
let loc = real_arg.expr_loc in
|
358
|
let const = const || ((* Types. *)get_static_value formal_type <> None) in
|
359
|
let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in
|
360
|
(*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*)
|
361
|
try_unify ~sub:sub formal_type real_type loc
|
362
|
|
363
|
(* typing an application implies:
|
364
|
- checking that const formal parameters match real const (maybe symbolic) arguments
|
365
|
- checking type adequation between formal and real arguments
|
366
|
An application may embed an homomorphic/internal function, in which case we need to split
|
367
|
it in many calls
|
368
|
*)
|
369
|
and type_appl env in_main loc const f args =
|
370
|
let targs = List.map (type_expr env in_main const) args in
|
371
|
if Basic_library.is_homomorphic_fun f && List.exists is_tuple_type targs
|
372
|
then
|
373
|
try
|
374
|
let targs = Utils.transpose_list (List.map type_list_of_type targs) in
|
375
|
(* Types. *)type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)
|
376
|
with
|
377
|
Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l')))
|
378
|
|
379
|
else (
|
380
|
type_dependent_call env in_main loc const f (List.combine args targs)
|
381
|
)
|
382
|
|
383
|
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)
|
384
|
and type_dependent_call env in_main loc const f targs =
|
385
|
(* Format.eprintf "Typing.type_dependent_call %s@." f; *)
|
386
|
let tins, touts = new_var (), new_var () in
|
387
|
(* Format.eprintf "tin=%a, tout=%a@." print_ty tins print_ty touts; *)
|
388
|
let tfun = (* Type_predef. *)type_arrow tins touts in
|
389
|
(* Format.eprintf "fun=%a@." print_ty tfun; *)
|
390
|
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
|
391
|
(* Format.eprintf "type subtyping@."; *)
|
392
|
let tins = type_list_of_type tins in
|
393
|
if List.length targs <> List.length tins then
|
394
|
raise (Error (loc, WrongArity (List.length tins, List.length targs)))
|
395
|
else
|
396
|
begin
|
397
|
List.iter2 (
|
398
|
fun (a,t) ti ->
|
399
|
let t' = type_add_const env (const || (* Types. *)get_static_value ti <> None) a t in
|
400
|
(* Format.eprintf "uniying ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts; *)
|
401
|
try_unify ~sub:true ti t' a.expr_loc;
|
402
|
(* Format.eprintf "unified ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts; *)
|
403
|
|
404
|
)
|
405
|
targs
|
406
|
tins;
|
407
|
touts
|
408
|
end
|
409
|
|
410
|
(* type a simple call without dependent types
|
411
|
but possible homomorphic extension.
|
412
|
[targs] is here a list of arguments' types. *)
|
413
|
and type_simple_call env in_main loc const f targs =
|
414
|
let tins, touts = new_var (), new_var () in
|
415
|
let tfun = (* Type_predef. *)type_arrow tins touts in
|
416
|
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
|
417
|
(*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*)
|
418
|
try_unify ~sub:true tins (type_of_type_list targs) loc;
|
419
|
touts
|
420
|
|
421
|
(** [type_expr env in_main expr] types expression [expr] in environment
|
422
|
[env], expecting it to be [const] or not. *)
|
423
|
and type_expr ?(is_annot=false) env in_main const expr =
|
424
|
let resulting_ty =
|
425
|
match expr.expr_desc with
|
426
|
| Expr_const c ->
|
427
|
let ty = type_const ~is_annot expr.expr_loc c in
|
428
|
let ty = (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty in
|
429
|
expr.expr_type <- Expr_type_hub.export ty;
|
430
|
ty
|
431
|
| Expr_ident v ->
|
432
|
let tyv =
|
433
|
try
|
434
|
Env.lookup_value (fst env) v
|
435
|
with Not_found ->
|
436
|
Format.eprintf "Failure in typing expr %a. Not in typing environement@." Printers.pp_expr expr;
|
437
|
raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))
|
438
|
in
|
439
|
let ty = instantiate (ref []) (ref []) tyv in
|
440
|
let ty' =
|
441
|
if const
|
442
|
then (* Type_predef. *)type_static (Dimension.mkdim_var ()) (new_var ())
|
443
|
else new_var () in
|
444
|
try_unify ty ty' expr.expr_loc;
|
445
|
expr.expr_type <- Expr_type_hub.export ty;
|
446
|
ty
|
447
|
| Expr_array elist ->
|
448
|
let ty_elt = new_var () in
|
449
|
List.iter (fun e -> try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist;
|
450
|
let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
|
451
|
let ty = (* Type_predef. *)type_array d ty_elt in
|
452
|
expr.expr_type <- Expr_type_hub.export ty;
|
453
|
ty
|
454
|
| Expr_access (e1, d) ->
|
455
|
type_subtyping_arg env in_main false (* not necessary a constant *) (expr_of_dimension d) (* Type_predef. *)type_int;
|
456
|
let ty_elt = new_var () in
|
457
|
let d = Dimension.mkdim_var () in
|
458
|
type_subtyping_arg env in_main const e1 ((* Type_predef. *)type_array d ty_elt);
|
459
|
expr.expr_type <- Expr_type_hub.export ty_elt;
|
460
|
ty_elt
|
461
|
| Expr_power (e1, d) ->
|
462
|
let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in
|
463
|
type_subtyping_arg env in_main true (expr_of_dimension d) (* Type_predef. *)type_int;
|
464
|
Dimension.eval Basic_library.eval_env eval_const d;
|
465
|
let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in
|
466
|
let ty = (* Type_predef. *)type_array d ty_elt in
|
467
|
expr.expr_type <- Expr_type_hub.export ty;
|
468
|
ty
|
469
|
| Expr_tuple elist ->
|
470
|
let ty = new_ty (Ttuple (List.map (type_expr ~is_annot env in_main const) elist)) in
|
471
|
expr.expr_type <- Expr_type_hub.export ty;
|
472
|
ty
|
473
|
| Expr_ite (c, t, e) ->
|
474
|
type_subtyping_arg env in_main const c (* Type_predef. *)type_bool;
|
475
|
let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in
|
476
|
expr.expr_type <- Expr_type_hub.export ty;
|
477
|
ty
|
478
|
| Expr_appl (id, args, r) ->
|
479
|
(* application of non internal function is not legal in a constant
|
480
|
expression *)
|
481
|
(match r with
|
482
|
| None -> ()
|
483
|
| Some c ->
|
484
|
check_constant expr.expr_loc const false;
|
485
|
type_subtyping_arg env in_main const c (* Type_predef. *)type_bool);
|
486
|
let args_list = expr_list_of_expr args in
|
487
|
let targs = new_ty (Ttuple (List.map (fun a -> Expr_type_hub.import a.expr_type) args_list)) in
|
488
|
args.expr_type <- Expr_type_hub.export targs;
|
489
|
let touts = type_appl env in_main expr.expr_loc const id args_list in
|
490
|
expr.expr_type <- Expr_type_hub.export touts;
|
491
|
touts
|
492
|
| Expr_fby (e1,e2)
|
493
|
| Expr_arrow (e1,e2) ->
|
494
|
(* fby/arrow is not legal in a constant expression *)
|
495
|
check_constant expr.expr_loc const false;
|
496
|
let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in
|
497
|
expr.expr_type <- Expr_type_hub.export ty;
|
498
|
ty
|
499
|
| Expr_pre e ->
|
500
|
(* pre is not legal in a constant expression *)
|
501
|
check_constant expr.expr_loc const false;
|
502
|
let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in
|
503
|
expr.expr_type <- Expr_type_hub.export ty;
|
504
|
ty
|
505
|
| Expr_when (e1,c,l) ->
|
506
|
(* when is not legal in a constant expression *)
|
507
|
check_constant expr.expr_loc const false;
|
508
|
let typ_l = (* Type_predef. *)type_clock (type_const ~is_annot expr.expr_loc (Const_tag l)) in
|
509
|
let expr_c = expr_of_ident c expr.expr_loc in
|
510
|
type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
|
511
|
let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in
|
512
|
expr.expr_type <- Expr_type_hub.export ty;
|
513
|
ty
|
514
|
| Expr_merge (c,hl) ->
|
515
|
(* merge is not legal in a constant expression *)
|
516
|
check_constant expr.expr_loc const false;
|
517
|
let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in
|
518
|
let expr_c = expr_of_ident c expr.expr_loc in
|
519
|
let typ_l = (* Type_predef. *)type_clock typ_in in
|
520
|
type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
|
521
|
expr.expr_type <- Expr_type_hub.export typ_out;
|
522
|
typ_out
|
523
|
in
|
524
|
Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr (* Types. *)print_ty resulting_ty);
|
525
|
resulting_ty
|
526
|
|
527
|
and type_branches ?(is_annot=false) env in_main loc const hl =
|
528
|
let typ_in = new_var () in
|
529
|
let typ_out = new_var () in
|
530
|
try
|
531
|
let used_labels =
|
532
|
List.fold_left (fun accu (t, h) ->
|
533
|
unify typ_in (type_const ~is_annot loc (Const_tag t));
|
534
|
type_subtyping_arg env in_main const h typ_out;
|
535
|
if List.mem t accu
|
536
|
then raise (Error (loc, Already_bound t))
|
537
|
else t :: accu) [] hl in
|
538
|
let type_labels = get_enum_type_tags (coretype_type typ_in) in
|
539
|
if List.sort compare used_labels <> List.sort compare type_labels
|
540
|
then let unbound_tag = List.find (fun t -> not (List.mem t used_labels)) type_labels in
|
541
|
raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))
|
542
|
else (typ_in, typ_out)
|
543
|
with Unify (t1, t2) ->
|
544
|
raise (Error (loc, Type_clash (t1,t2)))
|
545
|
|
546
|
(** [type_eq env eq] types equation [eq] in environment [env] *)
|
547
|
let type_eq env in_main undefined_vars eq =
|
548
|
(*Format.eprintf "Typing.type_eq %a@." Printers.pp_node_eq eq;*)
|
549
|
(* Check undefined variables, type lhs *)
|
550
|
let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in
|
551
|
let ty_lhs = type_expr env in_main false expr_lhs in
|
552
|
(* Check multiple variable definitions *)
|
553
|
let define_var id uvars =
|
554
|
if ISet.mem id uvars
|
555
|
then ISet.remove id uvars
|
556
|
else raise (Error (eq.eq_loc, Already_defined id))
|
557
|
in
|
558
|
(* check assignment of declared constant, assignment of clock *)
|
559
|
let ty_lhs =
|
560
|
type_of_type_list
|
561
|
(List.map2 (fun ty id ->
|
562
|
if get_static_value ty <> None
|
563
|
then raise (Error (eq.eq_loc, Assigned_constant id)) else
|
564
|
match get_clock_base_type ty with
|
565
|
| None -> ty
|
566
|
| Some ty -> ty)
|
567
|
(type_list_of_type ty_lhs) eq.eq_lhs) in
|
568
|
let undefined_vars =
|
569
|
List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
|
570
|
(* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
|
571
|
to a (always non-constant) lhs variable *)
|
572
|
type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;
|
573
|
undefined_vars
|
574
|
|
575
|
|
576
|
(* [type_coreclock env ck id loc] types the type clock declaration [ck]
|
577
|
in environment [env] *)
|
578
|
let type_coreclock env ck id loc =
|
579
|
match ck.ck_dec_desc with
|
580
|
| Ckdec_any -> ()
|
581
|
| Ckdec_bool cl ->
|
582
|
let dummy_id_expr = expr_of_ident id loc in
|
583
|
let when_expr =
|
584
|
List.fold_left
|
585
|
(fun expr (x, l) ->
|
586
|
{expr_tag = new_tag ();
|
587
|
expr_desc= Expr_when (expr,x,l);
|
588
|
expr_type = Types.Main.new_var ();
|
589
|
expr_clock = Clocks.new_var true;
|
590
|
expr_delay = Delay.new_var ();
|
591
|
expr_loc=loc;
|
592
|
expr_annot = None})
|
593
|
dummy_id_expr cl
|
594
|
in
|
595
|
ignore (type_expr env false false when_expr)
|
596
|
|
597
|
let rec check_type_declaration loc cty =
|
598
|
match cty with
|
599
|
| Tydec_clock ty
|
600
|
| Tydec_array (_, ty) -> check_type_declaration loc ty
|
601
|
| Tydec_const tname ->
|
602
|
Format.printf "TABLE: %a@." print_type_table ();
|
603
|
(* TODO REMOVE *)
|
604
|
if not (Hashtbl.mem type_table cty)
|
605
|
then raise (Error (loc, Unbound_type tname));
|
606
|
| _ -> ()
|
607
|
|
608
|
let type_var_decl vd_env env vdecl =
|
609
|
(*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*)
|
610
|
check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
|
611
|
let eval_const id = (* Types. *)get_static_value (Env.lookup_value env id) in
|
612
|
let type_dim d =
|
613
|
begin
|
614
|
type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) (* Type_predef. *)type_int;
|
615
|
Dimension.eval Basic_library.eval_env eval_const d;
|
616
|
end in
|
617
|
let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
|
618
|
|
619
|
let ty_static =
|
620
|
if vdecl.var_dec_const
|
621
|
then (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty
|
622
|
else ty in
|
623
|
(match vdecl.var_dec_value with
|
624
|
| None -> ()
|
625
|
| Some v -> type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static);
|
626
|
try_unify ty_static (Expr_type_hub.import vdecl.var_type) vdecl.var_loc;
|
627
|
let new_env = Env.add_value env vdecl.var_id ty_static in
|
628
|
type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
|
629
|
(*Format.eprintf "END %a@." Types.print_ty ty_static;*)
|
630
|
new_env
|
631
|
|
632
|
let type_var_decl_list vd_env env l =
|
633
|
List.fold_left (type_var_decl vd_env) env l
|
634
|
|
635
|
let type_of_vlist vars =
|
636
|
let tyl = List.map (fun v -> Expr_type_hub.import v.var_type) vars in
|
637
|
type_of_type_list tyl
|
638
|
|
639
|
let add_vdecl vd_env vdecl =
|
640
|
if List.exists (fun v -> v.var_id = vdecl.var_id) vd_env
|
641
|
then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
|
642
|
else vdecl::vd_env
|
643
|
|
644
|
let check_vd_env vd_env =
|
645
|
ignore (List.fold_left add_vdecl [] vd_env)
|
646
|
|
647
|
(** [type_node env nd loc] types node [nd] in environment env. The
|
648
|
location is used for error reports. *)
|
649
|
let type_node env nd loc =
|
650
|
let is_main = nd.node_id = !Options.main_node in
|
651
|
let vd_env_ol = nd.node_outputs@nd.node_locals in
|
652
|
let vd_env = nd.node_inputs@vd_env_ol in
|
653
|
check_vd_env vd_env;
|
654
|
let init_env = env in
|
655
|
let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
|
656
|
let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in
|
657
|
let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in
|
658
|
let new_env = Env.overwrite env delta_env in
|
659
|
let undefined_vars_init =
|
660
|
List.fold_left
|
661
|
(fun uvs v -> ISet.add v.var_id uvs)
|
662
|
ISet.empty vd_env_ol in
|
663
|
let undefined_vars =
|
664
|
let eqs, auts = get_node_eqs nd in
|
665
|
(* TODO XXX: il faut typer les handlers de l'automate *)
|
666
|
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs
|
667
|
in
|
668
|
(* Typing asserts *)
|
669
|
List.iter (fun assert_ ->
|
670
|
let assert_expr = assert_.assert_expr in
|
671
|
type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool
|
672
|
) nd.node_asserts;
|
673
|
(* Typing annots *)
|
674
|
List.iter (fun annot ->
|
675
|
List.iter (fun (_, eexpr) -> ignore (type_expr ~is_annot:true (new_env, vd_env) false false eexpr.eexpr_qfexpr)) annot.annots
|
676
|
) nd.node_annot;
|
677
|
|
678
|
(* check that table is empty *)
|
679
|
let local_consts = List.fold_left (fun res vdecl -> if vdecl.var_dec_const then ISet.add vdecl.var_id res else res) ISet.empty nd.node_locals in
|
680
|
let undefined_vars = ISet.diff undefined_vars local_consts in
|
681
|
if (not (ISet.is_empty undefined_vars)) then
|
682
|
raise (Error (loc, Undefined_var undefined_vars));
|
683
|
let ty_ins = type_of_vlist nd.node_inputs in
|
684
|
let ty_outs = type_of_vlist nd.node_outputs in
|
685
|
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
|
686
|
generalize ty_node;
|
687
|
(* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
|
688
|
nd.node_type <- Expr_type_hub.export ty_node;
|
689
|
Env.add_value env nd.node_id ty_node
|
690
|
|
691
|
let type_imported_node env nd loc =
|
692
|
let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
|
693
|
let vd_env = nd.nodei_inputs@nd.nodei_outputs in
|
694
|
check_vd_env vd_env;
|
695
|
ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
|
696
|
let ty_ins = type_of_vlist nd.nodei_inputs in
|
697
|
let ty_outs = type_of_vlist nd.nodei_outputs in
|
698
|
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
|
699
|
generalize ty_node;
|
700
|
(*
|
701
|
if (is_polymorphic ty_node) then
|
702
|
raise (Error (loc, Poly_imported_node nd.nodei_id));
|
703
|
*)
|
704
|
let new_env = Env.add_value env nd.nodei_id ty_node in
|
705
|
nd.nodei_type <- Expr_type_hub.export ty_node;
|
706
|
new_env
|
707
|
|
708
|
let type_top_const env cdecl =
|
709
|
let ty = type_const cdecl.const_loc cdecl.const_value in
|
710
|
let d =
|
711
|
if is_dimension_type ty
|
712
|
then dimension_of_const cdecl.const_loc cdecl.const_value
|
713
|
else Dimension.mkdim_var () in
|
714
|
let ty = (* Type_predef. *)type_static d ty in
|
715
|
let new_env = Env.add_value env cdecl.const_id ty in
|
716
|
cdecl.const_type <- Expr_type_hub.export ty;
|
717
|
new_env
|
718
|
|
719
|
let type_top_consts env clist =
|
720
|
List.fold_left type_top_const env clist
|
721
|
|
722
|
let rec type_top_decl env decl =
|
723
|
match decl.top_decl_desc with
|
724
|
| Node nd -> (
|
725
|
try
|
726
|
type_node env nd decl.top_decl_loc
|
727
|
with Error (loc, err) as exc -> (
|
728
|
if !Options.global_inline then
|
729
|
Format.eprintf "Type error: failing node@.%a@.@?"
|
730
|
Printers.pp_node nd
|
731
|
;
|
732
|
raise exc)
|
733
|
)
|
734
|
| ImportedNode nd ->
|
735
|
type_imported_node env nd decl.top_decl_loc
|
736
|
| Const c ->
|
737
|
type_top_const env c
|
738
|
| TypeDef _ -> List.fold_left type_top_decl env (consts_of_enum_type decl)
|
739
|
| Open _ -> env
|
740
|
|
741
|
let get_type_of_call decl =
|
742
|
match decl.top_decl_desc with
|
743
|
| Node nd ->
|
744
|
let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.node_type) in
|
745
|
type_list_of_type in_typ, type_list_of_type out_typ
|
746
|
| ImportedNode nd ->
|
747
|
let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.nodei_type) in
|
748
|
type_list_of_type in_typ, type_list_of_type out_typ
|
749
|
| _ -> assert false
|
750
|
|
751
|
let type_prog env decls =
|
752
|
try
|
753
|
List.fold_left type_top_decl env decls
|
754
|
with Failure _ as exc -> raise exc
|
755
|
|
756
|
(* Once the Lustre program is fully typed,
|
757
|
we must get back to the original description of dimensions,
|
758
|
with constant parameters, instead of unifiable internal variables. *)
|
759
|
|
760
|
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types,
|
761
|
i.e. replacing unifiable second_order variables with the original static parameters.
|
762
|
Once restored in this formulation, dimensions may be meaningfully printed.
|
763
|
*)
|
764
|
let uneval_vdecl_generics vdecl =
|
765
|
if vdecl.var_dec_const
|
766
|
then
|
767
|
match get_static_value (Expr_type_hub.import vdecl.var_type) with
|
768
|
| None -> (Format.eprintf "internal error: %a@." (* Types. *)print_ty (Expr_type_hub.import vdecl.var_type); assert false)
|
769
|
| Some d -> Dimension.uneval vdecl.var_id d
|
770
|
|
771
|
let uneval_node_generics vdecls =
|
772
|
List.iter uneval_vdecl_generics vdecls
|
773
|
|
774
|
let uneval_top_generics decl =
|
775
|
match decl.top_decl_desc with
|
776
|
| Node nd ->
|
777
|
uneval_node_generics (nd.node_inputs @ nd.node_outputs)
|
778
|
| ImportedNode nd ->
|
779
|
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
|
780
|
| Const _
|
781
|
| TypeDef _
|
782
|
| Open _ -> ()
|
783
|
|
784
|
let uneval_prog_generics prog =
|
785
|
List.iter uneval_top_generics prog
|
786
|
|
787
|
let rec get_imported_symbol decls id =
|
788
|
match decls with
|
789
|
| [] -> assert false
|
790
|
| decl::q ->
|
791
|
(match decl.top_decl_desc with
|
792
|
| ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf -> decl
|
793
|
| Const c when id = c.const_id && decl.top_decl_itf -> decl
|
794
|
| TypeDef _ -> get_imported_symbol (consts_of_enum_type decl @ q) id
|
795
|
| _ -> get_imported_symbol q id)
|
796
|
|
797
|
let check_env_compat header declared computed =
|
798
|
uneval_prog_generics header;
|
799
|
Env.iter declared (fun k decl_type_k ->
|
800
|
let loc = (get_imported_symbol header k).top_decl_loc in
|
801
|
let computed_t =
|
802
|
instantiate (ref []) (ref [])
|
803
|
(try Env.lookup_value computed k
|
804
|
with Not_found -> raise (Error (loc, Declared_but_undefined k))) in
|
805
|
(*Types.print_ty Format.std_formatter decl_type_k;
|
806
|
Types.print_ty Format.std_formatter computed_t;*)
|
807
|
try_unify ~sub:true ~semi:true decl_type_k computed_t loc
|
808
|
)
|
809
|
|
810
|
let check_typedef_top decl =
|
811
|
(*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*)
|
812
|
(*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*)
|
813
|
(*Format.eprintf "%a" Corelang.print_type_table ();*)
|
814
|
match decl.top_decl_desc with
|
815
|
| TypeDef ty ->
|
816
|
let owner = decl.top_decl_owner in
|
817
|
let itf = decl.top_decl_itf in
|
818
|
let decl' =
|
819
|
try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id)
|
820
|
with Not_found -> raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in
|
821
|
let owner' = decl'.top_decl_owner in
|
822
|
(*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*)
|
823
|
let itf' = decl'.top_decl_itf in
|
824
|
(match decl'.top_decl_desc with
|
825
|
| Const _ | Node _ | ImportedNode _ -> assert false
|
826
|
| TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') -> ()
|
827
|
| _ -> raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id)))
|
828
|
| _ -> ()
|
829
|
|
830
|
let check_typedef_compat header =
|
831
|
List.iter check_typedef_top header
|
832
|
end
|
833
|
|
834
|
include Make(Types.Main) (struct
|
835
|
type type_expr = Types.Main.type_expr
|
836
|
let import x = x
|
837
|
let export x = x
|
838
|
end)
|
839
|
(* Local Variables: *)
|
840
|
(* compile-command:"make -C .." *)
|
841
|
(* End: *)
|