From 57f6881c6c8b66981a17ff1735d845e1c845fdea Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 19 Dec 2019 13:21:11 -0800
Subject: [PATCH] feat: restore state when catching `Exception.postpone`

cc @Kha
---
 src/Init/Lean/Elab/Term.lean    | 32 ++++++++++++++++++++++++++------
 src/Init/Lean/Elab/TermApp.lean |  2 +-
 tests/lean/run/frontend1.lean   |  2 ++
 3 files changed, 29 insertions(+), 7 deletions(-)

diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 863739a4eb..762cccafea 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -425,12 +425,12 @@ pure mvar
   All unlogged trace messages produced by the elaboration method are logged using
   the position information at `stx`. If the elaboration method throws an `Exception.error`,
   the error is logged and a synthetic sorry expression is returned.
-  If the elaboration throws `Exception.postpone` and `resuming == false`,
+  If the elaboration throws `Exception.postpone` and `catchExPostpone == true`,
   a new synthetic metavariable of kind `SyntheticMVarKind.postponed` is created, registered,
   and returned.
-  We use `resuming == true` to prevent the creation of another synthetic metavariable
-  when resuming the elaboration. -/
-def elabTerm (stx : Syntax) (expectedType? : Option Expr) (resuming := false) : TermElabM Expr :=
+  The option `catchExPostpone == false` is used to implement `resumeElabTerm`
+  to prevent the creation of another synthetic metavariable when resuming the elaboration. -/
+def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) : TermElabM Expr :=
 withFreshMacroScope $ withNode stx $ fun node => do
   trace! `Elab.step (toString stx);
   s ← get;
@@ -442,12 +442,32 @@ withFreshMacroScope $ withNode stx $ fun node => do
       (tracingAt stx (elab node expectedType?))
       (fun ex => match ex with
         | Exception.error ex => exceptionToSorry stx ex expectedType?
-        | Exception.postpone => if resuming then throw ex else postponeElabTerm stx expectedType?)
+        | Exception.postpone =>
+          if catchExPostpone then do
+            /- If `elab` threw `Exception.postpone`, we reset any state modifications.
+               For example, we want to make sure pending synthetic metavariables created by `elab` before
+               it threw `Exception.postpone` are discarded.
+               Note that we are also discarding the trace messages created by `elab`. If we decide to save
+               them, we can do by modifying `tracingAt`.
+
+               For example, consider the expression.
+               `((f.x a1).x a2).x a3`
+               Now, suppose the elaboration of `f.x a1` produces an `Exception.postpone`.
+               Then, a new metavariable `?m` is created. Then, `?m.x a2` also throws `Exception.postpone`
+               because the type of `?m` is not yet known. Then another, metavariable `?n` is created, and
+               finally `?n.x a3` also throws `Exception.postpone`. If we did not restore the state, we would
+               keep "dead" metavariables `?m` and `?n` on the pending synthetic metavariable list. This is
+               wasteful because when we resume the elaboration of `((f.x a1).x a2).x a3`, we start it from scratch
+               and new metavariables are created for the nested functions. -/
+            set s;
+            postponeElabTerm stx expectedType?
+          else
+            throw ex)
   | none      => throwError stx ("elaboration function for '" ++ toString k ++ "' has not been implemented")
 
 /-- Auxiliary function used to implement `synthesizeSyntheticMVars`. -/
 private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr :=
-elabTerm stx expectedType? true
+elabTerm stx expectedType? false
 
 /--
   Make sure `e` is a type by inferring its type and making sure it is a `Expr.sort`
diff --git a/src/Init/Lean/Elab/TermApp.lean b/src/Init/Lean/Elab/TermApp.lean
index 51fd8a17a3..01d061abaa 100644
--- a/src/Init/Lean/Elab/TermApp.lean
+++ b/src/Init/Lean/Elab/TermApp.lean
@@ -318,7 +318,7 @@ private partial def elabAppFn (ref : Syntax) : Syntax → List LVal → Array Na
         acc
     | _ => unreachable!
   else do
-    f ← withoutPostponing $ elabTerm f none;
+    f ← elabTerm f none;
     s ← observing $ elabAppLVals ref f lvals namedArgs args expectedType? explicit;
     pure $ acc.push s
 
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index aa7f9bd946..bd0f021ebf 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -152,3 +152,5 @@ f a
 #eval run "#check fun x => foo x x.w s4"
 #eval run "#check bla (fun x => x.w) s4"
 #eval run "#check #[1, 2, 3].foldl (fun r a => r.push a) #[]"
+#eval run "#check #[1, 2, 3].foldl (fun r a => (r.push a).push a) #[]"
+#eval run "#check #[1, 2, 3].foldl (fun r a => ((r.push a).push a).push a) #[]"