Project

General

Profile

Download (26.6 KB) Statistics
| Branch: | Tag: | Revision:
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: *)
(10-10/66)