Fixed base clock in code generation

Put the base clock inside the equation where it 
belongs.

compiler/global/clocks.ml

@@ -138,4 +138,8 @@ let same_control ck1 ck2 = match ck_repr ck1, ck_repr ck2 with
   | Cvar {contents = Cindex i1}, Cvar {contents = Cindex i2} -> i1 = i2
   | _ -> false
 
-
+(** returns the first clock of a ct. *)
+let rec first_ck ct = match ct with
+  | Ck ck -> ck
+  | Cprod [] -> assert false
+  | Cprod (ct::_) -> first_ck ct

compiler/main/mls2obc.ml

@@ -434,9 +434,10 @@ let empty_call_context = None
     [j] obj decs
     [s] the actions used in the step method.
     [v] var decs *)
-let rec translate_eq map call_context ({ Minils.eq_lhs = pat; Minils.eq_rhs = e } as eq)
+let rec translate_eq map call_context
+    ({ Minils.eq_lhs = pat; Minils.eq_base_ck = ck; Minils.eq_rhs = e } as eq)
     (v, si, j, s) =
-  let { Minils.e_desc = desc; Minils.e_base_ck = ck; Minils.e_loc = loc } = e in
+  let { Minils.e_desc = desc; Minils.e_loc = loc } = e in
   match (pat, desc) with
     | pat, Minils.Ewhen (e,_,_) ->
         translate_eq map call_context {eq with Minils.eq_rhs = e} (v, si, j, s)

compiler/minils/analysis/clocking.ml

@@ -144,7 +144,7 @@ let rec stateful e = match e.e_desc with
   | _ -> false
 
 
-let typing_eq h { eq_lhs = pat; eq_rhs = e; eq_loc = loc } =
+let typing_eq h ({ eq_lhs = pat; eq_rhs = e; eq_loc = loc } as eq) =
   (* typing the expression, returns ct, ck_base *)
   let rec typing e =
     let ct,base = match e.e_desc with
@@ -201,7 +201,6 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e; eq_loc = loc } =
           in
           ct, base_ck
     in
-    e.e_base_ck <- base;
     (try unify ct e.e_ct
      with Unify ->
        eprintf "Inconsistent clock annotation for exp %a.@\n"
@@ -215,14 +214,15 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e; eq_loc = loc } =
      with Unify -> error_message e.e_loc (Etypeclash (actual_ct, expected_ct)));
     base
   in
-  let ct,_ = typing e in
+  let ct,base_ck = typing e in
   let pat_ct = typing_pat h pat in
   (try unify ct pat_ct
     with Unify ->
       eprintf "Incoherent clock between right and left side of the equation.@\n";
-      error_message loc (Etypeclash (ct, pat_ct)))
+      error_message loc (Etypeclash (ct, pat_ct)));
+  { eq with eq_base_ck = base_ck }
 
-let typing_eqs h eq_list = List.iter (typing_eq h) eq_list
+let typing_eqs h eq_list = List.map (typing_eq h) eq_list
 
 let append_env h vds =
   List.fold_left (fun h { v_ident = n; v_clock = ck } -> Env.add n ck h) h vds
@@ -230,34 +230,37 @@ let append_env h vds =
 
 let typing_contract h contract =
   match contract with
-    | None -> h
-    | Some { c_local = l_list;
+    | None -> None, h
+    | Some ({ c_local = l_list;
              c_eq = eq_list;
              c_assume = e_a;
              c_enforce = e_g;
-             c_controllables = c_list } ->
+             c_controllables = c_list } as contract) ->
         let h' = append_env h l_list in
         (* assumption *)
         (* property *)
-        typing_eqs h' eq_list;
+        let eq_list = typing_eqs h' eq_list in
         expect_extvalue h' Cbase e_a;
         expect_extvalue h' Cbase e_g;
