Project

General

Profile

Download (26.5 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 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 env id loc = clock_expr env (expr_of_ident id loc)
491

    
492
and clock_carrier env c loc ce =
493
  let expr_c = expr_of_ident c loc in
494
  let ck = clock_expr env expr_c in
495
  let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in
496
  let ckb = new_var true in
497
  let ckcarry = new_ck (Ccarrying (cr, ckb)) ck.cscoped in
498
  try_unify ck ckcarry expr_c.expr_loc;
499
  unify_tuple_clock (Some ckb) ce expr_c.expr_loc;
500
  cr
501

    
502
(** [clock_expr env expr] performs the clock calculus for expression [expr] in
503
    environment [env] *)
504
and clock_expr env expr =
505
  let resulting_ck =
506
    match expr.expr_desc with
507
    | Expr_const _ ->
508
      let ck = new_var true in
509
      expr.expr_clock <- ck;
510
      ck
511
    | Expr_ident v ->
512
      let ckv =
513
        try Env.lookup_value env v
514
        with Not_found ->
515
          failwith ("Internal error, variable \"" ^ v ^ "\" not found")
516
      in
517
      let ck = instantiate (ref []) (ref []) ckv in
518
      expr.expr_clock <- ck;
519
      ck
520
    | Expr_array elist ->
521
      let ck = clock_standard_args env elist in
522
      expr.expr_clock <- ck;
523
      ck
524
    | Expr_access (e1, _) ->
525
      (* dimension, being a static value, doesn't need to be clocked *)
526
      let ck = clock_standard_args env [ e1 ] in
527
      expr.expr_clock <- ck;
528
      ck
529
    | Expr_power (e1, _) ->
530
      (* dimension, being a static value, doesn't need to be clocked *)
531
      let ck = clock_standard_args env [ e1 ] in
532
      expr.expr_clock <- ck;
533
      ck
534
    | Expr_tuple elist ->
535
      let ck = new_ck (Ctuple (List.map (clock_expr env) elist)) true in
536
      expr.expr_clock <- ck;
537
      ck
538
    | Expr_ite (c, t, e) ->
539
      let ck_c = clock_standard_args env [ c ] in
540
      let ck = clock_standard_args env [ t; e ] in
541
      (* Here, the branches may exhibit a tuple clock, not the condition *)
542
      unify_tuple_clock (Some ck_c) ck expr.expr_loc;
543
      expr.expr_clock <- ck;
544
      ck
545
    | Expr_appl (id, args, r) -> (
546
      try
547
        (* for a modular compilation scheme, all inputs/outputs must share the
548
           same clock ! this is also the reset clock ! *)
549
        let cr =
550
          match r with
551
          | None ->
552
            new_var true
553
          | Some c ->
554
            clock_standard_args env [ c ]
555
        in
556
        let couts = clock_appl env id args (clock_uncarry cr) expr.expr_loc in
557
        expr.expr_clock <- couts;
558
        couts
559
      with exn ->
560
        Format.eprintf "Current expr: %a@." Printers.pp_expr expr;
561
        raise exn)
562
    | Expr_fby (e1, e2) | Expr_arrow (e1, e2) ->
563
      let ck = clock_standard_args env [ e1; e2 ] in
564
      unify_tuple_clock None ck expr.expr_loc;
565
      expr.expr_clock <- ck;
566
      ck
567
    | Expr_pre e ->
568
      (* todo : deal with phases as in tail ? *)
569
      let ck = clock_standard_args env [ e ] in
570
      expr.expr_clock <- ck;
571
      ck
572
    | Expr_when (e, c, l) ->
573
      let ce = clock_standard_args env [ e ] in
574
      let c_loc = loc_of_cond expr.expr_loc c in
575
      let cr = clock_carrier env c c_loc ce in
576
      let ck = clock_on ce cr l in
577
      let cr' = new_carrier (Carry_const c) ck.cscoped in
578
      let ck' = clock_on ce cr' l in
579
      expr.expr_clock <- ck';
580
      ck
581
    | Expr_merge (c, hl) ->
582
      let cvar = new_var true in
583
      let crvar = new_carrier Carry_name true in
584
      List.iter
585
        (fun (t, h) ->
586
          let ckh = clock_uncarry (clock_expr env h) in
587
          unify_tuple_clock
588
            (Some (new_ck (Con (cvar, crvar, t)) true))
589
            ckh h.expr_loc)
590
        hl;
591
      let cr = clock_carrier env c expr.expr_loc cvar in
592
      try_unify_carrier cr crvar expr.expr_loc;
593
      let cres = clock_current (snd (List.hd hl)).expr_clock in
594
      expr.expr_clock <- cres;
595
      cres
596
  in
597
  Log.report ~level:4 (fun fmt ->
598
      Format.fprintf fmt "Clock of expr %a: %a@ " Printers.pp_expr expr
599
        Clocks.print_ck resulting_ck);
600
  resulting_ck
601

    
602
let clock_of_vlist vars =
603
  let ckl = List.map (fun v -> v.var_clock) vars in
604
  clock_of_clock_list ckl
605

    
606
(** [clock_eq env eq] performs the clock-calculus for equation [eq] in
607
    environment [env] *)
608
let clock_eq env eq =
609
  let expr_lhs =
610
    expr_of_expr_list eq.eq_loc
611
      (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs)
612
  in
613
  let ck_rhs = clock_expr env eq.eq_rhs in
614
  clock_subtyping_arg env expr_lhs ck_rhs
615

    
616
(* [clock_coreclock cck] returns the clock_expr corresponding to clock
617
   declaration [cck] *)
618
let clock_coreclock env cck id loc scoped =
619
  match cck.ck_dec_desc with
620
  | Ckdec_any ->
621
    new_var scoped
622
  | Ckdec_bool cl ->
623
    let temp_env = Env.add_value env id (new_var true) in
624
    (* We just want the id to be present in the environment *)
625
    let dummy_id_expr = expr_of_ident id loc in
626
    let when_expr =
627
      List.fold_left
628
        (fun expr (x, l) ->
629
          {
630
            expr_tag = new_tag ();
631
            expr_desc = Expr_when (expr, x, l);
632
            expr_type = Types.new_var ();
633
            expr_clock = new_var scoped;
634
            expr_delay = Delay.new_var ();
635
            expr_loc = loc;
636
            expr_annot = None;
637
          })
638
        dummy_id_expr cl
639
    in
640
    clock_expr temp_env when_expr
641

    
642
(* Clocks a variable declaration *)
643
let clock_var_decl scoped env vdecl =
644
  let ck =
645
    clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped
646
  in
647
  let ck =
648
    (* WTF ???? if vdecl.var_dec_const then (try_generalize ck vdecl.var_loc;
649
       ck) else *)
650
    if Types.get_clock_base_type vdecl.var_type <> None then
651
      new_ck (Ccarrying (new_carrier Carry_name scoped, ck)) scoped
652
    else ck
653
  in
654
  (if vdecl.var_dec_const then
655
   match vdecl.var_dec_value with
656
   | None ->
657
     ()
658
   | Some v ->
659
     let ck_static = clock_expr env v in
660
     try_unify ck ck_static v.expr_loc);
661
  try_unify ck vdecl.var_clock vdecl.var_loc;
662
  Env.add_value env vdecl.var_id ck
663

    
664
(* Clocks a variable declaration list *)
665
let clock_var_decl_list env scoped l =
666
  List.fold_left (clock_var_decl scoped) env l
667

    
668
(** [clock_node env nd] performs the clock-calculus for node [nd] in environment
669
    [env]. Generalization of clocks wrt scopes follows this rule: - generalize
670
    inputs (unscoped). - generalize outputs. As they are scoped, only clocks
671
    coming from inputs are allowed to be generalized. - generalize locals. As
672
    outputs don't depend on them (checked the step before), they can be
673
    generalized. *)
674
let clock_node env loc nd =
675
  (* let is_main = nd.node_id = !Options.main_node in *)
676
  let new_env = clock_var_decl_list env false nd.node_inputs in
677
  let new_env = clock_var_decl_list new_env true nd.node_outputs in
678
  let new_env = clock_var_decl_list new_env true nd.node_locals in
679
  let eqs, _ = get_node_eqs nd in
680
  (* TODO XXX: perform the clocking on auts. For the moment, it is ignored *)
681
  List.iter (clock_eq new_env) eqs;
682
  let ck_ins = clock_of_vlist nd.node_inputs in
683
  let ck_outs = clock_of_vlist nd.node_outputs in
684
  let ck_node = new_ck (Carrow (ck_ins, ck_outs)) false in
685
  unify_imported_clock None ck_node loc;
686
  Log.report ~level:3 (fun fmt ->
687
      Format.fprintf fmt "Clock of %s: %a@ " nd.node_id print_ck ck_node);
688
  (* Local variables may contain first-order carrier variables that should be
689
     generalized. That's not the case for types. *)
690
  try_generalize ck_node loc;
691
  (* List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc)
692
     nd.node_inputs; List.iter (fun vdecl -> try_generalize vdecl.var_clock
693
     vdecl.var_loc) nd.node_outputs;*)
694
  (*List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc)
695
    nd.node_locals;*)
696
  (* TODO : Xavier pourquoi ai je cette erreur ? *)
697
  (* if (is_main && is_polymorphic ck_node) then raise (Error
698
     (loc,(Cannot_be_polymorphic ck_node))); *)
699
  Log.report ~level:3 (fun fmt ->
700
      Format.fprintf fmt "Generalized clock of %s: %a@ @ " nd.node_id print_ck
701
        ck_node);
702
  nd.node_clock <- ck_node;
703
  Env.add_value env nd.node_id ck_node
704

    
705
let check_imported_pclocks loc ck_node =
706
  let pck = ref None in
707
  let rec aux ck =
708
    match ck.cdesc with
709
    | Carrow (ck1, ck2) ->
710
      aux ck1;
711
      aux ck2
712
    | Ctuple cl ->
713
      List.iter aux cl
714
    | Con (ck', _, _) ->
715
      aux ck'
716
    | Clink ck' ->
717
      aux ck'
718
    | Ccarrying (_, ck') ->
719
      aux ck'
720
    | Cvar | Cunivar -> (
721
      match !pck with
722
      | None ->
723
        ()
724
      | Some (_, _) ->
725
        raise (Error (loc, Invalid_imported_clock ck_node)))
726
  in
727
  aux ck_node
728

    
729
let clock_imported_node env loc nd =
730
  let new_env = clock_var_decl_list env false nd.nodei_inputs in
731
  ignore (clock_var_decl_list new_env false nd.nodei_outputs);
732
  let ck_ins = clock_of_vlist nd.nodei_inputs in
733
  let ck_outs = clock_of_vlist nd.nodei_outputs in
734
  let ck_node = new_ck (Carrow (ck_ins, ck_outs)) false in
735
  unify_imported_clock None ck_node loc;
736
  check_imported_pclocks loc ck_node;
737
  try_generalize ck_node loc;
738
  nd.nodei_clock <- ck_node;
739
  Env.add_value env nd.nodei_id ck_node
740

    
741
let new_env = clock_var_decl_list
742

    
743
let clock_top_const env cdecl =
744
  let ck = new_var false in
745
  try_generalize ck cdecl.const_loc;
746
  Env.add_value env cdecl.const_id ck
747

    
748
let clock_top_consts env clist = List.fold_left clock_top_const env clist
749

    
750
let rec clock_top_decl env decl =
751
  match decl.top_decl_desc with
752
  | Node nd ->
753
    clock_node env decl.top_decl_loc nd
754
  | ImportedNode nd ->
755
    clock_imported_node env decl.top_decl_loc nd
756
  | Const c ->
757
    clock_top_const env c
758
  | TypeDef _ ->
759
    List.fold_left clock_top_decl env (consts_of_enum_type decl)
760
  | Include _ | Open _ ->
761
    env
762

    
763
let clock_prog env decls = List.fold_left clock_top_decl env decls
764

    
765
(* Once the Lustre program is fully clocked, we must get back to the original
766
   description of clocks, with constant parameters, instead of unifiable
767
   internal variables. *)
768

    
769
(* The following functions aims at 'unevaluating' carriers occuring in clock
770
   expressions, i.e. replacing unifiable second_order variables with the
771
   original carrier names. Once restored in this formulation, clocks may be
772
   meaningfully printed. *)
773
let uneval_vdecl_generics vdecl =
774
  (*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@."
775
    Printers.pp_node_var vdecl;*)
776
  if Types.get_clock_base_type vdecl.var_type <> None then
777
    match get_carrier_name vdecl.var_clock with
778
    | None ->
779
      Format.eprintf "internal error: %a@." print_ck vdecl.var_clock;
780
      assert false
781
    | Some cr ->
782
      Clocks.uneval vdecl.var_id cr
783

    
784
let uneval_node_generics vdecls = List.iter uneval_vdecl_generics vdecls
785

    
786
let uneval_top_generics decl =
787
  match decl.top_decl_desc with
788
  | Node nd ->
789
    (* A node could contain first-order carrier variable in local vars. This is
790
       not the case for types. *)
791
    uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)
792
  | ImportedNode nd ->
793
    uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
794
  | Const _ | Include _ | Open _ | TypeDef _ ->
795
    ()
796

    
797
let uneval_prog_generics prog = List.iter uneval_top_generics prog
798

    
799
let check_env_compat header declared computed =
800
  uneval_prog_generics header;
801
  Env.iter declared (fun k decl_clock_k ->
802
      try
803
        let computed_c =
804
          instantiate (ref []) (ref []) (Env.lookup_value computed k)
805
        in
806
        try_semi_unify decl_clock_k computed_c Location.dummy_loc
807
      with Not_found ->
808
        (* If the lookup failed then either an actual required element should
809
           have been declared and is missing but typing should have catch it, or
810
           it was a contract and does not require this additional check. *)
811
        ())
812
(* Local Variables: *)
813
(* compile-command:"make -C .." *)
814
(* End: *)
(10-10/66)