exporter: refactor Clauses

[W95Psp]

While defining Clauses I was a bit aggressive towards binders, and entirely got rid of them. This is a bad design, as pointed out by @Nadrieril in our conversation in #655.

Currently, a Clause is a ClauseKind + an identifier.

We should instead have a Clause being a struct with first a Binder<ClauseKind> and then a ClauseId, which accounts for binders.

[Nadrieril]

This may cause issues because we don't have access to the binder when recursively converting PredicateKind. The thing I had in mind was:

enum PredicateKind {
  Clause(UnboundClause),
  ...
}

with an API to get from Predicate to Clause by mapping the binder over like rustc does. Maybe there's a simpler option.

[W95Psp]

Yes, that's a good point.

To recap a bit, the issue is that if we go with a Clause object that contains a Binder<ClauseKind> and a clause identifier, then no clause identifier will be accessible from a Predicate.

If we confirm we should always work with Binder<ClauseKind>s and Binder<PredicateKind>s and never work with ClauseKinds and PredicateKinds, then I think we should really have the identifier above the Binder<...>.

Currently Predicate is defined as Binder<PredicateKind>, and we are discussing about adding Clause defined as Binder<PredicateKind>.

What about defining a Predicate (resp. Clause) as structs with both a field kind of type PredicateKind (resp. ClauseKind) and a field clause_id of type ClauseId (using a newtype as you suggest in #626)? (we could also define only one struct for those two with a generic, but that would be more confusing than anything else)

Edit: and ClauseId might be better named PredicateId

[W95Psp]

Regarding our conversation in your PR @Nadrieril, I'm not crazy: there was a renaming from Clause to ClauseKind in Rustc... Clauses used not to have binders at all!

In commit fca56a8, the type Clause has been renamed as ClauseKind, then commit 21226e makes Clause a Binder<ClauseKind>, essentially (with an indirection via PredicateKind and an invariant where the
predicate kind has to be a ty::PredicateKind::Clause(ClauseKind)).