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