dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 11:08:25 +00:00
Code Issues Releases Wiki Activity

Update code

Browse Source
This commit is contained in:
Daniel Hillerström
2020-10-27 00:58:20 +00:00
parent 8700c0f439
commit e2af947cbd
3 changed files with 31 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
code/unix2.links
View File

@@ -545,15 +545,13 @@ fun init(fsys, main) {
### Stream redirection ### Stream redirection
### ###
sig >> : (Comp(a, { Create: (String) -> FileDescr sig >> : (Comp(a, { Create: (String) -> FileDescr
, Open: (String) {}-> Option (FileDescr)
, Write:(FileDescr, String) -> () |e}), String) , Write:(FileDescr, String) -> () |e}), String)
{ Create:(String) -> FileDescr { Create:(String) -> FileDescr
, Open:(String) -> Option (FileDescr) , Write:(FileDescr, String) -> () |e}~> a
, Write:(FileDescr, String) -> () |e}~> ()
op f >> fname { op f >> fname {
var fd = create(fname); var fd = create(fname);
handle(f()) { handle(f()) {
case Return(_) -> () case Return(x) -> x
case Write(_, cs, resume) -> case Write(_, cs, resume) ->
resume(write(fd, cs)) resume(write(fd, cs))
} }

2
macros.tex
View File

@@ -408,6 +408,8 @@
\newcommand{\UCreate}{\dec{Create}} \newcommand{\UCreate}{\dec{Create}}
\newcommand{\fread}{\dec{fread}} \newcommand{\fread}{\dec{fread}}
\newcommand{\fcreate}{\dec{fcreate}} \newcommand{\fcreate}{\dec{fcreate}}
\newcommand{\Ucreate}{\dec{create}}
\newcommand{\redirect}{\texttt{>}}
%% %%
%% Some control operators %% Some control operators

31
thesis.tex
View File

@@ -3429,7 +3429,7 @@ $\texttt{stdout}$.
% %
\[ \[
\bl \bl
\fileRW : (\UnitType \to \alpha \eff \{\URead : \Int \opto \Option\,\String;\UWrite : \Record{\Int;\String} \opto \Unit\}) \to \alpha \eff \{\State~\FileSystem\}\\ \fileRW : (\UnitType \to \alpha \eff \{\URead : \Int \opto \Option\,\String;\UWrite : \Record{\Int;\String} \opto \UnitType\}) \to \alpha \eff \{\State~\FileSystem\}\\
\fileRW~m \defas \fileRW~m \defas
\ba[t]{@{}l} \ba[t]{@{}l}
\Handle\;m\,\Unit\;\With\\ \Handle\;m\,\Unit\;\With\\
@@ -3437,7 +3437,8 @@ $\texttt{stdout}$.
\Return\;res &\mapsto& res\\ \Return\;res &\mapsto& res\\
\OpCase{\URead}{ino}{resume} &\mapsto& \OpCase{\URead}{ino}{resume} &\mapsto&
\bl \bl
\Let\;cs\revto \optionalise\,(\lambda\Unit.\fread\,\Record{ino;\Uget\,\Unit})\\ \Let\;cs\revto \faild\,\Record{\None;\lambda\Unit.\\
\quad\Some\,(\fread\,\Record{ino;\Uget\,\Unit})}\\
\In\;resume\,cs \In\;resume\,cs
\el\\ \el\\
\OpCase{\UWrite}{\Record{ino;cs}}{resume} &\mapsto& \OpCase{\UWrite}{\Record{ino;cs}}{resume} &\mapsto&
@@ -3468,14 +3469,36 @@ $\texttt{stdout}$.
\Let\;ino \revto \faild\,\Record{-1; \lambda\Unit.\\ \Let\;ino \revto \faild\,\Record{-1; \lambda\Unit.\\
\quad\bl \quad\bl
\Let\;\Record{ino;fs} = \fcreate\,\Record{\,fname;\Uget\,\Unit}\\ \Let\;\Record{ino;fs} = \fcreate\,\Record{\,fname;\Uget\,\Unit}\\
\In\;\Uput~fs;\,ino};\,resume\,ino \In\;\Uput~fs;\,ino}
\el \el\\
\In\; resume\,ino
\el \el
\ea \ea
\ea \ea
\el \el
\] \]
\paragraph{Stream redirection}
%
\[
\bl
\redirect : \Record{\UnitType \to \alpha \eff \{\Write : \Record{\Int;\String} \opto \UnitType\}; \String} \to \alpha \eff \{\UCreate : \String \opto \Int;\Write : \Record{\Int;\String}\}\\
m~\redirect~fname \defas
\ba[t]{@{}l}
\Let\;ino \revto \Ucreate~fname\;\In\\
\Handle\;m\,\Unit\;\With\\
~\ba{@{~}l@{~}c@{~}l}
\Return\;res &\mapsto& res\\
\OpCase{\Write}{\Record{\_;cs}}{resume} &\mapsto& resume\,(\Do\;\Write\,\Record{ino;cs})
\ea
\ea
\el
\]
%
\paragraph{File linking and unlinking}
\dhil{Maybe axe\dots}
% \begin{figure}[t] % \begin{figure}[t]
% \centering % \centering
% \begin{tikzpicture}[node distance=4cm,auto,>=stealth'] % \begin{tikzpicture}[node distance=4cm,auto,>=stealth']