推論規則をレイアウトする bcprules.sty

今まで推論規則を書くときは proof.sty を使っていた.

\[
  \infer[\mbox{\sc T-App}]{
    \Gamma \vdash t_1\ t_2 : \tau_2
  }{
    \Gamma \vdash t_1 : \tau_1 \rightarrow \tau_2
    & \Gamma \vdash t_2 : \tau_1
  }
\]

と書くと

のようにレイアウトされる.


しかし,前提の部分が長すぎる場合にどう改行してよいのか不明で*1

\[
  \infer[\mbox{\sc T-VeryLong}]{
    \Gamma \vdash \mbox{foo}\ t_1\ t_2 : \mbox{bar}\ \alpha\ \beta
  }{
    \Gamma \vdash t_1 : \mbox{very-long-constructor}\ \alpha
    & \Gamma \vdash t_2 : \mbox{another-very-long-constructor}\ \beta
    & \mbox{have-very-long-property}(\alpha, \beta)
  }
\]

とかが Overfull \hbox というメッセージと共に

となってしまう.


Benjamin C. Pierce 先生の bcprules.sty を最近知った.
http://www.cis.upenn.edu/~bcpierce/papers/index.shtml

\infrule[T-App]{
  \Gamma \vdash t_1 : \tau_1 \rightarrow \tau_2
  \andalso \Gamma \vdash t_2 : \tau_1
}{
  \Gamma \vdash t_1\ t_2 : \tau_2
}

と書くと

のようにレイアウトされる.まさに TAPL のレイアウトだ.


bcprules.sty の場合,先程のように前提が長い例は

\infrule[T-VeryLong]{
  \Gamma \vdash t_1 : \mbox{very-long-constructor}\ \alpha
  \andalso \Gamma \vdash t_2 : \mbox{another-very-long-constructor}\ \beta
  \andalso \mbox{have-very-long-property}(\alpha, \beta)
}{
  \Gamma \vdash \mbox{foo}\ t_1\ t_2 : \mbox{bar}\ \alpha\ \beta
}


となる.
また,普通に \\ で改行を入れることもできる.

\infrule[T-VeryLong]{
  \Gamma \vdash t_1 : \mbox{very-long-constructor}\ \alpha
  \andalso \Gamma \vdash t_2 : \mbox{another-very-long-constructor}\ \beta
  \\
  \andalso \mbox{have-very-long-property}(\alpha, \beta)
}{
  \Gamma \vdash \mbox{foo}\ t_1\ t_2 : \mbox{bar}\ \alpha\ \beta
}

*1:\vbox 作ってその中に行毎に \hbox 作ってその中に書く,という方法でそれっぽいことはできた