From f30ff6ae798447b7a2caa018e24ea8431b7d8112 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 29 Aug 2024 19:03:51 +0200
Subject: [PATCH] refactor: put new eqns options into backward namespace
 (#5207)

in #4154 and #5129 the rules for equational lemmas have changed, and new
options were introduced that can be used to revert to the pre-4.12
behavior. Hopefully nobody really needs these options besides for
backwards compatibility, therefore we put these options in the
`backward` option name space.

So the previous behavior can be achieved by setting
```lean
set_option backward.eqns.nonrecursive false
set_option backward.eqns.deepRecursiveSplit false
```
---
 src/Lean/Elab/PreDefinition/Eqns.lean        | 2 +-
 src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean | 2 +-
 src/Lean/Meta/Eqns.lean                      | 6 +++---
 tests/lean/run/eqnOptions.lean               | 4 ++--
 tests/lean/run/wfEqns5.lean                  | 4 ++--
 5 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index 11ec07514d..62350a1556 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -91,7 +91,7 @@ private def findMatchToSplit? (deepRecursiveSplit : Bool) (env : Environment) (e
 partial def splitMatch? (mvarId : MVarId) (declNames : Array Name) : MetaM (Option (List MVarId)) := commitWhenSome? do
   let target ← mvarId.getType'
   let rec go (badCases : ExprSet) : MetaM (Option (List MVarId)) := do
-    if let some e := findMatchToSplit? (eqns.deepRecursiveSplit.get (← getOptions)) (← getEnv)
+    if let some e := findMatchToSplit? (backward.eqns.deepRecursiveSplit.get (← getOptions)) (← getEnv)
                                        target declNames badCases then
       try
         Meta.Split.splitMatch mvarId e
diff --git a/src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean b/src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean
index c0c20ee104..8121cf2f69 100644
--- a/src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean
@@ -94,7 +94,7 @@ def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if (← isRecursiveDefinition declName) then
     return none
   if let some (.defnInfo info) := (← getEnv).find? declName then
-    if eqns.nonrecursive.get (← getOptions) then
+    if backward.eqns.nonrecursive.get (← getOptions) then
       mkEqns declName info
     else
       let o ← mkSimpleEqThm declName
diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean
index 8707ca4edc..80e57b225f 100644
--- a/src/Lean/Meta/Eqns.lean
+++ b/src/Lean/Meta/Eqns.lean
@@ -12,12 +12,12 @@ import Lean.Meta.Match.MatcherInfo
 
 namespace Lean.Meta
 
-register_builtin_option eqns.nonrecursive : Bool := {
+register_builtin_option backward.eqns.nonrecursive : Bool := {
     defValue := true
     descr    := "Create fine-grained equational lemmas even for non-recursive definitions."
   }
 
-register_builtin_option eqns.deepRecursiveSplit : Bool := {
+register_builtin_option backward.eqns.deepRecursiveSplit : Bool := {
     defValue := true
     descr    := "Create equational lemmas for recursive functions like for non-recursive \
                 functions. If disabled, match statements in recursive function definitions \
@@ -35,7 +35,7 @@ This is implemented by
  * eagerly realizing the equations when they are set to a non-default vaule
  * when realizing them lazily, reset the options to their default
 -/
-def eqnAffectingOptions : Array (Lean.Option Bool) := #[eqns.nonrecursive, eqns.deepRecursiveSplit]
+def eqnAffectingOptions : Array (Lean.Option Bool) := #[backward.eqns.nonrecursive, backward.eqns.deepRecursiveSplit]
 
 /--
 Environment extension for storing which declarations are recursive.
diff --git a/tests/lean/run/eqnOptions.lean b/tests/lean/run/eqnOptions.lean
index 3055e2dacd..3d85276acb 100644
--- a/tests/lean/run/eqnOptions.lean
+++ b/tests/lean/run/eqnOptions.lean
@@ -17,7 +17,7 @@ end Test1
 
 namespace Test2
 
-set_option eqns.nonrecursive false in
+set_option backward.eqns.nonrecursive false in
 def nonrecfun : Bool → Nat
   | false => 0
   | true => 0
@@ -42,7 +42,7 @@ def nonrecfun : Bool → Nat
   | true => 0
 
 -- should have no effect
-set_option eqns.nonrecursive false
+set_option backward.eqns.nonrecursive false
 
 /--
 info: equations:
diff --git a/tests/lean/run/wfEqns5.lean b/tests/lean/run/wfEqns5.lean
index 5402be4e06..71e48766e6 100644
--- a/tests/lean/run/wfEqns5.lean
+++ b/tests/lean/run/wfEqns5.lean
@@ -32,7 +32,7 @@ info: foo.eq_def :
 #check foo.eq_4
 
 
-set_option eqns.deepRecursiveSplit false in
+set_option backward.eqns.deepRecursiveSplit false in
 def bar : Nat → Nat → Nat
   | 0, m => match m with | 0 => 0 | m => m
   | n+1, m => bar n m
@@ -101,7 +101,7 @@ info: Structural.foo.eq_def :
 #check Structural.foo.eq_4
 
 
-set_option eqns.deepRecursiveSplit false in
+set_option backward.eqns.deepRecursiveSplit false in
 def bar : Nat → Nat → Nat
   | 0, m => match m with | 0 => 0 | m => m
   | n+1, m => bar n m