Project

General

Profile

Download (27.1 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

    
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 Lustre_types
23
open Corelang
24
open Clocks
25

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

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

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

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

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

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

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

    
134

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

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

    
161

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

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

    
222
let try_unify_carrier ck1 ck2 loc =
223
  try
224
    unify_carrier ck1 ck2
225
  with
226
  | Unify (ck1',ck2') ->
227
    raise (Error (loc, Clock_clash (ck1',ck2')))
228
  | Mismatch (cr1,cr2) ->
229
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
230

    
231
(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify
232
    (ck1,ck2)] if the clocks are not unifiable.*)
233
let rec unify ck1 ck2 =
234
  let ck1 = repr ck1 in
235
  let ck2 = repr ck2 in
236
  if ck1==ck2 then
237
    ()
238
  else
239
    match ck1.cdesc,ck2.cdesc with
240
    | Cvar, Cvar ->
241
      if ck1.cid < ck2.cid then
242
        begin
243
          ck2.cdesc <- Clink (simplify ck1);
244
          update_scope ck2.cscoped ck1
245
        end
246
      else
247
        begin
248
          ck1.cdesc <- Clink (simplify ck2);
249
          update_scope ck1.cscoped ck2
250
        end
251
    | (Cvar, _) when (not (occurs ck1 ck2)) ->
252
      update_scope ck1.cscoped ck2;
253
      ck1.cdesc <- Clink (simplify ck2)
254
    | (_, Cvar) when (not (occurs ck2 ck1)) ->
255
      update_scope ck2.cscoped ck1;
256
      ck2.cdesc <- Clink (simplify ck1)
257
    | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
258
      unify_carrier cr1 cr2;
259
      unify ck1' ck2'
260
    | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->
261
      raise (Unify (ck1,ck2))
262
    | Carrow (c1,c2), Carrow (c1',c2') ->
263
      unify c1 c1'; unify c2 c2'
264
    | Ctuple ckl1, Ctuple ckl2 ->
265
      if (List.length ckl1) <> (List.length ckl2) then
266
        raise (Unify (ck1,ck2));
267
      List.iter2 unify ckl1 ckl2
268
    | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
269
      unify_carrier c1 c2;
270
      unify ck' ck''
271
    | Cunivar, _ | _, Cunivar -> ()
272
    | _,_ -> raise (Unify (ck1,ck2))
273

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

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

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

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

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

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

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

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

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

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

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

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

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

    
494
and clock_call env f args clock_reset loc =
495
  (* Format.eprintf "Clocking call %s@." f; *)
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 _ ->
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, _) ->
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, _) ->
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
  let eqs, _ = get_node_eqs nd in (* TODO XXX: perform the clocking on auts.
685
					For the moment, it is ignored *)
686
  List.iter (clock_eq new_env) eqs;
687
  let ck_ins = clock_of_vlist nd.node_inputs in
688
  let ck_outs = clock_of_vlist nd.node_outputs in
689
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
690
  unify_imported_clock None ck_node loc;
691
  Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
692
  (* Local variables may contain first-order carrier variables that should be generalized.
693
     That's not the case for types. *)
694
  try_generalize ck_node loc;
695
  (*
696
    List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs;
697
    List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;*)
698
  (*List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;*)
699
  (* TODO : Xavier pourquoi ai je cette erreur ? *)
700
  (*  if (is_main && is_polymorphic ck_node) then
701
      raise (Error (loc,(Cannot_be_polymorphic ck_node)));
702
  *)
703
  Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
704
  nd.node_clock <- ck_node;
705
  Env.add_value env nd.node_id ck_node
706

    
707

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

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

    
737

    
738
let new_env = clock_var_decl_list
739
              
740
let clock_top_const env cdecl=
741
  let ck = new_var false in
742
  try_generalize ck cdecl.const_loc;
743
  Env.add_value env cdecl.const_id ck
744

    
745
let clock_top_consts env clist =
746
  List.fold_left clock_top_const env clist
747
 
748
let rec clock_top_decl env decl =
749
  match decl.top_decl_desc with
750
  | Node nd ->
751
    clock_node env decl.top_decl_loc nd
752
  | ImportedNode nd ->
753
    clock_imported_node env decl.top_decl_loc nd
754
  | Const c ->
755
    clock_top_const env c
756
  | TypeDef _ -> List.fold_left clock_top_decl env (consts_of_enum_type decl)
757
  | Include _ | Open _    -> env
758

    
759
let clock_prog env decls =
760
  List.fold_left clock_top_decl env decls
761

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

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

    
778
let uneval_node_generics vdecls =
779
  List.iter uneval_vdecl_generics vdecls
780

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

    
792
let uneval_prog_generics prog =
793
 List.iter uneval_top_generics prog
794

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