2f0f04c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Some corrections in the docs/reference were done.

2f0f04cDenis Buzdalov7 years ago

docs/reference/codegen.rst+2

compare with master

unifiedsplit

@@ -1,3 +1,5 @@

1+.. _code-generation-targets:

1************************

3************************

2Code Generation Targets

4Code Generation Targets

3************************

5************************

docs/reference/compilation.rst+15−15

@@ -54,7 +54,7 @@ by setting a verbosity level.

54 Checking, and the individual steps prior to code generation.

57−By default Idris' progress reporting is set to quiet-``-q``, or ``--quiet``.

57+By default Idris' progress reporting is set to quiet: ``-q``, or ``--quiet``.

59Logging Internal Operation

60===========================

@@ -100,32 +100,32 @@ Environment Variables

100Several paths set by default within the Idris compiler can be

101overridden through environment variables. The provided variables are:

102

103−* `IDRIS_CC` Change the `C` compiler used by the `C` backend.

103+* ``IDRIS_CC`` Change the *C compiler* used by the *C backend*.

104−* `IDRIS_CFLAGS` Change the `C` flags passed to the `C` compiler.

104+* ``IDRIS_CFLAGS`` Change the *C flags* passed to the *C compiler*.

105−* `TARGET` Change the target directory i.e. `data dir` where Idris installs files when installing using Cabal/Stack.

105+* ``TARGET`` Change the target directory i.e. *data dir* where Idris installs files when installing using Cabal/Stack.

106−* `IDRIS_LIBRARY_PATH` Change the location of where installed packages are found/installed.

106+* ``IDRIS_LIBRARY_PATH`` Change the location of where installed packages are found/installed.

107−* `IDRIS_DOC_PATH` Change the location of where generated idrisdoc for packages are installed.

107+* ``IDRIS_DOC_PATH`` Change the location of where generated idrisdoc for packages are installed.

108

109.. note::

110

111 In versions of Idris prior to 0.12.3 the environment variables

112− `IDRIS_LIBRARY_PATH` and `TARGET` were both used to affect the

112+ ``IDRIS_LIBRARY_PATH`` and ``TARGET`` were both used to affect the

113 installation of single packages and direct where Idris installed

114 its data. The meaning of these variables has changed, and command

115 line options are preferred when changing where individual packages

116 are installed.

117

118−The CLI option `--ibcsubdir` can be used to direct where generated IBC

118+The CLI option ``--ibcsubdir`` can be used to direct where generated IBC

119files are placed. However, this means Idris will install files in a

120non-standard location separate from the rest of the installed

121−packages. The CLI option `--idrispath <dir>` allows you to add a

121+packages. The CLI option ``--idrispath <dir>`` allows you to add a

122directory to the library search path; this option can be used multiple

123−times and can be shortened to `-i <dir>`. Similary, the `--sourcepath

123+times and can be shortened to ``-i <dir>``. Similary, the ``--sourcepath

124−<dir>` option can be used to add directories to the source search

124+<dir>`` option can be used to add directories to the source search

125−path. There is no shortened version for this option as `-s` is a

125+path. There is no shortened version for this option as ``-s`` is a

126reserved flag.

127

128Further, Idris also supports options to augment the paths used, and

129−pass options to the code generator backend. The option `--cg-opt

129+pass options to the code generator backend. The option ``--cg-opt

130−<ARG>` can be used to pass options to the code generator. The format

130+<ARG>`` can be used to pass options to the code generator. The format

131−of `<ARG>` is dependent on the selected backend.

131+of ``<ARG>`` is dependent on the selected backend.

docs/reference/erasure.rst+1−1

@@ -269,7 +269,7 @@ Usage warnings are quite bad and unhelpful at the moment. We should

269include more information and at least translate argument numbers to

270their names.

271

272−There is no decent documentation yet. This wiki page is the first one.

272+There is no decent documentation yet. This page is the first one.

273

274There is no generally accepted terminology. We switch between

