From ff40d147743b1b18d701480e278388b1623fed4a Mon Sep 17 00:00:00 2001
From: June Rousseau <june.rousseau@cs.au.dk>
Date: Sun, 3 Nov 2024 16:55:09 +0100
Subject: [PATCH] feat(cerisier): tweak UI

---
 lib/interactive_ui.ml | 38 +++++++++++++++++++++++++-------------
 lib/pretty_printer.ml |  8 ++++----
 2 files changed, 29 insertions(+), 17 deletions(-)

diff --git a/lib/interactive_ui.ml b/lib/interactive_ui.ml
index d87f603..445ba2c 100644
--- a/lib/interactive_ui.ml
+++ b/lib/interactive_ui.ml
@@ -206,7 +206,7 @@ module MkUi (Cfg : MachineConfig) : Ui = struct
 
   module Identity = struct
     let width = 1 + int_of_float (floor @@ (log (float max_int) /. log 16.))
-    let ui ?(attr = A.empty) z = I.hsnap ~align:`Right width (I.string attr (Int.ui width z))
+    let ui ?(attr = A.empty) z = I.hsnap ~align:`Left width (I.string attr (Int.ui width z))
   end
 
   module ETable_panel = struct
@@ -215,14 +215,24 @@ module MkUi (Cfg : MachineConfig) : Ui = struct
        <eid>: <identity>
     *)
     let ui width (etbl : Machine.e_table) =
-      (* let eid_width = EC_counter.width + 2 + Identity.width +2 in *)
-      let render_etbl enclaves =
-        List.fold_left
-          (fun img (eid, (id, _)) ->
-            img <-> (I.empty <|> EC_counter.ui eid <|> I.string A.empty ": " <|> Identity.ui id))
-          I.empty enclaves
+      let nenclaves = 20. in
+      (* Arbitrary number *)
+      let eid_width = EC_counter.width + 2 + Identity.width + 2 in
+      let ncols = max 1 (width / eid_width) in
+      let nregs_per_col = nenclaves /. float ncols |> ceil |> int_of_float in
+      let rec loop fst_col etable =
+        if etable = [] then I.empty
+        else
+          let col, etable = CCList.take_drop nregs_per_col etable in
+          List.fold_left
+            (fun img (eid, (id, _)) ->
+              img
+              <-> ((if not fst_col then I.string A.empty "  " else I.empty)
+                  <|> EC_counter.ui eid <|> I.string A.empty ": " <|> Identity.ui id))
+            I.empty col
+          <|> loop false etable
       in
-      render_etbl (Machine.ETableMap.to_seq etbl |> List.of_seq) |> I.hsnap ~align:`Left width
+      loop true (Machine.ETableMap.to_seq etbl |> List.of_seq) |> I.hsnap ~align:`Left width
   end
 
   module Instr = struct
@@ -352,10 +362,9 @@ module MkUi (Cfg : MachineConfig) : Ui = struct
       let start_stk = upd_stk stk height start_stk 2 in
 
       let img_of_dataline = render_prog width pc (addr_show start_prog) in
-      (* let img_of_stack = *)
-      (*   if show_stack then render_stack width stk (addr_show start_stk) else I.empty *)
-      (* in *)
-      let img_of_stack = if show_stack then I.empty else I.empty in
+      let img_of_stack =
+        if show_stack then render_stack width stk (addr_show start_stk) else I.empty
+      in
 
       (img_of_dataline </> img_of_stack, start_prog, start_stk)
   end
@@ -400,7 +409,10 @@ module MkUi (Cfg : MachineConfig) : Ui = struct
           I.hsnap ~align:`Right term_width
             (I.string A.empty "machine state: " <|> Exec_state.ui (fst m))
         in
-        let img = regs_img <-> mach_state_img <-> etbl_img <-> mem_img in
+        let img =
+          I.string A.empty "REGFILE:" <-> regs_img <-> I.string A.empty "ETABLE:" <-> etbl_img
+          <-> mach_state_img <-> mem_img
+        in
         Term.image term img;
         (* watch for a relevant event *)
         let rec process_events () =
diff --git a/lib/pretty_printer.ml b/lib/pretty_printer.ml
index a4ef1d6..8f29ee2 100644
--- a/lib/pretty_printer.ml
+++ b/lib/pretty_printer.ml
@@ -100,10 +100,10 @@ let string_of_machine_op (s : machine_op) : string =
   | LoadU (r1, r2, c) -> "loadU" ^- string_of_rrc r1 r2 c
   | StoreU (r, c1, c2) -> "storeU" ^- string_of_rcc r c1 c2
   | PromoteU r -> "promoteU" ^- string_of_regname r
-  | EInit (r1, r2) -> "EInit" ^- string_of_rr r1 r2
-  | EDeInit (r1, r2) -> "EDeInit" ^- string_of_rr r1 r2
-  | EStoreId (r1, r2, r3) -> "EStoreId" ^- string_of_rrr r1 r2 r3
-  | IsUnique (r1, r2) -> "IsUnique" ^- string_of_rr r1 r2
+  | EInit (r1, r2) -> "einit" ^- string_of_rr r1 r2
+  | EDeInit (r1, r2) -> "edeinit" ^- string_of_rr r1 r2
+  | EStoreId (r1, r2, r3) -> "estoreid" ^- string_of_rrr r1 r2 r3
+  | IsUnique (r1, r2) -> "isunique" ^- string_of_rr r1 r2
   | Fail -> "fail"
   | Halt -> "halt"