[Tex/LaTex] How to align the premises in a semantic

alignmath-modesemantics

I'm using the semantic package to describe the operational semantic of a language. The problem is that it doesn't look nice when there are many premises. I would like to align them to the left.

\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}

enter image description here

Best Answer

In the interim, here's a completely alternative implementation using a basic array that provides the a comparable display to \inference yet has the alignment you're looking for:

enter image description here

\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}
Related Question