From 38bc3beffbafad5bb0773bde1a8b4b77c457ff03 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 17 Oct 2018 14:25:50 -0700
Subject: [PATCH] fix(library/init): `alternative` instances
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Both `alternative` and `monad` implement `applicative`. However,
their default implementations for `seq_right` and `seq_left` are
different. The `alternative` implementation uses the inefficient default
version for `seq_right` available at `applicative`:
```
(seq_right := λ α β a b, const α id <$> a <*> b)
```
instead of the more efficient
```
(seq_right := λ α β x y, x >>= λ _, y)
```
defined at `monad` using the `bind` operator.

This commit makes sure the `applicative` instances for `reader_t`,
`state_t`, `option` and `parsec_t` use the efficient version.
I found the problem when inspecting the generated code for:
```
def symbol (s : string) : parsec' unit :=
(str s *> whitespace) <?> ("'" ++ s ++ "'")
```
---
 library/init/control/reader.lean     | 3 ++-
 library/init/control/state.lean      | 3 ++-
 library/init/data/option/basic.lean  | 3 ++-
 library/init/lean/parser/parsec.lean | 5 +++--
 4 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/library/init/control/reader.lean b/library/init/control/reader.lean
index 7ede948c25..1fa9d7a369 100644
--- a/library/init/control/reader.lean
+++ b/library/init/control/reader.lean
@@ -59,7 +59,8 @@ section
 
   instance [alternative m] : alternative (reader_t ρ m) :=
   { failure := @reader_t.failure _ _ _ _,
-    orelse  := @reader_t.orelse _ _ _ _ }
+    orelse  := @reader_t.orelse _ _ _ _,
+    ..reader_t.monad }
 
   instance (ε) [monad m] [monad_except ε m] : monad_except ε (reader_t ρ m) :=
   { throw := λ α, reader_t.lift ∘ throw,
diff --git a/library/init/control/state.lean b/library/init/control/state.lean
index 58df17a9ff..4074bd7c48 100644
--- a/library/init/control/state.lean
+++ b/library/init/control/state.lean
@@ -43,7 +43,8 @@ section
 
   instance [alternative m] : alternative (state_t σ m) :=
   { failure := @state_t.failure _ _ _ _,
-    orelse  := @state_t.orelse _ _ _ _ }
+    orelse  := @state_t.orelse _ _ _ _,
+    ..state_t.monad }
 
   @[inline] protected def get : state_t σ m σ :=
   λ s, pure (s, s)
diff --git a/library/init/data/option/basic.lean b/library/init/data/option/basic.lean
index bc91b160e0..3679277f6e 100644
--- a/library/init/data/option/basic.lean
+++ b/library/init/data/option/basic.lean
@@ -55,7 +55,8 @@ protected def orelse {α : Type u} : option α → option α → option α
 
 instance : alternative option :=
 { failure := @none,
-  orelse  := @option.orelse }
+  orelse  := @option.orelse,
+  ..option.monad }
 
 protected def lt {α : Type u} (r : α → α → Prop) : option α → option α → Prop
 | none (some x)     := true
diff --git a/library/init/lean/parser/parsec.lean b/library/init/lean/parser/parsec.lean
index 8ab979b37d..943ebfd12a 100644
--- a/library/init/lean/parser/parsec.lean
+++ b/library/init/lean/parser/parsec.lean
@@ -201,8 +201,9 @@ match r with
   | other         := pure other
 
 instance [inhabited μ] : alternative (parsec_t μ m) :=
-{ orelse  := λ _, parsec_t.orelse,
-  failure := λ _, parsec_t.failure }
+{ orelse         := λ _, parsec_t.orelse,
+  failure        := λ _, parsec_t.failure,
+  ..parsec_t.monad }
 
 /-- Parse `p` without consuming any input. -/
 def lookahead (p : parsec_t μ m α) : parsec_t μ m α :=