Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / clock_calculus.ml @ 70e1006b

History | View | Annotate | Download (30.9 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
let try_unify_carrier ck1 ck2 loc =
277
  try
278
    unify_carrier ck1 ck2
279
  with
280
  | Unify (ck1',ck2') ->
281
    raise (Error (loc, Clock_clash (ck1',ck2')))
282
  | Subsume (ck,cset) ->
283
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
284
  | Mismatch (cr1,cr2) ->
285
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
286

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

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

    
436
(* Returns the value corresponding to a pclock (integer) factor
437
   expression. Expects a constant expression (checked by typing). *)
438
let int_factor_of_expr e =
439
  match e.expr_desc with 
440
  | Expr_const
441
      (Const_int i) -> i
442
  | _ -> failwith "Internal error: int_factor_of_expr"
443

    
444
(** [clock_uncarry ck] drops the possible carrier name from clock [ck] *)
445
let clock_uncarry ck =
446
  let ck = repr ck in
447
  match ck.cdesc with
448
  | Ccarrying (_, ck') -> ck'
449
  | _                  -> ck
450

    
451
let try_unify ck1 ck2 loc =
452
  try
453
    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
let try_semi_unify ck1 ck2 loc =
463
  try
464
    semi_unify ck1 ck2
465
  with
466
  | Unify (ck1',ck2') ->
467
    raise (Error (loc, Clock_clash (ck1',ck2')))
468
  | Subsume (ck,cset) ->
469
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
470
  | Mismatch (cr1,cr2) ->
471
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
472

    
473
(* ck2 is a subtype of ck1 *)
474
let rec sub_unify sub ck1 ck2 =
475
  match (repr ck1).cdesc, (repr ck2).cdesc with
476
  | Ctuple cl1         , Ctuple cl2         ->
477
    if List.length cl1 <> List.length cl2
478
    then raise (Unify (ck1, ck2))
479
    else List.iter2 (sub_unify sub) cl1 cl2
480
  | Ctuple [c1]        , _                  -> sub_unify sub c1 ck2
481
  | _                  , Ctuple [c2]        -> sub_unify sub ck1 c2
482
  | Con (c1, cr1, t1)  , Con (c2, cr2, t2) when t1=t2 ->
483
    begin
484
      unify_carrier cr1 cr2;
485
      sub_unify sub c1 c2
486
    end
487
  | Ccarrying (cr1, c1), Ccarrying (cr2, c2)->
488
    begin
489
      unify_carrier cr1 cr2;
490
      sub_unify sub c1 c2
491
    end
492
  | _, Ccarrying (_, c2)           when sub -> sub_unify sub ck1 c2
493
  | _                                       -> unify ck1 ck2
494

    
495
let try_sub_unify sub ck1 ck2 loc =
496
  try
497
    sub_unify sub ck1 ck2
498
  with
499
  | Unify (ck1',ck2') ->
500
    raise (Error (loc, Clock_clash (ck1',ck2')))
501
  | Subsume (ck,cset) ->
502
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
503
  | Mismatch (cr1,cr2) ->
504
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
505

    
506
(* Unifies all the clock variables in the clock type of a tuple 
507
   expression, so that the clock type only uses at most one clock variable *)
508
let unify_tuple_clock ref_ck_opt ck loc =
509
(*(match ref_ck_opt with
510
| None     -> Format.eprintf "unify_tuple_clock None %a@." Clocks.print_ck ck
511
  | Some ck' -> Format.eprintf "unify_tuple_clock (Some %a) %a@." Clocks.print_ck ck' Clocks.print_ck ck);*)
512
  let ck_var = ref ref_ck_opt in
513
  let rec aux ck =
514
    match (repr ck).cdesc with
515
    | Con _
516
    | Cvar _ ->
517
        begin
518
          match !ck_var with
519
          | None ->
520
              ck_var:=Some ck
521
          | Some v ->
522
              (* may fail *)
523
              try_unify ck v loc
524
        end
525
    | Ctuple cl ->
526
        List.iter aux cl
527
    | Carrow _ -> assert false (* should not occur *)
528
    | Ccarrying (_, ck1) ->
529
        aux ck1
530
    | _ -> ()
531
  in aux ck
532

    
533
(* Unifies all the clock variables in the clock type of an imported
534
   node, so that the clock type only uses at most one base clock variable,
535
   that is, the activation clock of the node *)
536
let unify_imported_clock ref_ck_opt ck loc =
537
  let ck_var = ref ref_ck_opt in
538
  let rec aux ck =
539
    match (repr ck).cdesc with
540
    | Cvar _ ->
541
        begin
542
          match !ck_var with
543
          | None ->
544
              ck_var:=Some ck
545
          | Some v ->
546
              (* cannot fail *)
547
              try_unify ck v loc
548
        end
549
    | Ctuple cl ->
550
        List.iter aux cl
551
    | Carrow (ck1,ck2) ->
552
        aux ck1; aux ck2
553
    | Ccarrying (_, ck1) ->
554
        aux ck1
555
    | Con (ck1, _, _) -> aux ck1
556
    | _ -> ()
557
  in
558
  aux ck
559

    
560
(* Clocks a list of arguments of Lustre builtin operators:
561
   - type each expression, remove carriers of clocks as
562
     carriers may only denote variables, not arbitrary expr.
563
   - try to unify these clocks altogether
564
*)
565
let rec clock_standard_args env expr_list =
566
  let ck_list = List.map (fun e -> clock_uncarry (clock_expr env e)) expr_list in
567
  let ck_res = new_var true in
568
  List.iter2 (fun e ck -> try_unify ck ck_res e.expr_loc) expr_list ck_list;
569
  ck_res
570

    
571
(* emulates a subtyping relation between clocks c and (cr : c),
572
   used during node application only *)
573
and clock_subtyping_arg env ?(sub=true) real_arg formal_clock =
574
  let loc = real_arg.expr_loc in
575
  let real_clock = clock_expr env real_arg in
576
  try_sub_unify sub formal_clock real_clock loc
577

    
578
(* computes clocks for node application *)
579
and clock_appl env f args clock_reset loc =
580
 let args = expr_list_of_expr args in
581
  if Basic_library.is_internal_fun f && List.exists is_tuple_expr args
582
  then
583
      let args = Utils.transpose_list (List.map expr_list_of_expr args) in
584
      Clocks.clock_of_clock_list (List.map (fun args -> clock_call env f args clock_reset loc) args)
585
  else
586
    clock_call env f args clock_reset loc
587

    
588
and clock_call env f args clock_reset loc =
589
  let cfun = clock_ident false env f loc in
590
  let cins, couts = split_arrow cfun in
591
  let cins = clock_list_of_clock cins in
592
  List.iter2 (clock_subtyping_arg env) args cins;
593
  unify_imported_clock (Some clock_reset) cfun loc;
594
  couts
595

    
596
and clock_ident nocarrier env id loc =
597
  clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc)
598

    
599
and clock_carrier env c loc ce =
600
  let expr_c = expr_of_ident c loc in
601
  let ck = clock_expr ~nocarrier:false env expr_c in
602
  let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in
603
  let ckb = new_var true in
604
  let ckcarry = new_ck (Ccarrying (cr, ckb)) ck.cscoped in
605
  try_unify ck ckcarry expr_c.expr_loc;
606
  unify_tuple_clock (Some ckb) ce expr_c.expr_loc;
607
  cr
608

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

    
702
let clock_of_vlist vars =
703
  let ckl = List.map (fun v -> v.var_clock) vars in
704
  clock_of_clock_list ckl
705

    
706
(** [clock_eq env eq] performs the clock-calculus for equation [eq] in
707
    environment [env] *)
708
let clock_eq env eq =
709
  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
710
  let ck_rhs = clock_expr env eq.eq_rhs in
711
  clock_subtyping_arg env expr_lhs ck_rhs
712

    
713
(* [clock_coreclock cck] returns the clock_expr corresponding to clock
714
    declaration [cck] *)
715
let clock_coreclock env cck id loc scoped =
716
  match cck.ck_dec_desc with
717
  | Ckdec_any -> new_var scoped
718
  | Ckdec_pclock (n,(a,b)) ->
719
      let ck = new_ck (Pck_const (n,(a,b))) scoped in
720
      if n mod b <> 0 then raise (Error (loc,Invalid_const ck));
721
      ck
722
  | Ckdec_bool cl ->
723
      let temp_env = Env.add_value env id (new_var true) in
724
      (* We just want the id to be present in the environment *)
725
      let dummy_id_expr = expr_of_ident id loc in
726
      let when_expr =
727
        List.fold_left
728
          (fun expr (x,l) ->
729
                {expr_tag = new_tag ();
730
                 expr_desc = Expr_when (expr,x,l);
731
                 expr_type = Types.new_var ();
732
                 expr_clock = new_var scoped;
733
                 expr_delay = Delay.new_var ();
734
                 expr_loc = loc;
735
		 expr_annot = None})
736
          dummy_id_expr cl
737
      in
738
      clock_expr temp_env when_expr
739

    
740
(* Clocks a variable declaration *)
741
let clock_var_decl scoped env vdecl =
742
  let ck = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in
743
  let ck =
744
(* WTF ????
745
    if vdecl.var_dec_const
746
    then
747
      (try_generalize ck vdecl.var_loc; ck)
748
    else
749
 *)
750
      if Types.get_clock_base_type vdecl.var_type <> None
751
      then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped
752
      else ck in
753
  vdecl.var_clock <- ck;
754
  Env.add_value env vdecl.var_id ck
755

    
756
(* Clocks a variable declaration list *)
757
let clock_var_decl_list env scoped l =
758
  List.fold_left (clock_var_decl scoped) env l
759

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

    
795

    
796
let check_imported_pclocks loc ck_node =
797
  let pck = ref None in
798
  let rec aux ck =
799
    match ck.cdesc with
800
    | Carrow (ck1,ck2) -> aux ck1; aux ck2
801
    | Ctuple cl -> List.iter aux cl
802
    | Con (ck',_,_) -> aux ck'
803
    | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) -> 
804
        raise (Error (loc, (Invalid_imported_clock ck_node)))
805
    | Pck_const (n,p) ->
806
        begin
807
          match !pck with
808
          | None -> pck := Some (n,p)
809
          | Some (n',p') ->
810
              if (n,p) <> (n',p') then
811
                raise (Error (loc, (Invalid_imported_clock ck_node)))
812
        end
813
    | Clink ck' -> aux ck'
814
    | Ccarrying (_,ck') -> aux ck'
815
    | Cvar _ | Cunivar _ ->
816
        match !pck with
817
        | None -> ()
818
        | Some (_,_) ->
819
            raise (Error (loc, (Invalid_imported_clock ck_node)))
820
  in
821
  aux ck_node
822

    
823
let clock_imported_node env loc nd =
824
  let new_env = clock_var_decl_list env false nd.nodei_inputs in
825
  ignore(clock_var_decl_list new_env false nd.nodei_outputs);
826
  let ck_ins = clock_of_vlist nd.nodei_inputs in
827
  let ck_outs = clock_of_vlist nd.nodei_outputs in
828
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
829
  unify_imported_clock None ck_node loc;
830
  check_imported_pclocks loc ck_node;
831
  try_generalize ck_node loc;
832
  nd.nodei_clock <- ck_node;
833
  Env.add_value env nd.nodei_id ck_node
834

    
835
let clock_top_const env cdecl=
836
  let ck = new_var false in
837
  try_generalize ck cdecl.const_loc;
838
  Env.add_value env cdecl.const_id ck
839

    
840
let clock_top_consts env clist =
841
  List.fold_left clock_top_const env clist
842
 
843
let rec clock_top_decl env decl =
844
  match decl.top_decl_desc with
845
  | Node nd ->
846
    clock_node env decl.top_decl_loc nd
847
  | ImportedNode nd ->
848
    clock_imported_node env decl.top_decl_loc nd
849
  | Const c ->
850
    clock_top_const env c
851
  | TypeDef _ -> List.fold_left clock_top_decl env (consts_of_enum_type decl)
852
  | Open _    -> env
853

    
854
let clock_prog env decls =
855
  List.fold_left clock_top_decl env decls
856

    
857
(* Once the Lustre program is fully clocked,
858
   we must get back to the original description of clocks,
859
   with constant parameters, instead of unifiable internal variables. *)
860

    
861
(* The following functions aims at 'unevaluating' carriers occuring in clock expressions,
862
   i.e. replacing unifiable second_order variables with the original carrier names.
863
   Once restored in this formulation, clocks may be meaningfully printed.
864
*)
865
let uneval_vdecl_generics vdecl =
866
 (*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@." Printers.pp_node_var vdecl;*)
867
 if Types.get_clock_base_type vdecl.var_type <> None
868
 then
869
   match get_carrier_name vdecl.var_clock with
870
   | None    -> (Format.eprintf "internal error: %a@." print_ck vdecl.var_clock; assert false)
871
   | Some cr -> Clocks.uneval vdecl.var_id cr
872

    
873
let uneval_node_generics vdecls =
874
  List.iter uneval_vdecl_generics vdecls
875

    
876
let uneval_top_generics decl =
877
  match decl.top_decl_desc with
878
  | Node nd ->
879
      (* A node could contain first-order carrier variable in local vars. This is not the case for types. *)
880
      uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)
881
  | ImportedNode nd ->
882
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
883
  | Const _
884
  | Open _
885
  | TypeDef _ -> ()
886

    
887
let uneval_prog_generics prog =
888
 List.iter uneval_top_generics prog
889

    
890
let check_env_compat header declared computed =
891
  uneval_prog_generics header;
892
  Env.iter declared (fun k decl_clock_k -> 
893
    let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
894
    try_semi_unify decl_clock_k computed_c Location.dummy_loc
895
  ) 
896
(* Local Variables: *)
897
(* compile-command:"make -C .." *)
898
(* End: *)