Lean.PrettyPrinter.Delaborator.Builtins

source

def Lean.PrettyPrinter.Delaborator.maybeAddBlockImplicit (ident : Lean.Syntax) :

Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax

Equations

Lean.PrettyPrinter.Delaborator.maybeAddBlockImplicit ident = do let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPAnalysisBlockImplicit if a = true then do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.explicit #[Lean.Syntax.atom info "@", ident]) else pure ident

source

def Lean.PrettyPrinter.Delaborator.unfoldMDatas :

Lean.Expr → Lean.Expr

Equations

source

def Lean.PrettyPrinter.Delaborator.delabFVar :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabFVar = do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.fvar id x => tryCatch (do let l ← liftM (Lean.Meta.getLocalDecl id) Lean.PrettyPrinter.Delaborator.maybeAddBlockImplicit (Lean.mkIdent (Lean.LocalDecl.userName l))) fun x => Lean.PrettyPrinter.Delaborator.maybeAddBlockImplicit (Lean.mkIdent id.name) | x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.Builtins" "Lean.PrettyPrinter.Delaborator.delabFVar" 26 31 "unreachable code has been reached"

source

def Lean.PrettyPrinter.Delaborator.delabBVar :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabBVar = do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.bvar idx x => pure (Lean.mkIdent (Lean.Name.mkSimple ("#" ++ toString idx))) | x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.Builtins" "Lean.PrettyPrinter.Delaborator.delabBVar" 37 34 "unreachable code has been reached"

source

def Lean.PrettyPrinter.Delaborator.delabMVar :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabMVar = do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.mvar n x => do let mvarDecl ← liftM (Lean.Meta.getMVarDecl n) let n : Lean.Name := match mvarDecl.userName with | Lean.Name.anonymous => Lean.Name.replacePrefix n.name `_uniq `m | n => n let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.syntheticHole #[Lean.Syntax.atom info "?", Lean.mkIdent n]) | x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.Builtins" "Lean.PrettyPrinter.Delaborator.delabMVar" 42 32 "unreachable code has been reached"

source

def Lean.PrettyPrinter.Delaborator.delabSort :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabSort = do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.sort l x => match l with | Lean.Level.zero x => do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.prop #[Lean.Syntax.atom info "Prop"]) | Lean.Level.succ (Lean.Level.zero x) x_1 => do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.type #[Lean.Syntax.atom info "Type", Lean.Syntax.node Lean.SourceInfo.none `null #[]]) | x => match Lean.Level.dec l with | some l' => do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.type #[Lean.Syntax.atom info "Type", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Level.quote l' 1024]]) | none => do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.sort #[Lean.Syntax.atom info "Sort", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Level.quote l 1024]]) | x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.Builtins" "Lean.PrettyPrinter.Delaborator.delabSort" 52 32 "unreachable code has been reached"

source

def Lean.PrettyPrinter.Delaborator.unresolveNameGlobal (n₀ : Lean.Name) :

Lean.PrettyPrinter.Delaborator.DelabM Lean.Name

Equations

