-
Notifications
You must be signed in to change notification settings - Fork 4
/
V1.TypeChecker.html
86 lines (65 loc) · 20.4 KB
/
V1.TypeChecker.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
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>V1.TypeChecker</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- Type checker for the WHILE language.</a>
<a id="42" class="Symbol">{-#</a> <a id="46" class="Keyword">OPTIONS</a> <a id="54" class="Pragma">--postfix-projections</a> <a id="76" class="Symbol">#-}</a>
<a id="81" class="Keyword">module</a> <a id="88" href="V1.TypeChecker.html" class="Module">V1.TypeChecker</a> <a id="103" class="Keyword">where</a>
<a id="110" class="Keyword">open</a> <a id="115" class="Keyword">import</a> <a id="122" href="Library.html" class="Module">Library</a>
<a id="131" class="Keyword">import</a> <a id="138" href="V1.AST.html" class="Module">V1.AST</a> <a id="145" class="Symbol">as</a> <a id="148" class="Module">A</a>
<a id="150" class="Keyword">open</a> <a id="155" class="Keyword">import</a> <a id="162" href="V1.WellTypedSyntax.html" class="Module">V1.WellTypedSyntax</a>
<a id="182" class="Comment">-- Type errors.</a>
<a id="198" class="Comment">--</a>
<a id="201" class="Comment">-- Currently, these errors do not carry enough evidence that</a>
<a id="262" class="Comment">-- something is wrong. The type checker does not produce</a>
<a id="320" class="Comment">-- evidence of ill-typedness in case of failure,</a>
<a id="369" class="Comment">-- only of well-typedness in case of success.</a>
<a id="416" class="Keyword">data</a> <a id="TypeError"></a><a id="421" href="V1.TypeChecker.html#421" class="Datatype">TypeError</a> <a id="431" class="Symbol">:</a> <a id="433" class="PrimitiveType">Set</a> <a id="437" class="Keyword">where</a>
<a id="TypeError.typeMismatch"></a><a id="445" href="V1.TypeChecker.html#445" class="InductiveConstructor">typeMismatch</a> <a id="458" class="Symbol">:</a> <a id="460" class="Symbol">(</a><a id="461" href="V1.TypeChecker.html#461" class="Bound">tinf</a> <a id="466" href="V1.TypeChecker.html#466" class="Bound">texp</a> <a id="471" class="Symbol">:</a> <a id="473" href="V1.AST.html#282" class="Datatype">Type</a><a id="477" class="Symbol">)</a> <a id="480" class="Symbol">→</a> <a id="482" href="V1.TypeChecker.html#461" class="Bound">tinf</a> <a id="487" href="Relation.Binary.PropositionalEquality.Core.html#799" class="Function Operator">≢</a> <a id="489" href="V1.TypeChecker.html#466" class="Bound">texp</a> <a id="494" class="Symbol">→</a> <a id="496" href="V1.TypeChecker.html#421" class="Datatype">TypeError</a>
<a id="507" class="Keyword">instance</a>
<a id="PrintError"></a><a id="518" href="V1.TypeChecker.html#518" class="Function">PrintError</a> <a id="529" class="Symbol">:</a> <a id="531" href="Library.Print.html#196" class="Record">Print</a> <a id="537" href="V1.TypeChecker.html#421" class="Datatype">TypeError</a>
<a id="549" href="Library.Print.html#244" class="Field">print</a> <a id="555" class="Symbol">{{</a><a id="557" href="V1.TypeChecker.html#518" class="Function">PrintError</a><a id="567" class="Symbol">}}</a> <a id="570" class="Symbol">=</a> <a id="572" class="Symbol">λ</a> <a id="574" class="Keyword">where</a>
<a id="584" class="Symbol">(</a><a id="585" href="V1.TypeChecker.html#445" class="InductiveConstructor">typeMismatch</a> <a id="598" href="V1.TypeChecker.html#598" class="Bound">tinf</a> <a id="603" href="V1.TypeChecker.html#603" class="Bound">texp</a> <a id="608" class="Symbol">_)</a> <a id="611" class="Symbol">→</a> <a id="613" href="Data.String.Base.html#1932" class="Function">String.concat</a> <a id="627" href="Function.html#1645" class="Function Operator">$</a>
<a id="635" class="String">"type mismatch: expected "</a> <a id="662" href="Agda.Builtin.List.html#173" class="InductiveConstructor Operator">∷</a> <a id="664" href="Library.Print.html#244" class="Field">print</a> <a id="670" href="V1.TypeChecker.html#603" class="Bound">texp</a> <a id="675" href="Agda.Builtin.List.html#173" class="InductiveConstructor Operator">∷</a>
<a id="683" class="String">", but inferred "</a> <a id="701" href="Agda.Builtin.List.html#173" class="InductiveConstructor Operator">∷</a> <a id="703" href="Library.Print.html#244" class="Field">print</a> <a id="709" href="V1.TypeChecker.html#598" class="Bound">tinf</a> <a id="714" href="Agda.Builtin.List.html#173" class="InductiveConstructor Operator">∷</a> <a id="716" href="Agda.Builtin.List.html#158" class="InductiveConstructor">[]</a>
<a id="720" class="Comment">-- Type error monad.</a>
<a id="742" class="Keyword">open</a> <a id="747" href="Library.Error.html#134" class="Module">ErrorMonad</a> <a id="758" class="Symbol">{</a><a id="759" class="Argument">E</a> <a id="761" class="Symbol">=</a> <a id="763" href="V1.TypeChecker.html#421" class="Datatype">TypeError</a><a id="772" class="Symbol">}</a>
<a id="775" class="Comment">-- Checking expressions</a>
<a id="799" class="Comment">---------------------------------------------------------------------------</a>
<a id="876" class="Keyword">mutual</a>
<a id="886" class="Comment">-- Type inference.</a>
<a id="inferExp"></a><a id="908" href="V1.TypeChecker.html#908" class="Function">inferExp</a> <a id="917" class="Symbol">:</a> <a id="919" class="Symbol">(</a><a id="920" href="V1.TypeChecker.html#920" class="Bound">e</a> <a id="922" class="Symbol">:</a> <a id="924" href="V1.AST.html#494" class="Datatype">A.Exp</a><a id="929" class="Symbol">)</a> <a id="931" class="Symbol">→</a> <a id="933" href="Library.Error.html#170" class="Function">Error</a> <a id="939" class="Symbol">(</a><a id="940" href="Agda.Builtin.Sigma.html#139" class="Record">Σ</a> <a id="942" href="V1.AST.html#282" class="Datatype">Type</a> <a id="947" class="Symbol">(λ</a> <a id="950" href="V1.TypeChecker.html#950" class="Bound">t</a> <a id="952" class="Symbol">→</a> <a id="954" href="V1.WellTypedSyntax.html#367" class="Datatype">Exp</a> <a id="958" href="V1.TypeChecker.html#950" class="Bound">t</a><a id="959" class="Symbol">))</a>
<a id="964" href="V1.TypeChecker.html#908" class="Function">inferExp</a> <a id="973" class="Symbol">(</a><a id="974" href="V1.AST.html#512" class="InductiveConstructor">A.eInt</a> <a id="981" href="V1.TypeChecker.html#981" class="Bound">i</a><a id="982" class="Symbol">)</a> <a id="985" class="Symbol">=</a> <a id="987" href="Library.Monad.html#1110" class="Function">return</a> <a id="994" class="Symbol">(</a><a id="995" href="V1.AST.html#306" class="InductiveConstructor">int</a> <a id="1000" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="1002" href="V1.WellTypedSyntax.html#407" class="InductiveConstructor">eInt</a> <a id="1008" href="V1.TypeChecker.html#981" class="Bound">i</a><a id="1009" class="Symbol">)</a>
<a id="1013" href="V1.TypeChecker.html#908" class="Function">inferExp</a> <a id="1022" class="Symbol">(</a><a id="1023" href="V1.AST.html#546" class="InductiveConstructor">A.eBool</a> <a id="1031" href="V1.TypeChecker.html#1031" class="Bound">b</a><a id="1032" class="Symbol">)</a> <a id="1034" class="Symbol">=</a> <a id="1036" href="Library.Monad.html#1110" class="Function">return</a> <a id="1043" class="Symbol">(</a><a id="1044" href="V1.AST.html#301" class="InductiveConstructor">bool</a> <a id="1049" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="1051" href="V1.WellTypedSyntax.html#465" class="InductiveConstructor">eBool</a> <a id="1057" href="V1.TypeChecker.html#1031" class="Bound">b</a><a id="1058" class="Symbol">)</a>
<a id="1062" href="V1.TypeChecker.html#908" class="Function">inferExp</a> <a id="1071" class="Symbol">(</a><a id="1072" href="V1.AST.html#580" class="InductiveConstructor">A.ePlus</a> <a id="1080" href="V1.TypeChecker.html#1080" class="Bound">e₁</a> <a id="1083" href="V1.TypeChecker.html#1083" class="Bound">e₂</a><a id="1085" class="Symbol">)</a> <a id="1087" class="Symbol">=</a> <a id="1089" href="V1.TypeChecker.html#1674" class="Function">inferOp</a> <a id="1097" href="V1.WellTypedSyntax.html#249" class="InductiveConstructor">plus</a> <a id="1103" href="V1.TypeChecker.html#1080" class="Bound">e₁</a> <a id="1106" href="V1.TypeChecker.html#1083" class="Bound">e₂</a>
<a id="1111" href="V1.TypeChecker.html#908" class="Function">inferExp</a> <a id="1120" class="Symbol">(</a><a id="1121" href="V1.AST.html#614" class="InductiveConstructor">A.eGt</a> <a id="1129" href="V1.TypeChecker.html#1129" class="Bound">e₁</a> <a id="1132" href="V1.TypeChecker.html#1132" class="Bound">e₂</a><a id="1134" class="Symbol">)</a> <a id="1136" class="Symbol">=</a> <a id="1138" href="V1.TypeChecker.html#1674" class="Function">inferOp</a> <a id="1146" href="V1.WellTypedSyntax.html#271" class="InductiveConstructor">gt</a> <a id="1152" href="V1.TypeChecker.html#1129" class="Bound">e₁</a> <a id="1155" href="V1.TypeChecker.html#1132" class="Bound">e₂</a>
<a id="1160" href="V1.TypeChecker.html#908" class="Function">inferExp</a> <a id="1169" class="Symbol">(</a><a id="1170" href="V1.AST.html#648" class="InductiveConstructor">A.eAnd</a> <a id="1178" href="V1.TypeChecker.html#1178" class="Bound">e₁</a> <a id="1181" href="V1.TypeChecker.html#1181" class="Bound">e₂</a><a id="1183" class="Symbol">)</a> <a id="1185" class="Symbol">=</a> <a id="1187" href="V1.TypeChecker.html#1674" class="Function">inferOp</a> <a id="1195" href="V1.WellTypedSyntax.html#294" class="InductiveConstructor">and</a> <a id="1201" href="V1.TypeChecker.html#1178" class="Bound">e₁</a> <a id="1204" href="V1.TypeChecker.html#1181" class="Bound">e₂</a>
<a id="1209" href="V1.TypeChecker.html#908" class="Function">inferExp</a> <a id="1218" class="Symbol">(</a><a id="1219" href="V1.AST.html#682" class="InductiveConstructor">A.eCond</a> <a id="1227" href="V1.TypeChecker.html#1227" class="Bound">e₁</a> <a id="1230" href="V1.TypeChecker.html#1230" class="Bound">e₂</a> <a id="1233" href="V1.TypeChecker.html#1233" class="Bound">e₃</a><a id="1235" class="Symbol">)</a> <a id="1237" class="Symbol">=</a> <a id="1239" class="Keyword">do</a>
<a id="1246" href="V1.TypeChecker.html#1246" class="Bound">e₁'</a> <a id="1250" href="Library.Monad.html#1002" class="Field Operator">←</a> <a id="1252" href="V1.TypeChecker.html#1446" class="Function">checkExp</a> <a id="1261" href="V1.TypeChecker.html#1227" class="Bound">e₁</a> <a id="1264" href="V1.AST.html#301" class="InductiveConstructor">bool</a>
<a id="1273" class="Symbol">(</a><a id="1274" href="V1.TypeChecker.html#1274" class="Bound">t</a> <a id="1276" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="1278" href="V1.TypeChecker.html#1278" class="Bound">e₂'</a><a id="1281" class="Symbol">)</a> <a id="1283" href="Library.Monad.html#1002" class="Field Operator">←</a> <a id="1285" href="V1.TypeChecker.html#908" class="Function">inferExp</a> <a id="1294" href="V1.TypeChecker.html#1230" class="Bound">e₂</a>
<a id="1301" href="V1.TypeChecker.html#1301" class="Bound">e₃'</a> <a id="1305" href="Library.Monad.html#1002" class="Field Operator">←</a> <a id="1307" href="V1.TypeChecker.html#1446" class="Function">checkExp</a> <a id="1316" href="V1.TypeChecker.html#1233" class="Bound">e₃</a> <a id="1319" href="V1.TypeChecker.html#1274" class="Bound">t</a>
<a id="1325" href="Library.Monad.html#1110" class="Function">return</a> <a id="1332" class="Symbol">(</a><a id="1333" href="V1.TypeChecker.html#1274" class="Bound">t</a> <a id="1335" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="1337" href="V1.WellTypedSyntax.html#616" class="InductiveConstructor">eCond</a> <a id="1343" href="V1.TypeChecker.html#1246" class="Bound">e₁'</a> <a id="1347" href="V1.TypeChecker.html#1278" class="Bound">e₂'</a> <a id="1351" href="V1.TypeChecker.html#1301" class="Bound">e₃'</a><a id="1354" class="Symbol">)</a>
<a id="1359" class="Comment">-- Type checking.</a>
<a id="1379" class="Comment">-- Calls inference and checks inferred type against given type.</a>
<a id="checkExp"></a><a id="1446" href="V1.TypeChecker.html#1446" class="Function">checkExp</a> <a id="1455" class="Symbol">:</a> <a id="1457" class="Symbol">(</a><a id="1458" href="V1.TypeChecker.html#1458" class="Bound">e</a> <a id="1460" class="Symbol">:</a> <a id="1462" href="V1.AST.html#494" class="Datatype">A.Exp</a><a id="1467" class="Symbol">)</a> <a id="1469" class="Symbol">(</a><a id="1470" href="V1.TypeChecker.html#1470" class="Bound">t</a> <a id="1472" class="Symbol">:</a> <a id="1474" href="V1.AST.html#282" class="Datatype">Type</a><a id="1478" class="Symbol">)</a> <a id="1480" class="Symbol">→</a> <a id="1482" href="Library.Error.html#170" class="Function">Error</a> <a id="1488" class="Symbol">(</a><a id="1489" href="V1.WellTypedSyntax.html#367" class="Datatype">Exp</a> <a id="1493" href="V1.TypeChecker.html#1470" class="Bound">t</a><a id="1494" class="Symbol">)</a>
<a id="1498" href="V1.TypeChecker.html#1446" class="Function">checkExp</a> <a id="1507" href="V1.TypeChecker.html#1507" class="Bound">e</a> <a id="1509" href="V1.TypeChecker.html#1509" class="Bound">t</a> <a id="1511" class="Symbol">=</a> <a id="1513" class="Keyword">do</a>
<a id="1520" class="Symbol">(</a><a id="1521" href="V1.TypeChecker.html#1521" class="Bound">t'</a> <a id="1524" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="1526" href="V1.TypeChecker.html#1526" class="Bound">e'</a><a id="1528" class="Symbol">)</a> <a id="1530" href="Library.Monad.html#1002" class="Field Operator">←</a> <a id="1532" href="V1.TypeChecker.html#908" class="Function">inferExp</a> <a id="1541" href="V1.TypeChecker.html#1507" class="Bound">e</a>
<a id="1547" href="Function.html#3662" class="Function Operator">case</a> <a id="1552" href="V1.TypeChecker.html#1521" class="Bound">t'</a> <a id="1555" href="Library.Eq.html#655" class="Field Operator">≟</a> <a id="1557" href="V1.TypeChecker.html#1509" class="Bound">t</a> <a id="1559" href="Function.html#3662" class="Function Operator">of</a> <a id="1562" class="Symbol">λ</a> <a id="1564" class="Keyword">where</a>
<a id="1576" class="Symbol">(</a><a id="1577" href="Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="1581" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="1585" class="Symbol">)</a> <a id="1587" class="Symbol">→</a> <a id="1589" href="Library.Monad.html#1110" class="Function">return</a> <a id="1596" href="V1.TypeChecker.html#1526" class="Bound">e'</a>
<a id="1605" class="Symbol">(</a><a id="1606" href="Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="1610" href="V1.TypeChecker.html#1610" class="Bound">t'≢t</a><a id="1614" class="Symbol">)</a> <a id="1616" class="Symbol">→</a> <a id="1618" href="Library.Error.html#912" class="Function">throwError</a> <a id="1629" class="Symbol">(</a><a id="1630" href="V1.TypeChecker.html#445" class="InductiveConstructor">typeMismatch</a> <a id="1643" href="V1.TypeChecker.html#1521" class="Bound">t'</a> <a id="1646" href="V1.TypeChecker.html#1509" class="Bound">t</a> <a id="1648" href="V1.TypeChecker.html#1610" class="Bound">t'≢t</a><a id="1652" class="Symbol">)</a>
<a id="1657" class="Comment">-- Operators.</a>
<a id="inferOp"></a><a id="1674" href="V1.TypeChecker.html#1674" class="Function">inferOp</a> <a id="1682" class="Symbol">:</a> <a id="1684" class="Symbol">∀{</a><a id="1686" href="V1.TypeChecker.html#1686" class="Bound">t</a> <a id="1688" href="V1.TypeChecker.html#1688" class="Bound">t'</a><a id="1690" class="Symbol">}</a> <a id="1692" class="Symbol">(</a><a id="1693" href="V1.TypeChecker.html#1693" class="Bound">op</a> <a id="1696" class="Symbol">:</a> <a id="1698" href="V1.WellTypedSyntax.html#211" class="Datatype">Op</a> <a id="1701" href="V1.TypeChecker.html#1686" class="Bound">t</a> <a id="1703" href="V1.TypeChecker.html#1688" class="Bound">t'</a><a id="1705" class="Symbol">)</a> <a id="1707" class="Symbol">(</a><a id="1708" href="V1.TypeChecker.html#1708" class="Bound">e₁</a> <a id="1711" href="V1.TypeChecker.html#1711" class="Bound">e₂</a> <a id="1714" class="Symbol">:</a> <a id="1716" href="V1.AST.html#494" class="Datatype">A.Exp</a><a id="1721" class="Symbol">)</a> <a id="1723" class="Symbol">→</a> <a id="1725" href="Library.Error.html#170" class="Function">Error</a> <a id="1731" class="Symbol">(</a><a id="1732" href="Agda.Builtin.Sigma.html#139" class="Record">Σ</a> <a id="1734" href="V1.AST.html#282" class="Datatype">Type</a> <a id="1739" class="Symbol">(λ</a> <a id="1742" href="V1.TypeChecker.html#1742" class="Bound">t</a> <a id="1744" class="Symbol">→</a> <a id="1746" href="V1.WellTypedSyntax.html#367" class="Datatype">Exp</a> <a id="1750" href="V1.TypeChecker.html#1742" class="Bound">t</a><a id="1751" class="Symbol">))</a>
<a id="1756" href="V1.TypeChecker.html#1674" class="Function">inferOp</a> <a id="1764" class="Symbol">{</a><a id="1765" href="V1.TypeChecker.html#1765" class="Bound">t</a><a id="1766" class="Symbol">}</a> <a id="1768" class="Symbol">{</a><a id="1769" href="V1.TypeChecker.html#1769" class="Bound">t'</a><a id="1771" class="Symbol">}</a> <a id="1773" href="V1.TypeChecker.html#1773" class="Bound">op</a> <a id="1776" href="V1.TypeChecker.html#1776" class="Bound">e₁</a> <a id="1779" href="V1.TypeChecker.html#1779" class="Bound">e₂</a> <a id="1782" class="Symbol">=</a> <a id="1784" class="Keyword">do</a>
<a id="1791" href="V1.TypeChecker.html#1791" class="Bound">e₁'</a> <a id="1795" href="Library.Monad.html#1002" class="Field Operator">←</a> <a id="1797" href="V1.TypeChecker.html#1446" class="Function">checkExp</a> <a id="1806" href="V1.TypeChecker.html#1776" class="Bound">e₁</a> <a id="1809" href="V1.TypeChecker.html#1765" class="Bound">t</a>
<a id="1815" href="V1.TypeChecker.html#1815" class="Bound">e₂'</a> <a id="1819" href="Library.Monad.html#1002" class="Field Operator">←</a> <a id="1821" href="V1.TypeChecker.html#1446" class="Function">checkExp</a> <a id="1830" href="V1.TypeChecker.html#1779" class="Bound">e₂</a> <a id="1833" href="V1.TypeChecker.html#1765" class="Bound">t</a>
<a id="1839" href="Library.Monad.html#1110" class="Function">return</a> <a id="1846" class="Symbol">(</a><a id="1847" href="V1.TypeChecker.html#1769" class="Bound">t'</a> <a id="1850" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="1852" href="V1.WellTypedSyntax.html#540" class="InductiveConstructor">eOp</a> <a id="1856" href="V1.TypeChecker.html#1773" class="Bound">op</a> <a id="1859" href="V1.TypeChecker.html#1791" class="Bound">e₁'</a> <a id="1863" href="V1.TypeChecker.html#1815" class="Bound">e₂'</a><a id="1866" class="Symbol">)</a>
<a id="1869" class="Comment">-- Checking the program.</a>
<a id="1894" class="Comment">---------------------------------------------------------------------------</a>
<a id="checkProgram"></a><a id="1971" href="V1.TypeChecker.html#1971" class="Function">checkProgram</a> <a id="1984" class="Symbol">:</a> <a id="1986" class="Symbol">(</a><a id="1987" href="V1.TypeChecker.html#1987" class="Bound">prg</a> <a id="1991" class="Symbol">:</a> <a id="1993" href="V1.AST.html#818" class="Record">A.Program</a><a id="2002" class="Symbol">)</a> <a id="2004" class="Symbol">→</a> <a id="2006" href="Library.Error.html#170" class="Function">Error</a> <a id="2012" href="V1.WellTypedSyntax.html#729" class="Record">Program</a>
<a id="2020" href="V1.TypeChecker.html#1971" class="Function">checkProgram</a> <a id="2033" class="Symbol">(</a><a id="2034" href="V1.AST.html#852" class="InductiveConstructor">A.program</a> <a id="2044" href="V1.TypeChecker.html#2044" class="Bound">e</a><a id="2045" class="Symbol">)</a> <a id="2047" class="Symbol">=</a> <a id="2049" class="Keyword">do</a>
<a id="2054" href="V1.TypeChecker.html#2054" class="Bound">e'</a> <a id="2057" href="Library.Monad.html#1002" class="Field Operator">←</a> <a id="2059" href="V1.TypeChecker.html#1446" class="Function">checkExp</a> <a id="2068" href="V1.TypeChecker.html#2044" class="Bound">e</a> <a id="2070" href="V1.AST.html#306" class="InductiveConstructor">int</a>
<a id="2076" href="Library.Monad.html#1110" class="Function">return</a> <a id="2083" href="Function.html#1645" class="Function Operator">$</a> <a id="2085" href="V1.WellTypedSyntax.html#763" class="InductiveConstructor">program</a> <a id="2093" href="V1.TypeChecker.html#2054" class="Bound">e'</a>
<a id="2098" class="Comment">-- -}</a>
<a id="2104" class="Comment">-- -}</a>
<a id="2110" class="Comment">-- -}</a>
<a id="2116" class="Comment">-- -}</a>
<a id="2122" class="Comment">-- -}</a>
<a id="2128" class="Comment">-- -}</a>
</pre></body></html>