Collapse Theory/Runtime sections

Soonad · Sep 14, 2019 · 6e1e218 · 6e1e218
1 parent 0abed2d
commit 6e1e218
Show file tree

Hide file tree

Showing 5 changed files with 10 additions and 14 deletions.
diff --git a/docs/source/index.rst b/docs/source/index.rst
@@ -34,19 +34,13 @@ Table of contents
    language/4.Core-Features
    language/5.Datatypes
 
-.. toctree::
-    :maxdepth: 2
-    :numbered:
-    :caption: Runtime
-
-    runtime/Formality-Net
-
 .. toctree::
     :maxdepth: 2
     :numbered:
     :caption: Theory
 
-    theory/TODO
+    theory/Formality-Net
+    theory/Self-Types
 
 .. toctree::
     :maxdepth: 2
@@ -64,4 +58,4 @@ Table of contents
     :caption: Articles
     :numbered:
 
-    tutorials/What-Are-Proofs
+    articles/What-Are-Proofs
diff --git a/docs/source/language/1.Motivation.md b/docs/source/language/1.Motivation.md
@@ -18,6 +18,6 @@ Formality's substitution algorithm is **asymptotically faster** than Haskell's,
 
 Formality's unique approach to termination is conjectured to allow it to have elegant, powerful type-level features that would be otherwise impossible without causing logical inconsistencies. For example, instead of built-in datatypes, we rely on [Self Types](https://www.semanticscholar.org/paper/Self-Types-for-Dependently-Typed-Lambda-Encodings-Fu-Stump/652f673e13b889e0fd7adbd480c2fdf290621f66), which allow us to implement inductive families with native lambdas. As history tells, having elegant foundations often pays back. We've not only managed to port several proofs from other assistants, but found techniques to [emulate Coq's structural recursion](https://github.com/moonad/Formality-Base/commit/b777d806c6fa37f2ce306fbe87b3ed267152b90c), to perform large eliminations, and even an hypothetical encoding of [higher inductive types](https://github.com/moonad/Formality-Base/blob/master/Example.HigherInductiveType.fm); and we've barely began exploring the system.
 
-![](https://github.com/moonad/formality/raw/master/docs/images/inet-simulation.gif)
+![](https://github.com/moonad/formality/raw/master/archive/images/inet-simulation.gif)
 
 *Interaction Net (inet) simulation*
diff --git a/docs/source/runtime/Formality-Net.md → docs/source/theory/Formality-Net.md b/docs/source/runtime/Formality-Net.md → docs/source/theory/Formality-Net.md
@@ -6,7 +6,7 @@ main one, plus a list of "rewrite rules" that are activated whenever two nodes
 are connected by their main ports. Our system includes 6 types of nodes, ERA,
 CON, OP1, OP2, ITE, NUM.
 
-![](https://raw.githubusercontent.com/moonad/Formality/master/docs/images/fm-net-node-types.png)
+![](https://raw.githubusercontent.com/moonad/Formality/master/archive/images/fm-net-node-types.png)
 
 - `CON` has 3 ports and an integer label. It is used to represent lambdas,
   applications, boxes (implicitly) and duplications. Since FM-Core is based on
@@ -37,7 +37,7 @@ In order to perform computations, FM-Net has a set of rewrite rules that are
 triggered whenever two nodes are connected by their main ports. This is an
 extensive list of those rules:
 
-![](https://raw.githubusercontent.com/moonad/Formality/master/docs/images/fm-net-rewrite-rules.png)
+![](https://raw.githubusercontent.com/moonad/Formality/master/archive/images/fm-net-rewrite-rules.png)
 
 Note that, while there are many rules (since we need to know what to do on each
 combination of a node), most of those have the same "shape" (such as OP2-OP2,
@@ -98,7 +98,7 @@ Those rules allow us to add, multiply, divide and so on native numbers.
 The process of compiling FM-Core to FM-Net can be defined by the following
 function `k_b(net)`:
 
-![](https://raw.githubusercontent.com/moonad/Formality/master/docs/images/fm-net-compilation.png)
+![](https://raw.githubusercontent.com/moonad/Formality/master/archive/images/fm-net-compilation.png)
 
 This function recursively walks through a term, creating nodes and "temporary
 variables" (`x_b`) in the process. It also keeps track of the number of boxes it

diff --git a/docs/source/theory/Self-Types.md b/docs/source/theory/Self-Types.md
@@ -0,0 +1,3 @@
+# Self-Types
+
+(TODO)
diff --git a/docs/source/theory/TODO.md b/docs/source/theory/TODO.md