Cannot match a variable against an optional non-terminal in a rule definition

[yusungsim]

Hi, I'm currently experimenting with SpecTec to specify the Rust programming language's syntax and semantics. During the process, I found a case where SpecTec toolchain fails to parse the optional nonterminal (i.e. x?) in the rule definition.

The below DSL code is a minified version of the error inducing code.

Code of interest :

;; syntax blockExpression =
;;     | Stmts statements?

syntax blockExpression
    = statements?

syntax statement =
    | LetStmt blockExpression 

syntax statements =
    | Stmts statement*


syntax state = nat  (; just for demo ;)           

relation interp_statement:  state |- statement -> state

rule interp_statement/let :
    s |- LetStmt be -> s

And the below is the result of running ./watsup to compile above code into LaTeX, which emits an error message that cannot match the expected type of optional non-terminal.

The error message :

$ ./watsup min_optional/a.watsup --latex
min_optional/a.watsup:22.10-22.20: type error: expression does not match expected type `blockExpression` = `statements?`

The error states that it cannot match the nonterminal blockExpression with the variable be, which in case the blockExpression is an option of statements.

Interestingly, if you replace the syntax definition of blockExpression with the same version written in the variant (ie. first two commented lines in the DSL code block), SpecTec successfully parses it and produces a LaTeX code.

I expect that the toolchain should accept the original code, also, because there are no actual difference between defining blockExpression directly as an option of statements or using a single variant. I'm not sure if it is a bug, or it is intended to reject such use of optional element.

[rossberg]

Right, that's one of the annoying ad-hoc limitations of the frontend right now. It uses backtracking to disambiguate some of these cases, but only in shallow ways that cannot handle more general ones.

Incidentally, though, I'm already in the process of reworking the frontend to change that and operate more consistently. It should also produce better error messages. I can't give an ETA, but hope that it's gonna be a couple of weeks.

[yusungsim]

Thank you for checking this so quickly :) I think it should be fine for now using a workaround with the variant. Once the frontend reworking is complete, please let me know, and I'll try it for myself.