Generated LaTeX code incorrectly renders an inference rule, missing a symbol after a display hint `"()"`.

[yusungsim]

Hi, I came across an issue while rendering an inference rule to a LaTeX code.

Below is a minified DSL code of interest.

;; just for demo
syntax state = nat

syntax value =
    | VUnit     hint(show "()")

;; relation definition
relation interp : state -> value state

rule interp:
    s -> VUnit s'  (; `s'` does not appear in generated LaTeX code ;)

The value VUnit has a display hint show "()", and the value is used in the inference rule interp.

When this code is compiled and a LaTeX code is generated, the LaTeX code incorrectly renders the inference rule. Specifically, the rendered rule misses the symbol s' at the rightmost part of the rule, right after the `()'. Below is the result LaTeX code of rendering the above DSL code. (i.e. $ ./watsup min_state/a.watsup --latex)

$$
\begin{array}[t]{@{}lrrl@{}l@{}}
& {\mathit{state}} & ::= & 0 ~|~ 1 ~|~ 2 ~|~ \dots \\
& {\mathit{value}} & ::= & \mbox{\texttt{`()'}} \\
\end{array}
$$

$\boxed{{\mathit{state}} \rightarrow {\mathit{value}}~{\mathit{state}}}$

$$
\begin{array}{@{}c@{}}\displaystyle
\frac{
}{
s \rightarrow \mbox{\texttt{`()'}}
} \, {[\textsc{\scriptsize interp}]}
\qquad
\end{array}
$$

As you see in the 14th line (s \rightarrow \mbox{\texttt{`()'}}), the rendered rule misses the last symbol s'.

I experimented with variants of the code to narrow down the cause of this issue, and I expect that the display hint has something to do with this issue. If the display hint of value VUnit is removed as the below code, SpecTec correctly renders the rule with the symbol s'.

(Parts of the modified DSL code and its resulting LaTeX code)

...
syntax value =
    | VUnit
...

```latex
...
s \rightarrow \mathsf{vunit}~{s'}
...

I also checked the IL compiled from the DSL code (i.e. $ ./watsup min_state/a.watsup --print-il), but it seems SpecTec correctly produces IL with the symbol s'. So I think that this issue is related with the LaTeX backend.

;; min_state/a.watsup:2.1-2.19
syntax state = nat

;; min_state/a.watsup:4.1-5.32
syntax value =
  | VUnit

;; min_state/a.watsup:8.1-8.39
relation interp: `%->%%`(state, value, state)
  ;; min_state/a.watsup:10.1-11.18
  rule _{s : state, s' : state}:
    `%->%%`(s, VUnit_value, s')

[rossberg]

Ah yes. Expansion is a bit naive, it assumes all following elements of the same sequence are arguments, and the expansion is just not using them. Fixing that will require adding a notion of hint arity somehow, so that only a suitable prefix is used. I will give that a try.

In the mean time, there are two possible workarounds:

1. Use hint(show () %%).
2. Don't use a hint, but instead write the constructor directly as `() (note the leading backtick for escaping, which turns the parens into atoms).

The former is a bit of a hack. The latter may be even closer to what you really want.

Btw, show hints use expressions, not strings. If you put quotes around, they'll just get type-set as a text literal.

[rossberg]

Okay, for now I implemented a hack that should fix this.