Revision 6fdfb60b 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