Simplifying command-line usage of F*

[mtzguido]

There are two really annoying aspects of the F* command line that have to worked around:

1- To extract a module that we've already checked, we must still call F* on the source file. So if we have .cache/A.fst.checked we cannot do fstar.exe --codegen OCaml .cache/A.fst.checked (complains about an invalid extension) and must instead call F* on A.fst. The problem is that A.fst can be anywhere on the include path, and an F*-generated .depend file does not help us find it as the rules look like:

output/A.ml: .cache/A.fst.checked ....

.cache/A.fst.checked: foo/bar/A.fst ...

This means we have some awful makefile rules like:

$(OUTPUT_DIR)/%.ml:
       $(FSTAR) $(subst .checked,,$(notdir $<)) --codegen OCaml --extract_module $(subst .fst.checked,,$(notdir $<))

where the subst turns the checked file into the source file name (not path!) and relies on F* finding paths in the command line across its include path, which we also want to remove (fstar.exe Prims.fst should not just work anywhere, it should only work if Prims is in the current directory).

The first patch allows F* to take a checked file as argument, by performing a simple rewriting of it into its source file (which F* can indeed find in its configured include path). This turns the rule into:

$(OUTPUT_DIR)/%.ml:
       $(FSTAR) $< --codegen OCaml --extract_module $(subst .fst.checked,,$(notdir $<))

2- --codegen will by default extract all modules, so we need to explicitly restrict in most makefiles, as we have rules to generate only the target we want. This also entails some chopping of the names involved to obtain only the module name, as above. The second patch makes F*, by default, only extract the modules that were given in the command line, though this behavior can be overriden with any of the --extract toggles. The rule now becomes:

$(OUTPUT_DIR)/%.ml:
       $(FSTAR) $< --codegen OCaml

[mtzguido]

This worked on check-world here, and I think should be compatible with all existing uses. To restore the old behavior, if you were not passing any extraction filter, add --extract '*'. And if you were, just add that at the beginning.

Merging.