Merge branch 'dev' into goal/diag

Pantograph/Environment.lean

@@ -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
+  let info ← match info? with
-  | none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
+    | none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
-  | some info =>
+    | some info => pure info
-    let module? := env.getModuleIdxFor? name >>=
+  let module? := env.getModuleIdxFor? name >>=
-      (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
+    (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
-    let value? := match args.value?, info with
+  let value? := match args.value?, info with
-      | .some true, _ => info.value?
+    | .some true, _ => info.value?
-      | .some false, _ => .none
+    | .some false, _ => .none
-      | .none, .defnInfo _ => info.value?
+    | .none, .defnInfo _ => info.value?
-      | .none, _ => .none
+    | .none, _ => .none
-    return .ok {
+  -- Information common to all symbols
-      type := ← (serialize_expression options info.type).run',
+  let core := {
-      value? := ← value?.mapM (λ v => serialize_expression options v |>.run'),
+    type := ← (serialize_expression options info.type).run',
-      publicName? := Lean.privateToUserName? name |>.map (·.toString),
+    isUnsafe := info.isUnsafe,
-      -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
+    value? := ← value?.mapM (λ v => serialize_expression options v |>.run'),
-      typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none,
+    publicName? := Lean.privateToUserName? name |>.map (·.toString),
-      valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none,
+    -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
-      module? := module?
+    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

Pantograph/Protocol.lean

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

Test/Environment.lean

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

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