library MKDS version 0.0

%% Mein kleines Dateisystem

from Basic/StructuredDatatypes get String
from Basic/Numbers get Nat,Int
from Basic/StructuredDatatypes get FiniteMap
from States get Stateful,Ref,Maybe,Unit
from IO get IOsort,IO,IORef


spec MKDS =
Int then
    sorts FS, Name, Data
then
    Maybe[sort Data]
and Stateful[sort FS][sort Maybe[Data]]
and Stateful[sort FS][sort Unit]
and Stateful[sort FS][sort Int]
then
ops
   createFS : FS;
   readFS   : FS* Name-> St[FS,Maybe[Data]];
   writeFS  : FS* Name* Data-> St[FS, Unit];
   statFS   : FS* Name-> St[FS, Int]

   forall f: FS; n, m: Name; d: Data

   . data(readFS(state(writeFS(f, n, d)), n))= just(d)
   . state(readFS(state(writeFS(f, n, d)), m))= 
       state(writeFS(state(readFS(f, m)), n, d)) if not (m= n)
   . data(statFS(state(readFS(f, n)), n))= data(statFS(f, n)) + 1
   . data(statFS(state(readFS(f, m)), n))= data(statFS(f, n))  if (not (m= n))
   . data(statFS(state(writeFS(f, m, d)), n))= data(statFS(f, n))
   . data(statFS(createFS, n))= 0
end


%% implementing MKDS

spec MKDSimpl = 
IO and Nat and Int then 
     sorts Name = String;
           Data = String;
then FiniteMap[sort Name fit S |-> Name][sort Int fit T |-> Int]
and  IORef[sort FiniteMap[Name, Int]]
and  Stateful[sort World][sort IORef[FiniteMap[Name, Int]]]
and  Maybe[sort Data]
and  IOsort[sort Maybe[Data]]
and  IOsort[sort Unit]
and  IOsort[sort Int]
then
   sorts FS = IORef[FiniteMap[Name, Int]]
then
   IOsort[sort FS]
then
ops
   createFS : World-> IO[FS];
   readFS   : World* FS* Name-> IO[Maybe[Data]];
   writeFS  : World* FS* Name* Data-> IO[Unit];
   statFS   : World* FS* Name-> IO[Int];

   lookup   : FiniteMap[Name, Int]* Name-> Int

   forall w, w', w'', w''', w4, w5: World; r: IORef[FiniteMap[Name, Int]];
          fd: FD; u:Unit; n: Name; d: Data; md: Maybe[Data]; 
          fm : FiniteMap[Name, Int]
   . newIORef(w, [])= st(w', r) => createFS(w) = st(w', r)
%% Bizarrely, this line gies a "type mismatch" error:
%%  . createFS(w) = newIORef(w, []) 


   %% Implement writeFS(file, data) by 
   %% fd= open(file, CREATE); 
   %% write(fd, data); 
   %% close(fd);
   . open(w, n, CREATE)= st(w', just(fd)) /\
     write(w', fd, d)= st(w'', just(u)) /\
     close(w'', fd)= st(w''', u) => 
        writeFS(w, r, n, d)= st(w''', u)

   %% Implement readFS(file) by
   %% fd= open(file, READ);
   %% data= read(fd);
   %% close(fd);
   %% count[file]++;
   %% (Note we need to keep track of how often a file is accessed.)
   . open(w, n, READ)= st(w', just(fd)) /\
     read(w', fd)= st(w'', md) /\
     close(w'', fd)= st(w''', u) /\ 
     getIORef(w''', r)= st(w4, fm) /\
     setIORef(w4, r, fm[(lookup(fm, n)+1)/n])= st(w5, u) =>
        readFS(w, r, n)= st(w5, md)
   
   . lookup(fm, n)= eval(n, fm) if def (eval(n, fm))
   . lookup(fm, n)= 0           if not (def (eval (n, fm)))

   . getIORef(w, r)= st(w', fm) =>
     statFS(w, r, n) = st(w', lookup(fm, n))

end