More rendering fixes for e^(x<e)

Wasm-DSL · Jul 27, 2023 · 132d6c0 · 132d6c0
1 parent 799c5d3
commit 132d6c0
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 9 deletions.
diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml
@@ -444,7 +444,7 @@ and render_iter env = function
   | ListN ({it = ParenE (e, _); _}, None) | ListN (e, None) ->
     "^{" ^ render_exp env e ^ "}"
   | ListN (e, Some id) ->
-    "^{" ^ id.it ^ "<" ^ render_exp env e ^ "}"
+    "^{" ^ render_varid env id ^ "<" ^ render_exp env e ^ "}"
 
 
 (* Types *)

diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
@@ -4270,12 +4270,12 @@ $$
  &&&\quad {\land}~{\mathit{ga}_{\mathit{ex}}^\ast} = \mathrm{globals}({\mathit{externval}^\ast}) \\
  &&&\quad {\land}~{\mathit{ta}_{\mathit{ex}}^\ast} = \mathrm{tables}({\mathit{externval}^\ast}) \\
  &&&\quad {\land}~{\mathit{ma}_{\mathit{ex}}^\ast} = \mathrm{mems}({\mathit{externval}^\ast}) \\
- &&&\quad {\land}~{\mathit{fa}^\ast} = {{|\mathit{s}.\mathsf{func}|} + \mathit{i}_{\mathit{func}}^{i_func<\mathit{n}_{\mathit{func}}}} \\
- &&&\quad {\land}~{\mathit{ga}^\ast} = {{|\mathit{s}.\mathsf{global}|} + \mathit{i}_{\mathit{global}}^{i_global<\mathit{n}_{\mathit{global}}}} \\
- &&&\quad {\land}~{\mathit{ta}^\ast} = {{|\mathit{s}.\mathsf{table}|} + \mathit{i}_{\mathit{table}}^{i_table<\mathit{n}_{\mathit{table}}}} \\
- &&&\quad {\land}~{\mathit{ma}^\ast} = {{|\mathit{s}.\mathsf{mem}|} + \mathit{i}_{\mathit{mem}}^{i_mem<\mathit{n}_{\mathit{mem}}}} \\
- &&&\quad {\land}~{\mathit{ea}^\ast} = {{|\mathit{s}.\mathsf{elem}|} + \mathit{i}_{\mathit{elem}}^{i_elem<\mathit{n}_{\mathit{elem}}}} \\
- &&&\quad {\land}~{\mathit{da}^\ast} = {{|\mathit{s}.\mathsf{data}|} + \mathit{i}_{\mathit{data}}^{i_data<\mathit{n}_{\mathit{data}}}} \\
+ &&&\quad {\land}~{\mathit{fa}^\ast} = {{|\mathit{s}.\mathsf{func}|} + \mathit{i}_{\mathit{func}}^{\mathit{i}_{\mathit{func}}<\mathit{n}_{\mathit{func}}}} \\
+ &&&\quad {\land}~{\mathit{ga}^\ast} = {{|\mathit{s}.\mathsf{global}|} + \mathit{i}_{\mathit{global}}^{\mathit{i}_{\mathit{global}}<\mathit{n}_{\mathit{global}}}} \\
+ &&&\quad {\land}~{\mathit{ta}^\ast} = {{|\mathit{s}.\mathsf{table}|} + \mathit{i}_{\mathit{table}}^{\mathit{i}_{\mathit{table}}<\mathit{n}_{\mathit{table}}}} \\
+ &&&\quad {\land}~{\mathit{ma}^\ast} = {{|\mathit{s}.\mathsf{mem}|} + \mathit{i}_{\mathit{mem}}^{\mathit{i}_{\mathit{mem}}<\mathit{n}_{\mathit{mem}}}} \\
+ &&&\quad {\land}~{\mathit{ea}^\ast} = {{|\mathit{s}.\mathsf{elem}|} + \mathit{i}_{\mathit{elem}}^{\mathit{i}_{\mathit{elem}}<\mathit{n}_{\mathit{elem}}}} \\
+ &&&\quad {\land}~{\mathit{da}^\ast} = {{|\mathit{s}.\mathsf{data}|} + \mathit{i}_{\mathit{data}}^{\mathit{i}_{\mathit{data}}<\mathit{n}_{\mathit{data}}}} \\
  &&&\quad {\land}~{\mathit{xi}^\ast} = {\mathrm{instexport}({\mathit{fa}_{\mathit{ex}}^\ast}~{\mathit{fa}^\ast},\, {\mathit{ga}_{\mathit{ex}}^\ast}~{\mathit{ga}^\ast},\, {\mathit{ta}_{\mathit{ex}}^\ast}~{\mathit{ta}^\ast},\, {\mathit{ma}_{\mathit{ex}}^\ast}~{\mathit{ma}^\ast},\, \mathit{export})^\ast} \\
  &&&\quad {\land}~\mathit{m} = \{ \begin{array}[t]{@{}l@{}}
 \mathsf{func}~{\mathit{fa}_{\mathit{ex}}^\ast}~{\mathit{fa}^\ast},\; \\
@@ -4346,9 +4346,9 @@ $$
  &&&\quad {\land}~\mathit{f} = \{ \begin{array}[t]{@{}l@{}}
 \mathsf{local}~\epsilon,\; \mathsf{module}~\mathit{m} \}\end{array} \\
  &&&\quad {\land}~\mathit{n}_{\mathit{elem}} = {|{\mathit{elem}^\ast}|} \\
- &&&\quad {\land}~{\mathit{instr}_{\mathit{elem}}^\ast} = \mathrm{concat}_{\mathit{instr}}({\mathrm{runelem}({\mathit{elem}^\ast}[\mathit{i}],\, \mathit{i})^{i<\mathit{n}_{\mathit{elem}}}}) \\
+ &&&\quad {\land}~{\mathit{instr}_{\mathit{elem}}^\ast} = \mathrm{concat}_{\mathit{instr}}({\mathrm{runelem}({\mathit{elem}^\ast}[\mathit{i}],\, \mathit{i})^{\mathit{i}<\mathit{n}_{\mathit{elem}}}}) \\
  &&&\quad {\land}~\mathit{n}_{\mathit{data}} = {|{\mathit{data}^\ast}|} \\
- &&&\quad {\land}~{\mathit{instr}_{\mathit{data}}^\ast} = \mathrm{concat}_{\mathit{instr}}({\mathrm{rundata}({\mathit{data}^\ast}[\mathit{j}],\, \mathit{j})^{j<\mathit{n}_{\mathit{data}}}}) \\
+ &&&\quad {\land}~{\mathit{instr}_{\mathit{data}}^\ast} = \mathrm{concat}_{\mathit{instr}}({\mathrm{rundata}({\mathit{data}^\ast}[\mathit{j}],\, \mathit{j})^{\mathit{j}<\mathit{n}_{\mathit{data}}}}) \\
  &&&\quad {\land}~{\mathit{start}^?} = {(\mathsf{start}~\mathit{x})^?} \\
 \end{array}
 $$