Project

General

Profile

Revision 45c13277 src/clock_calculus.ml

View differences:

src/clock_calculus.ml
430 430
      (Const_int i) -> i
431 431
  | _ -> failwith "Internal error: int_factor_of_expr"
432 432

  
433
(* Unifies all the clock variables in the clock type of a tuple 
434
   expression, so that the clock type only uses at most one clock variable *)
435
let unify_tuple_clock ref_ck_opt ck =
436
  let ck_var = ref ref_ck_opt in
437
  let rec aux ck =
438
    match (repr ck).cdesc with
439
    | Con _
440
    | Cvar _ ->
441
        begin
442
          match !ck_var with
443
          | None ->
444
              ck_var:=Some ck
445
          | Some v ->
446
              (* may fail *)
447
              unify v ck
448
        end
449
    | Ctuple cl ->
450
        List.iter aux cl
451
    | Carrow _ -> assert false (* should not occur *)
452
    | Ccarrying (_, ck1) ->
453
        aux ck1
454
    | _ -> ()
455
  in
456
  aux ck
457

  
458
(* Unifies all the clock variables in the clock type of an imported
459
   node, so that the clock type only uses at most one base clock variable,
460
   that is, the activation clock of the node *)
461
let unify_imported_clock ref_ck_opt ck =
462
  let ck_var = ref ref_ck_opt in
463
  let rec aux ck =
464
    match (repr ck).cdesc with
465
    | Cvar _ ->
466
        begin
467
          match !ck_var with
468
          | None ->
469
              ck_var:=Some ck
470
          | Some v ->
471
              (* cannot fail *)
472
              unify v ck
473
        end
474
    | Ctuple cl ->
475
        List.iter aux cl
476
    | Carrow (ck1,ck2) ->
477
        aux ck1; aux ck2
478
    | Ccarrying (_, ck1) ->
479
        aux ck1
480
    | Con (ck1, _, _) -> aux ck1
481
    | _ -> ()
482
  in
483
  aux ck
484

  
485 433
(** [clock_uncarry ck] drops the possible carrier name from clock [ck] *)
486 434
let clock_uncarry ck =
487 435
  let ck = repr ck in
......
544 492
  | Mismatch (cr1,cr2) ->
545 493
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
546 494

  
495
(* Unifies all the clock variables in the clock type of a tuple 
496
   expression, so that the clock type only uses at most one clock variable *)
497
let unify_tuple_clock ref_ck_opt ck loc =
498
  let ck_var = ref ref_ck_opt in
499
  let rec aux ck =
500
    match (repr ck).cdesc with
501
    | Con _
502
    | Cvar _ ->
503
        begin
504
          match !ck_var with
505
          | None ->
506
              ck_var:=Some ck
507
          | Some v ->
508
              (* may fail *)
509
              try_unify v ck loc
510
        end
511
    | Ctuple cl ->
512
        List.iter aux cl
513
    | Carrow _ -> assert false (* should not occur *)
514
    | Ccarrying (_, ck1) ->
515
        aux ck1
516
    | _ -> ()
517
  in
518
  aux ck
519

  
520
(* Unifies all the clock variables in the clock type of an imported
521
   node, so that the clock type only uses at most one base clock variable,
522
   that is, the activation clock of the node *)
523
let unify_imported_clock ref_ck_opt ck loc =
524
  let ck_var = ref ref_ck_opt in
525
  let rec aux ck =
526
    match (repr ck).cdesc with
527
    | Cvar _ ->
528
        begin
529
          match !ck_var with
530
          | None ->
531
              ck_var:=Some ck
532
          | Some v ->
533
              (* cannot fail *)
534
              try_unify v ck loc
535
        end
536
    | Ctuple cl ->
537
        List.iter aux cl
538
    | Carrow (ck1,ck2) ->
539
        aux ck1; aux ck2
540
    | Ccarrying (_, ck1) ->
541
        aux ck1
