git.iko.soy/Idris-dev
on 008fb1f help sign in
Idris-dev/docs/reference/elaborator-reflection.rst
197 lines 9.8 kB history raw
1.. _elaborator-reflection:
3*********************
4Elaborator Reflection
5*********************
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.
14The Elaborator State
15====================
17The elaborator state contains information about the ongoing elaboration process.
18In particular, it contains a *goal type*, which is to be filled by an under-construction *proof term*.
19The proof term can contain *holes*, each of which has a scope in which it is valid and a type.
20Some holes may additionally contain *guesses*, which can be substituted in the scope of the hole.
21The holes are tracked in a *hole queue*, and one of them is *focused*.
22In addition to the goal type, proof term, and holes, the elaborator state contains a collection of unsolved unification problems that can affect elaboration.
24The elaborator state is not directly available to Idris programs.
25Instead, it is modified through the use of *tactics*, which are operations that affect the elaborator state.
26A tactic that returns a value of type ``a``, potentially modifying the elaborator state, has type ``Elab a``.
27The default tactics are all in the namespace ``Language.Reflection.Elab.Tactics``.
30Running Elaborator Scripts
31==========================
33On their own, tactics have no effect.
34The meta-operation ``%runElab script`` runs ``script`` in the current elaboration context.
35For example, the following script constructs the identity function at type ``Nat``:
37.. code-block:: idris
39 idNat : Nat -> Nat
40 idNat = %runElab (do intro `{{x}}
41 fill (Var `{{x}})
42 solve)
45On the right-hand side, the Idris elaborator has the goal ``Nat -> Nat``.
46When it encounters the ``%runElab`` directive, it fulfills this goal by running the provided script.
47The first tactic, ``intro``, constructs a lambda that binds the name ``x``.
48The name argument is optional because a default name can be taken from the function type.
49Now, the proof term is of the form ``\x : Nat => {hole}``.
50The second tactic, ``fill``, fills this hole with a guess, giving the term ``\x : Nat => {hole≈x}``.
51Finally, the ``solve`` tactic instantiates the guess, giving the result ``\x : Nat => x``.
53Because elaborator scripts are ordinary Idris expressions, it is also possible to use them in multiple contexts.
54Note that there is nothing ``Nat``-specific about the above script.
55We can generate identity functions at any concrete type using the same script:
57.. code-block:: idris
59 mkId : Elab ()
60 mkId = do intro `{{x}}
61 fill (Var `{{x}})
62 solve
64 idNat : Nat -> Nat
65 idNat = %runElab mkId
67 idUnit : () -> ()
68 idUnit = %runElab mkId
70 idString : String -> String
71 idString = %runElab mkId
74Interactively Building Elab Scripts
75===================================
77You can build an ``Elab`` script interactively at the REPL.
78Use the command ``:metavars``, or ``:m`` for short, to list the available holes.
79Then, issue the ``:elab <hole>`` command at the REPL
80to enter the elaboration shell.
82At the shell, you can enter proof tactics to alter the proof state.
83You can view the system-provided tactics prior to entering the shell
84by issuing the REPL command ``:browse Language.Reflection.Elab.Tactics``.
85When you have discharged all goals, you can complete the proof
86using the ``:qed`` command and receive in return an elaboration script
87that fills the hole.
89The interactive elaboration shell accepts a limited number of commands,
90including a subset of the commands understood by the normal Idris REPL
91as well as some elaboration-specific commands.
93General-purpose commands:
95- ``:eval <EXPR>``, or ``:e <EXPR>`` for short, evaluates the provided expression
96 and prints the result.
98- ``:type <EXPR>``, or ``:t <EXPR>`` for short, prints the provided expression
99 together with its type.
101- ``:search <TYPE>`` searches for definitions having the provided type.
103- ``:doc <NAME>`` searches for definitions with the provided name and prints their
104 documentation.
107Commands for viewing the proof state:
109- ``:state`` displays the current state of the term being constructed. It lists both
110 other goals and the current goal.
112- ``:term`` displays the current proof term as well as its yet-to-be-filled holes.
115Commands for manipulating the proof state:
117- ``:undo`` undoes the effects of the last tactic.
119- ``:abandon`` gives up on proving the current lemma and quits the elaboration shell.
121- ``:qed`` finishes the script and exits the elaboration shell. The shell will only accept
122 this command once it reports, "No more goals." On exit, it will print out the finished
123 elaboration script for you to copy into your program.
126Failure
127=======
129Some tactics may *fail*.
130For 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.
131Scripts can also fail explicitly using the ``fail`` tactic.
133To account for failure, there is an ``Alternative`` implementation for ``Elab``.
134The ``<|>`` operator first tries the script to its left.
135If that script fails, any changes that it made to the state are undone and the right argument is executed.
136If the first argument succeeds, then the second argument is not executed.
138Querying the Elaboration State
139==============================
141``Elab`` includes operations to query the elaboration state, allowing scripts to use information about their environment to steer the elaboration process.
142The ordinary Idris bind syntax can be used to propagate this information.
143For example, a tactic that solves the current goal when it is the unit type might look like this:
145.. code-block:: idris
147 triv : Elab ()
148 triv = do compute
149 g <- getGoal
150 case (snd g) of
151 `(() : Type) => do fill `(() : ())
152 solve
153 otherGoal => fail [ TermPart otherGoal
154 , TextPart "is not trivial"
155 ]
158The tactic ``compute`` normalises the type of its goal with respect to the current context.
159While not strictly necessary, this allows ``triv`` to be used in contexts where the triviality of the goal is not immediately apparent.
160Then, ``getGoal`` is used, and its result is bound to ``g``.
161Because it returns a pair consisting of the current goal's name and type, we case-split on its second projection.
162If the goal type turns out to have been the unit type, we fill using the unit constructor and solve the goal.
163Otherwise, we fail with an error message informing the user that the current goal is not trivial.
165Additionally, the elaboration state can be dumped into an error message with the ``debug`` tactic.
166A variant, ``debugMessage``, allows arbitrary messages to be included with the state, allowing for a kind of "``printf`` debugging" of elaboration scripts.
167The 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.
169Changing the Global Context
170===========================
172``Elab`` scripts can modify the global context during execution.
173Just 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.
174Furthermore, this allows ``Elab`` reflection to be used to implement features such as interface deriving.
175The operations ``declareType``, ``defineFunction``, and ``addImplementation`` allow ``Elab`` scripts to modify the global context.
177Using Idris's Features
178======================
180The Idris compiler has a number of ways to automate the construction of terms.
181On its own, the ``Elab`` state and its interactions with the unifier allow implicits to be solved using unification.
182Additional operations use further features of Idris.
183In particular, ``resolveTC`` solves the current goal using interface resolution, ``search`` invokes the proof search mechanism, and ``sourceLocation`` finds the context in the original file at which the elaboration script is invoked.
186Recursive Elaboration
187=====================
189The elaboration mechanism can be invoked recursively using the ``runElab`` tactic.
190This 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.
191This 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.
193Learn More
194==========
195While this documentation is still incomplete, elaboration reflection works in Idris today.
196As 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.
197All of the built-in tactics contain documentation strings.