refactor(library/init/lean/parser/parsec): make sure custom error message doesn't need to be inhabited

library/init/data/option/basic.lean

@@ -19,6 +19,10 @@ def get_or_else {α : Type u} : option α → α → α
 | (some x) _ := x
 | none     e := e
 
+def get {α : Type u} [inhabited α] : option α → α
+| (some x) := x
+| none     := default α
+
 def to_bool {α : Type u} : option α → bool
 | (some _) := tt
 | none     := ff
@@ -31,10 +35,6 @@ def is_none {α : Type u} : option α → bool
 | (some _) := ff
 | none     := tt
 
-def get {α : Type u} : Π {o : option α}, is_some o → α
-| (some x) h := x
-| none     h := false.rec _ $ bool.ff_ne_tt h
-
 @[inline] protected def bind {α : Type u} {β : Type v} : option α → (α → option β) → option β
 | none     b := none
 | (some a) b := b a

library/init/data/option/instances.lean

@@ -15,8 +15,5 @@ lemma option.eq_of_eq_some {α : Type u} : Π {x y : option α}, (∀z, x = some
 | (some z) none     h := option.no_confusion ((h z).1 rfl)
 | (some z) (some w) h := option.no_confusion ((h w).2 rfl) (congr_arg some)
 
-lemma option.eq_some_of_is_some {α : Type u} : Π {o : option α} (h : option.is_some o), o = some (option.get h)
-| (some x) h := rfl
-
 lemma option.eq_none_of_is_none {α : Type u} : Π {o : option α}, o.is_none → o = none
 | none h := rfl

library/init/lean/parser/basic.lean

@@ -123,7 +123,7 @@ m (sum α syntax × message_log) :=
 do (r, _) ← (((r.run cfg).run {messages:=message_log.empty}).parse s).run {},
 pure $ match r with
 | except.ok (a, st) := (sum.inl a, st.messages)
-| except.error msg  := (sum.inr msg.custom, message_log.empty.add (message_of_parsec_message cfg msg))
+| except.error msg  := (sum.inr msg.custom.get, message_log.empty.add (message_of_parsec_message cfg msg))
 
 open coroutine
 open monad_parsec

library/init/lean/parser/combinators.lean

@@ -24,7 +24,7 @@ do args ← rs.mfoldl (λ (p : list syntax) r, do
      args ← pure p,
      -- on error, append partial syntax tree to previous successful parses and rethrow
      a ← catch r $ λ msg,
-       let args := msg.custom :: args in
+       let args := msg.custom.get :: args in
        throw {msg with custom := syntax.node ⟨k, args.reverse⟩},
      pure (a::args)
    ) [],
@@ -46,7 +46,7 @@ private def many1_aux (p : parser) : list syntax → nat → parser
 | as (n+1) := do
   a ← catch p (λ msg, throw {msg with custom :=
     -- append `syntax.missing` to make clear that list is incomplete
-    syntax.node ⟨none, (syntax.missing::msg.custom::as).reverse⟩}),
+    syntax.node ⟨none, (syntax.missing::msg.custom.get::as).reverse⟩}),
   many1_aux (a::as) n <|> pure (syntax.node ⟨none, (a::as).reverse⟩)
 
 def many1 (r : parser) : parser :=
@@ -77,7 +77,7 @@ private def sep_by_aux (p : m syntax) (sep : parser) (allow_trailing_sep : bool)
   let p := if p_opt then some <$> p <|> pure none else some <$> p,
   some a ← catch p (λ msg, throw {msg with custom :=
     -- append `syntax.missing` to make clear that list is incomplete
-    syntax.node ⟨none, (syntax.missing::msg.custom::as).reverse⟩})
+    syntax.node ⟨none, (syntax.missing::msg.custom.get::as).reverse⟩})
     | pure (syntax.node ⟨none, as.reverse⟩),
   -- I don't want to think about what the output on a failed separator parse should look like
   let sep := try sep,
@@ -121,7 +121,7 @@ instance sep_by1.view {α β} (p sep : parser) (a) [parser.has_view p α] [parse
 def optional (r : parser) : parser :=
 do r ← optional $
      -- on error, wrap in "some"
-     catch r (λ msg, throw {msg with custom := syntax.node ⟨none, [msg.custom]⟩}),
+     catch r (λ msg, throw {msg with custom := syntax.node ⟨none, [msg.custom.get]⟩}),
    pure $ match r with
    | some r := syntax.node ⟨none, [r]⟩
    | none   := syntax.node ⟨none, []⟩

library/init/lean/parser/identifier.lean

@@ -38,7 +38,7 @@ def is_id_end_escape (c : char) : bool :=
 c = id_end_escape
 
 namespace parser
-variables {m : Type → Type} {μ : Type} [monad m] [monad_parsec μ m] [alternative m] [inhabited μ]
+variables {m : Type → Type} {μ : Type} [monad m] [monad_parsec μ m] [alternative m]
 open monad_parsec
 
 def id_part_default : m string :=

library/init/lean/parser/module.lean

@@ -83,14 +83,14 @@ private def commands_aux : bool → nat → module_parser_m unit
       -- unknown command: try to skip token, or else single character
       when (¬ recovering) $ do {
         it ← left_over,
-        log_message {expected := dlist.singleton "command", it := it, custom := ()}
+        log_message {expected := dlist.singleton "command", it := it, custom := some ()}
       },
       try (monad_lift token *> pure ()) <|> (any *> pure ()),
       pure (tt, none)
     }) $ λ msg, do {
       -- error inside command: log error, return partial syntax tree
       log_message msg,
-      pure (tt, some msg.custom)
+      pure (tt, some msg.custom.get)
     },
   match c with
   | some c := yield_command c *> commands_aux recovering n
