git.iko.soy/Idris-dev
on master help sign in
inital changes following comments, more to come
9472245Martin Baker
docs/proofs/elabReflection.rst+5−5
compare with master
unifiedsplit
@@ -3,7 +3,7 @@ Extending Idris using Elaborator Reflection
3
3
4Idris 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.
4Idris 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.
5
5
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`_ .
7
7
8Here is a diagram of the multistage process at the top level when Idris code gets compiled:
8Here is a diagram of the multistage process at the top level when Idris code gets compiled:
9
9
@@ -11,7 +11,7 @@ Here is a diagram of the multistage process at the top level when Idris code get
11 :width: 484px
11 :width: 484px
12 :height: 147px
12 :height: 147px
13
13
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.
15
15
16.. image:: ../image/compareToProofAssist.png
16.. image:: ../image/compareToProofAssist.png
17 :width: 229px
17 :width: 229px
@@ -46,10 +46,10 @@ As already mentioned the TT core language is kept syntactically very simple. Par
46 :height: 145px
46 :height: 145px
47
47
48.. target-notes::
48.. target-notes::
49−.. _`Edwin Brady 2013 paper`: https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf
49+.. _`Edwin Brady's 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
50+.. _`David Christiansen's PhD thesis`: https://davidchristiansen.dk/david-christiansen-phd.pdf
51.. _`Elaborator reflection: extending Idris in Idris`: https://dl.acm.org/citation.cfm?doid=2951913.2951932
51.. _`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+
53
53
54
54
55
55
docs/proofs/tactics.rst+14−6
@@ -3,7 +3,12 @@ Elaborator Reflection - Tactics
3
3
4The Idris part of the code for elaborator reflection is in
4The Idris part of the code for elaborator reflection is in
5Elab.idr `<https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Language/Reflection/Elab.idr>`_
5Elab.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.
7+
8+Holes
9+=====
10+
11+For more information about holes and guesses see `Dependently Typed Functional Programs and their Proofs McBride 1999`_.
7
12
8Proof State
13Proof State
9===========
14===========
@@ -24,7 +29,7 @@ There are many other pieces of information in the proof state such as the names
24Names TTName
29Names TTName
25------------
30------------
26
31
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.
28The names used in terms have different constructors depending on their type:
33The names used in terms have different constructors depending on their type:
29
34
30+---------------------------+-----------------------------------------------+
35+---------------------------+-----------------------------------------------+
@@ -120,7 +125,7 @@ Since names are used frequently in elaborator reflection there is a shortcut for
120 P Ref (UN "a") (TConst (AType (ATInt ITBig))) : TT
125 P Ref (UN "a") (TConst (AType (ATInt ITBig))) : TT
121
126
122
127
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)
124 - example
129 - example
125
130
126 .. code-block:: idris
131 .. code-block:: idris
@@ -151,7 +156,7 @@ quasiquotation summary:
151TT
156TT
152==
157==
153
158
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.
155So internally the program is stored as a tree structure using the following syntax:
160So internally the program is stored as a tree structure using the following syntax:
156
161
157+------------+-------+-------------+---------------------------------------------+
162+------------+-------+-------------+---------------------------------------------+
@@ -169,8 +174,9 @@ So internally the program is stored as a tree structure using the following synt
169| binding | | | binding. |
174| binding | | | binding. |
170+------------+-------+-------------+---------------------------------------------+
175+------------+-------+-------------+---------------------------------------------+
171| application| t ::= | t t | As with Idris, juxtaposition indicates |
176| application| t ::= | t t | As with Idris, juxtaposition indicates |
172−| | | | function application. Note: we use the same |
177+| | | | function application. Note: the same symbol |
173−| | | | symbol 't' for terms |
178+| | | | 't' is used for both terms, this does not |
179+| | | | imply they are the same term. |
174+------------+-------+-------------+---------------------------------------------+
180+------------+-------+-------------+---------------------------------------------+
175| Type | t ::= | T | |
181| Type | t ::= | T | |
176| constructor| | | |
182| constructor| | | |
@@ -429,3 +435,5 @@ However this would cause the application of f to be ill-typed, as it expects an
429
435
430 letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()
436 letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()
431
437
438+... target-notes::
439+. _`Dependently Typed Functional Programs and their Proofs McBride 1999`: https://www.era.lib.ed.ac.uk/handle/1842/374