From 178ab8ef2e7aba9e18c9fcfeda12e763d62983af Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 11 Dec 2023 02:07:30 -0800
Subject: [PATCH] fix: Option.getD eagerly evaluates dflt (#3043)

Reported [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/Panics.20in.20Std.2EHashMap.2Efind!/near/406872395).
The `dflt` argument of `Option.getD` is not evaluated lazily, as the
documentation says, because even after `macro_inline` the expression
```lean
match opt, dflt with
| some x, _ => x
| none, e => e
```
still has the semantics of evaluating `dflt` when `opt` is `some x`.
---
 src/Init/Prelude.lean                            |  7 ++++---
 tests/lean/optionGetD.lean                       | 12 ++++++++++++
 tests/lean/optionGetD.lean.expected.out          |  1 +
 tests/lean/smartUnfoldingMatch.lean.expected.out |  6 +++---
 4 files changed, 20 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/optionGetD.lean
 create mode 100644 tests/lean/optionGetD.lean.expected.out

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 3d26bc852ef4..b0bebd46c294 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2213,9 +2213,10 @@ returns `a` if `opt = some a` and `dflt` otherwise.
 This function is `@[macro_inline]`, so `dflt` will not be evaluated unless
 `opt` turns out to be `none`.
 -/
-@[macro_inline] def Option.getD : Option α → α → α
-  | some x, _ => x
-  | none,   e => e
+@[macro_inline] def Option.getD (opt : Option α) (dflt : α) : α :=
+  match opt with
+  | some x => x
+  | none => dflt
 
 /--
 Map a function over an `Option` by applying the function to the contained
diff --git a/tests/lean/optionGetD.lean b/tests/lean/optionGetD.lean
new file mode 100644
index 000000000000..e32e15a15aa6
--- /dev/null
+++ b/tests/lean/optionGetD.lean
@@ -0,0 +1,12 @@
+import Lean.Data.HashMap
+
+def test (m : Lean.HashMap Nat Nat) : IO (Nat × Nat) := do
+  let start := 1
+  let mut i := start
+  let mut count := 0
+  while i != 0 do
+    i := (m.find? i).getD (panic! "key is not in the map")
+    count := count + 1
+  return (i, count)
+
+#eval test (.ofList [(1,3),(3,2),(2,0)])
diff --git a/tests/lean/optionGetD.lean.expected.out b/tests/lean/optionGetD.lean.expected.out
new file mode 100644
index 000000000000..3947600ce84b
--- /dev/null
+++ b/tests/lean/optionGetD.lean.expected.out
@@ -0,0 +1 @@
+(0, 3)
diff --git a/tests/lean/smartUnfoldingMatch.lean.expected.out b/tests/lean/smartUnfoldingMatch.lean.expected.out
index 3d995b176e3e..2532b3c9eb77 100644
--- a/tests/lean/smartUnfoldingMatch.lean.expected.out
+++ b/tests/lean/smartUnfoldingMatch.lean.expected.out
@@ -1,4 +1,4 @@
 42
-[Meta.debug] r: match x, 0 with
-    | some x, x_1 => x
-    | none, e => e
+[Meta.debug] r: match x with
+    | some x => x
+    | none => 0