Have patterns as returns instead of coma separated variables

[pascutto]

Gospel only allows comma-separated variable names as return values at the moment. Allowing patterns would be closer to OCaml and more convenient and generic (e.g. when destructing records).

[n-osborne]

For now, return values can be labelled as ghost (see: https://github.com/ocaml-gospel/gospel/blob/main/src/uast.mli#L88). But patterns can't be labelled as ghost.

In order to keep the possibility of ghost returned values, my first naïve first guess would be to have a pair composed of a list for the ghost return values and a pattern for the actual return value. Keeping them cleanly separated and being able to typecheck the pattern against the type declared in the OCaml signature.

I don't know about the concrete syntax though :-)

[pascutto]

Perhaps you also want to have a pattern to describe the ghost values. The current syntax does not work very well with this as [x:t] can be both a ghost variable and a non-ghost singleton list, so I'm not sure what syntax to use either.

[n-osborne]

128 suggest to use [@ghost x: t, y: t']

Also, as there is only one OCaml return value, we could have a comma separated list of patterns, the last one being the actual return value and the other, if any, the ghost values. The downside being that it may be too much implicit. Also, a function that would return unit and a ghost value would have to explicitly mention the unit in its header.

[pascutto]

A comma-separated list of patterns is ambiguous since patterns can be comma-separated identifiers.

It looks like [@ghost x: t, y: t'] could work, I forgot about this suggestion. It's a bit more verbose but ghost variables are not that frequent. Does someone else have a suggestion or should we go with that?