Cleaning up code & architecture

[xldenis]

I'm going to note some of my thinking for how I'd like to clean up the organization of Creusot.

• Replace translated_items with a graph structure.
  • The backbone of the translation is a single IndexMap, this has been fine until now, but isn't any more. Moving to a graph structure allows us to be less sensitive to the order of insertions and also perform selective printing of the translated items so that we could generate multiple outputs (ie: one per module / function).
• Replace the main id type with a wrapper around DefId. The DefId is rustc's internal id for everything, but it doesn't map well onto what Creusot needs. For example: rustc shares the same DefId for the closure type and closure function or a struct type and it's constructor. Disambiguating these in the identifier would help clean up various bits.
• Push CloneMap to the edges of the work flow. This should be relegated to a mere detail of the Why3 translation and not nearly such an essential object in the translation flow.
• Free translated_items of Why3 AST, I'd like the internal representation of translated_item to consist entirely of Creusot IR, and be entirely free of any why3 stuff (and thus CloneMap).

[xldenis]

I've begun work in this direction.

• Handling of builtins has been simplified and moved up to Term.
• Lowering of Term to Why3 no longer needs trait resolution
• I am working towards removing the 'incremental clones' feature of CloneMap. This should help simplify it.

[xldenis]

I still need to move closure_hack out of CloneMap and to a Term level thing.

[xldenis]

I've now moved lowering of logic functions to Why3 to the backend module. Remaining:

• External functions
• Lowering FMIR to why3
• Interfaces (an entirely why3 concept)

Then, the next step will be to restrict the interactions of the backend with rustc and Creusot by removing their dependency on TranslationCtx. I would like to instead give them a BackendCtx or equivalent which only forwards a very limited query api of TyCtxt and TranslationCtx. This will help surface any implicit dependencies and push things to be handled at the proper level.
Off the top of my head some of the allowed queries:

• type_of
• adt_def
• term
• pre_sig_of
• contract_of
• fmir_body
• item_type
• def_span: Maybe this should be banned?
• Ideally, not much else.

With this done, we can move backend into its own crate, finishing the split.

Simultaneously, translated_items can be ripped out of TranslationCtx, instead a separate loop can drive generation of why3 using backend and ctx.