fix: compiler do a; b as a >>= fun _ => b

Consider the following example
```lean
def div!: Nat → Nat → Nat
| x, 0 => panic! "division by zero"
| x, y => x/y

def weird (x : Nat) : MetaM Nat :=
unless (x > 0) (throwOther "x == 0") *>
let y := div! 10 x;
pure y
```
If we execute `weird 0`, it produces a "division by zero" panic
message.
This is a simple version of a much bigger function in the new
frontend.
This is not due to a bug in the compiler.
It produces the panic message because of the `do`-encoding
refactoring. Recall that, a few months ago,
we started to compile `do a; b` as `a *> b` (i.e., `seqRight a b`).
Thus, the example above is
`seqRight action1 (let y := div! 10 x; pure y)`
where `action1` is the `unless ...`.
In A-normal form, this is equivalent to

```lean
let y:= div! 10 x;
let action2 := pure y;
seqRight action1 action2
```
Thus, we execute `div! 10 x` before we even execute the `seqRight`.
This is counterintuitive and demonstrates once again how impure
features such as `panic!` are dangerous.

This commit reverts the `do`-encoding refactoring, and encodes
`do a; b` as `a >>= fun _ b` as we did in Lean3.

cc @Kha

src/frontends/lean/builtin_exprs.cpp

@@ -347,7 +347,9 @@ static expr parse_do(parser & p, bool has_braces) {
                                    pos);
             }
         } else {
-            r = p.rec_save_pos(mk_app(p.save_pos(mk_const({"HasSeqRight", "seqRight"}), ps[i]), es[i], r), ps[i]);
+            expr action2 = p.save_pos(mk_lambda("_", mk_expr_placeholder(), r), ps[i]);
+            r = p.rec_save_pos(mk_app(p.save_pos(mk_bind_fn(p), ps[i]), es[i], action2), ps[i]);
+            // r = p.rec_save_pos(mk_app(p.save_pos(mk_const({"HasSeqRight", "seqRight"}), ps[i]), es[i], r), ps[i]);
         }
     }
     return r;