5The Idris elaborator is responsible for converting high-level Idris code into the core language.
6It 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.
7For details, see Edwin Brady's 2013 paper in the Journal of Functional Programming.
9Elaborator reflection makes the elaboration type as well as a selection of its tactics available to Idris code.
10This 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.
15Elaborator reflection is a new, **experimental** feature. It **will change**. You've been warned.
20The elaborator state contains information about the ongoing elaboration process.
21In particular, it contains a *goal type*, which is to be filled by an under-construction *proof term*.
22The proof term can contain *holes*, each of which has a scope in which it is valid and a type.
23Some holes may additionally contain *guesses*, which can be substituted in the scope of the hole.
24The holes are tracked in a *hole queue*, and one of them is *focused*.
25In addition to the goal type, proof term, and holes, the elaborator state contains a collection of unsolved unification problems that can affect elaboration.
27The elaborator state is not directly available to Idris programs.
28Instead, it is modified through the use of *tactics*, which are operations that affect the elaborator state.
29A tactic that returns a value of type ``a``, potentially modifying the elaborator state, has type ``Elab a``.
30The default tactics are all in the namespace ``Language.Reflection.Elab.Tactics``.
33Running Elaborator Scripts
34==========================
36On their own, tactics have no effect.
37The meta-operation ``%runElab script`` runs ``script`` in the current elaboration context.
38For example, the following script constructs the identity function at type ``Nat``:
43 idNat = %runElab (do intro (Just (UN "x"))
48On the right-hand side, the Idris elaborator has the goal ``Nat -> Nat``.
49When it encounters the ``%runElab`` directive, it fulfills this goal by running the provided script.
50The first tactic, ``intro``, constructs a lambda that binds the name ``x``.
51The name argument is optional because a default name can be taken from the function type.
52Now, the proof term is of the form ``\x : Nat => {hole}``.
53The second tactic, ``fill``, fills this hole with a guess, giving the term ``\x : Nat => {hole≈x}``.
54Finally, the ``solve`` tactic instantiates the guess, giving the result ``\x : Nat => x``.
56Because elaborator scripts are ordinary Idris expressions, it is also possible to use them in multiple contexts.
57Note that there is nothing ``Nat``-specific about the above script.
58We can generate identity functions at any concrete type using the same script:
63 mkId = do intro (Just (UN "x"))
71 idUnit = %runElab mkId
73 idString : String -> String
74 idString = %runElab mkId
77Interactively Building Elab Scripts
78===================================
80To build an ``Elab`` script interactively, use the ``:elab`` command at the REPL.
81It takes the name of a hole as an argument.
82The interface is largely the same as in Idris's interactive prover, except all meta-commands start with colon.
83For example, use ``:qed`` instead of ``qed``, ``:abandon`` instead of ``abandon``, and ``:undo`` instead of ``undo``.
89Some tactics may *fail*.
90For 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.
91Scripts can also fail explicitly using the ``fail`` tactic.
93To account for failure, there is an ``Alternative`` instance for ``Elab``.
94The ``<|>`` operator first tries the script to its left.
95If that script fails, any changes that it made to the state are undone and the right argument is executed.
96If the first argument succeeds, then the second argument is not executed.
98Querying the Elaboration State
99==============================
101``Elab`` includes operations to query the elaboration state, allowing scripts to use information about their environment to steer the elaboration process.
102The ordinary Idris bind syntax can be used to propagate this information.
103For example, a tactic that solves the current goal when it is the unit type might look like this:
111 `(() : Type) => do fill `(() : ())
113 otherGoal => fail [ TermPart otherGoal
114 , TextPart "is not trivial"
118The tactic ``compute`` normalises the type of its goal with respect to the current context.
119While not strictly necessary, this allows ``triv`` to be used in contexts where the triviality of the goal is not immediately apparent.
120Then, ``getGoal`` is used, and its result is bound to ``g``.
121Because it returns a pair consisting of the current goal's name and type, we case-split on its second projection.
122If the goal type turns out to have been the unit type, we fill using the unit constructor and solve the goal.
123Otherwise, we fail with an error message informing the user that the current goal is not trivial.
125Additionally, the elaboration state can be dumped into an error message with the ``debug`` tactic.
126A variant, ``debugMessage``, allows arbitrary messages to be included with the state, allowing for a kind of "``printf`` debuggging" of elaboration scripts.
127The 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.
129Changing the Global Context
130===========================
132``Elab`` scripts can modify the global context during execution.
133Just 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.
134Furthermore, this allows ``Elab`` reflection to be used to implement features such as type class deriving.
135The operations ``declareType``, ``defineFunction``, and ``addInstance`` allow ``Elab`` scripts to modify the global context.
137Using Idris's Features
138======================
140The Idris compiler has a number of ways to automate the construction of terms.
141On its own, the ``Elab`` state and its interactions with the unifier allow implicits to be solved using unification.
142Additional operations use further features of Idris.
143In 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.
149The elaboration mechanism can be invoked recursively using the ``runElab`` tactic.
150This tactic takes a goal type and an elaboration script as arguments and runs the script in a fresh lexical evironment to create an inhabitant of the provided goal type.
151This 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.
155While this documentation is still incomplete, elaboration reflection works in Idris today.
156As 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.
157All 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