git.iko.soy/Idris-dev
on master help sign in
update some diagrams for example
73dfb0cMartin Baker
docs/image/elabProofStateEx1_1.png
compare with master
unifiedsplit

Binary file not shown.

docs/image/elabProofStateEx1_1.svg+23−22
@@ -26,8 +26,8 @@
26 inkscape:pageopacity="0.0"
26 inkscape:pageopacity="0.0"
27 inkscape:pageshadow="2"
27 inkscape:pageshadow="2"
28 inkscape:zoom="1"
28 inkscape:zoom="1"
29− inkscape:cx="425.25613"
29+ inkscape:cx="298"
30− inkscape:cy="593.17666"
30+ inkscape:cy="772.5"
31 inkscape:document-units="px"
31 inkscape:document-units="px"
32 inkscape:current-layer="layer1"
32 inkscape:current-layer="layer1"
33 showgrid="false"
33 showgrid="false"
@@ -207,24 +207,25 @@
207 <text
207 <text
208 sodipodi:linespacing="125%"
208 sodipodi:linespacing="125%"
209 id="text4163"
209 id="text4163"
210− y="315.36218"
210+ y="275.36218"
211− x="171"
211+ x="135"
212 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
212 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
213 xml:space="preserve"
213 xml:space="preserve"
214 inkscape:export-xdpi="61.120499"
214 inkscape:export-xdpi="61.120499"
215 inkscape:export-ydpi="61.120499"><tspan
215 inkscape:export-ydpi="61.120499"><tspan
216 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
216 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
217− y="315.36218"
217+ y="275.36218"
218− x="171"
218+ x="135"
219 sodipodi:role="line"
219 sodipodi:role="line"
220 id="tspan4165">starts off empty</tspan></text>
220 id="tspan4165">starts off empty</tspan></text>
221 <path
221 <path
222 style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
222 style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
223− d="m 157,223.3622 11,88"
223+ d="m 154,237.3622 0,25"
224 id="path4167"
224 id="path4167"
225 inkscape:connector-curvature="0"
225 inkscape:connector-curvature="0"
226 inkscape:export-xdpi="61.120499"
226 inkscape:export-xdpi="61.120499"
227− inkscape:export-ydpi="61.120499" />
227+ inkscape:export-ydpi="61.120499"
228+ sodipodi:nodetypes="cc" />
228 <text
229 <text
229 inkscape:export-ydpi="61.120499"
230 inkscape:export-ydpi="61.120499"
230 inkscape:export-xdpi="61.120499"
231 inkscape:export-xdpi="61.120499"
@@ -244,24 +245,24 @@
244 inkscape:export-xdpi="61.120499"
245 inkscape:export-xdpi="61.120499"
245 xml:space="preserve"
246 xml:space="preserve"
246 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
247 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
247− x="240"
248+ x="233.57927"
248− y="345.36218"
249+ y="309.21585"
249 id="text4794"
250 id="text4794"
250 sodipodi:linespacing="125%"><tspan
251 sodipodi:linespacing="125%"><tspan
251 id="tspan4796"
252 id="tspan4796"
252 sodipodi:role="line"
253 sodipodi:role="line"
253− x="240"
254+ x="233.57927"
254− y="345.36218"
255+ y="309.21585"
255 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">this is the signature</tspan><tspan
256 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'">this is the signature</tspan><tspan
256 sodipodi:role="line"
257 sodipodi:role="line"
257− x="240"
258+ x="233.57927"
258− y="364.11218"
259+ y="327.96585"
259 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
260 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
260 id="tspan4810">we are looking for</tspan></text>
261 id="tspan4810">we are looking for</tspan></text>
261 <path
262 <path
262 inkscape:connector-curvature="0"
263 inkscape:connector-curvature="0"
263 id="path4798"
264 id="path4798"
264− d="m 298,236.3622 9,98"
265+ d="m 298,236.3622 -0.42683,58.52439"
265 style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
266 style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
266 sodipodi:nodetypes="cc"
267 sodipodi:nodetypes="cc"
267 inkscape:export-xdpi="61.120499"
268 inkscape:export-xdpi="61.120499"
@@ -269,26 +270,26 @@
269 <text
270 <text
270 sodipodi:linespacing="125%"
271 sodipodi:linespacing="125%"
271 id="text4800"
272 id="text4800"
272− y="350.36218"
273+ y="335.85608"
273− x="404"
274+ x="383.54877"
274 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
275 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
275 xml:space="preserve"
276 xml:space="preserve"
276 inkscape:export-xdpi="61.120499"
277 inkscape:export-xdpi="61.120499"
277 inkscape:export-ydpi="61.120499"><tspan
278 inkscape:export-ydpi="61.120499"><tspan
278 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
279 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
279− y="350.36218"
280+ y="335.85608"
280− x="404"
281+ x="383.54877"
281 sodipodi:role="line"
282 sodipodi:role="line"
282 id="tspan4802">machine chosen</tspan><tspan
283 id="tspan4802">machine chosen</tspan><tspan
283 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
284 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
284− y="369.11218"
285+ y="354.60608"
285− x="404"
286+ x="383.54877"
286 sodipodi:role="line"
287 sodipodi:role="line"
287 id="tspan4812">names for the holes</tspan></text>
288 id="tspan4812">names for the holes</tspan></text>
288 <path
289 <path
289 sodipodi:nodetypes="cc"
290 sodipodi:nodetypes="cc"
290 style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
291 style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
291− d="m 432,265.3622 8,68"
292+ d="m 432,265.3622 0.15244,56.82317"
292 id="path4804"
293 id="path4804"
293 inkscape:connector-curvature="0"
294 inkscape:connector-curvature="0"
294 inkscape:export-xdpi="61.120499"
295 inkscape:export-xdpi="61.120499"
docs/image/elabProofStateEx1_2.png

