From ff4671cdd091da66668d20cf18b3fc829ad8bb1d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 12 Dec 2023 18:56:25 -0800 Subject: [PATCH 1/8] chore: Rename lib. commands to env. This is done to improve clarity and align with Lean's terminology --- Pantograph.lean | 8 ++++---- Pantograph/Protocol.lean | 8 ++++---- README.md | 10 +++++----- Test/Catalog.lean | 3 +-- Test/Integration.lean | 8 ++++---- 5 files changed, 18 insertions(+), 19 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index a66db35..c376999 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -33,8 +33,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | "reset" => run reset | "stat" => run stat | "expr.echo" => run expr_echo - | "lib.catalog" => run lib_catalog - | "lib.inspect" => run lib_inspect + | "env.catalog" => run env_catalog + | "env.inspect" => run env_inspect | "options.set" => run options_set | "options.print" => run options_print | "goal.start" => run goal_start @@ -60,14 +60,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let state ← get let nGoals := state.goalStates.size 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 names := env.constants.fold (init := #[]) (λ acc name info => match to_filtered_symbol name info with | .some x => acc.push x | .none => acc) 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 env ← Lean.MonadEnv.getEnv let name := args.name.toName diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index a88a54a..b544881 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -102,13 +102,13 @@ structure ExprEchoResult where deriving Lean.ToJson -- Print all symbols in environment -structure LibCatalog where +structure EnvCatalog where deriving Lean.FromJson -structure LibCatalogResult where +structure EnvCatalogResult where symbols: Array String deriving Lean.ToJson -- Print the type of a symbol -structure LibInspect where +structure EnvInspect where name: String -- If true/false, show/hide the value expressions; By default definitions -- values are shown and theorem values are hidden. @@ -116,7 +116,7 @@ structure LibInspect where -- If true, show the type and value dependencies dependency?: Option Bool := .some false deriving Lean.FromJson -structure LibInspectResult where +structure EnvInspectResult where type: Expression value?: Option Expression := .none module?: Option String := .none diff --git a/README.md b/README.md index 2b8425c..1ca4d7b 100644 --- a/README.md +++ b/README.md @@ -42,13 +42,13 @@ also accept lean options of the form `--key=value` e.g. `--pp.raw=true`. Example: (~5k symbols) ``` $ pantograph Init -lib.catalog -lib.inspect {"name": "Nat.le_add_left"} +env.catalog +env.inspect {"name": "Nat.le_add_left"} ``` Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting) ``` $ pantograph Mathlib.Analysis.Seminorm -lib.catalog +env.catalog ``` 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. - `reset`: Delete all cached expressions and proof trees - `expr.echo {"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 -- `lib.inspect {"name": , "value": }`: Show the type and package of a +- `env.catalog`: Display a list of all safe Lean symbols in the current environment +- `env.inspect {"name": , "value": }`: Show the type and package of a given symbol; If value flag is set, the value is printed or hidden. By default only the values of definitions are printed. - `options.set { key: value, ... }`: Set one or more options (not Lean options; those diff --git a/Test/Catalog.lean b/Test/Catalog.lean index e082369..99447e7 100644 --- a/Test/Catalog.lean +++ b/Test/Catalog.lean @@ -10,8 +10,7 @@ open Lean def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do let entries: List (Name × Bool) := [ ("Nat.add_comm".toName, false), - ("Lean.Name".toName, true), - ("_private.Init.0.Lean.Name".toName, true) + ("Lean.Name".toName, true) ] let suite := entries.foldl (λ suites (symbol, target) => let constant := env.constants.find! symbol diff --git a/Test/Integration.lean b/Test/Integration.lean index 65c2da6..44faf1b 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -49,20 +49,20 @@ def test_option_modify : IO LSpec.TestSeq := let module? := Option.some "Init.Data.Nat.Basic" let options: Protocol.Options := {} subroutine_runner [ - subroutine_step "lib.inspect" + subroutine_step "env.inspect" [("name", .str "Nat.add_one")] (Lean.toJson ({ type := { pp? }, module? }: - Protocol.LibInspectResult)), + Protocol.EnvInspectResult)), subroutine_step "options.set" [("printExprAST", .bool true)] (Lean.toJson ({ }: Protocol.OptionsSetResult)), - subroutine_step "lib.inspect" + subroutine_step "env.inspect" [("name", .str "Nat.add_one")] (Lean.toJson ({ type := { pp?, sexp? }, module? }: - Protocol.LibInspectResult)), + Protocol.EnvInspectResult)), subroutine_step "options.print" [] (Lean.toJson ({ options with printExprAST := true }: From 3c96a7c0ea9cb47e6fd8b74035704b521b133f68 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 13 Dec 2023 19:35:32 -0800 Subject: [PATCH 2/8] feat: env_add command --- Pantograph.lean | 33 +++++++++++++++++++++++++++++++++ Pantograph/Protocol.lean | 8 ++++++++ 2 files changed, 41 insertions(+) diff --git a/Pantograph.lean b/Pantograph.lean index c376999..3462ccb 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -35,6 +35,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | "expr.echo" => run expr_echo | "env.catalog" => run env_catalog | "env.inspect" => run env_inspect + | "env.add" => run env_add | "options.set" => run options_set | "options.print" => run options_print | "goal.start" => run goal_start @@ -50,6 +51,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc } errorCommand := errorI "command" errorIndex := errorI "index" + errorExpr := errorI "expr" -- Command Functions reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do let state ← get @@ -91,6 +93,37 @@ def execute (command: Protocol.Command): MainM Lean.Json := do valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none, module? := module? } + env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do + let env ← Lean.MonadEnv.getEnv + let type ← match syntax_from_str env args.type with + | .ok syn => do + match ← syntax_to_expr syn with + | .error e => return .error $ errorExpr e + | .ok expr => pure expr + | .error e => return .error $ errorExpr e + let value ← match syntax_from_str env args.value with + | .ok syn => do + try + let expr ← Lean.Elab.Term.elabTerm (stx := syn) (expectedType? := .some type) + pure $ expr + catch ex => return .error $ errorExpr (← ex.toMessageData.toString) + | .error e => return .error $ errorExpr e + let constant := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx + (name := args.name.toName) + (levelParams := []) + (type := type) + (value := value) + (hints := Lean.mkReducibilityHintsRegularEx 1) + (safety := Lean.DefinitionSafety.safe) + (all := []) + let env' ← match env.addDecl constant with + | .error e => do + let options ← Lean.MonadOptions.getOptions + let errorMessage ← (e.toMessageData options).toString + return .error $ errorI "kernel" errorMessage + | .ok env' => pure env' + Lean.MonadEnv.modifyEnv (λ _ => env') + return .ok {} expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do let state ← get let env ← Lean.MonadEnv.getEnv diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index b544881..8bf754a 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -125,6 +125,14 @@ structure EnvInspectResult where typeDependency?: Option (Array String) := .none valueDependency?: Option (Array String) := .none deriving Lean.ToJson +structure EnvAdd where + name: String + type: String + value: String + isTheorem?: Bool + deriving Lean.FromJson +structure EnvAddResult where + deriving Lean.ToJson /-- Set options; See `Options` struct above for meanings -/ structure OptionsSet where From 85eb42207c4d234714e87e00de3e2cc35a103483 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 14 Dec 2023 05:52:12 -0800 Subject: [PATCH 3/8] fix: env_add monads --- Pantograph.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index bdaa57c..ad3b221 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -105,14 +105,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let env ← Lean.MonadEnv.getEnv let type ← match syntax_from_str env args.type with | .ok syn => do - match ← syntax_to_expr syn with + match ← (syntax_to_expr syn |> runTermElabM) with | .error e => return .error $ errorExpr e | .ok expr => pure expr | .error e => return .error $ errorExpr e let value ← match syntax_from_str env args.value with | .ok syn => do try - let expr ← Lean.Elab.Term.elabTerm (stx := syn) (expectedType? := .some type) + let expr ← Lean.Elab.Term.elabTerm (stx := syn) (expectedType? := .some type) |> runTermElabM pure $ expr catch ex => return .error $ errorExpr (← ex.toMessageData.toString) | .error e => return .error $ errorExpr e From a540dd4540badfbc4fe2b0441ef77b314023c3d9 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 14 Dec 2023 11:11:24 -0800 Subject: [PATCH 4/8] test: env.add --- Pantograph.lean | 40 ++++++++++++++++++++++++---------------- Test/Integration.lean | 23 ++++++++++++++++++++++- 2 files changed, 46 insertions(+), 17 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index ad3b221..aeb920e 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -103,18 +103,25 @@ def execute (command: Protocol.Command): MainM Lean.Json := do } env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do let env ← Lean.MonadEnv.getEnv - let type ← match syntax_from_str env args.type with - | .ok syn => do - match ← (syntax_to_expr syn |> runTermElabM) with - | .error e => return .error $ errorExpr e - | .ok expr => pure expr - | .error e => return .error $ errorExpr e - let value ← match syntax_from_str env args.value with - | .ok syn => do - try - let expr ← Lean.Elab.Term.elabTerm (stx := syn) (expectedType? := .some type) |> runTermElabM - pure $ expr - catch ex => return .error $ errorExpr (← ex.toMessageData.toString) + let tv?: Except String (Lean.Expr × Lean.Expr) ← runTermElabM (do + let type ← match syntax_from_str env args.type with + | .ok syn => do + match ← syntax_to_expr syn with + | .error e => return .error e + | .ok expr => pure expr + | .error e => return .error e + let value ← match syntax_from_str env args.value with + | .ok syn => do + try + let expr ← Lean.Elab.Term.elabTerm (stx := syn) (expectedType? := .some type) + let expr ← Lean.instantiateMVars expr + pure $ expr + catch ex => return .error (← ex.toMessageData.toString) + | .error e => return .error e + pure $ .ok (type, value) + ) + let (type, value) ← match tv? with + | .ok t => pure t | .error e => return .error $ errorExpr e let constant := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx (name := args.name.toName) @@ -135,9 +142,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do let state ← get let env ← Lean.MonadEnv.getEnv - match syntax_from_str env args.expr with - | .error str => return .error $ errorI "parsing" str - | .ok syn => runTermElabM do + let syn ← match syntax_from_str env args.expr with + | .error str => return .error $ errorI "parsing" str + | .ok syn => pure syn + runTermElabM (do match ← syntax_to_expr syn with | .error str => return .error $ errorI "elab" str | .ok expr => do @@ -148,7 +156,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do expr := (← serialize_expression (options := state.options) expr) } catch exception => - return .error $ errorI "typing" (← exception.toMessageData.toString) + return .error $ errorI "typing" (← exception.toMessageData.toString)) options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do let state ← get let options := state.options diff --git a/Test/Integration.lean b/Test/Integration.lean index 16eb73c..351efa3 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -112,12 +112,33 @@ def test_tactic : IO LSpec.TestSeq := Protocol.GoalTacticResult)) ] +def test_env : IO LSpec.TestSeq := + let name := "Pantograph.Mystery" + subroutine_runner [ + subroutine_step "env.add" + [ + ("name", .str name), + ("type", .str "Prop → Prop → Prop"), + ("value", .str "λ (a b: Prop) => Or a b"), + ("isTheorem", .bool false) + ] + (Lean.toJson ({}: Protocol.EnvAddResult)), + subroutine_step "env.inspect" + [("name", .str name)] + (Lean.toJson ({ + value? := .some { pp? := .some "fun a b => a ∨ b" }, + type := { pp? := .some "Prop → Prop → Prop" }, + }: + Protocol.EnvInspectResult)) + ] + def suite: IO LSpec.TestSeq := do return LSpec.group "Integration" $ (LSpec.group "Option modify" (← test_option_modify)) ++ (LSpec.group "Malformed command" (← test_malformed_command)) ++ - (LSpec.group "Tactic" (← test_tactic)) + (LSpec.group "Tactic" (← test_tactic)) ++ + (LSpec.group "Env" (← test_env)) end Pantograph.Test.Integration From aef93cf5063ed5ef9a4e599728fc8dfc8bccd533 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 15 Dec 2023 13:07:59 -0500 Subject: [PATCH 5/8] fix: Force instantiate all mvars in env.add --- Pantograph.lean | 1 + Test/Integration.lean | 22 +++++++++++++++++++--- 2 files changed, 20 insertions(+), 3 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index aeb920e..2bd066e 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -114,6 +114,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .ok syn => do try let expr ← Lean.Elab.Term.elabTerm (stx := syn) (expectedType? := .some type) + Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing let expr ← Lean.instantiateMVars expr pure $ expr catch ex => return .error (← ex.toMessageData.toString) diff --git a/Test/Integration.lean b/Test/Integration.lean index 351efa3..0a6c210 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -113,21 +113,37 @@ def test_tactic : IO LSpec.TestSeq := ] def test_env : IO LSpec.TestSeq := - let name := "Pantograph.Mystery" + let name1 := "Pantograph.mystery" + let name2 := "Pantograph.mystery2" subroutine_runner [ subroutine_step "env.add" [ - ("name", .str name), + ("name", .str name1), ("type", .str "Prop → Prop → Prop"), ("value", .str "λ (a b: Prop) => Or a b"), ("isTheorem", .bool false) ] (Lean.toJson ({}: Protocol.EnvAddResult)), subroutine_step "env.inspect" - [("name", .str name)] + [("name", .str name1)] (Lean.toJson ({ value? := .some { pp? := .some "fun a b => a ∨ b" }, type := { pp? := .some "Prop → Prop → Prop" }, + }: + Protocol.EnvInspectResult)), + subroutine_step "env.add" + [ + ("name", .str name2), + ("type", .str "Nat → Int"), + ("value", .str "λ (a: Nat) => a + 1"), + ("isTheorem", .bool false) + ] + (Lean.toJson ({}: Protocol.EnvAddResult)), + subroutine_step "env.inspect" + [("name", .str name2)] + (Lean.toJson ({ + value? := .some { pp? := .some "fun a => Int.ofNat a + 1" }, + type := { pp? := .some "Nat → Int" }, }: Protocol.EnvInspectResult)) ] From da194a1165745607468e45b9bd2c0e66d95aa7ef Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 15 Dec 2023 13:37:55 -0500 Subject: [PATCH 6/8] refactor: env. operations into its own file --- Pantograph.lean | 73 +++------------------------------ Pantograph/Environment.lean | 82 +++++++++++++++++++++++++++++++++++++ Pantograph/Protocol.lean | 3 ++ 3 files changed, 90 insertions(+), 68 deletions(-) create mode 100644 Pantograph/Environment.lean diff --git a/Pantograph.lean b/Pantograph.lean index 2bd066e..30ac0c0 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -2,6 +2,7 @@ import Pantograph.Goal import Pantograph.Protocol import Pantograph.Serial import Pantograph.Symbol +import Pantograph.Environment import Lean.Data.HashMap namespace Pantograph @@ -59,7 +60,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc } errorCommand := errorI "command" errorIndex := errorI "index" - errorExpr := errorI "expr" -- Command Functions reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do let state ← get @@ -70,76 +70,13 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let state ← get let nGoals := state.goalStates.size return .ok { nGoals } - env_catalog (_: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do - let env ← Lean.MonadEnv.getEnv - let names := env.constants.fold (init := #[]) (λ acc name info => - match to_filtered_symbol name info with - | .some x => acc.push x - | .none => acc) - return .ok { symbols := names } + env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do + Environment.catalog args env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do let state ← get - let env ← Lean.MonadEnv.getEnv - let name := args.name.toName - let info? := env.find? name - match info? with - | none => return .error $ 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 state.options info.type).run', - value? := ← value?.mapM (λ v => serialize_expression state.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? - } + Environment.inspect args state.options env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do - let env ← Lean.MonadEnv.getEnv - let tv?: Except String (Lean.Expr × Lean.Expr) ← runTermElabM (do - let type ← match syntax_from_str env args.type with - | .ok syn => do - match ← syntax_to_expr syn with - | .error e => return .error e - | .ok expr => pure expr - | .error e => return .error e - let value ← match syntax_from_str env args.value with - | .ok syn => do - try - let expr ← Lean.Elab.Term.elabTerm (stx := syn) (expectedType? := .some type) - Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing - let expr ← Lean.instantiateMVars expr - pure $ expr - catch ex => return .error (← ex.toMessageData.toString) - | .error e => return .error e - pure $ .ok (type, value) - ) - let (type, value) ← match tv? with - | .ok t => pure t - | .error e => return .error $ errorExpr e - let constant := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx - (name := args.name.toName) - (levelParams := []) - (type := type) - (value := value) - (hints := Lean.mkReducibilityHintsRegularEx 1) - (safety := Lean.DefinitionSafety.safe) - (all := []) - let env' ← match env.addDecl constant with - | .error e => do - let options ← Lean.MonadOptions.getOptions - let errorMessage ← (e.toMessageData options).toString - return .error $ errorI "kernel" errorMessage - | .ok env' => pure env' - Lean.MonadEnv.modifyEnv (λ _ => env') - return .ok {} + Environment.addDecl args expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do let state ← get let env ← Lean.MonadEnv.getEnv diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean new file mode 100644 index 0000000..e9a884e --- /dev/null +++ b/Pantograph/Environment.lean @@ -0,0 +1,82 @@ +import Pantograph.Protocol +import Pantograph.Symbol +import Pantograph.Serial +import Lean + +open Lean +open Pantograph + +namespace Pantograph.Environment + +abbrev CR α := Except Protocol.InteractionError α + +def catalog (_: Protocol.EnvCatalog): CoreM (CR Protocol.EnvCatalogResult) := do + let env ← Lean.MonadEnv.getEnv + let names := env.constants.fold (init := #[]) (λ acc name info => + match to_filtered_symbol name info with + | .some x => acc.push x + | .none => acc) + return .ok { symbols := names } +def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (CR Protocol.EnvInspectResult) := do + 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? + } +def addDecl (args: Protocol.EnvAdd): CoreM (CR Protocol.EnvAddResult) := do + let env ← Lean.MonadEnv.getEnv + let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do + let type ← match syntax_from_str env args.type with + | .ok syn => do + match ← syntax_to_expr syn with + | .error e => return .error e + | .ok expr => pure expr + | .error e => return .error e + let value ← match syntax_from_str env args.value with + | .ok syn => do + try + let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type) + Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing + let expr ← instantiateMVars expr + pure $ expr + catch ex => return .error (← ex.toMessageData.toString) + | .error e => return .error e + pure $ .ok (type, value) + let (type, value) ← match ← tvM.run' (ctx := {}) |>.run' with + | .ok t => pure t + | .error e => return .error $ Protocol.errorExpr e + let constant := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx + (name := args.name.toName) + (levelParams := []) + (type := type) + (value := value) + (hints := Lean.mkReducibilityHintsRegularEx 1) + (safety := Lean.DefinitionSafety.safe) + (all := []) + let env' ← match env.addDecl constant with + | .error e => do + let options ← Lean.MonadOptions.getOptions + let desc ← (e.toMessageData options).toString + return .error $ { error := "kernel", desc } + | .ok env' => pure env' + Lean.MonadEnv.modifyEnv (λ _ => env') + return .ok {} + +end Pantograph.Environment diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 8bf754a..c0204d0 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -79,6 +79,9 @@ structure InteractionError where desc: String deriving Lean.ToJson +def errorIndex (desc: String): InteractionError := { error := "index", desc } +def errorExpr (desc: String): InteractionError := { error := "expr", desc } + --- Individual command and return types --- From dc90b6b73e9e016144871d9619206d9ced04f636 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 15 Dec 2023 13:40:36 -0500 Subject: [PATCH 7/8] chore: Move environment functions to its own file Symbol.lean is now subsumed --- Pantograph.lean | 1 - Pantograph/Environment.lean | 24 +++++++++++++++++++++++- Pantograph/Goal.lean | 2 -- Pantograph/Symbol.lean | 29 ----------------------------- Test/Catalog.lean | 4 ++-- Test/Serial.lean | 1 - 6 files changed, 25 insertions(+), 36 deletions(-) delete mode 100644 Pantograph/Symbol.lean diff --git a/Pantograph.lean b/Pantograph.lean index 30ac0c0..9d9399d 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -1,7 +1,6 @@ import Pantograph.Goal import Pantograph.Protocol import Pantograph.Serial -import Pantograph.Symbol import Pantograph.Environment import Lean.Data.HashMap diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index e9a884e..ab4513f 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -1,5 +1,4 @@ import Pantograph.Protocol -import Pantograph.Symbol import Pantograph.Serial import Lean @@ -10,6 +9,29 @@ namespace Pantograph.Environment abbrev CR α := Except Protocol.InteractionError α +def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool := + isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ info.isUnsafe + where + isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with + | .str _ name => name == "Lean" + | _ => true + +def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String := + let pref := match info with + | .axiomInfo _ => "a" + | .defnInfo _ => "d" + | .thmInfo _ => "t" + | .opaqueInfo _ => "o" + | .quotInfo _ => "q" + | .inductInfo _ => "i" + | .ctorInfo _ => "c" + | .recInfo _ => "r" + s!"{pref}{toString n}" + +def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String := + if is_symbol_unsafe_or_internal n info + then Option.none + else Option.some <| to_compact_symbol_name n info def catalog (_: Protocol.EnvCatalog): CoreM (CR Protocol.EnvCatalogResult) := do let env ← Lean.MonadEnv.getEnv let names := env.constants.fold (init := #[]) (λ acc name info => diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 1589408..9b68319 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -1,7 +1,5 @@ import Lean -import Pantograph.Symbol - def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog := { msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false diff --git a/Pantograph/Symbol.lean b/Pantograph/Symbol.lean deleted file mode 100644 index ba80877..0000000 --- a/Pantograph/Symbol.lean +++ /dev/null @@ -1,29 +0,0 @@ -import Lean - -namespace Pantograph - -def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool := - isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ info.isUnsafe - where - isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with - | .str _ name => name == "Lean" - | _ => true - -def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String := - let pref := match info with - | .axiomInfo _ => "a" - | .defnInfo _ => "d" - | .thmInfo _ => "t" - | .opaqueInfo _ => "o" - | .quotInfo _ => "q" - | .inductInfo _ => "i" - | .ctorInfo _ => "c" - | .recInfo _ => "r" - s!"{pref}{toString n}" - -def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String := - if is_symbol_unsafe_or_internal n info - then Option.none - else Option.some <| to_compact_symbol_name n info - -end Pantograph diff --git a/Test/Catalog.lean b/Test/Catalog.lean index 44c2bf7..43becdc 100644 --- a/Test/Catalog.lean +++ b/Test/Catalog.lean @@ -1,6 +1,6 @@ import LSpec import Pantograph.Serial -import Pantograph.Symbol +import Pantograph.Environment namespace Pantograph.Test.Catalog @@ -14,7 +14,7 @@ def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do ] let suite := entries.foldl (λ suites (symbol, target) => let constant := env.constants.find! symbol - let test := LSpec.check symbol.toString ((is_symbol_unsafe_or_internal symbol constant) == target) + let test := LSpec.check symbol.toString ((Environment.is_symbol_unsafe_or_internal symbol constant) == target) LSpec.TestSeq.append suites test) LSpec.TestSeq.done return suite diff --git a/Test/Serial.lean b/Test/Serial.lean index 0730bad..e502fa8 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -1,6 +1,5 @@ import LSpec import Pantograph.Serial -import Pantograph.Symbol namespace Pantograph.Test.Serial From 1c370ef2ae3db85907f8870dd85532266ff513e9 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 26 Dec 2023 12:22:57 -0500 Subject: [PATCH 8/8] refactor: Rename Test/{Catalog,Environment} --- Test/{Catalog.lean => Environment.lean} | 6 +++--- Test/Main.lean | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) rename Test/{Catalog.lean => Environment.lean} (88%) diff --git a/Test/Catalog.lean b/Test/Environment.lean similarity index 88% rename from Test/Catalog.lean rename to Test/Environment.lean index 43becdc..3bd8448 100644 --- a/Test/Catalog.lean +++ b/Test/Environment.lean @@ -2,7 +2,7 @@ import LSpec import Pantograph.Serial import Pantograph.Environment -namespace Pantograph.Test.Catalog +namespace Pantograph.Test.Environment open Pantograph open Lean @@ -24,7 +24,7 @@ def suite: IO LSpec.TestSeq := do (opts := {}) (trustLevel := 1) - return LSpec.group "Catalog" $ + return LSpec.group "Environment" $ (LSpec.group "Symbol visibility" (← test_symbol_visibility env)) -end Pantograph.Test.Catalog +end Pantograph.Test.Environment diff --git a/Test/Main.lean b/Test/Main.lean index 5178e85..4a8ab1f 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -1,5 +1,5 @@ import LSpec -import Test.Catalog +import Test.Environment import Test.Holes import Test.Integration import Test.Proofs @@ -15,7 +15,7 @@ def main := do Integration.suite, Proofs.suite, Serial.suite, - Catalog.suite + Environment.suite ] let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done LSpec.lspecIO $ all