Skip to content

Commit ff43526

Browse files
committed
[spectec] Remove unnecessary push and pop of frame
1 parent 55d3203 commit ff43526

1 file changed

Lines changed: 3 additions & 2 deletions

File tree

spectec/src/il2al/transpile.ml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1166,8 +1166,9 @@ let handle_unframed_algo instrs =
11661166

11671167
let post_instr instr =
11681168
let ret =
1169-
match !frame_arg with
1170-
| Some { it = ExpA f; _ } ->
1169+
match instr.it, !frame_arg with
1170+
| IfI _, _ -> [instr]
1171+
| _, Some { it = ExpA f; _ } -> (* Ignore if current instr is IfI *)
11711172
let zeroE = natE Z.zero ~note:natT in
11721173
let frame = frameE (zeroE, postprocess_frame f) ~at:f.at ~note:evalctxT in
11731174
let _f = frameE (zeroE, varE "_f" ~note:f.note) ~note:evalctxT in

0 commit comments

Comments
 (0)