library IO version 0.0

%% CASL I/O!
%% A. N. Other

from Basic/StructuredDatatypes get String
from States get Stateful,Ref,Maybe

spec IOsort[sort S] =
   sort World
then 
   Stateful[sort World][sort S]
with
   sorts St[World,S] |-> IO[S]
end

spec IORef[sort S] = 
   sort World
then 
   Ref[sort World][sort S]
with 
   sort Ref[S] |-> IORef[S],
   ops  newRef |-> newIORef,
        getRef |-> getIORef,
	setRef |-> setIORef
end


spec IO =
   sorts Filepath = String;
         Data;
   free type Errno ::= EPERM | EBADF | EINVAL
then 
    Maybe [sort Filepath]
and IOsort[sort Maybe[Filepath]]
and Maybe [sort FD]
and IOsort[sort Maybe[FD]]
and Maybe [sort Data]
and IOsort[sort Maybe[Data]]
and Maybe [sort Unit]
and IOsort[sort Maybe[Unit]]
and IOsort[sort Unit]
and IORef [sort Errno]

then 
   free type Mode ::= READ | WRITE | CREATE

   ops open  : World* Filepath * Mode -> IO[Maybe[FD]];
       close : World* FD-> IO[Unit];
       read  : World* FD -> IO[Maybe[Data]];
       write : World* FD* Data -> IO[Maybe [Unit]];
   
       errno : IORef[Errno];
 
   forall w,w',w'',w''', w'''': World; 
          name: String; u: Unit; cont: Data; m: Mode; fd1, fd2: FD

   . (data(open(w, name, READ))= nothing)=> 
          data(open(w, name, WRITE))= nothing

   . open(w, name, m)= st(w', just (fd1)) /\
     write(w', fd1, cont)= st(w'', just(u)) /\
     close(w'', fd1) = st(w''', u) /\
     open(w''', name, READ)= st(w'''', just (fd2)) =>
     val(data(read(w'''', fd2)))= cont
	  
   %% and so on and so forth :-) 

end