@@ -120,7 +120,7 @@ def module.parser : module_parser_m unit := do
   ) $ λ msg, do {
     -- fatal error (should only come from header.parser or eoi), yield partial syntax tree and stop
     log_message msg,
-    yield_command msg.custom
+    yield_command msg.custom.get
   },
   it ← left_over,
   -- add `eoi` node for left-over input

library/init/lean/parser/parsec.lean

@@ -23,7 +23,7 @@ structure message (μ : Type := unit) :=
 (it         : iterator)
 (unexpected : string       := "")          -- unexpected input
 (expected   : dlist string := dlist.empty) -- expected productions
-(custom     : μ)
+(custom     : option μ)
 
 def expected.to_string : list string → string
 | []       := ""
@@ -85,8 +85,8 @@ do r ← p s.mk_iterator,
 def eps : parsec_t μ m unit :=
 parsec_t.pure ()
 
-protected def failure [inhabited μ] : parsec_t μ m α :=
-λ it, pure (error { unexpected := "failure", it := it, custom := default μ } ff)
+protected def failure : parsec_t μ m α :=
+λ it, pure (error { unexpected := "failure", it := it, custom := none } ff)
 
 def merge (msg₁ msg₂ : message μ) : message μ :=
 { expected := msg₁.expected ++ msg₂.expected, ..msg₁ }
@@ -200,7 +200,7 @@ match r with
   | error msg₁ ff := do { r ← q it, pure $ orelse_mk_res msg₁ r }
   | other         := pure other
 
-instance [inhabited μ] : alternative (parsec_t μ m) :=
+instance : alternative (parsec_t μ m) :=
 { orelse         := λ _, parsec_t.orelse,
   failure        := λ _, parsec_t.failure,
   ..parsec_t.monad }
@@ -255,9 +255,10 @@ instance monad_parsec_trans {m n : Type → Type} [has_monad_lift m n] [monad_fu
 
 namespace monad_parsec
 open parsec_t
-variables {m : Type → Type} [monad m] [monad_parsec μ m] [inhabited μ] {α β : Type}
+variables {m : Type → Type} [monad m] [monad_parsec μ m] {α β : Type}
 
-def error {α : Type} (unexpected : string) (expected : dlist string := dlist.empty) (it : option iterator := none) (custom : μ := default _) : m α :=
+def error {α : Type} (unexpected : string) (expected : dlist string := dlist.empty)
+          (it : option iterator := none) (custom : option μ := none) : m α :=
 lift $ λ it', result.error { unexpected := unexpected, expected := expected, it := it.get_or_else it', custom := custom } ff
 
 def left_over : m iterator :=
@@ -365,7 +366,7 @@ def str (s : string) : m string :=
 if s.is_empty then pure ""
 else lift $ λ it, match str_aux s.length s.mk_iterator it with
   | some it' := result.ok s it' none
-  | none     := result.error { it := it, expected := dlist.singleton (repr s), custom := default μ } ff
+  | none     := result.error { it := it, expected := dlist.singleton (repr s), custom := none } ff
 
 private def take_aux : nat → string → iterator → result μ string
 | 0     r it := result.ok r it none
@@ -575,10 +576,10 @@ variables {m : Type → Type} [monad m] {α β : Type}
 def parse (p : parsec_t μ m α) (s : string) (fname := "") : m (except (message μ) α) :=
 run p s fname
 
-def parse_with_eoi [inhabited μ] (p : parsec_t μ m α) (s : string) (fname := "") : m (except (message μ) α) :=
+def parse_with_eoi (p : parsec_t μ m α) (s : string) (fname := "") : m (except (message μ) α) :=
 run (p <* eoi) s fname
 
-def parse_with_left_over [inhabited μ] (p : parsec_t μ m α) (s : string) (fname := "") : m (except (message μ) (α × iterator)) :=
+def parse_with_left_over (p : parsec_t μ m α) (s : string) (fname := "") : m (except (message μ) (α × iterator)) :=
 run (prod.mk <$> p <*> left_over) s fname
 
 end parsec_t

library/init/lean/parser/rec.lean

@@ -33,7 +33,7 @@ private def run_aux (base : α → m δ) (rec : α → rec_t α δ m δ) : nat
 protected def run (x : rec_t α δ m β) (base : α → m δ) (rec : α → rec_t α δ m δ) (max_rec : ℕ) : m β :=
 x.run (run_aux base rec max_rec)
 
-protected def run_parsec {γ : Type} [inhabited γ] [monad_parsec γ m] (x : rec_t α δ m β)
+protected def run_parsec {γ : Type} [monad_parsec γ m] (x : rec_t α δ m β)
   (rec : α → rec_t α δ m δ) : m β :=
 do it ← monad_parsec.left_over,
    rec_t.run x (λ _, monad_parsec.error "rec_t.run_parsec: no progress") rec (it.remaining+1)

library/init/lean/parser/string_literal.lean

@@ -9,7 +9,7 @@ import init.lean.parser.parsec
 namespace lean
 namespace parser
 open monad_parsec
-variables {m : Type → Type} {μ : Type} [monad m] [monad_parsec μ m] [alternative m] [inhabited μ]
+variables {m : Type → Type} {μ : Type} [monad m] [monad_parsec μ m] [alternative m]
 
 def parse_hex_digit : m nat :=
 (    (do d ← digit, pure $ d.val - '0'.val)