Add README and catalog functions

This commit is contained in:
Leni Aniva 2023-05-09 22:51:19 -07:00
parent f6a520c7a0
commit b5cb464694
4 changed files with 87 additions and 13 deletions

View File

@ -1,42 +1,84 @@
import Lean.Data.Json
import Pantograph.Commands
import Lean.Environment
import Pantograph.Commands
namespace Pantograph
-- Utilities
def option_expect (o: Option α) (error: String): Except String α :=
match o with
| .some value => return value
| .none => throw error
structure State where
environments: Array String
environments: Array Lean.Environment
-- State monad
abbrev T (m: Type → Type) := StateT State m
abbrev Subroutine := T (Except String) Lean.Json
abbrev Subroutine α := ExceptT String (T IO) α
def nextId (s: State): Nat := s.environments.size
structure Command where
cmd: String
payload: Lean.Json
deriving Lean.FromJson
--def create_environment (args: Create): Subroutine := do
-- let state ← get
namespace Commands
def create (args: Create): Subroutine CreateResult := do
let state ← get
let id := nextId state
let env ← Lean.importModules
(imports := args.imports.map strTransform)
(opts := {})
(trustLevel := 1)
modify fun s => { environments := s.environments.push env }
return { id := id }
where strTransform (s: String): Lean.Import :=
let li := s.split (λ c => c == '.')
let name := li.foldl (λ pre segment => Lean.Name.str pre segment) Lean.Name.anonymous
{ module := name, runtimeOnly := false }
def catalog (args: Catalog): Subroutine CatalogResult := do
let state ← get
match state.environments.get? args.id with
| .some env =>
let names := env.constants.toList.map (λ ⟨x, _⟩ => toString x)
return { theorems := names }
| .none => throw s!"Invalid environment id {args.id}"
unsafe def clear: Subroutine ClearResult := do
let state ← get
for env in state.environments do
env.freeRegions
return { n := state.environments.size }
end Commands
end Pantograph
open Pantograph
def execute (command: String): T (ExceptT String IO) Lean.Json := do
let state ← get
unsafe def execute (command: String): ExceptT String (T IO) Lean.Json := do
let obj ← Lean.Json.parse command
let command: Command ← Lean.fromJson? obj
match command.cmd with
| "create" =>
let create: Commands.Create ← Lean.fromJson? command.payload
return Lean.toJson create.imports
let args: Commands.Create ← Lean.fromJson? command.payload
let ret ← Commands.create args
return Lean.toJson ret
| "catalog" =>
let catalog: Commands.Catalog ← Lean.fromJson? command.payload
return "catalog stub"
let args: Commands.Catalog ← Lean.fromJson? command.payload
let ret ← Commands.catalog args
return Lean.toJson ret
| "clear" =>
-- Delete all the environments
let ret ← Commands.clear
return Lean.toJson ret
| cmd => throw s!"Unknown verb: {cmd}"
-- Main IO functions
unsafe def getLines : IO String := do
@ -46,13 +88,13 @@ unsafe def getLines : IO String := do
| line => pure <| line ++ (← getLines)
unsafe def loop : T IO Unit := do
let state ← get
let command ← getLines
if command == "" then return ()
let ret ← execute command
match ret with
| .error e => IO.println s!"Could not parse json: {e}"
| .error e => IO.println s!"Error: {e}"
| .ok obj => IO.println <| toString <| obj
loop
unsafe def main : IO Unit :=
StateT.run' loop ⟨#[]⟩

View File

@ -10,4 +10,14 @@ structure Catalog where
id: Nat
deriving Lean.FromJson
structure CreateResult where
id: Nat
deriving Lean.ToJson
structure CatalogResult where
theorems: List String
deriving Lean.ToJson
structure ClearResult where
n: Nat -- Number of environments reset
deriving Lean.ToJson
end Pantograph.Commands

21
README.md Normal file
View File

@ -0,0 +1,21 @@
# Pantograph
An interaction system for Lean 4.
## Installation
Install `elan` and `lean4`. Then, execute
``` sh
lake build
```
## Usage
Before usage, put the packages that you wish the REPL to use into a directory
and build them. Put this directory into the variable `$LEAN_PATH`. Then
```
$ build/bin/Pantograph
{"cmd": "create", "payload": {"imports": ["Mathlib.Analysis.Seminorm"]}}
```

View File

@ -16,4 +16,5 @@ lean_lib Pantograph {
@[default_target]
lean_exe pantograph {
root := `Main
supportInterpreter := true
}