Lean.Meta.WHNF

source

def Lean.Meta.smartUnfoldingSuffix :

String

Equations

Lean.Meta.smartUnfoldingSuffix = "_sunfold"

source

@[inline]

def Lean.Meta.mkSmartUnfoldingNameFor (declName : Lean.Name) :

Lean.Name

Equations

Lean.Meta.mkSmartUnfoldingNameFor declName = Lean.Name.mkStr declName Lean.Meta.smartUnfoldingSuffix

source

def Lean.Meta.hasSmartUnfoldingDecl (env : Lean.Environment) (declName : Lean.Name) :

Bool

Equations

Lean.Meta.hasSmartUnfoldingDecl env declName = Lean.Environment.contains env (Lean.Meta.mkSmartUnfoldingNameFor declName)

source

constant Lean.Meta.smartUnfolding :

Lean.Option Bool

source

def Lean.Meta.markSmartUnfoldingMatch (e : Lean.Expr) :

Lean.Expr

Equations

Lean.Meta.markSmartUnfoldingMatch e = Lean.mkAnnotation `sunfoldMatch e

source

def Lean.Meta.smartUnfoldingMatch? (e : Lean.Expr) :

Option Lean.Expr

Equations

Lean.Meta.smartUnfoldingMatch? e = Lean.annotation? `sunfoldMatch e

source

def Lean.Meta.markSmartUnfoldigMatchAlt (e : Lean.Expr) :

Lean.Expr

Equations

Lean.Meta.markSmartUnfoldigMatchAlt e = Lean.mkAnnotation `sunfoldMatchAlt e

source

def Lean.Meta.smartUnfoldingMatchAlt? (e : Lean.Expr) :

Option Lean.Expr

Equations

Lean.Meta.smartUnfoldingMatchAlt? e = Lean.annotation? `sunfoldMatchAlt e

source

def Lean.Meta.isAuxDef (constName : Lean.Name) :

Lean.MetaM Bool

Equations

Lean.Meta.isAuxDef constName = do let env ← Lean.getEnv pure (Lean.isAuxRecursor env constName || Lean.isNoConfusion env constName)

source

def Lean.Meta.toCtorIfLit :

Lean.Expr → Lean.Expr

Equations

