Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / clock_calculus.ml @ 14d694c7

History | View | Annotate | Download (31.5 KB)

1
(* ----------------------------------------------------------------------------
2
 * SchedMCore - A MultiCore Scheduling Framework
3
 * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
4
 *
5
 * This file is part of Prelude
6
 *
7
 * Prelude is free software; you can redistribute it and/or
8
 * modify it under the terms of the GNU Lesser General Public License
9
 * as published by the Free Software Foundation ; either version 2 of
10
 * the License, or (at your option) any later version.
11
 *
12
 * Prelude is distributed in the hope that it will be useful, but
13
 * WITHOUT ANY WARRANTY ; without even the implied warranty of
14
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15
 * Lesser General Public License for more details.
16
 *
17
 * You should have received a copy of the GNU Lesser General Public
18
 * License along with this program ; if not, write to the Free Software
19
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
20
 * USA
21
 *---------------------------------------------------------------------------- *)
22

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

    
26
(* Though it shares similarities with the typing module, no code
27
    is shared.  Simple environments, very limited identifier scoping, no
28
    identifier redefinition allowed. *)
29
open Utils
30
open LustreSpec
31
open Corelang
32
open Clocks
33
open Format
34

    
35
let loc_of_cond loc_containing id =
36
  let pos_start =
37
    {loc_containing.Location.loc_end with 
38
     Lexing.pos_cnum=loc_containing.Location.loc_end.Lexing.pos_cnum-(String.length id)}
39
  in
40
  {Location.loc_start = pos_start;
41
   Location.loc_end = loc_containing.Location.loc_end}
42

    
43
(** [occurs cvar ck] returns true if the clock variable [cvar] occurs in
44
    clock [ck]. False otherwise. *)
45
let rec occurs cvar ck =
46
  let ck = repr ck in
47
  match ck.cdesc with
48
  | Carrow (ck1, ck2) ->
49
      (occurs cvar ck1) || (occurs cvar ck2)
50
  | Ctuple ckl ->
51
      List.exists (occurs cvar) ckl
