Merge pull request 'feat: Print inductives, constructors, and recursors in env.inspect' (#43) from env/inspect into dev

Reviewed-on: #43
This commit is contained in:
Leni Aniva 2024-01-17 14:02:55 -08:00
commit 42c3da4a67
4 changed files with 137 additions and 21 deletions

View File

@ -43,25 +43,53 @@ 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',
isUnsafe := info.isUnsafe,
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,
isReflexive := induct.isReflexive,
isNested := induct.isNested,
} }
| .ctorInfo ctor => { core with constructorInfo? := .some {
induct := ctor.induct.toString,
cidx := ctor.cidx,
numParams := ctor.numParams,
numFields := ctor.numFields,
} }
| .recInfo r => { core with recursorInfo? := .some {
all := r.all.map (·.toString),
numParams := r.numParams,
numIndices := r.numIndices,
numMotives := r.numMotives,
numMinors := r.numMinors,
k := r.k,
} }
| _ => 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,15 +120,45 @@ 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
isReflexive: Bool := false
isNested: Bool := false
deriving Lean.ToJson
-- See `ConstructorVal`
structure ConstructorInfo where
induct: String
cidx: Nat
numParams: Nat
numFields: Nat
deriving Lean.ToJson
structure RecursorInfo where
all: List String
numParams: Nat
numIndices: Nat
numMotives: Nat
numMinors: Nat
k: Bool
deriving Lean.ToJson
structure EnvInspectResult where
type: Expression
isUnsafe: Bool := false
value?: Option Expression := .none
module?: Option String := .none
-- If the name is private, displays the public facing name
publicName?: Option String := .none
typeDependency?: Option (Array String) := .none
valueDependency?: Option (Array String) := .none
inductInfo?: Option InductInfo := .none
constructorInfo?: Option ConstructorInfo := .none
recursorInfo?: Option RecursorInfo := .none
deriving Lean.ToJson
structure EnvAdd where
name: String
type: String

View File

@ -1,12 +1,18 @@
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.ConstructorInfo
deriving instance DecidableEq, Repr for Protocol.RecursorInfo
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 +24,56 @@ def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do
LSpec.TestSeq.append suites test) LSpec.TestSeq.done
return suite
inductive ConstantCat where
| induct (info: Protocol.InductInfo)
| ctor (info: Protocol.ConstructorInfo)
| recursor (info: Protocol.RecursorInfo)
def test_inspect (env: Environment): IO LSpec.TestSeq := do
let testCases: List (String × ConstantCat) := [
("Or", ConstantCat.induct {
numParams := 2,
numIndices := 0,
all := ["Or"],
ctors := ["Or.inl", "Or.inr"],
}),
("Except.ok", ConstantCat.ctor {
induct := "Except",
cidx := 1,
numParams := 2,
numFields := 1,
}),
("Eq.rec", ConstantCat.recursor {
all := ["Eq"],
numParams := 2,
numIndices := 1,
numMotives := 1,
numMinors := 1,
k := true,
}),
("ForM.rec", ConstantCat.recursor {
all := ["ForM"],
numParams := 3,
numIndices := 0,
numMotives := 1,
numMinors := 1,
k := false,
})
]
let inner: CoreM LSpec.TestSeq := do
testCases.foldlM (λ acc (name, cat) => do
let args: Protocol.EnvInspect := { name := name }
let result ← match ← Environment.inspect args (options := {}) with
| .ok result => pure $ result
| .error e => panic! s!"Error: {e.desc}"
let p := match cat with
| .induct info => LSpec.test name (result.inductInfo? == .some info)
| .ctor info => LSpec.test name (result.constructorInfo? == .some info)
| .recursor info => LSpec.test name (result.recursorInfo? == .some info)
return LSpec.TestSeq.append acc p
) LSpec.TestSeq.done
runCoreMSeq env inner
def suite: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
@ -25,6 +81,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

View File

@ -70,7 +70,7 @@ def test_instance (env: Environment): IO LSpec.TestSeq := do
let env ← MonadEnv.getEnv
let source := "λ x y: Nat => HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) x y"
let s := syntax_from_str env source |>.toOption |>.get!
let expr := (← runTermElabMInMeta <| syntax_to_expr s) |>.toOption |>.get!
let _expr := (← runTermElabMInMeta <| syntax_to_expr s) |>.toOption |>.get!
return LSpec.TestSeq.done
runMetaMSeq env metaM