DEFINITION MODULE FileIO;

(* Driver for File Based IO *)

(* This module interprets the contents of files as a stream of octets without
   any particular structure. The module represents the lowest level interface
   for file based IO in the standard library. *)

FROM Integers IMPORT CARDINAL64; (* assuming 64-bit file systems *)


(* File accessor, file status and file mode *)

TYPE
    File = OPAQUE; (* implementation defined file accessor *)

    Status = ( success,               (* operation completed successfully   *)
               invalidAccessor,       (* the passed in accessor is invalid  *)
               fileNotFound,          (* no file found with this filename   *)
               nameTooLong,           (* the passed in filename is too long *)
               invalidName,           (* the passed in filename is invalid  *)
               invalidMode,           (* the passed in mode is invalid      *)
               alreadyOpen,           (* the passed in file is already open *)
               accessDenied,          (* the filesystem denied file access  *)
               accessBeyondEOF,       (* attempt to read past end of file   *)
               fileSizeLimitExceeded, (* attempt to write past size limit   *)
               openFileLimitExceeded, (* attempt to open too many files     *)
               deviceFull,            (* the device capacity is exceeded    *)
               deviceError );         (* the device reported a failure      *)

    Mode = SET OF ( read,             (* reading is permitted if set        *)
                    write,            (* writing is permitted if set        *)
                    append,           (* writing always appends if set      *)
                    sync );           (* writing always flushes if set      *)


(* Alias types for implementation dependent file position and file size *)

    FilePos = ALIAS OF CARDINAL64;
    FileSize = ALIAS OF CARDINAL64;


(* Predefined file modes *)

CONST
    write = { Mode.write };
    readOnly = { Mode.read };
    readWrite = { Mode.read, Mode.write };
    append = { Mode.write, Mode.append };

    defaultBufferSize = <implementation defined value>;


(* Predefined open file accessors *)

VAR
    stdIn, stdOut, stdErr, nullFile : File;


(* Opening files *)

PROCEDURE Open ( VAR file       : File;
                 CONST filename : ARRAY OF CHAR;
                 mode           : Mode;
                 VAR status     : Status );
(* Opens the file <filename> in file mode <mode>. If sucessful passes a file
   accessor back in <file>, otherwise passes NIL back in <file>. The status of
   the operation is passed back in <status>. *)

PROCEDURE OpenWithBuffer ( VAR file         : File;
                           CONST filename   : ARRAY OF CHAR;
                           mode             : Mode;
                           VAR buffer       : ARRAY OF OCTET;
                           VAR status       : Status );
(* Opens the file <filename> in file mode <mode> using <buffer> as a custom
   file buffer. If successful passes a file accessor back in <file>, otherwise
   passes NIL back in <file>. The status is passed back in <status>. *)

PROCEDURE ReOpen ( VAR file : File; mode : Mode );
(* Closes the file associated with <file> and reopens it in mode <mode>.*)


(* File mode, status and name *)

PROCEDURE ModeOf ( file : File ) : Mode;
(* Returns the file mode of file accessor <file>.
   Returns an empty set if <file> is invalid. *)

PROCEDURE StatusOf ( file : File ) : Status;
(* Returns the status of the most recent operation for file accessor <file>.*)

PROCEDURE GetName ( file : File; VAR filename : ARRAY OF CHAR );
(* Passes the name of the file associated with <file> back in <filename>.
   Passes an empty string if <file> is invalid or if the name exceeds the
   capacity of <filename>. *)


(* File position operations *)

PROCEDURE EOF ( file : File ) : BOOLEAN;
(* Returns TRUE if the end of the file associated with file accessor <file>
   has been reached, otherwise FALSE. *)

PROCEDURE CurrentPos ( file : File ) : FilePos;
(* Returns the current read/write position for file accessor <file>. *)

PROCEDURE SetPos ( file : File; index : FilePos );
(* Sets the read/write position for file accessor <file> to <index>. *)

PROCEDURE Advance ( file : File; offset : FilePos );
(* Advances the read/write position for file accessor <file> by <offset>. *)

PROCEDURE Rewind ( file : File );
(* Sets the read/write position for file accessor <file> to the beginning of
   the file and resets its end-of-file status. *)


(* Read and write operations *)

PROCEDURE Read ( file : File; VAR data : OCTET );
(* Reads one octet of data at the current position of <file>, passes it back
   in <data> and advances the read/write position of <file> by one. *)

PROCEDURE Lookahead ( file : File; VAR data : OCTET );
(* Passes in <data> the octet that is going to be read next by procedure Read.
   Procedure Lookahead does not update the read/write position of <file>. *)

PROCEDURE Write ( file : File; data : OCTET );
(* Performs a write or append operation depending on the mode of <file>.
   In write mode, the procedure writes one octet in <data> to the current
   position of <file>. In append mode, the procedure atomically sets the
   current read/write position of <file> to the end of the file and appends
   one octet in <data> to the end of the file. In either mode, the current
   read/write position of <file> is advanced by one after the data has been
   written. *)

PROCEDURE ReadBlock ( file : File;
                      VAR data : ARRAY OF OCTET; VAR octetsRead : FileSize );
(* Reads a block of data at the current position of <file>. Passes the block
   of data back in <data> and the number of octets read in <octetsRead>.
   The read/write position of <file> is advanced accordingly. *)

PROCEDURE WriteBlock ( file : File;
                       data : ARRAY OF OCTET; VAR octetsWritten : FileSize );
(* Performs a write or append operation depending on the mode of <file>.
   In write mode, the procedure writes the block of data passed in <data>
   starting at the current read/write position of <file>. In append mode, the
   procedure atomically sets the current read/write position of <file> to the
   end of the file and appends the block of data passed in <data> to the end
   of the file. In either mode, the current read/write position of <file> is
   advanced by the number of octets written and the number of octets written
   is passed back in <octetsWritten> after the data has been written. *)

PROCEDURE Flush ( file : File );
(* Writes unwritten data in the buffer of <file> to its associated file. *)


(* Closing files *)

PROCEDURE Close ( VAR file : File; VAR status : Status );
(* Performs Flush on <file> and closes the associated file. Passes NIL back
   in <file>. The status of the operation is passed back in <status>. *)

END FileIO.