| /- | |
| Copyright (c) 2019 Microsoft Corporation. All rights reserved. | |
| Released under Apache 2.0 license as described in the file LICENSE. | |
| Authors: Leonardo de Moura | |
| -/ | |
| 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 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]!.isNatLit then | |
| return mkRawNatLit (args[0]!.natLit?.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 |