Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / clock_calculus.ml @ 8b3afe43

History | View | Annotate | Download (26.7 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
(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify
257
    (ck1,ck2)] if the clocks are not unifiable.*)
258
let rec unify ck1 ck2 =
259
  let ck1 = repr ck1 in
260
  let ck2 = repr ck2 in
261
  if ck1=ck2 then
262
    ()
263
  else
264
    let left_const = is_concrete_pck ck1 in
265
    let right_const = is_concrete_pck ck2 in
266
    if left_const && right_const then
267
      unify_static_pck ck1 ck2
268
    else
269
      match ck1.cdesc,ck2.cdesc with
270
      | Cvar cset1,Cvar cset2->
271
          if ck1.cid < ck2.cid then
272
            begin
273
              ck2.cdesc <- Clink (simplify ck1);
274
              update_scope ck2.cscoped ck1;
275
              subsume ck1 cset2
276
            end
277
          else
278
            begin
279
              ck1.cdesc <- Clink (simplify ck2);
280
              update_scope ck1.cscoped ck2;
281
              subsume ck2 cset1
282
            end
283
      | Cvar cset, Pck_up (_,_) | Cvar cset, Pck_down (_,_)
284
      | Cvar cset, Pck_phase (_,_) | Cvar cset, Pck_const (_,_) ->
285
          if (occurs ck1 ck2) then
286
            begin
287
              if (simplify ck2 = ck1) then
288
                ck2.cdesc <- Clink (simplify ck1)
289
              else
290
                raise (Unify (ck1,ck2));
291
              end
292
          else
293
            begin
294
              ck1.cdesc <- Clink (simplify ck2);
295
              subsume ck2 cset
296
            end
297
      | Pck_up (_,_), Cvar cset | Pck_down (_,_), Cvar cset
298
      | Pck_phase (_,_), Cvar cset | Pck_const (_,_), Cvar cset ->
299
            if (occurs ck2 ck1) then
300
              begin
301
                if ((simplify ck1) = ck2) then
302
                  ck1.cdesc <- Clink (simplify ck2)
303
                else
304
                  raise (Unify (ck1,ck2));
305
              end
306
            else
307
              begin
308
                ck2.cdesc <- Clink (simplify ck1);
309
                subsume ck1 cset
310
              end
311
      | (Cvar cset,_) when (not (occurs ck1 ck2)) ->
312
          subsume ck2 cset;
313
          update_scope ck1.cscoped ck2;
314
          ck1.cdesc <- Clink (simplify ck2)
315
      | (_, (Cvar cset)) when (not (occurs ck2 ck1)) ->
316
          subsume ck1 cset;
317
          update_scope ck2.cscoped ck1;
318
          ck2.cdesc <- Clink (simplify ck1)
319
      | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
320
          unify_carrier cr1 cr2;
321
          unify ck1' ck2'
322
      | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->
323
          raise (Unify (ck1,ck2))
324
      | Carrow (c1,c2), Carrow (c1',c2') ->
325
          unify c1 c1'; unify c2 c2'
326
      | Ctuple ckl1, Ctuple ckl2 ->
327
          if (List.length ckl1) <> (List.length ckl2) then
328
            raise (Unify (ck1,ck2));
329
          List.iter2 unify ckl1 ckl2
330
      | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
331
          unify_carrier c1 c2;
332
          unify ck' ck''
333
      | Pck_const (i,r), Pck_const (i',r') ->
334
          if i<>i' || r <> r' then
335
            raise (Unify (ck1,ck2))
