Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / clock_calculus.ml @ d4807c3d

History | View | Annotate | Download (31.2 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 cfun = clock_ident false env f loc in
576
  let cins, couts = split_arrow cfun in
577
  let cins = clock_list_of_clock cins in
578
  let args = expr_list_of_expr args in
579
  List.iter2 (clock_subtyping_arg env) args cins;
580
  unify_imported_clock (Some clock_reset) cfun;
581
  couts
582

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

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

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

    
722
let clock_of_vlist vars =
723
  let ckl = List.map (fun v -> v.var_clock) vars in
724
  clock_of_clock_list ckl
725

    
726
(** [clock_eq env eq] performs the clock-calculus for equation [eq] in
727
    environment [env] *)
728
let clock_eq env eq =
729
  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
730
  let ck_rhs = clock_expr env eq.eq_rhs in
731
  clock_subtyping_arg env expr_lhs ck_rhs
732

    
733

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

    
761
(* Clocks a variable declaration *)
762
let clock_var_decl scoped env vdecl =
763
  let ck = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in
764
  let ck =
765
(* WTF ????
766
    if vdecl.var_dec_const
767
    then
768
      (try_generalize ck vdecl.var_loc; ck)
769
    else
770
 *)
771
      if Types.is_clock_type vdecl.var_type
772
      then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped
773
      else ck in
774
  vdecl.var_clock <- ck;
775
  Env.add_value env vdecl.var_id ck
776

    
777
(* Clocks a variable declaration list *)
778
let clock_var_decl_list env scoped l =
779
  List.fold_left (clock_var_decl scoped) env l
780

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

    
814

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

    
842
let clock_imported_node env loc nd =
843
  let new_env = clock_var_decl_list env false nd.nodei_inputs in
844
  ignore(clock_var_decl_list new_env false nd.nodei_outputs);
845
  let ck_ins = clock_of_vlist nd.nodei_inputs in
846
  let ck_outs = clock_of_vlist nd.nodei_outputs in
847
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
848
  unify_imported_clock None ck_node;
849
  check_imported_pclocks loc ck_node;
850
  try_generalize ck_node loc;
851
  nd.nodei_clock <- ck_node;
852
  Env.add_value env nd.nodei_id ck_node
853

    
854
let clock_top_consts env clist =
855
  List.fold_left (fun env cdecl ->
856
    let ck = new_var false in
857
    try_generalize ck cdecl.const_loc;
858
    Env.add_value env cdecl.const_id ck) env clist
859

    
860
let clock_top_decl env decl =
861
  match decl.top_decl_desc with
862
  | Node nd ->
863
    clock_node env decl.top_decl_loc nd
864
  | ImportedNode nd ->
865
    clock_imported_node env decl.top_decl_loc nd
866
  | Consts clist ->
867
    clock_top_consts env clist
868
  | Open _ ->
869
    env
870

    
871
let clock_prog env decls =
872
  List.fold_left (fun e decl -> clock_top_decl e decl) env decls
873

    
874
(* Once the Lustre program is fully clocked,
875
   we must get back to the original description of clocks,
876
   with constant parameters, instead of unifiable internal variables. *)
877

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

    
890
let uneval_node_generics vdecls =
891
  List.iter uneval_vdecl_generics vdecls
892

    
893
let uneval_top_generics decl =
894
  match decl.top_decl_desc with
895
  | Node nd ->
896
      (* A node could contain first-order carrier variable in local vars. This is not the case for types. *)
897
      uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)
898
  | ImportedNode nd ->
899
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
900
  | Consts clist -> ()
901
  | Open _  -> ()
902

    
903
let uneval_prog_generics prog =
904
 List.iter uneval_top_generics prog
905

    
906
let check_env_compat header declared computed =
907
  uneval_prog_generics header;
908
  Env.iter declared (fun k decl_clock_k -> 
909
    let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
910
    try_semi_unify decl_clock_k computed_c Location.dummy_loc
911
  ) 
912
(* Local Variables: *)
913
(* compile-command:"make -C .." *)
914
(* End: *)