Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / clocks.ml @ b1a97ade

History | View | Annotate | Download (19.3 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
(** Clocks definitions and a few utility functions on clocks. *)
24
open Utils
25
open Format
26

    
27
(* Clock type sets, for subtyping. *)
28
type clock_set =
29
    CSet_all
30
  | CSet_pck of int*rat
31

    
32
(* Clock carriers basically correspond to the "c" in "x when c" *)
33
type carrier_desc =
34
  | Carry_const of ident
35
  | Carry_name
36
  | Carry_var
37
  | Carry_link of carrier_expr
38

    
39
(* Carriers are scoped, to detect clock extrusion. In other words, we
40
   check the scope of a clock carrier before generalizing it. *)
41
and carrier_expr =
42
    {mutable carrier_desc: carrier_desc;
43
     mutable carrier_scoped: bool;
44
     carrier_id: int}
45

    
46
type clock_expr =
47
    {mutable cdesc: clock_desc;
48
     mutable cscoped: bool;
49
     cid: int}
50

    
51
(* pck stands for periodic clock. Easier not to separate pck from other clocks *)
52
and clock_desc =
53
  | Carrow of clock_expr * clock_expr
54
  | Ctuple of clock_expr list
55
  | Con of clock_expr * carrier_expr * ident
56
  | Pck_up of clock_expr * int
57
  | Pck_down of clock_expr * int
58
  | Pck_phase of clock_expr * rat
59
  | Pck_const of int * rat
60
  | Cvar of clock_set (* Monomorphic clock variable *)
61
  | Cunivar of clock_set (* Polymorphic clock variable *)
62
  | Clink of clock_expr (* During unification, make links instead of substitutions *)
63
  | Ccarrying of carrier_expr * clock_expr
64

    
65
type error =
66
  | Clock_clash of clock_expr * clock_expr
67
  | Not_pck
68
  | Clock_set_mismatch of clock_expr * clock_set
69
  | Cannot_be_polymorphic of clock_expr
70
  | Invalid_imported_clock of clock_expr
71
  | Invalid_const of clock_expr
72
  | Factor_zero
73
  | Carrier_mismatch of carrier_expr * carrier_expr
74
  | Carrier_extrusion of clock_expr * carrier_expr
75
  | Clock_extrusion of clock_expr * clock_expr
76

    
77
exception Unify of clock_expr * clock_expr
78
exception Subsume of clock_expr * clock_set
79
exception Mismatch of carrier_expr * carrier_expr
80
exception Scope_carrier of carrier_expr
81
exception Scope_clock of clock_expr
82
exception Error of Location.t * error
83

    
84
let new_id = ref (-1)
85

    
86
let new_ck desc scoped =
87
  incr new_id; {cdesc=desc; cid = !new_id; cscoped = scoped}
88

    
89
let new_var scoped =
90
  new_ck (Cvar CSet_all) scoped
91

    
92
let new_univar () =
93
  new_ck (Cunivar CSet_all) false
94

    
95
let new_carrier_id = ref (-1)
96

    
97
let new_carrier desc scoped =
98
  incr new_carrier_id; {carrier_desc = desc;
99
                        carrier_id = !new_carrier_id;
100
                        carrier_scoped = scoped}
101

    
102
let new_carrier_name () =
103
  new_carrier Carry_name true
104

    
105
let rec repr =
106
  function
107
      {cdesc=Clink ck'} ->
108
        repr ck'
109
    | ck -> ck
110

    
111
let rec carrier_repr =
112
  function {carrier_desc = Carry_link cr'} -> carrier_repr cr'
113
    | cr -> cr
114

    
115
(** Splits [ck] into the [lhs,rhs] of an arrow clock. Expects an arrow clock
116
    (ensured by language syntax) *)
117
let split_arrow ck =
118
  match (repr ck).cdesc with
119
  | Carrow (cin,cout) -> cin,cout
120
    (* Functions are not first order, I don't think the var case
121
       needs to be considered here *)
122
  | _ -> failwith "Internal error: not an arrow clock"
123

    
124
let get_carrier_name ck =
125
 match (repr ck).cdesc with
126
 | Ccarrying (cr, _) -> Some cr
127
 | _                 -> None
128

    
129
let uncarrier ck =
130
 match ck.cdesc with
131
 | Ccarrying (_, ck') -> ck'
132
 | _                  -> ck
133

    
134
(* Removes all links in a clock. Only used for clocks
135
   simplification though. *)
136
let rec deep_repr ck =
137
  match ck.cdesc with
138
  | Carrow (ck1,ck2) ->
139
      new_ck (Carrow (deep_repr ck1, deep_repr ck2)) ck.cscoped
140
  | Ctuple cl ->
141
      new_ck (Ctuple (List.map deep_repr cl)) ck.cscoped
142
  | Con (ck', c, l) ->
143
      new_ck (Con (deep_repr ck', c, l)) ck.cscoped
144
  | Pck_up (ck',k) ->
145
      new_ck (Pck_up (deep_repr ck',k)) ck.cscoped
146
  | Pck_down (ck',k) ->
147
      new_ck (Pck_down (deep_repr ck',k)) ck.cscoped
148
  | Pck_phase (ck',q) ->
149
      new_ck (Pck_phase (deep_repr ck',q)) ck.cscoped
150
  | Pck_const (_,_) | Cvar _ | Cunivar _ -> ck
151
  | Clink ck' -> deep_repr ck'
152
  | Ccarrying (cr,ck') -> new_ck (Ccarrying (cr, deep_repr ck')) ck.cscoped
153

    
154
(** Splits ck into the [lhs,rhs] of an arrow clock. Expects an arrow clock
155
    (ensured by language syntax) *)
156
let split_arrow ck =
157
  match (repr ck).cdesc with
158
  | Carrow (cin,cout) -> cin,cout
159
  | _ -> failwith "Internal error: not an arrow clock"
160

    
161
(** Returns the clock corresponding to a clock list. *)
162
let clock_of_clock_list ckl =
163
  if (List.length ckl) > 1 then
164
    new_ck (Ctuple ckl) true
165
  else
166
    List.hd ckl
167

    
168
let clock_list_of_clock ck =
169
 match (repr ck).cdesc with
170
 | Ctuple cl -> cl
171
 | _         -> [ck]
172

    
173
let clock_of_impnode_clock ck =
174
  let ck = repr ck in
175
  match ck.cdesc with
176
  | Carrow _ | Clink _ | Cvar _ | Cunivar _ ->
177
      failwith "internal error clock_of_impnode_clock"
178
  | Ctuple cklist -> List.hd cklist
179
  | Con (_,_,_) | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_)
180
  | Pck_const (_,_) | Ccarrying (_,_) -> ck
181

    
182
(** [intersect set1 set2] returns the intersection of clock subsets
183
    [set1] and [set2]. *)
184
let intersect set1 set2 =
185
  match set1,set2 with
186
  | CSet_all,_ -> set2
187
  | _,CSet_all -> set1
188
  | CSet_pck (k,q), CSet_pck (k',q') ->
189
      let k'',q'' = lcm k k',max_rat q q' in
190
      CSet_pck (k'',q'')
191

    
192
(** [can_be_pck ck] returns true if [ck] "may be" a pclock (the uncertainty is
193
    due to clock variables) *)
194
let rec can_be_pck ck =
195
  match (repr ck).cdesc with
196
  | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) | Pck_const (_,_)
197
  | Cvar _ | Cunivar _ ->
198
      true
199
  | Ccarrying (_,ck') -> can_be_pck ck
200
  | _ -> false
201

    
202
(** [is_concrete_pck ck] returns true if [ck] is a concrete [pck] (pck
203
    transformations applied to a pck constant) *)
204
let rec is_concrete_pck ck =
205
  match ck.cdesc with
206
  | Carrow (_,_) | Ctuple _ | Con (_,_,_)
207
  | Cvar _ | Cunivar _ -> false
208
  | Pck_up (ck',_) | Pck_down (ck',_) -> is_concrete_pck ck'
209
  | Pck_phase (ck',_) -> is_concrete_pck ck'
210
  | Pck_const (_,_) -> true
211
  | Clink ck' -> is_concrete_pck ck'
212
  | Ccarrying (_,ck') -> false
213

    
214
(** [is_polymorphic ck] returns true if [ck] is polymorphic. *)
215
let rec is_polymorphic ck =
216
  match ck.cdesc with
217
  | Cvar _ | Pck_const (_,_) -> false
218
  | Carrow (ck1,ck2) -> (is_polymorphic ck1) || (is_polymorphic ck2)
219
  | Ctuple ckl -> List.exists (fun c -> is_polymorphic c) ckl
220
  | Con (ck',_,_) -> is_polymorphic ck'
221
  | Pck_up (ck',_) | Pck_down (ck',_) -> is_polymorphic ck'
222
  | Pck_phase (ck',_) -> is_polymorphic ck'
223
  | Cunivar _ -> true
224
  | Clink ck' -> is_polymorphic ck'
225
  | Ccarrying (_,ck') -> is_polymorphic ck'
226

    
227
(** [constrained_vars_of_clock ck] returns the clock variables subject
228
    to sub-typing constraints appearing in clock [ck]. Removes duplicates *)
229
(* Used mainly for debug, non-linear complexity. *)
230
let rec constrained_vars_of_clock ck =
231
  let rec aux vars ck =
232
    match ck.cdesc with
233
    | Pck_const (_,_) ->
234
        vars
235
    | Cvar cset ->
236
        begin
237
          match cset with
238
          | CSet_all -> vars
239
          | _ ->
240
              list_union [ck] vars
241
        end
242
    | Carrow (ck1,ck2) ->
243
        let l = aux vars ck1 in
244
        aux l ck2
245
    | Ctuple ckl ->
246
        List.fold_left
247
          (fun acc ck' -> aux acc ck') 
248
          vars ckl
249
    | Con (ck',_,_) -> aux vars ck'
250
    | Pck_up (ck',_) | Pck_down (ck',_) -> aux vars ck'
251
    | Pck_phase (ck',_) -> aux vars ck'
252
    | Cunivar cset ->
253
        begin
254
          match cset with
255
          | CSet_all -> vars
256
          | _ -> list_union [ck] vars
257
        end
258
    | Clink ck' -> aux vars ck'
259
    | Ccarrying (_,ck') -> aux vars ck'
260
  in
261
  aux [] ck
262

    
263
let print_ckset fmt s =
264
  match s with
265
  | CSet_all -> ()
266
  | CSet_pck (k,q) ->
267
      let (a,b) = simplify_rat q in
268
      if k = 1 && a = 0 then
269
        fprintf fmt "<:P"
270
      else
271
        fprintf fmt "<:P_(%i,%a)" k print_rat (a,b)
272

    
273
let rec print_carrier fmt cr =
274
 (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
275
  match cr.carrier_desc with
276
  | Carry_const id -> fprintf fmt "%s" id
277
  | Carry_name ->
278
      fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
279
  | Carry_var ->
280
    fprintf fmt "'%s" (name_of_carrier cr.carrier_id)
281
  | Carry_link cr' ->
282
    print_carrier fmt cr'
283

    
284
(* Simple pretty-printing, performs no simplifications. Linear
285
   complexity. For debug mainly. *)
286
let rec print_ck_long fmt ck =
287
  match ck.cdesc with
288
  | Carrow (ck1,ck2) ->
289
      fprintf fmt "%a->%a" print_ck_long ck1 print_ck_long ck2
290
  | Ctuple cklist ->
291
    fprintf fmt "(%a)"
292
      (fprintf_list ~sep:" * " print_ck_long) cklist
293
  | Con (ck,c,l) ->
294
    fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
295
  | Pck_up (ck,k) ->
296
    fprintf fmt "%a*^%i" print_ck_long ck k
297
  | Pck_down (ck,k) ->
298
    fprintf fmt "%a/^%i" print_ck_long ck k
299
  | Pck_phase (ck,q) ->
300
    fprintf fmt "%a~>%a" print_ck_long ck print_rat (simplify_rat q)
301
  | Pck_const (n,p) ->
302
    fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
303
  | Cvar cset ->
304
    fprintf fmt "'_%i%a" ck.cid print_ckset cset
305
  | Cunivar cset ->
306
    fprintf fmt "'%i%a" ck.cid print_ckset cset
307
  | Clink ck' ->
308
    fprintf fmt "link %a" print_ck_long ck'
309
  | Ccarrying (cr,ck') ->
310
    fprintf fmt "(%a:%a)" print_carrier cr print_ck_long ck'
311

    
312
(** [period ck] returns the period of [ck]. Expects a constant pclock
313
    expression belonging to the correct clock set. *)
314
let rec period ck =
315
  let rec aux ck =
316
    match ck.cdesc with
317
    | Carrow (_,_) | Ctuple _ | Con (_,_,_)
318
    | Cvar _ | Cunivar _ ->
319
        failwith "internal error: can only compute period of const pck"
320
    | Pck_up (ck',k) ->
321
        (aux ck')/.(float_of_int k)
322
    | Pck_down (ck',k) ->
323
        (float_of_int k)*.(aux ck')
324
    | Pck_phase (ck',_) ->
325
        aux ck'
326
    | Pck_const (n,_) ->
327
        float_of_int n
328
    | Clink ck' -> aux ck'
329
    | Ccarrying (_,ck') -> aux ck'
330
  in
331
  int_of_float (aux ck)
332

    
333
(** [phase ck] returns the phase of [ck]. It is not expressed as a
334
    fraction of the period, but instead as an amount of time. Expects a
335
    constant expression belonging to the correct P_k *)
336
let phase ck =
337
  let rec aux ck =
338
  match ck.cdesc with
339
  | Carrow (_,_) | Ctuple _ | Con (_,_,_)
340
  | Cvar _ | Cunivar _ ->
341
      failwith "internal error: can only compute phase of const pck"
342
  | Pck_up (ck',_) ->
343
      aux ck'
344
  | Pck_down (ck',k) ->
345
      aux ck'
346
  | Pck_phase (ck',(a,b)) ->
347
      let n = period ck' in
348
      let (a',b') = aux ck' in
349
      sum_rat (a',b') (n*a,b)
350
  | Pck_const (n,(a,b)) ->
351
      (n*a,b)
352
  | Clink ck' -> aux ck'
353
  | Ccarrying (_,ck') -> aux ck'
354
  in
355
  let (a,b) = aux ck in
356
  simplify_rat (a,b)
357

    
358
let eq_carrier cr1 cr2 =
359
  match (carrier_repr cr1).carrier_desc, (carrier_repr cr2).carrier_desc with
360
 | Carry_const id1, Carry_const id2 -> id1 = id2
361
 | _                                -> cr1.carrier_id = cr2.carrier_id
362

    
363
(* Returns the clock root of a clock *)
364
let rec root ck =
365
  match (repr ck).cdesc with
366
  | Con (ck',_,_) | Clink ck' | Ccarrying (_,ck') ->
367
      root ck'
368
  | Pck_up _ | Pck_down _ | Pck_phase _ | Pck_const _ | Cvar _ | Cunivar _ -> ck
369
  | Carrow _ | Ctuple _ -> failwith "Internal error pclock_parent"
370

    
371
(* Returns the branch of clock [ck] in its clock tree *)
372
let rec branch ck =
373
  let rec branch ck acc =
374
    match (repr ck).cdesc with
375
    | Ccarrying (_, ck) -> branch ck acc
376
    | Con (ck, cr, l)   -> branch ck ((cr, l) :: acc)
377
    | Ctuple _
378
    | Carrow _          -> assert false
379
    | _                 -> acc
380
  in branch ck [];;
381

    
382
(* Tests whether clock branches [br1] nd [br2] are statically disjoint *)
383
let rec disjoint_branches br1 br2 =
384
 match br1, br2 with
385
 | []          , _
386
 | _           , []           -> false
387
 | (cr1,l1)::q1, (cr2,l2)::q2 -> eq_carrier cr1 cr2 && ((l1 <> l2) || disjoint_branches q1 q2);;
388

    
389
(* Disjunction relation between variables based upon their static clocks. *)
390
let disjoint ck1 ck2 =
391
 root ck1 = root ck2 && disjoint_branches (branch ck1) (branch ck2);;
392

    
393
(** [normalize pck] returns the normal form of clock [pck]. *)
394
let normalize pck =
395
  let changed = ref true in
396
  let rec aux pck =
397
    match pck.cdesc with
398
    | Pck_up ({cdesc=Pck_up (pck',k')},k) ->
399
        changed:=true;
400
        new_ck (Pck_up (aux pck',k*k')) pck.cscoped
401
    | Pck_up ({cdesc=Pck_down (pck',k')},k) ->
402
        changed:=true;
403
        new_ck (Pck_down (new_ck (Pck_up (aux pck',k)) pck.cscoped,k')) pck.cscoped
404
    | Pck_up ({cdesc=Pck_phase (pck',(a,b))},k) ->
405
        changed:=true;
406
        new_ck (Pck_phase (new_ck (Pck_up (aux pck',k)) pck.cscoped,(a*k,b))) pck.cscoped
407
    | Pck_down ({cdesc=Pck_down (pck',k')},k) ->
408
        changed:=true;
409
        new_ck (Pck_down (aux pck',k*k')) pck.cscoped
410
    | Pck_down ({cdesc=Pck_phase (pck',(a,b))},k) ->
411
        changed:=true;
412
        new_ck (Pck_phase (new_ck (Pck_down (aux pck',k)) pck.cscoped,(a,b*k))) pck.cscoped
413
    | Pck_phase ({cdesc=Pck_phase (pck',(a',b'))},(a,b)) ->
414
        changed:=true;
415
        let (a'',b'') = sum_rat (a,b) (a',b') in
416
        new_ck (Pck_phase (aux pck',(a'',b''))) pck.cscoped
417
    | Pck_up (pck',k') ->
418
        new_ck (Pck_up (aux pck',k')) pck.cscoped
419
    | Pck_down (pck',k') ->
420
        new_ck (Pck_down (aux pck',k')) pck.cscoped
421
    | Pck_phase (pck',k') ->
422
        new_ck (Pck_phase (aux pck',k')) pck.cscoped
423
    | Ccarrying (cr,ck') ->
424
        new_ck (Ccarrying (cr, aux ck')) pck.cscoped
425
    | _ -> pck
426
  in
427
  let nf=ref pck in
428
  while !changed do
429
    changed:=false;
430
    nf:=aux !nf
431
  done;
432
  !nf
433

    
434
(** [canonize pck] reduces transformations of [pck] and removes
435
    identity transformations. Expects a normalized periodic clock ! *)
436
let canonize pck =
437
  let rec remove_id_trans pck =
438
    match pck.cdesc with
439
    | Pck_up (pck',1) | Pck_down (pck',1) | Pck_phase (pck',(0,_)) ->
440
        remove_id_trans pck'
441
    | _ -> pck
442
  in
443
  let pck =
444
    match pck.cdesc with
445
    | Pck_phase ({cdesc=Pck_down ({cdesc=Pck_up (v,k)},k')},k'') ->
446
        let gcd = gcd k k' in
447
        new_ck (Pck_phase
448
                  (new_ck (Pck_down
449
                             (new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd))
450
                     pck.cscoped,k''))
451
          pck.cscoped
452
    | Pck_down ({cdesc=Pck_up (v,k)},k') ->
453
        let gcd = gcd k k' in
454
        new_ck (Pck_down (new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd)) pck.cscoped
455
    | _ -> pck
456
  in
457
  remove_id_trans pck
458

    
459
(** [simplify pck] applies pclocks simplifications to [pck] *)
460
let simplify pck =
461
  if (is_concrete_pck pck) then
462
    let n = period pck in
463
    let (a,b) = phase pck in
464
    let phase' = simplify_rat (a,b*n) in 
465
    new_ck (Pck_const (n,phase')) pck.cscoped
466
  else
467
    let pck' = deep_repr pck in
468
    let nf_pck = normalize pck' in
469
    canonize nf_pck
470
        
471
let print_cvar fmt cvar =
472
  match cvar.cdesc with
473
  | Cvar cset ->
474
 (*
475
      if cvar.cscoped
476
      then
477
	fprintf fmt "[_%s%a]"
478
	  (name_of_type cvar.cid)
479
	  print_ckset cset
480
      else
481
 *)
482
	fprintf fmt "_%s%a"
483
	  (name_of_type cvar.cid)
484
	  print_ckset cset
485
  | Cunivar cset ->
486
 (*
487
      if cvar.cscoped
488
      then
489
	fprintf fmt "['%s%a]"
490
	  (name_of_type cvar.cid)
491
	  print_ckset cset
492
      else
493
 *)
494
	fprintf fmt "'%s%a"
495
	  (name_of_type cvar.cid)
496
	  print_ckset cset
497
  | _ -> failwith "Internal error print_cvar"
498

    
499
(* Nice pretty-printing. Simplifies expressions before printing them. Non-linear
500
   complexity. *)
501
let print_ck fmt ck =
502
  let rec aux fmt ck =
503
    let ck = simplify ck in
504
    match ck.cdesc with
505
    | Carrow (ck1,ck2) ->
506
      fprintf fmt "%a->%a" aux ck1 aux ck2
507
    | Ctuple cklist ->
508
      fprintf fmt "(%a)" 
509
	(fprintf_list ~sep:" * " aux) cklist
510
    | Con (ck,c,l) ->
511
      fprintf fmt "%a on %s(%a)" aux ck l print_carrier c
512
    | Pck_up (ck,k) ->
513
      fprintf fmt "%a*.%i" aux ck k
514
    | Pck_down (ck,k) ->
515
      fprintf fmt "%a/.%i" aux ck k
516
    | Pck_phase (ck,q) ->
517
      fprintf fmt "%a->.%a" aux ck print_rat (simplify_rat q)
518
    | Pck_const (n,p) ->
519
      fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
520
    | Cvar cset ->
521
(*
522
      if ck.cscoped
523
      then
524
        fprintf fmt "[_%s]" (name_of_type ck.cid)
525
      else
526
*)
527
	fprintf fmt "_%s" (name_of_type ck.cid)
528
    | Cunivar cset ->
529
(*
530
      if ck.cscoped
531
      then
532
        fprintf fmt "['%s]" (name_of_type ck.cid)
533
      else
534
*)
535
        fprintf fmt "'%s" (name_of_type ck.cid)
536
    | Clink ck' ->
537
        aux fmt ck'
538
    | Ccarrying (cr,ck') ->
539
      fprintf fmt "(%a:%a)" print_carrier cr aux ck'
540
  in
541
  let cvars = constrained_vars_of_clock ck in
542
  aux fmt ck;
543
  if cvars <> [] then
544
    fprintf fmt " (where %a)"
545
      (fprintf_list ~sep:", " print_cvar) cvars
546

    
547
(* prints only the Con components of a clock, useful for printing nodes *)
548
let rec print_ck_suffix fmt ck =
549
  let ck = simplify ck in
550
  match ck.cdesc with
551
  | Carrow _
552
  | Ctuple _
553
  | Cvar _
554
  | Cunivar _   -> ()
555
  | Con (ck,c,l) ->
556
    fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c
557
  | Clink ck' ->
558
    print_ck_suffix fmt ck'
559
  | Ccarrying (cr,ck') ->
560
    fprintf fmt "%a" print_ck_suffix ck'
561
  | _ -> assert false
562

    
563
let pp_error fmt = function
564
  | Clock_clash (ck1,ck2) ->
565
      reset_names ();
566
      fprintf fmt "Expected clock %a, got clock %a@."
567
      print_ck ck1
568
      print_ck ck2
569
  | Not_pck ->
570
    fprintf fmt "The clock of this expression must be periodic@."
571
  | Carrier_mismatch (cr1, cr2) ->
572
     fprintf fmt "Name clash. Expected clock %a, got clock %a@."
573
       print_carrier cr1
574
       print_carrier cr2
575
  | Clock_set_mismatch (ck,cset) ->
576
      reset_names ();
577
    fprintf fmt "Clock %a is not included in clock set %a@."
578
      print_ck ck
579
      print_ckset cset
580
  | Cannot_be_polymorphic ck ->
581
      reset_names ();
582
    fprintf fmt "The main node cannot have a polymorphic clock: %a@."
583
      print_ck ck
584
  | Invalid_imported_clock ck ->
585
      reset_names ();
586
    fprintf fmt "Not a valid imported node clock: %a@."
587
      print_ck ck
588
  | Invalid_const ck ->
589
      reset_names ();
590
    fprintf fmt "Clock %a is not a valid periodic clock@."
591
      print_ck ck;
592
  | Factor_zero ->
593
    fprintf fmt "Cannot apply clock transformation with factor 0@."
594
  | Carrier_extrusion (ck,cr) ->
595
    fprintf fmt "This node has clock@.%a@.It is invalid as %a escapes its scope@."
596
      print_ck ck
597
      print_carrier cr
598
  | Clock_extrusion (ck_node,ck) ->
599
    fprintf fmt "This node has clock@.%a@.It is invalid as %a escapes its scope@."
600
      print_ck ck_node
601
      print_ck ck
602

    
603
let const_of_carrier cr =
604
 match (carrier_repr cr).carrier_desc with
605
 | Carry_const id -> id
606
 | Carry_name
607
 | Carry_var
608
 | Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
609
 
610
let uneval const cr =
611
  (*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*)
612
  let cr = carrier_repr cr in
613
  match cr.carrier_desc with
614
  | Carry_var -> cr.carrier_desc <- Carry_const const
615
  | Carry_name -> cr.carrier_desc <- Carry_const const
616
  | _         -> assert false
617

    
618
(* Local Variables: *)
619
(* compile-command:"make -C .." *)
620
(* End: *)