From 27b962f14d96f34f6d6e905cc8a317d73ca6c8b2 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Tue, 13 Feb 2024 15:17:19 +1100
Subject: [PATCH] chore: upstream liftCommandElabM (#3304)

These are used in the implementation of `ext`.
---
 src/Lean/Elab/Command.lean | 46 +++++++++++++++++++++++++++++++++++++-
 1 file changed, 45 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index d760d6ef30..dd72d37f8d 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -1,10 +1,11 @@
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Gabriel Ebner
 -/
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
+import Lean.Elab.SetOption
 
 namespace Lean.Elab.Command
 
@@ -503,6 +504,49 @@ def expandDeclId (declId : Syntax) (modifiers : Modifiers) : CommandElabM Expand
 
 end Elab.Command
 
+open Elab Command MonadRecDepth
+
+/--
+Lifts an action in `CommandElabM` into `CoreM`, updating the traces and the environment.
+
+Commands that modify the processing of subsequent commands,
+such as `open` and `namespace` commands,
+only have an effect for the remainder of the `CommandElabM` computation passed here,
+and do not affect subsequent commands.
+-/
+def liftCommandElabM (cmd : CommandElabM α) : CoreM α := do
+  let (a, commandState) ←
+    cmd.run {
+      fileName := ← getFileName
+      fileMap := ← getFileMap
+      ref := ← getRef
+      tacticCache? := none
+    } |>.run {
+      env := ← getEnv
+      maxRecDepth := ← getMaxRecDepth
+      scopes := [{ header := "", opts := ← getOptions }]
+    }
+  modify fun coreState => { coreState with
+    traceState.traces := coreState.traceState.traces ++ commandState.traceState.traces
+    env := commandState.env
+  }
+  if let some err := commandState.messages.msgs.toArray.find? (·.severity matches .error) then
+    throwError err.data
+  pure a
+
+/--
+Given a command elaborator `cmd`, returns a new command elaborator that
+first evaluates any local `set_option ... in ...` clauses and then invokes `cmd` on what remains.
+-/
+partial def withSetOptionIn (cmd : CommandElab) : CommandElab := fun stx => do
+  if stx.getKind == ``Lean.Parser.Command.in &&
+     stx[0].getKind == ``Lean.Parser.Command.set_option then
+      let opts ← Elab.elabSetOption stx[0][1] stx[0][2]
+      Command.withScope (fun scope => { scope with opts }) do
+        withSetOptionIn cmd stx[1]
+  else
+    cmd stx
+
 export Elab.Command (Linter addLinter)
 
 end Lean