Small documentation updates

docs/app/index.rst

@@ -0,0 +1,50 @@
+.. _proofs-index:
+
+################################
+Structuring Idris 2 Applications
+################################
+
+A tutorial on structuring Idris 2 applications using ``Control.App``.
+
+.. note::
+
+   The documentation for Idris has been published under the Creative
+   Commons CC0 License. As such to the extent possible under law, *The
+   Idris Community* has waived all copyright and related or neighboring
+   rights to Documentation for Idris.
+
+   More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
+
+.. toctree::
+   :maxdepth: 1
+
+Idris applications have ``main : IO ()`` as an entry point.  A type ``IO a`` is
+a description of interactive actions which produce a value of type ``a``. This
+is fine for primitives, but ``IO`` does not support exceptions so we have to be
+explicit about how an operation handles failure. Also, if we do
+want to support exceptions, we also want to explain how exceptions and linearity
+(see Section :ref:`sect-multiplicites`) interact.
+
+In this tutorial, we describe a parameterised type ``App`` and a related 
+parameterised type ``App1``, which together allow us to structure larger
+applications, taking into account both exceptions and linearity. The aims of
+``App`` and ``App1`` are that they should:
+
+* make it possible to express what interactions a function does, in its type,
+  without too much notational overhead.
+* have little or no performance overhead compared to writing in \texttt{IO}.
+* be compatible with other libraries and techniques for describing effects,
+  such as algebraic effects or monad transformers.
+* be sufficiently easy to use and performant that it can be the basis of
+  *all* libraries that make foreign function calls, much as *IO*
+  is in Idris 1 and Haskell
+* be compatible with linear types, meaning that they should express whether a
+  section of code is linear (guaranteed to execute exactly once without
+  throwing an exception) or whether it might throw an exception.
+
+We begin by introducing ``App``, with some small example
+programs, then show how to extend it with exceptions, state, and other
+interfaces.
+
+[To be continued...]
+

docs/index.rst

@@ -25,6 +25,7 @@ and yet to be updated, so use with caution!
    tutorial/index
    updates/updates
    typedd/typedd
+   app/index
    proofs/index
    faq/faq
    reference/index

docs/typedd/typedd.rst

@@ -79,6 +79,8 @@ In ``DataStore.idr`` and ``DataStoreHoles.idr``, add ``import Data.Strings`` and
 ``import System.REPL``. Also in ``DataStore.idr``, the ``schema`` argument to
 ``display`` is required for matching, so change the type to:
 
+.. code-block:: idris
+
     display : {schema : _} -> SchemaType schema -> String
 
 In ``TypeFuns.idr`` add ``import Data.Strings``
@@ -89,6 +91,8 @@ Chapter 7
 ``Abs`` is now a separate interface from ``Neg``. So, change the type of ``eval``
 to include ``Abs`` specifically:
 
+.. code-block:: idris
+
     eval : (Abs num, Neg num, Integral num) => Expr num -> num
 
 Also, take ``abs`` out of the ``Neg`` implementation for ``Expr`` and add an
@@ -158,6 +162,8 @@ In ``Hangman.idr``:
 + ``guesses`` and ``letters`` are implicit arguments to ``game``, but are used by the
   definition, so add them to its type:
 
+.. code-block:: idris
+
     game : {guesses : _} -> {letters : _} ->
            WordState (S guesses) (S letters) -> IO Finished
 
@@ -215,6 +221,8 @@ tests/typedd-book/chapter10/SnocList.idr for the full details.
 Also, in ``snocListHelp``, ``input`` is used at run time so needs to be bound
 in the type:
 
+.. code-block:: idris
+
     snocListHelp : {input : _} ->
                    (snoc : SnocList input) -> (rest : List a) -> SnocList (input +
 
@@ -267,6 +275,8 @@ In ``TestStore.idr``:
 + In ``filterKeys``, there is an error in the ``SNil`` case, which wasn't caught
   because of the type of ``SNil`` above. It should be:
 
+.. code-block:: idris
+
       filterKeys test DataStore.empty | SNil = []
 
 Chapter 11

docs/updates/updates.rst

@@ -261,7 +261,12 @@ It will postpone resolution if a name can't be resolved immediately, but unlike
 Idris 1, it won't attempt significant backtracking
 
 If you get an ambiguous name error, generally the best approach is to
-give the namespace explicitly.
+give the namespace explicitly. You can also rebind names locally:
+
+.. code-block:: idris
+
+    Main> let (::) = Prelude.(::) in [1,2,3]
+    [1, 2, 3]
 
 One difficulty which remains is resolving ambiguous names where one possibility
 is an interface method, and another is a concrete top level function.

libs/base/base.ipkg

@@ -1,6 +1,10 @@
 package base
 
-modules = Control.Monad.Identity,
+modules = Control.App,
+          Control.App.Console,
+          Control.App.FileIO,
+
+          Control.Monad.Identity,
           Control.Monad.State,
           Control.Monad.Trans,
           Control.WellFounded,