From c76751861aac4b4161d16d378a37222c425a3e8e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 8 Dec 2023 16:17:16 -0800 Subject: [PATCH 1/4] fix: Change the main interaction monad to MetaM --- Main.lean | 6 +----- Pantograph.lean | 18 ++++++++++++------ Test/Catalog.lean | 5 +---- Test/Integration.lean | 6 +----- 4 files changed, 15 insertions(+), 20 deletions(-) diff --git a/Main.lean b/Main.lean index 59a7e95..e833649 100644 --- a/Main.lean +++ b/Main.lean @@ -102,11 +102,7 @@ unsafe def main (args: List String): IO Unit := do options := options } try - let termElabM := loop.run context |>.run' {} - let metaM := termElabM.run' (ctx := { - declName? := some "_pantograph", - errToSorry := false - }) + let metaM := loop.run context |>.run' {} let coreM := metaM.run' IO.println "ready." discard <| coreM.toIO coreContext { env := env } diff --git a/Pantograph.lean b/Pantograph.lean index a66db35..ab6a7b1 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -16,11 +16,17 @@ structure State where goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty /-- Main state monad for executing commands -/ -abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM) +abbrev MainM := ReaderT Context (StateT State Lean.MetaM) -- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables -- certain monadic features in `MainM` abbrev CR α := Except Protocol.InteractionError α +def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α := + termElabM.run' (ctx := { + declName? := .none, + errToSorry := false, + }) + def execute (command: Protocol.Command): MainM Lean.Json := do let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := match Lean.fromJson? command.payload with @@ -97,7 +103,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match syntax_from_str env args.expr with | .error str => return .error $ errorI "parsing" str | .ok syn => do - match (← syntax_to_expr syn) with + match ← runTermElabM <| syntax_to_expr syn with | .error str => return .error $ errorI "elab" str | .ok expr => do try @@ -133,7 +139,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do (match syntax_from_str env expr with | .error str => return .error <| errorI "parsing" str | .ok syn => do - (match (← syntax_to_expr syn) with + (match ← runTermElabM <| syntax_to_expr syn with | .error str => return .error <| errorI "elab" str | .ok expr => return .ok expr)) | .none, .some copyFrom => @@ -145,7 +151,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match expr? with | .error error => return .error error | .ok expr => - let goalState ← GoalState.create expr + let goalState ← runTermElabM <| GoalState.create expr let stateId := state.nextId set { state with goalStates := state.goalStates.insert stateId goalState, @@ -159,9 +165,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 (← GoalState.execute goalState args.goalId tactic)) + pure ( Except.ok (← runTermElabM <| GoalState.execute goalState args.goalId tactic)) | .none, .some expr => do - pure ( Except.ok (← GoalState.tryAssign goalState args.goalId expr)) + pure ( Except.ok (← runTermElabM <| GoalState.tryAssign 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 diff --git a/Test/Catalog.lean b/Test/Catalog.lean index e082369..44c2bf7 100644 --- a/Test/Catalog.lean +++ b/Test/Catalog.lean @@ -10,8 +10,7 @@ open Lean def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do let entries: List (Name × Bool) := [ ("Nat.add_comm".toName, false), - ("Lean.Name".toName, true), - ("_private.Init.0.Lean.Name".toName, true) + ("Lean.Name".toName, true) ] let suite := entries.foldl (λ suites (symbol, target) => let constant := env.constants.find! symbol @@ -19,8 +18,6 @@ def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do LSpec.TestSeq.append suites test) LSpec.TestSeq.done return suite - - def suite: IO LSpec.TestSeq := do let env: Environment ← importModules (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false })) diff --git a/Test/Integration.lean b/Test/Integration.lean index 65c2da6..50ee740 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -33,11 +33,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d let result ← step return suite ++ result) LSpec.TestSeq.done try - let termElabM := commands.run context |>.run' {} - let metaM := termElabM.run' (ctx := { - declName? := some "_pantograph", - errToSorry := false - }) + let metaM := commands.run context |>.run' {} let coreM := metaM.run' return Prod.fst $ (← coreM.toIO coreContext { env := env }) catch ex => From 1fb189a38fd78e27e0a069db5829e3b6d8b22b50 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 8 Dec 2023 17:31:25 -0800 Subject: [PATCH 2/4] fix: Consolidate TermElabM blocks --- Pantograph.lean | 12 ++++++------ Pantograph/Goal.lean | 6 ++++++ Pantograph/Serial.lean | 4 ++-- 3 files changed, 14 insertions(+), 8 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index ab6a7b1..a5a181b 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -134,24 +134,23 @@ 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 _ Lean.Expr ← (match args.expr, args.copyFrom with + 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 ← runTermElabM <| syntax_to_expr syn with + (match ← syntax_to_expr syn with | .error str => return .error <| errorI "elab" str - | .ok expr => return .ok expr)) + | .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}" - | .some cInfo => return .ok cInfo.type) + | .some cInfo => return .ok (← GoalState.create cInfo.type)) | _, _ => return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied") match expr? with | .error error => return .error error - | .ok expr => - let goalState ← runTermElabM <| GoalState.create expr + | .ok goalState => let stateId := state.nextId set { state with goalStates := state.goalStates.insert stateId goalState, @@ -225,6 +224,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match state.goalStates.find? args.stateId with | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" | .some goalState => do + goalState.restoreMetaM let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr) return .ok { root?, diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 3645087..1589408 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -51,6 +51,10 @@ protected def GoalState.env (state: GoalState): Environment := state.savedState.term.meta.core.env private def GoalState.mvars (state: GoalState): SSet MVarId := state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k +private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit := + state.savedState.term.restore +def GoalState.restoreMetaM (state: GoalState): MetaM Unit := + state.savedState.term.meta.restore /-- Inner function for executing tactic on goal state -/ def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) : @@ -84,6 +88,7 @@ inductive TacticResult where /-- Execute tactic on given state -/ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String): M TacticResult := do + state.restoreElabM let goal ← match state.savedState.tactic.goals.get? goalId with | .some goal => pure $ goal | .none => return .indexError goalId @@ -118,6 +123,7 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String } protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do + state.restoreElabM let goal ← match state.savedState.tactic.goals.get? goalId with | .some goal => pure goal | .none => return .indexError goalId diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 42fc4e2..3d0d945 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -242,8 +242,8 @@ def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: Metavar of_name (n: Name) := name_to_ast n (sanitize := false) protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalState := .none) (options: Protocol.Options := {}): MetaM (Array Protocol.Goal):= do + state.restoreMetaM let goals := state.goals.toArray - state.savedState.term.meta.restore let parentDecl? := parent.bind (λ parentState => let parentGoal := parentState.goals.get! state.parentGoalId parentState.mctx.findDecl? parentGoal) @@ -256,8 +256,8 @@ protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalSt /-- Print the metavariables in a readable format -/ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do + goalState.restoreMetaM let savedState := goalState.savedState - savedState.term.meta.restore let goals := savedState.tactic.goals let mctx ← getMCtx let root := goalState.root From 45beca0bc4b9b6df45a945c9ab2504fb6332967a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 8 Dec 2023 17:32:30 -0800 Subject: [PATCH 3/4] doc: TermElabM metavariable generation --- Pantograph/Serial.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 3d0d945..072872b 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -26,6 +26,7 @@ def syntax_from_str (env: Environment) (s: String): Except String Syntax := (fileName := "") +/-- Parse a syntax object. May generate additional metavariables! -/ def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do try let expr ← Elab.Term.elabType syn From ab1b309c7267e6557ce319311f62c71e6d89bf70 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 12 Dec 2023 18:39:02 -0800 Subject: [PATCH 4/4] feat: Use CoreM as the main interaction monad --- Main.lean | 3 +-- Pantograph.lean | 22 ++++++++++++---------- Test/Integration.lean | 3 +-- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/Main.lean b/Main.lean index e833649..68d1a3e 100644 --- a/Main.lean +++ b/Main.lean @@ -102,8 +102,7 @@ unsafe def main (args: List String): IO Unit := do options := options } try - let metaM := loop.run context |>.run' {} - let coreM := metaM.run' + let coreM := loop.run context |>.run' {} IO.println "ready." discard <| coreM.toIO coreContext { env := env } catch ex => diff --git a/Pantograph.lean b/Pantograph.lean index a5a181b..1e3dbe3 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -16,16 +16,18 @@ structure State where goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty /-- Main state monad for executing commands -/ -abbrev MainM := ReaderT Context (StateT State Lean.MetaM) +abbrev MainM := ReaderT Context (StateT State Lean.CoreM) -- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables -- certain monadic features in `MainM` abbrev CR α := Except Protocol.InteractionError α -def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α := +def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α := + metaM.run' +def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α := termElabM.run' (ctx := { declName? := .none, errToSorry := false, - }) + }) |>.run' def execute (command: Protocol.Command): MainM Lean.Json := do let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := @@ -89,8 +91,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .none, .defnInfo _ => info.value? | .none, _ => .none return .ok { - type := ← serialize_expression state.options info.type, - value? := ← value?.mapM (λ v => serialize_expression state.options v), + type := ← (serialize_expression state.options info.type).run', + value? := ← value?.mapM (λ v => serialize_expression state.options v |>.run'), publicName? := Lean.privateToUserName? name |>.map (·.toString), -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug. typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none, @@ -102,8 +104,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let env ← Lean.MonadEnv.getEnv match syntax_from_str env args.expr with | .error str => return .error $ errorI "parsing" str - | .ok syn => do - match ← runTermElabM <| syntax_to_expr syn with + | .ok syn => runTermElabM do + match ← syntax_to_expr syn with | .error str => return .error $ errorI "elab" str | .ok expr => do try @@ -176,7 +178,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do goalStates := state.goalStates.insert state.nextId nextGoalState, nextId := state.nextId + 1, } - let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) + let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run' return .ok { nextStateId? := .some nextStateId, goals? := .some goals, @@ -209,7 +211,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) + let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options) |>.run' return .ok { nextStateId, goals, @@ -223,7 +225,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let state ← get match state.goalStates.find? args.stateId with | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" - | .some goalState => do + | .some goalState => runMetaM <| do goalState.restoreMetaM let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr) return .ok { diff --git a/Test/Integration.lean b/Test/Integration.lean index 50ee740..5aad1e7 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -33,8 +33,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d let result ← step return suite ++ result) LSpec.TestSeq.done try - let metaM := commands.run context |>.run' {} - let coreM := metaM.run' + let coreM := commands.run context |>.run' {} return Prod.fst $ (← coreM.toIO coreContext { env := env }) catch ex => return LSpec.check s!"Uncaught IO exception: {ex.toString}" false