feat: Improve #print prefix filtering. (#355)

This adds additional filtering to #print prefix including showing lemmas/definitions and
hiding internal and unstable auto-generated names.

Co-authored-by: François G. Dorais <fgdorais@gmail.com>

Std/Lean/Name.lean

@@ -11,3 +11,25 @@ def hasNum : Name → Bool
   | .anonymous => false
   | .str p _ => p.hasNum
   | .num _ _ => true
+
+/-- The frontend does not allow user declarations to start with `_` in any of its parts.
+   We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`). -/
+def isInternalOrNum : Name → Bool
+  | .str p s => s.get 0 == '_' || isInternalOrNum p
+  | .num _ _ => true
+  | _       => false
+
+/--
+Returns true if this a part of name that is internal or dynamically
+generated so that it may easily be changed.
+
+Generally, user code should not explicitly use internal names.
+-/
+def isInternalDetail : Name → Bool
+  | .str p s     =>
+    s.startsWith "_"
+      || s.startsWith "match_"
+      || s.startsWith "proof_"
+      || p.isInternalOrNum
+  | .num _ _     => true
+  | p            => p.isInternalOrNum

Std/Lean/Util/EnvSearch.lean

@@ -4,38 +4,29 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shing Tak Lam, Daniel Selsam, Mario Carneiro
 -/
 import Lean.Modifiers
+import Std.Tactic.Lint.Misc
 
 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 := {})
+    (includeImports := true)
     : m (Array ConstantInfo) := do
   let matches_ ←
-    if opts.stage1 then
+    if includeImports 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_
+  @[nolint unusedArguments]
+  check matches_ (_name : Name) cinfo := do
+    let include ← p cinfo
+    if include then
+      pure $ matches_.push cinfo
     else
       pure matches_

Std/Tactic/PrintPrefix.lean

@@ -3,37 +3,132 @@ 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.Name
 import Std.Lean.Util.EnvSearch
-import Lean.Elab.Command
+import Lean.Elab.Tactic.Config
 
 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
+Options to control `#print prefix` command and `getMatchingConstants`.
 -/
-syntax (name := printPrefix) "#print prefix " ident : command
+structure PrintPrefixConfig where
+  /-- Include declarations in imported environment. -/
+  imported : Bool := true
+  /-- Include declarations whose types are propositions. -/
+  propositions : Bool := true
+  /-- Exclude declarations whose types are not propositions. -/
+  propositionsOnly : Bool := false
+  /-- Print the type of a declaration. -/
+  showTypes : Bool := true
+  /--
+  Include internal declarations (names starting with `_`, `match_` or `proof_`)
+  -/
+  internals : Bool := false
+
+/-- Function elaborating `Config`. -/
+declare_config_elab elabPrintPrefixConfig PrintPrefixConfig
 
 /--
 The command `#print prefix foo` will print all definitions that start with
 the namespace `foo`.
