diff options
| -rw-r--r-- | docs/index.html | 28 | ||||
| -rw-r--r-- | docs/script.js | 138 |
2 files changed, 111 insertions, 55 deletions
diff --git a/docs/index.html b/docs/index.html index 0f63a7a..97747f0 100644 --- a/docs/index.html +++ b/docs/index.html @@ -19,11 +19,11 @@ <div class="example"> <div class="left"> <pre class="code"> -<span class="def">pow</span> <span class="term">[<span class="symbol">index</span> (<span class="symbol">iterate</span> (<span class="symbol">mul</span> 0) <span class="ternary">(+1)</span>)]</span> +<span class="def">pow</span> <span class="term">[<span class="symbol" data-std="List_Church.bruijn.html#index">index</span> (<span class="symbol" data-std="List_Church.bruijn.html#iterate">iterate</span> (<span class="symbol" data-std="Number_Ternary.bruijn.html#mul">mul</span> 0) <span class="ternary">(+1)</span>)]</span> -<span class="def">…**…</span> <span class="symbol">pow</span> +<span class="def">…**…</span> <span class="symbol" data-std="Math.bruijn.html#pow">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> +<span class="com">:test</span> <span class="test">(<span class="term"><span class="ternary">(+2)</span> <span class="mixfix" data-std="Math.bruijn.html#pow">**</span> <span class="ternary">(+3)</span> <span class="mixfix" data-std="Number_Ternary.bruijn.html#eq?">=?</span> <span class="ternary">(+8)</span></span>)</span> <span class="test">(<span class="symbol" data-std="Logic_Binary.bruijn.html#true">true</span>)</span></pre> </div> <div class="right"> @@ -51,13 +51,13 @@ <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="repl">></span> <span class="symbol" data-std="Number_Ternary.bruijn.html#add">add</span> <span class="term">[[(([([[1 0 [[0]]]] ((((0 [[(((0...</span></pre> </div> <div class="left"> <pre class="code"> -<span class="repl">></span> <span class="com">:time</span> <span class="symbol">factorial</span> <span class="ternary">(+42)</span> +<span class="repl">></span> <span class="com">:time</span> <span class="symbol" data-std="Math.bruijn.html#fac">factorial</span> <span class="ternary">(+42)</span> <span class="time">0.01 seconds</span></pre> </div> <div class="right"> @@ -75,10 +75,10 @@ </div> <div class="right"> <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> +<span class="repl">></span> <span class="mixfix" data-std="Math.bruijn.html#∏…→…|…">∏</span> <span class="ternary">(+1)</span> <span class="mixfix" data-std="Math.bruijn.html#∏…→…|…">→</span> <span class="ternary">(+3)</span> <span class="mixfix" data-std="Math.bruijn.html#∏…→…|…">|</span> <span class="symbol" data-std="Number_Ternary.bruijn.html#inc">++‣</span> +<span class="repl">></span> <span class="symbol" data-std="String.bruijn.html#string→number">number!</span> <span class="mixfix" data-std="List_Church.bruijn.html#map"><$></span> <span class="left-app">(</span><span class="symbol" data-std="String.bruijn.html#lines">lines</span> <span class="string">"42\n25"</span><span class="right-app">)</span> +<span class="repl">></span> <span class="term"><span class="symbol" data-std="Math.bruijn.html#sum">sum</span> (<span class="symbol" data-std="List_Church.bruijn.html#take">take</span> <span class="ternary">(+3)</span> (<span class="symbol" data-std="List_Church.bruijn.html#repeat">repeat</span> <span class="ternary">(+4)</span>))</span> +<span class="repl">></span> <span class="binary">(+10b)</span> <span class="mixfix" data-std="Number_Binary.bruijn.html#and!">⋀!</span> <span class="binary">(+12b)</span></pre> </div> <div class="left"> @@ -107,9 +107,9 @@ hello world!</pre </div> <div class="right"> <pre class="code"> -<span class="repl">></span> <span class="symbol">length</span> <span class="meta">`</span><span class="symbol">factorial</span> -<span class="repl">></span> <span class="prefix">!</span><span class="left-app">(</span><span class="symbol">swap</span> <span class="meta">`</span><span class="left-app">(</span><span class="unary">(+2u)</span> <span class="unary">(+3u)</span><span class="right-app">))</span> -<span class="repl">></span> <span class="symbol">lhs</span> <span class="left-app">(</span><span class="symbol">blc→meta</span> <span class="string">"010000100000110"</span><span class="right-app">)</span> +<span class="repl">></span> <span class="symbol" data-std="Meta.bruijn.html#length">length</span> <span class="meta">`</span><span class="symbol" data-std="Math.bruijn.html#fac">factorial</span> +<span class="repl">></span> <span class="prefix" data-std="Meta.bruijn.html#eval">!</span><span class="left-app">(</span><span class="symbol" data-std="Meta.bruijn.html#swap">swap</span> <span class="meta">`</span><span class="left-app">(</span><span class="unary">(+2u)</span> <span class="unary">(+3u)</span><span class="right-app">))</span> +<span class="repl">></span> <span class="symbol" data-std="Meta.bruijn.html#lhs">lhs</span> <span class="left-app">(</span><span class="symbol" data-std="Meta.bruijn.html#blc→meta">blc→meta</span> <span class="string">"010000100000110"</span><span class="right-app">)</span> </pre> </div> </div> @@ -132,8 +132,8 @@ $ bruijn</pre> <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> +<span class="def" data-std="Number_Unary.bruijn.html#add">add</span> ⧗ Unary → Unary → Unary +also known as <span class="def" data-std="Number_Unary.bruijn.html#add">…+…</span> in std/Number/Unary.bruijn:35 # adds two unary numbers ...</pre> diff --git a/docs/script.js b/docs/script.js index b388472..043b336 100644 --- a/docs/script.js +++ b/docs/script.js @@ -1,53 +1,109 @@ -[...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>") -}) +[...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() - }) -} + [...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 notify = (s, e, cb) => { + clearPopups(); + const popup = document.createElement("div"); + popup.className = "popup"; + const content = document.createElement("div"); + content.innerHTML = s; + popup.style.left = e.pageX + "px"; + popup.style.top = e.pageY + "px"; + popup.style.cursor = "pointer"; + popup.appendChild(content); + document.body.appendChild(popup); + popup.addEventListener("click", cb, { once: true }); +}; + +// TODO: maybe this should be combined with std_map (less hard coding) +// this would require imports etc on index.html examples +const symbolJump = (p) => { + if (p === null) return; + const url = `https://bruijn.marvinborner.de/std/${p}`; + window.open(url, "_blank").focus(); +}; const describe = (c, d) => { - [...document.getElementsByClassName(c)].forEach(el => el.addEventListener("click", e => notify(d, e))); -} + [...document.getElementsByClassName(c)].forEach((el) => + el.addEventListener("click", (e) => + notify(d, e, () => symbolJump(el.getAttribute("data-std"))), + ), + ); +}; -describe("binary", "Syntactic sugar for a binary number representation using abstractions as data. Needs a sign and brackets to differentiate it from de 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. Using this identifier will substitute the term on its right side."); -describe("header", "[0] is the identity operation. It returns the first argument it gets. Nothing more."); -describe("index", "This number references the nth abstraction, starting counting from the inside. These 'de 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( + "binary", + "Syntactic sugar for a binary number representation using abstractions as data. Needs a sign and brackets to differentiate it from de 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. Using this identifier will substitute the term on its right side.", +); +describe( + "header", + "[0] is the identity operation. It returns the first argument it gets. Nothing more.", +); +describe( + "index", + "This number references the nth abstraction, starting counting from the inside. These 'de 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("meta", "This is the quote operator. It converts any given expression to bruijn's meta encoding. The meta encoding can be used for self modification and can be turned back to normal bruijn code."); -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("prefix", "This is a prefix operator. They can be defined like *‣ where the ‣ can then be any other term."); +describe( + "meta", + "This is the quote operator. It converts any given expression to bruijn's meta encoding. The meta encoding can be used for self modification and can be turned back to normal bruijn code.", +); +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. Click to jump to its definition.", +); +describe( + "prefix", + "This is a prefix operator. They can be defined like *‣ where the ‣ can then be any other term. Click to jump to its definition.", +); 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 de Bruijn indices."); +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. <u>Click</u> to jump to its definition.", +); +describe( + "ternary", + "Syntactic sugar for a balanced ternary number representation using abstractions as data. Needs a sign and brackets to differentiate it from de Bruijn indices.", +); describe("time", "Incredibly fast for lambda calculus standards."); -describe("unary", "Syntactic sugar for a unary number representation using abstractions as data. This is commonly known as a Church numeral. Needs a sign and brackets to differentiate it from de Bruijn indices."); +describe( + "unary", + "Syntactic sugar for a unary number representation using abstractions as data. This is commonly known as a Church numeral. Needs a sign and brackets to differentiate it from de Bruijn indices.", +); -document.body.addEventListener("click", clearPopups, true) +document.body.addEventListener("click", clearPopups, true); |