542
    | Con (ck1, _, _) -> aux ck1
543
    | _ -> ()
544
  in
545
  aux ck
546

  
547 547
(* Clocks a list of arguments of Lustre builtin operators:
548 548
   - type each expression, remove carriers of clocks as
549 549
     carriers may only denote variables, not arbitrary expr.
......
577 577
  let cins, couts = split_arrow cfun in
578 578
  let cins = clock_list_of_clock cins in
579 579
  List.iter2 (clock_subtyping_arg env) args cins;
580
  unify_imported_clock (Some clock_reset) cfun;
580
  unify_imported_clock (Some clock_reset) cfun loc;
581 581
  couts
582 582

  
583 583
and clock_ident nocarrier env id loc =
......
589 589
  let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in
590 590
  let ckcarry = new_ck (Ccarrying (cr,ce)) ck.cscoped in
591 591
  try_unify ck ckcarry expr_c.expr_loc;
592
  cr
592
  ce, cr
593 593

  
594 594
(** [clock_expr env expr] performs the clock calculus for expression [expr] in
595 595
    environment [env] *)
......
632 632
    let ck_c = clock_standard_args env [c] in
633 633
    let ck = clock_standard_args env [t; e] in
634 634
    (* Here, the branches may exhibit a tuple clock, not the condition *)
635
    unify_tuple_clock (Some ck_c) ck;
635
    unify_tuple_clock (Some ck_c) ck expr.expr_loc;
636 636
    expr.expr_clock <- ck;
637 637
    ck
638 638
  | Expr_appl (id, args, r) ->
......
656 656
  | Expr_fby (e1,e2)
657 657
  | Expr_arrow (e1,e2) ->
658 658
    let ck = clock_standard_args env [e1; e2] in
659
    unify_tuple_clock None ck;
659
    unify_tuple_clock None ck expr.expr_loc;
660 660
    expr.expr_clock <- ck;
661 661
    ck
662 662
  | Expr_pre e -> (* todo : deal with phases as in tail ? *)
......
666 666
  | Expr_when (e,c,l) ->
667 667
      let ce = clock_standard_args env [e] in
668 668
      let c_loc = loc_of_cond expr.expr_loc c in
669
      let cr = clock_carrier env c c_loc ce in
669
      let ck_c, cr = clock_carrier env c c_loc ce in
670 670
      let ck = new_ck (Con (ce,cr,l)) true in
671 671
      let cr' = new_carrier (Carry_const c) ck.cscoped in
672 672
      let ck' = new_ck (Con (ce,cr',l)) true in
673
      unify_tuple_clock (Some ck_c) ce expr.expr_loc;
673 674
      expr.expr_clock <- ck';
674 675
      ck
675 676
  | Expr_merge (c,hl) ->
676 677
      let cvar = new_var true in
677
      let cr = clock_carrier env c expr.expr_loc cvar in
678
      let ck_c, cr = clock_carrier env c expr.expr_loc cvar in
678 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;
679 681
      expr.expr_clock <- cvar;
680 682
      cvar
681 683
  in
......
759 761
  let ck_ins = clock_of_vlist nd.node_inputs in
760 762
  let ck_outs = clock_of_vlist nd.node_outputs in
761 763
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
762
  unify_imported_clock None ck_node;
764
  unify_imported_clock None ck_node loc;
763 765
  Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
764 766
  (* Local variables may contain first-order carrier variables that should be generalized.
765 767
     That's not the case for types. *)
......
810 812
  let ck_ins = clock_of_vlist nd.nodei_inputs in
811 813
  let ck_outs = clock_of_vlist nd.nodei_outputs in
812 814
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
813
  unify_imported_clock None ck_node;
815
  unify_imported_clock None ck_node loc;
814 816
  check_imported_pclocks loc ck_node;
815 817
  try_generalize ck_node loc;
816 818
  nd.nodei_clock <- ck_node;

Also available in: Unified diff