Project

General

Profile

Revision d52e7821 src/clock_calculus.ml

View differences:

src/clock_calculus.ml
273 273
        end
274 274
    | _,_ -> assert false
275 275

  
276
let try_unify_carrier ck1 ck2 loc =
277
  try
278
    unify_carrier ck1 ck2
279
  with
280
  | Unify (ck1',ck2') ->
281
    raise (Error (loc, Clock_clash (ck1',ck2')))
282
  | Subsume (ck,cset) ->
283
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
284
  | Mismatch (cr1,cr2) ->
285
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
286

  
276 287
(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify
277 288
    (ck1,ck2)] if the clocks are not unifiable.*)
278 289
let rec unify ck1 ck2 =
......
459 470
  | Mismatch (cr1,cr2) ->
460 471
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
461 472

  
462
(* ck1 is a subtype of ck2 *)
473
(* ck2 is a subtype of ck1 *)
463 474
let rec sub_unify sub ck1 ck2 =
464 475
  match (repr ck1).cdesc, (repr ck2).cdesc with
465 476
  | Ctuple cl1         , Ctuple cl2         ->
......
478 489
      unify_carrier cr1 cr2;
479 490
      sub_unify sub c1 c2
480 491
    end
481
  | Ccarrying (_, c1)  , _         when sub -> sub_unify sub c1 ck2
492
  | _, Ccarrying (_, c2)           when sub -> sub_unify sub ck1 c2
482 493
  | _                                       -> unify ck1 ck2
483 494

  
484 495
let try_sub_unify sub ck1 ck2 loc =
......
495 506
(* Unifies all the clock variables in the clock type of a tuple 
496 507
   expression, so that the clock type only uses at most one clock variable *)
497 508
let unify_tuple_clock ref_ck_opt ck loc =
509
(*(match ref_ck_opt with
510
| None     -> Format.eprintf "unify_tuple_clock None %a@." Clocks.print_ck ck
511
  | Some ck' -> Format.eprintf "unify_tuple_clock (Some %a) %a@." Clocks.print_ck ck' Clocks.print_ck ck);*)
498 512
  let ck_var = ref ref_ck_opt in
499 513
  let rec aux ck =
500 514
    match (repr ck).cdesc with
......
506 520
              ck_var:=Some ck
507 521
          | Some v ->
508 522
              (* may fail *)
509
              try_unify v ck loc
523
              try_unify ck v loc
510 524
        end
511 525
    | Ctuple cl ->
512 526
        List.iter aux cl
......
514 528
    | Ccarrying (_, ck1) ->
515 529
        aux ck1
516 530
    | _ -> ()
517
  in
518
  aux ck
531
  in aux ck
519 532

  
520 533
(* Unifies all the clock variables in the clock type of an imported
521 534
   node, so that the clock type only uses at most one base clock variable,
......
531 544
              ck_var:=Some ck
532 545
          | Some v ->
533 546
              (* cannot fail *)
534
              try_unify v ck loc
547
              try_unify ck v loc
535 548
        end
536 549
    | Ctuple cl ->
537 550
        List.iter aux cl
......
587 600
  let expr_c = expr_of_ident c loc in
588 601
  let ck = clock_expr ~nocarrier:false env expr_c in
589 602
  let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in
590
  let ckcarry = new_ck (Ccarrying (cr,ce)) ck.cscoped in
603
  let ckb = new_var true in
604
  let ckcarry = new_ck (Ccarrying (cr, ckb)) ck.cscoped in
591 605
  try_unify ck ckcarry expr_c.expr_loc;
592
  ce, cr
606
  unify_tuple_clock (Some ckb) ce expr_c.expr_loc;
607
  cr
593 608

  
594 609
(** [clock_expr env expr] performs the clock calculus for expression [expr] in
595 610
    environment [env] *)
......
666 681
  | Expr_when (e,c,l) ->
667 682
      let ce = clock_standard_args env [e] in
668 683
      let c_loc = loc_of_cond expr.expr_loc c in
669
      let ck_c, cr = clock_carrier env c c_loc ce in
670
      let ck = new_ck (Con (ce,cr,l)) true in
684
      let cr = clock_carrier env c c_loc ce in
685
      let ck = clock_on ce cr l in
671 686
      let cr' = new_carrier (Carry_const c) ck.cscoped in
672
      let ck' = new_ck (Con (ce,cr',l)) true in
673
      unify_tuple_clock (Some ck_c) ce expr.expr_loc;
687
      let ck' = clock_on ce cr' l in
674 688
      expr.expr_clock <- ck';
675 689
      ck
676 690
  | Expr_merge (c,hl) ->
677 691
      let cvar = new_var true in
678
      let ck_c, cr = clock_carrier env c expr.expr_loc cvar in
679
      List.iter (fun (t, h) -> clock_subtyping_arg env h (new_ck (Con (cvar,cr,t)) true)) hl;
680
      unify_tuple_clock (Some ck_c) cvar expr.expr_loc;
692
      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;
694
      let cr = clock_carrier env c expr.expr_loc cvar in
695
      try_unify_carrier cr crvar expr.expr_loc;
681 696
      expr.expr_clock <- cvar;
682 697
      cvar
683 698
  in

Also available in: Unified diff