Revision c518d082
Added by Xavier Thirioux almost 8 years ago
| src/clocks.ml | ||
|---|---|---|
| 121 | 121 |
needs to be considered here *) |
| 122 | 122 |
| _ -> failwith "Internal error: not an arrow clock" |
| 123 | 123 |
|
| 124 |
let get_carrier_name ck = |
|
| 125 |
match (repr ck).cdesc with |
|
| 126 |
| Ccarrying (cr, _) -> Some cr |
|
| 127 |
| _ -> None |
|
| 128 |
|
|
| 124 | 129 |
let uncarrier ck = |
| 125 | 130 |
match ck.cdesc with |
| 126 |
| Ccarrying (cr, ck') -> ck'
|
|
| 127 |
| _ -> ck
|
|
| 131 |
| Ccarrying (_, ck') -> ck'
|
|
| 132 |
| _ -> ck |
|
| 128 | 133 |
|
| 129 | 134 |
(* Removes all links in a clock. Only used for clocks |
| 130 | 135 |
simplification though. *) |
| ... | ... | |
| 268 | 273 |
let rec print_carrier fmt cr = |
| 269 | 274 |
(* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *) |
| 270 | 275 |
match cr.carrier_desc with |
| 271 |
| Carry_const id -> fprintf fmt "'%s'" id
|
|
| 276 |
| Carry_const id -> fprintf fmt "%s" id
|
|
| 272 | 277 |
| Carry_name -> |
| 273 |
fprintf fmt "?%s" (name_of_carrier cr.carrier_id)
|
|
| 278 |
fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
|
|
| 274 | 279 |
| Carry_var -> |
| 275 |
fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
|
|
| 280 |
fprintf fmt "'%s" (name_of_carrier cr.carrier_id)
|
|
| 276 | 281 |
| Carry_link cr' -> |
| 277 | 282 |
print_carrier fmt cr' |
| 278 | 283 |
|
| ... | ... | |
| 512 | 517 |
fprintf fmt " (where %a)" |
| 513 | 518 |
(fprintf_list ~sep:", " print_cvar) cvars |
| 514 | 519 |
|
| 520 |
(* prints only the Con components of a clock, useful for printing nodes *) |
|
| 521 |
let rec print_ck_suffix fmt ck = |
|
| 522 |
let ck = simplify ck in |
|
| 523 |
match ck.cdesc with |
|
| 524 |
| Carrow _ |
|
| 525 |
| Ctuple _ |
|
| 526 |
| Cvar _ |
|
| 527 |
| Cunivar _ -> () |
|
| 528 |
| Con (ck,c,l) -> |
|
| 529 |
fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c |
|
| 530 |
| Clink ck' -> |
|
| 531 |
print_ck_suffix fmt ck' |
|
| 532 |
| Ccarrying (cr,ck') -> |
|
| 533 |
fprintf fmt "%a" print_ck_suffix ck' |
|
| 534 |
| _ -> assert false |
|
| 535 |
|
|
| 515 | 536 |
let pp_error fmt = function |
| 516 | 537 |
| Clock_clash (ck1,ck2) -> |
| 517 | 538 |
reset_names (); |
| ... | ... | |
| 552 | 573 |
print_ck ck_node |
| 553 | 574 |
print_ck ck |
| 554 | 575 |
|
| 576 |
let uneval const cr = |
|
| 577 |
(*Format.printf "uneval %s %a@." const print_carrier cr;*) |
|
| 578 |
let cr = carrier_repr cr in |
|
| 579 |
match cr.carrier_desc with |
|
| 580 |
| Carry_var -> cr.carrier_desc <- Carry_const const |
|
| 581 |
| _ -> assert false |
|
| 555 | 582 |
|
| 556 | 583 |
(* Local Variables: *) |
| 557 | 584 |
(* compile-command:"make -C .." *) |
Also available in: Unified diff
- added generation of clock information in interface (.lusi) files
- added clock checking between interface and implementation files