+
+For example, the command below will print out definitions in the `List` namespace:
+
+```lean
+#print prefix List
+```
+
+`#print prefix` can be controlled by flags in `PrintPrefixConfig`.  These provide
+options for filtering names and formatting.   For example,
+`#print prefix` by default excludes internal names, but this can be controlled
+via config:
+```lean
+#print prefix (config:={internals:=true}) List
+```
+
+By default, `#print prefix` prints the type after each name.  This can be controlled
+by setting `showTypes` to `false`:
+```lean
+#print prefix (config:={showTypes:=false}) List
+```
+
+The complete set of flags can be seen in the documentation
+for `Lean.Elab.Command.PrintPrefixConfig`.
+-/
+syntax (name := printPrefix) "#print" "prefix" (Lean.Parser.Tactic.config)? ident : command
+
+/--
+`reverseName name` reverses the components of a name.
+-/
+private def reverseName : Name → (pre : Name := .anonymous) → Name
+| .anonymous, p => p
+| .str q s, p => reverseName q (.str p s)
+| .num q n, p => reverseName q (.num p n)
+
+/--
+`takeNameSuffix n name` returns a pair `(pre, suf)` where `suf` contains the last `n` components
+of the name and `pre` contains the rest.
+-/
+private def takeNameSuffix (cnt : Nat) (name : Name) (pre : Name := .anonymous) : Name × Name :=
+  match cnt, name with
+  | .succ cnt, .str q s => takeNameSuffix cnt q (.str pre s)
+  | .succ cnt, .num q n => takeNameSuffix cnt q (.num pre n)
+  | _, name => (name, reverseName pre)
+
+/--
+`matchName opts pre cinfo` returns true if the search options should include the constant.
+-/
+private def matchName (opts : PrintPrefixConfig)
+                      (pre : Name) (cinfo : ConstantInfo) : MetaM Bool := do
+  let name := cinfo.name
+  let preCnt := pre.getNumParts
+  let nameCnt := name.getNumParts
+  if preCnt > nameCnt then return false
+  let (root, post) := takeNameSuffix (nameCnt - preCnt) name
+  if root ≠ pre then return false
+  if !opts.internals && post.isInternalDetail then return false
+  let isProp := (Expr.isProp <$> Lean.Meta.inferType cinfo.type) <|> pure false
+  if opts.propositions then do
+    if opts.propositionsOnly && !(←isProp) then return false
+  else do
+    if opts.propositionsOnly || (←isProp) then return false
+  pure true
+
+private def lexNameLt : Name -> Name -> Bool
+| _, .anonymous => false
+| .anonymous, _ => true
+| .num p m, .num q n => m < n || m == n && lexNameLt p q
+| .num _ _, .str _ _ => true
+| .str _ _, .num _ _ => false
+| .str p m, .str q n => m < n || m == n && lexNameLt p q
+
+private def appendMatchingConstants (msg : String) (opts : PrintPrefixConfig) (pre : Name)
+     : MetaM String := do
+  let cinfos ← getMatchingConstants (matchName opts pre) opts.imported
+  let cinfos := cinfos.qsort fun p q => lexNameLt (reverseName p.name) (reverseName q.name)
+  let mut msg := msg
+  let ppInfo cinfo :=
+        if opts.showTypes then do
+          pure s!"{cinfo.name} : {← Meta.ppExpr cinfo.type}\n"
+        else
+          pure s!"{cinfo.name}\n"
+  for cinfo in cinfos do
+    msg := msg ++ (← ppInfo cinfo)
+  pure msg
+
+/--
+Implementation for #print prefix
 -/
 @[command_elab printPrefix] def elabPrintPrefix : CommandElab
