@@ -0,0 +1,120 @@
1+*********************
2+Elaborator Reflection
3+*********************
4+
5+The Idris elaborator is responsible for converting high-level Idris code into the core language.
6+It 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.
7+For details, see Edwin Brady's 2013 paper in the Journal of Functional Programming.
8+
9+Elaborator reflection makes the elaboration type as well as a selection of its tactics available to Idris code.
10+This 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.
11+
12+WARNING
13+=======
14+
15+Elaborator reflection is a new, **experimental** feature. It **will change**. You've been warned.
16+
17+The Elaborator State
18+====================
19+
20+The elaborator state contains information about the ongoing elaboration process.
21+In particular, it contains a *goal type*, which is to be filled by an under-construction *proof term*.
22+The proof term can contain *holes*, each of which has a scope in which it is valid and a type.
23+Some holes may additionally contain *guesses*, which can be substituted in the scope of the hole.
24+The holes are tracked in a *hole queue*, and one of them is *focused*.
25+In addition to the goal type, proof term, and holes, the elaborator state contains a collection of unsolved unification problems that can affect elaboration.
26+
27+The elaborator state is not directly available to Idris programs.
28+Instead, it is modified through the use of *tactics*, which are operations that affect the elaborator state.
29+A tactic that returns a value of type ``a``, potentially modifying the elaborator state, has type ``Elab a``.
30+The default tactics are all in the namespace ``Language.Reflection.Elab.Tactics``.
31+
32+
33+Running Elaborator Scripts
34+==========================
35+
36+On their own, tactics have no effect.
37+The meta-operation ``%runElab script`` runs ``script`` in the current elaboration context.
38+For example, the following script constructs the identity function at type ``Nat``:
39+
40+.. code-block:: idris
41+ idNat : Nat -> Nat
42+ idNat = %runElab (do intro (Just (UN "x"))
43+ fill (Var (UN "x"))
44+ solve)
45+
46+On the right-hand side, the Idris elaborator has the goal ``Nat -> Nat``.
47+When it encounters the ``%runElab`` directive, it fulfills this goal by running the provided script.
48+The first tactic, ``intro``, constructs a lambda that binds the name ``x``.
49+The name argument is optional because a default name can be taken from the function type.
50+Now, the proof term is of the form ``\x : Nat => {hole}``.
51+The second tactic, ``fill``, fills this hole with a guess, giving the term ``\x : Nat => {hole≈x}``.
52+Finally, the ``solve`` tactic instantiates the guess, giving the result ``\x : Nat => x``.
53+
54+Because elaborator scripts are ordinary Idris expressions, it is also possible to use them in multiple contexts.
55+Note that there is nothing ``Nat``-specific about the above script.
56+We can generate identity functions at any concrete type using the same script:
57+
58+.. code-block:: idris
59+ mkId : Elab ()
60+ mkId = do intro (Just (UN "x"))
61+ fill (Var (UN "x"))
62+ solve
63+
64+ idNat : Nat -> Nat
65+ idNat = %runElab mkId
66+
67+ idUnit : () -> ()
68+ idUnit = %runElab mkId
69+
70+ idString : String -> String
71+ idString = %runElab mkId
72+
73+
74+Failure
75+=======
76+
77+Some tactics may *fail*.
78+For 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.
79+Scripts can also fail explicitly using the ``fail`` tactic.
80+
81+To account for failure, there is an ``Alternative`` instance for ``Elab``.
82+The ``<|>`` operator first tries the script to its left.
83+If that script fails, any changes that it made to the state are undone and the right argument is executed.
84+If the first argument succeeds, then the second argument is not executed.
85+
86+Querying the Elaboration State
87+==============================
88+
89+``Elab`` includes operations to query the elaboration state, allowing scripts to use information about their environment to steer the elaboration process.
90+The ordinary Idris bind syntax can be used to propagate this information.
91+For example, a tactic that solves the current goal when it is the unit type might look like this:
92+
93+.. code-block:: idris
94+ triv : Elab ()
95+ triv = do compute
96+ g <- getGoal
97+ case (snd g) of
98+ `(() : Type) => do fill `(() : ())
99+ solve
100+ otherGoal => fail [ TermPart otherGoal
101+ , TextPart "is not trivial"
102+ ]
103+
104+The tactic ``compute`` normalises the type of its goal with respect to the current context.
105+While not strictly necessary, this allows ``triv`` to be used in contexts where the triviality of the goal is not immediately apparent.
106+Then, ``getGoal`` is used, and its result is bound to ``g``.
107+Because it returns a pair consisting of the current goal's name and type, we case-split on its second projection.
108+If the goal type turns out to have been the unit type, we fill using the unit constructor and solve the goal.
109+Otherwise, we fail with an error message informing the user that the current goal is not trivial.
110+
111+Additionally, the elaboration state can be dumped into an error message with the ``debug`` tactic.
112+A variant, ``debugMessage``, allows arbitrary strings to be included with the state, allowing for a kind of "``printf`` debuggging" of elaboration scripts.
113+
114+
115+
116+Learn More
117+==========
118+While this documentation is still incomplete, elaboration reflection works in Idris today.
119+As 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.
120+All of the built-in tactics contain documentation strings.