git.iko.soy/Idris-dev
on f572cd0 help sign in
Idris-dev/docs/reference/documenting.rst
132 lines 4.8 kB history raw
1.. _sect-documenting:
3======================
4Documenting Idris Code
5======================
7Idris documentation comes in two major forms: comments, which exist for
8a reader’s edification and are ignored by the compiler, and inline API
9documentation, 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, in Vim).
14Comments
15--------
17Use comments to explain why code is written the way that it is. Idris’s
18comment syntax is the same as that of Haskell: lines beginning with
19``--`` are comments, and regions bracketed by ``{-`` and ``-}`` are
20comments even if they extend across multiple lines. These can be used to
21comment out lines of code or provide simple documentation for the
22readers 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 first
40paragraph of the documentation is taken to be an overview, and in some
41contexts, only this overview will be shown. After the documentation for
42the declaration as a whole, it is possible to associate documetation
43with specific named parameters, which can either be explicitly name or
44the results of converting free variables to implicit parameters.
45Annotations are the same as with Javadoc annotations, that is for the
46named parameter ``(n : T)``, the corresponding annotation is
47``||| @ n Some description`` that is placed before the declaration.
49Documentation is written in Markdown, though not all contexts will
50display all possible formatting (for example, images are not displayed
51when viewing documentation in the REPL, and only some terminals render
52italics correctly). A comprehensive set of examples is given below.
54.. code-block:: idris
56 module Docs
58 ||| Add some numbers.
59 |||
60 ||| Addition is really great. This paragraph is not part of the overview.
61 ||| Still the same paragraph. Lists are also nifty:
62 ||| * Really nifty!
63 ||| * Yep!
64 ||| * The name `add` is a **bold** choice
65 ||| @ n is the recursive param
66 ||| @ m is not
67 add : (n, m : Nat) -> Nat
68 add Z m = m
69 add (S n) m = S (add n m)
72 ||| Append some vectors
73 ||| @ a the contents of the vectors
74 ||| @ xs the first vector (recursive param)
75 ||| @ ys the second vector (not analyzed)
76 appendV : (xs : Vect n a) -> (ys : Vect m a) -> Vect (add n m) a
77 appendV [] ys = ys
78 appendV (x::xs) ys = x :: appendV xs ys
80 ||| Here's a simple datatype
81 data Ty =
82 ||| Unit
83 UNIT |
84 ||| Functions
85 ARR Ty Ty
87 ||| Points to a place in a typing context
88 data Elem : Vect n Ty -> Ty -> Type where
89 Here : {ts : Vect n Ty} -> Elem (t::ts) t
90 There : {ts : Vect n Ty} -> Elem ts t -> Elem (t'::ts) t
92 ||| A more interesting datatype
93 ||| @ n the number of free variables
94 ||| @ ctxt a typing context for the free variables
95 ||| @ ty the type of the term
96 data Term : (ctxt : Vect n Ty) -> (ty : Ty) -> Type where
98 ||| The consructor of the unit type
99 ||| More comment
100 ||| @ ctxt the typing context
101 UnitCon : {ctxt : Vect n Ty} -> Term ctxt UNIT
103 ||| Function application
104 ||| @ f the function to apply
105 ||| @ x the argument
106 App : {ctxt : Vect n Ty} -> (f : Term ctxt (ARR t1 t2)) -> (x : Term ctxt t1) -> Term ctxt t2
108 ||| Lambda
109 ||| @ body the function body
110 Lam : {ctxt : Vect n Ty} -> (body : Term (t1::ctxt) t2) -> Term ctxt (ARR t1 t2)
112 ||| Variables
113 ||| @ i de Bruijn index
114 Var : {ctxt : Vect n Ty} -> (i : Elem ctxt t) -> Term ctxt t
116 ||| A computation that may someday finish
117 codata Partial : Type -> Type where
119 ||| A finished computation
120 ||| @ value the result
121 Now : (value : a) -> Partial a
123 ||| A not-yet-finished computation
124 ||| @ rest the remaining work
125 Later : (rest : Partial a) -> Partial a
127 ||| We can document records just like normal data
128 record Yummy : Type where
130 ||| Make a yummy
131 ||| @ food what to eat
132 MkYummy : (food : String) -> Yummy