diff options
| -rw-r--r-- | docs/.gitignore | 1 | ||||
| -rw-r--r-- | docs/content.css | 65 | ||||
| -rw-r--r-- | docs/content.js | 26 | ||||
| -rw-r--r-- | docs/content.template | 17 | ||||
| -rwxr-xr-x | docs/gen.sh | 20 | ||||
| -rw-r--r-- | docs/index.css | 14 | ||||
| -rw-r--r-- | docs/index.html | 121 | ||||
| -rw-r--r-- | docs/index.template | 15 | ||||
| -rw-r--r-- | docs/readme.md | 4 | ||||
| -rw-r--r-- | docs/res/logo.png | bin | 0 -> 29198 bytes | |||
| -rw-r--r-- | docs/script.js | 50 | ||||
| -rw-r--r-- | docs/style.css | 160 | ||||
| -rw-r--r-- | readme.md | 7 |
13 files changed, 498 insertions, 2 deletions
diff --git a/docs/.gitignore b/docs/.gitignore new file mode 100644 index 0000000..4e1ae2d --- /dev/null +++ b/docs/.gitignore @@ -0,0 +1 @@ +std/ diff --git a/docs/content.css b/docs/content.css new file mode 100644 index 0000000..941e5c3 --- /dev/null +++ b/docs/content.css @@ -0,0 +1,65 @@ +body { + font-family: monospace; + background-color: #222222; + color: #cccccc; + font-size: 1.2em; +} + +a { + color: #cccccc; +} + +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; +} diff --git a/docs/content.js b/docs/content.js new file mode 100644 index 0000000..4fb7a16 --- /dev/null +++ b/docs/content.js @@ -0,0 +1,26 @@ +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(/(?<![+-0-9])([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 new file mode 100644 index 0000000..c19461f --- /dev/null +++ b/docs/content.template @@ -0,0 +1,17 @@ +<!DOCTYPE html> +<html> + <head> + <meta charset="UTF-8" /> + <meta name="viewport" content="width=device-width" /> + <link rel="stylesheet" href="content.css" type="text/css" media="all"> + <title>bruijn std/</title> + </head> + <body> + <h1>NAME</h1> +<pre> +CONTENT +</pre> + + <script src="content.js" charset="utf-8"></script> + </body> +</html> diff --git a/docs/gen.sh b/docs/gen.sh new file mode 100755 index 0000000..4e7a80b --- /dev/null +++ b/docs/gen.sh @@ -0,0 +1,20 @@ +#!/bin/env bash + +set -e + +rm -rf std/ && mkdir -p std/ + +files=$(find ../std/ -type f | sort) +links="" + +for file in $files; do + name=$(echo $file | cut -c8-) + filename=$(sed s@/@_@g <<<"$name") + links="$links\n<li><span class='com'>:import</span> <a href="$filename.html">$name</a></li>" + awk 'NR==FNR { gsub("<", "\\<", $0); gsub(">", "\\>", $0); a[n++]=$0; next } /CONTENT/ { for (i=0;i<n;++i) print a[i]; next } 1' "$file" content.template >std/$filename.html + sed -i -e "s@NAME@$name@g" std/$filename.html +done + +sed -e "s@LINKS@$links@g" index.template >std/index.html + +cp content.js content.css index.css std/ diff --git a/docs/index.css b/docs/index.css new file mode 100644 index 0000000..1e70968 --- /dev/null +++ b/docs/index.css @@ -0,0 +1,14 @@ +body { + font-family: monospace; + background-color: #222222; + color: #cccccc; + font-size: 1.2em; +} + +a { + color: #cccccc; +} + +.com { + color: #ff64bd; +} diff --git a/docs/index.html b/docs/index.html new file mode 100644 index 0000000..1644c88 --- /dev/null +++ b/docs/index.html @@ -0,0 +1,121 @@ +<!DOCTYPE html> +<html> + <head> + <meta charset="UTF-8" /> + <meta name="viewport" content="width=device-width" /> + <link rel="stylesheet" href="style.css" type="text/css" media="all"> + <title>bruijn</title> + </head> + <body> + <div class="header"> + <img src="res/logo.png" /> + <h1>bruijn</h1> + </div> + + <div class="example"> + <pre class="code"> +<span class="def">pow</span> <span class="term">[<span class="symbol">…!!…</span> (<span class="symbol">iterate</span> (<span class="symbol">…⋅…</span> 0) <span class="ternary">(+1)</span>)]</span> + +<span class="def">…**…</span> <span class="symbol">pow</span> + +<span class="com">:test</span> <span class="test">(<span class="term"><span class="ternary">(+2)</span> <span class="mixfix">**</span> <span class="ternary">(+3)</span> <span class="mixfix">=?</span> <span class="ternary">(+8)</span></span>)</span> <span class="test">(<span class="symbol">true</span>)</span></pre> + + <p> + Functional language based on pure bruijn-indexed lambda calculus. + </p> + </div> + + <div class="bar small"> + <b>Hint</b>: Click on anything you don't understand. + </div> + + <div class="example"> + <p> + Lambdas all the way down.<br> + No primitive functions. + </p> + <pre class="code"> +<span class="repl">></span> <span class="ternary">(+5)</span> +<span class="term">[[[[2 (2 (1 3))]]]]</span> +<span class="repl">></span> <span class="char">'a'</span> +<span class="term">[[[1 (0 (0 (0 (0 (1 (1 (0 2)))))))]]]</span> +<span class="repl">></span> <span class="symbol">add</span> +<span class="term">[[(([([[1 0 [[0]]]] ((((0 [[(((0...</span></pre> + </div> + + <div class="example"> + <pre class="code"> +<span class="repl">></span> <span class="com">:time</span> <span class="symbol">factorial</span> <span class="ternary">(+30)</span> +<span class="time">0.35 seconds</span></pre> + <p> + Efficient call-by-need reduction using abstract machines. + </p> + </div> + + <div class="example"> + <p> + Substantial standard library.<br> + <a href="std/">Docs</a> + </p> + <pre class="code"> +<span class="repl">></span> <span class="mixfix">∏</span> <span class="ternary">(+1)</span> <span class="mixfix">→</span> <span class="ternary">(+3)</span> <span class="mixfix">|</span> <span class="symbol">++‣</span> +<span class="repl">></span> <span class="symbol">number!</span> <span class="mixfix"><$></span> <span class="left-app">(</span><span class="symbol">lines</span> <span class="string">"42\n25"</span><span class="right-app">)</span> +<span class="repl">></span> <span class="term"><span class="symbol">sum</span> (<span class="symbol">take</span> <span class="ternary">(+3)</span> (<span class="symbol">repeat</span> <span class="ternary">(+4)</span>))</span> +<span class="repl">></span> <span class="binary">(+10b)</span> <span class="mixfix">⋀!</span> <span class="binary">(+12b)</span></pre> + </div> + + <div class="example"> + <pre class="code"> +$ echo "main [0]" > echo.bruijn +$ bruijn -b echo.bruijn > echo +$ wc -c echo +2 echo +$ echo "hello world!" | bruijn -e echo +hello world!</pre> + <p> + Compilation to Tromp's binary lambda calculus.<br> + Support for byte and ASCII encoding. + </p> + </div> + + <div class="bar big"> + Learn more: <a href="https://github.com/marvinborner/bruijn">GitHub</a> + </div> + + <div class="instructions"> + <h1>Installation</h1> + <pre class="code"> +$ git clone https://github.com/marvinborner/bruijn.git && cd bruijn +$ <span class="stack">stack</span> run # for playing around +$ <span class="stack">stack</span> install +$ bruijn</pre> + </div> + + <div class="instructions"> + <h1>Broogle</h1> + <pre class="code"> +$ ./broogle.sh -f add +<span class="def">add</span> ⧗ Unary → Unary → Unary +also known as <span class="def">…+…</span> +in std/Number/Unary.bruijn:35 +# adds two unary numbers +...</pre> + </div> + + <div class="instructions"> + <h1>Syntax highlighting</h1> + <ol> + <li>Use vim and vim-plug</li> + <li>Add "Plug 'marvinborner/bruijn', { 'rtp': 'editors/vim' }" to your .vimrc</li> + <li>Run :PlugInstall</li> + </ol> + Learn more: <a href="https://github.com/marvinborner/bruijn/tree/main/editors">GitHub</a> + </div> + + <div class="bar big"> + Standard library: <a href="std/">Docs</a> + </div> + + <script src="script.js" charset="utf-8"></script> + </body> +</html> diff --git a/docs/index.template b/docs/index.template new file mode 100644 index 0000000..9cbb1f5 --- /dev/null +++ b/docs/index.template @@ -0,0 +1,15 @@ +<!DOCTYPE html> +<html> + <head> + <meta charset="UTF-8" /> + <meta name="viewport" content="width=device-width" /> + <link rel="stylesheet" href="index.css" type="text/css" media="all"> + <title>bruijn standard library</title> + </head> + <body> + <h1>bruijn standard library</h1> + <ol> + LINKS + </ol> + </body> +</html> diff --git a/docs/readme.md b/docs/readme.md new file mode 100644 index 0000000..a8b0829 --- /dev/null +++ b/docs/readme.md @@ -0,0 +1,4 @@ +# Docs + +Visit the compiled [docs](https://bruijn.marvinborner.de) for the full +experience. diff --git a/docs/res/logo.png b/docs/res/logo.png Binary files differnew file mode 100644 index 0000000..aa2d80b --- /dev/null +++ b/docs/res/logo.png diff --git a/docs/script.js b/docs/script.js new file mode 100644 index 0000000..21f0cdf --- /dev/null +++ b/docs/script.js @@ -0,0 +1,50 @@ +[...document.getElementsByClassName("term")].forEach(el => { + el.innerHTML = el.innerHTML + .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(/(?<!\+)([0-9])/g, "<span class='index'>$1</span>") +}) + +const clearPopups = () => { + [...document.getElementsByClassName("popup")].forEach(el => { + el.remove() + }) +} + +const notify = (s, e) => { + console.log(e); + clearPopups() + const popup = document.createElement("div") + popup.className = "popup" + const content = document.createTextNode(s) + popup.style.left = e.pageX + "px"; + popup.style.top = e.pageY + "px"; + popup.appendChild(content) + document.body.appendChild(popup) +} + +const describe = (c, d) => { + [...document.getElementsByClassName(c)].forEach(el => el.addEventListener("click", e => notify(d, e))); +} + +describe("binary", "Syntactic sugar for a binary number representation using abstractions as data. Needs a sign and brackets to differentiate it from bruijn indices"); +describe("char", "Syntactic sugar for a binary representation of characters using abstractions as data."); +describe("com", "This indicates a command to the interpreter. The most common commands are :test (verifying α-equivalency) and :import (importing definitions from other files)."); +describe("def", "This defines a new term substitution."); +describe("header", "[0] is the identity operation. It returns the first argument it gets. Nothing more."); +describe("index", "These numbers reference the nth abstraction, starting counting from the inside. These 'bruijn indices' replace the concept of variables in lambda calculus."); +describe("left-abs", "The opening bracket of a function abstraction. It's basically the equivalent of the λ in lambda calculus."); +describe("left-app", "The opening bracket of a function application."); +describe("mixfix", "This is a mixfix operator. They can be defined like …*… where the … can then be any other term. You can use them without the … as a notation of function application."); +describe("repl", "This indicates a REPL input."); +describe("right-abs", "The closing bracket of a function abstraction."); +describe("right-app", "The closing bracket of a function application."); +describe("stack", "Stack is a dependency manager for Haskell. Install it using the corresponding instructions for your operating system.") +describe("string", "Syntactic sugar for a list of binary encoded chars.") +describe("symbol", "This substitutes a previously defined term (for example from the standard library)."); +describe("ternary", "Syntactic sugar for a balanced ternary number representation using abstractions as data. Needs a sign and brackets to differentiate it from bruijn indices."); +describe("time", "Incredibly fast for lambda calculus standards."); + +document.body.addEventListener("click", clearPopups, true) diff --git a/docs/style.css b/docs/style.css new file mode 100644 index 0000000..7eec6b0 --- /dev/null +++ b/docs/style.css @@ -0,0 +1,160 @@ +body { + font-family: monospace; + background-color: #222222; + color: #cccccc; + font-size: 1.2em; + padding: 0; + margin: 0; +} + +a { + color: #cccccc; +} + +.header { + display: flex; + align-items: center; + flex-direction: column; +} + +.header img { + width: auto; + max-height: 20vh; +} + +.header h1 { + margin-top: -0.5em; + font-size: 3em; +} + +.example { + display: flex; + align-items: center; + justify-content: center; + flex-flow: row wrap; + column-gap: 5vw; + max-width: 80%; + margin: 0 auto; +} + +.example p { + font-size: 1.3em; + max-width: 80vw; + text-align: center; +} + +.instructions { + max-width: 80%; + margin: 0 auto; +} + +@media(min-width: 768px) { + .example { + flex-flow: row nowrap; + max-width: 80%; + } + + .example p { + width: 30vw; + font-size: 1.5em; + } + + .instructions { + max-width: 80%; + } +} + +@media(min-width: 1800px) { + .example { + flex-flow: row nowrap; + max-width: 35%; + } + + .instructions { + max-width: 35%; + } +} + +.bar { + text-align: center; + background-color: #333333; + margin: 30px 0; +} + +.bar.small { + font-size: 1.2em; + line-height: 1.2em; + padding: 15px; +} + +.bar.big { + font-size: 2em; + line-height: 5em; + padding: 20px; +} + +.bar a { + color: #cccccc; +} + +.popup { + position: absolute; + display: block; + border-sizing: border-box; + box-shadow: 0 10px 50px rgba(0,0,0,.6); + background-color: #333333; + border-radius: 10px; + padding: 15px; + max-width: 300px; +} + +.code { + background-color: #333333; + padding: 15px; + font-size: 1.2em; + border-radius: 10px; +} + +.instructions .code { + overflow-x: scroll; +} + +.code .repl { + color: #13dbee; +} + +.code .def { + color: #13dbee; +} + +.code .left-abs, .code .right-abs { + color: #6b82ff; +} + +.code .left-app, .code .right-app { + color: #ff8750; +} + +.code .com { + color: #ff64bd; +} + +.code .ternary, .code .binary { + color: #b1ee13; +} + +.code .char, .code .string { + color: #b1ee13; +} + +.code .mixfix { + color: #eee513; +} + +.code .symbol { + color: #f9f9f9; +} + +.code .index { + color: #ff5050; +} @@ -6,6 +6,8 @@ [Jump to examples](#Examples) or use the navigation tree to jump to other sections. +Docs, examples and more: [website](https://bruijn.marvinborner.de). + ## Features - **De Bruijn indices[\[0\]](#References)** eliminate the complexity of @@ -261,7 +263,7 @@ Some other great functions: # lazy evaluation using infinite lists and indexing pow2 …!!… (iterate (…⋅… (+2)) (+1)) - :test ((pow2 (+5)) =? ((+32))) (true) + :test ((pow2 (+5)) =? (+32)) (true) # options :test (map inc (some (+1))) (some (+2)) @@ -274,7 +276,8 @@ Some other great functions: :test (main [0]) (false) -Read the files in `std/` for an overview of all functions/libraries. +Read the files in `std/` for an overview of all functions/libraries or +visit the interactive [website](https://bruijn.marvinborner.de). ### Compilation to BLC |
