@@ -1,57 +1,46 @@
1−Example 1
2−=========
1+Elaborator Reflection - Identity Example
2+========================================
33
4−.. list-table:: Nat identity
4+.. list-table::
55
6− * - As an example of elaborator reflection here we step through this identity implementation:
7− - Nat identity.
8−
9− .. code-block:: idris
6+ * - This example of elaborator reflection steps through this metaprogram that generates the identity function:
7+ - .. code-block:: idris
108
119 %language ElabReflection
1210
1311 idNat : Nat -> Nat
14− idNat = %runElab (do
15− intro `{{x}}
16− fill (Var `{{x}})
17− solve
18− )
12+ idNat = %runElab (do intro `{{x}}
13+ fill (Var `{{x}})
14+ solve)
1915
20−.. list-table:: Nat identity
16+.. list-table::
2117
22− * - We start off with a hole for the whole term (of type Nat->Nat).
23− We fill that with 'intro' which creates a lambda term with a hole for the expression.
24− - diagram
18+ * - At the beginning of executing the elaboration script, the initial state consists of a single hole of type Nat -> Nat.
2519
26− .. image:: ../image/tree.png
20+ Fill that with 'intro' which creates a lambda term with a hole for the expression.
21+ - .. image:: ../image/tree.png
2722 :width: 133px
2823 :height: 106px
2924
30−After each tactic we will look at the state:
25+The following is a walkthough looking at the state after each tactic:
3126
32−.. list-table:: evolution of state
27+.. list-table::
3328
34− * - We start with the type signature like this:
35− - Nat identity.
36−
37− .. code-block:: idris
29+ * - Start with the type signature like this:
30+ - .. code-block:: idris
3831
3932 %language ElabReflection
4033
4134 idNat : Nat -> Nat
4235 idNat = %runElab (do
4336
44− * - In order to investigate how the program works we can look at the proofState at each stage as the tactics are applied. So here is the proofState at the start:
45− - state
46−
47− .. image:: ../image/elabProofStateEx1_1.png
37+ * - In order to investigate how the program works this table shows the proofState at each stage as the tactics are applied. So here is the proofState at the start:
38+ - .. image:: ../image/elabProofStateEx1_1.png
4839 :width: 310px
4940 :height: 124px
5041
51− * - We can also look at the logic at each stage:
52− - logic
53−
54− .. image:: ../image/elabLogicEx1_1.png
42+ * - This table also shows the logic at each stage:
43+ - .. image:: ../image/elabLogicEx1_1.png
5544 :width: 126px
5645 :height: 33px
5746
@@ -64,9 +53,7 @@ After each tactic we will look at the state:
6453
6554 getHoles
6655
67− - state.
68−
69− .. code-block:: idris
56+ - .. code-block:: idris
7057
7158 getEnv=[]
7259