Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / clock_calculus.ml @ d3e4c22f

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 [c1]        , Ctuple [c2]        -> sub_unify sub c1 c2
526
  | Ctuple cl1         , Ctuple cl2         ->
527
    if List.length cl1 <> List.length cl2
528
    then raise (Unify (ck1, ck2))
529
    else List.iter2 (sub_unify sub) cl1 cl2
530
  | Ctuple [c1]        , _                  -> sub_unify sub c1 ck2
531
  | _                  , Ctuple [c2]        -> sub_unify sub ck1 c2
532
  | Con (c1, cr1, t1)  , Con (c2, cr2, t2) when t1=t2 ->
533
    begin
534
      unify_carrier cr1 cr2;
535
      sub_unify sub c1 c2
536
    end
537
  | Ccarrying (cr1, c1), Ccarrying (cr2, c2)->
538
    begin
539
      unify_carrier cr1 cr2;
540
      sub_unify sub c1 c2
541
    end
542
  | Ccarrying (_, c1)  , _         when sub -> sub_unify sub c1 ck2
543
  | _                                       -> unify ck1 ck2
544

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

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

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

    
574
(* computes clocks for node application *)
575
and clock_appl env f args clock_reset loc =
576
  let cfun = clock_ident false env f loc in
577
  let cins, couts = split_arrow cfun in
578
  let cins = clock_list_of_clock cins in
579
  let args = expr_list_of_expr args in
580
  List.iter2 (clock_subtyping_arg env) args cins;
581
  unify_imported_clock (Some clock_reset) cfun;
582
  couts
583

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

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

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

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

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

    
734

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

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

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

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

    
815

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

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

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

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

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

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

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

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

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

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

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