SIGNATURE BinFile[data]

-- low-level binary file I/O of (nearly) arbitrary data objects 

SORT data

IMPORT  Void            ONLY void            
        Com[void]       ONLY com
        Com[data]       ONLY com ans
        File            ONLY file

FUN write : file ** denotation ** data -> com[void]
    -- write data to output, tagging it with denotation

FUN read : file ** denotation -> com[data]
    -- read data from input which was written with given tag

FUN tagMismatches? : ans[data] -> bool
    -- check for failure because of tag mismatch on read

FUN invalidFormat? : ans[data] -> bool
    -- check for failure because of invalid format on read

FUN cannotLinkFun?    : ans[data] -> bool
    -- check for failure of runtime linkage of a function 

/* NB. Strong typing is violated by this functions. The user
       is responsible to perform type checks using the supplied
       string tags.

       A tag mismatch error has the format
       "binary IO tag mismatches, found '%%', expected '&&'"
       %% is the tag found in the file,
       && is the tag given in the call of read,
       both contain also the internal tag

       On some systems binary IO objects may contain functions;
       a functions code is dynamically linked to the running process.
       See system dependend documentation.
*/