Unexpected interaction of comments and Cryptol blocks

[sauclovian-g]

The saw-script lexer treats Cryptol blocks (both terms and types) as lexemes and doesn't look inside them at all. This means comments in Cryptol blocks are handled by Cryptol's lexer downstream, and that has some odd consequences:

1. Comments that start in Cryptol blocks end at the end of the Cryptol block.

sawscript> let x = {{ /* 3 }} */
Parse error at <stdin>:1:20-1:22: Unexpected `*/'

and

sawscript> let x = ( {{ 1 // one }}, 2)
sawscript> return x
[21:06:41.173] (\(u1217 : isort 0) ->
  \(_P : PLiteral u1217) -> ecNumber (TCNum 1) u1217 _P,2)

(the }} and after is not commented out)

2. Comments that appear to end in Cryptol blocks actually don't, because the Cryptol block is recognized even inside a comment:

sawscript> let x = /* {{ 1 */ 2 }}
<stdin>:1:9-1:11: Unclosed block comment
Parse error at <stdin>:2:1-2:1: Unexpected `EOF'

and

let x = // {{ 3
}};
"abc";

which succeeds leaves x bound to "abc".

All this is not entirely desirable, and the last behavior is definitely confusing. On the minus side it's not clear that this is fixable without rewriting the lexer with an entirely different approach.