-        append_env h c_list
+        let h = append_env h c_list in
+        Some { contract with c_eq = eq_list }, h
 
 
 let typing_node node =
   let h0 = append_env Env.empty node.n_input in
   let h0 = append_env h0 node.n_output in
-  let h = typing_contract h0 node.n_contract in
+  let contract, h = typing_contract h0 node.n_contract in
   let h = append_env h node.n_local in
-  typing_eqs h node.n_equs;
+  let equs = typing_eqs h node.n_equs in
   (* synchronize input and output on base : find the free vars and set them to base *)
   Env.iter (fun _ ck -> unify_ck Cbase (root_ck_of ck)) h0;
   (*update clock info in variables descriptions *)
   let set_clock vd = { vd with v_clock = ck_repr (Env.find vd.v_ident h) } in
   let node = { node with n_input = List.map set_clock node.n_input;
                          n_output = List.map set_clock node.n_output;
-                         n_local = List.map set_clock node.n_local }
+                         n_local = List.map set_clock node.n_local;
+                         n_equs = equs;
+                         n_contract = contract; }
   in
   let sign = Mls_utils.signature_of_node node in
   Check_signature.check_signature sign;

compiler/minils/analysis/interference.ml

@@ -60,6 +60,10 @@ module InterfRead = struct
     | Cbase | Cvar { contents = Cindex _ } -> acc
     | Cvar { contents = Clink ck } -> vars_ck acc ck
 
+  let rec vars_ct acc ct = match ct with
+    | Ck ck -> vars_ck acc ck
+    | Cprod ct_list -> List.fold_left vars_ct acc ct_list
+
   let rec ivar_of_extvalue w = match w.w_desc with
     | Wvar x -> Ivar x
     | Wfield(w, f) -> Ifield (ivar_of_extvalue w, f)
@@ -100,7 +104,7 @@ module InterfRead = struct
       | Eiterator (_, _, _, _, _, Some x) -> IvarSet.add (Ivar x) acc
       | _ -> acc
     in
-      e, vars_ck acc e.e_base_ck
+      e, vars_ct acc e.e_ct
 
   let rec vars_pat acc = function
     | Evarpat x -> IvarSet.add (Ivar x) acc

compiler/minils/analysis/level_clock.ml

@@ -20,9 +20,8 @@ open Minils
    indeed if it was Con (Cvar,c,x) x would have to be defined with an expression of clock Cvar.*)
 
 let eq _ acc eq =
-  let e = eq.eq_rhs in
-  let _ = match ck_repr e.e_base_ck with
-    | Cvar {contents = Cindex _} -> unify_ck e.e_base_ck e.e_level_ck
+  let _ = match ck_repr eq.eq_base_ck with
+    | Cvar {contents = Cindex _} -> unify_ck eq.eq_base_ck eq.eq_rhs.e_level_ck
     | _ -> ()
   in
   eq,acc (* no recursion since in minils exps are not recursive *)
@@ -30,4 +29,4 @@ let eq _ acc eq =
 let program p =
   let funs = { Mls_mapfold.defaults with Mls_mapfold.eq = eq } in
   let p, _ = Mls_mapfold.program_it funs [] p in
-  p
+  p

compiler/minils/minils.ml

