-
Notifications
You must be signed in to change notification settings - Fork 0
/
runwhile.html
70 lines (53 loc) · 10.9 KB
/
runwhile.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
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>runwhile</title><link rel="stylesheet" href="Agda.css"></head><body><pre><a id="1" class="Comment">-- Type checker and interpreter for WHILE language.</a>
<a id="54" class="Keyword">module</a> <a id="61" href="runwhile.html" class="Module">runwhile</a> <a id="70" class="Keyword">where</a>
<a id="77" class="Keyword">open</a> <a id="82" class="Keyword">import</a> <a id="89" href="Library.html" class="Module">Library</a>
<a id="97" class="Keyword">open</a> <a id="102" class="Keyword">import</a> <a id="109" href="WellTypedSyntax.html" class="Module">WellTypedSyntax</a> <a id="125" class="Keyword">using</a> <a id="131" class="Symbol">(</a><a id="132" href="WellTypedSyntax.html#1473" class="Record">Program</a><a id="139" class="Symbol">)</a>
<a id="141" class="Keyword">open</a> <a id="146" class="Keyword">import</a> <a id="153" href="TypeChecker.html" class="Module">TypeChecker</a> <a id="169" class="Keyword">using</a> <a id="175" class="Symbol">(</a><a id="176" href="TypeChecker.html#6235" class="Function">checkProgram</a><a id="188" class="Symbol">)</a>
<a id="191" class="Keyword">import</a> <a id="198" href="AST.html" class="Module">AST</a> <a id="202" class="Symbol">as</a> <a id="205" class="Module">A</a>
<a id="207" class="Keyword">import</a> <a id="214" href="Parser.html" class="Module">Parser</a>
<a id="221" class="Keyword">open</a> <a id="226" class="Keyword">import</a> <a id="233" href="Interpreter.html" class="Module">Interpreter</a> <a id="245" class="Keyword">using</a> <a id="251" class="Symbol">(</a><a id="252" href="Interpreter.html#3403" class="Function">runProgram</a><a id="262" class="Symbol">)</a>
<a id="265" class="Comment">-- Other modules, not used here.</a>
<a id="298" class="Keyword">import</a> <a id="305" href="Value.html" class="Module">Value</a>
<a id="311" class="Keyword">import</a> <a id="318" href="UntypedInterpreter.html" class="Module">UntypedInterpreter</a>
<a id="338" class="Comment">-- Parse.</a>
<a id="parse"></a><a id="349" href="runwhile.html#349" class="Function">parse</a> <a id="355" class="Symbol">:</a> <a id="357" href="Agda.Builtin.String.html#174" class="Postulate">String</a> <a id="364" class="Symbol">→</a> <a id="366" href="Agda.Builtin.IO.html#70" class="Postulate">IO</a> <a id="369" href="AST.html#1331" class="Record">A.Program</a>
<a id="379" href="runwhile.html#349" class="Function">parse</a> <a id="385" href="runwhile.html#385" class="Bound">contents</a> <a id="394" class="Symbol">=</a> <a id="396" class="Keyword">do</a>
<a id="401" href="Function.html#3497" class="Function Operator">case</a> <a id="406" href="Parser.html#524" class="Postulate">Parser.parse</a> <a id="419" href="runwhile.html#385" class="Bound">contents</a> <a id="428" href="Function.html#3497" class="Function Operator">of</a> <a id="431" class="Symbol">λ</a> <a id="433" class="Keyword">where</a>
<a id="443" class="Symbol">(</a><a id="444" href="Parser.html#437" class="InductiveConstructor">bad</a> <a id="448" href="runwhile.html#448" class="Bound">cs</a><a id="450" class="Symbol">)</a> <a id="452" class="Symbol">→</a> <a id="454" class="Keyword">do</a>
<a id="463" href="Library.IO.html#621" class="Postulate">putStrLn</a> <a id="472" class="String">"SYNTAX ERROR"</a>
<a id="493" href="Library.IO.html#621" class="Postulate">putStrLn</a> <a id="502" class="Symbol">(</a><a id="503" href="Data.String.Base.html#924" class="Function">String.fromList</a> <a id="519" href="runwhile.html#448" class="Bound">cs</a><a id="521" class="Symbol">)</a>
<a id="529" href="Library.IO.html#509" class="Postulate">exitFailure</a>
<a id="545" class="Symbol">(</a><a id="546" href="Parser.html#418" class="InductiveConstructor">ok</a> <a id="549" href="runwhile.html#549" class="Bound">prg</a><a id="552" class="Symbol">)</a> <a id="554" class="Symbol">→</a> <a id="556" href="Library.Monad.html#1110" class="Function">return</a> <a id="563" href="runwhile.html#549" class="Bound">prg</a>
<a id="569" class="Keyword">where</a>
<a id="577" class="Keyword">open</a> <a id="582" href="Parser.html" class="Module">Parser</a> <a id="589" class="Keyword">using</a> <a id="595" class="Symbol">(</a><a id="596" href="Parser.html#390" class="Datatype">Err</a><a id="599" class="Symbol">;</a> <a id="601" href="Parser.html#418" class="InductiveConstructor">ok</a><a id="603" class="Symbol">;</a> <a id="605" href="Parser.html#437" class="InductiveConstructor">bad</a><a id="608" class="Symbol">)</a>
<a id="611" class="Comment">-- Type check.</a>
<a id="check"></a><a id="627" href="runwhile.html#627" class="Function">check</a> <a id="633" class="Symbol">:</a> <a id="635" href="AST.html#1331" class="Record">A.Program</a> <a id="645" class="Symbol">→</a> <a id="647" href="Agda.Builtin.IO.html#70" class="Postulate">IO</a> <a id="650" href="WellTypedSyntax.html#1473" class="Record">Program</a>
<a id="658" href="runwhile.html#627" class="Function">check</a> <a id="664" href="runwhile.html#664" class="Bound">prg</a> <a id="668" class="Symbol">=</a> <a id="670" class="Keyword">do</a>
<a id="675" href="Function.html#3497" class="Function Operator">case</a> <a id="680" href="TypeChecker.html#6235" class="Function">checkProgram</a> <a id="693" href="runwhile.html#664" class="Bound">prg</a> <a id="697" href="Function.html#3497" class="Function Operator">of</a> <a id="700" class="Symbol">λ</a> <a id="702" class="Keyword">where</a>
<a id="712" class="Symbol">(</a><a id="713" href="Library.Error.html#238" class="InductiveConstructor">fail</a> <a id="718" href="runwhile.html#718" class="Bound">err</a><a id="721" class="Symbol">)</a> <a id="723" class="Symbol">→</a> <a id="725" class="Keyword">do</a>
<a id="734" href="Library.IO.html#621" class="Postulate">putStrLn</a> <a id="743" class="String">"TYPE ERROR"</a>
<a id="762" href="Library.IO.html#588" class="Postulate">putStr</a> <a id="771" class="Symbol">(</a><a id="772" href="Library.Print.html#244" class="Field">print</a> <a id="778" href="runwhile.html#664" class="Bound">prg</a><a id="781" class="Symbol">)</a>
<a id="789" href="Library.IO.html#621" class="Postulate">putStrLn</a> <a id="798" class="String">"The type error is:"</a>
<a id="825" href="Library.IO.html#621" class="Postulate">putStrLn</a> <a id="834" class="Symbol">(</a><a id="835" href="Library.Print.html#244" class="Field">print</a> <a id="841" href="runwhile.html#718" class="Bound">err</a><a id="844" class="Symbol">)</a>
<a id="852" href="Library.IO.html#509" class="Postulate">exitFailure</a>
<a id="868" class="Symbol">(</a><a id="869" href="Library.Error.html#268" class="InductiveConstructor">ok</a> <a id="872" href="runwhile.html#872" class="Bound">prg'</a><a id="876" class="Symbol">)</a> <a id="878" class="Symbol">→</a> <a id="880" href="Library.Monad.html#1110" class="Function">return</a> <a id="887" href="runwhile.html#872" class="Bound">prg'</a>
<a id="894" class="Keyword">where</a>
<a id="902" class="Keyword">open</a> <a id="907" href="Library.Error.html#134" class="Module">ErrorMonad</a> <a id="918" class="Keyword">using</a> <a id="924" class="Symbol">(</a><a id="925" href="Library.Error.html#238">fail</a><a id="929" class="Symbol">;</a> <a id="931" href="Library.Error.html#268">ok</a><a id="933" class="Symbol">)</a>
<a id="936" class="Comment">-- Interpret.</a>
<a id="run"></a><a id="951" href="runwhile.html#951" class="Function">run</a> <a id="955" class="Symbol">:</a> <a id="957" href="WellTypedSyntax.html#1473" class="Record">Program</a> <a id="965" class="Symbol">→</a> <a id="967" href="Agda.Builtin.IO.html#70" class="Postulate">IO</a> <a id="970" href="Agda.Builtin.Unit.html#69" class="Record">⊤</a>
<a id="972" href="runwhile.html#951" class="Function">run</a> <a id="976" href="runwhile.html#976" class="Bound">prg'</a> <a id="981" class="Symbol">=</a> <a id="983" href="Library.IO.html#621" class="Postulate">putStrLn</a> <a id="992" class="Symbol">(</a><a id="993" href="Library.Print.html#244" class="Field">print</a> <a id="999" class="Symbol">(</a><a id="1000" href="Interpreter.html#3403" class="Function">runProgram</a> <a id="1011" href="runwhile.html#976" class="Bound">prg'</a><a id="1015" class="Symbol">))</a>
<a id="1019" class="Comment">-- Display usage information and exit.</a>
<a id="usage"></a><a id="1059" href="runwhile.html#1059" class="Function">usage</a> <a id="1065" class="Symbol">:</a> <a id="1067" href="Agda.Builtin.IO.html#70" class="Postulate">IO</a> <a id="1070" href="Agda.Builtin.Unit.html#69" class="Record">⊤</a>
<a id="1072" href="runwhile.html#1059" class="Function">usage</a> <a id="1078" class="Symbol">=</a> <a id="1080" class="Keyword">do</a>
<a id="1085" href="Library.IO.html#621" class="Postulate">putStrLn</a> <a id="1094" class="String">"Usage: runwhile <SourceFile>"</a>
<a id="1127" href="Library.IO.html#509" class="Postulate">exitFailure</a>
<a id="1140" class="Comment">-- Parse command line argument and send file content through pipeline.</a>
<a id="runwhile"></a><a id="1212" href="runwhile.html#1212" class="Function">runwhile</a> <a id="1221" class="Symbol">:</a> <a id="1223" href="Agda.Builtin.IO.html#70" class="Postulate">IO</a> <a id="1226" href="Agda.Builtin.Unit.html#69" class="Record">⊤</a>
<a id="1228" href="runwhile.html#1212" class="Function">runwhile</a> <a id="1237" class="Symbol">=</a> <a id="1239" class="Keyword">do</a>
<a id="1244" href="runwhile.html#1244" class="Bound">file</a> <a id="1249" href="Agda.Builtin.List.html#132" class="InductiveConstructor Operator">∷</a> <a id="1251" href="Agda.Builtin.List.html#117" class="InductiveConstructor">[]</a> <a id="1254" href="Library.Monad.html#1002" class="Field Operator">←</a> <a id="1256" href="Library.IO.html#552" class="Postulate">getArgs</a> <a id="1264" class="Keyword">where</a> <a id="1270" class="CatchallClause Symbol">_</a><a id="1271" class="CatchallClause"> </a><a id="1272" class="CatchallClause Symbol">→</a><a id="1273" class="CatchallClause"> </a><a id="1274" href="runwhile.html#1059" class="CatchallClause Function">usage</a>
<a id="1282" href="runwhile.html#951" class="Function">run</a> <a id="1286" href="Library.Monad.html#1243" class="Function Operator">=<<</a> <a id="1290" href="runwhile.html#627" class="Function">check</a> <a id="1296" href="Library.Monad.html#1243" class="Function Operator">=<<</a> <a id="1300" href="runwhile.html#349" class="Function">parse</a> <a id="1306" href="Library.Monad.html#1243" class="Function Operator">=<<</a> <a id="1310" href="Library.IO.html#654" class="Postulate">readFiniteFile</a> <a id="1325" href="runwhile.html#1244" class="Bound">file</a>
<a id="1332" href="Library.Monad.html#1110" class="Function">return</a> <a id="1339" class="Symbol">_</a>
<a id="main"></a><a id="1342" href="runwhile.html#1342" class="Function">main</a> <a id="1347" class="Symbol">=</a> <a id="1349" href="runwhile.html#1212" class="Function">runwhile</a>
<a id="1360" class="Comment">-- -}</a>
</pre></body></html>