336
      | (_, Pck_up (pck2',k)) when (not right_const) ->
337
          let ck1' = simplify (new_ck (Pck_down (ck1,k)) true) in
338
          unify ck1' pck2'
339
      | (_,Pck_down (pck2',k)) when (not right_const) ->
340
          subsume ck1 (CSet_pck (k,(0,1)));
341
          let ck1' = simplify (new_ck (Pck_up (ck1,k)) true) in
342
          unify ck1' pck2'
343
      | (_,Pck_phase (pck2',(a,b))) when (not right_const) ->
344
          subsume ck1 (CSet_pck (b,(a,b)));
345
          let ck1' = simplify (new_ck (Pck_phase (ck1,(-a,b))) true) in
346
          unify ck1' pck2'
347
      | Pck_up (pck1',k),_ ->
348
          let ck2' = simplify (new_ck (Pck_down (ck2,k)) true) in
349
          unify pck1' ck2'
350
      | Pck_down (pck1',k),_ ->
351
          subsume ck2 (CSet_pck (k,(0,1)));
352
          let ck2' = simplify (new_ck (Pck_up (ck2,k)) true) in
353
          unify pck1' ck2'
354
      | Pck_phase (pck1',(a,b)),_ ->
355
          subsume ck2 (CSet_pck (b,(a,b)));
356
          let ck2' = simplify (new_ck (Pck_phase (ck2,(-a,b))) true) in
357
          unify pck1' ck2'
358
      (* Corner case for some functions like ite, need to unify guard clock
359
	 with output clocks *)
360
(*
361
      | Ctuple ckl, (Cvar _) -> List.iter (unify ck2) ckl
362
      | (Cvar _), Ctuple ckl ->	List.iter (unify ck1) ckl
363
*)
364
      | Cunivar _, _ | _, Cunivar _ -> ()
365
      | _,_ -> raise (Unify (ck1,ck2))
366

    
367
(* Returns the value corresponding to a pclock (integer) factor
368
   expression. Expects a constant expression (checked by typing). *)
369
let int_factor_of_expr e =
370
  match e.expr_desc with 
371
  | Expr_const
372
      (Const_int i) -> i
373
  | _ -> failwith "Internal error: int_factor_of_expr"
374

    
375
(* Unifies all the clock variables in the clock type of a tuple 
376
   expression, so that the clock type only uses at most one clock variable *)
377
let unify_tuple_clock ref_ck_opt ck =
378
  let ck_var = ref ref_ck_opt in
379
  let rec aux ck =
380
    match (repr ck).cdesc with
381
    | Con _
382
    | Cvar _ ->
383
        begin
384
          match !ck_var with
385
          | None ->
386
              ck_var:=Some ck
387
          | Some v ->
388
              (* may fail *)
389
              unify v ck
390
        end
391
    | Ctuple cl ->
392
        List.iter aux cl
393
    | Carrow _ -> assert false (* should not occur *)
394
    | Ccarrying (_, ck1) ->
395
        aux ck1
396
    | _ -> ()
397
  in
398
  aux ck
399

    
400
(* Unifies all the clock variables in the clock type of an imported
401
   node, so that the clock type only uses at most one base clock variable,
402
   that is, the activation clock of the node *)
403
let unify_imported_clock ref_ck_opt ck =
404
  let ck_var = ref ref_ck_opt in
405
  let rec aux ck =
406
    match (repr ck).cdesc with
407
    | Cvar _ ->
408
        begin
409
          match !ck_var with
410
          | None ->
411
              ck_var:=Some ck
412
          | Some v ->
413
              (* cannot fail *)
414
              unify v ck
415
        end
416
    | Ctuple cl ->
417
        List.iter aux cl
418
    | Carrow (ck1,ck2) ->
419
        aux ck1; aux ck2
420
    | Ccarrying (_, ck1) ->
421
        aux ck1
422
    | Con (ck1, _, _) -> aux ck1
423
    | _ -> ()
424
  in
425
  aux ck
426

    
427
(** [clock_uncarry ck] drops the possible carrier name from clock [ck] *)
428
let clock_uncarry ck =
429
  let ck = repr ck in
430
  match ck.cdesc with
431
  | Ccarrying (_, ck') -> ck'
432
  | _                  -> ck
433

    
434
let try_unify ck1 ck2 loc =
435
  try
436
    unify ck1 ck2
437
  with
438
  | Unify (ck1',ck2') ->
439
    raise (Error (loc, Clock_clash (ck1',ck2')))
440
  | Subsume (ck,cset) ->
441
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
442
  | Mismatch (cr1,cr2) ->
443
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
444

    
445
(* Checks whether ck1 is a subtype of ck2 *)
446
let rec clock_subtyping ck1 ck2 =
447
  match (repr ck1).cdesc, (repr ck2).cdesc with
448
  | Ccarrying _         , Ccarrying _ -> unify ck1 ck2
449
  | Ccarrying (cr', ck'), _           -> unify ck' ck2
450
  | _                                 -> unify ck1 ck2
451

    
452
(* Clocks a list of arguments of Lustre builtin operators:
453
   - type each expression, remove carriers of clocks as
454
     carriers may only denote variables, not arbitrary expr.
455
   - try to unify these clocks altogether
456
*)
457
let rec clock_standard_args env expr_list =
458
  let ck_list = List.map (fun e -> clock_uncarry (clock_expr env e)) expr_list in
459
  let ck_res = new_var true in
460
  List.iter2 (fun e ck -> try_unify ck ck_res e.expr_loc) expr_list ck_list;
461
  ck_res
462

    
463
(* emulates a subtyping relation between clocks c and (cr : c),
464
   used during node application only *)
465
and clock_subtyping_arg env real_arg formal_clock =
466
  let loc = real_arg.expr_loc in
467
  let real_clock = clock_expr env real_arg in
468
  try
469
    clock_subtyping real_clock formal_clock
470
  with
471
  | Unify (ck1',ck2') ->
472
    raise (Error (loc, Clock_clash (real_clock, formal_clock)))
473
  | Subsume (ck,cset) ->
474
    raise (Error (loc, Clock_set_mismatch (ck, cset)))
475
  | Mismatch (cr1,cr2) ->
476
    raise (Error (loc, Carrier_mismatch (cr1, cr2)))
477

    
478
(* computes clocks for node application *)
479
and clock_appl env f args clock_reset loc =
480
  let cfun = clock_ident false env f loc in
481
  let cins, couts = split_arrow cfun in
482
  let cins = clock_list_of_clock cins in
483
  let args = expr_list_of_expr args in
484
  List.iter2 (clock_subtyping_arg env) args cins;
485
  unify_imported_clock (Some clock_reset) cfun;
486
  couts
487

    
488
and clock_ident nocarrier env id loc =
489
  clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc)
490

    
491
and clock_carrier env c loc ce =
492
  let expr_c = expr_of_ident c loc in
493
  let ck = clock_expr ~nocarrier:false env expr_c in
494
  let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in
495
  let ckcarry = new_ck (Ccarrying (cr,ce)) ck.cscoped in
496
  try_unify ck ckcarry expr_c.expr_loc;
497
  cr
498

    
499
(** [clock_expr env expr] performs the clock calculus for expression [expr] in
500
    environment [env] *)
501
and clock_expr ?(nocarrier=true) env expr =
502
  let resulting_ck = 
503
    match expr.expr_desc with
504
      | Expr_const cst ->
505
      let ck = new_var true in
506
      expr.expr_clock <- ck;
507
      ck
508
  | Expr_ident v ->
509
      let ckv =
510
        try
511
          Env.lookup_value env v
512
        with Not_found -> 
513
	  failwith ("Internal error, variable \""^v^"\" not found")
514
      in
515
      let ck = instantiate (ref []) (ref []) ckv in
516
      expr.expr_clock <- ck;
517
      ck
518
  | Expr_array elist ->
519
    let ck = clock_standard_args env elist in
520
    expr.expr_clock <- ck;
521
    ck
522
  | Expr_access (e1, d) ->
523
    (* dimension, being a static value, doesn't need to be clocked *)
524
    let ck = clock_standard_args env [e1] in
525
    expr.expr_clock <- ck;
526
    ck
527
  | Expr_power (e1, d) ->
528
    (* dimension, being a static value, doesn't need to be clocked *)
529
    let ck = clock_standard_args env [e1] in
530
    expr.expr_clock <- ck;
531
    ck
532
  | Expr_tuple elist ->
533
    let ck = new_ck (Ctuple (List.map (clock_expr env) elist)) true in
534
    expr.expr_clock <- ck;
535
    ck
536
  | Expr_ite (c, t, e) ->
537
    let ck_c = clock_standard_args env [c] in
538
    let ck = clock_standard_args env [t; e] in
539
    (* Here, the branches may exhibit a tuple clock, not the condition *)
540
    unify_tuple_clock (Some ck_c) ck;
541
    expr.expr_clock <- ck;
542
    ck
543
  | Expr_appl (id, args, r) ->
544
    (try
545
(* for a modular compilation scheme, all inputs/outputs must share the same clock !
546
   this is also the reset clock !
547
*)
548
    let cr =
549
      match r with
550
      | None        -> new_var true
551
      | Some (x, _) -> let loc_r = loc_of_cond expr.expr_loc x in
552
		       let expr_r = expr_of_ident x loc_r in
553
		       clock_expr env expr_r in
554
    let couts = clock_appl env id args cr expr.expr_loc in
555
    expr.expr_clock <- couts;
556
    couts
557
    with exn -> (
558
      Format.eprintf "Current expr: %a@." Printers.pp_expr expr; 
559
      raise exn
560
    ))
561
  | Expr_fby (e1,e2)
562
  | Expr_arrow (e1,e2) ->
563
    let ck = clock_standard_args env [e1; e2] in
564
    expr.expr_clock <- ck;
565
    ck
566
  | Expr_pre e -> (* todo : deal with phases as in tail ? *)
567
      let ck = clock_standard_args env [e] in
568
      expr.expr_clock <- ck;
569
      ck
570
  | Expr_when (e,c,l) ->
571
      let ce = clock_standard_args env [e] in
572
      let c_loc = loc_of_cond expr.expr_loc c in
573
      let cr = clock_carrier env c c_loc ce in
574
      let ck = new_ck (Con (ce,cr,l)) true in
575
      let cr' = new_carrier (Carry_const c) ck.cscoped in
576
      let ck' = new_ck (Con (ce,cr',l)) true in
577
      expr.expr_clock <- ck';
578
      ck
579
  | Expr_merge (c,hl) ->
580
      let cvar = new_var true in
581
      let cr = clock_carrier env c expr.expr_loc cvar in
582
      List.iter (fun (t, h) -> clock_subtyping_arg env h (new_ck (Con (cvar,cr,t)) true)) hl;
583
      expr.expr_clock <- cvar;
584
      cvar
585
  | Expr_uclock (e,k) ->
586
      let pck = clock_expr env e in
587
      if not (can_be_pck pck) then
588
        raise (Error (e.expr_loc, Not_pck));
589
      if k = 0 then
590
        raise (Error (expr.expr_loc, Factor_zero));
591
      (try
592
        subsume pck (CSet_pck (k,(0,1)))
593
      with Subsume (ck,cset) ->
594
        raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (k,(0,1))))));
595
      let ck = new_ck (Pck_up (pck,k)) true in
596
      expr.expr_clock <- ck;
597
      ck
598
  | Expr_dclock (e,k) ->
599
      let pck = clock_expr env e in
600
      if not (can_be_pck pck) then
601
        raise (Error (e.expr_loc, Not_pck));
602
      if k = 0 then
603
        raise (Error (expr.expr_loc, Factor_zero));
604
      (try
605
        subsume pck (CSet_pck (1,(0,1)))
606
      with Subsume (ck,cset) ->
607
        raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (1,(0,1))))));
608
      let ck = new_ck (Pck_down (pck,k)) true in
609
      expr.expr_clock <- ck;
610
      ck
611
  | Expr_phclock (e,(a,b)) ->
612
      let pck = clock_expr env e in
613
      if not (can_be_pck pck) then
614
        raise (Error (e.expr_loc, Not_pck));
615
      let (a,b) = simplify_rat (a,b) in
616
      (try
617
        subsume pck (CSet_pck (b,(0,1)))
618
      with Subsume (ck,cset) ->
619
        raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (b,(0,1))))));
