max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/lean/parser/parsec): mark *_mk_res functions as [inline_if_reduce]

Browse source
This commit is contained in:
Leonardo de Moura 2018-10-25 10:10:54 -07:00
parent 628b0c7919
commit 370f67b27b
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/init/lean/parser/parsec.lean
View file

@ -91,7 +91,7 @@ protected def failure : parsec_t μ m α :=
def merge (msg₁ msg₂ : message μ) : message μ :=
{ expected := msg₁.expected ++ msg₂.expected, ..msg₁ }
@[inline] private def bind_mk_res (ex₁ : option (dlist string)) (r : result μ β) : result μ β :=
@[inline_if_reduce] private def bind_mk_res (ex₁ : option (dlist string)) (r : result μ β) : result μ β :=
match ex₁, r with
| none, ok b it _ := ok b it none
| none, error msg _ := error msg tt
@ -148,6 +148,7 @@ match r with
r ← p it,
pure $ labels_mk_res r lbls
@[inline_if_reduce]
private def try_mk_res (r : result μ α) : result μ α :=
match r with
| error msg _ := error msg ff
@ -175,7 +176,7 @@ Without the `try` combinator we will not be able to backtrack on the `let` keywo
r ← p it,
pure $ try_mk_res r
@[inline] private def orelse_mk_res (msg₁ : message μ) (r : result μ α) : result μ α :=
@[inline_if_reduce] private def orelse_mk_res (msg₁ : message μ) (r : result μ α) : result μ α :=
match r with
| ok a it' (some ex₂) := ok a it' (some $ msg₁.expected ++ ex₂)
| error msg₂ ff := error (merge msg₁ msg₂) ff