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 (Scope_carrier cr) ->
81
    raise (Error (loc, Carrier_extrusion (ck_node, cr)))
82
  | (Scope_clock ck) ->
83
    raise (Error (loc, Clock_extrusion (ck_node, ck)))
84

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

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

    
132

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

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

    
159

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
611
(** [clock_eq env eq] performs the clock-calculus for equation [eq] in
612
    environment [env] *)
613
let clock_eq env eq =
614
  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
615
  let ck_rhs = clock_expr env eq.eq_rhs in
616
  clock_subtyping_arg env expr_lhs ck_rhs
617

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

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

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

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

    
706

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

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

    
736

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

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

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

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

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

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

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

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

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