620
      let ck = new_ck (Pck_phase (pck,(a,b))) true in
621
      expr.expr_clock <- ck;
622
      ck
623
  in
624
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck);
625
  resulting_ck
626

    
627
let clock_of_vlist vars =
628
  let ckl = List.map (fun v -> v.var_clock) vars in
629
  clock_of_clock_list ckl
630

    
631
(** [clock_eq env eq] performs the clock-calculus for equation [eq] in
632
    environment [env] *)
633
let clock_eq env eq =
634
  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
635
  let ck_rhs = clock_expr env eq.eq_rhs in
636
  clock_subtyping_arg env expr_lhs ck_rhs
637

    
638

    
639
(* [clock_coreclock cck] returns the clock_expr corresponding to clock
640
    declaration [cck] *)
641
let clock_coreclock env cck id loc scoped =
642
  match cck.ck_dec_desc with
643
  | Ckdec_any -> new_var scoped
644
  | Ckdec_pclock (n,(a,b)) ->
645
      let ck = new_ck (Pck_const (n,(a,b))) scoped in
646
      if n mod b <> 0 then raise (Error (loc,Invalid_const ck));
647
      ck
648
  | Ckdec_bool cl ->
649
      let temp_env = Env.add_value env id (new_var true) in
650
      (* We just want the id to be present in the environment *)
