Improvements over let operators

[W95Psp]

Hi,

Following the conversation in #1868, this PR improves the implementations of let operators in the following ways:

• simplify the parser by letting let<OP> and and<OP> be treated as operator nodes Op instead of simple names;
• better printing;
• more documentation;
• support "sequence operators", i.e. x <- y ;* z and x ;* z.

There are two problems still:

• ~I added the support for the existing various characters one can use in regular operators for let operators, but this causes ;// to be parsed as the sequence operator (;//) instead of a sequence then a comment. It is not very user friendly in my opinion: should I just drop support for slashes in let operators (which leads to an inconsistency with what's accepted for regular operators --+// is a legal operator), or should I simply make the lexer reject the sequence operator ;//?~ commit 4fea177 forbids double slashes in let operators
• Type ascription on let bindings is not accepted yet (let* x: foo = ... is rejected), which is not what one might expect. This should be easily fixed though, I have to look into that.

[W95Psp]

As we discussed last Friday with @nikswamy and @aseemr, I made the following changes: (note below * denotes any sequence of operator chars)

• the monadic sequence x ;* y is now desugared into a LetOperator node in the surface AST (i.e. let* _ = x in y) instead of a enhanced Bind node;
• I reverted the enhancements of Bind (which consisted in accepting an optional operator);
• I removed support for the syntax x <- y ;* z;
• this PR deprecates the lightweight do notation (that is x ;; y or x <- y ; z), raising a warning ;
• type ascription is now supported (that is let C x y: sometype = ... and ...: othertype = ... in ...), details are given in issue #2678.

What do you think @nikswamy and @aseemr? Could we merge this PR?

[nikswamy]

Thanks @W95Psp! This looks great and I tried using it a bit and had no problems.

One thing that was not clear to me from the comments here is whether or not this is actually solving the type ascription problem mentioned in issue #2678 . I don't believe that it is, which is fine, since addressing 2678 is not the purpose of the PR.

Just for the record, here are some examples of the behavior I observed:

let test5 (x:option (ℤ & ℤ)) : option ℤ =
  let? ((x :ℤ), (y:bool)) = x in //fails correctly, noting that the annotation on y is incompatible
  Some ( x + 0 )

type foo t = | Foo: t → foo t

let test6 (x:option (foo ℤ)) : option ℤ =
  let? (Foo (x : bool)) = x in //succeds while ignoring the annotation on x
  Some ( x + 0 )

let test7 x =
  let? Foo x : foo bool = x in //fails respecting the annotation on the whole pattern
  Some (x + 1)

The second thing: I debated whether to deprecate the old syntax, wondering if it would cause surprises to others. But, after some discussions, I decided to go ahead with it, as the new syntax is clearly superior. Besides, and for the record, if you can't migrate to the new syntax right away, you can always suppress warning 350 for the time being.

So, I'm merging this as is. Thanks again!

[W95Psp]

Thanks for merging :) Yes, this PR doesn't solve issue #2678 at all; I mentioned it only because I had to rewrite patterns generated by the desugaring of let operators specifically to avoid #2678. Fixing issue #2678 would allow for a simplification of the desugaring of let operators.