Revision 6a1a01d2 src/clock_calculus.ml
| src/clock_calculus.ml | ||
|---|---|---|
| 441 | 441 |
(Const_int i) -> i |
| 442 | 442 |
| _ -> failwith "Internal error: int_factor_of_expr" |
| 443 | 443 |
|
| 444 |
(** [clock_uncarry ck] drops the possible carrier name from clock [ck] *)
|
|
| 445 |
let clock_uncarry ck = |
|
| 444 |
(** [clock_uncarry ck] drops the possible carrier(s) name(s) from clock [ck] *)
|
|
| 445 |
let rec clock_uncarry ck =
|
|
| 446 | 446 |
let ck = repr ck in |
| 447 | 447 |
match ck.cdesc with |
| 448 | 448 |
| Ccarrying (_, ck') -> ck' |
| 449 |
| Con(ck', cr, l) -> clock_on (clock_uncarry ck') cr l |
|
| 450 |
| Ctuple ckl -> clock_of_clock_list (List.map clock_uncarry ckl) |
|
| 449 | 451 |
| _ -> ck |
| 450 | 452 |
|
| 451 | 453 |
let try_unify ck1 ck2 loc = |
| ... | ... | |
| 557 | 559 |
in |
| 558 | 560 |
aux ck |
| 559 | 561 |
|
| 562 |
(* Computes the root clock of a tuple or a node clock, |
|
| 563 |
which is not the same as the base clock. |
|
| 564 |
Root clock will be used as the call clock |
|
| 565 |
of a given node instance *) |
|
| 566 |
let compute_root_clock ck = |
|
| 567 |
let root = Clocks.root ck in |
|
| 568 |
let branch = ref None in |
|
| 569 |
let rec aux ck = |
|
| 570 |
match (repr ck).cdesc with |
|
| 571 |
| Ctuple cl -> |
|
| 572 |
List.iter aux cl |
|
| 573 |
| Carrow (ck1,ck2) -> |
|
| 574 |
aux ck1; aux ck2 |
|
| 575 |
| _ -> |
|
| 576 |
begin |
|
| 577 |
match !branch with |
|
| 578 |
| None -> |
|
| 579 |
branch := Some (Clocks.branch ck) |
|
| 580 |
| Some br -> |
|
| 581 |
(* cannot fail *) |
|
| 582 |
branch := Some (Clocks.common_prefix br (Clocks.branch ck)) |
|
| 583 |
end |
|
| 584 |
in |
|
| 585 |
begin |
|
| 586 |
aux ck; |
|
| 587 |
Clocks.clock_of_root_branch root (Utils.desome !branch) |
|
| 588 |
end |
|
| 589 |
|
|
| 560 | 590 |
(* Clocks a list of arguments of Lustre builtin operators: |
| 561 | 591 |
- type each expression, remove carriers of clocks as |
| 562 | 592 |
carriers may only denote variables, not arbitrary expr. |
| ... | ... | |
| 658 | 688 |
let cr = |
| 659 | 689 |
match r with |
| 660 | 690 |
| None -> new_var true |
| 661 |
| Some (x, _) -> let loc_r = loc_of_cond expr.expr_loc x in |
|
| 662 |
let expr_r = expr_of_ident x loc_r in |
|
| 663 |
clock_expr env expr_r in |
|
| 691 |
| Some c -> clock_standard_args env [c] in |
|
| 664 | 692 |
let couts = clock_appl env id args cr expr.expr_loc in |
| 665 | 693 |
expr.expr_clock <- couts; |
| 666 | 694 |
couts |
| ... | ... | |
| 690 | 718 |
| Expr_merge (c,hl) -> |
| 691 | 719 |
let cvar = new_var true in |
| 692 | 720 |
let crvar = new_carrier Carry_name true in |
| 693 |
List.iter (fun (t, h) -> let ckh = clock_expr env h in unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl;
|
|
| 721 |
List.iter (fun (t, h) -> let ckh = clock_uncarry (clock_expr env h) in unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl;
|
|
| 694 | 722 |
let cr = clock_carrier env c expr.expr_loc cvar in |
| 695 | 723 |
try_unify_carrier cr crvar expr.expr_loc; |
| 696 |
expr.expr_clock <- cvar; |
|
| 697 |
cvar |
|
| 724 |
let cres = clock_current ((snd (List.hd hl)).expr_clock) in |
|
| 725 |
expr.expr_clock <- cres; |
|
| 726 |
cres |
|
| 698 | 727 |
in |
| 699 | 728 |
Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck); |
| 700 | 729 |
resulting_ck |
Also available in: Unified diff