From f1ed13efffa7563ac12bd9352faa45e80a1c84c7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Jan 2021 15:33:48 -0800 Subject: [PATCH] feat: improve `elabMatchAux` We now (try to) postpone `match ... with` elaboration when pattern variables and patterns still contain metavariables before invoking `mkMatcher`. This improvement makes sure we can elaborate an example submitted by Daniel Selsam. Remark: this update may create performance problems since we backtrack `elabMatchTypeAndDiscrs` and `elabMatchAltView`. We hope this is not a problem in practice since we use the "quick-check" `waitExpectedTypeAndDiscrs`. Recall that we could compile Lean without this commit. So, it suggests cases where we need to postpone after `elabMatchAltView` are rare. --- src/Lean/Elab/Match.lean | 92 ++++++++++++++++---------- src/Lean/Elab/Term.lean | 11 ++- tests/lean/forErrors.lean.expected.out | 2 - tests/lean/run/Daniel1.lean | 17 +++++ 4 files changed, 83 insertions(+), 39 deletions(-) create mode 100644 tests/lean/run/Daniel1.lean diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index ae8f0b8fd8..af6673f5cc 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -708,44 +708,64 @@ def reportMatcherResultErrors (altLHSS : List AltLHS) (result : MatcherResult) : private def elabMatchAux (discrStxs : Array Syntax) (altViews : Array MatchAltView) (matchOptType : Syntax) (expectedType : Expr) : TermElabM Expr := do - let (discrs, matchType, altViews) ← elabMatchTypeAndDiscrs discrStxs matchOptType altViews expectedType - let matchAlts ← liftMacroM $ expandMacrosInPatterns altViews - trace[Elab.match]! "matchType: {matchType}" - let alts ← matchAlts.mapM $ fun alt => elabMatchAltView alt matchType - /- - We should not use `synthesizeSyntheticMVarsNoPostponing` here. Otherwise, we will not be - able to elaborate examples such as: - ``` - def f (x : Nat) : Option Nat := none + let (discrs, matchType, altLHSS, rhss) ← commitIfDidNotPostpone do + let (discrs, matchType, altViews) ← elabMatchTypeAndDiscrs discrStxs matchOptType altViews expectedType + let matchAlts ← liftMacroM $ expandMacrosInPatterns altViews + trace[Elab.match]! "matchType: {matchType}" + let alts ← matchAlts.mapM $ fun alt => elabMatchAltView alt matchType + /- + We should not use `synthesizeSyntheticMVarsNoPostponing` here. Otherwise, we will not be + able to elaborate examples such as: + ``` + def f (x : Nat) : Option Nat := none - def g (xs : List (Nat × Nat)) : IO Unit := - xs.forM fun x => - match f x.fst with - | _ => pure () - ``` - If `synthesizeSyntheticMVarsNoPostponing`, the example above fails at `x.fst` because - the type of `x` is only available after we proces the last argument of `List.forM`. + def g (xs : List (Nat × Nat)) : IO Unit := + xs.forM fun x => + match f x.fst with + | _ => pure () + ``` + If `synthesizeSyntheticMVarsNoPostponing`, the example above fails at `x.fst` because + the type of `x` is only available after we proces the last argument of `List.forM`. - We apply pending default types to make sure we can process examples such as - ``` - let (a, b) := (0, 0) - ``` - -/ - synthesizeSyntheticMVarsUsingDefault - let rhss := alts.map Prod.snd - let matchType ← instantiateMVars matchType - let altLHSS ← alts.toList.mapM fun alt => do - let altLHS ← Match.instantiateAltLHSMVars alt.1 - withRef altLHS.ref do - for d in altLHS.fvarDecls do - if d.hasExprMVar then - withExistingLocalDecls altLHS.fvarDecls do - throwMVarError m!"invalid match-expression, type of pattern variable '{d.toExpr}' contains metavariables{indentExpr d.type}" - for p in altLHS.patterns do - if p.hasExprMVar then - withExistingLocalDecls altLHS.fvarDecls do - throwMVarError m!"invalid match-expression, pattern contains metavariables{indentExpr (← p.toExpr)}" - pure altLHS + We apply pending default types to make sure we can process examples such as + ``` + let (a, b) := (0, 0) + ``` + -/ + synthesizeSyntheticMVarsUsingDefault + let rhss := alts.map Prod.snd + let matchType ← instantiateMVars matchType + let altLHSS ← alts.toList.mapM fun alt => do + let altLHS ← Match.instantiateAltLHSMVars alt.1 + /- Remark: we try to postpone before throwing an error. + The combinator `commitIfDidNotPostpone` ensures we backtrack any updates that have been performed. + The quick-check `waitExpectedTypeAndDiscrs` minimizes the number of scenarios where we have to postpone here. + Here is an example that passes the `waitExpectedTypeAndDiscrs` test, but postpones here. + ``` + def bad (ps : Array (Nat × Nat)) : Array (Nat × Nat) := + (ps.filter fun (p : Prod _ _) => + match p with + | (x, y) => x == 0) + ++ + ps + ``` + When we try to elaborate `fun (p : Prod _ _) => ...` for the first time, we haven't propagated the type of `ps` yet + because `Array.filter` has type `{α : Type u_1} → (α → Bool) → (as : Array α) → optParam Nat 0 → optParam Nat (Array.size as) → Array α` + However, the partial type annotation `(p : Prod _ _)` makes sure we succeed at the quick-check `waitExpectedTypeAndDiscrs`. + -/ + withRef altLHS.ref do + for d in altLHS.fvarDecls do + if d.hasExprMVar then + withExistingLocalDecls altLHS.fvarDecls do + tryPostpone + throwMVarError m!"invalid match-expression, type of pattern variable '{d.toExpr}' contains metavariables{indentExpr d.type}" + for p in altLHS.patterns do + if p.hasExprMVar then + withExistingLocalDecls altLHS.fvarDecls do + tryPostpone + throwMVarError m!"invalid match-expression, pattern contains metavariables{indentExpr (← p.toExpr)}" + pure altLHS + return (discrs, matchType, altLHSS, rhss) let numDiscrs := discrs.size let matcherName ← mkAuxName `match let matcherResult ← mkMatcher matcherName matchType numDiscrs altLHSS diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index e702ebb70b..c84d5c2ca0 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -206,11 +206,20 @@ def getMessageLog : TermElabM MessageLog := /-- Apply the result/exception and state captured with `observing`. We use this method to implement overloaded notation and symbols. -/ -def applyResult (result : TermElabResult α) : TermElabM α := +@[inline] def applyResult (result : TermElabResult α) : TermElabM α := match result with | EStateM.Result.ok a r => do r.restore; pure a | EStateM.Result.error ex r => do r.restore; throw ex +/-- + Execute `x`, but keep state modifications only if `x` did not postpone. + This method is useful to implement elaboration functions that cannot decide whether + they need to postpone or not without updating the state. -/ +def commitIfDidNotPostpone (x : TermElabM α) : TermElabM α := do + -- We just reuse the implementation of `observing` and `applyResult`. + let r ← observing x + applyResult r + @[inline] protected def liftMetaM {α} (x : MetaM α) : TermElabM α := liftM x diff --git a/tests/lean/forErrors.lean.expected.out b/tests/lean/forErrors.lean.expected.out index 898ea84d83..f115441e1f 100644 --- a/tests/lean/forErrors.lean.expected.out +++ b/tests/lean/forErrors.lean.expected.out @@ -1,4 +1,2 @@ forErrors.lean:3:29-3:30: error: failed to synthesize instance ToStream α ?m -forErrors.lean:5:15-5:39: error: failed to synthesize instance - ToString α diff --git a/tests/lean/run/Daniel1.lean b/tests/lean/run/Daniel1.lean new file mode 100644 index 0000000000..fdd267289f --- /dev/null +++ b/tests/lean/run/Daniel1.lean @@ -0,0 +1,17 @@ +def small (ps : Array (Nat × Nat)) : Array (Nat × Nat) := + (ps.filter fun (p : Prod _ _) => + match p with + | (x, y) => x == 0) + ++ + ps + +#eval small #[(1, 2), (0, 3), (2, 4)] + +variables {α β : Type} [Inhabited α] [Inhabited β] + +def P (xys : Array (α × β)) (f : α → β) : Prop := True + +example (xys : Array (α × β)) + (pred? : α → Bool) + (H : Subtype $ P (xys.filter fun (x, _) => pred? x)) + : Unit := ()