4

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

  • You should be using \mathit{newloc} or, more probably, \operatorname{newloc} (and similarly for the other operators). – egreg Oct 5 '15 at 8:05
  • @egreg, good remark – Inti Gonzalez-Herrera Oct 5 '15 at 12:41
3

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}

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.