ATSLIB/prelude/filebas
The functions declared in this package are mostly provided
for the sake of convenience. For full-fledged IO support,
please see [ATSLIB/libc/SATS/stdio.sats].
Synopsis
fun{} dirsep_get ():<> charNZ
Description
This function returns the character for separating directory names
in a vaild path. In Unix-like systems, this character is the slash
symbol (/).
Synopsis
fun{} dirname_self ():<> string
Description
This function returns the name referring to the self directory, which
is "." by default.
Synopsis
fun{} dirname_parent ():<> string
Description
This function returns the name referring to the self directory, which
is ".." by default.
Synopsis
fun{}
filename_get_ext(name: string):<> vStrptr0
Synopsis
fun{}
filename_get_base (name: string):<> vStrptr1
Synopsis
fun
test_file_exists
(path: NSH(string)): bool = "mac#%"
Description
This function tests whether a given path refers to a file in existence.
Synopsis
fun{}
test_file_mode
(path: NSH(string)): int
Description
This function calls [stat] to obtain the mode of a given file and then
applies its second argument f to the mode to return an integer: ~1/0/1
means error/false/true, respectively.
Synopsis
fun
test_file_isblk(path: NSH(string)): int = "mac#%"
Synopsis
fun
test_file_ischr(path: NSH(string)): int = "mac#%"
Synopsis
fun
test_file_isdir(path: NSH(string)): int = "mac#%"
Synopsis
fun
test_file_isfifo(path: NSH(string)): int = "mac#%"
Synopsis
fun
test_file_isreg(path: NSH(string)): int = "mac#%"
Synopsis
fun
fileref_open_exn
(path: NSH(string), file_mode): FILEref = "mac#%"
Description
This function calls the libc-function fclose (declared in [stdio.h]) to create
a handle for the file referred to by its first argument path
and then set the mode of the created handle according to its second
argument fm. In case of a failure, a fatal non-catchable
exception is raised.
Synopsis
fun{}
fileref_open_opt
(path: NSH(string), file_mode): Option_vt(FILEref)
Description
This function is the optional version of fileref_open_exn: The
returned value is an option that indicates whether a call to
fileref_open_opt successfully yields a file handle or not.
Synopsis
fun
fileref_close(fil: FILEref): void = "mac#%"
Description
This function calls the libc-function fclose (declared in [stdio.h]) to close a
given file handle. Note that fileref_close does not report any
errors.
Synopsis
fun
fileref_flush(fil: FILEref): void = "mac#%"
Description
This function calls the libc-function fflush (declared in [stdio.h]) to flush a
given file handle. Note that fileref_flush does not report any
errors.
Synopsis
fun
fileref_getc(input: FILEref): int = "mac#%"
Description
This function reads a char from a given file handle. Note that the function
is based on the libc-function fgetc, and it returns a negative
integer (EOF) as an indication of error.
Synopsis
overload fileref_putc with fileref_putc_int
overload fileref_putc with fileref_putc_char
Synopsis
fun
fileref_putc_int
(out: FILEref, c: int): void = "mac#%"
Description
This function, which overloads the symbol fileref_putc, casts
its first argument into a char and then write the char to a given file
handle. Note that the function is based on the libc-function fputc,
and it does not report any errors.
Synopsis
fun
fileref_putc_char
(out: FILEref, c: char): void = "mac#%"
Description
This function, which overloads the symbol fileref_putc, writes
a char to a given file handle. Note that the function is based on the
libc-function fputc, and it does not report any errors.
Synopsis
fun
fileref_puts
(out: FILEref, NSH(string)): void = "mac#%"
Description
This function writes a string to a given file handle. Note that the
function is based on the libc-function fputs, and it does not
report any errors. The following code gives a reference implementation of
the function:
implement
fileref_puts
(out, str) = let
val str = g1ofg0_string(str)
implement{env}
string_foreach$cont (c, env) = true
implement{env}
string_foreach$fwork (c, env) = fileref_putc (out, c)
val _ = string_foreach (str)
in
end
Synopsis
fun
fileref_is_eof(inp: FILEref): bool = "mac#%"
Description
This function tests whether the end of a given file handle is reached. It
is based on the libc-function feof declared in [stdio.h].
Example
The following code gives a naive implementation of file-copying:
fun fprint_fileref
(
out: FILEref, inp: FILEref
) : void = let
in
if ~fileref_is_eof(inp) then let
val () = fileref_putc (out, fileref_getc (inp))
in
fprint_fileref (out, inp)
end else ()
end
implement
main () = let
val () = fprint_fileref (stdout_ref, stdin_ref) in 0
end
Synopsis
typedef
fileref_load_type(a:t@ype) =
(FILEref, &a? >> opt(a, b)) -<fun1> #[b:bool] bool(b)
Synopsis
fun{a:t0p}
fileref_load : fileref_load_type (a)
Description
This function loads a value from a given file handle into a given variable,
and returns a boolean to indicate whether loading is successful or not. It
is only implemented for certain template arguments.
Synopsis
fun
fileref_load_int : fileref_load_type(int) = "mac#%"
Description
This function is a specific instance of fileref_load for
loading a integer.
Synopsis
Synopsis for [fileref_load_char] is unavailable.
Description
This function is a specific instance of fileref_load for
loading a character.
Synopsis
fun
fileref_load_double : fileref_load_type(double) = "mac#%"
Description
This function is a specific instance of fileref_load for
loading a double-precision float.
Synopsis
Synopsis for [fileref_load_string] is unavailable.
Description
This function is a specific instance of fileref_load for
loading a doubly-quoted string.
Synopsis
fun{a:t0p}
fileref_get_optval
(inp: FILEref): Option_vt(a)
Description
This function reads a value from a given file handle. It is only
implemented for certain template arguments.
Synopsis
fun
fileref_get_line_charlst(inp: FILEref): charlst_vt
Description
This function reads chars from a given file handle until a newline
symbol or EOF is reached and it then returns a linear list of the chars in
the order they were read. Note that the newline symbol is not included in
the chars returned.
Synopsis
fun
fileref_get_lines_charlstlst(inp: FILEref): List0_vt(charlst_vt)
Description
This function returns a linear list consisting of all the lines read from a
given file handle. Note that each of the returned lines is obtained by
calling fileref_get_line_charlst.
Synopsis
fun{}
fileref_get_line_string(inp: FILEref): Strptr1
Description
This function returns a line read from a given file handle.
It is just a specialization of fileref_get_line_string_main,
and its implementation is given as follows:
implement{}
fileref_get_line_string
(filr) = let
var n: int
val str = fileref_get_line_string_main (filr, n)
prval () = lemma_strnptr_param (str)
in
strnptr2strptr (str)
end
Synopsis
fun{}
fileref_get_line_string_main
(
inp: FILEref, nchar: &int? >> int(n)
) : #[n:nat] strnptr(n)
Description
This function returns a line read from a given file handle and records
the length of the line in its second (call-by-reference) argument. Note
that the length information can only be trusted if there are no occurrences
of the NUL char in the line.
Synopsis
fun{}
fileref_get_lines_stringlst(inp: FILEref): List0_vt(Strptr1)
Description
This function returns a linear list consisting of all the lines read from a
given file handle. Note that each of the returned lines is obtained by
calling fileref_get_line_string.
Synopsis
fun{}
fileref_get_line_string$bufsize(): intGte(1)
Description
This function returns the size of the initial buffer to be used by
fileref_get_line_string. Note that
fileref_get_line_string can automatically increase the size of
the buffer it uses if the buffer is not large enough.
Synopsis
fun
fileref_get_file_charlst(inp: FILEref): List0_vt(char)
Description
This function reads chars from a given file handle until none is left
and it then returns a linear list of the chars in the order they were read.
Example
The following code prints out the content of a given file backwardly:
fun fprint_fileref_back
(out: FILEref, inp: FILEref): void = let
fun loop (cs: List_vt (char)):<cloref1> void =
case+ cs of
| ~list_vt_cons
(c, cs) => let
val () = fileref_putc (out, c) in loop (cs)
end
| ~list_vt_nil () => ()
val cs = fileref_get_file_charlst (inp)
in
loop (list_vt_reverse (cs))
end
implement
main () = let
val () = fprint_fileref_back (stdout_ref, stdin_ref) in 0
end
Synopsis
fun
fileref_get2_file_charlst(inp: FILEref, n: int): List0_vt(char)
Description
This function reads chars from a given file handle until either the number
of chars being read reaches n (the value of the second argument) or no
char is left. It then returns a linear list consisting of the chars in the
order they were read and also updates the second argument with the length
of the returned list, that is, the number of chars being actually read.
Synopsis
fun
fileref_put_charlst(inp: FILEref, cs: NSH(List(char))): void
Description
This function prints out the chars in its second argument to the file
handle provided as its first argument. Note that it does not report any
errors. Example
The following code removes every empty line in a given file:
staload UN = "prelude/SATS/unsafe.sats"
fun remove_empty_lines
(
out: FILEref, inp: FILEref, isfst: bool
) : void = let
val EOL = '\n'
val iseof = fileref_is_eof (inp)
in
if ~iseof then let
var isfst: bool = isfst
val cs =
fileref_get_line_charlst (inp)
val iscons = list_vt_is_cons (cs)
val () = if iscons then {
val () = if isfst then (isfst := false) else fileref_putc (out, EOL)
val () = fileref_put_charlst (out, $UN.list_vt2t (cs))
}
val () = list_vt_free (cs)
in
remove_empty_lines (out, inp, isfst)
end else ()
end
implement
main () = let
val () = remove_empty_lines (stdout_ref, stdin_ref, true)
in
0
end
Clearly, this is a wasteful and inefficient way of removing empty lines.
Synopsis
fun{}
fileref_foreach(inp: FILEref): void
Description
This function reads from a given file handle multiple characters and then
applies to them the function implemented by
fileref_foreach$fworkv. It does so repeatedly until it can read
no more characters from the file handle.
Synopsis
fun{
env:vt0p
} fileref_foreach_env(inp: FILEref, env: &(env) >> _): void
Description
This function does essentially the same as fileref_foreach
except for taking an additional argument that serves as an environment.
Actually, fileref_foreach is implemented as a special case of
fileref_foreach_env.
Synopsis
fun{}
fileref_foreach$bufsize(): sizeGte(1)
Description
This function determines the size of the buffer allocated for storing
characters during the evaluation of a call to fileref_foreach_env.
Synopsis
fun{
env:vt0p
} fileref_foreach$fwork(c: char, env: &(env) >> _): void
Description
This function is used in the default implementation of fileref_foreach$fworkv.
Synopsis
fun{
env:vt0p
} fileref_foreach$fworkv
{n:int} (arrayref(char, n), size_t(n), &(env) >> _): void
Description
This function is directly called in the implementation of fileref_foreach_env.