feat: Migrate #print prefix from Mathlib (#321)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

.github/workflows/build.yml

@@ -48,4 +48,4 @@ jobs:
 
       - name: Check for long lines
         run: |
-          ! (find . -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
+          ! (find Std -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')

Std.lean

@@ -101,6 +101,7 @@ import Std.Lean.PersistentHashSet
 import Std.Lean.Position
 import Std.Lean.Tactic
 import Std.Lean.TagAttribute
+import Std.Lean.Util.EnvSearch
 import Std.Lean.Util.Path
 import Std.Linter
 import Std.Linter.UnnecessarySeqFocus
@@ -131,6 +132,7 @@ import Std.Tactic.NormCast.Ext
 import Std.Tactic.NormCast.Lemmas
 import Std.Tactic.OpenPrivate
 import Std.Tactic.PrintDependents
+import Std.Tactic.PrintPrefix
 import Std.Tactic.RCases
 import Std.Tactic.Relation.Rfl
 import Std.Tactic.Relation.Symm

Std/Lean/Util/EnvSearch.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2021 Shing Tak Lam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Shing Tak Lam, Daniel Selsam, Mario Carneiro
+-/
+import Lean.Modifiers
+
+namespace Lean
+
+/--
+Options to control `getMatchingConstants` options below.
+-/
+structure EnvironmentSearchOptions where
+  /-- Include declarations in imported environment. -/
+  stage1       : Bool := true
+  /-- Include private declarations. -/
+  checkPrivate : Bool := false
+
+/--
+Find constants in current environment that match find options and predicate.
+-/
+def getMatchingConstants {m} [Monad m] [MonadEnv m]
+    (p : ConstantInfo → m Bool)
+    (opts : EnvironmentSearchOptions := {})
+    : m (Array ConstantInfo) := do
+  let matches_ ←
+    if opts.stage1 then
+      (← getEnv).constants.map₁.foldM (init := #[]) check
+    else
+      pure #[]
+  (← getEnv).constants.map₂.foldlM (init := matches_) check
+where
+  /-- Check constant should be returned -/
+  check matches_ name cinfo := do
+    if opts.checkPrivate || !isPrivateName name then
+      if ← p cinfo then
+        pure $ matches_.push cinfo
+      else
+        pure matches_
+    else
+      pure matches_

Std/Tactic/PrintPrefix.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2021 Shing Tak Lam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Shing Tak Lam, Daniel Selsam, Mario Carneiro
+-/
+import Std.Lean.Util.EnvSearch
+import Lean.Elab.Command
+
+namespace Lean.Elab.Command
+
+private def appendMatchingConstants (msg : String)
+    (ϕ : ConstantInfo → MetaM Bool) (opts : EnvironmentSearchOptions := {}) : MetaM String := do
+  let cinfos ← getMatchingConstants ϕ opts
+  let cinfos := cinfos.qsort fun p q => p.name.lt q.name
+  let mut msg := msg
+  for cinfo in cinfos do
+    msg := msg ++ s!"{cinfo.name} : {← Meta.ppExpr cinfo.type}\n"
+  pure msg
+
+/--
+Command for #print prefix
+-/
+syntax (name := printPrefix) "#print prefix " ident : command
+
+/--
+The command `#print prefix foo` will print all definitions that start with
+the namespace `foo`.
+-/
+@[command_elab printPrefix] def elabPrintPrefix : CommandElab
+| `(#print prefix%$tk $name:ident) => do
+  let nameId := name.getId
+  liftTermElabM do
+    let mut msg ← appendMatchingConstants "" fun cinfo => pure $ nameId.isPrefixOf cinfo.name
+    if msg.isEmpty then
+      if let [name] ← resolveGlobalConst name then
+        msg ← appendMatchingConstants msg fun cinfo => pure $ name.isPrefixOf cinfo.name
+    if !msg.isEmpty then
+      logInfoAt tk msg
+| _ => throwUnsupportedSyntax

test/print_prefix.lean

@@ -0,0 +1,57 @@
+import Std.Tactic.PrintPrefix
+import Std.Tactic.GuardMsgs
+
+namespace EmptyPrefixTest
+
+end EmptyPrefixTest
+
+-- Note.  This error message could be cleaned up, but left during migration from Mathlib
+/--
+error: unknown constant 'EmptyPrefixTest'
+-/
+#guard_msgs in
+#print prefix EmptyPrefixTest
+
+namespace Prefix.Test
+
+/-- Supress lint -/
+def foo (_l:List String) : Int := 0
+
+end Prefix.Test
+
+/--
+info: Prefix.Test.foo : List String → Int
+Prefix.Test.foo._cstage1 : List String → Int
+Prefix.Test.foo._cstage2 : _obj → _obj
+Prefix.Test.foo._closed_1._cstage2 : _obj
+-/
+#guard_msgs in
+#print prefix Prefix.Test
+
+/-- Supress lint -/
+structure TestStruct where
+  /-- Supress lint -/
+  foo : Int
+  /-- Supress lint -/
+  bar : Int
+
+
+/--
+info: TestStruct : Type
+TestStruct._sizeOf_1 : TestStruct → Nat
+TestStruct._sizeOf_inst : SizeOf TestStruct
+TestStruct.bar : TestStruct → Int
+TestStruct.casesOn : {motive : TestStruct → Sort u} → (t : TestStruct) → ((foo bar : Int) → motive { foo := foo, bar := bar }) → motive t
+TestStruct.foo : TestStruct → Int
+TestStruct.mk : Int → Int → TestStruct
+TestStruct.noConfusion : {P : Sort u} → {v1 v2 : TestStruct} → v1 = v2 → TestStruct.noConfusionType P v1 v2
+TestStruct.noConfusionType : Sort u → TestStruct → TestStruct → Sort u
+TestStruct.rec : {motive : TestStruct → Sort u} → ((foo bar : Int) → motive { foo := foo, bar := bar }) → (t : TestStruct) → motive t
+TestStruct.recOn : {motive : TestStruct → Sort u} → (t : TestStruct) → ((foo bar : Int) → motive { foo := foo, bar := bar }) → motive t
+TestStruct.mk.inj : ∀ {foo bar foo_1 bar_1 : Int}, { foo := foo, bar := bar } = { foo := foo_1, bar := bar_1 } → foo = foo_1 ∧ bar = bar_1
+TestStruct.mk.injEq : ∀ (foo bar foo_1 bar_1 : Int),
+  ({ foo := foo, bar := bar } = { foo := foo_1, bar := bar_1 }) = (foo = foo_1 ∧ bar = bar_1)
+TestStruct.mk.sizeOf_spec : ∀ (foo bar : Int), sizeOf { foo := foo, bar := bar } = 1 + sizeOf foo + sizeOf bar
+-/
+#guard_msgs in
+#print prefix TestStruct