git.iko.soy/Idris-dev
on master help sign in
update some diagrams for example
commit73dfb0c005531965ff025eb3bfc5c335125418b6 authorMartin Baker <git87465@martinb.com> dateSat 18 May 2019, 16:01 (7 years ago) parent540e76b
5 files changed+58−46
compare with master
unifiedsplit
docs/image/elabProofStateEx1_1.png docs/image/elabProofStateEx1_1.svg+23−22 docs/image/elabProofStateEx1_2.png docs/image/elabProofStateEx1_2.svg+30−20 docs/proofs/example1.rst+5−4
docs/image/elabProofStateEx1_1.png

Binary file not shown.

docs/image/elabProofStateEx1_1.svg+23−22
@@ -26,8 +26,8 @@
2626 inkscape:pageopacity="0.0"
2727 inkscape:pageshadow="2"
2828 inkscape:zoom="1"
29− inkscape:cx="425.25613"
30− inkscape:cy="593.17666"
29+ inkscape:cx="298"
30+ inkscape:cy="772.5"
3131 inkscape:document-units="px"
3232 inkscape:current-layer="layer1"
3333 showgrid="false"
@@ -207,24 +207,25 @@
207207 <text
208208 sodipodi:linespacing="125%"
209209 id="text4163"
210− y="315.36218"
211− x="171"
210+ y="275.36218"
211+ x="135"
212212 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"
213213 xml:space="preserve"
214214 inkscape:export-xdpi="61.120499"
215215 inkscape:export-ydpi="61.120499"><tspan
216216 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"
218− x="171"
217+ y="275.36218"
218+ x="135"
219219 sodipodi:role="line"
220220 id="tspan4165">starts off empty</tspan></text>
221221 <path
222222 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"
224224 id="path4167"
225225 inkscape:connector-curvature="0"
226226 inkscape:export-xdpi="61.120499"
227− inkscape:export-ydpi="61.120499" />
227+ inkscape:export-ydpi="61.120499"
228+ sodipodi:nodetypes="cc" />
228229 <text
229230 inkscape:export-ydpi="61.120499"
230231 inkscape:export-xdpi="61.120499"
@@ -244,24 +245,24 @@
244245 inkscape:export-xdpi="61.120499"
245246 xml:space="preserve"
246247 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− y="345.36218"
248+ x="233.57927"
249+ y="309.21585"
249250 id="text4794"
250251 sodipodi:linespacing="125%"><tspan
251252 id="tspan4796"
252253 sodipodi:role="line"
253− x="240"
254− y="345.36218"
254+ x="233.57927"
255+ y="309.21585"
255256 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
256257 sodipodi:role="line"
257− x="240"
258− y="364.11218"
258+ x="233.57927"
259+ y="327.96585"
259260 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
260261 id="tspan4810">we are looking for</tspan></text>
261262 <path
262263 inkscape:connector-curvature="0"
263264 id="path4798"
264− d="m 298,236.3622 9,98"
265+ d="m 298,236.3622 -0.42683,58.52439"
265266 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"
266267 sodipodi:nodetypes="cc"
267268 inkscape:export-xdpi="61.120499"
@@ -269,26 +270,26 @@
269270 <text
270271 sodipodi:linespacing="125%"
271272 id="text4800"
272− y="350.36218"
273− x="404"
273+ y="335.85608"
274+ x="383.54877"
274275 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"
275276 xml:space="preserve"
276277 inkscape:export-xdpi="61.120499"
277278 inkscape:export-ydpi="61.120499"><tspan
278279 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− x="404"
280+ y="335.85608"
281+ x="383.54877"
281282 sodipodi:role="line"
282283 id="tspan4802">machine chosen</tspan><tspan
283284 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− x="404"
285+ y="354.60608"
286+ x="383.54877"
286287 sodipodi:role="line"
287288 id="tspan4812">names for the holes</tspan></text>
288289 <path
289290 sodipodi:nodetypes="cc"
290291 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"
292293 id="path4804"
293294 inkscape:connector-curvature="0"
294295 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 @@
1515 id="svg2"
1616 version="1.1"
1717 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">
1922 <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>
2139 <sodipodi:namedview
2240 id="base"
2341 pagecolor="#ffffff"
@@ -218,37 +236,29 @@
218236 y="226.36218"
219237 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold'"
220238 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" />
229239 <text
230240 sodipodi:linespacing="125%"
231241 id="text4800"
232− y="350.36218"
233− x="404"
242+ y="290.36218"
243+ x="163"
234244 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"
235245 xml:space="preserve"
236246 inkscape:export-xdpi="61.120499"
237247 inkscape:export-ydpi="61.120499"><tspan
238248 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"
240− x="404"
249+ y="290.36218"
250+ x="163"
241251 sodipodi:role="line"
242− id="tspan4802">machine chosen</tspan><tspan
252+ id="tspan4812">replace the focussed hole</tspan><tspan
243253 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"
245− x="404"
254+ y="309.11218"
255+ x="163"
246256 sodipodi:role="line"
247− id="tspan4812">names for the holes</tspan></text>
257+ id="tspan6225">with a lambda</tspan></text>
248258 <path
249259 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"
251− d="m 432,265.3622 8,68"
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)"
261+ d="m 307,242.3622 c -5.24693,34.96318 -108.05981,45.71777 -126,0"
252262 id="path4804"
253263 inkscape:connector-curvature="0"
254264 inkscape:export-xdpi="61.120499"
docs/proofs/example1.rst+5−4
@@ -14,10 +14,11 @@ Elaborator Reflection - Identity Example
1414 solve)
1515
1616.. list-table::
17+ :widths: 200 100
1718
1819 * - At the beginning of executing the elaboration script, the initial state consists of a single hole of type Nat -> Nat.
1920
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.
2122 - .. image:: ../image/tree.png
2223 :width: 133px
2324 :height: 106px
@@ -34,10 +35,10 @@ The following is a walkthough looking at the state after each tactic:
3435 idNat : Nat -> Nat
3536 idNat = %runElab (do
3637
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:
3839 - .. image:: ../image/elabProofStateEx1_1.png
3940 :width: 310px
40− :height: 124px
41+ :height: 115px
4142
4243 * - This table also shows the logic at each stage:
4344 - .. image:: ../image/elabLogicEx1_1.png
@@ -87,7 +88,7 @@ The following is a walkthough looking at the state after each tactic:
8788
8889 .. image:: ../image/elabProofStateEx1_2.png
8990 :width: 312px
90− :height: 124px
91+ :height: 84px
9192
9293 * - logic now looks like this
9394 - logic