-- FileIOPrivate.mesa -- Last edited by -- MBrown on September 17, 1983 8:42 pm -- Teitelman on May 26, 1982 4:52 pm -- Last Edited by: Levin, September 22, 1983 2:48 pm DIRECTORY FS USING [Lock, OpenFile, StreamOptions], Rope USING [ROPE], VM USING [Interval]; FileIOPrivate: CEDAR DEFINITIONS = BEGIN ROPE: TYPE = Rope.ROPE; -- We model the behavior of a File IOStream with variables "file", "fileLen", and --"streamIndex", where -- file is an ARRAY [0..fileLen) OF CHAR -- streamIndex is an INT [0..fileLen] -- The real stream contains a lot of redundant state to make the frequently-used --operations GetChar and PutChar fast. We shall list some invariant properties of --this state below. These invariants hold on entry to and exit from each stream --operation. (Redundant properties, included for their intuitive value, are given in --parentheses.) -- We also define a piece of fictional state: trueDataBytesInBuffer. -- trueDataBytesInBuffer ::= MIN[bufferBytes, fileLen - firstByteInBuffer]. -- trueDataBytesInBuffer is too expensive for PutByte to maintain at all times, but it --is useful for other operations. DataHandle: TYPE = REF Data; FSDataHandle: TYPE = REF Data.fs; AlpineDataHandle: TYPE = REF Data.alpine; FileSystem: TYPE = {fs, alpine}; Data: TYPE = RECORD [ -- common part, followed by variant depending on FileSystem. -- order these components to optimize the code generated for GetChar and PutChar. index: CARDINAL _ 0, -- index is IN [0..bufferBytes]. -- didPut AND index >= dataBytesInBuffer => trueDataBytesInBuffer = index. dataBytesInBuffer: CARDINAL _ 0, -- dataBytesInBuffer is IN [0..trueDataBytesInBuffer] => IN [0..bufferBytes]. -- NOT didPut OR (didPut AND index <= dataBytesInBuffer) => -- trueDataBytesInBuffer = dataBytesInBuffer. bufferBytes: CARDINAL _ 0, -- (see buffer below). eofInBuffer: BOOL _ FALSE, -- eofInBuffer <=> fileLen <= firstFileByteInBuffer + bufferBytes. -- (this means fileLen = 0, or file[fileLen-1] is contained in the buffer. This --is a useful piece of redundant state; fortunately, none of the cheap operations --need to update it). didPut: BOOL _ FALSE, -- (somebody has done a Put and not updated dataBytesInBuffer, FileLength, and --bufferDirty). bufferDirty: BOOL _ FALSE, -- didPut OR bufferDirty => there exists some i IN [0..trueDataBytesInBuffer) such --that buffer[i] # file[i] as last read from file system. (Not maintained for --Pilot because of its mapped files.) accessRights: FS.Lock, streamOptions: FS.StreamOptions, tiogaReader: BOOL _ FALSE, -- TRUE iff file is being read as a Tioga file (reading the plain text only). --This implies that the file length shown in the stream is not the true file length, --but instead is the Tioga plain text length. streamIsClosed: BOOL _ FALSE, -- stream.Close[] was called. -- (all operations should now raise StreamError[streamClosed]). firstFileByteInBuffer: INT _ 0, -- streamIndex = firstFileByteInBuffer + index. -- firstFileByteInBuffer < fileLen OR firstFileByteInBuffer = fileLen = 0. -- firstFileByteInBuffer MOD bytesPerPage = 0. -- (buffer[0] is indentified with file[firstFileByteInBuffer]. There is always --one file byte in the buffer unless file is empty.) fileLength: INT _ 0, -- NOT didPut => fileLen = fileLength. -- didPut AND index > dataBytesInBuffer => fileLen = firstFileByteInBuffer + --index. buffer: LONG POINTER TO PACKED ARRAY [0..0) OF CHAR _ NIL, -- (the current stream buffer.) -- buffer is really PACKED ARRAY [0..bufferBytes) OF CHAR. -- file[firstFileByteInBuffer..firstFileByteInBuffer+trueDataBytesInBuffer) = -- buffer[0..trueDataBytesInBuffer) -- (in case of Pilot, buffer[0..bufferBytes) are always backed by pages of file.) bufferInterval: VM.Interval _ TRASH, -- (a space of length maxBufferPages pages for the stream buffer above. If buffer --= NIL, the space has not yet been created.) fileName: ROPE, body: SELECT type: FileSystem FROM fs => [ fileHandle: FS.OpenFile, byteLength: INT, --current value of fileHandle.OpenInfo[].bytes byteSize: INT --current value of fileHandle.OpenInfo[].pages*bytesPerPage ], alpine => [ fileHandle: REF ANY, --AlpFile.Handle (includes transaction) byteLength: INT, --current value of fileHandle.ReadProperties[[byteLength: TRUE]] byteSize: INT --current value of fileHandle.GetSize[]*bytesPerPage ], ENDCASE]; END. CHANGE LOG Created by MBrown on December 12, 1980 12:04 PM Changed by MBrown on January 6, 1981 8:53 PM -- Added Invalidate, added trans field to pilot data. Changed by MBrown on January 16, 1981 10:00 AM -- DataObject is now defined without using a Stream.Handle (copied structure from --FileStreamImpl). Changed by MBrown on January 18, 1981 1:00 AM -- LeaderPage now defined here (but it uses something called FileStream.Subtype for its --"dataType" field). Changed by MBrown on 18-Jan-81 16:49:31 -- Added bufferDirty (for juniper stream use). and streamIsClosed (for diagnosis from --the debugger). Improved the description of invariants. Changed by MBrown on January 21, 1981 3:45 PM -- Complete re-think of Pilot FileStream state, to make Put faster and generally reduce --the number of expensive conversions betweeen pages and bytes. Not yet implemented. Changed by MBrown on January 22, 1981 3:12 PM -- Improved comments on invariants. Changed by MBrown on January 25, 1981 8:19 PM -- Added Juniper variant of Data. Changed by MBrown on 27-Jan-81 15:10:07 -- FileByteStreamJuniper -> Juniper. Changed by MBrown on 29-Jan-81 20:43:05 -- Added JOpen, POpen. Changed by Russ Atkinson on 26-May-81 14:07:10 -- CedarString -> Rope, LONG CARDINAL -> LONG INTEGER Changed by MBrown on 7-Dec-81 10:30:56 -- Conversion to IO, INT, ROPE, etc. Changed by MBrown on March 26, 1982 4:40 pm -- Added tiogaReader field (this is redundant, but may be useful for debugging), and the --IsThisThingATiogaFile proc. Changed by Teitelman on May 26, 1982 4:52 pm -- changed to safe language, name change IOStream -> IO. Changed by MBrown on August 23, 1982 2:18 pm -- Eliminated TEXTDataOffset, added bufferParms, renamed JOpen -> JuniperOpen, --POpen -> ComSoftOpen, added CIFSOpen, added CIFS open file to pilot variant of Data. Changed by MBrown on May 16, 1983 2:03 pm -- Eliminated Juniper stuff, added Alpine stuff. Changed by MBrown on June 22, 1983 11:29 am -- Eliminated Pilot stuff, added FS stuff. Changed by MBrown on September 17, 1983 8:42 pm -- Eliminated all procs, since file stream impl is one module (FS).