275"dotted", "unused", "erased", "irrelevant", "inaccessible", while each

docs/reference/ffi.rst+7−6

@@ -204,9 +204,10 @@ unable to pass the closed-over values through C. If we want to pass Idris values

204to the callback we have to pass them through C explicitly. Non-primitive Idris

205values can be passed to C via the ``Raw`` type.

206

207−The other big limitation is that it doesn't support IO functions. Use

207+The other big limitation is that it doesn't support ``IO`` functions. Use

208−``unsafePerformIO`` to wrap them (i.e. to make an IO function usable as a callback, change the return type

208+``unsafePerformIO`` to wrap them (i.e. to make an ``IO`` function usable as a

209+callback, change the return type from ``IO r`` to ``r``, and change the ``= do``

209−from IOr to r, and change the = do to = unsafePerformIO $ do).

210+to ``= unsafePerformIO $ do``).

210

211

211There are two special function names:

212There are two special function names:

212``%wrapper`` returns the function pointer that wraps an Idris function. This

213``%wrapper`` returns the function pointer that wraps an Idris function. This

@@ -258,7 +259,7 @@ useful to access constants that are preprocessor definitions (like ``INT_MAX``).

258 main = print !intMax

259 main = print !intMax

259

260

260For more complicated interactions with C (such as reading and setting fields

261For more complicated interactions with C (such as reading and setting fields

261−of a C struct), there is a module CFFI available in the contrib package.

262+of a C ``struct``), there is a module C FFI available in the contrib package.

262

263

263C heap

264C heap

264------

265------

@@ -371,7 +372,7 @@ Usage from C code

371The ``Raw`` type constructor allows you to access or return a runtime

372The ``Raw`` type constructor allows you to access or return a runtime

372representation of the value. For instance, if you want to copy a string

373representation of the value. For instance, if you want to copy a string

373generated from C code into an Idris value, you may want to return a

374generated from C code into an Idris value, you may want to return a

374−``Raw String``instead of a ``String`` and use ``MKSTR`` or ``MKSTRlen`` to

375+``Raw String`` instead of a ``String`` and use ``MKSTR`` or ``MKSTRlen`` to

375copy it over.

376copy it over.

376

377

377.. code-block:: idris

378.. code-block:: idris

@@ -393,7 +394,7 @@ FFI implementation

393------------------

394------------------

394

395

395In order to write bindings to external libraries, the details of how

396In order to write bindings to external libraries, the details of how

396−``foreign`` works are unnecessary --- you simply need to know that

397+``foreign`` works are unnecessary: you simply need to know that

397``foreign`` takes an FFI descriptor, the function name, and its

398``foreign`` takes an FFI descriptor, the function name, and its

398type. It is instructive to look a little deeper, however:

399type. It is instructive to look a little deeper, however:

399

400

docs/reference/internals.rst+31−28

@@ -10,8 +10,8 @@ free to contribute.

10This document assumes that you are already familiar with Idris. It is

11intended for those who want to work on the internals.

13−People looking to develop new back ends may want to look at [[Idris back

13+People looking to develop new back ends may want to look at

14−end IRs\|Idris-back-end-IRs]]

14+:ref:`code-generation-targets`

16Core/TT.hs

17==========

@@ -53,7 +53,7 @@ with ``SC`` and ``CaseAlt`` to get GHC to generate a function for

53mapping over contained terms.

55Constructor 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

57the compiler, the tags are datatype-local. After defunctionalization,

58however, they are made globally unique.

@@ -91,12 +91,12 @@ dictionary which makes totality checking easier.

91The ``normalise*`` functions give different behaviors - but

92``normalise`` is the most common.

94−``normaliseC`` - "resolved" means with names converted to de Bruijn

94+- ``normaliseC`` - "resolved" means with names converted to de Bruijn

95−indices as appropriate.

95+ indices as appropriate;

97−``normaliseAll`` - reduce everything, even if it's non-total

97+- ``normaliseAll`` - reduce everything, even if it's non-total;

