From 7cdf917c9708aced043cd5fb9f3b89f53adb987a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 15 Aug 2020 15:51:00 -0700
Subject: [PATCH] fix: compiler `do a; b` as `a >>= fun _ => b`
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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 | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index b05ccc0e77..a44eff011a 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/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;