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 (_s, e) id =
27
  let pos_start =
28
    { e with Lexing.pos_cnum = e.Lexing.pos_cnum - (String.length id) }
29
  in
30
  pos_start, e
31

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

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

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

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

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

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

    
133

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

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

    
160

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
493
and clock_call env f args clock_reset loc =
494
  (* Format.eprintf "Clocking call %s@." f; *)
495
  let cfun = clock_ident false env f loc in
496
  let cins, couts = split_arrow cfun in
497
  let cins = clock_list_of_clock cins in
498
  List.iter2 (clock_subtyping_arg env) args cins;
499
  unify_imported_clock (Some clock_reset) cfun loc;
500
  couts
501

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

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

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

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

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

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

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

    
708

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

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

    
738

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

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

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

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

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

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

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

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

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