From 02556f3c790f49f1556d8161257413f9e9e9bb21 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Sep 2024 11:56:06 -0700 Subject: [PATCH 1/4] feat: Expose `GoalState` functions --- Pantograph.lean | 2 +- Pantograph/Goal.lean | 12 +++++++----- Pantograph/Library.lean | 7 ------- 3 files changed, 8 insertions(+), 13 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 35ab117..5e96a5e 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -164,7 +164,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .some branchId, .none => do match state.goalStates.find? branchId with | .none => return .error $ errorIndex s!"Invalid state index {branchId}" - | .some branch => pure $ goalContinue target branch + | .some branch => pure $ target.continue branch | .none, .some goals => pure $ goalResume target goals | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied" diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index d92a807..408ada1 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -39,15 +39,15 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do --Elab.Term.synthesizeSyntheticMVarsNoPostponing --let expr ← instantiateMVars expr - let goal ← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous) + let root ← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous) let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState - let root := goal.mvarId! - let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root]} + let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root.mvarId!]} return { - root, + root := root.mvarId!, savedState, parentMVar? := .none, } +@[export pantograph_goal_state_is_conv] protected def GoalState.isConv (state: GoalState): Bool := state.convMVar?.isSome protected def GoalState.goals (state: GoalState): List MVarId := @@ -56,6 +56,7 @@ protected def GoalState.goals (state: GoalState): List MVarId := protected def GoalState.goalsArray (state: GoalState): Array MVarId := state.goals.toArray protected def GoalState.mctx (state: GoalState): MetavarContext := state.savedState.term.meta.meta.mctx +@[export pantograph_goal_state_env] protected def GoalState.env (state: GoalState): Environment := state.savedState.term.meta.core.env @@ -85,7 +86,7 @@ private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tac state.savedState.restore Elab.Tactic.setGoals [goal] - +@[export pantograph_goal_state_focus] protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do let goal ← state.savedState.tactic.goals.get? goalId return { @@ -121,6 +122,7 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S /-- Brings into scope all goals from `branch` -/ +@[export pantograph_goal_state_continue] protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState := if !target.goals.isEmpty then .error s!"Target state has unresolved goals" diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index c4ce4ff..2fd1972 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -134,10 +134,6 @@ def goalStartExpr (expr: String) (levels: Array String): CoreM (Protocol.CR Goal def goalResume (target: GoalState) (goals: Array String): Except String GoalState := target.resume (goals.map (λ n => { name := n.toName }) |>.toList) -@[export pantograph_goal_continue] -def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState := - target.continue branch - @[export pantograph_goal_serialize_m] def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) := runMetaM <| state.serializeGoals (parent := .none) options @@ -189,8 +185,5 @@ def goalConvExit (state: GoalState): CoreM TacticResult := @[export pantograph_goal_calc_m] def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult := runTermElabM <| state.tryCalc goalId pred -@[export pantograph_goal_focus] -def goalFocus (state: GoalState) (goalId: Nat): Option GoalState := - state.focus goalId end Pantograph -- 2.44.1 From 8394e1b4682be29ca8ff167bb3aa25314f3508e2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 7 Sep 2024 13:47:55 -0700 Subject: [PATCH 2/4] feat: Expose `conv` and `calc` tactics --- Pantograph/Goal.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 408ada1..1c2bf8d 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -235,6 +235,7 @@ protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: Str state.tryTacticM goalId $ Tactic.evalLet binderName.toName type /-- Enter conv tactic mode -/ +@[export pantograph_goal_state_conv_m] protected def GoalState.conv (state: GoalState) (goalId: Nat): Elab.TermElabM TacticResult := do if state.convMVar?.isSome then @@ -265,6 +266,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat): return .failure #[← exception.toMessageData.toString] /-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/ +@[export pantograph_goal_state_conv_exit_m] protected def GoalState.convExit (state: GoalState): Elab.TermElabM TacticResult := do let (convRhs, convGoal) ← match state.convMVar? with @@ -305,6 +307,8 @@ protected def GoalState.calcPrevRhsOf? (state: GoalState) (goalId: Nat) := state.calcPrevRhs? else .none + +@[export pantograph_goal_state_try_calc_m] protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): Elab.TermElabM TacticResult := do state.restoreElabM -- 2.44.1 From 4042ec707ee8a0eaec685c9b71812d62bc120d59 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 7 Sep 2024 13:54:52 -0700 Subject: [PATCH 3/4] refactor: Use `Meta.mapMetaM` --- Pantograph/Goal.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 1c2bf8d..0109204 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -71,10 +71,10 @@ protected def GoalState.metaState (state: GoalState): Meta.State := protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do mvarId.withContext m |>.run' (← read) state.metaState -protected def GoalState.withParentContext (state: GoalState) (m: MetaM α): MetaM α := do - state.withContext state.parentMVar?.get! m -protected def GoalState.withRootContext (state: GoalState) (m: MetaM α): MetaM α := do - state.withContext state.root m +protected def GoalState.withParentContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α := + Meta.mapMetaM <| state.withContext state.parentMVar?.get! +protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α := + Meta.mapMetaM <| state.withContext state.root private def GoalState.mvars (state: GoalState): SSet MVarId := state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k -- 2.44.1 From 7c49fcff2760e8df7dbdb1c9189a3a8c4ac872c3 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 8 Sep 2024 11:53:10 -0700 Subject: [PATCH 4/4] refactor: Un-export two field accessor functions User should use `lean_ctor_get` --- Pantograph/Goal.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 0109204..beba847 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -56,7 +56,6 @@ protected def GoalState.goals (state: GoalState): List MVarId := protected def GoalState.goalsArray (state: GoalState): Array MVarId := state.goals.toArray protected def GoalState.mctx (state: GoalState): MetavarContext := state.savedState.term.meta.meta.mctx -@[export pantograph_goal_state_env] protected def GoalState.env (state: GoalState): Environment := state.savedState.term.meta.core.env @@ -64,7 +63,6 @@ protected def GoalState.env (state: GoalState): Environment := protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): Option Meta.Context := do let mvarDecl ← state.mctx.findDecl? mvarId return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances } -@[export pantograph_goal_state_meta_state] protected def GoalState.metaState (state: GoalState): Meta.State := state.savedState.term.meta.meta -- 2.44.1