-| `(#print prefix%$tk $name:ident) => do
+| `(#print prefix%$tk $[$cfg:config]? $name:ident) => do
   let nameId := name.getId
   liftTermElabM do
-    let mut msg ← appendMatchingConstants "" fun cinfo => pure $ nameId.isPrefixOf cinfo.name
+    let opts ← elabPrintPrefixConfig (mkOptionalNode cfg)
+    let mut msg ← appendMatchingConstants "" opts nameId
     if msg.isEmpty then
       if let [name] ← resolveGlobalConst name then
-        msg ← appendMatchingConstants msg fun cinfo => pure $ name.isPrefixOf cinfo.name
+        msg ← appendMatchingConstants msg opts name
     if !msg.isEmpty then
       logInfoAt tk msg
 | _ => throwUnsupportedSyntax

test/print_prefix.lean

@@ -1,6 +1,20 @@
 import Std.Tactic.PrintPrefix
 import Std.Tactic.GuardMsgs
 
+/--
+info: Empty : Type
+Empty.casesOn : (motive : Empty → Sort u) → (t : Empty) → motive t
+Empty.rec : (motive : Empty → Sort u) → (t : Empty) → motive t
+Empty.recOn : (motive : Empty → Sort u) → (t : Empty) → motive t
+-/
+#guard_msgs in
+#print prefix Empty -- Test type that probably won't change much.
+
+/--
+-/
+#guard_msgs in
+#print prefix (config:={imported:=false}) Empty
+
 namespace EmptyPrefixTest
 
 end EmptyPrefixTest
@@ -21,9 +35,6 @@ 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
@@ -35,11 +46,26 @@ structure TestStruct where
   /-- Supress lint -/
   bar : Int
 
+/--
+info: TestStruct : Type
+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.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
+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
+-/
+#guard_msgs in
+#print prefix TestStruct
 
 /--
 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
@@ -48,10 +74,94 @@ TestStruct.noConfusion : {P : Sort u} → {v1 v2 : TestStruct} → v1 = v2 → T
 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
+-/
+#guard_msgs in
+#print prefix (config:={propositions:=false}) TestStruct
+
+/--
+info: 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
+#print prefix (config:={propositionsOnly:=true}) TestStruct
+
+/--
+info: TestStruct
+TestStruct.bar
+TestStruct.casesOn
+TestStruct.foo
+TestStruct.mk
+TestStruct.mk.inj
+TestStruct.mk.injEq
+TestStruct.mk.sizeOf_spec
+TestStruct.noConfusion
+TestStruct.noConfusionType
+TestStruct.rec
+TestStruct.recOn
+-/
+#guard_msgs in
+#print prefix (config:={showTypes:=false}) TestStruct
+
+/--
+Artificial test function to show #print prefix filters out internals
+including match_/proof_.
+
+Note.  Internal names are inherently subject to change.  This test case may
+fail regularly when the Lean version is changed.  If so, we should disable
+the test case using this function below until a more robust solution is found.
+-/
+def testMatchProof : (n : Nat) → Fin n → Unit
+  | _,  ⟨0, _⟩ => ()
+  | Nat.succ as, ⟨Nat.succ i, h⟩ => testMatchProof as ⟨i, Nat.le_of_succ_le_succ h⟩
+
+/--
+info: testMatchProof : (n : Nat) → Fin n → Unit
+-/
+#guard_msgs in
+#print prefix testMatchProof
+
+/--
+info: testMatchProof : (n : Nat) → Fin n → Unit
+testMatchProof._cstage1 : (n : Nat) → Fin n → Unit
+testMatchProof._cstage2 : _obj → _obj → _obj
+testMatchProof._sunfold : (n : Nat) → Fin n → Unit
+testMatchProof._unsafe_rec : (n : Nat) → Fin n → Unit
+testMatchProof.match_1 : (motive : (x : Nat) → Fin x → Sort u_1) →
+  (x : Nat) →
+    (x_1 : Fin x) →
+      ((n : Nat) → (isLt : 0 < n) → motive n { val := 0, isLt := isLt }) →
+        ((as i : Nat) → (h : Nat.succ i < Nat.succ as) → motive (Nat.succ as) { val := Nat.succ i, isLt := h }) →
+          motive x x_1
+testMatchProof.match_1._cstage1 : (motive : (x : Nat) → Fin x → Sort u_1) →
+  (x : Nat) →
+    (x_1 : Fin x) →
+      ((n : Nat) → (isLt : 0 < n) → motive n { val := 0, isLt := isLt }) →
+        ((as i : Nat) → (h : Nat.succ i < Nat.succ as) → motive (Nat.succ as) { val := Nat.succ i, isLt := h }) →
+          motive x x_1
+testMatchProof.proof_1 : ∀ (as i : Nat), Nat.succ i < Nat.succ as → Nat.succ i ≤ as
+testMatchProof.proof_2 : ∀ (as i : Nat), Nat.succ i < Nat.succ as → Nat.succ i ≤ as
+-/
+#guard_msgs in
+#print prefix (config:={internals:=true}) testMatchProof
+
+private inductive TestInd where
+| foo : TestInd
+| bar : TestInd
+
+/--
+info: _private.test.print_prefix.0.TestInd : Type
+_private.test.print_prefix.0.TestInd.bar : TestInd
+_private.test.print_prefix.0.TestInd.bar.sizeOf_spec : sizeOf TestInd.bar = 1
+_private.test.print_prefix.0.TestInd.casesOn : {motive : TestInd → Sort u} → (t : TestInd) → motive TestInd.foo → motive TestInd.bar → motive t
+_private.test.print_prefix.0.TestInd.foo : TestInd
+_private.test.print_prefix.0.TestInd.foo.sizeOf_spec : sizeOf TestInd.foo = 1
+_private.test.print_prefix.0.TestInd.noConfusion : {P : Sort v✝} → {x y : TestInd} → x = y → TestInd.noConfusionType P x y
+_private.test.print_prefix.0.TestInd.noConfusionType : Sort v✝ → TestInd → TestInd → Sort v✝
+_private.test.print_prefix.0.TestInd.rec : {motive : TestInd → Sort u} → motive TestInd.foo → motive TestInd.bar → (t : TestInd) → motive t
+_private.test.print_prefix.0.TestInd.recOn : {motive : TestInd → Sort u} → (t : TestInd) → motive TestInd.foo → motive TestInd.bar → motive t
+_private.test.print_prefix.0.TestInd.toCtorIdx : TestInd → Nat
+-/
+#guard_msgs in
+#print prefix TestInd