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 clock-calculus module. Based on type inference algorithms with
|
15
|
destructive unification. Uses a bit of subtyping for periodic clocks. *)
|
16
|
|
17
|
(* Though it shares similarities with the typing module, no code is shared.
|
18
|
Simple environments, very limited identifier scoping, no identifier
|
19
|
redefinition allowed. *)
|
20
|
open Utils
|
21
|
open Lustre_types
|
22
|
open Corelang
|
23
|
open Clocks
|
24
|
|
25
|
let loc_of_cond (_s, e) id =
|
26
|
let pos_start =
|
27
|
{ e with Lexing.pos_cnum = e.Lexing.pos_cnum - String.length id }
|
28
|
in
|
29
|
pos_start, e
|
30
|
|
31
|
(** [occurs cvar ck] returns true if the clock variable [cvar] occurs in clock
|
32
|
[ck]. False otherwise. *)
|
33
|
let rec occurs cvar ck =
|
34
|
let ck = repr ck in
|
35
|
match ck.cdesc with
|
36
|
| Carrow (ck1, ck2) ->
|
37
|
occurs cvar ck1 || occurs cvar ck2
|
38
|
| Ctuple ckl ->
|
39
|
List.exists (occurs cvar) ckl
|
40
|
| Con (ck', _, _) ->
|
41
|
occurs cvar ck'
|
42
|
| Cvar ->
|
43
|
ck = cvar
|
44
|
| Cunivar ->
|
45
|
false
|
46
|
| Clink ck' ->
|
47
|
occurs cvar ck'
|
48
|
| Ccarrying (_, ck') ->
|
49
|
occurs cvar ck'
|
50
|
|
51
|
(* Clocks generalization *)
|
52
|
let rec generalize_carrier cr =
|
53
|
match cr.carrier_desc with
|
54
|
| Carry_const _ | Carry_name ->
|
55
|
if cr.carrier_scoped then raise (Scope_carrier cr);
|
56
|
cr.carrier_desc <- Carry_var
|
57
|
| Carry_var ->
|
58
|
()
|
59
|
| Carry_link cr' ->
|
60
|
generalize_carrier cr'
|
61
|
|
62
|
(* Generalize by side-effects *)
|
63
|
|
64
|
(** Promote monomorphic clock variables to polymorphic clock variables. *)
|
65
|
let rec generalize ck =
|
66
|
match ck.cdesc with
|
67
|
| Carrow (ck1, ck2) ->
|
68
|
generalize ck1;
|
69
|
generalize ck2
|
70
|
| Ctuple clist ->
|
71
|
List.iter generalize clist
|
72
|
| Con (ck', cr, _) ->
|
73
|
generalize ck';
|
74
|
generalize_carrier cr
|
75
|
| Cvar ->
|
76
|
if ck.cscoped then raise (Scope_clock ck);
|
77
|
ck.cdesc <- Cunivar
|
78
|
| Cunivar ->
|
79
|
()
|
80
|
| Clink ck' ->
|
81
|
generalize ck'
|
82
|
| Ccarrying (cr, ck') ->
|
83
|
generalize_carrier cr;
|
84
|
generalize ck'
|
85
|
|
86
|
let try_generalize ck_node loc =
|
87
|
try generalize ck_node with
|
88
|
| Scope_carrier cr ->
|
89
|
raise (Error (loc, Carrier_extrusion (ck_node, cr)))
|
90
|
| Scope_clock ck ->
|
91
|
raise (Error (loc, Clock_extrusion (ck_node, ck)))
|
92
|
|
93
|
(* Clocks instanciation *)
|
94
|
let instantiate_carrier cr inst_cr_vars =
|
95
|
let cr = carrier_repr cr in
|
96
|
match cr.carrier_desc with
|
97
|
| Carry_const _ | Carry_name ->
|
98
|
cr
|
99
|
| Carry_link _ ->
|
100
|
failwith "Internal error"
|
101
|
| Carry_var -> (
|
102
|
try List.assoc cr.carrier_id !inst_cr_vars
|
103
|
with Not_found ->
|
104
|
let cr_var = new_carrier Carry_name true in
|
105
|
inst_cr_vars := (cr.carrier_id, cr_var) :: !inst_cr_vars;
|
106
|
cr_var)
|
107
|
|
108
|
(* inst_ck_vars ensures that a polymorphic variable is instanciated with the
|
109
|
same monomorphic variable if it occurs several times in the same type.
|
110
|
inst_cr_vars is the same for carriers. *)
|
111
|
|
112
|
(** Downgrade polymorphic clock variables to monomorphic clock variables *)
|
113
|
let rec instantiate inst_ck_vars inst_cr_vars ck =
|
114
|
match ck.cdesc with
|
115
|
| Carrow (ck1, ck2) ->
|
116
|
{
|
117
|
ck with
|
118
|
cdesc =
|
119
|
Carrow
|
120
|
( instantiate inst_ck_vars inst_cr_vars ck1,
|
121
|
instantiate inst_ck_vars inst_cr_vars ck2 );
|
122
|
}
|
123
|
| Ctuple cklist ->
|
124
|
{
|
125
|
ck with
|
126
|
cdesc = Ctuple (List.map (instantiate inst_ck_vars inst_cr_vars) cklist);
|
127
|
}
|
128
|
| Con (ck', c, l) ->
|
129
|
let c' = instantiate_carrier c inst_cr_vars in
|
130
|
{ ck with cdesc = Con (instantiate inst_ck_vars inst_cr_vars ck', c', l) }
|
131
|
| Cvar ->
|
132
|
ck
|
133
|
| Clink ck' ->
|
134
|
{ ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck') }
|
135
|
| Ccarrying (cr, ck') ->
|
136
|
let cr' = instantiate_carrier cr inst_cr_vars in
|
137
|
{
|
138
|
ck with
|
139
|
cdesc = Ccarrying (cr', instantiate inst_ck_vars inst_cr_vars ck');
|
140
|
}
|
141
|
| Cunivar -> (
|
142
|
try List.assoc ck.cid !inst_ck_vars
|
143
|
with Not_found ->
|
144
|
let var = new_ck Cvar true in
|
145
|
inst_ck_vars := (ck.cid, var) :: !inst_ck_vars;
|
146
|
var)
|
147
|
|
148
|
let rec update_scope_carrier scoped cr =
|
149
|
if not scoped then (
|
150
|
cr.carrier_scoped <- scoped;
|
151
|
match cr.carrier_desc with
|
152
|
| Carry_const _ | Carry_name | Carry_var ->
|
153
|
()
|
154
|
| Carry_link cr' ->
|
155
|
update_scope_carrier scoped cr')
|
156
|
|
157
|
let rec update_scope scoped ck =
|
158
|
if not scoped then (
|
159
|
ck.cscoped <- scoped;
|
160
|
match ck.cdesc with
|
161
|
| Carrow (ck1, ck2) ->
|
162
|
update_scope scoped ck1;
|
163
|
update_scope scoped ck2
|
164
|
| Ctuple clist ->
|
165
|
List.iter (update_scope scoped) clist
|
166
|
| Con (ck', _, _) ->
|
167
|
update_scope scoped ck' (*; update_scope_carrier scoped cr*)
|
168
|
| Cvar | Cunivar ->
|
169
|
()
|
170
|
| Clink ck' ->
|
171
|
update_scope scoped ck'
|
172
|
| Ccarrying (cr, ck') ->
|
173
|
update_scope_carrier scoped cr;
|
174
|
update_scope scoped ck')
|
175
|
|
176
|
(* Unifies two clock carriers *)
|
177
|
let unify_carrier cr1 cr2 =
|
178
|
let cr1 = carrier_repr cr1 in
|
179
|
let cr2 = carrier_repr cr2 in
|
180
|
if cr1 == cr2 then ()
|
181
|
else
|
182
|
match cr1.carrier_desc, cr2.carrier_desc with
|
183
|
| Carry_const id1, Carry_const id2 ->
|
184
|
if id1 <> id2 then raise (Mismatch (cr1, cr2))
|
185
|
| Carry_const _, Carry_name ->
|
186
|
cr2.carrier_desc <- Carry_link cr1;
|
187
|
update_scope_carrier cr2.carrier_scoped cr1
|
188
|
| Carry_name, Carry_const _ ->
|
189
|
cr1.carrier_desc <- Carry_link cr2;
|
190
|
update_scope_carrier cr1.carrier_scoped cr2
|
191
|
| Carry_name, Carry_name ->
|
192
|
if cr1.carrier_id < cr2.carrier_id then (
|
193
|
cr2.carrier_desc <- Carry_link cr1;
|
194
|
update_scope_carrier cr2.carrier_scoped cr1)
|
195
|
else (
|
196
|
cr1.carrier_desc <- Carry_link cr2;
|
197
|
update_scope_carrier cr1.carrier_scoped cr2)
|
198
|
| _, _ ->
|
199
|
assert false
|
200
|
|
201
|
(* Semi-unifies two clock carriers *)
|
202
|
let semi_unify_carrier cr1 cr2 =
|
203
|
let cr1 = carrier_repr cr1 in
|
204
|
let cr2 = carrier_repr cr2 in
|
205
|
if cr1 == cr2 then ()
|
206
|
else
|
207
|
match cr1.carrier_desc, cr2.carrier_desc with
|
208
|
| Carry_const id1, Carry_const id2 ->
|
209
|
if id1 <> id2 then raise (Mismatch (cr1, cr2))
|
210
|
| Carry_const _, Carry_name ->
|
211
|
cr2.carrier_desc <- Carry_link cr1;
|
212
|
update_scope_carrier cr2.carrier_scoped cr1
|
213
|
| Carry_name, Carry_const _ ->
|
214
|
raise (Mismatch (cr1, cr2))
|
215
|
| Carry_name, Carry_name ->
|
216
|
if cr1.carrier_id < cr2.carrier_id then (
|
217
|
cr2.carrier_desc <- Carry_link cr1;
|
218
|
update_scope_carrier cr2.carrier_scoped cr1)
|
219
|
else (
|
220
|
cr1.carrier_desc <- Carry_link cr2;
|
221
|
update_scope_carrier cr1.carrier_scoped cr2)
|
222
|
| _, _ ->
|
223
|
assert false
|
224
|
|
225
|
let try_unify_carrier ck1 ck2 loc =
|
226
|
try unify_carrier ck1 ck2 with
|
227
|
| Unify (ck1', ck2') ->
|
228
|
raise (Error (loc, Clock_clash (ck1', ck2')))
|
229
|
| Mismatch (cr1, cr2) ->
|
230
|
raise (Error (loc, Carrier_mismatch (cr1, cr2)))
|
231
|
|
232
|
(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify (ck1,ck2)] if
|
233
|
the clocks are not unifiable.*)
|
234
|
let rec unify ck1 ck2 =
|
235
|
let ck1 = repr ck1 in
|
236
|
let ck2 = repr ck2 in
|
237
|
if ck1 == ck2 then ()
|
238
|
else
|
239
|
match ck1.cdesc, ck2.cdesc with
|
240
|
| Cvar, Cvar ->
|
241
|
if ck1.cid < ck2.cid then (
|
242
|
ck2.cdesc <- Clink (simplify ck1);
|
243
|
update_scope ck2.cscoped ck1)
|
244
|
else (
|
245
|
ck1.cdesc <- Clink (simplify ck2);
|
246
|
update_scope ck1.cscoped ck2)
|
247
|
| Cvar, _ when not (occurs ck1 ck2) ->
|
248
|
update_scope ck1.cscoped ck2;
|
249
|
ck1.cdesc <- Clink (simplify ck2)
|
250
|
| _, Cvar when not (occurs ck2 ck1) ->
|
251
|
update_scope ck2.cscoped ck1;
|
252
|
ck2.cdesc <- Clink (simplify ck1)
|
253
|
| Ccarrying (cr1, ck1'), Ccarrying (cr2, ck2') ->
|
254
|
unify_carrier cr1 cr2;
|
255
|
unify ck1' ck2'
|
256
|
| Ccarrying (_, _), _ | _, Ccarrying (_, _) ->
|
257
|
raise (Unify (ck1, ck2))
|
258
|
| Carrow (c1, c2), Carrow (c1', c2') ->
|
259
|
unify c1 c1';
|
260
|
unify c2 c2'
|
261
|
| Ctuple ckl1, Ctuple ckl2 ->
|
262
|
if List.length ckl1 <> List.length ckl2 then raise (Unify (ck1, ck2));
|
263
|
List.iter2 unify ckl1 ckl2
|
264
|
| Con (ck', c1, l1), Con (ck'', c2, l2) when l1 = l2 ->
|
265
|
unify_carrier c1 c2;
|
266
|
unify ck' ck''
|
267
|
| Cunivar, _ | _, Cunivar ->
|
268
|
()
|
269
|
| _, _ ->
|
270
|
raise (Unify (ck1, ck2))
|
271
|
|
272
|
(** [unify ck1 ck2] semi-unifies clocks [ck1] and [ck2]. Raises [Unify
|
273
|
(ck1,ck2)] if the clocks are not semi-unifiable.*)
|
274
|
let rec semi_unify ck1 ck2 =
|
275
|
let ck1 = repr ck1 in
|
276
|
let ck2 = repr ck2 in
|
277
|
if ck1 == ck2 then ()
|
278
|
else
|
279
|
match ck1.cdesc, ck2.cdesc with
|
280
|
| Cvar, Cvar ->
|
281
|
if ck1.cid < ck2.cid then (
|
282
|
ck2.cdesc <- Clink (simplify ck1);
|
283
|
update_scope ck2.cscoped ck1)
|
284
|
else (
|
285
|
ck1.cdesc <- Clink (simplify ck2);
|
286
|
update_scope ck1.cscoped ck2)
|
287
|
| Cvar, _ ->
|
288
|
raise (Unify (ck1, ck2))
|
289
|
| _, Cvar when not (occurs ck2 ck1) ->
|
290
|
update_scope ck2.cscoped ck1;
|
291
|
ck2.cdesc <- Clink (simplify ck1)
|
292
|
| Ccarrying (cr1, ck1'), Ccarrying (cr2, ck2') ->
|
293
|
semi_unify_carrier cr1 cr2;
|
294
|
semi_unify ck1' ck2'
|
295
|
| Ccarrying (_, _), _ | _, Ccarrying (_, _) ->
|
296
|
raise (Unify (ck1, ck2))
|
297
|
| Carrow (c1, c2), Carrow (c1', c2') ->
|
298
|
semi_unify c1 c1';
|
299
|
semi_unify c2 c2'
|
300
|
| Ctuple ckl1, Ctuple ckl2 ->
|
301
|
if List.length ckl1 <> List.length ckl2 then raise (Unify (ck1, ck2));
|
302
|
List.iter2 semi_unify ckl1 ckl2
|
303
|
| Con (ck', c1, l1), Con (ck'', c2, l2) when l1 = l2 ->
|
304
|
semi_unify_carrier c1 c2;
|
305
|
semi_unify ck' ck''
|
306
|
| Cunivar, _ | _, Cunivar ->
|
307
|
()
|
308
|
| _, _ ->
|
309
|
raise (Unify (ck1, ck2))
|
310
|
|
311
|
(* Returns the value corresponding to a pclock (integer) factor expression.
|
312
|
Expects a constant expression (checked by typing). *)
|
313
|
let int_factor_of_expr e =
|
314
|
match e.expr_desc with
|
315
|
| Expr_const (Const_int i) ->
|
316
|
i
|
317
|
| _ ->
|
318
|
failwith "Internal error: int_factor_of_expr"
|
319
|
|
320
|
(** [clock_uncarry ck] drops the possible carrier(s) name(s) from clock [ck] *)
|
321
|
let rec clock_uncarry ck =
|
322
|
let ck = repr ck in
|
323
|
match ck.cdesc with
|
324
|
| Ccarrying (_, ck') ->
|
325
|
ck'
|
326
|
| Con (ck', cr, l) ->
|
327
|
clock_on (clock_uncarry ck') cr l
|
328
|
| Ctuple ckl ->
|
329
|
clock_of_clock_list (List.map clock_uncarry ckl)
|
330
|
| _ ->
|
331
|
ck
|
332
|
|
333
|
let try_unify ck1 ck2 loc =
|
334
|
try unify ck1 ck2 with
|
335
|
| Unify (ck1', ck2') ->
|
336
|
raise (Error (loc, Clock_clash (ck1', ck2')))
|
337
|
| Mismatch (cr1, cr2) ->
|
338
|
raise (Error (loc, Carrier_mismatch (cr1, cr2)))
|
339
|
|
340
|
let try_semi_unify ck1 ck2 loc =
|
341
|
try semi_unify ck1 ck2 with
|
342
|
| Unify (ck1', ck2') ->
|
343
|
raise (Error (loc, Clock_clash (ck1', ck2')))
|
344
|
| Mismatch (cr1, cr2) ->
|
345
|
raise (Error (loc, Carrier_mismatch (cr1, cr2)))
|
346
|
|
347
|
(* ck2 is a subtype of ck1 *)
|
348
|
let rec sub_unify sub ck1 ck2 =
|
349
|
match (repr ck1).cdesc, (repr ck2).cdesc with
|
350
|
| Ctuple cl1, Ctuple cl2 ->
|
351
|
if List.length cl1 <> List.length cl2 then raise (Unify (ck1, ck2))
|
352
|
else List.iter2 (sub_unify sub) cl1 cl2
|
353
|
| Ctuple [ c1 ], _ ->
|
354
|
sub_unify sub c1 ck2
|
355
|
| _, Ctuple [ c2 ] ->
|
356
|
sub_unify sub ck1 c2
|
357
|
| Con (c1, cr1, t1), Con (c2, cr2, t2) when t1 = t2 ->
|
358
|
unify_carrier cr1 cr2;
|
359
|
sub_unify sub c1 c2
|
360
|
| Ccarrying (cr1, c1), Ccarrying (cr2, c2) ->
|
361
|
unify_carrier cr1 cr2;
|
362
|
sub_unify sub c1 c2
|
363
|
| _, Ccarrying (_, c2) when sub ->
|
364
|
sub_unify sub ck1 c2
|
365
|
| _ ->
|
366
|
unify ck1 ck2
|
367
|
|
368
|
let try_sub_unify sub ck1 ck2 loc =
|
369
|
try sub_unify sub ck1 ck2 with
|
370
|
| Unify (ck1', ck2') ->
|
371
|
raise (Error (loc, Clock_clash (ck1', ck2')))
|
372
|
| Mismatch (cr1, cr2) ->
|
373
|
raise (Error (loc, Carrier_mismatch (cr1, cr2)))
|
374
|
|
375
|
(* Unifies all the clock variables in the clock type of a tuple expression, so
|
376
|
that the clock type only uses at most one clock variable *)
|
377
|
let unify_tuple_clock ref_ck_opt ck loc =
|
378
|
(*(match ref_ck_opt with | None -> Format.eprintf "unify_tuple_clock None
|
379
|
%a@." Clocks.print_ck ck | Some ck' -> Format.eprintf "unify_tuple_clock
|
380
|
(Some %a) %a@." Clocks.print_ck ck' Clocks.print_ck ck);*)
|
381
|
let ck_var = ref ref_ck_opt in
|
382
|
let rec aux ck =
|
383
|
match (repr ck).cdesc with
|
384
|
| Con _ | Cvar -> (
|
385
|
match !ck_var with
|
386
|
| None ->
|
387
|
ck_var := Some ck
|
388
|
| Some v ->
|
389
|
(* may fail *)
|
390
|
try_unify ck v loc)
|
391
|
| Ctuple cl ->
|
392
|
List.iter aux cl
|
393
|
| Carrow _ ->
|
394
|
assert false (* should not occur *)
|
395
|
| Ccarrying (_, ck1) ->
|
396
|
aux ck1
|
397
|
| _ ->
|
398
|
()
|
399
|
in
|
400
|
aux ck
|
401
|
|
402
|
(* Unifies all the clock variables in the clock type of an imported node, so
|
403
|
that the clock type only uses at most one base clock variable, that is, the
|
404
|
activation clock of the node *)
|
405
|
let unify_imported_clock ref_ck_opt ck loc =
|
406
|
let ck_var = ref ref_ck_opt in
|
407
|
let rec aux ck =
|
408
|
match (repr ck).cdesc with
|
409
|
| Cvar -> (
|
410
|
match !ck_var with
|
411
|
| None ->
|
412
|
ck_var := Some ck
|
413
|
| Some v ->
|
414
|
(* cannot fail *)
|
415
|
try_unify ck v loc)
|
416
|
| Ctuple cl ->
|
417
|
List.iter aux cl
|
418
|
| Carrow (ck1, ck2) ->
|
419
|
aux ck1;
|
420
|
aux ck2
|
421
|
| Ccarrying (_, ck1) ->
|
422
|
aux ck1
|
423
|
| Con (ck1, _, _) ->
|
424
|
aux ck1
|
425
|
| _ ->
|
426
|
()
|
427
|
in
|
428
|
aux ck
|
429
|
|
430
|
(* Computes the root clock of a tuple or a node clock, which is not the same as
|
431
|
the base clock. Root clock will be used as the call clock of a given node
|
432
|
instance *)
|
433
|
let compute_root_clock ck =
|
434
|
let root = Clocks.root ck in
|
435
|
let branch = ref None in
|
436
|
let rec aux ck =
|
437
|
match (repr ck).cdesc with
|
438
|
| Ctuple cl ->
|
439
|
List.iter aux cl
|
440
|
| Carrow (ck1, ck2) ->
|
441
|
aux ck1;
|
442
|
aux ck2
|
443
|
| _ -> (
|
444
|
match !branch with
|
445
|
| None ->
|
446
|
branch := Some (Clocks.branch ck)
|
447
|
| Some br ->
|
448
|
(* cannot fail *)
|
449
|
branch := Some (Clocks.common_prefix br (Clocks.branch ck)))
|
450
|
in
|
451
|
aux ck;
|
452
|
Clocks.clock_of_root_branch root (Utils.desome !branch)
|
453
|
|
454
|
(* Clocks a list of arguments of Lustre builtin operators: - type each
|
455
|
expression, remove carriers of clocks as carriers may only denote variables,
|
456
|
not arbitrary expr. - try to unify these clocks altogether *)
|
457
|
let rec clock_standard_args env expr_list =
|
458
|
let ck_list =
|
459
|
List.map (fun e -> clock_uncarry (clock_expr env e)) expr_list
|
460
|
in
|
461
|
let ck_res = new_var true in
|
462
|
List.iter2 (fun e ck -> try_unify ck ck_res e.expr_loc) expr_list ck_list;
|
463
|
ck_res
|
464
|
|
465
|
(* emulates a subtyping relation between clocks c and (cr : c), used during node
|
466
|
application only *)
|
467
|
and clock_subtyping_arg env ?(sub = true) real_arg formal_clock =
|
468
|
let loc = real_arg.expr_loc in
|
469
|
let real_clock = clock_expr env real_arg in
|
470
|
try_sub_unify sub formal_clock real_clock loc
|
471
|
|
472
|
(* computes clocks for node application *)
|
473
|
and clock_appl env f args clock_reset loc =
|
474
|
let args = expr_list_of_expr args in
|
475
|
if Basic_library.is_homomorphic_fun f && List.exists is_tuple_expr args then
|
476
|
let args = Utils.transpose_list (List.map expr_list_of_expr args) in
|
477
|
Clocks.clock_of_clock_list
|
478
|
(List.map (fun args -> clock_call env f args clock_reset loc) args)
|
479
|
else clock_call env f args clock_reset loc
|
480
|
|
481
|
and clock_call env f args clock_reset loc =
|
482
|
(* Format.eprintf "Clocking call %s@." f; *)
|
483
|
let cfun = clock_ident false env f loc in
|
484
|
let cins, couts = split_arrow cfun in
|
485
|
let cins = clock_list_of_clock cins in
|
486
|
List.iter2 (clock_subtyping_arg env) args cins;
|
487
|
unify_imported_clock (Some clock_reset) cfun loc;
|
488
|
couts
|
489
|
|
490
|
and clock_ident nocarrier env id loc =
|
491
|
clock_expr ~nocarrier env (expr_of_ident id loc)
|
492
|
|
493
|
and clock_carrier env c loc ce =
|
494
|
let expr_c = expr_of_ident c loc in
|
495
|
let ck = clock_expr ~nocarrier:false env expr_c in
|
496
|
let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in
|
497
|
let ckb = new_var true in
|
498
|
let ckcarry = new_ck (Ccarrying (cr, ckb)) ck.cscoped in
|
499
|
try_unify ck ckcarry expr_c.expr_loc;
|
500
|
unify_tuple_clock (Some ckb) ce expr_c.expr_loc;
|
501
|
cr
|
502
|
|
503
|
(** [clock_expr env expr] performs the clock calculus for expression [expr] in
|
504
|
environment [env] *)
|
505
|
and clock_expr ?(nocarrier = true) env expr =
|
506
|
let resulting_ck =
|
507
|
match expr.expr_desc with
|
508
|
| Expr_const _ ->
|
509
|
let ck = new_var true in
|
510
|
expr.expr_clock <- ck;
|
511
|
ck
|
512
|
| Expr_ident v ->
|
513
|
let ckv =
|
514
|
try Env.lookup_value env v
|
515
|
with Not_found ->
|
516
|
failwith ("Internal error, variable \"" ^ v ^ "\" not found")
|
517
|
in
|
518
|
let ck = instantiate (ref []) (ref []) ckv in
|
519
|
expr.expr_clock <- ck;
|
520
|
ck
|
521
|
| Expr_array elist ->
|
522
|
let ck = clock_standard_args env elist in
|
523
|
expr.expr_clock <- ck;
|
524
|
ck
|
525
|
| Expr_access (e1, _) ->
|
526
|
(* dimension, being a static value, doesn't need to be clocked *)
|
527
|
let ck = clock_standard_args env [ e1 ] in
|
528
|
expr.expr_clock <- ck;
|
529
|
ck
|
530
|
| Expr_power (e1, _) ->
|
531
|
(* dimension, being a static value, doesn't need to be clocked *)
|
532
|
let ck = clock_standard_args env [ e1 ] in
|
533
|
expr.expr_clock <- ck;
|
534
|
ck
|
535
|
| Expr_tuple elist ->
|
536
|
let ck = new_ck (Ctuple (List.map (clock_expr env) elist)) true in
|
537
|
expr.expr_clock <- ck;
|
538
|
ck
|
539
|
| Expr_ite (c, t, e) ->
|
540
|
let ck_c = clock_standard_args env [ c ] in
|
541
|
let ck = clock_standard_args env [ t; e ] in
|
542
|
(* Here, the branches may exhibit a tuple clock, not the condition *)
|
543
|
unify_tuple_clock (Some ck_c) ck expr.expr_loc;
|
544
|
expr.expr_clock <- ck;
|
545
|
ck
|
546
|
| Expr_appl (id, args, r) -> (
|
547
|
try
|
548
|
(* for a modular compilation scheme, all inputs/outputs must share the
|
549
|
same clock ! this is also the reset clock ! *)
|
550
|
let cr =
|
551
|
match r with
|
552
|
| None ->
|
553
|
new_var true
|
554
|
| Some c ->
|
555
|
clock_standard_args env [ c ]
|
556
|
in
|
557
|
let couts = clock_appl env id args (clock_uncarry cr) expr.expr_loc in
|
558
|
expr.expr_clock <- couts;
|
559
|
couts
|
560
|
with exn ->
|
561
|
Format.eprintf "Current expr: %a@." Printers.pp_expr expr;
|
562
|
raise exn)
|
563
|
| Expr_fby (e1, e2) | Expr_arrow (e1, e2) ->
|
564
|
let ck = clock_standard_args env [ e1; e2 ] in
|
565
|
unify_tuple_clock None ck expr.expr_loc;
|
566
|
expr.expr_clock <- ck;
|
567
|
ck
|
568
|
| Expr_pre e ->
|
569
|
(* todo : deal with phases as in tail ? *)
|
570
|
let ck = clock_standard_args env [ e ] in
|
571
|
expr.expr_clock <- ck;
|
572
|
ck
|
573
|
| Expr_when (e, c, l) ->
|
574
|
let ce = clock_standard_args env [ e ] in
|
575
|
let c_loc = loc_of_cond expr.expr_loc c in
|
576
|
let cr = clock_carrier env c c_loc ce in
|
577
|
let ck = clock_on ce cr l in
|
578
|
let cr' = new_carrier (Carry_const c) ck.cscoped in
|
579
|
let ck' = clock_on ce cr' l in
|
580
|
expr.expr_clock <- ck';
|
581
|
ck
|
582
|
| Expr_merge (c, hl) ->
|
583
|
let cvar = new_var true in
|
584
|
let crvar = new_carrier Carry_name true in
|
585
|
List.iter
|
586
|
(fun (t, h) ->
|
587
|
let ckh = clock_uncarry (clock_expr env h) in
|
588
|
unify_tuple_clock
|
589
|
(Some (new_ck (Con (cvar, crvar, t)) true))
|
590
|
ckh h.expr_loc)
|
591
|
hl;
|
592
|
let cr = clock_carrier env c expr.expr_loc cvar in
|
593
|
try_unify_carrier cr crvar expr.expr_loc;
|
594
|
let cres = clock_current (snd (List.hd hl)).expr_clock in
|
595
|
expr.expr_clock <- cres;
|
596
|
cres
|
597
|
in
|
598
|
Log.report ~level:4 (fun fmt ->
|
599
|
Format.fprintf fmt "Clock of expr %a: %a@ " Printers.pp_expr expr
|
600
|
Clocks.print_ck resulting_ck);
|
601
|
resulting_ck
|
602
|
|
603
|
let clock_of_vlist vars =
|
604
|
let ckl = List.map (fun v -> v.var_clock) vars in
|
605
|
clock_of_clock_list ckl
|
606
|
|
607
|
(** [clock_eq env eq] performs the clock-calculus for equation [eq] in
|
608
|
environment [env] *)
|
609
|
let clock_eq env eq =
|
610
|
let expr_lhs =
|
611
|
expr_of_expr_list eq.eq_loc
|
612
|
(List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs)
|
613
|
in
|
614
|
let ck_rhs = clock_expr env eq.eq_rhs in
|
615
|
clock_subtyping_arg env expr_lhs ck_rhs
|
616
|
|
617
|
(* [clock_coreclock cck] returns the clock_expr corresponding to clock
|
618
|
declaration [cck] *)
|
619
|
let clock_coreclock env cck id loc scoped =
|
620
|
match cck.ck_dec_desc with
|
621
|
| Ckdec_any ->
|
622
|
new_var scoped
|
623
|
| Ckdec_bool cl ->
|
624
|
let temp_env = Env.add_value env id (new_var true) in
|
625
|
(* We just want the id to be present in the environment *)
|
626
|
let dummy_id_expr = expr_of_ident id loc in
|
627
|
let when_expr =
|
628
|
List.fold_left
|
629
|
(fun expr (x, l) ->
|
630
|
{
|
631
|
expr_tag = new_tag ();
|
632
|
expr_desc = Expr_when (expr, x, l);
|
633
|
expr_type = Types.new_var ();
|
634
|
expr_clock = new_var scoped;
|
635
|
expr_delay = Delay.new_var ();
|
636
|
expr_loc = loc;
|
637
|
expr_annot = None;
|
638
|
})
|
639
|
dummy_id_expr cl
|
640
|
in
|
641
|
clock_expr temp_env when_expr
|
642
|
|
643
|
(* Clocks a variable declaration *)
|
644
|
let clock_var_decl scoped env vdecl =
|
645
|
let ck =
|
646
|
clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped
|
647
|
in
|
648
|
let ck =
|
649
|
(* WTF ???? if vdecl.var_dec_const then (try_generalize ck vdecl.var_loc;
|
650
|
ck) else *)
|
651
|
if Types.get_clock_base_type vdecl.var_type <> None then
|
652
|
new_ck (Ccarrying (new_carrier Carry_name scoped, ck)) scoped
|
653
|
else ck
|
654
|
in
|
655
|
(if vdecl.var_dec_const then
|
656
|
match vdecl.var_dec_value with
|
657
|
| None ->
|
658
|
()
|
659
|
| Some v ->
|
660
|
let ck_static = clock_expr env v in
|
661
|
try_unify ck ck_static v.expr_loc);
|
662
|
try_unify ck vdecl.var_clock vdecl.var_loc;
|
663
|
Env.add_value env vdecl.var_id ck
|
664
|
|
665
|
(* Clocks a variable declaration list *)
|
666
|
let clock_var_decl_list env scoped l =
|
667
|
List.fold_left (clock_var_decl scoped) env l
|
668
|
|
669
|
(** [clock_node env nd] performs the clock-calculus for node [nd] in environment
|
670
|
[env]. Generalization of clocks wrt scopes follows this rule: - generalize
|
671
|
inputs (unscoped). - generalize outputs. As they are scoped, only clocks
|
672
|
coming from inputs are allowed to be generalized. - generalize locals. As
|
673
|
outputs don't depend on them (checked the step before), they can be
|
674
|
generalized. *)
|
675
|
let clock_node env loc nd =
|
676
|
(* let is_main = nd.node_id = !Options.main_node in *)
|
677
|
let new_env = clock_var_decl_list env false nd.node_inputs in
|
678
|
let new_env = clock_var_decl_list new_env true nd.node_outputs in
|
679
|
let new_env = clock_var_decl_list new_env true nd.node_locals in
|
680
|
let eqs, _ = get_node_eqs nd in
|
681
|
(* TODO XXX: perform the clocking on auts. For the moment, it is ignored *)
|
682
|
List.iter (clock_eq new_env) eqs;
|
683
|
let ck_ins = clock_of_vlist nd.node_inputs in
|
684
|
let ck_outs = clock_of_vlist nd.node_outputs in
|
685
|
let ck_node = new_ck (Carrow (ck_ins, ck_outs)) false in
|
686
|
unify_imported_clock None ck_node loc;
|
687
|
Log.report ~level:3 (fun fmt ->
|
688
|
Format.fprintf fmt "Clock of %s: %a@ " nd.node_id print_ck ck_node);
|
689
|
(* Local variables may contain first-order carrier variables that should be
|
690
|
generalized. That's not the case for types. *)
|
691
|
try_generalize ck_node loc;
|
692
|
(* List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc)
|
693
|
nd.node_inputs; List.iter (fun vdecl -> try_generalize vdecl.var_clock
|
694
|
vdecl.var_loc) nd.node_outputs;*)
|
695
|
(*List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc)
|
696
|
nd.node_locals;*)
|
697
|
(* TODO : Xavier pourquoi ai je cette erreur ? *)
|
698
|
(* if (is_main && is_polymorphic ck_node) then raise (Error
|
699
|
(loc,(Cannot_be_polymorphic ck_node))); *)
|
700
|
Log.report ~level:3 (fun fmt ->
|
701
|
Format.fprintf fmt "Generalized clock of %s: %a@ @ " nd.node_id print_ck
|
702
|
ck_node);
|
703
|
nd.node_clock <- ck_node;
|
704
|
Env.add_value env nd.node_id ck_node
|
705
|
|
706
|
let check_imported_pclocks loc ck_node =
|
707
|
let pck = ref None in
|
708
|
let rec aux ck =
|
709
|
match ck.cdesc with
|
710
|
| Carrow (ck1, ck2) ->
|
711
|
aux ck1;
|
712
|
aux ck2
|
713
|
| Ctuple cl ->
|
714
|
List.iter aux cl
|
715
|
| Con (ck', _, _) ->
|
716
|
aux ck'
|
717
|
| Clink ck' ->
|
718
|
aux ck'
|
719
|
| Ccarrying (_, ck') ->
|
720
|
aux ck'
|
721
|
| Cvar | Cunivar -> (
|
722
|
match !pck with
|
723
|
| None ->
|
724
|
()
|
725
|
| Some (_, _) ->
|
726
|
raise (Error (loc, Invalid_imported_clock ck_node)))
|
727
|
in
|
728
|
aux ck_node
|
729
|
|
730
|
let clock_imported_node env loc nd =
|
731
|
let new_env = clock_var_decl_list env false nd.nodei_inputs in
|
732
|
ignore (clock_var_decl_list new_env false nd.nodei_outputs);
|
733
|
let ck_ins = clock_of_vlist nd.nodei_inputs in
|
734
|
let ck_outs = clock_of_vlist nd.nodei_outputs in
|
735
|
let ck_node = new_ck (Carrow (ck_ins, ck_outs)) false in
|
736
|
unify_imported_clock None ck_node loc;
|
737
|
check_imported_pclocks loc ck_node;
|
738
|
try_generalize ck_node loc;
|
739
|
nd.nodei_clock <- ck_node;
|
740
|
Env.add_value env nd.nodei_id ck_node
|
741
|
|
742
|
let new_env = clock_var_decl_list
|
743
|
|
744
|
let clock_top_const env cdecl =
|
745
|
let ck = new_var false in
|
746
|
try_generalize ck cdecl.const_loc;
|
747
|
Env.add_value env cdecl.const_id ck
|
748
|
|
749
|
let clock_top_consts env clist = List.fold_left clock_top_const env clist
|
750
|
|
751
|
let rec clock_top_decl env decl =
|
752
|
match decl.top_decl_desc with
|
753
|
| Node nd ->
|
754
|
clock_node env decl.top_decl_loc nd
|
755
|
| ImportedNode nd ->
|
756
|
clock_imported_node env decl.top_decl_loc nd
|
757
|
| Const c ->
|
758
|
clock_top_const env c
|
759
|
| TypeDef _ ->
|
760
|
List.fold_left clock_top_decl env (consts_of_enum_type decl)
|
761
|
| Include _ | Open _ ->
|
762
|
env
|
763
|
|
764
|
let clock_prog env decls = List.fold_left clock_top_decl env decls
|
765
|
|
766
|
(* Once the Lustre program is fully clocked, we must get back to the original
|
767
|
description of clocks, with constant parameters, instead of unifiable
|
768
|
internal variables. *)
|
769
|
|
770
|
(* The following functions aims at 'unevaluating' carriers occuring in clock
|
771
|
expressions, i.e. replacing unifiable second_order variables with the
|
772
|
original carrier names. Once restored in this formulation, clocks may be
|
773
|
meaningfully printed. *)
|
774
|
let uneval_vdecl_generics vdecl =
|
775
|
(*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@."
|
776
|
Printers.pp_node_var vdecl;*)
|
777
|
if Types.get_clock_base_type vdecl.var_type <> None then
|
778
|
match get_carrier_name vdecl.var_clock with
|
779
|
| None ->
|
780
|
Format.eprintf "internal error: %a@." print_ck vdecl.var_clock;
|
781
|
assert false
|
782
|
| Some cr ->
|
783
|
Clocks.uneval vdecl.var_id cr
|
784
|
|
785
|
let uneval_node_generics vdecls = List.iter uneval_vdecl_generics vdecls
|
786
|
|
787
|
let uneval_top_generics decl =
|
788
|
match decl.top_decl_desc with
|
789
|
| Node nd ->
|
790
|
(* A node could contain first-order carrier variable in local vars. This is
|
791
|
not the case for types. *)
|
792
|
uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)
|
793
|
| ImportedNode nd ->
|
794
|
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
|
795
|
| Const _ | Include _ | Open _ | TypeDef _ ->
|
796
|
()
|
797
|
|
798
|
let uneval_prog_generics prog = List.iter uneval_top_generics prog
|
799
|
|
800
|
let check_env_compat header declared computed =
|
801
|
uneval_prog_generics header;
|
802
|
Env.iter declared (fun k decl_clock_k ->
|
803
|
try
|
804
|
let computed_c =
|
805
|
instantiate (ref []) (ref []) (Env.lookup_value computed k)
|
806
|
in
|
807
|
try_semi_unify decl_clock_k computed_c Location.dummy_loc
|
808
|
with Not_found ->
|
809
|
(* If the lookup failed then either an actual required element should
|
810
|
have been declared and is missing but typing should have catch it, or
|
811
|
it was a contract and does not require this additional check. *)
|
812
|
())
|
813
|
(* Local Variables: *)
|
814
|
(* compile-command:"make -C .." *)
|
815
|
(* End: *)
|