Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / clock_calculus.ml @ b38ffff3

History | View | Annotate | Download (30.1 KB)

1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - LIFL             *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *) 
10
(*  This file was originally from the Prelude compiler              *)
11
(*                                                                  *) 
12
(********************************************************************)
13

    
14

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

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

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

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

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

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

    
86
let try_generalize ck_node loc =
87
  try 
88
    generalize ck_node
89
  with (Scope_carrier cr) ->
90
    raise (Error (loc, Carrier_extrusion (ck_node, cr)))
91
  | (Scope_clock ck) ->
92
    raise (Error (loc, Clock_extrusion (ck_node, ck)))
93

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

    
110
(** Downgrade polymorphic clock variables to monomorphic clock variables *)
111
(* inst_ck_vars ensures that a polymorphic variable is instanciated with
112
   the same monomorphic variable if it occurs several times in the same
113
   type. inst_cr_vars is the same for carriers. *)
114
let rec instantiate inst_ck_vars inst_cr_vars ck =
115
  match ck.cdesc with
116
  | Carrow (ck1,ck2) ->
117
      {ck with cdesc =
118
       Carrow ((instantiate inst_ck_vars inst_cr_vars ck1),
119
               (instantiate inst_ck_vars inst_cr_vars ck2))}
120
  | Ctuple cklist ->
121
      {ck with cdesc = Ctuple 
122
         (List.map (instantiate inst_ck_vars inst_cr_vars) cklist)}
