Export discriminant values in AdtDef

[Nadrieril]

The discriminant is the runtime integer value used to identify a given enum variant. It's the value on which we do a SwitchInt. This PR makes hax export them.

I would have prefered a discriminant field in VariantDef but that would have been tricky to fit into the SInto scheme.

[W95Psp]

How does this compare to the field discr of type VariantDiscr of the VariantDef struct?
I guess VariantDiscr is too high level as the discriminant is not normalized yet?

Anyway, the SInto mechanism should be a convenience, not a barrier, so I'm in favor of breaking the SInto scheme here: let's kill VariantDef SInto instance, and provide a function that does this translation instead, function that can then take as an extra parameter a discriminant value.

Shall we merge VariantDiscr and DiscriminantValue? E.g. we could rename VariantDiscr as DiscriminantDefinition, and add a definition field in DiscriminantValue

[Nadrieril]

How does this compare to the field discr of type VariantDiscr of the VariantDef struct? I guess VariantDiscr is too high level as the discriminant is not normalized yet?

Yeah, it's a recipe for how to compute the DiscriminantValue but we don't want to compute it ourselves.

Anyway, the SInto mechanism should be a convenience, not a barrier, so I'm in favor of breaking the SInto scheme here: let's kill VariantDef SInto instance, and provide a function that does this translation instead, function that can then take as an extra parameter a discriminant value.

👍

Shall we merge VariantDiscr and DiscriminantValue? E.g. we could rename VariantDiscr as DiscriminantDefinition, and add a definition field in DiscriminantValue

I guess we could do that; I don't have a use for VariantDiscr atm.

[W95Psp]

Nice, let's do so then. Do you want to do it?

In hax engine we rely on VariantDiscr: if a user defines an explicit discriminant we extract the discriminant expression (this was added in #571)

[Nadrieril]

If you feel like doing it, please do. Otherwise I'll do it myself in a day or two when I'm finished with other things

[Nadrieril]

Marking as draft while I do this

[Nadrieril]

This PR is ready, and so is the corresponding charon change: AeneasVerif/charon#255

[W95Psp]

LGTM, thanks!