From 44d470d63e406be5b08cdab2f206c5fac7b6cca5 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 22 May 2023 19:45:08 -0700 Subject: [PATCH] Rename ids so they are consistent --- Main.lean | 20 ++++++++++---------- Pantograph/Commands.lean | 17 +++++++++-------- README.md | 8 ++++---- 3 files changed, 23 insertions(+), 22 deletions(-) diff --git a/Main.lean b/Main.lean index f3ec8dc..ad84760 100644 --- a/Main.lean +++ b/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 diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index 353d162..a3ec9da 100644 --- a/Pantograph/Commands.lean +++ b/Pantograph/Commands.lean @@ -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 diff --git a/README.md b/README.md index 13a0f3d..263878c 100644 --- a/README.md +++ b/README.md @@ -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}