feat: Add definitions and theorems to the environment #41

Merged
aniva merged 9 commits from env/add-decl into dev 2023-12-26 12:41:02 -08:00
5 changed files with 18 additions and 19 deletions
Showing only changes of commit 12544b81ee - Show all commits

View File

@ -33,8 +33,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| "reset" => run reset | "reset" => run reset
| "stat" => run stat | "stat" => run stat
| "expr.echo" => run expr_echo | "expr.echo" => run expr_echo
| "lib.catalog" => run lib_catalog | "env.catalog" => run env_catalog
| "lib.inspect" => run lib_inspect | "env.inspect" => run env_inspect
| "options.set" => run options_set | "options.set" => run options_set
| "options.print" => run options_print | "options.print" => run options_print
| "goal.start" => run goal_start | "goal.start" => run goal_start
@ -60,14 +60,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let state ← get let state ← get
let nGoals := state.goalStates.size let nGoals := state.goalStates.size
return .ok { nGoals } return .ok { nGoals }
lib_catalog (_: Protocol.LibCatalog): MainM (CR Protocol.LibCatalogResult) := do env_catalog (_: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let names := env.constants.fold (init := #[]) (λ acc name info => let names := env.constants.fold (init := #[]) (λ acc name info =>
match to_filtered_symbol name info with match to_filtered_symbol name info with
| .some x => acc.push x | .some x => acc.push x
| .none => acc) | .none => acc)
return .ok { symbols := names } return .ok { symbols := names }
lib_inspect (args: Protocol.LibInspect): MainM (CR Protocol.LibInspectResult) := do env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
let state ← get let state ← get
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let name := args.name.toName let name := args.name.toName

View File

@ -102,13 +102,13 @@ structure ExprEchoResult where
deriving Lean.ToJson deriving Lean.ToJson
-- Print all symbols in environment -- Print all symbols in environment
structure LibCatalog where structure EnvCatalog where
deriving Lean.FromJson deriving Lean.FromJson
structure LibCatalogResult where structure EnvCatalogResult where
symbols: Array String symbols: Array String
deriving Lean.ToJson deriving Lean.ToJson
-- Print the type of a symbol -- Print the type of a symbol
structure LibInspect where structure EnvInspect where
name: String name: String
-- If true/false, show/hide the value expressions; By default definitions -- If true/false, show/hide the value expressions; By default definitions
-- values are shown and theorem values are hidden. -- values are shown and theorem values are hidden.
@ -116,7 +116,7 @@ structure LibInspect where
-- If true, show the type and value dependencies -- If true, show the type and value dependencies
dependency?: Option Bool := .some false dependency?: Option Bool := .some false
deriving Lean.FromJson deriving Lean.FromJson
structure LibInspectResult where structure EnvInspectResult where
type: Expression type: Expression
value?: Option Expression := .none value?: Option Expression := .none
module?: Option String := .none module?: Option String := .none

View File

@ -42,13 +42,13 @@ also accept lean options of the form `--key=value` e.g. `--pp.raw=true`.
Example: (~5k symbols) Example: (~5k symbols)
``` ```
$ pantograph Init $ pantograph Init
lib.catalog env.catalog
lib.inspect {"name": "Nat.le_add_left"} env.inspect {"name": "Nat.le_add_left"}
``` ```
Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting) Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
``` ```
$ pantograph Mathlib.Analysis.Seminorm $ pantograph Mathlib.Analysis.Seminorm
lib.catalog env.catalog
``` ```
Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
``` ```
@ -68,8 +68,8 @@ where the application of `assumption` should lead to a failure.
See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
- `reset`: Delete all cached expressions and proof trees - `reset`: Delete all cached expressions and proof trees
- `expr.echo {"expr": <expr>}`: Determine the type of an expression and round-trip it - `expr.echo {"expr": <expr>}`: Determine the type of an expression and round-trip it
- `lib.catalog`: Display a list of all safe Lean symbols in the current context - `env.catalog`: Display a list of all safe Lean symbols in the current environment
- `lib.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a - `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
given symbol; If value flag is set, the value is printed or hidden. By default given symbol; If value flag is set, the value is printed or hidden. By default
only the values of definitions are printed. only the values of definitions are printed.
- `options.set { key: value, ... }`: Set one or more options (not Lean options; those - `options.set { key: value, ... }`: Set one or more options (not Lean options; those

View File

@ -10,8 +10,7 @@ open Lean
def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do
let entries: List (Name × Bool) := [ let entries: List (Name × Bool) := [
("Nat.add_comm".toName, false), ("Nat.add_comm".toName, false),
("Lean.Name".toName, true), ("Lean.Name".toName, true)
("_private.Init.0.Lean.Name".toName, true)
] ]
let suite := entries.foldl (λ suites (symbol, target) => let suite := entries.foldl (λ suites (symbol, target) =>
let constant := env.constants.find! symbol let constant := env.constants.find! symbol

View File

@ -49,20 +49,20 @@ def test_option_modify : IO LSpec.TestSeq :=
let module? := Option.some "Init.Data.Nat.Basic" let module? := Option.some "Init.Data.Nat.Basic"
let options: Protocol.Options := {} let options: Protocol.Options := {}
subroutine_runner [ subroutine_runner [
subroutine_step "lib.inspect" subroutine_step "env.inspect"
[("name", .str "Nat.add_one")] [("name", .str "Nat.add_one")]
(Lean.toJson ({ (Lean.toJson ({
type := { pp? }, module? }: type := { pp? }, module? }:
Protocol.LibInspectResult)), Protocol.EnvInspectResult)),
subroutine_step "options.set" subroutine_step "options.set"
[("printExprAST", .bool true)] [("printExprAST", .bool true)]
(Lean.toJson ({ }: (Lean.toJson ({ }:
Protocol.OptionsSetResult)), Protocol.OptionsSetResult)),
subroutine_step "lib.inspect" subroutine_step "env.inspect"
[("name", .str "Nat.add_one")] [("name", .str "Nat.add_one")]
(Lean.toJson ({ (Lean.toJson ({
type := { pp?, sexp? }, module? }: type := { pp?, sexp? }, module? }:
Protocol.LibInspectResult)), Protocol.EnvInspectResult)),
subroutine_step "options.print" subroutine_step "options.print"
[] []
(Lean.toJson ({ options with printExprAST := true }: (Lean.toJson ({ options with printExprAST := true }: