Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / clocks.ml @ 6a1a01d2

History | View | Annotate | Download (19.9 KB)

1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - LIFL             *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *) 
10
(*  This file was originally from the Prelude compiler              *)
11
(*                                                                  *) 
12
(********************************************************************)
13

    
14
(** Clocks definitions and a few utility functions on clocks. *)
15
open Utils
16
open Format
17

    
18
(* Clock type sets, for subtyping. *)
19
type clock_set =
20
    CSet_all
21
  | CSet_pck of int*rat
22

    
23
(* Clock carriers basically correspond to the "c" in "x when c" *)
24
type carrier_desc =
25
  | Carry_const of ident
26
  | Carry_name
27
  | Carry_var
28
  | Carry_link of carrier_expr
29

    
30
(* Carriers are scoped, to detect clock extrusion. In other words, we
31
   check the scope of a clock carrier before generalizing it. *)
32
and carrier_expr =
33
    {mutable carrier_desc: carrier_desc;
34
     mutable carrier_scoped: bool;
35
     carrier_id: int}
36

    
37
type clock_expr =
38
    {mutable cdesc: clock_desc;
39
     mutable cscoped: bool;
40
     cid: int}
41

    
42
(* pck stands for periodic clock. Easier not to separate pck from other clocks *)
43
and clock_desc =
44
  | Carrow of clock_expr * clock_expr
45
  | Ctuple of clock_expr list
46
  | Con of clock_expr * carrier_expr * ident
47
  | Pck_up of clock_expr * int
48
  | Pck_down of clock_expr * int
49
  | Pck_phase of clock_expr * rat
50
  | Pck_const of int * rat
51
  | Cvar of clock_set (* Monomorphic clock variable *)
52
  | Cunivar of clock_set (* Polymorphic clock variable *)
53
  | Clink of clock_expr (* During unification, make links instead of substitutions *)
54
  | Ccarrying of carrier_expr * clock_expr
55

    
56
type error =
57
  | Clock_clash of clock_expr * clock_expr
58
  | Not_pck
59
  | Clock_set_mismatch of clock_expr * clock_set
60
  | Cannot_be_polymorphic of clock_expr
61
  | Invalid_imported_clock of clock_expr
62
  | Invalid_const of clock_expr
63
  | Factor_zero
64
  | Carrier_mismatch of carrier_expr * carrier_expr
65
  | Carrier_extrusion of clock_expr * carrier_expr
66
  | Clock_extrusion of clock_expr * clock_expr
67

    
68
exception Unify of clock_expr * clock_expr
69
exception Subsume of clock_expr * clock_set
70
exception Mismatch of carrier_expr * carrier_expr
71
exception Scope_carrier of carrier_expr
72
exception Scope_clock of clock_expr
73
exception Error of Location.t * error
74

    
75
let new_id = ref (-1)
76

    
77
let new_ck desc scoped =
78
  incr new_id; {cdesc=desc; cid = !new_id; cscoped = scoped}
79

    
80
let new_var scoped =
81
  new_ck (Cvar CSet_all) scoped
82

    
83
let new_univar () =
84
  new_ck (Cunivar CSet_all) false
85

    
86
let new_carrier_id = ref (-1)
87

    
88
let new_carrier desc scoped =
89
  incr new_carrier_id; {carrier_desc = desc;
90
                        carrier_id = !new_carrier_id;
91
                        carrier_scoped = scoped}
92

    
93
let new_carrier_name () =
94
  new_carrier Carry_name true
95

    
96
let rec repr =
97
  function
