Note from a brief discussion with @trefis. In a future PR it might be worth adding a version of Pattern_head.destruct that returned a list of "destructed" patterns, allowing it to work on or-patterns. It would allow for simpler code in places like compat and simplify_head_pat.

I have thought about extending the notion of head to or-patterns (which may have several heads). One property that we lose as soon as we leave the fragment of simple patterns is the equivalence between pattern_desc and head * pattern list. Indeed, this equivalence does not take into account the binding structure "above" the head of the pattern, as present in the cases Tpat_var and Tpat_alias.

So I think that rather than extending destruct, we should have a different API for this case that emphasize that we are talking about the shape of the matched values, as a lossy projection from the pattern: heads : pattern -> head list.

@Octachron I updated as you suggested. I'll clean up the history and merge later today.

@gasche:

So I think that rather than extending destruct, we should have a different API for this case

I believe that is what @lpw25 was suggesting.

Ah, I realize I forgot to answer:

In particular, the code often uses names of the form d... for pattern head variables. Could we use more mnemonic names? Like h.. as a shorthand for head (which is also used) for instance?

d... is often used to indicate we're working with a "discriminating" pattern (which I guess we should call "discriminating head") as produced by discr_pat, not just any head.
I will have another look at the code to see if it's actually used properly.

I pushed some minor renaming along these lines, but things were mostly OK IMO.

The renamings look nice (in particular in simple_match_args), and make it much more clearer that d is a shorthand for discriminating, thanks!

I rebased and cleaned up the history.
I'll merge once the CI is green.