651
      let dummy_id_expr = expr_of_ident id loc in
652
      let when_expr =
653
        List.fold_left
654
          (fun expr (x,l) ->
655
                {expr_tag = new_tag ();
656
                 expr_desc = Expr_when (expr,x,l);
657
                 expr_type = Types.new_var ();
658
                 expr_clock = new_var scoped;
659
                 expr_delay = Delay.new_var ();
660
                 expr_loc = loc;
661
		 expr_annot = None})
662
          dummy_id_expr cl
663
      in
664
      clock_expr temp_env when_expr
665

    
666
(* Clocks a variable declaration *)
667
let clock_var_decl scoped env vdecl =
668
  let ck = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in
669
  let ck = 
670
    if vdecl.var_dec_const
671
    then
672
      (try_generalize ck vdecl.var_loc; ck)
673
    else
674
      match vdecl.var_type.Types.tdesc with
675
      | Types.Tclock _ -> new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped
676
      | _              -> ck in
677
  vdecl.var_clock <- ck;
678
  Env.add_value env vdecl.var_id ck
679

    
680
(* Clocks a variable declaration list *)
681
let clock_var_decl_list env scoped l =
682
  List.fold_left (clock_var_decl scoped) env l
683

    
684
(** [clock_node env nd] performs the clock-calculus for node [nd] in
685
    environment [env]. *)
