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