Project

General

Profile

Revision 01c7d5e1 src/clock_calculus.ml

View differences:

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