git.iko.soy/Idris-dev
on 2be265d help sign in
Idris-dev/docs/reference/documenting.rst
135 lines 4.9 kB history raw
1.. _sect-documenting:
3**********************
4Documenting Idris Code
5**********************
7Idris documentation comes in two major forms: comments, which exist
8for a reader’s edification and are ignored by the compiler, and inline
9API documentation, which the compiler parses and stores for future
10reference. To consult the documentation for a declaration ``f``, write
11``:doc f`` at the REPL or use the appropriate command in your editor
12(``C-c C-d`` in Emacs, ``<LocalLeader>h`` in Vim).
14Comments
15========
17Use comments to explain why code is written the way that it
18is. Idris’s comment syntax is the same as that of Haskell: lines
19beginning with ``--`` are comments, and regions bracketed by ``{-``
20and ``-}`` are comments even if they extend across multiple
21lines. These can be used to comment out lines of code or provide
22simple documentation for the readers of Idris code.
24Inline Documentation
25====================
27Idris also supports a comprehensive and rich inline syntax for Idris
28code to be generated. This syntax also allows for named parameters and
29variables within type signatures to be individually annotated using a
30syntax similar to Javadoc parameter annotations.
32Documentation always comes before the declaration being documented.
33Inline documentation applies to either top-level declarations or to
34constructors. Documentation for specific arguments to constructors, type
35constructors, or functions can be associated with these arguments using
36their names.
38The inline documentation for a declaration is an unbroken string of
39lines, each of which begins with ``|||`` (three pipe symbols). The
40first paragraph of the documentation is taken to be an overview, and
41in some contexts, only this overview will be shown. After the
42documentation for the declaration as a whole, it is possible to
43associate documentation with specific named parameters, which can
44either be explicitly name or the results of converting free variables
45to implicit parameters. Annotations are the same as with Javadoc
46annotations, that is for the named parameter ``(n : T)``, the
47corresponding annotation is ``||| @ n Some description`` that is
48placed before the declaration.
50Documentation is written in Markdown, though not all contexts will
51display all possible formatting (for example, images are not displayed
52when viewing documentation in the REPL, and only some terminals render
53italics correctly). A comprehensive set of examples is given below.
55.. code-block:: idris
58 ||| Modules can also be documented.
59 module Docs
61 ||| Add some numbers.
62 |||
63 ||| Addition is really great. This paragraph is not part of the overview.
64 ||| Still the same paragraph. Lists are also nifty:
65 ||| * Really nifty!
66 ||| * Yep!
67 ||| * The name `add` is a **bold** choice
68 ||| @ n is the recursive param
69 ||| @ m is not
70 add : (n, m : Nat) -> Nat
71 add Z m = m
72 add (S n) m = S (add n m)
75 ||| Append some vectors
76 ||| @ a the contents of the vectors
77 ||| @ xs the first vector (recursive param)
78 ||| @ ys the second vector (not analysed)
79 appendV : (xs : Vect n a) -> (ys : Vect m a) -> Vect (add n m) a
80 appendV [] ys = ys
81 appendV (x::xs) ys = x :: appendV xs ys
83 ||| Here's a simple datatype
84 data Ty =
85 ||| Unit
86 UNIT |
87 ||| Functions
88 ARR Ty Ty
90 ||| Points to a place in a typing context
91 data Elem : Vect n Ty -> Ty -> Type where
92 Here : {ts : Vect n Ty} -> Elem (t::ts) t
93 There : {ts : Vect n Ty} -> Elem ts t -> Elem (t'::ts) t
95 ||| A more interesting datatype
96 ||| @ n the number of free variables
97 ||| @ ctxt a typing context for the free variables
98 ||| @ ty the type of the term
99 data Term : (ctxt : Vect n Ty) -> (ty : Ty) -> Type where
101 ||| The constructor of the unit type
102 ||| More comment
103 ||| @ ctxt the typing context
104 UnitCon : {ctxt : Vect n Ty} -> Term ctxt UNIT
106 ||| Function application
107 ||| @ f the function to apply
108 ||| @ x the argument
109 App : {ctxt : Vect n Ty} -> (f : Term ctxt (ARR t1 t2)) -> (x : Term ctxt t1) -> Term ctxt t2
111 ||| Lambda
112 ||| @ body the function body
113 Lam : {ctxt : Vect n Ty} -> (body : Term (t1::ctxt) t2) -> Term ctxt (ARR t1 t2)
115 ||| Variables
116 ||| @ i de Bruijn index
117 Var : {ctxt : Vect n Ty} -> (i : Elem ctxt t) -> Term ctxt t
119 ||| A computation that may someday finish
120 codata Partial : Type -> Type where
122 ||| A finished computation
123 ||| @ value the result
124 Now : (value : a) -> Partial a
126 ||| A not-yet-finished computation
127 ||| @ rest the remaining work
128 Later : (rest : Partial a) -> Partial a
130 ||| We can document records, including their fields and constructors
131 record Yummy where
132 ||| Make a yummy
133 constructor MkYummy
134 ||| What to eat
135 food : String