filename: operations on file names

value current_dir_name : string
The conventional name for the current directory (e.g. . in Unix).
value concat : string -> string -> string
concat dir file returns a file name that designates file file in directory dir.
value is_absolute : string -> bool
Return true if the file name is absolute or starts with an explicit reference to the current directory (./ or ../ in Unix), and false if it is relative to the current directory.
value check_suffix : string -> string -> bool
check_suffix name suff returns true if the filename name ends with the suffix suff.
value chop_suffix : string -> string -> string
chop_suffix name suff removes the suffix suff from the filename name. The behavior is undefined if name does not end with the suffix suff.
value basename : string -> string
value dirname : string -> string
Split a file name into directory name / base file name. concat (dirname name) (basename name) returns a file name which is equivalent to name. Moreover, after setting the current directory to dirname name (with sys__chdir), references to basename name (which is a relative file name) designate the same file as name before the call to chdir.