@@ -0,0 +1,431 @@
1+Elaborator Reflection - Tactics
2+===============================
3+
4+The Idris part of the code for elaborator reflection is in
5+Elab.idr `<https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Language/Reflection/Elab.idr>`_
6+Before we look at the Elab monad we need to know how to construct terms.
7+
8+Proof State
9+===========
10+
11+Tactics operate on the proof state. The proof state contains various pieces of information, at this stage, the important ones for us are:
12+
13+- A hole queue - This contains a list of the names of the holes used in the proof term. The solution to each hole may depend on the other holes.
14+- A goal type - The type of the term that is under construction for the current goal.
15+- A possibly incomplete proof term, which is being calculated and should be the goal type at the end of elaboration.
16+- Context - A collection of open unification problems, representing recoverable failures of unification that may yet unify once more variables are solved.
17+
18+There are many other pieces of information in the proof state such as the names used , such as the bodies of case blocks that need to be elaborated.but, for now, we will leave the system to handle these.
19+
20+.. image:: image/elabProofState.png
21+ :width: 283px
22+ :height: 232px
23+
24+Names TTName
25+------------
26+
27+Names in an Idris program are evaluated at runtime but sometimes we need a 'variable name' which can be referred to as an unevaluated symbol.
28+The names used in terms have different constructors depending on their type:
29+
30++---------------------------+-----------------------------------------------+
31+| UN String | A user-provided name |
32++---------------------------+-----------------------------------------------+
33+| NS (UN "foo") ["B", "A"]) | A name in some namespace |
34++---------------------------+-----------------------------------------------+
35+| MN Int String | Machine-chosen names |
36++---------------------------+-----------------------------------------------+
37+| SN SpecialName | Special names, to make conflicts impossible |
38+| | and language features predictable |
39++---------------------------+-----------------------------------------------+
40+
41+
42+A user defined name can be constructed like this:
43+
44+.. code-block:: idris
45+
46+ Idris> UN "x"
47+ UN "x" : TTName
48+
49+.. code-block:: idris
50+
51+ Idris> NS (UN "x") ["b","a"]
52+ NS (UN "x") ["b", "a"] : TTName
53+
54+.. list-table:: machine-chosen names
55+
56+ * - A machine-chosen name needs to be generated within an Elab monad (see below for details) and is unique within that monad. This produced: {abc_140}{abc_141} so although gensym "abc" was called twice each one had a different integer:
57+ - example of unique names:
58+
59+ .. code-block:: idris
60+
61+ implementation Show TTName where
62+ show (UN s) = "`{{"++s++"}}"
63+ show (NS t a) = "{"++(show t)++
64+ "."++(show a)++"}"
65+ show (MN i s) = "{"++s++"_"++(show i)++"}"
66+ show (SN sn) = "TTName special name"
67+
68+ showGensym : String
69+ showGensym = %runElab (do
70+ debugMessage [TextPart (
71+ show !(gensym "abc") ++
72+ show !(gensym "abc")
73+ )]
74+ )
75+
76+Quasiquotation
77+==============
78+
79+Since names are used frequently in elaborator reflection there is a shortcut for constructing them:
80+
81+.. list-table:: Quasiquotation
82+
83+ * - An unresolved variable "x" is wrapped in backtick and double braces:
84+ - example
85+
86+ .. code-block:: idris
87+
88+ Idris> `{{x}}
89+ UN "x" : TTName
90+
91+
92+ * - Single braces are used for existing variables:
93+ - example
94+
95+ .. code-block:: idris
96+
97+ Idris> `{x}
98+ No such variable x
99+ Idris> :let x=2
100+ Idris> `{x}
101+ UN "x" : TTName
102+
103+
104+ * - brackets are used for an expression:
105+ - example here type is inferable
106+
107+ .. code-block:: idris
108+
109+ Idris> :let a=2
110+ Idris> `(a)
111+ P Ref (UN "a") (TConst (AType (ATInt ITBig))) : TT
112+
113+
114+ * - Expression with explicit type:
115+ - example
116+
117+ .. code-block:: idris
118+
119+ Idris> `(a:Integer)
120+ P Ref (UN "a") (TConst (AType (ATInt ITBig))) : TT
121+
122+
123+ * - If we want the vale we can escape from quasiquotation by using anti-quotation (tilde)
124+ - example
125+
126+ .. code-block:: idris
127+
128+ Idris> `(~a)
129+ 2 : Integer
130+
131+quasiquotation summary:
132+
133++------------+-----------+----------------------------------------------------------+
134+| |Reification| |
135++============+===========+==========================================================+
136+| \`{{n}} | TTName | Use for new names. Unresolved quotation of the name n. |
137++------------+-----------+----------------------------------------------------------+
138+| \`{n} | TTName | Use for existing names. Resolved quotation of the name |
139+| | | n. n is a reference to a unique name in scope. |
140++------------+-----------+----------------------------------------------------------+
141+| \`(e) | | expression e for which a type is inferable. |
142++------------+-----------+----------------------------------------------------------+
143+| \`(e:t) | | expression e with a given type e. |
144++------------+-----------+----------------------------------------------------------+
145+| ~a | | anti-quotation - sub region which can be evaluated rather|
146+| | | than quoted. |
147++------------+-----------+----------------------------------------------------------+
148+|(Var\`{{x}})| Raw | |
149++------------+-----------+----------------------------------------------------------+
150+
151+TT
152+==
153+
154+There is a notation for a term in TT as it is being constructed (based on a BNF-like grammar), this is used for example in the debug output, it is a compact way to see the state of the term so we use it here.
155+So internally the program is stored as a tree structure using the following syntax:
156+
157++------------+-------+-------------+---------------------------------------------+
158+| | | Syntax | More Information |
159++============+=======+=============+=============================================+
160+| term | | t | |
161++------------+-------+-------------+---------------------------------------------+
162+| binding | | b | |
163++------------+-------+-------------+---------------------------------------------+
164+| constant | t ::= | c | |
165++------------+-------+-------------+---------------------------------------------+
166+| variable | t ::= | x | |
167++------------+-------+-------------+---------------------------------------------+
168+| variable | t ::= | b.t | so a dot '.' tells us this is some sort of |
169+| binding | | | binding. |
170++------------+-------+-------------+---------------------------------------------+
171+| application| t ::= | t t | As with Idris, juxtaposition indicates |
172+| | | | function application. Note: we use the same |
173+| | | | symbol 't' for terms |
174++------------+-------+-------------+---------------------------------------------+
175+| Type | t ::= | T | |
176+| constructor| | | |
177++------------+-------+-------------+---------------------------------------------+
178+| Data | t ::= | C | |
179+| constructor| | | |
180++------------+-------+-------------+---------------------------------------------+
181+| function | b::= | λ c:t | colon ':' separates parameters from body of |
182+| | | | binding. |
183++------------+-------+-------------+---------------------------------------------+
184+| let binding| b::= | let\|-> t:t | |
185++------------+-------+-------------+---------------------------------------------+
186+| function | b::= | ∀ x:t | |
187++------------+-------+-------------+---------------------------------------------+
188+| Type | c::= | \*i | The universe hierarchy is usually handled |
189+| universe | | | automatically so we can just use\* for the |
190+| | | | type of types. |
191++------------+-------+-------------+---------------------------------------------+
192+| integer | c:== | i | |
193+| literal | | | |
194++------------+-------+-------------+---------------------------------------------+
195+|integer type| c:== | Integer | |
196++------------+-------+-------------+---------------------------------------------+
197+| string | c:== | s | |
198+| literal | | | |
199++------------+-------+-------------+---------------------------------------------+
200+| string type| c:== | String | |
201++------------+-------+-------------+---------------------------------------------+
202+|focused hole| | ?x : t | Conor McBride 1999 thesis. |
203++------------+-------+-------------+---------------------------------------------+
204+| guess | | ?x ≈ t : t | Conor McBride 1999 thesis. |
205++------------+-------+-------------+---------------------------------------------+
206+
207+Sometimes the part of the term in focus is underlined.
208+
209+Reflection of the well typed core language
210+
211+.. code-block:: idris
212+
213+ data TT =
214+ ||| A reference to some name (P for Parameter)
215+ P NameType TTName TT |
216+ ||| de Bruijn variables
217+ V Int |
218+ ||| Bind a variable
219+ Bind TTName (Binder TT) TT |
220+ ||| Apply one term to another
221+ App TT TT |
222+ ||| Embed a constant
223+ TConst Const |
224+ ||| Erased terms
225+ Erased |
226+ ||| The type of types along (with universe constraints)
227+ TType TTUExp |
228+ ||| Alternative universes for dealing with uniqueness
229+ UType Universe |
230+
231+TT stores local bound variables using De Bruijn index, when working in Idris this does not concern the user because string names are used for variables. Converting bound variables internally to index values means that the same variable name can be used, in different lambda terms, without ambiguity and without the need for α-substitution.
232+De Bruijn index which is a integer where:
233+
234+- 0=inside current (inner) lambda term
235+- 1= next outer lambda term
236+- 2= next outer and so on
237+
238+Raw
239+---
240+Raw is similar to TT except it is used before types are known. The types should be resolved by the type checker.
241+
242+.. code-block:: idris
243+
244+ data Raw =
245+ ||| Variables, global or local
246+ Var TTName |
247+ ||| Bind a variable
248+ RBind TTName (Binder Raw) Raw |
249+ ||| Application
250+ RApp Raw Raw |
251+ ||| The type of types
252+ RType |
253+ ||| Alternative universes for dealing with uniqueness
254+ RUType Universe |
255+ ||| Embed a constant
256+ RConstant Const |
257+
258+Expression Syntax
259+=================
260+
261+There is a way of notating expressions such as those used in the proof state (example: goal type and proof terms) which is reasonably standard in the papers written about this subject.
262+
263+This notation is not entered directly by metaprogrammers but it is seen, for example in debug output. So this notation is explained here because it is useful to be familiar with it.
264+
265+The notation assumes right-associativity, in the absence of brackets, the term to the right binds more tightly than the one on the left.
266+So, for nested lambda terms:
267+
268++---------------+--------+-------------------+
269+| λ a . λ b . f | means | λ a .( λ b . f) |
270++---------------+--------+-------------------+
271+
272+and the same for function application:
273+
274++---------------+--------+-------------------+
275+| f g x | means | f (g x) |
276++---------------+--------+-------------------+
277+
278+In contrast, in lambda calculus, function application is usually regarded as left-associative,
279+Here are some typical examples of the notation used for expressions:
280+
281++-----------------------+
282+| ? {hole_0} . {hole_0} |
283++-----------------------+
284+
285+The term, to be derived, may start off in this state following something like this:
286+
287+.. code-block:: idris
288+
289+ myScript : Elab ()
290+ myScript= do
291+
292+The dot '.' tells us this is some sort of binding.
293+
294++----------------------------------------------+
295+| ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0} |
296++----------------------------------------------+
297+
298+This is a slightly more complicated example arising from:
299+
300+.. code-block:: idris
301+
302+ idNat : Nat -> Nat
303+ idNat = %runElab (do
304+
305+This introduces a guess that hole_0 = hole_2 .
306+
307++----------------------------------------------------+
308+| ?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0} |
309++----------------------------------------------------+
310+
311+Following on from the previous example a lambda function is introduced like this:
312+
313+.. code-block:: idris
314+
315+ intro `{{x}}
316+
317+So now the expression is wrapped in a lambda binding.
318+
319++-------------------------------------------------------+
320+| ?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0} |
321++-------------------------------------------------------+
322+
323+Following on, we can use the fill tactic like this:
324+
325+.. code-block:: idris
326+
327+ fill (Var `{{x}})
328+
329+which introduces another guess.
330+
331++--------------------------------+
332+| ?{hole_0} ≈ λ x . x . {hole_0} |
333++--------------------------------+
334+
335+The solve tactic completes the proof
336+
337+Binders
338+=======
339+
340+Here we look at each tactic in turn to see how they affect the proof state.
341+
342+Introduction tactics for binders. The binder types are:
343+
344+- lambda function (intro)
345+- dependent function (forall)
346+- let (letBind)
347+- pattern (patbind)
348+
349+A precondition of these tactics is that the focused hole is of the form:
350+
351++-----------+
352+| ?h : t.h |
353++-----------+
354+
355+that is, that the body of its scope consists directly of a reference to the hole-bound variable. If a hole binder were of the form:
356+
357++--------------------+
358+| ?h : t1 -> t2.f h |
359++--------------------+
360+
361+and a tactic such as
362+
363++------------------+
364+| intro \`{{x}} |
365++------------------+
366+
367+were applied, the result would be the term
368+
369++---------------------------+
370+| ?h : t2 . λ x:t1. f h |
371++---------------------------+
372+
373+However this would cause the application of f to be ill-typed, as it expects an argument of type t1->t2, not an argument of type t2. Additionally, some binding tactics require that t, the type of the hole h, have a specific form, because the binder to be established may have a typing rule associated with it.
374+
375+.. list-table:: Binders
376+ :widths: 10 30
377+ :stub-columns: 1
378+
379+ * - intro
380+ - Introduce a lambda binding around the current hole and focus on the body.
381+
382+ Requires that the hole be in binding form (use 'attack' if it might not be).
383+
384+ @ n the name to use for the argument.
385+
386+ Signature:
387+
388+ intro : (n : TTName) -> Elab ()
389+
390+ Result
391+
392+ λn:t1.?h:[n/x]t2.h
393+
394+ * - intro'
395+ - Introduce a lambda binding around the current hole and focus on the body, using the name provided by the type of the hole.
396+
397+ Requires that the hole be immediately under its binder (use 'attack' if it might not be).
398+
399+ Signature:
400+
401+ intro' : Elab ()
402+
403+ * - forall
404+ - Introduce a dependent function type binding into the current hole, and focus on the body. Requires that the hole be immediately under its binder
405+
406+ (use 'attack' if it might not be).
407+
408+ Signature:
409+
410+ forall : TTName -> Raw -> Elab ()
411+
412+ * - patbind
413+ - Introduce a new pattern binding. Requires that the hole be immediately under its binder (use 'attack' if it might not be).
414+
415+ Signature:
416+
417+ patbind : TTName -> Elab ()
418+
419+ * - letbind
420+ - Introduce a new let binding.
421+
422+ Requires that the hole be immediately under its binder (use 'attack' if it might not be).
423+
424+ - @ n the name to let bind
425+ - @ ty the type of the term to be let-bound
426+ - @ tm the term to be bound
427+
428+ Signature:
429+
430+ letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()
431+