@@ -57,7 +57,6 @@ and extvalue_desc =
 and exp = {
   e_desc            : edesc;
   e_level_ck        : ck; (*when no data dep, execute the exp on this clock (set by [switch] *)
-  mutable e_base_ck : ck;
   mutable e_ct      : ct;
   e_ty              : ty;
   e_linearity : linearity;
@@ -109,6 +108,7 @@ type eq = {
   eq_lhs    : pat;
   eq_rhs    : exp;
   eq_unsafe : bool;
+  eq_base_ck : ck;
   eq_loc    : location }
 
 type var_dec = {
@@ -196,21 +196,21 @@ let mk_vd_extvalue vd =
   mk_extvalue ~ty:vd.v_type ~linearity:vd.v_linearity
               ~clock:vd.v_clock ~loc:vd.v_loc (Wvar vd.v_ident)
 
-let mk_exp level_ck ty ~linearity ?(ck = Cbase)
+let mk_exp level_ck ty ~linearity
     ?(ct = fresh_ct ty) ?(loc = no_location) desc =
   { e_desc = desc; e_ty = ty; e_linearity = linearity;
-    e_level_ck = level_ck; e_base_ck = ck; e_ct = ct; e_loc = loc }
+    e_level_ck = level_ck; e_ct = ct; e_loc = loc }
 
 let mk_var_dec ?(loc = no_location) ident ty linearity ck =
   { v_ident = ident; v_type = ty; v_linearity = linearity;  v_clock = ck; v_loc = loc }
 
 let mk_extvalue_exp ?(clock = fresh_clock())
     ?(loc = no_location) level_ck ty ~linearity desc =
-  mk_exp ~ck:clock ~loc:loc level_ck ty ~linearity:linearity
+  mk_exp ~loc:loc level_ck ty ~linearity:linearity
     (Eextvalue (mk_extvalue ~clock:clock ~loc:loc ~linearity:linearity ~ty:ty desc))
 
-let mk_equation ?(loc = no_location) unsafe pat exp =
-  { eq_lhs = pat; eq_rhs = exp; eq_unsafe = unsafe; eq_loc = loc }
+let mk_equation ?(loc = no_location) ?(base_ck=fresh_clock()) unsafe pat exp =
+  { eq_lhs = pat; eq_rhs = exp; eq_unsafe = unsafe; eq_base_ck = base_ck; eq_loc = loc }
 
 let mk_node
     ?(input = []) ?(output = []) ?(contract = None) ?(pinst = ([],[]))

compiler/minils/mls_compare.ml

@@ -61,9 +61,6 @@ struct
     else
       let cr = Linearity.linearity_compare e1.e_linearity e2.e_linearity in
       if cr <> 0 then cr
-      else
-      let cr = C.clock_compare e1.e_base_ck e2.e_base_ck in
-      if cr <> 0 then cr
       else
         match e1.e_desc, e2.e_desc with
         | Eextvalue w1, Eextvalue w2 ->

compiler/minils/mls_mapfold.ml

@@ -41,11 +41,10 @@ let rec exp_it funs acc e = funs.exp funs acc e
 and exp funs acc e =
   let e_ty, acc = ty_it funs.global_funs acc e.e_ty in
   let e_level_ck, acc = ck_it funs.global_funs acc e.e_level_ck in
-  let e_base_ck, acc = ck_it funs.global_funs acc e.e_base_ck in
   let e_ct, acc = ct_it funs.global_funs acc e.e_ct in
   let ed, acc = edesc_it funs acc e.e_desc in
   { e with e_desc = ed; e_ty = e_ty; e_level_ck = e_level_ck;
-           e_base_ck = e_base_ck; e_ct = e_ct }, acc
+           e_ct = e_ct }, acc
 
 and extvalue_it funs acc w = funs.extvalue funs acc w
 and extvalue funs acc w =
@@ -141,8 +140,9 @@ and pat funs acc p = match p with
 and eq_it funs acc eq = funs.eq funs acc eq
 and eq funs acc eq =
   let eq_lhs, acc = pat_it funs acc eq.eq_lhs in
+  let eq_base_ck, acc = ck_it funs.global_funs acc eq.eq_base_ck in
   let eq_rhs, acc = exp_it funs acc eq.eq_rhs in
-    { eq with eq_lhs = eq_lhs; eq_rhs = eq_rhs }, acc
+    { eq with eq_lhs = eq_lhs; eq_rhs = eq_rhs; eq_base_ck = eq_base_ck }, acc
 
 and eqs_it funs acc eqs = funs.eqs funs acc eqs
 and eqs funs acc eqs = mapfold (eq_it funs) acc eqs

compiler/minils/mls_printer.ml

@@ -173,10 +173,10 @@ and print_tag_w_list ff tag_w_list =
   fprintf ff "@[%a@]" (print_list print_handler """""") tag_w_list
 
 
-and print_eq ff { eq_lhs = p; eq_rhs = e } =
+and print_eq ff { eq_lhs = p; eq_rhs = e; eq_base_ck = base_ck } =
   if !Compiler_options.full_type_info
   then fprintf ff "@[<2>%a :: %a =@ %a@]"
-    print_pat p  print_ck e.e_base_ck  print_exp e
+    print_pat p  print_ck base_ck  print_exp e
   else fprintf ff "@[<2>%a =@ %a@]" print_pat p  print_exp e
 
 

compiler/minils/mls_utils.ml

@@ -156,7 +156,7 @@ struct
 
   let antidep { eq_rhs = e } = is_fby e
 
-  let clock { eq_rhs = e } = e.e_base_ck
+  let clock eq = eq.eq_base_ck
 
   let head ck =
     let rec headrec ck l =

compiler/minils/sigali/sigalimain.ml

@@ -184,13 +184,13 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) =
 
 let rec translate_eq env f
     (acc_dep,acc_states,acc_init,acc_inputs,acc_ctrl,acc_cont,acc_eqs)
