Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / clock_calculus.ml @ 3b2bd83d

History | View | Annotate | Download (26.6 KB)

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

    
15
(** Main clock-calculus module. Based on type inference algorithms with
16
  destructive unification. Uses a bit of subtyping for periodic clocks. *)
17

    
18
(* Though it shares similarities with the typing module, no code
19
    is shared.  Simple environments, very limited identifier scoping, no
20
    identifier redefinition allowed. *)
21
open Utils
22
open LustreSpec
23
open Corelang
24
open Clocks
25
open Format
26

    
27
let loc_of_cond loc_containing id =
28
  let pos_start =
29
    {loc_containing.Location.loc_end with 
30
     Lexing.pos_cnum=loc_containing.Location.loc_end.Lexing.pos_cnum-(String.length id)}
31
  in
32
  {Location.loc_start = pos_start;
33
   Location.loc_end = loc_containing.Location.loc_end}
34

    
35
(** [occurs cvar ck] returns true if the clock variable [cvar] occurs in
36
    clock [ck]. False otherwise. *)
37
let rec occurs cvar ck =
38
  let ck = repr ck in
39
  match ck.cdesc with
40
  | Carrow (ck1, ck2) ->
41
      (occurs cvar ck1) || (occurs cvar ck2)
42
  | Ctuple ckl ->
43
      List.exists (occurs cvar) ckl
