Add titles to all bundled Dex libraries and make their renderings minimally presentable.

8 files changed, 41 insertions, 33 deletions

diff --git a/lib/diagram.dx b/lib/diagram.dx
index 5d99a347..09e5ac53 100644
--- a/lib/diagram.dx
+++ b/lib/diagram.dx
@@ -1,4 +1,4 @@
-'# Vector graphics library
+'# Vector Graphics
 
 import png
 
diff --git a/lib/fft.dx b/lib/fft.dx
index e7f37b28..14b9f416 100644
--- a/lib/fft.dx
+++ b/lib/fft.dx
@@ -1,15 +1,13 @@
 '# Fast Fourier Transform
 For arrays whose size is a power of 2, we use a radix-2 algorithm based
-on the [Fhutark demo](https://github.com/diku-dk/fft/blob/master/lib/github.com/diku-dk/fft/stockham-radix-2.fut#L30).
-This demo also uses types to enforce internally that the array sizes are powers of 2.
+on the [Futhark demo](https://github.com/diku-dk/fft/blob/master/lib/github.com/diku-dk/fft/stockham-radix-2.fut#L30).
+That demo also uses types to enforce internally that the array sizes are powers of 2.
 
 'For non-power-of-2 sized arrays, it uses
 [Bluestein's Algorithm](https://en.wikipedia.org/wiki/Chirp_Z-transform),
 which calls the power-of-2 FFT as a subroutine.
 
-
-
-'### Helper functions
+'## Helper functions
 
 def odd_sized_palindrome {a n} (mid:a) (seq:n=>a) : ((n|Unit|n)=>a) =
   -- Turns sequence 12345 into 543212345.
@@ -51,7 +49,7 @@ def power_of_2_fft {log2_n}
   (direction: FTDirection)
   (x: ((Fin log2_n)=>(Fin 2))=>Complex) :
       ((Fin log2_n)=>(Fin 2))=>Complex =
-  -- (Fin n)=>(Fin 2) has 2^n elements, so (Fin log2_n)=>(Fin n) has exactly n.
+  -- (Fin n)=>(Fin 2) has 2^n elements, so (Fin log2_n)=>(Fin 2) has exactly n.
 
   dir_const = case direction of
     ForwardFT -> -pi
diff --git a/lib/linalg.dx b/lib/linalg.dx
index 7487424e..a557bfd6 100644
--- a/lib/linalg.dx
+++ b/lib/linalg.dx
@@ -1,4 +1,4 @@
-'## Linear Algebra
+'# Linear Algebra
 - Cholesky Decomposition
 - LU Decomposition
 - Matrix Inversion
@@ -14,7 +14,7 @@ def first_ix_of {n} [Ix n] (x:n) : n = unsafe_from_ordinal n 0
 def last_ix_of  {n} [Ix n] (x:n) : n = unsafe_from_ordinal n (unsafe_nat_diff (size n) 1)
 def is_last {n} [Ix n] (x:n) : Bool = ((ordinal x) + 1) == size n
 
-'### Triangular matrices
+'## Triangular matrices
 
 def LowerTriMat (n:Type) [Ix n] (v:Type) : Type = (i:n)=>(..i)=>v
 def UpperTriMat (n:Type) [Ix n] (v:Type) : Type = (i:n)=>(i..)=>v
@@ -33,7 +33,7 @@ def lower_tri_diag {n v} (l:LowerTriMat n v) : n=>v =
 def lower_tri_identity {a n} [Ix n, Add a, Mul a] : LowerTriMat n a =
   for i j. select (is_last j) one zero
 
-'### Representing inequalities between indices
+'## Representing inequalities between indices
 
 -- These would be unnecessary if there were syntax for dependent pairs.
 data LowerTriIx n    = MkLowerTriIx    i:n j:(..i)
@@ -41,7 +41,7 @@ data UpperTriIx n    = MkUpperTriIx    i:n j:(i..)
 data LowerTriIxExc n = MkLowerTriIxExc i:n j:(..<i)
 data UpperTriIxExc n = MkUpperTriIxExc i:n j:(i<..)
 
-'### Flipping inequalities between indices
+'## Flipping inequalities between indices
 
 -- TODO: Put these in instances of an Isomorphism interface?
 def transpose_upper_ix {n} [Ix n] (i:n) (j:(i..)) : LowerTriIx n =
@@ -81,7 +81,7 @@ def transpose_lower_to_upper_no_diag {n v}
     (MkLowerTriIxExc j' i') = transpose_upper_ix_exc i j
     lower.j'.i'
 
-'### Type-shifting inequalities between indices
+'## Type-shifting inequalities between indices
 
 instance {m n} [Ix n, Ix m, Subset m n] Subset (LowerTriIx m) (LowerTriIx n)
   inject' = \(MkLowerTriIx i j).
@@ -135,7 +135,7 @@ instance {m n} [Ix n, Ix m, Subset m n] Subset (UpperTriIxExc m) (UpperTriIxExc
         j'' = from_just $ project m j'
         Just $ MkUpperTriIxExc i' $ from_just $ project _ j''
 
-'### Chaining inequalities between indices
+'## Chaining inequalities between indices
 
 def relax_ii {n} {p:n} [Ix n] (i:(p ..)) (j:(.. p)) : LowerTriIx n =
   i' = inject n i
@@ -157,7 +157,7 @@ def relax_ee {n} {p:n} [Ix n] (i:(p<..)) (j:(..<p)) : LowerTriIxExc n =
   j' = inject n j
   MkLowerTriIxExc i' $ from_just $ project _ j'
 
-'### Linalg helpers
+'## Linalg helpers
 
 def skew_symmetric_prod {v n} [VSpace v]
     (lower: (i:n)=>(..<i)=>Float) (y: n=>v) : n=>v =
@@ -191,7 +191,7 @@ def upper_tri_mat {a b h} (ref:Ref h (UpperTriMat a b)) (i:a) (j:(i..)) : Ref h
   d = %indexRef ref i
   d!j
 
-'### Cholesky decomposition
+'## Cholesky decomposition
 
 def chol {n} (x:n=>n=>Float) : LowerTriMat n Float =
   yield_state zero \buf.
@@ -210,7 +210,7 @@ def chol {n} (x:n=>n=>Float) : LowerTriMat n Float =
           b = get $ mat j' (from_just $ project (..j') j')
           mat i j := a / b
 
-'### Permutations
+'## Permutations
 
 -- The sign of the determinant of a permutation is either 1.0 or -1.0
 PermutationSign = Float
@@ -234,7 +234,7 @@ def perm_to_table {n} ((perm, _):Permutation n) : n=>n = perm
 def perm_sign    {n} ((_, sign):Permutation n) : PermutationSign = sign
 
 
-'### LU decomposition functions
+'## LU decomposition functions
 
 def pivotize {n} (a:n=>n=>Float) : Permutation n =
   -- Gives a row permutation that makes Gaussian elimination more stable.
@@ -303,7 +303,7 @@ def lu {n} (a: n=>n=>Float) :
         lower_tri_mat lRef i' (inject _ j') := (a.i'.j - s) / ujj
   (lower, upper, permutation)
 
-'### General linear algebra functions.
+'## General linear algebra functions
 
 def solve {n v} [VSpace v] (a:n=>n=>Float) (b:n=>v) : n=>v =
   -- There's a small speedup possible by exploiting the fact
diff --git a/lib/parser.dx b/lib/parser.dx
index 2525ec0a..77578051 100644
--- a/lib/parser.dx
+++ b/lib/parser.dx
@@ -1,6 +1,8 @@
+'# Parser Combinators
 
+'Basic combinator-based parser in Dex (as opposed of Dex).
 
-'Utilities unrelated to parsing
+'## Utilities unrelated to parsing
 
 def from_ordinal_exc (n:Type) [Ix n] (i:Nat) : {Except} n =
   if (0 <= i) && (i < size n)
@@ -17,7 +19,7 @@ def index_list {a} (l:List a) (i:Nat) : {Except} a =
   (AsList n xs) = l
   xs.(from_ordinal_exc _ i)
 
-'The Parser type
+'## The Parser type
 
 def ParserHandle (h:Type) : Type = (String & Ref h Nat)
 
@@ -34,7 +36,7 @@ def run_parser_partial {a} (s:String) (parser:Parser a) : Maybe a =
     catch $ do
       f (s, pos)
 
-'Primitive combinators
+'## Primitive combinators
 
 def p_char (c:Char) : Parser Unit = MkParser \(s, posRef).
   i = get posRef
@@ -79,7 +81,7 @@ def try {a} (parser:Parser a) : Parser a = MkParser \h.
       throw ()
     Just x -> x
 
-'Derived combinators
+'## Derived combinators
 
 def parse_digit : Parser Int = try $ MkParser \h.
   c = parse h $ parse_any
diff --git a/lib/plot.dx b/lib/plot.dx
index 9e2ec6df..76431ceb 100644
--- a/lib/plot.dx
+++ b/lib/plot.dx
@@ -1,4 +1,4 @@
-'# Plotting library
+'# Plotting
 
 import diagram
 import png
diff --git a/lib/png.dx b/lib/png.dx
index 9f050337..5b27db27 100644
--- a/lib/png.dx
+++ b/lib/png.dx
@@ -1,3 +1,8 @@
+'# PNG Rendering
+
+'This is a wrapper around a foreign PNG encoding function.  The main
+purpose is to be able to render images in Dex notebooks.
+
 '## Base 64 encoder
 
 encoding_table =
diff --git a/lib/set.dx b/lib/set.dx
index 310a93a3..c77d951f 100644
--- a/lib/set.dx
+++ b/lib/set.dx
@@ -1,7 +1,8 @@
-import sort
+'# Sets and Set-Indexed Arrays
 
+import sort
 
-'### Monoidal enforcement of uniqueness in sorted lists
+'## Monoidal enforcement of uniqueness in sorted lists
 
 def last {n a} (xs:n=>a) : Maybe a =
   s = size n
@@ -41,7 +42,7 @@ def remove_duplicates_from_sorted {n a} [Eq a] (xs:n=>a) : List a =
   reduce (AsList 0 []) merge_unique_sorted_lists xlists
 
 
-'### Sets
+'## Sets
 
 data Set a [Ord a] =
   -- Guaranteed to be in sorted order with unique elements,
@@ -78,7 +79,7 @@ def set_intersect {a}
   UnsafeAsSet _ intersection
 
 
-'### Index set for sets of strings
+'## Index set for sets of strings
 
 -- Todo: Make polymorphic in type.  Waiting on a bugfix.
 -- data SetIx a l:(Set a) [Ord a] =
diff --git a/lib/sort.dx b/lib/sort.dx
index 06268e42..e6a7c77b 100644
--- a/lib/sort.dx
+++ b/lib/sort.dx
@@ -1,14 +1,16 @@
-'## Monoidal Merge Sort
-Warning: Very slow for now!!
-Because merging sorted lists is associative, we can expose the
+'# Monoidal Merge Sort
+
+'Warning: Very slow for now!!
+
+'Because merging sorted lists is associative, we can expose the
 parallelism of merge sort to the Dex compiler by making a monoid
-and using reduce or yield_accum.
+and using `reduce` or `yield_accum`.
 However, this approach puts a lot of pressure on the compiler.
 As noted on [StackOverflow](https://stackoverflow.com/questions/21877572/can-you-formulate-the-bubble-sort-as-a-monoid-or-semigroup),
 if the compiler does the reduction one element at a time,
 it's doing bubble / insertion sort with quadratic time cost.
-However, if breaks the list in half recursively, it'll be doing parallel mergesort.
-Currently it'll do the quadratic time version.
+However, if it breaks the list in half recursively, it'll be doing parallel mergesort.
+Currently the Dex compiler will do the quadratic-time version.
 
 def concat_table {a b v} (leftin: a=>v) (rightin: b=>v) : ((a|b)=>v) =
   for idx. case idx of