-
Notifications
You must be signed in to change notification settings - Fork 4
/
V2.runwhile.html
69 lines (52 loc) · 11.2 KB
/
V2.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
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>V2.runwhile</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- Type checker and interpreter for WHILE language.</a>
<a id="54" class="Keyword">module</a> <a id="61" href="V2.runwhile.html" class="Module">V2.runwhile</a> <a id="73" class="Keyword">where</a>
<a id="80" class="Keyword">open</a> <a id="85" class="Keyword">import</a> <a id="92" href="Library.html" class="Module">Library</a>
<a id="100" class="Keyword">open</a> <a id="105" class="Keyword">import</a> <a id="112" href="V2.WellTypedSyntax.html" class="Module">V2.WellTypedSyntax</a> <a id="131" class="Keyword">using</a> <a id="137" class="Symbol">(</a><a id="138" href="V2.WellTypedSyntax.html#1319" class="Record">Program</a><a id="145" class="Symbol">)</a>
<a id="147" class="Keyword">open</a> <a id="152" class="Keyword">import</a> <a id="159" href="V2.TypeChecker.html" class="Module">V2.TypeChecker</a> <a id="178" class="Keyword">using</a> <a id="184" class="Symbol">(</a><a id="185" href="V2.TypeChecker.html#5851" class="Function">checkProgram</a><a id="197" class="Symbol">)</a>
<a id="200" class="Keyword">import</a> <a id="207" href="V2.AST.html" class="Module">V2.AST</a> <a id="214" class="Symbol">as</a> <a id="217" class="Module">A</a>
<a id="219" class="Keyword">import</a> <a id="226" href="V2.Parser.html" class="Module">V2.Parser</a> <a id="236" class="Symbol">as</a> <a id="239" class="Module">Parser</a>
<a id="246" class="Keyword">open</a> <a id="251" class="Keyword">import</a> <a id="258" href="V2.Interpreter.html" class="Module">V2.Interpreter</a> <a id="273" class="Keyword">using</a> <a id="279" class="Symbol">(</a><a id="280" href="V2.Interpreter.html#1090" class="Function">runProgram</a><a id="290" class="Symbol">)</a>
<a id="293" class="Comment">-- Other modules, not used here.</a>
<a id="326" class="Keyword">import</a> <a id="333" href="V2.Value.html" class="Module">V2.Value</a>
<a id="342" class="Keyword">import</a> <a id="349" href="V2.UntypedInterpreter.html" class="Module">V2.UntypedInterpreter</a>
<a id="372" class="Comment">-- Parse.</a>
<a id="parse"></a><a id="383" href="V2.runwhile.html#383" class="Function">parse</a> <a id="389" class="Symbol">:</a> <a id="391" href="Agda.Builtin.String.html#247" class="Postulate">String</a> <a id="398" class="Symbol">→</a> <a id="400" href="Agda.Builtin.IO.html#111" class="Postulate">IO</a> <a id="403" href="V2.AST.html#1134" class="Record">A.Program</a>
<a id="413" href="V2.runwhile.html#383" class="Function">parse</a> <a id="419" href="V2.runwhile.html#419" class="Bound">contents</a> <a id="428" class="Symbol">=</a> <a id="430" href="Function.html#3662" class="Function Operator">case</a> <a id="435" href="V2.Parser.html#530" class="Postulate">Parser.parse</a> <a id="448" href="V2.runwhile.html#419" class="Bound">contents</a> <a id="457" href="Function.html#3662" class="Function Operator">of</a> <a id="460" class="Symbol">λ</a> <a id="462" class="Keyword">where</a>
<a id="472" class="Symbol">(</a><a id="473" href="V2.Parser.html#443" class="InductiveConstructor">bad</a> <a id="477" href="V2.runwhile.html#477" class="Bound">cs</a><a id="479" class="Symbol">)</a> <a id="481" class="Symbol">→</a> <a id="483" class="Keyword">do</a>
<a id="492" href="Library.IO.html#621" class="Postulate">putStrLn</a> <a id="501" class="String">"SYNTAX ERROR"</a>
<a id="522" href="Library.IO.html#621" class="Postulate">putStrLn</a> <a id="531" class="Symbol">(</a><a id="532" href="Agda.Builtin.String.html#345" class="Primitive">String.fromList</a> <a id="548" href="V2.runwhile.html#477" class="Bound">cs</a><a id="550" class="Symbol">)</a>
<a id="558" href="Library.IO.html#509" class="Postulate">exitFailure</a>
<a id="574" class="Symbol">(</a><a id="575" href="V2.Parser.html#424" class="InductiveConstructor">ok</a> <a id="578" href="V2.runwhile.html#578" class="Bound">prg</a><a id="581" class="Symbol">)</a> <a id="583" class="Symbol">→</a> <a id="585" href="Library.Monad.html#1110" class="Function">return</a> <a id="592" href="V2.runwhile.html#578" class="Bound">prg</a>
<a id="598" class="Keyword">where</a>
<a id="608" class="Keyword">open</a> <a id="613" href="V2.Parser.html" class="Module">Parser</a> <a id="620" class="Keyword">using</a> <a id="626" class="Symbol">(</a><a id="627" href="V2.Parser.html#396" class="Datatype">Err</a><a id="630" class="Symbol">;</a> <a id="632" href="V2.Parser.html#424" class="InductiveConstructor">ok</a><a id="634" class="Symbol">;</a> <a id="636" href="V2.Parser.html#443" class="InductiveConstructor">bad</a><a id="639" class="Symbol">)</a>
<a id="642" class="Comment">-- Type check.</a>
<a id="check"></a><a id="658" href="V2.runwhile.html#658" class="Function">check</a> <a id="664" class="Symbol">:</a> <a id="666" href="V2.AST.html#1134" class="Record">A.Program</a> <a id="676" class="Symbol">→</a> <a id="678" href="Agda.Builtin.IO.html#111" class="Postulate">IO</a> <a id="681" href="V2.WellTypedSyntax.html#1319" class="Record">Program</a>
<a id="689" href="V2.runwhile.html#658" class="Function">check</a> <a id="695" href="V2.runwhile.html#695" class="Bound">prg</a> <a id="699" class="Symbol">=</a> <a id="701" href="Function.html#3662" class="Function Operator">case</a> <a id="706" href="V2.TypeChecker.html#5851" class="Function">checkProgram</a> <a id="719" href="V2.runwhile.html#695" class="Bound">prg</a> <a id="723" href="Function.html#3662" class="Function Operator">of</a> <a id="726" class="Symbol">λ</a> <a id="728" class="Keyword">where</a>
<a id="738" class="Symbol">(</a><a id="739" href="Library.Error.html#238" class="InductiveConstructor">fail</a> <a id="744" href="V2.runwhile.html#744" class="Bound">err</a><a id="747" class="Symbol">)</a> <a id="749" class="Symbol">→</a> <a id="751" class="Keyword">do</a>
<a id="760" href="Library.IO.html#621" class="Postulate">putStrLn</a> <a id="769" class="String">"TYPE ERROR"</a>
<a id="788" href="Library.IO.html#588" class="Postulate">putStr</a> <a id="797" class="Symbol">(</a><a id="798" href="Library.Print.html#244" class="Field">print</a> <a id="804" href="V2.runwhile.html#695" class="Bound">prg</a><a id="807" class="Symbol">)</a>
<a id="815" href="Library.IO.html#621" class="Postulate">putStrLn</a> <a id="824" class="String">"The type error is:"</a>
<a id="851" href="Library.IO.html#621" class="Postulate">putStrLn</a> <a id="860" class="Symbol">(</a><a id="861" href="Library.Print.html#244" class="Field">print</a> <a id="867" href="V2.runwhile.html#744" class="Bound">err</a><a id="870" class="Symbol">)</a>
<a id="878" href="Library.IO.html#509" class="Postulate">exitFailure</a>
<a id="894" class="Symbol">(</a><a id="895" href="Library.Error.html#268" class="InductiveConstructor">ok</a> <a id="898" href="V2.runwhile.html#898" class="Bound">prg'</a><a id="902" class="Symbol">)</a> <a id="904" class="Symbol">→</a> <a id="906" href="Library.Monad.html#1110" class="Function">return</a> <a id="913" href="V2.runwhile.html#898" class="Bound">prg'</a>
<a id="920" class="Keyword">where</a>
<a id="930" class="Keyword">open</a> <a id="935" href="Library.Error.html#134" class="Module">ErrorMonad</a> <a id="946" class="Keyword">using</a> <a id="952" class="Symbol">(</a><a id="953" href="Library.Error.html#238">fail</a><a id="957" class="Symbol">;</a> <a id="959" href="Library.Error.html#268">ok</a><a id="961" class="Symbol">)</a>
<a id="964" class="Comment">-- Interpret.</a>
<a id="run"></a><a id="979" href="V2.runwhile.html#979" class="Function">run</a> <a id="983" class="Symbol">:</a> <a id="985" href="V2.WellTypedSyntax.html#1319" class="Record">Program</a> <a id="993" class="Symbol">→</a> <a id="995" href="Agda.Builtin.IO.html#111" class="Postulate">IO</a> <a id="998" href="Agda.Builtin.Unit.html#137" class="Record">⊤</a>
<a id="1000" href="V2.runwhile.html#979" class="Function">run</a> <a id="1004" href="V2.runwhile.html#1004" class="Bound">prg'</a> <a id="1009" class="Symbol">=</a> <a id="1011" href="Library.IO.html#621" class="Postulate">putStrLn</a> <a id="1020" class="Symbol">(</a><a id="1021" href="Library.Print.html#244" class="Field">print</a> <a id="1027" class="Symbol">(</a><a id="1028" href="V2.Interpreter.html#1090" class="Function">runProgram</a> <a id="1039" href="V2.runwhile.html#1004" class="Bound">prg'</a><a id="1043" class="Symbol">))</a>
<a id="1047" class="Comment">-- Display usage information and exit.</a>
<a id="usage"></a><a id="1087" href="V2.runwhile.html#1087" class="Function">usage</a> <a id="1093" class="Symbol">:</a> <a id="1095" href="Agda.Builtin.IO.html#111" class="Postulate">IO</a> <a id="1098" href="Agda.Builtin.Unit.html#137" class="Record">⊤</a>
<a id="1100" href="V2.runwhile.html#1087" class="Function">usage</a> <a id="1106" class="Symbol">=</a> <a id="1108" class="Keyword">do</a>
<a id="1113" href="Library.IO.html#621" class="Postulate">putStrLn</a> <a id="1122" class="String">"Usage: runwhile <SourceFile>"</a>
<a id="1155" href="Library.IO.html#509" class="Postulate">exitFailure</a>
<a id="1168" class="Comment">-- Parse command line argument and send file content through pipeline.</a>
<a id="runwhile"></a><a id="1240" href="V2.runwhile.html#1240" class="Function">runwhile</a> <a id="1249" class="Symbol">:</a> <a id="1251" href="Agda.Builtin.IO.html#111" class="Postulate">IO</a> <a id="1254" href="Agda.Builtin.Unit.html#137" class="Record">⊤</a>
<a id="1256" href="V2.runwhile.html#1240" class="Function">runwhile</a> <a id="1265" class="Symbol">=</a> <a id="1267" class="Keyword">do</a>
<a id="1272" href="V2.runwhile.html#1272" class="Bound">file</a> <a id="1277" href="Agda.Builtin.List.html#173" class="InductiveConstructor Operator">∷</a> <a id="1279" href="Agda.Builtin.List.html#158" class="InductiveConstructor">[]</a> <a id="1282" href="Library.Monad.html#1002" class="Field Operator">←</a> <a id="1284" href="Library.IO.html#552" class="Postulate">getArgs</a>
<a id="1296" class="Keyword">where</a> <a id="1302" class="CatchallClause Symbol">_</a><a id="1303" class="CatchallClause"> </a><a id="1304" class="CatchallClause Symbol">→</a><a id="1305" class="CatchallClause"> </a><a id="1306" href="V2.runwhile.html#1087" class="CatchallClause Function">usage</a>
<a id="1314" href="V2.runwhile.html#979" class="Function">run</a> <a id="1318" href="Library.Monad.html#1243" class="Function Operator">=<<</a> <a id="1322" href="V2.runwhile.html#658" class="Function">check</a> <a id="1328" href="Library.Monad.html#1243" class="Function Operator">=<<</a> <a id="1332" href="V2.runwhile.html#383" class="Function">parse</a> <a id="1338" href="Library.Monad.html#1243" class="Function Operator">=<<</a> <a id="1342" href="Library.IO.html#654" class="Postulate">readFiniteFile</a> <a id="1357" href="V2.runwhile.html#1272" class="Bound">file</a>
<a id="1364" href="Library.Monad.html#1110" class="Function">return</a> <a id="1371" class="Symbol">_</a>
<a id="main"></a><a id="1374" href="V2.runwhile.html#1374" class="Function">main</a> <a id="1379" class="Symbol">=</a> <a id="1381" href="V2.runwhile.html#1240" class="Function">runwhile</a>
<a id="1392" class="Comment">-- -}</a>
</pre></body></html>