From a1421439f83300dc8c456c26b568aacc448baffd Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 16 Jan 2024 13:29:30 -0800 Subject: [PATCH 1/2] feat: Print inductives in env.inspect --- Pantograph/Environment.lean | 52 +++++++++++++++++++++++-------------- Pantograph/Protocol.lean | 14 ++++++++++ Test/Environment.lean | 23 +++++++++++++++- 3 files changed, 69 insertions(+), 20 deletions(-) diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index ab4513f..5295b6d 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -43,25 +43,39 @@ 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', + 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, + isUnsafe := induct.isUnsafe, + isReflexive := induct.isReflexive, + isNested := induct.isNested, + } } + | _ => 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 diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index c0204d0..ef463b1 100644 --- a/Pantograph/Protocol.lean +++ b/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,6 +120,17 @@ 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 + isUnsafe: Bool := false + isReflexive: Bool := false + isNested: Bool := false + deriving Lean.ToJson structure EnvInspectResult where type: Expression value?: Option Expression := .none @@ -127,7 +139,9 @@ structure EnvInspectResult where publicName?: Option String := .none typeDependency?: Option (Array String) := .none valueDependency?: Option (Array String) := .none + inductInfo?: Option InductInfo := .none deriving Lean.ToJson + structure EnvAdd where name: String type: String diff --git a/Test/Environment.lean b/Test/Environment.lean index 3bd8448..44fb8de 100644 --- a/Test/Environment.lean +++ b/Test/Environment.lean @@ -1,12 +1,16 @@ 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.EnvInspectResult + def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do let entries: List (Name × Bool) := [ ("Nat.add_comm".toName, false), @@ -18,6 +22,22 @@ def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do LSpec.TestSeq.append suites test) LSpec.TestSeq.done return suite +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 { + numParams := 2, + numIndices := 0, + all := ["Or"], + ctors := ["Or.inl", "Or.inr"], + }) + return LSpec.TestSeq.append LSpec.TestSeq.done test + runCoreMSeq env inner + def suite: IO LSpec.TestSeq := do let env: Environment ← importModules (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false })) @@ -25,6 +45,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 From 93a34f9fda9a15a3b96d2532a77f2b7f23990a7c Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 16 Jan 2024 14:11:52 -0800 Subject: [PATCH 2/2] feat: Print constructor and recursor info --- Pantograph/Environment.lean | 16 +++++++++++- Pantograph/Protocol.lean | 21 +++++++++++++-- Test/Environment.lean | 52 +++++++++++++++++++++++++++++++------ Test/Serial.lean | 2 +- 4 files changed, 79 insertions(+), 12 deletions(-) diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index 5295b6d..18e4445 100644 --- a/Pantograph/Environment.lean +++ b/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 diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index ef463b1..4277783 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -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 diff --git a/Test/Environment.lean b/Test/Environment.lean index 44fb8de..df3f3ae 100644 --- a/Test/Environment.lean +++ b/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 diff --git a/Test/Serial.lean b/Test/Serial.lean index 765b74e..70e86e8 100644 --- a/Test/Serial.lean +++ b/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