vstd: map_err spec

[hayley-leblanc]

This PR adds a specification for the Result type's map_err method.

[hayley-leblanc]

The fmt check is failing with the following suggestion:

-pub fn map_err<T, E, F, O: FnOnce(E) -> F>(result: Result<T, E>, op: O) -> (mapped_result: Result<T, F>)
-    requires 
-        result.is_err() ==> op.requires((result.get_Err_0(),)), 
-    ensures 
+pub fn map_err<T, E, F, O: FnOnce(E) -> F>(result: Result<T, E>, op: O) -> (mapped_result: Result<
+    T,
+    F,
+>)
+    requires
+        result.is_err() ==> op.requires((result.get_Err_0(),)),
+    ensures

which I assume/hope is not actually the desired formatting?

[jaybosamiya]

Ah, errrrr, you seem to have hit a particularly unfortunate case for the verusfmt due to the original line being just barely above the width (i.e., number of columns) limit, and there being lots of tiny one/two character pieces in it to play with wrt splitting the line up, so the constraints are kinda just rough.

In particular, pub fn map_err<T, E, F, O: FnOnce(E) -> F>(result: Result<T, E>, op: O) -> (mapped_result: Result<T, F>) is 104 characters, while the column max limit is 100. In attempting to push it below the limit, verusfmt decides that the "best" way to do so is to break the final Result up. Probably a better position to break things would be at the -> but I don't see a trivial way to "convince" the constraint-solving system to prioritize a break there.

If you don't find it too terrible to shorten some identifiers, you could consider shortening the result -> res, giving:

pub fn map_err<T, E, F, O: FnOnce(E) -> F>(res: Result<T, E>, op: O) -> (mapped_res: Result<T,F>)

which goes below the width limit (is 97 characters), and thus isn't in the particularly awkward state.

A more brute-force approach is to just add a #[verusfmt::skip] to the function, but that is (imho) too drastic a measure for this, and completely negates internal formatting.

If you are curious about or want to play around with improving the formatter to convince it into breaking at the ->, the relevant place to look at would be here.

Sorry that you've hit this nasty edge case for the formatter, but hopefully the above explanation gives some workarounds or at least explanations as to why it is behaving non-ideally.

[tjhance]

I took a look but I don't really grok the way pretty makes its decisions. I tried putting -> (mapped_result: Result<T, F>) in a 'group' but it didn't seem to help. I would have expected pretty's heuristics to prioritize keeping a larger group on one line rather than splitting a small group across multiple lines. Kind of puzzled about how to approach this.

[parno]

I took a look but I don't really grok the way pretty makes its decisions.

Wadler's original paper suggests this as a heuristic for deciding which of two possible lines is "prettier":

If both lines are shorter than the available width, the longer one is better. If one line fits in the available width and the other does not, the one that fits is better. If both lines are longer than the available width, the shorter one is better.

The pretty crate follows Wadler's paper fairly closely, but deviates in a few places, so that's another possible source of surprise.

I tried putting -> (mapped_result: Result<T, F>) in a 'group' but it didn't seem to help.

That makes sense -- in general with pretty, you describe how the output can be laid out (possibly including newlines), and then if you want to allow the printer to consider putting it all on one line, you can "group" a set of documents, which adds a single-line version of those documents to the set to consider. As illustrated by Jay's example, the printer already has the option of grouping generic arguments; it just didn't choose that option in Hayley's version.

In Hayley's example, I think the printer has the option to break up the initial list of generic types (<T, E, F, O: FnOnce(E) -> F>), the arguments to map_err (result: Result<T, E>, op: O), or the result type. Breaking up the generic types would result in more lines than breaking the result type. I think breaking the arguments would create at least as many lines as breaking the result type, so either it creates more, so the choice is the result type, or it creates the same and some heuristic chose the result type.

Note that Rust doesn't allow a line break between the closing parenthesis of the arguments and the arrow (->), so the printer doesn't currently allow that.

[hayley-leblanc]

I have no issue shortening result to res in the variable names, as long as the difference in style from the rest of the file is okay with others. If not, I have the map_err spec living in my own project for now, so I'm not in a rush to get this merged; if y'all want to fix verusfmt first that's fine with me.

[parno]

I don't think there is an easy fix to verusfmt; I think it's mostly working as intended. I'd be inclined to go with Jay's suggestion of using res.

[tjhance]

It sounds like an easy fix would be to allow a newline before the ->, giving an easier way for the printer to lay out the return type on a single line. I think the fact that Rust's formatter doesn't do the same is a weak factor compared to the improvement in readability.

[tjhance]

Specifically I think we should allow newlines in all these places:

pub fn map_err<
  T,
  E,
  F,
  O: FnOnce(E) -> F
>(
  result: Result<T, E>,
  op: O
)
  -> (mapped_result: Result<
    T, 
    F
  >)
{
...
}

while making -> (mapped_result: Result<T, F>) into a group, and making everything from the pub to the { a group.