Lean.PrettyPrinter.Delaborator.unresolveNameGlobal n₀ = (fun unresolveNameCore => let _do_jp := fun y => do let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPFullNames let _do_jp : PUnit → Lean.PrettyPrinter.Delaborator.DelabM Lean.Name := fun y => do let a ← Lean.getEnv let initialNames : Array Lean.Name := List.toArray (Lean.getRevAliases a n₀) let initialNames : Array Lean.Name := Array.push initialNames (Lean.rootNamespace ++ n₀) let r ← forIn initialNames { fst := none, snd := PUnit.unit } fun initialName r => let r := r.snd; do let a ← unresolveNameCore initialName match a with | none => pure (ForInStep.yield { fst := none, snd := PUnit.unit }) | some n => pure (ForInStep.done { fst := some n, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.PrettyPrinter.Delaborator.DelabM Lean.Name := fun y => pure n₀ match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a if a = true then do let a ← Lean.resolveGlobalName n₀ match a with | [(potentialMatch, x)] => if (potentialMatch == n₀) = true then pure n₀ else pure (Lean.rootNamespace ++ n₀) | x => pure n₀ else do let y ← pure PUnit.unit _do_jp y; if Lean.Name.hasMacroScopes n₀ = true then pure n₀ else do let y ← pure PUnit.unit _do_jp y) (Lean.PrettyPrinter.Delaborator.unresolveNameGlobal.unresolveNameCore n₀)

source

def Lean.PrettyPrinter.Delaborator.unresolveNameGlobal.unresolveNameCore (n₀ : Lean.Name) (n : Lean.Name) :

Lean.PrettyPrinter.Delaborator.DelabM (Option Lean.Name)

Equations

Lean.PrettyPrinter.Delaborator.unresolveNameGlobal.unresolveNameCore n₀ n = let revComponents := Lean.Name.components' n; let candidate := Lean.Name.anonymous; do let r ← let col := { start := 0, stop := List.length revComponents, step := 1 }; forIn col { fst := none, snd := { fst := candidate, snd := revComponents } } fun i r => let r := r.snd; let candidate := r.fst; let revComponents := r.snd; let _do_jp := fun candidate revComponents y => do let a ← Lean.resolveGlobalName candidate match a with | [(potentialMatch, x)] => if (potentialMatch == n₀) = true then pure (ForInStep.done { fst := some (some candidate), snd := { fst := candidate, snd := revComponents } }) else pure (ForInStep.yield { fst := none, snd := { fst := candidate, snd := revComponents } }) | x => pure (ForInStep.yield { fst := none, snd := { fst := candidate, snd := revComponents } }); match revComponents with | [] => pure (ForInStep.done { fst := some none, snd := { fst := candidate, snd := revComponents } }) | cmpt :: rest => let candidate := cmpt ++ candidate; let revComponents := rest; do let y ← pure PUnit.unit _do_jp candidate revComponents y let x : MProd Lean.Name (List Lean.Name) := r.snd match x with | { fst := candidate, snd := revComponents } => let _do_jp := fun y => pure none; match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a

source

def Lean.PrettyPrinter.Delaborator.delabConst :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabConst = do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.const c₀ ls x => do let _ ← read let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPPrivateNames let c₀ : Lean.Name := if a = true then c₀ else Option.getD (Lean.privateToUserName? c₀) c₀ let c ← Lean.PrettyPrinter.Delaborator.unresolveNameGlobal c₀ let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPUniverses let _do_jp : Lean.Name → Lean.Syntax → Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax := fun c stx => do let stx ← Lean.PrettyPrinter.Delaborator.maybeAddBlockImplicit stx let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPTagAppFns let _do_jp : Lean.Syntax → Unit → Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax := fun stx y => pure stx if a = true then do let r ← Lean.PrettyPrinter.Delaborator.annotateCurPos stx let stx : Lean.Syntax := r let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getPos let a_1 ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let y ← Lean.PrettyPrinter.Delaborator.addTermInfo a stx a_1 false _do_jp stx y else do let y ← pure PUnit.unit _do_jp stx y if (List.isEmpty ls || !a) = true then do let a ← Lean.getLCtx let _do_jp : Lean.Name → PUnit → Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax := fun c y => do let y ← pure (Lean.mkIdent c) _do_jp c y if Lean.LocalContext.usesUserName a c = true then do let a ← read if (c == c₀ && !a.inPattern) = true then let c := `_root_ ++ c; do let y ← pure PUnit.unit _do_jp c y else let c := c₀; do let y ← pure PUnit.unit _do_jp c y else do let y ← pure PUnit.unit _do_jp c y else do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.explicitUniv #[Lean.mkIdent c, Lean.Syntax.atom info ".{", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (let a := Array.map Lean.quote (List.toArray ls); Lean.mkSepArray (Array.map (fun a => a) a) (Lean.mkAtom ","))), Lean.Syntax.atom info "}"]) _do_jp c y | x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.Builtins" "Lean.PrettyPrinter.Delaborator.delabConst" 89 37 "unreachable code has been reached"

source

def Lean.PrettyPrinter.Delaborator.withMDataOptions {α : Type} [inst : Inhabited α] (x : Lean.PrettyPrinter.Delaborator.DelabM α) :

Lean.PrettyPrinter.Delaborator.DelabM α

Equations

Lean.PrettyPrinter.Delaborator.withMDataOptions x = do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match a with | Lean.Expr.mdata m x x_1 => do let a ← read let posOpts : Lean.PrettyPrinter.Delaborator.OptionsPerPos := a.optionsPerPos let pos ← Lean.PrettyPrinter.Delaborator.SubExpr.getPos let r ← forIn m posOpts fun x r => match x with | (k, v) => let posOpts := r; if Lean.Name.isPrefixOf `pp k = true then let opts := Option.getD (Std.RBMap.find? posOpts pos) { entries := [] }; let posOpts := Std.RBMap.insert posOpts pos (Lean.KVMap.insert opts k v); do pure PUnit.unit pure (ForInStep.yield posOpts) else do pure PUnit.unit pure (ForInStep.yield posOpts) let x : Lean.PrettyPrinter.Delaborator.OptionsPerPos := r let posOpts : Lean.PrettyPrinter.Delaborator.OptionsPerPos := x withReader (fun a => { defaultOptions := a.defaultOptions, optionsPerPos := posOpts, currNamespace := a.currNamespace, openDecls := a.openDecls, inPattern := a.inPattern, subExpr := a.subExpr }) (Lean.PrettyPrinter.Delaborator.SubExpr.withMDataExpr x) | x => x

source

partial def Lean.PrettyPrinter.Delaborator.withMDatasOptions {α : Type} [inst : Inhabited α] (x : Lean.PrettyPrinter.Delaborator.DelabM α) :

Lean.PrettyPrinter.Delaborator.DelabM α

source

def Lean.PrettyPrinter.Delaborator.delabAppFn :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabAppFn = do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr if Lean.Expr.isConst (Lean.Expr.consumeMData a) = true then Lean.PrettyPrinter.Delaborator.withMDatasOptions Lean.PrettyPrinter.Delaborator.delabConst else Lean.PrettyPrinter.Delaborator.delab

source

structure Lean.PrettyPrinter.Delaborator.ParamKind :

Type

name : Lean.Name
bInfo : Lean.BinderInfo
defVal : Option Lean.Expr
isAutoParam : Bool

source

def Lean.PrettyPrinter.Delaborator.ParamKind.isRegularExplicit (param : Lean.PrettyPrinter.Delaborator.ParamKind) :

Bool

Equations

Lean.PrettyPrinter.Delaborator.ParamKind.isRegularExplicit param = (Lean.BinderInfo.isExplicit param.bInfo && !param.isAutoParam && Option.isNone param.defVal)

source

def Lean.PrettyPrinter.Delaborator.getParamKinds :

Lean.PrettyPrinter.Delaborator.DelabM (Array Lean.PrettyPrinter.Delaborator.ParamKind)

Equations

Lean.PrettyPrinter.Delaborator.getParamKinds = (fun forallTelescopeArgs => do let e ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr tryCatch (Lean.Meta.withTransparency Lean.Meta.TransparencyMode.all (forallTelescopeArgs (Lean.Expr.getAppFn e) (Lean.Expr.getAppArgs e) fun params x => Array.mapM (fun param => do let l ← liftM (Lean.Meta.getLocalDecl (Lean.Expr.fvarId! param)) pure { name := Lean.LocalDecl.userName l, bInfo := Lean.LocalDecl.binderInfo l, defVal := Lean.Expr.getOptParamDefault? (Lean.LocalDecl.type l), isAutoParam := Lean.Expr.isAutoParam (Lean.LocalDecl.type l) }) params)) fun x => pure #[]) Lean.PrettyPrinter.Delaborator.getParamKinds.forallTelescopeArgs

source

partial def Lean.PrettyPrinter.Delaborator.getParamKinds.forallTelescopeArgs (f : Lean.Expr) (args : Array Lean.Expr) (k : Array Lean.Expr → Lean.Expr → Lean.PrettyPrinter.Delaborator.DelabM (Array Lean.PrettyPrinter.Delaborator.ParamKind)) :

Lean.PrettyPrinter.Delaborator.DelabM (Array Lean.PrettyPrinter.Delaborator.ParamKind)

source

def Lean.PrettyPrinter.Delaborator.delabAppExplicit :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabAppExplicit = do let paramKinds ← Lean.PrettyPrinter.Delaborator.getParamKinds let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.withAppFnArgs (do let stx ← Lean.PrettyPrinter.Delaborator.delabAppFn let needsExplicit : Bool := Lean.Syntax.getKind stx != `Lean.Parser.Term.explicit let _do_jp : Lean.Syntax → Lean.PrettyPrinter.Delaborator.DelabM (Lean.Syntax × List Lean.PrettyPrinter.Delaborator.ParamKind × Array Lean.Syntax) := fun stx => pure (stx, Array.toList paramKinds, #[]) if needsExplicit = true then do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.explicit #[Lean.Syntax.atom info "@", stx]) _do_jp y else do let y ← pure stx _do_jp y) fun x => match x with | (fnStx, paramKinds, argStxs) => let isInstImplicit := match paramKinds with | [] => false | param :: x => param.bInfo == Lean.BinderInfo.instImplicit; do let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPAnalysisHole let _do_jp : Lean.Syntax → Lean.PrettyPrinter.Delaborator.DelabM (Lean.Syntax × List Lean.PrettyPrinter.Delaborator.ParamKind × Array Lean.Syntax) := fun argStx => pure (fnStx, List.tailD paramKinds [], Array.push argStxs argStx) if a = true then do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]) _do_jp y else if (isInstImplicit == true) = true then do let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPInstances let _do_jp : Lean.Syntax → Lean.PrettyPrinter.Delaborator.DelabM (Lean.Syntax × List Lean.PrettyPrinter.Delaborator.ParamKind × Array Lean.Syntax) := fun stx => do let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPInstanceTypes if a = true then do let typeStx ← Lean.PrettyPrinter.Delaborator.SubExpr.withType Lean.PrettyPrinter.Delaborator.delab let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeAscription #[Lean.Syntax.atom info ":", typeStx]]], Lean.Syntax.atom info ")"]) _do_jp y else do let y ← pure stx _do_jp y if a = true then do let y ← Lean.PrettyPrinter.Delaborator.delab _do_jp y else do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]) _do_jp y else do let y ← Lean.PrettyPrinter.Delaborator.delab _do_jp y let x : Lean.Syntax × List Lean.PrettyPrinter.Delaborator.ParamKind × Array Lean.Syntax := discr match x with | (fnStx, x, argStxs) => pure (Lean.Syntax.mkApp fnStx argStxs)

source

def Lean.PrettyPrinter.Delaborator.shouldShowMotive (motive : Lean.Expr) (opts : Lean.Options) :

Lean.MetaM Bool

Equations

Lean.PrettyPrinter.Delaborator.shouldShowMotive motive opts = do let a ← pure (Lean.getPPMotivesPi opts) <&&> Lean.PrettyPrinter.Delaborator.returnsPi motive let a_1 ← pure (Lean.getPPMotivesNonConst opts) <&&> Lean.PrettyPrinter.Delaborator.isNonConstFun motive pure (Lean.getPPMotivesAll opts) <||> pure a <||> pure a_1

source

def Lean.PrettyPrinter.Delaborator.isRegularApp :

Lean.PrettyPrinter.Delaborator.DelabM Bool

Equations

Lean.PrettyPrinter.Delaborator.isRegularApp = do let e ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let _do_jp : PUnit → Lean.PrettyPrinter.Delaborator.DelabM Bool := fun y => do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.withNaryFn (Lean.PrettyPrinter.Delaborator.withMDatasOptions (Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPUniverses <||> Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPAnalysisBlockImplicit)) let _do_jp : PUnit → Lean.PrettyPrinter.Delaborator.DelabM Bool := fun y => do let r ← let col := { start := 0, stop := Lean.Expr.getAppNumArgs e, step := 1 }; forIn col { fst := none, snd := PUnit.unit } fun i r => let r := r.snd; do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.withNaryArg i (Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPAnalysisNamedArg) if a = true then pure (ForInStep.done { fst := some false, snd := PUnit.unit }) else do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.PrettyPrinter.Delaborator.DelabM Bool := fun y => pure true match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a if a = true then pure false else do let y ← pure PUnit.unit _do_jp y if (!Lean.Expr.isConst (Lean.PrettyPrinter.Delaborator.unfoldMDatas (Lean.Expr.getAppFn e))) = true then pure false else do let y ← pure PUnit.unit _do_jp y

source

def Lean.PrettyPrinter.Delaborator.unexpandRegularApp (stx : Lean.Syntax) :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.unexpandRegularApp stx = do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let discr ← pure (Lean.PrettyPrinter.Delaborator.unfoldMDatas (Lean.Expr.getAppFn a)) match discr with | Lean.Expr.const c x x_1 => do let a ← Lean.getEnv let fs ← pure (Lean.KeyedDeclsAttribute.getValues Lean.PrettyPrinter.Delaborator.appUnexpanderAttribute a c) let ref ← Lean.getRef List.firstM (fun f => match EStateM.run (ReaderT.run (f stx) ref) () with | EStateM.Result.ok stx x => pure stx | x => failure) fs | x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.Builtins" "Lean.PrettyPrinter.Delaborator.unexpandRegularApp" 201 67 "unreachable code has been reached"

source

def Lean.PrettyPrinter.Delaborator.unexpandCoe (stx : Lean.Syntax) :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.unexpandCoe stx = Lean.PrettyPrinter.Delaborator.whenPPOption Lean.getPPCoercions do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let a ← pure (Lean.PrettyPrinter.Delaborator.isCoe a) let _do_jp : PUnit → Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax := fun y => do let _ ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let discr : Lean.Syntax := stx if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 1 = true then let discr := Lean.Syntax.getArg discr_2 0; let arg := discr; let fn := discr_1; pure arg else let discr := Lean.Syntax.getArg discr 1; let args := Lean.Syntax.getArgs discr; let fn := discr_1; do let _ ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Array.get! args 0, Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (Array.eraseIdx args 0))]) else let discr := stx; failure if (!a) = true then do let y ← failure _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.PrettyPrinter.Delaborator.unexpandStructureInstance (stx : Lean.Syntax) :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.unexpandStructureInstance stx = Lean.PrettyPrinter.Delaborator.whenPPOption Lean.getPPStructureInstances do let env ← Lean.getEnv let e ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let discr ← pure (Lean.Expr.isConstructorApp? env e) match discr with | some s => do guard (Lean.isStructure env s.induct = true) let fieldNames : Array Lean.Name := Lean.getStructureFields env s.induct let fields : Array Lean.Syntax := #[] guard ((Array.size fieldNames == Lean.Syntax.getNumArgs (Lean.Syntax.getOp stx 1)) = true) let args : Array Lean.Expr := Lean.Expr.getAppArgs e let fieldVals : Array Lean.Expr := Array.extract args s.numParams (Array.size args) let r ← let col := { start := 0, stop := Array.size fieldNames, step := 1 }; forIn col fields fun idx r => let fields := r; let fieldName := Array.getOp fieldNames idx; let fieldId := Lean.mkIdent fieldName; do let fieldPos ← Lean.PrettyPrinter.Delaborator.SubExpr.nextExtraPos let fieldId : Lean.Syntax := Lean.PrettyPrinter.Delaborator.annotatePos fieldPos fieldId Lean.PrettyPrinter.Delaborator.addFieldInfo fieldPos (s.induct ++ fieldName) fieldName fieldId (Array.getOp fieldVals idx) let field ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.structInstField #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.structInstLVal #[fieldId, Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ":=", Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) idx]) let fields : Array Lean.Syntax := Array.push fields field pure PUnit.unit pure (ForInStep.yield fields) let x : Array Lean.Syntax := r let fields : Array Lean.Syntax := x let tyStx ← Lean.PrettyPrinter.Delaborator.SubExpr.withType do let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPStructureInstanceType if a = true then Lean.PrettyPrinter.Delaborator.delab >>= pure ∘ some else pure none if Array.isEmpty fields = true then do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.structInst #[Lean.Syntax.atom info "{", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.optEllipsis #[Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match tyStx with | some tyStx => #[Lean.Syntax.atom info ":", tyStx] | none => Array.empty)), Lean.Syntax.atom info "}"]) else let lastField := Array.back fields; let fields := Array.pop fields; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.structInst #[Lean.Syntax.atom info "{", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null (Array.push (Array.append #[] (Array.map (fun fields => Lean.Syntax.node Lean.SourceInfo.none `group #[fields, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ","]]) fields)) (Lean.Syntax.node Lean.SourceInfo.none `group #[lastField, Lean.Syntax.node Lean.SourceInfo.none `null #[]])), Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.optEllipsis #[Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (match tyStx with | some tyStx => #[Lean.Syntax.atom info ":", tyStx] | none => Array.empty)), Lean.Syntax.atom info "}"]) | x => failure

source

def Lean.PrettyPrinter.Delaborator.delabAppImplicit :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabAppImplicit = do let paramKinds ← Lean.PrettyPrinter.Delaborator.getParamKinds let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPExplicit let _do_jp : PUnit → Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax := fun y => let _do_jp := fun isImplicitApp => let _do_jp := fun y => do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.withAppFnArgs (do let a ← Lean.PrettyPrinter.Delaborator.delabAppFn pure (a, Array.toList paramKinds, #[])) fun x => match x with | (fnStx, paramKinds, argStxs) => do let arg ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let opts ← Lean.getOptions let mkNamedArg : Lean.Name → Lean.Syntax → Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax := fun name argStx => do let a ← pure (Lean.mkIdent name) let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.namedArgument #[Lean.Syntax.atom info "(", a, Lean.Syntax.atom info ":=", argStx, Lean.Syntax.atom info ")"]) let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPAnalysisSkip let a_1 ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPAnalysisHole let _do_jp : Option Lean.Syntax → Lean.PrettyPrinter.Delaborator.DelabM (Lean.Syntax × List Lean.PrettyPrinter.Delaborator.ParamKind × Array Lean.Syntax) := fun argStx? => let argStxs := match argStx? with | none => argStxs | some stx => Array.push argStxs stx; pure (fnStx, List.tailD paramKinds [], argStxs) if a = true then do let y ← pure none _do_jp y else if a_1 = true then do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.hole #[Lean.Syntax.atom info "_"]) _do_jp (some y) else match paramKinds with | [] => do let y ← Lean.PrettyPrinter.Delaborator.delab _do_jp (some y) | param :: rest => if (Option.isSome param.defVal && List.isEmpty rest) = true then let v := Option.get! param.defVal; if (!Lean.Expr.hasLooseBVars v && v == arg) = true then do let y ← pure none _do_jp y else do let y ← Lean.PrettyPrinter.Delaborator.delab _do_jp (some y) else if (!Lean.PrettyPrinter.Delaborator.ParamKind.isRegularExplicit param && Option.isNone param.defVal) = true then do let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPAnalysisNamedArg <||> pure (param.name == `motive) <&&> liftM (Lean.PrettyPrinter.Delaborator.shouldShowMotive arg opts) if a = true then do let a ← Lean.PrettyPrinter.Delaborator.delab let y ← mkNamedArg param.name a _do_jp (some y) else do let y ← pure none _do_jp y else do let y ← Lean.PrettyPrinter.Delaborator.delab _do_jp (some y) let x : Lean.Syntax × List Lean.PrettyPrinter.Delaborator.ParamKind × Array Lean.Syntax := discr match x with | (fnStx, x, argStxs) => let stx := Lean.Syntax.mkApp fnStx argStxs; do let a ← Lean.PrettyPrinter.Delaborator.isRegularApp if a = true then do let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPNotation let a_1 ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPStructureInstances let a_2 ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPNotation HOrElse.hOrElse (SeqRight.seqRight (guard (a = true)) fun x => Lean.PrettyPrinter.Delaborator.unexpandRegularApp stx) fun x => HOrElse.hOrElse (SeqRight.seqRight (guard (a_1 = true)) fun x => Lean.PrettyPrinter.Delaborator.unexpandStructureInstance stx) fun x => HOrElse.hOrElse (SeqRight.seqRight (guard (a_2 = true)) fun x => Lean.PrettyPrinter.Delaborator.unexpandCoe stx) fun x => pure stx else pure stx; if isImplicitApp = true then do let y ← failure _do_jp y else do let y ← pure PUnit.unit _do_jp y; do let y ← tryCatch (do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let a ← liftM (Lean.Meta.inferType a) let ty ← liftM (Lean.Meta.whnf a) pure (Lean.Expr.isForall ty && (Lean.Expr.binderInfo ty == Lean.BinderInfo.implicit || Lean.Expr.binderInfo ty == Lean.BinderInfo.instImplicit))) fun x => pure false _do_jp y if a = true then if Array.any paramKinds (fun param => !Lean.PrettyPrinter.Delaborator.ParamKind.isRegularExplicit param) 0 (Array.size paramKinds) = true then do let y ← failure _do_jp y else do let y ← pure PUnit.unit _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

structure Lean.PrettyPrinter.Delaborator.AppMatchState :

Type

info : Lean.Meta.MatcherInfo
matcherTy : Lean.Expr
params : Array Lean.Expr
motive : Option (Lean.Syntax × Lean.Expr)
motiveNamed : Bool
discrs : Array Lean.Syntax
varNames : Array (Array Lean.Name)
rhss : Array Lean.Syntax
moreArgs : Array Lean.Syntax

source

def Lean.PrettyPrinter.Delaborator.delabAppMatch :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabAppMatch = Lean.PrettyPrinter.Delaborator.whenPPOption Lean.getPPNotation (Lean.PrettyPrinter.Delaborator.whenPPOption Lean.getPPMatch do let st ← Lean.PrettyPrinter.Delaborator.SubExpr.withAppFnArgs (do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.const c us x => do let discr ← Lean.Meta.getMatcherInfo? c match discr with | some info => do let a ← Lean.getConstInfo c pure { info := info, matcherTy := Lean.ConstantInfo.instantiateTypeLevelParams a us, params := #[], motive := none, motiveNamed := false, discrs := #[], varNames := #[], rhss := #[], moreArgs := #[] } | x => failure | x => failure) fun st => if Array.size st.params < st.info.numParams then do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr pure { info := st.info, matcherTy := st.matcherTy, params := Array.push st.params a, motive := st.motive, motiveNamed := st.motiveNamed, discrs := st.discrs, varNames := st.varNames, rhss := st.rhss, moreArgs := st.moreArgs } else if Option.isNone st.motive = true then do let lamMotive ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let piMotive ← Lean.Meta.lambdaTelescope lamMotive fun xs body => liftM (Lean.Meta.mkForallFVars xs body false true) let piStx ← withTheReader Lean.PrettyPrinter.Delaborator.SubExpr (fun cfg => { expr := piMotive, pos := cfg.pos }) Lean.PrettyPrinter.Delaborator.delab let named ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPAnalysisNamedArg pure { info := st.info, matcherTy := st.matcherTy, params := st.params, motive := some (piStx, lamMotive), motiveNamed := named, discrs := st.discrs, varNames := st.varNames, rhss := st.rhss, moreArgs := st.moreArgs } else if Array.size st.discrs < st.info.numDiscrs then do let a ← Lean.PrettyPrinter.Delaborator.delab pure { info := st.info, matcherTy := st.matcherTy, params := st.params, motive := st.motive, motiveNamed := st.motiveNamed, discrs := Array.push st.discrs a, varNames := st.varNames, rhss := st.rhss, moreArgs := st.moreArgs } else if Array.size st.rhss < Array.size st.info.altNumParams then do let discr ← Lean.PrettyPrinter.Delaborator.skippingBinders (Array.getOp st.info.altNumParams (Array.size st.rhss)) fun varNames => do let rhs ← Lean.PrettyPrinter.Delaborator.delab pure (varNames, rhs) let x : Array Lean.Name × Lean.Syntax := discr match x with | (varNames, rhs) => pure { info := st.info, matcherTy := st.matcherTy, params := st.params, motive := st.motive, motiveNamed := st.motiveNamed, discrs := st.discrs, varNames := Array.push st.varNames varNames, rhss := Array.push st.rhss rhs, moreArgs := st.moreArgs } else do let a ← Lean.PrettyPrinter.Delaborator.delab pure { info := st.info, matcherTy := st.matcherTy, params := st.params, motive := st.motive, motiveNamed := st.motiveNamed, discrs := st.discrs, varNames := st.varNames, rhss := st.rhss, moreArgs := Array.push st.moreArgs a } let _do_jp : PUnit → Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax := fun y => let _discr := st.rhss; match st.discrs, st.rhss with | #[discr], #[] => do let stx ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.nomatch #[Lean.Syntax.atom info "nomatch", discr]) pure (Lean.Syntax.mkApp stx st.moreArgs) | x, #[] => failure | x, x_1 => do let pats ← Lean.PrettyPrinter.Delaborator.delabPatterns st let _do_jp : Lean.Syntax → Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax := fun stx => pure (Lean.Syntax.mkApp stx st.moreArgs) let x : Lean.Syntax × Lean.Expr := Option.get! st.motive match x with | (piStx, lamMotive) => do let opts ← Lean.getOptions let a ← pure st.motiveNamed <||> liftM (Lean.PrettyPrinter.Delaborator.shouldShowMotive lamMotive opts) if a = true then do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.match #[Lean.Syntax.atom info "match", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (let a := st.discrs; Lean.mkSepArray (Array.map (fun a => Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchDiscr #[Lean.Syntax.node Lean.SourceInfo.none `null #[], a]) a) (Lean.mkAtom ","))), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec #[Lean.Syntax.atom info ":", piStx]], Lean.Syntax.atom info "with", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (let a := st.rhss; Array.map (fun x => match x with | (pats, a) => Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (Lean.Syntax.SepArray.ofElems pats).elemsAndSeps), Lean.Syntax.atom info "=>", a]) (Array.zip pats a)))]]) _do_jp y else do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.match #[Lean.Syntax.atom info "match", Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (let a := st.discrs; Lean.mkSepArray (Array.map (fun a => Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchDiscr #[Lean.Syntax.node Lean.SourceInfo.none `null #[], a]) a) (Lean.mkAtom ","))), Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "with", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlts #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (let a := st.rhss; Array.map (fun x => match x with | (pats, a) => Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.matchAlt #[Lean.Syntax.atom info "|", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (Lean.Syntax.SepArray.ofElems pats).elemsAndSeps), Lean.Syntax.atom info "=>", a]) (Array.zip pats a)))]]) _do_jp y if (decide (Array.size st.discrs < st.info.numDiscrs) || decide (Array.size st.rhss < Array.size st.info.altNumParams)) = true then do let y ← failure _do_jp y else do let y ← pure PUnit.unit _do_jp y)

source

def Lean.PrettyPrinter.Delaborator.delabLetFun :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabLetFun = do let stxV ← Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg Lean.PrettyPrinter.Delaborator.delab Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.lam n t b x => do let n ← Lean.PrettyPrinter.Delaborator.getUnusedName n b let stxB ← Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody n Lean.PrettyPrinter.Delaborator.delab let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPLetVarTypes <||> Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPAnalysisLetVarType if a = true then do let stxT ← Lean.PrettyPrinter.Delaborator.SubExpr.withBindingDomain Lean.PrettyPrinter.Delaborator.delab let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.let_fun #[Lean.Syntax.atom info "let_fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letDecl #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letIdDecl #[Lean.mkIdent n, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec #[Lean.Syntax.atom info ":", stxT]], Lean.Syntax.atom info ":=", stxV]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], stxB]) else do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.let_fun #[Lean.Syntax.atom info "let_fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letDecl #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letIdDecl #[Lean.mkIdent n, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", stxV]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], stxB]) | x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.Builtins" "Lean.PrettyPrinter.Delaborator.delabLetFun" 434 37 "unreachable code has been reached"

source

def Lean.PrettyPrinter.Delaborator.delabMData :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabMData = do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match Lean.inaccessible? a with | some x => do let s ← Lean.PrettyPrinter.Delaborator.SubExpr.withMDataExpr Lean.PrettyPrinter.Delaborator.delab let a ← read if a.inPattern = true then do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.inaccessible #[Lean.Syntax.atom info ".(", s, Lean.Syntax.atom info ")"]) else pure s | x => do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let a_1 ← Lean.getOptions if (Lean.isLetFun a && Lean.getPPNotation a_1) = true then Lean.PrettyPrinter.Delaborator.SubExpr.withMDataExpr Lean.PrettyPrinter.Delaborator.delabLetFun else do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match Lean.isLHSGoal? a with | some x => Lean.PrettyPrinter.Delaborator.SubExpr.withMDataExpr (Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn (Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg Lean.PrettyPrinter.Delaborator.delab)) | x => Lean.PrettyPrinter.Delaborator.withMDataOptions Lean.PrettyPrinter.Delaborator.delab

source

partial def Lean.PrettyPrinter.Delaborator.hasIdent (id : Lean.Name) :

Lean.Syntax → Bool

source

def Lean.PrettyPrinter.Delaborator.delabLam :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabLam = Lean.PrettyPrinter.Delaborator.delabBinders (fun curNames stxBody => do let e ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let stxT ← Lean.PrettyPrinter.Delaborator.SubExpr.withBindingDomain Lean.PrettyPrinter.Delaborator.delab let ppTypes ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPFunBinderTypes let _ ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPExplicit let usedDownstream ← pure (Array.any curNames (fun n => Lean.PrettyPrinter.Delaborator.hasIdent (Lean.Syntax.getId n) stxBody) 0 (Array.size curNames)) let blockImplicitLambda : Bool := true if (!blockImplicitLambda) = true then pure stxBody else let defaultCase := fun x => if ppTypes = true then let _do_jp := fun stxCurNames => do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stxCurNames, Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeAscription #[Lean.Syntax.atom info ":", stxT]]], Lean.Syntax.atom info ")"]); if Array.size curNames > 1 then do let y ← do let _ ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app #[Array.get! curNames 0, Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] (Array.eraseIdx curNames 0))]) _do_jp y else do let y ← pure (Array.get! curNames 0) _do_jp y else pure (Array.back curNames); let _do_jp := fun group => let discr := stxBody; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.fun = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.isOfKind discr_2 `Lean.Parser.Term.basicFun = true then let discr := Lean.Syntax.getArg discr_2 0; let discr_3 := Lean.Syntax.getArg discr_2 1; let discr_4 := Lean.Syntax.getArg discr_2 2; let stxBody := discr_4; let binderGroups := Lean.Syntax.getArgs discr; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[group] binderGroups), Lean.Syntax.atom info "=>", stxBody]]) else let discr := Lean.Syntax.getArg discr 1; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun #[Lean.Syntax.node Lean.SourceInfo.none `null #[group], Lean.Syntax.atom info "=>", stxBody]]) else let discr := stxBody; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.fun #[Lean.Syntax.atom info "fun", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.basicFun #[Lean.Syntax.node Lean.SourceInfo.none `null #[group], Lean.Syntax.atom info "=>", stxBody]]); match Lean.Expr.binderInfo e, ppTypes with | Lean.BinderInfo.default, x => do let y ← defaultCase () _do_jp y | Lean.BinderInfo.auxDecl, x => do let y ← defaultCase () _do_jp y | Lean.BinderInfo.implicit, true => do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.implicitBinder #[Lean.Syntax.atom info "{", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] curNames), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ":", stxT], Lean.Syntax.atom info "}"]) _do_jp y | Lean.BinderInfo.implicit, false => do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.implicitBinder #[Lean.Syntax.atom info "{", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] curNames), Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "}"]) _do_jp y | Lean.BinderInfo.strictImplicit, true => do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.strictImplicitBinder #[Lean.Syntax.atom info "⦃", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] curNames), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ":", stxT], Lean.Syntax.atom info "⦄"]) _do_jp y | Lean.BinderInfo.strictImplicit, false => do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.strictImplicitBinder #[Lean.Syntax.atom info "⦃", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] curNames), Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info "⦄"]) _do_jp y | Lean.BinderInfo.instImplicit, x => if usedDownstream = true then do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.instBinder #[Lean.Syntax.atom info "[", Lean.Syntax.node Lean.SourceInfo.none `null #[Array.back curNames, Lean.Syntax.atom info ":"], stxT, Lean.Syntax.atom info "]"]) _do_jp y else do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.instBinder #[Lean.Syntax.atom info "[", Lean.Syntax.node Lean.SourceInfo.none `null #[], stxT, Lean.Syntax.atom info "]"]) _do_jp y) #[]

source

def Lean.PrettyPrinter.Delaborator.delabForall :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabForall = Lean.PrettyPrinter.Delaborator.delabBinders (fun curNames stxBody => do let e ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let _do_jp : Bool → Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax := fun prop => do let stxT ← Lean.PrettyPrinter.Delaborator.SubExpr.withBindingDomain Lean.PrettyPrinter.Delaborator.delab let _do_jp : Lean.Syntax → Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax := fun group => if prop = true then let discr := stxBody; if Lean.Syntax.isOfKind discr `Lean.Parser.Term.forall = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let discr_3 := Lean.Syntax.getArg discr 2; let discr := Lean.Syntax.getArg discr 3; let stxBody := discr; let groups := Lean.Syntax.getArgs discr_2; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.forall #[Lean.Syntax.atom info "∀", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[group] groups), Lean.Syntax.atom info ",", stxBody]) else let discr := stxBody; do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.forall #[Lean.Syntax.atom info "∀", Lean.Syntax.node Lean.SourceInfo.none `null #[group], Lean.Syntax.atom info ",", stxBody]) else do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.depArrow #[group, Lean.Syntax.atom info "→", stxBody]) match Lean.Expr.binderInfo e with | Lean.BinderInfo.implicit => do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.implicitBinder #[Lean.Syntax.atom info "{", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] curNames), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ":", stxT], Lean.Syntax.atom info "}"]) _do_jp y | Lean.BinderInfo.strictImplicit => do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.strictImplicitBinder #[Lean.Syntax.atom info "⦃", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] curNames), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ":", stxT], Lean.Syntax.atom info "⦄"]) _do_jp y | Lean.BinderInfo.instImplicit => do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.instBinder #[Lean.Syntax.atom info "[", Lean.Syntax.node Lean.SourceInfo.none `null #[Array.back curNames, Lean.Syntax.atom info ":"], stxT, Lean.Syntax.atom info "]"]) _do_jp y | x => let dependent := Array.any curNames (fun n => Lean.PrettyPrinter.Delaborator.hasIdent (Lean.Syntax.getId n) stxBody) 0 (Array.size curNames); if dependent = true then do let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPPiBinderTypes if (prop && !a) = true then do let a ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.forall #[Lean.Syntax.atom info "∀", Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.simpleBinder #[Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] curNames), Lean.Syntax.node Lean.SourceInfo.none `null #[]]], Lean.Syntax.atom info ",", stxBody]) pure a else do let y ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.explicitBinder #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null (Array.append #[] curNames), Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ":", stxT], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ")"]) _do_jp y else do let a ← Array.foldrM (fun x stxBody => do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.arrow #[stxT, Lean.Syntax.atom info "→", stxBody])) stxBody curNames (Array.size curNames) pure a let y ← tryCatch (liftM (Lean.Meta.isProp e)) fun x => pure false _do_jp y) #[]

source

def Lean.PrettyPrinter.Delaborator.delabLetE :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabLetE = do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.letE n t v b x => do let n ← Lean.PrettyPrinter.Delaborator.getUnusedName n b let stxV ← Lean.PrettyPrinter.Delaborator.SubExpr.descend v 1 Lean.PrettyPrinter.Delaborator.delab let stxB ← Lean.Meta.withLetDecl n t v fun fvar => let b := Lean.Expr.instantiate1 b fvar; Lean.PrettyPrinter.Delaborator.SubExpr.descend b 2 Lean.PrettyPrinter.Delaborator.delab let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPLetVarTypes <||> Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPAnalysisLetVarType if a = true then do let stxT ← Lean.PrettyPrinter.Delaborator.SubExpr.descend t 0 Lean.PrettyPrinter.Delaborator.delab let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.let #[Lean.Syntax.atom info "let", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letDecl #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letIdDecl #[Lean.mkIdent n, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.typeSpec #[Lean.Syntax.atom info ":", stxT]], Lean.Syntax.atom info ":=", stxV]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], stxB]) else do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.let #[Lean.Syntax.atom info "let", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letDecl #[Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.letIdDecl #[Lean.mkIdent n, Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.node Lean.SourceInfo.none `null #[], Lean.Syntax.atom info ":=", stxV]], Lean.Syntax.node Lean.SourceInfo.none `null #[Lean.Syntax.atom info ";"], stxB]) | x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.Builtins" "Lean.PrettyPrinter.Delaborator.delabLetE" 592 38 "unreachable code has been reached"

source

def Lean.PrettyPrinter.Delaborator.delabLit :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabLit = do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.lit l x => match l with | Lean.Literal.natVal n => pure (Lean.quote n) | Lean.Literal.strVal s => pure (Lean.quote s) | x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.Builtins" "Lean.PrettyPrinter.Delaborator.delabLit" 605 31 "unreachable code has been reached"

source

def Lean.PrettyPrinter.Delaborator.delabOfNat :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabOfNat = Lean.PrettyPrinter.Delaborator.whenPPOption Lean.getPPCoercions do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.app (Lean.Expr.app x (Lean.Expr.lit (Lean.Literal.natVal n) x_1) x_2) x_3 x_4 => pure (Lean.quote n) | x => failure

source

def Lean.PrettyPrinter.Delaborator.delabOfScientific :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabOfScientific = Lean.PrettyPrinter.Delaborator.whenPPOption Lean.getPPCoercions do let expr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr guard ((Lean.Expr.getAppNumArgs expr == 5) = true) let discr ← pure (Lean.Expr.getArg! expr 2 (Lean.Expr.getAppNumArgs expr)) match discr with | Lean.Expr.lit (Lean.Literal.natVal m) x => do let discr ← pure (Lean.Expr.getArg! expr 4 (Lean.Expr.getAppNumArgs expr)) match discr with | Lean.Expr.lit (Lean.Literal.natVal e) x => let _do_jp := fun s => let str := toString m; if (s && e == String.length str) = true then pure (Lean.Syntax.mkScientificLit ("0." ++ str)) else if (s && decide (e < String.length str)) = true then let mStr := String.extract str 0 (String.length str - e); let eStr := String.extract str (String.length str - e) (String.length str); pure (Lean.Syntax.mkScientificLit (mStr ++ "." ++ eStr)) else pure (Lean.Syntax.mkScientificLit ((str ++ "e" ++ if s = true then "-" else "") ++ toString e)); match Lean.Expr.getArg! expr 3 (Lean.Expr.getAppNumArgs expr) with | Lean.Expr.const (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "Bool" x_2) "true" x_3) x x_1 => do let y ← pure true _do_jp y | Lean.Expr.const (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "Bool" x_2) "false" x_3) x x_1 => do let y ← pure false _do_jp y | x => do let y ← failure _do_jp y | x => failure | x => failure

source

def Lean.PrettyPrinter.Delaborator.delabProj :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.delabProj = do let discr ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr match discr with | Lean.Expr.proj x idx x_1 x_2 => do let e ← Lean.PrettyPrinter.Delaborator.SubExpr.withProj Lean.PrettyPrinter.Delaborator.delab let idx : Lean.Syntax := Lean.Syntax.mkLit Lean.fieldIdxKind (toString (idx + 1)) let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.proj #[e, Lean.Syntax.atom info ".", idx]) | x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.Builtins" "Lean.PrettyPrinter.Delaborator.delabProj" 644 38 "unreachable code has been reached"