F*: extract implementations without associated types as val instance ...

[W95Psp]

When extracting interfaces in F*, the impl blocks are extracted entirely with all the associated items and their body.
This causes multiple issues:

• the dependency graph (both in the engine and in F*) for an interface is big, since all inner dependencies used by the bodies of trait associated items are included
• we often extract interfaces for code we don't want or can't extract, so including full items of impls in the interfaces is counter-productive here

Solution:

1. Systematically hoist all the associated items and bundle them separately, so that we can decide which associated item shall be exposed or not in the interface
2. Use a val whenever the impl has no associated type or constants (we never want to extract code for associated functions in interfaces, that's the whole purpose of interfaces)
3. Use a F* tactic to generate val for everything not mentioned when defining a impl

Action plan:

• We will implement a stronger version of (2), whenever an impl has no associated type, but only consts and fns, then we use an opaque val. That might cause issues with constants, let's see in practice.
• In the impl extraction bit of the F* backend, want a boolean that says whether we're extracting opaquely or not: in fsti mode, we should output either a let or a val, in fst mode we should output either nothing or a let.
• We need to patch import_thir: in c_item_unwrapped, we need to use c_body instead of c_expr when importing an impl that has no associated types