fix: Execute expr parsing within goal.start
This commit is contained in:
parent
f42a27e036
commit
5db727e30b
|
@ -95,11 +95,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
|
||||
let state ← get
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
let expr?: Except Protocol.InteractionError GoalState ← runTermElabM (match args.expr, args.copyFrom with
|
||||
| .some expr, .none => do
|
||||
match ← exprParse expr with
|
||||
| .ok expr => return .ok (← GoalState.create expr)
|
||||
| .error e => return .error e
|
||||
let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
|
||||
| .some expr, .none =>
|
||||
(match syntax_from_str env expr with
|
||||
| .error str => return .error <| errorI "parsing" str
|
||||
| .ok syn => do
|
||||
(match ← syntax_to_expr syn with
|
||||
| .error str => return .error <| errorI "elab" str
|
||||
| .ok expr => return .ok (← GoalState.create expr)))
|
||||
| .none, .some copyFrom =>
|
||||
(match env.find? <| copyFrom.toName with
|
||||
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
|
||||
|
|
|
@ -76,12 +76,6 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
|
|||
(trustLevel := 1)
|
||||
return { env := env }
|
||||
|
||||
/-- Execute a `CoreM` monad -/
|
||||
@[export pantograph_exec_core]
|
||||
def execCore {α} (context: Lean.Core.Context) (state: Lean.Core.State) (coreM: Lean.CoreM α):
|
||||
IO (α × Lean.Core.State) :=
|
||||
coreM.toIO context state
|
||||
|
||||
@[export pantograph_env_catalog_m]
|
||||
def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
|
||||
Environment.catalog ({}: Protocol.EnvCatalog)
|
||||
|
|
Loading…
Reference in New Issue