Equations
- Lean.Meta.withPPInaccessibleNamesImp flag x = withTheReader Lean.Core.Context (fun ctx => { options := Lean.Option.setIfNotSet ctx.options Lean.Meta.pp.inaccessibleNames flag, currRecDepth := ctx.currRecDepth, maxRecDepth := ctx.maxRecDepth, ref := ctx.ref, currNamespace := ctx.currNamespace, openDecls := ctx.openDecls, initHeartbeats := ctx.initHeartbeats, maxHeartbeats := ctx.maxHeartbeats }) x
def
Lean.Meta.withPPInaccessibleNames
{m : Type → Type u_1}
{α : Type}
[inst : MonadControlT Lean.MetaM m]
[inst : Monad m]
(x : m α)
(flag : optParam Bool true)
:
m α
Equations
- Lean.Meta.withPPInaccessibleNames x flag = Lean.Meta.mapMetaM (fun {α} => Lean.Meta.withPPInaccessibleNamesImp flag) x
@[inline]
Equations
- Lean.Meta.ToHide.isMarked fvarId = do let s ← get pure (Std.RBTree.contains s.hiddenInaccessible fvarId || Std.RBTree.contains s.hiddenInaccessibleProp fvarId)
Equations
- Lean.Meta.ToHide.unmark fvarId = modify fun s => { hiddenInaccessibleProp := Std.RBTree.erase s.hiddenInaccessibleProp fvarId, hiddenInaccessible := Std.RBTree.erase s.hiddenInaccessible fvarId, modified := true }
Equations
- Lean.Meta.ToHide.moveToHiddeProp fvarId = modify fun s => { hiddenInaccessibleProp := Std.RBTree.insert s.hiddenInaccessibleProp fvarId, hiddenInaccessible := Std.RBTree.erase s.hiddenInaccessible fvarId, modified := true }
Equations
- Lean.Meta.ToHide.hasVisibleDep localDecl = do let s ← get let a ← Lean.getMCtx pure (Lean.MetavarContext.findLocalDeclDependsOn a localDecl fun fvarId => !Std.RBTree.contains s.hiddenInaccessible fvarId)
Equations
- Lean.Meta.ToHide.hasInaccessibleNameDep localDecl = do let s ← get let a ← Lean.getMCtx pure (Lean.MetavarContext.findLocalDeclDependsOn a localDecl fun fvarId => Std.RBTree.contains s.hiddenInaccessible fvarId || Std.RBTree.contains s.hiddenInaccessibleProp fvarId)
Equations
- Lean.Meta.ToHide.visitVisibleExpr e = (fun visit => do let a ← liftM (Lean.Meta.instantiateMVars e) Lean.MonadCacheT.run (visit a)) Lean.Meta.ToHide.visitVisibleExpr.visit
Equations
- Lean.Meta.ToHide.fixpointStep = do let a ← read Lean.Meta.ToHide.visitVisibleExpr a.goalTarget let a ← Lean.getLCtx Lean.LocalContext.forM a fun localDecl => let fvarId := Lean.LocalDecl.fvarId localDecl; do let a ← get if Std.RBTree.contains a.hiddenInaccessible fvarId = true then do let a ← Lean.Meta.ToHide.hasVisibleDep localDecl let _do_jp : Unit → Lean.Meta.ToHide.M PUnit := fun y => do let a ← liftM (Lean.Meta.isProp (Lean.LocalDecl.type localDecl)) if a = true then do let a ← Lean.Meta.ToHide.hasInaccessibleNameDep localDecl if a = true then pure PUnit.unit else Lean.Meta.ToHide.moveToHiddeProp fvarId else pure PUnit.unit if a = true then do let y ← Lean.Meta.ToHide.unmark fvarId _do_jp y else do let y ← pure PUnit.unit _do_jp y else do Lean.Meta.ToHide.visitVisibleExpr (Lean.LocalDecl.type localDecl) match Lean.LocalDecl.value? localDecl with | some value => Lean.Meta.ToHide.visitVisibleExpr value | x => pure ()
Equations
- Lean.Meta.ToHide.collect goalTarget = do let a ← Lean.getOptions if Lean.Option.get a Lean.Meta.pp.inaccessibleNames = true then pure (∅, ∅) else do let lctx ← Lean.getLCtx let hiddenInaccessible : Lean.FVarIdSet := Lean.LocalContext.foldl lctx (fun hiddenInaccessible localDecl => Id.run (if Lean.Name.isInaccessibleUserName (Lean.LocalDecl.userName localDecl) = true then Std.RBTree.insert hiddenInaccessible (Lean.LocalDecl.fvarId localDecl) else hiddenInaccessible)) ∅ let discr ← StateRefT'.run (ReaderT.run Lean.Meta.ToHide.fixpoint { goalTarget := goalTarget }) { hiddenInaccessibleProp := ∅, hiddenInaccessible := hiddenInaccessible, modified := false } let x : Unit × Lean.Meta.ToHide.State := discr match x with | (x, s) => pure (s.hiddenInaccessible, s.hiddenInaccessibleProp)
Equations
- Lean.Meta.ppGoal mvarId = do let a ← Lean.getMCtx match Lean.MetavarContext.findDecl? a mvarId with | none => pure (Std.Format.text "unknown goal") | some mvarDecl => let indent := 2; do let a ← Lean.getOptions let ppAuxDecls : Bool := Lean.Option.get a Lean.Meta.pp.auxDecls let lctx : Lean.LocalContext := mvarDecl.lctx let a ← Lean.getOptions let lctx : Id Lean.LocalContext := StateT.run' (Lean.LocalContext.sanitizeNames lctx) { options := a, nameStem2Idx := ∅, userName2Sanitized := ∅ } Lean.Meta.withLCtx lctx mvarDecl.localInstances do let discr ← Lean.Meta.ToHide.collect mvarDecl.type let x : Lean.FVarIdSet × Lean.FVarIdSet := discr match x with | (hidden, hiddenProp) => (fun pushPending => (fun ppVars => do let discr ← Lean.LocalContext.foldlM lctx (fun x localDecl => match x with | (varNames, prevType?, fmt) => if (!ppAuxDecls && Lean.LocalDecl.isAuxDecl localDecl || Std.RBTree.contains hidden (Lean.LocalDecl.fvarId localDecl)) = true then pure (varNames, prevType?, fmt) else ppVars varNames prevType? fmt localDecl) ([], none, Lean.Format.nil) let x : List Lean.Name × Option Lean.Expr × Lean.Format := discr match x with | (varNames, type?, fmt) => do let fmt ← pushPending varNames type? fmt let fmt : Lean.Format := Lean.Meta.addLine fmt let a ← Lean.Meta.instantiateMVars mvarDecl.type let typeFmt ← Lean.Meta.ppExpr a let fmt : Lean.Format := fmt ++ Std.Format.text "⊢ " ++ Lean.Format.nest indent typeFmt match mvarDecl.userName with | Lean.Name.anonymous => pure fmt | name => pure (Std.Format.text "case " ++ Lean.format (Lean.Name.eraseMacroScopes name) ++ Lean.Format.line ++ fmt)) (Lean.Meta.ppGoal.ppVars indent hiddenProp)) (Lean.Meta.ppGoal.pushPending indent)
def
Lean.Meta.ppGoal.pushPending
(indent : Int)
(ids : List Lean.Name)
(type? : Option Lean.Expr)
(fmt : Lean.Format)
:
Equations
- Lean.Meta.ppGoal.pushPending indent ids type? fmt = if List.isEmpty ids = true then pure fmt else let fmt := Lean.Meta.addLine fmt; match type? with | none => pure fmt | some type => do let typeFmt ← Lean.Meta.ppExpr type pure (fmt ++ Lean.Format.group (Lean.Format.joinSep (List.reverse ids) (Lean.format " ") ++ Std.Format.text " :" ++ Lean.Format.nest indent (Lean.Format.line ++ typeFmt)))
def
Lean.Meta.ppGoal.ppVars
(indent : Int)
(hiddenProp : Lean.FVarIdSet)
(varNames : List Lean.Name)
(prevType? : Option Lean.Expr)
(fmt : Lean.Format)
(localDecl : Lean.LocalDecl)
:
Equations
- Lean.Meta.ppGoal.ppVars indent hiddenProp varNames prevType? fmt localDecl = if Std.RBTree.contains hiddenProp (Lean.LocalDecl.fvarId localDecl) = true then do let fmt ← Lean.Meta.ppGoal.pushPending indent varNames prevType? fmt let fmt : Lean.Format := Lean.Meta.addLine fmt let type ← Lean.Meta.instantiateMVars (Lean.LocalDecl.type localDecl) let typeFmt ← Lean.Meta.ppExpr type let fmt : Lean.Format := fmt ++ Std.Format.text " : " ++ typeFmt pure ([], none, fmt) else match localDecl with | Lean.LocalDecl.cdecl x x_1 varName type x_2 => let varName := Lean.Name.simpMacroScopes varName; do let type ← Lean.Meta.instantiateMVars type if (prevType? == none || prevType? == some type) = true then pure (varName :: varNames, some type, fmt) else do let fmt ← Lean.Meta.ppGoal.pushPending indent varNames prevType? fmt pure ([varName], some type, fmt) | Lean.LocalDecl.ldecl x x_1 varName type val x_2 => let varName := Lean.Name.simpMacroScopes varName; do let fmt ← Lean.Meta.ppGoal.pushPending indent varNames prevType? fmt let fmt : Lean.Format := Lean.Meta.addLine fmt let type ← Lean.Meta.instantiateMVars type let val ← Lean.Meta.instantiateMVars val let typeFmt ← Lean.Meta.ppExpr type let valFmt ← Lean.Meta.ppExpr val let fmt : Lean.Format := fmt ++ Lean.Format.group (Lean.format varName ++ Std.Format.text " : " ++ typeFmt ++ Std.Format.text " :=" ++ Lean.Format.nest indent (Lean.Format.line ++ valFmt)) pure ([], none, fmt)