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