feat: Print inductives in env.inspect

This commit is contained in:
Leni Aniva 2024-01-16 13:29:30 -08:00
parent 6692303da6
commit 6fb1b2e787
3 changed files with 69 additions and 20 deletions

View File

@ -43,25 +43,39 @@ def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (CR P
let env ← Lean.MonadEnv.getEnv
let name := args.name.toName
let info? := env.find? name
match info? with
| none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
| some info =>
let module? := env.getModuleIdxFor? name >>=
(λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
let value? := match args.value?, info with
| .some true, _ => info.value?
| .some false, _ => .none
| .none, .defnInfo _ => info.value?
| .none, _ => .none
return .ok {
type := ← (serialize_expression options info.type).run',
value? := ← value?.mapM (λ v => serialize_expression options v |>.run'),
publicName? := Lean.privateToUserName? name |>.map (·.toString),
-- 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,
valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
module? := module?
}
let info ← match info? with
| none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
| some info => pure info
let module? := env.getModuleIdxFor? name >>=
(λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
let value? := match args.value?, info with
| .some true, _ => info.value?
| .some false, _ => .none
| .none, .defnInfo _ => info.value?
| .none, _ => .none
-- Information common to all symbols
let core := {
type := ← (serialize_expression options info.type).run',
value? := ← value?.mapM (λ v => serialize_expression options v |>.run'),
publicName? := Lean.privateToUserName? name |>.map (·.toString),
-- 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,
valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
module? := module?
}
let result := match info with
| .inductInfo induct => { core with inductInfo? := .some {
numParams := induct.numParams,
numIndices := induct.numIndices,
all := induct.all.map (·.toString),
ctors := induct.ctors.map (·.toString),
isRec := induct.isRec,
isUnsafe := induct.isUnsafe,
isReflexive := induct.isReflexive,
isNested := induct.isNested,
} }
| _ => core
return .ok result
def addDecl (args: Protocol.EnvAdd): CoreM (CR Protocol.EnvAddResult) := do
let env ← Lean.MonadEnv.getEnv
let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do

View File

@ -110,6 +110,7 @@ structure EnvCatalog where
structure EnvCatalogResult where
symbols: Array String
deriving Lean.ToJson
-- Print the type of a symbol
structure EnvInspect where
name: String
@ -119,6 +120,17 @@ structure EnvInspect where
-- If true, show the type and value dependencies
dependency?: Option Bool := .some false
deriving Lean.FromJson
-- See `InductiveVal`
structure InductInfo where
numParams: Nat
numIndices: Nat
all: List String
ctors: List String
isRec: Bool := false
isUnsafe: Bool := false
isReflexive: Bool := false
isNested: Bool := false
deriving Lean.ToJson
structure EnvInspectResult where
type: Expression
value?: Option Expression := .none
@ -127,7 +139,9 @@ structure EnvInspectResult where
publicName?: Option String := .none
typeDependency?: Option (Array String) := .none
valueDependency?: Option (Array String) := .none
inductInfo?: Option InductInfo := .none
deriving Lean.ToJson
structure EnvAdd where
name: String
type: String

View File

@ -1,12 +1,16 @@
import LSpec
import Pantograph.Serial
import Pantograph.Environment
import Test.Common
namespace Pantograph.Test.Environment
open Pantograph
open Lean
deriving instance DecidableEq, Repr for Protocol.InductInfo
deriving instance DecidableEq, Repr for Protocol.EnvInspectResult
def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do
let entries: List (Name × Bool) := [
("Nat.add_comm".toName, false),
@ -18,6 +22,22 @@ def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do
LSpec.TestSeq.append suites test) LSpec.TestSeq.done
return suite
def test_inspect (env: Environment): IO LSpec.TestSeq := do
let inner: CoreM LSpec.TestSeq := do
let args: Protocol.EnvInspect := { name := "Or" }
let result ← match ← Environment.inspect args (options := {}) with
| .ok result => pure $ result
| .error e => panic! s!"Error: {e.desc}"
--IO.println s!"{reprStr result.inductInfo?}"
let test := LSpec.check "Or" (result.inductInfo? == .some {
numParams := 2,
numIndices := 0,
all := ["Or"],
ctors := ["Or.inl", "Or.inr"],
})
return LSpec.TestSeq.append LSpec.TestSeq.done test
runCoreMSeq env inner
def suite: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
@ -25,6 +45,7 @@ def suite: IO LSpec.TestSeq := do
(trustLevel := 1)
return LSpec.group "Environment" $
(LSpec.group "Symbol visibility" (← test_symbol_visibility env))
(LSpec.group "Symbol visibility" (← test_symbol_visibility env)) ++
(LSpec.group "Inspect" (← test_inspect env))
end Pantograph.Test.Environment