-
Notifications
You must be signed in to change notification settings - Fork 4
/
V1.AST.html
87 lines (67 loc) · 16 KB
/
V1.AST.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>V1.AST</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- Agda definition of C-- abstract syntax trees</a>
<a id="49" class="Comment">-- and Haskell bindings to the ones generated by the parser.</a>
<a id="111" class="Keyword">module</a> <a id="118" href="V1.AST.html" class="Module">V1.AST</a> <a id="125" class="Keyword">where</a>
<a id="132" class="Keyword">open</a> <a id="137" class="Keyword">import</a> <a id="144" href="Library.html" class="Module">Library</a>
<a id="153" class="Symbol">{-#</a> <a id="157" class="Keyword">FOREIGN</a> <a id="165" class="Pragma">GHC</a> <a id="169" class="Pragma">import</a> <a id="176" class="Pragma">qualified</a> <a id="186" class="Pragma">Data.Text</a> <a id="196" class="Symbol">#-}</a>
<a id="200" class="Symbol">{-#</a> <a id="204" class="Keyword">FOREIGN</a> <a id="212" class="Pragma">GHC</a> <a id="216" class="Pragma">import</a> <a id="223" class="Pragma">While.Abs</a> <a id="233" class="Symbol">#-}</a>
<a id="237" class="Symbol">{-#</a> <a id="241" class="Keyword">FOREIGN</a> <a id="249" class="Pragma">GHC</a> <a id="253" class="Pragma">import</a> <a id="260" class="Pragma">While.Print</a> <a id="272" class="Symbol">#-}</a>
<a id="277" class="Keyword">data</a> <a id="Type"></a><a id="282" href="V1.AST.html#282" class="Datatype">Type</a> <a id="287" class="Symbol">:</a> <a id="289" class="PrimitiveType">Set</a> <a id="293" class="Keyword">where</a>
<a id="Type.bool"></a><a id="301" href="V1.AST.html#301" class="InductiveConstructor">bool</a> <a id="Type.int"></a><a id="306" href="V1.AST.html#306" class="InductiveConstructor">int</a> <a id="310" class="Symbol">:</a> <a id="312" href="V1.AST.html#282" class="Datatype">Type</a>
<a id="318" class="Symbol">{-#</a> <a id="322" class="Keyword">COMPILE</a> <a id="330" class="Pragma">GHC</a> <a id="334" href="V1.AST.html#282" class="Datatype">Type</a> <a id="339" class="Pragma">=</a> <a id="341" class="Pragma">data</a> <a id="346" class="Pragma">Type</a>
<a id="353" class="Pragma">(</a> <a id="355" class="Pragma">TBool</a>
<a id="363" class="Pragma">|</a> <a id="365" class="Pragma">TInt</a>
<a id="372" class="Pragma">)</a> <a id="374" class="Symbol">#-}</a>
<a id="379" class="Keyword">data</a> <a id="Boolean"></a><a id="384" href="V1.AST.html#384" class="Datatype">Boolean</a> <a id="392" class="Symbol">:</a> <a id="394" class="PrimitiveType">Set</a> <a id="398" class="Keyword">where</a>
<a id="Boolean.true"></a><a id="406" href="V1.AST.html#406" class="InductiveConstructor">true</a> <a id="Boolean.false"></a><a id="411" href="V1.AST.html#411" class="InductiveConstructor">false</a> <a id="417" class="Symbol">:</a> <a id="419" href="V1.AST.html#384" class="Datatype">Boolean</a>
<a id="428" class="Symbol">{-#</a> <a id="432" class="Keyword">COMPILE</a> <a id="440" class="Pragma">GHC</a> <a id="444" href="V1.AST.html#384" class="Datatype">Boolean</a> <a id="452" class="Pragma">=</a> <a id="454" class="Pragma">data</a> <a id="459" class="Pragma">Boolean</a> <a id="467" class="Pragma">(BTrue</a> <a id="474" class="Pragma">|</a> <a id="476" class="Pragma">BFalse)</a> <a id="484" class="Symbol">#-}</a>
<a id="489" class="Keyword">data</a> <a id="Exp"></a><a id="494" href="V1.AST.html#494" class="Datatype">Exp</a> <a id="498" class="Symbol">:</a> <a id="500" class="PrimitiveType">Set</a> <a id="504" class="Keyword">where</a>
<a id="Exp.eInt"></a><a id="512" href="V1.AST.html#512" class="InductiveConstructor">eInt</a> <a id="519" class="Symbol">:</a> <a id="521" class="Symbol">(</a><a id="522" href="V1.AST.html#522" class="Bound">i</a> <a id="524" class="Symbol">:</a> <a id="526" href="Agda.Builtin.Int.html#219" class="Datatype">ℤ</a><a id="527" class="Symbol">)</a> <a id="538" class="Symbol">→</a> <a id="540" href="V1.AST.html#494" class="Datatype">Exp</a>
<a id="Exp.eBool"></a><a id="546" href="V1.AST.html#546" class="InductiveConstructor">eBool</a> <a id="553" class="Symbol">:</a> <a id="555" class="Symbol">(</a><a id="556" href="V1.AST.html#556" class="Bound">b</a> <a id="558" class="Symbol">:</a> <a id="560" href="V1.AST.html#384" class="Datatype">Boolean</a><a id="567" class="Symbol">)</a> <a id="572" class="Symbol">→</a> <a id="574" href="V1.AST.html#494" class="Datatype">Exp</a>
<a id="Exp.ePlus"></a><a id="580" href="V1.AST.html#580" class="InductiveConstructor">ePlus</a> <a id="587" class="Symbol">:</a> <a id="589" class="Symbol">(</a><a id="590" href="V1.AST.html#590" class="Bound">e</a> <a id="592" href="V1.AST.html#592" class="Bound">e'</a> <a id="595" class="Symbol">:</a> <a id="597" href="V1.AST.html#494" class="Datatype">Exp</a><a id="600" class="Symbol">)</a> <a id="606" class="Symbol">→</a> <a id="608" href="V1.AST.html#494" class="Datatype">Exp</a>
<a id="Exp.eGt"></a><a id="614" href="V1.AST.html#614" class="InductiveConstructor">eGt</a> <a id="621" class="Symbol">:</a> <a id="623" class="Symbol">(</a><a id="624" href="V1.AST.html#624" class="Bound">e</a> <a id="626" href="V1.AST.html#626" class="Bound">e'</a> <a id="629" class="Symbol">:</a> <a id="631" href="V1.AST.html#494" class="Datatype">Exp</a><a id="634" class="Symbol">)</a> <a id="640" class="Symbol">→</a> <a id="642" href="V1.AST.html#494" class="Datatype">Exp</a>
<a id="Exp.eAnd"></a><a id="648" href="V1.AST.html#648" class="InductiveConstructor">eAnd</a> <a id="655" class="Symbol">:</a> <a id="657" class="Symbol">(</a><a id="658" href="V1.AST.html#658" class="Bound">e</a> <a id="660" href="V1.AST.html#660" class="Bound">e'</a> <a id="663" class="Symbol">:</a> <a id="665" href="V1.AST.html#494" class="Datatype">Exp</a><a id="668" class="Symbol">)</a> <a id="674" class="Symbol">→</a> <a id="676" href="V1.AST.html#494" class="Datatype">Exp</a>
<a id="Exp.eCond"></a><a id="682" href="V1.AST.html#682" class="InductiveConstructor">eCond</a> <a id="689" class="Symbol">:</a> <a id="691" class="Symbol">(</a><a id="692" href="V1.AST.html#692" class="Bound">e</a> <a id="694" href="V1.AST.html#694" class="Bound">e'</a> <a id="697" href="V1.AST.html#697" class="Bound">e''</a> <a id="701" class="Symbol">:</a> <a id="703" href="V1.AST.html#494" class="Datatype">Exp</a><a id="706" class="Symbol">)</a> <a id="708" class="Symbol">→</a> <a id="710" href="V1.AST.html#494" class="Datatype">Exp</a>
<a id="715" class="Symbol">{-#</a> <a id="719" class="Keyword">COMPILE</a> <a id="727" class="Pragma">GHC</a> <a id="731" href="V1.AST.html#494" class="Datatype">Exp</a> <a id="735" class="Pragma">=</a> <a id="737" class="Pragma">data</a> <a id="742" class="Pragma">Exp</a>
<a id="748" class="Pragma">(</a> <a id="750" class="Pragma">EInt</a>
<a id="757" class="Pragma">|</a> <a id="759" class="Pragma">EBool</a>
<a id="767" class="Pragma">|</a> <a id="769" class="Pragma">EPlus</a>
<a id="777" class="Pragma">|</a> <a id="779" class="Pragma">EGt</a>
<a id="785" class="Pragma">|</a> <a id="787" class="Pragma">EAnd</a>
<a id="794" class="Pragma">|</a> <a id="796" class="Pragma">ECond</a>
<a id="804" class="Pragma">)</a> <a id="806" class="Symbol">#-}</a>
<a id="811" class="Keyword">record</a> <a id="Program"></a><a id="818" href="V1.AST.html#818" class="Record">Program</a> <a id="826" class="Symbol">:</a> <a id="828" class="PrimitiveType">Set</a> <a id="832" class="Keyword">where</a>
<a id="840" class="Keyword">constructor</a> <a id="Program.program"></a><a id="852" href="V1.AST.html#852" class="InductiveConstructor">program</a>
<a id="862" class="Keyword">field</a>
<a id="Program.theMain"></a><a id="872" href="V1.AST.html#872" class="Field">theMain</a> <a id="881" class="Symbol">:</a> <a id="883" href="V1.AST.html#494" class="Datatype">Exp</a>
<a id="887" class="Keyword">open</a> <a id="892" href="V1.AST.html#818" class="Module">Program</a> <a id="900" class="Keyword">public</a>
<a id="908" class="Symbol">{-#</a> <a id="912" class="Keyword">COMPILE</a> <a id="920" class="Pragma">GHC</a> <a id="924" href="V1.AST.html#818" class="Record">Program</a> <a id="932" class="Pragma">=</a> <a id="934" class="Pragma">data</a> <a id="939" class="Pragma">Program</a> <a id="947" class="Pragma">(Prg)</a> <a id="953" class="Symbol">#-}</a>
<a id="958" class="Comment">-- Pretty printer</a>
<a id="977" class="Keyword">private</a>
<a id="987" class="Keyword">postulate</a>
<a id="printType"></a><a id="1001" href="V1.AST.html#1001" class="Postulate">printType</a> <a id="1014" class="Symbol">:</a> <a id="1016" href="V1.AST.html#282" class="Datatype">Type</a> <a id="1024" class="Symbol">→</a> <a id="1026" href="Agda.Builtin.String.html#247" class="Postulate">String</a>
<a id="printBoolean"></a><a id="1037" href="V1.AST.html#1037" class="Postulate">printBoolean</a> <a id="1050" class="Symbol">:</a> <a id="1052" href="V1.AST.html#384" class="Datatype">Boolean</a> <a id="1060" class="Symbol">→</a> <a id="1062" href="Agda.Builtin.String.html#247" class="Postulate">String</a>
<a id="printExp"></a><a id="1073" href="V1.AST.html#1073" class="Postulate">printExp</a> <a id="1086" class="Symbol">:</a> <a id="1088" href="V1.AST.html#494" class="Datatype">Exp</a> <a id="1096" class="Symbol">→</a> <a id="1098" href="Agda.Builtin.String.html#247" class="Postulate">String</a>
<a id="printProgram"></a><a id="1109" href="V1.AST.html#1109" class="Postulate">printProgram</a> <a id="1122" class="Symbol">:</a> <a id="1124" href="V1.AST.html#818" class="Record">Program</a> <a id="1132" class="Symbol">→</a> <a id="1134" href="Agda.Builtin.String.html#247" class="Postulate">String</a>
<a id="1142" class="Symbol">{-#</a> <a id="1146" class="Keyword">COMPILE</a> <a id="1154" class="Pragma">GHC</a> <a id="1158" href="V1.AST.html#1001" class="Postulate">printType</a> <a id="1171" class="Pragma">=</a> <a id="1173" class="Pragma">\</a> <a id="1175" class="Pragma">t</a> <a id="1177" class="Pragma">-></a> <a id="1180" class="Pragma">Data.Text.pack</a> <a id="1195" class="Pragma">(printTree</a> <a id="1206" class="Pragma">(t</a> <a id="1209" class="Pragma">::</a> <a id="1212" class="Pragma">Type))</a> <a id="1222" class="Symbol">#-}</a>
<a id="1226" class="Symbol">{-#</a> <a id="1230" class="Keyword">COMPILE</a> <a id="1238" class="Pragma">GHC</a> <a id="1242" href="V1.AST.html#1037" class="Postulate">printBoolean</a> <a id="1255" class="Pragma">=</a> <a id="1257" class="Pragma">\</a> <a id="1259" class="Pragma">b</a> <a id="1261" class="Pragma">-></a> <a id="1264" class="Pragma">Data.Text.pack</a> <a id="1279" class="Pragma">(printTree</a> <a id="1290" class="Pragma">(b</a> <a id="1293" class="Pragma">::</a> <a id="1296" class="Pragma">Boolean))</a> <a id="1306" class="Symbol">#-}</a>
<a id="1310" class="Symbol">{-#</a> <a id="1314" class="Keyword">COMPILE</a> <a id="1322" class="Pragma">GHC</a> <a id="1326" href="V1.AST.html#1073" class="Postulate">printExp</a> <a id="1339" class="Pragma">=</a> <a id="1341" class="Pragma">\</a> <a id="1343" class="Pragma">e</a> <a id="1345" class="Pragma">-></a> <a id="1348" class="Pragma">Data.Text.pack</a> <a id="1363" class="Pragma">(printTree</a> <a id="1374" class="Pragma">(e</a> <a id="1377" class="Pragma">::</a> <a id="1380" class="Pragma">Exp))</a> <a id="1390" class="Symbol">#-}</a>
<a id="1394" class="Symbol">{-#</a> <a id="1398" class="Keyword">COMPILE</a> <a id="1406" class="Pragma">GHC</a> <a id="1410" href="V1.AST.html#1109" class="Postulate">printProgram</a> <a id="1423" class="Pragma">=</a> <a id="1425" class="Pragma">\</a> <a id="1427" class="Pragma">p</a> <a id="1429" class="Pragma">-></a> <a id="1432" class="Pragma">Data.Text.pack</a> <a id="1447" class="Pragma">(printTree</a> <a id="1458" class="Pragma">(p</a> <a id="1461" class="Pragma">::</a> <a id="1464" class="Pragma">Program))</a> <a id="1474" class="Symbol">#-}</a>
<a id="1479" class="Keyword">instance</a>
<a id="PrintType"></a><a id="1490" href="V1.AST.html#1490" class="Function">PrintType</a> <a id="1500" class="Symbol">:</a> <a id="1502" href="Library.Print.html#196" class="Record">Print</a> <a id="1508" href="V1.AST.html#282" class="Datatype">Type</a>
<a id="1515" href="Library.Print.html#244" class="Field">print</a> <a id="1521" class="Symbol">{{</a><a id="1523" href="V1.AST.html#1490" class="Function">PrintType</a><a id="1532" class="Symbol">}}</a> <a id="1535" class="Symbol">=</a> <a id="1537" href="V1.AST.html#1001" class="Postulate">printType</a>
<a id="PrintBoolean"></a><a id="1550" href="V1.AST.html#1550" class="Function">PrintBoolean</a> <a id="1563" class="Symbol">:</a> <a id="1565" href="Library.Print.html#196" class="Record">Print</a> <a id="1571" href="V1.AST.html#384" class="Datatype">Boolean</a>
<a id="1581" href="Library.Print.html#244" class="Field">print</a> <a id="1587" class="Symbol">{{</a><a id="1589" href="V1.AST.html#1550" class="Function">PrintBoolean</a><a id="1601" class="Symbol">}}</a> <a id="1604" class="Symbol">=</a> <a id="1606" href="V1.AST.html#1037" class="Postulate">printBoolean</a>
<a id="PrintExp"></a><a id="1622" href="V1.AST.html#1622" class="Function">PrintExp</a> <a id="1631" class="Symbol">:</a> <a id="1633" href="Library.Print.html#196" class="Record">Print</a> <a id="1639" href="V1.AST.html#494" class="Datatype">Exp</a>
<a id="1645" href="Library.Print.html#244" class="Field">print</a> <a id="1651" class="Symbol">{{</a><a id="1653" href="V1.AST.html#1622" class="Function">PrintExp</a><a id="1661" class="Symbol">}}</a> <a id="1664" class="Symbol">=</a> <a id="1666" href="V1.AST.html#1073" class="Postulate">printExp</a>
<a id="PrintProgram"></a><a id="1678" href="V1.AST.html#1678" class="Function">PrintProgram</a> <a id="1691" class="Symbol">:</a> <a id="1693" href="Library.Print.html#196" class="Record">Print</a> <a id="1699" href="V1.AST.html#818" class="Record">Program</a>
<a id="1709" href="Library.Print.html#244" class="Field">print</a> <a id="1715" class="Symbol">{{</a><a id="1717" href="V1.AST.html#1678" class="Function">PrintProgram</a><a id="1729" class="Symbol">}}</a> <a id="1732" class="Symbol">=</a> <a id="1734" href="V1.AST.html#1109" class="Postulate">printProgram</a>
<a id="1748" class="Comment">-- Eq instance</a>
<a id="1764" class="Keyword">instance</a>
<a id="EqType"></a><a id="1775" href="V1.AST.html#1775" class="Function">EqType</a> <a id="1782" class="Symbol">:</a> <a id="1784" href="Library.Eq.html#610" class="Record">Eq</a> <a id="1787" href="V1.AST.html#282" class="Datatype">Type</a>
<a id="1794" href="Library.Eq.html#655" class="Field Operator">_≟_</a> <a id="1798" class="Symbol">{{</a><a id="1800" href="V1.AST.html#1775" class="Function">EqType</a><a id="1806" class="Symbol">}}</a> <a id="1809" class="Symbol">=</a> <a id="1811" class="Symbol">λ</a> <a id="1813" class="Keyword">where</a>
<a id="1823" href="V1.AST.html#301" class="InductiveConstructor">bool</a> <a id="1828" href="V1.AST.html#301" class="InductiveConstructor">bool</a> <a id="1833" class="Symbol">→</a> <a id="1835" href="Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="1839" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
<a id="1848" href="V1.AST.html#301" class="InductiveConstructor">bool</a> <a id="1853" href="V1.AST.html#306" class="InductiveConstructor">int</a> <a id="1858" class="Symbol">→</a> <a id="1860" href="Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="1863" class="Symbol">λ</a> <a id="1865" class="Symbol">()</a>
<a id="1872" href="V1.AST.html#306" class="InductiveConstructor">int</a> <a id="1877" href="V1.AST.html#301" class="InductiveConstructor">bool</a> <a id="1882" class="Symbol">→</a> <a id="1884" href="Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="1887" class="Symbol">λ</a> <a id="1889" class="Symbol">()</a>
<a id="1896" href="V1.AST.html#306" class="InductiveConstructor">int</a> <a id="1901" href="V1.AST.html#306" class="InductiveConstructor">int</a> <a id="1906" class="Symbol">→</a> <a id="1908" href="Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="1912" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
</pre></body></html>