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].


  • dirsep_get
  • dirname_self
  • dirname_parent
  • filename_get_ext
  • filename_get_base
  • test_file_exists
  • test_file_mode
  • test_file_isblk
  • test_file_ischr
  • test_file_isdir
  • test_file_isfifo
  • test_file_isreg
  • fileref_open_exn
  • fileref_open_opt
  • fileref_close
  • fileref_flush
  • fileref_getc
  • fileref_putc
  • fileref_putc_int
  • fileref_putc_char
  • fileref_puts
  • fileref_is_eof
  • fileref_load_type
  • fileref_load
  • fileref_load_int
  • fileref_load_char
  • fileref_load_double
  • fileref_load_string
  • fileref_get_optval
  • fileref_get_line_charlst
  • fileref_get_lines_charlstlst
  • fileref_get_line_string
  • fileref_get_line_string_main
  • fileref_get_lines_stringlst
  • fileref_get_line_string$bufsize
  • fileref_get_file_charlst
  • fileref_get2_file_charlst
  • fileref_put_charlst
  • fileref_foreach
  • fileref_foreach_env
  • fileref_foreach$bufsize
  • fileref_foreach$fwork
  • fileref_foreach$fworkv
  • Overloaded Symbols

  • dirsep_get

    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 (/).

    dirname_self

    Synopsis

    fun{} dirname_self ():<> string

    Description

    This function returns the name referring to the self directory, which is "." by default.

    dirname_parent

    Synopsis

    fun{} dirname_parent ():<> string

    Description

    This function returns the name referring to the self directory, which is ".." by default.

    filename_get_ext

    Synopsis

    fun{}
    filename_get_ext (name: string):<> vStrptr0

    filename_get_base

    Synopsis

    fun{}
    filename_get_base (name: string):<> vStrptr1

    test_file_exists

    Synopsis

    fun
    test_file_exists
      (path: NSH(string)): bool = "mac#%"

    Description

    This function tests whether a given path refers to a file in existence.

    test_file_mode

    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.

    test_file_isblk

    Synopsis

    fun
    test_file_isblk(path: NSH(string)): int = "mac#%"

    test_file_ischr

    Synopsis

    fun
    test_file_ischr(path: NSH(string)): int = "mac#%"

    test_file_isdir

    Synopsis

    fun
    test_file_isdir(path: NSH(string)): int = "mac#%"

    test_file_isfifo

    Synopsis

    fun
    test_file_isfifo(path: NSH(string)): int = "mac#%"

    test_file_isreg

    Synopsis

    fun
    test_file_isreg(path: NSH(string)): int = "mac#%"

    fileref_open_exn

    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.

    fileref_open_opt

    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.

    fileref_close

    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.

    fileref_flush

    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.

    fileref_getc

    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.

    fileref_putc

    Synopsis

    overload fileref_putc with fileref_putc_int
    overload fileref_putc with fileref_putc_char

    fileref_putc_int

    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.

    fileref_putc_char

    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.

    fileref_puts

    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
      // nothing
    end // end of [fileref_puts]
    

    fileref_is_eof

    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 of [if]
    end // end of [fprint_fileref]
    
    implement
    main () = let
      val () = fprint_fileref (stdout_ref, stdin_ref) in 0(*normal*)
    end // end of [main]
    

    fileref_load_type

    Synopsis

    typedef
    fileref_load_type(a:t@ype) =
      (FILEref, &a? >> opt (a, b)) -<fun1> #[b:bool] bool (b)

    fileref_load

    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.

    fileref_load_int

    Synopsis

    fun
    fileref_load_int : fileref_load_type (int) = "mac#%"

    Description

    This function is a specific instance of fileref_load for loading a integer.

    fileref_load_char

    Synopsis

    Synopsis for [fileref_load_char] is unavailable.

    Description

    This function is a specific instance of fileref_load for loading a character.

    fileref_load_double

    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.

    fileref_load_string

    Synopsis

    Synopsis for [fileref_load_string] is unavailable.

    Description

    This function is a specific instance of fileref_load for loading a doubly-quoted string.

    fileref_get_optval

    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.

    fileref_get_line_charlst

    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.

    fileref_get_lines_charlstlst

    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.

    fileref_get_line_string

    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 // uninitialized
      val str = fileref_get_line_string_main (filr, n)
      prval () = lemma_strnptr_param (str)
    in
      strnptr2strptr (str)
    end // end of [fileref_get_line_string]
    

    fileref_get_line_string_main

    Synopsis

    fun{}
    fileref_get_line_string_main
    (
      inp: FILEref, nchar: &int? >> int(n)
    ) : #[n:nat] strnptr(n) // end-of-function

    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.

    fileref_get_lines_stringlst

    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.

    fileref_get_line_string$bufsize

    Synopsis

    fun{}
    fileref_get_line_string$bufsize((*void*)): 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.

    fileref_get_file_charlst

    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 // end of [list_vt_cons]
        | ~list_vt_nil () => ()
      // end of [loop]
      val cs = fileref_get_file_charlst (inp)
    in
      loop (list_vt_reverse (cs))
    end // end of [fprint_fileref_back]
    
    implement
    main () = let
      val () = fprint_fileref_back (stdout_ref, stdin_ref) in 0(*normal*)
    end // end of [main]
    

    fileref_get2_file_charlst

    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.

    fileref_put_charlst

    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)
      // end of [val]
      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))
      } // end of [if] // end of [val]
      val () = list_vt_free (cs)
    in
      remove_empty_lines (out, inp, isfst)
    end else () // end of [if]
    //
    end // end of [remove_empty_lines]
    
    implement
    main () = let
      val () = remove_empty_lines (stdout_ref, stdin_ref, true(*isfst*))
    in
      0(*normal*)
    end // end of [main]
    
    Clearly, this is a wasteful and inefficient way of removing empty lines.

    fileref_foreach

    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.

    fileref_foreach_env

    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.

    fileref_foreach$bufsize

    Synopsis

    fun{}
    fileref_foreach$bufsize((*void*)): 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.

    fileref_foreach$fwork

    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.

    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.

    Overloaded Symbols


    This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi. SourceForge.net Logo