feat: elaborate #print axioms command

src/Lean/Elab/Print.lean

@@ -68,12 +68,16 @@ match env.find? id with
   printInduct id us nparams nindices t ctors u
 | none => throwUnknownId id
 
-private def printId (id : Name) : CommandElabM Unit := do
+def resolveId (id : Name) : CommandElabM (List Name) := do
 cs ← liftTermElabM none $ Term.resolveGlobalName id;
 let cs := cs.filter fun ⟨_, ps⟩ => ps.isEmpty;
 let cs := cs.map fun ⟨c, _⟩ => c;
 when cs.isEmpty $ throwUnknownId id;
-cs.forM fun c => printIdCore c
+pure cs
+
+private def printId (id : Name) : CommandElabM Unit := do
+cs ← resolveId id;
+cs.forM printIdCore
 
 @[builtinCommandElab «print»] def elabPrint : CommandElab :=
 fun stx =>
@@ -88,6 +92,48 @@ fun stx =>
   else
     throwError "invalid #print command"
 
+namespace CollectAxioms
+
+structure State :=
+(visited : NameSet := {})
+(axioms  : Array Name := #[])
+
+abbrev M := ReaderT Environment $ StateM State
+
+partial def collect : Name → M Unit
+| c => do
+  let collectExpr (e : Expr) : M Unit := e.getUsedConstants.forM collect;
+  s ← get;
+  unless (s.visited.contains c) do
+    modify fun s => { s with visited := s.visited.insert c };
+    env ← read;
+    match env.find? c with
+    | some (ConstantInfo.axiomInfo _)  => modify fun s => { s with axioms := s.axioms.push c }
+    | some (ConstantInfo.defnInfo v)   => collectExpr v.type *> collectExpr v.value
+    | some (ConstantInfo.thmInfo v)    => collectExpr v.type *> collectExpr v.value.get
+    | some (ConstantInfo.opaqueInfo v) => collectExpr v.type *> collectExpr v.value
+    | some (ConstantInfo.quotInfo _)   => pure ()
+    | some (ConstantInfo.ctorInfo v)   => collectExpr v.type
+    | some (ConstantInfo.recInfo v)    => collectExpr v.type
+    | some (ConstantInfo.inductInfo v) => collectExpr v.type *> v.ctors.forM collect
+    | none                             => pure ()
+
+end CollectAxioms
+
+private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
+env ← getEnv;
+let (_, s) := ((CollectAxioms.collect constName).run env).run {};
+if s.axioms.isEmpty then
+  logInfo ("'" ++ constName ++ "' does not depend on any axioms")
+else
+  logInfo ("'" ++ constName ++ "' depends on axioms: " ++ toString s.axioms.toList)
+
+@[builtinCommandElab «printAxioms»] def elabPrintAxioms : CommandElab :=
+fun stx => do
+  let id := (stx.getArg 2).getId;
+  cs ← resolveId id;
+  cs.forM printAxiomsOf
+
 end Command
 end Elab
 end Lean

src/Lean/Parser/Command.lean

@@ -82,7 +82,7 @@ declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «
 @[builtinCommandParser] def synth          := parser! "#synth " >> termParser
 @[builtinCommandParser] def exit           := parser! "#exit"
 @[builtinCommandParser] def print          := parser! "#print " >> (ident <|> strLit)
-@[builtinCommandParser] def printAxioms    := parser! "#print " >> "axioms " >> optional ident
+@[builtinCommandParser] def printAxioms    := parser! "#print " >> "axioms " >> ident
 @[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident
 @[builtinCommandParser] def «init_quot»    := parser! "init_quot"
 @[builtinCommandParser] def «set_option»   := parser! "set_option " >> ident >> (nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit)

src/Lean/Util/FoldConsts.lean

@@ -58,6 +58,9 @@ end FoldConstsImpl
 @[implementedBy FoldConstsImpl.foldUnsafe]
 constant foldConsts {α : Type} (e : Expr) (init : α) (f : Name → α → α) : α := init
 
+def getUsedConstants (e : Expr) : Array Name :=
+e.foldConsts #[] fun c cs => cs.push c
+
 end Expr
 
 def getMaxHeight (env : Environment) (e : Expr) : UInt32 :=

tests/lean/run/nativeReflBackdoor.lean

@@ -34,3 +34,5 @@ We managed to prove `False` using the unsound annotation `implementedBy` above.
 -/
 theorem unsound : False :=
 Bool.noConfusion trueEqFalse
+
+#print axioms unsound -- axiom 'Lean.ofReduceBool' is listed