Started creating new docs with wiki

4 files changed, 254 insertions, 0 deletions

diff --git a/docs/wiki_src/introduction/installation.md b/docs/wiki_src/introduction/installation.md
new file mode 100644
index 0000000..3334ad3
--- /dev/null
+++ b/docs/wiki_src/introduction/installation.md
@@ -0,0 +1,24 @@
+# Installation
+
+You first need to install Haskell's
+[Stack](https://docs.haskellstack.org/en/stable/) using their official
+instructions for your operating system. After that, clone the bruijn
+repository using
+
+``` bash
+$ git clone https://github.com/marvinborner/bruijn
+$ cd bruijn
+```
+
+Then, run bruijn using `stack run`{.bash}. This starts bruijn's
+[REPL](../coding/REPL.md). You can now play around with bruijn.
+
+Passing normal arguments to `bruijn`{.bash} with `stack`{.bash} can be
+done with `stack run -- [args]`. If you enjoy it, you can install
+`bruijn` into your stack path using `stack install`.
+
+------------------------------------------------------------------------
+
+Please create an issue on
+[GitHub](https://github.com/marvinborner/bruijn/issues/new) if you
+encounter any issues.
diff --git a/docs/wiki_src/introduction/lambda-calculus.md b/docs/wiki_src/introduction/lambda-calculus.md
new file mode 100644
index 0000000..59a7c59
--- /dev/null
+++ b/docs/wiki_src/introduction/lambda-calculus.md
@@ -0,0 +1,76 @@
+# Lambda calculus
+
+Bruijn is based on De Bruijn indexed lambda calculus.
+
+## Traditional lambda calculus
+
+Lambda calculus basically has three types of expressions:
+
+-   *Variable*: `x` represents another expression.
+-   *Abstraction*: `λx.E` accepts an argument x and binds it to
+    expression `E` respectively. It's helpful to think of abstractions
+    as anonymous functions.
+-   *Application*: `(f x)` applies `f` to `x` -- the standard convention
+    allows repeated left-associative application: `(f x y z)` is
+    `(((f x) y) z)`.
+
+Combining these expressions and removing redundant parentheses can
+result in expressions like λx.λy.x y, basically representing a function
+with two parameters that uses its second parameter as an argument for
+its first.
+
+Evaluating expressions is called *reduction*. There's only one rule you
+need to know: `((λx.E) A)` becomes `E[x := A]` -- that is, calling an
+abstraction with an argument substitutes the argument inside the
+expression of the abstraction ("β-reduction"). There are many different
+kinds of reduction techniques, but they basically all come back to this
+simple rule -- mainly because of the "Church-Rosser theorem" that states
+that the order of reduction doesn't change the eventual result.
+
+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)`).
+
+## De Bruijn indices
+
+Programs written in lambda calculus often have many abstractions and
+therefore at least as many variables. I hate naming variables,
+especially if you need hundreds of them for small programs. With that
+many variables it's also really complicated to compare two expressions,
+since you first need to resolve shadowed and conflicting variables
+("α-conversion").
+
+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.
+
+While confusing at first, programs written with De Bruijn indices can
+actually be way easier to understand than the equivalent program with
+named variables.
+
+## Bruijn's bracketing
+
+Bruijn's final syntactic variation from lambda calculus is the use of
+square brackets instead of lambda symbols. By putting the entire
+abstracted term in brackets, it's much clearer where indices and the
+respective terms are bound to.
+
+Representing `λλ1 0` in bruijn's syntax then becomes `[[1 0]]`{.bruijn}.
+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]
+```
diff --git a/docs/wiki_src/introduction/setup.md b/docs/wiki_src/introduction/setup.md
new file mode 100644
index 0000000..92f9886
--- /dev/null
+++ b/docs/wiki_src/introduction/setup.md
@@ -0,0 +1,6 @@
+# Setup
+
+-   unicode keymap
+-   editors
+-   syntax highlighting
+-   broogle
diff --git a/docs/wiki_src/introduction/syntax.md b/docs/wiki_src/introduction/syntax.md
new file mode 100644
index 0000000..55e2c21
--- /dev/null
+++ b/docs/wiki_src/introduction/syntax.md
@@ -0,0 +1,148 @@
+# Syntax
+
+Bruijn has an arguably weird syntax, although it's not strictly meant as
+an esoteric programming language. Most notably the usage of lambda
+calculus logic, combinators, and De Bruijn indices can be confusing at
+first -- it's definitely possible to get used to them though!
+
+Bruijn uses a [variation of lambda calculus](lambda-calculus.md).
+
+## Definitions
+
+Bruijn works by defining named substitution rules, where each usage of
+the identifier will get substituted respectively.
+
+Since there's no other major syntactic block, bruijn omits the equal
+symbol for definitions.
+
+For example:
+
+``` bruijn
+# define `id` as [0]
+id [0]
+
+# [0] [0] ⤳ [0]
+still-id id id
+
+# `main` is now [0]
+main still-id
+```
+
+Note that this does *not* actually extend the functionality of lambda
+calculus. These identifiers are static constants and can't be
+dynamically changed.
+
+In fact, bruijn's interpreter works by producing *one* final huge lambda
+calculus expression for any given program, that then gets reduced by a
+normal lambda calculus reducer.
+
+## Open terms
+
+If you use De Bruijn indices that reach out of their environment, you
+have created an *open term*. Depending on the context, these terms are
+typically seen as invalid if standing by themself.
+
+``` bruijn
+# open terms
+open0 0
+open1 [[2]]
+open2 [[0 1] 1]
+
+# closed terms
+closed0 [0 [1]]
+closed1 [[[2 0] 1]]
+```
+
+Bruijn does not give warnings for open terms and reduces them as normal.
+In some cases it's actually encouraged to use open terms as sub-terms
+for better readability (see [coding style
+suggestions](../coding/style.md)).
+
+## Imports
+
+Files can either be imported into a namespace (capital word) or the
+current environment (.):
+
+``` bruijn
+:import std/Pair P
+:import std/Logic .
+
+main [P.pair true false]
+```
+
+All paths get the `.bruijn` extension appended automatically.
+
+Only top-level definitions get imported using `:import`{.bruijn}. If you
+also want to import second-level definitions (for example imported
+definitions from the imported file), you can use `:input`{.bruijn}.
+
+``` bruijn
+:input std/Math
+```
+
+## Tests
+
+Tests compare the *normal form* of two expressions. Note that the
+parentheses around the two terms are always mandatory.
+
+``` bruijn
+:test ([0] [[1]]) ([[1]] [[1]] [0])
+```
+
+Execution succeeds silently. Example of failing test:
+
+``` bruijn
+:test ([0] [[1]]) ([[1]] [0])
+```
+
+After running:
+
+    ERROR test failed: ([0] [[1]]) = ([[1]] [0])
+          reduced to [[1]] = [[0]]
+
+Tests are always run for the executed file and any files it contains. If
+they take too long, you can enable the *YOLO* mode by using bruijn's
+`-y` argument.
+
+## Scoping
+
+Indented lines (by tab) act as a `where` statement for the less indented
+lines.
+
+``` bruijn
+foo [[0]]
+
+bar [0] foo
+    foo bar
+        bar [[1]]
+
+# foo is still `[[0]]`
+# bar is `[0] [[1]]`
+main [[0 foo bar]]
+```
+
+Also note that bruijn does *not* support recursion -- you wouldn't be
+able to use `bar`{.bruijn} in `foo`{.bruijn} without its sub definition.
+See [recursion](../coding/recursion.md) to learn how to use recursion
+anyway.
+
+## Syntactic sugar
+
+Some typical data encodings are provided as syntactic sugar. You can
+learn more about the internal specifics in [data
+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)`
+-   *Characters*: `'C'`{.bruijn} where `C` is any ASCII character
+-   *Strings*: `"X1..XN"`{.bruijn} where `X1...XN` are any ASCII
+    characters
+-   *Quotes*: `` `T ``{.briujn} where `T` is any lambda term ([meta
+    programming](../coding/meta-programming.md))
+
+## Types
+
+TODO.