How to automatically separate words in inference from semantic package?

Question

I'm trying to use inference from semantic package to describe static semantics of a language.

I would like to separate nonterminals in inference rules with spaces without inserting them by hand.

Is there a way to automatically separate the words SimpleExpr_1 RelOper SimpleExpr_2 from following code with spaces, as if it was written as SimpleExpr_1\ RelOper\ SimpleExpr_2 ?

\inference
  {\Gamma \vdash Expr_1 : \textsc{Integer} \quad 
   \Gamma \vdash Expr_2 : \textsc{Integer}}
  {\Gamma \vdash SimpleExpr_1 RelOper SimpleExpr_2 : \textsc{Boolean}}

Edit: I should add, that I tried solution presented here: Making mathmode obey spaces , but for reasons unknown to me it doesn't seem to apply to inference. Any ideas?

Answer 1

I see you are already using \quad, the other spacing command in math mode are:

\, thin space

\: medium space

\; thicker space

\quad thicker

\qquad and thicker

\! negative thin space

Answer 2

One way is to redefine \predicatebegin to define spaces in math mode as not ignored. A subtle point, though, is that the tokens have already been read, so spaces already have catcode 10. This can be reverted using \scantokens. I thought it would be best to only scan tokens from |- to :, but this can easily be changed.

\documentclass{article}
\usepackage{semantic}

\begingroup\catcode`\ =\active%
\gdef\mathobeyspaces{\catcode`\ =\active\let =\ }%
\endgroup

\def\predicatebegin#1|-#2:#3\predicateend
  {$#1|-\mathobeyspaces \scantokens{#2}:#3$}%

\begin{document}
\inference
  {\Gamma |-Expr_1:\textsc{Integer} \quad 
   \Gamma |-Expr_2: \textsc{Integer}}
  {\Gamma |-SimpleExpr_1 RelOper SimpleExpr_2: \textsc{Boolean}}
\end{document}