35 lines
870 B
Text
35 lines
870 B
Text
/-
|
|
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Leonardo de Moura
|
|
-/
|
|
import Lean.Meta.Transform
|
|
|
|
namespace Lean.Elab.Structural
|
|
open Meta
|
|
|
|
private def shouldBetaReduce (e : Expr) (recFnName : Name) : Bool :=
|
|
if e.isHeadBetaTarget then
|
|
e.getAppFn.find? (·.isConstOf recFnName) |>.isSome
|
|
else
|
|
false
|
|
|
|
/--
|
|
Beta reduce terms where the recursive function occurs in the lambda term.
|
|
This is useful to improve the effectiveness of `elimRecursion`.
|
|
Example:
|
|
```
|
|
def f : Nat → Nat
|
|
| 0 => 1
|
|
| i+1 => (fun x => f x) i
|
|
```
|
|
-/
|
|
def preprocess (e : Expr) (recFnName : Name) : CoreM Expr :=
|
|
Core.transform e
|
|
fun e => return TransformStep.visit <|
|
|
if shouldBetaReduce e recFnName then
|
|
e.headBeta
|
|
else
|
|
e
|
|
|
|
end Lean.Elab.Structural
|