Skip to content

Commit

Permalink
Add between parser combinator
Browse files Browse the repository at this point in the history
Implement parens in terms of between.
  • Loading branch information
justjoheinz committed Nov 18, 2024
1 parent fc3d2a0 commit 1fe35f9
Showing 1 changed file with 11 additions and 0 deletions.
11 changes: 11 additions & 0 deletions libs/contrib/Data/String/Parser.idr
Original file line number Diff line number Diff line change
Expand Up @@ -406,3 +406,14 @@ export
ntimes : Monad m => (n : Nat) -> ParseT m a -> ParseT m (Vect n a)
ntimes Z p = pure Vect.Nil
ntimes (S n) p = [| p :: (ntimes n p) |]


||| Run the parser p between the opening parser `o` and the closing parser `c`,
||| returning the result of p.
export
between : Monad m => ParseT m o -> ParseT m c -> ParseT m p -> ParseT m p
between o c p = do
_ <- o
result <- p
_ <- c
pure result

0 comments on commit 1fe35f9

Please sign in to comment.