Binary file not shown.

docs/image/elabProofStateEx1_2.svg+30−20
@@ -15,9 +15,27 @@
15 id="svg2"
15 id="svg2"
16 version="1.1"
16 version="1.1"
17 inkscape:version="0.91 r13725"
17 inkscape:version="0.91 r13725"
18− sodipodi:docname="elabProofStateEx1_2.svg">
18+ sodipodi:docname="elabProofStateEx1_2.svg"
19+ inkscape:export-filename="/home/mjb/Idris-dev/docs/image/elabProofStateEx1_2.png"
20+ inkscape:export-xdpi="61.120499"
21+ inkscape:export-ydpi="61.120499">
19 <defs
22 <defs
20− id="defs4" />
23+ id="defs4">
24+ <marker
25+ inkscape:stockid="Arrow1Mend"
26+ orient="auto"
27+ refY="0.0"
28+ refX="0.0"
29+ id="Arrow1Mend"
30+ style="overflow:visible;"
31+ inkscape:isstock="true">
32+ <path
33+ id="path4252"
34+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
35+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"
36+ transform="scale(0.4) rotate(180) translate(10,0)" />
37+ </marker>
38+ </defs>
21 <sodipodi:namedview
39 <sodipodi:namedview
22 id="base"
40 id="base"
23 pagecolor="#ffffff"
41 pagecolor="#ffffff"
@@ -218,37 +236,29 @@
218 y="226.36218"
236 y="226.36218"
219 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
237 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
220 id="tspan4790">(hole_2 , Nat)</tspan></text>
238 id="tspan4790">(hole_2 , Nat)</tspan></text>
221− <path
222− inkscape:connector-curvature="0"
223− id="path4798"
224− d="m 298,236.3622 9,98"
225− style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
226− sodipodi:nodetypes="cc"
227− inkscape:export-xdpi="61.120499"
228− inkscape:export-ydpi="61.120499" />
229 <text
239 <text
230 sodipodi:linespacing="125%"
240 sodipodi:linespacing="125%"
231 id="text4800"
241 id="text4800"
232− y="350.36218"
242+ y="290.36218"
233− x="404"
243+ x="163"
234 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
244 style="font-style:normal;font-weight:normal;font-size:15px;line-height:125%;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
235 xml:space="preserve"
245 xml:space="preserve"
236 inkscape:export-xdpi="61.120499"
246 inkscape:export-xdpi="61.120499"
237 inkscape:export-ydpi="61.120499"><tspan
247 inkscape:export-ydpi="61.120499"><tspan
238 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
248 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
239− y="350.36218"
249+ y="290.36218"
240− x="404"
250+ x="163"
241 sodipodi:role="line"
251 sodipodi:role="line"
242− id="tspan4802">machine chosen</tspan><tspan
252+ id="tspan4812">replace the focussed hole</tspan><tspan
243 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
253 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
244− y="369.11218"
254+ y="309.11218"
245− x="404"
255+ x="163"
246 sodipodi:role="line"
256 sodipodi:role="line"
247− id="tspan4812">names for the holes</tspan></text>
257+ id="tspan6225">with a lambda</tspan></text>
248 <path
258 <path
249 sodipodi:nodetypes="cc"
259 sodipodi:nodetypes="cc"
250− style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
260+ style="fill:none;fill-rule:evenodd;stroke:#000000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow1Mend)"
251− d="m 432,265.3622 8,68"
261+ d="m 307,242.3622 c -5.24693,34.96318 -108.05981,45.71777 -126,0"
252 id="path4804"
262 id="path4804"
253 inkscape:connector-curvature="0"
263 inkscape:connector-curvature="0"
254 inkscape:export-xdpi="61.120499"
264 inkscape:export-xdpi="61.120499"
docs/proofs/example1.rst+5−4
@@ -14,10 +14,11 @@ Elaborator Reflection - Identity Example
14 solve)
14 solve)
15
15
16.. list-table::
16.. list-table::
17+ :widths: 200 100
17
18
18 * - At the beginning of executing the elaboration script, the initial state consists of a single hole of type Nat -> Nat.
19 * - At the beginning of executing the elaboration script, the initial state consists of a single hole of type Nat -> Nat.
19
20
20− Fill that with 'intro' which creates a lambda term with a hole for the expression.
21+ As a first approximation, the state consists of a term with holes in it, an indicator of which hole is focused, a queue of the next holes to focus on, and miscellaneous information like a source of fresh names. The intro tactic modifies this state, replacing the focused hole with a lambda and focusing on the lambda's body.
21 - .. image:: ../image/tree.png
22 - .. image:: ../image/tree.png
22 :width: 133px
23 :width: 133px
23 :height: 106px
24 :height: 106px
@@ -34,10 +35,10 @@ The following is a walkthough looking at the state after each tactic:
34 idNat : Nat -> Nat
35 idNat : Nat -> Nat
35 idNat = %runElab (do
36 idNat = %runElab (do
36
37
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+ * - In order to investigate how the program works this table shows the proof state at each stage as the tactics are applied. So here is the proof state at the start:
38 - .. image:: ../image/elabProofStateEx1_1.png
39 - .. image:: ../image/elabProofStateEx1_1.png
39 :width: 310px
40 :width: 310px
40− :height: 124px
41+ :height: 115px
41
42
42 * - This table also shows the logic at each stage:
43 * - This table also shows the logic at each stage:
43 - .. image:: ../image/elabLogicEx1_1.png
44 - .. image:: ../image/elabLogicEx1_1.png
@@ -87,7 +88,7 @@ The following is a walkthough looking at the state after each tactic:
87
88
88 .. image:: ../image/elabProofStateEx1_2.png
89 .. image:: ../image/elabProofStateEx1_2.png
89 :width: 312px
90 :width: 312px
90− :height: 124px
91+ :height: 84px
91
92
92 * - logic now looks like this
93 * - logic now looks like this
93 - logic
94 - logic