vine: docs (#167)

.github/workflows/gh-pages.yml

@@ -0,0 +1,33 @@
+name: Publish GitHub Pages
+
+on:
+  push:
+    branches:
+      - main
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    steps:
+      - uses: actions/checkout@v3
+
+      - name: install mdbook
+        run: curl https://github.com/rust-lang/mdBook/releases/download/v0.4.43/mdbook-v0.4.43-x86_64-unknown-linux-gnu.tar.gz -L | tar -xz
+      - run: mv docs/theme/{prod-,}toc.js.hbs
+      - run: ../mdbook build
+        working-directory: docs
+      - run: find docs/book -iname '*.html' -exec sed -e 's#\.html##g' -e 's#/index#/#g' -i -- {} ';'
+
+      - uses: actions/configure-pages@v3
+      - uses: actions/upload-pages-artifact@v2
+        with:
+          path: "docs/static"
+
+      - id: deployment
+        uses: actions/deploy-pages@v1

README.md

@@ -5,18 +5,23 @@
 
 Vine is an experimental new programming language based on interaction nets.
 
-Vine is still under heavy development; there are many bugs, and many things will change.
-
-See [`vine/examples/`](./vine/examples/) for examples of Vine.
+Vine is a multi-paradigm language, featuring seamless interop between functional
+and imperative patterns. See [`vine/examples/`](./vine/examples/) for examples
+of Vine.
 
 ```sh
 cargo run -r --bin vine run vine/examples/$NAME.vi
 ```
 
-If you're curious to learn more, join the [Vine Discord server](https://discord.gg/bgUPV8KjDv).
+If you're curious to learn more, take a look at the
+[Vine Docs](https://vine.dev/docs/), and join the
+[Vine Discord server](https://discord.gg/bgUPV8KjDv).
+
+(Vine is still under heavy development; many things will change.)
 
 ## Sub-Projects
 
-Vine compiles to [Ivy](./ivy/), a low-level interaction-combinator programming language.
+Vine compiles to [Ivy](./ivy/), a low-level interaction-combinator programming
+language.
 
 Ivy code runs on the [IVM](./ivm/), a performant interaction combinator runtime.

cspell.json

@@ -13,7 +13,9 @@
     "delims",
     "deque",
     "desugared",
+    "dprint",
     "dyntest",
+    "extrinsics",
     "fizzbuzz",
     "freelist",
     "hashbrown",
@@ -25,6 +27,7 @@
     "miri",
     "nilary",
     "nohash",
+    "nats",
     "nonoverlapping",
     "nums",
     "peekable",
@@ -34,9 +37,13 @@
     "repr",
     "rotr",
     "rustyline",
+    "sequentializing",
     "scrutinee",
     "sixel",
     "strs",
+    "structs",
+    "subexpressions",
+    "subpatterns",
     "unpark",
     "vecs",
     "visitee",

docs/.gitignore

@@ -0,0 +1 @@
+book

docs/book.toml

@@ -0,0 +1,7 @@
+[book]
+authors = ["tjjfvi"]
+language = "en"
+multilingual = false
+src = "src"
+title = "The Vine Programming Language"
+create-missing = false

docs/src/README.md

@@ -0,0 +1,22 @@
+<h1 align="center">
+  <img src="https://vine.dev/favicon-1024.png" width="128" height="128" align="center">
+  <p style="text-align: center">The Vine Programming Language</p>
+</h1>
+
+Vine is an experimental new programming language based on interaction nets.
+
+Vine is a multi-paradigm language, featuring seamless interop between functional
+and imperative patterns.
+
+See
+[`vine/examples/`](https://github.com/VineLang/vine/tree/main/vine/examples/)
+for examples of Vine.
+
+```sh
+cargo run -r --bin vine run vine/examples/$NAME.vi
+```
+
+If you're curious to learn more, join the
+[Vine Discord server](https://discord.gg/bgUPV8KjDv).
+
+(Vine is still under heavy development; many things will change.)

docs/src/SUMMARY.md

@@ -0,0 +1,32 @@
+# Summary
+
+[Introduction](./README.md)
+
+- [Getting Started](./starting/index.md)
+  - [Installation](./starting/installation.md)
+  - [Hello, world!](./starting/hello-world.md)
+
+- [Vine Language Features](./features/index.md)
+  - [The Usual](./features/usual.md)
+  - [Modules](./features/modules.md)
+  - [Types](./features/types/index.md)
+    - [Primitive Types](./features/types/primitives.md)
+    - [Standard Types](./features/types/standard.md)
+    - [Structs](./features/types/structs.md)
+    - [Enums](./features/types/enums.md)
+  - [Methods](./features/methods.md)
+  - [IO](./features/io.md)
+  - [Patterns](./features/patterns.md)
+  - [Conditions](./features/conditions.md)
+  - [Values, Spaces, and Places](./features/values-spaces-places.md)
+  - [References](./features/references.md)
+  - [The Inverse](./features/inverse.md)
+
+- [The Vine Compiler](./compiler/index.md)
+  - [Architecture](./compiler/architecture.md)
+  - [Stacked Flow Graphs](./compiler/sfg.md)
+
+- [Ivy and the IVM](./ivy/index.md)
+  - [Ivy's Interaction System](./ivy/interaction-system.md)
+  - [Statistics](./ivy/statistics.md)
+  - [Extrinsics](./ivy/extrinsics.md)

docs/src/compiler/architecture.md

@@ -0,0 +1,37 @@
+# Architecture
+
+The **cli** is the entrypoint to the compiler, and collects all of the
+compilation options. Most notably, it creates a list of *entrypoints*, paths to
+top-level modules (the main module, the standard library, and any third-party
+libraries).
+
+The **loader** then takes this list of entrypoints and queries the file system
+for their contents. It invokes the *parser* (which in turn invokes the *lexer*)
+to parse the file into an *AST*. The loader then finds any files included in
+this AST, and recursively loads them. Once this process is complete, the loader
+returns an AST node representing the entire compilation unit.
+
+The **resolver** then takes the AST and uses it to build a module graph. The
+nodes of the module graph are called *definitions*. Definitions can have
+different kinds of *bindings*, usually represented as AST nodes (taken out of
+the original compilation unit AST). For example, an `fn` item will have a value
+binding, and the parameters and body of the function will be represented as AST
+nodes. The resolver also disambiguates certain AST nodes, e.g. differentiating
+local variables from constants.
+
+The **checker** then passes over the module graph and checks the types and forms
+of all expressions. It also disambiguates AST nodes based on the inferred types
+and forms; e.g. desugaring method calls and inserting explicit coercions.
+
+The **distiller** then takes every value binding and distills the AST into *Vine
+Intermediate Representation*. VIR is much simpler than the AST; compound
+expressions are distilled into sequential, atomic steps, and high-level
+control-flow constructs are distilled into a [*Stacked Flow Graph*](./sfg).
+
+The **normalizer** then transforms the VIR to remove all of the *divergence*.
+
+The **analyzer** then performs various analyses on the VIR, including
+reachability analysis, and dataflow analysis (determining which locals are used
+by which *stages*, and how).
+
+The **emitter** then converts the VIR into a collection of *Ivy nets*.

docs/src/compiler/index.md

@@ -0,0 +1,3 @@
+# The Vine Compiler
+
+An introduction to the internals of the Vine compiler. Here be dragons!

docs/src/compiler/sfg.md

@@ -0,0 +1,64 @@
+# Stacked Flow Graphs
+
+Many compilers use Control Flow Graphs (CFGs) to represent the control flow of a
+function. The Vine compiler uses Stacked Flow Graphs (SFGs), an extension of
+CFGs, a representation that allows for greater parallelization (among other
+benefits).
+
+## Layers, Stages, and Steps
+
+An SFG consists of a forest of *layers*. Each layer is itself analogous to a
+CFG, and consists of several *stages* (analogous to basic blocks in a CFG).
+
+Flow begins in the initial stage of the initial layer. Flow can transfer between
+layers. Once flow exits a layer, flow returns to the previous layer. This is
+analogous to a call stack (hence the "stacked" flow graph).
+
+Each stage contains a series of *steps*. Flow visits each step in a stage
+sequentially.
+
+A step can:
+
+- *invoke* a variable
+- *transfer* to another layer
+- *diverge* to an ancestor layer
+- perform a primitive operation, such as constructing a tuple, or calling a
+  function
+
+After the last step of a stage, if the stage has a *terminator*, flow transfers
+to another stage in the same layer. Otherwise, flow exits the layer.
+
+## Interfaces and Transfers
+
+Every stage has an *interface*. Within a layer, multiple stages may have the
+same interface. Every interface has one or more stages; interfaces with exactly
+one stage are *unconditional*.
+
+A transfers specifies a *target* interface. If there are multiple stages with
+that interface, the transfer must supply a *payload* which will determine which
+stage is transferred to. The interface specifies the type of this payload, and
+how it is used.
+
+For example, a boolean interface has two stages. One stage is associated with a
+payload of `true`; the other with `false`.
+
+## Forestry and Divergence
+
+Recall that layers are structured in a forest; the forest has one or more root
+layers, and every non-root layer has a single parent layer.
+
+When transferring to another layer (i.e. in a transfer step), the target must be
+in either a root layer, or a child of the current layer.
+
+A step can *diverge*, causing flow to immediately exit several layers. A diverge
+step specifies a target ancestor layer, and optionally a stage in that layer.
+Flow exits layers until it reaches the target ancestor layer. If a stage is
+specified, flow transfers to that stage; otherwise, the target layer is exited
+as well.
+
+(Divergence is used to implement features like `return`, `break`, and
+`continue`. In the 'call stack' analogy, divergence is analogous to throwing an
+exception that is caught by a function higher up on the stack.)
+
+In Vine, SFGs are *normalized* before being emitted. Normalization removes all
+divergence by splitting stages at points where flow may diverge.

docs/src/features/conditions.md

@@ -0,0 +1,112 @@
+# Conditions
+
+Conditions are expressions which evaluate to booleans (the `Bool` type).
+
+Conditions include:
+
+- the usual:
+  - boolean literals (`true`, `false`)
+  - short-circuiting logical operators (`&&`, `||`, `!`)
+  - non-short-circuiting ("bitwise") operators (`&`, `|`, `^`)
+  - comparison operators (`==`, `!=`, `<`, `<=`, `>`, `>=`)
+- comparison chains
+- the `is` operator
+- the implication operator (`=>`)
+
+## Comparison Chains
+
+In Vine, you can chain comparison operators.
+
+For example, `a < b < c` is equivalent to `(a < b) & (b < c)`.
+
+More generally, `a() < b() < c()` is equivalent to
+
+```rs
+do {
+  let x = a();
+  let y = b();
+  let z = c();
+  (x < y) & (y < z)
+}
+```
+
+Note that comparison chains do not short-circuit; all of the subexpressions are
+evaluated exactly once.
+
+All of the comparison operators can be chained. As a contrived example, these
+are equivalent:
+
+```rs
+1 == 1 < 2 <= 3 > 0 != 5 // true
+(1 == 1) & (1 < 2) & (2 <= 3) & (3 > 0) & (0 != 5) // true
+```
+
+## The `is` Operator
+
+The `is` operator checks if an expression matches some pattern, and returns a
+boolean.
+
+```rs
+let option = Some(1);
+option is Some(_); // true
+option is None; // false
+```
+
+Any variables bound by the patterns are in scope in subsequent *true-paths*
+including `&&` chains, then-blocks of an `if`, and the body of a `while`.
+
+```rs
+let option = Some(1);
+
+option is Some(value) && value > 0; // true
+
+if option is Some(value) {
+  value; // 1
+} else {
+  // `value` is not bound in this scope
+}
+```
+
+A true-path is broken by negation (`!`) and disjunction (`||`).
+
+```rs
+// invalid:
+!(option is Some(value)) && value > 0
+
+// invalid:
+option is Some(value) || value > 0
+```
+
+## Implication
+
+In logic, the statement "P implies Q" is true if, whenever P is true, Q is also
+true. This is equivalent to "P is false, or Q is true". Vine has an implication
+operator, `=>`, with the same semantics.
+
+```rs
+true => true // true
+true => false // false
+false => true // true
+false => false // true
+```
+
+The implies operator also continues the true-path; variables bound in the
+left-hand side are in scope in the right-hand side:
+
+```rs
+let x = Some(1);
+x is Some(value) => value > 0 // true
+x is Some(value) => value == 0 // false
+
+let y = None;
+y is Some(value) => value > 0 // true
+y is Some(value) => value == 0 // true
+```
+
+A common pattern in other languages is to write
+`value == null || validate(value)` to validate a nullable value. In Vine, this
+is written with the implication operator:
+
+```rs
+value is Some(value) => validate(value)
+```

docs/src/features/index.md

@@ -0,0 +1,4 @@
+# Vine Language Features
+
+An overview of Vine's language features, from [the usual](./usual.md) to
+[the bizarre](./inverse.md).