98e4b2882f
This PR migrates usages of `Std.Range` to the new polymorphic ranges. This PR unfortunately increases the transitive imports for frequently-used parts of `Init` because the ranges now rely on iterators in order to provide their functionality for types other than `Nat`. However, iteration over ranges in compiled code is as efficient as before in the examples I checked. This is because of a special `IteratorLoop` implementation provided in the PR for this purpose. There were two issues that were uncovered during migration: * In `IndPredBelow.lean`, migrating the last remaining range causes `compilerTest1.lean` to break. I have minimized the issue and came to the conclusion it's a compiler bug. Therefore, I have not replaced said old range usage yet (see #9186). * In `BRecOn.lean`, we are publicly importing the ranges. Making this import private should theoretically work, but there seems to be a problem with the module system, causing the build to panic later in `Init.Data.Grind.Poly` (see #9185). * In `FuzzyMatching.lean`, inlining fails with the new ranges, which would have led to significant slowdown. Therefore, I have not migrated this file either.
48 lines
1.7 KiB
Text
48 lines
1.7 KiB
Text
/-
|
|
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Leonardo de Moura
|
|
-/
|
|
prelude
|
|
import Lean.Meta.Basic
|
|
import Lean.Meta.FunInfo
|
|
import Lean.Util.MonadCache
|
|
|
|
namespace Lean.Meta
|
|
|
|
partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : MetaM Expr :=
|
|
let rec visit (e : Expr) : MonadCacheT Expr Expr MetaM Expr :=
|
|
checkCache e fun _ => Core.withIncRecDepth do
|
|
if (← (pure skipTypes <&&> isType e)) then
|
|
return e
|
|
else if (← (pure skipProofs <&&> isProof e)) then
|
|
return e
|
|
else
|
|
let e ← whnf e
|
|
match e with
|
|
| Expr.app .. =>
|
|
let f ← visit e.getAppFn
|
|
let nargs := e.getAppNumArgs
|
|
let finfo ← getFunInfoNArgs f nargs
|
|
let mut args := e.getAppArgs
|
|
for i in *...args.size do
|
|
if h : i < finfo.paramInfo.size then
|
|
let info := finfo.paramInfo[i]
|
|
if !explicitOnly || info.isExplicit then
|
|
args ← args.modifyM i visit
|
|
else
|
|
args ← args.modifyM i visit
|
|
if f.isConstOf ``Nat.succ && args.size == 1 && args[0]!.isRawNatLit then
|
|
return mkRawNatLit (args[0]!.rawNatLit?.get! + 1)
|
|
else
|
|
return mkAppN f args
|
|
| Expr.lam .. => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b)
|
|
| Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← visit b)
|
|
| Expr.proj n i s .. => return mkProj n i (← visit s)
|
|
| _ => return e
|
|
visit e |>.run
|
|
|
|
def reduceAll (e : Expr) : MetaM Expr :=
|
|
reduce e false false false
|
|
|
|
end Lean.Meta
|