2023-05-09 16:39:24 -07:00
|
|
|
|
import Lean.Data.Json
|
2023-05-09 22:51:19 -07:00
|
|
|
|
import Lean.Environment
|
2023-05-07 15:19:45 -07:00
|
|
|
|
|
2023-05-09 22:51:19 -07:00
|
|
|
|
import Pantograph.Commands
|
2023-05-12 16:12:21 -07:00
|
|
|
|
import Pantograph.Symbols
|
2023-05-09 16:39:24 -07:00
|
|
|
|
|
|
|
|
|
namespace Pantograph
|
|
|
|
|
|
2023-05-09 22:51:19 -07:00
|
|
|
|
-- Utilities
|
|
|
|
|
def option_expect (o: Option α) (error: String): Except String α :=
|
|
|
|
|
match o with
|
|
|
|
|
| .some value => return value
|
|
|
|
|
| .none => throw error
|
|
|
|
|
|
2023-05-20 13:03:12 -07:00
|
|
|
|
structure Command where
|
|
|
|
|
cmd: String
|
|
|
|
|
payload: Lean.Json
|
|
|
|
|
deriving Lean.FromJson
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
|
|
|
|
|
def parse_command (s: String): Except String Command := do
|
|
|
|
|
let s := s.trim
|
|
|
|
|
match s.get? 0 with
|
|
|
|
|
| .some '{' => -- Parse in Json mode
|
|
|
|
|
Lean.fromJson? (← Lean.Json.parse s)
|
|
|
|
|
| .some _ => -- Parse in line mode
|
|
|
|
|
let offset := s.posOf ' ' |> s.offsetOfPos
|
|
|
|
|
if offset = s.length then
|
|
|
|
|
return { cmd := s.take offset, payload := Lean.Json.null }
|
|
|
|
|
else
|
|
|
|
|
let payload ← s.drop offset |> Lean.Json.parse
|
|
|
|
|
return { cmd := s.take offset, payload := payload }
|
|
|
|
|
| .none => throw "Command is empty"
|
|
|
|
|
|
2023-05-17 21:58:03 -07:00
|
|
|
|
|
2023-05-09 16:39:24 -07:00
|
|
|
|
structure State where
|
2023-05-09 22:51:19 -07:00
|
|
|
|
environments: Array Lean.Environment
|
2023-05-09 16:39:24 -07:00
|
|
|
|
|
|
|
|
|
-- State monad
|
|
|
|
|
abbrev T (m: Type → Type) := StateT State m
|
2023-05-09 22:51:19 -07:00
|
|
|
|
abbrev Subroutine α := ExceptT String (T IO) α
|
|
|
|
|
|
|
|
|
|
def nextId (s: State): Nat := s.environments.size
|
2023-05-09 18:01:09 -07:00
|
|
|
|
|
2023-05-17 21:58:03 -07:00
|
|
|
|
open Commands
|
2023-05-09 16:39:24 -07:00
|
|
|
|
|
2023-05-09 22:51:19 -07:00
|
|
|
|
unsafe def execute (command: String): ExceptT String (T IO) Lean.Json := do
|
2023-05-20 13:03:12 -07:00
|
|
|
|
let command: Command ← parse_command command
|
2023-05-09 18:01:09 -07:00
|
|
|
|
match command.cmd with
|
|
|
|
|
| "create" =>
|
2023-05-09 22:51:19 -07:00
|
|
|
|
let args: Commands.Create ← Lean.fromJson? command.payload
|
2023-05-17 21:58:03 -07:00
|
|
|
|
let ret ← create args
|
2023-05-09 22:51:19 -07:00
|
|
|
|
return Lean.toJson ret
|
2023-05-09 18:01:09 -07:00
|
|
|
|
| "catalog" =>
|
2023-05-09 22:51:19 -07:00
|
|
|
|
let args: Commands.Catalog ← Lean.fromJson? command.payload
|
2023-05-17 21:58:03 -07:00
|
|
|
|
let ret ← catalog args
|
2023-05-09 22:51:19 -07:00
|
|
|
|
return Lean.toJson ret
|
|
|
|
|
| "clear" =>
|
|
|
|
|
-- Delete all the environments
|
2023-05-17 21:58:03 -07:00
|
|
|
|
let ret ← clear
|
|
|
|
|
return Lean.toJson ret
|
|
|
|
|
| "proof.trace" =>
|
|
|
|
|
let args: Commands.ProofTrace ← Lean.fromJson? command.payload
|
|
|
|
|
let ret ← proof_trace args
|
2023-05-09 22:51:19 -07:00
|
|
|
|
return Lean.toJson ret
|
2023-05-09 18:01:09 -07:00
|
|
|
|
| cmd => throw s!"Unknown verb: {cmd}"
|
2023-05-17 21:58:03 -07:00
|
|
|
|
where
|
|
|
|
|
create (args: Create): Subroutine CreateResult := do
|
|
|
|
|
let state ← get
|
|
|
|
|
let id := nextId state
|
|
|
|
|
let env ← Lean.importModules
|
|
|
|
|
(imports := args.imports.map (λ str => { module := strToName str, runtimeOnly := false }))
|
|
|
|
|
(opts := {})
|
|
|
|
|
(trustLevel := 1)
|
|
|
|
|
modify fun s => { environments := s.environments.push env }
|
|
|
|
|
let num_filtered_symbols := env.constants.fold (init := 0) (λ acc name info =>
|
|
|
|
|
acc + if is_symbol_unsafe_or_internal name info then 0 else 1)
|
|
|
|
|
return {
|
|
|
|
|
id := id,
|
|
|
|
|
symbols := env.constants.size,
|
|
|
|
|
filtered_symbols := num_filtered_symbols }
|
|
|
|
|
catalog (args: Catalog): Subroutine CatalogResult := do
|
|
|
|
|
let state ← get
|
|
|
|
|
match state.environments.get? args.id with
|
|
|
|
|
| .some env =>
|
|
|
|
|
let names := env.constants.fold (init := []) (λ es name info =>
|
|
|
|
|
match to_filtered_symbol name info with
|
|
|
|
|
| .some x => x::es
|
|
|
|
|
| .none => es)
|
|
|
|
|
return { theorems := names }
|
|
|
|
|
| .none => throw s!"Invalid environment id {args.id}"
|
|
|
|
|
clear: Subroutine ClearResult := do
|
|
|
|
|
let state ← get
|
|
|
|
|
for env in state.environments do
|
|
|
|
|
env.freeRegions
|
|
|
|
|
return { n := state.environments.size }
|
|
|
|
|
proof_trace (args: ProofTrace): Subroutine ProofTraceResult := do
|
|
|
|
|
-- Step 1: Create tactic state
|
|
|
|
|
-- Step 2: Execute tactic
|
|
|
|
|
-- Step 3: ??
|
|
|
|
|
return { expr := "test" }
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
end Pantograph
|
|
|
|
|
|
|
|
|
|
open Pantograph
|
|
|
|
|
|
2023-05-09 16:39:24 -07:00
|
|
|
|
|
2023-05-09 22:51:19 -07:00
|
|
|
|
|
2023-05-09 16:39:24 -07:00
|
|
|
|
-- Main IO functions
|
|
|
|
|
|
|
|
|
|
unsafe def getLines : IO String := do
|
|
|
|
|
match (← (← IO.getStdin).getLine) with
|
|
|
|
|
| "" => pure ""
|
|
|
|
|
| "\n" => pure "\n"
|
|
|
|
|
| line => pure <| line ++ (← getLines)
|
|
|
|
|
|
|
|
|
|
unsafe def loop : T IO Unit := do
|
|
|
|
|
let command ← getLines
|
|
|
|
|
if command == "" then return ()
|
2023-05-09 18:01:09 -07:00
|
|
|
|
let ret ← execute command
|
|
|
|
|
match ret with
|
2023-05-09 22:51:19 -07:00
|
|
|
|
| .error e => IO.println s!"Error: {e}"
|
2023-05-09 16:39:24 -07:00
|
|
|
|
| .ok obj => IO.println <| toString <| obj
|
2023-05-09 22:51:19 -07:00
|
|
|
|
loop
|
2023-05-09 16:39:24 -07:00
|
|
|
|
|
2023-05-12 01:08:36 -07:00
|
|
|
|
unsafe def main : IO Unit := do
|
2023-05-12 16:12:21 -07:00
|
|
|
|
Lean.enableInitializersExecution
|
2023-05-12 01:08:36 -07:00
|
|
|
|
Lean.initSearchPath (← Lean.findSysroot)
|
2023-05-09 16:39:24 -07:00
|
|
|
|
StateT.run' loop ⟨#[]⟩
|