Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add Documentation for Elaborator Reflection #4700

Merged
merged 45 commits into from
Dec 2, 2019
Merged
Changes from 1 commit
Commits
Show all changes
45 commits
Select commit Hold shift + click to select a range
d748d5e
add documentation for elaboration reflection
May 8, 2019
cd58dfb
add documentation for elaboration reflection
May 8, 2019
b6fde49
fix image paths
May 8, 2019
278de06
change title of theorem proving section
May 8, 2019
5e25d2b
fix minor formatting issue
May 8, 2019
1772239
minor change - add reference
May 9, 2019
9472245
inital changes following comments, more to come
May 15, 2019
d0a4575
further improvements from comments
May 15, 2019
420f2b8
add readme file to explain image file formats
May 15, 2019
0fb8b75
fix typo
May 15, 2019
5267e39
fix reference
May 15, 2019
5cd37d8
change as suggested
May 15, 2019
ae9484a
more suggested changes
May 16, 2019
40c7a8a
update copyright notice to 2019
May 16, 2019
dd2c427
update elabOverview image
May 16, 2019
7b70c6c
improve some diagrams
May 17, 2019
8933505
remove space which caused incorrect formatting
May 17, 2019
efbb287
change text around logic diagram
May 17, 2019
edd8da7
start to make changes to identity example
May 17, 2019
654c431
rename file
May 18, 2019
540e76b
remove some duplicated definitions and tidy up
May 18, 2019
73dfb0c
update some diagrams for example
May 18, 2019
a13f2ab
more small changes
May 19, 2019
d85b8c6
more small changes
May 19, 2019
6255c0d
add svg diagram
May 19, 2019
566daf7
changes to generatingData.rst
May 20, 2019
08c0900
changes to generatingData.rst
May 21, 2019
231d842
changes to generatingData.rst
May 21, 2019
ff054c1
changes to generatingData.rst
May 22, 2019
1b71663
changes to tactics.rst
May 22, 2019
543a382
changes to tactics.rst
May 22, 2019
671bb4d
changes to primitive.rst
May 22, 2019
b093a14
add diagram to illustrate Raw structure used for function definition
May 22, 2019
75feef7
fix example code for generating functions
May 23, 2019
19d6e29
tidy up diagrams for example
May 23, 2019
defab73
update hole diagrams & remove reference to logic
Jul 1, 2019
a4da735
fix markup error
Jul 2, 2019
00f95a4
add a page about the notation for holes and guesses
Jul 3, 2019
810528d
corrections to identity example
Jul 3, 2019
8f8303e
corrections to identity example
Jul 3, 2019
eda6a87
extend holes example
Jul 4, 2019
d73e3c5
add example and diagram for fill
Jul 5, 2019
c2690a9
add example and diagram for solve
Jul 5, 2019
c891750
add diagram for attack
Jul 6, 2019
cf3071d
explain getEnv, getGoal, getHoles and getGuess better
Jul 16, 2019
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
add a page about the notation for holes and guesses
martinbaker committed Jul 3, 2019
commit 00f95a47c13cf836c6d04a5d58c111feb67dc39d
177 changes: 177 additions & 0 deletions docs/proofs/holes.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,177 @@
Elaborator Reflection - Holes
=============================

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'.

* 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).
* A guess is like a hole that is not yet bound.

The theory around this was developed in `Dependently Typed Functional Programs and their Proofs by McBride 1999`_.

Notation for Holes and Guesses
------------------------------

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.

* A focused hole is notated like this ?x:t . t
* A guess is notated like this ?x ≈ t:t . t

The following example shows how this is used:

Simple Example
--------------

Start with a code file that just contains:

.. code-block:: idris
%language ElabReflection
testFn : Nat
testFn = %runElab (do debug {a = ()})
when this is loaded the following is displayed:

.. code-block:: idris
Holes:
----------------------------------
{hole_2} : Prelude.Nat.Nat
----------------------------------
{hole_0} : Prelude.Nat.Nat
Term:
?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}
This shows information about the state when debug is encountered, during tactic execution, which allows us to investigate what is happening at each stage.

* The "Holes" part shows the types of the holes and the local context of each
* The "Term" part shows where these holes are in the expression being constructed.

So starting with the "Term" part we have.