-    { Minils.eq_lhs = pat; Minils.eq_rhs = e } =
+    { Minils.eq_lhs = pat; Minils.eq_rhs = e; eq_base_ck = ck } =
 
   let prefix = f ^ "_" in
 
   let prefixed n = prefix ^ n in
 
-  let { Minils.e_desc = desc; Minils.e_base_ck = ck } = e in
+  let { Minils.e_desc = desc } = e in
   match pat, desc with
   | Minils.Evarpat(n), Minils.Efby(opt_c, e) ->
       let sn = prefixed (name n) in

compiler/minils/transformations/inline_extvalues.ml

@@ -98,14 +98,16 @@ let form_new_extvalue_node nd =
   let rec form_new_extvalue e =
     try
       let se = form_new_const e in
-      mk_extvalue ~ty:e.e_ty ~linearity:e.e_linearity ~clock:e.e_base_ck ~loc:e.e_loc (Wconst se)
+      mk_extvalue ~ty:e.e_ty ~linearity:e.e_linearity
+        ~clock:(Clocks.first_ck e.e_ct) ~loc:e.e_loc (Wconst se)
     with Errors.Fallback ->
       let w_d = match e.e_desc with
         | Eextvalue w -> w.w_desc
         | Ewhen (e, v, x) -> Wwhen (form_new_extvalue e, v, x)
         | _ -> raise Errors.Fallback
       in
-      mk_extvalue ~ty:e.e_ty ~linearity:e.e_linearity ~clock:e.e_base_ck ~loc:e.e_loc w_d
+      mk_extvalue ~ty:e.e_ty ~linearity:e.e_linearity
+        ~clock:(Clocks.first_ck e.e_ct) ~loc:e.e_loc w_d
 
   and form_new_const e =
     let se_d = match e.e_desc with
@@ -135,7 +137,7 @@ let form_new_extvalue_node nd =
 
   and form_new_const_w w =
     let mk_exp w =
-      mk_exp w.w_ck w.w_ty ~linearity:w.w_linearity ~ck:w.w_ck ~ct:(Ck w.w_ck) (Eextvalue w) in
+      mk_exp w.w_ck w.w_ty ~linearity:w.w_linearity ~ct:(Ck w.w_ck) (Eextvalue w) in
     form_new_const (mk_exp w)
 
   and form_new_extvalue_eq _ n eq = match eq.eq_rhs.e_desc with

compiler/minils/transformations/schedule_interf.ml

@@ -7,9 +7,6 @@ open Misc
 open Sgraph
 
 