99−``normaliseTrace`` - special-purpose for debugging

99+- ``normaliseTrace`` - special-purpose for debugging.

100

101``simplify`` - reduce the things that are small - the list argument is

102the things to not reduce.

@@ -110,8 +110,8 @@ Core/Elaborate.hs

110=================

111

112Idris 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

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).

114+``Elab`` monad (or ``Elab'`` when there's a custom state).

115

116Lots of plumbing for errors.

117

@@ -122,17 +122,17 @@ The string in the pair returned by elaborate is log information.

122See JFP paper, but the names don't necessarily map to each other. The

123paper is the "idealized version" without logging, additional state, etc.

124

125−All the tactics take Raws, typechecking happens there.

125+All the tactics take ``Raw`` s, typechecking happens there.

126

127−claim (x : t) assumes a new x : t.

127+``claim (x : t)`` assumes a new ``x : t``.

128

129PLEASE TIDY THINGS UP!

130

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

132fail) or from a machine (so continue)

133

134−Idris-level syntax for providing alternatives explicitly: (\| x, y, z

134+Idris-level syntax for providing alternatives explicitly: ``(| x, y, z

135−\|) try x, y, z in order, and take the first that succeeds.

135+|)`` try ``x``, ``y``, ``z`` in order, and take the first that succeeds.

136

137Core/ProofState.hs

138==================

@@ -140,37 +140,40 @@ Core/ProofState.hs

140Core/Unify.hs

141=============

142

143−Deals with unification. Unification can reply with: - this works - this

143+Deals with unification. Unification can reply with:

144−can never work - this will work if these other unification problems work

145−out (eg unifying f x with 1)

146

144

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+

147−match\_unify: same thing as unification except it's just matching name

150+``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

151+against name, term against term. ``x + y`` matches to ``0 + y`` with

149−for <== syntax as well as type class resolution.

152+``x = 0``. Used for ``<==`` syntax as well as type class resolution.

150

153

151Idris/AbsSyntaxTree.hs

154Idris/AbsSyntaxTree.hs

152======================

155======================

153

156

154−PTerm is the datatype of Idris syntax. P is for Program. Each PTerm

157+``PTerm`` is the datatype of Idris syntax. ``P`` is for *Program*.

155−turns into a TT term by applying a series of tactics.

158+Each ``PTerm`` turns into a TT term by applying a series of tactics.

156

159

157−IState is the major interpreter state. The global context is the

160+``IState`` is the major interpreter state. The global context is the

158−tt\_ctxt field.

161+``tt_ctxt`` field.

159

162

160−Ctxt maps possibly ambiguous names to their referents.

163+``Ctxt`` maps possibly ambiguous names to their referents.

161

164

162Idris/ElabDecls.hs

165Idris/ElabDecls.hs

163==================

166==================

164

167

165−This is where the actual elaboration from PTerm to TT happens.

168+This is where the actual elaboration from ``PTerm`` to ``TT`` happens.

166

169

167Idris/ElabTerm.hs

170Idris/ElabTerm.hs

168=================

171=================

169

172

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

171things like metavars and so forth. It has to remember what names are

174things like metavars and so forth. It has to remember what names are

172still to be defined, and it doesn't yet know the type (filled in by

175still to be defined, and it doesn't yet know the type (filled in by

173unificaiton later). Also case expressions have to turn into top-level

176unificaiton later). Also case expressions have to turn into top-level

174functions.

177functions.

175

178

176−resolveTC is type class resolution.

179+``resolveTC`` is type class resolution.

docs/reference/uniqueness-types.rst+1−1

@@ -199,7 +199,7 @@ return it in exactly the condition in which it was received!

199The restriction is that when a ``Borrowed`` type is matched, any

200pattern variables under the ``Read`` which have a unique type may not

201be referred to at all on the right hand side (unless they are

202−themselves ``lent`` to another function).

202+themselves lent to another function).

203

204Uniqueness information is stored in the type, and in particular in

205function types. Once we're in a unique context, any new function which