From 56511d90186e080e2f695ffbabe2a62dbd662f26 Mon Sep 17 00:00:00 2001
From: 702fbtngus <702fbtngus@kaist.ac.kr>
Date: Thu, 12 Sep 2024 21:57:15 +0900
Subject: [PATCH] Added postprocess & merge pop and assert

---
 spectec/src/il2al/dune            |  1 +
 spectec/src/il2al/postprocess.ml  | 58 +++++++++++++++++++++++++++++++
 spectec/src/il2al/postprocess.mli |  1 +
 spectec/src/il2al/translate.ml    |  8 ++---
 4 files changed, 62 insertions(+), 6 deletions(-)
 create mode 100644 spectec/src/il2al/postprocess.ml
 create mode 100644 spectec/src/il2al/postprocess.mli

diff --git a/spectec/src/il2al/dune b/spectec/src/il2al/dune
index 296c058f43..0e7f5aa545 100644
--- a/spectec/src/il2al/dune
+++ b/spectec/src/il2al/dune
@@ -9,6 +9,7 @@
     transpile
     free
     preprocess
+    postprocess
     il_walk
     encode
     def
diff --git a/spectec/src/il2al/postprocess.ml b/spectec/src/il2al/postprocess.ml
new file mode 100644
index 0000000000..e4c0fe0978
--- /dev/null
+++ b/spectec/src/il2al/postprocess.ml
@@ -0,0 +1,58 @@
+open Al
+open Ast
+(* open Free *)
+(* open Al_util *)
+(* open Printf *)
+open Util
+open Source
+(* open Def *)
+(* open Il2al_util *)
+
+let rec merge_pop_assert' instrs =
+  let rec merge_helper acc = function
+    | ({ it = AssertI ({ it = TopValueE None; _ } as e1); _ } as i1) ::
+    ({ it = PopI e2; _ } as i2) ::
+    ({ it = AssertI ({ it = BinE (EqOp, e31, e32); _ }); _ } as i3) :: il ->
+      (match e2.it with
+      | CaseE ([{ it = El.Atom.Atom ("CONST" | "VCONST"); _ }]::_ as mixop, hd::tl)
+      when Eq.eq_expr e31 hd ->
+        let e1 = { e1 with it = TopValueE (Some e32) } in
+        let i1 = { i1 with it = AssertI e1 } in
+        let e2 = { e2 with it = CaseE (mixop, e32::tl) } in
+        let i2 = { i2 with it = PopI e2 } in
+        merge_helper (i2 :: i1 :: acc) il
+      | _ -> merge_helper (i1 :: acc) (i2 :: i3 :: il)
+      )
+    | i :: il -> merge_helper (i :: acc) il
+    | [] -> List.rev acc
+  in
+  let instrs = merge_helper [] instrs in
+  List.map (fun i ->
+    let it =
+      match i.it with
+      | IfI (e, il1, il2) -> IfI (e, merge_pop_assert' il1, merge_pop_assert' il2)
+      | EitherI (il1, il2) -> EitherI (merge_pop_assert' il1, merge_pop_assert' il2)
+      | EnterI (e1, e2, il) -> EnterI (e1, e2, merge_pop_assert' il)
+      | OtherwiseI (il) -> OtherwiseI (merge_pop_assert' il)
+      | instr -> instr
+    in
+    { i with it }
+  ) instrs
+
+
+let merge_pop_assert algo =
+  let it =
+    match algo.it with
+    | RuleA (name, anchor, args, instrs) ->
+      RuleA (name, anchor, args, merge_pop_assert' instrs)
+    | FuncA (name, args, instrs) ->
+      FuncA (name, args, merge_pop_assert' instrs)
+  in
+  { algo with it }
+
+
+let postprocess (al: Al.Ast.algorithm list) : Al.Ast.algorithm list =
+  al
+  |> List.map Transpile.remove_state
+  |> List.map merge_pop_assert
+  
\ No newline at end of file
diff --git a/spectec/src/il2al/postprocess.mli b/spectec/src/il2al/postprocess.mli
new file mode 100644
index 0000000000..7ef823c139
--- /dev/null
+++ b/spectec/src/il2al/postprocess.mli
@@ -0,0 +1 @@
+val postprocess: Al.Ast.algorithm list -> Al.Ast.algorithm list
diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml
index d3e4bd676a..5f77555c1a 100644
--- a/spectec/src/il2al/translate.ml
+++ b/spectec/src/il2al/translate.ml
@@ -369,12 +369,8 @@ let cond_of_pop_value e =
   let at = e.at in
   let bt = boolT in
   match e.it with
-  | CaseE (op, [t; _]) ->
-    (match get_atom op with
-    | Some {it = Il.Atom "CONST"; _} -> topValueE (Some t) ~note:bt
-    | Some {it = Il.Atom "VCONST"; _} -> topValueE (Some t) ~note:bt
-    | _ -> topValueE None ~note:bt
-    )
+  | CaseE (_op, [_t; _]) ->
+    topValueE None ~note:bt
   | GetCurFrameE ->
     topFrameE () ~at:at ~note:bt
   | GetCurLabelE ->