-let eq_clock eq =
-  eq.eq_rhs.e_base_ck
-
 module Cost =
 struct
   open Interference_graph
@@ -76,7 +73,10 @@ struct
             min_same_ck (min_eq, min_c, min_same_ctrl) l
     in
     let eqs_wcost =
-      List.map (fun eq -> (eq, cost eq, Clocks.same_control (eq_clock eq) ck)) rem_eqs in
+      List.map
+        (fun eq -> (eq, cost eq, Clocks.same_control (Mls_utils.Vars.clock eq) ck))
+        rem_eqs
+    in
     let (eq, c, same_ctrl), eqs_wcost = Misc.assert_1min eqs_wcost in
     min_same_ck (eq, c, same_ctrl) eqs_wcost
 end
@@ -125,7 +125,7 @@ let schedule eq_list inputs node_list =
         let rem_eqs = free_eqs node_list in
         (* compute new costs for the next step *)
         let costs = Cost.update_cost eq uses costs in
-          schedule_aux rem_eqs (eq::sched_eqs) node_list (eq_clock eq) costs
+          schedule_aux rem_eqs (eq::sched_eqs) node_list (Mls_utils.Vars.clock eq) costs
   in
   let costs = Cost.init_cost uses inputs in
   let rem_eqs = free_eqs node_list in

compiler/minils/transformations/tomato.ml

@@ -211,7 +211,7 @@ let rec add_equation is_input (tenv : tom_env) eq =
         let ed, add_when, when_count, class_id_list = decompose e' in
         ed, (fun e' -> { e with e_desc = Ewhen (add_when e', cn, x) }), when_count + 1,
         class_ref_of_var is_input
-          (mk_extvalue ~clock:e'.e_base_ck ~ty:Initial.tbool
+          (mk_extvalue ~clock:(Clocks.first_ck e'.e_ct) ~ty:Initial.tbool
                        ~linearity:Linearity.Ltop (Wvar x)) x
         :: class_id_list
 
@@ -219,7 +219,7 @@ let rec add_equation is_input (tenv : tom_env) eq =
         let class_id_list, clause_list = mapfold_right add_clause clause_list [] in
         let x_id =
           class_ref_of_var is_input
-            (mk_extvalue ~clock:e.e_base_ck ~ty:Initial.tbool
+            (mk_extvalue ~clock:(Clocks.first_ck e.e_ct) ~ty:Initial.tbool
                          ~linearity:Linearity.Ltop (Wvar x)) x
         in
         Emerge (dummy_var, clause_list), id, 0, x_id :: class_id_list
@@ -363,12 +363,11 @@ let rec reconstruct ((tenv, cenv) as env) mapping =
         Misc.take (List.length repr.er_children - repr.er_when_count) repr.er_children in
 
       let ed = reconstruct_exp_desc mapping repr.er_head.e_desc repr.er_children in
-      let ck = reconstruct_clock mapping repr.er_head.e_base_ck in
       let level_ck =
         reconstruct_clock mapping repr.er_head.e_level_ck in (* not strictly needed, done for
                                                             consistency reasons *)
       let ct = reconstruct_clock_type mapping repr.er_head.e_ct in
-      { repr.er_head with e_desc = ed; e_base_ck = ck; e_level_ck = level_ck; e_ct = ct; } in
+      { repr.er_head with e_desc = ed; e_level_ck = level_ck; e_ct = ct; } in
 
     let e = repr.er_add_when e in
 
@@ -577,7 +576,7 @@ let rec fix_output_var_dec mapping vd (seen, equs, vd_list) =
       mk_equation false
         (Evarpat new_id)
         (mk_exp new_clock vd.v_type ~ct:(Ck new_clock)
-           ~ck:new_clock ~linearity:Linearity.Ltop (Eextvalue w))
+            ~linearity:Linearity.Ltop (Eextvalue w))
     in
     (seen, new_eq :: equs, new_vd :: vd_list)
   else