From 8b4f1bcfb1cf9932d2971854b9444bff30db38fa Mon Sep 17 00:00:00 2001
From: Artem Khyzha <artem.khyzha@arm.com>
Date: Mon, 16 Sep 2024 11:48:16 +0100
Subject: [PATCH] Updates to miaou7

---
 tools/miaou.ml | 42 +++++++++++++++++++++++-------------------
 1 file changed, 23 insertions(+), 19 deletions(-)

diff --git a/tools/miaou.ml b/tools/miaou.ml
index 6ce8fa909..581246cc7 100644
--- a/tools/miaou.ml
+++ b/tools/miaou.ml
@@ -150,7 +150,7 @@ module Make
       | 1 -> 3
       | n -> n+1
 
-    let pp_evt k = sprintf "E%d" k
+    let pp_evt k = sprintf "E\\textsubscript{%d}" k
 
     (* Pretty print elements for n-ary operators *)
 
@@ -164,8 +164,8 @@ module Make
 
     let sep op =
       match op with
-      | Union -> ",",", or"
-      | Inter|Seq|Cartesian -> ";","; and"
+      | Union -> ".","."
+      | Inter|Seq|Cartesian -> ".","."
       | _ -> assert false
 
     (***********)
@@ -258,7 +258,7 @@ module Make
     let pp_rel_id e1 e2 id =
       Item
         (sprintf
-           "\\expandafter\\MakeUppercase%s"
+           "\\expandafter{\\MakeUppercase%s}"
            (do_pp_rel_id e1 e2 id))
 
     let tr_rel_id e1 e2 loc id = pp_rel_id  e1 e2 (pp_id loc id)
@@ -440,8 +440,14 @@ module Make
       | Item txt ->
          Some
            (Item
-              (sprintf "\\expandafter\\MakeUppercase\\notthecase{%s}" txt))
-      | List _|DiffPair _|IfCond _ ->
+              (sprintf "\\expandafter{\\MakeUppercase\\notthecase{%s}}" txt))
+      | List (op,intro_txt,sep_txt,es) ->
+         (* eprintf "~~~~~~~~~~~~~~~~~~~~\n"; *)
+         (* eprintf "%s\n" (sprintf "\\expandafter{\\MakeUppercase\\notthecase{%s}}" intro_txt); *)
+         (* eprintf "%s\n" (List.fold_left (fun acc e -> acc ^ "," ^ (pp_txt e)) " " es) ; *)
+         (* eprintf "~~~~~~~~~~~~~~~~~~~~\n"; *)
+         Some (List (op,(sprintf "\\expandafter{\\MakeUppercase\\notthecase{%s}}" intro_txt),sep_txt,es))
+      | DiffPair _|IfCond _ ->
          None
 
     and tr_evts e1 = function
@@ -451,7 +457,7 @@ module Make
          tr_evts_id e1 loc "anyevent"
       | Var (loc,id) ->
          tr_evts_id e1 loc id
-      | Op1 (loc,Comp,e) ->
+      | Op1 (loc,Comp,e) | App (loc,Var (_,"exempt"),e) ->
          begin
            match tr_evts_not e1 e with
            | None -> tr_fail loc
@@ -488,13 +494,7 @@ module Make
                [Op1 (_,ToId,Var (_,"A"));
                 Var (_,"amo");
                 Op1 (_,ToId,Var (_,"L"));]))
-        ->
-         mk_list Inter
-           [pp_evts_id e1 "ExpW";
-            pp_evts_id e1 "A";
-            pp_evts_id e1 "REL";
-            pp_evts_id e1 "byamo";]
-(*         pp_evts_id e1 "rangeAamoL" *)
+        -> pp_evts_id e1 "rangeAamoL"
       | App (_,Var (_,"range"),Var (_,"lxsx")) ->
          pp_evts_id e1 "rangelxsx"
       |  App (_,
@@ -537,9 +537,9 @@ module Make
       | _,_ -> false
 
     let rec flatten_out = function
-      | List ((Inter|Union|Seq as op),_,_,ts)
+      | List ((Inter|Union|Seq as op),intro_txt,sep_txt,ts)
         ->
-         mk_list op (flatten_op op ts)
+         List (op,intro_txt,sep_txt,(flatten_op op ts))
       | List (op,txt,s,ts) ->
          List (op,txt,s,List.map flatten_out ts)
       | DiffPair (e1,e2) ->
@@ -590,9 +590,11 @@ module Make
     and pp_txt indent s = function
       | Item txt
       | List (_,_,_,[Item txt]) ->
+         (* eprintf "%s\\item %s%s:\n" indent txt s ; *)
          printf "%s\\item %s%s\n" indent txt s
       | List (_,txt,(s1,s2),txts) ->
          printf "%s\\item %s:\n" indent (Misc.capitalize txt) ;
+         (* eprintf "123%s\\item %s:\n" indent txt ; *)
          let indent = next_indent indent in
          printf "%s\\begin{itemize}\n" indent ;
          pp_txts indent s1 s2 s txts ;
@@ -668,12 +670,14 @@ module Make
       let pref =
         match ty with
         | Some RLN|None ->
+          (* assumes /<name>emph macro *)
+          let def_txt = (pp_id loc id) ^ "emph" in
            sprintf
-             "\\expandafter\\MakeUppercase\\%s{an Effect %s}{an Effect %s} if and only if"
-             (pp_id loc id) (pp_evt 1) (pp_evt 2)
+             "\\expandafter{\\MakeUppercase\\%s{an Effect %s}{an Effect %s}} if"
+              def_txt (pp_evt 1) (pp_evt 2)
         | Some SET ->
            sprintf
-             "\\expandafter\\MakeUppercase\\%s{an Effect %s} if and only if"
+             "\\expandafter{\\MakeUppercase\\%s{an Effect %s}} if"
              (pp_id loc id) (pp_evt 1) in
       let d =
         if O.flatten then