Rename ids so they are consistent
This commit is contained in:
parent
51477a4806
commit
44d470d63e
20
Main.lean
20
Main.lean
|
@ -90,7 +90,7 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
|
|||
errorIndex (s: String) := Lean.toJson ({ error := "index", desc := s }: InteractionError)
|
||||
create (args: Create): Subroutine Lean.Json := do
|
||||
let state ← get
|
||||
let id := state.environments.size
|
||||
let envId := state.environments.size
|
||||
let env ← Lean.importModules
|
||||
(imports := args.imports.map (λ str => { module := str_to_name str, runtimeOnly := false }))
|
||||
(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 =>
|
||||
acc + if is_symbol_unsafe_or_internal name info then 0 else 1)
|
||||
return Lean.toJson ({
|
||||
id := id,
|
||||
envId := envId,
|
||||
symbols := env.constants.size,
|
||||
filtered_symbols := num_filtered_symbols }: CreateResult)
|
||||
catalog (args: Catalog): Subroutine Lean.Json := do
|
||||
let state ← get
|
||||
match state.getEnv args.id with
|
||||
match state.getEnv args.envId with
|
||||
| .error error => return Lean.toJson <| errorIndex error
|
||||
| .ok env =>
|
||||
let names := env.constants.fold (init := []) (λ es name info =>
|
||||
match to_filtered_symbol name info with
|
||||
| .some x => x::es
|
||||
| .none => es)
|
||||
return Lean.toJson <| ({ theorems := names }: CatalogResult)
|
||||
return Lean.toJson <| ({ symbols := names }: CatalogResult)
|
||||
clear: Subroutine Lean.Json := do
|
||||
let state ← get
|
||||
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
|
||||
let context ← read
|
||||
let state ← get
|
||||
match state.getEnv args.id with
|
||||
match state.getEnv args.envId with
|
||||
| .error error => return Lean.toJson <| errorIndex error
|
||||
| .ok env =>
|
||||
let name := str_to_name args.symbol
|
||||
let name := str_to_name args.name
|
||||
let info? := env.find? name
|
||||
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 =>
|
||||
let format ← Serial.expr_to_str
|
||||
(env := env)
|
||||
|
@ -144,7 +144,7 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
|
|||
let context ← read
|
||||
let state ← get
|
||||
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
|
||||
| .ok env => pure env
|
||||
let tree := Meta.createProofTree
|
||||
|
@ -152,8 +152,6 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
|
|||
(env := env)
|
||||
(coreContext := context.coreContext)
|
||||
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 =>
|
||||
let syn ← match Serial.syntax_from_str env expr with
|
||||
| .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"
|
||||
throw <| errorIndex str
|
||||
| .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)
|
||||
let (_, tree) := ← (Meta.ProofM.start expr |>.run tree)
|
||||
return tree
|
||||
|
|
|
@ -21,17 +21,17 @@ structure Create where
|
|||
imports : List String := []
|
||||
deriving Lean.FromJson
|
||||
structure CreateResult where
|
||||
id: Nat
|
||||
envId: Nat
|
||||
symbols: Nat
|
||||
filtered_symbols: Nat
|
||||
deriving Lean.ToJson
|
||||
|
||||
-- Print all symbols in environment
|
||||
structure Catalog where
|
||||
id: Nat
|
||||
envId: Nat
|
||||
deriving Lean.FromJson
|
||||
structure CatalogResult where
|
||||
theorems: List String
|
||||
symbols: List String
|
||||
deriving Lean.ToJson
|
||||
|
||||
-- Reset the state of REPL
|
||||
|
@ -41,8 +41,8 @@ structure ClearResult where
|
|||
|
||||
-- Print the type of a symbol
|
||||
structure Inspect where
|
||||
id: Nat -- Environment id
|
||||
symbol: String
|
||||
envId: Nat -- Environment id
|
||||
name: String
|
||||
deriving Lean.FromJson
|
||||
structure InspectResult where
|
||||
type: String
|
||||
|
@ -50,7 +50,7 @@ structure InspectResult where
|
|||
deriving Lean.ToJson
|
||||
|
||||
structure ProofStart where
|
||||
id: Nat -- Environment id
|
||||
envId: Nat -- Environment id
|
||||
name: Option String -- Identifier of the proof
|
||||
-- Only one of the fields below may be populated.
|
||||
expr: Option String -- Proof expression
|
||||
|
@ -62,14 +62,15 @@ structure ProofStartResult where
|
|||
deriving Lean.ToJson
|
||||
|
||||
structure ProofTactic where
|
||||
-- Identifiers for tree, state, and goal
|
||||
treeId: Nat
|
||||
stateId: Nat
|
||||
goalId: Option Nat -- defaults to 0
|
||||
goalId: Option Nat
|
||||
tactic: String
|
||||
deriving Lean.FromJson
|
||||
structure ProofTacticResultSuccess where
|
||||
goals: Array String
|
||||
nextId?: Option Nat
|
||||
nextId?: Option Nat -- Next proof state id
|
||||
deriving Lean.ToJson
|
||||
structure ProofTacticResultFailure where
|
||||
errorMessages: Array String -- Error messages generated by tactic
|
||||
|
|
|
@ -35,20 +35,20 @@ Example: (~5k symbols)
|
|||
```
|
||||
$ lake env build/bin/Pantograph
|
||||
create {"imports": ["Init"]}
|
||||
catalog {"id": 0}
|
||||
inspect {"id": 0, "symbol": "Nat.le_add_left"}
|
||||
catalog {"envId": 0}
|
||||
inspect {"envId": 0, "name": "Nat.le_add_left"}
|
||||
```
|
||||
Example with `mathlib` (~90k symbols)
|
||||
```
|
||||
$ lake env build/bin/Pantograph
|
||||
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
|
||||
```
|
||||
$ lake env build/bin/Pantograph
|
||||
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": 1, "goalId": 0, "tactic": "assumption"}
|
||||
proof.printTree {"treeId": 0}
|
||||
|
|
Loading…
Reference in New Issue