Updates to reference documentation

docs/reference/REPL.rst

@@ -0,0 +1,183 @@
+REPL commands
+=============
+
+The main way of interacting with Disco is through the REPL, *i.e.*
+"Read-Eval-Print Loop".  Disco displays a prompt, *Reads* what you
+type, *Evaluates* it, *Prints* a result, and then *Loops* to do the
+whole thing again.
+
+The prompt looks like this:
+
+::
+
+   Disco>
+
+The main thing you can do is enter :doc:`expressions <expression>`,
+which are evaluated.  However, you can also enter :doc:`definitions
+<definition>` and :doc:`import statements <import>`, as well as use
+various special REPL commands, listed below.  All the special REPL
+commands begin with a colon.
+
+``:{`` / ``:}``
+---------------
+
+You can enter a multi-line input (*e.g.* a whole function definition)
+at the REPL by first entering ``:{``, then entering all the lines you
+want, then typing ``:}`` when you're done.
+
+``:help``
+---------
+
+Show the list of all available commands.
+
+``:load``
+---------
+
+Load a ``.disco`` file.  For example,
+
+::
+
+   Disco> :load example/tree.disco
+   Loading tree.disco...
+   Loaded.
+
+``:reload``
+-----------
+
+Reload the file that was most recently loaded with ``:load``.  This is
+a helpful option if you are editing a ``.disco`` file.  Instead of
+typing out the name of the file again every time you want to test your
+latest changes, you can just type ``:reload``.  In fact, you can even
+abbreviate it to just ``:r``.
+
+``:names``
+----------
+
+Show a list of all the names that are defined, with their types.  This
+is useful, for example, if you have just used ``:load`` to load a file
+and want to see what definitions it contains. For example:
+
+::
+
+   Disco> :load example/tree.disco
+   Loading tree.disco...
+   Loaded.
+   Disco> :names
+   type Tree = Unit + ℕ × Tree × Tree
+   leaf : Tree
+   node : ℕ × Tree × Tree → Tree
+   tree1 : Tree
+   treeFold : r × (ℕ × r × r → r) × Tree → r
+   treeHeight : Tree → ℕ
+   treeSize : Tree → ℕ
+   treeSum : Tree → ℕ
+
+``:doc``
+--------
+
+Show documentation for something. For example:
+
+::
+
+   Disco> :doc +
+   This expression has multiple possible types.  Some examples:
+   ~+~ : ℕ × ℕ → ℕ
+   ~+~ : ℤ × ℤ → ℤ
+   ~+~ : 𝔽 × 𝔽 → 𝔽
+   ~+~ : ℚ × ℚ → ℚ
+   precedence level 7, left associative
+
+   The sum of two numbers, types, or graphs.
+
+   https://disco-lang.readthedocs.io/en/latest/reference/addition.html
+
+``:table``
+----------
+
+The ``:table`` command formats various things as a table.  It can
+format lists, or lists of tuples, or lists of lists:
+
+::
+
+   Disco> :table [1,2,3,4,5]
+   1
+   2
+   3
+   4
+   5
+
+   Disco> :table [(1,1), (2,4), (3,9)]
+   1  1
+   2  4
+   3  9
+
+   Disco> :table [[1,2,3], [4,5,6], [7,8,9]]
+   1  2  3
+   4  5  6
+   7  8  9
+
+It can also display a table of inputs and outputs for any function:
+
+::
+
+   Disco> :table +
+   Disco> :table +
+     0  0  0
+     0  1  1
+     1  0  1
+     0  2  2
+     1  1  2
+     2  0  2
+     0  3  3
+     1  2  3
+     2  1  3
+     3  0  3
+     0  4  4
+     1  3  4
+     2  2  4
+     3  1  4
+     4  0  4
+     0  5  5
+     1  4  5
+     2  3  5
+     3  2  5
+     4  1  5
+     5  0  5
+     0  6  6
+     1  5  6
+     2  4  6
+     3  3  6
+   ...
+
+
+``:defn``
+---------
+
+Show the definition of a name.  For example:
+
+::
+
+   Disco> :load example/tree.disco
+   Disco> :defn treeFold
+   treeFold : r4 × (ℕ × r4 × r4 → r4) × Tree → r4
+   treeFold(x, f, left(■)) = x
+   treeFold(x, f, right(n, l, r)) = f(n, treeFold(x, f, l), treeFold(x, f, r))
+
+``:test``
+---------
+
+Test a proposition, and display the results.  For example:
+
+::
+
+   Disco> :test forall n:N. n > 5
+     - Certainly false: ∀n. n > 5
+       Found counterexample:
+         n = 0
+
+``:print``
+----------
+
+Print a :doc:`string <string>` directly, without double quotes and
+escape sequences.
+

docs/reference/addition.rst

@@ -4,9 +4,8 @@ Addition
 .. note::
 
    This page concerns the ``+`` operator on numbers; for the ``+``
-   operator on :doc:`types <types>`, see :doc:`sum types <sumtype>`; for
-   the ``+`` operator on :doc:`graphs <graphs>`, see :doc:`overlay
-   <overlay>`.
+   operator on :doc:`types <types>`, see :doc:`sum types <sumtype>`;
+   or see the ``+`` (``overlay``) operator on :doc:`graphs <graphs>`.
 
 Values of all :doc:`numeric types <numeric>` can be added using the ``+``
 operator.  For example:

docs/reference/bag.rst