686
let clock_node env loc nd =
687
  (* let is_main = nd.node_id = !Options.main_node in *)
688
  let new_env = clock_var_decl_list env false nd.node_inputs in
689
  let new_env = clock_var_decl_list new_env true nd.node_outputs in
690
  let new_env = clock_var_decl_list new_env true nd.node_locals in
691
  List.iter (clock_eq new_env) nd.node_eqs;
692
  let ck_ins = clock_of_vlist nd.node_inputs in
693
  let ck_outs = clock_of_vlist nd.node_outputs in
694
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
695
  unify_imported_clock None ck_node;
696
  (*Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);*)
697
  try_generalize ck_node loc;
698
  (* TODO : Xavier pourquoi ai je cette erreur ? *)
699
(*  if (is_main && is_polymorphic ck_node) then
700
    raise (Error (loc,(Cannot_be_polymorphic ck_node)));
701
*)
702
  nd.node_clock <- ck_node;
703
  Env.add_value env nd.node_id ck_node
704

    
705

    
706
let check_imported_pclocks loc ck_node =
707
  let pck = ref None in
708
  let rec aux ck =
709
    match ck.cdesc with
710
    | Carrow (ck1,ck2) -> aux ck1; aux ck2
711
    | Ctuple cl -> List.iter aux cl
