feat: Print inductives, constructors, and recursors in env.inspect #43

Merged
aniva merged 2 commits from env/inspect into dev 2024-01-17 14:02:56 -08:00
4 changed files with 79 additions and 12 deletions
Showing only changes of commit 93a34f9fda - Show all commits

View File

@ -56,6 +56,7 @@ def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (CR P
-- 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.
@ -70,10 +71,23 @@ def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (CR P
all := induct.all.map (·.toString),
ctors := induct.ctors.map (·.toString),
isRec := induct.isRec,
isUnsafe := induct.isUnsafe,
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

View File

@ -127,19 +127,36 @@ structure InductInfo where
all: List String
ctors: List String
isRec: Bool := false
isUnsafe: 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
inductInfo?: Option InductInfo := .none
constructorInfo?: Option ConstructorInfo := .none
recursorInfo?: Option RecursorInfo := .none
deriving Lean.ToJson
structure EnvAdd where

View File

@ -9,6 +9,8 @@ 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
@ -22,20 +24,54 @@ 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 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 {
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,
})
return LSpec.TestSeq.append LSpec.TestSeq.done test
]
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

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