# Elaborator Reflection - Tactics¶

The Idris part of the code for elaborator reflection is in Elab.idr https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Language/Reflection/Elab.idr Before looking at the Elab monad we need to know how to construct terms.

## Proof State¶

The terminology ‘Proof State’ is used by analogy to proof assistants but, as used here, it’s really more of a metaprogramming state.

Tactics operate on the proof state. The proof state contains various pieces of information, at this stage, the important ones for us are:

- 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. For more information about holes and guesses see Dependently Typed Functional Programs and their Proofs by McBride 1999 [1].
- A goal type - The type of the term that is under construction for the current goal.
- A possibly incomplete proof term, which is being calculated and should be the goal type at the end of elaboration.
- Context - A collection of open unification problems, representing recoverable failures of unification that may yet unify once more variables are solved.

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.

## Names TTName¶

Names in an Idris program are evaluated at runtime but sometimes a ‘variable name’ is needed, which can be referred to as an unevaluated symbol. The names used in terms have different constructors depending on their type:

UN String | A user-provided name |

NS (UN “foo”) [“B”, “A”]) | A name in some namespace |

MN Int String | Machine-chosen names |

SN SpecialName | Special names, to make conflicts impossible and language features predictable |

A user defined name can be constructed like this:

```
Idris> UN "x"
UN "x" : TTName
```

```
Idris> NS (UN "x") ["b","a"]
NS (UN "x") ["b", "a"] : TTName
```

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: | example of unique names: ```
implementation Show TTName where
show (UN s) = "`{{"++s++"}}"
show (NS t a) = "{"++(show t)++
"."++(show a)++"}"
show (MN i s) = "{"++s++"_"++(show i)++"}"
show (SN sn) = "TTName special name"
showGensym : String
showGensym = %runElab (do
debugMessage [TextPart (
show !(gensym "abc") ++
show !(gensym "abc")
)]
)
``` |

## Quasiquotation¶

Since names are used frequently in elaborator reflection there is a shortcut for constructing them:

An unresolved variable “x” is wrapped in backtick and double braces: | ```
Idris> `{{x}}
UN "x" : TTName
``` |

Single braces are used for existing variables: | ```
Idris> `{x}
No such variable x
Idris> :let x=2
Idris> `{x}
UN "x" : TTName
``` |

brackets are used for an expression: here type is inferable |
```
Idris> :let a=2
Idris> `(a)
P Ref (UN "a") (TConst (AType (ATInt ITBig))) : TT
``` |

Expression with explicit type: | ```
Idris> `(a:Integer)
P Ref (UN "a") (TConst (AType (ATInt ITBig))) : TT
``` |

If we want the value we can escape from quasiquotation by using anti-quotation (tilde) | ```
Idris> `(~a)
2 : Integer
``` |

quasiquotation summary:

Reification | ||
---|---|---|

`{{n}} | TTName | Use for new names. Unresolved quotation of the name n. |

`{n} | TTName | Use for existing names. Resolved quotation of the name n. n is a reference to a unique name in scope. |

`(e) | expression e for which a type is inferable. | |

`(e:t) | expression e with a given type e. | |

~a | anti-quotation - sub region which can be evaluated rather than quoted. | |

(Var`{{x}}) | Raw |

## TT¶

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 it is used here. So internally the program is stored as a tree structure using the following syntax:

Syntax | More Information | ||
---|---|---|---|

term | t | ||

binding | b | ||

constant | t ::= | c | |

variable | t ::= | x | |

variable binding | t ::= | b.t | so a dot ‘.’ tells us this is some sort of binding. |

application | t ::= | t t | As with Idris, juxtaposition indicates function application. Note: the same symbol ‘t’ is used for both terms, this does not imply they are the same term. |

Type constructor | t ::= | T | |

Data constructor | t ::= | C | |

function | b::= | λ c:t | colon ‘:’ separates parameters from body of binding. |

let binding | b::= | let|-> t:t | |

function | b::= | ∀ x:t | |

Type universe | c::= | *i | The universe hierarchy is usually handled automatically so we can just use* for the type of types. |

integer literal | c:== | i | |

integer type | c:== | Integer | |

