Pantograph/Environment.lean

@@ -43,9 +43,9 @@ 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
-  let info ← match info? with
+  match info? with
   | none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
-    | some info => pure info
+  | some info =>
     let module? := env.getModuleIdxFor? name >>=
       (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
     let value? := match args.value?, info with
@@ -53,10 +53,8 @@ def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (CR P
       | .some false, _ => .none
       | .none, .defnInfo _ => info.value?
       | .none, _ => .none
-  -- Information common to all symbols
+    return .ok {
-  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.
@@ -64,32 +62,6 @@ def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (CR P
       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

Pantograph/Protocol.lean

@@ -110,7 +110,6 @@ structure EnvCatalog where
 structure EnvCatalogResult where
   symbols: Array String
   deriving Lean.ToJson
-
 -- Print the type of a symbol
 structure EnvInspect where
   name: String
@@ -120,45 +119,15 @@ 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

Test/Environment.lean

@@ -1,18 +1,12 @@
 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),
@@ -24,56 +18,6 @@ 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 }))
@@ -81,7 +25,6 @@ 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

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