From 64b5e05a3eedfb82db9169a8536f14d88fcf1d6d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 27 Sep 2018 14:53:30 -0700
Subject: [PATCH] feat(library/init/lean/parser/parsec): try to minimize the
 amount of inlined code

---
 library/init/lean/parser/parsec.lean | 34 ++++++++++++++++------------
 1 file changed, 20 insertions(+), 14 deletions(-)

diff --git a/library/init/lean/parser/parsec.lean b/library/init/lean/parser/parsec.lean
index d43d2a3888..a4e1561747 100644
--- a/library/init/lean/parser/parsec.lean
+++ b/library/init/lean/parser/parsec.lean
@@ -93,13 +93,13 @@ protected def failure [inhabited μ] : parsec_t μ m α :=
 def merge (msg₁ msg₂ : message μ) : message μ :=
 { expected := msg₁.expected ++ msg₂.expected, ..msg₁ }
 
-private def bind_1 (r : result μ β) : result μ β :=
+private def bind_mk_res_ok (r : result μ β) : result μ β :=
 match r with
 | ok_eps b it msg₂ := ok b it
 | error msg ff     := error msg tt
 | other            := other
 
-private def bind_2 (ex₁) (r : result μ β) : result μ β :=
+private def bind_mk_res_ok_eps (ex₁) (r : result μ β) : result μ β :=
 match r with
 | ok_eps b it ex₂ := ok_eps b it (ex₁ ++ ex₂)
 | error msg₂ ff   := error { expected := ex₁ ++ msg₂.expected, .. msg₂ } ff
@@ -116,9 +116,9 @@ match r with
 λ it, do
  r ← p it,
  match r with
- | ok a it := bind_1 <$> q a it
- | ok_eps a it ex₁ := bind_2 ex₁ <$> q a it
- | error msg c := pure (error msg c)
+ | ok a it         := bind_mk_res_ok <$> q a it
+ | ok_eps a it ex₁ := bind_mk_res_ok_eps ex₁ <$> q a it
+ | error msg c     := pure (error msg c)
 
 instance : monad (parsec_t μ m) :=
 { bind := λ _ _, parsec_t.bind, pure := λ _, parsec_t.pure }
@@ -144,14 +144,22 @@ instance : has_monad_lift m (parsec_t μ m) :=
 def expect (msg : message μ) (exp : string) : message μ :=
 {expected := dlist.singleton exp, ..msg}
 
-@[inline] def labels (p : parsec_t μ m α) (lbls : dlist string) : parsec_t μ m α :=
-λ it, do
-  r ← p it,
-  pure $ match r with
+private def labels_mk_res (r : result μ α) (lbls : dlist string) : result μ α :=
+match r with
   | ok_eps a it _  := ok_eps a it lbls
   | error msg ff   := error {expected := lbls, ..msg} ff
   | other          := other
 
+@[inline] def labels (p : parsec_t μ m α) (lbls : dlist string) : parsec_t μ m α :=
+λ it, do
+  r ← p it,
+  pure $ labels_mk_res r lbls
+
+private def try_mk_res (r : result μ α) : result μ α :=
+match r with
+| error msg _  := error msg ff
+| other        := other
+
 /--
 `try p` behaves like `p`, but it pretends `p` hasn't
 consumed any input when `p` fails.
@@ -172,11 +180,9 @@ Without the `try` combinator we will not be able to backtrack on the `let` keywo
 @[inline] def try (p : parsec_t μ m α) : parsec_t μ m α :=
 λ it, do
   r ← p it,
-  pure $ match r with
-  | error msg _  := error msg ff
-  | other        := other
+  pure $ try_mk_res r
 
-private def orelse_cont (msg₁ : message μ) (r : result μ α) : result μ α :=
+private def orelse_mk_res (msg₁ : message μ) (r : result μ α) : result μ α :=
 match r with
 | ok_eps a it' ex₂ := ok_eps a it' (msg₁.expected ++ ex₂)
 | error msg₂ ff    := error (merge msg₁ msg₂) ff
@@ -198,7 +204,7 @@ match r with
 λ it, do
   r ← p it,
   match r with
-  | error msg₁ ff := do { r ← q it, pure $ orelse_cont msg₁ r }
+  | error msg₁ ff := do { r ← q it, pure $ orelse_mk_res msg₁ r }
   | other         := pure other
 
 instance [inhabited μ] : alternative (parsec_t μ m) :=