Reference for UNIX.

code/unix.links

@@ -1,5 +1,52 @@
 # Tiny UNIX in Links.
 
+##
+## Functional utils
+##
+typename Option(a) = [|None|Some:a|];
+
+sig modify : (a, b, [(a, b)]) ~> [(a, b)]
+fun modify(x, y, xs) {
+  switch (xs) {
+    case [] -> []
+    case (x', y') :: xs' ->
+      if (x == x') (x, y) :: xs'
+      else (x', y') :: modify(x, y, xs')
+  }
+}
+
+###
+### Generic queue
+###
+module Queue {
+  typename T(a) = (front:[a], rear:[a]);
+
+  sig empty : T(a)
+  var empty = (front=[], rear=[]);
+
+  sig enqueue : (a, T(a)) -> T(a)
+  fun enqueue(x, q) {
+    (q with rear = x :: q.rear)
+  }
+
+  sig dequeue : (T(a)) ~> (Option(a), T(a))
+  fun dequeue(q) {
+    switch(q.front) {
+      case [] ->
+        switch (q.rear) {
+          case []   -> (None, q)
+          case rear -> dequeue((front=reverse(rear),rear=[]))
+        }
+      case x :: xs -> (Some(x), (q with front = xs))
+    }
+  }
+
+  sig singleton : (a) -> T(a)
+  fun singleton(x) { enqueue(x, empty) }
+}
+
+
+
 ##
 ## Environment
 ##
@@ -95,48 +142,13 @@ fun runState(st0, m) {
   f(st0)
 }
 
-##
-## Option type
-##
-typename Option(a) = [|None|Some:a|];
-
-##
-## Generic queue
-##
-module Queue {
-  typename T(a) = (front:[a], rear:[a]);
-
-  sig empty : T(a)
-  var empty = (front=[], rear=[]);
-
-  sig enqueue : (a, T(a)) -> T(a)
-  fun enqueue(x, q) {
-    (q with rear = x :: q.rear)
-  }
-
-  sig dequeue : (T(a)) ~> (Option(a), T(a))
-  fun dequeue(q) {
-    switch(q.front) {
-      case [] ->
-        switch (q.rear) {
-          case []   -> (None, q)
-          case rear -> dequeue((front=reverse(rear),rear=[]))
-        }
-      case x :: xs -> (Some(x), (q with front = xs))
-    }
-  }
-
-  sig singleton : (a) -> T(a)
-  fun singleton(x) { enqueue(x, empty) }
-}
-
 ##
 ## File IO
 ##
 sig stdin : FileDescr
 var stdin = 0;
 sig stderr : FileDescr
-var stderr = 3;
+var stderr = 2;
 
 sig eof : String
 var eof = "\x00";
@@ -149,6 +161,9 @@ typename Mode = [|Create|Append|];
 sig fopen : (Mode, String) {Fopen:(Mode, String) -> FileDescr |_}-> FileDescr
 fun fopen(mode, filename) { do Fopen(mode, filename) }
 
+sig fclose : (FileDescr) {Fclose:(FileDescr) -> () |_}-> ()
+fun fclose(fd) { do Fclose(fd) }
+
 typename File = Queue.T(String);
 
 sig emptyFile : File
@@ -165,33 +180,54 @@ fun readFile(file) {
   }
 }
 
-typename FileStore = [(FileDescr, File)];
+typename FileTable = [(FileDescr, File)];
+typename FileStore = [(String, FileDescr)];
+typename FileSystem = (next:Int,ft:FileTable,fs:FileStore);
 
-sig defaultStore : FileStore
-var defaultStore = [ (stdin , emptyFile)
+sig defaultFileSystem : () -> FileSystem
+fun defaultFileSystem() {
+  var defaultTable = [ (stdin , emptyFile)
                      , (stdout, emptyFile)
                      , (stderr, emptyFile) ];
 
-sig lookupFile : (FileDescr, FileStore) ~> File
-fun lookupFile(fd, fs) {
-   switch (lookup(fd, fs)) {
-     case Nothing -> error("No such file")
+  var defaultStore = [ ("stdin" , stdin)
+                     , ("stdout", stdout)
+                     , ("stderr", stderr) ];
+
+  (next=3,ft=defaultTable,fs=defaultStore)
+}
+
+sig lookupFile : (FileDescr, FileSystem) ~> File
+fun lookupFile(fd, fsys) {
+   switch (lookup(fd, fsys.ft)) {
+     case Nothing -> error("err: No such file(" ^^ intToString(fd) ^^ ")")
      case Just(file) -> file
    }
 }
 
-sig replaceFile : (FileDescr, File, FileStore) ~> FileStore
-fun replaceFile(fd, file, fs) {
-  switch (fs) {
-    case [] -> error("No such file")
-    case (fd', file') :: fs' ->
-      if (fd == fd') (fd, file) :: fs'
-      else (fd', file') :: replaceFile(fd, file, fs')
-  }
+sig replaceFile : (FileDescr, File, FileSystem) ~> FileSystem
+fun replaceFile(fd, file, fsys) {
+  var ft = modify(fd, file, fsys.ft);
+  (fsys with ft = ft) # TODO handle nonexistent file.
 }
 
-sig createFile : (FileDescr, FileStore) -> FileStore
-fun createFile(fd, fs) { (fd, emptyFile) :: fs }
+sig createFile : (String, FileSystem) -> (FileDescr, FileSystem)
+fun createFile(filename, fsys) {
+  var fd = fsys.next;
+  (fd, (next = fd + 1, fs = (filename, fd) :: fsys.fs, ft = (fd, emptyFile) :: fsys.ft))
+}
+
+sig openFile : (Mode, String, FileSystem) ~> (FileDescr, FileSystem)
+fun openFile(mode, filename, fsys) {
+  var (fd, fsys') = switch (lookup(filename, fsys.fs)) {
+      case Nothing -> createFile(filename, fsys)
+      case Just(fd) -> (fd, fsys)
+  };
+  switch (mode) {
+    case Create -> error("erase")
+    case Append -> (fd, fsys')
+  }
+}
 
 sig closeFile : (File) ~> File
 fun closeFile((=front,=rear)) {
@@ -201,17 +237,32 @@ fun closeFile((=front,=rear)) {
 sig allowState : (() {Get-,Put- |e}~> a) -> () {Get:s,Put:(s) -> () |e}~> a
 fun allowState(f) { (f : (() {Get:s,Put:(s) -> () |e}~> a) <- (() {Get-,Put- |e}~> a)) }
 
-sig fileIO : (Comp(a, {Get-,Put-,Gets:(FileDescr) -> String,Puts:(FileDescr,String) -> () |e})) {Get:() {}-> FileStore,Put:(FileStore) -> (),Gets{_},Puts{_} |e}~> a
+sig fileIO : (Comp(a, {Get-,Put-,Gets:(FileDescr) -> String,Puts:(FileDescr,String) -> (),Fclose:(FileDescr) -> (),Fopen:(Mode,String) -> FileDescr |e})) {Get:() {}-> FileSystem,Put:(FileSystem) -> (),Gets{_},Puts{_},Fclose{_},Fopen{_} |e}~> a
 fun fileIO(m) {
   handle(allowState(m)()) {
     case Gets(fd, resume) ->
-      var fs = get();
-      var (ch, file) = readFile(lookupFile(fd, fs));
-      put(replaceFile(fd, file, fs)); resume(ch)
+      var fsys = get();
+      var (ch, file) = readFile(lookupFile(fd, fsys));
+      put(replaceFile(fd, file, fsys)); resume(ch)
     case Puts(fd, ch, resume) ->
-      var fs = get();
-      var fs' = replaceFile(fd, writeFile(ch, lookupFile(fd, fs)), fs);
-      put(fs'); resume(())
+      var fsys = get();
+      var fsys' = replaceFile(fd, writeFile(ch, lookupFile(fd, fsys)), fsys);
+      put(fsys'); resume(())
+    case Fopen(mode, filename, resume) ->
+      var fsys = get();
+      var (fd, fsys') = openFile(mode, filename, fsys);
+      put(fsys'); resume(fd)
+    case Fclose(fd, resume) ->
+      var fsys = get();
+      var fsys' = replaceFile(fd, closeFile(lookupFile(fd, fsys)), fsys);
+      put(fsys'); resume(())
+  }
+}
+
+sig redirect : (Comp(a, {Puts:(FileDescr,String) -> () |e}), FileDescr) {Puts:(FileDescr,String) -> () |e}~> a
+fun redirect(m, fd) {
+  handle(m()) {
+    case Puts(_,s,resume) -> resume(puts(fd, s))
   }
 }
 
@@ -293,7 +344,11 @@ fun provenance(m) {
 sig example : () {Fork:Bool,Getenv:(String) -> String,Su:(User) -> (),Puts:(FileDescr,String) -> (),Yield:() |_}~> ()
 fun example() {
   var pid = fork();
-  var () = if (pid) su(Alice) else su(Bob);
+  var () = {
+    if (pid) redirect(fun(){puts(stdout, "dummy")}, stderr)
+    else if (fork()) su(Alice)
+    else su(Bob)
+  };
   var user = whoami();
   puts(stdout, "Hello World!");
   var uid = getenv("UID");
@@ -313,3 +368,33 @@ fun init() {
     })
   })
 }
+
+sig example' : () {Fork:Bool,Fclose:(FileDescr) -> (),Fopen:(Mode,String) -> FileDescr,Getenv:(String) -> String,Su:(User) -> (),Puts:(FileDescr,String) -> (),Yield:() |_}~> ()
+fun example'() {
+  var pid = fork();
+  var () = {
+    if (pid) redirect(fun(){puts(stdout, "dummy")}, stderr)
+    else if (fork()) su(Alice)
+    else su(Bob)
+  };
+  var user = whoami();
+  var fd = fopen(Append, user ^^ ".txt");
+  puts(fd, "Hello World!");
+  var uid = getenv("UID");
+  echo("My UID is " ^^ uid);
+  (if (amiroot()) { yield(); echo(user ^^ " is running as root.") } else ());
+  echo("My home dir is /home/" ^^ user);
+  fclose(fd)
+}
+
+
+sig init' : (FileSystem) {Fclose{_},Fopen{_},Fork{_},Get{_},Getenv{_},Gets{_},Put{_},Puts{_},Su{_},Yield{_}|_}~> ((), FileSystem)
+fun init'(fsys) {
+  runState(fsys, fun() {
+    fileIO(fun() {
+      schedule(fun() {
+        usermgr(Root, envs, example')
+      })
+    })
+  })
+}

thesis.bib

@@ -1004,3 +1004,15 @@
   publisher = {{ACM}},
   year      = {1998}
 }
+
+# Unix
+@article{RitchieT74,
+  author    = {Dennis Ritchie and
+               Ken Thompson},
+  title     = {The {UNIX} Time-Sharing System},
+  journal   = {Commun. {ACM}},
+  volume    = {17},
+  number    = {7},
+  pages     = {365--375},
+  year      = {1974}
+}