feat(engine/fstar): --interfaces: add option to extract only fsti

[W95Psp]

Fixes #397 and fixes #465

[franziskuskiefer]

So I can't get both anymore? That's a little weird.
Now I have to explicitly add all the modules I want to have interfaces for. Can't we make this a little nicer?

[W95Psp]

I re-read the explanations on the --interfaces flag, that was very unclear.

I now wrote that:

Modules for which Hax should extract interfaces (*.fsti files) in supplement to implementations (*.fst files). By default we extract no interface, only implementations. This flag expects a space-separated list of inclusion clauses. An inclusion clause is a Rust path prefixed with +, +! or -. - means implementation only, +! means interface only and + means implementation and interface. Rust path chunks can be either a concrete string, or a glob (just like bash globs, but with Rust paths).

Is that the behavior you would expect?

edit: Oh and I just edited the title, which was very misleading as well...

[franziskuskiefer]

Ok, lets get this in. It works.
We may want to improve on this later. Right now we have to add +! twice (for -i and --interfaces), to get only an interfaces, which is a little unintuitive. If the -i flag is only about what to include, a + should be enough.

[W95Psp]

You mean that if you want only the interface for Foo (without impl), then you don't want to extract dependencies of Foo's items, right?

So maybe we should have, for -i "modifies":

• + includes items with dependencies and with bodies;
• +! include items without dependencies but with bodies;
• +!! (or something else...) include items without dependencies or bodies.

But then, we need to have a representation for items without bodies, define what that means for types, for traits, etc. And also we need to define what it means in the various backend, to have empty bodies, which is not easy.