real good switch fix.

The order switch then reset was wrong, since some reset reset slower inner blocks and equations, to have reset correct after switch it would have been necessary to sample the reset condition correctly (use r when c) using the level_ck... anyway the order seems now irrelevant considering code size.

compiler/heptagon/main/hept_compiler.ml

@@ -44,12 +44,12 @@ let compile_program p =
   (* Shared variables (last) *)
   let p = pass "Last" true Last.program p pp in
 
-  (* Remove switch statements *)
-  let p = pass "switch" true Switch.program p pp in
-
   (* Reset *)
   let p = pass "Reset" true Reset.program p pp in
 
+  (* Remove switch statements *)
+  let p = pass "switch" true Switch.program p pp in
+
   (* Every *)
   let p = pass "Every" true Every.program p pp in
 

compiler/heptagon/transformations/reset.ml

@@ -94,8 +94,8 @@ let eqdesc funs (res,stateful) = function
       else ( (* recursive call to remove useless resets *)
         let b, _ = Hept_mapfold.block_it funs (res,stateful) b in
         Eblock(b), (res,stateful))
-  | Eswitch _ | Eautomaton _ | Epresent _ ->
-      Format.eprintf "[reset] should be done after [switch automaton present]";
+  | Eautomaton _ | Epresent _ ->
+      Format.eprintf "[reset] should be done after [automaton present]";
       assert false
   | _ -> raise Errors.Fallback
 

compiler/heptagon/transformations/switch.ml

@@ -124,10 +124,12 @@ let level_up defnames constr h =
   let ident_level_up n new_h =
     let old_n = rename n h in
     let new_n = fresh_case_var (Idents.name old_n) constr in
-    add n new_n new_h in
+    add n new_n new_h
+  in
   fold (fun n _ new_h -> ident_level_up n new_h) defnames empty
 
-let add_to_vds vd_env locals h =
+(* only use of [vd_env] is here to create y_Up with the same type as y, etc. *)
+let add_to_locals vd_env locals h =
   let add_one n nn (locals,vd_env) =
     let orig_vd = Idents.Env.find n vd_env in
     let vd_nn = mk_var_dec nn orig_vd.v_type in
@@ -180,7 +182,6 @@ let eqdesc funs (vd_env,env,h) eqd = match eqd with
 
       (* typing have proved that defined variables are the same among states *)
       let defnames = (List.hd sw_h_l).w_block.b_defnames in
-      let defnames = Rename.rename_defnames defnames h in
 
       (* deal with the handlers *)
       let switch_handler (c_h_l, locals, equs, vd_env) sw_h =
@@ -189,7 +190,7 @@ let eqdesc funs (vd_env,env,h) eqd = match eqd with
         let h = Rename.level_up defnames constr h in
         let env = Env.level_up constr ck env in
         (* add to the locals the new vars from leveling_up *)
-        let locals,vd_env = Rename.add_to_vds vd_env locals h in
+        let locals,vd_env = Rename.add_to_locals vd_env locals h in
         (* mapfold with updated envs *)
         let b_eq, (_,_,h) = block_it funs (vd_env,env,h) sw_h.w_block in
         (* inline the handler as a block *)
@@ -202,16 +203,15 @@ let eqdesc funs (vd_env,env,h) eqd = match eqd with
       in
 
       (* create a merge equation for each defnames *)
-      let new_merge n equs =
-        let ty = (Idents.Env.find n defnames) in
-        let c_h_to_c_e (constr,h) =
-          constr, mk_exp (Evar (Rename.rename n h)) ty in
+      let new_merge n ty equs =
+        let c_h_to_c_e (constr,h) = constr, mk_exp (Evar(Rename.rename n h)) ty in
         let c_e_l = List.map c_h_to_c_e c_h_l in
         let merge = mk_exp (Emerge (ck, c_e_l)) ty in
-        (mk_equation (Eeq (Evarpat n, merge))) :: equs
+        (mk_equation (Eeq (Evarpat (Rename.rename n h), merge))) :: equs
       in
       let equs =
-        Idents.Env.fold (fun n _ equs -> new_merge n equs) defnames equs in
+        Idents.Env.fold (fun n ty equs -> new_merge n ty equs) defnames equs
+      in
      
         (* return the transformation in a block *)
       let b = mk_block ~defnames:defnames ~locals:locals equs in

test/good/autohiera.ept

@@ -0,0 +1,28 @@
+node count() returns (o : int)
+let
+  o = 0 fby (o + 1);
+tel
+
+node main(x : bool) returns (d : bool)
+var last c : bool = false;
+let
+  d = c;
+  automaton
+    state One
+      var last xone : bool = false;
+      do
+        automaton
+          state A
+            do c = xone & x;
+               xone = true;
+            until count() = 2 then B
+          state B
+            do
+            until count() = 3 then A
+        end 
+      until count() = 5 then Two
+    state Two
+      do c = x;
+      until count() = 3 then One
+  end
+tel

test/good/autohiera2.ept

@@ -0,0 +1,24 @@
+node count() returns (o : int)
+let
+  o = 0 fby (o + 1);
+tel
+
+node main(x : bool) returns (c : bool)
+let
+  automaton
+    state One
+      do
+        automaton
+          state A
+            do c = x;
+            until count() = 2 then B
+          state B
+            do c = not(x);
+            until true then A
+        end 
+      until true then Two
+    state Two
+      do c = x;
+      until true then One
+  end
+tel