@@ -0,0 +1,177 @@
1+Elaborator Reflection - Holes
2+=============================
4+The process of doing proofs and elaborator reflection tends to involve stating with a desired conclusion and working back to known premises. This often needs intermediate sub-goals which may only be partially solved, these are encoded using 'holes' and 'guesses'.
6+* A hole is a term (an expression - a chunk of code) which is yet to be determined. We do have information about its type (this process tends to be type driven).
7+* A guess is like a hole that is not yet bound.
9+The theory around this was developed in `Dependently Typed Functional Programs and their Proofs by McBride 1999`_.
11+Notation for Holes and Guesses
12+------------------------------
14+There is a notation used in the McBride 1999 thesis which is adapted for the TT language. When working on elaborator reflection it is useful to know this notation, for instance when reading the output of the 'debug' tactic.
16+* A focused hole is notated like this ?x:t . t
17+* A guess is notated like this ?x ≈ t:t . t
19+The following example shows how this is used:
24+Start with a code file that just contains:
28+ %language ElabReflection
31+ testFn = %runElab (do debug {a = ()})
33+when this is loaded the following is displayed:
38+ ----------------------------------
39+ {hole_2} : Prelude.Nat.Nat
41+ ----------------------------------
42+ {hole_0} : Prelude.Nat.Nat
45+ ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}
47+This shows information about the state when debug is encountered, during tactic execution, which allows us to investigate what is happening at each stage.
49+* The "Holes" part shows the types of the holes and the local context of each
50+* The "Term" part shows where these holes are in the expression being constructed.
52+So starting with the "Term" part we have.
56+ ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}
58+.. sidebar:: attack tactic
60+ This kind of thing tends to arise from "attack", which helps keep binding forms in order.
62+The meaning of this is not immediately apparent so it helps to add some parentheses to make the structure clearer:
66+ (?{hole_0} ≈ (? {hole_2} . {hole_2}) . {hole_0})
68+First lets look at the inner part:
72+ ? {hole_2} . {hole_2}
74+We can substitute in the type from the "Holes" part:
78+ ? {hole_2}:Nat . {hole_2}:Nat
80+So we are looking for a hole of type Nat and all we know is it has type Nat.
82+Going back to the full term, the above is wrapped in a guess, so it means: 'a guess that is itself a hole'.
84+Example Showing Patterns
85+------------------------
87+In this example a parameter 'n' has been added to the function. This allows us to see how patterns are used. Starting with this file:
91+ %language ElabReflection
94+ testFn n = %runElab (do debug {a = ()})
102+ ----------------------------------
103+ {hole_3} : Prelude.Nat.Nat
106+ ----------------------------------
107+ {hole_1} : Prelude.Nat.Nat
109+ ----------------------------------
110+ {hole_0} : patTy n : Prelude.Nat.Nat . Prelude.Nat.Nat
113+ ?{hole_0} ≈ pat n : Prelude.Nat.Nat .
114+ ?{hole_1} ≈ ? {hole_3} . {hole_3} . {hole_1} .
117+The ns above the lines show the context of the holes on the right hand side - they include the variable n that is an argument!
119+patTy is a binding form in Idris's core language that introduces a pattern variable. The idea is that the left-hand side and right-hand side of each pattern should have the same type. Because pattern variables may occur multiple times on either side of the equation, we can achieve this by documenting their types with a binding form that wraps each side. This new binding form is why an "attack" was necessary prior to elaborating the RHS.
121+patTy is a type former, and pat is the corresponding introduction form. So you can think of patTy as being a bit like a dependent function type, and pat as being a bit like lambda, except they don't introduce functions (they instead are used for pattern-matching definitions).
123+More Complicated Example
124+------------------------
126+This example does not introduce any new notation but the extra complexity gives a more realistic idea of how it is used. Here we start with this file:
128+.. code-block:: idris
130+ %language ElabReflection
132+ testFn : (n : Nat) -> (n = plus n Z) -> (S n = S (plus n Z))
133+ testFn k ih = %runElab (do debug {a = ()})
137+.. code-block:: idris
141+ ih : = Prelude.Nat.Nat Prelude.Nat.Nat k
142+ (Prelude.Nat.plus k Prelude.Nat.Z)
143+ ----------------------------------
144+ {hole_4} : = Prelude.Nat.Nat Prelude.Nat.Nat (Prelude.Nat.S k)
145+ (Prelude.Nat.S (Prelude.Nat.plus k Prelude.Nat.Z))
148+ ih : = Prelude.Nat.Nat Prelude.Nat.Nat k
149+ (Prelude.Nat.plus k Prelude.Nat.Z)
150+ ----------------------------------
151+ {hole_2} : = Prelude.Nat.Nat Prelude.Nat.Nat (Prelude.Nat.S k)
152+ (Prelude.Nat.S (Prelude.Nat.plus k Prelude.Nat.Z))
155+ ----------------------------------
156+ {hole_1} : patTy ih : = Prelude.Nat.Nat Prelude.Nat.Nat k
157+ (Prelude.Nat.plus k Prelude.Nat.Z) .
158+ = Prelude.Nat.Nat Prelude.Nat.Nat (Prelude.Nat.S k)
159+ (Prelude.Nat.S (Prelude.Nat.plus k Prelude.Nat.Z))
161+ ----------------------------------
162+ {hole_0} : patTy k : Prelude.Nat.Nat .
163+ patTy ih : = Prelude.Nat.Nat Prelude.Nat.Nat k
164+ (Prelude.Nat.plus k Prelude.Nat.Z) .
165+ = Prelude.Nat.Nat Prelude.Nat.Nat (Prelude.Nat.S k)
166+ (Prelude.Nat.S (Prelude.Nat.plus k Prelude.Nat.Z))
169+ ?{hole_0} ≈ pat k : Prelude.Nat.Nat .
170+ ?{hole_1} ≈ pat ih : = Prelude.Nat.Nat Prelude.Nat.Nat k
171+ (Prelude.Nat.plus k Prelude.Nat.Z) .
172+ ?{hole_2} ≈ ? {hole_4} . {hole_4} . {hole_2} .
177+.. _`Dependently Typed Functional Programs and their Proofs by McBride 1999`: https://www.era.lib.ed.ac.uk/handle/1842/374