Project

General

Profile

Revision d3e4c22f src/clock_calculus.ml

View differences:

src/clock_calculus.ml
519 519
  | Mismatch (cr1,cr2) ->
520 520
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
521 521

  
522
(* Checks whether ck1 is a subtype of ck2 *)
523
let rec clock_subtyping ck1 ck2 =
522
(* ck1 is a subtype of ck2 *)
523
let rec sub_unify sub ck1 ck2 =
524 524
  match (repr ck1).cdesc, (repr ck2).cdesc with
525
  | Ccarrying _         , Ccarrying _ -> unify ck1 ck2
526
  | Ccarrying (cr', ck'), _           -> unify ck' ck2
527
  | _                                 -> unify ck1 ck2
525
  | Ctuple [c1]        , Ctuple [c2]        -> sub_unify sub c1 c2
526
  | Ctuple cl1         , Ctuple cl2         ->
527
    if List.length cl1 <> List.length cl2
528
    then raise (Unify (ck1, ck2))
529
    else List.iter2 (sub_unify sub) cl1 cl2
530
  | Ctuple [c1]        , _                  -> sub_unify sub c1 ck2
531
  | _                  , Ctuple [c2]        -> sub_unify sub ck1 c2
532
  | Con (c1, cr1, t1)  , Con (c2, cr2, t2) when t1=t2 ->
533
    begin
534
      unify_carrier cr1 cr2;
535
      sub_unify sub c1 c2
536
    end
537
  | Ccarrying (cr1, c1), Ccarrying (cr2, c2)->
538
    begin
539
      unify_carrier cr1 cr2;
540
      sub_unify sub c1 c2
541
    end
542
  | Ccarrying (_, c1)  , _         when sub -> sub_unify sub c1 ck2
543
  | _                                       -> unify ck1 ck2
544

  
545
let try_sub_unify sub ck1 ck2 loc =
546
  try
547
    sub_unify sub ck1 ck2
548
  with
549
  | Unify (ck1',ck2') ->
550
    raise (Error (loc, Clock_clash (ck1',ck2')))
551
  | Subsume (ck,cset) ->
552
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
553
  | Mismatch (cr1,cr2) ->
554
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
528 555

  
529 556
(* Clocks a list of arguments of Lustre builtin operators:
530 557
   - type each expression, remove carriers of clocks as
......
539 566

  
540 567
(* emulates a subtyping relation between clocks c and (cr : c),
541 568
   used during node application only *)
542
and clock_subtyping_arg env real_arg formal_clock =
569
and clock_subtyping_arg env ?(sub=true) real_arg formal_clock =
543 570
  let loc = real_arg.expr_loc in
544 571
  let real_clock = clock_expr env real_arg in
545
  try
546
    clock_subtyping real_clock formal_clock
547
  with
548
  | Unify (ck1',ck2') ->
549
    raise (Error (loc, Clock_clash (real_clock, formal_clock)))
550
  | Subsume (ck,cset) ->
551
    raise (Error (loc, Clock_set_mismatch (ck, cset)))
552
  | Mismatch (cr1,cr2) ->
553
    raise (Error (loc, Carrier_mismatch (cr1, cr2)))
572
  try_sub_unify sub real_clock formal_clock loc
554 573

  
555 574
(* computes clocks for node application *)
556 575
and clock_appl env f args clock_reset loc =
......
779 798
  let ck_outs = clock_of_vlist nd.node_outputs in
780 799
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
781 800
  unify_imported_clock None ck_node;
782
  (*Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);*)
801
  Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
783 802
  (* Local variables may contain first-order carrier variables that should be generalized.
784 803
     That's not the case for types. *)
785 804
  List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs;
......
789 808
(*  if (is_main && is_polymorphic ck_node) then
790 809
    raise (Error (loc,(Cannot_be_polymorphic ck_node)));
791 810
*)
811
  Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
792 812
  nd.node_clock <- ck_node;
793 813
  Env.add_value env nd.node_id ck_node
794 814

  
......
832 852
  nd.nodei_clock <- ck_node;
833 853
  Env.add_value env nd.nodei_id ck_node
834 854

  
835
let clock_function env loc fcn =
836
  let new_env = clock_var_decl_list env false fcn.fun_inputs in
837
  ignore(clock_var_decl_list new_env false fcn.fun_outputs);
838
  let ck_ins = clock_of_vlist fcn.fun_inputs in
839
  let ck_outs = clock_of_vlist fcn.fun_outputs in
840
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
841
  unify_imported_clock None ck_node;
842
  check_imported_pclocks loc ck_node;
843
  try_generalize ck_node loc;
844
  Env.add_value env fcn.fun_id ck_node
845

  
846 855
let clock_top_consts env clist =
847 856
  List.fold_left (fun env cdecl ->
848 857
    let ck = new_var false in
......
855 864
    clock_node env decl.top_decl_loc nd
856 865
  | ImportedNode nd ->
857 866
    clock_imported_node env decl.top_decl_loc nd
858
  | ImportedFun fcn ->
859
    clock_function env decl.top_decl_loc fcn
860 867
  | Consts clist ->
861 868
    clock_top_consts env clist
862 869
  | Open _ ->
......
891 898
      uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)
892 899
  | ImportedNode nd ->
893 900
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
894
  | ImportedFun nd ->
895
      ()
896 901
  | Consts clist -> ()
897 902
  | Open _  -> ()
898 903

  

Also available in: Unified diff