Parens and "Unexpected end of layout block"

[weaversa]

It would be nice to be able to parenthesize valid cryptol statements in the interpreter. For example, the following statements give errors
(x where x = 1) + 1 and (f where f x = x+1) 10

Main> x where x = 1
Assuming a = 1
1
Main> (x where x = 1)

Parse error at 2:1, unexpected end of layout block
Main> (x where x = 1) + 1

Parse error at 1:17, unexpected +
Main> f where f x = x+1
Assuming a = 1
<function>
Main> :t f where f x = x+1
f
where
  f x = x + 1
 : {a} (a >= 1, fin a) => [a] -> [a]
Main> f where f x = x+1 10
[warning] at <interactive>:1:1--1:21:
  Defaulting type parameter 'bits'
             of literal or demoted expression
             at <interactive>:1:19--1:21
  to 4
[warning] at <interactive>:1:1--1:21:
  Defaulting type parameter 'bits'
             of literal or demoted expression
             at <interactive>:1:17--1:18
  to 1

[error] at <interactive>:1:17--1:21:
  Type mismatch:
    Expected type: [?y20] -> ?d21
    Inferred type: [?a21]
  where
  ?y20 is type parameter 'bits'
          of literal or demoted expression
          at <interactive>:1:19--1:21
  ?a21 is type parameter 'bits'
          of literal or demoted expression
          at <interactive>:1:17--1:18
  ?d21 is 1st type parameter
          of expression (+)
          at <interactive>:1:16--1:17
Main> (f where f x = x+1) 10
Parse error at 1:21, unexpected 10

[acfoltzer]

Confirmed that this doesn't only occur in the interpreter, but also if you have such expressions in files. It only seems to arise with where clauses, so something funky must be going on in the layout-handling code. For example (\x -> x + 1) 10 works fine.

Added a test case for this in 17ee75e.

[elliottt]

The layout processor didn't account for layout blocks that were terminated by parens or braces, so this accounts for that in the context stack that is kept by the layout processor.

[brianhuffman]

@elliottt Changeset 3487737 broke one of the regression tests, involving AES.cry. The parser now does the wrong thing if the first token after where is an open parenthesis. For example:

Cryptol> x + y where [x,y] = [3:[8], 4:[8]]
7
Cryptol> x + y where (x,y) = (3:[8], 4:[8])

Parse error at 2:1, unexpected end of input

[elliottt]

I've fixed the AES regression, but there was another test (regression/r03.icry) that was failing for seemingly unrelated reasons. @brianhuffman, let me know if you notice anything else, otherwise I'll hopefully close this one :)

[brianhuffman]

@elliottt Everything looks good to me now: no failed regressions, and back down to 4 failing issue tests. In particular, regression/r03.icry works for me; maybe something there is dependent on which version of cvc4 you have?