refactor: move Lean.Core.Exception to Lean.Exception

src/Lean/CoreM.lean

@@ -8,6 +8,7 @@ import Init.Control.StateRef
 import Lean.Util.RecDepth
 import Lean.Util.Trace
 import Lean.Environment
+import Lean.Exception
 import Lean.InternalExceptionId
 import Lean.Eval
 
@@ -27,20 +28,6 @@ structure Context :=
 (maxRecDepth    : Nat := 1000)
 (ref            : Syntax := Syntax.missing)
 
-inductive Exception
-| error (ref : Syntax) (msg : MessageData)
-| internal (id : InternalExceptionId)
-
-def Exception.toMessageData : Exception → MessageData
-| Exception.error _ msg => msg
-| Exception.internal id => id.toString
-
-def Exception.getRef : Exception → Syntax
-| Exception.error ref _ => ref
-| Exception.internal _  => Syntax.missing
-
-instance Exception.inhabited : Inhabited Exception := ⟨Exception.error (arbitrary _) (arbitrary _)⟩
-
 abbrev CoreM := ReaderT Context $ StateRefT State $ EIO Exception
 
 instance CoreM.inhabited {α} : Inhabited (CoreM α) :=
@@ -188,7 +175,7 @@ instance hasEval {α} [MetaHasEval α] : MetaHasEval (CoreM α) :=
 
 end Core
 
-export Core (CoreM Exception Exception.error Exception.internal)
+export Core (CoreM)
 
 @[inline] def catchInternalId {α} {m : Type → Type} [MonadExcept Exception m] (id : InternalExceptionId) (x : m α) (h : Exception → m α) : m α :=
 catch x fun ex => match ex with

src/Lean/Elab/App.lean

@@ -362,7 +362,7 @@ match eType.getAppFn, lval with
 | _, _ =>
   throwLValError e eType "invalid field notation, type is not of the form (C ...) where C is a constant"
 
-private partial def resolveLValLoop (e : Expr) (lval : LVal) : Expr → Array Core.Exception → TermElabM LValResolution
+private partial def resolveLValLoop (e : Expr) (lval : LVal) : Expr → Array Exception → TermElabM LValResolution
 | eType, previousExceptions => do
   eType ← whnfCore eType;
   tryPostponeIfMVar eType;

src/Lean/Elab/Command.lean

@@ -65,7 +65,7 @@ let scope      := s.scopes.head!;
 def liftCoreM {α} (x : CoreM α) : CommandElabM α := do
 s ← get;
 ctx ← read;
-let Eα := Except Core.Exception α;
+let Eα := Except Exception α;
 let x : CoreM Eα := catch (do a ← x; pure $ Except.ok a) (fun ex => pure $ Except.error ex);
 let x : EIO Exception (Eα × Core.State) := (ReaderT.run x (mkCoreContext ctx s)).run { env := s.env, ngen := s.ngen };
 (ea, coreS) ← liftM x;

src/Lean/Exception.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Message
+import Lean.InternalExceptionId
+
+namespace Lean
+
+/- Exception type used in most Lean monads -/
+inductive Exception
+| error (ref : Syntax) (msg : MessageData)
+| internal (id : InternalExceptionId)
+
+def Exception.toMessageData : Exception → MessageData
+| Exception.error _ msg => msg
+| Exception.internal id => id.toString
+
+def Exception.getRef : Exception → Syntax
+| Exception.error ref _ => ref
+| Exception.internal _  => Syntax.missing
+
+instance Exception.inhabited : Inhabited Exception := ⟨Exception.error (arbitrary _) (arbitrary _)⟩
+
+end Lean

src/Lean/Meta/Basic.lean

@@ -154,10 +154,10 @@ pure $ MessageData.withContext { env := sCore.env, mctx := s.mctx, lctx := ctx.l
 def throwError {α} (msg : MessageData) : MetaM α := do
 ref ← getRef;
 msg ← addContext msg;
-throw $ Core.Exception.error ref msg
+throw $ Exception.error ref msg
 
 def throwIsDefEqStuck {α} : MetaM α :=
-throw $ Core.Exception.internal isDefEqStuckExceptionId
+throw $ Exception.internal isDefEqStuckExceptionId
 
 def checkRecDepth : MetaM Unit :=
 liftM $ Core.checkRecDepth

src/Lean/Meta/ExprDefEq.lean

@@ -371,10 +371,10 @@ structure Context :=
 abbrev CheckAssignmentM := ReaderT Context $ StateRefT State $ MetaM
 
 def throwCheckAssignmentFailure {α} : CheckAssignmentM α :=
-throw $ Core.Exception.internal checkAssignmentExceptionId
+throw $ Exception.internal checkAssignmentExceptionId
 
 def throwOutOfScopeFVar {α} : CheckAssignmentM α :=
-throw $ Core.Exception.internal outOfScopeExceptionId
+throw $ Exception.internal outOfScopeExceptionId
 
 private def findCached? (e : Expr) : CheckAssignmentM (Option Expr) := do
 s ← get;

src/Lean/Util/Sorry.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Message
-import Lean.CoreM
+import Lean.Exception
 
 namespace Lean
 
@@ -55,7 +55,7 @@ partial def MessageData.hasSyntheticSorry : MessageData → Bool
 | MessageData.node msgs         => msgs.any MessageData.hasSyntheticSorry
 | _                             => false
 
-def Core.Exception.hasSyntheticSorry : Exception → Bool
+def Exception.hasSyntheticSorry : Exception → Bool
 | Exception.error _ msg => msg.hasSyntheticSorry
 | _                     => false