Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / clocks.ml @ fc886259

History | View | Annotate | Download (20.5 KB)

1 a2d97a3e ploc
(********************************************************************)
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 22fe1c93 ploc
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 fc886259 xthirioux
let print_ckset fmt s =
76
  match s with
77
  | CSet_all -> ()
78
  | CSet_pck (k,q) ->
79
      let (a,b) = simplify_rat q in
80
      if k = 1 && a = 0 then
81
        fprintf fmt "<:P"
82
      else
83
        fprintf fmt "<:P_(%i,%a)" k print_rat (a,b)
84
85
let rec print_carrier fmt cr =
86
 (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
87
  match cr.carrier_desc with
88
  | Carry_const id -> fprintf fmt "%s" id
89
  | Carry_name ->
90
      fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
91
  | Carry_var ->
92
    fprintf fmt "'%s" (name_of_carrier cr.carrier_id)
93
  | Carry_link cr' ->
94
    print_carrier fmt cr'
95
96
(* Simple pretty-printing, performs no simplifications. Linear
97
   complexity. For debug mainly. *)
98
let rec print_ck_long fmt ck =
99
  match ck.cdesc with
100
  | Carrow (ck1,ck2) ->
101
      fprintf fmt "%a->%a" print_ck_long ck1 print_ck_long ck2
102
  | Ctuple cklist ->
103
    fprintf fmt "(%a)"
104
      (fprintf_list ~sep:" * " print_ck_long) cklist
105
  | Con (ck,c,l) ->
106
    fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
107
  | Pck_up (ck,k) ->
108
    fprintf fmt "%a*^%i" print_ck_long ck k
109
  | Pck_down (ck,k) ->
110
    fprintf fmt "%a/^%i" print_ck_long ck k
111
  | Pck_phase (ck,q) ->
112
    fprintf fmt "%a~>%a" print_ck_long ck print_rat (simplify_rat q)
113
  | Pck_const (n,p) ->
114
    fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
115
  | Cvar cset ->
116
    fprintf fmt "'_%i%a" ck.cid print_ckset cset
117
  | Cunivar cset ->
118
    fprintf fmt "'%i%a" ck.cid print_ckset cset
119
  | Clink ck' ->
120
    fprintf fmt "link %a" print_ck_long ck'
121
  | Ccarrying (cr,ck') ->
122
    fprintf fmt "(%a:%a)" print_carrier cr print_ck_long ck'
123
124 22fe1c93 ploc
let new_id = ref (-1)
125
126
let new_ck desc scoped =
127
  incr new_id; {cdesc=desc; cid = !new_id; cscoped = scoped}
128
129
let new_var scoped =
130
  new_ck (Cvar CSet_all) scoped
131
132
let new_univar () =
133
  new_ck (Cunivar CSet_all) false
134
135
let new_carrier_id = ref (-1)
136
137
let new_carrier desc scoped =
138
  incr new_carrier_id; {carrier_desc = desc;
139
                        carrier_id = !new_carrier_id;
140
                        carrier_scoped = scoped}
141
142
let new_carrier_name () =
143
  new_carrier Carry_name true
144
145
let rec repr =
146
  function
147
      {cdesc=Clink ck'} ->
148
        repr ck'
149
    | ck -> ck
150
151
let rec carrier_repr =
152
  function {carrier_desc = Carry_link cr'} -> carrier_repr cr'
153
    | cr -> cr
154
155
(** Splits [ck] into the [lhs,rhs] of an arrow clock. Expects an arrow clock
156
    (ensured by language syntax) *)
157
let split_arrow ck =
158
  match (repr ck).cdesc with
159
  | Carrow (cin,cout) -> cin,cout
160
    (* Functions are not first order, I don't think the var case
161
       needs to be considered here *)
162
  | _ -> failwith "Internal error: not an arrow clock"
163
164 8f1c7e91 xthirioux
let get_carrier_name ck =
165
 match (repr ck).cdesc with
166
 | Ccarrying (cr, _) -> Some cr
167
 | _                 -> None
168
169 fc886259 xthirioux
let rename_carrier_static rename cr =
170
  match (carrier_repr cr).carrier_desc with
171
  | Carry_const id -> { cr with carrier_desc = Carry_const (rename id) }
172
  | _              -> (Format.eprintf "internal error: Clocks.rename_carrier_static %a@." print_carrier cr; assert false)
173
174
let rec rename_static rename ck =
175
 match (repr ck).cdesc with
176
 | Ccarrying (cr, ck') -> { ck with cdesc = Ccarrying (rename_carrier_static rename cr, rename_static rename ck') }
177
 | Con (ck', cr, l)    -> { ck with cdesc = Con (rename_static rename ck', rename_carrier_static rename cr, l) }
178
 | _                   -> ck
179
180 22fe1c93 ploc
let uncarrier ck =
181
 match ck.cdesc with
182 8f1c7e91 xthirioux
 | Ccarrying (_, ck') -> ck'
183
 | _                  -> ck
184 22fe1c93 ploc
185
(* Removes all links in a clock. Only used for clocks
186
   simplification though. *)
187
let rec deep_repr ck =
188
  match ck.cdesc with
189
  | Carrow (ck1,ck2) ->
190
      new_ck (Carrow (deep_repr ck1, deep_repr ck2)) ck.cscoped
191
  | Ctuple cl ->
192
      new_ck (Ctuple (List.map deep_repr cl)) ck.cscoped
193
  | Con (ck', c, l) ->
194
      new_ck (Con (deep_repr ck', c, l)) ck.cscoped
195
  | Pck_up (ck',k) ->
196
      new_ck (Pck_up (deep_repr ck',k)) ck.cscoped
197
  | Pck_down (ck',k) ->
198
      new_ck (Pck_down (deep_repr ck',k)) ck.cscoped
199
  | Pck_phase (ck',q) ->
200
      new_ck (Pck_phase (deep_repr ck',q)) ck.cscoped
201
  | Pck_const (_,_) | Cvar _ | Cunivar _ -> ck
202
  | Clink ck' -> deep_repr ck'
203
  | Ccarrying (cr,ck') -> new_ck (Ccarrying (cr, deep_repr ck')) ck.cscoped
204
205
(** Splits ck into the [lhs,rhs] of an arrow clock. Expects an arrow clock
206
    (ensured by language syntax) *)
207
let split_arrow ck =
208
  match (repr ck).cdesc with
209
  | Carrow (cin,cout) -> cin,cout
210
  | _ -> failwith "Internal error: not an arrow clock"
211
212
(** Returns the clock corresponding to a clock list. *)
213
let clock_of_clock_list ckl =
214
  if (List.length ckl) > 1 then
215
    new_ck (Ctuple ckl) true
216
  else
217
    List.hd ckl
218
219
let clock_list_of_clock ck =
220
 match (repr ck).cdesc with
221
 | Ctuple cl -> cl
222
 | _         -> [ck]
223
224 6fdfb60b xthirioux
let clock_on ck cr l =
225
 clock_of_clock_list (List.map (fun ck -> new_ck (Con (ck,cr,l)) true) (clock_list_of_clock ck))
226
227 54d032f5 xthirioux
let clock_current ck =
228
 clock_of_clock_list (List.map (fun ck -> match (repr ck).cdesc with Con(ck',_,_) -> ck' | _ -> assert false) (clock_list_of_clock ck))
229
230 22fe1c93 ploc
let clock_of_impnode_clock ck =
231
  let ck = repr ck in
232
  match ck.cdesc with
233
  | Carrow _ | Clink _ | Cvar _ | Cunivar _ ->
234
      failwith "internal error clock_of_impnode_clock"
235
  | Ctuple cklist -> List.hd cklist
236
  | Con (_,_,_) | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_)
237
  | Pck_const (_,_) | Ccarrying (_,_) -> ck
238
239
(** [intersect set1 set2] returns the intersection of clock subsets
240
    [set1] and [set2]. *)
241
let intersect set1 set2 =
242
  match set1,set2 with
243
  | CSet_all,_ -> set2
244
  | _,CSet_all -> set1
245
  | CSet_pck (k,q), CSet_pck (k',q') ->
246
      let k'',q'' = lcm k k',max_rat q q' in
247
      CSet_pck (k'',q'')
248
249
(** [can_be_pck ck] returns true if [ck] "may be" a pclock (the uncertainty is
250
    due to clock variables) *)
251
let rec can_be_pck ck =
252
  match (repr ck).cdesc with
253
  | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) | Pck_const (_,_)
254
  | Cvar _ | Cunivar _ ->
255
      true
256
  | Ccarrying (_,ck') -> can_be_pck ck
257
  | _ -> false
258
259
(** [is_concrete_pck ck] returns true if [ck] is a concrete [pck] (pck
260
    transformations applied to a pck constant) *)
261
let rec is_concrete_pck ck =
262
  match ck.cdesc with
263
  | Carrow (_,_) | Ctuple _ | Con (_,_,_)
264
  | Cvar _ | Cunivar _ -> false
265
  | Pck_up (ck',_) | Pck_down (ck',_) -> is_concrete_pck ck'
266
  | Pck_phase (ck',_) -> is_concrete_pck ck'
267
  | Pck_const (_,_) -> true
268
  | Clink ck' -> is_concrete_pck ck'
269
  | Ccarrying (_,ck') -> false
270
271
(** [is_polymorphic ck] returns true if [ck] is polymorphic. *)
272
let rec is_polymorphic ck =
273
  match ck.cdesc with
274
  | Cvar _ | Pck_const (_,_) -> false
275
  | Carrow (ck1,ck2) -> (is_polymorphic ck1) || (is_polymorphic ck2)
276
  | Ctuple ckl -> List.exists (fun c -> is_polymorphic c) ckl
277
  | Con (ck',_,_) -> is_polymorphic ck'
278
  | Pck_up (ck',_) | Pck_down (ck',_) -> is_polymorphic ck'
279
  | Pck_phase (ck',_) -> is_polymorphic ck'
280
  | Cunivar _ -> true
281
  | Clink ck' -> is_polymorphic ck'
282
  | Ccarrying (_,ck') -> is_polymorphic ck'
283
284
(** [constrained_vars_of_clock ck] returns the clock variables subject
285
    to sub-typing constraints appearing in clock [ck]. Removes duplicates *)
286
(* Used mainly for debug, non-linear complexity. *)
287
let rec constrained_vars_of_clock ck =
288
  let rec aux vars ck =
289
    match ck.cdesc with
290
    | Pck_const (_,_) ->
291
        vars
292
    | Cvar cset ->
293
        begin
294
          match cset with
295
          | CSet_all -> vars
296
          | _ ->
297
              list_union [ck] vars
298
        end
299
    | Carrow (ck1,ck2) ->
300
        let l = aux vars ck1 in
301
        aux l ck2
302
    | Ctuple ckl ->
303
        List.fold_left
304
          (fun acc ck' -> aux acc ck') 
305
          vars ckl
306
    | Con (ck',_,_) -> aux vars ck'
307
    | Pck_up (ck',_) | Pck_down (ck',_) -> aux vars ck'
308
    | Pck_phase (ck',_) -> aux vars ck'
309
    | Cunivar cset ->
310
        begin
311
          match cset with
312
          | CSet_all -> vars
313
          | _ -> list_union [ck] vars
314
        end
315
    | Clink ck' -> aux vars ck'
316
    | Ccarrying (_,ck') -> aux vars ck'
317
  in
318
  aux [] ck
319
320
(** [period ck] returns the period of [ck]. Expects a constant pclock
321
    expression belonging to the correct clock set. *)
322
let rec period ck =
323
  let rec aux ck =
324
    match ck.cdesc with
325
    | Carrow (_,_) | Ctuple _ | Con (_,_,_)
326
    | Cvar _ | Cunivar _ ->
327
        failwith "internal error: can only compute period of const pck"
328
    | Pck_up (ck',k) ->
329
        (aux ck')/.(float_of_int k)
330
    | Pck_down (ck',k) ->
331
        (float_of_int k)*.(aux ck')
332
    | Pck_phase (ck',_) ->
333
        aux ck'
334
    | Pck_const (n,_) ->
335
        float_of_int n
336
    | Clink ck' -> aux ck'
337
    | Ccarrying (_,ck') -> aux ck'
338
  in
339
  int_of_float (aux ck)
340
341
(** [phase ck] returns the phase of [ck]. It is not expressed as a
342
    fraction of the period, but instead as an amount of time. Expects a
343
    constant expression belonging to the correct P_k *)
344
let phase ck =
345
  let rec aux ck =
346
  match ck.cdesc with
347
  | Carrow (_,_) | Ctuple _ | Con (_,_,_)
348
  | Cvar _ | Cunivar _ ->
349
      failwith "internal error: can only compute phase of const pck"
350
  | Pck_up (ck',_) ->
351
      aux ck'
352
  | Pck_down (ck',k) ->
353
      aux ck'
354
  | Pck_phase (ck',(a,b)) ->
355
      let n = period ck' in
356
      let (a',b') = aux ck' in
357
      sum_rat (a',b') (n*a,b)
358
  | Pck_const (n,(a,b)) ->
359
      (n*a,b)
360
  | Clink ck' -> aux ck'
361
  | Ccarrying (_,ck') -> aux ck'
362
  in
363
  let (a,b) = aux ck in
364
  simplify_rat (a,b)
365 b1a97ade xthirioux
366
let eq_carrier cr1 cr2 =
367
  match (carrier_repr cr1).carrier_desc, (carrier_repr cr2).carrier_desc with
368
 | Carry_const id1, Carry_const id2 -> id1 = id2
369
 | _                                -> cr1.carrier_id = cr2.carrier_id
370
371 919292ca xthirioux
let eq_clock ck1 ck2 =
372
 (repr ck1).cid = (repr ck2).cid
373
374 8f89eba8 xthirioux
(* Returns the clock root of a clock *)
375
let rec root ck =
376 919292ca xthirioux
  let ck = repr ck in
377
  match ck.cdesc with
378 6fdfb60b xthirioux
  | Ctuple (ck'::_)
379
  | Con (ck',_,_) | Clink ck' | Ccarrying (_,ck') -> root ck'
380 22fe1c93 ploc
  | Pck_up _ | Pck_down _ | Pck_phase _ | Pck_const _ | Cvar _ | Cunivar _ -> ck
381 6fdfb60b xthirioux
  | Carrow _ | Ctuple _ -> failwith "Internal error root"
382 22fe1c93 ploc
383 8f89eba8 xthirioux
(* Returns the branch of clock [ck] in its clock tree *)
384
let rec branch ck =
385
  let rec branch ck acc =
386
    match (repr ck).cdesc with
387
    | Ccarrying (_, ck) -> branch ck acc
388
    | Con (ck, cr, l)   -> branch ck ((cr, l) :: acc)
389 6fdfb60b xthirioux
    | Ctuple (ck::_)    -> branch ck acc
390 919292ca xthirioux
    | Ctuple _
391 8f89eba8 xthirioux
    | Carrow _          -> assert false
392
    | _                 -> acc
393
  in branch ck [];;
394
395 54d032f5 xthirioux
let clock_of_root_branch r br =
396
 List.fold_left (fun ck (cr,l) -> new_ck (Con (ck, cr, l)) true) r br
397
398
(* Computes the (longest) common prefix of two branches *)
399
let rec common_prefix br1 br2 =
400
 match br1, br2 with
401
 | []          , _
402
 | _           , []           -> []
403
 | (cr1,l1)::q1, (cr2,l2)::q2 ->
404
   if eq_carrier cr1 cr2 && (l1 = l2)
405
   then (cr1, l1) :: common_prefix q1 q2
406
   else []
407
408 8f89eba8 xthirioux
(* Tests whether clock branches [br1] nd [br2] are statically disjoint *)
409
let rec disjoint_branches br1 br2 =
410
 match br1, br2 with
411
 | []          , _
412
 | _           , []           -> false
413 b1a97ade xthirioux
 | (cr1,l1)::q1, (cr2,l2)::q2 -> eq_carrier cr1 cr2 && ((l1 <> l2) || disjoint_branches q1 q2);;
414 8f89eba8 xthirioux
415
(* Disjunction relation between variables based upon their static clocks. *)
416
let disjoint ck1 ck2 =
417 919292ca xthirioux
  eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2)
418 8f89eba8 xthirioux
419 22fe1c93 ploc
(** [normalize pck] returns the normal form of clock [pck]. *)
420
let normalize pck =
421
  let changed = ref true in
422
  let rec aux pck =
423
    match pck.cdesc with
424
    | Pck_up ({cdesc=Pck_up (pck',k')},k) ->
425
        changed:=true;
426
        new_ck (Pck_up (aux pck',k*k')) pck.cscoped
427
    | Pck_up ({cdesc=Pck_down (pck',k')},k) ->
428
        changed:=true;
429
        new_ck (Pck_down (new_ck (Pck_up (aux pck',k)) pck.cscoped,k')) pck.cscoped
430
    | Pck_up ({cdesc=Pck_phase (pck',(a,b))},k) ->
431
        changed:=true;
432
        new_ck (Pck_phase (new_ck (Pck_up (aux pck',k)) pck.cscoped,(a*k,b))) pck.cscoped
433
    | Pck_down ({cdesc=Pck_down (pck',k')},k) ->
434
        changed:=true;
435
        new_ck (Pck_down (aux pck',k*k')) pck.cscoped
436
    | Pck_down ({cdesc=Pck_phase (pck',(a,b))},k) ->
437
        changed:=true;
438
        new_ck (Pck_phase (new_ck (Pck_down (aux pck',k)) pck.cscoped,(a,b*k))) pck.cscoped
439
    | Pck_phase ({cdesc=Pck_phase (pck',(a',b'))},(a,b)) ->
440
        changed:=true;
441
        let (a'',b'') = sum_rat (a,b) (a',b') in
442
        new_ck (Pck_phase (aux pck',(a'',b''))) pck.cscoped
443
    | Pck_up (pck',k') ->
444
        new_ck (Pck_up (aux pck',k')) pck.cscoped
445
    | Pck_down (pck',k') ->
446
        new_ck (Pck_down (aux pck',k')) pck.cscoped
447
    | Pck_phase (pck',k') ->
448
        new_ck (Pck_phase (aux pck',k')) pck.cscoped
449
    | Ccarrying (cr,ck') ->
450
        new_ck (Ccarrying (cr, aux ck')) pck.cscoped
451
    | _ -> pck
452
  in
453
  let nf=ref pck in
454
  while !changed do
455
    changed:=false;
456
    nf:=aux !nf
457
  done;
458
  !nf
459
460
(** [canonize pck] reduces transformations of [pck] and removes
461
    identity transformations. Expects a normalized periodic clock ! *)
462
let canonize pck =
463
  let rec remove_id_trans pck =
464
    match pck.cdesc with
465
    | Pck_up (pck',1) | Pck_down (pck',1) | Pck_phase (pck',(0,_)) ->
466
        remove_id_trans pck'
467
    | _ -> pck
468
  in
469
  let pck =
470
    match pck.cdesc with
471
    | Pck_phase ({cdesc=Pck_down ({cdesc=Pck_up (v,k)},k')},k'') ->
472
        let gcd = gcd k k' in
473
        new_ck (Pck_phase
474
                  (new_ck (Pck_down
475
                             (new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd))
476
                     pck.cscoped,k''))
477
          pck.cscoped
478
    | Pck_down ({cdesc=Pck_up (v,k)},k') ->
479
        let gcd = gcd k k' in
480
        new_ck (Pck_down (new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd)) pck.cscoped
481
    | _ -> pck
482
  in
483
  remove_id_trans pck
484
485
(** [simplify pck] applies pclocks simplifications to [pck] *)
486
let simplify pck =
487
  if (is_concrete_pck pck) then
488
    let n = period pck in
489
    let (a,b) = phase pck in
490
    let phase' = simplify_rat (a,b*n) in 
491
    new_ck (Pck_const (n,phase')) pck.cscoped
492
  else
493
    let pck' = deep_repr pck in
494
    let nf_pck = normalize pck' in
495
    canonize nf_pck
496
        
497
let print_cvar fmt cvar =
498
  match cvar.cdesc with
499
  | Cvar cset ->
500
 (*
501
      if cvar.cscoped
502
      then
503 52cfee34 xthirioux
	fprintf fmt "[_%s%a]"
504 22fe1c93 ploc
	  (name_of_type cvar.cid)
505
	  print_ckset cset
506
      else
507
 *)
508 52cfee34 xthirioux
	fprintf fmt "_%s%a"
509 22fe1c93 ploc
	  (name_of_type cvar.cid)
510
	  print_ckset cset
511
  | Cunivar cset ->
512
 (*
513
      if cvar.cscoped
514
      then
515
	fprintf fmt "['%s%a]"
516
	  (name_of_type cvar.cid)
517
	  print_ckset cset
518
      else
519
 *)
520
	fprintf fmt "'%s%a"
521
	  (name_of_type cvar.cid)
522
	  print_ckset cset
523
  | _ -> failwith "Internal error print_cvar"
524
525
(* Nice pretty-printing. Simplifies expressions before printing them. Non-linear
526
   complexity. *)
527
let print_ck fmt ck =
528
  let rec aux fmt ck =
529
    let ck = simplify ck in
530
    match ck.cdesc with
531
    | Carrow (ck1,ck2) ->
532
      fprintf fmt "%a->%a" aux ck1 aux ck2
533
    | Ctuple cklist ->
534
      fprintf fmt "(%a)" 
535
	(fprintf_list ~sep:" * " aux) cklist
536
    | Con (ck,c,l) ->
537
      fprintf fmt "%a on %s(%a)" aux ck l print_carrier c
538
    | Pck_up (ck,k) ->
539
      fprintf fmt "%a*.%i" aux ck k
540
    | Pck_down (ck,k) ->
541
      fprintf fmt "%a/.%i" aux ck k
542
    | Pck_phase (ck,q) ->
543
      fprintf fmt "%a->.%a" aux ck print_rat (simplify_rat q)
544
    | Pck_const (n,p) ->
545
      fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
546
    | Cvar cset ->
547
(*
548
      if ck.cscoped
549
      then
550 52cfee34 xthirioux
        fprintf fmt "[_%s]" (name_of_type ck.cid)
551 22fe1c93 ploc
      else
552
*)
553 52cfee34 xthirioux
	fprintf fmt "_%s" (name_of_type ck.cid)
554 22fe1c93 ploc
    | Cunivar cset ->
555
(*
556
      if ck.cscoped
557
      then
558
        fprintf fmt "['%s]" (name_of_type ck.cid)
559
      else
560
*)
561
        fprintf fmt "'%s" (name_of_type ck.cid)
562
    | Clink ck' ->
563
        aux fmt ck'
564
    | Ccarrying (cr,ck') ->
565
      fprintf fmt "(%a:%a)" print_carrier cr aux ck'
566
  in
567
  let cvars = constrained_vars_of_clock ck in
568
  aux fmt ck;
569
  if cvars <> [] then
570
    fprintf fmt " (where %a)"
571
      (fprintf_list ~sep:", " print_cvar) cvars
572
573 8f1c7e91 xthirioux
(* prints only the Con components of a clock, useful for printing nodes *)
574
let rec print_ck_suffix fmt ck =
575
  let ck = simplify ck in
576
  match ck.cdesc with
577
  | Carrow _
578
  | Ctuple _
579
  | Cvar _
580
  | Cunivar _   -> ()
581
  | Con (ck,c,l) ->
582
    fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c
583
  | Clink ck' ->
584
    print_ck_suffix fmt ck'
585
  | Ccarrying (cr,ck') ->
586
    fprintf fmt "%a" print_ck_suffix ck'
587
  | _ -> assert false
588
589 22fe1c93 ploc
let pp_error fmt = function
590
  | Clock_clash (ck1,ck2) ->
591
      reset_names ();
592
      fprintf fmt "Expected clock %a, got clock %a@."
593
      print_ck ck1
594
      print_ck ck2
595
  | Not_pck ->
596
    fprintf fmt "The clock of this expression must be periodic@."
597
  | Carrier_mismatch (cr1, cr2) ->
598
     fprintf fmt "Name clash. Expected clock %a, got clock %a@."
599
       print_carrier cr1
600
       print_carrier cr2
601
  | Clock_set_mismatch (ck,cset) ->
602
      reset_names ();
603
    fprintf fmt "Clock %a is not included in clock set %a@."
604
      print_ck ck
605
      print_ckset cset
606
  | Cannot_be_polymorphic ck ->
607
      reset_names ();
608
    fprintf fmt "The main node cannot have a polymorphic clock: %a@."
609
      print_ck ck
610
  | Invalid_imported_clock ck ->
611
      reset_names ();
612
    fprintf fmt "Not a valid imported node clock: %a@."
613
      print_ck ck
614
  | Invalid_const ck ->
615
      reset_names ();
616
    fprintf fmt "Clock %a is not a valid periodic clock@."
617
      print_ck ck;
618
  | Factor_zero ->
619
    fprintf fmt "Cannot apply clock transformation with factor 0@."
620
  | Carrier_extrusion (ck,cr) ->
621
    fprintf fmt "This node has clock@.%a@.It is invalid as %a escapes its scope@."
622
      print_ck ck
623
      print_carrier cr
624
  | Clock_extrusion (ck_node,ck) ->
625
    fprintf fmt "This node has clock@.%a@.It is invalid as %a escapes its scope@."
626
      print_ck ck_node
627
      print_ck ck
628
629 d4807c3d xthirioux
let const_of_carrier cr =
630
 match (carrier_repr cr).carrier_desc with
631
 | Carry_const id -> id
632
 | Carry_name
633
 | Carry_var
634
 | Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
635
 
636 8f1c7e91 xthirioux
let uneval const cr =
637 89b9e25c xthirioux
  (*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*)
638 8f1c7e91 xthirioux
  let cr = carrier_repr cr in
639
  match cr.carrier_desc with
640
  | Carry_var -> cr.carrier_desc <- Carry_const const
641 d4807c3d xthirioux
  | Carry_name -> cr.carrier_desc <- Carry_const const
642 8f1c7e91 xthirioux
  | _         -> assert false
643 22fe1c93 ploc
644
(* Local Variables: *)
645
(* compile-command:"make -C .." *)
646
(* End: *)