Use a file-based I/O interface to the compiler

[xrchz]

Make the top-level interface to the compiler accept the names of input file(s) on the command line, including a way to specify stdin, and an optional output file instead of stdout. (See comment in #319.) Probably depends on #248 and #354.

[xrchz]

Amongst other things, the .file directive in our .S file template should reflect the actual name of the output file.

[oskarabrahamsson]

The most annoying issue is that command-line arguments are dealt with in two places:

• In the main function in compiler64ProgScript.sml, and
• In the pure compiler function in compilerScript.sml.

I suggest moving all options parsing to the main function in compiler64ProgScript.sml, remove the command-line and file-system model arguments from compile_{32,64} and pass the compiler configuration records created from options parsing instead.

Alternatively, one can:

• Do it the other way around. This seems like more of a hassle, since the main function needs to decide whether to compile at all, or just print a help message, among other things.
• Keep it the way it is, and keep writing command-line options parsers in two places. I suspect this is one reason why the compiler binary so seldomly receives any updates.

Finally, I don't think #248 is required anymore: it's probably easier to extend the existing ad-hoc options parsing code.

[tanyongkiam]

I think I would prefer the "do it the other way around" option of @oskarabrahamsson

Here is what I suggest. I think we should put as much of the pure parsing code into one place as possible.

Inside compilerScript: define a function parse_options: mlstring list -> run_compile_config

where the intended semantics is that it parses the input command line strings cl and
returns the desired behavior of the compiler based on the flags.

These behaviors should be modeled using a new datatype run_compile_config, which has one constructor for each different major behaviors we want from the compiler.

Inside compiler64Prog: one writes (in CakeML) a function that:

1. calls CommandLine.arguments()
2. passes it to parse_options
3. matches on the result and runs the appropriate behavior (many of which are not pure, and thus need to be placed here).

[mn200]

A general library for parsing command-line options (akin to the SML/NJ getopt library that HOL uses in a variety of places) might be a nice side-effect of this.

[tanyongkiam]

A general library for parsing command-line options (akin to the SML/NJ getopt library that HOL uses in a variety of places) might be a nice side-effect of this.

From what I understand, this was tried, but got too complicated in the end:

#248

Perhaps one might want to go for something easier (and that also supports what HOL needs)