.. code-block:: idris
?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}
.. sidebar:: attack tactic

This kind of thing tends to arise from "attack", which helps keep binding forms in order.

The meaning of this is not immediately apparent so it helps to add some parentheses to make the structure clearer:

.. code-block:: idris
(?{hole_0} ≈ (? {hole_2} . {hole_2}) . {hole_0})
First lets look at the inner part:

.. code-block:: idris
? {hole_2} . {hole_2}
We can substitute in the type from the "Holes" part:

.. code-block:: idris
? {hole_2}:Nat . {hole_2}:Nat
So we are looking for a hole of type Nat and all we know is it has type Nat.

Going back to the full term, the above is wrapped in a guess, so it means: 'a guess that is itself a hole'.

Example Showing Patterns
------------------------

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:

.. code-block:: idris
%language ElabReflection
testFn : Nat -> Nat
testFn n = %runElab (do debug {a = ()})
when loaded gives:

.. code-block:: idris
Holes:
n : Prelude.Nat.Nat
----------------------------------
{hole_3} : Prelude.Nat.Nat
n : Prelude.Nat.Nat
----------------------------------
{hole_1} : Prelude.Nat.Nat
----------------------------------
{hole_0} : patTy n : Prelude.Nat.Nat . Prelude.Nat.Nat
Term:
?{hole_0} ≈ pat n : Prelude.Nat.Nat .
?{hole_1} ≈ ? {hole_3} . {hole_3} . {hole_1} .
{hole_0}
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!

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.

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).

More Complicated Example
------------------------

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:

.. code-block:: idris
%language ElabReflection
testFn : (n : Nat) -> (n = plus n Z) -> (S n = S (plus n Z))
testFn k ih = %runElab (do debug {a = ()})
when loaded gives:

.. code-block:: idris
Holes:
k : Prelude.Nat.Nat
ih : = Prelude.Nat.Nat Prelude.Nat.Nat k
(Prelude.Nat.plus k Prelude.Nat.Z)
----------------------------------
{hole_4} : = Prelude.Nat.Nat Prelude.Nat.Nat (Prelude.Nat.S k)
(Prelude.Nat.S (Prelude.Nat.plus k Prelude.Nat.Z))
k : Prelude.Nat.Nat
ih : = Prelude.Nat.Nat Prelude.Nat.Nat k
(Prelude.Nat.plus k Prelude.Nat.Z)
----------------------------------
{hole_2} : = Prelude.Nat.Nat Prelude.Nat.Nat (Prelude.Nat.S k)
(Prelude.Nat.S (Prelude.Nat.plus k Prelude.Nat.Z))
k : Prelude.Nat.Nat
----------------------------------
{hole_1} : patTy ih : = Prelude.Nat.Nat Prelude.Nat.Nat k
(Prelude.Nat.plus k Prelude.Nat.Z) .
= Prelude.Nat.Nat Prelude.Nat.Nat (Prelude.Nat.S k)
(Prelude.Nat.S (Prelude.Nat.plus k Prelude.Nat.Z))
----------------------------------
{hole_0} : patTy k : Prelude.Nat.Nat .
patTy ih : = Prelude.Nat.Nat Prelude.Nat.Nat k
(Prelude.Nat.plus k Prelude.Nat.Z) .
= Prelude.Nat.Nat Prelude.Nat.Nat (Prelude.Nat.S k)
(Prelude.Nat.S (Prelude.Nat.plus k Prelude.Nat.Z))
Term:
?{hole_0} ≈ pat k : Prelude.Nat.Nat .
?{hole_1} ≈ pat ih : = Prelude.Nat.Nat Prelude.Nat.Nat k
(Prelude.Nat.plus k Prelude.Nat.Z) .
?{hole_2} ≈ ? {hole_4} . {hole_4} . {hole_2} .
{hole_1} .
{hole_0}
.. target-notes::
.. _`Dependently Typed Functional Programs and their Proofs by McBride 1999`: https://www.era.lib.ed.ac.uk/handle/1842/374
1 change: 1 addition & 0 deletions docs/proofs/index.rst
Original file line number Diff line number Diff line change
@@ -27,6 +27,7 @@ A tutorial on theorem proving in Idris.
interactiveOld
elabReflection
tactics
holes
example1
primitive
generatingData