Project

General

Profile

Revision 89b9e25c src/clock_calculus.ml

View differences:

src/clock_calculus.ml
743 743
(* Clocks a variable declaration *)
744 744
let clock_var_decl scoped env vdecl =
745 745
  let ck = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in
746
  let ck = 
746
  let ck =
747
(* WTF ????
747 748
    if vdecl.var_dec_const
748 749
    then
749 750
      (try_generalize ck vdecl.var_loc; ck)
750 751
    else
751
      match vdecl.var_type.Types.tdesc with
752
      | Types.Tclock _ -> new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped
753
      | _              -> ck in
752
 *)
753
      if Types.is_clock_type vdecl.var_type
754
      then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped
755
      else ck in
754 756
  vdecl.var_clock <- ck;
755 757
  Env.add_value env vdecl.var_id ck
756 758

  
......
759 761
  List.fold_left (clock_var_decl scoped) env l
760 762

  
761 763
(** [clock_node env nd] performs the clock-calculus for node [nd] in
762
    environment [env]. *)
764
    environment [env].
765
    Generalization of clocks wrt scopes follows this rule:
766
    - generalize inputs (unscoped).
767
    - generalize outputs. As they are scoped, only clocks coming from inputs
768
      are allowed to be generalized.
769
    - generalize locals. As outputs don't depend on them (checked the step before),
770
      they can be generalized. 
771
 *)
763 772
let clock_node env loc nd =
764 773
  (* let is_main = nd.node_id = !Options.main_node in *)
765 774
  let new_env = clock_var_decl_list env false nd.node_inputs in
766 775
  let new_env = clock_var_decl_list new_env true nd.node_outputs in
767
  let new_env = clock_var_decl_list new_env true nd.node_locals in
776
  let new_env = clock_var_decl_list new_env false nd.node_locals in
768 777
  List.iter (clock_eq new_env) nd.node_eqs;
769 778
  let ck_ins = clock_of_vlist nd.node_inputs in
770 779
  let ck_outs = clock_of_vlist nd.node_outputs in
771 780
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
772 781
  unify_imported_clock None ck_node;
773 782
  (*Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);*)
774
  try_generalize ck_node loc;
783
  (* Local variables may contain first-order carrier variables that should be generalized.
784
     That's not the case for types. *)
785
  List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs;
786
  List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;
787
  List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;
775 788
  (* TODO : Xavier pourquoi ai je cette erreur ? *)
776 789
(*  if (is_main && is_polymorphic ck_node) then
777 790
    raise (Error (loc,(Cannot_be_polymorphic ck_node)));
......
861 874
   Once restored in this formulation, clocks may be meaningfully printed.
862 875
*)
863 876
let uneval_vdecl_generics vdecl =
877
 (*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@." Printers.pp_node_var vdecl;*)
864 878
 if Types.is_clock_type vdecl.var_type
865 879
 then
866 880
   match get_carrier_name vdecl.var_clock with
......
873 887
let uneval_top_generics decl =
874 888
  match decl.top_decl_desc with
875 889
  | Node nd ->
876
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
890
      (* A node could contain first-order carrier variable in local vars. This is not the case for types. *)
891
      uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)
877 892
  | ImportedNode nd ->
878 893
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
879 894
  | ImportedFun nd ->

Also available in: Unified diff