@@ -3,25 +3,34 @@ Extending Idris using Elaborator Reflection
33
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.
55
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`_ .
77
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.
9+
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.
913
1014.. image:: ../image/idrisTopLevel.png
1115 :width: 484px
1216 :height: 147px
17+ :alt: diagram showing these stages of Idris compilation
1318
1419TT 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.
1520
16−.. image:: ../image/compareToProofAssist.png
17− :width: 229px
18− :height: 114px
21+.. list-table::
22+
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.
24+ - .. image:: ../image/compareToProofAssist.png
25+ :width: 229px
26+ :height: 114px
27+ :alt: diagram comparing elaboration with proof assistant
1928
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.
2130During elaboration TT (Raw) structure contains:
2231
23−- holes - terms yet to be inferred.
24−- guesses - Suppresses β-reduction while precise structure not known.
32+- holes - placeholders for terms that have not yet been filled in.
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.
2534
2635Type checker:
2736
@@ -31,12 +40,14 @@ Type checker:
3140.. image:: ../image/elabOverview.png
3241 :width: 268px
3342 :height: 219px
43+ :alt: alternate text
3444
3545As 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:
3646
3747.. image:: ../image/binders.png
3848 :width: 310px
3949 :height: 203px
50+ :alt: alternate text
4051
4152.. list-table::
4253
@@ -44,12 +55,12 @@ As already mentioned the TT core language is kept syntactically very simple. Par
4455 - .. image:: ../image/elab.png
4556 :width: 141px
4657 :height: 145px
58+ :alt: alternate text
4759
4860.. target-notes::
4961.. _`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
5162.. _`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
5364
5465
5566