@@ -10,8 +10,8 @@ free to contribute.
1010This document assumes that you are already familiar with Idris. It is
1111intended for those who want to work on the internals.
1212
13−People looking to develop new back ends may want to look at [[Idris back
14−end IRs\|Idris-back-end-IRs]]
13+People looking to develop new back ends may want to look at
14+:ref:`code-generation-targets`
1515
1616Core/TT.hs
1717==========
@@ -53,7 +53,7 @@ with ``SC`` and ``CaseAlt`` to get GHC to generate a function for
5353mapping over contained terms.
5454
5555Constructor cases (``ConCase`` in ``CaseAlt``) refer to numbered
56−constructors. Every constructor is numbered 0,1,2,…. At this stage in
56+constructors. Every constructor is numbered *0,1,2,…*. At this stage in
5757the compiler, the tags are datatype-local. After defunctionalization,
5858however, they are made globally unique.
5959
@@ -91,12 +91,12 @@ dictionary which makes totality checking easier.
9191The ``normalise*`` functions give different behaviors - but
9292``normalise`` is the most common.
9393
94−``normaliseC`` - "resolved" means with names converted to de Bruijn
95−indices as appropriate.
94+- ``normaliseC`` - "resolved" means with names converted to de Bruijn
95+ indices as appropriate;
9696
97−``normaliseAll`` - reduce everything, even if it's non-total
97+- ``normaliseAll`` - reduce everything, even if it's non-total;
9898
99−``normaliseTrace`` - special-purpose for debugging
99+- ``normaliseTrace`` - special-purpose for debugging.
100100
101101``simplify`` - reduce the things that are small - the list argument is
102102the things to not reduce.
@@ -110,8 +110,8 @@ Core/Elaborate.hs
110110=================
111111
112112Idris definitions are elaborated one by one and turned into the
113−corresponding TT. This is done with a tactic language as an EDSL in the
114−Elab monad (or Elab' when there's a custom state).
113+corresponding ``TT``. This is done with a tactic language as an EDSL in the
114+``Elab`` monad (or ``Elab'`` when there's a custom state).
115115
116116Lots of plumbing for errors.
117117
@@ -122,17 +122,17 @@ The string in the pair returned by elaborate is log information.
122122See JFP paper, but the names don't necessarily map to each other. The
123123paper is the "idealized version" without logging, additional state, etc.
124124
125−All the tactics take Raws, typechecking happens there.
125+All the tactics take ``Raw`` s, typechecking happens there.
126126
127−claim (x : t) assumes a new x : t.
127+``claim (x : t)`` assumes a new ``x : t``.
128128
129129PLEASE TIDY THINGS UP!
130130
131−proofSearch flag to try' is whether the failure came from a human (so
131+``proofSearch`` flag is to try whether the failure came from a human (so
132132fail) or from a machine (so continue)
133133
134−Idris-level syntax for providing alternatives explicitly: (\| x, y, z
135−\|) try x, y, z in order, and take the first that succeeds.
134+Idris-level syntax for providing alternatives explicitly: ``(| x, y, z
135+|)`` try ``x``, ``y``, ``z`` in order, and take the first that succeeds.
136136
137137Core/ProofState.hs
138138==================
@@ -140,37 +140,40 @@ Core/ProofState.hs
140140Core/Unify.hs
141141=============
142142
143−Deals with unification. Unification can reply with: - this works - this
144−can never work - this will work if these other unification problems work
145−out (eg unifying f x with 1)
143+Deals with unification. Unification can reply with:
146144
147−match\_unify: same thing as unification except it's just matching name
148−against name, term against term. x + y matches to 0 + y with x = 0. Used
149−for <== syntax as well as type class resolution.
145+- this works
146+- this can never work
147+- this will work if these other unification problems work out (e.g.
148+ unifying ``f x`` with ``1``)
149+
150+``match_unify``: same thing as unification except it's just matching name
151+against name, term against term. ``x + y`` matches to ``0 + y`` with
152+``x = 0``. Used for ``<==`` syntax as well as type class resolution.
150153
151154Idris/AbsSyntaxTree.hs
152155======================
153156
154−PTerm is the datatype of Idris syntax. P is for Program. Each PTerm
155−turns into a TT term by applying a series of tactics.
157+``PTerm`` is the datatype of Idris syntax. ``P`` is for *Program*.
158+Each ``PTerm`` turns into a TT term by applying a series of tactics.
156159
157−IState is the major interpreter state. The global context is the
158−tt\_ctxt field.
160+``IState`` is the major interpreter state. The global context is the
161+``tt_ctxt`` field.
159162
160−Ctxt maps possibly ambiguous names to their referents.
163+``Ctxt`` maps possibly ambiguous names to their referents.
161164
162165Idris/ElabDecls.hs
163166==================
164167
165−This is where the actual elaboration from PTerm to TT happens.
168+This is where the actual elaboration from ``PTerm`` to ``TT`` happens.
166169
167170Idris/ElabTerm.hs
168171=================
169172
170−build is the function that creates a Raw. All the "junk" is to deal with
173+``build`` is the function that creates a ``Raw``. All the "junk" is to deal with
171174things like metavars and so forth. It has to remember what names are
172175still to be defined, and it doesn't yet know the type (filled in by
173176unificaiton later). Also case expressions have to turn into top-level
174177functions.
175178
176−resolveTC is type class resolution.
179+``resolveTC`` is type class resolution.