52
  | Con (ck',_,_) -> occurs cvar ck'
53
  | Pck_up (ck',_) -> occurs cvar ck'
54
  | Pck_down (ck',_) -> occurs cvar ck'
55
  | Pck_phase (ck',_) -> occurs cvar ck'
56
  | Cvar _ -> ck=cvar
57
  | Cunivar _ | Pck_const (_,_) -> false
58
  | Clink ck' -> occurs cvar ck'
59
  | Ccarrying (_,ck') -> occurs cvar ck'
60

    
61
(* Clocks generalization *)
62
let rec generalize_carrier cr =
63
  match cr.carrier_desc with
64
  | Carry_const _
65
  | Carry_name ->
66
      if cr.carrier_scoped then
67
        raise (Scope_carrier cr);
68
      cr.carrier_desc <- Carry_var
69
  | Carry_var -> ()
70
  | Carry_link cr' -> generalize_carrier cr'
71

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

    
94
let try_generalize ck_node loc =
95
  try 
96
    generalize ck_node
97
  with (Scope_carrier cr) ->
98
    raise (Error (loc, Carrier_extrusion (ck_node, cr)))
99
  | (Scope_clock ck) ->
100
    raise (Error (loc, Clock_extrusion (ck_node, ck)))
101

    
102
(* Clocks instanciation *)
103
let instantiate_carrier cr inst_cr_vars =
104
  let cr = carrier_repr cr in
105
  match cr.carrier_desc with
106
  | Carry_const _
107
  | Carry_name -> cr
108
  | Carry_link _ ->
109
      failwith "Internal error"
110
  | Carry_var ->
111
      try
112
        List.assoc cr.carrier_id !inst_cr_vars
113
      with Not_found ->            
114
        let cr_var = new_carrier Carry_name true in
115
        inst_cr_vars := (cr.carrier_id,cr_var)::!inst_cr_vars;
116
        cr_var
117

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

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

    
188
let rec update_scope_carrier scoped cr =
189
  if (not scoped) then
190
    begin
191
      cr.carrier_scoped <- scoped;
192
      match cr.carrier_desc with
193
	| Carry_const _ | Carry_name | Carry_var -> ()
194
      | Carry_link cr' -> update_scope_carrier scoped cr'
195
    end
196

    
197
let rec update_scope scoped ck =
198
  if (not scoped) then
199
    begin
200
      ck.cscoped <- scoped;
201
      match ck.cdesc with
202
      | Carrow (ck1,ck2) ->
203
          update_scope scoped ck1; update_scope scoped ck2
204
      | Ctuple clist ->
205
          List.iter (update_scope scoped) clist
206
      | Con (ck',cr,_) -> update_scope scoped ck'(*; update_scope_carrier scoped cr*)
207
      | Cvar cset ->
208
          ck.cdesc <- Cvar cset
209
      | Pck_up (ck',_) -> update_scope scoped ck'
210
      | Pck_down (ck',_) -> update_scope scoped ck'
211
      | Pck_phase (ck',_) -> update_scope scoped ck'
212
      | Pck_const (_,_) | Cunivar _ -> ()
213
      | Clink ck' ->
214
          update_scope scoped ck'
215
      | Ccarrying (cr,ck') ->
216
          update_scope_carrier scoped cr; update_scope scoped ck'
217
    end
218

    
219
(* Unifies two static pclocks. *)
220
let unify_static_pck ck1 ck2 =
221
  if (period ck1 <> period ck2) || (phase ck1 <> phase ck2) then
222
    raise (Unify (ck1,ck2))
223

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

    
256
(* Semi-unifies two clock carriers *)
257
let semi_unify_carrier cr1 cr2 =
258
  let cr1 = carrier_repr cr1 in
259
  let cr2 = carrier_repr cr2 in
260
  if cr1=cr2 then ()
261
  else
262
    match cr1.carrier_desc, cr2.carrier_desc with
263
    | Carry_const id1, Carry_const id2 ->
264
      if id1 <> id2 then raise (Mismatch (cr1, cr2))
265
    | Carry_const _, Carry_name ->
266
      begin
267
	cr2.carrier_desc <- Carry_link cr1;
268
	update_scope_carrier cr2.carrier_scoped cr1
269
      end
270
    | Carry_name, Carry_const _ -> raise (Mismatch (cr1, cr2))
271
    | Carry_name, Carry_name ->
272
      if cr1.carrier_id < cr2.carrier_id then
273
        begin
274
          cr2.carrier_desc <- Carry_link cr1;
275
          update_scope_carrier cr2.carrier_scoped cr1
276
        end
277
      else
278
        begin
279
          cr1.carrier_desc <- Carry_link cr2;
280
          update_scope_carrier cr1.carrier_scoped cr2
281
        end
282
    | _,_ -> assert false
283

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

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

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

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

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

    
493
(** [clock_uncarry ck] drops the possible carrier name from clock [ck] *)
494
let clock_uncarry ck =
495
  let ck = repr ck in
496
  match ck.cdesc with
497
  | Ccarrying (_, ck') -> ck'
498
  | _                  -> ck
499

    
500
let try_unify ck1 ck2 loc =
501
  try
502
    unify ck1 ck2
503
  with
504
  | Unify (ck1',ck2') ->
505
    raise (Error (loc, Clock_clash (ck1',ck2')))
506
  | Subsume (ck,cset) ->
507
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
508
  | Mismatch (cr1,cr2) ->
509
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
510

    
511
let try_semi_unify ck1 ck2 loc =
512
  try
513
    semi_unify ck1 ck2
514
  with
515
  | Unify (ck1',ck2') ->
516
    raise (Error (loc, Clock_clash (ck1',ck2')))
517
  | Subsume (ck,cset) ->
518
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
519
  | Mismatch (cr1,cr2) ->
520
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
521

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

    
544
let try_sub_unify sub ck1 ck2 loc =
545
  try
546
    sub_unify sub ck1 ck2
547
  with
548
  | Unify (ck1',ck2') ->
549
    raise (Error (loc, Clock_clash (ck1',ck2')))
550
  | Subsume (ck,cset) ->
551
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
552
  | Mismatch (cr1,cr2) ->
553
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
554

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

    
566
(* emulates a subtyping relation between clocks c and (cr : c),
567
   used during node application only *)
568
and clock_subtyping_arg env ?(sub=true) real_arg formal_clock =
569
  let loc = real_arg.expr_loc in
570
  let real_clock = clock_expr env real_arg in
571
  try_sub_unify sub real_clock formal_clock loc
572

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

    
583
and clock_call env f args clock_reset loc =
584
  let cfun = clock_ident false env f loc in
585
  let cins, couts = split_arrow cfun in
586
  let cins = clock_list_of_clock cins in
587
  List.iter2 (clock_subtyping_arg env) args cins;
588
  unify_imported_clock (Some clock_reset) cfun;
589
  couts
590

    
591
and clock_ident nocarrier env id loc =
592
  clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc)
593

    
594
and clock_carrier env c loc ce =
595
  let expr_c = expr_of_ident c loc in
596
  let ck = clock_expr ~nocarrier:false env expr_c in
597
  let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in
598
  let ckcarry = new_ck (Ccarrying (cr,ce)) ck.cscoped in
599
  try_unify ck ckcarry expr_c.expr_loc;
600
  cr
601

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

    
730
let clock_of_vlist vars =
731
  let ckl = List.map (fun v -> v.var_clock) vars in
732
  clock_of_clock_list ckl
733

    
734
(** [clock_eq env eq] performs the clock-calculus for equation [eq] in
735
    environment [env] *)
736
let clock_eq env eq =
737
  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
738
  let ck_rhs = clock_expr env eq.eq_rhs in
739
  clock_subtyping_arg env expr_lhs ck_rhs
740

    
741

    
742
(* [clock_coreclock cck] returns the clock_expr corresponding to clock
743
    declaration [cck] *)
744
let clock_coreclock env cck id loc scoped =
745
  match cck.ck_dec_desc with
746
  | Ckdec_any -> new_var scoped
747
  | Ckdec_pclock (n,(a,b)) ->
748
      let ck = new_ck (Pck_const (n,(a,b))) scoped in
749
      if n mod b <> 0 then raise (Error (loc,Invalid_const ck));
750
      ck
751
  | Ckdec_bool cl ->
752
      let temp_env = Env.add_value env id (new_var true) in
753
      (* We just want the id to be present in the environment *)
754
      let dummy_id_expr = expr_of_ident id loc in
755
      let when_expr =
756
        List.fold_left
757
          (fun expr (x,l) ->
758
                {expr_tag = new_tag ();
759
                 expr_desc = Expr_when (expr,x,l);
760
                 expr_type = Types.new_var ();
761
                 expr_clock = new_var scoped;
762
                 expr_delay = Delay.new_var ();
763
                 expr_loc = loc;
764
		 expr_annot = None})
765
          dummy_id_expr cl
766
      in
767
      clock_expr temp_env when_expr
768

    
769
(* Clocks a variable declaration *)
770
let clock_var_decl scoped env vdecl =
771
  let ck = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in
772
  let ck =
773
(* WTF ????
774
    if vdecl.var_dec_const
775
    then
776
      (try_generalize ck vdecl.var_loc; ck)
777
    else
778
 *)
779
      if Types.is_clock_type vdecl.var_type
780
      then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped
781
      else ck in
782
  vdecl.var_clock <- ck;
783
  Env.add_value env vdecl.var_id ck
784

    
785
(* Clocks a variable declaration list *)
786
let clock_var_decl_list env scoped l =
787
  List.fold_left (clock_var_decl scoped) env l
788

    
789
(** [clock_node env nd] performs the clock-calculus for node [nd] in
790
    environment [env].
791
    Generalization of clocks wrt scopes follows this rule:
792
    - generalize inputs (unscoped).
793
    - generalize outputs. As they are scoped, only clocks coming from inputs
794
      are allowed to be generalized.
795
    - generalize locals. As outputs don't depend on them (checked the step before),
796
      they can be generalized. 
797
 *)
798
let clock_node env loc nd =
799
  (* let is_main = nd.node_id = !Options.main_node in *)
800
  let new_env = clock_var_decl_list env false nd.node_inputs in
801
  let new_env = clock_var_decl_list new_env true nd.node_outputs in
802
  let new_env = clock_var_decl_list new_env true nd.node_locals in
803
  List.iter (clock_eq new_env) nd.node_eqs;
804
  let ck_ins = clock_of_vlist nd.node_inputs in
805
  let ck_outs = clock_of_vlist nd.node_outputs in
806
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
807
  unify_imported_clock None ck_node;
808
  Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
809
  (* Local variables may contain first-order carrier variables that should be generalized.
810
     That's not the case for types. *)
811
  List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs;
812
  List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;
813
  (*List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;*)
814
  (* TODO : Xavier pourquoi ai je cette erreur ? *)
815
(*  if (is_main && is_polymorphic ck_node) then
816
    raise (Error (loc,(Cannot_be_polymorphic ck_node)));
817
*)
818
  Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
819
  nd.node_clock <- ck_node;
820
  Env.add_value env nd.node_id ck_node
821

    
822

    
823
let check_imported_pclocks loc ck_node =
824
  let pck = ref None in
825
  let rec aux ck =
826
    match ck.cdesc with
827
    | Carrow (ck1,ck2) -> aux ck1; aux ck2
828
    | Ctuple cl -> List.iter aux cl
829
    | Con (ck',_,_) -> aux ck'
830
    | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) -> 
831
        raise (Error (loc, (Invalid_imported_clock ck_node)))
832
    | Pck_const (n,p) ->
833
        begin
834
          match !pck with
835
          | None -> pck := Some (n,p)
836
          | Some (n',p') ->
837
              if (n,p) <> (n',p') then
838
                raise (Error (loc, (Invalid_imported_clock ck_node)))
839
        end
840
    | Clink ck' -> aux ck'
841
    | Ccarrying (_,ck') -> aux ck'
842
    | Cvar _ | Cunivar _ ->
843
        match !pck with
844
        | None -> ()
845
        | Some (_,_) ->
846
            raise (Error (loc, (Invalid_imported_clock ck_node)))
847
  in
848
  aux ck_node
849

    
850
let clock_imported_node env loc nd =
851
  let new_env = clock_var_decl_list env false nd.nodei_inputs in
852
  ignore(clock_var_decl_list new_env false nd.nodei_outputs);
853
  let ck_ins = clock_of_vlist nd.nodei_inputs in
854
  let ck_outs = clock_of_vlist nd.nodei_outputs in
855
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
856
  unify_imported_clock None ck_node;
857
  check_imported_pclocks loc ck_node;
858
  try_generalize ck_node loc;
859
  nd.nodei_clock <- ck_node;
860
  Env.add_value env nd.nodei_id ck_node
861

    
862
let clock_top_consts env clist =
863
  List.fold_left (fun env cdecl ->
864
    let ck = new_var false in
865
    try_generalize ck cdecl.const_loc;
866
    Env.add_value env cdecl.const_id ck) env clist
867

    
868
let clock_top_decl env decl =
869
  match decl.top_decl_desc with
870
  | Node nd ->
871
    clock_node env decl.top_decl_loc nd
872
  | ImportedNode nd ->
873
    clock_imported_node env decl.top_decl_loc nd
874
  | Consts clist ->
875
    clock_top_consts env clist
876
  | Open _ ->
877
    env
878

    
879
let clock_prog env decls =
880
  List.fold_left (fun e decl -> clock_top_decl e decl) env decls
881

    
882
(* Once the Lustre program is fully clocked,
883
   we must get back to the original description of clocks,
884
   with constant parameters, instead of unifiable internal variables. *)
885

    
886
(* The following functions aims at 'unevaluating' carriers occuring in clock expressions,
887
   i.e. replacing unifiable second_order variables with the original carrier names.
888
   Once restored in this formulation, clocks may be meaningfully printed.
889
*)
890
let uneval_vdecl_generics vdecl =
891
 (*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@." Printers.pp_node_var vdecl;*)
892
 if Types.is_clock_type vdecl.var_type
893
 then
894
   match get_carrier_name vdecl.var_clock with
895
   | None    -> (Format.eprintf "internal error: %a@." print_ck vdecl.var_clock; assert false)
896
   | Some cr -> Clocks.uneval vdecl.var_id cr
897

    
898
let uneval_node_generics vdecls =
899
  List.iter uneval_vdecl_generics vdecls
900

    
901
let uneval_top_generics decl =
902
  match decl.top_decl_desc with
903
  | Node nd ->
904
      (* A node could contain first-order carrier variable in local vars. This is not the case for types. *)
905
      uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)
906
  | ImportedNode nd ->
907
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
908
  | Consts clist -> ()
909
  | Open _  -> ()
910

    
911
let uneval_prog_generics prog =
912
 List.iter uneval_top_generics prog
913

    
914
let check_env_compat header declared computed =
915
  uneval_prog_generics header;
916
  Env.iter declared (fun k decl_clock_k -> 
917
    let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
918
    try_semi_unify decl_clock_k computed_c Location.dummy_loc
919
  ) 
920
(* Local Variables: *)
921
(* compile-command:"make -C .." *)
922
(* End: *)