712
    | Con (ck',_,_) -> aux ck'
713
    | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) -> 
714
        raise (Error (loc, (Invalid_imported_clock ck_node)))
715
    | Pck_const (n,p) ->
716
        begin
717
          match !pck with
718
          | None -> pck := Some (n,p)
719
          | Some (n',p') ->
720
              if (n,p) <> (n',p') then
721
                raise (Error (loc, (Invalid_imported_clock ck_node)))
722
        end
723
    | Clink ck' -> aux ck'
724
    | Ccarrying (_,ck') -> aux ck'
725
    | Cvar _ | Cunivar _ ->
726
        match !pck with
727
        | None -> ()
728
        | Some (_,_) ->
729
            raise (Error (loc, (Invalid_imported_clock ck_node)))
730
  in
731
  aux ck_node
732

    
733
let clock_imported_node env loc nd =
734
  let new_env = clock_var_decl_list env false nd.nodei_inputs in
735
  ignore(clock_var_decl_list new_env false nd.nodei_outputs);
736
  let ck_ins = clock_of_vlist nd.nodei_inputs in
737
  let ck_outs = clock_of_vlist nd.nodei_outputs in
738
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
739
  unify_imported_clock None ck_node;
740
  check_imported_pclocks loc ck_node;
741
  try_generalize ck_node loc;
742
  nd.nodei_clock <- ck_node;
743
  Env.add_value env nd.nodei_id ck_node
744

    
745
let clock_function env loc fcn =
746
  let new_env = clock_var_decl_list env false fcn.fun_inputs in
747
  ignore(clock_var_decl_list new_env false fcn.fun_outputs);
748
  let ck_ins = clock_of_vlist fcn.fun_inputs in
749
  let ck_outs = clock_of_vlist fcn.fun_outputs in
750
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
751
  unify_imported_clock None ck_node;
752
  check_imported_pclocks loc ck_node;
753
  try_generalize ck_node loc;
754
  Env.add_value env fcn.fun_id ck_node
755

    
756
let clock_top_consts env clist =
757
  List.fold_left (fun env cdecl ->
758
    let ck = new_var false in
759
    try_generalize ck cdecl.const_loc;
760
    Env.add_value env cdecl.const_id ck) env clist
761

    
762
let clock_top_decl env decl =
763
  match decl.top_decl_desc with
764
  | Node nd ->
765
    clock_node env decl.top_decl_loc nd
766
  | ImportedNode nd ->
767
    clock_imported_node env decl.top_decl_loc nd
768
  | ImportedFun fcn ->
769
    clock_function env decl.top_decl_loc fcn
770
  | Consts clist ->
771
    clock_top_consts env clist
772
  | Open _ ->
773
    env
774

    
775
let clock_prog env decls =
776
  List.fold_left (fun e decl -> clock_top_decl e decl) env decls
777

    
778
let check_env_compat header declared computed =
779
  Env.iter declared (fun k decl_clock_k -> 
780
    let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
781
    try_unify decl_clock_k computed_c Location.dummy_loc
782
  ) 
783
(* Local Variables: *)
784
(* compile-command:"make -C .." *)
785
(* End: *)