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

@@ -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

tests/compiler/strictOrSimp.lean

@@ -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)