| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Lang.Crucible.Syntax.Monad
Synopsis
- class (Alternative m, Monad m) => MonadSyntax atom m | m -> atom where
- describe :: MonadSyntax atom m => Text -> m a -> m a
- atom :: (MonadSyntax atom m, IsAtom atom, Eq atom) => atom -> m ()
- cons :: MonadSyntax atom m => m a -> m b -> m (a, b)
- depCons :: MonadSyntax atom m => m a -> (a -> m b) -> m b
- depConsCond :: MonadSyntax atom m => m a -> (a -> m (Either Text b)) -> m b
- followedBy :: MonadSyntax atom m => m a -> m b -> m b
- rep :: MonadSyntax atom m => m a -> m [a]
- list :: MonadSyntax atom m => [m a] -> m [a]
- backwards :: MonadSyntax atom m => m a -> m a
- emptyList :: MonadSyntax atom m => m ()
- atomic :: MonadSyntax atom m => m atom
- anyList :: MonadSyntax atom m => m [Syntax atom]
- sideCondition :: MonadSyntax atom m => Text -> (a -> Maybe b) -> m a -> m b
- sideCondition' :: MonadSyntax atom m => Text -> (a -> Bool) -> m a -> m a
- satisfy :: MonadSyntax atom m => (Syntax atom -> Bool) -> m (Syntax atom)
- syntaxToDatum :: Syntactic expr atom => expr -> Datum atom
- datum :: (MonadSyntax atom m, IsAtom atom, Eq atom) => Datum atom -> m ()
- position :: MonadSyntax atom m => m Position
- withProgressStep :: MonadSyntax atom m => ProgressStep -> m a -> m a
- commit :: MonadSyntax atom m => m ()
- parse :: MonadSyntax atom m => Syntax atom -> m a -> m a
- data ProgressStep
- data Progress
- emptyProgress :: Progress
- pushProgress :: ProgressStep -> Progress -> Progress
- later :: MonadSyntax atom m => m a -> m a
- data Reason atom = Reason {}
Documentation
class (Alternative m, Monad m) => MonadSyntax atom m | m -> atom where Source #
Monads that can parse syntax need a few fundamental operations.
A parsing monad maintains an implicit "focus", which is the syntax
currently being matched, as well as the progress, which is the path
taken through the surrounding syntactic context to reach the
current focus. Additionally, the reason for a failure will always
be reported with respect to explicit descriptions - these are
inserted through withReason.
Methods
anything :: m (Syntax atom) Source #
Succeed with the current focus.
progress :: m Progress Source #
Succeed with the current progress.
withFocus :: Syntax atom -> m a -> m a Source #
Run a new parser with a different focus.
withProgress :: (Progress -> Progress) -> m a -> m a Source #
Run a parser in a modified notion of progress.
withReason :: Reason atom -> m a -> m a Source #
Run a parser with a new reason for failure.
Fail, and additionally prohibit backtracking across the failure.
delimit :: m a -> m a Source #
Delimit the dynamic extent of a cut.
Make the first solution reported by a computation into the only solution reported, eliminating further backtracking and previous errors. This allows syntax to be matched in exclusive "layers", reminiscent of the effect of trampolining through a macro expander. Use when solutions are expected to be unique.
Instances
Describing syntax
describe :: MonadSyntax atom m => Text -> m a -> m a Source #
Annotate a parser with a description, documenting its role in the grammar. These descriptions are used to construct error messages.
atom :: (MonadSyntax atom m, IsAtom atom, Eq atom) => atom -> m () Source #
Succeed if and only if the focus is some particular given atom.
cons :: MonadSyntax atom m => m a -> m b -> m (a, b) Source #
If the current focus is a list, apply one parser to its head and another to its tail.
depCons :: MonadSyntax atom m => m a -> (a -> m b) -> m b Source #
Use the result of parsing the head of the current-focused list to compute a parsing action to use for the tail of the list.
depConsCond :: MonadSyntax atom m => m a -> (a -> m (Either Text b)) -> m b Source #
A dependent cons (see depcons) that can impose a validation
step on the head of a list focus. If the head fails the validation
(that is, the second action returns Left), the error is reported
in the head position.
followedBy :: MonadSyntax atom m => m a -> m b -> m b Source #
If the current focus is a list, apply one parser to its head and another to its tail, ignoring the result of the head.
rep :: MonadSyntax atom m => m a -> m [a] Source #
Produce a parser that matches a list of things matched by another parser.
list :: MonadSyntax atom m => [m a] -> m [a] Source #
Match a list focus elementwise.
backwards :: MonadSyntax atom m => m a -> m a Source #
When the current focus is a list, reverse its contents while invoking another parser. If it is not a list, fail.
emptyList :: MonadSyntax atom m => m () Source #
Succeed if and only if the focus is the empty list.
atomic :: MonadSyntax atom m => m atom Source #
Succeed if and only if the focus is any atom, returning the atom.
anyList :: MonadSyntax atom m => m [Syntax atom] Source #
Succeed if and only if the focus is a list, returning its contents.
sideCondition :: MonadSyntax atom m => Text -> (a -> Maybe b) -> m a -> m b Source #
Impose a side condition on a parser, failing with the given
description if the side condition is Nothing.
sideCondition' :: MonadSyntax atom m => Text -> (a -> Bool) -> m a -> m a Source #
Impose a Boolean side condition on a parser, failing with the
given description if the side condition is False.
satisfy :: MonadSyntax atom m => (Syntax atom -> Bool) -> m (Syntax atom) Source #
Succeed if and only if the focus satisfies a Boolean predicate.
Eliminating location information
syntaxToDatum :: Syntactic expr atom => expr -> Datum atom Source #
Strip location information from a syntax object
datum :: (MonadSyntax atom m, IsAtom atom, Eq atom) => Datum atom -> m () Source #
Succeed only if the focus, having been stripped of position information, is structurally equal to some datum.
Parsing context
position :: MonadSyntax atom m => m Position Source #
Return the source position of the focus.
withProgressStep :: MonadSyntax atom m => ProgressStep -> m a -> m a Source #
Manually add a progress step to the current path through the
context. Use this to appropriately guard calls to parse.
Control structures
commit :: MonadSyntax atom m => m () Source #
Trivially succeed, but prevent backtracking.
parse :: MonadSyntax atom m => Syntax atom -> m a -> m a Source #
Manually override the focus. Use this with care - it can lead to
bogus error selection unless withProgress is used to provide an
appropriate path.
Progress through a parsing problem
data ProgressStep Source #
Components of a path taken through a syntax object to reach the current focus.
Constructors
| First | The head of a list was followed |
| Rest | The tail of a list was followed |
| Late | The path was annotated as |
Instances
| Show ProgressStep Source # | |
Defined in Lang.Crucible.Syntax.Monad Methods showsPrec :: Int -> ProgressStep -> ShowS # show :: ProgressStep -> String # showList :: [ProgressStep] -> ShowS # | |
| Eq ProgressStep Source # | |
Defined in Lang.Crucible.Syntax.Monad | |
| Ord ProgressStep Source # | |
Defined in Lang.Crucible.Syntax.Monad Methods compare :: ProgressStep -> ProgressStep -> Ordering # (<) :: ProgressStep -> ProgressStep -> Bool # (<=) :: ProgressStep -> ProgressStep -> Bool # (>) :: ProgressStep -> ProgressStep -> Bool # (>=) :: ProgressStep -> ProgressStep -> Bool # max :: ProgressStep -> ProgressStep -> ProgressStep # min :: ProgressStep -> ProgressStep -> ProgressStep # | |
The path taken through a syntax object to reach the current focus.
emptyProgress :: Progress Source #
An empty path, used to initialize parsers
pushProgress :: ProgressStep -> Progress -> Progress Source #
Add a step to a progress path
Errors
later :: MonadSyntax atom m => m a -> m a Source #
Transform a parser such that its errors are considered to occur after others, and thus be reported with a higher priority.