123
  | Con (ck',c,l) ->
124
      let c' = instantiate_carrier c inst_cr_vars in
125
      {ck with cdesc = Con ((instantiate inst_ck_vars inst_cr_vars ck'),c',l)}
126
  | Cvar _ | Pck_const (_,_) -> ck
127
  | Pck_up (ck',k) ->
128
      {ck with cdesc = Pck_up ((instantiate inst_ck_vars inst_cr_vars ck'),k)}
129
  | Pck_down (ck',k) ->
130
      {ck with cdesc = Pck_down ((instantiate inst_ck_vars inst_cr_vars ck'),k)}
131
  | Pck_phase (ck',q) ->
132
      {ck with cdesc = Pck_phase ((instantiate inst_ck_vars inst_cr_vars ck'),q)}
133
  | Clink ck' ->
134
      {ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')}
135
  | Ccarrying (cr,ck') ->
136
      let cr' = instantiate_carrier cr inst_cr_vars in
137
        {ck with cdesc =
138
         Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')}
139
  | Cunivar cset ->
140
      try
141
        List.assoc ck.cid !inst_ck_vars
142
      with Not_found ->
143
        let var = new_ck (Cvar cset) true in
144
	inst_ck_vars := (ck.cid, var)::!inst_ck_vars;
145
	var
146

    
147
(** [subsume pck1 cset1] subsumes clock [pck1] by clock subset
148
    [cset1]. The clock constraint is actually recursively transfered to
149
    the clock variable appearing in [pck1] *)
150
let subsume pck1 cset1 =
151
  let rec aux pck cset =
152
    match cset with
153
    | CSet_all ->
154
        ()
155
    | CSet_pck (k,(a,b)) ->
156
        match pck.cdesc with
157
        | Cvar cset' ->
158
            pck.cdesc <- Cvar (intersect cset' cset)
159
        | Pck_up (pck',k') ->
160
            let rat = if a=0 then (0,1) else (a,b*k') in
161
            aux pck' (CSet_pck ((k*k'),rat))
162
        | Pck_down (pck',k') ->
163
            let k''=k/(gcd k k') in
164
            aux pck' (CSet_pck (k'',(a*k',b)))
165
        | Pck_phase (pck',(a',b')) ->
166
            let (a'',b'')= max_rat (sum_rat (a,b) (-a',b')) (0,1) in
167
            aux pck' (CSet_pck (k, (a'',b'')))
168
        | Pck_const (n,(a',b')) ->
169
            if n mod k <> 0 || (max_rat (a,b) (a',b')) <> (a',b') then
170
              raise (Subsume (pck1, cset1))
171
        | Clink pck' ->
172
            aux pck' cset
173
        | Cunivar _ -> ()
174
        | Ccarrying (_,ck') ->
175
            aux ck' cset
176
        | _ -> raise (Subsume (pck1, cset1))
177
  in
178
  aux pck1 cset1
179

    
180
let rec update_scope_carrier scoped cr =
181
  if (not scoped) then
182
    begin
183
      cr.carrier_scoped <- scoped;
184
      match cr.carrier_desc with
185
	| Carry_const _ | Carry_name | Carry_var -> ()
186
      | Carry_link cr' -> update_scope_carrier scoped cr'
187
    end
188

    
189
let rec update_scope scoped ck =
190
  if (not scoped) then
191
    begin
192
      ck.cscoped <- scoped;
193
      match ck.cdesc with
194
      | Carrow (ck1,ck2) ->
195
          update_scope scoped ck1; update_scope scoped ck2
196
      | Ctuple clist ->
197
          List.iter (update_scope scoped) clist
198
      | Con (ck',cr,_) -> update_scope scoped ck'(*; update_scope_carrier scoped cr*)
199
      | Cvar cset ->
200
          ck.cdesc <- Cvar cset
201
      | Pck_up (ck',_) -> update_scope scoped ck'
202
      | Pck_down (ck',_) -> update_scope scoped ck'
203
      | Pck_phase (ck',_) -> update_scope scoped ck'
204
      | Pck_const (_,_) | Cunivar _ -> ()
205
      | Clink ck' ->
206
          update_scope scoped ck'
207
      | Ccarrying (cr,ck') ->
208
          update_scope_carrier scoped cr; update_scope scoped ck'
209
    end
210

    
211
(* Unifies two static pclocks. *)
212
let unify_static_pck ck1 ck2 =
213
  if (period ck1 <> period ck2) || (phase ck1 <> phase ck2) then
214
    raise (Unify (ck1,ck2))
215

    
216
(* Unifies two clock carriers *)
217
let unify_carrier cr1 cr2 =
218
  let cr1 = carrier_repr cr1 in
219
  let cr2 = carrier_repr cr2 in
220
  if cr1==cr2 then ()
221
  else
222
    match cr1.carrier_desc, cr2.carrier_desc with
223
    | Carry_const id1, Carry_const id2 ->
224
      if id1 <> id2 then raise (Mismatch (cr1, cr2))
225
    | Carry_const _, Carry_name ->
226
      begin
227
	cr2.carrier_desc <- Carry_link cr1;
228
	update_scope_carrier cr2.carrier_scoped cr1
229
      end
230
    | Carry_name, Carry_const _ ->
231
      begin
232
        cr1.carrier_desc <- Carry_link cr2;
233
        update_scope_carrier cr1.carrier_scoped cr2
234
      end
235
    | Carry_name, Carry_name ->
236
      if cr1.carrier_id < cr2.carrier_id then
237
        begin
238
          cr2.carrier_desc <- Carry_link cr1;
239
          update_scope_carrier cr2.carrier_scoped cr1
240
        end
241
      else
242
        begin
243
          cr1.carrier_desc <- Carry_link cr2;
244
          update_scope_carrier cr1.carrier_scoped cr2
245
        end
246
    | _,_ -> assert false
247

    
248
(* Semi-unifies two clock carriers *)
249
let semi_unify_carrier cr1 cr2 =
250
  let cr1 = carrier_repr cr1 in
251
  let cr2 = carrier_repr cr2 in
252
  if cr1==cr2 then ()
253
  else
254
    match cr1.carrier_desc, cr2.carrier_desc with
255
    | Carry_const id1, Carry_const id2 ->
256
      if id1 <> id2 then raise (Mismatch (cr1, cr2))
257
    | Carry_const _, Carry_name ->
258
      begin
259
	cr2.carrier_desc <- Carry_link cr1;
260
	update_scope_carrier cr2.carrier_scoped cr1
261
      end
262
    | Carry_name, Carry_const _ -> raise (Mismatch (cr1, cr2))
263
    | Carry_name, Carry_name ->
264
      if cr1.carrier_id < cr2.carrier_id then
265
        begin
266
          cr2.carrier_desc <- Carry_link cr1;
267
          update_scope_carrier cr2.carrier_scoped cr1
268
        end
269
      else
270
        begin
271
          cr1.carrier_desc <- Carry_link cr2;
272
          update_scope_carrier cr1.carrier_scoped cr2
273
        end
274
    | _,_ -> assert false
275

    
276
(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify
277
    (ck1,ck2)] if the clocks are not unifiable.*)
278
let rec unify ck1 ck2 =
279
  let ck1 = repr ck1 in
280
  let ck2 = repr ck2 in
281
  if ck1==ck2 then
282
    ()
283
  else
284
    let left_const = is_concrete_pck ck1 in
285
    let right_const = is_concrete_pck ck2 in
286
    if left_const && right_const then
287
      unify_static_pck ck1 ck2
288
    else
289
      match ck1.cdesc,ck2.cdesc with
290
      | Cvar cset1,Cvar cset2->
291
          if ck1.cid < ck2.cid then
292
            begin
293
              ck2.cdesc <- Clink (simplify ck1);
294
              update_scope ck2.cscoped ck1;
295
              subsume ck1 cset2
296
            end
297
          else
298
            begin
299
              ck1.cdesc <- Clink (simplify ck2);
300
              update_scope ck1.cscoped ck2;
301
              subsume ck2 cset1
302
            end
303
      | Cvar cset, Pck_up (_,_) | Cvar cset, Pck_down (_,_)
304
      | Cvar cset, Pck_phase (_,_) | Cvar cset, Pck_const (_,_) ->
305
          if (occurs ck1 ck2) then
306
            begin
307
              if (simplify ck2 = ck1) then
308
                ck2.cdesc <- Clink (simplify ck1)
309
              else
310
                raise (Unify (ck1,ck2));
311
              end
312
          else
313
            begin
314
              ck1.cdesc <- Clink (simplify ck2);
315
              subsume ck2 cset
316
            end
317
      | Pck_up (_,_), Cvar cset | Pck_down (_,_), Cvar cset
318
      | Pck_phase (_,_), Cvar cset | Pck_const (_,_), Cvar cset ->
319
            if (occurs ck2 ck1) then
320
              begin
321
                if ((simplify ck1) = ck2) then
322
                  ck1.cdesc <- Clink (simplify ck2)
323
                else
324
                  raise (Unify (ck1,ck2));
325
              end
326
            else
327
              begin
328
                ck2.cdesc <- Clink (simplify ck1);
329
                subsume ck1 cset
330
              end
331
      | (Cvar cset,_) when (not (occurs ck1 ck2)) ->
332
          subsume ck2 cset;
333
          update_scope ck1.cscoped ck2;
334
          ck1.cdesc <- Clink (simplify ck2)
335
      | (_, (Cvar cset)) when (not (occurs ck2 ck1)) ->
336
          subsume ck1 cset;
337
          update_scope ck2.cscoped ck1;
338
          ck2.cdesc <- Clink (simplify ck1)
339
      | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
340
          unify_carrier cr1 cr2;
341
          unify ck1' ck2'
342
      | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->
343
          raise (Unify (ck1,ck2))
344
      | Carrow (c1,c2), Carrow (c1',c2') ->
345
          unify c1 c1'; unify c2 c2'
346
      | Ctuple ckl1, Ctuple ckl2 ->
347
          if (List.length ckl1) <> (List.length ckl2) then
348
            raise (Unify (ck1,ck2));
349
          List.iter2 unify ckl1 ckl2
350
      | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
351
          unify_carrier c1 c2;
352
          unify ck' ck''
353
      | Pck_const (i,r), Pck_const (i',r') ->
354
          if i<>i' || r <> r' then
355
            raise (Unify (ck1,ck2))
356
      | (_, Pck_up (pck2',k)) when (not right_const) ->
357
          let ck1' = simplify (new_ck (Pck_down (ck1,k)) true) in
358
          unify ck1' pck2'
359
      | (_,Pck_down (pck2',k)) when (not right_const) ->
360
          subsume ck1 (CSet_pck (k,(0,1)));
361
          let ck1' = simplify (new_ck (Pck_up (ck1,k)) true) in
362
          unify ck1' pck2'
363
      | (_,Pck_phase (pck2',(a,b))) when (not right_const) ->
364
          subsume ck1 (CSet_pck (b,(a,b)));
365
          let ck1' = simplify (new_ck (Pck_phase (ck1,(-a,b))) true) in
366
          unify ck1' pck2'
367
      | Pck_up (pck1',k),_ ->
368
          let ck2' = simplify (new_ck (Pck_down (ck2,k)) true) in
369
          unify pck1' ck2'
370
      | Pck_down (pck1',k),_ ->
371
          subsume ck2 (CSet_pck (k,(0,1)));
372
          let ck2' = simplify (new_ck (Pck_up (ck2,k)) true) in
373
          unify pck1' ck2'
374
      | Pck_phase (pck1',(a,b)),_ ->
375
          subsume ck2 (CSet_pck (b,(a,b)));
376
          let ck2' = simplify (new_ck (Pck_phase (ck2,(-a,b))) true) in
377
          unify pck1' ck2'
378
      | Cunivar _, _ | _, Cunivar _ -> ()
379
      | _,_ -> raise (Unify (ck1,ck2))
380

    
381
(** [unify ck1 ck2] semi-unifies clocks [ck1] and [ck2]. Raises [Unify
382
    (ck1,ck2)] if the clocks are not semi-unifiable.*)
383
let rec semi_unify ck1 ck2 =
384
  let ck1 = repr ck1 in
385
  let ck2 = repr ck2 in
386
  if ck1==ck2 then
387
    ()
388
  else
389
      match ck1.cdesc,ck2.cdesc with
390
      | Cvar cset1,Cvar cset2->
391
          if ck1.cid < ck2.cid then
392
            begin
393
              ck2.cdesc <- Clink (simplify ck1);
394
              update_scope ck2.cscoped ck1
395
            end
396
          else
397
            begin
398
              ck1.cdesc <- Clink (simplify ck2);
399
              update_scope ck1.cscoped ck2
400
            end
401
      | (Cvar cset,_) -> raise (Unify (ck1,ck2))
402
      | (_, (Cvar cset)) when (not (occurs ck2 ck1)) ->
403
          update_scope ck2.cscoped ck1;
404
          ck2.cdesc <- Clink (simplify ck1)
405
      | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
406
          semi_unify_carrier cr1 cr2;
407
          semi_unify ck1' ck2'
408
      | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->
409
          raise (Unify (ck1,ck2))
410
      | Carrow (c1,c2), Carrow (c1',c2') ->
411
	begin
412
          semi_unify c1 c1';
413
	  semi_unify c2 c2'
414
	end
415
      | Ctuple ckl1, Ctuple ckl2 ->
416
          if (List.length ckl1) <> (List.length ckl2) then
417
            raise (Unify (ck1,ck2));
418
          List.iter2 semi_unify ckl1 ckl2
419
      | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
420
          semi_unify_carrier c1 c2;
421
          semi_unify ck' ck''
422
      | Cunivar _, _ | _, Cunivar _ -> ()
423
      | _,_ -> raise (Unify (ck1,ck2))
424

    
425
(* Returns the value corresponding to a pclock (integer) factor
426
   expression. Expects a constant expression (checked by typing). *)
427
let int_factor_of_expr e =
428
  match e.expr_desc with 
429
  | Expr_const
430
      (Const_int i) -> i
431
  | _ -> failwith "Internal error: int_factor_of_expr"
432

    
433
(* Unifies all the clock variables in the clock type of a tuple 
434
   expression, so that the clock type only uses at most one clock variable *)
435
let unify_tuple_clock ref_ck_opt ck =
436
  let ck_var = ref ref_ck_opt in
437
  let rec aux ck =
438
    match (repr ck).cdesc with
439
    | Con _
440
    | Cvar _ ->
441
        begin
442
          match !ck_var with
443
          | None ->
444
              ck_var:=Some ck
445
          | Some v ->
446
              (* may fail *)
447
              unify v ck
448
        end
449
    | Ctuple cl ->
450
        List.iter aux cl
451
    | Carrow _ -> assert false (* should not occur *)
452
    | Ccarrying (_, ck1) ->
453
        aux ck1
454
    | _ -> ()
455
  in
456
  aux ck
457

    
458
(* Unifies all the clock variables in the clock type of an imported
459
   node, so that the clock type only uses at most one base clock variable,
460
   that is, the activation clock of the node *)
461
let unify_imported_clock ref_ck_opt ck =
462
  let ck_var = ref ref_ck_opt in
463
  let rec aux ck =
464
    match (repr ck).cdesc with
465
    | Cvar _ ->
466
        begin
467
          match !ck_var with
468
          | None ->
469
              ck_var:=Some ck
470
          | Some v ->
471
              (* cannot fail *)
472
              unify v ck
473
        end
474
    | Ctuple cl ->
475
        List.iter aux cl
476
    | Carrow (ck1,ck2) ->
477
        aux ck1; aux ck2
478
    | Ccarrying (_, ck1) ->
479
        aux ck1
480
    | Con (ck1, _, _) -> aux ck1
481
    | _ -> ()
482
  in
483
  aux ck
484

    
485
(** [clock_uncarry ck] drops the possible carrier name from clock [ck] *)
486
let clock_uncarry ck =
487
  let ck = repr ck in
488
  match ck.cdesc with
489
  | Ccarrying (_, ck') -> ck'
490
  | _                  -> ck
491

    
492
let try_unify ck1 ck2 loc =
493
  try
494
    unify ck1 ck2
495
  with
496
  | Unify (ck1',ck2') ->
497
    raise (Error (loc, Clock_clash (ck1',ck2')))
498
  | Subsume (ck,cset) ->
499
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
500
  | Mismatch (cr1,cr2) ->
501
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
502

    
503
let try_semi_unify ck1 ck2 loc =
504
  try
505
    semi_unify ck1 ck2
506
  with
507
  | Unify (ck1',ck2') ->
508
    raise (Error (loc, Clock_clash (ck1',ck2')))
509
  | Subsume (ck,cset) ->
510
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
511
  | Mismatch (cr1,cr2) ->
512
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
513

    
514
(* ck1 is a subtype of ck2 *)
515
let rec sub_unify sub ck1 ck2 =
516
  match (repr ck1).cdesc, (repr ck2).cdesc with
517
  | Ctuple cl1         , Ctuple cl2         ->
518
    if List.length cl1 <> List.length cl2
519
    then raise (Unify (ck1, ck2))
520
    else List.iter2 (sub_unify sub) cl1 cl2
521
  | Ctuple [c1]        , _                  -> sub_unify sub c1 ck2
522
  | _                  , Ctuple [c2]        -> sub_unify sub ck1 c2
523
  | Con (c1, cr1, t1)  , Con (c2, cr2, t2) when t1=t2 ->
524
    begin
525
      unify_carrier cr1 cr2;
526
      sub_unify sub c1 c2
527
    end
528
  | Ccarrying (cr1, c1), Ccarrying (cr2, c2)->
529
    begin
530
      unify_carrier cr1 cr2;
531
      sub_unify sub c1 c2
532
    end
533
  | Ccarrying (_, c1)  , _         when sub -> sub_unify sub c1 ck2
534
  | _                                       -> unify ck1 ck2
535

    
536
let try_sub_unify sub ck1 ck2 loc =
537
  try
538
    sub_unify sub ck1 ck2
539
  with
540
  | Unify (ck1',ck2') ->
541
    raise (Error (loc, Clock_clash (ck1',ck2')))
542
  | Subsume (ck,cset) ->
543
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
544
  | Mismatch (cr1,cr2) ->
545
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
546

    
547
(* Clocks a list of arguments of Lustre builtin operators:
548
   - type each expression, remove carriers of clocks as
549
     carriers may only denote variables, not arbitrary expr.
550
   - try to unify these clocks altogether
551
*)
552
let rec clock_standard_args env expr_list =
553
  let ck_list = List.map (fun e -> clock_uncarry (clock_expr env e)) expr_list in
554
  let ck_res = new_var true in
555
  List.iter2 (fun e ck -> try_unify ck ck_res e.expr_loc) expr_list ck_list;
556
  ck_res
557

    
558
(* emulates a subtyping relation between clocks c and (cr : c),
559
   used during node application only *)
560
and clock_subtyping_arg env ?(sub=true) real_arg formal_clock =
561
  let loc = real_arg.expr_loc in
562
  let real_clock = clock_expr env real_arg in
563
  try_sub_unify sub real_clock formal_clock loc
564

    
565
(* computes clocks for node application *)
566
and clock_appl env f args clock_reset loc =
567
 let args = expr_list_of_expr args in
568
  if Basic_library.is_internal_fun f && List.exists is_tuple_expr args
569
  then
570
      let args = Utils.transpose_list (List.map expr_list_of_expr args) in
571
      Clocks.clock_of_clock_list (List.map (fun args -> clock_call env f args clock_reset loc) args)
572
  else
573
    clock_call env f args clock_reset loc
574

    
575
and clock_call env f args clock_reset loc =
576
  let cfun = clock_ident false env f loc in
577
  let cins, couts = split_arrow cfun in
578
  let cins = clock_list_of_clock cins in
579
  List.iter2 (clock_subtyping_arg env) args cins;
580
  unify_imported_clock (Some clock_reset) cfun;
581
  couts
582

    
583
and clock_ident nocarrier env id loc =
584
  clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc)
585

    
586
and clock_carrier env c loc ce =
587
  let expr_c = expr_of_ident c loc in
588
  let ck = clock_expr ~nocarrier:false env expr_c in
589
  let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in
590
  let ckcarry = new_ck (Ccarrying (cr,ce)) ck.cscoped in
591
  try_unify ck ckcarry expr_c.expr_loc;
592
  cr
593

    
594
(** [clock_expr env expr] performs the clock calculus for expression [expr] in
595
    environment [env] *)
596
and clock_expr ?(nocarrier=true) env expr =
597
  let resulting_ck = 
598
    match expr.expr_desc with
599
      | Expr_const cst ->
600
      let ck = new_var true in
601
      expr.expr_clock <- ck;
602
      ck
603
  | Expr_ident v ->
604
      let ckv =
605
        try
606
          Env.lookup_value env v
607
        with Not_found -> 
608
	  failwith ("Internal error, variable \""^v^"\" not found")
609
      in
610
      let ck = instantiate (ref []) (ref []) ckv in
611
      expr.expr_clock <- ck;
612
      ck
613
  | Expr_array elist ->
614
    let ck = clock_standard_args env elist in
615
    expr.expr_clock <- ck;
616
    ck
617
  | Expr_access (e1, d) ->
618
    (* dimension, being a static value, doesn't need to be clocked *)
619
    let ck = clock_standard_args env [e1] in
620
    expr.expr_clock <- ck;
621
    ck
622
  | Expr_power (e1, d) ->
623
    (* dimension, being a static value, doesn't need to be clocked *)
624
    let ck = clock_standard_args env [e1] in
625
    expr.expr_clock <- ck;
626
    ck
627
  | Expr_tuple elist ->
628
    let ck = new_ck (Ctuple (List.map (clock_expr env) elist)) true in
629
    expr.expr_clock <- ck;
630
    ck
631
  | Expr_ite (c, t, e) ->
632
    let ck_c = clock_standard_args env [c] in
633
    let ck = clock_standard_args env [t; e] in
634
    (* Here, the branches may exhibit a tuple clock, not the condition *)
635
    unify_tuple_clock (Some ck_c) ck;
636
    expr.expr_clock <- ck;
637
    ck
638
  | Expr_appl (id, args, r) ->
639
    (try
640
(* for a modular compilation scheme, all inputs/outputs must share the same clock !
641
   this is also the reset clock !
642
*)
643
    let cr =
644
      match r with
645
      | None        -> new_var true
646
      | Some (x, _) -> let loc_r = loc_of_cond expr.expr_loc x in
647
		       let expr_r = expr_of_ident x loc_r in
648
		       clock_expr env expr_r in
649
    let couts = clock_appl env id args cr expr.expr_loc in
650
    expr.expr_clock <- couts;
651
    couts
652
    with exn -> (
653
      Format.eprintf "Current expr: %a@." Printers.pp_expr expr; 
654
      raise exn
655
    ))
656
  | Expr_fby (e1,e2)
657
  | Expr_arrow (e1,e2) ->
658
    let ck = clock_standard_args env [e1; e2] in
659
    unify_tuple_clock None ck;
660
    expr.expr_clock <- ck;
661
    ck
662
  | Expr_pre e -> (* todo : deal with phases as in tail ? *)
663
      let ck = clock_standard_args env [e] in
664
      expr.expr_clock <- ck;
665
      ck
666
  | Expr_when (e,c,l) ->
667
      let ce = clock_standard_args env [e] in
668
      let c_loc = loc_of_cond expr.expr_loc c in
669
      let cr = clock_carrier env c c_loc ce in
670
      let ck = new_ck (Con (ce,cr,l)) true in
671
      let cr' = new_carrier (Carry_const c) ck.cscoped in
672
      let ck' = new_ck (Con (ce,cr',l)) true in
673
      expr.expr_clock <- ck';
674
      ck
675
  | Expr_merge (c,hl) ->
676
      let cvar = new_var true in
677
      let cr = clock_carrier env c expr.expr_loc cvar in
678
      List.iter (fun (t, h) -> clock_subtyping_arg env h (new_ck (Con (cvar,cr,t)) true)) hl;
679
      expr.expr_clock <- cvar;
680
      cvar
681
  in
682
  Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck);
683
  resulting_ck
684

    
685
let clock_of_vlist vars =
686
  let ckl = List.map (fun v -> v.var_clock) vars in
687
  clock_of_clock_list ckl
688

    
689
(** [clock_eq env eq] performs the clock-calculus for equation [eq] in
690
    environment [env] *)
691
let clock_eq env eq =
692
  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
693
  let ck_rhs = clock_expr env eq.eq_rhs in
694
  clock_subtyping_arg env expr_lhs ck_rhs
695

    
696

    
697
(* [clock_coreclock cck] returns the clock_expr corresponding to clock
698
    declaration [cck] *)
699
let clock_coreclock env cck id loc scoped =
700
  match cck.ck_dec_desc with
701
  | Ckdec_any -> new_var scoped
702
  | Ckdec_pclock (n,(a,b)) ->
703
      let ck = new_ck (Pck_const (n,(a,b))) scoped in
704
      if n mod b <> 0 then raise (Error (loc,Invalid_const ck));
705
      ck
706
  | Ckdec_bool cl ->
707
      let temp_env = Env.add_value env id (new_var true) in
708
      (* We just want the id to be present in the environment *)
709
      let dummy_id_expr = expr_of_ident id loc in
710
      let when_expr =
711
        List.fold_left
712
          (fun expr (x,l) ->
713
                {expr_tag = new_tag ();
714
                 expr_desc = Expr_when (expr,x,l);
715
                 expr_type = Types.new_var ();
716
                 expr_clock = new_var scoped;
717
                 expr_delay = Delay.new_var ();
718
                 expr_loc = loc;
719
		 expr_annot = None})
720
          dummy_id_expr cl
721
      in
722
      clock_expr temp_env when_expr
723

    
724
(* Clocks a variable declaration *)
725
let clock_var_decl scoped env vdecl =
726
  let ck = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in
727
  let ck =
728
(* WTF ????
729
    if vdecl.var_dec_const
730
    then
731
      (try_generalize ck vdecl.var_loc; ck)
732
    else
733
 *)
734
      if Types.get_clock_base_type vdecl.var_type <> None
735
      then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped
736
      else ck in
737
  vdecl.var_clock <- ck;
738
  Env.add_value env vdecl.var_id ck
739

    
740
(* Clocks a variable declaration list *)
741
let clock_var_decl_list env scoped l =
742
  List.fold_left (clock_var_decl scoped) env l
743

    
744
(** [clock_node env nd] performs the clock-calculus for node [nd] in
745
    environment [env].
746
    Generalization of clocks wrt scopes follows this rule:
747
    - generalize inputs (unscoped).
748
    - generalize outputs. As they are scoped, only clocks coming from inputs
749
      are allowed to be generalized.
750
    - generalize locals. As outputs don't depend on them (checked the step before),
751
      they can be generalized. 
752
 *)
753
let clock_node env loc nd =
754
  (* let is_main = nd.node_id = !Options.main_node in *)
755
  let new_env = clock_var_decl_list env false nd.node_inputs in
756
  let new_env = clock_var_decl_list new_env true nd.node_outputs in
757
  let new_env = clock_var_decl_list new_env true nd.node_locals in
758
  List.iter (clock_eq new_env) nd.node_eqs;
759
  let ck_ins = clock_of_vlist nd.node_inputs in
760
  let ck_outs = clock_of_vlist nd.node_outputs in
761
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
762
  unify_imported_clock None ck_node;
763
  Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
764
  (* Local variables may contain first-order carrier variables that should be generalized.
765
     That's not the case for types. *)
766
  try_generalize ck_node loc;
767
(*
768
  List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs;
769
  List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;*)
770
  (*List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;*)
771
  (* TODO : Xavier pourquoi ai je cette erreur ? *)
772
(*  if (is_main && is_polymorphic ck_node) then
773
    raise (Error (loc,(Cannot_be_polymorphic ck_node)));
774
*)
775
  Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
776
  nd.node_clock <- ck_node;
777
  Env.add_value env nd.node_id ck_node
778

    
779

    
780
let check_imported_pclocks loc ck_node =
781
  let pck = ref None in
782
  let rec aux ck =
783
    match ck.cdesc with
784
    | Carrow (ck1,ck2) -> aux ck1; aux ck2
785
    | Ctuple cl -> List.iter aux cl
786
    | Con (ck',_,_) -> aux ck'
787
    | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) -> 
788
        raise (Error (loc, (Invalid_imported_clock ck_node)))
789
    | Pck_const (n,p) ->
790
        begin
791
          match !pck with
792
          | None -> pck := Some (n,p)
793
          | Some (n',p') ->
794
              if (n,p) <> (n',p') then
795
                raise (Error (loc, (Invalid_imported_clock ck_node)))
796
        end
797
    | Clink ck' -> aux ck'
798
    | Ccarrying (_,ck') -> aux ck'
799
    | Cvar _ | Cunivar _ ->
800
        match !pck with
801
        | None -> ()
802
        | Some (_,_) ->
803
            raise (Error (loc, (Invalid_imported_clock ck_node)))
804
  in
805
  aux ck_node
806

    
807
let clock_imported_node env loc nd =
808
  let new_env = clock_var_decl_list env false nd.nodei_inputs in
809
  ignore(clock_var_decl_list new_env false nd.nodei_outputs);
810
  let ck_ins = clock_of_vlist nd.nodei_inputs in
811
  let ck_outs = clock_of_vlist nd.nodei_outputs in
812
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
813
  unify_imported_clock None ck_node;
814
  check_imported_pclocks loc ck_node;
815
  try_generalize ck_node loc;
816
  nd.nodei_clock <- ck_node;
817
  Env.add_value env nd.nodei_id ck_node
818

    
819
let clock_top_consts env clist =
820
  List.fold_left (fun env cdecl ->
821
    let ck = new_var false in
822
    try_generalize ck cdecl.const_loc;
823
    Env.add_value env cdecl.const_id ck) env clist
824

    
825
let clock_top_decl env decl =
826
  match decl.top_decl_desc with
827
  | Node nd ->
828
    clock_node env decl.top_decl_loc nd
829
  | ImportedNode nd ->
830
    clock_imported_node env decl.top_decl_loc nd
831
  | Consts clist ->
832
    clock_top_consts env clist
833
  | Open _ ->
834
    env
835

    
836
let clock_prog env decls =
837
  List.fold_left (fun e decl -> clock_top_decl e decl) env decls
838

    
839
(* Once the Lustre program is fully clocked,
840
   we must get back to the original description of clocks,
841
   with constant parameters, instead of unifiable internal variables. *)
842

    
843
(* The following functions aims at 'unevaluating' carriers occuring in clock expressions,
844
   i.e. replacing unifiable second_order variables with the original carrier names.
845
   Once restored in this formulation, clocks may be meaningfully printed.
846
*)
847
let uneval_vdecl_generics vdecl =
848
 (*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@." Printers.pp_node_var vdecl;*)
849
 if Types.get_clock_base_type vdecl.var_type <> None
850
 then
851
   match get_carrier_name vdecl.var_clock with
852
   | None    -> (Format.eprintf "internal error: %a@." print_ck vdecl.var_clock; assert false)
853
   | Some cr -> Clocks.uneval vdecl.var_id cr
854

    
855
let uneval_node_generics vdecls =
856
  List.iter uneval_vdecl_generics vdecls
857

    
858
let uneval_top_generics decl =
859
  match decl.top_decl_desc with
860
  | Node nd ->
861
      (* A node could contain first-order carrier variable in local vars. This is not the case for types. *)
862
      uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)
863
  | ImportedNode nd ->
864
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
865
  | Consts clist -> ()
866
  | Open _  -> ()
867

    
868
let uneval_prog_generics prog =
869
 List.iter uneval_top_generics prog
870

    
871
let check_env_compat header declared computed =
872
  uneval_prog_generics header;
873
  Env.iter declared (fun k decl_clock_k -> 
874
    let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
875
    try_semi_unify decl_clock_k computed_c Location.dummy_loc
876
  ) 
877
(* Local Variables: *)
878
(* compile-command:"make -C .." *)
879
(* End: *)