Visualize Church numerals Background

Visualizing λ-calculus terms

Famous lambda-juggler (and code golfer) John Tromp devised an interesting visualization of terms in the λ-calculus. In his words:


  abstractions (lambdas) are represented by horizontal lines, variables by vertical lines emanating down from their binding lambda, and applications by horizontal links connecting the leftmost variables.


For example, the lambda term λf.λx.f (f (f (f x))) corresponds to the visualization:

-------------------
 |   |   |   |
-------------------
 |   |   |   |   |
 |   |   |   |----
 |   |   |----
 |   |----
 |----
 |


Read it from top to bottom:


The first horizontal line represents the first λ. 
The four lines descending from it represent the fs in the body.
Similarly, the second horizontal line represents the second λ, and the single new line descending from it represents the x in the body.
The rightmost f line and the x line are connected by a horizontal line representing an application (f&nbsp;x).
The next application is (f&nbsp;(f&nbsp;x)), et cetera.


Church numerals

The Church numerals are a specific sequence of terms in the λ-calculus, taking on the following pattern:

0 = λf. λx. x
1 = λf. λx. f x
2 = λf. λx. f (f x)
3 = λf. λx. f (f (f x))
...


Task

Given an input number n, print some ASCII art that visualizes the nth Church numeral. For instance, the example above is your target output when given n = 4. For n = 0, print:

---

---
 |
 |


Test cases

Your answer must output exactly the same text (modulo trailing newlines) as this stack snippet for all integer inputs n ≥ 0:



function visualize() {
  var vin = document.getElementById('visualize-in');
  var vout = document.getElementById('visualize-out');
  var n = Number(vin.value);
  if (n &lt; 0) n = 0;
  var line = '-'.repeat(4 * n + 3);
  var bars = function(k) { return '   |'.repeat(k).substr(2); };
  var img = [line, bars(n), line, bars(n + 1)];
  for (var i = n; i &gt; 0; --i) img.push(bars(i) + '----');
  vout.innerHTML = img.join('\n') + '\n |';
}
&lt;label for="visualize-in"&gt;n&amp;nbsp;&lt;input style="width:50px;" type="number" id="visualize-in" name="visualize-in" onchange="visualize()"/&gt;&lt;/label&gt;
&lt;pre style="background-color: #eff0f1" id="visualize-out"&gt;&lt;/pre&gt;




This is code-golf, so the shortest code in bytes wins.
Retina, 74 67 63 bytes

Byte count assumes ISO 8859-1 encoding.

.
 |  
^
$.'$*----¶
\z
¶$` |
+`(.+\|) .+$
$&amp;¶$1----
$
¶ |
  ¶
¶


Input is in unary, using any character except linefeeds as the digit.

Try it online!

Explanation

.
 |  


We start by turning each unary digit into  |   (note the trailing spaces). This gives us the second line of the output (plus two trailing spaces if the input is at least 1).

^
$.'$*----¶


We match the beginning of the string in order to prepend the first line. This is done using some Retina-specific substitution features. $* repeats the character on the right as many times as its left arugment. $.' evaluates the number of characters to the right of the match. Since the match is only the beginning of the string this gives as many - as there are characters in the string and --- appends three more. The ¶ is an alias for a linefeed. So now we've got the first two lines.

\z
¶$` |


Now we append the next two lines. We do this by matching the end of the string and appending a linefeed, the entire string again and then  | to get the fourth line right.

+`(.+\|) .+$
$&amp;¶$1----


Time for the applications. The leading + makes Retina repeat this stage until the output stops changing (in this case because the regex no long matches). The regex matches the entire last line, provided it contains a | follows by a space. We capture everything up to the | (which will be the second to last) in group 1. We write the line back with $&amp;, a linefeed, then group 1 (thereby dropping the last |) and then ----.

$
¶ |


This just adds the final line containing only a single |.

  ¶
¶


Finally we need to get rid of the trailing spaces on the second line.