module system/posix/file
imports
  system/posix/error
  term/string

/**
 * Standard file descriptors
 */
strategies 

  // Standard input, equal to <fileno> stdin
  STDIN_FILENO =
    prim("SSL_STDIN_FILENO")
    
  // Standard output, equal to <fileno> stdout
  STDOUT_FILENO =
    prim("SSL_STDOUT_FILENO")
    
  // Standard error output, equal to <fileno> stderr
  STDERR_FILENO =
    prim("SSL_STDERR_FILENO")

/**
 * Terminal I/O
 */
strategies

  /**
   * Succeeds if file descriptor refers to a terminal device.
   */
  isatty =
    ?filedes; prim("SSL_isatty", filedes) => 1

/**
 * These  functions  return  information  about the specified
 * file.  You do not need any access rights to  the  file  to
 * get  this  information  but  you need search rights to all
 * directories named in the path leading to the file.
 */
strategies

  modification-time =
    ?file; prim("SSL_modification_time", file)

/**
 * File operations
 */
strategies

 /**
  * link-file creats a hard link from file 'new' to file 'old'.
  */
  link-file =
    ?(old, new); prim("SSL_link", old, new)

/**
 * Directories
 */
strategies

 /**
  * The  readdir()  function  returns  a  pointer  to a dirent
  * structure representing the next  directory  entry  in  the
  * directory  stream  pointed  to by dir.  It returns NULL on
  * reaching the end-of-file or if an error occurred. 
  */
  readdir = 
    ?dir; prim("SSL_readdir", dir)

  /**
   * Returns the current working directory.
   */
  getcwd =
    prim("SSL_getcwd")

  /**
   * Change current working directory.
   *
   * @type String -> String
   */
  chdir =
    ?pathname; prim("SSL_chdir", pathname) => 0
    <+ <conc-strings; perror; fail> ("SSL/chdir: Cannot change current working directory to ", <id>)

  /**
   * Create directory
   *
   * @type String -> Int
   */
  mkdir(|mode) =
    where(
      ?pathname; prim("SSL_mkdir", pathname, mode) => 0
      <+ <conc-strings; perror; fail> ("SSL/mkdir: Cannot create directory ", <id>)
    )

  mkdir =
    mkdir(|[Read(), Write(), Execute()])

  /**
   * Remove empty directory
   *
   * @type String -> Int
   */
  rmdir =
    ?pathname; prim("SSL_rmdir", pathname) => 0
    <+ <conc-strings; perror; fail> ("SSL/rmdir: Cannot delete directory ", <id>)

/**
 * Primitive file operations
 */
strategies

  /**
   * Opening a file
   */
   
  // create a file and return a file descriptor
  creat =
    ?pathname; prim("SSL_creat", pathname)

  // open a file and return a file descriptor
  open =
    ?pathname; prim("SSL_open", pathname)

  /**
   * Closing a file
   *
   * Deallocates a file descriptor   
   */
  close =
    ?fd; prim("SSL_close", fd)
    
  /**
   * Duplicating a file descriptor
   */
  dup =
    ?fd; prim("SSL_dup", fd)

  dup2 =
    ?(fd1, fd2); prim("SSL_dup2", fd1, fd2)

  /**
   * checks the accessibility of the specified file wrt to the
   * specified permissions. Fails if the access is not allowed,
   * returns the path otherwise.
   *
   * @type (String, List(AccessPermission)) -> String
   *
   * @inc access
   */
  access =
    ?(path, permissions); prim("SSL_access", path, permissions)

signature
  constructors
    F_OK: AccessPermission
    R_OK: AccessPermission
    W_OK: AccessPermission
    X_OK: AccessPermission
    
/**
 * Connecting high and low level file operations
 */    
strategies 
 
  /**
   * The fdopen function associates a stream with the existing file 
   * descriptor, fd.
   * 
   * The mode of the stream ("r", "r+", "w", "w+",  "a", "a+") must be 
   * compatible with the mode of the file descriptor.  The file position 
   *
   * @type (FileDescr, String) -> Stream
   */
  fdopen = 
    ?(fd, mode); prim("SSL_fdopen", fd, mode); !Stream(<id>)

  /**
   * The function fileno examines the argument stream and returns its 
   * integer descriptor
   *
   * @type Stream -> FileDescr
   * @inc fileno
   */
  fileno = 
    ?Stream(stream); prim("SSL_fileno", stream)

  /**
   * Mode of a file
   * @type String -> FileMode
   */
  filemode =
    ?pathname; prim("SSL_filemode", pathname); ?(<id>, 0)
    <+ <conc-strings; perror; fail> ("SSL/filemode: Cannot get filemode from ", <id>)

  /**
   * @type File -> FileMode
   */
  isreg =
    ?mode; prim("SSL_S_ISREG", mode)
    
  /**
   * Succeeds when applied to a File which is a directory.
   *
   * Idiom: <file-exists ; filemode ; isdir> "/etc"
   *
   * @type File -> FileMode
   */
  isdir =
    ?mode; prim("SSL_S_ISDIR", mode)

  /**
   * @type File -> FileMode
   */
  ischr =
    ?mode; prim("SSL_S_ISCHR", mode)

  /**
   * @type File -> FileMode
   */
  isblk =
    ?mode; prim("SSL_S_ISBLK", mode)

  /**
   * @type File -> FileMode
   */
  isfifo =
    ?mode; prim("SSL_S_ISFIFO", mode)

  /**
   * @type File -> FileMode
   */
  islnk =
    ?mode; prim("SSL_S_ISLNK", mode) 

  /**
   * @type File -> FileMode
   */
  issock =
    ?mode; prim("SSL_S_ISSOCK", mode) 

/**
 * Pipes (and FIFOs)
 */
strategies
 
  /**
   * Pipe creates a pair Pipe(fd1, fd2) of file descriptors, pointing
   * to a pipe inode, and places them in the array pointed to by filedes.
   * fd1 is for reading, fd2 is for writing.
   *
   * @type _ -> Pipe
   */
  pipe =
    prim("SSL_pipe")
    
signature
  constructors
    Pipe       : Int * Int -> Pipe