feat: Remove display of implementation details #50

Merged
aniva merged 5 commits from io/serial into dev 2024-03-28 22:35:38 -07:00
4 changed files with 31 additions and 28 deletions
Showing only changes of commit 35c4ea693d - Show all commits

View File

@ -7,14 +7,15 @@ open Pantograph
namespace Pantograph.Environment namespace Pantograph.Environment
def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool := def isNameInternal (n: Lean.Name): Bool :=
isLeanSymbol n (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) info.isUnsafe -- Returns true if the name is an implementation detail which should not be shown to the user.
isLeanSymbol n (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) n.isAuxLemma
where where
isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with
| .str _ name => name == "Lean" | .str _ name => name == "Lean"
| _ => true | _ => true
def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String := def toCompactSymbolName (n: Lean.Name) (info: Lean.ConstantInfo): String :=
let pref := match info with let pref := match info with
| .axiomInfo _ => "a" | .axiomInfo _ => "a"
| .defnInfo _ => "d" | .defnInfo _ => "d"
@ -26,14 +27,14 @@ def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
| .recInfo _ => "r" | .recInfo _ => "r"
s!"{pref}{toString n}" s!"{pref}{toString n}"
def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String := def toFilteredSymbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
if is_symbol_unsafe_or_internal n info if isNameInternal n || info.isUnsafe
then Option.none then Option.none
else Option.some <| to_compact_symbol_name n info else Option.some <| toCompactSymbolName n info
def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let names := env.constants.fold (init := #[]) (λ acc name info => let names := env.constants.fold (init := #[]) (λ acc name info =>
match to_filtered_symbol name info with match toFilteredSymbol name info with
| .some x => acc.push x | .some x => acc.push x
| .none => acc) | .none => acc)
return { symbols := names } return { symbols := names }
@ -58,8 +59,14 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
value? := ← value?.mapM (λ v => serialize_expression options v |>.run'), value? := ← value?.mapM (λ v => serialize_expression options v |>.run'),
publicName? := Lean.privateToUserName? name |>.map (·.toString), publicName? := Lean.privateToUserName? name |>.map (·.toString),
-- BUG: Warning: getUsedConstants here will not include projections. This is a known bug. -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none, typeDependency? := if args.dependency?.getD false
valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none, then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n)
else .none,
valueDependency? := ← if args.dependency?.getD false
then info.value?.mapM (λ e => do
let e ← (unfoldAuxLemmas e).run'
pure $ e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => name_to_ast n) )
else pure (.none),
module? := module? module? := module?
} }
let result := match info with let result := match info with

View File

@ -165,12 +165,6 @@ def goalResume (target: GoalState) (goals: Array String): Except String GoalStat
def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) := def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) :=
runMetaM <| state.serializeGoals (parent := .none) options runMetaM <| state.serializeGoals (parent := .none) options
def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
@[export pantograph_goal_print_m] @[export pantograph_goal_print_m]
def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := do def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := do
let metaM := do let metaM := do

View File

@ -6,17 +6,20 @@ import Lean
import Pantograph.Protocol import Pantograph.Protocol
import Pantograph.Goal import Pantograph.Goal
namespace Pantograph
open Lean open Lean
-- Symbol processing functions --
def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
namespace Pantograph
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
--- Input Functions --- --- Input Functions ---
/-- Read a theorem from the environment -/
def expr_from_const (env: Environment) (name: Name): Except String Lean.Expr :=
match env.find? name with
| none => throw s!"Symbol not found: {name}"
| some cInfo => return cInfo.type
/-- Read syntax object from string -/ /-- Read syntax object from string -/
def syntax_from_str (env: Environment) (s: String): Except String Syntax := def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
Parser.runParserCategory Parser.runParserCategory

View File

@ -14,14 +14,14 @@ deriving instance DecidableEq, Repr for Protocol.ConstructorInfo
deriving instance DecidableEq, Repr for Protocol.RecursorInfo deriving instance DecidableEq, Repr for Protocol.RecursorInfo
deriving instance DecidableEq, Repr for Protocol.EnvInspectResult deriving instance DecidableEq, Repr for Protocol.EnvInspectResult
def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do def test_symbol_visibility: IO LSpec.TestSeq := do
let entries: List (Name × Bool) := [ let entries: List (Name × Bool) := [
("Nat.add_comm".toName, false), ("Nat.add_comm".toName, false),
("Lean.Name".toName, true) ("Lean.Name".toName, true),
("Init.Data.Nat.Basic._auxLemma.4".toName, true),
] ]
let suite := entries.foldl (λ suites (symbol, target) => let suite := entries.foldl (λ suites (symbol, target) =>
let constant := env.constants.find! symbol let test := LSpec.check symbol.toString ((Environment.isNameInternal symbol) == target)
let test := LSpec.check symbol.toString ((Environment.is_symbol_unsafe_or_internal symbol constant) == target)
LSpec.TestSeq.append suites test) LSpec.TestSeq.done LSpec.TestSeq.append suites test) LSpec.TestSeq.done
return suite return suite
@ -78,12 +78,11 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do
def suite: IO LSpec.TestSeq := do def suite: IO LSpec.TestSeq := do
let env: Environment ← importModules let env: Environment ← importModules
(imports := #[`Init]) (imports := #[`Init])
--(imports := #["Prelude"].map (λ str => { module := str.toName, runtimeOnly := false }))
(opts := {}) (opts := {})
(trustLevel := 1) (trustLevel := 1)
return LSpec.group "Environment" $ return LSpec.group "Environment" $
(LSpec.group "Symbol visibility" (← test_symbol_visibility env)) ++ (LSpec.group "Symbol visibility" (← test_symbol_visibility)) ++
(LSpec.group "Inspect" (← test_inspect env)) (LSpec.group "Inspect" (← test_inspect env))
end Pantograph.Test.Environment end Pantograph.Test.Environment