Add README and catalog functions
This commit is contained in:
parent
0b2db92b4a
commit
5a297e8fef
68
Main.lean
68
Main.lean
|
@ -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 ⟨#[]⟩
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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"]}}
|
||||
```
|
||||
|
||||
|
|
@ -16,4 +16,5 @@ lean_lib Pantograph {
|
|||
@[default_target]
|
||||
lean_exe pantograph {
|
||||
root := `Main
|
||||
supportInterpreter := true
|
||||
}
|
||||
|
|
Loading…
Reference in New Issue