Idris 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.
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 [1] and for customising the elaboration process see [2].
Here is a diagram of the multistage process at the top level when Idris code gets compiled:
TT is a core language which is syntactically very simple but 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) like LTac in Coq. Here we use the word 'tactics' to refer to these elaboration tactics - not to be confused with the old tactics mechanism.
This gives the opportunity to allow the primitives of the elaboration mechanism to be exposed to metaprograms.
During elaboration TT (Raw) structure contains:
- holes - terms yet to be inferred.
- guesses - Suppresses β-reduction while precise structure not known.
Type checker:
- include universe levels
- distinguish between global and local bound names.
Is this old tactics:
As 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:
AsPat Code to elaborate pattern variables. |
code |
Clause Code to elaborate clauses. |
code |
Data Code to elaborate data structures. |
code |
Implementation Code to elaborate instances. |
code |
Interface Code to elaborate interfaces. |
code |
Provider Code to elaborate type providers. |
code |
Quasiquote Code to elaborate quasiquotations. |
code |
Record Code to elaborate records. |
code |
Rewrite Code to elaborate rewrite rules. |
code |
RunElab Code to run the elaborator process. |
code |
Term Code to elaborate terms. |
code |
Transform Transformations for elaborate terms. |
code |
Type Code to elaborate types. |
code |
Utils Elaborator utilities. |
code |
Value Code to elaborate values. |
code |
[2] Practical Reflection and Metaprogramming for Dependent Types David Christiansen