Skip to content

Commit

Permalink
Add between parser combinator (#3414)
Browse files Browse the repository at this point in the history
Implement parens in terms of between.
  • Loading branch information
justjoheinz authored Dec 2, 2024
1 parent 35cbbcc commit ec74792
Showing 1 changed file with 9 additions and 1 deletion.
10 changes: 9 additions & 1 deletion libs/contrib/Data/String/Parser.idr
Original file line number Diff line number Diff line change
Expand Up @@ -285,10 +285,17 @@ covering
spaces1 : Monad m => ParseT m ()
spaces1 = skip (some space) <?> "whitespaces"


||| 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 = id <$ o <*> p <* c

||| Discards brackets around a matching parser
export
parens : Monad m => ParseT m a -> ParseT m a
parens p = char '(' *> p <* char ')'
parens p = between (char '(') (char ')') p

||| Discards whitespace after a matching parser
export
Expand Down Expand Up @@ -406,3 +413,4 @@ 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) |]

0 comments on commit ec74792

Please sign in to comment.