Lean.Meta.toCtorIfLit x = match x with | Lean.Expr.lit (Lean.Literal.natVal v) x => if (v == 0) = true then Lean.mkConst `Nat.zero else Lean.mkApp (Lean.mkConst `Nat.succ) (Lean.mkRawNatLit (v - 1)) | Lean.Expr.lit (Lean.Literal.strVal v) x => Lean.mkApp (Lean.mkConst `String.mk) (Lean.toExpr (String.toList v)) | e => e

source

partial def Lean.Meta.getStuckMVar? :

Lean.Expr → Lean.MetaM (Option Lean.MVarId)

source

@[specialize]

partial def Lean.Meta.whnfEasyCases (e : Lean.Expr) (k : Lean.Expr → Lean.MetaM Lean.Expr) :

Lean.MetaM Lean.Expr

source

inductive Lean.Meta.ReduceMatcherResult :

Type

reduced: Lean.Expr → Lean.Meta.ReduceMatcherResult
stuck: Lean.Expr → Lean.Meta.ReduceMatcherResult
notMatcher: Lean.Meta.ReduceMatcherResult
partialApp: Lean.Meta.ReduceMatcherResult

source

def Lean.Meta.reduceMatcher? (e : Lean.Expr) :

Lean.MetaM Lean.Meta.ReduceMatcherResult

Equations

Lean.Meta.reduceMatcher? e = match Lean.Expr.getAppFn e with | Lean.Expr.const declName declLevels x => do let discr ← Lean.Meta.getMatcherInfo? declName match discr with | some info => let args := Lean.Expr.getAppArgs e; let prefixSz := info.numParams + 1 + info.numDiscrs; if Array.size args < prefixSz + Lean.Meta.Match.MatcherInfo.numAlts info then pure Lean.Meta.ReduceMatcherResult.partialApp else do let constInfo ← Lean.getConstInfo declName let f : Lean.Expr := Lean.ConstantInfo.instantiateValueLevelParams constInfo declLevels let auxApp : Lean.Expr := Lean.mkAppN f (Array.ofSubarray (Array.toSubarray args 0 prefixSz)) let auxAppType ← Lean.Meta.inferType auxApp Lean.Meta.forallBoundedTelescope auxAppType (some (Lean.Meta.Match.MatcherInfo.numAlts info)) fun hs x => do let auxApp ← Lean.Meta.whnfMatcher (Lean.mkAppN auxApp hs) let auxAppFn : Lean.Expr := Lean.Expr.getAppFn auxApp let i : Nat := prefixSz let r ← forIn hs { fst := none, snd := i } fun h r => let r := r.snd; let i := r; let _do_jp := fun i y => let i := i + 1; do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := i }); if (auxAppFn == h) = true then let result := Lean.mkAppN (Array.getOp args i) (Lean.Expr.getAppArgs auxApp); let result := Lean.mkAppN result (Array.ofSubarray (Array.toSubarray args (prefixSz + Lean.Meta.Match.MatcherInfo.numAlts info) (Array.size args))); pure (ForInStep.done { fst := some (Lean.Meta.ReduceMatcherResult.reduced (Lean.Expr.headBeta result)), snd := i }) else do let y ← pure PUnit.unit _do_jp i y let x : Nat := r.snd let i : Nat := x let _do_jp : PUnit → Lean.MetaM Lean.Meta.ReduceMatcherResult := fun y => pure (Lean.Meta.ReduceMatcherResult.stuck auxApp) match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a | x => pure Lean.Meta.ReduceMatcherResult.notMatcher | x => pure Lean.Meta.ReduceMatcherResult.notMatcher

source

def Lean.Meta.project? (e : Lean.Expr) (i : Nat) :

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Meta.project? e i = do let e ← Lean.Meta.whnf e let e : Lean.Expr := Lean.Meta.toCtorIfLit e Lean.matchConstCtor (Lean.Expr.getAppFn e) (fun x => pure none) fun ctorVal x => let numArgs := Lean.Expr.getAppNumArgs e; let idx := ctorVal.numParams + i; if idx < numArgs then pure (some (Lean.Expr.getArg! e idx (Lean.Expr.getAppNumArgs e))) else pure none

source

def Lean.Meta.reduceProj? (e : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Meta.reduceProj? e = match e with | Lean.Expr.proj x i c x_1 => Lean.Meta.project? c i | x => pure none

source

partial def Lean.Meta.whnfCore (e : Lean.Expr) :

Lean.MetaM Lean.Expr

source

def Lean.Meta.smartUnfoldingReduce? (e : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Meta.smartUnfoldingReduce? e = (fun goMatch => OptionT.run (go e)) Lean.Meta.smartUnfoldingReduce?.go Lean.Meta.smartUnfoldingReduce?.goMatch

source

partial def Lean.Meta.smartUnfoldingReduce?.go (e : Lean.Expr) :

OptionT Lean.MetaM Lean.Expr

source

partial def Lean.Meta.smartUnfoldingReduce?.goMatch (e : Lean.Expr) :

OptionT Lean.MetaM Lean.Expr

source

partial def Lean.Meta.unfoldProjInst? (e : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

source

partial def Lean.Meta.unfoldDefinition? (e : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

source

def Lean.Meta.unfoldDefinition (e : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.unfoldDefinition e = do let discr ← Lean.Meta.unfoldDefinition? e match discr with | some e => pure e | x => Lean.throwError (Lean.toMessageData "failed to unfold definition" ++ Lean.toMessageData (Lean.indentExpr e) ++ Lean.toMessageData "")

source

@[specialize]

partial def Lean.Meta.whnfHeadPred (e : Lean.Expr) (pred : Lean.Expr → Lean.MetaM Bool) :

Lean.MetaM Lean.Expr

source

def Lean.Meta.whnfUntil (e : Lean.Expr) (declName : Lean.Name) :

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Meta.whnfUntil e declName = do let e ← Lean.Meta.whnfHeadPred e fun e => pure !Lean.Expr.isAppOf e declName if Lean.Expr.isAppOf e declName = true then pure (some e) else pure none

source

def Lean.Meta.reduceRecMatcher? (e : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Meta.reduceRecMatcher? e = if (!Lean.Expr.isApp e) = true then pure none else do let a ← Lean.Meta.reduceMatcher? e match a with | Lean.Meta.ReduceMatcherResult.reduced e => pure (some e) | x => Lean.Meta.matchConstAux (Lean.Expr.getAppFn e) (fun x => pure none) fun cinfo lvls => match cinfo with | Lean.ConstantInfo.recInfo rec => Lean.Meta.reduceRec rec lvls (Lean.Expr.getAppArgs e) (fun x => pure none) fun e => pure (some e) | Lean.ConstantInfo.quotInfo rec => Lean.Meta.reduceQuotRec rec lvls (Lean.Expr.getAppArgs e) (fun x => pure none) fun e => pure (some e) | c@h:(Lean.ConstantInfo.defnInfo x) => do let a ← Lean.Meta.isAuxDef (Lean.ConstantInfo.name c) if a = true then Lean.Meta.deltaBetaDefinition c lvls (Lean.Expr.getAppRevArgs e) (fun x => pure none) fun e => pure (some e) else pure none | x => pure none

source

unsafe def Lean.Meta.reduceBoolNativeUnsafe (constName : Lean.Name) :

Lean.MetaM Bool

Equations

Lean.Meta.reduceBoolNativeUnsafe constName = Lean.evalConstCheck Bool `Bool constName

source

unsafe def Lean.Meta.reduceNatNativeUnsafe (constName : Lean.Name) :

Lean.MetaM Nat

Equations

Lean.Meta.reduceNatNativeUnsafe constName = Lean.evalConstCheck Nat `Nat constName

source

@[implementedBy Lean.Meta.reduceBoolNativeUnsafe]

constant Lean.Meta.reduceBoolNative (constName : Lean.Name) :

Lean.MetaM Bool

source

@[implementedBy Lean.Meta.reduceNatNativeUnsafe]

constant Lean.Meta.reduceNatNative (constName : Lean.Name) :

Lean.MetaM Nat

source

def Lean.Meta.reduceNative? (e : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Meta.reduceNative? e = match e with | Lean.Expr.app (Lean.Expr.const fName x x_1) (Lean.Expr.const argName x_2 x_3) x_4 => if (fName == `Lean.reduceBool) = true then do let a ← Lean.Meta.reduceBoolNative argName pure (some (Lean.toExpr a)) else if (fName == `Lean.reduceNat) = true then do let a ← Lean.Meta.reduceNatNative argName pure (some (Lean.toExpr a)) else pure none | x => pure none

source

@[inline]

def Lean.Meta.withNatValue {α : Type} (a : Lean.Expr) (k : Nat → Lean.MetaM (Option α)) :

Lean.MetaM (Option α)

Equations

Lean.Meta.withNatValue a k = do let a ← Lean.Meta.whnf a match a with | Lean.Expr.const (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "Nat" x_2) "zero" x_3) x x_1 => k 0 | Lean.Expr.lit (Lean.Literal.natVal v) x => k v | x => pure none

source

def Lean.Meta.reduceUnaryNatOp (f : Nat → Nat) (a : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Meta.reduceUnaryNatOp f a = Lean.Meta.withNatValue a fun a => pure (some (Lean.mkRawNatLit (f a)))

source

def Lean.Meta.reduceBinNatOp (f : Nat → Nat → Nat) (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Meta.reduceBinNatOp f a b = Lean.Meta.withNatValue a fun a => Lean.Meta.withNatValue b fun b => let cls := `Meta.isDefEq.whnf.reduceBinOp; do let a_1 ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Option Lean.Expr) := fun y => pure (some (Lean.mkRawNatLit (f a b))) if a_1 = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData a ++ Lean.toMessageData " op " ++ Lean.toMessageData b ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Meta.reduceBinNatPred (f : Nat → Nat → Bool) (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Meta.reduceBinNatPred f a b = Lean.Meta.withNatValue a fun a => Lean.Meta.withNatValue b fun b => pure (some (Lean.toExpr (f a b)))

source

def Lean.Meta.reduceNat? (e : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Meta.reduceNat? e = if (Lean.Expr.hasFVar e || Lean.Expr.hasMVar e) = true then pure none else match e with | Lean.Expr.app (Lean.Expr.const fn x x_1) a x_2 => if (fn == `Nat.succ) = true then Lean.Meta.reduceUnaryNatOp Nat.succ a else pure none | Lean.Expr.app (Lean.Expr.app (Lean.Expr.const fn x x_1) a1 x_2) a2 x_3 => if (fn == `Nat.add) = true then Lean.Meta.reduceBinNatOp Nat.add a1 a2 else if (fn == `Nat.sub) = true then Lean.Meta.reduceBinNatOp Nat.sub a1 a2 else if (fn == `Nat.mul) = true then Lean.Meta.reduceBinNatOp Nat.mul a1 a2 else if (fn == `Nat.div) = true then Lean.Meta.reduceBinNatOp Nat.div a1 a2 else if (fn == `Nat.mod) = true then Lean.Meta.reduceBinNatOp Nat.mod a1 a2 else if (fn == `Nat.beq) = true then Lean.Meta.reduceBinNatPred Nat.beq a1 a2 else if (fn == `Nat.ble) = true then Lean.Meta.reduceBinNatPred Nat.ble a1 a2 else pure none | x => pure none

source

partial def Lean.Meta.whnfImp (e : Lean.Expr) :

Lean.MetaM Lean.Expr

source

def Lean.Meta.reduceProjOf? (e : Lean.Expr) (p : Lean.Name → Bool) :

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Meta.reduceProjOf? e p = if (!Lean.Expr.isApp e) = true then pure none else match Lean.Expr.getAppFn e with | Lean.Expr.const name x x_1 => do let env ← Lean.getEnv match Lean.Environment.getProjectionStructureName? env name with | some structName => if p structName = true then Lean.Meta.unfoldDefinition? e else pure none | none => pure none | x => pure none