Rename ids so they are consistent

This commit is contained in:
Leni Aniva 2023-05-22 19:45:08 -07:00
parent 1ad45f650f
commit ba779766c0
3 changed files with 23 additions and 22 deletions

View File

@ -90,7 +90,7 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
errorIndex (s: String) := Lean.toJson ({ error := "index", desc := s }: InteractionError) errorIndex (s: String) := Lean.toJson ({ error := "index", desc := s }: InteractionError)
create (args: Create): Subroutine Lean.Json := do create (args: Create): Subroutine Lean.Json := do
let state ← get let state ← get
let id := state.environments.size let envId := state.environments.size
let env ← Lean.importModules let env ← Lean.importModules
(imports := args.imports.map (λ str => { module := str_to_name str, runtimeOnly := false })) (imports := args.imports.map (λ str => { module := str_to_name str, runtimeOnly := false }))
(opts := {}) (opts := {})
@ -99,19 +99,19 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
let num_filtered_symbols := env.constants.fold (init := 0) (λ acc name info => 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) acc + if is_symbol_unsafe_or_internal name info then 0 else 1)
return Lean.toJson ({ return Lean.toJson ({
id := id, envId := envId,
symbols := env.constants.size, symbols := env.constants.size,
filtered_symbols := num_filtered_symbols }: CreateResult) filtered_symbols := num_filtered_symbols }: CreateResult)
catalog (args: Catalog): Subroutine Lean.Json := do catalog (args: Catalog): Subroutine Lean.Json := do
let state ← get let state ← get
match state.getEnv args.id with match state.getEnv args.envId with
| .error error => return Lean.toJson <| errorIndex error | .error error => return Lean.toJson <| errorIndex error
| .ok env => | .ok env =>
let names := env.constants.fold (init := []) (λ es name info => let names := env.constants.fold (init := []) (λ es name info =>
match to_filtered_symbol name info with match to_filtered_symbol name info with
| .some x => x::es | .some x => x::es
| .none => es) | .none => es)
return Lean.toJson <| ({ theorems := names }: CatalogResult) return Lean.toJson <| ({ symbols := names }: CatalogResult)
clear: Subroutine Lean.Json := do clear: Subroutine Lean.Json := do
let state ← get let state ← get
let nEnv := state.environments.size let nEnv := state.environments.size
@ -122,13 +122,13 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
inspect (args: Inspect): Subroutine Lean.Json := do inspect (args: Inspect): Subroutine Lean.Json := do
let context ← read let context ← read
let state ← get let state ← get
match state.getEnv args.id with match state.getEnv args.envId with
| .error error => return Lean.toJson <| errorIndex error | .error error => return Lean.toJson <| errorIndex error
| .ok env => | .ok env =>
let name := str_to_name args.symbol let name := str_to_name args.name
let info? := env.find? name let info? := env.find? name
match info? with match info? with
| none => return Lean.toJson <| errorIndex s!"Symbol not found {args.symbol}" | none => return Lean.toJson <| errorIndex s!"Symbol not found {args.name}"
| some info => | some info =>
let format ← Serial.expr_to_str let format ← Serial.expr_to_str
(env := env) (env := env)
@ -144,7 +144,7 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
let context ← read let context ← read
let state ← get let state ← get
let ret?: Except Lean.Json Meta.ProofTree ← ExceptT.run <| (do let ret?: Except Lean.Json Meta.ProofTree ← ExceptT.run <| (do
let env ← match state.getEnv args.id with let env ← match state.getEnv args.envId with
| .error error => throw <| Lean.toJson <| errorIndex error | .error error => throw <| Lean.toJson <| errorIndex error
| .ok env => pure env | .ok env => pure env
let tree := Meta.createProofTree let tree := Meta.createProofTree
@ -152,8 +152,6 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
(env := env) (env := env)
(coreContext := context.coreContext) (coreContext := context.coreContext)
let expr: Lean.Expr ← match args.expr, args.copyFrom with let expr: Lean.Expr ← match args.expr, args.copyFrom with
| .none, .none =>
throw <| Lean.toJson ({ error := "arguments", desc := "At least one of {expr, copyFrom} must be supplied" }: InteractionError)
| .some expr, .none => | .some expr, .none =>
let syn ← match Serial.syntax_from_str env expr with let syn ← match Serial.syntax_from_str env expr with
| .error str => throw <| Lean.toJson ({ error := "parsing", desc := str }: InteractionError) | .error str => throw <| Lean.toJson ({ error := "parsing", desc := str }: InteractionError)
@ -168,6 +166,8 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
IO.println "Symbol not found" IO.println "Symbol not found"
throw <| errorIndex str throw <| errorIndex str
| .ok expr => pure expr | .ok expr => pure expr
| .none, .none =>
throw <| Lean.toJson ({ error := "arguments", desc := "At least one of {expr, copyFrom} must be supplied" }: InteractionError)
| _, _ => throw <| Lean.toJson ({ error := "arguments", desc := "Cannot populate both of {expr, copyFrom}" }: InteractionError) | _, _ => throw <| Lean.toJson ({ error := "arguments", desc := "Cannot populate both of {expr, copyFrom}" }: InteractionError)
let (_, tree) := ← (Meta.ProofM.start expr |>.run tree) let (_, tree) := ← (Meta.ProofM.start expr |>.run tree)
return tree return tree

View File

@ -21,17 +21,17 @@ structure Create where
imports : List String := [] imports : List String := []
deriving Lean.FromJson deriving Lean.FromJson
structure CreateResult where structure CreateResult where
id: Nat envId: Nat
symbols: Nat symbols: Nat
filtered_symbols: Nat filtered_symbols: Nat
deriving Lean.ToJson deriving Lean.ToJson
-- Print all symbols in environment -- Print all symbols in environment
structure Catalog where structure Catalog where
id: Nat envId: Nat
deriving Lean.FromJson deriving Lean.FromJson
structure CatalogResult where structure CatalogResult where
theorems: List String symbols: List String
deriving Lean.ToJson deriving Lean.ToJson
-- Reset the state of REPL -- Reset the state of REPL
@ -41,8 +41,8 @@ structure ClearResult where
-- Print the type of a symbol -- Print the type of a symbol
structure Inspect where structure Inspect where
id: Nat -- Environment id envId: Nat -- Environment id
symbol: String name: String
deriving Lean.FromJson deriving Lean.FromJson
structure InspectResult where structure InspectResult where
type: String type: String
@ -50,7 +50,7 @@ structure InspectResult where
deriving Lean.ToJson deriving Lean.ToJson
structure ProofStart where structure ProofStart where
id: Nat -- Environment id envId: Nat -- Environment id
name: Option String -- Identifier of the proof name: Option String -- Identifier of the proof
-- Only one of the fields below may be populated. -- Only one of the fields below may be populated.
expr: Option String -- Proof expression expr: Option String -- Proof expression
@ -62,14 +62,15 @@ structure ProofStartResult where
deriving Lean.ToJson deriving Lean.ToJson
structure ProofTactic where structure ProofTactic where
-- Identifiers for tree, state, and goal
treeId: Nat treeId: Nat
stateId: Nat stateId: Nat
goalId: Option Nat -- defaults to 0 goalId: Option Nat
tactic: String tactic: String
deriving Lean.FromJson deriving Lean.FromJson
structure ProofTacticResultSuccess where structure ProofTacticResultSuccess where
goals: Array String goals: Array String
nextId?: Option Nat nextId?: Option Nat -- Next proof state id
deriving Lean.ToJson deriving Lean.ToJson
structure ProofTacticResultFailure where structure ProofTacticResultFailure where
errorMessages: Array String -- Error messages generated by tactic errorMessages: Array String -- Error messages generated by tactic

View File

@ -35,20 +35,20 @@ Example: (~5k symbols)
``` ```
$ lake env build/bin/Pantograph $ lake env build/bin/Pantograph
create {"imports": ["Init"]} create {"imports": ["Init"]}
catalog {"id": 0} catalog {"envId": 0}
inspect {"id": 0, "symbol": "Nat.le_add_left"} inspect {"envId": 0, "name": "Nat.le_add_left"}
``` ```
Example with `mathlib` (~90k symbols) Example with `mathlib` (~90k symbols)
``` ```
$ lake env build/bin/Pantograph $ lake env build/bin/Pantograph
create {"imports": ["Mathlib.Analysis.Seminorm"]} create {"imports": ["Mathlib.Analysis.Seminorm"]}
catalog {"id": 0} catalog {"envId": 0}
``` ```
Example proving a theorem: (alternatively use `proof.start {"id": 0, "name": "aa", "copyFrom": "Nat.add_comm", "expr": ""}`) to prime the proof Example proving a theorem: (alternatively use `proof.start {"id": 0, "name": "aa", "copyFrom": "Nat.add_comm", "expr": ""}`) to prime the proof
``` ```
$ lake env build/bin/Pantograph $ lake env build/bin/Pantograph
create {"imports": ["Init"]} create {"imports": ["Init"]}
proof.start {"id": 0, "expr": "∀ (n m : Nat), n + m = m + n"} proof.start {"envId": 0, "expr": "∀ (n m : Nat), n + m = m + n"}
proof.tactic {"treeId": 0, "stateId": 0, "goalId": 0, "tactic": "intro n m"} proof.tactic {"treeId": 0, "stateId": 0, "goalId": 0, "tactic": "intro n m"}
proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "assumption"} proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "assumption"}
proof.printTree {"treeId": 0} proof.printTree {"treeId": 0}