Insert frame based on the variable f

spectec/src/il2al/translate.ml

@@ -105,7 +105,7 @@ let rec insert_instrs target il =
 
 (** Translation *)
 
-(* `Il.atom` -> `atom` *) 
+(* `Il.atom` -> `atom` *)
 let translate_atom atom = atom.it, atom.note.Il.Atom.def
 
 (* `Il.iter` -> `iter` *)
@@ -779,7 +779,8 @@ let translate_helper partial_funcs def =
     in
     let blocks = List.map (translate_helper_body name) unified_clauses in
     let body =
-      letI (varE "f", getCurFrameE ()) :: Transpile.merge_blocks blocks
+      Transpile.merge_blocks blocks
+      |> Transpile.insert_frame_binding
       |> Transpile.enhance_readability
       |> (if List.mem id partial_funcs then Fun.id else Transpile.ensure_return)
       |> Transpile.flatten_if in
@@ -805,8 +806,8 @@ let translate_helpers il =
 
 let rec kind_of_context e =
   match e.it with
-  | Il.CaseE ([{it = Il.Atom "FRAME_"; _} as atom]::_, _) -> translate_atom atom 
-  | Il.CaseE ([{it = Il.Atom "LABEL_"; _} as atom]::_, _) -> translate_atom atom 
+  | Il.CaseE ([{it = Il.Atom "FRAME_"; _} as atom]::_, _) -> translate_atom atom
+  | Il.CaseE ([{it = Il.Atom "LABEL_"; _} as atom]::_, _) -> translate_atom atom
   | Il.CaseE ([[]; [{it = Il.Semicolon; _}]; []], e')
   | Il.ListE [ e' ]
   | Il.TupE [_ (* z *); e'] -> kind_of_context e'
@@ -1078,7 +1079,8 @@ and translate_rgroup (instr_name, rgroup) =
       al_params
   in
   let body =
-    letI (varE "f", getCurFrameE ()) :: instrs
+    instrs
+    |> Transpile.insert_frame_binding
     |> insert_nop
     |> Transpile.enhance_readability
     |> Transpile.infer_assert

spectec/src/il2al/transpile.ml

@@ -288,7 +288,7 @@ let remove_dead_assignment il =
           let bindings = free_expr e11 @ free_expr e12 in
           let get_bounds_iters e =
             match e.it with
-            | IterE (_, _, ListN (e_iter, _)) -> free_expr e_iter 
+            | IterE (_, _, ListN (e_iter, _)) -> free_expr e_iter
             | _ -> IdSet.empty
           in
           let bounds_iters = (get_bounds_iters e11) @ (get_bounds_iters e12) in
@@ -439,7 +439,7 @@ let flatten_if instrs =
       Walk.default_config with
       post_instr = lift flatten_if';
     } in
-  
+
   Walk.walk_instrs walk_config instrs
 
 let rec mk_access ps base =
@@ -549,6 +549,26 @@ let insert_state_binding algo =
     RuleA (name, params, body)
   | _ -> algo
 
+let insert_frame_binding instrs =
+  let frame_count = ref 0 in
+
+  let count_frame e =
+    (match e.it with
+    | VarE "f" -> frame_count := !frame_count + 1
+    | _ -> ());
+    e
+  in
+
+  let walk_config =
+    {
+      Walk.default_config with
+      pre_expr = count_frame;
+    }
+  in
+
+  match Walk.walk_instrs walk_config instrs with
+  | il when !frame_count > 0 -> (letI (varE "f", getCurFrameE ())) :: il
+  | _ -> instrs
 
 (* Applied for reduction rules: infer assert from if *)
 let count_if instrs =
@@ -634,7 +654,7 @@ let remove_enter algo =
         begin match e_arity.it with
         | NumE z when Z.to_int z = 0 ->
             pushI e_frame ~at:instr.at :: il @ [ popI e_frame ~at:instr.at ]
-        | _ -> 
+        | _ ->
             let e_tmp = iterE (varE ("val"), [ "val" ], List) in
             pushI e_frame ~at:instr.at :: il @ [
               popallI e_tmp ~at:instr.at;
@@ -648,7 +668,7 @@ let remove_enter algo =
         pushI e_frame ~at:instr.at :: il @ [ popI e_frame ~at:instr.at ]
     | _ -> [ instr ]
   in
-  
+
   let enter_frame_to_push instr =
     match instr.it with
     | EnterI (e_frame, { it = ListE ([ { it = CaseE ((Atom.Atom "FRAME_", _), []); _ } ]); _ }, il) ->

spectec/src/il2al/transpile.mli

@@ -7,6 +7,7 @@ val enhance_readability : instr list -> instr list
 val flatten_if : instr list -> instr list
 val remove_state : algorithm -> algorithm
 val insert_state_binding : algorithm -> algorithm
+val insert_frame_binding : instr list -> instr list
 val remove_sub : expr -> expr
 val infer_assert : instr list -> instr list
 val ensure_return :  instr list -> instr list