mirror of
https://github.com/dhil/phd-dissertation
synced 2026-03-13 11:08:25 +00:00
Update code
This commit is contained in:
267
code/unix2.links
267
code/unix2.links
@@ -1,16 +1,32 @@
|
|||||||
# Tiny UNIX revision 2.
|
# Tiny UNIX revision 2.
|
||||||
|
|
||||||
sig str : ((a, [Char])) ~> (a, String)
|
|
||||||
fun str((x, cs)) { (x, implode(cs)) }
|
|
||||||
|
|
||||||
typename Option(a) = [|None|Some:a|];
|
typename Option(a) = [|None|Some:a|];
|
||||||
|
|
||||||
sig lookup : (a, [(a, b)]) ~> Option(b)
|
sig fail : () {Fail:Zero |_}-> a
|
||||||
|
fun fail() { switch (do Fail) {} }
|
||||||
|
|
||||||
|
sig optionalise : (Comp(a, {Fail:Zero |e})) {Fail{_} |e}~> Option(a)
|
||||||
|
fun optionalise(m) {
|
||||||
|
handle(m()) {
|
||||||
|
case Return(x) -> Some(x)
|
||||||
|
case Fail(_) -> None
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
sig withDefault : (a, Comp(a, {Fail:Zero |e})) {Fail{_} |e}~> a
|
||||||
|
fun withDefault(x', m) {
|
||||||
|
handle(m()) {
|
||||||
|
case Return(x) -> x
|
||||||
|
case Fail(_) -> x'
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
sig lookup : (a, [(a, b)]) {Fail:Zero |_}~> b
|
||||||
fun lookup(k, kvs) {
|
fun lookup(k, kvs) {
|
||||||
switch (kvs) {
|
switch (kvs) {
|
||||||
case [] -> None
|
case [] -> fail()
|
||||||
case (k', v) :: kvs' ->
|
case (k', v) :: kvs' ->
|
||||||
if (k == k') Some(v)
|
if (k == k') v
|
||||||
else lookup(k, kvs')
|
else lookup(k, kvs')
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@@ -44,14 +60,6 @@ fun has(k, kvs) {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
sig fromSome : (Option(a)) ~> a
|
|
||||||
fun fromSome(x) {
|
|
||||||
switch (x) {
|
|
||||||
case None -> error("fromSome")
|
|
||||||
case Some(x) -> x
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
##
|
##
|
||||||
## Basic i/o
|
## Basic i/o
|
||||||
##
|
##
|
||||||
@@ -185,22 +193,32 @@ fun slice(m) {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
sig runNext : ([Pstate(a, { Fork:Bool |e})]) {Fork{_},Interrupt{_} |e}~> [a]
|
sig schedule : ([Pstate(a, { Fork:Bool |e})]) {Fork{_},Interrupt{_} |e}~> [a]
|
||||||
fun runNext(ps) {
|
fun schedule(ps) {
|
||||||
sig run : (Pstate (a, { Fork:() {}-> Bool|e })) {Fork{_},Interrupt{_} |e}~> [a]
|
# sig run : (Pstate (a, { Fork:() {}-> Bool|e })) {Fork{_},Interrupt{_} |e}~> [a]
|
||||||
fun run(p) {
|
# fun run(p) {
|
||||||
switch(p) {
|
# switch(p) {
|
||||||
case Done(res) -> [res]
|
# case Done(res) -> [res]
|
||||||
case Paused(resume) -> runNext(nondet(resume))
|
# case Paused(resume) -> runNext(nondet(resume))
|
||||||
|
# }
|
||||||
|
# }
|
||||||
|
# concatMap(run, ps)
|
||||||
|
fun schedule(ps, done) {
|
||||||
|
switch (ps) {
|
||||||
|
case [] -> done
|
||||||
|
case Done(res) :: ps' ->
|
||||||
|
schedule(ps', res :: done)
|
||||||
|
case Paused(resume) :: ps' ->
|
||||||
|
schedule(ps' ++ nondet(resume), done)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
concatMap(run, ps)
|
schedule(ps, [])
|
||||||
}
|
}
|
||||||
|
|
||||||
sig timeshare : (Comp(a, {Fork:Bool,Interrupt:() |e})) {Fork{_},Interrupt{_} |e}~> [a]
|
sig timeshare : (Comp(a, {Fork:Bool,Interrupt:() |e})) {Fork{_},Interrupt{_} |e}~> [a]
|
||||||
fun timeshare(m) {
|
fun timeshare(m) {
|
||||||
var p = Paused(fun() { slice(m) });
|
var p = Paused(fun() { slice(m) });
|
||||||
runNext([p])
|
schedule([p])
|
||||||
}
|
}
|
||||||
|
|
||||||
fun example4() {
|
fun example4() {
|
||||||
@@ -231,6 +249,89 @@ fun example4() {
|
|||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fun forktest(n) {
|
||||||
|
fun loop(i, n) {
|
||||||
|
if (i >= n) (-1)
|
||||||
|
else {
|
||||||
|
var x = fork();
|
||||||
|
println("< x = " ^^ (if (x) "true" else "false") ^^ ", i = " ^^ intToString(i));
|
||||||
|
ignore(loop(i+1,n));
|
||||||
|
println("> x = " ^^ (if (x) "true" else "false") ^^ ", i = " ^^ intToString(i));
|
||||||
|
exit(i)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
loop(0, n)
|
||||||
|
}
|
||||||
|
|
||||||
|
fun test(i) {
|
||||||
|
if (i == 2) ()
|
||||||
|
else {
|
||||||
|
println("< i = " ^^ intToString(i));
|
||||||
|
var x = fork();
|
||||||
|
test(i+1);
|
||||||
|
println("> i = " ^^ intToString(i))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fun ritchie() {
|
||||||
|
echo("UNIX is basically ");
|
||||||
|
echo("a simple operating system, ");
|
||||||
|
echo("but ");
|
||||||
|
echo("you have to be a genius to understand the simplicity.\n")
|
||||||
|
}
|
||||||
|
|
||||||
|
fun hamlet() {
|
||||||
|
echo("To be, or not to be,\n");
|
||||||
|
echo("that is the question:\n");
|
||||||
|
echo("Whether 'tis nobler in the mind to suffer\n")
|
||||||
|
}
|
||||||
|
|
||||||
|
fun example5() {
|
||||||
|
basicIO(fun() {
|
||||||
|
nondet(fun() {
|
||||||
|
sessionmgr(Root, fun() {
|
||||||
|
status(fun() {
|
||||||
|
if (fork()) {
|
||||||
|
su(Alice);
|
||||||
|
ritchie()
|
||||||
|
} else {
|
||||||
|
su(Bob);
|
||||||
|
hamlet()
|
||||||
|
}
|
||||||
|
})
|
||||||
|
})
|
||||||
|
})
|
||||||
|
})
|
||||||
|
}
|
||||||
|
|
||||||
|
fun interruptWrite(m) {
|
||||||
|
handle(m()) {
|
||||||
|
case Return(res) -> res
|
||||||
|
case Write(fd, cs, resume) ->
|
||||||
|
interrupt(); resume(do Write(fd, cs))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fun example5'() {
|
||||||
|
basicIO(fun() {
|
||||||
|
timeshare(fun() {
|
||||||
|
interruptWrite(fun() {
|
||||||
|
sessionmgr(Root, fun() {
|
||||||
|
status(fun() {
|
||||||
|
if (fork()) {
|
||||||
|
su(Alice);
|
||||||
|
ritchie()
|
||||||
|
} else {
|
||||||
|
su(Bob);
|
||||||
|
hamlet()
|
||||||
|
}
|
||||||
|
})
|
||||||
|
})
|
||||||
|
})
|
||||||
|
})
|
||||||
|
})
|
||||||
|
}
|
||||||
|
|
||||||
##
|
##
|
||||||
## Generic state handling
|
## Generic state handling
|
||||||
##
|
##
|
||||||
@@ -250,7 +351,7 @@ fun runState(st0, m) {
|
|||||||
f(st0)
|
f(st0)
|
||||||
}
|
}
|
||||||
|
|
||||||
fun example5() {
|
fun example6() {
|
||||||
runState(0, fun() {
|
runState(0, fun() {
|
||||||
var x = 3;
|
var x = 3;
|
||||||
put(x);
|
put(x);
|
||||||
@@ -280,21 +381,20 @@ typename FileSystem = (dir:Directory,dregion:DataRegion,inodes:IList
|
|||||||
sig fsys0 : FileSystem
|
sig fsys0 : FileSystem
|
||||||
var fsys0 = (dir = [("stdout", 0)], inodes = [(0, (loc=0, lno=1))], dregion = [(0, "")], lnext = 1, inext = 1);
|
var fsys0 = (dir = [("stdout", 0)], inodes = [(0, (loc=0, lno=1))], dregion = [(0, "")], lnext = 1, inext = 1);
|
||||||
|
|
||||||
sig fopen : (String, FileSystem) ~> (Option(Int), FileSystem)
|
sig fopen : (String, FileSystem) {Fail:Zero |_}~> (Int, FileSystem)
|
||||||
fun fopen(fname, fsys) { (lookup(fname, fsys.dir), fsys) }
|
fun fopen(fname, fsys) { (lookup(fname, fsys.dir), fsys) }
|
||||||
|
|
||||||
sig ftruncate : (Int, FileSystem) ~> FileSystem
|
sig ftruncate : (Int, FileSystem) {Fail:Zero |_}~> FileSystem
|
||||||
fun ftruncate(ino, fsys) {
|
fun ftruncate(ino, fsys) {
|
||||||
var inode = fromSome(lookup(ino, fsys.inodes));
|
var inode = lookup(ino, fsys.inodes);
|
||||||
var dregion = modify(inode.loc, "", fsys.dregion);
|
var dregion = modify(inode.loc, "", fsys.dregion);
|
||||||
(fsys with =dregion)
|
(fsys with =dregion)
|
||||||
}
|
}
|
||||||
|
|
||||||
sig fcreate : (String, FileSystem) ~> (Int, FileSystem)
|
sig fcreate : (String, FileSystem) {Fail:Zero |_}~> (Int, FileSystem)
|
||||||
fun fcreate(fname, fsys) {
|
fun fcreate(fname, fsys) {
|
||||||
if (has(fname, fsys.dir)) {
|
if (has(fname, fsys.dir)) {
|
||||||
var (ino, fsys) = fopen(fname, fsys);
|
var (ino, fsys) = fopen(fname, fsys);
|
||||||
var ino = fromSome(ino);
|
|
||||||
(ino, ftruncate(ino, fsys))
|
(ino, ftruncate(ino, fsys))
|
||||||
} else {
|
} else {
|
||||||
var loc = fsys.lnext;
|
var loc = fsys.lnext;
|
||||||
@@ -309,65 +409,59 @@ fun fcreate(fname, fsys) {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
sig ftruncate : (Int, FileSystem) ~> FileSystem
|
sig ftruncate : (Int, FileSystem) {Fail:Zero |_}~> FileSystem
|
||||||
fun ftruncate(ino, fsys) {
|
fun ftruncate(ino, fsys) {
|
||||||
var inode = fromSome(lookup(ino, fsys.inodes));
|
var inode = lookup(ino, fsys.inodes);
|
||||||
var dregion = modify(inode.loc, "", fsys.dregion);
|
var dregion = modify(inode.loc, "", fsys.dregion);
|
||||||
(fsys with =dregion)
|
(fsys with =dregion)
|
||||||
}
|
}
|
||||||
|
|
||||||
sig fopen : (String, FileSystem) ~> (Option(Int), FileSystem)
|
sig fopen : (String, FileSystem) {Fail:Zero |_}~> Int
|
||||||
fun fopen(fname, fsys) { (lookup(fname, fsys.dir), fsys) }
|
fun fopen(fname, fsys) { lookup(fname, fsys.dir) }
|
||||||
|
|
||||||
sig fclose : (Int, FileSystem) ~> FileSystem
|
sig fclose : (Int, FileSystem) ~> FileSystem
|
||||||
fun fclose(_, fsys) { fsys }
|
fun fclose(_, fsys) { fsys }
|
||||||
|
|
||||||
sig fwrite : (Int, String, FileSystem) ~> FileSystem
|
sig fwrite : (Int, String, FileSystem) {Fail:Zero |_}~> FileSystem
|
||||||
fun fwrite(ino, cs, fsys) {
|
fun fwrite(ino, cs, fsys) {
|
||||||
var inode = fromSome(lookup(ino, fsys.inodes));
|
var inode = lookup(ino, fsys.inodes);
|
||||||
var file = fromSome(lookup(inode.loc, fsys.dregion));
|
var file = lookup(inode.loc, fsys.dregion);
|
||||||
var file' = file ^^ cs;
|
var file' = file ^^ cs;
|
||||||
(fsys with dregion = modify(inode.loc, file', fsys.dregion))
|
(fsys with dregion = modify(inode.loc, file', fsys.dregion))
|
||||||
}
|
}
|
||||||
|
|
||||||
sig fread : (Int, FileSystem) ~> Option(String)
|
sig fread : (Int, FileSystem) {Fail:Zero |_}~> String
|
||||||
fun fread(ino, fsys) {
|
fun fread(ino, fsys) {
|
||||||
var inode = fromSome(lookup(ino, fsys.inodes));
|
var inode = lookup(ino, fsys.inodes);
|
||||||
lookup(inode.loc, fsys.dregion)
|
lookup(inode.loc, fsys.dregion)
|
||||||
}
|
}
|
||||||
|
|
||||||
sig flink : (String, String, FileSystem) ~> Option(FileSystem)
|
sig flink : (String, String, FileSystem) {Fail:Zero |_}~> FileSystem
|
||||||
fun flink(src, dest, fsys) {
|
fun flink(src, dest, fsys) {
|
||||||
switch (lookup(dest, fsys.dir)) {
|
var ino = lookup(dest, fsys.dir);
|
||||||
case None -> None
|
var inode = lookup(ino, fsys.inodes);
|
||||||
case Some(ino) ->
|
var inode' = (inode with lno = inode.lno + 1);
|
||||||
var inode = fromSome(lookup(ino, fsys.inodes));
|
var inodes = modify(ino, inode', fsys.inodes);
|
||||||
var inode = (inode with lno = inode.lno + 1);
|
|
||||||
var inodes = modify(ino, inode, fsys.inodes);
|
|
||||||
|
|
||||||
var dir = (src, ino) :: fsys.dir;
|
var dir = (src, ino) :: fsys.dir;
|
||||||
Some((fsys with inodes = inodes, dir = dir))
|
(fsys with inodes = inodes, dir = dir)
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
sig funlink : (String, FileSystem) ~> Option(FileSystem)
|
sig funlink : (String, FileSystem) {Fail:Zero |_}~> FileSystem
|
||||||
fun funlink(fname, fsys) {
|
fun funlink(fname, fsys) {
|
||||||
switch (lookup(fname, fsys.dir)) {
|
var i = lookup(fname, fsys.dir);
|
||||||
case None -> None
|
|
||||||
case Some(i) ->
|
|
||||||
var dir = remove(fname, fsys.dir);
|
var dir = remove(fname, fsys.dir);
|
||||||
|
|
||||||
var inode = fromSome(lookup(i, fsys.inodes));
|
var inode = lookup(i, fsys.inodes);
|
||||||
var inode = (inode with lno = inode.lno - 1);
|
var inode' = (inode with lno = inode.lno - 1);
|
||||||
|
|
||||||
if (inode.lno > 0) {
|
if (inode'.lno > 0) {
|
||||||
var inodes = modify(i, inode, fsys.inodes);
|
var inodes = modify(i, inode', fsys.inodes);
|
||||||
Some((fsys with inodes = inodes, dir = dir))
|
(fsys with inodes = inodes, dir = dir)
|
||||||
} else {
|
} else {
|
||||||
var dregion = remove(inode.loc, fsys.dregion);
|
var dregion = remove(inode'.loc, fsys.dregion);
|
||||||
var inodes = remove(i, fsys.inodes);
|
var inodes = remove(i, fsys.inodes);
|
||||||
Some((fsys with inodes = inodes, dir = dir, dregion = dregion))
|
(fsys with inodes = inodes, dir = dir, dregion = dregion)
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -398,32 +492,38 @@ fun unlink(fname) { do Unlink(fname) }
|
|||||||
sig injectState : (() { |e}~> a) -> () {Get:s,Put:(s) -> () |e}~> a
|
sig injectState : (() { |e}~> a) -> () {Get:s,Put:(s) -> () |e}~> a
|
||||||
fun injectState(f) { (f : (() {Get:s,Put:(s) -> () |e}~> a) <- (() { |e}~> a)) }
|
fun injectState(f) { (f : (() {Get:s,Put:(s) -> () |e}~> a) <- (() { |e}~> a)) }
|
||||||
|
|
||||||
sig fileIO : (Comp(a, { Close:(FileDescr) -> ()
|
sig fileIO : (Comp(a, { #Close:(FileDescr) -> ()
|
||||||
, Create:(String) -> FileDescr
|
Create:(String) -> FileDescr
|
||||||
, Read:(FileDescr) -> Option(String)
|
, Read:(FileDescr) -> Option(String)
|
||||||
, Open:(String) -> Option(FileDescr)
|
, Open:(String) -> Option(FileDescr)
|
||||||
, Truncate:(FileDescr) -> ()
|
, Truncate:(FileDescr) -> ()
|
||||||
, Write:(FileDescr, String) -> () |e}))
|
, Write:(FileDescr, String) -> ()
|
||||||
{Close{_},Create{_},Read{_},Open{_},Truncate{_},Write{_},Get:FileSystem,Put:(FileSystem) -> () |e}~> a
|
, Fail{p}|e}))
|
||||||
|
{Create{_},Read{_},Open{_},Truncate{_},Write{_},Get:FileSystem,Put:(FileSystem) -> (),Fail{p} |e}~> a
|
||||||
fun fileIO(m) {
|
fun fileIO(m) {
|
||||||
handle(injectState(m)()) {
|
handle(injectState(m)()) {
|
||||||
case Return(x) -> x
|
case Return(x) -> x
|
||||||
case Close(_, resume) ->
|
|
||||||
resume(())
|
|
||||||
case Create(fname, resume) ->
|
case Create(fname, resume) ->
|
||||||
var (fd, fsys) = fcreate(fname, get());
|
var ino = withDefault(-1, fun() {
|
||||||
put(fsys); resume(fd)
|
var (ino, fsys) = fcreate(fname, get());
|
||||||
case Read(fd, resume) ->
|
put(fsys); ino
|
||||||
resume(fread(fd, get()))
|
}); resume(ino)
|
||||||
|
case Read(ino, resume) ->
|
||||||
|
var contents = optionalise(fun() { fread(ino, get()) });
|
||||||
|
resume(contents)
|
||||||
case Open(fname, resume) ->
|
case Open(fname, resume) ->
|
||||||
var (fd, fsys) = fopen(fname, get());
|
var ino = optionalise(fun() { fopen(fname, get()) });
|
||||||
put(fsys); resume(fd)
|
resume(ino)
|
||||||
case Truncate(fd, resume) ->
|
case Truncate(ino, resume) ->
|
||||||
var fsys = ftruncate(fd, get());
|
withDefault((), fun() {
|
||||||
put(fsys); resume(())
|
var fsys = ftruncate(ino, get());
|
||||||
case Write(fd, cs, resume) ->
|
put(fsys)
|
||||||
var fsys = fwrite(fd, cs, get());
|
}); resume(())
|
||||||
put(fsys); resume(())
|
case Write(ino, cs, resume) ->
|
||||||
|
withDefault((), fun() {
|
||||||
|
var fsys = fwrite(ino, cs, get());
|
||||||
|
put(fsys)
|
||||||
|
}); resume(())
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -477,20 +577,13 @@ op f >>> fname {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fun example6() {
|
fun example7() {
|
||||||
if (fork()) {
|
if (fork()) {
|
||||||
su(Alice);
|
su(Alice);
|
||||||
var fd = create("ritchie.txt");
|
ritchie >> "ritchie.txt"
|
||||||
fun(){echo("UNIX is basically a simple operating system, ")} >> "ritchie.txt";
|
|
||||||
fun(){echo("but you have to be a genius to understand the simplicity.")} >>> "ritchie.txt"
|
|
||||||
} else {
|
} else {
|
||||||
su(Bob);
|
su(Bob);
|
||||||
var hamlet = "hamlet";
|
hamlet >> "hamlet"
|
||||||
fun(){echo("To be, or not to be, that is the question:\n")} >> hamlet;
|
|
||||||
fun(){echo("Whether 'tis nobler in the mind to suffer\n")} >>> hamlet;
|
|
||||||
fun(){echo("The slings and arrows of outrageous fortune,\n")} >>> hamlet;
|
|
||||||
fun(){echo("Or to take arms against a sea of troubles\n")} >>> hamlet;
|
|
||||||
fun(){echo("And by opposing end them.")} >>> hamlet
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user