core: nom and surround

This commit is contained in:
Nathan McCarty 2025-01-25 12:56:42 -05:00
parent 3029432699
commit 59fba4584d

View file

@ -198,6 +198,7 @@ Lift a parser producing a `List` or `List1` of `Char` into a parser producing a
`String`
```idris
-- TODO: Rename these
export
parseString : Parser (List Char) -> Parser String
parseString x = do
@ -250,6 +251,40 @@ exactString str with (asList str)
pure input
```
Wrap a parser in delimiter characters, discarding the value of the delimiters
```idris
export
delimited : (before, after : Char) -> Parser a -> Parser a
delimited before after x = do
starting_state <- save
_ <- parseExactChar before
val <- x
Just _ <- tryMaybe $ parseExactChar after
| _ => throw $
MkParseError starting_state "Unmatched delimiter \{show before}"
pure val
```
Consume any number of characters of the provided character class and discard the
result. Also a version for doing so on both sides of a provided parser
```idris
export
nom : Parser Char -> Parser ()
nom x = do
_ <- many x
pure ()
export
surround : (around : Parser Char) -> (item : Parser a) -> Parser a
surround around item = do
nom around
val <- item
nom around
pure val
```
### Composition of boolean functions
```idris