Revision 0038002e 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