string literal | c:== | s | |

string type | c:== | String | |

focused hole | ?x : t | Conor McBride 1999 thesis. | |

guess | ?x ≈ t : t | Conor McBride 1999 thesis. |

Sometimes the part of the term in focus is underlined.

Reflection of the well typed core language

```
data TT =
||| A reference to some name (P for Parameter)
P NameType TTName TT |
||| de Bruijn variables
V Int |
||| Bind a variable
Bind TTName (Binder TT) TT |
||| Apply one term to another
App TT TT |
||| Embed a constant
TConst Const |
||| Erased terms
Erased |
||| The type of types along (with universe constraints)
TType TTUExp |
||| Alternative universes for dealing with uniqueness
UType Universe |
```

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. De Bruijn index which is a integer where:

- 0=inside current (inner) lambda term
- 1= next outer lambda term
- 2= next outer and so on

## Raw¶

Raw is similar to TT except it is used before types are known. The types should be resolved by the type checker.

```
data Raw =
||| Variables, global or local
Var TTName |
||| Bind a variable
RBind TTName (Binder Raw) Raw |
||| Application
RApp Raw Raw |
||| The type of types
RType |
||| Alternative universes for dealing with uniqueness
RUType Universe |
||| Embed a constant
RConstant Const |
```

## Expression Syntax¶

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.

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.

The notation assumes right-associativity, in the absence of brackets, the term to the right binds more tightly than the one on the left. So, for nested lambda terms:

λ a . λ b . f | means | λ a .( λ b . f) |

and the same for function application:

f g x | means | f (g x) |

In contrast, in lambda calculus, function application is usually regarded as left-associative, Here are some typical examples of the notation used for expressions:

? {hole_0} . {hole_0} |

The term, to be derived, may start off in this state following something like this:

```
myScript : Elab ()
myScript= do
```

The dot ‘.’ tells us this is some sort of binding.

?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0} |

This is a slightly more complicated example arising from:

```
idNat : Nat -> Nat
idNat = %runElab (do
```

This introduces a guess that hole_0 = hole_2 .

?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0} |

Following on from the previous example a lambda function is introduced like this:

```
intro `{{x}}
```

So now the expression is wrapped in a lambda binding.

?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0} |

Following on, we can use the fill tactic like this:

```
fill (Var `{{x}})
```

which introduces another guess.

?{hole_0} ≈ λ x . x . {hole_0} |

The solve tactic completes the proof

## Binders¶

Here we look at each tactic in turn to see how they affect the proof state.

Introduction tactics for binders. The binder types are:

- lambda function (intro)
- dependent function (forall)
- let (letBind)
- pattern (patbind)

A precondition of these tactics is that the focused hole is of the form:

?h : t.h |

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:

?h : t1 -> t2.f h |

and a tactic such as

intro `{{x}} |

were applied, the result would be the term

?h : t2 . λ x:t1. f h |

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.

intro | Introduce a lambda binding around the current hole and focus on the body. Requires that the hole be in binding form (use ‘attack’ if it might not be). @ n the name to use for the argument. Signature: intro : (n : TTName) -> Elab () Result λn:t1.?h:[n/x]t2.h |
---|---|

intro’ | Introduce a lambda binding around the current hole and focus on the body, using the name provided by the type of the hole. Requires that the hole be immediately under its binder (use ‘attack’ if it might not be). Signature: intro’ : Elab () |

forall | Introduce a dependent function type binding into the current hole, and focus on the body. Requires that the hole be immediately under its binder (use ‘attack’ if it might not be). Signature: forall : TTName -> Raw -> Elab () |

patbind | Introduce a new pattern binding. Requires that the hole be immediately under its binder (use ‘attack’ if it might not be). Signature: patbind : TTName -> Elab () |

letbind | Introduce a new let binding. Requires that the hole be immediately under its binder (use ‘attack’ if it might not be). - @ n the name to let bind
- @ ty the type of the term to be let-bound
- @ tm the term to be bound
Signature: letbind : (n : TTName) -> (ty, tm : Raw) -> Elab () |

[1] | https://www.era.lib.ed.ac.uk/handle/1842/374 |