Fix rendering of subscript atoms

spectec/spec/wasm-3.0/6-typing.watsup

@@ -8,9 +8,8 @@ syntax init hint(desc "initialization status") =
 syntax localtype hint(desc "local type") =
   init valtype
 
-;; TODO(1, rossberg): fix rendering of subscript
 syntax instrtype hint(desc "instruction type") =
-  resulttype ->_ localidx* resulttype  hint(show %0 `->_ %2 %3) hint(macro "to")
+  resulttype ->_ localidx* resulttype  hint(macro "to")
 
 
 syntax context hint(desc "context") hint(macro "%" "C%") =

spectec/src/backend-latex/render.ml

@@ -59,6 +59,11 @@ let rec ends_sub_exp e =
   | FuseE (_e1, e2) -> ends_sub_exp e2
   | _ -> false
 
+let as_arith_exp e =
+  match e.it with
+  | ArithE e1 -> e1
+  | _ -> e
+
 let as_paren_exp e =
   match e.it with
   | ParenE (e1, _) -> e1
@@ -1070,14 +1075,23 @@ Printf.eprintf "[render %s:X @ %s] try expansion\n%!" (Source.string_of_region e
   | TupE es -> "(" ^ render_exps ", " env es ^ ")"
   | InfixE (e1, atom, e2) ->
     let id = typed_id atom in
-    let e = AtomE atom $ atom.at in
-    let args = List.map arg_of_exp (as_seq_exp e1 @ [e] @ as_seq_exp e2) in
+    let ea = AtomE atom $ atom.at in
+    let args = List.map arg_of_exp ([e1; ea] @ as_seq_exp e2) in
     render_expand render_exp env env.show_atom env.macro_atom id args
       (fun () ->
-        (match e1.it with
-        | SeqE [] -> "{" ^ space (render_atom env) atom ^ "}\\;"
-        | _ -> render_exp env e1 ^ space (render_atom env) atom
-        ) ^ render_exp env e2
+        (* Handle subscripting and unary uses *)
+        (match Atom.is_sub atom, (as_arith_exp e1).it with
+        | false, SeqE [] -> "{" ^ render_atom env atom ^ "}\\, "
+        | true, SeqE [] -> "{" ^ render_atom env atom ^ "}_"
+        | false, _ -> render_exp env e1 ^ space (render_atom env) atom
+        | true, _ -> render_exp env e1 ^ " " ^ render_atom env atom ^ "_"
+        ) ^
+        (match Atom.is_sub atom, e2.it with
+        | true, SeqE (e21::e22::es2) ->
+          "{" ^ render_exps "," env (as_tup_exp e21) ^ "} " ^ render_exp_seq env (e22::es2)
+        | true, _ -> "{" ^ render_exps "," env (as_tup_exp e2) ^ "} {}"
+        | false, _ -> render_exp env e2
+        )
       )
   | BrackE (l, e1, r) ->
     let id = typed_id l in

spectec/src/el/atom.ml

@@ -55,8 +55,15 @@ let eq atom1 atom2 =
 let compare atom1 atom2 =
   compare atom1.it atom2.it
 
-let sub atom1 atom2 =
+let is_sub atom =
+  match atom.it with
+  | Atom id -> id <> "" && id.[String.length id - 1] = '_'
+  | ArrowSub | Arrow2Sub -> true
+  | _ -> false
+
+let sub atom1 atom2 = 
   match atom1.it, atom2.it with
+  | Atom id1, Atom id2 -> id1 = id2 ^ "_"
   | ArrowSub, Arrow
   | Arrow2Sub, Arrow2 -> true
   | _, _ -> false
@@ -127,8 +134,8 @@ let name atom =
   | Mem -> "in"
   | Arrow -> "arrow"              (* Latex: \rightarrow *)
   | Arrow2 -> "darrow"            (* Latex: \Rightarrow *)
-  | ArrowSub -> "arrowsub"        (* Latex: \rightarrow with subscript *)
-  | Arrow2Sub -> "darrowsub"      (* Latex: \Rightarrow with subscript *)
+  | ArrowSub -> "arrow_"          (* Latex: \rightarrow with subscript *)
+  | Arrow2Sub -> "darrow_"        (* Latex: \Rightarrow with subscript *)
   | Colon -> "colon"              (* Latex: : *)
   | Sub -> "sub"                  (* Latex: \leq or <: *)
   | Sup -> "sup"                  (* Latex: \geq or :> *)