Cryptol record parsing incorrect?

[weaversa]

Is saw miscounting curly braces? The cryptol interpreter seems to think everything is ok.

sawscript> print {{ {x=10, y=1} }}
[19:41:28.566] Assuming a = Integer
[19:41:28.566] Assuming b = Integer
[19:41:28.567] {x = 10, y = 1}
sawscript> print {{ {x=10, y={a=1, b=2}} }}
Parse error at <stdin>:1:31-1:32: Unexpected `}'
sawscript> print {{ {x=10, y={a=1, b=2} }}

user error (Cryptol parse error:
Parse error at <stdin>:2:0,
  unexpected: end of file)

Cryptol> {x=10, y=11}
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type of field 'x'
  * Using 'Integer' for type of field 'y'
{x = 10, y = 11}
Cryptol> {x=10, y={a=1, b=2}}
Showing a specific instance of polymorphic result:
  * Using 'Integer' for type of field 'x'
  * Using 'Integer' for type of field 'a'
  * Using 'Integer' for type of field 'b'
{x = 10, y = {a = 1, b = 2}}

[brianhuffman]

The saw-script lexer treats any occurrence of }} as the end of the Cryptol quotes. As a workaround you'll need to put a space between the two close braces in your embedded Cryptol, like this:

print {{ {x=10, y={a=1, b=2} } }}

instead of this:

print {{ {x=10, y={a=1, b=2}} }}

As for alternatives, we could:

• Change the saw-script cryptol quotes from {{ }} to some other combination that can't occur in valid cryptol code. However this would be a major breaking change (very unwise).
• Make the saw-script lexer count open braces in embedded cryptol syntax, and don't look for the closing }} until all internal braces are matched. A naive implementation of this rule would have problems if your cryptol code included a quoted string containing unmatched { or } characters, though, so we'd have to make the saw-script lexer pretty sophisticated.

[weaversa]

@brianhuffman Thanks for discovering what's going on. I feel that as long as the limitations of the parser are documented somewhere (maybe this ticket is good enough) and there's an easy workaround, then we can move on.