Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / clock_calculus.ml @ 45c13277

History | View | Annotate | Download (30.3 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
(** [clock_uncarry ck] drops the possible carrier name from clock [ck] *)
434
let clock_uncarry ck =
435
  let ck = repr ck in
436
  match ck.cdesc with
437
  | Ccarrying (_, ck') -> ck'
438
  | _                  -> ck
439

    
440
let try_unify ck1 ck2 loc =
441
  try
442
    unify ck1 ck2
443
  with
444
  | Unify (ck1',ck2') ->
445
    raise (Error (loc, Clock_clash (ck1',ck2')))
446
  | Subsume (ck,cset) ->
447
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
448
  | Mismatch (cr1,cr2) ->
449
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
450

    
451
let try_semi_unify ck1 ck2 loc =
452
  try
453
    semi_unify ck1 ck2
454
  with
455
  | Unify (ck1',ck2') ->
456
    raise (Error (loc, Clock_clash (ck1',ck2')))
457
  | Subsume (ck,cset) ->
458
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
459
  | Mismatch (cr1,cr2) ->
460
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
461

    
462
(* ck1 is a subtype of ck2 *)
463
let rec sub_unify sub ck1 ck2 =
464
  match (repr ck1).cdesc, (repr ck2).cdesc with
465
  | Ctuple cl1         , Ctuple cl2         ->
466
    if List.length cl1 <> List.length cl2
467
    then raise (Unify (ck1, ck2))
468
    else List.iter2 (sub_unify sub) cl1 cl2
469
  | Ctuple [c1]        , _                  -> sub_unify sub c1 ck2
470
  | _                  , Ctuple [c2]        -> sub_unify sub ck1 c2
471
  | Con (c1, cr1, t1)  , Con (c2, cr2, t2) when t1=t2 ->
472
    begin
473
      unify_carrier cr1 cr2;
474
      sub_unify sub c1 c2
475
    end
476
  | Ccarrying (cr1, c1), Ccarrying (cr2, c2)->
477
    begin
478
      unify_carrier cr1 cr2;
479
      sub_unify sub c1 c2
480
    end
481
  | Ccarrying (_, c1)  , _         when sub -> sub_unify sub c1 ck2
482
  | _                                       -> unify ck1 ck2
483

    
484
let try_sub_unify sub ck1 ck2 loc =
485
  try
486
    sub_unify sub ck1 ck2
487
  with
488
  | Unify (ck1',ck2') ->
489
    raise (Error (loc, Clock_clash (ck1',ck2')))
490
  | Subsume (ck,cset) ->
491
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
492
  | Mismatch (cr1,cr2) ->
493
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
494

    
495
(* Unifies all the clock variables in the clock type of a tuple 
496
   expression, so that the clock type only uses at most one clock variable *)
497
let unify_tuple_clock ref_ck_opt ck loc =
498
  let ck_var = ref ref_ck_opt in
499
  let rec aux ck =
500
    match (repr ck).cdesc with
501
    | Con _
502
    | Cvar _ ->
503
        begin
504
          match !ck_var with
505
          | None ->
506
              ck_var:=Some ck
507
          | Some v ->
508
              (* may fail *)
509
              try_unify v ck loc
510
        end
511
    | Ctuple cl ->
512
        List.iter aux cl
513
    | Carrow _ -> assert false (* should not occur *)
514
    | Ccarrying (_, ck1) ->
515
        aux ck1
516
    | _ -> ()
517
  in
518
  aux ck
519

    
520
(* Unifies all the clock variables in the clock type of an imported
521
   node, so that the clock type only uses at most one base clock variable,
522
   that is, the activation clock of the node *)
523
let unify_imported_clock ref_ck_opt ck loc =
524
  let ck_var = ref ref_ck_opt in
525
  let rec aux ck =
526
    match (repr ck).cdesc with
527
    | Cvar _ ->
528
        begin
529
          match !ck_var with
530
          | None ->
531
              ck_var:=Some ck
532
          | Some v ->
533
              (* cannot fail *)
534
              try_unify v ck loc
535
        end
536
    | Ctuple cl ->
537
        List.iter aux cl
538
    | Carrow (ck1,ck2) ->
539
        aux ck1; aux ck2
540
    | Ccarrying (_, ck1) ->
541
        aux ck1
542
    | Con (ck1, _, _) -> aux ck1
543
    | _ -> ()
544
  in
545
  aux ck
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 loc;
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
  ce, 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 expr.expr_loc;
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 expr.expr_loc;
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 ck_c, 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
      unify_tuple_clock (Some ck_c) ce expr.expr_loc;
674
      expr.expr_clock <- ck';
675
      ck
676
  | Expr_merge (c,hl) ->
677
      let cvar = new_var true in
678
      let ck_c, cr = clock_carrier env c expr.expr_loc cvar in
679
      List.iter (fun (t, h) -> clock_subtyping_arg env h (new_ck (Con (cvar,cr,t)) true)) hl;
680
      unify_tuple_clock (Some ck_c) cvar expr.expr_loc;
681
      expr.expr_clock <- cvar;
682
      cvar
683
  in
684
  Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck);
685
  resulting_ck
686

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

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

    
698

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

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

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

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

    
781

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

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

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

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

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

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

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

    
857
let uneval_node_generics vdecls =
858
  List.iter uneval_vdecl_generics vdecls
859

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

    
870
let uneval_prog_generics prog =
871
 List.iter uneval_top_generics prog
872

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