Support for custom syntax extensions #2909
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds support for custom syntax extensions.
You can write in place of a top-level declaration
```your_dsl_name
whatever syntax
```
In a compiler plugin, you can call
passing "your_dsl_name" to register a custom parser for whatever syntax your DSL chooses.
The
extension_parser
has type:receiving:
open_namespaces_and_abbreviations: The open namespaces and module abbreviations in the current scope environment
the concrete syntax of the your DSL as a string
The source range at which the string begins (so you can report syntax errors relative to the position in the source file)
and returning
either an error message or a FStar.Parser.AST.decl'. If the latter, then this decl' is processed by the rest of the compiler pipeline as is.
For an example of this mechanism see: https://github.com/FStarLang/steel/blob/nik_ranges/share/steel/examples/pulse/CustomSyntax.fst