Parse error with infix operator and if-then-else

[robdockins]

The following snippet of Cryptol code used to be accepted, but now does not parse. I feel like it probably should still be accepted.

// Make a buggy version of fib state machine which returns wrong value
// when state counter has magic value.
mk_buggy_fib_no_init : {a} (fin a, a >= 1) => [a] ->
  ([1], ([8], [8], [a])) -> ([8], ([8], [8], [a]))
mk_buggy_fib_no_init magic (_, (fn, fn1, k)) = (fn', (fn1, fn2, k+1))
  where
  fn2 = fn + fn1
  // Change output when state has magic value.
  fn' = fn + if k == magic then 1 else 0

The problem occurs on the final line, where the if keyword seems to interact badly with the + operator. Adding parens around the if then else causes the code to be accepted.

[brianhuffman]

Similarly, the parser rejects lambdas on the right-hand side of infix operators. It would be nice to allow this as well, so that (for example) we could use an infix application operator with a higher-order function:

generate : {n, ix, a} (fin ix, fin n, n >= 1, ix >= width (n - 1)) => ([ix] -> a) -> [n]a
generate f = [ f i | i <- [0 .. n-1] ]

infixl 1 $
f $ x = f x

foo : [10][4]
foo = generate $ \(i:[8]) -> if i == 0 then 1 else foo@(i-1)

[yav]

OK, so I just fixed this one hopefully, both of these examples work. In addition, I added support for something like Haskell's BlockArguments extension, so you can write @brianhuffman's example without the $:

foo : [10][4]
foo = generate \(i:[8]) -> if i == 0 then 1 else foo@(i-1)

I'll add a section to Syntax.md to summarize the high-level syntactic structure of Cryptol expressions