@@ -0,0 +1,431 @@
1+Elaborator Reflection - Tactics
2+===============================
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.
11+Tactics operate on the proof state. The proof state contains various pieces of information, at this stage, the important ones for us are:
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.
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.
20+.. image:: image/elabProofState.png
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:
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++---------------------------+-----------------------------------------------+
42+A user defined name can be constructed like this:
51+ Idris> NS (UN "x") ["b","a"]
52+ NS (UN "x") ["b", "a"] : TTName
54+.. list-table:: machine-chosen names
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:
59+ .. code-block:: idris
61+ implementation Show TTName where
62+ show (UN s) = "`{{"++s++"}}"
63+ show (NS t a) = "{"++(show t)++
65+ show (MN i s) = "{"++s++"_"++(show i)++"}"
66+ show (SN sn) = "TTName special name"
69+ showGensym = %runElab (do
70+ debugMessage [TextPart (
71+ show !(gensym "abc") ++
79+Since names are used frequently in elaborator reflection there is a shortcut for constructing them:
81+.. list-table:: Quasiquotation
83+ * - An unresolved variable "x" is wrapped in backtick and double braces:
86+ .. code-block:: idris
92+ * - Single braces are used for existing variables:
95+ .. code-block:: idris
104+ * - brackets are used for an expression:
105+ - example here type is inferable
107+ .. code-block:: idris
111+ P Ref (UN "a") (TConst (AType (ATInt ITBig))) : TT
114+ * - Expression with explicit type:
117+ .. code-block:: idris
120+ P Ref (UN "a") (TConst (AType (ATInt ITBig))) : TT
123+ * - If we want the vale we can escape from quasiquotation by using anti-quotation (tilde)
126+ .. code-block:: idris
131+quasiquotation summary:
133++------------+-----------+----------------------------------------------------------+
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|
147++------------+-----------+----------------------------------------------------------+
148+|(Var\`{{x}})| Raw | |
149++------------+-----------+----------------------------------------------------------+
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:
157++------------+-------+-------------+---------------------------------------------+
158+| | | Syntax | More Information |
159++============+=======+=============+=============================================+
161++------------+-------+-------------+---------------------------------------------+
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 | |
177++------------+-------+-------------+---------------------------------------------+
178+| Data | t ::= | C | |
180++------------+-------+-------------+---------------------------------------------+
181+| function | b::= | λ c:t | colon ':' separates parameters from body of |
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 | |
194++------------+-------+-------------+---------------------------------------------+
195+|integer type| c:== | Integer | |
196++------------+-------+-------------+---------------------------------------------+
197+| string | c:== | s | |
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++------------+-------+-------------+---------------------------------------------+
207+Sometimes the part of the term in focus is underlined.
209+Reflection of the well typed core language
211+.. code-block:: idris
214+ ||| A reference to some name (P for Parameter)
215+ P NameType TTName TT |
216+ ||| de Bruijn variables
219+ Bind TTName (Binder TT) TT |
220+ ||| Apply one term to another
222+ ||| Embed a constant
226+ ||| The type of types along (with universe constraints)
228+ ||| Alternative universes for dealing with uniqueness
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:
234+- 0=inside current (inner) lambda term
235+- 1= next outer lambda term
236+- 2= next outer and so on
240+Raw is similar to TT except it is used before types are known. The types should be resolved by the type checker.
242+.. code-block:: idris
245+ ||| Variables, global or local
248+ RBind TTName (Binder Raw) Raw |
251+ ||| The type of types
253+ ||| Alternative universes for dealing with uniqueness
255+ ||| Embed a constant
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.
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.
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:
268++---------------+--------+-------------------+
269+| λ a . λ b . f | means | λ a .( λ b . f) |
270++---------------+--------+-------------------+
272+and the same for function application:
274++---------------+--------+-------------------+
275+| f g x | means | f (g x) |
276++---------------+--------+-------------------+
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:
281++-----------------------+
282+| ? {hole_0} . {hole_0} |
283++-----------------------+
285+The term, to be derived, may start off in this state following something like this:
287+.. code-block:: idris
292+The dot '.' tells us this is some sort of binding.
294++----------------------------------------------+
295+| ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0} |
296++----------------------------------------------+
298+This is a slightly more complicated example arising from:
300+.. code-block:: idris
303+ idNat = %runElab (do
305+This introduces a guess that hole_0 = hole_2 .
307++----------------------------------------------------+
308+| ?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0} |
309++----------------------------------------------------+
311+Following on from the previous example a lambda function is introduced like this:
313+.. code-block:: idris
317+So now the expression is wrapped in a lambda binding.
319++-------------------------------------------------------+
320+| ?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0} |
321++-------------------------------------------------------+
323+Following on, we can use the fill tactic like this:
325+.. code-block:: idris
329+which introduces another guess.
331++--------------------------------+
332+| ?{hole_0} ≈ λ x . x . {hole_0} |
333++--------------------------------+
335+The solve tactic completes the proof
340+Here we look at each tactic in turn to see how they affect the proof state.
342+Introduction tactics for binders. The binder types are:
344+- lambda function (intro)
345+- dependent function (forall)
349+A precondition of these tactics is that the focused hole is of the form:
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:
357++--------------------+
358+| ?h : t1 -> t2.f h |
359++--------------------+
367+were applied, the result would be the term
369++---------------------------+
370+| ?h : t2 . λ x:t1. f h |
371++---------------------------+
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.
375+.. list-table:: Binders
380+ - Introduce a lambda binding around the current hole and focus on the body.
382+ Requires that the hole be in binding form (use 'attack' if it might not be).
384+ @ n the name to use for the argument.
388+ intro : (n : TTName) -> Elab ()
395+ - Introduce a lambda binding around the current hole and focus on the body, using the name provided by the type of the hole.
397+ Requires that the hole be immediately under its binder (use 'attack' if it might not be).
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
406+ (use 'attack' if it might not be).
410+ forall : TTName -> Raw -> Elab ()
413+ - Introduce a new pattern binding. Requires that the hole be immediately under its binder (use 'attack' if it might not be).
417+ patbind : TTName -> Elab ()
420+ - Introduce a new let binding.
422+ Requires that the hole be immediately under its binder (use 'attack' if it might not be).
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
430+ letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()