aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--docs/code.css36
-rw-r--r--docs/code.js56
-rw-r--r--docs/content.css54
-rw-r--r--docs/content.js26
-rw-r--r--docs/content.template5
-rwxr-xr-xdocs/gen.sh2
-rw-r--r--docs/mkdocs.yml3
-rw-r--r--docs/wiki_src/coding/compilation.md23
-rw-r--r--docs/wiki_src/coding/data-structures.md2
-rw-r--r--docs/wiki_src/coding/meta-programming.md10
-rw-r--r--docs/wiki_src/custom.css11
-rw-r--r--docs/wiki_src/introduction/lambda-calculus.md26
-rw-r--r--docs/wiki_src/introduction/syntax.md6
13 files changed, 143 insertions, 117 deletions
diff --git a/docs/code.css b/docs/code.css
new file mode 100644
index 0000000..76fb483
--- /dev/null
+++ b/docs/code.css
@@ -0,0 +1,36 @@
+.com {
+ color: #ff64bd;
+}
+
+.def {
+ color: #13dbee;
+}
+
+.comment {
+ color: #999999;
+}
+
+.type {
+ color: #ffa120;
+}
+
+.left-abs, .right-abs {
+ color: #6b82ff;
+}
+
+.left-app, .right-app {
+ color: #ff8750;
+}
+
+.index {
+ color: #ff5050;
+}
+
+.number {
+ color: #b1ee13;
+}
+
+/* lol */
+.string, .string * {
+ color: #bb73f0 !important;
+}
diff --git a/docs/code.js b/docs/code.js
new file mode 100644
index 0000000..8440591
--- /dev/null
+++ b/docs/code.js
@@ -0,0 +1,56 @@
+// high-quality syntax highlighter
+// TODO: Implement actual highlighter (or fix many regex bugs)
+
+const term = (t) =>
+ t
+ .replaceAll(/'(.)'/g, "<span class='string'>'$1'</span>")
+ .replaceAll(/"([^\"]*)"/g, "<span class='string'>\"$1\"</span>")
+ .replaceAll(/(\([+-][0-9]+[ubt]?\))/g, "<span class='number'>$1</span>")
+ .replaceAll(/(?<!\>)(\()/g, "<span class='left-app'>(</span>")
+ .replaceAll(/(\))(?!\<)/g, "<span class='right-app'>)</span>")
+ .replaceAll("[", "<span class='left-abs'>[</span>")
+ .replaceAll("]", "<span class='right-abs'>]</span>")
+ .replaceAll(/(?<![+-\d])([0-9])/g, "<span class='index'>$1</span>");
+
+const highlightTerm = (elem) => {
+ elem.innerHTML = term(elem.innerHTML);
+};
+
+const highlight = (elem) => {
+ const fixPath = (p) => p.replace("/", "_");
+
+ elem.innerHTML = elem.innerHTML
+ .replaceAll(
+ /^:import std\/(.*) (.*)$/gm,
+ (_, p, s) =>
+ `<span class="com">:import</span> <a href='${fixPath(
+ p,
+ )}.bruijn.html'>std/${p}</a> ${s}`,
+ )
+ .replaceAll(
+ /^:input std\/(.*)$/gm,
+ (_, p) =>
+ `<span class="com">:input</span> <a href='${fixPath(
+ p,
+ )}.bruijn.html'>std/${p}</a>`,
+ )
+ .replaceAll(
+ /^:test (\(.*\)) (\(.*\))$/gm,
+ (_, t1, t2) => `<span class='com'>:test</span> ${term(t1)} ${term(t2)}`,
+ )
+ .replaceAll(
+ /^:time (.*)$/gm,
+ (_, t) => `<span class='com'>:time</span> ${term(t)}`,
+ )
+ .replaceAll(
+ /^([^:\n<#][^ ]*) (.*)$/gm,
+ (_, d, t) => `<span class='def'>${d}</span> ${term(t)}`,
+ )
+ .replaceAll(/^# (.*)$/gm, "<span class='comment'># $1</span>")
+ .replaceAll(/ ⧗ (.*)\n/g, " ⧗ <span class='type'>$1</span>\n");
+};
+
+window.onload = () => {
+ [...document.querySelectorAll("code.language-bruijn")].forEach(highlight);
+ [...document.querySelectorAll("code.bruijn")].forEach(highlightTerm);
+};
diff --git a/docs/content.css b/docs/content.css
index c6d4d5c..3fbc301 100644
--- a/docs/content.css
+++ b/docs/content.css
@@ -15,56 +15,6 @@ a {
}
pre {
- margin: 0 0 1em;
- padding: .5em 1em;
-}
-
-pre .line {
- display: block;
- float: left;
- margin: 0 1em 0 -1em;
- border-right: 1px solid;
- text-align: right;
-}
-
-pre .line span {
- display: block;
- padding: 0 .5em 0 1em;
-}
-
-pre .cl {
- display: block;
- clear: both;
-}
-
-.com {
- color: #ff64bd;
-}
-
-.def {
- color: #13dbee;
-}
-
-.comment {
- color: #999999;
-}
-
-.type {
- color: #ffa120;
-}
-
-.left-abs, .right-abs {
- color: #6b82ff;
-}
-
-.left-app, .right-app {
- color: #ff8750;
-}
-
-.index {
- color: #ff5050;
-}
-
-.number {
- color: #b1ee13;
+ margin: 0;
+ padding: .5em;
}
diff --git a/docs/content.js b/docs/content.js
deleted file mode 100644
index f107fc5..0000000
--- a/docs/content.js
+++ /dev/null
@@ -1,26 +0,0 @@
-const code = document.getElementsByTagName("pre")[0]
-
-const fixPath = p => p.replace("/", "_")
-
-const term = t => t
- .replaceAll(/(\([+-][0-9]+[ubt]?\))/g, "<span class='number'>$1</span>")
- .replaceAll(/(?<!\>)(\()/g, "<span class='left-app'>(</span>")
- .replaceAll(/(\))(?!\<)/g, "<span class='right-app'>)</span>")
- .replaceAll("[", "<span class='left-abs'>[</span>")
- .replaceAll("]", "<span class='right-abs'>]</span>")
- .replaceAll(/(?<![+-\d])([0-9])/g, "<span class='index'>$1</span>")
-
-code.innerHTML = code.innerHTML
- .replaceAll(/^:import std\/(.*) (.*)$/gm, (_, p, s) => `<span class="com">:import</span> <a href='${fixPath(p)}.bruijn.html'>std/${p}</a> ${s}`)
- .replaceAll(/^:input std\/(.*)$/gm, (_, p) => `<span class="com">:input</span> <a href='${fixPath(p)}.bruijn.html'>std/${p}</a>`)
- .replaceAll(/^:test \((.*)\) \((.*)\)$/gm, (_, t1, t2) => `<span class='com'>:test</span> (${term(t1)}) (${term(t2)})`)
- .replaceAll(/^([^:\n<#][^ ]*) (.*)$/gm, (_, d, t) => `<span class='def'>${d}</span> ${term(t)}`)
- .replaceAll(/^# (.*)$/gm, "<span class='comment'># $1</span>")
- .replaceAll(/ ⧗ (.*)\n/g, " ⧗ <span class='type'>$1</span>\n")
-
-code.innerHTML = `<span class="line"></span>${code.innerHTML}<span class="cl"></span>`
-const lines = code.innerHTML.split(/\n/).length - 1
-for (let i = 0; i < lines; i++) {
- const cur = code.getElementsByTagName("span")[0]
- cur.innerHTML += `<span>${i + 1}</span>`
-}
diff --git a/docs/content.template b/docs/content.template
index a2d5c6e..470acb4 100644
--- a/docs/content.template
+++ b/docs/content.template
@@ -4,14 +4,17 @@
<meta charset="UTF-8" />
<meta name="viewport" content="width=device-width" />
<link rel="stylesheet" href="content.css" type="text/css" media="all">
+ <link rel="stylesheet" href="code.css" type="text/css" media="all">
<title>bruijn std/NAME</title>
</head>
<body>
<h1>NAME</h1>
<pre>
+<code class="language-bruijn">
CONTENT
+</code>
</pre>
- <script src="content.js" charset="utf-8"></script>
+ <script src="code.js" charset="utf-8"></script>
</body>
</html>
diff --git a/docs/gen.sh b/docs/gen.sh
index f79ce6b..7b5eb72 100755
--- a/docs/gen.sh
+++ b/docs/gen.sh
@@ -17,7 +17,7 @@ done
sed -e "s@LINKS@$links@g" index.template >std/index.html
-cp res/* content.js content.css index.css std/
+cp res/* code.js content.css index.css code.css std/
echo "std done"
diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml
index 1b7fd60..5f7f14f 100644
--- a/docs/mkdocs.yml
+++ b/docs/mkdocs.yml
@@ -2,7 +2,8 @@ site_name: Bruijn Wiki
docs_dir: wiki_src/
site_dir: wiki/
-extra_css: [custom.css]
+extra_css: [custom.css, ../code.css]
+extra_javascript: [../code.js]
theme:
name: terminal
diff --git a/docs/wiki_src/coding/compilation.md b/docs/wiki_src/coding/compilation.md
index 9863c21..330bc9f 100644
--- a/docs/wiki_src/coding/compilation.md
+++ b/docs/wiki_src/coding/compilation.md
@@ -1,6 +1,6 @@
# Compilation
-Bruijn can be compiled to John Tromp’s binary lambda calculus (BLC).
+Bruijn can be compiled to John Tromp's binary lambda calculus (BLC).
BLC uses the following encoding:
@@ -12,26 +12,27 @@ BLC uses the following encoding:
There are two modes of compilation:
-- **Bitwise** compiles to BLC and encodes every bit as 1 bit and pads
- the last remaining byte: `bruijn -b path`
-- **ASCII** compiles to BLC and encodes every bit as 1 ASCII character
- (`'0'`/`'1'`): `bruijn -B path`
+- **Bitwise** compiles to BLC and encodes every bit as 1 bit and pads
+ the last remaining byte: `bruijn -b path`
+- **ASCII** compiles to BLC and encodes every bit as 1 ASCII character
+ (`'0'`/`'1'`): `bruijn -B path`
## Compilation overhead
Typical compilation to BLC results in much redundant code, since every
used function gets substituted and translated separately. In
-`((+3) + (+4) + (+3))`, for example, `add` gets compiled to BLC two
-times, resulting in a redundant overhead of around 3500 bits.
+`((+3) + (+4) + (+3))`{.bruijn}, for example, `add`{.bruijn} gets
+compiled to BLC two times, resulting in a redundant overhead of around
+3500 bits.
This is because BLC was never intended for compilation of normal
programs, but mainly as an academic encoding model. This also means that
-it’s quite good for writing very expressive and minimal programs
-(i.e. obfuscated code golfing, see [John Tromp’s
+it's quite good for writing very expressive and minimal programs
+(i.e. obfuscated code golfing, see [John Tromp's
IOCCC](https://ioccc.org/2012/tromp/hint.html)).
-Most programs, however, won’t be golfed and can result in rather large
-compiled programs. While there’s not really any practical need for
+Most programs, however, won't be golfed and can result in rather large
+compiled programs. While there's not really any practical need for
compilation aside from golfing, you could still use the
[BLoC](https://github.com/marvinborner/bloc) project to optimize
redundant terms.
diff --git a/docs/wiki_src/coding/data-structures.md b/docs/wiki_src/coding/data-structures.md
index 0516bf7..3d2a387 100644
--- a/docs/wiki_src/coding/data-structures.md
+++ b/docs/wiki_src/coding/data-structures.md
@@ -39,7 +39,7 @@ syntactic sugar.
- default syntactic sugar for numbers (optional suffix `t`),
e.g. `(+3)`{.bruijn}
-- encoding: `(+4)`{.bruijn}=`[[[[(1 (1 3))]]]]`,
+- encoding: `(+4)`{.bruijn}=`[[[[(1 (1 3))]]]]`{.bruijn},
`(-4)`{.bruijn}=`[[[[(2 (2 3))]]]]`{.bruijn}
- faster and more compact than binary[^1]
- positive and negative numbers
diff --git a/docs/wiki_src/coding/meta-programming.md b/docs/wiki_src/coding/meta-programming.md
index 5d1caa0..334e285 100644
--- a/docs/wiki_src/coding/meta-programming.md
+++ b/docs/wiki_src/coding/meta-programming.md
@@ -1,4 +1,4 @@
-# Meta programming
+# Metaprogramming
Bruijn has a homoiconic meta encoding inspired by Lisp's quoting
feature.
@@ -8,11 +8,9 @@ self-interpretation](https://text.marvinborner.de/2023-09-03-21.html).
## Encoding
-``` bruijn
-`X ⤳ [[[2 (+Xu)]]]
-`(M N) ⤳ [[[1 `M `N]]]
-`[M] ⤳ [[[0 `M]]]
-```
+ `X ⤳ [[[2 (+Xu)]]]
+ `(M N) ⤳ [[[1 `M `N]]]
+ `[M] ⤳ [[[0 `M]]]
Any quoted term gets converted to this encoding:
diff --git a/docs/wiki_src/custom.css b/docs/wiki_src/custom.css
index 170b4cc..d68a10c 100644
--- a/docs/wiki_src/custom.css
+++ b/docs/wiki_src/custom.css
@@ -2,7 +2,16 @@ pre {
width: 100%;
white-space: pre;
overflow-x: scroll;
- display: inline-grid;
+ display: grid;
+}
+
+/* to match std */
+pre, pre > code, code.bruijn {
+ background-color: #222222;
+}
+
+pre a {
+ color: var(--font-color);
}
.headerlink {
diff --git a/docs/wiki_src/introduction/lambda-calculus.md b/docs/wiki_src/introduction/lambda-calculus.md
index 574c5ee..067eaad 100644
--- a/docs/wiki_src/introduction/lambda-calculus.md
+++ b/docs/wiki_src/introduction/lambda-calculus.md
@@ -30,11 +30,9 @@ When we talk about reduction in bruijn, we typically mean "reduction
until normal form" -- we reduce until the term can't be reduced any
further (there does not exist any `((λx.E) A)`).
-``` bruijn
-((λx.x) (λx.x)) ⤳ (λx.x)
-((λx.x) (λx.λy.x)) ⤳ (λx.λy.x)
-((λx.λy.x) (λx.x)) ⤳ (λy.λx.x)
-```
+ ((λx.x) (λx.x)) ⤳ (λx.x)
+ ((λx.x) (λx.λy.x)) ⤳ (λx.λy.x)
+ ((λx.λy.x) (λx.x)) ⤳ (λy.λx.x)
## De Bruijn indices
@@ -49,9 +47,9 @@ De Bruijn replace the concept of variables by using numeric references
to the abstraction layer. Let me explain using an example: The
expression `λx.x` becomes `λ0` -- the `0` refers to the first parameter
of the abstraction. Subsequently, the expression `λx.λy.x y` becomes
-`λλ1 0`{.bruijn}. Basically, if you're reading from left to right
-starting at the abstraction you want to bind, you increment on every
-occurring `λ` until you arrive at the index.
+`λλ1 0`. Basically, if you're reading from left to right starting at the
+abstraction you want to bind, you increment on every occurring `λ` until
+you arrive at the index.
While confusing at first, programs written with De Bruijn indices can
actually be way easier to understand than the equivalent program with
@@ -72,10 +70,10 @@ The application of `λ0` and `λλ1 0` becomes `[0] [[1 0]]`{.bruijn}.
Random example reductions:
``` bruijn
-[0] [[1]] ⤳ [[1]]
-[[0]] [[1]] ⤳ [0]
-[[1]] [[1]] ⤳ [[[1]]]
-[[0]] [0] [[1]] ⤳ [[1]]
-[[0 1]] [0] ⤳ [0 [0]]
-[[1 0]] [0] ⤳ [0]
+a [0] [[1]] ⤳ [[1]]
+b [[0]] [[1]] ⤳ [0]
+c [[1]] [[1]] ⤳ [[[1]]]
+d [[0]] [0] [[1]] ⤳ [[1]]
+e [[0 1]] [0] ⤳ [0 [0]]
+f [[1 0]] [0] ⤳ [0]
```
diff --git a/docs/wiki_src/introduction/syntax.md b/docs/wiki_src/introduction/syntax.md
index 4dbc784..e14f8c6 100644
--- a/docs/wiki_src/introduction/syntax.md
+++ b/docs/wiki_src/introduction/syntax.md
@@ -138,9 +138,9 @@ structures](../coding/data-structures.md).
- *Numbers*: `(SXB)`{.bruijn} where `S` is `+`/`-`, `X` is a number
and `B` is the *base* of the encoded number (or `t` by default)
- - `u` for unary base (postive, Church): `(+42u)`
- - `b` for binary base (positive): `(+42b)`
- - `t` for balanced ternary (positive/negative): `(-42t)`
+ - `u` for unary base (postive, Church): `(+42u)`{.bruijn}
+ - `b` for binary base (positive): `(+42b)`{.bruijn}
+ - `t` for balanced ternary (positive/negative): `(-42t)`{.bruijn}
- *Characters*: `'C'`{.bruijn} where `C` is any ASCII character
- *Strings*: `"X1..XN"`{.bruijn} where `X1...XN` are any ASCII
characters