Documentation: Edits to document :- statements

[davidcok]

No description provided.

[acioc]

Added a few formatting notes below. I generally try to follow semantic line breaks: https://sembr.org/ since this makes it much easier to handle future diffs.

[RustanLeino]

There are many things to say about the :- statement, including the many variations of expressions, functions, methods, value-carrying or not, etc. I like that many fine points (like when things are evaluated, the use of expect, and some practical consequences of using this feature) are explained only at the end.

I find the syntactic desugaring of the :- a compelling explanation for what :- does. This is not part of the explanations above. Here's a possible sequence of steps for explaining the feature. These are different from above, so ignore if you'd like or use as you see fit.

• Say :- is related to :=, but also handles failures
• Define failure-compatible type
• Explain the simple case x :- E;, where x is a local variable and E is an expression of a value-carrying failure-compatible type. Show the desugaring for this statement. If it helps, assume IsFailure, PropagateFailure, and Extract are all functions.
• Explain the multi-RHS case x, y, z :- E, F, G;. Show the desugaring for this statement.
• Explain the variable where the type of E is not value-carrying. Say that the desugaring is the same, except that the call to Extract() is omitted.
• Explain x, y, z :- M();, where M is a method call whose first parameter is a value-carrying failure-compatible type. Show the desugaring for this statement.
• Mention the variation of this statement where the failure-compatible type is not value-carrying.
• Mention that PropagateFailure and Extract need not be functions--they can be method.
• Mention the :- can be followed by expect (as you already do in a separate section above).
• Mention the fine points (evaluation order, etc.).