如何按语义对齐前提？

Question

我正在使用语义包描述语言的操作语义。问题是，当有很多前提时，它看起来不太好看。我想将它们左对齐。

\documentclass[11pt]{book}

\usepackage{floatflt,amsmath,amssymb}
\usepackage[ligature, inference]{semantic}
\begin{document}

\mathlig{->}{\rightarrow}
\mathlig{|-}{\vdash}
\mathlig{=>}{\Rightarrow}
\mathligson

\[
% struct literal
\inference[It(22):]
{
so,E,S|-e_1:v_1,S_1 \\
\ldots \\
so,E,S_{n-1}|-e_n:v_n,S_n \\
class(T)=(a_1:T_1, \ldots, a_n:T_n) \\  % take the fields of the object
l_i = newloc(S_n) \; for \; i = 1 \ldots n \\
v=T(a_1=l_1, \ldots, a_n=l_n) \\ % assign locations to fields
S_f = S_n[v_1/l_1, \ldots, v_n/l_n]
}
{so, E, S|-struct\;T\;\{ e_1, \ldots, e_n \}:v,S_f}
\quad\quad
% list literal
\inference[It(21):]
{
so,E,S|-e_1:v_1,S_1 \\
\ldots \\
so,E,S_{n-1}|-e_n:v_n,S_n \\
l_i = newloc(S_n) \; for \; i = 1 \ldots n \\
v=Table(a_1=l_1, \ldots, a_n=l_n) \\
S_f = S_n[v_1/l_1, \ldots, v_n/l_n]
}
{so, E, S|-\#[e_1, \ldots, e_n]:v,S_f}
\]
\end{document}

Answer 1

在此期间，这里有一个完全替代的实现，使用一个基本的实现array，它提供了可比较的显示，但\inference具有您正在寻找的对齐方式：

\documentclass{article}

\usepackage[ligature, inference]{semantic}

\begin{document}

\mathlig{->}{\rightarrow}
\mathlig{|-}{\vdash}
\mathlig{=>}{\Rightarrow}
\mathligson

\[
  % struct literal
  \inference[It(22):]
  {
    so,E,S|-e_1:v_1,S_1 \\
    \ldots \\
    so,E,S_{n-1}|-e_n:v_n,S_n \\
    class(T)=(a_1:T_1, \ldots, a_n:T_n) \\  % take the fields of the object
    l_i = newloc(S_n) \; for \; i = 1 \ldots n \\
    v=T(a_1=l_1, \ldots, a_n=l_n) \\ % assign locations to fields
    S_f = S_n[v_1/l_1, \ldots, v_n/l_n]
  }
  {so, E, S|-struct\;T\;\{ e_1, \ldots, e_n \}:v,S_f}
  \quad\quad
  % list literal
  \inference[It(21):]
  {
    so,E,S|-e_1:v_1,S_1 \\
    \ldots \\
    so,E,S_{n-1}|-e_n:v_n,S_n \\
    l_i = newloc(S_n) \; for \; i = 1 \ldots n \\
    v=Table(a_1=l_1, \ldots, a_n=l_n) \\
    S_f = S_n[v_1/l_1, \ldots, v_n/l_n]
  }
  {so, E, S|-\#[e_1, \ldots, e_n]:v,S_f}
\]

\renewcommand{\inference}[3][]{%
  \begin{array}[b]{@{}c@{}l@{}}
    \smash{\raisebox{-.5\normalbaselineskip}{\footnotesize #1}} & 
      \begin{array}[b]{l}
        #2
      \end{array} \\
      \cline{2-2}
    & \begin{array}[t]{l}
        #3
      \end{array}
  \end{array}
}

\[
  % struct literal
  \inference[It(22):]
  {
    so,E,S|-e_1:v_1,S_1 \\
    \ldots \\
    so,E,S_{n-1}|-e_n:v_n,S_n \\
    class(T)=(a_1:T_1, \ldots, a_n:T_n) \\  % take the fields of the object
    l_i = newloc(S_n) \; for \; i = 1 \ldots n \\
    v=T(a_1=l_1, \ldots, a_n=l_n) \\ % assign locations to fields
    S_f = S_n[v_1/l_1, \ldots, v_n/l_n]
  }
  {so, E, S|-struct\;T\;\{ e_1, \ldots, e_n \}:v,S_f}
  \quad\quad
  % list literal
  \inference[It(21):]
  {
    so,E,S|-e_1:v_1,S_1 \\
    \ldots \\
    so,E,S_{n-1}|-e_n:v_n,S_n \\
    l_i = newloc(S_n) \; for \; i = 1 \ldots n \\
    v=Table(a_1=l_1, \ldots, a_n=l_n) \\
    S_f = S_n[v_1/l_1, \ldots, v_n/l_n]
  }
  {so, E, S|-\#[e_1, \ldots, e_n]:v,S_f}
\]

\end{document}