From e391cb5b64c7f343b41c3a89bb393ef1f520f40e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 24 Aug 2020 16:48:15 -0700
Subject: [PATCH] refactor: use internal exceptions instead of `OptionT`

@Kha: the motivations are

- Code is more uniform, and make sure we are using only `ReaderT` and
`StateRefT` on top of our basic monads.
- It is easier to support variants of `monadMap`. We don't need to
explain the system how these variants behave with `OptionT`.
---
 src/Lean/Delaborator.lean | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index f13e1dd589..ce344a420d 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -79,12 +79,22 @@ structure Context :=
 (defaultOptions : Options)
 (optionsPerPos  : OptionsPerPos)
 
--- Exceptions from delaborators are not expected, so use a simple `OptionT` to signal whether
+-- Exceptions from delaborators are not expected. We use an internal exception to signal whether
 -- the delaborator was able to produce a Syntax object.
-abbrev DelabM := ReaderT Context $ OptionT MetaM
+def registerDelabFailureId : IO InternalExceptionId := registerInternalExceptionId `delabFailure
+@[init registerDelabFailureId] constant delabFailureId : InternalExceptionId := arbitrary _
+
+abbrev DelabM := ReaderT Context MetaM
 abbrev Delab := DelabM Syntax
 
-instance DelabM.inhabited {α} : Inhabited (DelabM α) := ⟨failure⟩
+instance DelabM.inhabited {α} : Inhabited (DelabM α) := ⟨throw $ arbitrary _⟩
+
+@[inline] protected def orelse {α} (d₁ d₂ : DelabM α) : DelabM α := do
+catchInternalId delabFailureId d₁ (fun _ => d₂)
+protected def failure {α} : DelabM α := throw $ Exception.internal delabFailureId
+instance : Alternative DelabM :=
+{ orelse  := fun _ => Delaborator.orelse,
+  failure := fun _ => Delaborator.failure }
 
 -- Macro scopes in the delaborator output are ultimately ignored by the pretty printer,
 -- so give a trivial implementation.
@@ -465,8 +475,8 @@ end Delaborator
 /-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/
 def delab (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Syntax := do
 opts ← getOptions;
-some stx ← Delaborator.delab { expr := e, defaultOptions := opts, optionsPerPos := optionsPerPos }
-  | unreachable!;
-pure stx
+catchInternalId Delaborator.delabFailureId
+  (Delaborator.delab.run { expr := e, defaultOptions := opts, optionsPerPos := optionsPerPos })
+  (fun _ => unreachable!)
 
 end Lean