git.iko.soy/Idris-dev
on master help sign in
changes to generatingData.rst
08c0900Martin Baker
docs/image/generateDatatype.pngnew file
compare with master
unifiedsplit

Binary file not shown.

docs/image/generateDatatype.svgnew file+540
@@ -0,0 +1,540 @@
1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
2+<!-- Created with Inkscape (http://www.inkscape.org/) -->
3+
4+<svg
5+ xmlns:dc="http://purl.org/dc/elements/1.1/"
6+ xmlns:cc="http://creativecommons.org/ns#"
7+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
8+ xmlns:svg="http://www.w3.org/2000/svg"
9+ xmlns="http://www.w3.org/2000/svg"
10+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
11+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
12+ width="210mm"
13+ height="297mm"
14+ viewBox="0 0 744.09448819 1052.3622047"
15+ id="svg2"
16+ version="1.1"
17+ inkscape:version="0.91 r13725"
18+ sodipodi:docname="generateDatatype.svg">
19+ <defs
20+ id="defs4">
21+ <marker
22+ inkscape:isstock="true"
23+ style="overflow:visible;"
24+ id="marker7147"
25+ refX="0.0"
26+ refY="0.0"
27+ orient="auto"
28+ inkscape:stockid="Arrow2Mend">
29+ <path
30+ transform="scale(0.6) rotate(180) translate(0,0)"
31+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
32+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#ff0000;stroke-opacity:1;fill:#ff0000;fill-opacity:1"
33+ id="path7149" />
34+ </marker>
35+ <marker
36+ inkscape:stockid="Arrow2Mend"
37+ orient="auto"
38+ refY="0.0"
39+ refX="0.0"
40+ id="marker6819"
41+ style="overflow:visible;"
42+ inkscape:isstock="true">
43+ <path
44+ id="path6821"
45+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#ff0000;stroke-opacity:1;fill:#ff0000;fill-opacity:1"
46+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
47+ transform="scale(0.6) rotate(180) translate(0,0)" />
48+ </marker>
49+ <marker
50+ inkscape:isstock="true"
51+ style="overflow:visible;"
52+ id="marker6325"
53+ refX="0.0"
54+ refY="0.0"
55+ orient="auto"
56+ inkscape:stockid="Arrow2Mend">
57+ <path
58+ transform="scale(0.6) rotate(180) translate(0,0)"
59+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
60+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#ff0000;stroke-opacity:1;fill:#ff0000;fill-opacity:1"
61+ id="path6327" />
62+ </marker>
63+ <marker
64+ inkscape:stockid="Arrow2Mend"
65+ orient="auto"
66+ refY="0.0"
67+ refX="0.0"
68+ id="marker5163"
69+ style="overflow:visible;"
70+ inkscape:isstock="true">
71+ <path
72+ id="path5165"
73+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#ff0000;stroke-opacity:1;fill:#ff0000;fill-opacity:1"
74+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
75+ transform="scale(0.6) rotate(180) translate(0,0)" />
76+ </marker>
77+ <marker
78+ inkscape:isstock="true"
79+ style="overflow:visible;"
80+ id="marker5133"
81+ refX="0.0"
82+ refY="0.0"
83+ orient="auto"
84+ inkscape:stockid="Arrow2Mend"
85+ inkscape:collect="always">
86+ <path
87+ transform="scale(0.6) rotate(180) translate(0,0)"
88+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
89+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#ff0000;stroke-opacity:1;fill:#ff0000;fill-opacity:1"
90+ id="path5135" />
91+ </marker>
92+ <marker
93+ inkscape:stockid="Arrow2Mend"
94+ orient="auto"
95+ refY="0.0"
96+ refX="0.0"
97+ id="Arrow2Mend"
98+ style="overflow:visible;"
99+ inkscape:isstock="true"
100+ inkscape:collect="always">
101+ <path
102+ id="path4183"
103+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#ff0000;stroke-opacity:1;fill:#ff0000;fill-opacity:1"
104+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
105+ transform="scale(0.6) rotate(180) translate(0,0)" />
106+ </marker>
107+ </defs>
108+ <sodipodi:namedview
109+ id="base"
110+ pagecolor="#ffffff"
111+ bordercolor="#666666"
112+ borderopacity="1.0"
113+ inkscape:pageopacity="0.0"
114+ inkscape:pageshadow="2"
115+ inkscape:zoom="1"
116+ inkscape:cx="380.92935"
117+ inkscape:cy="520"
118+ inkscape:document-units="px"
119+ inkscape:current-layer="layer1"
120+ showgrid="false"
121+ inkscape:window-width="1212"
122+ inkscape:window-height="1011"
123+ inkscape:window-x="-4"
124+ inkscape:window-y="0"
125+ inkscape:window-maximized="0" />
126+ <metadata
127+ id="metadata7">
128+ <rdf:RDF>
129+ <cc:Work
130+ rdf:about="">
131+ <dc:format>image/svg+xml</dc:format>
132+ <dc:type
133+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
134+ <dc:title></dc:title>
135+ </cc:Work>
136+ </rdf:RDF>
137+ </metadata>
138+ <g
139+ inkscape:label="Layer 1"
140+ inkscape:groupmode="layer"
141+ id="layer1">
142+ <rect
143+ style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
144+ id="rect4136"
145+ width="201"
146+ height="69"
147+ x="116"
148+ y="203.3622"
149+ inkscape:export-xdpi="61.120499"
150+ inkscape:export-ydpi="61.120499" />
151+ <rect
152+ y="322.36218"
153+ x="113"
154+ height="69"
155+ width="201"
156+ id="rect4138"
157+ style="opacity:1;fill:none;fill-opacity:1;stroke:#0000ff;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
158+ inkscape:export-xdpi="61.120499"
159+ inkscape:export-ydpi="61.120499" />
160+ <rect
161+ y="202.3622"
162+ x="381"
163+ height="69"
164+ width="201"
165+ id="rect4140"
166+ style="opacity:1;fill:none;fill-opacity:1;stroke:#000000;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
167+ inkscape:export-xdpi="61.120499"
168+ inkscape:export-ydpi="61.120499" />
169+ <text
170+ xml:space="preserve"
171+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
172+ x="125"
173+ y="227.3622"
174+ id="text4142"
175+ sodipodi:linespacing="125%"
176+ inkscape:export-xdpi="61.120499"
177+ inkscape:export-ydpi="61.120499"><tspan
178+ sodipodi:role="line"
179+ id="tspan4144"
180+ x="125"
181+ y="227.3622">declareDatatype</tspan></text>
182+ <text
183+ sodipodi:linespacing="125%"
184+ id="text4146"
185+ y="225.3622"
186+ x="389"
187+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
188+ xml:space="preserve"
189+ inkscape:export-xdpi="61.120499"
190+ inkscape:export-ydpi="61.120499"><tspan
191+ y="225.3622"
192+ x="389"
193+ id="tspan4148"
194+ sodipodi:role="line">defineDatatype</tspan></text>
195+ <path
196+ style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker5133)"
197+ d="m 190,271.3622 0,48"
198+ id="path4150"
199+ inkscape:connector-curvature="0"
200+ inkscape:export-xdpi="61.120499"
201+ inkscape:export-ydpi="61.120499" />
202+ <text
203+ sodipodi:linespacing="125%"
204+ id="text5074"
205+ y="295.36218"
206+ x="201"
207+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
208+ xml:space="preserve"
209+ inkscape:export-xdpi="61.120499"
210+ inkscape:export-ydpi="61.120499"><tspan
211+ y="295.36218"
212+ x="201"
213+ sodipodi:role="line"
214+ id="tspan5080"
215+ style="font-size:15px;fill:#ff0000">Declare</tspan></text>
216+ <text
217+ xml:space="preserve"
218+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
219+ x="117"
220+ y="344.36218"
221+ id="text5082"
222+ sodipodi:linespacing="125%"
223+ inkscape:export-xdpi="61.120499"
224+ inkscape:export-ydpi="61.120499"><tspan
225+ style="font-size:15px;fill:#0000ff"
226+ sodipodi:role="line"
227+ id="tspan5084"
228+ x="117"
229+ y="344.36218">name:TTName</tspan><tspan
230+ style="font-size:15px;fill:#0000ff"
231+ id="tspan5086"
232+ sodipodi:role="line"
233+ x="117"
234+ y="363.11218">arguments:List FunArg</tspan><tspan
235+ style="font-size:15px;fill:#0000ff"
236+ id="tspan5088"
237+ sodipodi:role="line"
238+ x="117"
239+ y="381.86218">returnType:Raw</tspan></text>
240+ <text
241+ xml:space="preserve"
242+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;"
243+ x="111"
244+ y="313.36218"
245+ id="text5095"
246+ sodipodi:linespacing="125%"
247+ inkscape:export-xdpi="61.120499"
248+ inkscape:export-ydpi="61.120499"><tspan
249+ style="font-size:15px;fill:#0000ff;"
250+ id="tspan5097"
251+ sodipodi:role="line"
252+ x="111"
253+ y="313.36218">TyDecl</tspan></text>
254+ <rect
255+ style="opacity:1;fill:none;fill-opacity:1;stroke:#0000ff;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
256+ id="rect5099"
257+ width="125"
258+ height="88"
259+ x="170"
260+ y="415.36218"
261+ inkscape:export-xdpi="61.120499"
262+ inkscape:export-ydpi="61.120499" />
263+ <path
264+ inkscape:connector-curvature="0"
265+ id="path5101"
266+ d="m 247,364.3622 0,48"
267+ style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow2Mend)"
268+ inkscape:export-xdpi="61.120499"
269+ inkscape:export-ydpi="61.120499" />
270+ <text
271+ xml:space="preserve"
272+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
273+ x="260"
274+ y="408.36218"
275+ id="text5103"
276+ sodipodi:linespacing="125%"
277+ inkscape:export-xdpi="61.120499"
278+ inkscape:export-ydpi="61.120499"><tspan
279+ style="font-size:15px;fill:#ff0000"
280+ id="tspan5105"
281+ sodipodi:role="line"
282+ x="260"
283+ y="408.36218">MkFunArg</tspan></text>
284+ <text
285+ sodipodi:linespacing="125%"
286+ id="text5107"
287+ y="437.36218"
288+ x="174"
289+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
290+ xml:space="preserve"
291+ inkscape:export-xdpi="61.120499"
292+ inkscape:export-ydpi="61.120499"><tspan
293+ y="437.36218"
294+ x="174"
295+ id="tspan5109"
296+ sodipodi:role="line"
297+ style="font-size:15px;fill:#0000ff">name:TTName</tspan><tspan
298+ y="456.11218"
299+ x="174"
300+ sodipodi:role="line"
301+ id="tspan5113"
302+ style="font-size:15px;fill:#0000ff">type:Raw</tspan><tspan
303+ y="474.86218"
304+ x="174"
305+ sodipodi:role="line"
306+ style="font-size:15px;fill:#0000ff"
307+ id="tspan5121">plicity:Plicity</tspan><tspan
308+ y="493.61218"
309+ x="174"
310+ sodipodi:role="line"
311+ style="font-size:15px;fill:#0000ff"
312+ id="tspan5123">erasure:Erasure</tspan></text>
313+ <text
314+ sodipodi:linespacing="125%"
315+ id="text5115"
316+ y="409.36218"
317+ x="170"
318+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
319+ xml:space="preserve"
320+ inkscape:export-xdpi="61.120499"
321+ inkscape:export-ydpi="61.120499"><tspan
322+ y="409.36218"
323+ x="170"
324+ sodipodi:role="line"
325+ id="tspan5117"
326+ style="font-size:15px;fill:#0000ff">FunArg</tspan></text>
327+ <text
328+ sodipodi:linespacing="125%"
329+ id="text5125"
330+ y="526.36218"
331+ x="105"
332+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
333+ xml:space="preserve"
334+ inkscape:export-xdpi="61.120499"
335+ inkscape:export-ydpi="61.120499"><tspan
336+ y="526.36218"
337+ x="105"
338+ sodipodi:role="line"
339+ id="tspan5127"
340+ style="font-size:15px;fill:#ff0000">Explicit</tspan><tspan
341+ y="545.11218"
342+ x="105"
343+ sodipodi:role="line"
344+ style="font-size:15px;fill:#ff0000"
345+ id="tspan5129">Implicit</tspan><tspan
346+ y="563.86218"
347+ x="105"
348+ sodipodi:role="line"
349+ style="font-size:15px;fill:#ff0000"
350+ id="tspan5131">Constraint</tspan></text>
351+ <path
352+ inkscape:connector-curvature="0"
353+ id="path5161"
354+ d="m 169,473.3622 c -30.23945,2.9603 -39.98191,17.10078 -41,36"
355+ style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker5163)"
356+ sodipodi:nodetypes="cc"
357+ inkscape:export-xdpi="61.120499"
358+ inkscape:export-ydpi="61.120499" />
359+ <path
360+ style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker6325)"
361+ d="m 245,499.3622 0,28"
362+ id="path6319"
363+ inkscape:connector-curvature="0"
364+ sodipodi:nodetypes="cc"
365+ inkscape:export-xdpi="61.120499"
366+ inkscape:export-ydpi="61.120499" />
367+ <text
368+ sodipodi:linespacing="125%"
369+ id="text6321"
370+ y="544.36218"
371+ x="221"
372+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
373+ xml:space="preserve"
374+ inkscape:export-xdpi="61.120499"
375+ inkscape:export-ydpi="61.120499"><tspan
376+ y="544.36218"
377+ x="221"
378+ sodipodi:role="line"
379+ id="tspan6323"
380+ style="font-size:15px;fill:#ff0000">Erased</tspan><tspan
381+ y="563.11218"
382+ x="221"
383+ sodipodi:role="line"
384+ style="font-size:15px;fill:#ff0000"
385+ id="tspan6773">NotErased</tspan></text>
386+ <rect
387+ style="opacity:1;fill:none;fill-opacity:1;stroke:#0000ff;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
388+ id="rect6775"
389+ width="247"
390+ height="49"
391+ x="347"
392+ y="322.36218"
393+ inkscape:export-xdpi="61.120499"
394+ inkscape:export-ydpi="61.120499" />
395+ <path
396+ inkscape:connector-curvature="0"
397+ id="path6777"
398+ d="m 458,271.3622 0,48"
399+ style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker5133)"
400+ inkscape:export-xdpi="61.120499"
401+ inkscape:export-ydpi="61.120499" />
402+ <text
403+ xml:space="preserve"
404+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
405+ x="469"
406+ y="295.36218"
407+ id="text6779"
408+ sodipodi:linespacing="125%"
409+ inkscape:export-xdpi="61.120499"
410+ inkscape:export-ydpi="61.120499"><tspan
411+ style="font-size:15px;fill:#ff0000"
412+ id="tspan6781"
413+ sodipodi:role="line"
414+ x="469"
415+ y="295.36218">DefineDatatype</tspan></text>
416+ <text
417+ sodipodi:linespacing="125%"
418+ id="text6783"
419+ y="344.36218"
420+ x="351"
421+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
422+ xml:space="preserve"
423+ inkscape:export-xdpi="61.120499"
424+ inkscape:export-ydpi="61.120499"><tspan
425+ y="344.36218"
426+ x="351"
427+ sodipodi:role="line"
428+ id="tspan6789"
429+ style="font-size:15px;fill:#0000ff">name:TTName</tspan><tspan
430+ y="363.11218"
431+ x="351"
432+ sodipodi:role="line"
433+ style="font-size:15px;fill:#0000ff"
434+ id="tspan7130">constructors : List ConstructorDefn</tspan></text>
435+ <text
436+ sodipodi:linespacing="125%"
437+ id="text6791"
438+ y="313.36218"
439+ x="379"
440+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
441+ xml:space="preserve"
442+ inkscape:export-xdpi="61.120499"
443+ inkscape:export-ydpi="61.120499"><tspan
444+ y="313.36218"
445+ x="379"
446+ sodipodi:role="line"
447+ id="tspan6793"
448+ style="font-size:15px;fill:#0000ff">DataDefn</tspan></text>
449+ <rect
450+ style="opacity:1;fill:none;fill-opacity:1;stroke:#0000ff;stroke-width:2;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
451+ id="rect6799"
452+ width="201"
453+ height="69"
454+ x="380"
455+ y="418.36218"
456+ inkscape:export-xdpi="61.120499"
457+ inkscape:export-ydpi="61.120499" />
458+ <path
459+ inkscape:connector-curvature="0"
460+ id="path6801"
461+ d="m 539,367.3622 0,48"
462+ style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker6819)"
463+ inkscape:export-xdpi="61.120499"
464+ inkscape:export-ydpi="61.120499" />
465+ <text
466+ xml:space="preserve"
467+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
468+ x="450"
469+ y="386.36218"
470+ id="text6803"
471+ sodipodi:linespacing="125%"
472+ inkscape:export-xdpi="61.120499"
473+ inkscape:export-ydpi="61.120499"><tspan
474+ style="font-size:15px;fill:#ff0000"
475+ id="tspan6805"
476+ sodipodi:role="line"
477+ x="450"
478+ y="386.36218">Constructor</tspan></text>
479+ <text
480+ sodipodi:linespacing="125%"
481+ id="text6807"
482+ y="440.36218"
483+ x="384"
484+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
485+ xml:space="preserve"
486+ inkscape:export-xdpi="61.120499"
487+ inkscape:export-ydpi="61.120499"><tspan
488+ y="440.36218"
489+ x="384"
490+ id="tspan6809"
491+ sodipodi:role="line"
492+ style="font-size:15px;fill:#0000ff">name:TTName</tspan><tspan
493+ y="459.11218"
494+ x="384"
495+ sodipodi:role="line"
496+ id="tspan6811"
497+ style="font-size:15px;fill:#0000ff">arguments:List FunArg</tspan><tspan
498+ y="477.86218"
499+ x="384"
500+ sodipodi:role="line"
501+ id="tspan6813"
502+ style="font-size:15px;fill:#0000ff">returnType:Raw</tspan></text>
503+ <text
504+ sodipodi:linespacing="125%"
505+ id="text6815"
506+ y="409.36218"
507+ x="378"
508+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
509+ xml:space="preserve"
510+ inkscape:export-xdpi="61.120499"
511+ inkscape:export-ydpi="61.120499"><tspan
512+ y="409.36218"
513+ x="378"
514+ sodipodi:role="line"
515+ id="tspan6817"
516+ style="font-size:15px;fill:#0000ff">ConstructorDefn</tspan></text>
517+ <text
518+ inkscape:export-ydpi="61.120499"
519+ inkscape:export-xdpi="61.120499"
520+ sodipodi:linespacing="125%"
521+ id="text7135"
522+ y="425.36218"
523+ x="307"
524+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:20px;line-height:125%;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';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"
525+ xml:space="preserve"><tspan
526+ y="425.36218"
527+ x="307"
528+ sodipodi:role="line"
529+ id="tspan7137"
530+ style="font-size:15px;fill:#ff0000">MkFunArg</tspan></text>
531+ <path
532+ inkscape:export-ydpi="61.120499"
533+ inkscape:export-xdpi="61.120499"
534+ style="fill:none;fill-rule:evenodd;stroke:#ff0000;stroke-width:2;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker7147)"
535+ d="m 379,458.3622 -80,-35"
536+ id="path7145"
537+ inkscape:connector-curvature="0"
538+ sodipodi:nodetypes="cc" />
539+ </g>
540+</svg>
docs/proofs/generatingData.rst+29−6
@@ -1,11 +1,29 @@
1−Generating Data and Functions at Compile Time
1+Generating Datatypes and Functions at Compile Time
2−=============================================
2+==================================================
3
3
4−We can construct a datatype at compile-time in an Elab monad.
4+Program elements, such as datatypes and functions can be constructed at compile-time in the Elab monad.
5This can allow proofs to be generated for user defined types or it could allow types to be automatically generated to support user defined types.
5This can allow proofs to be generated for user defined types or it could allow types to be automatically generated to support user defined types.
6An example is the code, from `Elaborator reflection: extending Idris in Idris`_, that automatically generates accessibility predicates using the Bove-Capretta method.
6An example is the code, from `Elaborator reflection: extending Idris in Idris`_, that automatically generates accessibility predicates using the Bove-Capretta method.
7
7
8+Generating Datatypes
9+--------------------
10+
11+There are two main 'tactics' associated with generating datatypes:
12+
13+- declareDatatype
14+- defineDatatype
15+
16+Which declare and define the datatype as the names suggest.
17+
18+.. list-table::
19+
20+ * - These 'tactics' and the data structures associated with them are listed in the tables later on this page, for now, here is a summary:
21+ - .. image:: ../image/generateDatatype.png
22+ :width: 332px
23+ :height: 246px
24+ :alt: diagram illustrating data structures associated with declareDatatype defineDatatype.
25+
8−Here is a simple example constucting a boolean type:
26+Here is a simple example constructing a boolean type:
9
27
10.. code-block:: idris
28.. code-block:: idris
11
29
@@ -24,7 +42,7 @@ Here is a simple example constucting a boolean type:
24
42
25.. list-table::
43.. list-table::
26
44
27− * - This type is now availible to us as if we had compiled it in the usual way:
45+ * - This type is now available to us as if we had compiled it in the usual way:
28 - .. code-block:: idris
46 - .. code-block:: idris
29
47
30 λΠ> :printdef Two
48 λΠ> :printdef Two
@@ -40,7 +58,10 @@ Here is a simple example constucting a boolean type:
40 λΠ> T
58 λΠ> T
41 T : Two
59 T : Two
42
60
61+Generating Functions
62+--------------------
63+
43−We can now add some function definitions to the above code:
64+We can now add some function definitions to the above datatype:
44
65
45.. code-block:: idris
66.. code-block:: idris
46
67
@@ -289,6 +310,8 @@ The above functions use the following data/records:
289 ||| fully-qualified, and it must have been previously declared as a
310 ||| fully-qualified, and it must have been previously declared as a
290 ||| datatype.
311 ||| datatype.
291 name : TTName
312 name : TTName
313+ ||| A list of constructors for the datatype.
314+ constructors : List ConstructorDefn
292
315
293 * - CtorArg
316 * - CtorArg
294 - CtorParameter
317 - CtorParameter