From 3ccc9ca7ac86504e100a39066e0c83443a57d047 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Mon, 2 Jun 2025 09:14:56 -0700
Subject: [PATCH] fix: remove incorrect strictOr/strictAnd optimizations
 (#8594)

This PR removes incorrect optimizations for strictOr/strictAnd from the
old compiler, along with deleting an incorrect test. In order to do
these optimizations correctly, nontermination analysis is required.
Arguably, the correct way to express these optimizations is by exposing
the implementation of strictOr/strictAnd to a nontermination-aware phase
of the compiler, and then having them follow from more general
transformations.
---
 src/Lean/Compiler/ConstFolding.lean | 30 +----------------------------
 tests/compiler/strictOrSimp.lean    | 11 -----------
 2 files changed, 1 insertion(+), 40 deletions(-)
 delete mode 100644 tests/compiler/strictOrSimp.lean

diff --git a/src/Lean/Compiler/ConstFolding.lean b/src/Lean/Compiler/ConstFolding.lean
index 3206481113..388ae6f195 100644
--- a/src/Lean/Compiler/ConstFolding.lean
+++ b/src/Lean/Compiler/ConstFolding.lean
@@ -150,36 +150,8 @@ def natFoldFns : List (Name × BinFoldFn) :=
    (``Nat.ble,   foldNatBle)
 ]
 
-def getBoolLit : Expr → Option Bool
-  | Expr.const ``Bool.true _  => some true
-  | Expr.const ``Bool.false _ => some false
-  | _                         => none
-
-def foldStrictAnd (_ : Bool) (a₁ a₂ : Expr) : Option Expr :=
-  let v₁ := getBoolLit a₁
-  let v₂ := getBoolLit a₂
-  match v₁, v₂ with
-  | some true,  _ => a₂
-  | some false, _ => a₁
-  | _, some true  => a₁
-  | _, some false => a₂
-  | _, _          => none
-
-def foldStrictOr (_ : Bool) (a₁ a₂ : Expr) : Option Expr :=
-  let v₁ := getBoolLit a₁
-  let v₂ := getBoolLit a₂
-  match v₁, v₂ with
-  | some true,  _ => a₁
-  | some false, _ => a₂
-  | _, some true  => a₂
-  | _, some false => a₁
-  | _, _          => none
-
-def boolFoldFns : List (Name × BinFoldFn) :=
-  [(``strictOr, foldStrictOr), (``strictAnd, foldStrictAnd)]
-
 def binFoldFns : List (Name × BinFoldFn) :=
-  boolFoldFns ++ uintBinFoldFns ++ natFoldFns
+  uintBinFoldFns ++ natFoldFns
 
 def foldNatSucc (_ : Bool) (a : Expr) : Option Expr := do
   let n ← getNumLit a
diff --git a/tests/compiler/strictOrSimp.lean b/tests/compiler/strictOrSimp.lean
deleted file mode 100644
index ea135c5015..0000000000
--- a/tests/compiler/strictOrSimp.lean
+++ /dev/null
@@ -1,11 +0,0 @@
-partial def spin : Nat → Bool
-| n => spin (n)
-
-@[inline] def C : Nat := 0
-
-def f (b : Nat) :=
-if strictOr (C == 0) (spin b) then "hello"
-else "world"
-
-def main (xs : List String) : IO Unit :=
-IO.println (f 0)