@@ -0,0 +1,132 @@
+Bags
+====
+
+For any :doc:`type <types>` ``T``, ``Bag(T)`` is the type of *finite
+bags* with elements of type ``T``.  A bag is like a :doc:`set` (and
+unlike a :doc:`list`) in that it doesn't care about the order of the
+elements; however, unlike a :doc:`set`, a bag cares *how many copies*
+of each element there are.
+
+* The built-in ``bag`` function can be used to convert other
+  collections (*e.g.* :doc:`sets <set>` or :doc:`lists <list>`) to bags.
+
+    ::
+
+       Disco> bag([])
+       ⟅⟆
+       Disco> bag({1,2,3})
+       ⟅1, 2, 3⟆
+       Disco> bag("hello")
+       ⟅'e', 'h', 'l' # 2, 'o'⟆
+
+* Notice how single elements are simply listed by themselves, but
+  elements occuring more than once are written with a ``#`` followed
+  by a natural number (called the *cardinality*).  You can write bags this way yourself:
+
+    ::
+
+       Disco> ⟅'a' # 2, 'b' # 3⟆
+       ⟅'a' # 2, 'b' # 3⟆
+       Disco> ⟅'a' # 2, 'b' # 1⟆
+       ⟅'a' # 2, 'b'⟆
+       Disco> ⟅'a' # 0, 'b' # 1⟆
+       ⟅'b'⟆
+
+* Of course, entering the ``⟅⟆`` characters can be difficult, so you
+  can also just stick with entering bags via the ``bag`` function.
+
+* One common place where bags show up is in the output of the ``factor``
+  function (from the ``num`` standard library module) for representing
+  the prime factorization of a natural number.  In a prime
+  factorization, the *order* of the prime factors does not matter (since
+  multiplication is commutative), but it matters how many copies there
+  are of each factor.
+
+    ::
+
+       Disco> import num
+       Disco> factor(10)
+       ⟅2, 5⟆
+       Disco> factor(12)
+       ⟅2 # 2, 3⟆
+       Disco> factor(64)
+       ⟅2 # 6⟆
+
+* Just as with :doc:`lists <list>` and :doc:`sets <set>`, an
+  :doc:`ellipsis <ellipsis>` can be used to generate a range of
+  elements in a bag.  For example,
+
+    ::
+
+       Disco> ⟅'a' .. 'e'⟆
+       ⟅'a', 'b', 'c', 'd', 'e'⟆
+       Disco> ⟅1, 3 .. 9⟆
+       ⟅1, 3, 5, 7, 9⟆
+
+* :doc:`Comprehension <comprehension>` notation can also be used,
+  for example:
+
+    ::
+
+       Disco> ⟅ abs(x - 5) | x in ⟅1 .. 10⟆, x^2 > 5 ⟆
+       ⟅0, 1 # 2, 2 # 2, 3, 4, 5⟆
+
+* The order of elements in a bag does not matter, but the number of
+  copies of each element does matter.  Two bags with the same elements
+  in a different order are considered the same, whereas two bags with
+  the same elements but a different number of copies of each are
+  considered different.  For example,
+
+    ::
+
+       Disco> ⟅1,2,3⟆ == ⟅1,3,2⟆
+       T
+       Disco> ⟅1,2,3⟆ == ⟅1,1,2,3⟆
+       F
+
+* To check whether a bag contains a given element at least once, one can
+  use the ``elem`` operator (also written ``∈``):
+
+    ::
+
+       Disco> 2 elem ⟅1,2,3⟆
+       T
+       Disco> 5 elem ⟅1,2,3⟆
+       F
+       Disco> 2 ∈ ⟅1,2,3⟆
+       T
+
+Bags support various operations, including :doc:`size <size>`,
+:doc:`union <collection-ops>`, :doc:`intersection <collection-ops>`,
+:doc:`difference <collection-ops>`, :doc:`subset <collection-ops>`, and :doc:`power set <power>`.
+
+Converting to and from sets
+---------------------------
+
+Converting a bag to a :doc:`set <set>` using the ``set`` function
+simply discards the cardinalities; converting a set to a bag using
+``bag`` results in a bag where every element has cardinality 1.
+
+However, there is another type of conversion, using the built-in
+functions
+
+* ``bagCounts : Bag(a) -> Set(a * N)``
+
+* ``bagFromCounts : Collection(a * N) -> Bag(a)``
+
+The ``bagCounts`` function converts a bag into a set of pairs, where
+each pair has an element from the bag paired with its cardinality.
+For example:
+
+::
+
+   Disco> bagCounts(bag "hello world")
+   {(' ', 1), ('d', 1), ('e', 1), ('h', 1), ('l', 3), ('o', 2), ('r', 1), ('w', 1)}
+
+The ``bagFromCounts`` function takes any collection of (value,
+cardinality) pairs and converts it into a bag.  For example:
+
+::
+
+   Disco> bagFromCounts [('h', 3), ('i', 2), ('!', 7), ('i',3)]
+   ⟅'!' # 7, 'h' # 3, 'i' # 5⟆

docs/reference/bool.rst

@@ -2,8 +2,8 @@ Booleans
 ========
 
 The type of *booleans* is written ``Bool`` or ``Boolean``.  There are
-exactly two values of type ``Boolean``: ``false`` and ``true`` (which
-can also be written ``False`` and ``True``).
+exactly two values of type ``Boolean``: ``F`` and ``T`` (which
+can also be written ``False`` and ``True``, or ``false`` and ``true``).
 
 :doc:`Logical operators <logic-ops>` can be used to manipulate
 ``Boolean`` values, and expressions of type ``Boolean`` can be used as