Creating pretty “cross-format” inference rules in Org mode

Given problem 2 above, it's not even worth evaluating this approach; it's not a valid solution. But it may be that we can extend it to become one.

We start with a little bit of elisp code which our macro will use.

(let*
   ;; Find the last non-empty string, …
  ((last-nonempty (position "" premises :test-not 'equal :from-end t))
   ;; … and take only up to that element of the list.
   (premises (seq-take premises (+ last-nonempty 1))))

  ;; Join the resulting list using the spacer, with the wrapper around
  ;; each element.
  (mapconcat (lambda (p) (format wrapper p)) premises spacer))

This code block has three var arguments:

• premises, which defaults to (), and should be a list of strings. Note that trailing emptystrings will be deleted —the reason for this will be seen when we get to defining macros.
• wrapper, which defaults to %s, and which should be a format string —this will be applied to each premise, to allow for formatting.
• spacer, which defaults to a string of three non-breaking spaces, —this will be inserted between each premise.

We can make use of this code block, which is named format-premises, by an inline source code call, with the syntax such as

call_format-premises(wrapper="*%s*",
                     spacer=" , ",
                     premises='("hello" "world"))

See the Org manual regarding inline source code calls.

This call wraps each of the words hello and world with asterisks, which is the Org syntax for bold, and separates them with three dashes. Admire the results in the export: *hello* , *world*

Not quite right, actually. By default, the results are wrapped in

• verbatim emphasis delimiters, =, and outside of those,
• an invocation of the results macro, which as far as I can tell is simply used to demarcate the results, so that successive C-c C-c invocations will overwrite them, rather than prepend them.

This can be seen by hitting C-c C-c on the call, which results in the following being placed right after it.

{{{results(=*hello* , *world*=)}}}

We definitely don't want the verbatim wrapper, and can do without the results macro wrapper —in the end use-case of this call, users would not be manually invoking it.

Thankfully, the wrappers can be replaced via the optional <end header arguments> argument, placed in (square) brackets after the arguments. These affect the result of the code block —an additional optional argument, <inside header arguments>, would come before the arguments and would apply to the source block itself; we have no need of this. We could use :results raw to eliminate both wrappers. That is,

call_format-premises(wrapper="*%s*",
                     spacer=" , ",
                     premises='("hello" "world"))[:results raw]

results in the expected output

*hello* , *world*

which exports as expected, as seen here: hello , world

Now, this invocation is too intrusive for our purposes. But we can prettify it into a macro! Note the linebreaks here are only for presentation; they cannot be present in the actual macro.

#+Macro: premise2
  call_format-premises(
     wrapper="$1",
     spacer="$2",
     premises='("$3" "$4" "$5" "$6"
                "$7" "$8" "$9" "$10"))
   [:results raw]

You'll notice that we have lost some flexibility in the translation: the macro allows for 8 premise arguments —I say “allows for” because omitting arguments does not cause any errors— whereas format-premises allows an arbitrary number. Unfortunately, it seems Org macros don't have support for an arbitrary number of arguments. In this case, it seems an acceptable loss; if you have more than 8 premises —or honestly, more than 4— then this inference rule presentation is probably the wrong tool for you.

In any case, our macro looks promising; if we invoke it

{{{premise2(   ,/%s/,p,q)}}}

we get nicely formatted output: p/   /q

Unfortunately, as promising as this development was, we've reached a point where it falls apart. If we place our macro into the table,

#+attr_HTML: :frame void :cellpadding 0 :class noboldheader
|            <c>             |                |
| {{{premise2(/%s/,   ,p,q)}}} |                |
|         {{{bar2}}}         | @@html: @@name |
|            /r/             |                |

we unfortunately notice on export that it just expands to the text of the call.

This is a limitation of Org tables! They do not support inline code in their cells.

So, we find ourselves at a bit of a dead end. But there is a solution, which can make use of many of the pieces we constructed here; table formulas!

As a first venture, consider:

#+attr_HTML: :frame void :cellpadding 0 :class noboldheader
|    <c>     |                           |
| /p/   /q/  | @@latex:\vspace{-0.7em}@@ |
| {{{bar2}}} | modus-ponens              |
|    /r/      |                           |
#+tblfm: @2$1='(org-sbe format-premises (wrapper "\"/%s/\"") (spacer "\"   \"") (premises "p" "q"))

The function org-sbe (“Org-source babel execute”) is necessary to invoke code in a source block within this file. It takes as argument the name of the code block —as a string or as, as we have chosen, a symbol—, as well as lists for the arguments of the code block, in the form (argument-name value₁ value₂ value₃) —so, allowing for lists of arguments— where each value should be a string. The premise cell can then be auto-filled by invoking the table formula with C-c C-c. Also, notice we have moved the LaTeX code to move up the horizontal rule to the cell next to the premise, since we are no longer use a macro. With all that in place, here is the resulting table:

We can improve the appearance of solution in Org at least somewhat by finding a way to place the premises in the table itself, rather than in the formula.

Thankfully, Org tables account for use cases such as this; they include comment rows, similar to the alignment tag row. To use them, we must add a first column —which will not be exported— which contains a / for comment rows.

This row can also contain other markers; we actually make use of two of them immediately. A _ indicates that the contents of the row are names for the cells below. A ^ is similar, but the names are for the cells above.

We can achieve better appearance in Org by using comment rows for

• the premises,
• the rule name,
• the conclusion, and
• the wrapper and spacer.

Then the end user needs only insert a table template, fill in the comment rows, and evaluate the formulas to get their inference rule.

We also replaced the bar2 macro with an identical one whose name looks a bit more like a horizontal rule. For reference, there are 10 dashes in the name, and they can easily be typed using C-u 10 -.

#+Macro: inf---------------- @@latex:\hrulefill\vspace{-0.3em}@@@@html:<hr>@@