1.. _elaborator-reflection:
7The Idris elaborator is responsible for converting high-level Idris code into the core language.
8It is implemented as a kind of embedded tactic language in Haskell, where tactic scripts are written in an *elaboration monad* that provides error handling and a proof state.
9For details, see Edwin Brady's 2013 paper in the Journal of Functional Programming.
11Elaborator reflection makes the elaboration type as well as a selection of its tactics available to Idris code.
12This means that metaprograms written in Idris can have complete control over the elaboration process, generating arbitrary code, and they have access to all of the facilities available in the elaborator, such as higher-order unification, type checking, and emitting auxiliary definitions.
17Elaborator reflection is a new, **experimental** feature. It **will change**. You've been warned.
22The elaborator state contains information about the ongoing elaboration process.
23In particular, it contains a *goal type*, which is to be filled by an under-construction *proof term*.
24The proof term can contain *holes*, each of which has a scope in which it is valid and a type.
25Some holes may additionally contain *guesses*, which can be substituted in the scope of the hole.
26The holes are tracked in a *hole queue*, and one of them is *focused*.
27In addition to the goal type, proof term, and holes, the elaborator state contains a collection of unsolved unification problems that can affect elaboration.
29The elaborator state is not directly available to Idris programs.
30Instead, it is modified through the use of *tactics*, which are operations that affect the elaborator state.
31A tactic that returns a value of type ``a``, potentially modifying the elaborator state, has type ``Elab a``.
32The default tactics are all in the namespace ``Language.Reflection.Elab.Tactics``.
35Running Elaborator Scripts
36==========================
38On their own, tactics have no effect.
39The meta-operation ``%runElab script`` runs ``script`` in the current elaboration context.
40For example, the following script constructs the identity function at type ``Nat``:
45 idNat = %runElab (do intro (Just (UN "x"))
50On the right-hand side, the Idris elaborator has the goal ``Nat -> Nat``.
51When it encounters the ``%runElab`` directive, it fulfills this goal by running the provided script.
52The first tactic, ``intro``, constructs a lambda that binds the name ``x``.
53The name argument is optional because a default name can be taken from the function type.
54Now, the proof term is of the form ``\x : Nat => {hole}``.
55The second tactic, ``fill``, fills this hole with a guess, giving the term ``\x : Nat => {hole≈x}``.
56Finally, the ``solve`` tactic instantiates the guess, giving the result ``\x : Nat => x``.
58Because elaborator scripts are ordinary Idris expressions, it is also possible to use them in multiple contexts.
59Note that there is nothing ``Nat``-specific about the above script.
60We can generate identity functions at any concrete type using the same script:
65 mkId = do intro (Just (UN "x"))
73 idUnit = %runElab mkId
75 idString : String -> String
76 idString = %runElab mkId
79Interactively Building Elab Scripts
80===================================
82To build an ``Elab`` script interactively, use the ``:elab`` command at the REPL.
83It takes the name of a hole as an argument.
84The interface is largely the same as in Idris's interactive prover, except all meta-commands start with colon.
85For example, use ``:qed`` instead of ``qed``, ``:abandon`` instead of ``abandon``, and ``:undo`` instead of ``undo``.
91Some tactics may *fail*.
92For example, ``intro`` will fail if the focused hole does not have a function type, ``solve`` will fail if the current hole does not contain a guess, and ``fill`` will fail if the term to be filled in has the wrong type.
93Scripts can also fail explicitly using the ``fail`` tactic.
95To account for failure, there is an ``Alternative`` instance for ``Elab``.
96The ``<|>`` operator first tries the script to its left.
97If that script fails, any changes that it made to the state are undone and the right argument is executed.
98If the first argument succeeds, then the second argument is not executed.
100Querying the Elaboration State
101==============================
103``Elab`` includes operations to query the elaboration state, allowing scripts to use information about their environment to steer the elaboration process.
104The ordinary Idris bind syntax can be used to propagate this information.
105For example, a tactic that solves the current goal when it is the unit type might look like this:
113 `(() : Type) => do fill `(() : ())
115 otherGoal => fail [ TermPart otherGoal
116 , TextPart "is not trivial"
120The tactic ``compute`` normalises the type of its goal with respect to the current context.
121While not strictly necessary, this allows ``triv`` to be used in contexts where the triviality of the goal is not immediately apparent.
122Then, ``getGoal`` is used, and its result is bound to ``g``.
123Because it returns a pair consisting of the current goal's name and type, we case-split on its second projection.
124If the goal type turns out to have been the unit type, we fill using the unit constructor and solve the goal.
125Otherwise, we fail with an error message informing the user that the current goal is not trivial.
127Additionally, the elaboration state can be dumped into an error message with the ``debug`` tactic.
128A variant, ``debugMessage``, allows arbitrary messages to be included with the state, allowing for a kind of "``printf`` debuggging" of elaboration scripts.
129The message format used by ``debugMessage`` is the same for errors produced by the error reflection mechanism, allowing the re-use of the Idris pretty-printer when rendering messages.
131Changing the Global Context
132===========================
134``Elab`` scripts can modify the global context during execution.
135Just as the Idris elaborator produces auxiliary definitions to implement features such as ``where``-blocks and ``case`` expressions, user elaboration scripts may need to define functions.
136Furthermore, this allows ``Elab`` reflection to be used to implement features such as type class deriving.
137The operations ``declareType``, ``defineFunction``, and ``addInstance`` allow ``Elab`` scripts to modify the global context.
139Using Idris's Features
140======================
142The Idris compiler has a number of ways to automate the construction of terms.
143On its own, the ``Elab`` state and its interactions with the unifier allow implicits to be solved using unification.
144Additional operations use further features of Idris.
145In particular, ``resolveTC`` solves the current goal using type class resolution, ``search`` invokes the proof search mechanism, and ``sourceLocation`` finds the context in the original file at which the elaboration script is invoked.
151The elaboration mechanism can be invoked recursively using the ``runElab`` tactic.
152This tactic takes a goal type and an elaboration script as arguments and runs the script in a fresh lexical environment to create an inhabitant of the provided goal type.
153This is primarily useful for code generation, particularly for generating pattern-matching clauses, where variable scope needs to be one that isn't the present local context.
157While this documentation is still incomplete, elaboration reflection works in Idris today.
158As you wait for the completion of the documentation, the list of built-in tactics can be obtained using the ``:browse`` command in an Idris REPL or the corresponding feature in one of the graphical IDE clients to explore the ``Language.Reflection.Elab.Tactics`` namespace.
159All of the built-in tactics contain documentation strings.
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list