| /- | |
| 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 (← (skipTypes <&&> isType e)) then | |
| return e | |
| else if (← (skipProofs <&&> isProof e)) then | |
| return e | |
| else | |
| let e ← whnf e | |
| match e with | |
| | Expr.app .. => | |
| let f := 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 | |
| pure (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) | |
| | _ => return e | |
| visit e |>.run | |
| end Lean.Meta |