Grammar rules as documentation on the AST module #975
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.
Following a discussion with @karthikbhargavan, @cmester0 and I have been experimenting with putting OCaml comments directly onto the AST module, documenting the grammar rules covered by the internal AST of hax.
However, we believe that's not the best way to do things.
@cmester0 had a great idea: use the rust printer of hax to generate the grammar.
The idea is the following:
enumerate
anddefault
enumerate
for typet
is of typet set
,default
for typet
is of typet
enumerate
for eacht
scalar will be a default value (say 0 for ints, "" for strings, etc.)enumerate
oft list
would be all possible combinations of the valuesenumerate<t>
in list of length from zero to say 3enumerate
oft option
would be the setNone
andSome
of all the values inenumerate
for typet
default
andenumerate
. We need to make sure thoseenumerate
are finite somehow (we can have aseen
list of values, or do something statically, let's see)Status: let's not merge this