Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / clock_calculus.ml @ 8f1c7e91

History | View | Annotate | Download (30.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
(* Checks whether ck1 is a subtype of ck2 *)
523
let rec clock_subtyping ck1 ck2 =
524
  match (repr ck1).cdesc, (repr ck2).cdesc with
525
  | Ccarrying _         , Ccarrying _ -> unify ck1 ck2
526
  | Ccarrying (cr', ck'), _           -> unify ck' ck2
527
  | _                                 -> unify ck1 ck2
528

    
529
(* Clocks a list of arguments of Lustre builtin operators:
530
   - type each expression, remove carriers of clocks as
531
     carriers may only denote variables, not arbitrary expr.
532
   - try to unify these clocks altogether
533
*)
534
let rec clock_standard_args env expr_list =
535
  let ck_list = List.map (fun e -> clock_uncarry (clock_expr env e)) expr_list in
536
  let ck_res = new_var true in
537
  List.iter2 (fun e ck -> try_unify ck ck_res e.expr_loc) expr_list ck_list;
538
  ck_res
539

    
540
(* emulates a subtyping relation between clocks c and (cr : c),
541
   used during node application only *)
542
and clock_subtyping_arg env real_arg formal_clock =
543
  let loc = real_arg.expr_loc in
544
  let real_clock = clock_expr env real_arg in
545
  try
546
    clock_subtyping real_clock formal_clock
547
  with
548
  | Unify (ck1',ck2') ->
549
    raise (Error (loc, Clock_clash (real_clock, formal_clock)))
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
(* computes clocks for node application *)
556
and clock_appl env f args clock_reset loc =
557
  let cfun = clock_ident false env f loc in
558
  let cins, couts = split_arrow cfun in
559
  let cins = clock_list_of_clock cins in
560
  let args = expr_list_of_expr args in
561
  List.iter2 (clock_subtyping_arg env) args cins;
562
  unify_imported_clock (Some clock_reset) cfun;
563
  couts
564

    
565
and clock_ident nocarrier env id loc =
566
  clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc)
567

    
568
and clock_carrier env c loc ce =
569
  let expr_c = expr_of_ident c loc in
570
  let ck = clock_expr ~nocarrier:false env expr_c in
571
  let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in
572
  let ckcarry = new_ck (Ccarrying (cr,ce)) ck.cscoped in
573
  try_unify ck ckcarry expr_c.expr_loc;
574
  cr
575

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

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

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

    
715

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

    
743
(* Clocks a variable declaration *)
744
let clock_var_decl scoped env vdecl =
745
  let ck = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in
746
  let ck = 
747
    if vdecl.var_dec_const
748
    then
749
      (try_generalize ck vdecl.var_loc; ck)
750
    else
751
      match vdecl.var_type.Types.tdesc with
752
      | Types.Tclock _ -> new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped
753
      | _              -> ck in
754
  vdecl.var_clock <- ck;
755
  Env.add_value env vdecl.var_id ck
756

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

    
761
(** [clock_node env nd] performs the clock-calculus for node [nd] in
762
    environment [env]. *)
763
let clock_node env loc nd =
764
  (* let is_main = nd.node_id = !Options.main_node in *)
765
  let new_env = clock_var_decl_list env false nd.node_inputs in
766
  let new_env = clock_var_decl_list new_env true nd.node_outputs in
767
  let new_env = clock_var_decl_list new_env true nd.node_locals in
768
  List.iter (clock_eq new_env) nd.node_eqs;
769
  let ck_ins = clock_of_vlist nd.node_inputs in
770
  let ck_outs = clock_of_vlist nd.node_outputs in
771
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
772
  unify_imported_clock None ck_node;
773
  (*Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);*)
774
  try_generalize ck_node loc;
775
  (* TODO : Xavier pourquoi ai je cette erreur ? *)
776
(*  if (is_main && is_polymorphic ck_node) then
777
    raise (Error (loc,(Cannot_be_polymorphic ck_node)));
778
*)
779
  nd.node_clock <- ck_node;
780
  Env.add_value env nd.node_id ck_node
781

    
782

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

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

    
822
let clock_function env loc fcn =
823
  let new_env = clock_var_decl_list env false fcn.fun_inputs in
824
  ignore(clock_var_decl_list new_env false fcn.fun_outputs);
825
  let ck_ins = clock_of_vlist fcn.fun_inputs in
826
  let ck_outs = clock_of_vlist fcn.fun_outputs in
827
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
828
  unify_imported_clock None ck_node;
829
  check_imported_pclocks loc ck_node;
830
  try_generalize ck_node loc;
831
  Env.add_value env fcn.fun_id ck_node
832

    
833
let clock_top_consts env clist =
834
  List.fold_left (fun env cdecl ->
835
    let ck = new_var false in
836
    try_generalize ck cdecl.const_loc;
837
    Env.add_value env cdecl.const_id ck) env clist
838

    
839
let clock_top_decl env decl =
840
  match decl.top_decl_desc with
841
  | Node nd ->
842
    clock_node env decl.top_decl_loc nd
843
  | ImportedNode nd ->
844
    clock_imported_node env decl.top_decl_loc nd
845
  | ImportedFun fcn ->
846
    clock_function env decl.top_decl_loc fcn
847
  | Consts clist ->
848
    clock_top_consts env clist
849
  | Open _ ->
850
    env
851

    
852
let clock_prog env decls =
853
  List.fold_left (fun e decl -> clock_top_decl e decl) env decls
854

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

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

    
870
let uneval_node_generics vdecls =
871
  List.iter uneval_vdecl_generics vdecls
872

    
873
let uneval_top_generics decl =
874
  match decl.top_decl_desc with
875
  | Node nd ->
876
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
877
  | ImportedNode nd ->
878
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
879
  | ImportedFun nd ->
880
      ()
881
  | Consts clist -> ()
882
  | Open _  -> ()
883

    
884
let uneval_prog_generics prog =
885
 List.iter uneval_top_generics prog
886

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