Revision 01c7d5e1 src/clock_calculus.ml
src/clock_calculus.ml | ||
---|---|---|
685 | 685 |
List.iter (fun (t, h) -> clock_subtyping_arg env h (new_ck (Con (cvar,cr,t)) true)) hl; |
686 | 686 |
expr.expr_clock <- cvar; |
687 | 687 |
cvar |
688 |
| Expr_uclock (e,k) -> |
|
689 |
let pck = clock_expr env e in |
|
690 |
if not (can_be_pck pck) then |
|
691 |
raise (Error (e.expr_loc, Not_pck)); |
|
692 |
if k = 0 then |
|
693 |
raise (Error (expr.expr_loc, Factor_zero)); |
|
694 |
(try |
|
695 |
subsume pck (CSet_pck (k,(0,1))) |
|
696 |
with Subsume (ck,cset) -> |
|
697 |
raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (k,(0,1)))))); |
|
698 |
let ck = new_ck (Pck_up (pck,k)) true in |
|
699 |
expr.expr_clock <- ck; |
|
700 |
ck |
|
701 |
| Expr_dclock (e,k) -> |
|
702 |
let pck = clock_expr env e in |
|
703 |
if not (can_be_pck pck) then |
|
704 |
raise (Error (e.expr_loc, Not_pck)); |
|
705 |
if k = 0 then |
|
706 |
raise (Error (expr.expr_loc, Factor_zero)); |
|
707 |
(try |
|
708 |
subsume pck (CSet_pck (1,(0,1))) |
|
709 |
with Subsume (ck,cset) -> |
|
710 |
raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (1,(0,1)))))); |
|
711 |
let ck = new_ck (Pck_down (pck,k)) true in |
|
712 |
expr.expr_clock <- ck; |
|
713 |
ck |
|
714 |
| Expr_phclock (e,(a,b)) -> |
|
715 |
let pck = clock_expr env e in |
|
716 |
if not (can_be_pck pck) then |
|
717 |
raise (Error (e.expr_loc, Not_pck)); |
|
718 |
let (a,b) = simplify_rat (a,b) in |
|
719 |
(try |
|
720 |
subsume pck (CSet_pck (b,(0,1))) |
|
721 |
with Subsume (ck,cset) -> |
|
722 |
raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (b,(0,1)))))); |
|
723 |
let ck = new_ck (Pck_phase (pck,(a,b))) true in |
|
724 |
expr.expr_clock <- ck; |
|
725 |
ck |
|
726 | 688 |
in |
727 | 689 |
Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck); |
728 | 690 |
resulting_ck |
Also available in: Unified diff