From 89afabae29f600dd793b39d23216280a2cd4890a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 21 Oct 2018 10:57:23 -0700 Subject: [PATCH] refactor(library/init/lean/parser/parsec): make sure custom error message doesn't need to be inhabited --- library/init/data/option/basic.lean | 8 ++++---- library/init/data/option/instances.lean | 3 --- library/init/lean/parser/basic.lean | 2 +- library/init/lean/parser/combinators.lean | 8 ++++---- library/init/lean/parser/identifier.lean | 2 +- library/init/lean/parser/module.lean | 6 +++--- library/init/lean/parser/parsec.lean | 19 ++++++++++--------- library/init/lean/parser/rec.lean | 2 +- library/init/lean/parser/string_literal.lean | 2 +- 9 files changed, 25 insertions(+), 27 deletions(-) diff --git a/library/init/data/option/basic.lean b/library/init/data/option/basic.lean index 3679277f6e..42c074fddc 100644 --- a/library/init/data/option/basic.lean +++ b/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 diff --git a/library/init/data/option/instances.lean b/library/init/data/option/instances.lean index 00f7172fdd..9a28e34616 100644 --- a/library/init/data/option/instances.lean +++ b/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 diff --git a/library/init/lean/parser/basic.lean b/library/init/lean/parser/basic.lean index 1920a7d18b..e8d7e87aff 100644 --- a/library/init/lean/parser/basic.lean +++ b/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 diff --git a/library/init/lean/parser/combinators.lean b/library/init/lean/parser/combinators.lean index e1e7847c90..527c6bc7ef 100644 --- a/library/init/lean/parser/combinators.lean +++ b/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, []⟩ diff --git a/library/init/lean/parser/identifier.lean b/library/init/lean/parser/identifier.lean index d7a95eee99..cdf0d021e6 100644 --- a/library/init/lean/parser/identifier.lean +++ b/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 := diff --git a/library/init/lean/parser/module.lean b/library/init/lean/parser/module.lean index 17b78623e8..110f677754 100644 --- a/library/init/lean/parser/module.lean +++ b/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 diff --git a/library/init/lean/parser/parsec.lean b/library/init/lean/parser/parsec.lean index 0c17fce496..baf1b9e8bc 100644 --- a/library/init/lean/parser/parsec.lean +++ b/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 diff --git a/library/init/lean/parser/rec.lean b/library/init/lean/parser/rec.lean index 57e1be56c0..2cfdfeaad9 100644 --- a/library/init/lean/parser/rec.lean +++ b/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) diff --git a/library/init/lean/parser/string_literal.lean b/library/init/lean/parser/string_literal.lean index 8bbddf233f..99560063c6 100644 --- a/library/init/lean/parser/string_literal.lean +++ b/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)