@@ -3,25 +3,34 @@ Extending Idris using Elaborator Reflection
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.
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`_ .
6+In order to extend the language we need to know something about how Idris is compiled. 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`_ .
8−Here is a diagram of the multistage process at the top level when Idris code gets compiled:
8+Compilation of Idris proceeds through a number of stages.
10+- First, Idris is desugared by inserting placeholders for terms to be guessed by the compiler and replacing certain syntactic forms, such as do-notation, with the functions that implement them.
11+- Then, this desugared Idris is translated into a much simpler core language, called TT. This translation process is called elaboration.
12+- Finally, TT is type checked a second time to rule out errors, and then compiled into the target language.
10.. image:: ../image/idrisTopLevel.png
14.. image:: ../image/idrisTopLevel.png
11 :width: 484px
15 :width: 484px
12 :height: 147px
16 :height: 147px
17+ :alt: diagram showing these stages of Idris compilation
14TT 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.
19TT 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.
23+ * - There are some similarities with a proof assistant but in Idris the elaborator is an interpreter of Idris source in the elaboration monad, where each syntactic construct of Idris is interpreted as a sequence of tactics.
16−.. image:: ../image/compareToProofAssist.png
24+ - .. image:: ../image/compareToProofAssist.png
17− :width: 229px
25+ :width: 229px
18− :height: 114px
26+ :height: 114px
27+ :alt: diagram comparing elaboration with proof assistant
20−This gives the opportunity to allow the primitives of the elaboration mechanism to be exposed to metaprograms.
29+The primitives in the elaboration library are not just useful for the implementors of Idris itself. They can also be used by authors of extensions to the compiler, using a mechanism known as elaborator reflection.
21During elaboration TT (Raw) structure contains:
30During elaboration TT (Raw) structure contains:
23−- holes - terms yet to be inferred.
32+- holes - placeholders for terms that have not yet been filled in.
24−- guesses - Suppresses β-reduction while precise structure not known.
33+- guesses - similar to let bindings, except with no reduction rule, so that elaboration programs can control the precise shape of terms that are under construction.
26Type checker:
35Type checker:
@@ -31,12 +40,14 @@ Type checker:
31.. image:: ../image/elabOverview.png
40.. image:: ../image/elabOverview.png
32 :width: 268px
41 :width: 268px
33 :height: 219px
42 :height: 219px
35As already mentioned the TT core language is kept syntactically very simple. Part of the reason for this is that its correctness is already well proven using logic. For instance, here are the binders in TT with corresponding code and logic type introduction rules:
45As already mentioned the TT core language is kept syntactically very simple. Part of the reason for this is that its correctness is already well proven using logic. For instance, here are the binders in TT with corresponding code and logic type introduction rules:
37.. image:: ../image/binders.png
47.. image:: ../image/binders.png
38 :width: 310px
48 :width: 310px
39 :height: 203px
49 :height: 203px
41.. list-table::
52.. list-table::
@@ -44,12 +55,12 @@ As already mentioned the TT core language is kept syntactically very simple. Par
44 - .. image:: ../image/elab.png
55 - .. image:: ../image/elab.png
45 :width: 141px
56 :width: 141px
46 :height: 145px
57 :height: 145px
48.. target-notes::
60.. target-notes::
49.. _`Edwin Brady's 2013 paper`: https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf
61.. _`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
51.. _`Elaborator reflection: extending Idris in Idris`: https://dl.acm.org/citation.cfm?doid=2951913.2951932
62.. _`Elaborator reflection: extending Idris in Idris`: https://dl.acm.org/citation.cfm?doid=2951913.2951932
52−
63+.. _`David Christiansen's PhD thesis`: https://davidchristiansen.dk/david-christiansen-phd.pdf