Pantograph/Environment.lean

@@ -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

Pantograph/Protocol.lean

@@ -127,12 +127,27 @@ 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
@@ -140,6 +155,8 @@ structure EnvInspectResult where
   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

Test/Environment.lean

@@ -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

Test/Serial.lean

@@ -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