44
  | Con (ck',_,_) -> occurs cvar ck'
45
  | Cvar  -> ck=cvar
46
  | Cunivar   -> false
47
  | Clink ck' -> occurs cvar ck'
48
  | Ccarrying (_,ck') -> occurs cvar ck'
49

    
50
(* Clocks generalization *)
51
let rec generalize_carrier cr =
52
  match cr.carrier_desc with
53
  | Carry_const _
54
  | Carry_name ->
55
      if cr.carrier_scoped then
56
        raise (Scope_carrier cr);
57
      cr.carrier_desc <- Carry_var
58
  | Carry_var -> ()
59
  | Carry_link cr' -> generalize_carrier cr'
60

    
61
(** Promote monomorphic clock variables to polymorphic clock variables. *)
62
(* Generalize by side-effects *)
63
let rec generalize ck =
64
    match ck.cdesc with
65
    | Carrow (ck1,ck2) ->
66
        generalize ck1; generalize ck2
67
    | Ctuple clist ->
68
        List.iter generalize clist
69
    | Con (ck',cr,_) -> generalize ck'; generalize_carrier cr
70
    | Cvar ->
71
        if ck.cscoped then
72
          raise (Scope_clock ck);
73
        ck.cdesc <- Cunivar 
74
    | Cunivar -> () 
75
    | Clink ck' ->
76
        generalize ck'
77
    | Ccarrying (cr,ck') ->
78
        generalize_carrier cr; generalize ck'
79

    
80
let try_generalize ck_node loc =
81
  try 
82
    generalize ck_node
83
  with (Scope_carrier cr) ->
84
    raise (Error (loc, Carrier_extrusion (ck_node, cr)))
85
  | (Scope_clock ck) ->
86
    raise (Error (loc, Clock_extrusion (ck_node, ck)))
87

    
88
(* Clocks instanciation *)
89
let instantiate_carrier cr inst_cr_vars =
90
  let cr = carrier_repr cr in
91
  match cr.carrier_desc with
92
  | Carry_const _
93
  | Carry_name -> cr
94
  | Carry_link _ ->
95
      failwith "Internal error"
96
  | Carry_var ->
97
      try
98
        List.assoc cr.carrier_id !inst_cr_vars
99
      with Not_found ->            
100
        let cr_var = new_carrier Carry_name true in
101
        inst_cr_vars := (cr.carrier_id,cr_var)::!inst_cr_vars;
102
        cr_var
103

    
104
(** Downgrade polymorphic clock variables to monomorphic clock variables *)
105
(* inst_ck_vars ensures that a polymorphic variable is instanciated with
106
   the same monomorphic variable if it occurs several times in the same
107
   type. inst_cr_vars is the same for carriers. *)
108
let rec instantiate inst_ck_vars inst_cr_vars ck =
109
  match ck.cdesc with
110
  | Carrow (ck1,ck2) ->
111
      {ck with cdesc =
112
       Carrow ((instantiate inst_ck_vars inst_cr_vars ck1),
113
               (instantiate inst_ck_vars inst_cr_vars ck2))}
114
  | Ctuple cklist ->
115
      {ck with cdesc = Ctuple 
116
         (List.map (instantiate inst_ck_vars inst_cr_vars) cklist)}
117
  | Con (ck',c,l) ->
118
      let c' = instantiate_carrier c inst_cr_vars in
119
      {ck with cdesc = Con ((instantiate inst_ck_vars inst_cr_vars ck'),c',l)}
120
  | Cvar  -> ck
121
  | Clink ck' ->
122
      {ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')}
123
  | Ccarrying (cr,ck') ->
124
      let cr' = instantiate_carrier cr inst_cr_vars in
125
        {ck with cdesc =
126
         Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')}
127
  | Cunivar ->
128
      try
129
        List.assoc ck.cid !inst_ck_vars
130
      with Not_found ->
131
        let var = new_ck Cvar true in
132
	inst_ck_vars := (ck.cid, var)::!inst_ck_vars;
133
	var
134

    
135

    
136
let rec update_scope_carrier scoped cr =
137
  if (not scoped) then
138
    begin
139
      cr.carrier_scoped <- scoped;
140
      match cr.carrier_desc with
141
	| Carry_const _ | Carry_name | Carry_var -> ()
142
      | Carry_link cr' -> update_scope_carrier scoped cr'
143
    end
144

    
145
let rec update_scope scoped ck =
146
  if (not scoped) then
147
    begin
148
      ck.cscoped <- scoped;
149
      match ck.cdesc with
150
      | Carrow (ck1,ck2) ->
151
          update_scope scoped ck1; update_scope scoped ck2
152
      | Ctuple clist ->
153
          List.iter (update_scope scoped) clist
154
      | Con (ck',cr,_) -> update_scope scoped ck'(*; update_scope_carrier scoped cr*)
155
      | Cvar | Cunivar -> ()
156
      | Clink ck' ->
157
          update_scope scoped ck'
158
      | Ccarrying (cr,ck') ->
159
          update_scope_carrier scoped cr; update_scope scoped ck'
160
    end
161

    
162

    
163
(* Unifies two clock carriers *)
164
let unify_carrier cr1 cr2 =
165
  let cr1 = carrier_repr cr1 in
166
  let cr2 = carrier_repr cr2 in
167
  if cr1==cr2 then ()
168
  else
169
    match cr1.carrier_desc, cr2.carrier_desc with
170
    | Carry_const id1, Carry_const id2 ->
171
      if id1 <> id2 then raise (Mismatch (cr1, cr2))
172
    | Carry_const _, Carry_name ->
173
      begin
174
	cr2.carrier_desc <- Carry_link cr1;
175
	update_scope_carrier cr2.carrier_scoped cr1
176
      end
177
    | Carry_name, Carry_const _ ->
178
      begin
179
        cr1.carrier_desc <- Carry_link cr2;
180
        update_scope_carrier cr1.carrier_scoped cr2
181
      end
182
    | Carry_name, Carry_name ->
183
      if cr1.carrier_id < cr2.carrier_id then
184
        begin
185
          cr2.carrier_desc <- Carry_link cr1;
186
          update_scope_carrier cr2.carrier_scoped cr1
187
        end
188
      else
189
        begin
190
          cr1.carrier_desc <- Carry_link cr2;
191
          update_scope_carrier cr1.carrier_scoped cr2
192
        end
193
    | _,_ -> assert false
194

    
195
(* Semi-unifies two clock carriers *)
196
let semi_unify_carrier cr1 cr2 =
197
  let cr1 = carrier_repr cr1 in
198
  let cr2 = carrier_repr cr2 in
199
  if cr1==cr2 then ()
200
  else
201
    match cr1.carrier_desc, cr2.carrier_desc with
202
    | Carry_const id1, Carry_const id2 ->
203
      if id1 <> id2 then raise (Mismatch (cr1, cr2))
204
    | Carry_const _, Carry_name ->
205
      begin
206
	cr2.carrier_desc <- Carry_link cr1;
207
	update_scope_carrier cr2.carrier_scoped cr1
208
      end
209
    | Carry_name, Carry_const _ -> raise (Mismatch (cr1, cr2))
210
    | Carry_name, Carry_name ->
211
      if cr1.carrier_id < cr2.carrier_id then
212
        begin
213
          cr2.carrier_desc <- Carry_link cr1;
214
          update_scope_carrier cr2.carrier_scoped cr1
215
        end
216
      else
217
        begin
218
          cr1.carrier_desc <- Carry_link cr2;
219
          update_scope_carrier cr1.carrier_scoped cr2
220
        end
221
    | _,_ -> assert false
222

    
223
let try_unify_carrier ck1 ck2 loc =
224
  try
225
    unify_carrier ck1 ck2
226
  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
233
    (ck1,ck2)] if 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
    ()
239
  else
240
    match ck1.cdesc,ck2.cdesc with
241
    | Cvar, Cvar ->
242
      if ck1.cid < ck2.cid then
243
        begin
244
          ck2.cdesc <- Clink (simplify ck1);
245
          update_scope ck2.cscoped ck1
246
        end
247
      else
248
        begin
249
          ck1.cdesc <- Clink (simplify ck2);
250
          update_scope ck1.cscoped ck2
251
        end
252
    | (Cvar, _) when (not (occurs ck1 ck2)) ->
253
      update_scope ck1.cscoped ck2;
254
      ck1.cdesc <- Clink (simplify ck2)
255
    | (_, Cvar) when (not (occurs ck2 ck1)) ->
256
      update_scope ck2.cscoped ck1;
257
      ck2.cdesc <- Clink (simplify ck1)
258
    | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
259
      unify_carrier cr1 cr2;
260
      unify ck1' ck2'
261
    | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->
262
      raise (Unify (ck1,ck2))
263
    | Carrow (c1,c2), Carrow (c1',c2') ->
264
      unify c1 c1'; unify c2 c2'
265
    | Ctuple ckl1, Ctuple ckl2 ->
266
      if (List.length ckl1) <> (List.length ckl2) then
267
        raise (Unify (ck1,ck2));
268
      List.iter2 unify ckl1 ckl2
269
    | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
270
      unify_carrier c1 c2;
271
      unify ck' ck''
272
    | Cunivar, _ | _, Cunivar -> ()
273
    | _,_ -> raise (Unify (ck1,ck2))
274

    
275
(** [unify ck1 ck2] semi-unifies clocks [ck1] and [ck2]. Raises [Unify
276
    (ck1,ck2)] if the clocks are not semi-unifiable.*)
277
let rec semi_unify ck1 ck2 =
278
  let ck1 = repr ck1 in
279
  let ck2 = repr ck2 in
280
  if ck1==ck2 then
281
    ()
282
  else
283
      match ck1.cdesc,ck2.cdesc with
284
      | Cvar, Cvar ->
285
          if ck1.cid < ck2.cid then
286
            begin
287
              ck2.cdesc <- Clink (simplify ck1);
288
              update_scope ck2.cscoped ck1
289
            end
290
          else
291
            begin
292
              ck1.cdesc <- Clink (simplify ck2);
293
              update_scope ck1.cscoped ck2
294
            end
295
      | (Cvar, _) -> raise (Unify (ck1,ck2))
296
      | (_, Cvar) when (not (occurs ck2 ck1)) ->
297
          update_scope ck2.cscoped ck1;
298
          ck2.cdesc <- Clink (simplify ck1)
299
      | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
300
          semi_unify_carrier cr1 cr2;
301
          semi_unify ck1' ck2'
302
      | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->
303
          raise (Unify (ck1,ck2))
304
      | Carrow (c1,c2), Carrow (c1',c2') ->
305
	begin
306
          semi_unify c1 c1';
307
	  semi_unify c2 c2'
308
	end
309
      | Ctuple ckl1, Ctuple ckl2 ->
310
          if (List.length ckl1) <> (List.length ckl2) then
311
            raise (Unify (ck1,ck2));
312
          List.iter2 semi_unify ckl1 ckl2
313
      | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
314
          semi_unify_carrier c1 c2;
315
          semi_unify ck' ck''
316
      | Cunivar, _ | _, Cunivar -> ()
317
      | _,_ -> raise (Unify (ck1,ck2))
318

    
319
(* Returns the value corresponding to a pclock (integer) factor
320
   expression. Expects a constant expression (checked by typing). *)
321
let int_factor_of_expr e =
322
  match e.expr_desc with 
323
  | Expr_const
324
      (Const_int i) -> i
325
  | _ -> failwith "Internal error: int_factor_of_expr"
326

    
327
(** [clock_uncarry ck] drops the possible carrier(s) name(s) from clock [ck] *)
328
let rec clock_uncarry ck =
329
  let ck = repr ck in
330
  match ck.cdesc with
331
  | Ccarrying (_, ck') -> ck'
332
  | Con(ck', cr, l)    -> clock_on (clock_uncarry ck') cr l
333
  | Ctuple ckl         -> clock_of_clock_list (List.map clock_uncarry ckl)
334
  | _                  -> ck
335

    
336
let try_unify ck1 ck2 loc =
337
  try
338
    unify ck1 ck2
339
  with
340
  | Unify (ck1',ck2') ->
341
    raise (Error (loc, Clock_clash (ck1',ck2')))
342
  | Mismatch (cr1,cr2) ->
343
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
344

    
345
let try_semi_unify ck1 ck2 loc =
346
  try
347
    semi_unify ck1 ck2
348
  with
349
  | Unify (ck1',ck2') ->
350
    raise (Error (loc, Clock_clash (ck1',ck2')))
351
  | Mismatch (cr1,cr2) ->
352
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
353

    
354
(* ck2 is a subtype of ck1 *)
355
let rec sub_unify sub ck1 ck2 =
356
  match (repr ck1).cdesc, (repr ck2).cdesc with
357
  | Ctuple cl1         , Ctuple cl2         ->
358
    if List.length cl1 <> List.length cl2
359
    then raise (Unify (ck1, ck2))
360
    else List.iter2 (sub_unify sub) cl1 cl2
361
  | Ctuple [c1]        , _                  -> sub_unify sub c1 ck2
362
  | _                  , Ctuple [c2]        -> sub_unify sub ck1 c2
363
  | Con (c1, cr1, t1)  , Con (c2, cr2, t2) when t1=t2 ->
364
    begin
365
      unify_carrier cr1 cr2;
366
      sub_unify sub c1 c2
367
    end
368
  | Ccarrying (cr1, c1), Ccarrying (cr2, c2)->
369
    begin
370
      unify_carrier cr1 cr2;
371
      sub_unify sub c1 c2
372
    end
373
  | _, Ccarrying (_, c2)           when sub -> sub_unify sub ck1 c2
374
  | _                                       -> unify ck1 ck2
375

    
376
let try_sub_unify sub ck1 ck2 loc =
377
  try
378
    sub_unify sub ck1 ck2
379
  with
380
  | Unify (ck1',ck2') ->
381
    raise (Error (loc, Clock_clash (ck1',ck2')))
382
  | Mismatch (cr1,cr2) ->
383
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
384

    
385
(* Unifies all the clock variables in the clock type of a tuple 
386
   expression, so that the clock type only uses at most one clock variable *)
387
let unify_tuple_clock ref_ck_opt ck loc =
388
(*(match ref_ck_opt with
389
| None     -> Format.eprintf "unify_tuple_clock None %a@." Clocks.print_ck ck
390
  | Some ck' -> Format.eprintf "unify_tuple_clock (Some %a) %a@." Clocks.print_ck ck' Clocks.print_ck ck);*)
391
  let ck_var = ref ref_ck_opt in
392
  let rec aux ck =
393
    match (repr ck).cdesc with
394
    | Con _
395
    | Cvar ->
396
        begin
397
          match !ck_var with
398
          | None ->
399
              ck_var:=Some ck
400
          | Some v ->
401
              (* may fail *)
402
              try_unify ck v loc
403
        end
404
    | Ctuple cl ->
405
        List.iter aux cl
406
    | Carrow _ -> assert false (* should not occur *)
407
    | Ccarrying (_, ck1) ->
408
        aux ck1
409
    | _ -> ()
410
  in aux ck
411

    
412
(* Unifies all the clock variables in the clock type of an imported
413
   node, so that the clock type only uses at most one base clock variable,
414
   that is, the activation clock of the node *)
415
let unify_imported_clock ref_ck_opt ck loc =
416
  let ck_var = ref ref_ck_opt in
417
  let rec aux ck =
418
    match (repr ck).cdesc with
419
    | Cvar ->
420
        begin
421
          match !ck_var with
422
          | None ->
423
              ck_var:=Some ck
424
          | Some v ->
425
              (* cannot fail *)
426
              try_unify ck v loc
427
        end
428
    | Ctuple cl ->
429
        List.iter aux cl
430
    | Carrow (ck1,ck2) ->
431
        aux ck1; aux ck2
432
    | Ccarrying (_, ck1) ->
433
        aux ck1
434
    | Con (ck1, _, _) -> aux ck1
435
    | _ -> ()
436
  in
437
  aux ck
438

    
439
(* Computes the root clock of a tuple or a node clock,
440
   which is not the same as the base clock.
441
   Root clock will be used as the call clock 
442
   of a given node instance *)
443
let compute_root_clock ck =
444
  let root = Clocks.root ck in
445
  let branch = ref None in
446
  let rec aux ck =
447
    match (repr ck).cdesc with
448
    | Ctuple cl ->
449
        List.iter aux cl
450
    | Carrow (ck1,ck2) ->
451
        aux ck1; aux ck2
452
    | _ ->
453
        begin
454
          match !branch with
455
          | None ->
456
              branch := Some (Clocks.branch ck)
457
          | Some br ->
458
              (* cannot fail *)
459
              branch := Some (Clocks.common_prefix br (Clocks.branch ck))
460
        end
461
  in
462
  begin
463
    aux ck;
464
    Clocks.clock_of_root_branch root (Utils.desome !branch)
465
  end
466

    
467
(* Clocks a list of arguments of Lustre builtin operators:
468
   - type each expression, remove carriers of clocks as
469
     carriers may only denote variables, not arbitrary expr.
470
   - try to unify these clocks altogether
471
*)
472
let rec clock_standard_args env expr_list =
473
  let ck_list = List.map (fun e -> clock_uncarry (clock_expr env e)) expr_list in
474
  let ck_res = new_var true in
475
  List.iter2 (fun e ck -> try_unify ck ck_res e.expr_loc) expr_list ck_list;
476
  ck_res
477

    
478
(* emulates a subtyping relation between clocks c and (cr : c),
479
   used during node application only *)
480
and clock_subtyping_arg env ?(sub=true) real_arg formal_clock =
481
  let loc = real_arg.expr_loc in
482
  let real_clock = clock_expr env real_arg in
483
  try_sub_unify sub formal_clock real_clock loc
484

    
485
(* computes clocks for node application *)
486
and clock_appl env f args clock_reset loc =
487
 let args = expr_list_of_expr args in
488
  if Basic_library.is_homomorphic_fun f && List.exists is_tuple_expr args
489
  then
490
      let args = Utils.transpose_list (List.map expr_list_of_expr args) in
491
      Clocks.clock_of_clock_list (List.map (fun args -> clock_call env f args clock_reset loc) args)
492
  else
493
    clock_call env f args clock_reset loc
494

    
495
and clock_call env f args clock_reset loc =
496
  let cfun = clock_ident false env f loc in
497
  let cins, couts = split_arrow cfun in
498
  let cins = clock_list_of_clock cins in
499
  List.iter2 (clock_subtyping_arg env) args cins;
500
  unify_imported_clock (Some clock_reset) cfun loc;
501
  couts
502

    
503
and clock_ident nocarrier env id loc =
504
  clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc)
505

    
506
and clock_carrier env c loc ce =
507
  let expr_c = expr_of_ident c loc in
508
  let ck = clock_expr ~nocarrier:false env expr_c in
509
  let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in
510
  let ckb = new_var true in
511
  let ckcarry = new_ck (Ccarrying (cr, ckb)) ck.cscoped in
512
  try_unify ck ckcarry expr_c.expr_loc;
513
  unify_tuple_clock (Some ckb) ce expr_c.expr_loc;
514
  cr
515

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

    
608
let clock_of_vlist vars =
609
  let ckl = List.map (fun v -> v.var_clock) vars in
610
  clock_of_clock_list ckl
611

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

    
619
(* [clock_coreclock cck] returns the clock_expr corresponding to clock
620
    declaration [cck] *)
621
let clock_coreclock env cck id loc scoped =
622
  match cck.ck_dec_desc with
623
  | Ckdec_any -> new_var scoped
624
  | Ckdec_bool cl ->
625
      let temp_env = Env.add_value env id (new_var true) in
626
      (* We just want the id to be present in the environment *)
627
      let dummy_id_expr = expr_of_ident id loc in
628
      let when_expr =
629
        List.fold_left
630
          (fun expr (x,l) ->
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
          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 = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in
645
  let ck =
646
(* WTF ????
647
    if vdecl.var_dec_const
648
    then
649
      (try_generalize ck vdecl.var_loc; ck)
650
    else
651
 *)
652
      if Types.get_clock_base_type vdecl.var_type <> None
653
      then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped
654
      else ck in
655
  (if vdecl.var_dec_const
656
   then match vdecl.var_dec_value with
657
   | None   -> ()
658
   | Some v ->
659
     begin
660
       let ck_static = clock_expr env v in
661
       try_unify ck ck_static v.expr_loc
662
     end);
663
  try_unify ck vdecl.var_clock vdecl.var_loc;
664
  Env.add_value env vdecl.var_id ck
665

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

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

    
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) -> aux ck1; aux ck2
711
    | Ctuple cl -> List.iter aux cl
712
    | Con (ck',_,_) -> aux ck'
713
    | Clink ck' -> aux ck'
714
    | Ccarrying (_,ck') -> aux ck'
715
    | Cvar | Cunivar  ->
716
        match !pck with
717
        | None -> ()
718
        | Some (_,_) ->
719
            raise (Error (loc, (Invalid_imported_clock ck_node)))
720
  in
721
  aux ck_node
722

    
723
let clock_imported_node env loc nd =
724
  let new_env = clock_var_decl_list env false nd.nodei_inputs in
725
  ignore(clock_var_decl_list new_env false nd.nodei_outputs);
726
  let ck_ins = clock_of_vlist nd.nodei_inputs in
727
  let ck_outs = clock_of_vlist nd.nodei_outputs in
728
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
729
  unify_imported_clock None ck_node loc;
730
  check_imported_pclocks loc ck_node;
731
  try_generalize ck_node loc;
732
  nd.nodei_clock <- ck_node;
733
  Env.add_value env nd.nodei_id ck_node
734

    
735
let clock_top_const env cdecl=
736
  let ck = new_var false in
737
  try_generalize ck cdecl.const_loc;
738
  Env.add_value env cdecl.const_id ck
739

    
740
let clock_top_consts env clist =
741
  List.fold_left clock_top_const env clist
742
 
743
let rec clock_top_decl env decl =
744
  match decl.top_decl_desc with
745
  | Node nd ->
746
    clock_node env decl.top_decl_loc nd
747
  | ImportedNode nd ->
748
    clock_imported_node env decl.top_decl_loc nd
749
  | Const c ->
750
    clock_top_const env c
751
  | TypeDef _ -> List.fold_left clock_top_decl env (consts_of_enum_type decl)
752
  | Open _    -> env
753

    
754
let clock_prog env decls =
755
  List.fold_left clock_top_decl env decls
756

    
757
(* Once the Lustre program is fully clocked,
758
   we must get back to the original description of clocks,
759
   with constant parameters, instead of unifiable internal variables. *)
760

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

    
773
let uneval_node_generics vdecls =
774
  List.iter uneval_vdecl_generics vdecls
775

    
776
let uneval_top_generics decl =
777
  match decl.top_decl_desc with
778
  | Node nd ->
779
      (* A node could contain first-order carrier variable in local vars. This is not the case for types. *)
780
      uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)
781
  | ImportedNode nd ->
782
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
783
  | Const _
784
  | Open _
785
  | TypeDef _ -> ()
786

    
787
let uneval_prog_generics prog =
788
 List.iter uneval_top_generics prog
789

    
790
let check_env_compat header declared computed =
791
  uneval_prog_generics header;
792
  Env.iter declared (fun k decl_clock_k -> 
793
    let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
794
    try_semi_unify decl_clock_k computed_c Location.dummy_loc
795
  ) 
796
(* Local Variables: *)
797
(* compile-command:"make -C .." *)
798
(* End: *)