[ fix #472 ] Port doc about comments from Idris1

docs/source/reference/documenting.rst

@@ -0,0 +1,131 @@
+.. _sect-documenting:
+
+**********************
+Documenting Idris Code
+**********************
+
+Idris documentation comes in two major forms: comments, which exist
+for a reader’s edification and are ignored by the compiler, and inline
+API documentation, which the compiler parses and stores for future
+reference. To consult the documentation for a declaration ``f``, write
+``:doc f`` at the REPL or use the appropriate command in your editor
+(``C-c C-d`` in Emacs, ``<LocalLeader>h`` in Vim).
+
+Comments
+========
+
+Use comments to explain why code is written the way that it
+is. Idris’s comment syntax is the same as that of Haskell: lines
+beginning with ``--`` are comments, and regions bracketed by ``{-``
+and ``-}`` are comments even if they extend across multiple
+lines. These can be used to comment out lines of code or provide
+simple documentation for the readers of Idris code.
+
+Inline Documentation
+====================
+
+Idris also supports a comprehensive and rich inline syntax for Idris
+code to be generated. This syntax also allows for named parameters and
+variables within type signatures to be individually annotated using a
+syntax similar to Javadoc parameter annotations.
+
+Documentation always comes before the declaration being documented.
+Inline documentation applies to either top-level declarations or to
+constructors. Documentation for specific arguments to constructors, type
+constructors, or functions can be associated with these arguments using
+their names.
+
+The inline documentation for a declaration is an unbroken string of
+lines, each of which begins with ``|||`` (three pipe symbols). The
+first paragraph of the documentation is taken to be an overview, and
+in some contexts, only this overview will be shown. After the
+documentation for the declaration as a whole, it is possible to
+associate documentation with specific named parameters, which can
+either be explicitly name or the results of converting free variables
+to implicit parameters.  Annotations are the same as with Javadoc
+annotations, that is for the named parameter ``(n : T)``, the
+corresponding annotation is ``||| @ n Some description`` that is
+placed before the declaration.
+
+Documentation is written in Markdown, though not all contexts will
+display all possible formatting (for example, images are not displayed
+when viewing documentation in the REPL, and only some terminals render
+italics correctly). A comprehensive set of examples is given below.
+
+.. code-block:: idris
+
+
+    ||| Modules can also be documented.
+    module Docs
+
+    ||| Add some numbers.
+    |||
+    ||| Addition is really great. This paragraph is not part of the overview.
+    ||| Still the same paragraph. 
+    |||
+    ||| You can even provide examples which are inlined in the documentation:
+    ||| ```idris example
+    ||| add 4 5
+    ||| ```
+    ||| 
+    ||| Lists are also nifty:
+    ||| * Really nifty!
+    ||| * Yep!
+    ||| * The name `add` is a **bold** choice
+    ||| @ n is the recursive param
+    ||| @ m is not
+    add : (n, m : Nat) -> Nat
+    add Z     m = m
+    add (S n) m = S (add n m)
+
+
+    ||| Append some vectors
+    ||| @ a the contents of the vectors
+    ||| @ xs the first vector (recursive param)
+    ||| @ ys the second vector (not analysed)
+    appendV : (xs : Vect n a) -> (ys : Vect m a) -> Vect (add n m) a
+    appendV []      ys = ys
+    appendV (x::xs) ys = x :: appendV xs ys
+
+    ||| Here's a simple datatype
+    data Ty =
+      ||| Unit
+      UNIT |
+      ||| Functions
+      ARR Ty Ty
+
+    ||| Points to a place in a typing context
+    data Elem : Vect n Ty -> Ty -> Type where
+      Here : {ts : Vect n Ty} -> Elem (t::ts) t
+      There : {ts : Vect n Ty} -> Elem ts t -> Elem (t'::ts) t
+
+    ||| A more interesting datatype
+    ||| @ n the number of free variables
+    ||| @ ctxt a typing context for the free variables
+    ||| @ ty the type of the term
+    data Term : (ctxt : Vect n Ty) -> (ty : Ty) -> Type where
+
+      ||| The constructor of the unit type
+      ||| More comment
+      ||| @ ctxt the typing context
+      UnitCon : {ctxt : Vect n Ty} -> Term ctxt UNIT
+
+      ||| Function application
+      ||| @ f the function to apply
+      ||| @ x the argument
+      App : {ctxt : Vect n Ty} -> (f : Term ctxt (ARR t1 t2)) -> (x : Term ctxt t1) -> Term ctxt t2
+
+      ||| Lambda
+      ||| @ body the function body
+      Lam : {ctxt : Vect n Ty} -> (body : Term (t1::ctxt) t2) -> Term ctxt (ARR t1 t2)
+
+      ||| Variables
+      ||| @ i de Bruijn index
+      Var : {ctxt : Vect n Ty} -> (i : Elem ctxt t) -> Term ctxt t
+
+    ||| We can document records, including their fields and constructors
+    record Yummy where
+      ||| Make a yummy
+      constructor MkYummy
+      ||| What to eat
+      food : String

docs/source/reference/index.rst

@@ -17,6 +17,7 @@ This is a placeholder, to get set up with readthedocs.
    :maxdepth: 1
 
    packages
+   documenting
    envvars
    records
    literate