Correct syntax for struct pattern wildcards

[Timmmm]

The syntax was changed from .. to _ but this wasn't updated.

[Timmmm]

This is slightly an excuse for me to ask how parsing works. I can't wrap my head around it. The OTT stuff does seem to be used, but clearly not entirely because this mistake doesn't seem to have had any effect. There's also src/lib/parser.mly which seems to do the actual parsing? And the AST seems to be in _build/default/src/lib/ast.ml but then src/lib/parse_ast.ml seems to have a lot of the same code?

I found doc/old/internals.md but I'm not sure how up-to-date it is. Any help appreciated!

[github-actions]

Test Results

    9 files  ±0     20 suites  ±0   0s ⏱️ ±0s
  625 tests ±0    625 ✅ ±0  0 💤 ±0  0 ❌ ±0 
2 006 runs  ±0  2 005 ✅ ±0  1 💤 ±0  0 ❌ ±0 

Results for commit a9f53ce. ± Comparison against base commit ad35e5d.

[Alasdair]

The gist of it is that sail.ott generates ast.lem, which in turn generates ast.ml. The actual syntax in sail.ott doesn't really matter as long as it generates the correct data structure (in some places it's wrong because of this constraint). We could in theory use it for documentation but, the grammar in the manual is instead generated from the parser instead using obelisk. That ott file is very old, if you go back a version of it is in the very first commit, quite a while before I ever worked on Sail!

The reason the build is set up like that is so if you wanted to write part of Sail in Lem (so you could export it to Isabelle and verify it), it can access the syntax tree and it'll generate OCaml that will inter-operate nicely with unverified OCaml parts.

parse_ast.ml is similar to ast.ml (it was at one point generated by another ott file), but it has a little more syntactic sugar. The parser (parser.mly) creates types from that file, and then there's an initial checking/desugaring pass (in initial_check.ml) that maps that onto the actual AST. It's mostly a mechanical 1-to-1 translation but it does a few key things:

• It disambiguates types (we have atyp in parse_ast.ml, then typ, nexp, n_constraint in ast.ml)
• It attaches documentation comments and attributes into the syntax tree
• It parses infix expressions (so we can handle fixity declarations imported from other files)

After that we type check, descatter scattered definitions, and then infer and check effect information. The overall Sail frontend flow is handled in frontend.ml.

[Alasdair]

Oh, another key difference between parse_ast.ml and ast.ml is that the syntax tree in ast.ml is parametric in the annotation type, so when you type check you go from uannot ast to tannot ast - that way you can never mix untyped (uannot) and typed (tannot) terms.

[Timmmm]

Very helpful information, thank you!