From f42a27e0366a6f5fa858ffea1379675236494377 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 10 Mar 2024 08:13:10 -0700 Subject: [PATCH] feat(lib): Expose goal state interface --- Pantograph.lean | 24 +++++++--------- Pantograph/Library.lean | 62 +++++++++++++++++++++++++--------------- Pantograph/Protocol.lean | 2 +- Pantograph/Version.lean | 1 + 4 files changed, 52 insertions(+), 37 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index ad563f0..cc2471f 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -49,6 +49,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do errorCommand s!"Unknown command {cmd}" return Lean.toJson error where + errorCommand := errorI "command" + errorIndex := errorI "index" -- Command Functions reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do let state ← get @@ -93,14 +95,11 @@ 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 _ 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))) + 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 | .none, .some copyFrom => (match env.find? <| copyFrom.toName with | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" @@ -123,9 +122,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .some goalState => do let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with | .some tactic, .none => do - pure ( Except.ok (← runTermElabM <| GoalState.execute goalState args.goalId tactic)) + pure ( Except.ok (← goalTactic goalState args.goalId tactic)) | .none, .some expr => do - pure ( Except.ok (← runTermElabM <| GoalState.tryAssign goalState args.goalId expr)) + pure ( Except.ok (← goalTryAssign goalState args.goalId expr)) | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied") match nextGoalState? with | .error error => return .error error @@ -157,8 +156,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .none => return .error $ errorIndex s!"Invalid state index {branchId}" | .some branch => pure $ target.continue branch | .none, .some goals => - let goals := goals.map (λ name => { name := name.toName }) - pure $ target.resume goals + pure $ goalResume target goals | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied" match nextState? with | .error error => return .error <| errorI "structure" error @@ -168,7 +166,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do goalStates := state.goalStates.insert nextStateId nextGoalState, nextId := state.nextId + 1 } - let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options) |>.run' + let goals ← goalSerialize nextGoalState (options := state.options) return .ok { nextStateId, goals, diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index a8c0ce7..b1a6864 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -1,6 +1,7 @@ import Pantograph.Environment import Pantograph.Goal import Pantograph.Protocol +import Pantograph.Serial import Pantograph.Version import Lean @@ -44,11 +45,6 @@ def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α := }) |>.run' def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc } -def errorCommand := errorI "command" -def errorIndex := errorI "index" - -@[export pantograph_version] -def pantographVersion: String := version /-- Adds the given paths to Lean package search path -/ @[export pantograph_init_search] @@ -82,30 +78,27 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do /-- 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) := +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] +@[export pantograph_env_catalog_m] def envCatalog: Lean.CoreM Protocol.EnvCatalogResult := Environment.catalog ({}: Protocol.EnvCatalog) -@[export pantograph_env_inspect] -def envInspect (cc: Lean.Core.Context) (cs: Lean.Core.State) - (name: String) (value: Bool) (dependency: Bool) (options: Protocol.Options): IO (Protocol.CR Protocol.EnvInspectResult) := do - let coreM: Lean.CoreM _ := Environment.inspect ({ +@[export pantograph_env_inspect_m] +def envInspect (name: String) (value: Bool) (dependency: Bool) (options: Protocol.Options): + Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) := + Environment.inspect ({ name, value? := .some value, dependency?:= .some dependency }: Protocol.EnvInspect) options - let (result, _) ← coreM.toIO cc cs - return result -@[export pantograph_env_add] -def envAdd (cc: Lean.Core.Context) (cs: Lean.Core.State) - (name: String) (type: String) (value: String) (isTheorem: Bool): IO (Protocol.CR Protocol.EnvAddResult) := do - let coreM: Lean.CoreM _ := Environment.addDecl { name, type, value, isTheorem } - let (result, _) ← coreM.toIO cc cs - return result +@[export pantograph_env_add_m] +def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool): + Lean.CoreM (Protocol.CR Protocol.EnvAddResult) := + Environment.addDecl { name, type, value, isTheorem } -@[export pantograph_expr_parse] +@[export pantograph_expr_parse_m] def exprParse (s: String): Lean.CoreM (Protocol.CR Lean.Expr) := do let env ← Lean.MonadEnv.getEnv let syn ← match syntax_from_str env s with @@ -116,8 +109,9 @@ def exprParse (s: String): Lean.CoreM (Protocol.CR Lean.Expr) := do | .error str => return .error $ errorI "elab" str | .ok expr => return .ok expr) -@[export pantograph_expr_print] -def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do +@[export pantograph_expr_print_m] +def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options): + Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do let termElabM: Lean.Elab.TermElabM _ := try let type ← Lean.Meta.inferType expr @@ -129,8 +123,30 @@ def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options): Lean.CoreM (Proto return .error $ errorI "typing" (← exception.toMessageData.toString) runTermElabM termElabM -@[export pantograph_goal_start] +@[export pantograph_goal_start_m] def goalStart (expr: Lean.Expr): Lean.CoreM GoalState := runTermElabM (GoalState.create expr) +@[export pantograph_goal_tactic_m] +def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := + runTermElabM <| GoalState.execute state goalId tactic + +@[export pantograph_goal_try_assign_m] +def goalTryAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult := + runTermElabM <| GoalState.tryAssign state goalId expr + +@[export pantograph_goal_continue] +def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState := + target.continue branch + +@[export pantograph_goal_resume] +def goalResume (target: GoalState) (goals: Array String): Except String GoalState := + target.resume (goals.map (λ n => { name := n.toName }) |>.toList) + +@[export pantograph_goal_serialize_m] +def goalSerialize (state: GoalState) (options: Protocol.Options): Lean.CoreM (Array Protocol.Goal) := + runMetaM <| state.serializeGoals (parent := .none) options + + + end Pantograph diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 5015ad1..91c44a8 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -221,7 +221,7 @@ structure GoalContinue where -- The state which is an ancestor of `target` where goals will be extracted from branch?: Option Nat := .none -- Or, the particular goals that should be brought back into scope - goals?: Option (List String) := .none + goals?: Option (Array String) := .none deriving Lean.FromJson structure GoalContinueResult where nextStateId: Nat diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index 7bf12f9..e412ced 100644 --- a/Pantograph/Version.lean +++ b/Pantograph/Version.lean @@ -1,5 +1,6 @@ namespace Pantograph +@[export pantograph_version] def version := "0.2.12-alpha" end Pantograph