# Tiny UNIX revision 2.

sig str : ((a, [Char])) ~> (a, String)
fun str((x, cs)) { (x, implode(cs)) }

typename Option(a) = [|None|Some:a|];

sig lookup : (a, [(a, b)]) ~> Option(b)
fun lookup(k, kvs) {
  switch (kvs) {
    case [] -> None
    case (k', v) :: kvs' ->
      if (k == k') Some(v)
      else lookup(k, kvs')
  }
}

sig modify : (a, b, [(a, b)]) ~> [(a, b)]
fun modify(k, v, kvs) {
  switch (kvs) {
    case [] -> []
    case (k', v') :: kvs' ->
      if (k == k') (k, v) :: kvs'
      else (k', v') :: modify(k, v, kvs')
  }
}

sig remove : (a, [(a, b)]) ~> [(a, b)]
fun remove(k, kvs) {
  switch (kvs) {
    case [] -> []
    case (k', v') :: kvs' ->
      if (k == k') kvs'
      else (k', v') :: remove(k, kvs')
  }
}

sig fromSome : (Option(a)) ~> a
fun fromSome(x) {
  switch (x) {
    case None -> error("fromSome")
    case Some(x) -> x
  }
}

##
## Basic i/o
##
typename File = [Char];
typename FileDescr = Int;

sig stdout : FileDescr
var stdout = 1;

sig basicIO : (Comp(a, {Putc:(FileDescr,Char) -> () |e})) {Putc{_} |e}~> (a, File)
fun basicIO(m) {
  handle(m()) {
    case Return(res) -> (res, [])
    case Putc(_, c, resume) ->
      var (res, file) = resume(());
      (res, c :: file)
  }
}

sig echo : (String) {Putc:(FileDescr,Char) -> () |_}~> ()
fun echo(cs) { iter(fun(c) { do Putc(stdout, c) }, explode(cs)) }

fun example0() {
  str(basicIO(fun() {
        echo("Hello"); echo("World")
  }))
}

##
## Exceptions: non-local exits
##
sig exit : (Int) {Exit:(Int) -> Zero |_}-> a
fun exit(n) { switch(do Exit(n)) {} }

sig status : (Comp(a, {Exit:(Int) -> Zero |e})) {Exit{_} |e}~> Int
fun status(m) {
  handle(m()) {
    case Return(_) -> 0
    case Exit(n, _) -> n
  }
}

fun example1() {
  str(basicIO(fun() {
        status(fun() {
          echo("dead"); exit(1); echo("code")
        })
  }))
}

##
## Dynamic binding: user-specific environments.
##
typename User = [|Alice|Bob|Root|];

sig whoami : () {Ask:String |_}-> String
fun whoami() { do Ask }

sig env : (User, Comp(a, {Ask:String |e})) {Ask{_} |e}~> a
fun env(user, m) {
  handle(m()) {
    case Return(x) -> x
    case Ask(resume) ->
      switch (user) {
        case Alice -> resume("alice")
        case Bob   -> resume("bob")
        case Root  -> resume("root")
      }
  }
}

fun example2() {
  env(Root, whoami)
}

###
### Session management.
###
sig su : (User) {Su:(User) -> () |_}-> ()
fun su(user) { do Su(user) }

sig sessionmgr : (User, Comp(a, {Ask:String,Su:(User) -> () |e})) {Ask{_},Su{_} |e}~> a
fun sessionmgr(user, m) {
  env(user, fun() {
     handle(m()) {
       case Return(x) -> x
       case Su(user', resume) ->
         env(user', fun() { resume(()) })
     }
  })
}

fun example3() {
  str(basicIO(fun() {
        sessionmgr(Root, fun() {
          status(fun() {
            su(Alice); echo(whoami()); echo(" ");
            su(Bob);   echo(whoami()); echo(" ");
            su(Root);  echo(whoami())
          })
        })
  }))
}

##
## Nondeterminism: time sharing.
##
sig fork : () {Fork:Bool |_}-> Bool
fun fork() { do Fork }

sig nondet : (Comp(a, {Fork:Bool |e})) {Fork{_} |e}~> [a]
fun nondet(m) {
  handle(m()) {
    case Return(res) -> [res]
    case Fork(resume) -> resume(true) ++ resume(false)
  }
}

sig interrupt : () {Interrupt:() |_}-> ()
fun interrupt() { do Interrupt }

typename Pstate(a,e::Eff) = forall q::Presence.
                            [|Done:a
                             |Paused:() {Interrupt{q} |e}~> Pstate(a, { |e})|];

sig slice : (Comp(a, {Interrupt:() |e})) {Interrupt{_} |e}~> Pstate(a, { |e})
fun slice(m) {
  handle(m()) {
    case Return(res) -> Done(res)
    case Interrupt(resume) -> Paused(fun() { resume(()) })
  }
}

sig runNext : ([Pstate(a, { Fork:Bool |e})]) {Fork{_},Interrupt{_} |e}~> [a]
fun runNext(ps) {
  sig run : (Pstate (a, { Fork:() {}-> Bool|e })) {Fork{_},Interrupt{_} |e}~> [a]
  fun run(p) {
    switch(p) {
      case Done(res) -> [res]
      case Paused(resume) -> runNext(nondet(resume))
    }
  }
  concatMap(run, ps)
}

sig timeshare : (Comp(a, {Fork:Bool,Interrupt:() |e})) {Fork{_},Interrupt{_} |e}~> [a]
fun timeshare(m) {
  var p = Paused(fun() { slice(m) });
  runNext([p])
}

fun example4() {
  str(basicIO(fun() {
        timeshare(fun() {
          sessionmgr(Root, fun() {
            status(fun() {
              var parent = fork();
              (if (parent) su(Alice) else su(Bob));
              echo(whoami() ^^ "> Hello ");
              interrupt();
              echo(whoami() ^^ "> Bye ");
              interrupt();
              if (parent) exit(0)
              else {
                var parent = fork();
                interrupt();
                (if (parent) su(Root)
                 else {
                  echo(whoami() ^^ "> oops ");
                  exit(1)
                });
                echo(whoami() ^^ "> !! ")
              }
            })
          })
        })
      }))
}

##
## Generic state handling
##
sig get : () {Get:s |_}-> s
fun get() { do Get }

sig put : (s) {Put:(s) -> () |_}-> ()
fun put(st) { do Put(st) }

sig runState : (s, Comp(a, {Get:() -> s,Put:(s) -> () |e})) {Get{_},Put{_} |e}~> (a, s)
fun runState(st0, m) {
  var f = handle(m()) {
    case Return(x) -> fun(st) { (x, st) }
    case Get(resume) -> fun(st) { resume(st)(st) }
    case Put(st,resume) -> fun(_) { resume(())(st) }
  };
  f(st0)
}

##
## State: file i/o
##
typename INode      = (loc:Int,lno:Int);
typename IList      = [(Int, INode)];  # INode index -> INode
typename Directory  = [(String, Int)]; # Filename -> INode index
typename DataRegion = [(Int, File)];   # Loc -> File

typename FileSystem = (dir:Directory,dregion:DataRegion,inodes:IList
                                    ,lnext:Int         ,inext:Int    );


sig falloc : (String, FileSystem) ~> (Int, FileSystem)
fun falloc(fname, fsys) {
  var loc = fsys.lnext;
  var dregion = (loc, []) :: fsys.dregion;

  var i   = fsys.inext;
  var inode = (loc=loc,lno=1);
  var inodes = (i, inode) :: fsys.inodes;

  var dir = (fname, i) :: fsys.dir;
  (i, (=dir,=dregion,=inodes,lnext=loc+1,inext=i+1))
}

typename WriteMode = [|Create|Append|];

sig fwrite : (WriteMode, String, [Char], FileSystem) ~> FileSystem
fun fwrite(mode,fname, cs, fsys) {
  var (ino,fsys') = switch (lookup(fname, fsys.dir)) {
     case None    -> falloc(fname, fsys)
     case Some(i) -> (i,fsys)
  };
  var inode = fromSome(lookup(ino, fsys'.inodes));
  var file = fromSome(lookup(inode.loc, fsys'.dregion));
  var file' = switch (mode) {
     case Create -> cs
     case Append -> file ++ cs
  };
  (fsys' with dregion = modify(inode.loc, file, fsys'.dregion))
}

sig fread : (String, FileSystem) ~> Option([Char])
fun fread(fname, fsys) {
  switch (lookup(fname, fsys.dir)) {
    case None    -> None
    case Some(i) ->
      var inode = fromSome(lookup(i, fsys.inodes));
      lookup(inode.loc, fsys.dregion)
  }
}

sig flink : (String, String, FileSystem) ~> Option(FileSystem)
fun flink(src, dest, fsys) {
  switch (lookup(dest, fsys.dir)) {
    case None -> None
    case Some(i) ->
      var inode  = fromSome(lookup(i, fsys.inodes));
      var inode  = (inode with lno = inode.lno + 1);
      var inodes = modify(i, inode, fsys.inodes);

      var dir    = (src, i) :: fsys.dir;
      Some((fsys with inodes = inodes, dir = dir))
  }
}

sig funlink : (String, FileSystem) ~> Option(FileSystem)
fun funlink(fname, fsys) {
  switch (lookup(fname, fsys.dir)) {
    case None -> None
    case Some(i) ->
      var dir = remove(fname, fsys.dir);

      var inode  = fromSome(lookup(i, fsys.inodes));
      var inode  = (inode with lno = inode.lno - 1);

      if (inode.lno > 0) {
        var inodes = modify(i, inode, fsys.inodes);
        Some((fsys with inodes = inodes, dir = dir))
      } else {
        var dregion = remove(inode.loc, fsys.dregion);
        var inodes = remove(i, fsys.inodes);
        Some((fsys with inodes = inodes, dir = dir, dregion = dregion))
      }
  }
}