98
      {cdesc=Clink ck'} ->
99
        repr ck'
100
    | ck -> ck
101

    
102
let rec carrier_repr =
103
  function {carrier_desc = Carry_link cr'} -> carrier_repr cr'
104
    | cr -> cr
105

    
106
(** Splits [ck] into the [lhs,rhs] of an arrow clock. Expects an arrow clock
107
    (ensured by language syntax) *)
108
let split_arrow ck =
109
  match (repr ck).cdesc with
110
  | Carrow (cin,cout) -> cin,cout
111
    (* Functions are not first order, I don't think the var case
112
       needs to be considered here *)
113
  | _ -> failwith "Internal error: not an arrow clock"
114

    
115
let get_carrier_name ck =
116
 match (repr ck).cdesc with
117
 | Ccarrying (cr, _) -> Some cr
118
 | _                 -> None
119

    
120
let uncarrier ck =
121
 match ck.cdesc with
122
 | Ccarrying (_, ck') -> ck'
123
 | _                  -> ck
124

    
125
(* Removes all links in a clock. Only used for clocks
126
   simplification though. *)
127
let rec deep_repr ck =
128
  match ck.cdesc with
129
  | Carrow (ck1,ck2) ->
130
      new_ck (Carrow (deep_repr ck1, deep_repr ck2)) ck.cscoped
131
  | Ctuple cl ->
132
      new_ck (Ctuple (List.map deep_repr cl)) ck.cscoped
133
  | Con (ck', c, l) ->
134
      new_ck (Con (deep_repr ck', c, l)) ck.cscoped
135
  | Pck_up (ck',k) ->
136
      new_ck (Pck_up (deep_repr ck',k)) ck.cscoped
137
  | Pck_down (ck',k) ->
138
      new_ck (Pck_down (deep_repr ck',k)) ck.cscoped
139
  | Pck_phase (ck',q) ->
140
      new_ck (Pck_phase (deep_repr ck',q)) ck.cscoped
141
  | Pck_const (_,_) | Cvar _ | Cunivar _ -> ck
142
  | Clink ck' -> deep_repr ck'
143
  | Ccarrying (cr,ck') -> new_ck (Ccarrying (cr, deep_repr ck')) ck.cscoped
144

    
145
(** Splits ck into the [lhs,rhs] of an arrow clock. Expects an arrow clock
146
    (ensured by language syntax) *)
147
let split_arrow ck =
148
  match (repr ck).cdesc with
149
  | Carrow (cin,cout) -> cin,cout
150
  | _ -> failwith "Internal error: not an arrow clock"
151

    
152
(** Returns the clock corresponding to a clock list. *)
153
let clock_of_clock_list ckl =
154
  if (List.length ckl) > 1 then
155
    new_ck (Ctuple ckl) true
156
  else
157
    List.hd ckl
158

    
159
let clock_list_of_clock ck =
160
 match (repr ck).cdesc with
161
 | Ctuple cl -> cl
162
 | _         -> [ck]
163

    
164
let clock_on ck cr l =
165
 clock_of_clock_list (List.map (fun ck -> new_ck (Con (ck,cr,l)) true) (clock_list_of_clock ck))
166

    
167
let clock_current ck =
168
 clock_of_clock_list (List.map (fun ck -> match (repr ck).cdesc with Con(ck',_,_) -> ck' | _ -> assert false) (clock_list_of_clock ck))
169

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

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

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

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

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

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

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

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

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

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

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

    
355
let eq_carrier cr1 cr2 =
356
  match (carrier_repr cr1).carrier_desc, (carrier_repr cr2).carrier_desc with
357
 | Carry_const id1, Carry_const id2 -> id1 = id2
358
 | _                                -> cr1.carrier_id = cr2.carrier_id
359

    
360
let eq_clock ck1 ck2 =
361
 (repr ck1).cid = (repr ck2).cid
362

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

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

    
384
let clock_of_root_branch r br =
385
 List.fold_left (fun ck (cr,l) -> new_ck (Con (ck, cr, l)) true) r br
386

    
387
(* Computes the (longest) common prefix of two branches *)
388
let rec common_prefix br1 br2 =
389
 match br1, br2 with
390
 | []          , _
391
 | _           , []           -> []
392
 | (cr1,l1)::q1, (cr2,l2)::q2 ->
393
   if eq_carrier cr1 cr2 && (l1 = l2)
394
   then (cr1, l1) :: common_prefix q1 q2
395
   else []
396

    
397
(* Tests whether clock branches [br1] nd [br2] are statically disjoint *)
398
let rec disjoint_branches br1 br2 =
399
 match br1, br2 with
400
 | []          , _
401
 | _           , []           -> false
402
 | (cr1,l1)::q1, (cr2,l2)::q2 -> eq_carrier cr1 cr2 && ((l1 <> l2) || disjoint_branches q1 q2);;
403

    
404
(* Disjunction relation between variables based upon their static clocks. *)
405
let disjoint ck1 ck2 =
406
  eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2)
407

    
408
(** [normalize pck] returns the normal form of clock [pck]. *)
409
let normalize pck =
410
  let changed = ref true in
411
  let rec aux pck =
412
    match pck.cdesc with
413
    | Pck_up ({cdesc=Pck_up (pck',k')},k) ->
414
        changed:=true;
415
        new_ck (Pck_up (aux pck',k*k')) pck.cscoped
416
    | Pck_up ({cdesc=Pck_down (pck',k')},k) ->
417
        changed:=true;
418
        new_ck (Pck_down (new_ck (Pck_up (aux pck',k)) pck.cscoped,k')) pck.cscoped
419
    | Pck_up ({cdesc=Pck_phase (pck',(a,b))},k) ->
420
        changed:=true;
421
        new_ck (Pck_phase (new_ck (Pck_up (aux pck',k)) pck.cscoped,(a*k,b))) pck.cscoped
422
    | Pck_down ({cdesc=Pck_down (pck',k')},k) ->
423
        changed:=true;
424
        new_ck (Pck_down (aux pck',k*k')) pck.cscoped
425
    | Pck_down ({cdesc=Pck_phase (pck',(a,b))},k) ->
426
        changed:=true;
427
        new_ck (Pck_phase (new_ck (Pck_down (aux pck',k)) pck.cscoped,(a,b*k))) pck.cscoped
428
    | Pck_phase ({cdesc=Pck_phase (pck',(a',b'))},(a,b)) ->
429
        changed:=true;
430
        let (a'',b'') = sum_rat (a,b) (a',b') in
431
        new_ck (Pck_phase (aux pck',(a'',b''))) pck.cscoped
432
    | Pck_up (pck',k') ->
433
        new_ck (Pck_up (aux pck',k')) pck.cscoped
434
    | Pck_down (pck',k') ->
435
        new_ck (Pck_down (aux pck',k')) pck.cscoped
436
    | Pck_phase (pck',k') ->
437
        new_ck (Pck_phase (aux pck',k')) pck.cscoped
438
    | Ccarrying (cr,ck') ->
439
        new_ck (Ccarrying (cr, aux ck')) pck.cscoped
440
    | _ -> pck
441
  in
442
  let nf=ref pck in
443
  while !changed do
444
    changed:=false;
445
    nf:=aux !nf
446
  done;
447
  !nf
448

    
449
(** [canonize pck] reduces transformations of [pck] and removes
450
    identity transformations. Expects a normalized periodic clock ! *)
451
let canonize pck =
452
  let rec remove_id_trans pck =
453
    match pck.cdesc with
454
    | Pck_up (pck',1) | Pck_down (pck',1) | Pck_phase (pck',(0,_)) ->
455
        remove_id_trans pck'
456
    | _ -> pck
457
  in
458
  let pck =
459
    match pck.cdesc with
460
    | Pck_phase ({cdesc=Pck_down ({cdesc=Pck_up (v,k)},k')},k'') ->
461
        let gcd = gcd k k' in
462
        new_ck (Pck_phase
463
                  (new_ck (Pck_down
464
                             (new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd))
465
                     pck.cscoped,k''))
466
          pck.cscoped
467
    | Pck_down ({cdesc=Pck_up (v,k)},k') ->
468
        let gcd = gcd k k' in
469
        new_ck (Pck_down (new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd)) pck.cscoped
470
    | _ -> pck
471
  in
472
  remove_id_trans pck
473

    
474
(** [simplify pck] applies pclocks simplifications to [pck] *)
475
let simplify pck =
476
  if (is_concrete_pck pck) then
477
    let n = period pck in
478
    let (a,b) = phase pck in
479
    let phase' = simplify_rat (a,b*n) in 
480
    new_ck (Pck_const (n,phase')) pck.cscoped
481
  else
482
    let pck' = deep_repr pck in
483
    let nf_pck = normalize pck' in
484
    canonize nf_pck
485
        
486
let print_cvar fmt cvar =
487
  match cvar.cdesc with
488
  | Cvar cset ->
489
 (*
490
      if cvar.cscoped
491
      then
492
	fprintf fmt "[_%s%a]"
493
	  (name_of_type cvar.cid)
494
	  print_ckset cset
495
      else
496
 *)
497
	fprintf fmt "_%s%a"
498
	  (name_of_type cvar.cid)
499
	  print_ckset cset
500
  | Cunivar cset ->
501
 (*
502
      if cvar.cscoped
503
      then
504
	fprintf fmt "['%s%a]"
505
	  (name_of_type cvar.cid)
506
	  print_ckset cset
507
      else
508
 *)
509
	fprintf fmt "'%s%a"
510
	  (name_of_type cvar.cid)
511
	  print_ckset cset
512
  | _ -> failwith "Internal error print_cvar"
513

    
514
(* Nice pretty-printing. Simplifies expressions before printing them. Non-linear
515
   complexity. *)
516
let print_ck fmt ck =
517
  let rec aux fmt ck =
518
    let ck = simplify ck in
519
    match ck.cdesc with
520
    | Carrow (ck1,ck2) ->
521
      fprintf fmt "%a->%a" aux ck1 aux ck2
522
    | Ctuple cklist ->
523
      fprintf fmt "(%a)" 
524
	(fprintf_list ~sep:" * " aux) cklist
525
    | Con (ck,c,l) ->
526
      fprintf fmt "%a on %s(%a)" aux ck l print_carrier c
527
    | Pck_up (ck,k) ->
528
      fprintf fmt "%a*.%i" aux ck k
529
    | Pck_down (ck,k) ->
530
      fprintf fmt "%a/.%i" aux ck k
531
    | Pck_phase (ck,q) ->
532
      fprintf fmt "%a->.%a" aux ck print_rat (simplify_rat q)
533
    | Pck_const (n,p) ->
534
      fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
535
    | Cvar cset ->
536
(*
537
      if ck.cscoped
538
      then
539
        fprintf fmt "[_%s]" (name_of_type ck.cid)
540
      else
541
*)
542
	fprintf fmt "_%s" (name_of_type ck.cid)
543
    | Cunivar cset ->
544
(*
545
      if ck.cscoped
546
      then
547
        fprintf fmt "['%s]" (name_of_type ck.cid)
548
      else
549
*)
550
        fprintf fmt "'%s" (name_of_type ck.cid)
551
    | Clink ck' ->
552
        aux fmt ck'
553
    | Ccarrying (cr,ck') ->
554
      fprintf fmt "(%a:%a)" print_carrier cr aux ck'
555
  in
556
  let cvars = constrained_vars_of_clock ck in
557
  aux fmt ck;
558
  if cvars <> [] then
559
    fprintf fmt " (where %a)"
560
      (fprintf_list ~sep:", " print_cvar) cvars
561

    
562
(* prints only the Con components of a clock, useful for printing nodes *)
563
let rec print_ck_suffix fmt ck =
564
  let ck = simplify ck in
565
  match ck.cdesc with
566
  | Carrow _
567
  | Ctuple _
568
  | Cvar _
569
  | Cunivar _   -> ()
570
  | Con (ck,c,l) ->
571
    fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c
572
  | Clink ck' ->
573
    print_ck_suffix fmt ck'
574
  | Ccarrying (cr,ck') ->
575
    fprintf fmt "%a" print_ck_suffix ck'
576
  | _ -> assert false
577

    
578
let pp_error fmt = function
579
  | Clock_clash (ck1,ck2) ->
580
      reset_names ();
581
      fprintf fmt "Expected clock %a, got clock %a@."
582
      print_ck ck1
583
      print_ck ck2
584
  | Not_pck ->
585
    fprintf fmt "The clock of this expression must be periodic@."
586
  | Carrier_mismatch (cr1, cr2) ->
587
     fprintf fmt "Name clash. Expected clock %a, got clock %a@."
588
       print_carrier cr1
589
       print_carrier cr2
590
  | Clock_set_mismatch (ck,cset) ->
591
      reset_names ();
592
    fprintf fmt "Clock %a is not included in clock set %a@."
593
      print_ck ck
594
      print_ckset cset
595
  | Cannot_be_polymorphic ck ->
596
      reset_names ();
597
    fprintf fmt "The main node cannot have a polymorphic clock: %a@."
598
      print_ck ck
599
  | Invalid_imported_clock ck ->
600
      reset_names ();
601
    fprintf fmt "Not a valid imported node clock: %a@."
602
      print_ck ck
603
  | Invalid_const ck ->
604
      reset_names ();
605
    fprintf fmt "Clock %a is not a valid periodic clock@."
606
      print_ck ck;
607
  | Factor_zero ->
608
    fprintf fmt "Cannot apply clock transformation with factor 0@."
609
  | Carrier_extrusion (ck,cr) ->
610
    fprintf fmt "This node has clock@.%a@.It is invalid as %a escapes its scope@."
611
      print_ck ck
612
      print_carrier cr
613
  | Clock_extrusion (ck_node,ck) ->
614
    fprintf fmt "This node has clock@.%a@.It is invalid as %a escapes its scope@."
615
      print_ck ck_node
616
      print_ck ck
617

    
618
let const_of_carrier cr =
619
 match (carrier_repr cr).carrier_desc with
620
 | Carry_const id -> id
621
 | Carry_name
622
 | Carry_var
623
 | Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
624
 
625
let uneval const cr =
626
  (*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*)
627
  let cr = carrier_repr cr in
628
  match cr.carrier_desc with
629
  | Carry_var -> cr.carrier_desc <- Carry_const const
630
  | Carry_name -> cr.carrier_desc <- Carry_const const
631
  | _         -> assert false
632

    
633
(* Local Variables: *)
634
(* compile-command:"make -C .." *)
635
(* End: *)