From 39a14aee0f8cecaafb685bdb8fead68253342788 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 22 Aug 2020 13:36:15 -0700 Subject: [PATCH] refactor: move `Lean.Core.Exception` to `Lean.Exception` --- src/Lean/CoreM.lean | 17 ++--------------- src/Lean/Elab/App.lean | 2 +- src/Lean/Elab/Command.lean | 2 +- src/Lean/Exception.lean | 26 ++++++++++++++++++++++++++ src/Lean/Meta/Basic.lean | 4 ++-- src/Lean/Meta/ExprDefEq.lean | 4 ++-- src/Lean/Util/Sorry.lean | 4 ++-- 7 files changed, 36 insertions(+), 23 deletions(-) create mode 100644 src/Lean/Exception.lean diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index bac26afd9c..46716caeae 100644 --- a/src/Lean/CoreM.lean +++ b/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 diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 39072bfe49..3c4f8e24d4 100644 --- a/src/Lean/Elab/App.lean +++ b/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; diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 54f1772721..96cca11882 100644 --- a/src/Lean/Elab/Command.lean +++ b/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; diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean new file mode 100644 index 0000000000..f72f54614b --- /dev/null +++ b/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 diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 9746e47970..7f71cb88a9 100644 --- a/src/Lean/Meta/Basic.lean +++ b/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 diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index fe97980c18..194ec5b8c5 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/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; diff --git a/src/Lean/Util/Sorry.lean b/src/Lean/Util/Sorry.lean index 5ac97cd0a9..33b5208637 100644 --- a/src/Lean/Util/Sorry.lean +++ b/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