Add support for directories to the filesystem FFI

[xrchz]

This issue is for adding the ability to read the contents of directories using the CakeML basis. It is probably a requirement for #614.

[hferee]

Summary of what I think is required for this:

• being able to tell regular files from directories, i.e in inode_tbl, replace inode with a stat record containing:
  • the inode number
  • a mode, encoding flags like S_IFDIR and S_IFREG
  • optionally, but ideally, all of C's stat structure, like file permissions
• restrict most existing file operations to files with S_IFREG
• add FFI and basis library functions for openDir, closeDir, readDir
  • the DIR datatype is implemented as a file descriptor
  • openDir and closeDir are similar to openOut and closeOut but restricted to files with S_IFDIR:
• ideally, but optionally, implement getDir and chDir, which modify a state (separate from the filesystem) representing the current directory name.

The last point introduces a major difficulty, avoided until now: model relative paths, and more generally, the directory structure. Everything currently assumes that a given file will always be addressed using the same filename (e.g. after creating file foo, $pwd/foo and foo do not represent the same inode). I suggest changing the fs.files field from (mlstring#mlstring) list to: a tree of such (mlstring#mlstring) list representing the regular files immediately in the directory ; its subdirectories being its children. This requires to define a tree lookup and update function (which understands _/_, .., .), as well as a path equivalence function.

[xrchz]

Great fleshing out of this issue! Should we perhaps be trying to tap into any existing formal file system models? I think there's been a lot of work on that by eg Tom Ridge, Philippa Gardner, ...

[hferee]

Yes (ECOOP18 seems good for this), especially as they model it with separation logic, when our current model is a big unseparable block. I don't see why inode_tbl and files could not be represented in a finer way (i.e. per file/inode), but afaik infds can't, as the knowledge of all the currently opened file descriptors is required to allocate a new one. I don't have time to work on this in the following weeks, but I will give it a thought later or provide help is anyone wants to jump in.