9472245 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

inital changes following comments, more to come

commit9472245345f67e2b7184ee364374d40e03a9658e authorMartin Baker <git87465@martinb.com> dateWed 15 May 2019, 11:13 (7 years ago) parent1772239

2 files changed+19−11

compare with master

unifiedsplit

docs/proofs/elabReflection.rst+5−5 docs/proofs/tactics.rst+14−6

docs/proofs/elabReflection.rst+5−5

@@ -3,7 +3,7 @@ Extending Idris using Elaborator Reflection

44Idris provides a mechanism to modify the language without having to recompile Idris itself. We can think of this in terms of metaprogramming or domain specific languages or just building in new capabilities.

6−In order to extend the language we need to know something about how Idris is complied. On this page we try to limit this explanation to only what we need to customise the elaboration. For more details of the compiler see `Edwin Brady 2013 paper`_ and for customising the elaboration process see `David Christiansen Practical Reflection and Metaprogramming`_ and `Elaborator reflection: extending Idris in Idris`_. For more information about holes and guesses see `Dependently Typed Functional Programs and their Proofs McBride 1999`_.

6+In order to extend the language we need to know something about how Idris is complied. This page explains only what is needed to customise the elaboration. For more information about the compiler's implementation see `Edwin Brady's 2013 paper`_ and for customising the elaboration process see `Elaborator reflection: extending Idris in Idris`_ and `David Christiansen's PhD thesis`_ .

88Here is a diagram of the multistage process at the top level when Idris code gets compiled:

@@ -11,7 +11,7 @@ Here is a diagram of the multistage process at the top level when Idris code get

1111 :width: 484px

1212 :height: 147px

1313

14−TT is a core language which is syntactically very simple, this makes it easy for computers to process but very verbose and hard for humans to read. This elaboration is done by a logic language (proof tactics) similar to LTac in Coq. Here we use the word 'tactics' to refer to these elaboration tactics - not to be confused with the old tactics mechanism.

14+TT is a core language which is syntactically very simple, this makes it easy for computers to process but very verbose and hard for humans to read. This elaboration is done by a logic language (proof tactics) similar to LTac in Coq. Here the word 'tactics' is used to refer to these elaboration tactics - not to be confused with the old tactics mechanism.

1515

1616.. image:: ../image/compareToProofAssist.png

1717 :width: 229px

@@ -46,10 +46,10 @@ As already mentioned the TT core language is kept syntactically very simple. Par

4646 :height: 145px

4747

4848.. target-notes::

49−.. _`Edwin Brady 2013 paper`: https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf

50−.. _`David Christiansen Practical Reflection and Metaprogramming`: https://davidchristiansen.dk/david-christiansen-phd.pdf

49+.. _`Edwin Brady's 2013 paper`: https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf

50+.. _`David Christiansen's PhD thesis`: https://davidchristiansen.dk/david-christiansen-phd.pdf

5151.. _`Elaborator reflection: extending Idris in Idris`: https://dl.acm.org/citation.cfm?doid=2951913.2951932

52−.. _`Dependently Typed Functional Programs and their Proofs McBride 1999`: https://www.era.lib.ed.ac.uk/handle/1842/374

52+

5353

5454

5555

docs/proofs/tactics.rst+14−6

@@ -3,7 +3,12 @@ Elaborator Reflection - Tactics

44The Idris part of the code for elaborator reflection is in

55Elab.idr `<https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Language/Reflection/Elab.idr>`_

6−Before we look at the Elab monad we need to know how to construct terms.

6+Before looking at the Elab monad we need to know how to construct terms.

8+Holes

9+=====

10+

11+For more information about holes and guesses see `Dependently Typed Functional Programs and their Proofs McBride 1999`_.

712

813Proof State

914===========

@@ -24,7 +29,7 @@ There are many other pieces of information in the proof state such as the names

2429Names TTName

2530------------

2631

27−Names in an Idris program are evaluated at runtime but sometimes we need a 'variable name' which can be referred to as an unevaluated symbol.

32+Names in an Idris program are evaluated at runtime but sometimes a 'variable name' is needed, which can be referred to as an unevaluated symbol.

2833The names used in terms have different constructors depending on their type:

2934

3035+---------------------------+-----------------------------------------------+

@@ -120,7 +125,7 @@ Since names are used frequently in elaborator reflection there is a shortcut for

120125 P Ref (UN "a") (TConst (AType (ATInt ITBig))) : TT

121126

122127

123− * - If we want the vale we can escape from quasiquotation by using anti-quotation (tilde)

128+ * - If we want the value we can escape from quasiquotation by using anti-quotation (tilde)

124129 - example

125130

126131 .. code-block:: idris

@@ -151,7 +156,7 @@ quasiquotation summary:

151156TT

152157==

153158

154−There is a notation for a term in TT as it is being constructed (based on a BNF-like grammar), this is used for example in the debug output, it is a compact way to see the state of the term so we use it here.

159+There is a notation for a term in TT as it is being constructed (based on a BNF-like grammar), this is used for example in the debug output, it is a compact way to see the state of the term so it is used here.

155160So internally the program is stored as a tree structure using the following syntax:

156161

157162+------------+-------+-------------+---------------------------------------------+

@@ -169,8 +174,9 @@ So internally the program is stored as a tree structure using the following synt

170175+------------+-------+-------------+---------------------------------------------+

171176| application| t ::= | t t | As with Idris, juxtaposition indicates |

172−| | | | function application. Note: we use the same |

173−| | | | symbol 't' for terms |

177+| | | | function application. Note: the same symbol |

178+| | | | 't' is used for both terms, this does not |

179+| | | | imply they are the same term. |

174180+------------+-------+-------------+---------------------------------------------+

175181| Type | t ::= | T | |

176182| constructor| | | |

@@ -429,3 +435,5 @@ However this would cause the application of f to be ill-typed, as it expects an

429435

430436 letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()

431437

438+... target-notes::

439+. _`Dependently Typed Functional Programs and their Proofs McBride 1999`: https://www.era.lib.ed.ac.uk/handle/1842/374