aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity

feat: Implement repl interfaces

This commit is contained in:
Leni Aniva 2025-01-15 21:23:37 -08:00
parent c9f524b9ae
commit bc4bf47c8b
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 7 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
Repl.lean
View File

@ -48,6 +48,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
| "env.describe" => run env_describe
| "env.module_read" => run env_module_read
| "env.catalog" => run env_catalog | "env.catalog" => run env_catalog
| "env.inspect" => run env_inspect | "env.inspect" => run env_inspect
| "env.add" => run env_add | "env.add" => run env_add
@ -85,6 +87,11 @@ 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 }
env_describe (args: Protocol.EnvDescribe): MainM (CR Protocol.EnvDescribeResult) := do
let result ← Environment.describe args
return .ok result
env_module_read (args: Protocol.EnvModuleRead): MainM (CR Protocol.EnvModuleReadResult) := do
Environment.moduleRead args
env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
let result ← Environment.catalog args let result ← Environment.catalog args
return .ok result return .ok result